Reproduce — release `2026-06-pq-threshold-stack`

Anyone can re-derive every gate result from the pinned commits. The certificate is reproducible or it is vibes.

1. Check out the exact objects

Use the hashes in RELEASE-MANIFEST.toml (a new commit invalidates the certificate until prove-release.sh is rerun):

for r in pulsar corona magnetar consensus p3q security; do
  git -C ~/work/lux/luxfi/$r rev-parse HEAD   # must match RELEASE-MANIFEST.toml
done

2. Run the once-and-for-all proof

bash ~/work/lux/luxfi/security/framework/prove-release.sh \
     ~/work/lux/luxfi/security/releases/2026-06-pq-threshold-stack
# -> writes gate-results.json, prints PASS/FAIL

3. Per-layer evidence (run independently)

# assurance gate (cheat-class detectors + budgets) — every repo
bash ~/work/lux/luxfi/security/framework/check.sh

# tests (the implementation evidence layer — NOT the proof)
(cd ~/work/lux/luxfi/pulsar    && go test ./ref/go/pkg/pulsar/ -count=1)
(cd ~/work/lux/luxfi/corona    && go test ./... -count=1)
(cd ~/work/lux/luxfi/magnetar  && CGO_ENABLED=1 go test ./... -count=1)
(cd ~/work/lux/luxfi/consensus && GOWORK=off go test ./protocol/quasar/ -count=1)
(cd ~/work/lux/luxfi/p3q       && cargo test --workspace)

# red-team PoCs MUST PASS = the attacks fail closed
(cd ~/work/lux/luxfi/consensus && GOWORK=off go test ./protocol/quasar/ -run Redteam -count=1)
(cd ~/work/lux/luxfi/p3q       && cargo test --workspace f1_ f2_ f3_ f4_)

# interop (independent FIPS verifiers — the standards-conformance hook)
(cd ~/work/lux/luxfi/pulsar    && go test ./ref/go/pkg/pulsar/ -run 'BCCSign|Interop' -count=1)

4. Machine-checked math (the proof layer)

EasyCrypt/Lean live in luxfi/proofs + each repo's proofs/. Both toolchains are live on the host — Lean via lake build, EasyCrypt via the opam switch (eval $(opam env); easycrypt compile <file>.ec, z3/alt-ergo solvers). Actually compile every EC theory (a .eco or a "proven" doc line is not evidence):

# EasyCrypt: machine-check every theory (fails on any non-compiling .ec)
bash ~/work/lux/luxfi/security/framework/checks/ec-machine-check.sh ~/work/lux/luxfi/pulsar
bash ~/work/lux/luxfi/security/framework/checks/ec-machine-check.sh ~/work/lux/luxfi/corona

# no undischarged theorem-critical axiom; comment-aware unproven-assertion budget
bash ~/work/lux/luxfi/security/framework/checks/circular-proof.sh ~/work/lux/luxfi/pulsar
bash ~/work/lux/luxfi/security/framework/checks/claims-vs-reality.sh ~/work/lux/luxfi/pulsar
bash ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh    ~/work/lux/luxfi/corona

Corona's wrapper_combine_refines_abs machine-checks conditional on the disclosed OPEN bridge combine_abs_op_lifted_eq_rlwe (AXIOM-INVENTORY C11) — EC-compiled, not "fully proven."

5. Read the claim chain

CLAIMS.md (claim → evidence class → assumptions) · ASSUMPTIONS.md (the A/B/C ledger) · redteam/*.md (adversarial evidence) · EXTERNAL-REVIEW-SIGNOFF.md (claim-ID sign-off). The release is "proven under stated assumptions" only when all five layers + external sign-off are present.

3.1 KiB Raw Permalink Blame History

Reproduce — release 2026-06-pq-threshold-stack