Further typechecker and interpreter cleanup

CHANGES.md

@@ -11,13 +11,53 @@
 
 ## Bug fixes
 
+* Unexpected special-case type behavior of monad binds in the
+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.)
+See issue #2162.
+
+There are three 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 statements of the form ```x <- e;``` where ```e```
+is a pure (non-monadic) term used to be (improperly) accepted at the
+top level of scripts.
+These statements now generate a warning.
+This will become an error in a future release and such statements
+should be rewritten as ```let x = e;```.
+For example, ```t <- unfold_term ["reverse"] {{ reverse 0b01 }};```
+should be changed to ```let t = unfold_term ["reverse"] {{ reverse 0b01 }};```.
+
+The third is that statements of the form ```x <- s;``` or just ```s;```
+where ```s``` is a term in the _wrong_ monad also used to be
+improperly accepted at the top level of scripts.
+These statements silently did nothing.
+They will now generate a warning.
+This will become an error in a future release.
+Such statements should be removed or rewritten.
+For example, it used to be possible to write ```llvm_assert {{ False }};```
+at the top level (outside any specification) and it would be ignored.
+```llvm_assert``` is only meaningful within an LLVM specification.
+
 * A number of SAWScript type checking problems have been fixed,
 including issue #2077.
-Some of these problems were partially mutually compensating; for
-example, in some cases nonexistent typedefs had been mishandled in
-ways that made them mostly work.
 Some previously accepted scripts and specs may be rejected and need
 (generally minor) adjustment.
+Prior to these changes the typechecker allowed unbound type variables
+in a number of places (such as on the right-hand side of typedefs, and
+in function signatures), so for example type names contaning typos
+would not necessarily have been caught and will now fail.
+```typedef t = nonexistent``` was previously accepted and now is not.
+These problems could trigger panics, but there does not appear to have
+been any way to produce unsoundness in the sense of false
+verifications.
 
 * Counterexamples including SMT arrays are now printed with the array
   contents instead of placeholder text.

doc/manual/manual.md

@@ -3353,8 +3353,8 @@ look up `S<u8, u16>` and `S<u32, u64>` from the example above as `MIRAdt`s:
 ~~~~
 m <- mir_load_module "example.linked-mir.json";
 
-s_8_16  <- mir_find_adt m "example::S" [mir_u8,  mir_u16];
-s_32_64 <- mir_find_adt m "example::S" [mir_u32, mir_u64];
+let s_8_16  = mir_find_adt m "example::S" [mir_u8,  mir_u16];
+let s_32_64 = mir_find_adt m "example::S" [mir_u32, mir_u64];
 ~~~~
 
 The `mir_adt` command (for constructing a struct type), `mir_struct_value` (for
@@ -3384,7 +3384,7 @@ pub fn s(x: u32) -> Option<u32> {
 ~~~~
 m <- mir_load_module "example.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 n_spec = do {
   mir_execute_func [];

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/misc/rewrite.saw

@@ -7,7 +7,7 @@ rule_thm <- prove_print (admit "assume rule") rule;
 print "== Original version of rule:";
 print_term rule;
 let rule_ss = addsimps [rule_thm] empty_ss;
-t <- rewrite rule_ss rule;
+let t = rewrite rule_ss rule;
 print "== Rule rewritten with itself:";
 print_term t;
 print "== Proof result:";

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