Stream: fiat-crypto

Topic: Rupicola


view this post on Zulip Rasmus Holdsbjerg-Larsen (Dec 03 2020 at 13:28):

@Clément Pit-Claudel @Jade Philipoom @Benjamin Salling Hvass
We have had a look at the Rupicola project and have a few questions:
In order to learn about the compilation procedure, we attempted to compile a slightly more complicated variant of the swap function; which swaps the value of three cells:
https://github.com/RasmusHoldsbjergCSAU/rupicola/blob/master/src/Rupicola/Examples/Cells/swapthree.v
The compile tactic of Rupicola is not able to derive this function; although it is able to derive other simple functions, such as swap and increment.
Are we missing something that would allow the compile tactic to derive this function? 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 :grinning_face_with_smiling_eyes:

view this post on Zulip Bas Spitters (Dec 03 2020 at 13:42):

Incidentally, there is the nice rust backend for fiat-crypto. Is something similar planned for rupicola via bedrock2 ?

view this post on Zulip Clément Pit-Claudel (Dec 04 2020 at 13:39):

The compile tactic of Rupicola is not able to derive this function; although it is able to derive other simple functions, such as swap and increment.

You have two problems in that code: you overwrite c1 here:

        let/d c1 := put v1 c2 in
        let/d c2 := put v2 c3 in
        let/d c1 := put v3 c1 in

and you call swap instead of swapthree here:

            WeakestPrecondition.call
                (swapthree :: functions)
                "swap"

Here's the corrected snippet:

    Definition swapthree_gallina_spec (c1 c2 c3: cell) :=
        let/d v1 := get c1 in
        let/d v2 := get c2 in
        let/d v3 := get c3 in
        let/d c2 := put v1 c2 in
        let/d c3 := put v2 c3 in
        let/d c1 := put v3 c1 in
        (c1, c2, c3).

With these two fixes things almost work, but the compile tactic gets stuck on seps because it doesn't know that it should unfold it. It works if you replace seps with stars:

Definition ThreeCells a_ptr b_ptr c_ptr abc
  : list word -> Semantics.mem -> Prop :=
  fun _ =>
    (cell_value a_ptr (fst (fst abc)) * cell_value b_ptr (snd (fst abc)) * cell_value c_ptr (snd abc))%sep.

I'll get to the other questions later today :)

view this post on Zulip Rasmus Holdsbjerg-Larsen (Dec 04 2020 at 15:44):

Thanks, this works!
It seems to me that using seps and repeating "*" do similar things.
Would it be possible to make the compiler handle code using seps by unfolding at an appropriate point in the compilation process?
Or would it make more sense to avoid using seps altogether and stick with the "*" notation?

view this post on Zulip Clément Pit-Claudel (Dec 04 2020 at 16:06):

It makes complete sense to do that, and it's just a matter of adding an unfolding hint for seps. I thought that would work but in fact there's a "repeat" missing in compile around the call to "autounfold" in compile

view this post on Zulip Bas Spitters (Dec 08 2020 at 10:23):

@Clément Pit-Claudel in general, do you expect to need separation logic for cryptographic code, or would Hoare logic be enough.
We are (iniitally) mostly interested in adding loops and function calls to fiat-crypto.

view this post on Zulip Clément Pit-Claudel (Dec 10 2020 at 02:27):

Hmm! Depends on the primitive. For something like modular exponentiation, there's basically no separation logic involved. For something like a signing function, you'll want to be reasoning about buffers, which we do model using separation logic.

view this post on Zulip Bas Spitters (Dec 10 2020 at 09:19):

Thanks @Clément Pit-Claudel Do you have more insights into @Rasmus Holdsbjerg-Larsen other questions. We're excited to get started on rupicola.


Last updated: Feb 06 2023 at 05:03 UTC