zeekayandHanzo Dev 38367da825 proofs: no-double-finalization under the decided-height sign-gate + scheme-agnostic cert ...

Formalizes the incident-1082814 / height-10-storm durable fix as shipped in
luxfi/consensus v1.35.16 (audited against the code 2026-07-02).

definitions/finality-definitions.tex:
- two finality authorities (acceptance vs certified finality; sole QC writer)
- durable decided-floor phi = max(FinHeight, fsync'd finalizedThrough,
  vm.LastAccepted height); monotone, restart-surviving, sign-gate-only (PART-A)
- sign admissibility (decided-height gate + one-per-height/lock rule)
- canonical-commitment keying (duplicate alias vs fork)
- observable double-finalization

quasar-cert-soundness.tex: new section "Finality Admission: No Double-Finalization"
- Lemma floor-soundness (phi <= network decided height, costs no liveness)
- Lemma no-window durability (slot{H} present OR phi>=H, always)
- Lemma honest one-canonical-per-height, durable across restart
- Theorem No double-finalization (quorum intersection + honest one-per-height)
- Corollary PART-A non-interference (ledger stays (0,false)-until-cert)
- discharges the prior FLAG on Cor. "No conflicting certificates" (code verified)
- empirical: 5-node storm to height 76, 0 equivocation, rolling-restart reconverge

pq-finality-no-bls.tex: new section "Scheme-agnostic certificate and the
signature registry"
- SigSchemeID registry (0x10 BLS .. 0x52 Pulsar-M-65 production default)
- scheme-parametric quorum predicate; scheme-bound transcript
- Lemma cross-suite confusion resistance (flipped byte breaks sig verify)
- Proposition PQ migration is a profile flip (safety invariant under s->s')
- assumption-diversity remark (Pulsar+ML-DSA both lattice; SLH-DSA is disjoint)

Both PDFs regenerated; pdflatex clean (20 pp / 7 pp).


Co-authored-by: Hanzo Dev <[email protected]>

2026-09-17 13:05:51 -07:00

333 KiB

Raw Permalink History

View Raw