diff --git a/instructions/defaults/planning.md b/instructions/defaults/planning.md index 61e767d..8a2edc3 100644 --- a/instructions/defaults/planning.md +++ b/instructions/defaults/planning.md @@ -45,6 +45,15 @@ At `planning/read_context`, load context in this order: - If a task reveals additional required work, add or revise a task artifact during planning instead of silently expanding implementation scope. - For a change request after a completed pass, use new revision task IDs such as `fix-storage-root-revision` instead of reopening completed task IDs. +## Generated Artifacts (keep them out of git) + +Before writing task files, account for what this project's toolchain will generate that must NOT be tracked — build outputs, dependency/vendor directories, caches, coverage and test output, editor/tool scratch. Two failure modes to preempt, because either one makes `planner_git_inspect` and later commits swell with generated bulk instead of source: + +- a fresh project whose `.gitignore` is missing or empty, so the first build/dependency step fills the worktree with untracked bulk; +- an existing project adopting a new tool or technology that emits an artifact its current `.gitignore` does not yet cover. + +If the relevant ignore rules are absent, add updating `.gitignore` as an explicit task (or fold it into the setup/scaffolding task that first produces the artifact), so git inspection and commits stay to source only. You already know the conventional artifact names for each ecosystem — apply them; there is no need to spell them out here. If the repository already ignores everything the plan will generate, note that and move on. + ## Restrictions - Do not edit production files or write tests yet. diff --git a/src/guard/tool-policy.ts b/src/guard/tool-policy.ts index 0bcfc6b..9ae626b 100644 --- a/src/guard/tool-policy.ts +++ b/src/guard/tool-policy.ts @@ -29,6 +29,7 @@ export const PLANNER_WRAPPER_TOOLS = [ "planner_refactor_review", "planner_doubt_review", "planner_elenchus_check", + "planner_reason", "planner_skill_create", "planner_skill_update", "planner_contract_scan", @@ -141,6 +142,7 @@ const STEP_ALLOWED_TOOLS = { "planner_contract_read", "planner_contract_upsert", "planner_elenchus_check", + "planner_reason", "planner_git_commit", "planner_exec", ], @@ -187,6 +189,7 @@ const STEP_ALLOWED_TOOLS = { consistency_check: [ "planner_gate_check", "planner_elenchus_check", + "planner_reason", "planner_task_upsert", "planner_contract_route", "planner_contract_read", @@ -205,6 +208,7 @@ const STEP_ALLOWED_TOOLS = { "planner_skill_create", "planner_skill_update", "planner_elenchus_check", + "planner_reason", "planner_debug_strategy", "planner_debug_probe", "planner_debug_result", @@ -264,6 +268,7 @@ const STEP_ALLOWED_TOOLS = { "planner_contract_check", "planner_contract_upsert", "planner_elenchus_check", + "planner_reason", "planner_report_stuck", "planner_skill_create", "planner_skill_update", @@ -329,6 +334,7 @@ const STEP_ALLOWED_TOOLS = { "planner_git_inspect", "planner_doubt_review", "planner_elenchus_check", + "planner_reason", "planner_skill_create", "planner_skill_update", "planner_contract_route", @@ -379,6 +385,7 @@ const STEP_ALLOWED_TOOLS = { "planner_recovery_resume", "planner_git_inspect", "planner_elenchus_check", + "planner_reason", ], }, } as const satisfies Record< @@ -406,7 +413,7 @@ export function getAllowedPlannerWrapperTools( // diagnosis tool (in-process engine, writes only planner artifacts) — // the one broken-state step where it must stay reachable. ...(state.stage === "recovery" && state.step === "repair_or_resume" - ? (["planner_elenchus_check"] as const) + ? (["planner_elenchus_check", "planner_reason"] as const) : []), ]); } diff --git a/src/index.tool-visibility.test.ts b/src/index.tool-visibility.test.ts index 4873956..53846be 100644 --- a/src/index.tool-visibility.test.ts +++ b/src/index.tool-visibility.test.ts @@ -137,8 +137,9 @@ describe("filterPlannerTools", () => { } }); - it("ALL_PLANNER_TOOL_NAMES has exactly 52 tools", () => { - expect(ALL_PLANNER_TOOL_NAMES).toHaveLength(52); + it("ALL_PLANNER_TOOL_NAMES has exactly 53 tools", () => { + expect(ALL_PLANNER_TOOL_NAMES).toHaveLength(53); + expect(ALL_PLANNER_TOOL_NAMES).toContain("planner_reason"); expect(ALL_PLANNER_TOOL_NAMES).toContain("planner_artifact_read"); expect(ALL_PLANNER_TOOL_NAMES).toContain("planner_report_stuck"); expect(ALL_PLANNER_TOOL_NAMES).toContain("planner_refactor_review"); diff --git a/src/index.ts b/src/index.ts index e94628b..2e47925 100644 --- a/src/index.ts +++ b/src/index.ts @@ -177,6 +177,10 @@ import { PLANNER_QUESTION_TOOL_NAMES, type PlannerQuestionToolName, } from "./runtime/question-tools"; +import { + executePlannerReasonTool, + PLANNER_REASON_TOOL_NAME, +} from "./runtime/reason-tools"; import { executePlannerRecoveryReportTool, executePlannerRecoveryTool, @@ -209,6 +213,7 @@ import { executePlannerSpecTool, PLANNER_SPEC_TOOL_NAME, } from "./runtime/spec-tools"; +import { formatTransitionReasoningFuelTail } from "./runtime/status"; import { buildPlannerStuckCompactInstructions, executePlannerStuckTool, @@ -2961,6 +2966,72 @@ function registerPlannerTools( }, }); + pi.registerTool({ + name: PLANNER_REASON_TOOL_NAME, + label: "Planner Reason", + description: + "Grow and re-check the plan's living logical world with the bundled elenchus engine. Statements accumulate across stages: each assert adds facts, premises, or rules to a domain and re-checks the whole world against everything asserted before. Observations may name a source file to anchor to, so when that file later changes the knowledge demotes to a belief instead of raising a false contradiction. The engine's raw output is returned verbatim (CONSISTENT / WARNING / UNDERDETERMINED / CONFLICT and why); the tool never parses it. A reasoning-fuel line reports how much of the interacting-condition web on the table you have run through the engine.", + promptSnippet: + 'At the reasoning steps, default to building the world with planner_reason instead of trusting a prose chain: mode=assert with a domain and statements (each a .vrf line; add anchor="path" for a file observation), mode=retract with ids to remove a statement, mode=recheck to re-run as-is. A CONFLICT hard-blocks planner_finish_step until a re-run improves it — apply the drop/flip the output names or retract the wrong statement, never delete a valid premise. When the decision genuinely has no interacting-constraint web, the fuel line stays silent and you may skip it. Available at the discovery scan, planning/consistency_check, execution/write_tdd_plan, execution/contract_check, finalize/doubt_review, and recovery/repair_or_resume.', + parameters: { + type: "object", + properties: { + mode: { + type: "string", + enum: ["assert", "retract", "recheck"], + description: + '"assert" adds statements to a world domain and re-checks; "retract" removes statements by id and re-checks; "recheck" re-runs the world as-is.', + }, + domain: { + type: "string", + description: + 'World domain for asserted statements: "discovery", "plan", "scratch", or "task_". Required when mode=assert.', + }, + statements: { + type: "array", + items: { + type: "object", + properties: { + vrf: { + type: "string", + description: + "One elenchus statement (FACT/NOT/PREMISE/RULE/BELIEVES/SET/CLOSE/VAR), possibly multi-line. Instruments (PROVE/HENCE/TRY) are not stored.", + }, + anchor: { + type: "string", + description: + "Optional project-root-relative file this observation is read from. The tool hashes it now; only FACT/NOT may carry an anchor.", + }, + }, + required: ["vrf"], + additionalProperties: false, + }, + description: + "The statements to assert. Required and non-empty when mode=assert.", + }, + ids: { + type: "array", + items: { type: "string" }, + description: + 'Statement ids to remove, e.g. ["w3","w7"]. Required and non-empty when mode=retract.', + }, + }, + required: ["mode"], + additionalProperties: false, + } as never, + async execute(_toolCallId, params, _signal, _onUpdate, ctx) { + const { fs, projectPaths } = await resolveRuntimeContext(ctx.cwd); + await recordPlannerToolActivityForProject({ fs, projectPaths }); + const result = await executePlannerReasonTool({ + fs, + git: gitRunner, + projectPaths, + params, + }); + return plannerToolResponse(result); + }, + }); + pi.registerTool({ name: PLANNER_SPEC_TOOL_NAME, label: "Planner Spec Submit", @@ -3310,11 +3381,27 @@ function registerPlannerTools( transitionStatus: result.result.status, }); + // Ride the reasoning-fuel nudge on the transition tail so the model + // sees it in the drive loop (planner_finish_step), not only on a rare + // planner_status call. Computed for the step this transition lands on; + // self-silences when no interacting-condition web is warranted there. + // Presentational only — fuel enters no decision, and this seam calls + // the surfacing layer (status), never a fuel module, so the tone-only + // invariant holds. + const fuelLine = await formatTransitionReasoningFuelTail({ + fs, + status: result.result.status, + planPaths: result.planPaths, + state: result.result.state, + }); + return { content: [ { type: "text", - text: [result.text, compact?.text].filter(Boolean).join("\n\n"), + text: [result.text, compact?.text, fuelLine] + .filter(Boolean) + .join("\n\n"), }, ], details: compact ? { ...result, compact } : result, @@ -3460,15 +3547,13 @@ function registerPlannerTools( } const PLANNER_COMPACT_WIDGET_KEY = "planner-compact"; -// Refresh cadence for the indicator's slow-moving parts (the asymptotic bar, -// percent, and ETA). The SDK's setWidget has NO diffing — every call disposes -// the old component and rebuilds it (interactive-mode.js `setExtensionWidget`), -// so each push is a full teardown+repaint. A 1 Hz push of a live seconds counter -// therefore flickers the banner every second. We keep the indicator nearly -// static instead: no per-second elapsed in the rendered line, a coarse refresh, -// and a content dedup (see `setCompactWidget`) that skips a push when nothing -// visible changed — so in steady state the widget repaints only when the bar or -// ETA actually moves, not on a fixed clock. +// Tick cadence for the safety-deadline check only. The SDK's setWidget has NO +// diffing — every call disposes the old component and rebuilds it +// (interactive-mode.js `setExtensionWidget`), so each push is a full +// teardown+repaint that reflows the editor. So the rendered line is fully STATIC +// for the run (no elapsed, no moving percent/bar): the content dedup in +// `setCompactWidget` pushes it once and skips every later tick, and this interval +// only re-checks the deadline below. Nothing animates, so nothing flickers. const PLANNER_COMPACT_REFRESH_MS = 5000; // Safety deadline so a *failed* compaction can never leave the indicator up // forever. Pi's built-in /compact swallows a failure and never emits @@ -3667,26 +3752,24 @@ function registerPlannerCompactEvents( ) : PLANNER_COMPACT_MAX_MS; + // The rendered line is static (no elapsed/percent) — the same string every + // tick — so the widget setter's dedup pushes it once and never repaints it + // mid-run. The interval therefore exists only to enforce the safety + // deadline; it does not animate anything. + const text = formatCompactIndicator({ sizeLabel, reasonLabel, estimate }); const renderStatus = () => { try { - const elapsedMs = Date.now() - startedAt; - // Self-terminating deadline: the tick that draws the elapsed seconds - // also enforces the cap, so a failed compaction with no completion - // event and no follow-up turn cannot hang the indicator (the 124m - // "still Compacting…" case). A separate setTimeout could be lost across - // suspend/resume; this cannot — if the bar is ticking, the check runs. - if (elapsedMs >= clearAfterMs) { + // Self-terminating deadline: the same tick that keeps the banner up also + // enforces the cap, so a failed compaction with no completion event and + // no follow-up turn cannot hang the indicator (the 124m "still + // Compacting…" case). A separate setTimeout could be lost across + // suspend/resume; this cannot — if the interval is live, the check runs. + if (Date.now() - startedAt >= clearAfterMs) { // A run that never completed is not a representative timing sample. pendingCompact = null; stopCompactIndicator(ctx); return; } - const text = formatCompactIndicator({ - sizeLabel, - reasonLabel, - elapsedMs, - estimate, - }); setCompactWidget(ctx, [ctx.ui.theme.fg("accent", text)], text); } catch { // Never let a redraw throw out of the interval. @@ -3774,9 +3857,18 @@ function registerPlannerCompactEvents( // the chat, and no message can stream while summarization blocks the loop. So // the moment one arrives with the indicator still up, the run has ended — hide // it at once rather than waiting for the next agent_start or the safety cap. + // We clear on BOTH message_start and every streaming message_update: a + // streaming assistant reply is delivered as message_update tokens (the signal + // the dashboard itself tracks), and message_start alone does not fire reliably + // for it — so keying only on message_start left the banner sitting over the + // model's answer as it streamed. clearStaleCompactIndicator is idempotent (a + // no-op once nothing is up), so a per-token call is cheap. pi.on("message_start", async (_event, ctx) => { clearStaleCompactIndicator(ctx); }); + pi.on("message_update", async (_event, ctx) => { + clearStaleCompactIndicator(ctx); + }); // Proactive monitor: at every turn boundary, project the context budget from // the model's real output budget and compact *before* the window fills, so a diff --git a/src/runtime/AGENTS.md b/src/runtime/AGENTS.md index 41b8aff..c2d3c65 100644 --- a/src/runtime/AGENTS.md +++ b/src/runtime/AGENTS.md @@ -15,6 +15,7 @@ Runtime domain for planner stages, model-facing status, tool wrappers, timers, r - Runtime gates must never allow wrappers outside the current stage/step policy. - Artifacts are the durable truth after compact; chat memory is advisory only. - `planner_contract_upsert` may write AGENTS.md only. Other context files are read-only imports. +- Reasoning fuel is tone-only: its level changes only the directive the model reads, never an allow/block decision. The only hard floors stay on named terminal defects (a CONFLICT verdict, an un-CONSISTENT gate). Enforced by `fuel-never-blocks.invariant.test.ts`. ### Read First - `status.ts` @@ -69,12 +70,19 @@ Runtime domain for planner stages, model-facing status, tool wrappers, timers, r **SDD gates (spec-driven development)** — the deterministic verifier loop: the model authors structured artifacts, compilers in `vrf/` turn them into VRF, the elenchus engine judges, and `workflow-tools.ts` hard-gates on the verdict. - `elenchus-engine.ts` → thin lazy loader for the `elenchus-wasm` engine (`runElenchusCheck` with a sandboxed IMPORT resolver); degrades to a typed failure if the wasm is missing. -- `elenchus-tools.ts` → `planner_elenchus_check` (free-form, model-authored programs) + the shared `last-check.json` record (`ElenchusLastCheckRecord`, extended with `gate`/`sourceHash` for gate runs). +- `elenchus-tools.ts` → `planner_elenchus_check` (free-form, model-authored programs) + the shared `last-check.json` record (`ElenchusLastCheckRecord`, with `gate`/`sourceHash` for gate runs and a `repeat` counter that `writeElenchusLastCheck` increments on identical gate re-runs — the gate-thrash friction signal). - `spec-tools.ts` → `planner_spec_submit`: validates and persists `spec.json`/renders `spec.md` via `storage/spec-store.ts`; snapshots the previous version to `spec.prev.json` (change-request audit trail). - `gate-tools.ts` → `planner_gate_check` (`spec_consistency` | `plan_coverage` | `tdd_coverage`): loads durable artifacts, runs the matching deterministic compiler from `src/vrf/`, executes the engine, writes `coverage.md` sections + `last-check.json` (verdict + sha256 of the compiled source), and translates every machine gap into a concrete action or a ready-to-ask user question. Takes NO program — gate VRF is never hand-written (REQ-12). - `behavior-tools.ts` → `planner_behavior_upsert`: the per-task behavior board (`storage/behavior-store.ts`), the `planned → red → green` test-first toggle ladder. - Hard gates live in `workflow-tools.ts` (`validateSpecGatePassed`, `validatePlanCoverageGatePassed`, `validateTddCoverageGatePassed`): a gate step only advances on a CONSISTENT run whose `sourceHash` still matches the artifact on disk; legacy plans/tasks without the artifact degrade gracefully (REQ-11). +**Reasoning fuel** — a tone-only nudge toward the engine where a real interacting-condition web is on the table, computed entirely from the planner's own artifacts and records (never the engine's report). See the `fuel-never-blocks` Stable Contract above. +- `reasoning-fuel.ts` → pure math: `computeReasoningFuel({warrantedWeb, coverage, stale, friction})` (null when nothing warrants the engine), plus the warranted-web collectors (branches/spec-constraints/shared-surfaces) and the engagement/friction readers over `ElenchusLastCheckRecord`. No I/O, no store, no engine. +- `reason-context.ts` → `loadStepReasoningFuel`: assembles the current step's fuel by loading only the planner's own artifacts (spec constraints at consistency_check, task branches at the execution reasoning steps, shared task surfaces at doubt_review). The one bridge both the reason tool and `status.ts` call. +- `reason-directive.ts` → `renderReasoningDirective`: the tone ladder (silent when null, quiet ≥70, top-deficit in 30–69, directing below 30 or on any friction). Templated, never generative. +- `reason-tools.ts` → `planner_reason` (assert/retract/recheck over the living `vrf/world-store.ts`): returns the verdict + the engine's raw output verbatim + the fuel directive, and writes a model-authored `last-check.json` so fuel credits the engagement. Gated exactly like `planner_elenchus_check`. +- Surfacing: the fuel directive is rendered in `status.ts` (the `## Reasoning Fuel` section) AND on the tail of an applied workflow transition via `status.ts` `formatTransitionReasoningFuelTail`, which the tool dispatcher (`index.ts`) appends to `planner_finish_step`'s result — so the model meets the nudge in the drive loop it actually reads, not only on a rare `planner_status`. The dispatcher imports this from the surfacing layer (`status.ts`), never a fuel module, so the `fuel-never-blocks` invariant holds; `workflow-tools.ts` only passes `planPaths` through as data. + **TDD** — the structured pre/post-implementation evidence form. - `tdd-evidence.ts` → field/section name constants for the pre-implementation proof contract, post-implementation counterexample review, and merge-scope audit; no logic. - `tdd-form.ts` → `TDD_SECTIONS` (canonical order) + `mergeTddMarkdown`/`renderTddSection`, used by `artifact-tools.ts` to assemble/merge the TDD artifact. diff --git a/src/runtime/compact-eta.test.ts b/src/runtime/compact-eta.test.ts index 4b148aa..f5ee9a9 100644 --- a/src/runtime/compact-eta.test.ts +++ b/src/runtime/compact-eta.test.ts @@ -1,12 +1,10 @@ import { describe, expect, it } from "vitest"; import { type CompactTimingSample, - compactionProgressFraction, estimateCompactionDuration, formatCompactIndicator, formatDurationShort, formatEtaLabel, - renderProgressBar, } from "./compact-eta"; function sample( @@ -19,31 +17,21 @@ function sample( } describe("formatCompactIndicator", () => { - it("shows a static label (no ticking seconds) when there is no estimate", () => { + it("shows a bare static label when there is no estimate", () => { const estimate = estimateCompactionDuration({ samples: [], tokens: 118_000, model: "m", }); - // The line must NOT depend on elapsedMs: a per-second counter would push a - // full repaint every tick and flicker the widget. Same output at 12s / 40s. - const at12 = formatCompactIndicator({ - sizeLabel: "118k", - reasonLabel: "/compact", - elapsedMs: 12_000, - estimate, - }); - const at40 = formatCompactIndicator({ + const line = formatCompactIndicator({ sizeLabel: "118k", reasonLabel: "/compact", - elapsedMs: 40_000, estimate, }); - expect(at12).toBe("Compacting 118k tok (/compact)…"); - expect(at40).toBe(at12); + expect(line).toBe("Compacting 118k tok (/compact)…"); }); - it("shows a filling bar, percent and ETA once history exists — no elapsed", () => { + it("appends the predicted ETA as a fixed hint once history exists — no bar, no percent, no elapsed", () => { const estimate = estimateCompactionDuration({ samples: [ sample(50_000, 10_000), @@ -56,13 +44,13 @@ describe("formatCompactIndicator", () => { const line = formatCompactIndicator({ sizeLabel: "100k", reasonLabel: "context full", - elapsedMs: 5_000, estimate, }); - // bar + percent + ETA, but no ` /` segment before the `~`. - expect(line).toMatch( - /^Compacting 100k tok \(context full\) [█░]+ \d+% · ~/, - ); + // A static ETA hint, never an animated bar/percent — nothing that moves + // mid-run and reflows the banner on every push. + expect(line).toMatch(/^Compacting 100k tok \(context full\) · ~/); + expect(line).not.toMatch(/[█░]/); + expect(line).not.toMatch(/%/); }); }); @@ -259,89 +247,6 @@ describe("estimateCompactionDuration", () => { }); }); -describe("compactionProgressFraction", () => { - it("is zero at start and rises monotonically", () => { - const eta = 20_000; - const at0 = compactionProgressFraction({ - elapsedMs: 0, - etaMs: eta, - reliability: "stable", - }); - const at5 = compactionProgressFraction({ - elapsedMs: 5_000, - etaMs: eta, - reliability: "stable", - }); - const at10 = compactionProgressFraction({ - elapsedMs: 10_000, - etaMs: eta, - reliability: "stable", - }); - expect(at0).toBe(0); - expect(at5).toBeGreaterThan(at0); - expect(at10).toBeGreaterThan(at5); - }); - - it("reaches the fill target exactly at the ETA", () => { - const p = compactionProgressFraction({ - elapsedMs: 20_000, - etaMs: 20_000, - reliability: "stable", - }); - expect(p).toBeCloseTo(0.9, 5); - }); - - it("never reaches 100% even long past the ETA", () => { - const p = compactionProgressFraction({ - elapsedMs: 10_000_000, - etaMs: 20_000, - reliability: "stable", - }); - expect(p).toBeLessThan(1); - expect(p).toBeLessThanOrEqual(0.99); - }); - - it("fills more conservatively when noisy than when stable", () => { - const stable = compactionProgressFraction({ - elapsedMs: 20_000, - etaMs: 20_000, - reliability: "stable", - }); - const noisy = compactionProgressFraction({ - elapsedMs: 20_000, - etaMs: 20_000, - reliability: "noisy", - }); - expect(noisy).toBeLessThan(stable); - }); - - it("is zero for a 'none' reliability", () => { - expect( - compactionProgressFraction({ - elapsedMs: 5_000, - etaMs: 0, - reliability: "none", - }), - ).toBe(0); - }); -}); - -describe("renderProgressBar", () => { - it("renders empty and full bars", () => { - expect(renderProgressBar(0, 10)).toBe("░░░░░░░░░░"); - expect(renderProgressBar(1, 10)).toBe("██████████"); - }); - - it("renders a partial bar", () => { - expect(renderProgressBar(0.5, 10)).toBe("█████░░░░░"); - }); - - it("clamps out-of-range fractions", () => { - expect(renderProgressBar(-1, 4)).toBe("░░░░"); - expect(renderProgressBar(2, 4)).toBe("████"); - }); -}); - describe("formatDurationShort", () => { it("formats seconds and minutes", () => { expect(formatDurationShort(8_000)).toBe("8s"); diff --git a/src/runtime/compact-eta.ts b/src/runtime/compact-eta.ts index 3934f47..9cd94ab 100644 --- a/src/runtime/compact-eta.ts +++ b/src/runtime/compact-eta.ts @@ -57,8 +57,6 @@ * (b) lowers the bar's fill target so it is less likely to overrun. */ -import { clamp } from "./num"; - export interface CompactTimingSample { /** `tokensBefore` — the context size that was summarized. */ tokens: number; @@ -106,20 +104,6 @@ const CV_STABLE = 0.25; const MIN_SPREAD = 1e-9; // Never predict a sub-second compaction — the round-trip alone costs more. const ETA_FLOOR_MS = 800; -// The bar creeps from its ETA target toward this cap but never reaches 100% -// until the real completion event fires. -const PROGRESS_CAP = 0.99; -// Time-constant (in units of ETA) for the post-ETA asymptotic creep. -const PROGRESS_CREEP = 0.6; - -// Bar fill reached exactly at the predicted ETA, chosen by confidence: a stable -// estimate fills close to full, a noisy or single-sample one stays conservative -// so an overrun is less jarring. -const FILL_AT_ETA: Record, number> = { - stable: 0.9, - noisy: 0.8, - single: 0.75, -}; function noEstimate(): CompactEtaEstimate { return { @@ -307,36 +291,6 @@ export function estimateCompactionDuration(input: { }; } -/** - * Fraction (0..CAP) to fill the bar after `elapsedMs`, given the predicted ETA. - * - * Honest and monotonic: it fills linearly to `FILL_AT_ETA[reliability]` at - * exactly the ETA, then creeps asymptotically toward — but never reaches — - * `PROGRESS_CAP`. The real completion event is what shows 100%; the bar itself - * never claims to be done. - */ -export function compactionProgressFraction(input: { - elapsedMs: number; - etaMs: number; - reliability: CompactEtaReliability; -}): number { - if (!(input.etaMs > 0) || input.reliability === "none") return 0; - const target = FILL_AT_ETA[input.reliability]; - const f = Math.max(0, input.elapsedMs) / input.etaMs; - const p = - f <= 1 - ? target * f - : target + - (PROGRESS_CAP - target) * (1 - Math.exp(-(f - 1) / PROGRESS_CREEP)); - return clamp(p, 0, PROGRESS_CAP); -} - -/** Render a fixed-width block bar for the given fraction. */ -export function renderProgressBar(fraction: number, width = 10): string { - const filled = clamp(Math.round(fraction * width), 0, width); - return "█".repeat(filled) + "░".repeat(width - filled); -} - /** * Short human duration. Below a minute it is just seconds (`8s`, `45s`). At or * above a minute it always shows minutes AND seconds together, seconds @@ -352,32 +306,27 @@ export function formatDurationShort(ms: number): string { } /** - * Compose the one-line compaction indicator. With learned history it shows an - * honest, asymptotic bar (`… ██████░░░░ 62% · ~30s`); with no history yet it is - * a bare label. Deliberately carries NO per-second elapsed: the SDK repaints the - * whole widget on every push (no diffing), so a ticking seconds counter flickers - * the banner every second. The bar/percent advance slowly off `elapsedMs` while - * the *rendered* line changes only coarsely, so the dedup in the widget setter - * skips most pushes and the banner stays visually still. Pure so the format is - * unit-tested without the SDK, and shared by every surface that shows the run. + * Compose the one-line compaction indicator. It is STATIC for the whole run: + * with learned history it appends the predicted duration as a fixed hint + * (`Compacting 100k tok (context full) · ~30s`), otherwise a bare label. Nothing + * here depends on elapsed time — the SDK repaints the whole widget on every push + * (no diffing), so any line that changed mid-run (a ticking counter, a moving + * percent bar) tore the banner down and reflowed the editor on every update. + * A constant line lets the widget setter's content dedup skip every push after + * the first, so the banner is drawn once and stays put until it clears. Pure so + * the format is unit-tested without the SDK, and shared by every surface that + * shows the run. */ export function formatCompactIndicator(input: { sizeLabel: string; reasonLabel: string; - elapsedMs: number; estimate: CompactEtaEstimate; }): string { + const head = `Compacting ${input.sizeLabel} tok (${input.reasonLabel})`; if (!input.estimate.hasEstimate) { - return `Compacting ${input.sizeLabel} tok (${input.reasonLabel})…`; + return `${head}…`; } - const frac = compactionProgressFraction({ - elapsedMs: input.elapsedMs, - etaMs: input.estimate.etaMs, - reliability: input.estimate.reliability, - }); - const bar = renderProgressBar(frac); - const pct = Math.round(frac * 100); - return `Compacting ${input.sizeLabel} tok (${input.reasonLabel}) ${bar} ${pct}% · ${formatEtaLabel(input.estimate)}`; + return `${head} · ${formatEtaLabel(input.estimate)}`; } /** diff --git a/src/runtime/compact.ts b/src/runtime/compact.ts index 22c56b8..04cb398 100644 --- a/src/runtime/compact.ts +++ b/src/runtime/compact.ts @@ -137,10 +137,12 @@ export function clearPlannerCompactionInFlight( } /** - * Decide whether a resume signal (`agent_start` / `turn_start` / `message_start`) - * should tear down the compaction indicator. Summarization blocks the agent loop, - * so the loop only runs *between* compactions — any resume signal therefore means - * the compaction is over and an indicator still up is stale. + * Decide whether a resume signal (`agent_start` / `turn_start` / `message_start` + * / a streaming `message_update`) should tear down the compaction indicator. + * Summarization blocks the agent loop, so the loop only runs *between* + * compactions — any resume signal therefore means the compaction is over and an + * indicator still up is stale. A streaming reply surfaces as message_update + * tokens, so it is included: the banner must not sit over the model's answer. * * We clear when EITHER our per-registration interval is live OR the shared, * dashboard-mirrored banner line is still showing. Gating on the timer alone diff --git a/src/runtime/elenchus-last-check.test.ts b/src/runtime/elenchus-last-check.test.ts new file mode 100644 index 0000000..70584f9 --- /dev/null +++ b/src/runtime/elenchus-last-check.test.ts @@ -0,0 +1,71 @@ +import { describe, expect, it } from "vitest"; +import { MockPlannerFs } from "../test/mock-fs"; +import { + type ElenchusLastCheckRecord, + readElenchusLastCheck, + writeElenchusLastCheck, +} from "./elenchus-tools"; + +const DIR = "/plan/elenchus"; + +function gateRecord( + overrides: Partial = {}, +): ElenchusLastCheckRecord { + return { + name: "spec_consistency", + stage: "spec", + step: "verify_spec", + outcome: "WARNING", + recordedAt: "2026-07-08T00:00:00.000Z", + gate: "spec_consistency", + sourceHash: "hash-1", + ...overrides, + }; +} + +describe("writeElenchusLastCheck — gate-thrash repeat counter", () => { + it("starts at 0 and increments while gate, source, and verdict all repeat", async () => { + const fs = new MockPlannerFs(); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(0); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(1); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(2); + }); + + it("resets when the source hash changes (real progress)", async () => { + const fs = new MockPlannerFs(); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(1); + await writeElenchusLastCheck(fs, DIR, gateRecord({ sourceHash: "hash-2" })); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(0); + }); + + it("resets when the verdict changes", async () => { + const fs = new MockPlannerFs(); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + await writeElenchusLastCheck(fs, DIR, gateRecord()); + await writeElenchusLastCheck( + fs, + DIR, + gateRecord({ outcome: "CONSISTENT" }), + ); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBe(0); + }); + + it("never sets a repeat counter on a model-authored (non-gate) check", async () => { + const fs = new MockPlannerFs(); + const record: ElenchusLastCheckRecord = { + name: "world", + stage: "execution", + step: "contract_check", + outcome: "CONSISTENT", + recordedAt: "2026-07-08T00:00:00.000Z", + }; + await writeElenchusLastCheck(fs, DIR, record); + await writeElenchusLastCheck(fs, DIR, record); + expect((await readElenchusLastCheck(fs, DIR))?.repeat).toBeUndefined(); + }); +}); diff --git a/src/runtime/elenchus-tools.ts b/src/runtime/elenchus-tools.ts index 50d194b..be69a3c 100644 --- a/src/runtime/elenchus-tools.ts +++ b/src/runtime/elenchus-tools.ts @@ -79,6 +79,14 @@ export interface ElenchusLastCheckRecord { /** sha256 of the compiled source artifact (e.g. spec.json), so a gate pass * is invalidated when the artifact changes after the check. */ sourceHash?: string; + /** + * How many times in a row this exact gate run repeated — same gate, same + * sourceHash, same outcome. Computed by {@link writeElenchusLastCheck}; used + * by the reasoning-fuel layer as the gate-thrash friction signal. A real + * change (new sourceHash) or a different verdict resets it to 0. Only ever + * set for gate runs; model-authored checks leave it unset. + */ + repeat?: number; } const LAST_CHECK_FILE = "last-check.json"; @@ -103,12 +111,32 @@ export async function writeElenchusLastCheck( elenchusDir: string, record: ElenchusLastCheckRecord, ): Promise { + // Gate thrash: re-running the SAME gate with the SAME source and the SAME + // verdict is spinning, not progress. Carry a repeat counter so the fuel layer + // can name it. A model-authored check (no gate) never accrues one; any real + // change (new sourceHash) or a different verdict resets it. + const stored = record.gate + ? { ...record, repeat: await nextGateRepeat(fs, elenchusDir, record) } + : record; await fs.writeTextAtomic( join(elenchusDir, LAST_CHECK_FILE), - `${JSON.stringify(record, null, "\t")}\n`, + `${JSON.stringify(stored, null, "\t")}\n`, ); } +async function nextGateRepeat( + fs: PlannerToolContext["fs"], + elenchusDir: string, + record: ElenchusLastCheckRecord, +): Promise { + const previous = await readElenchusLastCheck(fs, elenchusDir); + const same = + previous?.gate === record.gate && + previous?.sourceHash === record.sourceHash && + previous?.outcome === record.outcome; + return same ? (previous?.repeat ?? 0) + 1 : 0; +} + /** * Run the bundled elenchus engine on a model-authored `.vrf` program, or record * a terminal `not_applicable` escape. The escape — mirroring doubt_review's diff --git a/src/runtime/fuel-never-blocks.invariant.test.ts b/src/runtime/fuel-never-blocks.invariant.test.ts new file mode 100644 index 0000000..6aecddd --- /dev/null +++ b/src/runtime/fuel-never-blocks.invariant.test.ts @@ -0,0 +1,85 @@ +import { readdirSync, readFileSync } from "node:fs"; +import { dirname, join, relative } from "node:path"; +import { fileURLToPath } from "node:url"; +import { describe, expect, it } from "vitest"; + +/** + * The load-bearing property of the whole reasoning-fuel redesign: fuel is + * TONE-ONLY. Its level must not enter any allow/block decision anywhere — the + * only floors are on named terminal defects (a CONFLICT verdict, an + * un-CONSISTENT gate), never on how much fuel there is. + * + * We enforce this structurally: the modules that decide what is allowed, + * blocked, gated, or transitionable must not import the fuel modules at all. If + * a decision cannot even see fuel, it cannot key on it. Break the property — + * import a fuel module into any decision path — and this test fails. + */ + +const SRC_ROOT = join(dirname(fileURLToPath(import.meta.url)), ".."); + +// The modules that produce or shape the fuel level. +const FUEL_MODULES = ["reasoning-fuel", "reason-context", "reason-directive"]; + +// Every module that decides allow / block / gate / transition. +const DECISION_MODULES = [ + "guard/tool-policy.ts", + "runtime/orchestrator.ts", + "runtime/orchestrator-gate.ts", + "runtime/workflow-tools.ts", + "runtime/gate-tools.ts", + "runtime/state-machine.ts", + "runtime/state-transition.ts", +]; + +// The only non-test modules allowed to import a fuel module — the surfacing +// layer (the reason tool and the status text), plus the fuel graph itself. +const ALLOWED_FUEL_IMPORTERS = new Set([ + "runtime/reason-context.ts", + "runtime/reason-directive.ts", + "runtime/reason-tools.ts", + "runtime/status.ts", +]); + +function importsAnyFuelModule(source: string): boolean { + return FUEL_MODULES.some((mod) => + new RegExp(`from\\s+"[^"]*${mod}"`).test(source), + ); +} + +describe("fuel is tone-only — it enters no allow/block decision", () => { + it("no decision module imports a fuel module", () => { + for (const rel of DECISION_MODULES) { + const source = readFileSync(join(SRC_ROOT, rel), "utf8"); + expect( + importsAnyFuelModule(source), + `${rel} must not import a fuel module — fuel is tone-only and cannot gate`, + ).toBe(false); + } + }); + + it("only the surfacing layer imports a fuel module", () => { + const offenders: string[] = []; + for (const file of walkTsFiles(SRC_ROOT)) { + const rel = relative(SRC_ROOT, file).replace(/\\/g, "/"); + if (rel.endsWith(".test.ts")) continue; + if (FUEL_MODULES.some((mod) => rel.endsWith(`${mod}.ts`))) continue; + if (ALLOWED_FUEL_IMPORTERS.has(rel)) continue; + if (importsAnyFuelModule(readFileSync(file, "utf8"))) offenders.push(rel); + } + expect( + offenders, + "unexpected fuel importers outside the surfacing layer", + ).toEqual([]); + }); +}); + +function* walkTsFiles(dir: string): Generator { + for (const entry of readdirSync(dir, { withFileTypes: true })) { + const full = join(dir, entry.name); + if (entry.isDirectory()) { + yield* walkTsFiles(full); + } else if (entry.name.endsWith(".ts")) { + yield full; + } + } +} diff --git a/src/runtime/reason-context.ts b/src/runtime/reason-context.ts new file mode 100644 index 0000000..6ff0c14 --- /dev/null +++ b/src/runtime/reason-context.ts @@ -0,0 +1,149 @@ +import { readTaskBehaviorsIfExists } from "../storage/behavior-store"; +import type { PlannerFs } from "../storage/fs"; +import type { PlanStoragePaths } from "../storage/paths"; +import { createTaskStoragePaths } from "../storage/paths"; +import { readPlanRecordIfExists } from "../storage/plan-store"; +import type { PlanStateRecord, TaskRecord } from "../storage/schema"; +import { readSpecRecordIfExists } from "../storage/spec-store"; +import { readTaskRecord } from "../storage/task-store"; +import { readElenchusLastCheck } from "./elenchus-tools"; +import type { FuelLastCheck, ReasoningFuel } from "./reasoning-fuel"; +import { + computeReasoningFuel, + coverageFromLastCheck, + frictionFromLastCheck, + sharedTaskSurfaces, + warrantedWebFromBranches, + warrantedWebFromSpecConstraints, +} from "./reasoning-fuel"; + +/** + * Assembles reasoning fuel for the current step by loading only the planner's + * OWN artifacts — the spec's constraints, the active task's declared branches, + * the plan's shared task surfaces — plus its own last-check record. Nothing + * here reads the engine's report. This is the bridge the reason tool and the + * status line both call so fuel is computed one way everywhere. + * + * The warranted web per step mirrors where a real interacting-condition web + * lives: the spec's constraints at consistency_check, the task's branches at + * the two execution reasoning steps, the plan's shared surfaces at + * doubt_review. Steps with no measurable web (the discovery scan, the recovery + * repair) return 0, so fuel is null there and the directive stays silent. + */ + +export interface StepReasoningFuel { + fuel: ReasoningFuel; + /** Plural noun for the web at this step, for the directive to name. */ + webNoun: string; +} + +interface StepWeb { + warrantedWeb: number; + webNoun: string; +} + +async function warrantedWebForStep( + fs: PlannerFs, + planPaths: PlanStoragePaths, + state: PlanStateRecord, +): Promise { + if (state.stage === "planning" && state.step === "consistency_check") { + const spec = await readSpecRecordIfExists(fs, planPaths); + return { + warrantedWeb: spec ? warrantedWebFromSpecConstraints(spec) : 0, + webNoun: "spec constraints", + }; + } + if ( + state.stage === "execution" && + (state.step === "write_tdd_plan" || state.step === "contract_check") + ) { + return { + warrantedWeb: await countActiveTaskBranches(fs, planPaths, state), + webNoun: "declared branches", + }; + } + if (state.stage === "finalize" && state.step === "doubt_review") { + const tasks = await loadAllTaskRecords(fs, planPaths); + return { + warrantedWeb: sharedTaskSurfaces(tasks), + webNoun: "shared task surfaces", + }; + } + return { warrantedWeb: 0, webNoun: "" }; +} + +async function countActiveTaskBranches( + fs: PlannerFs, + planPaths: PlanStoragePaths, + state: PlanStateRecord, +): Promise { + const taskId = state.activeTaskId; + if (!taskId) return 0; + const record = await readTaskBehaviorsIfExists( + fs, + createTaskStoragePaths(planPaths, taskId), + ); + if (!record) return 0; + const branches = record.behaviors.flatMap((behavior) => behavior.branches); + return warrantedWebFromBranches(branches); +} + +async function loadAllTaskRecords( + fs: PlannerFs, + planPaths: PlanStoragePaths, +): Promise { + const plan = await readPlanRecordIfExists(fs, planPaths); + if (!plan) return []; + const records: TaskRecord[] = []; + for (const summary of plan.tasks) { + try { + records.push( + await readTaskRecord( + fs, + createTaskStoragePaths(planPaths, summary.taskId), + ), + ); + } catch { + // A summary without a materialized task.json yet contributes no scope. + } + } + return records; +} + +/** + * Compute the current step's reasoning fuel. `stale` (from a world run's own + * anchor sweep) and `lastCheck` may be passed in to avoid re-reading them right + * after a run; both default to a fresh read / zero. + */ +export async function loadStepReasoningFuel(input: { + fs: PlannerFs; + planPaths: PlanStoragePaths; + state: PlanStateRecord; + stale?: number; + lastCheck?: FuelLastCheck | null; +}): Promise { + const { fs, planPaths, state } = input; + const { warrantedWeb, webNoun } = await warrantedWebForStep( + fs, + planPaths, + state, + ); + const lastCheck = + input.lastCheck !== undefined + ? input.lastCheck + : await readElenchusLastCheck(fs, planPaths.elenchusDir); + const coverage = coverageFromLastCheck({ + warrantedWeb, + lastCheck, + stage: state.stage, + step: state.step, + }); + const fuel = computeReasoningFuel({ + warrantedWeb, + coverage, + stale: input.stale ?? 0, + friction: frictionFromLastCheck(lastCheck), + }); + return { fuel, webNoun }; +} diff --git a/src/runtime/reason-directive.test.ts b/src/runtime/reason-directive.test.ts new file mode 100644 index 0000000..9d82fb2 --- /dev/null +++ b/src/runtime/reason-directive.test.ts @@ -0,0 +1,66 @@ +import { describe, expect, it } from "vitest"; +import { renderReasoningDirective } from "./reason-directive"; +import { computeReasoningFuel, type ReasoningFuel } from "./reasoning-fuel"; + +const CONTEXT = { webNoun: "declared branches", reasonTool: "planner_reason" }; + +function directive(input: { + warrantedWeb: number; + coverage: number; + stale?: number; + friction?: number; +}): string { + const fuel = computeReasoningFuel({ stale: 0, friction: 0, ...input }); + return renderReasoningDirective(fuel, CONTEXT); +} + +describe("renderReasoningDirective — the tone ladder", () => { + it("stays silent when fuel is null (no web warrants the engine)", () => { + expect(directive({ warrantedWeb: 0, coverage: 0 })).toBe(""); + }); + + it("is quiet at ≥70 — a single fuel line, no nagging", () => { + expect(directive({ warrantedWeb: 3, coverage: 3 })).toBe( + "Reasoning fuel: 100", + ); + }); + + it("names the top deficit and a cheap move in the middle band (30–69)", () => { + // W=4, covered 2 ⇒ fuel 60, unmet 2. + const text = directive({ warrantedWeb: 4, coverage: 2 }); + expect(text.startsWith("Reasoning fuel: 60")).toBe(true); + expect(text).toContain("2 declared branches still unmodeled"); + expect(text).toContain("planner_reason"); + // The middle band is one line, not the directing pair. + expect(text).not.toContain("What's needed now"); + }); + + it("switches to the directing tone below 30", () => { + // W=4, covered 0 ⇒ fuel 20. + const text = directive({ warrantedWeb: 4, coverage: 0 }); + expect(text).toContain("Reasoning fuel: 20"); + expect(text).toContain("4 declared branches still unmodeled"); + expect(text).toContain("What's needed now:"); + expect(text).toContain("What's NOT needed now:"); + }); + + it("any friction forces the directing tone even above 30", () => { + // W=2 covered 2 but friction 1 ⇒ fuel 60 (mid band by number) yet R>0. + const text = directive({ warrantedWeb: 2, coverage: 2, friction: 1 }); + expect(text).toContain("thrash, not progress"); + expect(text).toContain("What's needed now:"); + }); + + it("names a stale anchor deficit when it is the top deficit", () => { + // W=0 but two stale anchors ⇒ fuel 33, and stale is the only (top) deficit. + const fuel: ReasoningFuel = computeReasoningFuel({ + warrantedWeb: 0, + coverage: 0, + stale: 2, + friction: 0, + }); + expect(fuel.fuel).toBe(33); + const text = renderReasoningDirective(fuel, CONTEXT); + expect(text).toContain("2 stale anchors"); + }); +}); diff --git a/src/runtime/reason-directive.ts b/src/runtime/reason-directive.ts new file mode 100644 index 0000000..bcaa8ac --- /dev/null +++ b/src/runtime/reason-directive.ts @@ -0,0 +1,94 @@ +import type { ReasoningFuel } from "./reasoning-fuel"; + +/** + * The tone ladder — the ONLY effect a fuel level has. Fuel never blocks; it + * only changes how loudly the directive speaks: + * + * null → silent (nothing warrants the engine here) + * ≥ 70 → quiet: a single "Reasoning fuel: NN" line + * 30–69 → names the top deficit and one cheap next move + * < 30 or R>0 → directing: names the deficit and prescribes a different move, + * with a "what's needed now / not needed now" pair + * + * The texts are templated (signal → text), never generative. A deficit is only + * ever named from the planner's own accounting — warranted web left unmodeled, + * stale anchors, gate thrash — never from anything read out of the engine. + */ + +export interface ReasoningDirectiveContext { + /** + * What the web is made of at this step, as a plural noun the directive can + * drop into a sentence — e.g. "branches", "spec constraints", "shared task + * surfaces". Only used when there is unmet web to name. + */ + webNoun: string; + /** + * The reason move to prescribe, e.g. "planner_reason". Named in the low-fuel + * directing tone so the model knows exactly which tool to reach for. + */ + reasonTool: string; +} + +/** The deficit fragments this fuel names, most-actionable first. */ +function deficitFragments( + fuel: ReasoningFuel, + context: ReasoningDirectiveContext, +): string[] { + const fragments: string[] = []; + if (fuel.unmet > 0) { + fragments.push( + `${fuel.unmet} ${context.webNoun} still unmodeled — run them through ${context.reasonTool}`, + ); + } + if (fuel.stale > 0) { + fragments.push( + `${fuel.stale} stale anchor${fuel.stale === 1 ? "" : "s"}: a source changed since you asserted it — re-assert or retract`, + ); + } + if (fuel.friction > 0) { + fragments.push( + "you re-ran a gate with the same verdict and no change — that is thrash, not progress; change the input or move on", + ); + } + return fragments; +} + +/** + * Render the directive line(s) for a computed fuel, or "" when fuel is null + * (nothing here warrants the engine — stay silent). + */ +export function renderReasoningDirective( + fuel: ReasoningFuel, + context: ReasoningDirectiveContext, +): string { + if (fuel.fuel === null) return ""; + + const level = fuel.fuel; + const fragments = deficitFragments(fuel, context); + + // Any friction (a named thinking pathology) forces the directing tone even at + // otherwise-high fuel — the signal must be surfaced by name. + const directing = fuel.friction > 0 || level < 30; + if (!directing) { + if (level >= 70) { + return `Reasoning fuel: ${level}`; + } + const top = fragments[0] ?? "some web is unmodeled"; + return `Reasoning fuel: ${level} — ${top}.`; + } + + // The directing tone. Name every deficit, then say what is and is not the + // move now. + const named = fragments.length > 0 ? fragments.join("; ") : "the web is thin"; + const needed = + fuel.unmet > 0 + ? `model the remaining ${context.webNoun} with ${context.reasonTool}` + : fuel.stale > 0 + ? "reconcile the stale anchors, then re-check" + : "change what you feed the engine before re-checking"; + return [ + `Reasoning fuel: ${level} — ${named}.`, + `What's needed now: ${needed}.`, + "What's NOT needed now: another identical run — it will not move the verdict.", + ].join("\n"); +} diff --git a/src/runtime/reason-tools.test.ts b/src/runtime/reason-tools.test.ts new file mode 100644 index 0000000..107bdea --- /dev/null +++ b/src/runtime/reason-tools.test.ts @@ -0,0 +1,271 @@ +import { mkdtemp, rm } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import { afterEach, describe, expect, it } from "vitest"; +import type { + GitBranchInput, + GitCommitInput, + GitCreateBranchInput, + GitDeleteBranchInput, + GitMergeInput, + GitRepoInput, + GitRunner, + GitSwitchBranchInput, + GitWorktreeAddInput, + GitWorktreeRemoveInput, +} from "../git/runner"; +import { + type TaskBehavior, + validateTaskBehaviors, + writeTaskBehaviors, +} from "../storage/behavior-store"; +import { createNodeFs } from "../storage/fs"; +import { + createPlanStoragePaths, + createProjectStoragePaths, + createTaskStoragePaths, +} from "../storage/paths"; +import { initializePlanFiles } from "../storage/plan-store"; +import { ensureProjectRecord, setActivePlan } from "../storage/project-store"; +import { + createInitialPlanState, + createPlanRecord, + type PlannerStep, +} from "../storage/schema"; +import { initializePlanState } from "../storage/state-store"; +import { executePlannerReasonTool } from "./reason-tools"; + +// The orchestrator preflight inspects the current branch; the mock reports the +// active plan branch as clean. (Mirrors elenchus-tools.test.ts.) +class MockGitRunner implements GitRunner { + async init(_input: GitRepoInput): Promise {} + async currentBranch(_input: GitRepoInput): Promise { + return "plan/plan-a"; + } + async headCommit(_input: GitRepoInput): Promise { + return "abc123"; + } + async statusPorcelain(_input: GitRepoInput): Promise { + return ""; + } + async diffStat(_input: GitRepoInput): Promise { + return ""; + } + async diffNameOnly(_input: GitRepoInput): Promise { + return ""; + } + async listProjectFiles(_input: GitRepoInput): Promise { + return []; + } + async branchExists(_input: GitBranchInput): Promise { + return true; + } + async createBranch(_input: GitCreateBranchInput): Promise {} + async deleteBranch(_input: GitDeleteBranchInput): Promise {} + async switchBranch(_input: GitSwitchBranchInput): Promise {} + async stageAll(_input: GitRepoInput): Promise {} + async commit(_input: GitCommitInput): Promise {} + async merge(_input: GitMergeInput): Promise {} + async worktreeAdd(_input: GitWorktreeAddInput): Promise {} + async worktreeRemove(_input: GitWorktreeRemoveInput): Promise {} +} + +const git = new MockGitRunner(); +const tempDirs: string[] = []; + +afterEach(async () => { + await Promise.all( + tempDirs.splice(0).map((dir) => rm(dir, { recursive: true, force: true })), + ); +}); + +async function createSetup( + step: PlannerStep = "consistency_check", + stage: "planning" | "execution" = "planning", + activeTaskId: string | null = null, +) { + const root = await mkdtemp(join(tmpdir(), "reason-tools-")); + tempDirs.push(root); + const fs = createNodeFs(); + const projectPaths = createProjectStoragePaths({ + agentDir: join(root, "agent"), + projectRoot: join(root, "repo"), + }); + const planPaths = createPlanStoragePaths(projectPaths, "plan-a"); + const worktreePath = join( + root, + "repo", + ".pi", + "pi-code-planner", + "worktrees", + "plan-a", + ); + await ensureProjectRecord(fs, projectPaths); + await initializePlanFiles( + fs, + planPaths, + createPlanRecord({ planId: "plan-a", title: "Plan A" }), + ); + await fs.mkdirp(worktreePath); + await fs.mkdirp(planPaths.elenchusDir); + await initializePlanState(fs, planPaths, { + ...createInitialPlanState({ + baseBranch: "main", + planBranch: "plan/plan-a", + worktreePath, + }), + stage, + step, + stepStatus: "running", + currentBranch: "plan/plan-a", + activeTaskId, + }); + await setActivePlan(fs, projectPaths, "plan-a"); + return { fs, projectPaths, planPaths, projectRoot: join(root, "repo") }; +} + +function run(setup: { fs: unknown; projectPaths: unknown }, params: unknown) { + return executePlannerReasonTool({ + fs: setup.fs as never, + git, + projectPaths: setup.projectPaths as never, + params, + }); +} + +describe("planner_reason tool", () => { + it("asserts facts into the world and reports a CONSISTENT verdict with raw output", async () => { + const setup = await createSetup(); + const result = await run(setup, { + mode: "assert", + domain: "discovery", + statements: [{ vrf: "FACT cache is_lru" }], + }); + expect(result.status).toBe("applied"); + expect(result.details?.verdict).toBe("CONSISTENT"); + // The raw engine output is present verbatim (JSON verdict body). + expect(result.text).toContain("CONSISTENT"); + expect(result.text).toContain("world verdict"); + }); + + it("surfaces a CONFLICT with the finish_step block hint", async () => { + const setup = await createSetup(); + const result = await run(setup, { + mode: "assert", + domain: "discovery", + statements: [ + { vrf: "FACT db is_postgres" }, + { vrf: "ASSUME db is_sqlite" }, + { + vrf: "PREMISE only_one:\n EXCLUSIVE\n db is_postgres\n db is_sqlite", + }, + ], + }); + expect(result.details?.verdict).toBe("CONFLICT"); + expect(result.text).toContain("CONFLICT"); + expect(result.text).toContain("planner_finish_step stays blocked"); + }); + + it("retract removes a statement and re-checks; unknown ids are reported, never thrown", async () => { + const setup = await createSetup(); + await run(setup, { + mode: "assert", + domain: "discovery", + statements: [{ vrf: "FACT cache is_lru" }], + }); + const removed = await run(setup, { mode: "retract", ids: ["w1"] }); + expect(removed.status).toBe("applied"); + expect(removed.details?.verdict).toBe("CONSISTENT"); + + const missing = await run(setup, { mode: "retract", ids: ["w99"] }); + expect(missing.status).toBe("applied"); + expect(missing.text).toContain("No statements matched w99"); + }); + + it("recheck re-runs the world as-is (an empty world is CONSISTENT)", async () => { + const setup = await createSetup(); + const result = await run(setup, { mode: "recheck" }); + expect(result.status).toBe("applied"); + expect(result.details?.verdict).toBe("CONSISTENT"); + }); + + it("anchors an observation to an existing file and rejects a missing one", async () => { + const setup = await createSetup(); + await setup.fs.writeTextAtomic( + join(setup.projectRoot, "src/cache.ts"), + "export const CACHE = 'lru';\n", + ); + const ok = await run(setup, { + mode: "assert", + domain: "discovery", + statements: [{ vrf: "FACT cache is_lru", anchor: "src/cache.ts" }], + }); + expect(ok.status).toBe("applied"); + + const missing = await run(setup, { + mode: "assert", + domain: "discovery", + statements: [{ vrf: "FACT gone observed", anchor: "src/nope.ts" }], + }); + expect(missing.status).toBe("blocked"); + expect(missing.text).toContain("Cannot anchor"); + }); + + it("rejects an instrument keyword with a mode hint", async () => { + const setup = await createSetup(); + const result = await run(setup, { + mode: "assert", + domain: "discovery", + statements: [{ vrf: "PROVE merge is_blocked" }], + }); + expect(result.status).toBe("blocked"); + expect(result.text).toMatch(/instrument/i); + }); + + it("surfaces the reasoning-fuel directive once a web exists (execution branches)", async () => { + const setup = await createExecSetupWithBranches(["BR-1", "BR-2"]); + const result = await run(setup, { + mode: "assert", + domain: "task_a", + statements: [{ vrf: "FACT br_1 covered" }, { vrf: "FACT br_2 covered" }], + }); + expect(result.status).toBe("applied"); + // A model-authored run on a 2-branch step credits the full web ⇒ fuel 100. + expect(result.details?.fuel).toBe(100); + expect(result.text).toContain("Reasoning fuel: 100"); + }); + + it("stays silent on fuel where no web is warranted (W=0)", async () => { + const setup = await createSetup(); + const result = await run(setup, { mode: "recheck" }); + expect(result.details?.fuel).toBeNull(); + expect(result.text).not.toContain("Reasoning fuel"); + }); +}); + +async function createExecSetupWithBranches(branchIds: string[]) { + const setup = await createSetup("contract_check", "execution", "task-a"); + const behavior: TaskBehavior = { + id: "BHV-1", + statement: "Adds a dependency with cycle rejection", + kind: "error", + requirement: null, + test: null, + branches: branchIds.map((id) => ({ + id, + condition: `${id} condition`, + covered: false, + })), + status: "planned", + }; + await writeTaskBehaviors( + setup.fs, + createTaskStoragePaths(setup.planPaths, "task-a"), + validateTaskBehaviors({ + taskId: "task-a", + behaviors: [behavior], + previous: null, + }), + ); + return setup; +} diff --git a/src/runtime/reason-tools.ts b/src/runtime/reason-tools.ts new file mode 100644 index 0000000..46d9fe9 --- /dev/null +++ b/src/runtime/reason-tools.ts @@ -0,0 +1,311 @@ +import { join } from "node:path"; +import { errorMessage } from "../errors"; +import { sha256 } from "../hash"; +import type { PlanStoragePaths } from "../storage/paths"; +import type { PlanStateRecord } from "../storage/schema"; +import { readSpecRecordIfExists } from "../storage/spec-store"; +import { syncVrfTemplatesToPlan } from "../vrf/manager"; +import { + assertWorldStatements, + retractWorldStatements, + runWorldCheck, + type WorldStatementInput, + type WorldVerdict, +} from "../vrf/world-store"; +import { + type ElenchusLastCheckRecord, + writeElenchusLastCheck, +} from "./elenchus-tools"; +import { + checkPlannerOrchestratorToolAllowed, + runPlannerOrchestrator, +} from "./orchestrator"; +import { loadStepReasoningFuel } from "./reason-context"; +import { renderReasoningDirective } from "./reason-directive"; +import type { PlannerToolContext } from "./tool-context"; +import { blockedResult } from "./tool-result"; + +export const PLANNER_REASON_TOOL_NAME = "planner_reason" as const; +export type PlannerReasonToolName = typeof PLANNER_REASON_TOOL_NAME; + +export interface PlannerReasonToolInput extends PlannerToolContext { + params: unknown; +} + +export interface PlannerReasonToolResult { + status: "applied" | "blocked"; + toolName: PlannerReasonToolName; + text: string; + details: { + mode: "assert" | "retract" | "recheck"; + verdict: WorldVerdict | null; + fuel: number | null; + } | null; +} + +interface AssertStatement { + vrf: string; + /** Project-root-relative file to anchor this observation to (the tool hashes it). */ + anchor?: string; +} + +type ReasonParams = + | { mode: "assert"; domain: string; statements: AssertStatement[] } + | { mode: "retract"; ids: string[] } + | { mode: "recheck" }; + +/** + * `planner_reason` — the model's handle on the living elenchus world. It never + * hands the model a parsed report: it runs the whole world through the engine, + * scans the verdict, and returns the raw output verbatim plus the step's + * reasoning-fuel directive. Three modes: + * + * assert — add FACT/PREMISE/RULE/… statements to a domain, then re-check; + * observations may name a file to anchor to (hashed here, so stale + * knowledge later demotes to belief instead of a false CONFLICT). + * retract — remove statements by id, then re-check; always succeeds (the + * anti-deadlock escape). + * recheck — re-run the world as-is (cheap orientation). + * + * Gated exactly like planner_elenchus_check: allowed only where both + * guard/tool-policy and stage-behavior list it (the six reasoning steps). + */ +export async function executePlannerReasonTool( + input: PlannerReasonToolInput, +): Promise { + try { + const orchestrator = await runPlannerOrchestrator(input); + if (orchestrator.preflight.context.status !== "ready") { + return blocked(orchestrator.preflight.context.reason); + } + const policy = checkPlannerOrchestratorToolAllowed({ + orchestrator, + toolName: PLANNER_REASON_TOOL_NAME, + }); + if (!policy.allow) { + return blocked( + policy.reason ?? "planner_reason is blocked by planner state.", + ); + } + + const { planPaths, state } = orchestrator.preflight.context; + const params = parseReasonParams(input.params); + + // The spec template must resolve when the world compiles the spec layer. + await syncVrfTemplatesToPlan(input.fs, { + projectPaths: input.projectPaths, + planPaths, + }); + + if (params.mode === "assert") { + const inputs = await buildAssertInputs(input, state, params); + // Validates every statement up front; a bad one throws → blocked, and + // nothing is written (all-or-nothing). + await assertWorldStatements(input.fs, planPaths, inputs); + } else if (params.mode === "retract") { + const { removed, missing } = await retractWorldStatements( + input.fs, + planPaths, + params.ids, + ); + if (removed.length === 0 && missing.length > 0) { + // Still re-check below, but tell the model none of its ids matched. + return await finishRun(input, planPaths, state, params.mode, { + note: `No statements matched ${missing.join(", ")}. Nothing was retracted.`, + }); + } + } + + return await finishRun(input, planPaths, state, params.mode, {}); + } catch (error) { + return blocked(errorMessage(error)); + } +} + +async function finishRun( + input: PlannerReasonToolInput, + planPaths: PlanStoragePaths, + state: PlanStateRecord, + mode: ReasonParams["mode"], + opts: { note?: string }, +): Promise { + const elenchusDir = planPaths.elenchusDir; + + const spec = await readSpecRecordIfExists(input.fs, planPaths); + const run = await runWorldCheck(input.fs, planPaths, { + spec, + hashProjectFile: (path) => hashProjectFile(input, path), + }); + if (!run.ok) return blocked(run.reason); + + const record: ElenchusLastCheckRecord = { + name: "world", + stage: state.stage, + step: state.step, + outcome: run.verdict, + recordedAt: new Date().toISOString(), + }; + await writeElenchusLastCheck(input.fs, elenchusDir, record); + + const { fuel, webNoun } = await loadStepReasoningFuel({ + fs: input.fs, + planPaths, + state, + stale: run.compiled.demoted.length, + lastCheck: record, + }); + const directive = renderReasoningDirective(fuel, { + webNoun, + reasonTool: PLANNER_REASON_TOOL_NAME, + }); + + const consistent = run.verdict === "CONSISTENT"; + const text = [ + `planner_reason ${mode} → world verdict: ${run.verdict} (${run.engineVersion}).`, + ...(opts.note ? [opts.note] : []), + "", + run.output, + "", + consistent + ? "CONSISTENT: the whole living world holds. Record the conclusion, then continue." + : run.verdict === "CONFLICT" + ? "CONFLICT: a proven contradiction in the world. planner_finish_step stays blocked for this step until a re-run improves the verdict. Apply the drop/flip the output names, or retract the wrong statement — never delete a valid premise to force green — then re-check." + : "Not CONSISTENT yet. Read the output: assert the FACT/NOT it names, pin down an UNDERDETERMINED atom, or fix the wrong statement — then re-check.", + ...(directive ? ["", directive] : []), + "", + "Call planner_status before choosing the next planner action.", + ].join("\n"); + + return { + status: "applied", + toolName: PLANNER_REASON_TOOL_NAME, + text, + details: { mode, verdict: run.verdict, fuel: fuel.fuel }, + }; +} + +async function buildAssertInputs( + input: PlannerReasonToolInput, + state: { stage: string; step: string }, + params: Extract, +): Promise { + const origin = { stage: state.stage, step: state.step }; + const inputs: WorldStatementInput[] = []; + for (const statement of params.statements) { + const lines = statement.vrf.split("\n"); + const base: WorldStatementInput = { + lines, + domain: params.domain, + origin, + }; + if (statement.anchor) { + const hash = await hashProjectFile(input, statement.anchor); + if (hash === null) { + throw new Error( + `Cannot anchor to "${statement.anchor}": no such file under the project root. Assert the observation without an anchor, or fix the path.`, + ); + } + inputs.push({ ...base, anchor: { path: statement.anchor, hash } }); + } else { + inputs.push(base); + } + } + return inputs; +} + +/** sha256 of a project-root-relative file, or null when it does not exist. */ +async function hashProjectFile( + input: PlannerReasonToolInput, + path: string, +): Promise { + const absolute = join(input.projectPaths.projectRoot, path); + if (!(await input.fs.exists(absolute))) return null; + try { + return sha256(await input.fs.readText(absolute)); + } catch { + return null; + } +} + +function parseReasonParams(value: unknown): ReasonParams { + const record = asObject(value); + const mode = record.mode; + if (mode === "assert") { + return { + mode: "assert", + domain: requiredString(record, "domain"), + statements: parseStatements(record.statements), + }; + } + if (mode === "retract") { + return { mode: "retract", ids: parseIds(record.ids) }; + } + if (mode === "recheck") { + return { mode: "recheck" }; + } + throw new TypeError( + 'planner_reason.mode must be "assert", "retract", or "recheck".', + ); +} + +function parseStatements(value: unknown): AssertStatement[] { + if (!Array.isArray(value) || value.length === 0) { + throw new TypeError( + "planner_reason.statements must be a non-empty array when mode=assert.", + ); + } + return value.map((entry, index) => { + const record = asObject(entry, `statements[${index}]`); + const vrf = record.vrf; + if (typeof vrf !== "string" || vrf.trim().length === 0) { + throw new TypeError( + `planner_reason.statements[${index}].vrf must be a non-empty .vrf string.`, + ); + } + const anchor = record.anchor; + if (anchor !== undefined && typeof anchor !== "string") { + throw new TypeError( + `planner_reason.statements[${index}].anchor must be a project-root-relative file path.`, + ); + } + return anchor ? { vrf, anchor } : { vrf }; + }); +} + +function parseIds(value: unknown): string[] { + if (!Array.isArray(value) || value.length === 0) { + throw new TypeError( + "planner_reason.ids must be a non-empty array of statement ids when mode=retract.", + ); + } + return value.map((id, index) => { + if (typeof id !== "string" || id.trim().length === 0) { + throw new TypeError( + `planner_reason.ids[${index}] must be a non-empty statement id (e.g. "w3").`, + ); + } + return id.trim(); + }); +} + +function requiredString(record: Record, key: string): string { + const value = record[key]; + if (typeof value !== "string" || value.trim().length === 0) { + throw new TypeError(`planner_reason.${key} must be a non-empty string.`); + } + return value.trim(); +} + +function asObject( + value: unknown, + where = "parameters", +): Record { + if (!value || typeof value !== "object" || Array.isArray(value)) { + throw new TypeError(`planner_reason ${where} must be an object.`); + } + return value as Record; +} + +function blocked(text: string): PlannerReasonToolResult { + return blockedResult(PLANNER_REASON_TOOL_NAME, text); +} diff --git a/src/runtime/reasoning-fuel-surfacing.test.ts b/src/runtime/reasoning-fuel-surfacing.test.ts new file mode 100644 index 0000000..134c998 --- /dev/null +++ b/src/runtime/reasoning-fuel-surfacing.test.ts @@ -0,0 +1,180 @@ +import { join } from "node:path"; +import { describe, expect, it } from "vitest"; +import { + createPlanStoragePaths, + createProjectStoragePaths, + type PlanStoragePaths, +} from "../storage/paths"; +import { initializePlanFiles } from "../storage/plan-store"; +import { ensureProjectRecord, setActivePlan } from "../storage/project-store"; +import { + createInitialPlanState, + createPlanRecord, + type PlanStateRecord, +} from "../storage/schema"; +import { validateSpecRecord, writeSpecArtifacts } from "../storage/spec-store"; +import { initializePlanState } from "../storage/state-store"; +import { MockPlannerFs } from "../test/mock-fs"; +import { formatTransitionReasoningFuelTail } from "./status"; + +/** + * The reasoning-fuel nudge must reach the model in the drive loop — on the tail + * of an applied workflow transition (planner_finish_step), not only on a rare + * planner_status call. formatTransitionReasoningFuelTail is that seam. These + * tests pin the gate condition (only on an applied transition against a ready + * plan) and the self-silencing (empty when no web, present when a web or + * friction warrants the engine). + */ + +async function setupPlan(overrides: Partial): Promise<{ + fs: MockPlannerFs; + planPaths: PlanStoragePaths; + state: PlanStateRecord; +}> { + const fs = new MockPlannerFs(); + const projectPaths = createProjectStoragePaths({ + agentDir: "/agent", + projectRoot: "/repo/app", + }); + const planPaths = createPlanStoragePaths(projectPaths, "plan-a"); + const worktreePath = "/repo/app/.pi/pi-code-planner/worktrees/plan-a"; + await ensureProjectRecord(fs, projectPaths); + await initializePlanFiles( + fs, + planPaths, + createPlanRecord({ planId: "plan-a", title: "Plan A" }), + ); + await fs.mkdirp(worktreePath); + const state: PlanStateRecord = { + ...createInitialPlanState({ + baseBranch: "main", + planBranch: "plan/plan-a", + worktreePath, + }), + stage: "planning", + step: "consistency_check", + stepStatus: "running", + currentBranch: "plan/plan-a", + ...overrides, + }; + await initializePlanState(fs, planPaths, state); + await setActivePlan(fs, projectPaths, "plan-a"); + return { fs, planPaths, state }; +} + +async function writeSpecWithConstraints( + fs: MockPlannerFs, + planPaths: PlanStoragePaths, + count: number, +): Promise { + await writeSpecArtifacts( + fs, + planPaths, + validateSpecRecord({ + requirements: [ + { + id: "REQ-1", + statement: "Behavior.", + acceptance: "Checked.", + acceptanceAtom: "req_1_ok", + priority: "must", + inScope: true, + }, + ], + constraints: Array.from({ length: count }, (_, i) => ({ + id: `CON-${i + 1}`, + statement: `Constraint ${i + 1}.`, + kind: "invariant" as const, + })), + }), + ); +} + +describe("formatTransitionReasoningFuelTail", () => { + it("stays empty when the transition did not apply", async () => { + const { fs, planPaths, state } = await setupPlan({}); + await writeSpecWithConstraints(fs, planPaths, 2); + const tail = await formatTransitionReasoningFuelTail({ + fs, + status: "blocked", + planPaths, + state, + }); + expect(tail).toBe(""); + }); + + it("stays empty when no plan is ready (no planPaths or state)", async () => { + const { fs, planPaths, state } = await setupPlan({}); + await writeSpecWithConstraints(fs, planPaths, 2); + expect( + await formatTransitionReasoningFuelTail({ + fs, + status: "applied", + planPaths: undefined, + state, + }), + ).toBe(""); + expect( + await formatTransitionReasoningFuelTail({ + fs, + status: "applied", + planPaths, + state: null, + }), + ).toBe(""); + }); + + it("surfaces the fuel nudge on an applied transition that lands on a webby step", async () => { + const { fs, planPaths, state } = await setupPlan({}); + await writeSpecWithConstraints(fs, planPaths, 2); + const tail = await formatTransitionReasoningFuelTail({ + fs, + status: "applied", + planPaths, + state, + }); + expect(tail).toContain("Reasoning fuel:"); + expect(tail).toContain("## Reasoning Fuel"); + expect(tail).toContain("spec constraints"); + }); + + it("stays silent on an applied transition with no interacting-condition web", async () => { + const { fs, planPaths, state } = await setupPlan({}); + // consistency_check with a spec that declares zero constraints ⇒ W = 0. + await writeSpecWithConstraints(fs, planPaths, 0); + const tail = await formatTransitionReasoningFuelTail({ + fs, + status: "applied", + planPaths, + state, + }); + expect(tail).toBe(""); + }); + + it("surfaces gate-thrash friction even when the step has no web", async () => { + const { fs, planPaths, state } = await setupPlan({}); + // No spec ⇒ W = 0, but a gate re-run with the same verdict (repeat ≥ 2) + // is friction — the one signal that fired in the real 1-hour run. + await fs.writeTextAtomic( + join(planPaths.elenchusDir, "last-check.json"), + JSON.stringify({ + name: "plan-gate", + stage: "planning", + step: "consistency_check", + outcome: "CONSISTENT", + recordedAt: "2026-07-05T00:00:00.000Z", + gate: "plan_coverage", + sourceHash: "abc", + repeat: 2, + }), + ); + const tail = await formatTransitionReasoningFuelTail({ + fs, + status: "applied", + planPaths, + state, + }); + expect(tail).toContain("Reasoning fuel:"); + expect(tail).toContain("thrash"); + }); +}); diff --git a/src/runtime/reasoning-fuel.test.ts b/src/runtime/reasoning-fuel.test.ts new file mode 100644 index 0000000..c3e1543 --- /dev/null +++ b/src/runtime/reasoning-fuel.test.ts @@ -0,0 +1,253 @@ +import { describe, expect, it } from "vitest"; +import { SCHEMA_VERSION } from "../constants"; +import type { TaskRecord } from "../storage/schema"; +import type { SpecConstraint, SpecRecord } from "../storage/spec-store"; +import { + computeReasoningFuel, + coverageFromLastCheck, + type FuelLastCheck, + frictionFromLastCheck, + sharedTaskSurfaces, + warrantedWebFromBranches, + warrantedWebFromSpecConstraints, +} from "./reasoning-fuel"; + +function fuel(input: { + warrantedWeb: number; + coverage: number; + stale?: number; + friction?: number; +}): number | null { + return computeReasoningFuel({ + stale: 0, + friction: 0, + ...input, + }).fuel; +} + +describe("computeReasoningFuel — the 2×2 incentive", () => { + it("no web, no stale, no friction ⇒ null (silent; the engine is not warranted)", () => { + expect(fuel({ warrantedWeb: 0, coverage: 0 })).toBeNull(); + }); + + it("running the engine where there is no web earns nothing (null, not 100)", () => { + // Coverage is capped at the warranted web, so a run on a W=0 step cannot + // manufacture credit — the anti-ritual property. + expect(fuel({ warrantedWeb: 0, coverage: 5 })).toBeNull(); + }); + + it("a web fully modeled with no stale/friction ⇒ ~100 (the quiet good path)", () => { + expect(fuel({ warrantedWeb: 3, coverage: 3 })).toBe(100); + }); + + it("a web left entirely unmodeled ⇒ low fuel, scaled to the web ignored", () => { + // The anti-laziness property, with a gradient: bigger ignored web bites more. + expect(fuel({ warrantedWeb: 1, coverage: 0 })).toBe(50); + expect(fuel({ warrantedWeb: 3, coverage: 0 })).toBe(25); + expect(fuel({ warrantedWeb: 4, coverage: 0 })).toBe(20); + }); + + it("partial coverage lands between (a genuine gradient)", () => { + // W=4, modeled 2 ⇒ unmet 2 ⇒ round(100*(1-2/5)) = 60. + expect(fuel({ warrantedWeb: 4, coverage: 2 })).toBe(60); + }); +}); + +describe("computeReasoningFuel — stale and friction", () => { + it("stale anchors alone drag fuel down and keep it non-null", () => { + const result = computeReasoningFuel({ + warrantedWeb: 0, + coverage: 0, + stale: 2, + friction: 0, + }); + // round(100*(1 - 2/(0+2+0+1))) = round(33.3) = 33. + expect(result.fuel).toBe(33); + }); + + it("friction alone drags fuel down and keeps it non-null", () => { + expect(fuel({ warrantedWeb: 0, coverage: 0, friction: 1 })).toBe(50); + }); + + it("a fully modeled web still dips when an anchor is stale", () => { + // W=2 covered, one stale: deficit 1 over denom (2+1+0+1)=4 ⇒ 75. + expect(fuel({ warrantedWeb: 2, coverage: 2, stale: 1 })).toBe(75); + }); +}); + +describe("computeReasoningFuel — clamping and structure", () => { + it("clamps coverage into [0, warrantedWeb] and floors negatives", () => { + expect(fuel({ warrantedWeb: 3, coverage: 9 })).toBe(100); + expect(fuel({ warrantedWeb: 3, coverage: -4 })).toBe(25); + }); + + it("reports the derived pieces the directive names", () => { + const result = computeReasoningFuel({ + warrantedWeb: 4, + coverage: 1, + stale: 1, + friction: 1, + }); + expect(result.unmet).toBe(3); + expect(result.stale).toBe(1); + expect(result.friction).toBe(1); + // deficit 5 over denom (4+1+1+1)=7 ⇒ round(100*(1-5/7)) = 29. + expect(result.fuel).toBe(29); + }); + + it("truncates fractional inputs deterministically", () => { + expect(fuel({ warrantedWeb: 3.9, coverage: 0.9 })).toBe( + fuel({ warrantedWeb: 3, coverage: 0 }), + ); + }); +}); + +describe("warranted-web collectors", () => { + it("counts declared branches", () => { + expect(warrantedWebFromBranches([])).toBe(0); + expect( + warrantedWebFromBranches([ + { id: "BR-1" }, + { id: "BR-2" }, + { id: "BR-3" }, + ]), + ).toBe(3); + }); + + it("counts declared spec constraints", () => { + expect(warrantedWebFromSpecConstraints(specWithConstraints(0))).toBe(0); + expect(warrantedWebFromSpecConstraints(specWithConstraints(2))).toBe(2); + }); + + it("counts only surfaces two or more tasks share", () => { + const tasks = [ + task("t1", ["src/a.ts", "src/b.ts"]), + task("t2", ["src/b.ts", "src/c.ts"]), + task("t3", ["src/c.ts"]), + ]; + // b.ts (t1,t2) and c.ts (t2,t3) are shared; a.ts is not. + expect(sharedTaskSurfaces(tasks)).toBe(2); + }); + + it("no shared surface ⇒ no cross-task web", () => { + const tasks = [task("t1", ["src/a.ts"]), task("t2", ["src/b.ts"])]; + expect(sharedTaskSurfaces(tasks)).toBe(0); + }); +}); + +describe("engagement — coverageFromLastCheck", () => { + const base = { warrantedWeb: 3, stage: "execution", step: "contract_check" }; + + it("a model-authored qualifying run on this step grants the full web", () => { + expect( + coverageFromLastCheck({ + ...base, + lastCheck: lastCheck({ outcome: "CONSISTENT" }), + }), + ).toBe(3); + }); + + it("credits engagement even on a CONFLICT (honest work is not punished)", () => { + expect( + coverageFromLastCheck({ + ...base, + lastCheck: lastCheck({ outcome: "CONFLICT" }), + }), + ).toBe(3); + }); + + it("a gate run is the mechanical floor, not the model's reasoning ⇒ 0", () => { + expect( + coverageFromLastCheck({ + ...base, + lastCheck: lastCheck({ + outcome: "CONSISTENT", + gate: "spec_consistency", + }), + }), + ).toBe(0); + }); + + it("a check on a different step is stale for this one ⇒ 0", () => { + expect( + coverageFromLastCheck({ + ...base, + lastCheck: lastCheck({ outcome: "CONSISTENT", step: "write_tdd_plan" }), + }), + ).toBe(0); + }); + + it("a not_applicable escape is not engagement ⇒ 0", () => { + expect( + coverageFromLastCheck({ + ...base, + lastCheck: lastCheck({ outcome: "not_applicable" }), + }), + ).toBe(0); + }); + + it("no check at all ⇒ 0", () => { + expect(coverageFromLastCheck({ ...base, lastCheck: null })).toBe(0); + }); +}); + +describe("friction — frictionFromLastCheck", () => { + it("fires when a gate re-ran twice with the same verdict + source", () => { + expect(frictionFromLastCheck(lastCheck({ repeat: 2 }))).toBe(1); + expect(frictionFromLastCheck(lastCheck({ repeat: 5 }))).toBe(1); + }); + + it("does not fire on a first run or a single legitimate re-run", () => { + expect(frictionFromLastCheck(lastCheck({}))).toBe(0); + expect(frictionFromLastCheck(lastCheck({ repeat: 1 }))).toBe(0); + expect(frictionFromLastCheck(null)).toBe(0); + }); +}); + +function lastCheck(overrides: Partial): FuelLastCheck { + return { + stage: "execution", + step: "contract_check", + outcome: "CONSISTENT", + ...overrides, + }; +} + +function specWithConstraints(count: number): SpecRecord { + const constraints: SpecConstraint[] = Array.from( + { length: count }, + (_, i) => ({ + id: `CON-${i + 1}`, + statement: `constraint ${i + 1}`, + kind: "invariant", + }), + ); + return { + schemaVersion: SCHEMA_VERSION, + requirements: [ + { + id: "REQ-1", + statement: "s", + acceptance: "a", + acceptanceAtom: "req_1_ok", + priority: "must", + inScope: true, + }, + ], + nonGoals: [], + constraints, + assumptions: [], + }; +} + +function task(taskId: string, scope: string[]): TaskRecord { + return { + schemaVersion: SCHEMA_VERSION, + taskId, + title: taskId, + status: "pending", + objective: "o", + scope, + acceptanceCriteria: [], + }; +} diff --git a/src/runtime/reasoning-fuel.ts b/src/runtime/reasoning-fuel.ts new file mode 100644 index 0000000..4cf6669 --- /dev/null +++ b/src/runtime/reasoning-fuel.ts @@ -0,0 +1,194 @@ +import type { TaskRecord } from "../storage/schema"; +import type { SpecRecord } from "../storage/spec-store"; + +/** + * Reasoning fuel: a deterministic scalar that pulls the model toward the + * elenchus engine where a genuine web of interacting conditions is on the + * table, and stays neutral where there is none. It is computed entirely from + * the planner's OWN artifacts (behavior-board branches, spec constraints, the + * task graph) and its own records (the last-check verdict enum, its repeat + * counter, the compiler's stale-anchor sweep). It never reads a field of the + * engine's report beyond the verdict code — that is the whole point of the + * redesign, and the guard against re-coupling to the engine's private JSON. + * + * The shape of the incentive is a 2×2: + * + * | | no web (W=0) | web (W>0) | + * | ran elenchus | null (neutral) | ~100 (quiet, good path) | + * | skipped elenchus | null (correct) | low fuel (nudge: lazy) | + * + * Running the engine where there is no web earns nothing (W caps coverage) and + * costs nothing (fuel stays null): no ritual incentive, no punishment. + * Skipping it where a web exists depletes fuel in proportion to the web left + * unmodeled. Fuel never blocks anything — its only effect is the tone of the + * directive the status/tool-tail renders. The hard floors stay on named + * terminal defects (a CONFLICT verdict, an un-CONSISTENT gate), never on fuel. + */ + +export interface ReasoningFuelInput { + /** Warranted web: how much interacting-condition structure is on the table. */ + warrantedWeb: number; + /** How much of the web the model actually ran through the engine (0..W). */ + coverage: number; + /** Stale anchors scoped to this step, from the planner's own hash sweep. */ + stale: number; + /** Behavioral friction (gate thrash), from the planner's own records. */ + friction: number; +} + +export interface ReasoningFuel { + /** + * 0..100, or null when there is no web, no stale anchor, and no friction — + * i.e. nothing here warrants the engine, so the directive stays silent. + */ + fuel: number | null; + warrantedWeb: number; + coverage: number; + /** Warranted web the model did not run through the engine. */ + unmet: number; + stale: number; + friction: number; +} + +/** + * The core math. Deterministic, pure, and blind to the engine's report: + * + * unmet = max(0, W - coverage) + * deficit = unmet + stale + friction + * fuel = round(100 * (1 - deficit / (W + stale + friction + 1))) + * + * The `+1` in the denominator gives a gradient (one unmet unit of a 1-web step + * lands at 50, of a 4-web step at 20) and guards the divide. Coverage is capped + * at the warranted web so a run on a no-web step can never manufacture credit. + */ +export function computeReasoningFuel(input: ReasoningFuelInput): ReasoningFuel { + const warrantedWeb = Math.max(0, Math.trunc(input.warrantedWeb)); + const coverage = Math.min( + warrantedWeb, + Math.max(0, Math.trunc(input.coverage)), + ); + const stale = Math.max(0, Math.trunc(input.stale)); + const friction = Math.max(0, Math.trunc(input.friction)); + const unmet = warrantedWeb - coverage; + if (warrantedWeb === 0 && stale === 0 && friction === 0) { + return { fuel: null, warrantedWeb, coverage, unmet, stale, friction }; + } + const deficit = unmet + stale + friction; + const denominator = warrantedWeb + stale + friction + 1; + const fuel = Math.round(100 * (1 - deficit / denominator)); + return { fuel, warrantedWeb, coverage, unmet, stale, friction }; +} + +// --------------------------------------------------------------------------- +// demand collectors — warranted web, from the planner's own artifacts +// --------------------------------------------------------------------------- + +/** + * The web an execution step (write_tdd_plan / contract_check) warrants: the + * number of branches the active task declared on its behavior board. This is + * the strongest, already-proven demand signal — the branch-contract in + * elenchus-tools already forces a checked program to model every one of them. + */ +export function warrantedWebFromBranches( + branches: readonly { id: string }[], +): number { + return branches.length; +} + +/** + * The web a consistency_check step warrants: the number of interacting + * constraints the model itself declared in the spec. Zero constraints ⇒ no + * declared interaction ⇒ no pressure; we never invent a web the artifacts do + * not show. + */ +export function warrantedWebFromSpecConstraints(spec: SpecRecord): number { + return spec.constraints.length; +} + +/** + * The web a doubt_review step warrants: the number of surfaces (scope + * entries — files/areas) that two or more tasks share. Shared surfaces are + * where cross-task interactions actually live; a plan whose tasks touch + * disjoint surfaces has no cross-task web to check. + */ +export function sharedTaskSurfaces(tasks: readonly TaskRecord[]): number { + const counts = new Map(); + for (const task of tasks) { + for (const entry of task.scope ?? []) { + const key = entry.trim(); + if (!key) continue; + counts.set(key, (counts.get(key) ?? 0) + 1); + } + } + let shared = 0; + for (const count of counts.values()) { + if (count >= 2) shared += 1; + } + return shared; +} + +// --------------------------------------------------------------------------- +// engagement + friction — from the planner's own last-check record +// --------------------------------------------------------------------------- + +/** + * The minimal shape of the last-check record the fuel layer reads. Structurally + * a subset of {@link import("./elenchus-tools").ElenchusLastCheckRecord}; kept + * local so the fuel math depends on no store and stays trivially testable. + */ +export interface FuelLastCheck { + stage: string; + step: string; + outcome: string; + /** Set on gate runs (compiler-authored); a model-authored run leaves it unset. */ + gate?: string; + /** How many times in a row the same gate re-ran with the same verdict + source. */ + repeat?: number; +} + +/** + * Verdicts that count as the model having engaged the engine. CONFLICT is + * included on purpose: surfacing a real contradiction is honest engagement, so + * fuel does not punish it — the existing CONFLICT-block on finish_step is what + * keeps the step from advancing until the contradiction is resolved. + */ +export const QUALIFYING_VERDICTS: ReadonlySet = new Set([ + "CONSISTENT", + "WARNING", + "UNDERDETERMINED", + "CONFLICT", +]); + +/** + * Coverage from the last check: the full warranted web if a *model-authored* + * qualifying run happened on this very step, else 0. Gate runs (compiler + * -authored, `gate` set) are the mechanical floor, not the model's own + * reasoning about the web, so they never grant coverage. A check recorded on a + * different step is stale for this one — coverage resets when the step changes. + */ +export function coverageFromLastCheck(input: { + warrantedWeb: number; + lastCheck: FuelLastCheck | null; + stage: string; + step: string; +}): number { + const { lastCheck } = input; + if (!lastCheck) return 0; + if (lastCheck.gate !== undefined) return 0; + if (lastCheck.stage !== input.stage || lastCheck.step !== input.step) { + return 0; + } + return QUALIFYING_VERDICTS.has(lastCheck.outcome) + ? Math.max(0, Math.trunc(input.warrantedWeb)) + : 0; +} + +/** + * Gate-thrash friction: 1 when the latest gate re-ran two or more times with + * the same verdict AND the same source hash (its `repeat` counter reached 2), + * else 0. A legitimate re-run after a real change resets the counter, so it + * never fires on progress. + */ +export function frictionFromLastCheck(lastCheck: FuelLastCheck | null): number { + return lastCheck && (lastCheck.repeat ?? 0) >= 2 ? 1 : 0; +} diff --git a/src/runtime/simplified-flow.test.ts b/src/runtime/simplified-flow.test.ts index f356761..2f3e4ff 100644 --- a/src/runtime/simplified-flow.test.ts +++ b/src/runtime/simplified-flow.test.ts @@ -71,6 +71,7 @@ describe("simplified local-model workflow", () => { "planner_contract_read", "planner_contract_upsert", "planner_elenchus_check", + "planner_reason", "planner_git_commit", "planner_exec", ]); diff --git a/src/runtime/stage-behavior.ts b/src/runtime/stage-behavior.ts index e3f1981..54d0d2c 100644 --- a/src/runtime/stage-behavior.ts +++ b/src/runtime/stage-behavior.ts @@ -218,6 +218,7 @@ export const PLANNER_STAGE_BEHAVIOR = { "planner_contract_read", "planner_contract_upsert", "planner_elenchus_check", + "planner_reason", "planner_git_commit", "planner_exec", ], @@ -360,6 +361,7 @@ export const PLANNER_STAGE_BEHAVIOR = { "planner_status", "planner_gate_check", "planner_elenchus_check", + "planner_reason", "planner_task_upsert", "planner_contract_route", "planner_contract_read", @@ -401,6 +403,7 @@ export const PLANNER_STAGE_BEHAVIOR = { "planner_skill_create", "planner_skill_update", "planner_elenchus_check", + "planner_reason", "planner_debug_strategy", "planner_debug_probe", "planner_debug_result", @@ -493,6 +496,7 @@ export const PLANNER_STAGE_BEHAVIOR = { "planner_contract_route", "planner_contract_read", "planner_elenchus_check", + "planner_reason", "planner_git_commit", "planner_report_stuck", "planner_skill_create", @@ -624,6 +628,7 @@ export const PLANNER_STAGE_BEHAVIOR = { "planner_git_inspect", "planner_doubt_review", "planner_elenchus_check", + "planner_reason", "planner_skill_create", "planner_skill_update", "planner_contract_check", @@ -780,7 +785,11 @@ export const PLANNER_STAGE_BEHAVIOR = { requiredArtifacts: ["state.json", "decisions.md"], updatedArtifacts: ["state.json"], requiredGates: ["user_repair_decision"], - expectedTools: ["planner_recovery_resume", "planner_elenchus_check"], + expectedTools: [ + "planner_recovery_resume", + "planner_elenchus_check", + "planner_reason", + ], commitPolicy: "forbidden", compactPolicy: "not_allowed", }), diff --git a/src/runtime/status.ts b/src/runtime/status.ts index bacd957..bc8be8e 100644 --- a/src/runtime/status.ts +++ b/src/runtime/status.ts @@ -8,6 +8,7 @@ import type { } from "../instructions/schema"; import { loadEffectivePlannerSettings } from "../settings/manager"; import type { PlannerFs } from "../storage/fs"; +import type { PlanStoragePaths } from "../storage/paths"; import type { PlannerStage, PlannerStep, @@ -23,6 +24,9 @@ import { } from "./lifecycle"; import { filterPlannerWrapperToolsForLifecycle } from "./orchestrator-gate"; import type { PlannerPreflightResult } from "./preflight"; +import { loadStepReasoningFuel } from "./reason-context"; +import { renderReasoningDirective } from "./reason-directive"; +import { PLANNER_REASON_TOOL_NAME } from "./reason-tools"; import { listActivePlannerSkillSummaries, type PlannerSkillSummary, @@ -952,6 +956,74 @@ export const PLANNER_STEP_RULES = { }), } as const satisfies Record; +/** + * The "## Reasoning Fuel" section, or [] when nothing here warrants the engine + * (the directive is empty). Computed from the planner's own artifacts + records + * only; never reads the engine's report. Staleness is left to the reason tool's + * own run — status renders the lighter web-vs-engagement view. + */ +async function formatReasoningFuelSection( + fs: PlannerFs, + planPaths: PlanStoragePaths, + state: PlanStateRecord, +): Promise { + const { fuel, webNoun } = await loadStepReasoningFuel({ + fs, + planPaths, + state, + }); + const directive = renderReasoningDirective(fuel, { + webNoun, + reasonTool: PLANNER_REASON_TOOL_NAME, + }); + return directive ? ["## Reasoning Fuel", directive, ""] : []; +} + +/** + * The "## Reasoning Fuel" block as a single trailing string (or "" when nothing + * here warrants the engine). Purely presentational. + */ +async function formatReasoningFuelLine(input: { + fs: PlannerFs; + planPaths: PlanStoragePaths; + state: PlanStateRecord; +}): Promise { + const section = await formatReasoningFuelSection( + input.fs, + input.planPaths, + input.state, + ); + return section.length > 0 ? section.join("\n").trimEnd() : ""; +} + +/** + * The reasoning-fuel nudge for the step a just-run workflow transition landed + * on, or "" when the transition did not apply, no plan was ready, or nothing + * here warrants the engine. Lets a transition ride the same nudge the model + * would otherwise only see on a rare planner_status call — surfaced on the tail + * of e.g. planner_finish_step, the tool the model actually reads each step. + * + * This is the sanctioned surfacing seam: it lives in the surfacing layer + * (status), so the tool dispatcher that calls it never imports a fuel module + * and the tone-only invariant holds. Presentational only — the fuel level + * enters no allow/block decision here or anywhere. + */ +export async function formatTransitionReasoningFuelTail(input: { + fs: PlannerFs; + status: string; + planPaths: PlanStoragePaths | undefined; + state: PlanStateRecord | null; +}): Promise { + if (input.status !== "applied" || !input.planPaths || !input.state) { + return ""; + } + return formatReasoningFuelLine({ + fs: input.fs, + planPaths: input.planPaths, + state: input.state, + }); +} + export async function buildPlannerStatusText( input: PlannerStatusTextInput, ): Promise { @@ -1021,6 +1093,12 @@ export async function buildPlannerStatusText( const instructionBundle = inlineStageInstruction ? await readCurrentStageInstruction(input.fs, preflight) : []; + // Reasoning fuel: how much of the interacting-condition web on the table the + // model has run through the engine. Only rendered when a web is warranted + // here (else the directive is empty and the section is dropped). + const reasoningFuelSection = preflight.planPaths + ? await formatReasoningFuelSection(input.fs, preflight.planPaths, state) + : []; lines.push( "", `You are in worktree \`${state.worktreePath ?? "(none)"}\` (branch \`${preflight.gitReality?.branch ?? state.currentBranch ?? "(unknown)"}\`) — work here.`, @@ -1033,6 +1111,7 @@ export async function buildPlannerStatusText( `- stepStatus: ${state.stepStatus}`, `- activeTaskId: ${state.activeTaskId ?? "(none)"}`, "", + ...reasoningFuelSection, "## Languages", "Write each kind of generated text in the language shown here (resolved live from settings) unless the user explicitly requested another in this conversation:", `- final summary and general prose — humanLanguage: ${settings.effective.metadata.humanLanguage}`, diff --git a/src/runtime/tool-gating-invariant.test.ts b/src/runtime/tool-gating-invariant.test.ts index 08a672c..ea011c7 100644 --- a/src/runtime/tool-gating-invariant.test.ts +++ b/src/runtime/tool-gating-invariant.test.ts @@ -90,10 +90,17 @@ describe("planner tool gating invariant", () => { for (const step of stepList) { const set = setFor(stage, step); if (stage === "recovery" && step === "repair_or_resume") { + // The guard scopes in the two pure-diagnosis reasoning tools here + // (proving the repair decision); everything else stays fixed. expect(set).toContain("planner_elenchus_check"); + expect(set).toContain("planner_reason"); expect( JSON.stringify( - set.filter((tool) => tool !== "planner_elenchus_check"), + set.filter( + (tool) => + tool !== "planner_elenchus_check" && + tool !== "planner_reason", + ), ), ).toEqual(baseline); continue; diff --git a/src/runtime/workflow-tools.test.ts b/src/runtime/workflow-tools.test.ts index 59f3eb5..3ef888e 100644 --- a/src/runtime/workflow-tools.test.ts +++ b/src/runtime/workflow-tools.test.ts @@ -365,6 +365,9 @@ describe("workflowToolTransition", () => { params: {}, }); expect(finished.result.status).toBe("applied"); + // The applied result carries the plan's storage paths so the dispatcher + // can surface the reasoning-fuel nudge for the step it landed on. + expect(finished.planPaths).toBeDefined(); }); it("ignores an elenchus CONFLICT recorded for a different step", async () => { diff --git a/src/runtime/workflow-tools.ts b/src/runtime/workflow-tools.ts index 1763d56..84b73b8 100644 --- a/src/runtime/workflow-tools.ts +++ b/src/runtime/workflow-tools.ts @@ -75,6 +75,13 @@ export interface PlannerWorkflowToolExecutionResult { transition: PlannerStateTransition; result: PlannerStateTransitionResult; lifecycle: PlannerLifecycleDecision | null; + /** + * The active plan's storage paths when this transition ran against a ready + * plan — pure data pass-through, so the surfacing layer (the tool dispatcher) + * can render the reasoning-fuel nudge for the resulting step without any + * decision module importing a fuel module. Absent when no plan is ready. + */ + planPaths?: PlanStoragePaths; } export async function executePlannerWorkflowTool( @@ -172,6 +179,10 @@ export async function executePlannerWorkflowTool( transition, result, lifecycle, + planPaths: + orchestrator.preflight.context.status === "ready" + ? orchestrator.preflight.context.planPaths + : undefined, }; } diff --git a/src/vrf/AGENTS.md b/src/vrf/AGENTS.md index 38cdf18..36e02aa 100644 --- a/src/vrf/AGENTS.md +++ b/src/vrf/AGENTS.md @@ -2,7 +2,7 @@ ## Planner Contracts ### Purpose -elenchus/VRF domain: the bundled premise-template library, its sync/routing plumbing, and the deterministic SDD compilers that turn durable planner artifacts into engine-checkable programs. +elenchus/VRF domain: the bundled premise-template library, its sync/routing plumbing, the deterministic SDD compilers that turn durable planner artifacts into engine-checkable programs, and the plan's living logical world (an accumulating registry of model-asserted statements). ### Parent - `../AGENTS.md` @@ -16,6 +16,7 @@ elenchus/VRF domain: the bundled premise-template library, its sync/routing plum - Every compiler is unit-tested through the REAL wasm engine (`runtime/elenchus-engine.ts`), never a mock — a premise regression must fail CI with the engine's own verdict. - `VRF_TEMPLATE_NAMES` (schema.ts) must list every file in `vrf/defaults/`; a project override at `.pi/pi-code-planner/vrf/.vrf` beats the bundled default. - elenchus `SET`s do not cross files: a compiler whose program needs sets (coverage, tdd-coverage) must emit a fully self-contained file, not a template import. +- For model-authored programs (`world-store.ts`, `runtime/elenchus-tools.ts`) the planner reads only the verdict code and hands the engine's raw output on verbatim — it never parses the report body (orphans/beliefs/derivations). The narrow, bounded parse of `status`/`conflicts`/`warnings`/`goals` in `runtime/gate-tools.ts` is legitimate only because those are compiler-authored programs whose atom vocabulary the planner owns. ### Read First - `schema.ts` @@ -35,6 +36,7 @@ elenchus/VRF domain: the bundled premise-template library, its sync/routing plum - `spec-compiler.ts` → `compileSpecConsistency`: `spec.json` → the spec_consistency gate program. Imports `vrf/defaults/spec-consistency.vrf` (the engine-verified freedom-valve arc from `docs/sdd/models/`), fully closes every requirement subject (FACT/NOT, never omitted) so `CHECK BIDIRECTIONAL` noise is zero, emits assumptions as ` holds` leaves, constraint relations as PREMISE blocks, acceptance atoms as advisory PROVE goals. Claim is bound through the bare `spec_gate.spec_verified` VAR port. - `coverage-compiler.ts` → `compilePlanCoverage`: `spec.json` + `TaskRecord.requirements` → self-contained Skolem witness tables (`TOTAL covered_by ON requirements` names each dropped requirement; `TOTAL traces ON tasks` names each orphan task). Deferred requirements and non-goals never enter the requirement set — a freedom-valve deferral IS the discharge. - `tdd-coverage-compiler.ts` → `compileTddCoverage`: `behaviors.json` → per-phase witness tables (`has_red_test` at write_tests, plus `has_green_test` at run_final_tests; green still totals red so test-first stays visible). -- Consumers: `runtime/gate-tools.ts` (the only caller of the compilers) and `runtime/elenchus-tools.ts` (free-form checks importing the templates). +- `world-store.ts` → the living world: a persistent registry (`/elenchus/world/world.json`) of model-asserted statements compiled into per-domain files (acyclic layer order spec → discovery → plan → task_* → scratch) and re-checked as a whole. Observations carry a file anchor; a stale hash demotes `FACT`→`BELIEVES planner` at compile time. Runs scan the verdict and return the raw output — `WorldRunRecord` holds the verdict only, never the report. Consumed by `runtime/reason-tools.ts`. +- Consumers: `runtime/gate-tools.ts` (the only caller of the compilers), `runtime/elenchus-tools.ts` (free-form checks importing the templates), and `runtime/reason-tools.ts` (the living world). - `vrf.test.ts` → the engine-backed harness: every template parses bare, reaches CONSISTENT on an honest green fixture, and yields CONFLICT/WARNING on violated/omitted duties. diff --git a/src/vrf/world-store.test.ts b/src/vrf/world-store.test.ts new file mode 100644 index 0000000..3813b41 --- /dev/null +++ b/src/vrf/world-store.test.ts @@ -0,0 +1,585 @@ +import { readFileSync } from "node:fs"; +import { mkdtemp, rm } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { dirname, join } from "node:path"; +import { fileURLToPath } from "node:url"; +import { afterAll, describe, expect, it } from "vitest"; +import { SCHEMA_VERSION } from "../constants"; +import { sha256 } from "../hash"; +import { createNodeFs } from "../storage/fs"; +import { + createPlanStoragePaths, + createProjectStoragePaths, + type PlanStoragePaths, +} from "../storage/paths"; +import type { SpecRecord } from "../storage/spec-store"; +import { MockPlannerFs } from "../test/mock-fs"; +import { syncVrfTemplatesToPlan } from "./manager"; +import { + assertWorldStatements, + collectAnchorPaths, + compileWorld, + readWorldRecord, + readWorldRunRecord, + retractWorldStatements, + runWorldCheck, + sweepWorldAnchors, + WORLD_ENTRY_NAME, + type WorldRecord, + type WorldStatement, + type WorldStatementInput, +} from "./world-store"; + +const ORIGIN = { stage: "discovery", step: "scan_project_structure" }; + +function mockPlanPaths(): PlanStoragePaths { + return createPlanStoragePaths( + createProjectStoragePaths({ agentDir: "/agent", projectRoot: "/repo/app" }), + "plan-w", + ); +} + +function statement( + lines: string[], + overrides: Partial = {}, +): WorldStatementInput { + return { lines, domain: "discovery", origin: ORIGIN, ...overrides }; +} + +describe("world registry", () => { + it("assigns sequential ids, infers kinds, and persists", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + const added = await assertWorldStatements(fs, planPaths, [ + statement(["FACT cache is_lru"]), + statement(["KNOWS planner repo uses_vitest"]), + statement([ + "PREMISE only_one:", + " EXCLUSIVE", + " db is_postgres", + " db is_sqlite", + ]), + statement(["TOTAL covered_by ON requirements"], { domain: "plan" }), + ]); + expect(added.map((s) => s.id)).toEqual(["w1", "w2", "w3", "w4"]); + expect(added.map((s) => s.kind)).toEqual([ + "fact", + "believes", + "premise", + "premise", + ]); + const record = await readWorldRecord(fs, planPaths); + expect(record.nextId).toBe(5); + expect(record.statements).toHaveLength(4); + }); + + it("does not lose statements when asserts race (the plan.json lost-update class)", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await Promise.all( + ["a", "b", "c", "d", "e"].map((atom) => + assertWorldStatements(fs, planPaths, [ + statement([`FACT subject_${atom} observed`]), + ]), + ), + ); + const record = await readWorldRecord(fs, planPaths); + expect(record.statements).toHaveLength(5); + expect(new Set(record.statements.map((s) => s.id)).size).toBe(5); + }); + + it("rejects instrument keywords and points at the reason modes", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["PROVE merge is_blocked"]), + ]), + ).rejects.toThrow(/instrument.*reason/s); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["FACT a b", "TRY hotfix is_needed"]), + ]), + ).rejects.toThrow(/instrument/); + }); + + it("rejects compiler-owned lines and unknown keywords", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(['IMPORT "../../outside.vrf"']), + ]), + ).rejects.toThrow(/owned by the world compiler/); + await expect( + assertWorldStatements(fs, planPaths, [statement(["FROB cache"])]), + ).rejects.toThrow(/must start with one of/); + }); + + it("rejects invalid domains and anchors on non-observations", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["FACT a b"], { domain: "main" }), + ]), + ).rejects.toThrow(/not valid/); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["FACT a b"], { domain: "../evil" }), + ]), + ).rejects.toThrow(/not valid/); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["RULE r1:", " WHEN a b", " THEN c d"], { + anchor: { path: "src/x.ts", hash: "h" }, + }), + ]), + ).rejects.toThrow(/only FACT\/NOT/); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["FACT a b"], { + anchor: { path: "../outside.ts", hash: "h" }, + }), + ]), + ).rejects.toThrow(/project-root-relative/); + }); + + it("a failed batch writes nothing (all-or-nothing)", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await expect( + assertWorldStatements(fs, planPaths, [ + statement(["FACT good statement"]), + statement(["CHECK"]), + ]), + ).rejects.toThrow(); + const record = await readWorldRecord(fs, planPaths); + expect(record.statements).toHaveLength(0); + }); + + it("retract removes by id, names unknown ids, and never throws", async () => { + const fs = new MockPlannerFs(); + const planPaths = mockPlanPaths(); + await assertWorldStatements(fs, planPaths, [ + statement(["FACT a b"]), + statement(["FACT c d"]), + ]); + const result = await retractWorldStatements(fs, planPaths, ["w1", "w99"]); + expect(result.removed).toEqual(["w1"]); + expect(result.missing).toEqual(["w99"]); + const record = await readWorldRecord(fs, planPaths); + expect(record.statements.map((s) => s.id)).toEqual(["w2"]); + }); +}); + +describe("anchor sweep", () => { + const record: WorldRecord = { + version: 1, + nextId: 4, + statements: [ + world("w1", ["FACT cache is_lru"], { + anchor: { path: "src/cache.ts", hash: "aaa" }, + }), + world("w2", ["NOT logger is_verbose"], { + anchor: { path: "src/log.ts", hash: "bbb" }, + }), + world("w3", ["FACT repo uses_vitest"]), + ], + }; + + it("collects sorted unique anchor paths", () => { + expect(collectAnchorPaths(record)).toEqual(["src/cache.ts", "src/log.ts"]); + }); + + it("flags changed and deleted files; unsampled paths stay fresh", () => { + const stale = sweepWorldAnchors( + record, + new Map([ + ["src/cache.ts", "CHANGED"], + ["src/log.ts", null], + ]), + ); + expect(stale).toEqual([ + { statementId: "w1", path: "src/cache.ts" }, + { statementId: "w2", path: "src/log.ts" }, + ]); + expect( + sweepWorldAnchors(record, new Map([["src/cache.ts", "aaa"]])), + ).toEqual([]); + expect(sweepWorldAnchors(record, new Map())).toEqual([]); + }); +}); + +describe("world compiler", () => { + it("is deterministic and independent of registry order", () => { + const a: WorldRecord = { + version: 1, + nextId: 4, + statements: [ + world("w1", ["FACT cache is_lru"]), + world("w2", ["FACT task_1 is_planned"], { domain: "plan" }), + world("w3", ["ASSUME task_1 is_easy"], { domain: "scratch" }), + ], + }; + const b: WorldRecord = { + ...a, + statements: [...a.statements].reverse(), + }; + const first = compileWorld(a); + const second = compileWorld(b); + expect([...first.files.entries()]).toEqual([...second.files.entries()]); + expect(first.worldHash).toBe(second.worldHash); + }); + + it("sorts statement ids numerically (w10 after w9)", () => { + const record: WorldRecord = { + version: 1, + nextId: 11, + statements: [ + world("w10", ["FACT later statement"]), + world("w9", ["FACT earlier statement"]), + ], + }; + const compiled = compileWorld(record); + const discovery = compiled.files.get("world/discovery.vrf") ?? ""; + expect(discovery.indexOf("earlier")).toBeLessThan( + discovery.indexOf("later"), + ); + }); + + it("layers imports acyclically: discovery < plan < task_* < scratch", () => { + const record: WorldRecord = { + version: 1, + nextId: 5, + statements: [ + world("w1", ["FACT cache is_lru"]), + world("w2", ["FACT task_a is_planned"], { domain: "plan" }), + world("w3", ["FACT step_1 done"], { domain: "task_alpha" }), + world("w4", ["ASSUME all is_well"], { domain: "scratch" }), + ], + }; + const compiled = compileWorld(record); + expect(compiled.domains).toEqual([ + "discovery", + "plan", + "task_alpha", + "scratch", + ]); + expect(compiled.files.get("world/discovery.vrf")).not.toContain("IMPORT"); + expect(compiled.files.get("world/plan.vrf")).toContain( + 'IMPORT "discovery.vrf"', + ); + const scratch = compiled.files.get("world/scratch.vrf") ?? ""; + expect(scratch).toContain('IMPORT "discovery.vrf"'); + expect(scratch).toContain('IMPORT "plan.vrf"'); + expect(scratch).toContain('IMPORT "task_alpha.vrf"'); + const entry = compiled.files.get(WORLD_ENTRY_NAME) ?? ""; + expect(entry).toContain("CHECK BIDIRECTIONAL"); + }); + + it("demotes stale observations to planner beliefs and strips BECAUSE", () => { + const record: WorldRecord = { + version: 1, + nextId: 3, + statements: [ + world("w1", ['FACT cache is_lru BECAUSE "read src/cache.ts"'], { + anchor: { path: "src/cache.ts", hash: "old" }, + }), + world("w2", ["NOT logger is_verbose"], { + anchor: { path: "src/log.ts", hash: "old" }, + }), + ], + }; + const compiled = compileWorld(record, { + stale: [ + { statementId: "w1", path: "src/cache.ts" }, + { statementId: "w2", path: "src/log.ts" }, + ], + }); + const discovery = compiled.files.get("world/discovery.vrf") ?? ""; + expect(discovery).toContain("BELIEVES planner cache is_lru"); + expect(discovery).not.toContain("BECAUSE"); + expect(discovery).toContain("BELIEVES planner NOT logger is_verbose"); + expect(compiled.demoted).toHaveLength(2); + }); + + it("includes the spec as the ground layer with a rewritten template import", () => { + const record: WorldRecord = { + version: 1, + nextId: 2, + statements: [world("w1", ["FACT cache is_lru"])], + }; + const compiled = compileWorld(record, { spec: minimalSpec() }); + const spec = compiled.files.get("world/spec.vrf") ?? ""; + expect(spec).toContain('IMPORT "../templates/spec-consistency.vrf"'); + expect(spec).not.toContain('IMPORT "templates/'); + expect(compiled.values["spec_gate.spec_verified"]).toBe(true); + expect(compiled.files.get("world/discovery.vrf")).toContain( + 'IMPORT "spec.vrf"', + ); + }); + + it("maps every emitted statement line back to its statement id", () => { + const record: WorldRecord = { + version: 1, + nextId: 3, + statements: [ + world("w1", ["FACT cache is_lru"]), + world("w2", [ + "PREMISE only_one:", + " EXCLUSIVE", + " db is_postgres", + " db is_sqlite", + ]), + ], + }; + const compiled = compileWorld(record); + const discovery = (compiled.files.get("world/discovery.vrf") ?? "").split( + "\n", + ); + expect( + compiled.sourceMap.filter((e) => e.statementId === "w2"), + ).toHaveLength(4); + for (const entry of compiled.sourceMap) { + const line = discovery[entry.line - 1] ?? ""; + expect(entry.file).toBe("world/discovery.vrf"); + expect(line.trim().length).toBeGreaterThan(0); + } + }); + + it("throws on a hand-edited registry with an invalid domain", () => { + const record: WorldRecord = { + version: 1, + nextId: 2, + statements: [world("w1", ["FACT a b"], { domain: "../evil" })], + }; + expect(() => compileWorld(record)).toThrow(/invalid domain/); + }); +}); + +describe("world run through the real engine", () => { + const fs = createNodeFs(); + const roots: string[] = []; + + afterAll(async () => { + await Promise.all( + roots.map((root) => rm(root, { recursive: true, force: true })), + ); + }); + + async function livePaths(): Promise { + const root = await mkdtemp(join(tmpdir(), "world-store-")); + roots.push(root); + const projectPaths = createProjectStoragePaths({ + agentDir: join(root, "agent"), + projectRoot: join(root, "repo"), + }); + const planPaths = createPlanStoragePaths(projectPaths, "plan-live"); + await fs.mkdirp(planPaths.elenchusDir); + await syncVrfTemplatesToPlan(fs, { projectPaths, planPaths }); + return planPaths; + } + + it("checks a healthy cross-domain world, persists the verdict, and returns raw output", async () => { + const planPaths = await livePaths(); + await assertWorldStatements(fs, planPaths, [ + statement(["FACT cache is_lru"]), + // A RULE (not a PREMISE) so the cross-domain consequence is actually + // derived — a bare PREMISE would leave task_1 undetermined (WARNING). + statement( + [ + "RULE needs_cache:", + " WHEN discovery.cache is_lru", + " THEN task_1 is_ready", + ], + { domain: "plan" }, + ), + ]); + const run = await runWorldCheck(fs, planPaths, { + now: () => "2026-07-07T00:00:00.000Z", + }); + expect(run.ok, run.ok ? "" : run.reason).toBe(true); + if (!run.ok) return; + expect(run.verdict).toBe("CONSISTENT"); + // The store never parses the report — the derived consequence reaches the + // caller (and thus the model) in the raw output verbatim. + expect(run.output).toContain("plan.task_1 is_ready"); + const persisted = await readWorldRunRecord(fs, planPaths); + expect(persisted?.verdict).toBe("CONSISTENT"); + expect(persisted?.worldHash).toBe(run.compiled.worldHash); + }); + + it("demoted stale knowledge cannot raise a false CONFLICT, and the false belief shows in the raw output", async () => { + const planPaths = await livePaths(); + const originalContent = "export const CACHE = 'lru';\n"; + await assertWorldStatements(fs, planPaths, [ + statement(["FACT cache is_lru"], { + anchor: { path: "src/cache.ts", hash: sha256(originalContent) }, + }), + statement(["FACT cache uses_fifo"]), + statement([ + "RULE fifo_not_lru:", + " WHEN cache uses_fifo", + " THEN NOT cache is_lru", + ]), + ]); + // As plain FACTs this world is contradictory; with the anchor stale the + // observation demotes to a belief and the engine stays CONSISTENT while + // deriving the belief's negation (the named "false belief" nudge). The + // staleness the planner acts on is its own compiled `demoted` list. + const run = await runWorldCheck(fs, planPaths, { + hashProjectFile: async () => sha256("export const CACHE = 'fifo';\n"), + }); + expect(run.ok, run.ok ? "" : run.reason).toBe(true); + if (!run.ok) return; + expect(run.verdict).toBe("CONSISTENT"); + expect(run.compiled.demoted).toEqual([ + { statementId: "w1", path: "src/cache.ts" }, + ]); + // The contradicted claim and its owning agent are visible in the raw + // output for the model to read — pi-planner itself never parses them out. + expect(run.output).toContain("discovery.cache is_lru"); + expect(run.output).toContain("planner"); + }); + + it("a contradictory world yields CONFLICT and the raw output carries the repair", async () => { + const planPaths = await livePaths(); + await assertWorldStatements(fs, planPaths, [ + statement(["FACT db is_postgres"]), + statement(["ASSUME db is_sqlite"]), + statement([ + "PREMISE only_one:", + " EXCLUSIVE", + " db is_postgres", + " db is_sqlite", + ]), + ]); + const run = await runWorldCheck(fs, planPaths); + expect(run.ok, run.ok ? "" : run.reason).toBe(true); + if (!run.ok) return; + expect(run.verdict).toBe("CONFLICT"); + // The conflicting atom and the drop/flip repair reach the model in the raw + // output; the store's only reading of it is the verdict scan above. + expect(run.output).toContain("discovery.db is_postgres"); + expect(run.output).toContain("drop"); + }); + + it("checks spec + world together through the synced template", async () => { + const planPaths = await livePaths(); + await assertWorldStatements(fs, planPaths, [ + statement(["FACT cache is_lru"]), + ]); + const run = await runWorldCheck(fs, planPaths, { spec: minimalSpec() }); + expect(run.ok, run.ok ? "" : run.reason).toBe(true); + if (!run.ok) return; + expect(["CONSISTENT", "WARNING"]).toContain(run.verdict); + expect(run.output).toContain("req_1_ok"); + }); + + it("surfaces a plain-text engine diagnostic as a failed run, not a crash", async () => { + const planPaths = await livePaths(); + await assertWorldStatements(fs, planPaths, [ + // Parses as a keyword-led statement but is semantically broken: the + // premise body is missing its THEN. + statement(["PREMISE broken:", " WHEN a b"]), + ]); + const run = await runWorldCheck(fs, planPaths); + expect(run.ok).toBe(false); + if (run.ok) return; + expect(run.reason.length).toBeGreaterThan(0); + }); + + it("an empty world checks clean (the vacuum is CONSISTENT; fuel scoring is a separate concern)", async () => { + const planPaths = await livePaths(); + const run = await runWorldCheck(fs, planPaths); + expect(run.ok, run.ok ? "" : run.reason).toBe(true); + if (!run.ok) return; + expect(run.verdict).toBe("CONSISTENT"); + }); +}); + +describe("engine decoupling invariant", () => { + it("the store never parses the engine report — only the verdict token", () => { + // The anti-regression guard for this whole redesign: pi-planner must not + // grow a dependency on the engine's private JSON shape for model-authored + // programs. If a future edit reads report internals here, this fails. + const source = readFileSync( + join(dirname(fileURLToPath(import.meta.url)), "world-store.ts"), + "utf8", + ); + for (const forbidden of [ + "elenchus-report", + "ElenchusJsonReport", + "parseElenchusReport", + ".orphans", + ".beliefs", + ".derived", + ".retract", + ".unsat_core", + ".fixes", + ".tried", + ".goals", + ".derivation", + ]) { + expect( + source, + `world-store must not reference ${forbidden}`, + ).not.toContain(forbidden); + } + }); +}); + +function world( + id: string, + lines: string[], + overrides: Partial> = {}, +): WorldStatement { + const kind = overrides.kind ?? inferKindForTest(lines[0] ?? ""); + return { + id, + kind, + lines, + domain: "discovery", + origin: ORIGIN, + assertedAt: "2026-07-07T00:00:00.000Z", + ...overrides, + }; +} + +function inferKindForTest(firstLine: string): WorldStatement["kind"] { + const keyword = firstLine.trim().split(/\s+/, 1)[0] ?? ""; + switch (keyword) { + case "FACT": + return "fact"; + case "NOT": + return "not"; + case "ASSUME": + return "assume"; + case "RULE": + return "rule"; + case "PREMISE": + return "premise"; + default: + return "fact"; + } +} + +function minimalSpec(): SpecRecord { + return { + schemaVersion: SCHEMA_VERSION, + requirements: [ + { + id: "REQ-1", + statement: "The cache evicts least-recently-used entries.", + acceptance: "Eviction test passes.", + acceptanceAtom: "req_1_ok", + priority: "must", + inScope: true, + }, + ], + nonGoals: [], + constraints: [], + assumptions: [], + }; +} diff --git a/src/vrf/world-store.ts b/src/vrf/world-store.ts new file mode 100644 index 0000000..92c8a86 --- /dev/null +++ b/src/vrf/world-store.ts @@ -0,0 +1,702 @@ +import { readFileSync } from "node:fs"; +import { basename, join, resolve } from "node:path"; +import { sha256 } from "../hash"; +import { isPathInsideOrEqual } from "../path-utils"; +import { runElenchusCheck } from "../runtime/elenchus-engine"; +import { withFileWriteLock } from "../storage/file-lock"; +import type { PlannerFs } from "../storage/fs"; +import { safeReaddir } from "../storage/fs"; +import { readJsonIfExists, writeJson } from "../storage/json"; +import type { PlanStoragePaths } from "../storage/paths"; +import type { SpecRecord } from "../storage/spec-store"; +import { compileSpecConsistency } from "./spec-compiler"; + +/** + * The plan's living logical world: a persistent registry of model-asserted + * VRF statements (`/elenchus/world/world.json`) compiled into a + * multi-domain program the engine re-checks as a whole. Unlike the one-shot + * programs of `planner_elenchus_check`, statements accumulate across stages, + * so every new assertion is tested against everything asserted before. + * + * The store treats the engine exactly as `planner_elenchus_check` does: it runs + * a program, scans the output for one of four verdict codes, and hands the raw + * output to callers verbatim. It never parses the report body — no orphans, no + * beliefs, no derivations — so it stays decoupled from the engine's private + * JSON shape. Everything a fuel/directive layer needs beyond the verdict comes + * from the planner's own artifacts, never from the engine's output. + * + * Statements about project files carry an anchor (path + content hash taken + * at assert time). When the file changes, the compiler demotes the statement + * from knowledge to belief (`FACT …` → `BELIEVES planner …`): stale knowledge + * can no longer raise a false CONFLICT, and the demoted line reaches the model + * directly in the raw output (a rule deriving its negation surfaces it there as + * a named false belief). The staleness the planner acts on comes from its own + * hash sweep ({@link sweepWorldAnchors}), not from reading the report. + * + * Domains form a fixed acyclic layer order (spec → discovery → plan → + * task_ → scratch; task domains alphabetical among themselves). Each + * compiled file imports every earlier domain in that total order, because the + * engine resolves qualified cross-domain references only through the + * referencing file's own imports and rejects import cycles (probed). The + * consequences: statements may reference earlier layers (`discovery.cache + * is_lru` from `plan`), never later ones — a link pointing "forward" belongs + * in the later domain; and since elenchus SETs do not cross files, a SET and + * its FOR EACH consumers must live in the same domain. + * + * The world holds only establishing/constraining statements (facts, premises, + * rules, beliefs, sets, closures, vars). Instruments (PROVE/HENCE/TRY) are + * run-scoped questions, not territory — they are posed per run by the reason + * tool, and CHECK/IMPORT/DOMAIN lines are compiler-owned. + */ + +/** + * The engine's terminal verdict, scanned from its output as one of four codes + * (or "unknown"). This scan is the whole of the store's coupling to the + * engine: the report body is never parsed. + */ +export type WorldVerdict = + | "CONSISTENT" + | "WARNING" + | "UNDERDETERMINED" + | "CONFLICT" + | "unknown"; + +const WORLD_VERDICTS: readonly WorldVerdict[] = [ + "CONSISTENT", + "WARNING", + "UNDERDETERMINED", + "CONFLICT", +]; + +/** First verdict code present in the engine output, or "unknown". */ +export function detectWorldVerdict(output: string): WorldVerdict { + for (const verdict of WORLD_VERDICTS) { + if (output.includes(verdict)) return verdict; + } + return "unknown"; +} + +/** + * Whether the engine output is a JSON object (a real verdict) rather than a + * plain-text diagnostic (syntax/citation/resolver error). Used only to route a + * diagnostic to a failure — no field of the parsed object is ever read. + */ +function isJsonVerdictBody(output: string): boolean { + try { + const parsed: unknown = JSON.parse(output); + return !!parsed && typeof parsed === "object" && !Array.isArray(parsed); + } catch { + return false; + } +} + +export type WorldStatementKind = + | "fact" + | "not" + | "assume" + | "premise" + | "rule" + | "believes" + | "set" + | "close" + | "var"; + +export interface WorldAnchor { + /** Project-root-relative file the statement observes. */ + path: string; + /** sha256 of that file's content when the statement was asserted. */ + hash: string; +} + +export interface WorldOrigin { + stage: string; + step: string; +} + +export interface WorldStatement { + /** Store-assigned id, `w` — the handle retract/repair texts use. */ + id: string; + kind: WorldStatementKind; + /** Verbatim .vrf lines (one statement, possibly a multi-line block). */ + lines: string[]; + domain: string; + anchor?: WorldAnchor; + origin: WorldOrigin; + assertedAt: string; +} + +export interface WorldRecord { + version: 1; + nextId: number; + statements: WorldStatement[]; +} + +export interface WorldStatementInput { + lines: string[]; + domain: string; + anchor?: WorldAnchor; + origin: WorldOrigin; +} + +export interface WorldStaleAnchor { + statementId: string; + path: string; +} + +export interface WorldSourceMapEntry { + /** Compiled file, relative to the plan's elenchus dir. */ + file: string; + /** 1-based line within that file. */ + line: number; + statementId: string; +} + +export interface CompiledWorld { + /** File name (relative to the elenchus dir) → content. */ + files: Map; + /** VAR port values the run must pass (the spec claim port when included). */ + values: Record; + /** Maps every emitted statement line back to its statement id. */ + sourceMap: WorldSourceMapEntry[]; + /** Model domains in compile (layer) order; excludes the spec domain. */ + domains: string[]; + /** Statements demoted to beliefs because their anchor went stale. */ + demoted: WorldStaleAnchor[]; + /** sha256 over all compiled files — the world's content fingerprint. */ + worldHash: string; +} + +/** + * The last persisted world run. Holds only the verdict code and provenance — + * never the report body — so nothing downstream can grow a dependency on the + * engine's private JSON shape. Callers that need the run's detail read the raw + * output the run returned, not this record. + */ +export interface WorldRunRecord { + recordedAt: string; + verdict: WorldVerdict; + engineVersion: string; + worldHash: string; + demoted: WorldStaleAnchor[]; +} + +export type WorldRunResult = + | { + ok: true; + verdict: WorldVerdict; + /** The engine's raw output, handed to the model verbatim. */ + output: string; + compiled: CompiledWorld; + engineVersion: string; + } + | { ok: false; reason: string }; + +const WORLD_DIR = "world"; +const WORLD_JSON_FILE = "world.json"; +const WORLD_RESULT_FILE = "last-run.json"; +const WORLD_ENTRY_FILE = "main.vrf"; +const SPEC_DOMAIN_FILE = "spec.vrf"; + +/** Engine entry path, relative to the elenchus dir (the resolver root). */ +export const WORLD_ENTRY_NAME = `${WORLD_DIR}/${WORLD_ENTRY_FILE}`; + +// Closed domain shape: discovery | plan | task_ | scratch. "main" and +// "spec" can never collide because neither matches the pattern. +const WORLD_DOMAIN_PATTERN = /^(discovery|plan|scratch|task_[a-z0-9_]{1,48})$/; + +// First keyword of a statement → its kind. KNOWS is epistemic like BELIEVES; +// quantifiers/coverage/preference forms check rather than establish, so they +// count as premises for the structural signals. +const KEYWORD_KINDS: Readonly> = { + FACT: "fact", + NOT: "not", + ASSUME: "assume", + PREMISE: "premise", + RULE: "rule", + BELIEVES: "believes", + KNOWS: "believes", + SET: "set", + CLOSE: "close", + VAR: "var", + DEFAULT: "var", + TOTAL: "premise", + EXISTS: "premise", + FOR: "premise", + PREFERS: "premise", +}; + +const INSTRUMENT_KEYWORDS = new Set(["PROVE", "HENCE", "TRY"]); +const COMPILER_KEYWORDS = new Set(["CHECK", "IMPORT", "DOMAIN", "PROVIDE"]); + +export function worldDirPath(planPaths: PlanStoragePaths): string { + return join(planPaths.elenchusDir, WORLD_DIR); +} + +export function worldJsonPath(planPaths: PlanStoragePaths): string { + return join(worldDirPath(planPaths), WORLD_JSON_FILE); +} + +function worldResultPath(planPaths: PlanStoragePaths): string { + return join(worldDirPath(planPaths), WORLD_RESULT_FILE); +} + +function emptyWorldRecord(): WorldRecord { + return { version: 1, nextId: 1, statements: [] }; +} + +export async function readWorldRecord( + fs: PlannerFs, + planPaths: PlanStoragePaths, +): Promise { + return ( + (await readJsonIfExists(fs, worldJsonPath(planPaths))) ?? + emptyWorldRecord() + ); +} + +/** + * Serialized read-modify-write on world.json — same lost-update class as + * plan.json: Pi runs same-message tool calls concurrently, so a batch of + * asserts would otherwise clobber each other. See {@link withFileWriteLock}. + */ +export async function updateWorldRecord( + fs: PlannerFs, + planPaths: PlanStoragePaths, + update: (record: WorldRecord) => WorldRecord, +): Promise { + const path = worldJsonPath(planPaths); + return await withFileWriteLock(path, async () => { + const current = + (await readJsonIfExists(fs, path)) ?? emptyWorldRecord(); + const next = update(current); + await writeJson(fs, path, next); + return next; + }); +} + +function firstKeyword(line: string): string { + return line.trim().split(/\s+/, 1)[0] ?? ""; +} + +function isStatementText(line: string): boolean { + const trimmed = line.trim(); + return trimmed.length > 0 && !trimmed.startsWith("//"); +} + +/** + * Validate one statement input and infer its kind from the first keyword. + * Throws with a model-actionable message: what was rejected and which move + * expresses that intent instead. + */ +export function validateWorldStatementInput( + input: WorldStatementInput, +): Omit { + const domain = input.domain.trim(); + if (!WORLD_DOMAIN_PATTERN.test(domain)) { + throw new Error( + `World domain "${domain}" is not valid. Use "discovery", "plan", "scratch", or "task_" (lowercase letters, digits, underscores).`, + ); + } + const lines = input.lines.map((line) => line.replace(/\s+$/, "")); + const textLines = lines.filter(isStatementText); + if (textLines.length === 0) { + throw new Error( + "A world statement needs at least one non-comment .vrf line.", + ); + } + for (const line of textLines) { + const keyword = firstKeyword(line); + if (INSTRUMENT_KEYWORDS.has(keyword)) { + throw new Error( + `${keyword} is an instrument, not territory: it is posed per run, never stored. Use the matching reason mode (prove/hence/abduct) instead of asserting it into the world.`, + ); + } + if (COMPILER_KEYWORDS.has(keyword)) { + throw new Error( + `${keyword} lines are owned by the world compiler and cannot be asserted. State only facts, premises, rules, beliefs, sets, closures, or vars.`, + ); + } + } + const kind = KEYWORD_KINDS[firstKeyword(textLines[0] ?? "")]; + if (!kind) { + throw new Error( + `Statement must start with one of: ${Object.keys(KEYWORD_KINDS).join(", ")}. Got "${firstKeyword(textLines[0] ?? "")}".`, + ); + } + const origin = { + stage: input.origin.stage.trim(), + step: input.origin.step.trim(), + }; + if (!origin.stage || !origin.step) { + throw new Error("Statement origin needs a non-empty stage and step."); + } + const anchor = validateAnchor(input.anchor, kind); + return anchor + ? { kind, lines, domain, anchor, origin } + : { kind, lines, domain, origin }; +} + +function validateAnchor( + anchor: WorldAnchor | undefined, + kind: WorldStatementKind, +): WorldAnchor | undefined { + if (!anchor) return undefined; + if (kind !== "fact" && kind !== "not") { + throw new Error( + `Anchors mark observations of files, so only FACT/NOT statements may carry one (got a ${kind}). State the observation as a FACT and put the law over it in a separate premise or rule.`, + ); + } + const path = anchor.path.trim().replace(/\\/g, "/"); + const hash = anchor.hash.trim(); + if (!path || !hash) { + throw new Error("An anchor needs both a file path and a content hash."); + } + if ( + path.startsWith("/") || + /^[a-zA-Z]:/.test(path) || + path.split("/").includes("..") + ) { + throw new Error( + `Anchor path must be project-root-relative without ".." segments: "${anchor.path}".`, + ); + } + return { path, hash }; +} + +/** + * Append validated statements atomically, assigning `w` ids. All inputs + * are validated before anything is written, so a batch is all-or-nothing. + */ +export async function assertWorldStatements( + fs: PlannerFs, + planPaths: PlanStoragePaths, + inputs: readonly WorldStatementInput[], + now: () => string = () => new Date().toISOString(), +): Promise { + const prepared = inputs.map(validateWorldStatementInput); + let added: WorldStatement[] = []; + await updateWorldRecord(fs, planPaths, (record) => { + let nextId = record.nextId; + added = prepared.map((statement) => ({ + id: `w${nextId++}`, + assertedAt: now(), + ...statement, + })); + return { + ...record, + nextId, + statements: [...record.statements, ...added], + }; + }); + return added; +} + +/** + * Remove statements by id. Never throws on unknown ids — retraction is the + * anti-deadlock escape and must always succeed; unknown ids are reported so + * the caller can name them. + */ +export async function retractWorldStatements( + fs: PlannerFs, + planPaths: PlanStoragePaths, + ids: readonly string[], +): Promise<{ removed: string[]; missing: string[] }> { + const wanted = new Set(ids.map((id) => id.trim()).filter(Boolean)); + let removed: string[] = []; + await updateWorldRecord(fs, planPaths, (record) => { + removed = record.statements + .filter((statement) => wanted.has(statement.id)) + .map((statement) => statement.id); + return { + ...record, + statements: record.statements.filter( + (statement) => !wanted.has(statement.id), + ), + }; + }); + const removedSet = new Set(removed); + return { + removed, + missing: [...wanted].filter((id) => !removedSet.has(id)), + }; +} + +/** Sorted unique anchor paths — what a sweep must hash. */ +export function collectAnchorPaths(record: WorldRecord): string[] { + const paths = new Set(); + for (const statement of record.statements) { + if (statement.anchor) paths.add(statement.anchor.path); + } + return [...paths].sort(); +} + +/** + * Compare stored anchor hashes against current file hashes. `null` means the + * file is gone (stale); a path missing from the map was not sampled and is + * treated as fresh — pass every {@link collectAnchorPaths} entry for a full + * sweep. + */ +export function sweepWorldAnchors( + record: WorldRecord, + currentHashes: ReadonlyMap, +): WorldStaleAnchor[] { + const stale: WorldStaleAnchor[] = []; + for (const statement of record.statements) { + const anchor = statement.anchor; + if (!anchor) continue; + const current = currentHashes.get(anchor.path); + if (current === undefined) continue; + if (current === null || current !== anchor.hash) { + stale.push({ statementId: statement.id, path: anchor.path }); + } + } + return stale; +} + +function statementIdNumber(id: string): number { + const match = /^w(\d+)$/.exec(id); + return match ? Number(match[1]) : Number.MAX_SAFE_INTEGER; +} + +// Layer order for the acyclic import chain; ties break alphabetically. +function domainLayer(domain: string): number { + if (domain === "discovery") return 0; + if (domain === "plan") return 1; + if (domain.startsWith("task_")) return 2; + return 3; // scratch +} + +function compareDomains(a: string, b: string): number { + return domainLayer(a) - domainLayer(b) || a.localeCompare(b, "en"); +} + +/** + * Demote a stale observation line from knowledge to belief. Only FACT/NOT + * lines change; the engine's BELIEVES form takes no BECAUSE clause, so an + * evidence clause moves into the trailing comment. + */ +function demoteLine(line: string, path: string): string { + const because = /\s+BECAUSE\s+"[^"]*"\s*$/.exec(line); + const bare = because ? line.slice(0, because.index) : line; + const demoted = bare + .replace(/^(\s*)FACT\s+/, "$1BELIEVES planner ") + .replace(/^(\s*)NOT\s+/, "$1BELIEVES planner NOT "); + return `${demoted} // stale anchor: ${path} changed since asserted`; +} + +/** + * Deterministically compile the registry into per-domain files plus the + * `main.vrf` entry (`CHECK BIDIRECTIONAL`). Statements sort by id within a + * domain and domains by layer, so byte-identical output never depends on + * registry order. When `spec` is given, the spec-consistency program joins + * the world as its ground layer under `spec.vrf` (every domain imports it). + */ +export function compileWorld( + record: WorldRecord, + options: { + stale?: readonly WorldStaleAnchor[]; + spec?: SpecRecord | null; + } = {}, +): CompiledWorld { + const staleById = new Map( + (options.stale ?? []).map((entry) => [entry.statementId, entry]), + ); + const byDomain = new Map(); + for (const statement of record.statements) { + if (!WORLD_DOMAIN_PATTERN.test(statement.domain)) { + throw new Error( + `world.json contains an invalid domain "${statement.domain}" (statement ${statement.id}) — the registry was edited outside the reason tool.`, + ); + } + const group = byDomain.get(statement.domain) ?? []; + group.push(statement); + byDomain.set(statement.domain, group); + } + const domains = [...byDomain.keys()].sort(compareDomains); + + const files = new Map(); + const sourceMap: WorldSourceMapEntry[] = []; + const demoted: WorldStaleAnchor[] = []; + let values: Record = {}; + + let hasSpec = false; + if (options.spec) { + const compiledSpec = compileSpecConsistency(options.spec); + // The spec program imports its template relative to the elenchus dir; + // from inside world/ that is one level up. + files.set( + `${WORLD_DIR}/${SPEC_DOMAIN_FILE}`, + compiledSpec.program.replace( + 'IMPORT "templates/spec-consistency.vrf"', + 'IMPORT "../templates/spec-consistency.vrf"', + ), + ); + values = { ...compiledSpec.values }; + hasSpec = true; + } + + const importsFor = (index: number): string[] => { + const imports: string[] = []; + if (hasSpec) imports.push(`IMPORT "${SPEC_DOMAIN_FILE}"`); + for (const earlier of domains.slice(0, index)) { + imports.push(`IMPORT "${earlier}.vrf"`); + } + return imports; + }; + + domains.forEach((domain, index) => { + const file = `${WORLD_DIR}/${domain}.vrf`; + const lines: string[] = [ + "// Generated by pi-code-planner's world compiler from world.json —", + "// do not edit by hand; grow the world through the reason tool.", + `DOMAIN ${domain}`, + ...importsFor(index), + ]; + const statements = [...(byDomain.get(domain) ?? [])].sort( + (a, b) => statementIdNumber(a.id) - statementIdNumber(b.id), + ); + for (const statement of statements) { + lines.push(""); + const anchorNote = statement.anchor + ? ` [anchor ${statement.anchor.path}]` + : ""; + lines.push( + `// ${statement.id} (${statement.origin.stage}/${statement.origin.step})${anchorNote}`, + ); + const staleEntry = staleById.get(statement.id); + if (staleEntry) demoted.push(staleEntry); + for (const line of statement.lines) { + lines.push( + staleEntry && isStatementText(line) + ? demoteLine(line, staleEntry.path) + : line, + ); + sourceMap.push({ + file, + line: lines.length, + statementId: statement.id, + }); + } + } + files.set(file, `${lines.join("\n")}\n`); + }); + + const entryLines: string[] = [ + "// Generated by pi-code-planner's world compiler — the entry that checks", + "// the whole living world in one run.", + "DOMAIN world", + ...importsFor(domains.length), + "", + "CHECK BIDIRECTIONAL", + ]; + files.set(WORLD_ENTRY_NAME, `${entryLines.join("\n")}\n`); + + const worldHash = sha256( + [...files.keys()] + .sort() + .map((name) => `${name}\n${files.get(name) ?? ""}`) + .join("\n---\n"), + ); + return { files, values, sourceMap, domains, demoted, worldHash }; +} + +/** + * Materialize compiled files under `world/` and prune compiled `.vrf` files + * whose domain no longer exists, so the directory always mirrors the registry. + */ +export async function writeCompiledWorld( + fs: PlannerFs, + planPaths: PlanStoragePaths, + compiled: CompiledWorld, +): Promise { + const dir = worldDirPath(planPaths); + await fs.mkdirp(dir); + for (const [name, content] of compiled.files) { + await fs.writeTextAtomic(join(planPaths.elenchusDir, name), content); + } + const keep = new Set( + [...compiled.files.keys()].map((name) => basename(name)), + ); + for (const entry of await safeReaddir(fs, dir)) { + if (entry.endsWith(".vrf") && !keep.has(entry)) { + await fs.removeFile(join(dir, entry)); + } + } +} + +/** + * Compile the current registry (sweeping anchors when a hasher is provided), + * write it, and run the engine over the whole world. A plain-text engine + * diagnostic (bad premise body, etc.) comes back as `ok: false` with the text + * verbatim. On success the verdict persists to `world/last-run.json` and the + * raw output is returned for the caller to hand to the model. + */ +export async function runWorldCheck( + fs: PlannerFs, + planPaths: PlanStoragePaths, + input: { + spec?: SpecRecord | null; + /** Hash a project-root-relative file; null when it does not exist. */ + hashProjectFile?: (path: string) => Promise; + values?: Record; + now?: () => string; + } = {}, +): Promise { + const record = await readWorldRecord(fs, planPaths); + let stale: WorldStaleAnchor[] = []; + if (input.hashProjectFile) { + const hashes = new Map(); + for (const path of collectAnchorPaths(record)) { + hashes.set(path, await input.hashProjectFile(path)); + } + stale = sweepWorldAnchors(record, hashes); + } + const compiled = compileWorld(record, { stale, spec: input.spec ?? null }); + await writeCompiledWorld(fs, planPaths, compiled); + + const elenchusDir = planPaths.elenchusDir; + const read = (path: string): string => { + const target = resolve(elenchusDir, path); + if (!isPathInsideOrEqual(target, elenchusDir)) { + throw new Error(`elenchus import escapes the plan dir: ${path}`); + } + return readFileSync(target, "utf8"); + }; + const run = await runElenchusCheck({ + root: WORLD_ENTRY_NAME, + read, + format: "json", + // Compiled values win so a caller cannot unset the spec claim port. + values: { ...input.values, ...compiled.values }, + }); + if (!run.ok) return { ok: false, reason: run.reason }; + // A plain-text diagnostic (bad premise body, citation, resolver failure) is + // not a verdict — surface it verbatim as a failure, like runCheck does. + if (!isJsonVerdictBody(run.output)) { + return { ok: false, reason: run.output.trim() }; + } + const verdict = detectWorldVerdict(run.output); + const runRecord: WorldRunRecord = { + recordedAt: (input.now ?? (() => new Date().toISOString()))(), + verdict, + engineVersion: run.engineVersion, + worldHash: compiled.worldHash, + demoted: compiled.demoted, + }; + await writeJson(fs, worldResultPath(planPaths), runRecord); + return { + ok: true, + verdict, + output: run.output.trim(), + compiled, + engineVersion: run.engineVersion, + }; +} + +/** The last persisted world run, or null before the first check. */ +export async function readWorldRunRecord( + fs: PlannerFs, + planPaths: PlanStoragePaths, +): Promise { + return await readJsonIfExists(fs, worldResultPath(planPaths)); +}