From 3a9fb918d9c63532bb4d869d300a5e6541b3e1c1 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 4 Mar 2022 12:34:59 -0800
Subject: [PATCH 01/15] added preconditions to Mr Solver

---
 src/SAWScript/Builtins.hs               | 29 ++++++++-
 src/SAWScript/Interpreter.hs            |  7 +++
 src/SAWScript/Prover/MRSolver.hs        |  3 +-
 src/SAWScript/Prover/MRSolver/Monad.hs  | 80 +++++++++++++++++++++----
 src/SAWScript/Prover/MRSolver/Solver.hs | 55 +++++++++++++----
 src/SAWScript/Value.hs                  |  2 +
 6 files changed, 147 insertions(+), 29 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 9454f86a72..a95569d946 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -71,6 +71,7 @@ import Verifier.SAW.SATQuery
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
 import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
 import Verifier.SAW.SharedTerm
+import Verifier.SAW.Recognizer
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import Verifier.SAW.Prim (rethrowEvalError)
@@ -1560,15 +1561,39 @@ ensureMonadicTerm sc t
       False -> monadifyTypedTerm sc t
 ensureMonadicTerm sc t = monadifyTypedTerm sc t
 
+-- | Run Mr Solver with the given debug level to prove that the first term
+-- refines the second
 mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool
 mrSolver sc dlvl t1 t2 =
-  do m1 <- ttTerm <$> ensureMonadicTerm sc t1
+  do rw <- get
+     m1 <- ttTerm <$> ensureMonadicTerm sc t1
      m2 <- ttTerm <$> ensureMonadicTerm sc t2
-     res <- liftIO $ Prover.askMRSolver sc dlvl Nothing m1 m2
+     let env = rwMRSolverEnv rw
+     res <- liftIO $ Prover.askMRSolver sc dlvl env Nothing m1 m2
      case res of
        Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False
        Nothing -> return True
 
+-- | Set the precondition for a named function, given as a SAW core term
+mrSolverSetPrecond :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel ()
+mrSolverSetPrecond sc f pre =
+  do rw <- get
+     f_mon <- ttTerm <$> ensureMonadicTerm sc f
+     gdef <- case Monadify.asTypedGlobalDef f_mon of
+       Just gdef -> return gdef
+       Nothing -> fail "mr_solver_set_precond: Not an identifier"
+     -- NOTE: do not monadify pre, as it is supposed to be pure
+     (asPiList -> (f_args, _)) <- io $ scTypeOf sc f_mon
+     pre_tp <- io (scTypeOf sc $ ttTerm pre)
+     pre_tp_req <- io (scBoolType sc >>= scPiList sc f_args)
+     correct_tp <- io (scConvertible sc True pre_tp pre_tp_req)
+     if correct_tp then return () else
+       fail ("mr_solver_set_precond: incorrect type for precondition\n" ++
+             "Expected: " ++ showTerm pre_tp_req ++ "\n" ++
+             "Actual: " ++ showTerm pre_tp)
+     let env = rwMRSolverEnv rw
+     put (rw { rwMRSolverEnv = Prover.mrEnvAddPrecond gdef (ttTerm pre) env })
+
 setMonadification :: SharedContext -> String -> String -> TopLevel ()
 setMonadification sc cry_str saw_str =
   do rw <- get
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index e53db153db..114ea7f32d 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -67,6 +67,7 @@ import SAWScript.Value
 import SAWScript.Proof (newTheoremDB)
 import SAWScript.Prover.Rewrite(basic_ss)
 import SAWScript.Prover.Exporter
+import SAWScript.Prover.MRSolver (emptyMREnv)
 import Verifier.SAW.Conversion
 --import Verifier.SAW.PrettySExp
 import Verifier.SAW.Prim (rethrowEvalError)
@@ -474,6 +475,7 @@ buildTopLevelEnv proxy opts =
                    , rwDocs       = primDocEnv primsAvail
                    , rwCryptol    = ce0
                    , rwMonadify   = Monadify.defaultMonEnv
+                   , rwMRSolverEnv = emptyMREnv
                    , rwProofs     = []
                    , rwPPOpts     = SAWScript.Value.defaultPPOpts
                    , rwJVMTrans   = jvmTrans
@@ -3167,6 +3169,11 @@ primitives = Map.fromList
     Experimental
     [ "Call the monadic-recursive solver at the supplied debug level" ]
 
+  , prim "mr_solver_set_precond"  "Term -> Term -> TopLevel ()"
+    (scVal mrSolverSetPrecond)
+    Experimental
+    [ "Set the precondition for use in Mr Solver of a function to a function" ]
+
   , prim "monadify_term" "Term -> TopLevel Term"
     (scVal monadifyTypedTerm)
     Experimental
diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 856f94a5a7..fb2589766d 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -9,7 +9,8 @@ Portability : non-portable (language extensions)
 -}
 
 module SAWScript.Prover.MRSolver
-  (askMRSolver, MRFailure(..), showMRFailure, isCompFunType) where
+  (askMRSolver, MRFailure(..), showMRFailure, isCompFunType,
+   MREnv(..), emptyMREnv, mrEnvAddPrecond) where
 
 import SAWScript.Prover.MRSolver.Term
 import SAWScript.Prover.MRSolver.Monad
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index b5e4526a3c..a379a3d0ef 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -73,6 +73,7 @@ data MRFailure
   | MalformedDefsFun Term
   | MalformedComp Term
   | NotCompFunType Term
+  | PrecondNotProvable FunName FunName Term
     -- | A local variable binding
   | MRFailureLocalVar LocalName MRFailure
     -- | Information about the context of the failure
@@ -129,6 +130,10 @@ instance PrettyInCtx MRFailure where
     ppWithPrefix "Could not handle computation:" t
   prettyInCtx (NotCompFunType tp) =
     ppWithPrefix "Not a computation or computational function type:" tp
+  prettyInCtx (PrecondNotProvable f g pre) =
+    prettyAppList [return "Could not prove precondition for functions",
+                   prettyInCtx f, return "and", prettyInCtx g,
+                   return ":", prettyInCtx pre]
   prettyInCtx (MRFailureLocalVar x err) =
     local (x:) $ prettyInCtx err
   prettyInCtx (MRFailureCtx ctx err) =
@@ -189,23 +194,31 @@ data CoIndHyp = CoIndHyp {
   -- | The LHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
   coIndHypLHS :: [Term],
   -- | The RHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
-  coIndHypRHS :: [Term]
+  coIndHypRHS :: [Term],
+  -- | The precondition for the left-hand arguments, as a closed function from
+  -- the left-hand arguments to @Bool@
+  coIndHypPrecondLHS :: Term,
+  -- | The precondition for the right-hand arguments, as a closed function from
+  -- the left-hand arguments to @Bool@
+  coIndHypPrecondRHS :: Term
 } deriving Show
 
 -- | Extract the @i@th argument on either the left- or right-hand side of a
 -- coinductive hypothesis
 coIndHypArg :: CoIndHyp -> Either Int Int -> Term
-coIndHypArg (CoIndHyp _ _ _ args1 _) (Left i) = args1 !! i
-coIndHypArg (CoIndHyp _ _ _ _ args2) (Right i) = args2 !! i
+coIndHypArg hyp (Left i) = (coIndHypLHS hyp) !! i
+coIndHypArg hyp (Right i) = (coIndHypRHS hyp) !! i
 
 -- | A map from pairs of function names to co-inductive hypotheses over those
 -- names
 type CoIndHyps = Map (FunName, FunName) CoIndHyp
 
 instance PrettyInCtx CoIndHyp where
-  prettyInCtx (CoIndHyp ctx f1 f2 args1 args2) =
+  prettyInCtx (CoIndHyp ctx f1 f2 args1 args2 pre1 pre2) =
     local (const $ map fst $ reverse ctx) $
     prettyAppList [return (ppCtx ctx <> "."),
+                   prettyTermApp pre1 args1, return "=>",
+                   prettyTermApp pre2 args2, return "=>",
                    prettyInCtx (FunBind f1 args1 CompFunReturn),
                    return "|=",
                    prettyInCtx (FunBind f2 args2 CompFunReturn)]
