Prove termination of diff algorithm implementation - #37
Conversation
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%
| -- 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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
| -- calls to other lifted functions inside a reflected body prevent PLE | ||
| -- from unfolding this function's defining equations. |
There was a problem hiding this comment.
I don't think LH is designed to work like that. Maybe there is a bug when mixing inlined and reflected functions?
There was a problem hiding this comment.
One workaround to try is to make all functions reflected.
There was a problem hiding this comment.
I removed this wrong statement in 29d584a; changing to reflect indeed allow to use it in the source body and get it unfolded in the logic. From comments I read somewhere, and my current observations, it seems that inlined functions are substitued before constraint solving, meaning that PLE would fail to expand them if it were to produce them.
Changing current inline for reflect raises the checked constraint from 1608 to 1754, but using just a single lifting mechanism could be a better practice.
| -- | 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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
withProof seems to be duplicating ? from liquid-prelude, while ? produces less work for LH, and should allow reflecting functions that use lemmas.
There was a problem hiding this comment.
The problem I see is this would affect downstream Diff users because they would have to build liquid-prelude. I'm not sure ? is worth its weight.
There was a problem hiding this comment.
To not affect Diff dependencies it would need to be an import provided either with conditional compilation, or Diff and Diff-liquidhaskell would need to use different implementations of a module that imports the ?.
Yet another solution would be to treat const the same as ? in LH, so we don't need to import ?.
I guess you can keep withProof for now, and mention this problem in a comment.
| && (poj prev < lenb <=> len v > 0) | ||
| && (len v > 0 => | ||
| _kdiag (head v) == _kdiag prev - 1) | ||
| && (poj prev < lenb => |
There was a problem hiding this comment.
It is unclear why this condition is necessary. It might depend on what the _wfDistanceToGoal is defined to be for the empty list.
…eason#28) The optimization introduced in `dstep` (narrowing the wave front to only within bound nodes) solves the problem this additional equations addressed in seereason@33bf8bc They are removed to avoid unnecessary complexity.
Co-authored-by: Facundo Domínguez <facundominguez@gmail.com>
9928375 to
e5cb8c3
Compare
2 participants
All commits build independenlty and can be read in sequence.