Crypto wave 2: BLS12-381 signature scheme + field-multiply HW

[junjihashimoto]

Summary

Wave 2 of the Crypto HW/reference build-out (wave 1 = AES/Keccak/SHA-512/HKDF/RLP/Merkle HW, PR #80). Adds the BLS12-381 signature scheme (pure-data reference — the load-bearing addition) plus field-multiply HW for four curves.

Deliverable A — BLS12-381 (primary)

IP/Crypto/BLS12_381.lean (~640 LOC). BLS signatures on the
BLS12-381 pairing-friendly curve — the curve Ethereum 2.0 consensus
(validator aggregate signatures), zk-rollup proof verification, and
threshold-signature schemes are built on. Sparkle had no BLS /
pairing IP before this.

Full tower, layered like the existing Ed25519 tower:

Fp   — 381-bit base prime
Fp2  — Fp[u]/(u²+1)
Fp6  — Fp2[v]/(v³-ξ), ξ = u+1
Fp12 — Fp6[w]/(w²-v)   (pairing target group GT)
G1   — E(Fp): y² = x³ + 4                 (Jacobian)
G2   — E'(Fp2): y² = x³ + 4(u+1)          (the twist)
Pairing — optimal ate: Miller loop + final exponentiation
sign / verify / aggregate / verifyAggregate

• Pairing transcribed line-for-line from Ethereum's py_ecc
  optimized_bls12_381 (pseudo-binary loop encoding, D-type untwist
  ψ(x,y)=(x·w⁻², y·w⁻³), homogeneous-projective linefunc with
  num/den accumulation, full (p¹²−1)/r final exp). Verified
  bilinear + non-degenerate — the property that makes
  sign/verify work.
• Hash-to-curve (explicit in-file): real RFC 9380 §5.3
  expand_message_xmd(SHA-256) feeding a documented SIMPLE
  placeholder hashToG2 (scalar·generator), NOT the SSWU suite —
  so it is intentionally not blst/eth2-KAT interoperable. Clearly
  marked so nobody mistakes it for production H2C.
• Test (bls12381-test): Fp12 pairing bilinearity +
  non-degeneracy, sign→verify PASSES, tampered-sig /
  wrong-message / wrong-keyset REJECTED, 3-sig aggregate
  verifies. Self-consistency (documented), not third-party KAT.
• Out of scope (documented): pairing HW — 381-bit modmul + Miller
  loop on an FPGA is a research project. BLS's value here is the
  machine-checkable reference + IP-catalog presence.

Deliverable B — field-multiply HW (4 curves)

Bit-serial double-and-add modular multiply (MSB-first, per-bit
conditional-subtract reduction), each a circuit do FSM + sim
cross-check vs the pure-data mul + #synthesizeVerilog:

IP	file	prime	test
Goldilocks	GoldilocksHW.lean	2⁶⁴−2³²+1	goldilocks-mul-hw-test ✅
secp256k1	Secp256k1FieldHW.lean	2²⁵⁶−2³²−977	secp256k1-mul-hw-test ✅
P-256	P256FieldHW.lean	NIST P-256	p256-mul-hw-test ✅
Ed25519	Ed25519FieldHW.lean	2²⁵⁵−19	ed25519-mul-hw-test ✅

Ed25519's HW is the follow-up its own docstring promised ("the HW
engine … follows in L.2.b"). All four share one verified generic
shift-add mod-p skeleton (not Solinas/field-specific fast reduction —
that's a follow-up); each matches (a·b) mod p exactly.

Punted (as scoped): RSA-PSS HW (2048-bit modexp), point-op /
scalar-mul HW, pairing HW.

Verification (local)

• lake build clean — all #synthesizeVerilog compile.
• 5/5 new exes ALL PASS: bls12381-test,
  {goldilocks,secp256k1,p256,ed25519}-mul-hw-test.
• lake exe test: 13/13 lspec.
• 12 new #synthesizeVerilog invocations (3 per field HW).

New Sparkle-side limitation found

A @[reducible, inline] helper wrapping a Signal.mux over an
<*>-built comparison fails synth ("Cannot instantiate Seq.seq")
though it sim-passes — the conditional-subtract must be inlined
directly into the circuit do body. Also: use BitVec.ule (not
<=) and BitVec.append (0#k) v (not .setWidth) for
zero-extend. (Extends the gotcha inventory from PR #79/#80.)

CI wiring

lakefile.lean — 5 new lean_exe stanzas. Tests/AllTests.lean —
5 imports + .main calls (release-gate runner). Synth runs at
lake build; behavioural mains under lake test.