design: SPEC/PLAN authority architecture and executable design gate #379

Closed
nsaspy wants to merge 28 commits from docs/spec-seeded-symbolic-plans into main
Owner

Summary

Replaces the failed PR #290 design with a rewritten, executable design record
for the SPEC / VALIDATE / PLAN authority architecture, plus the design gate
that validates it through real merged code. This is no longer a docs-only PR:
it changes CI, an executable gate script, research KB state, deterministic
corpus, and two live tests.

  • docs/research/spec-plan-authority.md — full design record: canonical SPEC
    language (merged rlm_spec_lang grammar unchanged), BASE adoption of
    rage/288-spec-plan-graph-executor with explicitly declared D6 deltas
    (D6-1..D6-10), expert contracts and inner capabilities, TDD RED/GREEN
    evidence contract, HTTP/network assertion model, PLAN→SPEC compatibility and
    replan safety, durability (forward projection, never compaction), S0–S11
    implementation DAG.
  • scripts/design_gate.pl — executable design gate (deterministic; no model
    or network calls) validating the normative design through real merged
    parsers, the adopted BASE module, and gate-local normative checkers:
    59 checks in 13 groups, all green.
  • research/spec-plan-refinement-kb.pl + -state.pl — hardened research KB
    with machine-checked evidence refs (kb_evidence_refs_resolve).
  • .github/workflows/ci.yml — design-gate step with non-fatal BASE fetch;
    the BASE object is pinned by commit id
    (71a10ae…, rage/288-spec-plan-graph-executor now pushed to this remote).
  • test/deterministic_corpus.pl — manifest entries for two tests added on
    main without corpus entries (main's own unit lane was red for this;
    b654831/eb2411a).
  • test/live_conversation_scale_openrouter_test.pl,
    test/live_completion_openrouter_test.pl — assertions corrected to pin the
    runtime retrieval contract rather than one model-authored plan shape; child
    session token headroom + reasoning-effort pinned. No test was skipped,
    xfailed, or weakened into accepting a wrong answer.

Runtime invariant implemented (design level): model output is inert data —
SPEC compilation grants nothing (closed metadata schema, no capability field),
planning cannot widen authority, plans seed only from a fingerprint-verified
frozen spec, dropped obligations are unrecoverable, and patches re-run the
full validation chain against the same frozen ref.

Non-goals

  • No production runtime implementation of the D6 deltas, expert packs, plan
    KB, or plan_validate_against_spec/4 (slices S0–S11 in §13).
  • No merge of the rlm_direct/rlm_spec_strategy substrates (S10).
  • No change to the merged SPEC/PLAN/VERIFY public APIs.

Evidence

  • Design gate: 59/59 checks green at head, in this worktree and in fresh
    --no-local GitHub clones of the PR head (thin-clone BASE-missing case
    halts 1 with the candidate list; after the CI fetch step the pinned id
    resolves).
  • Deterministic suites: check_runtime, load_all, PlUnit gate-report mode
    1066/1066 in 92 suites, benchmark/run.pl -- deterministic 16/16,
    CLI demo/trace smoke.
  • Paid live lane with OPENROUTER_TEST_MODEL=z-ai/glm-5.3-flash: 11/11.
    This does not prove the required CI lane (which pins
    openai/gpt-oss-120b via the repo variable).

Known separate issue (pre-existing on main, not introduced here)

live_planner_context_openrouter_test fails with the pinned
openai/gpt-oss-120b. Characterized across consecutive runs: the failures
move between stages (one-hop tool_result_envelope_field references;
ungranted parallel op; malformed step) — stochastic plan-authoring
fragility under this harness rather than one deterministic defect. This
predates the PR: main's own paid lane fails identically (run 33254062233 at
b654831), and this branch's lane failed the same way before this slice
(runs at 5bb2817, 7c9e007).

