zeekayandHanzo Dev a413de56af lean: the scheme IDs the deployed gate reads, and forgery relative to the adversary ...

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

2026-07-29 11:56:31 -07:00

..

Coverage.lean

lean: the scheme IDs the deployed gate reads, and forgery relative to the adversary

2026-07-29 11:56:31 -07:00

Profile.lean

lean: the scheme IDs the deployed gate reads, and forgery relative to the adversary

2026-07-29 11:56:31 -07:00