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

@@ -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,

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;

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;

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;

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);

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";
 
 
 ////////////////////////////////////////////////////

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 }});

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 }});

heapster-saw/examples/linked_list_mr_solver.saw

@@ -26,10 +26,10 @@ heapster_typecheck_fun env "is_head"
   "(). arg0:int64<>, arg1:List<int64<>,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 }});

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);

intTests/test1894/test.saw

@@ -1 +1 @@
-(\n -> n) 1;
+return ((\n -> n) 1);

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);

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;