From aa768b7b2ee3457155bb8761fd5f5448d95c3d26 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 20 Oct 2020 13:27:13 -0700
Subject: [PATCH 01/12] Add `TValue` constructor for `IntMod` type.

Also reimplement `IntMod` type in simulator backends
to use it.
---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs        | 1 +
 saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs | 1 -
 saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs      | 1 -
 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs  | 1 -
 saw-core/src/Verifier/SAW/Simulator/Concrete.hs     | 1 -
 saw-core/src/Verifier/SAW/Simulator/Prims.hs        | 2 ++
 saw-core/src/Verifier/SAW/Simulator/RME.hs          | 1 -
 saw-core/src/Verifier/SAW/Simulator/Value.hs        | 3 +++
 8 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 60be46e8..7e118c24 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1367,6 +1367,7 @@ asCryptolTypeValue v =
   case v of
     SC.VBoolType -> return C.tBit
     SC.VIntType -> return C.tInteger
+    SC.VIntModType n -> return (C.tIntMod (C.tNum n))
     SC.VArrayType v1 v2 -> do
       t1 <- asCryptolTypeValue v1
       t2 <- asCryptolTypeValue v2
diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
index 7b11c20d..fc2c35b8 100644
--- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
+++ b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
@@ -269,7 +269,6 @@ beConstMap be =
   , ("Prelude.bvToInt" , bvToIntOp be)
   , ("Prelude.sbvToInt", sbvToIntOp be)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", constFun (VFun force))
   , ("Prelude.intModEq"  , intModEqOp be)
diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index c51dc3ce..bc536604 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -196,7 +196,6 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , constFun (VFun force))
   , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp)
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index f2c3d63c..00383116 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -250,7 +250,6 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , constFun (VFun force))
   , ("Prelude.fromIntMod", fromIntModOp sym)
   , ("Prelude.intModEq"  , intModEqOp sym)
diff --git a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
index b8fac5a2..a227ab06 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
@@ -253,7 +253,6 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", constFun (VFun force))
   , ("Prelude.intModEq"  , intModEqOp)
diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
index 5131e532..f1f70fab 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
@@ -226,6 +226,8 @@ constMap bp = Map.fromList
 -}
   , ("Prelude.intMin", intBinOp "intMin" (bpIntMin bp))
   , ("Prelude.intMax", intBinOp "intMax" (bpIntMax bp))
+  -- Modular Integers
+  , ("Prelude.IntMod", natFun $ \n -> pure $ TValue (VIntModType n))
   -- Vectors
   , ("Prelude.Vec", vecTypeOp)
   , ("Prelude.gen", genOp)
diff --git a/saw-core/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs
index 0135b6ba..b880030e 100644
--- a/saw-core/src/Verifier/SAW/Simulator/RME.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/RME.hs
@@ -240,7 +240,6 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", constFun (VFun force))
   , ("Prelude.intModEq"  , intModEqOp)
diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs
index 12c94923..9a52b487 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Value.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs
@@ -69,6 +69,7 @@ data TValue l
   = VVecType !Natural !(TValue l)
   | VBoolType
   | VIntType
+  | VIntModType !Natural
   | VArrayType !(TValue l) !(TValue l)
   | VPiType !(TValue l) !(Thunk l -> EvalM l (TValue l))
   | VUnitType
@@ -172,6 +173,7 @@ instance Show (Extra l) => Show (TValue l) where
     case v of
       VBoolType      -> showString "Bool"
       VIntType       -> showString "Integer"
+      VIntModType n  -> showParen True (showString "IntMod " . shows n)
       VArrayType{}   -> showString "Array"
       VPiType t _    -> showParen True
                         (shows t . showString " -> ...")
