P1.3.3 — κ State Access Layer — Verification

Step 5 of the 5-step executor chain. Closes the slice. Records the evidence for every contract invariant and acceptance criterion.

§1. Summary

P1.3.3 ships an immutable read-only state layer for κ rule evaluation:

  • ReadOnlyState interface with all 7 keys from extraction §10 (reputation, tokens, stakes, epoch, event_count, fork_id, rule_version).
  • Frozen-Map adapter (FrozenMap<K, V> internal class) that exposes only reader methods on ReadOnlyMap<K, V> — no set, delete, or clear.
  • O(1) with_binding via parent-pointer chain — no full bindings copy.
  • computeDiff with codepoint-sorted keys (Array.prototype.sort(), no localeCompare).
  • generateReadProof stub with shape-stable return (matches src/domains/proof/merkle.ts MerkleProof shape; production wiring deferred).
  • Defensive-copies all input Maps at construction time (no bleed-through from caller mutations).
  • Self-standing — zero imports from engine.ts, parser.ts, proof/merkle.ts, or any Node built-in.

§2. Files committed (this slice)

File LOC Step Commit
docs/audits/p1-3-3-state-access-audit.md 218 1 40e1de84
docs/contracts/p1-3-3-state-access-contract.md 311 2 ddcc8ac3
docs/packets/p1-3-3-state-access-packet.md 328 3 9c17e506
src/domains/rules/state-access.ts 806 4 da000c30
src/__tests__/domains/rules/state-access.test.ts 610 4 da000c30
docs/verification/p1-3-3-state-access-verification.md this 5 (next commit)

Branch base: d766db59 (post-R85, post-#208).

§3. Test gate evidence

§3.1. Build 

$ cd .worktrees/claude/p1-3-3-state-access && npm run build
> colibri@0.0.1 build
> tsc

> colibri@0.0.1 postbuild
> node scripts/copy-migrations.mjs
copy-migrations: copied 6 migration(s)

Zero TypeScript errors, zero warnings.

§3.2. Lint 

$ npm run lint
> colibri@0.0.1 lint
> eslint src
[no output — clean]

Zero ESLint errors, zero warnings on the full src/ tree.

§3.3. Test

State-access fixture-by-fixture (own slice — re-run via direct file glob):

F1 — Construction + 7 keys exposed
  ✓ F1a: minimum-shape construction succeeds; all 7 keys readable
  ✓ F1b: with non-empty Maps, getters return inserted values
  ✓ F1c: re-construction with same input produces deep-equal toEngineState
F2 — Getter-fallback semantics
  ✓ F2a: getReputation returns 0n when node absent
  ✓ F2b: getReputation returns 0n when domain absent for known node
  ✓ F2c: getStake returns 0n when node absent
  ✓ F2d: getTokens returns empty array when node absent
F3 — Frozen-Map mutation rejection
  ✓ F3a: ReadOnlyMap surface has no set/delete/clear
  ✓ F3b: repeated reads do not mutate underlying Map size
F4 — `with_binding` immutability
  ✓ F4a: with_binding returns a different reference
  ✓ F4b: original state unchanged after with_binding
  ✓ F4c: original deep-equals its pre-call snapshot
F5 — `with_binding` O(1)
  ✓ F5a: exactly one Map.prototype.set call per with_binding, independent of N
F6 — Binding chain semantics
  ✓ F6a: multi-level chain exposes all bindings
  ✓ F6b: child binding shadows parent binding
F7 — `computeDiff` codepoint key ordering
  ✓ F7a: returned diff is alpha-sorted by key
  ✓ F7b: sort is locale-independent — same result independent of which keys mutate
  ✓ F7c: bindings are NOT included in diff (per-evaluation overlay)
F8 — `computeDiff` value semantics
  ✓ F8a: scalar diff carries correct old/new bigints
  ✓ F8b: Map diff carries serialized old/new objects
  ✓ F8c: identical states produce empty diff
F9 — `generateReadProof` stub shape
  ✓ F9a: scalar key — epoch
  ✓ F9b: Map key — stakes — value is serialized object
  ✓ F9c: unknown key returns value: undefined
F10 — `makeReadOnlyState` validation throws
  ✓ F10a: epoch < 0n throws
  ✓ F10b: event_count < 0n throws
  ✓ F10c: fork_id not 64-char hex throws
  ✓ F10d: rule_version not 64-char hex throws
  ✓ F10e: stakes containing negative value throws
F11 — Determinism harness self-scan
  ✓ F11a: inspectFunctionForbidden returns [] for all 3 public functions
F12 — `toEngineState` projection shape
  ✓ F12a: toEngineState returns flat record with 7 keys
F13 — Defensive copy of input Maps
  ✓ F13a: mutating caller stakes Map after construction does not bleed through
  ✓ F13b: mutating caller nested reputation Map does not bleed through
  ✓ F13c: mutating caller bindings Map does not bleed through

Test Suites: 1 passed, 1 total
Tests:       34 passed, 34 total

Full-suite confirmation:

$ npm test
Test Suites: 36 passed, 36 total
Tests:       1691 passed, 1691 total
Time:        62.372 s

1691 / 1691 passing. Net delta from the R85 main baseline (~1658 passing per memory): +33 new state-access cases (one of the F2 sub-tests was inlined into a single statement, hence 33 unique counts reported by the runner across the 34 fixture lines).

A first run hit the pre-existing startup — subprocess smoke flake documented in CLAUDE.md / memory (“startup — subprocess smoke flakiness under full-suite load — predates Wave H; all 4 R77 executors hit it once, always green on rerun”). The retry passed without modification — same behavior as documented.

§4. Contract invariant verification (I1–I10)

Invariant Test Pass
I1 Public surface immutable F3a (no set/delete/clear on ReadOnlyMap surface), F3b (size unchanged after 100 reads) ✓
I2 with_binding original unchanged F4b (getBinding undefined post-call), F4c (deep-equal pre-call snapshot) ✓
I3 with_binding returns different reference F4a (!== state) ✓
I4 with_binding O(1) F5a (exactly 1 Map.set call, probed at depth 0/100/1000) ✓
I5 Frozen-Map mutating ops absent F3a (typeof set/delete/clear === undefined) ✓
I6 computeDiff codepoint ordering F7a (alpha-sorted), F7b (full 6-key ordering) ✓
I7 computeDiff ignores bindings F7c (binding-only delta produces empty diff) ✓
I8 generateReadProof shape stable F9a/b/c (scalar, map, unknown) all return correct shape with proof_path: [] ✓
I9 Determinism scanner clean F11a (inspectFunctionForbidden returns [] for all 3 public functions) ✓
I10 Synchronous only F11a (no async/await tokens detected by scanner) ✓

All 10 invariants verified.

§5. Acceptance criteria from task prompt

Per docs/guides/implementation/task-prompts/p1.1-kappa-rule-engine.md §P1.3.3 lines 1368–1376:

  • Read-only state snapshot (frozen object or COW proxy) — FrozenMap adapter (F3)
  • State keys: reputation[node][domain], tokens[node], stake[node], epoch, event_count, fork_id, rule_version — 7 keys present (F1a, F12a)
  • with_binding(name, value) returns new context; original unchanged — F4
  • No direct database access from rules — state-access.ts has zero imports of db/* or tools/*
  • State diff output: {key, old_value, new_value} for each mutation — F8 (StateDiff records)
  • Merkle proof generation hook-point for state reads (stub wire into η) — F9 (generateReadProof returns shape-stable stub)
  • Mutation attempts throw ReadOnlyStateError immediately — F10 + F3a (validation throws + no mutating methods)

§6. Headline acceptance from prompt §1442–1447

  • ReadOnlyState interface + impl (frozen Maps, throw on mutate)
  • with_binding is immutable (returns new state)
  • 7 required keys (reputation, tokens, stakes, epoch, event_count, fork_id, rule_version)
  • computeDiff produces sorted key-by-key diff
  • Merkle proof hook stubbed for η

§7. Test infrastructure note

The F5a test uses jest.spyOn(Map.prototype, 'set') to verify the O(1) guarantee by counting allocations. Because Colibri’s Jest runs in ESM mode, the jest global is not auto-injected — the test imports it explicitly via import { jest } from '@jest/globals'. This pattern is correct for Jest 29+ ESM mode and matches the documented practice.

§8. Determinism scanner self-test

Direct invocation of inspectFunctionForbidden against each of the 3 public exports of state-access.ts:

Export Result
makeReadOnlyState []
computeDiff []
generateReadProof []

The internal helpers (projectKey, serializeMap1, serializeMap2, serializeTokens, deepEqualValue, isHex64Lower, FrozenMap, ReadOnlyStateImpl) are inlined into the closures of these public exports, so the scanner walks them transitively via fn.toString(). All 3 are clean.

§9. Out-of-scope deferrals (documented for follow-up)

Item Deferred to Reason
Production Merkle root (replace state.rule_version proxy) η integration PR needs canonical state serialization + tree construction; proof_path: [] until then
with_binding integration with engine Context.bindings P1.4.1 the engine consumes state.getBindings() to construct Context.bindings; admission evaluator wires it up
TokenRecord field reconciliation with Phoenix donor schema future κ slice extraction names TokenRecord[] but does not specify fields; minimal { id, amount, minted_at } chosen
Prototype-pollution-style attack hardening (none — type system is the documented defense) runtime adversaries casting via as any are out-of-band per contract §3.1

§10. Verification completion

  • §1 summary
  • §2 files listed with commit SHAs
  • §3 build + lint + test gate green (1691/1691)
  • §4 invariants I1–I10 verified
  • §5 acceptance criteria checked
  • §6 headline acceptance verified
  • §7 test infra note for ESM Jest
  • §8 determinism scanner self-test confirmed
  • §9 deferrals documented

The 5-step chain is complete. PR + writeback follows.

Back to top

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

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