From 6d81c4475cf8fc0369b714144d06b85f9db2da5d Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Wed, 29 Mar 2023 11:47:19 -0400
Subject: [PATCH] move test_funs out of Prelude, add doc to MrSolverEvidence,
 some reverts

---
 .../mr_solver/mr_solver_test_funs.sawcore     | 67 +++++++++++++++++
 examples/mr_solver/mr_solver_unit_tests.saw   | 16 +++--
 saw-core/prelude/Prelude.sawcore              | 72 ++-----------------
 src/SAWScript/Proof.hs                        |  4 +-
 src/SAWScript/Prover/MRSolver/Monad.hs        | 10 +--
 5 files changed, 85 insertions(+), 84 deletions(-)
 create mode 100644 examples/mr_solver/mr_solver_test_funs.sawcore

diff --git a/examples/mr_solver/mr_solver_test_funs.sawcore b/examples/mr_solver/mr_solver_test_funs.sawcore
new file mode 100644
index 0000000000..ddce1f02bc
--- /dev/null
+++ b/examples/mr_solver/mr_solver_test_funs.sawcore
@@ -0,0 +1,67 @@
+module test_funs where
+
+import Prelude;
+
+test_fun0 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
+test_fun0 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0);
+
+test_fun1 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
+test_fun1 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1);
+
+test_fun2 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
+test_fun2 x = retS VoidEv emptyFunStack (Vec 64 Bool) x;
+
+-- If x == 0 then x else 0; should be equal to 0
+test_fun3 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
+test_fun3 x =
+  ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
+      (retS VoidEv emptyFunStack (Vec 64 Bool) x)
+      (retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0));
+
+{-
+-- let rec f x = 0 in f x
+test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
+test_fun4 x =
+  letRecM1
+    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
+    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (y:Vec 64 Bool) ->
+      returnM (Vec 64 Bool) (bvNat 64 0))
+    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) ->
+      f x);
+
+-- Alternate version of test_fun4 that uses letRecM directly
+test_fun4_alt : Vec 64 Bool -> CompM (Vec 64 Bool);
+test_fun4_alt x =
+  letRecM
+    (LRT_Cons (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool))
+     LRT_Nil)
+    (Vec 64 Bool)
+    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
+      ((\ (y:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)), ()))
+    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) -> f x);
+
+-- let rec f = f in f x
+test_fun5 : Vec 64 Bool -> CompM (Vec 64 Bool);
+test_fun5 x =
+  letRecM1
+    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
+    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f)
+    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f x);
+
+-- let rec f = g and g = f in f x
+test_fun6 : Vec 64 Bool -> CompM (Vec 64 Bool);
+test_fun6 x =
+  letRecM
+    (LRT_Cons
+      (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
+      (LRT_Cons
+        (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
+        LRT_Nil))
+    (Vec 64 Bool)
+    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
+       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
+      (f2, (f1, ())))
+    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
+       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
+      f1 x);
+-}
\ No newline at end of file
diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw
index d124f94e20..b30a187b23 100644
--- a/examples/mr_solver/mr_solver_unit_tests.saw
+++ b/examples/mr_solver/mr_solver_unit_tests.saw
@@ -1,5 +1,7 @@
 enable_experimental;
 
+load_sawcore_from_file "mr_solver_test_funs.sawcore";
+
 let eq_bool b1 b2 =
   if b1 then
     if b2 then true else false
@@ -31,14 +33,14 @@ let const0_refines =
                "((", const0_core, ") x) ", "((", const0_core, ") x)"];
 prove_extcore prove_refinement (parse_core const0_refines);
 
-// The function test_fun0 from the prelude = const0
-test_fun0 <- parse_core "test_fun0";
+// 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 prove_refinement tactic)
 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 prove_refinement (parse_core const0_test_fun0_refines);
+prove_extcore prove_refinement (parse_core_mod "test_funs" const0_test_fun0_refines);
 
 // not const0 <= const1
 run_test "const0 |= const1" (mr_solver_query const0 const1) false;
@@ -48,20 +50,20 @@ run_test "const0 |= const1" (mr_solver_query const0 const1) false;
 //                "((", const0_core, ") x) ", "((", const1_core, ") x)"];
 // prove_extcore prove_refinement (parse_core const0_const1_refines);
 
-// The function test_fun1 from the prelude = const1
-test_fun1 <- parse_core "test_fun1";
+// 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 prove_refinement tactic)
 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 prove_refinement (parse_core const1_test_fun1_refines);
+prove_extcore prove_refinement (parse_core_mod "test_funs" const1_test_fun1_refines);
 // (using prove_refinement 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 prove_refinement (parse_core const0_test_fun1_refines);
