From 6c93ef22780e149293e901b5342b8c64687463dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Wed, 6 May 2026 13:59:46 -0600
Subject: [PATCH 1/8] Ignore `dstep` to prove `addsnake` termination
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The manhattan distance from a node towards the algorithm's end point (lena, lenb)
is used as termination metric for `addsnake`. Phantom parameters for both
input lengths are introduced to provide them as arguments to the metric.

The diagonal predicate `DiagPred` is a refinement type alias encoding the
condition of an equality predicate (such as `canDiag`) to enter the recursive call
inside `addsnake`. This allows Liquid Haskell to know that both coordinates
are smaller than its corresponding input length, those fulfilling
`manhattanDistance` preconditions.

`dstep` is extended to provide the required phantom parameters and is
temporarily ignored because proving node coordinates in a wave front are
within bounds (`manhatanDistance` preconditions) requires discarting
out-of-bounds nodes. This is implemented as an optimization in a following commit.

Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
---
 src/Data/Algorithm/Diff.hs | 58 +++++++++++++++++++++++++++-----------
 1 file changed, 42 insertions(+), 16 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index f408393..437b2a3 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -169,6 +169,18 @@ furthestReaching x y
   | poi x >= poi y = x
   | otherwise      = y
 
+-- * Proving the algorithm termination in Liquid Haskell
+--
+-- The original algorithm is known to terminate because a wave front /eventually/ reaches the 'endPoint'.
+-- To prove this, both inputs lengths are threaded within phantom parameters throughout the implementation.
+-- In essence, both lengths are used to encode the edit grid and its end point.
+
+{-@ reflect _manhattanDistance @-}
+_manhattanDistance :: Int -> Int -> DL -> Int
+_manhattanDistance lena lenb dl  = lena - (poi dl) + lenb - (poj dl)
+
+{-@ type DiagPred M N = i : Nat -> j : Nat -> {b : Bool | ((i >= M || j >= N) => not b)} @-}
+
 -- | Build a /diagonal predicate/ — a closure that tests whether position
 -- @(i, j)@ in the edit graph has a diagonal edge (a /match point/ in Myers'
 -- terminology).
@@ -186,6 +198,7 @@ canDiag eq as bs lena lenb = \ i j ->
      arAs = listArray (0,lena - 1) as
      arBs = listArray (0,lenb - 1) bs
 
+{-@ ignore dstep @-}
 -- | Perform one breadth-first search expansion step, advancing every wave front
 -- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following
 -- any available snake.
@@ -210,22 +223,24 @@ canDiag eq as bs lena lenb = \ i j ->
 -- with one more node than the input.
 {-@
 dstep
-  :: (Nat -> Nat -> Bool)
+  :: lena : Nat
+  -> lenb : Nat
+  -> DiagPred lena lenb
   -> d : Nat
   -> {nodes : WaveFront d | len nodes > 0}
   -> {v : WaveFront (d + 1) | len v = len nodes + 1}
 @-}
 dstep
-  :: (Int -> Int -> Bool) -- ^ Diagonal predicate
+  :: Int                  -- ^ First input's length phantom parameter for termination check.
+  -> Int                  -- ^ Second input's length phantom parameter for termination check.
+  -> (Int -> Int -> Bool) -- ^ Diagonal predicate
   -> Int                  -- ^ The current D-length; used for the static check of wave front invariant.
   -> [DL]                 -- ^ A non-empty wave front of nodes at edit distance D
   -> [DL]                 -- ^ A non-empty wave front of nodes at edit distance D+1
--- NOTE: @_d@ is a phantom (apparently unused) parameter required by local LiquidHaskell specifications.
--- This parameter sits at the first equation as a workaround
--- to GHC removing it when desugaring multi-equation definitions.
--- See https://github.com/ucsd-progsys/liquidhaskell/issues/2704
-dstep _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes"
-dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls
+-- @lena@, @lenb@ and @_d@ are named in the first equation as a workaround
+-- to https://github.com/ucsd-progsys/liquidhaskell/issues/2704
+dstep lena lenb _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes"
+dstep lena lenb cd _ (dl:dls) = addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls
   where
     {-@ hStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x + 1} @-}
     hStep node = node {poi = poi node + 1, path = F : path node}
@@ -239,11 +254,10 @@ dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls
                      -> {v : [DLN (_d+1)] | _wfDiags (_kdiag prev - 1) v && len v = len rest + 1}
                      / [len rest] @-}
     stepAndMerge :: DL -> [DL] -> [DL]
-    stepAndMerge prev [] = [addsnake cd $ vStep prev]
+    stepAndMerge prev [] = [addsnake lena lenb cd $ vStep prev]
     stepAndMerge prev (next:rest) =
-      addsnake cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest
+      addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest
 
-{-@ lazy addsnake @-}
 -- | Follow a /snake/ from the current position of a 'DL' node.
 --
 -- A snake is a sequence of diagonal (cost-free) edges in the edit graph,
@@ -252,10 +266,22 @@ dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls
 -- @(poi dl, poj dl)@, this function advances both 'poi' and 'poj' as long
 -- as consecutive elements match, leaving 'path' unchanged (diagonal moves
 -- are not recorded as edit steps).
-{-@ addsnake :: (Nat -> Nat -> Bool) -> x : DL -> {v : DL | path v == path x && _kdiag v = _kdiag x} @-}
-addsnake :: (Int -> Int -> Bool) -> DL -> DL
-addsnake cd dl
-    | cd pi pj = addsnake cd $
+{-@
+addsnake :: lena : Nat
+         -> lenb : Nat
+         -> DiagPred lena lenb
+         -> dl : DL
+         -> {v : DL | path v == path dl
+                   && _kdiag v = _kdiag dl}
+         / [_manhattanDistance lena lenb dl]
+@-}
+addsnake :: Int                  -- ^ First input's length phantom parameter for termination check.
+         -> Int                  -- ^ Second input's length phantom parameter for termination check.
+         -> (Int -> Int -> Bool) -- ^ Diagonal predicate, a.k.a. 'canDiag'
+         -> DL
+         -> DL
+addsnake lena lenb cd dl
+    | cd pi pj = addsnake lena lenb cd $
                  dl {poi = pi + 1, poj = pj + 1, path = path dl}
     | otherwise   = dl
     where pi = poi dl; pj = poj dl
@@ -290,7 +316,7 @@ addsnake cd dl
 -- unchanged.
 ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI]
 ses eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) .
-            concat . iterate (uncurry (dstep cd) . withD) . (:[]) . addsnake cd $
+            concat . iterate (uncurry (dstep lena lenb cd) . withD) . (:[]) . addsnake lena lenb cd $
             DL {poi=0,poj=0,path=[]}
             where cd = canDiag eq as bs lena lenb
                   lena = length as; lenb = length bs

From 2b5ee5276435dfef4f853081b7e87109837d4c69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= <facundo.dominguez@tweag.io>
Date: Thu, 9 Jul 2026 12:29:53 +0000
Subject: [PATCH 2/8] Add a benchmark with a larger size difference between
 inputs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
---
 bench/bench.hs | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/bench/bench.hs b/bench/bench.hs
index a24391e..c67991b 100644
--- a/bench/bench.hs
+++ b/bench/bench.hs
@@ -24,7 +24,10 @@ doBenchMarks seed =
   let rbools = randoms (mkStdGen seed) :: [Bool]
       (s1000_1, rbools1) = splitAt 1000 rbools
       (s1000_2, rbools2) = splitAt 1000 rbools1
