Contract — P3.2.1 Finality State Machine

Module: src/domains/consensus/finality.ts Test: src/__tests__/domains/consensus/finality.test.ts Type: pure, in-memory, single-round FSM.


1. Module shape

Type exports

export type FinalityLevel =
  | 'PENDING'
  | 'SOFT'
  | 'QUORUM'
  | 'HARD'
  | 'ABSOLUTE';

export const FINALITY_ORDER: readonly FinalityLevel[] = [
  'PENDING',
  'SOFT',
  'QUORUM',
  'HARD',
  'ABSOLUTE',
] as const;

export interface Transition {
  readonly from: FinalityLevel;
  readonly to: FinalityLevel;
  readonly epoch: bigint;
  readonly evidence: Buffer;
}

Class

export class FinalitySM {
  constructor(
    round_id: bigint,
    n_arbiters: bigint,
    dispute_window_epochs?: bigint /* default 100n */,
  );
  current(): FinalityLevel;
  receiveVote(vote: Vote, currentEpoch: bigint): void;
  observeEquivocation(epoch: bigint): void;
  sealEpoch(epoch: bigint, sealRoot: Buffer): void;
  requireExternalEffectsAllowed(): void;
  transitions(): readonly Transition[];
}

Error classes

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

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

Constructor preconditions

  • round_id >= 0n — round identifier (audit only).
  • n_arbiters >= 1n — propagates QuorumError from quorumThreshold on violation.
  • dispute_window_epochs >= 1n — minimum 1 to enable any ABSOLUTE promotion.

2. Transition rules

PENDING → SOFT

Trigger: first call to receiveVote(v, currentEpoch) while at PENDING. Evidence: encodeEvidence({ tag: 'soft', vote: v }) — canonical bytes of the triggering vote.

SOFT → QUORUM

Trigger: after each receiveVote, the FSM re-checks hasQuorum(allReceived, n_arbiters). If true, advance. Evidence: encodeEvidence({ tag: 'quorum', votes: <matching-group> }) — the votes whose (round_id, merkle_root, rule_version_hash) triple matches the achieving group (largest group by voteGroupKey).

Caveat: hasQuorum does NOT deduplicate by sender_id — the FSM does. P3.2.1 keeps a Map<senderId, Vote> for the current round so two votes from the same arbiter on the same triple count as one. The FSM stores only the FIRST vote per sender_id and ignores subsequent matching ones.

QUORUM → HARD

Trigger: a subsequent epoch’s vote stream re-achieves QUORUM on the SAME (merkle_root, rule_version_hash) triple AND no observeEquivocation was recorded between the two QUORUM moments.

Operationalization (gotcha L908-L912):

  • When the FSM enters QUORUM in currentEpoch_A, it snapshots lastQuorumEvidence: {epoch: A, triple: <key>}.
  • The FSM advances to a “new round” by accepting votes with a different round_id-context — actually, more precisely: receiveVote carries currentEpoch. When currentEpoch > lastQuorumEvidence.epoch AND hasQuorum is true AND voteGroupKey(achievingGroup[0]) === lastQuorumEvidence.triple AND equivocationObservedSinceLastQuorum === false, transition to HARD.
  • If a different triple wins quorum in a later epoch, OR an equivocation was observed since last QUORUM, the FSM stays at QUORUM and resets the triple snapshot to the new winning group.

Evidence: encodeEvidence({ tag: 'hard', prev: <prev-quorum-evidence>, curr: <curr-quorum-evidence> }).

HARD → ABSOLUTE

Trigger: sealEpoch(epoch, sealRoot) called while at HARD AND epoch - hardEpoch >= dispute_window_epochs.

Evidence: encodeEvidence({ tag: 'absolute', sealRoot: sealRoot }).

If sealEpoch is called when current level is HARD but dispute window has not elapsed (epoch < hardEpoch + window), the call is a no-op (silent — sealing of an in-window epoch is informational). The FSM does NOT throw; the seal is recorded only if it crosses the threshold.

If sealEpoch is called below HARD (PENDING/SOFT/QUORUM), it is a no-op (no promotion possible). The FSM does NOT throw because epoch sealing is an externally-driven event that the FSM does not control.


