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]>