P1.2.3 — κ AST Validator — Behavioral Contract

Step 2 of the 5-step executor chain. Builds on docs/audits/p1-2-3-validator-audit.md. Defines the public surface, semantics, and invariants for src/domains/rules/validator.ts.

§1. Module identity

Path: src/domains/rules/validator.ts
Axis: κ — Rule Engine (Phase 1 Wave 4)
Kind: pure synchronous module; no I/O, no DB access, no network, no env reads, no console output, read-only over its input AST
Runtime dependencies: none beyond TypeScript stdlib + AST type imports
Internal dependencies:
- ./parser.js — type-only imports of AST node interfaces (RuleNode, GuardClause, EffectCall, Expression, BinaryOp, UnaryOp, LogicalOp, IntLiteral, BoolLiteral, StringLiteral, VarRef, FuncCall, Location, AnyNode)
No imports from src/db/*, src/middleware/*, src/domains/{tasks,skills,trail,proof,router,integrations}/*, or any Node built-ins.

§2. Public API

§2.1. Result types

export interface ValidationError {
  /** Stable code identifying the violation class (see §3.6 for enumeration). */
  code: string;
  /** Human-readable diagnostic. Includes structural context (e.g. function name). */
  message: string;
  /** Structural path from the rule root, e.g. ['guards', '0', 'condition', 'left']. */
  path: string[];
  /** Source span of the offending AST node. `null` only if the node has no location. */
  location: Location | null;
}

export type ValidationResult =
  | { valid: true }
  | { valid: false; errors: ValidationError[] };

§2.2. Constants

/** Function names disallowed in any call position (EffectCall or FuncCall). */
export const FORBIDDEN_FUNCTIONS: readonly string[];

/** Top-level variable roots permitted in `$<root>.<...>` references. */
export const IN_SCOPE_ROOTS: readonly string[];

FORBIDDEN_FUNCTIONS is exposed for testing and so future callers can introspect the blocklist. The Phase-1 contents are: 'time', 'now', 'read_file', 'http_get', 'random', 'rand'. The list is readonly and frozen at module load.

IN_SCOPE_ROOTS is similarly exposed: 'event', 'actor', 'stake', 'reputation', 'token', 'state', 'obligation', 'finality', 'vrf_output'. Also readonly and frozen.

§2.3. The seven check functions

Each takes a RuleNode and returns a (possibly empty) array of ValidationError. None throws.

export function forbiddenFunctions(rule: RuleNode): ValidationError[];
export function sideEffectsInGuard(rule: RuleNode): ValidationError[];
export function mutationOfInput(rule: RuleNode): ValidationError[];
export function typeCompatibility(rule: RuleNode): ValidationError[];
export function scopeCheck(rule: RuleNode): ValidationError[];
export function cycleDetection(rule: RuleNode): ValidationError[];
export function axiomCheck(rule: RuleNode): ValidationError[];

The seven axiom sub-stubs are also exported for granular testing:

export function checkAxiom01(rule: RuleNode): ValidationError[];  // Append-Only Events
export function checkAxiom02(rule: RuleNode): ValidationError[];  // Reputation is Derived
export function checkAxiom03(rule: RuleNode): ValidationError[];  // No Absolute Authority
export function checkAxiom04(rule: RuleNode): ValidationError[];  // Consequence Windows
export function checkAxiom05(rule: RuleNode): ValidationError[];  // Subjective Finality
export function checkAxiom06(rule: RuleNode): ValidationError[];  // Right to Exit
export function checkAxiom07(rule: RuleNode): ValidationError[];  // Technical Sovereignty

axiomCheck(rule) invokes all seven checkAxiomNN functions and concatenates their results in order AX-01 → AX-07.

§2.4. The composer

/**
 * Run all 7 checks against `rule`. No short-circuit — every check runs and
 * its errors are aggregated. Returns `{valid: true}` iff every check returned
 * `[]`. The input `rule` is not mutated.
 */
export function validate(rule: RuleNode): ValidationResult;

§3. Semantics

§3.1. forbiddenFunctions

