Repository navigation
R1: decide the flow, not the position — locate the wrap-decision root and refuse producer/consumer disagreement - #8349
Merged
Merged
Conversation
…correct the census's own emitter attribution The lane's problem statement said the Rust emitter wraps every shared_types member. Measured against two independently produced emitted trees, that is not what happens, and the difference decides what a fix may be. Three findings, none of which change code: The emitter that produced the 55-site census is frozen v1, not v2. The emitted files are named v2_* because their SOURCE modules are v2 .dag files; stage0 carries v1_compiler_emit_rust.rs and no v2_compiler_translate.rs at all, so wrap_decision_gate was dormant throughout. An earlier cross-lane inference that joined the v2 catalog's position fork to these numbers is retired here. The root is a type-level fact consumed through occurrence-level keys. build_shared_types computes membership once per type; three seams then consult it through properties of each occurrence's syntax, and no arm refuses when they disagree -- render_rust_shared_type_if_needed returns the unwrapped rendering on a miss, silently. The inconsistency is far narrower than a position rule: ten types, fourteen bare field occurrences, every one wrapped at every signature occurrence and bare at one or more field occurrences, with zero bare signature occurrences in the population. Two instruments agree type for type and line for line. That makes R1 one defect producing both signs -- a signature returning Rc<T> into a bare field is the over, a bare field into a parameter typed Rc<T> is the under -- so one fix moves both counts, where a position-based fix would have moved half and worsened half. Two position-based readings are recorded as retired rather than deleted: that signature wraps while field does not, and that generic enclosing items force bare. Both were held with confidence; the first came from a sample selected by the failing sites themselves, the second was predicted from the arm cascade and falsified at 17 of 17 and 6 of 6. Disposition ruled (b) -- specification for the v2 emitter, not a v1 repair -- with the resulting coverage gap declared: the v1 image stays red and the burn-down is unmeasurable until the emitter flips. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…es producer/consumer disagreement Follows the (b) ruling: the fix is a concept v2 is missing, not a repair in the frozen v1 seed. wrap_decision_gate answers one position at a time, and every consumer acts on that answer alone. A value does not live at one position -- it is produced at one and consumed at another -- so when the two answers differ, the emitted program carries a type error no stage located, because no stage compared them. Measured, that is ten types and fourteen occurrences, and it produces BOTH error directions from one inconsistency. wrap_decision_flow_gate makes the flow the decided unit. It projects the same authority at both ends -- never a second lookup, so the ends cannot disagree about the catalog -- and refuses, typed and located, when the catalog's answers for the two positions differ. wrap_decisions_equal compares reference layers, not merely by-value against by-reference. Deliberately NOT a fifth TargetOwnershipUseSite inhabitant. Adding OwnershipAtCallArgument would be a fifth position opinion about a defect whose cause is that every position already holds its own; a missing inhabitant is the right fix only when the missing position is the one that should decide. This is also why "53 of 54 at call-argument position" does not locate the defect: that is where rustc points, and the cause is in the field declaration. Rung: silent wrongness -> mitigatable. NOT structural impossibility -- the invalid state stays writable, since a catalog may still state different layers at two positions and the only answer here is refusal. Next rung is a modeled layer transition, which is a carrier change and is sequenced ahead of the pipeline edit rather than inside it. Not wired into 06_translate here. Evidence by execution: six new witnesses green, six pre-existing unregressed, both directions drawn from the live catalog by varying only flow direction over Diagnostics. Two mutations executed; the profile is not uniform and is reported as measured -- forcing agreement reds the two directions and the layer control but NOT the missing-row witness, which is therefore a propagation regression control and not a disagreement control; layer-blind equality reds only the distinct-layer witness, which is what earns it its place. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The flow-gate note said "never a second lookup". That is the loose form and it is an overclaim. What the construction rules out is a divergent AUTHORITY -- one function over one catalog, so no second opinion exists to drift -- not a repeated read. It performs two traversals of the row list. The repeated read is a real cost shape and is now named rather than waved off as small, per DESIGN section 6's rule that a proven cost shape is fixed regardless of the realized n. It is not fixed here because the per-carrier policy that would serve both ends from one fold is the same carrier the next rung needs; building half of it now to save one fold would fork what the transition work has to own. Trigger recorded: that carrier landing. Also drops two statements the construction commit made stale: the section no longer claims to change no code, and the seam-2 figure is fourteen occurrences across ten types rather than the pre-sweep ten across six. Re-verified: module compiles clean, six flow witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tations DESIGN section 4c calls a `data NAME_note: String` whose sole purpose is commentary modeling debt, and names the leading `//` block as where irreducible rationale belongs. Both rows this branch introduced are converted. Worth stating why this is not a no-op that the gate would have waved through: `prose_row_introduction_gate` enforces only under `prose_row_migration_scope`, and none of this branch's three touched paths are among its 262 entries -- so these rows would have been COUNTED as out-of-scope residue and never refused. Legal, and still debt in the direction the migration exists to remove. Writing new prose rows into an unmigrated path because the wall does not reach there yet is the same move as relying on a check not to fire. Verified rather than assumed, against a gunbc built from this tree rather than the shim (which the annotation class is known not to be an oracle for): both compile-clean annotation refusal classes are clear -- no indented `//` inside a declaration body, and no trailing block at EOF naming no subject -- the module compiles clean, and all witnesses stay green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
…was refuted Tested the claim that this changes no emitted output outside its own module, rather than asserting it. Same entry, same command, same source roots, same binary; only the commit differs, so M is fixed by construction. Prediction written before the run, in both directions. Whole artifact diffed -- all 177 files, no grep for the shape I believed I touched, since the hazard is a second consequence the author did not predict. Two files differ, not one, and both halves of the prediction were wrong in detail: the predicted file lost a GLOB IMPORT rather than the two note constants (which turn out never to have emitted at all, in either arm), and a module I never touched -- v2_std_cross_tree_resolution.rs -- moved two pub use lines. The tempting reading of the second file is emission nondeterminism. The control refutes it: B vs B-prime, same commit re-run, is 0 differing files, and A vs B-prime reproduces the reorder exactly. It is deterministically caused by this change, by widening an import list in an unrelated module. Ownerships stated separately because they have different answers: the ARTIFACT change is mine; there is no DEFECT -- sorted line multisets are identical, so it is a pure reorder of explicit named re-exports, order-irrelevant to resolution, with no non-pub-use line involved. The whole-artifact form buys a positive argument an absence cannot: 177 files, 2 differ, 46 lines, every other byte identical -- so a path keying on emitted text this change perturbed would have had to surface elsewhere, and nothing does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…and restore a space I ate Two corrections, one substantive. THE SUBSTANTIVE ONE. This receipt read the note constants' absence from both arms as evidence that a `data NAME_note: String` prose row emits nothing. That is the vacuous-closure error the same section warns about, committed against its own author: the prose rows existed only on an intermediate commit, so NEITHER ARM EVER CONTAINED ONE, and an absence measured over a closure that never held the shape proves nothing about the shape. The general form is independently known false -- another lane watched a `_note` row appear in generated `.rs`. Whether a prose row emits is a per-site fact needing its own two-arm receipt, and this receipt does not carry one. The prose-to-annotation conversion here is justified by section 4c modeling debt alone, which was always its only real argument. A discipline follows and is recorded with it: do not convert prose rows on a PR whose emission measurement is already banked, because the conversion may be an artifact change that invalidates it. Worth being plain about the shape of the mistake, since it is the one I spent the evening catching in other people's claims: I did not measure the thing I reported. I measured something adjacent that could not have come out any other way, and read the result as though it had been at risk. THE COSMETIC ONE. An earlier edit's replacement pattern ate the space after `=` on the pre-existing `wrap_decision_composite_note` line -- a line this branch had no business touching. Restored. Caught independently in review. Re-verified: test module compiles clean, six flow witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s in the same file (#8349) The receipt read a pub-use reorder in v2_std_cross_tree_resolution.rs as deterministically caused by widening an import list, on the strength of a repeat-emit control at 0 differing files. Another lane obtained the identical shape from the null alone, with the same flag and the same SHA, moving the same two lines. A control can only accumulate failures to refute, so the file is excluded from attribution rather than explained, and the repeat count is stated as n rather than as proof. The substitution half of the receipt and the construction itself never rested on this paragraph. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…own subject file (#8349) The common-line relative-order test reported REORDERED on a file that is a pure addition of four functions. Adding code adds copies of high-multiplicity boilerplate lines, and a greedy multiplicity cap mis-pairs them, so surviving content lines appear transposed. The verdict resolved to SAME-ORDER only after excluding boilerplate, while a genuinely reordered file stayed REORDERED at every filter level and both controls behaved correctly throughout — the instrument passes its own validation while answering wrongly on a real file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rplate heuristic (#8349) Restricting the common set to values appearing exactly once on both sides reproduces both verdicts without any judgement about which lines are boilerplate: SAME-ORDER at 93 for the subject file, REORDERED at 134 for the re-export file. The heuristic filter is kept only as the route by which the false fire was found. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…oved lines (#8349) A reorder exists iff some line is both deleted and added by the alignment. That asks the question directly rather than extracting a common subsequence, so it is immune to the multiplicity family that broke three earlier variants. It reports SAME-ORDER for the subject file and REORDERED for the re-export file, naming the two qualified_name re-exports as the movers. The boilerplate heuristic and the unique-valued restriction are kept only as the route: the first can hide a reorder of boilerplate, the second cannot see a reorder of repeated lines. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… unequal (#8349) A transposition admits two alignments, and a symmetric one has no fact of the matter about which side moved. This case is a block of two qualified_name re-exports crossing a block of four cross_tree_import_model lines, so minimality picks the smaller group. Where the groups are equal size the honest output is the unordered pair. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ger (#8349) The size clause is dropped: an implementer holds the forward and reverse mover sets, which are equal in size for any transposition, so a size test refuses the cases it exists to preserve. Agreement between directions is the test; disagreement is the signature of a symmetric transposition. Both directions return the same two lines here. Minimality is a cost argument rather than an observation, so the naming is recorded as the likelier mover. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… 4 of 12 (#8349) The receipt justified its four clean pairs by a never-one-repeat rule that has since been withdrawn. At the measured rate a four-pair control misses a genuinely unstable file often, so no repeat count is offered as a clearing argument here. What excludes the file is membership in the known-unstable set. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ere are now two (#8349) The row a session greps to learn what this file covers named only wrap_decision_gate and its two RED controls, while this PR adds a second authority over a producer/consumer pair and six witnesses with a deliberately non-uniform mutation profile. Not false — incomplete, which is the shape that sponsors re-deriving an arm that already exists. The profile is stated so it says which witness guards which arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…06 candidates, direction open (#8349) The 55/28/27 count is keyed on rendered diagnostic text. A two-arm run varying only a carrier deletion left 18 sites textually identical while the realization changed underneath them, and those 18 are disjoint from the 55 — so the census misses them. The same mechanism also renders under two signatures the renderer picks between inconsistently, splitting 43 sites of one cause across two roots. A 306-row one-layer pool is a candidate set, not a hidden population; its largest block is a genuine carrier disagreement wearing the same shape. Direction of the error is unestablished in general. The mechanism and the construction are unaffected — neither reads a printed type name. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
#8349) The correction published one commit ago rested on a specimen read from one module's artifact and applied to sites in another: 01_tokenize's Nat is an enum and its closure carries no algebra alias, so those 18 sites did not move because nothing about their type changed, and an enum against an integer is a carrier disagreement rather than a wrap decision. The two spellings were two different types sharing a leaf name, not one type printed twice, so there is no 43-site mechanism. What survives is a real hazard with no measured cost here: a leaf name can denote different types under different module authorities, so a census pooled across modules is keyed on a name that is not unique over the population it pools. Alias expansion does not fix that; resolved type identity per artifact does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…fusal that narrows because of it (#8331) * Vias: what makes a net legitimately present on two layers, and the refusals that follow Rebased onto main after the copper base merged; this now carries only the via delta. The copper increment refused ANY net realized on more than one layer, having no way to tell a routed layer change from two conductors forking one name. A via is that distinction, so NetRealizedMoreThanOnce is DELETED and replaced rather than joined - a superseded refusal that still has a constructor is a second authority for one question. Both via endpoints are CopperLayerRefs, so a via inherits the stackup binding for free and cannot join one board's layer to another's. What a reference cannot carry is the endpoints being DIFFERENT, so a via from a layer to itself is a checked refusal reporting its ordinal. THE KEYSTONE ASSERTS BOTH DIRECTIONS IN ONE RUN: the identical split refuses with no via and admits with one. A via on a DIFFERENT net does not route this one, and that control is built so counting cannot pass it - same two layers, same via count, only net identity differs. AND THE HOLE NARROWING OPENED, found in review and confirmed by execution before fixing: vcc realized twice on layer 0 plus a vcc via 0 to 1 was ADMITTED, because both rows sit on a layer some via reaches. Narrowing a refusal is a DELETION - it drops every case the old form caught for reasons the new form does not model, and nothing fails when it happens because the dropped cases are the ones no witness named. Same-layer duplication is now its own cause, and the same probe refuses. DECLARED: via reachability is the WEAK form - each realized layer must be touched by some via of that net, but the vias are not required to connect those layers into one component, so a net on layers 0,1,2,3 with vias 0-1 and 2-3 passes and is still two islands. Via geometry is absent entirely. 15 witnesses green by execution. * Copper: real connectivity, retained evidence, and a name that matches the object Four corrections, all of them modeling defects this branch shipped and its approvals did not catch. Modeling accuracy outranks the approved shape. 1. TWO ISLANDS ADMITTED. net_split_is_unrouted asked only whether every realized layer was TOUCHED by some connection of its net, and said so in a rung note. A net on layers 0,1,2,3 joined 0-1 and 2-3 satisfied that and is two electrically separate conductors. It is now the real question: reachability from each realized layer, expanded to a fixpoint over the net's own connections, refusing unless every realized layer lands in one component. The iteration bound is the realization count, which is exact rather than a guess -- each pass adds an ordinal or the set is closed, and the set cannot exceed the realized layers. Asked from every realized layer rather than a chosen seed, so no sentinel head extraction is needed. Proven by sabotage: restoring the weak form turns w_two_islands_of_one_net_refuse FAIL while the bridged case still passes. 2. THE ADMITTED VALUE DROPPED THE CONNECTIONS IT JUDGED. admit_copper read the connection population to decide the verdict and returned only the realizations, so two different connection populations justified one admitted result and no renderer, DRC or projection could recover which joins made the split nets whole. AdmittedCopper is now a sole_constructor record carrying board, realizations and connections, minted at one admit_callers-sealed site. 3. AN ENDPOINT ON A LAYER THE NET DOES NOT OCCUPY ADMITTED. Every check a connection faced was about the layer -- does this board have it, does it belong to this stackup -- and none about the join. A VCC connection could terminate where no VCC copper exists. New counted refusal InterlayerConnectionEndpointHasNoConductor, naming net and ordinal. 4. IT WAS NOT A VIA. The object carries a net and two layer references and no coordinate, drill, annular ring, span, plating or keepout. Calling it Via invites a renderer to draw a hole no fabricator could build. Renamed InterlayerConnection throughout; ManufacturableVia is the later carrier once geometry is grounded. 19 witnesses PASS (4 new). Compile gate contributes no diagnostic naming any pcb file; the 41 pre-existing Empty diagnostics are in src/v2/lens/complexity_accumulator_copy/analyze.dag, untouched here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the duplicated match arm and the comment vias made false review 52813 (claude-opus-4-7): NetHasTwoConductorsOnOneLayer was written twice in one RED control - a copy-paste artifact the substrate accepted because a second arm for a variant already matched is unreachable rather than illegal. Deleted; 19 witnesses still pass. review 52810 (cursor): the comment above realizations_of_net still said a split net with vias was something this increment does not model, which InterlayerConnection makes false. Rewritten to say what the two refusals now separate: same-layer duplication is a fork, multi-layer presence is a connectivity question. 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>
…ing (#8358) Main is red on doc reachability and has been for four consecutive runs. Two distinct causes; this fixes the one that is decidable without guessing. DANGLING LINK 1 - a relative-path defect, not a missing file. docs/plans/effect-namespace-grants.md linked to docs/plans/node-subtree-visibility-grants.md, which EXISTS - but the link was written repo-root-relative from inside docs/plans, so it resolves to docs/plans/docs/plans/... and lands nowhere. Broken on GitHub too, for anyone who clicked it. Now relative to the file that carries it. DANGLING LINK 2 - a target no commit has ever added. docs/probes/root_b_primitive_repr_fork_2026-08-16.md, landed by #8337, cites docs/plans/self-host-cargo-refusal-root-partition.md. That path is in no commit in this repository. I did not invent the document and did not guess which existing plan was meant: the citation survives as text naming the plan and stating that the link pointed at a file which does not exist, so the intent is preserved and the false link is gone. If the plan exists under another name its author can restore the link in one edit. MEASURED: doc_graph_has_no_dangling_links goes FAIL to PASS. WHAT THIS DOES NOT FIX, stated rather than left for the next reader to rediscover: doc_graph_has_no_orphan_docs still fails. Two probe docs carry no HandAuthoredDocBind row in gunbc.doc_graph_roots - class_b_trim_pool_coincidence_receipt and root_b_primitive_repr_fork_2026-08-16. A bind row must name the .dag work the document binds to, which is a statement about whose evidence supports which declaration. Authoring that for another session's probe would be guessing at their modeling, so those two rows are owed by their authors rather than supplied here. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…re Name::Variant paths in pattern and nested-argument positions (#8351) * Root K: admit a parent-enum import from its authored variant, not from the parent's own spelling The emitter qualifies a variant by its parent (`Parent::Variant`) in patterns and nested constructions, at sites where the .dag source spells only the VARIANT. The authored-source gate inside `reference_derived_use_lines` asked whether the PARENT was spelled in the module, so every such parent's use-line was refused and the emitted `Parent::Variant` had no import — 109 of Root K's 132 sites. Measured, not assumed. Compiling `v2.lens.complexity_accumulator_copy.analyze` (86-file closure, gunbc built from this tree): - 7 distinct parent enums appear as qualified heads while the .dag source contains ZERO occurrences of any of their names. - Opening the gate outright admitted 6 of the 7 (EdgeLabel, NamedEdgeTargetLookup, NodeKind, LetBindingFact, Outcome, ParseSubtreeFind) — so collection was never the wall, the gate was — and ALSO admitted AuthoredTokenOrdinal and FiniteSet, neither of which the module references: exactly the fabrication class the gate exists to refuse. So the gate is not relaxed, the question is corrected. A parent-enum candidate is admitted when an authored VARIANT of that same enum is spelled, and only on the UNAMBIGUOUS binding: `derive_variant_to_enum` maps a variant shared by two enums to the empty string, so a homonym variant admits NEITHER enum rather than picking one. After: unimported qualified-head sites across that closure 56 -> 19 (31 -> 7 in the module itself), no file worse, and both fabricated names stay absent. Regen reaches a fixed point with no seed drift — v1 seed modules are HostNative import-bearing and receive [] from this pass, confirmed by execution. Residue, declared not hidden: a corpus-wide ambiguous variant leaves its parent unimported even where the emitter qualifies it from the scrutinee type, and a parent reached by neither its own spelling nor an unambiguous authored variant (measured: `Behavior`) stays unsynthesized. Both refuse rather than fabricate. Dissolve-on is the one the text gate already carries: derive use-lines from the module's bound-reference structure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Carry the rationale as an annotation, and re-check the fix with a two-arm artifact diff Two changes, neither altering emitter behaviour. DESIGN 4c: the two `data NAME_note: String` rows this change introduced are the misplaced form — a String declaration whose sole purpose is commentary. Both are converted to leading `//` blocks above the declarations they explain. Both paths are outside `prose_row_migration_scope` (checked against all 262 entries), so this was not forced by the gate; it is the form DESIGN asks for. The dated measurement moves out of the tree entirely and lives in the commit and PR, where it cannot rot. The variant-induced arm also stops minting a dissolution condition of its own: it dissolves with the text gate it corrects, on the trigger `reference_derived_authored_source_gate_note` already declares. RE-CHECK, prompted by a sibling lane's finding that a fix's removed output can be load-bearing for an unrelated consumer — a class no refusal-counting instrument can see, because nothing refuses. An error histogram cannot distinguish unmasking from new emission, so I diffed the emitted ARTIFACT across both arms at the same entry and the same commit (identical closure by construction — no module-count mismatch): use-lines added 33 use-lines removed (line grain) 4 names lost (name grain) 0 <- the 4 are the same lines rewritten with MORE names files whose NON-import body changed 0 glob variant clashes, 256 emitted enums 0 So the change is purely additive at name grain and touches nothing but imports. Unimported qualified-head sites stay at 19 (from 56), confirming the annotation conversion changed no emitted behaviour. regen --verify: regen_divergence_count=0. All five witness controls still PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Say what the gate now admits: the note described one arm while the code had two review 52768 (cursor/composer-2.5, REQUEST_CHANGES) found the typed carrier contradicting its own implementation. Verified: after Root K the gate decision is reference_derived_candidate_authored, a disjunction, while reference_derived_authored_source_gate_note still opened "only when the candidate name appears in this module's authored source text" — false as written — and the new annotation cited that note as its dissolution anchor, so the citation pointed at text denying the change. DESIGN section 3 stale-citation, in the carrier a reader consults to learn what the gate does. The note now states both attesting forms (direct spelling; variant-induced, where a unit-only enum is admitted by an unambiguously-binding spelled variant), the homonym refusal that makes the second arm fail-closed (derive_variant_to_enum maps a shared variant to the empty string, so it never equals the enum name), and the declared residue both arms still refuse. The AuthoredTokenOrdinal receipt gains the reason it cannot be readmitted: it is a record, not a unit-only enum -- verified against dag/std/occurrence_identity.dag rather than asserted. Also completes the sibling witness note, which named the direct predicate as "the" gate law. Not false, but incomplete in a live carrier -- the file a session greps to learn the surface, so it silently invited re-deriving an arm that already exists. It now scopes itself to the direct arm and points at the second witness. Asked the directive question separately from the mention grep: no plan carrier instructs anyone to extend the single-arm behavior. Receipts, by execution: 8 of 8 witnesses PASS across both files. regen fixed point confirmed the hard way -- regenerate, rebuild the seed from the new mirror, regenerate again, byte-identical (md5). Emitted delta is exactly one line, the note value, with no behavioral change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the residue class this gate cannot reach, measured rather than reasoned The residue clause added in 5678180 said the remaining sites are "refused by both arms." Two of the three residual enum heads are not refused — they never reach the arms. Behavior's variant Transform is spelled bare in a pattern position in an import-free module and binds unambiguously, so the variant-induced arm's preconditions hold, and no use-line is emitted anyway. Established by execution, not inference: forcing the gate to admit unconditionally, regenerating, rebuilding the seed, and re-emitting v2.lens.complexity_accumulator_copy.analyze still yields no Behavior use-line. The gate is a filter over a candidate set, so a name the collector never proposes cannot be admitted by any gate decision. The homonym explanation was checked and refuted first -- Transform, Loop and OpBitCast each belong to exactly one enum. That distinction matters because the two classes have different fixes and only one of them lives here. The clause now separates refused-here from never-reaching-here and points the remaining work upstream at the candidate producer, which is where the existing dissolve-on already aims. Pre-existing and unchanged by Root K: Behavior:: occurs 7 times in both the base and fix arms. No regression, and the probe was reverted before this commit -- the tree was clean, and this diff carries only the note. 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>
…d definition's arguments (~73 sites) — and an enrolled witness asserts the broken shape (#8350) * Stop discarding the TypeEnv at the applied-binding renderer, so the closed-alias peel can answer A reference to a zero-parameter alias reaches the emitter carrying the RESOLVED DEFINITION's type arguments as its children, while its authored spelling is still the alias name. A renderer that prints name-plus-children therefore emits ClosedCarrierAlias<ProbeQuantity, ProbeScale, ProbeMagnitude> for a Rust alias declared with no parameters at all -- E0107, "type alias takes 0 generic arguments but 3 were supplied". Four renderers already refuse that shape by asking the one peel authority rust_fn_sig_peel_closed_alias. render_rust_type_with_applied_binding is the fifth path and it was not missing the guard: it reaches render_rust_applied_type, which asks, and was answered with an EMPTY TypeEnv the function constructed inline, plus an empty_emit_graph_info() it handed to render_rust_type. An empty env resolves no binding, and the peel predicate returns false for "I could not look this up" exactly as for "this declaration has parameters" -- so the unanswerable case widened into the applied form instead of refusing. Every one of its twelve callers already held the TypeEnv it was throwing away. So this passes it through rather than adding a check: the peel authority stays the single authority and is simply told the truth. Measured with an instrumented seed on the minimal fixture: base="ClosedCarrierAlias" children=3 envbindings=0. The witness that covered this fixture asserted the broken shape and was green, so the defect had a defender. It now asserts the emitted declaration and the bare use site together and excludes the applied spelling, which is a pair that has to agree. The next rung is upstream and deliberately not taken here: an alias reference that preserved its AUTHORED arity would make the shape unwritable rather than refused, and then no renderer would need to ask. * Drop the trailing semicolon that made the new note an item-declaration parse error A .dag data declaration is terminated by the newline, not by a semicolon. The trailing ; put a second, empty item where the parser expected a declaration, so 05_emit_rust.dag stopped parsing at that point -- which is why the regen job reported 'expected item declaration', then 26 orphaned source annotations and three unresolved v1.compiler.emit_rust imports downstream of it. One cause, 29 diagnostics. * Regenerate the stage0 seed for the applied-binding env change Mechanical output of regen_stage0 over the edited .dag, not hand-written. One file changes, v1_compiler_emit_rust.rs, +34/-45: the twelve callers gain env.clone(), the signature gains the parameter, and the two inline empty TypeEnv literals collapse into it -- which is where the 45 deletions come from. Round 2 over the rebuilt seed produces a byte-identical diff to round 1, so the self-host fixed point settles in one round rather than oscillating. MEASURED, on the emitted closures rather than on the fixture alone: src/v2/lens/coverage.dag 39 applied-use sites -> 0 src/v2/compiler/03_ingest.dag 74 applied-use sites -> 1 The fixture now emits the declaration and the use site in agreement: pub type ClosedCarrierAlias = Rc<Root4AliasCarrier<ProbeQuantity, ProbeScale, ProbeMagnitude>>; pub fn witness(items: Rc<Vec<ClosedCarrierAlias>>) -> Rc<Vec<ClosedCarrierAlias>> THE ONE REMAINING SITE IS NOT CLOSED AND IS NOT THIS ROOT. std_integer.rs emits pub type PositiveInt = Rc<Nat<Magnitude>>; from type PositiveInt = Nat where gt_zero, where dag/std/nat.dag declares type Nat = CommutativeSemiring<Magnitude> with no parameters. Same symptom class, different cause: that path is render_rust_alias_rhs_type, which already holds a real env and asks alias_base_is_zero_param_decl -- so the failure is that the lookup does not find Nat under the resolved def_mod, and that predicate's Absent arm also answers false. The conflation is the same shape one layer over; the cause is module resolution across two same-named nat modules, which this change does not touch. Stated as located residue, not as a fix. --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
#8364) main at 8a346ec carries two HandAuthoredDocBind rows with home ProbeDoc and slug root_b_primitive_repr_fork_2026-08-16, so both derive the key probe/root_b_primitive_repr_fork_2026-08-16, hand_authored_key_collision_count is nonzero, and doc_graph_bind_identities_unique fails. main is red. Not a bad merge: two lanes independently authored a bind for the same document. 76d6435 (#8362) bound the probe; 8a346ec (#8333, mine) bound it again while landing the plan it cites. The rows are not identical, so the resolution is a content judgement rather than a dedupe. Deleted MINE and kept #8362's, which is the strictly more informative of the two: it names rust_seed_host_numeric_alias as an additional work, and its dissolution states the specific condition — RustCorpusRepr's two fused axes split into independent facts — where mine restated roughly the same idea with no second work and a looser trigger. That is also the condition eager-deer's Root B cut (#8357) is actually executing against, so the surviving row is the one a reader can act on. Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 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>
…ar arity from its single authority (#8341) * Root D receipt: E0107 generic-arity root-caused to the checkpoint-scalar arity strip Witness is registered as a Rust checkpoint scalar while std.types records arity 1, so every Witness<T> in type position loses its argument. Measured live on 06_translate and localised by probe-then-revert instrumentation of the generated emitter. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Root D half 2: delete the Witness checkpoint-scalar rows and derive scalar arity from its single authority extdeps.languages.rust.types carried { dag_name: Witness, target_type: Witness } and a lowercase twin. A TypeCheckpoint row states target SPELLING and cannot state arity, so membership of that table is read by v1.compiler.05_emit_rust rust_render_checkpoint_scalar_bare as the proposition 'arity 0 in Rust' — the E0109 phantom-param wall. Witness is the generic enum v2.std.witness.Witness<C>, arity 1 by std.types container_type_arity, so every Witness<T> in type position lost its argument and emitted as Rc<Witness>: rustc E0107 'missing generics for enum Witness'. Delete the rows, and consult the declared-arity authority before the strip so no leaf with declared arity can be classified a checkpoint scalar however the spelling table is later edited. Measured on src/v2/compiler/06_translate.dag, same route and same single entry on both sides: E0107 21 -> 17, the four Witness sites gone, every other error code identical. The dag/std/integer.dag closure is byte-identical, which is the collateral control. Witness: dag/test/claim/root_d_checkpoint_scalar_declared_arity_witness_test.dag — green with the change, red with the change reverted and the binary rebuilt. Receipt: docs/probes/root_d_generic_arity_2026-08-16.md Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Escape the braces in rust_checkpoint_scalar_arity_note so the emitted prose reads Present{false} Review 52707 caught it: an unescaped {false} inside a data String is a format placeholder, so the generated projection was a format!(...) call rendering 'Presentfalse'. Escaped as \{false\}; the regenerated extdeps_languages_rust_types.rs now carries a plain literal with no format! at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Add the two-arm artifact diff over the full 06_translate closure Per smart-ram-730's re-check: a per-code histogram cannot distinguish unmasking from newly introduced emission, and a defect's output can be load-bearing for an unrelated consumer. Diffing the emitted trees instead: 91 files both arms, 2 differ, 8 lines = the 4 targeted Witness sites and nothing else. Same entry both arms, so M is fixed by construction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Re-take the before-arm from a detached worktree at the merge-base SHA Section 9's arm was defended by chronology, which is an account rather than an audit: an emit reads the working tree, so an uncommitted edit leaves no trace a timestamp reveals. Re-taken from git worktree add --detach 5e1a73f, zero dirty tracked files, real compile output. Byte-identical to the original before-arm (0 files differ), same 2-file/8-line delta to the after arm, and the introduced construct Witness<T> is absent from the base arm — the WHAT read that a timestamp cannot give. Also records that the same include counts 1 -> 5 tree-wide against 0 -> 4 per-file, so scope is stated with the number. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bind the Root D probe receipt so it is not a doc-graph orphan docs/probes/root_d_generic_arity_2026-08-16.md was introduced by this PR with no inbound markdown link. The doc graph reaches documents only through `](...)` edges from ROADMAP.md / DESIGN.md / docs/runbooks/README.md plus the typed HandAuthoredDocBind extra roots, so a probe cited exclusively from `.dag` carrier prose -- which is how the three notes in this PR cite it -- is unreachable and `doc_graph_has_no_orphan_docs` reds. Discriminated by execution rather than by reading, because main currently carries an unrelated orphan that reds the SAME row name: this worktree does not contain that file at all, and the witness FAILS with the probe present and PASSES with it moved aside. The defect is this PR's, not the one inherited from main, and it is not an unrelated fix riding a single-seam PR. Bound at subject grain per the existing ProbeDoc precedent: primary_work is the guard this probe measures, additional_works the table whose rows it removed. The retirement names the identity-keying change that makes both halves the probe localises structurally unreachable, at which point row and probe delete together. doc_graph_has_no_orphan_docs, doc_graph_has_no_dangling_links, doc_graph_works_refs_carry_symbols, doc_graph_bind_identities_unique, doc_graph_hand_authored_slugs_not_registered and production_doc_binds_all_carry_a_retirement all PASS locally. 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>
…selects an observed key (#8334) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `fleet_multi_principal_probe` `modeled_fleet_automation_credential_identity` hashed the DECLARED material and stamped it onto every `PrincipalReachObservation`, so the receipt's `credential_identity` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- the same authority the hand-authored CI shell already compares against, so the model and that fragment cannot disagree about which key is expected. The membership test is space-delimited rather than a bare substring, so a fingerprint carrying the declared one as a prefix does not match. Exit 1 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. Options are derived from the locus, so an agent binding cannot be paired with identity-file options or the reverse, and the receipt names where the credential was held rather than leaving a reader to infer it from which function was called. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. 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> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. 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> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. 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> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. 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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
…8361) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `fleet_multi_principal_probe` `modeled_fleet_automation_credential_identity` hashed the DECLARED material and stamped it onto every `PrincipalReachObservation`, so the receipt's `credential_identity` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- the same authority the hand-authored CI shell already compares against, so the model and that fragment cannot disagree about which key is expected. The membership test is space-delimited rather than a bare substring, so a fingerprint carrying the declared one as a prefix does not match. Exit 1 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. Options are derived from the locus, so an agent binding cannot be paired with identity-file options or the reverse, and the receipt names where the credential was held rather than leaving a reader to infer it from which function was called. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. 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> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. 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> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. 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> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the systemd unit file so a Spark serving unit can become bytes SparkServingUserUnitSpec is typed fields and deliberately not systemd INI syntax. That left a gap rather than a decision: nothing could turn the spec into a file, so WriteUserUnitFile had no bytes to deliver and the unit member had nothing to be observed against. extdeps.systemd.unit_file models the format, cited to systemd.unit(5) and systemd.service(5). One directive type per section, so `ExecStart=` in [Unit] and `WantedBy=` in [Service] have no representation -- the misplacement class is structurally impossible rather than validated. The file is a record of three sections, so a transposed or duplicated section is likewise unwritable. extdeps.ollama.server_env owns OLLAMA_HOST / OLLAMA_MODELS. They previously appeared in the tree only inside a prose comment, so any consumer had to spell the literals itself -- a second authority for ollama's own names. gunbc.spark_serving_unit_render maps the spec onto that authority and is the single rendering, so the write side and the observe side cannot drift into two renderings of one spec and report a permanent MemberChanged against itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the two new extdeps modules in scope_carrier_paths The placement gate refused: a new dag/extdeps file must both declare extdeps_model_scope AND join scope_carrier_paths. Both modules already declared the scope; neither was rostered, and the frozen legacy manifest is not a landing state for a new file. 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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
…ly served it (#8344) * Delete the 27-row self-host frontier roster and the machinery that only served it Operator ruling: the frontier roster is either derived from live state or it does not exist. It was neither -- 27 hand-authored rows whose measurement fields were ordinary parameters, so a row that claimed execution measurement was indistinguishable from one that asserted it. It attracted readers, it misrouted them, and it produced nothing. This deletes it at the root rather than pruning it row by row. WHAT THE DELETION PROVED, which is the part worth reading. Every consumer that looked load-bearing turned out to consume an empty projection: crate layout appended compiler_frontier_emitter_produced_stage0_mod_basenames(), a fold admitting only EmitterProduced rows. All 27 were SeedRetained, so the term was [] at every call and no emitted byte changes. wet enrollment appended a roster fold whose own gate, falsifier_self_host_wet_template_only_holds, asserted that term had length zero. crate partition named the roster as a dissolution target for module exports the roster could not have supplied -- rows carried a path and a disposition and nothing else. So the roster's real dependents were its own census tests. Those, the promotion and authorization machinery, and the per-module probe survey go with it. WHAT SURVIVES AND WHERE IT WENT. Crate layout is a separate concept that was squatting in the frontier module; it moves to v2.compiler.self_host.stage0_crate_layout with the registration rows and projections that actually produced bytes. The producer/qualification vocabulary in emitter_producer_provenance survives at half its size -- the EmitterProducer x EmissionQualification axes, the realized closure carriers, the receipt and its single mint -- because its live consumers (candidate_generation, the direct rust door contract, the production qualification lens) never read a roster row. EVIDENCE, PER DESIGN 4b. Deleted witnesses fall in two classes and both are stated in the carriers rather than here. Green-by-construction: seven crate layout witnesses guarded by a disposition match whose EmitterProduced arm was unreachable, or comparing zero to zero. Subject-retired: the authorization forgery controls proved an unauthorized EmitterProduced disposition was unwritable, and that disposition no longer has a representation to forge. Two claims survived and keep their controls: a V2Emitter receipt cannot be minted with the seed emitter in its realized closure, and the generated crate layout artifact must match its registration rows. ONE CLAIM IS GENUINELY RETIRED RATHER THAN CLIMBED, said plainly. transition_parity_host_index_agrees_with_hand_rows redded when the derived module index and the hand-authored qualified-module rows disagreed. Deleting one side of a duality retires the parity claim; it does not discharge it. The surviving authority is the path-module binding index, and the crate-partition dissolve target now points there instead of at the roster. The frontier_probe_survey bin is removed with its .dag surface and transport. Justified per bin, not by a class sentence, because an earlier change deleted four bins on one blanket justification and was reverted for exactly that -- see the second-removal paragraph in gunbc.ci_release_bins. NOT DONE HERE, named rather than left to be found: the frontier_probe subsystem (frontier_probe, frontier_probe_types, assemble_detail and their tests) still stands. It is the adjacent weed -- its subject was per-module roster measurement -- but it has independent test consumers and deserves its own cut. The plan carriers written in the roster's vocabulary (wave2_prep_design, v2_self_hosting) are quarry now, not authority, and are not rewritten here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Follow the bin deletion through build.rs and the generated workflow The build failed in 39s because deleting src/bin/frontier_probe_survey.rs left two references to it standing: build.rs still declared a rerun-if-changed on the file, and .github/workflows/ci.yml still passed --bin frontier_probe_survey to the release build and then asserted the resulting artifact existed at four verify sites and one tar site. ci.yml is a generated artifact and the honest way to update it is to regenerate it from gunbc.ci_release_bins, which is where the pack row was already removed. `gunbc ci` cannot run in this container -- the shim panics reading ci_layer_roots.dag out of a temp workspace -- so the eight occurrences are removed by hand and the drift gate is the check: it compares ci.yml against `gunbc ci` output byte for byte, so if this hand edit is not exactly what the generator produces, CI says so. That is the intended instrument for this rather than a local claim I cannot make. Stated because it is the kind of thing worth noticing rather than routing around: a hand-edited generated artifact is only acceptable here because a byte-exact gate independently checks it in the same run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Fix the parse error my own note introduced: nested double quotes in a .dag string The retained-kernel test gate failed with four panics, all the same: for_each_parsed_module_binding could not parse dag/gunbc/ci_release_bins.dag. The per-bin justification I added there quoted the earlier blanket sentence verbatim -- not "a probe bin whose subject was cli_run" -- inside a double-quoted string, which terminated the string mid-prose and left the remainder as garbage tokens. Worth noticing rather than just fixing. The failure surfaced four modules away from its cause, in a materialization-provider test whose subject is disk cache probes, because the whole-corpus module-path index parses every .dag file before anything else runs. So a prose edit in a bin roster reds a cache test, and the panic names the parse site rather than the reader. That is the same ordering property this program spent the afternoon on: what breaks first is not what is wrong, it is what runs first. The sentence now paraphrases instead of quoting. Checked the other nine multi-paragraph notes this change adds: each opens and closes exactly once, with the odd per-line quote counts expected of a string spanning blank lines. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Two workflows still named the deleted probe bin: take the heal regeneration The frontier cut deleted the frontier_probe_survey bin and its row in the release pack, and I removed its eight occurrences from ci.yml by hand. fleet-converge.yml and falsifier.yml build the same pack from the same authority and still named it, so heal regenerated them and could not push workflow paths itself. These are its bytes, not mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Move the deletion rationale into an authored annotation: it is prose, not program data DESIGN 4c, enforced by prose_row_introduction_gate: this path's prose is already migrated, so a new data NAME_note: String row is refused. The note explains what the frontier cut removed from this module and what survived, which is exactly irreducible rationale about a construction's shape -- it belongs above the declaration it explains, not in a String the compiler must carry. Six sibling rows on out-of-scope paths were reported and not enforced; left as they are rather than widening the diff past the refusal. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Delete the freeze rows and transport claims naming witnesses the cut removed The floor refused with StaleFrozenPathDeferral: two gunbc.witness_deferral_freeze rows named test decls the entry no longer declares. A freeze row left behind is not inert -- it becomes a standing exemption the next witness to take that name inherits, which is the refusal's own wording and the reason it is loud. Same two names were still enrolled as ClaimRun rows in the supply transport, and its note explained why one of them was there. Removed both and rewrote the note to say what happened to their subjects: the parity witness had the duality between the derived index and the hand rows as its subject, and the cut removed one side, so the claim is retired rather than dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Import the equality helper from its definer: the old path resolved by pool coincidence emitter_producer_provenance_witness_test imported schedule_witness_entries_structurally_equal from wet_receipt_enrollment, which neither defines it nor imports it. It is defined in seed_emitter_behavioral_wet_known_red_entries, a module this file already imports. The reference resolved on main only because some other member of the assembled closure had dragged the definer into the pool; the cut changed the closure and it stopped resolving, refusing the whole discovery corpus. This is the Class B accidental-coverage shape DESIGN records as an open thread — a bare cross-module reference binding by pool membership rather than by the importing file's own closure. Importing from the definer is the fix that does not depend on who else is in the pool. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Retire the frontier probe receipts with the roster they measured The cut deleted the two HandAuthoredDocBind rows for the frontier probe receipts but left the documents in the tree, so three files lost their only inbound reachability and became orphans. Deleting the bind rows was correct — every declaration they cite (frontier_probe_exact_head_closeout_note, frontier_probe_run_interruption_note, frontier_roster_provenance_constructor_inflation_note, compiler_frontier_receipt_totality_wall_holds) is deleted by this PR, so the binds would otherwise dangle. What was missing is the other half: a document whose entire subject is retired is retired with it, never left standing. Deleted with the rows: docs/probes/frontier_probe_exact_head_survey_2026-08-03.{md,tsv} docs/probes/frontier_probe_run_interrupted_2026-08-06.md docs/probes/diff_frontier_declared_vs_survey.sh (only input was the TSV above) docs/probes/run_frontier_probe_survey_per_module.sh The two scripts are frontier-probe transport and served nothing else. Two unrelated STR-RC-0 scaffolds cited the second one as a class exemplar; their comments now state the class without the pointer, so the deletion leaves no stale citation behind. This is the branch's own doc-graph defect, distinct from the five inherited rows main is currently red on (the root_b probe orphan, fixed by #8333). Same lens, same five row names, two different causes — which is why "those are the known inherited rows" had to be checked rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Cut cleanup: the citations the deletion left pointing at nothing cursor review 52817 on #8344 named six stale citations to symbols and files this cut deletes. All six verified against the tree and fixed per site — a mechanical substitution across them produces sentences that parse and say nothing, which I did once already tonight and am not repeating. stage0_crate_layout_emit.dag the generated-artifact template still embedded 'Authority: v2.compiler.self_host.frontier' in both the .dag and .rs emit paths after the import was repointed, so the next regen would bake a deleted module name into two generated artifacts. Now names the real authority, v2.compiler.self_host.stage0_crate_layout. ci_layer_roots.dag witness_admission_offline_note dropped the deleted exclusion note from the paired list. ci_layer_roots.dag long_lane_exclusion_note dropped the 'Named consumer with file-grain exclusion row' sentence; both things it named are gone. ci_layer_roots.dag falsifier_self_host_wet_note the frontier-row flip no longer gates wet enrollment; says so, and points at the note recording that the term it fed was already empty. ci_release_bins_witness_test.dag note claimed two positive gap bins while the tests assert one. witness_deferral_freeze.dag the terminating-survey specimen is rewritten rather than removed: it did terminate, but by its subject being deleted rather than by reaching 27 of 27 receipts, and that is the disposition the freeze cannot express. Two more of the same class the review did not reach, found by sweeping every deleted symbol rather than fixing the six named: doc_graph_roots.dag the bind for this cut's own coordination document had primary_work pointing at v2.compiler.self_host.frontier_band_a_emit_readiness, a module this PR deletes. Repointed to the door-contract note already in its additional_works, which is the closest surviving subject. discrete_cost_derivation (.dag + .md) cited the deleted exclusion note as live evidence for the 'green CI implies coverage' claim. The claim stands; the specimen is now stated as one that has since been deleted with its subject, which is an instance of the pattern rather than a loss of it. Census after: every decl_name bound in doc_graph_roots resolves in the tree. An earlier run of that census reported two missing — both were my grep omitting 'func' declarations, not defects. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Cut cleanup 2: the deleted-MODULE citations the symbol sweep missed cursor review 52826. Two of its four findings were already fixed in 5921f90 (the emit template, the release-bins note); it ran on the older head. The other two are real, and they show the first sweep was keyed on the wrong thing: I swept deleted SYMBOLS, and a DeclarationRef names a MODULE PATH independently of whether the symbol it cites still exists somewhere. Sweeping module paths instead found three sites, one more than the review. stage0_rust_source_lifecycle_scaffold.dag hand_maintained_stage0_filenames_authority_ref still named v2.compiler.self_host.frontier while the import three hundred lines above had been repointed to stage0_crate_layout. Repointed. dissolution_migration_census.dag a NarrativeOnly residue row for a note in the deleted probe-survey module. Removed; the partition witness asserts sum-of-parts against the total rather than a literal count, so it stays true by construction. self_host_promotion_obligations.dag RE-HOMED rather than retired, and the distinction is the point. Both refs named the deleted frontier module, which made the bound trigger one that can NEVER fire — DeclarationAppears waiting on a module nobody will re-create is a permanently pending obligation wearing a checkable trigger, which is worse than an honest unbound one. The obligation itself survives the roster because it was never about the roster: the hazard is that a self-host promotion can be granted on evidence the v1 seed produced, and EmitterProducer still carries a V1SeedEmitter arm in v2.compiler.self_host.emitter_producer_provenance. So the subject moves there, the trigger keeps its declaration name and moves with it, and the 'n/27' framing — which really was roster-specific — is gone from the claim. Its witness needs no change: it asserts the bound and unbound arms stay distinguishable, and both still are. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Repoint two live references to the deleted frontier module cursor review 52843. Both name it as a LIVE authority, unlike the several prose sites that correctly say 'was carved out of' or 'was deleted with' — those stay, because a historical reference to a deleted thing is accurate. language_target_registry.dag Rust's TargetGovernedByContracts named the deleted module as its governing contract id. Repointed to v2.compiler.self_host.emit_coverage_frontier. Note that the row's own governing_contract_id_resolution_note explains this field carries a module name only because the real strategy authority lives in a private overlay and cannot be resolved from here — so the field is a stand-in either way, but a stand-in naming something that exists is strictly better than one naming something deleted. stage0_emit_plan.dag the disposition-authority note said the projection derives from the deleted roster's seed-retained facts. It derives from stage0_crate_layout's hand-maintained filename facts, which is where the carve-out put them. Deliberately NOT changed: cli_run.rs uses the string as a synthetic submodule name in a prefix-matching unit test. It tests string logic and never resolves the module, so it is not a stale citation — any name would do. My earlier sweeps missed both because they keyed on 'module_path:' fields and import lines. These are a contract_ids list element and prose. Third sweep form, and the one that should have been first: grep the bare module name in any syntactic position, then decide per site whether the reference is live or historical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Regenerate the artifacts the authority-string change restamps cursor review 52843's first finding, and the one with teeth: I changed the emit template's authority string without regenerating what it stamps, so the committed artifacts and the template disagreed and generated_artifact_drift_gate would have refused. Ran the real generator rather than hand-editing generated files: gunbc run --entry dag/tools/generated_artifact_gate.dag --function main_wet It rewrote two artifacts with the new authority — and .github/workflows/ci.yml, which is the part worth recording. The merge earlier took the ours side of ci.yml purely to obtain a tree that builds, on the stated plan that regen would overwrite it by construction. It did: the generator produced MAIN's AUTHORED_CONFLICTS line, not mine. So the hand-picked side was wrong and would have shipped a workflow that silently dropped main's change. That is exactly the failure the generated-artifact merge driver refuses in order to prevent, and the reason the rule is regenerate rather than resolve. Still owed and dispatched separately: gunbc_stage0_crate_layout_generated.rs carries the same string but is emitted by regen_stage0 rather than by this gate, so it needs the stage0 regeneration, not this one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Regenerate the last artifact carrying the old authority string gunbc_stage0_crate_layout_generated.rs is the emitted Rust OF the .dag row this PR changed, so it is owned by regen_stage0 rather than by the generated_artifact_gate that produced the previous commit. Ran regen_stage0: 144 files written, exactly one changed, and it is this one. That single-file result is the receipt that the earlier gate run had already covered everything else it owns. Both regeneration paths now agree with the template, so the drift gate and the regen job have nothing left to refuse on this string. Instrument note, recorded because it is the fourth of its kind tonight: the subject-presence greps I printed beside this run were mangled by nested quoting — the pattern's second word was taken as a filename, so both reported 0 with a 'No such file' line above them. The numbers were garbage. The run is still trustworthy, but on the strength of what regen CHANGED, not on the checks I attached to it. A broken check that prints a plausible 0 is worse than no check, and this is the same family as reading a truncated tail: absence manufactured by the instrument, read as a measurement. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Repoint to the right authority, and clear two more dissolution triggers cursor review 52854, both real. MY REPOINT WAS WRONG AND THE REASON IS THE ERROR I HAVE BEEN WARNING OTHERS ABOUT ALL NIGHT. I moved Rust's TargetGovernedByContracts to v2.compiler.self_host.emit_coverage_frontier because the name resembled the deleted module. It does not answer the same question: that carrier's own two-axis note says it answers axis (a), whether a witness body runs native, and explicitly disclaims axis (b), module self-emission. Picking it on name resemblance is precisely 18.2's finding — a name says the carrier was involved, not how — applied by me while citing it to someone else. Repointed to v2.compiler.self_host.emitter_producer_provenance, the surviving producer authority, which is also where the promotion obligation re-homed earlier in this PR. And the field's own note is updated: its stated purpose is a resolvable module a reader can open, so the note naming the deleted one made it false on its face while the field beside it had already moved. The note now records the wrong first choice rather than quietly showing the second — a reader deciding whether this field means anything is better served by knowing it was mis-picked once. seed_emitter_behavioral_wet_module_bindings carried two dissolution triggers whose subjects the cut removed: authorization waiting on 'witness-realization + frontier_probe_survey', and 'Frontier rows stay SeedRetained'. Both rewritten to name what actually remains — witness-realization alone, and the binding's own absence. A trigger naming a deleted subject cannot fire, which makes it strictly worse than honest prose. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Roadmap paths, and the plan carriers the cut decayed claude review 52858. The first finding is the serious one: STRUCTURED fields, not prose. THREE LIVE ROADMAP NODES pointed path: at the deleted file — v2-emitter- producer-provenance, v2-emitter-first-behavioral-module, v2-emitter-native- bootstrap, all active in gunbc.roadmap_authority. Repointed PER NODE from what each node says it does, not uniformly: producer-provenance -> emitter_producer_provenance.dag (its handback wants a result refused without a receipt from the run that made it — that module's mint wall) first-behavioral-module-> wet_receipt_enrollment.dag (handback is test results plus the updated list entry; the list entry was a roster row, and wet enrollment is what survived carrying per-module receipts) native-bootstrap -> v2_emitter_direct_rust_door_contract.dag (handback is two builds and the old compiler taken away) Picking one target for all three would have repeated the mistake in the commit before this one, where I chose emit_coverage_frontier because the name resembled the deleted module. Swept afterward: every path: in the roadmap now resolves on disk, the sole non-file being a dotted module reference. WAVE2_PREP_DESIGN IS MARKED SUPERSEDED RATHER THAN REPOINTED, and that is a disposition rather than a shortcut. Its entire mechanism section names the roster, its count, its baseline, its census attribution, its sweep order and its gate — all deleted. There is no mapping from a roster row to a replacement, so repointing eight symbols would fabricate an authority the document never had. DESIGN §3 rules that a plan authored while the deleted structure lived is re-read as quarry: its findings may be evidence, its sequencing is the old structure's gravity written down. The header now says so and tells the reader every symbol below names something gone. The other two plan carriers had specific enough claims to repoint per site. Residual live citations of the deleted module across all .dag: zero, counting only live references — the several prose sites that say 'was carved out of' or 'was deleted with' stay, because a historical reference to a deleted thing is accurate and sweeping those would be the mechanical substitution this PR has already had to undo once. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * The self-hosting tracker outlived its roster: declare the gap, do not refill it review 52867 caught v2_self_hosting.dag still presenting the deleted frontier.dag as the live roster carrier -- seven citations across the status line, the state-of-play census, two Wave 1 residual lists, the Wave 3 exit gate and the retirement condition. The claude review on the same head credited this file with quarry annotation it does not have, so the finding is real and the approval was wrong about it. Quarry-bannering it would be the wrong repair. wave2_prep_design earned that treatment because its whole mechanism section named deleted roster symbols with no surviving mapping; this file is the live sequencer for a program whose Wave 1 is still in flight. It is not superseded by the cut -- it merely cited what the cut removed. So: repoint to the surviving authorities, and where a claim was denominated by the roster, retire the fraction rather than re-author it. 0/27 and 27/27 both came from the same hand-authored row list, so both measured the roster's opinion of how many compiler modules exist. The substance survives (no module is self-emitted with a green equivalence receipt; every module must flip or be declared pinned-kernel) and is now stated qualitatively, with the derived denominator named as the first Wave 3 obligation. Restoring a count here would rebuild the weed inside the replacement, which is the failure DESIGN section 3 warns about by name. The frontier probe residuals are marked retired rather than outstanding: the survey never produced a receipt on any host including a dedicated runner, so its deletion costs machinery, not evidence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 --------- 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> Co-authored-by: gunbc-ci-auto-heal <bts53@scarletmail.rutgers.edu>
…easured (#8367) * Plan status: Root A landed, Root D half 1 has no live owner, Root B measured The status table said Root A was 'unknown; under challenge' after it merged, and named vivid-wren as owner of a Root D whose halves have different owners and different states. A shared coordination document that is stale about what landed sends the next reader at finished work — which happened to me tonight: I dispatched a duplicate work item for Root D half 1 off this table before finding PR #8350 already at the merge bar with its author's session archived. A LANDED, #8347 as c4e9cc9. 12.5's challenge was RIGHT, which is why what landed is not what 12.5 proposed: a fused-map split, not the coproduct-skip edit the retracted diagnosis pointed at. The skip is still there and still deliberate. Recorded with two receipts — the stage0 regeneration the first push missed, and the two regen runs that reported a perfect fixed point while compiling a tree that never contained the fix. D split by owner: half 2 landed; half 1 is #8350, at the merge bar, no live owner, shepherded here. B 18.3 adds smart-ibex's executed flip: 211->204 errors, 203->196 sites, 195 common / 8 removed / 1 added, containment 0-of-18 disjoint. The 43-site renderer-inconsistency reading and the +18 reassignment are RETRACTED — read off a different module's artifact, never reached a carrier. What survives is sharper than the retraction: the leaf name Nat denotes two different types under two module authorities, so a census pooled across modules is keyed on a name that is not unique over the population it pools. Key on resolved type identity, not the printed name, and let a site carry more than one root. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Root D half 1 landed too — bbb5213, minutes after the row was written The row said 'at the merge bar, no live owner, shepherded here'. It merged while this PR was open. Recording it rather than letting a status document be stale about a merge inside its own review window — which is the failure the PR exists to fix, and it would be a poor look for the fix to exhibit it. Its author's session was archived before it landed, so the merge is also the receipt that an ownerless PR at the bar does not need a new session, only someone watching for it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 * Strike the superseded instruction, and give half 2 its receipt cursor review 52846, both findings real. 12.5 said 'treat A as unpartitioned, not as diagnosed' immediately above the RESOLVED block this PR added, so the section told a skimming reader that landed work was still open. I appended a resolution without striking the claim it supersedes, which is the plan-ledger form of rung inflation — and doing it in the very PR whose purpose is status honesty. Struck rather than deleted: the instruction was correct when written, and the paragraph above it records WHY the then-current diagnosis was refused, which still governs. The Root D row claimed both halves landed while citing only half 1. Half 2 is 7cfeb6f (PR #8341), verified an ancestor of origin/main before citing it rather than copied from the review. Receipt added. Swept my own additions for the same class afterward: every LANDED claim in this diff now names a merge commit, and all four SHAs this document cites (bbb5213, 7cfeb6f, c4e9cc9, 6a3779d) are confirmed ancestors of origin/main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 --------- 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>
…s stays open (#8349) The rung line said the invalid state remains writable; it did not say WHAT remains writable. A missing use-site ownership catalog and an absent value-semantics bundle both refuse with a typed located diagnostic here, and a witness drives that arm. Absence-as-no-facts still has an arm at other ownership lookups, including a live v1 one that answers a miss with an empty set and no refusal — an under-wrap producer, and under-wrap is 28 of the 55. Closing the class means making ownership-absence unrepresentable, which is this row's next rung; widening refusal instead would add validations where construction is the answer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 17, 2026
It is an unrelated performance postmortem that accumulated here because I was on this branch without realizing it. It now lives on doc/reconcile-root-cause off main. This branch is parked on #8349 and should carry only the ownership cut.
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
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.
Two motions: locate R1's root against measured evidence, then build the construction the root asks for. Not doc-only — an earlier revision of this PR was, and this description said so; that is corrected here rather than left standing.
Diff: one amended section in
docs/plans/rc-ownership-wrap-decision-design.md;wrap_decision_flow_gateand its helpers insrc/v2/compiler/wrap_decision.dag; six witnesses insrc/v2/test/claim/wrap_decision_predicate_test.dag; fiveDeclarationRefrows added to the doc's existingHandAuthoredDocBindso the cited v1 symbols are bound rather than named in prose. No hand-Rust, no hand-shell.Part 1 — the root, and a correction to the lane's own problem statement
The design note says the fail-open is that the emitter wraps every
shared_typesmember. Measured, that is not what happens.The census emitter is frozen v1, not v2. Emitted files are named
v2_*because their source modules are v2.dagfiles. stage0 carriesv1_compiler_emit_rust.rsand nov2_compiler_translate.rs;build_shared_typesappears in exactly two stage0 files;cli_run.rsimportscrate::v1_compiler_emit_rustdirectly. Sowrap_decision_gatewas dormant while all 55 sites were produced. An earlier cross-lane inference joining the v2 catalog fork to these numbers is retired here.The root is a type-level fact consumed through occurrence-level keys.
build_shared_typescomputes membership once per type; three seams then consult it through properties of each occurrence's syntax, and no arm refuses —render_rust_shared_type_if_neededreturns the unwrapped rendering on a miss, silently.The inconsistency is narrow, and it is one defect producing both signs. Ten types, fourteen bare field occurrences, each wrapped at every signature occurrence and bare at one or more field occurrences, with zero bare signatures in the population. A signature returning
Rc<T>into a bare field is the over; a bare field into anRc<T>parameter is the under. One fix moves both counts; a position-based fix moves half and worsens half. Two independently produced trees agree type for type, count for count, line for line.Recorded as retired rather than deleted, because the next reader's cheapest hypotheses are exactly these: signature wraps, field does not (plain struct fields run 121 wrapped to 5 bare) and generic enclosing items force bare (refuted at 17/17 and 6/6). A first sweep also keyed only on outermost field types and missed element-position misses inside containers (
Rc<Vec<Finding>>); the published table is the corrected sweep.Witnessis excluded — 65 bare signature occurrences, a different root; admitting it would give the population a second mechanism.Part 2 — the construction
wrap_decision_flow_gatemakes the flow, not the position, the decided unit: it projectswrap_decision_gateat producer and consumer sites through the same authority and refuses — typed, located, naming the carrier — when that authority's answers for the two positions differ.wrap_decisions_equalcompares reference layers, not merely by-value against by-reference.Deliberately not a fifth
TargetOwnershipUseSiteinhabitant.OwnershipAtCallArgumentwould add a fifth position opinion to a defect whose cause is that every position already holds its own. This is also why 53 of 54 at call-argument position does not locate the defect: that is where rustc points; the cause is in the field declaration.Rung (§4b): silent wrongness → mitigatable. Not structural impossibility — the invalid state stays writable, since a catalog may still state different layers at two positions and the only answer here is refusal. Next rung is a modeled layer transition (
TargetValueExpressioncarrying its layer, plus a total raise/lower/refuse), which is a carrier change and is sequenced ahead of the pipeline edit rather than inside it. Not wired into06_translate— that is a separate motion with its own evidence.Evidence by execution, with a non-uniform mutation profile
Twelve witnesses green: six new, six pre-existing unregressed. Both directions come from the live rust catalog by varying only flow direction over
Diagnostics, whose rows already disagree by position.Two mutations were executed rather than a single RED asserted, and the profile is not uniform, so it is reported as measured:
wrap_decision_gates_agreeforcedtruewrap_decisions_equalmade layer-blindThe missing-row witness therefore does not discriminate this reconciliation — it is a propagation regression control, labelled as one rather than kept under the flattering name. The distinct-layer witness earns its place from mutation two:
RcagainstBoxis a real disagreement that a by-value-vs-by-reference comparison calls agreement, and every other witness passes under that bug.Disposition, and what is not claimed
Ruled (b) — specification for the v2 emitter, not a v1 repair. A bounded exception to the v1 freeze was refused and escalated to the operator rather than self-approved: §5 puts that verdict outside the diff and outside the manager. Declared cost of (b): the v1 image stays red on these sites, the burn-down is unmeasurable until the emitter flips, and the after-measurement is synthetic-control-only.
Not claimed: the 55-site census and its direction/position breakdown are smart-ibex-716's and have not been independently reproduced here — that needs the
cargo checkhalf, which was not run. The consistency sweep and the root are reproduced on a second instrument.One self-correction carried in the history rather than squashed away: the flow-gate note first said "never a second lookup". That is an overclaim — this is two traversals of one catalog, and what it rules out is a divergent authority, not a repeated read. The repeated read is a real cost shape, named with its trigger (the per-carrier policy carrier the next rung needs) rather than dismissed as small.
🤖 Generated with Claude Code