P3.6.1 — VRF Stub (Leader Election) — Behavioral Contract

Step 2 of the 5-step chain. The audit (Step 1) confirmed a greenfield slice. This contract specifies exported symbols, signatures, runtime invariants, and the acceptance corpus that Step 5 (verify) measures against.

§1. Module surface

Module: src/domains/consensus/vrf-stub.ts

Exported symbols:

Symbol	Kind	Signature
VrfProvider	interface	{ eval(seed, input, privKey): VrfEvalOutput; verify(seed, input, output, proof, pubKey): boolean }
VrfEvalOutput	interface	{ readonly output: Buffer; readonly proof: Buffer }
HmacVrfProvider	class	implements VrfProvider (HMAC-SHA256)
defaultVrf	const	VrfProvider — module-level singleton, currently new HmacVrfProvider()
vrfEval	function	(seed: Buffer, input: Buffer, privKey: Buffer) => VrfEvalOutput
vrfVerify	function	(seed: Buffer, input: Buffer, output: Buffer, proof: Buffer, pubKey: Buffer) => boolean
selectLeader	function	(arbiters: readonly string[], seed: Buffer, round_id: bigint) => string
VrfError	class	extends Error — thrown on empty arbiters / malformed args

No state outside the defaultVrf singleton. No I/O. Zero Math.* / Date.* / network / DB / env / wall-clock / random / floating-point.

§2. vrfEval contract

Pure function — (Buffer, Buffer, Buffer) → VrfEvalOutput.

Computes:

output = HMAC-SHA256(privKey, seed || input)        # 32 bytes
proof  = HMAC-SHA256(privKey, output || seed)       # 32 bytes

Both Buffers are freshly allocated; the caller may inspect them without affecting subsequent calls. privKey is consumed only by createHmac; not retained, not exposed.

Preconditions:

• Buffer.isBuffer(seed) — false → VrfError('seed must be a Buffer')
• Buffer.isBuffer(input) — false → VrfError('input must be a Buffer')
• Buffer.isBuffer(privKey) — false → VrfError('privKey must be a Buffer')
• privKey.length >= 1 — empty key buffer → VrfError('privKey must be non-empty')

seed.length and input.length are unbounded; HMAC-SHA256 handles any byte length. Zero-length is permitted for both (produces a defined output).

Postconditions:

• output.length === 32
• proof.length === 32
• Determinism: vrfEval(seedA, inputA, kA) and vrfEval(seedB, inputB, kB) produce byte-identical outputs iff (seedA, inputA, kA) byte- equal (seedB, inputB, kB).

Delegation: vrfEval(...) is defaultVrf.eval(...). Phase 1.5 swap-in replaces defaultVrf only.

§3. vrfVerify contract

Pure function — (Buffer, Buffer, Buffer, Buffer, Buffer) → boolean.

For the HMAC stub, verification re-computes the same HMAC pair using pubKey as the symmetric key (in Option A pubKey ≡ privKey — the “keys” are symmetric secrets) and compares with timingSafeEqual.

expectedOutput = HMAC-SHA256(pubKey, seed || input)
expectedProof  = HMAC-SHA256(pubKey, output || seed)
return timingSafeEqual(expectedOutput, output)
    && timingSafeEqual(expectedProof, proof)

Preconditions:

• All five arguments are Buffers; non-Buffer → return false (defensive — verify is a query and should not throw on bad input from an attacker).
• output.length === 32 and proof.length === 32; mismatched lengths → false.
• pubKey.length >= 1; empty → false.

Postconditions:

• Returns true iff (output, proof) were produced by vrfEval(seed, input, pubKey).
• Returns false for any tampering with seed, input, output, proof, or pubKey.
• Constant-time on the equality compare (HMAC re-computation is not itself constant-time; this matches the Option A simplicity profile — Option B will be fully constant-time).

§4. selectLeader contract

Pure function — (readonly string[], Buffer, bigint) → string.

