Repository navigation
The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares - #9560
Merged
Merged
Conversation
… for two compiles the roster shares gunbc#9477 made a shared memoized compile's fill a preparation cost rather than the first payer's, because a merge-blocking per-claim ceiling charged with an order-dependent number is a fact about discovery order and not about the tree. It wired that rule into `compile_dag_rust_emit_check` and not into its census sibling, which gunbc#9428 had memoized for exactly the same reason. One accounting rule, two homes, applied in one of them. MEASURED, not inferred. On main run 33131296988 (b6003a4) the floor refuses with `completed_over_cost_requirement=1` and `failed=0`: `test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_ and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any row of this file -- while the row demonstrably paid two shared compiles, being the first claim to reach both `green_named_authority_source` and `green_own_declaration_source`, each of which a later claim then reads free. Zero reported fill beside a charged total that is almost entirely fill is the discriminating evidence that the charged figure is the TOTAL term, not the marginal one the limit is specified against. Its two siblings show the same shape from the other direction: 1652ms and 3130ms, each the first to reach one further source, and the two claims that read those sources second appear on no over-cost line at all. THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row is grandfathered, no witness is withheld: the missing bracket is added, so a census MISS records its fill through the same accumulator the sibling memo writes and `run_claim_measured` performs the same split it already performs. Nothing is exempted -- the fill is still measured on the enforcing clock, still counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows have never emitted. Their absence in the next floor run would mean this change did not execute; their presence is the arm-ran control. The two forward-freeze receipts are corrected in the same change. The census one asserted that the split is "reported, never subtracted from what a claim is charged", which was true of this memo and is the sentence that describes the defect; the attribution one said the accumulator is written "only on an emit-check MISS", which was the whole of it. No declaration is added, so neither receipt's hand-item delta moves. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…s retry list snappy-dove-250 and sleek-cat-45 established that the fill subtraction covers exactly ONE shared artifact. Verified here by code read: record_shared_artifact_fill_cpu has a single call site, inside compile_dag_rust_emit_check, and the memoized sibling compile_dag_diagnostic_census (#9428) has no bracket -- so a census miss accumulates nothing and run_claim_measured subtracts zero for it. So the marginal rebuild fixed one artifact's attribution, not shared-build attribution in general. Sixteen of the 203 rows sit in a census-calling module and may be charged for work they do not own. They are NAMED rather than counted, because of the property that makes this roster's shape risky: a row frozen for cost that belongs to a shared build cannot take the roster's exit, since the exit is "make it cheap" and the cost is not its own to reduce. It would sit here looking exactly like debt, forever, and nothing would prompt a retry. A named list with a dated trigger -- when #9560 lands the census bracket, re-measure these sixteen -- is the difference between a declared impurity and a silent one. HOW TO READ SIXTEEN, stated in the carrier so it is not mistaken for a defect count: it is an UPPER bound on census-caused miswarding, since only the claim arriving first at a source absorbs the fill. It is NOT a bound on the general class -- both_closure_edge_index is the obvious next candidate and its treatment is UNVERIFIED, asserted in neither direction, per the finder's own caveat which I am not going to launder into a claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rd state as the one that must not exist The bracket in the previous commit fixes ONE instance. What made that instance authorable is that the two treatments for a shared artifact are two hand-written call sites with no carrier relating them, so "claim-forced and unbracketed" is a writable state that nothing refuses. THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED. Preparation-forceable -- every identity it can be asked for is knowable before the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index` is this arm, and the run reports `provenance=built-by-preparation` for both index identities the floor's resolves can reach. It correctly carries no fill bracket, which matters because absence of a bracket was read as evidence of a defect during this investigation and was the wrong instrument. Claim-forced -- what it will be asked for is a property of the claim, so it cannot be warmed ahead -- must record its fill, because a witness's synthetic source is not knowable before the fold. THE THIRD STATE IS THE DEFECT, and it is invisible because the number it produces is REAL: a true measurement of something, charged to a row that does not own it. Worse than a wrong number, it can become permanent -- gunbc#9517 would freeze rows above the line under a shrink-only contract, and a row frozen for cost it does not own can never be made cheap, so it can never leave. PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review diligence; the third state stays writable and this paragraph will not stop the next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing class and the warm-or-net treatment is DERIVED from it, at which point the third state has no spelling. That construction is not made here and is not claimed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…ver-cautious caveat The previous clause named it "the obvious next candidate" for unbracketed shared-build miswarding and left it UNVERIFIED. That was over-cautious rather than wrong, and over-caution here has a cost: it sends the next reader to measure something already correct. Confirmed by code read in this carrier rather than relayed: run_required_floor calls warm_bare_reference_edge_index TWICE during strict-preparation -- over the source roots and over witness_layer_roots() -- reporting cost as [floor-phase] phase=shared-index-warm. Both index identities the fold can reach are built and billed before any claim window opens, so the artifact needs no bracket and its ~28s reaches no row on this roster. Runtime confirmation on run 33135617689 is sleek-cat-45's and is attributed as theirs; the warm sites are this carrier's own reading. Replaced with the well-posed successor, which is sleek-cat-45's framing and is a construction question rather than a roster one: an artifact is either PREPARATION-FORCEABLE (warm it, bill preparation) or CLAIM-FORCED-ONLY (net the fill, report the split). The census memo was in NEITHER arm, and that "neither" is a writable state is the actual defect -- #9560 closes one instance, the next memoization reintroduces it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
6 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…loor refusal on this branch predates
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…predates #9560 The three failing checks on 4d22d6d started 01:10-02:10Z, so refs/pull/9521/merge was computed against main as it stood before ba27746 (#9560) landed. That base no longer exists. A rerun replays the pinned ref and would reproduce the red exactly; only a push forces recomputation. The trigger for pushing was a settled, non-cancelled witnesses run on a head containing #9560: run 33140335064 on ba27746, with required-witnesses-build, required-witnesses-floor and witnesses all green. No content change. The tree is byte-identical to 4d22d6d. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 28, 2026
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…population as a monotone debt contract (#9517) * Restore the operator's 500ms per-claim ceiling; freeze the population that accumulated under the 10x drift The ceiling was set to 500ms by operator ruling at #8283 (2026-08-17) and was never repealed. It was raised twice in 18 hours, and neither raise had a ruling on the value: 500 -> 1552 (#8514): justified only by "measured-max plus one scheduler quantum" over the then-current tree. That is the tree-copied oracle DESIGN section 5 forbids -- the ceiling was set to whatever the slowest witness happened to cost, which is a change detector, not a budget. Its own comment said "not an open slack ratchet"; it ratcheted 3.2x eleven hours later. 1552 -> 5000 (#8533): cited "operator ruling 2026-08-19" on both clocks. That ruling was about SPLITTING CPU from wall. The operator's quoted words in the diff -- "DO NOT set CPU and wall to the same 5000ms" -- presuppose 5000 was already on the table, so it is a ruling about the mechanical copy and not about the magnitude. The value rode in as a passenger, which is the authority substitution failure mode DESIGN names. CPU returns to 500. Wall goes to 2000, derived from the population it must not trip rather than as a multiple of the CPU figure: over the 11,572 rows within the CPU budget on run 33109071348 the worst wall was 1037ms. The diagnostic cost line moves 1552 -> 100 because at 1552 it became unfireable under a 500ms ceiling -- permanently green by construction, which section 4b calls worse than absent. 320 witnesses exceed 500ms (54.7% of the fold's CPU over 2.7% of its rows). They are frozen in v2.workflow.floor_cost_debt and WITHHELD FROM EXECUTION. Not relocated: the files do not move, because relocation to a long/ home is the move the 2026-08-04 admission ruling forbids and gunbc.witness_deferral_freeze exists to close -- it deletes coverage while retaining the source with nothing counting the loss. The difference here is that the withhold is declared, counted every run, identity-grain and shrink-only. Coverage for those 320 rows is GONE while they sit there, and that is declared as a section 4b(3) rung drop (mechanically preventable -> outside the ladder) rather than described as a deferral. A row leaves by being made cheap and having its line deleted; the roster is self-correcting, since a row wrongly included proves itself by passing under the ceiling once released. A rostered identity the tree no longer carries BLOCKS (stale_cost_debt), so the roster cannot rot into a permission slip. The withheld population itself does not block. Verified: cargo check clean; v1_src_dag_parse reports 4203 files parse-clean. The five preemption_reachability assertions still hold at the new limits (60317 > 500 trips the same arm; 42 is inside both). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Withhold at claim-build as a fourth decline, not as a skip inside the fold The first cut withheld cost-debt rows with a `continue` at the top of the execution loop. That form would have red the floor on its first run, in two places, and a code review approved it: ClaimIdentityCountsDisagree -- planned == executed + not_attempted is exact, and 320 planned claims that neither executed nor published as not-attempted break it. TerminalLedgerIncomplete -- every planned identity must appear exactly once in the terminal population, and a withheld claim produces no terminal row. A third partition (SitePartitionInexact) guards the site level. All three are the fail-closed design working: a `continue` at the top of a fold is exactly the shape that leaves a partition behind. So withholding moves to claim BUILD time as a fourth RequiredFloorDisposition arm, DeclinedCostDebt, alongside the long-home and live-tree declines. A withheld row never becomes a planned claim, all three partitions stay exact, and the fold builds no scope and allocates no frame for it. Cost debt is ordered LAST among the declines. A row that already declines for a home reason keeps that decline, never enters the cost-debt reverse join, and surfaces as a STALE roster row -- which blocks, and whose diagnostic says to delete the line. Ordering it first would silently convert a stale row into a permanent, plausible-looking withhold. The fourth arm made three Rust matches and two .dag folds fail to compile, which is what discovery_census's own comment says it is for ("A FOURTH DISPOSITION ARM MUST FAIL TO COMPILE IN THIS FOLD"). MEASURED INTERACTION, and it is a real fork rather than a tidy-up: 7 identities sit in both this roster and floor_expected_red, and leaving both claims standing blocks in EITHER direction. Withheld and still enrolled, the expected-red reverse join calls them stale. Un-withheld, they exceed the 500ms ceiling and ExpectedRedArm explicitly refuses to hold an interrupted budget outcome, so they land as failures. All 7 measure 561-3010ms, so none can execute inside the ceiling. Cost debt therefore wins: enrollment in floor_expected_red asserts the identity REACHES ITS SUBJECT AND ANSWERS, and a withheld row answers nothing, so the roster that yields is the one making a claim the run cannot support. The enrollment is dormant, not deleted, and the suppression is counted per roster rather than silent. Verified: cargo check clean; v1_src_dag_parse 4203 files parse-clean. One annotation had to move to module-item grain (DESIGN 4c) -- the parse sweep caught it, cargo did not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore the 100ms warning tier beside the 500ms hard error, ranked and bounded Operator ruling 2026-08-27: a warning over 100ms, a hard error over 500ms. The hard error is required_floor_claim_cpu_safety_limit_ms, already restored. The warning is required_floor_claim_cost_line_ms, already re-pointed to 100 -- so the pairing was in the tree; what was missing is that the print was unbounded. WHY THIS IS NOT THE WARN TIER DELETED ON 2026-08-20, stated in the code so a reader who recognises the shape does not delete it again. That tier was a second threshold on the SAFETY DEADLINE -- an admission mechanism -- and "over a threshold, reported, allowed to finish" is the widen DESIGN section 5 forbids of a failure arm. The cost line is not a failure arm: it judges only completed claims, nothing reads it to fail a run, and a row it names has already been admitted and has already answered. Warning and hard error are two mechanisms here, not two tiers of one. RANKED AND BOUNDED. At a 100ms line the population is ~835 rows on the measured corpus, and this file already carries the receipt for what that does to a log: the prior 5000/10000 pair "fired on the MEDIAN witness (several hundred [floor-witness-slow] lines)". So the print is the 25 most expensive, ranked on the declared cost basis, which is the actionable head of a distribution whose median is ~1ms. The cap is not silent (DESIGN section 5): the dropped count is printed and the complete population is in the per-claim cost TSV this run uploads. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the collapsed whitespace in the stale-cost-debt diagnostic Two reviewers flagged this independently and I initially assumed it was a false positive, because the neighbouring strings in the same change use `\` line continuations correctly. It was real: this one was written without them, cargo fmt collapsed it to a single physical line, and the indentation survived as literal padding -- "so" followed by eighteen spaces followed by "nothing". Cosmetic, but it is the text of a BLOCKING refusal, which is the one diagnostic a person reads at the moment the run stops. Now uses `\` continuations like the other two strings this change added, both of which were checked and were fine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Import floor_cost_debt into required_floor so the roster is in the frame the host evaluates it in CI refused: floor refused: floor_cost_debt_roster: no declaration named 'v2.workflow.floor_cost_debt.floor_cost_debt_roster' in this execution's loaded index The host evaluates each roster by qualified name in required_floor's frame, and that frame's scope is this module's closure, so a roster with no import edge is not in the world the frame was built from. THIS IS THE FOURTH TIME. required_floor.dag already carries three paragraphs about it, ending: "every new roster the host evaluates in this frame must be remembered here by whoever adds it, and the failure surfaces only from a full CI run." That prediction was exact, including the cost -- a ~30 minute fold, on a change whose entire subject is the cost of folds. Four occurrences is a defect in the mechanism, not four careless authors, and the note now says why the prose cannot hold it: a reader adding a roster is thinking about the roster's CONTENT, while this edge is a fact about the FRAME the host will evaluate it in. Different grains. The structural repair the file already names -- the host deriving reachability from the qualified names it calls -- is what deletes this list and these paragraphs together; this change adds the fourth data point for it rather than attempting it here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rebuild the roster on MARGINAL cost: 119 of the 320 were never expensive snappy-dove-250 asked whether the figure this roster's universe was discovered by is a claim's marginal cost or its charged cost. It was charged, and the answer changes 37% of the population. `v1_compiler.cli_run` `run_claim_measured` began SUBTRACTING shared-artifact fill from a claim's charged CPU at gunbc#9477, which landed 18:49. This roster was measured from run 33109071348 at aea5e0d, 15:34 -- three hours earlier. So every figure behind the first cut was a CHARGED figure, in which whichever claim touched a shared artifact first was billed the whole fill. MEASURED, not estimated: of the 320 identities the first roster held, 119 measure at or under 500ms once fill is attributed to the artifact instead. The extremes are the tell -- test.claim.alias_identity_across_unwrap_witness a_second_alias_still_emits_its_own_name_and_not_the_first was the SECOND most expensive row in the corpus at 4250ms charged, and its marginal cost is 0ms. It never cost anything. That is the failure this change exists to prevent, committed by the change itself: freezing a working witness at identity grain under a shrink-only contract, on a number that was real and measured the wrong subject. It would have looked correct from the inside forever. The universe is now discovered from main run 33131296988 (b6003a4), the first completed floor measurement after #9477: 203 identities. Counts corrected with it -- expected-red overlap 7 -> 6 (521-3865ms marginal), the 100ms warning population ~835 -> ~924, and the withheld-row count in the summary comment. WHAT SURVIVES THE CORRECTION, checked rather than assumed: test.claim.live_deploy.emit is still the most expensive module in the corpus at 85.5s marginal across 53 rows -- 10.7% of a 13.3-minute fold -- so the "one emission recomputed 53 times" diagnosis was robust to the basis change. And the row currently refusing main (callable_candidate_ambiguity_witness.neither_green_source_refuses_and_neither_mis_resolves) is in the new roster by name. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the bounded impurity the marginal basis does not fix, with its retry list snappy-dove-250 and sleek-cat-45 established that the fill subtraction covers exactly ONE shared artifact. Verified here by code read: record_shared_artifact_fill_cpu has a single call site, inside compile_dag_rust_emit_check, and the memoized sibling compile_dag_diagnostic_census (#9428) has no bracket -- so a census miss accumulates nothing and run_claim_measured subtracts zero for it. So the marginal rebuild fixed one artifact's attribution, not shared-build attribution in general. Sixteen of the 203 rows sit in a census-calling module and may be charged for work they do not own. They are NAMED rather than counted, because of the property that makes this roster's shape risky: a row frozen for cost that belongs to a shared build cannot take the roster's exit, since the exit is "make it cheap" and the cost is not its own to reduce. It would sit here looking exactly like debt, forever, and nothing would prompt a retry. A named list with a dated trigger -- when #9560 lands the census bracket, re-measure these sixteen -- is the difference between a declared impurity and a silent one. HOW TO READ SIXTEEN, stated in the carrier so it is not mistaken for a defect count: it is an UPPER bound on census-caused miswarding, since only the claim arriving first at a source absorbs the fill. It is NOT a bound on the general class -- both_closure_edge_index is the obvious next candidate and its treatment is UNVERIFIED, asserted in neither direction, per the finder's own caveat which I am not going to launder into a claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * both_closure_edge_index is settled and is not a defect: correct the over-cautious caveat The previous clause named it "the obvious next candidate" for unbracketed shared-build miswarding and left it UNVERIFIED. That was over-cautious rather than wrong, and over-caution here has a cost: it sends the next reader to measure something already correct. Confirmed by code read in this carrier rather than relayed: run_required_floor calls warm_bare_reference_edge_index TWICE during strict-preparation -- over the source roots and over witness_layer_roots() -- reporting cost as [floor-phase] phase=shared-index-warm. Both index identities the fold can reach are built and billed before any claim window opens, so the artifact needs no bracket and its ~28s reaches no row on this roster. Runtime confirmation on run 33135617689 is sleek-cat-45's and is attributed as theirs; the warm sites are this carrier's own reading. Replaced with the well-posed successor, which is sleek-cat-45's framing and is a construction question rather than a roster one: an artifact is either PREPARATION-FORCEABLE (warm it, bill preparation) or CLAIM-FORCED-ONLY (net the fill, report the split). The census memo was in NEITHER arm, and that "neither" is a writable state is the actual defect -- #9560 closes one instance, the next memoization reintroduces it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The wall clock condemned the rows the CPU clock exonerated: re-derive it, and complete the census FIRST EXECUTION OF THIS MECHANISM (run 33136345225) -- the fold reached my code for the first time in seven attempts and the two predicted lines landed exactly: "roster withholds 203" and "floor_expected_red: 6 suppressed". Partitions all exact (planned=executed=terminal=11794), failed=0, stale_quarantine=0, stale_route_gap=0, stale_cost_debt=0. Thirty rows failed, and they are TWO populations needing opposite fixes. SIXTEEN FAILED ON WALL WITH CPU INSIDE THE CEILING, and that is my defect. run_claim_measured subtracts shared-artifact fill from CPU and does NOT subtract it from WALL, so a first-touch payer reads ~0ms CPU and carries the whole shared build on the wall clock. Specimen, same row and same run: alias_identity_across_unwrap_witness.a_second_alias_still_emits_its_own_name_and_not_the_first reports marginal_cpu_ms=0 fill_cpu_ms=3772 with wall_ms=3782. The CPU clock exonerates it; a 2000ms wall clock condemns it. For the same work. The 2000ms figure was derived by the right method from the wrong population: it was measured BEFORE the roster was rebased onto marginal cost, when a fill payer carried a large CPU figure and was therefore excluded from the "inside the CPU budget" population the derivation reads. The rebase moved those rows into it and I did not re-derive. Same class as the charged-basis roster, one clock over. Re-derived on the corrected population: max wall among rows at or under the 500ms CPU ceiling is 3859ms (33131296988) and 3782ms (33136345225), so 8000ms clears the worst legitimate payer by ~2x while still catching the 504-SECOND stuck-claim specimen this clock exists for. Its next-rung trigger is netting fill out of wall as it already is out of CPU, at which point the figure re-derives downward against a population that no longer contains these rows. FOURTEEN FAILED ON CPU and are added: seven INTERRUPTED at 501-508ms having never reached a verdict, seven completed over. 203 -> 217. That is the initial census completing rather than the roster growing: a row cannot be discovered as over-ceiling by a measurement taken under a ceiling ten times looser, so the population was only fully knowable once the ceiling it is defined against was the one actually running. From here the direction is shrink-only in earnest. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The wall figure is a declared interim, not a derived ceiling — a derivation filtered by the quantity it derives cannot see its own worst case Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Wall stays raw: netting fill out of the safety deadline would delete the only detector over the region it is blind in Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The roster is empty and keyed on marginal: withholding a charged-basis row moves its fill to the next claim instead of removing it * Delete the duplicated required_floor import line in the census witness carrier (review 57129) * The trailing rung-drop note named no subject: fold it above a declaration (DESIGN 4c) * The preemption fixture's wall input equalled the live wall limit: decouple it so the CPU arm is provably the sole cause (review 57138) * The fixture-home disposition witness matched three arms of a four-arm coproduct * Enroll the 266 over-budget identities, measured on main where the ceiling cannot mask them 220 expensive passes (verdict reached, outcome pass, cpu 511..3757ms) plus 46 rows too expensive to reach a verdict at all (44 budget-interrupted on cpu, 2 over-budget on wall at ~19s). Read from main run 33141550579's per-claim cost receipt and from warm-tern-34's identity-grain list, never from this branch: measuring cost under the tightened ceiling perturbs the quantity, and a first attempt that did so clustered every interrupted row at 501..505ms and would have laundered six live main failures as cost debt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the observed fill relocation, the two fill formats, and the three-way split * Close the model/host disposition divergence review 57235 found: the cost decline is an identity fact, not a module fact The modeled required_floor_site_disposition took only module_path, so it could never produce DeclinedCostDebt. The fold declined 266 identities by name while gunbc.discovery_census called every one of them Planned, and two Rust comments cited that function for a precedence it did not carry. Worse, a witness in this branch ASSERTED the divergence as a contract (w_site_disposition_never_answers_cost_debt). It is inverted rather than deleted: three rows now check the arm is produced, that an unrostered sibling in the same module stays Planned, and that a home decline outranks cost debt. The mixed_sites fixture gains a real roster member, without which the partition assertion passed at 0 == 0. Also: the floor_cost_debt header said CURRENTLY CARRYING NO IDENTITIES while the population block below it said 266; and the change had no SeedGrowthJustification row, now gunbc.floor_cost_debt_seed_growth, recording both the item delta (+1) and the line delta (+252/-12). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist the fixture annotation to module-item grain (DESIGN 4c) The note explaining the new roster-member site sat inside mixed_sites()'s body, which the parse sweep refuses at four located diagnostics -- one per line. Hoisted above the declaration, and the neighbouring note corrected from three disposition arms to four. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the reference_edges relocation at its consuming module: 268 rows, and the non-termination argument was false calm-ram-380 predicted, from main's fill attribution joined against this roster, that merging as-is would relocate a ~26s reference_edges bill from four withheld payers onto the two rest_path_reaches_no_cli members the roster did not hold. Confirmed at identity grain on the branch run: both breached (59817ms completed-over-budget, and an interrupt at 27939ms against 500ms). Both are now enrolled, closing the module 8/8. The remedy they proposed -- preparation warms for reference_edges as a prerequisite -- is not needed, and the field that decides it was in the line being quoted. consumer_modules is 1 on every claim-paid reference_edges line in both runs, so the bill cannot leave the module and enrolment terminates by exhaustion. The broad keys are already warmed: module_path_index fills 70826ms across 454 claims / 109 modules as paid_by=<outside-fold>. Warming is done exactly where breadth made a first-toucher unaffordable; what remains claim-paid is narrow. This refutes this file's own argument that enrolment is STRUCTURALLY non-terminating. Corrected in place, bounded per key rather than universal, with an explicit note that a broad claim-paid key would behave the old way and would need the warm. Also records how the false universal survived two supports that looked independent: a general claim, and a relocation receipt equally consistent with the claim being false. A receipt that cannot discriminate the general case from the bounded one corroborates nothing about scope. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restate the interrupt-point receipt without quoting the string gunbc#9599 deletes floor_cost_debt.dag quoted the old INTERRUPTED-BEFORE-VERDICT rendering verbatim -- 'at least 5002ms' -- in two places, as the receipt for why an interrupt point is not a cost. gunbc#9599 gives the bound its own named field (interrupt_point=) and renders the cost field as UNMEASURED, so both quotes would name a string that no longer exists. Repaired so the paragraph survives that merge in either order: the mechanism is stated, the new field name is referenced, and the superseded wording is not quoted. Quoting it would have been a citation rotting the day it was written. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Stop transcribing the roster size: one stale count found, five more behind it review 57254 found claim_executor.rs stating 217 rows where the carrier header says 268. The fix is not to re-transcribe. The roster is a function, its size is a property of that function, and a numeral in prose is a second representation that rots on the next enrolment -- so the numeral is dropped and the authority named. Sweeping the class found five more, all in the carrier, all left behind when the header moved to 268. They split two ways and the distinction is the point: HISTORICAL (kept, and now anchored): 'withholding 266 rows left 16 others tripping' is a measurement against the roster AS IT STOOD AT THAT RUN. That figure is correct and must NOT track the current size; updating it would silently restate what was measured. LIVE CLAIMS (de-transcribed): four clauses describing the CURRENT roster, including the 4b(3) bounded-population declaration. A roster function is bounded by being finite and enumerable; a transcribed size is not what makes it so. 268 now appears only in the two header statements the file designates as where the count lives. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Nullary variants take bare patterns: True {} never matched, and 11 witnesses died on it The disposition added for review 57235 matched `True {} =>` / `False {} =>` against v2.std.logic's `type Bool = True | False`. Nullary variants are matched bare; a record pattern against a fieldless variant matches no scrutinee, so every call fell through at runtime. It parses. It typechecks. It dies at execution with cause=pattern-match-failure, which is why three parse sweeps and a clean build lane all passed over it. Found by reading the cancelled floor job's log, not by any check. Blast radius was wider than the edit: 11 of 19 test fns in discovery_census_witness_test.dag errored, including several that never call the disposition -- they went down through the shared census fold. So 'witnesses unrelated to my change are failing' was not evidence the cause lay elsewhere. grep -rn 'True {}' --include=*.dag over 4243 files returns exactly one hit: this one. Zero precedent in the corpus was the tell. Also in this batch, closing review 57258's Population B finding: the roster is now floor_cost_debt_proven_roster() (221, reached a verdict and passed, marginal CPU over the ceiling) and floor_cost_debt_censored_roster() (47, preempted before a verdict, own cost UNMEASURED), unioned. The header had asserted the proven case over the whole roster -- written when the carrier held only proven rows, never re-read when the censored ones were enrolled, and contradicted by the population block below it. Withheld population verified unchanged at 268 unique identities. No second decline arm is minted: a disposition names an admission outcome and the answer is the same for both classes. Evidence strength is a different axis, and a second arm would make the host re-decide what the roster already answers. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Branch the native Bool with if: the True/False arms never matched, proven by a discriminating control 873a618 changed True {} to True and fixed NOTHING -- the braces were never the defect. still-cat-738 measured through the real binary that a record pattern against a genuine nullary variant (A {} over type T = A | B) matches fine, and that True/False over the corpus Bool fails in BOTH spellings. The mechanism: std.types declares type Bool = True | False but Bool is realized NATIVELY as a machine scalar, and v1_interpreter match_pattern's VariantPattern arm handles Variant/Record/List/Str/Int/Null with no arm for Value::Bool, so those patterns fall through to None. v2.std.algebra any matches its own result as lowercase true/false, and every corpus consumer branches with if. CONFIRMED BY EXECUTION, not inferred. Two runs of the same invocation through gunbc run: match True/False -> cause: PatternMatchFailure { value: "true" } if/else -> evaluates, refused only at the ProcessExit boundary The control establishes that evaluation happens and the ProcessExit refusal is post-evaluation, so the clean arm is evidence rather than an absence of evidence. value: "true" is the native bool in plain sight. I had proposed a parser wall refusing nullary record patterns. It would have had ZERO true positives, made working code unwritable, and -- worst -- refused this text, sent me to the bare spelling, and produced the same runtime failure with a wall standing as evidence the class was handled. still-cat measured before building, which is the only reason it did not land. Also closes review 57268: witness_floor_workflow.dag transcribed the wall limit as (2000) when it is set elsewhere in this same diff -- a fresh transcription rot inside the diff that reworks a fixture to prevent exactly that. Both parenthesised values are dropped and the constants named. Two more of the class fell out: the preemption fixture's receipt carried the live figure in present tense while recording that it had already rotted twice, and my own first repair re-transcribed all three values while explaining why not to. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close rest_path_reaches_no_cli at 12/12 from source membership, not from a log The floor completed (run 33172726547): withheld_cost_debt=268, stale_cost_debt=0, planned=executed=12684, interrupted_before_verdict=11, completed_over_cost_requirement=3. The mechanism works; the conjuncts did not empty. One of the 11 is explained outright. dropping_the_definition_edge_roster_ surfaces_more recorded 'cost at least 28769ms' and paid cache=reference_edges fill_ms=25995 -- ~90% of it a bill four withheld siblings used to pay. It did not become expensive; it inherited. I had declared this module closed at 8 members. It has TWELVE. The count came from identities two floor logs happened to print, and a log names the claims that RAN AND REPORTED, never a module's membership; the authority is grep -c 'test fn' on the module source. The termination argument was sound and its INPUT was wrong. All four remaining members are now enrolled, so the module is closed at 12/12 and the roster is 272. Because consumer_modules=1 on that key, with every member withheld no claim reaches the artifact at all -- the fill STOPS HAPPENING rather than relocating to a thirteenth. That is what exhaustion buys. Recorded: why three independent tests looked for this fill and none could see it. Its disposition is EXCLUSIVE and disposition is computed as consumer_modules > 1, so the run's shared_fill_ms=727 -- a real figure, correctly summed, verified here at 725 over 4 rows -- bounds CROSS-MODULE relocation only, a population this 25995ms fill is not in. A paid_by- difference test over warmed keys cannot see it either (outside-fold in every run, cannot differ by construction), nor can a census of which REFUSED rows are shared (an inheritor is the sole payer, hence exclusive, and it completes or is interrupted rather than being refused). Three tests agreed while sharing one blind spot. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enrol four verified cost rows; record that the ceiling lands inside a dense band The 12/12 closure is confirmed by execution (run 33191118450): reference_edges now carries no claim-paid key at all, only outside-fold warms, so the 25995ms fill STOPPED HAPPENING rather than relocating, and its payer left the interrupted set. Relocation is dissolved. Four rows enrolled, each verified at a ceiling that lets it finish (run 33190645319, same tree, ceiling only): operation_argv 520ms PASS, per_language_ratchet 646ms PASS, inert_carrier 1146ms PASS, scan_denominator 23794ms COMPLETED_OVER_BUDGET. Roster 276. Seven other residual rows were REFUSED enrolment after the same check. Cost makes a row a candidate; outcome makes it eligible. Six of the interrupted are in main's 47 unexpected failures -- inherited defects that a 500ms ceiling makes present as interrupts because they never reach the verdict that would report the failure. Enrolling them would have put broken witnesses into a roster whose proven class asserts the witness works. Both readers had the outcome column and framed the set by expense. Three more were refused and are NOT new failures: two are KNOWN-RED on main and one is NO-ROUTE. The 47 are UNEXPECTED failures, so an enrolled red and a hermetically-refused row are outside that population by construction. Absent from the 47 is not the same as new. Recorded, unresolved: the counters rose 11->12 and 3->5 from rows paying NO fill. Four bootstrap_footprint siblings sit at 492/502/502/506ms against a 500ms line, and an earlier run had two of them at 512/502 -- membership is decided by run-to-run variance. Exact counts: 21 rows at 400ms, 15 at 450ms, 8 at 500ms, 4 at 600ms. Per-row enrolment cannot converge at a threshold inside a cluster, and moving the line is an operator decision this carrier records rather than pre-empts. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm exercised one of them. The near miss that hid it: `[A,A]` answered
`[A,A]` DOES refuse correctly as repeated-observed, so the obvious fixture finds
nothing. Only the answered-once case slipped.
REPAIRED AT TWO LAYERS, and the receipt shows neither substitutes for the other:
- `ObservationRepeatedExpected`, checked FIRST. The other three arms are
statements ABOUT a question set and are meaningless without a well-formed one;
answering "missing" here names the OBSERVATION as the defect when the ROSTER
is, sending a consumer to fix the wrong artifact.
- `prove_repair_roster` refuses a duplicate outright, so a `ProvenRepairRoster`
cannot HOLD one -- construction at the mint rather than validation at the join.
The generic arm is NOT dead after the proof-side wall: the law is key-generic and
`legacy_binding_observation` derives its expected list with no proven roster, so
the arm is reachable from that consumer's denominator. A quiet guard, not a
decoration.
MUTATION RECEIPT, two independent mutations in sequence (not overlapped):
deleting the law's check reds 2 arms and leaves the proof arm TRUE; deleting the
proof's refusal reds only the proof arm. Unmutated, 24 arms green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Carry the repeated-expected arm into the two binding witnesses the new variant also made non-exhaustive
`ObservationRepeatedExpected` landed with arms added to the repair envelope and
its witness, and NOT to the two binding witnesses that match the same
key-generic law. Six matches, one arm each.
WHY IT REACHED CI: the local check was `v1_src_dag_parse`, which returned
`4210 file(s) parse-clean` and was read as evidence the tree was well-formed.
Exhaustiveness is a RESOLVE-time judgment, so a parse sweep can never see it --
parse-clean and resolves are different claims about different phases, and the
green one was not about the thing being changed. The verification is now a
resolve of each affected witness, which reproduces the six diagnostics when the
arms are absent and passes when they are present.
The variant refusing every exhaustive match across three files is the substrate
doing its job -- nothing could have silently kept the old vocabulary. What
failed was my check, not the wall.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
* scm: a typed read-command result that names no destination (#9443)
* scm: a typed read-command result that names no destination
Recut onto current main so the diff matches the scope this PR claims.
WHY THE RECUT. The previous composition reached main through the save
branch's ancestry, so it carried repository_save.dag and its witness --
neither of which is on main, and both of which belong to #9434, which is
draft. Merging this PR would therefore have landed the parked save half
as a consequence of branch topology rather than as a decision anyone
made. Nobody would have done anything wrong; the ancestry would simply
have outranked the park.
The park is respected rather than routed around. No convert_to_draft
event exists on #9434 and draft is not this tooling's default, so the
hold is unexplained rather than accidental -- and the correct response to
an unexplained hold is to leave it standing.
WHAT REMAINS, and why the load refinement is not scope creep: splitting
RepositoryLoadRefusal out of RepositoryLoad is what lets
ScmReadRepositoryUnavailable carry a refusal that CANNOT hold a success.
Without it this module's unavailable arm would be constructible holding
RepositoryLoaded, with nothing to refuse the pair. It is the enabling
half of this change, not a neighbour travelling with it.
The dependency runs one way, checked before cutting: the save witness
imports RepositoryLoadRefused, and nothing read-side references save. So
dropping save costs this PR nothing.
Both keystones return `true` on this tree over current main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Drop the refusal-path accessor: the third instance of a shape this PR
documents as twice-removed
`repository_load_refusal_path` had exactly one occurrence in the tree --
its own definition. No consumer, so DESIGN section 6 residue.
WHAT MAKES THIS WORSE THAN ORDINARY DEAD CODE: read_command.dag's own
header, in this same PR, cites this exact helper shape being removed
twice before -- once as `checkout_succeeded`, once from
`gunbc.scm.ancestry` under review 56207 -- and states the reason that
survives. This change re-added the third instance while documenting the
first two. Neither a lens nor a green run can see that; only reading the
two files against each other does.
The surviving rationale in the deleted comment block was about the TYPES
(why no `loaded: Bool` exists), not about the accessor, so it moves to
`type RepositoryLoad` rather than being deleted along with the function.
A prose row removed for one reason must not silently take its contents
with it.
It gains the reason the shape keeps recurring, which was written down
nowhere: with no consumer the accessor is residue, and WITH one it is
worse -- a fourth refusal arm would be absorbed by the projection instead
of failing to compile at each site that must decide about it.
Both keystones return `true` after the deletion.
Reported by review 57012.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Enroll the three read-command route gaps the floor actually reported
The floor reported route_gap_unenrolled=3 on this branch, all three in
scm_read_command_witness, all with one cause:
the hermetic route has no arm for Read (operation declares no
mock_response)
scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer
scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log
scm_read_command_keystone_holds
Same boundary already recorded for the load witness: extdeps.filesystem
declares no mock_response, so the hermetic frame has no arm for a FAILING
read. All three claims exercise the absent-repository path, and the
keystone inherits the gap by composing them. They pass under `gunbc run`,
which performs the real read; they cannot reach their subject hermetically.
MEASURED, NOT PREDICTED. These were foreseeable and were deliberately NOT
pre-enrolled: enrolling an identity that does not gap is a stale row and
reds the build, which is what stale_route_gap counts. The rows are added
now because a run reported these exact three identities.
Enrolment records the gap as known debt. It does not make the gap
acceptable and it is not a fix: the remedy is a hermetic arm for a failing
read, which belongs to the filesystem boundary and not to this PR.
Roster 112 -> 115; the module still evaluates and returns its list.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Anchor a relative source root the same way in both module-index builders (#9548)
* Anchor a relative source root the same way in both module-index builders
The two builders disagreed on how a relative source root resolves:
try_build_module_index anchored through anchor_source_root (process
workspace), while try_index_source_root_into_module_index read the string
straight off the filesystem (process CWD). One concept, two answers,
selected by which builder a caller happened to reach.
The fork survived because the one place it is observable is the one place
nothing was asserting: every CI invocation runs with its CWD at the
workspace root, where both spellings denote the same directory.
A root that cannot be anchored still falls through to the existence
refusal with its ORIGINAL spelling, so the diagnostic names what the
caller asked for rather than a rewritten form they never wrote.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Trigger a fresh merge ref against main after #9551
The merge ref is computed when the head is pushed, against main as it was
at that moment; main moving afterwards recomputes nothing, and a RERUN
replays the original pinned ref. #9551 landed the four emit mirrors after
this branch's last push, so its base predates the regen fix.
Empty rather than a local merge of main deliberately: main's change here IS
the generated mirrors, and merging it locally would mean hand-resolving
emitted files -- the one state the regen gate forbids. Pushing recomputes
the base without touching them.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Measure the fan decoder's execution identity, and refuse to call it bound (#9536)
* Instrument the decoder's execution identity by composing two things that already existed
gunbc.bmc_fan_program_interpretation modelled a decoder identity and refused to author
one, because both digests are properties of an execution and a hand-written pair would
be two literals typed by whoever typed the decoder -- agreeing because one person wrote
both, and continuing to agree after the thing they describe changed. This produces them
from an execution instead, which is what an operator adoption needs: a corrected decoder
that assigns different meaning to the same bytes must be distinguishable from a refactor
that assigns the same meaning.
NOTHING IS MINTED. Both halves were found by searching before building, which is why
this module is short:
v2.lens.module_graph import_closure_live enumerates the entry's closure
tools.multi_module_compile_fixture compile_fixture returns a structural digest over
the (path, content) vector AND the
running compiler binary's own hash,
both host-computed from what ran
ONE NEAR-MISS IS DELIBERATELY NOT REUSED, and it is recorded so nobody "fixes" this by
adopting it. std.interface_summary typed_module_key is exactly the right shape -- a
source key combined with compiler identity -- at the wrong grain: its module_key folds a
module's source hash with its DIRECT IMPORT INTERFACE hashes. A body-only change in a
transitively imported module leaves it unchanged while changing what this decoder
produces; std.decimal canonical_exact_decimal could be rewritten and the key would not
move. It answers "may I reuse a cached typecheck"; this answers "is this the same
reader". Borrowing the first to answer the second invents the entailment rather than
misstating any fact.
THE DISCRIMINATING PAIR IS MEASURED, both halves, because an identity that moves on
everything and one that moves on nothing both look fine from a single run. Baseline
3282f082abc9d722 over 40 modules; one comment line added to std/decimal.dag, inside the
closure, moved it to 9bcfbd782022b120; one comment line added to gunbc/fleet_fan_wiring.dag,
outside it, left it byte-identical to baseline. Both restored byte-exactly. The compiler
digest held across all three.
The second half is the one worth having: a digest over the whole tree passes the first
test and is useless, since every unrelated edit would invalidate an adoption.
WHAT IS NOT CLAIMED. There is no enrolled witness, and the reason is structural rather
than neglect: the instrument reads the live tree and takes about four and a half minutes,
so the floor planner declines it, and the mutation half would have to edit tracked
source, which no hermetic witness may do. The evidence is a recorded measurement with its
controls -- weaker than an executing one, and said so rather than dressed up. The
next-rung trigger is a fixture-grain closure the instrument owns, at which point the pair
becomes an ordinary witness.
Cost is recorded too, because it decides where this may run: the closure walk alone is
about 4m28s. On demand only; nothing here is enrolled in a required lane, and a
four-minute live-tree walk on every push would be the corpus-denominated cost that gets
paid by every consumer wanting something else.
* Report the identity as measured-but-unbound, because nothing here proves the decoder ran on this vector
The side-chat raised the objection that matters and it is right. This instrument
enumerates a closure, hashes that exact vector, and compiles it. It does NOT execute the
decoder against that vector -- a semantic program digest is produced by some other run,
through the interpreter's own resolution of the same entry. Pairing this identity with
that digest would be two individually correct observations with an invented arrow
between them: the same fake join removed from the capture observer on #9299, one level
up.
The two subjects are very probably identical, since the walk follows the same import
edges the interpreter resolves. "Very probably" is what the objection is about. Nothing
here proves the interpreter received this vector and no wider one.
So the standing is not handed out from here. DecoderIdentityEstablished is what lets a
consumer treat two readings as same-reader, and granting it from a run that did not
perform the reading would restore the unbound claim under a name that reads as bound.
The binding is now its own three-state carrier, the measured-but-unbound arm names its
own gap, and the standing derived from it is still the absent one.
That is the instrument reporting what it has rather than failing. The obligation is
NARROWED rather than discharged: what was missing was any producer at all; what is
missing now is one execution that both hashes its source vector and runs the decoder
against that exact vector, returning the identity and the semantic result together.
That trigger is recorded on the arm.
* Sharpen the binding trigger to name the missing host capability
Looked rather than assumed, and the gap is larger than 'finish the instrument'. Two
routes could bind the identity to a decode and neither is reachable today.
EXECUTE-THE-VECTOR: the seed registers exactly one fixture builtin,
compile_dag_multi_module_fixture, which COMPILES a supplied (path, content) vector. No
builtin evaluates one. So running the decoder against that exact vector needs a new host
surface -- v1 seed growth, which the freeze admits only in service of the v2 self-host
program, and this is not that.
PROVE-THE-SUBJECTS-EQUAL: nothing exposes the RUNNING program's resolved module set.
module_declaration_facts reads the source tree, which is the same authority the closure
walk already consumed, so comparing the two would compare a reading against itself rather
than against what the interpreter received.
Recorded at this grain because a trigger that reads as small invites someone to just
finish it, find the capability absent, and close the gap with an argument instead -- which
is the invented arrow this carrier exists to refuse.
* Consume the decoder declaration instead of re-minting it (review 57069)
A byte-identical DeclarationRef for the decoder stood in this instrument
beside gunbc.bmc_fan_program_interpretation fan_program_decoder, which is
the module declaring the standing the instrument exists to discharge --
and which this module already imported from, so consuming it costs one
import member. Two authorities for one fact can drift independently
(DESIGN section 3); worse here than in general, because a drift would
identify a reader other than the one whose standing is at stake.
The entry PATH stays authored and is not the same fork: a module path
does not carry which source root stores the module, and deriving one
needs an observed ModuleStorageIndex rather than a pure transform. The
annotation now says so, so the next reader does not read the surviving
path as a missed half of this repair.
Measured after: identity unchanged -- 40 modules,
source_closure=3282f082abc9d722, compiler_runtime=f2c179fb7e10d373,
the same values the pre-fix baseline reported.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Say that the typed_module_key grain claim is an argument, not a measurement
The note asserted as fact that a body-only change in a transitively
imported module leaves typed_module_key unchanged while changing what the
decoder produces. The reasoning is sound and has now been endorsed by two
reviews and one external adjudication -- which is exactly why it needed
correcting rather than leaving: convergent readings of one argument are
not independent evidence about that argument, and an approved PR carrying
an unmeasured claim stated as fact is the rung inflation DESIGN 4b(1)
names as worse than sitting low.
I tried to measure it and found the route blocked, so the note now carries
that instead of the assertion. The only live producer of import interface
hashes is v2.lens.interface_summary module_key_for_rel_path. It has zero
consumers in the corpus; the first attempt to run it refused with
export_signature_facts `empty authored type name` on
extdeps.shell.credentials env_credential -- a pattern returning an
anonymous record, one of three such declarations. So that lens's live path
is inert in the DESIGN section 6 sense: the machinery exists and the first
exercise of it does not work.
Authoring the two export lists by hand was rejected rather than
overlooked: the claim IS that a body edit leaves the exports equal, so
asserting that equality assumes what the control exists to establish.
Next-rung trigger recorded on the note. Identity re-measured unchanged
(40 modules, source_closure=3282f082abc9d722).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Delete three commentary String rows and the digests they transcribed (review 57083)
The review flagged typed_module_key_grain_note, decoder_identity_
discrimination_note and decoder_identity_cost_note as the section 4c
pattern DESIGN discourages -- pure prose duplicating the // blocks above
them -- and noted broad corpus precedent for it. Precedent is the reason
to fix it in new code rather than the reason to keep it: adding fresh
instances of a discouraged pattern because the corpus is full of them is
how a discouraged pattern becomes the convention.
DESIGN is stricter here than the remark was. Two of the three rows
transcribed digests and a wall time into prose, inside the very module
whose entry point re-derives them, which is the standing "name the
instrument, never transcribe its output" ruling and not merely commentary
debt. So the numbers are gone from the // blocks too. What survives is
the SHAPE of the controls, which does not rot: an edit INSIDE the closure
moves source_closure, an edit OUTSIDE it leaves it byte-identical, both
restore. Anyone wanting the figures runs report_decoder_identity, which
prints them with the module count.
The // blocks are kept where they carry irreducible rationale -- why
typed_module_key is the wrong grain, why no hermetic witness can hold this
pair -- which section 4c permits and which the String rows were only
restating.
Re-measured after: unchanged, 40 modules, same digests the instrument
prints.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Witness evidence integrity: an undeclared live_tree_disposition silently declines the module — make silence REFUSE, burn down the 338, then the staged DeclinedLiveTree root deletion is safe (#9471)
* The live-read derivation detects a quarter of the readers it would have to replace
`v2.std.live_tree`'s note named the nightly affected-set falsifier as the thing
that catches a row declaring `SubstrateInputsOnly` while reading live state.
That cadence was deleted by the floor cut (#8283) and the repository carries
three workflows, none of which runs a predict-only cold comparison. The same
note stated the undeclared fail-closed default as THE fact, while the required
floor's own scan defaults the identical silence the opposite way -- so a reader
asking what happens to a witness that declares nothing was told the half that
withholds it, and the consumer that actually executes admits it.
What survives as the backstop is `effect_reach_derived_reads_live_tree_for_entry`,
and it does not derive this fact. It answers host-reading only when two
INDEPENDENT existentials both hold somewhere in the import closure -- some file
carries a repository path literal, some file carries a host-sink call shape --
so a closure that performs a real `Filesystem.Read` and names no path answers
false, and two modules that never call each other supply the two halves between
them. The ceiling is filed as a §4b row on the derivation's own authority, with
its next-rung trigger naming the capability (call-reachability-grade per-witness
classification) rather than an artifact that would contribute to one.
The evidence is a planted pair rather than a corpus count: two fixture entries
differing by exactly one import edge whose only content is a path-literal row,
performing a byte-identical read. The positive control derives host-reading; the
sink-only entry does not. Authored both sides, so the red is a property of the
derivation and cannot be dissolved by corpus drift.
The consequence runs opposite to the standing objection that an authored
disposition duplicates a derivable fact. `reads_live_tree_effective` consults the
declaration FIRST and reaches the derivation only for a row already claiming
SubstrateInputsOnly, so the derivation is the sole thing between a lying row and
a predict-skip. Replacing the declaration with it would be a scope narrowing
wearing a construction argument.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* The derivation's third bound: an unreadable closure file is skipped toward ADMIT
Confirmed by reading effect_reach_derived_reads_live_tree_for_closure_paths: a
closure file that cannot be read hits a bare `continue`, leaving both flags as
they were. Every unreadable file therefore biases the accumulation toward false,
which biases toward admitting a row that claims SubstrateInputsOnly -- the one
arm that could notice its own blindness discards it, in the direction that
weakens the only thing standing behind a lying declaration.
It compounds the empty-adjacency bound rather than sitting beside it: where the
closure is the entry alone, one failed read leaves the loop having seen nothing.
And unlike the conjunction and the adjacency, which are properties of the corpus
and measurable today, this one is a property of the run, so its magnitude is
whatever the filesystem did that time and nothing records it.
Found by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Route the ceiling row onto the ladder vocabulary instead of a prose blob
Review 56493 observed that the §4b class row was a large `String`, which §4c
names as misplaced data, and reported that no typed §4b carrier existed to route
into. One does: `gunbc.guarantee_rung_drop` declares the closed `GuaranteeRung`
vocabulary, and `gunbc.hermetic_mock_fidelity` already files a discovered class
in exactly this shape -- typed rung and ceiling, closed-coproduct reasons, and
rationale left in annotations beside the row.
So the row follows that pattern rather than minting a class of its own. The three
bounds become a closed coproduct, because naming them is what lets the class be
recognised a second time; enforcement becomes two reachable arms rather than a
sentence; and the next-rung trigger is DERIVED by a total function over the
coproduct rather than stored, which makes a trigger-less row unwritable instead
of merely checked. That all three bounds derive the same trigger is the finding,
not a redundancy: the capability replaces the approach rather than patching a
term.
The record is named for its subject. No corpus-wide §4b carrier exists, and
minting one from a single instance would put a second authority beside
hermetic_mock_fidelity -- the ladder VOCABULARY is the part that must not fork,
and that is what is reused.
Verified by execution: `gunbc compile --entry src/v2/std/effect_reach.dag`
returns 0 blocking errors, 21 files emitted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record that stamping the silent population was built and dropped
A future reader who finds the fail-closed default and the 24.7% backstop
measurement will reach for the obvious move -- stamp every silent witness file
-- and there is nothing in the tree telling them it was already tried. It was:
520 files stamped, silence made a typed located refusal on both consumers, then
discarded because the floor's decline arm was already being deleted at its root,
which is what made a truthful ReadsLiveTree stamp cost coverage in the first
place.
The note records the reason rather than the fact, because the reason is what
transfers: the arm's deletion is the enabling event for a truthful stamp, not
its reward, and the question revives when the selection consumer acquires an
enforcement it currently lacks -- not when the silent population grows.
Suggested by swift-badger-524, who observed the work would otherwise be visible
only in a reflog and one message.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Sweep the dead-cadence enforcement claim from all three of its homes
One claim lived in three places: v2.std.live_tree's disposition note, the same
module's stamp_provenance row, and a mirrored comment above
parse_entry_live_tree_disposition in cli_run.rs. Each said the nightly
affected-set falsifier catches a row declaring SubstrateInputsOnly while reading
live state. falsifier.yml was deleted by the 2026-08-15 floor cut. Correcting one
home leaves the other two as authorities for a false claim, so all three move
together.
The stamp_provenance row gets more than a past tense, because its consequence is
specific: the 2026-07-11 batch is machine-vouched rather than author-vouched and
inherits the deleted classifier's blind spot -- a live read hidden behind an
import was invisible to entry-text scanning. Those stamps were admitted on the
promise that a cadence would catch them if wrong. That promise is now UNMET, not
merely unfulfilled: nothing verifies a stamp, and one that was wrong the day it
was written is still wrong and still unobserved.
Three other authorities carry the same claim and belong to other owners; they are
deliberately not in this diff.
Verified: gunbc compile --entry src/v2/std/live_tree.dag -> 6 files emitted,
0 diagnostics.
Sites located by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Turn the supply fold from an honest screen into a real cross-mode selector: the six inputs supply.dag names as missing (#9472)
* wip: cross-mode supply selector
* wip2
* wip3
* wip4: duration state, commitment horizon
* review: fail-closed unbounded-duration availability, quote billing basis projection, Second-typed axis params
* witness: choose the window that the previous fold actually admitted
* Answer the new affordability arm in the sibling fabric witness suite
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids (#9564)
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids
Review 46148 ruled that absence is established by a successful listing and never
by a failed read. The ruling was written as a `data ... : String` note, which
DESIGN section 4c calls commentary no `Accepted` program can read -- and it was
then violated in gunbc.deploy_transition, authored beside the note, where a
present-and-unreadable marker rendered as absent and so as PERMITTED at the belt
seam (#9561). A note is not a mechanism.
extdeps.filesystem.filesystem_io gains a carrier with one mint.
FilesystemEstablishedAbsence is sole_constructor; its only mint takes a
FilesystemDirectoryListing, itself sole_constructor and minted only from a
listing whose success channel was true. A module deciding absence from a read
alone has no value to return and no way to build one. filesystem_entry_presence
and filesystem_file_observation are the folds: presence is decided by the
listing, the read is consulted only for an entry the listing named, and every
way of not establishing absence lands in one indeterminate arm.
Consumers, so this is not a carrier with no consumer:
- gunbc.roadmap_verification_receipt, both walks. Already correct by hand; they
now consume the carrier instead of restating the rule, and their private
second spelling of List's wire encoding is deleted for
filesystem_listing_names_entry.
- gunbc.devboot.build read_text_file,…
Merged
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…ransfer and retirement are fused (#9521) * File a contradiction between two authorities: DESIGN records a climb trigger for the pair the hollowing plan schedules for deletion DESIGN records the regen host's hand-written ordering at *mitigatable* with "the host being derived from the carrier" as its next-rung trigger. `gunbc.plans.cli_run_hollowing_plan` carries a row whose subject is exactly that pair -- authority `v2.workflow.required_regen` / `v1_compiler.required_regen_host` -- and dispositions it `delete-with-v1`, trigger "Wave 4 real-fixpoint cutover", adding "bulk GENERATED cutover, not piecemeal". One authority asserts a climb, the other schedules a deletion, neither cites the other, and nothing refuses over the pair. This carrier records that and nothing else. It is not a repair, not a plan, and not a proposal for the Wave 4 work: resolving the contradiction means editing DESIGN against a plan, which is an operator decision. It gates nothing and says so, since a carrier named for a wall while occupying none is inflation (DESIGN 4b). Three findings, all measured: 1. THE AUTHORITY RELATIONSHIP IS A COMMENT. `required_regen_run` and `required_regen_sync_admission` occur exactly once across all of src/v1/stage0/src/*.rs, and the occurrence is prose naming the carrier as authority for an ordering. No production Rust calls into it; its only executor is its own witness. That is specification-without-execution on the production path, and it explains the divergence better than the host's Vec<String> refusal channel does -- 23 production refusal sites covering ~21 distinct states against six named by the carrier is what a comment-held correspondence produces given time, because nothing ever forced the two together. 2. THE TRIGGER HAS FAILED THREE PRECONDITIONS, each found only by attempting the step the previous one unblocked: the carrier sits in a tree the regen closure does not root; a relocated carrier still needs a seed-side consumer that does not exist; and the only honest candidate consumer is hand-Rust already scheduled for deletion at the same gate. A trigger nobody can satisfy is worse than a declared stall -- 4b(2) exists to separate "cannot climb" from "can climb but unbuilt", and this row reads as the second while being the first, so it never ranks and never retires. 3. CLOSURE MEMBERSHIP IS BY IMPORT, NOT BY RESIDENCE. The control table carries both arms -- two modules with seed importers, emitted; three with none, not emitted -- so precondition two is checkable by the next reader rather than re-derivable only by trying it. The witness makes the record self-invalidating: it asserts the trigger is unsatisfiable, so repairing a precondition turns it RED and forces the census to be revisited instead of decaying silently. It declares SubstrateInputsOnly explicitly, because the fail-closed default would make it ReadsLiveTree and DECLINED -- discovered, counted, never executed -- which is exactly the inert decoration this census warns about. Both control arms are asserted in each direction plus an anti-vacuity check, since either arm alone passes over an empty table. Verified by execution: 0 blocking errors for both modules, contributing zero advisory diagnostics of their own. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Wave 4 lacks a total disposition for the required-regen obligation: transfer and retirement are fused Recut of this PR's original claim, which overreached in two ways. Both were mine and both are removed rather than softened. WHAT THIS NOW CLAIMS. `gunbc.plans.cli_run_hollowing_plan` carries one row -- authority `v2.workflow.required_regen` / `v1_compiler.required_regen_host` -- dispositioned `delete-with-v1` at the Wave 4 cutover. That row answers for two different futures with different obligations: TRANSFER, where the operation survives under a successor and owes an equivalence receipt, and RETIRE, where the operation ceases and owes proof its subject is empty. Both end in deleting the same two files, which is why one row can cover them and why nothing notices that it does. `delete-with-v1` states the ACTION and leaves the JUSTIFICATION unstated. The plan may still choose retirement. What it may not do is let `delete-with-v1` stand in for PROVING the subject retired. THE ASYMMETRY IS THE CONTENT. The host is one realization, so a transfer moves its work to the successor and a retirement ends it -- both admit deletion. The carrier is the operation's DEFINITION, so deleting it under a transfer destroys the referent of the very equivalence receipt that transfer owes. Only retirement admits it. A symmetric pair of predicates would be the fused row again in typed clothing, so the witness asserts the two must DISAGREE under Transferred and AGREE under Retired. WHAT WAS WRONG BEFORE. 1. THREE FAILED ROUTES ARE NOT AN IMPOSSIBILITY PROOF. The original concluded the trigger was unsatisfiable and the class could not climb. The evidence licenses only CurrentSeedImportDerivationUnavailable. "Host derived from carrier" does not require the host to import a Rust type generated into the v1 stage0 closure; that is one construction, and it is the one refuted. Four others -- build-time generation, interpreting the carrier and passing a typed receipt, moving the operation to the promoted v2 product, and the operation retiring with its subject -- are reachable and UNEXAMINED, and are now enumerated as such. This was the same equivalence-across-a-gap this lane had already caught itself making about the closure stubs. 2. COMMENT-HELD CONFORMANCE IS NOT ABSENT ENFORCEMENT. The grep establishes that no production Rust CONSUMES the carrier. It does not establish that required-regen behaviour is absent: the hand-written host is an INDEPENDENT REALIZATION and it does enforce the operation. The honest pair is OperationEnforcedByIndependentRealization with CarrierRealizationConformanceUnobserved. What is missing is a mechanically enforced RELATION between two realizations, not the enforcement, and that changes both severity and repair. 3. DESIGN AND THE PLAN ARE NOT NECESSARILY CONTRADICTORY. A next-rung trigger is an obligation while its subject remains LIVE, and a terminal migration may remove the subject entirely -- deleting an operation whose subject is gone is retiring it, not declining to climb. They are compatible under exactly that condition, and nobody had checked whether it holds. The unchecked condition is the defect; the arbitration request between the two authorities is withdrawn. WHAT SURVIVES, with its measurements: the seed-import route is genuinely unavailable (closed two-variant regen roots, zero emitted files declaring a v2.* source module, and the both-arms closure-membership control table showing membership is by import rather than residence); carrier/host conformance is comment-held, at a cost of 23 production refusal sites covering ~21 distinct states against six the carrier names; and the plan's row is not total. The witness guards the specific overclaim that caused this recut: if anyone later marks every derivation route refuted, the impossibility claim returns silently, so `witness_exactly_one_route_is_refuted` and `witness_no_impossibility_claim_is_reachable` go red instead. One gap stated rather than papered over: nothing detects the plan GAINING a disposition later, so that half remains review diligence. Verified by execution: 0 blocking errors, contributing zero advisory diagnostics of its own. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Convert the carrier's prose to annotations and its receipts to typed obligations (§4c) Addresses review 57011 (REQUEST_CHANGES, narrowly on §4c). Both findings verified against the code and both fixed rather than argued. FINDING 1 -- the two `data ...: String` notes were hoisted prose. Correct, and the precedent I had followed does not excuse it: I modeled this carrier on `gunbc.whole_corpus_compile_admission`, which uses the same pattern on main. §4c records that hoisting comments into `data ...: String` rows was itself the failure (#6262), and that the first cleanup it forced swept 215 dead prose rows across ~130 files (#6424). An existing instance is not a licence. Both notes are now `//` annotation blocks, which is the sanctioned quarantine channel, and the module carries zero commentary String rows. The machine-consumed counts the review asked to be lifted are now a typed row, `ConformanceDivergence`, with the site count and state count as separate members because two states refuse at two sites each -- a site total read as a state total overstates the divergence. `conformance_divergence_is_observed` derives the verdict rather than storing it, so the finding EXPIRES LOUDLY: if a conformance relation later lands and the carrier names every state the host refuses, the witness goes red instead of the census standing as a claim about a state that has ended. FINDING 2 -- the String payloads on the coproduct arms. The review called these less severe; they were the load-bearing half, and fixing them made a case testable that had been unrepresentable. `Retired` carried free-form `*_empty_receipt: String` fields, which can ASSERT discharge without exhibiting it. It now carries `discharged: List<RetirementObligation>` over a closed two-member vocabulary, and `retirement_fully_discharged` requires both. So a retirement that names itself while discharging only one obligation now admits NEITHER deletion -- which is this carrier's own thesis enforced one level in: naming a disposition is not proving it. That case could not be written before, so it could not be tested; `witness_partial_retirement_admits_neither_deletion` covers it now. `RouteRefuted` / `RouteUnexamined` are payload-free. Each route is a named `data` declaration with its reasoning in a `//` block above it, so the rationale sits in the channel §4c sanctions and where a reader actually encounters it, rather than in a string nothing consumes. WHAT DID NOT CHANGE: the lifecycle coproduct, the asymmetric admittance pair, and the witnesses the review found well-modeled. The asymmetry is still asserted as a DISAGREEMENT under Transferred and an agreement under a fully discharged Retired, because separate assertions are satisfied by a pair that answers false to everything -- the fused row again in typed clothing. Verified by execution: 0 blocking errors, contributing zero advisory diagnostics of its own (7 sources, 12 files emitted, 95 advisories all from the shared std closure). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve the transcribed conformance counts and the retirement predicate, and split transfer by what the successor replaces Review 57020 raised two findings and both are correct. The five conformance counts were transcribed off a live-tree scan with no instrument naming them -- the 2026-08-24 ruling's exact prohibition. The repair is not to re-source them. The standing this carrier needs is qualitative: has a conformance relation been observed at all. The predicate that consumed the counts answered false regardless of whether they were current, so the numbers could rot without changing any decision, which is the evidence they were not carrying one. They are replaced by a typed RealizationConformance whose live value asserts an ABSENCE of observation and therefore owes no instrument. Conformance is modeled as its own axis rather than an arm of the lifecycle, because the operation's fate and the state of the relation between its realizations are independent questions. The retirement predicate was a hand-rolled Bool over a closed coproduct. Rather than respell it, the state that made it necessary is gone: a partially discharged retirement is now its own arm, Retired carries nothing, and the predicate dissolved rather than being reformulated. This also removes a state with no meaning -- Retired with an empty discharge list was neither retired nor prepared. Separately, a defect of my own found before review reached it: the transfer arm carried a successor AUTHORITY while denying carrier deletion, so the carrier encoded a terminal state in which two definitions answer for one operation. Split into RealizationTransferred (carrier stays canonical) and AuthorityTransferred (both delete), with a witness asserting the two DISAGREE, so re-fusing them in either direction goes red. Verified by execution, not by compiling: all seven affected witnesses return true, against an oracle first shown to discriminate by a planted false control. Compiles 0 blocking / 95 advisory, unchanged baseline. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the control table's transcribed magnitude, keeping the distinction its consumers actually read Review 57043 approved but noted that the closure-membership control table reintroduced transcribed integers in a file that elsewhere retracts them. Measured against the consumers rather than argued: every reader tested seed_importers == 0 or > 0, so the MAGNITUDE was read by nothing and a row could drift from one importer to seven with no witness changing. That is the same test this file applies to the conformance counts a few declarations up -- a member that can rot without changing any decision was never carrying one -- so the magnitude is deleted rather than defended as a fixture. The field becomes seed_reachable: Bool, which is the zero/non-zero distinction the rule actually turns on and a structural fact about the import graph rather than a measurement of a population. emitted stays a stored Bool because it IS read directly: it is the observed consequence the control exists to pair against reachability. Expressing reachability as a coproduct was considered and rejected -- filtering on it would have required a match returning true for one arm and false for the other, which is the predicate-dissolution shape review 57020 objected to. All three affected witnesses verified by execution, not by compiling. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Force a fresh merge ref: this PR's checks were pinned to a base that predates #9560 The three failing checks on 4d22d6d started 01:10-02:10Z, so refs/pull/9521/merge was computed against main as it stood before ba27746 (#9560) landed. That base no longer exists. A rerun replays the pinned ref and would reproduce the red exactly; only a push forces recomputation. The trigger for pushing was a settled, non-cancelled witnesses run on a head containing #9560: run 33140335064 on ba27746, with required-witnesses-build, required-witnesses-floor and witnesses all green. No content change. The tree is byte-identical to 4d22d6d. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Absorption was fused into AuthorityTransferred, and its incompleteness was one symbol over two owners The carrier exists to name a fused disposition, and it fused one two levels in. ABSORPTION IS A THIRD CONTINUATION. An obligation can survive while ceasing to be an INDEPENDENTLY NAMED operation, performed as one inseparable part of a broader transaction. That is not an authority transfer: a transfer hands the operation to a successor that still answers for it by name, while absorption dissolves the name and owes a COVERAGE receipt over every old input population, ordering guarantee, refusal and consumer obligation. WHY THE COMPLETED ARM ALONE WOULD HAVE BEEN A DECORATION. A completed absorption has the same deletion truth table as an authority transfer -- the absorber is canonical, so both files go -- so an Absorbed arm on its own changes no predicate outcome and no witness over it can go red for the right reason. The INCOMPLETE state is what makes it a wall: coverage that has not been demonstrated admits NEITHER deletion, which authority transfer never does. AND INCOMPLETENESS ITSELF SPLITS, IN TWO, WHICH IS THE ARM COUNT AND ITS REASON. An unproduced coverage receipt is an ABSENT OBSERVATION -- the absorber may cover everything, the remedy is to produce the receipt, owned by whoever lands the absorption. A receipt that SHOWS a gap is an observation with a negative result -- the remedy is to widen the absorber or refuse the absorption, owned by whoever owns the broader operation, and the design is wrong. Opposite owners, opposite repairs: DESIGN's not-applicable-rendered-as-malformed conflation. The two AGREE on both deletion predicates, which is exactly why collapsing them is tempting and exactly why a truth-table test cannot see the split. THE PRECEDENT IS IN THIS FILE, AND IT IS NOT THE ONE FIRST PROPOSED. A peer suggested retirement's three arms as precedent for distinguishing kinds of incompleteness. Checked: they are MirrorPopulationStillOccupied / RequiredConsumersRemain / BothObligationsOutstanding -- subsets over two named obligations, not kinds of incompleteness. The analogy fails and did not carry the split. What carried it is that this module ALREADY separates absent-observation from negative-result twice: RouteStatus (RouteRefuted vs RouteUnexamined) and RealizationConformance (unobserved vs observed). Collapsing absorption's would leave one module speaking two vocabularies about one concept. NO THIRD ARM. "Absorber not yet identified" is not a coverage state -- an obligation with no named absorber is Active, not absorbed. THE SPLIT IS READ, NOT MERELY DECLARED. Without a consumer, AbsorptionCoverage would be the richer name over an unchanged wall this module objects to elsewhere, so absorption_coverage_is_refuted answers the question whose two states have different owners. EVIDENCE, EXECUTED. Six witnesses green. Mutation: fusing prepared absorption with authority transfer on the carrier axis (one arm, false -> true) turns the disagreement witness and the closed-vocabulary gap sweep RED, while the agree-on-deletion-differ-on-refutation witness correctly stays green because it tests the other axis -- evidence the witnesses are not restatements of one assertion. Carrier restored byte-identical to its pre-mutation bytes and both reds return to green. ONE ANNOTATION RECORDS A WORKAROUND FOR A FILED PARSER DEFECT. The parser refuses a newline between the parameter list and the return arrow, at ANY name length -- executed on a controlled pair, a one-character name with the break refuses and the same name with the arrow on one line compiles clean. A test fn name here is therefore short in order to keep the ARROW on one line, not because short names are preferred; the defect is filed and owned elsewhere. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* The floor's demand and its supply selection are one join, and select_supply gets its first caller
select_supply has been complete and unconsumed since it landed. This module
is the join: the required floor's own Work becomes a Demand, and the candidate
roster is ranked by the authority that already knew how, rather than by a
second ranking written beside it.
What this does NOT do is stated in the module header rather than left to be
inferred: selecting an offer is a DECISION, not an execution. No Grant is
committed, no process starts, no host effect is reached. The invariant
fabric_witness_run builds toward -- no committed Grant, no process -- is not
established here.
Four rows, green by execution in one run: a host larger than the floor is
selected for it (positive control), a host smaller than the floor is
CONSIDERED and REFUSED rather than silently dropped (the discriminating red),
an empty roster selects nothing and considers nothing, and the floor demand
carries the authority's own satisfaction requirement rather than a copy.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A compare-and-set whose target came from the expectation could commit against a slot that was never there
std.durable_compare_and_set has had no production realization since it landed.
This is the first, and it is the shape that module's own header asks for: the
store owns the read and the conditional write in one operation, so no caller
ever supplies a free-standing observation and the declared key-relation
boundary is closed by construction rather than observed and refused.
The mechanism is generation-suffixed slots. A slot at generation N is the file
<root>/<key>.<N>, written once and never rewritten, so both expectations reduce
to one primitive -- create-if-absent is create-new key.1, update-from-N is
create-new key.N+1 -- and create-new is O_EXCL. Exclusion is therefore performed
by the operating system on the write itself rather than by a lock the caller
holds, which is the gap the interface names: the existing exclusion is flock,
single-host by construction, and cannot serialize two writers on different
hosts. Verified on both the interpreter and the emitter paths rather than taken
from the prose note, because a rung is per-path.
THE DEFECT THIS COMMIT ALSO REPAIRS WAS MINE, FOUND BEFORE IT LANDED. The first
cut derived the target generation from the EXPECTATION and let O_EXCL decide.
That is sound for ExpectSlotAbsent and wrong for ExpectSlotGeneration, because
O_EXCL excludes competing writers for the TARGET PATH and establishes nothing
about which generation is currently the head. An attempt expecting generation 7
against an EMPTY store computed target 8, found key.8 free, won the create, and
reported a commit on a precondition that was never true.
The target is now derived from the OBSERVATION. An expectation is a claim about
the store, and deriving the write target from the claim rather than from the
store is the whole of the bug. The invariant is that the read establishes
eligibility and the exclusive write decides the winner -- reading first does not
reopen a time-of-check-to-time-of-use race, because two writers that both
observe head N both derive N+1 and exactly one create succeeds.
THE EVIDENCE IS THE FILESYSTEM, NOT A BOOLEAN. The live probe drives five
attempts and the store is left holding exactly slot-a.1 and slot-a.2. There is
no slot-a.8 and no slot-b.8, and under the old derivation both would exist --
an expectation of generation 7 is refused against a slot at generation 2 and
against a slot that does not exist at all, with no write attempted in either
case.
That probe is an entry point rather than a shell script because an ad-hoc .sh
here is unmodeled realization: if a measurement is worth re-deriving it is worth
an entry point.
TWO FURTHER DEFECTS FOUND BY BUILDING RATHER THAN BY READING. CasOutcome has
three arms and none can say the attempt's digest does not match its payload;
reporting that as a store refusal blames the store for the caller lying, so the
input is narrowed instead of the shared type widened -- a sole_constructor
verified-attempt whose only mint verifies the digest, which the interface says
is exactly the realizing store's duty and which is available here because this
realization is concrete at the type the hash function accepts. And the key is
interpolated into a path, so a key carrying a separator escaped the store root;
refused at the mint, and refusing the separator alone is sufficient because the
generation suffix is always appended so a bare dot-dot can never be a final
component.
A WITNESS WAS DELETED RATHER THAN REPAIRED. the_target_generation_is_derived_-
from_the_expectation_and_never_supplied was green, and it was green because it
pinned the defective invariant. Keeping it beside the fix would leave the corpus
asserting both the defect and its repair. Its replacement cannot be hermetic:
the corrected derivation reads the store, so every discriminating row for it
performs a host effect and belongs to the live probe.
Scope declared rather than overclaimed. sole_constructor confines construction
on the source-to-.dag path; DESIGN records by execution that an emitted mirror
is forgeable, so the mint is sufficient for the path this carrier travels and
nothing more is claimed. O_EXCL serializes writers only against the SAME store
instance -- two local roots on two hosts are two stores. And the probe treats an
unreadable generation as the end of the chain because the transport cannot
distinguish absent from unreadable; that conflation is declared with a rung and
a trigger rather than resolved by parsing an error string.
Not opened for merge: no production consumer exists yet. The broker cut is what
consumes it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Selection decides which cell, the store decides whether we get it -- and the offer names the cell
The first production consumer of three authorities that were each complete and
unconsumed: product.fabric.selection ranked nothing for anyone, the floor's
demand-side dispatch had only witness rows behind it, and the file-backed
compare-and-set had no caller at all. The value is not new vocabulary -- this
invents none -- it is that those three stop being furniture.
THE INVARIANT, and the reason the two steps are in this order: SELECTION IS A
DECISION, NOT A CLAIM. Two brokers ranking one roster reach the SAME answer, so
selection alone hands one cell to both. The compare-and-set is what makes the
reservation exclusive, and the store rather than a lock decides, so it holds
across hosts. No committed compare-and-set, no reservation.
THE ARROW, which is the part that changed after review. The first cut took the
slot as a parameter BESIDE the selection, so a caller could reserve srv3-06
against a decision that chose a different supplier: two true facts with the
relation between them asserted by neither, and every arm still reading as
plausible. Five hermetic rows and two live receipts were green over it, because
each tests a projection and none tests the join.
The repair is construction. FabricCellCandidate is sole_constructor and its mint
refuses unless the offer's executor is exactly the slot's canonical instance
name, so the broker now takes a roster and no slot at all, and recovers the key
from the WINNING offer. That is the same renderer's output carried through
selection rather than a second identity authority -- the property the store's
key must have. A reservation for a cell the market did not choose has no
spelling.
THE RUNG IS PATH-SCOPED AND THE MODULE SAYS SO. Structurally impossible on the
source-to-.dag acceptance path: the validator is fixed and module-owned with
zero caller freedom, so it cannot be defeated the way a caller-supplied
predicate can. UNESTABLISHED across emission -- DESIGN carries an executed
receipt that a fixed-law mint of this shape emits as a pub struct with a pub
field deriving Deserialize. A class's rung is the minimum across its paths, so
both are stated and the next-rung trigger is named.
EVIDENCE, by execution and by the filesystem rather than by return values.
Seven hermetic rows green, including the arrow's positive control and its
discriminating red (an offer executed by anyone else refuses at the mint), and
a fail-open guard asserting all four non-commit arms report the cell unheld.
Three live rows: the broker reserves the cell whose offer won, leaving exactly
srv3-06.1; a second writer expecting the same absent slot LOSES, leaving exactly
srv3-06.1 and srv3-06.2 with no third file and nothing overwritten; and an
empty roster reserves nothing, leaving the store EMPTY -- the only observation
that catches a broker fabricating a decision the market refused to make.
The probe's own refusal codes split NoCellAdmissible into nothing-offered and
everything-rejected, because one code for both hid a fixture declaring 1 thread
against the floor's required 8, which read exactly like a correct refusal.
WHAT THIS DOES NOT DO. It issues no ExecutionGrant, starts no process and
reaches no host. A reservation is the precondition for a Grant and is not one:
ExecutionGrant carries reservations that must commit atomically across ledgers,
and manufacturing one from a slot generation would fabricate the very atomicity
that record exists to guarantee.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A capacity class the supplier cannot author: control-plane work refuses customer capacity at admission
gunbc.fabric_capacity_class_gap has recorded, unconsumed, that nothing
structurally prevents CONTROL-PLANE capacity -- the cells running our own
scheduler, reconciliation, admission and receipt work -- from being offered as
customer-executable supply. That class sat BELOW mitigatable: not a failure
being contained, an invalid state simply representable and unremarked. This is
its named next-rung trigger, and the gap carrier's own words for what it was
waiting on.
WHERE THE CLASS DOES NOT GO, AND WHY THE CARRIER'S TRIGGER TEXT IS WRONG.
That trigger reads "a capacity class on product.fabric.work Shape". Taken
literally it names the Shape RECORD -- and Shape is one type carried by BOTH
ExecutionRequirements and SupplierOffer, so a required field there is stated by
the SUPPLIER. That is ClassOnSupplierOffer, the arm the same carrier refuses two
declarations earlier, arriving through the type system with its refutation
intact: it asks the party with the least knowledge and the most incentive to say
yes to make the safety assertion. Nobody would choose it; the shared type hands
it over. The ruled rationale governs over the ruled name -- "we originate the
demand, so we hold the fact" is true of the work side and false of a type the
supply side also carries.
A SECOND, INDEPENDENT REASON Shape WAS THE WRONG CARRIER, and it is why this
was worth stopping for rather than arguing about: shape_material HAND-ENUMERATES
its inputs. A class added there would have been SILENTLY ABSENT from the material
identity, so two shapes differing only in class would share one identity -- and
the guard against exactly that, unstated_and_stated_do_not_collapse_in_the_material,
varies the ENVELOPE and would have stayed green over it.
THAT TRAP FOLLOWED THE FIELD TO ITS NEW HOME. work_identity_material
hand-enumerates too, and reads all four requirements fields by hand today. Its
own annotation records isolation having been omitted and repaired "ONE FIELD
LATER". This is the third field. capacity_class is added to that material, and
the row proving it -- two demands alike but for their class must not share an
identity -- is authored to vary THE CLASS, because the existing collapse guard
varies the envelope and cannot fail on this. Verified by execution in both
directions: removing the field from the material turns that row FALSE while the
identical-demands control stays TRUE.
The hand-enumeration itself is NOT repaired here. Deriving materials from the
record is the right fix and changes every material identity in the fabric -- a
content-hash event, not a field addition -- and bundling it inside a safety cut
would have a reviewer approve one change while receiving two.
WHAT AN EXECUTOR IS SANCTIONED FOR IS OUR FACT. ExecutionRequirements says what
work REQUIRES; gunbc.fabric_executor_class says what an executor may serve, and
it is a fleet-side roster we author about machines we own or rent. The supplier
is never asked. That follows the precedent already in product.supplier.ubicloud,
which refuses to name an isolation profile from a published price list -- and a
class invented from a catalog would be worse than an invented profile, because a
broker reading it would ROUTE ACROSS A SAFETY BOUNDARY rather than mis-rank.
Our own cells are control-plane BY CONSTRUCTION rather than by a roster row
someone must remember to add: a RunnerSlotIdentity cannot name anything but a
cell in our build fleet, so fleet_cell_sanction derives the sanction from the
identity. An UNCLASSIFIED executor REFUSES rather than defaulting -- "we have
not classified this" and "this serves customers" are different states with
different remedies, and a default would let the roster grow a sanction nobody
authored.
ADMISSION RUNS BEFORE FUNGIBILITY, and the order is the safety property. Once
two offers are fungible they are interchangeable by definition, so a class
boundary checked after ranking is a boundary already crossed. The broker filters
the roster first, so an unsanctioned cell is never a candidate and cannot be
reached by a tie-break, a price, or a later change to the ranking.
EVIDENCE: eight hermetic rows green, both walls asserted in both directions
(control-plane work refused on customer capacity AND customer work refused on
our cells), each with the positive control that stops it being satisfied by an
admission that refuses everything. The e2e broker probe still reserves the cell
whose offer won, leaving exactly srv3-06.1. Re-verified on a compiler rebuilt
from this HEAD after finding the previous binary was 87 commits stale.
CapacityAdmission and CapacityAdmitted collided with gunbc.fleet_capacity_control,
which answers a different question -- whether a HOST is active by provider. Names
are corpus-global and a duplicate refuses whole-corpus while every entry-scoped
witness passes, so the collision was found by sweep rather than by the eight
green rows. Renamed to CapacityClassAdmission / CapacityClassAdmitted.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The partial commit has no constructor: an atomic two-ledger reservation, because purity makes the join free
ExecutionGrant carries resource_reservations and money_reservation, and its own
annotation states the invariant: "resource admitted with money refused must
commit no resource reservation, and money admitted with resource refused must
commit no money reservation; both are one canonical state transition. A partial
commit is the state that leaks capacity or budget with no grant to account for
it, and it is unreachable only if the join is atomic rather than sequential."
That join did not exist. This is it.
ATOMICITY IS NOT A PROTOCOL HERE, AND THAT IS THE WHOLE DESIGN. Two-phase
commit, compensating release, an undo log -- every one of those makes the
partial state REACHABLE and then works to escape it, which is validation
standing where construction was available. These ledgers are PURE: reserving
returns a new ledger rather than mutating one. So the join simply declines to
produce a pair unless both sides advanced, and the partial commit has no
constructor. Nothing unwinds because nothing was ever applied. On a money
refusal the advanced resource ledger is computed and goes out of scope -- in a
mutating design that branch is the leak.
GENERIC OVER BOTH QUANTITIES, WHICH IS WHY THIS CUT IS SMALL. EncumbranceLedger
<Q, S> in extdeps.accounting.encumbrance is already the cited authority for
holding a commitment against an appropriation, and product.fabric.budget is one
instantiation of it for money -- complete, with lease generation fencing, and
consumed by nothing but its own witness. A resource ledger is a SECOND
INSTANTIATION, not a second authority, so this join names no quantity at all.
Inventing a resource-specific ledger beside the generic would be the
re-invention DESIGN calls a failed decomposition.
An earlier note of mine said this was blocked on "two ledgers that do not
exist". That was wrong and is corrected here: the generic authority and the
money instantiation both exist. `ReservationRef` being a branded string is true;
"therefore nothing holds anything" was an inference past a verified fact, and
budget.dag holds and fences things today.
ONE REFERENCE KEYS BOTH SIDES, and that is load-bearing rather than tidy. The
encumbrance authority refuses a duplicate reference, and its own note explains
why: first-match resolution and rewrite-all-matches are the same operation only
while a reference is unique.
THE REFUSAL ARMS CARRY NO LEDGER AT ALL, so a caller cannot mistake a refusal
for a no-op advance and persist it. That is the reachable form of the leak in a
pure design: a caller writes back whatever joint_reservation_ledgers returns, so
an arm that carried the advanced pair would be committed to storage by a caller
doing exactly the right thing.
EVIDENCE, INCLUDING A RED THAT ACTUALLY FIRES. Six rows green, both refusal
directions asserted separately because the arms are separate code. Verified by
execution in both directions: with the money-refusal branch changed to commit
the resource side -- the partial commit itself -- the guard returns FALSE while
the positive control stays TRUE.
A FIRST DRAFT OF THAT GUARD WAS A DECORATION AND IS RECORDED HERE BECAUSE IT
ALMOST SHIPPED. It asserted that the caller's own ledger was unchanged after a
refusal. The ledgers are pure values, so that assertion CANNOT FAIL whatever the
join does -- permanently green by construction, and worse than absent because it
would have been cited as the guard against precisely the leak it could not
detect. The replacement asserts what is authorable: a refusal yields nothing to
persist.
WHAT THIS DOES NOT DO. It mints no ReservationRef and issues no ExecutionGrant.
Binding the held pair to a minted reference, and requiring ExecutionGrant to
carry held reservations rather than branded strings, is the following cut -- and
it is now executable rather than blocked, which the previous frontier was not.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The intermediate reservation had no reason to exist: the broker holds both ledgers itself
HEAD landed product.fabric.joint_reservation as a standalone module that took two
pure ledgers and returned a joined outcome. Nothing else was ever going to call
it. The only caller it could have -- the broker in gunbc.fabric_control_plane --
already holds the demand, the offer, the selection cost and the store slot, so
routing them out to a module that knows none of those and back again is a second
representation of one decision (§2). It is deleted at the root rather than
refined from the leaves (§3, delete-first), and what replaces it is the broker
making the reservation directly.
WHAT SURVIVES IS THE GUARANTEE, NOT THE MODULE. CellReservation gains a
BudgetRefused arm and CellReserved gains the advanced account, and that pairing
is the whole safety argument: no arm carries an account without a cell, and no
arm carries a cell without an account. The partial commit -- an encumbrance with
nothing running, or a running cell nobody is paying for -- has no constructor, so
it is unwritable rather than checked (§4b, structurally impossible).
THE ORDERING CLAIM WAS WITHDRAWN, AND THE RECEIPT IS WHY. A witness asserting
"the budget refuses before the store is touched" was authored, went green, and
STAYED GREEN under a mutation moving the compare-and-set ahead of the
encumbrance. The substrate is lazy: the branch that is not returned is never
forced, so both spellings are equally effect-free and the row discriminated
nothing -- a decoration cited as coverage. It is replaced by rows that assert
what the carrier actually guarantees.
THREE ROWS, EACH EXCLUDING WHAT THE OTHERS ADMIT. A ceiling below the liability
refuses with a ledger cause. An offer quoted in a currency the account does not
hold refuses on the OTHER axis, which is what excludes a broker that returns
BudgetRefused unconditionally -- and it is only authorable because the currency
presented to the budget comes from the offer rather than from the account, which
would have made the check green by construction. A ceiling of 999 against a
liability of 1000 refuses only if the FULL selection cost was presented, so a
broker encumbering the marginal charge alone goes red where the other two stay
green.
Compile: 0 blocking over both entries. All five rows verified returning true by
execution, not by typecheck.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The annotation said the refusals were counted and nothing counted them
Review 57180 (codex/gpt-5.6-sol, REQUEST_CHANGES) flagged two Boolean predicates
over substrate coproducts and cited a predicate-dissolution rule in DESIGN.md.
THAT RULE IS NOT IN DESIGN.md. It lives in docs/plans/nat-grounding-unification-
design.md and it is narrower than cited: a manual match is forbidden WHERE A
CANONICAL FOLD ALREADY EXISTS, which is why is_zero must become nat_cata.
Neither CapacityClassAdmission nor CellReservation has a catamorphism, so the
rule as stated does not reach either site.
Following it to the code found two real defects underneath it, and both are
worse than the thing that was reported.
THE ROSTER WAS SILENTLY NARROWED WHILE THE ANNOTATION CLAIMED OTHERWISE.
admitted_cell_roster kept the admitted through the Bool; refused_cell_admissions
collected the refused and HAD NO CALLER. So a demand refused entirely on the
capacity-class safety line and a demand nobody offered anything for arrived as
one symbol, and their remedies are opposite: offer more capacity, versus stop
asking for capacity you are not sanctioned to use. The prose above them read
"the refusals are COUNTED rather than silently filtered". Nothing counted them.
That is the empty-observation narrow with a sentence standing where the
mechanism was supposed to be.
Two folds re-running one judgement could also only agree by convention -- an
edit to either could put a candidate in neither half or in both, undetected. One
partition_cell_roster now makes the decision once and returns both halves, so
they cannot disagree, and NoCellAdmissible carries the refused population so the
two states are distinguishable by the caller. The Bool dies with its only
production caller.
THE OTHER PREDICATE HAD NO PRODUCTION CONSUMER AT ALL. cell_reservation_is_held
was called only by the two witness rows that existed to cover it -- an artifact
whose only consumer is its own test. Deleted. What replaces it exercises the
partition through the real broker: a refused executor is reported, an empty
roster reports none, and the pair excludes a broker that always reports a
refusal.
AND THE FOUR CAPACITY ROWS WERE ASSERTING THROUGH A COLLAPSE THEY THEMSELVES
DECLARED ILLEGAL. The Bool answered false for both a refused class and an
unclassified executor, while the unclassified row's own annotation said those
two states have different remedies and must not be collapsed. The row could not
see the distinction it was about. Each now names its arm, and the substitution
is executed rather than asserted: swapping the unclassified row's selector to
the other refusal arm returns false, which is the red the old Bool could not
produce.
Compile: 0 blocking. Eight rows verified returning true by execution, plus the
one mutation returning false.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The reservation had no way to end: the release half, and the slot finally says who holds it
The broker minted reservations and nothing ever ended them. product.fabric.budget
has had settle_money and release_money since it landed, fenced on the lease
generation; product.fabric.arbitration models the DECISION as ReleaseDirective
and says in its own header that the fabric releases nothing there. What was
missing was the actuator. Measured before starting: release_money and
settle_money had witness callers and ZERO production consumers.
THE SLOT PAYLOAD WAS WRITE-ONLY AND RELEASE IS ITS FIRST READER. That is the
part of this change that is not plumbing. The broker wrote the reservation into
the slot and nothing ever read it back, so the question release has to ask -- IS
THIS CELL HELD, AND BY WHICH RESERVATION -- had no answer. Without one, release
is a blind write: it frees whatever is in the slot on the strength of a
generation the CALLER supplied, which is a second account of who holds the cell
and free to disagree with the store.
The generation fence does not close that. It establishes the slot has not MOVED
since it was observed, which is a different question from whether it is held and
by whom. A slot already free at generation N admits a release presenting N, and
that is not a harmless no-op: it writes free over free, so a re-reservation
racing the second release finds its precondition broken by the release of a hold
that never existed.
So CellSlotState is typed, CellHeld carries the reservation reference itself
rather than re-rendering the demand and offer into a second spelling of an
identity that already exists, and the decode REFUSES an unrecognised payload
rather than answering either state.
THE PARTIAL RELEASE HAS NO CONSTRUCTOR, and it leaks the opposite way to the
reservation's: freeing the cell while the encumbrance stands bills a customer
for an idle machine, and releasing the money while the cell stays held strands
capacity under work nothing requires. Same construction argument as the reserve
half -- the money transition is pure, the slot write is the only effect, and no
arm of CellRelease carries one without the other.
AND THE FUNCTION WAS UNREACHABLE UNTIL THE LAST COMMIT OF THIS CHANGE, WHICH THE
WITNESSES COULD NOT HAVE TOLD ME. release_reserved_cell takes a
CasSlotObservation, and that type had no production producer anywhere: the file
store answers CasSlotProbe and file_compare_and_set converts internally without
ever building an observation. So the release path was callable only from
hand-built values, and my own witnesses were authoring the exact input the store
is supposed to supply -- an artifact with no final consumer, hidden by its own
tests. Found by writing the live probe row, not by the witnesses.
The repair is one observation surface in the store, observe_cas_slot_state, plus
release_reserved_cell_at beside the pure decision. It deliberately does not
delegate the bound arm to cas_probe_as_readable: that projection answers
CasReadableAbsent for a slot past the probe bound, which is right for reporting
a lost race and wrong for a decision caller, who would read "the cell is empty"
from a store that could not tell it anything and pick the remedy for an empty
cell instead of repairing the slot. file_compare_and_set is left alone -- it
produces outcomes rather than observations, so there is no second producer, and
restructuring it would rewrite a load-bearing function whose header narrates a
previously-fixed write-decides bug for no gain to it.
Seven witness rows, every one green by execution, and the holder wall carries an
executed RED: disabling the comparison returns false. Compile 0 blocking across
the witness and probe entries.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The two tags were the same length and the decode was quietly relying on it
Review 57256 (APPROVE, non-blocking) noticed that decode_cell_slot_payload
computed the body ONCE against the length of the held tag and reused it for the
free arm, which is correct only because both tags happen to be five characters.
The note is right and the coupling bought nothing, so it is removed rather than
documented.
WHY IT WAS WORTH A COMMIT RATHER THAN A REPLY. The failure it sets up is silent
and delayed: a third tag of any other length decodes to a body sliced at the
wrong offset, and every existing row stays green because the two tags that
already exist still agree. So the check that would catch it is exactly the check
nobody writes -- the round trip over a tag that does not exist yet.
The same defect had a second face the note did not name: each tag was spelled
TWICE, once rendering and once decoding, so the two spellings could drift
independently of the lengths. Both are one rule. The tags are named once and the
body is derived from the tag that MATCHED, so there is no offset to get wrong
and no second spelling to disagree.
PROVEN BY EXECUTION RATHER THAN BY INSPECTION, because "now it is decoupled" is
the kind of claim that reads as obviously true and is worth one run: with
cell_free_tag temporarily changed from "free|" to "released|" -- five characters
to nine -- both_slot_states_survive_the_round_trip still returns true. Under the
previous form that substitution sliced the free body at offset 5 and would have
failed. Tag restored, compile 0 blocking.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* compute fabric design (#9604)
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm ex…
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* The floor's demand and its supply selection are one join, and select_supply gets its first caller
select_supply has been complete and unconsumed since it landed. This module
is the join: the required floor's own Work becomes a Demand, and the candidate
roster is ranked by the authority that already knew how, rather than by a
second ranking written beside it.
What this does NOT do is stated in the module header rather than left to be
inferred: selecting an offer is a DECISION, not an execution. No Grant is
committed, no process starts, no host effect is reached. The invariant
fabric_witness_run builds toward -- no committed Grant, no process -- is not
established here.
Four rows, green by execution in one run: a host larger than the floor is
selected for it (positive control), a host smaller than the floor is
CONSIDERED and REFUSED rather than silently dropped (the discriminating red),
an empty roster selects nothing and considers nothing, and the floor demand
carries the authority's own satisfaction requirement rather than a copy.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A compare-and-set whose target came from the expectation could commit against a slot that was never there
std.durable_compare_and_set has had no production realization since it landed.
This is the first, and it is the shape that module's own header asks for: the
store owns the read and the conditional write in one operation, so no caller
ever supplies a free-standing observation and the declared key-relation
boundary is closed by construction rather than observed and refused.
The mechanism is generation-suffixed slots. A slot at generation N is the file
<root>/<key>.<N>, written once and never rewritten, so both expectations reduce
to one primitive -- create-if-absent is create-new key.1, update-from-N is
create-new key.N+1 -- and create-new is O_EXCL. Exclusion is therefore performed
by the operating system on the write itself rather than by a lock the caller
holds, which is the gap the interface names: the existing exclusion is flock,
single-host by construction, and cannot serialize two writers on different
hosts. Verified on both the interpreter and the emitter paths rather than taken
from the prose note, because a rung is per-path.
THE DEFECT THIS COMMIT ALSO REPAIRS WAS MINE, FOUND BEFORE IT LANDED. The first
cut derived the target generation from the EXPECTATION and let O_EXCL decide.
That is sound for ExpectSlotAbsent and wrong for ExpectSlotGeneration, because
O_EXCL excludes competing writers for the TARGET PATH and establishes nothing
about which generation is currently the head. An attempt expecting generation 7
against an EMPTY store computed target 8, found key.8 free, won the create, and
reported a commit on a precondition that was never true.
The target is now derived from the OBSERVATION. An expectation is a claim about
the store, and deriving the write target from the claim rather than from the
store is the whole of the bug. The invariant is that the read establishes
eligibility and the exclusive write decides the winner -- reading first does not
reopen a time-of-check-to-time-of-use race, because two writers that both
observe head N both derive N+1 and exactly one create succeeds.
THE EVIDENCE IS THE FILESYSTEM, NOT A BOOLEAN. The live probe drives five
attempts and the store is left holding exactly slot-a.1 and slot-a.2. There is
no slot-a.8 and no slot-b.8, and under the old derivation both would exist --
an expectation of generation 7 is refused against a slot at generation 2 and
against a slot that does not exist at all, with no write attempted in either
case.
That probe is an entry point rather than a shell script because an ad-hoc .sh
here is unmodeled realization: if a measurement is worth re-deriving it is worth
an entry point.
TWO FURTHER DEFECTS FOUND BY BUILDING RATHER THAN BY READING. CasOutcome has
three arms and none can say the attempt's digest does not match its payload;
reporting that as a store refusal blames the store for the caller lying, so the
input is narrowed instead of the shared type widened -- a sole_constructor
verified-attempt whose only mint verifies the digest, which the interface says
is exactly the realizing store's duty and which is available here because this
realization is concrete at the type the hash function accepts. And the key is
interpolated into a path, so a key carrying a separator escaped the store root;
refused at the mint, and refusing the separator alone is sufficient because the
generation suffix is always appended so a bare dot-dot can never be a final
component.
A WITNESS WAS DELETED RATHER THAN REPAIRED. the_target_generation_is_derived_-
from_the_expectation_and_never_supplied was green, and it was green because it
pinned the defective invariant. Keeping it beside the fix would leave the corpus
asserting both the defect and its repair. Its replacement cannot be hermetic:
the corrected derivation reads the store, so every discriminating row for it
performs a host effect and belongs to the live probe.
Scope declared rather than overclaimed. sole_constructor confines construction
on the source-to-.dag path; DESIGN records by execution that an emitted mirror
is forgeable, so the mint is sufficient for the path this carrier travels and
nothing more is claimed. O_EXCL serializes writers only against the SAME store
instance -- two local roots on two hosts are two stores. And the probe treats an
unreadable generation as the end of the chain because the transport cannot
distinguish absent from unreadable; that conflation is declared with a rung and
a trigger rather than resolved by parsing an error string.
Not opened for merge: no production consumer exists yet. The broker cut is what
consumes it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Selection decides which cell, the store decides whether we get it -- and the offer names the cell
The first production consumer of three authorities that were each complete and
unconsumed: product.fabric.selection ranked nothing for anyone, the floor's
demand-side dispatch had only witness rows behind it, and the file-backed
compare-and-set had no caller at all. The value is not new vocabulary -- this
invents none -- it is that those three stop being furniture.
THE INVARIANT, and the reason the two steps are in this order: SELECTION IS A
DECISION, NOT A CLAIM. Two brokers ranking one roster reach the SAME answer, so
selection alone hands one cell to both. The compare-and-set is what makes the
reservation exclusive, and the store rather than a lock decides, so it holds
across hosts. No committed compare-and-set, no reservation.
THE ARROW, which is the part that changed after review. The first cut took the
slot as a parameter BESIDE the selection, so a caller could reserve srv3-06
against a decision that chose a different supplier: two true facts with the
relation between them asserted by neither, and every arm still reading as
plausible. Five hermetic rows and two live receipts were green over it, because
each tests a projection and none tests the join.
The repair is construction. FabricCellCandidate is sole_constructor and its mint
refuses unless the offer's executor is exactly the slot's canonical instance
name, so the broker now takes a roster and no slot at all, and recovers the key
from the WINNING offer. That is the same renderer's output carried through
selection rather than a second identity authority -- the property the store's
key must have. A reservation for a cell the market did not choose has no
spelling.
THE RUNG IS PATH-SCOPED AND THE MODULE SAYS SO. Structurally impossible on the
source-to-.dag acceptance path: the validator is fixed and module-owned with
zero caller freedom, so it cannot be defeated the way a caller-supplied
predicate can. UNESTABLISHED across emission -- DESIGN carries an executed
receipt that a fixed-law mint of this shape emits as a pub struct with a pub
field deriving Deserialize. A class's rung is the minimum across its paths, so
both are stated and the next-rung trigger is named.
EVIDENCE, by execution and by the filesystem rather than by return values.
Seven hermetic rows green, including the arrow's positive control and its
discriminating red (an offer executed by anyone else refuses at the mint), and
a fail-open guard asserting all four non-commit arms report the cell unheld.
Three live rows: the broker reserves the cell whose offer won, leaving exactly
srv3-06.1; a second writer expecting the same absent slot LOSES, leaving exactly
srv3-06.1 and srv3-06.2 with no third file and nothing overwritten; and an
empty roster reserves nothing, leaving the store EMPTY -- the only observation
that catches a broker fabricating a decision the market refused to make.
The probe's own refusal codes split NoCellAdmissible into nothing-offered and
everything-rejected, because one code for both hid a fixture declaring 1 thread
against the floor's required 8, which read exactly like a correct refusal.
WHAT THIS DOES NOT DO. It issues no ExecutionGrant, starts no process and
reaches no host. A reservation is the precondition for a Grant and is not one:
ExecutionGrant carries reservations that must commit atomically across ledgers,
and manufacturing one from a slot generation would fabricate the very atomicity
that record exists to guarantee.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A capacity class the supplier cannot author: control-plane work refuses customer capacity at admission
gunbc.fabric_capacity_class_gap has recorded, unconsumed, that nothing
structurally prevents CONTROL-PLANE capacity -- the cells running our own
scheduler, reconciliation, admission and receipt work -- from being offered as
customer-executable supply. That class sat BELOW mitigatable: not a failure
being contained, an invalid state simply representable and unremarked. This is
its named next-rung trigger, and the gap carrier's own words for what it was
waiting on.
WHERE THE CLASS DOES NOT GO, AND WHY THE CARRIER'S TRIGGER TEXT IS WRONG.
That trigger reads "a capacity class on product.fabric.work Shape". Taken
literally it names the Shape RECORD -- and Shape is one type carried by BOTH
ExecutionRequirements and SupplierOffer, so a required field there is stated by
the SUPPLIER. That is ClassOnSupplierOffer, the arm the same carrier refuses two
declarations earlier, arriving through the type system with its refutation
intact: it asks the party with the least knowledge and the most incentive to say
yes to make the safety assertion. Nobody would choose it; the shared type hands
it over. The ruled rationale governs over the ruled name -- "we originate the
demand, so we hold the fact" is true of the work side and false of a type the
supply side also carries.
A SECOND, INDEPENDENT REASON Shape WAS THE WRONG CARRIER, and it is why this
was worth stopping for rather than arguing about: shape_material HAND-ENUMERATES
its inputs. A class added there would have been SILENTLY ABSENT from the material
identity, so two shapes differing only in class would share one identity -- and
the guard against exactly that, unstated_and_stated_do_not_collapse_in_the_material,
varies the ENVELOPE and would have stayed green over it.
THAT TRAP FOLLOWED THE FIELD TO ITS NEW HOME. work_identity_material
hand-enumerates too, and reads all four requirements fields by hand today. Its
own annotation records isolation having been omitted and repaired "ONE FIELD
LATER". This is the third field. capacity_class is added to that material, and
the row proving it -- two demands alike but for their class must not share an
identity -- is authored to vary THE CLASS, because the existing collapse guard
varies the envelope and cannot fail on this. Verified by execution in both
directions: removing the field from the material turns that row FALSE while the
identical-demands control stays TRUE.
The hand-enumeration itself is NOT repaired here. Deriving materials from the
record is the right fix and changes every material identity in the fabric -- a
content-hash event, not a field addition -- and bundling it inside a safety cut
would have a reviewer approve one change while receiving two.
WHAT AN EXECUTOR IS SANCTIONED FOR IS OUR FACT. ExecutionRequirements says what
work REQUIRES; gunbc.fabric_executor_class says what an executor may serve, and
it is a fleet-side roster we author about machines we own or rent. The supplier
is never asked. That follows the precedent already in product.supplier.ubicloud,
which refuses to name an isolation profile from a published price list -- and a
class invented from a catalog would be worse than an invented profile, because a
broker reading it would ROUTE ACROSS A SAFETY BOUNDARY rather than mis-rank.
Our own cells are control-plane BY CONSTRUCTION rather than by a roster row
someone must remember to add: a RunnerSlotIdentity cannot name anything but a
cell in our build fleet, so fleet_cell_sanction derives the sanction from the
identity. An UNCLASSIFIED executor REFUSES rather than defaulting -- "we have
not classified this" and "this serves customers" are different states with
different remedies, and a default would let the roster grow a sanction nobody
authored.
ADMISSION RUNS BEFORE FUNGIBILITY, and the order is the safety property. Once
two offers are fungible they are interchangeable by definition, so a class
boundary checked after ranking is a boundary already crossed. The broker filters
the roster first, so an unsanctioned cell is never a candidate and cannot be
reached by a tie-break, a price, or a later change to the ranking.
EVIDENCE: eight hermetic rows green, both walls asserted in both directions
(control-plane work refused on customer capacity AND customer work refused on
our cells), each with the positive control that stops it being satisfied by an
admission that refuses everything. The e2e broker probe still reserves the cell
whose offer won, leaving exactly srv3-06.1. Re-verified on a compiler rebuilt
from this HEAD after finding the previous binary was 87 commits stale.
CapacityAdmission and CapacityAdmitted collided with gunbc.fleet_capacity_control,
which answers a different question -- whether a HOST is active by provider. Names
are corpus-global and a duplicate refuses whole-corpus while every entry-scoped
witness passes, so the collision was found by sweep rather than by the eight
green rows. Renamed to CapacityClassAdmission / CapacityClassAdmitted.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The partial commit has no constructor: an atomic two-ledger reservation, because purity makes the join free
ExecutionGrant carries resource_reservations and money_reservation, and its own
annotation states the invariant: "resource admitted with money refused must
commit no resource reservation, and money admitted with resource refused must
commit no money reservation; both are one canonical state transition. A partial
commit is the state that leaks capacity or budget with no grant to account for
it, and it is unreachable only if the join is atomic rather than sequential."
That join did not exist. This is it.
ATOMICITY IS NOT A PROTOCOL HERE, AND THAT IS THE WHOLE DESIGN. Two-phase
commit, compensating release, an undo log -- every one of those makes the
partial state REACHABLE and then works to escape it, which is validation
standing where construction was available. These ledgers are PURE: reserving
returns a new ledger rather than mutating one. So the join simply declines to
produce a pair unless both sides advanced, and the partial commit has no
constructor. Nothing unwinds because nothing was ever applied. On a money
refusal the advanced resource ledger is computed and goes out of scope -- in a
mutating design that branch is the leak.
GENERIC OVER BOTH QUANTITIES, WHICH IS WHY THIS CUT IS SMALL. EncumbranceLedger
<Q, S> in extdeps.accounting.encumbrance is already the cited authority for
holding a commitment against an appropriation, and product.fabric.budget is one
instantiation of it for money -- complete, with lease generation fencing, and
consumed by nothing but its own witness. A resource ledger is a SECOND
INSTANTIATION, not a second authority, so this join names no quantity at all.
Inventing a resource-specific ledger beside the generic would be the
re-invention DESIGN calls a failed decomposition.
An earlier note of mine said this was blocked on "two ledgers that do not
exist". That was wrong and is corrected here: the generic authority and the
money instantiation both exist. `ReservationRef` being a branded string is true;
"therefore nothing holds anything" was an inference past a verified fact, and
budget.dag holds and fences things today.
ONE REFERENCE KEYS BOTH SIDES, and that is load-bearing rather than tidy. The
encumbrance authority refuses a duplicate reference, and its own note explains
why: first-match resolution and rewrite-all-matches are the same operation only
while a reference is unique.
THE REFUSAL ARMS CARRY NO LEDGER AT ALL, so a caller cannot mistake a refusal
for a no-op advance and persist it. That is the reachable form of the leak in a
pure design: a caller writes back whatever joint_reservation_ledgers returns, so
an arm that carried the advanced pair would be committed to storage by a caller
doing exactly the right thing.
EVIDENCE, INCLUDING A RED THAT ACTUALLY FIRES. Six rows green, both refusal
directions asserted separately because the arms are separate code. Verified by
execution in both directions: with the money-refusal branch changed to commit
the resource side -- the partial commit itself -- the guard returns FALSE while
the positive control stays TRUE.
A FIRST DRAFT OF THAT GUARD WAS A DECORATION AND IS RECORDED HERE BECAUSE IT
ALMOST SHIPPED. It asserted that the caller's own ledger was unchanged after a
refusal. The ledgers are pure values, so that assertion CANNOT FAIL whatever the
join does -- permanently green by construction, and worse than absent because it
would have been cited as the guard against precisely the leak it could not
detect. The replacement asserts what is authorable: a refusal yields nothing to
persist.
WHAT THIS DOES NOT DO. It mints no ReservationRef and issues no ExecutionGrant.
Binding the held pair to a minted reference, and requiring ExecutionGrant to
carry held reservations rather than branded strings, is the following cut -- and
it is now executable rather than blocked, which the previous frontier was not.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The intermediate reservation had no reason to exist: the broker holds both ledgers itself
HEAD landed product.fabric.joint_reservation as a standalone module that took two
pure ledgers and returned a joined outcome. Nothing else was ever going to call
it. The only caller it could have -- the broker in gunbc.fabric_control_plane --
already holds the demand, the offer, the selection cost and the store slot, so
routing them out to a module that knows none of those and back again is a second
representation of one decision (§2). It is deleted at the root rather than
refined from the leaves (§3, delete-first), and what replaces it is the broker
making the reservation directly.
WHAT SURVIVES IS THE GUARANTEE, NOT THE MODULE. CellReservation gains a
BudgetRefused arm and CellReserved gains the advanced account, and that pairing
is the whole safety argument: no arm carries an account without a cell, and no
arm carries a cell without an account. The partial commit -- an encumbrance with
nothing running, or a running cell nobody is paying for -- has no constructor, so
it is unwritable rather than checked (§4b, structurally impossible).
THE ORDERING CLAIM WAS WITHDRAWN, AND THE RECEIPT IS WHY. A witness asserting
"the budget refuses before the store is touched" was authored, went green, and
STAYED GREEN under a mutation moving the compare-and-set ahead of the
encumbrance. The substrate is lazy: the branch that is not returned is never
forced, so both spellings are equally effect-free and the row discriminated
nothing -- a decoration cited as coverage. It is replaced by rows that assert
what the carrier actually guarantees.
THREE ROWS, EACH EXCLUDING WHAT THE OTHERS ADMIT. A ceiling below the liability
refuses with a ledger cause. An offer quoted in a currency the account does not
hold refuses on the OTHER axis, which is what excludes a broker that returns
BudgetRefused unconditionally -- and it is only authorable because the currency
presented to the budget comes from the offer rather than from the account, which
would have made the check green by construction. A ceiling of 999 against a
liability of 1000 refuses only if the FULL selection cost was presented, so a
broker encumbering the marginal charge alone goes red where the other two stay
green.
Compile: 0 blocking over both entries. All five rows verified returning true by
execution, not by typecheck.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The annotation said the refusals were counted and nothing counted them
Review 57180 (codex/gpt-5.6-sol, REQUEST_CHANGES) flagged two Boolean predicates
over substrate coproducts and cited a predicate-dissolution rule in DESIGN.md.
THAT RULE IS NOT IN DESIGN.md. It lives in docs/plans/nat-grounding-unification-
design.md and it is narrower than cited: a manual match is forbidden WHERE A
CANONICAL FOLD ALREADY EXISTS, which is why is_zero must become nat_cata.
Neither CapacityClassAdmission nor CellReservation has a catamorphism, so the
rule as stated does not reach either site.
Following it to the code found two real defects underneath it, and both are
worse than the thing that was reported.
THE ROSTER WAS SILENTLY NARROWED WHILE THE ANNOTATION CLAIMED OTHERWISE.
admitted_cell_roster kept the admitted through the Bool; refused_cell_admissions
collected the refused and HAD NO CALLER. So a demand refused entirely on the
capacity-class safety line and a demand nobody offered anything for arrived as
one symbol, and their remedies are opposite: offer more capacity, versus stop
asking for capacity you are not sanctioned to use. The prose above them read
"the refusals are COUNTED rather than silently filtered". Nothing counted them.
That is the empty-observation narrow with a sentence standing where the
mechanism was supposed to be.
Two folds re-running one judgement could also only agree by convention -- an
edit to either could put a candidate in neither half or in both, undetected. One
partition_cell_roster now makes the decision once and returns both halves, so
they cannot disagree, and NoCellAdmissible carries the refused population so the
two states are distinguishable by the caller. The Bool dies with its only
production caller.
THE OTHER PREDICATE HAD NO PRODUCTION CONSUMER AT ALL. cell_reservation_is_held
was called only by the two witness rows that existed to cover it -- an artifact
whose only consumer is its own test. Deleted. What replaces it exercises the
partition through the real broker: a refused executor is reported, an empty
roster reports none, and the pair excludes a broker that always reports a
refusal.
AND THE FOUR CAPACITY ROWS WERE ASSERTING THROUGH A COLLAPSE THEY THEMSELVES
DECLARED ILLEGAL. The Bool answered false for both a refused class and an
unclassified executor, while the unclassified row's own annotation said those
two states have different remedies and must not be collapsed. The row could not
see the distinction it was about. Each now names its arm, and the substitution
is executed rather than asserted: swapping the unclassified row's selector to
the other refusal arm returns false, which is the red the old Bool could not
produce.
Compile: 0 blocking. Eight rows verified returning true by execution, plus the
one mutation returning false.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The reservation had no way to end: the release half, and the slot finally says who holds it
The broker minted reservations and nothing ever ended them. product.fabric.budget
has had settle_money and release_money since it landed, fenced on the lease
generation; product.fabric.arbitration models the DECISION as ReleaseDirective
and says in its own header that the fabric releases nothing there. What was
missing was the actuator. Measured before starting: release_money and
settle_money had witness callers and ZERO production consumers.
THE SLOT PAYLOAD WAS WRITE-ONLY AND RELEASE IS ITS FIRST READER. That is the
part of this change that is not plumbing. The broker wrote the reservation into
the slot and nothing ever read it back, so the question release has to ask -- IS
THIS CELL HELD, AND BY WHICH RESERVATION -- had no answer. Without one, release
is a blind write: it frees whatever is in the slot on the strength of a
generation the CALLER supplied, which is a second account of who holds the cell
and free to disagree with the store.
The generation fence does not close that. It establishes the slot has not MOVED
since it was observed, which is a different question from whether it is held and
by whom. A slot already free at generation N admits a release presenting N, and
that is not a harmless no-op: it writes free over free, so a re-reservation
racing the second release finds its precondition broken by the release of a hold
that never existed.
So CellSlotState is typed, CellHeld carries the reservation reference itself
rather than re-rendering the demand and offer into a second spelling of an
identity that already exists, and the decode REFUSES an unrecognised payload
rather than answering either state.
THE PARTIAL RELEASE HAS NO CONSTRUCTOR, and it leaks the opposite way to the
reservation's: freeing the cell while the encumbrance stands bills a customer
for an idle machine, and releasing the money while the cell stays held strands
capacity under work nothing requires. Same construction argument as the reserve
half -- the money transition is pure, the slot write is the only effect, and no
arm of CellRelease carries one without the other.
AND THE FUNCTION WAS UNREACHABLE UNTIL THE LAST COMMIT OF THIS CHANGE, WHICH THE
WITNESSES COULD NOT HAVE TOLD ME. release_reserved_cell takes a
CasSlotObservation, and that type had no production producer anywhere: the file
store answers CasSlotProbe and file_compare_and_set converts internally without
ever building an observation. So the release path was callable only from
hand-built values, and my own witnesses were authoring the exact input the store
is supposed to supply -- an artifact with no final consumer, hidden by its own
tests. Found by writing the live probe row, not by the witnesses.
The repair is one observation surface in the store, observe_cas_slot_state, plus
release_reserved_cell_at beside the pure decision. It deliberately does not
delegate the bound arm to cas_probe_as_readable: that projection answers
CasReadableAbsent for a slot past the probe bound, which is right for reporting
a lost race and wrong for a decision caller, who would read "the cell is empty"
from a store that could not tell it anything and pick the remedy for an empty
cell instead of repairing the slot. file_compare_and_set is left alone -- it
produces outcomes rather than observations, so there is no second producer, and
restructuring it would rewrite a load-bearing function whose header narrates a
previously-fixed write-decides bug for no gain to it.
Seven witness rows, every one green by execution, and the holder wall carries an
executed RED: disabling the comparison returns false. Compile 0 blocking across
the witness and probe entries.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The two tags were the same length and the decode was quietly relying on it
Review 57256 (APPROVE, non-blocking) noticed that decode_cell_slot_payload
computed the body ONCE against the length of the held tag and reused it for the
free arm, which is correct only because both tags happen to be five characters.
The note is right and the coupling bought nothing, so it is removed rather than
documented.
WHY IT WAS WORTH A COMMIT RATHER THAN A REPLY. The failure it sets up is silent
and delayed: a third tag of any other length decodes to a body sliced at the
wrong offset, and every existing row stays green because the two tags that
already exist still agree. So the check that would catch it is exactly the check
nobody writes -- the round trip over a tag that does not exist yet.
The same defect had a second face the note did not name: each tag was spelled
TWICE, once rendering and once decoding, so the two spellings could drift
independently of the lengths. Both are one rule. The tags are named once and the
body is derived from the tag that MATCHED, so there is no offset to get wrong
and no second spelling to disagree.
PROVEN BY EXECUTION RATHER THAN BY INSPECTION, because "now it is decoupled" is
the kind of claim that reads as obviously true and is worth one run: with
cell_free_tag temporarily changed from "free|" to "released|" -- five characters
to nine -- both_slot_states_survive_the_round_trip still returns true. Under the
previous form that substitution sliced the free body at offset 5 and would have
failed. Tag restored, compile 0 blocking.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* compute fabric design (#9604)
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm ex…
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.
The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into
compile_dag_rust_emit_checkand not into its censussibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a4) the floor refuses
with
completed_over_cost_requirement=1andfailed=0:test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_ and_neither_mis_resolvesat 5812ms against the 5000ms fail-stop. That runcarries 259 per-claim
[floor-shared-fill]lines and NOT ONE of them names anyrow of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both
green_named_authority_sourceandgreen_own_declaration_source, each of which a later claim then reads free.Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and
run_claim_measuredperforms the same split it already performs.Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a
[floor-shared-fill]line these rowshave never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 noreply@anthropic.com
RELATION TO gunbc#9517, stated so the two are not read as competing. That PR
restores the ceiling to 500ms and freezes the 320 rows above it in
v2.workflow.floor_cost_debt, withheld from execution; six rows of this file,including this one, are on that roster by name. This PR touches no ceiling
constant and adds no debt row. It is the shrink-only contract's sanctioned
exit taken for these rows: made cheap, so the line can be deleted rather than
the witness withheld. If #9517 lands first, these six rows should leave its
roster on their own marginal cost rather than needing a freeze -- and the
finding above is why that is worth checking for the rest of the 320: a row on
that roster because it was charged another row's compile is on it for a reason
that is not its own cost, and a freeze makes that permanent.
WHAT IS NOT CLAIMED. The memo -- and therefore this attribution -- is armed
only under the floor's prepared-inventory guard, so no in-session run can
exercise it and none was attempted. The confirming measurement is this PR's own
floor phase. Read it as:
[floor-shared-fill] claim=test.claim.callable_ candidate_ambiguity_witness.*lines present (the arm-ran control, absent onevery main run to date) and
completed_over_cost_requirement=0. A singletiming is not evidence here in any case -- the budget carrier records a ~2x
ambient spread on shared hosts -- which is why the claim rests on the presence
or absence of the split line rather than on a number straddling a threshold.