Prove termination of diff algorithm implementation by ninioArtillero · Pull Request #37 · seereason/Diff

ninioArtillero · 2026-08-01T00:15:43Z

All commits build independenlty and can be read in sequence.

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.

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.

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%

facundominguez · 2026-08-01T13:03:03Z

+            -- HACK: This check saves us from an unneeded call to furthestReaching,
+            -- as the horizontal child of the next node would be out-of-bounds,
+            -- but in fact we could drop this child node altogether because
+            -- the next node being on the right border means all previous nodes
+            -- would need to cross the next node's diagonal in more steps,
+            -- and thus cannot compete to the endpoint.
+            -- However, this would result in a negligible performance gain
+            -- and the loss of the wave front diagonal invariant,
+            -- so we keep it for now.
+            if poi next >= lena then addsnake lena lenb cd (vStep prev) : stepAndMerge next rest


Adding vStep prev in the middle of the wavefront is rather arbitrary.

I'm wondering if we could reformulate the wavefront invariant from

prev and next are two diagonals apart

to

prev and next are two diagonals apart if poi next < lena

This should suffice to ensure that furthestReaching is always called with nodes in the same diagonal, and it is the reason that motivates the wavefront invariant.

and it is the reason that motivates the wavefront invariant.

Maybe this should be said at the place where the Wavefront type alias is defined.

facundominguez · 2026-08-01T13:13:21Z

+-- calls to other lifted functions inside a reflected body prevent PLE
+-- from unfolding this function's defining equations.


I don't think LH is designed to work like that. Maybe there is a bug when mixing inlined and reflected functions?

One workaround to try is to make all functions reflected.

facundominguez · 2026-08-01T13:36:37Z

+-- In particular, this justifies discarding the nodes after a bottom-boundary node:
+-- suppose @(i, lenb)@ is on diagonal @k + 2@, then the following nodes would
+-- have distances at least @_manhattanDistance lena lenb i lenb + 2@, thus
+-- they cannot beat that node's surviving children in the race to the goal.


It is still unclear how this relates to the previous proof.

In any case, it may be worth reviewing the need for the lemma before polishing this.

facundominguez · 2026-08-01T13:38:32Z

+      -> {_wfDistanceToGoal lena lenb xs == lena + lenb + 1
+          || _wfDistanceToGoal lena lenb xs >= lena - lenb - k}


This disjunction is not exactly what has been discussed before.

facundominguez · 2026-08-01T15:06:32Z

+-- | Attach a proof term (typically a lemma application) to a value.
+-- The lemma's postcontition enters the verification context at the
+-- application site while the value is returned unchanged.
+{-@ withProof :: x:a -> b -> {v:a | v = x} @-}
+withProof :: a -> b -> a
+withProof x _ = x


Is this necessary?

It's not, but so far the lemmas seem to be necessary for the proof to proceed, and in stepAndMerge passing it in a let results in three leves of nested expressions, which felt a little awkward. I thought about importing the homonymous function from ProofCombinators (or even ?), but preffered defining it here rather than adding another dependency (which would need to be added to both Diff and `Diff-liquidhaskell) just for a single combinator.

withProof seems to be duplicating ? from liquid-prelude, while ? produces less work for LH, and should allow reflecting functions that use lemmas.

facundominguez · 2026-08-01T16:30:40Z