@@ -231,6 +244,8 @@ data FunAssump = FunAssump {
 
 -- | A map from function names to function refinement assumptions over that
 -- name
+--
+-- FIXME: this should probably be an 'IntMap' on the 'VarIndex' of globals
 type FunAssumps = Map FunName FunAssump
 
 -- | An assumption that something is equal to one of the constructors of a
@@ -252,6 +267,26 @@ asEither _ = Nothing
 -- | A map from 'Term's to 'DataTypeAssump's over that term
 type DataTypeAssumps = HashMap Term DataTypeAssump
 
+-- | A global MR Solver environment
+data MREnv = MREnv {
+  -- | The set of function refinements to be assumed by to Mr. Solver (which
+  -- have hopefully been proved previously...)
+  mreFunAssumps :: FunAssumps,
+  -- | The preconditions associated with functions by the user
+  mrePreconditions :: Map FunName Term
+  }
+
+-- | The empty 'MREnv'
+emptyMREnv :: MREnv
+emptyMREnv = MREnv { mreFunAssumps = Map.empty,
+                     mrePreconditions = Map.empty }
+
+-- | Add a precondition to an 'MREnv'
+mrEnvAddPrecond :: GlobalDef -> Term -> MREnv -> MREnv
+mrEnvAddPrecond gdef pre env =
+  env { mrePreconditions =
+          Map.insert (GlobalName gdef []) pre (mrePreconditions env) }
+
 -- | Parameters and locals for MR. Solver
 data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
@@ -262,8 +297,8 @@ data MRInfo = MRInfo {
   -- variables, in order from innermost to outermost, i.e., where element @0@
   -- corresponds to deBruijn index @0@
   mriUVars :: [(LocalName,Type)],
-  -- | The set of function refinements to be assumed by to Mr. Solver
-  mriFunAssumps :: FunAssumps,
+  -- | The top-level Mr Solver environment
+  mriEnv :: MREnv,
   -- | The current set of co-inductive hypotheses
   mriCoIndHyps :: CoIndHyps,
   -- | The current assumptions, which are conjoined into a single Boolean term;
@@ -314,9 +349,9 @@ mrSMTTimeout = mriSMTTimeout <$> ask
 mrUVars :: MRM [(LocalName,Type)]
 mrUVars = mriUVars <$> ask
 
--- | Get the current value of 'mriFunAssumps'
+-- | Get the current function assumptions
 mrFunAssumps :: MRM FunAssumps
-mrFunAssumps = mriFunAssumps <$> ask
+mrFunAssumps = mreFunAssumps <$> mriEnv <$> ask
 
 -- | Get the current value of 'mriCoIndHyps'
 mrCoIndHyps :: MRM CoIndHyps
@@ -339,12 +374,12 @@ mrVars :: MRM MRVarMap
 mrVars = mrsVars <$> get
 
 -- | Run an 'MRM' computation and return a result or an error
-runMRM :: SharedContext -> Maybe Integer -> Int -> FunAssumps ->
+runMRM :: SharedContext -> Maybe Integer -> Int -> MREnv ->
           MRM a -> IO (Either MRFailure a)
-runMRM sc timeout debug assumps m =
+runMRM sc timeout debug env m =
   do true_tm <- scBool sc True
      let init_info = MRInfo { mriSC = sc, mriSMTTimeout = timeout,
-                              mriDebugLevel = debug, mriFunAssumps = assumps,
+                              mriDebugLevel = debug, mriEnv = env,
                               mriUVars = [], mriCoIndHyps = Map.empty,
                               mriAssumptions = true_tm,
                               mriDataTypeAssumps = HashMap.empty }
@@ -473,6 +508,7 @@ mrTypeOf :: Term -> MRM Term
 mrTypeOf t =
   -- NOTE: scTypeOf' wants the type context in the most recently bound var
   -- first, i.e., in the mrUVarCtxRev order
+  mrDebugPPPrefix 2 "mrTypeOf:" t >>
   mrUVarCtxRev >>= \ctx -> liftSC2 scTypeOf' (map snd ctx) t
 
 -- | Check if two 'Term's are convertible in the 'MRM' monad
@@ -792,7 +828,7 @@ mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 -- | Run a compuation under an additional co-inductive assumption
 withCoIndHypRaw :: CoIndHyp -> MRM a -> MRM a
 withCoIndHypRaw hyp m =
-  do debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
+  do debugPretty 2 ("withCoIndHypRaw" <+> ppInEmptyCtx hyp)
      hyps' <- Map.insert (coIndHypLHSFun hyp,
                           coIndHypRHSFun hyp) hyp <$> mrCoIndHyps
      local (\info -> info { mriCoIndHyps = hyps' }) m
@@ -820,7 +856,9 @@ withFunAssump fname args rhs m =
      ctx <- mrUVarCtx
      assumps <- mrFunAssumps
      let assumps' = Map.insert fname (FunAssump ctx args rhs) assumps
-     local (\info -> info { mriFunAssumps = assumps' }) m
+     local (\info ->
+             let env' = (mriEnv info) { mreFunAssumps = assumps' } in
+             info { mriEnv = env' }) m
 
 -- | Generate fresh evars for the context of a 'FunAssump' and substitute them
 -- into its arguments and right-hand side
@@ -831,6 +869,16 @@ instantiateFunAssump fassump =
      rhs <- substTermLike 0 evars $ fassumpRHS fassump
      return (args, rhs)
 
+-- | Look up the precondition associated with a function name, returning the
+-- trivial @True@ one if there is none
+mrGetPrecond :: FunName -> MRM Term
+mrGetPrecond nm =
+  (Map.lookup nm <$> mrePreconditions <$> mriEnv <$> ask) >>= \case
+  Just t -> return t
+  Nothing ->
+    do (nm_args, _) <- asPiList <$> funNameType nm
+       liftSC1 scBool True >>= liftSC2 scPiList nm_args
+
 -- | Add an assumption of type @Bool@ to the current path condition while
 -- executing a sub-computation
 withAssumption :: Term -> MRM a -> MRM a
@@ -840,6 +888,12 @@ withAssumption phi m =
      assumps' <- liftSC2 scAnd phi assumps
      local (\info -> info { mriAssumptions = assumps' }) m
 
+-- | Remove any existing assumptions and replace them with a Boolean term
+withOnlyAssumption :: Term -> MRM a -> MRM a
+withOnlyAssumption phi m =
+  do mrDebugPPPrefix 1 "withOnlyAssumption" phi
+     local (\info -> info { mriAssumptions = phi }) m
+
 -- | Add a 'DataTypeAssump' to the current context while executing a
 -- sub-computations
 withDataTypeAssump :: Term -> DataTypeAssump -> MRM a -> MRM a
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 8f25dc5d72..6c18e9f253 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -117,7 +117,8 @@ module SAWScript.Prover.MRSolver.Solver where
 import Data.Either
 import Data.List (findIndices, intercalate)
 import Control.Monad.Except
-import qualified Data.Map as Map
+
+import Prettyprinter
 
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.SharedTerm
@@ -345,17 +346,42 @@ handling the recursive ones
 -- * Handling Coinductive Hypotheses
 ----------------------------------------------------------------------
 
--- | Run a compuation under the additional co-inductive assumption that
--- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are
--- the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@ are the given
--- argument lists, and @x1, ..., xn@ is the current context of uvars. If
--- while running the given computation a 'CoIndHypMismatchWidened' error is
--- reached with the given names, the state is restored and the computation is
--- re-run with the widened hypothesis.
+-- | Prove the precondition of a coinductive hypothesis applied to the given
+-- left- and right-hand arguments
+proveCoIndHypPreCond :: CoIndHyp -> [Term] -> [Term] -> MRM ()
+proveCoIndHypPreCond hyp args1 args2 =
+  do pre1 <- liftSC2 scApplyAll (coIndHypPrecondLHS hyp) args1
+     pre2 <- liftSC2 scApplyAll (coIndHypPrecondRHS hyp) args2
+     -- FIXME: pre is just for printing / debugging purposes...
+     pre <- liftSC2 scAnd pre1 pre2
+     success <- liftSC2 scAnd pre1 pre2 >>= mrProvable
+     if success then return () else
+       throwMRFailure $
+       PrecondNotProvable (coIndHypLHSFun hyp) (coIndHypRHSFun hyp) pre
+
+-- | Run a compuation @m@ under the additional co-inductive assumption that
+--
+-- > forall x1, ..., xn. preF y1 ... ym -> preG z1 ... zl ->
+-- >   F y1 ... ym |= G z1 ... zl@
+--
+-- where @F@ and @G@ are the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@
+-- are the given argument lists, @x1, ..., xn@ is the current context of uvars,
+-- and @preF@ and @preG@ are the preconditions associated with @F@ and @G@,
+-- respectively. Note that @m@ is run with /only/ these preconditions as
+-- assumptions; all other assumptions are thrown away. If while running the
+-- given computation a 'CoIndHypMismatchWidened' error is reached with the given
+-- names, the state is restored and the computation is re-run with the widened
+-- hypothesis.
 withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
 withCoIndHyp f1 args1 f2 args2 m =
   do ctx <- mrUVarCtx
-     withCoIndHyp' (CoIndHyp ctx f1 f2 args1 args2) m
+     pre1 <- mrGetPrecond f1
+     pre2 <- mrGetPrecond f2
+     pre <- liftSC2 scAnd pre1 pre2
+     let hyp = CoIndHyp ctx f1 f2 args1 args2 pre1 pre2
+     debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
+     proveCoIndHypPreCond hyp args1 args2
+     withOnlyAssumption pre $ withCoIndHyp' hyp m
 
 -- | The main loop of 'withCoIndHyp'
 withCoIndHyp' :: CoIndHyp -> MRM a -> MRM a
@@ -382,6 +408,8 @@ matchCoIndHyp hyp args1 args2 =
      if and (eqs1 ++ eqs2) then return () else
        throwError $ MRExnWiden (coIndHypLHSFun hyp) (coIndHypRHSFun hyp)
        (map Left (findIndices not eqs1) ++ map Right (findIndices not eqs2))
+     proveCoIndHypPreCond hyp args1 args2
+
 
 -- | Generalize some of the arguments of a coinductive hypothesis
 generalizeCoIndHyp :: CoIndHyp -> [Either Int Int] -> MRM CoIndHyp
@@ -412,7 +440,7 @@ generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) =
 -- | Add a new variable of the given type to the context of a coinductive
 -- hypothesis and set the specified arguments to that new variable
 generalizeCoIndHypArgs :: CoIndHyp -> Term -> [Either Int Int] -> MRM CoIndHyp
-generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2) tp specs =
+generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2 pre1 pre2) tp specs =
   do let set_arg i args =
            take i args ++ (Unshared $ LocalVar 0) : drop (i+1) args
      let (specs1, specs2) = partitionEithers specs
@@ -421,7 +449,7 @@ generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2) tp specs =
      args2' <- liftTermLike 0 1 args2
      let args1'' = foldr set_arg args1' specs1
          args2'' = foldr set_arg args2' specs2
-     return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2''
+     return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2'' pre1 pre2
 
 
 ----------------------------------------------------------------------
@@ -726,16 +754,17 @@ mrRefinesFun _ _ = error "mrRefinesFun: unreachable!"
 askMRSolver ::
   SharedContext ->
   Int {- ^ The debug level -} ->
+  MREnv {- ^ The Mr Solver environment -} ->
   Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} ->
   Term -> Term -> IO (Maybe MRFailure)
 
-askMRSolver sc dlvl timeout t1 t2 =
+askMRSolver sc dlvl env timeout t1 t2 =
   do tp1 <- scTypeOf sc t1 >>= scWhnf sc
      tp2 <- scTypeOf sc t2 >>= scWhnf sc
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->
          fmap (either Just (const Nothing)) $
-         runMRM sc timeout dlvl Map.empty $
+         runMRM sc timeout dlvl env $
          withUVars uvar_ctx $ \vars ->
          do tps_are_eq <- mrConvertible tp1 tp2
             if tps_are_eq then return () else
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index ca1eac5f59..8e0e40bb2b 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -76,6 +76,7 @@ import SAWScript.JavaPretty (prettyClass)
 import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity)
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
+import SAWScript.Prover.MRSolver.Monad as MRSolver
 import SAWScript.Crucible.LLVM.Skeleton
 import SAWScript.X86 (X86Unsupported(..), X86Error(..))
 
@@ -431,6 +432,7 @@ data TopLevelRW =
   , rwDocs    :: Map SS.Name String
   , rwCryptol :: CEnv.CryptolEnv
   , rwMonadify :: Monadify.MonadifyEnv
+  , rwMRSolverEnv :: MRSolver.MREnv
   , rwProofs  :: [Value] {- ^ Values, generated anywhere, that represent proofs. -}
   , rwPPOpts  :: PPOpts
   -- , rwCrucibleLLVMCtx :: Crucible.LLVMContext

From 5352afbd8ff728110a2e099c5f5a5670283a85bc Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 4 Mar 2022 18:11:08 -0800
Subject: [PATCH 02/15] changed how preconditions work so that they are given
 with a precondHint in the spec rather than with a separate
 mr_solver_set_precond command

---
 saw-core/prelude/Prelude.sawcore        |  4 ++
 src/SAWScript/Prover/MRSolver/Monad.hs  | 65 +++++++++++++----
 src/SAWScript/Prover/MRSolver/Solver.hs | 93 ++++++++++++++-----------
 3 files changed, 106 insertions(+), 56 deletions(-)

diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 7b0676ff67..43cdafd843 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -2158,6 +2158,10 @@ orM a m1 m2 = existsM Bool a (\ (b:Bool) -> ite (CompM a) b m1 m2);
 -- those computations diverge from each other.
 primitive forallM : (a b:sort 0) -> (a -> CompM b) -> CompM b;
 
+-- A hint to Mr Solver that a recursive function has the given precondition
+precondHint : (a : sort 0) -> Bool -> a -> a;
+precondHint _ _ a = a;
+
 -- NOTE: for the simplicity and efficiency of MR solver, we define all
 -- fixed-point computations in CompM via a primitive multiFixM, defined below.
 -- Thus, even though fixM is really the primitive operation, we write this file
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index a379a3d0ef..af462235be 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -197,10 +197,10 @@ data CoIndHyp = CoIndHyp {
   coIndHypRHS :: [Term],
   -- | The precondition for the left-hand arguments, as a closed function from
   -- the left-hand arguments to @Bool@
-  coIndHypPrecondLHS :: Term,
+  coIndHypPrecondLHS :: Maybe Term,
   -- | The precondition for the right-hand arguments, as a closed function from
   -- the left-hand arguments to @Bool@
-  coIndHypPrecondRHS :: Term
+  coIndHypPrecondRHS :: Maybe Term
 } deriving Show
 
 -- | Extract the @i@th argument on either the left- or right-hand side of a
@@ -217,8 +217,12 @@ instance PrettyInCtx CoIndHyp where
   prettyInCtx (CoIndHyp ctx f1 f2 args1 args2 pre1 pre2) =
     local (const $ map fst $ reverse ctx) $
     prettyAppList [return (ppCtx ctx <> "."),
-                   prettyTermApp pre1 args1, return "=>",
-                   prettyTermApp pre2 args2, return "=>",
+                   (case pre1 of
+                       Just f -> prettyTermApp f args1
+                       Nothing -> return "True"), return "=>",
+                   (case pre2 of
+                       Just f -> prettyTermApp f args2
+                       Nothing -> return "True"), return "=>",
                    prettyInCtx (FunBind f1 args1 CompFunReturn),
                    return "|=",
                    prettyInCtx (FunBind f2 args2 CompFunReturn)]
@@ -267,6 +271,8 @@ asEither _ = Nothing
 -- | A map from 'Term's to 'DataTypeAssump's over that term
 type DataTypeAssumps = HashMap Term DataTypeAssump
 
+-- FIXME HERE NOW: remove preconditions from MREnv
+
 -- | A global MR Solver environment
 data MREnv = MREnv {
   -- | The set of function refinements to be assumed by to Mr. Solver (which
@@ -826,8 +832,8 @@ mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
 mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 
 -- | Run a compuation under an additional co-inductive assumption
-withCoIndHypRaw :: CoIndHyp -> MRM a -> MRM a
-withCoIndHypRaw hyp m =
+withCoIndHyp :: CoIndHyp -> MRM a -> MRM a
+withCoIndHyp hyp m =
   do debugPretty 2 ("withCoIndHypRaw" <+> ppInEmptyCtx hyp)
      hyps' <- Map.insert (coIndHypLHSFun hyp,
                           coIndHypRHSFun hyp) hyp <$> mrCoIndHyps
@@ -842,6 +848,25 @@ instantiateCoIndHyp (CoIndHyp {..}) =
      rhs <- substTermLike 0 evars coIndHypRHS
      return (lhs, rhs)
 
+-- | Apply the preconditions of a 'CoIndHyp' to their respective arguments,
+-- yielding @Bool@ conditions, using the constant @True@ value when a
+-- precondition is absent
+applyCoIndHypPreconds :: CoIndHyp -> MRM (Term, Term)
+applyCoIndHypPreconds hyp =
+  let apply_precond :: Maybe Term -> [Term] -> MRM Term
+      apply_precond (Just (asLambdaList -> (vars, phi))) args
+        | length vars == length args
+          -- NOTE: applying to a list of arguments == substituting the reverse
+          -- of that list, because the first argument corresponds to the
+          -- greatest deBruijn index
+        = substTerm 0 (reverse args) phi
+      apply_precond (Just _) _ =
+        error "applyCoIndHypPreconds: wrong number of arguments for precondition!"
+      apply_precond Nothing _ = liftSC1 scBool True in
+  do pre1 <- apply_precond (coIndHypPrecondLHS hyp) (coIndHypLHS hyp)
+     pre2 <- apply_precond (coIndHypPrecondRHS hyp) (coIndHypRHS hyp)
+     return (pre1, pre2)
+
 -- | Look up the 'FunAssump' for a 'FunName', if there is one
 mrGetFunAssump :: FunName -> MRM (Maybe FunAssump)
 mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps
@@ -869,15 +894,27 @@ instantiateFunAssump fassump =
      rhs <- substTermLike 0 evars $ fassumpRHS fassump
      return (args, rhs)
 
--- | Look up the precondition associated with a function name, returning the
--- trivial @True@ one if there is none
-mrGetPrecond :: FunName -> MRM Term
+-- FIXME HERE NOW: delete this and remove the preconditions from the env
+-- | Look up the precondition associated with a function name, if there is one
+-- mrLookupPrecond :: FunName -> MRM (Maybe Term)
+-- mrLookupPrecond nm = Map.lookup nm <$> mrePreconditions <$> mriEnv <$> ask
+
+-- | Get the precondition hint associated with a function name, by unfolding the
+-- name and checking if its body has the form
+--
+-- > \ x1 ... xn -> precondHint a phi m
+--
+-- If so, return @\ x1 ... xn -> phi@ as a term with the @xi@ variables free.
+-- Otherwise, return 'Nothing'.
+mrGetPrecond :: FunName -> MRM (Maybe Term)
 mrGetPrecond nm =
-  (Map.lookup nm <$> mrePreconditions <$> mriEnv <$> ask) >>= \case
-  Just t -> return t
-  Nothing ->
-    do (nm_args, _) <- asPiList <$> funNameType nm
-       liftSC1 scBool True >>= liftSC2 scPiList nm_args
+  mrFunNameBody nm >>= \case
+  Just (asLambdaList ->
+        (args,
+         asApplyAll -> (isGlobalDef "Prelude.precondHint" -> Just (),
+                        [_, phi, _]))) ->
+    Just <$> liftSC2 scLambdaList args phi
+  _ -> return Nothing
 
 -- | Add an assumption of type @Bool@ to the current path condition while
 -- executing a sub-computation
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 6c18e9f253..df12b04b77 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -114,6 +114,7 @@ C |- F e1 ... en >>= k |= F' e1' ... em' >>= k':
 
 module SAWScript.Prover.MRSolver.Solver where
 
+import Data.Maybe
 import Data.Either
 import Data.List (findIndices, intercalate)
 import Control.Monad.Except
@@ -346,20 +347,17 @@ handling the recursive ones
 -- * Handling Coinductive Hypotheses
 ----------------------------------------------------------------------
 
--- | Prove the precondition of a coinductive hypothesis applied to the given
--- left- and right-hand arguments
-proveCoIndHypPreCond :: CoIndHyp -> [Term] -> [Term] -> MRM ()
-proveCoIndHypPreCond hyp args1 args2 =
-  do pre1 <- liftSC2 scApplyAll (coIndHypPrecondLHS hyp) args1
-     pre2 <- liftSC2 scApplyAll (coIndHypPrecondRHS hyp) args2
-     -- FIXME: pre is just for printing / debugging purposes...
+-- | Prove the precondition of a coinductive hypothesis
+proveCoIndHypPreCond :: CoIndHyp -> MRM ()
+proveCoIndHypPreCond hyp =
+  do (pre1, pre2) <- applyCoIndHypPreconds hyp
      pre <- liftSC2 scAnd pre1 pre2
-     success <- liftSC2 scAnd pre1 pre2 >>= mrProvable
+     success <- mrProvable pre
      if success then return () else
        throwMRFailure $
        PrecondNotProvable (coIndHypLHSFun hyp) (coIndHypRHSFun hyp) pre
 
--- | Run a compuation @m@ under the additional co-inductive assumption that
+-- | Co-inductively prove the refinement
 --
 -- > forall x1, ..., xn. preF y1 ... ym -> preG z1 ... zl ->
 -- >   F y1 ... ym |= G z1 ... zl@
@@ -367,35 +365,47 @@ proveCoIndHypPreCond hyp args1 args2 =
 -- where @F@ and @G@ are the given 'FunName's, @y1, ..., ym@ and @z1, ..., zl@
 -- are the given argument lists, @x1, ..., xn@ is the current context of uvars,
 -- and @preF@ and @preG@ are the preconditions associated with @F@ and @G@,
--- respectively. Note that @m@ is run with /only/ these preconditions as
--- assumptions; all other assumptions are thrown away. If while running the
--- given computation a 'CoIndHypMismatchWidened' error is reached with the given
--- names, the state is restored and the computation is re-run with the widened
--- hypothesis.
-withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
-withCoIndHyp f1 args1 f2 args2 m =
+-- respectively. This proof is performed by coinductively assuming the
+-- refinement holds and proving the refinement with the definitions of @F@ and
+-- @G@ unfolded to their bodies. Note that this refinement is performed with
+-- /only/ the preconditions @preF@ and @preG@ as assumptions; all other
+-- assumptions are thrown away. If while running the refinement computation a
+-- 'CoIndHypMismatchWidened' error is reached with the given names, the state is
+-- restored and the computation is re-run with the widened hypothesis.
+mrRefinesCoInd :: FunName -> [Term] -> FunName -> [Term] -> MRM ()
+mrRefinesCoInd f1 args1 f2 args2 =
   do ctx <- mrUVarCtx
-     pre1 <- mrGetPrecond f1
-     pre2 <- mrGetPrecond f2
+     preF1 <- mrGetPrecond f1
+     preF2 <- mrGetPrecond f2
+     let hyp = CoIndHyp ctx f1 f2 args1 args2 preF1 preF2
+     proveCoIndHypPreCond hyp
+     proveCoIndHyp hyp
+
+-- | Prove the refinement represented by a 'CoIndHyp' coinductively. This is the
+-- main loop implementing 'mrRefinesCoInd'. See that function for documentation.
+proveCoIndHyp :: CoIndHyp -> MRM ()
+proveCoIndHyp hyp =
+  do let f1 = coIndHypLHSFun hyp
+         f2 = coIndHypRHSFun hyp
+         args1 = coIndHypLHS hyp
+         args2 = coIndHypRHS hyp
+     debugPretty 1 ("proveCoIndHyp" <+> ppInEmptyCtx hyp)
+     lhs <- fromMaybe (error "proveCoIndHyp") <$> mrFunBody f1 args1
+     rhs <- fromMaybe (error "proveCoIndHyp") <$> mrFunBody f2 args2
+     (pre1, pre2) <- applyCoIndHypPreconds hyp
      pre <- liftSC2 scAnd pre1 pre2
-     let hyp = CoIndHyp ctx f1 f2 args1 args2 pre1 pre2
-     debugPretty 1 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
-     proveCoIndHypPreCond hyp args1 args2
-     withOnlyAssumption pre $ withCoIndHyp' hyp m
-
--- | The main loop of 'withCoIndHyp'
-withCoIndHyp' :: CoIndHyp -> MRM a -> MRM a
-withCoIndHyp' hyp m =
-  withCoIndHypRaw hyp m `catchError` \case
-  MRExnWiden nm1' nm2' new_vars
-    | coIndHypLHSFun hyp == nm1' && coIndHypRHSFun hyp == nm2' ->
-        -- NOTE: the state automatically gets reset here because we defined MRM
-        -- with ExceptT at a lower level than StateT
-        do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2'
-           debugPrint 2 $ "Widening indices: " ++ intercalate ", " (map show new_vars)
-           hyp' <- generalizeCoIndHyp hyp new_vars
-           withCoIndHyp' hyp' m
-  e -> throwError e
+     (withOnlyUVars (coIndHypCtx hyp) $ withOnlyAssumption pre $
+      withCoIndHyp hyp $ mrRefines lhs rhs) `catchError` \case
+       MRExnWiden nm1' nm2' new_vars
+         | f1 == nm1' && f2 == nm2' ->
+           -- NOTE: the state automatically gets reset here because we defined
+           -- MRM with ExceptT at a lower level than StateT
+           do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2'
+              debugPrint 2 ("Widening indices: " ++
+                            intercalate ", " (map show new_vars))
+              hyp' <- generalizeCoIndHyp hyp new_vars
+              proveCoIndHyp hyp'
+       e -> throwError e
 
 
 -- | Test that a coinductive hypothesis for the given function names matches the
@@ -408,7 +418,7 @@ matchCoIndHyp hyp args1 args2 =
      if and (eqs1 ++ eqs2) then return () else
        throwError $ MRExnWiden (coIndHypLHSFun hyp) (coIndHypRHSFun hyp)
        (map Left (findIndices not eqs1) ++ map Right (findIndices not eqs2))
-     proveCoIndHypPreCond hyp args1 args2
+     proveCoIndHypPreCond hyp
 
 
 -- | Generalize some of the arguments of a coinductive hypothesis
@@ -608,7 +618,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   -- * If it is convertible to our goal, continue and prove that k1 |= k2
   -- * If it can be widened with our goal, restart the current proof branch
   --   with the widened hypothesis (done by throwing a
-  --   'CoIndHypMismatchWidened' error for 'withCoIndHyp' to catch)
+  --   'CoIndHypMismatchWidened' error for 'proveCoIndHyp' to catch)
   -- * Otherwise, throw a 'CoIndHypMismatchFailure' error.
   (Just hyp, _) ->
     matchCoIndHyp hyp args1 args2 >>
@@ -636,10 +646,9 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   -- that f1 args1 |= f2 args2 under the assumption that f1 args1 |= f2 args2,
   -- and then try to prove that k1 |= k2
   _ | tps_eq
-    , Just (f1_body, _) <- maybe_f1_body
-    , Just (f2_body, _) <- maybe_f2_body ->
-      do withCoIndHyp f1 args1 f2 args2 $ mrRefines f1_body f2_body
-         mrRefinesFun k1 k2
+    , Just _ <- maybe_f1_body
+    , Just _ <- maybe_f2_body ->
+      mrRefinesCoInd f1 args1 f2 args2 >> mrRefinesFun k1 k2
 
   -- If we cannot line up f1 and f2, then making progress here would require us
   -- to somehow split either m1 or m2 into some bind m' >>= k' such that m' is

From 670f641fc7a7936b4114e987e5b4492afcb3fa3e Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 09:56:18 -0800
Subject: [PATCH 03/15] added logic to normalize precondHint terms

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

diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index df12b04b77..793b02ffbc 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -228,6 +228,8 @@ normComp (CompTerm t) =
       return $ ExistsM (Type tp) (CompFunTerm body_tm)
     (isGlobalDef "Prelude.forallM" -> Just (), [tp, _, body_tm]) ->
       return $ ForallM (Type tp) (CompFunTerm body_tm)
+    (isGlobalDef "Prelude.precondHint" -> Just (), [_, _, body_tm]) ->
+      normCompTerm body_tm
     (isGlobalDef "Prelude.letRecM" -> Just (), [lrts, _, defs_f, body_f]) ->
       do
         -- Bind fresh function vars for the letrec-bound functions

From 4fab1e8c597a2e46dffa7fbbaf743eafa2ed04c7 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 13:53:20 -0800
Subject: [PATCH 04/15] fixed a bug in smallestBitSetElem

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

diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
index fb7ae57fef..59c3e3276d 100644
--- a/saw-core/src/Verifier/SAW/Term/Functor.hs
+++ b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -58,6 +58,7 @@ module Verifier.SAW.Term.Functor
     -- * Sets of free variables
   , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
   , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
+  , smallestBitSetElem
   , looseVars, smallestFreeVar
   ) where
 
@@ -485,7 +486,7 @@ bitSetElems = go 0 where
   go shft bs = case smallestBitSetElem bs of
     Nothing -> []
     Just i ->
-      shft + i : go (shft + i + 1) (multiDecrBitSet (shft + i + 1) bs)
+      shft + i : go (shft + i + 1) (multiDecrBitSet (i + 1) bs)
 
 -- | Compute the free variables of a term given free variables for its immediate
 -- subterms

From 4c8f7a1e14cf5f945a2ae37117f447e2a0c90206 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 13:54:56 -0800
Subject: [PATCH 05/15] fixed a subtle free variable bug in
 mrTrySetAppliedEVar; also changed mrSetEVarClosed to have a more
 understandable error message

---
 src/SAWScript/Prover/MRSolver/Monad.hs | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index af462235be..4036b9132f 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -744,7 +744,15 @@ mrSetEVarClosed var val =
      -- 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) var_tp
