Rasmus Holdsbjerg-Larsen
Rasmus Holdsbjerg-Larsen
I am currently attempting to use Bedrock2 for cryptographic applications that use field arithmetic generated by Fiat Crypto. I am however having a bit of trouble with the ecancel_assumption tactic....
Opening a pull request for the changes suggested in #1215
Continuing on the discussion here #1150 I have made modifications to the Bedrock2 specs for field operations that allow for arbitrary finite fields, as opposed to the current versions that...
I asked about this here: #1113 , but am not sure if anyone has seen it. The question is about the specs for Bedrock2 field operations in ```Bedrock/Specs/Field.v```. Currently these...
Lately, I have been trying to use Bedrock2 functions for implementing elliptic curves. We have worked out a simple example illustrating the functionality of the Bedrock2 framework that is needed...
I noticed that the Bedrock2 synthesis pipeline generates Bedrock2 functions that do not make use of return values, a functionality that is supported by Bedrock2 as far as I can...
We have been using the Fiat Crypto framework for developing verified and efficient implementations of quadratic field extensions to be used for curves such as FourQ and BLS-12. The project...
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...
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...
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...