Merge pull request #1755 from GaloisInc/feature/cryptol-property-unfo…

…lding

Allow use of Cryptol property names as simplification rules

intTests/test_property_as_rewrite_rule/README.md

@@ -0,0 +1,5 @@
+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.

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

intTests/test_property_as_rewrite_rule/test.saw

@@ -0,0 +1,13 @@
+import "test.cry";
+
+// 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;

intTests/test_property_as_rewrite_rule/test.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+$SAW test.saw

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -358,34 +358,33 @@ 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 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)

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

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)