fix(proxy): never inject a cross-account previous_response_id anchor (takeover of #1274) - #1638
Open
Komzpa wants to merge 6 commits into
Open
fix(proxy): never inject a cross-account previous_response_id anchor (takeover of #1274)#1638Komzpa wants to merge 6 commits into
Komzpa wants to merge 6 commits into
Conversation
Komzpa
pushed a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
Komzpa
added a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
The HTTP-bridge compact-anchor optimization injects `previous_response_id = session.last_completed_response_id` and trims the stored history prefix. A `previous_response_id` is account-scoped upstream: only the account that created a response can resume it. The injection had no ownership check, so when a Codex session failed over to a different account (durable owner unavailable, or a durable record restored onto a session bound to another account) the anchor pointed at a response the serving account never created. Upstream accepted the `response.create` but never emitted `response.created`, and with the history trimmed away there was no fallback — the per-bridge `response_create_gate` (`Semaphore(1)`) wedged. The holder's client saw "idle timeout waiting for SSE"; queued requests saw "temporarily overloaded". Track the owning account of `last_completed_response_id` (`last_completed_response_account_id`), set in lockstep at both setters — the real `response.completed` path records the session's current account, the durable restore records the durable owner account — and gate the session-level anchor injection on owner == serving account. On mismatch, fall through to a full-history resend (correct output, more tokens), never a cross-account anchor. Regression tests: anchor injected when same-account; anchor skipped + full history resent after cross-account failover. OpenSpec: fix-cross-account-previous-response-anchor (sticky-session-operations).
The session-level compact anchor was not the only injection site that runs after the serving account is bound. When an owner forward fails, the local recovery path rebinds with allow_previous_response_recovery_rebind / allow_bootstrap_owner_rebind, which are explicitly allowed to bind the session to an account other than the durable record's owner, and then injects durable_lookup.latest_response_id into the recovery payload with the stored prefix trimmed away. That is the same wedge: upstream accepts the response.create, never emits response.created, and the per-bridge response_create_gate stays held. Gate that injection on durable_lookup.account_id == session.account.id and keep the full input on a mismatch. Both declines now emit a cross_account_anchor_declined bridge event naming the injection site and the anchor's owning account, so the wedge family stays visible in bridge logs. The remaining proxy-side site, the pre-binding fresh-reattach durable anchor, is already covered: setting previous_response_id there makes the durable owner a required account, so both session creation and session reuse refuse to serve it elsewhere and an unavailable owner degrades along the account-neutral full-resend path instead. Tests: same-account recovery still anchors, cross-account recovery keeps the full input. The owner-unavailable fake now honours preferred_account_id when it builds the recovery session, matching what the real creation path pins.
…l bridge The unit coverage stubs _get_or_create_http_bridge_session and _submit_http_bridge_request, so it never sends a frame upstream, waits for response.created, or touches the response-create gate: it would still pass if the real bridge path stayed wedged. Add bridge-level coverage that runs the real path. A durable record owned by a paused account is restored onto a session created on another account, and the fake upstream models the account scope of previous_response_id: a response.create carrying an anchor it never issued is accepted and then answered with silence, exactly like upstream. With the guard the turn goes upstream as a full-history resend and settles; without it the request never completes and the run fails on the 5s POST timeout with the gate still held. The same test then proves same-account continuity is untouched: once the durable record names the account that created the response, the next turn reuses the session and anchors on it instead of resending the history.
Komzpa
force-pushed
the
pr1274-rebased-20260806
branch
from
August 6, 2026 23:01
70f686f to
02b3c12
Compare
Komzpa
added a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Takeover of #1274 by @aididhaiqal — the original three commits are carried with authorship intact; two additions on top. The original diagnosis was exactly right and turned out to be the root cause of the bridge-wedge family we have been mitigating from the other end all day (#1580 detection, #1630 quarantine): an injected
previous_response_idbelonging to a different account is accepted by upstream, which then never emitsresponse.created, and the client waits forever.What this adds over #1274 as-is:
mixin.py; main's newer try/abort structure kept verbatim).allow_previous_response_recovery_rebind/allow_bootstrap_owner_rebind) could legally land on a non-owner account and then injected the durable anchor — same wedge, different door. Now gated the same way.previous_response_id(accepts the alien anchor, answers with silence). Removing the guard reproduces the production wedge (5s POST timeout, gate held); keeping it settles via full-history resend, and a follow-up turn proves same-account continuity still anchors.cross_account_anchor_declinedwith site + owning account — a concrete key for the Keep HTTP bridge missing-created watchdog armed after prelude #1580/fix(proxy): quarantine silent HTTP bridge sessions (takeover of #1405) #1630 detection path.fresh_reattach_anchor_injectedsite is documented as safe-by-construction (injection there makes the durable owner a required account) rather than double-guarded.Verification: bridge suites 604 passed; full unit suite 5681 passed / 3 skipped; ruff + format clean;
openspec validate fix-cross-account-previous-response-anchor --strictgreen.Happy to fold this back into #1274's branch instead if @aididhaiqal prefers to land it under the original PR.