Supplier bindings, per-supplier billing quantum, and an acquisition simulation by gunbai-bot[bot] · Pull Request #8960 · gunb-ai/gunbc

gunbai-bot · 2026-08-23T00:31:44Z

What this is

The first three layers of a CI cost broker: route each job to the cheapest admissible supply. This PR lands the supplier quoting layer and an acquisition simulation. It does not land workflow routing or a business ledger, and the scope section below says so explicitly rather than letting the module names imply it.

The defects this found, all caught by execution rather than by review

Per-minute squashed into per-hour was a 20x overcharge on short jobs. OfferQuote had no per-minute arm, so Ubicloud's published per-minute rate was being carried as an hourly one — and offer_quoted_total_for_grant rounds hourly up to whole billed hours, so a three-minute job priced as a full hour. QuotedPerMinute now exists. This is a correctness defect in the thing the product is.

Billing quantum was one synthetic hour applied to every supplier. It is now a per-supplier field on the offer, with 0 meaning continuous. That turns owned capacity's lack of increment waste from prose into a fact the selector can rank on.

The quantum was billed against the wrong magnitude. quantum_billed_slots(used_slots: taken, …) passed a job count into a parameter meaning a duration, so a 60-slot minimum rounded a slot's concurrency up to sixty instead of billing each of its jobs for sixty. Both are Nat, so it typechecked; running the witnesses is what disagreed.

A witness claimed a flip and asserted the same arm on both sides. demand_shape_alone_flips_the_acquisition_verdict asserted costs_more && costs_more under a comment promising opposite arms, and compared unequal means. It now holds mean demand equal at ten — flat ten every slot against six hundred once in sixty, the same 6000 job-slots — and asserts opposite arms.

Two types under one name. Qualifying the fabric's Offer to SupplierOffer collided with a projection in the Ubicloud binding that was already called that, making a field self-referential with nothing refusing. Renamed to SupplierOfferProjection.

The price authority was 20% stale. Refreshed to the 2026-08-22 first-party values, with the provenance note now separating what was READ from what is PROJECTED by the vendor's per-vCPU linearity, and recording that standard x64's absence is a first-party contradiction between Ubicloud's own two surfaces rather than a settled fact.

The first production supplier binding

SupplierOffer was previously constructed only in test fixtures — the selection fold had nothing real to rank. product.supplier.ubicloud is the first real one. It consumes the existing shape and price authorities rather than restating them, and it refuses rather than guessing where it cannot express a fact: memory and disk have no home in Shape, so they surface as UnexpressedSupplyFact, and the binding refuses to bind until provisioning delay is measured, because ready_at feeds the delay valuation.

Route on marginal, acquire on allocated

product.workload_simulation answers the acquisition question — does a commitment pay off under a given demand shape — deliberately separate from routing. Fusing the two is what talks operators into capacity they cannot fill. Deterministic and swept rather than stochastic, because a run-varying number cannot be a regression control.

Witnesses, all green by execution

witness	result
`flat_demand_at_committed_width_makes_the_commitment_pay`	true
`bursty_demand_of_equal_mean_makes_the_same_commitment_lose`	true
`demand_shape_alone_flips_the_acquisition_verdict`	true
`quantum_rounding_bills_a_partial_increment_as_a_whole_one`	true
`a_coarse_billing_increment_multiplies_the_rented_total`	true
`unplaced_work_refuses_the_verdict_instead_of_reporting_a_saving`	true
`committed_occupancy_separates_a_filled_lane_from_an_idle_one`	true

What is NOT modeled, stated so the names do not overclaim

Per-job arrival and duration; job identity; memory, disk and architecture as load-bearing routing facts rather than sidecar observations; the canonical selector (the simulation consumes lanes in caller order and says so — it does not silently stand in for a selector); customer tariffs, revenue, profit and margin; setup fees, minimum terms and included usage; queue delay and SLOs. workload_simulation is a capacity occupancy and cost comparator, not a workflow simulator and not a business model. Those are the next two cuts.

Known red

The main.rs regen divergence is tonight's fleet-wide class from #8691, fixed by #8953. Not hand-edited here — that is the laundering arm.

…e modeled advantage of owning

…olding

…ionPolicy 'Provider', 'Offer' and 'Selection' each name two unrelated things in this corpus: gunbc.dispatch_selection's ProviderOffer is an agent-runtime credential binding carrying no price, and product.fabric.supply's Offer is a priced compute-supply ask. They do not unify -- there is no proven coincidence to bundle, only a shared English word -- so the generic name goes to neither. dispatch_selection already qualifies its side; this qualifies ours.

…currency Executing the witnesses caught a units error in the simulation's billing core. quantum_billed_slots(used_slots: taken, ...) passed a JOB COUNT into a parameter meaning a DURATION, so a 60-slot minimum increment rounded a slot's concurrency up to sixty instead of billing each of its jobs for sixty. Both magnitudes are Nat, so it typechecked; only running it disagreed. Replaced by billed_slots_per_job, which states the model's standing assumption -- one slot is one job's runtime, and jobs of differing duration are not modeled until arrivals carry a duration -- rather than leaving it implicit. The shape witnesses were reworked in the same pass because their fixture moved two axes at once: a 60-slot increment against one-slot jobs is so dominant that owning wins under every arrival shape, which is a real effect but not the one those tests claim to measure. Renting now bills per slot there, so demand shape is the only thing varying, and the increment gets its own witness. The flip is now demonstrated at EQUAL MEAN -- flat ten every slot versus six hundred once in sixty, the same 6000 job-slots -- where it previously compared unequal means and asserted the same arm on both sides while its comment claimed a flip. All seven witnesses green by execution against a freshly built binary.

…d prices Three defects, two of them mine from the preceding commits. The rename collapsed two distinct types into one name. product.supplier.ubicloud already called its projection SupplierOffer, so renaming the fabric carrier to the same word made 'offer: SupplierOffer' read as the wrapper referring to itself. Nothing refused -- two types under one name is exactly the ambiguity resolved by silent last-import-wins -- so the projection is now named SupplierOfferProjection and says in its header why the name is load-bearing. Adding QuotedPerMinute left offer_affordability_for's inner match without an arm for it. This one the compiler DID refuse, which is the difference between a closed coproduct and a convention: the arm was missing from the moment the variant landed and the first resolve of a module that reaches it said so. The Ubicloud price authority still carried the 2026-07-21 read, which would have understated both premium x64 and arm64 by 20% in every projection the binding makes. Refreshed to the 2026-08-22 first-party values, and the note now separates what was READ at that date -- the two standard-2 rows -- from what is PROJECTED by the vendor's own per-vCPU linearity at the 16 size, so a later reader can tell an observation from an inference. It also records that standard x64's absence is a first-party CONTRADICTION between Ubicloud's own two surfaces rather than a settled fact, which needs its own carrier instead of a row quietly picking a side.

…the field name Addresses review 54950's unit-modeling block, which is correct and is the repository's own stated rule rather than a stylistic preference: std.measure's money_rate_billing_unit_note says an amount is never 'folded into a bare amount with the unit in the field name', and every money field in this module was literally variable_micros_per_slot: Nat. The reason it is worth the churn is specific to this model. Its central arithmetic multiplies a RATE by a DURATION and adds the result to a RUNNING TOTAL, and on bare Nat all three are the same type -- which is exactly how the billing quantum came to be applied to a slot's concurrency instead of a job's duration and typechecked the whole way. Money now flows through measure_add, measure_le and measure_scale_fraction_floor, so scaling a rate by a count is the only spelling that compiles and adding a slot count to a total has none. That is the construction move DESIGN section 5 prefers over a check. Counts stay Nat deliberately: slots, jobs, capacity and the occupancy permille are dimensionless tallies. Giving them a money carrier would be the same error pointed the other way, and the occupancy quotient the review also flagged is job-slots over capacity-slots with no money in it at all. money_difference is introduced rather than reached for in std because std.measure carries no subtraction and the omission is principled -- a Nat-backed measure cannot represent a negative result, so a general difference needs a refusal arm. Both call sites here have already established the ordering with measure_le, so the difference is total by construction and the guard belongs in the caller's branch. Also imports nat_max explicitly, which the review flagged: it was resolving ambiently while nat_min beside it was imported by name.

gunbai-bot · 2026-08-23T03:44:20Z

Addressed in 5371d9dada3. The unit-modeling block in review 54950 is correct, and I want to be specific about why it is correct here rather than just complying, because the failure it names had already happened in this module and I had not connected the two.

Fixed: money is now a carrier

Every money field is MoneyAmountMicro, and every money operation goes through measure_add, measure_le or measure_scale_fraction_floor:

was	now
`variable_micros_per_slot: Nat`	`variable_per_slot: MoneyAmountMicro`
`committed_micros_per_slot: Nat`	`committed_per_slot: MoneyAmountMicro`
`PlacementAccum.variable_micros: Nat`	`variable_spend: MoneyAmountMicro`
`RunAccum.variable_micros: Nat`	`variable_spend: MoneyAmountMicro`
`SimulationResult.{variable,committed,total}_micros: Nat`	`{variable,committed,total}_spend: MoneyAmountMicro`
`CommitmentPaysOff.saved_micros: Nat`	`saved: MoneyAmountMicro`
`CommitmentCostsMore.excess_micros: Nat`	`excess: MoneyAmountMicro`

The rule is the repository's own, not a preference: std.measure's money_rate_billing_unit_note says an amount is "never folded into a bare amount with the unit in the field name", and my fields were literally variable_micros_per_slot.

The concrete cost of not having done this. This model's central arithmetic multiplies a rate by a duration and adds the result to a running total. On bare Nat those are one type. That is exactly how the billing quantum came to be applied to a slot's concurrency instead of a job's duration — see the third commit on this PR, which fixed it. It typechecked the whole way and only executing the witnesses disagreed. So this finding is not adjacent to the defect this PR already fixed; it is that defect's root cause. Scaling a rate by a count is now the only spelling that compiles, and adding a slot count to a total has none — the construction move §5 prefers over a check.

Partly disagreed: two of the three cited expressions

I checked each of the three arithmetic sites the finding lists as "mixing money-micros with duration-slots".

line 123, billed * variable_micros_per_slot — agreed, this was rate × duration on bare Nat. Now measure_scale_fraction_floor.
line 173, committed_micros_per_slot * slots — agreed, same shape. Now measure_scale_fraction_floor.
line 236, the quotient — this one has no money in it. It is committed_slot_jobs * 1000 / (committed_capacity * slots), i.e. job-slots over capacity-slots, yielding a permille. All four operands are dimensionless tallies. It is unchanged and I believe it should be.

That distinction is load-bearing rather than pedantic: counts stay Nat deliberately. Slots, jobs, capacity and the occupancy permille are not money, and giving them a money carrier would be the same error pointed the other way. I have said so in the module header so the next reader does not "fix" it.

One new function, and why it is not in std

money_difference. std.measure carries add, scale and compare but no subtraction, and that omission looks principled: a Nat-backed measure cannot represent a negative result, so a general difference would need a refusal arm. Both call sites here have already established the ordering with measure_le, so the difference is total by construction and the guard belongs in the caller's branch rather than in a shared carrier. If you would rather this live in std.measure with an explicit refusal variant, say so and I will move it — I did not want to add a partial operation to a std carrier on my own authority.

The non-blocking note was right

nat_max was resolving ambiently while nat_min beside it was imported by name. Now imported explicitly. Worth flagging that ambient resolution is why it went unnoticed — the module resolved and ran green with the symbol never named in its import list.

Verification status

Three of seven witnesses re-verified green after the conversion, including all three that exercise the money arithmetic end-to-end through simulate and acquisition_verdict — flat_demand_at_committed_width_makes_the_commitment_pay, bursty_demand_of_equal_mean_makes_the_same_commitment_lose, and demand_shape_alone_flips_the_acquisition_verdict. The remaining four are still running locally; this container's CPU is heavily contended and each witness costs a full corpus resolve. I will post the completed table rather than leave this implied, and I am not claiming them green until they are.

— sent from neat-heron-312

gunbai-bot · 2026-08-23T03:51:39Z

Verification completed for 5371d9dada3. All seven witnesses re-run individually against a freshly built binary after the MoneyAmountMicro conversion, and all seven return true:

witness	result
`flat_demand_at_committed_width_makes_the_commitment_pay`	`true`
`bursty_demand_of_equal_mean_makes_the_same_commitment_lose`	`true`
`demand_shape_alone_flips_the_acquisition_verdict`	`true`
`quantum_rounding_bills_a_partial_increment_as_a_whole_one`	`true`
`a_coarse_billing_increment_multiplies_the_rented_total`	`true`
`unplaced_work_refuses_the_verdict_instead_of_reporting_a_saving`	`true`
`committed_occupancy_separates_a_filled_lane_from_an_idle_one`	`true`

This completes the table I said I would post rather than leave implied. Every verdict is unchanged from before the conversion, which is the result I wanted: moving money onto a carrier was meant to make a class of error unwritable, not to alter any answer. Had a verdict moved, the conversion would have changed behaviour and that would have needed explaining rather than reporting.

The quantum_rounding witness is worth calling out because it is the one whose subject the conversion changed. It asserts 60 * billed_slots_per_job(quantum_slots: 60) == 3600 — sixty concurrent jobs each billed sixty, not sixty between them. Under the old bare-Nat shape that expression and the wrong one were both well-typed; that is what this finding fixes at the root.

— sent from neat-heron-312

…iently CI refused with 'dag/test/claim/fabric_witness_run_test.dag:45:20: unresolved type Nat' on a fixture parameter I added. The file carries no import list at all and had been resolving every name ambiently. WHY LOCAL VERIFICATION COULD NOT HAVE CAUGHT THIS, which is the part worth recording. I verified with 'gunbc run', which resolves ambiently; the floor's strict preparation does not. So all seven witnesses passing locally was fully consistent with the floor refusing, and I had been treating evidence from the looser path as though it covered the stricter one. The two answer different questions. The review on this PR had already pointed at this exact hazard -- nat_max resolving without being imported -- and I fixed the one instance it named without asking where else the class applied. It applied two files over, in the fixture I had just edited. Both zero-import files this PR touches now import what they use, and every imported name was checked to exist in its module rather than assumed, since a name that does not exist refuses identically. Verified by running claim_executor --required-floor locally: strict preparation now completes with zero refusals and the fold proceeds into witness execution, which is precisely where CI stopped.

gunbai-bot · 2026-08-23T04:57:34Z

CI red fixed in b6328f9eebc. The failure was mine, and the reason it escaped local verification is worth recording because it invalidates how I had been reporting evidence on this PR.

The failure

dag/test/claim/fabric_witness_run_test.dag:45:20: error: unresolved type 'Nat'
required-ci: FAILED PHASE floor refused: subject=fa7a07325205bbaa modules_resolved=3829

I added a Nat-typed parameter to a fixture in a file that carries no import list at all and had been resolving every name ambiently.

Why my local runs could not have caught it

I verified with gunbc run, which resolves symbols ambiently. The floor's strict preparation does not. So "all seven witnesses green locally" was fully consistent with the floor refusing — the two paths answer different questions, and I was treating evidence from the looser one as though it covered the stricter one. Every green I reported on this PR was real, and none of it was evidence for the check that actually gates merge.

Worse, this PR's own review had already pointed at exactly this hazard — nat_max resolving while never appearing in the import list — and I fixed the single instance it named without asking where else the class applied. It applied two files over, in the fixture I had just edited. The non-blocking note was the more valuable half of that review and I under-read it.

Fix

Both zero-import files this PR touches now import what they use: Nat in fabric_witness_run_test.dag, and a full list in the new workload_simulation_witness_test.dag, which had never faced the strict path at all. I checked that all twelve imported names exist in their module rather than assuming, since a name that does not exist refuses identically and would have cost another CI round trip.

Verified against the check that failed, not the one that passed

Built claim_executor and ran --required-floor locally. Strict preparation now completes with zero refusals and the fold proceeds into witness execution — which is precisely where CI stopped. That is the discriminating evidence; re-running gunbc run would have reproduced the same false green.

One prediction of mine was wrong

I had said a red would most likely be the main.rs regen divergence. It was not. required-regen reported first_generation_equal=true and its declared_divergent=1 [main.rs] did not fail that phase. The floor was the only failing phase, and the regen class from #8691/#8953 was never implicated on this branch.

— sent from neat-heron-312

Addresses review 54991. The file already models every other duration it carries as std.measure's Second -- GrantDuration's two arms and AffordableUnderEstimate.duration_seconds -- so billing_quantum_seconds: Nat was not consistency with its neighbours, it was the one place in this file where the magnitude's name lived in the field name instead of in its type. It is also the same class fixed one commit earlier for money, and gating it behind a dissolve-on row while having converted money on principle would have been incoherent. The internal ceiling arithmetic still runs on unwrapped counts, and the header now says why: a value handed to measure_scale_fraction_ceil as num: is a dimensionless multiplier, not a duration.

