[P0] Harden #57 post-merge retention, adapter identity, and terminal resolution invariants #80

Closed
opened 2026-08-17 19:53:50 +00:00 by lost-rob0t · 0 comments
lost-rob0t commented 2026-08-17 19:53:50 +00:00 (Migrated from github.com)

Discovered by

Post-merge adversarial review of PR #78 / main at 7af5d5f6dc833c70bd547571654485eb73a1a704.

This is a substrate hardening issue. It does not implement #79 canonical provider/tool/MCP adoption.

1. Prune is not linearizable with admission/dispatch

rlm_effect_prune/2 currently reads attempts and later deletes the call without holding the rlm_effect_state mutex used by admission/dispatch/observation transitions.

A stale interleaving can therefore be:

pruner reads: all attempts terminal
-> retry/resample ticket is admitted
-> attempt becomes dispatching / adapter may cross boundary
-> stale pruner deletes call + active attempt + observation/event state

Additionally, rlm_effect_admit/3 and rlm_effect_cancel_ticket/3 validate a ticket before entering the effect-state mutex. If pruning removes the call between validation and claim, the old code can create an orphan attempt against a call that no longer exists.

Required fix

  • serialize prune check + delete under the same effect-state critical section;
  • validate/revalidate tickets inside the atomic admission and pre-claim cancellation critical sections;
  • add deterministic tests for the post-validation/prune interleaving, without sleeps.

2. Adapter identity is not part of executable identity

effect_execute(Adapter, Kind, Request, Options, ...) chooses the code that crosses the external boundary, but rlm_effect_prepare/4 hashes only Kind + Request + Semantics.

Therefore the same request can be submitted with adapter A and later invoked/reconciled with adapter B while sharing one durable attempt unless every caller manually encodes adapter identity into the request. The generic executor does not enforce this and the docs do not require it.

Required fix

  • bind the code-owned adapter identity into executor-side semantics before fingerprint/call/attempt derivation;
  • persist enough trusted adapter identity with the attempt to verify fresh-process reconciliation uses the same adapter;
  • wrong-adapter reconciliation must fail closed without invoking the adapter;
  • provide an executor preparation helper suitable for #53 authority construction so authority and execution use the exact same adapter-bound ticket.

3. abandoned indeterminate attempts are still accepted as retry/resample parents

The state machine distinguishes trusted resolutions:

indeterminate -> retry_authorized
indeterminate -> abandoned

but allowed_explicit_parent_status/2 currently accepts abandoned as an explicit retry/resample parent. This defeats the semantic distinction between authorizing a risky retry and abandoning the uncertain operation.

Required fix

An abandoned attempt must not become an explicit retry/resample parent. Only retry_authorized should unlock retry after an indeterminate remote outcome.

4. Explicit reconciliation can downgrade an already-authoritative local observation

effect_reconcile/3 always calls the reconciliation adapter after rlm_effect_status/2, including when the attempt is already observed. If the remote reconciliation is unavailable or returns uncertainty, the public result can become indeterminate even though an immutable local authoritative observation already exists.

Required fix

  • observed attempts replay the local observation and do not call remote reconciliation;
  • reconciliation recording conflicts/errors return structured outcomes rather than predicate failure;
  • tests prove an already-observed attempt cannot be downgraded by explicit reconciliation.

Acceptance

  • prune check/delete is linearizable with admission, dispatch, observation, cancellation, and indeterminate resolution;
  • stale post-validation tickets cannot create orphan attempts after pruning;
  • adapter identity participates in executor effect identity and wrong-adapter reconciliation fails closed;
  • abandoned cannot be retried/resampled;
  • observed reconciliation is local replay and cannot become indeterminate;
  • deterministic adversarial tests cover each interleaving/terminal invariant;
  • canonical deterministic CI and configured REAL OpenRouter gates are green;
  • #57 remains open and #79 remains the separate adoption slice.

Refs #57 #79 #53 #54

## Discovered by Post-merge adversarial review of PR #78 / `main` at `7af5d5f6dc833c70bd547571654485eb73a1a704`. This is a substrate hardening issue. It does **not** implement #79 canonical provider/tool/MCP adoption. ## 1. Prune is not linearizable with admission/dispatch `rlm_effect_prune/2` currently reads attempts and later deletes the call without holding the `rlm_effect_state` mutex used by admission/dispatch/observation transitions. A stale interleaving can therefore be: ```text pruner reads: all attempts terminal -> retry/resample ticket is admitted -> attempt becomes dispatching / adapter may cross boundary -> stale pruner deletes call + active attempt + observation/event state ``` Additionally, `rlm_effect_admit/3` and `rlm_effect_cancel_ticket/3` validate a ticket before entering the effect-state mutex. If pruning removes the call between validation and claim, the old code can create an orphan attempt against a call that no longer exists. ### Required fix - serialize prune check + delete under the same effect-state critical section; - validate/revalidate tickets inside the atomic admission and pre-claim cancellation critical sections; - add deterministic tests for the post-validation/prune interleaving, without sleeps. ## 2. Adapter identity is not part of executable identity `effect_execute(Adapter, Kind, Request, Options, ...)` chooses the code that crosses the external boundary, but `rlm_effect_prepare/4` hashes only `Kind + Request + Semantics`. Therefore the same request can be submitted with adapter A and later invoked/reconciled with adapter B while sharing one durable attempt unless every caller manually encodes adapter identity into the request. The generic executor does not enforce this and the docs do not require it. ### Required fix - bind the code-owned adapter identity into executor-side semantics before fingerprint/call/attempt derivation; - persist enough trusted adapter identity with the attempt to verify fresh-process reconciliation uses the same adapter; - wrong-adapter reconciliation must fail closed without invoking the adapter; - provide an executor preparation helper suitable for #53 authority construction so authority and execution use the exact same adapter-bound ticket. ## 3. `abandoned` indeterminate attempts are still accepted as retry/resample parents The state machine distinguishes trusted resolutions: ```text indeterminate -> retry_authorized indeterminate -> abandoned ``` but `allowed_explicit_parent_status/2` currently accepts `abandoned` as an explicit retry/resample parent. This defeats the semantic distinction between authorizing a risky retry and abandoning the uncertain operation. ### Required fix An `abandoned` attempt must not become an explicit retry/resample parent. Only `retry_authorized` should unlock retry after an indeterminate remote outcome. ## 4. Explicit reconciliation can downgrade an already-authoritative local observation `effect_reconcile/3` always calls the reconciliation adapter after `rlm_effect_status/2`, including when the attempt is already `observed`. If the remote reconciliation is unavailable or returns uncertainty, the public result can become `indeterminate` even though an immutable local authoritative observation already exists. ### Required fix - observed attempts replay the local observation and do not call remote reconciliation; - reconciliation recording conflicts/errors return structured outcomes rather than predicate failure; - tests prove an already-observed attempt cannot be downgraded by explicit reconciliation. ## Acceptance - [ ] prune check/delete is linearizable with admission, dispatch, observation, cancellation, and indeterminate resolution; - [ ] stale post-validation tickets cannot create orphan attempts after pruning; - [ ] adapter identity participates in executor effect identity and wrong-adapter reconciliation fails closed; - [ ] `abandoned` cannot be retried/resampled; - [ ] observed reconciliation is local replay and cannot become indeterminate; - [ ] deterministic adversarial tests cover each interleaving/terminal invariant; - [ ] canonical deterministic CI and configured REAL OpenRouter gates are green; - [ ] #57 remains open and #79 remains the separate adoption slice. Refs #57 #79 #53 #54
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
nsaspy/prolog-rlm#80
No description provided.