Merge pull request #1806 from GaloisInc/heapster-itree-mr-solver-alt

Update monadification and MR solver to work with the SpecM monad
GaloisInc · Jan 26, 2023 · acbf303 · acbf303
2 parents aa4297e + cc9fd58
commit acbf303
Show file tree

Hide file tree

Showing 17 changed files with 1,382 additions and 820 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -285,7 +285,7 @@ jobs:
 
         # If you change the entree-specs commit below, make sure you update the
         # documentation in saw-core-coq/README.md accordingly.
-      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3
+      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb
 
       # FIXME: the following steps generate Coq libraries for the SAW core to
       # Coq translator and builds them; if we do other Coq tests, these steps

diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
diff --git a/examples/mr_solver/SpecPrims.cry b/examples/mr_solver/SpecPrims.cry
@@ -3,25 +3,25 @@ module SpecPrims where
 
 /* Specification primitives */
 
-// The specification that holds for f x for some input x
-exists : {a, b} (a -> b) -> b
-exists f = error "Cannot run exists"
+// The specification that holds for for some element of type a
+exists : {a} a
+exists = error "Cannot run exists"
 
-// The specification that holds for f x for all inputs x
-forall : {a, b} (a -> b) -> b
-forall f = error "Cannot run forall"
+// The specification that holds for for all elements of type a
+forall : {a} a
+forall = error "Cannot run forall"
 
 // The specification that a computation has no errors
 noErrors : {a} a
-noErrors = exists (\x -> x)
+noErrors = exists
 
 // The specification that matches any computation. This calls exists at the
-// function type () -> a, which is monadified to () -> CompM a. This means that
+// function type () -> a, which is monadified to () -> SpecM a. This means that
 // the exists does not just quantify over all values of type a like noErrors,
 // but it quantifies over all computations of type a, including those that
 // contain errors.
 anySpec : {a} a
-anySpec = exists (\f -> f ())
+anySpec = exists ()
 
 // The specification which asserts that the first argument is True and then
 // returns the second argument

diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw
@@ -3,8 +3,10 @@ enable_experimental;
 import "SpecPrims.cry" as SpecPrims;
 import "monadify.cry";
 load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore";