3. observeEquivocation

observeEquivocation(epoch: bigint): void;

Externally invoked — the equivocation handler (P3.5.x) calls this when an equivocation proof is constructed for THIS round. The FSM records:

  • equivocationObservedSinceLastQuorum = true

This blocks the next QUORUM→HARD promotion. The FSM does NOT roll back from QUORUM — that would violate monotonicity. It simply refuses to climb to HARD until a fresh QUORUM moment after the equivocation has been processed downstream.

epoch is recorded for audit but does not affect transitions.

Calling observeEquivocation does NOT itself add a transition entry.


4. requireExternalEffectsAllowed

requireExternalEffectsAllowed(): void;
  • At levels HARD and ABSOLUTE: silent no-op (returns void).
  • At levels PENDING, SOFT, QUORUM: throws PrematureExternalEffectError with message "external effects forbidden at <level>".

This is the public gate that consensus consumers MUST call before producing irreversible side effects (per consensus.md L54 and s06 L27).


5. Monotonicity invariant

For any time t > 0, FINALITY_ORDER.indexOf(level_t) >= FINALITY_ORDER.indexOf(level_{t-1}). The implementation enforces this via a private __advance(target: FinalityLevel) helper that throws FinalityRollbackError if idx(target) < idx(current).

External callers cannot trigger rollback because the only mutators (receiveVote, observeEquivocation, sealEpoch) only ever move up. The throw is for defensive coverage — if a future refactor introduces a setter, the guard fires.


6. transitions()

Returns a shallow copy of the internal Transition[] log. The returned array is a NEW array; the contained Transition objects are the SAME references (transitions are immutable per the interface readonly). Mutating the returned array (e.g. push, pop, splice) does NOT affect the FSM’s internal log.

Order: chronological by insertion.

After a full PENDING→SOFT→QUORUM→HARD→ABSOLUTE traversal, length === 4.


7. Internal state model

class FinalitySM {
  private readonly round_id: bigint;
  private readonly n_arbiters: bigint;
  private readonly dispute_window_epochs: bigint;

  private level: FinalityLevel = 'PENDING';
  private readonly votesBySender: Map<string, Vote> = new Map();
  private lastQuorumEvidence: { epoch: bigint; triple: string; votes: readonly Vote[] } | null = null;
  private equivocationObservedSinceLastQuorum: boolean = false;
  private hardEpoch: bigint | null = null;
  private readonly transitionLog: Transition[] = [];
}

Inputs to mutators are caller-provided bigints / Buffers / Votes. No clock reads. No randomness. No I/O. No console output. The FSM is a pure event-driven state machine.


8. Determinism / forbidden tokens

Module body must not contain (per Phase 3 corpus self-scan):

  • Math.* (Math.random, Math.floor, etc.)
  • Date.* (Date.now, new Date)
  • setTimeout, setInterval, setImmediate
  • process.hrtime, performance.now
  • async/await, Promise constructors
  • floats (0., .0, 1e0, etc.) outside of comments

A self-scan test loads the compiled finality.js file and asserts none of the patterns appear in the source body (JSDoc-stripped).


9. Test plan (acceptance criteria with traceable IDs)

