Route effectful canonical tools through #57 effect boundary (#79 slice 1) #86

Merged
lost-rob0t merged 2 commits from 79-tool-effect-boundary into main 2026-08-19 04:19:42 +00:00
lost-rob0t commented 2026-08-18 02:43:22 +00:00 (Migrated from github.com)

Summary

Slice 1 of #79. Effectful rlm_tool execution crosses the #57 durable effect identity / observation boundary before the handler mutation, with the reviewed authority/identity defects hardened.

Canonical path implemented

normalize executable operation (schema + preflight)
-> capability / hard-policy / confinement
-> rlm_effect_executor:effect_prepare(rlm_tool, tool, Request, Options, execute(Ticket A))
-> #53 authority fingerprints Ticket A
-> authorized continuation carries ground Ticket A
-> rlm_effect_executor:effect_execute_prepared(rlm_tool, Ticket A, Authority, Outcome)
-> validate/admit SAME Ticket A under the #57 execution lease
-> durable dispatch
-> effect_adapter_submit(rlm_tool, Attempt, Request, Outcome)
-> perform_tool_effect (trusted tool handler boundary)
-> authoritative observation OR conservative uncertainty

There is no second preparation after authority. A stale store namespace, execution epoch, call identity, executable fingerprint, attempt identity, mode, or parent lineage fails closed through the existing #57 ticket validation contract; authority over Ticket A is never permission to silently prepare Ticket B.

Trusted tool executor identity

Effectful tool executable semantics now include a stable code-owned executor identity digest derived from the trusted preflight/handler predicate entrypoints, plus the trusted effect class and effective execution limits. The digest is separate from:

  • the model-facing tool name;
  • adapter identity rlm_tool;
  • ephemeral registry_N allocation;
  • effect metadata.

The callable itself is not persisted or exposed to the model. The live registry handle remains metadata only for dispatch lookup.

Authority / edit invariants

  • #53 modes unchanged: approve_diff, allow_once, allow_session, dangerous.
  • Exact ticket: approved effectful continuations carry the prepared ground ticket directly.
  • Edited pending proposals: edited payload -> normalize -> preflight -> prepare NEW ticket -> compose NEW authority operation -> continuation carries NEW ticket. The old ticket is not an executable fallback.
  • #54 direction preserved: approval continuation calls the trusted prepared-ticket executor directly; it does not start a nested async path.
  • Fresh reads preserved: effect:read tools retain the direct fresh-read path and are not memoized through #57.
  • No second ledger / scheduler: admission, dispatch, observation, reconciliation, uncertainty, and cancellation remain in the existing #57 executor.

Result-contract corrections

  • missing effect store still maps to public effect_store_required, preserving store_not_open as the cause;
  • non-store preparation failures preserve their structured #57 error kind instead of being mislabeled effect_store_required;
  • effect replay trace fingerprint remains scalar and uses none when no authoritative fingerprint is available, never an observation dict.

Tests

The original nine PR #86 behavioral/crash tests remain in test/rlm_tool_effect_test.pl and its fresh-process fixtures. Added adversarial coverage proves:

  1. authority over pending Ticket A cannot execute a fresh epoch after another execution is observed and the logical call is pruned/advanced; external mutation count remains 1;
  2. two materially different trusted bindings with identical tool name/args/preflight details/effect class have different durable executable identity and execute independently;
  3. two separately allocated registries using the same trusted binding retain the same durable effect identity, proving registry_N allocation is not semantic identity;
  4. missing store classification remains effect_store_required with store_not_open cause;
  5. non-store preparation causes such as lifecycle conflict, migration fence, and invalid effect state retain their actual kinds;
  6. replay trace fingerprint remains the established scalar shape (none on replay) and external mutation count remains 1.

Mutation-count assertions use fixture state independent from the effect ledger. The stale-ticket race uses deterministic state/epoch advancement, not sleeps.

Documentation

docs/effect-adapters.md now documents the prepared-ticket executor ABI, literal Ticket-A authority/admission invariant, stale-ticket failure behavior, stable trusted tool executor identity, edit behavior, and the distinction between semantic identity, adapter identity, ephemeral registry identity, model-facing names, and metadata.

Non-goals

No Slice 2+ work is included:

  • provider request adoption;
  • effectful MCP request adoption;
  • MCP lifecycle adoption;
  • external tool-pack lifecycle work.

#79 and #57 remain open. This PR does not claim #79 complete.

Verification

The branch is pushed and exact-head GitHub CI is the source of truth for final verification. Do not treat the prior head's deterministic or REAL OpenRouter result as verification of the hardened head.

Exact commands required by this slice:

swipl -q -s test/check_runtime.pl
swipl -q -s test/load_all.pl
swipl -q -s test/run_tests.pl
swipl -q -s benchmark/run.pl -- deterministic
swipl -q -s benchmark/run.pl -- deep-experiment
swipl -q -s bin/prolog-rlm.pl -- demo --json
git diff --check

REAL OpenRouter is only considered passed when the GitHub Actions job on the final exact head completes successfully.

Regression audit

Boundary Classification
perform_tool_effect (effectful tools) #57 gated through exact prepared ticket
perform_tool_effect (read tools) read-only, intentionally fresh-read
provider dispatch (model_complete / http_post) out of #79 Slice 1 scope
mcp_transport_exchange out of #79 Slice 1 scope
MCP install/run/start/stop/restart out of #79 Slice 1 scope