Definition. Walks every node in the rule. For every EffectCall and every FuncCall, compares its name (or function field on EffectCall) to FORBIDDEN_FUNCTIONS. On match, emits one ValidationError:

code:     "FORBIDDEN_FUNCTION"
message:  `Forbidden function call: ${name}. Reason: ${reason}.`
path:     [...path-to-the-node]
location: <node>.location

The reason mapping (string interpolated into the message):

'time', 'now' → "clock reads are non-deterministic"
'read_file' → "filesystem reads are non-deterministic"
'http_get' → "network IO is non-deterministic and side-effecting"
'random', 'rand' → "randomness is non-deterministic; use a precomputed VRF input"

Order: errors are emitted in pre-order traversal (rule root → guards → effects).

Allowlist: VarRef nodes are not invoked here at all; they are not call shapes. $vrf_output references therefore pass this check trivially. (The allowlist phrasing in the task prompt is informational — VarRef-only allowlist would be dead code at this check; it is also enforced positively at scopeCheck.)

§3.2. sideEffectsInGuard

Definition. For each GuardClause whose condition is non-null, walks the condition expression sub-tree. Every FuncCall encountered emits one ValidationError:

code:     "SIDE_EFFECT_IN_GUARD"
message:  `Function call '${name}' not permitted in guard expression: guards must be read-only.`
path:     [...path-to-funcCall]
location: <funcCall>.location

Conservative scope decision (per audit §5.2). Phase 1 of this check rejects ALL FuncCall in guard position — including the eight pure builtins (min, max, decay, etc.). The fine-grained “pure builtins are OK” allowlist is a P1.3.x or post-ADR loosening, NOT in this task’s scope. This decision is purely additive — loosening later does not break callers (fewer errors).

EffectCall cannot syntactically appear inside a GuardClause.condition per the parser grammar (extraction §1: only Expression body for guards) — so this check focuses on FuncCall exclusively.

§3.3. mutationOfInput

Definition. Walks every node in the rule looking for assignment-shaped patterns against $event.X. The κ DSL grammar (extraction §1) does NOT include an assignment operator (= is only the comparison ==), so no AST node represents assignment.

Therefore: this check always returns [] in Phase 1. It is scaffolded so the structural-7-check requirement holds; the function body documents (a) why it returns [], (b) what it would do if assignment were added in a future grammar revision, and (c) the reserved code INPUT_MUTATION.

This is a parser-level guarantee that the validator inherits — the parser is the stricter gate. The check is not vacuous code: when assignment is added (if ever), this is the slot to fill.

§3.4. typeCompatibility

Definition. Walks every expression in the rule. Maintains a type tag per visited node, where types are:

type Type = 'int' | 'bool' | 'string' | 'unknown';

Inference rules (per audit §5.4):

Node	Rule
`IntLiteral`	`int`
`BoolLiteral`	`bool`
`StringLiteral`	`string`
`VarRef`	`unknown`
`FuncCall`	`unknown`
`UnaryOp{op:'-'}`	`unknown` if operand is `unknown`, else `int` if operand is `int`, else error + return `unknown`
`LogicalOp{op:'and'\\|'or'}`	both operands must be `bool \\| unknown`; result `bool` (or `unknown` if any operand was unknown). Concrete-non-bool operand → error
`LogicalOp{op:'not'}`	operand must be `bool \\| unknown`; result `bool`. Concrete-non-bool → error
`BinaryOp{op:'+'\\|'-'\\|'*'\\|'/'\\|'%'}`	both operands must be `int \\| unknown`; result `int` (or `unknown` if either was unknown). Concrete-non-int → error
`BinaryOp{op:'=='\\|'!='}`	if both concrete and unequal → error; result `bool`
`BinaryOp{op:'<'\\|'>'\\|'<='\\|'>='}`	both operands must be `int \\| unknown`; result `bool`. Concrete-non-int → error

Error emission:

code:     "TYPE_INCOMPATIBLE"
message:  `Type mismatch: ${op} requires ${expected}; got ${leftType} and ${rightType}.`
path:     [...path-to-the-Op-node]
location: <opNode>.location

