Hanzo AI b951244d27 fhe/lean: TFHE Lean<->EC bridge map ...

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)

2026-05-19 11:30:28 -07:00

..

easycrypt

fhe/proofs: TFHE EC theories (0/0 admits)

2026-05-19 11:30:28 -07:00

lean-easycrypt-bridge.md

fhe/lean: TFHE Lean<->EC bridge map

2026-05-19 11:30:28 -07:00