remove storage keyword

Author: nivcertora

CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec

@@ -30,37 +30,37 @@ ghost prevstar(address, address) returns bool {
 
 // HOOKS
 
-hook Sstore currentContract.dll.head address newHead STORAGE {
+hook Sstore currentContract.dll.head address newHead {
     ghostHead = newHead;
 }
-hook Sstore currentContract.dll.tail address newTail STORAGE {
+hook Sstore currentContract.dll.tail address newTail {
     ghostTail = newTail;
 }
 
-hook Sstore currentContract.dll.accounts[KEY address key].next address newNext STORAGE {
+hook Sstore currentContract.dll.accounts[KEY address key].next address newNext {
     ghostNext[key] = newNext;
 }
 
-hook Sstore currentContract.dll.accounts[KEY address key].prev address newPrev STORAGE {
+hook Sstore currentContract.dll.accounts[KEY address key].prev address newPrev {
     ghostPrev[key] = newPrev;
 }
-hook Sstore currentContract.dll.accounts[KEY address key].value uint256 newValue STORAGE {
+hook Sstore currentContract.dll.accounts[KEY address key].value uint256 newValue {
     ghostValue[key] = newValue;
 }
 
-hook Sload address head currentContract.dll.head STORAGE {
+hook Sload address head currentContract.dll.head {
     require ghostHead == head;
 }
-hook Sload address tail currentContract.dll.tail STORAGE {
+hook Sload address tail currentContract.dll.tail {
     require ghostTail == tail;
 }
-hook Sload address next currentContract.dll.accounts[KEY address key].next STORAGE {
+hook Sload address next currentContract.dll.accounts[KEY address key].next {
     require ghostNext[key] == next;
 }
-hook Sload address prev currentContract.dll.accounts[KEY address key].prev STORAGE {
+hook Sload address prev currentContract.dll.accounts[KEY address key].prev {
     require ghostPrev[key] == prev;
 }
-hook Sload uint256 value currentContract.dll.accounts[KEY address key].value STORAGE {
+hook Sload uint256 value currentContract.dll.accounts[KEY address key].value {
     require ghostValue[key] == value;
 }
 

CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec

@@ -29,15 +29,15 @@ ghost uint256 ghostLength {
 // HOOKS
 // Store hook to synchronize ghostLength with the length of the set._inner._values array. 
 // We need to use (offset 0) here, as there is no keyword yet to access the length.
-hook Sstore currentContract.set.(offset 0) uint256 newLength STORAGE {
+hook Sstore currentContract.set.(offset 0) uint256 newLength {
     ghostLength = newLength;
 }
 // Store hook to synchronize ghostValues array with set._inner._values.
-hook Sstore currentContract.set._inner._values[INDEX uint256 index] bytes32 newValue STORAGE {
+hook Sstore currentContract.set._inner._values[INDEX uint256 index] bytes32 newValue {
     ghostValues[index] = newValue;
 }
 // Store hook to synchronize ghostIndexes array with set._inner._indexes.
-hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIndex STORAGE {
+hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIndex {
     ghostIndexes[value] = newIndex;
 }
 
@@ -51,13 +51,13 @@ hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIn
 
 // Load hook to synchronize ghostLength with the length of the set._inner._values array. 
 // Again we use (offset 0) here, as there is no keyword yet to access the length.
-hook Sload uint256 length currentContract.set.(offset 0) STORAGE {
+hook Sload uint256 length currentContract.set.(offset 0) {
     require ghostLength == length;
 }
-hook Sload bytes32 value currentContract.set._inner._values[INDEX uint256 index] STORAGE {
+hook Sload bytes32 value currentContract.set._inner._values[INDEX uint256 index] {
     require ghostValues[index] == value;
 }
-hook Sload uint256 index currentContract.set._inner._indexes[KEY bytes32 value] STORAGE {
+hook Sload uint256 index currentContract.set._inner._indexes[KEY bytes32 value] {
     require ghostIndexes[value] == index;
 }
 

CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec

@@ -42,7 +42,7 @@ definition updateSucc(bytes32 a, bytes32 b) returns bool = forall bytes32 X. for
             (reach@old(X, Y) && !(reach@old(X, a) && a != Y && reach@old(a, Y))) ||
             (reach@old(X, a) && reach@old(b, Y)));
 
-hook Sstore currentContract.list.elements[KEY bytes32 key].nextKey bytes32 newNextKey STORAGE {
+hook Sstore currentContract.list.elements[KEY bytes32 key].nextKey bytes32 newNextKey {
     bytes32 otherKey;
     
     require reachSuccInvariant(otherKey);
@@ -56,24 +56,24 @@ hook Sstore currentContract.list.elements[KEY bytes32 key].nextKey bytes32 newNe
     assert reachSuccInvariant(otherKey), "Successor invariant not preserved";
 }
 
-hook Sstore currentContract.list.elements[KEY bytes32 key].valid uint256 value STORAGE {
+hook Sstore currentContract.list.elements[KEY bytes32 key].valid uint256 value {
     ghostValid[key] = value != 0;
 }
 
-hook Sstore currentContract.list.head bytes32 newHead STORAGE {
+hook Sstore currentContract.list.head bytes32 newHead {
     ghostHead = newHead;
 }
 
-hook Sload bytes32 nextKey currentContract.list.elements[KEY bytes32 key].nextKey STORAGE {
+hook Sload bytes32 nextKey currentContract.list.elements[KEY bytes32 key].nextKey {
     require ghostSucc[key] == nextKey;
     require reachSuccInvariant(key);
 }
 
-hook Sload bytes32 head currentContract.list.head STORAGE {
+hook Sload bytes32 head currentContract.list.head {
     require ghostHead == head;
 }
 
-hook Sload uint256 valueValid currentContract.list.elements[KEY bytes32 key].valid STORAGE {
+hook Sload uint256 valueValid currentContract.list.elements[KEY bytes32 key].valid {
     require valueValid != 0 <=> ghostValid[key];
 }
 

CVLByExample/Storage/certora/specs/storage.spec

@@ -128,7 +128,7 @@ ghost mapping(address => mathint) numOfOperations {
 }
 
 /// hook on a complex data structure, a mapping to a struct with a dynamic array
-hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) STORAGE {
+hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) {
     require  old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element  
     accountBalanceMirror[a][i] = new_value;
     numOfOperations[a] = old_value + 1;

CVLByExample/Structs/BankAccounts/certora/specs/structs.spec

@@ -123,7 +123,7 @@ ghost mapping(address => uint256) numOfAccounts {
 
 /// Store hook to synchronize numOfAccounts with the length of the customers[KEY address a].accounts array.
 /// We need to use (offset 32) here, as there is no keyword yet to access the length.
-hook Sstore _customers[KEY address user].(offset 32) uint256 newLength STORAGE {
+hook Sstore _customers[KEY address user].(offset 32) uint256 newLength {
     if (newLength > numOfAccounts[user])
         require accountBalanceMirror[user][require_uint256(newLength-1)] == 0 ;   
     numOfAccounts[user] = newLength;
@@ -138,19 +138,19 @@ invariant checkNumOfAccounts(address user)
 
 /// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances.
 /// (offset 32) is the location of the size of the mapping. It is used because the field `size` is not yet supported in cvl.  
-hook Sload uint256 length _customers[KEY address user].(offset 32) STORAGE {
+hook Sload uint256 length _customers[KEY address user].(offset 32) {
     require numOfAccounts[user] == length; 
 }
 
 /// hook on a complex data structure, a mapping to a struct with a dynamic array
-hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) STORAGE {
+hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) {
     require  old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element  
     sumBalances =  sumBalances + new_value - old_value ;
     accountBalanceMirror[a][i] = new_value;
 }
 
 /// Sload on a struct field.
-hook Sload uint256 value  _customers[KEY address a].accounts[INDEX uint256 i].accountBalance   STORAGE {
+hook Sload uint256 value  _customers[KEY address a].accounts[INDEX uint256 i].accountBalance   {
     // when balance load, safely assume it is less than the sum of all values
     require to_mathint(value) <= sumBalances;
     require to_mathint(i) <= to_mathint(numOfAccounts[a]-1);

DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec

@@ -238,7 +238,7 @@ ghost mathint sumBalances{
 /* here we state when and how the ghost is updated */
 hook Sstore _balances[KEY address a] uint256 new_balance
 // the old value that balances[a] holds before the store
-    (uint256 old_balance) STORAGE {
+    (uint256 old_balance) {
   sumBalances = sumBalances + new_balance - old_balance;
 }
 

DEFI/ERC20/certora/specs/ERC20Broken.spec

@@ -114,7 +114,7 @@ ghost mathint sum_of_balances {
     init_state axiom sum_of_balances == 0;
 }
 
-hook Sstore _balances[KEY address a] uint new_value (uint old_value) STORAGE {
+hook Sstore _balances[KEY address a] uint new_value (uint old_value) {
     // when balance changes, update ghost
     sum_of_balances = sum_of_balances + new_value - old_value;
 }

DEFI/ERC20/certora/specs/ERC20Fixed.spec

@@ -99,13 +99,13 @@ persistent ghost mathint sum_of_balances {
     init_state axiom sum_of_balances == 0;
 }
 
-hook Sstore _balances[KEY address a] uint new_value (uint old_value) STORAGE {
+hook Sstore _balances[KEY address a] uint new_value (uint old_value) {
     // when balance changes, update ghost
     sum_of_balances = sum_of_balances + new_value - old_value;
 }
 
 // This `sload` makes `sum_of_balances >= to_mathint(balance)` hold at the beginning of each rule.
-hook Sload uint256 balance _balances[KEY address a]  STORAGE {
+hook Sload uint256 balance _balances[KEY address a]  {
   require sum_of_balances >= to_mathint(balance);
 }
 

DEFI/ERC20/certora/specs/ERC20Full.spec

@@ -81,11 +81,11 @@ ghost mathint numberOfChangesOfBalances {
 // overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an 
 // already used address (or upgraded from corrupted state).
 // We restrict such behavior by making sure no balance is greater than the sum of balances.
-hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+hook Sload uint256 balance _balances[KEY address addr] {
     require sumOfBalances >= to_mathint(balance);
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     sumOfBalances = sumOfBalances - oldValue + newValue;
     numberOfChangesOfBalances = numberOfChangesOfBalances + 1;
 }

DEFI/Immutable/Immutable.spec

@@ -32,7 +32,7 @@ rule HavocProoved(env e){
 
 // ghost uint ghostUint256;
 
-// hook Sload uint256 _MY_UINT currentContract.MY_UINT STORAGE {
+// hook Sload uint256 _MY_UINT currentContract.MY_UINT {
 //     require ghostUint256 == _MY_UINT;
 // }