Antje WorringandHanzo Dev dd53f8b350 fhe/easycrypt: port TFHE proofs to current EasyCrypt ...

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>

2026-06-02 11:33:51 -07:00

..

easycrypt

fhe/easycrypt: port TFHE proofs to current EasyCrypt

2026-06-02 11:33:51 -07:00

lean-easycrypt-bridge.md

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

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