Repository navigation
Session lease: a refusal is not a plan, so delete RefuseForeignOwner rather than answer for it - #10123
Merged
gunbai-bot[bot] merged 3 commits intoSep 3, 2026
Conversation
…rather than answer for it Two judgement-pile sites from the #10028 nested-exhaustiveness census, both in gunbc.host.host_effect_nbd_proxy_serve (host_effect_nbd_proxy_serve_apply and ..._apply_with_observation), both uncovered on `Apply { plan: RefuseForeignOwner }`. The obvious repair is an arm, and it is the wrong one. `Apply` is the decision that EXECUTES a plan, so `Apply { plan: RefuseForeignOwner }` reads "execute the refusal" -- and at a host-effect boundary an accept arm there would be fail-open, while a refuse arm would be a second place answering a question the decision already answers. WHAT THE PRODUCER ACTUALLY DOES. gunbc.session_lease decision_for_process_port_verdict is the sole producer of UpsertDecision<ProcessLeasePlan>, and it maps Conflict to `Refuse { reason: "foreign process owns port" }`. RefuseForeignOwner is constructed nowhere in the tree: grep over every file, unfiltered, finds the declaration and one prose mention in docs/plans/dispatch-maintain-cc.md, and no constructor and no pattern anywhere. So one fact -- a foreign owner holds the port, therefore refuse -- had two representations, one of them dead, and the dead one is what every consumer of the decision was being asked to answer for. So the variant is deleted. Both sites are then exhaustive with the arms they already had; no arm is authored at all, and the fan-out is zero because there was nothing to migrate. That is §4b rung 4 -- the state has no constructor -- rather than rung 2. The doc line that listed the three plans is corrected in the same commit. ENROLLED EVIDENCE, not a discarded probe. test.claim.process_lease_plan_is_not_a_refusal_witness hands two fixture sources to the compiler through gunbc.compile_diagnostic_census: w_a_refusal_cannot_be_written_as_a_lease_plan -- blocking rows > 0 w_a_real_plan_on_the_same_arm_is_admitted -- 0 Both import the real gunbc.session_lease, so re-adding the variant makes the negative go quiet and the file fail. The pair differs only in WHICH plan is written into the same `Apply`, so a green negative cannot be explained by `Apply` being unusable. SENSITIVITY, MEASURED. With RefuseForeignOwner added back, the negative returns false. The remaining nested-exhaustiveness diagnostics on a whole-root resolve of this module are the two gunbc.package_delivery sites (the checker false positive still-swift-363 owns) and roadmap_belt_actuate, which is J5. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u
…-172-j3-lease-plan-refusal
…unt is a corpus claim Correcting the evidence I added in the previous commit, on the authority of the instrument's own carrier note. gunbc.compile_diagnostic_census says of itself: "a census taken of a fixture that imports any production module carries that closure's rows - blocking ones among them - and a CensusObserved is not evidence that the fixture itself compiled clean", and it names the two exact forms: "a count scoped to a class AND subject_name, and a DIFFERENTIAL between two censuses whose sources differ on one axis". Mine were TOTAL blocking counts -- `> 0` against `== 0` -- which is the weakest of the three and the one that note explicitly rules out. The positive was asserting that the entire gunbc.session_lease closure emits no blocking row, which is a property of the corpus that happens to hold today; and the negative would have been satisfied by any row from anywhere in that closure, so its green did not mean the wall was what refused. MEASURED, rather than assumed: the two fixtures carry 3 and 2 rows and differ at exactly one key -- InternalError at variable:RefuseForeignOwner, which is the deleted plan failing to resolve. Both assertions are scoped to that key, so the shared rows cancel and the remaining one is attributable to the plan the two sources differ by. The census is also now read through the coproduct into an Optional, so CensusNotRunnable stays distinct from "observed nothing" rather than folding into the same count. Both witnesses re-run green in the scoped form. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u
gunbai-bot
Bot
deleted the
session/keen-ferret-172-j3-lease-plan-refusal
branch
September 3, 2026 00:23
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
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.
Session lease: a refusal is not a plan, so delete RefuseForeignOwner rather than answer for it
Two judgement-pile sites from the #10028 nested-exhaustiveness census, both in
gunbc.host.host_effect_nbd_proxy_serve (host_effect_nbd_proxy_serve_apply and
..._apply_with_observation), both uncovered on
Apply { plan: RefuseForeignOwner }.The obvious repair is an arm, and it is the wrong one.
Applyis the decision thatEXECUTES a plan, so
Apply { plan: RefuseForeignOwner }reads "execute the refusal" --and at a host-effect boundary an accept arm there would be fail-open, while a refuse arm
would be a second place answering a question the decision already answers.
WHAT THE PRODUCER ACTUALLY DOES. gunbc.session_lease decision_for_process_port_verdict is
the sole producer of UpsertDecision, and it maps Conflict to
Refuse { reason: "foreign process owns port" }. RefuseForeignOwner is constructed nowherein the tree: grep over every file, unfiltered, finds the declaration and one prose mention
in docs/plans/dispatch-maintain-cc.md, and no constructor and no pattern anywhere. So one
fact -- a foreign owner holds the port, therefore refuse -- had two representations, one of
them dead, and the dead one is what every consumer of the decision was being asked to
answer for.
So the variant is deleted. Both sites are then exhaustive with the arms they already had;
no arm is authored at all, and the fan-out is zero because there was nothing to migrate.
That is §4b rung 4 -- the state has no constructor -- rather than rung 2. The doc line that
listed the three plans is corrected in the same commit.
ENROLLED EVIDENCE, not a discarded probe. test.claim.process_lease_plan_is_not_a_refusal_witness
hands two fixture sources to the compiler through gunbc.compile_diagnostic_census:
w_a_refusal_cannot_be_written_as_a_lease_plan -- blocking rows > 0
w_a_real_plan_on_the_same_arm_is_admitted -- 0
Both import the real gunbc.session_lease, so re-adding the variant makes the negative go
quiet and the file fail. The pair differs only in WHICH plan is written into the same
Apply, so a green negative cannot be explained byApplybeing unusable.SENSITIVITY, MEASURED. With RefuseForeignOwner added back, the negative returns false.
The remaining nested-exhaustiveness diagnostics on a whole-root resolve of this module are
the two gunbc.package_delivery sites (the checker false positive still-swift-363 owns) and
roadmap_belt_actuate, which is J5.
Co-Authored-By: Claude Opus 5 noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u
🤖 Generated with Claude Code
https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u