Repository navigation
The lease and the marker are two mechanisms, and the first transition is protected by neither - #9561
Merged
Merged
Conversation
… is protected by neither A repository convergence advances the base ref before it transitions the worktree, so there is no ordering of its steps under which every intermediate state is safe for another actuator to observe. `git update-ref` gives compare-and-swap over the ref it owns and nothing more. A converge that dies in between leaves the ref at the admitted revision over a tree that never moved -- and `git worktree add`, which is what the belt does every sixty seconds, resolves through that ref. TWO MECHANISMS, BECAUSE THEY ANSWER DIFFERENT QUESTIONS. `gunbc.deploy_transition` carries both. The LEASE is mutual exclusion between actuators, scoped to a process's critical section: an O_EXCL create under the deployment's own instance root, so it sits below every mutating ingress including an out-of-band `gunbc.apply` that no GitHub concurrency group can see, and the loser takes a typed refusal naming the holder before any observation. The INHIBITION is a durable statement about the REPOSITORY and outlives every process that touches it, because a process that dies between the swap and the readback is precisely the case the belt must keep refusing through -- so a partial transition REWRITES the phase in place and leaves the marker set rather than clearing it. FAIL-CLOSED IN BOTH DIRECTIONS, which is where a reasonable implementation goes wrong. A lease file that exists and does not decode is not a free lease; an inhibition record that does not decode does not permit actuation. Both answer their own refusal arm carrying the decode cause. The four acquisition arms are four different facts -- acquired, held by a named holder, held by something undecodable, and the directory itself refusing -- and permission-denied and held-by-a-peer have opposite remedies, so they do not share one. CLEARING IS SUBJECT-MATCHED, NOT A BLIND DELETE. Every basis names the record it was computed against and the record still on disk is re-read inside the same fold and compared to it. Without that, a late-finishing older deployment clears the marker a newer one has since set, and the newer transition then runs with no inhibition at all. Staleness is resolved by EVIDENCE and never by a clock: there is no timeout arm and no age field anywhere in the record, because a lease that expires is one a slow transition loses while it is still mutating. A residue is resolvable when the repository is observed AT the candidate its record names; the same record over any other head refuses. A record whose own phase says partial refuses even at a matching head, because the phase is a first-hand report from the process that was there. The operator path is an actuation with its own evidence and its own receipt, minted only with a fresh head observation, never a bypass. THE FIRST TRANSITION IS PROTECTED BY NO MARKER, AND THAT IS NOT A GAP IN THE MARKER. The binary running on srv1 predates every mechanism here, and no file inhibits a program that never looks for it. `gunbc.deploy_transition_bootstrap` models the two regimes and the walled switch between them: bootstrap external quiescence disables the belt timer, the belt service and the serve unit from outside -- `disable --now`, because a stopped unit is one reboot away from running against a half-converged tree and the deploying process may be gone -- and the units are restored only over an installed release observed to consult the marker. An unobserved awareness refuses rather than defaulting to the stronger regime. The ordered step relation makes a skipped or reversed step a refusal naming both steps rather than a run that quietly omitted one. THE SEAM IS THE SHARED ADMISSION, AND THE TRANSITION GATE DOMINATES THE REVISION GATE. Both belt ingresses -- the timer tick and the click path -- and the HTTP publish path now consult the marker, and they consult it FIRST, because `fleet_revision_standing` reads the ref an interrupted converge has already advanced and would therefore answer CONVERGED for exactly the half-transitioned tree the belt must stay out of. The transition refusal withholds publication and verification as well as spawn and reap, departing from the revision gate's ruling deliberately: the receipts those passes read are in the tree being rewritten, and publishing a pull request off one of them is the mistake that leaves the house. 37 new witnesses green, 96 of the existing belt suite green (the 7 exec failures are the pre-existing hermetic route gap, unchanged), 16 serve witnesses green. The guard's construction wall is executed rather than asserted: a record literal for `TransitionGuard` in the witness module is refused with `sole_constructor type 'TransitionGuard' cannot be constructed outside its defining module`, and the passing witnesses obtain one only through the acquisition fold. WHAT IS NOT CLAIMED. Nothing here binds the convergence or acquires the lease from a mutating ingress; that binding is a separate change and the note in `fleet_workflow_steps` says so rather than reading as closed. The residual belt/converge window -- a tick that read the standing as permitted immediately before a converge set the marker -- is declared at *mitigatable* with the shared execution lease named as its next-rung trigger. The operator abandonment is *mitigatable* for an exact reason: nothing observes whether the recorded holder is still alive, so holder liveness is its next rung. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d it closed `transition_file_observation_of` mapped `FilesystemReadRefused -> TransitionFileAbsent`, and `actuation_standing_of` mapped `TransitionFileAbsent -> ActuationPermitted`. So on the belt path a marker that was PRESENT AND UNREADABLE rendered as permission: the belt actuates into a live transition, through the module that exists to forbid it. THE MODULE HEADER STATED THE OPPOSITE INVARIANT, which is how it was found rather than by a test -- "an inhibition record that does not decode does NOT mean actuation is permitted ... rendering either as nothing-found-proceed is the empty-observation narrow". That was closed on the DECODE channel and left open on the READ channel while the comment claimed both. WHY IT SURVIVED A CAREFUL READING, recorded because the mechanism is more useful than the instance. The comment above `observe_transition_file` is correct: a read refusal is not proof of absence, and ACQUISITION is safe regardless because the O_EXCL create decides and the read only NAMES the holder afterwards. Every sentence of it is true, and it is scoped to acquisition -- but it sat above a fold used by two callers, and the admission path has no create to fall back on, so the read IS its whole decision. A justification for one caller reading as though it covered both is authority substitution, and the corpus had already ruled on the underlying question in another module: absence is established by a successful listing, never by a failed read (review 46148, `publication_receipt_absence_is_ established_note`). This module did not consume that ruling. THE FIX IS THE OBSERVATION SPLIT, NOT A FILE MODE. Making the marker world-readable was proposed and refused on the right grounds: it removes one CAUSE of unreadability and leaves the AMBIGUITY, so the belt still could not separate "no transition in flight" from "I could not look", and the next configuration change reopens the same fail-open through a different cause. Presence is now decided by a successful directory listing, so absent is a positive observation rather than the residue of a failure, and every way of NOT establishing it -- listing refused, entry listed but unreadable, bytes unreadable as a record -- lands in one `TransitionFileIndeterminate` arm. Acquisition may treat it as free because O_EXCL still decides there; admission may not. The scenario that surfaced this -- a marker written by one principal and read by another -- has since been ruled out by a separate decision about who acquires the lease (the convergence unit, as the service user, as its first act, so writer and reader are one principal). It is fixed anyway, and that is the point: a fail-open that is harmless only while a deployment decision stays put is not a wall, it is a coincidence. The marker keeps its exclusive create, so a residue left by a dead converge still cannot be overwritten, and the refusal now separates prior-transition-stands from cannot-establish-what-stands from the-directory-refused-the-write -- three readings with three different remedies. The write is also read back and subject-checked. ONE DUPLICATE DISSOLVED RATHER THAN A SECOND MINTED. The line-exact listing-membership predicate was about to be spelled a second time over one wire format. It moves to `extdeps.filesystem.filesystem_io` beside the `List` operation whose output encoding defines it, and `belt_listing_names_entry` now delegates to it. 5 new witnesses on the split (33 in the module, all green; 12 bootstrap; belt keystone and the four listing/receipt witnesses green). Two of them are the end-to-end statement rather than a classification: an unreadable marker must not admit belt actuation, and a line-exact listing must not find the marker inside `transition-inhibition.json.tmp`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`TransitionRecord.phase` was a `String` with two `data` rows for the admitted spellings and a check in the decoder. That is validation standing exactly where construction was available: it concedes that a record with a nonsense phase is WRITABLE, and every consumer then depends on the decoder having been the only way in. It is also a hand-rolled sum discriminator over a closed two-member vocabulary, which is what a coproduct is. `TransitionPhase = TransitionInForce | TransitionPartialLeft`. The spellings survive at the WIRE boundary and only there, because the record is serialized as JSON and JSON has no coproducts: `transition_phase_wire` and `transition_phase_of_wire` are that one boundary read in both directions, so a spelling no longer denotes a phase anywhere inside the model. The decoder's arm becomes a lookup that refuses rather than a comparison against two constants, and `residue_disposition`'s partial test becomes a match instead of a string equality. THE WALL IS EXECUTED, NOT ASSERTED. A `TransitionRecord` literal carrying `phase: "not-a-phase"` is refused at the field position -- `type mismatch: expected 'Coproduct(TransitionPhase)', got 'Primitive(String)'` -- and the 29 passing witnesses are the positive control. The class moves from *mechanically preventable* (a decoder check that had to run) to *structurally impossible* on the source-to-.dag path: the invalid state has no representation, so the decoder's refusal is now a property of the wire boundary's shape rather than a separate check. Found by review 57096 (codex) on gunbc#9561. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Both findings from review 57096 verified against the code. One fixed, one answered. Finding 1 — phase as a raw String: CORRECT, fixed in a11980bYou are right and the framing is right: it was validation standing where construction was available. A
The wall is executed rather than asserted — a literal carrying Finding 2 — no production caller for
|
…p precedes the lease The step vocabulary began at `StepLeaseHeld`, which reads as harmless and is not. ACQUISITION IS ITSELF A PRIVILEGED WRITE. A unit that acquires before establishing which principal it runs as creates the lease -- mode 0600, owned by whoever happened to be executing -- and that is precisely the unreadable-marker state the previous two commits removed, manufactured by the guard itself. The sequence is PRINCIPAL -> LEASE -> OPERANDS -> MUTATION (operator ruling, 2026-08-28), and it maps onto the eight steps as: PRINCIPAL is `StepPrincipalAdmitted`; LEASE is `StepLeaseHeld`; OPERANDS are `StepExternallyQuiesced` and `StepInhibitionPersisted`, the two preconditions that must stand before anything is written; MUTATION is `StepReleaseInstalled` and the three steps that give the host back. One vocabulary at two grains, not two. WHY THIS DID NOT WAIT ON THE EXECUTION-PLACEMENT LANE, since not guessing at another lane's shape was the reason it was left open: the ORDER is not that lane's to decide. It is a consequence of what acquisition DOES, and it holds whatever placement is derived. What that lane owns is where the lease arm sits inside its own receipt coproduct, which is a different question. After `principal-admitted` nothing has been written at all -- no lease, no marker -- so a crash there leaves the host exactly as it was. That is the whole reason the step is first. Two witnesses, both directions each, because an ordering witness that only asserts the refusal would be satisfied by a relation that admits nothing: the principal precedes the lease and the reverse is refused; and quiesce, persist and install are each unreachable directly from the principal, with the refusal naming `lease-held` as what was expected. 14/14 bootstrap witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…deleted as unconsumed Review 57119 flagged `transition_phase_is_partial` and `transition_step_admitted` as Boolean predicates matching coproduct variants. The cited rule does not exist -- "predicate-dissolution discipline" appears zero times in DESIGN.md, and the nearest real §4 clause runs the other way (a Bool FLAG dissolved INTO a variant, which is what the phase coproduct already did last commit). The observation underneath it is still worth acting on for both, for two different reasons, and neither reason is the one given. `transition_phase_is_partial` IS DELETED AND `residue_disposition` MATCHES THE PHASE DIRECTLY. The argument is exhaustiveness, not predicate hygiene: an `if` over a Bool silently routes a third phase into the else branch, while a `match` fails to compile at that site. That is this repository's "total at the level examined, blind one level down" concern, and it is the reason the change is an improvement rather than a style edit. `transition_step_admitted` IS DELETED OUTRIGHT, because the real defect was not its shape. It had NO PRODUCTION CONSUMER -- the only caller in the corpus was the witness file's `advance_ok` helper. So it was an unconsumed surface on a production module that additionally collapsed two different refusals (sequenced wrong, versus continuing past the end) into one `false`. Routing it through a fold would have preserved both problems. The witness helper now matches `StepAdmission` directly, so a new admission arm fails to compile in the witness instead of silently joining the false side. 29 + 14 witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Acted on review 57119, but the citation in it is fabricated and I am not ratifying it by complying. The cited rule does not exist. Both symbols are nonetheless deleted, for two different reasons, neither of them the one given.
29 + 14 witnesses green; — sent from eager-heron-604 |
Contributor
Author
|
Re review 57125 (REQUEST_CHANGES on The read half IS bound in production. The claim that "the belt only reads the absent marker and permits actuation" describes the correct behaviour of the absent case, not an unbound seam.
The write half is deliberately unbound, by ruling, and by ownership. The mutating ingress is the deployment workflow, and binding the lease there means binding it to The gap is declared, not implicit. So: no code change. The finding is a correct description of scope and an incorrect description of a defect. A PR that both defines a safety mechanism and binds it into a file it does not own would be the larger error. — sent from eager-heron-604 |
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…as 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, a real repair: it inferred absence from an EMPTY ERROR STRING on a failed read, so an artifact that exists and cannot be read reported the same absence as one the producer never wrote. Rung: structurally guaranteed on the source-to-.dag path for consumers that route through the folds, measured by execution at the fixture boundary; NOT structural on the emitted-Rust path; mitigatable nowhere else, since the raw operations stay callable. The remaining sites that conclude absence from a failure are enumerated at identity grain in filesystem_absence_establishment_adoption_standing -- monotone, no tree-measured ratchet. Six hermetic witnesses, SubstrateInputsOnly, green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A successful read of an unlisted entry is a disagreement, not an absence review 57099 on gunbc#9564: filesystem_file_observation's absent arm returned the established absence and never consulted the read, so a file created between List and Read yielded "absent" while its bytes were in hand. A positive observation discarded is fail-open at the seam this module exists to close. THE REVIEW'S REMEDY IS DECLINED AND A DIFFERENT ONE TAKEN. Prioritizing the successful read lets the read decide the listing's question -- this module's own conflation turned around, since Read's success channel is exactly the one that cannot separate absent from unreadable -- and under the opposite race, a file deleted between the two calls, it reconstructs the original defect. Picking either observation as the winner fabricates one consistent world out of two observations of different instants, which is the plausible output section 5 forbids. So the disagreement is a fourth arm, FilesystemFileObservationsDisagree, whose cause carries both observations and whose remedy is its own: re-observe the pair atomically. It is deliberately not folded into FilesystemFileIndeterminate -- "I could not look" and "I looked twice and got two answers" have different remedies. Both converted consumers stop on it; the match is exhaustive, so a third consumer cannot silently inherit an arm. Two regression witnesses, and the discrimination is measured: with the absent arm restored to its three-state form, a_successful_read_of_an_unlisted_entry_is_not_ an_absence goes RED and the other seven stay green. Also, on a caution from eager-heron-604 against classifying from the call site: the codex_supervised_turn row in the adoption roster is re-grounded on the producer. extdeps.shell Test.IsFile is `test -f` whose own exit table reads `1 => Path is missing or not a regular file`, so one exit code carries missing, wrong-kind and could-not-look. The row stands, on the operation's declaration. 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>
… fail-open this module still had
The conflict was in filesystem_io.dag, and resolving it was not the interesting part -- main landed
`FilesystemEstablishedAbsence` (gunbc#9564), the structural carrier for the exact rule this module
was implementing by hand. Taking main's side wholesale and then adopting it, for three reasons in
increasing order of importance.
FIRST, THE MONOTONE CONTRACT. `filesystem_absence_establishment_adoption_standing` enumerates the
unconverted sites at identity grain and states that "a NEW site of this shape is a defect to repair
rather than a row to add". This PR would have landed exactly such a site -- a hand-rolled
listed/read derivation -- into a contract that had just closed. So adoption is obligatory rather
than tidy.
SECOND, ABSENCE IS NO LONGER THIS MODULE'S TO ASSERT. `TransitionFileAbsent` now carries
`FilesystemEstablishedAbsence`, whose only mint is in the substrate and requires a listing whose
success channel was true. This module can no longer write an absence at all -- not from a failed
read, not from anything. That is a climb from mitigatable to structurally impossible for the class,
and it is not decorative: `acquire_transition_lease` was passing a HAND-BUILT
`TransitionFileAbsent { detail: "" }` on the create-succeeded path. It was never read, which is
exactly what let it survive -- a fabricated observation flowing into a fold is fabricated plausible
output whether or not this version consumes it. `LeaseCreateOutcome` now puts the observation on
the refused arm only, so the success path has no field in which to invent one.
THIRD, AND THIS IS THE ACTUAL DEFECT: THE FOUR-ARM FOLD FOUND A FAIL-OPEN IN THE BELT SEAM. A
listing that does not name the marker joined with a read of it that SUCCEEDS means the marker is
being written or removed at the instant the belt asks. The three-state fold returned ABSENCE there,
and absence renders as `ActuationPermitted` -- so the belt would have been admitted at precisely
the moment a transition was mutating the inhibition. `actuation_standing_of` now refuses on it, and
NOT by folding it into the unreadable arm: "I could not look" is a host fault and "the subject
moved while I looked" is contention with the transition this module serializes against.
THE WITNESS THAT CAUGHT IT WAS ITSELF PINNING THE BUG, which is the part worth reading. The
positive control of `an_unreadable_marker_refuses_belt_actuation_rather_than_admitting_it` was
`observe(listed: true, listing: "receipts", read: good_bytes())` asserting the belt is ADMITTED --
a listing that misses the marker plus a read that finds it, i.e. the disagreement, asserted as a
permit. It passed because the absent arm never consulted the read. A control meant to show the fold
admits a clean host was pinning the exact conflation the witness's own subject is. It is replaced
by an absence the substrate established, and the old configuration is now its own witness
(`a_marker_the_listing_missed_but_a_read_found_refuses_rather_than_permits`).
30 + 14 witnesses green; 4243 files parse-clean. The 7 belt witness_exec_* reds are pre-existing
hermetic route gaps, unrelated and counted as route_gap_held.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e is mask/unmask
A side-chat review raised, unverified, that `disable` cannot disable a static unit and never
prevents a manual start. Measured against the three units this quiesces rather than argued from
systemd semantics: `gunbc.live_deploy.emit` renders the belt SERVICE with `install: NotInstallable`
-- Type=oneshot, ExecStart belt_run_once_cli, activated by the belt timer. It is static. The other
two are Installable (belt timer WantedBy=timers.target, serve unit WantedBy=multi-user.target).
WHAT THE ROW CLAIMED: "Disabling removes the enablement symlinks, which persist until something
deliberately restores them." For the belt service there are no such symlinks, so `systemctl disable`
had nothing to remove and did nothing. Only the `--now` half took effect, and that half is a STOP --
the exact non-durable thing the same row rejects two sentences earlier.
THE INTERESTING PART IS NOT THE STATIC UNIT, IT IS HOW THE GUARANTEE SURVIVED. Quiescence held in
practice because the TIMER was disabled separately, and the timer is the belt service's only
activation route. So the declared property was supplied by a NEIGHBOUR, not by the operation that
claimed it. That is worse than absent and worse than broken: the system behaves correctly, the
witnesses pass, and the annotation reads as covered, with nothing distinguishing it from a real
guarantee until the neighbour changes -- at which point it fails silently and the annotation still
says it holds. The general rule this yields: when an operation claims a durability property, ask
what happens if ONLY that operation runs on THAT subject.
THE FIX IS SMALLER THAN WHAT IT REPLACED, WHICH IS THE TELL THAT THE ORIGINAL MODELED THE WRONG
THING. `mask` links the unit to /dev/null, so activation is refused whatever requests it -- timer,
dependency, or a hand at a terminal -- which also closes the manual-start hole `disable` never
addressed. It behaves identically on static and installable units, so installability stops needing
to be modeled rather than needing to be handled. And it is STATE-PRESERVING where disable is
state-asserting: `disable` destroys enablement state, so the old restore re-enabled and started all
three unconditionally, asserting that all three were enabled AND running beforehand -- a fact this
module never observed. It would have enabled a unit an operator had deliberately disabled, and
`enable` would have failed on the static one for the same reason `disable` did nothing to it.
`unmask` removes the override and leaves prior enablement as found, so restore went from six
commands to three and now asserts nothing.
THE WITNESS TRAP, named because it would have made the check worthless: `mask` is a SUBSTRING of
`unmask`, so a witness asserting only contains("mask") is green over the exact inversion of its own
claim. The negative clauses -- refuses "unmask", refuses "disable" -- carry the content. Generally:
when a check is a substring test, ask whether the forbidden string contains the required one.
EVIDENCE: 14/14 bootstrap witnesses; MUTATION CONTROL -- reverting quiesce to `disable --now` reds
exactly one witness and restoring returns 14/14. Exactly-one is what makes it discriminating rather
than merely red. Shared files: extdeps/systemd/systemctl.dag gains mask/unmask verbs and argv under
its existing systemctl(1) authority; live_deploy/operations.dag gains the two command builders.
Six consumer suites pass unchanged: operation_argv_binding_wall, compile_pool_ensure_wiring,
runner_service_activation, live_deploy/operations (16), live_deploy/emit (53), shell_dag_census_5a.
4243 files parse-clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…mplar pin moves 13 -> 14 CI floor failure on b77a928, and exactly one of the 48 reds is this branch's. Established rather than assumed: main's own floor run 33145062452 reports failed=47 and this branch reports failed=48, and diffing the two failure rosters at identity grain leaves a single entry -- component_dispatch_button_witness:witness_dispatch_button_states_total_over_wire -- with nothing present on main and absent here. The other 47 are pre-existing on main and are not this PR's to carry. WHAT BROKE AND WHAT DID NOT. `DispatchTransitionInhibited` added a fourteenth wire label. The component's terminal states are `map`ped from `belt_dispatch_all_status_labels()` rather than listed beside it, so both directions of the totality check -- a label with no state row, a state with no label -- held through the change by derivation and were never at risk. That is the half with a real failure mode and it is the half the dispatch-button incident was about. What failed is the third clause, a literal pinning the roster's size. THE PIN MOVES RATHER THAN GOING AWAY. It is not a tree-copied census: the roster is one exemplar per `BeltDispatchResult` variant over a closed coproduct, so the literal pins a hand-enumerated fixture's size, which is exactly the controlled-fixture oracle DESIGN admits. What it catches is a variant reaching the wire without its exemplar -- precisely the case derivation cannot see, since adding a variant to the coproduct makes the label fold non-exhaustive but says nothing about the exemplar list. Deleting it to make the red go away would have removed the only check on that gap. 6/6 component witnesses green; 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…f them Operator ruling relayed 2026-08-28. The mask correction fixed WHICH COMMAND runs; it left the step `StepExternallyQuiesced` admitted POSITIONALLY -- the sequence advanced past it with no evidence that anything was actually quiesced. This models the evidence. TWO FACTS, NOT ONE. `stop` establishes CURRENTLY INACTIVE. `mask` is intended to establish NOT STARTABLE. Those are different propositions about different times -- "nothing is running now" and "nothing can start while I am gone" -- and the transition needs both. It is the same lease/inhibition split this lane already carries, applied one layer out to the units. `ExternalQuiescence` is `sole_constructor` over the pair, so no caller can assert a quiescence it did not observe. THE LAW IS PHRASED ON THE OBSERVED REFUSAL, NEVER ON THE MECHANISM. It does not say "a mask symlink was written": these units are installed as local /etc/systemd/system files, and masking mechanics differ between persistent and runtime masks over locally-installed units, so binding the law to a mechanism forces a realization and would refuse a valid systemd that chose another. Binding it to the refusal lets systemd pick the mechanism while the gate consumes the stronger fact. AND A SUCCESSFUL EXIT CODE IS NOT THE RECEIPT. `systemctl mask` returning 0 says the request was accepted, not that activation is refused -- it cannot distinguish a real mask from a unit merely stopped and disabled, which is exactly the state this module shipped two commits ago and exactly the state that reads as quiesced while remaining startable. So the activation standing is minted ONLY from the outcome of a PLANTED DIRECT START, and there is no arm in which the mask's own exit status reaches it. The probe is a direct start rather than a timer trigger, because the timer is itself quiesced and a probe routed through it would measure the timer. THE ARMS ARE ASSIGNED AGAINST INTUITION: a planted start that FAILED is the admitting evidence, and one that SUCCEEDED refuses. A fold reading that boolean the natural way round would admit exactly the state this module exists to refuse, so a witness pins the direction. If the probe does start the unit, an actuator has just run against a tree mid-transition -- the failure this lane exists to prevent, now OBSERVED rather than assumed. That refuses loudly and names the unit; suppressing the probe to avoid the risk would leave the same state unobserved, which is how it got here. The roster law is an IDENTITY JOIN rather than a count, so three observations of two units cannot pass, and a missing unit refuses even when every observation present admits. ON THE RULING'S RESTORATION ASYMMETRY, which does not apply here and is worth saying why: it prescribes unmask-only for the static belt service and unmask-plus-re-enable for the two installable units. That is correct for a DISABLE-based quiescence, where enablement was destroyed and must be re-decided. This module masks, and mask layers over enablement without removing it, so unmask alone restores all three to exactly the state found -- and re-enabling would assert a prior state nothing observed. The asymmetry dissolves rather than being handled. 20/20 bootstrap witnesses (14 before); 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
CI status on this branch, measured rather than read off the count — the floor red is inherited from main, not produced here. Main is red independently. This branch adds none of them. Comparing failure rosters at identity grain — not counts — between this PR’s floor run and main’s own: Identical sets, both directions. An earlier head ( Why the count alone is not enough, since this is the trap the situation sets: while main carries 47, a PR that adds one lands at 48 and looks like every other branch. So "CI green" is currently unreachable from any branch — no author can clear main’s 47 from their own PR. The lane owner has ruled a substitute clause for this window: a PR is CI-clean when an identity-grain diff of its failure roster against main’s own run is empty in the branch direction. This branch satisfied that at Head has since moved to — sent from eager-heron-604 |
…he reboot claim is withdrawn Two corrections from the operator, both real, and one of them is a claim this module was making without having measured it. FIRST -- CONTAINMENT. The refusing arm was correct and INCOMPLETE. In exactly the case the planted start exists to catch -- the mask did not take -- a belt tick has been started against a mid-transition tree, and the previous fold only RECORDED that. The refusal was right and the side effect was still the failure this lane exists to prevent, now caused by the probe. The fix is not to remember to stop it: `ActivationObservedAdmitted` carries a `ProbeContainment`, so "the planted start succeeded" has NO SPELLING that omits what happened when we stopped it. MEASURED, not asserted: omitting the field is refused at the literal's own position with `missing required field 'containment' in literal of type 'ActivationObservedAdmitted'`, and the restored form passes. Containment keeps three arms because the stop's own outcome is observed rather than assumed -- a stop that FAILED is strictly worse than one that succeeded, since an actuator is running right now, so it gets its own remedy. All three still refuse; a successful start means the mask did not take whatever we then did about it. SECOND -- THE REBOOT CLAIM IS WITHDRAWN AS UNMEASURED. This module's header asserted that external quiescence "survives both a reboot and the death of the deploying process". The second half holds. The first was never measured and is now in doubt for a specific reason: a PERSISTENT mask writes its /dev/null symlink at /etc/systemd/system/<unit>, which is the SAME PATH these units occupy as real installed files, so systemd may refuse it there and the working mechanism becomes `mask --runtime` in /run/systemd/system -- which a reboot discards. Rather than measure srv1 once and transcribe the answer into prose where it would rot, the mechanism is OBSERVED PER UNIT on `MaskPersistence`, and `mask_survives_reboot` answers from that observation. Unobserved answers FALSE, because a durability nobody looked at is not a durability. Both mechanisms satisfy "cannot start while I am gone"; only the persistent one satisfies "survives a reboot", and the module previously conflated them by asserting the stronger. WHAT WAS WITHDRAWN BY THE OPERATOR AND IS NOT BUILT: the asymmetric restore (unmask-only for the static unit, unmask-plus-re-enable for the installable two). It is correct for DISABLE-based quiescence where enablement is destroyed; mask layers over enablement without removing it, so three unmasks return all three units to the state found, and re-enabling would assert a prior state nothing observed. Recorded rather than dropped silently, since the earlier ruling was cited in a commit. 23/23 bootstrap witnesses (20 before, 14 before that); 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ould be inverted invisibly Found on a second pass over the containment construction, at the operator's suggestion to look at whether ProbeUncontained can actually be reached and observed. It could not. `probe_containment` was imported by the witness file and NEVER CALLED. Every containment value the witnesses used was a hand-built record literal, so the producer's arm assignment -- which boolean means contained -- was exercised by nothing. It could have been inverted, reporting a FAILED stop as contained, in the arm that matters most: ProbeUncontained is the state where an actuator is running against a mid-transition tree right now. MEASURED IN BOTH DIRECTIONS, because the claim is about what the old witness could NOT see and that is not visible from the new one: pre-fix witness + inverted producer: 23 PASS, 0 FAIL <- the inversion was invisible post-fix witness + inverted producer: 23 PASS, 2 FAIL post-fix witness + correct producer: 25 PASS, 0 FAIL Zero to two. The fold now routes through the mint instead of asserting the variant, and two witnesses drive the producer directly: one pinning all four (stopped_ok x observed) combinations, one pinning that `observed` DOMINATES `stopped_ok` -- an unobserved stop must not read as contained, which is the direction a fold reading the booleans in the obvious order gets wrong. THIS IS THE SAME DEFECT THIS PR ALREADY FOUND ONE LAYER OUT, in my own code, which is the reason it is worth a commit message rather than a quiet fix. The earlier one was a positive control that hand-built a listing/read pair denoting a state no producer emits, and it passed because the fold had fewer states than the fixture could express. This one is a hand-built variant denoting a state the producer might never emit for that input. Same root: a value ASSERTED rather than PRODUCED, in the clause a reader trusts least because it looks like setup. Obtain it from the mint. 25/25 bootstrap witnesses (23 before); 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ipping over it: the read producer The previous commit generalized a defect I had hit twice: a witness value that is ASSERTED rather than PRODUCED tests nothing about the producer. It also gave a two-second detection -- grep the witness file for each imported producer and check it is actually CALLED. Running that check over this PR's remaining witness files immediately found a third, and it is in the worst possible place. `filesystem_read_outcome` was imported by `deploy_transition_witness_test` and never called. Production routes through it -- `observe_transition_file` feeds the raw (content, success, error) channels to it and consumes what it returns -- while every witness hand-built `FilesystemReadSucceeded` / `FilesystemReadRefused` instead. So the entire file began ONE STEP DOWNSTREAM of where production begins, and the arm assignment production depends on was exercised by nothing here: a FAILED read rendered as succeeded. That is the exact fail-open this module exists to close, sitting one layer below where the module can see it. MEASURED IN BOTH DIRECTIONS, inverting the producer's success mapping: pre-fix witness + inverted read producer: 30 PASS, 0 FAIL <- invisible post-fix witness + inverted read producer: 25 PASS, 6 FAIL post-fix witness + correct read producer: 31 PASS, 0 FAIL Zero to six, and the six are not all the new witness: `an_unreadable_marker_refuses_belt_actuation`, `a_marker_that_is_listed_and_unreadable_is_not_absent` and the disagreement witness now catch a producer inversion they previously could not see, because they consume what the producer returns instead of what the author asserted. Also adds a direct witness over the producer's arms including the case a reader gets wrong: a failed read carrying LEFTOVER CONTENT is still refused. Content non-empty is not evidence the read succeeded, and that is the same conflation as inferring absence from an empty error string. WHAT THE DETECTION MISSES, since it should not be trusted further than it goes: it flags any imported lowercase name never followed by `(`, so `data` values import clean and show as false positives (two here). It finds uncalled PRODUCERS, not producers called on a path that cannot discriminate. It is a cheap first pass whose result must still be confirmed by mutating the producer and requiring a red. 31/31 deploy_transition witnesses (30 before); 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…no home; and one unconsumed predicate is deleted Reviews 57261 and 57264 both flag two Bool predicates over coproducts, citing a "predicate-dissolution rule". THAT RULE DOES NOT EXIST -- `predicate-dissolution` greps ZERO times in DESIGN.md, for the third and fourth citation of it on this PR. Neither finding is actioned as stated, and neither is dismissed: checking them found something real, and worse than what was reported. WHAT IS NOT THE DEFECT. Both predicates match EXHAUSTIVELY over their coproducts, so a new variant fails to compile at the match rather than silently joining an arm. That is the good shape, and it is what distinguishes these from `transition_phase_is_partial` earlier in this PR, which was consumed by an `if` and did lose exhaustiveness at the consumer. WHAT IS THE DEFECT, and only the first half was reported: both were UNCONSUMED production surfaces. `quiescence_admits` had no caller outside its witnesses, so it is DELETED and the Bool projection moves into the witness file, where a new `QuiescenceAdmission` arm now fails to compile in the file that asserts over it -- strictly stronger than the fold it replaces. `mask_survives_reboot` was worse than unconsumed, and the review did not reach this. `MaskPersistence` WAS NOT CARRIED BY `ExternalQuiescence` AT ALL -- it was a free-floating type with one Bool reader and no home. So the commit that introduced it stated that the mask mechanism is "OBSERVED PER UNIT on MaskPersistence" while NOTHING OBSERVED IT: a claim about where a fact lives, with no carrier holding the fact. That is the authority-substitution shape aimed at my own commit message, and it is exactly the failure the field was added to fix, reproduced one level up. So the fix is to make the claim true rather than to delete the predicate: `ExternalQuiescence` now carries `persistence`, `observe_unit_quiescence` requires it, and `quiescence_survives_reboot` reads it off the record. The arity wall caught two call sites my edit missed, which is the mechanism doing its job. AND IT DELIBERATELY DOES NOT GATE THE ADMISSION. "Nothing can start while I am gone" and "the inhibition survives a reboot" are different propositions; a transition that does not span a reboot is CORRECTLY admitted over a runtime mask. A witness makes both claims together, because either alone is satisfied by a wrong implementation: refusing a runtime mask would be over-strict, and reporting it as reboot-durable would restore the unmeasured claim this field replaced. ON THE LEASE BINDING, third repetition across 57096 / 57125 / 57261 / 57264: correct as a description of scope, declined by lane-owner ruling, and unchanged. Binding it means binding GitNativeConvergence, which this session does not own, and would land acquisition ahead of the principal check it depends on. The gap is declared in source rather than concealed. 26/26 bootstrap witnesses (25 before); 4243 files parse-clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Addressing reviews 57261 and 57264 (same two findings). Head is now Finding 2 — the cited rule does not exist, and checking it found something worse
What is not the defect: both predicates match exhaustively, so a new variant fails to compile at the match rather than silently joining an arm. That is the good shape, and it is what distinguishes them from What is the defect, and only half of it was reported: both were unconsumed production surfaces.
So that one is fixed by making the claim true rather than by deleting the predicate: Finding 1 — lease binding: declined, third repetitionSame item as 57096 finding 2, 57125, and now twice more. Correct as a description of scope; declined by lane-owner ruling and unchanged. Binding it means binding 26/26 bootstrap witnesses, 31/31 deploy_transition, 4243 files parse-clean. — sent from eager-heron-604 |
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm exercised one of them. The near miss that hid it: `[A,A]` answered
`[A,A]` DOES refuse correctly as repeated-observed, so the obvious fixture finds
nothing. Only the answered-once case slipped.
REPAIRED AT TWO LAYERS, and the receipt shows neither substitutes for the other:
- `ObservationRepeatedExpected`, checked FIRST. The other three arms are
statements ABOUT a question set and are meaningless without a well-formed one;
answering "missing" here names the OBSERVATION as the defect when the ROSTER
is, sending a consumer to fix the wrong artifact.
- `prove_repair_roster` refuses a duplicate outright, so a `ProvenRepairRoster`
cannot HOLD one -- construction at the mint rather than validation at the join.
The generic arm is NOT dead after the proof-side wall: the law is key-generic and
`legacy_binding_observation` derives its expected list with no proven roster, so
the arm is reachable from that consumer's denominator. A quiet guard, not a
decoration.
MUTATION RECEIPT, two independent mutations in sequence (not overlapped):
deleting the law's check reds 2 arms and leaves the proof arm TRUE; deleting the
proof's refusal reds only the proof arm. Unmutated, 24 arms green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Carry the repeated-expected arm into the two binding witnesses the new variant also made non-exhaustive
`ObservationRepeatedExpected` landed with arms added to the repair envelope and
its witness, and NOT to the two binding witnesses that match the same
key-generic law. Six matches, one arm each.
WHY IT REACHED CI: the local check was `v1_src_dag_parse`, which returned
`4210 file(s) parse-clean` and was read as evidence the tree was well-formed.
Exhaustiveness is a RESOLVE-time judgment, so a parse sweep can never see it --
parse-clean and resolves are different claims about different phases, and the
green one was not about the thing being changed. The verification is now a
resolve of each affected witness, which reproduces the six diagnostics when the
arms are absent and passes when they are present.
The variant refusing every exhaustive match across three files is the substrate
doing its job -- nothing could have silently kept the old vocabulary. What
failed was my check, not the wall.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
* scm: a typed read-command result that names no destination (#9443)
* scm: a typed read-command result that names no destination
Recut onto current main so the diff matches the scope this PR claims.
WHY THE RECUT. The previous composition reached main through the save
branch's ancestry, so it carried repository_save.dag and its witness --
neither of which is on main, and both of which belong to #9434, which is
draft. Merging this PR would therefore have landed the parked save half
as a consequence of branch topology rather than as a decision anyone
made. Nobody would have done anything wrong; the ancestry would simply
have outranked the park.
The park is respected rather than routed around. No convert_to_draft
event exists on #9434 and draft is not this tooling's default, so the
hold is unexplained rather than accidental -- and the correct response to
an unexplained hold is to leave it standing.
WHAT REMAINS, and why the load refinement is not scope creep: splitting
RepositoryLoadRefusal out of RepositoryLoad is what lets
ScmReadRepositoryUnavailable carry a refusal that CANNOT hold a success.
Without it this module's unavailable arm would be constructible holding
RepositoryLoaded, with nothing to refuse the pair. It is the enabling
half of this change, not a neighbour travelling with it.
The dependency runs one way, checked before cutting: the save witness
imports RepositoryLoadRefused, and nothing read-side references save. So
dropping save costs this PR nothing.
Both keystones return `true` on this tree over current main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Drop the refusal-path accessor: the third instance of a shape this PR
documents as twice-removed
`repository_load_refusal_path` had exactly one occurrence in the tree --
its own definition. No consumer, so DESIGN section 6 residue.
WHAT MAKES THIS WORSE THAN ORDINARY DEAD CODE: read_command.dag's own
header, in this same PR, cites this exact helper shape being removed
twice before -- once as `checkout_succeeded`, once from
`gunbc.scm.ancestry` under review 56207 -- and states the reason that
survives. This change re-added the third instance while documenting the
first two. Neither a lens nor a green run can see that; only reading the
two files against each other does.
The surviving rationale in the deleted comment block was about the TYPES
(why no `loaded: Bool` exists), not about the accessor, so it moves to
`type RepositoryLoad` rather than being deleted along with the function.
A prose row removed for one reason must not silently take its contents
with it.
It gains the reason the shape keeps recurring, which was written down
nowhere: with no consumer the accessor is residue, and WITH one it is
worse -- a fourth refusal arm would be absorbed by the projection instead
of failing to compile at each site that must decide about it.
Both keystones return `true` after the deletion.
Reported by review 57012.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Enroll the three read-command route gaps the floor actually reported
The floor reported route_gap_unenrolled=3 on this branch, all three in
scm_read_command_witness, all with one cause:
the hermetic route has no arm for Read (operation declares no
mock_response)
scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer
scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log
scm_read_command_keystone_holds
Same boundary already recorded for the load witness: extdeps.filesystem
declares no mock_response, so the hermetic frame has no arm for a FAILING
read. All three claims exercise the absent-repository path, and the
keystone inherits the gap by composing them. They pass under `gunbc run`,
which performs the real read; they cannot reach their subject hermetically.
MEASURED, NOT PREDICTED. These were foreseeable and were deliberately NOT
pre-enrolled: enrolling an identity that does not gap is a stale row and
reds the build, which is what stale_route_gap counts. The rows are added
now because a run reported these exact three identities.
Enrolment records the gap as known debt. It does not make the gap
acceptable and it is not a fix: the remedy is a hermetic arm for a failing
read, which belongs to the filesystem boundary and not to this PR.
Roster 112 -> 115; the module still evaluates and returns its list.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Anchor a relative source root the same way in both module-index builders (#9548)
* Anchor a relative source root the same way in both module-index builders
The two builders disagreed on how a relative source root resolves:
try_build_module_index anchored through anchor_source_root (process
workspace), while try_index_source_root_into_module_index read the string
straight off the filesystem (process CWD). One concept, two answers,
selected by which builder a caller happened to reach.
The fork survived because the one place it is observable is the one place
nothing was asserting: every CI invocation runs with its CWD at the
workspace root, where both spellings denote the same directory.
A root that cannot be anchored still falls through to the existence
refusal with its ORIGINAL spelling, so the diagnostic names what the
caller asked for rather than a rewritten form they never wrote.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Trigger a fresh merge ref against main after #9551
The merge ref is computed when the head is pushed, against main as it was
at that moment; main moving afterwards recomputes nothing, and a RERUN
replays the original pinned ref. #9551 landed the four emit mirrors after
this branch's last push, so its base predates the regen fix.
Empty rather than a local merge of main deliberately: main's change here IS
the generated mirrors, and merging it locally would mean hand-resolving
emitted files -- the one state the regen gate forbids. Pushing recomputes
the base without touching them.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Measure the fan decoder's execution identity, and refuse to call it bound (#9536)
* Instrument the decoder's execution identity by composing two things that already existed
gunbc.bmc_fan_program_interpretation modelled a decoder identity and refused to author
one, because both digests are properties of an execution and a hand-written pair would
be two literals typed by whoever typed the decoder -- agreeing because one person wrote
both, and continuing to agree after the thing they describe changed. This produces them
from an execution instead, which is what an operator adoption needs: a corrected decoder
that assigns different meaning to the same bytes must be distinguishable from a refactor
that assigns the same meaning.
NOTHING IS MINTED. Both halves were found by searching before building, which is why
this module is short:
v2.lens.module_graph import_closure_live enumerates the entry's closure
tools.multi_module_compile_fixture compile_fixture returns a structural digest over
the (path, content) vector AND the
running compiler binary's own hash,
both host-computed from what ran
ONE NEAR-MISS IS DELIBERATELY NOT REUSED, and it is recorded so nobody "fixes" this by
adopting it. std.interface_summary typed_module_key is exactly the right shape -- a
source key combined with compiler identity -- at the wrong grain: its module_key folds a
module's source hash with its DIRECT IMPORT INTERFACE hashes. A body-only change in a
transitively imported module leaves it unchanged while changing what this decoder
produces; std.decimal canonical_exact_decimal could be rewritten and the key would not
move. It answers "may I reuse a cached typecheck"; this answers "is this the same
reader". Borrowing the first to answer the second invents the entailment rather than
misstating any fact.
THE DISCRIMINATING PAIR IS MEASURED, both halves, because an identity that moves on
everything and one that moves on nothing both look fine from a single run. Baseline
3282f082abc9d722 over 40 modules; one comment line added to std/decimal.dag, inside the
closure, moved it to 9bcfbd782022b120; one comment line added to gunbc/fleet_fan_wiring.dag,
outside it, left it byte-identical to baseline. Both restored byte-exactly. The compiler
digest held across all three.
The second half is the one worth having: a digest over the whole tree passes the first
test and is useless, since every unrelated edit would invalidate an adoption.
WHAT IS NOT CLAIMED. There is no enrolled witness, and the reason is structural rather
than neglect: the instrument reads the live tree and takes about four and a half minutes,
so the floor planner declines it, and the mutation half would have to edit tracked
source, which no hermetic witness may do. The evidence is a recorded measurement with its
controls -- weaker than an executing one, and said so rather than dressed up. The
next-rung trigger is a fixture-grain closure the instrument owns, at which point the pair
becomes an ordinary witness.
Cost is recorded too, because it decides where this may run: the closure walk alone is
about 4m28s. On demand only; nothing here is enrolled in a required lane, and a
four-minute live-tree walk on every push would be the corpus-denominated cost that gets
paid by every consumer wanting something else.
* Report the identity as measured-but-unbound, because nothing here proves the decoder ran on this vector
The side-chat raised the objection that matters and it is right. This instrument
enumerates a closure, hashes that exact vector, and compiles it. It does NOT execute the
decoder against that vector -- a semantic program digest is produced by some other run,
through the interpreter's own resolution of the same entry. Pairing this identity with
that digest would be two individually correct observations with an invented arrow
between them: the same fake join removed from the capture observer on #9299, one level
up.
The two subjects are very probably identical, since the walk follows the same import
edges the interpreter resolves. "Very probably" is what the objection is about. Nothing
here proves the interpreter received this vector and no wider one.
So the standing is not handed out from here. DecoderIdentityEstablished is what lets a
consumer treat two readings as same-reader, and granting it from a run that did not
perform the reading would restore the unbound claim under a name that reads as bound.
The binding is now its own three-state carrier, the measured-but-unbound arm names its
own gap, and the standing derived from it is still the absent one.
That is the instrument reporting what it has rather than failing. The obligation is
NARROWED rather than discharged: what was missing was any producer at all; what is
missing now is one execution that both hashes its source vector and runs the decoder
against that exact vector, returning the identity and the semantic result together.
That trigger is recorded on the arm.
* Sharpen the binding trigger to name the missing host capability
Looked rather than assumed, and the gap is larger than 'finish the instrument'. Two
routes could bind the identity to a decode and neither is reachable today.
EXECUTE-THE-VECTOR: the seed registers exactly one fixture builtin,
compile_dag_multi_module_fixture, which COMPILES a supplied (path, content) vector. No
builtin evaluates one. So running the decoder against that exact vector needs a new host
surface -- v1 seed growth, which the freeze admits only in service of the v2 self-host
program, and this is not that.
PROVE-THE-SUBJECTS-EQUAL: nothing exposes the RUNNING program's resolved module set.
module_declaration_facts reads the source tree, which is the same authority the closure
walk already consumed, so comparing the two would compare a reading against itself rather
than against what the interpreter received.
Recorded at this grain because a trigger that reads as small invites someone to just
finish it, find the capability absent, and close the gap with an argument instead -- which
is the invented arrow this carrier exists to refuse.
* Consume the decoder declaration instead of re-minting it (review 57069)
A byte-identical DeclarationRef for the decoder stood in this instrument
beside gunbc.bmc_fan_program_interpretation fan_program_decoder, which is
the module declaring the standing the instrument exists to discharge --
and which this module already imported from, so consuming it costs one
import member. Two authorities for one fact can drift independently
(DESIGN section 3); worse here than in general, because a drift would
identify a reader other than the one whose standing is at stake.
The entry PATH stays authored and is not the same fork: a module path
does not carry which source root stores the module, and deriving one
needs an observed ModuleStorageIndex rather than a pure transform. The
annotation now says so, so the next reader does not read the surviving
path as a missed half of this repair.
Measured after: identity unchanged -- 40 modules,
source_closure=3282f082abc9d722, compiler_runtime=f2c179fb7e10d373,
the same values the pre-fix baseline reported.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Say that the typed_module_key grain claim is an argument, not a measurement
The note asserted as fact that a body-only change in a transitively
imported module leaves typed_module_key unchanged while changing what the
decoder produces. The reasoning is sound and has now been endorsed by two
reviews and one external adjudication -- which is exactly why it needed
correcting rather than leaving: convergent readings of one argument are
not independent evidence about that argument, and an approved PR carrying
an unmeasured claim stated as fact is the rung inflation DESIGN 4b(1)
names as worse than sitting low.
I tried to measure it and found the route blocked, so the note now carries
that instead of the assertion. The only live producer of import interface
hashes is v2.lens.interface_summary module_key_for_rel_path. It has zero
consumers in the corpus; the first attempt to run it refused with
export_signature_facts `empty authored type name` on
extdeps.shell.credentials env_credential -- a pattern returning an
anonymous record, one of three such declarations. So that lens's live path
is inert in the DESIGN section 6 sense: the machinery exists and the first
exercise of it does not work.
Authoring the two export lists by hand was rejected rather than
overlooked: the claim IS that a body edit leaves the exports equal, so
asserting that equality assumes what the control exists to establish.
Next-rung trigger recorded on the note. Identity re-measured unchanged
(40 modules, source_closure=3282f082abc9d722).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Delete three commentary String rows and the digests they transcribed (review 57083)
The review flagged typed_module_key_grain_note, decoder_identity_
discrimination_note and decoder_identity_cost_note as the section 4c
pattern DESIGN discourages -- pure prose duplicating the // blocks above
them -- and noted broad corpus precedent for it. Precedent is the reason
to fix it in new code rather than the reason to keep it: adding fresh
instances of a discouraged pattern because the corpus is full of them is
how a discouraged pattern becomes the convention.
DESIGN is stricter here than the remark was. Two of the three rows
transcribed digests and a wall time into prose, inside the very module
whose entry point re-derives them, which is the standing "name the
instrument, never transcribe its output" ruling and not merely commentary
debt. So the numbers are gone from the // blocks too. What survives is
the SHAPE of the controls, which does not rot: an edit INSIDE the closure
moves source_closure, an edit OUTSIDE it leaves it byte-identical, both
restore. Anyone wanting the figures runs report_decoder_identity, which
prints them with the module count.
The // blocks are kept where they carry irreducible rationale -- why
typed_module_key is the wrong grain, why no hermetic witness can hold this
pair -- which section 4c permits and which the String rows were only
restating.
Re-measured after: unchanged, 40 modules, same digests the instrument
prints.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Witness evidence integrity: an undeclared live_tree_disposition silently declines the module — make silence REFUSE, burn down the 338, then the staged DeclinedLiveTree root deletion is safe (#9471)
* The live-read derivation detects a quarter of the readers it would have to replace
`v2.std.live_tree`'s note named the nightly affected-set falsifier as the thing
that catches a row declaring `SubstrateInputsOnly` while reading live state.
That cadence was deleted by the floor cut (#8283) and the repository carries
three workflows, none of which runs a predict-only cold comparison. The same
note stated the undeclared fail-closed default as THE fact, while the required
floor's own scan defaults the identical silence the opposite way -- so a reader
asking what happens to a witness that declares nothing was told the half that
withholds it, and the consumer that actually executes admits it.
What survives as the backstop is `effect_reach_derived_reads_live_tree_for_entry`,
and it does not derive this fact. It answers host-reading only when two
INDEPENDENT existentials both hold somewhere in the import closure -- some file
carries a repository path literal, some file carries a host-sink call shape --
so a closure that performs a real `Filesystem.Read` and names no path answers
false, and two modules that never call each other supply the two halves between
them. The ceiling is filed as a §4b row on the derivation's own authority, with
its next-rung trigger naming the capability (call-reachability-grade per-witness
classification) rather than an artifact that would contribute to one.
The evidence is a planted pair rather than a corpus count: two fixture entries
differing by exactly one import edge whose only content is a path-literal row,
performing a byte-identical read. The positive control derives host-reading; the
sink-only entry does not. Authored both sides, so the red is a property of the
derivation and cannot be dissolved by corpus drift.
The consequence runs opposite to the standing objection that an authored
disposition duplicates a derivable fact. `reads_live_tree_effective` consults the
declaration FIRST and reaches the derivation only for a row already claiming
SubstrateInputsOnly, so the derivation is the sole thing between a lying row and
a predict-skip. Replacing the declaration with it would be a scope narrowing
wearing a construction argument.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* The derivation's third bound: an unreadable closure file is skipped toward ADMIT
Confirmed by reading effect_reach_derived_reads_live_tree_for_closure_paths: a
closure file that cannot be read hits a bare `continue`, leaving both flags as
they were. Every unreadable file therefore biases the accumulation toward false,
which biases toward admitting a row that claims SubstrateInputsOnly -- the one
arm that could notice its own blindness discards it, in the direction that
weakens the only thing standing behind a lying declaration.
It compounds the empty-adjacency bound rather than sitting beside it: where the
closure is the entry alone, one failed read leaves the loop having seen nothing.
And unlike the conjunction and the adjacency, which are properties of the corpus
and measurable today, this one is a property of the run, so its magnitude is
whatever the filesystem did that time and nothing records it.
Found by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Route the ceiling row onto the ladder vocabulary instead of a prose blob
Review 56493 observed that the §4b class row was a large `String`, which §4c
names as misplaced data, and reported that no typed §4b carrier existed to route
into. One does: `gunbc.guarantee_rung_drop` declares the closed `GuaranteeRung`
vocabulary, and `gunbc.hermetic_mock_fidelity` already files a discovered class
in exactly this shape -- typed rung and ceiling, closed-coproduct reasons, and
rationale left in annotations beside the row.
So the row follows that pattern rather than minting a class of its own. The three
bounds become a closed coproduct, because naming them is what lets the class be
recognised a second time; enforcement becomes two reachable arms rather than a
sentence; and the next-rung trigger is DERIVED by a total function over the
coproduct rather than stored, which makes a trigger-less row unwritable instead
of merely checked. That all three bounds derive the same trigger is the finding,
not a redundancy: the capability replaces the approach rather than patching a
term.
The record is named for its subject. No corpus-wide §4b carrier exists, and
minting one from a single instance would put a second authority beside
hermetic_mock_fidelity -- the ladder VOCABULARY is the part that must not fork,
and that is what is reused.
Verified by execution: `gunbc compile --entry src/v2/std/effect_reach.dag`
returns 0 blocking errors, 21 files emitted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record that stamping the silent population was built and dropped
A future reader who finds the fail-closed default and the 24.7% backstop
measurement will reach for the obvious move -- stamp every silent witness file
-- and there is nothing in the tree telling them it was already tried. It was:
520 files stamped, silence made a typed located refusal on both consumers, then
discarded because the floor's decline arm was already being deleted at its root,
which is what made a truthful ReadsLiveTree stamp cost coverage in the first
place.
The note records the reason rather than the fact, because the reason is what
transfers: the arm's deletion is the enabling event for a truthful stamp, not
its reward, and the question revives when the selection consumer acquires an
enforcement it currently lacks -- not when the silent population grows.
Suggested by swift-badger-524, who observed the work would otherwise be visible
only in a reflog and one message.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Sweep the dead-cadence enforcement claim from all three of its homes
One claim lived in three places: v2.std.live_tree's disposition note, the same
module's stamp_provenance row, and a mirrored comment above
parse_entry_live_tree_disposition in cli_run.rs. Each said the nightly
affected-set falsifier catches a row declaring SubstrateInputsOnly while reading
live state. falsifier.yml was deleted by the 2026-08-15 floor cut. Correcting one
home leaves the other two as authorities for a false claim, so all three move
together.
The stamp_provenance row gets more than a past tense, because its consequence is
specific: the 2026-07-11 batch is machine-vouched rather than author-vouched and
inherits the deleted classifier's blind spot -- a live read hidden behind an
import was invisible to entry-text scanning. Those stamps were admitted on the
promise that a cadence would catch them if wrong. That promise is now UNMET, not
merely unfulfilled: nothing verifies a stamp, and one that was wrong the day it
was written is still wrong and still unobserved.
Three other authorities carry the same claim and belong to other owners; they are
deliberately not in this diff.
Verified: gunbc compile --entry src/v2/std/live_tree.dag -> 6 files emitted,
0 diagnostics.
Sites located by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Turn the supply fold from an honest screen into a real cross-mode selector: the six inputs supply.dag names as missing (#9472)
* wip: cross-mode supply selector
* wip2
* wip3
* wip4: duration state, commitment horizon
* review: fail-closed unbounded-duration availability, quote billing basis projection, Second-typed axis params
* witness: choose the window that the previous fold actually admitted
* Answer the new affordability arm in the sibling fabric witness suite
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids (#9564)
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids
Review 46148 ruled that absence is established by a successful listing and never
by a failed read. The ruling was written as a `data ... : String` note, which
DESIGN section 4c calls commentary no `Accepted` program can read -- and it was
then violated in gunbc.deploy_transition, authored beside the note, where a
present-and-unreadable marker rendered as absent and so as PERMITTED at the belt
seam (#9561). A note is not a mechanism.
extdeps.filesystem.filesystem_io gains a carrier with one mint.
FilesystemEstablishedAbsence is sole_constructor; its only mint takes a
FilesystemDirectoryListing, itself sole_constructor and minted only from a
listing whose success channel was true. A module deciding absence from a read
alone has no value to return and no way to build one. filesystem_entry_presence
and filesystem_file_observation are the folds: presence is decided by the
listing, the read is consulted only for an entry the listing named, and every
way of not establishing absence lands in one indeterminate arm.
Consumers, so this is not a carrier with no consumer:
- gunbc.roadmap_verification_receipt, both walks. Already correct by hand; they
now consume the carrier instead of restating the rule, and their private
second spelling of List's wire encoding is deleted for
filesystem_listing_names_entry.
- gunbc.devboot.build read_text_file,…
…elt, drop my superseded helper Wind-down merge to current main (deb0db8). One conflict, in `dag/gunbc/roadmap_belt_actuate.dag`, and main's side wins outright rather than being reconciled. WHAT COLLIDED. This branch had added `belt_listing_names_entry` delegating to `filesystem_listing_names_entry`, plus two prose notes restating the absence law. Main has since adopted the filesystem authority directly in that module -- `filesystem_entry_presence` and `filesystem_file_observation` decide listing and receipt, `ReceiptSourceAbsent` projects only from `FilesystemEstablishedAbsence` -- and deleted both the prose copies and the second spelling of List's membership encoding. That is strictly further along the same road this branch was on, so the resolution is main's block wholesale. Nothing referenced the deleted helper. Its import was then dead and is removed, which is the class this PR spent the afternoon on: an imported name with no call site. WHAT IS INHERITED AND NOT MINE, stated here so a reader of the next red does not re-derive it. The `.dag` parse sweep now reports CITATION-DEBT-ROW-STALE and CITED-MODULE-ABSENT rows naming `test.claim.annotation_carrier`, `test.fixture.frontier` and `extdeps.network.mac`. All three subjects -- and `declaration_index.rs`, which carries the debt rosters -- are BYTE-IDENTICAL to origin/main in this tree, verified per file rather than assumed from "I did not touch it". So the condition is main's as it stands, inherited by taking main, and under the wind-down directive it is not this branch's to repair. Rebuilt the sweep binary first and re-measured, because a roster compiled into a stale binary reproduces exactly this signature for a different reason. 31/26/6 witnesses green after the merge. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The finding that is independent of this PR: the revision gate is satisfied by the artifact of the failure it exists to notice
gunbc.live_deploy.repository_convergencerepository_converge_wetimports objects, thencompare-and-swaps the base ref, then transitions the worktree.
git update-refgives CAS over theref it owns and nothing more — it does not span the later reset. So a converge that dies between the
swap and the reset leaves
refs/remotes/origin/mainADVANCED over a tree that never moved. Themodule reports that as
ConvergencePartialTransitionLeft.fleet_revision_standingreads that ref. So on exactly that host, in exactly that state,belt_revision_admissionanswersBeltRevisionAdmitted— the gate that exists to keep the belt offan unadmitted tree returns CONVERGED for the half-transitioned one, and
git worktree addthenresolves through the advanced ref. This is a defect in the existing gate. It does not depend on
anything in this PR, and it is not fixed by anything in this PR. It is the reason the transition
gate must DOMINATE the revision gate rather than sit beside it: asking the marker second would mean
asking it after the revision gate had already said yes.
That ordering is what the diff implements, at all three ingresses (timer tick, click path, HTTP
publish), and the reason is written beside the fold.
The change
A repository convergence is a multi-step mutation on a live host and there is no ordering of its
steps under which every intermediate state is safe for another actuator to observe. Two mechanisms,
because they answer different questions.
The host-local lease is mutual exclusion between actuators, scoped to a process's critical
section —
Filesystem.WriteOwnerOnlyis realized withcreate_new/O_EXCL, so acquisition is oneatomic kernel operation and two racing acquirers cannot both win. It sits below every mutating
ingress, including the out-of-band
gunbc.apply DashboardSrv1that a GitHub concurrency group cannotsee. Four arms, because they are four different facts with different remedies: acquired, held by a
named holder, held by something undecodable, and the directory itself refusing.
The durable inhibition is a statement about the REPOSITORY and outlives every process that
touches it, because a process that dies between the swap and the readback is precisely the case the
belt must keep refusing through. A partial transition REWRITES the phase in place and leaves the
marker set. Its create is exclusive too, so a residue left by a dead converge cannot be overwritten —
that residue is the only durable evidence the partial transition happened.
Absence is established by a successful listing, never by a failed read.
Filesystem.Readanswerssuccess=falseboth for a path that does not exist and one that cannot be read, and those two worldshave opposite correct actions. Presence is decided by
Filesystem.List, so absent is a positiveobservation and every way of not establishing it lands in one indeterminate arm. Acquisition may
treat that as free because O_EXCL still decides there; admission may not, because the read is its
whole decision. (The first push got this wrong in exactly the way its own module header said it
should not — see the second commit.)
Clearing is subject-matched. Every basis names the record it was computed against, and the record
still on disk is re-read inside the same fold as the delete. Without it, a late-finishing older
deployment clears the marker a newer one has since set, and the newer transition runs unprotected.
Staleness is resolved by evidence, never by a clock. There is no timeout arm and no age field
anywhere in the record — a lease that expires is one a slow transition loses while it is still
mutating. A residue is resolvable when the repository is observed AT the candidate its record names.
A record whose own phase says partial refuses even at a matching head, because the phase is a
first-hand report from the process that was there.
The first transition is protected by no marker, and that is not a gap in the marker. The binary
running on srv1 predates every mechanism here, and no file inhibits a program that never looks for
it.
gunbc.deploy_transition_bootstrapmodels bootstrap external quiescence (disable --now, notstop, over belt timer + belt service + serve unit), steady-state in-process inhibition, and thewalled switch between them — restoration is admitted only over an INSTALLED release observed to
consult the marker, and an unobserved awareness refuses rather than defaulting to the stronger
regime. The order is a modeled successor relation, so a skipped or reversed step is a typed refusal
naming both steps.
The sequence is PRINCIPAL → LEASE → OPERANDS → MUTATION, and the first arrow is the one an
earlier revision of this vocabulary got wrong: it began at the lease, which reads as harmless and is
not. Acquisition is itself a privileged write, so a unit that acquires before establishing which
principal it runs as creates the lease as mode 0600 owned by whoever happened to be executing —
precisely the unreadable-marker state the second commit removed, manufactured by the guard itself.
The guard must not produce the hazard it detects. After
principal-admittednothing has been writtenat all, no lease and no marker, so a crash there leaves the host exactly as it was.
One deliberate departure from precedent, ruled on by the dispatching lane: a transition refusal
withholds publication and verification as well as spawn and reap. The revision gate's ruling blocks
spawn/teardown only, on the grounds that verification and publication read independently bound
receipts. That argument does not survive here — those receipts live in the tree being rewritten, and
publication is the pass that leaves the house.
Evidence
45 witnesses across the two new modules, all green. 96/103 on the existing belt suite (the 7 exec
failures are the pre-existing hermetic route gap — verified identical on
HEADby swapping theoriginals back in, not assumed). 16/16 serve.
The construction wall is executed rather than asserted: a
TransitionGuardrecord literal in thewitness module is refused with
sole_constructor type 'TransitionGuard' cannot be constructed outside its defining module, and the passing witnesses obtain one only through the acquisition fold.What is not claimed
GitNativeConvergenceflip, are one change held by the dispatching lane. Thefleet_workflow_stepsnote is updated to say the wall EXISTS AND IS NOT ACQUIRED, rather thanreading as closed.
ReleaseMarkerAwarenesshas no observer. Until one exists the regime fold refuses, which iscorrect and deliberately not defaulted.
.dagpath and NOT on theemitted-Rust path, per the open DESIGN §4b item. The residual belt/converge window — a tick that
read the standing as permitted immediately before a converge set the marker — is mitigatable,
next-rung trigger the shared execution lease. Operator abandonment is mitigatable because nothing
observes whether the recorded holder is still alive; next-rung trigger is holder liveness.