Kernel Closure — Dual-Layer Verification Scaffold

Why This Matters

The SpeyBooks kernel doctrine requires every Class M invariant to be enforced by at least two independent layers — a database layer and a verification layer — so that no single failure point can silently compromise financial correctness. M1 through M3 delivered the database enforcement side: constraints, triggers, RLS policies, and domain types. What was absent was the verification side: executable proof scripts that independently confirm each invariant holds, both structurally and against live data.

This release delivers that missing layer. Four verification scripts and a coverage gate script now mechanically prove every delivered axiom — rounding correctness, double-entry conservation, RLS mutation containment, monetary domain integrity, and typed error semantics — and the coverage gate enforces that no future axiom can be marked delivered without satisfying both layers. The gate ran for the first time at the end of this session and reported zero violations across all 17 delivered axioms.

Verification Scripts Delivered

Monetary constraints (AX-RND-001..005, AX-MON-002)

Twelve checks confirming that the canonical rounding functions are present with exact signatures, that all monetary CHECK constraints are installed and validated, that every constraint references the canonical arithmetic function, and that zero live rows violate any monetary invariant. Covers gross conservation, VAT derivation, net pipeline correctness, VAT sign polarity, and NULL prohibition on monetary columns.

Enforced by: verification script — Class M Tests layer. Proof: scripts/verify-monetary-constraints.sql — 12/12 checks passed.

Double-entry conservation (AX-ALG-001)

Six checks confirming that the balance enforcement function exists with exact signature, that the constraint trigger is present, deferred, and invokes the correct function, that the monetary column uses the canonical pence domain, and that zero posted transactions violate the conservation invariant. Includes phantom transaction detection and NULL amount guard.

Enforced by: verification script — Class M Tests layer. Proof: scripts/verify-double-entry.sql — 6/6 checks passed.

RLS mutation containment (AX-TEN-002)

Five checks confirming that all UPDATE RLS policies carry both USING and WITH CHECK clauses, and that WITH CHECK equals USING exactly — not merely that both sides reference the tenant column, but that the write predicate is identical to the read predicate. This closes the cross-tenant reassignment vector at the proof layer.

Enforced by: verification script — Class M Tests layer. Proof: scripts/verify-rls-policy-symmetry.sql — 5/5 checks passed, 25 UPDATE policies verified.

Typed error codec (AX-ERR-001)

Enumerates all 72 CHECK constraints in the accounting schema and confirms each has a typed entry in the constraint error map. Fails the build if any constraint is unmapped. This converts the error codec from a static code artefact to a mechanically verified coverage guarantee.

Enforced by: coverage gate — Class M Tests layer. Proof: scripts/constraint-coverage-check.sh — 72/72 constraints mapped.

Deterministic Constraint Error Codec

The previous error handler resolved database violations by substring-matching raw PostgreSQL error messages — a brittle pattern vulnerable to message text changes and incapable of distinguishing constraint semantics. This has been replaced by a deterministic pipeline:

PostgreSQL constraint violation
→ error.constraint (driver metadata)
→ CONSTRAINT_ERROR_MAP lookup
→ typed ApiError

All 72 accounting schema CHECK constraints are classified into two tiers. Ten kernel invariant constraints — covering ledger algebra, rounding pipeline correctness, and conservation laws — map to 500 responses with structured internal telemetry. Sixty-two business rule constraints map to typed 400 responses with field annotations for precise client feedback. Raw PostgreSQL error strings no longer reach the API boundary under any path.

Enforced by: runtime error codec + CI coverage gate — Class M. Proof: constraint-coverage-check.sh — 72/72 constraints.

Threat Closure

Security Posture Change

The error codec moves from Class O (substring matching on raw database messages — leaks structural information in development, provides no typed semantics in production) to Class M (deterministic constraint name lookup — no database internals reach the API boundary, kernel invariant faults produce structured internal telemetry). The CI gate ensures this property cannot silently regress as new constraints are added.

Verification Record

Axiom coverage gate:
  17/17 delivered axioms checked
  0 violations
  All Class M axioms: ≥ 2 independent enforcement layers confirmed

verify-monetary-constraints.sql:   12/12 PASS
verify-double-entry.sql:            6/6  PASS
verify-rls-policy-symmetry.sql:     5/5  PASS  (25 UPDATE policies)
constraint-coverage-check.sh:      72/72 PASS

Adversarial review:
  ALG-VERIFY-001/002/003/004 — double-entry script revised, all findings resolved
  TEN-VERIFY-001 — RLS symmetry script revised, equality proof substituted for token check
  AX-ERR-001 codec — approved, two-tier classification confirmed correct

Architectural Context

M1 through M3 established database-layer enforcement across all delivered invariants. This release closes the second-layer gap, satisfying the kernel doctrine’s dual-layer requirement for all 17 delivered axioms. The axiom registry has been updated to reflect delivered Tests layers for the closed axioms.

M4 (Provenance) can now build on a kernel that is not only enforced at the database layer but independently verified — every invariant has a proof script that can be run after any restore, migration, or schema change to confirm the mathematical properties of the ledger remain intact.

Operational Impact

Verification: Running scripts/verify-axiom-coverage.sh now confirms dual-layer closure across all delivered axioms. Zero violations.

Error semantics: Every mapped accounting CHECK constraint violation now produces a typed API error; user-recoverable faults include field annotations where relevant, while kernel invariant faults return safe opaque 500s with structured internal telemetry.

CI gate: Any future migration that adds a CHECK constraint without a corresponding error codec entry will fail the build.

Post-restore: All four verification scripts can be run after any database restore to confirm ledger integrity before traffic is resumed.

Kernel Status

Files Changed

Backend:

• api/src/lib/api-error.ts — CONSTRAINT_ERROR_MAP added; deterministic constraint → ApiError pipeline replacing substring matching; structured telemetry for kernel invariant faults

Scripts:

• scripts/verify-monetary-constraints.sql — 12-check monetary domain verification (AX-RND-001..005, AX-MON-002)
• scripts/verify-double-entry.sql — 6-check double-entry conservation verification (AX-ALG-001)
• scripts/verify-rls-policy-symmetry.sql — 5-check RLS UPDATE policy symmetry verification (AX-TEN-002)
• scripts/constraint-coverage-check.sh — CI gate confirming 100% constraint → error codec coverage (AX-ERR-001)

Registry:

• docs/kernel/axioms.yml — Tests layer delivered for AX-RND-001..005, AX-MON-002, AX-ALG-001, AX-TEN-002, AX-ERR-001

M4 (Provenance) begins with a kernel that is mathematically closed: every delivered invariant has independent proof.