From e3343b00c39e77fe8f4ec43fd1a6c69ae0d64d89 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 11 Feb 2022 16:56:30 -0800
Subject: [PATCH 01/22] added parse_core_mod command; made ensureMonadicTerm a
 bit smarter by making it normalize the input type before deciding if it is
 already computational

---
 src/SAWScript/Builtins.hs    | 27 ++++++++++++++++++++-------
 src/SAWScript/Interpreter.hs |  7 +++++++
 2 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index d9c2244a42..8ddfbbd47d 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1385,8 +1385,8 @@ tailPrim :: [a] -> TopLevel [a]
 tailPrim [] = fail "tail: empty list"
 tailPrim (_ : xs) = return xs
 
-parseCore :: String -> TopLevel Term
-parseCore input =
+parseCoreMod :: String -> String -> TopLevel Term
+parseCoreMod mnm_str input =
   do sc <- getSharedContext
      let base = "<interactive>"
          path = "<interactive>"
@@ -1397,18 +1397,29 @@ parseCore input =
            do let msg = show err
               printOutLnTop Opts.Error msg
               fail msg
-     let mnm = Just $ mkModuleName ["Cryptol"]
-     err_or_t <- io $ runTCM (typeInferComplete uterm) sc mnm []
+     let mnm =
+           mkModuleName $ Text.splitOn (Text.pack ".") $ Text.pack mnm_str
+     _ <- io $ scFindModule sc mnm -- Check that mnm exists
+     err_or_t <- io $ runTCM (typeInferComplete uterm) sc (Just mnm) []
      case err_or_t of
        Left err -> fail (show err)
        Right (TC.TypedTerm x _) -> return x
 
+parseCore :: String -> TopLevel Term
+parseCore = parseCoreMod "Cryptol"
+
 parse_core :: String -> TopLevel TypedTerm
 parse_core input = do
   t <- parseCore input
   sc <- getSharedContext
   io $ mkTypedTerm sc t
 
+parse_core_mod :: String -> String -> TopLevel TypedTerm
+parse_core_mod mnm input = do
+  t <- parseCoreMod mnm input
+  sc <- getSharedContext
+  io $ mkTypedTerm sc t
+
 prove_core :: ProofScript () -> String -> TopLevel Theorem
 prove_core script input =
   do sc <- getSharedContext
@@ -1532,9 +1543,11 @@ monadifyTypedTerm sc t =
 
 -- | Ensure that a 'TypedTerm' has been monadified
 ensureMonadicTerm :: SharedContext -> TypedTerm -> TopLevel TypedTerm
-ensureMonadicTerm _ t
-  | TypedTermOther tp <- ttType t
-  , Prover.isCompFunType tp = return t
+ensureMonadicTerm sc t
+  | TypedTermOther tp <- ttType t =
+    io (Prover.isCompFunType sc tp) >>= \case
+      True -> return t
+      False -> monadifyTypedTerm sc t
 ensureMonadicTerm sc t = monadifyTypedTerm sc t
 
 mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 7df26f6d31..48b53b4fdc 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2225,6 +2225,13 @@ primitives = Map.fromList
     [ "Parse a Term from a String in SAWCore syntax."
     ]
 
+  , prim "parse_core_mod"      "String -> String -> Term"
+    (funVal2 parse_core_mod)
+    Current
+    [ "Parse a Term from the second supplied String in SAWCore syntax,"
+    , "relative to the module specified by the first String"
+    ]
+
   , prim "prove_core"         "ProofScript () -> String -> TopLevel Theorem"
     (pureVal prove_core)
     Current

From 61e3b58e1a072c1e84bb8c49ee9586f057ec0761 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 11 Feb 2022 16:59:16 -0800
Subject: [PATCH 02/22] fixed mrFunOutType, isCompFunType, and askMRSolver to
 normalize types

---
 src/SAWScript/Prover/MRSolver.hs | 36 +++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index d29bfa0617..5e268aec85 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -671,13 +671,18 @@ mrConvertible = liftSC4 scConvertibleEval scTypeCheckWHNF True
 -- compute the type @CompM [args/vars]a@ of @f@ applied to @args@. Return the
 -- type @[args/vars]a@ that @CompM@ is applied to.
 mrFunOutType :: FunName -> [Term] -> MRM Term
-mrFunOutType ((asPiList . funNameType) -> (vars, asCompM -> Just tp)) args
-  | length vars == length args =
-    substTermLike 0 args tp
-mrFunOutType _ _ =
-  -- NOTE: this is an error because we should only ever call mrFunOutType with a
-  -- well-formed application at a CompM type
-  error "mrFunOutType"
+mrFunOutType fname args =
+  liftSC1 scWhnf (funNameType fname) >>= \case
+  (asPiList -> (vars, asCompM -> Just tp))
+    | length vars == length args -> substTermLike 0 args tp
+  ftype@(asPiList -> (vars, _)) ->
+    do pp_ftype <- mrPPInCtx ftype
+       pp_fname <- mrPPInCtx fname
+       debugPrint 0 "mrFunOutType: function applied to the wrong number of args"
+       debugPrint 0 ("Expected: " ++ show (length vars) ++
+                     ", found: " ++ show (length args))
+       debugPretty 0 ("For function: " <> pp_fname <> " with type: " <> pp_ftype)
+       error"mrFunOutType"
 
 -- | Turn a 'LocalName' into one not in a list, adding a suffix if necessary
 uniquifyName :: LocalName -> [LocalName] -> LocalName
@@ -984,8 +989,8 @@ _debugPrettyInCtx i a =
   (mrUVars <$> get) >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
 
 -- | Pretty-print an object relative to the current context
-_mrPPInCtx :: PrettyInCtx a => a -> MRM SawDoc
-_mrPPInCtx a =
+mrPPInCtx :: PrettyInCtx a => a -> MRM SawDoc
+mrPPInCtx a =
   runReader (prettyInCtx a) <$> map fst <$> mrUVars <$> get
 
 -- | Pretty-print the result of 'ppWithPrefixSep' relative to the current uvar
@@ -1121,10 +1126,11 @@ asCompM (asApp -> Just (isGlobalDef "Prelude.CompM" -> Just (), tp)) =
   return tp
 asCompM _ = fail "not a CompM type!"
 
--- | Test if a type is a monadic function type of 0 or more arguments
-isCompFunType :: Term -> Bool
-isCompFunType (asPiList -> (_, asCompM -> Just _)) = True
-isCompFunType _ = False
+-- | Test if a type normalizes to a monadic function type of 0 or more arguments
+isCompFunType :: SharedContext -> Term -> IO Bool
+isCompFunType sc t = scWhnf sc t >>= \case
+  (asPiList -> (_, asCompM -> Just _)) -> return True
+  _ -> return False
 
 -- | Pattern-match on a @LetRecTypes@ list in normal form and return a list of
 -- the types it specifies, each in normal form and with uvars abstracted out
@@ -1531,8 +1537,8 @@ askMRSolver ::
   Term -> Term -> IO (Maybe MRFailure)
 
 askMRSolver sc dlvl smt_conf timeout t1 t2 =
-  do tp1 <- scTypeOf sc t1
-     tp2 <- scTypeOf sc t2
+  do tp1 <- scTypeOf sc t1 >>= scWhnf sc
+     tp2 <- scTypeOf sc t2 >>= scWhnf sc
      init_st <- mkMRState sc Map.empty smt_conf timeout dlvl
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->

From 9655e0fa8f481e9fea58800324e3b304c11d7534 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 14 Feb 2022 11:55:28 -0800
Subject: [PATCH 03/22] expanded the notion of a "function name" for MR Solver
 to include not just globals but also (tuple and record) projections of
 globals

---
 src/SAWScript/Prover/MRSolver.hs | 82 ++++++++++++++++++++++++++------
 1 file changed, 67 insertions(+), 15 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 5e268aec85..0c888e8589 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -193,18 +193,61 @@ newtype MRVar = MRVar { unMRVar :: ExtCns Term } deriving (Eq, Show, Ord)
 mrVarType :: MRVar -> Term
 mrVarType = ecType . unMRVar
 
+-- | A tuple or record projection of a 'Term'
+data TermProj = TermProjLeft | TermProjRight | TermProjRecord FieldName
+              deriving (Eq, Ord, Show)
+
+-- | Apply a 'TermProj' to perform a projection on a 'Term'
+doTermProj :: Term -> TermProj -> MRM Term
+doTermProj t TermProjLeft = liftSC1 scPairLeft t
+doTermProj t TermProjRight = liftSC1 scPairRight t
+doTermProj t (TermProjRecord fld) = liftSC2 scRecordSelect t fld
+
+-- | Apply a 'TermProj' to a type to get the output type of the projection,
+-- assuming that the type is already normalized
+doTypeProj :: Term -> TermProj -> MRM Term
+doTypeProj (asPairType -> Just (tp1, _)) TermProjLeft = return tp1
+doTypeProj (asPairType -> Just (_, tp2)) TermProjRight = return tp2
+doTypeProj (asRecordType -> Just tp_map) (TermProjRecord fld)
+  | Just tp <- Map.lookup fld tp_map
+  = return tp
+doTypeProj _ _ =
+  -- FIXME: better error message? This is an error and not an MRFailure because
+  -- we should only be projecting types for terms that we have already seen...
+  error "doTypeProj"
+
 -- | Names of functions to be used in computations, which are either names bound
 -- by letrec to for recursive calls to fixed-points, existential variables, or
--- global named constants
+-- (possibly projections of) of global named constants
 data FunName
-  = LetRecName MRVar | EVarFunName MRVar | GlobalName GlobalDef
+  = LetRecName MRVar | EVarFunName MRVar | GlobalName GlobalDef [TermProj]
   deriving (Eq, Ord, Show)
 
--- | Get the type of a 'FunName'
-funNameType :: FunName -> Term
-funNameType (LetRecName var) = mrVarType var
-funNameType (EVarFunName var) = mrVarType var
-funNameType (GlobalName gd) = globalDefType gd
+-- | Get and normalize the type of a 'FunName'
+funNameType :: FunName -> MRM Term
+funNameType (LetRecName var) = liftSC1 scWhnf $ mrVarType var
+funNameType (EVarFunName var) = liftSC1 scWhnf $ mrVarType var
+funNameType (GlobalName gd projs) =
+  liftSC1 scWhnf (globalDefType gd) >>= \gd_tp ->
+  foldM doTypeProj gd_tp projs
+
+-- | Recognize a 'Term' as (possibly a projection of) a global name
+asTypedGlobalProj :: Recognizer Term (GlobalDef, [TermProj])
+asTypedGlobalProj (asRecordSelector ->
+                   Just ((asTypedGlobalProj -> Just (d, projs)), fld)) =
+  return (d, TermProjRecord fld:projs)
+asTypedGlobalProj (asPairSelector ->
+                   Just ((asTypedGlobalProj -> Just (d, projs)), isRight))
+  | isRight = return (d, TermProjRight:projs)
+  | not isRight = return (d, TermProjLeft:projs)
+asTypedGlobalProj (asTypedGlobalDef -> Just glob) = Just (glob, [])
+asTypedGlobalProj _ = Nothing
+
+-- | Recognize a 'Term' as (possibly a projection of) a global name
+asGlobalFunName :: Recognizer Term FunName
+asGlobalFunName (asTypedGlobalProj -> Just (glob, projs)) =
+  Just $ GlobalName glob projs
+asGlobalFunName _ = Nothing
 
 -- | A term specifically known to be of type @sort i@ for some @i@
 newtype Type = Type Term deriving Show
@@ -287,10 +330,16 @@ instance PrettyInCtx Type where
 instance PrettyInCtx MRVar where
   prettyInCtx (MRVar ec) = return $ ppName $ ecName ec
 
+instance PrettyInCtx TermProj where
+  prettyInCtx TermProjLeft = return (pretty '.' <> "1")
+  prettyInCtx TermProjRight = return (pretty '.' <> "2")
+  prettyInCtx (TermProjRecord fld) = return (pretty '.' <> pretty fld)
+
 instance PrettyInCtx FunName where
   prettyInCtx (LetRecName var) = prettyInCtx var
   prettyInCtx (EVarFunName var) = prettyInCtx var
-  prettyInCtx (GlobalName i) = return $ viaShow i
+  prettyInCtx (GlobalName g projs) =
+    foldM (\pp proj -> (pp <>) <$> prettyInCtx proj) (viaShow g) projs
 
 instance PrettyInCtx Comp where
   prettyInCtx (CompTerm t) = prettyInCtx t
@@ -672,7 +721,7 @@ mrConvertible = liftSC4 scConvertibleEval scTypeCheckWHNF True
 -- type @[args/vars]a@ that @CompM@ is applied to.
 mrFunOutType :: FunName -> [Term] -> MRM Term
 mrFunOutType fname args =
-  liftSC1 scWhnf (funNameType fname) >>= \case
+  funNameType fname >>= \case
   (asPiList -> (vars, asCompM -> Just tp))
     | length vars == length args -> substTermLike 0 args tp
   ftype@(asPiList -> (vars, _)) ->