14b6ec7 improves the runtime's planner repair loop for every model (with
deterministic test coverage): tool_result_envelope_field retries now teach
the corrected two-hop envelope form, capability_denied retries name the
denied capability plus the granted list, and the rlm-operate skill body
states the one-hop rejection rule up front. This does not make the 120b lane
green and is not claimed to. A dedicated follow-up slice should own it with
120B-specific live evidence; the z-ai/glm-5.3-flash 11/11 run is not
offered as evidence for that lane.

Follow-up scope after merge

  • S0: merge the rage/288 BASE unchanged (its branch is now published).
  • S1–S11 per §13; roadmap reconciliation in the same slices.
  • Own the 120B planner-context failure in a dedicated slice with live
    evidence on that model.
## Summary Replaces the failed PR #290 design with a rewritten, executable design record for the SPEC / VALIDATE / PLAN authority architecture, plus the design gate that validates it through real merged code. This is no longer a docs-only PR: it changes CI, an executable gate script, research KB state, deterministic corpus, and two live tests. - `docs/research/spec-plan-authority.md` — full design record: canonical SPEC language (merged `rlm_spec_lang` grammar unchanged), BASE adoption of `rage/288-spec-plan-graph-executor` with explicitly declared D6 deltas (D6-1..D6-10), expert contracts and inner capabilities, TDD RED/GREEN evidence contract, HTTP/network assertion model, PLAN→SPEC compatibility and replan safety, durability (forward projection, never compaction), S0–S11 implementation DAG. - `scripts/design_gate.pl` — executable design gate (deterministic; no model or network calls) validating the normative design through real merged parsers, the adopted BASE module, and gate-local normative checkers: **59 checks in 13 groups, all green**. - `research/spec-plan-refinement-kb.pl` + `-state.pl` — hardened research KB with machine-checked evidence refs (`kb_evidence_refs_resolve`). - `.github/workflows/ci.yml` — design-gate step with non-fatal BASE fetch; the BASE object is pinned by commit id (`71a10ae…`, `rage/288-spec-plan-graph-executor` now pushed to this remote). - `test/deterministic_corpus.pl` — manifest entries for two tests added on main without corpus entries (main's own unit lane was red for this; `b654831`/`eb2411a`). - `test/live_conversation_scale_openrouter_test.pl`, `test/live_completion_openrouter_test.pl` — assertions corrected to pin the runtime retrieval contract rather than one model-authored plan shape; child session token headroom + reasoning-effort pinned. No test was skipped, xfailed, or weakened into accepting a wrong answer. Runtime invariant implemented (design level): model output is inert data — SPEC compilation grants nothing (closed metadata schema, no capability field), planning cannot widen authority, plans seed only from a fingerprint-verified frozen spec, dropped obligations are unrecoverable, and patches re-run the full validation chain against the same frozen ref. ## Non-goals - No production runtime implementation of the D6 deltas, expert packs, plan KB, or `plan_validate_against_spec/4` (slices S0–S11 in §13). - No merge of the `rlm_direct`/`rlm_spec_strategy` substrates (S10). - No change to the merged SPEC/PLAN/VERIFY public APIs. ## Evidence - Design gate: 59/59 checks green at head, in this worktree and in fresh `--no-local` GitHub clones of the PR head (thin-clone BASE-missing case halts 1 with the candidate list; after the CI fetch step the pinned id resolves). - Deterministic suites: `check_runtime`, `load_all`, PlUnit gate-report mode 1066/1066 in 92 suites, `benchmark/run.pl -- deterministic` 16/16, CLI demo/trace smoke. - Paid live lane with `OPENROUTER_TEST_MODEL=z-ai/glm-5.3-flash`: 11/11. This does not prove the required CI lane (which pins `openai/gpt-oss-120b` via the repo variable). ## Known separate issue (pre-existing on main, not introduced here) `live_planner_context_openrouter_test` fails with the pinned `openai/gpt-oss-120b`. Characterized across consecutive runs: the failures move between stages (one-hop `tool_result_envelope_field` references; ungranted `parallel` op; malformed step) — stochastic plan-authoring fragility under this harness rather than one deterministic defect. This predates the PR: main's own paid lane fails identically (run 33254062233 at `b654831`), and this branch's lane failed the same way before this slice (runs at `5bb2817`, `7c9e007`). `14b6ec7` improves the runtime's planner repair loop for every model (with deterministic test coverage): `tool_result_envelope_field` retries now teach the corrected two-hop envelope form, `capability_denied` retries name the denied capability plus the granted list, and the rlm-operate skill body states the one-hop rejection rule up front. This does not make the 120b lane green and is not claimed to. A dedicated follow-up slice should own it with 120B-specific live evidence; the `z-ai/glm-5.3-flash` 11/11 run is not offered as evidence for that lane. ## Follow-up scope after merge - S0: merge the rage/288 BASE unchanged (its branch is now published). - S1–S11 per §13; roadmap reconciliation in the same slices. - Own the 120B planner-context failure in a dedicated slice with live evidence on that model.
Define the concrete architecture before implementation: intent features,
environment-aware validateSpec hard gate with structured spec_fault
diagnostics, fingerprint-gated plan_seed_from_spec compiler, plan-vs-spec
validation with typed patches, project retrieval/write/validation engines
over normalized symbolRef/sourceSpan/revision grammar, data-driven expert
mapping, expert-scoped context compilation, direct/symbolic/recursive
strategy selection, lambda-RLM combinator mapping, long-horizon KB, and
implementation slices S1-S10. Includes the Prolog refinement KB (drives
the work itself), a design-consistency gate script, corrected flow in
typed-plans.md, and the roadmap pointer.
Replace the presence-only #288 contract script with scripts/design_gate.pl,
which validates the normative design through real implementations (merged
main modules, unmerged rage/288 BASE, and new D6 design targets). Harden the
refinement KB completion discipline: bare status(done) without completion
evidence or a validated decision is a kb_violation. Wire the gate into CI
and update the roadmap slice descriptions (S0-S11).
- durability is forward projection, never compaction: append-only logs with
  monotone ids, projection cursor advances, boundary summaries carry the
  covered message-id range, prior ranges stay addressable via context ops
  (supersedes rlm_conversation_warm compaction in S11; resolves the plan-KB
  compaction open question)
