From a27cdc79486fa44e11daeaa641737c03fecade67 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Wed, 23 Feb 2022 13:13:29 -0800
Subject: [PATCH 1/7] move unchanging bits of MRState to new MRInfo, add
 CoIndHyp

---
 src/SAWScript/Prover/MRSolver/Monad.hs  | 126 +++++++++++++++++-------
 src/SAWScript/Prover/MRSolver/SMT.hs    |   2 +-
 src/SAWScript/Prover/MRSolver/Solver.hs |   4 +-
 3 files changed, 93 insertions(+), 39 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index b89e3ae1c1..2a67b74955 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -163,6 +164,26 @@ asEVarApp var_map (asExtCnsApp -> Just (ec, args))
     Just (MRVar ec, args, maybe_inst)
 asEVarApp _ _ = Nothing
 
+-- | A co-inductive hypothesis of the form:
+--
+-- > forall x1, ..., xn. F y1 ... ym |= G z1 ... zl
+--
+-- for some universal context @x1:T1, ..., xn:Tn@ and some lists of argument
+-- expressions @y1, ..., ym@ and @z1, ..., zl@ over the universal context.
+data CoIndHyp = CoIndHyp {
+  -- | 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
+  coIndHypCtx :: [(LocalName,Term)],
+  -- | The LHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
+  coIndHypLHS :: [Term],
+  -- | The RHS argument expressions @y1, ..., ym@ over the 'coIndHypCtx' uvars
+  coIndHypRHS :: [Term] }
+
+-- | A map from pairs of function names to co-inductive hypotheses over those
+-- names
+type CoIndHyps = Map (FunName, FunName) CoIndHyp
+
 -- | An assumption that a named function refines some specificaiton. This has
 -- the form
 --
@@ -181,42 +202,45 @@ data FunAssump = FunAssump {
   -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars
   fassumpRHS :: NormComp }
 
--- | State maintained by MR. Solver
-data MRState = MRState {
+-- | A map from function names to function refinement assumptions over that
+-- name
+type FunAssumps = Map FunName FunAssump
+
+-- | Parameters for MR. Solver
+data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
   mrSC :: SharedContext,
   -- | SMT timeout for SMT calls made by Mr. Solver
   mrSMTTimeout :: Maybe Integer,
+  -- | The debug level, which controls debug printing
+  mrDebugLevel :: Int,
+  -- | The set of function refinements to be assumed by to Mr. Solver
+  mrFunAssumps :: FunAssumps
+}
+
+-- | State maintained by MR. Solver
+data MRState = MRState {
   -- | The context of universal variables, which are free SAW core variables, in
   -- order from innermost to outermost, i.e., where element @0@ corresponds to
   -- deBruijn index @0@
   mrUVars :: [(LocalName,Type)],
   -- | The existential and letrec-bound variables
   mrVars :: MRVarMap,
-  -- | The current assumptions of function refinement
-  mrFunAssumps :: Map FunName FunAssump,
+  -- | The current set of co-inductive hypotheses
+  mrCoIndHyps :: CoIndHyps,
   -- | The current assumptions, which are conjoined into a single Boolean term;
   -- note that these have the current UVars free
-  mrAssumptions :: Term,
-  -- | The debug level, which controls debug printing
-  mrDebugLevel :: Int
+  mrAssumptions :: Term
 }
 
--- | Build a default, empty state from SMT configuration parameters and a set of
--- function refinement assumptions
-mkMRState :: SharedContext -> Map FunName FunAssump ->
-             Maybe Integer -> Int -> IO MRState
-mkMRState sc fun_assumps timeout dlvl =
-  scBool sc True >>= \true_tm ->
-  return $ MRState { mrSC = sc,
-                     mrSMTTimeout = timeout, mrUVars = [], mrVars = Map.empty,
-                     mrFunAssumps = fun_assumps, mrAssumptions = true_tm,
-                     mrDebugLevel = dlvl }
-
--- | Mr. Monad, the monad used by MR. Solver, which is the state-exception monad
-newtype MRM a = MRM { unMRM :: StateT MRState (ExceptT MRFailure IO) a }
+-- | Mr. Monad, the monad used by MR. Solver, which has 'MRInfo' as as a
+-- shared environment, 'MRState' as state, and 'MRFailure' as an exception
+-- type, all over an 'IO' monad
+newtype MRM a = MRM { unMRM :: ReaderT MRInfo (StateT MRState
+                                              (ExceptT MRFailure IO)) a }
               deriving (Functor, Applicative, Monad, MonadIO,
-                        MonadState MRState, MonadError MRFailure)
+                        MonadReader MRInfo, MonadState MRState,
+                                            MonadError MRFailure)
 
 instance MonadTerm MRM where
   mkTermF = liftSC1 scTermF
@@ -225,8 +249,12 @@ instance MonadTerm MRM where
   substTerm = liftSC3 instantiateVarList
 
 -- | Run an 'MRM' computation and return a result or an error
-runMRM :: MRState -> MRM a -> IO (Either MRFailure a)
-runMRM init_st m = runExceptT $ flip evalStateT init_st $ unMRM m
+runMRM :: MRInfo -> MRM a -> IO (Either MRFailure a)
+runMRM init_info m =
+  do true_tm <- scBool (mrSC init_info) True
+     let init_st = MRState { mrUVars = [], mrVars = Map.empty,
+                             mrAssumptions = true_tm, mrCoIndHyps = Map.empty }
+     runExceptT $ flip evalStateT init_st $ flip runReaderT init_info $ unMRM m
 
 -- | Apply a function to any failure thrown by an 'MRM' computation
 mapFailure :: (MRFailure -> MRFailure) -> MRM a -> MRM a
@@ -255,29 +283,29 @@ catchErrorEither m = catchError (Right <$> m) (return . Left)
 
 -- | Lift a nullary SharedTerm computation into 'MRM'
 liftSC0 :: (SharedContext -> IO a) -> MRM a
-liftSC0 f = (mrSC <$> get) >>= \sc -> liftIO (f sc)
+liftSC0 f = (mrSC <$> ask) >>= \sc -> liftIO (f sc)
 
 -- | Lift a unary SharedTerm computation into 'MRM'
 liftSC1 :: (SharedContext -> a -> IO b) -> a -> MRM b
-liftSC1 f a = (mrSC <$> get) >>= \sc -> liftIO (f sc a)
+liftSC1 f a = (mrSC <$> ask) >>= \sc -> liftIO (f sc a)
 
 -- | Lift a binary SharedTerm computation into 'MRM'
 liftSC2 :: (SharedContext -> a -> b -> IO c) -> a -> b -> MRM c
-liftSC2 f a b = (mrSC <$> get) >>= \sc -> liftIO (f sc a b)
+liftSC2 f a b = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b)
 
 -- | Lift a ternary SharedTerm computation into 'MRM'
 liftSC3 :: (SharedContext -> a -> b -> c -> IO d) -> a -> b -> c -> MRM d
-liftSC3 f a b c = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c)
+liftSC3 f a b c = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c)
 
 -- | Lift a quaternary SharedTerm computation into 'MRM'
 liftSC4 :: (SharedContext -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d ->
            MRM e
-liftSC4 f a b c d = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d)
+liftSC4 f a b c d = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c d)
 
 -- | Lift a quinary SharedTerm computation into 'MRM'
 liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) ->
            a -> b -> c -> d -> e -> MRM f
-liftSC5 f a b c d e = (mrSC <$> get) >>= \sc -> liftIO (f sc a b c d e)
+liftSC5 f a b c d e = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c d e)
 
 
 ----------------------------------------------------------------------
@@ -624,9 +652,38 @@ mrSubstEVarsStrict top_t =
 _mrSubstEVarsStrict :: Term -> MRM (Maybe Term)
 _mrSubstEVarsStrict = mrSubstEVarsStrict
 
