Lean evidence and supporting research
The Lean development contains generic KEM/announcement results, Construction A address and spending research, classical controls, and proof infrastructure. The ERC now focuses on key exchange (D-024). Start with the ERC evidence map; reviewing the ERC does not require reading the entire development or building Lean.
Reading paths
- Key exchange: security overview →
GamesandKEMAnonymity→SharedSecretHiding→AnonymityFromSPR→MLKEMandSPRTwoHop. AddMultiUnlink,MultiRecipient, and the KEM portion ofSoundnessfor the corresponding claim. The commitment-format roundtrip is inInvariants. - Construction A address form: reference →
Blinding,Invariants,ConstructionA,BlindingROM,BlindingEntropy. - Spending: Construction A security
→
Ownership,WidenedSigning,SpendSecurity,ConstructionASecurity. - Classical comparison:
Demo,DKSAP,DKSAPOracle. - Maintaining proofs: the build section below, pin policy, upstream notes, and tooling guide.
What is established, and what is not
The generic full-announcement model decomposes unlinkability into shared-secret
hiding, auxiliary-data independence, and KEM anonymity. SharedSecretHiding
identifies its hiding terms with KEM IND-CPA advantages. AnonymityFromSPR
and SPRTwoHop structure the anonymity reduction with seeded-MLWE terms and
named primitive/encoding assumptions. These are conditional statements.
Construction A instantiates the auxiliary data with a blinded ML-DSA address.
Its ROM query bound is proved in BlindingROM/BlindingEntropy. That proof
is about Construction A, not the D-024 commitment/CREATE2 derivation. The latter
has an abstract encoding roundtrip and executable vectors, but no dedicated
end-to-end privacy capstone in this tree.
The related-key spend reduction proves a bound for ownership witnesses.
It is not signature EUF-CMA security. Signature-layer losses remain uncomposed;
the widened HVZK bound is the trivial 1. Active ANO-CCA mapping to FIPS-203
ML-KEM, quantum random-oracle access, and runtime side channels are not supplied
by these results. See the separate security documents above.
Complete module map
All modules below live in PqStealth/. Categories describe the mathematics, not isolated build targets.
| Track | Modules | Role |
|---|---|---|
| Announcement model | Games, KEMAnonymity | Scheme experiments, KEM anonymity, full auxiliary-data model and completeness |
| KEM reductions | SharedSecretHiding, AnonymityFromSPR, MLKEM, SPRTwoHop | Hiding/IND-CPA bridge, SPR route, concrete ML-KEM types, conditional seeded-MLWE decomposition |
| Multiple challenges | MultiUnlink, MultiRecipient | Generic hybrid bounds |
| Detection | Soundness | Conditional KEM false-positive bounds and classical comparison |
| Mixed encoding/algebra | Invariants | Both meta-address roundtrips plus ML-DSA norm/signing-key results |
| Construction A derivation | Blinding, ConstructionA, BlindingROM, BlindingEntropy | Blinded-key identity, announcement instantiation, address-hash query and entropy bounds |
| Construction A spending | Ownership, WidenedSigning, SpendSecurity | Ownership/SIS relation, widened signing facts, related-key witness reduction |
| Construction A assembly | ConstructionASecurity | Re-exports/combines address and spending statements; not a commitment-profile capstone |
| Classical research | DKSAP, DKSAPOracle, Demo | Classical scheme, attack/reduction models, runnable toy example |
| Proof support | Reorder, ROMUpToBad, Controls | Sampling identities, random-oracle machinery, positive/negative controls |
| Audit | Axioms | Frozen axiom lists for selected headline declarations |
Games still imports Blinding; Invariants mixes encodings and ML-DSA;
Soundness imports DKSAP. The root and audit import all tracks. This
refactor separates documentation, not the compilation graph. No spending
proofs or audit guards have been removed.
Build and verification for maintainers
From lean/, using the pinned Lean 4.32.0 / VCVio revision in
lakefile.toml and lean-toolchain:
lake exe cache get
lake build
python3 scripts/check_citations.py
python3 scripts/check_sizes.pyVCVio compiles from source; a cold build can take hours. Do not update the pin as part of routine documentation work. The pin guide documents the reviewed upgrade procedure.
Axioms.lean uses #guard_msgs around #print axioms to freeze selected
headline dependency cones; an unexpected sorryAx or other axiom changes the
output and fails the guard. CI additionally rejects package warnings/sorries.
This checks proof dependencies, not whether hypotheses are true, non-vacuous,
or applicable to application code. Demo.lean guards toy evaluation output.
The citation script checks supported source-range citations; the size script checks selected Construction A/classical vector sizes. It does not currently read commitment vectors. Python/TS commitment replay is separate evidence. The Lean CI workflow runs the build, warning check, and both scripts. Build status must be read from an actual run; these instructions are not a fresh full-build claim.