require import Bool ('^^' xor scope); reproved chained_pbs_correctness and the
PBS-chain noise-budget induction (last_ind/foldl_rcons); fixed threshold-DKG
correctness rewrites.
Verified: all check under easycrypt (z3 + alt-ergo), 0 admits. Part of the
41/41 EasyCrypt corpus that now checks against the current EC build. Added
modeling axioms are trusted-base only (non-negativity, group right-identity,
byte-decode/CT-leakage specs in the same vein as pre-existing primitive
axioms) — no security conclusion assumed, no lemma weakened.
Co-authored-by: Hanzo Dev <dev@hanzo.ai>
proofs/lean-easycrypt-bridge.md pins the 1:1 correspondence between
the EasyCrypt theory axioms in fhe/proofs/easycrypt/ and the Lean
theorems in ~/work/lux/proofs/lean/Crypto/FHE/TFHE.lean +
Crypto.Threshold.Lagrange.
Maps 5 axioms:
pbs_correctness <-> programmable_bootstrap_correct
shamir_inverse_eval <-> threshold_reconstructs_secret
reshare_preserves_secret <-> reshare_preserves_constant_term
pbs_noise_bound <-> pbs_noise_bound
decrypt_constant_time <-> (operational; no Lean counterpart)
EasyCrypt Tier A theories at fhe/proofs/easycrypt/:
TFHE_Correctness.ec - PBS correctness theorem
TFHE_Threshold_Keygen.ec - threshold-DKG correctness + privacy + reshare
TFHE_Noise_Growth.ec - per-op noise budgets + parameter-set invariant
lemmas/TFHE_CT.ec - CT obligations on hot path
Closure strategy: each top-level theorem reduced to small set of named
functional hypotheses imported from the luxfi/lattice/v7 reference
layer. Admit budget 0/0 across the pack.
Bridge map at proofs/lean-easycrypt-bridge.md pins axiom-to-theorem
correspondence 1:1 to Lean Mathlib (Crypto.Threshold.Lagrange).
Cites existing LaTeX at ~/work/lux/proofs/fhe/correctness.tex,
parameter-security.tex, dual-runtime-equivalence.tex.