evalInput = utf8Bytes(round_id.toString())   # decimal-string canonical
{output}  = HmacVrfProvider.eval(seed, evalInput, seed)
idx       = output.readUInt32BE(0) % arbiters.length
return arbiters[idx]

Design note on the “key” choice: selectLeader uses seed as both the seed AND the private key parameter to eval. This intentionally turns the output into a publicly-derivable value — any party that knows seed and round_id can reproduce the selection. That matches the spec line next_leader = VRF(prev_merkle_root, round_id) in consensus.md §157, where every arbiter must agree on the same leader without any party holding a secret key. The secret-key flavor vrfEval(seed, input, privKey) remains available for ECVRF-style proofs in Phase 1.5; selectLeader is a separate public-output flavor documented as such in source. (The naming privKey is retained for API stability with future ECVRF.)

Preconditions:

• Array.isArray(arbiters) and arbiters.length >= 1 — arbiters.length === 0 → VrfError('arbiters must be non-empty')
• Every element of arbiters is a string (type-system enforced; no runtime check — TS contract).
• Buffer.isBuffer(seed) — false → VrfError.
• typeof round_id === 'bigint' — TypeScript enforced.

Postconditions:

• Returns one of arbiters (preserves caller-supplied identity).
• Determinism: same (arbiters, seed, round_id) always returns the same arbiter.
• Single-arbiter trivially: selectLeader(["A"], seed, r) returns "A" for any (seed, r) (no HMAC computed — fast path).
• Modulo bias is documented; for arbiters.length ≤ 1000 the statistical bias against the largest-index arbiter is bounded by arbiters.length / 2^32 < 2^-22. Negligible for Phase 0/Phase 5 arbiter sizes.

§5. VrfProvider interface contract

export interface VrfProvider {
  eval(seed: Buffer, input: Buffer, privKey: Buffer): VrfEvalOutput;
  verify(
    seed: Buffer,
    input: Buffer,
    output: Buffer,
    proof: Buffer,
    pubKey: Buffer,
  ): boolean;
}

Stable across Option A → Option B swap. No additional methods are added by Option B — RFC 9381 ECVRF has the same (seed, input, key) → (output, proof) shape, just with different internals.

Required implementations:

• HmacVrfProvider (this slice): symmetric HMAC-SHA256.
• NobleCurvesVrfProvider (Phase 1.5): RFC 9381 ECVRF-EDWARDS25519- SHA512-TAI atop @noble/curves.

Swap point: a single mutable assignment to defaultVrf (made readonly here, replaced in the Phase 1.5 commit). Callers use the function wrappers (vrfEval, vrfVerify) and never hold a reference to a concrete provider, so they survive the swap by definition.

§6. VrfError contract

export class VrfError extends Error {
  override readonly name = 'VrfError';
}

Thrown synchronously from vrfEval and selectLeader on precondition violation. Never thrown from vrfVerify (which always returns boolean).

§7. Determinism + crypto profile

Property	Status
Deterministic outputs	YES — HMAC-SHA256 is deterministic for fixed key+message
Externally verifiable	NO — explicit module-header warning; ADR-002 cited
Constant-time verify equality	YES — timingSafeEqual on 32-byte buffers
Constant-time HMAC	NO (out of scope for Option A; Option B will be)
No wall-clock	YES
No randomness	YES
No floating-point	YES — bigint round_id, Buffer keys, UInt32BE for index
Forbidden-token scan compliant	YES — verified by self-scan test

§8. Module-corpus invariant (forbidden-token self-scan)

Inherited from gossip-wire.test.ts / time-anchors.test.ts pattern: the source body of vrf-stub.ts (with JSDoc stripped) must not match any of:

