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).
zooqueen