From 06b3516b08fc0afff9b748aadbbf1f3d36e79ada Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 18 Dec 2024 19:02:52 -0500 Subject: [PATCH] Fix examples and tests that don't typecheck any more. In particular the interpreter used to allow "x <- e;" for a pure term e as long as it was at the syntactic top level; this should have been "let x = e;" and now it will be rejected. The failures so far (except for one) have been linked to three specific saw-script builtins: unfold_term, parse_core_mod, and mir_find_adt. I've checked all uses I can find of these. There might be more cases lurking though. Also update the CHANGES entry to specifically mention this behavior, since it's quite conceivable that downstream users will have their own instances of this problem. --- CHANGES.md | 7 +- doc/rust-tutorial/code/enums.saw | 2 +- doc/rust-tutorial/code/structs.saw | 8 +- examples/mr_solver/monadify.saw | 20 ++--- examples/mr_solver/mr_solver_unit_tests.saw | 16 ++-- heapster-saw/examples/Dilithium2.saw | 86 +++++++++---------- heapster-saw/examples/arrays_mr_solver.saw | 6 +- .../examples/exp_explosion_mr_solver.saw | 2 +- .../examples/linked_list_mr_solver.saw | 6 +- heapster-saw/examples/sha512_mr_solver.saw | 8 +- intTests/test1894/test.saw | 2 +- intTests/test1973/test.saw | 2 +- intTests/test_intro_examples/rewrite.saw | 2 +- 13 files changed, 86 insertions(+), 81 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ce66f10607..d4b02eddce 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -16,12 +16,17 @@ syntactic top level has been removed. (This was _not_ specifically associated with the TopLevel monad, so top-level binds and binds in functions in TopLevel, or in nested do-blocks, would behave differently.) -The primary visible consequence is that the repl no longer accepts +There are two primary visible consequences. +The first is that the repl no longer accepts non-monadic expressions. These can still be evaluated and printed; just prefix them with ```return```. (Affordances specifically for the repl so this is not required there may be restored in the future.) +The second is that top-level statements of the form ```x <- e;``` +where ```e``` is a pure (non-monadic) term used to be (improperly) +accepted. +These are now rejected and need to be changed to ```let x = e;```. See issue #2162. * A number of SAWScript type checking problems have been fixed, diff --git a/doc/rust-tutorial/code/enums.saw b/doc/rust-tutorial/code/enums.saw index c45c4b67f5..05c337a6ce 100644 --- a/doc/rust-tutorial/code/enums.saw +++ b/doc/rust-tutorial/code/enums.saw @@ -2,7 +2,7 @@ enable_experimental; m <- mir_load_module "enums.linked-mir.json"; -option_u32 <- mir_find_adt m "core::option::Option" [mir_u32]; +let option_u32 = mir_find_adt m "core::option::Option" [mir_u32]; let i_found_something_spec = do { x <- mir_fresh_var "x" mir_u32; diff --git a/doc/rust-tutorial/code/structs.saw b/doc/rust-tutorial/code/structs.saw index be8d957c92..e08eca0212 100644 --- a/doc/rust-tutorial/code/structs.saw +++ b/doc/rust-tutorial/code/structs.saw @@ -2,9 +2,9 @@ enable_experimental; m <- mir_load_module "structs.linked-mir.json"; -s_adt <- mir_find_adt m "structs::S" []; -t_adt <- mir_find_adt m "structs::T" []; -foo_adt <- mir_find_adt m "structs::Foo" [mir_u32, mir_u64]; +let s_adt = mir_find_adt m "structs::S" []; +let t_adt = mir_find_adt m "structs::T" []; +let foo_adt = mir_find_adt m "structs::Foo" [mir_u32, mir_u64]; let make_foo_spec = do { mir_execute_func []; @@ -17,7 +17,7 @@ let make_foo_spec = do { mir_verify m "structs::make_foo" [] false make_foo_spec z3; -bar_adt <- mir_find_adt m "structs::Bar" []; +let bar_adt = mir_find_adt m "structs::Bar" []; let do_stuff_with_bar_spec1 = do { z1 <- mir_fresh_var "z1" mir_u32; diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw index 20a382d7d1..e174a18c45 100644 --- a/examples/mr_solver/monadify.saw +++ b/examples/mr_solver/monadify.saw @@ -21,8 +21,8 @@ let run_test name cry_term mon_term_expected = print_term mon_term_expected; exit 1; }; }; -my_abs <- unfold_term ["my_abs"] {{ my_abs }}; -my_abs_M <- parse_core_mod "CryptolM" "\ +let my_abs = unfold_term ["my_abs"] {{ my_abs }}; +let my_abs_M = parse_core_mod "CryptolM" "\ \ \\(x : (mseq VoidEv (TCNum 64) Bool)) -> \ \ bindS VoidEv (isFinite (TCNum 64)) \ \ (mseq VoidEv (TCNum 64) Bool) \ @@ -45,8 +45,8 @@ my_abs_M <- parse_core_mod "CryptolM" "\ \ (retS VoidEv (mseq VoidEv (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" "\ +let err_if_lt0 = unfold_term ["err_if_lt0"] {{ err_if_lt0 }}; +let err_if_lt0_M = parse_core_mod "CryptolM" "\ \ \\(x : (mseq VoidEv (TCNum 64) Bool)) -> \ \ bindS VoidEv (isFinite (TCNum 64)) (mseq VoidEv (TCNum 64) Bool) (assertFiniteS VoidEv (TCNum 64)) \ \ (\\(x' : (isFinite (TCNum 64))) -> \ @@ -77,8 +77,8 @@ print "Monadified term:"; print_term sha1M; */ -fib <- unfold_term ["fib"] {{ fib }}; -fibM <- parse_core_mod "CryptolM" "\ +let fib = unfold_term ["fib"] {{ fib }}; +let fibM = parse_core_mod "CryptolM" "\ \ \\(_x : Vec 64 Bool) -> \ \ FixS VoidEv (Tp_Arr (Tp_bitvector 64) (Tp_M (Tp_bitvector 64))) \ \ (\\(fib : (Vec 64 Bool -> SpecM VoidEv (Vec 64 Bool))) -> \ @@ -115,12 +115,12 @@ fibM <- parse_core_mod "CryptolM" "\ \ _x"; run_test "fib" fib fibM; -noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }}; -noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv a"; +let noErrors = unfold_term ["noErrors"] {{ SpecPrims::noErrors }}; +let noErrorsM = parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv a"; run_test "noErrors" noErrors noErrorsM; -fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }}; -fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\ +let fibSpecNoErrors = unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }}; +let fibSpecNoErrorsM = parse_core_mod "CryptolM" "\ \ \\(__p1 : (mseq VoidEv (TCNum 64) Bool)) -> \ \ existsS VoidEv (mseq VoidEv (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 index ac0f9482d4..870f50521b 100644 --- a/examples/mr_solver/mr_solver_unit_tests.saw +++ b/examples/mr_solver/mr_solver_unit_tests.saw @@ -19,11 +19,11 @@ let run_test name test expected = // The constant 0 function const0 x = 0 let ret0_core = "retS VoidEv (Vec 64 Bool) (bvNat 64 0)"; let const0_core = str_concat "\\ (_:Vec 64 Bool) -> " ret0_core; -const0 <- parse_core_mod "SpecM" const0_core; +let const0 = parse_core_mod "SpecM" const0_core; // The constant 1 function const1 x = 1 let const1_core = "\\ (_:Vec 64 Bool) -> retS VoidEv (Vec 64 Bool) (bvNat 64 1)"; -const1 <- parse_core_mod "SpecM" const1_core; +let const1 = parse_core_mod "SpecM" const1_core; // const0 <= const0 prove_extcore mrsolver (refines [] const0 const0); @@ -41,7 +41,7 @@ run_test "refines [x] (const0 x) (const0 x)" (term_apply const0 [x]))) true; // The function test_fun0 <= const0 -test_fun0 <- parse_core_mod "test_funs" "test_fun0"; +let test_fun0 = parse_core_mod "test_funs" "test_fun0"; prove_extcore mrsolver (refines [] const0 test_fun0); // (testing that "refines [] const0 test_fun0" is actually "const0 <= test_fun0") let const0_test_fun0_refines = @@ -60,7 +60,7 @@ run_test "refines [] const0 const1" (is_convertible (parse_core_mod "SpecM" cons (refines [] const0 const1)) true; // The function test_fun1 = const1 -test_fun1 <- parse_core_mod "test_funs" "test_fun1"; +let test_fun1 = parse_core_mod "test_funs" "test_fun1"; 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") @@ -82,7 +82,7 @@ let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \ \ (bvEq 64 x (bvNat 64 0)) \ \ (retS VoidEv (Vec 64 Bool) x) \ \ (retS VoidEv (Vec 64 Bool) (bvNat 64 0))"; -ifxEq0 <- parse_core_mod "SpecM" ifxEq0_core; +let ifxEq0 = parse_core_mod "SpecM" ifxEq0_core; // ifxEq0 <= const0 prove_extcore mrsolver (refines [] ifxEq0 const0); @@ -106,7 +106,7 @@ run_test "refines [] ifxEq0 const1" (is_convertible (parse_core_mod "SpecM" ifxE // noErrors1 x = existsS x. retS x let noErrors1_core = "\\ (_:Vec 64 Bool) -> existsS VoidEv (Vec 64 Bool)"; -noErrors1 <- parse_core_mod "SpecM" noErrors1_core; +let noErrors1 = parse_core_mod "SpecM" noErrors1_core; // const0 <= noErrors prove_extcore mrsolver (refines [] noErrors1 noErrors1); @@ -136,14 +136,14 @@ let noErrorsRec1_core = \ (Vec 64 Bool) \ \ (existsS VoidEv (Vec 64 Bool)) \ \ (f x))"; -noErrorsRec1 <- parse_core_mod "SpecM" noErrorsRec1_core; +let noErrorsRec1 = parse_core_mod "SpecM" noErrorsRec1_core; // loop x = loop x let loop1_core = "FixS VoidEv (Tp_Arr (Tp_bitvector 64) (Tp_M (Tp_bitvector 64))) \ \ (\\ (f: Vec 64 Bool -> SpecM VoidEv (Vec 64 Bool)) \ \ (x:Vec 64 Bool) -> f x)"; -loop1 <- parse_core_mod "SpecM" loop1_core; +let loop1 = parse_core_mod "SpecM" loop1_core; // loop1 <= noErrorsRec1 prove_extcore mrsolver (refines [] loop1 noErrorsRec1); diff --git a/heapster-saw/examples/Dilithium2.saw b/heapster-saw/examples/Dilithium2.saw index 89a45c9d20..a62f408887 100644 --- a/heapster-saw/examples/Dilithium2.saw +++ b/heapster-saw/examples/Dilithium2.saw @@ -301,49 +301,49 @@ heapster_typecheck_fun_rename env "pqcrystals_dilithium2_ref_verify" "crypto_sig // The saw-core terms generated by Heapster // ////////////////////////////////////////////// -randombytes <- parse_core_mod "Dilithium2" "randombytes"; -shake256_init <- parse_core_mod "Dilithium2" "shake256_init"; -shake256_absorb <- parse_core_mod "Dilithium2" "shake256_absorb"; -shake256_finalize <- parse_core_mod "Dilithium2" "shake256_finalize"; -shake256_squeeze <- parse_core_mod "Dilithium2" "shake256_squeeze"; -shake256 <- parse_core_mod "Dilithium2" "shake256"; -poly_challenge <- parse_core_mod "Dilithium2" "poly_challenge"; -poly_ntt <- parse_core_mod "Dilithium2" "poly_ntt"; -polyvec_matrix_expand <- parse_core_mod "Dilithium2" "polyvec_matrix_expand"; -polyvec_matrix_pointwise_montgomery <- parse_core_mod "Dilithium2" "polyvec_matrix_pointwise_montgomery"; -polyvecl_uniform_eta <- parse_core_mod "Dilithium2" "polyvecl_uniform_eta"; -polyvecl_uniform_gamma1 <- parse_core_mod "Dilithium2" "polyvecl_uniform_gamma1"; -polyvecl_reduce <- parse_core_mod "Dilithium2" "polyvecl_reduce"; -polyvecl_add <- parse_core_mod "Dilithium2" "polyvecl_add"; -polyvecl_ntt <- parse_core_mod "Dilithium2" "polyvecl_ntt"; -polyvecl_invntt_tomont <- parse_core_mod "Dilithium2" "polyvecl_invntt_tomont"; -polyvecl_pointwise_poly_montgomery <- parse_core_mod "Dilithium2" "polyvecl_pointwise_poly_montgomery"; -polyvecl_chknorm <- parse_core_mod "Dilithium2" "polyvecl_chknorm"; -polyveck_uniform_eta <- parse_core_mod "Dilithium2" "polyveck_uniform_eta"; -polyveck_reduce <- parse_core_mod "Dilithium2" "polyveck_reduce"; -polyveck_caddq <- parse_core_mod "Dilithium2" "polyveck_caddq"; -polyveck_add <- parse_core_mod "Dilithium2" "polyveck_add"; -polyveck_sub <- parse_core_mod "Dilithium2" "polyveck_sub"; -polyveck_shiftl <- parse_core_mod "Dilithium2" "polyveck_shiftl"; -polyveck_ntt <- parse_core_mod "Dilithium2" "polyveck_ntt"; -polyveck_invntt_tomont <- parse_core_mod "Dilithium2" "polyveck_invntt_tomont"; -polyveck_pointwise_poly_montgomery <- parse_core_mod "Dilithium2" "polyveck_pointwise_poly_montgomery"; -polyveck_chknorm <- parse_core_mod "Dilithium2" "polyveck_chknorm"; -polyveck_power2round <- parse_core_mod "Dilithium2" "polyveck_power2round"; -polyveck_decompose <- parse_core_mod "Dilithium2" "polyveck_decompose"; -polyveck_make_hint <- parse_core_mod "Dilithium2" "polyveck_make_hint"; -polyveck_use_hint <- parse_core_mod "Dilithium2" "polyveck_use_hint"; -polyveck_pack_w1 <- parse_core_mod "Dilithium2" "polyveck_pack_w1"; -pack_pk <- parse_core_mod "Dilithium2" "pack_pk"; -unpack_pk <- parse_core_mod "Dilithium2" "unpack_pk"; -pack_sk <- parse_core_mod "Dilithium2" "pack_sk"; -unpack_sk <- parse_core_mod "Dilithium2" "unpack_sk"; -pack_sig <- parse_core_mod "Dilithium2" "pack_sig"; -unpack_sig <- parse_core_mod "Dilithium2" "unpack_sig"; -crypto_sign_keypair <- parse_core_mod "Dilithium2" "crypto_sign_keypair"; -crypto_sign_signature <- parse_core_mod "Dilithium2" "crypto_sign_signature"; -crypto_sign <- parse_core_mod "Dilithium2" "crypto_sign"; -crypto_sign_verify <- parse_core_mod "Dilithium2" "crypto_sign_verify"; +let randombytes = parse_core_mod "Dilithium2" "randombytes"; +let shake256_init = parse_core_mod "Dilithium2" "shake256_init"; +let shake256_absorb = parse_core_mod "Dilithium2" "shake256_absorb"; +let shake256_finalize = parse_core_mod "Dilithium2" "shake256_finalize"; +let shake256_squeeze = parse_core_mod "Dilithium2" "shake256_squeeze"; +let shake256 = parse_core_mod "Dilithium2" "shake256"; +let poly_challenge = parse_core_mod "Dilithium2" "poly_challenge"; +let poly_ntt = parse_core_mod "Dilithium2" "poly_ntt"; +let polyvec_matrix_expand = parse_core_mod "Dilithium2" "polyvec_matrix_expand"; +let polyvec_matrix_pointwise_montgomery = parse_core_mod "Dilithium2" "polyvec_matrix_pointwise_montgomery"; +let polyvecl_uniform_eta = parse_core_mod "Dilithium2" "polyvecl_uniform_eta"; +let polyvecl_uniform_gamma1 = parse_core_mod "Dilithium2" "polyvecl_uniform_gamma1"; +let polyvecl_reduce = parse_core_mod "Dilithium2" "polyvecl_reduce"; +let polyvecl_add = parse_core_mod "Dilithium2" "polyvecl_add"; +let polyvecl_ntt = parse_core_mod "Dilithium2" "polyvecl_ntt"; +let polyvecl_invntt_tomont = parse_core_mod "Dilithium2" "polyvecl_invntt_tomont"; +let polyvecl_pointwise_poly_montgomery = parse_core_mod "Dilithium2" "polyvecl_pointwise_poly_montgomery"; +let polyvecl_chknorm = parse_core_mod "Dilithium2" "polyvecl_chknorm"; +let polyveck_uniform_eta = parse_core_mod "Dilithium2" "polyveck_uniform_eta"; +let polyveck_reduce = parse_core_mod "Dilithium2" "polyveck_reduce"; +let polyveck_caddq = parse_core_mod "Dilithium2" "polyveck_caddq"; +let polyveck_add = parse_core_mod "Dilithium2" "polyveck_add"; +let polyveck_sub = parse_core_mod "Dilithium2" "polyveck_sub"; +let polyveck_shiftl = parse_core_mod "Dilithium2" "polyveck_shiftl"; +let polyveck_ntt = parse_core_mod "Dilithium2" "polyveck_ntt"; +let polyveck_invntt_tomont = parse_core_mod "Dilithium2" "polyveck_invntt_tomont"; +let polyveck_pointwise_poly_montgomery = parse_core_mod "Dilithium2" "polyveck_pointwise_poly_montgomery"; +let polyveck_chknorm = parse_core_mod "Dilithium2" "polyveck_chknorm"; +let polyveck_power2round = parse_core_mod "Dilithium2" "polyveck_power2round"; +let polyveck_decompose = parse_core_mod "Dilithium2" "polyveck_decompose"; +let polyveck_make_hint = parse_core_mod "Dilithium2" "polyveck_make_hint"; +let polyveck_use_hint = parse_core_mod "Dilithium2" "polyveck_use_hint"; +let polyveck_pack_w1 = parse_core_mod "Dilithium2" "polyveck_pack_w1"; +let pack_pk = parse_core_mod "Dilithium2" "pack_pk"; +let unpack_pk = parse_core_mod "Dilithium2" "unpack_pk"; +let pack_sk = parse_core_mod "Dilithium2" "pack_sk"; +let unpack_sk = parse_core_mod "Dilithium2" "unpack_sk"; +let pack_sig = parse_core_mod "Dilithium2" "pack_sig"; +let unpack_sig = parse_core_mod "Dilithium2" "unpack_sig"; +let crypto_sign_keypair = parse_core_mod "Dilithium2" "crypto_sign_keypair"; +let crypto_sign_signature = parse_core_mod "Dilithium2" "crypto_sign_signature"; +let crypto_sign = parse_core_mod "Dilithium2" "crypto_sign"; +let crypto_sign_verify = parse_core_mod "Dilithium2" "crypto_sign_verify"; //////////////////////////////////////////////////// diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw index a67d31ec6a..21c9f2f453 100644 --- a/heapster-saw/examples/arrays_mr_solver.saw +++ b/heapster-saw/examples/arrays_mr_solver.saw @@ -1,10 +1,10 @@ include "arrays.saw"; // Test that contains0 |= contains0 -contains0 <- parse_core_mod "arrays" "contains0"; +let contains0 = parse_core_mod "arrays" "contains0"; prove_extcore mrsolver (refines [] contains0 contains0); -noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0"; +let noErrorsContains0 = parse_core_mod "arrays" "noErrorsContains0"; prove_extcore mrsolver (refines [] contains0 noErrorsContains0); include "specPrims.saw"; @@ -13,6 +13,6 @@ import "arrays.cry"; monadify_term {{ zero_array_spec }}; // FIXME: Uncomment once FunStacks are removed -zero_array <- parse_core_mod "arrays" "zero_array"; +let zero_array = parse_core_mod "arrays" "zero_array"; prove_extcore mrsolver (refines [] zero_array {{ zero_array_loop_spec }}); prove_extcore mrsolver (refines [] zero_array {{ zero_array_spec }}); diff --git a/heapster-saw/examples/exp_explosion_mr_solver.saw b/heapster-saw/examples/exp_explosion_mr_solver.saw index 0cf92af63e..f4833cd98f 100644 --- a/heapster-saw/examples/exp_explosion_mr_solver.saw +++ b/heapster-saw/examples/exp_explosion_mr_solver.saw @@ -2,5 +2,5 @@ include "exp_explosion.saw"; import "exp_explosion.cry"; -exp_explosion <- parse_core_mod "exp_explosion" "exp_explosion"; +let exp_explosion = parse_core_mod "exp_explosion" "exp_explosion"; prove_extcore mrsolver (refines [] exp_explosion {{ exp_explosion_spec }}); diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index a64acdef73..9eec7bf536 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -26,10 +26,10 @@ heapster_typecheck_fun env "is_head" "(). arg0:int64<>, arg1:List,always,R> -o \ \ arg0:true, arg1:true, ret:int64<>"; -is_head <- parse_core_mod "linked_list" "is_head"; +let is_head = parse_core_mod "linked_list" "is_head"; prove_extcore mrsolver (refines [] is_head is_head); -is_elem <- parse_core_mod "linked_list" "is_elem"; +let is_elem = parse_core_mod "linked_list" "is_elem"; prove_extcore mrsolver (refines [] is_elem is_elem); is_elem_noErrorsSpec <- parse_core @@ -61,5 +61,5 @@ monadify_term {{ Left }}; monadify_term {{ nil }}; monadify_term {{ cons }}; -sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc"; +let sorted_insert_no_malloc = parse_core_mod "linked_list" "sorted_insert_no_malloc"; prove_extcore mrsolver (refines [] sorted_insert_no_malloc {{ sorted_insert_spec }}); diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw index 27d38a002d..5a41fd28a8 100644 --- a/heapster-saw/examples/sha512_mr_solver.saw +++ b/heapster-saw/examples/sha512_mr_solver.saw @@ -1,9 +1,9 @@ include "sha512.saw"; -round_00_15 <- parse_core_mod "SHA512" "round_00_15"; -round_16_80 <- parse_core_mod "SHA512" "round_16_80"; -processBlock <- parse_core_mod "SHA512" "processBlock"; -processBlocks <- parse_core_mod "SHA512" "processBlocks"; +let round_00_15= parse_core_mod "SHA512" "round_00_15"; +let round_16_80 = parse_core_mod "SHA512" "round_16_80"; +let processBlock = parse_core_mod "SHA512" "processBlock"; +let processBlocks = parse_core_mod "SHA512" "processBlocks"; // Test that every function refines itself // prove_extcore mrsolver (refines [] processBlocks processBlocks); diff --git a/intTests/test1894/test.saw b/intTests/test1894/test.saw index 7e22ea36a3..900a38462d 100644 --- a/intTests/test1894/test.saw +++ b/intTests/test1894/test.saw @@ -1 +1 @@ -(\n -> n) 1; +return ((\n -> n) 1); diff --git a/intTests/test1973/test.saw b/intTests/test1973/test.saw index 173e71ba4e..ed2a7fc2cd 100644 --- a/intTests/test1973/test.saw +++ b/intTests/test1973/test.saw @@ -2,7 +2,7 @@ enable_experimental; m <- mir_load_module "test.linked-mir.json"; -s_adt <- mir_find_adt m "test::S" []; +let s_adt = mir_find_adt m "test::S" []; let f_spec = do { s_ref <- mir_alloc (mir_adt s_adt); diff --git a/intTests/test_intro_examples/rewrite.saw b/intTests/test_intro_examples/rewrite.saw index d5a7e693e8..faefde6963 100644 --- a/intTests/test_intro_examples/rewrite.saw +++ b/intTests/test_intro_examples/rewrite.saw @@ -5,7 +5,7 @@ let {{ }}; f_eq_g <- prove_print abc {{ \x y -> f x y == g x y }}; print f_eq_g; -t1 <- unfold_term ["h"] {{ \x y -> h x y == 2*(f x y) }}; +let t1 = unfold_term ["h"] {{ \x y -> h x y == 2*(f x y) }}; print_term t1; t2 <- rewrite (addsimp f_eq_g empty_ss) t1; print_term t2;