mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zooqueen
506123454e
Adds two Lean 4 + Mathlib theories that replace the reconstruct-then-sign
misdirection in the Pulsar/Corona EasyCrypt byte-equality cones with the
HONEST no-leak identity, machine-checked on this host (lake build green,
0 sorry; #print axioms shows only [propext, Classical.choice, Quot.sound]
-- no sorryAx).
Crypto/Pulsar/NoLeakAggregate.lean:
- z_aggregate_no_reconstruct: the masked Lagrange z-aggregate equals
central z = (interp y).eval0 + c*f.eval0; the secret polynomial f
(master s1) is NEVER formed, only f.eval 0 inside the already-public z.
- z_aggregate_depends_only_on_secret: aggregate is a function of f.eval 0
+ public (y,c); the sharing randomness is invisible.
- hint_highbits_stable_under_hidden_shift / hint_is_fips_hint: re-exports
of the machine-checked BoundaryClearance facts -- the hint is recovered
from PUBLIC w' only, HighBits stable under the hidden c*s2 shift.
- NoLeakReduction + no_leak_under_standard_assumptions: the residual is a
STANDARD Module-LWE/Module-SIS simulation reduction, NOT a reconstruct.
Crypto/Corona/NoLeakAggregate.lean:
- pairwise_mask_telescopes: Sum_i (maskPrime_i - mask_i) = 0 by Fubini
reindex (the Corona telescoping pairwise-PRF mask cancellation).
- summed_response_is_mask_free: Sum_i z_i = Sum_i base_i (masks vanish).
- secret_aggregate_no_reconstruct: surviving c*Sum_i lambda_i*s_i = c*s
by Lagrange-at-0, master secret never formed.
- NoLeakReduction + no_leak_under_standard_assumptions: same standard
Module-LWE/Module-SIS residual.
The correctness cores depend on NO opaque assumption (the Module-LWE/MSIS
opaques are used only by the residual-reduction packaging). Both are the
machine-checked anchors for the new Pulsar_N1_NoLeak.ec / Corona_N1_NoLeak.ec
EC theories.