From f992bda50785b3a738f7acdfc318ea46adfedf8b Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 26 Apr 2021 12:58:07 -0700
Subject: [PATCH] Update uses of saw-core API WRT simpset annotations.

Currently, we use trivial `()` annotations and ignore annotations
collected by rewrite steps. The plan is to allocate unique nonces
for each theorem and use those to track theorem dependencies.
---
 deps/saw-core                                 |  2 +-
 src/SAWScript/Builtins.hs                     | 38 +++++++++----------
 src/SAWScript/Crucible/LLVM/MethodSpecIR.hs   |  2 +-
 .../Crucible/LLVM/ResolveSetupValue.hs        |  2 +-
 src/SAWScript/Interpreter.hs                  |  2 +-
 src/SAWScript/Proof.hs                        | 16 ++++----
 src/SAWScript/Prover/Rewrite.hs               |  4 +-
 src/SAWScript/Value.hs                        | 16 ++++----
 8 files changed, 41 insertions(+), 41 deletions(-)

diff --git a/deps/saw-core b/deps/saw-core
index e4c59543fc..92a96c32f7 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit e4c59543fc7520d6cfa3d44b0602a3274685b35d
+Subproject commit 92a96c32f7dec1bbee7a214cb1c4791b48e17136
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index baa9504c88..4f4d1ade43 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -286,8 +286,8 @@ replacePrim pat replace t = do
     unless c $ fail $ unlines
       [ "terms do not have convertible types", show tpat, show ty1, show trepl, show ty2 ]
 
-  let ss = emptySimpset
-  t' <- io $ replaceTerm sc ss (tpat, trepl) (ttTerm t)
+  let ss = emptySimpset :: SV.SAWSimpset
+  (_,t') <- io $ replaceTerm sc ss (tpat, trepl) (ttTerm t)
 
   io $ do
     ty  <- scTypeOf sc (ttTerm t)
@@ -494,11 +494,11 @@ unfoldGoal unints =
      prop' <- io (unfoldProp sc unints' (goalProp goal))
      return (prop', UnfoldEvidence unints')
 
-simplifyGoal :: Simpset -> ProofScript ()
+simplifyGoal :: SV.SAWSimpset -> ProofScript ()
 simplifyGoal ss =
   execTactic $ tacticChange $ \goal ->
   do sc <- getSharedContext
