[CERT-3525] reset storage syntax

docs/cvl/expr.md

@@ -53,7 +53,7 @@ specials_fields ::=
 
 special_vars ::=
            | "lastReverted" | "lastHasThrown"
-           | "lastStorage"
+           | "lastStorage"  | "currentStorage"
            | "allContracts"
            | "lastMsgSig"
            | "_"
@@ -287,7 +287,8 @@ There are also several built-in variables:
    overwriting the value set by `withdraw`.
    ````
 
- * `lastStorage` refers to the most recent state of the EVM storage.  See
+ * `currentStorage` refers to the most recent state of the EVM storage.
+   `lastStorage` is a deprecated synonym for `currentStorage`.  See
    {ref}`storage-type` for more details.
 
  * You can use the variable `_` as a placeholder for a value you are not
@@ -408,9 +409,9 @@ using MyContract as c;
 using OtherContract as o;
 
 rule compare_state_of_c(env e) {
-   storage init = lastStorage;
+   storage init = currentStorage;
    o.mutateOtherState(e); // changes `o` but not `c`
-   assert lastStorage[c] == init[c];
+   assert currentStorage[c] == init[c];
 }
 ```
 
@@ -421,9 +422,9 @@ using MyContract as c;
 using OtherContract as o;
 
 rule compare_state_of_c(env e) {
-   storage init = lastStorage;
+   storage init = currentStorage;
    c.mutateContractState(e); // changes `c`
-   assert lastStorage[c] == init[c];
+   assert currentStorage[c] == init[c];
 }
 ```
 

docs/cvl/types.md

@@ -263,33 +263,57 @@ CVL supports this kind of specification using the special `storage` type.  A
 variable of type `storage` represents a snapshot of the EVM storage and
 the state of {ref}`ghosts <ghost-functions>` at a given point in time.
 
-The EVM storage can be reset to a saved storage value `s` by appending `at s` to
-the end of a function call.  For example, the following rule checks that "if you
+The EVM storage can be reset to a saved storage by assigning to the
+`currentStorage` variable.  For example, the following rule checks that "if you
 stake more, you earn more":
 
 ```cvl
 rule bigger_stake_more_earnings() {
-    storage initial = lastStorage;
+    storage initial = currentStorage;
     env e;
 
     uint less; uint more;
     require less < more;
 
     // stake less
-    stake(e, less) at initial;
+    currentStorage = initial;
+    stake(e, less);
     earnings_less = earnings(e);
 
     // stake more
-    stake(e, more) at initial;
+    currentStorage = initial;
+    stake(e, more);
     earnings_more = earnings(e);
 
     assert earnings_less < earnings_more, "if you stake more, you earn more";
 }
 ```
 
-The `lastStorage` variable contains the state of the EVM after the most recent
+The `currentStorage` variable contains the state of the EVM after the most recent
 contract function call.
 
+```{deprecated} 5.0
+`lastStorage` is a deprecated synonym for `currentStorage`.
+```
+
+````{deprecated} 5.0
+There is a deprecated syntax for first resetting the storage state and then
+calling a function.  If `f` is a contract function and `s` is a `storage`
+variable, you can write
+```cvl
+f() at s;
+```
+This syntax is shorthand for first assigning to `currentStorage` and then
+calling `f`.  The above example is equivalent to
+```cvl
+currentStorage = s;
+f();
+```
+
+You can only use this `at` syntax for contract functions; it is disallowed for
+other types of functions (such as CVL functions or definitions).
+````
+
 (sort)=
 ### Uninterpreted sorts
 

docs/prover/changelog.md

@@ -4,6 +4,12 @@ Release Notes
 ```{contents}
 ```
 
+Future
+------
+
+### CVL
+ - add syntax for resetting storage that is separate from method calls
+
 4.10.1 (August 21, 2023)
 ------------------------