[P1] Add proof-carrying child results and host-controlled verifier gates

lost-rob0t commented

2026-08-16 05:06:18 +00:00

(Migrated from github.com)

Goal

Make supervised/recursive agent completion distinct from result acceptance.

A child agent may finish successfully, but its result must be rejectable when required evidence is missing, stale, untrusted, or fails a host-required verifier.

This implements the first bounded slice from RLM-RESEARCH-010-logic-native-control-plane.org.

Required result contract

Add a reusable typed result envelope equivalent in semantics to:

rrlm_result{
    task:Task,
    status:Status,
    value:Value,
    claims:Claims,
    evidence:EvidenceRefs,
    provenance:Provenance,
    verification:Verification,
    usage:Usage,
    trace_ref:TraceRef
}.

Exact names may follow existing module conventions.

This is not chain-of-thought storage. Evidence consists of explicit runtime artifacts such as source/artifact refs, hashes, tests, solver outcomes, derivation refs, structured tool observations, and verifier reports.

Acceptance boundary

Provide a deterministic acceptance operation equivalent to:

accept_result(Result, Policy, Outcome).

The acceptance gate must be able to require:

valid typed result structure;
required claim/evidence relationships;
evidence references that resolve through the existing artifact/context layer where applicable;
provenance class sufficient for the requested policy;
required verifier success;
complete usage/trace linkage;
no authority/capability widening across delegation.

Child completion and parent acceptance must be separate traceable events.

Evidence/provenance rule

A successful Prolog derivation does not automatically make model-authored premises trusted facts.

The implementation needs a minimal provenance/evidence distinction sufficient to prevent proof laundering. At minimum preserve the difference between:

trusted deterministic/runtime assertion;
externally observed source/tool evidence;
model-generated/extracted claim;
derived claim;
unresolved/conflicting/unsupported claim where applicable.

Do not build a giant ontology in this slice. Keep the representation minimal and explicit.

Host-controlled verifier policy

Trusted host/runtime code may declare required verifier(s) for a task/result class.

The model may propose additional verification, but it must not be able to:

remove a host-required verifier;
redefine the predicate that accepts its own output;
turn verifier timeout/crash into success;
satisfy an observed-evidence requirement with an unverified model assertion.

Verifier outcomes must distinguish at least:

passed;
failed;
error(...);
timeout(...).

Recursive delegation

Verifier/evidence requirements are narrowing-only across child delegation. A child may receive stricter requirements than its parent, never weaker requirements than the parent/host requires for the returned result.

Compose with existing capability narrowing and the authority design in #53.

Integration

Reuse existing runtime pieces instead of creating parallel systems:

rlm_agent supervision/lifecycle;
rlm_artifact immutable refs and provenance;
rlm_graph trace/checkpoint state where useful;
rlm_completion usage and trajectory data;
#53 host authority/approval;
#54 async task/future contract.

Do not require every public completion API to adopt the result envelope in the first patch. Integrate first at the supervised-child/result-acceptance boundary, then widen only with tests.

Acceptance criteria

Define a typed proof/evidence result envelope.
Add deterministic schema validation.
Add separate result acceptance predicate/API.
Existing evidence/artifact refs can be resolved and validated.
Missing required evidence rejects structurally.
Model-authored claims cannot satisfy a policy requiring trusted/observed evidence without appropriate evidence refs.
Host-required verifiers cannot be waived by model output.
Verifier pass/fail/error/timeout remain distinct outcomes.
Child completion and parent acceptance appear separately in trace data.
Recursive children inherit equal-or-stricter evidence/verifier policy.
Result acceptance does not require or persist private chain-of-thought.
Tests cover valid acceptance, missing evidence, stale/missing refs, proof laundering attempt, verifier fail/error/timeout, and attempted policy weakening.

Non-goals

No arbitrary model-writable Prolog database.
No unrestricted call/1 verifier supplied by model output.
No replacement of #53 authority/approval semantics.
No requirement to formalize every natural-language artifact as Prolog facts.
No claim that a valid proof makes untrusted premises true.

Research

research/RLM-RESEARCH-010-logic-native-control-plane.org

