The native side can refuse, and the label that would report it aborts on any real value by gunbai-bot[bot] · Pull Request #10109 · gunb-ai/gunbc

gunbai-bot · 2026-09-02T18:53:04Z

The native side can refuse, and the label that would report it aborts on any real value

THE OBLIGATION

Verdict.SemanticMismatch carries actual: Outcome<RuntimeValue>, so Rejected is one of its
two inhabitants. native_agreement_divergence_from_run answered only for Accepted. #10051
took the accepted-with-advisories arm and handed this one back; it is the last uncovered
combination, actual: Rejected with falsification: Present — the existing
actual: _, falsification: Absent arm already covers the other half.

The new arm names the native side with the sentinel this function's own siblings use for "no
value here" (build_failed, run_failed, deferred) and keeps the interpreted side real,
because the falsification receipt holds it. Reporting "?" for both would discard a value in
hand — the loss v2.std.native_agreement exists to prevent, per its own carrier note. Widening
the type was considered and rejected: absence is already modelled here by a named string, and
departing from that idiom for one arm is the wrong size of change.

THE FOLD'S SUBJECT IS THE VERDICT, NOT THE RUN

It read run.verdict and nothing else, so taking the whole TestClaimRun made its only
reachable caller a full emit-vs-eval execution — the cache receipt is unreachable input that no
witness can supply, which is why this arm had no executable evidence available.
native_agreement_divergence_from_verdict takes what the fold reads; ..._from_run delegates,
and no caller changes.

THE WITNESS FOUND A LIVE ABORT, AND IT IS THE LARGER HALF OF THIS CHANGE

runtime_value_discriminant_octet declared Optional<Int> while returning
list_at_optional(xs: bytes, index: 1) over a List<Byte> — an Optional<Byte>. The record
then reached octet_display's Int parameter, so runtime_value_octet_label aborted with
cannot apply Lt to Record and Int for any primitive with a second byte.

It stayed invisible because the only arm reached in practice was the empty-list one, whose
Absent answers "?". So the formatter that exists to stop a divergence being reported as
values-unknown could instead abort exactly when a divergence was being reported. Its only
consumers are the three call sites in the function this PR already edits.

Fixed by naming the conversion (integer_u8_from_byte) rather than widening the declaration,
because the carrier's octet IS an integer.

EVIDENCE, ALL BY EXECUTION

label_of_a_two_byte_primitive                                ABORTS before the fix, true after
label_of_an_empty_primitive_is_unknown                       true in BOTH states
rejected_native_side_is_named_and_the_interpreted_value_survives   true
  ... with native_value mutated "rejected" -> "?"            false
rejected_without_a_receipt_still_reports_both_sides_unknown  true

The second row is why the first is a control and not a presence-detector for the fix. The
mutation row is why the third is discriminating rather than merely executed.

CHECKER RECEIPT

Instrument bound rather than described: #10028 branch binary 788ee9c8339, sha256
60e8f568661e113b5e1173e39abe8bffe10b8663d780c7bc03a8fc878964a640, self-reporting that SHA.
Base 22e3d709639, root=src/v2.

before  39 blocking   resolved 2036 sources
after   38 blocking   resolved 2036 sources     <- population pinned
BEFORE-ONLY: exactly `SemanticMismatch { actual: Rejected, falsification: Present }`
AFTER-ONLY:  none
diagnostics remaining in any file this change touches: 0

The population is pinned across the pair, which is what licenses reading the drop as a repair
rather than as a narrower look at the corpus. The final tree reports 2038 sources because this
change ADDS two witness modules — stated rather than left as an unexplained drift.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u

