mirror of
https://github.com/luxfi/threshold.git
synced 2026-10-30 15:15:53 +00:00
zeekay
f4765ea61c
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).
46 lines
1.6 KiB
Plaintext
46 lines
1.6 KiB
Plaintext
// Single-party Ed25519 Sign (RFC 8032 §5.1.6).
|
|
//
|
|
// This file documents the call surface for the libjade port of
|
|
// single-party Ed25519. As of this submission, libjade does not yet
|
|
// provide Ed25519; the function below is a STUB documenting the
|
|
// expected signature. The Lux profile's CT story for Ed25519 inherits
|
|
// from `crypto/ed25519` (Go standard library) until a libjade port
|
|
// lands.
|
|
//
|
|
// Algorithm (RFC 8032 §5.1.6):
|
|
// 1. h = SHA-512(sk) // 64 bytes
|
|
// 2. s = clamp(h[0..32]) // scalar
|
|
// 3. prefix = h[32..64]
|
|
// 4. A = sB // compressed Edwards public key
|
|
// 5. r = SHA-512(prefix || M)
|
|
// 6. R = rB // compressed Edwards point
|
|
// 7. k = SHA-512(R || A || M) mod L
|
|
// 8. s' = (r + ks) mod L
|
|
// 9. sig = R || s' // 64 bytes
|
|
|
|
require "../lib/frost_params.jinc"
|
|
|
|
// sk: 32-byte Ed25519 secret seed (SECRET)
|
|
// pk: 32-byte Ed25519 public key (PUBLIC)
|
|
// msg: up to FROST_MAX_MSG bytes (PUBLIC)
|
|
// msg_len: actual message length in bytes (PUBLIC)
|
|
// sig: output 64-byte signature (PUBLIC)
|
|
//
|
|
// CT obligation: time + memory access independent of sk.
|
|
// Inherited from libjade SHA-512 + ed25519 point arithmetic
|
|
// (when those ship).
|
|
inline
|
|
fn ed25519_sign(
|
|
reg ptr u8[32] sk,
|
|
reg ptr u8[32] pk,
|
|
reg ptr u8[FROST_MAX_MSG] msg,
|
|
reg u64 msg_len,
|
|
reg ptr u8[FROST_SIG_BYTES] sig
|
|
) -> reg ptr u8[FROST_SIG_BYTES]
|
|
{
|
|
// TODO: jasmin implementation. Tracked in ../SUBMISSION-STATUS.md
|
|
// §3.5; until libjade ports Ed25519, Lux inherits CT posture from
|
|
// Go `crypto/ed25519`.
|
|
return sig;
|
|
}
|