-set_monadification "SpecPrims::exists" "Prelude.existsM";
-set_monadification "SpecPrims::forall" "Prelude.forallM";
+
+// Set the monadification of the Cryptol exists and forall functions
+set_monadification "SpecPrims::exists" "Prelude.existsS" true;
+set_monadification "SpecPrims::forall" "Prelude.forallS" true;
 
 let run_test name cry_term mon_term_expected =
   do { print (str_concat "Test: " name);
@@ -21,40 +23,48 @@ let run_test name cry_term mon_term_expected =
 
 my_abs <- unfold_term ["my_abs"] {{ my_abs }};
 my_abs_M <- parse_core_mod "CryptolM" "\
-\ \\(x : (mseq (TCNum 64) Bool)) -> \
-\   bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
+\ \\(x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \
+\   bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \
+\         (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\         (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \
 \     (\\(x' : (isFinite (TCNum 64))) -> \
-\        bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
+\        bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \
+\              (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\              (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \
 \          (\\(x'' : (isFinite (TCNum 64))) -> \
-\             ite (CompM (mseq (TCNum 64) Bool)) \
-\               (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \
-\                  (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
-\               (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
+\             ite (SpecM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)) \
+\               (ecLt (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PCmpMSeqBool VoidEv emptyFunStack (TCNum 64) x') x \
+\                  (ecNumber (TCNum 0) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 64) x''))) \
+\               (bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \
+\                      (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\                      (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \
 \                  (\\(x''' : (isFinite (TCNum 64))) -> \
-\                     returnM (mseq (TCNum 64) Bool) (ecNeg (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x))) \
-\               (returnM (mseq (TCNum 64) Bool) x)))";
+\                     retS VoidEv emptyFunStack \
+\                             (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\                             (ecNeg (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PRingMSeqBool VoidEv emptyFunStack (TCNum 64) x''') x))) \
+\               (retS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) x)))";
 run_test "my_abs" my_abs my_abs_M;
 
 err_if_lt0 <- unfold_term ["err_if_lt0"] {{ err_if_lt0 }};
 err_if_lt0_M <- parse_core_mod "CryptolM" "\
-\ \\(x : (mseq (TCNum 64) Bool)) -> \
-\   bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
+\ \\(x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \
+\   bindS VoidEv emptyFunStack (isFinite (TCNum 64)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \
 \     (\\(x' : (isFinite (TCNum 64))) -> \
-\        bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
+\        bindS VoidEv emptyFunStack (isFinite (TCNum 64)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \
 \          (\\(x'' : (isFinite (TCNum 64))) -> \
-\             ite (CompM (mseq (TCNum 64) Bool)) \
-\               (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \
-\                  (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
-\               (bindM (isFinite (TCNum 8)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 8)) \
+\             ite (SpecM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)) \
+\               (ecLt (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PCmpMSeqBool VoidEv emptyFunStack (TCNum 64) x') x \
+\                  (ecNumber (TCNum 0) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 64) x''))) \
+\               (bindS VoidEv emptyFunStack (isFinite (TCNum 8)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 8)) \
 \                  (\\(x''' : (isFinite (TCNum 8))) -> \
-\                     ecErrorM (mseq (TCNum 64) Bool) (TCNum 5) \
-\                       (seqToMseq (TCNum 5) (mseq (TCNum 8) Bool) \
-\                          [ ecNumber (TCNum 120) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \
-\                          , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \
-\                          , ecNumber (TCNum 60) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \
-\                          , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \
-\                          , ecNumber (TCNum 48) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') ]))) \
-\               (returnM (mseq (TCNum 64) Bool) x)))";
+\                     ecErrorM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) (TCNum 5) \
+\                       (seqToMseq VoidEv emptyFunStack (TCNum 5) (mseq VoidEv emptyFunStack (TCNum 8) Bool) \
+\                          [ ecNumber (TCNum 120) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') \
+\                          , (ecNumber (TCNum 32) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''')) \
+\                          , ecNumber (TCNum 60) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') \
+\                          , (ecNumber (TCNum 32) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''')) \
+\                          , ecNumber (TCNum 48) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') ]))) \
+\               (retS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) x)))";
 run_test "err_if_lt0" err_if_lt0 err_if_lt0_M;
 
 /*
@@ -69,46 +79,53 @@ print_term sha1M;
 
 fib <- unfold_term ["fib"] {{ fib }};
 fibM <- parse_core_mod "CryptolM" "\
-\ \\(_x : (mseq (TCNum 64) Bool)) -> \
-\   multiArgFixM (LRT_Fun (mseq (TCNum 64) Bool) (\\(_ : (mseq (TCNum 64) Bool)) -> LRT_Ret (mseq (TCNum 64) Bool))) \
-\     (\\(fib : ((mseq (TCNum 64) Bool) -> (CompM (mseq (TCNum 64) Bool)))) -> \
-\        \\(x : (mseq (TCNum 64) Bool)) -> \
-\          bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
-\            (\\(x' : (isFinite (TCNum 64))) -> \
-\               bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
-\                 (\\(x'' : (isFinite (TCNum 64))) -> \
-\                    ite (CompM (mseq (TCNum 64) Bool)) \
-\                      (ecEq (mseq (TCNum 64) Bool) (PEqMSeqBool (TCNum 64) x') x \
-\                         (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \
-\                      (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
-\                         (\\(x''' : (isFinite (TCNum 64))) -> \
-\                            returnM (mseq (TCNum 64) Bool) \
-\                              (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \
-\                                 (PLiteralSeqBoolM (TCNum 64) x''')))) \
-\                      (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
-\                         (\\(x''' : (isFinite (TCNum 64))) -> \
-\                            bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \
-\                              (\\(x'''' : (isFinite (TCNum 64))) -> \
-\                                 bindM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \
-\                                   (fib \
-\                                      (ecMinus (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \
-\                                         (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \
-\                                            (PLiteralSeqBoolM (TCNum 64) x'''')))) \
-\                                   (\\(x''''' : (mseq (TCNum 64) Bool)) -> \
-\                                      returnM (mseq (TCNum 64) Bool) \
-\                                        (ecMul (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \
-\                                           x''''')))))))) \
+\ \\(_x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \
+\   multiArgFixS VoidEv emptyFunStack \
+\                (LRT_Fun (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\                   (\\(_ : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \
+\                      LRT_Ret (mseq VoidEv emptyFunStack (TCNum 64) Bool))) \
+\     ((\\ (stk:FunStack) -> \
+\      (\\(fib : ((mseq VoidEv stk (TCNum 64) Bool) -> \
+\                 (SpecM VoidEv stk (mseq VoidEv stk (TCNum 64) Bool)))) -> \
+\         \\(x : (mseq VoidEv stk (TCNum 64) Bool)) -> \
+\           bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \
+\             (\\(x' : (isFinite (TCNum 64))) -> \
+\                bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \
+\                  (\\(x'' : (isFinite (TCNum 64))) -> \
+\                     ite (SpecM VoidEv stk (mseq VoidEv stk (TCNum 64) Bool)) \
+\                       (ecEq (mseq VoidEv stk (TCNum 64) Bool) (PEqMSeqBool VoidEv stk (TCNum 64) x') x \
+\                          (ecNumber (TCNum 0) (mseq VoidEv stk (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv stk (TCNum 64) x''))) \
+\                       (bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \
+\                          (\\(x''' : (isFinite (TCNum 64))) -> \
+\                             retS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) \
+\                               (ecNumber (TCNum 1) (mseq VoidEv stk (TCNum 64) Bool) \
+\                                  (PLiteralSeqBoolM VoidEv stk (TCNum 64) x''')))) \
+\                       (bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \
+\                          (\\(x''' : (isFinite (TCNum 64))) -> \
+\                             bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \
+\                               (\\(x'''' : (isFinite (TCNum 64))) -> \
+\                                  bindS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) (mseq VoidEv stk (TCNum 64) Bool) \
+\                                    (fib \
+\                                       (ecMinus (mseq VoidEv stk (TCNum 64) Bool) (PRingMSeqBool VoidEv stk (TCNum 64) x''') x \
+\                                          (ecNumber (TCNum 1) (mseq VoidEv stk (TCNum 64) Bool) \
+\                                             (PLiteralSeqBoolM VoidEv stk (TCNum 64) x'''')))) \
+\                                    (\\(x''''' : (mseq VoidEv stk (TCNum 64) Bool)) -> \
+\                                       retS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) \
+\                                         (ecMul (mseq VoidEv stk (TCNum 64) Bool) (PRingMSeqBool VoidEv stk (TCNum 64) x''') x \
+\                                            x'''''))))))))) \
+\      (pushFunStack (singletonFrame (LRT_Fun (mseq VoidEv emptyFunStack (TCNum 64) Bool) \
+\                                            (\\ (_:Vec 64 Bool) -> \
+\                                               LRT_Ret (mseq VoidEv emptyFunStack (TCNum 64) Bool)))) \
+\                    emptyFunStack)) \
 \     _x";
 run_test "fib" fib fibM;
 
 noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }};
-noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsM a a (\\(x : a) -> returnM a x)";
+noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv emptyFunStack a";
 run_test "noErrors" noErrors noErrorsM;
 
 fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }};
 fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\
-\ \\(__p1 : (mseq (TCNum 64) Bool)) -> \
-\   existsM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \
-\     (\\(x : (mseq (TCNum 64) Bool)) -> \
-\        returnM (mseq (TCNum 64) Bool) x)";
+\ \\(__p1 : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \
+\   existsS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)";
 run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM;
diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw
@@ -15,14 +15,17 @@ let run_test name test expected =
          do { print "Test failed\n"; exit 1; }; };
 
 // The constant 0 function const0 x = 0
-const0 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)";
+const0 <- parse_core
+  "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)";
 
 // The constant 1 function const1 x = 1
-const1 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 1)";
+const1 <- parse_core
+  "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)";
 
 // const0 <= const0
 run_test "const0 |= const0" (mr_solver_query const0 const0) true;
 
+/*
 // The function test_fun0 from the prelude = const0
 test_fun0 <- parse_core "test_fun0";
 run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true;
@@ -34,44 +37,52 @@ run_test "const0 |= const1" (mr_solver_query const0 const1) false;
 test_fun1 <- parse_core "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;
+*/
 
 // ifxEq0 x = If x == 0 then x else 0; should be equal to 0
 ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \
-                       \ ite (CompM (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0)) \
-                       \     (returnM (Vec 64 Bool) x) \
-                       \     (returnM (Vec 64 Bool) (bvNat 64 0))";
+                       \ 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))";
 
 // ifxEq0 <= const0
 run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true;
 
 // not ifxEq0 <= const1
 run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false;
 
-// noErrors1 x = exists x. returnM x
-noErrors1 <- parse_core "\\ (x:Vec 64 Bool) -> \
-                          \ existsM (Vec 64 Bool) (Vec 64 Bool) \
-                          \ (\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool) x)";
+// noErrors1 x = existsS x. retS x
+noErrors1 <- parse_core
+  "\\ (_:Vec 64 Bool) -> existsS VoidEv emptyFunStack (Vec 64 Bool)";
 
 // const0 <= noErrors
 run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true;
 
 // const1 <= noErrors
 run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true;
 
-// noErrorsRec1 x = orM (existsM x. returnM x) (noErrorsRec1 x)
+// noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x)
 // Intuitively, this specifies functions that either return a value or loop
 noErrorsRec1 <- parse_core
-  "fixM (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
-      \ (\\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (x:Vec 64 Bool) -> \
-          \ orM (Vec 64 Bool) \
-              \ (existsM (Vec 64 Bool) (Vec 64 Bool) \
-                       \ (\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool) x)) \
+  "fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
+      \ (\\ (f: fixSFun VoidEv emptyFunStack \
+                      \ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
+          \ (x:Vec 64 Bool) -> \
+          \ orS VoidEv (fixSStack (Vec 64 Bool) \
+                                \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
+              \ (Vec 64 Bool) \
+              \ (existsS VoidEv (fixSStack (Vec 64 Bool) \
+                                         \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
+                         \ (Vec 64 Bool)) \
               \ (f x))";
 
 // loop x = loop x
 loop1 <- parse_core
-  "fixM (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
-      \ (\\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (x:Vec 64 Bool) -> f x)";
+  "fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \
+      \ (\\ (f: fixSFun VoidEv emptyFunStack \
+                      \ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \
+          \ (x:Vec 64 Bool) -> f x)";
 
 // loop1 <= noErrorsRec1
 run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true;