Merge pull request #1297 from GaloisInc/ruleOfProp-intEq

Recognize rewrite rules using `intEq` and `intModEq` relations.

intTests/test_rewrite_int/test.saw

@@ -0,0 +1,39 @@
+// This test ensures that rewrite rules using `intEq` and `intModEq` will work.
+
+let ss0 = add_cryptol_defs ["ecEq"] (cryptol_ss ());
+
+let {{
+  squareInt : Integer -> Integer
+  squareInt x = x * x
+
+  squareZ5 : Z 5 -> Z 5
+  squareZ5 x = x * x
+}};
+
+let prove_rule t =
+  do {
+    thm <- prove_print z3 (rewrite ss0 t);
+    print thm;
+    return thm;
+  };
+
+squareInt_plus <-
+  prove_rule {{ \x y -> squareInt (x + y) == squareInt x + squareInt y + 2 * x * y }};
+
+squareInt_times <-
+  prove_rule {{ \x y -> squareInt (x * y) == squareInt x * squareInt y }};
+
+squareZ5_plus <-
+  prove_rule {{ \x y -> squareZ5 (x + y) == squareZ5 x + squareZ5 y + 2 * x * y }};
+
+squareZ5_times <-
+  prove_rule {{ \x y -> squareZ5 (x * y) == squareZ5 x * squareZ5 y }};
+
+let ss1 = addsimps [squareInt_plus, squareInt_times, squareZ5_plus, squareZ5_times] ss0;
+let tac = do { simplify ss1; print_goal; w4_unint_z3 ["squareInt", "squareZ5"]; };
+
+prove_print tac
+  {{ \x y z -> squareInt (x * y + z) == squareInt x * squareInt y + squareInt z + 2 * x * y * z }};
+
+prove_print tac
+  {{ \x y z -> squareZ5 (x * y + z) == squareZ5 x * squareZ5 y + squareZ5 z + 2 * x * y * z }};

intTests/test_rewrite_int/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

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

@@ -293,6 +293,12 @@ vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq"
 equalNatIdent :: Ident
 equalNatIdent = mkIdent (mkModuleName ["Prelude"]) "equalNat"
 
+intEqIdent :: Ident
+intEqIdent = mkIdent (mkModuleName ["Prelude"]) "intEq"
+
+intModEqIdent :: Ident
+intModEqIdent = mkIdent (mkModuleName ["Prelude"]) "intModEq"
+
 -- | Converts a universally quantified equality proposition from a
 -- Term representation to a RewriteRule.
 ruleOfTerm :: Term -> Maybe a -> RewriteRule a
@@ -345,6 +351,10 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
   Just $ mkRewriteRule [] x y ann
+ruleOfProp (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
+  Just $ mkRewriteRule [] x y ann
+ruleOfProp (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
+  Just $ mkRewriteRule [] x y ann
 ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann
 ruleOfProp (R.asEq -> Just (_, x, y)) ann =
   Just $ mkRewriteRule [] x y ann