For UnaryOp/LogicalOp{not}, the message reflects single-operand context. The walker emits one error per offending operator node and continues — children are still inferred to populate parent decisions; on error the parent’s type defaults to a sensible fallthrough (e.g. arithmetic-with-error → int; comparison-with-error → bool) so cascading errors are bounded.

Unknown propagation. A subtree containing unknown (e.g. a VarRef) does not produce a type error at this stage. This matches the audit §5.4 rule “unknown short-circuits to OK.” The intent is: P1.2.3 catches statically-decidable type clashes (literals + literals); deeper type checking happens at evaluator time (P1.3.1) when bindings exist.

§3.5. scopeCheck

Definition. Walks every VarRef in the rule. Compares path[0] against IN_SCOPE_ROOTS. On miss, emits:

code:     "UNDEFINED_VAR"
message:  `Variable '$${path.join('.')}' is undefined: top-level root '${path[0]}' is not in κ context.`
path:     [...path-to-the-VarRef]
location: <varRef>.location

The walk is unaware of scope nesting — κ rules in Phase 1 do not introduce new bindings inside the body (no let, no lambda parameter). Future scope extensions (e.g. P1.3.x evaluator with actor-injected sub-bindings) would expand IN_SCOPE_ROOTS or stitch a context-aware variant.

A VarRef whose path is empty (path: []) — defensively impossible per the parser, which always builds at least a one-element path from $<ident> — is treated as undefined and emits an error.

§3.6. cycleDetection

Definition. Per audit §5.6 + the task prompt’s explicit allowance: cycleDetection(rule) always returns [].

Rationale (documented in JSDoc):

The parser produces a tree by construction within a single rule. There are no AST cycles.
Cross-rule (rule-to-rule) references are not visible at single-rule scope. They are detected by the registry (P1.2.4) at build time over the rule graph.
The check is scaffolded so future single-rule cycle conditions (e.g., recursive macros, if added) have a slot.

The reserved code CYCLE_DETECTED is named for completeness; it is not currently emitted.

§3.7. axiomCheck (and its 7 sub-stubs)

Definition. axiomCheck(rule) returns [...checkAxiom01(rule), ..., ...checkAxiom07(rule)]. Each checkAxiomNN is a separate exported function with its own JSDoc citing the corresponding axiom from docs/3-world/physics/constitution.md.

Each stub returns []. Each carries a docstring explaining what the future check would do (per audit §5.7 table).

The reserved codes AX_01_VIOLATION through AX_07_VIOLATION are named for completeness; they are not currently emitted.

§3.8. validate (composer)

Definition.

export function validate(rule: RuleNode): ValidationResult {
  const errors = [
    ...forbiddenFunctions(rule),
    ...sideEffectsInGuard(rule),
    ...mutationOfInput(rule),
    ...typeCompatibility(rule),
    ...scopeCheck(rule),
    ...cycleDetection(rule),
    ...axiomCheck(rule),
  ];
  if (errors.length === 0) return { valid: true };
  return { valid: false, errors };
}

Invariant (no short-circuit). The composer runs every check unconditionally and aggregates all errors. The order of errors in the output reflects the check order above; within a check, errors reflect AST traversal order (pre-order).

Invariant (read-only). The composer never mutates the input AST. All checks share this invariant; verification F8b deep-compares pre/post.

§4. ValidationError code enumeration

Per audit §10:

Code	Source check	Active in Phase 1?
`FORBIDDEN_FUNCTION`	forbiddenFunctions	yes
`SIDE_EFFECT_IN_GUARD`	sideEffectsInGuard	yes
`INPUT_MUTATION`	mutationOfInput	reserved
`TYPE_INCOMPATIBLE`	typeCompatibility	yes
`UNDEFINED_VAR`	scopeCheck	yes
`CYCLE_DETECTED`	cycleDetection	reserved
`AX_01_VIOLATION`	checkAxiom01	reserved
`AX_02_VIOLATION`	checkAxiom02	reserved
`AX_03_VIOLATION`	checkAxiom03	reserved
`AX_04_VIOLATION`	checkAxiom04	reserved
`AX_05_VIOLATION`	checkAxiom05	reserved
`AX_06_VIOLATION`	checkAxiom06	reserved
`AX_07_VIOLATION`	checkAxiom07	reserved

