mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
ac9676a47a
The formal/lean library (53 files — a separate formalization from lean/) had ~110 type-check errors across 38 files and had never had its Mathlib oleans built. It now verifies at 0 errors under the project's strict setting: `lake env lean -D autoImplicit=false`, all 53 files. Fixed the same families as the sibling lean/ tree (the content is diverged, so each was repaired directly): - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE/Verkle): omega needs in-scope structure invariants; Nat-division bounds; noncomputable over opaque verifiers; Fin n index → Nat; deriving Inhabited. - DeFi (AMM/staking/fees/flashloan/HFT/router): constant-product invariant and fee bounds via Nat.div_mul_le_self / Nat.div_le_of_le_mul; dead tactics. - Protocol/Consensus/Warp/Bridge: BFT quorum theorems tightened to n=3f+1; pipe-projection parse fixes; split-after-simp; dead tactics; built the Consensus/Safety + ThresholdProof dependency oleans from clean source. - Network/Compute/Trust/Build: record-projection opacity (unfold+split), foldl-min monotonicity, BEq parse parens. - autoImplicit=false: declared previously auto-bound variables (explicit binders / variable blocks); the lakefile sets autoImplicit:=false. Integrity: no sorry/admit/native_decide; no proof-by-assumption axiom cheats. Statement changes only tightened false/trivial draft theorems to true invariants. Remaining axioms are trusted-base only (opaque crypto primitives, protocol modeling / honesty-static, build determinism). Co-authored-by: Hanzo Dev <[email protected]>
124 lines
4.1 KiB
Lean4
124 lines
4.1 KiB
Lean4
/-
|
|
Threshold Protocol Composition
|
|
|
|
Proves that the threshold protocols compose safely:
|
|
LSS → FROST (Schnorr threshold)
|
|
LSS → CMP (ECDSA threshold)
|
|
LSS → TFHE (FHE threshold decryption)
|
|
LSS → Corona (PQ threshold)
|
|
|
|
All share the same access structure (t-of-n).
|
|
Key shares from one protocol don't leak to another.
|
|
|
|
Maps to:
|
|
- lux/threshold/protocols/: all protocol implementations
|
|
- lux/mpc: MPC wallet using CMP
|
|
- lux/kms: key management using all protocols
|
|
|
|
Properties:
|
|
- Same access structure across all protocols
|
|
- Protocol independence: compromising FROST doesn't compromise CMP
|
|
- Composable security: UC-framework composition theorem
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Crypto.Threshold.Composition
|
|
|
|
/-- Protocol identifier -/
|
|
inductive Protocol where
|
|
| frost -- Schnorr threshold (Bitcoin, Taproot)
|
|
| cmp -- ECDSA threshold (Ethereum, EVM chains)
|
|
| tfhe -- FHE threshold decryption
|
|
| corona -- Post-quantum threshold (lattice-based)
|
|
| bls -- BLS threshold (validator consensus)
|
|
| lss -- Base: linear secret sharing
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- Unified threshold parameters (shared across protocols) -/
|
|
structure UnifiedParams where
|
|
t : Nat
|
|
n : Nat
|
|
ht : t ≤ n
|
|
ht0 : 0 < t
|
|
|
|
/-- A protocol instance bound to parameters -/
|
|
structure ProtocolInstance where
|
|
protocol : Protocol
|
|
params : UnifiedParams
|
|
|
|
/-- Key material is protocol-specific (no cross-contamination) -/
|
|
structure KeyMaterial where
|
|
protocol : Protocol
|
|
shareData : Nat
|
|
deriving DecidableEq
|
|
|
|
/-- Two protocol instances share the same access structure -/
|
|
def sameAccessStructure (a b : ProtocolInstance) : Prop :=
|
|
a.params.t = b.params.t ∧ a.params.n = b.params.n
|
|
|
|
/-- COMPOSITION: Same access structure across all protocols -/
|
|
theorem uniform_access_structure (p : UnifiedParams) (proto1 proto2 : Protocol) :
|
|
sameAccessStructure ⟨proto1, p⟩ ⟨proto2, p⟩ := by
|
|
simp [sameAccessStructure]
|
|
|
|
/-- INDEPENDENCE: Key material tagged with different protocols is distinct.
|
|
Because the `protocol` field is part of the structure, differing protocols
|
|
force the whole `KeyMaterial` records to differ (no cross-contamination). -/
|
|
theorem protocol_independence (k1 k2 : KeyMaterial)
|
|
(h : k1.protocol ≠ k2.protocol) :
|
|
k1 ≠ k2 := by
|
|
intro heq
|
|
exact h (by rw [heq])
|
|
|
|
/-- THRESHOLD CONSISTENCY: t-of-n is the same t across all protocols -/
|
|
theorem threshold_consistent (p : UnifiedParams)
|
|
(frost_t cmp_t tfhe_t : Nat)
|
|
(hf : frost_t = p.t) (hc : cmp_t = p.t) (ht : tfhe_t = p.t) :
|
|
frost_t = cmp_t ∧ cmp_t = tfhe_t := by
|
|
constructor <;> omega
|
|
|
|
/-- All protocols in the Lux stack -/
|
|
def luxProtocols : List Protocol :=
|
|
[.frost, .cmp, .tfhe, .corona, .bls, .lss]
|
|
|
|
theorem six_protocols : luxProtocols.length = 6 := rfl
|
|
|
|
/-- Multi-protocol key ceremony: generate shares for ALL protocols
|
|
in a single coordinated ceremony -/
|
|
def multiProtocolKeygen (p : UnifiedParams) : List ProtocolInstance :=
|
|
luxProtocols.map (⟨·, p⟩)
|
|
|
|
/-- All instances share parameters -/
|
|
theorem multi_keygen_uniform (p : UnifiedParams) (i j : Nat)
|
|
(hi : i < (multiProtocolKeygen p).length)
|
|
(hj : j < (multiProtocolKeygen p).length) :
|
|
sameAccessStructure
|
|
(multiProtocolKeygen p)[i]
|
|
(multiProtocolKeygen p)[j] := by
|
|
-- Every instance produced by the ceremony carries the SAME params `p`,
|
|
-- so list-indexing at any `i`/`j` yields `⟨_, p⟩`, whose params agree.
|
|
simp only [multiProtocolKeygen, sameAccessStructure, List.getElem_map]
|
|
exact ⟨trivial, trivial⟩
|
|
|
|
/-- Protocol ordering: LSS is the foundation, everything else builds on it -/
|
|
def dependsOn : Protocol → Protocol → Prop
|
|
| .frost, .lss => True
|
|
| .cmp, .lss => True
|
|
| .tfhe, .lss => True
|
|
| .corona, .lss => True
|
|
| .bls, .lss => True
|
|
| _, _ => False
|
|
|
|
/-- LSS has no dependencies (it's the base) -/
|
|
theorem lss_no_deps (p : Protocol) : ¬dependsOn .lss p := by
|
|
cases p <;> simp [dependsOn]
|
|
|
|
/-- Every non-LSS protocol depends on LSS -/
|
|
theorem all_depend_on_lss (p : Protocol) (h : p ≠ .lss) :
|
|
dependsOn p .lss := by
|
|
cases p <;> simp_all [dependsOn]
|
|
|
|
end Crypto.Threshold.Composition
|