@@ -760,7 +809,7 @@ extCnsToFunName ec = let var = MRVar ec in mrVarInfo var >>= \case
   Just (FunVarInfo _) -> return $ LetRecName var
   Nothing
     | Just glob <- asTypedGlobalDef (Unshared $ FTermF $ ExtCns ec) ->
-      return $ GlobalName glob
+      return $ GlobalName glob []
   _ -> error "extCnsToFunName: unreachable"
 
 -- | Get the body of a function @f@ if it has one
@@ -769,7 +818,10 @@ mrFunNameBody (LetRecName var) =
   mrVarInfo var >>= \case
   Just (FunVarInfo body) -> return $ Just body
   _ -> error "mrFunBody: unknown letrec var"
-mrFunNameBody (GlobalName glob) = return $ globalDefBody glob
+mrFunNameBody (GlobalName glob projs)
+  | Just body <- globalDefBody glob
+  = Just <$> foldM doTermProj body projs
+mrFunNameBody (GlobalName _ _) = return Nothing
 mrFunNameBody (EVarFunName _) = return Nothing
 
 -- | Get the body of a function @f@ applied to some arguments, if possible
@@ -798,9 +850,9 @@ mrCallsFun f = memoFixTermFun $ \recurse t -> case t of
          _ | f == g -> return True
          Just body -> recurse body
          Nothing -> return False
-  (asTypedGlobalDef -> Just gdef) ->
+  (asTypedGlobalProj -> Just (gdef, projs)) ->
     case globalDefBody gdef of
-      _ | f == GlobalName gdef -> return True
+      _ | f == GlobalName gdef projs -> return True
       Just body -> recurse body
       Nothing -> return False
   (unwrapTermF -> tf) ->
@@ -1226,8 +1278,8 @@ normComp (CompTerm t) =
       do fun_name <- extCnsToFunName ec
          return $ FunBind fun_name args CompFunReturn
 
-    ((asTypedGlobalDef -> Just gdef), args) ->
-      return $ FunBind (GlobalName gdef) args CompFunReturn
+    ((asGlobalFunName -> Just f), args) ->
+      return $ FunBind f args CompFunReturn
 
     _ -> throwError (MalformedComp t)
 

From be6beea5d0f2f8d98b6944cc1aa22bf4e9201710 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 14 Feb 2022 15:56:24 -0800
Subject: [PATCH 04/22] added support for recognizing multiFixM computations to
 normComp

---
 src/SAWScript/Prover/MRSolver.hs | 103 ++++++++++++++++++++++---------
 1 file changed, 73 insertions(+), 30 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 0c888e8589..3d826c72c7 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -216,6 +216,15 @@ doTypeProj _ _ =
   -- we should only be projecting types for terms that we have already seen...
   error "doTypeProj"
 
+-- | Recognize a 'Term' as 0 or more projections
+asProjAll :: Term -> (Term, [TermProj])
+asProjAll (asRecordSelector -> Just ((asProjAll -> (t, projs)), fld)) =
+  (t, TermProjRecord fld:projs)
+asProjAll (asPairSelector -> Just ((asProjAll -> (t, projs)), isRight))
+  | isRight = (t, TermProjRight:projs)
+  | not isRight = (t, TermProjLeft:projs)
+asProjAll t = (t, [])
+
 -- | Names of functions to be used in computations, which are either names bound
 -- by letrec to for recursive calls to fixed-points, existential variables, or
 -- (possibly projections of) of global named constants
@@ -233,14 +242,8 @@ funNameType (GlobalName gd projs) =
 
 -- | Recognize a 'Term' as (possibly a projection of) a global name
 asTypedGlobalProj :: Recognizer Term (GlobalDef, [TermProj])
-asTypedGlobalProj (asRecordSelector ->
-                   Just ((asTypedGlobalProj -> Just (d, projs)), fld)) =
-  return (d, TermProjRecord fld:projs)
-asTypedGlobalProj (asPairSelector ->
-                   Just ((asTypedGlobalProj -> Just (d, projs)), isRight))
-  | isRight = return (d, TermProjRight:projs)
-  | not isRight = return (d, TermProjLeft:projs)
-asTypedGlobalProj (asTypedGlobalDef -> Just glob) = Just (glob, [])
+asTypedGlobalProj (asProjAll -> ((asTypedGlobalDef -> Just glob), projs)) =
+  Just (glob, projs)
 asTypedGlobalProj _ = Nothing
 
 -- | Recognize a 'Term' as (possibly a projection of) a global name
@@ -1202,6 +1205,48 @@ asNestedPairs (asPairValue -> Just (x, asNestedPairs -> Just xs)) = Just (x:xs)
 asNestedPairs (asFTermF -> Just UnitValue) = Just []
 asNestedPairs _ = Nothing
 
+-- | Syntactically project then @i@th element of the body of a lambda. That is,
+-- assuming the input 'Term' has the form
+--
+-- > \ (x1:T1) ... (xn:Tn) -> (e1, (e2, ... (en, ())))
+--
+-- return the bindings @x1:T1,...,xn:Tn@ and @ei@
+synProjFunBody :: Int -> Term -> Maybe ([(LocalName, Term)], Term)
+synProjFunBody i (asLambdaList -> (vars, asTupleValue -> Just es)) =
+  -- NOTE: we are doing 1-based indexing instead of 0-based, thus the -1
+  Just $ (vars, es !! (i-1))
+synProjFunBody _ _ = Nothing
+
+-- | Bind fresh function variables for a @letRecM@ or @multiFixM@ with the given
+-- @LetRecTypes@ and definitions for the function bodies as a lambda
+mrFreshLetRecVars :: Term -> Term -> MRM [Term]
+mrFreshLetRecVars lrts defs_f =
+  do
+    -- First, make fresh function constants for all the bound functions, using
+    -- the names bound by defs_f and just "F" if those run out
+    let fun_var_names =
+          map fst (fst $ asLambdaList defs_f) ++ repeat "F"
+    fun_tps <- asLRTList lrts
+    funs <- zipWithM mrFreshVar fun_var_names fun_tps
+    fun_tms <- mapM mrVarTerm funs
+
+    -- Next, apply the definition function defs_f to our function vars, yielding
+    -- the definitions of the individual letrec-bound functions in terms of the
+    -- new function constants
+    defs_tm <- mrApplyAll defs_f fun_tms
+    defs <- case asNestedPairs defs_tm of
+      Just defs -> return defs
+      Nothing -> throwError (MalformedDefsFun defs_f)
+
+    -- Remember the body associated with each fresh function constant
+    zipWithM_ (\f body ->
+                lambdaUVarsM body >>= \cl_body ->
+                mrSetVarInfo f (FunVarInfo cl_body)) funs defs
+
+    -- Finally, return the terms for the fresh function variables
+    return fun_tms
+
+
 -- | Normalize a 'Term' of monadic type to monadic normal form
 normCompTerm :: Term -> MRM NormComp
 normCompTerm = normComp . CompTerm
@@ -1236,28 +1281,9 @@ normComp (CompTerm t) =
       return $ ForallM (Type tp) (CompFunTerm body_tm)
     (isGlobalDef "Prelude.letRecM" -> Just (), [lrts, _, defs_f, body_f]) ->
       do
-        -- First, make fresh function constants for all the bound functions,
-        -- using the names bound by body_f and just "F" if those run out
-        let fun_var_names =
-              map fst (fst $ asLambdaList body_f) ++ repeat "F"
-        fun_tps <- asLRTList lrts
-        funs <- zipWithM mrFreshVar fun_var_names fun_tps
-        fun_tms <- mapM mrVarTerm funs
-
-        -- Next, apply the definition function defs_f to our function vars,
-        -- yielding the definitions of the individual letrec-bound functions in
-        -- terms of the new function constants
-        defs_tm <- mrApplyAll defs_f fun_tms
-        defs <- case asNestedPairs defs_tm of
-          Just defs -> return defs
-          Nothing -> throwError (MalformedDefsFun defs_f)
-
-        -- Remember the body associated with each fresh function constant
-        zipWithM_ (\f body ->
-                    lambdaUVarsM body >>= \cl_body ->
-                    mrSetVarInfo f (FunVarInfo cl_body)) funs defs
-
-        -- Finally, apply the body function to our function vars and recursively
+        -- Bind fresh function vars for the letrec-bound functions
+        fun_tms <- mrFreshLetRecVars lrts defs_f
+        -- Apply the body function to our function vars and recursively
         -- normalize the resulting computation
         body_tm <- mrApplyAll body_f fun_tms
         normComp (CompTerm body_tm)
@@ -1272,6 +1298,23 @@ normComp (CompTerm t) =
         mrApplyAll body args >>= normCompTerm
     -}
 
+    -- Recognize (multiFixM lrts (\ f1 ... fn -> (body1, ..., bodyn))).i args
+    (asTupleSelector ->
+     Just (asApplyAll -> (isGlobalDef "Prelude.multiFixM" -> Just (),
+                          [lrts, defs_f]),
+           i), args)
+      -- Extract out the function \f1 ... fn -> bodyi
+      | Just (vars, body_i) <- synProjFunBody i defs_f ->
+        do
+          -- Bind fresh function variables for the functions f1 ... fn
+          fun_tms <- mrFreshLetRecVars lrts defs_f
+          -- Re-abstract the body
+          body_f <- liftSC2 scLambdaList vars body_i
+          -- Apply body_f to f1 ... fn and the top-level arguments
+          body_tm <- mrApplyAll body_f (fun_tms ++ args)
+          normComp (CompTerm body_tm)
+
+
     -- For an ExtCns, we have to check what sort of variable it is
     -- FIXME: substitute for evars if they have been instantiated
     ((asExtCns -> Just ec), args) ->

From 80084759917cc116ef2cd36dd4c86b6d34de64a0 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 15 Feb 2022 06:43:54 -0800
Subject: [PATCH 05/22] fixed a bug in withUVars; added some debugging around
 calling into an SMT solver

---
 src/SAWScript/Prover/MRSolver.hs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 3d826c72c7..1be18ee8c2 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -146,7 +146,7 @@ import Verifier.SAW.SharedTerm
 import Verifier.SAW.Recognizer
 import Verifier.SAW.Cryptol.Monadify
 