@@ -271,6 +273,7 @@ suffixTValue tv =
          Just ("_Vec_" ++ show n ++ a')
     VBoolType -> Just "_Bool"
     VIntType -> Just "_Int"
+    VIntModType n -> Just ("_IntMod_" ++ show n)
     VArrayType a b ->
       do a' <- suffixTValue a
          b' <- suffixTValue b

From 69707b4b550451b42f4c6e31b88617ab93d2e35c Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 10:03:57 -0700
Subject: [PATCH 02/12] Avoid using `error` within what4 backend.

---
 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index 00383116..e16d90d2 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -883,7 +883,8 @@ argTypes :: IsSymExprBuilder sym => TValue (What4 sym) -> IO [TValue (What4 sym)
 argTypes v =
   case v of
     VPiType v1 f ->
-      do v2 <- f (error "argTypes: unsupported dependent SAW-Core type")
+      do x <- delay (fail "argTypes: unsupported dependent SAW-Core type")
+         v2 <- f x
          vs <- argTypes v2
          return (v1 : vs)
     _ -> return []

From 337aa80c915b8961170eb2cd34fae74b64e0c4f9 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 10:44:14 -0700
Subject: [PATCH 03/12] Add `VIntMod` constructor to `Value` datatype.

Also convert primitive implementations to use it.
---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs  |  2 +-
 .../src/Verifier/SAW/Simulator/BitBlast.hs    | 24 ++++++++++++-------
 .../src/Verifier/SAW/Simulator/SBV.hs         | 20 ++++++++++------
 .../src/Verifier/SAW/Simulator/What4.hs       | 24 ++++++++++++-------
 .../src/Verifier/SAW/Simulator/Concrete.hs    | 16 ++++++-------
 saw-core/src/Verifier/SAW/Simulator/Prims.hs  |  6 +++++
 saw-core/src/Verifier/SAW/Simulator/RME.hs    | 24 ++++++++++++-------
 saw-core/src/Verifier/SAW/Simulator/Value.hs  |  2 ++
 8 files changed, 75 insertions(+), 43 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 7e118c24..16735b1b 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1462,7 +1462,7 @@ exportValue ty v = case ty of
     V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
 
   TV.TVIntMod _modulus ->
-    V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")
+    V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")
 
   TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")"
 
diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
index fc2c35b8..24f393b4 100644
--- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
+++ b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
@@ -270,7 +270,7 @@ beConstMap be =
   , ("Prelude.sbvToInt", sbvToIntOp be)
   -- Integers mod n
   , ("Prelude.toIntMod"  , toIntModOp)
-  , ("Prelude.fromIntMod", constFun (VFun force))
+  , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp be)
   , ("Prelude.intModAdd" , intModBinOp (+))
   , ("Prelude.intModSub" , intModBinOp (-))
@@ -352,27 +352,33 @@ toIntModOp :: BValue l
 toIntModOp =
   Prims.natFun $ \n -> return $
   Prims.intFun "toIntModOp" $ \x -> return $
-  VInt (x `mod` toInteger n)
+  VIntMod n (x `mod` toInteger n)
+
+fromIntModOp :: BValue l
+fromIntModOp =
+  constFun $
+  Prims.intModFun "fromIntModOp" $ \x -> return $
+  VInt x
 
 intModEqOp :: AIG.IsAIG l g => g s -> BValue (l s)
 intModEqOp be =
   constFun $
-  Prims.intFun "intModEqOp" $ \x -> return $
-  Prims.intFun "intModEqOp" $ \y -> return $
+  Prims.intModFun "intModEqOp" $ \x -> return $
+  Prims.intModFun "intModEqOp" $ \y -> return $
   VBool (AIG.constant be (x == y))
 
 intModBinOp :: (Integer -> Integer -> Integer) -> BValue l
 intModBinOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModBinOp x" $ \x -> return $
-  Prims.intFun "intModBinOp y" $ \y -> return $
-  VInt (f x y `mod` toInteger n)
+  Prims.intModFun "intModBinOp x" $ \x -> return $
+  Prims.intModFun "intModBinOp y" $ \y -> return $
+  VIntMod n (f x y `mod` toInteger n)
 
 intModUnOp :: (Integer -> Integer) -> BValue l
 intModUnOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModUnOp" $ \x -> return $
-  VInt (f x `mod` toInteger n)
+  Prims.intModFun "intModUnOp" $ \x -> return $
+  VIntMod n (f x `mod` toInteger n)
 
 ----------------------------------------
 
diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index bc536604..b53ca245 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -196,7 +196,7 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.toIntMod"  , constFun (VFun force))
+  , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp)
   , ("Prelude.intModAdd" , intModBinOp svPlus)
@@ -433,6 +433,12 @@ svShiftR b x i = svIte b (svNot (svShiftRight (svNot x) i)) (svShiftRight x i)
 ------------------------------------------------------------
 -- Integers mod n
 
+toIntModOp :: SValue
+toIntModOp =
+  Prims.natFun' "toIntMod" $ \n -> pure $
+  Prims.intFun "toIntMod" $ \x -> pure $
+  VIntMod n x
+
 fromIntModOp :: SValue
 fromIntModOp =
   Prims.natFun $ \n -> return $
@@ -442,23 +448,23 @@ fromIntModOp =
 intModEqOp :: SValue
 intModEqOp =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModEqOp" $ \x -> return $
-  Prims.intFun "intModEqOp" $ \y -> return $
+  Prims.intModFun "intModEqOp" $ \x -> return $
+  Prims.intModFun "intModEqOp" $ \y -> return $
   let modulus = literalSInteger (toInteger n)
   in VBool (svEqual (svRem (svMinus x y) modulus) (literalSInteger 0))
 
 intModBinOp :: (SInteger -> SInteger -> SInteger) -> SValue
 intModBinOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModBinOp x" $ \x -> return $
-  Prims.intFun "intModBinOp y" $ \y -> return $
-  VInt (normalizeIntMod n (f x y))
+  Prims.intModFun "intModBinOp x" $ \x -> return $
+  Prims.intModFun "intModBinOp y" $ \y -> return $
+  VIntMod n (normalizeIntMod n (f x y))
 
 intModUnOp :: (SInteger -> SInteger) -> SValue
 intModUnOp f =
   Prims.natFun $ \n -> return $
   Prims.intFun "intModUnOp" $ \x -> return $
-  VInt (normalizeIntMod n (f x))
+  VIntMod n (normalizeIntMod n (f x))
 
 normalizeIntMod :: Natural -> SInteger -> SInteger
 normalizeIntMod n x =
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index e16d90d2..ef9d6c68 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -250,7 +250,7 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.toIntMod"  , constFun (VFun force))
+  , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", fromIntModOp sym)
   , ("Prelude.intModEq"  , intModEqOp sym)
   , ("Prelude.intModAdd" , intModBinOp sym W.intAdd)
@@ -454,17 +454,23 @@ intMax sym i1 i2 = do
 ------------------------------------------------------------
 -- Integers mod n
 
+toIntModOp :: SValue sym
+toIntModOp =
+  Prims.natFun' "toIntMod" $ \n -> pure $
+  Prims.intFun "toIntMod" $ \x -> pure $
+  VIntMod n x
+
 fromIntModOp :: IsExprBuilder sym => sym -> SValue sym
 fromIntModOp sym =
   Prims.natFun $ \n -> return $
   Prims.intFun "fromIntModOp" $ \x ->
