diff --git a/instructions/defaults/planning.md b/instructions/defaults/planning.md index 8a2edc3..73c5dd4 100644 --- a/instructions/defaults/planning.md +++ b/instructions/defaults/planning.md @@ -26,8 +26,9 @@ At `planning/read_context`, load context in this order: - Split the plan into small ordered tasks, each independently understandable and small enough for one TDD loop. - In a follow-up planning pass, existing completed task artifacts are history. Create new revision task IDs for new work; do not reuse a completed task ID. 4. `write_task_files` - - Call `planner_task_upsert` once per behavioral task with semantic fields only: task id, title, objective, scope, acceptance criteria, `requirements` (the exact `REQ-n` ids from `spec.json` this task discharges **or enables** — a setup/infrastructure task cites the requirement it is a prerequisite for, e.g. a "cargo init" task cites the `REQ-n` whose code it makes buildable; **only `REQ-n` ids belong here, never `CON-n` constraints or `ASM-n` assumptions** — the coverage gate at `consistency_check` names every requirement no task covers and every task that traces to nothing), and optional Local Contract Context fields. The wrapper creates `task.json`, `task.md`, and empty TDD lifecycle artifacts; do not write task JSON manually. Upsert is keyed by task id and **replaces the whole record** — there is no delete tool, so retire a redundant task by folding its scope into another, and when editing an existing task resupply every field (an omitted `requirements` is wiped back to orphan). + - Call `planner_task_upsert` once per behavioral task with semantic fields only: task id, title, objective, scope, acceptance criteria, `requirements` (the exact `REQ-n` ids from `spec.json` this task actually **discharges** — implements and proves; **only `REQ-n` ids belong here, never `CON-n` constraints or `ASM-n` assumptions**, and never a `REQ-n` the task merely enables), `dependsOn` (the taskIds this task builds on — foundations first), and optional Local Contract Context fields. A setup/infrastructure task that implements no requirement leaves `requirements` empty and is not orphan work: the task that discharges a requirement lists it under `dependsOn`. The coverage gate at `consistency_check` names every requirement no task discharges, and every task neither discharging a requirement nor depended on by one. The wrapper creates `task.json`, `task.md`, and empty TDD lifecycle artifacts; do not write task JSON manually. Upsert is keyed by task id and **replaces the whole record** — there is no delete tool, so retire a redundant task by folding its scope into another, and when editing an existing task resupply every field (an omitted `requirements` or `dependsOn` is wiped). - Each `task.md` must state scope, acceptance criteria, expected files or symbols, dependency context, checks, and the relevant AGENTS.md chain when known. + - Before finishing this step, discharge the "Generated Artifacts" rule below: by default the plan carries a task that puts the toolchain's generated output under `.gitignore`. - In a follow-up planning pass, call `planner_task_upsert` only for new or still-pending revision tasks. Completed task IDs are immutable audit history. 5. `verify_plan` — verify tasks are ordered, bounded, testable, and free of hidden broad work. Record decisions and remaining risks. 6. `consistency_check` — run the requirement-coverage gate with `planner_gate_check` (gate: `plan_coverage`), plus `planner_elenchus_check` for any interacting-constraint web. See "Consistency Check" below. @@ -47,12 +48,11 @@ At `planning/read_context`, load context in this order: ## 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: +Every toolchain emits output that must NOT be tracked — build outputs, dependency/vendor directories, caches, coverage and test output, editor/tool scratch. Untracked, it swells `planner_git_inspect` and every later commit with generated bulk instead of source, and buries the real diff. -- 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. +**Default action:** the plan carries a task that writes the correct `.gitignore` entries for what this project will generate, folded into the setup/scaffolding task that first produces the artifact when there is one, or a standalone `.gitignore` task otherwise. Do this whether the project is fresh (its `.gitignore` is missing or empty) or existing (it adopts a new tool that emits an artifact the current `.gitignore` does not yet cover). You already know the conventional artifact names for each ecosystem — apply them; there is no need to spell them out here. -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. +**The only escape:** the repository already ignores everything the plan will generate. If so, state that in one line and move on — do not add a redundant task. Never skip this silently: either the plan has the ignore task, or you have written why it is unnecessary. ## Restrictions @@ -89,7 +89,7 @@ If doubt remains, revise `plan.md` or task artifacts before entering execution. ## Consistency Check (elenchus) -At `consistency_check`, run the requirement-coverage gate: call `planner_gate_check` with `gate: "plan_coverage"`. It reads `spec.json` and every task's `requirements` list, compiles them into VRF deterministically, and runs the engine — you write NO program. The verdict is total: every in-scope requirement must be covered by at least one task (a dropped requirement is **named**), and every task must trace to at least one requirement (orphan work is **named**). Iterate until **CONSISTENT**: fix a gap in place with `planner_task_upsert` (add the missing `requirements` ids or a missing task), or de-scope a requirement through a recorded user decision, then re-run the gate. `planner_finish_step` refuses to advance while the latest plan_coverage run is not CONSISTENT or is stale (spec.json or a task's requirements changed after the pass). +At `consistency_check`, run the requirement-coverage gate: call `planner_gate_check` with `gate: "plan_coverage"`. It reads `spec.json` and every task's `requirements` and `dependsOn`, compiles them into VRF deterministically, and runs the engine — you write NO program. The verdict is total: every in-scope requirement must be discharged by at least one task (a dropped requirement is **named**), and every task must be justified — it either discharges a requirement or a discharging task (transitively) depends on it — else it is orphan work and is **named**. A dependency cycle is rejected too (dependsOn must form a DAG). Iterate until **CONSISTENT**: fix a gap in place with `planner_task_upsert` (add the missing `requirements` id, add a `dependsOn` so an infra task is justified by the task that needs it, or add a missing task), or de-scope a requirement through a recorded user decision, then re-run the gate. `planner_finish_step` refuses to advance while the latest plan_coverage run is not CONSISTENT or is stale (spec.json or a task's requirements/dependsOn changed after the pass). On top of the mandatory coverage gate, when the plan itself has a web of interacting constraints — exclusive owners, ordering/dependency chains, mutually exclusive states — model it with a free-form `planner_elenchus_check` (`IMPORT "templates/plan-consistency.vrf"`, see the template header and the `pi-planner-elenchus` skill; the engine is a three-valued SAT checker over formal logic, no arithmetic — model quantities as named symbolic states, never numbers). A CONFLICT there is also a hard gate. Record every conclusion in `decisions.md`. diff --git a/src/index.ts b/src/index.ts index 2e47925..c39bfd4 100644 --- a/src/index.ts +++ b/src/index.ts @@ -434,7 +434,13 @@ const TASK_UPSERT_TOOL_PARAMETERS = { type: "array", items: { type: "string" }, description: - "Spec traceability: the REQ-n ids from spec.json this task discharges OR enables (a setup/infrastructure task cites the requirement it is a prerequisite for). Required in practice for plans with a spec — the plan_coverage gate names every requirement no task covers and every task that traces to nothing. Upsert REPLACES the whole task record: when editing an existing task, resupply this list or it is wiped back to orphan work.", + "Spec traceability: the REQ-n ids from spec.json this task actually DISCHARGES (implements and proves) — never a REQ it only enables. A setup/infrastructure task that implements no requirement leaves this empty and instead earns its place through `dependsOn`. The plan_coverage gate names every requirement no task discharges. Upsert REPLACES the whole task record: resupply this list when editing or it is wiped.", + }, + dependsOn: { + type: "array", + items: { type: "string" }, + description: + "Build-order dependencies: taskIds this task builds on (foundations first) — NOT REQ-n ids. This is how a non-discharging setup task avoids being orphan work: a task that discharges a requirement depends on it. The plan_coverage gate justifies a task if it discharges a requirement OR a discharging task (transitively) depends on it, and rejects a dependency cycle. Upsert REPLACES the whole record: resupply this list when editing.", }, contractChain: { type: "array", @@ -3172,7 +3178,8 @@ function registerPlannerTools( }, requirement: { type: ["string", "null"], - description: "Optional REQ-n this behavior exercises.", + description: + 'A SINGLE REQ-n id (a string, e.g. "REQ-1") this behavior exercises, or null — never an array. Every in-scope REQ-n this task owns must be cited by at least one behavior or the tdd_coverage gate BLOCKS; set it on the behavior that verifies that requirement.', }, test: { type: ["object", "null"], diff --git a/src/runtime/AGENTS.md b/src/runtime/AGENTS.md index c2d3c65..b655c82 100644 --- a/src/runtime/AGENTS.md +++ b/src/runtime/AGENTS.md @@ -73,7 +73,7 @@ Runtime domain for planner stages, model-facing status, tool wrappers, timers, r - `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. +- `behavior-tools.ts` → `planner_behavior_upsert`: the per-task behavior board (`storage/behavior-store.ts`), the `planned → red → green` test-first toggle ladder. The write is a MERGE, so `computeBehaviorBoardNudges` guards the two silent traps: an identical resubmit is named a no-op (else the model loops on the same board), and any in-scope owned REQ no behavior cites is named on the write itself (the same gap `tdd_coverage` would later block on). Both are nudges in the success text, never blocks — the board is already saved. - 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. diff --git a/src/runtime/behavior-tools.test.ts b/src/runtime/behavior-tools.test.ts new file mode 100644 index 0000000..fa3356a --- /dev/null +++ b/src/runtime/behavior-tools.test.ts @@ -0,0 +1,128 @@ +import { describe, expect, it } from "vitest"; +import { SCHEMA_VERSION } from "../constants"; +import type { + TaskBehavior, + TaskBehaviorsRecord, +} from "../storage/behavior-store"; +import { computeBehaviorBoardNudges } from "./behavior-tools"; + +function behavior( + overrides: Partial & { id: string }, +): TaskBehavior { + return { + statement: `does ${overrides.id}`, + kind: "happy", + requirement: null, + test: null, + branches: [], + status: "planned", + ...overrides, + }; +} + +function board(behaviors: TaskBehavior[]): TaskBehaviorsRecord { + return { schemaVersion: SCHEMA_VERSION, taskId: "setup-project", behaviors }; +} + +describe("computeBehaviorBoardNudges", () => { + it("flags a byte-identical resubmit as a no-op", () => { + const record = board([behavior({ id: "BHV-1" })]); + const previous = board([behavior({ id: "BHV-1" })]); + const lines = computeBehaviorBoardNudges({ + previous, + record, + ownedRequirements: [], + coverableRequirements: null, + }); + expect(lines.join("\n")).toContain("No change"); + }); + + it("stays silent when the board actually changed", () => { + const previous = board([behavior({ id: "BHV-1", status: "planned" })]); + const record = board([ + behavior({ + id: "BHV-1", + status: "red", + test: { file: "t.rs", name: "t" }, + }), + ]); + const lines = computeBehaviorBoardNudges({ + previous, + record, + ownedRequirements: [], + coverableRequirements: null, + }); + expect(lines.join("\n")).not.toContain("No change"); + }); + + it("names an owned in-scope requirement no behavior cites", () => { + const record = board([behavior({ id: "BHV-1" })]); + const lines = computeBehaviorBoardNudges({ + previous: null, + record, + ownedRequirements: ["REQ-1"], + coverableRequirements: new Set(["REQ-1"]), + }).join("\n"); + expect(lines).toContain("Owned requirements no behavior cites yet: REQ-1"); + expect(lines).toContain('"requirement": "REQ-1"'); + }); + + it("stays silent once the owned requirement is cited", () => { + const record = board([behavior({ id: "BHV-1", requirement: "REQ-1" })]); + const lines = computeBehaviorBoardNudges({ + previous: null, + record, + ownedRequirements: ["REQ-1"], + coverableRequirements: new Set(["REQ-1"]), + }); + expect(lines.join("\n")).not.toContain("Owned requirements"); + }); + + it("ignores an owned requirement the spec no longer counts as coverable", () => { + const record = board([behavior({ id: "BHV-1" })]); + const lines = computeBehaviorBoardNudges({ + previous: null, + record, + ownedRequirements: ["REQ-9"], + // REQ-9 is owned by the task but out of scope / deferred in the spec. + coverableRequirements: new Set(["REQ-1"]), + }); + expect(lines.join("\n")).not.toContain("Owned requirements"); + }); + + it("never nudges about requirements for a legacy plan without a spec", () => { + const record = board([behavior({ id: "BHV-1" })]); + const lines = computeBehaviorBoardNudges({ + previous: null, + record, + ownedRequirements: ["REQ-1"], + coverableRequirements: null, + }); + expect(lines.join("\n")).not.toContain("Owned requirements"); + }); + + it("surfaces BOTH traps on the identical-resubmit loop the session hit", () => { + // setup-project owns REQ-1, no behavior cites it, and the model resubmits + // the same two-green board — exactly the 13-call loop from the live run. + const twoGreen = [ + behavior({ + id: "BHV-1", + status: "green", + test: { file: "tests/setup.rs", name: "test_cargo_toml_exists" }, + }), + behavior({ + id: "BHV-2", + status: "green", + test: { file: "tests/setup.rs", name: "test_source_files_exist" }, + }), + ]; + const lines = computeBehaviorBoardNudges({ + previous: board(twoGreen.map((b) => ({ ...b }))), + record: board(twoGreen.map((b) => ({ ...b }))), + ownedRequirements: ["REQ-1"], + coverableRequirements: new Set(["REQ-1"]), + }).join("\n"); + expect(lines).toContain("No change"); + expect(lines).toContain("Owned requirements no behavior cites yet: REQ-1"); + }); +}); diff --git a/src/runtime/behavior-tools.ts b/src/runtime/behavior-tools.ts index 63f21e2..3ed6eb9 100644 --- a/src/runtime/behavior-tools.ts +++ b/src/runtime/behavior-tools.ts @@ -3,6 +3,7 @@ import type { GitRunner } from "../git/runner"; import { readTaskBehaviorsIfExists, type TaskBehavior, + type TaskBehaviorsRecord, validateTaskBehaviors, writeTaskBehaviors, } from "../storage/behavior-store"; @@ -76,9 +77,12 @@ export async function executePlannerBehaviorTool(input: { // cite a real, in-scope requirement that this task actually owns // (task.requirements) — otherwise the coverage totality binds the wrong set. const spec = await readSpecRecordIfExists(input.fs, planPaths); + let ownedRequirements: readonly string[] = []; + let coverableRequirements: ReadonlySet | null = null; if (spec) { const task = await readTaskRecord(input.fs, taskPaths); - const owned = new Set(task.requirements ?? []); + ownedRequirements = task.requirements ?? []; + const owned = new Set(ownedRequirements); for (const behavior of record.behaviors) { if (!behavior.requirement) continue; const known = spec.requirements.find( @@ -95,7 +99,18 @@ export async function executePlannerBehaviorTool(input: { ); } } + coverableRequirements = new Set( + spec.requirements + .filter((req) => req.inScope && req.deferral === undefined) + .map((req) => req.id), + ); } + const nudges = computeBehaviorBoardNudges({ + previous, + record, + ownedRequirements, + coverableRequirements, + }); await writeTaskBehaviors(input.fs, taskPaths, record); const byStatus = { planned: 0, red: 0, green: 0 }; for (const behavior of record.behaviors) { @@ -112,6 +127,7 @@ export async function executePlannerBehaviorTool(input: { (behavior) => `- ${behavior.id} [${behavior.status}] (${behavior.kind}${behavior.requirement ? `, ${behavior.requirement}` : ""}) ${behavior.statement}${behavior.test ? ` — ${behavior.test.file} :: ${behavior.test.name}` : ""}`, ), + ...nudges, "", 'Any earlier tdd_coverage gate pass is now stale. Run planner_gate_check with gate: "tdd_coverage" to see what the machine still counts as uncovered.', ].join("\n"), @@ -125,3 +141,50 @@ export async function executePlannerBehaviorTool(input: { function blocked(text: string) { return blockedResult(PLANNER_BEHAVIOR_TOOL_NAME, text); } + +/** + * Break the two silent traps a behavior write can fall into. Upsert MERGES, so a + * resubmit that omits `requirement` re-persists an identical board — the model + * then reads a bare "written" and loops on the same list (seen live: 13 identical + * resubmits). And the tdd_coverage gate hard-blocks on any in-scope owned REQ that + * no behavior cites, a gap the model otherwise only discovers by round-tripping + * through the gate. Naming both here, on the write itself, is a nudge (never a + * block): the board is already saved. + */ +export function computeBehaviorBoardNudges(input: { + previous: TaskBehaviorsRecord | null; + record: TaskBehaviorsRecord; + /** task.requirements (every REQ-n the task cites), empty for legacy plans. */ + ownedRequirements: readonly string[]; + /** In-scope, non-deferred spec REQ-n ids; null when the plan has no spec. */ + coverableRequirements: ReadonlySet | null; +}): string[] { + const lines: string[] = []; + const unchanged = + input.previous !== null && + JSON.stringify(input.previous.behaviors) === + JSON.stringify(input.record.behaviors); + if (unchanged) { + lines.push( + "", + "No change: this board is identical to the one already saved — resubmitting the same list will NOT advance the tdd_coverage gate. To move forward, flip a status, attach a test witness, or set `requirement` on a behavior.", + ); + } + if (input.coverableRequirements) { + const cited = new Set( + input.record.behaviors + .map((behavior) => behavior.requirement) + .filter((req): req is string => Boolean(req)), + ); + const uncoveredOwned = [...new Set(input.ownedRequirements)] + .filter((id) => input.coverableRequirements?.has(id) && !cited.has(id)) + .sort(); + if (uncoveredOwned.length > 0) { + lines.push( + "", + `Owned requirements no behavior cites yet: ${uncoveredOwned.join(", ")}. The tdd_coverage gate BLOCKS until each is exercised — set \`requirement\` to that single REQ-n string (e.g. "requirement": "${uncoveredOwned[0]}") on the behavior that verifies it, then resubmit the FULL list.`, + ); + } + } + return lines; +} diff --git a/src/runtime/gate-tools.test.ts b/src/runtime/gate-tools.test.ts index ac54e83..ae54ed6 100644 --- a/src/runtime/gate-tools.test.ts +++ b/src/runtime/gate-tools.test.ts @@ -15,13 +15,14 @@ describe("describeCoverageGaps", () => { } as never; } - it("tells an orphan setup task to cite the REQ it discharges OR enables", () => { + it("tells an orphan setup task to cite its REQ or declare a dependsOn", () => { const [gap] = describeCoverageGaps(orphanReport("init-project"), { "init-project": "Initialize Rust workspace", }); expect(gap).toContain('Task "Initialize Rust workspace" is ORPHAN'); - expect(gap).toContain("discharges OR enables"); - expect(gap).toContain("prerequisite"); + // The new structural remedy: a discharging task depends on the infra task. + expect(gap).toContain("dependsOn"); + expect(gap).toContain("infrastructure"); }); it("names the no-delete reality and the wipe-on-omit trap", () => { @@ -29,10 +30,21 @@ describe("describeCoverageGaps", () => { // The model tried to delete; say there is none and give the real alternative. expect(gap).toContain("no delete tool"); expect(gap).toContain("fold its scope"); - // Omitting requirements on a re-upsert wiped coverage — warn about it. + // Omitting requirements/dependsOn on a re-upsert wiped it — warn about it. expect(gap).toContain("resupply"); }); + it("maps a dependency-mode is_justified block back to the orphan taskId", () => { + const [gap] = describeCoverageGaps( + { + warnings: [{ blocked_by: ["plan_coverage.task_stray is_justified"] }], + } as never, + { task_stray: "stray-work" }, + ); + expect(gap).toContain('Task "stray-work" is ORPHAN'); + expect(gap).toContain("dependsOn"); + }); + it("still reports a dropped requirement (uncovered) distinctly", () => { const gaps = describeCoverageGaps( { diff --git a/src/runtime/gate-tools.ts b/src/runtime/gate-tools.ts index 7613944..b404bfb 100644 --- a/src/runtime/gate-tools.ts +++ b/src/runtime/gate-tools.ts @@ -236,6 +236,25 @@ async function runPlanCoverageGate(input: { ].join("\n"), ); } + if (compiled.unknownDependencyRefs.length > 0) { + return blocked( + [ + "Some tasks declare a `dependsOn` id that names no task in this plan:", + ...compiled.unknownDependencyRefs.map( + (ref) => `- task ${ref.taskId} → dependsOn ${ref.dependsOn}`, + ), + "Fix the task via planner_task_upsert (exact taskIds — dependsOn takes taskIds, not REQ-n), or create the missing task.", + ].join("\n"), + ); + } + if (compiled.dependencyCycle) { + return blocked( + [ + `The task dependency graph has a cycle: ${compiled.dependencyCycle.join(" → ")}.`, + "dependsOn must form a DAG (foundations before composition). Break the cycle via planner_task_upsert — a task cannot transitively depend on itself.", + ].join("\n"), + ); + } const run = await runGateProgram({ fs: input.fs, planPaths: input.planPaths, @@ -277,7 +296,7 @@ async function runPlanCoverageGate(input: { : []), consistent ? "CONSISTENT: every in-scope requirement is discharged and no task is orphan work. Record the conclusion in decisions.md, then call planner_finish_step." - : "Not CONSISTENT: the plan drops a requirement or carries orphan work. Fix the tasks (planner_task_upsert with the right `requirements`), or de-scope a requirement through a recorded user decision, then re-run planner_gate_check.", + : "Not CONSISTENT: the plan drops a requirement or carries orphan work. Fix the tasks (planner_task_upsert — cite the REQ-n a task discharges, or give an infra task a `dependsOn` on the task that needs it), or de-scope a requirement through a recorded user decision, then re-run planner_gate_check.", ].join("\n"), details: { gate: "plan_coverage", @@ -339,7 +358,11 @@ export async function planCoverageSourceHash( ): Promise { const traceability = [...tasks] .sort((a, b) => a.taskId.localeCompare(b.taskId)) - .map((task) => [task.taskId, [...(task.requirements ?? [])].sort()]); + .map((task) => [ + task.taskId, + [...(task.requirements ?? [])].sort(), + [...(task.dependsOn ?? [])].sort(), + ]); return sha256( `${await fs.readText(planPaths.specJson)}\n${JSON.stringify(traceability)}`, ); @@ -350,17 +373,24 @@ export function describeCoverageGaps( taskSubjects: Record, ): string[] { const gaps: string[] = []; + const orphanMessage = (taskId: string) => + `Task "${taskId}" is ORPHAN work. Either cite the REQ-n it discharges via planner_task_upsert, or — if it is infrastructure that implements no requirement — declare it as a \`dependsOn\` of the task that builds on it (foundations before composition), so a discharging task justifies it. There is no delete tool: to retire a redundant task, fold its scope into another. Upsert replaces the whole task, so resupply \`requirements\`/\`dependsOn\` every time.`; for (const warning of report.warnings ?? []) { for (const blocked of warning.blocked_by ?? []) { - const subject = blocked.split(" ")[0] ?? blocked; + // TOTAL warnings print a bare subject; a PREMISE blocked_by is + // domain-qualified (`plan_coverage. is_justified`). + const subject = (blocked.split(" ")[0] ?? blocked).replace( + /^plan_coverage\./, + "", + ); if (blocked.includes("no covered_by witness")) { gaps.push( `${specSubjectToRequirementId(subject)} is DROPPED — no task discharges it. Add it to a task's \`requirements\` via planner_task_upsert, or de-scope it through a recorded user decision.`, ); } else if (blocked.includes("no traces witness")) { - gaps.push( - `Task "${taskSubjects[subject] ?? subject}" is ORPHAN work — it traces to no requirement. Re-run planner_task_upsert (same taskId) citing the REQ-n it discharges OR enables — a setup/infrastructure task cites the requirement it is a prerequisite for (e.g. a "cargo init" task cites the REQ whose code it makes buildable). There is no delete tool: to retire a redundant task instead, fold its scope into the task that already covers that REQ. Upsert replaces the whole task, so resupply \`requirements\` every time or it is wiped back to orphan.`, - ); + gaps.push(orphanMessage(taskSubjects[subject] ?? subject)); + } else if (blocked.includes("is_justified")) { + gaps.push(orphanMessage(taskSubjects[subject] ?? subject)); } else { gaps.push(`Blocked by \`${blocked}\`.`); } diff --git a/src/runtime/task-tools.test.ts b/src/runtime/task-tools.test.ts index 39facad..185c6cb 100644 --- a/src/runtime/task-tools.test.ts +++ b/src/runtime/task-tools.test.ts @@ -98,6 +98,29 @@ describe("planner task tools", () => { }); }); + it("persists dependsOn through the upsert tool", async () => { + const setup = await createTaskSetup(); + const result = await executePlannerTaskTool({ + ...setup, + toolName: "planner_task_upsert", + params: { + taskId: "model-task", + title: "Model", + objective: "Builds on scaffolding.", + scope: ["src/model.ts"], + acceptanceCriteria: ["Depends on setup."], + dependsOn: ["setup-project"], + }, + }); + expect(result.status).toBe("applied"); + await expect( + readTaskRecord( + setup.fs, + createTaskStoragePaths(setup.planPaths, "model-task"), + ), + ).resolves.toMatchObject({ dependsOn: ["setup-project"] }); + }); + it("blocks reopening a completed task id during follow-up planning", async () => { const setup = await createTaskSetup(); const createResult = await executePlannerTaskTool({ diff --git a/src/runtime/task-tools.ts b/src/runtime/task-tools.ts index 19bdefe..d86bbcf 100644 --- a/src/runtime/task-tools.ts +++ b/src/runtime/task-tools.ts @@ -31,6 +31,7 @@ const TASK_UPSERT_SCHEMA = { "Each criterion is one observable, testable outcome.", ), requirements: stringArray("Cite exact REQ-n ids from spec.json."), + dependsOn: stringArray("taskIds this task builds on — not REQ-n ids."), contractChain: stringArray(), relevantContracts: stringArray(), forbiddenAreas: stringArray(), diff --git a/src/runtime/workflow-tools.ts b/src/runtime/workflow-tools.ts index 84b73b8..43a13a4 100644 --- a/src/runtime/workflow-tools.ts +++ b/src/runtime/workflow-tools.ts @@ -300,7 +300,7 @@ async function validatePlanCoverageGatePassed( return 'This plan has a spec, so requirement coverage is a hard gate. Call planner_gate_check with gate: "plan_coverage" at planning/consistency_check and reach CONSISTENT before advancing.'; } if (lastCheck.outcome !== "CONSISTENT") { - return `The latest plan_coverage gate ended in ${lastCheck.outcome} — a requirement is dropped or a task is orphan work. Fix the tasks' \`requirements\` via planner_task_upsert (or de-scope through a recorded user decision), then re-run planner_gate_check.`; + return `The latest plan_coverage gate ended in ${lastCheck.outcome} — a requirement is dropped or a task is orphan work. Fix the tasks via planner_task_upsert (cite the REQ-n a task discharges, or give an infra task a \`dependsOn\` on the task that needs it; or de-scope through a recorded user decision), then re-run planner_gate_check.`; } if (lastCheck.sourceHash) { const plan = await readPlanRecord(fs, planPaths); @@ -315,7 +315,7 @@ async function validatePlanCoverageGatePassed( } const currentHash = await planCoverageSourceHash(fs, planPaths, tasks); if (lastCheck.sourceHash !== currentHash) { - return "spec.json or a task's requirements changed after the last plan_coverage pass — the verdict is stale. Re-run planner_gate_check at planning/consistency_check."; + return "spec.json or a task's requirements/dependsOn changed after the last plan_coverage pass — the verdict is stale. Re-run planner_gate_check at planning/consistency_check."; } } return null; diff --git a/src/storage/AGENTS.md b/src/storage/AGENTS.md index 1ec42a9..4261083 100644 --- a/src/storage/AGENTS.md +++ b/src/storage/AGENTS.md @@ -40,7 +40,7 @@ Storage domain for persisted planner records, paths, JSON IO, schema defaults, s - `migrate-layout.ts` → `migrateLayout` runs from the `/planner-create` and `/planner-resume` command handlers (not on every session start), before the command reads a plan so resume finds it at the nested path (best-effort, idempotent): moves legacy flat `extensionDir/plans/` into the owning `projects//plans/` (attributed via `project.json`), drops the stale `skills/bundled/` system-skill dir, and removes the legacy `plans/` and global `skills/` dirs once they are empty. Never destroys a source on a destination collision; leaves orphan plans and the legacy global user-skill pool untouched. - `plan-store.ts` → `initializePlanFiles` scaffolds a new plan's directory (creates `tasksDir`/`contractsBaselineDir`, writes empty request/goal/plan/discovery/questions/decisions/verify markdown placeholders) and saves `plan.json`; `readPlanRecord`/`updatePlanRecord` are the read/update API runtime uses for `PlanRecord`. Distinct from `state-store.ts`, which owns `state.json` (runtime/transition data) rather than `plan.json` (static plan metadata). - `project-store.ts` → owns `project.json` per project (one project can have many plans). `ensureProjectRecord` creates-if-missing; `setActivePlan`/`upsertProjectPlanSummary` are the only mutators — `setActivePlan` is how the extension tracks which plan is "current" across sessions. -- `task-store.ts` → `upsertTaskArtifacts` writes both `task.json` (`TaskRecord`) and a rendered `task.md` (objective/scope/acceptance criteria/contract chain/forbidden areas/domain details sections) from the same input, and touches `tdd.md`/`refactor.md` placeholders if absent. `updateTaskStatus` is the only place `TaskRecord.status` changes. Task IDs are validated through `sanitizeIdPart` from `ids.ts` to guarantee they're safe path segments. +- `task-store.ts` → `upsertTaskArtifacts` writes both `task.json` (`TaskRecord`) and a rendered `task.md` (objective/scope/acceptance criteria/depends-on/contract chain/forbidden areas/domain details sections) from the same input, and touches `tdd.md`/`refactor.md` placeholders if absent. `TaskRecord.requirements` is the REQ-n ids the task DISCHARGES (never enables); `TaskRecord.dependsOn` is the taskIds it builds on — the plan_coverage gate justifies a non-discharging setup task by having a discharging task depend on it. Both default to `[]` on read so legacy `task.json` parses. `updateTaskStatus` is the only place `TaskRecord.status` changes. Task IDs are validated through `sanitizeIdPart` from `ids.ts` to guarantee they're safe path segments. - `spec-store.ts` → the SDD spec artifact (`spec.json` + rendered `spec.md`, SPEC.md §5.1): `SpecRecord` validation is the local-model hardening line (strict `REQ-n`/`CON-n`/`ASM-n` ids, VRF-safe lowercase snake_case atoms, the REQ-14 freedom valve — a missing `acceptanceAtom` requires `deferral.rationale`), plus optional machine-checkable constraint relations (`implies`/`exclusive`/`oneof`/`atleast`). `readSpecRecordIfExists` returning null = supported legacy state. - `behavior-store.ts` → per-task `behaviors.json` (the test-coverage toggle board): `BHV-n` entries with the mechanical `planned → red → green` ladder; `planned → green` is rejected (test-first by data), a red/green behavior cannot silently vanish from a resubmit, and a red+ behavior must name its witnessing test. - `compact-timing-store.ts` → per-project rolling history (`compact-timing.json`, newest `COMPACT_TIMING_MAX_SAMPLES`) of `(tokens, ms, model, at)` compaction samples, feeding the empirical ETA in `runtime/compact-eta.ts`. `readCompactTimingHistory` degrades absent/corrupt files to empty (never throws); `recordCompactTiming` is best-effort (a write failure is swallowed so it can never break compaction). Path comes from `paths.ts` `compactTimingJson`. diff --git a/src/storage/schema.ts b/src/storage/schema.ts index 6c62862..475be28 100644 --- a/src/storage/schema.ts +++ b/src/storage/schema.ts @@ -231,6 +231,12 @@ export interface TaskRecord { // Spec traceability (SDD): REQ-n ids from spec.json this task discharges. // Optional and defaulted to [] on read so legacy task.json files parse. requirements?: string[]; + // Build-order dependencies: taskIds this task depends on (foundations first). + // The plan_coverage gate justifies a non-discharging task by having a + // discharging task (transitively) depend on it — a setup task is not orphan + // because it borrows a REQ, but because real work depends on it. Optional and + // defaulted to [] on read so legacy task.json files parse. + dependsOn?: string[]; contractChain?: string[]; relevantContracts?: string[]; forbiddenAreas?: string[]; diff --git a/src/storage/task-store.test.ts b/src/storage/task-store.test.ts index 837cf6e..3599e44 100644 --- a/src/storage/task-store.test.ts +++ b/src/storage/task-store.test.ts @@ -66,6 +66,38 @@ describe("planner task store", () => { expect((await readTaskRecord(fs, result.paths)).requirements).toEqual([]); }); + it("persists dependsOn, renders it, and defaults it to [] for a legacy record", async () => { + const fs = new MockPlannerFs(); + const planPaths = createPlanStoragePaths( + createProjectStoragePaths({ + agentDir: "/agent", + projectRoot: "/repo/app", + }), + "plan-a", + ); + const result = await upsertTaskArtifacts(fs, planPaths, { + taskId: "model-task", + title: "Model", + objective: "Depends on scaffolding.", + scope: [], + acceptanceCriteria: ["Builds on setup."], + dependsOn: ["setup-project", "setup-project"], + }); + // Deduped and rendered. + expect((await readTaskRecord(fs, result.paths)).dependsOn).toEqual([ + "setup-project", + ]); + const md = await fs.readText(result.paths.taskMd); + expect(md).toContain("## Depends On"); + expect(md).toContain("- setup-project"); + + // A record written before the field existed still reads as []. + const raw = JSON.parse(await fs.readText(result.paths.taskJson)); + delete raw.dependsOn; + await fs.writeTextAtomic(result.paths.taskJson, JSON.stringify(raw)); + expect((await readTaskRecord(fs, result.paths)).dependsOn).toEqual([]); + }); + it("persists requirements and renders them into task.md", async () => { const fs = new MockPlannerFs(); const planPaths = createPlanStoragePaths( diff --git a/src/storage/task-store.ts b/src/storage/task-store.ts index c098e05..eac61cb 100644 --- a/src/storage/task-store.ts +++ b/src/storage/task-store.ts @@ -17,6 +17,7 @@ export interface UpsertTaskArtifactsInput { scope: string[]; acceptanceCriteria: string[]; requirements?: string[]; + dependsOn?: string[]; contractChain?: string[]; relevantContracts?: string[]; forbiddenAreas?: string[]; @@ -42,6 +43,7 @@ export async function upsertTaskArtifacts( "acceptanceCriteria", ), requirements: stringArray(input.requirements ?? [], "requirements"), + dependsOn: stringArray(input.dependsOn ?? [], "dependsOn"), contractChain: stringArray(input.contractChain ?? [], "contractChain"), relevantContracts: stringArray( input.relevantContracts ?? [], @@ -64,9 +66,13 @@ export async function readTaskRecord( paths: TaskStoragePaths, ): Promise { const record = await readJson(fs, paths.taskJson); - // Legacy task.json files predate spec traceability; default the field so - // every consumer can rely on it being an array. - return { ...record, requirements: record.requirements ?? [] }; + // Legacy task.json files predate spec traceability and build-order deps; + // default the fields so every consumer can rely on them being arrays. + return { + ...record, + requirements: record.requirements ?? [], + dependsOn: record.dependsOn ?? [], + }; } export async function updateTaskStatus( @@ -109,6 +115,10 @@ function formatTaskMarkdown(task: TaskRecord): string { "", ...list(task.requirements ?? [], "(no spec traceability recorded)"), "", + "## Depends On", + "", + ...list(task.dependsOn ?? [], "(no build-order dependencies)"), + "", "## TDD Rule", "", "Tests, mocks, fixtures, implementation, refactor, and final checks belong to this task lifecycle. Do not create a separate testing task.", diff --git a/src/vrf/AGENTS.md b/src/vrf/AGENTS.md index 36e02aa..5d858a4 100644 --- a/src/vrf/AGENTS.md +++ b/src/vrf/AGENTS.md @@ -34,7 +34,7 @@ elenchus/VRF domain: the bundled premise-template library, its sync/routing plum - `routing.ts` → `getRecommendedVrfTemplates(stage, step)`: which template a step reaches for by default (always "use it or record not_applicable", never "decide whether it applies"). - `paths.ts` → template path/import helpers. - `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. +- `coverage-compiler.ts` → `compilePlanCoverage`: `spec.json` + each `TaskRecord.requirements`/`dependsOn` → self-contained witness tables. `TOTAL covered_by ON requirements` always names each dropped requirement. The orphan dimension has two modes: **dependency mode** (any task declares `dependsOn`) emits a justification web — a task is not orphan if it discharges a requirement OR a discharging task transitively depends on it (`depends_on` facts + `CLOSE depends_on TRANSITIVE` for reachability AND cycle rejection + `self_justified`/`dep_justified` RULEs + `every_task_justified` PREMISE); a cycle is found in TS (`dependencyCycle`) so the gate reports it cleanly instead of an engine crash. **Legacy mode** (no `dependsOn` anywhere) keeps the old `TOTAL traces ON tasks`, grandfathered so resume never breaks. Deferred requirements and non-goals never enter the requirement set — a freedom-valve deferral IS the discharge. This is what dissolves the borrowed-REQ trap: an infra task owns no requirement, so tdd_coverage never demands a behavior exercise one. - `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). - `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). diff --git a/src/vrf/coverage-compiler.test.ts b/src/vrf/coverage-compiler.test.ts index bb6f526..52e8988 100644 --- a/src/vrf/coverage-compiler.test.ts +++ b/src/vrf/coverage-compiler.test.ts @@ -40,7 +40,11 @@ function spec(input?: Partial) { }); } -function task(taskId: string, requirements: string[]): TaskRecord { +function task( + taskId: string, + requirements: string[], + dependsOn: string[] = [], +): TaskRecord { return { schemaVersion: SCHEMA_VERSION, taskId, @@ -50,6 +54,7 @@ function task(taskId: string, requirements: string[]): TaskRecord { scope: [], acceptanceCriteria: ["c"], requirements, + dependsOn, }; } @@ -128,6 +133,66 @@ describe("plan-coverage compiler through the real engine", () => { expect(compiled.program).not.toContain("req_9"); }); + it("dependency mode: an infra task that discharges nothing is justified by a dependent discharging task", async () => { + const compiled = compilePlanCoverage(spec(), [ + task("setup-project", []), // discharges nothing + task("alpha", ["REQ-1"], ["setup-project"]), + task("beta", ["REQ-2"], ["setup-project"]), + ]); + expect(compiled.mode).toBe("dependency"); + // No borrowed-REQ trace: setup-project owns no requirement. + expect(compiled.program).not.toContain("TOTAL traces ON tasks"); + expect(compiled.program).toContain("CLOSE depends_on TRANSITIVE"); + const report = await run(compiled.program); + expect(report.status).toBe("CONSISTENT"); + }); + + it("dependency mode: a truly orphan task (no discharge, nothing depends on it) is NAMED", async () => { + const compiled = compilePlanCoverage(spec(), [ + task("setup-project", []), + task("alpha", ["REQ-1", "REQ-2"], ["setup-project"]), + task("stray-work", []), // nothing depends on it, discharges nothing + ]); + const report = await run(compiled.program); + expect(report.status).toBe("WARNING"); + const blocked = report.warnings.flatMap((w) => w.blocked_by ?? []); + const subject = blocked + .find((b) => b.includes("is_justified")) + ?.split(" ")[0] + ?.replace(/^plan_coverage\./, ""); + expect(subject).toBeDefined(); + expect(compiled.taskSubjects[subject ?? ""]).toBe("stray-work"); + }); + + it("dependency mode: collects unknown dependsOn references", () => { + const compiled = compilePlanCoverage(spec(), [ + task("alpha", ["REQ-1", "REQ-2"], ["ghost-task"]), + ]); + expect(compiled.mode).toBe("dependency"); + expect(compiled.unknownDependencyRefs).toEqual([ + { taskId: "alpha", dependsOn: "ghost-task" }, + ]); + }); + + it("dependency mode: detects a dependency cycle in TS (no engine crash)", () => { + const compiled = compilePlanCoverage(spec(), [ + task("a", ["REQ-1"], ["b"]), + task("b", ["REQ-2"], ["a"]), + ]); + expect(compiled.dependencyCycle).not.toBeNull(); + expect(compiled.dependencyCycle).toContain("a"); + expect(compiled.dependencyCycle).toContain("b"); + // The cyclic CLOSE is withheld so the engine never sees an invalid program. + expect(compiled.program).not.toContain("CLOSE depends_on TRANSITIVE"); + }); + + it("stays in legacy mode when no task declares dependsOn", () => { + const compiled = compilePlanCoverage(spec(), [task("alpha", ["REQ-1"])]); + expect(compiled.mode).toBe("legacy"); + expect(compiled.program).toContain("TOTAL traces ON tasks"); + expect(compiled.program).not.toContain("is_justified"); + }); + it("is deterministic and sanitizes/deduplicates task subjects", () => { const tasks = [ task("Fix.Storage", ["REQ-1"]), diff --git a/src/vrf/coverage-compiler.ts b/src/vrf/coverage-compiler.ts index bdf4240..2695080 100644 --- a/src/vrf/coverage-compiler.ts +++ b/src/vrf/coverage-compiler.ts @@ -4,14 +4,26 @@ import { specRequirementSubject } from "./spec-compiler"; /** * Deterministic plan-coverage compiler (SPEC.md REQ-4b/4c): from `spec.json` - * plus each task's `requirements` traceability list it emits the Skolem - * witness tables the coverage gate runs: + * plus each task's traceability it emits the Skolem witness tables + logic web + * the coverage gate runs. Two totalities are always present: * * - `TOTAL covered_by ON requirements` — every in-scope, non-deferred * requirement must be the subject of at least one `covered_by` pair; the * engine NAMES each dropped requirement. - * - `TOTAL traces ON tasks` — every task must trace to at least one - * requirement; the engine NAMES each orphan task. + * + * The orphan dimension has two modes, chosen by the plan itself: + * + * - **dependency mode** (some task declares `dependsOn`): a task is not orphan + * if it DISCHARGES a requirement OR a discharging task (transitively) depends + * on it. Emitted as `depends_on` facts + `CLOSE depends_on TRANSITIVE` (which + * also rejects a dependency cycle — a DAG check the old model lacked) + two + * `RULE`s that derive `is_justified`, gated by `PREMISE every_task_justified`. + * This is what lets a `cargo init` task own zero requirements yet not be + * orphan work: the task that discharges REQ-1 depends on it. + * - **legacy mode** (no task declares `dependsOn` — every pre-dependsOn plan): + * the old `TOTAL traces ON tasks`, where every task must itself cite a + * requirement. Grandfathered so resuming an existing plan never breaks; a + * plan opts into dependency mode the moment any task declares `dependsOn`. * * Requirements discharged through the freedom valve (deferral) and non-goals * never enter the requirement set (REQ-3, §2.2): a deferral IS the discharge. @@ -20,8 +32,7 @@ import { specRequirementSubject } from "./spec-compiler"; * data and do not cross files, so the sets, the witness pairs, and the TOTAL * lines must live in one generated file. That is fine — this program is * compiler-authored end to end (REQ-12), there is nothing for a model to get - * wrong. Plain `CHECK` suffices: everything here is data, and TOTAL is a - * compile-time scan. + * wrong. */ export interface CompiledPlanCoverage { @@ -32,6 +43,11 @@ export interface CompiledPlanCoverage { taskCount: number; /** Requirements a task cites that the spec does not know (hard error upstream). */ unknownRequirementRefs: Array<{ taskId: string; requirement: string }>; + /** dependsOn ids that name no task in the plan (hard error upstream). */ + unknownDependencyRefs: Array<{ taskId: string; dependsOn: string }>; + /** A dependency cycle among tasks, as an ordered taskId path, or null. */ + dependencyCycle: string[] | null; + mode: "legacy" | "dependency"; } /** `fix-storage-root` → `task_fix_storage_root` (collision-checked). */ @@ -47,6 +63,44 @@ function taskSubjectFor(taskId: string, used: Set): string { return candidate; } +/** + * First dependency cycle among the tasks (over declared, in-plan edges), as an + * ordered taskId path `a → b → … → a`, or null for a DAG. Detected in TS so the + * gate reports a clean message instead of relying on the engine's CLOSE crash. + */ +function findDependencyCycle( + adjacency: Map, +): string[] | null { + const WHITE = 0; + const GREY = 1; + const BLACK = 2; + const color = new Map(); + const stack: string[] = []; + let cycle: string[] | null = null; + + function visit(node: string): boolean { + color.set(node, GREY); + stack.push(node); + for (const next of adjacency.get(node) ?? []) { + const c = color.get(next) ?? WHITE; + if (c === GREY) { + const from = stack.indexOf(next); + cycle = [...stack.slice(from), next]; + return true; + } + if (c === WHITE && visit(next)) return true; + } + stack.pop(); + color.set(node, BLACK); + return false; + } + + for (const node of adjacency.keys()) { + if ((color.get(node) ?? WHITE) === WHITE && visit(node)) break; + } + return cycle; +} + export function compilePlanCoverage( spec: SpecRecord, tasks: readonly TaskRecord[], @@ -59,14 +113,31 @@ export function compilePlanCoverage( ); const knownRequirementIds = new Set(spec.requirements.map((req) => req.id)); + const coverableIds = new Set(coverable.map((req) => req.id)); + const taskIds = new Set(orderedTasks.map((task) => task.taskId)); + const usedSubjects = new Set(); const taskSubjects: Record = {}; + const subjectByTaskId = new Map(); + for (const task of orderedTasks) { + const subject = taskSubjectFor(task.taskId, usedSubjects); + taskSubjects[subject] = task.taskId; + subjectByTaskId.set(task.taskId, subject); + } + const unknownRequirementRefs: CompiledPlanCoverage["unknownRequirementRefs"] = []; + const unknownDependencyRefs: CompiledPlanCoverage["unknownDependencyRefs"] = + []; + + const usesDeps = orderedTasks.some( + (task) => (task.dependsOn ?? []).length > 0, + ); + const mode: CompiledPlanCoverage["mode"] = usesDeps ? "dependency" : "legacy"; const lines: string[] = [ "// Generated by pi-code-planner's deterministic coverage compiler from", - "// spec.json + the tasks' requirements traceability. Do not edit by hand.", + "// spec.json + the tasks' traceability. Do not edit by hand.", "DOMAIN plan_coverage", "", ]; @@ -81,40 +152,99 @@ export function compilePlanCoverage( if (orderedTasks.length > 0) { lines.push("SET tasks"); for (const task of orderedTasks) { - const subject = taskSubjectFor(task.taskId, usedSubjects); - taskSubjects[subject] = task.taskId; - lines.push(` ${subject}`); + lines.push(` ${subjectByTaskId.get(task.taskId) as string}`); } lines.push(""); } - const coverableIds = new Set(coverable.map((req) => req.id)); + // covered_by witnesses (both modes): a task's cited requirement covers it. for (const task of orderedTasks) { - const subject = Object.keys(taskSubjects).find( - (key) => taskSubjects[key] === task.taskId, - ) as string; + const subject = subjectByTaskId.get(task.taskId) as string; for (const requirement of [...(task.requirements ?? [])].sort()) { if (!knownRequirementIds.has(requirement)) { unknownRequirementRefs.push({ taskId: task.taskId, requirement }); continue; } - // A pair citing a deferred/out-of-scope requirement still counts as - // the task's own trace, but only coverable requirements are totaled. - const reqSubject = specRequirementSubject(requirement); if (coverableIds.has(requirement)) { - lines.push(`FACT ${reqSubject} covered_by ${subject}`); + lines.push( + `FACT ${specRequirementSubject(requirement)} covered_by ${subject}`, + ); } - lines.push(`FACT ${subject} traces ${reqSubject}`); } } - lines.push(""); - if (coverable.length > 0) { - lines.push("TOTAL covered_by ON requirements"); - } - if (orderedTasks.length > 0) { - lines.push("TOTAL traces ON tasks"); + let dependencyCycle: string[] | null = null; + + if (mode === "legacy") { + // Every task must itself cite a coverable-or-deferred requirement. + for (const task of orderedTasks) { + const subject = subjectByTaskId.get(task.taskId) as string; + for (const requirement of [...(task.requirements ?? [])].sort()) { + if (!knownRequirementIds.has(requirement)) continue; // already flagged + lines.push( + `FACT ${subject} traces ${specRequirementSubject(requirement)}`, + ); + } + } + lines.push(""); + if (coverable.length > 0) lines.push("TOTAL covered_by ON requirements"); + if (orderedTasks.length > 0) lines.push("TOTAL traces ON tasks"); + } else { + // Dependency mode: justify each task structurally. + const adjacency = new Map(); + for (const task of orderedTasks) adjacency.set(task.taskId, []); + for (const task of orderedTasks) { + for (const dep of [...new Set(task.dependsOn ?? [])].sort()) { + if (!taskIds.has(dep)) { + unknownDependencyRefs.push({ taskId: task.taskId, dependsOn: dep }); + continue; + } + adjacency.get(task.taskId)?.push(dep); + } + } + dependencyCycle = findDependencyCycle(adjacency); + + for (const task of orderedTasks) { + const subject = subjectByTaskId.get(task.taskId) as string; + lines.push(`FACT ${subject} in_plan`); + } + for (const task of orderedTasks) { + const subject = subjectByTaskId.get(task.taskId) as string; + const discharges = [...(task.requirements ?? [])].some((req) => + coverableIds.has(req), + ); + if (discharges) lines.push(`FACT ${subject} discharges_req`); + } + let edgeCount = 0; + for (const task of orderedTasks) { + const subject = subjectByTaskId.get(task.taskId) as string; + for (const dep of adjacency.get(task.taskId) ?? []) { + lines.push( + `FACT ${subject} depends_on ${subjectByTaskId.get(dep) as string}`, + ); + edgeCount += 1; + } + } + // CLOSE rejects a cycle at compile time; skip it when TS already found one + // so the gate can report a clean message instead of an engine crash. + if (edgeCount > 0 && !dependencyCycle) { + lines.push("CLOSE depends_on TRANSITIVE"); + } + lines.push(""); + if (coverable.length > 0) lines.push("TOTAL covered_by ON requirements"); + lines.push( + "RULE self_justified FOR EACH t IN tasks:", + " WHEN t discharges_req", + " THEN t is_justified", + "RULE dep_justified FOR EACH d depends_on t:", + " WHEN d discharges_req", + " THEN t is_justified", + "PREMISE every_task_justified FOR EACH t IN tasks:", + " WHEN t in_plan", + " THEN t is_justified", + ); } + lines.push("", "CHECK"); return { @@ -123,5 +253,8 @@ export function compilePlanCoverage( requirementCount: coverable.length, taskCount: orderedTasks.length, unknownRequirementRefs, + unknownDependencyRefs, + dependencyCycle, + mode, }; }