From a4a743cd57676d7a02e1fc4df0ab7594cfe9d08d Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Fri, 7 Oct 2022 13:08:04 -0700
Subject: [PATCH 1/9] Unfold bare Cryptol properties when interpreting them as
 rewrite rules

---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 14 +++++++++
 saw-core/src/Verifier/SAW/Rewriter.hs        | 22 ++++++++++++++
 src/SAWScript/Builtins.hs                    | 30 +++++++++++++-------
 src/SAWScript/Proof.hs                       | 13 ++++++---
 4 files changed, 65 insertions(+), 14 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 73d58e3a7d..e2abac61bc 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1213,6 +1213,20 @@ cryptolURI (p:ps) (Just uniq) =
        , uriFragment = Just frag
        }
 
+-- | Tests if the given 'NameInfo' represents a name imported
+--   from Cryptol. If so, return the unqualified identifier
+--   associated with that 'NameInfo'.
+isCryptolName :: NameInfo -> Maybe Text
+isCryptolName (ImportedName uri _)
+  | Just sch <- uriScheme uri
+  , unRText sch == "cryptol"
+  , Left True <- uriAuthority uri
+  , Just (False, x :| xs) <- uriPath uri
+  , [] <- uriQuery uri
+  , Nothing <- uriFragment uri
+  = Just (unRText (last (x:xs)))
+isCryptolName _ = Nothing
+
 -- | Tests if the given 'NameInfo' represents a name imported
 --   from the given Cryptol module name.  If so, it returns
 --   the identifier within that module.  Note, this does
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index e03f1872c9..732de859fa 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -30,6 +30,7 @@ module Verifier.SAW.Rewriter
   , ruleOfTerm
   , ruleOfTerms
   , ruleOfProp
+  , unfoldableTerm
   , scDefRewriteRules
   , scEqsRewriteRules
   , scEqRewriteRule
@@ -395,6 +396,27 @@ scEqRewriteRule sc i = ruleOfTerm <$> scTypeOfGlobal sc i <*> pure Nothing
 scEqsRewriteRules :: SharedContext -> [Ident] -> IO [RewriteRule a]
 scEqsRewriteRules sc = mapM (scEqRewriteRule sc)
 
+-- | Finds the first named constant in the term that may be amenable to
+-- unfolding
+unfoldableTerm :: Term -> Either NameInfo ()
+unfoldableTerm t
+  | Just _ <- R.asFTermF t =
+    Right ()
+  | Just _ <- R.asLocalVar t =
+    Right ()
+  | Just (EC _ nmi _, Just _body) <- R.asConstant t =
+    -- is matching (Just _body) too strict?
+    Left nmi
+  | Just (_, _, body) <- R.asLambda t =
+    unfoldableTerm body
+  | Just (_, _, body) <- R.asPi t =
+    unfoldableTerm body
+  | Just body <- R.asEqTrue t =
+    unfoldableTerm body
+  | Just (f, x) <- R.asApp t =
+    unfoldableTerm f >> unfoldableTerm x
+  | otherwise = Right ()
+
 -- | Transform the given rewrite rule to a set of one or more
 -- equivalent rewrite rules, if possible.
 --
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 1496bc07f4..b3e8a71b26 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1523,19 +1523,29 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
+addSimpWith :: (forall a. RewriteRule a -> RewriteRule a) -> Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
+addSimpWith f thm ss =
+  do  sc <- getSharedContext
+      mkRule sc (thmProp thm)
+  where
+    mkRule sc prop =
+      io (propToRewriteRule sc prop (Just (thmNonce thm))) >>= \case
+        Right Nothing -> fail "addsimp: cannot interpret theorem as equation"
+        Right (Just rule) -> pure (addRule (f rule) ss)
+        Left nmi ->
+          case Cryptol.isCryptolName nmi of
+            Nothing -> fail "addsimp: cannot unfold a non-cryptol term"
+            Just name ->
+              do  idx <- resolveName sc (Text.unpack name)
+                  prop' <- io $ unfoldProp sc (Set.fromList idx) prop
+                  prop'' <- io $ betaReduceProp sc prop'
+                  mkRule sc prop''
+
 addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp thm ss =
-  do sc <- getSharedContext
-     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
-       Nothing -> fail "addsimp: theorem not an equation"
-       Just rule -> pure (addRule rule ss)
+addsimp = addSimpWith id
 
 addsimp_shallow :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp_shallow thm ss =