-  in s1000_1 `deepseq` s1000_2 `deepseq` defaultMain [
-    bgroup "diff bool lists" $ [bench "1000 bools" $ nf (getDiff s1000_1) s1000_2]
-    ]
-    
+      s500_2 = take 500 s1000_2
+  in (s1000_1, s1000_2, s500_2) `deepseq` defaultMain
+      [ bgroup "diff bool lists"
+          [ bench "1000 bools" $ nf (getDiff s1000_1) s1000_2
+          , bench "1000/500 bools" $ nf (getDiff s1000_1) s500_2
+          ]
+      ]

From b0db718ef61b95289b59d7873b58dcca7b5d1b3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Wed, 6 May 2026 13:59:46 -0600
Subject: [PATCH 3/8] Refactor/optimize `dstep` by narrowing wave front to edit
 grid
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`dstep` is optimized by adding checks that prevent the production
of out-of-bound nodes (those that would exit the edit grid).
This solves the problem `getDiffBy` empty list equations
where intended to address in
https://github.com/seereason/Diff/commit/33bf8bc7f95a825b51f97e53848d39ef957546d9
which are removed to avoid unnecessary complexity.

Adds a source note describing the design choice to leave aside a (small) possible
optimization in favor of reduced specification complexity.

Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
---
 src/Data/Algorithm/Diff.hs | 68 ++++++++++++++++++++++++++++++++++----
 1 file changed, 61 insertions(+), 7 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index 437b2a3..39e43ad 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -143,6 +143,47 @@ _wfDiags :: Int -> [DL] -> Bool
 _wfDiags _ [] = True
 _wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls
 
+--------------------------------------------------------------------------------
+-- [NOTE: diagonal-invariant]
+--
+-- The '_wfDiags' predicate states that succesive nodes in a wave front lie
+-- on diagonals whose indices differ by two. This is leveraged by LiquidHaskell
+-- to check that the 'furthestReaching' precondition stating that the two nodes
+-- it compares lie on the same diagonal is satisfied within `dstep`.
+-- However, even though a more flexible predicate could be used to prove it,
+-- a compromise was made in preserving this invariant to keep the specification
+-- complexity low at a negligible performance penalty cost.
+-- This note documents this compromise.
+--
+-- To prove 'ses' terminates, wave fronts are restricted to be within the
+-- edit grid. This is done by placing checks for boundary nodes within 'dstep'
+-- to avoid constructing nodes outside the grid. 'dstep' leverages such checks
+-- in optimizations that rely on the observation that boundary nodes signal
+-- other nodes cannot compete to the goal:
+--
+--  * If a bottom boundary is found, all subsequent nodes are not considered.
+--
+--  * If a right boundary is found, all previously constructed child nodes
+--    can be dropped.
+--
+-- Both preserve the diagonal invariant, as the wave front would just become
+-- narrower. However, due to the asymmetry of list traversal, the first one is
+-- readily implemented, while the second requires an additional operation whose
+-- cost trumps the gain of not keeping them for next iterations (according to the
+-- existing benchmarks). Because of this, and 'stepAndMege' looking a two
+-- succesive nodes at a time, only the current iteration child /could/ be
+-- effectively dropped.
+--
+-- However, dropping the current iteration child node results in wave fronts
+-- with holes: now for every right boundary node found, a diagonal is not
+-- occupied. This requires the diagonal invariant to be changed to "diagonal
+-- indices in succesive nodes of a wave front differ by 2, unless a node lies
+-- on the right boundary, in which case its diagonal must differ from the previous
+-- by a factor of 2". It was decided to not follow this path, because the gain
+-- of not keeping this node was found to be negligible compared with the resulting
+-- increase in specification complexity.
+--------------------------------------------------------------------------------
+
 -- A wave front is a list of 'DL' nodes, all at the same edit distance @D@,
 -- with k-diagonals @D@, @D−2@, …, @-D+2@, @-D@.
 {-@ type WaveFront D = {xs : [DLN D] | _wfDiags D xs} @-}
@@ -240,7 +281,11 @@ dstep
 -- @lena@, @lenb@ and @_d@ are named in the first equation as a workaround
 -- to https://github.com/ucsd-progsys/liquidhaskell/issues/2704
 dstep lena lenb _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes"
-dstep lena lenb cd _ (dl:dls) = addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls
+-- This definition branches according to whether a node is on a boundary
+-- to avoid constructing out-of-bound nodes and discarding other non-competing nodes.
+dstep lena lenb cd _ (dl:dls) =
+  if poi dl >= lena then stepAndMerge dl dls
+  else addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls
   where
     {-@ hStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x + 1} @-}
     hStep node = node {poi = poi node + 1, path = F : path node}
@@ -253,10 +298,21 @@ dstep lena lenb cd _ (dl:dls) = addsnake lena lenb cd (hStep dl) : stepAndMerge
                      -> {rest : [DLN _d] | _wfDiags (_kdiag prev - 2) rest}
                      -> {v : [DLN (_d+1)] | _wfDiags (_kdiag prev - 1) v && len v = len rest + 1}
                      / [len rest] @-}
-    stepAndMerge :: DL -> [DL] -> [DL]
-    stepAndMerge prev [] = [addsnake lena lenb cd $ vStep prev]
-    stepAndMerge prev (next:rest) =
-      addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest
+    stepAndMerge prev nodes =
+      -- When a node lies in the bottom boundary no subsequent node can reach
+      -- the goal faster.
+      if poj prev >= lenb then []
+      else case nodes of
+        [] -> [addsnake lena lenb cd $ vStep prev]
+        (next:rest) ->
+            -- The next node being on the right border implies 'hStep' would
+            -- produce a node outside the grid, but also that previous node's
+            -- children cannot compete to the endpoint.
+            -- However, we keep @prev@'s vertical child node to preserve
+            -- the '_wfDiags' invariant at a negligible performance penalty.
+            -- See [NOTE: diagonal-invariant]
+            if poi next >= lena then vStep prev : stepAndMerge next rest
+            else addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest
 
 -- | Follow a /snake/ from the current position of a 'DL' node.
 --
@@ -345,8 +401,6 @@ getGroupedDiff = getGroupedDiffBy (==)
 -- | A form of 'getDiff' with no 'Eq' constraint. Instead, an equality predicate
 -- is taken as the first argument.
 getDiffBy :: (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]
-getDiffBy _ a [] = map First a
-getDiffBy _ [] b = map Second b
 getDiffBy eq a b = markup a b . reverse $ ses eq a b
     where markup (x:xs) (y:ys) ds
             | eq x y = Both x y : markup xs ys ds

From 4839d720e36a47e4c1fc2006c598221565be7bf5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Wed, 6 May 2026 13:59:46 -0600
Subject: [PATCH 4/8] Prove `dstep` reduces distance to goal
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A `_wfDistanceToGoal` function is defined to be used as termination metric
for `ses`. In this commit, `dstep` is specified and checked to reduce it
from input to output.

The wave front diagonal condition is changed to look at the head
of the node list instead of the diagonal edit distance parameter,
and its nodes are specified to be within bounds.
Indeed, now that wave fronts are trimmed down to be within bounds,
we can no longer guarantee that the first node's diagonal matches
the edit distance.

The `stepAndMerge` specification is strengthen to preserve this new variant of
wave front diagonal invariant: With the current optimization of `dstep`,
wave fronts don't necessarily grow, but the 2-step specing is preserved.

Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
---
 src/Data/Algorithm/Diff.hs | 180 ++++++++++++++++++++++++++++++++-----
 1 file changed, 160 insertions(+), 20 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index 39e43ad..f2b28f8 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -124,9 +124,15 @@ data DL = DL
                      --   'S' steps are stored.
     } deriving (Show, Eq)
 