-  VInt <$> (W.intMod sym x =<< W.intLit sym (toInteger n))
+  VIntMod n <$> (W.intMod sym x =<< W.intLit sym (toInteger n))
 
 intModEqOp :: IsExprBuilder sym => sym -> SValue sym
 intModEqOp sym =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModEqOp" $ \x -> return $
-  Prims.intFun "intModEqOp" $ \y ->
+  Prims.intModFun "intModEqOp" $ \x -> return $
+  Prims.intModFun "intModEqOp" $ \y ->
   do modulus <- W.intLit sym (toInteger n)
      d <- W.intSub sym x y
      r <- W.intMod sym d modulus
@@ -476,17 +482,17 @@ intModBinOp ::
   (sym -> SInt sym -> SInt sym -> IO (SInt sym)) -> SValue sym
 intModBinOp sym f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModBinOp x" $ \x -> return $
-  Prims.intFun "intModBinOp y" $ \y ->
-  VInt <$> (normalizeIntMod sym n =<< f sym x y)
+  Prims.intModFun "intModBinOp x" $ \x -> return $
+  Prims.intModFun "intModBinOp y" $ \y ->
+  VIntMod n <$> (normalizeIntMod sym n =<< f sym x y)
 
 intModUnOp ::
   IsExprBuilder sym => sym ->
   (sym -> SInt sym -> IO (SInt sym)) -> SValue sym
 intModUnOp sym f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModUnOp" $ \x ->
-  VInt <$> (normalizeIntMod sym n =<< f sym x)
+  Prims.intModFun "intModUnOp" $ \x ->
+  VIntMod n <$> (normalizeIntMod sym n =<< f sym x)
 
 normalizeIntMod :: IsExprBuilder sym => sym -> Natural -> SInt sym -> IO (SInt sym)
 normalizeIntMod sym n x =
diff --git a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
index a227ab06..2f76992c 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
@@ -318,27 +318,27 @@ toIntModOp :: CValue
 toIntModOp =
   Prims.natFun $ \n -> return $
   Prims.intFun "toIntModOp" $ \x -> return $
-  VInt (x `mod` toInteger n)
+  VIntMod n (x `mod` toInteger n)
 
 intModEqOp :: CValue
 intModEqOp =
   constFun $
-  Prims.intFun "intModEqOp" $ \x -> return $
-  Prims.intFun "intModEqOp" $ \y -> return $
+  Prims.intModFun "intModEqOp" $ \x -> return $
+  Prims.intModFun "intModEqOp" $ \y -> return $
   VBool (x == y)
 
 intModBinOp :: (Integer -> Integer -> Integer) -> CValue
 intModBinOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModBinOp x" $ \x -> return $
-  Prims.intFun "intModBinOp y" $ \y -> return $
-  VInt (f x y `mod` toInteger n)
+  Prims.intModFun "intModBinOp x" $ \x -> return $
+  Prims.intModFun "intModBinOp y" $ \y -> return $
+  VIntMod n (f x y `mod` toInteger n)
 
 intModUnOp :: (Integer -> Integer) -> CValue
 intModUnOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModUnOp" $ \x -> return $
-  VInt (f x `mod` toInteger n)
+  Prims.intModFun "intModUnOp" $ \x -> return $
+  VIntMod n (f x `mod` toInteger n)
 
 ------------------------------------------------------------
 
diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
index f1f70fab..7666a582 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
@@ -297,6 +297,11 @@ intFun msg f = strictFun g
   where g (VInt i) = f i
         g _ = panic $ "expected Integer "++ msg
 
+intModFun :: VMonad l => String -> (VInt l -> MValue l) -> Value l
+intModFun msg f = strictFun g
+  where g (VIntMod _ i) = f i
+        g _ = panic $ "expected IntMod "++ msg
+
 toBool :: Show (Extra l) => Value l -> VBool l
 toBool (VBool b) = b
 toBool x = panic $ unwords ["Verifier.SAW.Simulator.toBool", show x]
@@ -1251,6 +1256,7 @@ muxValue bp b = value
     value (VBool x)         (VBool y)         = VBool <$> bpMuxBool bp b x y
     value (VWord x)         (VWord y)         = VWord <$> bpMuxWord bp b x y
     value (VInt x)          (VInt y)          = VInt <$> bpMuxInt bp b x y
+    value (VIntMod n x)     (VIntMod _ y)     = VIntMod n <$> bpMuxInt bp b x y
     value (VNat m)          (VNat n)          | m == n = return $ VNat m
     value (VString x)       (VString y)       | x == y = return $ VString x
     value (VFloat x)        (VFloat y)        | x == y = return $ VFloat x
diff --git a/saw-core/src/Verifier/SAW/Simulator/RME.hs b/saw-core/src/Verifier/SAW/Simulator/RME.hs
index b880030e..1991f1ee 100644
--- a/saw-core/src/Verifier/SAW/Simulator/RME.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/RME.hs
@@ -241,7 +241,7 @@ constMap =
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
   , ("Prelude.toIntMod"  , toIntModOp)
-  , ("Prelude.fromIntMod", constFun (VFun force))
+  , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp)
   , ("Prelude.intModAdd" , intModBinOp (+))
   , ("Prelude.intModSub" , intModBinOp (-))
@@ -300,27 +300,33 @@ toIntModOp :: RValue
 toIntModOp =
   Prims.natFun $ \n -> return $
   Prims.intFun "toIntModOp" $ \x -> return $
