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

New issue

Closed

opened 2026-09-10 21:18:02 +00:00 by nsaspy · 1 comment

nsaspy commented

2026-09-10 21:18:02 +00:00

Owner

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`

nsaspy commented

2026-09-10 21:23:27 +00:00

Author

Owner

Duplicate of #56 (pre-existing Forgejo mirror with GitHub number parity). Closing this accidental duplicate created by today's open-state sync; #56 stays canonical on Forgejo.

nsaspy closed this issue

2026-09-10 21:23:28 +00:00