-  do sc <- getSharedContext
-     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
-       Nothing -> fail "addsimp: theorem not an equation"
-       Just rule -> pure (addRule (shallowRule rule) ss)
+addsimp_shallow = addSimpWith shallowRule
 
 -- TODO: remove this, it implicitly adds axioms
 addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 30a488911e..0cc929e6c6 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -224,12 +224,16 @@ boolToProp sc vars tm =
 propToTerm :: SharedContext -> Prop -> IO Term
 propToTerm _sc (Prop tm) = pure tm
 
--- | Attempt to interpret a proposition as a rewrite rule.
-propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a))
+-- | Attempt to interpret a proposition as a rewrite rule. If interpretation
+-- fails, check if a (sub)term can be unfolded.
+propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Either NameInfo (Maybe (RewriteRule a)))
 propToRewriteRule _sc (Prop tm) ann =
   case ruleOfProp tm ann of
-    Nothing -> pure Nothing
-    Just r  -> pure (Just r)
+    Just r  -> pure (Right (Just r))
+    Nothing ->
+      case unfoldableTerm tm of
+        Left nmi -> pure (Left nmi)
+        Right () -> pure (Right Nothing)
 
 -- | Attempt to split an if/then/else proposition.
 --   If it succeeds to find a term like "EqTrue (ite Bool b x y)",
@@ -397,6 +401,7 @@ localHypSimpset sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps
     processHyp ss (n,h) =
       case ruleOfProp (unProp h) Nothing of
         Nothing -> fail $ "Hypothesis " ++ show n ++ "cannot be used as a rewrite rule."
+        -- check `unfoldableTerm`?
         Just r  -> return (addRule r ss)
 
     nhyps = [ (n,h)

From c8dd3c83a7df1bd6f0dc7681bd47193c616efa17 Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Fri, 7 Oct 2022 17:53:18 -0700
Subject: [PATCH 2/9] Add a test

---
 intTests/test_property_as_rewrite_rule/README.md | 4 ++++
 intTests/test_property_as_rewrite_rule/test.cry  | 4 ++++
 intTests/test_property_as_rewrite_rule/test.saw  | 4 ++++
 intTests/test_property_as_rewrite_rule/test.sh   | 3 +++
 4 files changed, 15 insertions(+)
 create mode 100644 intTests/test_property_as_rewrite_rule/README.md
 create mode 100644 intTests/test_property_as_rewrite_rule/test.cry
 create mode 100644 intTests/test_property_as_rewrite_rule/test.saw
 create mode 100755 intTests/test_property_as_rewrite_rule/test.sh

diff --git a/intTests/test_property_as_rewrite_rule/README.md b/intTests/test_property_as_rewrite_rule/README.md
new file mode 100644
index 0000000000..79f77b73f4
--- /dev/null
+++ b/intTests/test_property_as_rewrite_rule/README.md
@@ -0,0 +1,4 @@
+This tests limited automatic unfolding in `addsimp*`. Rather than unwrap
+`XorInvolutes` into its functional definition at the `prove*` site, we can prove
+the property by name and include its *immediate* definition as the rewrite rule.
+No further unwrapping takes place.
\ No newline at end of file
diff --git a/intTests/test_property_as_rewrite_rule/test.cry b/intTests/test_property_as_rewrite_rule/test.cry
new file mode 100644
index 0000000000..df15846140
--- /dev/null
+++ b/intTests/test_property_as_rewrite_rule/test.cry
@@ -0,0 +1,4 @@
+module Test where
+
+XorInvolutes : [8] -> [8] -> Bit
+property XorInvolutes x y = (x ^ y) ^ y == x
diff --git a/intTests/test_property_as_rewrite_rule/test.saw b/intTests/test_property_as_rewrite_rule/test.saw
new file mode 100644
index 0000000000..9f127762e4
--- /dev/null
+++ b/intTests/test_property_as_rewrite_rule/test.saw
@@ -0,0 +1,4 @@
+import "test.cry";
+
+p <- prove_print z3 {{ XorInvolutes }};
+let rules = addsimp p empty_ss;
\ No newline at end of file
diff --git a/intTests/test_property_as_rewrite_rule/test.sh b/intTests/test_property_as_rewrite_rule/test.sh
new file mode 100755
index 0000000000..ac0feae188
--- /dev/null
+++ b/intTests/test_property_as_rewrite_rule/test.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+$SAW test.saw
\ No newline at end of file

From 82fe90444988db3b92dab2cc90017b191377b6a4 Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Mon, 10 Oct 2022 14:04:08 -0700
Subject: [PATCH 3/9] Revert "Unfold bare Cryptol properties when interpreting
 them as rewrite rules"

This reverts commit a4a743cd57676d7a02e1fc4df0ab7594cfe9d08d.
---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 14 ---------
 saw-core/src/Verifier/SAW/Rewriter.hs        | 22 --------------
 src/SAWScript/Builtins.hs                    | 30 +++++++-------------
 src/SAWScript/Proof.hs                       | 13 +++------
 4 files changed, 14 insertions(+), 65 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index e2abac61bc..73d58e3a7d 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1213,20 +1213,6 @@ cryptolURI (p:ps) (Just uniq) =
        , uriFragment = Just frag
        }
 