No unrelated cleanup.

## Summary Slice 1 of #79. Effectful `rlm_tool` execution crosses the #57 durable effect identity / observation boundary before the handler mutation, with the reviewed authority/identity defects hardened. ## Canonical path implemented ```text normalize executable operation (schema + preflight) -> capability / hard-policy / confinement -> rlm_effect_executor:effect_prepare(rlm_tool, tool, Request, Options, execute(Ticket A)) -> #53 authority fingerprints Ticket A -> authorized continuation carries ground Ticket A -> rlm_effect_executor:effect_execute_prepared(rlm_tool, Ticket A, Authority, Outcome) -> validate/admit SAME Ticket A under the #57 execution lease -> durable dispatch -> effect_adapter_submit(rlm_tool, Attempt, Request, Outcome) -> perform_tool_effect (trusted tool handler boundary) -> authoritative observation OR conservative uncertainty ``` There is no second preparation after authority. A stale store namespace, execution epoch, call identity, executable fingerprint, attempt identity, mode, or parent lineage fails closed through the existing #57 ticket validation contract; authority over Ticket A is never permission to silently prepare Ticket B. ## Trusted tool executor identity Effectful tool executable semantics now include a stable code-owned executor identity digest derived from the trusted preflight/handler predicate entrypoints, plus the trusted effect class and effective execution limits. The digest is separate from: - the model-facing tool name; - adapter identity `rlm_tool`; - ephemeral `registry_N` allocation; - effect metadata. The callable itself is not persisted or exposed to the model. The live registry handle remains metadata only for dispatch lookup. ## Authority / edit invariants - **#53 modes unchanged:** `approve_diff`, `allow_once`, `allow_session`, `dangerous`. - **Exact ticket:** approved effectful continuations carry the prepared ground ticket directly. - **Edited pending proposals:** edited payload -> normalize -> preflight -> prepare NEW ticket -> compose NEW authority operation -> continuation carries NEW ticket. The old ticket is not an executable fallback. - **#54 direction preserved:** approval continuation calls the trusted prepared-ticket executor directly; it does not start a nested async path. - **Fresh reads preserved:** `effect:read` tools retain the direct fresh-read path and are not memoized through #57. - **No second ledger / scheduler:** admission, dispatch, observation, reconciliation, uncertainty, and cancellation remain in the existing #57 executor. ## Result-contract corrections - missing effect store still maps to public `effect_store_required`, preserving `store_not_open` as the cause; - non-store preparation failures preserve their structured #57 error kind instead of being mislabeled `effect_store_required`; - effect replay trace `fingerprint` remains scalar and uses `none` when no authoritative fingerprint is available, never an observation dict. ## Tests The original nine PR #86 behavioral/crash tests remain in `test/rlm_tool_effect_test.pl` and its fresh-process fixtures. Added adversarial coverage proves: 10. authority over pending Ticket A cannot execute a fresh epoch after another execution is observed and the logical call is pruned/advanced; external mutation count remains 1; 11. two materially different trusted bindings with identical tool name/args/preflight details/effect class have different durable executable identity and execute independently; 12. two separately allocated registries using the same trusted binding retain the same durable effect identity, proving `registry_N` allocation is not semantic identity; 13. missing store classification remains `effect_store_required` with `store_not_open` cause; 14. non-store preparation causes such as lifecycle conflict, migration fence, and invalid effect state retain their actual kinds; 15. replay trace fingerprint remains the established scalar shape (`none` on replay) and external mutation count remains 1. Mutation-count assertions use fixture state independent from the effect ledger. The stale-ticket race uses deterministic state/epoch advancement, not sleeps. ## Documentation `docs/effect-adapters.md` now documents the prepared-ticket executor ABI, literal Ticket-A authority/admission invariant, stale-ticket failure behavior, stable trusted tool executor identity, edit behavior, and the distinction between semantic identity, adapter identity, ephemeral registry identity, model-facing names, and metadata. ## Non-goals No Slice 2+ work is included: - provider request adoption; - effectful MCP request adoption; - MCP lifecycle adoption; - external tool-pack lifecycle work. #79 and #57 remain open. This PR does **not** claim #79 complete. ## Verification The branch is pushed and exact-head GitHub CI is the source of truth for final verification. Do not treat the prior head's deterministic or REAL OpenRouter result as verification of the hardened head. Exact commands required by this slice: ```sh swipl -q -s test/check_runtime.pl swipl -q -s test/load_all.pl swipl -q -s test/run_tests.pl swipl -q -s benchmark/run.pl -- deterministic swipl -q -s benchmark/run.pl -- deep-experiment swipl -q -s bin/prolog-rlm.pl -- demo --json git diff --check ``` REAL OpenRouter is only considered passed when the GitHub Actions job on the final exact head completes successfully. ## Regression audit | Boundary | Classification | |---|---| | `perform_tool_effect` (effectful tools) | #57 gated through exact prepared ticket | | `perform_tool_effect` (read tools) | read-only, intentionally fresh-read | | provider dispatch (`model_complete` / `http_post`) | out of #79 Slice 1 scope | | `mcp_transport_exchange` | out of #79 Slice 1 scope | | MCP install/run/start/stop/restart | out of #79 Slice 1 scope | No unrelated cleanup.
Sign in to join this conversation.
No description provided.