Repository navigation
Conversation
…supply gets its first caller select_supply has been complete and unconsumed since it landed. This module is the join: the required floor's own Work becomes a Demand, and the candidate roster is ranked by the authority that already knew how, rather than by a second ranking written beside it. What this does NOT do is stated in the module header rather than left to be inferred: selecting an offer is a DECISION, not an execution. No Grant is committed, no process starts, no host effect is reached. The invariant fabric_witness_run builds toward -- no committed Grant, no process -- is not established here. Four rows, green by execution in one run: a host larger than the floor is selected for it (positive control), a host smaller than the floor is CONSIDERED and REFUSED rather than silently dropped (the discriminating red), an empty roster selects nothing and considers nothing, and the floor demand carries the authority's own satisfaction requirement rather than a copy. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… against a slot that was never there std.durable_compare_and_set has had no production realization since it landed. This is the first, and it is the shape that module's own header asks for: the store owns the read and the conditional write in one operation, so no caller ever supplies a free-standing observation and the declared key-relation boundary is closed by construction rather than observed and refused. The mechanism is generation-suffixed slots. A slot at generation N is the file <root>/<key>.<N>, written once and never rewritten, so both expectations reduce to one primitive -- create-if-absent is create-new key.1, update-from-N is create-new key.N+1 -- and create-new is O_EXCL. Exclusion is therefore performed by the operating system on the write itself rather than by a lock the caller holds, which is the gap the interface names: the existing exclusion is flock, single-host by construction, and cannot serialize two writers on different hosts. Verified on both the interpreter and the emitter paths rather than taken from the prose note, because a rung is per-path. THE DEFECT THIS COMMIT ALSO REPAIRS WAS MINE, FOUND BEFORE IT LANDED. The first cut derived the target generation from the EXPECTATION and let O_EXCL decide. That is sound for ExpectSlotAbsent and wrong for ExpectSlotGeneration, because O_EXCL excludes competing writers for the TARGET PATH and establishes nothing about which generation is currently the head. An attempt expecting generation 7 against an EMPTY store computed target 8, found key.8 free, won the create, and reported a commit on a precondition that was never true. The target is now derived from the OBSERVATION. An expectation is a claim about the store, and deriving the write target from the claim rather than from the store is the whole of the bug. The invariant is that the read establishes eligibility and the exclusive write decides the winner -- reading first does not reopen a time-of-check-to-time-of-use race, because two writers that both observe head N both derive N+1 and exactly one create succeeds. THE EVIDENCE IS THE FILESYSTEM, NOT A BOOLEAN. The live probe drives five attempts and the store is left holding exactly slot-a.1 and slot-a.2. There is no slot-a.8 and no slot-b.8, and under the old derivation both would exist -- an expectation of generation 7 is refused against a slot at generation 2 and against a slot that does not exist at all, with no write attempted in either case. That probe is an entry point rather than a shell script because an ad-hoc .sh here is unmodeled realization: if a measurement is worth re-deriving it is worth an entry point. TWO FURTHER DEFECTS FOUND BY BUILDING RATHER THAN BY READING. CasOutcome has three arms and none can say the attempt's digest does not match its payload; reporting that as a store refusal blames the store for the caller lying, so the input is narrowed instead of the shared type widened -- a sole_constructor verified-attempt whose only mint verifies the digest, which the interface says is exactly the realizing store's duty and which is available here because this realization is concrete at the type the hash function accepts. And the key is interpolated into a path, so a key carrying a separator escaped the store root; refused at the mint, and refusing the separator alone is sufficient because the generation suffix is always appended so a bare dot-dot can never be a final component. A WITNESS WAS DELETED RATHER THAN REPAIRED. the_target_generation_is_derived_- from_the_expectation_and_never_supplied was green, and it was green because it pinned the defective invariant. Keeping it beside the fix would leave the corpus asserting both the defect and its repair. Its replacement cannot be hermetic: the corrected derivation reads the store, so every discriminating row for it performs a host effect and belongs to the live probe. Scope declared rather than overclaimed. sole_constructor confines construction on the source-to-.dag path; DESIGN records by execution that an emitted mirror is forgeable, so the mint is sufficient for the path this carrier travels and nothing more is claimed. O_EXCL serializes writers only against the SAME store instance -- two local roots on two hosts are two stores. And the probe treats an unreadable generation as the end of the chain because the transport cannot distinguish absent from unreadable; that conflation is declared with a rung and a trigger rather than resolved by parsing an error string. Not opened for merge: no production consumer exists yet. The broker cut is what consumes it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…and the offer names the cell The first production consumer of three authorities that were each complete and unconsumed: product.fabric.selection ranked nothing for anyone, the floor's demand-side dispatch had only witness rows behind it, and the file-backed compare-and-set had no caller at all. The value is not new vocabulary -- this invents none -- it is that those three stop being furniture. THE INVARIANT, and the reason the two steps are in this order: SELECTION IS A DECISION, NOT A CLAIM. Two brokers ranking one roster reach the SAME answer, so selection alone hands one cell to both. The compare-and-set is what makes the reservation exclusive, and the store rather than a lock decides, so it holds across hosts. No committed compare-and-set, no reservation. THE ARROW, which is the part that changed after review. The first cut took the slot as a parameter BESIDE the selection, so a caller could reserve srv3-06 against a decision that chose a different supplier: two true facts with the relation between them asserted by neither, and every arm still reading as plausible. Five hermetic rows and two live receipts were green over it, because each tests a projection and none tests the join. The repair is construction. FabricCellCandidate is sole_constructor and its mint refuses unless the offer's executor is exactly the slot's canonical instance name, so the broker now takes a roster and no slot at all, and recovers the key from the WINNING offer. That is the same renderer's output carried through selection rather than a second identity authority -- the property the store's key must have. A reservation for a cell the market did not choose has no spelling. THE RUNG IS PATH-SCOPED AND THE MODULE SAYS SO. Structurally impossible on the source-to-.dag acceptance path: the validator is fixed and module-owned with zero caller freedom, so it cannot be defeated the way a caller-supplied predicate can. UNESTABLISHED across emission -- DESIGN carries an executed receipt that a fixed-law mint of this shape emits as a pub struct with a pub field deriving Deserialize. A class's rung is the minimum across its paths, so both are stated and the next-rung trigger is named. EVIDENCE, by execution and by the filesystem rather than by return values. Seven hermetic rows green, including the arrow's positive control and its discriminating red (an offer executed by anyone else refuses at the mint), and a fail-open guard asserting all four non-commit arms report the cell unheld. Three live rows: the broker reserves the cell whose offer won, leaving exactly srv3-06.1; a second writer expecting the same absent slot LOSES, leaving exactly srv3-06.1 and srv3-06.2 with no third file and nothing overwritten; and an empty roster reserves nothing, leaving the store EMPTY -- the only observation that catches a broker fabricating a decision the market refused to make. The probe's own refusal codes split NoCellAdmissible into nothing-offered and everything-rejected, because one code for both hid a fixture declaring 1 thread against the floor's required 8, which read exactly like a correct refusal. WHAT THIS DOES NOT DO. It issues no ExecutionGrant, starts no process and reaches no host. A reservation is the precondition for a Grant and is not one: ExecutionGrant carries reservations that must commit atomically across ledgers, and manufacturing one from a slot generation would fabricate the very atomicity that record exists to guarantee. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…es customer capacity at admission gunbc.fabric_capacity_class_gap has recorded, unconsumed, that nothing structurally prevents CONTROL-PLANE capacity -- the cells running our own scheduler, reconciliation, admission and receipt work -- from being offered as customer-executable supply. That class sat BELOW mitigatable: not a failure being contained, an invalid state simply representable and unremarked. This is its named next-rung trigger, and the gap carrier's own words for what it was waiting on. WHERE THE CLASS DOES NOT GO, AND WHY THE CARRIER'S TRIGGER TEXT IS WRONG. That trigger reads "a capacity class on product.fabric.work Shape". Taken literally it names the Shape RECORD -- and Shape is one type carried by BOTH ExecutionRequirements and SupplierOffer, so a required field there is stated by the SUPPLIER. That is ClassOnSupplierOffer, the arm the same carrier refuses two declarations earlier, arriving through the type system with its refutation intact: it asks the party with the least knowledge and the most incentive to say yes to make the safety assertion. Nobody would choose it; the shared type hands it over. The ruled rationale governs over the ruled name -- "we originate the demand, so we hold the fact" is true of the work side and false of a type the supply side also carries. A SECOND, INDEPENDENT REASON Shape WAS THE WRONG CARRIER, and it is why this was worth stopping for rather than arguing about: shape_material HAND-ENUMERATES its inputs. A class added there would have been SILENTLY ABSENT from the material identity, so two shapes differing only in class would share one identity -- and the guard against exactly that, unstated_and_stated_do_not_collapse_in_the_material, varies the ENVELOPE and would have stayed green over it. THAT TRAP FOLLOWED THE FIELD TO ITS NEW HOME. work_identity_material hand-enumerates too, and reads all four requirements fields by hand today. Its own annotation records isolation having been omitted and repaired "ONE FIELD LATER". This is the third field. capacity_class is added to that material, and the row proving it -- two demands alike but for their class must not share an identity -- is authored to vary THE CLASS, because the existing collapse guard varies the envelope and cannot fail on this. Verified by execution in both directions: removing the field from the material turns that row FALSE while the identical-demands control stays TRUE. The hand-enumeration itself is NOT repaired here. Deriving materials from the record is the right fix and changes every material identity in the fabric -- a content-hash event, not a field addition -- and bundling it inside a safety cut would have a reviewer approve one change while receiving two. WHAT AN EXECUTOR IS SANCTIONED FOR IS OUR FACT. ExecutionRequirements says what work REQUIRES; gunbc.fabric_executor_class says what an executor may serve, and it is a fleet-side roster we author about machines we own or rent. The supplier is never asked. That follows the precedent already in product.supplier.ubicloud, which refuses to name an isolation profile from a published price list -- and a class invented from a catalog would be worse than an invented profile, because a broker reading it would ROUTE ACROSS A SAFETY BOUNDARY rather than mis-rank. Our own cells are control-plane BY CONSTRUCTION rather than by a roster row someone must remember to add: a RunnerSlotIdentity cannot name anything but a cell in our build fleet, so fleet_cell_sanction derives the sanction from the identity. An UNCLASSIFIED executor REFUSES rather than defaulting -- "we have not classified this" and "this serves customers" are different states with different remedies, and a default would let the roster grow a sanction nobody authored. ADMISSION RUNS BEFORE FUNGIBILITY, and the order is the safety property. Once two offers are fungible they are interchangeable by definition, so a class boundary checked after ranking is a boundary already crossed. The broker filters the roster first, so an unsanctioned cell is never a candidate and cannot be reached by a tie-break, a price, or a later change to the ranking. EVIDENCE: eight hermetic rows green, both walls asserted in both directions (control-plane work refused on customer capacity AND customer work refused on our cells), each with the positive control that stops it being satisfied by an admission that refuses everything. The e2e broker probe still reserves the cell whose offer won, leaving exactly srv3-06.1. Re-verified on a compiler rebuilt from this HEAD after finding the previous binary was 87 commits stale. CapacityAdmission and CapacityAdmitted collided with gunbc.fleet_capacity_control, which answers a different question -- whether a HOST is active by provider. Names are corpus-global and a duplicate refuses whole-corpus while every entry-scoped witness passes, so the collision was found by sweep rather than by the eight green rows. Renamed to CapacityClassAdmission / CapacityClassAdmitted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…on, because purity makes the join free ExecutionGrant carries resource_reservations and money_reservation, and its own annotation states the invariant: "resource admitted with money refused must commit no resource reservation, and money admitted with resource refused must commit no money reservation; both are one canonical state transition. A partial commit is the state that leaks capacity or budget with no grant to account for it, and it is unreachable only if the join is atomic rather than sequential." That join did not exist. This is it. ATOMICITY IS NOT A PROTOCOL HERE, AND THAT IS THE WHOLE DESIGN. Two-phase commit, compensating release, an undo log -- every one of those makes the partial state REACHABLE and then works to escape it, which is validation standing where construction was available. These ledgers are PURE: reserving returns a new ledger rather than mutating one. So the join simply declines to produce a pair unless both sides advanced, and the partial commit has no constructor. Nothing unwinds because nothing was ever applied. On a money refusal the advanced resource ledger is computed and goes out of scope -- in a mutating design that branch is the leak. GENERIC OVER BOTH QUANTITIES, WHICH IS WHY THIS CUT IS SMALL. EncumbranceLedger <Q, S> in extdeps.accounting.encumbrance is already the cited authority for holding a commitment against an appropriation, and product.fabric.budget is one instantiation of it for money -- complete, with lease generation fencing, and consumed by nothing but its own witness. A resource ledger is a SECOND INSTANTIATION, not a second authority, so this join names no quantity at all. Inventing a resource-specific ledger beside the generic would be the re-invention DESIGN calls a failed decomposition. An earlier note of mine said this was blocked on "two ledgers that do not exist". That was wrong and is corrected here: the generic authority and the money instantiation both exist. `ReservationRef` being a branded string is true; "therefore nothing holds anything" was an inference past a verified fact, and budget.dag holds and fences things today. ONE REFERENCE KEYS BOTH SIDES, and that is load-bearing rather than tidy. The encumbrance authority refuses a duplicate reference, and its own note explains why: first-match resolution and rewrite-all-matches are the same operation only while a reference is unique. THE REFUSAL ARMS CARRY NO LEDGER AT ALL, so a caller cannot mistake a refusal for a no-op advance and persist it. That is the reachable form of the leak in a pure design: a caller writes back whatever joint_reservation_ledgers returns, so an arm that carried the advanced pair would be committed to storage by a caller doing exactly the right thing. EVIDENCE, INCLUDING A RED THAT ACTUALLY FIRES. Six rows green, both refusal directions asserted separately because the arms are separate code. Verified by execution in both directions: with the money-refusal branch changed to commit the resource side -- the partial commit itself -- the guard returns FALSE while the positive control stays TRUE. A FIRST DRAFT OF THAT GUARD WAS A DECORATION AND IS RECORDED HERE BECAUSE IT ALMOST SHIPPED. It asserted that the caller's own ledger was unchanged after a refusal. The ledgers are pure values, so that assertion CANNOT FAIL whatever the join does -- permanently green by construction, and worse than absent because it would have been cited as the guard against precisely the leak it could not detect. The replacement asserts what is authorable: a refusal yields nothing to persist. WHAT THIS DOES NOT DO. It mints no ReservationRef and issues no ExecutionGrant. Binding the held pair to a minted reference, and requiring ExecutionGrant to carry held reservations rather than branded strings, is the following cut -- and it is now executable rather than blocked, which the previous frontier was not. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… both ledgers itself HEAD landed product.fabric.joint_reservation as a standalone module that took two pure ledgers and returned a joined outcome. Nothing else was ever going to call it. The only caller it could have -- the broker in gunbc.fabric_control_plane -- already holds the demand, the offer, the selection cost and the store slot, so routing them out to a module that knows none of those and back again is a second representation of one decision (§2). It is deleted at the root rather than refined from the leaves (§3, delete-first), and what replaces it is the broker making the reservation directly. WHAT SURVIVES IS THE GUARANTEE, NOT THE MODULE. CellReservation gains a BudgetRefused arm and CellReserved gains the advanced account, and that pairing is the whole safety argument: no arm carries an account without a cell, and no arm carries a cell without an account. The partial commit -- an encumbrance with nothing running, or a running cell nobody is paying for -- has no constructor, so it is unwritable rather than checked (§4b, structurally impossible). THE ORDERING CLAIM WAS WITHDRAWN, AND THE RECEIPT IS WHY. A witness asserting "the budget refuses before the store is touched" was authored, went green, and STAYED GREEN under a mutation moving the compare-and-set ahead of the encumbrance. The substrate is lazy: the branch that is not returned is never forced, so both spellings are equally effect-free and the row discriminated nothing -- a decoration cited as coverage. It is replaced by rows that assert what the carrier actually guarantees. THREE ROWS, EACH EXCLUDING WHAT THE OTHERS ADMIT. A ceiling below the liability refuses with a ledger cause. An offer quoted in a currency the account does not hold refuses on the OTHER axis, which is what excludes a broker that returns BudgetRefused unconditionally -- and it is only authorable because the currency presented to the budget comes from the offer rather than from the account, which would have made the check green by construction. A ceiling of 999 against a liability of 1000 refuses only if the FULL selection cost was presented, so a broker encumbering the marginal charge alone goes red where the other two stay green. Compile: 0 blocking over both entries. All five rows verified returning true by execution, not by typecheck. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Review 57180 (codex/gpt-5.6-sol, REQUEST_CHANGES) flagged two Boolean predicates over substrate coproducts and cited a predicate-dissolution rule in DESIGN.md. THAT RULE IS NOT IN DESIGN.md. It lives in docs/plans/nat-grounding-unification- design.md and it is narrower than cited: a manual match is forbidden WHERE A CANONICAL FOLD ALREADY EXISTS, which is why is_zero must become nat_cata. Neither CapacityClassAdmission nor CellReservation has a catamorphism, so the rule as stated does not reach either site. Following it to the code found two real defects underneath it, and both are worse than the thing that was reported. THE ROSTER WAS SILENTLY NARROWED WHILE THE ANNOTATION CLAIMED OTHERWISE. admitted_cell_roster kept the admitted through the Bool; refused_cell_admissions collected the refused and HAD NO CALLER. So a demand refused entirely on the capacity-class safety line and a demand nobody offered anything for arrived as one symbol, and their remedies are opposite: offer more capacity, versus stop asking for capacity you are not sanctioned to use. The prose above them read "the refusals are COUNTED rather than silently filtered". Nothing counted them. That is the empty-observation narrow with a sentence standing where the mechanism was supposed to be. Two folds re-running one judgement could also only agree by convention -- an edit to either could put a candidate in neither half or in both, undetected. One partition_cell_roster now makes the decision once and returns both halves, so they cannot disagree, and NoCellAdmissible carries the refused population so the two states are distinguishable by the caller. The Bool dies with its only production caller. THE OTHER PREDICATE HAD NO PRODUCTION CONSUMER AT ALL. cell_reservation_is_held was called only by the two witness rows that existed to cover it -- an artifact whose only consumer is its own test. Deleted. What replaces it exercises the partition through the real broker: a refused executor is reported, an empty roster reports none, and the pair excludes a broker that always reports a refusal. AND THE FOUR CAPACITY ROWS WERE ASSERTING THROUGH A COLLAPSE THEY THEMSELVES DECLARED ILLEGAL. The Bool answered false for both a refused class and an unclassified executor, while the unclassified row's own annotation said those two states have different remedies and must not be collapsed. The row could not see the distinction it was about. Each now names its arm, and the substitution is executed rather than asserted: swapping the unclassified row's selector to the other refusal arm returns false, which is the red the old Bool could not produce. Compile: 0 blocking. Eight rows verified returning true by execution, plus the one mutation returning false. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ally says who holds it The broker minted reservations and nothing ever ended them. product.fabric.budget has had settle_money and release_money since it landed, fenced on the lease generation; product.fabric.arbitration models the DECISION as ReleaseDirective and says in its own header that the fabric releases nothing there. What was missing was the actuator. Measured before starting: release_money and settle_money had witness callers and ZERO production consumers. THE SLOT PAYLOAD WAS WRITE-ONLY AND RELEASE IS ITS FIRST READER. That is the part of this change that is not plumbing. The broker wrote the reservation into the slot and nothing ever read it back, so the question release has to ask -- IS THIS CELL HELD, AND BY WHICH RESERVATION -- had no answer. Without one, release is a blind write: it frees whatever is in the slot on the strength of a generation the CALLER supplied, which is a second account of who holds the cell and free to disagree with the store. The generation fence does not close that. It establishes the slot has not MOVED since it was observed, which is a different question from whether it is held and by whom. A slot already free at generation N admits a release presenting N, and that is not a harmless no-op: it writes free over free, so a re-reservation racing the second release finds its precondition broken by the release of a hold that never existed. So CellSlotState is typed, CellHeld carries the reservation reference itself rather than re-rendering the demand and offer into a second spelling of an identity that already exists, and the decode REFUSES an unrecognised payload rather than answering either state. THE PARTIAL RELEASE HAS NO CONSTRUCTOR, and it leaks the opposite way to the reservation's: freeing the cell while the encumbrance stands bills a customer for an idle machine, and releasing the money while the cell stays held strands capacity under work nothing requires. Same construction argument as the reserve half -- the money transition is pure, the slot write is the only effect, and no arm of CellRelease carries one without the other. AND THE FUNCTION WAS UNREACHABLE UNTIL THE LAST COMMIT OF THIS CHANGE, WHICH THE WITNESSES COULD NOT HAVE TOLD ME. release_reserved_cell takes a CasSlotObservation, and that type had no production producer anywhere: the file store answers CasSlotProbe and file_compare_and_set converts internally without ever building an observation. So the release path was callable only from hand-built values, and my own witnesses were authoring the exact input the store is supposed to supply -- an artifact with no final consumer, hidden by its own tests. Found by writing the live probe row, not by the witnesses. The repair is one observation surface in the store, observe_cas_slot_state, plus release_reserved_cell_at beside the pure decision. It deliberately does not delegate the bound arm to cas_probe_as_readable: that projection answers CasReadableAbsent for a slot past the probe bound, which is right for reporting a lost race and wrong for a decision caller, who would read "the cell is empty" from a store that could not tell it anything and pick the remedy for an empty cell instead of repairing the slot. file_compare_and_set is left alone -- it produces outcomes rather than observations, so there is no second producer, and restructuring it would rewrite a load-bearing function whose header narrates a previously-fixed write-decides bug for no gain to it. Seven witness rows, every one green by execution, and the holder wall carries an executed RED: disabling the comparison returns false. Compile 0 blocking across the witness and probe entries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…on it Review 57256 (APPROVE, non-blocking) noticed that decode_cell_slot_payload computed the body ONCE against the length of the held tag and reused it for the free arm, which is correct only because both tags happen to be five characters. The note is right and the coupling bought nothing, so it is removed rather than documented. WHY IT WAS WORTH A COMMIT RATHER THAN A REPLY. The failure it sets up is silent and delayed: a third tag of any other length decodes to a body sliced at the wrong offset, and every existing row stays green because the two tags that already exist still agree. So the check that would catch it is exactly the check nobody writes -- the round trip over a tag that does not exist yet. The same defect had a second face the note did not name: each tag was spelled TWICE, once rendering and once decoding, so the two spellings could drift independently of the lengths. Both are one rule. The tags are named once and the body is derived from the tag that MATCHED, so there is no offset to get wrong and no second spelling to disagree. PROVEN BY EXECUTION RATHER THAN BY INSPECTION, because "now it is decoupled" is the kind of claim that reads as obviously true and is worth one run: with cell_free_tag temporarily changed from "free|" to "released|" -- five characters to nine -- both_slot_states_survive_the_round_trip still returns true. Under the previous form that substitution sliced the free body at offset 5 and would have failed. Tag restored, compile 0 blocking. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm exercised one of them. The near miss that hid it: `[A,A]` answered
`[A,A]` DOES refuse correctly as repeated-observed, so the obvious fixture finds
nothing. Only the answered-once case slipped.
REPAIRED AT TWO LAYERS, and the receipt shows neither substitutes for the other:
- `ObservationRepeatedExpected`, checked FIRST. The other three arms are
statements ABOUT a question set and are meaningless without a well-formed one;
answering "missing" here names the OBSERVATION as the defect when the ROSTER
is, sending a consumer to fix the wrong artifact.
- `prove_repair_roster` refuses a duplicate outright, so a `ProvenRepairRoster`
cannot HOLD one -- construction at the mint rather than validation at the join.
The generic arm is NOT dead after the proof-side wall: the law is key-generic and
`legacy_binding_observation` derives its expected list with no proven roster, so
the arm is reachable from that consumer's denominator. A quiet guard, not a
decoration.
MUTATION RECEIPT, two independent mutations in sequence (not overlapped):
deleting the law's check reds 2 arms and leaves the proof arm TRUE; deleting the
proof's refusal reds only the proof arm. Unmutated, 24 arms green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Carry the repeated-expected arm into the two binding witnesses the new variant also made non-exhaustive
`ObservationRepeatedExpected` landed with arms added to the repair envelope and
its witness, and NOT to the two binding witnesses that match the same
key-generic law. Six matches, one arm each.
WHY IT REACHED CI: the local check was `v1_src_dag_parse`, which returned
`4210 file(s) parse-clean` and was read as evidence the tree was well-formed.
Exhaustiveness is a RESOLVE-time judgment, so a parse sweep can never see it --
parse-clean and resolves are different claims about different phases, and the
green one was not about the thing being changed. The verification is now a
resolve of each affected witness, which reproduces the six diagnostics when the
arms are absent and passes when they are present.
The variant refusing every exhaustive match across three files is the substrate
doing its job -- nothing could have silently kept the old vocabulary. What
failed was my check, not the wall.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
* scm: a typed read-command result that names no destination (#9443)
* scm: a typed read-command result that names no destination
Recut onto current main so the diff matches the scope this PR claims.
WHY THE RECUT. The previous composition reached main through the save
branch's ancestry, so it carried repository_save.dag and its witness --
neither of which is on main, and both of which belong to #9434, which is
draft. Merging this PR would therefore have landed the parked save half
as a consequence of branch topology rather than as a decision anyone
made. Nobody would have done anything wrong; the ancestry would simply
have outranked the park.
The park is respected rather than routed around. No convert_to_draft
event exists on #9434 and draft is not this tooling's default, so the
hold is unexplained rather than accidental -- and the correct response to
an unexplained hold is to leave it standing.
WHAT REMAINS, and why the load refinement is not scope creep: splitting
RepositoryLoadRefusal out of RepositoryLoad is what lets
ScmReadRepositoryUnavailable carry a refusal that CANNOT hold a success.
Without it this module's unavailable arm would be constructible holding
RepositoryLoaded, with nothing to refuse the pair. It is the enabling
half of this change, not a neighbour travelling with it.
The dependency runs one way, checked before cutting: the save witness
imports RepositoryLoadRefused, and nothing read-side references save. So
dropping save costs this PR nothing.
Both keystones return `true` on this tree over current main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Drop the refusal-path accessor: the third instance of a shape this PR
documents as twice-removed
`repository_load_refusal_path` had exactly one occurrence in the tree --
its own definition. No consumer, so DESIGN section 6 residue.
WHAT MAKES THIS WORSE THAN ORDINARY DEAD CODE: read_command.dag's own
header, in this same PR, cites this exact helper shape being removed
twice before -- once as `checkout_succeeded`, once from
`gunbc.scm.ancestry` under review 56207 -- and states the reason that
survives. This change re-added the third instance while documenting the
first two. Neither a lens nor a green run can see that; only reading the
two files against each other does.
The surviving rationale in the deleted comment block was about the TYPES
(why no `loaded: Bool` exists), not about the accessor, so it moves to
`type RepositoryLoad` rather than being deleted along with the function.
A prose row removed for one reason must not silently take its contents
with it.
It gains the reason the shape keeps recurring, which was written down
nowhere: with no consumer the accessor is residue, and WITH one it is
worse -- a fourth refusal arm would be absorbed by the projection instead
of failing to compile at each site that must decide about it.
Both keystones return `true` after the deletion.
Reported by review 57012.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Enroll the three read-command route gaps the floor actually reported
The floor reported route_gap_unenrolled=3 on this branch, all three in
scm_read_command_witness, all with one cause:
the hermetic route has no arm for Read (operation declares no
mock_response)
scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer
scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log
scm_read_command_keystone_holds
Same boundary already recorded for the load witness: extdeps.filesystem
declares no mock_response, so the hermetic frame has no arm for a FAILING
read. All three claims exercise the absent-repository path, and the
keystone inherits the gap by composing them. They pass under `gunbc run`,
which performs the real read; they cannot reach their subject hermetically.
MEASURED, NOT PREDICTED. These were foreseeable and were deliberately NOT
pre-enrolled: enrolling an identity that does not gap is a stale row and
reds the build, which is what stale_route_gap counts. The rows are added
now because a run reported these exact three identities.
Enrolment records the gap as known debt. It does not make the gap
acceptable and it is not a fix: the remedy is a hermetic arm for a failing
read, which belongs to the filesystem boundary and not to this PR.
Roster 112 -> 115; the module still evaluates and returns its list.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Anchor a relative source root the same way in both module-index builders (#9548)
* Anchor a relative source root the same way in both module-index builders
The two builders disagreed on how a relative source root resolves:
try_build_module_index anchored through anchor_source_root (process
workspace), while try_index_source_root_into_module_index read the string
straight off the filesystem (process CWD). One concept, two answers,
selected by which builder a caller happened to reach.
The fork survived because the one place it is observable is the one place
nothing was asserting: every CI invocation runs with its CWD at the
workspace root, where both spellings denote the same directory.
A root that cannot be anchored still falls through to the existence
refusal with its ORIGINAL spelling, so the diagnostic names what the
caller asked for rather than a rewritten form they never wrote.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Trigger a fresh merge ref against main after #9551
The merge ref is computed when the head is pushed, against main as it was
at that moment; main moving afterwards recomputes nothing, and a RERUN
replays the original pinned ref. #9551 landed the four emit mirrors after
this branch's last push, so its base predates the regen fix.
Empty rather than a local merge of main deliberately: main's change here IS
the generated mirrors, and merging it locally would mean hand-resolving
emitted files -- the one state the regen gate forbids. Pushing recomputes
the base without touching them.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Measure the fan decoder's execution identity, and refuse to call it bound (#9536)
* Instrument the decoder's execution identity by composing two things that already existed
gunbc.bmc_fan_program_interpretation modelled a decoder identity and refused to author
one, because both digests are properties of an execution and a hand-written pair would
be two literals typed by whoever typed the decoder -- agreeing because one person wrote
both, and continuing to agree after the thing they describe changed. This produces them
from an execution instead, which is what an operator adoption needs: a corrected decoder
that assigns different meaning to the same bytes must be distinguishable from a refactor
that assigns the same meaning.
NOTHING IS MINTED. Both halves were found by searching before building, which is why
this module is short:
v2.lens.module_graph import_closure_live enumerates the entry's closure
tools.multi_module_compile_fixture compile_fixture returns a structural digest over
the (path, content) vector AND the
running compiler binary's own hash,
both host-computed from what ran
ONE NEAR-MISS IS DELIBERATELY NOT REUSED, and it is recorded so nobody "fixes" this by
adopting it. std.interface_summary typed_module_key is exactly the right shape -- a
source key combined with compiler identity -- at the wrong grain: its module_key folds a
module's source hash with its DIRECT IMPORT INTERFACE hashes. A body-only change in a
transitively imported module leaves it unchanged while changing what this decoder
produces; std.decimal canonical_exact_decimal could be rewritten and the key would not
move. It answers "may I reuse a cached typecheck"; this answers "is this the same
reader". Borrowing the first to answer the second invents the entailment rather than
misstating any fact.
THE DISCRIMINATING PAIR IS MEASURED, both halves, because an identity that moves on
everything and one that moves on nothing both look fine from a single run. Baseline
3282f082abc9d722 over 40 modules; one comment line added to std/decimal.dag, inside the
closure, moved it to 9bcfbd782022b120; one comment line added to gunbc/fleet_fan_wiring.dag,
outside it, left it byte-identical to baseline. Both restored byte-exactly. The compiler
digest held across all three.
The second half is the one worth having: a digest over the whole tree passes the first
test and is useless, since every unrelated edit would invalidate an adoption.
WHAT IS NOT CLAIMED. There is no enrolled witness, and the reason is structural rather
than neglect: the instrument reads the live tree and takes about four and a half minutes,
so the floor planner declines it, and the mutation half would have to edit tracked
source, which no hermetic witness may do. The evidence is a recorded measurement with its
controls -- weaker than an executing one, and said so rather than dressed up. The
next-rung trigger is a fixture-grain closure the instrument owns, at which point the pair
becomes an ordinary witness.
Cost is recorded too, because it decides where this may run: the closure walk alone is
about 4m28s. On demand only; nothing here is enrolled in a required lane, and a
four-minute live-tree walk on every push would be the corpus-denominated cost that gets
paid by every consumer wanting something else.
* Report the identity as measured-but-unbound, because nothing here proves the decoder ran on this vector
The side-chat raised the objection that matters and it is right. This instrument
enumerates a closure, hashes that exact vector, and compiles it. It does NOT execute the
decoder against that vector -- a semantic program digest is produced by some other run,
through the interpreter's own resolution of the same entry. Pairing this identity with
that digest would be two individually correct observations with an invented arrow
between them: the same fake join removed from the capture observer on #9299, one level
up.
The two subjects are very probably identical, since the walk follows the same import
edges the interpreter resolves. "Very probably" is what the objection is about. Nothing
here proves the interpreter received this vector and no wider one.
So the standing is not handed out from here. DecoderIdentityEstablished is what lets a
consumer treat two readings as same-reader, and granting it from a run that did not
perform the reading would restore the unbound claim under a name that reads as bound.
The binding is now its own three-state carrier, the measured-but-unbound arm names its
own gap, and the standing derived from it is still the absent one.
That is the instrument reporting what it has rather than failing. The obligation is
NARROWED rather than discharged: what was missing was any producer at all; what is
missing now is one execution that both hashes its source vector and runs the decoder
against that exact vector, returning the identity and the semantic result together.
That trigger is recorded on the arm.
* Sharpen the binding trigger to name the missing host capability
Looked rather than assumed, and the gap is larger than 'finish the instrument'. Two
routes could bind the identity to a decode and neither is reachable today.
EXECUTE-THE-VECTOR: the seed registers exactly one fixture builtin,
compile_dag_multi_module_fixture, which COMPILES a supplied (path, content) vector. No
builtin evaluates one. So running the decoder against that exact vector needs a new host
surface -- v1 seed growth, which the freeze admits only in service of the v2 self-host
program, and this is not that.
PROVE-THE-SUBJECTS-EQUAL: nothing exposes the RUNNING program's resolved module set.
module_declaration_facts reads the source tree, which is the same authority the closure
walk already consumed, so comparing the two would compare a reading against itself rather
than against what the interpreter received.
Recorded at this grain because a trigger that reads as small invites someone to just
finish it, find the capability absent, and close the gap with an argument instead -- which
is the invented arrow this carrier exists to refuse.
* Consume the decoder declaration instead of re-minting it (review 57069)
A byte-identical DeclarationRef for the decoder stood in this instrument
beside gunbc.bmc_fan_program_interpretation fan_program_decoder, which is
the module declaring the standing the instrument exists to discharge --
and which this module already imported from, so consuming it costs one
import member. Two authorities for one fact can drift independently
(DESIGN section 3); worse here than in general, because a drift would
identify a reader other than the one whose standing is at stake.
The entry PATH stays authored and is not the same fork: a module path
does not carry which source root stores the module, and deriving one
needs an observed ModuleStorageIndex rather than a pure transform. The
annotation now says so, so the next reader does not read the surviving
path as a missed half of this repair.
Measured after: identity unchanged -- 40 modules,
source_closure=3282f082abc9d722, compiler_runtime=f2c179fb7e10d373,
the same values the pre-fix baseline reported.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Say that the typed_module_key grain claim is an argument, not a measurement
The note asserted as fact that a body-only change in a transitively
imported module leaves typed_module_key unchanged while changing what the
decoder produces. The reasoning is sound and has now been endorsed by two
reviews and one external adjudication -- which is exactly why it needed
correcting rather than leaving: convergent readings of one argument are
not independent evidence about that argument, and an approved PR carrying
an unmeasured claim stated as fact is the rung inflation DESIGN 4b(1)
names as worse than sitting low.
I tried to measure it and found the route blocked, so the note now carries
that instead of the assertion. The only live producer of import interface
hashes is v2.lens.interface_summary module_key_for_rel_path. It has zero
consumers in the corpus; the first attempt to run it refused with
export_signature_facts `empty authored type name` on
extdeps.shell.credentials env_credential -- a pattern returning an
anonymous record, one of three such declarations. So that lens's live path
is inert in the DESIGN section 6 sense: the machinery exists and the first
exercise of it does not work.
Authoring the two export lists by hand was rejected rather than
overlooked: the claim IS that a body edit leaves the exports equal, so
asserting that equality assumes what the control exists to establish.
Next-rung trigger recorded on the note. Identity re-measured unchanged
(40 modules, source_closure=3282f082abc9d722).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Delete three commentary String rows and the digests they transcribed (review 57083)
The review flagged typed_module_key_grain_note, decoder_identity_
discrimination_note and decoder_identity_cost_note as the section 4c
pattern DESIGN discourages -- pure prose duplicating the // blocks above
them -- and noted broad corpus precedent for it. Precedent is the reason
to fix it in new code rather than the reason to keep it: adding fresh
instances of a discouraged pattern because the corpus is full of them is
how a discouraged pattern becomes the convention.
DESIGN is stricter here than the remark was. Two of the three rows
transcribed digests and a wall time into prose, inside the very module
whose entry point re-derives them, which is the standing "name the
instrument, never transcribe its output" ruling and not merely commentary
debt. So the numbers are gone from the // blocks too. What survives is
the SHAPE of the controls, which does not rot: an edit INSIDE the closure
moves source_closure, an edit OUTSIDE it leaves it byte-identical, both
restore. Anyone wanting the figures runs report_decoder_identity, which
prints them with the module count.
The // blocks are kept where they carry irreducible rationale -- why
typed_module_key is the wrong grain, why no hermetic witness can hold this
pair -- which section 4c permits and which the String rows were only
restating.
Re-measured after: unchanged, 40 modules, same digests the instrument
prints.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Witness evidence integrity: an undeclared live_tree_disposition silently declines the module — make silence REFUSE, burn down the 338, then the staged DeclinedLiveTree root deletion is safe (#9471)
* The live-read derivation detects a quarter of the readers it would have to replace
`v2.std.live_tree`'s note named the nightly affected-set falsifier as the thing
that catches a row declaring `SubstrateInputsOnly` while reading live state.
That cadence was deleted by the floor cut (#8283) and the repository carries
three workflows, none of which runs a predict-only cold comparison. The same
note stated the undeclared fail-closed default as THE fact, while the required
floor's own scan defaults the identical silence the opposite way -- so a reader
asking what happens to a witness that declares nothing was told the half that
withholds it, and the consumer that actually executes admits it.
What survives as the backstop is `effect_reach_derived_reads_live_tree_for_entry`,
and it does not derive this fact. It answers host-reading only when two
INDEPENDENT existentials both hold somewhere in the import closure -- some file
carries a repository path literal, some file carries a host-sink call shape --
so a closure that performs a real `Filesystem.Read` and names no path answers
false, and two modules that never call each other supply the two halves between
them. The ceiling is filed as a §4b row on the derivation's own authority, with
its next-rung trigger naming the capability (call-reachability-grade per-witness
classification) rather than an artifact that would contribute to one.
The evidence is a planted pair rather than a corpus count: two fixture entries
differing by exactly one import edge whose only content is a path-literal row,
performing a byte-identical read. The positive control derives host-reading; the
sink-only entry does not. Authored both sides, so the red is a property of the
derivation and cannot be dissolved by corpus drift.
The consequence runs opposite to the standing objection that an authored
disposition duplicates a derivable fact. `reads_live_tree_effective` consults the
declaration FIRST and reaches the derivation only for a row already claiming
SubstrateInputsOnly, so the derivation is the sole thing between a lying row and
a predict-skip. Replacing the declaration with it would be a scope narrowing
wearing a construction argument.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* The derivation's third bound: an unreadable closure file is skipped toward ADMIT
Confirmed by reading effect_reach_derived_reads_live_tree_for_closure_paths: a
closure file that cannot be read hits a bare `continue`, leaving both flags as
they were. Every unreadable file therefore biases the accumulation toward false,
which biases toward admitting a row that claims SubstrateInputsOnly -- the one
arm that could notice its own blindness discards it, in the direction that
weakens the only thing standing behind a lying declaration.
It compounds the empty-adjacency bound rather than sitting beside it: where the
closure is the entry alone, one failed read leaves the loop having seen nothing.
And unlike the conjunction and the adjacency, which are properties of the corpus
and measurable today, this one is a property of the run, so its magnitude is
whatever the filesystem did that time and nothing records it.
Found by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Route the ceiling row onto the ladder vocabulary instead of a prose blob
Review 56493 observed that the §4b class row was a large `String`, which §4c
names as misplaced data, and reported that no typed §4b carrier existed to route
into. One does: `gunbc.guarantee_rung_drop` declares the closed `GuaranteeRung`
vocabulary, and `gunbc.hermetic_mock_fidelity` already files a discovered class
in exactly this shape -- typed rung and ceiling, closed-coproduct reasons, and
rationale left in annotations beside the row.
So the row follows that pattern rather than minting a class of its own. The three
bounds become a closed coproduct, because naming them is what lets the class be
recognised a second time; enforcement becomes two reachable arms rather than a
sentence; and the next-rung trigger is DERIVED by a total function over the
coproduct rather than stored, which makes a trigger-less row unwritable instead
of merely checked. That all three bounds derive the same trigger is the finding,
not a redundancy: the capability replaces the approach rather than patching a
term.
The record is named for its subject. No corpus-wide §4b carrier exists, and
minting one from a single instance would put a second authority beside
hermetic_mock_fidelity -- the ladder VOCABULARY is the part that must not fork,
and that is what is reused.
Verified by execution: `gunbc compile --entry src/v2/std/effect_reach.dag`
returns 0 blocking errors, 21 files emitted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record that stamping the silent population was built and dropped
A future reader who finds the fail-closed default and the 24.7% backstop
measurement will reach for the obvious move -- stamp every silent witness file
-- and there is nothing in the tree telling them it was already tried. It was:
520 files stamped, silence made a typed located refusal on both consumers, then
discarded because the floor's decline arm was already being deleted at its root,
which is what made a truthful ReadsLiveTree stamp cost coverage in the first
place.
The note records the reason rather than the fact, because the reason is what
transfers: the arm's deletion is the enabling event for a truthful stamp, not
its reward, and the question revives when the selection consumer acquires an
enforcement it currently lacks -- not when the silent population grows.
Suggested by swift-badger-524, who observed the work would otherwise be visible
only in a reflog and one message.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Sweep the dead-cadence enforcement claim from all three of its homes
One claim lived in three places: v2.std.live_tree's disposition note, the same
module's stamp_provenance row, and a mirrored comment above
parse_entry_live_tree_disposition in cli_run.rs. Each said the nightly
affected-set falsifier catches a row declaring SubstrateInputsOnly while reading
live state. falsifier.yml was deleted by the 2026-08-15 floor cut. Correcting one
home leaves the other two as authorities for a false claim, so all three move
together.
The stamp_provenance row gets more than a past tense, because its consequence is
specific: the 2026-07-11 batch is machine-vouched rather than author-vouched and
inherits the deleted classifier's blind spot -- a live read hidden behind an
import was invisible to entry-text scanning. Those stamps were admitted on the
promise that a cadence would catch them if wrong. That promise is now UNMET, not
merely unfulfilled: nothing verifies a stamp, and one that was wrong the day it
was written is still wrong and still unobserved.
Three other authorities carry the same claim and belong to other owners; they are
deliberately not in this diff.
Verified: gunbc compile --entry src/v2/std/live_tree.dag -> 6 files emitted,
0 diagnostics.
Sites located by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Turn the supply fold from an honest screen into a real cross-mode selector: the six inputs supply.dag names as missing (#9472)
* wip: cross-mode supply selector
* wip2
* wip3
* wip4: duration state, commitment horizon
* review: fail-closed unbounded-duration availability, quote billing basis projection, Second-typed axis params
* witness: choose the window that the previous fold actually admitted
* Answer the new affordability arm in the sibling fabric witness suite
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids (#9564)
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids
Review 46148 ruled that absence is established by a successful listing and never
by a failed read. The ruling was written as a `data ... : String` note, which
DESIGN section 4c calls commentary no `Accepted` program can read -- and it was
then violated in gunbc.deploy_transition, authored beside the note, where a
present-and-unreadable marker rendered as absent and so as PERMITTED at the belt
seam (#9561). A note is not a mechanism.
extdeps.filesystem.filesystem_io gains a carrier with one mint.
FilesystemEstablishedAbsence is sole_constructor; its only mint takes a
FilesystemDirectoryListing, itself sole_constructor and minted only from a
listing whose success channel was true. A module deciding absence from a read
alone has no value to return and no way to build one. filesystem_entry_presence
and filesystem_file_observation are the folds: presence is decided by the
listing, the read is consulted only for an entry the listing named, and every
way of not establishing absence lands in one indeterminate arm.
Consumers, so this is not a carrier with no consumer:
- gunbc.roadmap_verification_receipt, both walks. Already correct by hand; they
now consume the carrier instead of restating the rule, and their private
second spelling of List's wire encoding is deleted for
filesystem_listing_names_entry.
- gunbc.devboot.build read_text_file,…
# Conflicts: # DESIGN.md # dag/gunbc/discovery_census.dag # dag/gunbc/durable_cas_file_store.dag # dag/gunbc/fabric_control_plane.dag # dag/gunbc/guarantee_rung_drop.dag # dag/gunbc/scm/read_command.dag # dag/gunbc/seed_growth_admission.dag # dag/gunbc/witness_deferral_freeze.dag # dag/test/claim/discovery_census_witness_test.dag # dag/test/claim/fabric_control_plane_witness_test.dag # dag/test/claim/srv1_residue_rehearsal_witness_test.dag # dag/tools/fabric_control_plane_live_probe.dag # src/v1/05_emit_rust.dag # src/v1/stage0/src/cli_run.rs # src/v1/stage0/src/v1_compiler_emit_rust.rs # src/v1/stage0/src/v1_compiler_infer.rs # src/v1/stage0/src/v1_compiler_infer_types.rs # src/v1/stage0/src/v1_tests_claim_reference_derived_disposition_census_witness_test.rs # src/v2/workflow/floor_expected_red.dag # src/v2/workflow/floor_route_gap.dag # src/v2/workflow/required_floor.dag
…hot had re-added what #9496 deliberately removed The update-branch snapshot inside the squashed #9604 carried main as it stood at 18:18Z, which still contained the fifth-arm discriminating red that #9466 added. #9496 then retracted it on main. Merging the stale snapshot forward re-proposed that block, so this branch's delta silently reverted another lane's deliberate removal. This branch owns four files. Anything else in its diff is snapshot residue, not a change anyone authored here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Clean text merge, no conflicts -- GitHub's CONFLICTING status was computed against an older main. Verified after merging: zero conflict markers, DESIGN.md and ROADMAP.md byte-identical to main (generated artifacts, so a silent text-merge would have been the hazard), and the branch's own 4-file contribution intact. Owner session (silent-bear-842) is idle; merged forward by crisp-newt-899 under the wind-down directive to get open PRs conflict-free and pushed.
Contributor
|
Closing as an accidental duplicate of #9598 — same four files, same content, opened from a local working branch name. `wip-release2` is my scratch branch for resolving #9598's conflict against the second reorg (#9641). I did not push it — this session auto-pushes local branches, which is also what produced #9633 from `wip-release` earlier tonight. I want to correct my own earlier explanation of that: I told a peer the cause was pushing a refspec of the form `git push origin :`, letting the local name reach origin. That was wrong. I ran no push for this branch at all, so the mechanism is the session auto-push, not the refspec form. A lane acting on my first explanation would have looked in the wrong place. #9598 is the one to keep — it holds the review history (four approvals), the settlement layer merged in from #9604, and is the branch the operator has been asked to rule on. Two PRs on one head also couple their check state, and #9633 demonstrated the cost concretely: two — sent from silent-bear-842 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
silent-bear-842.Pushing to
wip-release2advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan