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— propagatesQuorumErrorfromquorumThresholdon 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 snapshotslastQuorumEvidence: {epoch: A, triple: <key>}. - The FSM advances to a “new round” by accepting votes with a different
round_id-context — actually, more precisely:receiveVotecarriescurrentEpoch. WhencurrentEpoch > lastQuorumEvidence.epochANDhasQuorumis true ANDvoteGroupKey(achievingGroup[0]) === lastQuorumEvidence.tripleANDequivocationObservedSinceLastQuorum === 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
HARDandABSOLUTE: silent no-op (returns void). - At levels
PENDING,SOFT,QUORUM: throwsPrematureExternalEffectErrorwith 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,setImmediateprocess.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
receiveVoteafter ABSOLUTE are silent no-ops (the round is sealed). - Calls to
sealEpochafter 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
currentEpochprogression 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 aVote-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).