+     eith_err <-
+       liftSC2 (runTCM $ checkSubtype (TypedTerm val val_tp) var_tp) Nothing []
+     case eith_err of
+       Left _ ->
+         error ("mrSetEVarClosed: incorrect instantiation for evar " ++
+                showMRVar var ++
+                "\nexpected type:\n" ++ showTerm var_tp ++
+                "\nactual type:\n" ++ showTerm val_tp)
+       Right _ -> return ()
      modify $ \st ->
        st { mrsVars =
             Map.alter
@@ -766,6 +774,8 @@ mrTrySetAppliedEVar evar args t =
   let (evar_vars, _) = asPiList (mrVarType evar) in
   -- Get all the free variables of t
   let free_vars = bitSetElems (looseVars t) in
+  -- Get the maximum deBruijn index of free_vars
+  let max_fv = maximum free_vars in
   -- For each free var of t, find an arg equal to it
   case mapM (\i -> findIndex (\case
                                  (asLocalVar -> Just j) -> i == j
@@ -776,15 +786,17 @@ mrTrySetAppliedEVar evar args t =
           -- Build a list of the input vars x1 ... xn as terms, noting that the
           -- first variable is the least recently bound and so has the highest
           -- deBruijn index
-          let arg_ixs = [length args - 1, length args - 2 .. 0]
+          let arg_ixs = reverse [0 .. length args - 1]
           arg_vars <- mapM (liftSC1 scLocalVar) arg_ixs
 
-          -- For free variable of t, we substitute the corresponding variable
-          -- xi, substituting error terms for the variables that are not free
-          -- (since we have nothing else to substitute for them)
+          -- For each free variable of t, we substitute the corresponding
+          -- variable xi, substituting error terms for the variables that are
+          -- not free (since we have nothing else to substitute for them)
           let var_map = zip free_vars fv_arg_ixs
-          let subst = flip map [0 .. length args - 1] $ \i ->
-                maybe (error "mrTrySetAppliedEVar: unexpected free variable")
+          let subst = flip map [0 .. max_fv] $ \i ->
+                maybe (error
+                       ("mrTrySetAppliedEVar: unexpected free variable "
+                        ++ show i ++ " in term\n" ++ showTerm t))
                 (arg_vars !!) (lookup i var_map)
           body <- substTerm 0 subst t
 

From fe62c84635b5dfead57b5008a9aed7a83b35e22a Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 13:55:21 -0800
Subject: [PATCH 06/15] added some printing helper functions

---
 src/SAWScript/Prover/MRSolver/SMT.hs    | 7 ++++++-
 src/SAWScript/Prover/MRSolver/Solver.hs | 1 -
 src/SAWScript/Prover/MRSolver/Term.hs   | 7 +++++++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index cb49875836..8cd193b8a6 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -274,7 +274,12 @@ mrProveEqSimple eqf t1 t2 =
 mrProveEq :: Term -> Term -> MRM Bool
 mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
-     tp <- mrTypeOf t1
+     tp <- mrTypeOf t1 >>= mrSubstEVars
+     tp2 <- mrTypeOf t2 >>= mrSubstEVars
+     tps_eq <- mrConvertible tp tp2
+     if tps_eq then return () else
+       error ("mrProveEq: types not equal:\n" ++
+              showTerm tp ++ "\n" ++ showTerm tp2)
      varmap <- mrVars
      cond_in_ctx <- mrProveEqH varmap tp t1 t2
      res <- withTermInCtx cond_in_ctx mrProvable
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 793b02ffbc..442f7d3946 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -439,7 +439,6 @@ generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) =
     do let arg' = coIndHypArg hyp spec'
        tp' <- mrTypeOf arg'
        mrDebugPPPrefixSep 2 "generalizeCoIndHyp: the type of" arg' "is" tp'
-       debugPrint 2 ("arg' = " ++ show arg')
        tps_eq <- mrConvertible arg_tp tp'
        args_eq <- if tps_eq then mrProveEq arg arg' else return False
        return $ if args_eq then Left spec' else Right spec'
diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs
index fcc88f4639..78feb8d8b7 100644
--- a/src/SAWScript/Prover/MRSolver/Term.hs
+++ b/src/SAWScript/Prover/MRSolver/Term.hs
@@ -56,6 +56,10 @@ newtype MRVar = MRVar { unMRVar :: ExtCns Term } deriving (Eq, Show, Ord)
 mrVarType :: MRVar -> Term
 mrVarType = ecType . unMRVar
 
+-- | Print the string name of an 'MRVar'
+showMRVar :: MRVar -> String
+showMRVar = show . ppName . ecName . unMRVar
+
 -- | A tuple or record projection of a 'Term'
 data TermProj = TermProjLeft | TermProjRight | TermProjRecord FieldName
               deriving (Eq, Ord, Show)
@@ -324,6 +328,9 @@ instance PrettyInCtx Type where
 instance PrettyInCtx MRVar where
   prettyInCtx (MRVar ec) = return $ ppName $ ecName ec
 
+instance PrettyInCtx [Term] where
+  prettyInCtx xs = list <$> mapM prettyInCtx xs
+
 instance PrettyInCtx TermProj where
   prettyInCtx TermProjLeft = return (pretty '.' <> "1")
   prettyInCtx TermProjRight = return (pretty '.' <> "2")

From 3962bdc0423fb8bc94b1fdf06242a5abd004aaf0 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 14:26:21 -0800
Subject: [PATCH 07/15] removed the type equality check in mrProveEq

---
 src/SAWScript/Prover/MRSolver/SMT.hs | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index 8cd193b8a6..04f85ece7f 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -275,11 +275,6 @@ mrProveEq :: Term -> Term -> MRM Bool
 mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
      tp <- mrTypeOf t1 >>= mrSubstEVars
-     tp2 <- mrTypeOf t2 >>= mrSubstEVars
-     tps_eq <- mrConvertible tp tp2
-     if tps_eq then return () else
-       error ("mrProveEq: types not equal:\n" ++
-              showTerm tp ++ "\n" ++ showTerm tp2)
      varmap <- mrVars
      cond_in_ctx <- mrProveEqH varmap tp t1 t2
      res <- withTermInCtx cond_in_ctx mrProvable

From eccfdebce30c86798356ff720b7ea264e8d99f05 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 15:14:01 -0800
Subject: [PATCH 08/15] added Mr Solver proof that contains0 |=
 noErrorsContains0

---
 heapster-saw/examples/arrays.sawcore       | 37 ++++++++++++++++++++++
 heapster-saw/examples/arrays_mr_solver.saw |  6 +++-
 2 files changed, 42 insertions(+), 1 deletion(-)

diff --git a/heapster-saw/examples/arrays.sawcore b/heapster-saw/examples/arrays.sawcore
index 7c20a89268..6b1f16867b 100644
--- a/heapster-saw/examples/arrays.sawcore
+++ b/heapster-saw/examples/arrays.sawcore
@@ -2,3 +2,40 @@
 module arrays where
 
 import Prelude;
+
+-- The helper function for noErrorsContains0
+--
+-- noErrorsContains0H len i v =
+--   orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
+noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+                     CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+noErrorsContains0H len_top i_top v_top =
+  letRecM
+    (LRT_Cons
+     (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
+      LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
+      LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
+      LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
+     LRT_Nil)
+    (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
+    (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+       ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
+           precondHint
+             (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
+             (and (bvsle 64 0x0000000000000000 i)
+                  (bvsle 64 i 0x0fffffffffffffff))
+             (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                  (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                           (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
+                  (f len (bvAdd 64 i 0x0000000000000001) v))), ()))
+    (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+       f len_top i_top v_top);
+
+-- The specification that contains0 has no errors
+noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+                    CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+noErrorsContains0 len v =
+  noErrorsContains0H len 0x0000000000000000 v;
diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw
index 838e1d2874..eaa38a79f7 100644
--- a/heapster-saw/examples/arrays_mr_solver.saw
+++ b/heapster-saw/examples/arrays_mr_solver.saw
@@ -16,4 +16,8 @@ let run_test name test expected =
 
 // Test that contains0 |= contains0
 contains0 <- parse_core_mod "arrays" "contains0";
-run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;
+// run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;
+
+noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
+run_test "contains0 |= noErrorsContains0"
+  (mr_solver_debug 0 contains0 noErrorsContains0) true;

From 02aed402170b77b2c1052f5ce53fc9c6c71344d1 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 15:43:04 -0800
Subject: [PATCH 09/15] removed mr_solver_set_precond; removed preconditions
 from MR Solver environments; changed mr_solver command to remember
 refinements that have been proved

---
 src/SAWScript/Builtins.hs               | 25 +------------
 src/SAWScript/Interpreter.hs            |  5 ---
 src/SAWScript/Prover/MRSolver.hs        |  2 +-
 src/SAWScript/Prover/MRSolver/Monad.hs  | 45 -----------------------
 src/SAWScript/Prover/MRSolver/Solver.hs | 17 +++++++--
 src/SAWScript/Prover/MRSolver/Term.hs   | 49 +++++++++++++++++++++++++
 src/SAWScript/Value.hs                  |  2 +-
 7 files changed, 66 insertions(+), 79 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index a95569d946..1765ce785b 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -71,7 +71,6 @@ import Verifier.SAW.SATQuery
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
 import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
 import Verifier.SAW.SharedTerm
-import Verifier.SAW.Recognizer
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import Verifier.SAW.Prim (rethrowEvalError)
@@ -1571,28 +1570,8 @@ mrSolver sc dlvl t1 t2 =
      let env = rwMRSolverEnv rw
      res <- liftIO $ Prover.askMRSolver sc dlvl env Nothing m1 m2
      case res of
-       Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False
-       Nothing -> return True
-
--- | Set the precondition for a named function, given as a SAW core term
-mrSolverSetPrecond :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel ()
-mrSolverSetPrecond sc f pre =
-  do rw <- get
-     f_mon <- ttTerm <$> ensureMonadicTerm sc f
-     gdef <- case Monadify.asTypedGlobalDef f_mon of
-       Just gdef -> return gdef
-       Nothing -> fail "mr_solver_set_precond: Not an identifier"
-     -- NOTE: do not monadify pre, as it is supposed to be pure
-     (asPiList -> (f_args, _)) <- io $ scTypeOf sc f_mon
-     pre_tp <- io (scTypeOf sc $ ttTerm pre)
-     pre_tp_req <- io (scBoolType sc >>= scPiList sc f_args)
-     correct_tp <- io (scConvertible sc True pre_tp pre_tp_req)
-     if correct_tp then return () else
-       fail ("mr_solver_set_precond: incorrect type for precondition\n" ++
-             "Expected: " ++ showTerm pre_tp_req ++ "\n" ++
-             "Actual: " ++ showTerm pre_tp)
-     let env = rwMRSolverEnv rw
-     put (rw { rwMRSolverEnv = Prover.mrEnvAddPrecond gdef (ttTerm pre) env })
+       Left err -> io (putStrLn $ Prover.showMRFailure err) >> return False
+       Right env' -> put (rw { rwMRSolverEnv = env' }) >> return True
 
 setMonadification :: SharedContext -> String -> String -> TopLevel ()
 setMonadification sc cry_str saw_str =
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 114ea7f32d..4a4b2c8f10 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3169,11 +3169,6 @@ primitives = Map.fromList
     Experimental
     [ "Call the monadic-recursive solver at the supplied debug level" ]
 
-  , prim "mr_solver_set_precond"  "Term -> Term -> TopLevel ()"
-    (scVal mrSolverSetPrecond)
-    Experimental
-    [ "Set the precondition for use in Mr Solver of a function to a function" ]
-
   , prim "monadify_term" "Term -> TopLevel Term"
     (scVal monadifyTypedTerm)
     Experimental
diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index fb2589766d..759116dedf 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -10,7 +10,7 @@ Portability : non-portable (language extensions)
 
 module SAWScript.Prover.MRSolver
   (askMRSolver, MRFailure(..), showMRFailure, isCompFunType,
-   MREnv(..), emptyMREnv, mrEnvAddPrecond) where
+   MREnv(..), emptyMREnv) where
 
 import SAWScript.Prover.MRSolver.Term
 import SAWScript.Prover.MRSolver.Monad
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 4036b9132f..38be1476dc 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -227,31 +227,6 @@ instance PrettyInCtx CoIndHyp where
                    return "|=",
                    prettyInCtx (FunBind f2 args2 CompFunReturn)]
 
--- | An assumption that a named function refines some specificaiton. This has
--- the form
---
--- > forall x1, ..., xn. F e1 ... ek |= m
---
--- for some universal context @x1:T1, .., xn:Tn@, some list of argument
--- expressions @ei@ over the universal @xj@ variables, and some right-hand side
--- computation expression @m@.
-data FunAssump = FunAssump {
-  -- | The uvars that were in scope when this assmption was created, in order
-  -- from outermost to innermost; that is, the uvars as "seen from outside their
-  -- scope", which is the reverse of the order of 'mrUVars', below
-  fassumpCtx :: [(LocalName,Term)],
-  -- | The argument expressions @e1, ..., en@ over the 'fassumpCtx' uvars
-  fassumpArgs :: [Term],
-  -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars
-  fassumpRHS :: NormComp
-}
-
--- | A map from function names to function refinement assumptions over that
--- name
---
--- FIXME: this should probably be an 'IntMap' on the 'VarIndex' of globals
-type FunAssumps = Map FunName FunAssump
-
 -- | An assumption that something is equal to one of the constructors of a
 -- datatype, e.g. equal to @Left@ of some 'Term' or @Right@ of some 'Term'
 data DataTypeAssump = IsLeft Term | IsRight Term
@@ -273,26 +248,6 @@ type DataTypeAssumps = HashMap Term DataTypeAssump
 
 -- FIXME HERE NOW: remove preconditions from MREnv
 
--- | A global MR Solver environment
-data MREnv = MREnv {
-  -- | The set of function refinements to be assumed by to Mr. Solver (which
-  -- have hopefully been proved previously...)
-  mreFunAssumps :: FunAssumps,
-  -- | The preconditions associated with functions by the user
-  mrePreconditions :: Map FunName Term
-  }
-
--- | The empty 'MREnv'
-emptyMREnv :: MREnv
-emptyMREnv = MREnv { mreFunAssumps = Map.empty,
-                     mrePreconditions = Map.empty }
-
--- | Add a precondition to an 'MREnv'
-mrEnvAddPrecond :: GlobalDef -> Term -> MREnv -> MREnv
-mrEnvAddPrecond gdef pre env =
-  env { mrePreconditions =
-          Map.insert (GlobalName gdef []) pre (mrePreconditions env) }
-
 -- | Parameters and locals for MR. Solver
 data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 442f7d3946..fbde43b184 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -760,20 +760,21 @@ mrRefinesFun _ _ = error "mrRefinesFun: unreachable!"
 -- * External Entrypoints
 ----------------------------------------------------------------------
 
--- | Test two monadic, recursive terms for equivalence
+-- | Test two monadic, recursive terms for refinement. On success, if the
+-- left-hand term is a named function, add the refinement to the 'MREnv'
+-- environment.
 askMRSolver ::
   SharedContext ->
   Int {- ^ The debug level -} ->
   MREnv {- ^ The Mr Solver environment -} ->
   Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} ->
-  Term -> Term -> IO (Maybe MRFailure)
+  Term -> Term -> IO (Either MRFailure MREnv)
 
 askMRSolver sc dlvl env timeout t1 t2 =
   do tp1 <- scTypeOf sc t1 >>= scWhnf sc
      tp2 <- scTypeOf sc t2 >>= scWhnf sc
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->
-         fmap (either Just (const Nothing)) $
          runMRM sc timeout dlvl env $
          withUVars uvar_ctx $ \vars ->
          do tps_are_eq <- mrConvertible tp1 tp2
@@ -783,4 +784,12 @@ askMRSolver sc dlvl env timeout t1 t2 =
             m1 <- mrApplyAll t1 vars >>= normCompTerm
             m2 <- mrApplyAll t2 vars >>= normCompTerm
             mrRefines m1 m2
-       _ -> return $ Just $ NotCompFunType tp1
+            -- If t1 is a named function, add forall xs. f1 xs |= m2 to the env
+            case asGlobalFunName t1 of
+              Just f1 ->
+                let fassump = FunAssump { fassumpCtx = uvar_ctx,
+                                          fassumpArgs = vars,
+                                          fassumpRHS = m2 } in
+                return $ mrEnvAddFunAssump f1 fassump env
+              Nothing -> return env
+       _ -> return $ Left $ NotCompFunType tp1
diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs
index 78feb8d8b7..cd7a10c86d 100644
--- a/src/SAWScript/Prover/MRSolver/Term.hs
+++ b/src/SAWScript/Prover/MRSolver/Term.hs
@@ -37,6 +37,9 @@ import GHC.Generics
 
 import Prettyprinter
 
+import Data.Map (Map)
+import qualified Data.Map as Map
+
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.Term.CtxTerm (MonadTerm(..))
 import Verifier.SAW.Term.Pretty
@@ -168,6 +171,52 @@ isCompFunType sc t = scWhnf sc t >>= \case
   _ -> return False
 
 
+----------------------------------------------------------------------
+-- * Mr Solver Environments
+----------------------------------------------------------------------
+
+-- | An assumption that a named function refines some specification. This has
+-- the form
+--
+-- > forall x1, ..., xn. F e1 ... ek |= m
+--
+-- for some universal context @x1:T1, .., xn:Tn@, some list of argument
+-- expressions @ei@ over the universal @xj@ variables, and some right-hand side
+-- computation expression @m@.
+data FunAssump = FunAssump {
+  -- | The uvars that were in scope when this assmption was created, in order
+  -- from outermost to innermost; that is, the uvars as "seen from outside their
+  -- scope", which is the reverse of the order of 'mrUVars', below
+  fassumpCtx :: [(LocalName,Term)],
+  -- | The argument expressions @e1, ..., en@ over the 'fassumpCtx' uvars
+  fassumpArgs :: [Term],
+  -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars
+  fassumpRHS :: NormComp
+}
+
+-- | A map from function names to function refinement assumptions over that
+-- name
+--
+-- FIXME: this should probably be an 'IntMap' on the 'VarIndex' of globals
+type FunAssumps = Map FunName FunAssump
+
+-- | A global MR Solver environment
+data MREnv = MREnv {
+  -- | The set of function refinements to be assumed by to Mr. Solver (which
+  -- have hopefully been proved previously...)
+  mreFunAssumps :: FunAssumps
+  }
+
+-- | The empty 'MREnv'
+emptyMREnv :: MREnv
+emptyMREnv = MREnv { mreFunAssumps = Map.empty }
+
+-- | Add a 'FunAssump' to a Mr Solver environment
+mrEnvAddFunAssump :: FunName -> FunAssump -> MREnv -> MREnv
+mrEnvAddFunAssump f fassump env =
+  env { mreFunAssumps = Map.insert f fassump (mreFunAssumps env) }
+
+
 ----------------------------------------------------------------------
 -- * Utility Functions for Transforming 'Term's
 ----------------------------------------------------------------------
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 8e0e40bb2b..9da3910473 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -76,7 +76,7 @@ import SAWScript.JavaPretty (prettyClass)
 import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity)
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
-import SAWScript.Prover.MRSolver.Monad as MRSolver
+import SAWScript.Prover.MRSolver.Term as MRSolver
 import SAWScript.Crucible.LLVM.Skeleton
 import SAWScript.X86 (X86Unsupported(..), X86Error(..))
 

