package coq-fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.6.tar.gz
sha512=187f30e4bbb53636cd261e50ae1856a15cb9820b59b1a126ff0791567d896a29b6c93eb93dbf9cd1af5cae6c47723cedc8dfa175769eebb9cf363e27e5decbe6
Description
Coq code and proofs for a command-line binary that can synthesize proven-correct big-integer modular field arithmetic operations for cryptography. Target languages include C, Rust, Zig, Go, and bedrock2.
Dependencies (8)
-
coq-bedrock2-compiler
= "0.0.9" -
coq-rupicola
= "0.0.11" -
coq-rewriter
>= "0.0.12" -
coq-coqprime
>= "1.6.0" -
coq
>= "9.0~" -
ocamlfind
build -
ocaml
build & >= "4.08~" -
conf-findutils
build
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page