-import SAWScript.Proof (termToProp)
+import SAWScript.Proof (termToProp, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
 
 
@@ -775,7 +775,7 @@ withUVars = helper [] where
   helper vars [] m = m $ reverse vars
   helper vars ((nm,tp):ctx) m =
     substTerm 0 vars tp >>= \tp' ->
-    withUVar nm (Type tp') $ \var -> helper (var:vars) ctx m
+    withUVarLift nm (Type tp') vars $ \var vars' -> helper (var:vars') ctx m
 
 -- | Build 'Term's for all the uvars currently in scope, ordered from least to
 -- most recently bound
@@ -1071,7 +1071,10 @@ mrProvableRaw prop_term =
   do smt_conf <- mrSMTConfig <$> get
      timeout <- mrSMTTimeout <$> get
      prop <- liftSC1 termToProp prop_term
+     debugPrint 2 ("Calling SMT solver with proposition: " ++
+                   prettyProp defaultPPOpts prop)
      (smt_res, _) <- liftSC4 SBV.proveUnintSBVIO smt_conf mempty timeout prop
+     debugPrint 2 "Finished calling SMT solver"
      case smt_res of
        Just _ -> return False
        Nothing -> return True
@@ -1083,7 +1086,8 @@ mrProvable bool_tm =
   do assumps <- mrAssumptions <$> get
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
      forall_prop <- piUVarsM prop
-     mrProvableRaw forall_prop
+     forall_prop' <- liftSC2 scGeneralizeExts (getAllExts forall_prop) forall_prop
+     mrProvableRaw forall_prop'
 
 -- | Build a Boolean 'Term' stating that two 'Term's are equal. This is like
 -- 'scEq' except that it works on open terms.

From 73d6468e7db95124637298b69cef40e32a848ac6 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 15 Feb 2022 11:01:28 -0800
Subject: [PATCH 06/22] changed mrProvable so now it instantiates all uvars
 with ExtCnss, so that we do not pass the SMT solver uvars that do not occur
 in the proposition we want to prove

---
 src/SAWScript/Prover/MRSolver.hs | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 1be18ee8c2..e6ba22701b 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -794,6 +794,13 @@ lambdaUVarsM t = mrUVarCtx >>= \ctx -> liftSC2 scLambdaList ctx t
 piUVarsM :: Term -> MRM Term
 piUVarsM t = mrUVarCtx >>= \ctx -> liftSC2 scPiList ctx t
 
+-- | Instantiate all uvars in a term with fresh 'ExtCns's
+instantiateUVarsM :: TermLike a => a -> MRM a
+instantiateUVarsM a =
+  do ctx <- mrUVarCtx
+     ecs <- mapM (\(nm,tp) -> liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns) ctx
+     substTermLike 0 ecs a
+
 -- | Convert an 'MRVar' to a 'Term', applying it to all the uvars in scope
 mrVarTerm :: MRVar -> MRM Term
 mrVarTerm (MRVar ec) =
@@ -1074,10 +1081,11 @@ mrProvableRaw prop_term =
      debugPrint 2 ("Calling SMT solver with proposition: " ++
                    prettyProp defaultPPOpts prop)
      (smt_res, _) <- liftSC4 SBV.proveUnintSBVIO smt_conf mempty timeout prop
-     debugPrint 2 "Finished calling SMT solver"
      case smt_res of
-       Just _ -> return False
-       Nothing -> return True
+       Just _ ->
+         debugPrint 2 "SMT solver response: not provable" >> return False
+       Nothing ->
+         debugPrint 2 "SMT solver response: provable" >> return True
 
 -- | Test if a Boolean term over the current uvars is provable given the current
 -- assumptions
@@ -1085,9 +1093,8 @@ mrProvable :: Term -> MRM Bool
 mrProvable bool_tm =
   do assumps <- mrAssumptions <$> get
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
-     forall_prop <- piUVarsM prop
-     forall_prop' <- liftSC2 scGeneralizeExts (getAllExts forall_prop) forall_prop
-     mrProvableRaw forall_prop'
+     forall_prop <- instantiateUVarsM prop
+     mrProvableRaw forall_prop
 
 -- | Build a Boolean 'Term' stating that two 'Term's are equal. This is like
 -- 'scEq' except that it works on open terms.

From 536dccad9b7c923d9e555af904e55291e7b13f00 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 15 Feb 2022 12:41:12 -0800
Subject: [PATCH 07/22] whoops, fixed instantiateUVarsM to reverse the list of
 uvars and substitute outer instantiations into the types of inner ones as it
 goes

---
 src/SAWScript/Prover/MRSolver.hs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index e6ba22701b..bc63f9dc7b 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -798,7 +798,17 @@ piUVarsM t = mrUVarCtx >>= \ctx -> liftSC2 scPiList ctx t
 instantiateUVarsM :: TermLike a => a -> MRM a
 instantiateUVarsM a =
   do ctx <- mrUVarCtx
-     ecs <- mapM (\(nm,tp) -> liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns) ctx
+     -- Remember: the uvar context is outermost to innermost, so we bind
+     -- variables from left to right, substituting earlier ones into the types
+     -- of later ones, but all substitutions are in reverse order, since
+     -- substTerm and friends like innermost bindings first
+     let helper :: [Term] -> [(LocalName,Term)] -> MRM [Term]
+         helper tms [] = return tms
+         helper tms ((nm,tp):vars) =
+           do tp' <- substTerm 0 tms tp
+              tm <- liftSC2 scFreshEC nm tp' >>= liftSC1 scExtCns
+              helper (tm:tms) vars
+     ecs <- helper [] ctx
      substTermLike 0 ecs a
 
 -- | Convert an 'MRVar' to a 'Term', applying it to all the uvars in scope

From ab31ae3f6453efec78f869c655188280865eb538 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 15 Feb 2022 14:18:34 -0800
Subject: [PATCH 08/22] added support for the maybe eliminator

---
 src/SAWScript/Prover/MRSolver.hs | 41 +++++++++++++++++++++++++++++---
 1 file changed, 38 insertions(+), 3 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index bc63f9dc7b..97563faf49 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -261,6 +261,7 @@ data NormComp
   | ErrorM Term -- ^ A term @errorM a str@
   | Ite Term Comp Comp -- ^ If-then-else computation
   | Either CompFun CompFun Term -- ^ A sum elimination
+  | MaybeElim Type Comp CompFun Term -- ^ A maybe elimination
   | OrM Comp Comp -- ^ an @orM@ computation
   | ExistsM Type CompFun -- ^ an @existsM@ computation
   | ForallM Type CompFun -- ^ a @forallM@ computation
@@ -363,11 +364,16 @@ instance PrettyInCtx NormComp where
   prettyInCtx (ErrorM str) =
     prettyAppList [return "errorM", return "_", parens <$> prettyInCtx str]
   prettyInCtx (Ite cond t1 t2) =
-    prettyAppList [return "ite", return "_", prettyInCtx cond,
+    prettyAppList [return "ite", return "_", parens <$> prettyInCtx cond,
                    parens <$> prettyInCtx t1, parens <$> prettyInCtx t2]
   prettyInCtx (Either f g eith) =
     prettyAppList [return "either", return "_", return "_", return "_",
-                   prettyInCtx f, prettyInCtx g, prettyInCtx eith]
+                   parens <$> prettyInCtx f, parens <$> prettyInCtx g,
+                   parens <$> prettyInCtx eith]
+  prettyInCtx (MaybeElim tp m f mayb) =
+    prettyAppList [return "maybe", parens <$> prettyInCtx tp,
+                   return (parens "CompM _"), parens <$> prettyInCtx m,
+                   parens <$> prettyInCtx f, parens <$> prettyInCtx mayb]
   prettyInCtx (OrM t1 t2) =
     prettyAppList [return "orM", return "_",
                    parens <$> prettyInCtx t1, parens <$> prettyInCtx t2]
@@ -419,7 +425,11 @@ instance TermLike NormComp where
     Ite <$> liftTermLike n i cond <*> liftTermLike n i t1 <*> liftTermLike n i t2
   liftTermLike n i (Either f g eith) =
     Either <$> liftTermLike n i f <*> liftTermLike n i g <*> liftTermLike n i eith
-  liftTermLike n i (OrM t1 t2) = OrM <$> liftTermLike n i t1 <*> liftTermLike n i t2
+  liftTermLike n i (MaybeElim tp m f mayb) =
+    MaybeElim <$> liftTermLike n i tp <*> liftTermLike n i m
+              <*> liftTermLike n i f <*> liftTermLike n i mayb
+  liftTermLike n i (OrM t1 t2) =
+    OrM <$> liftTermLike n i t1 <*> liftTermLike n i t2
   liftTermLike n i (ExistsM tp f) =
     ExistsM <$> liftTermLike n i tp <*> liftTermLike n i f
   liftTermLike n i (ForallM tp f) =
@@ -435,6 +445,9 @@ instance TermLike NormComp where
   substTermLike n s (Either f g eith) =
     Either <$> substTermLike n s f <*> substTermLike n s g
     <*> substTermLike n s eith
+  substTermLike n s (MaybeElim tp m f mayb) =
+    MaybeElim <$> substTermLike n s tp <*> substTermLike n s m
+              <*> substTermLike n s f <*> substTermLike n s mayb
   substTermLike n s (OrM t1 t2) =
     OrM <$> substTermLike n s t1 <*> substTermLike n s t2
   substTermLike n s (ExistsM tp f) =
@@ -1294,6 +1307,8 @@ normComp (CompTerm t) =
       return $ Ite cond (CompTerm then_tm) (CompTerm else_tm)
     (isGlobalDef "Prelude.either" -> Just (), [_, _, _, f, g, eith]) ->
       return $ Either (CompFunTerm f) (CompFunTerm g) eith
+    (isGlobalDef "Prelude.maybe" -> Just (), [tp, _, m, f, mayb]) ->
+      return $ MaybeElim (Type tp) (CompTerm m) (CompFunTerm f) mayb
     (isGlobalDef "Prelude.orM" -> Just (), [_, m1, m2]) ->
       return $ OrM (CompTerm m1) (CompTerm m2)
     (isGlobalDef "Prelude.existsM" -> Just (), [tp, _, body_tm]) ->
@@ -1356,6 +1371,8 @@ normBind (Ite cond comp1 comp2) k =
   return $ Ite cond (CompBind comp1 k) (CompBind comp2 k)
 normBind (Either f g t) k =
   return $ Either (compFunComp f k) (compFunComp g k) t
+normBind (MaybeElim tp m f t) k =
+  return $ MaybeElim tp (CompBind m k) (compFunComp f k) t
 normBind (OrM comp1 comp2) k =
   return $ OrM (CompBind comp1 k) (CompBind comp2 k)
 normBind (ExistsM tp f) k = return $ ExistsM tp (compFunComp f k)
@@ -1463,6 +1480,24 @@ mrRefines' m1 (Ite cond2 m2 m2') =
   do not_cond2 <- liftSC1 scNot cond2
      withAssumption cond2 (mrRefines m1 m2)
      withAssumption not_cond2 (mrRefines m1 m2')
+mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
+  do cond <- mrEq' tp e1 e2
+     not_cond <- liftSC1 scNot cond
+     cond_pf <- piUVarsM cond >>= mrFreshVar "pf" >>= mrVarTerm
+     m1' <- applyNormCompFun f1 cond_pf
+     cond_holds <- mrProvable cond
+     if cond_holds then mrRefines m1' m2 else
+       withAssumption cond (mrRefines m1' m2) >>
+       withAssumption not_cond (mrRefines m1 m2)
+mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) =
+  do cond <- mrEq' tp e1 e2
+     not_cond <- liftSC1 scNot cond
+     cond_pf <- piUVarsM cond >>= mrFreshVar "pf" >>= mrVarTerm
+     m2' <- applyNormCompFun f2 cond_pf
+     cond_holds <- mrProvable cond
+     if cond_holds then mrRefines m1 m2' else
+       withAssumption cond (mrRefines m1 m2') >>
+       withAssumption not_cond (mrRefines m1 m2)
 -- FIXME: handle sum elimination
 -- mrRefines (Either f1 g1 e1) (Either f2 g2 e2) =
 mrRefines' m1 (ForallM tp f2) =

From a1d5e4fa27ded8bdbde323af79e758187fc81553 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 17 Feb 2022 17:31:12 -0800
Subject: [PATCH 09/22] added applyGlobalOpenTerm and vectorTypeOpenTerm
 combinators

---
 saw-core/src/Verifier/SAW/OpenTerm.hs | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs
index d271153071..57c1fd7ad0 100644
--- a/saw-core/src/Verifier/SAW/OpenTerm.hs
+++ b/saw-core/src/Verifier/SAW/OpenTerm.hs
@@ -27,13 +27,14 @@ module Verifier.SAW.OpenTerm (
   unitOpenTerm, unitTypeOpenTerm,
   stringLitOpenTerm, stringTypeOpenTerm,
   trueOpenTerm, falseOpenTerm, boolOpenTerm, boolTypeOpenTerm,
-  arrayValueOpenTerm, bvLitOpenTerm, bvTypeOpenTerm,
+  arrayValueOpenTerm, vectorTypeOpenTerm, bvLitOpenTerm, bvTypeOpenTerm,
   pairOpenTerm, pairTypeOpenTerm, pairLeftOpenTerm, pairRightOpenTerm,
   tupleOpenTerm, tupleTypeOpenTerm, projTupleOpenTerm,
   tupleOpenTerm', tupleTypeOpenTerm',
   recordOpenTerm, recordTypeOpenTerm, projRecordOpenTerm,
   ctorOpenTerm, dataTypeOpenTerm, globalOpenTerm, extCnsOpenTerm,
-  applyOpenTerm, applyOpenTermMulti, applyPiOpenTerm, piArgOpenTerm,
+  applyOpenTerm, applyOpenTermMulti, applyGlobalOpenTerm,
+  applyPiOpenTerm, piArgOpenTerm,
   lambdaOpenTerm, lambdaOpenTermMulti, piOpenTerm, piOpenTermMulti,
   arrowOpenTerm, letOpenTerm, sawLetOpenTerm,
   -- * Monadic operations for building terms with binders
@@ -179,6 +180,10 @@ bvLitOpenTerm :: [Bool] -> OpenTerm
 bvLitOpenTerm bits =
   arrayValueOpenTerm boolTypeOpenTerm $ map boolOpenTerm bits
 
+-- | Create a SAW core term for a vector type
+vectorTypeOpenTerm :: OpenTerm -> OpenTerm -> OpenTerm
+vectorTypeOpenTerm n a = applyGlobalOpenTerm "Prelude.Vec" [n,a]
+
 -- | Create a SAW core term for the type of a bitvector
 bvTypeOpenTerm :: Integral a => a -> OpenTerm
 bvTypeOpenTerm n =
@@ -287,6 +292,10 @@ applyOpenTerm (OpenTerm f) (OpenTerm arg) =
 applyOpenTermMulti :: OpenTerm -> [OpenTerm] -> OpenTerm
 applyOpenTermMulti = foldl applyOpenTerm
 
+-- | Apply a named global to 0 or more arguments
+applyGlobalOpenTerm :: Ident -> [OpenTerm] -> OpenTerm
+applyGlobalOpenTerm ident = applyOpenTermMulti (globalOpenTerm ident)
+
 -- | Compute the output type of applying a function of a given type to an
 -- argument. That is, given @tp@ and @arg@, compute the type of applying any @f@
 -- of type @tp@ to @arg@.

From 2820052bfa1b71fb2f72eaa3d577d82a5140b4d0 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 17 Feb 2022 17:31:50 -0800
Subject: [PATCH 10/22] trying a new approach to getting SMT solving to work,
 by substiting uninterpreted functions in place of variable-length vectors

---
 src/SAWScript/Prover/MRSolver.hs | 127 ++++++++++++++++++++++++++++---
 1 file changed, 117 insertions(+), 10 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 97563faf49..a9c51b5e80 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -135,6 +135,7 @@ import Control.Monad.Trans.Maybe
 import qualified Data.IntMap as IntMap
 import Data.Map (Map)
 import qualified Data.Map as Map
+import qualified Data.Set as Set
 
 import Prettyprinter
 
@@ -144,8 +145,14 @@ import Verifier.SAW.Term.Pretty
 import Verifier.SAW.SCTypeCheck
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Recognizer
+import Verifier.SAW.OpenTerm
 import Verifier.SAW.Cryptol.Monadify
 
+import Verifier.SAW.Simulator
+import qualified Verifier.SAW.Prim as Prim
+import Verifier.SAW.Simulator.TermModel
+import Verifier.SAW.Simulator.Prims
+
 import SAWScript.Proof (termToProp, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
 
@@ -691,11 +698,9 @@ catchErrorEither m = catchError (Right <$> m) (return . Left)
 -- FIXME: replace these individual lifting functions with a more general
 -- typeclass like LiftTCM
 
-{-
 -- | Lift a nullary SharedTerm computation into 'MRM'
 liftSC0 :: (SharedContext -> IO a) -> MRM a
 liftSC0 f = (mrSC <$> get) >>= \sc -> liftIO (f sc)
--}
 
 -- | Lift a unary SharedTerm computation into 'MRM'
 liftSC1 :: (SharedContext -> a -> IO b) -> a -> MRM b
@@ -714,6 +719,11 @@ liftSC4 :: (SharedContext -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d ->
            MRM e
 liftSC4 f a b c d = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d)
 
+-- | Lift a quaternary SharedTerm computation into 'MRM'
+liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) ->
+           a -> b -> c -> d -> e -> MRM f
+liftSC5 f a b c d e = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d e)
+
 -- | Apply a 'Term' to a list of arguments and beta-reduce in Mr. Monad
 mrApplyAll :: Term -> [Term] -> MRM Term
 mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize
@@ -807,9 +817,9 @@ lambdaUVarsM t = mrUVarCtx >>= \ctx -> liftSC2 scLambdaList ctx t
 piUVarsM :: Term -> MRM Term
 piUVarsM t = mrUVarCtx >>= \ctx -> liftSC2 scPiList ctx t
 
--- | Instantiate all uvars in a term with fresh 'ExtCns's
-instantiateUVarsM :: TermLike a => a -> MRM a
-instantiateUVarsM a =
+-- | Instantiate all uvars in a term using the supplied function
+instantiateUVarsM :: TermLike a => (LocalName -> Term -> MRM Term) -> a -> MRM a
+instantiateUVarsM f a =
   do ctx <- mrUVarCtx
      -- Remember: the uvar context is outermost to innermost, so we bind
      -- variables from left to right, substituting earlier ones into the types
@@ -819,7 +829,7 @@ instantiateUVarsM a =
          helper tms [] = return tms
          helper tms ((nm,tp):vars) =
            do tp' <- substTerm 0 tms tp
-              tm <- liftSC2 scFreshEC nm tp' >>= liftSC1 scExtCns
+              tm <- f nm tp'
               helper (tm:tms) vars
      ecs <- helper [] ctx
      substTermLike 0 ecs a
@@ -1069,8 +1079,8 @@ debugPretty i pp = debugPrint i $ renderSawDoc defaultPPOpts pp
 
 -- | Pretty-print an object in the current context if the current debug level is
 -- at least the supplied 'Int'
-_debugPrettyInCtx :: PrettyInCtx a => Int -> a -> MRM ()
-_debugPrettyInCtx i a =
+debugPrettyInCtx :: PrettyInCtx a => Int -> a -> MRM ()
+debugPrettyInCtx i a =
   (mrUVars <$> get) >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
 
 -- | Pretty-print an object relative to the current context
@@ -1093,6 +1103,86 @@ mrDebugPPPrefixSep i pre a1 sp a2 =
 -- * Calling Out to SMT
 ----------------------------------------------------------------------
 
+-- | Test if a 'Term' is a 'BVVec' type
+asBVVecType :: Recognizer Term (Term, Term, Term)
+asBVVecType (asApplyAll ->
+             (isGlobalDef "Prelude.Vec" -> Just _,
+              [(asApplyAll ->
+                (isGlobalDef "Prelude.bvToNat" -> Just _, [n, len])), a])) =
+  Just (n, len, a)
+asBVVecType _ = Nothing
+
+-- | Apply @genBVVec@ to arguments @n@, @len@, and @a@, along with a function of
+-- type @Vec n Bool -> a@
+genBVVecTerm :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
+genBVVecTerm sc n_tm len_tm a_tm f_tm =
+  let n = closedOpenTerm n_tm
+      len = closedOpenTerm len_tm
+      a = closedOpenTerm a_tm
+      f = closedOpenTerm f_tm in
+  completeOpenTerm sc $
+  applyOpenTermMulti (globalOpenTerm "Prelude.genBVVec")
+  [n, len, a,
+   lambdaOpenTerm "i" (vectorTypeOpenTerm n boolTypeOpenTerm) $ \i ->
+    lambdaOpenTerm "_" (applyGlobalOpenTerm "Prelude.is_bvult" [n, i, len]) $ \_ ->
+    applyOpenTerm f i]
+
+-- | Match a term of the form @genBVVec n len a (\ i _ -> f i)@ and return @f@
+asGenBVVecTerm :: Recognizer Term Term
+asGenBVVecTerm (asApplyAll ->
+                   (isGlobalDef "Prelude.genBVVec" -> Just _,
+                    [_, _, _,
+                     (asLambdaList -> ([_,_], asApp ->
+                                       Just (f, asLocalVar -> Just 1)))])) =
+  Just f
+asGenBVVecTerm _ = Nothing
+
+type TmPrim = Prim TermModel
+
+-- | An implementation of a primitive function that expects a @genBVVec@ term
+primGenBVVec :: (Term -> TmPrim) -> TmPrim
+primGenBVVec f =
+  PrimFilterFun "genBVVecPrim"
+  (\case
+      VExtra (VExtraTerm _ (asGenBVVecTerm -> Just g)) -> return g
+      _ -> mzero)
+  f
+
+-- | An implementation of a primitive function that expects a bitvector term
+primBVTermFun :: SharedContext -> (Term -> TmPrim) -> TmPrim
+primBVTermFun sc =
+  PrimFilterFun "primBVTermFun" $
+  \case
+    VExtra (VExtraTerm _ w_tm) -> return w_tm
+    VWord (Left (_,w_tm)) -> return w_tm
+    VWord (Right bv) ->
+      lift $ scBvConst sc (fromIntegral (Prim.width bv)) (Prim.unsigned bv)
+    _ -> mzero
+
+-- | Implementations of primitives for normalizing SMT terms
+smtNormPrims :: SharedContext -> Map Ident TmPrim
+smtNormPrims sc = Map.fromList
+  [
+    ("Prelude.genBVVec",
+     Prim (do tp <- scTypeOfGlobal sc "Prelude.genBVVec"
+              VExtra <$> VExtraTerm (VTyTerm (mkSort 1) tp) <$>
+                scGlobalDef sc "Prelude.genBVVec")),
+
+    ("Prelude.atBVVec",
+     PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a ->
+      primGenBVVec $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
+      Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix))
+  ]
+
+-- | Normalize a 'Term' before building an SMT query for it
+normSMTProp :: Term -> MRM Term
+normSMTProp t =
+  debugPrint 2 "Normalizing term:" >>
+  debugPrettyInCtx 2 t >>
+  liftSC0 return >>= \sc ->
+  liftSC0 scGetModuleMap >>= \modmap ->
+  liftSC5 normalizeSharedTerm modmap (smtNormPrims sc) Map.empty Set.empty t
+
 -- | Test if a closed Boolean term is "provable", i.e., its negation is
 -- unsatisfiable, using an SMT solver. By "closed" we mean that it contains no
 -- uvars or 'MRVar's.
@@ -1116,8 +1206,25 @@ mrProvable :: Term -> MRM Bool
 mrProvable bool_tm =
   do assumps <- mrAssumptions <$> get
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
-     forall_prop <- instantiateUVarsM prop
-     mrProvableRaw forall_prop
+     prop_inst <- flip instantiateUVarsM prop $ \nm tp ->
+       liftSC1 scWhnf tp >>= \case
+       (asBVVecType -> Just (n, len, a)) ->
+         -- For variables of type BVVec, create a Vec n Bool -> a function as an
+         -- ExtCns and apply genBVVec to it
+         do
+           debugPrint 2 ("Is BVVec variable: " ++ show nm)
+           ec_tp <-
+             liftSC1 completeOpenTerm $
+             arrowOpenTerm "_" (applyOpenTermMulti (globalOpenTerm "Prelude.Vec")
+                                [closedOpenTerm n, boolTypeOpenTerm])
+             (closedOpenTerm a)
+           ec <- liftSC2 scFreshEC nm ec_tp >>= liftSC1 scExtCns
+           liftSC4 genBVVecTerm n len a ec
+       tp' ->
+         debugPrint 2 ("Is not BVVec variable: " ++ show nm ++ " of type:") >>
+         debugPrettyInCtx 2 tp' >>
+         liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns
+     normSMTProp prop_inst >>= mrProvableRaw
 
 -- | Build a Boolean 'Term' stating that two 'Term's are equal. This is like
 -- 'scEq' except that it works on open terms.

From 201c796a0431aacbc5bef56124d95453771c4a0a Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 06:45:59 -0800
Subject: [PATCH 11/22] whoops: need to coerce the type of the condition in
 MaybeElim to a proposition by adding an EqTrue

---
 src/SAWScript/Prover/MRSolver.hs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index a9c51b5e80..fbcff18d0f 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -1169,9 +1169,15 @@ smtNormPrims sc = Map.fromList
                 scGlobalDef sc "Prelude.genBVVec")),
 
     ("Prelude.atBVVec",
+     Prim (do tp <- scTypeOfGlobal sc "Prelude.atBVVec"
+              VExtra <$> VExtraTerm (VTyTerm (mkSort 1) tp) <$>
+                scGlobalDef sc "Prelude.atBVVec")
+     -- FIXME HERE NOW: use the following for atBVVec!
+     {-
      PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a ->
       primGenBVVec $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
-      Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix))
+      Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix) -}
+    )
   ]
 
 -- | Normalize a 'Term' before building an SMT query for it
