Targeting bedrock2

[RasmusHoldsbjergCSAU]

I can see in the documentation that fiat is supposed to target bedrock2, and that this output is converted to C.

How is this conversion done, and is it possible to not convert to C, and instead generate bedrock2 functions? @JasonGross @jadephilipoom @andres-erbsen

[JasonGross]

The conversion is done at https://github.com/mit-plv/fiat-crypto/blob/7b250931d9ec98a45f365b505f037f8a810a60f7/src/Bedrock/Field/Stringification/Stringification.v#L147-L220. The conversion to bedrock2 functions is at https://github.com/mit-plv/fiat-crypto/blob/7b250931d9ec98a45f365b505f037f8a810a60f7/src/Bedrock/Field/Translation/Func.v#L43-L87 There are examples in https://github.com/mit-plv/fiat-crypto/blob/master/src/Bedrock/Field/Synthesis/Examples/ of generating bedrock2 functions.

The translation to C uses a slightly modified version of https://github.com/mit-plv/bedrock2/blob/13365e8113131601a60dd6b6ffddc5a0b92aed58/bedrock2/src/bedrock2/ToCString.v#L147-L169

[spitters]

Great. Thanks! So, it seems we may be able to just use bedrock2 for loops and function calls and avoid rupicola?

[JasonGross]

I'll let @samuelgruetter @andres-erbsen @jadephilipoom comment on the viability of writing and proving loops and function calls directly in bedrock2 for crypto algorithms. Definitely possible in theory, though, and I think rupicola also targets bedrock2.

[jadephilipoom]

Yes, it should be possible to use bedrock2 directly, although the proofs might be trickier because you have to reason about both the algorithm and details of its representation at the same time.

[spitters]

Concretely for field inversion, we only need to iterate divstep a fixed number of times. Would that become hard because of the synthesized optimized implementation?

[andres-erbsen]

If I wanted to verify euclidian inversion, I would do exactly what you are suggesting. bedrock2 and the fiat-bedrock2 connection are far from polished, but there isn't a fundamental obstacle.

[spitters]

@RasmusHoldsbjergCSAU has been having some success with this. Stepping back, is this a good general division of concerns: straightline code in fiat-crypto, more complex code (loop, function calls, ...) in bedrock2 ?

[andres-erbsen]

Yes, this is a reasonable division of work between tools. It is currently practically enforced by the fact that the fiat-crypo toolchain can only generate starightline code. More philosphically, I am not aware of any non-straightline code where fiat-crypto-style partial evaluation would offer great benefit, instead I think controlling details like memory management is often important in higher-level functions (and this is best done in bedrock2).

Some of us are currently experimenting with rule-based synthesis of bedrock2 code from specifically-structured gallina code (the Rupicola project), but it is far from superseding writing and verifying bedrock2 code.