Repository navigation
Codex press: a user agent that is not a string is a missing user agent - #10137
Merged
briansrls merged 6 commits intoSep 3, 2026
Merged
Conversation
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
…72-j5b-initialize-disposition
…ontrol 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
Contributor
Author
|
Addressed in the push above (review 59089). Both halves were right, and the second one was the one that cost something. The hand-rolled predicate is gone. The positive control was genuinely weak, not just stylistically so. Asserting Evidence. Both witnesses execute green under a gunbc built from the #10028 branch. The strengthened control was then mutated in isolation — expected variant moved from — sent from keen-ferret-172 |
… 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
requested changes
Sep 3, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
There was a problem hiding this comment.
HOLD on exact head 7e1c76f. The missing match arm is real, but AccountTripMissing is the wrong answer. This input contains an initialize result and a present userAgent member; its value is malformed for the required string contract. Downstream, AccountTripMissing becomes AccountStandingInitializeMissing, renders initialize_missing, and ultimately says “codex app-server trip missing initialize result.” That is false and points at the transport instead of the malformed provider response.
The three existing sibling arms do not establish this answer; they expose the broader conflation. Split response absence from missing/malformed required-member content. A present non-string member needs a typed malformed/unreadable-initialize-result disposition, classified as incomplete/protocol-invalid; reserve initialize-missing for an absent initialize response. Migrate the adjacent absent/duplicate/not-object member cases as their actual facts require rather than adding a fourth route into the false downstream reason. Keep the current string positive control and add a discriminator requiring the final classification/reason, not only the local frame disposition.
… 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
Contributor
Author
|
Addressed in The split turned out to be total rather than a policy line.
On the witness. You were right that the old one asserted the frame's answer and would have passed unchanged while the actuated reason lied. Five witnesses now: two on the frame disposition, two on the final classification and its operator projection, and one that builds a full standing receipt with present wire evidence and reads the actuated refusal reason off a real All five green under a gunbc built from the #10028 branch, and all 22 sibling witnesses in The annotation that argued malformed equals missing is deleted; what replaces it states why every arm of that reader describes a frame that arrived. — sent from keen-ferret-172 |
…72-j5b-initialize-disposition
Contributor
Author
|
@briansrls — your HOLD on
The migration is total, which is stronger than the "adjacent cases" framing. One deliberate deviation from your text, flagged rather than glossed. You wrote "classified as incomplete/protocol-invalid". I did not route it to the existing On the discriminator. The fifth witness builds a full I have also removed the annotation that argued a non-string userAgent is a missing one. You were right that the sibling arms expose the conflation rather than establishing the answer, and an argued conflation is worse than a silent one. — sent from keen-ferret-172 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
… surfaces The checker in this PR reports 13 sites that main's checker cannot see. Two are owned elsewhere (#10137, #10109); these are the eleven unowned. They follow ONE rule, not three shapes: an added arm must preserve the producer's declared state AS FAR AS THE CONSUMER'S CARRIER CAN REPRESENT IT. PROPAGATE (4) -- refinement_preservation:42, :44, :60, idempotent_operation_conformance:200. These RECONSTRUCT an Outcome. Widening alone would match `diagnostics: _` while still EMITTING `diagnostics: None`, which does not discard a present fact -- it FABRICATES the absence of one, downstream, where nothing can recover it (DESIGN.md section 5, fabricated-plausible-output). They now bind `diagnostics: ds` and re-emit it. This is not a new rule: the Rejected arm directly beneath each already reads `Rejected { diagnostics: d } => Rejected { diagnostics: d }`, so the change removes a section 3 fork between two arms of a single match. refinement_preservation:42 FORWARDS into an inner match rather than reconstructing, so plain propagation had nowhere to put the outer advisory. It uses the existing `v2.std.diagnostic.bind_outcome_accepted`, which is exactly that composition -- merge into an accepted inner, prepend via rejected_with_pending on a rejected one. No new combinator was minted. WIDEN (6) -- refinement_preservation:54, :70, :79, idempotent_operation_conformance:238, language_behavior_equivalence_test:255, :268. The four witnesses assert propositions that name no diagnostics; the two bridges FORWARD a claim into a runner and return Verdict / TestClaimRun, which carry no position for an emit-time advisory, so widening asserts nothing false. idempotent:238 was checked against its own authored rationale rather than its name: that annotation states a non-pass claim is established only by a comparison that RAN AND DIVERGED, and an `Accepted { diagnostics: Some }` run did run -- so `Some => false` would contradict the sentence the site exists to enforce. REFUSE (1) -- compile_eval_thesis_proof_test:86, a VALUE-CONSTRUCTOR omission. `diagnostics: _` is already a wildcard there, so `Some => false` is not merely wrong but unwritable; the missing variant is the other value constructor, which the witness cannot destructure and so cannot evaluate its proposition over. Arm is false, with TranslateResult added to the import block. CARRIER GAP, recorded not fixed: widening the two language_behavior_equivalence bridges DROPS the emit-time advisory, because Verdict and TestClaimRun have nowhere to put it. That is section 4b's outside-the-modeled-guarantee column -- honest loss at a boundary -- whereas every alternative fabricates an event: mapping Accepted{diagnostics: Some} onto SemanticMismatch{actual: Rejected} asserts a mismatch observed against a rejection that never happened, and TestClaimRun is a product with no refusal variant, so there is no arm to add. NOT TAKEN, deliberately: the whole of refinement_preservation_generated_nonempty_list_claim is literally bind_outcome(o, f), and the section 2 fold would dissolve sites :42 and :44 by removing both matches. That reshapes the function well beyond the ruled repair; "the checker forced me to touch this line" is not authority to restructure the code around it. Recorded in the PR as an observation. VERIFIED BY EXECUTION, binary built 12:53:33 from the merged tree: of the twelve sites this checker reported under the src/v2 root arm, one remains -- native_agreement_support:21, which is #10109's. No new error kind appeared; the 20 other blocking errors in that arm are in ownership_movable_test.dag (imports v1.compiler.ownership, unreachable because v1 is not a source root in this arm) and a deliberate leak fixture, neither of which this diff touches. Ruling and per-site verification with tidy-lynx-804 (BT-N). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf
briansrls
deleted the
session/keen-ferret-172-j5b-initialize-disposition
branch
September 3, 2026 17:10
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 3, 2026
…tes surfaced, all closed) (#10028) * See through nested patterns in the .dag exhaustiveness checker `check_match_exhaustiveness` folded arm coverage as `VariantPattern { name: n, parent_enum: _, field_bindings: _ }` and keyed a covered-set on the head name alone, so an arm restricting a field to ONE inner constructor marked its whole variant covered. The parser does not lose the nesting -- `parse_field_bindings` recurses into `parse_pattern` -- so the fact was DISCARDED, not missing. MEASURED, both halves, on `type Inner = P { v: Bool } | Q` / `type Outer = A { i: Inner } | B` with `match o { A { i: P { v: v } } => v B => false }`: before: gunbc compile --target rust -> exit 0, `compiled: 6 files emitted, 0 diagnostics` cargo check on the emission -> error[E0004]: non-exhaustive patterns: `&Inner::Q` not covered, exit 101 after: gunbc compile -> refused at emit, error[m.dag:5:3]: non-exhaustive match: missing variant(s) A { i: Q } The emission was a FAITHFUL lowering of the accepted graph, so the target compiler was performing the analysis the front end declined. That backstop is expiring: rustc catches these only while the seed still emits Rust, and section 7 shrinks the seed toward zero. THE CONSTRUCTION. Coverage is now a pattern MATRIX -- rows of patterns over a vector of column types -- specialised one constructor at a time. Per-field coverage would fail open in the original direction (`A { x: P, y: Q }` beside `A { x: R, y: S }` reports both columns covered while `A { x: P, y: S }` matches nothing), so the columns are carried jointly and never separately. Field types come from `lookup_variant_in_type`, the same authority that types the binding a nested pattern introduces. The branch gate is signature COMPLETENESS, not "some row is irrefutable" -- the latter drops the constructor rows that also cover a wildcard's values and refuses `A { x: P, y: _ }` beside `A { x: _, y: P }` and `A { x: Q, y: Q }`, which is exhaustive. That near-miss is pinned by its own control. RETAINED BLINDNESS, DECLARED RATHER THAN WIDENED: a column whose type carries no closed constructor roster -- Int, String, Bool -- is not refused when covered only by literals. That is the pre-existing top-level behaviour carried to depth, and closing Bool would refuse live code (`v2.compiler.infer` `infer_bool_literal_pattern_classify` is exhaustive THROUGH its nesting). NEXT-RUNG TRIGGER: a closed constructor roster for the kernel scalar types. Rung claimed for nested COPRODUCT columns only: below-the-ladder -> 3. EVIDENCE. 13 single-module fixtures executed against a seed rebuilt from this change, 13/13 at their asserted counts. Eight are new, and two cannot pass under a weaker implementation: `w_two_nested_columns_are_judged_jointly_not_per_field` is red under per-field coverage, `w_overlapping_wildcard_columns_are_not_over_refused` is red under the completeness-gate near-miss above. `w_optional_nested_*` carries the shape that actually occurred -- nesting inside `Present` over `Optional<T>`, where the roster is SYNTHESISED rather than read off declared children. The population specimen is gunbc#9964 (still-swift-363): adding a fourth `InferredNode` variant refused SEVEN flat matches and stayed silent on TWO nested ones in the same run. Those two sites were repaired there; this is the checker. Ledger: a second instance on the existing `accepted_source_emits_uncompilable_target` row -- same invalid state, different mechanism -- converted to one-line form per gunbc#9898. Regen: `v1_compiler_infer_patterns.rs` only. Baseline regen on an unmodified tree drifts `compiler_tests.rs` and `std_realization_schedule.rs`; those are not this change and are not committed here. The candidate is byte-identical from linux/amd64 and arm64 (sha256 00b0f2f949de75a6, 1414 lines). `docs/design-ledgers.md` regenerated via `tools.generated_artifact_gate` `main_wet_one`: one line changed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Hold the variant-in-type-position narrowing, and correct the Bool scope claim Two corrections against my own previous commit, both found by measurement rather than review. 1. THE VARIANT-IN-TYPE-POSITION NARROWING IS REVERTED, NOT REFINED. I had read the two `gunbc.package_delivery` refusals as false positives: the producer returns `HostCliDependencyAbsent?`, Optional of a single VARIANT, so by inhabitance only that variant can occur and the parent's other arm is unreachable. That reading is not wrong about inhabitance, and it is still not what should govern. The .dag type system already answers what that column is, and answers it out loud: on `Present { value: a } => a.tool` it refuses `no field 'tool' on type 'VObs'` (still-swift-363, executed). The corpus sites survive only because they destructure IN THE PATTERN, which works against a variant even when the column is the parent -- one column, two spellings, and only one makes the type system speak. A roster answering `singleton` while resolution answers `parent` is one concept with two answers inside one compiler (section 3). The decisive ground is section 5 and it does not require the merits to be settled: the narrowing is the arm that makes the checker STOP REPORTING a class. If it is wrong it suppresses a real floor class permanently; if the other reading is wrong, two sites carry an unreachable arm -- wasteful, loud, safe. Under genuine uncertainty the refusing arm wins. What is actually undecided -- whether a variant should be a FIRST-CLASS TYPE, making `HostCliDependencyAbsent?` genuinely a singleton Optional -- is recorded at the declaration as a section 4b(2) no-untracked-stall. It is a substrate question (Rust cannot express it, hence the emitter's variant_to_enum) and is deliberately not settled here. The two witnesses are inverted to PIN the parent-roster behaviour, with the negative left loud on purpose: if the substrate later makes variants first-class, that witness fails, and the failure is the signal. 2. THE BOOL SCOPE CLAIM IN THE PREVIOUS COMMIT WAS FALSE. It said Bool columns stay open. `std.types` declares `type Bool = True | False`, an ordinary Disj, so a Bool column resolves to a two-arm roster and IS closed -- correctly, since the emitted match faces the same two arms. `gunbc.host_standup GreenPlaceFromGunbcGate` matching `{ gate_verdict: false }` without covering `true` is a genuine nested defect, not a phantom. So the checker is right and the prose was wrong. It UNDERSTATED what the change does, which is still a rung-honesty defect: a scope sentence nobody can check against the code fails the same way an inflated one does, pointing the other way. Genuinely open, refused nowhere: Int and String. That half of the claim survives. CENSUS, corrected for a double-count. An earlier figure of 190 counted BOTH renderings the compiler emits per diagnostic -- a byte-range summary line and an `error[file:line:col]` line -- so it read instrument output as subject content. Split: 95 and 95. Comparable figures, both grepped on the error form over a whole-corpus compile of dag + src/v2: main's checker ... 11 sites this change ...... 95 sites, 47 files delta ............ 84 newly exposed Main is green with those 11 already standing because the required floor runs a gate closure and does not compile the whole corpus -- "main is green" and "the corpus eliminates closed variants exhaustively" were never the same claim. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Record the two census rulings at the carriers that will be read next Annotation-only: the emitted seed is byte-identical, which is section 4c's erased projection doing what it promises -- prose that changes no semantic bytes. 1. THE package_delivery PAIR IS A MODELING DEFECT, NOT A MISSING ARM (tidy-lynx-804, after reading the producer). My previous note framed those two sites as an open question with two defensible repairs. That was too weak. Adding a `HostCliDependencyPresent` arm would answer for a state that cannot occur by inhabitance -- a fabricated plausible output at a site whose whole purpose is refusal, silencing the checker without making anything exhaustive. The real repair is ordinary section 2 modeling and is cheaper than the substrate question I had named: the concept `an absence carrying tool and hint` already exists but is fused into a variant, so it cannot be named in a type position. Give it its own type, let the observation be `Present | Absent(that type)`, and both matches become exhaustive with one arm -- legitimately. That is its own PR and explicitly NOT a row in this census. So my 4b(2) row was pointing at the wrong blocker. Whether a variant should be FIRST-CLASS is still undecided and still recorded, but it is not what these two sites are waiting on. 2. A MECHANICAL `=> false` IS A TEST-ONLY REPAIR. I had called the 8 production sites carrying the same Scaffold shape `probably A-like`. They are not, and the reasoning generalises to every future census of this class: in a `test fn -> Bool` the arm is a claim ABOUT THE FIXTURE and naming each shape BUYS fail-closure, because a variant added later turns the site red again. In a production `fn` the identical arm is a semantic answer returned to a real caller and SPENDS that property, converting a site that fails loudly on an unhandled variant into one that silently answers false. Same shape, opposite effect -- and the diagnostic cannot tell them apart, because it reports the missing witness and not what the enclosing declaration returns. Recorded in the witness carrier rather than a handoff message, because the census will keep producing this shape after the handoff is forgotten. 3. THE POLARITY READ IS BLOCKING, NOT ADVISORY. I had filed it as a caveat. A site whose match INVERTS its assertion needs `true`, and writing `false` flips what the test means while leaving it green -- and NEITHER instrument in this program can catch that: the suite is green by construction either way, and the site leaves the refusal census either way. Nothing downstream contradicts a wrong polarity, so it has to be read at the site before the arm is written. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Strike the withdrawn polarity obligation from the witness carrier A blocking per-site POLARITY read was recorded here two commits ago. It had already been retracted when I wrote it -- the retraction went to another lane and not to me -- so I cemented an obligation nobody was holding. It is struck rather than quietly deleted, because the reason it was put in a witness carrier is the reason leaving it would be worse than never recording it: a carrier outlives the thread that wrote it, so a retracted requirement standing here reads as live to everyone who touches this census afterwards. WHAT CLOSED IT was a structural argument, not a larger sample. Every group A enclosing declaration is NULLARY -- `test fn name() -> Bool`, no parameters -- so nothing threads in from outside and the scrutinee is a closed term. Exactly one arm is ever taken, and an arm added for a shape the closed scrutinee does not have is UNREACHABLE: never evaluated, producing no value. Polarity is a property of how a value reaches an assertion; a dead arm has none to get wrong. Verified here before amending: 63 of 63 nullary, zero exceptions, zero unresolved. What replaces it is the useful half, and it BOUNDS this PR's own claims rather than adding an obligation to someone else's: the green at a repaired A site is green BY CONSTRUCTION, so there is no discriminating red to construct per site and this suite must not be cited as validating a repair batch. A batch is reviewable by reading the arms against the declaration, and by the witnesses here covering the CHECKER. The test-vs-production buys/spends distinction is untouched and still stands. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Restate the polarity obligation as a distinction, not a withdrawal This annotation has now been wrong in both directions -- first recording a blocking per-site polarity read, then withdrawing it wholesale -- and the operator's ruling separates them. The added arms are unreachable, so the suite passes identically before and after and cannot discriminate a wrong arm. That retires the EXECUTING witness, not the SOURCE read: an arm whose value is never computed is still an authored claim about what the value would be, and only a reading of the source can judge it. Unreachability removes runtime execution as an oracle; it does not make the authored value self-justifying. The sharpest part, and the part this carrier had wrong: the checker's shrinking refusal set is the discriminating evidence for EXHAUSTIVENESS, not for POLARITY. The two had been conflated here, which is what produced both the over-demand and the over-withdrawal. Restated rather than deleted, for the same reason it was struck rather than deleted before: a witness carrier outlives the thread that wrote it, so an obligation left in either wrong state reads as settled to whoever next touches the census. Annotation-only -- every changed line begins with //, verified mechanically rather than by eye, so under DESIGN section 4c this is erased before any semantic pass and cannot move a diagnostic. The live checker is unchanged at 788ee9c, so no downstream receipt is invalidated by this commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Re-trigger CI: the run on f7d13bd registered as a corpse Run 33683206017 was created 21:06:04Z for this head and never acquired a runner: status=pending, jobs=0, updatedAt frozen at 21:06:05Z -- one second after creation and untouched 22 minutes later. `gh run rerun` refuses it with "this workflow is already running", so the dead registration holds the slot and cannot be revived in place. Classified before acting rather than assumed: the repository's CI is healthy. Runs created AFTER this one, on file-instrument-class and four other session branches, are in_progress. So this is an isolated never-acquired registration, not queue contention and not a provider outage, and re-triggering is the right response rather than waiting longer. An empty commit is the mechanism because a workflow_dispatch run would not attach to the pull request as a check, and the corpse blocks rerun. No source change: the tree is identical to f7d13bd. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * File the go and python instances of the class, with the python arm's discriminating detail still-swift-363 produced a three-line probe accepted with zero blocking diagnostics on all three reachable targets; rust emits a compiling module and python and go do not. They stated honestly that they had NOT run either toolchain, so the go and python halves arrived as source readings. I ran python, and the executed result is materially worse than the reading: py_compile PASSES import SUCCEEDS typing.get_type_hints NameError: name 'Optional' is not defined calling the function NameError: name 'Present' is not defined `from __future__ import annotations` defers annotations to strings, so the undefined `Optional` never evaluates at import and the module loads clean. The defect surfaces only when the function is CALLED. That is the sentence worth carrying: AN EMISSION DEFECT THAT SURVIVES IMPORT IS FAR MORE DANGEROUS THAN ONE THAT DIES AT IMPORT, because every cheap verification anyone would reach for reports success. "python emission is uncompilable" understates it into something a reader would expect a smoke test to catch. The GO arm is recorded as a SOURCE READING and not a toolchain receipt, because no go toolchain exists in this container. It is kept lexically separate from the python result rather than sitting beside it as though both were executed: two values returned from single-return signatures, `[]*int64` declared against `[]interface{}` returned, and an undefined `Present`. Filed as a further instance on the existing row rather than as a new class -- these are the same invalid state reached on two more targets, and minting a second name for it is the nicknaming DESIGN section 3 forbids. Row compiles 0-blocking at 10 files and 95 advisories; the projection was regenerated rather than hand-edited, and the checker restored by sha afterward. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Dissolve the duplicate irrefutability predicate into v1.std.core (review 59122) review 59122 (codex/gpt-5.6-sol, REQUEST_CHANGES) found that this PR added `pattern_is_irrefutable` to 04_patterns while `match_pattern_is_irrefutable` already existed in 05_emit_rust -- two hand-written discriminators over one type, free to drift as MatchPattern grows. Verified before acting: the predicate is mine, added by bc31751, absent from main, and the two bodies agree on every constructor that exists today. The finding is correct. Irrefutability is a fact ABOUT `MatchPattern`, so it now lives with the type in v1.std.core (00_core.dag), which already declares MatchPattern and hosts 202 functions. Both consumers import it; neither re-derives it. Definition count is now 1 in v1.std.core and 0 in each consumer. Two judgement calls. The surviving NAME is main's `match_pattern_is_irrefutable` rather than mine -- renaming an established symbol to this branch's spelling would be nickname churn on top of a section 3 fix. The surviving BODY is the exhaustive one rather than emit's `_ => false`: a catch-all answers `false` for any constructor added to MatchPattern later, silently classifying a new irrefutable form as refutable, while the exhaustive match refuses and makes the author decide. Behaviour-preserving today, fail-closed tomorrow. VERIFIED BY REGEN FIXED POINT, not by reading the two bodies. Pass 1 declared drift in exactly the three expected mirrors and nothing else: v1_std_core.rs gains the function, v1_compiler_infer_patterns.rs loses its local copy, and v1_compiler_emit_rust.rs loses its local copy while its five call sites become `crate::v1_std_core::`-qualified -- the mechanical consequence of the definition changing modules, not of the predicate changing meaning. Pass 2, run from a binary built from the installed seed, reports first_generation_equal=true at 153/153. That second pass is the receipt: the recipe warns a single pass can self-verify at divergence 0 for the wrong reason. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Repair the eleven nested-pattern exhaustiveness sites the new checker surfaces The checker in this PR reports 13 sites that main's checker cannot see. Two are owned elsewhere (#10137, #10109); these are the eleven unowned. They follow ONE rule, not three shapes: an added arm must preserve the producer's declared state AS FAR AS THE CONSUMER'S CARRIER CAN REPRESENT IT. PROPAGATE (4) -- refinement_preservation:42, :44, :60, idempotent_operation_conformance:200. These RECONSTRUCT an Outcome. Widening alone would match `diagnostics: _` while still EMITTING `diagnostics: None`, which does not discard a present fact -- it FABRICATES the absence of one, downstream, where nothing can recover it (DESIGN.md section 5, fabricated-plausible-output). They now bind `diagnostics: ds` and re-emit it. This is not a new rule: the Rejected arm directly beneath each already reads `Rejected { diagnostics: d } => Rejected { diagnostics: d }`, so the change removes a section 3 fork between two arms of a single match. refinement_preservation:42 FORWARDS into an inner match rather than reconstructing, so plain propagation had nowhere to put the outer advisory. It uses the existing `v2.std.diagnostic.bind_outcome_accepted`, which is exactly that composition -- merge into an accepted inner, prepend via rejected_with_pending on a rejected one. No new combinator was minted. WIDEN (6) -- refinement_preservation:54, :70, :79, idempotent_operation_conformance:238, language_behavior_equivalence_test:255, :268. The four witnesses assert propositions that name no diagnostics; the two bridges FORWARD a claim into a runner and return Verdict / TestClaimRun, which carry no position for an emit-time advisory, so widening asserts nothing false. idempotent:238 was checked against its own authored rationale rather than its name: that annotation states a non-pass claim is established only by a comparison that RAN AND DIVERGED, and an `Accepted { diagnostics: Some }` run did run -- so `Some => false` would contradict the sentence the site exists to enforce. REFUSE (1) -- compile_eval_thesis_proof_test:86, a VALUE-CONSTRUCTOR omission. `diagnostics: _` is already a wildcard there, so `Some => false` is not merely wrong but unwritable; the missing variant is the other value constructor, which the witness cannot destructure and so cannot evaluate its proposition over. Arm is false, with TranslateResult added to the import block. CARRIER GAP, recorded not fixed: widening the two language_behavior_equivalence bridges DROPS the emit-time advisory, because Verdict and TestClaimRun have nowhere to put it. That is section 4b's outside-the-modeled-guarantee column -- honest loss at a boundary -- whereas every alternative fabricates an event: mapping Accepted{diagnostics: Some} onto SemanticMismatch{actual: Rejected} asserts a mismatch observed against a rejection that never happened, and TestClaimRun is a product with no refusal variant, so there is no arm to add. NOT TAKEN, deliberately: the whole of refinement_preservation_generated_nonempty_list_claim is literally bind_outcome(o, f), and the section 2 fold would dissolve sites :42 and :44 by removing both matches. That reshapes the function well beyond the ruled repair; "the checker forced me to touch this line" is not authority to restructure the code around it. Recorded in the PR as an observation. VERIFIED BY EXECUTION, binary built 12:53:33 from the merged tree: of the twelve sites this checker reported under the src/v2 root arm, one remains -- native_agreement_support:21, which is #10109's. No new error kind appeared; the 20 other blocking errors in that arm are in ownership_movable_test.dag (imports v1.compiler.ownership, unreachable because v1 is not a source root in this arm) and a deliberate leak fixture, neither of which this diff touches. Ruling and per-site verification with tidy-lynx-804 (BT-N). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Admit the four TargetChanged bindings the irrefutability dissolution moves The namespace-wave-admission phase refused this PR with 4 unadjudicated deltas, 0 stale, 47 consumed. The four are the call sites of match_pattern_is_irrefutable, whose target moved when review 59122's §3 fix dissolved the duplicate predicate into v1.std.core: v1.compiler.emit_rust::collect_pattern_rc_variant_guards v1.compiler.emit_rust::emit_typed_match_arm_strs v1.compiler.emit_rust::rc_arm_has_refutable_plain_field v1.compiler.emit_rust::rc_pattern_preludes `match_pattern_is_irrefutable` base {v1.compiler.emit_rust} -> head {v1.std.core} TargetChanged does not auto-admit -- gunbc.compiler_frontend_program_interlock records that it refuses unless an exact authored transition admission names it -- so this adds one exact row per binding, following the #10011 and #9436 re-home precedent. These are DATA rows in the already-rostered NAMESPACE_TRANSITION_ADMISSIONS declaration: no new declaration, type, function or admission mechanism, so the existing seed-growth justification covers them. They carry their own deletion trigger, as that roster's rule requires -- once this PR merges the rows match no delta and go stale, which reds required CI until they are removed. WHY THE FILE IS EDITED DIRECTLY rather than through a .dag. The rows exist only in src/v1/stage0/src/namespace_wave_admission.rs; no .dag carries them, so there is nothing to project from. Confirmed two ways rather than assumed: the --required-regen pass never names this file (0 mentions in its log), and `git check-attr merge` reports `unspecified` for it while reporting `generated-artifact` for v1_compiler_emit_rust.rs and docs/design-failure-modes.md as a control. It is hand Rust that the candidate tree copies through. NOT FIXED HERE, because it is not this lane's: the floor still refuses on one site, src/v2/compiler/self_host/native_agreement_support.dag:21, missing `SemanticMismatch { actual: Rejected, falsification: Present }`. That is #10109's and its diff adds exactly that arm. This PR cannot go green until #10109 lands. A NOTE ON THE DIAGNOSIS, because the first one was wrong and its wrongness was invisible. The propagate arms in the previous commit introduce exactly four new pattern bindings (ds, cd, ds, ds), and I initially attributed deltas=4 to those and confirmed it by counting them in the diff. Two independent explanations each predicted four, so the matching count ratified the wrong one. The itemisation sits ~50 lines above the failure line in the job log and names the real subject. The failing set is not enumerated AT the failure line while all 47 passing admissions are, which is the wrong way round. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * File the ConstructorsOpen conflation, and discharge the 17 now-consumed rows TWO UNRELATED THINGS THE REQUIRED RUN AT 543c83d ASKED FOR. 1. THE ADMISSION ROSTER. Main's 17 `call-reachability grounding gunbc#10156` rows became CONSUMED when that transition landed, and this branch touches the roster, so they are due. A previous commit deliberately preserved them on the grounds that nothing observed said they were consumed; that was correct on the evidence then and is superseded by an observation that says they are. Deleted, with the identity join run FIRST: the phase's own CONSUMED ADMISSION enumeration joined against the labelled rows on (module::in_declaration, spelling, target), both set differences EMPTY under LC_ALL=C, 17 for 17. The dead const is removed too -- this time exactly its two declaration lines, NOT the surrounding prose, which is the over-deletion the previous merge had to repair from main's side. Roster is now 4 rows: this PR's own, which inherit the same obligation. 2. A THIRD INSTANCE OF THE PR'S OWN FAILURE CLASS, FOUND BY REVIEW 59399 AND FILED RATHER THAN FIXED. `constructor_roster_for` answers `ConstructorsOpen` from an ELSE branch, conflating three states with three different correct answers: a genuine open scalar (a witness is owed), a single-constructor product -- a record, no `|`, hence no Disj connective -- which is CLOSED with one constructor and whose total destructure is total, and a type whose lookup FAILED, which is ignorance and not an answer. The arm answers `[]`, i.e. exhaustive, when no row head is irrefutable. That is a widening failure arm and it is AUTHORED BY THIS PR, not inherited: origin/main carries zero occurrences of ConstructorsOpen and never examines these positions at all. WHY IT IS FILED AND NOT FIXED, MEASURED RATHER THAN ARGUED. The one-line remedy -- delete the guard so the arm refuses -- was implemented, built, and reverted. Positive control fires; a `_`-arm match stays green; and the corpus reports NINETEEN sites, sampled rather than counted, which are FALSE POSITIVES of the second kind: v2.std.grammar derive_grammar_relation_token_edges_recursive_step matches a Witness with both arms present and is reported for its nested DeriveGrammarRelationTokensProgress column, a three-field record. Flipping the arm trades a fail-open for a fail-closed-on-valid-input without touching the modelling deficit underneath, and for the third state it would blame the author for the checker's ignorance -- DESIGN section 5's top-as-answer versus top-as-ignorance, the same clause the review cites, pointing the other way. Rung found at 1 (the emitted target refuses at its own compiler, so the harm is a failed downstream build, not a silent wrong answer). Ceiling STRUCTURAL, because membership is decidable from the type environment. Next-rung trigger: split the roster three ways, sufficient for a closed single-constructor product to be adjudicated as closed and an unresolved type to refuse as unresolved; the nineteen sites are that trigger's acceptance corpus, not its debt. NOT IN THIS COMMIT, AND NOT A DEFECT: the required run also refused on COMPLETED-OVER-COST-REQUIREMENT for v2.test.emit.rust_produced_decl_emit.rust_produced_decl_name_discriminates at cost=507ms against a 500ms CPU budget, in a file this PR does not touch, with claims_failed=0, unexpected_failures=0 and 13/13 changed witnesses passed. That is the known near-the-line variance class; the remedy is a rerun, not a diff. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Correct this change's own scope sentence about what ConstructorsOpen covers The note above `ConstructorRoster` read "GENUINELY OPEN, and refused nowhere: Int and String columns", enumerating two states. That is false, and it is false in the way the paragraph DIRECTLY ABOVE IT warns against: that paragraph corrects an earlier draft for understating scope and calls it a rung-honesty defect, because "a scope sentence nobody can check against the code is the same failure as an inflated one, pointing the other way". This sentence committed the same error one paragraph below its own warning. `ConstructorsOpen` is an ELSE branch. It is not the set {Int, String}; it is everything that is not optional, not a witness, and carries no Disj connective -- three states with three different correct answers: - a genuine open scalar, where a finite literal set cannot cover the value space and a witness is owed; - a SINGLE-CONSTRUCTOR PRODUCT (a record, no `|`, hence no Disj), which is CLOSED with exactly one constructor and whose total destructure is total; - a type whose lookup FAILED, where resolve_scrutinee_type returns the node unchanged -- IGNORANCE, NOT AN ANSWER. The note now names all three, carries the live specimen (v2.std.grammar derive_grammar_relation_token_edges_recursive_step, whose nested DeriveGrammarRelationTokensProgress column is a three-field record), records the measured nineteen-site false-positive population that reverted the obvious fix, and names the three-way roster split as the next-rung trigger with those sites as its acceptance corpus. FOUND BY READING THE APPROVAL RATHER THAN BANKING IT. review 59419 credited this block for "honestly naming what stays open (Int/String columns) as a next-rung trigger". The block does exist and does say that, so the credit was accurate -- but checking it is what surfaced that the sentence itself was incomplete. An approval resting on a claim the code only partly supports is harder to catch than one resting on an absent artifact. ANNOTATION ONLY, so §4c's annotation-erased projection means no semantic change: the stage0 mirror is byte-unchanged (verified, zero diff) and no regen is owed. Full-root compile is clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf --------- Co-authored-by: Brian Searls <briansearls1@gmail.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
1 participant
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.
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 notbeen 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.
VALUE shape, so a green negative cannot be explained by the key being unreadable.
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
🤖 Generated with Claude Code
https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u