- hard requirement 7.3: no mode one-shots; every model/harness exchange
  re-projects current project state into the model context across direct,
  typed_plan, and recursive_symbolic modes, with RED-test obligations on
  S5/S10/S11
- record both as validated research-KB decisions (d12 dec_forward_projection,
  d06 dec_multi_run_state)
Recursive adversarial review (glm-5.3-flash) of the SPEC/PLAN rewrite at
5bb2817: verdict NEEDS-CHANGES — B1 CI-unresolvable BASE ref; M1 vacuous
capability-safety checks; M2 gameable obligation coverage; M3 dangling-
grammar contradiction on environment inputs; M4 IMPLEMENTED/UNMERGED
misclassification; M5 undefined project(read) shape; M6 missing
inner_capabilities field; M7 unresolvable KB evidence refs; M8 undeclared
BASE deltas (revision side, closed symbol_kind); minors incl. failing
live_conversation_scale lane. Includes the ordered fix prompt with the 11
gate checks to add.
B1: the bare local ref rage/288-spec-plan-graph-executor did not resolve
in canonical CI clones, making the required gate step permanently red.
The gate now pins the BASE object id, resolves it through an explicit
ordered candidate list (pinned id, refs/heads, refs/remotes/origin,
refs/remotes/github), fails with the candidate list in the fault message,
and asserts the resolved commit equals the pin (new base_ref_resolvable
check, written red-first). ci.yml fetches the BASE branch non-fatally
before the gate; the pinned id remains the authority. Design record 6.2
cites the pin. Verified in fresh thin/full local clones: missing object
halts 1 with candidates; after the CI fetch the pinned id resolves.
Replaces the self-comparing capability_unchanged (both sides read the
same static fact) with checks that read real API surfaces: the compiled
frozen outcome is walked for capability-shaped terms against the closed
merged rlm_tool capability model; a registry provider whose metadata
attempts a capability field is rejected by the real rlm_assertion
normalization with a clean twin attributing the rejection; and
host_observation_refusal drives a trusted capability-gated observer
through the real spec_observe_execute/5 collect ABI and spec_verify/4 —
refusal (indeterminate(policy_denied), unresolved, observer_control) is
computed from the side table + environment capability set, never
pre-set, with the granted twin proving the branch selection. Deletes the
pre-set-payload http_observe_denied_without_cap and the dead
require_ok/2 and environment_allows/3 helpers. KB d10 evidence refs and
design record 14 capability bullet updated to the new check ids.
d6_resolvable/6 resolves expr input(Name) from Environment.inputs FIRST,
then from dependency-closure step binds — exactly doc D6-1 and §11 item
5. Environment.inputs is threaded through d6_validate_graph/3,
d6_check_closure, d6_compat_dangling, and the dataflow round trip
(d6_validate_graph/2 keeps empty inputs for env-free graphs). Fixes the
inverted d6_compat_spec_inputs logic: a required SPEC input missing from
Environment.inputs is a fault regardless of any step referencing it;
the reference-based escape hatch is removed (§11 item 7). New
spec_input_env_dataflow check (written red-first): positive round trip
consumes a SPEC input_decl through expr(input(user_payload)) with the
resolved create content bound from the environment, the same graph
dangles with an empty environment, and the compat layer reports both
missing_spec_input and dangling_input independent of step references.
Obligations satisfy a plan_established requirement only when the
establishing step (per-kind op table: tdd_evidence admits edit|create —
its evidence contract is a code change, so no-op run steps prove
nothing) is transitively required by a validate/1 step carrying the
bound spec's fingerprint. The review's mutation graph (no-op run step
wired to validate) and a disconnected edit variant are permanent
negative checks (obligation_causal_link, written red-first: both were
accepted before). d6_apply_patch_full_chain/5 re-runs parse + env-aware
graph validation (dangling-input re-check included) + spec compat on the
patched graph — the compat-only re-check is gone; replan_drop_rejected
uses the full chain and new patch_full_chain rejects a patch whose
patched graph dangles, at the plan_validation phase. Doc §9/§11.2
updated to state the enforced rules.
§8.1 gains the required inner_capabilities:[capability] field D6-8 and
§8.2 already reference: expert inner-loop grants (e.g. model(P)),
distinct from the op's own required capabilities, validated against
environment grants at preflight. expert_contract_ok/2 now shape-checks
model_policy{provider:atom, max_iterations:>0} instead of accepting any
dict, closes budget_policy to shared_step_budget, closes completion to
applied_and_observed and failure to blocked|failed, requires non-empty
effects, and validates every capability element against the merged
rlm_tool capability model. New expert_contract_shape check (red-first
under the lax checker): missing inner_capabilities, inner widening,
bad model_policy, unknown budget/completion/failure atoms are all
rejected; widening check now covers inner capabilities too. Doc §8.1
updated.
Removes the undefined project(read) shape from doc §4.2: the merged
capability model is closed and has no project/1; index-backed symbol
observers require filesystem(observation), matching the gate side table.
observer_required_capabilities/2 is completed for ALL registry kinds
(record_count and public_api_compatible added) and a new
observer_side_table_complete check (red-first: two kinds had no entries)
enforces that every kind has an entry, every entry is a valid merged
capability shape, and every entry is observation-scoped across
network|filesystem|process — observation capability is never write
authority. A dedicated index(observation) capability is declared a NEW
DESIGN TARGET for S2. Doc §4.2 reconciled with the side table.
d6_args_shape_resolved/2 is now called on every resolved step the
dataflow round trip executes (locate/read/edit), upgrading the
equality-only check: admission-time substitution is followed by strict
post-resolution shape validation, making the adjacent comment true.
Resolved edit/create content accepts text as atom or SWI string and
validated edit_action dicts, matching D6-2's 'text or a valid
edit_action dict' contract; non-text values are rejected.
New kb_evidence_refs_resolve check (runs last; red-first): every
gate:<Id> evidence ref must name a check id the gate defines
(check/2 now registers check_defined/1), every design anchor must match
a GitHub-style slug parsed from the design record's own headings, and
source: refs must name checkout files/defined predicates or the loaded
pinned BASE module. Mutation-verified: bogus gate refs and phantom
anchors are rejected.