• Math. (locale-dependent / non-deterministic)
• Date. (wall-clock)
• crypto. followed by an identifier (forces NAMED imports)
• Number( (number-coercion path; bigint-only)
• A floating-point literal regex (-?\d+\.\d+)

Test asserts these are absent.

§9. Acceptance criteria (test corpus, AC#1–AC#22)

Tests live in src/__tests__/domains/consensus/vrf-stub.test.ts. Each AC is a single test or a small group of expects under one test(...).

ID	Subject	Assertion
AC#1	vrfEval shape	output.length === 32 and proof.length === 32
AC#2	vrfEval determinism (10000×)	10000 calls with same (seed, input, privKey) produce byte-identical (output, proof)
AC#3	vrfEval collision-free over test range	10000 distinct (seed, input) pairs under one privKey → Set<hex>.size === 10000
AC#4	vrfEval key sensitivity	Two distinct privKey values on same (seed, input) produce distinct outputs
AC#5	vrfEval rejects non-Buffer seed	throws VrfError
AC#6	vrfEval rejects non-Buffer input	throws VrfError
AC#7	vrfEval rejects non-Buffer privKey	throws VrfError
AC#8	vrfEval rejects empty privKey	throws VrfError
AC#9	vrfEval accepts zero-length seed/input	returns 32+32 bytes
AC#10	vrfVerify roundtrip — correct key	returns true
AC#11	vrfVerify rejects wrong key	returns false
AC#12	vrfVerify rejects tampered output	returns false
AC#13	vrfVerify rejects tampered proof	returns false
AC#14	vrfVerify rejects tampered seed	returns false
AC#15	vrfVerify defensive — non-Buffer arg	returns false (does not throw)
AC#16	selectLeader determinism	same (arbiters, seed, round_id) → same arbiter, 1000×
AC#17	selectLeader single-arbiter	selectLeader(["A"], seed, r) === "A" for varied seeds/rounds
AC#18	selectLeader uniformity smoke	1000 round_ids over 4 arbiters → chi-squared statistic below 16.27 (loose 99% CI)
AC#19	selectLeader variable sizes	returns valid arbiter id for n ∈ {1, 2, 3, 4, 7, 10, 13, 100}
AC#20	selectLeader empty arbiters	throws VrfError
AC#21	VrfProvider interface	defaultVrf exposes eval + verify methods; HmacVrfProvider is instanceof a class that implements VrfProvider; function wrappers delegate through defaultVrf
AC#22	Module-corpus token scan	source body contains none of Math./Date./crypto.X/Number(/<floating-point-literal>

Sub-AC for header warning (AC#23): the source body contains the literal phrase “NOT RFC 9381” and “externally verifiable” inside the top-of-file JSDoc.

Target count: ~25 tests (some ACs share a single test block). Acceptable delta: +20–30 against baseline 2744.

§10. Constants used in the test corpus

For determinism across test runs, the test file uses fixed Buffers:

Symbol	Value	Source
K1	Buffer.alloc(32, 0x01)	Test-only private key
K2	Buffer.alloc(32, 0x02)	Distinct private key
SEED1	Buffer.alloc(32, 0x10)	Fixed seed
SEED2	Buffer.alloc(32, 0x20)	Distinct seed
INPUT1	Buffer.from('hello', 'utf8')	Fixed input
ARBITERS4	["A","B","C","D"]	4-arbiter committee for uniformity test

No process-level entropy. No crypto.randomBytes. No time. The chi- squared bound uses a loose threshold computed by hand (16.27 ≈ 99% CI for df=3); the test does not call any statistics library.

§11. Self-review

• No new npm dependency (@noble/curves deferred per ADR-002).
• All Buffer/bigint, zero floating-point.
• HMAC-SHA256 via NAMED imports (no crypto.X in body).
• Module header carries the RFC 9381 disclosure.
• VrfProvider interface present and swap-ready.
• defaultVrf re-exports through function wrappers — no caller coupling to HmacVrfProvider.
• selectLeader distribution test uses seeded inputs, not crypto.randomBytes.
• Empty-arbiters and bad-type cases throw VrfError (eval) or return false (verify).
• ADR-005 stub-shipping precedent honored.
• Module-corpus token scan covers Math./Date./crypto.X/ Number(/floating-point.

Ready for Step 3 (packet).