-  VInt (x `mod` toInteger n)
+  VIntMod n (x `mod` toInteger n)
+
+fromIntModOp :: RValue
+fromIntModOp =
+  constFun $
+  Prims.intModFun "fromIntModOp" $ \x -> return $
+  VInt x
 
 intModEqOp :: RValue
 intModEqOp =
   constFun $
-  Prims.intFun "intModEqOp" $ \x -> return $
-  Prims.intFun "intModEqOp" $ \y -> return $
+  Prims.intModFun "intModEqOp" $ \x -> return $
+  Prims.intModFun "intModEqOp" $ \y -> return $
   VBool (RME.constant (x == y))
 
 intModBinOp :: (Integer -> Integer -> Integer) -> RValue
 intModBinOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModBinOp x" $ \x -> return $
-  Prims.intFun "intModBinOp y" $ \y -> return $
-  VInt (f x y `mod` toInteger n)
+  Prims.intModFun "intModBinOp x" $ \x -> return $
+  Prims.intModFun "intModBinOp y" $ \y -> return $
+  VIntMod n (f x y `mod` toInteger n)
 
 intModUnOp :: (Integer -> Integer) -> RValue
 intModUnOp f =
   Prims.natFun $ \n -> return $
-  Prims.intFun "intModUnOp" $ \x -> return $
-  VInt (f x `mod` toInteger n)
+  Prims.intModFun "intModUnOp" $ \x -> return $
+  VIntMod n (f x `mod` toInteger n)
 
 ----------------------------------------
 
diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs
index 9a52b487..34030ed5 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Value.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs
@@ -56,6 +56,7 @@ data Value l
   | VToNat (Value l)
   | VNat !Natural
   | VInt (VInt l)
+  | VIntMod !Natural (VInt l)
   | VArray (VArray l)
   | VString !String
   | VFloat !Float
@@ -156,6 +157,7 @@ instance Show (Extra l) => Show (Value l) where
       VToNat x       -> showString "bvToNat " . showParen True (shows x)
       VNat n         -> shows n
       VInt _         -> showString "<<integer>>"
+      VIntMod n _    -> showString ("<<Z " ++ show n ++ ">>")
       VArray{}       -> showString "<<array>>"
       VFloat float   -> shows float
       VDouble double -> shows double

From 7fd75f90eb3e9f29767ed6845bb83dbaced7b8a3 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 14:14:11 -0700
Subject: [PATCH 04/12] Add `scIntModType` to SharedTerm library.

---
 saw-core/src/Verifier/SAW/SharedTerm.hs | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index b7c4f9ce..7d6ab1f8 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -170,6 +170,8 @@ module Verifier.SAW.SharedTerm
   , scIntEq, scIntLe, scIntLt
   , scIntToNat, scNatToInt
   , scIntToBv, scBvToInt, scSbvToInt
+    -- *** IntMod
+  , scIntModType
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1699,6 +1701,15 @@ scSbvToInt
 scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x]
 
 
+-- Primitive operations on IntMod
+
+-- | Create a term representing the prelude @IntMod@ type.
+--
+-- > IntMod : Nat -> sort 0;
+scIntModType :: SharedContext -> Term -> IO Term
+scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
+
+
 -- Primitive operations on bitvectors
 
 -- | Create a term computing the type of a length-n bitvector.

From 5a5d4302a84f77353ceb07921d0f253f2215dc8b Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 14:14:34 -0700
Subject: [PATCH 05/12] Add function `asIntModType` to Recognizer library.

---
 saw-core/src/Verifier/SAW/Recognizer.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs
index 9543721a..8190f949 100644
--- a/saw-core/src/Verifier/SAW/Recognizer.hs
+++ b/saw-core/src/Verifier/SAW/Recognizer.hs
@@ -59,6 +59,7 @@ module Verifier.SAW.Recognizer
   , asBool
   , asBoolType
   , asIntegerType
+  , asIntModType
   , asBitvectorType
   , asVectorType
   , asVecType
@@ -343,6 +344,9 @@ asBoolType = isGlobalDef "Prelude.Bool"
 asIntegerType :: Recognizer Term ()
 asIntegerType = isGlobalDef "Prelude.Integer"
 
+asIntModType :: Recognizer Term Natural
+asIntModType = isGlobalDef "Prelude.IntMod" @> asNat
+
 asVectorType :: Recognizer Term (Term, Term)
 asVectorType = helper ((isGlobalDef "Prelude.Vec" @> return) <@> return) where
   helper r t =

From 8a80a19803ec2cbfbed4829ed1c3371e79ed9505 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 14:16:13 -0700
Subject: [PATCH 06/12] Add constructor `FOTIntMod` to `FirstOrderType`
 datatype.

Quantified variables of type `IntMod n` should work again in
the what4/sbv backends.
---
 cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs    |  1 +
 saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs    |  4 ++++
 .../src/Verifier/SAW/Simulator/What4.hs           | 15 +++++++++++++++
 .../Verifier/SAW/Simulator/What4/FirstOrder.hs    |  4 +++-
 saw-core/src/Verifier/SAW/FiniteValue.hs          |  4 ++++
 5 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index 4a92aee2..276244e6 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -96,6 +96,7 @@ cryptolTypeOfFirstOrderType fot =
   case fot of
     FOTBit -> C.tBit
     FOTInt -> C.tInteger
+    FOTIntMod n -> C.tIntMod (C.tNum n)
     FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t)
     FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts)
     FOTArray a b ->
diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index b53ca245..6e72b639 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -635,6 +635,8 @@ vAsFirstOrderType v =
       -> return FOTBit
     VIntType
       -> return FOTInt
+    VIntModType n
+      -> return (FOTIntMod n)
     VVecType n v2
       -> FOTVec n <$> vAsFirstOrderType v2
     VUnitType
@@ -706,6 +708,7 @@ newVarsForType v nm =
 newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue)
 newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s)
 newVars FOTInt = nextId <&> \s-> (IntegerLabel s, vInteger <$> existsSInteger s)
+newVars (FOTIntMod n) = nextId <&> \s-> (IntegerLabel s, VIntMod n <$> existsSInteger s)
 newVars (FOTVec n FOTBit) =
   if n == 0
     then nextId <&> \s-> (WordLabel s, return (vWord (literalSWord 0 0)))
@@ -727,6 +730,7 @@ newVars (FOTRec tm) = do
 newCodeGenVars :: (Natural -> Bool) -> FirstOrderType -> StateT Int IO (SBVCodeGen SValue)
 newCodeGenVars _checkSz FOTBit = nextId <&> \s -> (vBool <$> svCgInput KBool s)
 newCodeGenVars _checkSz FOTInt = nextId <&> \s -> (vInteger <$> svCgInput KUnbounded s)
+newCodeGenVars _checkSz (FOTIntMod _) = nextId <&> \s -> (vInteger <$> svCgInput KUnbounded s)
 newCodeGenVars checkSz (FOTVec n FOTBit)
   | n == 0    = nextId <&> \_ -> return (vWord (literalSWord 0 0))
   | checkSz n = nextId <&> \s -> vWord <$> cgInputSWord s (fromIntegral n)
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index ef9d6c68..f50ef4d8 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -905,6 +905,8 @@ vAsFirstOrderType v =
       -> return FOTBit
     VIntType
       -> return FOTInt
+    VIntModType n
+      -> return (FOTIntMod n)
     VVecType n v2
       -> FOTVec n <$> vAsFirstOrderType v2
     VArrayType iv ev
@@ -934,6 +936,12 @@ data TypedExpr sym where
   TypedExpr :: BaseTypeRepr ty -> SymExpr sym ty -> TypedExpr sym
 
 
+mkSymbol :: String -> IO W.SolverSymbol
+mkSymbol str =
+  case W.userSymbol str of
+    Right solverSymbol -> pure solverSymbol
+    Left _ -> fail $ "Cannot create solver symbol " ++ str
+
 -- | Generate a new variable from a given BaseType
 
 freshVar :: forall sym ty. (IsSymExprBuilder sym, Given sym) =>
@@ -993,6 +1001,13 @@ newVarFOT (FOTRec tm)
        args <- traverse (return . ready) (vals :: (Map String (SValue sym)))
        return (RecLabel labels, vRecord args)
 
+newVarFOT (FOTIntMod n)
+  = do nm <- nextId
+       let r = BaseIntegerRepr
+       nm' <- lift $ mkSymbol nm
+       si <- lift $ W.freshConstant (given :: sym) nm' r
+       return (BaseLabel (TypedExpr r si), VIntMod n si)
+
 newVarFOT fot
   | Some r <- fotToBaseType fot
   = do nm <- nextId
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs
index 1d62689a..a7273611 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs
@@ -48,6 +48,8 @@ fotToBaseType FOTBit
   = Some BaseBoolRepr
 fotToBaseType FOTInt
   = Some BaseIntegerRepr
+fotToBaseType (FOTIntMod _n)
+  = Some BaseIntegerRepr
 fotToBaseType (FOTVec nat FOTBit)
   | Just (Some (PosNat nr)) <- somePosNat nat
   = Some (BaseBVRepr nr)