## Goal Make supervised/recursive agent completion distinct from **result acceptance**. A child agent may finish successfully, but its result must be rejectable when required evidence is missing, stale, untrusted, or fails a host-required verifier. This implements the first bounded slice from `RLM-RESEARCH-010-logic-native-control-plane.org`. ## Required result contract Add a reusable typed result envelope equivalent in semantics to: ```prolog rrlm_result{ task:Task, status:Status, value:Value, claims:Claims, evidence:EvidenceRefs, provenance:Provenance, verification:Verification, usage:Usage, trace_ref:TraceRef }. ``` Exact names may follow existing module conventions. This is not chain-of-thought storage. Evidence consists of explicit runtime artifacts such as source/artifact refs, hashes, tests, solver outcomes, derivation refs, structured tool observations, and verifier reports. ## Acceptance boundary Provide a deterministic acceptance operation equivalent to: ```prolog accept_result(Result, Policy, Outcome). ``` The acceptance gate must be able to require: - valid typed result structure; - required claim/evidence relationships; - evidence references that resolve through the existing artifact/context layer where applicable; - provenance class sufficient for the requested policy; - required verifier success; - complete usage/trace linkage; - no authority/capability widening across delegation. Child completion and parent acceptance must be separate traceable events. ## Evidence/provenance rule A successful Prolog derivation does **not** automatically make model-authored premises trusted facts. The implementation needs a minimal provenance/evidence distinction sufficient to prevent proof laundering. At minimum preserve the difference between: - trusted deterministic/runtime assertion; - externally observed source/tool evidence; - model-generated/extracted claim; - derived claim; - unresolved/conflicting/unsupported claim where applicable. Do not build a giant ontology in this slice. Keep the representation minimal and explicit. ## Host-controlled verifier policy Trusted host/runtime code may declare required verifier(s) for a task/result class. The model may propose additional verification, but it must not be able to: - remove a host-required verifier; - redefine the predicate that accepts its own output; - turn verifier timeout/crash into success; - satisfy an observed-evidence requirement with an unverified model assertion. Verifier outcomes must distinguish at least: - `passed`; - `failed`; - `error(...)`; - `timeout(...)`. ## Recursive delegation Verifier/evidence requirements are narrowing-only across child delegation. A child may receive stricter requirements than its parent, never weaker requirements than the parent/host requires for the returned result. Compose with existing capability narrowing and the authority design in #53. ## Integration Reuse existing runtime pieces instead of creating parallel systems: - `rlm_agent` supervision/lifecycle; - `rlm_artifact` immutable refs and provenance; - `rlm_graph` trace/checkpoint state where useful; - `rlm_completion` usage and trajectory data; - #53 host authority/approval; - #54 async task/future contract. Do not require every public completion API to adopt the result envelope in the first patch. Integrate first at the supervised-child/result-acceptance boundary, then widen only with tests. ## Acceptance criteria - [ ] Define a typed proof/evidence result envelope. - [ ] Add deterministic schema validation. - [ ] Add separate result acceptance predicate/API. - [ ] Existing evidence/artifact refs can be resolved and validated. - [ ] Missing required evidence rejects structurally. - [ ] Model-authored claims cannot satisfy a policy requiring trusted/observed evidence without appropriate evidence refs. - [ ] Host-required verifiers cannot be waived by model output. - [ ] Verifier pass/fail/error/timeout remain distinct outcomes. - [ ] Child completion and parent acceptance appear separately in trace data. - [ ] Recursive children inherit equal-or-stricter evidence/verifier policy. - [ ] Result acceptance does not require or persist private chain-of-thought. - [ ] Tests cover valid acceptance, missing evidence, stale/missing refs, proof laundering attempt, verifier fail/error/timeout, and attempted policy weakening. ## Non-goals - No arbitrary model-writable Prolog database. - No unrestricted `call/1` verifier supplied by model output. - No replacement of #53 authority/approval semantics. - No requirement to formalize every natural-language artifact as Prolog facts. - No claim that a valid proof makes untrusted premises true. ## Research `research/RLM-RESEARCH-010-logic-native-control-plane.org`

lost-rob0t commented

2026-08-18 07:15:23 +00:00

(Migrated from github.com)

