mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
a413de56af
StrictE2EPQ/Profile.lean modelled a scheme-ID table no Go package declares: ML-DSA at 0x40/0x41/0x42, Pulsar at 0x50/0x51, an SLH-DSA-256s at 0x80. The production identity scheme, ML-DSA-65, is 0x42 and was labelled devnet-only; 0x52 is Pulsar-M-65, and the SLH-DSA family is 0x61-0x63, all f variants and on the wallet and contract-auth axes rather than the signature axis. A gate proof over those identifiers says nothing about the gate. Every enum now carries a `byte` function holding the value its Go constant table assigns, so the constants are checked by the build rather than asserted in a comment. luxStrictPQ_wire_bytes pins the eight production code points against config/profiles.go, luxStrictPQ_blocks_disjoint states the raw-ML-DSA / Pulsar-M block split ChainSecurityProfile.Validate requires, and sigSchemeID_byte_inj states that one byte names one scheme. Each enum, each predicate and each profile field cites the Go declaration it mirrors by line. Three consensus packages declare overlapping tables and they disagree. pkg/wire/candidate.go:346-352 gives Pulsar-M the 0x41/0x42/0x43 bytes config/pq_mode.go:303-305 gives raw ML-DSA, while candidate.go:342 requires the two to be identical; byte 0x10 is ContractAuthZChainProof, post-quantum, at config/pq_mode.go:868 and ContractAuthECDSASecp256k1Legacy, classical, at protocol/auth/scheme_ids.go:201. The model follows config and protocol/auth, records each divergence on the enum it affects, and where the two disagree about admissibility takes the intersection, so IsE2EPQ never admits a scheme either Go verifier refuses. Quasar/Consensus.lean defined AdvForge as "the three verification bits are true" and ignored its adversary argument. QuasarCert is a free record, so ⟨0,0,true,true,true,0,0⟩ satisfied it and quasar_triple_defense returned AdvBreak adv a for every adversary and every assumption. That refutes the hypotheses of single_assumption_prevents_forgery, assumption_independence and two_break_independence, which made all three vacuously true, and made quasar_triple_defense a way to mint the breaks it claims to require. Forgery is now relative to provenance. AdvProduced pairs "this adversary produced the certificate" with the EUF-CMA freshness condition, "no honest quorum did"; both predicates are opaque, because a forgery and an honestly finalized certificate carry identical fields and provenance is a protocol event rather than a function of them. The three unforgeability axioms take AdvProduced as a premise. protocol_correctness supplies the honest certificate, without which security over an empty set of valid certificates would say nothing. honest_cert_not_forgery and valid_cert_not_universally_forged state what the old definition denied, and forge_not_implied_by_validity proves that three set bits are not sufficient for AdvForge — so the definition cannot be weakened back to a predicate over the fields without failing to compile. The corpus: 760 theorems, 504 axioms, 0 sorry. vacuity.py is unchanged at 75; neither file contributes an entry. LLM.md's three headline numbers and the Quasar row were stale and are now measured. Co-authored-by: Hanzo Dev <[email protected]>
241 lines
9.8 KiB
Lean4
241 lines
9.8 KiB
Lean4
/-
|
|
LUX_STRICT_E2E_PQ Surface Coverage
|
|
|
|
Theorem: under a strict-PQ profile, every one of the 14 enumerated
|
|
surfaces is bound to a PQ primitive. This is the Lean 4 counterpart
|
|
to Theorem E2E-PQ-COVERAGE in
|
|
`~/work/lux/proofs/strict-e2e-pq/strict-e2e-pq-soundness.tex`.
|
|
|
|
The proof is by structural decomposition of `IsE2EPQ`: each field
|
|
fixes one surface; the conjunction of all fields fixes all surfaces.
|
|
|
|
Companion paper: ~/work/lux/papers/lp-stricte2epq/sections/01-intro.tex
|
|
-/
|
|
|
|
import StrictE2EPQ.Profile
|
|
import Mathlib.Tactic
|
|
|
|
namespace StrictE2EPQ
|
|
|
|
/-! ## Field projections from IsE2EPQ -/
|
|
|
|
/-- Project the 20 conjuncts of IsE2EPQ into named lemmas so downstream
|
|
proofs do not have to walk the conjunction tree by hand. Each lemma
|
|
extracts one bound from the conjunction. -/
|
|
|
|
lemma isE2EPQ_suite {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isStrictPQSuite p.hashSuiteID = true := h.1
|
|
|
|
lemma isE2EPQ_identity {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isPQScheme p.identitySchemeID = true := h.2.1
|
|
|
|
lemma isE2EPQ_finality {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isPQScheme p.finalitySchemeID = true := h.2.2.1
|
|
|
|
lemma isE2EPQ_highValue {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isPQScheme p.highValueSchemeID = true := h.2.2.2.1
|
|
|
|
lemma isE2EPQ_proofPolicy {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.proofPolicyID = .starkFRISHA3PQ := h.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_backends {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
∀ b ∈ p.allowedProofBackends, isStrictPQBackend b = true :=
|
|
h.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_soundnessBits {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.minSoundnessBits ≥ 128 := h.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_hashOutputBits {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.minHashOutputBits ≥ 384 := h.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_requireTransparent {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.requireTransparent = true := h.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidPairings {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidPairings = true := h.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidKZG {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidKZG = true := h.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidTrustedSetup {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidTrustedSetup = true := h.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidClassicalSNARKs {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidClassicalSNARKs = true := h.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidDevProofs {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidDevProofs = true := h.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_forbidFallbacks {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.forbidFallbacks = true := h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_requireTypedTxAuth {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
p.requireTypedTxAuth = true := h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_wallet {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isStrictPQWallet p.walletSchemeID = true := h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_contractAuth {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isStrictPQContractAuth p.contractAuthSchemeID = true :=
|
|
h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_bridge {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isStrictPQBridge p.bridgeProfileID = true :=
|
|
h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
|
|
|
|
lemma isE2EPQ_drbg {p : ChainSecurityProfile} (h : IsE2EPQ p) :
|
|
isStrictPQDRBG p.drbgSchemeID = true :=
|
|
h.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2
|
|
|
|
/-! ## The 14 surfaces, named -/
|
|
|
|
/-- The 14 surfaces over which strict-PQ claims coverage. Each constructor
|
|
names one surface; the proposition `SurfaceIsPQ` below states what
|
|
PQ-coverage means for that surface. -/
|
|
inductive Surface where
|
|
| profileBoot : Surface -- 1. ChainSecurityProfile loaded
|
|
| identityRegister : Surface -- 2. OpRegisterKey
|
|
| identityRotate : Surface -- 3. OpRotateKey
|
|
| identityRevoke : Surface -- 4. OpRevokeKey
|
|
| sessionAuth : Surface -- 5. OpAuthorizeSession
|
|
| txAuth : Surface -- 6. TxAuthEnvelope
|
|
| contractPermit : Surface -- 7. PQPermit
|
|
| zchainCommit : Surface -- 8. ZRegistryRoots
|
|
| execVerifyAuth : Surface -- 9. VerifyAuthPassed
|
|
| finalityBind : Surface -- 10. ComputeRoundDigest
|
|
| finalitySign : Surface -- 11. Pulsar
|
|
| proofVerify : Surface -- 12. p3q
|
|
| p2pTransport : Surface -- 13. ML-KEM + ML-DSA
|
|
| bridgeAdmit : Surface -- 14. BridgeProfile
|
|
deriving DecidableEq, Repr
|
|
|
|
/-- `SurfaceIsPQ p s` is the proposition that surface `s` is bound to a
|
|
PQ primitive under profile `p`. -/
|
|
def SurfaceIsPQ (p : ChainSecurityProfile) : Surface → Prop
|
|
| .profileBoot => isStrictPQSuite p.hashSuiteID = true
|
|
| .identityRegister => isPQScheme p.identitySchemeID = true
|
|
| .identityRotate => isPQScheme p.identitySchemeID = true
|
|
| .identityRevoke => isPQScheme p.identitySchemeID = true
|
|
| .sessionAuth => isPQScheme p.identitySchemeID = true
|
|
| .txAuth => isStrictPQWallet p.walletSchemeID = true
|
|
∧ p.requireTypedTxAuth = true
|
|
| .contractPermit => isStrictPQContractAuth p.contractAuthSchemeID = true
|
|
| .zchainCommit => isStrictPQSuite p.hashSuiteID = true
|
|
| .execVerifyAuth => isStrictPQSuite p.hashSuiteID = true
|
|
| .finalityBind => isStrictPQSuite p.hashSuiteID = true
|
|
| .finalitySign => isPQScheme p.finalitySchemeID = true
|
|
| .proofVerify => (∀ b ∈ p.allowedProofBackends, isStrictPQBackend b = true)
|
|
∧ p.forbidPairings = true
|
|
∧ p.forbidKZG = true
|
|
∧ p.forbidTrustedSetup = true
|
|
∧ p.forbidClassicalSNARKs = true
|
|
| .p2pTransport => isPQScheme p.identitySchemeID = true
|
|
∧ isStrictPQSuite p.hashSuiteID = true
|
|
| .bridgeAdmit => isStrictPQBridge p.bridgeProfileID = true
|
|
|
|
/-! ## The 14-path coverage theorem -/
|
|
|
|
/-- For a strict-PQ profile, every surface is PQ-bound. This is
|
|
Theorem E2E-PQ-COVERAGE from the soundness paper. -/
|
|
theorem coverage (p : ChainSecurityProfile) (hp : IsE2EPQ p) :
|
|
∀ s : Surface, SurfaceIsPQ p s := by
|
|
intro s
|
|
cases s
|
|
case profileBoot => exact isE2EPQ_suite hp
|
|
case identityRegister => exact isE2EPQ_identity hp
|
|
case identityRotate => exact isE2EPQ_identity hp
|
|
case identityRevoke => exact isE2EPQ_identity hp
|
|
case sessionAuth => exact isE2EPQ_identity hp
|
|
case txAuth => exact ⟨isE2EPQ_wallet hp, isE2EPQ_requireTypedTxAuth hp⟩
|
|
case contractPermit => exact isE2EPQ_contractAuth hp
|
|
case zchainCommit => exact isE2EPQ_suite hp
|
|
case execVerifyAuth => exact isE2EPQ_suite hp
|
|
case finalityBind => exact isE2EPQ_suite hp
|
|
case finalitySign => exact isE2EPQ_finality hp
|
|
case proofVerify => exact ⟨isE2EPQ_backends hp,
|
|
isE2EPQ_forbidPairings hp,
|
|
isE2EPQ_forbidKZG hp,
|
|
isE2EPQ_forbidTrustedSetup hp,
|
|
isE2EPQ_forbidClassicalSNARKs hp⟩
|
|
case p2pTransport => exact ⟨isE2EPQ_identity hp, isE2EPQ_suite hp⟩
|
|
case bridgeAdmit => exact isE2EPQ_bridge hp
|
|
|
|
/-! ## Bridge invariant: PQ E2E implies no classical admin -/
|
|
|
|
/-- A bridge profile state pairs the two booleans that this paper's
|
|
Section 11 constrains. -/
|
|
structure BridgeProfileState where
|
|
allowsClassicalAdmin : Bool
|
|
postQuantumEndToEnd : Bool
|
|
|
|
/-- The bridge invariant: PQ-E2E excludes classical admin. -/
|
|
def BridgeInvariant (b : BridgeProfileState) : Prop :=
|
|
b.postQuantumEndToEnd = true → b.allowsClassicalAdmin = false
|
|
|
|
/-- A bridge profile cannot simultaneously claim PostQuantumEndToEnd
|
|
and AllowsClassicalAdmin. -/
|
|
theorem bridge_pq_no_classical (b : BridgeProfileState)
|
|
(hp : b.postQuantumEndToEnd = true) (hc : b.allowsClassicalAdmin = true) :
|
|
¬ BridgeInvariant b := by
|
|
intro h
|
|
have := h hp
|
|
rw [hc] at this
|
|
exact Bool.noConfusion this
|
|
|
|
/-! ## Forbid* relaxation breaks IsE2EPQ -/
|
|
|
|
/-- Relaxing ForbidPairings to false breaks IsE2EPQ. -/
|
|
theorem relax_pairings_breaks (p : ChainSecurityProfile)
|
|
(_hp : IsE2EPQ p)
|
|
(q : ChainSecurityProfile)
|
|
(h_eq : q = { p with forbidPairings := false }) :
|
|
¬ IsE2EPQ q := by
|
|
intro hq
|
|
have hqf : q.forbidPairings = true := isE2EPQ_forbidPairings hq
|
|
rw [h_eq] at hqf
|
|
exact Bool.noConfusion hqf
|
|
|
|
/-- Relaxing ForbidKZG to false breaks IsE2EPQ. -/
|
|
theorem relax_kzg_breaks (p : ChainSecurityProfile)
|
|
(_hp : IsE2EPQ p)
|
|
(q : ChainSecurityProfile)
|
|
(h_eq : q = { p with forbidKZG := false }) :
|
|
¬ IsE2EPQ q := by
|
|
intro hq
|
|
have hqf : q.forbidKZG = true := isE2EPQ_forbidKZG hq
|
|
rw [h_eq] at hqf
|
|
exact Bool.noConfusion hqf
|
|
|
|
/-- Relaxing RequireTypedTxAuth to false breaks IsE2EPQ. -/
|
|
theorem relax_typed_tx_auth_breaks (p : ChainSecurityProfile)
|
|
(_hp : IsE2EPQ p)
|
|
(q : ChainSecurityProfile)
|
|
(h_eq : q = { p with requireTypedTxAuth := false }) :
|
|
¬ IsE2EPQ q := by
|
|
intro hq
|
|
have hqf : q.requireTypedTxAuth = true := isE2EPQ_requireTypedTxAuth hq
|
|
rw [h_eq] at hqf
|
|
exact Bool.noConfusion hqf
|
|
|
|
/-- Relaxing ForbidTrustedSetup to false breaks IsE2EPQ. -/
|
|
theorem relax_trusted_setup_breaks (p : ChainSecurityProfile)
|
|
(q : ChainSecurityProfile)
|
|
(h_eq : q = { p with forbidTrustedSetup := false }) :
|
|
¬ IsE2EPQ q := by
|
|
intro hq
|
|
have hqf : q.forbidTrustedSetup = true := isE2EPQ_forbidTrustedSetup hq
|
|
rw [h_eq] at hqf
|
|
exact Bool.noConfusion hqf
|
|
|
|
/-- Relaxing ForbidFallbacks to false breaks IsE2EPQ. -/
|
|
theorem relax_fallbacks_breaks (p : ChainSecurityProfile)
|
|
(q : ChainSecurityProfile)
|
|
(h_eq : q = { p with forbidFallbacks := false }) :
|
|
¬ IsE2EPQ q := by
|
|
intro hq
|
|
have hqf : q.forbidFallbacks = true := isE2EPQ_forbidFallbacks hq
|
|
rw [h_eq] at hqf
|
|
exact Bool.noConfusion hqf
|
|
|
|
end StrictE2EPQ
|