P3.5.1 — Equivocation Slasher — Behavioral Contract

Step 2 of the 5-step chain. The audit (Step 1) confirmed a greenfield slice consuming P3.1.1 + P3.1.2 + λ P2.2.2. This contract specifies behaviors, signatures, and the acceptance corpus that Step 5 measures against.

§1. Module surface

Module: src/domains/consensus/equivocation.ts

Exported symbols:

Symbol	Kind	Signature
EQUIVOCATION_BAND	const	SeverityBand — 'critical'
EQUIVOCATION_DOMAIN	const	Domain — 'arbitration'
VerifyEquivocationResult	type	{valid: true} \| {valid: false, reason: VerifyEquivocationReason}
VerifyEquivocationReason	type	'sig_a_invalid' \| 'sig_b_invalid' \| 'same_tuple' \| 'different_round_or_level'
ApplySlashResult	type	{applied: true, history_event} \| {applied: false, reason: ApplySlashReason}
ApplySlashReason	type	'invalid_proof' \| 'duplicate' \| 'lambda_double_jeopardy'
buildEquivocationProof	function	re-export from ./messages.js (one-line wrapper for ergonomic call-site)
verifyEquivocationProof	function	(proof, attackerPubKey) → VerifyEquivocationResult
evidenceHashHex	function	(proof) → string (lowercase hex of proof.evidence_hash)
applyEquivocationSlash	function	(args) → ApplySlashResult

No mutable module state. No I/O. Zero Math.* / Date.* / network / DB / env. The slasher is a pure layer — λ persistence and the idempotency Set are caller-owned.

§2. Constants

import { DAMAGE_CRITICAL } from '../rules/bps-constants.js';

/**
 * Equivocation maps to the `critical` severity band per
 * task-breakdown.md §P3.5.1 line 963 ("Slash amount: maps to `critical`
 * offense (8000bps loss)"). `damage_for('critical')` yields
 * `DAMAGE_CRITICAL = 8_000n`.
 */
export const EQUIVOCATION_BAND: SeverityBand = 'critical';

/**
 * Per consensus.md §147 ("hard scar on arbitration domain") and the
 * λ schema's five-domain enum (schema.ts §A): equivocation always
 * lands in the `arbitration` domain.
 */
export const EQUIVOCATION_DOMAIN: Domain = 'arbitration';

DAMAGE_CRITICAL is imported as a documentation anchor and surfaces in the JSDoc body so grep finds the constant; the slasher does not pass the raw bps value to λ (λ derives it from the band).

§3. verifyEquivocationProof(proof, attackerPubKey) contract

Pure function — (EquivocationProof, KeyObject) → VerifyEquivocationResult.

Defensive re-verification of a proof. Returns {valid: true} iff:

1. verifySignature(proof.signed_vote_a, attackerPubKey) === true
2. verifySignature(proof.signed_vote_b, attackerPubKey) === true
3. Tuples differ — at least one of merkle_root or rule_version_hash is non-equal between the two votes.
4. Same round_id in both votes (the spec’s “same finality level in the same round” condition reduces to same-round at the structural layer; vote_type is not checked because vote_type distinguishes ACCEPT/REJECT/ABSTAIN, not finality level).

On failure, returns {valid: false, reason} with the first failing check (short-circuit order: 1 → 2 → 3 → 4).

Reason codes:

Reason	Trigger
sig_a_invalid	verifySignature(vote_a, pubkey) === false
sig_b_invalid	verifySignature(vote_b, pubkey) === false
same_tuple	Both merkle_root AND rule_version_hash match by Buffer.compare === 0
different_round_or_level	signed_vote_a.round_id !== signed_vote_b.round_id

Notes:

• buildEquivocationProof (P3.1.1) already enforces these preconditions at construction time. verifyEquivocationProof is a stateless re-check for proofs that arrive over the wire — the wire could carry hand-crafted Buffers that bypass the constructor.
• attackerPubKey is a KeyObject per the P3.1.1 convention. The caller is responsible for resolving the public key from proof.attacker_id via whatever soul-vector index ξ provides.
• The function NEVER throws. Even a malformed proof structurally (e.g. zero-length signature) returns a valid: false result with the appropriate reason — Ed25519 verify returns false for malformed signatures rather than throwing.

§4. evidenceHashHex(proof) contract

