mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
d3bff5e2dc
The lean/ proof library (88 files) had ~180 type-check errors across ~45 files plus 31 proof-by-assumption axiom cheats. It now type-checks cleanly under Lean 4.14.0 + Mathlib, with every theorem genuinely proven from definitions. Errors fixed: - Stale Mathlib imports: Data.Nat.Basic / Data.Int.Basic were removed this rev -> Data.Nat.Defs / Data.Int.Defs (57 files). - Shared AI/Agent/Governance/Contract/DeFi/Ecology draft files: same proof-rot as the zoo-labs sibling library (now reconciled): omega missing in-scope bounds, dead tactics after simp, simp over-reduction, doc-comment placement, reserved-word binders, deriving Repr on Finset-bearing structs, noncomputable defs over opaque primitives. - Consensus/Liveness: collapsed a 74-error cascade (undefined shared state model inlined from Safety.lean; the |>. pipe-projection vs comparison parse trap on 14 lines rewritten to explicit dot projection). - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE), Consensus, Protocol, Warp, Trust, GPU, Compute, Network, DeFi: brought structure invariants into scope for omega, Nat-division bounds via Nat.div_le_of_le_mul / Nat.div_mul_le_self, noncomputable over opaque crypto ops, deriving Inhabited for index access. Integrity: - Removed all 31 `theorem X := X_ax` cheats (axiom asserting the identical statement) and proved each from definitions; removed the UNSOUND content_addressed axiom (hash-injectivity over a struct with free fields). - Quorum-intersection theorems (BFT/Quasar/Flare/Warp/BLS/GPU/Bridge): the draft hypothesis 3f<n is insufficient (n unbounded above makes them false); tightened to the optimal-resilience invariant n=3f+1 / 2t>n. Statement intent preserved. - Net axiom change: -35 / +1 (the one addition, honesty_static, is a fixed-validator-set modeling assumption matching sibling files). - Remaining axioms are trusted-base only: opaque crypto primitives (groups, pairings, hardness, hashes, FHE encrypt/decrypt, BLS soundness, forward secrecy, Fisher-Yates uniformity) and protocol modeling assumptions. No sorry/admit/native_decide. Verified all theorems trace to [propext, Classical.choice, Quot.sound] plus those primitives. Co-authored-by: Hanzo Dev <[email protected]>
111 lines
3.2 KiB
Lean4
111 lines
3.2 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zach Kelling
|
||
|
||
ML-KEM (FIPS 203) Key Encapsulation Correctness
|
||
|
||
Post-quantum key encapsulation mechanism. Used for key exchange
|
||
in the hybrid handshake protocol.
|
||
|
||
Based on CRYSTALS-Kyber (Module-LWE).
|
||
|
||
Maps to:
|
||
- luxfi/crypto: mlkem package
|
||
- lux/node: post-quantum key exchange in SSP handshake
|
||
- Quasar consensus: quantum-safe channel establishment
|
||
|
||
Properties:
|
||
- Correctness: decaps(encaps(pk)) recovers the shared secret
|
||
- IND-CCA2 security under Module-LWE
|
||
- Key sizes by security level
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Crypto.MLKEM
|
||
|
||
/-- ML-KEM security levels (FIPS 203) -/
|
||
inductive SecurityLevel where
|
||
| mlkem512 -- NIST Level 1 (128-bit)
|
||
| mlkem768 -- NIST Level 3 (192-bit) ← default for Lux
|
||
| mlkem1024 -- NIST Level 5 (256-bit)
|
||
deriving DecidableEq, Repr
|
||
|
||
/-- Public key sizes (bytes) -/
|
||
def pkSize : SecurityLevel → Nat
|
||
| .mlkem512 => 800
|
||
| .mlkem768 => 1184
|
||
| .mlkem1024 => 1568
|
||
|
||
/-- Secret key sizes (bytes) -/
|
||
def skSize : SecurityLevel → Nat
|
||
| .mlkem512 => 1632
|
||
| .mlkem768 => 2400
|
||
| .mlkem1024 => 3168
|
||
|
||
/-- Ciphertext sizes (bytes) -/
|
||
def ctSize : SecurityLevel → Nat
|
||
| .mlkem512 => 768
|
||
| .mlkem768 => 1088
|
||
| .mlkem1024 => 1568
|
||
|
||
/-- Shared secret size (always 32 bytes) -/
|
||
def ssSize : SecurityLevel → Nat
|
||
| _ => 32
|
||
|
||
/-- Key generation -/
|
||
axiom keygen : SecurityLevel → Nat × Nat -- (pk, sk)
|
||
|
||
/-- Encapsulation: pk → (ct, ss) -/
|
||
axiom encaps : SecurityLevel → Nat → Nat × Nat
|
||
|
||
/-- Decapsulation: sk → ct → ss -/
|
||
axiom decaps : SecurityLevel → Nat → Nat → Nat
|
||
|
||
/-- Correctness: decaps(sk, encaps(pk).ct) = encaps(pk).ss
|
||
for matching (pk, sk) keypair -/
|
||
axiom mlkem_correctness :
|
||
∀ (level : SecurityLevel),
|
||
let (pk, sk) := keygen level
|
||
let (ct, ss) := encaps level pk
|
||
decaps level sk ct = ss
|
||
|
||
/-- IND-CCA2 security: ciphertexts are indistinguishable
|
||
under Module-LWE hardness assumption -/
|
||
axiom mlkem_ind_cca2 :
|
||
∀ (level : SecurityLevel) (pk : Nat) (ss0 ss1 : Nat),
|
||
-- No PPT/quantum adversary can distinguish encapsulations
|
||
-- of ss0 vs ss1 with non-negligible advantage
|
||
True
|
||
|
||
/-- Shared secret is always 32 bytes -/
|
||
theorem ss_fixed_size (level : SecurityLevel) : ssSize level = 32 := by
|
||
cases level <;> rfl
|
||
|
||
/-- ML-KEM-768 is the default for Lux (NIST Level 3) -/
|
||
theorem default_level_3 : pkSize .mlkem768 = 1184 := rfl
|
||
|
||
/-- Key sizes grow with security level -/
|
||
theorem pk_monotone_512_768 : pkSize .mlkem512 < pkSize .mlkem768 := by
|
||
simp [pkSize]
|
||
|
||
theorem pk_monotone_768_1024 : pkSize .mlkem768 < pkSize .mlkem1024 := by
|
||
simp [pkSize]
|
||
|
||
/-- Ciphertext size is bounded -/
|
||
theorem ct_bounded (level : SecurityLevel) : ctSize level ≤ 1568 := by
|
||
cases level <;> simp [ctSize]
|
||
|
||
/-- Combined hybrid KEM: ML-KEM + X25519 for belt-and-suspenders -/
|
||
axiom hybrid_kem_ss : SecurityLevel → Nat → Nat → Nat
|
||
|
||
/-- Hybrid KEM: shared secret combines both KEMs -/
|
||
axiom hybrid_kem_combines_both :
|
||
∀ (level : SecurityLevel) (mlkem_ss x25519_ss : Nat),
|
||
-- The hybrid shared secret is derived from BOTH components
|
||
-- Breaking requires breaking BOTH ML-KEM AND X25519
|
||
hybrid_kem_ss level mlkem_ss x25519_ss ≠ mlkem_ss ∨
|
||
hybrid_kem_ss level mlkem_ss x25519_ss ≠ x25519_ss
|
||
|
||
end Crypto.MLKEM
|