From 7ee43cfe5a90e484794b957db4eb231c2b6b40c3 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 7 Mar 2022 16:52:01 -0800
Subject: [PATCH 10/15] added initialization of rwMRSolverEnv field to
 saw-remote-api

---
 saw-remote-api/src/SAWServer.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index 776abea42e..b6ac03c7f6 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -59,6 +59,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import qualified Cryptol.Utils.Ident as Cryptol
 import Verifier.SAW.Cryptol.Monadify (defaultMonEnv)
+import SAWScript.Prover.MRSolver (emptyMREnv)
 
 import qualified Argo
 --import qualified CryptolServer (validateServerState, ServerState(..))
@@ -219,6 +220,7 @@ initialState readFileFn =
                 , rwDocs = mempty
                 , rwCryptol = cenv
                 , rwMonadify = defaultMonEnv
+                , rwMRSolverEnv = emptyMREnv
                 , rwPPOpts = defaultPPOpts
                 , rwJVMTrans = jvmTrans
                 , rwPrimsAvail = mempty

From ee4b67bd87c1a41e71c9675b62e79caccee1bd22 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 8 Mar 2022 07:05:46 -0800
Subject: [PATCH 11/15] whoops, need to avoid calling maximum on an empty list

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

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 38be1476dc..15df3e0f0f 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -729,8 +729,6 @@ mrTrySetAppliedEVar evar args t =
   let (evar_vars, _) = asPiList (mrVarType evar) in
   -- Get all the free variables of t
   let free_vars = bitSetElems (looseVars t) in