… on any real value THE OBLIGATION. `Verdict.SemanticMismatch` carries `actual: Outcome<RuntimeValue>`, so `Rejected` is one of its two inhabitants, and `native_agreement_divergence_from_run` answered only for `Accepted`. #10051 took the accepted-with-advisories arm and returned this one; it is the last uncovered combination: `actual: Rejected` WITH `falsification: Present`. The arm names the native side with the sentinel this function's siblings already use for "no value here" (`build_failed`, `run_failed`, `deferred`) and keeps the INTERPRETED side real, because the falsification receipt holds it. Reporting "?" for both would discard a value in hand, which is the loss v2.std.native_agreement exists to prevent. THE FOLD'S SUBJECT IS THE VERDICT, NOT THE RUN. It read `run.verdict` and nothing else, so taking the whole `TestClaimRun` made its only reachable caller a full emit-vs-eval execution: the cache receipt is unreachable input no witness can supply. `..._from_verdict` takes what the fold reads; `..._from_run` delegates and no caller changes. AND THE WITNESS FOUND A LIVE ABORT, WHICH IS THE LARGER HALF OF THIS CHANGE. `runtime_value_discriminant_octet` declared `Optional<Int>` while returning `list_at_optional(xs: bytes, ...)` over a `List<Byte>` -- an `Optional<Byte>`. The record then reached `octet_display`'s Int parameter, so `runtime_value_octet_label` aborted with `cannot apply Lt to Record and Int` for ANY primitive with a second byte. It stayed invisible because the only arm reached in practice was the empty-list one, whose `Absent` answers "?". So the formatter that exists to stop a divergence being reported as values-unknown could instead abort exactly when a divergence was being reported. Fixed by naming the conversion (`integer_u8_from_byte`) rather than widening the declaration, because the octet IS an integer. EVIDENCE, ALL BY EXECUTION. - label_of_a_two_byte_primitive: ABORTS before the fix, `true` after. - label_of_an_empty_primitive_is_unknown: `true` in both states, so the pair is not measuring the fix's presence. - rejected_native_side_is_named_and_the_interpreted_value_survives: `true`; mutating `native_value: "rejected"` to `"?"` turns it `false`, so it is discriminating. - rejected_without_a_receipt_still_reports_both_sides_unknown: `true`; the neighbouring falsification-Absent case still answers "?"/"?", so the new arm did not swallow it. CHECKER RECEIPT (#10028 branch binary 788ee9c, sha256 60e8f568...), root=src/v2 over base 22e3d70: before 39 blocking / after 38, resolved 2036 sources in both. BEFORE-ONLY is exactly `SemanticMismatch { actual: Rejected, falsification: Present }`; AFTER-ONLY is empty; no diagnostic remains in any file this change touches. The final tree reports 2038 sources because this change ADDS two witness modules. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u

… outside a test file REQUIRED-FLOOR REFUSAL cause=FloorDiscoveryRefused on run 33669954217 named exactly one file: src/v2/test/claim/self_host/native_agreement_label_probe.dag carried two `test fn` declarations while its name did not end in `_test.dag`, so floor discovery could not enrol them. The refusal is the correct one: a `test` declaration outside the discovered population is an inert probe that would be cited as coverage without ever executing. Renamed the file and its module to native_agreement_label_probe_test; both witnesses re-run green under the new module name (label_of_a_two_byte_primitive, and the empty-primitive control that still answers "?"). No behaviour change -- the probe body is untouched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TRH9V13en3PBh7UX7Qw71u

…72-j9-native-agreement-rejected

briansrls

APPROVE on exact head 24ded50. The uncovered SemanticMismatch { actual: Rejected, falsification: Present } arm is real, and narrowing the pure extractor from TestClaimRun to the Verdict it actually reads makes the arm directly witnessable without changing callers. The octet repair is not a rider: making the missing arm reachable exercises the existing formatter, whose declared Optional<Int> was fed Optional<Byte> and aborted on every present value; integer_u8_from_byte is the owned conversion. The negative, positive, and mutation controls discriminate both repairs. Content approved; merge waits on exact-head required checks and current-main composition.

…72-j9-native-agreement-rejected

… 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

…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

…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>

gunbc-ci-auto-heal and others added 2 commits September 2, 2026 18:52

gunbai-bot Bot mentioned this pull request Sep 2, 2026

First append after the ledger split moves two files, not three: file the declared-return-vs-generic-instantiation class #10124

Merged

gunbc-ci-auto-heal added 2 commits September 2, 2026 22:47

Merge origin/main (floor cost repair #10133)

c0c9521

Merge remote-tracking branch 'origin/main' into session/keen-ferret-1…

24ded50

…72-j9-native-agreement-rejected

gunbai-bot Bot mentioned this pull request Sep 3, 2026

See through nested patterns in the .dag exhaustiveness checker (13 sites surfaced, all closed) #10028

Merged

briansrls approved these changes Sep 3, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/keen-ferret-1…

30d5bfa

…72-j9-native-agreement-rejected

briansrls merged commit 38d76db into main Sep 3, 2026
7 checks passed

briansrls deleted the session/keen-ferret-172-j9-native-agreement-rejected branch September 3, 2026 17:09

Navigation Menu

Repository navigation

The native side can refuse, and the label that would report it aborts on any real value - #10109

The native side can refuse, and the label that would report it aborts on any real value#10109
briansrls merged 5 commits into
mainfrom
session/keen-ferret-172-j9-native-agreement-rejected

gunbai-bot Bot commented Sep 2, 2026

Uh oh!

briansrls left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Sep 2, 2026

THE OBLIGATION

THE FOLD'S SUBJECT IS THE VERDICT, NOT THE RUN

THE WITNESS FOUND A LIVE ABORT, AND IT IS THE LARGER HALF OF THIS CHANGE

EVIDENCE, ALL BY EXECUTION

CHECKER RECEIPT

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant