Audit — P3.2.1 Finality State Machine (5 levels)

Task: monotonic 5-level finality FSM (PENDING → SOFT → QUORUM → HARD → ABSOLUTE) gating external side effects. Branch: feature/p3-2-1-finality-sm Worktree: .worktrees/claude/p3-2-1-finality-sm Base: origin/main @ 498e6ea5 (post P3.1.2 BFT quorum). Spec source: docs/spec/s06-consensus.md §Finality levels. Concept source: docs/3-world/physics/laws/consensus.md §The five finality levels. Task prompt: docs/guides/implementation/task-prompts/p3.1-theta-consensus.md §P3.2.1 (L740-L919).

1. Surface inventory — pre-task

src/domains/consensus/ already ships:

File Origin Exports relevant to P3.2.1
messages.ts P3.1.1 (#234) Vote, Commit, Reveal, EquivocationProof, nextLogical, canonicalSerialize, signMessage, verifySignature, hashMessage. P3.2.1 imports Vote type only.
quorum.ts P3.1.2 (#237) quorumThreshold(n), hasQuorum(votes, n), voteGroupKey(v), detectDoubleVote. P3.2.1 consumes hasQuorum + voteGroupKey.
time-anchors.ts P3.4.1 (#235) STA broadcast/median — not consumed by P3.2.1.
gossip-wire.ts P3.3.1 (#236) IHAVE/IWANT — not consumed by P3.2.1.

Test scaffolding pattern — src/__tests__/domains/consensus/quorum.test.ts shows the established style: bigint LCG for property tests, makeVote helper, AC-numbered describe blocks, contract-source citations.

2. Spec & concept-doc cross-reference

s06 §Finality levels (lines 17-27)

Level Condition (s06) External effects (s06)
PENDING Event submitted None
SOFT Some votes, below quorum None
QUORUM votes ≥ threshold None (dispute window active)
HARD Quorum held for full dispute window (≥24h) Yes
ABSOLUTE HARD + no pending appeals Irreversible effects

Rule: no irreversible external side-effects before HARD finality.

consensus.md §The five finality levels (L42-L54)

Level What holds
PENDING Event received; no arbiter has voted
SOFT A single arbiter has signed
QUORUM quorum arbiters have signed the same root
HARD Two consecutive rounds have reached QUORUM without conflicting votes
ABSOLUTE Epoch-sealed: the round’s root is embedded in the next epoch’s genesis

consensus.md worked example (L118)

“Next round: if round 43 also reaches QUORUM without a conflicting reveal, round 42 transitions QUORUM → HARD. Epoch sealing later promotes it to ABSOLUTE.”

Task-prompt overrides

  • Dispute window: s06 says “≥24h”; task prompt §P3.2.1 says “100 epochs” (L764). The FSM does NOT run a wall timer (gotcha note L913-L915 in the source prompt) — dispute_window_epochs: bigint = 100n is configurable, default 100.
  • QUORUM→HARD trigger (gotcha L908-L912): “keep last round’s QUORUM evidence; on next round’s QUORUM, compare merkle_roots; if same and no equivocation observed between, transition to HARD. Otherwise stay at QUORUM and reset the counter.”

Resolution

The two spec sources are not contradictory once read together:

  • s06 framing — “Quorum held for full dispute window” — is the prose generalization.
  • consensus.md framing — “Two consecutive rounds have reached QUORUM without conflicting votes” — is the operationalization.
  • The task prompt formalizes “two consecutive rounds without conflicting reveal” as the runtime rule and uses 100-epoch dispute window as a parallel governance gate (after HARD, no rollback for 100 epochs before promotion to ABSOLUTE via epoch seal).

The implementation follows the task prompt’s operational rule as authoritative — backed by both concept doc L51 and L118.

3. Target API (from task prompt L788-L825) 

type FinalityLevel = "PENDING" | "SOFT" | "QUORUM" | "HARD" | "ABSOLUTE"
const FINALITY_ORDER: FinalityLevel[] = ["PENDING", "SOFT", "QUORUM", "HARD", "ABSOLUTE"]

class FinalitySM {
  constructor(round_id: bigint, n_arbiters: bigint, dispute_window_epochs: bigint = 100n)
  current(): FinalityLevel
  receiveVote(vote: Vote, currentEpoch: bigint): void
  sealEpoch(epoch: bigint, sealRoot: Buffer): void
  requireExternalEffectsAllowed(): void
  transitions(): Array<{from: FinalityLevel, to: FinalityLevel, epoch: bigint, evidence: Buffer}>
}

Errors:

  • FinalityRollbackError — thrown when monotonicity is violated.
  • PrematureExternalEffectError — thrown by requireExternalEffectsAllowed if current() < HARD.

4. Determinism & Phase 3 forbidden tokens

Per task prompt §Forbidden (L865-L870 of source plus the surrounding p3.1-theta-consensus.md §Forbidden tokens global block):

  • Math.*, Date.*, Math.random (already κ-forbidden)
  • number literals for round_id / epoch (bigint only)
  • floats anywhere
  • mutating state via getters
  • external side effects before HARD

The messages.ts source contains a forbidden-token self-scan; quorum.ts has one too. P3.2.1 will follow the same convention — a corpus self-scan test verifying finality.ts body contains none of Math., Date., Math.random, setTimeout, setInterval, process.hrtime, performance.now.

The FSM body has NO time reads, NO randomness, NO I/O. All inputs are caller-supplied bigints + Buffers.

5. Single-arbiter clause (task prompt L827-L832)

For n=1:

  • quorumThreshold(1n) === 1n (already proven in P3.1.2 corpus, AC#5).
  • First receiveVote → SOFT.
  • Same receiveVote (or vote group with cardinality 1) → QUORUM (because hasQuorum([v], 1n) === true).
  • Same group two rounds in a row → HARD.
  • sealEpoch → ABSOLUTE.

Trace:

new FinalitySM(round_id=1, n=1, window=100)
  current() === "PENDING"
  receiveVote(v_r1, epoch=10)
  current() === "QUORUM"     # n=1: SOFT and QUORUM coalesce
  # Note: transitions() shows PENDING→SOFT then SOFT→QUORUM as TWO entries
  # because the FSM walks one level per state-machine step
  receiveVote(v_r2, epoch=11)  # same root + rule_version_hash
  current() === "HARD"
  sealEpoch(12, sealRoot)
  current() === "ABSOLUTE"

Two interpretations resolve into one — the FSM steps through SOFT for ONE tick at n=1 (records the SOFT→QUORUM transition with the single-vote evidence) then advances. The “trivially within one round” semantics from L770 is enforced by the loop in receiveVote re-checking quorum after every vote.

6. Evidence types per transition (task prompt L771-L774)

Transition Evidence (Buffer encoding)
PENDING → SOFT canonical bytes of the triggering vote (canonicalSerialize(vote))
SOFT → QUORUM canonical bytes of the array of votes in the matching group (the votes that achieved quorum)
QUORUM → HARD canonical bytes of the pair {prev: <round-N votes>, curr: <round-N+1 votes>}
HARD → ABSOLUTE the sealRoot: Buffer passed to sealEpoch

Encoding reuses κ canonical-serialize via canonicalSerialize from messages.ts — round-trip stable per κ P1.5.4. Buffer fields inside the structure get the hex-rewrite pass via rewriteBuffersToHex (which is private but canonicalSerialize(vote_array) handles arrays of votes correctly because Vote is a plain object).

Wait — canonicalSerialize is typed ConsensusMessage | Vote, not Vote[]. The evidence for SOFT→QUORUM is a list. Solution: wrap into a plain object {votes: [...]} — this is a plain object whose values are arrays of plain Vote objects, both supported by rewriteBuffersToHex + κ canonicalize. However the exported canonicalSerialize signature won’t accept that wrapper at compile time. The FSM must use a local SHA-256 helper that hashes a Buffer concatenation, OR re-marshal evidence via a thin wrapper.

Decision: P3.2.1 implements its own encodeEvidence(value) helper INSIDE finality.ts that goes through κ canonicalize directly (it’s a public export of src/domains/rules/canonical.ts per the import in messages.ts L71). Buffer pre-rewrite is done locally to avoid coupling. This keeps the FSM module self-contained and avoids widening canonicalSerialize’s public type.

7. Monotonicity & error semantics (gotcha L916-L918)

“DO NOT silently ignore a downward attempt; throw a typed error.”

FinalityRollbackError extends Error with name = 'FinalityRollbackError'. Constructor takes from and to levels and produces a deterministic message string.

PrematureExternalEffectError similar pattern. Used by requireExternalEffectsAllowed; HARD and ABSOLUTE pass, the rest throw.

The FSM itself never produces a downward attempt; the throw is for misuse (e.g. caller subclass bug). Defensive guard implemented via private helper __advance(target: FinalityLevel) that verifies FINALITY_ORDER.indexOf(target) >= FINALITY_ORDER.indexOf(this.level) before mutating internal state.

8. State exposed via getters that DO NOT mutate (AC L775)

  • current() returns the current level (string enum value — immutable by JS semantics).
  • transitions() returns a fresh shallow copy of the internal transition log array (gotcha L919). Caller may not mutate internal state.

getters DO NOT mutate is satisfied trivially because the internal level is a string and the internal log is an array — the returned copies are detached.

9. Tests planned (acceptance criteria → test mapping)

AC Test
AC1: 5 levels, strict order FINALITY_ORDER shape assertion
AC2: PENDING→SOFT on first vote n=4, single vote → current() === 'SOFT'
AC3: SOFT→QUORUM via hasQuorum n=4, 3 matching votes → current() === 'QUORUM'
AC4: QUORUM→HARD on 2 consecutive round 1 quorum, round 2 quorum (same root+rule), no conflicting reveal → HARD
AC5: HARD→ABSOLUTE on sealEpoch seal → ABSOLUTE
AC6: Monotonicity rollback throws internal helper exercise via setLevelForTesting → throws FinalityRollbackError
AC7: requireExternalEffectsAllowed throws at PENDING/SOFT/QUORUM three asserts
AC8: requireExternalEffectsAllowed silent at HARD/ABSOLUTE two asserts
AC9: Single-arbiter n=1 trace full 5-level path with one vote per round
AC10: Evidence recorded per transition transitions() length === 4 after full traversal, every entry has epoch: bigint, evidence: Buffer non-empty
AC11: Conflicting reveal between rounds resets HARD counter round 1 quorum, round 1 equivocation observed, round 2 quorum → still QUORUM (not HARD)
AC12: 100-epoch dispute window dispute_window_epochs configurable; default 100; epoch gap between HARD and ABSOLUTE must be ≥ window for promotion
AC13: Different root in round N+1 resets counter r1 quorum at root_A, r2 quorum at root_B → still QUORUM
AC14: transitions() returns copy mutate returned array → internal log unchanged
AC15: Forbidden-token self-scan regex over compiled file body
AC16: 5-level full path PENDING→SOFT→QUORUM→HARD→ABSOLUTE in 4 transitions
AC17: nArbiters < 1n throws constructor invariant via QuorumError propagation

Total ≈ 25-40 test cases (L task estimate per packet).

10. Build / lint / test gates

  • npm run build — TypeScript strict check (errors must be zero).
  • npm run lint — ESLint with the project’s Phase 3 ruleset.
  • npm test — full Jest run; baseline 2818 passing + 1 pre-existing failure in reputation/tools.test.ts (better-sqlite3 schema issue — not in P3.2.1 scope). Expected delta: +25 to +40 (L task).

11. Out of scope

  • consensus_finality MCP tool — that’s P3.7.1 (next wave).
  • Persistence of FSM state — Phase 3 in-memory only; persistence to mcp_consensus_votes table (per consensus.md L197) is a later phase.
  • VRF leader rotation hookup — that’s P3.6.1 (parallel slice).
  • Wall-clock dispute window timer — explicitly out per gotcha L913-L915.
  • Multi-FSM coordination — one FSM = one round. Cross-round aggregation is consumer concern.

12. Approval

Step 1 of 5 complete. Proceeding to Step 2 (contract).

Back to top

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

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