Fix the SAWScript interpreter's environment handling

CHANGES.md

@@ -6,12 +6,18 @@ This release supports [version
 
 ## Changes
 
+* The `cryptol_load` and `cryptol_prims` commands now fail if used
+  in a nested scope, instead of behaving strangely.
+
 * The old behavior of SAWScript where top-level names could be
   arbitrarily rebound, such that existing uses would see the updated
   value, has been superseded. Among other problems, it wasn't
   type safe.
-  Substitute functionality is now available by using the new syntax
-  `let rebindable`.
+  Now, rebinding a variable creates a new variable that hides the
+  old one; prior references are not affected.
+
+  Substitute functionality for the old behavior is now available by
+  using the new syntax `let rebindable`.
   After `let rebindable x = 3`, `x` is mutable and a subsequent
   `let rebindable x = 4` will change the value seen by all uses.
   The value type must remain the same; to avoid unnecessary
@@ -174,6 +180,16 @@ This release supports [version
 
 ## Bug Fixes
 
+* The Cryptol environment now tracks SAWScript scopes properly (#2304).
+  Note though that SAWCore-level names, which are for example bound by
+  uses of `let {{ ... }}`, are still not scoped and can trigger
+  duplicate variable errors.
+  See #2726 for further information.
+
+* A number of internal weirdnesses in SAWScript's internal variable handling
+  have been cleaned out; for example, bindings made in `proof_subshell` no
+  longer escape the subshell (#2243).
+
 * Fix a bug that would cause SAW to crash when loading an instantiation of a
   parameterized Cryptol module that contains newtypes or enums (#2673).
 

examples/ecdsa/ecdsa.saw

@@ -412,115 +412,102 @@ p384_point_ops_sub_simp <- do {
 };
 
 p384_point_ops_field_mul_simp <- do {
-  let {{ thm x = p384_ec_point_ops::p384_point_ops.field.mul x ==
-                 p384_field::p384_field_mul x }};
+  let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.mul x ==
+                   p384_field::p384_field_mul x }};
   // This is pretty quick even without the rewriting and uniterpretation
   // used above.
-  let t = unfold_term ["thm"] {{ thm }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_point_ops_field_sq_simp <- do {
-  let {{ thm x = p384_ec_point_ops::p384_point_ops.field.sq x ==
-                 p384_field::p384_field_sq x }};
+  let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.sq x ==
+                   p384_field::p384_field_sq x }};
   // This is pretty quick even without the rewriting and uninterpretation
   // used above.
-  let t = unfold_term ["thm"] {{ thm }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_point_ops_field_mul_simp2 <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.field.mul x ==
-                 p384_field::p384_field_mul x }};
+  let t = {{ \x -> ecc::p384_curve.point_ops.field.mul x ==
+                   p384_field::p384_field_mul x }};
   // This is pretty quick even without the rewriting and uniterpretation
   // used above.
-  let t = unfold_term ["thm"] {{ thm }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_point_ops_field_sq_simp2 <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.field.sq x ==
-                 p384_field::p384_field_sq x }};
+  let t = {{ \x -> ecc::p384_curve.point_ops.field.sq x ==
+                   p384_field::p384_field_sq x }};
   // This is pretty quick even without the rewriting and uniterpretation
   // used above.
-  let t = unfold_term ["thm"] {{ thm }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 
 p384_curve_field_mul_simp <- do {
-  let {{ thm x y = ecc::p384_curve.point_ops.group_field.mul (x, y) ==
-                   mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.mul (x, y) ==
+               mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print (unint_z3 ["p384_group_mul"]) t;
 };
 
 p384_curve_field_sq_simp <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.group_field.sq x ==
-                 p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x -> ecc::p384_curve.point_ops.group_field.sq x ==
+               p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print (unint_z3 ["p384_mod_mul"]) t;
 };
 p384_curve_field_div_simp <- do {
-  let {{ thm x y = ecc::p384_curve.point_ops.group_field.div (x,y) ==
-                   p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.div (x,y) ==
+               p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print (unint_z3 ["p384_mod_div"]) t;
 };
 p384_curve_twin_mul_simp <- do {
-  let {{ thm x = ecc::p384_curve.twin_mul x ==
-                 p384_ec_mul::p384_ec_twin_mul x }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x -> ecc::p384_curve.twin_mul x ==
+                   p384_ec_mul::p384_ec_twin_mul x }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print (unint_z3 ["p384_ec_twin_mul"]) t;
 };
 p384_curve_is_equal_simp <- do {
-  let {{ thm x y = ecc::p384_curve.point_ops.group_field.is_equal (x, y) ==
-                   (x == y) }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.is_equal (x, y) ==
+                     (x == y) }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_curve_is_val_simp <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.group_field.is_val x ==
-                 p384_field::p384_is_group_val x }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x -> ecc::p384_curve.point_ops.group_field.is_val x ==
+                   p384_field::p384_is_group_val x }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_curve_norm_simp <- do {
-  let {{ thm x = ecc::p384_curve.point_ops.group_field.normalize x ==
-                 (if x < p384_field::p384_group_size
-                  then x
-                  else x - p384_field::p384_group_size) }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ \x -> ecc::p384_curve.point_ops.group_field.normalize x ==
+                   (if x < p384_field::p384_group_size
+                    then x
+                    else x - p384_field::p384_group_size) }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_curve_field_zero_simp <- do {
-  let {{ thm = ecc::p384_curve.point_ops.group_field.field_zero == 0 }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ ecc::p384_curve.point_ops.group_field.field_zero == 0 }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;
 };
 p384_curve_base_simp <- do {
-  let {{ thm = ecc::p384_curve.base == ecc::p384_base }};
-  let t = unfold_term ["thm"] {{ thm }};
+  let t = {{ ecc::p384_curve.base == ecc::p384_base }};
   let t = rewrite ss0 t;
   //print_term t;
   prove_print z3 t;

intTests/test1646/test01.log.good

@@ -0,0 +1,5 @@
+ Loading file "test01.saw"
+ x=a
+ test01.saw:8:5-8:6: Warning: Redeclaration of x
+ test01.saw:3:5-3:6: Warning: Previous declaration was here
+ x=a

intTests/test1646/test1.saw → intTests/test1646/test01.saw

@@ -1,4 +1,4 @@
-// The second f call will print x=b.
+// The second f call nowadays will print x=a.
 
 let x = "a";
 

intTests/test1646/test02.log.good

@@ -0,0 +1,5 @@
+ Loading file "test02.saw"
+ x=a
+ test02.saw:8:5-8:6: Warning: Redeclaration of x
+ test02.saw:3:5-3:6: Warning: Previous declaration was here
+ x=a

intTests/test1646/test2.saw → intTests/test1646/test02.saw

@@ -1,9 +1,9 @@
-// The second f call will panic with an internal type error.
+// The second f call nowadays just prints a.
 
 let x = "a";
 
 let f () = print (str_concat "x=" x);
 f ();
 
 let x = 5;
-f();
+f ();

intTests/test1646/test03.log.good

@@ -0,0 +1,5 @@
+ Loading file "test03.saw"
+ test03.saw:9:8-9:9: Warning: Redeclaration of x
+ test03.saw:4:8-4:9: Warning: Previous declaration was here
+ x=a
+ x=a

intTests/test1646/test04.log.good

@@ -0,0 +1,5 @@
+ Loading file "test04.saw"
+ test04.saw:9:8-9:9: Warning: Redeclaration of x
+ test04.saw:4:8-4:9: Warning: Previous declaration was here
+ x=a
+ x=a

intTests/test1646/test05.log.good

@@ -0,0 +1,3 @@
+ Loading file "test05.saw"
+ x=a
+ x=b

intTests/test1646/test06.log.good

@@ -0,0 +1,13 @@
+ Loading file "test06.saw"
+ x=a
+ test06.saw:8:16-8:17: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    test06.saw:8:20-8:21: The type Int arises from the type of this term
+    test06.saw:3:20-3:23: The type String arises from the type of this term
+
+    Expected: Int
+    Found:    String
+
+    within "x" (test06.saw:8:16-8:17)
+
+FAILED

intTests/test1646/test07.log.good

@@ -0,0 +1,8 @@
+ Loading file "test07.saw"
+ Type errors:
+  test07.saw:4:4-4:26: Invalid use of 'rebindable'
+  test07.saw:4:4-4:26: It is only allowed at the syntactic top level
+  test07.saw:9:4-9:26: Invalid use of 'rebindable'
+  test07.saw:9:4-9:26: It is only allowed at the syntactic top level
+
+FAILED

intTests/test1646/test08.log.good

@@ -0,0 +1,8 @@
+ Loading file "test08.saw"
+ Type errors:
+  test08.saw:4:4-4:26: Invalid use of 'rebindable'
+  test08.saw:4:4-4:26: It is only allowed at the syntactic top level
+  test08.saw:9:4-9:26: Invalid use of 'rebindable'
+  test08.saw:9:4-9:26: It is only allowed at the syntactic top level
+
+FAILED

intTests/test1646/test09.log.good

@@ -0,0 +1,4 @@
+ Loading file "test09.saw"
+ test09.saw:7:4-7:5: Warning: Redeclaration of x
+ test09.saw:4:16-4:17: Warning: Previous declaration was here
+ a

intTests/test1646/test09.saw

@@ -0,0 +1,11 @@
+// This should print a. Binding x in a nested scope should have no
+// effect.
+
+let rebindable x = "a";
+
+do {
+   x <- return 3;
+   return ();
+};
+
+print x;

intTests/test1646/test10.log.good

@@ -0,0 +1,4 @@
+ Loading file "test10.saw"
+ test10.saw:7:8-7:9: Warning: Redeclaration of x
+ test10.saw:4:16-4:17: Warning: Previous declaration was here
+ a

intTests/test1646/test10.saw

@@ -0,0 +1,11 @@
+// This should print a. Binding x in a nested scope creates a new
+// variable and should have no effect on the rebindable one.
+
+let rebindable x = "a";
+
+do {
+   let x = 3;
+   return ();
+};
+
+print x;

intTests/test1646/test11.log.good

@@ -0,0 +1,5 @@
+ Loading file "test11.saw"
+ test11.saw:6:8-6:9: Warning: Redeclaration of x
+ test11.saw:3:16-3:17: Warning: Previous declaration was here
+ 3
+ b

intTests/test1646/test11.saw

@@ -0,0 +1,12 @@
+// This should print 3 then b.
+
+let rebindable x = "a";
+
+do {
+   let x = 3;
+   print x;
+   return ();
+};
+
+let rebindable x = "b";
+print x;

intTests/test1646/test12.log.good

@@ -0,0 +1,7 @@
+ Loading file "test12.saw"
+ test12.saw:6:8-6:9: Warning: Redeclaration of x
+ test12.saw:3:16-3:17: Warning: Previous declaration was here
+ 3
+ test12.saw:11:5-11:6: Warning: Redeclaration of x
+ test12.saw:3:16-3:17: Warning: Previous declaration was here
+ b

intTests/test1646/test12.saw

@@ -0,0 +1,13 @@
+// This should print 3 then b.
+
+let rebindable x = "a";
+
+do {
+   let x = 3;
+   print x;
+   return ();
+};
+
+let x = "b";
+print x;
+

intTests/test1646/test13.log.good

@@ -0,0 +1,9 @@
+ Loading file "test13.saw"
+ test13.saw:7:8-7:9: Warning: Redeclaration of x
+ test13.saw:4:16-4:17: Warning: Previous declaration was here
+ 3
+ test13.saw:12:5-12:6: Warning: Redeclaration of x
+ test13.saw:4:16-4:17: Warning: Previous declaration was here
+ b
+ test13.saw:15:16-15:17: Cannot rebind x: Previous binding was not tagged 'rebindable'
+FAILED

intTests/test1646/test13.saw

@@ -0,0 +1,16 @@
+// This is rejected; once the rebindable tag is dropped it can't be
+// readded.
+
+let rebindable x = "a";
+
+do {
+   let x = 3;
+   print x;
+   return ();
+};
+
+let x = "b";
+print x;
+
+let rebindable x = "c";
+print x;

intTests/test1646/test14.log.good

@@ -0,0 +1,6 @@
+ Loading file "test14.saw"
+ x=a
+ x=b
+ test14.saw:11:5-11:6: Warning: Redeclaration of x
+ test14.saw:8:16-8:17: Warning: Previous declaration was here
+ x=b

intTests/test1646/test14.saw

@@ -0,0 +1,12 @@
+// The second f call should print x=b. So should the third.
+
+let rebindable x = "a";
+
+let f () = print (str_concat "x=" x);
+f ();
+
+let rebindable x = "b";
+f ();
+
+let x = "c";
+f ();

intTests/test1646/test15.isaw

@@ -0,0 +1,4 @@
+let rebindable x = 3
+let rebindable y = 4
+let y = 5
+:env