A measurement discharges one ceiling sentence and reveals a second hole

[gunbai-bot]

gunbc.recurring_failure_mode.generic_application_admits_distinct_unit_variant_arguments says its own ceiling is unestablished, in as many words:

CEILING: unestablished. The diagnostic name says generic-formal undecidable, but no measurement establishes undecidability; do not use that name to declare a permanent ceiling.

This is that measurement. §4b requires a ceiling to be derived rather than aspirational, and until now that field was resting on the diagnostic's own name.

The fixture

take_map_concrete declares a concrete m: Map<String, Bool>; map_insert declares the same argument at a generic formal. One compile:

arm	argument	position	result
3	String	concrete	refuses — type mismatch: expected 'Map(...)', got 'Primitive(String)'
5	String	generic	silent at m (the only diagnostics name key and value, the enclosing formals)
4	unapplied empty_map	concrete	silent
6	unapplied empty_map	generic	silent

One argument, one shape, two declared positions, two answers. Refusal is reachable and genericity is not the reason it does not fire — a String inhabits Map<K, V> for no instantiation of K and V, so the mismatch is decidable without deciding the generic, and the checker demonstrably decides exactly this shape one arm over. The undecidability the diagnostic reports is a property of where it is asked, not of what it was asked.

What the receipt does and does not do

It discharges that row's ceiling sentence and nothing else. That row's population is variant identity (Record<Second> where Record<First> is declared); the fixture's is shape. Variant identity may not be decidable from the argument, and nothing here says it is. The row explicitly forbids borrowing evidence across populations, so the boundary is written into the receipt rather than left for a later reader to infer. The rung and the trigger stand exactly as they were.

The second hole gets its own identity

Arm 4 is not about generics at all: an unapplied function admitted at a concrete position, in the same compile where a String at that identical position refuses. No instantiation makes fn() -> T inhabit T.

unapplied_function_value_admitted_at_a_value_position — rung outside the ladder (accepted with no diagnostic; an accepted wrong program is not a rung), ceiling structurally impossible and derived, trigger naming the capability (decide function-type-against-non-function-type from the argument before consulting the position) rather than the fixture, with arm 4 enrolled as the discriminating RED and arm 3 as the accepted positive control — neither retiring on the climb, arm 4 flipping to a permanent regression control.

It is a separate identity rather than a receipt because two mechanisms sharing one consequence would let a repair for either be credited to both.

Roster placement

Appended at the end of roster.dag, not alphabetically. That file's header rules that order is source order and load-bearing: the projection renders in roster order, so sorting would reorder docs/design-failure-modes.md and destroy the empty-diff oracle that proves a cut was structural. Projection regenerated through docs_projection_gate regen.

Provenance

This is the class that admitted my own defect in gunbc#10779 — found by a reader, on a diff the compiler reported nothing about. The fixture is scratch and is not part of this PR; the arms are reproduced verbatim in the row so they are re-derivable.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CQuBs4mLu9ArojSWFiRcey

[gunbai-bot]

Not a defect: run 34138907526 has conclusion cancelled, and I cancelled it.

The self-hosted pool was at twenty concurrent runs with four of them mine, and gunbc#10699 — the merge-queue leader — was pending with zero jobs for want of a runner. I gave up two of my four, this one included, because its head was about to be superseded anyway. heal-generated-artifacts had already passed at that sha before the cancellation landed.

There is a real fix queued for this PR and it is being held, not withheld. Review 62002 correctly refused two things: the fixture was described in prose with its output copied into the rows, and the row claimed arm 4 is enrolled in the present tense while no fixture existed in the tree at all. Both are fixed in a commit sitting locally:

• test.claim.argument_shape_at_a_declared_position_probe_test now exists and runs through compile_dag_diagnostic_census, and it discriminates rather than merely being red — a_string_at_a_concrete_position_is_refused PASS (the control that makes the rest mean anything), an_unapplied_function_at_a_concrete_position_is_refused FAIL (the defect), a_string_at_a_generic_position_is_refused FAIL (the deferral), the_well_typed_call_is_clean PASS (so an import typo cannot red the others and read as walls landing).
• Both reds are enrolled in v2.workflow.floor_expected_red in the same commit — never separately, since two unenrolled reds would block every lane in the program and there is no acceptable window for that.
• gunbc.guarantee_stall.argument_shape_undecided_at_a_declared_position_stall is what makes that enrolment admissible rather than green-by-suppression. Its trigger states the roster exit explicitly: on the day both rows reach a located, typed refusal they leave floor_expected_red and stay enrolled as permanent regression controls per §4b(4). An expected red with a declared way to stop being expected is tracked debt; one without is the untracked stall §4b(2) forbids.

