Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives

Building

See here for details (remember to use --recursive when cloning, or to use git submodule update --init --recursive). Note that this fork currently requires Coq 8.15.0. To generate some of the larger files ulimit -s unlimited might be necessary. To test/benchmark the inversion files, see here