Repository navigation
Vias: what makes a net legitimately present on two layers, and the refusal that narrows because of it - #8331
Merged
Merged
Conversation
gunbai-bot
Bot
changed the title
Contributor
|
Fixed rather than left — review 52671 flagged it as cosmetic, and it is slightly more than that. The counted-causes policy means every distinct problem is reported. A net split across four layers with no via is one problem, not four; deriving the cause from the realization list emitted it once per realization, which is a duplicate wearing the policy. A reader counting causes would have seen four findings where one exists. The split cause now derives from Worth noting what the control was doing: it pinned 14 witnesses green by execution. — sent from zesty-heron-736 |
Contributor
|
Fixed — review 52678 found a real fail-open, and I confirmed it by execution before touching anything: How the hole opened, since the mechanism is the part worth keeping. Before vias, any net with more than one realization refused — which caught same-layer duplication by accident. The via increment replaced that with a via-reachability question, which asks only whether each realized layer is reached by a via of that net. Two rows on layer 0 are both on a layer the via reaches, so both passed. Narrowing a refusal is a deletion. It silently 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 exactly the ones no witness named. Same-layer duplication and cross-layer routing are different questions, so they are two causes now rather than one re-aimed at a narrower target. The cause carries the net and not the ordinal: naming which layer is duplicated needs a fold over distinct ordinals this increment does not build, and picking one would name a layer the model never established as the offender. Also hoisted a rationale comment that had been sitting inside a declaration body, which the substrate refused at module-item grain (DESIGN §4c) — worth noting only because it means the annotation rule is enforced, not advisory. 15 witnesses green by execution, 9 of them RED controls. — sent from zesty-heron-736 |
gunbai-bot
Bot
force-pushed
the
session/pcb-via
branch
from
August 16, 2026 23:01
16ce0ca to
5d7678c
Compare
…fusals 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.
gunbai-bot
Bot
force-pushed
the
session/pcb-via
branch
from
August 17, 2026 02:07
1f658a7 to
0da885c
Compare
|
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. |
Contributor
|
Status note, no code change. This branch's only red is the two doc-graph witnesses, and neither is caused by anything here — both fail identically on clean main. The dangling half is fixed by #8358 (two links repointed). The orphan half is docs/probes/root_b_primitive_repr_fork_2026-08-16.md, which landed on main with no inbound link. I checked whether to bind it myself and concluded I should not: the probe's own text names docs/plans/self-host-cargo-refusal-root-partition.md as its parent, that plan is carried by #8333, and inventing a different inbound link here would stand up a second authority for where the probe belongs that would have to be deleted when #8333 lands. So this PR unblocks when #8358 and #8333 are both in. Nothing further is owed from this branch. — sent from zesty-heron-736 |
… 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>
Contributor
|
Reworked despite the two approvals — four modeling defects, all confirmed against the code before touching it. Per the standing ruling that modeling accuracy outranks history, approvals do not settle whether the model is right.
19 witnesses pass, 4 new. Compile gate produces no diagnostic naming any pcb file. Separately: this branch's CI red is still the two doc-graph witnesses inherited from main, unrelated to anything here. — sent from zesty-heron-736 |
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>
briansrls
added a commit
that referenced
this pull request
Aug 17, 2026
… and refuse producer/consumer disagreement (#8349) * R1: locate the wrap-decision root at fourteen field occurrences, and 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> * R1: decide the flow, not the position — wrap_decision_flow_gate refuses 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> * Correct my own overclaim: two traversals of one catalog, not one lookup 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> * Move the two new rationale blocks from prose rows to authored // annotations 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> * Two-arm artifact diff: my prediction was wrong twice, and the excuse 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> * Retract an unsupported emission claim I made against my own receipt, 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> * Retract the reorder causal claim: the null produces the same two lines 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> * Record the order test's false-fire arm: it misreported this branch's 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> * Rest the reorder read on the unique-valued restriction, not the boilerplate 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> * Rest the reorder read on the diff-based instrument, which names the moved 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> * State why naming a mover is sound here: the two transposed groups are 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> * Ground the mover naming in the forward/reverse test, and mark it a wager (#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> * Stop citing the repeat count as a clearing argument; the flip rate is 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> * Complete the witness note's enumeration: it listed one surface and there 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> * Declare the census denominator incomplete by execution: +18 proven, 306 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> * Withdraw the +18 and the renderer-inconsistency reading; the 55 stands (#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> * Vias: what makes a net legitimately present on two layers, and the refusal 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> * Unbreak the doc graph's dangling half: two links that pointed at nothing (#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> * Root K: variant qualification without a use-line — 109 of 132 sites are 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> * Root D half 1: a zero-parameter alias is emitted carrying its resolved 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> * Doc graph: one bind per document — drop the duplicate Root B probe row (#8364) main at 8a346ec3 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. 76d64357 (#8362) bound the probe; 8a346ec3 (#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> * Root D half 2: delete the Witness checkpoint-scalar rows, derive scalar 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 5e1a73fa339, 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> * Materialize and read back the agent selector file, so IdentitiesOnly 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> * Model the systemd unit file so a Spark serving unit can become bytes (#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…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #8328. The copper lane's third carrier.
#8328 refused any net realized on more than one layer, because it had no way to tell a routed layer change from two conductors forking one name. A via is exactly that distinction — so this narrows the refusal rather than adding a second one beside it.
NetRealizedMoreThanOnceis deleted;NetSplitAcrossLayersWithoutAViareplaces it. The old variant is gone rather than left as a dead arm: a superseded refusal that still has a constructor is a second authority for one question.What the reference gives for free
Both via endpoints are
CopperLayerRefs, so a via inherits the stackup binding without its own check — it cannot join a layer of one board to a layer of another, and it cannot name an ordinal the board does not have.w_red_a_via_selected_against_another_stackup_is_refusedproves that inheritance rather than assuming it.What the reference cannot carry is the two endpoints being different, since that is a relation between two values rather than a property of either. So a via from a layer to itself is a checked refusal, and it reports the ordinal so the author knows which one.
The keystone
w_a_via_makes_a_split_net_admissibleasserts both directions in one run: the identical split realization refuses with no via and admits with one. Asserting only the admitting half would let a refusal that had quietly stopped firing read as success.w_red_a_via_on_another_net_does_not_route_this_oneis built so counting cannot pass it — same two layers, same number of vias, only the net identity differs.Declared, so the guarantee is not read as stronger than it is
Reachability is the weak form. Each realized layer must be touched by some via of that net; the vias are not required to connect those layers into one component. A net on layers 0, 1, 2, 3 with vias 0–1 and 2–3 satisfies this and is still two islands. Catching that is a connectivity fixpoint over the via graph, which this increment does not build. The rung note says so in the module.
Via geometry — drill diameter, annular ring, tented/plugged, blind and buried spans — is likewise absent. A via here is a connectivity fact, not yet a manufacturable feature.
Evidence
14 witnesses green by execution, 8 of them RED controls. The compile-clean gate reports only the three pre-existing
witness_import_closureerrors that #8326 fixes; none are in these files.Also drops an unused
NonEmptyStrimport that review 52667 noticed on #8328.