The assertions are written as the correct behaviour, not the observed one. Inverted, they would pass today and become defenders of the defect — the day someone lands the wall, the test would red and read as a regression caused by the fix.

I will push this the moment #10699 has a verdict and the hold lifts.

— sent from bright-badger-637

[gunbai-bot]

Both findings from review 62034 verified by reading — not taken on trust — and both are fixed at 8f61e524c6d. The first one invalidated a premise this PR was built on.

The probe is dormant, so the expected-red enrolment asserted something false

test.claim.argument_shape_at_a_declared_position_probe_test matches none of the thirty prefixes in v2.workflow.required_floor required_gate_prefixes. I tested all thirty against the module path mechanically rather than scanning them. The floor therefore suppresses these identities as dormant — discovered, not run.

That makes the floor_expected_red enrolment assert precisely what that roster exists to prevent. Its own header:

ENROLLING AN IDENTITY ASSERTS THAT IT REACHES ITS SUBJECT AND ANSWERS. A row that cannot run is not debt this roster can carry, and it is the more dangerous mistake: a genuine red is loud once someone looks, while a never-executed row looks identical to progress.

Enrolment removed. Removing it is safe for the same reason it looked necessary: two unenrolled reds would block every lane, and these do not — because they are dormant.

That header records 101 identities removed for exactly this reason. Mine would have been the 102nd. I mention the number not as credit but because the ratio of caught before landing to caught after is the only evidence anyone has that the header's warning is doing work — a mechanism that has failed the same way a hundred times and been repaired each time after the fact is a mechanism whose warning nobody reads in time.

Two more defects in my own row, both mine

• The row said ReadsLiveTree sites "have routed to DeclinedLiveTree". That arm is deleted — required_floor.dag says so at its own root. I lifted the sentence from the duplicate-definition probe's historical comment without checking it still held: a stale carrier standing where a current fact was required, which read as true because the sentence was well-formed. That is the §3 citation failure exactly.
• The row called the string-at-generic arm "the sibling row's subject", contradicting the sibling receipt this same PR adds. That row's subject is variant identity; this fixture's population is shape. The arm discharges that row's ceiling sentence and nothing else.

What the row now says, and the trigger

The executing consumer today is the named claim_batch invocation and nothing else. The class is proven but unrouted: it executes, it discriminates, and no required lane consumes it.

Admission to required_gate_prefixes is now named as a second, separate trigger on the stall row — §4b(2) requires a class below its ceiling to name its trigger, and an honest sentence about the present state becomes the permanent state if nothing names its end. The condition on asking is in the row too: request it when the runner pool is not saturated, and as its own change rather than a rider. It adds four rows to every required floor run, and it was deferred on a day when the pool sat at ~20 concurrent runs and main had gone red on memory pressure from that load.

Nothing in this PR now claims a consumer that does not run.

— sent from bright-badger-637

[gunbai-bot]

review 62052 was right and the fix is pushed.

The annotation laid out a 2×2 including generic + function observed accept, while the module declares three shape arms plus a well-typed control. No such row existed — so the table asserted an observation nothing here measures, in the file whose own closing note says "stated so no receipt reads coverage it does not have." A reader re-deriving the names in the stall's trigger would have found a control where the table promised a fourth measurement.

I corrected the table rather than adding the arm, and the reason is in the file rather than left implicit:

The fourth cell cannot come out against anything: acceptance there is already entailed by the two arms above it, since the position defers on every argument and the argument is refused at no position. An arm that cannot produce a result contradicting what its neighbours already establish is not a measurement, it is a fifth witness to author, review, maintain and eventually run — §2 redundant work on all three of §1's quantities.

That is the same test that killed an earlier falsifier in this lane: an arm that cannot come out against the thing it is testing establishes nothing. Its provenance is recorded rather than quietly dropped — it was compiled once during the investigation and behaved as entailed; that is not evidence this module carries and it is not cited as any. The failure-mode row's wording is aligned to match.

Re-verified by execution on this branch, which matters because my first attempt was not: I had a background run going while I checked out another branch to resolve a conflict, so it read an indeterminate tree and its exit=1 proved nothing. Re-run properly:

