Bas Spitters
Bas Spitters
As do CPP and ITP of course.
Related to: https://github.com/coq/platform/issues/61
Yes, we plan to maintain it for the long term. @haselwarter , @TheoWinterhalter and myself will be likely maintainers. Will create an opam package.
I haven't looked at coqutil closely enough, but how big is the overlap with stdpp. Some of the goals seem similar, at least wrt basic definitions, sets, maps. On Mon,...
We're using fiat with my PhD-students in https://github.com/AU-COBRA/AUCurves, which also depends on bedrock2.
Great. Thanks! So, it seems we may be able to just use bedrock2 for loops and function calls and avoid rupicola?
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?
@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...
This commit by @eorloff might solve this issue: https://github.com/eorloff/fiat-crypto
What is the current status of this issue? Has there been any progress in connecting bedrock to C semantics, such as CompCert/VST ?