From 9e5928945794efd6659a42adbb7af0f867faff36 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 2 Jun 2022 09:49:16 -0400
Subject: [PATCH 1/2] Remove unreachable TVIntMod cases in What4 backend

These cases for `Z m` indices in the What4 implementation of `(@)` are
unreachable by virtue of the fact that the index must be `Integral`. Let's
remove them to make the code simpler.

See https://github.com/GaloisInc/cryptol/issues/1359#issuecomment-1142107469
for where this was originally noticed.
---
 src/Cryptol/Eval/What4.hs | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index 0e6bc98f1..849fbe289 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/src/Cryptol/Eval/What4.hs
@@ -505,7 +505,7 @@ indexFront_int ::
   TValue ->
   SInteger (What4 sym) ->
   SEval (What4 sym) (Value sym)
-indexFront_int sym mblen _a xs ix idx
+indexFront_int sym mblen _a xs _ix idx
   | Just i <- W4.asInteger idx
   = lookupSeqMap xs i
 
@@ -535,16 +535,13 @@ indexFront_int sym mblen _a xs ix idx
           _                        -> Nothing
       )
 
-    -- Maximum possible in-bounds index given `Z m`
-    -- type information and the length
-    -- of the sequence. If the sequences is infinite and the
-    -- integer is unbounded, there isn't much we can do.
+    -- Maximum possible in-bounds index given the length
+    -- of the sequence. If the sequence is infinite, there
+    -- isn't much we can do.
     maxIdx =
-      case (mblen, ix) of
-        (Nat n, TVIntMod m)  -> Just (min (toInteger n) (toInteger m))
-        (Nat n, _)           -> Just n
-        (_    , TVIntMod m)  -> Just m
-        _                    -> Nothing
+      case mblen of
+        Nat n -> Just n
+        Inf   -> Nothing
 indexFront_segs ::
   W4.IsSymExprBuilder sym =>
   What4 sym ->

From c37a71b4c5d09d12e7c7fc9dbb85a28d0758784a Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 2 Jun 2022 10:15:33 -0400
Subject: [PATCH 2/2] 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                         | 7 +++++++
 src/Cryptol/Eval/What4.hs          | 2 +-
 tests/issues/issue1359.icry        | 7 +++++++
 tests/issues/issue1359.icry.stdout | 5 +++++
 4 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/issues/issue1359.icry
 create mode 100644 tests/issues/issue1359.icry.stdout

diff --git a/CHANGES.md b/CHANGES.md
index eb93b7116..8207c3258 100644
--- a/CHANGES.md
+++ b/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
diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index 849fbe289..b53c0e863 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/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 =>
diff --git a/tests/issues/issue1359.icry b/tests/issues/issue1359.icry
new file mode 100644
index 000000000..487e0a67c
--- /dev/null
+++ b/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))
diff --git a/tests/issues/issue1359.icry.stdout b/tests/issues/issue1359.icry.stdout
new file mode 100644
index 000000000..182b749b0
--- /dev/null
+++ b/tests/issues/issue1359.icry.stdout
@@ -0,0 +1,5 @@
+Loading module Cryptol
+Safe
+Safe
+Safe
+Safe