@@ -1590,7 +1596,8 @@ mrRefines' m1 (Ite cond2 m2 m2') =
 mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
   do cond <- mrEq' tp e1 e2
      not_cond <- liftSC1 scNot cond
-     cond_pf <- piUVarsM cond >>= mrFreshVar "pf" >>= mrVarTerm
+     cond_pf <-
+       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
      m1' <- applyNormCompFun f1 cond_pf
      cond_holds <- mrProvable cond
      if cond_holds then mrRefines m1' m2 else
@@ -1599,7 +1606,8 @@ mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
 mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) =
   do cond <- mrEq' tp e1 e2
      not_cond <- liftSC1 scNot cond
-     cond_pf <- piUVarsM cond >>= mrFreshVar "pf" >>= mrVarTerm
+     cond_pf <-
+       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
      m2' <- applyNormCompFun f2 cond_pf
      cond_holds <- mrProvable cond
      if cond_holds then mrRefines m1 m2' else

From b388f9a4fb36ee4f9cd4a15cccb24f424f939820 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 09:49:34 -0800
Subject: [PATCH 12/22] added back the implementaiton of atBVVec; enriched
 primBVTermFun to handle vector values

---
 src/SAWScript/Prover/MRSolver.hs | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index fbcff18d0f..3a0ca68de3 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -125,6 +125,7 @@ module SAWScript.Prover.MRSolver
 
 import Data.List (find, findIndex)
 import qualified Data.Text as T
+import qualified Data.Vector as V
 import Data.IORef
 import System.IO (hPutStrLn, stderr)
 import Control.Monad.Reader
@@ -148,10 +149,10 @@ import Verifier.SAW.Recognizer
 import Verifier.SAW.OpenTerm
 import Verifier.SAW.Cryptol.Monadify
 
-import Verifier.SAW.Simulator
 import qualified Verifier.SAW.Prim as Prim
 import Verifier.SAW.Simulator.TermModel
 import Verifier.SAW.Simulator.Prims
+import Verifier.SAW.Simulator.MonadLazy
 
 import SAWScript.Proof (termToProp, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
@@ -1139,6 +1140,14 @@ asGenBVVecTerm _ = Nothing
 
 type TmPrim = Prim TermModel
 
+-- | Convert a Boolean value to a 'Term'; like 'readBackValue' but that function
+-- requires a 'SimulatorConfig' which we cannot easily generate here...
+boolValToTerm :: SharedContext -> Value TermModel -> IO Term
+boolValToTerm _ (VBool (Left tm)) = return tm
+boolValToTerm sc (VBool (Right b)) = scBool sc b
+boolValToTerm _ (VExtra (VExtraTerm _tp tm)) = return tm
+boolValToTerm _ v = error ("boolValToTerm: unexpected value: " ++ show v)
+
 -- | An implementation of a primitive function that expects a @genBVVec@ term
 primGenBVVec :: (Term -> TmPrim) -> TmPrim
 primGenBVVec f =
@@ -1157,7 +1166,12 @@ primBVTermFun sc =
     VWord (Left (_,w_tm)) -> return w_tm
     VWord (Right bv) ->
       lift $ scBvConst sc (fromIntegral (Prim.width bv)) (Prim.unsigned bv)
-    _ -> mzero
+    VVector vs ->
+      lift $
+      do tms <- traverse (boolValToTerm sc <=< force) (V.toList vs)
+         tp <- scBoolType sc
+         scVectorReduced sc tp tms
+    v -> lift (putStrLn ("primBVTermFun: unhandled value: " ++ show v)) >> mzero
 
 -- | Implementations of primitives for normalizing SMT terms
 smtNormPrims :: SharedContext -> Map Ident TmPrim
@@ -1169,14 +1183,9 @@ smtNormPrims sc = Map.fromList
                 scGlobalDef sc "Prelude.genBVVec")),
 
     ("Prelude.atBVVec",
-     Prim (do tp <- scTypeOfGlobal sc "Prelude.atBVVec"
-              VExtra <$> VExtraTerm (VTyTerm (mkSort 1) tp) <$>
-                scGlobalDef sc "Prelude.atBVVec")
-     -- FIXME HERE NOW: use the following for atBVVec!
-     {-
      PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a ->
       primGenBVVec $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
-      Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix) -}
+      Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix)
     )
   ]
 

