package coq-fiat-crypto

  1. Overview
  2. No Docs
Cryptographic Primitive Code Generation by Fiat

Install

Dune Dependency

github.com Edit opam file Versions (7)

Authors

  1. A
    Andres Erbsen <andreser@mit.edu>
  2. G
    Google Inc.
  3. J
    Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com>
  4. M
    Massachusetts Institute of Technology
  5. Z
    Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>

Maintainers

  1. J
    Jason Gross <jgross@mit.edu>

Sources

v0.0.17.tar.gz
sha512=c7688c84fcc10cc063cff24d5d3d52edd04f26b16adb00e7389d648964e2a0cc0d81fa615d9091e491edd6fed81859f1ea4a12e19ba6793975be2b301369778a

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.

Tags

logpath:Crypto

Published: 17 Oct 2022

Dependencies (8)

  1. coq-bedrock2-compiler = "0.0.4"
  2. coq-rupicola = "0.0.6"
  3. coq-rewriter >= "0.0.6" & <= "0.0.7"
  4. coq-coqprime >= "1.2.0"
  5. coq >= "8.15~"
  6. ocamlfind build
  7. ocaml build & >= "4.08~"
  8. conf-findutils build

Dev Dependencies

None

Used by

None

Conflicts

None