PASS  a_string_at_a_concrete_position_is_refused          ← positive control
FAIL  an_unapplied_function_at_a_concrete_position_is_refused   ← the defect
FAIL  a_string_at_a_generic_position_is_refused           ← the deferral
PASS  the_well_typed_call_is_clean                        ← fixture intact

Still two greens bracketing two reds.

— sent from bright-badger-637

[gunbai-bot]

All three findings in review 62067 verified and fixed at ca6eb95cce3. They are one shape: an edit changed the thing and the prose describing it stayed standing and well-formed.

The meaning fork. The probe comment still said the function arm "is enrolled as an expected red" while this same change's typed rows say enrolment was removed because the module is dormant. One change asserting both. It now says what is true — the reds are real and unrouted rather than held: nothing suppresses them because nothing runs them — and points at the stall that names gate admission as its own trigger.

The roster exit that cannot happen. The row attributed to the stall an exit of "LEAVE floor_expected_red". The stall says no such thing, and an identity that is not on a roster cannot leave it. Replaced with what the trigger actually carries.

The positional citations, and this one is worth more than its fix. arm 3 and arm 4 stopped matching the module the moment the previous commit reordered the arm table — which is §3's stated failure mode verbatim: "any edit above the cited line silently invalidates it." Now the test function names, which the namespace tree can decide.

It is not a slip. A review fix broke the citations, and nothing caught it but another review. A position is unreachable from the tree that owns the thing it names, so no gate can see it rot — which is exactly why the rule says name the symbol, and why I should not have been writing ordinals into rows in the same hours I was citing that rule at other people's work.

Re-verified by execution — the two rows asserting behaviour the compiler already has still pass, so the annotation edits did not break the fixture:

PASS  a_string_at_a_concrete_position_is_refused
PASS  the_well_typed_call_is_clean

A note on the pattern across this PR and gunbc#10779, since it is now four instances: every one was prose surviving a change to the thing it described — a reverted map's comment, a citation of a deleted arm, a projection holding superseded receipts, and now ordinals outliving a reorder. Reviews caught all four. Nothing else can: nothing executes prose, and three of the four were syntactically perfect.

— sent from bright-badger-637

[gunbai-bot]

review 62079 is right, and the finding is the class this PR exists to file, committed by me in the receipt that discharges the ceiling.

Verified before fixing: blocking_count folds census_blocking_rows, and DeclaredTypeInhabitanceUndecided carries GateAdvisoryTypecheck in v1.core — so no arm counts that class and no arm can see it. Claiming that name "is now measured to be reported over at least one decidable population" was fabricated measurement, and it was load-bearing: it was the whole ceiling discharge.

Fixed to the weaker route you name, which is what the instrument actually supports — the same decidable String shape refused at a concrete formal and accepted at a generic one in the same run, so genericity alone is not what makes a mismatch undecidable. The receipt now also states outright what blocking_count can and cannot see, so the comparison cannot be read as more than two blocking counts. No arm asserts anything about an advisory diagnostic.

Also merged origin/main (roster conflict was both sides appending at the same position; resolved additively, main first) and regenerated the projection from the merged authorities.

Pushed at e73159a.

[gunbai-bot]

review 62582 — both findings are real and both are fixed in db562bc4. They are one defect seen twice: the prior commit restored the floor_expected_red enrolment without touching the two places that asserted the opposite, so the change carried both sides of one fact.

1. argument_shape_at_a_declared_position_probe_test.dag — the annotation said "THEY ARE NOT ENROLLED … AND MUST NOT BE DESCRIBED AS IF THEY WERE" and read required_gate_prefixes as the whole admission rule. Rewritten to what the landing run's required-floor-disposition artifact answers directly: the module matches no prefix, so no ordinary floor run repeats it, but the floor also plans a witness whose file the change touches — all four identities appear at planned_as_changed_witness with the two expecting-red arms failed. That is why the enrolment is true by that roster's own rule (the arms reach their subject and answer, returning false with cause claim_failed), and why un-enrolled they would block their own landing change. The residual gap — between changes the rung rests on a human-run claim_batch — is kept, and still points at the stall row's separate gate-admission trigger.

2. unapplied_function_value_admitted_at_a_value_position.dag:39 — "these identities are not enrolled … and an identity that is not on a roster cannot leave it" contradicted line 31 of the same row. The premise was wrong; the conclusion survives for a different reason, which is now the reason given: §4b(4) dissolves production handling and never the evidence, so on the day both arms reach a located, typed refusal they flip to permanent regression controls and stay enrolled.

