Add mrsolver tactic, remove old MRSolver interface (#1907)

* add refines SAW command to build refinesS terms

* have refines command use fresh_symbolic variables

* add MREvidence, keep track of Theorems and SolverStats,  overhaul MRSolver commands

* revert unnecessary DataTypeAssump bits of 33694b2

* fix infinite loop in `mrCallsFun` on recursive sub-functions

* use solver caching (i.e. use applyProverToGoal) in MRSolver

* fix typo in docs of mrsolver_with

* remove extraneous .saw from heapster-saw Makefile

* incorporate comments from @bboston7 and @eddywestbrook

* add RefinesS type for asRefinesS, fix haddock

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -49,7 +49,7 @@ data TypedTermType
  deriving Show
 
 
--- | Convert the 'ttTerm' field of a 'TypedTerm' to a SAW core term
+-- | Convert the 'ttType' field of a 'TypedTerm' to a SAW core term
 ttTypeAsTerm :: SharedContext -> Env -> TypedTerm -> IO Term
 ttTypeAsTerm sc env (TypedTerm (TypedTermSchema schema) _) =
   importSchema sc env schema

examples/mr_solver/mr_solver_unit_tests.saw

@@ -26,44 +26,55 @@ let const1_core = "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool)
 const1 <- parse_core const1_core;
 
 // const0 <= const0
-run_test "const0 |= const0" (mr_solver_query const0 const0) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] const0 const0);
+// (testing that "refines [] const0 const0" is actually "const0 <= const0")
 let const0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const0_core, ") x) ", "((", const0_core, ") x)"];
-prove_extcore mrsolver (parse_core const0_refines);
-
-// The function test_fun0 = const0
+run_test "refines [] const0 const0" (is_convertible (parse_core const0_refines)
+                                                    (refines [] const0 const0)) true;
+// (testing that "refines [x] ..." gives the same expression as "refines [] ...")
+x <- fresh_symbolic "x" {| [64] |};
+run_test "refines [x] (const0 x) (const0 x)"
+         (is_convertible (refines [] const0 const0)
+                         (refines [x] (term_apply const0 [x])
+                                      (term_apply const0 [x]))) true;
+
+// The function test_fun0 <= const0
 test_fun0 <- parse_core_mod "test_funs" "test_fun0";
-run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] const0 test_fun0);
+// (testing that "refines [] const0 test_fun0" is actually "const0 <= test_fun0")
 let const0_test_fun0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const0_core, ") x) ", "(test_fun0 x)"];
-prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun0_refines);
+run_test "refines [] const0 test_fun0" (is_convertible (parse_core_mod "test_funs" const0_test_fun0_refines)
+                                                       (refines [] const0 test_fun0)) true;
 
 // not const0 <= const1
-run_test "const0 |= const1" (mr_solver_query const0 const1) false;
-// (using mrsolver tactic - fails as expected)
-// let const0_const1_refines =
-//   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
-//                "((", const0_core, ") x) ", "((", const1_core, ") x)"];
-// prove_extcore mrsolver (parse_core const0_const1_refines);
+fails (prove_extcore mrsolver (refines [] const0 const1));
+// (testing that "refines [] const0 const1" is actually "const0 <= const1")
+let const0_const1_refines =
+  str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
+               "((", const0_core, ") x) ", "((", const1_core, ") x)"];
+run_test "refines [] const0 const1" (is_convertible (parse_core const0_const1_refines)
+                                                    (refines [] const0 const1)) true;
 
 // The function test_fun1 = const1
 test_fun1 <- parse_core_mod "test_funs" "test_fun1";
-run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true;
-run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] const1 test_fun1);
+fails (prove_extcore mrsolver (refines [] const0 test_fun1));
+// (testing that "refines [] const1 test_fun1" is actually "const1 <= test_fun1")
 let const1_test_fun1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const1_core, ") x) ", "(test_fun1 x)"];
-prove_extcore mrsolver (parse_core_mod "test_funs" const1_test_fun1_refines);
-// (using mrsolver tactic - fails as expected)
-// let const0_test_fun1_refines =
-//   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
-//                "((", const0_core, ") x) ", "(test_fun1 x)"];
-// prove_extcore mrsolver (parse_core_mod "test_funs" const0_test_fun1_refines);
+run_test "refines [] const1 test_fun1" (is_convertible (parse_core_mod "test_funs" const1_test_fun1_refines)
+                                                       (refines [] const1 test_fun1)) true;
+// (testing that "refines [] const0 test_fun1" is actually "const0 <= test_fun1")
+let const0_test_fun1_refines =
+  str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
+               "((", const0_core, ") x) ", "(test_fun1 x)"];
+run_test "refines [] const0 test_fun1" (is_convertible (parse_core_mod "test_funs" const0_test_fun1_refines)
+                                                       (refines [] const0 test_fun1)) true;
 
 // ifxEq0 x = If x == 0 then x else 0; should be equal to 0
 let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
@@ -74,41 +85,46 @@ let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
 ifxEq0 <- parse_core ifxEq0_core;
 
 // ifxEq0 <= const0
-run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] ifxEq0 const0);
+// (testing that "refines [] ifxEq0 const0" is actually "ifxEq0 <= const0")
 let ifxEq0_const0_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", ifxEq0_core, ") x) ", "((", const0_core, ") x)"];
-prove_extcore mrsolver (parse_core ifxEq0_const0_refines);
+run_test "refines [] ifxEq0 const0" (is_convertible (parse_core ifxEq0_const0_refines)
+                                                    (refines [] ifxEq0 const0)) true;
+
 
 // not ifxEq0 <= const1
-run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
-// (using mrsolver tactic - fails as expected)
-// let ifxEq0_const1_refines =
-//   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
-//                "((", ifxEq0_core, ") x) ", "((", const1_core, ") x)"];
-// prove_extcore mrsolver (parse_core ifxEq0_const1_refines);
+fails (prove_extcore mrsolver (refines [] ifxEq0 const1));
+// (testing that "refines [] ifxEq0 const1" is actually "ifxEq0 <= const1")
+let ifxEq0_const1_refines =
+  str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
+               "((", ifxEq0_core, ") x) ", "((", const1_core, ") x)"];
+run_test "refines [] ifxEq0 const1" (is_convertible (parse_core ifxEq0_const1_refines)
+                                                    (refines [] ifxEq0 const1)) true;
 
 // noErrors1 x = existsS x. retS x
 let noErrors1_core =
   "\\ (_:Vec 64 Bool) -> existsS VoidEv emptyFunStack (Vec 64 Bool)";
 noErrors1 <- parse_core noErrors1_core;
 
 // const0 <= noErrors
-run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] noErrors1 noErrors1);
+// (testing that "refines [] noErrors1 noErrors1" is actually "noErrors1 <= noErrors1")
 let noErrors1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", noErrors1_core, ") x) ", "((", noErrors1_core, ") x)"];
-prove_extcore mrsolver (parse_core noErrors1_refines);
+run_test "refines [] noErrors1 noErrors1" (is_convertible (parse_core noErrors1_refines)
+                                                          (refines [] noErrors1 noErrors1)) true;
 
 // const1 <= noErrors
-run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] const1 noErrors1);
+// (testing that "refines [] const1 noErrors1" is actually "const1 <= noErrors1")
 let const1_noErrors1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", const1_core, ") x) ", "((", noErrors1_core, ") x)"];
-prove_extcore mrsolver (parse_core const1_noErrors1_refines);
+run_test "refines [] const1 noErrors1" (is_convertible (parse_core const1_noErrors1_refines)
+                                                       (refines [] const1 noErrors1)) true;
 
 // noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x)
 // Intuitively, this specifies functions that either return a value or loop
@@ -135,9 +151,10 @@ let loop1_core =
 loop1 <- parse_core loop1_core;
 
 // loop1 <= noErrorsRec1
-run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;
-// (using mrsolver tactic)
+prove_extcore mrsolver (refines [] loop1 noErrorsRec1);
+// (testing that "refines [] loop1 noErrorsRec1" is actually "loop1 <= noErrorsRec1")
 let loop1_noErrorsRec1_refines =
   str_concats ["(x:Vec 64 Bool) -> refinesS_eq VoidEv emptyFunStack (Vec 64 Bool) ",
                "((", loop1_core, ") x) ", "((", noErrorsRec1_core, ") x)"];
-prove_extcore mrsolver (parse_core loop1_noErrorsRec1_refines);
+run_test "refines [] loop1 noErrorsRec1" (is_convertible (parse_core loop1_noErrorsRec1_refines)
+                                                         (refines [] loop1 noErrorsRec1)) true;

heapster-saw/examples/Makefile

@@ -41,7 +41,7 @@ endif
 	$(SAW) $<
 
 # Lists all the Mr Solver tests, without their ".saw" suffix
-MR_SOLVER_TESTS = # arrays_mr_solver linked_list_mr_solver sha512_mr_solver
+MR_SOLVER_TESTS = exp_explosion_mr_solver # arrays_mr_solver linked_list_mr_solver sha512_mr_solver
 
 .PHONY: mr-solver-tests $(MR_SOLVER_TESTS)
 mr-solver-tests: $(MR_SOLVER_TESTS)

heapster-saw/examples/arrays_mr_solver.saw

@@ -2,14 +2,15 @@ include "arrays.saw";
 
 // Test that contains0 |= contains0
 contains0 <- parse_core_mod "arrays" "contains0";
-mr_solver_test contains0 contains0;
+prove_extcore mrsolver (refines [] contains0 contains0);
 
 noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
-mr_solver_prove contains0 noErrorsContains0;
+prove_extcore mrsolver (refines [] contains0 noErrorsContains0);
+
 
 include "specPrims.saw";
 import "arrays.cry";
 
 zero_array <- parse_core_mod "arrays" "zero_array";
-mr_solver_test zero_array {{ zero_array_loop_spec }};
-mr_solver_prove zero_array {{ zero_array_spec }};
+prove_extcore mrsolver (refines [] zero_array {{ zero_array_loop_spec }});
+prove_extcore mrsolver (refines [] zero_array {{ zero_array_spec }});

heapster-saw/examples/exp_explosion_mr_solver.saw

@@ -1,7 +1,6 @@
 include "exp_explosion.saw";
 
 import "exp_explosion.cry";
-monadify_term {{ op }};
 
 exp_explosion <- parse_core_mod "exp_explosion" "exp_explosion";
-mr_solver_prove exp_explosion {{ exp_explosion_spec }};
+prove_extcore mrsolver (refines [] exp_explosion {{ exp_explosion_spec }});

heapster-saw/examples/linked_list_mr_solver.saw

@@ -27,11 +27,10 @@ heapster_typecheck_fun env "is_head"
      \ arg0:true, arg1:true, ret:int64<>";
 
 is_head <- parse_core_mod "linked_list" "is_head";
-mr_solver_test is_head is_head;
+prove_extcore mrsolver (refines [] is_head is_head);
 
 is_elem <- parse_core_mod "linked_list" "is_elem";
-
-mr_solver_test is_elem is_elem;
+prove_extcore mrsolver (refines [] is_elem is_elem);
 
 is_elem_noErrorsSpec <- parse_core
   "\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \
@@ -52,9 +51,9 @@ is_elem_noErrorsSpec <- parse_core
     \                                    Vec 64 Bool)) \
     \                       (Vec 64 Bool)) \
     \              (f x)) (x, y)";
-mr_solver_test is_elem is_elem_noErrorsSpec;
+prove_extcore mrsolver (refines [] is_elem is_elem_noErrorsSpec);
 
-mr_solver_prove is_elem {{ is_elem_spec }};
+prove_extcore mrsolver (refines [] is_elem {{ is_elem_spec }});
 
 
 monadify_term {{ Right }};
@@ -63,4 +62,4 @@ monadify_term {{ nil }};
 monadify_term {{ cons }};
 
 sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc";
-mr_solver_prove sorted_insert_no_malloc {{ sorted_insert_spec }};
+prove_extcore mrsolver (refines [] sorted_insert_no_malloc {{ sorted_insert_spec }});

heapster-saw/examples/sha512_mr_solver.saw

@@ -6,14 +6,28 @@ processBlock <- parse_core_mod "SHA512" "processBlock";
 processBlocks <- parse_core_mod "SHA512" "processBlocks";
 
 // Test that every function refines itself
-// mr_solver_test processBlocks processBlocks;
-// mr_solver_test processBlock processBlock;
-// mr_solver_test round_16_80 round_16_80;
-// mr_solver_test round_00_15 round_00_15;
+// prove_extcore mrsolver (refines [] processBlocks processBlocks);
+// prove_extcore mrsolver (refines [] processBlock processBlock);
+// prove_extcore mrsolver (refines [] round_16_80 round_16_80);
+// prove_extcore mrsolver (refines [] round_00_15 round_00_15);
 
 import "sha512.cry";
 
-mr_solver_prove round_00_15 {{ round_00_15_spec }};
-mr_solver_prove round_16_80 {{ round_16_80_spec }};
-mr_solver_prove processBlock {{ processBlock_spec }};
-// mr_solver_prove processBlocks {{ processBlocks_spec }};
+thm_round_00_15 <-
+  prove_extcore mrsolver (refines [] round_00_15 {{ round_00_15_spec }});
+
+thm_round_16_80 <-
+  prove_extcore
+    (mrsolver_with (addrefns [thm_round_00_15] empty_rs))
+    (refines [] round_16_80 {{ round_16_80_spec }});
+
+thm_processBlock <-
+  prove_extcore
+    (mrsolver_with (addrefns [thm_round_00_15, thm_round_16_80] empty_rs))
+    (refines [] processBlock {{ processBlock_spec }});
+
+// thm_processBlocks <-
+//   prove_extcore
+//     (mrsolver_with (addrefns [thm_processBlock] empty_rs))
+//     (refines [] processBlocks {{ processBlocks_spec }});
+

saw-script.cabal

@@ -182,6 +182,7 @@ library
     SAWScript.Prover.MRSolver.Monad
     SAWScript.Prover.MRSolver.SMT
     SAWScript.Prover.MRSolver.Solver
+    SAWScript.Prover.MRSolver.Evidence
     SAWScript.Prover.MRSolver.Term
     SAWScript.Prover.RME
     SAWScript.Prover.ABC