--- | Tests if the given 'NameInfo' represents a name imported
---   from Cryptol. If so, return the unqualified identifier
---   associated with that 'NameInfo'.
-isCryptolName :: NameInfo -> Maybe Text
-isCryptolName (ImportedName uri _)
-  | Just sch <- uriScheme uri
-  , unRText sch == "cryptol"
-  , Left True <- uriAuthority uri
-  , Just (False, x :| xs) <- uriPath uri
-  , [] <- uriQuery uri
-  , Nothing <- uriFragment uri
-  = Just (unRText (last (x:xs)))
-isCryptolName _ = Nothing
-
 -- | Tests if the given 'NameInfo' represents a name imported
 --   from the given Cryptol module name.  If so, it returns
 --   the identifier within that module.  Note, this does
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 732de859fa..e03f1872c9 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -30,7 +30,6 @@ module Verifier.SAW.Rewriter
   , ruleOfTerm
   , ruleOfTerms
   , ruleOfProp
-  , unfoldableTerm
   , scDefRewriteRules
   , scEqsRewriteRules
   , scEqRewriteRule
@@ -396,27 +395,6 @@ scEqRewriteRule sc i = ruleOfTerm <$> scTypeOfGlobal sc i <*> pure Nothing
 scEqsRewriteRules :: SharedContext -> [Ident] -> IO [RewriteRule a]
 scEqsRewriteRules sc = mapM (scEqRewriteRule sc)
 
--- | Finds the first named constant in the term that may be amenable to
--- unfolding
-unfoldableTerm :: Term -> Either NameInfo ()
-unfoldableTerm t
-  | Just _ <- R.asFTermF t =
-    Right ()
-  | Just _ <- R.asLocalVar t =
-    Right ()
-  | Just (EC _ nmi _, Just _body) <- R.asConstant t =
-    -- is matching (Just _body) too strict?
-    Left nmi
-  | Just (_, _, body) <- R.asLambda t =
-    unfoldableTerm body
-  | Just (_, _, body) <- R.asPi t =
-    unfoldableTerm body
-  | Just body <- R.asEqTrue t =
-    unfoldableTerm body
-  | Just (f, x) <- R.asApp t =
-    unfoldableTerm f >> unfoldableTerm x
-  | otherwise = Right ()
-
 -- | Transform the given rewrite rule to a set of one or more
 -- equivalent rewrite rules, if possible.
 --
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index b3e8a71b26..1496bc07f4 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1523,29 +1523,19 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
-addSimpWith :: (forall a. RewriteRule a -> RewriteRule a) -> Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addSimpWith f thm ss =
-  do  sc <- getSharedContext
-      mkRule sc (thmProp thm)
-  where
-    mkRule sc prop =
-      io (propToRewriteRule sc prop (Just (thmNonce thm))) >>= \case
-        Right Nothing -> fail "addsimp: cannot interpret theorem as equation"
-        Right (Just rule) -> pure (addRule (f rule) ss)
-        Left nmi ->
-          case Cryptol.isCryptolName nmi of
-            Nothing -> fail "addsimp: cannot unfold a non-cryptol term"
-            Just name ->
-              do  idx <- resolveName sc (Text.unpack name)
-                  prop' <- io $ unfoldProp sc (Set.fromList idx) prop
-                  prop'' <- io $ betaReduceProp sc prop'
-                  mkRule sc prop''
-
 addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp = addSimpWith id
