A few questions about Rupicola

[RasmusHoldsbjergCSAU]

I asked these questions on the fiat-crypto zulip stream, but am not sure who has seen the post; so I will post here as well:

We have had a look at the Rupicola project and have a few questions:
We have tried compiling some very simple functions to bedrock2 using rupicola, by simply using the compile tactic after writing the function specification in Gallina. This approach, however, seems insufficient when compiling more complicated functions.
What kinds of functions can the compile tactic reasonably be expected to derive? And how can the compilation procedure be modified/extended to handle different kinds of functions.

Also, we had a look at the derivation of of the MontgomeryLadder here: https://github.com/mit-plv/fiat-crypto/blob/master/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v#L301

This is quite a bit more involved. Can you comment on a general strategy to derive more complicated functions such as this? We are particularly interested in functions making use of loops and function calls, so if you could comment on this, that would be great as well.

The questions are mainly aimed at @jadephilipoom and @cpitclaudel, but anyone with insight is more than welcome to comment : )

[jadephilipoom]

To get rupicola to compile a function, you need to define lemmas for every kind of expression you want to compile (other than the ones in the core library) and add them to the compile_custom tactic so that compile_step will use them. We have only added the lemmas we currently need, so I'm not surprised there are gaps. If you search for lemmas prefixed with compile_, those are compilation lemmas, and you should be able to copy the pattern.

The Montgomery ladder proof is a bit of a mess, to be honest, but the basic structure of the proof is:

• compile the pre-loop part of the function
• apply the compile_downto lemma (which handles the loop using an invariant) and prove its preconditions
• compile the loop body
• compile the post-loop part of the function

At various points the proof converts between "literal" local variables and local-variables-as-separation-logic, which is mostly a side effect of an experiment we were doing at the time but may be helpful to get the loop lemma working. I'd suggest trying with a simple loop first and then scaling up.

[jadephilipoom]

Also, instead of using the compile tactic (which is repeat compile_step, the Montgomery ladder proof uses repeat safe_compile_step, which is a variant of compile_step that only takes a step if it can solve all the side conditions. So wherever you see repeat safe_compile_step, it's essentially trying as many compilation lemmas as it can until it gets stuck and needs special handling again.

[RasmusHoldsbjergCSAU]

Thanks for the response; I have now a few more questions:
At the current state; is it possible to actually generate bedrock functions implementing Montgomery Ladder, and if so how?
Also, with respect to using function calls with Rupicola, is it necessary that the called functions are encoded as bedrock functions? Or would it be possible to reason about the correctness of code calling functions written in e.g. C or Coq?
I ask because I would like to use the Fiat field implementations that perform operations in the Montgomery domain (wordbywordmontgomery in Fiat Crypto), and thus do not strictly satisfy the field axioms for intermediate computations.

[jadephilipoom]

At the current state; is it possible to actually generate bedrock functions implementing Montgomery Ladder, and if so how?

Yes, it is possible to generate the Montgomery ladder function with calls to field functions. In fact, fiat-crypto has a definition and output test for this. The line here prints montgomery_body, which is a bedrock2 function, and redirects it to a file:
https://github.com/mit-plv/fiat-crypto/blob/c86d501734e6645cd61b4514b9c2ce6cacf439b0/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v#L492

The expected value is here (sorry, no nice bedrock2 notations):
https://github.com/mit-plv/fiat-crypto/blob/master/output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected

This version requires the caller to allocate all the memory the function needs for intermediate values. In ScalarMult.v there's a bedrock2 function with a slightly nicer interface; it just allocates the memory and calls the montladder_body function.
https://github.com/mit-plv/fiat-crypto/blob/c86d501734e6645cd61b4514b9c2ce6cacf439b0/src/Bedrock/Group/ScalarMult/ScalarMult.v#L120

There are proofs for these that show they are correct assuming whatever functions you have for field operations match the specifications given in Spec/Field.v. It's highly unfortunate that the fiat-crypto field operation specs are not quite aligned (I've been spending some of my free time on fixing the issue, but it's not my day job and may still take some time), but if you wanted to write some untrusted glue code that makes them compatible that should work fine. If you have a specific curve in mind, you could even write the glue code in bedrock2 and prove that it's correct.

The scmul_func bedrock2 function is proven against this spec in terms of group arithmetic:
https://github.com/mit-plv/fiat-crypto/blob/c86d501734e6645cd61b4514b9c2ce6cacf439b0/src/Bedrock/Specs/Group.v#L43

That proof is here (bedrock2's program_logic_goal_for_function creates a goal that says "if this function's callers obey their specs, then this function obeys its spec":
https://github.com/mit-plv/fiat-crypto/blob/c86d501734e6645cd61b4514b9c2ce6cacf439b0/src/Bedrock/Group/ScalarMult/ScalarMult.v#L225

Also, with respect to using function calls with Rupicola, is it necessary that the called functions are encoded as bedrock functions? Or would it be possible to reason about the correctness of code calling functions written in e.g. C or Coq?

There's an unverified print-as-C functionality for bedrock2:
https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ToCString.v
There's no formal model of C there, though, so it somewhat weakens the correctness guarantees. It can generate function calls, and your proofs will just have the precondition that the external functions you call obey their specifications.