+                                          && (poj prev < lenb <=> len v > 0)
+                                          && (len v > 0 =>
+                                               _kdiag (head v) == _kdiag prev - 1)
+                                          && (poj prev < lenb =>


It is unclear why this condition is necessary. It might depend on what the _wfDistanceToGoal is defined to be for the empty list.

facundominguez · 2026-08-03T14:37:09Z

+                -- 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.
+                `withProof` _wfDistanceLowerBound lena lenb (_kdiag next - 2) rest


This lemma looks unnecessary. This is my reasoning skipping the prevalent lena and lenb parameters:

By preconditions we know that distanceToGoal (next:rest) > 0.
Then, by definition of distanceToGoal we know that distanceToGoal rest > 0, which is the precondition of the recursive call stepAndMerge next rest.

Next we can prove that stepAndMerge decreases distanceToGoal as follows:

distanceToGoal (stepAndMerge prev (next:rest)) < distanceToGoal (next:rest) == (by definition of stepAndMerge and distanceToGoal and IF guard "poi next < lena") ( manhattanDistance (addsnake cd (furthestReaching (vStep prev) (hStep next)) `min` distanceToGoal (stepAndMerge next rest) ) < (manhattanDistance next `min` distanceToGoal rest) <== (by definition of min) H1 && HI where HI: distanceToGoal (stepAndMerge next rest) < distanceToGoal rest H1: manhattanDistance (addsnake cd (furthestReaching (vStep prev) (hStep next)) < manhattanDistance next

HI holds because it is the postcondition of the recursive call.

Now we prove H1

manhattanDistance (addsnake cd (furthestReaching (vStep prev) (hStep next)) <= (by postcondition of addsnake) manhattanDistance (furthestReaching (vStep prev) (hStep next)) == (by definition of furthestReaching) min (manhattanDistance (vStep prev)) (manhattanDistance (hStep next)) <= (by definition of min) manhattanDistance (hStep next) < (by definition of hStep and IF guard "poi next < lena") manhattanDistance next

QED

Isn't taking HI (postcondition) as given assuming what we want to prove?

I don't think so. It is the inductive hypothesis. We assume the property holds for rest, and we want to prove it for next:rest.

…Goal`

facundominguez · 2026-08-03T19:12:03Z

This PR should revert 33bf8bc, which is made redundant by a0f181c.

facundominguez · 2026-08-05T12:01:08Z

+
+{-@ reflect _manhattanDistance @-}
+{-@ _manhattanDistance :: lena : Nat -> lenb : Nat -> {i : Nat | lena >= i} -> { j : Nat | lenb >= j} -> Nat @-}
+_manhattanDistance :: Int -> Int -> Int -> Int -> Int


Maybe this could be changed or augmented with another function with type:

_manhattanDistanceDL :: Int -> Int -> DL -> Int

ninioArtillero added 5 commits July 31, 2026 18:13

Refactor/optimize dstep by removing out-of-bound nodes

a0f181c

ses termination proof

5eda54d

facundominguez reviewed Aug 1, 2026

View reviewed changes

Comment thread src/Data/Algorithm/Diff.hs Outdated

facundominguez reviewed Aug 1, 2026

View reviewed changes

Comment thread src/Data/Algorithm/Diff.hs Outdated

facundominguez reviewed Aug 1, 2026

View reviewed changes

Comment thread src/Data/Algorithm/Diff.hs Outdated

facundominguez reviewed Aug 1, 2026

View reviewed changes

facundominguez reviewed Aug 3, 2026

View reviewed changes

ninioArtillero added 4 commits August 3, 2026 11:23

Move and reflect step functions in the top level to reduce spec

d02c7fc

Rename spec variable to match source

d5ce740

Simplify workaround documentation

1bf7759

Reflect _manhattanDistance to allow PLE unfolding of `_wfDistanceTo…

29d584a

…Goal`

facundominguez reviewed Aug 5, 2026

View reviewed changes

		-- calls to other lifted functions inside a reflected body prevent PLE
		-- from unfolding this function's defining equations.

		-> {_wfDistanceToGoal lena lenb xs == lena + lenb + 1
		\|\| _wfDistanceToGoal lena lenb xs >= lena - lenb - k}

Uh oh!

Conversation

ninioArtillero commented Aug 1, 2026

Uh oh!

facundominguez Aug 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

facundominguez Aug 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

facundominguez Aug 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

facundominguez commented Aug 3, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

facundominguez Aug 1, 2026 •

edited

Loading

facundominguez Aug 1, 2026 •

edited

Loading

facundominguez Aug 3, 2026 •

edited

Loading