CatCrypt Core
🚧 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/.
Contents
| 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,DiamondEmulation,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 qdist and the CP-distinguisher distance, stable under local operations); diamond-distance emulation QUCEmulatesDiamond is a preorder with additive error, preserved by sequential composition on either side and by tensoring with a fixed instrument, and gives UCEmulates with the adversary as simulator; the embedding of classical subdistributions with equality of the classical and quantum distances, and quantum relational Hoare logic |
| Quantum systems and quantum UC | Quantum/{SubInstrumentOrder,QSysCat,QSysCatTensor,QSysCatPrivate,QSysCatOpenTheory,ClassicalLiftSys,ClassicalLiftFunctor,QRealizes,QRealizesMem,QOTPReactive,QOTPInsecure}.lean, Crypto/{OpenTheoryObs,UCTransport}.lean — Selinger's order on subinstruments, an ω-complete partial order in which sequencing is ω-continuous; the traced symmetric monoidal category of quantum reactive systems (⊕ traced by the ω-supremum of the feedback runs, ⊗ of registers by framing), its variant with registers private to morphisms, and its Int construction as an open theory with quantum emulation closed under composition; the classical lift of reactive systems as a traced braided monoidal functor, with statistical transport of realization bounds; transport of realization along observation-preserving maps; realization of quantum reactive systems with simulators holding quantum registers, and the quantum one-time pad realizing the secure quantum channel and, over an insecure channel, the confidential channel with Pauli tampering (guide) |
| Party language | Crypto/Party/* — classical and quantum party programs in do notation, denoted as reactive systems; parallel composition and loops agree with the Int construction on systems; the category of wiring diagrams with a faithful traced monoidal denotation functor; subroutine calls as multi-call hybrids; qubit ports with linear ownership; port typing, opacity, a relational program logic, refinement, time certificates and quantum weakest preconditions derived from programs (party_derive); F_AKE, X3DH and PQXDH as programs (guide) |
| Quantum random oracles | Quantum/QROM/* — semi-classical one-way to hiding for every mixed initial state (O2HTheorem.o2h_semiclassical_mixed) and for multi-round adversaries whose local operations are arbitrary completely positive trace-preserving maps (O2HGeneral.o2h_semiclassical_gen, through a unitary dilation that keeps the acceptance probability), completely positive instruments (Quantum/CPInstrument), measure-and-reprogram for a single reprogrammed point (MeasureReprogram.measure_reprogram), Zhandry's compressed oracle with equality of output probabilities against the standard oracle and at most q database entries after q queries (CompressedOracle.prOut_compressed_eq, CompressedOracleLocal.runCmp_database_le), 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) |
Build
See BUILDING.md for building the library and the documentation.
Dependencies
Pinned in lakefile.lean and lake-manifest.json; the toolchain is in lean-toolchain:
- Mathlib
- nominal-lean — the nominal-sets layer (
Nominal/)
Documentation
- 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. - Proof automation: CatCryptCore/Tactics/README.md
documents
catcrypt_autoandcatcrypt_auto?, their goal shapes and arms, and how a library registers shapes and arms for its own goals, with the VCVio registrations as the worked example. - 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.
Relation to SSProve
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
Related projects
- hax-lean — a partially verified version of hax, a tool for high-assurance translation of a large subset of Rust into formal languages.
Citing
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
License
MIT. See LICENSE.