-  -- Get the maximum deBruijn index of free_vars
-  let max_fv = maximum free_vars in
   -- For each free var of t, find an arg equal to it
   case mapM (\i -> findIndex (\case
                                  (asLocalVar -> Just j) -> i == j
@@ -748,7 +746,9 @@ mrTrySetAppliedEVar evar args t =
           -- variable xi, substituting error terms for the variables that are
           -- not free (since we have nothing else to substitute for them)
           let var_map = zip free_vars fv_arg_ixs
-          let subst = flip map [0 .. max_fv] $ \i ->
+          let subst_vars = if free_vars == [] then [] else
+                             [0 .. maximum free_vars]
+          let subst = flip map subst_vars $ \i ->
                 maybe (error
                        ("mrTrySetAppliedEVar: unexpected free variable "
                         ++ show i ++ " in term\n" ++ showTerm t))

From a301dc659b52b60a0460ec96330d8daeede4c4e7 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 8 Mar 2022 07:19:50 -0800
Subject: [PATCH 12/15] updated efq1 to call Eq__rec instead of the Eq#rec
 recursor

---
 saw-core/prelude/Prelude.sawcore | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 43cdafd843..c8e065f121 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1718,9 +1718,9 @@ efq a contra =
 -- Ex Falso Quodlibet at sort 1
 efq1 : (a : sort 1) -> Eq Bool True False -> a;
 efq1 a contra =
-  Eq#rec Bit Bit1
-         (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
-         () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
+  Eq__rec Bit Bit1
+          (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
+          () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
 
 -- Generate an empty BVVec
 emptyBVVec : (n : Nat) -> (a : sort 0) -> BVVec n (bvNat n 0) a;

From 34518a69677c52b8825fc42c85fc026c669fc064 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Tue, 8 Mar 2022 10:52:47 -0800
Subject: [PATCH 13/15] changed multiFixM to be primitive, because the
 translator was not working correctly on some of its helper functions...

---
 .../CryptolPrimitivesForSAWCore.v             | 80 ++++++++++++-------
 .../generated/CryptolToCoq/SAWCorePrelude.v   | 53 +++++++++---
 saw-core/prelude/Prelude.sawcore              | 62 +++++++++-----
 3 files changed, 138 insertions(+), 57 deletions(-)

diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
index a57aee7096..175ebcd520 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
@@ -131,6 +131,9 @@ Definition ecRatio : SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Integer ->
 Definition eqRational : Rational -> Rational -> SAWCoreScaffolding.Bool :=
   fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (==) Rational"%string.
 
+Definition leRational : Rational -> Rational -> SAWCoreScaffolding.Bool :=
+  fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (<=) Rational"%string.
+
 Definition ltRational : Rational -> Rational -> SAWCoreScaffolding.Bool :=
   fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (<) Rational"%string.
 
@@ -219,6 +222,9 @@ Definition errorBinary : forall (s : SAWCoreScaffolding.String), forall (a : Typ
 Definition boolCmp : SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool :=
   fun (x : SAWCoreScaffolding.Bool) (y : SAWCoreScaffolding.Bool) (k : SAWCoreScaffolding.Bool) => if x then SAWCoreScaffolding.and y k else SAWCoreScaffolding.or y k.
 
+Definition boolLt : SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool :=
+  fun (x : SAWCoreScaffolding.Bool) (y : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.and (SAWCoreScaffolding.not x) y.
+
 Definition integerCmp : SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Integer -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool :=
   fun (x : SAWCoreScaffolding.Integer) (y : SAWCoreScaffolding.Integer) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.or (SAWCoreScaffolding.intLt x y) (SAWCoreScaffolding.and (SAWCoreScaffolding.intEq x y) k).
 
@@ -235,12 +241,25 @@ Definition vecCmp : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), fora
   fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (xs : SAWCoreVectorsAsCoqVectors.Vec n a) (ys : SAWCoreVectorsAsCoqVectors.Vec n a) (k : SAWCoreScaffolding.Bool) => let var__0   := SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool in
   SAWCoreVectorsAsCoqVectors.foldr var__0 SAWCoreScaffolding.Bool n (fun (f1 : var__0) => f1) k (SAWCorePrelude.zipWith a a var__0 f n xs ys).
 
+Definition vecLt : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (a -> a -> SAWCoreScaffolding.Bool) -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Bool :=
+  fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : a -> a -> SAWCoreScaffolding.Bool) (xs : SAWCoreVectorsAsCoqVectors.Vec n a) (ys : SAWCoreVectorsAsCoqVectors.Vec n a) => let var__0   := SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool in
+  SAWCoreVectorsAsCoqVectors.foldr var__0 SAWCoreScaffolding.Bool n (fun (f1 : var__0) => f1) SAWCoreScaffolding.false (SAWCorePrelude.zipWith a a var__0 f n xs ys).
+
 Definition unitCmp : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool :=
-  fun (_1 : unit : Type) (_2 : unit : Type) (_3 : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.false.
+  fun (_1 : unit : Type) (_2 : unit : Type) (k : SAWCoreScaffolding.Bool) => k.
+
+Definition unitLe : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool :=
+  fun (_1 : unit : Type) (_2 : unit : Type) => SAWCoreScaffolding.true.
+
+Definition unitLt : (unit : Type) -> (unit : Type) -> SAWCoreScaffolding.Bool :=
+  fun (_1 : unit : Type) (_2 : unit : Type) => SAWCoreScaffolding.false.
 
 Definition pairCmp : forall (a : Type), forall (b : Type), (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> prod a b -> prod a b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool :=
   fun (a : Type) (b : Type) (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (x12 : prod a b) (y12 : prod a b) (k : SAWCoreScaffolding.Bool) => f (fst x12) (fst y12) (g (snd x12) (snd y12) k).
 
+Definition pairLt : forall (a : Type), forall (b : Type), (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) -> (b -> b -> SAWCoreScaffolding.Bool) -> prod a b -> prod a b -> SAWCoreScaffolding.Bool :=
+  fun (a : Type) (b : Type) (f : a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (g : b -> b -> SAWCoreScaffolding.Bool) (x : prod a b) (y : prod a b) => f (fst x) (fst y) (g (snd x) (snd y)).
+
 Definition PEq : Type -> Type :=
   fun (a : Type) => RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil.
 
@@ -278,55 +297,61 @@ Definition PEqPair : forall (a : Type), forall (b : Type), PEq a -> PEq b -> PEq
   fun (a : Type) (b : Type) (pa : RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (pb : RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) => RecordCons "eq" (SAWCorePrelude.pairEq a b (RecordProj pa "eq") (RecordProj pb "eq")) RecordNil.
 
 Definition PCmp : Type -> Type :=
-  fun (a : Type) => RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (PEq a) RecordTypeNil).
+  fun (a : Type) => let var__0   := a -> a -> SAWCoreScaffolding.Bool in
+  RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (PEq a) (RecordTypeCons "le" var__0 (RecordTypeCons "lt" var__0 RecordTypeNil))).
 
 Definition PCmpBit : PCmp SAWCoreScaffolding.Bool :=
-  RecordCons "cmp" boolCmp (RecordCons "cmpEq" PEqBit RecordNil).
+  RecordCons "cmp" boolCmp (RecordCons "cmpEq" PEqBit (RecordCons "le" implies (RecordCons "lt" boolLt RecordNil))).
 
 Definition PCmpInteger : PCmp SAWCoreScaffolding.Integer :=
-  RecordCons "cmp" integerCmp (RecordCons "cmpEq" PEqInteger RecordNil).
+  RecordCons "cmp" integerCmp (RecordCons "cmpEq" PEqInteger (RecordCons "le" SAWCoreScaffolding.intLe (RecordCons "lt" SAWCoreScaffolding.intLt RecordNil))).
 
 Definition PCmpRational : PCmp Rational :=
-  RecordCons "cmp" rationalCmp (RecordCons "cmpEq" PEqRational RecordNil).
+  RecordCons "cmp" rationalCmp (RecordCons "cmpEq" PEqRational (RecordCons "le" leRational (RecordCons "lt" ltRational RecordNil))).
 
 Definition PCmpVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (SAWCoreVectorsAsCoqVectors.Vec n a) :=
-  fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "cmp" (vecCmp n a (RecordProj pa "cmp")) (RecordCons "cmpEq" (PEqVec n a (RecordProj pa "cmpEq")) RecordNil).
+  fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec n a in
+  RecordCons "cmp" (vecCmp n a (RecordProj pa "cmp")) (RecordCons "cmpEq" (PEqVec n a (RecordProj pa "cmpEq")) (RecordCons "le" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "cmp") x y SAWCoreScaffolding.true) (RecordCons "lt" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "cmp") x y SAWCoreScaffolding.false) RecordNil))).
 
 Definition PCmpSeq : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n a) :=
-  fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream a)) "invalid Cmp instance"%string) n.
+  fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PCmp a -> PCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream a)) "invalid Cmp instance"%string) n.
 
 Definition PCmpWord : forall (n : SAWCoreScaffolding.Nat), PCmp (SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) :=
