mirror of
https://github.com/luxfi/threshold.git
synced 2026-10-30 15:15:53 +00:00
zeekay
1307d8d373
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).
42 lines
1.3 KiB
Plaintext
42 lines
1.3 KiB
Plaintext
// FROST transcript binding helpers (Lux profile).
|
|
//
|
|
// The Lux profile binds session transcripts via domain-separated
|
|
// SHA-512 (Ed25519) / tagged SHA-256 (secp256k1-Taproot). These are
|
|
// stubs documenting the call surface; concrete implementations live
|
|
// in the upstream single-party Jasmin libraries (libjade for SHA-256;
|
|
// upstream Ed25519 SHA-512 not yet ported).
|
|
|
|
require "frost_params.jinc"
|
|
|
|
// Tagged SHA-256 (BIP-340 §3.3): hash = SHA-256(SHA-256(tag) ||
|
|
// SHA-256(tag) || msg).
|
|
inline
|
|
fn frost_tagged_sha256(
|
|
reg ptr u8[32] tag_hash,
|
|
reg ptr u8[FROST_MAX_MSG] msg,
|
|
reg u64 msg_len,
|
|
reg ptr u8[32] out
|
|
) -> reg ptr u8[32]
|
|
{
|
|
// TODO: jasmin implementation (uses libjade SHA-256 absorb/finalize).
|
|
return out;
|
|
}
|
|
|
|
// SHA-512 absorb-finalize for Ed25519 transcript binding (RFC 8032
|
|
// §5.1.6 step 2). The Ed25519 single-party path computes
|
|
// k = SHA-512(R || A || PH(M)) mod L
|
|
// where PH = identity for Ed25519, identity for Ed25519ctx with the
|
|
// ctx prefix, or SHA-512 for Ed25519ph.
|
|
inline
|
|
fn frost_sha512(
|
|
reg ptr u8[FROST_MAX_MSG] msg,
|
|
reg u64 msg_len,
|
|
reg ptr u8[64] out
|
|
) -> reg ptr u8[64]
|
|
{
|
|
// TODO: jasmin implementation. libjade does not yet provide
|
|
// Ed25519 SHA-512; an upstream port is tracked in
|
|
// ../SUBMISSION-STATUS.md §3.5.
|
|
return out;
|
|
}
|