security/releases/2026-06-pq-threshold-stack/ASSUMPTIONS.md

Assumption ledger — release 2026-06-pq-threshold-stack

The proof is "under stated assumptions." This is the complete, cross-repo list of those assumptions, bucketed. Authoritative per-repo detail: luxfi/{pulsar,corona,magnetar}/AXIOM-INVENTORY.md + .assurance/reviewed-axioms.txt. Buckets:

• A — standard math fact. Discharge in a proof assistant or import from a trusted library. Allowed language: machine-checked / standard-math bridge.
• B — spec/serialization bridge. Accept with KATs + fuzzing + independent- implementation comparison + review. Allowed language: interop-tested and reviewed.
• C — open security assumption. Blocks "fully proven" unless discharged or explicitly excluded from the theorem. Allowed language: open assumption / review blocker / not fully proven.

Bucket histogram (real declarations)

Repo	A	B	C
pulsar (78 axioms)	16	41	21
corona (56 axioms)	18	27	11
magnetar	—	—	(threshold leg research-only; standalone leg has none)
p3q	—	—	1 (FRI proximity-gap soundness — standard STARK assumption)
consensus	—	—	1 (honest-majority / validator-threshold)

A — standard math facts (Lean-bridged; should fully discharge)

lagrange_inverse_eval, threshold_partial_response_identity, reconstruct_linear, shamir_correct, add_share_zeroR (pulsar + corona). Each is bridged to a Mathlib-backed Lean lemma (e.g. lagrange_inverse_eval → Crypto.{Pulsar,Corona}.Shamir.shamir_correct_at_target). These are the algebraic core the threshold reduction uses, never the security claim itself.

Implementation-correspondence bridges (§3 — close the theorem↔code gap)

Formal object	Implementation	Bridge evidence
Lean BoundaryClear	Go BoundaryClear	BoundaryClearance.lean + boundary_test.go (debug-oracle)
Lean FindHint↔UseHint	Go FindHint	machine-checked lemma + exhaustive edge tests
FIPS HighBits/Decompose	Go decompose/highBitsCoeff	KAT + property tests vs FIPS contract
FIPS sig encode	Go FinalizeSignature	independent-verifier interop (CIRCL + pq-crystals)

Where a bridge is only an axiom it is an interface axiom in bucket B and listed in AXIOM-INVENTORY.md.

C — OPEN security assumptions (the "fully-proven" blockers)

Each: statement · dependent claim · why open · what discharges it.

Toolchain note (corrected): the EasyCrypt toolchain is live on the authoring host (opam switch proofs: easycrypt + why3 + alt-ergo, z3 solver). Every .ec theory machine-checks via easycrypt compile, and the framework gate runs checks/ec-machine-check.sh on each invocation (pulsar 14/14, corona 14/14). The C-assumptions below are open not for lack of a toolchain — they are open because the relevant ops are opaque and the byte-walk that would discharge them is unwritten; the EC proofs are machine-checked conditional on these disclosed axioms.

1. combine_body_axiom (pulsar, corona) — the extracted threshold combine equals the centralised FIPS signer on the Lagrange-reconstructed master secret (reconstruct-then-sign). Blocks PULSAR-C3 / CORONA-EC byte-equality as an unconditional EC proof. Discharge: the Jasmin byte-walk. Why open: combine_abs_op is an opaque op, so the bridge is machine-checked only conditional on this axiom; the decomposition (Encoding/Reconstruct/ CombineSpec/CombineBridge) is unwritten.
2. S_functional_spec (pulsar, corona) — the single-party module is a faithful FIPS 204/RLWE signer. Discharge: libjade byte-walk.
3. pulsar combine_body_{matrix_a,mask_y,z_via_aggregation,partial_responses,w_low}_spec, sign_body_{matrix_a,mask_y,y,cs1,w_low}_spec, combine/sign_no_reject_on_accepted_honest_layout — the per-stage reconstruct-then-sign refinement steps. (The V04 ctx axioms mldsa_sign_ctx_axiom / algebraic_aggregate_ctx_body_axiom were removed with the deleted V04_Sign_Ctx.ec.)
4. corona combine_body_spec, combine_abs_op_lifted_bridge, threshold_public_commitment_eq_central, sign_abs_op_lifted_eq_rlwe — Boschini combine steps 2–6 inside the atomic byte-walk; reconstruct-then-sign refinement. Update — the combine bridge was discharged: the former whole-signature axiom combine_abs_op_lifted_eq_rlwe is now a machine-checked lemma (combine_abs_op_lifted defined as the real threshold aggregate; the secret-bearing z-leg proven via the keystone no_leak_z_aggregate). Its only residual is the narrow public-commitment axiom threshold_public_commitment_eq_central (the w = A·y agreement — no c·s; value public, EC op usk-parameterized), on which wrapper_combine_refines_abs is now conditionally machine-checked.
5. NonceTranscript soundness (pulsar) — validator-MPC clearance; today a debug oracle, registered fail-closed. Discharge: the validator-MPC security argument + a sound boundary-clearance ZK.
6. PartialProof / small-norm range (pulsar) — the L∞ bound has no faithful uniform-mask Σ proof; range gate is fail-closed (L2≠L∞).
7. FRI proximity-gap soundness (p3q) — standard STARK assumption; stated, not proven.
8. honest-validator-threshold (consensus) — the BFT majority assumption.
9. threshold SLH-DSA one-time-key safety (magnetar) — only relevant to the research-only THBS-SE leg, which reconstructs the seed; the production leg (independent sigs + quorum cert) does not rely on it. Honest: true no-reconstruction threshold SLH-DSA is open research (Kondi–Kumar–Vanegas).

The honest one-liner: All axioms are discharged, bridged, or disclosed. Open security assumptions remain review blockers. No claim is marketed "fully proven" while it depends on an undischarged C-assumption (enforced by luxfi/security/framework/checks/circular-proof.sh + claims-vs-reality.sh).