-  fun (n : SAWCoreScaffolding.Nat) => RecordCons "cmp" (bvCmp n) (RecordCons "cmpEq" (PEqWord n) RecordNil).
+  fun (n : SAWCoreScaffolding.Nat) => RecordCons "cmp" (bvCmp n) (RecordCons "cmpEq" (PEqWord n) (RecordCons "le" (SAWCoreVectorsAsCoqVectors.bvule n) (RecordCons "lt" (SAWCoreVectorsAsCoqVectors.bvult n) RecordNil))).
 
 Definition PCmpSeqBool : forall (n : Num), PCmp (seq n SAWCoreScaffolding.Bool) :=
   fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PCmp (seq n1 SAWCoreScaffolding.Bool)) (fun (n1 : SAWCoreScaffolding.Nat) => PCmpWord n1) (SAWCoreScaffolding.error (PCmp (SAWCorePrelude.Stream SAWCoreScaffolding.Bool)) "invalid Cmp instance"%string) n.
 
 Definition PCmpUnit : PCmp (unit : Type) :=
-  RecordCons "cmp" unitCmp (RecordCons "cmpEq" PEqUnit RecordNil).
+  RecordCons "cmp" unitCmp (RecordCons "cmpEq" PEqUnit (RecordCons "le" unitLe (RecordCons "lt" unitLt RecordNil))).
 
 Definition PCmpPair : forall (a : Type), forall (b : Type), PCmp a -> PCmp b -> PCmp (prod a b) :=
-  fun (a : Type) (b : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (pb : RecordTypeCons "cmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "cmp" (pairCmp a b (RecordProj pa "cmp") (RecordProj pb "cmp")) (RecordCons "cmpEq" (PEqPair a b (RecordProj pa "cmpEq") (RecordProj pb "cmpEq")) RecordNil).
+  fun (a : Type) (b : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (pb : RecordTypeCons "cmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (b -> b -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0   := RecordProj pa "cmp" in
+  RecordCons "cmp" (pairCmp a b var__0 (RecordProj pb "cmp")) (RecordCons "cmpEq" (PEqPair a b (RecordProj pa "cmpEq") (RecordProj pb "cmpEq")) (RecordCons "le" (pairLt a b var__0 (RecordProj pb "le")) (RecordCons "lt" (pairLt a b var__0 (RecordProj pb "lt")) RecordNil))).
 
 Definition PSignedCmp : Type -> Type :=
-  fun (a : Type) => RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (PEq a) RecordTypeNil).
+  fun (a : Type) => let var__0   := a -> a -> SAWCoreScaffolding.Bool in
+  RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (PEq a) (RecordTypeCons "sle" var__0 (RecordTypeCons "slt" var__0 RecordTypeNil))).
 
 Definition PSignedCmpVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (SAWCoreVectorsAsCoqVectors.Vec n a) :=
-  fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "scmp" (vecCmp n a (RecordProj pa "scmp")) (RecordCons "signedCmpEq" (PEqVec n a (RecordProj pa "signedCmpEq")) RecordNil).
+  fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec n a in
+  RecordCons "scmp" (vecCmp n a (RecordProj pa "scmp")) (RecordCons "signedCmpEq" (PEqVec n a (RecordProj pa "signedCmpEq")) (RecordCons "sle" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "scmp") x y SAWCoreScaffolding.true) (RecordCons "slt" (fun (x : var__0) (y : SAWCoreVectorsAsCoqVectors.Vec n a) => vecCmp n a (RecordProj pa "scmp") x y SAWCoreScaffolding.false) RecordNil))).
 
 Definition PSignedCmpSeq : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n a) :=