All KB state refs regenerated: the four dangling gate ids
(d6_dataflow_ok, http_schema_ok, http_malformed_rejected,
design_gate_passes) replaced with defined check ids, and every
design:#sN-style anchor replaced with real heading slugs; d06 gains the
missing §7.3 anchor for the multi-run claim.

dec_forward_projection (d12) and dec_multi_run_state (d06) are no
longer backed by self-authored refs only: forward_projection_snapshot
exercises the §12.2 data model (snapshot covers:[event_lo,event_hi] —
now part of the §12.1 snapshot schema and the gate snapshot schema —
plus boundary-summary id range as derived data over a trusted_runtime
range) and multi_run_reprojection pins the §7.3 mode table (one §7.1
normalization boundary; per-exchange re-projection obligations owned by
declared slices S5/S10/S11).
Declares the two undeclared BASE divergences from the review: D6-9 —
diff sides gain revision(revision_ref) (BASE side_valid/1 admits
path|ref|span only; S3 owns resolution; until then BASE rejects what
the D6 layer accepts) and D6-10 — symbol_kind is enforced as the closed
13-atom set at reconciliation (BASE decoding accepts any non-empty atom
kind). §6.2 now states explicitly that these Section 5 features are
deltas, not BASE features. New gate pins: symbol_kind_closed (D6 layer
accepts kind:function, rejects kind:frobnicate) and diff_revision_side
(accept head/working/committed/branch/remote sides, reject invalid
ones, and assert the unchanged BASE validator still rejects revision
sides). Verified against the real BASE module: revision-side graphs are
rejected by plan_graph_validate as claimed.
§2.1 no longer lists the native model_step_handler with charge-back as
merged-main rlm_plan capability (merged main has neither it nor
charge_native_model_execution/2 — verified against git show main).
§2.2 gains explicit UNMERGED rows for the branch-only rlm_plan handler
hook + charge-back (adoption via S10) and rlm_tool's extra
capability_shape(spec/1|plan/1) shapes. §8.2's self-contradictory
'merged native model_step_handler' sentence is rewritten: both the
handler hook and the charge-back predicate are UNMERGED, adoption is
S10. Gate header now states that the IMPLEMENTED layer loads this
checkout's modules and that branch-only features are validated as
UNMERGED-adoption surface, not merged main.
Subplans use rlm/2 (merged AST + design record §7.2); the phantom
strategy_select/3 reference is replaced by the single strategy_mode/2
normalization boundary (design record §7.1) with runtime atoms
direct|typed_plan, matching rlm_spec_strategy's actual normalize_mode.
path_template_name/2 now succeeds when {Name} occurs anywhere in the
path (embedded "/users/{id}" or whole "/{id}"), with a non-empty
alphanumeric name; a declared path_param without a matching template
still fails. New http_path_param_ok check (red-first under the
whole-template-only matcher) compiles a positive GET /users/{id}
endpoint contract with path_params {id:integer} and a derivable
missing_resource 404 scenario.
live_conversation_scale_openrouter_test failed 3/3 with the pinned paid
model because validate_model_retrieval pinned an exact three-transition
plan (context(search) -> model -> final) plus exact child echo and
model_calls >= 2. The real provider consistently emits a valid two-step
plan (context(search) -> final): per-generation payloads confirm HTTP
200, a correct cold search over 40000 messages hitting the exact needle
sequence/content, and a final value carrying the payload. The plan shape
is model free-choice inside the closed vocabulary, not a runtime
guarantee, so the test now pins the retrieval contract itself: exactly
one ok context(search) whose binding contains the exact needle match,
every step ok, final last, every model(openrouter) step (when the model
uses one) bound to a real provider response for the pinned model,
model_calls >= 1, and the exact payload present in the user-visible
answer. Dot-syntax dict access inside assertion/1 replaced with
get_dict/3 (it raises spurious instantiation errors in that context).
Passes 3/3 with z-ai/glm-5.3-flash.
Section 14 now lists the real per-group counts after the findings work
(base_adoption 1, spec_grammar 10, plan_base 7, d6_delta 7, dataflow 2,
capability_safety 4, replan 7, tdd_evidence 4, http_contract 5,
edit_action 6, durability+state_readability 3, kb_dag 3 = 59) and
describes each new check. Also fixes the singleton-variable warning in
evidence_ref_resolves/2.
live_completion_openrouter began failing against the pinned paid model
(z-ai/glm-5.3-flash, snapshot -20260826) after the adversarial review:
the depth-one child's 128-token completion budget was consumed entirely
by reasoning text (finish_reason length, empty content ->
missing_final_output), and with more headroom the child sometimes tried
to 'verify' the instruction via an ungranted context_slice tool call
(correctly refused at preflight: child capabilities are model-only).
The runtime behaved per contract in both paths. Test plumbing is
tightened instead of the invariant set: the child's max_tokens goes
128->512 and the completion session pins reasoning_effort(minimal),
which enforce_plan_reasoning_effort/2 propagates into the nested child
model step, suppressing runaway reasoning. Passes 3/3 with the pinned
model.
Appends the resolution section: every finding id (B1, M1-M8, m1-m6)
mapped to its closing commit with evidence, the TDD red-first ledger,
and the operational note on making the pinned BASE object fetchable in
canonical CI. Records the resolved-head state: design gate 59 checks in
13 groups green, deterministic suites 1061/1061, benchmark 16/16, demo
ok, git diff --check clean, paid live lane 11/11 with
z-ai/glm-5.3-flash.
Brings main's rlm_direct/rml_native_tool fixes and the two new
deterministic tests into the PR so the CI merge checkout is
self-consistent; main's own unit lane is red because those tests were
added without deterministic_corpus.pl manifest entries (pre-existing on
main, b654831/eb2411a) — the manifest entries are added in the next
commit.
Main added rlm_direct_context_peek_contract_test.pl and
rlm_native_any_schema_test.pl without deterministic_corpus.pl entries,
so the gate-report corpus rejects the unclassified candidates and both
main's unit lane (b654831/eb2411a) and this PR's merge-checkout lane
are red. Adds the two include entries (main is 8 commits ahead of the
PR base; both test files arrive via the main merge in the previous
commit). Gate-report mode now completes 1066/1066 in 92 suites.
gpt-oss-120b planner retries repeated the same authoring mistakes because
the repair diagnostics for two fault classes carried no actionable
content: tool_result_envelope_field rendered only the raw fault term
(now teaches the corrected two-hop envelope form), and capability_denied
errors have no detail key at all (now names the denied capability and
the granted capability list). The rlm-operate skill body additionally
states the one-hop rejection rule up front so first attempts avoid it.
Deterministic coverage: new planner_retry_explains_tool_result_envelope_field
test (red-first) and the existing repairable-without-execution test now
asserts the richer rendering. Full suite 1067/1067.