From af6d5165953e1e78bd36f509df5a711e83f59539 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 11:14:52 -0800
Subject: [PATCH 13/22] refactored mrProveEq to support proving equality of
 arbitrary vectors by proving equality at all indices

---
 src/SAWScript/Prover/MRSolver.hs | 109 +++++++++++++++++--------------
 1 file changed, 60 insertions(+), 49 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 3a0ca68de3..4eb427fcfd 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -1259,72 +1259,83 @@ mrEq' (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
 mrEq' _ _ _ = error "mrEq': unsupported type"
 
 -- | A "simple" strategy for proving equality between two terms, which we assume
--- are of the same type. This strategy first checks if either side is an
--- uninstantiated evar, in which case it set that evar to the other side. If
--- not, it builds an equality proposition by applying the supplied function to
--- both sides, and passes this proposition to an SMT solver.
+-- are of the same type, which builds an equality proposition by applying the
+-- supplied function to both sides and passes this proposition to an SMT solver.
 mrProveEqSimple :: (Term -> Term -> MRM Term) -> MRVarMap -> Term -> Term ->
                    MRM ()
+-- NOTE: The use of mrSubstEVars instead of mrSubstEVarsStrict means that we
+-- allow evars in the terms we send to the SMT solver, but we treat them as
+-- uvars.
+mrProveEqSimple eqf _ t1 t2 =
+  do t1' <- mrSubstEVars t1
+     t2' <- mrSubstEVars t2
+     prop <- eqf t1' t2'
+     success <- mrProvable prop
+     if success then return () else
+       throwError (TermsNotEq t1 t2)
+
+
+-- | Prove that two terms are equal, instantiating evars if necessary, or
+-- throwing an error if this is not possible
+mrProveEq :: Term -> Term -> MRM ()
+mrProveEq t1 t2 =
+  do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
+     tp <- mrTypeOf t1
+     varmap <- mrVars <$> get
+     mrProveEqH varmap tp t1 t2
+
+
+-- | The main workhorse for 'prProveEq'
+mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM ()
 
 -- If t1 is an instantiated evar, substitute and recurse
-mrProveEqSimple eqf var_map (asEVarApp var_map -> Just (_, args, Just f)) t2 =
-  mrApplyAll f args >>= \t1' -> mrProveEqSimple eqf var_map t1' t2
+mrProveEqH var_map tp (asEVarApp var_map -> Just (_, args, Just f)) t2 =
+  mrApplyAll f args >>= \t1' -> mrProveEqH var_map tp t1' t2
 
 -- If t1 is an uninstantiated evar, instantiate it with t2
-mrProveEqSimple _ var_map t1@(asEVarApp var_map ->
-                              Just (evar, args, Nothing)) t2 =
+mrProveEqH var_map _tp t1@(asEVarApp var_map -> Just (evar, args, Nothing)) t2 =
   do t2' <- mrSubstEVars t2
      success <- mrTrySetAppliedEVar evar args t2'
      if success then return () else throwError (TermsNotEq t1 t2)
 
 -- If t2 is an instantiated evar, substitute and recurse
-mrProveEqSimple eqf var_map t1 (asEVarApp var_map -> Just (_, args, Just f)) =
-  mrApplyAll f args >>= \t2' -> mrProveEqSimple eqf var_map t1 t2'
+mrProveEqH var_map tp t1 (asEVarApp var_map -> Just (_, args, Just f)) =
+  mrApplyAll f args >>= \t2' -> mrProveEqH var_map tp t1 t2'
 
 -- If t2 is an uninstantiated evar, instantiate it with t1
-mrProveEqSimple _ var_map t1 t2@(asEVarApp var_map ->
-                                 Just (evar, args, Nothing)) =
+mrProveEqH var_map _tp t1 t2@(asEVarApp var_map -> Just (evar, args, Nothing)) =
   do t1' <- mrSubstEVars t1
      success <- mrTrySetAppliedEVar evar args t1'
      if success then return () else throwError (TermsNotEq t1 t2)
 