--- This refinement type alias represents a 'DL' value with a fixed /D-length/,
--- which we call a "D-path location node".
-{-@ type DLN D = { x : DL | len (path x) = D } @-}
+-- Field refinements are implemented with measures, which means they are
+-- available only when a 'DL' value is pattern matched;
+-- This invariant on DLs makes the coordinates non-negativity available
+-- for any value of type 'DL' regardless of whether it has been pattern matched.
+{-@ using (DL) as { dl : DL | poi dl >= 0 && poj dl >= 0 } @-}
+
+-- A "D-path location node" is a 'DL' value within the edit grid bounds
+-- having a fixed /D-length/.
+{-@ type DLN M N D = { x : DL | len (path x) = D && _withinBounds M N x} @-}
 
 {-@ inline _kdiag @-}
 -- | Computes the k-diagonal of a node.
@@ -186,8 +192,14 @@ _wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls
 
 -- A wave front is a list of 'DL' nodes, all at the same edit distance @D@,
 -- with k-diagonals @D@, @D−2@, …, @-D+2@, @-D@.
-{-@ type WaveFront D = {xs : [DLN D] | _wfDiags D xs} @-}
+-- Wave fronts establish a connection with the Myers algorithm:
+-- @D@ corresponds to the algorithm's current iteration step and the resulting
+-- 'ses' length. In Myers the diagonal arrangement is used to optimize space;
+-- within 'dstep' it allows us to ensure 'furthestReaching' always compares
+-- nodes on the same diagonals.
+{-@ type WaveFront M N D = {xs : [DLN M N D] | _wfDiags (_kdiag (head xs)) xs} @-}
 
+{-@ reflect furthestReaching @-}
 -- | Select the furthest-reaching candidate of two 'DL' nodes competing for the
 -- same k-diagonal, as required by the Myers algorithm.
 --
@@ -203,8 +215,8 @@ _wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls
 --
 -- > length (path x) == length (path y)
 {-@ furthestReaching ::  x : DL
-                     -> {y : DL | _kdiag x = _kdiag y}
-                     -> {v : DL | v = x || v = y} @-}
+                     -> {y : DL | _kdiag x = _kdiag y && len (path x) = len (path y)}
+                     -> {v : DL | (v = x || v = y)} @-}
 furthestReaching :: DL -> DL -> DL
 furthestReaching x y
   | poi x >= poi y = x
@@ -220,6 +232,106 @@ furthestReaching x y
 _manhattanDistance :: Int -> Int -> DL -> Int
 _manhattanDistance lena lenb dl  = lena - (poi dl) + lenb - (poj dl)
 
+{-@ reflect _wfDistanceToGoal @-}
+-- | The smallest manhattan distance from a wave front node to the goal @(lena, lenb)@.
+-- The empty wave front yields @lena + lenb + 2@, a sentinel strictly greater
+-- than any in-bounds node's distance, acting as the identity for the minimum.
+_wfDistanceToGoal :: Int -> Int -> [DL] -> Int
+_wfDistanceToGoal lena lenb [] = lena + lenb + 2
+_wfDistanceToGoal lena lenb (dl:dls) =
+  -- We avoid using 'min' here so that LH can unfold this definition.
+  if _manhattanDistance lena lenb dl < _wfDistanceToGoal lena lenb dls
+  then _manhattanDistance lena lenb dl
+  else _wfDistanceToGoal lena lenb dls
+
+-- | A lemma that expresses a lower bound of the wavefront distance in terms
+-- of the diagonal of the first node: @lena - lenb - k@
+--
+-- We assume all the nodes to be within the grid.
+--
+-- @lena - lenb@ is the diagonal of the goal. Informally, the
+-- shortest way from a node must necessarily visit all the intermediate
+-- diagonals. The minimum amount of diagonals to visit is given by the
+-- difference between the diagonal indices of the goal and the first element.
+--
+-- We can prove it manually like so:
+--
+-- For every node @dl = DL i j p@ we can prove
+-- @H(dl) = _manhattanDistance lena lenb dl >= lena - lenb - (i - j)@
+--
+-- @
+--   _manhattanDistance lena lenb dl
+-- =
+--   lena - (poi dl) + lenb - (poj dl)
+-- =
+--   lena - i + lenb - j
+-- =
+--   lena - lenb - (i - j) + 2 * (lenb - j)
+-- >=
+--   lena - lenb - (i - j)
+-- @
+--
+-- Since @H(dl)@ holds for every node in the wave front, it follows
+-- that the wave front distance is at least as large as the smallest of
+-- these bounds, which is @lena - lenb - k@ for the largest @k = i0 - j0@,
+-- which is the diagonal of the first node.
+--
+-- QED
+-- @
+{-@ _wfDistanceLowerBoundK
+      :: lena : Nat -> lenb : Nat -> {k : Int | lenb + k + 2 >= 0}
+      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags k v}
+      -> {_wfDistanceToGoal lena lenb xs >= lena - lenb - k}
+      / [len xs] @-}
+_wfDistanceLowerBoundK :: Int -> Int -> Int -> [DL] -> ()
+_wfDistanceLowerBoundK _    _    _ []      = ()
+_wfDistanceLowerBoundK lena lenb k (_:dls) = _wfDistanceLowerBoundK lena lenb (k - 2) dls
+
+-- | If a wave front's node (@prev@) is on the bottom boundary, then the following
+-- nodes lie farther from the goal. Intuitively, the reason is that the following
+-- nodes children would need more steps to cross @prev@'s diagonal to reach the goal.
+-- This lemma allows LH to reason about the case where nodes are discarded
+-- after a bottom-boundary node within 'dstep'.
+{-@
+_wfDistanceLowerBound
+      :: lena : Nat -> lenb : Nat -> {prev : DL | _withinBounds lena lenb prev}
+      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags (_kdiag prev - 2) v}
+      -> { poj prev >= lenb =>  _wfDistanceToGoal lena lenb xs > _manhattanDistance lena lenb prev}
+ @-}
+_wfDistanceLowerBound :: Int -> Int -> DL -> [DL] -> ()
+_wfDistanceLowerBound lena lenb prev [] = ()
+_wfDistanceLowerBound lena lenb prev xs@(_:_) = ()
+  where
+    _lemma = _wfDistanceLowerBoundK lena lenb (_kdiag prev - 2) xs
+
+
+-- | The termination metric is non-negative: every in-bounds node has a
+-- non-negative manhattan distance to the goal, and the empty wave front
+-- yields the positive sentinel. Needed because the @Nat@ result refinement
+-- of the reflected '_wfDistanceToGoal' is not instantiated at logic-level
+-- applications, while termination metrics must be provably non-negative.
+{-@ _minDistanceNonNegative
+      :: lena : Nat -> lenb : Nat
+      -> xs : [{dl : DL | _withinBounds lena lenb dl}]
+      -> {_wfDistanceToGoal lena lenb xs >= 0}
+      / [len xs] @-}
+_minDistanceNonNegative :: Int -> Int -> [DL] -> ()
+_minDistanceNonNegative _    _    []       = ()
+_minDistanceNonNegative lena lenb (_:dls) = _minDistanceNonNegative lena lenb dls
+
+{-@ inline _reducesDistanceToGoal @-}
+_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool
+_reducesDistanceToGoal lena lenb wf1 wf2 = _wfDistanceToGoal lena lenb wf2 < _wfDistanceToGoal lena lenb wf1
+
+{-@ inline _withinBounds @-}
+{-@ _withinBounds :: lena : Nat -> lenb : Nat -> dl : DL -> {v:Bool | v <=> (poi dl <= lena && poj dl <= lenb) } @-}
+_withinBounds :: Int -> Int -> DL -> Bool
+_withinBounds lena lenb dl = poi dl <= lena && poj dl <= lenb
+
+{-@ inline endPoint @-}
+endPoint :: Int -> Int -> DL -> Bool
+endPoint lena lenb dl = poi dl == lena && poj dl == lenb
+
 {-@ type DiagPred M N = i : Nat -> j : Nat -> {b : Bool | ((i >= M || j >= N) => not b)} @-}
 
 -- | Build a /diagonal predicate/ — a closure that tests whether position