Spec/Verify foundation is implemented in draft PR #92. It introduces a shared structured evidence/provenance policy substrate, trusted versioned assertion evaluators/collectors, explicit non-boolean verification states, and host-policy narrowing that model-authored Specs cannot weaken.

#56 remains open. The broader result-envelope / accept_result(...) / child-result delegation work should consume these shared evidence/verifier primitives rather than adding a second incompatible verifier stack.

Spec/Verify foundation is implemented in draft PR #92. It introduces a shared structured evidence/provenance policy substrate, trusted versioned assertion evaluators/collectors, explicit non-boolean verification states, and host-policy narrowing that model-authored Specs cannot weaken. #56 remains open. The broader result-envelope / `accept_result(...)` / child-result delegation work should consume these shared evidence/verifier primitives rather than adding a second incompatible verifier stack.

lost-rob0t commented

2026-08-26 17:55:09 +00:00

(Migrated from github.com)

RAGE slice started from exact canonical main 267697bef10a3fffff7c093e1435ece770e7444b on branch rage/56-result-acceptance. No competing #56 branch/PR or downstream a0-symbolics/agentProlog ownership was found; merged #92 is the required evidence/Spec/Verify substrate and is reused here.

TDD-first commit a8beb5048e14a661d16610d4c30b66738d457312 defined the first reusable child-result acceptance contract before production code. No PR/CI was opened on the test-only head, so the repository gate was not intentionally left red.

Analyze/design: child completion and parent acceptance stay distinct. The result envelope is closed data. Artifact existence/freshness is resolved through canonical rlm_artifact; provenance/trust policy is checked through canonical rlm_evidence; required verifier outcomes are supplied as a separate trusted host context. The child envelope's own verification field is inert proposal metadata and cannot satisfy a host-required verifier. Policy narrowing uses evidence_policy_narrow/3, monotonic booleans, and unioned required-verifier sets.

Adversarial review of the first realization found three real bugs before promotion: non-completed children could still reach accepted state, claim-local evidence refs were not required to be declared/resolved by the result envelope, and duplicate IDs could fail nondeterministically instead of returning a structured error. Those findings were pinned in tests before the hardened realization. A further interface review preserved typed ground artifact refs instead of generic closed-data retagging, so refs retain reusable identity while arbitrary payloads remain canonical closed data.

Current realization head is 60bb1effb46abedf7ac23cc544ac6ba63c1a5f08. The deterministic contract now covers valid acceptance, non-completed rejection, missing claim evidence, undeclared claim refs, stale/missing artifact refs, model-claim proof laundering against observed-evidence policy, child-proposed verifier laundering, distinct verifier fail/error/timeout states, monotonic policy narrowing, duplicate claim IDs, and nonground result rejection. The production module is in test/load_all.pl, and the suite is registered in the authoritative deterministic corpus.

Decision gate before CI: GO to verification, not GO to merge. This is intentionally only the first #56 slice: typed envelope + deterministic acceptance gate. Separate acceptance trace events and deeper supervised-child integration remain follow-up scope. docs/result-acceptance.md records the public/security boundary.

Next step is exact-head repository-native verification. Any changed head invalidates prior evidence; if the gate finds a semantic defect, preserve it and repair rather than weakening the contract.

