zkir-crypto

Formally verified cryptographic circuits for Plonky3. The idea is to write gadget specifications in Coq, prove them correct, and extract working Rust code that integrates with the Plonky3 STARK prover.

What this is

A library of AIR (Algebraic Intermediate Representation) circuits for common cryptographic primitives. The gadgets are specified and verified in Coq/Rocq, then extracted to Rust code targeting Plonky3. All gadgets work over the Mersenne-31 field.

Building

Prerequisites:

• Coq 8.19+
• Rust 1.75+

make coq      # build proofs
make generate # extract Rust from Coq
make rust     # build Rust library
make test     # run tests

Or just make to build everything.

Project layout

coq/
  theories/
    Field/          - Mersenne-31 arithmetic
    Foundations/    - shared definitions (vectors, bit vectors, SHA256 state)
    DSL/            - constraint/witness DSL (CExpr, WExpr, Gadget, Composition)
    Reflection/     - proof automation tactics
    Gadgets/        - verified gadget implementations
    LookupTables/   - lookup table infrastructure
    Synthesis/      - Coq to Rust pretty-printing
rust/
  src/
    generated/      - extracted Rust code (don't edit by hand)
    gadgets/        - gadget implementations for witness generation
    crypto_chip/    - crypto chip infrastructure
    tests/          - test suite
scripts/
  generate_all.py   - extraction script

How extraction works

The Coq code includes a pretty-printer that converts gadget definitions to Rust strings. Running make generate evaluates these in Coq and writes the output to rust/src/generated/. The generated code implements Plonky3's Air trait.

See scripts/generate_all.py for the list of extracted gadgets.

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.