13 codes total. 4 active in Phase 1.

§5. Determinism + purity invariants

Invariant	Implementation discipline
Pure — same `rule` input ⇒ same `ValidationResult` output	No `Math.random`, no `Date.now()`, no `process.*`, no module-level mutable state. Walker recurses with a local `errors` array; no closure captures of mutable scope outside the function.
Read-only	No `node.x = ...` anywhere. `path` extension is `[...prev, segment]` (immutable). No `Object.assign`, no `delete`, no `splice` on inputs.
No throw on validator path	Every check + `validate()` returns; never throws. (Defensive: if the input violates `RuleNode` shape unexpectedly, the walker’s `default` case in switch returns `[]` — never crashes.)
No I/O	No `fs.`, no `http.`, no `console.`, no `process.env.`. ESLint guarded.

§6. Path encoding

path is an array of strings. Encoding rules:

Field-named segments use the field name as-is: 'guards', 'effects', 'condition', 'left', 'right', 'operand', 'operands', 'args', 'function', 'name'.
Index segments are stringified integers: '0', '1', etc.
Composition is [...parentPath, segment].

Examples:

Offending node	Path
Guard 0’s condition root	`['guards', '0', 'condition']`
Left operand of a binary op in guard 0’s condition	`['guards', '0', 'condition', 'left']`
Effect 2’s third arg	`['effects', '2', 'args', '2']`
Operand of a `not` in guard 1	`['guards', '1', 'condition', 'operands', '0']`

§7. Test-only contract

The validator test file MUST:

Use the parser to construct ASTs from DSL strings (not hand-crafted AST literals — testing the contract end-to-end).
Assert structurally on ValidationError shape: code, presence of path, location !== undefined, message non-empty.
Exercise each named export at least once, including all 7 axiom sub-stubs and the composer.
Cover the F1–F9 fixture matrix per audit §13.
Include an explicit “AST is read-only” deep-equal fixture (F8b).
Include the multi-error fixture asserting errors.length >= 3 (F9), proving no short-circuit.

The test file MUST NOT:

Mutate any constant exported by validator.ts (no (FORBIDDEN_FUNCTIONS as any).push(...)).
Use console.* for assertions.
Test against parser internals (e.g., reaching into lexer.ts).
Test via jest.fn() mocks of validator helpers — the surface is pure functions, mock-free.

§8. Forbidden surface (locked from prompt)

✗ Do not short-circuit on first error — aggregate everything.
✗ Do not consult external I/O for axiom check — axioms are static.
✗ Do not mutate the input AST — validator is read-only.
✗ Do not edit main checkout.

§9. Compatibility with future tasks

Downstream consumer	Validator contribution
P1.2.4 — Rule Loader / Registry	calls `validate(rule)` per parsed rule before indexing; rejects on `valid: false`. The registry is also where cross-rule cycleDetection moves.
P1.3.1 — Core Evaluation Loop	assumes validator-passed rules. May tighten `unknown` types based on context bindings; would not invalidate the validator’s static stance.
P3+ π Governance	activates the AX_NN_VIOLATION codes by replacing the stubs with real check bodies. Code names + signatures are stable.
Future ADR-006-dsl-grammar	should ratify FORBIDDEN_FUNCTIONS list + IN_SCOPE_ROOTS list as part of the grammar spec.

The check function signatures (return type, single-rule input) are designed to be additive: a future ADR can grow check-bodies without changing the type contract.

§10. Acceptance criteria (locked from prompt)

7 check functions implemented + exported (§2.3).
Each rejects its target violation class (test fixtures F1–F7).
Aggregates all errors (multi-error fixture F9 proves no short-circuit).
Structured ValidationError {code, message, path, location} (§2.1).
Axiom checks structured for later π wiring — named function per axiom (§2.3, §3.7).
npm run build && npm run lint && npm test ALL THREE green (CLAUDE.md §5).
Zero new lint warnings.
No regressions on the 1467-test baseline.

Next step: packet (Step 3 of 5).