mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
2dd030dd98
Each of these made the corpus unsound: from a false axiom every theorem in
it follows, so the 756 stated results meant nothing while they stood.
Crypto/Magnetar.lean carried two axioms of the shape
∀ (oracle : Nat → Nat), ∃ (x : Nat), oracle x ≠ x
which the identity function refutes, yielding `∃ x, x ≠ x`. Both were roots
of `lean_lib Crypto`, so both compiled. Neither had a user. Family
disjointness quantifies over adversaries and advantages; `Nat → Nat` cannot
state it, so it is prose until the advantage model exists.
Protocol/Handshake.lean defined the session KDF as integer addition and then
axiomatised that distinct transcripts give distinct keys. ⟨1,1,1⟩ and ⟨1,0,2⟩
both derive 3 with transcripts 1 ≠ 2. `deriveSessionKey` is now opaque, which
is what a hash is in a model, and collision resistance is the one assumed
property. `transcript_binding` followed from unfolding the addition; it now
follows from the assumption.
Consensus/Safety.lean `unique_threshold` counts `honestPreferring` over
`Finset.univ` — the whole validator set, not the k-sample — so it needs
`2 * alpha > n`. Legal counterexample without it: n = 1000, f = 100, k = 20,
alpha = 14, with 900 honest nodes split 450/450, satisfies every hypothesis
and concludes v1 = v2. The hypothesis is now stated and threaded through
`theorem safety`, which makes the real limitation visible in the type: with
alpha ≤ k ≤ n it forces sampling more than half the network every round. In
the sub-sampled regime the protocol runs, safety is probabilistic and no
theorem of this shape holds. Consensus.ThresholdProof already proves the
pigeonhole under exactly this hypothesis.
strict-e2e-pq cited ePrint 2024/1113 as "Corona: A Lattice-Based Threshold
Signature for Post-Quantum Consensus" with no authors. That paper is
Ringtail, by Boschini, Kaviani, Lai, Malavolta, Takahashi and Tibouchi.
Corona is our implementation of it. Restored their title and their names.
Verified with a local lake build over every library.
Co-authored-by: Hanzo Dev <[email protected]>
LUX_STRICT_E2E_PQ formal proof tree
Machine-checked counterparts to the LUX_STRICT_E2E_PQ paper
(luxfi/papers/lp-stricte2epq/).
The strict-e2e-pq profile pins every byte that gates a state transition on Lux to a FIPS 203 / 204 / 205 primitive or a SHA3-family transcript. This directory carries the proofs of the underlying soundness claims, the TLA+ state machine for the profile lifecycle, and the Go property tests that exercise the canonical Go code under both strict and permissive profiles.
See LP-105 §Claims and evidence for the canonical claims/evidence table.
Files
| File | Language | Purpose |
|---|---|---|
strict-e2e-pq-soundness.tex |
LaTeX | formal soundness statement (companion to lp-stricte2epq §13) |
../tla/StrictPQProfile.tla |
TLA+ | profile state machine and SchemeGate invariant |
../tla/MC_StrictPQProfile.tla |
TLA+ | TLC model checker config |
../lean/StrictE2EPQ/Profile.lean |
Lean 4 | IsE2EPQ profile proposition |
../lean/StrictE2EPQ/Coverage.lean |
Lean 4 | 14-path PQ coverage theorem |
../property/strict_pq_test.go |
Go | property tests against luxfi/consensus |
Build
# Lean 4
cd ../lean && lake build StrictE2EPQ
# TLA+
cd ../tla && tlc MC_StrictPQProfile.tla
# Go property tests
cd ../property && GOWORK=off go test ./...
Soundness statement
Under LUX_STRICT_E2E_PQ:
- Every signed transaction is verified under ML-DSA-65 (FIPS 204).
tx_auth_rootinclusion is sound under SHA3-384 Merkle.ComputeRoundDigestis collision-resistant under SHA3-384.- Pulsar finality signatures verify under M-LWE soundness.
- Profile-bumps are the only mechanism that can relax the posture; the pinned digest is the operator-visible barrier.
See strict-e2e-pq-soundness.tex for the formal statement; see
Profile.lean and Coverage.lean for the Lean 4 propositions.