-  fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream a)) "invalid SignedCmp instance"%string) n.
+  fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, PSignedCmp a -> PSignedCmp (seq n1 a)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpVec n1) (fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream a)) "invalid SignedCmp instance"%string) n.
 
 Definition PSignedCmpWord : forall (n : SAWCoreScaffolding.Nat), PSignedCmp (SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) :=
-  fun (n : SAWCoreScaffolding.Nat) => RecordCons "scmp" (bvSCmp n) (RecordCons "signedCmpEq" (PEqWord n) RecordNil).
+  fun (n : SAWCoreScaffolding.Nat) => RecordCons "scmp" (bvSCmp n) (RecordCons "signedCmpEq" (PEqWord n) (RecordCons "sle" (SAWCoreVectorsAsCoqVectors.bvsle n) (RecordCons "slt" (SAWCoreVectorsAsCoqVectors.bvslt n) RecordNil))).
 
 Definition PSignedCmpSeqBool : forall (n : Num), PSignedCmp (seq n SAWCoreScaffolding.Bool) :=
   fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => PSignedCmp (seq n1 SAWCoreScaffolding.Bool)) (fun (n1 : SAWCoreScaffolding.Nat) => PSignedCmpWord n1) (SAWCoreScaffolding.error (PSignedCmp (SAWCorePrelude.Stream SAWCoreScaffolding.Bool)) "invalid SignedCmp instance"%string) n.
 
 Definition PSignedCmpUnit : PSignedCmp (unit : Type) :=
-  RecordCons "scmp" unitCmp (RecordCons "signedCmpEq" PEqUnit RecordNil).
+  RecordCons "scmp" unitCmp (RecordCons "signedCmpEq" PEqUnit (RecordCons "sle" unitLe (RecordCons "slt" unitLt RecordNil))).
 
 Definition PSignedCmpPair : forall (a : Type), forall (b : Type), PSignedCmp a -> PSignedCmp b -> PSignedCmp (prod a b) :=
-  fun (a : Type) (b : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (pb : RecordTypeCons "scmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) => RecordCons "scmp" (pairCmp a b (RecordProj pa "scmp") (RecordProj pb "scmp")) (RecordCons "signedCmpEq" (PEqPair a b (RecordProj pa "signedCmpEq") (RecordProj pb "signedCmpEq")) RecordNil).
+  fun (a : Type) (b : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (pb : RecordTypeCons "scmp" (b -> b -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (b -> b -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (b -> b -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => let var__0   := RecordProj pa "scmp" in
+  RecordCons "scmp" (pairCmp a b var__0 (RecordProj pb "scmp")) (RecordCons "signedCmpEq" (PEqPair a b (RecordProj pa "signedCmpEq") (RecordProj pb "signedCmpEq")) (RecordCons "sle" (pairLt a b var__0 (RecordProj pb "sle")) (RecordCons "slt" (pairLt a b var__0 (RecordProj pb "slt")) RecordNil))).
 
 Definition PZero : Type -> Type :=
   fun (a : Type) => a.
@@ -523,19 +548,19 @@ Definition ecFieldDiv : forall (a : Type), PField a -> a -> a -> a :=
   fun (a : Type) (pf : RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) => RecordProj pf "fieldDiv".
 
 Definition ecCeiling : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer :=
-  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "ceiling".
+  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "ceiling".
 
 Definition ecFloor : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer :=
-  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "floor".
+  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "floor".
 
 Definition ecTruncate : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer :=
-  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "trunc".
+  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "trunc".
 
 Definition ecRoundAway : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer :=
-  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundAway".
+  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundAway".
 
 Definition ecRoundToEven : forall (a : Type), PRound a -> a -> SAWCoreScaffolding.Integer :=
-  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundToEven".
+  fun (a : Type) (pr : RecordTypeCons "ceiling" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "floor" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundAway" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "roundCmp" (RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (RecordTypeCons "roundField" (RecordTypeCons "fieldDiv" (a -> a -> a) (RecordTypeCons "fieldRing" (RecordTypeCons "add" (a -> a -> a) (RecordTypeCons "int" (SAWCoreScaffolding.Integer -> a) (RecordTypeCons "mul" (a -> a -> a) (RecordTypeCons "neg" (a -> a) (RecordTypeCons "ringZero" a (RecordTypeCons "sub" (a -> a -> a) RecordTypeNil)))))) (RecordTypeCons "recip" (a -> a) RecordTypeNil))) (RecordTypeCons "roundToEven" (a -> SAWCoreScaffolding.Integer) (RecordTypeCons "trunc" (a -> SAWCoreScaffolding.Integer) RecordTypeNil))))))) => RecordProj pr "roundToEven".
 
 Definition ecLg2 : forall (n : Num), seq n SAWCoreScaffolding.Bool -> seq n SAWCoreScaffolding.Bool :=
   fun (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 SAWCoreScaffolding.Bool -> seq n1 SAWCoreScaffolding.Bool) SAWCoreVectorsAsCoqVectors.bvLg2 (SAWCoreScaffolding.error (SAWCorePrelude.Stream SAWCoreScaffolding.Bool -> SAWCorePrelude.Stream SAWCoreScaffolding.Bool) "ecLg2: expected finite word"%string) n.
@@ -556,19 +581,19 @@ Definition ecNotEq : forall (a : Type), PEq a -> a -> a -> SAWCoreScaffolding.Bo
   fun (a : Type) (pa : RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (x : a) (y : a) => SAWCoreScaffolding.not (ecEq a pa x y).
 
 Definition ecLt : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool :=
-  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => RecordProj pa "cmp" x y SAWCoreScaffolding.false.
+  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "lt".
 
 Definition ecGt : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool :=
-  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => ecLt a pa y x.
+  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (x : a) (y : a) => ecLt a pa y x.
 
 Definition ecLtEq : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool :=
-  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => SAWCoreScaffolding.not (ecLt a pa y x).
+  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "le".
 
 Definition ecGtEq : forall (a : Type), PCmp a -> a -> a -> SAWCoreScaffolding.Bool :=
-  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => SAWCoreScaffolding.not (ecLt a pa x y).
+  fun (a : Type) (pa : RecordTypeCons "cmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "cmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "le" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "lt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) (x : a) (y : a) => ecLtEq a pa y x.
 
 Definition ecSLt : forall (a : Type), PSignedCmp a -> a -> a -> SAWCoreScaffolding.Bool :=
-  fun (a : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) RecordTypeNil)) (x : a) (y : a) => RecordProj pa "scmp" x y SAWCoreScaffolding.false.
+  fun (a : Type) (pa : RecordTypeCons "scmp" (a -> a -> SAWCoreScaffolding.Bool -> SAWCoreScaffolding.Bool) (RecordTypeCons "signedCmpEq" (RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) (RecordTypeCons "sle" (a -> a -> SAWCoreScaffolding.Bool) (RecordTypeCons "slt" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil)))) => RecordProj pa "slt".
 
 Definition ecAnd : forall (a : Type), PLogic a -> a -> a -> a :=
   fun (a : Type) (pa : RecordTypeCons "and" (a -> a -> a) (RecordTypeCons "logicZero" a (RecordTypeCons "not" (a -> a) (RecordTypeCons "or" (a -> a -> a) (RecordTypeCons "xor" (a -> a -> a) RecordTypeNil))))) => RecordProj pa "and".
@@ -694,7 +719,8 @@ Definition PEqFloat : forall (e : Num), forall (p : Num), PEq (TCFloat e p) :=
   fun (e : Num) (p : Num) => RecordCons "eq" (fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: (==) Float"%string) RecordNil.
 
 Definition PCmpFloat : forall (e : Num), forall (p : Num), PCmp (TCFloat e p) :=
-  fun (e : Num) (p : Num) => RecordCons "cmp" (fun (x : unit : Type) (y : unit : Type) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string) (RecordCons "cmpEq" (PEqFloat e p) RecordNil).
+  fun (e : Num) (p : Num) => let var__0   := fun (x : unit : Type) (y : unit : Type) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string in
+  RecordCons "cmp" (fun (x : unit : Type) (y : unit : Type) (k : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.error SAWCoreScaffolding.Bool "Unimplemented: Cmp Float"%string) (RecordCons "cmpEq" (PEqFloat e p) (RecordCons "le" var__0 (RecordCons "lt" var__0 RecordNil))).
 
 Definition PZeroFloat : forall (e : Num), forall (p : Num), PZero (TCFloat e p) :=
   fun (e : Num) (p : Num) => SAWCoreScaffolding.error (TCFloat e p) "Unimplemented: Zero Float"%string.
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index 792b54e6e9..78855c23b9 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -377,12 +377,12 @@ Definition and_triv2 : forall (x : SAWCoreScaffolding.Bool), SAWCoreScaffolding.
   fun (x : SAWCoreScaffolding.Bool) => let var__0   := SAWCoreScaffolding.not SAWCoreScaffolding.true in
   SAWCoreScaffolding.iteDep (fun (b : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreScaffolding.and (SAWCoreScaffolding.not b) b) SAWCoreScaffolding.false) x (trans SAWCoreScaffolding.Bool (SAWCoreScaffolding.and var__0 SAWCoreScaffolding.true) var__0 SAWCoreScaffolding.false (and_True2 var__0) not_True) (and_False2 (SAWCoreScaffolding.not SAWCoreScaffolding.false)).
 
-Definition FalseProp : Prop :=
-  SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false.
-
 Definition EqTrue : SAWCoreScaffolding.Bool -> Prop :=
   fun (x : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool x SAWCoreScaffolding.true.
 
+Definition TrueProp : Prop :=
+  EqTrue SAWCoreScaffolding.true.
+
 Definition TrueI : EqTrue SAWCoreScaffolding.true :=
   SAWCoreScaffolding.Refl SAWCoreScaffolding.Bool SAWCoreScaffolding.true.
 
@@ -534,6 +534,9 @@ Axiom head : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVect
 
 Axiom tail : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a -> SAWCoreVectorsAsCoqVectors.Vec n a .
 
+Definition atWithDefault' : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), a -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a :=
+  fun (n_top : SAWCoreScaffolding.Nat) (a : Type) (d : a) => Nat__rec (fun (n : SAWCoreScaffolding.Nat) => SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (fun (_1 : SAWCoreVectorsAsCoqVectors.Vec 0 a) (_2 : SAWCoreScaffolding.Nat) => d) (fun (n : SAWCoreScaffolding.Nat) (rec_f : SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (v : SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a) (i : SAWCoreScaffolding.Nat) => Nat_cases a (head n a v) (fun (i_prev : SAWCoreScaffolding.Nat) (_1 : a) => rec_f (tail n a v) i_prev) i) n_top.
+
 (* Prelude.atWithDefault was skipped *)
 
 Definition sawAt : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a :=
@@ -1009,10 +1012,16 @@ Definition genBVVec : forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCore
 Definition genBVVecFromVec : forall (m : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec m a -> a -> forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), BVVec n len a :=
   fun (m : SAWCoreScaffolding.Nat) (a : Type) (v : SAWCoreVectorsAsCoqVectors.Vec m a) (def : a) (n : SAWCoreScaffolding.Nat) (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) => genBVVec n len a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (_1 : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i len) SAWCoreScaffolding.true) => SAWCoreVectorsAsCoqVectors.atWithDefault m a def v (SAWCoreVectorsAsCoqVectors.bvToNat n i)).
 
-Definition efq : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a :=
+Definition FalseProp : Prop :=
+  SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false.
+
+Definition efq : forall (a : Type), FalseProp -> a :=
   fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => let var__0   := if SAWCoreScaffolding.true then unit : Type else a in
   SAWCoreScaffolding.coerce (unit : Type) a (trans Type (unit : Type) var__0 a (sym Type var__0 (unit : Type) (ite_true Type (unit : Type) a)) (trans Type var__0 (if SAWCoreScaffolding.false then unit : Type else a) a (eq_cong SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false contra Type (fun (b : SAWCoreScaffolding.Bool) => if b then unit : Type else a)) (ite_false Type (unit : Type) a))) tt.
 
+Definition efq1 : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a :=
+  fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => SAWCoreScaffolding.Eq__rec Bit Bit1 (fun (b : Bit) (_1 : SAWCoreScaffolding.Eq Bit Bit1 b) => SAWCorePrelude.Bit_rect (fun (_2 : Bit) => Type) (unit : Type) a b) tt Bit0 (efq (SAWCoreScaffolding.Eq Bit Bit1 Bit0) contra).
+
 Definition emptyBVVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), BVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a :=
   fun (n : SAWCoreScaffolding.Nat) (a : Type) => genBVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (pf : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0)) SAWCoreScaffolding.true) => let var__0   := SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0) in
   efq a (trans SAWCoreScaffolding.Bool SAWCoreScaffolding.true var__0 SAWCoreScaffolding.false (sym SAWCoreScaffolding.Bool var__0 SAWCoreScaffolding.true pf) (not_bvult_zero n i))).
@@ -1130,8 +1139,6 @@ Definition foldIRT : forall (As : ListSort), forall (Ds : IRTSubsts As), forall
 
 (* Prelude.bindM was skipped *)
 
-(* Prelude.existsM was skipped *)
-
 (* Prelude.errorM was skipped *)
 
 Definition fmapM : forall (a : Type), forall (b : Type), (a -> b) -> CompM a -> CompM b :=
@@ -1147,6 +1154,21 @@ Definition fmapM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a
 Definition fmapM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> d) -> CompM a -> CompM b -> CompM c -> CompM d :=
   fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => applyM c d (fmapM2 a b (c -> d) f m1 m2) m3.
 
+Definition bindM2 : forall (a : Type), forall (b : Type), forall (c : Type), CompM a -> CompM b -> (a -> b -> CompM c) -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (m1 : CompM a) (m2 : CompM b) (f : a -> b -> CompM c) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)).
+
+Definition bindM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), CompM a -> CompM b -> CompM c -> (a -> b -> c -> CompM d) -> CompM d :=
+  fun (a : Type) (b : Type) (c : Type) (d : Type) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) (f : a -> b -> c -> CompM d) => @bindM CompM _ a d m1 (fun (x : a) => bindM2 b c d m2 m3 (f x)).
+
+Definition bindApplyM : forall (a : Type), forall (b : Type), (a -> CompM b) -> CompM a -> CompM b :=
+  fun (a : Type) (b : Type) (f : a -> CompM b) (m : CompM a) => @bindM CompM _ a b m f.
+
+Definition bindApplyM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a -> b -> CompM c) -> CompM a -> CompM b -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (f : a -> b -> CompM c) (m1 : CompM a) (m2 : CompM b) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)).
+
+Definition bindApplyM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> CompM d) -> CompM a -> CompM b -> CompM c -> CompM d :=
+  fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> CompM d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => bindM3 a b c d m1 m2 m3 f.
+
 Definition composeM : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> (b -> CompM c) -> a -> CompM c :=
   fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (g : b -> CompM c) (x : a) => @bindM CompM _ b c (f x) g.
 
