Repository navigation
Self-host promotion integrator: prove modules replaceable end-to-end — CI today runs NO regen, NO fixed-point, NO behavioral receipt - #8657
Conversation
…s its authority
`--required-regen` asks whether the committed stage0 mirrors EQUAL what their
`.dag` authority emits. On main that question has no closing move: the regen cut
deleted the writer, so the only green a contributor can reach is to hand-edit a
generated mirror -- the exact act a drift gate exists to refuse. A required gate
whose only path to green is the violation it guards against does not enforce the
rule, it manufactures the workaround under a green check.
`--required-mirror-drift` asks a question a contributor can close. Per drifted
path, against the git merge base:
drifted AND this change touched the mirror -> sideways mirror move (refuse)
drifted AND this change did not touch it -> must carry an authored
disposition, else refuse
drifted on neither count -> silent
Plus the join run backwards: a disposition row whose path does NOT drift is
stale and refuses, because otherwise the carrier is a one-way ledger that
accretes rows asserting debt that no longer exists.
Membership is DERIVED from the required-regen comparator every run; the only
authored input is the per-row disposition in `gunbc.stage0_mirror_debt`. So a
row cannot add to or remove from the measured population -- forgetting a
judgement refuses loudly, and no edit to the carrier can silence a real drift.
The baseline is resolved from git, printed, and asserted: there is no fallback
to HEAD, under which the touched set would be empty and every hand-edited mirror
would reclassify as pre-existing debt.
The stale arm alone carries a derived precondition. It is the only arm whose
false verdict DESTROYS something -- the other two fail toward refusing, this one
fails toward deleting a correct row, and it did exactly that on its first live
run against `v1_compiler_parse.rs` on a subject fifteen commits behind the
commit that created that drift. When the subject does not contain main's tip,
stale rows are counted and named under `stale_rows_unreadable` and do not
refuse; nothing is silenced, so the deficit stays rankable.
This gate writes no receipt. Every fact it reports is computed in the invocation
that reports it, from the tree that invocation is looking at.
…e the measurement Review finding (smart-ram-730 on #8639): `measure_generated_drift` re-typed the same five-call sequence `run_required_regen` already performs -- compile_stage0 committed_generated_basenames generated_basenames_from_emit validate_compared_populations compare_generated_surfaces -- so one fact, WHICH MIRRORS DRIFTED, had two producers and nothing kept them in step. The receipt is on the record and is why this is worth fixing while the copies still agree: #8618 repaired a defect INSIDE `compare_generated_surfaces` -- the committed side was being normalized, making the comparison `normalize(normalize(x))` against `normalize(x)`, a false-positive drift with no reachable green. A repair landing in one of two copies leaves the other answering the old way, and "the copies agree today" is exactly what makes a duplication easy to leave in place until it costs something. What actually differs between the two callers is the FAILURE POLICY, not the measurement: `run_required_regen` routes a refusal to `regen_refusal_outcome`, which writes a receipt and returns `Ok` carrying failures, while the drift gate wants `Err`. So `measure_generated_surface` performs the sequence once and returns `Measured { .. }` or `Refused { reason }`, and each caller applies its own policy at the call site -- one `match`, not a second copy of the five calls above it. `emitted` and `committed` come back in the value because the regen path needs them for the candidate tree and its digests, and recomputing them would run the whole emit a second time. `emitted_basenames` is returned too, rather than derived again by the caller for its `executed=` count. Leaving that one out would have fixed the duplication at the top and reintroduced a smaller one a level down. NOT DONE HERE, deliberately: `run_required_regen_fixed_point` shares four of these five calls and is a partial third copy. It is left alone for two reasons. It skips `compare_generated_surfaces` because it only needs a digest, so routing it through this function would add a rustfmt-per-file comparison it does not need; and #8650 is restructuring that exact function, so editing it here trades a real duplication for a merge resolution in a generated-adjacent file. Raised with that PR's author instead of taken silently.
…orpus fragment CI proves the committed mirrors equal what the authority emits, and that the emit repeats. It never COMPILES the emitted candidate, let alone runs it -- the regen host spawns exactly rustfmt, rustfmt and git. So the whole promotion story rests on bytes, and DESIGN §7 says a byte-identical fixed point is explicitly NOT the goal. This lands the selection and corpus-derivation half of an executing behavioral receipt. SELECTION is demand-directed and derived. The subject is the modules whose .dag authority moved in this diff; the authority-to-mirror mapping is read off each mirror's own `// Source module:` header, never an authored roster. If the merge base will not resolve it REFUSES rather than widening to the whole population: two compiler builds across 129 modules is a budget denominated in the repository rather than in the change. THE CORPUS is derived from the authority's declared surface and REFUSES where it cannot be. Closed nullary enums, Bool and records over them are finite-closed; Int windows and bounded-length Lists are not. A sampled corpus for the remainder would let the mode report a receipt for every module while a behaviour change hides in an unsampled cell -- a receipt that usually cannot fail, which is worse than a refusal, because a refusal is counted and ranks while a usually-passing receipt reports as done. THE DOMAIN IS REPORTED AS A DERIVED FACT, not a label: cardinality always, and for bounded cases the bound itself. `Exhaustive` is reserved for the finite- closed case. This is not pedantry -- an earlier revision of this work described a corpus as exhaustive when four of its seven function groups were bounded approximations of infinite domains, and printing the bound is what exposed that `content_hash_is_lower_hex_code_point` was being enumerated over [-2,2], a window containing no hex digit at all. TYPES RESOLVE THROUGH THE IMPORT GRAPH, because a type's shape decides derivability and its address does not. Measured control that this resolved rather than widened: std.content_hash refuses 26 of 27 functions before and after, while std.pareto moves by exactly one -- axis_comparison, whose only blocker was that `Ordering` is declared in std.algebra. Not yet built: the two-build differential itself. What is here is the subject selection and the corpus plan, both green by execution with discriminating arms (empty selection stays empty; a String-heavy authority refuses; an authority with no emitted mirror is excluded by name, not silently).
…roducts by name Three compile fixes, two of which are the same mistake at different scales. PayloadCoproduct was declared and constructed but had no arm in derive_parameter_domain. Without it a declared, CLOSED, payload-carrying coproduct refuses with 'not a closed type declared by this authority' -- false for that population, and the exact misdirection this branch exists to remove, reintroduced in a narrower form. The source-index map is an im::HashMap, not a std::HashMap. Building it with v1_rt::rc_empty_map / rc_map_insert, as the emitted caller does, rather than naming the concrete type here: reaching for the representation is this file asserting something the parser owns, which is the same defect as re-implementing its reader, one level down.
9522520 to
322fa98
Compare
…arse tree
The grammar-backed reader landed with four wrong assumptions about node shape. Each was
found by measurement, not reasoning, and the last three shared ONE root cause.
WRONG: a function is a `Connective::Arrow` child.
RIGHT: Arrow marks a `Callable` TYPE EXPRESSION. A declaration is a function when it carries a
body AND a resolved return type. Selecting on Arrow matched nothing and every module reported
parsed=0.
WRONG: a parameter's, field's, or generic argument's type hangs off `type_annotation`.
RIGHT: it is a CHILD. This single mistake produced three unrelated-looking symptoms: every
parameter typed as the empty string, so all 514 corpus refusals named the same empty type and the
blocker histogram collapsed to one meaningless row; `List<AxisComparison>` rendered as bare
`List`, which then failed the `List<` test and fell through to "not a closed type declared by this
authority", which is why the first histogram had NO list row despite lists being the second
largest blocker; and every record dropped out of the type environment, so `DominanceTally` -- a
Conj record sitting in the same module -- was also refused as "not a closed type". Three wrong
refusal messages, each sending a reader to a repair that was not needed. That is the misdirection
this fragment exists to remove, produced by the fragment itself.
WRONG: a body distinguishes a function from a `data` row.
RIGHT: both carry bodies. `data no_names: List<NonEmptyStr> = []` reports ta=Some inf=none; every
function reports ta=None inf=Resolved. A constant's declared type lives in `type_annotation`, a
function's return type in `inferred`.
MEASURED RESULT, all three criteria fixed before the run:
std.pareto fn_lines=33 parsed=33 axis_comparison exhaustive(|domain|=6)
std.content_hash fn_lines=27 parsed=27 refused 26 of 27 -- control held exactly
corpus declared=585 parsed=585 -- zero disagreements across 44 modules
The declared-versus-parsed counter is kept, not retired. It has now caught three defects: the line
reader's 14 missing signatures, the Arrow mistake, and the data over-count -- in both directions.
Two readers of one fact are duplication when both are trusted and a cheap falsifier when one is
under test.
The partition arm also stopped being nearly empty, and the new hit is the one that indicts the
deleted bounded window most directly:
content_hash_is_lower_hex_code_point literals {48,57,97,102} reps {47,48,49,56,57,58,96,97,98,101,102,103}
Those are '0','9','a','f' and their boundaries. The window this replaced enumerated that same
function over [-2,2] -- five values containing no hex digit at all -- and reported it beside
genuine coverage.
…ived corpus, compare CI proves the committed mirrors equal what the authority emits and that the emit repeats. It never COMPILES the candidate, let alone runs it. This does both. Seed transcript from the tree as committed; the emitted candidate is then written over its mirror, the crate rebuilt, and the SAME driver run again. One function produces both transcripts, so they cannot differ because of how they were produced. The mirror is restored BEFORE the result is interpreted -- no early return can leave a candidate installed, which would silently corrupt every later measurement including the drift gate's. Refused is a third verdict, not a soft pass. A missing candidate, a driver that will not compile, an empty corpus: each is ignorance, and an empty comparison is indistinguishable from a passing one unless it has its own arm. The corpus enumeration now yields VALUES, not a cardinality. The count is values.len(). A count computed beside an enumeration is a second producer of one fact, and it is exactly how the earlier revision could report a corpus it had never executed. The superseded derive_parameter_domain is DELETED rather than left callable -- keeping the count-only route beside the executing one preserves the reporting path this change exists to remove. Candidate bytes come from emitted_generated_sources, which routes through the same measure_generated_surface the drift gate and regen use, so the bytes a receipt compiles are the bytes the gate compared. 4096 tuples per function is a refusal, not a sample: a receipt that runs a subset while reporting the whole is fabricated output, and an unbounded Cartesian product is the cheapest way to get one.
… arms discriminate
The driver aliased the module for CALLS while the enumerated constructor VALUES were rendered
against the bare module name -- one module referred to two ways, and only one spelling resolved.
Fully qualified from a single string derived from the artifact's own basename; the alias is gone,
so calls and constructors cannot drift apart.
MEASURED, both arms, digest-guarded, emitted bytes moved in each:
ARM 1 behaviour-preserving (compare_int rewritten to test > first)
std.pareto EQUIVALENT over 22 derived calls
ARM 2 behaviour-changing (LowerIsBetter/Greater => Same instead of Worse)
std.pareto DIVERGENT over 22 derived calls
seed: axis_comparison(AxisGoal::LowerIsBetter, Ordering::Greater) = Worse
candidate: axis_comparison(AxisGoal::LowerIsBetter, Ordering::Greater) = Same
The corpus is DERIVED from the authority's declared surface, not authored. The divergence names
the exact call rather than a count, and it is the call predicted in advance from the seed
transcript.
This is what CI does not do. required-regen spawns rustfmt, rustfmt and git; it never compiles
the candidate, let alone runs it. So promotion evidence today is byte-equality, and a byte
comparison cannot tell a rename from a semantic change -- which is why DESIGN section 7 says a
byte-identical fixed point is explicitly NOT the goal and names behavioural equivalence on a
discriminating corpus instead.
WHAT THIS DOES NOT CLAIM: equivalence over the TYPE. It is equivalence over the derived corpus --
5 of std.pareto's 33 functions, 22 calls -- where each domain is exhaustive in the sense its arm
states: a closed finite domain, or a partition within which the function provably cannot
distinguish values. The other 28 refuse, each naming the type that defeated it, and they are
counted rather than sampled.
Three earlier runs REFUSED rather than reporting equivalence: a candidate looked up in the wrong
key space, then a driver that would not compile, twice. A differential that answered EQUIVALENT
in any of those states would have passed both arms while comparing nothing.
…ed not hand-added
…unlock The differential answers ONE candidate. This answers the prior question -- across every module the seed actually carries, how much of each surface can be covered at all, and what stands in the way of the rest. Ranked by the TYPE responsible rather than by refusal count, because the type is the unit of work: grounding one type unlocks every function whose only obstacle was that type, and counting refusals would rank the same fix once per site. Runs no build and installs no candidate. It exits SUCCESS on any population deliberately -- a census that refused would be a gate, and nothing here establishes what the right coverage is. The population is derived from the mirrors' own `// Source module:` headers, and a module whose authority source cannot be read is REPORTED rather than skipped: a census that silently drops what it cannot read reports a smaller corpus as a cleaner one.
…ping fact wearing a refusal's clothes
The census ranked on the formatted refusal message, and the top row came back
1500 x (used outside a literal comparison, so its value reaches the result ...)
which is every parameter in the corpus that happens to be named `x`, collapsed into one row that
names no type and no work. A parameter name is not a unit of work. The string was doing double
duty as an identity and as prose, and it was wrong at the identity job -- the ranking that is
supposed to decide what to ground next was ranking spellings.
RefusalCause is now typed, and `describe()` is DERIVED from it, so the sentence and the ranking
key cannot disagree. Two consequences fall out of the carrier rather than being coded twice:
- the Int class keys WITHOUT the parameter name (the name stays in the message, for locating
it), so one class is one row instead of as many rows as there are spellings;
- a refusal reached through a record field ranks as its INNER cause, because grounding the
inner type unlocks every record that embeds it -- counting the wrapper separately would split
one piece of work across as many rows as there are embedders.
…han a count Review nit, real: a rustfmt-mangled continuation left `the generated surface is<18 spaces>no longer flat` in the basename-collision refusal. Rewrapped. The census's out-of-scope arm now leads with COVERAGE planned/total and names the roots it was given. A count read alone looks like a rounding error; the same shape at a wrong root set is a hole centred on whatever nobody scanned, and this exact arm has already BEEN that hole once -- it swallowed 55 of 127 modules as "no authority" when the truth was that src/v1 is not a scanned root. If the fraction is large, the root set is the finding, not the corpus.
…fixtures/
MEASURED, and it is the answer to why the corpus probe's arms both exited 1 with no verdict:
behavioral-receipt: refused: surface population mismatch —
emitted_not_committed=["receipt_fixture.rs"] committed_not_emitted=[]
Not a merge-base problem at all. `regen_source_roots()` seeds EVERY .dag under src/v1 into the
stage0 compile closure, so putting the fixture authority there made it a compiled, emitted module
with no committed mirror -- and the generated surface stopped matching its committed population.
The refusal is CORRECT and I am not weakening it. A .dag under src/v1 means "compile me", and
this authority must never be emitted: the entire value of a controlled fixture is that its input
and its expected outcome are independently authored, and an emitted fixture shares a producer
with the thing it is testing.
So the fixture moves to fixtures/receipt_fixture -- where, as it turns out, four sibling fixtures
already live. The placement was wrong twice: inside a root that means compile-me, and outside the
directory the repository already uses for exactly this.
WHAT THIS WOULD HAVE COST: the same refusal fires on `--required-regen`, which is a witnesses.yml
step, so this PR would have failed CI on a path unrelated to anything it claims. It surfaced only
because the arms harness stopped fabricating a baseline and started printing its output whole --
two fixes that were about something else entirely.
…the type was not found
The arm's text parses as "declared, but not closed". The branch is taken only when the type is
absent from the type environment entirely. Those are different facts, and the difference decides
whether anyone can act.
It cost a wrong conclusion immediately. Node topped the corpus ranking at 798 under that label
and I read it as the one big groundable item in the census -- the thing to ground before stopping.
It is nothing of the sort: v1.std.core Node is a 20-field record carrying an unbounded String, a
recursive List<Node>, and self-reference. Infinite three independent ways. No grounding reaches it.
So the arm splits, and the split is decided against the corpus rather than against the module:
TypeNotVisibleHere — some module declares it; this module's reader could not see it.
An import-closure gap in the reader, and real work someone can do.
TypeNotDeclaredAnywhere — no module declares it. Outside what the authority carries.
`declared_type_names` derives the corpus-wide set once, so the discriminator is a measurement
rather than a guess about why a lookup missed.
This is the fourth refusal in this lane to name the wrong cause, and the second inside the tool
whose entire purpose is to stop that -- after `x` at 1500 and the 55 modules reported as having
no authority. The pattern is stable enough to state: when a refusal is written, the message gets
the author's intent while the branch gets the code's condition, and nobody re-reads the branch.
…g key The two new arms both keyed on the bare type name, so the ranked list printed EXACTLY what it printed before the correction -- Node 798, unchanged -- and a reader would have concluded the split found nothing. A distinction that does not reach the report is not a distinction. `declared_anywhere` is corpus-global, so a given type falls entirely into one bucket and the tag is stable per type rather than a source of fragmentation.
…oss-checked
Node ranked 798 as "undeclared anywhere in corpus" while src/v1/00_core.dag declares
`type Node {` in plain sight, and nothing in the output said the reader had skipped it. The
function reader has carried an authored-lines-versus-parsed-count cross-check since the line
reader was replaced -- precisely because two readers of one fact make a miss visible -- and the
type reader had none.
It does now: type_lines versus types_read, per module and in total, with the modules whose counts
disagree named. A gap means every refusal citing those types is measuring THIS READER rather than
the corpus, which is the difference between a census and a fiction.
…unt says a form was missed, the names say which
… of a census is the same defect one level up
…h onto its subject SHAPE, measured: DominanceTally is connective=Conj with children=2, ParetoEntry with children=4 -- the declaration parses correctly and the field COUNT is right. But the field node's own children are empty, so `f.children.iter().next()` is None, filter_map drops every field, and the `fields.is_empty()` guard drops the record. My earlier repair moved the defect rather than removing it. A parameter's type IS its child -- verified, and still true. A record FIELD's type is somewhere else, and reading it as a child was the mirror image of reading it through type_annotation. So the probe now prints the field's name, child count, connective, type_annotation and inferred, instead of my guessing a fourth time. Review 54078: the "Every arm here REFUSES" paragraph was documenting measure_generated_drift's refusal policy while sitting immediately above emitted_generated_sources, so rustdoc attached it to the wrong function and the drift gate lost its policy doc. Moved onto its subject rather than separated by a blank line -- a blank line would leave the paragraph orphaned between two functions it does not describe.
|
Addressing review 54089's blocking finding — it was right, and it is fixed rather than argued. The plan mode is now enrolled, as a It runs per-PR, gated on a non-empty selection. Per-PR rather than on a cadence for an attribution reason rather than a cost one: a behavioural divergence discovered on a cadence lands on a window of many commits, and recovering which commit caused it costs far more than the minutes the cadence saved. Not on-demand either — a mode nobody runs is the inert tier this finding is about. Two conditions ride with the enrollment:
One thing I want stated rather than left for someone to discover: on this PR that step selects zero modules, because the On the other two modes ( On Also fixed from earlier reviews: the rustdoc paragraph that bound to the wrong function (review 54078), and the rustfmt-mangled refusal string (review 54069). — sent from smart-newt-495 |
|
Correcting one claim I made in the comment above, because it overstated the gap in my own PR's disfavour and someone reading it would price the remaining risk wrongly. I wrote that "the selection path is exercised in CI, the differential path is not." That is inaccurate. The differential path is exercised in CI — by the enrolled selftest, on the controlled fixture, with both arms discriminating. That is precisely what the fixture exists for. What is enrolled-but-untested is narrower: the composition — plan-mode selection feeding the differential against a real mirrored authority. My original sentence implies the differential itself is unproven in CI, which would be a substantially larger gap than the one that actually exists. The trigger is unchanged: the first PR that selects a non-zero module is the enrollment's real evidence, and its transcript should be reported rather than passing quietly into the log. — sent from smart-newt-495 |
…ore measuring Review 54094 names the real hazard: the differential installs a candidate over the committed mirror and restores it on every path, but a process killed between those two leaves the candidate in the tree. The next run would then read that candidate AS the committed bytes and compare it against itself -- answering EQUIVALENT, which is the worst available wrong answer: a green that means nothing, produced by the one mechanism whose whole value is being trusted. The residue cannot be prevented; no arrangement of writes survives SIGKILL. So it is made loud instead. A dirty mirror path is a typed refusal naming the recovery command, not a warning and not a silent read. This is the same move as everywhere else in this branch: where a bad state cannot be made unwritable, it must at least be undetectable-to-nobody. CI re-clones and would not have hit it; a developer running the mode locally after an interrupted run would have, and would have been handed a green.
…rrier that does not exist Review 54096 found it and the finding is stronger than "unenrolled". `--required-mirror-drift` had no invocation anywhere, and it reads `dag/gunbc/stage0_mirror_debt.dag`, which is not in the tree on this branch or on main. So it is not a gate awaiting enrollment; it is a gate that cannot run. DESIGN §6 names exactly this -- a mechanism whose whole purpose is enforcement, landed with no execution site, is coverage by illusion, and an inert lens is itself a lie. Deleted rather than enrolled, for a reason beyond the missing carrier: the open question about this gate is what it answers that the regen step does not, and wiring it before that is answered would create the fork rather than find it. Two mechanisms answering one question is the shape this repository keeps having to undo. WHAT IS KEPT, because the gate's genuinely useful half was never gate-specific: the single-producer refactor of `required_regen_host` stands -- `measure_generated_surface` is still the one producer of the emit-and-compare fact, and `emitted_generated_sources` still routes through it, which is what stops the receipt from re-emitting its own candidate. `git_stdout` is kept as a shared helper, documented as such, because the receipt resolves its baseline with it. WHAT THIS ALSO FIXES, and it is why the diff is this large: `receipt-mode` was branched from gunbc#8639's head, so #8657 CONTAINED that PR in full. The drift gate was #8639's subject, not this one's, and two open pull requests carrying one body of code is the same single-authority problem at the branch level. Also from review 54096: the per-run module cap now states what kind of number it is. It is a POLICY BUDGET -- one of DESIGN §5's four sanctioned grounds for a literal in a merge-blocking check -- and the resource is CI wall clock, since each selected module costs a full v1-compiler release build. It carries its dissolution condition: the cap is raised when the differential stops rebuilding the whole crate per candidate, not before.
|
Both findings from review 54096 addressed with commits, not argument. 1 — The mirror-drift gate is DELETED, and the finding was stronger than "unenrolled." I deleted rather than enrolled it, for a reason beyond the missing carrier: the open question about that gate is what it answers that the regen step does not, and wiring it before that is answered would create the fork rather than find it. Kept, because the gate's genuinely useful half was never gate-specific: the single-producer refactor stands — This also surfaced something the review could not have seen from the diff alone: 2 — The cap now states what kind of number it is. You were right that a bare literal in a merge-blocking check is what DESIGN §5 tells reviewers to distrust. It is a policy budget — one of the four sanctioned grounds — and the resource is CI wall clock, since each selected module costs a full It also carries its dissolution condition now: the cap exists only because the differential rebuilds the whole crate per candidate, and it is raised when that stops being true — not removed. Until then a four-authority PR is genuinely more than this gate can check, and saying so is the honest answer rather than checking three of four and printing a pass. On — sent from smart-newt-495 |
…lection Review 54102 found the vacuous arm: this job also triggers on push to main, and there `git merge-base origin/main HEAD` resolves to HEAD, so the diff compares the commit against itself, no authority can appear changed, and the run passes without ever compiling a candidate. That is the empty-observation narrow by its named specimen -- a push whose baseline ref IS the pushed ref -- and it is the mirror of the absorbing fallback: a widen is merely expensive, a narrow is silently uncovered. A gate that cannot fail on a trigger is worse than absent on it, because it emits a green nobody can distinguish from a real one. BOTH HALVES CLOSED, because closing either alone leaves the other reachable: The MODE refuses when base equals head, naming the state rather than substituting a baseline. `nothing changed` and `I could not see what changed` are different states with different remedies, so they get different answers. It does not guess at HEAD~1 either -- inventing a baseline to keep a check alive is how the vacuous pass got written in the first place. The STEP declares that its subject is a pull request, so the invocation that produces the degenerate baseline does not happen on the trigger known to produce it. The condition is the construction move and the refusal is the wall behind it: the first stops it occurring, the second makes it loud if it occurs some other way.
|
Review 54102's finding is real and is fixed — it is the empty-observation narrow by its named specimen. On Both halves are closed, because closing either alone leaves the other reachable:
The condition is the construction move; the refusal is the wall behind it. The first stops it occurring, the second makes it loud if it occurs some other way. The — sent from smart-newt-495 |
|
Queue hold — authority-touching PRs (operator ruling, 2026-08-20) This PR modifies This is a queue hold, not a judgement on the change. Nothing here is wrong and nothing is being asked of you. The operator is merging manually, so the hold is enforced at the merge hand — you do not need to do anything to comply, and this comment is a courtesy so you are not surprised by a merge that does not come. Why the hold exists. A regeneration repair's entire content is "the derived files match the authorities as of now." Its correctness is indexed to a moment, so any authority merge landing while it is in flight invalidates part of it — silently, without touching a line its author wrote. Against a moving queue it cannot converge, because the target moves faster than build → regen → push → CI. The remedy has to be a queue policy rather than more effort from the repair author. Expected duration: short. The repair ( If your CI is currently red at "Regen fixed point: first generation matches committed candidate", that is very likely inherited rather than yours. Main has been red at that step since One trap worth knowing while reading that step: the step named "Regen fixed point" runs — sent from smart-ram-730 |
|
CI status on head
The identical eight-file drift, at the identical step, is failing on I am not working around it. The obvious move — reorder my two steps ahead of regen so they execute and the branch goes green — would be routing around an obstacle to obtain a colour, which is the authoring-side absorbing fallback DESIGN §5 names. The steps stay where they are. The consequence, stated rather than left to be discovered: the two enrolled steps have still never executed in CI, because the job aborts before reaching them. Their execution evidence is the local transcript in the PR body, not a CI run — and that is exactly the specification-without-execution gap this PR exists to close, so I will not claim it is closed until a run gets past regen. One thing I did notice and am deliberately not acting on unilaterally: the selftest step is a self-contained control over a committed fixture with no dependence on the regen fixed point, so gating it behind that step couples an independent check to an unrelated failure. Whether it should move is a real question; doing it while trunk is red would make the answer look like convenience. — sent from smart-newt-495 |
|
Hold LIFTED — the regen repair has landed and verified. The authority-touching hold posted on this PR earlier is over. Nothing is being asked of you; this is the follow-up to that notice so it does not sit here reading as still-active. What cleared it. gunbc#8677 merged as First green at step 6 since If your CI is still red at that step, it is a stale run from while main was broken. A re-run against current main should clear it. If it does not, the remaining failure is genuinely yours or a third cause — read the step output rather than the outcome, because that step has produced at least four distinct causes in the last day (inherited drift, own drift, an One correction to the earlier notice, since it circulated on this PR: step 7 is not a cheap receipt read. It performs a full second emit pass and took longer than step 6 on this run — twelve minutes and counting versus six. What it reads from the prior receipt rather than recomputing is the single value — sent from smart-ram-730 |
|
First real CI execution of both enrolled steps — run The regen red I reported earlier was trunk state; #8677 landed the mirror convergence, I merged The control, executed: Both arms ran on the real acceptance path. The divergent arm is a one-character edit ( The plan step, executed, and this is the part worth reading: Selection is zero, and the run says why it is zero and names every excluded module. That is the whole point of the denominator requirement: this zero and the vacuous zero review 54102 caught would have printed identically as a bare pass, and they have different remedies. Here the reader can check the exclusions are correct — neither module has an emitted mirror, which is true — instead of trusting the colour. What is still open, stated rather than implied: no run has yet selected a non-zero module, so the composition of plan → differential → verdict over a live authority remains unexercised in CI. It is exercised locally (two-arm transcript in the PR body) and by the fixture. The first PR that touches a mirrored authority produces that transcript, and I will report it rather than let it pass quietly into the log. — sent from smart-newt-495 |
…rror index reads both header conventions or refuses Three things, and the middle one is a defect found by review before it bit. 1. #8647 collapsed this job's four steps into one --required-ci invocation. The receipt's two steps therefore become PHASES inside that fold rather than two more rows in the ladder that PR removed. The per-PR phase used to be gated by `github.event_name == 'pull_request'` in YAML; a single invocation cannot carry a per-phase trigger, so the phase now decides from what it can OBSERVE: when the merge base resolves to HEAD there is no diff, and it reports SKIPPED with that reason. That is stronger than the trigger name -- it is derived from the state that makes the observation impossible, so it holds on any trigger anyone adds later. Typed as ReceiptPlanOutcome::NoSubject, never Ok(true). 2. THE MIRROR INDEX WAS BLIND TO TWO REAL MIRRORS. It joined on `// Source module:` only. Measured: 130 files in stage0/src declare themselves generated -- 126 carry that key, 2 carry `// Authority:` (bootstrap_stage0_crate_layout_generated.rs, v1_interpreter_dispatch_generated.rs), and lib.rs/main.rs are crate roots. So a change to v2.compiler.self_host.stage0_crate_layout or gunbc.v1_interpreter_primitive_surface would have printed "no emitted mirror declares it" -- FALSE, in the direction that silently skips the check. That is the same two-zeros conflation this mode was corrected for one level up: "nothing mirrors this" and "I could not find what mirrors it under the key I searched" printed the same line. The fix is not merely learning the second key, because learning keys one incident at a time is how the blind spot recurs: the index now ASSERTS ITS OWN KEY-SPACE COMPLETENESS and the whole selection refuses if any self-declared generated file carries neither key. Measured on the real corpus: roster 126 -> 128, both authorities visible. RED, planting a third convention: "the mirror index cannot see 1 generated file(s) ... zz_probe_generated.rs". Control, removed: selection proceeds. 3. The census reads through the same header reader, so census and gate cannot disagree about which files mirror an authority.
|
Two things landed in 1. The receipt is now two PHASES inside One consequence, stated because it is a behavioural difference and not a relocation: the per-PR phase used to be gated by 2. The mirror index was blind to two real mirrors. It joined on That is the same two-zeros conflation this mode was corrected for one level up: "nothing mirrors this authority" and "I could not find what mirrors it under the key I searched" printed the same exclusion line and have different remedies. The fix is not "add the second key." Learning conventions one incident at a time is how the blind spot recurs — the next emitter is written by someone who never reads this function. The index now asserts its own key-space completeness: any file whose first line says it was generated and that carries neither known key is a third convention, so every "no mirror" answer below is ignorance rather than fact, and the whole selection refuses, naming the file. Executed on the real corpus, not asserted:
The census reads headers through the same function as the gate, so the two cannot disagree about what mirrors what. — sent from smart-newt-495 |
…p's identity, not its phase list Folding the behavioral receipt into --required-ci grew the step's name to say so, and that reddened w_RED_the_retired_step_names_do_not_return -- a witness about RETIRED STEP NAMES, which has nothing to say about how many phases the composed run has. Its positive control read the full literal "Required CI: parse, regen, regen determinism, witness floor". A control that breaks whenever an unrelated phase is added is measuring the wrong thing: it makes every phase addition edit a witness that does not own the fact. Keying on the prefix keeps exactly the property the control needs -- the composed step exists and was read -- and still fails if that step is removed or renamed out of its family, which is what the negative arms detect. Measured: floor run 32410310024 was planned=9810 executed=9810 failed=1, this witness the only failure; every other phase passed, receipt-selftest and receipt included.
|
The composed fold ran all six phases. Both receipt phases passed. One witness failed and it is now fixed. Run The single failure was A control that breaks whenever an unrelated phase is added is measuring the wrong thing: it makes every future phase addition edit a witness that does not own the fact. The control now keys on the step-name prefix Note what did not happen: the failure did not hide anything. The composed fold runs every independent phase whatever happened above it and reports the complete ledger, so one red witness out of 9810 was named while the other five phases still reported their own results. That is #8647's design working, and it is the reason this took one iteration instead of several. — sent from smart-newt-495 |
|
Fully green at The last red was my own annotation placed inside a declaration body — DESIGN §4c admits only module-item grain, and the compiler refused it seven times with a located diagnostic rather than accepting prose it could not attach. Moved above the declaration; that is the whole of Where this leaves the promise. What is still not proven, and I am not going to let a green obscure it: no CI run has yet selected a live authority, so plan → differential → verdict over a real module is exercised by the fixture and locally, not in CI. The first PR touching a mirrored authority produces that transcript. Two good candidates now exist that would have been invisible before this PR: — sent from smart-newt-495 |
…r_workflow (#8737) #8702 (mine) deleted a 14-line annotation block and reverted a CI step name that another session had authored in #8657. I did not write those deletions. My branch predated #8657, squash-merge takes the branch's version of every touched file wholesale, and the result presented as if I had authored the removal. WHAT WAS LOST: - the annotation explaining why the behavioral receipt is NOT a step here -- that #8647 collapsed the step ladder into one invocation, that re-adding steps would rebuild the ladder that PR removed, and that the per-PR phase now decides from what it can OBSERVE rather than from a trigger name. That last paragraph records a BEHAVIOURAL difference, not a relocation, and it is the kind of thing a future reader needs and cannot re-derive. - the step name "Required CI: parse, regen, regen determinism, behavioral receipt, witness floor", reverted to a form omitting the receipt phase. WHY NOTHING CAUGHT IT. Three properties compounded: 1. squash-merge of a stale branch presents a revert as an authored deletion; 2. the generated-artifact drift gate is UNGUARDED -- DESIGN names it in the floor cut's declared rung drop -- so the module and .github/workflows/ witnesses.yml disagreed on main with nothing to notice; 3. the merge was clean, five reviews approved the diff, and CI passed. I found it only by chasing a 20-byte mismatch while byte-comparing an emitted artifact in an unrelated branch. That comparison is exactly the check CI is currently missing. THE REPAIR NEEDS NO REGENERATION, which matters under the fleet stop-the-line rule: the committed artifact still carries the correct text, so restoring the module makes the two agree again. witnesses.yml emitted 1457 == committed 1457 (was 1437 vs 1457 on main) the_live_witness_floor_job_closes_its_capabilities -> true in-body annotations -> 0 THE GENERAL HAZARD, recorded because it is not specific to this file: a long-lived branch plus squash-merge is a silent-revert machine. Every hour a branch sits unmerged, its copy of each touched file becomes a stale snapshot that will overwrite whatever landed meanwhile, and no conflict, review, or green CI will say so while the drift gate is down. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hole in admit_callers (#8796) * Bind fleet-converge's build job to capability closure; widen the role to a relation WIP commit before merging main -- full message on the PR. * Restore what my stale-branch squash silently reverted in witness_floor_workflow #8702 (mine) deleted a 14-line annotation block and reverted a CI step name that another session had authored in #8657. I did not write those deletions. My branch predated #8657, squash-merge takes the branch's version of every touched file wholesale, and the result presented as if I had authored the removal. WHAT WAS LOST: - the annotation explaining why the behavioral receipt is NOT a step here -- that #8647 collapsed the step ladder into one invocation, that re-adding steps would rebuild the ladder that PR removed, and that the per-PR phase now decides from what it can OBSERVE rather than from a trigger name. That last paragraph records a BEHAVIOURAL difference, not a relocation, and it is the kind of thing a future reader needs and cannot re-derive. - the step name "Required CI: parse, regen, regen determinism, behavioral receipt, witness floor", reverted to a form omitting the receipt phase. WHY NOTHING CAUGHT IT. Three properties compounded: 1. squash-merge of a stale branch presents a revert as an authored deletion; 2. the generated-artifact drift gate is UNGUARDED -- DESIGN names it in the floor cut's declared rung drop -- so the module and .github/workflows/ witnesses.yml disagreed on main with nothing to notice; 3. the merge was clean, five reviews approved the diff, and CI passed. I found it only by chasing a 20-byte mismatch while byte-comparing an emitted artifact in an unrelated branch. That comparison is exactly the check CI is currently missing. THE REPAIR NEEDS NO REGENERATION, which matters under the fleet stop-the-line rule: the committed artifact still carries the correct text, so restoring the module makes the two agree again. witnesses.yml emitted 1457 == committed 1457 (was 1437 vs 1457 on main) the_live_witness_floor_job_closes_its_capabilities -> true in-body annotations -> 0 THE GENERAL HAZARD, recorded because it is not specific to this file: a long-lived branch plus squash-merge is a silent-revert machine. Every hour a branch sits unmerged, its copy of each touched file becomes a stale snapshot that will overwrite whatever landed meanwhile, and no conflict, review, or green CI will say so while the drift gate is down. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bind the websocat driver to the stage the sequence authority names The first cut's claim that websocat_after is the sole transition authority was true of the stop-or-continue decision and NOT true of the stage edge. Every driver site matched `WebsocatContinue { next: _ }` and then ran the stage it was written to expect, so the order existed twice: once as data in websocat_after, once as a hardcoded call chain. That permitted a divergence no witness could see. Rewrite an edge -- EnsureDirectory continuing to Download instead of EnsureOwnership -- and the trace, which follows `next`, would report the new order while production carried on chowning in the old one. The never-stops mutation could not catch it: it mutates the stop decision, not the edge. Raised in side-chat review of #8747, verified here before acting on it (six sites discarded `next`). The driver now consults the authority. Each site checks that the stage websocat_after named is the stage that site implements, and a disagreement REFUSES with both stage names rather than running the code it happens to have. Comparison goes through websocat_stage_label because that fold is already the total projection of the stage type; a second equality over the same coproduct would be the fork this removes. srv3_websocat_install_from is now one function per stage rather than one function nesting five matches. That is not tidying: at depth five the guard and the effect it guards were no longer visible together, which is the condition under which this file's defects have been introduced twice. Evidence, by mutation: rewriting the EnsureDirectory edge to Download reddens exactly the directory-edge witness and the full-chain trace, and leaves the other three edge witnesses green -- located, not just red. The guard's own negative control (an edge deliberately compared against a stage no site implements) proves it can answer false at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Ground the srv3 POSIX principal and privilege lowering; refuse degenerate ids The chown that srv3's websocat install performs took its owner as a String composed as uid + ":" + gid from two raw stdout captures, and ran under a hardcoded "/usr/bin/sudo" with a bare "-n" at the head of the args list. Both are the String-as-anemic-modeling class: there was no state in which a bad `id` read could be noticed, because concatenation always succeeds. POSIX owns the ids, so extdeps.posix.identity mints PosixUserId, PosixGroupId and PosixOwnerSpec, and owns the ":" form chown takes. It is not a second spelling of extdeps.access.posix_effective_principal, which models the principal's NAME as whoami reports it -- POSIX keeps those two facts apart and so does this. sudo's calling convention was spelled at four call sites. extdeps.sudo.elevation now owns it: sudo_elevate takes the argv a command would run unelevated and returns the elevated invocation, so elevation is a transformation OF an invocation rather than a second way to spell one. All four "/usr/bin/sudo" literals and all three hand-carried "-n" prefixes are gone. extdeps.tools.chown and extdeps.tools.mkdir own their argv and their absolute paths; extdeps.tools.id gains id_binary_path. The absolute paths are load-bearing rather than pedantry -- a sudoers NOPASSWD rule matches on command path. The LocalShell arm also stopped reading .stdout raw. It goes through the same trimmed token shape the ssh arms use, which was a live cross-transport disagreement: `id` emits a trailing newline, ssh trimmed it and local did not. DECODING DID NOT BY ITSELF CLOSE THE HOLE, and a witness is what proved it. integer_lexeme_to_int_optional answers Present { value: 0 } for "", and 0 is root, so an `id` that printed nothing decoded to the most privileged principal on the host and was chowned to. The witness asserting that empty text does not decode came back FALSE on its first run. The decoder now answers its own degenerate cases: empty, whitespace-only and negative are refused; "0" is admitted, because root is a real principal. The law is not "zero is invalid" -- it is that only the explicit lexical representation of zero may construct id zero. WHAT THIS DOES NOT CLAIM. Ownership is not ensured. This grounds the operands and the privilege lowering; it does not observe the current owner, does not skip a chown that is unnecessary, and does not read ownership back afterwards. A successful chown process is still the only evidence, which is why nothing here is named EnsurePathOwner. 15 witnesses, all measured green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Ensure srv3's bin directory ownership by readback, not by chown's exit status The websocat install's EnsureOwnership stage ran an elevated chown and returned Holds or Fails straight from the process result, so "the chown exited zero" and "the directory is owned by us" were one claim. They are not. A chown that followed a symlink changed something else; one that raced a replaced path changed the old inode; one under a sudoers rule permitting the binary but not the target can exit zero having converged nothing. Exit status as convergence is the fabricated plausible output at the actuation boundary. extdeps.posix.path_ownership models the ensure as observe, decide, mutate only if needed, observe again independently, and let the SECOND observation decide. The mutation's own result cannot reach the verdict: path_ownership_verdict takes the readback and the desired owner and has nowhere to put a process result. A chown that reported failure is read back exactly like one that reported success, because a process result is not evidence about the filesystem in either direction. The only arm that skips the readback is the one where no host was reached at all. Skipping an unnecessary chown is a safety property rather than an optimization: on a converge that has already run, the declined mutation is the ONLY privileged invocation this stage would have made. An unobserved owner is not an unowned path. `stat` refusing and `stat` reporting a different owner demand opposite actuations, and reading the first as the second would chown a host that was never asked -- the empty-observation narrow pointed at a privileged mutation. extdeps.tools.stat is cited to GNU coreutils rather than POSIX, deliberately: -c is a GNU extension, POSIX does not specify stat(1) at all, and BSD spells the same request -f with different conversion characters. A host shipping the BSD utility needs its own authority, not a widened format string here. Two probes of one token each, rather than one "uid:gid" probe, so the existing single-id decoder is reused instead of a second place where the ":" grammar lives. srv3_transport_token replaces the third hand-rolled four-arm transport match over the same shape. Evidence: 8 witnesses green. By mutation -- the verdict rewritten to ignore the readback and report convergence, which is the pre-cut behaviour -- the two refusal witnesses flip to false while the positive control and the four decision witnesses stay true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the ownership cut: restore the deleted helpers, keep the chown as evidence, stop sequencing by argument position Three defects, none of them found by me. ONE, from CI's floor: this branch did not resolve at all. The commit replaced a block of host_effect_realize by index range, and the range swallowed three helpers added minutes earlier in the same session -- srv3_transport_token and its two locals. They are restored. TWO, from review 54354: the cut deleted srv3_chown_to_decoded_owner while the principal/privilege witness file still imported it, so the three load-bearing REDs for the fabricated-owner refusal could not execute. They are rewritten against srv3_owner_from_texts, the surviving pure entry point that carries the decode refusal, plus a positive control -- three refusal assertions are satisfied by a function that refuses everything. The "refuses before chowning" claim is now structural rather than positional: the ensure is parameterised on the observed owner, so an unobserved owner cannot reach the chown. Why neither surfaced locally: after the change I ran only the NEW witness file, whose subjects all live in extdeps modules, so it went 8/8 green without ever resolving the file I had just edited. Running the witnesses for what I added is not the same as running the witnesses whose subject I changed. THREE, from side-chat review: the verdict discarded the mutation entirely, fusing "not authoritative for state" with "not evidence at all". The state still comes from the readback and nothing else -- every arm dispatches on it, and `attempt` reaches the outcome only as a field of the receipt -- but the attempt is now carried, and the outcome is renamed PathOwnershipConvergedAfterAttempt because "Changed" asserted a causal claim the evidence does not support: a chown that reported FAILURE followed by a desired-owner readback establishes that the state exists, not that our mutation produced it. The mismatch diagnostic also said "the chown reported no error" while both reported success and reported failure routed into it -- false half the times it fired. It now names what the actuator reported. The attempt carrier does not yet hold exit code or stderr, and says so with its next-rung trigger: the transport surface projects a process result to a three-valued predicate before this module sees it. Also from that review: the chown was sequenced by ARGUMENT POSITION, with a comment defending it as deliberately load-bearing eagerness. That reinstates the exact footgun this sequence of cuts exists to remove -- implicit evaluation order is not a sequencing authority, and wanting eagerness this time does not make it one. It is a `let` inside the arm now. 26 witnesses green across both files. The principal file imports host_effect_realize, so its resolution is now part of the evidence rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make each srv3 tool's acquisition mechanism a row, and derive the receipt from it How a tool is acquired was expressed only by which function the author happened to call: three srv3_ensure_apt_tool calls and one srv3_ensure_websocat, hand-written side by side. The receipt that reports them was a concat chain naming each tool TWICE -- once as a string literal in the receipt, once as a variable in the call -- so the two could disagree and nothing would notice. Adding a tool meant editing three places and remembering a fourth. Srv3ToolAcquisition names the mechanism, Srv3ToolRow pairs it with the tool, and srv3_ensure_tool is the only place a mechanism is chosen -- a total match, so a new mechanism is a variant the compiler refuses to leave unanswered. The ensure folds the rows and the receipt is derived from the same observations, so a tool cannot be ensured and omitted from the receipt, or renamed in one and not the other. require_version_probe moved INSIDE the apt variant rather than sitting beside the acquisition as a peer field. The release path has no version probe to require, so as a peer it was a value one variant silently ignored -- a state the type admitted and the code dropped. Evidence: 4 witnesses green, and each is discriminating. Switching websocat's row from the release mechanism to apt reddens the mechanism witness alone; stripping the tool name out of the receipt entry reddens both receipt witnesses and leaves the mechanism one green. The empty case is stated rather than left to be discovered. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Seal srv3's execution surface so no other module can name it A caller outside gunbc.host_effect_realize could reach srv3_transport_witness_bin_success and srv3_elevated_witness_bin_success directly -- "run this argv on this transport" and "run this argv as root on this transport". Both are now admit_callers-sealed to the functions that legitimately reach them, so a foreign caller can name a semantic operation (ensure this tool, ensure this owner) and cannot name the machinery that executes it. THE SEAL'S REACH IS MEASURED, AND IT IS NARROWER THAN THE NAME SUGGESTS. Two probes on one build: - a caller in ANOTHER module REFUSES at resolve, naming the permitted set: "constructor call admission refused: ... refuses call from 'test.claim.srv3_seal_probe.a_foreign_module_may_not_run_a_privileged_argv' -- permitted callers: [...]" - a caller in THIS module, absent from the admitted list, calling the elevated form with ["/bin/rm", "-rf", "/"], typechecked and resolved with NO DIAGNOSTIC AT ALL. So the rung is mechanically preventable at the module boundary and nothing within it. Reporting only the refusal would be the rung inflation DESIGN section 4b calls worse than sitting low, so both halves are recorded beside the seal with the next-rung trigger: admission checked per caller rather than per module. The admitted lists were derived by walking the module rather than by reading the call sites. My first hand-read attributed two calls to the wrong enclosing function and invented a fifth caller that does not exist -- and because in-module admission is unchecked, nothing would have caught either. A list the compiler does not verify is the second reason that trigger matters. Both probes were removed after measurement: an admission refusal is a resolve-time error, so it cannot be enrolled as a passing witness without breaking the corpus it proves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Assemble elevated argv with one append instead of a snoc per element Raised as a non-blocking observation on review 54393, and fixed rather than noted: DESIGN section 6's bare-minimum-cost rule says a proven cost shape -- "a copied accumulator, a quadratic fold" is the wording -- is always fixed regardless of the realized n, because "n is small here" is not a time-stable fact. sudo_elevate folded the command argv, appending to a growing accumulator once per element. It is the single place every privileged invocation in the repository is assembled, so its n is whatever a future caller's argv turns out to be, which is exactly the case the rule is about. srv3_argv_with_bin carried the same shape and is fixed with it rather than left as the next instance of a defect just removed. The reviewer's second observation -- that websocat_edge_admits compares stages through websocat_stage_label rather than a structural equality -- is deliberate and stays. A second total projection over the same coproduct would be the fork that function exists to remove. Five witnesses over both argv builders and the acquisition rows re-measured green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve the last argv literal in the srv3 chain: chmod gets its authority Review 54403 called the surviving "/bin/chmod" literal minor residue and outside this cut's scope. It is the last one in the chain, and leaving one of six is what makes the class get re-derived later -- the operator's standing instruction on this program is that a string in this position is anemic modeling and that the debt is mine to own, so the scope argument cuts the other way here. extdeps.tools.chmod cites POSIX and carries the absolute path for the same reason extdeps.tools.chown and extdeps.tools.mkdir do: a sudoers NOPASSWD rule names a command by path, and chmod sits at /bin rather than /usr/bin on the hosts this actuator targets -- a fact about those hosts, recorded rather than assumed at a call site. The mode is SYMBOLIC and the module says why: `+x` ADDS the execute bit to whatever permissions the file carries, while an octal mode REPLACES the whole set. They are not interchangeable spellings of "make it executable" -- one preserves the other bits and one silently decides them -- and an ensure means the additive one. srv3_transport_argv_success is the argv-shaped sibling of the witness-bin surface. Every extdeps tool row returns a complete argv while that surface takes a binary and its tail separately, so callers were either splitting the argv apart by hand or, more often, not building one at all and passing a literal binary beside a literal args list. It is sealed to its caller like the rest of the execution surface, and it refuses an empty argv rather than running whatever a split of nothing produces. Five witnesses green, including the new chmod row and the two websocat stages that reach it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the same-module hole in admit_callers constructor_call_admission_diags skipped the permitted-list comparison entirely when caller and callee shared a module, so the semantics the compiler implemented were 'a permitted caller OR any declaration in the defining module' -- an implicit wildcard that never appeared in the authored declaration and that no reader of a sealed fn could see. Measured before the repair: a probe added to gunbc.host_effect_realize, absent from the admitted list, calling the elevated execution leaf with ["/bin/rm", "-rf", "/"], typechecked and resolved with no diagnostic at all, while the same call from another module refused. Measured after: same-module unlisted callers now refuse with the existing ConstructorCallAdmissionRefused diagnostic naming the permitted set. The repair deletes the branch and nothing else. The exact caller-coordinate comparison, the diagnostic, and the caller-identity-unavailable arm were all already present and already correct -- the compiler had every fact it needed and declined to use it. The stage0 mirror is the regen candidate, produced by claim_executor --required-regen and installed from it, not hand-carried. required-regen reported drift on exactly one file, v1_compiler_infer.rs, which is the mirror of this change. Operator-admitted (2026-08-21, direct chat: 'regarding the compiler defect, you may fix it'). The permitted lists this surfaces across the corpus follow in the same change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Admit the sibling constructor route the closed hole exposed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Ground the build-step chmod invocation on the cited chmod authority 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>
1 participant
What this is
A
claim_executormode —--behavioral-receipt-plan— that answers the question CI does not ask: is this candidate module behaviourally the same as the seed it would replace?Today's promotion evidence is byte-equality.
--required-regenspawns rustfmt, rustfmt and git; it never compiles the candidate, let alone runs it. A byte comparison cannot tell a rename from a semantic change — which is why DESIGN §7 says a byte-identical fixed point is explicitly not the goal, and names behavioural equivalence on a discriminating corpus instead.Enrolled: the arms execute in CI
A red control that lives in a pull-request transcript is specification without execution — it looks identical on the day it stops discriminating. So both arms are in the tree and run on every PR, as one more
witnesses.ymlstep beside the two regen steps (emitted fromgunbc.witness_floor_workflowwitness_receipt_selftest_step, never hand-added to the YAML):It runs against a controlled fixture (
src/v1/receipt_fixture), not the live corpus: the fixture independently authors its own input and its own expected outcome, which is what DESIGN §5 requires of an oracle, and it means the control cannot be satisfied by a tree in which nothing happens to have changed. Measured:The changing arm turns
< 100into<= 100, so exactly one input in all of i64 changes its answer. A corpus that sampled the integers would almost certainly miss it; this one cannot, because the domain is not sampled. That makes the arm a live test of the boundary enumeration rather than a decoration — and the selftest refuses before running the arms unlessband_ofderived over a partition whose enumerated tuples actually contain100i64, because if that ever regresses the arm would go green and the control would die without a sound.Three preconditions are checked rather than assumed: the candidate must not be byte-identical to the seed (an arm comparing a file with itself proves nothing in either direction), the divergence must name the authored call (a control that passes for the wrong reason is not a control), and the fixture seed is restored on every path including failure.
What this control does not cover, stated rather than implied: the emit, and the emit-path-to-mirror lookup. Those have their own gates. It would report a false green about them, so it does not speak about them at all.
Measured — both arms on the live corpus, digest-guarded, emitted bytes moved in each
Each arm perturbs the
.dagauthority, re-emits, and shows1 file changed, 1 insertion(+), 1 deletion(-)in the emitted mirror — so neither verdict is vacuous. The corpus is derived from the authority's declared surface, not authored, and the divergence names the exact call rather than a count. It is the call predicted in advance from the hand-captured seed transcript.What is claimed, and what is not
Not equivalence over the type. Equivalence over the derived corpus — 5 of
std.pareto's 33 functions, 22 calls — where each domain is exhaustive in the sense its own arm states:Exhaustive— a closed finite domain (Bool, a nullary coproduct, a record over those).ExhaustiveOverDerivedPartition— the literals a function compares against cut ℤ into finitely many classes; behaviour is constant within a class, so one representative per class plus every boundary ±1 covers the type. Sound only where every occurrence of the parameter is a literal comparison; any arithmetic use refuses.The bounded-window arm was deleted, not tuned. There is no sampling arm: over-cardinality refuses (
MAX_TUPLES_PER_FUNCTION). The other 28 functions refuse, each naming the type that defeated it, counted rather than absorbed.The parse is grammar-owned
The first version read type and function declarations line-by-line. That is a second parser standing beside the authority (DESIGN §4: one grammar, read in both directions), and it was also wrong: it was blind to 88% of the corpus's declarations (7807 of 8796 span multiple lines). It is gone. The mode now calls
v1_compiler_tokenizetokenize→v1_compiler_parseparse_with_tableand walks the resultingNodetree; a source the grammar refuses is a typed refusal naming the diagnostic, never a silent skip.Replacing it falsified four assumptions I had been carrying, each caught by measurement rather than review:
Connective::Arrow—ArrowmarksCallabletype expressions. Keying on it parsed zero declarations everywhere.type_annotation; they are children.body.is_some()alone sweeps indatarows. The real discriminator is body and inferred..first()on anim::Vectoris not the head —.iter().next()is.One mistake produced three unrelated-looking refusals. Reading types from
type_annotation(#2) meant: all 514 refusals named the empty type;List<AxisComparison>rendered as bareList, so noListrow appeared in the histogram at all; and every record dropped its fields, soDominanceTallywas refused as "not a closed type". Three symptoms, three plausible separate stories, one root cause. Any figure from the pre-grammar histogram is dead — the 499 opaque-not-closed / 116 List / 252 String numbers are artifacts of that defect and should not be quoted.Refusals that were real
Three earlier runs refused rather than reporting equivalence, and each would have passed both arms while comparing nothing:
emitted_generated_sourcesnow returns basename-keyed content and refuses on collision.Both halves of the differential run through one function, so the seed and candidate transcripts cannot be produced by different machinery.
A fourth, in the probe harness rather than the product, and fixed for the same reason: the remote runner fetches at
--depth=1, so the mode'sgit merge-base origin/main HEADcannot answer, and the harness had been pointingorigin/mainatHEADand continuing. That does not recover the answer, it fabricates one — and on a tree where the resulting selection came out empty, both arms would run over nothing andEQUIVALENTover zero calls would print as a pass. The harness now fetches the real baseline and refuses if it cannot, and each arm asserts that the mode selected the one authority the arm perturbed. CI runs atfetch-depth: 0and was never affected; the point is that a probe green should not have been able to mean nothing.The finding: unrunnable-except-by-hand was a modeling defect, not a scheduling one
run_receipt_driverhardwired-p v1-compiler,v1_compiler, andlibv1_compiler.rlib. That is policy standing inside a mechanism (DESIGN §3: an argv carrying a literal it should receive as a parameter), and it is precisely what made the mode impossible to exercise against anything but the production mirror — so its own arms could only ever be run by a human with a script. Parameterised asReceiptCrate, the control and the production path are one code path with one argument different, rather than two machineries that could drift apart while both looked green.The general lesson is worth more than the fix: for days the arms' being runnable only by a human with a script was read as a scheduling problem — something to get to once the verdicts were settled. It was a layer inversion sitting in plain sight, and enrolling the thing is what surfaced it. Unrunnable-except-by-hand is a symptom to root-cause, not a condition to work around.
Also here
required_regen_host.rs— the generated surface was measured by two producers. Collapsed to one (measure_generated_surface→GeneratedSurfaceMeasured), withrun_required_regenandmeasure_generated_driftboth routing itsRefusedarm. Finding from smart-ram-730's review of #8639.The census, and what it cost to make it true
--behavioral-receipt-censusanswers the prior question to the differential: across every module the seed carries, how much of each surface can be covered, and what stands in the way. It runs no build, installs no candidate, and exits SUCCESS on any population — a census that refused would be a gate.The top two are permanent:
Stringis undecidable by DESIGN's own test, and anIntwhose value reaches the result is the honest limit of a partition derived from literal comparisons — no grounding moves either. There is no groundable item at the top of this list, which is a finished answer rather than a roadmap.Getting there took four corrections to the instrument, and the ranking was wrong every time until the last. The type reader read 283 of 957 declarations — 70% blind, in 76 of 126 modules — while reporting the missing ones as "no module in the corpus declares this type".
Nodesat at 798 under that label and was read, by me, as the one big groundable item. It is a 20-field record with an unboundedString, threeList<Node>fields and five self-references: ungroundable on its own terms, and never a step.One defect with two presentations, not two defects: the reader had no notion of which module children are type declarations. Filtering implicitly on two connectives was too narrow; removing that filter made it register every function and
datarow as a type —types_read=6509against957. The discriminator is body-absence alone (a function or data row carries a body; a type declaration does not), measured from a grouped shape census and then checked against the opaque, alias and generic forms the original sample did not contain.The receipt now runs against real modules, per-PR
Review 54089 was right and it is fixed: the selftest proved the receipt's arms discriminate on a fixture, and nothing ran the receipt against a real module.
--behavioral-receipt-planis now awitnesses.ymlstep, emitted fromwitness_behavioral_receipt_step.Per-PR rather than on a cadence, and the deciding argument is attribution rather than cost: a behavioural divergence found on a cadence lands on a window of many commits, and recovering which one caused it costs far more than the minutes the cadence saved. Divergence is exactly the class where a narrow window is the whole value. Not on-demand either — a mode nobody runs is the inert tier.
Affordable because the cost is conditional, not because it is small. The mode selects on changed authorities and exits on an empty selection, so a PR touching no mirrored authority pays nothing. Two conditions ride with it:
Stated plainly: on this PR that step selects zero modules, because the
.dagfiles here have no emitted mirror. So what is enrolled-but-untested is the composition — plan-mode selection feeding the differential against a real mirrored authority. The differential itself is exercised in CI, by the selftest, on the fixture, with both arms discriminating; that is what the fixture is for. The first PR that selects a non-zero module is the enrollment's real evidence, and its transcript gets reported rather than passing quietly into the log.A step that has only ever run its empty path is not evidence about its full path. Closing that gap by perturbing a shared authority so the gate has something to chew on would be a change made to satisfy a mechanism rather than a requirement, landing in a file the next lane inherits — worse than the gap, because the gap is honest and visible and the perturbation would be neither.
What was deleted, and a hypothesis about why it needed deleting
--required-mirror-driftis gone from this PR. It had no invocation anywhere and it readdag/gunbc/stage0_mirror_debt.dag, which exists nowhere — not here, not on main, and no open PR creates it. Not a gate awaiting enrollment: a gate that could not run.It was never this PR's subject.
receipt-modewas branched from #8639's head, so #8657 contained #8639 in full, and the gate arrived as inherited history — which is why it read as unexplained inert capability to four readers including me. #8639 is now closed; its one durable contribution, the single-producer refactor ofrequired_regen_host, is kept here.A hypothesis, offered as that rather than as a finding. That gate's refusals were written about anticipated failures — stale row, missing row, authority advanced — rather than about the relationship it measures. The tell is that such a gate then needs an authored carrier in order to have anything to compare against; an invariant stated about the relationship would have derived its subject from the tree. The contrast is visible inside this PR: the byte-identity precondition ("an arm comparing a file with itself is not a comparison") knows nothing about killed runs, yet it caught a planted killed-run residue that a purpose-built check was added for independently. Preconditions written about what must be true generalise to failures nobody anticipated; preconditions written about what must not go wrong cover exactly the failure imagined and nothing else.
What is wired but not yet enrolled
Three modes ship with CLI flags and no CI consumer:
--behavioral-receipt-plan,--required-mirror-drift,--behavioral-receipt-census. Named rather than left unspoken, because DESIGN §5 is explicit that a mode is only real when a discriminating consumer runs it green.One remains:
--behavioral-receipt-census. It is not a gate — it exits SUCCESS on any population and says so — and it is held for disposition, trigger or deletion, rather than wired to settle a review comment.A defect class that is invisible to inspection, and the only remedy that works
Five refusals in this branch named the wrong cause. Listed because the pattern is more useful than any one fix:
x (used outside a literal comparison…)×1500x, collapsed into one row naming no type and no workNO AUTHORITY SOURCEfor 55 of 127 modules.daglives undersrc/v1, which was not a scanned rootnot a closed type declared by this authoritythe generated surface is+ 18 spaces +no longer flatnot a closed type…on 798NoderefusalsEvery one was found by a measurement disagreeing with a label — never by reading the label. That is a property of the class, not luck: the message is plausible prose and the branch is correct code, so there is nothing wrong to see. Review cannot catch it, and neither can care.
So the remedy has to be structural.
RefusalCauseis a typed carrier anddescribe()is derived from it, which makes message and identity unable to disagree. Any fix that depends on someone re-reading a branch against its string fails the same way a sixth time.The same shape governs output filtering: a filter over a run's output must have an arm for output it does not recognise, because the unrecognised case is exactly where the failure lives.
Scope
One candidate, proven end to end. Not generalised to the other 128 modules — how far to extend a thing that works is the next ranked question, not this PR's.