Live status (honest): this does NOT make the pinned 120b lane green.
Three consecutive 120b runs of live_planner_context failed at three
DIFFERENT stages (one-hop envelope fields, ungranted parallel op,
malformed step) — stochastic authoring fragility, documented in the PR
for a dedicated follow-up slice. Regression checks pass: 120b live
completion green, glm-5.3-flash planner-context green.
test(live): deduplicate all_steps_ok and keep helper clauses contiguous
Some checks failed
Tree-sitter FFI / Direct SWI-Prolog Tree-sitter FFI (pull_request) Successful in 3m24s
CI / REAL OpenRouter integration (pull_request) Has been skipped
Nix flake / Flake package and clean runtime load (pull_request) Failing after 7s
Clean SWI pack install / Install and load copied pack (pull_request) Successful in 1m55s
Paid OpenRouter / Pinned paid OpenRouter integration (pull_request) Failing after 1m50s
CI / Deterministic unit and load checks (pull_request) Successful in 3m45s
56e47596b7
Removes the duplicated all_steps_ok/1 clause pair left by the retrieval-
contract rework and groups the conversation-scale helper predicates so
plunit stops emitting discontiguous-clause warnings in the paid lane
logs. No behavior change: deterministic suite 1067/1067, live
conversation-scale green with the pinned glm model.
Author
Owner

