saw-core: Fix handling of atWithDefault for infinite bit sequences

When calling `atWithDefault n d v i`, `d` should be returned if `i` is greater
than or equal to `n`. `atWithDefault` is implemented as a primitive, so we must
ensure that this is done in `saw-core`'s `atWithDefaultOp` function. While
`atWithDefaultOp` was handling this correctly for generic infinite sequences, it
was _not_ correctly handling the special case of infinite bit sequences. This
led to the issues reported in #1768.

This patch fixes #1768 by introducing a `bpBvAtWithDefault` combinator that
implements the defaulting behavior above in terms of `bpBvAt`. I've added a test
case to demonstrate that the test case from #1768 now works as expected.

intTests/test1768/test.cry

@@ -0,0 +1,4 @@
+f : [2] -> [10]
+f x = take y
+  where
+    y = x # y

intTests/test1768/test.saw

@@ -0,0 +1,5 @@
+import "test.cry";
+print {{ f 0b11 }};
+print {{ f 0b10 }};
+print {{ f 0b00 }};
+sat z3 {{ \x -> f x == zero }};

intTests/test1768/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -769,21 +769,38 @@ atWithDefaultOp bp =
       VNat i ->
         case x of
           VVector xv -> lift (force (vecIdx d xv (fromIntegral i))) -- FIXME dangerous fromIntegral
-          VWord xw -> lift (VBool <$> bpBvAt bp xw (fromIntegral i)) -- FIXME dangerous fromIntegral
+          VWord xw -> lift (bpBvAtWithDefault bp (fromIntegral n) (force d) xw (fromIntegral i)) -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
       VBVToNat _sz i | bpIsSymbolicEvaluator bp -> do
         iv <- lift (toBits (bpUnpack bp) i)
         case x of
           VVector xv ->
             lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (force . vecIdx d xv) iv -- FIXME dangerous fromIntegral
           VWord xw ->
-            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (liftM VBool . bpBvAt bp xw) iv -- FIXME dangerous fromIntegral
+            lift $ selectV (lazyMuxValue bp tp) (fromIntegral n - 1) (bpBvAtWithDefault bp (fromIntegral n) (force d) xw) iv -- FIXME dangerous fromIntegral
           _ -> throwE "atOp: expected vector"
 
       VIntToNat _i | bpIsSymbolicEvaluator bp -> panic "atWithDefault: symbolic integer TODO"
 
       _ -> throwE $ "atOp: expected Nat, got " <> Text.pack (show idx)
 
+-- | @bpBvAtWithDefault bp w d vw i@ returns @bpBvAt bp vw i@ if @i@ is between
+-- @0@ (inclusive) and @w@ (exclusive), the bit width of @vw@. Otherwise, it
+-- returns @d@.
+bpBvAtWithDefault ::
+  VMonad l =>
+  BasePrims l ->
+  Int ->
+  MValue l ->
+  VWord l ->
+  Int ->
+  MValue l
+bpBvAtWithDefault bp w d vw i
+  | 0 <= i && i < w
+  = VBool <$> bpBvAt bp vw i
+  | otherwise
+  = d
+
 -- upd :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> a -> Vec n a;
 updOp :: (VMonadLazy l, Show (Extra l)) => BasePrims l -> Prim l
 updOp bp =