Repository navigation
SCM merge: a dependency-derived implication frontier, cut at the root - #8719
Merged
Merged
Conversation
Containment does not define interaction; dependency does. This lands the merge-specific implication vertical the SCM design note calls for, replacing an earlier slice whose operation had no target commit at all and therefore could only union bindings. THE ROOT CHANGED, so this is a replacement rather than a refinement (DESIGN section 3). The operation is now merge(store, target, target_dependencies, proposals): the target supplies every fact outside the frontier, and silence means PRESERVE IT. The prior shape merge(store, first, second) had nothing to preserve from, which is what forced the union. WHAT THE MODEL HOLDS - RequireBindingAbsent is an AUTHORED requirement. A dependency-derived frontier can decide whether removing f is compatible with its dependents, but it cannot express that the author asked for f to be absent. Modelling delete as the mere absence of a positive requirement would make it indistinguishable from silence -- and silence preserves -- so a delete by omission would read as "leave f alone", the exact inversion of the request. - Contains is retained for reconstruction and NEVER propagates. The live affected-set closure walks Contains in both directions, so an edit to f reaches its container and then every sibling -- the file model returning through the dependency lens. Here a child-body change never implicates its siblings. - Every other kind refuses by name (DependencyKindUnsupportedForMerge) instead of inheriting a reachability rule it was never validated against. Fifteen dependency kinds are not one closure algebra; widening the classifier is a deliberate act with its own controls. - Dependencies are role-grain, not node-grain. A replacement mints a new immutable node, so a target-read edge F1 -> K says nothing about F2. The binding ROLE is the bridge that survives the replacement, which keeps the question answerable without giving nodes a temporal identity they must not have. - A historical dependency is not eternal: a target row whose dependent was re-authored is superseded by the proposal's own rows, so retargeting k from f to h in one proposal lands. - validate_dependency only ever REFUSES; it never edits a role to repair a break. Affected is not modified -- a frontier that could rewrite its dependents would turn "g is affected by f" into permission to rewrite g. - The refusal is about an unsatisfied USE, not an illegal deletion. It carries the whole dependency (usage_site is the primary location, where the repair happens) plus the removal that made the source unavailable. Ten uses of f are ten located obligations, not one opaque "cannot delete", and it generalizes to replacement, where no deletion exists to blame. EVIDENCE -- 12 claims, all four classes falsified by mutation Contains propagates removal -> contains-no-propagate RED, controls green validator never refuses -> Arm B RED, Arm A green, edge-presence control RED source-insensitive refusal -> Arm A RED, Arm B green preservation rebuilt not reused -> both preservation claims RED The paired arms hold target, proposals, dependency kind, dependent, usage_site and row count FIXED and vary only which source the row requires (h survives, f is deleted). N2 and N3 are the pair's credential: each arm goes red under a different broken rule while the other stays green, so neither arm is decoration. TWO DEFECTS THIS RECEIPT FOUND IN ITS OWN TESTS, recorded because both were invisible to reading. Arm A originally carried an EMPTY dependency list, so an implementation that never read its dependency input passed it trivially -- the arm could not tell "no dependency" from "dependencies not consulted"; it now carries a real row, with a control proving that row is read. And the containment claim originally stated its row as dependent: f, which the proposal authored, so effective_dependencies discarded the row before validation -- the claim was green because its dependency was thrown away. Mutating Contains left it green, which is how the hole surfaced. Its annotation had already asserted it would go red; that sentence was false when written and is corrected in place.
merge.dag defined a local MergeDependencyKind whose arms -- DataDependsOn, BindsTo,
Contains -- were byte-identical to v2.std.dependency.DependencyKind's. That is the
section 3 nicknaming violation in its canonical form, the same shape DESIGN cites for
CpuArchitecture / TargetArchitecture: a second name for one concept, duplicated again in
everything derived from it.
The merge-specific fact was never the kind vocabulary. It is the CLASSIFIER -- which kinds
propagate a removal, which are supported at all -- so that is what this module now
contributes, over the shared kinds.
THE EXHAUSTIVE MATCH REPLACES A CATCH-ALL, which is why this is a strengthening rather than
a rename. The local enum carried UnsupportedKind { name: Symbol }: a stringly escape hatch
that would have silently absorbed any kind added upstream, under whatever name the caller
happened to pass. With the real coproduct, kind_propagates_removal and kind_is_supported are
total over 15 arms, so a sixteenth kind FAILS TO COMPILE here until merge states its policy
for it. "Every other kind refuses by name" stops being a route someone must remember and
becomes a property of the type -- validation replaced by construction.
The witness now names real kinds too: the unsupported-kind claim states PlacementDependsOn
and the edge-presence control states BarrierBefore, rather than invented probe names that
proved only that an invented arm behaved as invented.
All 12 claims green. This does not change any mutation receipt: the four falsifications are
over kind_propagates_removal, the validator, source sensitivity and preservation, none of
which changed shape.
These two files declared five top-level names that already exist elsewhere: ChoiceRequired gunbc.native_scm_interaction_contract (coproduct arm) CouldNotLand gunbc.native_scm_interaction_contract (coproduct arm) ApplyAcc dag/product/spatial_world.dag (type) bind v2.lens.cost.valuation_test (function) leaf v2.lens.complexity_lowering.loop_invariant_hoist_test (function) WHY THIS IS NOT A STYLE FIX. The resolver ADMITS duplicate top-level definitions and silently selects one with no diagnostic -- measured in #8707, with a control proving the instrument reaches the module and refuses correctly for a MISSING name, so the duplicates are admitted rather than merely unparsed. A top-level definition is corpus-wide, so `leaf` and `bind` were never local test helpers: they made the binding for those names arbitrary in any scope that holds both definitions. The witness floor builds one scope over ~3700 modules, and four claims in membership_reconcile_witness and tailscale_serve_route_key_witness failed there with "no field 'node' on type 'Node'" -- modules that import nothing from this change. That is what a corpus-wide name binding flipping looks like from the outside: the damage surfaces with no textual connection to its cause. THE ATTRIBUTION WAS ARITHMETIC, not a hypothesis. main at the branch point ran planned=9849 failed=0; this branch ran planned=9861 failed=4; 9849 + 12 claims = 9861 exactly, so both runs shared a base and these two files were the only variable. THE PREVIOUS COMMIT DID NOT FIX THIS, and predicting that it would was wrong. Consuming DependencyKind instead of forking it removed duplicate IMPORTED arm names and was correct on its own terms, but the breakage came from names this module DECLARES. CI refuted the prediction; the full scan that followed -- every type, arm and function name in both files checked against dag/ and src/v2 -- is what found the real five. WHAT IS NOT SETTLED, recorded rather than papered over: qualifying ChoiceRequired to MergeChoiceRequired removes the ambiguity without deciding whether the engine outcome and the contract's user-facing NativeScmPrimaryOutcome are the same two facts at two layers. They probably are, and one authority with a projection would be the section 3 answer. This change does not make that call. All 12 claims green; no mutation receipt is affected, since nothing but names changed.
Review flagged this as nit-tier. By DESIGN's own standard it is not: v2.std.dependency
already owns classify_dependency_kind<C>, and the three hand-written 15-arm matches here were
that function re-implemented three times over. "A fork always gets consolidated later, so it
is a correctness concern, not a style one."
It is also the SAME section 3 fork this module was corrected for once already, one layer
down. The first correction was at the VOCABULARY layer -- stop minting DataDependsOn beside
the real one. This is the DISPATCH layer -- stop re-walking the kinds that vocabulary
defines. What is genuinely merge-specific is the three POLICY VALUES; the walk from a kind to
its entry is upstream's.
THE ENFORCEMENT WAS THE WHOLE JUSTIFICATION FOR THE MATCHES, so it was measured rather than
assumed. Dropping one field from a classifier literal refuses, located and typed:
merge.dag:107:3: error: missing required field 'bootstrap_depends_on'
in literal of type 'DependencyKindClassifier'
A sixteenth kind adds a sixteenth field, so these literals fail to compile until merge states
its policy for it -- the same obligation the matches carried, now owed to one authority
instead of restated in three places. The refusal is arguably better than the non-exhaustive
match it replaces, since it names the missing field rather than the missing variant.
All 12 claims green. No mutation receipt is affected: the four falsifications are over
removal propagation, the validator, source sensitivity and preservation, and
kind_propagates_removal answers exactly as before -- only who performs the walk changed.
The 15 arm imports are dropped, since nothing in this module constructs an arm any more.
…not establish
Two corrections, both narrowing this module's claims to what it can actually support.
MergeCouldNotLand -> MergeRefused. "Could not land" asserts TERMINALITY, and the engine
cannot establish it. DependencyKindUnsupportedForMerge may mean this implementation has not
modeled the relation yet; TargetRootMissing may mean an incomplete fetch rather than a
permanently invalid target. Whether an engine refusal is terminal, machine-owned, or merely
awaiting more work is a decision ABOVE this module, so naming the arm for the terminal
conclusion is the same overclaim as a ledger reporting DONE for work that merely compiled.
MergeChoiceRequired now carries WHAT competed, not only WHERE. It held a bare role, which
locates the conflict and then discards its two causes -- both of which are in hand at the
moment of detection. That is the same information-loss defect as a usage_site that merely
duplicates its own dependent: every consumer must re-derive what the engine already knew, and
"which alternatives?" cannot be answered from a role at all.
type MergeChoiceEvidence { role: Symbol, held: RoleValue?, incoming: Requirement }
`held` is optional rather than asserted-present. The role IS resolved at that point, but
representing "not resolvable" honestly beats fabricating a value to satisfy totality.
WHAT IS DELIBERATELY NOT ADDED: a rendered question or a resumable continuation. Those need
audience authorization, stable resume identities, and proof the alternatives are materially
distinct -- none of which this layer holds. Manufacturing them here would fabricate evidence
one layer early, which is exactly why that projection belongs in a seam above the engine
rather than in the engine or in the presentation contract.
MEASURED, because a new field earns its place only if forgetting it can be detected:
forging `incoming` at the construction site turns one_role_authored_twice_asks RED
(forget_incoming_rc=1), and the restore returns it to green. The claim asserts the competing
PAIR, so an outcome that had forgotten what competed fails it. 12/12 green.
Caught by the harness rather than by reading: an earlier pass of this edit left one match arm
as MergeChoiceRequired { role: _ } => [], and all 12 claims went red uniformly. The restore
arm failing too is what identified it as a compile break in the edit rather than twelve logic
failures -- the diagnostic pointed at the type declaration, not the offending use site.
Contributor
Author
|
CI is red here for a defect on main, not in this PR. Third automated nag for the same external cause, so recording the evidence once. THE FAILURE, identical across all three of this branch's recent runs: That file is not in this diff. The floor REFUSES DURING PREPARATION on it, so no claim executes — this branch's witnesses are never reached, let alone failed. IT IS A SEMANTIC MERGE CONFLICT ON MAIN, and both contributing PRs were green: No textual conflict, and squash-merge without rebase means neither PR's CI ever compiled against the other. Main's own floor confirms it: 0336477 success at 04:45, then 73c62ca FAILURE at 05:23 — first red exactly at #8701. Still red at 2364f9a (2 arms declared against 4 variants). The fix is #8738, open. WHY I AM NOT PUSHING A FIX. The missing arms are a semantic decision in another lane's module: #8701 exists precisely because an origin advertising no ref is an ANSWER while a refused transport is the ABSENCE of one, and which arm licenses a WRITE is that lane's call. The two ways I could turn this branch green — guessing those arms, or adding a wildcard — are both worse than staying red. A wildcard would re-fuse the two states one level down and buy green by deleting the distinction #8701 was created to make. ONE THING IN THE LOG THAT IS NOT A FAILURE, since it names this module: STATUS OF THIS PR: five approvals, no outstanding findings, code complete. Twelve claims green locally with all four evidence classes falsified by mutation. One item stays UNVERIFIED and I am not marking it otherwise — whether the duplicate-top-level-name renames in d78879f clear the four earlier — sent from gentle-eagle-360 |
…arrival order Two correctness defects, both found by review rather than by me, and both in behaviour rather than naming. ONE: IDENTICAL AUTHORINGS WERE REPORTED AS A CHOICE. Two proposals that both require f = F, or both require f absent, AGREE. The old rule asked whenever a role was authored twice, so it fabricated a question whose alternatives were the same value -- the fabricated-plausible-output failure arriving through a refusal, which is the arm that looks safest. Its witness asserted the broad behaviour, so the defect was the contract rather than something the contract caught. That claim is DELETED, not amended: a test that enshrines wrong behaviour is worse than none, because it turns the bug into the specification and makes the repair look like a regression. TWO: THE CONTESTED EVIDENCE DEPENDED ON ARRIVAL ORDER. The fold stopped at the first competing authoring, so with A=F1, B=F2, C=F3 it reported (F1,F2) for one ordering and (F3,F2) for another. Both true, neither the fact, and order deciding which survives is exactly what this lane forbids -- a law this module ASSERTS a few lines away in root_node's annotation. I broke it in the one place a single run cannot reveal. Alternatives now accumulate over the whole population and the contest is reported after all of it has been seen. BOTH FIXES REST ON ONE MODELLING CHANGE. Neither Requirement nor RoleValue is the right comparison domain: a Requirement is AUTHORED SYNTAX and a RoleValue is RESULT PROVENANCE, and comparing across them cannot answer "is this the same request?" -- the only question that decides whether a contest exists. Both sides now normalize to DesiredRoleValue first. The conversion stays in the engine because normalizing a present binding stores the node and takes its ObjectId, which can itself collide; a seam doing that would duplicate this module's authority and redo its refusals. MergeChoiceRequired -> MergeRolesContested, the same correction as MergeRefused. That distinct alternatives EXIST is what this module establishes. That a USER must choose requires proving they survive the admitted equivalence quotient, that the population is closed, that no further machine work resolves them, and that they are authorized for presentation -- none of it here. The engine can establish that two requests name the same object; it deliberately does NOT claim two different objects are MATERIALLY different. held is gone rather than made optional. It was RoleValue? on the reasoning that the role is always resolved at that point -- which makes the optionality dishonest: it represents no real domain possibility and weakens an invariant. The authored state now structurally carries the alternatives, so "authored but no alternative" is unrepresentable instead of tolerated. MEASURED, 15/15 green, both defects falsified: treat any second authoring as a contest -> both agreement claims RED, real contest green stop at the first competitor -> accumulation claim RED, restore green The three new claims exist because the deleted one could not distinguish these cases. An earlier pass of this edit had a parse error and ALL 15 went red; the two mutation results that run reported looked exactly like the predicted reds and were void, since every claim was red before any mutation applied. The baseline sweep in the harness is what caught it -- a mutation receipt read without a green baseline is not a receipt. NOT ADDED, deliberately: per-alternative provenance (which proposal authored it). The seam needs it for amendment continuations, but it is seam-shaped work and faking an ordinal here would be inventing evidence one layer early. Recorded as the next slice.
The floor refused: "source annotation sits inside a declaration body. Only module-item grain is modeled." I put a // block inside a let binding in apply_requirement. DESIGN 4c admits only standalone leading blocks attached to module-scope declarations; body forms refuse until separately modeled. The rationale is unchanged, just hoisted to the function's own annotation. WORTH RECORDING, because it is why this cost a CI round trip rather than a local one: the 15-claim verification ran GREEN through `gunbc run` WITH the body annotation present. The interpreter admits what the floor refuses -- same source, two acceptance paths, two verdicts. That is exactly the per-path distinction DESIGN 4b insists on, appearing as a live gap rather than a doc principle, and it means a local green does not imply the floor accepts the file. Every "N/N green" in this branch's history carries that caveat. The floor is the stricter path so the class is caught rather than missed, but the cheap check is a grep for indented // before pushing, which now reports zero in both files. 15/15 still green after the move.
briansrls
pushed a commit
that referenced
this pull request
Aug 21, 2026
…io corpus (#8794) Two corrections to the design note, both about it being an authority that had stopped describing reality. SECTION 7 SPECIFIED AN OPERATION NOBODY CAN INVOKE. It read merge(store, first, second) -> Merged | ChoiceRequired | CouldNotLand. What shipped in #8719 is merge(store, target, target_dependencies, proposals) -> Merged | MergeRolesContested | MergeRefused. A stale authority is not a cosmetic problem: it is the premise contamination DESIGN records against its own CI paragraph, where a session planned an afternoon against a command that did not exist. Rewritten to the shipped signature, with the reasoning that produced it -- why the target arrived (the two-proposal form had nothing to preserve FROM, so it could only union bindings, which ships a program referencing a deleted node), why proposals became a list (a contest is a property of the population, not of a pair), and why both outcome arms are named for less than they conclude. SECTION 8 SAID "no merge kernel should be built without these" AND A KERNEL WAS BUILT. The honest thing is to state which of the thirteen it answers rather than let a reader assume. Measured by joining the 15 witness claims against the rows one at a time: FOUR ARE COVERED. The table now carries a blocked-on column, because "uncovered" was collapsing three different situations: 4 gaps sub-node recursion (the headline win; the kernel cannot express them) 3 gaps rename/move vocabulary the model does not have at all 2 gaps positional merge, an explicit non-goal of this slice 1 gap CLOSABLE NOW at the current grain -- duplicate named siblings That last one is the useful find. Measured: nothing in gunbc.scm.* or v2.std.node refuses a node carrying two children under one name, and the nearest live behaviour is content-hash canonicalization SORTING named edges, which orders duplicates rather than refusing them. It is the only structural scenario needing neither new grain nor new vocabulary. My earlier estimate from reading was "roughly five", close enough to feel safe and wrong enough to have mis-scoped the next slice. The note now says coverage claims must be measured. DIRECTION RECORDED: a CLI vertical before the depth recursion, reversing the note's own "headline win is the next slice" ordering. The reason is DESIGN section 5 rather than a change of view about value -- nothing has ever CONSUMED this kernel, and a witness suite authored alongside the code is not a consumer. Safe to reorder because depth changes how merge combines, not how add authors. The cost is designed for rather than discovered: a CLI makes the top-level-binding limit user-visible, and that refusal must say so plainly instead of reading as a defect. Co-authored-by: gunbc-ci-auto-heal <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Containment does not define interaction; dependency does. This lands the merge-specific implication vertical the SCM design note calls for.
Why this replaces rather than refines
The prior slice's operation was
merge(store, first, second)— no target commit. With nothing to preserve from, the only thing it could do with two proposals was union their bindings, which is neither a closed-scope reading nor a dependency model. The root shape was the defect, so this cuts at the root (DESIGN §3): the operation is nowThe target supplies every fact outside the frontier, and silence means preserve it.
The model
RequireBindingAbsentis an authored requirement. A frontier can decide whether removingfis compatible with its dependents; it cannot express that the author asked forfto be absent. Modelling delete as the absence of a positive requirement would make it indistinguishable from silence — and silence preserves — so delete-by-omission would read as "leavefalone", the exact inversion.Containsnever propagates. The live affected-set closure walksContainsin both directions, so editingfreaches its container and then every sibling — the file model returning through the dependency lens.F1 → Ksays nothing aboutF2. The role is the bridge that survives, which avoids giving nodes a temporal identity.validate_dependencyonly refuses, never edits. Affected ≠ modified.usage_site(where the repair happens), citing the removal as cause. Ten uses are ten located obligations, and it generalizes to replacement, where no deletion exists to blame.Evidence — 12 claims, four mutations
ContainspropagatesThe paired arms hold target, proposals, kind, dependent,
usage_siteand row count fixed, varying only which source the row requires. Mutations 2 and 3 are the credential: each arm goes red under a different broken rule while the other stays green, so neither arm is decoration.Two defects this receipt found in its own tests
Both were invisible to reading, and both are the same shape — an observation structurally incapable of producing the negative.
dependent: f, which the proposal authored — soeffective_dependenciesdiscarded it before validation. The claim was green because its dependency was thrown away. MutatingContainsleft it green, which is how the hole surfaced. Its annotation had already asserted it would go red; that sentence was false when written and is corrected in place.Rung
Mechanically preventable. The rules are ordinary code and the claims are what refuse a wrong edit. No structural guarantee is claimed: nothing here makes a container-propagating classifier unwritable.