lsc regen reports a conflict for a one-line generated change after a large proof block #280

This was generated by AI during triage.

Problem

lsc regen --backend=dafny merges a new generation into the proof file with git merge-file <dfy> <base> <gen> (tools/src/dafny-commands.ts:200). That call uses Git's default Myers diff. When a large handwritten proof block sits between two generated declarations, the default diff stops searching for the shortest edit script and treats some unchanged generated lines after the block as deleted from the .dfy and reinserted. If the new generation changes one of those lines, regen reports a conflict, restores the .dfy, and exits 1, even though no handwritten line touches the changed line.

The additions-only check in the same file already runs git diff --minimal (tools/src/dafny-commands.ts:54, added in 08fdfee), so the check and the merge disagree about which generated lines a .dfy kept. In the case below the check accepts the .dfy, and the merge then fails on it.

In that case the .dfy is the old generation plus 1,184 inserted proof lines, and it verifies. The only generation change is one line inside preempts. From the old generation to the .dfy, git diff --no-index reports 2,396 insertions and 95 deletions with the default algorithm, and 2,301 insertions and no deletions with --minimal, --histogram or --patience. With Git 2.50.1, git merge-file on the same three files conflicts with the default and with --diff-algorithm=myers. It merges cleanly with --diff-algorithm=minimal, histogram or patience, and the merged file differs from the .dfy only in the preempts line. The conflict hunk pairs the new preempts line with the body of an unrelated handwritten predicate, ChildrenActive.

Deleting lines from the three files until no single deletion preserves the conflict left 31 generated lines and 513 proof lines. A small hand-written example therefore does not reproduce it; the proof block has to be large.

Reproduced with LemmaScript 0.6.8 (36eb31d) and 0.6.6. The git merge-file call is unchanged on main at 6b18f23.

Reproduction

The model is public in robertpenner/xstate at e9042e7. That commit keeps all generated declarations contiguous. The script moves a 1,184-line proof block back between them, which is the layout that conflicted.

git clone https://github.com/robertpenner/xstate && cd xstate && git checkout e9042e7
cd packages/core/test/machine-model
f=formal/machineModel.dfy
{ sed -n '1,1181p' $f; sed -n '1379,2562p' $f; sed -n '1182,1378p' $f; sed -n '2563,$p' $f; } > tmp && mv tmp $f
lsc check --backend=dafny machineModel.ts   # 454 verified, 0 errors
sed -i.bak 's/!below(candidate.node.path, kept.node.path)/!below(kept.node.path, candidate.node.path)/' machineModel.ts
lsc regen --backend=dafny --no-verify machineModel.ts

Gen changed. Three-way merging...
CONFLICT: machineModel.dfy — merge had conflicts, dfy restored. See machineModel.dfy.merged

On Git 2.44 or later, git merge-file --diff-algorithm=histogram formal/machineModel.dfy formal/machineModel.dfy.base formal/machineModel.dfy.gen on the files regen leaves behind exits 0.

Expected

When the .dfy passes the additions-only check, a generation change merges without conflict unless a handwritten line actually overlaps the changed generated lines. Today the only workaround is to keep every generated declaration in one contiguous prefix of the .dfy, which forces proof text away from the code it is about.

Possible fixes, for the maintainers to choose:

• Pass --diff-algorithm=minimal or histogram to git merge-file. Git added the option in 2.44; Git 2.39 rejects it with exit 129, which the current e.status > 0 branch would report as a conflict, so this needs a version check or a fallback.
• Merge from the additions-only structure: a .dfy that passed the check contains the old generation as a subsequence, so regen could locate the old generated lines from that alignment instead of from a fresh text diff.

Acceptance criteria

• The reproduction above merges without conflict, and the merged .dfy differs from the original only in the preempts line.
• A regression test changes one generated line that follows a large inserted proof block and expects a clean merge.
• A real conflict, where a handwritten edit overlaps the changed generated lines, still exits 1 and writes .dfy.merged.
• If the fix uses a Git option, regen on a Git version without it either falls back to today's behavior or reports the version requirement. It must not report a conflict caused by the rejected option.