CI floor: FAIL test.claim.pricing_surface_witness.witness_ubicloud_premium_2core_undercuts_github_2core_per_minute The witness pins ubicloud_premium_standard_2_price at 1600 micros/min. My 2026-08-22 first-party refresh moved it to 2000, so the witness went red -- correctly. That is what a pinned literal is FOR when the literal is grounded in an external authority, and it is the one thing that would have caught a price refresh applied to the carrier and forgotten everywhere else. DESIGN section 5 permits exactly this case and forbids its lookalike: a number copied from the current tree is a change detector, a number copied from a cited vendor page is an oracle. The header now says which one this is, so the next reader does not delete it as a snapshot. The economic claim it guards is unaffected -- GitHub 2-core at 6000 still exceeds Ubicloud premium at 2000, so Ubicloud still undercuts. The equality is what stops that ordering from being satisfied by a wrong number that happens to sort the same way. Verified by execution: the witness returns true. Checked for other pinned Ubicloud literals rather than fixing only the one that failed -- this is the sole site in the corpus outside the price authority itself.

Review 55030 flagged MoneyRate, ByteSize and HardwareThreadCount as unused in product.supplier.ubicloud. Checked each rather than applying the list: MoneyRate 0 uses removed HardwareThreadCount 1 use, in a COMMENT only removed ByteSize 2 real uses (UnexpressedSupplyFact's two arms) KEPT So the finding was right about two and wrong about one, and the one it was wrong about is the one a mechanical apply would have broken. HardwareThreadCount is the mirror case: my own first grep counted it as used because the match was inside prose, which is the same error pointed the other way. Verified by execution: the module still resolves.

gunbai-bot · 2026-08-23T07:54:30Z

Attribution of the remaining red, measured rather than asserted

This PR's last run failed 9 witnesses. Eight of them are main's, and one was mine. The one that was mine is fixed in a1e01373e34 and verified by execution.

The comparison, both runs against the same main commit 13db52a25:

run	failures
main `32621117917`	`passed=10343 known_red_held=36 failed=8`
this PR `32621649786`	`passed=10348 known_red_held=36 failed=9`

Main's eight, verbatim:

test.claim.fleet_intent_memory.srv2_population_matches_bmc_memory_summary
test.claim.runner_capacity_plan_witness.a_github_runner_in_a_fabric_slot_refuses_instead_of_reading_converged
test.claim.runner_capacity_plan_witness.a_width_above_the_committed_ceiling_is_refused_not_silently_unfulfilled
test.claim.runner_host_deploy.srv4_enables_six_named_runner_instances
test.claim.runner_slot_allocation_witness.an_identity_outside_the_committed_population_is_refused_not_classified
test.claim.runner_slot_allocation_witness.introducing_the_fabric_slot_deregisters_no_live_runner
test.claim.runner_slot_provision.witness_srv3_deploy_row_names_six_slots
test.claim.runner_slot_provision.witness_srv4_runner_count_six_materialization_target

This PR's nine were exactly those eight plus test.claim.pricing_surface_witness.witness_ubicloud_premium_2core_undercuts_github_2core_per_minute. Set difference of one, in the direction that identifies the owner.

The one that was mine, and why its red was correct

That witness pinned ubicloud_premium_standard_2_price at 1600 micros/min. My 2026-08-22 first-party refresh moved it to 2000, so it failed — which is what a pinned literal is for when the literal is grounded in an external authority. It is the one thing that would have caught a price refresh applied to the authority and forgotten everywhere else, and it caught it.

Updated to 2000 and annotated with which kind of literal it is, because it sits on a distinction §5 draws and a later reader could otherwise delete it as a self-copied snapshot: a number copied from the current tree is a change detector, a number copied from a cited vendor page is an oracle. The economic claim is unchanged — GitHub at 6000 still exceeds Ubicloud at 2000 — and the equality is what stops that ordering from being satisfied by a wrong number that happens to sort the same way. I checked for other pinned Ubicloud literals rather than fixing only the one that failed; this is the sole site outside the price authority itself.

Why the other eight are not mine, established before the result landed

My diff touches two files in the failing family — dag/gunbc/runner_slot_allocation.dag and dag/test/claim/runner_slot_allocation_witness_test.dag — so the coincidence is worth closing rather than waving away. The complete diff to both is three prose lines, rewording Offer to SupplierOffer inside comments. No declaration, expression or type reference changes. A comment cannot alter a witness verdict, and main fails the same two witnesses without this branch.

That family is the #8976 regression (CPU admission axis, DIMM-invalidated widths), currently routed to its owner. It was masked by the §4c annotation refusal until that was cleared by #8989.

Also worth flagging, not mine and not counted in `failed`

known_red_runtime_errored=170, the v2.test.lens_mock_totality.* family: enrolled expected-reds that threw instead of failing — no such function: <x>_published_mock_corpus. An enrollment asserts an expected verdict, and a claim that threw produced none, so 170 enrollments are currently asserting nothing while reading as held. Same count on main, so it is a corpus-wide condition rather than anything this branch introduced.

Net: this PR's own contribution to the failure count is zero. It will go green when main does.

— sent from neat-heron-312

gunbai-bot · 2026-08-23T08:36:15Z

There is nothing on this branch left to fix, and that is a measurement rather than a claim

Responding to the automated "CI FAILING @ 4505ce8 — push a fix" notice. I investigated rather than pushing something, and the correct action is no change.

The failure sets are identical

	run	result
this PR @ `4505ce8`	`32626195425`	`passed=10351 known_red_held=36 failed=8`
main @ `13db52a25`	`32621117917`	`passed=10343 known_red_held=36 failed=8`

Computed both directions of the set difference on the failing witness names:

in this PR but not main:   (empty)
in main but not this PR:   (empty)

Eight failures, the same eight. The previous run on this branch had nine — those eight plus my own witness_ubicloud_premium_2core_undercuts_github_2core_per_minute, which is fixed in a1e01373e34 and verified by execution. That fix is confirmed working by this run: the ninth is gone and no tenth appeared.

I computed the difference in both directions deliberately. One direction would only have shown that I introduced nothing new; the other is what rules out my branch masking a main failure, which would be the more dangerous asymmetry to leave unchecked.

What the remaining eight are

The #8976 regression — CPU admission axis and DIMM-invalidated widths — in runner_slot_allocation, runner_capacity_plan, runner_slot_provision, runner_host_deploy and fleet_intent_memory. It was masked by the §4c annotation refusal until #8989 cleared that, and is routed to its owner. Not mine to fix, and I am deliberately not duplicating it: I already opened a redundant PR for the annotation defect tonight before learning two other lanes had it in hand, and the lesson from that was to check ownership before writing the same fix a third time.

My branch touches two files in that family, so "not mine" needed evidence rather than assertion. The complete diff to both is three prose lines rewording Offer to SupplierOffer inside comments — no declaration, expression, or type reference. And main fails the same witnesses without this branch at all.

State

Six approvals, no REQUEST_CHANGES, mergeable=MERGEABLE, every review finding addressed, every witness this PR owns green by execution. This PR's own contribution to the failure count is zero. It goes green when main does, and pushing anything from here would be churn against a defect that is not on this branch.

— sent from neat-heron-312

…s the merge made silently Merges #8955 #8967 #8981 #8997 #9000 #9005 #9008 #9013 into one branch. Three resolutions carried real decisions, and two of them were invisible to git: - product.fabric.supply offer_fungibility_for: #8981 rewrote the body while main renamed Offer to SupplierOffer. Kept the new body on the current type name; unioned the import list. - gunbc.roadmap_style: #9005 and #8967 each added a panel in the same region. The first union interleaved the two rule sets into a file that parsed as garbage (expected LParen, found Ident) with NO conflict markers present. Redone as a real 3-way and checked at the block boundary. - roadmap_css_lift_parity_digest: both branches re-pinned it against a stylesheet holding only their own rules, so NEITHER value describes the merged sheet. Taking a side would have pinned a digest no emission produces. Re-derived by executing roadmap_css_derived_digest against this tree: e1434344ca3877e4. And one break git merged cleanly into a third file: #8960's t_offer_with_quantum predates #8981's required Shape.envelope and SupplierOffer.isolation, so the literal lost its type. Both branches were green alone; only the merged tree refuses. Repaired in the same style as t_offer beside it. Verified on this branch: 0 blocking parse errors (the 52 source-annotation diagnostics are pre-existing on main, same file, same count, measured with the same probe against a clean checkout); every witness in every changed test file passes.

…the diagnosis that outlived its deficit CI's floor found what my entry-scoped probe could not: dag/product/supplier/ubicloud.dag is a Shape/SupplierOffer construction site from main's #8960 that predates #8981 making `envelope` and `isolation` required. Same class as t_offer_with_quantum, different file, and the floor resolves 3866 modules where my probe resolved one import closure. The fill is not mechanical, and neither field takes a placeholder: envelope: the catalog publishes vcpus and memory_bytes, and this binding is the REASON #8981 added the field -- product.fabric.work records it, citing product.supplier.ubicloud by name. So memory is now EXPRESSED via cpu_memory_envelope, and MemoryNotExpressibleInShape is DELETED from UnexpressedSupplyFact rather than carried beside it. It would now be a false statement about the model. A diagnosis that outlives the deficit it diagnoses is worse than absent: it gets cited as a known gap while the gap is closed. Disk stays, because the storage axis is still unpopulated from this catalog and that fact is still true; the asymmetry is now the type's whole content. isolation: nobody has measured what a Ubicloud runner provides. The catalog carries vcpus, memory and disk and says nothing about kernel tenancy, namespacing or egress, so naming shared_kernel_sandbox_profile() would invent a vendor guarantee from a price list -- and worse than a wrong note, a broker would ROUTE work to it. The empty profile is fail-closed by construction: unsatisfied_isolation_guarantees filters the REQUIRED set against it, so every guarantee any work asks for comes back missing and the offer refuses BY NAME, while work requiring nothing still matches. The empty list alone would conflate "provides none" with "nobody looked", so IsolationNotObserved is added beside it as a stated coverage obligation. Censused every fabric Shape and SupplierOffer literal in the tree by hand afterwards rather than trusting one entry closure again: ubicloud was the last one. NOT FIXED HERE AND NOT MINE: the same floor run also refuses runner_slot_provision.dag:240 on a sole_constructor ArgvCommand. That site is untouched by this branch, is present on main, and main's own run 32646482842 is red on it. #9031 carries that repair.

…two breaks the merge made silently (#9023) * Subsume the fleet's disk reclaimer: model what has been holding slots at 2.5GB, before anything trusts a slot-width number A load-bearing fleet capacity mechanism runs on every runner host and has no representation in the substrate. ctrl-runner-reclaim.timer has been reclaiming runner workspace disk every 6h since 2026-07-23, and it is the reason slots measure ~2.5GB instead of the ~13GB its own header describes. Nothing in the corpus models it. READ FROM THE ARTIFACT, NOT FROM A DESCRIPTION OF IT. The model is derived from reclaim-runner-disk.sh and its .service/.timer, following the precedent runner_lifecycle_ctrl_void_note sets for exactly this case: read the ctrl artifact as ground truth, subsume it here, never invoke ctrl from gunbc. Reading it surfaced a fifth concern that a summary of the mechanism had dropped, and it is the sharpest one -- a review killed mid-run leaks a refs/heads/review/* ref, and once its object goes missing git gc dies AND writes a .git/gc.log that DISABLES ALL FUTURE AUTO-GC. The failure is self-perpetuating: the thing that would reclaim the disk is what the wedge turns off. NOT A SECOND HYGIENE AUTHORITY, and this is worth stating because the two were already being conflated. gunbc.host_hygiene_reaper reaps residual SLOTS -- stale cgroups, inactive units, control-override dirs -- and carries zero coverage of packs, repack, tmp_pack, _diag or docker; verified by grep against it and its _remediate half, all six terms zero. One word, "hygiene", over two mechanisms. So this is net-new modeling rather than wiring up an inert successor, and the module says where the boundary is. WHAT IS MODELED: the five growth paths as typed concerns; slot job state as a THREE-way fact (running / idle / unobservable) because "a job is running" and "we could not tell" refuse alike and repair differently; the repack decision as four arms rather than a Bool, so a consumer can tell "already packed" from "we did not look"; and the script's operator overrides carried as data rather than restated in prose. EVIDENCE, with the mutation that proves it discriminates. Seven witnesses green by execution. The control asserts the two refusals do not collapse to one answer; mutating the production arm so the unobservable case returns RepackRefusedSlotBusy turns that control RED (false) while its sibling stays GREEN (true) -- so it catches that specific defect rather than everything reddening. The fragmentation gate is asserted at both sides of the boundary, and the same 8GB checkout appears in the warranted and skipped rows so a gate that had drifted to charging on size would fail. WHAT IS DELIBERATELY NOT DONE: retiring runner_slot_disk_budget_per_slot. That literal is circular -- byte_size(40960000000), derived by its own annotation as "~38GB per slot at width 7 on 500GB class disk", which is the disk divided by the width it is then used to preflight -- and it measures ~16x observed occupancy. slot_observed_bytes is the observed quantity that replaces it. Per operator sequencing 2026-08-22 the reclaimer is subsumed first, because the width numbers are downstream of whether reclamation runs at all. Parse gate clean over 3881 modules. * Two age floors were bare Int days beside a Second: ground the day on the cited ISO 8601 authority (review 54879) review 54879 raised two findings on host_disk_reclaim, both real. reclaim_diag_max_age_days and reclaim_tmp_pack_min_age_days were flat Int scalars whose unit lived only in the identifier, sitting directly beside reclaim_per_repo_timeout: Second doing it correctly -- one module, two spellings for one concept. Adding Day to std.measure's Scale was the wrong repair: Scale is a closed coproduct, so a new member forces exhaustiveness churn across a load-bearing std module for one downstream field. Instead the day is grounded where the day already is cited -- extdeps.units.iso8601 gains iso8601_hours_per_day(), and std.measure composes seconds_per_day() from it exactly as minutes_per_hour() already delegates. Both fields now carry Second. Second finding: ObservationVerdict/UnknownRefused were imported and never used. Dropped, with an annotation recording WHY SlotJobState is not grounded on ObservationVerdict rather than leaving the next author to re-derive it -- ObservationVerdict answers whether a subject agrees with its desired state; SlotJobState answers what a slot is doing right now, as an input to a decision. A busy slot is not drifted, and reporting it as a convergence verdict would make correct operation read as a fault. Green by execution: the_two_refusals_do_not_share_one_answer -> true, the_fragmentation_gate_is_exclusive_at_both_sides -> true, and a new the_age_floors_keep_their_authored_ratio -> true. That one asserts the RELATION (diag floor is 3x the tmp_pack floor, both positive), not 259200 seconds: a literal transcribed from the same arithmetic that produced it is a change detector, red on a correct unit refactor and green if both floors were wrong by the same factor. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The fleet's disk reclaimer was installed by a script this repository could not see: model its service and timer, and teach systemd's authority the three directives that make it safe MVP step 2. gunbc.host_disk_reclaim models what the reclaimer DECIDES; this models how it is INSTALLED. The two are separate facts, and before this commit the second was authored nowhere in the repository -- a load-bearing, fleet-wide mechanism whose units were delivered by a shell script, so nothing here could observe it, converge it, or notice it had stopped. The extdeps extension is the load-bearing half. SystemdServiceDirective could not express Nice=, IOSchedulingClass= or TimeoutStartSec= -- the exact three directives that let maintenance share a host with live CI. A renderer missing them still produces a unit that RUNS; it simply competes with production for CPU and disk, so the omission is invisible in the rendered text and surfaces as someone else's latency. IOSchedulingClass gets a closed coproduct rather than a NonEmptyStr because the kernel closes that value set at three, and an authority that closes a set then carries it as a string has re-opened it. Two directives on the incumbent are deliberately NOT rendered. Documentation= points into the ctrl repo's copy of the script and goes stale on subsumption. EnvironmentFile=-/etc/default/ctrl-runner-reclaim is dropped for a stronger reason: it is an escape hatch of exactly the kind DESIGN section 5 forbids -- RECLAIM_GIT_GC disables the repack and RECLAIM_GIT_GC_MIN_PACKS moves the fragmentation gate, both of which are data rows here. A host carrying that file answers a different policy than the one modeled, silently. That is a deliberate behavioral difference from the incumbent, not a fidelity gap, and it has a standing witness because re-adding the line looks like an improvement. ExecStart still names the installed script. The terminal form is our own binary running slot_repack_decisions with no shell in the path, but that subcommand does not exist and a unit naming it would install a mechanism that cannot run -- strictly worse on a fleet whose disks fill without it. This is the gap-intolerant staged half of the replacement migration, taken deliberately, with its next-rung trigger named on the seam. Green by execution, six witnesses: the three resource directives reach the rendered text; the outer timeout is derived from the per-repo budget (asserted as the relation, not as 3600, so it cannot silently stop tracking); the derived value reaches the unit; no environment hatch is present; the timer drives the service persistently with jitter; and the three I/O classes do not collapse to one wire word. Corpus parse gate rc=0, 3884 modules, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * "Cut off a provider" names two actions with different blast radii: give the operator both controls, and let the unwired one refuse by name The operator asked for a capacity visualization AND control in the daily workspace -- turn a machine down, cut off a provider. This is the authority both halves read. WHERE A CONTROL HAS TO BIND TO BE REAL. Both axes meet at dispatch_selection provider_inventory_for_instance, which returns the ProviderInventory that selection resolves against. So cutting a runtime REMOVES ITS OFFER: the resolved selection has no constructor for a provider that made no offer, which is structural impossibility rather than a gate. A check placed after selection would concede that the selected-then-rejected state is writable. TWO AXES, NOT ONE ENABLED FLAG. Turning a machine down and cutting a runtime are different questions. Fusing them makes the smaller action unavailable -- an operator wanting Codex off everywhere would have to take hosts down to get it. They are two withdrawal rosters over two subject types. WITHDRAWAL, NOT ENABLEMENT. Rows name what is CUT OFF, so an unlisted subject is active. The inverse makes the roster load-bearing for ordinary operation: a host absent through an authoring slip goes dark. Withdrawal fails toward capacity remaining available, which is the recoverable direction -- too much capacity is a cost, too little is an outage. THE CONTROL NAMES ITS AXIS EXPLICITLY (operator ruling 2026-08-23). "Cut off a provider" could mean the runtime or one account binding, and the conflation is silent in the worst direction: an operator meaning "cut this Claude account" who gets Claude cut entirely discovers it as missing capacity, not as a refusal, because both readings are well-formed. So both controls exist from this first version and the unwired account axis REFUSES with a typed ControlUnbound carrying the axis and its trigger. An absent control would read as "not applicable here" -- the not-applicable-versus-malformed conflation. The axis is not hypothetical: a credentials update performing an active-slot swap restarted a live container on 2026-08-22, so it is already being operated by hand without a control. The decision takes its rosters as ARGUMENTS, with the global readers as thin wrappers, because the live rosters are empty and must stay empty -- a decision reading them directly would leave every refusal arm unreachable by any fixture, making the witnesses decoration that is cited as coverage. Green by execution, seven witnesses, plus the mutation proof: collapsing CapacityRefusedProviderWithdrawn into the host arm turns a_downed_host_and_a_cut_runtime_do_not_share_one_answer red while a_withdrawal_does_not_leak_to_its_siblings stays green. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Four control arms reported an effect that never happened: the control plans, and the gate that makes a cut real lands at the offer (review 54905) Two changes: the review 54905 repair, and the consumer that makes this authority non-inert. THE REPAIR, AND IT WAS THE FAIL-CLOSED FAILURE IN MY OWN DIFF. apply_capacity_control returned ControlApplied for CutHost, CutProviderRuntime, RestoreHost and RestoreProviderRuntime while actuating nothing -- the rosters are module-scope data rows, so a caller that cut srv3 and then read host_is_withdrawn(srv3) saw false immediately after being told the cut succeeded. The sibling witness asserting the rosters stay empty made the two claims jointly inconsistent by construction. That is DESIGN section 5 fabricated plausible output, and the existing witnesses could not see it because they compared outcome strings to each other rather than joining the control to the roster reader. WHAT ACTUALLY HAPPENS IS PLANNING, SO THE VOCABULARY NOW SAYS SO. ControlApplied is deleted; ControlPlanned carries the roster edit that would effect the request. Withdrawing capacity means authoring a row and committing it -- deliberately, so a withdrawal faces review like any other change to what the fleet does -- which is the same plan/apply split the fleet converge path already uses. The reviewer's proposed witness is now in tree in both directions: plan a cut, then READ THE ROSTER. Mutation proof that it discriminates: relabelling the planned arm "applied:" turns planning_a_cut_does_not_withdraw_anything_by_itself red. On the second finding, the Bool predicates are KEPT and the reason is recorded on them. Present => true / Absent => false is predicate dissolution and would block in std, but both callers -- the counts and the dispatch gate -- want the boolean and not the row, so dissolving would push a match over an Option whose payload is discarded into every call site. The Option readers are exported beside them. THE GATE. provider_inventory_for_instance now filters offers through the capacity authority, so a withdrawn host or runtime MAKES NO OFFER and ResolvedProviderSelection has no constructor for it. The declared inventory keeps its own function so the gate has an unfiltered denominator, and the withdrawn offers are returned separately: an inventory emptied by withdrawal and one empty because nothing is installed are different facts with opposite remedies, and a bare filter renders both as the same empty list -- the empty-observation narrow. capacity_admission collided with std.materialization_ladder; renamed to fleet_capacity_admission rather than aliased, since two spellings in one namespace is the fork. Green by execution: 9 control witnesses, 4 gate witnesses proving the gate CUTS (fixture-authored withdrawal, since the live rosters are empty and a gate reading them directly could only ever be witnessed neutral), plus 4 pre-existing dispatch_selection witnesses still green. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Put the fleet on the daily workspace: capacity at a glance, reading the same roster the dispatch gate reads The operator asked for live fleet info on the daily workspace. This is the panel. IT READS gunbc.fleet_capacity_control DIRECTLY, not a display copy. That is the whole difference between a control and a cockpit: a panel with its own roster drifts from the thing it claims to steer, and the drift is invisible because both sides stay internally consistent. WHAT IT SHOWS: a summary line (active hosts, active runtimes, committed slots), a row per host carrying committed width and per-slot memory ceiling with its capacity standing, and a row per provider runtime. Live values today: 4 of 4 hosts, 3 of 3 runtimes, 22 slots committed at 16 GiB each. EVERY NUMBER IS LABELLED COMMITTED RATHER THAN OBSERVED, IN THE RENDERED OUTPUT AND NOT ONLY IN A COMMENT. runner_slot_allocation states that srv3/srv4's width of 6 is a provisioning target -- two slots that do not exist yet -- while srv1/srv2's 5 matches live. A reader summing an unqualified column gets 22 for a fleet running 20, and a capacity decision made on that number is wrong on the only axis the panel exists to inform. An annotation cannot carry the qualifier because no operator reads the source. The withdrawn-slots line is ABSENT when nothing is withdrawn rather than reading zero: a standing "0 withdrawn" row is noise on every ordinary day and trains the reader to skip the row where a non-zero number finally matters. A DEFECT THE WITNESSES CAUGHT, WORTH RECORDING BECAUSE OF WHAT IT WOULD HAVE DONE. fleet_capacity_withdrawn_line bound its subtraction across a line break, so the second operand parsed as a separate term and the count was 22 rather than 0 -- the panel would have announced "22 slots withdrawn by operator control" on every page load, a fabricated claim on the operator's main surface, while the fleet was fully active. Found by nothing_withdrawn_means_no_withdrawn_line, not by reading. Green by execution, five witnesses. The load-bearing one serializes the ACTUAL daily workspace document and finds the panel in the HTML -- a witness over the fragment alone would prove it builds and say nothing about whether it is composed into the page. The slot total is asserted as a relation against gunbc_runner_slots_per_host rather than against the literal 22, so it goes red on a panel that silently stopped reading the allocation authority. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Regen the three drifting stage0 mirrors: two are this PR's own seed-closure edits, the third is inherited from main CI's regen phase refused at 38e95f3b14 naming three generated surfaces. Reproduced locally to a fixed point rather than guessed at. TWO ARE MINE AND ARE THIS PR'S OWN OBLIGATION. Adding iso8601_hours_per_day to extdeps.units.iso8601 and hours_per_day / seconds_per_day to std.measure -- the review 54879 unit-modeling repair -- put this change inside the v1 seed closure, so both modules owe a regenerated Rust mirror. The diffs are exactly those additions and nothing else. THE THIRD IS INHERITED AND IS REGENERATED, NOT AUTHORED. v1_compiler_emit_rust.rs drifts on main independently of this branch (three redundant `.clone()` removals from an emitter change whose committed mirror went stale); the drift was confirmed present on origin/main and on branches that do not touch the path. Regenerating a generated file is mechanical and idempotent -- if the owning lane lands the same regeneration the content is identical -- so this is installing the emitter's current output, not taking over someone's repair. Verified by execution rather than by inspection: claim_executor --required-regen refused with the same three files before, and returns first_generation_equal=true rc=0 after. The emitter was rebuilt from this branch's HEAD rather than reusing a stale binary, because main's emitter had itself moved -- generating mirrors with an old emitter is how you install an artifact CI then rejects. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Isolation becomes a fabric guarantee an offer can fail: seven named axes, a refusal that says which one, and the measurement that today's slots could not host a tenant Operator direction: slots need to be mutually exclusive, containerized, and ephemeral. This is the core half -- what work REQUIRES and an offer PROVIDES -- and it deliberately does not name a container. THREE GUARANTEES, NOT ONE, AND THIS FILE OWNS ONLY THE MIDDLE. Allocation exclusivity (may two grants reserve one cell) belongs to the durable grant store; a container provides none of it, and two brokers can each start one on the same cell. Ephemerality and sanitation belong to the lifecycle. Isolation -- what a run can observe once started -- is this. Conflating the sandbox with the exclusion wall is how a fabric double-books hardware while every run looks correctly isolated. THE MECHANISM IS ABSENT ON PURPOSE. OCI, nspawn, microVM and dedicated host are realization handlers; a core that named containers could not admit a supplier satisfying the same guarantees another way, which is DESIGN section 3's rule that transport sits outside the interface. THE MATCH RETURNS THE MISSING GUARANTEES, NOT A BOOL. "Not isolated enough" is unactionable; "cannot provide DedicatedKernel" tells a broker which supplier class to find. A Bool would collapse a shared-kernel host and a host with no namespacing into one answer with unrelated remedies. A MODELING ERROR I MADE AND CORRECTED BEFORE COMMITTING, because it is the more instructive half. I first gave the floor a FreshWritableRoot + AttemptScopedSecrets requirement and made the fleet-offer fixture claim the full sandbox profile so it would pass. Both were false: the floor has run green for months on slots providing neither, so the requirement invented a gap that does not exist, and the fixture asserted guarantees current_runner_slot_profile measures as absent -- a fixture lying to stay green. Corrected: the floor requires nothing and says why, the fixture states what the fleet actually provides, and the gap moved to tenant_workload_isolation_requirement, where it is real. CONSUMPTION STATUS IS DECLARED, NOT IMPLIED. offer_fungibility_for has no production consumer -- as its siblings ShapeNotCovered and CapabilitiesNotOffered already record -- so this is a modeled decision the broker will consume, not a live wall. The field and the arm that reads it land together, per the standing rule in fabric_witness_run after the inert-carrier lens caught an earlier declared-but-unread value. Green by execution, six witnesses. The gap witness asserts the COUNT of missing tenant guarantees (4) so that providing one turns it red rather than surviving partial progress, and it is paired with a control that today's slots STILL satisfy our own floor -- without which a match that refused every pairing would look like a working model. Adding the arm forced exhaustiveness at two existing match sites, which is the closed coproduct doing its job. Corpus parse gate rc=0, 0 diagnostics. NOTE FOR gunbc#8960: that PR renames Offer -> SupplierOffer. This adds a field and a fungibility arm to the same type against current main; whichever lands second carries the other through, and the content is mechanical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * A committed width cannot say what would buy more: name the binding axis per host, and report the unmeasured one as unmeasured The panel showed four hosts and a total. A total is the one number that cannot answer the question an operator actually has -- what unblocks more capacity -- because a committed width is a MINIMUM OVER AXES and the surviving number discards which axis produced it. THE AXES ARE NOT INTERCHANGEABLE PURCHASES. Where memory binds the remedy is DIMMs; where cores bind it is a different machine. A reader given only a fleet total assumes one story across four hosts. THIS IS ABOUT TO MATTER MUCH MORE THAN IT DOES TODAY, which is why it is authored now rather than after someone reads a total wrong. Measured now, memory binds everywhere and the column looks redundant. Once the CPU axis lands (gunbc#8976, relayed by warm-tern-755) srv1/srv3/srv4 become core-bound at 21 while srv2 stays memory-bound at 5 -- its 64 GiB DIMM install failed training and was reverted, so it holds 8x16 GiB where the others hold 8x64 -- and the single total becomes two unrelated stories at 68 committed against 20 running. THE UNMEASURED AXIS IS REPORTED AS UNMEASURED, NOT AS ADMITTING EVERYTHING. Disk returns DiskWidthUnconstrained on every host, and runner_slot_allocation's own reason string is explicit that this is "an unmeasured axis, not a measured all-clear". Rendering it as admitting any width would turn an absence of observation into a positive clearance. It is excluded from the BINDING set by construction: an axis that states no width cannot be at the minimum. host_binding_width_axes returns a LIST rather than a winner, because a tie is real information -- two axes at the same number means relieving either alone buys nothing -- and picking one would have to break the tie arbitrarily. TWO RAW LENGTHS BECAME DERIVED RESERVATIONS. The first revision wrote min-width 5rem and 9rem, which would have been the only untokened lengths in the stylesheet and would need re-tuning by eye whenever a label grew. They now derive the longest string each column can wear plus a gutter, following roadmap_component dispatch_reserved_width exactly. The metric column resolves to 35ch from "bound by memory · disk unmeasured"; a new host or a longer phrase moves it by derivation. CSS digest re-pinned to b6df98adc93f7077, derived by execution on this tree per the convention in that file -- never chosen -- with a re-pin note naming the rule family and its behavioral receipts. Green by execution: an unmeasured axis is not reported as binding, the binding axis sits at the committed width (asserted as a relation against gunbc_runner_slots_per_host, so a label authored independently of the arithmetic would go red), the panel renders it for every host, and the digest pin holds. Corpus parse gate rc=0, 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Hoist the isolation match out of the guard: it was computed twice on one input (review 54965) The guard and the IsolationNotProvided payload each called unsatisfied_isolation_guarantees on the same two arguments, so the fold ran twice per refusal. One let binding. Fixed rather than waved off as a nit on a two-element list, because DESIGN section 6's bare-minimum-cost rule is explicit that a proven cost-shape defect is always fixed regardless of the realized n: "n is small here" is not a time-stable fact, and pricing per-site exceptions is itself the redundant work the rule exists to avoid. The realized n grows with the guarantee set and with the offer roster a broker will eventually fold this over. Green by execution: the fleet offer is still eligible for the floor, a foreign trust domain still refuses despite ample capacity, and the shared-kernel offer still misses exactly [DedicatedKernel]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * An 8 GiB x64 workload was fungible with a 6 GiB arm offer: fold the resource envelope into the shape, and stop the identity dropping axes the matcher compares Reported by neat-heron-312 from the first production supplier binding (product.supplier.ubicloud), where memory and disk surfaced as UnexpressedSupplyFact. That is honest diagnosis and it does NOT repair the decision: a sidecar saying "memory was dropped" cannot route work. THE WRONG ANSWER, now executed as a witness. offer_covers_shape compared threads and nothing else, so an 8 GiB x64 need was declared FUNGIBLE with a 6 GiB arm offer whenever thread counts and the textual capability ref matched. The broker routes work to a machine that cannot run it and nothing downstream refuses, because fungibility already said yes. NO SECOND ENVELOPE WAS MINTED. gunbc.fleet_container already owned the requirement vocabulary -- CpuRequirement with its architecture axis, GpuRequirement, Memory, Storage, Network -- inside a model of OUR fleet's containers. Those are machine questions, not container questions: a bare-metal host and a rented VM answer them identically. So the five types moved verbatim to product.fabric.envelope and fleet_container now consumes them. A fact's home is its layer. EACH UNMET AXIS IS NAMED, for the reason the isolation match gives: "does not fit" is unactionable, "needs 8589934592 bytes, offered 6442450944" tells a broker which supplier class to find. Architecture is EQUALITY, not order -- there is no sense in which a bigger arm machine covers an x64 need -- and an axis the work does not state is skipped without being reported as checked. THE HALF A FUNGIBILITY FIX ALONE WOULD HAVE MISSED, and it was my own defect one PR earlier. work_identity_material hand-lists fields, and the isolation profile I added in #8981 never reached it -- so two works differing ONLY in what they require of their executor derived the SAME key and deduplicated onto each other, while fungibility compared the field. Identity and matching disagreeing about whether two things are the same work is exactly the divergence that module's own note records for threads. Both isolation and the envelope now feed the digest, with absence rendered as its own token so "no memory requirement" and "a requirement of zero" cannot collapse. ShapeNotCovered is DELETED rather than kept beside its replacement. It carried one axis, which ThreadsNotCovered now carries alongside the axes it could not express; nothing constructs it, and a variant every consumer must match and no producer can emit reads as coverage (section 4b(4)). Green by execution, seven witnesses: the reported wrong answer refuses naming BOTH failing axes, a larger same-arch offer still covers (positive control), a larger ARM offer does not cover an x64 need (the asymmetry that proves equality rather than order), an unstated axis neither refuses nor claims a check, and three material witnesses that memory, architecture, and stated-versus-unstated each change the work key. Four pre-existing fabric witnesses still green. Parse gate rc=0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The parse gate has a false-green mode, and this document caused it: the indexing line is not the verdict Three lanes adopted this recipe today on the strength of one clean run. Two of them hit failure modes the document did not describe, and one of them corrects a mechanism claim the document asserted. THE FALSE GREEN, which is the reason to fix this now. The run prints "indexed 3884 modules from 2 source roots" and SUCCEEDS at that step; the annotation-grain and parse diagnostics arrive after reconcile, at the very end -- 128 seconds on the box that measured it. Anyone who starts the command, sees a clean indexing line at 95 seconds and interrupts reads a defect-free tree that is not defect-free. That is worse than having no gate, because they will have "run the check". neat-heron-312 came within a minute of reporting the recipe as broken for exactly this reason. THE MECHANISM CLAIM WAS WRONG AND IS CORRECTED IN PLACE. This document said annotation grain is checked DURING INDEXING, and I repeated that to two other lanes in messages. It is not: indexing reads the sources and the refusal is raised later. What survives is the part that matters -- the diagnostic fires for modules the entry never imports and never compiles -- and it now rests on a measurement rather than on my reasoning about phases. THE GATE NOW HAS BOTH ARMS. A check that has never gone red is a decoration, and this one had only ever been run green. neat-heron-312 ran a discriminating pair on one tree with one binary: a planted in-body // in dag/product/workload_simulation.dag gives EXIT=1 with the located diagnostic, reverting gives EXIT=0 and 0 diagnostics. The planted defect sat in a module the trivial entry does not import -- six files compiled, 3884 indexed, diagnostic from one of the 3878 never compiled at all. That is stronger evidence for the trivial-entry trick than the argument that motivated it. THE STALE-BINARY MODE IS DOCUMENTED because it is the most expensive way this can go wrong. A binary predating --entry refuses the flag; falling back to a whole-corpus compile without an entry selects a parser that rejects // outright and returns ~25964 errors on a CLEAN tree (warm-tern-755, confirmed against a stashed HEAD). The degraded mode is loud and its output reads as a discovery rather than as a broken instrument -- the absorbing fallback with the failure wearing the costume of an answer. Five-figure error counts mean check your binary. Also recorded: the local gate locates by character offset while the floor gives file:line:col for the same class, so a mismatch against line numbers is expected rather than a broken grep. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Re-point the one citation the envelope move outlived (cited-symbol gate) Moving ResourceEnvelope from gunbc.fleet_container to product.fabric.envelope left a DeclarationRef in gunbc.doc_graph_roots naming the old home: cited-symbol: REFUSED DECLARATION-ABSENT gunbc.fleet_container ResourceEnvelope cited-symbol: FAIL 1 authored reference(s) do not resolve — a citation outlived what it names (DESIGN §3) Re-pointed to the new module. The declaration name and field are unchanged, so the citation names the same thing it always did. WORTH RECORDING RATHER THAN JUST FIXING: this is the §3 citation rule working exactly as designed, and it caught something no other gate would. The floor was green, the parse gate was green, every witness was green -- because nothing EXECUTES a doc-graph citation. It is a symbolic reference in a hand-authored plan binding, and the only thing that resolves it is the census built for that purpose. It is also the argument for symbolic citations over positional ones, made by execution rather than by assertion. A file:line pointer at the old location would have gone silently stale in the same move, with nothing able to detect it: a line offset is not reachable from the namespace tree, so no census could have refused it. The name was decidable, so it was refused, located, in one line. Verified: claim_executor --required-cited-symbol returns rc=0, "every authored reference resolves checked=390", where it refused before. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * A cell returns to supply only after teardown is proven, not when the process exits The operator asked for ephemerality: cleanup after customer jobs, fresh spawn with caching on every run. The load-bearing question underneath it is not HOW to clean but WHO DECIDES THE CELL IS CLEAN, and the tempting answer -- the job exited zero -- is wrong in a way that leaks one tenant's state into the next one's run. A job can exit zero and leave a detached child holding a mount, a populated writable layer, a secret tmpfs, or a live network namespace. So the exit status is an INPUT to sanitation and never its verdict, and this models the verdict. THE SPLIT THAT MAKES "FRESH SPAWN WITH CACHING" COHERENT rather than self-contradictory: the CELL (srv3-06) is a schedulable identity that persists across many attempts; the SANDBOX exists for exactly one attempt and none survives into the next. Fresh WRITABLE state per attempt, reused IMMUTABLE material underneath, and tenant code never edits the cache in place. SIX SEPARATELY-OBSERVABLE FACTS, NOT A `cleaned: Bool`. Each fails independently and each leaks something different, so a single boolean lets any one of them fail invisibly behind the others succeeding. An observation is three-valued, and the third value is the point: Unobservable says the readback could not REACH the fact. Collapsing it into Refuted would be safe but reports a failure that did not happen; collapsing it into Confirmed is how residue reaches the next tenant. They are kept distinct because their operator REMEDIES differ. THE DEFECT THIS IS SHAPED AGAINST is DESIGN's empty-observation narrow: a readback that confirms five facts and simply omits the sixth. A fold walking the OBSERVED list concludes "nothing was reported wrong" from a report that never covered the subject, and hands back a cell carrying the previous tenant's working tree. So the fold walks the REQUIRED list and demands an observation for each. Same narrow one level out: a host agent lost mid-attempt produces no readback at all -- exactly when the cell is MOST likely dirty -- so that yields every fact unobserved and quarantines with a full list, rather than nothing-to-clean. MEASURED, not asserted. Installing that precise defect in a copy of the tree and running all six witnesses: true a_fully_proven_teardown_returns_the_cell FALSE five_confirmations_and_a_silence_do_not_return_the_cell true an_unobservable_fact_refuses_reuse_without_claiming_teardown_failed true a_refused_teardown_names_the_fact_and_its_detail FALSE a_lost_host_agent_quarantines_with_every_fact_unproven true the_six_facts_do_not_share_a_wire_word Four of six pass the broken fold. That is the receipt for why those two witnesses exist and why a green suite here is not self-evidently meaningful: only the pair that walks the required list can see it. All six return true on this branch. The attempt's outcome is not a parameter of the verdict, and its ABSENCE is the enforcement -- there is no argument through which an exit status could arrive, so a caller cannot let a successful run stand in for a proven teardown (§5 construction over validation). An earlier draft also carried a same-signature forwarding function restating that in its name; it was a hollow alias with no caller, so the rule moved to the real function's header and the alias is gone. RUNG, honestly: this is a MODEL, and nothing observes a real cgroup yet -- current_runner_slot teardown is unmodeled and the readbacks here come from fixtures. The verdict logic is structurally guaranteed (a cell cannot be returned without a confirmation per required fact, because the constructor demands the list); the OBSERVATIONS are at mitigatable, since a host agent could report a confirmation it did not establish. Next-rung trigger: binding SanitationObservation to a real per-attempt readback on the host agent, at which point FactUnobservable stops being a fixture value and starts carrying real transport failures. Distinct from gunbc.host_disk_reclaim on purpose and stated in the module: that is a cadence over a host answering "healthy over weeks" and gates nothing; this is a barrier between two tenants, once per attempt, and is the only one that gates reuse. Folding them would make a slow disk-space job into a correctness dependency for every job start. Local parse gate: 0 diagnostics, rc=0, past reconcile. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The fleet's hardware reconcile had verdicts and no reader: render expectation-versus-observation, and keep "never read" out of "confirmed" The operator asked for live fleet info on the daily workspace. The capacity panel already shows committed slot widths; the HARDWARE those widths are derived from had no view at all. The inventory has been reconciling expectation against observation per host and producing typed verdicts the whole time -- gunbc.fleet_physical_inventory fleet_dimm_verdicts and fleet_processor_verdicts -- and nothing rendered them, so a disagreement between what the tree believes and what the machines report was reachable only by reading .dag source. THE COST OF THAT WAS ALREADY PAID. srv2's 64 GiB DIMM upgrade was modeled while the install failed training and was reverted, so the tree asserted a memory population the machine did not have and the slot widths computed from it were wrong on the one host that differed. The verdict existed and said so. Nobody could see it. THREE STANDINGS ARE NOT ENOUGH; THERE ARE FOUR, AND THE POINT IS THE ONES THAT ARE NOT REFUSALS. Confirmed and Refused are the obvious pair. UNREAD says no reading was taken, so there is nothing to disagree with. MISFILED says the observation was filed against a different host, so NEITHER machine has been assessed. Their remedies share nothing: go look at that host's DIMMs, go RUN a reading, go find out which machine was measured. Collapsing Unread into Confirmed asserts hardware nobody looked at; collapsing it into Refused sends the operator to inspect a machine that is fine. This is DESIGN's not-applicable-versus-malformed conflation on the axis where it currently costs the most. MEASURED, live, on the real fleet: 4 of 4 memory confirmed · 0 of 4 processor confirmed srv1..srv4 memory confirmed 8 sticks as expected srv1..srv4 processor unread no per-host processor reading exists... EVERY PROCESSOR ROW IN THE FLEET IS UNREAD. The part is modeled intent that every in-tree consumer agrees on, and no dmidecode receipt has ever been supplied for any host. A panel mapping "no contradiction found" to Confirmed would render four confirmations of a fact no instrument has measured, on the page the operator reads to decide what is true about their machines. THE DISCRIMINATING RED, measured rather than asserted. Installing exactly that collapse (ProcessorModelUnconfirmed => HardwareConfirmed) in a copy of the tree: FALSE every_processor_row_is_unread_and_none_is_confirmed true the_memory_axis_is_confirmed_on_every_host true the_four_verdict_shapes_map_to_four_distinct_standings true the_four_standings_do_not_share_a_wire_word true a_refusal_detail_carries_the_count_and_the_discrepancy_tally FALSE the_summary_reports_each_axis_separately_and_never_one_fraction Four of six pass the collapsed mapping. All eight witnesses return true on this branch. THE SUMMARY IS PER AXIS AND NEVER ONE FRACTION. Collapsed, it would read "4 of 8 confirmed" -- arithmetically true and useless. Memory is fully read; the processor axis has never been measured once. A solved problem beside an unstarted one, and averaging them hides both. Two live standings out of four means a mapping that collapsed the two UNOCCUPIED arms would pass everything the fleet can currently exercise, so those verdicts are authored in the witness rather than read from the roster. Same reason the mixed-population summary row is authored: the live rosters are all-confirmed and all-unread, and only a mixed input separates counting confirmations from counting members. The outstanding-contradictions line renders only when non-zero, and UNREAD deliberately does not count toward it -- nothing has been contradicted by a reading nobody took, and counting it would put the panel in a permanent alarm state the operator cannot clear by fixing anything. RUNG: the panel is a reader, and it inherits its subject's rung rather than adding one. The verdicts are the inventory's; this renders them without re-deriving them, so panel and reconcile cannot disagree -- the same reason the capacity panel reads the dispatch gate's own roster. Next-rung trigger for the processor axis is a dmidecode -t processor receipt per host, which is what turns four Unread rows into a real comparison; the panel is what makes their absence visible in the meantime. Column reservations derive from the longest label each column can wear (css_ch), following roadmap_component dispatch_reserved_width, so a new host or a longer standing word moves the reservation by derivation and there is no pixel to maintain. Local parse gate: 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Style the panel on the existing refused-state vocabulary, and re-pin the CSS digest by execution Two things the panel commit owed, and one real defect that only the whole-page consumer could find. THE DEFECT: the first draft painted the refused and misfiled standings with role_decl(prop: Color, r: SalienceRole). That COMPILED CLEAN -- 0 diagnostics, every one of the eight panel witnesses green -- and then failed at evaluation with NoSuchVariable { name: "SalienceRole" }. SalienceRole is a TYPE in gunbc.design.salience, not one of the theme roles role_decl accepts (CanvasRole, SurfaceRole, BorderRole, TextRole, TextDimRole, FigureRole, FocusRole, BoundaryRole). A name that resolves as a type and is then used where a value is needed passes the parse gate and dies on the page. Nothing in the panel's own witnesses could have caught it, and that is the point worth recording rather than just fixing: every witness tested the panel's LOGIC, and the stylesheet is not reachable from any of them. It surfaced within seconds of serializing the actual daily workspace, which is the consumer. A green witness file is not evidence the page renders. THE FIX is not a new role. var(--band-loud) is the established refused-state vocabulary in this stylesheet -- the activity obligation row already paints [data-state="refused"] with it -- so the panel reuses it rather than minting a parallel one for the same meaning. Confirmed and unread stay dim, unread additionally italic, so the four standings are distinguishable by material and not by colour alone. RECEIPT, by serializing the real page rather than the panel function: 233,714 bytes, the .fleet-hardware-standing section present, the summary line rendering "4 of 4 memory confirmed · 0 of 4 processor confirmed", four unread cells, and all twelve .hardware-* rules emitted. The derived reservations land as 6ch and 11ch -- 11 being the width of "confirmed", the longest of the four standing words plus the gutter -- so they are computed, not typed. THE RE-PIN: roadmap_css_lift_parity_digest moves 25d65c956b7578ca -> 9f37abcc65255edf, DERIVED by running roadmap_css_derived_digest against this tree, never chosen. The accompanying note states what moved and why. The two neighbouring digests deliberately did NOT move, and that is scope evidence rather than an absence of checking: moodboard_css did not move because this adds no rule it covers, and moodboard_html did not move because it renders the thesis and principles rather than the stylesheet. A change that had leaked past the roadmap stylesheet would have moved them too. Both re-run green here alongside the re-pinned one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The slot-total witness assumed two symmetric pairs; name all four hosts instead CI caught a real regression in my own witness after merging main. WHAT BROKE. The row asserted the panel's total equals srv1 * 2 + srv3 * 2 -- true only while the fleet was two symmetric pairs. #8976 made CPU an admission axis and the symmetry ended: srv1/srv3/srv4 became core-bound while srv2 stayed memory-bound on 8x16 GiB, because its 64 GiB upgrade failed training and was reverted. The doubling was never the property under test; it was a shortcut that happened to hold, and it turned a genuine fleet asymmetry into a red on a witness about summing. That the witness went red is correct behaviour -- it noticed the fleet changed shape. What was wrong is what it asserted. THE ATTRIBUTION, checked rather than assumed, because a red on my branch after merging main is exactly the case where blaming main is convenient. Main's own run 32621117917 at 13db52a25d fails EIGHT rows (fleet_intent_memory, runner_capacity_plan x2, runner_host_deploy, runner_slot_allocation x2, runner_slot_provision x2 -- all downstream of the same reverted DIMM upgrade). My branch failed NINE. The one difference is this row, and it is mine. THE FIX names all four hosts. That keeps the join the row exists to make -- the panel's total must equal the allocation authority's per-host widths -- while carrying no assumption about which hosts resemble each other, so a future asymmetry moves the number without reding the row. It also stays a real oracle rather than collapsing to measure() == measure(): the right side reads gunbc.runner_slot_allocation, a different authority from the panel fold on the left. Summing the panel's own fold on both sides would have been the quiet way to make this green and would have asserted nothing. Verified: this row and the three others in the file return true. The remaining eight failures are main's and predate this branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * A refused serialization answered as an empty page, greening every negative assertion (review 55040) Non-blocking review finding, and it is the absorbing fallback in my own witness file, so it is worth fixing rather than noting. empty_workspace_html matched the emission and returned "" on EmitRejected. That is ⊥-as-answer conflated with ⊥-as-ignorance: every !string_contains assertion in this file is SATISFIED by the empty string, so a total serialization failure would have rendered the negative rows green, while the positive rows could not distinguish "the panel is missing from the page" from "nothing serialized at all". Two states with opposite remedies collapsed into one answer, and the collapse fails in the quiet direction. Three changes, none of which widen: The emission is now its own function returning the typed result, so the refusal is available rather than discarded at the point of use. The rejected arm carries the reason instead of vanishing, prefixed with a marker no assertion in this file searches for -- so a positive assertion fails on it, the text names what happened, and the marker cannot accidentally satisfy an assertion either. The refusal gets its own row. Without one it is only ever observed indirectly, through whichever assertion happens to notice the page is not what it expected, and the ledger would read "the panel is absent" for a run where nothing was emitted. the_workspace_actually_serializes makes it a finding with its own name. The one row carrying a negative assertion over the HTML now also rests on the emission having succeeded. The reviewer's second note -- host_is_withdrawn / provider_is_withdrawn being Present => true / Absent => false -- I am leaving as it stands, and the reviewer read it the way I intended: both real callers want the Bool, the Option accessors are exported beside them, and dissolving the predicate would push a discarding match into every call site. The module already flags the tension; that is the honest state rather than a resolved one. Verified: all four rows over the serialized workspace return true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Nothing prevents the allocator from consuming the thing that allocates: three measurements and a ruling Capacity has classes. Customer execution -- CI, agent tasks, batch -- is offerable. Control plane -- scheduler, reconciliation, admission, receipts -- is not: if control capacity appears as available vCPU, available RAM, or a cheap slot, the allocator can schedule customer work onto the resources that run the allocator. Nothing in the fabric supply model expresses that distinction, so nothing refuses it. THREE MEASUREMENTS, because any one alone is answerable and only together are they a finding. 1. NO CAPACITY CLASS ANYWHERE. Searched ControlPlane / control_plane / CapacityClass / capacity_class / Customer / customer across product.fabric.supply, identity, work and gunbc.dispatch_selection. One hit: the word "customer" inside a prose comment about displacement. No type, field or arm names the distinction. The hit is CARRIED rather than rounded to zero -- "no hits" is the claim a re-run falsifies, "one hit, in prose, here is why it does not count" survives the re-run. 2. THE PLAUSIBLE CARRIER CANNOT HOLD IT AS A FACT. The only field shaped to carry it is TrustDomainRef, a NonEmptyStr where brand. A branded string carries the class only as a magic value agreed between producer and consumer -- convention standing where necessity was available. That is WORSE than the current absence, because absence is visible and a convention reads as coverage. 3. THE PROTECTION HAS NO REACH ACROSS THE SEAM, and this is the one that changes the picture. gunbc.fabric_control_plane_charge is real and host-parametric: on the owned fleet a control-plane resident is SUBTRACTED from what a host can commit, which is why control capacity never becomes offerable there. Its importers are ci_runner_placement, fleet_host_budget, itself and one witness -- all fleet-side. Zero references to it or to fleet_host_budget anywhere under product/. So the protection does not WEAKEN at the external-supplier seam. It was never present on that side of it. Reading "control-plane capacity is charged" as a property of the fabric is authority substitution: the fact lives in one carrier, the operation is governed by another, and no carrier claims the arrow between them. THE RULING, from the product-direction lane: THE CLASS GOES ON THE WORK, NOT THE OFFER. An offer is a thing a SUPPLIER SAYS ABOUT CAPACITY. Putting the class there asks the party with the least knowledge and the most incentive to say yes to make the safety assertion, a supplier that omits the field is admitted, and the claim is unfalsifiable from our side. We originate the demand, so we hold the fact. Both refused remedies are KEPT with their reasons rather than deleted, and the witness asserts their reasons are distinct: the offer arm is refused on an AUTHORITY question, the trust_domain arm on a REPRESENTATION one. A shared "not ruled in" would lose exactly the distinction that stops someone arguing the second is fine once the first is addressed -- and the trust_domain shortcut is cheap, looks like modeling, and is the one a later reader will reach for. THE MEASUREMENT BASE IS NAMED. The Offer field census was taken on gunbc#8981's head, the widest that record has ever been. Measuring the narrower record on main and reporting "no capacity class" would have been true of a smaller surface and invited the reply that the field landed since. RUNG: this class sits BELOW mitigatable -- there is no failure to contain, the invalid state is simply representable and unremarked. It is not on the ladder. Next-rung trigger: the ruled remedy landing on Shape, at which point it becomes a matching refusal and can be measured as one. Nothing here is consumed by admission and the module says so; this row keeps the gap countable rather than rediscovered. ONE THING I MEASURED THAT A READER WOULD OTHERWISE GET WRONG. The eight DeclarationRefs here look like the ones the cited-symbol gate enforces. They are not: a fabricated decl_name leaves the gate green at checked=390, unchanged, before and after this module gained an importing witness. That is a DECLARED scope rather than a defect -- the lens's law enrolls doc-graph binds, "structural, not corpus text scan", and its dissolve-on already names widening to every carrier. Recorded in the module because a citation that looks enforced and is not is worse than a plain string. Five witnesses green; local parse gate 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The Spark slot assignment was decided the same day this note said it was missing: a rotted REASON, not a rotted line fleet_intent_network refused to author the srv5/srv6 endpoints because "the operator supplied the router table but never stated the assignment", so choosing an address would be a 50/50 guess and therefore the fabricated-plausible-output failure DESIGN §5 forbids. THE DECISION EXISTS AND IS ONE IMPORT AWAY. gunbc.spark.dgx_procurement `dgx_spark_router_binding_operator_allocation` records srv5 taking spark-a3ee and srv6 taking spark-3bd5, decided 2026-08-07 under an explicit operator delegation, on an ascending-address-order basis kept precisely so the tie-break is attributable rather than looking like a measurement. `srv5_router_binding` and `srv6_router_binding` are both SlotAssigned carrying it. Both notes are dated 2026-08-07 -- the stated blocker was resolved the day it was written. THE DOCTRINE WAS INVOKED AGAINST THE WRONG TARGET, which is why this is a correction rather than a refresh. §5 forbids fabricating an OBSERVATION. An attributable ALLOCATION with a decider, a date and a basis is not one -- it is exactly what the operator delegated. So the module was refusing on the grounds that a decision had not been made while the decision sat one import away. THIS IS THE STALE-CITATION CLASS IN ITS EXPENSIVE FORM: a rotted REASON rather than a rotted line number, and unlike a stale line it propagates by being believed. A lane read it, concluded Spark work was blocked on an operator fact, and reported that upward before anyone opened the procurement carrier. WHAT THIS DELIBERATELY DOES NOT DO: no endpoint row is added, and `endpoints` / gunbc.fleet_intent's ComputeHost list are unchanged. In this module that membership IS enrollment -- the module says so structurally, which is a good decision, so that naming an identity cannot be mistaken for enrolling it. Authoring the rows would enroll the units, not describe them, and there is nothing to enroll into while they are unplugged and the converge timer is retired. A PROJECTED ENDPOINT ALSO CANNOT LIVE HERE, and that is structural. gunbc.spark.dgx_procurement imports THIS module for operator_host_srv5/srv6, so the reverse import is refused by the import graph's one law. Measured, not inferred -- I added the import and compiled: circular dependency detected: gunbc.fleet_intent_network -> gunbc.spark.dgx_procurement Recorded in the note so the next person starts from the constraint rather than the idea. ONE METHOD NOTE WORTH MORE THAN THIS DIFF. My FIRST probe of that cycle reported ZERO diagnostics and I nearly recorded "no cycle". The trivial parse-gate entry never imports this module, so the cycle was never on the resolve path; it appeared only once the probe entry actually reached the module I had changed. Stated generally: A CLEAN COMPILE IS NOT EVIDENCE OF NO CYCLE UNLESS THE ENTRY REACHES THE MODULE YOU CHANGED. That is an absence produced by machinery that never performed the measurement, rendered identically to a real zero -- the same class as a green gate whose census never reached your file. The citation is symbolic, module and symbol, no line number (§3). Local parse gate with an entry that DOES reach this module: 0 blocking. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * The axis column reserved the widest HOSTNAME for words that are not hostnames (review 55065) `.hardware-axis` took `hardware_subject_reserved_width()` — copied from the column beside it — so a column carrying "memory" and "processor" was reserved to the width of the longest HOST LABEL. Two unrelated populations that happen to be adjacent, and the derivation read the wrong one. Emitted 6ch for a column whose longest word is nine characters. That it looked derived is what made it survive review twice, mine included: the call is a derivation, it just derives from the wrong population. A hardcoded `11ch` would have been more obviously wrong. FIXED BY GIVING THE AXIS WORDS AN AUTHORITY. `hardware_axis_labels()` is now the one list, read by both the rendered rows and the reservation, so a third axis widens the column by derivation rather than by someone noticing. Emits 11ch, and the rows still render "memory" / "processor" from that same list rather than from their own literals. THE WITNESS ASSERTS THE DISCRIMINATING FACT, NOT THE TAUTOLOGY. A row checking that the axis width is derived from the axis labels would be `measure() == measure()` — it would pass against the defect too, because the defect is also a derivation. What separates them is that the subject population CANNOT HOLD the axis one: host labels are four characters, "processor" is nine. So the row asserts the two reservations differ and that the axis words are longer than any host label, which is exactly the condition the copy-paste violates. Digest re-pinned 9f37abcc65255edf -> becaf5e24965215d, derived by executing `roadmap_css_derived_digest` against this tree, never chosen. `moodboard_css` deliberately did not move and re-runs green beside it, which is the scope evidence that this touched only the roadmap stylesheet. Local parse gate: 0 diagnostics. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012q31BK3okLA8vG4kdTWtBf * Consolidate eight approved fabric/fleet PRs, and repair the two breaks the merge made silently Merges #8955 #8967 #8981 #8997 #9000 #9005 #9008 #9013 into one branch. Three resolutions carried real decisions, and two of them were invisible to git: - product.fabric.supply offer_fungibility_for: #8981 rewrote the body while main renamed Offer to SupplierOffer. Kept the new body on the current type name; unioned the import list. - gunbc.roadmap_style: #9005 and #8967 each added a panel in the same region. The first union interleaved the two rule sets into a file that parsed as garbage (expected LParen, found Ident) with NO conflict markers present. Redone as a real 3-way and checked at the block boundary. - roadmap_css_lift_parity_digest: both branches re-pinned it against a stylesheet holding only their own rules, so NEITHER value describes the merged sheet. Taking a side would have pinned a digest no emission produces. Re-derived by executing roadmap_css_derived_digest against this tree: e1434344ca3877e4. And one break git merged cleanly into a third file: #8960's t_offer_with_quantum predates #8981's required Shape.envelope and SupplierOffer.isolation, so the literal lost its type. Both branches were green alone; only the merged tree refuses. Repaired in the same style as t_offer beside it. Verified on this branch: 0 blocking parse errors (the 52 source-annotation diagnostics are pre-existing on main, same file, same count, measured with the same probe against a clean checkout); every witness in every changed test file passes. * The last construction site the merge stranded: ubicloud's offer, and the diagnosis that outlived its deficit CI's floor found what my entry-scoped probe could not: dag/product/supplier/ubicloud.dag is a Shape/SupplierOffer construction site from main's #8960 that predates #8981 making `envelope` and `isolation` required. Same class as t_offer_with_quantum, different file, and the floor resolves 3866 modules where my probe resolved one import closure. The fill is not mechanical, and neither field takes a placeholder: envelope: the catalog publishes vcpus and memory_bytes, and this binding is the REASON #8981 added the field -- product.fabric.work records it, citing product.supplier.ubicloud by name. So memory is now EXPRESSED via cpu_memory_envelope, and MemoryNotExpressibleInShape is DELETED from UnexpressedSupplyFact rather than carried beside it. It would now be a false statement about the model. A diagnosis that outlives the deficit it diagnoses is worse than absent: it gets cited as a known gap while the gap is closed. Disk stays, because the storage axis is still unpopulated from this catalog and that fact is still true; the asymmetry is now the type's whole content. isolation: nobody has measured what a Ubicloud runner provides. The catalog carries vcpus, memory and disk and says nothing about kernel tenancy, namespacing or egress, so naming shared_kernel_sandbox_profile() would invent a vendor guarantee from a price list -- and worse than a wrong note, a broker would ROUTE work to it. The empty profile is fail-closed by construction: unsatisfied_isolation_guarantees filters the REQUIRED set against it, so every guarantee any work asks for comes back missing and the offer refuses BY NAME, while work requiring nothing still matches. The empty list alone would conflate "provides none" with "nobody looked", so IsolationNotObserved is added beside it as a stated coverage obligation. Censused every fabric Shape and SupplierOffer literal in the tree by hand afterwards rather than trusting one entry closure again: ubicloud was the last one. NOT FIXED HERE AND NOT MINE: the same floor run also refuses runner_slot_provision.dag:240 on a sole_constructor ArgvCommand. That site is untouched by this branch, is present on main, and main's own run 32646482842 is red on it. #9031 carries that repair. * gib_label divides by the authority, not by 1073741824 review 55104, advisory. The literal was a correct number and a second representation of one std.measure already owns: gibibyte_scale_factor_bytes builds it from extdeps.units.iec_80000_13 iec_kibi_factor. Display-only is not an exemption -- that literal is what a GB/GiB confusion is made of, and the authority is what already settled which one this is. All 10 fleet_capacity_panel witnesses pass, including the whole-page serialization row. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

…(carrier-exactness recut) (#8990) * Split the encode refusal domain out of the decode one, so the load classifier cannot name a state the loader cannot produce Recut item 1 of 7. This is a correctness fix, not carrier tidying. THE DEFECT. ClosureDocIncompleteWithoutAdmission is produced by encode_closure_document_checked and by nothing else -- no decode path reaches it. It nevertheless sat in ClosureDocRefusal, which closure_document_load_standing matches EXHAUSTIVELY. So the load classifier was obliged to assign a standing to a state loading cannot produce, and it answered LoadDocumentMalformed -- which standing_may_supersede_generation makes the ONE standing permitted to supersede a newer document. An encode-only state had a route to "may overwrite". This is a closed match over a dishonest domain: exhaustiveness is satisfied, the compiler is content, and the arm answers for something that cannot occur. Nothing was miswritten; the TYPE was wider than the operation's domain. THE FIX is not a new guard. ClosureDocEncodeRefusal now carries that arm and ClosureDocEncodeOutcome refers to it, so the classifier's parameter can no longer express the cause. The question stops being answerable rather than being answered correctly -- DESIGN section 4b's top rung, unrepresentable rather than validated. EVIDENCE, and the control is the half that makes it evidence. A temporary paired probe, both files staged so they reached the remote runner: probe closure_document_load_standing(cause: ClosureDocIncompleteWithoutAdmission{..}) -> error: type mismatch: expected 'Coproduct(ClosureDocRefusal)', got 'Coproduct(ClosureDocEncodeRefusal)' control closure_document_load_standing(cause: ClosureDocNotAnObject) -> typechecks PAST the same call; fails only at the ProcessExit boundary, which is the host's return-type rule, not a typecheck Without the control the probe's failure would have been satisfied by any breakage at all -- a typo, a bad import, a wrong module name. The control proves the module loaded, the imports resolved and the call typechecked, so what the probe refuses is the domain split and nothing else. Both probe files are deleted in this commit: they declare no test fn and must never enrol, since a file designed to fail compilation would red the floor for everyone. Runtime suites green after the split: commit_closure_witness_main exit=0, load_standing_witness_main exit=0. ONE CONSEQUENCE STATED RATHER THAN HIDDEN. cause_is_incomplete_without_admission is now total by construction -- ClosureDocEncodeRefusal has one arm, so the match can only answer true, and by this stack's own standard that is a decoration. It is kept, because it is the correct residue of a climb: the check did not get stronger, it became unnecessary, and section 4b(4) keeps the evidence enrolled while the obsoleted discrimination goes. What replaced it is a compile-time property no Bool-returning witness can express, which is why the probe above is recorded here rather than enrolled as a claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bind the partial-closure admission to its subject, so a token for A cannot authorize encoding B Recut item 7, and the one the design thread called the highest-priority correction. This closes the authority-substitution hole #8965 declared as honest rung debt rather than fixed. THE DEFECT. PartialClosureAdmission { reason } carried no subject. The encoder took a closure PLUS an optional admission and checked only that one was PRESENT: admit closure A -> token T encode closure B with T -> ACCEPTED sole_constructor did not prevent it: .dag has no module privacy, so it blocks the record literal while the public mint stays freely callable. Nor could the existing mutation have caught it -- deleting the check proves the check is READ, which a bearer token satisfies perfectly. That is why this sat at mitigatable with the rung declared instead of claimed. THE REPAIR IS A SHAPE, NOT A CHECK. AdmittedPartialCommitClosure holds the closure it admits, and encode_admitted_partial_closure_document takes ONLY that carrier. There is no second closure to disagree with it, so "a token for A used on B" is not refused at runtime -- it has no spelling. The partial encode entry performs no validation because nothing is left to validate. `unresolved` is DERIVED at the mint from the closure it is given. A caller-supplied population would reintroduce the same substitution one field down: an admission truthfully about A, carrying B's missing objects. DISCRIMINATOR, and it had to be re-derived rather than copied. The thread specified "admission for A used with B -> refuses or cannot be constructed", but after the reshape the mismatch CANNOT BE PASSED -- one parameter, closure is a field -- so a probe passing a second closure would only be an arity error. The single remaining forgery route is hand-assembling the carrier: probe AdmittedPartialCommitClosure { closure: <never minted>, .. } -> error: sole_constructor type 'AdmittedPartialCommitClosure' cannot be constructed outside its defining module (exit 1) TWO CLAIMS ADDED, both executing: an_admission_names_the_objects_it_admits_as_missing -- the population is the closure's own, not a caller's assertion the_mint_refuses_a_complete_closure -- admitting a partial write for something with nothing missing is a category error, and this is what keeps the mint honest about deriving rather than trusting Suites: commit_closure_witness_main exit=0 (12 claims), load_standing_witness_main exit=0 (6 claims). THREE DEVIATIONS FROM THE PROPOSED SHAPE, each deliberate. NO NonEmptyList. The corpus has none, and minting one for a single field would grow net concepts to buy a guarantee the mint's refusal already provides. So the SUBJECT BINDING is structural while the emptiness exclusion stays mitigatable -- `unresolved: List` can represent an empty admitted population even though this mint cannot produce one. Next-rung trigger: a NonEmptyList authority earning its place from more than one consumer. NO one-member refusal coproduct. `type X = OnlyArm` does not declare a nullary variant, it reads as a type alias and fails to resolve. The refusal is an arm of PartialClosureAdmissionOutcome instead; a second genuine refusal joins that coproduct and every match fails to compile at the match, which is what the nesting was for. TWO ENCODE ENTRIES rather than one with an optional token: encode_complete_closure_document refuses anything uncontained; encode_admitted_partial_closure_document is total because the mint settled it. COVERAGE OWED, NOT CLAIMED. scm_commit_closure_json_v2_witness_test.dag has no ProcessExit driver, so the three call sites retargeted there are typechecked but NOT executed. The floor is the only thing that runs them and it is currently refusing for an inherited reason, so that execution is owed once main reopens. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Narrow the repository encode refusal to the one cause encoding can produce, and give that arm its first witness Recut item 6. Same dishonest-domain class as item 1, one layer up. THE DEFECT. RepositoryEncodeClosureDocRefusal wrapped the WHOLE ClosureDocRefusal decode population -- fifteen causes -- while encode_repository_checked produces exactly ONE of them (ClosureDocEdgeTargetUnresolved) from exactly one place. A consumer matching this arm had to handle format-tag and unknown-connective causes that no encode path can raise, and a reader could not tell from the type which were real. The type answered for a domain it does not own. It also round-tripped an identity through text: the arm carried a rendered key while its two sibling arms carry ObjectId directly. An identity left as a string is one nobody can resolve back. Both are fixed by RepositoryEncodeUncontainedTarget { target: ObjectId }, with first_uncontained_target returning the domain type instead of a key. THE ARM HAD NO WITNESS, AND THE GREEN SUITE IS HOW I ALMOST MISSED IT. All three suites passed after the change. But the encode-cause helper enumerates three tags and the claims asserted only two -- "commit_root" and "checked_out". Nothing drove "uncontained_target". The arm was REACHABLE (a grafted store whose root's children were never copied produces it) and merely unoccupied, so changing its payload type would have compiled green with nothing establishing that the identity survives. Reachable-and-empty is a quiet guard, not a dead one: the answer is to occupy it. scm_env_an_uncontained_target_refuses_to_encode_and_names_it now drives it, and asserts TWO things on purpose. The tag alone would pass whether the arm carried a resolvable ObjectId or a stringified one, so it also checks the CARRIED target against the store's own uncontained population -- which is the property the type change was for. Both halves measured rather than argued: 24 claims, membership vs the grafted store exit=0 membership vs the COMPLETE store (empty set) exit=1 The second is what proves the identity check is not vacuous. I could have reasoned that a fold over an empty list returns false; that is the substitution this stack keeps catching, so it was run instead. A DIRECT DRIVER IS ADDED TO THIS WITNESS, and it is scaffold with a stated end. The floor discovers `test fn` itself and never calls it; it exists because the floor is currently refusing before subject preparation for a reason this branch does not own, and these 24 claims otherwise had NO execution path -- this module's change would have been typechecked and never run. `gunbc run --function` cannot drive a Bool-returning `test fn`. Delete it once the floor executes these identities again; the comment on it says so. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Say only what the evidence establishes: an uncontained target, not the first Two corrections from design review of the item-6 landing. Both are the class this stack keeps producing -- a name or a tool promising more than anything verifies -- so they are fixed rather than argued. (1) THE HELPERS PROMISED AN ORDERING NOTHING CHECKS. first_uncontained_target and first_uncontained_key say FIRST. The witness establishes MEMBERSHIP: the carried target belongs to the store's uncontained population. With a single uncontained object every member is also the first, so the observation cannot distinguish "actually first" from "some legitimate member" -- the name was the stronger claim and it had no discriminator. Renamed to an_uncontained_target / an_uncontained_key. The refusal needs one ACTIONABLE EXAMPLE and no consumer depends on which; that is the real contract, so the name now states it. Deliberately NOT fixed by adding a two-target ordering fixture. Order is not an interface fact here, and pinning it would freeze an incidental traversal order that a later keyed or canonical representation of uncontained_targets should not have to preserve. This is the opposite decision from two_uncontained_children_are_named_in_order, where the reverse IS load-bearing because positions are the encoding -- the difference is whether anything downstream depends on the order, not whether an order exists. (2) THE DRIVER'S OWN COVERAGE WAS UNGUARDED. A hand-sequenced ProcessExit driver that omits a claim turns "driver green" into a subset run that reads as a full pass -- the nothing-ran-versus-nothing-failed trap, inside the tool added to avoid it. The invariant is that every declared `test fn` appears exactly once in its driver. Measured: scm_commit_closure_witness_test declared=13 dispatched=13 scm_load_standing_witness_test declared=6 dispatched=6 scm_repository_envelope_witness_test declared=24 dispatched=24 And the check discriminates -- planting a claim with no driver entry gives declared=7 dispatched=6 -- verified rather than assumed. NO GATE WAS COMMITTED FOR IT, and that is a decision rather than an omission. Durable enforcement machinery for an artifact with a scheduled deletion is scaffold protecting scaffold; the real dissolution is the floor executing these identities, which removes the driver and the invariant together. The rung is recorded on the driver as MITIGATABLE, enforced by hand. Suites after both changes: envelope_witness_main exit=0 (24), commit_closure_witness_main exit=0 (13), load_standing_witness_main exit=0 (6). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the driver's coverage invariant: an identity set, not a count The invariant recorded on the repository witness driver was declared == dispatched. That is the weaker check it sounds like, and recording it as the guarantee made this comment the fourth instance in this stack of prose asserting a wall stronger than the mechanism behind it -- this time inside the artifact added to prevent exactly that failure. WHAT CARDINALITY CANNOT SEE: declared A B C D dispatched A B C C Both populations are four and D never executes. Demonstrated rather than argued, by duplicating one dispatch and dropping another on a sibling witness: count check declared=6 dispatched=6 -> PASS reality an_honest_collision_is_its_own_standing_and_never_supersedes never ran The invariant is now exact SET EQUALITY of declared `test fn` names against dispatched reason strings, plus uniqueness in both populations. Measured across every witness carrying a driver: scm_commit_closure_witness_test 13 identities, sets equal, no dups scm_load_standing_witness_test 6 identities, sets equal, no dups scm_repository_envelope_witness_test 24 identities, sets equal, no dups and falsified by the planted case above, which the previous check passed. NO GATE IS COMMITTED, unchanged from before and for the same reason: durable enforcement machinery for an artifact with a scheduled deletion is scaffold protecting scaffold. The driver's dissolution trigger stands -- the required floor executing these identities removes the driver and the invariant together. What changed is only that the recorded invariant now matches the check that was actually run. Design review also resolved the fork left open in the previous commit, against the premise I offered: targeted mutation runs DO stay valuable after the floor returns, but the answer is to generate an ephemeral driver from the current roster at mutation time, not to keep a hand-maintained one. Two durable rosters -- floor discovery and ProcessExit dispatch -- would be two authorities for which claims belong to a witness, and the drift is predictable (a new test never dispatched, a renamed test leaving a stale entry). That changes nothing in the tree today; it settles what happens to this driver later. envelope_witness_main exit=0 (24 claims) after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * v1 inference: generic instantiation must reach record-literal field expectations (>=2 seams) — plus the adjacent below-floor fail-open where a generic field admits the wrong type silently (#8922) * A generic record literal admits the wrong field type silently at six seams: locate the fail-open, and record two repairs that do NOT close it DESIGN 4b names "values inhabit declared types" as the ordinary compiler floor. A record literal of a GENERIC type does not hold it: measured on eleven single-module probe roots, a wrongly-typed field value is accepted AND EMITTED at six positions -- fn return, let annotation, record field, list element, direct-call argument, and a module-scope data annotation -- while the non-generic control refuses with a located mismatch and the conforming generic control compiles clean. The field PRESENCE axis is unaffected (a generic literal missing a required field still refuses), which rules out "generic declarations are not processed" and confines the class to the field TYPE axis. Mechanism, by execution rather than by reading: the instantiation does reach the literal and the substitution is keyed correctly on "T", but the declaration's field type node carries no name to key on, so the parameter is never substituted and the expectation reaching the judgment is a NAMELESS node -- whereupon kernel_value_declared_type_mismatch returns false on formal_name == "". A second, independent fail-open sits beside it: the substitution value is read with resolved_type, whose Absent arm is the equally nameless error_type. Two repairs were built and run against the full arm table and moved NOTHING; both are recorded because they are the cost of the next attempt. What is still open is where the type-parameter reference loses its name, which is a modelling question in a stage DESIGN names load-bearing -- so no code changes here, and the probe states the exact next question rather than leaving it to be re-derived. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the mechanism: substitution is innocent, the class is any type declared WITH PARAMETERS, and the paired nonzero makes every zero a reading The first revision of this probe named the type-parameter reference losing its name as the cause. Two no-build discriminators falsify that, and a knowingly stale mechanism claim in a finding other lanes plan against is premise contamination -- so the doc is rewritten in one pass rather than annotated. WHAT CHANGED. A generic declaration whose parameter is UNUSED and whose field is a plain kernel type still fails open, so the trigger is that the declaration carries type parameters at all, not that a field mentions one. And forcing the instantiation to bail out with a wrong arity brings the field judgment back on the SAME declaration -- so record_lit_instantiated_fields does not fail to add an expectation, it preempts a working one. Instrumentation then showed authored_fte="" BEFORE substitution: substitution faithfully returns the nameless node it was given, and the declaration reached by the ident-keyed lookup is already identity-stripped where the name-keyed lookup's is not. PAIRED NONZERO. Every fail-open arm now carries a matched non-generic twin at the same seam, same run, same binary: six zeros, six reds. Plus an undeclared-name arm proving the generic module is compiled and its body judged. The twin design also rules out "that seam is unchecked for any type", which a bare perturbation would have left open. FOUR DEAD ENDS, ONE CAUSE, established by reading the construction site rather than by another build: ResolvedModule.module is the raw parsed node, build_type_env folds THOSE items into the bindings, and resolve_item_types runs later feeding resolved_item -- never the binding. ResolvedModule means import-resolved, not type-resolved. Also recorded: resolve_field is correct and has zero callers while its wired sibling resolve_field_init does not, which makes it an incomplete migration rather than dead scaffolding -- and a cleanup sweep deleting it would leave the lossy hand-rolled copy as the only authority. Claim staked on the PR. Still no code change: the remaining question is an ident-versus-intern address-space read, and a fifth blind repair would repeat the pattern the first four established. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The class is two rows, and the corpus reds the closed one: report it rather than narrow the wall (#8901) * The 8 and the 4 have different dispositions: the census rows encode the old answer (#8901) * LexMatchThunk is not generic, so it is none of the three rows: a fourth mechanism, bounded by three baseline arms (#8901) * Withdrawn: the generic carrier is the algebra, not the thunk -- one-variable pair puts the tokenize row in row (b) (#8901) * WIP: (a) fork dissolution — field_declared_type_node, authority + mirror * (a) mirror half restored: field_declared_type_node in v1_compiler_infer.rs * Drop stray backup file * (a) fork dissolution + measured (c) exposure; placeholder-carrier hypothesis refuted by execution * (c) an UNESTABLISHED return type must not become a lambda's body expectation * Install the emitted mirror for v1_compiler_infer.rs (regen candidate, not hand-tuned) * Delete four dissolved frontier rows (observed=0), fix two ContentHash construction defects the wall caught, admit list literals at FreeMonoid * (c) sibling: an UNESTABLISHED substituted param type must not bind a lambda parameter as an error type * Install emitted mirror for v1_compiler_emit_rust.rs (clone elision from the established-type fix) * BISECT ARM (not a landing state): revert (a) field_substitution_carrier, keep (c) Diagnostic push on a draft PR to separate (a) from (c) by execution. The floor caught 9 claims that pass on main and fail on this branch, every one of them against an independently authored oracle, so main's pass was not vacuous and this branch computes wrong values. Local floor OOMs (137) in a session container, so CI is the only instrument at whole-corpus scope. This arm reverts (a) only. It deliberately re-opens the row-(a) defect -- the kb2 RED will stop refusing -- and is NOT proposed for merge. Read the floor line, not the arms. Predicts: if (a) is the culprit, failed goes 9 -> 0 and the 6 samsung_dram stale-quarantine rows stay unmasked. If (c) is, failed stays 9. * Revert "BISECT ARM (not a landing state): revert (a) field_substitution_carrier, keep (c)" This reverts commit 18b5ddc6261acd3c5398a5fc5429fd9ea2e48f63. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Transport binding spine: one target-neutral semantic binding for all four transports, then Filesystem bindings + Rust renderer to restore the 03_ingest board (#8957) * WIP: Bind the file-transport realization handler AND migrate rest/shell/local * WIP: Transport binding spine: one target-neutral semantic binding for all fou * Regenerate the stage0 mirror for the transport binding spine review 54885 and deep-ant-102 both found the same thing: the de-fork existed in the .dag authority and not in the mirror v1 actually runs from, which is specification-without-execution in its textbook form -- the exact failure this cut exists to close. Produced by claim_executor --required-regen; the candidate tree drifted in exactly the four emit files this change re-typed. Also moves an annotation to module-item grain (§4c refused it at body grain) and records the fabricated-empty-base_url marker dependency beside classify_transport: kind is discriminated by marker-field PRESENCE, so making base_url refusable deletes the rest tag and reclassifies every rest transport as local. No binding arm requires a base_url value; that repair owes an explicit kind tag in the same change and is deliberately not taken here. * Drop the dead classify_transport import from the rust emitter Zero call sites since the de-fork: the rust backend consumes a BoundOperation and no longer classifies anything. A live import of the classifier is what a reader grepping 'does the target still classify?' finds first, so it reads as the fork surviving. Found in re-review by smart-ram-730. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Classify rustc mechanisms across diagnostic codes (#8978) * Classify rustc mechanisms across diagnostic codes * Record cross-code classifier provenance * Bind mechanism population to its measured ref --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> * Locate the LexMatchThunk apply receiver-type loss (#8983) * Locate LexMatchThunk apply receiver type loss * Record the bounded pre-descent ordering null * Reclassify the apply root as a representation gap --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Refuse per-code board shares for emitter roots (#8979) * Refuse per-code board shares for emitter roots * Audit shared-types membership authority consumers --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com> * Make impossible fn-field derives unselectable through aliases (#8985) Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Bind mock-totality witnesses to published corpora (#9006) Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * The .dag parser fabricated an empty path and silently ate unknown fields: five refusal arms, one live specimen repaired (#8949) * The parser fabricated an empty path and silently ate unknown fields: five refusal arms, one live specimen repaired `parse_file_fields` substituted an empty string literal when `path:` was omitted, so `transport file { }` and `transport file { path: "" }` produced byte-identical nodes. That is not merely an unchecked state: `is_file_transport` is DEFINED as "carries a base_path", so the fabrication made the absence unobservable to every downstream consumer -- an emit-side "declares no path" refusal is permanently green by construction. The rust realization duly emitted a filesystem write against "" with zero diagnostics. The refusal belongs at parse, where an absent path is decidable from the tokens alone, and that is where it now sits. CENSUS of every parser field that defaults rather than refuses (132 `Absent =>` arms in 02_parse.dag; all but these are legitimate token-absence handling): * parse_file_fields base_path -- omitted path fabricated as "". DEFECT, refused here. * parse_rest_fields base_url -- omitted url fabricated as "". NOT a defect: omitting `url:` is the norm (the base comes from the service config) and an empty base plus a full-URL path template is the authored absolute-form idiom recorded in extdeps.transports.rest. It is a state-space conflation with its own lane, not a refusal decidable from the tokens. * parse_config_fields endpoint -- omitted endpoint fabricated as "". NOT a defect: `config { }` is legal and shell services have no endpoint at all. * four `_` fallthrough arms (config, rest, shell, file) -- an unrecognized field was parsed and THROWN AWAY. Same fail-open reflex one layer over, and it had a live specimen: this repo authored `transport file { op: READ, path: ... }` in extdeps.cloud.gcp and the `op: READ` was swallowed whole, never resolved, never reported. All four refuse; the gcp site is repaired (read is the default verb, so the semantics are unchanged). MEASURED, not assumed. The corpus-wide parse gate against a binary rebuilt from the regenerated mirror indexes 3880 modules from 2 source roots, exit 0 -- so outside the one gcp.dag site nothing in the corpus was relying on a dropped field or an omitted file path. Regen produced exactly one drifted file, v1_compiler_parse.rs, across the 132-file mirror. EVIDENCE, enrolled: dag/test/claim/transport_field_refusal_witness_test.dag carries three positive controls and five discriminating REDs, all 8 PASS under claim_batch. The controls reach compile.emit; the five reds stop at compile.analyses, so the refusal is real and the harness is discriminating rather than false-for-everything. Per DESIGN §4b(4) these stay enrolled as the evidence the rung holds, not deleted with the machinery they replaced. v1 admission: this serves the v2 self-host program -- the file-transport realization lane (#8929) is exactly the consumer whose emitted write the fabrication corrupted. Semantics stay frozen; this is a defect repair, not growth. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Name the stage in the assertion, not just the outcome: the pathless-path RED could not tell parse from emission Folding in a finding from #8937 (sleek-fox-685, relayed by deep-ant-102) that is correct and that this PR's own oracle could not have caught. Every RED here asserted `!compiles(source)` -- ONE BOOLEAN, which is green whether PARSE refused the declaration or the parser fabricated "" and the EMISSION wall caught it downstream. Those are exactly the two states this change separates, so the row watching it could not see the thing it was watching: revert the parse arm, let the emitter catch the pathless case, and every `!compiles` red in this file stays green. Three rows, not the one that was asked for, because a single row could pass for the wrong reason: * w_red_pathless_file_transport_refuses_at_parse_not_emission asserts the parse class POSITIVELY (blocking `ParseError` >= 1) rather than by excluding the emission class. Naming a stage by exclusion still passes if some third, unrelated class is what refused. * w_control_unmodeled_verb_refuses_at_emission_not_parse runs the same two counters the other way, over a source the EMISSION wall refuses. Without it, `parse_blocking_count >= 1` is satisfiable by a counter that is nonzero for everything and `not_modeled == 0` by one that is always zero. * w_control_valid_file_transport_is_clean_at_both_stages reads zero from both on a clean source. Both counters answer -1 on CensusNotRunnable, so could-not-measure fails the `>= 1` AND the `== 0` assertions instead of silently satisfying one (DESIGN §5: top-as-ignorance is not top-as-answer). MEASURED: 11/11 PASS under claim_batch on the merged tree. The open question before running was whether a parse refusal reaches compile_dag_diagnostic_census as an observed blocking ParseError row or as CensusNotRunnable -- if the latter, the -1 arm would have failed the row for a reason unrelated to the wall. It is observed, so the stage assertion is real rather than accidentally green. ALSO: the discriminator fact recorded where the next author will hit it, as a `//` annotation on v1.compiler.core is_rest_transport. Transport KIND is discriminated by marker-property PRESENCE, so `rest_transport_node`'s always-written base_url -- filled from the "" that parse substitutes when `url:` is omitted, which is the NORM -- is load-bearing structure, not a lazy default: removing it reclassifies every rest transport in the corpus as `local`. It is also why is_local_transport is defined negatively. Regen confirms the annotation adds no mirror drift. Merged origin/main. Regen against the merged tree drifts ONE file, v1_compiler_emit_rust.rs, which is main's own red (#8691 landed without its second regen pass) and is #8953's to repair -- not regenerated here, because installing another lane's fix from this tree would give the corpus two producers for one file. v1_compiler_parse.rs is byte-identical to a fresh emit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * An annotation cannot fail: guard the kind-discrimination invariant the 00_core comment only described deep-ant-102 measured what I did not: ZERO witness rows asserted the classification my annotation documents. DESIGN §4c is explicit -- an annotation is never evidence a machine claim holds, because no Accepted program can read one. Prose is the right home for the RATIONALE and cannot be the guard for the INVARIANT, and a comment that reads as coverage to the next reader is worse than none. That reading is not hypothetical: a review of this very PR called the comment "a nice defense against a future 'consistency' edit". It is not a defense. These two rows are. w_red_rest_transport_classifies_as_rest_not_local w_control_shell_transport_emits_no_rest_client Asserted through EMISSION SHAPE rather than by calling is_rest_transport, and that is a reachability fact rather than a preference: CI's source roots are `dag` and `src/v2`, so v1.compiler.core is not in the witness pool and the predicate cannot be named from a witness at all. The consequence is the better subject anyway -- it runs the real pipeline instead of the predicate in isolation. The control supplies the other answer so the first row is not satisfied by an oracle that matches everything, which is the same defect the stage counters had before their inverse row. MUTATION-TESTED RATHER THAN ASSERTED, because "delete the fabricated base_url and this row fails" was a claim about a RED I had not executed. Scratch build with the always-written url_field removed from rest_transport_node -- the exact "tidy the lazy default" edit the annotation warns against: FAIL w_red_rest_transport_classifies_as_rest_not_local PASS w_control_shell_transport_emits_no_rest_client The mutation reds the specific claim and not the harness. Reverted; `git diff` on the mirror is empty, so nothing from the scratch build is in this commit. 13/13 PASS on the restored tree. Kept here rather than routed to #8954's roster witness: this PR introduces the annotation, so it should land with its guard rather than ship prose-only coverage and depend on another lane to close it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * End an unbraced arm body at a QUALIFIED pattern, not only a bare one (#8999) parse_match_arm_stmts consumes statements until looks_like_arm_start reports that the next tokens open a new arm. That predicate recognised a bare `_` and an UPPERCASE-start leaf, and nothing else. A namespace- qualified pattern begins with its lowercase module head, so it answered false: the body kept consuming, swallowed the next arm's pattern as one more statement, and the parse died on the FatArrow that followed. The reported span is that ARROW -- several lines below the arm that actually ended -- which is why this had to be bisected rather than read off the diagnostic. Four separate reproductions of the neighbouring shapes all parsed before the real one was found. MINIMAL REPRODUCTION, every clause load-bearing: Kind { f: _ } => let a = "p" <- unbraced arm body containing a `let` a mod.path.Other => "d" <- next pattern is DOTTED Drop the `let` and the body is a single expression that never enters the statement loop. Make the following pattern `_` or an uppercase leaf and the predicate already answered true. Both are needed. MEASURED. On the namespace-cut branch, where qualifying every pattern turns this from rare into ordinary, exactly one corpus file of 3875 reaches it: src/v1/05_emit.dag. That file is invalid under the parser its own branch carries -- it survives there only because the built binary predates its own committed mirror, so the defect is latent and would surface at that branch's first successful rebuild. This is therefore a grammar gap the cut made REACHABLE, not an accommodation for it, and it fails loudly at preparation rather than silently downstream. DISCRIMINATING RED, BY EXECUTION: the witness returns false against a parser with this one decision reverted to `false`, and true with it. Both runs were performed. ZERO-DRIFT, STRUCTURALLY: the new scan runs only where the old predicate already answered false, and it requires the TERMINAL segment to be uppercase with the arrow following the path or its brace group -- so no previously-accepted parse changes, and a lowercase dotted expression ending a body is unaffected. An expression statement genuinely followed by a FatArrow was never a legal parse. Receipt: required-regen over the 133-module subject reports first_generation_equal=true with only this repair's own mirror changed. 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> * Bind a qualified pattern head from the scrutinee, as the bare spelling already does (#9004) * Bind a qualified pattern head from the scrutinee, as the bare spelling already does Two spellings of one pattern name the same declaration, so they must bind the same node. lookup_variant_in_type forks on whether the head contains a dot: the bare branch answers from the SCRUTINEE, which carries the instantiation; the dotted branch answered from the SYMBOL INDEX, which returns the coproduct's DECLARATION. So the payload bound to the declaration's type PARAMETER instead of the scrutinee's type ARGUMENT, and every field read off it reported "no field 'root' on type 'T'" -- measured, not inferred, on a two-function probe whose only difference is the spelling of the head. Admission is unchanged: the index lookup still runs first and still decides whether the head names a variant of this coproduct at all. Only the bound node's source changes once admission succeeds, and the fallback arm reproduces the previous answer exactly. RECEIPTS. Discriminating RED proven in both directions on the same corpus: on the pre-fix binary the qualified arm returns false with the diagnostic above and the bare control returns true; after regen and rebuild both return true. One generated file drifted -- v1_compiler_infer_patterns.rs, this repair -- and the second pass reports first_generation_equal=true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-confound the witness pair: the arms differed in imports, not only in head spelling The floor reported the qualified arm at 58800ms CPU against a 5000ms budget with 1.21GB RSS growth while the bare arm passed under budget, and I read that as a cost of the qualified pattern head. It is not yet evidence of that. The qualified probe imported two names and the bare probe imported four, so the arms could differ in source-closure construction, import binding, symbol-index use and cache temperature as well as in the spelling under test. The pair was a controlled experiment for the SEMANTIC discriminator and not for the cost one -- a control must name its adversary, and cost was an adversary these arms never excluded. Both probes now import all four names, leaving the two pattern heads as the only difference. The semantic RED is unchanged and was re-proven in both directions after the edit, against binaries built from the pre-fix and post-fix mirrors: pre-fix qualified=false bare=true post-fix qualified=true bare=true No generated file changes; the seed is untouched by this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the witness to the census grain: it was measuring emission for a claim about resolution The subject is a BINDING fact and a binding fact is decided at typecheck. The witness asked it through compile_dag_rust_emit_check, which parses, resolves, typechecks, EMITS RUST, and then -- per the compiler's own compile_dag_diagnostic_census_row_note -- collapses the whole result to a Bool, discarding which judgment fired. The enrolled claim duly cost 58579ms CPU against a 5000ms budget with 1.21GB RSS growth while its bare control passed under budget. compile_dag_diagnostic_census reports the causal judgment directly as typed rows. That makes this witness narrower in subject, MORE discriminating -- it names the diagnostic instead of collapsing to false -- and cheaper for a principled reason rather than a convenient one: emission is downstream of the fact being tested, so removing it removes work, not evidence. CensusNotRunnable is a failure carrying its own cause and is never the expected red. Could-not-measure and measured-nothing are different states and only one of them is evidence. MEASURED, one fixture, both probe sources carrying identical imports so the only difference is the two pattern heads: pre-fix qualified OBSERVED[1] InternalError | no field 'root' on type 'T' | blocking=true | n=1 (enrolled fn returns false) pre-fix bare OBSERVED[0] post-fix qualified OBSERVED[0] (enrolled fn returns true) post-fix bare OBSERVED[0] (enrolled fn returns true) THE COST OBSERVATION IS NOT REPAIRED BY THIS CHANGE AND IS NOT CLAIMED TO BE. It is carried forward in the pull request body with its two ruled-out causes, its unattributed owners, and its next discriminator. 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> * Three prose rows still said srv4 commits six, and the disk arithmetic behind them refuses at twenty-one (#9001) The CPU-axis change (#8976) moved srv4 from 6 to 21 and left three prose rows asserting the old width. Prose cannot refuse, so nothing surfaced them -- they were found by review (fierce-hawk-734) rather than by any gate. gunbc_runner_slot_allocation_srv4_admission_note said "srv4 commits 6 slots at the memory axis" and that runner_count and the roster "both name 6 as the materialization target". Replaced, not annotated: two accounts of one width is what this module exists to prevent. srv4 memory-admits 29 and commits 21, the CPU axis binding, and neither number is authored -- runner_count derives from gunbc_runner_slots_per_host, so the note is a reading of one authoring. width_is_a_minimum_over_axes_note carried the same six in passing. Corrected. gunbc_runner_slot_width_ruling_note is deliberately NOT edited. It is labelled SUPERSEDED AND RETAINED AS METHOD with "PRIOR TEXT FOLLOWS UNEDITED", and its own header warns that reading on for current widths will mislead. Editing preserved historical text to agree with the present would destroy the only thing it is for. THE DISK ARITHMETIC IS THE PART THAT IS NOT COSMETIC. srv4_runner_count_disk_cap_note sized the per-slot charge at width 6 and read as reassurance. At width 21 the same charge is 21 x 40.96 GB, about 860 GB, against a Samsung 970 EVO 500GB -- so runner_width_disk_preflight is EXPECTED TO REFUSE srv4 at its committed width. The allocation axis cannot see this: disk is DiskWidthUnconstrained at allocation by the 2026-08-06 ruling. So the model commits a width the actuator is expected to stop, which is the fail-closed arm working and also means srv4 has a committed width it cannot currently reach. Recorded rather than resolved by lowering the commitment, because absorbing to a width the disk happens to permit is the fallback that ruling removed. AND THE CHARGE IS CIRCULAR, which is recorded at the authority rather than only in the rows citing it. runner_slot_disk_budget_per_slot_note claimed provenance: "derived from srv4_runner_count_disk_cap_note arithmetic (~38GB per slot at width 7 on 500GB class disk)". That is not a provenance -- disk size divided by the width of the day IS the derivation, so the charge was computed FROM a desired width and is now used to CONSTRAIN one. Nothing was measured. A live observation under an active reclaimer came in near 2.5 GB, two orders of magnitude below it. So a circular charge is refusing a derived width: two unmeasured numbers meeting, and neither the refusal nor a pass would be evidence about srv4's real disk. The refusal stays, because refusing on an unreliable charge is fail-closed and lowering the charge to make the width fit would be fitting the measurement to the answer. What is NOT claimed is that srv4 cannot hold 21 slots -- every ephemeral runner keeps a _work tree plus caches, so the true figure is not 2.5 GB either and the question is open in both directions. Each row carries the same dissolve-on: a measured per-slot disk series on srv4. Co-authored-by: Brian Searls <briansearls1@gmail.com> * Make the hand-built argv unwritable at the call site, and land the positive examples that show what to write instead (#8919) * Make the hand-built argv unwritable: seal ArgvCommand, and land the builders that show what to write instead extdeps.exec.command ArgvCommand becomes sole_constructor with one admitted mint (argv_command), caller-sealed by name to typed builders homed in each tool's own extdeps module beside its cited upstream authority. All 58 record constructions on main are converted in this change, because a partial seal is a dual-authority interval rather than a weaker seal (DESIGN section 3). The carrier splits program from arguments, which makes the empty argv unrepresentable and dissolves two runtime refusal arms in gunbc.command_runner (DESIGN section 4b: structurally impossible over mechanically preventable). The seal surfaced nine hand-spelled argvs that were never record literals and four List<String> laundering seams; all are converted or closed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Program spelling is an observation claim: one authority paragraph, one line per row still-seal-394's correction: the rule is not 'PATH-resolved is the safe default'. An absolute path is a claim that this repository observed the target's filesystem, and it is the STRONGER form wherever that claim is true -- a sudoers rule can name it and a preflight can test for it. PATH resolution is correct only where the host is unobserved. The reasoning, the climb criterion and the roadmap_dashboard_instance_apply counter-example live once at extdeps.exec.command program_spelling_is_an_observation_claim; the ten rows it governs carry one line pointing at it instead of ten copies of the paragraph. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Five more hand-spelled argvs the seal surfaced: /proc reads and the fd walk The refusal census does not stop at the record literal. build_cache_endpoint_observe still spelled four argvs as bare word lists (two cat, one stat -c %U, one readlink) and host_effect_realize spelled the /proc fd walk as a fifth; all five now derive from cited authorities, with find's -lname glob fact homed in a new extdeps.tools.findutils beside the flags rather than in the caller that met it. stat's name row gains the -- end-of-options guard its sibling rows already carried: one module was answering one question two ways, and these operands come from observed host state, which is exactly where a leading-dash path appears. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Cast the two NonEmptyStr literals at their call sites Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Admit two builders the wall caught, and measure the NonEmptyStr refinement the climb rests on The seal refused readlink_command and the findutils fd-walk builder -- two admit-list omissions of mine, caught by execution rather than by review. The empty-argv climb claims program: NonEmptyStr makes an empty program unwritable. NonEmptyStr is a refinement, not a mint, so that claim is only as good as its enforcement at construction. Measured with a discriminating pair on a freshly built gunbc: data p: NonEmptyStr = "" is REFUSED at the declaration, data p: NonEmptyStr = "mkdir" is accepted and evaluates. Recorded beside the deleted test, with the path boundary and the reason it is not enrolled. Two NonEmptyStr literals become data rows, because a cast of a String literal at a call site is refused by the same judgment. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Count the sh -c residual instead of estimating it: eleven, not six Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * The nbd programs do not both run on the BMC: correct the note that said so Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * State the two privileged word changes at the builder that makes them Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Name the two concrete products the hub still carries, and why the rule admits them Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * The transport-argv population is blocked by a floor defect, not this lane's residue Preliminary ruling relayed from the shell -> dag lane: an identifier in a transport argv position is never name-resolved, so no citation-based conversion of those sites is possible by any author until gunbc#8916 closes. Naming it as residue would read as a conversion that stopped short and would put the obligation on the wrong lane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * State the empty-program climb as four facts, not one claim Operator ruling relayed: a completed climb retains executing evidence, and this one has a recorded receipt with no enrolled route. The arms stay deleted -- the empty argv is unrepresentable regardless of enrolment -- but the claim is evidenced-but-not-floor-enrolled on the source path and unmeasured on the emission path, stated as separate facts so they cannot collapse into 'done'. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * The bracket-form regression control follows its builder's rename socket_inode_holder_argv became socket_inode_holder_command when the /proc fd walk stopped being a hand-spelled argv, and this witness -- the control that pins the ? wildcards against the bracketed glob that silently matches nothing -- still called the old name. CI caught it; I had not. It asserts exactly what it asserted before: the emitted pattern is socket:?3894042? and contains no brackets. Only the route to the words changed, from a List<String> return to argv_words over the ArgvCommand. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * One name, two operations: qualify the ten live-deploy references the merge made ambiguous THE MERGE PRODUCED A COLLISION NEITHER SIDE COULD SEE ALONE. main's #8845 added `gunbc.live_deploy.operations.rm_force_command(paths: List<String>) -> String` -- privileged shell TEXT for removing several paths. This branch added `extdeps.tools.gnu_coreutils.rm_force_command(path: String) -> ArgvCommand` -- the cited tool operation for one path. Different layers, different carriers, different arity, same spelling. Each was unambiguous in its own tree. THE COMPILER REFUSED RATHER THAN PICKING, which is the outcome worth recording: dag/gunbc/live_deploy/emit.dag:818:29: error: ambiguous reference 'rm_force_command': 2 candidates: extdeps.tools.gnu_coreutils.rm_force_command, gunbc.live_deploy.operations.rm_force_command — qualify by containment path, alias, or rename Ten references, six in `live_deploy/emit.dag` and four in its test. All ten want the shell-text one -- they pass `paths:` and feed `deploy_raw` -- so they are now spelled `gunbc.live_deploy.operations.rm_force_command`. Qualification is the diagnostic's own first suggestion and the least invasive of the three: it edits references, not authorities, and renames nobody's landed symbol. NEITHER NAME IS WRONG, which is why this is not a §3 nicknaming repair. §3 forbids two names for one concept; this is one name for two concepts, and both are honest in their own module -- `extdeps/` keeps the tool's real operation name, and the product layer names the privileged-text form it owns. If either should move it is a question for the live-deploy lane, not something to settle inside a merge. ONE LATENT INSTANCE LEFT DELIBERATELY, named rather than silently passed over: `dag/gunbc/build_cache_endpoint_path.dag:130` calls the unqualified `rm_force_command(path:)` and did NOT error, because `gunbc.live_deploy.operations` is not in that module's import closure. It is correct today and one import edge away from the same refusal -- the same closure-scoped resolution class this session filed as gap-analysis row 30 (gunbc#8943) and repaired four sites of in gunbc#8944. Left unqualified because this PR is otherwise complete and a speculative edit buys a 40-minute CI cycle; recorded here so the next reader finds it by search rather than by breakage. Regen passed on this head (first_generation_equal=true), so the inherited #8691 red is gone and this floor refusal was the only remaining failure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Merge main (§4c annotation fix, #8989) and align the one over-indented admit row THE MERGE closes the last inherited red. #8989 hoisted the §4c-illegal annotation out of `witness_retired_runner_slot_owner_refuses`'s match body; while it stood, floor preparation died before planning a single witness, so every "failing" floor verdict recorded anywhere in the repository during that window was uninformative rather than negative. This branch's own runs in that window say nothing about this branch. THE NIT, from review 54984 and held deliberately until now: one `decl_ref` row in `argv_command`'s `admit_callers` list sat at 8 spaces where its 39 siblings sat at 4. Now 40 of 40 at 4. It is cosmetic, which is exactly why it waited — pushing it alone would have cancelled an in-flight run, dropped five approvals (scored per head), and spent a ~45-minute CI cycle in a fleet completing about one run in six, all to correct four spaces. Riding the merge costs nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 * Two witnesses caught the spelling migration going both ways, and only one of them was the witness's fault THE FLOOR RAN FOR THE FIRST TIME ON THIS BRANCH and reported failed=10 against main's failed=8 on the same head (13db52a25, run 32621117917). The two extra are mine. They are opposite defects and the difference is the whole entry. BUSYBOX -- MY CODE WAS WRONG, THE WITNESS WAS RIGHT. `busybox_build_is_modeled_and_grounded` asserts `'mkdir' '-p'` and got `/usr/bin/mkdir`, because this migration routed the call through `mkdir_parents_command`, whose wrapper cites the recorded absolute path. `gunbc.busybox_bmc_build` runs its whole sequence under `LocalExec` on whichever machine the operator invoked the cross-build from -- it demands an `arm-linux-gnueabi-` toolchain, not a host this repository has ever read. So the absolute path was a claim about an unobserved filesystem: the exact §5 fabrication `extdeps.tools.mkdir`'s own rows warn against, committed by me while quoting the rule. Now routed through `mkdir_parents_command_at` with `mkdir_path_resolved_program`, with the reason stated at the call site as that module asks its PATH-resolved callers to do. The mkdir note is corrected in the same commit rather than left standing: it said the BMC applet was the one such caller and "every other caller gets the recorded absolute path". That became false the moment this second caller landed, and a note asserting a population it no longer has is the stale-recital class DESIGN §3 exists to stop. SUDO -- MY CODE WAS RIGHT, THE WITNESS PINNED THE OLD SPELLING. `srv4_runner_installer_command_cites_installer_with_env` asserts `'sudo' '-E' 'bash' ...` and now renders `/usr/bin/sudo`. That change is deliberate: sudoers matches on the absolute path, so a PATH-resolved spelling would let the caller's own PATH decide which binary crosses the privilege boundary, and `sudo_elevate` two functions above already used this row -- the alternative was two spellings of one binary in one module. The assertion is updated to the new words. THE ASYMMETRY IS THE POINT. Same migration, same kind of diff, two witnesses red, and the correct repair ran in opposite directions -- one edits the code, one edits the oracle. Deciding by which side is easier to change would have got one of them backwards; deciding by whether the host was OBSERVED gets both right. Also lands the annotation I owed at `sudo_binary_path` (review 55022): the -E row documented its own `-n` delta while the path delta was left implicit. Both are now stated at their rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DhAfyPkuxnjZaTzPn5PyE1 --------- 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> * A cost-shape defect that measured linear: file the per-step emit constant, and the refuted hypothesis (#8988) * A cost-shape defect that measured linear: file the per-step emit constant, and the refuted hypothesis I proposed fixing a quadratic accumulator in the orchestration emit path, measured it, and it does not exist. The refuted hypothesis is the more useful half of this row, so it is filed with the measurement rather than dropped. WHAT WAS HYPOTHESISED, and every sentence of it is true. v2.compiler.emit_orchestration orch_emit_steps_from folds left-linearly, carrying the accumulated script as a String and calling orch_emit_join2(left: everything_so_far, right: next_step) once per step. That join is not a concat: it reaches orch_emit_from_registry, builds a TargetModel whose binding spellings carry both operands verbatim, and runs the whole grammar emit pass over it. Read that way it is n-1 emit passes over payloads growing to the full script length -- the copied accumulator DESIGN section 6 names. WHAT IT MEASURES. A scaling probe -- identical trivial steps, only the count varying, release claim_batch, thread CPU with wall within 1-5ms on every row: n 8 16 32 64 128 | 128 256 512 1024 cpu 48 61 94 161 308 | 239 448 894 1863 ratio 1.27 1.54 1.71 1.91 | 1.87 2.00 2.08 Linear across two decades, no knee. A quadratic converges to 4.0 per doubling; this converges to 2.0, and the early sub-2.0 ratios are the fixed intercept washing out. Fit: about 14ms + 1.8-2.3ms per step, the slope moving between processes on one box with ambient contention -- the same 2x spread gunbc.witness_row_cost already records. SO THE CONSUMER'S COST IS ARITHMETIC. test.claim.live_deploy.emit twin_and_production_configure_disjoint_tailscale_endpoints budget-refused a required floor run at "at least 5008ms" against v2.workflow.required_floor required_floor_claim_cpu_safety_limit_ms. Run alone it PASSES at cpu=5489ms wall=5504ms -- 5008 was the interrupt point, not the cost, so the row is ~10% over the fail-stop rather than ~0.2%. At ~2ms/step its four scripts are roughly 2750 rendered lines. WHY THIS IS NOT A SECTION 6 ALWAYS-FIX. That rule fires on a PROVEN cost shape; a plausible one is a hypothesis. There is no wrong complexity class here, only a large constant, and reducing it means memoizing the emit path on declared-input content -- the Realization/content-hash carrier section 2 holds up as canonical and section 6 records v2 as still hand-rolling. Compiler-wide work on load-bearing files, filed rather than improvised. THE CLASS. A mechanism reading is not a cost measurement. The hypothesis named the right function, the right call and the right reason it is expensive, and was still the wrong complexity class, because whether a real mechanism DOMINATES depends on constants the source does not show. The tell is that the fix would have looked principled: orch_construct_seq2 is left "\n" right over two raw operand tokens, wrapping and escaping nothing, so it is associative and a rebalanced join tree renders byte-identical output. The rewrite was available, correct, byte-safe and pointless -- and merged, nothing afterwards would have distinguished it from a real fix. WHAT WAS DELIBERATELY NOT DONE. The witness was not split: it would zero this row's failure frequency while leaving sixteen siblings at ~8x the 500ms wall migration threshold, which is the absorbing fallback executed at authoring time, and the disclosure gate exists to keep that population visible. The fail-stop was not touched. No declared-ceiling lane was built -- the diagnostic advises one and no such mechanism was found in tree, which is recorded as an observation about the diagnostic. The row stays on the disclosure roster and will intermittently budget-refuse on main until the memoization lands. Named as a real intermittent red, not an acceptable one. Every symbol and module cited here was grep-verified against the tree; no positional citations (DESIGN section 3). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * "Two scripts each" was an unverified quantifier, and correcting it moved the finding The approving review found nothing; re-reading my own row did. Two defects, and the second one changes what this row says is worth fixing. THE QUANTIFIER. I wrote that the sixteen live_deploy.emit siblings emit "two scripts each". Counted per witness, twelve emit ONE, three emit two, one emits three, and the refused row emits four. I had counted the family and not the scripts, and asserted the second as though I had. WHAT CORRECTING IT EXPOSED. With the real counts the seventeen observed costs regress cleanly on script count: ~2235ms fixed per witness + ~773ms per emitted script scripts rows observed predicted 1 12 2830-3178ms 3008ms 2 3 3841-3979ms 3781ms 3 1 4109ms 4555ms 4 1 5504ms 5328ms The ~773ms marginal matches the probe's ~2ms/step over roughly 400 lines per script, so the emit constant explains the SLOPE. It does not explain the INTERCEPT -- and the intercept is the larger term for twelve of the sixteen. About 2.2 seconds is spent before the first script is emitted, outside orch_emit_pipeline entirely, and this probe did not measure what it is. WHY THAT MATTERS RATHER THAN BEING A REFINEMENT. The previous revision took 5504ms, divided by ~2ms/step, and reported "roughly 2750 rendered lines, about 690 per script". The slope only accounts for about 800. I had folded an unmeasured fixed cost into a measured per-step figure and published the quotient as though the whole row were emit -- the same class of error as the hypothesis this document exists to record, arrived at one layer further in. So the row now names the fixed term as unmeasured and unowned instead of absorbing it, and says plainly that it, not the emit constant, is the bigger target for most of the family. The split-the-witness paragraph now cites the regression's ~3781ms for a two-script witness instead of "about two scripts and under the fail-stop". The refusal to split is unchanged and unaffected. 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> * Supplier bindings, per-supplier billing quantum, and an acquisition simulation (#8960) * wip: ubicloud supplier binding (verifying) * Billing quantum is a per-supplier fact, and continuous capacity is the modeled advantage of owning * The acquisition question: does demand shape make a commitment worth holding * fix: named fold args, no block lambda, no next-line field values * refactor: qualify Offer/SelectionPolicy as SupplierOffer/SupplySelectionPolicy 'Provider', 'Offer' and 'Selection' each name two unrelated things in this corpus: gunbc.dispatch_selection's ProviderOffer is an agent-runtime credential binding carrying no price, and product.fabric.supply's Offer is a priced compute-supply ask. They do not unify -- there is no proven coincidence to bundle, only a shared English word -- so the generic name goes to neither. dispatch_selection already qualifies its side; this qualifies ours. * fix: bill the quantum against each job's duration, not the slot's concurrency Executing the witnesses caught a units error in the simulation's billing core. quantum_billed_slots(used_slots: taken, ...) passed a JOB COUNT into a parameter meaning a DURATION, so a 60-slot minimum increment rounded a slot's concurrency up to sixty instead of billing each of its jobs for sixty. Both magnitudes are Nat, so it typechecked; only running it disagreed. Replaced by billed_slots_per_job, which states the model's standing assumption -- one slot is one job's runtime, and jobs of differing duration are not modeled until arrivals carry a duration -- rather than leaving it implicit. The shape witnesses were reworked in the same pass because their fixture moved two axes at once: a 60-slot increment against one-slot jobs is so dominant that owning wins under every arrival shape, which is a real effect but not the one those tests claim to measure. Renting now bills per slot there, so demand shape is the only thing varying, and the increment gets its own witness. The flip is now demonstrated at EQUAL MEAN -- flat ten every slot versus six hundred once in sixty, the same 6000 job-slots -- where it previously compared unequal means and asserted the …

gunbc-ci-auto-heal added 2 commits August 23, 2026 00:29

wip: ubicloud supplier binding (verifying)

1f71cbd

Billing quantum is a per-supplier fact, and continuous capacity is th…

7772554

…e modeled advantage of owning

gunbai-bot Bot mentioned this pull request Aug 23, 2026

DO NOT MERGE — restored a stale fork of authorities that already exist on main #8950

Closed

gunbc-ci-auto-heal added 5 commits August 23, 2026 02:00

The acquisition question: does demand shape make a commitment worth h…

857af58

…olding

fix: named fold args, no block lambda, no next-line field values

fe67bd6

gunbai-bot Bot changed the title ~~gunbc private colo~~ Supplier bindings, per-supplier billing quantum, and an acquisition simulation Aug 23, 2026

gunbai-bot Bot marked this pull request as ready for review August 23, 2026 03:16

This was referenced Aug 23, 2026

main's floor is red: hoist an in-body source annotation to module grain #8993

Closed

Hoist a §4c-illegal annotation out of a match body: it refused the whole floor at preparation #8989

Merged

gunbc-ci-auto-heal added 3 commits August 23, 2026 05:56

Merge remote-tracking branch 'origin/main' into broker/supply-model

15cb301

briansrls merged commit 1722f5c into main Aug 23, 2026
1 of 2 checks passed

briansrls deleted the broker/supply-model branch August 23, 2026 14:43

gunbai-bot Bot mentioned this pull request Aug 23, 2026

Consolidate eight approved fabric/fleet PRs into one, and repair the two breaks the merge made silently #9023

Merged

gunbai-bot Bot mentioned this pull request Aug 27, 2026

Turn the supply fold into a cross-mode selector: the six inputs supply.dag named as missing, and a duration that can be unknown #9397

Merged

Navigation Menu

Repository navigation

Supplier bindings, per-supplier billing quantum, and an acquisition simulation - #8960

Supplier bindings, per-supplier billing quantum, and an acquisition simulation#8960
briansrls merged 13 commits into
mainfrom
broker/supply-model

gunbai-bot Bot commented Aug 23, 2026 •

edited

Loading

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Aug 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What this is

The defects this found, all caught by execution rather than by review

The first production supplier binding

Route on marginal, acquire on allocated

Witnesses, all green by execution

What is NOT modeled, stated so the names do not overclaim

Known red

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Fixed: money is now a carrier

Partly disagreed: two of the three cited expressions

One new function, and why it is not in std

The non-blocking note was right

Verification status

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

The failure

Why my local runs could not have caught it

Fix

Verified against the check that failed, not the one that passed

One prediction of mine was wrong

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

Attribution of the remaining red, measured rather than asserted

The one that was mine, and why its red was correct

Why the other eight are not mine, established before the result landed

Also worth flagging, not mine and not counted in failed

Uh oh!

gunbai-bot Bot commented Aug 23, 2026

There is nothing on this branch left to fix, and that is a measurement rather than a claim

The failure sets are identical

What the remaining eight are

State

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

gunbai-bot Bot commented Aug 23, 2026 •

edited

Loading

Also worth flagging, not mine and not counted in `failed`