Using rupicola for elliptic curves

[RasmusHoldsbjergCSAU]

I understand from #9 that it is possible to generate C code using Rupicola, but am unsure how

How was the C programs in e.g.
https://github.com/mit-plv/rupicola/blob/master/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.c
and
https://github.com/mit-plv/rupicola/blob/master/src/Rupicola/Examples/Assoc/Assoc.c
generated? I am assuming that they were not written by hand; and I think it would be helpful to try to recreate the steps in generating them.

I am trying make verified implementations of elliptic curve operations and have thus far used Fiat Crypto, but understand that one of the goals of Rupicola is to make compilation that supports functions calls, which could be very helpful.

It is unclear to me what is possible at the current state of Rupicola, as the documentation I have been able to find is sparse; if you could point me to some documentation that would be helpful as well.

[cpitclaudel]

Hi there,

Rupicola is still in exploratory stages at the moment; it's the spiritual successor to https://link.springer.com/chapter/10.1007%2F978-3-030-51054-1_7 , which used Facade and Bedrock 1 and was stuck on an old Coq version.

We don't have end-to-end examples yet for Rupicola; we've generated Bedrock 2 code but not extracted it to C yet. The .c files in the repo are all handwritten as guides of what we want to produce. And indeed the documentation is completely nonexistent, which we'll remediate as we make progress.

I'm currently mentoring an undergrad with the eventual goal of getting slightly-higher level primitives for crypto written in Rupicola, and I think @DIJamner was pondering working on crypto primitives in Rupicola. The best might be to set up a video call to discuss, if you're interested in more details?

[RasmusHoldsbjergCSAU]

Thank you for the reply
A video call would be great; I would love to learn about the project; when would you have time for this?

So the Bedrock code in e.g.
https://github.com/mit-plv/rupicola/blob/master/src/Rupicola/Examples/Assoc/Assoc.v
was generated using Rupicola?

[DIJamner]

Thanks for the mention, I would definitely like to be on that call. I have minimal hard time constraints at the moment, so I'll leave it to @cpitclaudel to suggest a convenient time.

[cpitclaudel]

A video call would be great; I would love to learn about the project; when would you have time for this?

Super. Next week would be best for me. Can you send me an email with Justin in CC?

[jadephilipoom]

There's already some fiat-crypto/rupicola integration in the fiat-crypto repo, see https://github.com/mit-plv/fiat-crypto/tree/master/src/Bedrock/Group

Still very much a work in progress. It's using rupicola to create higher-level functions in bedrock2 and calling fiat-crypto-generated field arithmetic. Not everything quite lines up yet, but might be worth a look!

[RasmusHoldsbjergCSAU]

Hi guys Just a follow-up from the meeting last friday. You spoke of a Mattermost channel that we could use to discuss rupicola related questions; would it be possible to add Benjamin, Bas and myself to this? Also, you might be interested in this; a coq-proof of the equivalence of exponentiation by repeated squaring and recursively multiplying for monoids: https://github.com/RasmusHoldsbjergCSAU/QuadraticFieldExtensions/blob/master/RepeatedSquaring.v Best, Rasmus

…

________________________________ From: jadephilipoom <[email protected]> Sent: 03 November 2020 08:44 To: mit-plv/rupicola <[email protected]> Cc: Rasmus Holdsbjerg-Larsen <[email protected]>; Author <[email protected]> Subject: Re: [mit-plv/rupicola] Using rupicola for elliptic curves (#10) There's already some fiat-crypto/rupicola integration in the fiat-crypto repo, see https://github.com/mit-plv/fiat-crypto/tree/master/src/Bedrock/Group Still very much a work in progress. It's using rupicola to create higher-level functions in bedrock2 and calling fiat-crypto-generated field arithmetic. Not everything quite lines up yet, but might be worth a look! — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub<#10 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AQS3EHU5YA2EN7OCDK4B2O3SN6YERANCNFSM4THJPVHA>.

[cpitclaudel]

You spoke of a Mattermost channel that we could use to discuss rupicola related questions; would it be possible to add Benjamin, Bas and myself to this?

Bas actually pointed out that Zulip would work, and that sounds a lot more convenient than having you all install a new chat client, so I've subscribed to #fiat-crypto there :)