@@ -124,4 +126,4 @@ tupleToList (viewAssign -> AssignExtend rs r) (viewAssign -> AssignExtend gvs gv
   (:) <$> groundToFOV r (unGVW gv) <*> tupleToList rs gvs
 #if !MIN_VERSION_GLASGOW_HASKELL(8,10,0,0)
 tupleToList _ _ = error "GADTs should rule this out."
-#endif
\ No newline at end of file
+#endif
diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs
index 4f249d9c..bfeca088 100644
--- a/saw-core/src/Verifier/SAW/FiniteValue.hs
+++ b/saw-core/src/Verifier/SAW/FiniteValue.hs
@@ -48,6 +48,7 @@ data FiniteValue
 data FirstOrderType
   = FOTBit
   | FOTInt
+  | FOTIntMod Natural
   | FOTVec Natural FirstOrderType
   | FOTArray FirstOrderType FirstOrderType
   | FOTTuple [FirstOrderType]
@@ -201,6 +202,8 @@ asFirstOrderType sc t = do
       -> return FOTBit
     (R.asIntegerType -> Just ())
       -> return FOTInt
+    (R.asIntModType -> Just n)
+      -> return (FOTIntMod n)
     (R.isVecType return -> Just (n R.:*: tp))
       -> FOTVec n <$> asFirstOrderType sc tp
     (R.asArrayType -> Just (tp1 R.:*: tp2)) -> do
@@ -237,6 +240,7 @@ scFirstOrderType sc ft =
   case ft of
     FOTBit      -> scBoolType sc
     FOTInt      -> scIntegerType sc
+    FOTIntMod n -> scIntModType sc =<< scNat sc n
     FOTVec n t  -> do n' <- scNat sc n
                       t' <- scFirstOrderType sc t
                       scVecType sc n' t'

From f01e44490259faa15193f5dcbfdb14f158338a2e Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 15:36:41 -0700
Subject: [PATCH 07/12] Correctly handle uninterpreted functions on IntMod in
 sbv/what4 backends.

When we generate an uninterpreted function in a symbolic backend that
takes an argument of type `IntMod n`, we normalize the symbolic integer
argument by reducing mod n. This ensures that the resulting expression
will respect the underlying equivalence relation for the `IntMod n` type.
---
 .../src/Verifier/SAW/Simulator/SBV.hs         |  5 ++++
 .../src/Verifier/SAW/Simulator/What4.hs       | 25 +++++++++++++------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index 6e72b639..2c7943f9 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -261,6 +261,8 @@ flattenSValue v = do
                                         return (concat xss, concat ss)
         VBool sb                  -> return ([sb], "")
         VInt si                   -> return ([si], "")
+        VIntMod 0 si              -> return ([si], "")
+        VIntMod n si              -> return ([svRem si (svInteger KUnbounded (toInteger n))], "")
         VWord sw                  -> return (if intSizeOf sw > 0 then [sw] else [], "")
         VCtorApp i (V.toList->ts) -> do (xss, ss) <- unzip <$> traverse (force >=> flattenSValue) ts
                                         return (concat xss, "_" ++ identName i ++ concat ss)
@@ -589,6 +591,9 @@ parseUninterpreted cws nm ty =
     VIntType
       -> return $ vInteger $ mkUninterpreted KUnbounded cws nm
 
+    VIntModType n
+      -> return $ VIntMod n $ mkUninterpreted KUnbounded cws nm
+
     (VVecType n VBoolType)
       -> return $ vWord $ mkUninterpreted (KBounded False (fromIntegral n)) cws nm
 
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index f50ef4d8..af2aa53e 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -728,7 +728,7 @@ parseUninterpreted sym ref app ty =
     VPiType _ f
       -> return $
          strictFun $ \x -> do
-           app' <- applyUnintApp app x
+           app' <- applyUnintApp sym app x
            t2 <- f (ready x)
            parseUninterpreted sym ref app' t2
 
@@ -738,6 +738,9 @@ parseUninterpreted sym ref app ty =
     VIntType
       -> VInt  <$> mkUninterpreted sym ref app BaseIntegerRepr
 
+    VIntModType n
+      -> VIntMod n <$> mkUninterpreted sym ref app BaseIntegerRepr
+
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
@@ -812,23 +815,29 @@ extendUnintApp (UnintApp nm xs tys) x ty =
 -- encode them as suffixes on the function name of the 'UnintApp'.
 applyUnintApp ::
   forall sym.
+  (W.IsExprBuilder sym) =>
+  sym ->
   UnintApp (SymExpr sym) ->
   SValue sym ->
   IO (UnintApp (SymExpr sym))
-applyUnintApp app0 v =
+applyUnintApp sym app0 v =
   case v of
     VUnit                     -> return app0
-    VPair x y                 -> do app1 <- applyUnintApp app0 =<< force x
-                                    app2 <- applyUnintApp app1 =<< force y
+    VPair x y                 -> do app1 <- applyUnintApp sym app0 =<< force x
+                                    app2 <- applyUnintApp sym app1 =<< force y
                                     return app2
-    VRecordValue elems        -> foldM applyUnintApp app0 =<< traverse (force . snd) elems
-    VVector xv                -> foldM applyUnintApp app0 =<< traverse force xv
+    VRecordValue elems        -> foldM (applyUnintApp sym) app0 =<< traverse (force . snd) elems
+    VVector xv                -> foldM (applyUnintApp sym) app0 =<< traverse force xv
     VBool sb                  -> return (extendUnintApp app0 sb BaseBoolRepr)
     VInt si                   -> return (extendUnintApp app0 si BaseIntegerRepr)
+    VIntMod 0 si              -> return (extendUnintApp app0 si BaseIntegerRepr)
+    VIntMod n si              -> do n' <- W.intLit sym (toInteger n)
+                                    si' <- W.intMod sym si n'
+                                    return (extendUnintApp app0 si' BaseIntegerRepr)
     VWord (DBV sw)            -> return (extendUnintApp app0 sw (W.exprType sw))
     VArray (SArray sa)        -> return (extendUnintApp app0 sa (W.exprType sa))
     VWord ZBV                 -> return app0
-    VCtorApp i xv             -> foldM applyUnintApp app' =<< traverse force xv
+    VCtorApp i xv             -> foldM (applyUnintApp sym) app' =<< traverse force xv
                                    where app' = suffixUnintApp ("_" ++ identName i) app0
     VNat n                    -> return (suffixUnintApp ("_" ++ show n) app0)
     TValue (suffixTValue -> Just s)
@@ -1114,7 +1123,7 @@ parseUninterpretedSAW sym sc ref trm app ty =
     VPiType t1 f
       -> return $
          strictFun $ \x -> do
-           app' <- applyUnintApp app x
+           app' <- applyUnintApp sym app x
            arg <- mkArgTerm sc t1 x
            let trm' = ArgTermApply trm arg
            t2 <- f (ready x)

From 80c40b5f99e0f6d65311d8d0706eb1f3d2c80d3a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Oct 2020 15:50:18 -0700
Subject: [PATCH 08/12] Remove duplicated code.

---
 .../src/Verifier/SAW/Simulator/What4.hs       | 25 +++++++++----------
 1 file changed, 12 insertions(+), 13 deletions(-)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index af2aa53e..a3f2d88d 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -945,23 +945,23 @@ data TypedExpr sym where
   TypedExpr :: BaseTypeRepr ty -> SymExpr sym ty -> TypedExpr sym
 
 
-mkSymbol :: String -> IO W.SolverSymbol
-mkSymbol str =
-  case W.userSymbol str of
-    Right solverSymbol -> pure solverSymbol
-    Left _ -> fail $ "Cannot create solver symbol " ++ str
+-- | Create a fresh constant with the given name and type.
+mkConstant ::
+  forall sym ty.
+  (IsSymExprBuilder sym) =>
+  sym -> String -> BaseTypeRepr ty -> IO (SymExpr sym ty)
+mkConstant sym name ty =
+  case W.userSymbol name of
+    Right solverSymbol -> W.freshConstant sym solverSymbol ty
+    Left _ -> fail $ "Cannot create solver symbol " ++ name
 
 -- | Generate a new variable from a given BaseType
 
 freshVar :: forall sym ty. (IsSymExprBuilder sym, Given sym) =>
   BaseTypeRepr ty -> String -> IO (TypedExpr sym)
 freshVar ty str =
-  case W.userSymbol str of
-    Right solverSymbol -> do
-      c <- W.freshConstant (given :: sym) solverSymbol ty
-      return (TypedExpr ty c)
-    Left _ ->
-      fail $ "Cannot create solver symbol " ++ str
+  do c <- mkConstant (given :: sym) str ty
+     return (TypedExpr ty c)
 
 nextId :: StateT Int IO String
 nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s))
