🚧 Under active development. CatCrypt is still evolving rapidly — APIs, module organization, and dependencies may change between releases.
The core of CatCrypt: machine-checked foundations for game-based cryptographic security proofs in Lean 4 — sub-distributions, a stateful-probabilistic program monad, probabilistic relational Hoare logic, state-separated packages, proof automation, forking lemmas, and Montgomery-curve mathematics.
📖 Documentation: hosted API reference · blueprint (dependency graph) · design & influences · The Joy of Cryptography in CatCrypt
This is the minimal-basis release. The universal-composability theory, concurrent UC, quantum verification, the verified compilation pipeline, and the full catalogue of concrete protocols live in separate, larger distributions.
Module names live under the CatCryptCore.* root (single entry point:
import CatCryptCore), so the library coexists with any package that has its
own CatCrypt.* module tree. Declared namespaces are CatCrypt.*:
open CatCrypt.Core, CatCrypt.Core.SPComp, etc. Paths in the table below
are relative to CatCryptCore/.
| Layer | Modules |
|---|---|
| Probability | Prob/* — sub-distributions, couplings, support, birthday bound, Schwartz–Zippel |
| Core | Core/* — typed heap (finite- and countable-typed locations), SPComp stateful-probabilistic monad, SPTree syntactic trees |
| Relational | Relational/* — pRHL judgment, sync/frame/reorder rules |
| Non-uniform | NonUniform/* — sampling from an arbitrary sub-distribution, conditioning, products, the unbounded while loop and its pHL / pRHL rules |
| Package | Package/* — interface-based package algebra |
| Category | Category/* — Kleisli of SPComp, family bicategory, cocartesian / affine structure |
| Graded WP kernel | XDijkstra/* — graded predicate transformers extending Std.Do with a grade, a frame rule, relational triples and transfer along monad morphisms; the xmvcgen tactics (guide) |
| Deep embedding | Deep/* — syntactic package calculus with semantic evaluation, SPComp → RawCode reflection |
| Bridge | Bridge/* — deep-to-shallow semantic bridge |
| Tactics | Tactics/* — pRHL automation (sync, invariant, WP/SP, ProofFrog, lazy sampling, remember/forget, triangle chaining, …) |
| Crypto foundation | Crypto/{Game,Advantage,SDist,SecurityDefs,Encryption,HybridArgument,NomAdvantage}.lean |
| Forking | Crypto/ForkingLemma.lean, Crypto/GeneralForkingLemma.lean — Pointcheval–Stern and Bellare–Neven |
| Up-to-bad | Crypto/BadEvent.lean — identical-until-bad / fundamental lemma of game-playing, bad-event union bounds, hybrid + up-to-bad, and lazy/eager sampling (Tactics/UpToBad.lean drives it) |
| Complexity | Crypto/{UCAdmClass,MonadCostModel,QueryBoundedUC,SizeBoundedUC,CTAdmClass,UCLevels,DummyAdversary,CompUCEquivalence,ConcreteReductions,RCL3,TraceRelating}.lean, Unary/ExpectedCost.lean — admissibility classes from query cost, total size and constant-time shape; the computational distance over admissible distinguishers and three levels of UC emulation; the dummy-adversary and constructive-cryptography equivalences at a bounded class; negligible functions; expected cost with the geometric-retry bound (guide) |
| Assumptions | Crypto/Assumptions/* — DDH, CDH, GapDH, DL, t-SDH, q-SDH, CoCDH, ODH, CR, OWF, PRP, RSA, AEAD, MAC |
| Curve math | Crypto/KeyAgreement/{MontgomeryLadder,MontgomeryAsWeierstrass,MontgomeryXOnly,Curve25519}.lean |
| Fujisaki–Okamoto | Crypto/PKE/{Games,FOTransformT}.lean, Crypto/KEM/{Games,FOTransformU,FOTransform,FIPS203KEM,FIPS203Security}.lean — PKE and KEM games, the T and U transforms with their classical reductions, the FIPS 203 KEM |
| Quantum foundations | Quantum/{Instrument,TraceNorm,UnitaryChannel,CPMap,Measurement,TensorProduct,KroneckerPSD,ChoiKraus,PartialTrace,Stinespring}.lean — instruments and channels on finite matrices, trace norm, completely positive maps, measurements, tensor products, positivity of Kronecker products, the Choi characterisation and Kraus form of completely positive maps, partial trace, Stinespring dilation and purification |
| Quantum distances | Crypto/UCMonad/{QuantumUC,DiamondNorm,DiamondNormStates,DiamondDominates,DiamondTensorStable,LocalOpFunctorial,QIndistDiamond}.lean, Quantum/{ClassicalEmbed,ClassicalLift,ClassicalDiamondLift,QRHL}.lean — the UCMonad instance of quantum instruments with the distinguishing distance qdist, the diamond norm qdistDiamond (a metric, above the CP-distinguisher distance, stable under local operations), the embedding of classical subdistributions with equality of the classical and quantum distances, and quantum relational Hoare logic |
| Quantum random oracles | Quantum/QROM/* — semi-classical one-way to hiding (O2HTheorem.o2h_semiclassical) and the search bound, quantum KEM games with classical decapsulation queries, normal form of adversaries, and the game hops of the Fujisaki–Okamoto proof with implicit rejection |
| ML-KEM | Crypto/MLKEM/* — the FIPS 203 specification over Z/3329Z with its NTT (Spec/, Crypto/Lattice/*), the module-LWE PKE, and IND-CCA security of ML-KEM-512 against quantum adversaries in the QROM, every term a proved number or a quantum module-LWE advantage of an explicit reduction (proof structure) |
See BUILDING.md for building the library and the documentation.
Pinned in lakefile.lean and lake-manifest.json; the toolchain is in lean-toolchain:
- Mathlib
- nominal-lean — the nominal-sets layer (
Nominal/)
- API reference: doc-gen4
- Blueprint: hosted blueprint and its
dependency graph (leanblueprint; sources in
blueprint/src/). It states the foundation layers and every worked scheme inCatCryptCore/Examples/, each statement linked to its Lean declaration in the API reference. - The Joy of Cryptography: JoyOfCrypto.md maps the chapters of
Rosulek's textbook to the worked schemes in
CatCryptCore/Examples/. - Graded weakest preconditions: CatCryptCore/XDijkstra/README.md
relates the kernel to
Std.Doandmvcgen;Demo.leanis the tutorial. - Design and influences: DESIGN.md · Changelog: CHANGELOG.md · Contributing: CONTRIBUTING.md
To build the manual, the API reference or the blueprint locally, see BUILDING.md.
The program logic, package algebra, and the ssprove_* tactic family port
the design of SSProve, the Coq/Rocq
framework for modular cryptographic proofs:
P. G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Abate, N. Sidorenco, C. Hriţcu, K. Maillard, B. Spitters. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ACM Transactions on Programming Languages and Systems 45(3), 2023. doi:10.1145/3594735
- hax-lean — a partially verified version of hax, a tool for high-assurance translation of a large subset of Rust into formal languages.
See CITATION.cff. The accompanying paper:
B. Spitters. CatCrypt: From Rust to Cryptographic Security in Lean. Cryptology ePrint Archive, Paper 2026/604. https://eprint.iacr.org/2026/604.pdf
MIT. See LICENSE.