AC# Description Test name
AC#1 FINALITY_ORDER is ['PENDING','SOFT','QUORUM','HARD','ABSOLUTE'] exactly FINALITY_ORDER has 5 levels in canonical order
AC#2 Initial level is PENDING new FSM starts at PENDING
AC#3 PENDING→SOFT on first vote receiveVote at n=4: first vote transitions to SOFT
AC#4 SOFT→QUORUM at threshold receiveVote at n=4: 3rd matching vote transitions to QUORUM
AC#5 Same-sender duplicate vote ignored receiveVote at n=4: two votes from same sender count as one
AC#6 QUORUM→HARD on 2 consecutive matching epochs QUORUM held two consecutive epochs same triple → HARD
AC#7 Different triple in epoch 2 resets HARD candidacy different triple in epoch 2: stays QUORUM, snapshot updated
AC#8 observeEquivocation blocks HARD equivocation between QUORUM moments: stays QUORUM
AC#9 HARD→ABSOLUTE on sealEpoch after dispute window sealEpoch at HARD + 100 epochs: transitions to ABSOLUTE
AC#10 sealEpoch before dispute window is no-op sealEpoch at HARD + 50 epochs: stays HARD, no transition
AC#11 sealEpoch below HARD is no-op sealEpoch at QUORUM: stays QUORUM, no transition
AC#12 Monotonicity: rollback throws __advance to lower level throws FinalityRollbackError (defensive) — exercised via a test-only setLevel that wraps __advance
AC#13 requireExternalEffectsAllowed throws at PENDING/SOFT/QUORUM three cases throw PrematureExternalEffectError
AC#14 requireExternalEffectsAllowed silent at HARD/ABSOLUTE two cases return undefined
AC#15 Single-arbiter n=1 full trace n=1: full PENDING→SOFT→QUORUM→HARD→ABSOLUTE with 4 transitions logged
AC#16 transitions() returns copy mutate returned array: internal log unchanged
AC#17 Each transition has bigint epoch + non-empty Buffer evidence shape assertion on full traversal
AC#18 Constructor with n_arbiters=0 throws QuorumError propagated from quorumThreshold
AC#19 Constructor with default 100-epoch window new FSM(1, 4) === new FSM(1, 4, 100n) semantics — window param defaults to 100n
AC#20 Custom dispute window honored new FSM(1, 4, 50n): HARD→ABSOLUTE at hardEpoch+50
AC#21 Forbidden-token self-scan finality.ts body uses none of κ-forbidden tokens
AC#22 5-level full path counts to 4 transitions length assertion
AC#23 observeEquivocation does NOT add a transition entry length assertion
AC#24 Vote with round_id mismatching FSM round_id is rejected receiveVote with foreign round_id: throws or silently skipped — chosen: silently skipped (caller filters; we record only matching round)
AC#25 Evidence buffer round-trips through canonical encoding the bytes for two identical inputs are byte-equal

Out-of-scope clarifications

  • ABSOLUTE is terminal — no further transitions. Calls to receiveVote after ABSOLUTE are silent no-ops (the round is sealed).
  • Calls to sealEpoch after ABSOLUTE are silent no-ops.
  • The FSM is single-round; cross-round logic (e.g. “the next round” in consensus.md L118) is encoded purely as currentEpoch progression INSIDE the same FSM. A second round’s votes share the same FSM instance for this design.

10. Wire reuse from messages.ts

P3.2.1 uses:

  • import type { Vote } from './messages.js'
  • import { canonicalSerialize } from './messages.js' — for evidence encoding (which works because we wrap evidence in a Vote-typed value when possible; for multi-vote evidence we use a thin local wrapper).

Actually, on second look, canonicalSerialize is typed ConsensusMessage | Vote. Multi-vote evidence won’t typecheck through it. Instead, P3.2.1 imports canonicalize from ../rules/canonical.js directly (same pattern messages.ts itself uses internally) AND replicates the local Buffer-to-hex pre-pass in a private helper __encodeEvidence.

Trade-off: __encodeEvidence is 15-20 LOC of duplication vs. importing private internals. Choosing duplication for module isolation. The pre-pass is small and self-evident; coupling to a private API is worse.


11. Performance

  • Constructor: O(1).
  • receiveVote: O(V) where V is total votes received (re-counts on every call; could be O(1) with incremental counts but Phase 3 explicitly trades for clarity).
  • current(): O(1).
  • transitions(): O(T) — copy of T-length log (T ≤ 4 in normal life).
  • requireExternalEffectsAllowed: O(1).

V is bounded by the arbiter count plus benign double-broadcast. For typical Phase 3 deployment (n ≤ 13 per consensus.md L34), V is tiny.


12. Approval

Step 2 of 5 complete. Proceeding to Step 3 (packet).


Back to top

Colibri — documentation-first MCP runtime. Apache 2.0 + Commons Clause.

This site uses Just the Docs, a documentation theme for Jekyll.