Antje WorringandHanzo Dev 79bc183c6e mlkem/easycrypt: port ML-KEM proofs to current EasyCrypt ...

Fixed message-type inconsistencies in the model; '^^' is now boolean-xor
(use '^' = RField.exp via Real); import RealOrder; stricter apply/rewrite.
Reproved mlkem_correctness and IND-CCA2 advantage bound.

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:32:55 -07:00

..

easycrypt

mlkem/easycrypt: port ML-KEM proofs to current EasyCrypt

2026-06-02 11:32:55 -07:00

lean-easycrypt-bridge.md

mlkem/lean: ML-KEM-768 Lean<->EC bridge map

2026-05-19 08:41:45 -07:00