Fix off-by-one error in What4 implementation of (@)

In the case where the index is a symbolic `Integer` and the sequence is of
length `n`, the What4 backend mistakenly chose `n` to be the largest possible
index. This corrects it to instead be `n - 1`.

Fixes #1359.

CHANGES.md

@@ -1,3 +1,10 @@
+# next
+
+## Bug fixes
+
+* Fix a bug in the What4 backend that could cause applications of `(@)` with
+  symbolic `Integer` indices to become out of bounds (#1359).
+
 # 2.13.0
 
 ## Language changes

src/Cryptol/Eval/What4.hs

@@ -540,7 +540,7 @@ indexFront_int sym mblen _a xs _ix idx
     -- isn't much we can do.
     maxIdx =
       case mblen of
-        Nat n -> Just n
+        Nat n -> Just (n - 1)
         Inf   -> Nothing
 indexFront_segs ::
   W4.IsSymExprBuilder sym =>

tests/issues/issue1359.icry

@@ -0,0 +1,7 @@
+:set prover=sbv-z3
+:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
+:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))
+
+:set prover=w4-z3
+:safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)
+:safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))

tests/issues/issue1359.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Safe
+Safe
+Safe
+Safe