Files
zeekay e6c6417d52 proofs/cmp: Tier A EC theories + Lean bridges + Jasmin CT scaffolds
Adds the Tier A formal-artifact cluster for protocols/cmp (Lux profile
of CGGMP21 threshold ECDSA, CCS '21 / ePrint 2021/060). Mirrors
luxfi/pulsar's Tier A structure adapted to CCS '21's 4-round keygen +
3-round presign + 1-round online sign decomposition.

- proofs/easycrypt/CGGMP21_N1.ec — Class N1 byte-equality reduction
- proofs/easycrypt/CGGMP21_N1_Refinement.ec — keygen/presign/sign refinement
- proofs/easycrypt/CGGMP21_Paillier.ec — Paillier additive homomorphism
- proofs/easycrypt/CGGMP21_ZK.ec — 17 ZK subprotocol cluster obligation
- proofs/easycrypt/CGGMP21_N4.ec — refresh / proactive rotation
- proofs/easycrypt/lemmas/CGGMP21_CT.ec — constant-time obligations
- proofs/easycrypt/AXIOM-INVENTORY.md — honest enumeration
- proofs/lean-easycrypt-bridge.md — Lean↔EC bridge map
- jasmin/lib/ + jasmin/single-party/ + jasmin/presign/ + jasmin/threshold/

Admit budget: 1/1 (same one-line group-identity admit as FROST_N4).
ZK cluster obligation surface honest: 17 subprotocols enumerated,
mechanization is multi-year program documented in
AXIOM-INVENTORY.md §closure roadmap.
2026-05-19 08:34:25 -07:00
..