mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
de9a19550c
Zero modules are now in no library, down from ten. The seven with content are rooted — Corona's Unforgeability, Shamir and OutputInterchange, Magnetar's Unforgeability and OutputInterchange, Precompile.P3Q, Compute.AIMint — so CI type-checks them and the axiom and vacuity reports cover them for the first time. Deleted three artifacts that described things that do not exist: `pulsar/hash-suite-separation.tex` proved a separation theorem about a selectable Pulsar-SHA3 / Pulsar-BLAKE3 hash suite. `HashSuiteID` and `BLAKE3` appear nowhere in `pulsar/pkg/pulsar`, and pulsar's own DD-002 records the decision as "No BLAKE3", rationale "BLAKE3 is not on the list. Including BLAKE3 in the NIST submission profile is a strategic liability." The theorem's premise is counterfactual. `lean/Crypto/Pulsar/dkg2.lean` carried Corona's parameters — q = 0x1000000004A01, M=8, N=7, sigma_E 6.108, the `corona.dkg2.*` domain tags — under a Pulsar namespace, calling them "Pulsar production" and "Pulsar canonical ring". Pulsar's ring is pulsar-mldsa65-fips204, K=6, L=5, q = 8380417. Seven of its sixteen declarations stated `True`, including `mlwe_b_hard` and `msis_ab_hard`, so the Pedersen hiding and binding theorems reduced to nothing. It cited `pulsar/dkg2/dkg2.go`, which does not exist. `lean/Crypto/Corona/dkg2.lean` modelled `luxfi/corona/dkg2/dkg2.go`, a package deleted from corona at `2cecc08` and absent at HEAD. `Crypto/CGGMP21.lean` and `Crypto/Threshold/CGGMP21.lean` both opened `namespace Crypto.Threshold.CGGMP21`, so rooting the first broke the import of the second. The orphan at the shorter path was the larger file and a strict superset — five extra results on Paillier homomorphism, Lagrange and Shamir evaluation. Consolidated into the rooted path; one file per namespace. `Main.lean` stated four conjuncts, of which `spreadBps * volumeUSD / 10000 >= 0` holds of every `Nat` and the fourth was `True`. Its header said "if this file compiles, the following hold: consensus is safe and live under BFT assumptions" across ten libraries, while it imported only Mathlib — no consensus module, no crypto module. It now imports Consensus.BFT and its conjuncts ARE `quorum_intersection` and `honest_majority_sufficient`, applied rather than restated, so compilation depends on those proofs. Safety, liveness and post-quantum hardness are named as deliberately absent, with the reason. Measured after: 750 theorems queried, 620 proved outright against Lean's ambient logic, 130 resting on axioms; 62 declarations carry no content, down from 75; 0 `sorry`. Co-authored-by: Hanzo Dev <[email protected]>
47 lines
2.1 KiB
Lean4
47 lines
2.1 KiB
Lean4
/-
|
|
Lux formal verification — entry point.
|
|
|
|
`lux_correctness` conjoins results proved elsewhere in this corpus. It holds
|
|
what it imports and nothing more, which is the only thing a top-level theorem
|
|
can honestly do: `lake build` succeeding here means Lean checked each
|
|
conjunct's proof, in its own module, from its own hypotheses.
|
|
|
|
Both conjuncts rest on Lean's ambient logic alone — no axiom of ours — which
|
|
`lean/axioms.py` reports per theorem. Deliberately absent:
|
|
|
|
- Safety and liveness. `Consensus.safety` composes two axioms and needs
|
|
`2 * alpha > n`, i.e. sampling more than half the network; in the
|
|
sub-sampled regime the protocol runs, safety is probabilistic and no
|
|
deterministic theorem of that shape holds. `Consensus.Liveness.liveness`
|
|
applies the ten axioms that are its argument.
|
|
- Post-quantum hardness. `Quasar.Consensus` reduces to hardness axioms: the
|
|
reduction is checked, the assumptions are assumed.
|
|
|
|
Maps to: the modules imported below.
|
|
-/
|
|
|
|
import Consensus.BFT
|
|
|
|
namespace Lux.Main
|
|
|
|
/-- Results this corpus proves outright, conjoined.
|
|
|
|
An earlier version stated four conjuncts, of which
|
|
`spreadBps * volumeUSD / 10000 ≥ 0` is true of every `Nat` and the fourth
|
|
was `True`; it imported no consensus or crypto module while its header said
|
|
"if this file compiles, consensus is safe and live" across ten libraries.
|
|
Each conjunct now names a theorem proved in the module it comes from, so
|
|
compilation depends on that proof rather than restating its statement. -/
|
|
theorem lux_correctness :
|
|
-- Quorum intersection: two quorums each above 2n/3, with f < n/3 faulty,
|
|
-- overlap in more than f nodes — so they share an honest one.
|
|
(∀ n f : Nat, f < n / 3 → ∀ q1 q2 : Nat,
|
|
q1 > 2 * n / 3 → q2 > 2 * n / 3 → q1 + q2 > n + f) ∧
|
|
-- An honest majority of 2f+1 in 3f+1 nodes clears that threshold.
|
|
(∀ f : Nat, 0 < f → 2 * f + 1 > 2 * (3 * f + 1) / 3) :=
|
|
⟨fun n f hf q1 q2 hq1 hq2 =>
|
|
Consensus.BFT.quorum_intersection n f hf q1 q2 hq1 hq2,
|
|
fun f hf => Consensus.BFT.honest_majority_sufficient f hf⟩
|
|
|
|
end Lux.Main
|