+addsimp thm ss =
+  do sc <- getSharedContext
+     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
+       Nothing -> fail "addsimp: theorem not an equation"
+       Just rule -> pure (addRule rule ss)
 
 addsimp_shallow :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp_shallow = addSimpWith shallowRule
+addsimp_shallow thm ss =
+  do sc <- getSharedContext
+     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
+       Nothing -> fail "addsimp: theorem not an equation"
+       Just rule -> pure (addRule (shallowRule rule) ss)
 
 -- TODO: remove this, it implicitly adds axioms
 addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 0cc929e6c6..30a488911e 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -224,16 +224,12 @@ boolToProp sc vars tm =
 propToTerm :: SharedContext -> Prop -> IO Term
 propToTerm _sc (Prop tm) = pure tm
 
--- | Attempt to interpret a proposition as a rewrite rule. If interpretation
--- fails, check if a (sub)term can be unfolded.
-propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Either NameInfo (Maybe (RewriteRule a)))
+-- | Attempt to interpret a proposition as a rewrite rule.
+propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a))
 propToRewriteRule _sc (Prop tm) ann =
   case ruleOfProp tm ann of
-    Just r  -> pure (Right (Just r))
-    Nothing ->
-      case unfoldableTerm tm of
-        Left nmi -> pure (Left nmi)
-        Right () -> pure (Right Nothing)
+    Nothing -> pure Nothing
+    Just r  -> pure (Just r)
 
 -- | Attempt to split an if/then/else proposition.
 --   If it succeeds to find a term like "EqTrue (ite Bool b x y)",
@@ -401,7 +397,6 @@ localHypSimpset sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps
     processHyp ss (n,h) =
       case ruleOfProp (unProp h) Nothing of
         Nothing -> fail $ "Hypothesis " ++ show n ++ "cannot be used as a rewrite rule."