@@ -239,7 +351,6 @@ canDiag eq as bs lena lenb = \ i j ->
      arAs = listArray (0,lena - 1) as
      arBs = listArray (0,lenb - 1) bs
 
-{-@ ignore dstep @-}
 -- | Perform one breadth-first search expansion step, advancing every wave front
 -- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following
 -- any available snake.
@@ -268,8 +379,10 @@ dstep
   -> lenb : Nat
   -> DiagPred lena lenb
   -> d : Nat
-  -> {nodes : WaveFront d | len nodes > 0}
-  -> {v : WaveFront (d + 1) | len v = len nodes + 1}
+  -> {nodes : WaveFront lena lenb d | len nodes > 0
+                                   && not (endPoint lena lenb (head nodes))
+                                   && _wfDistanceToGoal lena lenb nodes > 0}
+  -> {v : WaveFront lena lenb (d + 1) | len v > 0 && _reducesDistanceToGoal lena lenb nodes v}
 @-}
 dstep
   :: Int                  -- ^ First input's length phantom parameter for termination check.
@@ -285,22 +398,41 @@ dstep lena lenb _ _d [] = error "dstep: Cannot perform expansion on an empty lis
 -- to avoid constructing out-of-bound nodes and discarding other non-competing nodes.
 dstep lena lenb cd _ (dl:dls) =
   if poi dl >= lena then stepAndMerge dl dls
-  else addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls
+  else
+    (addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls)
+      -- If @dl@ lies on the bottom boundary, @stepAndMerge dl dls@ discards
+      -- all of @dls@; the lemma shows the discarded nodes are farther from
+      -- the goal than @dl@'s horizontal child.
+      `const` _wfDistanceLowerBound lena lenb dl dls
   where
-    {-@ hStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x + 1} @-}
+    {-@ hStep
+          :: x : DLN lena lenb _d
+          -> {v : DL | len (path v) = _d + 1 && poi v = poi x + 1 && poj v = poj x} @-}
     hStep node = node {poi = poi node + 1, path = F : path node}
-    {-@ vStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x - 1} @-}
+    {-@ vStep
+          :: x : DLN lena lenb _d
+          -> {v : DL | len (path v) = _d + 1 && poi v = poi x && poj v = poj x + 1} @-}
     vStep node = node {poj = poj node + 1, path = S : path node}
     -- Merge vertical step of previous node with horizontal step of next node,
     -- selecting the furthest-reaching candidate for each shared k-diagonal,
     -- and extend it along matching elements.
-     {-@ stepAndMerge :: prev : DLN _d
-                     -> {rest : [DLN _d] | _wfDiags (_kdiag prev - 2) rest}
-                     -> {v : [DLN (_d+1)] | _wfDiags (_kdiag prev - 1) v && len v = len rest + 1}
-                     / [len rest] @-}
+    {-@ stepAndMerge
+          :: prev : DLN lena lenb _d
+          -> nodes : {xs : [DLN lena lenb _d] | _wfDiags (_kdiag prev - 2) xs
+                                             && _wfDistanceToGoal lena lenb xs > 0}
+          -> {v : [DLN lena lenb (_d + 1)] | _wfDiags (_kdiag prev - 1) v
+                                          && (poj prev < lenb <=> len v > 0)
+                                          && (len v > 0 =>
+                                               _kdiag (head v) == _kdiag prev - 1)
+                                          && (poj prev < lenb =>
+                                               _wfDistanceToGoal lena lenb v
+                                                 < _manhattanDistance lena lenb prev
+                                            && _wfDistanceToGoal lena lenb v
+                                                 < _wfDistanceToGoal lena lenb nodes)}
+          / [len nodes] @-}
     stepAndMerge prev nodes =
       -- When a node lies in the bottom boundary no subsequent node can reach
-      -- the goal faster.
+      -- the goal faster. See lemma '_wfDistanceLowerBound'.
       if poj prev >= lenb then []
       else case nodes of
         [] -> [addsnake lena lenb cd $ vStep prev]
@@ -312,7 +444,12 @@ dstep lena lenb cd _ (dl:dls) =
             -- the '_wfDiags' invariant at a negligible performance penalty.
             -- See [NOTE: diagonal-invariant]
             if poi next >= lena then vStep prev : stepAndMerge next rest
-            else addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest
+            else
+              (addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest)
+                -- If @next@ lies on the bottom boundary, the recursive call
+                -- discards all of @rest@; the lemma shows the discarded nodes
+                -- are farther from the goal than the merged child.
+                `const` _wfDistanceLowerBound lena lenb next rest
 
 -- | Follow a /snake/ from the current position of a 'DL' node.
 --
@@ -326,9 +463,12 @@ dstep lena lenb cd _ (dl:dls) =
 addsnake :: lena : Nat
          -> lenb : Nat
          -> DiagPred lena lenb
-         -> dl : DL
+         -> {dl : DL | _withinBounds lena lenb dl}
          -> {v : DL | path v == path dl
-                   && _kdiag v = _kdiag dl}
+                   && _kdiag v = _kdiag dl
+                   && _withinBounds lena lenb v
+                   && poi v >= poi dl
+                   && poj v >= poj dl}
          / [_manhattanDistance lena lenb dl]
 @-}
 addsnake :: Int                  -- ^ First input's length phantom parameter for termination check.

From 5a65d00d581cb2768e29b5d6a16cf51261baae2a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Wed, 6 May 2026 13:59:46 -0600
Subject: [PATCH 5/8] Refactor `ses` to use wave-front wise search for the
 endpoint.

The implementation of `ses` changes from a `dropWhile` driven search for
the algorithm's end point in a lazy stream composed of all wave front nodes,
to the explicit recursion of a wave-front wise search for such end point.

This change was designed to allow a termination proof using Liquid Haskell:
by inspecting each wave front separately, instead of all concatenated together in an
infinite stream, we can define a wave front metric as its minimum distance to
the endpoint and show it is reduced by the recursive calls (to `dstep`).

Performance-wise, we get a small optimization of the benchmark of ~12%
---
 src/Data/Algorithm/Diff.hs | 45 +++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index f2b28f8..d3534f8 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -78,6 +78,7 @@ import Data.Array (listArray, (!))
 import Data.Algorithm.Diff.Type
 import Data.Algorithm.Diff.Refinement (fst3, snd3, thd3, headIsFirst,
                                         headIsSecond, headIsBoth, noStuttering)
+import Data.Foldable (find)
 
 -- | /Diff Instruction/ — an internal enum recording the direction of a single
 -- non-diagonal edge traversed in the Myers edit graph. Every non-diagonal
@@ -486,37 +487,37 @@ addsnake lena lenb cd dl
 -- | Compute shortest edit script (SES), as the minimum sequence of 'DI' edit
 -- steps that transforms @as@ into @bs@, returned in reverse order.
 --
--- @ses eq as bs@ runs the Myers O(ND) diff algorithm following
--- a five-step pipeline:
+-- @ses eq as bs@ runs the Myers O(ND) diff algorithm:
 --
--- 1. __Seed__: create an initial 0-path wave front @[addsnake cd (DL 0 0 [])]@
+-- 1. __Seed__: create an initial 0-path wave front @[addsnake lena lenb cd (DL 0 0 [])]@
 --    having a single node on the tip of the longest origin-sourced snake.