--- Otherwise, try to prove both sides are equal. The use of mrSubstEVars instead
--- of mrSubstEVarsStrict means that we allow evars in the terms we send to the
--- SMT solver, but we treat them as uvars.
-mrProveEqSimple eqf _ t1 t2 =
-  do t1' <- mrSubstEVars t1
-     t2' <- mrSubstEVars t2
-     prop <- eqf t1' t2'
-     success <- mrProvable prop
-     if success then return () else
-       throwError (TermsNotEq t1 t2)
-
-
--- | Prove that two terms are equal, instantiating evars if necessary, or
--- throwing an error if this is not possible
-mrProveEq :: Term -> Term -> MRM ()
-mrProveEq t1_top t2_top =
-  (do mrDebugPPPrefixSep 1 "mrProveEq" t1_top "==" t2_top
-      tp <- mrTypeOf t1_top
-      varmap <- mrVars <$> get
-      proveEq varmap tp t1_top t2_top)
-  where
-    proveEq :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM ()
-    proveEq var_map (asDataType -> Just (pn, [])) t1 t2
-      | primName pn == "Prelude.Nat" =
-        mrProveEqSimple (liftSC2 scEqualNat) var_map t1 t2
-    proveEq var_map (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
-      -- FIXME: make a better solver for bitvector equalities
-      mrProveEqSimple (liftSC3 scBvEq n) var_map t1 t2
-    proveEq var_map (asBoolType -> Just _) t1 t2 =
-      mrProveEqSimple (liftSC2 scBoolEq) var_map t1 t2
-    proveEq var_map (asIntegerType -> Just _) t1 t2 =
-      mrProveEqSimple (liftSC2 scIntEq) var_map t1 t2
-    proveEq _ _ t1 t2 =
-      -- As a fallback, for types we can't handle, just check convertibility
-      mrConvertible t1 t2 >>= \case
-      True -> return ()
-      False -> throwError (TermsNotEq t1 t2)
+-- For the nat, bitvector, Boolean, and integer types, call mrProveEqSimple
+mrProveEqH var_map (asDataType -> Just (pn, [])) t1 t2
+  | primName pn == "Prelude.Nat" =
+    mrProveEqSimple (liftSC2 scEqualNat) var_map t1 t2
+mrProveEqH var_map (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
+  -- FIXME: make a better solver for bitvector equalities
+  mrProveEqSimple (liftSC3 scBvEq n) var_map t1 t2
+mrProveEqH var_map (asBoolType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scBoolEq) var_map t1 t2
+mrProveEqH var_map (asIntegerType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scIntEq) var_map t1 t2
+
+-- For non-bitvector vector types, prove all projections are equal by
+-- quantifying over a universal index variable and proving equality at that
+-- index
+mrProveEqH var_map (asBVVecType -> Just (n, len, tp)) t1 t2 =
+  withUVar "eq_ix" (Type tp) $ \ix ->
+  liftSC2 scGlobalApply "Prelude.is_bvult" [n, ix, len] >>= \pf_tp ->
+  withUVar "eq_pf" (Type pf_tp) $ \pf ->
+  do t1' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t1, ix, pf]
+     t2' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t2, ix, pf]
+     mrProveEqH var_map tp t1' t2'
+
+-- As a fallback, for types we can't handle, just check convertibility
+mrProveEqH _ _ t1 t2 =
+  mrConvertible t1 t2 >>= \case
+  True -> return ()
+  False -> throwError (TermsNotEq t1 t2)
 
 
 ----------------------------------------------------------------------

From 338aa0e977ee577a9ea9701d05d6906fe57c36ee Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 17:10:47 -0800
Subject: [PATCH 14/22] got mrProveEq to handle pair types by changing it to
 return a TermInCtx; fixed a bug in withUVar, that assumptions added under the
 extended context should be thrown away when that context ends

---
 src/SAWScript/Prover/MRSolver.hs | 162 ++++++++++++++++++++++---------
 1 file changed, 114 insertions(+), 48 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 4eb427fcfd..f05eb37aab 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -157,6 +157,8 @@ import Verifier.SAW.Simulator.MonadLazy
 import SAWScript.Proof (termToProp, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
 
+-- import Debug.Trace
+
 
 ----------------------------------------------------------------------
 -- * Utility Functions for Transforming 'Term's
@@ -642,7 +644,8 @@ data MRState = MRState {
   mrVars :: MRVarMap,
   -- | The current assumptions of function refinement
   mrFunAssumps :: Map FunName FunAssump,
-  -- | The current assumptions, which are conjoined into a single Boolean term
+  -- | The current assumptions, which are conjoined into a single Boolean term;
+  -- note that these have the current UVars free
   mrAssumptions :: Term,
   -- | The debug level, which controls debug printing
   mrDebugLevel :: Int
@@ -770,14 +773,18 @@ uniquifyName nm nms =
     Nothing -> error "uniquifyName"
 
 -- | Run a MR Solver computation in a context extended with a universal
--- variable, which is passed as a 'Term' to the sub-computation
+-- variable, which is passed as a 'Term' to the sub-computation. Note that any
+-- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
 withUVar nm tp m =
   do st <- get
      let nm' = uniquifyName nm (map fst $ mrUVars st)
-     put (st { mrUVars = (nm',tp) : mrUVars st })
+     assumps' <- liftTerm 0 1 $ mrAssumptions st
+     put (st { mrUVars = (nm',tp) : mrUVars st,
+               mrAssumptions = assumps' })
      ret <- mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
-     modify (\st' -> st' { mrUVars = mrUVars st })
+     modify (\st' -> st' { mrUVars = mrUVars st,
+                           mrAssumptions = mrAssumptions st })
      return ret
 
 -- | Run a MR Solver computation in a context extended with a universal variable
@@ -1128,14 +1135,15 @@ genBVVecTerm sc n_tm len_tm a_tm f_tm =
     lambdaOpenTerm "_" (applyGlobalOpenTerm "Prelude.is_bvult" [n, i, len]) $ \_ ->
     applyOpenTerm f i]
 
--- | Match a term of the form @genBVVec n len a (\ i _ -> f i)@ and return @f@
-asGenBVVecTerm :: Recognizer Term Term
+-- | Match a term of the form @genBVVec n len a (\ i _ -> e)@, i.e., where @e@
+-- does not have the proof variable (the underscore) free
+asGenBVVecTerm :: Recognizer Term (Term, Term, Term, Term)
 asGenBVVecTerm (asApplyAll ->
                    (isGlobalDef "Prelude.genBVVec" -> Just _,
-                    [_, _, _,
-                     (asLambdaList -> ([_,_], asApp ->
-                                       Just (f, asLocalVar -> Just 1)))])) =
-  Just f
+                    [n, len, a,
+                     (asLambdaList -> ([_,_], e))]))
+  | not $ inBitSet 0 $ looseVars e
+  = Just (n, len, a, e)
 asGenBVVecTerm _ = Nothing
 
 type TmPrim = Prim TermModel
@@ -1149,11 +1157,18 @@ boolValToTerm _ (VExtra (VExtraTerm _tp tm)) = return tm
 boolValToTerm _ v = error ("boolValToTerm: unexpected value: " ++ show v)
 
 -- | An implementation of a primitive function that expects a @genBVVec@ term
-primGenBVVec :: (Term -> TmPrim) -> TmPrim
-primGenBVVec f =
+primGenBVVec :: SharedContext -> (Term -> TmPrim) -> TmPrim
+primGenBVVec sc f =
   PrimFilterFun "genBVVecPrim"
   (\case
-      VExtra (VExtraTerm _ (asGenBVVecTerm -> Just g)) -> return g
+      VExtra (VExtraTerm _ (asGenBVVecTerm -> Just (n, _, _, e))) ->
+        -- Generate the function \i -> [i/1,error/0]e
+        lift $
+        do i_tp <- scBoolType sc >>= scVecType sc n
+           let err_tm = error "primGenBVVec: unexpected variable occurrence"
+           i_tm <- scLocalVar sc 0
+           body <- instantiateVarList sc 0 [err_tm,i_tm] e
+           scLambda sc "i" i_tp body
       _ -> mzero)
   f
 
@@ -1184,7 +1199,7 @@ smtNormPrims sc = Map.fromList
 
     ("Prelude.atBVVec",
      PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a ->
-      primGenBVVec $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
+      primGenBVVec sc $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
       Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix)
     )
   ]
@@ -1227,7 +1242,6 @@ mrProvable bool_tm =
          -- For variables of type BVVec, create a Vec n Bool -> a function as an
          -- ExtCns and apply genBVVec to it
          do
-           debugPrint 2 ("Is BVVec variable: " ++ show nm)
            ec_tp <-
              liftSC1 completeOpenTerm $
              arrowOpenTerm "_" (applyOpenTermMulti (globalOpenTerm "Prelude.Vec")
@@ -1236,7 +1250,6 @@ mrProvable bool_tm =
            ec <- liftSC2 scFreshEC nm ec_tp >>= liftSC1 scExtCns
            liftSC4 genBVVecTerm n len a ec
        tp' ->
-         debugPrint 2 ("Is not BVVec variable: " ++ show nm ++ " of type:") >>
          debugPrettyInCtx 2 tp' >>
          liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns
      normSMTProp prop_inst >>= mrProvableRaw
@@ -1258,21 +1271,47 @@ mrEq' (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
   liftSC3 scBvEq n t1 t2
 mrEq' _ _ _ = error "mrEq': unsupported type"
 
+-- | A 'Term' in an extended context of universal variables, which are listed
+-- "outside in", meaning the highest deBruijn index comes first
+data TermInCtx = TermInCtx [(LocalName,Term)] Term
+
+-- | Conjoin two 'TermInCtx's, assuming they both have Boolean type
+andTermInCtx :: TermInCtx -> TermInCtx -> MRM TermInCtx
+andTermInCtx (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) =
+  do
+    -- Insert the variables in ctx2 into the context of t1 starting at index 0,
+    -- by lifting its variables starting at 0 by length ctx2
+    t1' <- liftTermLike 0 (length ctx2) t1
+    -- Insert the variables in ctx1 into the context of t1 starting at index
+    -- length ctx2, by lifting its variables starting at length ctx2 by length
+    -- ctx1
+    t2' <- liftTermLike (length ctx2) (length ctx1) t2
+    TermInCtx (ctx1++ctx2) <$> liftSC2 scAnd t1' t2'
+
+-- | Extend the context of a 'TermInCtx' with additional universal variables
+-- bound "outside" the 'TermInCtx'
+extTermInCtx :: [(LocalName,Term)] -> TermInCtx -> TermInCtx
+extTermInCtx ctx (TermInCtx ctx' t) = TermInCtx (ctx++ctx') t
+
+-- | Run an 'MRM' computation in the context of a 'TermInCtx', passing in the
+-- 'Term'
+withTermInCtx :: TermInCtx -> (Term -> MRM a) -> MRM a
+withTermInCtx (TermInCtx [] tm) f = f tm
+withTermInCtx (TermInCtx ((nm,tp):ctx) tm) f =
+  withUVar nm (Type tp) $ const $ withTermInCtx (TermInCtx ctx tm) f
+
 -- | A "simple" strategy for proving equality between two terms, which we assume
 -- are of the same type, which builds an equality proposition by applying the
 -- supplied function to both sides and passes this proposition to an SMT solver.
-mrProveEqSimple :: (Term -> Term -> MRM Term) -> MRVarMap -> Term -> Term ->
-                   MRM ()
+mrProveEqSimple :: (Term -> Term -> MRM Term) -> Term -> Term ->
+                   MRM TermInCtx
 -- NOTE: The use of mrSubstEVars instead of mrSubstEVarsStrict means that we
 -- allow evars in the terms we send to the SMT solver, but we treat them as
 -- uvars.
-mrProveEqSimple eqf _ t1 t2 =
+mrProveEqSimple eqf t1 t2 =
   do t1' <- mrSubstEVars t1
      t2' <- mrSubstEVars t2
-     prop <- eqf t1' t2'
-     success <- mrProvable prop
-     if success then return () else
-       throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> eqf t1' t2'
 
 
 -- | Prove that two terms are equal, instantiating evars if necessary, or
@@ -1282,60 +1321,87 @@ mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
      tp <- mrTypeOf t1
      varmap <- mrVars <$> get
-     mrProveEqH varmap tp t1 t2
+     cond_in_ctx <- mrProveEqH varmap tp t1 t2
+     success <- withTermInCtx cond_in_ctx mrProvable
+     if success then return () else
+       throwError (TermsNotEq t1 t2)
 
+-- | The main workhorse for 'prProveEq'. Build a Boolean term expressing that
+-- the third and fourth arguments, whose type is given by the second. This is
+-- done in a continuation monad so that the output term can be in a context with
+-- additional universal variables.
+mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM TermInCtx
 
--- | The main workhorse for 'prProveEq'
-mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM ()
+{-
+mrProveEqH _ _ t1 t2
+  | trace ("mrProveEqH:\n" ++ showTerm t1 ++ "\n==\n" ++ showTerm t2) False = undefined
+-}
 
 -- If t1 is an instantiated evar, substitute and recurse
 mrProveEqH var_map tp (asEVarApp var_map -> Just (_, args, Just f)) t2 =
   mrApplyAll f args >>= \t1' -> mrProveEqH var_map tp t1' t2
 
 -- If t1 is an uninstantiated evar, instantiate it with t2
-mrProveEqH var_map _tp t1@(asEVarApp var_map -> Just (evar, args, Nothing)) t2 =
+mrProveEqH var_map _tp (asEVarApp var_map -> Just (evar, args, Nothing)) t2 =
   do t2' <- mrSubstEVars t2
      success <- mrTrySetAppliedEVar evar args t2'
-     if success then return () else throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> liftSC1 scBool success
 
 -- If t2 is an instantiated evar, substitute and recurse
 mrProveEqH var_map tp t1 (asEVarApp var_map -> Just (_, args, Just f)) =
   mrApplyAll f args >>= \t2' -> mrProveEqH var_map tp t1 t2'
 
 -- If t2 is an uninstantiated evar, instantiate it with t1
-mrProveEqH var_map _tp t1 t2@(asEVarApp var_map -> Just (evar, args, Nothing)) =
+mrProveEqH var_map _tp t1 (asEVarApp var_map -> Just (evar, args, Nothing)) =
   do t1' <- mrSubstEVars t1
      success <- mrTrySetAppliedEVar evar args t1'
-     if success then return () else throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> liftSC1 scBool success
 
 -- For the nat, bitvector, Boolean, and integer types, call mrProveEqSimple
-mrProveEqH var_map (asDataType -> Just (pn, [])) t1 t2
+mrProveEqH _ (asDataType -> Just (pn, [])) t1 t2
   | primName pn == "Prelude.Nat" =
-    mrProveEqSimple (liftSC2 scEqualNat) var_map t1 t2
-mrProveEqH var_map (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
+    mrProveEqSimple (liftSC2 scEqualNat) t1 t2
+mrProveEqH _ (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
   -- FIXME: make a better solver for bitvector equalities
-  mrProveEqSimple (liftSC3 scBvEq n) var_map t1 t2
-mrProveEqH var_map (asBoolType -> Just _) t1 t2 =
-  mrProveEqSimple (liftSC2 scBoolEq) var_map t1 t2
-mrProveEqH var_map (asIntegerType -> Just _) t1 t2 =
-  mrProveEqSimple (liftSC2 scIntEq) var_map t1 t2
+  mrProveEqSimple (liftSC3 scBvEq n) t1 t2
+mrProveEqH _ (asBoolType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scBoolEq) t1 t2
+mrProveEqH _ (asIntegerType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scIntEq) t1 t2
+
+-- For pair types, prove both the left and right projections are equal
+mrProveEqH var_map (asPairType -> Just (tpL, tpR)) t1 t2 =
+  do t1L <- liftSC1 scPairLeft t1
+     t2L <- liftSC1 scPairLeft t2
+     t1R <- liftSC1 scPairRight t1
+     t2R <- liftSC1 scPairRight t2
+     condL <- mrProveEqH var_map tpL t1L t2L
+     condR <- mrProveEqH var_map tpR t1R t2R
+     andTermInCtx condL condR
 
 -- For non-bitvector vector types, prove all projections are equal by
 -- quantifying over a universal index variable and proving equality at that
 -- index
-mrProveEqH var_map (asBVVecType -> Just (n, len, tp)) t1 t2 =
-  withUVar "eq_ix" (Type tp) $ \ix ->
-  liftSC2 scGlobalApply "Prelude.is_bvult" [n, ix, len] >>= \pf_tp ->
-  withUVar "eq_pf" (Type pf_tp) $ \pf ->
-  do t1' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t1, ix, pf]
-     t2' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t2, ix, pf]
-     mrProveEqH var_map tp t1' t2'
+mrProveEqH _ (asBVVecType -> Just (n, len, tp)) t1 t2 =
+  liftSC0 scBoolType >>= \bool_tp ->
+  liftSC2 scVecType n bool_tp >>= \ix_tp ->
+  withUVarLift "eq_ix" (Type ix_tp) (n,(len,(tp,(t1,t2)))) $
+  \ix' (n',(len',(tp',(t1',t2')))) ->
+  liftSC2 scGlobalApply "Prelude.is_bvult" [n', ix', len'] >>= \pf_tp ->
+  withUVarLift "eq_pf" (Type pf_tp) (n',(len',(tp',(ix',(t1',t2'))))) $
+  \pf'' (n'',(len'',(tp'',(ix'',(t1'',t2''))))) ->
+  do t1_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n'', len'', tp'',
+                                                        t1'', ix'', pf'']
+     t2_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n'', len'', tp'',
+                                                        t2'', ix'', pf'']
+     var_map <- mrVars <$> get
+     extTermInCtx [("eq_ix",ix_tp),("eq_pf",pf_tp)] <$>
+       mrProveEqH var_map tp'' t1_prj t2_prj
 
 -- As a fallback, for types we can't handle, just check convertibility
 mrProveEqH _ _ t1 t2 =
-  mrConvertible t1 t2 >>= \case
-  True -> return ()
-  False -> throwError (TermsNotEq t1 t2)
+  do success <- mrConvertible t1 t2
+     TermInCtx [] <$> liftSC1 scBool success
 
 
 ----------------------------------------------------------------------

From 5778c25959b246b2603eb85a3ec53586af72ecd9 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 17:10:47 -0800
Subject: [PATCH 15/22] got mrProveEq to handle pair types by changing it to
 return a TermInCtx; fixed a bug in withUVar, that assumptions need to be
 lifted in the new context and then reverted when that context ends

---
 src/SAWScript/Prover/MRSolver.hs | 162 ++++++++++++++++++++++---------
 1 file changed, 114 insertions(+), 48 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 4eb427fcfd..f05eb37aab 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -157,6 +157,8 @@ import Verifier.SAW.Simulator.MonadLazy
 import SAWScript.Proof (termToProp, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
 
+-- import Debug.Trace
+
 
 ----------------------------------------------------------------------
 -- * Utility Functions for Transforming 'Term's
@@ -642,7 +644,8 @@ data MRState = MRState {
   mrVars :: MRVarMap,
   -- | The current assumptions of function refinement
   mrFunAssumps :: Map FunName FunAssump,
-  -- | The current assumptions, which are conjoined into a single Boolean term
+  -- | The current assumptions, which are conjoined into a single Boolean term;
+  -- note that these have the current UVars free
   mrAssumptions :: Term,
   -- | The debug level, which controls debug printing
   mrDebugLevel :: Int
@@ -770,14 +773,18 @@ uniquifyName nm nms =
     Nothing -> error "uniquifyName"
 
 -- | Run a MR Solver computation in a context extended with a universal
--- variable, which is passed as a 'Term' to the sub-computation
+-- variable, which is passed as a 'Term' to the sub-computation. Note that any
+-- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
 withUVar nm tp m =
   do st <- get
      let nm' = uniquifyName nm (map fst $ mrUVars st)
-     put (st { mrUVars = (nm',tp) : mrUVars st })
+     assumps' <- liftTerm 0 1 $ mrAssumptions st
+     put (st { mrUVars = (nm',tp) : mrUVars st,
+               mrAssumptions = assumps' })
      ret <- mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
-     modify (\st' -> st' { mrUVars = mrUVars st })
+     modify (\st' -> st' { mrUVars = mrUVars st,
+                           mrAssumptions = mrAssumptions st })
      return ret
 
 -- | Run a MR Solver computation in a context extended with a universal variable
@@ -1128,14 +1135,15 @@ genBVVecTerm sc n_tm len_tm a_tm f_tm =
     lambdaOpenTerm "_" (applyGlobalOpenTerm "Prelude.is_bvult" [n, i, len]) $ \_ ->
     applyOpenTerm f i]
 
--- | Match a term of the form @genBVVec n len a (\ i _ -> f i)@ and return @f@
-asGenBVVecTerm :: Recognizer Term Term
+-- | Match a term of the form @genBVVec n len a (\ i _ -> e)@, i.e., where @e@
+-- does not have the proof variable (the underscore) free
+asGenBVVecTerm :: Recognizer Term (Term, Term, Term, Term)
 asGenBVVecTerm (asApplyAll ->
                    (isGlobalDef "Prelude.genBVVec" -> Just _,
-                    [_, _, _,
-                     (asLambdaList -> ([_,_], asApp ->
-                                       Just (f, asLocalVar -> Just 1)))])) =
-  Just f
+                    [n, len, a,
+                     (asLambdaList -> ([_,_], e))]))
+  | not $ inBitSet 0 $ looseVars e
+  = Just (n, len, a, e)
 asGenBVVecTerm _ = Nothing
 
 type TmPrim = Prim TermModel
@@ -1149,11 +1157,18 @@ boolValToTerm _ (VExtra (VExtraTerm _tp tm)) = return tm
 boolValToTerm _ v = error ("boolValToTerm: unexpected value: " ++ show v)
 
 -- | An implementation of a primitive function that expects a @genBVVec@ term
-primGenBVVec :: (Term -> TmPrim) -> TmPrim
-primGenBVVec f =
+primGenBVVec :: SharedContext -> (Term -> TmPrim) -> TmPrim
+primGenBVVec sc f =
   PrimFilterFun "genBVVecPrim"
   (\case
-      VExtra (VExtraTerm _ (asGenBVVecTerm -> Just g)) -> return g
+      VExtra (VExtraTerm _ (asGenBVVecTerm -> Just (n, _, _, e))) ->
+        -- Generate the function \i -> [i/1,error/0]e
+        lift $
+        do i_tp <- scBoolType sc >>= scVecType sc n
+           let err_tm = error "primGenBVVec: unexpected variable occurrence"
+           i_tm <- scLocalVar sc 0
+           body <- instantiateVarList sc 0 [err_tm,i_tm] e
+           scLambda sc "i" i_tp body
       _ -> mzero)
   f
 
@@ -1184,7 +1199,7 @@ smtNormPrims sc = Map.fromList
 
     ("Prelude.atBVVec",
      PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a ->
-      primGenBVVec $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
+      primGenBVVec sc $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf ->
       Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix)
     )
   ]
@@ -1227,7 +1242,6 @@ mrProvable bool_tm =
          -- For variables of type BVVec, create a Vec n Bool -> a function as an
          -- ExtCns and apply genBVVec to it
          do
-           debugPrint 2 ("Is BVVec variable: " ++ show nm)
            ec_tp <-
              liftSC1 completeOpenTerm $
              arrowOpenTerm "_" (applyOpenTermMulti (globalOpenTerm "Prelude.Vec")
@@ -1236,7 +1250,6 @@ mrProvable bool_tm =
            ec <- liftSC2 scFreshEC nm ec_tp >>= liftSC1 scExtCns
            liftSC4 genBVVecTerm n len a ec
        tp' ->
-         debugPrint 2 ("Is not BVVec variable: " ++ show nm ++ " of type:") >>
          debugPrettyInCtx 2 tp' >>
          liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns
      normSMTProp prop_inst >>= mrProvableRaw
@@ -1258,21 +1271,47 @@ mrEq' (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
   liftSC3 scBvEq n t1 t2
 mrEq' _ _ _ = error "mrEq': unsupported type"
 
+-- | A 'Term' in an extended context of universal variables, which are listed
+-- "outside in", meaning the highest deBruijn index comes first
+data TermInCtx = TermInCtx [(LocalName,Term)] Term
+
+-- | Conjoin two 'TermInCtx's, assuming they both have Boolean type
+andTermInCtx :: TermInCtx -> TermInCtx -> MRM TermInCtx
+andTermInCtx (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) =
+  do
+    -- Insert the variables in ctx2 into the context of t1 starting at index 0,
+    -- by lifting its variables starting at 0 by length ctx2
+    t1' <- liftTermLike 0 (length ctx2) t1
+    -- Insert the variables in ctx1 into the context of t1 starting at index
+    -- length ctx2, by lifting its variables starting at length ctx2 by length
+    -- ctx1
+    t2' <- liftTermLike (length ctx2) (length ctx1) t2
+    TermInCtx (ctx1++ctx2) <$> liftSC2 scAnd t1' t2'
+
+-- | Extend the context of a 'TermInCtx' with additional universal variables
+-- bound "outside" the 'TermInCtx'
+extTermInCtx :: [(LocalName,Term)] -> TermInCtx -> TermInCtx
+extTermInCtx ctx (TermInCtx ctx' t) = TermInCtx (ctx++ctx') t
+
+-- | Run an 'MRM' computation in the context of a 'TermInCtx', passing in the
+-- 'Term'
+withTermInCtx :: TermInCtx -> (Term -> MRM a) -> MRM a
+withTermInCtx (TermInCtx [] tm) f = f tm
+withTermInCtx (TermInCtx ((nm,tp):ctx) tm) f =
+  withUVar nm (Type tp) $ const $ withTermInCtx (TermInCtx ctx tm) f
+
 -- | A "simple" strategy for proving equality between two terms, which we assume
 -- are of the same type, which builds an equality proposition by applying the
 -- supplied function to both sides and passes this proposition to an SMT solver.
-mrProveEqSimple :: (Term -> Term -> MRM Term) -> MRVarMap -> Term -> Term ->
-                   MRM ()
+mrProveEqSimple :: (Term -> Term -> MRM Term) -> Term -> Term ->
+                   MRM TermInCtx
 -- NOTE: The use of mrSubstEVars instead of mrSubstEVarsStrict means that we
 -- allow evars in the terms we send to the SMT solver, but we treat them as
 -- uvars.
-mrProveEqSimple eqf _ t1 t2 =
+mrProveEqSimple eqf t1 t2 =
   do t1' <- mrSubstEVars t1
      t2' <- mrSubstEVars t2
-     prop <- eqf t1' t2'
-     success <- mrProvable prop
-     if success then return () else
-       throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> eqf t1' t2'
 
 
 -- | Prove that two terms are equal, instantiating evars if necessary, or
@@ -1282,60 +1321,87 @@ mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
      tp <- mrTypeOf t1
      varmap <- mrVars <$> get
-     mrProveEqH varmap tp t1 t2
+     cond_in_ctx <- mrProveEqH varmap tp t1 t2
+     success <- withTermInCtx cond_in_ctx mrProvable
+     if success then return () else
+       throwError (TermsNotEq t1 t2)
 
+-- | The main workhorse for 'prProveEq'. Build a Boolean term expressing that
+-- the third and fourth arguments, whose type is given by the second. This is
+-- done in a continuation monad so that the output term can be in a context with
+-- additional universal variables.
+mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM TermInCtx
 
--- | The main workhorse for 'prProveEq'
-mrProveEqH :: Map MRVar MRVarInfo -> Term -> Term -> Term -> MRM ()
+{-
+mrProveEqH _ _ t1 t2
+  | trace ("mrProveEqH:\n" ++ showTerm t1 ++ "\n==\n" ++ showTerm t2) False = undefined
+-}
 
 -- If t1 is an instantiated evar, substitute and recurse
 mrProveEqH var_map tp (asEVarApp var_map -> Just (_, args, Just f)) t2 =
   mrApplyAll f args >>= \t1' -> mrProveEqH var_map tp t1' t2
 
 -- If t1 is an uninstantiated evar, instantiate it with t2
-mrProveEqH var_map _tp t1@(asEVarApp var_map -> Just (evar, args, Nothing)) t2 =
+mrProveEqH var_map _tp (asEVarApp var_map -> Just (evar, args, Nothing)) t2 =
   do t2' <- mrSubstEVars t2
      success <- mrTrySetAppliedEVar evar args t2'
-     if success then return () else throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> liftSC1 scBool success
 
 -- If t2 is an instantiated evar, substitute and recurse
 mrProveEqH var_map tp t1 (asEVarApp var_map -> Just (_, args, Just f)) =
   mrApplyAll f args >>= \t2' -> mrProveEqH var_map tp t1 t2'
 
 -- If t2 is an uninstantiated evar, instantiate it with t1
-mrProveEqH var_map _tp t1 t2@(asEVarApp var_map -> Just (evar, args, Nothing)) =
+mrProveEqH var_map _tp t1 (asEVarApp var_map -> Just (evar, args, Nothing)) =
   do t1' <- mrSubstEVars t1
      success <- mrTrySetAppliedEVar evar args t1'
-     if success then return () else throwError (TermsNotEq t1 t2)
+     TermInCtx [] <$> liftSC1 scBool success
 
 -- For the nat, bitvector, Boolean, and integer types, call mrProveEqSimple
-mrProveEqH var_map (asDataType -> Just (pn, [])) t1 t2
+mrProveEqH _ (asDataType -> Just (pn, [])) t1 t2
   | primName pn == "Prelude.Nat" =
-    mrProveEqSimple (liftSC2 scEqualNat) var_map t1 t2
-mrProveEqH var_map (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
+    mrProveEqSimple (liftSC2 scEqualNat) t1 t2
+mrProveEqH _ (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 =
   -- FIXME: make a better solver for bitvector equalities
-  mrProveEqSimple (liftSC3 scBvEq n) var_map t1 t2
-mrProveEqH var_map (asBoolType -> Just _) t1 t2 =
-  mrProveEqSimple (liftSC2 scBoolEq) var_map t1 t2
-mrProveEqH var_map (asIntegerType -> Just _) t1 t2 =
-  mrProveEqSimple (liftSC2 scIntEq) var_map t1 t2
+  mrProveEqSimple (liftSC3 scBvEq n) t1 t2
+mrProveEqH _ (asBoolType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scBoolEq) t1 t2
+mrProveEqH _ (asIntegerType -> Just _) t1 t2 =
+  mrProveEqSimple (liftSC2 scIntEq) t1 t2
+
+-- For pair types, prove both the left and right projections are equal
+mrProveEqH var_map (asPairType -> Just (tpL, tpR)) t1 t2 =
+  do t1L <- liftSC1 scPairLeft t1
+     t2L <- liftSC1 scPairLeft t2
+     t1R <- liftSC1 scPairRight t1
+     t2R <- liftSC1 scPairRight t2
+     condL <- mrProveEqH var_map tpL t1L t2L
+     condR <- mrProveEqH var_map tpR t1R t2R
+     andTermInCtx condL condR
 
 -- For non-bitvector vector types, prove all projections are equal by
 -- quantifying over a universal index variable and proving equality at that
 -- index
-mrProveEqH var_map (asBVVecType -> Just (n, len, tp)) t1 t2 =
-  withUVar "eq_ix" (Type tp) $ \ix ->
-  liftSC2 scGlobalApply "Prelude.is_bvult" [n, ix, len] >>= \pf_tp ->
-  withUVar "eq_pf" (Type pf_tp) $ \pf ->
-  do t1' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t1, ix, pf]
-     t2' <- liftSC2 scGlobalApply "Prelude.atBVVec" [n, len, tp, t2, ix, pf]
-     mrProveEqH var_map tp t1' t2'
+mrProveEqH _ (asBVVecType -> Just (n, len, tp)) t1 t2 =
+  liftSC0 scBoolType >>= \bool_tp ->
+  liftSC2 scVecType n bool_tp >>= \ix_tp ->
+  withUVarLift "eq_ix" (Type ix_tp) (n,(len,(tp,(t1,t2)))) $
+  \ix' (n',(len',(tp',(t1',t2')))) ->
+  liftSC2 scGlobalApply "Prelude.is_bvult" [n', ix', len'] >>= \pf_tp ->
+  withUVarLift "eq_pf" (Type pf_tp) (n',(len',(tp',(ix',(t1',t2'))))) $
+  \pf'' (n'',(len'',(tp'',(ix'',(t1'',t2''))))) ->
+  do t1_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n'', len'', tp'',
+                                                        t1'', ix'', pf'']
+     t2_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n'', len'', tp'',
+                                                        t2'', ix'', pf'']
+     var_map <- mrVars <$> get
+     extTermInCtx [("eq_ix",ix_tp),("eq_pf",pf_tp)] <$>
+       mrProveEqH var_map tp'' t1_prj t2_prj
 
 -- As a fallback, for types we can't handle, just check convertibility
 mrProveEqH _ _ t1 t2 =
-  mrConvertible t1 t2 >>= \case
-  True -> return ()
-  False -> throwError (TermsNotEq t1 t2)
+  do success <- mrConvertible t1 t2
+     TermInCtx [] <$> liftSC1 scBool success
 
 
 ----------------------------------------------------------------------

From 4fbc4c4d4139e43bf21fd805a9026e8cbd4a34f1 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 17:31:31 -0800
Subject: [PATCH 16/22] reordered some mrRefines cases; removed some unneeded
 debugging; changed variable instantiation in mrProvable to use the normalized
 types

---
 src/SAWScript/Prover/MRSolver.hs | 44 +++++++++++++++-----------------
 1 file changed, 21 insertions(+), 23 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index f05eb37aab..c3c25e3588 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -1249,9 +1249,7 @@ mrProvable bool_tm =
              (closedOpenTerm a)
            ec <- liftSC2 scFreshEC nm ec_tp >>= liftSC1 scExtCns
            liftSC4 genBVVecTerm n len a ec
-       tp' ->
-         debugPrettyInCtx 2 tp' >>
-         liftSC2 scFreshEC nm tp >>= liftSC1 scExtCns
+       tp' -> liftSC2 scFreshEC nm tp' >>= liftSC1 scExtCns
      normSMTProp prop_inst >>= mrProvableRaw
 
 -- | Build a Boolean 'Term' stating that two 'Term's are equal. This is like
@@ -1658,6 +1656,26 @@ mrRefines' (ReturnM e1) (ReturnM e2) = mrProveEq e1 e2
 mrRefines' (ErrorM _) (ErrorM _) = return ()
 mrRefines' (ReturnM e) (ErrorM _) = throwError (ReturnNotError e)
 mrRefines' (ErrorM _) (ReturnM e) = throwError (ReturnNotError e)
+mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
+  do cond <- mrEq' tp e1 e2
+     not_cond <- liftSC1 scNot cond
+     cond_pf <-
+       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
+     m1' <- applyNormCompFun f1 cond_pf
+     cond_holds <- mrProvable cond
+     if cond_holds then mrRefines m1' m2 else
+       withAssumption cond (mrRefines m1' m2) >>
+       withAssumption not_cond (mrRefines m1 m2)
+mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) =
+  do cond <- mrEq' tp e1 e2
+     not_cond <- liftSC1 scNot cond
+     cond_pf <-
+       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
+     m2' <- applyNormCompFun f2 cond_pf
+     cond_holds <- mrProvable cond
+     if cond_holds then mrRefines m1 m2' else
+       withAssumption cond (mrRefines m1 m2') >>
+       withAssumption not_cond (mrRefines m1 m2)
 mrRefines' (Ite cond1 m1 m1') m2_all@(Ite cond2 m2 m2') =
   liftSC1 scNot cond1 >>= \not_cond1 ->
   (mrEq cond1 cond2 >>= mrProvable) >>= \case
@@ -1679,26 +1697,6 @@ mrRefines' m1 (Ite cond2 m2 m2') =
   do not_cond2 <- liftSC1 scNot cond2
      withAssumption cond2 (mrRefines m1 m2)
      withAssumption not_cond2 (mrRefines m1 m2')
-mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 =
-  do cond <- mrEq' tp e1 e2
-     not_cond <- liftSC1 scNot cond
-     cond_pf <-
-       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
-     m1' <- applyNormCompFun f1 cond_pf
-     cond_holds <- mrProvable cond
-     if cond_holds then mrRefines m1' m2 else
-       withAssumption cond (mrRefines m1' m2) >>
-       withAssumption not_cond (mrRefines m1 m2)
-mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) =
-  do cond <- mrEq' tp e1 e2
-     not_cond <- liftSC1 scNot cond
-     cond_pf <-
-       liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm
-     m2' <- applyNormCompFun f2 cond_pf
-     cond_holds <- mrProvable cond
-     if cond_holds then mrRefines m1 m2' else
-       withAssumption cond (mrRefines m1 m2') >>
-       withAssumption not_cond (mrRefines m1 m2)
 -- FIXME: handle sum elimination
 -- mrRefines (Either f1 g1 e1) (Either f2 g2 e2) =
 mrRefines' m1 (ForallM tp f2) =

From 6c324e3340a179b02f54bd090cb0496ed1e273de Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 18 Feb 2022 18:37:39 -0800
Subject: [PATCH 17/22] bug fix in mrSetEVarClosed, to instantiate evars in the
 type of the evar being instantiated; trying to figure out why my
 uninterpreted functions do not work when passing them to the SMT solver...

---
 src/SAWScript/Prover/MRSolver.hs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index c3c25e3588..24eb831fd6 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -154,7 +154,7 @@ import Verifier.SAW.Simulator.TermModel
 import Verifier.SAW.Simulator.Prims
 import Verifier.SAW.Simulator.MonadLazy
 
-import SAWScript.Proof (termToProp, prettyProp)
+import SAWScript.Proof (termToProp, propToTerm, prettyProp)
 import qualified SAWScript.Prover.SBV as SBV
 
 -- import Debug.Trace
@@ -952,8 +952,11 @@ mrFreshEVars = helper [] where
 mrSetEVarClosed :: MRVar -> Term -> MRM ()
 mrSetEVarClosed var val =
   do val_tp <- mrTypeOf val
+     -- NOTE: need to instantiate any evars in the type of var, to ensure the
+     -- following subtyping check will succeed
+     var_tp <- mrSubstEVars $ mrVarType var
      -- FIXME: catch subtyping errors and report them as being evar failures
-     liftSC3 scCheckSubtype Nothing (TypedTerm val val_tp) (mrVarType var)
+     liftSC3 scCheckSubtype Nothing (TypedTerm val val_tp) var_tp
      modify $ \st ->
        st { mrVars =
             Map.alter
@@ -1223,7 +1226,8 @@ mrProvableRaw prop_term =
      prop <- liftSC1 termToProp prop_term
      debugPrint 2 ("Calling SMT solver with proposition: " ++
                    prettyProp defaultPPOpts prop)
-     (smt_res, _) <- liftSC4 SBV.proveUnintSBVIO smt_conf mempty timeout prop
+     unints <- Set.map ecVarIndex <$> getAllExtSet <$> liftSC1 propToTerm prop
+     (smt_res, _) <- liftSC4 SBV.proveUnintSBVIO smt_conf unints timeout prop
      case smt_res of
        Just _ ->
          debugPrint 2 "SMT solver response: not provable" >> return False

From 4916239a63b5129314ca73785cb704e01da4b5aa Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 21 Feb 2022 10:19:50 -0800
Subject: [PATCH 18/22] added MR solver test case for the arrays example

---
 heapster-saw/examples/arrays_mr_solver.saw | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 heapster-saw/examples/arrays_mr_solver.saw

diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw
new file mode 100644
index 0000000000..0229540028
--- /dev/null
+++ b/heapster-saw/examples/arrays_mr_solver.saw
@@ -0,0 +1,3 @@
+include "arrays.saw";
+contains0 <- parse_core_mod "arrays" "contains0";
+mr_solver_debug 2 contains0 contains0;

From 19280f4ccde8da3f43766e4257cbff43af91ce9b Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 21 Feb 2022 11:17:23 -0800
Subject: [PATCH 19/22] added a comment about withUVars being wrong

---
 src/SAWScript/Prover/MRSolver.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 24eb831fd6..5591ecff6a 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -805,6 +805,8 @@ withUVars = helper [] where
   helper :: [Term] -> [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a
   helper vars [] m = m $ reverse vars
   helper vars ((nm,tp):ctx) m =
+    -- FIXME: I think substituting here is wrong, but works on closed terms, so
+    -- it's fine to use at the top level at least...
     substTerm 0 vars tp >>= \tp' ->
     withUVarLift nm (Type tp') vars $ \var vars' -> helper (var:vars') ctx m
 

From 26fcc21b0c9272eae6f5180e58c3d6988bce5ab4 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 21 Feb 2022 12:27:33 -0800
Subject: [PATCH 20/22] changed MR Solver to use the What4 backend in place of
 SBV

---
 src/SAWScript/Builtins.hs        |  2 +-
 src/SAWScript/Prover/MRSolver.hs | 32 +++++++++++++++-----------------
 2 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 22e6c9c25c..22e4565920 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1562,7 +1562,7 @@ mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool
 mrSolver sc dlvl t1 t2 =
   do m1 <- ttTerm <$> ensureMonadicTerm sc t1
      m2 <- ttTerm <$> ensureMonadicTerm sc t2
-     res <- liftIO $ Prover.askMRSolver sc dlvl SBV.z3 Nothing m1 m2
+     res <- liftIO $ Prover.askMRSolver sc dlvl Nothing m1 m2
      case res of
        Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False
        Nothing -> return True
diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 5591ecff6a..b208a31dce 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -118,10 +118,7 @@ C |- F e1 ... en >>= k |= F' e1' ... em' >>= k':
 -}
 
 module SAWScript.Prover.MRSolver
-  (askMRSolver, MRFailure(..), showMRFailure, isCompFunType
-  , SBV.SMTConfig
-  , SBV.z3, SBV.cvc4, SBV.yices, SBV.mathSAT, SBV.boolector
-  ) where
+  (askMRSolver, MRFailure(..), showMRFailure, isCompFunType) where
 
 import Data.List (find, findIndex)
 import qualified Data.Text as T
@@ -155,7 +152,8 @@ import Verifier.SAW.Simulator.Prims
 import Verifier.SAW.Simulator.MonadLazy
 
 import SAWScript.Proof (termToProp, propToTerm, prettyProp)
-import qualified SAWScript.Prover.SBV as SBV
+import What4.Solver
+import SAWScript.Prover.What4
 
 -- import Debug.Trace
 
@@ -632,8 +630,6 @@ data FunAssump = FunAssump {
 data MRState = MRState {
   -- | Global shared context for building terms, etc.
   mrSC :: SharedContext,
-  -- | Global SMT configuration for the duration of the MR. Solver call
-  mrSMTConfig :: SBV.SMTConfig,
   -- | SMT timeout for SMT calls made by Mr. Solver
   mrSMTTimeout :: Maybe Integer,
   -- | The context of universal variables, which are free SAW core variables, in
@@ -653,11 +649,11 @@ data MRState = MRState {
 
 -- | Build a default, empty state from SMT configuration parameters and a set of
 -- function refinement assumptions
-mkMRState :: SharedContext -> Map FunName FunAssump -> SBV.SMTConfig ->
+mkMRState :: SharedContext -> Map FunName FunAssump ->
              Maybe Integer -> Int -> IO MRState
-mkMRState sc fun_assumps smt_config timeout dlvl =
+mkMRState sc fun_assumps timeout dlvl =
   scBool sc True >>= \true_tm ->
-  return $ MRState { mrSC = sc, mrSMTConfig = smt_config,
+  return $ MRState { mrSC = sc,
                      mrSMTTimeout = timeout, mrUVars = [], mrVars = Map.empty,
                      mrFunAssumps = fun_assumps, mrAssumptions = true_tm,
                      mrDebugLevel = dlvl }
@@ -1221,15 +1217,18 @@ normSMTProp t =
 -- | Test if a closed Boolean term is "provable", i.e., its negation is
 -- unsatisfiable, using an SMT solver. By "closed" we mean that it contains no
 -- uvars or 'MRVar's.
+--
+-- FIXME: use the timeout!
 mrProvableRaw :: Term -> MRM Bool
 mrProvableRaw prop_term =
-  do smt_conf <- mrSMTConfig <$> get
-     timeout <- mrSMTTimeout <$> get
+  do sc <- mrSC <$> get
      prop <- liftSC1 termToProp prop_term
+     unints <- Set.map ecVarIndex <$> getAllExtSet <$> liftSC1 propToTerm prop
      debugPrint 2 ("Calling SMT solver with proposition: " ++
                    prettyProp defaultPPOpts prop)
-     unints <- Set.map ecVarIndex <$> getAllExtSet <$> liftSC1 propToTerm prop
-     (smt_res, _) <- liftSC4 SBV.proveUnintSBVIO smt_conf unints timeout prop
+     sym <- liftIO $ setupWhat4_sym True
+     (smt_res, _) <-
+       liftIO $ proveWhat4_solver z3Adapter sym unints sc prop (return ())
      case smt_res of
        Just _ ->
          debugPrint 2 "SMT solver response: not provable" >> return False
@@ -1888,14 +1887,13 @@ mrRefinesFun _ _ = error "mrRefinesFun: unreachable!"
 askMRSolver ::
   SharedContext ->
   Int {- ^ The debug level -} ->
-  SBV.SMTConfig {- ^ SBV configuration -} ->
   Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} ->
   Term -> Term -> IO (Maybe MRFailure)
 
-askMRSolver sc dlvl smt_conf timeout t1 t2 =
+askMRSolver sc dlvl timeout t1 t2 =
   do tp1 <- scTypeOf sc t1 >>= scWhnf sc
      tp2 <- scTypeOf sc t2 >>= scWhnf sc
-     init_st <- mkMRState sc Map.empty smt_conf timeout dlvl
+     init_st <- mkMRState sc Map.empty timeout dlvl
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->
          fmap (either Just (const Nothing)) $ runMRM init_st $

From e4f94a1e17b4c72ac669851aad5d34710072136f Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 21 Feb 2022 15:43:31 -0800
Subject: [PATCH 21/22] lowered the debug level of arrays_mr_solver.saw to 1

---
 heapster-saw/examples/arrays_mr_solver.saw | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw
index 0229540028..0326bac2ec 100644
--- a/heapster-saw/examples/arrays_mr_solver.saw
+++ b/heapster-saw/examples/arrays_mr_solver.saw
@@ -1,3 +1,3 @@
 include "arrays.saw";
 contains0 <- parse_core_mod "arrays" "contains0";
-mr_solver_debug 2 contains0 contains0;
+mr_solver_debug 1 contains0 contains0;

From 8d0aa64b19c5313f84ec5ecb3a0b6f66101cdfa4 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Mon, 21 Feb 2022 19:10:36 -0500
Subject: [PATCH 22/22] fix typo in definition of `liftSC5`

---
 src/SAWScript/Prover/MRSolver.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index b208a31dce..f828ee69a1 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -719,7 +719,7 @@ liftSC4 :: (SharedContext -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d ->
            MRM e
 liftSC4 f a b c d = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d)
 
--- | Lift a quaternary SharedTerm computation into 'MRM'
+-- | Lift a quinary SharedTerm computation into 'MRM'
 liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) ->
            a -> b -> c -> d -> e -> MRM f
 liftSC5 f a b c d e = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d e)