-        -- check `unfoldableTerm`?
         Just r  -> return (addRule r ss)
 
     nhyps = [ (n,h)

From a18d411972e45d27dbe0bc0fc5367f07e8d1885f Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Fri, 14 Oct 2022 16:01:54 -0700
Subject: [PATCH 4/9] Unfold constants when adding simplification rules

Better than the earlier approach, this leverages the fact that every unfoldable
constant is constructed with a `Just body` and restricts unfolding to happen
within `ruleAsProp`. Also, pipe a `SharedContext` to `ruleAsProp` to allow
leveraging `scApplyAllBeta` to beta-reduce the unfolded term before checking
rule well-formedness again.
---
 saw-core/src/Verifier/SAW/Rewriter.hs | 59 ++++++++++++++-------------
 src/SAWScript/Builtins.hs             |  9 ++--
 src/SAWScript/Proof.hs                | 13 +++---
 3 files changed, 41 insertions(+), 40 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index e03f1872c9..b12373d92f 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -358,34 +358,37 @@ ruleOfTerms l r = mkRewriteRule [] l r False Nothing
 
 -- | Converts a parameterized equality predicate to a RewriteRule,
 -- returning 'Nothing' if the predicate is not an equation.
-ruleOfProp :: Term -> Maybe a -> Maybe (RewriteRule a)
-ruleOfProp (R.asPi -> Just (_, ty, body)) ann =
-  do rule <- ruleOfProp body ann
-     Just rule { ctxt = ty : ctxt rule }
-ruleOfProp (R.asLambda -> Just (_, ty, body)) ann =
-  do rule <- ruleOfProp body ann
-     Just rule { ctxt = ty : ctxt rule }
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (unwrapTermF -> Constant _ (Just body)) ann = ruleOfProp body ann
-ruleOfProp (R.asEq -> Just (_, x, y)) ann =
-  Just $ mkRewriteRule [] x y False ann
-ruleOfProp (R.asEqTrue -> Just body) ann = ruleOfProp body ann
-ruleOfProp _ _ = Nothing
+ruleOfProp :: SharedContext -> Term -> Maybe a -> IO (Maybe (RewriteRule a))
+ruleOfProp sc (R.asPi -> Just (_, ty, body)) ann =
+  do rule <- ruleOfProp sc body ann
+     pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+ruleOfProp sc (R.asLambda -> Just (_, ty, body)) ann =
+  do rule <- ruleOfProp sc body ann
+     pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp sc (unwrapTermF -> Constant _ (Just body)) ann = ruleOfProp sc body ann
+ruleOfProp _sc (R.asEq -> Just (_, x, y)) ann =
+  pure $ Just $ mkRewriteRule [] x y False ann
+ruleOfProp sc (R.asEqTrue -> Just body) ann = ruleOfProp sc body ann
+ruleOfProp sc (R.asApplyAll -> (R.asConstant -> Just (_, Just body), as)) ann =
+  do  app <- scApplyAllBeta sc body as
+      ruleOfProp sc app ann
+ruleOfProp _ _ _ = pure Nothing
 
 -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm'
 scEqRewriteRule :: SharedContext -> Ident -> IO (RewriteRule a)
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 1496bc07f4..6bd35e14e9 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -660,7 +660,7 @@ simplifyGoalWithLocals :: [Integer] -> SV.SAWSimpset -> ProofScript ()
 simplifyGoalWithLocals hs ss =
   execTactic $ tacticChange $ \goal ->
   do sc <- getSharedContext
-     ss' <- io (localHypSimpset (goalSequent goal) hs ss)
+     ss' <- io (localHypSimpset sc (goalSequent goal) hs ss)
      sqt' <- traverseSequentWithFocus
                (\p -> snd <$> io (simplifyProp sc ss' p)) (goalSequent goal)
      return (sqt', RewriteEvidence hs ss)
@@ -1540,9 +1540,10 @@ addsimp_shallow thm ss =
 -- TODO: remove this, it implicitly adds axioms
 addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimp' t ss =
-  case ruleOfProp t Nothing of
-    Nothing -> fail "addsimp': theorem not an equation"
-    Just rule -> pure (addRule rule ss)
+  do  sc <- getSharedContext
+      io (ruleOfProp sc t Nothing) >>= \case
+        Nothing -> fail "addsimp': theorem not an equation"
+        Just rule -> pure (addRule rule ss)
 
 addsimps :: [Theorem] -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimps thms ss = foldM (flip addsimp) ss thms
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 30a488911e..906fcb29e5 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -226,10 +226,7 @@ propToTerm _sc (Prop tm) = pure tm
 
 -- | Attempt to interpret a proposition as a rewrite rule.
 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)
+propToRewriteRule sc (Prop tm) = ruleOfProp sc tm
 
 -- | Attempt to split an if/then/else proposition.
 --   If it succeeds to find a term like "EqTrue (ite Bool b x y)",
@@ -390,12 +387,12 @@ simplifyProps sc ss (p:ps) =
 
 -- | Add hypotheses from the given sequent as rewrite rules
 --   to the given simpset.
-localHypSimpset :: Sequent -> [Integer] -> Simpset a -> IO (Simpset a)
-localHypSimpset sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps
+localHypSimpset :: SharedContext -> Sequent -> [Integer] -> Simpset a -> IO (Simpset a)
+localHypSimpset sc sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps
 
   where
     processHyp ss (n,h) =
-      case ruleOfProp (unProp h) Nothing of
+      ruleOfProp sc (unProp h) Nothing >>= \case
         Nothing -> fail $ "Hypothesis " ++ show n ++ "cannot be used as a rewrite rule."
         Just r  -> return (addRule r ss)
 
@@ -1632,7 +1629,7 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc
            check nenv e' sqt'
 
       RewriteEvidence hs ss e' ->
-        do ss' <- localHypSimpset sqt hs ss
+        do ss' <- localHypSimpset sc sqt hs ss
            (d1,sqt') <- simplifySequent sc ss' sqt
            (d2,sy) <- check nenv e' sqt'
            return (Set.union d1 d2, sy)

From 5b6e1796113b1f2dae3ea583d3c0166da2288822 Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Fri, 14 Oct 2022 16:08:47 -0700
Subject: [PATCH 5/9] Clarify test README

---
 intTests/test_property_as_rewrite_rule/README.md | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/intTests/test_property_as_rewrite_rule/README.md b/intTests/test_property_as_rewrite_rule/README.md
index 79f77b73f4..552184876a 100644
--- a/intTests/test_property_as_rewrite_rule/README.md
+++ b/intTests/test_property_as_rewrite_rule/README.md
@@ -1,4 +1,5 @@
-This tests limited automatic unfolding in `addsimp*`. Rather than unwrap
-`XorInvolutes` into its functional definition at the `prove*` site, we can prove
-the property by name and include its *immediate* definition as the rewrite rule.
-No further unwrapping takes place.
\ No newline at end of file
+This tests limited automatic unfolding in `addsimp*`. Rather than manually
+unwrap `XorInvolutes` into its functional definition at the `prove*` site in
+SAW, we can prove the property by name and include its *immediate* definition as
+the rewrite rule. No further unwrapping takes place, since `XorInvolutes`
+unfolds to a well-formed simplification rule.

From 5b4a65ac4a3c902d42cf35ca3873f5af6987d07f Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Mon, 17 Oct 2022 09:14:31 -0700
Subject: [PATCH 6/9] Change pattern-matching style in `ruleOfProp`

Also, previous commits' references to `ruleAsProp` should have been to
`ruleOfProp`.
---
 saw-core/src/Verifier/SAW/Rewriter.hs | 61 ++++++++++++++-------------
 1 file changed, 31 insertions(+), 30 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index b12373d92f..aac3070045 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -359,36 +359,37 @@ ruleOfTerms l r = mkRewriteRule [] l r False Nothing
 -- | Converts a parameterized equality predicate to a RewriteRule,
 -- returning 'Nothing' if the predicate is not an equation.
 ruleOfProp :: SharedContext -> Term -> Maybe a -> IO (Maybe (RewriteRule a))
-ruleOfProp sc (R.asPi -> Just (_, ty, body)) ann =
-  do rule <- ruleOfProp sc body ann
-     pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
-ruleOfProp sc (R.asLambda -> Just (_, ty, body)) ann =
-  do rule <- ruleOfProp sc body ann
-     pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp _sc (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp sc (unwrapTermF -> Constant _ (Just body)) ann = ruleOfProp sc body ann
-ruleOfProp _sc (R.asEq -> Just (_, x, y)) ann =
-  pure $ Just $ mkRewriteRule [] x y False ann
-ruleOfProp sc (R.asEqTrue -> Just body) ann = ruleOfProp sc body ann
-ruleOfProp sc (R.asApplyAll -> (R.asConstant -> Just (_, Just body), as)) ann =
-  do  app <- scApplyAllBeta sc body as
-      ruleOfProp sc app ann
-ruleOfProp _ _ _ = pure Nothing
+ruleOfProp sc term ann
+  | Just (_, ty, body) <- R.asPi term =
+    do  rule <- ruleOfProp sc body ann
+        pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+  | Just (_, ty, body) <- R.asLambda term =
+    do  rule <- ruleOfProp sc body ann
+        pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+  | (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef bvEqIdent -> Just (), [_, x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef equalNatIdent -> Just (), [x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef boolEqIdent -> Just (), [x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef intEqIdent -> Just (), [x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.isGlobalDef intModEqIdent -> Just (), [_, x, y]) <- R.asApplyAll term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | (R.asConstant -> Just (_, Just body), as) <- R.asApplyAll term =
+    do  app <- scApplyAllBeta sc body as
+        ruleOfProp sc app ann
+  | Constant _ (Just body) <- unwrapTermF term = ruleOfProp sc body ann
+  | Just (_, x, y) <- R.asEq term =
+    pure $ Just $ mkRewriteRule [] x y False ann
+  | Just body <- R.asEqTrue term = ruleOfProp sc body ann
+  | otherwise = pure Nothing
 
 -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm'
 scEqRewriteRule :: SharedContext -> Ident -> IO (RewriteRule a)

From be87b2006426b62bf7e441329fd902a23e217586 Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Mon, 17 Oct 2022 10:11:13 -0700
Subject: [PATCH 7/9] Comment on testing

---
 intTests/test_property_as_rewrite_rule/test.saw | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/intTests/test_property_as_rewrite_rule/test.saw b/intTests/test_property_as_rewrite_rule/test.saw
index 9f127762e4..eba8c62d9e 100644
--- a/intTests/test_property_as_rewrite_rule/test.saw
+++ b/intTests/test_property_as_rewrite_rule/test.saw
@@ -1,4 +1,13 @@
 import "test.cry";
 
-p <- prove_print z3 {{ XorInvolutes }};
-let rules = addsimp p empty_ss;
\ No newline at end of file
+// Existing capability
+p1 <- prove_print z3 {{ \(x: [8]) (y: [8]) -> (x ^ y) ^ y == x }};
+let r1 = addsimp p1 empty_ss;
+
+// New capability
+p2 <- prove_print z3 {{ XorInvolutes }};
+let r2 = addsimp p2 empty_ss;
+
+// New capability
+p3 <- prove_print z3 {{ \x y -> XorInvolutes x y }};
+let r3 = addsimp p3 empty_ss;
\ No newline at end of file

From 743cce7fb63d836f53c00a777299b0539c4f8a11 Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Mon, 17 Oct 2022 15:02:33 -0700
Subject: [PATCH 8/9] Demote constant-application matching to come after
 preexisting rules

---
 saw-core/src/Verifier/SAW/Rewriter.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index aac3070045..83786f3206 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -382,13 +382,13 @@ ruleOfProp sc term ann
     pure $ Just $ mkRewriteRule [] x y False ann
   | (R.isGlobalDef intModEqIdent -> Just (), [_, x, y]) <- R.asApplyAll term =
     pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.asConstant -> Just (_, Just body), as) <- R.asApplyAll term =
-    do  app <- scApplyAllBeta sc body as
-        ruleOfProp sc app ann
   | Constant _ (Just body) <- unwrapTermF term = ruleOfProp sc body ann
   | Just (_, x, y) <- R.asEq term =
     pure $ Just $ mkRewriteRule [] x y False ann
   | Just body <- R.asEqTrue term = ruleOfProp sc body ann
+  | (R.asConstant -> Just (_, Just body), as) <- R.asApplyAll term =
+    do  app <- scApplyAllBeta sc body as
+        ruleOfProp sc app ann
   | otherwise = pure Nothing
 
 -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm'

From 1c6f64ae67e5307b8fe395f0e50c833a19fe804a Mon Sep 17 00:00:00 2001
From: Sam Cowger <sam@galois.com>
Date: Tue, 18 Oct 2022 09:43:35 -0700
Subject: [PATCH 9/9] Use left-to-right rule recognition style without
 top-level pattern-matching

---
 saw-core/src/Verifier/SAW/Rewriter.hs | 57 ++++++++++++---------------
 1 file changed, 26 insertions(+), 31 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 83786f3206..b9596827df 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -359,37 +359,32 @@ ruleOfTerms l r = mkRewriteRule [] l r False Nothing
 -- | Converts a parameterized equality predicate to a RewriteRule,
 -- returning 'Nothing' if the predicate is not an equation.
 ruleOfProp :: SharedContext -> Term -> Maybe a -> IO (Maybe (RewriteRule a))
-ruleOfProp sc term ann
-  | Just (_, ty, body) <- R.asPi term =
-    do  rule <- ruleOfProp sc body ann
-        pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
-  | Just (_, ty, body) <- R.asLambda term =
-    do  rule <- ruleOfProp sc body ann
-        pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
-  | (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef bvEqIdent -> Just (), [_, x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef equalNatIdent -> Just (), [x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef boolEqIdent -> Just (), [x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef intEqIdent -> Just (), [x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | (R.isGlobalDef intModEqIdent -> Just (), [_, x, y]) <- R.asApplyAll term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | Constant _ (Just body) <- unwrapTermF term = ruleOfProp sc body ann
-  | Just (_, x, y) <- R.asEq term =
-    pure $ Just $ mkRewriteRule [] x y False ann
-  | Just body <- R.asEqTrue term = ruleOfProp sc body ann
-  | (R.asConstant -> Just (_, Just body), as) <- R.asApplyAll term =
-    do  app <- scApplyAllBeta sc body as
-        ruleOfProp sc app ann
-  | otherwise = pure Nothing
+ruleOfProp sc term ann =
+  case term of
+    (R.asPi -> Just (_, ty, body)) ->
+      do  rule <- ruleOfProp sc body ann
+          pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+    (R.asLambda -> Just (_, ty, body)) ->
+      do  rule <- ruleOfProp sc body ann
+          pure $ (\r -> r { ctxt = ty : ctxt r }) <$> rule
+    (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) -> eqRule x y
+    (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) -> eqRule x y
+    (unwrapTermF -> Constant _ (Just body)) -> ruleOfProp sc body ann
+    (R.asEq -> Just (_, x, y)) -> eqRule x y
+    (R.asEqTrue -> Just body) -> ruleOfProp sc body ann
+    (R.asApplyAll -> (R.asConstant -> Just (_, Just body), args)) ->
+      do  app <- scApplyAllBeta sc body args
+          ruleOfProp sc app ann
+    _ -> pure Nothing
+
+  where
+    eqRule x y = pure $ Just $ mkRewriteRule [] x y False ann
 
 -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm'
 scEqRewriteRule :: SharedContext -> Ident -> IO (RewriteRule a)