Lean proof browser
24 modules, 460 public declarations from lean/PqStealth/*.lean, one page per module. Every page shows each declaration's docstring, statement, axiom badge, a collapsible tactic proof and a GitHub permalink. Inline theorem names anywhere on this site link here.
| Module | Declarations | Axioms | Summary |
|---|---|---|---|
| AnonymityFromSPR | 4 | sorry-free ✓ | Proved: anonymity is bounded by the two per-branch SPR advantages -- hop through a game whose challenge ciphertext comes from a key-independent simulator … |
| Blinding | 4 | sorry-free ✓ | Proved: A·s' + e' + (A·s₁ + s₂) = A·(s₁ + s') + (s₂ + e') over any commutative ring -- the sender's published value is the honest ML-DSA public key of the … |
| BlindingEntropy | 15 | sorry-free ✓ | BlindingROM reduced the blinding term to the two bad-query probabilities. |
| BlindingROM | 20 | sorry-free ✓ | Proved: hashAddr ∘ pack as VCVio's lazily sampled randomOracle over unifSpec + (Bytes →ₒ Addr); the fresh-query lemma (from the empty cache the announced … |
| ConstructionA | 20 | sorry-free ✓ | Proved: the auxGen the real scheme uses -- view tag plus hashAddr (pack rho (power2Round (A *ᵥ s' + e' + t))), symmetric primitives bundled uninterpreted … |
| ConstructionASecurity | 2 | sorry-free ✓ | |
| Controls | 17 | sorry-free ✓ | Proved, all as ordinary theorems so the build keeps them honest: a scheme whose announcement IS the recipient's meta-address attains the maximal unlinkability … |
| DKSAP | 21 | sorry-free ✓ | Proved: DKSAP (ERC-5564 scheme 1, the only stealth scheme deployed today) as a StealthScheme, and its detection completeness; given the discrete logs of the … |
| DKSAPOracle | 38 | sorry-free ✓ | Proved: the key-recovery attack as an OracleComp (unifSpec + (G →ₒ F)) making EXACTLY two oracle queries whatever the number of announcements it is handed … |
| Demo | 19 | — | Everything else here is abstract, which is what makes the theorems apply to any curve and also what makes nothing executable. |
| Games | 14 | sorry-free ✓ | Proved: StealthScheme as an abstract randomized algorithm over VCVio's ProbComp (mirroring its own AsymmEncAlg idiom); detection completeness and the … |
| Invariants | 25 | sorry-free ✓ | Proved: centered-norm sub-additivity, hence the blinded secret is 2·eta-short and the signer bound doubles (beta' = tau·(2·eta) = 2·beta); the ownership … |
| KEMAnonymity | 20 | sorry-free ✓ | Proved: KEM (VCVio's KEMScheme over ProbComp) and its anonymity game -- key privacy, which VCVio does not ship; ofKEM, whose unlinkability EQUALS the … |
| MLKEM | 21 | sorry-free ✓ | Proved: the three DecidableEq instances VCVio's concrete encoding lacks (it sets all encoded types to ByteArray but as a plain def); that the concrete … |
| MultiRecipient | 19 | sorry-free ✓ | Proved: the n-recipient left-or-right game — n independently generated meta-addresses, the adversary NAMES the challenge pair after seeing all of them and … |
| MultiUnlink | 20 | sorry-free ✓ | Proved: the q-challenge left-or-right unlinkability game against two recipients (UnlinkExpMulti), and the hybrid bound `unlinkAdvantageMulti ≤ ∑ k ∈ range … |
| Ownership | 26 | sorry-free ✓ | Proved: spend forgery -- producing a short (s, e) with A *ᵥ s + e = t for a target you were not given -- cast as a VCVio SIS.Problem, with the honest … |
| ROMUpToBad | 24 | sorry-free ✓ | VCVio's tvDist_simulateQ_randomOracle_withProgramming_le_probEvent_bad bounds the distance between a lazily sampled random oracle and a programmed one (the … |
| Reorder | 5 | sorry-free ✓ | OracleComp's bind is syntactic, so two games that draw the same independent samples in different orders are not equal on the nose; they are equal under … |
| SPRTwoHop | 44 | sorry-free ✓ | Proved: the two decision-MLWE problems the SPR argument needs, both as VCVio LearningWithErrors.Problems over the seed rho; the two reduction adversaries … |
| SharedSecretHiding | 10 | sorry-free ✓ | Proved: each shared-secret-hiding term of unlinkAdvantage_ofKEMFull_le is the bias of a real-or-random guessing game, and that bias EQUALS … |
| Soundness | 21 | sorry-free ✓ | Proved: DKSAP's false-positive rate is EXACTLY 1 / |F|, for every hash h -- the leak is the uniform spending scalar, not a hash collision; and for the … |
| SpendSecurity | 23 | sorry-free ✓ | A recipient's stealth keys are all derived from one master ML-DSA key (A, t = A·s₁ + s₂): announcement i contributes a blinding offset (s'ᵢ, e'ᵢ) and the … |
| WidenedSigning | 28 | — | The standard ML-DSA identification scheme rejects when ‖z‖∞ < γ₁ - β and ‖r₀‖∞ < γ₂ - β, where β = τ·η bounds ‖c·s‖∞ for an η-short s. |