Add first-class Spec and Verify foundation #92

Merged

lost-rob0t merged 1 commit from agent/spec-verify-foundation into main

2026-08-18 14:27:47 +00:00

lost-rob0t commented

2026-08-18 07:07:10 +00:00

(Migrated from github.com)

Summary

Adds the domain-neutral architectural foundation for first-class immutable Specs and independent verification.

shared structured evidence/provenance policy substrate
trusted assertion registry with sanitized discovery and separate pure evaluator / optional observer identities
Spec normalize/validate/freeze/inspect/fingerprint APIs with optional artifact publication and exact historical resolution
pure spec_verify/4 over supplied observations
separate sync/async observation collection through the existing async runtime
project-KB snapshot/state coherence boundary without implementing a parser or final ontology
optional Plan binding/execution through existing rlm_plan/rlm_outcome
bounded Plan/Execute/Observe/Verify/repair composition over existing rlm_graph
project-KB K1 -> execution -> K2 refresh boundary without teaching planner/verifier to parse source
tests for security, immutable identity, stale evidence, verifier failures/timeouts, project-KB K1/K2 behavior, non-software domains, plan-only composition, repair, and wrong-Spec restart
concise architecture/API documentation plus TODO/PrologAgent roadmap reconciliation

Architectural invariant

The Spec defines desired state. Observations describe actual state. Plans may change, observations may change, and repair may replan, but the exact frozen Spec remains fixed unless an explicit new Spec version is created.

For project/code use, parsers/indexers are future observation providers. Spec/Verify do not parse source code. Project KB state, artifacts, graph checkpoints, authority, effects, and runtime observations remain distinct semantic classes.

Public composition

The new stages are independently reusable module APIs:

Spec only: normalize -> validate -> freeze
Verify supplied observations with no collection/planning/execution
Observe -> Verify
Frozen Spec + supplied Plan
Frozen Spec + supplied Plan + existing plan executor
full bounded graph composition with optional repair

Trusted assertion registry internals remain module-scoped; model-facing discovery is sanitized rather than exposing trusted closures through the broad runtime facade.

#56 should consume the shared evidence/verifier substrate for result acceptance rather than add a second verifier stack.
#69 TaskIR should reference the exact Frozen Spec instead of owning competing acceptance criteria.
#70 project-context/parser work can populate canonical project knowledge consumed by the semantic observation boundary.
#71 continuation/resume must remain bound to the exact original Spec reference.
#68 remains open as the broader workflow epic.

None of those parent issues are closed by this substrate slice.

Verification

Exact rebased head: c280c313bec1fbc02cae62af3be9ef56c156a826

GitHub Actions CI run #870 passed both jobs on the exact head.

Deterministic lane passed:

supported SWI-Prolog runtime check
production module load
live-integration definition load
full deterministic PlUnit suite
deterministic benchmark/conformance
deep recursion experiment
credential-free CLI demo/trace smoke
persistent graph resume across fresh SWI processes
durable artifact handoff across fresh SWI processes
whitespace check

REAL OpenRouter lane passed:

core suite
structured repair suite
benchmark suite
depth 0/1/2 recursion experiment
one-command REAL RLM CLI smoke

The branch was rebased onto canonical main 591c936d0476df5ac56de31fd327e7d0d678fb4e after the concurrent symbolic prompt-compiler research commit landed.

Deliberate non-goals

This PR does not build PrologAgent, the TUI, a source parser, a final project-KB ontology, a new scheduler/executor/authority/artifact/async runtime, or a second effect ledger. It does not auto-consult or execute model-generated Prolog.

## Summary Adds the domain-neutral architectural foundation for first-class immutable Specs and independent verification. - shared structured evidence/provenance policy substrate - trusted assertion registry with sanitized discovery and separate pure evaluator / optional observer identities - Spec normalize/validate/freeze/inspect/fingerprint APIs with optional artifact publication and exact historical resolution - pure `spec_verify/4` over supplied observations - separate sync/async observation collection through the existing async runtime - project-KB snapshot/state coherence boundary without implementing a parser or final ontology - optional Plan binding/execution through existing `rlm_plan`/`rlm_outcome` - bounded Plan/Execute/Observe/Verify/repair composition over existing `rlm_graph` - project-KB K1 -> execution -> K2 refresh boundary without teaching planner/verifier to parse source - tests for security, immutable identity, stale evidence, verifier failures/timeouts, project-KB K1/K2 behavior, non-software domains, plan-only composition, repair, and wrong-Spec restart - concise architecture/API documentation plus TODO/PrologAgent roadmap reconciliation ## Architectural invariant The Spec defines desired state. Observations describe actual state. Plans may change, observations may change, and repair may replan, but the exact frozen Spec remains fixed unless an explicit new Spec version is created. For project/code use, parsers/indexers are future observation providers. Spec/Verify do not parse source code. Project KB state, artifacts, graph checkpoints, authority, effects, and runtime observations remain distinct semantic classes. ## Public composition The new stages are independently reusable module APIs: - Spec only: normalize -> validate -> freeze - Verify supplied observations with no collection/planning/execution - Observe -> Verify - Frozen Spec + supplied Plan - Frozen Spec + supplied Plan + existing plan executor - full bounded graph composition with optional repair Trusted assertion registry internals remain module-scoped; model-facing discovery is sanitized rather than exposing trusted closures through the broad runtime facade. ## Related issue direction - #56 should consume the shared evidence/verifier substrate for result acceptance rather than add a second verifier stack. - #69 TaskIR should reference the exact Frozen Spec instead of owning competing acceptance criteria. - #70 project-context/parser work can populate canonical project knowledge consumed by the semantic observation boundary. - #71 continuation/resume must remain bound to the exact original Spec reference. - #68 remains open as the broader workflow epic. None of those parent issues are closed by this substrate slice. ## Verification Exact rebased head: `c280c313bec1fbc02cae62af3be9ef56c156a826` GitHub Actions CI run #870 passed both jobs on the exact head. Deterministic lane passed: - supported SWI-Prolog runtime check - production module load - live-integration definition load - full deterministic PlUnit suite - deterministic benchmark/conformance - deep recursion experiment - credential-free CLI demo/trace smoke - persistent graph resume across fresh SWI processes - durable artifact handoff across fresh SWI processes - whitespace check REAL OpenRouter lane passed: - core suite - structured repair suite - benchmark suite - depth 0/1/2 recursion experiment - one-command REAL RLM CLI smoke The branch was rebased onto canonical `main` `591c936d0476df5ac56de31fd327e7d0d678fb4e` after the concurrent symbolic prompt-compiler research commit landed. ## Deliberate non-goals This PR does not build PrologAgent, the TUI, a source parser, a final project-KB ontology, a new scheduler/executor/authority/artifact/async runtime, or a second effect ledger. It does not auto-consult or execute model-generated Prolog.