From 7ccfe27062cd9cda50ceaa1f1ebabf5097eceb03 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 16:23:30 +0000 Subject: [PATCH 1/7] SCM: the three-way manifest decision, kept one law by widening its operand The four-line three-way law -- S==B takes T, T==B takes S, S==T takes either, else conflict -- silently assumes all three sides HAVE the path. B, S and T each independently may not, which is eight states rather than four. THE CONCLUSION DRAWN FROM THAT WAS WRONG THE FIRST TIME AND IS RECORDED HERE BECAUSE THE CORRECTION IS THE DESIGN. I proposed enumerating the eight cases. What the discovery actually falsifies is BARE-LOCATOR OPERANDS, not the law. Widening the operand to PathState = PathAbsent | PathPresent { source: AuthoredSourceTarget } whose equality INCLUDES ABSENCE keeps the four lines total, and every presence case falls out as a consequence rather than a rule: source-deleted, both-deleted, source-added, both-added-identically, target-deleted, and both-added-differently. An eight-case implementation would have duplicated one algebra across presence combinations and let the copies drift -- decompress and map without the reduce, which is the redundancy DESIGN section 2 names. DELETE-VERSUS-MODIFY AND MODIFY-VERSUS-DELETE ARE THE POINT. They are the resurrection class of gunbc.scm.merge_base one layer down, at PATH grain rather than LINEAGE grain: taking the deletion silently discards an edit, taking the edit silently resurrects a file the other side deleted on purpose. Both produce a valid manifest and neither is visible to the caller. The law refuses them with no clause of its own -- there is simply no equality to appeal to. THE CONFLICT CARRIES ALL THREE STATES INCLUDING EXPLICIT ABSENCE. A deletion reported as a sentinel or fabricated locator would collapse absence back into a malformed-content representation -- the exact conflation the operand was widened to remove, reintroduced in the value that REPORTS it. No entries on the conflicted arm: a partial manifest beside a conflict list invites a caller to actuate the non-conflicting prefix, a corpus neither author wrote. And the conflict population is COMPLETE rather than first-wins, because fix-one, re-run, discover-another hides the size of the job -- each round individually honest, the sequence not. EVIDENCE. 442/0 across all SCM witness files, up from 435. Three mutations, each reding a DIFFERENT combination, so no claim duplicates another: mutation presence del/mod mod/del complete union bare-locator equality RED RED RED RED -- first-wins conflicts pass pass -- RED -- base-keyed subject RED -- -- pass RED as built pass pass pass pass pass One prediction of mine was wrong and is recorded rather than quietly dropped: I expected the complete-population claim to red under the base-keyed mutation. It does not, because all three of its paths exist in the base. Harmless -- that mutation is caught twice over -- but the wrong prediction is only visible because it was stated before the run. The three-source fixture is load-bearing, not spare: with two sources, any path where source and target disagree has one of them equal to the base, which the law RESOLVES instead of refusing, so an all-three-differ conflict is inexpressible. The first writing of the complete-population claim had exactly that defect -- intended two conflicting paths and built one -- and the claim caught it. The S==T arm returns one operand, and that the choice is unobservable is asserted by a claim rather than assumed. "They are equal so it does not matter" is the shape of reasoning that hid the root-versus-occurrence defect one module over. NOT IN THIS CUT: composing base derivation, manifest storage and the target-child mint into a merge verb. Both halves now exist and refuse independently. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/scm/manifest_merge.dag | 227 ++++++++++++++++++ .../scm/scm_manifest_merge_witness_test.dag | 221 +++++++++++++++++ 2 files changed, 448 insertions(+) create mode 100644 dag/gunbc/scm/manifest_merge.dag create mode 100644 dag/test/claim/scm/scm_manifest_merge_witness_test.dag diff --git a/dag/gunbc/scm/manifest_merge.dag b/dag/gunbc/scm/manifest_merge.dag new file mode 100644 index 00000000000..c5ffec90468 --- /dev/null +++ b/dag/gunbc/scm/manifest_merge.dag @@ -0,0 +1,227 @@ +module gunbc.scm.manifest_merge + +// THE THREE-WAY DECISION OVER ONE CORPUS MANIFEST, AND THE OPERAND IS WHAT MAKES IT ONE LAW. +// +// THE LAW ITSELF IS FOUR LINES AND DOES NOT GROW: +// +// S == B -> take T the source did not touch this path +// T == B -> take S the target did not touch this path +// S == T -> take either both arrived at the same state +// else -> CONFLICT +// +// WHAT MAKES IT TOTAL IS THAT THE OPERAND CARRIES PRESENCE. A first derivation of this module read +// the three sides as authored-source LOCATORS and then discovered that the law silently assumes all +// three sides HAVE the path -- B, S and T each independently may not, which is eight states, not +// four. The conclusion drawn from that was wrong: it proposed enumerating the eight. What the +// discovery actually falsifies is BARE-LOCATOR OPERANDS, not the law. Widening the operand to a +// PathState whose equality INCLUDES ABSENCE keeps the four lines total and yields every presence +// case as a consequence rather than as a separate rule: +// +// B=Present(X) S=Absent T=Present(X) -> S==T? no. T==B yes -> take S -> DELETED +// B=Present(X) S=Absent T=Absent -> S==T yes -> DELETED +// B=Absent S=Present(Y) T=Absent -> T==B yes -> take S -> ADDED +// B=Absent S=Present(Y) T=Present(Y) -> S==T yes -> ADDED +// B=Present(X) S=Absent T=Present(Y) -> no arm -> CONFLICT delete vs modify +// B=Present(X) S=Present(Y) T=Absent -> no arm -> CONFLICT modify vs delete +// +// THE LAST TWO ARE THE ONES THIS MODULE EXISTS TO GET RIGHT, and they are the resurrection class of +// gunbc.scm.merge_base one layer down -- at PATH grain rather than LINEAGE grain. Taking the deletion +// silently discards an edit; taking the edit silently resurrects a file the other side deleted on +// purpose. Neither is a conflict a user could see, and both produce a valid manifest. So the law must +// refuse rather than pick a side, and it does so with no clause of its own: there is simply no +// equality to appeal to. +// +// AN EIGHT-CASE IMPLEMENTATION WOULD HAVE BEEN THE REDUNDANCY DESIGN section 2 NAMES. It duplicates +// one algebra across presence combinations, and the copies are then free to drift -- decompress and +// map without the reduce. + +import std.types { Bool, List, String, NonEmptyStr } +import gunbc.scm.object_store { + AuthoredSourceTarget, + CorpusManifestEntry, + canonical_manifest_entries, + object_id_eq, +} + +// PRESENCE IS A STATE OF THE PATH, NOT AN OPTIONAL AROUND A LOCATOR, and the difference is that this +// type's equality is total over both arms. An `AuthoredSourceTarget?` would make absence a property +// of the CARRIER rather than a state of the subject, and every comparison would then have to unwrap +// before it could decide -- which is precisely where the four-line law was losing the deletion cases. +type PathState + = PathAbsent + | PathPresent { source: AuthoredSourceTarget } + +fn path_state_eq(left: PathState, right: PathState) -> Bool { + match left { + PathAbsent => + match right { + PathAbsent => true + PathPresent { source: _ } => false + } + PathPresent { source: l } => + match right { + PathAbsent => false + PathPresent { source: r } => object_id_eq(left: l.locator, right: r.locator) + } + } +} + +// A manifest holds at most one entry per path -- store_corpus_manifest refuses a duplicate before an +// identity is derived -- so the first match is THE match and no ambiguity rule is needed here. That +// is a property of the carrier this reads, not an assumption this module makes. +fn path_state_in(entries: List, path: String) -> PathState { + fold(entries, init: PathAbsent, f: fn(found, e) { + match found { + PathPresent { source: _ } => found + PathAbsent => + if (e.path as String) == path { + PathPresent { source: e.source } + } else { + found + } + } + }) +} + +// THE CONFLICT CARRIES ALL THREE STATES, INCLUDING EXPLICIT ABSENCE, AND THAT IS NOT DIAGNOSTIC +// GARNISH. A deletion reported as some sentinel or fabricated locator would collapse absence back +// into a malformed-content representation -- the exact presence/content conflation the operand was +// widened to remove, reintroduced in the value that REPORTS it. The diagnostic has to preserve the +// distinction the law decided on, or a reader of the conflict cannot reconstruct why it conflicted. +type ManifestPathConflict { + path: NonEmptyStr + base: PathState + source: PathState + target: PathState +} + +// NO MERGED ENTRIES ON THE CONFLICTED ARM. A partial manifest beside a conflict list invites a caller +// to actuate the non-conflicting prefix, which is a corpus neither author wrote; and a caller that +// did so would have a well-formed manifest with no record that anything was withheld. +// +// THE CONFLICT POPULATION IS COMPLETE, NOT FIRST-WINS. Reporting one conflict at a time hides the +// size of the job: a user fixes, re-runs, discovers another, and cannot tell after any single round +// whether they are near the end. That is the absorbing shape in slow motion -- each round is +// individually honest and the sequence is not. +type ManifestMergeOutcome + = ManifestMerged { entries: List } + | ManifestConflicted { conflicts: List } + +type MergeAcc { + entries: List + conflicts: List +} + +// THE DECISION LAW. Every arm below is one of the four lines; there is no presence clause, because +// `path_state_eq` already answers for absence. +fn merge_path( + acc: MergeAcc, + path: NonEmptyStr, + base: PathState, + source: PathState, + target: PathState, +) -> MergeAcc { + if path_state_eq(left: source, right: base) { + admit_state(acc: acc, path: path, state: target) + } else if path_state_eq(left: target, right: base) { + admit_state(acc: acc, path: path, state: source) + } else if path_state_eq(left: source, right: target) { + admit_state(acc: acc, path: path, state: source) + } else { + MergeAcc { + entries: acc.entries, + conflicts: concat( + [ManifestPathConflict { path: path, base: base, source: source, target: target }], + acc.conflicts + ), + } + } +} + +// AN ADMITTED ABSENCE WRITES NO ENTRY, which is how a deletion is represented in a manifest: the path +// is simply not in it. Writing an entry that means "deleted" would be a second representation of +// absence beside the one the manifest already has. +fn admit_state(acc: MergeAcc, path: NonEmptyStr, state: PathState) -> MergeAcc { + match state { + PathAbsent => acc + PathPresent { source: s } => + MergeAcc { + entries: concat([CorpusManifestEntry { path: path, source: s }], acc.entries), + conflicts: acc.conflicts, + } + } +} + +// THE SUBJECT IS THE UNION OF THE THREE SIDES' PATHS, because a path present on any side is a path +// the merge must decide. Taking the base's paths alone would silently drop every addition; taking the +// target's would silently drop every source addition. +// +// THE UNION IS DERIVED THROUGH THE MANIFEST'S OWN CANONICAL ORDER rather than through an order this +// module invents, so the conflict population and the merged entries are both reported in the order +// the carrier already uses. Deduplication is against the IMMEDIATELY PRECEDING path and not against +// every earlier one -- the quadratic scan a membership test would need is bought by the sort that has +// already happened, which is the same trade `a_duplicated_manifest_path` makes one module over. +type PathUnionAcc { + previous: String? + paths: List +} + +fn path_union_step(acc: PathUnionAcc, entry: CorpusManifestEntry) -> PathUnionAcc { + match acc.previous { + Present { value: p } => + if p == (entry.path as String) { + acc + } else { + PathUnionAcc { + previous: Present { value: entry.path as String }, + paths: concat([entry.path], acc.paths), + } + } + Absent => + PathUnionAcc { + previous: Present { value: entry.path as String }, + paths: concat([entry.path], acc.paths), + } + } +} + +fn merged_path_union( + base: List, + source: List, + target: List, +) -> List { + reverse( + fold( + canonical_manifest_entries(entries: concat(base, concat(source, target))), + init: PathUnionAcc { previous: none, paths: [] }, + f: fn(acc, e) { path_union_step(acc: acc, entry: e) }, + ).paths + ) +} + +// THE CONFLICT CHECK IS ON THE POPULATION, NOT ON A FLAG. A Bool set beside the accumulator would be +// a second authority for "did anything conflict", free to disagree with the list it describes. +fn merge_manifests( + base: List, + source: List, + target: List, +) -> ManifestMergeOutcome { + let decided = fold( + merged_path_union(base: base, source: source, target: target), + init: MergeAcc { entries: [], conflicts: [] }, + f: fn(acc, path) { + merge_path( + acc: acc, + path: path, + base: path_state_in(entries: base, path: path as String), + source: path_state_in(entries: source, path: path as String), + target: path_state_in(entries: target, path: path as String), + ) + }, + ) + if count(decided.conflicts) > 0 { + ManifestConflicted { conflicts: reverse(decided.conflicts) } + } else { + ManifestMerged { entries: reverse(decided.entries) } + } +} diff --git a/dag/test/claim/scm/scm_manifest_merge_witness_test.dag b/dag/test/claim/scm/scm_manifest_merge_witness_test.dag new file mode 100644 index 00000000000..61104969be7 --- /dev/null +++ b/dag/test/claim/scm/scm_manifest_merge_witness_test.dag @@ -0,0 +1,221 @@ +module test.claim.scm_manifest_merge_witness + +// CONTROLS FOR THE THREE-WAY DECISION, WRITTEN TO THE CASES A FOUR-LINE LAW OVER BARE LOCATORS GETS +// WRONG. Every wrong implementation here returns a VALID MANIFEST, so a control asserting "a manifest +// came back" discriminates nothing; each claim states the mutation it refutes. + +import std.types { Bool, String, List, NonEmptyStr } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.scm.object_store { + ObjectStore, ObjectId, empty_store, object_id_eq, + CorpusManifestEntry, AuthoredSourceTarget, + SourceStored, SourceLocatorCollision, store_authored_source, +} +import gunbc.scm.manifest_merge { + PathState, PathAbsent, PathPresent, path_state_eq, + ManifestPathConflict, + ManifestMergeOutcome, ManifestMerged, ManifestConflicted, + merge_manifests, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// TWO DISTINCT AUTHORED SOURCES, DERIVED THROUGH THE STORE rather than by naming digests, so the +// specimens are locators the store actually produces. A fixture that invented an ObjectId would be +// asserting over a value no producer makes. +// THREE DISTINCT SOURCES, NOT TWO, AND THE THIRD IS LOAD-BEARING RATHER THAN SPARE. A two-source +// fixture cannot express "base, source and target all differ at one path": with only x and y, any +// path where source and target disagree has one of them equal to the base, which the law resolves +// instead of refusing. The first writing of the complete-population claim below had exactly that +// defect -- it intended two conflicting paths and built one, and the claim caught it. +type Trio + = Trio { x: AuthoredSourceTarget, y: AuthoredSourceTarget, z: AuthoredSourceTarget } + | TrioUnavailable + +fn pair() -> Trio { + match store_authored_source(store: empty_store(), text: "X") { + SourceLocatorCollision { identity: _, existing: _, incoming: _ } => TrioUnavailable + SourceStored { store: s1, source: x } => + match store_authored_source(store: s1, text: "Y") { + SourceLocatorCollision { identity: _, existing: _, incoming: _ } => TrioUnavailable + SourceStored { store: s2, source: y } => + match store_authored_source(store: s2, text: "Z") { + SourceLocatorCollision { identity: _, existing: _, incoming: _ } => TrioUnavailable + SourceStored { store: _, source: z } => + Trio { + x: AuthoredSourceTarget { locator: x.locator }, + y: AuthoredSourceTarget { locator: y.locator }, + z: AuthoredSourceTarget { locator: z.locator }, + } + } + } + } +} + +fn at(path: String, source: AuthoredSourceTarget) -> List { + [CorpusManifestEntry { path: path as NonEmptyStr, source: source }] +} + +fn entries_hold(entries: List, path: String, source: AuthoredSourceTarget) -> Bool { + count(entries) == 1 + && fold(entries, init: false, f: fn(found, e) { + found || ((e.path as String) == path && object_id_eq(left: e.source.locator, right: source.locator)) + }) +} + +// THE SIX PRESENCE CASES, ASSERTED AS ONE CLAIM BECAUSE THEY ARE ONE LAW. Splitting them would +// suggest six rules exist; the point of the operand widening is that they are consequences. +test fn scm_mm_the_presence_cases_fall_out_of_the_one_law() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: _ } => + // source deleted a path the target left at base -> deleted + (match merge_manifests(base: at(path: "a", source: x), source: [], target: at(path: "a", source: x)) { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + }) + // both deleted -> deleted + && (match merge_manifests(base: at(path: "a", source: x), source: [], target: []) { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + }) + // source added a path the target does not have -> added + && (match merge_manifests(base: [], source: at(path: "a", source: y), target: []) { + ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) + ManifestConflicted { conflicts: _ } => false + }) + // both added the same content -> added, no conflict + && (match merge_manifests(base: [], source: at(path: "a", source: y), target: at(path: "a", source: y)) { + ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) + ManifestConflicted { conflicts: _ } => false + }) + // target deleted a path the source left at base -> deleted + && (match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: x), target: []) { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + }) + // both added different content -> conflict + && (match merge_manifests(base: [], source: at(path: "a", source: y), target: at(path: "a", source: x)) { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => count(c) == 1 + }) + } +} + +// DELETE VERSUS MODIFY. The central claim, and the reason the operand carries presence: a bare-locator +// law has no state to compare here and must either take the deletion -- silently discarding the +// target's edit -- or take the edit, silently resurrecting a file the source deleted on purpose. Both +// produce a valid manifest and neither is visible to the caller. +test fn scm_mm_a_delete_against_a_modify_conflicts_and_says_which_side_was_absent() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: _ } => + match merge_manifests(base: at(path: "a", source: x), source: [], target: at(path: "a", source: y)) { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 1 + && fold(c, init: false, f: fn(found, k) { + found || ( + (k.path as String) == "a" + && path_state_eq(left: k.base, right: PathPresent { source: x }) + && path_state_eq(left: k.source, right: PathAbsent) + && path_state_eq(left: k.target, right: PathPresent { source: y }) + ) + }) + } + } +} + +// MODIFY VERSUS DELETE, the mirror. Written separately because the two are decided by the SAME absent +// arm from opposite sides, and an implementation that special-cased one would pass the other. +test fn scm_mm_a_modify_against_a_delete_conflicts_and_says_which_side_was_absent() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: _ } => + match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: []) { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 1 + && fold(c, init: false, f: fn(found, k) { + found || ( + path_state_eq(left: k.base, right: PathPresent { source: x }) + && path_state_eq(left: k.source, right: PathPresent { source: y }) + && path_state_eq(left: k.target, right: PathAbsent) + ) + }) + } + } +} + +// THE COMPLETE POPULATION, AND A MERGEABLE PATH ALONGSIDE THEM. A first-wins implementation reports +// one conflict and passes every single-conflict control above; only a specimen with TWO conflicting +// paths separates it. The third path is mergeable and must NOT appear as a conflict, so the claim +// also refutes an implementation that gives up wholesale once any path conflicts. +test fn scm_mm_every_conflicting_path_is_reported_not_the_first() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: z } => + // a: base x, source y, target z -> all three differ -> CONFLICT + // b: base x, source ABSENT, target y -> delete versus modify -> CONFLICT + // c: base x, source x, target y -> source untouched -> take target, MERGEABLE + match merge_manifests( + base: concat(at(path: "a", source: x), concat(at(path: "b", source: x), at(path: "c", source: x))), + source: concat(at(path: "a", source: y), at(path: "c", source: x)), + target: concat(at(path: "a", source: z), concat(at(path: "b", source: y), at(path: "c", source: y))), + ) { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 2 + && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "a" }) + && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "b" }) + && !fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "c" }) + } + } +} + +// THE "EITHER" ARM IS GENUINELY EITHER, DERIVED RATHER THAN ASSUMED. When source and target agree the +// law returns one of them, and "they are equal so it does not matter" is the shape of reasoning that +// hid an identity defect one module over. So it is checked: swapping the two operands must produce +// the same entries. If a future change ever makes the choice observable, this goes red. +test fn scm_mm_when_both_sides_agree_the_operand_returned_is_unobservable() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: _ } => + match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: at(path: "a", source: y)) { + ManifestConflicted { conflicts: _ } => false + ManifestMerged { entries: left } => + match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: at(path: "a", source: y)) { + ManifestConflicted { conflicts: _ } => false + ManifestMerged { entries: right } => + entries_hold(entries: left, path: "a", source: y) + && entries_hold(entries: right, path: "a", source: y) + } + } + } +} + +// THE UNION IS THE SUBJECT, NOT THE BASE. A path added only by the source is decided; an +// implementation iterating the base's paths drops it silently and returns a manifest missing a file +// the source added. +test fn scm_mm_a_path_only_one_side_has_is_still_decided() -> Bool { + match pair() { + TrioUnavailable => false + Trio { x: x, y: y, z: _ } => + match merge_manifests(base: [], source: at(path: "new", source: y), target: at(path: "kept", source: x)) { + ManifestConflicted { conflicts: _ } => false + ManifestMerged { entries: e } => + count(e) == 2 + && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "new" }) + && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "kept" }) + } + } +} + +test fn scm_manifest_merge_witnesses_hold() -> Bool { + scm_mm_the_presence_cases_fall_out_of_the_one_law() + && scm_mm_a_delete_against_a_modify_conflicts_and_says_which_side_was_absent() + && scm_mm_a_modify_against_a_delete_conflicts_and_says_which_side_was_absent() + && scm_mm_every_conflicting_path_is_reported_not_the_first() + && scm_mm_when_both_sides_agree_the_operand_returned_is_unobservable() + && scm_mm_a_path_only_one_side_has_is_still_decided() +} From 2f32c9b45b2c0756751192bb2d869f5ab9ea1627 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 17:58:01 +0000 Subject: [PATCH 2/7] Take the merge law's operands from raw lists to store-constructed records, and its traversal from quadratic to one pass Both blocking findings of review 61418 on 7ccfe27062c, verified against the code before acting. Both are correct, and their fixes turn out to be the same fix. THE OPERANDS. merge_manifests took List on all three sides. That is worse than loose typing, because the module carried an ANNOTATION asserting that store_corpus_manifest refuses a duplicate path "so the first match is THE match" -- an assertion about a guarantee THE SIGNATURE DID NOT CARRY, which is validation-by-comment standing exactly where construction was available (DESIGN 5). The reviewer's specimen: a source of [a -> X, a -> Y] merged SUCCESSFULLY by silently selecting the first, and reversing that list changed the answer. Fabricated plausible output, forbidden outright. The three sides are now CorpusManifestRecord, which is sole_constructor and canonicalised at the store, so the specimen is no longer expressible at the boundary. THE TRAVERSAL. Every union path re-folded all three inputs through path_state_in -- quadratic in manifest size, and quadratic even when the three sides are identical and nothing conflicts. DESIGN 6 makes that unconditional: a proven cost-shape defect is always fixed regardless of the realized n, because n is not a time-stable fact about a compiler's corpus manifest. Replaced by a sorted grouping join -- tag each entry with its side, sort the three streams together by path, fold ONCE, close a group when the path changes. path_state_in and merged_path_union are DELETED, not made faster. The union, the three lookups and the decision are now the same traversal, so there is nothing left for them to answer. THE TWO ARE ONE. Assigning a group member to its side is total ONLY because no side can hold two entries for one path. A raw list can hold exactly that; a record cannot. A DECORATION IS DELETED RATHER THAN REPAIRED. The S==T "either operand is unobservable" claim called merged() with IDENTICAL arguments twice -- but repairing the swap would not have saved it. That arm is reached only when path_state_eq holds, path_state_eq on two present states compares locators, and AuthoredSourceTarget carries a locator and nothing else, so the operands are indistinguishable to every observer this corpus can write. No input could turn it red, so it asserted nothing while looking like coverage (DESIGN 4b). The unobservability is STRUCTURAL, which is a stronger statement than the claim made. Its red becomes authorable the day AuthoredSourceTarget gains a field outside the equality, and the annotation says so. That claim was cited as evidence in the PR body, so the PR body overstated what had been verified; it is corrected there. THE 4c REFUSAL, AND WHY MY OWN GUARD DID NOT SEE IT. The floor lane refused eight in-body annotations in the witness file. The local pre-push guard reported ZERO. It classified by what FOLLOWED an annotation block, and in-body comments are followed by ordinary expressions, which it read as "not a declaration, keep looking". A detector with false NEGATIVES is worse than no detector for the same reason a detector with false positives is: it gets cited as coverage. Rewritten to key on the only thing the rule is about -- module-item grain means column zero -- and controlled against 7ccfe27062c, where it reproduces all eight refused lines plus a ninth the CI log had truncated, and reads zero here. The labels themselves were worth keeping, so they are hoisted into the leading annotation of the claim they describe rather than dropped. EVIDENCE. 441/0 across all SCM witness files -- 442 minus the deleted decoration. Four mutations, two aimed at the join that did not exist before: mutation presence del/mod mod/del complete union bare-locator equality RED RED RED RED RED first-wins conflicts pass pass pass RED pass last group never closed RED RED RED pass RED target side dropped from join RED RED pass RED RED as built pass pass pass pass pass The last group is closed by close_groups and not by the fold, because a fold closes a group when it sees the NEXT path and the final group has none. An implementation missing that line drops the alphabetically last path from every merge and still returns a well-formed manifest. NO CLAIM IS ADDED FOR THE UNIQUENESS FIX, deliberately. It is now structural, so its red is unauthorable, which is the same test that retired the decoration above. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/scm/manifest_merge.dag | 200 ++++++++----- .../scm/scm_manifest_merge_witness_test.dag | 275 ++++++++++++------ 2 files changed, 319 insertions(+), 156 deletions(-) diff --git a/dag/gunbc/scm/manifest_merge.dag b/dag/gunbc/scm/manifest_merge.dag index c5ffec90468..3a3962f74b2 100644 --- a/dag/gunbc/scm/manifest_merge.dag +++ b/dag/gunbc/scm/manifest_merge.dag @@ -39,7 +39,7 @@ import std.types { Bool, List, String, NonEmptyStr } import gunbc.scm.object_store { AuthoredSourceTarget, CorpusManifestEntry, - canonical_manifest_entries, + CorpusManifestRecord, object_id_eq, } @@ -66,23 +66,6 @@ fn path_state_eq(left: PathState, right: PathState) -> Bool { } } -// A manifest holds at most one entry per path -- store_corpus_manifest refuses a duplicate before an -// identity is derived -- so the first match is THE match and no ambiguity rule is needed here. That -// is a property of the carrier this reads, not an assumption this module makes. -fn path_state_in(entries: List, path: String) -> PathState { - fold(entries, init: PathAbsent, f: fn(found, e) { - match found { - PathPresent { source: _ } => found - PathAbsent => - if (e.path as String) == path { - PathPresent { source: e.source } - } else { - found - } - } - }) -} - // THE CONFLICT CARRIES ALL THREE STATES, INCLUDING EXPLICIT ABSENCE, AND THAT IS NOT DIAGNOSTIC // GARNISH. A deletion reported as some sentinel or fabricated locator would collapse absence back // into a malformed-content representation -- the exact presence/content conflation the operand was @@ -156,68 +139,153 @@ fn admit_state(acc: MergeAcc, path: NonEmptyStr, state: PathState) -> MergeAcc { // the merge must decide. Taking the base's paths alone would silently drop every addition; taking the // target's would silently drop every source addition. // -// THE UNION IS DERIVED THROUGH THE MANIFEST'S OWN CANONICAL ORDER rather than through an order this -// module invents, so the conflict population and the merged entries are both reported in the order -// the carrier already uses. Deduplication is against the IMMEDIATELY PRECEDING path and not against -// every earlier one -- the quadratic scan a membership test would need is bought by the sort that has -// already happened, which is the same trade `a_duplicated_manifest_path` makes one module over. -type PathUnionAcc { - previous: String? - paths: List -} - -fn path_union_step(acc: PathUnionAcc, entry: CorpusManifestEntry) -> PathUnionAcc { - match acc.previous { - Present { value: p } => - if p == (entry.path as String) { - acc +// THE UNION IS TAKEN BY A SORTED GROUPING JOIN, IN ONE PASS. A first derivation of this module built +// the union and then asked each of the three manifests for its state at every path in it, which is a +// fold over all three inputs per union path -- quadratic in the manifest size, and quadratic even +// when the three sides are identical and nothing conflicts. DESIGN section 6 makes that +// unconditional: a proven cost-shape defect is always fixed regardless of the realized n, because n +// is not a time-stable fact about a compiler's corpus manifest. +// +// The replacement tags each entry with the side it came from, sorts the three streams together by +// path, and folds ONCE: entries sharing a path are adjacent by construction, so a group is closed +// when the path changes. The union, the three lookups, and the decision are then the same traversal +// rather than three -- which is also why `path_state_in` no longer exists. It was not made faster; +// there is nothing left for it to answer. +// +// ASSIGNING A GROUP MEMBER TO ITS SIDE IS TOTAL ONLY BECAUSE OF THE OPERAND ABOVE. Two entries from +// one side sharing a path would make "the source's state at this path" ambiguous, and a raw list can +// hold exactly that; `CorpusManifestRecord` cannot. The two corrections are one correction. +type ManifestSide + = ManifestBaseSide + | ManifestSourceSide + | ManifestTargetSide + +type SidedEntry { + side: ManifestSide + path: NonEmptyStr + source: AuthoredSourceTarget +} + +fn sided_entries(side: ManifestSide, entries: List) -> List { + map(entries, e => SidedEntry { side: side, path: e.path, source: e.source }) +} + +// A SLOT OPENS AT FULL ABSENCE. A side that never appears in the group is absent at this path, which +// is the state the law reads -- not a missing observation to be filled in later. +type PathSlot { + path: NonEmptyStr + base: PathState + source: PathState + target: PathState +} + +fn empty_slot(path: NonEmptyStr) -> PathSlot { + PathSlot { path: path, base: PathAbsent, source: PathAbsent, target: PathAbsent } +} + +fn slot_admit(slot: PathSlot, entry: SidedEntry) -> PathSlot { + match entry.side { + ManifestBaseSide => + PathSlot { + path: slot.path, + base: PathPresent { source: entry.source }, + source: slot.source, + target: slot.target, + } + ManifestSourceSide => + PathSlot { + path: slot.path, + base: slot.base, + source: PathPresent { source: entry.source }, + target: slot.target, + } + ManifestTargetSide => + PathSlot { + path: slot.path, + base: slot.base, + source: slot.source, + target: PathPresent { source: entry.source }, + } + } +} + +fn decide_slot(acc: MergeAcc, slot: PathSlot) -> MergeAcc { + merge_path( + acc: acc, + path: slot.path, + base: slot.base, + source: slot.source, + target: slot.target, + ) +} + +type GroupAcc { + open: PathSlot? + decided: MergeAcc +} + +fn group_step(acc: GroupAcc, entry: SidedEntry) -> GroupAcc { + match acc.open { + Present { value: slot } => + if (slot.path as String) == (entry.path as String) { + GroupAcc { open: Present { value: slot_admit(slot: slot, entry: entry) }, decided: acc.decided } } else { - PathUnionAcc { - previous: Present { value: entry.path as String }, - paths: concat([entry.path], acc.paths), + GroupAcc { + open: Present { value: slot_admit(slot: empty_slot(path: entry.path), entry: entry) }, + decided: decide_slot(acc: acc.decided, slot: slot), } } Absent => - PathUnionAcc { - previous: Present { value: entry.path as String }, - paths: concat([entry.path], acc.paths), + GroupAcc { + open: Present { value: slot_admit(slot: empty_slot(path: entry.path), entry: entry) }, + decided: acc.decided, } } } -fn merged_path_union( - base: List, - source: List, - target: List, -) -> List { - reverse( - fold( - canonical_manifest_entries(entries: concat(base, concat(source, target))), - init: PathUnionAcc { previous: none, paths: [] }, - f: fn(acc, e) { path_union_step(acc: acc, entry: e) }, - ).paths - ) +// THE LAST GROUP IS CLOSED BY THE CALLER, NOT BY THE FOLD. A fold closes a group when it sees the +// next path, and the final group has no next path -- so an implementation that forgot this line would +// silently drop the alphabetically last path from every merge, and would still return a well-formed +// manifest. The claim that reds on it is the union claim. +fn close_groups(acc: GroupAcc) -> MergeAcc { + match acc.open { + Present { value: slot } => decide_slot(acc: acc.decided, slot: slot) + Absent => acc.decided + } } // THE CONFLICT CHECK IS ON THE POPULATION, NOT ON A FLAG. A Bool set beside the accumulator would be // a second authority for "did anything conflict", free to disagree with the list it describes. +// +// THE OPERANDS ARE STORE-CONSTRUCTED RECORDS, NOT RAW LISTS. `CorpusManifestRecord` is +// sole_constructor and `store_corpus_manifest` refuses a duplicate path before an identity is +// derived, so no caller can hand this function a manifest holding two entries for one path. A first +// derivation took `List` and carried an annotation asserting that uniqueness +// held -- an assertion about a guarantee the SIGNATURE did not carry, which is validation-by-comment +// standing where construction was available. Under raw lists, a source of [a -> X, a -> Y] merged +// successfully by silently selecting the first, and reversing that list changed the answer: the +// fabricated plausible output DESIGN section 5 forbids outright. fn merge_manifests( - base: List, - source: List, - target: List, + base: CorpusManifestRecord, + source: CorpusManifestRecord, + target: CorpusManifestRecord, ) -> ManifestMergeOutcome { - let decided = fold( - merged_path_union(base: base, source: source, target: target), - init: MergeAcc { entries: [], conflicts: [] }, - f: fn(acc, path) { - merge_path( - acc: acc, - path: path, - base: path_state_in(entries: base, path: path as String), - source: path_state_in(entries: source, path: path as String), - target: path_state_in(entries: target, path: path as String), - ) - }, + let joined = sort_by( + concat( + sided_entries(side: ManifestBaseSide, entries: base.entries), + concat( + sided_entries(side: ManifestSourceSide, entries: source.entries), + sided_entries(side: ManifestTargetSide, entries: target.entries), + ), + ), + fn(e) { e.path as String }, + ) + let decided = close_groups( + acc: fold( + joined, + init: GroupAcc { open: none, decided: MergeAcc { entries: [], conflicts: [] } }, + f: fn(acc, e) { group_step(acc: acc, entry: e) }, + ) ) if count(decided.conflicts) > 0 { ManifestConflicted { conflicts: reverse(decided.conflicts) } diff --git a/dag/test/claim/scm/scm_manifest_merge_witness_test.dag b/dag/test/claim/scm/scm_manifest_merge_witness_test.dag index 61104969be7..54e5b130ecd 100644 --- a/dag/test/claim/scm/scm_manifest_merge_witness_test.dag +++ b/dag/test/claim/scm/scm_manifest_merge_witness_test.dag @@ -10,6 +10,11 @@ import gunbc.scm.object_store { ObjectStore, ObjectId, empty_store, object_id_eq, CorpusManifestEntry, AuthoredSourceTarget, SourceStored, SourceLocatorCollision, store_authored_source, + CorpusManifestRecord, store_corpus_manifest, + CorpusManifestStored, CorpusManifestDuplicatePath, CorpusManifestLocatorCollision, + find_corpus_manifest_record, + CorpusManifestFound, CorpusManifestAbsent, + CorpusManifestIsSemanticNode, CorpusManifestIsAuthoredSource, } import gunbc.scm.manifest_merge { PathState, PathAbsent, PathPresent, path_state_eq, @@ -56,6 +61,56 @@ fn at(path: String, source: AuthoredSourceTarget) -> List { [CorpusManifestEntry { path: path as NonEmptyStr, source: source }] } +// THE THREE SIDES ARE STORE-CONSTRUCTED, NOT ASSEMBLED HERE. `CorpusManifestRecord` is +// sole_constructor precisely so a fixture cannot forge one, so every specimen below is a record the +// store actually minted -- which also means these claims exercise the uniqueness guarantee the merge +// law now depends on instead of assuming it. +// +// EVERY WAY OF FAILING TO BUILD A SPECIMEN REDS THE CLAIM. `MergeUnavailable` is returned to a `false` +// at each call site rather than being skipped, because a fixture that silently failed to build would +// make each claim vacuously true -- a green with no subject, which is the specification-without- +// execution trap wearing a fixture's clothes. +type Manifest + = Manifest(CorpusManifestRecord) + | ManifestUnavailable + +fn manifest(entries: List) -> Manifest { + match store_corpus_manifest(store: empty_store(), entries: entries) { + CorpusManifestDuplicatePath { path: _ } => ManifestUnavailable + CorpusManifestLocatorCollision { identity: _, existing: _, incoming: _ } => ManifestUnavailable + CorpusManifestStored { store: s, manifest: reference } => + match find_corpus_manifest_record(store: s, identity: reference.locator) { + CorpusManifestAbsent { identity: _ } => ManifestUnavailable + CorpusManifestIsSemanticNode { identity: _ } => ManifestUnavailable + CorpusManifestIsAuthoredSource { identity: _ } => ManifestUnavailable + CorpusManifestFound(record) => Manifest(record) + } + } +} + +type Merged + = Merged(ManifestMergeOutcome) + | MergeUnavailable + +fn merged( + base: List, + source: List, + target: List, +) -> Merged { + match manifest(entries: base) { + ManifestUnavailable => MergeUnavailable + Manifest(b) => + match manifest(entries: source) { + ManifestUnavailable => MergeUnavailable + Manifest(s) => + match manifest(entries: target) { + ManifestUnavailable => MergeUnavailable + Manifest(t) => Merged(merge_manifests(base: b, source: s, target: t)) + } + } + } +} + fn entries_hold(entries: List, path: String, source: AuthoredSourceTarget) -> Bool { count(entries) == 1 && fold(entries, init: false, f: fn(found, e) { @@ -65,40 +120,67 @@ fn entries_hold(entries: List, path: String, source: Author // THE SIX PRESENCE CASES, ASSERTED AS ONE CLAIM BECAUSE THEY ARE ONE LAW. Splitting them would // suggest six rules exist; the point of the operand widening is that they are consequences. +// +// THE SIX SPECIMENS BELOW, IN ORDER, and what each one is: +// +// B=x S=absent T=x source deleted a path the target left at base -> DELETED +// B=x S=absent T=absent both deleted -> DELETED +// B=- S=y T=absent source added a path the target does not have -> ADDED +// B=- S=y T=y both added the same content -> ADDED, no conflict +// B=x S=x T=absent target deleted a path the source left at base -> DELETED +// B=- S=y T=x both added different content -> CONFLICT test fn scm_mm_the_presence_cases_fall_out_of_the_one_law() -> Bool { match pair() { TrioUnavailable => false Trio { x: x, y: y, z: _ } => - // source deleted a path the target left at base -> deleted - (match merge_manifests(base: at(path: "a", source: x), source: [], target: at(path: "a", source: x)) { - ManifestMerged { entries: e } => count(e) == 0 - ManifestConflicted { conflicts: _ } => false - }) - // both deleted -> deleted - && (match merge_manifests(base: at(path: "a", source: x), source: [], target: []) { - ManifestMerged { entries: e } => count(e) == 0 - ManifestConflicted { conflicts: _ } => false - }) - // source added a path the target does not have -> added - && (match merge_manifests(base: [], source: at(path: "a", source: y), target: []) { - ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) - ManifestConflicted { conflicts: _ } => false - }) - // both added the same content -> added, no conflict - && (match merge_manifests(base: [], source: at(path: "a", source: y), target: at(path: "a", source: y)) { - ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) - ManifestConflicted { conflicts: _ } => false - }) - // target deleted a path the source left at base -> deleted - && (match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: x), target: []) { - ManifestMerged { entries: e } => count(e) == 0 - ManifestConflicted { conflicts: _ } => false - }) - // both added different content -> conflict - && (match merge_manifests(base: [], source: at(path: "a", source: y), target: at(path: "a", source: x)) { - ManifestMerged { entries: _ } => false - ManifestConflicted { conflicts: c } => count(c) == 1 - }) + (match merged(base: at(path: "a", source: x), source: [], target: at(path: "a", source: x)) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + } + }) + && (match merged(base: at(path: "a", source: x), source: [], target: []) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + } + }) + && (match merged(base: [], source: at(path: "a", source: y), target: []) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) + ManifestConflicted { conflicts: _ } => false + } + }) + && (match merged(base: [], source: at(path: "a", source: y), target: at(path: "a", source: y)) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: e } => entries_hold(entries: e, path: "a", source: y) + ManifestConflicted { conflicts: _ } => false + } + }) + && (match merged(base: at(path: "a", source: x), source: at(path: "a", source: x), target: []) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: e } => count(e) == 0 + ManifestConflicted { conflicts: _ } => false + } + }) + && (match merged(base: [], source: at(path: "a", source: y), target: at(path: "a", source: x)) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => count(c) == 1 + } + }) } } @@ -110,18 +192,22 @@ test fn scm_mm_a_delete_against_a_modify_conflicts_and_says_which_side_was_absen match pair() { TrioUnavailable => false Trio { x: x, y: y, z: _ } => - match merge_manifests(base: at(path: "a", source: x), source: [], target: at(path: "a", source: y)) { - ManifestMerged { entries: _ } => false - ManifestConflicted { conflicts: c } => - count(c) == 1 - && fold(c, init: false, f: fn(found, k) { - found || ( - (k.path as String) == "a" - && path_state_eq(left: k.base, right: PathPresent { source: x }) - && path_state_eq(left: k.source, right: PathAbsent) - && path_state_eq(left: k.target, right: PathPresent { source: y }) - ) - }) + match merged(base: at(path: "a", source: x), source: [], target: at(path: "a", source: y)) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 1 + && fold(c, init: false, f: fn(found, k) { + found || ( + (k.path as String) == "a" + && path_state_eq(left: k.base, right: PathPresent { source: x }) + && path_state_eq(left: k.source, right: PathAbsent) + && path_state_eq(left: k.target, right: PathPresent { source: y }) + ) + }) + } } } } @@ -132,17 +218,21 @@ test fn scm_mm_a_modify_against_a_delete_conflicts_and_says_which_side_was_absen match pair() { TrioUnavailable => false Trio { x: x, y: y, z: _ } => - match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: []) { - ManifestMerged { entries: _ } => false - ManifestConflicted { conflicts: c } => - count(c) == 1 - && fold(c, init: false, f: fn(found, k) { - found || ( - path_state_eq(left: k.base, right: PathPresent { source: x }) - && path_state_eq(left: k.source, right: PathPresent { source: y }) - && path_state_eq(left: k.target, right: PathAbsent) - ) - }) + match merged(base: at(path: "a", source: x), source: at(path: "a", source: y), target: []) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 1 + && fold(c, init: false, f: fn(found, k) { + found || ( + path_state_eq(left: k.base, right: PathPresent { source: x }) + && path_state_eq(left: k.source, right: PathPresent { source: y }) + && path_state_eq(left: k.target, right: PathAbsent) + ) + }) + } } } } @@ -151,49 +241,51 @@ test fn scm_mm_a_modify_against_a_delete_conflicts_and_says_which_side_was_absen // one conflict and passes every single-conflict control above; only a specimen with TWO conflicting // paths separates it. The third path is mergeable and must NOT appear as a conflict, so the claim // also refutes an implementation that gives up wholesale once any path conflicts. +// +// THE THREE PATHS, AND WHY EACH IS THE ONE IT IS: +// +// a: B=x S=y T=z all three differ -> CONFLICT +// b: B=x S=absent T=y delete versus modify -> CONFLICT +// c: B=x S=x T=y source untouched -> take target, MERGEABLE +// +// The mergeable third path is not filler: it is what makes the claim distinguish "reported every +// conflict" from "reported every path". test fn scm_mm_every_conflicting_path_is_reported_not_the_first() -> Bool { match pair() { TrioUnavailable => false Trio { x: x, y: y, z: z } => - // a: base x, source y, target z -> all three differ -> CONFLICT - // b: base x, source ABSENT, target y -> delete versus modify -> CONFLICT - // c: base x, source x, target y -> source untouched -> take target, MERGEABLE - match merge_manifests( + match merged( base: concat(at(path: "a", source: x), concat(at(path: "b", source: x), at(path: "c", source: x))), source: concat(at(path: "a", source: y), at(path: "c", source: x)), target: concat(at(path: "a", source: z), concat(at(path: "b", source: y), at(path: "c", source: y))), ) { - ManifestMerged { entries: _ } => false - ManifestConflicted { conflicts: c } => - count(c) == 2 - && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "a" }) - && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "b" }) - && !fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "c" }) + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestMerged { entries: _ } => false + ManifestConflicted { conflicts: c } => + count(c) == 2 + && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "a" }) + && fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "b" }) + && !fold(c, init: false, f: fn(f2, k) { f2 || (k.path as String) == "c" }) } - } -} - -// THE "EITHER" ARM IS GENUINELY EITHER, DERIVED RATHER THAN ASSUMED. When source and target agree the -// law returns one of them, and "they are equal so it does not matter" is the shape of reasoning that -// hid an identity defect one module over. So it is checked: swapping the two operands must produce -// the same entries. If a future change ever makes the choice observable, this goes red. -test fn scm_mm_when_both_sides_agree_the_operand_returned_is_unobservable() -> Bool { - match pair() { - TrioUnavailable => false - Trio { x: x, y: y, z: _ } => - match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: at(path: "a", source: y)) { - ManifestConflicted { conflicts: _ } => false - ManifestMerged { entries: left } => - match merge_manifests(base: at(path: "a", source: x), source: at(path: "a", source: y), target: at(path: "a", source: y)) { - ManifestConflicted { conflicts: _ } => false - ManifestMerged { entries: right } => - entries_hold(entries: left, path: "a", source: y) - && entries_hold(entries: right, path: "a", source: y) - } } } } +// WHY THERE IS NO CLAIM HERE FOR THE `S == T` ARM RETURNING "EITHER" OPERAND. An earlier draft +// carried one, on the reasoning that "they are equal so it does not matter" is the shape that hid an +// identity defect one module over. It was a DECORATION and is deleted rather than repaired. The arm +// is reached only when `path_state_eq` holds, `path_state_eq` on two present states compares +// locators, and `AuthoredSourceTarget` carries a locator and nothing else -- so the two operands are +// not merely equal, they are indistinguishable to every observer this corpus can write, including +// `entries_hold`. There is no fixture that makes the choice observable, so no input can turn the +// claim red, so it asserted nothing while looking like coverage (DESIGN section 4b). The +// unobservability is structural, which is a stronger statement than the claim was making. +// +// ITS RED BECOMES AUTHORABLE THE DAY `AuthoredSourceTarget` GAINS A FIELD OUTSIDE THE EQUALITY -- +// at which point the arm has a real choice and this claim must come back with it. + // THE UNION IS THE SUBJECT, NOT THE BASE. A path added only by the source is decided; an // implementation iterating the base's paths drops it silently and returns a manifest missing a file // the source added. @@ -201,12 +293,16 @@ test fn scm_mm_a_path_only_one_side_has_is_still_decided() -> Bool { match pair() { TrioUnavailable => false Trio { x: x, y: y, z: _ } => - match merge_manifests(base: [], source: at(path: "new", source: y), target: at(path: "kept", source: x)) { - ManifestConflicted { conflicts: _ } => false - ManifestMerged { entries: e } => - count(e) == 2 - && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "new" }) - && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "kept" }) + match merged(base: [], source: at(path: "new", source: y), target: at(path: "kept", source: x)) { + MergeUnavailable => false + Merged(outcome) => + match outcome { + ManifestConflicted { conflicts: _ } => false + ManifestMerged { entries: e } => + count(e) == 2 + && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "new" }) + && fold(e, init: false, f: fn(f2, k) { f2 || (k.path as String) == "kept" }) + } } } } @@ -216,6 +312,5 @@ test fn scm_manifest_merge_witnesses_hold() -> Bool { && scm_mm_a_delete_against_a_modify_conflicts_and_says_which_side_was_absent() && scm_mm_a_modify_against_a_delete_conflicts_and_says_which_side_was_absent() && scm_mm_every_conflicting_path_is_reported_not_the_first() - && scm_mm_when_both_sides_agree_the_operand_returned_is_unobservable() && scm_mm_a_path_only_one_side_has_is_still_decided() } From 2990aa17a8115ccd0c8cbafb90a1a2e7e2a72d69 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 19:44:06 +0000 Subject: [PATCH 3/7] The merge verb: join the base derivation to the path algebra, and nothing else gunbc.scm.merge_base decides WHICH BASE a squash is entitled to use and refuses when there is none. gunbc.scm.manifest_merge decides EACH PATH against a base and refuses when the sides disagree irreconcilably. Both refuse independently, and both were controlled -- but nothing joined them, so there was no operation anyone could invoke to merge anything. This is that join. It introduces NO decision of its own: every refusal is one of the two modules' refusals carried outward, or a store fact observed at the boundary. THE ORDER IS FORCED, NOT CHOSEN. The base is derived BEFORE the manifests are read, for the reason merge_base runs its consumed-source join before it looks for a common ancestor: deriving a merged manifest against a base the repository is not entitled to use constructs the unsafe value and then discards it, and a resurrection that is computed and thrown away still existed. THE SQUASH WORKFLOW IS NOW STRUCTURAL RATHER THAN CONVENTIONAL. The result records ONE lineage edge -- parent is the target -- and the source is recorded as CONSUMED through SquashIntegrated rather than as a second parent. Nothing is lost by that: the receipt is precisely what merge_base reads to refuse the second merge, so "do not merge the same branch twice" is enforced by construction instead of by discipline, and there is no dev history to rebase because none was created. REFUSALS ARE NOT FLATTENED INTO ONE "MERGE FAILED" ARM. A consumed source, a conflicting path, a missing manifest and an invalid allocator have four different remedies and four different principals to blame. Collapsing them is the absorbing fallback DESIGN section 5 names. ONE PLACE DELIBERATELY DOES COLLAPSE, AND IT IS FLAGGED RATHER THAN HIDDEN. carry_mint folds the mint's three root refusals into one SquashMergeMintRootUnresolvable, because the root handed to the mint was minted BY THIS FUNCTION from the store one line earlier -- so all three mean "the store did not keep what it just accepted", which is one fact about one store and not three populations a caller acts on differently. This is the one judgement in the module I am least sure of, since the rest of the lane argues the other way, and it is written down so a reviewer can overturn it rather than have to find it. THE FIXTURE MOVED INSTEAD OF BEING COPIED. The repository builder was authored inside the merge_base witness and is needed verbatim here. Two copies of one construction rule drift INVISIBLY -- each copy keeps passing its own claims while the two fixtures quietly stop describing the same repository -- so it moved to test.fixture.scm_repository_builder and both witnesses read it. All twelve merge_base claims pass unchanged against the shared fixture, which is what makes the extraction safe to build on rather than a hopeful refactor. EVIDENCE. 446/0 across all SCM witness files, up from 441. The two halves' own behaviours are NOT re-asserted here; what is unproven until this file exists is that the JOIN preserves them. Three mutations, each reding a different combination: mutation both paths parent/receipt double merge conflict parent on the source pass RED pass pass drop the consumed receipt pass RED RED pass ignore merge_base's answer RED pass pass RED The second is the load-bearing one: dropping the receipt reds the double-merge claim, so the resurrection refusal genuinely flows THROUGH the verb rather than being asserted beside it. The scene is a DIVERGENCE and not a fast-forward, deliberately. If the target had not moved since the base, taking the source's manifest wholesale would be correct and every claim here would pass against an implementation that ignores the base entirely. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/scm/squash_merge.dag | 268 +++++++++++++ .../claim/scm/scm_merge_base_witness_test.dag | 146 +------ .../scm/scm_squash_merge_witness_test.dag | 377 ++++++++++++++++++ dag/test/fixture/scm_repository_builder.dag | 182 +++++++++ 4 files changed, 830 insertions(+), 143 deletions(-) create mode 100644 dag/gunbc/scm/squash_merge.dag create mode 100644 dag/test/claim/scm/scm_squash_merge_witness_test.dag create mode 100644 dag/test/fixture/scm_repository_builder.dag diff --git a/dag/gunbc/scm/squash_merge.dag b/dag/gunbc/scm/squash_merge.dag new file mode 100644 index 00000000000..8034084c2fd --- /dev/null +++ b/dag/gunbc/scm/squash_merge.dag @@ -0,0 +1,268 @@ +module gunbc.scm.squash_merge + +// THE MERGE VERB, WHICH IS THE COMPOSITION AND NOTHING ELSE. +// +// gunbc.scm.merge_base decides WHICH BASE a squash is entitled to use, and refuses when there is +// none. gunbc.scm.manifest_merge decides EACH PATH against a base, and refuses when the two sides +// disagree irreconcilably. Both were built to refuse independently, and both did -- but nothing +// joined them, so there was no operation a caller could invoke to merge anything. This module is +// that join, and it deliberately introduces no new decision of its own: every refusal below is one +// of the two modules' refusals carried outward, or a store fact observed at the boundary. +// +// THE ORDER IS FORCED, NOT CHOSEN. The base must be derived BEFORE the manifests are read, because +// deriving a merged manifest against a base the repository is not entitled to use would construct +// the unsafe value and then discard it -- the same reason merge_base runs its consumed-source join +// before it looks for a common ancestor. A resurrection that is computed and then thrown away is +// still a resurrection that existed. +// +// THE REFUSALS ARE NOT FLATTENED INTO ONE "MERGE FAILED" ARM. An already-consumed source, a +// conflicting path, a missing manifest and an invalid allocator have four different remedies and +// four different principals to blame: the first is an unsupported operation on an intact repository, +// the second is a decision only a human can make, the third is a damaged store, the fourth is a +// corrupt envelope. Collapsing them is the absorbing fallback DESIGN section 5 names -- a widened +// arm destroys the signal that would rank the precise deficit for repair. + +import std.types { List, String } +import gunbc.scm.object_store { + ObjectId, + CorpusManifestRecord, + CorpusManifestEntry, + CorpusManifestTarget, + CorpusManifestObjectRef, + store_corpus_manifest, + CorpusManifestStored, + CorpusManifestDuplicatePath, + CorpusManifestLocatorCollision, + find_corpus_manifest_record, + CorpusManifestFound, + CorpusManifestAbsent, + CorpusManifestIsSemanticNode, + CorpusManifestIsAuthoredSource, +} +import gunbc.scm.ancestry { RepositoryCommitRef } +import gunbc.scm.integration { SquashIntegrated } +import gunbc.scm.merge_base { + MergeBaseOutcome, + MergeBaseDerived, + MergeBaseSourceAlreadyConsumed, + MergeBaseHistoryUnwalkable, + MergeBaseHistoriesDisjoint, + merge_base, +} +import gunbc.scm.manifest_merge { + ManifestPathConflict, + ManifestMergeOutcome, + ManifestMerged, + ManifestConflicted, + merge_manifests, +} +import gunbc.scm.repository_envelope { + RepositoryEnvelope, + RepositoryCommit, + RepositoryCommitMint, + RepositoryCommitMinted, + RepositoryCommitMintAllocatorInvalid, + RepositoryCommitMintRootMissing, + RepositoryCommitMintRootIsAuthoredSource, + RepositoryCommitMintRootIsSemanticNode, + RepositoryCommitMintParentMissing, + RepositoryCommitMintIntegrationSourceMissing, + commit_at_reference, + mint_repository_commit, +} + +// WHICH SIDE'S ROOT FAILED TO RESOLVE IS PART OF THE FACT, NOT CONTEXT FOR A LOG LINE. Three commits +// are read here and all three can be damaged in the same three ways; an outcome naming only the +// locator would send an operator to diff a store against nine possibilities. The locator says WHAT +// is wrong and this says WHOSE. +type MergeSideName + = MergeBaseCommit + | MergeSourceCommit + | MergeTargetCommit + +type SquashMergeOutcome + = SquashMerged { repository: RepositoryEnvelope, reference: RepositoryCommitRef } + + // CARRIED OUT OF merge_base UNCHANGED. Re-wording them here would fork the authority for what a + // missing base MEANS, and the wording is the operator's only handle on the remedy. + | SquashMergeBaseRefused { refusal: MergeBaseOutcome } + + // THE CONFLICTS ARE THE ANSWER, NOT AN ERROR STRING. This is the one refusal whose remedy is a + // human decision, so it carries the complete population manifest_merge produced -- a caller that + // received a count could not act, and one that received the first could not size the job. + | SquashMergeConflicted { conflicts: List } + + // A COMMIT NAMES A MANIFEST THE STORE CANNOT PRODUCE. Distinguished by side and by occupant kind, + // because "absent" is a missing object while "occupied by an authored source" is an identity + // collision or a corrupt row -- different damage, different investigation. + | SquashMergeRootMissing { side: MergeSideName, root: ObjectId } + | SquashMergeRootIsAuthoredSource { side: MergeSideName, root: ObjectId } + | SquashMergeRootIsSemanticNode { side: MergeSideName, root: ObjectId } + + // A REFERENCE THAT NAMES NO COMMIT. Reachable before any history is walked, so it is not a + // merge_base refusal and must not be reported as one. + | SquashMergeCommitMissing { side: MergeSideName, reference: RepositoryCommitRef } + + // THE MERGED MANIFEST WOULD NOT STORE. Kept apart from the mint refusals below because this + // happens BEFORE any commit is proposed: the corpus itself could not be written down. + | SquashMergeResultDuplicatePath { path: String } + | SquashMergeResultLocatorCollision { identity: ObjectId } + + // THE MINT REFUSED. Carried outward one arm per cause for the same reason as the base refusals: + // an invalid allocator is a corrupt envelope, a missing parent is a vanished target, a missing + // integration source is a vanished source. Three repairs, three arms. + | SquashMergeAllocatorInvalid + | SquashMergeMintParentMissing { parent: RepositoryCommitRef } + | SquashMergeMintIntegrationSourceMissing { source: RepositoryCommitRef } + | SquashMergeMintRootUnresolvable { root: ObjectId } + +// READING ONE SIDE'S MANIFEST IS ONE FUNCTION, USED THREE TIMES. Writing the resolution inline per +// side would put one rule in three places and let the copies drift, which is the redundancy DESIGN +// section 2 names -- and it is exactly how the "which side" fact gets dropped from one of them. +type MergeSideManifest + = MergeSideManifestRead { record: CorpusManifestRecord } + | MergeSideManifestRefused { outcome: SquashMergeOutcome } + +fn read_side_manifest( + repository: RepositoryEnvelope, + side: MergeSideName, + reference: RepositoryCommitRef, +) -> MergeSideManifest { + match commit_at_reference(commits: repository.commits, reference: reference) { + Absent => + MergeSideManifestRefused { + outcome: SquashMergeCommitMissing { side: side, reference: reference }, + } + Present { value: commit } => + match find_corpus_manifest_record(store: repository.store, identity: commit.root.locator) { + CorpusManifestFound(record) => MergeSideManifestRead { record: record } + CorpusManifestAbsent { identity: r } => + MergeSideManifestRefused { outcome: SquashMergeRootMissing { side: side, root: r } } + CorpusManifestIsAuthoredSource { identity: r } => + MergeSideManifestRefused { + outcome: SquashMergeRootIsAuthoredSource { side: side, root: r }, + } + CorpusManifestIsSemanticNode { identity: r } => + MergeSideManifestRefused { + outcome: SquashMergeRootIsSemanticNode { side: side, root: r }, + } + } + } +} + +// THE MINT'S REFUSALS ARE TRANSLATED ONE-TO-ONE AND NEVER MERGED. The three root arms collapse to a +// single SquashMergeMintRootUnresolvable deliberately and this is the one place a distinction is +// dropped: the root handed to the mint was minted BY THIS FUNCTION from the store one line earlier, +// so all three mean the same thing here -- the store did not keep what it just accepted. That is one +// fact about one store, not three populations a caller could act on differently. +fn carry_mint(mint: RepositoryCommitMint) -> SquashMergeOutcome { + match mint { + RepositoryCommitMinted { repository: r, reference: c } => + SquashMerged { repository: r, reference: c } + RepositoryCommitMintAllocatorInvalid { next_ordinal: _ } => SquashMergeAllocatorInvalid + RepositoryCommitMintParentMissing { parent: p } => SquashMergeMintParentMissing { parent: p } + RepositoryCommitMintIntegrationSourceMissing { source: s } => + SquashMergeMintIntegrationSourceMissing { source: s } + RepositoryCommitMintRootMissing { root: r } => SquashMergeMintRootUnresolvable { root: r } + RepositoryCommitMintRootIsAuthoredSource { root: r } => + SquashMergeMintRootUnresolvable { root: r } + RepositoryCommitMintRootIsSemanticNode { root: r } => + SquashMergeMintRootUnresolvable { root: r } + } +} + +// THE COMMIT IS MINTED ONTO THE STORE THE MANIFEST WAS WRITTEN INTO, never onto the caller's +// repository value. Minting against the pre-store envelope would produce a commit whose root names a +// manifest that repository does not contain -- a dangling root written by the one operation that +// knows better. +fn commit_merged_manifest( + repository: RepositoryEnvelope, + target: RepositoryCommitRef, + source: RepositoryCommitRef, + message: String, + entries: List, +) -> SquashMergeOutcome { + match store_corpus_manifest(store: repository.store, entries: entries) { + CorpusManifestDuplicatePath { path: p } => + SquashMergeResultDuplicatePath { path: p as String } + CorpusManifestLocatorCollision { identity: i, existing: _, incoming: _ } => + SquashMergeResultLocatorCollision { identity: i } + CorpusManifestStored { store: stored, manifest: reference } => + carry_mint( + mint: mint_repository_commit( + repository: RepositoryEnvelope { + store: stored, + commits: repository.commits, + commit_allocator: repository.commit_allocator, + checked_out: repository.checked_out, + staged: repository.staged, + }, + root: CorpusManifestTarget { locator: reference.locator }, + message: message, + // THE PARENT IS THE TARGET AND ONLY THE TARGET. A squash records ONE lineage edge, and the + // source is recorded as CONSUMED rather than as a second parent -- which is what makes the + // operator's "kill dev history, never rebase" workflow the shape of the model instead of a + // convention layered over it. The source is not lost: SquashIntegrated below is precisely + // the record merge_base reads to refuse the second merge. + parent: Present { value: target }, + integration: SquashIntegrated { source: source }, + ) + ) + } +} + +// THE VERB. Base, then manifests, then decision, then commit -- and each step's refusal leaves +// immediately, so no later step ever runs against a value an earlier step declined to vouch for. +fn squash_merge( + repository: RepositoryEnvelope, + target: RepositoryCommitRef, + source: RepositoryCommitRef, + message: String, +) -> SquashMergeOutcome { + match merge_base(commits: repository.commits, target: target, source: source) { + MergeBaseSourceAlreadyConsumed { recorded_at: a, consumed: b, source: c } => + SquashMergeBaseRefused { + refusal: MergeBaseSourceAlreadyConsumed { recorded_at: a, consumed: b, source: c }, + } + MergeBaseHistoryUnwalkable { side: s, walk: w } => + SquashMergeBaseRefused { refusal: MergeBaseHistoryUnwalkable { side: s, walk: w } } + MergeBaseHistoriesDisjoint { target: t, source: s } => + SquashMergeBaseRefused { refusal: MergeBaseHistoriesDisjoint { target: t, source: s } } + MergeBaseDerived { base: base_ref } => + match read_side_manifest(repository: repository, side: MergeBaseCommit, reference: base_ref) { + MergeSideManifestRefused { outcome: o } => o + MergeSideManifestRead { record: base_manifest } => + match read_side_manifest( + repository: repository, + side: MergeSourceCommit, + reference: source, + ) { + MergeSideManifestRefused { outcome: o } => o + MergeSideManifestRead { record: source_manifest } => + match read_side_manifest( + repository: repository, + side: MergeTargetCommit, + reference: target, + ) { + MergeSideManifestRefused { outcome: o } => o + MergeSideManifestRead { record: target_manifest } => + match merge_manifests( + base: base_manifest, + source: source_manifest, + target: target_manifest, + ) { + ManifestConflicted { conflicts: c } => SquashMergeConflicted { conflicts: c } + ManifestMerged { entries: e } => + commit_merged_manifest( + repository: repository, + target: target, + source: source, + message: message, + entries: e, + ) + } + } + } + } + } +} diff --git a/dag/test/claim/scm/scm_merge_base_witness_test.dag b/dag/test/claim/scm/scm_merge_base_witness_test.dag index 7a2b154b6e9..e8518592484 100644 --- a/dag/test/claim/scm/scm_merge_base_witness_test.dag +++ b/dag/test/claim/scm/scm_merge_base_witness_test.dag @@ -59,8 +59,9 @@ import gunbc.scm.repository_envelope { RepositoryDecoded, RepositoryDecodeRefused, } -import gunbc.scm.staging { - StagedEntries, StagedEntriesRefused, staged_entries, +import test.fixture.scm_repository_builder { + MbBuild, MbBuilt, MbSetupFailed, + mb_start, mb_stage, mb_commit, mb_at, mb_head, mb_root_of, } import gunbc.scm.merge_base { MergeBaseOutcome, @@ -75,147 +76,6 @@ import gunbc.scm.merge_base { data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -// THE FIXTURE IS FALLIBLE FOR THE REASON THE STAGING FIXTURE'S HEADER GIVES AND THIS FILE INHERITS -// RATHER THAN RESTATES: a setup step that failed must stop the claim, never hand it a substitute -// specimen. Here the hazard is sharper than usual, because a fixture that silently declined to record -// an integration would leave a repository in which the consumed join CORRECTLY finds nothing -- and -// the refusal control would go green while asserting the opposite of what it claims to test. -type MbBuild - = MbBuilt { repository: RepositoryEnvelope, at: RepositoryCommitRef? } - | MbSetupFailed - -fn mb_start() -> MbBuild { - MbBuilt { - repository: RepositoryEnvelope { - store: empty_store(), - commits: [], - commit_allocator: MintedIdAllocator { next_ordinal: 0 }, - checked_out: none, - staged: none, - }, - at: none, - } -} - -// The manifest is built from the CURRENTLY STAGED entries so a later stage of a second path keeps the -// first, which is what makes S2 a content-descendant of S1 rather than a replacement of it. -fn mb_stage(build: MbBuild, path: String, text: String) -> MbBuild { - match build { - MbSetupFailed => MbSetupFailed - MbBuilt { repository: repository, at: at } => - match staged_entries(repository: repository) { - StagedEntriesRefused { cause: _ } => MbSetupFailed - StagedEntries { entries: entries } => - match store_authored_source(store: repository.store, text: text) { - SourceLocatorCollision { identity: _, existing: _, incoming: _ } => MbSetupFailed - SourceStored { store: with_source, source: source } => - match store_corpus_manifest( - store: with_source, - entries: concat( - filter(entries, fn(e) { (e.path as String) != path }), - [CorpusManifestEntry { - path: path as NonEmptyStr, - source: AuthoredSourceTarget { locator: source.locator }, - }], - ), - ) { - CorpusManifestDuplicatePath { path: _ } => MbSetupFailed - CorpusManifestLocatorCollision { identity: _, existing: _, incoming: _ } => MbSetupFailed - CorpusManifestStored { store: with_manifest, manifest: manifest } => - MbBuilt { - repository: RepositoryEnvelope { - store: with_manifest, - commits: repository.commits, - commit_allocator: repository.commit_allocator, - checked_out: repository.checked_out, - staged: Present { value: manifest }, - }, - at: at, - } - } - } - } - } -} - -fn mb_commit(build: MbBuild, message: String, integration: CommitIntegration) -> MbBuild { - match build { - MbSetupFailed => MbSetupFailed - MbBuilt { repository: repository, at: at } => - match repository.staged { - Absent => MbSetupFailed - Present { value: candidate } => - match mint_repository_commit( - repository: repository, - root: CorpusManifestTarget { locator: candidate.locator }, - message: message, - parent: at, - integration: integration, - ) { - RepositoryCommitMinted { repository: minted, reference: reference } => - MbBuilt { - repository: RepositoryEnvelope { - store: minted.store, - commits: minted.commits, - commit_allocator: minted.commit_allocator, - checked_out: Present { value: reference }, - staged: Present { value: candidate }, - }, - at: Present { value: reference }, - } - RepositoryCommitMintAllocatorInvalid { next_ordinal: _ } => MbSetupFailed - RepositoryCommitMintRootMissing { root: _ } => MbSetupFailed - RepositoryCommitMintRootIsAuthoredSource { root: _ } => MbSetupFailed - RepositoryCommitMintRootIsSemanticNode { root: _ } => MbSetupFailed - RepositoryCommitMintParentMissing { parent: _ } => MbSetupFailed - RepositoryCommitMintIntegrationSourceMissing { source: _ } => MbSetupFailed - } - } - } -} - -// MOVING THE CURSOR AND THE STAGE TOGETHER, because a branch point is both. Re-pointing `at` without -// re-pointing the stage would leave the next commit's content derived from the OTHER lineage's tip, -// which would build a fixture nobody could reach and quietly change what the claims are about. -fn mb_at(build: MbBuild, target: RepositoryCommitRef) -> MbBuild { - match build { - MbSetupFailed => MbSetupFailed - MbBuilt { repository: repository, at: _ } => - match commit_at_reference(commits: repository.commits, reference: target) { - Absent => MbSetupFailed - Present { value: c } => - MbBuilt { - repository: RepositoryEnvelope { - store: repository.store, - commits: repository.commits, - commit_allocator: repository.commit_allocator, - checked_out: Present { value: target }, - staged: Present { value: c.root }, - }, - at: Present { value: target }, - } - } - } -} - -fn mb_head(build: MbBuild) -> RepositoryCommitRef? { - match build { - MbSetupFailed => none - MbBuilt { repository: _, at: at } => at - } -} - -fn mb_root_of(build: MbBuild, reference: RepositoryCommitRef) -> ObjectId? { - match build { - MbSetupFailed => none - MbBuilt { repository: repository, at: _ } => - match commit_at_reference(commits: repository.commits, reference: reference) { - Absent => none - Present { value: c } => Present { value: c.root.locator } - } - } -} - // ONE SCENE, BUILT ONCE, ASSERTED MANY TIMES. Every claim below reads the same construction because // the discriminating facts are RELATIONS BETWEEN its commits -- that I1's root equals S1's while S2's // does not, that both share C0 with the target -- and a per-claim rebuild would let those relations diff --git a/dag/test/claim/scm/scm_squash_merge_witness_test.dag b/dag/test/claim/scm/scm_squash_merge_witness_test.dag new file mode 100644 index 00000000000..9de01d7182f --- /dev/null +++ b/dag/test/claim/scm/scm_squash_merge_witness_test.dag @@ -0,0 +1,377 @@ +module test.claim.scm_squash_merge_witness + +// CONTROLS FOR THE MERGE VERB, WRITTEN TO WHAT A COMPOSITION GETS WRONG. +// +// THE TWO HALVES ARE ALREADY CONTROLLED ELSEWHERE and are not re-asserted here: merge_base's +// resurrection refusal has its own witness, and manifest_merge's four-line law has its own. What is +// unproven until this file exists is that the JOIN preserves them -- that the verb actually consults +// the base derivation rather than merging against a convenient commit, that a conflict stops the +// commit rather than being counted and passed over, and that the squash records the source as +// consumed so the SECOND merge is refused by the first one's receipt. +// +// THE FAILURE THIS SURFACE PRODUCES IS A SUCCESSFUL MERGE. Every wrong composition below returns a +// well-formed repository with a well-formed new commit; none of them throws. So no claim here +// asserts "a merge happened" -- each states the mutation it refutes. + +import std.types { Bool, String, List, Int, NonEmptyStr } +import std.minted_identity { MintedId, MintedIdAllocator } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.scm.object_store { ObjectId, object_id_eq } +import gunbc.scm.integration { NoSquashIntegration, SquashIntegrated } +import gunbc.scm.ancestry { RepositoryCommitRef, RootCommit, DescendsFrom, repository_commit_ref_eq } +import gunbc.scm.repository_envelope { RepositoryEnvelope, commit_at_reference } +import gunbc.scm.staging { StagedEntries, StagedEntriesRefused, staged_entries } +import gunbc.scm.merge_base { + MergeBaseOutcome, MergeBaseDerived, MergeBaseSourceAlreadyConsumed, + MergeBaseHistoryUnwalkable, MergeBaseHistoriesDisjoint, +} +import gunbc.scm.manifest_merge { ManifestPathConflict, PathState, PathAbsent, PathPresent } +import gunbc.scm.squash_merge { + SquashMergeOutcome, + SquashMerged, + SquashMergeBaseRefused, + SquashMergeConflicted, + SquashMergeRootMissing, + SquashMergeRootIsAuthoredSource, + SquashMergeRootIsSemanticNode, + SquashMergeCommitMissing, + SquashMergeResultDuplicatePath, + SquashMergeResultLocatorCollision, + SquashMergeAllocatorInvalid, + SquashMergeMintParentMissing, + SquashMergeMintIntegrationSourceMissing, + SquashMergeMintRootUnresolvable, + MergeSideName, MergeBaseCommit, MergeSourceCommit, MergeTargetCommit, + squash_merge, +} +import test.fixture.scm_repository_builder { + MbBuild, MbBuilt, MbSetupFailed, + mb_start, mb_stage, mb_commit, mb_at, mb_head, mb_root_of, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE SCENE IS A DIVERGENCE, NOT A FAST-FORWARD, and the distinction is load-bearing. If the target +// had not moved since the base, taking the source's manifest wholesale would be correct, and every +// claim below would pass against an implementation that ignores the base entirely. Both sides +// therefore move, and they move on DIFFERENT paths so the merge is mergeable: +// +// C0 a = A0 the shared base +// T1 a = A0, t = T0 parent C0 the target adds its own path +// S1 a = A0, s = S0 parent C0 the source adds a different path +// +// The correct merge of T1 and S1 holds all three paths. An implementation that took the source's +// manifest as the answer loses `t`; one that took the target's loses `s`; one that merged against +// the wrong base can lose either. +type Scene + = Scene { build: MbBuild, base: RepositoryCommitRef, target: RepositoryCommitRef, source: RepositoryCommitRef } + | SceneUnavailable + +fn scene() -> Scene { + let c0 = mb_commit( + build: mb_stage(build: mb_start(), path: "a", text: "A0"), + message: "base", + integration: NoSquashIntegration, + ) + match mb_head(build: c0) { + Absent => SceneUnavailable + Present { value: base } => + let t1 = mb_commit( + build: mb_stage(build: c0, path: "t", text: "T0"), + message: "target", + integration: NoSquashIntegration, + ) + match mb_head(build: t1) { + Absent => SceneUnavailable + Present { value: target } => + let s1 = mb_commit( + build: mb_stage(build: mb_at(build: t1, target: base), path: "s", text: "S0"), + message: "source", + integration: NoSquashIntegration, + ) + match mb_head(build: s1) { + Absent => SceneUnavailable + Present { value: source } => + Scene { build: s1, base: base, target: target, source: source } + } + } + } +} + +fn scene_repository(s: Scene) -> RepositoryEnvelope? { + match s { + SceneUnavailable => none + Scene { build: b, base: _, target: _, source: _ } => + match b { + MbSetupFailed => none + MbBuilt { repository: r, at: _ } => Present { value: r } + } + } +} + +// READING THE COMMITTED CORPUS BACK OUT THROUGH THE ORDINARY STAGING READER rather than through the +// outcome value. A claim that inspected the entries it had just handed to the merge would assert +// that the merge returned its own argument; this asserts what the REPOSITORY now contains. +fn paths_after(repository: RepositoryEnvelope, at: RepositoryCommitRef) -> List { + match commit_at_reference(commits: repository.commits, reference: at) { + Absent => [] + Present { value: c } => + match staged_entries( + repository: RepositoryEnvelope { + store: repository.store, + commits: repository.commits, + commit_allocator: repository.commit_allocator, + checked_out: repository.checked_out, + staged: Present { value: c.root }, + } + ) { + StagedEntriesRefused { cause: _ } => [] + StagedEntries { entries: entries } => map(entries, e => e.path as String) + } + } +} + +// A CONFLICT WHOSE THREE SIDES ARE ALL PRESENT is what a modify-versus-modify looks like, and the +// claim states it rather than asserting a count, because a conflict reported with a fabricated +// absence would still be one conflict on one path. +fn state_is_present(state: PathState) -> Bool { + match state { + PathAbsent => false + PathPresent { source: _ } => true + } +} + +fn conflict_is_all_present(conflict: ManifestPathConflict, path: String) -> Bool { + (conflict.path as String) == path + && state_is_present(state: conflict.base) + && state_is_present(state: conflict.source) + && state_is_present(state: conflict.target) +} + +fn holds(paths: List, path: String) -> Bool { + fold(paths, init: false, f: fn(found, p) { found || p == path }) +} + +// THE MERGE TAKES BOTH SIDES' WORK, WHICH IS THE ONE THING A WRONG COMPOSITION CANNOT FAKE. Taking +// either side's manifest wholesale produces a valid repository and a valid commit; it just silently +// drops the other side's file. +test fn scm_sm_a_merge_carries_both_sides_paths() -> Bool { + match scene() { + SceneUnavailable => false + Scene { build: _, base: _, target: target, source: source } => + match scene_repository(s: scene()) { + Absent => false + Present { value: repository } => + match squash_merge( + repository: repository, + target: target, + source: source, + message: "merge", + ) { + SquashMerged { repository: merged, reference: at } => + let paths = paths_after(repository: merged, at: at) + count(paths) == 3 + && holds(paths: paths, path: "a") + && holds(paths: paths, path: "t") + && holds(paths: paths, path: "s") + SquashMergeConflicted { conflicts: _ } => false + SquashMergeBaseRefused { refusal: _ } => false + SquashMergeRootMissing { side: _, root: _ } => false + SquashMergeRootIsAuthoredSource { side: _, root: _ } => false + SquashMergeRootIsSemanticNode { side: _, root: _ } => false + SquashMergeCommitMissing { side: _, reference: _ } => false + SquashMergeResultDuplicatePath { path: _ } => false + SquashMergeResultLocatorCollision { identity: _ } => false + SquashMergeAllocatorInvalid => false + SquashMergeMintParentMissing { parent: _ } => false + SquashMergeMintIntegrationSourceMissing { source: _ } => false + SquashMergeMintRootUnresolvable { root: _ } => false + } + } + } +} + +// THE RESULT'S PARENT IS THE TARGET AND ITS INTEGRATION NAMES THE SOURCE. This is the operator's +// squash workflow as a structural fact rather than a convention: ONE lineage edge, and the source +// recorded as consumed rather than as a second parent. An implementation that parented the merge on +// the SOURCE also produces a valid repository holding all three paths, so the previous claim does +// not separate it from this one. +test fn scm_sm_the_result_parents_the_target_and_records_the_source_consumed() -> Bool { + match scene() { + SceneUnavailable => false + Scene { build: _, base: _, target: target, source: source } => + match scene_repository(s: scene()) { + Absent => false + Present { value: repository } => + match squash_merge( + repository: repository, + target: target, + source: source, + message: "merge", + ) { + SquashMerged { repository: merged, reference: at } => + match commit_at_reference(commits: merged.commits, reference: at) { + Absent => false + Present { value: c } => + match c.integration { + NoSquashIntegration => false + SquashIntegrated { source: recorded } => + repository_commit_ref_eq(left: recorded, right: source) + && match c.ancestry { + RootCommit => false + DescendsFrom { parent: p } => + repository_commit_ref_eq(left: p, right: target) + } + } + } + SquashMergeConflicted { conflicts: _ } => false + SquashMergeBaseRefused { refusal: _ } => false + SquashMergeRootMissing { side: _, root: _ } => false + SquashMergeRootIsAuthoredSource { side: _, root: _ } => false + SquashMergeRootIsSemanticNode { side: _, root: _ } => false + SquashMergeCommitMissing { side: _, reference: _ } => false + SquashMergeResultDuplicatePath { path: _ } => false + SquashMergeResultLocatorCollision { identity: _ } => false + SquashMergeAllocatorInvalid => false + SquashMergeMintParentMissing { parent: _ } => false + SquashMergeMintIntegrationSourceMissing { source: _ } => false + SquashMergeMintRootUnresolvable { root: _ } => false + } + } + } +} + +// MERGING THE SAME SOURCE TWICE IS REFUSED BY THE FIRST MERGE'S OWN RECEIPT, and it is refused +// THROUGH THE BASE DERIVATION rather than by a check this module added. That is what makes the +// composition load-bearing: a verb that derived its base by any other route would merge again +// happily, and the resurrection merge_base exists to prevent would arrive through the verb. +test fn scm_sm_merging_the_same_source_twice_is_refused_by_the_first_merges_receipt() -> Bool { + match scene() { + SceneUnavailable => false + Scene { build: _, base: _, target: target, source: source } => + match scene_repository(s: scene()) { + Absent => false + Present { value: repository } => + match squash_merge( + repository: repository, + target: target, + source: source, + message: "merge", + ) { + SquashMerged { repository: merged, reference: at } => + match squash_merge( + repository: merged, + target: at, + source: source, + message: "merge again", + ) { + SquashMergeBaseRefused { refusal: r } => + match r { + MergeBaseSourceAlreadyConsumed { recorded_at: rec, consumed: cons, source: _ } => + repository_commit_ref_eq(left: rec, right: at) + && repository_commit_ref_eq(left: cons, right: source) + MergeBaseDerived { base: _ } => false + MergeBaseHistoryUnwalkable { side: _, walk: _ } => false + MergeBaseHistoriesDisjoint { target: _, source: _ } => false + } + SquashMerged { repository: _, reference: _ } => false + SquashMergeConflicted { conflicts: _ } => false + SquashMergeRootMissing { side: _, root: _ } => false + SquashMergeRootIsAuthoredSource { side: _, root: _ } => false + SquashMergeRootIsSemanticNode { side: _, root: _ } => false + SquashMergeCommitMissing { side: _, reference: _ } => false + SquashMergeResultDuplicatePath { path: _ } => false + SquashMergeResultLocatorCollision { identity: _ } => false + SquashMergeAllocatorInvalid => false + SquashMergeMintParentMissing { parent: _ } => false + SquashMergeMintIntegrationSourceMissing { source: _ } => false + SquashMergeMintRootUnresolvable { root: _ } => false + } + SquashMergeConflicted { conflicts: _ } => false + SquashMergeBaseRefused { refusal: _ } => false + SquashMergeRootMissing { side: _, root: _ } => false + SquashMergeRootIsAuthoredSource { side: _, root: _ } => false + SquashMergeRootIsSemanticNode { side: _, root: _ } => false + SquashMergeCommitMissing { side: _, reference: _ } => false + SquashMergeResultDuplicatePath { path: _ } => false + SquashMergeResultLocatorCollision { identity: _ } => false + SquashMergeAllocatorInvalid => false + SquashMergeMintParentMissing { parent: _ } => false + SquashMergeMintIntegrationSourceMissing { source: _ } => false + SquashMergeMintRootUnresolvable { root: _ } => false + } + } + } +} + +// A CONFLICT STOPS THE LINE. The scene is re-cut so both sides modify the SAME path to different +// content, which the four-line law refuses. What this claim adds over manifest_merge's own controls +// is that the refusal REACHES THE REPOSITORY: no commit is minted, the conflict population arrives +// intact, and the commit list is unchanged -- a verb that counted the conflicts and committed the +// mergeable remainder would produce a corpus neither author wrote. +test fn scm_sm_a_conflicting_path_mints_no_commit() -> Bool { + let c0 = mb_commit( + build: mb_stage(build: mb_start(), path: "a", text: "A0"), + message: "base", + integration: NoSquashIntegration, + ) + match mb_head(build: c0) { + Absent => false + Present { value: base } => + let t1 = mb_commit( + build: mb_stage(build: c0, path: "a", text: "TARGET"), + message: "target", + integration: NoSquashIntegration, + ) + match mb_head(build: t1) { + Absent => false + Present { value: target } => + let s1 = mb_commit( + build: mb_stage(build: mb_at(build: t1, target: base), path: "a", text: "SOURCE"), + message: "source", + integration: NoSquashIntegration, + ) + match mb_head(build: s1) { + Absent => false + Present { value: source } => + match s1 { + MbSetupFailed => false + MbBuilt { repository: repository, at: _ } => + let before = count(repository.commits) + match squash_merge( + repository: repository, + target: target, + source: source, + message: "merge", + ) { + SquashMergeConflicted { conflicts: conflicts } => + count(conflicts) == 1 + && count(repository.commits) == before + && fold(conflicts, init: false, f: fn(seen, c) { + seen || conflict_is_all_present(conflict: c, path: "a") + }) + SquashMerged { repository: _, reference: _ } => false + SquashMergeBaseRefused { refusal: _ } => false + SquashMergeRootMissing { side: _, root: _ } => false + SquashMergeRootIsAuthoredSource { side: _, root: _ } => false + SquashMergeRootIsSemanticNode { side: _, root: _ } => false + SquashMergeCommitMissing { side: _, reference: _ } => false + SquashMergeResultDuplicatePath { path: _ } => false + SquashMergeResultLocatorCollision { identity: _ } => false + SquashMergeAllocatorInvalid => false + SquashMergeMintParentMissing { parent: _ } => false + SquashMergeMintIntegrationSourceMissing { source: _ } => false + SquashMergeMintRootUnresolvable { root: _ } => false + } + } + } + } + } +} + +test fn scm_squash_merge_witnesses_hold() -> Bool { + scm_sm_a_merge_carries_both_sides_paths() + && scm_sm_the_result_parents_the_target_and_records_the_source_consumed() + && scm_sm_merging_the_same_source_twice_is_refused_by_the_first_merges_receipt() + && scm_sm_a_conflicting_path_mints_no_commit() +} diff --git a/dag/test/fixture/scm_repository_builder.dag b/dag/test/fixture/scm_repository_builder.dag new file mode 100644 index 00000000000..930729c044b --- /dev/null +++ b/dag/test/fixture/scm_repository_builder.dag @@ -0,0 +1,182 @@ +module test.fixture.scm_repository_builder + +// BUILDING A REPOSITORY BY THE OPERATIONS THAT ACTUALLY BUILD ONE, FOR EVERY CLAIM THAT NEEDS ONE. +// +// This was authored inside the merge_base witness and then needed verbatim by the squash_merge +// witness. Copying it would have put one construction rule in two files and let them drift -- and the +// drift would be invisible, because each copy would go on passing its own claims while the two +// fixtures quietly stopped describing the same repository. That is the redundancy DESIGN section 2 +// names, so the builder moved here and both witnesses read it. +// +// NOTHING HERE FORGES A COMMIT. Every row is produced by store_authored_source, +// store_corpus_manifest and mint_repository_commit, so a fixture cannot construct a repository the +// real operations could not produce -- which is what makes a claim over one of these scenes evidence +// about the product rather than about the fixture. + +import std.types { Bool, String, List, Int, NonEmptyStr } +import std.minted_identity { MintedId, MintedIdAllocator } +import gunbc.scm.object_store { + ObjectStore, ObjectId, empty_store, + CorpusManifestEntry, CorpusManifestObjectRef, CorpusManifestTarget, + CorpusManifestStored, CorpusManifestDuplicatePath, CorpusManifestLocatorCollision, + store_corpus_manifest, + SourceStored, SourceLocatorCollision, store_authored_source, + AuthoredSourceTarget, +} +import gunbc.scm.integration { CommitIntegration } +import gunbc.scm.ancestry { RepositoryCommitRef } +import gunbc.scm.repository_envelope { + RepositoryEnvelope, + RepositoryCommit, + RepositoryCommitMinted, + RepositoryCommitMintAllocatorInvalid, + RepositoryCommitMintRootIsAuthoredSource, + RepositoryCommitMintRootIsSemanticNode, + RepositoryCommitMintRootMissing, + RepositoryCommitMintParentMissing, + RepositoryCommitMintIntegrationSourceMissing, + mint_repository_commit, + commit_at_reference, +} +import gunbc.scm.staging { StagedEntries, StagedEntriesRefused, staged_entries } + +// THE FIXTURE IS FALLIBLE FOR THE REASON THE STAGING FIXTURE'S HEADER GIVES AND THIS FILE INHERITS +// RATHER THAN RESTATES: a setup step that failed must stop the claim, never hand it a substitute +// specimen. Here the hazard is sharper than usual, because a fixture that silently declined to record +// an integration would leave a repository in which the consumed join CORRECTLY finds nothing -- and +// the refusal control would go green while asserting the opposite of what it claims to test. +type MbBuild + = MbBuilt { repository: RepositoryEnvelope, at: RepositoryCommitRef? } + | MbSetupFailed + +fn mb_start() -> MbBuild { + MbBuilt { + repository: RepositoryEnvelope { + store: empty_store(), + commits: [], + commit_allocator: MintedIdAllocator { next_ordinal: 0 }, + checked_out: none, + staged: none, + }, + at: none, + } +} + +// The manifest is built from the CURRENTLY STAGED entries so a later stage of a second path keeps the +// first, which is what makes S2 a content-descendant of S1 rather than a replacement of it. +fn mb_stage(build: MbBuild, path: String, text: String) -> MbBuild { + match build { + MbSetupFailed => MbSetupFailed + MbBuilt { repository: repository, at: at } => + match staged_entries(repository: repository) { + StagedEntriesRefused { cause: _ } => MbSetupFailed + StagedEntries { entries: entries } => + match store_authored_source(store: repository.store, text: text) { + SourceLocatorCollision { identity: _, existing: _, incoming: _ } => MbSetupFailed + SourceStored { store: with_source, source: source } => + match store_corpus_manifest( + store: with_source, + entries: concat( + filter(entries, fn(e) { (e.path as String) != path }), + [CorpusManifestEntry { + path: path as NonEmptyStr, + source: AuthoredSourceTarget { locator: source.locator }, + }], + ), + ) { + CorpusManifestDuplicatePath { path: _ } => MbSetupFailed + CorpusManifestLocatorCollision { identity: _, existing: _, incoming: _ } => MbSetupFailed + CorpusManifestStored { store: with_manifest, manifest: manifest } => + MbBuilt { + repository: RepositoryEnvelope { + store: with_manifest, + commits: repository.commits, + commit_allocator: repository.commit_allocator, + checked_out: repository.checked_out, + staged: Present { value: manifest }, + }, + at: at, + } + } + } + } + } +} + +fn mb_commit(build: MbBuild, message: String, integration: CommitIntegration) -> MbBuild { + match build { + MbSetupFailed => MbSetupFailed + MbBuilt { repository: repository, at: at } => + match repository.staged { + Absent => MbSetupFailed + Present { value: candidate } => + match mint_repository_commit( + repository: repository, + root: CorpusManifestTarget { locator: candidate.locator }, + message: message, + parent: at, + integration: integration, + ) { + RepositoryCommitMinted { repository: minted, reference: reference } => + MbBuilt { + repository: RepositoryEnvelope { + store: minted.store, + commits: minted.commits, + commit_allocator: minted.commit_allocator, + checked_out: Present { value: reference }, + staged: Present { value: candidate }, + }, + at: Present { value: reference }, + } + RepositoryCommitMintAllocatorInvalid { next_ordinal: _ } => MbSetupFailed + RepositoryCommitMintRootMissing { root: _ } => MbSetupFailed + RepositoryCommitMintRootIsAuthoredSource { root: _ } => MbSetupFailed + RepositoryCommitMintRootIsSemanticNode { root: _ } => MbSetupFailed + RepositoryCommitMintParentMissing { parent: _ } => MbSetupFailed + RepositoryCommitMintIntegrationSourceMissing { source: _ } => MbSetupFailed + } + } + } +} + +// MOVING THE CURSOR AND THE STAGE TOGETHER, because a branch point is both. Re-pointing `at` without +// re-pointing the stage would leave the next commit's content derived from the OTHER lineage's tip, +// which would build a fixture nobody could reach and quietly change what the claims are about. +fn mb_at(build: MbBuild, target: RepositoryCommitRef) -> MbBuild { + match build { + MbSetupFailed => MbSetupFailed + MbBuilt { repository: repository, at: _ } => + match commit_at_reference(commits: repository.commits, reference: target) { + Absent => MbSetupFailed + Present { value: c } => + MbBuilt { + repository: RepositoryEnvelope { + store: repository.store, + commits: repository.commits, + commit_allocator: repository.commit_allocator, + checked_out: Present { value: target }, + staged: Present { value: c.root }, + }, + at: Present { value: target }, + } + } + } +} + +fn mb_head(build: MbBuild) -> RepositoryCommitRef? { + match build { + MbSetupFailed => none + MbBuilt { repository: _, at: at } => at + } +} + +fn mb_root_of(build: MbBuild, reference: RepositoryCommitRef) -> ObjectId? { + match build { + MbSetupFailed => none + MbBuilt { repository: repository, at: _ } => + match commit_at_reference(commits: repository.commits, reference: reference) { + Absent => none + Present { value: c } => Present { value: c.root.locator } + } + } +} From 85e6ef312347b3da9cdfda9b437f4012f0b6090d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 20:11:48 +0000 Subject: [PATCH 4/7] Hoist the refusal-arm rationale to module-item grain, and give the local guard the domain it was missing The floor lane refused 20 section 4c violations in squash_merge.dag: rationale written BETWEEN the arms of SquashMergeOutcome, and one note inside a call argument list. Only module-item grain is modeled. The per-arm reasoning is worth keeping, so it moves into one table above the type rather than being deleted. AND THE LOCAL GUARD REPORTED ZERO, FOR THE THIRD TIME AND THE THIRD DIFFERENT REASON. It enumerated with `git ls-files`, which lists TRACKED files only, and the new module was untracked when the guard ran -- so it opened every file except the one the change added, which is the only file that could have been newly wrong. The first version classified by what FOLLOWED an annotation block and missed in-body comments. The second keyed on column zero, which was right, and was controlled against a known-bad specimen -- but the control only proved the PREDICATE, and the defect this time was the DOMAIN. A detector's domain is as load-bearing as its test, and nothing I had run would have told me otherwise, because a detector that never opens a file reports the same "0" as one that opens it and finds nothing clean. Fixed to enumerate tracked AND untracked, and re-controlled the honest way: the repaired guard reproduces all 20 of CI's violations at CI's line numbers, then reads 0 after the repair. The reproduction against the failing specimen is the part that was missing, not the clean read. Witnesses unchanged and still 5/5; this cut moves prose, not behaviour. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/scm/squash_merge.dag | 50 ++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/dag/gunbc/scm/squash_merge.dag b/dag/gunbc/scm/squash_merge.dag index 8034084c2fd..403e926ebf2 100644 --- a/dag/gunbc/scm/squash_merge.dag +++ b/dag/gunbc/scm/squash_merge.dag @@ -80,37 +80,46 @@ type MergeSideName | MergeSourceCommit | MergeTargetCommit +// THE ARMS, AND WHY EACH IS ITS OWN ARM RATHER THAN A FIELD ON A SHARED ONE: +// +// SquashMergeBaseRefused carried out of merge_base UNCHANGED. Re-wording it here would +// fork the authority for what a missing base MEANS, and that +// wording is the operator's only handle on the remedy. +// SquashMergeConflicted the conflicts ARE the answer, not an error string. This is the +// one refusal whose remedy is a human decision, so it carries the +// complete population manifest_merge produced: a caller given a +// count could not act, and one given the first could not size the +// job. +// SquashMergeRoot* a commit names a manifest the store cannot produce. +// Distinguished by side AND by occupant kind, because "absent" is +// a missing object while "occupied by an authored source" is an +// identity collision or a corrupt row -- different damage, +// different investigation. +// SquashMergeCommitMissing a reference naming no commit. Reachable BEFORE any history is +// walked, so it is not a merge_base refusal and must not be +// reported as one. +// SquashMergeResult* the merged manifest would not store. Kept apart from the mint +// arms below because this happens before any commit is proposed: +// the corpus itself could not be written down. +// SquashMergeAllocatorInvalid a corrupt envelope. +// SquashMergeMintParentMissing a vanished target. +// SquashMergeMintIntegration... a vanished source. type SquashMergeOutcome = SquashMerged { repository: RepositoryEnvelope, reference: RepositoryCommitRef } - // CARRIED OUT OF merge_base UNCHANGED. Re-wording them here would fork the authority for what a - // missing base MEANS, and the wording is the operator's only handle on the remedy. | SquashMergeBaseRefused { refusal: MergeBaseOutcome } - // THE CONFLICTS ARE THE ANSWER, NOT AN ERROR STRING. This is the one refusal whose remedy is a - // human decision, so it carries the complete population manifest_merge produced -- a caller that - // received a count could not act, and one that received the first could not size the job. | SquashMergeConflicted { conflicts: List } - // A COMMIT NAMES A MANIFEST THE STORE CANNOT PRODUCE. Distinguished by side and by occupant kind, - // because "absent" is a missing object while "occupied by an authored source" is an identity - // collision or a corrupt row -- different damage, different investigation. | SquashMergeRootMissing { side: MergeSideName, root: ObjectId } | SquashMergeRootIsAuthoredSource { side: MergeSideName, root: ObjectId } | SquashMergeRootIsSemanticNode { side: MergeSideName, root: ObjectId } - // A REFERENCE THAT NAMES NO COMMIT. Reachable before any history is walked, so it is not a - // merge_base refusal and must not be reported as one. | SquashMergeCommitMissing { side: MergeSideName, reference: RepositoryCommitRef } - // THE MERGED MANIFEST WOULD NOT STORE. Kept apart from the mint refusals below because this - // happens BEFORE any commit is proposed: the corpus itself could not be written down. | SquashMergeResultDuplicatePath { path: String } | SquashMergeResultLocatorCollision { identity: ObjectId } - // THE MINT REFUSED. Carried outward one arm per cause for the same reason as the base refusals: - // an invalid allocator is a corrupt envelope, a missing parent is a vanished target, a missing - // integration source is a vanished source. Three repairs, three arms. | SquashMergeAllocatorInvalid | SquashMergeMintParentMissing { parent: RepositoryCommitRef } | SquashMergeMintIntegrationSourceMissing { source: RepositoryCommitRef } @@ -171,6 +180,12 @@ fn carry_mint(mint: RepositoryCommitMint) -> SquashMergeOutcome { } } +// THE PARENT IS THE TARGET AND ONLY THE TARGET. A squash records ONE lineage edge, and the source is +// recorded as CONSUMED rather than as a second parent -- which is what makes the operator's "kill dev +// history, never rebase" workflow the shape of the model instead of a convention layered over it. The +// source is not lost: the SquashIntegrated below is precisely the record merge_base reads to refuse +// the second merge. +// // THE COMMIT IS MINTED ONTO THE STORE THE MANIFEST WAS WRITTEN INTO, never onto the caller's // repository value. Minting against the pre-store envelope would produce a commit whose root names a // manifest that repository does not contain -- a dangling root written by the one operation that @@ -199,11 +214,6 @@ fn commit_merged_manifest( }, root: CorpusManifestTarget { locator: reference.locator }, message: message, - // THE PARENT IS THE TARGET AND ONLY THE TARGET. A squash records ONE lineage edge, and the - // source is recorded as CONSUMED rather than as a second parent -- which is what makes the - // operator's "kill dev history, never rebase" workflow the shape of the model instead of a - // convention layered over it. The source is not lost: SquashIntegrated below is precisely - // the record merge_base reads to refuse the second merge. parent: Present { value: target }, integration: SquashIntegrated { source: source }, ) From 5073531e6209662e6f0b2958eb47c079fc1aea78 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 20:58:29 +0000 Subject: [PATCH 5/7] Declare the nine namespace deltas the fixture extraction produced The floor lane refused the merge-verb branch with nine unadjudicated namespace-wave-admission deltas. All nine are mine and the wall is correct: moving a declaration between modules is a membership motion, and this roster exists so it is DECLARED rather than done quietly. WHAT MOVED AND WHY. test.claim.scm_merge_base_witness authored a repository builder -- MbBuild with its arms MbBuilt and MbSetupFailed, and the six operations mb_start, mb_stage, mb_commit, mb_at, mb_head, mb_root_of -- that constructs scenes through the real store and mint instead of forging rows. The squash-merge witness needs it VERBATIM. Copying it would put one construction rule in two files and the drift would be INVISIBLE: each copy would keep passing its own claims while the two fixtures quietly stopped describing the same repository. So it rehomes to test.fixture.scm_repository_builder, which is where this repository already puts fixtures shared across claims. NINE BINDINGS, ONE MODULE, ONE CHANGE CLASS: seven inside mb_scene and two inside scm_mb_the_scene_holds_the_root_relations_the_controls_depend_on. Every spelling is identical on both sides and only the declaring module differs, which is exactly the motion TargetChanged names. Nothing is requalified. THE EVIDENCE THAT THE MOVE PRESERVES BEHAVIOUR IS EXECUTED, NOT ASSERTED: all twelve merge_base claims pass unchanged against the shared fixture. That is the right positive control for a rehome, because a builder that had silently changed would surface as a claim that stopped discriminating rather than as a compile error -- the fixture still compiles either way. Each row names the exact (module, in_declaration, spelling, target) tuple and admits nothing else, and the trigger is the rows' own death: when this PR merges, base and head bind every spelling identically, no run can produce these deltas, and all nine report CONSUMED, due for deletion on the roster's next touch. That deletion is to be adjudicated by joining each row against main's tree on its own tuple, not by trusting this sentence. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/stage0/src/namespace_wave_admission.rs | 125 ++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index 64bd684ebb5..099f323a4cf 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -1559,7 +1559,132 @@ const PROBE_CAPTURE_REHOME_LABEL: &str = "gunbc#10639 serving-tree cut: SparkServingProbeCapture and its arms move from the deleted \ gunbc.spark.serving_terminal_health to their only reader, gunbc.spark.training_ready"; +/// THE SCM REPOSITORY BUILDER MOVES TO A SHARED FIXTURE (2026-09-06, gunbc#10676). No ordinal is +/// claimed, for the reason the entries above give. +/// +/// `test.claim.scm_merge_base_witness` authored a repository builder -- `MbBuild` with its two arms +/// `MbBuilt` and `MbSetupFailed`, and the six operations `mb_start`, `mb_stage`, `mb_commit`, +/// `mb_at`, `mb_head`, `mb_root_of` -- to construct scenes through the real store and mint rather +/// than by forging rows. The squash-merge verb's witness needs that construction VERBATIM. Copying +/// it would put one construction rule in two files, and the drift would be INVISIBLE: each copy +/// would keep passing its own claims while the two fixtures quietly stopped describing the same +/// repository (DESIGN.md §2). So the builder is rehomed to `test.fixture.scm_repository_builder`, +/// which is where this repository already puts fixtures shared across claims, and both witnesses +/// import it. +/// +/// NINE BINDINGS IN ONE MODULE resolve to the new declarer, which is `TargetChanged` and is not +/// auto-admitted: seven inside `mb_scene` and two inside +/// `scm_mb_the_scene_holds_the_root_relations_the_controls_depend_on`. Every spelling is identical +/// on both sides; only the declaring module differs, which is the membership motion this roster +/// exists to adjudicate. +/// +/// ONE CHANGE CLASS, AND NOTHING IS REQUALIFIED. No spelling changes, no behaviour changes, and the +/// evidence that the move is behaviour-preserving is executed rather than asserted: all twelve +/// `scm_merge_base_witness` claims pass unchanged against the shared fixture. That is the positive +/// control for a rehome -- a builder that had silently changed would show up as a claim that +/// stopped discriminating, not as a compile error. +/// +/// TRIGGER, AND IT IS THESE ROWS' OWN DEATH: they go when gunbc#10676 merges. Main then declares +/// the builder in `test.fixture.scm_repository_builder`, base and head bind each spelling +/// identically, and all nine report CONSUMED, coming due on this roster's next touch. Adjudicate +/// that deletion by joining each row against main's tree on its own +/// (module, in_declaration, spelling, target) tuple, not by trusting this sentence. +const SCM_REPOSITORY_BUILDER_REHOME_LABEL: &str = + "gunbc#10676 scm fixture extraction: the repository builder moves from \ + test.claim.scm_merge_base_witness to test.fixture.scm_repository_builder, so the merge_base \ + and squash_merge witnesses read one construction rule instead of two copies"; + pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "MbBuilt", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "MbSetupFailed", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "mb_start", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "mb_stage", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "mb_commit", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "mb_at", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "mb_scene", + spelling: "mb_head", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "scm_mb_the_scene_holds_the_root_relations_the_controls_depend_on", + spelling: "MbBuilt", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: SCM_REPOSITORY_BUILDER_REHOME_LABEL, + subject: AdmissionSubject::Binding { + module: "test.claim.scm_merge_base_witness", + in_declaration: "scm_mb_the_scene_holds_the_root_relations_the_controls_depend_on", + spelling: "mb_root_of", + target: "test.fixture.scm_repository_builder", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, TransitionAdmission { label: PROBE_CAPTURE_REHOME_LABEL, subject: AdmissionSubject::Binding { From 316b7d9f80ebe97474b2e94dfff9c29110154e13 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 6 Sep 2026 21:45:34 +0000 Subject: [PATCH 6/7] Dissolve the four consumed gunbc#10671 rows, on the roster touch they named The floor lane admitted this branch's nine fixture-rehome rows and then refused on a different count: four CONSUMED admissions due for deletion on this roster-touching change. That is the roster's own discipline working. gunbc#10671 merged, so its cable-leg rows can no longer be produced by any run, and they come due on the next change that touches this file -- which is this one. ADJUDICATED BY THE JOIN THOSE ROWS DEMANDED RATHER THAN BY THEIR OWN SENTENCE. The entries say in as many words not to trust the sentence, so the deletion was decided against main's tree in all three directions the join has: - product.cable_leg_observation DECLARES SecondaryNotObserved, as an arm of its compliance coproduct. - extdeps.transceiver.sff_8636 does NOT declare it. Its only surviving occurrence of the spelling is PROSE recording that an earlier head authored it -- which is the trap a grep count falls into and a declaration check does not. A count would have read 1 and I would have concluded the old declarer was still live and left four dead rows standing. - Both consumers -- test.claim.cable_leg_coding_witness and test.claim.cable_order_admission_witness -- import the spelling from the new declarer. So base and head bind it identically, no run can produce those four deltas, and CONSUMED is the correct reading rather than an author error. The const goes with its rows; the compiler confirms nothing else referenced it. The dissolution is recorded in the file, in the form the file already uses, so the next author inherits the adjudication rather than the conclusion. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/stage0/src/namespace_wave_admission.rs | 56 +++++-------------- 1 file changed, 13 insertions(+), 43 deletions(-) diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index 3ff71349aa0..044caef5d10 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -1560,9 +1560,6 @@ pub struct TransitionAdmission { /// the carrier in `product.cable_leg_observation`, base and head bind each spelling identically, /// and all four report CONSUMED, coming due on this roster's next touch. Adjudicate that deletion /// by joining each row against main's tree on its own tuple, not by trusting this sentence. -const LEG_OBSERVATION_REHOME_LABEL: &str = - "gunbc#10671 transceiver layer split: the cable-leg observation carrier moves from the \ - SFF-8636 byte-meaning module extdeps.transceiver.sff_8636 to product.cable_leg_observation"; /// THE SCM REPOSITORY BUILDER MOVES TO A SHARED FIXTURE (2026-09-06, gunbc#10676). No ordinal is /// claimed, for the reason the entries above give. @@ -1594,6 +1591,19 @@ const LEG_OBSERVATION_REHOME_LABEL: &str = /// identically, and all nine report CONSUMED, coming due on this roster's next touch. Adjudicate /// that deletion by joining each row against main's tree on its own /// (module, in_declaration, spelling, target) tuple, not by trusting this sentence. +/// THE gunbc#10671 ROWS DISSOLVED HERE (2026-09-06), BY THEIR OWN TRIGGER AND ON THE ROSTER TOUCH +/// THEY NAMED. gunbc#10671 merged, so the four cable-leg rows reported CONSUMED and came due on the +/// next roster-touching change, which is this one. +/// +/// ADJUDICATED BY THE JOIN THOSE ROWS DEMANDED RATHER THAN BY THEIR OWN SENTENCE, in all three +/// directions the join has. On main, `product.cable_leg_observation` DECLARES `SecondaryNotObserved` +/// as an arm of its compliance coproduct; `extdeps.transceiver.sff_8636` does NOT declare it -- its +/// only remaining occurrence of the spelling is prose recording that an earlier head authored it, +/// which is exactly the trap a grep-count would have fallen into and a declaration check does not; +/// and both consumers, `test.claim.cable_leg_coding_witness` and +/// `test.claim.cable_order_admission_witness`, import the spelling from the new declarer. So base and +/// head bind it identically, no run can produce those four deltas, and CONSUMED is the correct +/// reading rather than an author error. const SCM_REPOSITORY_BUILDER_REHOME_LABEL: &str = "gunbc#10676 scm fixture extraction: the repository builder moves from \ test.claim.scm_merge_base_witness to test.fixture.scm_repository_builder, so the merge_base \ @@ -1690,46 +1700,6 @@ pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ }, disposition: NamespaceDeltaDisposition::TargetChanged, }, - TransitionAdmission { - label: LEG_OBSERVATION_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.cable_leg_coding_witness", - in_declaration: "delivered_fs_leg", - spelling: "SecondaryNotObserved", - target: "product.cable_leg_observation", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: LEG_OBSERVATION_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.cable_leg_coding_witness", - in_declaration: "leg_with_unmodelled_code", - spelling: "SecondaryNotObserved", - target: "product.cable_leg_observation", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: LEG_OBSERVATION_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.cable_order_admission_witness", - in_declaration: "correctly_coded_leg", - spelling: "SecondaryNotObserved", - target: "product.cable_leg_observation", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: LEG_OBSERVATION_REHOME_LABEL, - subject: AdmissionSubject::Binding { - module: "test.claim.cable_order_admission_witness", - in_declaration: "delivered_leg", - spelling: "SecondaryNotObserved", - target: "product.cable_leg_observation", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, ]; /// The denominators a green must name (DESIGN §5): a run that cannot say what it covered is an From 16b6c84c5bf03c5366754dcd852641ec08c68e7d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 7 Sep 2026 01:10:09 +0000 Subject: [PATCH 7/7] Remove the root question the store already answered, instead of answering it more elegantly Side-chat ruling on the one judgement this branch flagged for overturning, and it overturned BOTH options I offered rather than picking one. WHAT I HAD. carry_mint folded mint_repository_commit's three root refusals into a single SquashMergeMintRootUnresolvable, arguing that on this route all three mean "the store did not keep what it just accepted". WHY THAT IS WRONG, VERIFIED AGAINST THE CODE RATHER THAN ACCEPTED. store_corpus_manifest returning CorpusManifestStored { store, manifest } already establishes that store holds a manifest object at that locator -- an absent or wrong-kind locator would have returned the store's own refusal instead. commit_merged_manifest then mints against THAT store with THAT locator, and the mint's three root refusals are exactly the three non-success arms of find_corpus_manifest_record, which the preceding success has excluded. So the arms are UNREACHABLE, and the collapse fabricated a public cause no execution can produce. It was wrong a second way that matters more. It reasoned about THIS CALLER'S CONTEXT INSIDE A TRANSLATOR THAT CANNOT SEE IT: handed a RepositoryCommitMint, nothing tells you the value came from a store call one line earlier. And the three are not one fact even in the impossible case -- a missing root means the object vanished, while a wrong-kind root means the locator now denotes something else, which contradicts a collision-aware insertion far more strongly. WHY KEEPING THEM DISTINCT WAS ALSO REFUSED, which is the part I had not seen: it would be honest about the CAUSE and still dishonest about the DOMAIN, leaving three states in SquashMergeOutcome that no run of squash_merge can reach. SO THE QUESTION IS REMOVED. mint_commit_from_stored_manifest consumes the CorpusManifestObjectRef the store branded, runs every other admission -- allocator, integration anchor preexistence, parent existence -- and returns BrandedRootMint, which has no root arms. mint_repository_commit resolves the root and then delegates, so the admission rules have ONE authority rather than two copies free to drift, and a caller holding only a locator still gets all three refusals because for that caller they are reachable and real. Rung 4: the invalid state has no constructor here. TWO OF MY OWN ERRORS ON THE WAY, BOTH CAUGHT BY EXECUTION. I deleted integration_anchor_resolves, which sat inside the region I replaced -- the compiler caught it. And my first narrow projection mapped the impossible root arms onto a fabricated allocator cause, committing the exact sin the ruling names, one level down. Removed by making mint_repository_commit_admitted return the narrow type directly, since it performs no admission and can only mint. 448/0 across the SCM witnesses on the merged tree. REVIEW STANDING, STATED PLAINLY: the three approvals on this PR were all given against 316b7d9f80e, which still carried the collapsed arm. None of them has seen this commit, and this one touches repository_envelope, a load-bearing module. The tally on this PR currently overstates its review coverage. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/scm/repository_envelope.dag | 158 +++++++++++++----- dag/gunbc/scm/squash_merge.dag | 60 +++---- .../scm/scm_squash_merge_witness_test.dag | 6 - 3 files changed, 148 insertions(+), 76 deletions(-) diff --git a/dag/gunbc/scm/repository_envelope.dag b/dag/gunbc/scm/repository_envelope.dag index b4a06048d92..76d66ef85bd 100644 --- a/dag/gunbc/scm/repository_envelope.dag +++ b/dag/gunbc/scm/repository_envelope.dag @@ -552,6 +552,101 @@ type RepositoryCommitMint // mint could produce a result and its supposed consumed source in one motion -- a self-consistent // repository whose provenance describes an event that could not have happened, and whose consumed // join would then refuse or admit on a record nothing ever integrated. +// It answers with the UNRESOLVABLE ANCHOR rather than a Bool, because the refusal has to name which +// reference could not be found and a Bool would force the caller to rediscover it. +fn integration_anchor_resolves( + repository: RepositoryEnvelope, + integration: CommitIntegration, +) -> RepositoryCommitRef? { + match integration { + NoSquashIntegration => none + SquashIntegrated { source: s } => + match commit_at_reference(commits: repository.commits, reference: s) { + Present { value: _ } => none + Absent => Present { value: s } + } + } +} + +// A ROOT THE STORE ITSELF JUST BRANDED HAS NOTHING LEFT TO RESOLVE, so this route cannot refuse for +// root resolution and its outcome type does not carry the arms. +// +// THE ROUTE EXISTS BECAUSE A CALLER CAN HOLD STRONGER EVIDENCE THAN `mint_repository_commit` +// ACCEPTS. That function takes a `CorpusManifestTarget`, which is a PROPOSITION about a locator, so +// its return type honestly carries the three ways resolving that proposition can fail. But a caller +// that has just received `CorpusManifestStored { store, manifest }` does not hold a proposition: it +// holds the `CorpusManifestObjectRef` THE STORE HANDED BACK, for an object that store demonstrably +// contains -- had the locator been absent or occupied by another kind, the store call would have +// returned its own refusal instead. Re-asking `find_corpus_manifest_record` there is asking a +// question that has already been answered, and then having to say something about an answer that +// cannot arrive. +// +// THE ALTERNATIVE THAT WAS BUILT FIRST AND REJECTED was for the caller to keep the generic route and +// TRANSLATE the three impossible root refusals into one coarser cause. That is worse than it looks. +// It fabricates a public arm no execution can produce, and it does so by REASONING ABOUT THE +// CALLER'S CONTEXT INSIDE A FUNCTION THAT CANNOT SEE IT -- a translator handed a +// `RepositoryCommitMint` has no evidence its argument came from the store one line earlier. And the +// three arms are not one fact even in the impossible case: a missing root would mean the object +// vanished, while a wrong-kind root would mean the locator now denotes something else, which +// contradicts a collision-aware insertion far more strongly. Collapsing them would erase the +// evidence needed to tell which invariant had failed. +// +// So the question is REMOVED rather than answered more elegantly, which is DESIGN section 5's +// construction over validation and section 4b's top rung: the invalid state has no constructor on +// this route. +// +// EVERY OTHER ADMISSION STILL RUNS. This is not a fast path around the mint's rules -- the allocator, +// the integration anchor's preexistence and the parent's existence are all still decided here, and +// `mint_repository_commit` now reaches them THROUGH this function rather than beside it, so there is +// one authority for those rules rather than two copies free to drift. +type BrandedRootMint + = BrandedRootMinted { repository: RepositoryEnvelope, reference: RepositoryCommitRef } + | BrandedRootAllocatorInvalid { next_ordinal: Int } + | BrandedRootParentMissing { parent: RepositoryCommitRef } + | BrandedRootIntegrationSourceMissing { source: RepositoryCommitRef } + +fn mint_commit_from_stored_manifest( + repository: RepositoryEnvelope, + root: CorpusManifestObjectRef, + message: String, + parent: RepositoryCommitRef?, + integration: CommitIntegration, +) -> BrandedRootMint { + if repository.commit_allocator.next_ordinal < 0 { + BrandedRootAllocatorInvalid { next_ordinal: repository.commit_allocator.next_ordinal } + } else { + match integration_anchor_resolves(repository: repository, integration: integration) { + Present { value: missing } => BrandedRootIntegrationSourceMissing { source: missing } + Absent => + match parent { + Present { value: parent_ref } => + match commit_at_reference(commits: repository.commits, reference: parent_ref) { + Absent => BrandedRootParentMissing { parent: parent_ref } + Present { value: _ } => + mint_repository_commit_admitted( + repository: repository, + root: root, + message: message, + ancestry: DescendsFrom { parent: parent_ref }, + integration: integration, + ) + } + Absent => + mint_repository_commit_admitted( + repository: repository, + root: root, + message: message, + ancestry: RootCommit, + integration: integration, + ) + } + } + } +} + +// THE GENERIC ROUTE RESOLVES THE ROOT AND THEN DELEGATES, so the admission rules live in exactly one +// place. A caller holding only a locator still gets the three root refusals, because for that caller +// they are reachable and real. fn mint_repository_commit( repository: RepositoryEnvelope, root: CorpusManifestTarget, @@ -572,63 +667,42 @@ fn mint_repository_commit( CorpusManifestIsSemanticNode { identity: r } => RepositoryCommitMintRootIsSemanticNode { root: r } CorpusManifestFound(record) => - match integration_anchor_resolves(repository: repository, integration: integration) { - Present { value: missing } => - RepositoryCommitMintIntegrationSourceMissing { source: missing } - Absent => - match parent { - Present { value: parent_ref } => - match commit_at_reference(commits: repository.commits, reference: parent_ref) { - Absent => RepositoryCommitMintParentMissing { parent: parent_ref } - Present { value: _ } => - mint_repository_commit_admitted( - repository: repository, - root: record.identity, - message: message, - ancestry: DescendsFrom { parent: parent_ref }, - integration: integration, - ) - } - Absent => - mint_repository_commit_admitted( - repository: repository, - root: record.identity, - message: message, - ancestry: RootCommit, - integration: integration, - ) - } - } + widen_branded_root_mint( + mint: mint_commit_from_stored_manifest( + repository: repository, + root: record.identity, + message: message, + parent: parent, + integration: integration, + ) + ) } } } -// It answers with the UNRESOLVABLE ANCHOR rather than a Bool, because the refusal has to name which -// reference could not be found and a Bool would force the caller to rediscover it. -fn integration_anchor_resolves( - repository: RepositoryEnvelope, - integration: CommitIntegration, -) -> RepositoryCommitRef? { - match integration { - NoSquashIntegration => none - SquashIntegrated { source: s } => - match commit_at_reference(commits: repository.commits, reference: s) { - Present { value: _ } => none - Absent => Present { value: s } - } +fn widen_branded_root_mint(mint: BrandedRootMint) -> RepositoryCommitMint { + match mint { + BrandedRootMinted { repository: r, reference: c } => + RepositoryCommitMinted { repository: r, reference: c } + BrandedRootAllocatorInvalid { next_ordinal: n } => + RepositoryCommitMintAllocatorInvalid { next_ordinal: n } + BrandedRootParentMissing { parent: p } => RepositoryCommitMintParentMissing { parent: p } + BrandedRootIntegrationSourceMissing { source: s } => + RepositoryCommitMintIntegrationSourceMissing { source: s } } } + fn mint_repository_commit_admitted( repository: RepositoryEnvelope, root: CorpusManifestObjectRef, message: String, ancestry: CommitAncestry, integration: CommitIntegration, -) -> RepositoryCommitMint { +) -> BrandedRootMint { let allocation = mint_id(alloc: repository.commit_allocator) let reference = RepositoryCommitRef { identity: allocation.id } - RepositoryCommitMinted { + BrandedRootMinted { repository: RepositoryEnvelope { store: repository.store, commits: concat(repository.commits, [RepositoryCommit { diff --git a/dag/gunbc/scm/squash_merge.dag b/dag/gunbc/scm/squash_merge.dag index 403e926ebf2..2b38ad88bad 100644 --- a/dag/gunbc/scm/squash_merge.dag +++ b/dag/gunbc/scm/squash_merge.dag @@ -27,7 +27,7 @@ import gunbc.scm.object_store { ObjectId, CorpusManifestRecord, CorpusManifestEntry, - CorpusManifestTarget, + CorpusManifestObjectRef, store_corpus_manifest, CorpusManifestStored, @@ -59,16 +59,13 @@ import gunbc.scm.manifest_merge { import gunbc.scm.repository_envelope { RepositoryEnvelope, RepositoryCommit, - RepositoryCommitMint, - RepositoryCommitMinted, - RepositoryCommitMintAllocatorInvalid, - RepositoryCommitMintRootMissing, - RepositoryCommitMintRootIsAuthoredSource, - RepositoryCommitMintRootIsSemanticNode, - RepositoryCommitMintParentMissing, - RepositoryCommitMintIntegrationSourceMissing, + BrandedRootMint, + BrandedRootMinted, + BrandedRootAllocatorInvalid, + BrandedRootParentMissing, + BrandedRootIntegrationSourceMissing, commit_at_reference, - mint_repository_commit, + mint_commit_from_stored_manifest, } // WHICH SIDE'S ROOT FAILED TO RESOLVE IS PART OF THE FACT, NOT CONTEXT FOR A LOG LINE. Three commits @@ -104,6 +101,20 @@ type MergeSideName // SquashMergeAllocatorInvalid a corrupt envelope. // SquashMergeMintParentMissing a vanished target. // SquashMergeMintIntegration... a vanished source. +// +// THERE IS NO ROOT-RESOLUTION ARM ON THIS ROUTE, AND THAT IS THE POINT. An earlier head carried one, +// folding the generic mint's three root refusals into a single SquashMergeMintRootUnresolvable on the +// reasoning that they all meant "the store did not keep what it just accepted". That reasoning was +// wrong twice. It fabricated a public cause no execution can produce; and it reasoned about THIS +// caller's context inside a translator that cannot see it -- handed a mint result, nothing tells you +// it came from the store one line earlier. Keeping the three arms distinct instead would have been +// honest about the cause and still dishonest about the DOMAIN, leaving three states in this type that +// no run of `squash_merge` can reach. +// +// The question is removed rather than answered: `store_corpus_manifest` hands back a +// CorpusManifestObjectRef for an object that store demonstrably contains, and +// `mint_commit_from_stored_manifest` consumes that brand instead of re-resolving a locator. Root +// refusal is unrepresentable here because there is nothing left to resolve (DESIGN section 4b rung 4). type SquashMergeOutcome = SquashMerged { repository: RepositoryEnvelope, reference: RepositoryCommitRef } @@ -123,7 +134,6 @@ type SquashMergeOutcome | SquashMergeAllocatorInvalid | SquashMergeMintParentMissing { parent: RepositoryCommitRef } | SquashMergeMintIntegrationSourceMissing { source: RepositoryCommitRef } - | SquashMergeMintRootUnresolvable { root: ObjectId } // READING ONE SIDE'S MANIFEST IS ONE FUNCTION, USED THREE TIMES. Writing the resolution inline per // side would put one rule in three places and let the copies drift, which is the redundancy DESIGN @@ -159,24 +169,18 @@ fn read_side_manifest( } } -// THE MINT'S REFUSALS ARE TRANSLATED ONE-TO-ONE AND NEVER MERGED. The three root arms collapse to a -// single SquashMergeMintRootUnresolvable deliberately and this is the one place a distinction is -// dropped: the root handed to the mint was minted BY THIS FUNCTION from the store one line earlier, -// so all three mean the same thing here -- the store did not keep what it just accepted. That is one -// fact about one store, not three populations a caller could act on differently. -fn carry_mint(mint: RepositoryCommitMint) -> SquashMergeOutcome { +// THE MINT'S REFUSALS ARE CARRIED ONE-TO-ONE, AND NOW THERE ARE ONLY THREE TO CARRY. Nothing is +// translated, widened or merged here; the branded route's outcome type and this one have the same +// shape because they describe the same three ways a commit can fail to be minted once its root is +// settled. +fn carry_mint(mint: BrandedRootMint) -> SquashMergeOutcome { match mint { - RepositoryCommitMinted { repository: r, reference: c } => + BrandedRootMinted { repository: r, reference: c } => SquashMerged { repository: r, reference: c } - RepositoryCommitMintAllocatorInvalid { next_ordinal: _ } => SquashMergeAllocatorInvalid - RepositoryCommitMintParentMissing { parent: p } => SquashMergeMintParentMissing { parent: p } - RepositoryCommitMintIntegrationSourceMissing { source: s } => + BrandedRootAllocatorInvalid { next_ordinal: _ } => SquashMergeAllocatorInvalid + BrandedRootParentMissing { parent: p } => SquashMergeMintParentMissing { parent: p } + BrandedRootIntegrationSourceMissing { source: s } => SquashMergeMintIntegrationSourceMissing { source: s } - RepositoryCommitMintRootMissing { root: r } => SquashMergeMintRootUnresolvable { root: r } - RepositoryCommitMintRootIsAuthoredSource { root: r } => - SquashMergeMintRootUnresolvable { root: r } - RepositoryCommitMintRootIsSemanticNode { root: r } => - SquashMergeMintRootUnresolvable { root: r } } } @@ -204,7 +208,7 @@ fn commit_merged_manifest( SquashMergeResultLocatorCollision { identity: i } CorpusManifestStored { store: stored, manifest: reference } => carry_mint( - mint: mint_repository_commit( + mint: mint_commit_from_stored_manifest( repository: RepositoryEnvelope { store: stored, commits: repository.commits, @@ -212,7 +216,7 @@ fn commit_merged_manifest( checked_out: repository.checked_out, staged: repository.staged, }, - root: CorpusManifestTarget { locator: reference.locator }, + root: reference, message: message, parent: Present { value: target }, integration: SquashIntegrated { source: source }, diff --git a/dag/test/claim/scm/scm_squash_merge_witness_test.dag b/dag/test/claim/scm/scm_squash_merge_witness_test.dag index 9de01d7182f..0da0438ee96 100644 --- a/dag/test/claim/scm/scm_squash_merge_witness_test.dag +++ b/dag/test/claim/scm/scm_squash_merge_witness_test.dag @@ -40,7 +40,6 @@ import gunbc.scm.squash_merge { SquashMergeAllocatorInvalid, SquashMergeMintParentMissing, SquashMergeMintIntegrationSourceMissing, - SquashMergeMintRootUnresolvable, MergeSideName, MergeBaseCommit, MergeSourceCommit, MergeTargetCommit, squash_merge, } @@ -185,7 +184,6 @@ test fn scm_sm_a_merge_carries_both_sides_paths() -> Bool { SquashMergeAllocatorInvalid => false SquashMergeMintParentMissing { parent: _ } => false SquashMergeMintIntegrationSourceMissing { source: _ } => false - SquashMergeMintRootUnresolvable { root: _ } => false } } } @@ -235,7 +233,6 @@ test fn scm_sm_the_result_parents_the_target_and_records_the_source_consumed() - SquashMergeAllocatorInvalid => false SquashMergeMintParentMissing { parent: _ } => false SquashMergeMintIntegrationSourceMissing { source: _ } => false - SquashMergeMintRootUnresolvable { root: _ } => false } } } @@ -285,7 +282,6 @@ test fn scm_sm_merging_the_same_source_twice_is_refused_by_the_first_merges_rece SquashMergeAllocatorInvalid => false SquashMergeMintParentMissing { parent: _ } => false SquashMergeMintIntegrationSourceMissing { source: _ } => false - SquashMergeMintRootUnresolvable { root: _ } => false } SquashMergeConflicted { conflicts: _ } => false SquashMergeBaseRefused { refusal: _ } => false @@ -298,7 +294,6 @@ test fn scm_sm_merging_the_same_source_twice_is_refused_by_the_first_merges_rece SquashMergeAllocatorInvalid => false SquashMergeMintParentMissing { parent: _ } => false SquashMergeMintIntegrationSourceMissing { source: _ } => false - SquashMergeMintRootUnresolvable { root: _ } => false } } } @@ -361,7 +356,6 @@ test fn scm_sm_a_conflicting_path_mints_no_commit() -> Bool { SquashMergeAllocatorInvalid => false SquashMergeMintParentMissing { parent: _ } => false SquashMergeMintIntegrationSourceMissing { source: _ } => false - SquashMergeMintRootUnresolvable { root: _ } => false } } }