--- 2. __Iterate__: apply 'dstep' repeatedly via 'iterate', producing an
---    infinite list of wave fronts (one per edit distance D = 0, 1, 2, …).
--- 3. __Flatten__: 'concat' all wave fronts into a single stream of 'DL' nodes.
--- 4. __Find__: 'dropWhile' skips nodes until one reaches @(lena, lenb)@ — the
---    bottom-right corner of the edit graph — which is the terminal node of a
---    shortest edit script.
--- 5. __Extract__: 'head' returns that node; its 'path' field carries the edit
+-- 2. __Search__: for each wave front at edit distance \( D = 0, 1, \ldots \),
+--    check whether any node has reached the goal @(lena, lenb)@. If not,
+--    apply 'dstep' to advance to edit distance \( D+1 \).
+-- 3. __Extract__: the first goal node's 'path' field carries the edit
 --    trace in reverse order.
 --
--- This implementation is purely functional: rather than updating a shared
--- diagonal frontier array in place, as in the original paper, it builds a new
--- list of 'DL' nodes for each value of \( D \) and concatenates them into
--- a single lazy stream. This is simpler but carries a larger per-node overhead:
--- each 'DL' holds its own edit trace as a @['DI']@ list that structurally
--- shares its tail with the parent node's trace (consing one step reuses the
--- existing spine), rather than the paper's single-integer-per-diagonal
--- representation. The asymptotic time
+-- This implementation deviates from the paper in the folowing way:
+-- rather than updating a shared diagonal frontier array in place,
+-- as in the original paper, it builds a new list of 'DL' nodes
+-- for each value of \( D \). This is simpler but carries a
+-- larger per-node overhead: each 'DL' holds its own edit trace as a @['DI']@
+-- list that structurally shares its tail with the parent node's trace (consing
+-- one step reuses the existing spine), rather than the paper's
+-- single-integer-per-diagonal representation. The asymptotic time
 -- and space complexity — \( O(ND) \) and \( O(D^2) \) respectively — is
 -- unchanged.
 ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI]
-ses eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) .
-            concat . iterate (uncurry (dstep lena lenb cd) . withD) . (:[]) . addsnake lena lenb cd $
-            DL {poi=0,poj=0,path=[]}
+ses eq as bs = search 0 [addsnake lena lenb cd (DL 0 0 [])]
             where cd = canDiag eq as bs lena lenb
                   lena = length as; lenb = length bs
-                  withD xs = (length . path . head $ xs, xs)
+                  search :: Int -> [DL] -> [DI]
+                  search _ [] = error "ses: The search must have a seed node"
+                  search d wf = case findEndpoint lena lenb wf of
+                      Just p  -> path p
+                      Nothing -> search (d + 1) (dstep lena lenb cd d wf)
+                  findEndpoint :: Int -> Int -> [DL] -> Maybe DL
+                  findEndpoint i j = find (endPoint i j)
 
 -- | Takes two lists and returns a list of differences between them. This is
 -- 'getDiffBy' with '==' used as predicate.

From a75f90c219b3e575b6dc4e808da385914e0929fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Wed, 6 May 2026 13:59:46 -0600
Subject: [PATCH 6/8] `ses` termination proof
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
---
 src/Data/Algorithm/Diff.hs | 43 ++++++++++++++++++++++++++++++--------
 1 file changed, 34 insertions(+), 9 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index d3534f8..7d0499e 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -344,13 +344,26 @@ endPoint lena lenb dl = poi dl == lena && poj dl == lenb
 --
 -- The first two 'Int' parameters stand for the lengths of the input lists,
 -- which are captured from the outer scope to compute them only once.
-canDiag :: (a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool
-canDiag eq as bs lena lenb = \ i j ->
-   if i < lena && j < lenb then (arAs ! i) `eq` (arBs ! j) else False
-   where
-     -- Lists are converted into arrays to have O(1) lookups.
-     arAs = listArray (0,lena - 1) as
-     arBs = listArray (0,lenb - 1) bs
+{-@
+canDiag :: (a -> b -> Bool)
+        -> [a]
+        -> [b]
+        -> lena : Int
+        -> lenb : Int
+        -> DiagPred lena lenb
+@-}
+canDiag :: (a -> b -> Bool) -- ^ Custom equality predicate
+        -> [a] -- ^ First input
+        -> [b] -- ^ Second input
+        -> Int -- ^ First input's length
+        -> Int -- ^ Second input's lenth
+        -> (Int -> Int -> Bool) -- ^ Diagonal predicate on the edit grid
+canDiag eq as bs lena lenb = \i j ->
+  (i < lena && j < lenb) && ((arAs ! i) `eq` (arBs ! j))
+  where
+    -- Lists are converted into arrays to have O(1) lookups.
+    arAs = listArray (0,lena - 1) as
+    arBs = listArray (0,lenb - 1) bs
 
 -- | Perform one breadth-first search expansion step, advancing every wave front
 -- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following
@@ -483,7 +496,6 @@ addsnake lena lenb cd dl
     | otherwise   = dl
     where pi = poi dl; pj = poj dl
 
-{-@ ignore ses @-}
 -- | Compute shortest edit script (SES), as the minimum sequence of 'DI' edit
 -- steps that transforms @as@ into @bs@, returned in reverse order.
 --
@@ -511,11 +523,24 @@ ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI]
 ses eq as bs = search 0 [addsnake lena lenb cd (DL 0 0 [])]
             where cd = canDiag eq as bs lena lenb
                   lena = length as; lenb = length bs
+                  {-@ search :: d : Nat
+                             -> {dls : WaveFront lena lenb d | len dls > 0}
+                             -> {v : [DI] | len v >= d}
+                             / [_wfDistanceToGoal lena lenb dls] @-}
                   search :: Int -> [DL] -> [DI]
                   search _ [] = error "ses: The search must have a seed node"
                   search d wf = case findEndpoint lena lenb wf of
                       Just p  -> path p
-                      Nothing -> search (d + 1) (dstep lena lenb cd d wf)
+                      Nothing -> let wf' = dstep lena lenb cd d wf
+                                 in search (d + 1)
+                                           (wf' `const` _minDistanceNonNegative lena lenb wf')
+                  -- The abstract refinement @q@ lets 'find' carry the wave
+                  -- front element refinement (notably @len (path dl) == d@)
+                  -- over to the returned endpoint.
+                  {-@ assume findEndpoint :: forall <q :: DL -> Bool>.
+                                             i : Nat -> j : Nat -> xs : [DL<q>]
+                                          -> { m : Maybe {dl : DL<q> | endPoint i j dl}
+                                             | m == Nothing => _wfDistanceToGoal i j xs > 0} @-}
                   findEndpoint :: Int -> Int -> [DL] -> Maybe DL
                   findEndpoint i j = find (endPoint i j)
 

From cfa80a032d9c65f8fbe4de766d4520d18f146916 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Mon, 3 Aug 2026 09:13:52 -0600
Subject: [PATCH 7/8] Move and reflect step functions in the top level to
 reduce spec

---
 src/Data/Algorithm/Diff.hs | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index 7d0499e..952983a 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -365,6 +365,14 @@ canDiag eq as bs lena lenb = \i j ->
     arAs = listArray (0,lena - 1) as
     arBs = listArray (0,lenb - 1) bs
 
+{-@ reflect hStep @-}
+hStep :: DL -> DL
+hStep node = node {poi = poi node + 1, path = F : path node}
+
+{-@ reflect vStep @-}
+vStep :: DL -> DL
+vStep node = node {poj = poj node + 1, path = S : path node}
+
 -- | Perform one breadth-first search expansion step, advancing every wave front
 -- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following
 -- any available snake.
@@ -419,14 +427,6 @@ dstep lena lenb cd _ (dl:dls) =
       -- the goal than @dl@'s horizontal child.
       `const` _wfDistanceLowerBound lena lenb dl dls
   where
