zeekay f4765ea61c proofs/frost: Tier A EC theories + Lean bridges + Jasmin CT scaffolds ...

Adds the Tier A formal-artifact cluster for protocols/frost (Lux profile
of Komlo-Goldberg / IETF FROST). Mirrors luxfi/pulsar's Tier A structure
adapted to Schnorr threshold signing.

- proofs/easycrypt/FROST_N1.ec — Class N1 byte-equality reduction
- proofs/easycrypt/FROST_N1_Refinement.ec — round-1/2/combine refinement
- proofs/easycrypt/FROST_Ciphersuite_Ed25519.ec — Ed25519 ciphersuite
- proofs/easycrypt/FROST_Ciphersuite_Secp256k1_Taproot.ec — BIP-340 ciphersuite
- proofs/easycrypt/FROST_N4.ec — DKG public-key preservation
- proofs/easycrypt/lemmas/FROST_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

Plus shared scripts/check-high-assurance.sh that gates all three
protocols (frost, cmp, bls) at admit budget 1/1 with skip-friendly
jasminc and easycrypt invocations.

Admit budget: 1/1 (one-line group-identity admit in FROST_N4 closure).

2026-05-19 08:34:13 -07:00

..

FROST_CT.ec

proofs/frost: Tier A EC theories + Lean bridges + Jasmin CT scaffolds

2026-05-19 08:34:13 -07:00