Repository navigation
devboot BuildRefusal: the arm carries the detail, not the outcome the refusal came from (#10028 J6) - #10162
Merged
Conversation
… refusal came from (#10028 J6) `WorktreeNotSnapshotted` and `ToolchainNotObserved` each named a REFUSAL VARIANT in a field position -- `SnapshotRefused`, `ToolchainObservationRefused`. A variant is not a type, so the field typed as the whole coproduct it belongs to (`SnapshotOutcome`, `ObservedToolchain`), and `WorktreeNotSnapshotted { refusal: SnapshotTaken { ... } }` was writable: a "not snapshotted" refusal carrying a successful snapshot. Every reader then had to answer for a state no producer can build, which is what the #10028 nested checker reports at both match sites. Both producers already destructure the detail at the call site and rebuild the wrapper around it, so holding the String directly is what the code was doing in every direction but the declaration. The unwritable state now has no constructor. EVIDENCE. All 18 witnesses in dag/test/claim/devboot_build_product_witness_test.dag executed green against this tree. No census probe is enrolled: the compile-diagnostic census cannot discriminate these two fixtures at ANY key -- measured, the red and green fixture histograms are identical, because the devboot import closure swamps the fixture and the census is scoped to the closure rather than to the fixture. That MISSING FIXTURE HARNESS -- a census whose subject is the fixture text rather than its transitive closure -- is this class's next-rung trigger, per DESIGN 4b. It is not a claim that the RED is unauthorable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
… instead of catching them (#10028) The nested site the checker reports here matched only JsonMemberFound { value: JsonString { .. } }, leaving JsonNull, JsonBool, JsonNumber, JsonArray and JsonObject matched by nothing. WHY ARMS AND NOT A TYPE CHANGE. This is not the #10162 shape. There the field named a VARIANT (SnapshotRefused), so it typed as the whole parent coproduct and an invalid state was writable; the repair was to narrow the field. Here JsonMemberFound's payload is already declared as JsonValue, the honest parent type, and the six value shapes are a real roster this reader genuinely has to answer for. No narrower type would be truthful, so the roster is the repair. WHY NAMED ARMS AND NOT A RESIDUAL WILDCARD. All five answer AccountTripMissing for the reason the string arm already gives, so a wildcard would read identically today -- and would silently absorb a seventh JsonValue variant into "missing" tomorrow, a plausible answer nobody chose. Named arms turn that into a refusal at the point the variant is added. json_number_as_int in this same module already enumerates the identical roster. Both witnesses re-executed green under a gunbc built from the #10028 branch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u
briansrls
pushed a commit
that referenced
this pull request
Sep 3, 2026
#10137) * Codex press: a user agent that is not a string is a missing user agent One judgement-pile site from the #10028 nested-exhaustiveness census -- gunbc.codex_app_server_press disposition_from_initialize_result, uncovered on `JsonMemberFound { value: _ }` for every non-string shape. THE ANSWER IS ESTABLISHED BY THE MODULE, NOT CHOSEN HERE. The site's own three other arms already say AccountTripMissing for the member being absent, duplicated, or hanging off something that is not an object -- all of which mean the same thing this one does: the initialize result did not identify a user agent. And the two sibling readers in this file, json_rpc_error_message and disposition_from_account_read_result, both already carry the `JsonMemberFound { value: _ }` arm explicitly. So this function was the one that had not been written down, not the one whose answer was open. The alternative -- AccountTripResultOk -- would have read a number as a valid agent, which is the fabricated-plausible-output arm DESIGN section 5 forbids at a boundary that decides whether an account is usable. EXECUTED EVIDENCE. * a_non_string_user_agent_is_missing_not_ok -- a numeric member. * a_real_user_agent_string_is_still_ok -- the control. The two differ only in the VALUE shape, so a green negative cannot be explained by the key being unreadable. * SENSITIVITY, MEASURED, on the new arm alone: line 612 answering AccountTripResultOk makes the negative return false. WHICH INSTRUMENT PROVED WHICH CLAIM. The site repair is confirmed under the #10028 checker build -- this module's nested diagnostic is gone from its output. The witnesses were run on a gunbc WITHOUT the nested checker, which is what CI compiles with today since #10028 is unmerged; under the checker build the closure still refuses on two gunbc.package_delivery sites, which are that checker's known false positive and not this subject. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u * Each disposition witness pins its expected variant, so the positive control stops accepting six of them (review 59089) codex/gpt-5.6-sol was right on both halves. The shared `disposition_is_missing` predicate hand-rolled a Bool over AccountTripFrameDisposition, and -- the part that actually cost something -- it made the positive control assert `not missing`, which any of six dispositions satisfies. A reader that answered AccountTripLoginRequiredSignal for a perfectly good user-agent string would have passed it. Both witnesses now match the disposition at the assertion site and name the variant they expect, every sibling answering false. No reusable predicate is declared, and the exact expected variant is the claim rather than its complement. EVIDENCE. Both witnesses green under a gunbc built from the #10028 branch. The strengthened control was mutated in isolation -- expected variant moved from AccountTripResultOk to AccountTripLoginRequiredSignal, nothing else touched -- and returned `false`, so it discriminates the specific variant rather than the negation it used to assert. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u * Name all five non-string value shapes at the initialize-result column instead of catching them (#10028) The nested site the checker reports here matched only JsonMemberFound { value: JsonString { .. } }, leaving JsonNull, JsonBool, JsonNumber, JsonArray and JsonObject matched by nothing. WHY ARMS AND NOT A TYPE CHANGE. This is not the #10162 shape. There the field named a VARIANT (SnapshotRefused), so it typed as the whole parent coproduct and an invalid state was writable; the repair was to narrow the field. Here JsonMemberFound's payload is already declared as JsonValue, the honest parent type, and the six value shapes are a real roster this reader genuinely has to answer for. No narrower type would be truthful, so the roster is the repair. WHY NAMED ARMS AND NOT A RESIDUAL WILDCARD. All five answer AccountTripMissing for the reason the string arm already gives, so a wildcard would read identically today -- and would silently absorb a seventh JsonValue variant into "missing" tomorrow, a plausible answer nobody chose. Named arms turn that into a refusal at the point the variant is added. json_number_as_int in this same module already enumerates the identical roster. Both witnesses re-executed green under a gunbc built from the #10028 branch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u * Split malformed-presence from absence: a present initialize result no longer actuates "missing initialize result" (review 59089) JsonMemberFound means the lookup SUCCEEDED. A present, parsed initialize result whose userAgent is not a readable string was answered AccountTripMissing, which reaches AccountStandingInitializeMissing, which renders the operator projection "initialize_missing" and ACTUATES the refusal reason "codex app-server trip missing initialize result". That sentence is false about the observed input, not merely coarse -- section 5's fabricated plausible output, actuated rather than logged. THE SPLIT IS TOTAL, NOT A POLICY LINE. disposition_from_initialize_result has exactly one caller and is reached only for an initialize response that arrived and parsed, so nothing it can observe is an absent response -- not a member that is absent, duplicated, hanging off a non-object, carrying the wrong value shape, or holding an empty string. All eight non-ok arms were wrong, so there is no boundary to defend. True absence enters elsewhere: observation_to_disposition mapping AccountTripResponseAbsent. AccountTripFrameDisposition += AccountTripResultUnusable AccountStandingClassification += AccountStandingInitializeUnusable projection "initialize_present_unreadable" reason "codex app-server initialize result arrived without a readable userAgent" AccountTripMissing keeps its name and its sentence, now narrower and true: no initialize frame on the wire. The five named JsonValue arms from the previous commit stay -- a seventh variant should still refuse rather than default; only their DESTINATION was wrong. Downstream arms added in the rate-limits liveness reader, the three columns of classify_account_trip, and codex_supervised_turn. EVIDENCE. Five witnesses, all green under a gunbc built from the #10028 branch. Four assert the frame disposition and the FINAL classification with its projection; the fifth builds a full standing receipt with present wire evidence and reads the ACTUATED refusal reason off a real press outcome, so it goes red if the old sentence is written into the new arm. The pair discriminates: absence and malformed-presence differ only in whether the initialize frame is on the wire. All 22 sibling witnesses in codex_app_server_press_witness_test re-executed green; nothing reclassified. The previous annotation argued that a non-string userAgent IS a missing userAgent, reasoning from the sibling readers. That was a durable assertion of the conflation and is deleted; what replaces it states why every arm of that reader describes a frame that arrived. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
WorktreeNotSnapshottedandToolchainNotObservedeach named a refusal VARIANT in a field position —SnapshotRefused,ToolchainObservationRefused. A variant is not a type, so each field typed as the whole coproduct it belongs to (SnapshotOutcome,ObservedToolchain), andWorktreeNotSnapshotted { refusal: SnapshotTaken { ... } }was writable: a "not snapshotted" refusal carrying a successful snapshot. Every reader had to answer for a state no producer can build, which is exactly what the #10028 nested checker reports at both match sites.Per-site justification. Both producers already destructure the detail at the call site and rebuild the wrapper around it, so holding the
Stringdirectly is what the code was doing in every direction but the declaration. This is the rung-4 arm of the choice, not the rung-2 one: the alternative — adding arms forSnapshotTaken/ToolchainObserved— would have made each reader answer for a state that stays constructible. The unwritable state now has no constructor.Source polarity. Both sites are ordinary production reads (
build_refusal_sentence, and the stage-labelling fold at build.dag:1412). Neither is a checker fixture, so no polarity inversion applies.Evidence
All 18 witnesses in
dag/test/claim/devboot_build_product_witness_test.dagexecuted green against this tree. Thedag/gunbc/devbootsubtree and that witness file are byte-identical between the tree the witnesses ran on and this PR's base, so the evidence transfers.No census probe is enrolled, and here is the measurement that decided it. The compile-diagnostic census cannot discriminate the red and green fixtures for this class at any key — measured, their diagnostic histograms are identical, because
compile_dag_diagnostic_censusis scoped to the fixture's transitive import closure and the devboot closure swamps the fixture. A probe written anyway would have been permanently green by construction: a decoration, and worse than absent because it would be cited as coverage.Per DESIGN §4b that is not a claim that the RED is unauthorable — corpus-unwritability is the first boundary and decides nothing. This class's next-rung trigger is the capability, stated so it cannot be retired by something narrower:
The narrower thing that must not retire this row is a census that merely reports the fixture's own file among its rows: that already exists, and it is exactly what fails here, because the closure's rows drown the fixture's at every key. Until the capability above lands, this class sits at rung 3 — structurally guaranteed by the type having no constructor for the invalid state — with no executing probe of its own.
🤖 Generated with Claude Code
https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u