Implement #280 for fewer spurious merge conflicts in Dafny backend

SPEC_DAFNY.md

@@ -68,6 +68,8 @@ Non-pure functions become Dafny `method` declarations.
 
 On merge conflict, the original `foo.dfy` is restored and the merged result is saved as `foo.dfy.merged` for manual inspection. Conflicts and additions-only failures retain the old anchor. A verifier failure after a clean additions-only merge instead retains the new anchor, because the proof already contains that generation; the next retry must not merge it a second time.
 
+Merges use `--diff-algorithm=minimal`, matching the additions-only check so large proof additions do not cause spurious generated-line deletions in the diff. Git versions before 2.44 fall back to the default algorithm with a warning; upgrading avoids the resulting false conflicts. Git execution errors restore the proof and retain the old anchor, but do not create `.dfy.merged` or record a verification conflict.
+
 ---
 
 ## 4. Helper Preambles

tools/fixtures/regen-large-proof/LICENSE

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2015 David Khourshid
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

tools/fixtures/regen-large-proof/README.md

@@ -0,0 +1,14 @@
+# Large proof merge fixture
+
+Reduced from `packages/core/test/machine-model/formal/machineModel.dfy` and
+`.dfy.gen` in [robertpenner/xstate at e9042e7](https://github.com/robertpenner/xstate/tree/e9042e7/packages/core/test/machine-model/formal),
+using the proof-block layout described in [LemmaScript #280](https://github.com/midspiral/LemmaScript/issues/280).
+The upstream MIT license is included in `LICENSE`.
+
+`base.txt` has 32 generated lines; `proof.txt` preserves them with 513 inserted
+lines. Changing `below(candidate.node.path, kept.node.path)` to
+`below(kept.node.path, candidate.node.path)` conflicts with Git's default merge
+diff, but merges exactly with `--diff-algorithm=minimal` (Git 2.54.0).
+These are line-based merge inputs, not valid Dafny programs. Keep their blank
+lines, indentation, and LF line endings: repeated braces and the distance
+between matches are what exercise the diff heuristic.

tools/fixtures/regen-large-proof/base.txt

@@ -0,0 +1,32 @@
+  decreases |path|
+  var nodes := machine.nodes;
+  var selections := parallelSelections(machine, snapshot, event);
+    var selected := selections[0];
+    var result := selected.evaluation.result;
+          var updated := apply(snapshot.context, selected.evaluation);
+          var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+          ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+        else
+          var plan := parallelPlan(machine, snapshot.active, selected.id, i_target_val, reenter);
+          var exited := runLifecycle(nodes, plan.exits, snapshot.context, event, true);
+          var updated := apply(exited.context, selected.evaluation);
+          var entered := runLifecycle(nodes, plan.entries, updated.context, event, false);
+          ParallelStep(ParallelSnapshot(plan.active, entered.context), false, ((exited.reused && updated.reused) && entered.reused), ((exited.effects + updated.effects) + entered.effects))
+      case None =>
+        var updated := apply(snapshot.context, selected.evaluation);
+        var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+        ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+    }
+      }
+  }
+}
+  (overlaps(conflictExits(machine, active, candidate), conflictExits(machine, active, kept)) && !(below(candidate.node.path, kept.node.path)))
+  decreases |kept|
+  decreases |pending|
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+
+  decreases |selections|
+{
+    var entries := SeqFilter((id: string) => plansEnter(plans, id), machine.order);
+    var updated := applyAll(exited.context, kept);