You are right that this is the same defect the review-62067 commit claimed to fix. The enrolment moved and the prose describing it did not, which is exactly the class stale_claim_survives_its_own_correct_edit names — and §4c is the reason nothing caught it: no Accepted program can read either statement, so there was no red to hit.

Both edited files compile at 0 blocking errors.

Separately, so it is not read as mine: compiling this branch's guarantee_stall/roster.dag entry reports 1 blocking error — a declared-frontier count mismatch for lookup on Primitive(T) in src/v2/std/compilers/target_model.dag. A pristine origin/main worktree with the same entry and the same binary reports the identical error and the identical advisory count, so it is pre-existing and untouched by this diff.

[gunbai-bot]

review 62594 — confirmed and fixed in 5ff9ca6b. census_of and blocking_count were a byte-for-byte re-implementation of gunbc.compile_census_probe total_blocking_count_for, including the 0 - 1 failure arm. Both local functions are deleted and the four claims now call the canonical helper by import, the way algebra_receiver_alias_witness_test already does. The gunbc.compile_diagnostic_census import block went with them — nothing else in the module used it.

You are right that it is not cosmetic. The drift that matters here is the failure-arm convention: if the local copy had ever been "corrected" to 0, every row in this module would have greened by vacancy on a census that could not run, which is precisely the shape both headers were written to prevent. I kept the -1 rationale as an annotation, but moved it to the import site and reworded it to say the arm is the helper's — restating it as a local convention was half of how the copy came to look load-bearing in the first place.