@@ -1013,8 +1013,7 @@ newVarFOT (FOTRec tm)
 newVarFOT (FOTIntMod n)
   = do nm <- nextId
        let r = BaseIntegerRepr
-       nm' <- lift $ mkSymbol nm
-       si <- lift $ W.freshConstant (given :: sym) nm' r
+       si <- lift $ mkConstant (given :: sym) nm r
        return (BaseLabel (TypedExpr r si), VIntMod n si)
 
 newVarFOT fot

From e2f714d8a415dd5ec7c3e5bf0fa6b3511f4f925a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 22 Oct 2020 05:41:25 -0700
Subject: [PATCH 09/12] Add function `scToIntMod` to SharedTerm library.

---
 saw-core/src/Verifier/SAW/SharedTerm.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index 7d6ab1f8..b8b0ae12 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -172,6 +172,7 @@ module Verifier.SAW.SharedTerm
   , scIntToBv, scBvToInt, scSbvToInt
     -- *** IntMod
   , scIntModType
+  , scToIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1709,6 +1710,12 @@ scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x]
 scIntModType :: SharedContext -> Term -> IO Term
 scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 
+-- | Convert an integer to an integer mod n.
+--
+-- > toIntMod : (n : Nat) -> Integer -> IntMod n;
+scToIntMod :: SharedContext -> Term -> Term -> IO Term
+scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors
 

From 363437fc46165382d88fde46adec561b1df5f9f4 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 2 Nov 2020 18:51:17 -0800
Subject: [PATCH 10/12] Add `FOVIntMod` constructor to `FirstOrderValue`
 datatype.

---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs |  1 +
 saw-core/src/Verifier/SAW/FiniteValue.hs     | 11 +++++++++++
 2 files changed, 12 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 16735b1b..ca7c216e 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1534,6 +1534,7 @@ exportFirstOrderValue fv =
   case fv of
     FOVBit b    -> V.VBit b
     FOVInt i    -> V.VInteger i
+    FOVIntMod _ i -> V.VInteger i
     FOVWord w x -> V.word V.Concrete (toInteger w) x
     FOVVec t vs
       | t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap V.Concrete . map (V.ready . V.VBit . fvAsBool) $ vs)))
diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs
index bfeca088..292f9069 100644
--- a/saw-core/src/Verifier/SAW/FiniteValue.hs
+++ b/saw-core/src/Verifier/SAW/FiniteValue.hs
@@ -59,6 +59,7 @@ data FirstOrderType
 data FirstOrderValue
   = FOVBit Bool
   | FOVInt Integer
+  | FOVIntMod Natural Integer
   | FOVWord Natural Integer -- ^ a more efficient special case for 'FOVVec FOTBit _'.
   | FOVVec FirstOrderType [FirstOrderValue]
   | FOVArray FirstOrderType FirstOrderType
@@ -91,6 +92,7 @@ instance Show FirstOrderValue where
     case fv of
       FOVBit b    -> shows b
       FOVInt i    -> shows i
+      FOVIntMod _ i -> shows i
       FOVWord _ x -> shows x
       FOVVec _ vs -> showString "[" . commaSep (map shows vs) . showString "]"
       FOVArray{}  -> shows $ firstOrderTypeOf fv
@@ -111,6 +113,7 @@ ppFirstOrderValue opts = loop
      | b         -> text "True"
      | otherwise -> text "False"
    FOVInt i      -> integer i
+   FOVIntMod _ i -> integer i
    FOVWord _w i  -> ppNat opts i
    FOVVec _ xs   -> brackets (sep (punctuate comma (map loop xs)))
    FOVArray{}    -> text $ show $ firstOrderTypeOf fv
@@ -161,6 +164,7 @@ firstOrderTypeOf fv =
   case fv of
     FOVBit _    -> FOTBit
     FOVInt _    -> FOTInt
+    FOVIntMod n _ -> FOTIntMod n
     FOVWord n _ -> FOTVec n FOTBit
     FOVVec t vs -> FOTVec (fromIntegral (length vs)) t
     -- Note: FOVArray contains type information, but not an actual Array value,
