zeekay fc11458680 mlkem/proofs: ML-KEM-768 EC theories (0/0 admits) ...

EasyCrypt Tier A theories at crypto/mlkem/proofs/easycrypt/:

  MLKEM_Correctness.ec    - encaps/decaps correctness (FO-K + CPAPKE)
  MLKEM_INDCCA2.ec        - IND-CCA2 reduction to MLWE/MLWR
  MLKEM_Wire_Format.ec    - FIPS 203 byte-equality + KAT determinism
                            + Pulsar envelope binding + X-Wing
  lemmas/MLKEM_CT.ec      - CT obligations on Keygen/Encaps/Decaps

Closure strategy: each top-level theorem reduced to small set of
named functional hypotheses imported from the cloudflare/circl
ML-KEM-768 wrapper. Admit budget 0/0 across the pack.

Bridge map at proofs/lean-easycrypt-bridge.md pins axiom-to-
theorem correspondence 1:1 to Lean Crypto.MLKEM.

References: FIPS 203 (NIST 2024); Hofheinz-Hovelmanns-Kiltz
TCC 2017 (FO-K); Bos et al. EuroS&P 2018 (CRYSTALS-Kyber);
draft-connolly-cfrg-xwing-kem (X-Wing hybrid).

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

..

MLKEM_CT.ec

mlkem/proofs: ML-KEM-768 EC theories (0/0 admits)

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