Files
zeekay e8f154a5b1 proofs/bls: Tier A EC theories + Lean bridges + Jasmin CT scaffolds
Adds the Tier A formal-artifact cluster for protocols/bls (Lux profile
of Boldyreva 2003 threshold BLS over BLS12-381). Mirrors luxfi/pulsar's
Tier A structure adapted to BLS's algebraically minimal threshold
construction (Lagrange + G2-linearity, no nonce sampling, no MtA, no ZK).

- proofs/easycrypt/BLS_Threshold_N1.ec — Class N1 byte-equality reduction
- proofs/easycrypt/BLS_Threshold_N1_Refinement.ec — partial_sign + aggregate
- proofs/easycrypt/BLS_Threshold_N4.ec — DKG public-key preservation
- proofs/easycrypt/lemmas/BLS_Threshold_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/threshold/ — Jasmin scaffolds

BLS-threshold has the smallest formal-methods surface of the three
classical threshold protocols. Admit budget: 1/1 (same one-line
group-identity admit as FROST_N4, CGGMP21_N4, Pulsar_N4).

Production deployment note: ships with trusted-dealer keygen only;
DKG gap disclosed in SUBMISSION-STATUS.md §3.3.
2026-05-19 08:34:32 -07:00
..