@@ -1171,7 +1193,15 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
   let var__5   := BVVec n len3 a in
   @returnM CompM _ var__5 (SAWCoreScaffolding.coerce (BVVec n var__4 a) var__5 (eq_cong var__3 var__4 len3 pf Type (fun (l : var__3) => BVVec n l a)) (appendBVVec n len1 len2 a v1 v2))) (bvEqWithProof n var__0 len3).
 
-(* Prelude.fixM was skipped *)
+(* Prelude.existsM was skipped *)
+
+Definition orM : forall (a : Type), CompM a -> CompM a -> CompM a :=
+  fun (a : Type) (m1 : CompM a) (m2 : CompM a) => @CompM.existsM SAWCoreScaffolding.Bool a (fun (b : SAWCoreScaffolding.Bool) => if b then m1 else m2).
+
+(* Prelude.forallM was skipped *)
+
+Definition precondHint : forall (a : Type), SAWCoreScaffolding.Bool -> a -> a :=
+  fun (_1 : Type) (_2 : SAWCoreScaffolding.Bool) (a : _1) => a.
 
 (* Prelude.LetRecType was skipped *)
 
@@ -1183,14 +1213,19 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
 
 (* Prelude.lrtTupleType was skipped *)
 
-(* Prelude.multiFixM was skipped *)
-
 (* Prelude.letRecM was skipped *)
 
 Definition letRecM1 : forall (a : Type), forall (b : Type), forall (c : Type), ((a -> CompM b) -> a -> CompM b) -> ((a -> CompM b) -> CompM c) -> CompM c :=
   fun (a : Type) (b : Type) (c : Type) (fn : (a -> CompM b) -> a -> CompM b) (body : (a -> CompM b) -> CompM c) => let var__0   := a -> CompM b in
   @CompM.letRecM (CompM.LRT_Cons (CompM.LRT_Fun a (fun (_1 : a) => CompM.LRT_Ret b)) CompM.LRT_Nil) c (fun (f : var__0) => pair (fn f) tt) (fun (f : var__0) => body f).
 
+(* Prelude.fixM was skipped *)
+
+(* Prelude.multiFixM was skipped *)
+
+Definition multiArgFixM : forall (lrt : CompM.LetRecType), (CompM.lrtToType lrt -> CompM.lrtToType lrt) -> CompM.lrtToType lrt :=
+  fun (lrt : CompM.LetRecType) (F : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt -> CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_2 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => SAWCoreScaffolding.fst (@CompM.multiFixM (CompM.LRT_Cons lrt CompM.LRT_Nil) (fun (f : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => pair (F f) tt)).
+
 (* Prelude.test_fun0 was skipped *)
 
 (* Prelude.test_fun1 was skipped *)
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index c8e065f121..8eeaaf033b 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -2266,27 +2266,6 @@ lrtPi lrts b =
   (\ (lrt:LetRecType) (_:LetRecTypes) (rest:sort 0) -> lrtToType lrt -> rest)
   lrts;
 
--- Apply a function the the body of a multi-arity lrtPi function
-lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) ->
-           lrtPi lrts a -> lrtPi lrts b;
-lrtPiMap a b f lrts_top =
-  LetRecTypes#rec
-  (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b)
-  (\ (x:a) -> f x)
-  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b)
-     (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) ->
-     rec (f g))
-  lrts_top;
-
--- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions
--- that return the individual arguments
-lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) ->
-            #(lrtPi lrts a, lrtPi lrts b);
-lrtPiPair a b lrts f =
-  (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f,
-   lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f);
-
-
 -- Build the product type (lrtToType lrt1, ..., lrtToType lrtn) from the
 -- LetRecTypes list [lrt1, ..., lrtn]
 lrtTupleType : LetRecTypes -> sort 0;
@@ -2391,6 +2370,32 @@ fixM a b f x =
           (\ (g: (y:a) -> CompM (b y)) -> (f g, ()))
           (\ (g: (y:a) -> CompM (b y)) -> g x);
 
+
+-- The following commented block allows multiFixM to be defined in terms of and
+-- to reduce to letRecM, which is useful if we want to define all our automated
+-- reasoning in terms of letRecM instead of multiFixM
+
+-- Apply a function the the body of a multi-arity lrtPi function
+{-
+lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) ->
+           lrtPi lrts a -> lrtPi lrts b;
+lrtPiMap a b f lrts_top =
+  LetRecTypes#rec
+  (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b)
+  (\ (x:a) -> f x)
+  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b)
+     (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) ->
+     rec (f g))
+  lrts_top;
+
+-- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions
+-- that return the individual arguments
+lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) ->
+            #(lrtPi lrts a, lrtPi lrts b);
+lrtPiPair a b lrts f =
+  (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f,
+   lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f);
+
 -- Build a monadic function that takes in its arguments and then calls letRecM.
 -- That is, build a function
 --
@@ -2443,6 +2448,21 @@ multiFixM lrts_top F_top =
       rec (lrtPiPair (lrtToType lrt) (lrtTupleType lrts) lrts_top F).(2)))
   lrts_top
   F_top;
+-}
+
+-- Construct a fixed-point for a tuple of mutually-recursive functions
+--
+-- NOTE: Currently, Mr Solver actually works better with a primitive multiFixM,
+-- so that's what we are going to do for now...
+primitive
+multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
+            lrtTupleType lrts;
+
+-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B
+multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) ->
+               lrtToType lrt;
+multiArgFixM lrt F =
+  (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(1);
 
 
 -- Test computations

From 3929005a66da17baad9ab33d3e5b77ab0aaf1781 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 8 Mar 2022 13:13:36 -0800
Subject: [PATCH 14/15] remove old comments

---
 src/SAWScript/Prover/MRSolver/Monad.hs | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 15df3e0f0f..433a4a382f 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -246,8 +246,6 @@ asEither _ = Nothing
 -- | A map from 'Term's to 'DataTypeAssump's over that term
 type DataTypeAssumps = HashMap Term DataTypeAssump
 
--- FIXME HERE NOW: remove preconditions from MREnv
-
 -- | Parameters and locals for MR. Solver
 data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
@@ -801,7 +799,7 @@ mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 -- | Run a compuation under an additional co-inductive assumption
 withCoIndHyp :: CoIndHyp -> MRM a -> MRM a
 withCoIndHyp hyp m =
-  do debugPretty 2 ("withCoIndHypRaw" <+> ppInEmptyCtx hyp)
+  do debugPretty 2 ("withCoIndHyp" <+> ppInEmptyCtx hyp)
      hyps' <- Map.insert (coIndHypLHSFun hyp,
                           coIndHypRHSFun hyp) hyp <$> mrCoIndHyps
      local (\info -> info { mriCoIndHyps = hyps' }) m
@@ -861,11 +859,6 @@ instantiateFunAssump fassump =
      rhs <- substTermLike 0 evars $ fassumpRHS fassump
      return (args, rhs)
 
--- FIXME HERE NOW: delete this and remove the preconditions from the env
--- | Look up the precondition associated with a function name, if there is one
--- mrLookupPrecond :: FunName -> MRM (Maybe Term)
--- mrLookupPrecond nm = Map.lookup nm <$> mrePreconditions <$> mriEnv <$> ask
-
 -- | Get the precondition hint associated with a function name, by unfolding the
 -- name and checking if its body has the form
 --

From f1827565fa44eb2d98eea37dd249d29ada9af3c6 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 8 Mar 2022 13:17:52 -0800
Subject: [PATCH 15/15] add `orM` and add more `mapsToExpl`s to
 SpecialTreatment.hs

---
 saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v    | 3 +--
 .../src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs    | 6 +++---
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index 78855c23b9..8ea02a2411 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -1195,8 +1195,7 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
 
 (* Prelude.existsM was skipped *)
 
-Definition orM : forall (a : Type), CompM a -> CompM a -> CompM a :=
-  fun (a : Type) (m1 : CompM a) (m2 : CompM a) => @CompM.existsM SAWCoreScaffolding.Bool a (fun (b : SAWCoreScaffolding.Bool) => if b then m1 else m2).
+(* Prelude.orM was skipped *)
 
 (* Prelude.forallM was skipped *)
 
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index c772b7d01d..d8e61537de 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -451,11 +451,11 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("errorM",               replace (Coq.App (Coq.ExplVar "errorM")
                                        [Coq.Var "CompM", Coq.Var "_"]))
   , ("catchM",               skip)
-  , ("existsM",              mapsTo compMModule "existsM")
-  , ("forallM",              mapsTo compMModule "forallM")
+  , ("existsM",              mapsToExpl compMModule "existsM")
+  , ("forallM",              mapsToExpl compMModule "forallM")
+  , ("orM",                  mapsToExpl compMModule "orM")
   , ("fixM",                 replace (Coq.App (Coq.ExplVar "fixM")
                                        [Coq.Var "CompM", Coq.Var "_"]))
-  , ("existsM",              mapsToExpl compMModule "existsM")
   , ("LetRecType",           mapsTo compMModule "LetRecType")
   , ("LRT_Ret",              mapsTo compMModule "LRT_Ret")
   , ("LRT_Fun",              mapsTo compMModule "LRT_Fun")