@@ -263,6 +267,13 @@ scFirstOrderValue sc fv =
     FOVInt i
       | i >= 0  -> scNatToInt sc =<< scNat sc (fromInteger i)
       | True    -> scIntNeg sc =<< scNatToInt sc =<< scNat sc (fromInteger (- i))
+    FOVIntMod 0 i ->
+      do n' <- scNat sc 0
+         scToIntMod sc n' =<< scFirstOrderValue sc (FOVInt i)
+    FOVIntMod n i ->
+      do n' <- scNat sc n
+         i' <- scNatToInt sc =<< scNat sc (fromInteger (i `mod` toInteger n))
+         scToIntMod sc n' i'
     FOVWord n x -> scBvConst sc n x
     FOVVec t vs -> do t' <- scFirstOrderType sc t
                       vs' <- traverse (scFirstOrderValue sc) vs

From 7b6167e22dd31489614c62e6bca35b1d19473686 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 2 Nov 2020 18:56:47 -0800
Subject: [PATCH 11/12] saw-core-what4: Add IntModLabel to Labeler type.

Also add `getLabelValues` function from saw-script to saw-core-what4.
---
 .../src/Verifier/SAW/Simulator/What4.hs       | 37 ++++++++++++++++---
 1 file changed, 31 insertions(+), 6 deletions(-)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index a3f2d88d..d35eeba3 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -49,6 +49,7 @@ module Verifier.SAW.Simulator.What4
   , w4Eval
   , w4EvalAny
   , w4EvalBasic
+  , getLabelValues
   ) where
 
 
@@ -80,9 +81,11 @@ import qualified Verifier.SAW.Simulator.Prims as Prims
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Simulator.Value
 import Verifier.SAW.TypedAST (FieldName, ModuleMap, identName)
-import Verifier.SAW.FiniteValue (FirstOrderType(..))
+import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..))
 
 -- what4
+import qualified What4.Expr.Builder as B
+import           What4.Expr.GroundEval
 import           What4.Interface(SymExpr,Pred,SymInteger, IsExpr,
                                  IsExprBuilder,IsSymExprBuilder)
 import qualified What4.Interface as W
@@ -985,10 +988,11 @@ myfun ::(Map String (Labeler sym, SValue sym)) -> (Map String (Labeler sym), Map
 myfun = fmap fst A.&&& fmap snd
 
 data Labeler sym
-   = BaseLabel  (TypedExpr sym)
-   | VecLabel   (Vector (Labeler sym))
-   | TupleLabel (Vector (Labeler sym))
-   | RecLabel   (Map FieldName (Labeler sym))
+  = BaseLabel (TypedExpr sym)
+  | IntModLabel Natural (SymInteger sym)
+  | VecLabel (Vector (Labeler sym))
+  | TupleLabel (Vector (Labeler sym))
+  | RecLabel (Map FieldName (Labeler sym))
 
 
 newVarFOT :: forall sym. (IsSymExprBuilder sym, Given sym) =>
@@ -1014,7 +1018,7 @@ newVarFOT (FOTIntMod n)
   = do nm <- nextId
        let r = BaseIntegerRepr
        si <- lift $ mkConstant (given :: sym) nm r
-       return (BaseLabel (TypedExpr r si), VIntMod n si)
+       return (IntModLabel n si, VIntMod n si)
 
 newVarFOT fot
   | Some r <- fotToBaseType fot
@@ -1029,6 +1033,27 @@ typedToSValue :: (IsExpr (SymExpr sym)) => TypedExpr sym -> IO (SValue sym)
 typedToSValue (TypedExpr ty expr) =
   maybe (fail "Cannot handle") return $ symExprToValue ty expr
 
+getLabelValues ::
+  forall sym t.
+  (SymExpr sym ~ B.Expr t) =>
+  GroundEvalFn t -> Labeler sym -> IO FirstOrderValue
+getLabelValues f =
+  \case
+    TupleLabel labels ->
+      FOVTuple <$> traverse (getLabelValues f) (V.toList labels)
+    VecLabel labels ->
+      FOVVec vty <$> traverse (getLabelValues f) (V.toList labels)
+      where vty = error "TODO: compute vector type, or just store it"
+    RecLabel labels ->
+      FOVRec <$> traverse (getLabelValues f) labels
+    IntModLabel n x ->
+      FOVIntMod n <$> groundEval f x
+    BaseLabel (TypedExpr ty bv) ->
+      do gv <- groundEval f bv
+         case (groundToFOV ty gv) of
+           Left err  -> fail err
+           Right fov -> pure fov
+
 ----------------------------------------------------------------------
 -- Evaluation through crucible-saw backend
 

From 47f626443ccd21e01557f3dc179d1c07d6adf33e Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 3 Nov 2020 10:52:00 -0800
Subject: [PATCH 12/12] Use `safeSymbol` instead of `userSymbol` to avoid an
 error case.

---
 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index d35eeba3..b9759c3e 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -953,10 +953,7 @@ mkConstant ::
   forall sym ty.
   (IsSymExprBuilder sym) =>
   sym -> String -> BaseTypeRepr ty -> IO (SymExpr sym ty)
-mkConstant sym name ty =
-  case W.userSymbol name of
-    Right solverSymbol -> W.freshConstant sym solverSymbol ty
-    Left _ -> fail $ "Cannot create solver symbol " ++ name
+mkConstant sym name ty = W.freshConstant sym (W.safeSymbol name) ty
 
 -- | Generate a new variable from a given BaseType