-    {-@ hStep
-          :: x : DLN lena lenb _d
-          -> {v : DL | len (path v) = _d + 1 && poi v = poi x + 1 && poj v = poj x} @-}
-    hStep node = node {poi = poi node + 1, path = F : path node}
-    {-@ vStep
-          :: x : DLN lena lenb _d
-          -> {v : DL | len (path v) = _d + 1 && poi v = poi x && poj v = poj x + 1} @-}
-    vStep node = node {poj = poj node + 1, path = S : path node}
     -- Merge vertical step of previous node with horizontal step of next node,
     -- selecting the furthest-reaching candidate for each shared k-diagonal,
     -- and extend it along matching elements.

From d1f3ec5d77af9604444d3fa3250e9236eb2b7750 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= <xavier.gongora@tweag.io>
Date: Mon, 10 Aug 2026 13:02:57 -0600
Subject: [PATCH 8/8] Amend docs and rearrange module to isolate LH specific
 machinery

---
 src/Data/Algorithm/Diff.hs | 397 ++++++++++++++++++++-----------------
 1 file changed, 210 insertions(+), 187 deletions(-)

diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs
index 952983a..c499021 100644
--- a/src/Data/Algorithm/Diff.hs
+++ b/src/Data/Algorithm/Diff.hs
@@ -125,81 +125,6 @@ data DL = DL
                      --   'S' steps are stored.
     } deriving (Show, Eq)
 
--- Field refinements are implemented with measures, which means they are
--- available only when a 'DL' value is pattern matched;
--- This invariant on DLs makes the coordinates non-negativity available
--- for any value of type 'DL' regardless of whether it has been pattern matched.
-{-@ using (DL) as { dl : DL | poi dl >= 0 && poj dl >= 0 } @-}
-
--- A "D-path location node" is a 'DL' value within the edit grid bounds
--- having a fixed /D-length/.
-{-@ type DLN M N D = { x : DL | len (path x) = D && _withinBounds M N x} @-}
-
-{-@ inline _kdiag @-}
--- | Computes the k-diagonal of a node.
--- Used in LiquidHaskell logic as an expression.
-_kdiag :: DL -> Int
-_kdiag dl = poi dl - poj dl
-
-{-@ reflect _wfDiags @-}
-{-@ _wfDiags :: Int -> xs : [DL] -> Bool / [len xs] @-}
--- | Checks if succesive nodes of a wave front lie within k-diagonals
--- differing by 2 as described in the Myers algorithm.
--- Used in LiquidHaskell logic as a predicate.
-_wfDiags :: Int -> [DL] -> Bool
-_wfDiags _ [] = True
-_wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls
-
---------------------------------------------------------------------------------
--- [NOTE: diagonal-invariant]
---
--- The '_wfDiags' predicate states that succesive nodes in a wave front lie
--- on diagonals whose indices differ by two. This is leveraged by LiquidHaskell
--- to check that the 'furthestReaching' precondition stating that the two nodes
--- it compares lie on the same diagonal is satisfied within `dstep`.
--- However, even though a more flexible predicate could be used to prove it,
--- a compromise was made in preserving this invariant to keep the specification
--- complexity low at a negligible performance penalty cost.
--- This note documents this compromise.
---
--- To prove 'ses' terminates, wave fronts are restricted to be within the
--- edit grid. This is done by placing checks for boundary nodes within 'dstep'
--- to avoid constructing nodes outside the grid. 'dstep' leverages such checks
--- in optimizations that rely on the observation that boundary nodes signal
--- other nodes cannot compete to the goal:
---
---  * If a bottom boundary is found, all subsequent nodes are not considered.
---
---  * If a right boundary is found, all previously constructed child nodes
---    can be dropped.
---
--- Both preserve the diagonal invariant, as the wave front would just become
--- narrower. However, due to the asymmetry of list traversal, the first one is
--- readily implemented, while the second requires an additional operation whose
--- cost trumps the gain of not keeping them for next iterations (according to the
--- existing benchmarks). Because of this, and 'stepAndMege' looking a two
--- succesive nodes at a time, only the current iteration child /could/ be
--- effectively dropped.
---
--- However, dropping the current iteration child node results in wave fronts
--- with holes: now for every right boundary node found, a diagonal is not
--- occupied. This requires the diagonal invariant to be changed to "diagonal
--- indices in succesive nodes of a wave front differ by 2, unless a node lies
--- on the right boundary, in which case its diagonal must differ from the previous
--- by a factor of 2". It was decided to not follow this path, because the gain
--- of not keeping this node was found to be negligible compared with the resulting
--- increase in specification complexity.
---------------------------------------------------------------------------------
-
--- A wave front is a list of 'DL' nodes, all at the same edit distance @D@,
--- with k-diagonals @D@, @D−2@, …, @-D+2@, @-D@.
--- Wave fronts establish a connection with the Myers algorithm:
--- @D@ corresponds to the algorithm's current iteration step and the resulting
--- 'ses' length. In Myers the diagonal arrangement is used to optimize space;
--- within 'dstep' it allows us to ensure 'furthestReaching' always compares
--- nodes on the same diagonals.
-{-@ type WaveFront M N D = {xs : [DLN M N D] | _wfDiags (_kdiag (head xs)) xs} @-}
-
 {-@ reflect furthestReaching @-}
 -- | Select the furthest-reaching candidate of two 'DL' nodes competing for the
 -- same k-diagonal, as required by the Myers algorithm.
@@ -223,118 +148,6 @@ furthestReaching x y
   | poi x >= poi y = x
   | otherwise      = y
 