-     prop' <- io (simplifyProp sc ss (goalProp goal))
+     (_,prop') <- io (simplifyProp sc ss (goalProp goal))
      return (prop', RewriteEvidence ss)
 
 goal_eval :: [String] -> ProofScript ()
@@ -882,28 +882,26 @@ quickCheckPrintPrim opts sc numTests tt =
                "----------Counterexample----------\n" ++
                showList cex' ""
 
-cryptolSimpset :: TopLevel Simpset
+cryptolSimpset :: TopLevel SV.SAWSimpset
 cryptolSimpset =
   do sc <- getSharedContext
      io $ Cryptol.mkCryptolSimpset sc
 
-addPreludeEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addPreludeEqs :: [String] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addPreludeEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Prelude"])
 
-addCryptolEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addCryptolEqs :: [String] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addCryptolEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Cryptol"])
 
-add_core_defs :: String -> [String] -> Simpset -> TopLevel Simpset
+add_core_defs :: String -> [String] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 add_core_defs modname names ss =
   do sc <- getSharedContext
      defs <- io $ mapM (getDef sc) names -- FIXME: warn if not found
@@ -917,16 +915,16 @@ add_core_defs modname names ss =
         Just d -> return d
         Nothing -> fail $ modname ++ " definition " ++ n ++ " not found"
 
-add_prelude_defs :: [String] -> Simpset -> TopLevel Simpset
+add_prelude_defs :: [String] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 add_prelude_defs = add_core_defs "Prelude"
 
-add_cryptol_defs :: [String] -> Simpset -> TopLevel Simpset
+add_cryptol_defs :: [String] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 add_cryptol_defs = add_core_defs "Cryptol"
 
-rewritePrim :: Simpset -> TypedTerm -> TopLevel TypedTerm
+rewritePrim :: SV.SAWSimpset -> TypedTerm -> TopLevel TypedTerm
 rewritePrim ss (TypedTerm schema t) = do
   sc <- getSharedContext
-  t' <- io $ rewriteSharedTerm sc ss t
+  (_,t') <- io $ rewriteSharedTerm sc ss t
   return (TypedTerm schema t')
 
 unfold_term :: [String] -> TypedTerm -> TopLevel TypedTerm
@@ -942,23 +940,23 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
-addsimp :: Theorem -> Simpset -> TopLevel Simpset
+addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimp thm ss =
   do sc <- getSharedContext
-     io (propToRewriteRule sc (thmProp thm)) >>= \case
+     io (propToRewriteRule sc (thmProp thm) (Just ())) >>= \case
        Nothing -> fail "addsimp: theorem not an equation"
        Just rule -> pure (addRule rule ss)
 
-addsimp' :: Term -> Simpset -> TopLevel Simpset
+addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimp' t ss =
-  case ruleOfProp t of
+  case ruleOfProp t Nothing of -- TODO!! track this as an axiom?
     Nothing -> fail "addsimp': theorem not an equation"
     Just rule -> pure (addRule rule ss)
 
-addsimps :: [Theorem] -> Simpset -> TopLevel Simpset
+addsimps :: [Theorem] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimps thms ss = foldM (flip addsimp) ss thms
 
-addsimps' :: [Term] -> Simpset -> TopLevel Simpset
+addsimps' :: [Term] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimps' ts ss = foldM (flip addsimp') ss ts
 
 print_type :: Term -> TopLevel ()
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
index 93ded0c184..10b297d46e 100644
--- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
@@ -321,7 +321,7 @@ data LLVMCrucibleContext arch =
   , _ccBackend         :: Sym
   , _ccLLVMSimContext  :: Crucible.SimContext (SAWCruciblePersonality Sym) Sym CL.LLVM
   , _ccLLVMGlobals     :: Crucible.SymGlobalState Sym
-  , _ccBasicSS         :: Simpset
+  , _ccBasicSS         :: Simpset ()
   }
 
 makeLenses ''LLVMCrucibleContext
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 5154b621cc..945670eda4 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -372,7 +372,7 @@ resolveSAWPred cc tm = do
      st <- sawCoreState sym
      let sc = saw_ctx st
      let ss = cc^.ccBasicSS
-     tm' <- rewriteSharedTerm sc ss tm
+     (_,tm') <- rewriteSharedTerm sc ss tm
      mx <- case getAllExts tm' of
              -- concretely evaluate if it is a closed term
              [] -> do modmap <- scGetModuleMap sc
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 88ff31e39c..76a4736eca 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1557,7 +1557,7 @@ primitives = Map.fromList
     ,  "goals 'prop1' and 'prop2'." ]
 
   , prim "empty_ss"            "Simpset"
-    (pureVal emptySimpset)
+    (pureVal (emptySimpset :: SAWSimpset))
     Current
     [ "The empty simplification rule set, containing no rules." ]
 
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index ce8721dd8e..a35d7476a6 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -146,9 +146,9 @@ propToTerm :: SharedContext -> Prop -> IO Term
 propToTerm _sc (Prop tm) = pure tm
 
 -- | Attempt to interpret a proposition as a rewrite rule.
-propToRewriteRule :: SharedContext -> Prop -> IO (Maybe (RewriteRule))
-propToRewriteRule _sc (Prop tm) =
-  case ruleOfProp tm of
+propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a))
+propToRewriteRule _sc (Prop tm) ann =
+  case ruleOfProp tm ann of
     Nothing -> pure Nothing
     Just r  -> pure (Just r)
 
@@ -173,10 +173,10 @@ unfoldProp sc unints (Prop tm) =
      return (Prop tm')
 
 -- | Rewrite the proposition using the provided Simpset
-simplifyProp :: SharedContext -> Simpset -> Prop -> IO Prop
+simplifyProp :: Ord a => SharedContext -> Simpset a -> Prop -> IO (Set a, Prop)
 simplifyProp sc ss (Prop tm) =
-  do tm' <- rewriteSharedTerm sc ss tm
-     return (Prop tm')
+  do (a, tm') <- rewriteSharedTerm sc ss tm
+     return (a, Prop tm')
 
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will
@@ -332,7 +332,7 @@ data Evidence
     -- | This type of evidence is used to modify a goal to prove via rewriting.
     --   The goal to prove is rewritten by the given simpset; then the provided
     --   evidence is used to check the modified goal.
-  | RewriteEvidence Simpset Evidence
+  | RewriteEvidence (Simpset ()) Evidence
 
     -- | This type of evidence is used to modify a goal to prove via unfolding
     --   constant definitions.  The goal to prove is modified by unfolding
@@ -608,7 +608,7 @@ checkEvidence sc = check mempty
            check hyps e' p'
 
       RewriteEvidence ss e' ->
-        do p' <- simplifyProp sc ss p
+        do (_,p') <- simplifyProp sc ss p -- TODO, remember the annotations!
            check hyps e' p'
 
       EvalEvidence vars e' ->
diff --git a/src/SAWScript/Prover/Rewrite.hs b/src/SAWScript/Prover/Rewrite.hs
index 0b50a7dd25..7afed1ff81 100644
--- a/src/SAWScript/Prover/Rewrite.hs
+++ b/src/SAWScript/Prover/Rewrite.hs
@@ -16,7 +16,7 @@ import Verifier.SAW.Term.Functor(preludeName, mkIdent, Ident, mkModuleName)
 import Verifier.SAW.Conversion
 import Verifier.SAW.SharedTerm(SharedContext,scFindDef)
 
-basic_ss :: SharedContext -> IO Simpset
+basic_ss :: SharedContext -> IO (Simpset a)
 basic_ss sc =
   do rs1 <- concat <$> traverse (defRewrites sc) defs
      rs2 <- scEqsRewriteRules sc eqs
@@ -67,7 +67,7 @@ basic_ss sc =
 
 
 
-defRewrites :: SharedContext -> Ident -> IO [RewriteRule]
+defRewrites :: SharedContext -> Ident -> IO [RewriteRule a]
 defRewrites sc ident =
   scFindDef sc ident >>= \maybe_def ->
   case maybe_def of
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 9151217077..dbebc393bb 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -126,7 +126,7 @@ data Value
     -- operations in these monads can fail at runtime.
   | VTopLevel (TopLevel Value)
   | VProofScript (ProofScript Value)
-  | VSimpset Simpset
+  | VSimpset SAWSimpset
   | VTheorem Theorem
   -----
   | VLLVMCrucibleSetup !(LLVMCrucibleSetupM Value)
@@ -154,6 +154,8 @@ data Value
   | VCFG SAW_CFG
   | VGhostVar CMS.GhostGlobal
 
+type SAWSimpset = Simpset ()
+
 data AIGNetwork where
   AIGNetwork :: (Typeable l, Typeable g, AIG.IsAIG l g) => AIG.Network l g -> AIGNetwork
 
@@ -165,7 +167,7 @@ data SAW_CFG where
   JVM_CFG :: Crucible.AnyCFG JVM -> SAW_CFG
 
 data BuiltinContext = BuiltinContext { biSharedContext :: SharedContext
-                                     , biBasicSS       :: Simpset
+                                     , biBasicSS       :: SAWSimpset
                                      }
   deriving Generic
 
@@ -245,7 +247,7 @@ showsSatResult opts r =
     showMulti _ [] = showString "]"
     showMulti s (eqn : eqns) = showString s . showEqn eqn . showMulti ", " eqns
 
-showSimpset :: PPOpts -> Simpset -> String
+showSimpset :: PPOpts -> Simpset a -> String
 showSimpset opts ss =
   unlines ("Rewrite Rules" : "=============" : map (show . ppRule) (listRules ss))
   where
@@ -382,7 +384,7 @@ data TopLevelRO =
   , roPosition      :: SS.Pos
   , roProxy         :: AIGProxy
   , roInitWorkDir   :: FilePath
-  , roBasicSS       :: Simpset
+  , roBasicSS       :: SAWSimpset
   }
 
 data TopLevelRW =
@@ -459,7 +461,7 @@ getOptions = TopLevel (asks roOptions)
 getProxy :: TopLevel AIGProxy
 getProxy = TopLevel (asks roProxy)
 
-getBasicSS :: TopLevel Simpset
+getBasicSS :: TopLevel SAWSimpset
 getBasicSS = TopLevel (asks roBasicSS)
 
 localOptions :: (Options -> Options) -> TopLevel a -> TopLevel a
@@ -870,10 +872,10 @@ instance FromValue Bool where
     fromValue (VBool b) = b
     fromValue _ = error "fromValue Bool"
 
-instance IsValue Simpset where
+instance IsValue SAWSimpset where
     toValue ss = VSimpset ss
 
-instance FromValue Simpset where
+instance FromValue SAWSimpset where
     fromValue (VSimpset ss) = ss
     fromValue _ = error "fromValue Simpset"