Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help


id: merge kind: intent checked_against_core: clear statement: “WHEN two branches derived from a common ancestor spec repo are joined, THE merge tool SHALL detect id collisions and reference breaks introduced by the union of their edits — using [[graph]]’s blast-radius query rather than re-deriving reachability independently — before reporting the merge complete, and SHALL never report success against a tree that [[linter.referential_integrity]] or [[linter.graph_shape]] would reject.”

Merge

A textually clean 3-way merge (no conflict markers) can still produce a semantically broken repo: two branches mint the same new id independently, or one branch renames an id (rename.md) while the other adds a fresh reference to the old name in a file the rename never touched. Git’s line-based merge can’t see either problem — both are clean at the text layer. This file specifies the check that runs after git’s merge succeeds: it reuses graph.md’s derived reachability rather than re-deriving it, and rename.md’s actual rewrite mechanism rather than inventing a second one, applied across two histories instead of one linear line — the “existing mechanism, new scope” move AGENTS.md #3a asks for before adding anything new.

Purpose

A textually clean 3-way merge (no conflict markers) can still produce a semantically broken repo: two branches mint the same new id independently, or one branch renames an id (rename.md) while the other adds a fresh reference to the old name in a file the rename never touched. Git’s line-based merge can’t see either problem — both are clean at the text layer. This file specifies the check that runs after git’s merge succeeds: it reuses graph.md’s derived reachability rather than re-deriving it, and rename.md’s actual rewrite mechanism rather than inventing a second one, applied across two histories instead of one linear line — the “existing mechanism, new scope” move AGENTS.md #3a asks for before adding anything new.

Constraints