--- * Proving the algorithm termination in Liquid Haskell
---
--- The original algorithm is known to terminate because a wave front /eventually/ reaches the 'endPoint'.
--- To prove this, both inputs lengths are threaded within phantom parameters throughout the implementation.
--- In essence, both lengths are used to encode the edit grid and its end point.
-
-{-@ reflect _manhattanDistance @-}
-_manhattanDistance :: Int -> Int -> DL -> Int
-_manhattanDistance lena lenb dl  = lena - (poi dl) + lenb - (poj dl)
-
-{-@ reflect _wfDistanceToGoal @-}
--- | The smallest manhattan distance from a wave front node to the goal @(lena, lenb)@.
--- The empty wave front yields @lena + lenb + 2@, a sentinel strictly greater
--- than any in-bounds node's distance, acting as the identity for the minimum.
-_wfDistanceToGoal :: Int -> Int -> [DL] -> Int
-_wfDistanceToGoal lena lenb [] = lena + lenb + 2
-_wfDistanceToGoal lena lenb (dl:dls) =
-  -- We avoid using 'min' here so that LH can unfold this definition.
-  if _manhattanDistance lena lenb dl < _wfDistanceToGoal lena lenb dls
-  then _manhattanDistance lena lenb dl
-  else _wfDistanceToGoal lena lenb dls
-
--- | A lemma that expresses a lower bound of the wavefront distance in terms
--- of the diagonal of the first node: @lena - lenb - k@
---
--- We assume all the nodes to be within the grid.
---
--- @lena - lenb@ is the diagonal of the goal. Informally, the
--- shortest way from a node must necessarily visit all the intermediate
--- diagonals. The minimum amount of diagonals to visit is given by the
--- difference between the diagonal indices of the goal and the first element.
---
--- We can prove it manually like so:
---
--- For every node @dl = DL i j p@ we can prove
--- @H(dl) = _manhattanDistance lena lenb dl >= lena - lenb - (i - j)@
---
--- @
---   _manhattanDistance lena lenb dl
--- =
---   lena - (poi dl) + lenb - (poj dl)
--- =
---   lena - i + lenb - j
--- =
---   lena - lenb - (i - j) + 2 * (lenb - j)
--- >=
---   lena - lenb - (i - j)
--- @
---
--- Since @H(dl)@ holds for every node in the wave front, it follows
--- that the wave front distance is at least as large as the smallest of
--- these bounds, which is @lena - lenb - k@ for the largest @k = i0 - j0@,
--- which is the diagonal of the first node.
---
--- QED
--- @
-{-@ _wfDistanceLowerBoundK
-      :: lena : Nat -> lenb : Nat -> {k : Int | lenb + k + 2 >= 0}
-      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags k v}
-      -> {_wfDistanceToGoal lena lenb xs >= lena - lenb - k}
-      / [len xs] @-}
-_wfDistanceLowerBoundK :: Int -> Int -> Int -> [DL] -> ()
-_wfDistanceLowerBoundK _    _    _ []      = ()
-_wfDistanceLowerBoundK lena lenb k (_:dls) = _wfDistanceLowerBoundK lena lenb (k - 2) dls
-
--- | If a wave front's node (@prev@) is on the bottom boundary, then the following
--- nodes lie farther from the goal. Intuitively, the reason is that the following
--- nodes children would need more steps to cross @prev@'s diagonal to reach the goal.
--- This lemma allows LH to reason about the case where nodes are discarded
--- after a bottom-boundary node within 'dstep'.
-{-@
-_wfDistanceLowerBound
-      :: lena : Nat -> lenb : Nat -> {prev : DL | _withinBounds lena lenb prev}
-      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags (_kdiag prev - 2) v}
-      -> { poj prev >= lenb =>  _wfDistanceToGoal lena lenb xs > _manhattanDistance lena lenb prev}
- @-}
-_wfDistanceLowerBound :: Int -> Int -> DL -> [DL] -> ()
-_wfDistanceLowerBound lena lenb prev [] = ()
-_wfDistanceLowerBound lena lenb prev xs@(_:_) = ()
-  where
-    _lemma = _wfDistanceLowerBoundK lena lenb (_kdiag prev - 2) xs
-
-
--- | The termination metric is non-negative: every in-bounds node has a
--- non-negative manhattan distance to the goal, and the empty wave front
--- yields the positive sentinel. Needed because the @Nat@ result refinement
--- of the reflected '_wfDistanceToGoal' is not instantiated at logic-level
--- applications, while termination metrics must be provably non-negative.
-{-@ _minDistanceNonNegative
-      :: lena : Nat -> lenb : Nat
-      -> xs : [{dl : DL | _withinBounds lena lenb dl}]
-      -> {_wfDistanceToGoal lena lenb xs >= 0}
-      / [len xs] @-}
-_minDistanceNonNegative :: Int -> Int -> [DL] -> ()
-_minDistanceNonNegative _    _    []       = ()
-_minDistanceNonNegative lena lenb (_:dls) = _minDistanceNonNegative lena lenb dls
-
-{-@ inline _reducesDistanceToGoal @-}
-_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool
-_reducesDistanceToGoal lena lenb wf1 wf2 = _wfDistanceToGoal lena lenb wf2 < _wfDistanceToGoal lena lenb wf1
-
-{-@ inline _withinBounds @-}
-{-@ _withinBounds :: lena : Nat -> lenb : Nat -> dl : DL -> {v:Bool | v <=> (poi dl <= lena && poj dl <= lenb) } @-}
-_withinBounds :: Int -> Int -> DL -> Bool
-_withinBounds lena lenb dl = poi dl <= lena && poj dl <= lenb
-
-{-@ inline endPoint @-}
-endPoint :: Int -> Int -> DL -> Bool
-endPoint lena lenb dl = poi dl == lena && poj dl == lenb
-
-{-@ type DiagPred M N = i : Nat -> j : Nat -> {b : Bool | ((i >= M || j >= N) => not b)} @-}
-
 -- | Build a /diagonal predicate/ — a closure that tests whether position
 -- @(i, j)@ in the edit graph has a diagonal edge (a /match point/ in Myers'
 -- terminology).
@@ -634,3 +447,213 @@ getGroupedDiffBy eq a b = groupDiff $ getDiffBy eq a b
     leadingBoths (Both w z : diffs) = let (as, bs, rest) = leadingBoths diffs
                                        in (w:as, z:bs, rest)
     leadingBoths diffs = ([], [], diffs)
