package coq-fiat-crypto
Cryptographic Primitive Code Generation by Fiat
Install
Dune Dependency
Authors
Maintainers
Sources
v0.1.3.tar.gz
sha512=7debd66c43908acd07d5b647965ff344571e22397814b29aaf19141fb9cc23ff4a04471c0c199179a7589c2bf89eff72e277508004c9005cd025de40a444a265
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.8" -
coq-rupicola
= "0.0.10" -
coq-rewriter
>= "0.0.6" -
coq-coqprime
>= "1.2.0" -
coq
>= "8.18~" -
ocamlfind
build -
ocaml
build & >= "4.08~" -
conf-findutils
build
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page