FULLY-PQ-AUDIT.md: per-production-path PQ-primitive ledger with file:line evidence, complete classical-crypto reachability list, and the verdict. Headline finding: QuasarCert.VerifyWithRealKeys required BLS-12-381 on the finality path (contradicting the cert's pure-PQ contract) -- FOUND AND FIXED under this audit (consensus: BLS optional + fail-closed >=1-leg guard, regression-tested). Post-fix verdict: the production consensus/finality/ signature-verification envelope is FULLY POST-QUANTUM. All other classical crypto (optional BLS fast-path, Corona DKG-ceremony Ed25519/X25519, Verkle banderwagon point-decode, qzmq ML-KEM stub, gated EVM precompiles, superseded+ forbidden Groth16) is confirmed OFF the finality-cert verification path. STANDARD-ASSUMPTIONS.md: the irreducible minimal cryptographic-assumption ledger -- Module-LWE, Module-SIS, SLH-DSA SHAKE hash-family EU-CMA, FRI proximity-gap soundness (staged), SHAKE/cSHAKE/KMAC as RO, honest-validator BFT threshold. For each: dependent claims, why standard/accepted, parameter set + NIST PQ category. The honest 'fully proven UNDER THESE assumptions' bedrock; explicitly excludes pairing/DLOG/factoring/trusted-setup.
15 KiB
Standard-Assumptions Ledger — Lux PQ Threshold Stack, release 2026-06-pq-threshold-stack
This is the irreducible bedrock: the complete, minimal set of cryptographic assumptions the entire release reduces to. It is the precise meaning of "fully proven under stated assumptions" — strip these and nothing is left to assume; everything else in the stack is a construction, a reduction, or an implementation bridge that rests on top of this list.
Relationship to the other ledgers. This file is the minimal external view (what a cryptographer must accept to trust the release). It is distinct from, and complementary to:
ASSUMPTIONS.md— the per-repo A/B/C axiom bucket disclosure (which declared EasyCrypt/Lean axioms are standard-math vs spec-bridge vs open).CLAIMS.md— the claim matrix (each claim ID → evidence class → assumptions → status).- per-repo
AXIOM-INVENTORY.md+.assurance/reviewed-axioms.txt— the authoritative bucketed source of truth.
Every Bucket-C "open assumption" in those files reduces to one of the assumptions below; this ledger is the closure of that reduction. No assumption here is "proven" — by definition. They are the accepted hardness / soundness substrate. Where the release proves something, it proves it relative to these.
A note on honesty. Two assumptions below (A1–A2 for the lattice families, A4 for FRI) are STANDARD and accepted in the literature and we STATE them rather than prove them — that is correct cryptographic practice, not a gap. What would be a gap is a construction-specific assumption masquerading as standard; we have none of those — every item below is a community-vetted, NIST-standardized or peer-reviewed hardness/soundness assumption, used at a standardized parameter set.
The six irreducible assumptions
| # | Assumption | Family | Standardization | Used by (claims) |
|---|---|---|---|---|
| A1 | Module-LWE (decisional/search hardness) | Lattice | FIPS 203 (ML-KEM), FIPS 204 (ML-DSA) | ML-DSA sigs, Pulsar, Corona, ML-KEM transport |
| A2 | Module-SIS (short integer solution hardness) | Lattice | FIPS 204 (ML-DSA EU-CMA) | ML-DSA sigs, Pulsar (strong unforgeability) |
| A3 | SLH-DSA hash-family security = preimage/2nd-preimage/collision resistance of SHAKE ⇒ FORS + WOTS+ + hypertree EU-CMA | Hash-based | FIPS 205 (SLH-DSA) | Magnetar standalone + certification, SLH-DSA precompile |
| A4 | FRI proximity-gap soundness (+ Fiat-Shamir in the ROM) | Hash-based IOP | Peer-reviewed (BBHR18, BCIKS20); not a NIST standard but the accepted STARK assumption | P3Q low-degree test (staged finality compression) |
| A5 | SHAKE / cSHAKE / KMAC modeled as a random oracle (and as a collision-resistant / domain-separating hash) | Symmetric (sponge) | FIPS 202, SP 800-185 | every Fiat-Shamir transcript, domain separation, Merkle/commitment binding, KMAC MACs |
| A6 | Honest-validator threshold (BFT majority; ≥ quorum weight is honest) | Protocol / system | Classical BFT model | the weighted quorum certificate = finality |
Everything else the release ships — threshold certification, byte-equality to FIPS verifiers, the BCC/CEF no-leak signing transcripts, Merkle inclusion, weighted-quorum binding — is a construction or reduction over A1–A6, not a new assumption.
A1 — Module-LWE
Statement. For the module rank, ring, and modulus of a given parameter set,
the decisional Module-LWE distribution (A, A·s + e) is computationally
indistinguishable from uniform (and search-MLWE is hard).
Which claims depend on it.
- ML-DSA per-validator signatures (P1, P4) — the quorum certificate's per-signer ML-DSA verifier; the EVM ML-DSA precompile (P9). EU-CMA of ML-DSA reduces to MLWE (key indistinguishability) + MSIS (A2).
- Pulsar threshold ML-DSA (P5) — same hardness; the threshold construction is byte-equal to a single-party FIPS 204 signature, so its unforgeability is exactly ML-DSA's under A1+A2 (the threshold layer adds no new hardness assumption — it adds the reconstruct-then-sign / BCC refinement, which is a construction over A1+A2, disclosed Bucket-C, not a hardness assumption).
- Corona threshold (P6) — Ringtail/Raccoon-family Module-LWE; the masked- aggregate signature's unforgeability reduces to MLWE.
- ML-KEM-768 transport (P10) — IND-CCA2 of ML-KEM reduces to MLWE.
Why standard. Module-LWE is the hardness assumption NIST standardized in FIPS 203 and FIPS 204 (2024) after the multi-year PQC competition. It is a structured-lattice problem with a worst-case-to-average-case connection (Langlois–Stehlé) and is the most scrutinized post-quantum assumption in deployment.
Parameter sets + security level.
- ML-DSA-65 (NIST PQ Category 3, ≥ AES-192-equivalent) — production
identity / quorum default (
ModeP65,pulsar/ref/go/pkg/pulsar/params.go:26;QuorumSchemeMLDSA65 = 0x42). - ML-DSA-44 (Cat 2) and ML-DSA-87 (Cat 5) also registered
(
QuorumSchemeMLDSA44/87). - Pulsar production ring/modulus:
N = 256(ring degree),Q = 0x1000000004A01(48-bit NTT-friendly prime), moduleM = 8,Dbar = 48,Kappa = 23; parameter tightness classical 2^142 / quantum 2^130 (BDGL sieving + Grover) perproofs/quasar-cert-soundness.texApp. E. - Corona production ring/modulus:
N = 256,q = 0x1000000004A01(48-bit) (corona/SECURITY.md:35-36).
A2 — Module-SIS
Statement. For the parameter set, finding a short nonzero z with A·z = 0 (mod q) (short integer solution in the module) is computationally hard.
Which claims depend on it. ML-DSA / Pulsar strong unforgeability (P1, P4, P5): an ML-DSA forgery yields a short MSIS solution. A1 gives key indistinguishability; A2 gives that you cannot forge a short signature vector. Together they are the EU-CMA reduction of FIPS 204.
Why standard. MSIS is the companion assumption to MLWE in the Fiat-Shamir-with-aborts (Lyubashevsky) signature design that FIPS 204 standardizes. Same lattice provenance and scrutiny as A1.
Parameter sets + security level. Same parameter sets as A1; the MSIS
bound is set by the ML-DSA-65 (Cat 3) / Pulsar (Dbar=48, Kappa=23)
parameters. Security level as A1: NIST Cat 3 for ML-DSA-65; Pulsar 2^142
classical / 2^130 quantum.
A3 — SLH-DSA hash-family security (FORS + WOTS+ + hypertree EU-CMA)
Statement. The SHAKE-based hash functions used by SLH-DSA are preimage-, second-preimage-, and collision-resistant (and behave as random oracles where the proof needs it), so that the FORS few-time signature, the WOTS+ one-time signature, and the XMSS/hypertree authentication structure together give EU-CMA for the stateless hash-based signature.
Which claims depend on it.
- Magnetar standalone per-validator SLH-DSA signatures (P2, P7) — the quorum certificate's SLH-DSA verifier; the EVM SLH-DSA precompile (P9).
- Magnetar threshold = certification (MAGNETAR-C1..C7): production Magnetar is N independent FIPS 205 signatures aggregated by a quorum cert; each signature's unforgeability is exactly A3. The certification layer adds no new hardness assumption (it is a count over independent A3 signatures).
- Not depended on by production: true no-reconstruction threshold SLH-DSA is open research (Kondi–Kumar–Vanegas impossibility for black-box-RO thresholdization). The research-only THBS-SE leg reconstructs the seed and is excluded from production claims.
Why standard. A3 is the security goal of NIST FIPS 205 (2024), inherited
from the SPHINCS+ submission (Bernstein et al.). It is the most conservative
PQ signature assumption: it rests on symmetric (hash) security only, with no
structured-lattice or number-theoretic assumption — which is precisely why
Magnetar is the cross-family backstop ("if every lattice family breaks,
hash-based one-wayness still secures finality", types.go:115-125).
Parameter sets + security level.
- SLH-DSA-SHAKE-192s (
ModeM192s,QuorumSchemeSLHDSA192s = 0x06) — Magnetar production target, NIST PQ Category 3 (≥ 192-bit classical), smallest signatures at that level (magnetar/SPEC.md §2). - SLH-DSA-SHAKE-192f (
0x16) and 256s (0x07) also registered. - Single-party primitive dispatches to
cloudflare/circl/sign/slhdsav1.6.3 (community-audited FIPS 205 reference).
A4 — FRI proximity-gap soundness (+ Fiat-Shamir in the ROM)
Statement. The FRI low-degree test is sound up to the proximity gap: a prover that passes the FRI verifier with non-negligible probability is, with overwhelming probability, committed to a codeword within the asserted distance of a low-degree polynomial. Combined with Fiat-Shamir (A5) the interactive soundness becomes non-interactive in the random-oracle model.
Which claims depend on it. P3Q STARK/FRI soundness (P3Q-C4, P8). This
is the ONE genuinely STARK-specific assumption, and it is stated, not
proven — correct practice. P3Q's docs frame it honestly: "64 queries over an
LDE of rate ≤ 1/8 gives ≥ 100-bit soundness for the FRI proximity gap"
(p3q-fri/src/prover_shared.rs:16); SECURITY.md:16 states a
conjectured-security target (≥ 128-bit classical, ≥ NIST PQ Cat 3). No
claim of a soundness proof is made.
Scope today. P3Q is staged, not live, for finality (the N-FIPS-verification Keccak-AIR circuit is not built — §4 of FULLY-PQ-AUDIT.md). So A4 currently gates a roadmap path (finality compression), not today's finality verification (which is full-node-verifiable under A1–A3, A5–A6). A4 becomes load-bearing for finality only when the P3Q rollup circuit ships and is audited.
Why standard / accepted. FRI and its proximity-gap soundness are the foundation of every deployed STARK (StarkWare, Plonky3, RISC Zero). The bounds are peer-reviewed (Ben-Sasson–Bentov–Horesh–Riabzev 2018; Ben-Sasson–Carmon– Ishai–Kopparty–Saraf 2020 proximity gaps). It is not a NIST standard, but it is the accepted soundness assumption for hash-based IOPs and depends only on symmetric (hash) security for its commitments, so it is post-quantum.
Parameter set + security level. Goldilocks field p = 2^64 − 2^32 + 1
(p3q-field/src/goldilocks.rs:15); cSHAKE256 Merkle commitments
(p3q-sha3, p3q-merkle); 64 FRI queries at LDE rate ≤ 1/8 → ≥ 100-bit FRI
soundness; conjectured ≥ 128-bit classical / NIST PQ Cat 3 overall target.
A5 — SHAKE / cSHAKE / KMAC as a random oracle (and collision-resistant hash)
Statement. The Keccak sponge instantiated as SHAKE128/256, cSHAKE256, and KMAC256 behaves as a random oracle where the security proofs need one, and is collision- and preimage-resistant where used as a plain hash; distinct cSHAKE customization strings yield independent oracles (domain separation).
Which claims depend on it. Pervasive — it is the symmetric substrate under everything:
- Fiat-Shamir for every challenge derivation (Pulsar
SampleInBall/transcript, Corona transcript, P3Q challenger, the no-leak BCC/CEF transcripts). - Merkle / vector-commitment binding (quorum-cert validator-set Merkle, FRI
Merkle, Verkle hash-based proof check
verifyIPAOpening). - KMAC256 MACs (
quasar/bls.goevent-horizon attestations, the KMAC envelope-auth patterns). - Domain separation: every protocol's distinct customization tags
(
MAGNETAR-…,PULSAR-…,CORONA-…,LUX-VERKLE-…) rely on SP 800-185's guarantee of no cross-(N,S) collision.
Why standard. FIPS 202 (SHA-3/SHAKE) and SP 800-185 (cSHAKE, KMAC, TupleHash). Keccak is the most analyzed sponge; the random-oracle instantiation of SHAKE is the standard modeling assumption for hash-based and Fiat-Shamir constructions. Post-quantum: best known quantum attacks are generic (Grover/BHT), so the security level halves predictably and the parameter sizes are chosen accordingly.
Parameter set + security level. SHAKE256 / cSHAKE256 / KMAC256 at 256-bit capacity → 128-bit collision / quantum-generic security; KMAC output widths 48 bytes (SHA3-384) canonical for the consensus MAC bundles (32-byte legacy refused under strict-PQ). This is consistent with NIST Cat 3 across the stack.
A6 — Honest-validator threshold (BFT majority)
Statement. A quorum-weight subset of the validator set is honest: at least the configured threshold weight of validators follow the protocol and do not collude to sign conflicting finality.
Which claims depend on it. The weighted quorum certificate = finality (QUASAR-C1..C7, P3). The certificate proves "≥ quorum weight of distinct, in-set validators each produced a valid INDEPENDENT PQ signature over the same domain-separated message"; that this implies finality (no two conflicting blocks finalize) is the BFT-majority argument — a system/protocol assumption, not a cryptographic-hardness one. The cryptography (A1–A3, A5) guarantees the signatures are unforgeable and the count is honest; A6 is what turns an honest count into safety.
Why standard. This is the classical Byzantine-fault-tolerance threshold
assumption underlying every BFT consensus (PBFT, Tendermint, HotStuff,
Snowman/Avalanche-family). It is not cryptographic and not post-quantum-
specific; it is the system trust model. The quorum-cert red-team
(QUASAR-C1..C7, all PoCs fail closed) verifies the cryptographic binding
that prevents count/weight inflation, duplicate signers, out-of-set signers,
and cross-domain replay — i.e. that an adversary cannot manufacture a
spurious honest count; A6 is the residual that the genuine count is honest.
The honest one-paragraph statement
The Lux PQ threshold stack is fully proven under exactly these six assumptions: Module-LWE (A1), Module-SIS (A2), the SLH-DSA SHAKE hash-family EU-CMA (A3), FRI proximity-gap soundness (A4, staged), SHAKE/cSHAKE/KMAC as a random oracle (A5), and an honest-validator BFT threshold (A6). A1–A3 and A5 are NIST-standardized (FIPS 202/203/204/205, SP 800-185) at NIST PQ Category 3 parameters; A4 is the peer-reviewed, accepted STARK soundness assumption (hash-based, post-quantum) and currently gates only the staged finality-compression path; A6 is the classical BFT system model. Every other security property the release asserts — threshold certification, FIPS byte-equality, no-leak signing transcripts, Merkle/quorum binding — is a construction or a reduction over this substrate, not a new assumption. Stripping these six leaves nothing to assume. This is the bedrock the "proven under stated assumptions" language refers to.
What is NOT on this list (deliberately): no pairing / co-CDH (the BLS fast-path is optional and off the PQ-finality path — see FULLY-PQ-AUDIT.md §2.1; a pure-PQ cert does not depend on it), no discrete log, no factoring, no elliptic-curve assumption, no trusted setup, no SNARK knowledge-of-exponent / AGM assumption (Groth16/KZG are superseded and forbidden under strict-PQ). Their absence from this ledger is the precise content of "fully PQ".