Pure function — (EquivocationProof) → string.

Returns proof.evidence_hash.toString('hex'). Lowercase by Node spec. Stable across calls. Exported because the idempotency Set keys on this string and the test corpus inspects it.

§5. applyEquivocationSlash(args) contract

Pure function — (args) → ApplySlashResult.

export interface ApplySlashArgs {
  readonly proof: EquivocationProof;
  readonly attackerPubKey: KeyObject;
  readonly current_epoch: bigint;
  readonly attackerRow: ReputationRow;
  readonly history: readonly ReputationHistoryRow[];
  readonly alreadyApplied: Set<string>;
}

export type ApplySlashResult =
  | {
      readonly applied: true;
      readonly evidence_hash_hex: string;
      readonly next_row: ReputationRow;
      readonly history_event: Omit<ReputationHistoryRow, 'id'>;
    }
  | { readonly applied: false; readonly reason: ApplySlashReason };

Algorithm:

1. Compute evidence_hash_hex = evidenceHashHex(proof).
2. If alreadyApplied.has(evidence_hash_hex) → return {applied: false, reason: 'duplicate'}. No λ call.
3. Call verifyEquivocationProof(proof, attackerPubKey). If valid === false → return {applied: false, reason: 'invalid_proof'}.
4. Sanity-check the row: attackerRow.node_id === proof.attacker_id AND attackerRow.domain === 'arbitration'. Mismatch → throw a programming-error Error (NOT an ApplySlashResult — caller bug, not a domain failure).
5. Call apply_penalty(attackerRow, 'critical', current_epoch, evidence_hash_hex, 'EQUIVOCATION_PROVEN', history). If λ throws DoublePenaltyError, return {applied: false, reason: 'lambda_double_jeopardy'}.
6. Mutate alreadyApplied.add(evidence_hash_hex).
7. Return {applied: true, evidence_hash_hex, next_row, history_event}.

Order matters: the cheap alreadyApplied check fires BEFORE the expensive crypto verification, so repeated honest re-submissions stay fast. The crypto re-check is for first-time arrival; the Set guard is for replay.

Idempotency contract:

For a given (proof, attackerPubKey, current_epoch, attackerRow, history) tuple and a Set S:

• First call with S = ∅ → applied: true, S' = {evidence_hash_hex}.
• Second call with the same S' = {evidence_hash_hex} → applied: false, reason: 'duplicate'. No mutation of S'. No λ call.

Reason: lambda_double_jeopardy:

Defense-in-depth. If a caller persists slashing history and then later re-instantiates with a stale empty alreadyApplied Set, λ’s own DoublePenaltyError fires (because the history will already carry a band:critical|... row with the same event_id). The slasher catches this and returns the structured result rather than letting the error propagate.

The check ORDER (Set → verify → row sanity → λ) is part of the contract: verify-before-history-check means a tampered proof can’t waste λ time, and Set-before-verify means a known-good proof can’t re-trigger Ed25519.

§6. buildEquivocationProof re-export

P3.1.1 already exports buildEquivocationProof with a 6-arg signature that the slasher accepts. To keep call-sites tidy, this module re-exports it as-is:

export { buildEquivocationProof } from './messages.js';

Pure re-export. No type narrowing, no signature change. Tests can import from either location; the re-export exists for documentation purposes (the slasher is the canonical home for the “equivocation” concept).

§7. Invariants (asserted in tests)

I1. Pure — equivocation.ts has no global state, no I/O, no Math.* / Date.* / RNG / DB / env / network. Forbidden-token corpus scan covers the body. I2. No throws on the verify path — verifyEquivocationProof always returns a VerifyEquivocationResult. Only Buffer.compare and the crypto layer are touched; both are total functions for these shapes. I3. No double-slash via Set — first call with empty Set returns applied: true; second call returns applied: false, reason: 'duplicate'. Set is mutated on success only. I4. λ delegation honors the band/domain mapping — the history_event reason starts with band:critical|EQUIVOCATION_PROVEN, the event_id is the lowercase-hex evidence hash, the domain is arbitration, and the delta matches λ’s apply_penalty formula. I5. Constant amount — every successful slash deducts the SAME fraction of score (8000bps via damage_for('critical')). For attackerRow.score = 10000n the deduction is exactly 8000n, leaving next_row.score === 2000. I6. Single-arbiter clause — n=1 (single keypair) self-slash works: sign two distinct tuples with the same key in the same round, build proof, verify, apply slash → applied: true. The slasher does not enforce n. I7. No edits to λ surface — the slasher only imports apply_penalty + DoublePenaltyError + type SeverityBand from ../reputation/penalties.js. It does NOT redefine, override, or extend any λ export. I8. Verification ordering — verify reason codes short-circuit in declaration order: sig_a_invalid > sig_b_invalid > same_tuple > different_round_or_level.