+-- | Get the 'CoIndHyp' for a pair of 'FunName's, if there is one
+mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
+mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps <$> get
+
+-- | Run a computation under the additional co-inductive assumption that a
+-- named function applied to some arguments refines another named function
+-- applied some arguments, where all the aforementioned arguments are 'Term's
+-- that can have the current uvars free
+withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
+withCoIndHyp nm1 args1 nm2 args2 m =
+  do mrDebugPPPrefixSep 1 "withCoIndHyp" (FunBind nm1 args1 CompFunReturn)
+                                    "|=" (FunBind nm2 args2 CompFunReturn)
+     ctx <- mrUVarCtx
+     hyps <- mrCoIndHyps <$> get
+     let hyps' = Map.insert (nm1, nm2) (CoIndHyp ctx args1 args2) hyps
+     modify (\s -> s { mrCoIndHyps = hyps' })
+     ret <- m
+     modify (\s -> s { mrCoIndHyps = hyps })
+     return ret
+
+-- | Generate fresh evars for the context of a 'CoIndHyp' and
+-- substitute them into its arguments and right-hand side
+instantiateCoIndHyp :: CoIndHyp -> MRM ([Term], [Term])
+instantiateCoIndHyp (CoIndHyp {..}) =
+  do evars <- mrFreshEVars coIndHypCtx
+     lhs <- substTermLike 0 evars coIndHypLHS
+     rhs <- substTermLike 0 evars coIndHypRHS
+     return (lhs, rhs)
+
 -- | Look up the 'FunAssump' for a 'FunName', if there is one
 mrGetFunAssump :: FunName -> MRM (Maybe FunAssump)
-mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps <$> get
+mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps <$> ask
 
 -- | Run a computation under the additional assumption that a named function
 -- applied to a list of arguments refines a given right-hand side, all of which
@@ -636,12 +693,9 @@ withFunAssump fname args rhs m =
   do mrDebugPPPrefixSep 1 "withFunAssump" (FunBind
                                            fname args CompFunReturn) "|=" rhs
      ctx <- mrUVarCtx
-     assumps <- mrFunAssumps <$> get
+     assumps <- mrFunAssumps <$> ask
      let assumps' = Map.insert fname (FunAssump ctx args rhs) assumps
-     modify (\s -> s { mrFunAssumps = assumps' })
-     ret <- m
-     modify (\s -> s { mrFunAssumps = assumps })
-     return ret
+     local (\info -> info { mrFunAssumps = assumps' }) m
 
 -- | Generate fresh evars for the context of a 'FunAssump' and substitute them
 -- into its arguments and right-hand side
@@ -666,7 +720,7 @@ withAssumption phi m =
 -- | Print a 'String' if the debug level is at least the supplied 'Int'
 debugPrint :: Int -> String -> MRM ()
 debugPrint i str =
-  (mrDebugLevel <$> get) >>= \lvl ->
+  (mrDebugLevel <$> ask) >>= \lvl ->
   if lvl >= i then liftIO (hPutStrLn stderr str) else return ()
 
 -- | Print a document if the debug level is at least the supplied 'Int'
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index ed318a1455..c528714506 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -162,7 +162,7 @@ normSMTProp t =
 -- FIXME: use the timeout!
 mrProvableRaw :: Term -> MRM Bool
 mrProvableRaw prop_term =
-  do sc <- mrSC <$> get
+  do sc <- mrSC <$> ask
      prop <- liftSC1 termToProp prop_term
      unints <- Set.map ecVarIndex <$> getAllExtSet <$> liftSC1 propToTerm prop
      debugPrint 2 ("Calling SMT solver with proposition: " ++
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 2f55d31c02..3cffd15b4f 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -602,10 +602,10 @@ askMRSolver ::
 askMRSolver sc dlvl timeout t1 t2 =
   do tp1 <- scTypeOf sc t1 >>= scWhnf sc
      tp2 <- scTypeOf sc t2 >>= scWhnf sc
-     init_st <- mkMRState sc Map.empty timeout dlvl
+     let init_info = MRInfo sc timeout dlvl Map.empty
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->
-         fmap (either Just (const Nothing)) $ runMRM init_st $
+         fmap (either Just (const Nothing)) $ runMRM init_info $
          withUVars uvar_ctx $ \vars ->
          do tps_are_eq <- mrConvertible tp1 tp2
             if tps_are_eq then return () else

From 31e3891cbc999e213bc8c9423b823ceb076fbf62 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Wed, 23 Feb 2022 13:30:38 -0800
Subject: [PATCH 2/7] use CoIndHyps instead of FunAssumps for co-induction in
 mrRefines'

---
 src/SAWScript/Prover/MRSolver/Solver.hs | 31 ++++++++++++++++---------
 1 file changed, 20 insertions(+), 11 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 3cffd15b4f..1299e8ef75 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -454,11 +454,21 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   mrConvertible tp1 tp2 >>= \tps_eq ->
   mrFunBodyRecInfo f1 args1 >>= \maybe_f1_body ->
   mrFunBodyRecInfo f2 args2 >>= \maybe_f2_body ->
-  mrGetFunAssump f1 >>= \case
+  mrGetCoIndHyp f1 f2 >>= \maybe_coIndHyp ->
+  mrGetFunAssump f1 >>= \maybe_fassump ->
+  case (maybe_coIndHyp, maybe_fassump) of
+
+  -- If we have a co-inductive assumption that f1 args1' |= f2 args2', then
+  -- prove that args1 = args1' and args2 = args2', and then that k1 |= k2
+  (Just coIndHyp, _) ->
+    do (args1', args2') <- instantiateCoIndHyp coIndHyp
+       zipWithM_ mrProveEq args1' args1
+       zipWithM_ mrProveEq args2' args2
+       mrRefinesFun k1 k2
 
   -- If we have an assumption that f1 args' refines some rhs, then prove that
   -- args1 = args' and then that rhs refines m2
-  Just fassump ->
+  (_, Just fassump) ->
     do (assump_args, assump_rhs) <- instantiateFunAssump fassump
        zipWithM_ mrProveEq assump_args args1
        m1' <- normBind assump_rhs k1
@@ -472,16 +482,15 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   _ | Just (f2_body, False) <- maybe_f2_body ->
       normBindTerm f2_body k2 >>= \m2' -> mrRefines m1 m2'
 
-  -- If we do not already have an assumption that f1 refines some specification,
-  -- and both f1 and f2 are recursive but have the same return type, then try to
-  -- coinductively prove that f1 args1 |= f2 args2 under the assumption that f1
-  -- args1 |= f2 args2, and then try to prove that k1 |= k2
-  Nothing
-    | tps_eq
+  -- If we don't have a co-inducitve hypothesis for f1 and f2, don't have an
+  -- assumption that f1 refines some specification, and both f1 and f2 are
+  -- recursive and have the same return type, then try to coinductively prove
+  -- 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 withFunAssump f1 args1 (FunBind f2 args2 CompFunReturn) $
-           mrRefines f1_body f2_body
+      do withCoIndHyp f1 args1 f2 args2 $ mrRefines f1_body f2_body
          mrRefinesFun k1 k2
 
   -- If we cannot line up f1 and f2, then making progress here would require us
@@ -489,7 +498,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   -- related to the function call on the other side and k' is related to the
   -- continuation on the other side, but we don't know how to do that, so give
   -- up
-  Nothing ->
+  _ ->
     throwError (CompsDoNotRefine m1 m2)
 
 {- FIXME: handle FunBind on just one side

From c078db1067fc4ccb1242d9c966003c2c2428bd39 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Wed, 23 Feb 2022 15:26:42 -0800
Subject: [PATCH 3/7] add mrAssertProveEq, add CoIndMismatch failures

---
 src/SAWScript/Prover/MRSolver/Monad.hs  | 15 +++++++++++++--
 src/SAWScript/Prover/MRSolver/SMT.hs    | 15 ++++++++++-----
 src/SAWScript/Prover/MRSolver/Solver.hs | 19 +++++++++++--------
 3 files changed, 34 insertions(+), 15 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 2a67b74955..d72856636a 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -66,6 +66,8 @@ data MRFailure
   | MalformedDefsFun Term
   | MalformedComp Term
   | NotCompFunType Term
+  | CoIndHypMismatchWidened FunName FunName CoIndHyp
+  | CoIndHypMismatchFailure (NormComp, NormComp) (NormComp, NormComp)
     -- | A local variable binding
   | MRFailureLocalVar LocalName MRFailure
     -- | Information about the context of the failure
@@ -122,6 +124,13 @@ instance PrettyInCtx MRFailure where
     ppWithPrefix "Could not handle computation:" t
   prettyInCtx (NotCompFunType tp) =
     ppWithPrefix "Not a computation or computational function type:" tp
+  prettyInCtx (CoIndHypMismatchWidened nm1 nm2 _) =
+    ppWithPrefixSep "[Internal] Trying to widen co-inductive hypothesis on:" nm1 "," nm2
+  prettyInCtx (CoIndHypMismatchFailure (tm1, tm2) (tm1', tm2')) =
+    vsepM [return "Could not match co-inductive hypotheis:",
+           ppWithPrefixSep "" tm1' "|=" tm2',
+           return "with goal:",
+           ppWithPrefixSep "" tm1 "|=" tm2]
   prettyInCtx (MRFailureLocalVar x err) =
     local (x:) $ prettyInCtx err
   prettyInCtx (MRFailureCtx ctx err) =
@@ -178,7 +187,8 @@ 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]
+} deriving Show
 
 -- | A map from pairs of function names to co-inductive hypotheses over those
 -- names
@@ -200,7 +210,8 @@ data FunAssump = FunAssump {
   -- | The argument expressions @e1, ..., en@ over the 'fassumpCtx' uvars
   fassumpArgs :: [Term],
   -- | The right-hand side upper bound @m@ over the 'fassumpCtx' uvars
-  fassumpRHS :: NormComp }
+  fassumpRHS :: NormComp
+}
 
 -- | A map from function names to function refinement assumptions over that
 -- name
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index c528714506..78ffc14420 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -262,16 +262,21 @@ mrProveEqSimple eqf t1 t2 =
      t2' <- mrSubstEVars t2
      TermInCtx [] <$> eqf t1' t2'
 
-
--- | Prove that two terms are equal, instantiating evars if necessary, or
--- throwing an error if this is not possible
-mrProveEq :: Term -> Term -> MRM ()
+-- | Prove that two terms are equal, instantiating evars if necessary,
+-- returning true on success
+mrProveEq :: Term -> Term -> MRM Bool
 mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
      tp <- mrTypeOf t1
      varmap <- mrVars <$> get
      cond_in_ctx <- mrProveEqH varmap tp t1 t2
-     success <- withTermInCtx cond_in_ctx mrProvable
+     withTermInCtx cond_in_ctx mrProvable
+
+-- | Prove that two terms are equal, instantiating evars if necessary, or
+-- throwing an error if this is not possible
+mrAssertProveEq :: Term -> Term -> MRM ()
+mrAssertProveEq t1 t2 =
+  do success <- mrProveEq t1 t2
      if success then return () else
        throwError (TermsNotEq t1 t2)
 
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 1299e8ef75..ffa8b41086 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -366,7 +366,7 @@ mrRefines t1 t2 =
 
 -- | The main implementation of 'mrRefines'
 mrRefines' :: NormComp -> NormComp -> MRM ()
-mrRefines' (ReturnM e1) (ReturnM e2) = mrProveEq e1 e2
+mrRefines' (ReturnM e1) (ReturnM e2) = mrAssertProveEq e1 e2
 mrRefines' (ErrorM _) (ErrorM _) = return ()
 mrRefines' (ReturnM e) (ErrorM _) = throwError (ReturnNotError e)
 mrRefines' (ErrorM _) (ReturnM e) = throwError (ReturnNotError e)
@@ -445,7 +445,7 @@ mrRefines' (FunBind (EVarFunName evar) args CompFunReturn) m2 =
 
 mrRefines' (FunBind (LetRecName f) args1 k1) (FunBind (LetRecName f') args2 k2)
   | f == f' && length args1 == length args2 =
-    zipWithM_ mrProveEq args1 args2 >>
+    zipWithM_ mrAssertProveEq args1 args2 >>
     mrRefinesFun k1 k2
 
 mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
@@ -462,15 +462,18 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   -- prove that args1 = args1' and args2 = args2', and then that k1 |= k2
   (Just coIndHyp, _) ->
     do (args1', args2') <- instantiateCoIndHyp coIndHyp
-       zipWithM_ mrProveEq args1' args1
-       zipWithM_ mrProveEq args2' args2
-       mrRefinesFun k1 k2
+       eq1 <- and <$> zipWithM mrProveEq args1' args1
+       eq2 <- and <$> zipWithM mrProveEq args2' args2
+       if eq1 && eq2 then mrRefinesFun k1 k2
+       else let m1' = FunBind f1 args1' CompFunReturn
+                m2' = FunBind f2 args2' CompFunReturn
+             in throwError (CoIndHypMismatchFailure (m1, m2) (m1', m2'))
 
   -- If we have an assumption that f1 args' refines some rhs, then prove that
   -- args1 = args' and then that rhs refines m2
   (_, Just fassump) ->
     do (assump_args, assump_rhs) <- instantiateFunAssump fassump
-       zipWithM_ mrProveEq assump_args args1
+       zipWithM_ mrAssertProveEq assump_args args1
        m1' <- normBind assump_rhs k1
        mrRefines m1' m2
 
@@ -508,7 +511,7 @@ mrRefines' m1@(FunBind f@(GlobalName _) args k1) m2 =
     -- If we have an assumption that f args' refines some rhs, then prove that
     -- args = args' and then that rhs refines m2
     do (assump_args, assump_rhs) <- instantiateFunAssump fassump
-       zipWithM_ mrProveEq assump_args args
+       zipWithM_ mrAssertProveEq assump_args args
        m1' <- normBind assump_rhs k1
        mrRefines m1' m2
   Nothing ->
@@ -525,7 +528,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2 =
   -- args1 = args' and then that rhs refines m2
   Just fassump ->
     do (assump_args, assump_rhs) <- instantiateFunAssump fassump
-       zipWithM_ mrProveEq assump_args args1
+       zipWithM_ mrAssertProveEq assump_args args1
        m1' <- normBind assump_rhs k1
        mrRefines m1' m2
 

From 82a8b0dd7eb8f32f1440d1383384e0da60b0545a Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 24 Feb 2022 10:56:31 -0800
Subject: [PATCH 4/7] move all but mrVars to MRInfo, make withCoIndHyp catch
 errs and recurse

---
 src/SAWScript/Prover/MRSolver/Monad.hs  | 105 +++++++++++++-----------
 src/SAWScript/Prover/MRSolver/SMT.hs    |   2 +-
 src/SAWScript/Prover/MRSolver/Solver.hs |   4 +-
 3 files changed, 60 insertions(+), 51 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index d72856636a..de89c8c0a9 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -217,7 +217,7 @@ data FunAssump = FunAssump {
 -- name
 type FunAssumps = Map FunName FunAssump
 
--- | Parameters for MR. Solver
+-- | Parameters and locals for MR. Solver
 data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
   mrSC :: SharedContext,
@@ -226,17 +226,11 @@ data MRInfo = MRInfo {
   -- | The debug level, which controls debug printing
   mrDebugLevel :: Int,
   -- | The set of function refinements to be assumed by to Mr. Solver
-  mrFunAssumps :: FunAssumps
-}
-
--- | State maintained by MR. Solver
-data MRState = MRState {
-  -- | The context of universal variables, which are free SAW core variables, in
-  -- order from innermost to outermost, i.e., where element @0@ corresponds to
-  -- deBruijn index @0@
+  mrFunAssumps :: FunAssumps,
+  -- | The current context of universal variables, which are free SAW core
+  -- variables, in order from innermost to outermost, i.e., where element @0@
+  -- corresponds to deBruijn index @0@
   mrUVars :: [(LocalName,Type)],
-  -- | The existential and letrec-bound variables
-  mrVars :: MRVarMap,
   -- | The current set of co-inductive hypotheses
   mrCoIndHyps :: CoIndHyps,
   -- | The current assumptions, which are conjoined into a single Boolean term;
@@ -244,6 +238,12 @@ data MRState = MRState {
   mrAssumptions :: Term
 }
 
+-- | State maintained by MR. Solver
+data MRState = MRState {
+  -- | The existential and letrec-bound variables
+  mrVars :: MRVarMap
+}
+
 -- | Mr. Monad, the monad used by MR. Solver, which has 'MRInfo' as as a
 -- shared environment, 'MRState' as state, and 'MRFailure' as an exception
 -- type, all over an 'IO' monad
@@ -260,11 +260,15 @@ instance MonadTerm MRM where
   substTerm = liftSC3 instantiateVarList
 
 -- | Run an 'MRM' computation and return a result or an error
-runMRM :: MRInfo -> MRM a -> IO (Either MRFailure a)
-runMRM init_info m =
-  do true_tm <- scBool (mrSC init_info) True
-     let init_st = MRState { mrUVars = [], mrVars = Map.empty,
-                             mrAssumptions = true_tm, mrCoIndHyps = Map.empty }
+runMRM :: SharedContext -> Maybe Integer -> Int -> FunAssumps ->
+          MRM a -> IO (Either MRFailure a)
+runMRM sc timeout debug assumps m =
+  do true_tm <- scBool sc True
+     let init_info = MRInfo { mrSC = sc, mrSMTTimeout = timeout,
+                              mrDebugLevel = debug, mrFunAssumps = assumps,
+                              mrUVars = [], mrCoIndHyps = Map.empty,
+                              mrAssumptions = true_tm }
+     let init_st = MRState { mrVars = Map.empty }
      runExceptT $ flip evalStateT init_st $ flip runReaderT init_info $ unMRM m
 
 -- | Apply a function to any failure thrown by an 'MRM' computation
@@ -358,7 +362,7 @@ mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize
 -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in
 -- the order as seen "from the outside"
 mrUVarCtx :: MRM [(LocalName,Term)]
-mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars <$> get
+mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars <$> ask
 
 -- | Get the type of a 'Term' in the current uvar context
 mrTypeOf :: Term -> MRM Term
@@ -399,15 +403,12 @@ uniquifyName nm nms =
 -- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
 withUVar nm tp m =
-  do st <- get
-     let nm' = uniquifyName nm (map fst $ mrUVars st)
-     assumps' <- liftTerm 0 1 $ mrAssumptions st
-     put (st { mrUVars = (nm',tp) : mrUVars st,
-               mrAssumptions = assumps' })
-     ret <- mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
-     modify (\st' -> st' { mrUVars = mrUVars st,
-                           mrAssumptions = mrAssumptions st })
-     return ret
+  do info <- ask
+     let nm' = uniquifyName nm (map fst $ mrUVars info)
+     assumps' <- liftTerm 0 1 $ mrAssumptions info
+     local (\_ -> info { mrUVars = (nm',tp) : mrUVars info,
+                         mrAssumptions = assumps' }) $
+       mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
 
 -- | Run a MR Solver computation in a context extended with a universal variable
 -- and pass it the lifting (in the sense of 'incVars') of an MR Solver term
@@ -436,7 +437,7 @@ withUVars = helper [] where
 -- most recently bound
 getAllUVarTerms :: MRM [Term]
 getAllUVarTerms =
-  (length <$> mrUVars <$> get) >>= \len ->
+  (length <$> mrUVars <$> ask) >>= \len ->
   mapM (liftSC1 scLocalVar) [len-1, len-2 .. 0]
 
 -- | Lambda-abstract all the current uvars out of a 'Term', with the least
@@ -665,23 +666,34 @@ _mrSubstEVarsStrict = mrSubstEVarsStrict
 
 -- | Get the 'CoIndHyp' for a pair of 'FunName's, if there is one
 mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
-mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps <$> get
-
--- | Run a computation under the additional co-inductive assumption that a
--- named function applied to some arguments refines another named function
--- applied some arguments, where all the aforementioned arguments are 'Term's
--- that can have the current uvars free
+mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps <$> ask
+
+-- | 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. This is done recursively, meaning this
+-- function will only return once no 'CoIndHypMismatchWidened' errors are
+-- raised with the given names.
 withCoIndHyp :: FunName -> [Term] -> FunName -> [Term] -> MRM a -> MRM a
 withCoIndHyp nm1 args1 nm2 args2 m =
+  do ctx <- mrUVarCtx
+     withCoIndHyp' (nm1, nm2) (CoIndHyp ctx args1 args2) m
+
+-- | The main loop of 'withCoIndHyp'
+withCoIndHyp' :: (FunName, FunName) -> CoIndHyp -> MRM a -> MRM a
+withCoIndHyp' (nm1, nm2) hyp@(CoIndHyp _ args1 args2) m =
   do mrDebugPPPrefixSep 1 "withCoIndHyp" (FunBind nm1 args1 CompFunReturn)
                                     "|=" (FunBind nm2 args2 CompFunReturn)
-     ctx <- mrUVarCtx
-     hyps <- mrCoIndHyps <$> get
-     let hyps' = Map.insert (nm1, nm2) (CoIndHyp ctx args1 args2) hyps
-     modify (\s -> s { mrCoIndHyps = hyps' })
-     ret <- m
-     modify (\s -> s { mrCoIndHyps = hyps })
-     return ret
+     st <- get
+     hyps' <- Map.insert (nm1, nm2) hyp <$> mrCoIndHyps <$> ask
+     (local (\info -> info { mrCoIndHyps = hyps' }) m) `catchError` \case
+       CoIndHypMismatchWidened nm1' nm2' hyp' | nm1 == nm1' && nm2 == nm2'
+         -> -- FIXME: Could restoring the state here cause any problems?
+            put st >> withCoIndHyp' (nm1, nm2) hyp' m
+       e -> throwError e
 
 -- | Generate fresh evars for the context of a 'CoIndHyp' and
 -- substitute them into its arguments and right-hand side
@@ -721,12 +733,9 @@ instantiateFunAssump fassump =
 -- executing a sub-computation
 withAssumption :: Term -> MRM a -> MRM a
 withAssumption phi m =
-  do assumps <- mrAssumptions <$> get
+  do assumps <- mrAssumptions <$> ask
      assumps' <- liftSC2 scAnd phi assumps
-     modify (\s -> s { mrAssumptions = assumps' })
-     ret <- m
-     modify (\s -> s { mrAssumptions = assumps })
-     return ret
+     local (\info -> info { mrAssumptions = assumps' }) m
 
 -- | Print a 'String' if the debug level is at least the supplied 'Int'
 debugPrint :: Int -> String -> MRM ()
@@ -742,19 +751,19 @@ debugPretty i pp = debugPrint i $ renderSawDoc defaultPPOpts pp
 -- at least the supplied 'Int'
 debugPrettyInCtx :: PrettyInCtx a => Int -> a -> MRM ()
 debugPrettyInCtx i a =
-  (mrUVars <$> get) >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
+  (mrUVars <$> ask) >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
 
 -- | Pretty-print an object relative to the current context
 mrPPInCtx :: PrettyInCtx a => a -> MRM SawDoc
 mrPPInCtx a =
-  runReader (prettyInCtx a) <$> map fst <$> mrUVars <$> get
+  runReader (prettyInCtx a) <$> map fst <$> mrUVars <$> ask
 
 -- | Pretty-print the result of 'ppWithPrefixSep' relative to the current uvar
 -- context to 'stderr' if the debug level is at least the 'Int' provided
 mrDebugPPPrefixSep :: PrettyInCtx a => Int -> String -> a -> String -> a ->
                       MRM ()
 mrDebugPPPrefixSep i pre a1 sp a2 =
-  (mrUVars <$> get) >>= \ctx ->
+  (mrUVars <$> ask) >>= \ctx ->
   debugPretty i $
   flip runReader (map fst ctx) (group <$> nest 2 <$>
                                 ppWithPrefixSep pre a1 sp a2)
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index 78ffc14420..363309b620 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -180,7 +180,7 @@ mrProvableRaw prop_term =
 -- assumptions
 mrProvable :: Term -> MRM Bool
 mrProvable bool_tm =
-  do assumps <- mrAssumptions <$> get
+  do assumps <- mrAssumptions <$> ask
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
      prop_inst <- flip instantiateUVarsM prop $ \nm tp ->
        liftSC1 scWhnf tp >>= \case
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index ffa8b41086..66defa2ded 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -614,10 +614,10 @@ askMRSolver ::
 askMRSolver sc dlvl timeout t1 t2 =
   do tp1 <- scTypeOf sc t1 >>= scWhnf sc
      tp2 <- scTypeOf sc t2 >>= scWhnf sc
-     let init_info = MRInfo sc timeout dlvl Map.empty
      case asPiList tp1 of
        (uvar_ctx, asCompM -> Just _) ->
-         fmap (either Just (const Nothing)) $ runMRM init_info $
+         fmap (either Just (const Nothing)) $
+         runMRM sc timeout dlvl Map.empty $
          withUVars uvar_ctx $ \vars ->
          do tps_are_eq <- mrConvertible tp1 tp2
             if tps_are_eq then return () else

From becee3bda3d3cc2f4d9f0dd285d60358e88e5b2e Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 24 Feb 2022 11:04:44 -0800
Subject: [PATCH 5/7] refactor MRInfo, MRState to make ask/get interface nicer

---
 src/SAWScript/Prover/MRSolver/Monad.hs | 122 +++++++++++++++----------
 src/SAWScript/Prover/MRSolver/SMT.hs   |   9 +-
 2 files changed, 80 insertions(+), 51 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index de89c8c0a9..2b6804f7e4 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -220,28 +220,28 @@ type FunAssumps = Map FunName FunAssump
 -- | Parameters and locals for MR. Solver
 data MRInfo = MRInfo {
   -- | Global shared context for building terms, etc.
-  mrSC :: SharedContext,
+  mriSC :: SharedContext,
   -- | SMT timeout for SMT calls made by Mr. Solver
-  mrSMTTimeout :: Maybe Integer,
+  mriSMTTimeout :: Maybe Integer,
   -- | The debug level, which controls debug printing
-  mrDebugLevel :: Int,
+  mriDebugLevel :: Int,
   -- | The set of function refinements to be assumed by to Mr. Solver
-  mrFunAssumps :: FunAssumps,
+  mriFunAssumps :: FunAssumps,
   -- | The current context of universal variables, which are free SAW core
   -- variables, in order from innermost to outermost, i.e., where element @0@
   -- corresponds to deBruijn index @0@
-  mrUVars :: [(LocalName,Type)],
+  mriUVars :: [(LocalName,Type)],
   -- | The current set of co-inductive hypotheses
-  mrCoIndHyps :: CoIndHyps,
+  mriCoIndHyps :: CoIndHyps,
   -- | The current assumptions, which are conjoined into a single Boolean term;
   -- note that these have the current UVars free
-  mrAssumptions :: Term
+  mriAssumptions :: Term
 }
 
 -- | State maintained by MR. Solver
 data MRState = MRState {
   -- | The existential and letrec-bound variables
-  mrVars :: MRVarMap
+  mrsVars :: MRVarMap
 }
 
 -- | Mr. Monad, the monad used by MR. Solver, which has 'MRInfo' as as a
@@ -253,6 +253,38 @@ newtype MRM a = MRM { unMRM :: ReaderT MRInfo (StateT MRState
                         MonadReader MRInfo, MonadState MRState,
                                             MonadError MRFailure)
 
+-- | Get the current value of 'mriSC'
+mrSC :: MRM SharedContext
+mrSC = mriSC <$> ask
+
+-- | Get the current value of 'mrSMTTimeout'
+mrSMTTimeout :: MRM (Maybe Integer)
+mrSMTTimeout = mriSMTTimeout <$> ask
+
+-- | Get the current value of 'mrDebugLevel'
+mrDebugLevel :: MRM Int
+mrDebugLevel = mriDebugLevel <$> ask
+
+-- | Get the current value of 'mrFunAssumps'
+mrFunAssumps :: MRM FunAssumps
+mrFunAssumps = mriFunAssumps <$> ask
+
+-- | Get the current value of 'mrUVars'
+mrUVars :: MRM [(LocalName,Type)]
+mrUVars = mriUVars <$> ask
+
+-- | Get the current value of 'mrCoIndHyps'
+mrCoIndHyps :: MRM CoIndHyps
+mrCoIndHyps = mriCoIndHyps <$> ask
+
+-- | Get the current value of 'mrAssumptions'
+mrAssumptions :: MRM Term
+mrAssumptions = mriAssumptions <$> ask
+
+-- | Get the current value of 'mrVars'
+mrVars :: MRM MRVarMap
+mrVars = mrsVars <$> get
+
 instance MonadTerm MRM where
   mkTermF = liftSC1 scTermF
   liftTerm = liftSC3 incVars
@@ -264,11 +296,11 @@ runMRM :: SharedContext -> Maybe Integer -> Int -> FunAssumps ->
           MRM a -> IO (Either MRFailure a)
 runMRM sc timeout debug assumps m =
   do true_tm <- scBool sc True
-     let init_info = MRInfo { mrSC = sc, mrSMTTimeout = timeout,
-                              mrDebugLevel = debug, mrFunAssumps = assumps,
-                              mrUVars = [], mrCoIndHyps = Map.empty,
-                              mrAssumptions = true_tm }
-     let init_st = MRState { mrVars = Map.empty }
+     let init_info = MRInfo { mriSC = sc, mriSMTTimeout = timeout,
+                              mriDebugLevel = debug, mriFunAssumps = assumps,
+                              mriUVars = [], mriCoIndHyps = Map.empty,
+                              mriAssumptions = true_tm }
+     let init_st = MRState { mrsVars = Map.empty }
      runExceptT $ flip evalStateT init_st $ flip runReaderT init_info $ unMRM m
 
 -- | Apply a function to any failure thrown by an 'MRM' computation
@@ -298,29 +330,29 @@ catchErrorEither m = catchError (Right <$> m) (return . Left)
 
 -- | Lift a nullary SharedTerm computation into 'MRM'
 liftSC0 :: (SharedContext -> IO a) -> MRM a
-liftSC0 f = (mrSC <$> ask) >>= \sc -> liftIO (f sc)
+liftSC0 f = mrSC >>= \sc -> liftIO (f sc)
 
 -- | Lift a unary SharedTerm computation into 'MRM'
 liftSC1 :: (SharedContext -> a -> IO b) -> a -> MRM b
-liftSC1 f a = (mrSC <$> ask) >>= \sc -> liftIO (f sc a)
+liftSC1 f a = mrSC >>= \sc -> liftIO (f sc a)
 
 -- | Lift a binary SharedTerm computation into 'MRM'
 liftSC2 :: (SharedContext -> a -> b -> IO c) -> a -> b -> MRM c
-liftSC2 f a b = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b)
+liftSC2 f a b = mrSC >>= \sc -> liftIO (f sc a b)
 
 -- | Lift a ternary SharedTerm computation into 'MRM'
 liftSC3 :: (SharedContext -> a -> b -> c -> IO d) -> a -> b -> c -> MRM d
-liftSC3 f a b c = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c)
+liftSC3 f a b c = mrSC >>= \sc -> liftIO (f sc a b c)
 
 -- | Lift a quaternary SharedTerm computation into 'MRM'
 liftSC4 :: (SharedContext -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d ->
            MRM e
-liftSC4 f a b c d = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c d)
+liftSC4 f a b c d = mrSC >>= \sc -> liftIO (f sc a b c d)
 
 -- | Lift a quinary SharedTerm computation into 'MRM'
 liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) ->
            a -> b -> c -> d -> e -> MRM f
-liftSC5 f a b c d e = (mrSC <$> ask) >>= \sc -> liftIO (f sc a b c d e)
+liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e)
 
 
 ----------------------------------------------------------------------
@@ -362,7 +394,7 @@ mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize
 -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in
 -- the order as seen "from the outside"
 mrUVarCtx :: MRM [(LocalName,Term)]
-mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars <$> ask
+mrUVarCtx = reverse <$> map (\(nm,Type tp) -> (nm,tp)) <$> mrUVars
 
 -- | Get the type of a 'Term' in the current uvar context
 mrTypeOf :: Term -> MRM Term
@@ -403,11 +435,10 @@ uniquifyName nm nms =
 -- assumptions made in the sub-computation will be lost when it completes.
 withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a
 withUVar nm tp m =
-  do info <- ask
-     let nm' = uniquifyName nm (map fst $ mrUVars info)
-     assumps' <- liftTerm 0 1 $ mrAssumptions info
-     local (\_ -> info { mrUVars = (nm',tp) : mrUVars info,
-                         mrAssumptions = assumps' }) $
+  do nm' <- uniquifyName nm <$> map fst <$> mrUVars
+     assumps' <- mrAssumptions >>= liftTerm 0 1
+     local (\info -> info { mriUVars = (nm',tp) : mriUVars info,
+                            mriAssumptions = assumps' }) $
        mapFailure (MRFailureLocalVar nm') (liftSC1 scLocalVar 0 >>= m)
 
 -- | Run a MR Solver computation in a context extended with a universal variable
@@ -437,7 +468,7 @@ withUVars = helper [] where
 -- most recently bound
 getAllUVarTerms :: MRM [Term]
 getAllUVarTerms =
-  (length <$> mrUVars <$> ask) >>= \len ->
+  (length <$> mrUVars) >>= \len ->
   mapM (liftSC1 scLocalVar) [len-1, len-2 .. 0]
 
 -- | Lambda-abstract all the current uvars out of a 'Term', with the least
@@ -476,7 +507,7 @@ mrVarTerm (MRVar ec) =
 
 -- | Get the 'VarInfo' associated with a 'MRVar'
 mrVarInfo :: MRVar -> MRM (Maybe MRVarInfo)
-mrVarInfo var = Map.lookup var <$> mrVars <$> get
+mrVarInfo var = Map.lookup var <$> mrVars
 
 -- | Convert an 'ExtCns' to a 'FunName'
 extCnsToFunName :: ExtCns Term -> MRM FunName
@@ -543,11 +574,11 @@ mrFreshVar nm tp = MRVar <$> liftSC2 scFreshEC nm tp
 mrSetVarInfo :: MRVar -> MRVarInfo -> MRM ()
 mrSetVarInfo var info =
   modify $ \st ->
-  st { mrVars =
+  st { mrsVars =
          Map.alter (\case
                        Just _ -> error "mrSetVarInfo"
                        Nothing -> Just info)
-         var (mrVars st) }
+         var (mrsVars st) }
 
 -- | Make a fresh existential variable of the given type, abstracting out all
 -- the current uvars and returning the new evar applied to all current uvars
@@ -583,14 +614,14 @@ mrSetEVarClosed var val =
      -- FIXME: catch subtyping errors and report them as being evar failures
      liftSC3 scCheckSubtype Nothing (TypedTerm val val_tp) var_tp
      modify $ \st ->
-       st { mrVars =
+       st { mrsVars =
             Map.alter
             (\case
                 Just (EVarInfo Nothing) -> Just $ EVarInfo (Just val)
                 Just (EVarInfo (Just _)) ->
                   error "Setting existential variable: variable already set!"
                 _ -> error "Setting existential variable: not an evar!")
-            var (mrVars st) }
+            var (mrsVars st) }
 
 
 -- | Try to set the value of the application @X e1 .. en@ of evar @X@ to an
@@ -636,7 +667,7 @@ mrTrySetAppliedEVar evar args t =
 -- | Replace all evars in a 'Term' with their instantiations when they have one
 mrSubstEVars :: Term -> MRM Term
 mrSubstEVars = memoFixTermFun $ \recurse t ->
-  do var_map <- mrVars <$> get
+  do var_map <- mrVars
      case t of
        -- If t is an instantiated evar, recurse on its instantiation
        (asEVarApp var_map -> Just (_, args, Just t')) ->
@@ -649,7 +680,7 @@ mrSubstEVars = memoFixTermFun $ \recurse t ->
 mrSubstEVarsStrict :: Term -> MRM (Maybe Term)
 mrSubstEVarsStrict top_t =
   runMaybeT $ flip memoFixTermFun top_t $ \recurse t ->
-  do var_map <- mrVars <$> get
+  do var_map <- lift mrVars
      case t of
        -- If t is an instantiated evar, recurse on its instantiation
        (asEVarApp var_map -> Just (_, args, Just t')) ->
@@ -666,7 +697,7 @@ _mrSubstEVarsStrict = mrSubstEVarsStrict
 
 -- | Get the 'CoIndHyp' for a pair of 'FunName's, if there is one
 mrGetCoIndHyp :: FunName -> FunName -> MRM (Maybe CoIndHyp)
-mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps <$> ask
+mrGetCoIndHyp nm1 nm2 = Map.lookup (nm1, nm2) <$> mrCoIndHyps
 
 -- | Run a compuation under the additional co-inductive assumption that
 -- @forall x1, ..., xn. F y1 ... ym |= G z1 ... zl@, where @F@ and @G@ are
@@ -688,8 +719,8 @@ withCoIndHyp' (nm1, nm2) hyp@(CoIndHyp _ args1 args2) m =
   do mrDebugPPPrefixSep 1 "withCoIndHyp" (FunBind nm1 args1 CompFunReturn)
                                     "|=" (FunBind nm2 args2 CompFunReturn)
      st <- get
-     hyps' <- Map.insert (nm1, nm2) hyp <$> mrCoIndHyps <$> ask
-     (local (\info -> info { mrCoIndHyps = hyps' }) m) `catchError` \case
+     hyps' <- Map.insert (nm1, nm2) hyp <$> mrCoIndHyps
+     (local (\info -> info { mriCoIndHyps = hyps' }) m) `catchError` \case
        CoIndHypMismatchWidened nm1' nm2' hyp' | nm1 == nm1' && nm2 == nm2'
          -> -- FIXME: Could restoring the state here cause any problems?
             put st >> withCoIndHyp' (nm1, nm2) hyp' m
@@ -706,7 +737,7 @@ instantiateCoIndHyp (CoIndHyp {..}) =
 
 -- | Look up the 'FunAssump' for a 'FunName', if there is one
 mrGetFunAssump :: FunName -> MRM (Maybe FunAssump)
-mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps <$> ask
+mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps
 
 -- | Run a computation under the additional assumption that a named function
 -- applied to a list of arguments refines a given right-hand side, all of which
@@ -716,9 +747,9 @@ withFunAssump fname args rhs m =
   do mrDebugPPPrefixSep 1 "withFunAssump" (FunBind
                                            fname args CompFunReturn) "|=" rhs
      ctx <- mrUVarCtx
-     assumps <- mrFunAssumps <$> ask
+     assumps <- mrFunAssumps
      let assumps' = Map.insert fname (FunAssump ctx args rhs) assumps
-     local (\info -> info { mrFunAssumps = assumps' }) m
+     local (\info -> info { mriFunAssumps = assumps' }) m
 
 -- | Generate fresh evars for the context of a 'FunAssump' and substitute them
 -- into its arguments and right-hand side
@@ -733,14 +764,13 @@ instantiateFunAssump fassump =
 -- executing a sub-computation
 withAssumption :: Term -> MRM a -> MRM a
 withAssumption phi m =
-  do assumps <- mrAssumptions <$> ask
-     assumps' <- liftSC2 scAnd phi assumps
-     local (\info -> info { mrAssumptions = assumps' }) m
+  do assumps' <- mrAssumptions >>= liftSC2 scAnd phi
+     local (\info -> info { mriAssumptions = assumps' }) m
 
 -- | Print a 'String' if the debug level is at least the supplied 'Int'
 debugPrint :: Int -> String -> MRM ()
 debugPrint i str =
-  (mrDebugLevel <$> ask) >>= \lvl ->
+  mrDebugLevel >>= \lvl ->
   if lvl >= i then liftIO (hPutStrLn stderr str) else return ()
 
 -- | Print a document if the debug level is at least the supplied 'Int'
@@ -751,19 +781,19 @@ debugPretty i pp = debugPrint i $ renderSawDoc defaultPPOpts pp
 -- at least the supplied 'Int'
 debugPrettyInCtx :: PrettyInCtx a => Int -> a -> MRM ()
 debugPrettyInCtx i a =
-  (mrUVars <$> ask) >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
+  mrUVars >>= \ctx -> debugPrint i (showInCtx (map fst ctx) a)
 
 -- | Pretty-print an object relative to the current context
 mrPPInCtx :: PrettyInCtx a => a -> MRM SawDoc
 mrPPInCtx a =
-  runReader (prettyInCtx a) <$> map fst <$> mrUVars <$> ask
+  runReader (prettyInCtx a) <$> map fst <$> mrUVars
 
 -- | Pretty-print the result of 'ppWithPrefixSep' relative to the current uvar
 -- context to 'stderr' if the debug level is at least the 'Int' provided
 mrDebugPPPrefixSep :: PrettyInCtx a => Int -> String -> a -> String -> a ->
                       MRM ()
 mrDebugPPPrefixSep i pre a1 sp a2 =
-  (mrUVars <$> ask) >>= \ctx ->
+  mrUVars >>= \ctx ->
   debugPretty i $
   flip runReader (map fst ctx) (group <$> nest 2 <$>
                                 ppWithPrefixSep pre a1 sp a2)
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index 363309b620..608f4ae9bd 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -18,7 +18,6 @@ module SAWScript.Prover.MRSolver.SMT where
 
 import qualified Data.Vector as V
 import Control.Monad.Reader
-import Control.Monad.State
 import Control.Monad.Except
 
 import Data.Map (Map)
@@ -162,7 +161,7 @@ normSMTProp t =
 -- FIXME: use the timeout!
 mrProvableRaw :: Term -> MRM Bool
 mrProvableRaw prop_term =
-  do sc <- mrSC <$> ask
+  do sc <- mrSC
      prop <- liftSC1 termToProp prop_term
      unints <- Set.map ecVarIndex <$> getAllExtSet <$> liftSC1 propToTerm prop
      debugPrint 2 ("Calling SMT solver with proposition: " ++
@@ -180,7 +179,7 @@ mrProvableRaw prop_term =
 -- assumptions
 mrProvable :: Term -> MRM Bool
 mrProvable bool_tm =
-  do assumps <- mrAssumptions <$> ask
+  do assumps <- mrAssumptions
      prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue
      prop_inst <- flip instantiateUVarsM prop $ \nm tp ->
        liftSC1 scWhnf tp >>= \case
@@ -268,7 +267,7 @@ mrProveEq :: Term -> Term -> MRM Bool
 mrProveEq t1 t2 =
   do mrDebugPPPrefixSep 1 "mrProveEq" t1 "==" t2
      tp <- mrTypeOf t1
-     varmap <- mrVars <$> get
+     varmap <- mrVars
      cond_in_ctx <- mrProveEqH varmap tp t1 t2
      withTermInCtx cond_in_ctx mrProvable
 
@@ -348,7 +347,7 @@ mrProveEqH _ (asBVVecType -> Just (n, len, tp)) t1 t2 =
                                                         t1'', ix'', pf'']
      t2_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n'', len'', tp'',
                                                         t2'', ix'', pf'']
-     var_map <- mrVars <$> get
+     var_map <- mrVars
      extTermInCtx [("eq_ix",ix_tp),("eq_pf",pf_tp)] <$>
        mrProveEqH var_map tp'' t1_prj t2_prj
 

From e786da4479acfe6c1adbca1649a89c2d15f4a169 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 24 Feb 2022 11:13:41 -0800
Subject: [PATCH 6/7] minor cleanup and refactoring

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

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 2b6804f7e4..116965fa66 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -223,19 +223,19 @@ data MRInfo = MRInfo {
   mriSC :: SharedContext,
   -- | SMT timeout for SMT calls made by Mr. Solver
   mriSMTTimeout :: Maybe Integer,
-  -- | The debug level, which controls debug printing
-  mriDebugLevel :: Int,
-  -- | The set of function refinements to be assumed by to Mr. Solver
-  mriFunAssumps :: FunAssumps,
   -- | The current context of universal variables, which are free SAW core
   -- 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 current set of co-inductive hypotheses
   mriCoIndHyps :: CoIndHyps,
   -- | The current assumptions, which are conjoined into a single Boolean term;
   -- note that these have the current UVars free
-  mriAssumptions :: Term
+  mriAssumptions :: Term,
+  -- | The debug level, which controls debug printing
+  mriDebugLevel :: Int
 }
 
 -- | State maintained by MR. Solver
@@ -253,6 +253,12 @@ newtype MRM a = MRM { unMRM :: ReaderT MRInfo (StateT MRState
                         MonadReader MRInfo, MonadState MRState,
                                             MonadError MRFailure)
 
+instance MonadTerm MRM where
+  mkTermF = liftSC1 scTermF
+  liftTerm = liftSC3 incVars
+  whnfTerm = liftSC1 scWhnf
+  substTerm = liftSC3 instantiateVarList
+
 -- | Get the current value of 'mriSC'
 mrSC :: MRM SharedContext
 mrSC = mriSC <$> ask
@@ -261,18 +267,14 @@ mrSC = mriSC <$> ask
 mrSMTTimeout :: MRM (Maybe Integer)
 mrSMTTimeout = mriSMTTimeout <$> ask
 
--- | Get the current value of 'mrDebugLevel'
-mrDebugLevel :: MRM Int
-mrDebugLevel = mriDebugLevel <$> ask
+-- | Get the current value of 'mrUVars'
+mrUVars :: MRM [(LocalName,Type)]
+mrUVars = mriUVars <$> ask
 
 -- | Get the current value of 'mrFunAssumps'
 mrFunAssumps :: MRM FunAssumps
 mrFunAssumps = mriFunAssumps <$> ask
 
--- | Get the current value of 'mrUVars'
-mrUVars :: MRM [(LocalName,Type)]
-mrUVars = mriUVars <$> ask
-
 -- | Get the current value of 'mrCoIndHyps'
 mrCoIndHyps :: MRM CoIndHyps
 mrCoIndHyps = mriCoIndHyps <$> ask
@@ -281,16 +283,14 @@ mrCoIndHyps = mriCoIndHyps <$> ask
 mrAssumptions :: MRM Term
 mrAssumptions = mriAssumptions <$> ask
 
+-- | Get the current value of 'mrDebugLevel'
+mrDebugLevel :: MRM Int
+mrDebugLevel = mriDebugLevel <$> ask
+
 -- | Get the current value of 'mrVars'
 mrVars :: MRM MRVarMap
 mrVars = mrsVars <$> get
 
-instance MonadTerm MRM where
-  mkTermF = liftSC1 scTermF
-  liftTerm = liftSC3 incVars
-  whnfTerm = liftSC1 scWhnf
-  substTerm = liftSC3 instantiateVarList
-
 -- | Run an 'MRM' computation and return a result or an error
 runMRM :: SharedContext -> Maybe Integer -> Int -> FunAssumps ->
           MRM a -> IO (Either MRFailure a)
@@ -764,7 +764,8 @@ instantiateFunAssump fassump =
 -- executing a sub-computation
 withAssumption :: Term -> MRM a -> MRM a
 withAssumption phi m =
-  do assumps' <- mrAssumptions >>= liftSC2 scAnd phi
+  do assumps <- mrAssumptions
+     assumps' <- liftSC2 scAnd phi assumps
      local (\info -> info { mriAssumptions = assumps' }) m
 
 -- | Print a 'String' if the debug level is at least the supplied 'Int'

From 74dd8a4916bf8b7c4d6395e1ddfe70b5aea95d7d Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Thu, 24 Feb 2022 11:46:12 -0800
Subject: [PATCH 7/7] add partially implemented mrWidenCoIndHyp, some minor
 cleanup

---
 src/SAWScript/Prover/MRSolver/Monad.hs  |  8 ++---
 src/SAWScript/Prover/MRSolver/SMT.hs    |  1 -
 src/SAWScript/Prover/MRSolver/Solver.hs | 46 +++++++++++++++++++------
 3 files changed, 39 insertions(+), 16 deletions(-)

diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 116965fa66..fd4ce458c2 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -127,10 +127,10 @@ instance PrettyInCtx MRFailure where
   prettyInCtx (CoIndHypMismatchWidened nm1 nm2 _) =
     ppWithPrefixSep "[Internal] Trying to widen co-inductive hypothesis on:" nm1 "," nm2
   prettyInCtx (CoIndHypMismatchFailure (tm1, tm2) (tm1', tm2')) =
-    vsepM [return "Could not match co-inductive hypotheis:",
-           ppWithPrefixSep "" tm1' "|=" tm2',
-           return "with goal:",
-           ppWithPrefixSep "" tm1 "|=" tm2]
+    do pp <- ppWithPrefixSep "" tm1 "|=" tm2
+       pp' <- ppWithPrefixSep "" tm1' "|=" tm2'
+       return $ "Could not match co-inductive hypothesis:" <> pp' <> line <>
+                                              "with goal:" <> pp
   prettyInCtx (MRFailureLocalVar x err) =
     local (x:) $ prettyInCtx err
   prettyInCtx (MRFailureCtx ctx err) =
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index 608f4ae9bd..f597b35756 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -17,7 +17,6 @@ namely 'mrProvable' and 'mrProveEq'.
 module SAWScript.Prover.MRSolver.SMT where
 
 import qualified Data.Vector as V
-import Control.Monad.Reader
 import Control.Monad.Except
 
 import Data.Map (Map)
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index 66defa2ded..49452fe4d6 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -114,7 +114,6 @@ C |- F e1 ... en >>= k |= F' e1' ... em' >>= k':
 
 module SAWScript.Prover.MRSolver.Solver where
 
-import Control.Monad.Reader
 import Control.Monad.Except
 import qualified Data.Map as Map
 
@@ -458,16 +457,21 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) =
   mrGetFunAssump f1 >>= \maybe_fassump ->
   case (maybe_coIndHyp, maybe_fassump) of
 
-  -- If we have a co-inductive assumption that f1 args1' |= f2 args2', then
-  -- prove that args1 = args1' and args2 = args2', and then that k1 |= k2
-  (Just coIndHyp, _) ->
-    do (args1', args2') <- instantiateCoIndHyp coIndHyp
-       eq1 <- and <$> zipWithM mrProveEq args1' args1
-       eq2 <- and <$> zipWithM mrProveEq args2' args2
-       if eq1 && eq2 then mrRefinesFun k1 k2
-       else let m1' = FunBind f1 args1' CompFunReturn
-                m2' = FunBind f2 args2' CompFunReturn
-             in throwError (CoIndHypMismatchFailure (m1, m2) (m1', m2'))
+  -- If we have a co-inductive assumption that f1 args1' |= f2 args2':
+  -- * 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)
+  -- * Otherwise, throw a 'CoIndHypMismatchFailure' error.
+  (Just hyp, _) ->
+    do (args1', args2') <- instantiateCoIndHyp hyp
+       mrWidenCoIndHyp f1 f2 args1 args2 args1' args2' >>= \case
+         Convertible -> mrRefinesFun k1 k2
+         Widened hyp' -> throwError (CoIndHypMismatchWidened f1 f2 hyp')
+         CouldNotWiden ->
+           let m1' = FunBind f1 args1' CompFunReturn
+               m2' = FunBind f2 args2' CompFunReturn
+            in throwError (CoIndHypMismatchFailure (m1, m2) (m1', m2'))
 
   -- If we have an assumption that f1 args' refines some rhs, then prove that
   -- args1 = args' and then that rhs refines m2
@@ -600,6 +604,26 @@ mrRefinesFun f1 f2
 mrRefinesFun _ _ = error "mrRefinesFun: unreachable!"
 
 
+-- | The result type of 'mrWidenCoIndHyp'
+data WidenCoIndHypResult = Convertible | Widened CoIndHyp | CouldNotWiden
+
+-- | Given a goal and a co-inductive hypothesis over the same pair of function
+-- names, try to widen them into a more general co-inductive hypothesis which
+-- implies both the given goal and the given co-inductive hypothesis. Returns
+-- 'Convertible' if the goal and co-inductive hypothesis are convertible (and
+-- therefore no widening needs to be done), 'Widened' if widening was
+-- successful, and 'CouldNotWiden' if the terms are neither convertible nor
+-- able to be widened.
+-- FIXME: Finish implementing this function!
+mrWidenCoIndHyp :: FunName -> FunName ->
+                    [Term] -> [Term] -> [Term] -> [Term] ->
+                    MRM WidenCoIndHypResult
+mrWidenCoIndHyp _f1 _f2 args1 args2 args1' args2' =
+  do eq1 <- and <$> zipWithM mrProveEq args1' args1
+     eq2 <- and <$> zipWithM mrProveEq args2' args2
+     return $ if eq1 && eq2 then Convertible else CouldNotWiden
+
+
 ----------------------------------------------------------------------
 -- * External Entrypoints
 ----------------------------------------------------------------------