Reproduced by hand against lib/git_engine.ml's exact invocation, git 2.55.0.
Nothing in the design or the code asserts any relationship between the candidate tree and the PR diffs it claims to contain. The only guard is git merge-base --is-ancestor <recorded_base> <pr_head> (git_engine.ml:70-84).
Given a recorded merge base that is a proper ancestor of the PR head but newer than the true fork point:
- the ancestry guard passes
merge-tree --write-tree exits 0- the candidate tree is missing one of the PR's two files
- the commit is non-empty, so an empty-commit post-condition does not catch it
Invariant 1 ("the exact validated tree became main") remains technically true and completely uninformative: it constrains which tree landed, never what is in it.
Honest scope: on the happy path the merge base is computed as merge-base(head, target tip), which would not produce this. The finding is "nothing would catch a wrong base," not "this happens today." The realistic injection point is M1's planned metadata adapters for tools with synthetic bases (ghstack), which supply the base from tool metadata rather than computing it.
The fix — state and implement the predicate
For each PR i, every path in diff(merge_base_i -> head_i) must appear in diff(parent_i -> synthetic_i) or be identically present on the left side. A tree walk over changed paths only, run after construction and before requesting validation.
Adjacent post-conditions to add in the same place
See docs/INVESTIGATION.md §6 Q3, §7 R1, §10.
Reproduced by hand against
lib/git_engine.ml's exact invocation, git 2.55.0.Nothing in the design or the code asserts any relationship between the candidate tree and the PR diffs it claims to contain. The only guard is
git merge-base --is-ancestor <recorded_base> <pr_head>(git_engine.ml:70-84).Given a recorded merge base that is a proper ancestor of the PR head but newer than the true fork point:
merge-tree --write-treeexits 0Invariant 1 ("the exact validated tree became main") remains technically true and completely uninformative: it constrains which tree landed, never what is in it.
Honest scope: on the happy path the merge base is computed as
merge-base(head, target tip), which would not produce this. The finding is "nothing would catch a wrong base," not "this happens today." The realistic injection point is M1's planned metadata adapters for tools with synthetic bases (ghstack), which supply the base from tool metadata rather than computing it.The fix — state and implement the predicate
For each PR i, every path in
diff(merge_base_i -> head_i)must appear indiff(parent_i -> synthetic_i)or be identically present on the left side. A tree walk over changed paths only, run after construction and before requesting validation.Adjacent post-conditions to add in the same place
git merge-base --all; refuse to build (or drop--merge-base) when it returns more than one OID — criss-cross merges currently pick one silently--attr-sourceexplicitly; decide which tree's.gitattributesgoverns rather than silently falling back to naive text merge--no-messagesand capture the conflicted-file stage listSee
docs/INVESTIGATION.md§6 Q3, §7 R1, §10.