Relax `_wfDiags` invariant to remove artificial node from `dstep`

[ninioArtillero]

This ticket is about deciding whether to relax the _wfDiags invariant to allow wave front diagonal indices to have wider gaps. Currently, the invariant states that diagonal indices for successive wave front nodes must differ by two. For dstep to preserve this invariant, stepAndMerge produces an artificial node whenever a node on the right boundary is found. The comment there is explicit about this:

        (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

The referenced source note goes into some details. In 2d3944d we have a working specification with the invariant relaxed as follows:

{-@ reflect _wfDiags @-}
{-@ _wfDiags :: Int -> Int -> xs : [DL] -> Bool / [len xs] @-}
-- | True if successive diagonal indices of a wave front differ by 2
-- or a multiple of 2 whenever a node lying on the right boundary is found.
_wfDiags 
  :: Int    -- ^ The length of the first input, determines the right boundary 
  -> Int    -- ^ The diagonal index of the previous node 
  -> [DL]   -- ^ A wave front
  -> Bool
_wfDiags _ _ [] = True
_wfDiags lena k (dl:dls) =
    (poi dl < lena && poi dl - poj dl == k - 2
      ||
     poi dl >= lena && mod (k - (poi dl - poj dl)) 2 == 0 && poi dl - poj dl <= k - 2
    ) &&
    _wfDiags lena (poi dl - poj dl) dls

This renders the vStep prev artificial node from the former excerpt unnecessary. However, as stated in [NOTE]: diagonal-invariant this results in a more complex specification. The possibility of simplifying this spec is not ruled out, but until this is accomplished the question of whether to integrate this change remains because the resulting performance gain (according to the existing benchmarks) doesn't justify it in my opinion (which I'm open to revisit).