Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update monadification and MR solver to work with the SpecM monad #1806

Merged
merged 31 commits into from
Jan 26, 2023
Merged

Update monadification and MR solver to work with the SpecM monad #1806

Show file tree
Hide file tree
Changes from 29 commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
a8194fd
Updated MR solver to work with SpecM instead of CompM
Dec 5, 2022
11bc867
got some of the MR solver unit tests working
Dec 6, 2022
3b28cc1
changed mrFreshCallVars to normalize the frame argument
Dec 6, 2022
ffd5b18
fixed a bug in mrFreshCallVars where uvars were not getting properly …
Dec 6, 2022
409888e
changed CompFuns to keep around their event types and fun stacks
Dec 7, 2022
1804e0f
added multiArgFixS
Dec 7, 2022
c3350ec
started updating linked_list_mr_solver.saw
Dec 7, 2022
9c63042
updated the core algorithm of the monadifier to use SpecM
Dec 7, 2022
b17a83e
fixed mrFreshCallVars to normalize the defs term; fixed a small print…
Dec 7, 2022
f9c9486
updated the noErrors spec in linked_list_mr_solver.saw
Dec 7, 2022
1280328
add debug output to missing mrProveRel case
m-yac Dec 8, 2022
d72e04b
un-comment a line that was accidentally commented by a previous commit
Dec 8, 2022
1e1b7e1
fixed mrReplaceCallsWithTerms to use term lifting when it recurses in…
Dec 8, 2022
5041302
Merge branch 'heapster-itree' into heapster-itree-mr-solver-alt
Dec 8, 2022
c82e5e3
updated the monadified versions of the cryptol primitives to use SpecM
Dec 10, 2022
19296d2
fixed some small bugs in CryptolM.sawcore
Dec 12, 2022
c58bf45
added list1OpenTerm operator
Dec 12, 2022
98927cf
fixed fixMacro to push the new frame onto the function stack when rec…
Dec 13, 2022
8b284e3
fixed the fixMacro to wrk, I think...
Dec 13, 2022
87bff2e
changed mrFreshVar to abstract over the current uvar context; added s…
Dec 13, 2022
9b168f3
updated the normalizer in SMT.hs to work with SpecM types
Dec 14, 2022
c3e7d6c
Merge branch 'master' into heapster-itree-mr-solver-alt
Dec 14, 2022
738897b
Merge branch 'master' into heapster-itree-mr-solver-alt
Jan 19, 2023
f74a65d
Merge branch 'master' into heapster-itree-mr-solver-alt
Jan 25, 2023
0fe52c5
updated some of the monadification tests to work with SpecM
Jan 25, 2023
9045407
commented out tests involving monadifying quantifiers, which don't qu…
Jan 25, 2023
1e16b60
changed the set_monadification command to allow for monadifications t…
Jan 25, 2023
ef7c47c
updated the monadification tests to succeed with the new SpecM monad
Jan 25, 2023
2a5bc52
resolve defined-but-not-used warnings in Solver.hs
m-yac Jan 25, 2023
603420f
update pinned commit to entree-specs
m-yac Jan 25, 2023
cc9fd58
style tweak in constraints in Monadify.hs
m-yac Jan 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
686 changes: 396 additions & 290 deletions cryptol-saw-core/saw/CryptolM.sawcore
View file
Open in desktop

Large diffs are not rendered by default.

507 changes: 340 additions & 167 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs
View file
Open in desktop

Large diffs are not rendered by default.

18 changes: 9 additions & 9 deletions examples/mr_solver/SpecPrims.cry
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
137 changes: 77 additions & 60 deletions examples/mr_solver/monadify.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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;

/*
Expand All @@ -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;
45 changes: 28 additions & 17 deletions examples/mr_solver/mr_solver_unit_tests.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
22 changes: 16 additions & 6 deletions heapster-saw/examples/linked_list_mr_solver.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,13 +35,23 @@ mr_solver_test is_elem is_elem;

is_elem_noErrorsSpec <- parse_core
"\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \
\ fixM (Vec 64 Bool * List (Vec 64 Bool)) \
\ (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \
\ (\\ (rec : (x : Vec 64 Bool * List (Vec 64 Bool)) -> CompM (Vec 64 Bool)) \
\ fixS VoidEv emptyFunStack \
\ (Vec 64 Bool * List (Vec 64 Bool)) \
\ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \
\ (\\ (f : fixSFun VoidEv emptyFunStack \
\ (Vec 64 Bool * List (Vec 64 Bool)) \
\ (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> \
\ Vec 64 Bool)) \
\ (x : Vec 64 Bool * List (Vec 64 Bool)) -> \
\ orM (Vec 64 Bool) \
\ (existsM (Vec 64 Bool) (Vec 64 Bool) (returnM (Vec 64 Bool))) \
\ (rec x)) (x, y)";
\ orS VoidEv (fixSStack (Vec 64 Bool * List (Vec 64 Bool)) \
\ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> \
\ Vec 64 Bool)) \
\ (Vec 64 Bool) \
\ (existsS VoidEv (fixSStack (Vec 64 Bool * List (Vec 64 Bool)) \
\ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> \
\ Vec 64 Bool)) \
\ (Vec 64 Bool)) \
\ (f x)) (x, y)";
mr_solver_test is_elem is_elem_noErrorsSpec;

mr_solver_prove is_elem {{ is_elem_spec }};
Expand Down
Loading