§8. Acceptance corpus (Step 5 will measure these)

ID	Property	Count
AC#1	verifyEquivocationProof happy path (valid proof)	1
AC#2	verifyEquivocationProof sig_a tampered → sig_a_invalid	1
AC#3	verifyEquivocationProof sig_b tampered → sig_b_invalid	1
AC#4	verifyEquivocationProof wrong pubkey for sig_a → sig_a_invalid	1
AC#5	verifyEquivocationProof same tuple → same_tuple	1
AC#6	verifyEquivocationProof different round_id → different_round_or_level	1
AC#7	verifyEquivocationProof short-circuit order (sig_a invalid AND same_tuple → returns sig_a_invalid first)	1
AC#8	verifyEquivocationProof never throws (malformed sig length)	1
AC#9	evidenceHashHex returns lowercase 64-char hex	1
AC#10	evidenceHashHex is stable across calls	1
AC#11	applyEquivocationSlash happy path → applied: true, score 10000 → 2000	1
AC#12	applyEquivocationSlash Set guard → second call returns duplicate	1
AC#13	applyEquivocationSlash invalid proof → invalid_proof (no λ call)	1
AC#14	applyEquivocationSlash λ double-jeopardy → lambda_double_jeopardy	1
AC#15	applyEquivocationSlash history_event reason has band:critical| prefix	1
AC#16	applyEquivocationSlash history_event event_id === evidence_hash_hex	1
AC#17	applyEquivocationSlash history_event domain === arbitration	1
AC#18	applyEquivocationSlash next_row.ban_until_epoch set to current_epoch + 100 (band=’critical’ triggers ban)	1
AC#19	applyEquivocationSlash row sanity-check throws on node_id mismatch	1
AC#20	applyEquivocationSlash row sanity-check throws on wrong domain	1
AC#21	Single-arbiter clause: n=1 self-equivocation builds + slashes	1
AC#22	EQUIVOCATION_BAND === 'critical' (constant guard)	1
AC#23	EQUIVOCATION_DOMAIN === 'arbitration' (constant guard)	1
AC#24	DAMAGE_CRITICAL import is grep-able in the source body	1
AC#25	Integration: detectDoubleVote pair → buildProof → verify → slash	1
AC#26	Integration: re-slash same pair via Set → duplicate	1
AC#27	Forbidden-token corpus scan (Math./Date./Math.random)	1
AC#28	buildEquivocationProof is re-exported and callable	1

Expected new tests: 28 grouped specs across ~25 it() blocks. Target delta against the 2744 baseline: +25.

§9. Out of scope

• VRF leader election (P3.6.x).
• Reputation history persistence (insertHistoryEvent is caller’s responsibility per λ P2.1.1 invariant).
• π suspension flow (“escalated to π for potential suspension” — Phase 6).
• Multi-arbiter slashing concurrency control (DB-level row locking).
• Network propagation of equivocation proofs (P3.3.x gossip).
• View-change trigger on equivocation_observed reason — P3.1.3 consumes applyEquivocationSlash output; the slasher itself does not emit ViewChange messages.

§10. Implementation notes (for Step 3 packet)

• Use Buffer.compare(a, b) === 0 (not .equals — both work, but P3.1.1 uses Buffer.compare so we match the convention).
• Catch DoublePenaltyError by instanceof check; rethrow other Error subclasses. λ may throw TypeError from damage_for if band is malformed — that is a programming error and propagates up.
• verifySignature in P3.1.1 throws on EquivocationProof (msg_type check) but not on Vote — votes are the only shape passed in.
• Use named function declarations, not arrows, for the four exports (matches P3.1.1 / P3.1.2 style).
• File header comment style: match P3.1.2 (canonical refs + invariants
  • forbidden-token note).