Corona is Module-LWE (threshold-Raccoon/Ringtail), NOT Ring-LWE. Confirmed in code: sign/sign.go samples A in R_q^{8x7} (sign.go:87 SamplePolyMatrix M=8,N=7), secret s a rank-7 ring vector, b=A*s+e (sign.go:106-107) over R_q=Z_q[X]/(X^256+1) (LogN=8), q=0x1000000004A01 -- rank>1 module structure, not rank-1 ring-LWE. threshold/threshold.go:4-5 already said Module-LWE.
Fixed the family label across README, SPEC, SUBMISSION, NIST-SUBMISSION, PATENTS, LLM, CONTRIBUTING, SECURITY, CHANGELOG, DEPLOYMENT-RUNBOOK, Makefile, AXIOM-INVENTORY, PROOF-CLAIMS, BLOCKERS, CRYPTOGRAPHER-SIGN-OFF, FIPS-TRACEABILITY, TRUSTED-COMPUTING-BASE, AUDIT-2026-05/06, docs/mptc/*, jasmin/README, 3 Go comments + cli help string.
Also corrected the downstream false claim that Corona (Ring-LWE) and Pulsar (Module-LWE) are 'different lattice families' giving 'structural/family diversity': both are Module-LWE, so the Double-Lattice defense is construction/implementation diversity (threshold-Raccoon vs ML-DSA), not hardness-family diversity; a Module-LWE break affects both legs (hash-based Magnetar is the assumption-diversifier). Fixed companion R-SIS -> Module-SIS where it was the module scheme's SIS assumption; added the Langlois-Stehle (DCC 2015) Module-LWE citation alongside LPR 2010.
Delicate artifacts: proof identifiers (rlwe_sign_op, RLWE_Functional theory/file, *_eq_rlwe bridges, CentralRLWESign, RLWESign, rlwe_compute_*) were NOT renamed -- EasyCrypt/jasmin toolchains are absent here so a rename cannot be compile-verified, and .assurance/ gates parse those names. Added clarifying naming notes to the 5 prominent .ec files, proofs/easycrypt/README.md, AXIOM-INVENTORY.md, and jasmin/rlwe/sign.jazz. .assurance/*.txt left untouched (already say Module-LWE/Module-SIS; rlwe tokens are gate-parsed identifiers). Left AUDIT-2026-06.md:463 historical rename-log and the ProtoStar-LWE paper-title substring untouched.
go build ./... and go test ./... green (GOWORK=off; all packages ok).
The EC byte-equality (corona_n1_byte_equality) proved the threshold combine
bit-equals CombineAbs, whose sign_abs_op_lifted_eq_rlwe bridge pins it to
rlwe_sign_op on the LAGRANGE-RECONSTRUCTED master secret -- exactly the path
the Boschini/Raccoon production combine must never take (CORONA-EC-RECON-MODEL).
This pass re-scopes that cone as IDEALISED CORRECTNESS and adds the HONEST
production model whose residual is a STANDARD Module-LWE/MSIS reduction.
New proofs/easycrypt/Corona_N1_NoLeak.ec (written; machine-recheck pending
EasyCrypt -- no `ec` on host, scripts/checks/ec-compile.sh is the CI gate):
- mask_telescope_zero [B, Lean-backed]: Sum_i (maskPrime_i - mask_i) = 0 --
the pairwise-PRF masks (z_i = R_i*u + maskPrime_i + c*lambda_i*s_i - mask_i)
are the same double sum reindexed (Fubini), so they cancel on aggregation.
Machine-checked in Lean as pairwise_mask_telescopes.
- no_leak_z_aggregate: the surviving aggregate is R*u + c*s by Lagrange-at-0
WITHOUT forming the master secret and with no per-party c*s_i ever exposed.
- no_leak_reduction [C-standard, OPEN]: under Module-LWE + Module-SIS the
public transcript leaks nothing about s beyond one Boschini signature. The
honest replacement for sign_abs_op_lifted_eq_rlwe -- a reduction to the SAME
substrate AXIOM-INVENTORY.md §1 already lists, secret NEVER reconstructed.
The CORRECTNESS CORE is machine-checked in Lean 4 + Mathlib on this host
(luxfi/proofs: Crypto.Corona.NoLeakAggregate / Threshold_Lagrange; lake build
green, #print axioms shows no sorryAx).
Disclosure updated to match reality: AXIOM-INVENTORY (new Bucket C-standard +
"A is machine-checked in Lean"), PROOF-CLAIMS (two models, §0 Disclosure 1),
BLOCKERS (CORONA-EC-RECON-MODEL re-scoped, first criterion now [x]), budget
AXIOM 56->58. Framework gate PASS (all 5 checks); go build + full test suite green.
Reclassify (not reduce) the EasyCrypt axiom surface and correct the prior
inventory's understatement. NO axioms discharged this pass (honest): no
easycrypt toolchain on host, and every in-file-derivable axiom is already a
proved lemma; residual A/B axioms are over abstract ops/constants
(op group_pk_width : int., op sig_len : int.) and the C axioms are open.
- AXIOM-INVENTORY.md: replace the §2 table that mislabelled the wrapper
bridges and section-local module contracts as "Discharged in the
Wrapper". They are now correctly bucket C / OPEN: combine_body_spec hides
the Boschini combine steps 2-6, and combine_abs_op_lifted_bridge /
sign_abs_op_lifted_eq_rlwe pin the lifted op to rlwe_sign_op on the
Lagrange-RECONSTRUCTED master secret (reconstruct-then-sign). Complete
bucketed census of all 56 axioms -- A (18, 5 Lean-bridged), B (27), C
(11) -- one row per axiom with name, file:line, justification. CT
contracts (sign_round{1,2}_constant_time) classified C/fail-closed.
- PROOF-CLAIMS.md: add assurance vocabulary + two load-bearing disclosures
-- (1) the EC byte-equality MODELS reconstruct-then-sign; (2) Corona has
NO independent interop verifier (R-LWE has no NIST target), so its
byte-equality is asserted + same-construction Go<->C++ KAT, never
"proven/verified". Corrects the §4 claim that Pulsar is machine-checked
"at every step" (it too rests on the same reconstruct-then-sign cone).
- BLOCKERS.md (new): CORONA-EC-RECON-MODEL, CORONA-CT-PENDING,
CORONA-NO-INDEP-VERIFIER -- all OPEN, all cross-referenced to the shared
external-review gate.
- .assurance/reviewed-axioms.txt: list every load-bearing / security-cone
axiom (A: 5 Lean-bridged; C: combine_body_axiom, S_functional_spec,
combine_body_spec, combine_abs_op_lifted_bridge, sign_abs_op_lifted_eq_rlwe)
with bucket + justification.
- .assurance/budget.txt: correct prose (0 real admit. tactics; AXIOM=56 exact).
Framework gate (circular-proof + axiom-budget + the other three) PASS with
full disclosure. go test ./... green (no Go touched).
Three Tier-A-required submission docs that were honestly omitted in
the v0.5.0 scaffold per the cryptographer agent's directive ("don't
fabricate proof claims that don't exist"):
- AXIOM-INVENTORY.md: enumerates construction-level + implementation-level
axioms with explicit closure plans. EC theory shells are roadmap v0.7.0;
this doc establishes the inventory the eventual proofs will discharge.
- FIPS-TRACEABILITY.md: Boschini ePrint 2024/1113 + IEEE S&P 2025
section → code mapping. R-LWE has no FIPS standard; Boschini paper
is the construction-level normative reference.
- CRYPTOGRAPHER-SIGN-OFF.md: APPROVED WITH GATES. Verdict mirrors
Pulsar's v1.0.7 sign-off structure. Gates: GATE-1 EC theory shells,
GATE-2 Lean ↔ EC bridge, GATE-3 dudect 10⁹ samples, GATE-4 external
audit. All on v0.7.0 / v0.8.0 roadmap.
Tier label honest assessment: **Tier A documentation shape complete**;
the algorithmic-soundness gates inherit from Boschini paper, the
formal-methods gates are explicitly roadmap-tracked, not fabricated.
This positions Corona for NIST MPTC v0.2 submission window with full
review-ready doc package.
zeekay
zooqueen