| id | kind | expr | traces_to | satisfies | |——————————————|———–|––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––|–––––––––––| | graph_reused_not_rederived | invariant | merge's collision and blast-radius checks query [[graph]]'s artifact for both branch tips; merge never independently re-walks markdown for reachability | [[merge]] | | | no_new_id_collision | invariant | ∀ id ∈ index(branch_A) ∩ index(branch_B): id was already defined, identically, in the common ancestor — an id newly minted by both branches independently is a collision, not a merge | [[merge]] | | | blast_radii_recorded_pre_merge | invariant | before applying the union of edits, merge records [[graph]].blast_radius(touched_ids) for each branch separately, against the common ancestor's graph | [[merge]] | | | semantic_conflict_iff_blast_radius_intersects | invariant | blast_radius_A(touched_A) ∩ blast_radius_B(touched_B) ≠ ∅ ⟹ the merge requires human review, even when the two branches' literal file diffs don't overlap | [[merge]] | | | rename_replayed_onto_foreign_edits | invariant | if branch A contains a [[rename]] application of (old_id, new_id) and branch B independently adds a new [[old_id]] reference within blast_radius_A, the merge rewrites that reference to [[new_id]] using rename.md's own rewrite mechanism — it is never left dangling and never silently dropped | [[merge]] | | | post_merge_relint_required | invariant | merge is not reported passed until [[linter.referential_integrity]] and [[linter.graph_shape]] are re-run against the merged tree and both report passed | [[merge]] | | | sequential_number_reassigned_on_conflict | invariant | if both branches independently claim the same next sequential number (a CHANGELOG entry or Revision heading), the merge tool renumbers one of the two rather than allowing a silent duplicate | [[merge]] | | | collision_failure | effect | merge.collision_failure(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | reverification_failure | effect | merge.reverification_failure(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | merge_aborted | effect | merge.merge_aborted(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

  • diverged
  • collision_checked
  • needs_review
  • rename_replayed
  • ref_integrity_reverified
  • merged
  • collision_failed (emits: [[merge.collision_failure]])
  • reverification_failed (emits: [[merge.reverification_failure]])
  • merge_failed (emits: [[merge.merge_aborted]])

Transitions

idfromtoguard
check_collisionsdivergedcollision_checked[[merge.no_new_id_collision]] ∧ [[merge.graph_reused_not_rederived]]
collision_faildivergedcollision_failed¬([[merge.no_new_id_collision]] ∧ [[merge.graph_reused_not_rederived]])
flag_reviewcollision_checkedneeds_review[[merge.semantic_conflict_iff_blast_radius_intersects]] ∧ [[merge.blast_radii_recorded_pre_merge]]
auto_proceedcollision_checkedrename_replayed¬flag_review.guard ∧ [[merge.rename_replayed_onto_foreign_edits]]
resolvedneeds_reviewrename_replayeda human has explicitly approved merging the intersecting blast radii ∧ [[merge.rename_replayed_onto_foreign_edits]]
reverifyrename_replayedref_integrity_reverified[[merge.post_merge_relint_required]]
reverify_failrename_replayedreverification_failed¬([[merge.post_merge_relint_required]])
acceptref_integrity_reverifiedmerged[[merge.sequential_number_reassigned_on_conflict]]
rejectref_integrity_reverifiedmerge_failed¬([[merge.sequential_number_reassigned_on_conflict]])

Properties

idkindderives_fromgeneratorpredicate
collision_across_branches_rejectedunit[[merge.no_new_id_collision]]two_branches_each_independently_defining_new_id("x")check(merge) == failed
inherited_id_not_falsely_flaggedunit[[merge.no_new_id_collision]]id_defined_in_common_ancestor_unchanged_in_both_branches()check(merge) != failed
textually_clean_semantic_conflict_flaggedunit[[merge.semantic_conflict_iff_blast_radius_intersects]]branch_A(renames x to y), branch_B(adds a new [[x]] reference in a file branch_A never touched)check(merge) == needs_review
rename_replay_repairs_dangling_refunit[[merge.rename_replayed_onto_foreign_edits]]same scenario, after human approvalpost_merge_repo has zero occurrences of [[x]]; branch_B's new reference now reads [[y]]
disjoint_blast_radii_auto_mergeunit[[merge.semantic_conflict_iff_blast_radius_intersects]]two_branches_touching_disjoint_namespaces_with_disjoint_blast_radii()check(merge) == merged — no human review required
duplicate_sequential_number_renumberedunit[[merge.sequential_number_reassigned_on_conflict]]both_branches_add_a_CHANGELOG_entry_claiming_the_same_next_number()post_merge_repo has two distinct sequential numbers; neither is duplicated
relint_gates_mergeunit[[merge.post_merge_relint_required]]merge_where(linter.referential_integrity or linter.graph_shape: fails against the merged tree)check(merge) == failed — mirrors rename.md’s stray_ref_caught_by_verify
blast_radius_recorded_before_applyunit[[merge.blast_radii_recorded_pre_merge]]merge_history_where_edits_were_applied_before_both_branches'_radii_were_recorded()check(merge) == failed — apply never precedes the recording step, for either branch
reachability_from_graph_artifact_onlyunit[[merge.graph_reused_not_rederived]]merge_invoked_with_the_markdown_walker_patched_to_panic()merge of an otherwise-clean diverged repo succeeds — collision and blast-radius checks only query [[graph]]’s artifact
collision_failure_label_assertedunit[[merge.collision_failure]]collision_failure_raised()error_label == "merge.collision_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
reverification_failure_label_assertedunit[[merge.reverification_failure]]reverification_failure_raised()error_label == "merge.reverification_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
merge_aborted_label_assertedunit[[merge.merge_aborted]]merge_aborted_raised()error_label == "merge.merge_aborted" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)

Notes

checked_against_core: clear (see AGENTS.md’s convention). rename_replayed_onto_foreign_edits was checked against AGENTS.md #3a specifically before being added as a new row rather than reusing rename.md’s old_id_fully_replaced as-is: it isn’t a duplicate, because it operates over two divergent histories being joined, not one linear history — old_id_fully_replaced guarantees completeness within a single rename’s own transaction, and says nothing about a reference minted on a different branch that the rename operation never saw. This file’s constraint is what makes that reference get rewritten anyway, once the branches meet.

What this file doesn’t replace. Two edits to the same row’s own field on both branches is an ordinary textual conflict — git already marks it, already forces a human to resolve it, and nothing here changes that. This file exists only for the cases where the text merge is clean but the result isn’t: id collisions and rename/reference splits that don’t overlap a single line.

Depends on graph.md, not a local reachability walk. Every blast-radius computation in this file’s Constraints is a graph query, computed once against the common ancestor for each branch (blast_radii_recorded_pre_merge) rather than recomputed after the union is applied — recomputing post-union would already have mixed the two branches’ edges together and lost the ability to tell which branch’s change reached which id.

Depends on rename.md, not a second rewrite mechanism. resolved/ auto_proceed’s rewrite step calls the same rewrite rename.md’s apply transition performs — this file only decides when a cross-branch replay is required, never how the rewrite itself works.

Decision of record (2026-09-30, user-approved; HITL ticket specodelic-mp1 row 2): “a human has explicitly approved” means an explicit, attributable, recorded human decision by the operator — a deliberate approve step (never inferred, timed-out into, or defaulted) whose decision lands in the repo’s decision trail (change notes / ticket). No CI gate or role requirement is assumed: the format describes tool contracts, not hosting policy, and an implementation may layer a gate or role on top, but the floor the resolved guard checks is the attributable operator decision itself. CI gates and roles were deliberately excluded — both presume infrastructure the spec cannot see, whereas a recorded operator decision is checkable by the merge lifecycle itself. This paragraph records the decision; constraint text is unchanged, same treatment as rename.md’s batch-rename decision.

Resolved question (was Needs Human Review): what “a human has explicitly approved” (the resolved transition’s guard) means operationally is now decided — see the decision of record above. The mechanism-agnostic floor stands: an attributable operator decision, recorded in the repo’s decision trail; gates and roles are layers an implementation may add, not assumptions the format makes.

Open question, relationship to refactor.md: a blast-radius intersection that triggers needs_review here may also be exactly the “unrelated fan-in” shape refactor.md flags as a tidy-first candidate — both files answer different questions (can this merge proceed safely, vs. should this node be split before more changes land on it) and are deliberately left as two files rather than merged into one, but a same-session finding from both on the same node is worth surfacing together rather than as two unrelated notices. Left open rather than wired automatically.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: collision_across_branches_rejected

  • WHEN two_branches_each_independently_defining_new_id("x")
  • THEN check(merge) == failed
  • VERIFIES [[merge.collision_across_branches_rejected]]

Scenario: inherited_id_not_falsely_flagged

  • WHEN id_defined_in_common_ancestor_unchanged_in_both_branches()
  • THEN check(merge) != failed
  • VERIFIES [[merge.inherited_id_not_falsely_flagged]]

Scenario: textually_clean_semantic_conflict_flagged

  • WHEN branch_A(renames x to y), branch_B(adds a new [[x]] reference in a file branch_A never touched)
  • THEN check(merge) == needs_review
  • VERIFIES [[merge.textually_clean_semantic_conflict_flagged]]

Scenario: rename_replay_repairs_dangling_ref

  • WHEN same scenario, after human approval
  • THEN post_merge_repo has zero occurrences of [[x]]; branch_B's new reference now reads [[y]]
  • VERIFIES [[merge.rename_replay_repairs_dangling_ref]]

Scenario: disjoint_blast_radii_auto_merge

  • WHEN two_branches_touching_disjoint_namespaces_with_disjoint_blast_radii()
  • THEN check(merge) == merged — no human review required
  • VERIFIES [[merge.disjoint_blast_radii_auto_merge]]

Scenario: duplicate_sequential_number_renumbered

  • WHEN both_branches_add_a_CHANGELOG_entry_claiming_the_same_next_number()
  • THEN post_merge_repo has two distinct sequential numbers; neither is duplicated
  • VERIFIES [[merge.duplicate_sequential_number_renumbered]]

Scenario: relint_gates_merge

  • WHEN merge_where(linter.referential_integrity or linter.graph_shape: fails against the merged tree)
  • THEN check(merge) == failed — mirrors rename.md’s stray_ref_caught_by_verify
  • VERIFIES [[merge.relint_gates_merge]]

Scenario: blast_radius_recorded_before_apply

  • WHEN merge_history_where_edits_were_applied_before_both_branches'_radii_were_recorded()
  • THEN check(merge) == failed — apply never precedes the recording step, for either branch
  • VERIFIES [[merge.blast_radius_recorded_before_apply]]

Scenario: reachability_from_graph_artifact_only

  • WHEN merge_invoked_with_the_markdown_walker_patched_to_panic()
  • THEN merge of an otherwise-clean diverged repo succeeds — collision and blast-radius checks only query [[graph]]’s artifact
  • VERIFIES [[merge.reachability_from_graph_artifact_only]]

Scenario: collision_failure_label_asserted

  • WHEN collision_failure_raised()
  • THEN error_label == "merge.collision_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[merge.collision_failure_label_asserted]]

Scenario: reverification_failure_label_asserted

  • WHEN reverification_failure_raised()
  • THEN error_label == "merge.reverification_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[merge.reverification_failure_label_asserted]]

Scenario: merge_aborted_label_asserted

  • WHEN merge_aborted_raised()
  • THEN error_label == "merge.merge_aborted" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[merge.merge_aborted_label_asserted]]