+
+--------------------------------------------------------------------------------
+-- * LiquidHaskell Wave Front Specification
+--
+-- Wave fronts establish a connection between the orignal the Myers algorithm
+-- and this implementation:
+-- Their nodes carry the edit distance, which also corresponds to the
+-- algorithm's current iteration step and the resulting 'ses' length.
+-- In Myers the diagonal arrangement invariant of the iteration is used to
+-- optimize space; within 'dstep' it allows us to ensure 'furthestReaching'
+-- always compares nodes on the same diagonals.
+--------------------------------------------------------------------------------
+
+-- Field refinements are implemented with measures, which means they are
+-- available only when a 'DL' value is pattern matched;
+-- This invariant on DLs makes the coordinates non-negativity available
+-- for any value of type 'DL' regardless of whether it has been pattern matched.
+{-@ using (DL) as { dl : DL | poi dl >= 0 && poj dl >= 0 } @-}
+
+-- A "D-path location node" is a 'DL' value within the edit grid bounds
+-- having a fixed /D-length/.
+{-@ type DLN M N D = { x : DL | len (path x) = D && _withinBounds M N x} @-}
+
+{-@ inline _kdiag @-}
+-- | Computes the k-diagonal of a node.
+-- Used in LiquidHaskell logic as an expression.
+_kdiag :: DL -> Int
+_kdiag dl = poi dl - poj dl
+
+{-@ reflect _wfDiags @-}
+{-@ _wfDiags :: Int -> xs : [DL] -> Bool / [len xs] @-}
+-- | Checks if succesive nodes of a wave front lie within k-diagonals
+-- differing by 2 as described in the Myers algorithm.
+-- Used in LiquidHaskell logic as a predicate.
+-- See [NOTE: diagonal-invariant]
+_wfDiags :: Int -> [DL] -> Bool
+_wfDiags _ [] = True
+_wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls
+
+--------------------------------------------------------------------------------
+-- [NOTE: diagonal-invariant]
+--
+-- The '_wfDiags' predicate states that succesive nodes in a wave front lie
+-- on diagonals whose indices differ by two. This is leveraged by LiquidHaskell
+-- to check that the 'furthestReaching' precondition stating that the two nodes
+-- it compares lie on the same diagonal is satisfied within `dstep`.
+-- However, even though a more flexible predicate could be used to prove it,
+-- a compromise was made in preserving this invariant to keep the specification
+-- complexity low at a negligible performance penalty cost.
+-- This note documents this compromise.
+--
+-- To prove 'ses' terminates, wave fronts are restricted to be within the
+-- edit grid. This is done by placing checks for boundary nodes within 'dstep'
+-- to avoid constructing nodes outside the grid. 'dstep' leverages such checks
+-- in optimizations that rely on the observation that boundary nodes signal
+-- other nodes cannot compete to the goal:
+--
+--  * If a bottom boundary is found, all subsequent nodes are not considered.
+--
+--  * If a right boundary is found, all previously constructed child nodes
+--    can be dropped.
+--
+-- Both preserve the diagonal invariant, as the wave front would just become
+-- narrower. However, due to the asymmetry of list traversal, the first one is
+-- readily implemented, while the second requires an additional operation whose
+-- cost trumps the gain of not keeping them for next iterations (according to the
+-- existing benchmarks). Because of this, and 'stepAndMege' looking a two
+-- succesive nodes at a time, only the current iteration child /could/ be
+-- effectively dropped.
+--
+-- However, dropping the current iteration child node results in wave fronts
+-- with holes: now for every right boundary node found, a diagonal is not
+-- occupied. This requires the diagonal invariant to be changed to "diagonal
+-- indices in succesive nodes of a wave front differ by 2, unless a node lies
+-- on the right boundary, in which case its diagonal must differ from the previous
+-- by a factor of 2". It was decided to not follow this path, because the gain
+-- of not keeping this node was found to be negligible compared with the resulting
+-- increase in specification complexity.
+--------------------------------------------------------------------------------
+
+-- A wave front is a list of 'DL' nodes, all at the same edit distance @D@,
+-- with k-diagonals @D@, @D−2@, …, @-D+2@, @-D@.
+-- See [NOTE: diagonal-invariant]
+{-@ type WaveFront M N D = {xs : [DLN M N D] | _wfDiags (_kdiag (head xs)) xs} @-}
+
+--------------------------------------------------------------------------------
+-- * Proving the Algorithm's Termination in LiquidHaskell
+--
+-- The `ses` (_smallest edit script_) function termination is proved by defining
+-- a wave front's distance to the _endpoint_ as decreasing metric.
+-- This function is the implementation's entry point to the Myers diff algorithm,
+-- whose original specification waives the need for a termination proof by
+-- bounding the algorithm's outer loop by the known worst case edit script length,
+-- i.e. the sum of both input's lengths. These lengths are threaded through the
+-- implementation as phantom parameters for the following helpers to provide the
+-- LiquidHaskell specification a notion of the edit grid (as nodes '_withinBounds')
+-- and its end point.
+--------------------------------------------------------------------------------
+
+{-@ reflect _manhattanDistance @-}
+_manhattanDistance :: Int -> Int -> DL -> Int
+_manhattanDistance lena lenb dl  = lena - (poi dl) + lenb - (poj dl)
+
+{-@ reflect _wfDistanceToGoal @-}
+-- | The smallest manhattan distance from a wave front node to the goal @(lena, lenb)@.
+-- The empty wave front yields @lena + lenb + 2@, a sentinel strictly greater
+-- than any in-bounds node's distance, acting as the identity for the minimum.
+_wfDistanceToGoal :: Int -> Int -> [DL] -> Int
+_wfDistanceToGoal lena lenb [] = lena + lenb + 2
+_wfDistanceToGoal lena lenb (dl:dls) =
+  -- We avoid using 'min' here so that LH can unfold this definition.
+  if _manhattanDistance lena lenb dl < _wfDistanceToGoal lena lenb dls
+  then _manhattanDistance lena lenb dl
+  else _wfDistanceToGoal lena lenb dls
+
+{-@ inline _reducesDistanceToGoal @-}
+_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool
+_reducesDistanceToGoal lena lenb wf1 wf2 =
+  _wfDistanceToGoal lena lenb wf2 < _wfDistanceToGoal lena lenb wf1
+
+{-@ inline _withinBounds @-}
+{-@ _withinBounds :: lena : Nat -> lenb : Nat -> dl : DL
+                   -> {v:Bool | v <=> (poi dl <= lena && poj dl <= lenb) } @-}
+_withinBounds :: Int -> Int -> DL -> Bool
+_withinBounds lena lenb dl = poi dl <= lena && poj dl <= lenb
+
+{-@ inline endPoint @-}
+endPoint :: Int -> Int -> DL -> Bool
+endPoint lena lenb dl = poi dl == lena && poj dl == lenb
+
+-- This refinement type alias allows LiquidHaskell to reason about the function
+-- parameter of 'addsnake' by defining the out-of-bounds coordinates of a node as
+-- a sufficient condition for 'addsnake' to preserve it.
+{-@ type DiagPred M N = i : Nat -> j : Nat -> {b : Bool | ((i >= M || j >= N) => not b)} @-}
+
+-- | A lemma that expresses a lower bound of the wavefront distance in terms
+-- of the diagonal of the first node: @lena - lenb - k@
+--
+-- We assume all the nodes to be within the grid.
+--
+-- @lena - lenb@ is the diagonal of the goal. Informally, the
+-- shortest way from a node must necessarily visit all the intermediate
+-- diagonals. The minimum amount of diagonals to visit is given by the
+-- difference between the diagonal indices of the goal and the first element.
+--
+-- We can prove it manually like so:
+--
+-- For every node @dl = DL i j p@ we can prove
+-- @H(dl) = _manhattanDistance lena lenb dl >= lena - lenb - (i - j)@
+--
+-- @
+--   _manhattanDistance lena lenb dl
+-- =
+--   lena - (poi dl) + lenb - (poj dl)
+-- =
+--   lena - i + lenb - j
+-- =
+--   lena - lenb - (i - j) + 2 * (lenb - j)
+-- >=
+--   lena - lenb - (i - j)
+-- @
+--
+-- Since @H(dl)@ holds for every node in the wave front, it follows
+-- that the wave front distance is at least as large as the smallest of
+-- these bounds, which is @lena - lenb - k@ for the largest @k = i0 - j0@,
+-- which is the diagonal of the first node.
+--
+-- QED
+-- @
+{-@ _wfDistanceLowerBoundK
+      :: lena : Nat -> lenb : Nat -> {k : Int | lenb + k + 2 >= 0}
+      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags k v}
+      -> {_wfDistanceToGoal lena lenb xs >= lena - lenb - k}
+      / [len xs] @-}
+_wfDistanceLowerBoundK :: Int -> Int -> Int -> [DL] -> ()
+_wfDistanceLowerBoundK _    _    _ []      = ()
+_wfDistanceLowerBoundK lena lenb k (_:dls) = _wfDistanceLowerBoundK lena lenb (k - 2) dls
+
+-- | If a wave front's node (@prev@) is on the bottom boundary, then the following
+-- nodes lie farther from the goal. Intuitively, the reason is that the following
+-- nodes children would need more steps to cross @prev@'s diagonal to reach the goal.
+-- This lemma allows LH to reason about the case where nodes are discarded
+-- after a bottom-boundary node within 'dstep'.
+{-@
+_wfDistanceLowerBound
+      :: lena : Nat -> lenb : Nat -> {prev : DL | _withinBounds lena lenb prev}
+      -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags (_kdiag prev - 2) v}
+      -> { poj prev >= lenb =>  _wfDistanceToGoal lena lenb xs > _manhattanDistance lena lenb prev}
+ @-}
+_wfDistanceLowerBound :: Int -> Int -> DL -> [DL] -> ()
+_wfDistanceLowerBound lena lenb prev [] = ()
+_wfDistanceLowerBound lena lenb prev xs@(_:_) = ()
+  where
+    _lemma = _wfDistanceLowerBoundK lena lenb (_kdiag prev - 2) xs
+
+
+-- | The termination metric is non-negative: every in-bounds node has a
+-- non-negative manhattan distance to the goal, and the empty wave front
+-- yields the positive sentinel. This lemma is needed because the @Nat@ result
+-- refinement of the reflected '_wfDistanceToGoal' is not instantiated at
+-- logic-level  applications, while termination metrics must be provably
+-- non-negative.
+{-@ _minDistanceNonNegative
+      :: lena : Nat -> lenb : Nat
+      -> xs : [{dl : DL | _withinBounds lena lenb dl}]
+      -> {_wfDistanceToGoal lena lenb xs >= 0}
+      / [len xs] @-}
+_minDistanceNonNegative :: Int -> Int -> [DL] -> ()
+_minDistanceNonNegative _    _    []       = ()
+_minDistanceNonNegative lena lenb (_:dls) = _minDistanceNonNegative lena lenb dls