Refinement pushed (88bca2e)

Branch reconciled against current main (a89175b, PR #286 runtime consolidation merged in; PR content preserved). The refined design is now defined in docs/research/spec-plan-authority.md — a design-only pass, no runtime changes.

Primary correction implemented in the design: the flow now runs INTENT → SPEC → VALIDATE SPEC (first-class hard gate) → Frozen Spec → PLAN COMPILER → plan KB → expert loop → observe → spec verification → replan/continue → FINAL. Gate invariants G1–G5: seeding accepts only a fingerprint-checked frozen_spec{}; invalid specs yield structured spec_fault/1 diagnostics and spec-source repair (never a plan); model text is inert until validated; spec repair and verification-time repair stay distinct; FINAL requires verification_report{status:passed}. Direct mode remains first-class (direct / symbolic / recursive_symbolic, host-selected, caller-pinnable).

Key reconciliations with merged reality (the PR's original sketch predated #286):

  • SPEC language: rlm_spec_lang's closed symbols already cover most seed constructs; the delta is minimal — input/2, artifact/2,3, forbidden/1, ordering/2, conflicts/2, spec-level evidence_policy/1. goal/validate/success/constraint map onto existing subject/require+assertion/output_contract/invariant rather than duplicating names.
  • validateSpec/3 extends the existing spec_validate/3 to be environment-aware with a diagnostics vocabulary (missing capability, contradictions, impossible requirements, dangling references, missing inputs, invalid output contracts, incompatible constraints, forbidden-effect conflicts, ordering cycles, no validation mechanism).
  • PLAN side: the merged rlm_plan closed AST stays the execution IR; the 12-op project vocabulary (rage/288 slice) desugars onto it; new plan_validate_against_spec + typed plan_patch keep model proposals candidate-only.
  • recursive_symbolic is not a new runtime — it is symbolic mode over the existing rlm_recursion_policy routes; λ-RLM split/map/filter/reduce/thresholds/termination map onto existing context ops, plan combinators, policy guards, and one new closed filter reducer.
  • Project engines (retrieval/diff/write/validation) are specified over symbolRef/sourceSpan/revision grammar with the write engine routed through the durable effect boundary (#79); tree-sitter stays internal to the index layer (#96–#99).

Managed by Prolog: research/spec-plan-refinement-kb.pl (+ persisted state) drove this refinement — 23 tasks, dependency graph, decisions, evidence; all done. scripts/spec_plan_authority_check.{pl,sh} is a deterministic design gate (schema shapes, example spec/plan, diagnostics vocabulary, slice graph, KB state): ALL CHECKS PASSED.

Evidence at this head: full deterministic suite 1061/1061 (90 suites), benchmark deterministic 16/16, check_runtime/load_all/CLI demo/make research-approval/git diff --check green.

Non-goals honored: no runtime/API changes in this PR; implementation is deferred to slices S1–S10 (dependency graph in §23 of the design record). The roadmap now points at the refinement record as the TaskIR/Phase-2/3 design input.

## Refinement pushed (`88bca2e`) Branch reconciled against current `main` (`a89175b`, PR #286 runtime consolidation merged in; PR content preserved). The refined design is now defined in **`docs/research/spec-plan-authority.md`** — a design-only pass, no runtime changes. **Primary correction implemented in the design:** the flow now runs INTENT → SPEC → **VALIDATE SPEC (first-class hard gate)** → Frozen Spec → PLAN COMPILER → plan KB → expert loop → observe → spec verification → replan/continue → FINAL. Gate invariants G1–G5: seeding accepts only a fingerprint-checked `frozen_spec{}`; invalid specs yield structured `spec_fault/1` diagnostics and spec-source repair (never a plan); model text is inert until validated; spec repair and verification-time repair stay distinct; FINAL requires `verification_report{status:passed}`. Direct mode remains first-class (`direct` / `symbolic` / `recursive_symbolic`, host-selected, caller-pinnable). **Key reconciliations with merged reality** (the PR's original sketch predated #286): - SPEC language: `rlm_spec_lang`'s closed symbols already cover most seed constructs; the delta is minimal — `input/2`, `artifact/2,3`, `forbidden/1`, `ordering/2`, `conflicts/2`, spec-level `evidence_policy/1`. `goal/validate/success/constraint` map onto existing `subject/require+assertion/output_contract/invariant` rather than duplicating names. - `validateSpec/3` extends the existing `spec_validate/3` to be environment-aware with a diagnostics vocabulary (missing capability, contradictions, impossible requirements, dangling references, missing inputs, invalid output contracts, incompatible constraints, forbidden-effect conflicts, ordering cycles, no validation mechanism). - PLAN side: the merged `rlm_plan` closed AST stays the execution IR; the 12-op project vocabulary (rage/288 slice) desugars onto it; new `plan_validate_against_spec` + typed `plan_patch` keep model proposals candidate-only. - `recursive_symbolic` is not a new runtime — it is symbolic mode over the existing `rlm_recursion_policy` routes; λ-RLM split/map/filter/reduce/thresholds/termination map onto existing context ops, plan combinators, policy guards, and one new closed `filter` reducer. - Project engines (retrieval/diff/write/validation) are specified over `symbolRef`/`sourceSpan`/revision grammar with the write engine routed through the durable effect boundary (#79); tree-sitter stays internal to the index layer (#96–#99). **Managed by Prolog:** `research/spec-plan-refinement-kb.pl` (+ persisted state) drove this refinement — 23 tasks, dependency graph, decisions, evidence; all `done`. `scripts/spec_plan_authority_check.{pl,sh}` is a deterministic design gate (schema shapes, example spec/plan, diagnostics vocabulary, slice graph, KB state): **ALL CHECKS PASSED**. **Evidence at this head:** full deterministic suite **1061/1061** (90 suites), benchmark deterministic **16/16**, check_runtime/load_all/CLI demo/`make research-approval`/`git diff --check` green. **Non-goals honored:** no runtime/API changes in this PR; implementation is deferred to slices S1–S10 (dependency graph in §23 of the design record). The roadmap now points at the refinement record as the TaskIR/Phase-2/3 design input.
nsaspy closed this pull request 2026-09-04 22:55:45 +00:00
Some checks failed
Tree-sitter FFI / Direct SWI-Prolog Tree-sitter FFI (pull_request) Successful in 3m24s
CI / REAL OpenRouter integration (pull_request) Has been skipped
Nix flake / Flake package and clean runtime load (pull_request) Failing after 7s
Clean SWI pack install / Install and load copied pack (pull_request) Successful in 1m55s
Paid OpenRouter / Pinned paid OpenRouter integration (pull_request) Failing after 1m50s
CI / Deterministic unit and load checks (pull_request) Successful in 3m45s

Pull request closed

Sign in to join this conversation.
No description provided.