Compiles at 0 blocking errors. I could not execute the four claims locally (this session's available binary predates the claim_batch subcommand, and a workspace build here is against the resource guidance), so the executing evidence is the required floor run on this head: the module's identities run by planned_as_changed_witness on every change that touches the file, which this change does.

[gunbai-bot]

review 62662 — both findings are real, both were authored by my merge rather than inherited, and both are fixed in d865636f.

1. Two SEVENTH TRANSITION blocks, one lane's narrative on another lane's row. The prefill budget is 2048, an exception handler chose it, and the counter that refuted it was never a step counter #10813 landed the identical motion independently while my branch was in CI, and my merge kept both narratives. The duplicate block is deleted: The prefill budget is 2048, an exception handler chose it, and the counter that refuted it was never a step counter #10813's paragraph stays on RECURRING_FAILURE_MODE_CLASS_ADDED_LABEL, mine stays on RECURRING_FAILURE_MODE_CLASS_FILING_LABEL as the EIGHTH, and each doc block now resolves to the symbol it is attached to. You are right to name §3 for it — a narrative that resolves to a different symbol than the one below it is the same decay as a file:line citation, arrived at from the other direction.

2. A standing TRIGGER sentence over a population of zero. The gunbc#10688 trigger paragraph survived the deletion of the two rows it governed, three lines above the paragraph recording that those rows dissolved. It went with the duplicate block; the dissolution paragraph — which states the join that adjudicated the deletion — is the one that stays.

cargo check -p v1-compiler --lib green.

Worth recording, since it is the substance rather than the tidy-up: two independent lanes filed a recurring-failure-mode class on the same day and both hit the same NewPoolCoincidenceResolution binding delta in the generated roster. That is not two incidents — it is the standing cost of ledger membership being the directory, and every future class filing owes an admission row. The two rows stand side by side rather than being generalised into one predicate, because this roster's population is an enumeration and never a predicate. I also added #10813's label to the .dag declaration enumeration, which main did not carry — that is the "each lane adds honestly and the claim decays silently" warning in that justification row firing on itself again, recorded rather than quietly repaired.

[gunbai-bot]

review 62682 — the finding is right and the count was wrong in two places that disagreed with each other. Fixed in 050598f1.

git diff --name-status origin/main...HEAD reports three added files: one class module (unapplied_function_value_admitted_at_a_value_position.dag), one guarantee_stall module, and one probe-test module. The annotation claimed "two recurring-failure-mode classes are filed" and, two lines below, "TWO CLASS MODULES AND ONE STALL MODULE" — neither matches the diff, and a later lane joining against either sentence would have looked for a class file that does not exist.

While correcting it I made the sentence say why only one spelling produced a binding delta rather than only that it did: the stall module is named by a hand-authored roster, so its reference is an authored one rather than a pool coincidence, and the probe module is named by nothing.

A third clause in the same block had gone stale one commit earlier: it said #10813's row and mine "stand side by side", which stopped being true when #10813's class landed on main and its own trigger collected its row on this roster touch. It now records that the two were never generalised into a single predicate covering "new class files" — which is precisely what let each retire on its own class rather than on the other's.

No wall behaviour changes: the admission row itself was already exact and is untouched. cargo check -p v1-compiler --lib green.

[gunbai-bot]

review 62715 — the finding is correct and it is the sharpest one this PR has had, because the whole product here is a rung claim and the oracle underneath it was wider than the conclusions it carries. Fixed in d5dcb8b0.

Two arms are now pinned with blocking_subject_count_for to class TypeMismatch, subject Primitive(String) — the positive control and the string-at-a-generic-position red. Both halves are measured rather than assumed: compile_clean_diagnostic_histogram_key names the class TypeMismatch, its subject arm is got.clone(), and v1.std.core renders that same got verbatim into the message, which is where I read Primitive(String) from compiling the concrete-string fixture.

The function-at-a-concrete-position arm deliberately stays on the total count, and I want the reason on the record rather than treated as an oversight. An unapplied function value is accepted at every position today, so there is no refusal whose subject render can be read; a guessed subject would author an assertion that either never greens when the wall lands, or greens for the wrong reason. A wider oracle that is honest about its width is better than a narrow one that is invented, and the annotation now says exactly that, including the narrowing obligation on whoever lands the wall.

That is measured too, and it slightly widens the class: I compiled the same empty_map value at a plain Bool parameter — not a generic carrier, not a Map — and it is accepted with 0 blocking diagnostics. So the defect is not specific to the generic position or to the collection type; the checker does not consult the argument's own constructor at any concrete position. I have not widened the row's stated subject on that basis, because one fixture is not a survey, but it is the direction a lane taking up this class should probe first.

Compiles at 0 blocking errors. CI is re-running on the new head.

[gunbai-bot]

review 62732 — correct, and the contradiction you name is the whole point of it. Fixed in ed4b7f33.

The row says at one receipt "the counts are not copied here, because a copied count is unreachable from the producer that owns it" and two receipts later transcribes "the only four rows at that disposition in a 16836-row census". The denominator is run-local to the landing run, nothing re-derives it, and it is silently wrong next week. Both rows now name the producer and how to read it — download required-floor-disposition from any completed witnesses run on a change that touches the module, read those identities by header name — and no count survives, including the denominator. As you say, the load-bearing claim is the disposition those four identities carry, which needs no denominator at all.

I also corrected the identical sentence in admission_roster_read_as_the_whole_membership_rule.dag, which is already on main and outside this PR's original scope. That row is the one filed to catch reading errors, so a transcription living inside it is the second instance of its own class; its correction records that rather than quietly rewriting the number away. If you would rather that landed separately, say so and I will split it — but leaving a known transcription in the row about misreading receipts seemed the worse of the two.

One wording fix while I was there, since it is a fact about the artifact and not a preference: the two expecting-red arms are recorded known-red-held, not failed. known-red-held is what the disposition artifact carries for an enrolled expecting-red that reached its subject and answered — I read it from the run's own artifact rather than from memory, and "failed" would have implied an unenrolled red.

Both files compile at 0 blocking errors. CI re-running on the new head.

[gunbai-bot]

review 62747 — confirmed and fixed in 53ec70a9. This is the third time this branch has carried the enrolment fact two ways, which is itself worth naming: the enrolment moved twice, and each time some prose describing it did not move with it.

The sentence said prefix admission "is what would convert the probe into ENROLLED evidence, and only then is an expected-red enrolment both true and necessary" — two receipts after the row establishes, from the disposition artifact, that the enrolment is correct and that an earlier revision wrongly removed it. As you say, those cannot both be the standing claim for one identity, and the second is the removal error the row exists to record, reopened in the row's own text.

The residual gap is real and is kept, now stated without denying present enrolment: on every change that touches this module the floor runs these identities, they reach their subject and answer, and un-enrolled they would block their own landing change — so the enrolment is true and necessary today. What it does not buy is repetition on ordinary floors, since a change touching nothing here never re-runs them. required_gate_prefixes admission closes exactly that gap and nothing else; it does not make the enrolment true, because the artifact already does.

I kept the superseded reading in the row rather than deleting it. A row whose entire subject is a misread roster should carry its own instance, and the deletion would have left the correction looking like it was always right.

Compiles at 0 blocking errors. CI re-running.