+// prove_extcore prove_refinement (parse_core_mod "test_funs" const0_test_fun1_refines);
 
 // ifxEq0 x = If x == 0 then x else 0; should be equal to 0
 let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 4682844cdf..45c9e49b96 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -172,6 +172,10 @@ eq_inv_map a b a1 a2 eq_a f1 f2 eq_f =
            (eq_cong a a2 a1 (sym a a1 a2 eq_a) b f2));
 
 
+data EqDep (t : sort 1) (P : t -> sort 0) (x : t) (p : P x) : (y : t) -> P y -> Prop where {
+    ReflDep : EqDep t P x p x p;
+  }
+
 -- Basic axiom about the behavior of "fix"
 axiom fix_unfold :
   (a : sort 1) ->
@@ -3307,74 +3311,6 @@ appendCastBVVecS E stack n len1 len2 len3 a v1 v2 =
     (bvEqWithProof n (bvAdd n len1 len2) len3);
 
 
---------------------------------------------------------------------------------
--- Monadic test functions
-
-test_fun0 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
-test_fun0 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0);
-
-test_fun1 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
-test_fun1 _ = retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1);
-
-test_fun2 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
-test_fun2 x = retS VoidEv emptyFunStack (Vec 64 Bool) x;
-
--- If x == 0 then x else 0; should be equal to 0
-test_fun3 : Vec 64 Bool -> SpecM VoidEv emptyFunStack (Vec 64 Bool);
-test_fun3 x =
-  ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
-      (retS VoidEv emptyFunStack (Vec 64 Bool) x)
-      (retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0));
-
-{-
--- let rec f x = 0 in f x
-test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
-test_fun4 x =
-  letRecM1
-    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
-    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (y:Vec 64 Bool) ->
-      returnM (Vec 64 Bool) (bvNat 64 0))
-    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) ->
-      f x);
-
--- Alternate version of test_fun4 that uses letRecM directly
-test_fun4_alt : Vec 64 Bool -> CompM (Vec 64 Bool);
-test_fun4_alt x =
-  letRecM
-    (LRT_Cons (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool))
-     LRT_Nil)
-    (Vec 64 Bool)
-    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
-      ((\ (y:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)), ()))
-    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) -> f x);
-
--- let rec f = f in f x
-test_fun5 : Vec 64 Bool -> CompM (Vec 64 Bool);
-test_fun5 x =
-  letRecM1
-    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
-    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f)
-    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f x);
-
--- let rec f = g and g = f in f x
-test_fun6 : Vec 64 Bool -> CompM (Vec 64 Bool);
-test_fun6 x =
-  letRecM
-    (LRT_Cons
-      (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
-      (LRT_Cons
-        (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
-        LRT_Nil))
-    (Vec 64 Bool)
-    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
-       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
-      (f2, (f1, ())))
-    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
-       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
-      f1 x);
--}
-
-
 --------------------------------------------------------------------------------
 -- SMT Array
 
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index c5d50b3bcb..edccec690d 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -1076,7 +1076,9 @@ data Evidence
     --   sequent calculus axiom, which connects a hypothesis to a conclusion.
   | AxiomEvidence
 
-  -- | TODO: Add some evidence
+    -- | FIXME: This is a placeholder for evidence that will be generated by
+    --   MRSolver - currently this trivial evidence is given whenever MRSolver
+    --   completes without error (see 'proveRefinement' in @Builtins.hs@)
   | MrSolverEvidence
 
 -- | The the proposition proved by a given theorem.
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 518b821f99..7ead557815 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -639,14 +639,8 @@ withUVar nm tp m = withUVars (singletonMRVarCtx nm tp) (\[v] -> m v)
 -- and pass it the lifting (in the sense of 'incVars') of an MR Solver term
 withUVarLift :: TermLike tm => LocalName -> Type -> tm ->
                 (Term -> tm -> MRM a) -> MRM a
-withUVarLift nm tp t m = withUVarsLift (singletonMRVarCtx nm tp) t (\[v] -> m v)
-
--- | Run a MR Solver computation in a context extended with a list of universal
--- variables, passing 'Term's for those variables to the supplied computation
--- and passing it the lifting (in the sense of 'incVars') of an MR Solver term
-withUVarsLift :: TermLike tm => MRVarCtx -> tm -> ([Term] -> tm -> MRM a) -> MRM a
-withUVarsLift ctx t m =
-  withUVars ctx (\vars -> liftTermLike 0 (mrVarCtxLength ctx) t >>= m vars)
+withUVarLift nm tp t m =
+  withUVar nm tp (\x -> liftTermLike 0 1 t >>= m x)
 
 -- | Run a MR Solver computation in a context extended with a list of universal
 -- variables, passing 'Term's for those variables to the supplied computation.