RAGE slice started from exact canonical `main` `267697bef10a3fffff7c093e1435ece770e7444b` on branch `rage/56-result-acceptance`. No competing #56 branch/PR or downstream `a0-symbolics`/`agentProlog` ownership was found; merged #92 is the required evidence/Spec/Verify substrate and is reused here. TDD-first commit `a8beb5048e14a661d16610d4c30b66738d457312` defined the first reusable child-result acceptance contract before production code. No PR/CI was opened on the test-only head, so the repository gate was not intentionally left red. Analyze/design: child completion and parent acceptance stay distinct. The result envelope is closed data. Artifact existence/freshness is resolved through canonical `rlm_artifact`; provenance/trust policy is checked through canonical `rlm_evidence`; required verifier outcomes are supplied as a separate trusted host context. The child envelope's own `verification` field is inert proposal metadata and cannot satisfy a host-required verifier. Policy narrowing uses `evidence_policy_narrow/3`, monotonic booleans, and unioned required-verifier sets. Adversarial review of the first realization found three real bugs before promotion: non-completed children could still reach accepted state, claim-local evidence refs were not required to be declared/resolved by the result envelope, and duplicate IDs could fail nondeterministically instead of returning a structured error. Those findings were pinned in tests before the hardened realization. A further interface review preserved typed ground artifact refs instead of generic closed-data retagging, so refs retain reusable identity while arbitrary payloads remain canonical closed data. Current realization head is `60bb1effb46abedf7ac23cc544ac6ba63c1a5f08`. The deterministic contract now covers valid acceptance, non-completed rejection, missing claim evidence, undeclared claim refs, stale/missing artifact refs, model-claim proof laundering against observed-evidence policy, child-proposed verifier laundering, distinct verifier fail/error/timeout states, monotonic policy narrowing, duplicate claim IDs, and nonground result rejection. The production module is in `test/load_all.pl`, and the suite is registered in the authoritative deterministic corpus. Decision gate before CI: **GO to verification, not GO to merge**. This is intentionally only the first #56 slice: typed envelope + deterministic acceptance gate. Separate acceptance trace events and deeper supervised-child integration remain follow-up scope. `docs/result-acceptance.md` records the public/security boundary. Next step is exact-head repository-native verification. Any changed head invalidates prior evidence; if the gate finds a semantic defect, preserve it and repair rather than weakening the contract.

lost-rob0t commented

2026-08-26 17:59:14 +00:00

(Migrated from github.com)

Exact-head verification complete for first #56 slice at 60bb1effb46abedf7ac23cc544ac6ba63c1a5f08.

Repository-native gate is fully green on the synthetic merge of this exact head into unchanged canonical main 267697bef10a3fffff7c093e1435ece770e7444b:

deterministic PlUnit: 79 suites / 899 discovered / 899 planned / 899 completed / 899 passed / 0 failed / 0 timeout / 0 blocked / 0 fixme;
deterministic benchmark/conformance: 16/16 pass;
deterministic deep recursion: 15/15 pass;
CLI/trace, graph restart, artifact restart, whitespace: pass;
credential-backed REAL OpenRouter: core, structured repair, benchmark, depth 0/1/2 and CLI smoke all pass;
pinned Paid OpenRouter: pass;
Nix flake: pass;
clean SWI pack install: pass;
Tree-sitter FFI: pass.

PR #255 is mergeable; no submitted reviews, conversation comments or unresolved review threads exist. Adversarial decision remains GO for this bounded API slice.

#56 remains open intentionally. This PR establishes the typed result envelope, artifact/evidence validation, host-controlled verifier gate, proof-laundering defenses and monotonic policy narrowing. Remaining epic scope includes separate child-completion/result-acceptance trace events and canonical supervised-child integration/correlation. Merge remains subject to the repository's explicit merge-on-green authorization gate.

Exact-head verification complete for first #56 slice at `60bb1effb46abedf7ac23cc544ac6ba63c1a5f08`. Repository-native gate is fully green on the synthetic merge of this exact head into unchanged canonical `main` `267697bef10a3fffff7c093e1435ece770e7444b`: - deterministic PlUnit: **79 suites / 899 discovered / 899 planned / 899 completed / 899 passed / 0 failed / 0 timeout / 0 blocked / 0 fixme**; - deterministic benchmark/conformance: 16/16 pass; - deterministic deep recursion: 15/15 pass; - CLI/trace, graph restart, artifact restart, whitespace: pass; - credential-backed REAL OpenRouter: core, structured repair, benchmark, depth 0/1/2 and CLI smoke all pass; - pinned Paid OpenRouter: pass; - Nix flake: pass; - clean SWI pack install: pass; - Tree-sitter FFI: pass. PR #255 is mergeable; no submitted reviews, conversation comments or unresolved review threads exist. Adversarial decision remains **GO for this bounded API slice**. #56 remains open intentionally. This PR establishes the typed result envelope, artifact/evidence validation, host-controlled verifier gate, proof-laundering defenses and monotonic policy narrowing. Remaining epic scope includes separate child-completion/result-acceptance trace events and canonical supervised-child integration/correlation. Merge remains subject to the repository's explicit merge-on-green authorization gate.