Merge branch 'liav/CERT-5336-V7-Examples' of https://github.com/Certo…

…ra/Examples into liav/CERT-5336-V7-Examples

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

@@ -23,13 +23,12 @@ ghost mapping(bytes32 => uint256) ghostIndexes {
 // ghost field for the length of the values array (stored in offset 0)
 ghost uint256 ghostLength {
     // assumption: it's infeasible to grow the list to these many elements.
-    axiom ghostLength < 0xffffffffffffffffffffffffffffffff;
+    axiom ghostLength < max_uint256;
 }
 
 // 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 {
+hook Sstore currentContract.set._inner._values.length uint256 newLength {
     ghostLength = newLength;
 }
 // Store hook to synchronize ghostValues array with set._inner._values.
@@ -50,8 +49,7 @@ hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIn
 // and that the solver can use this knowledge in the proofs.
 
 // 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) {
+hook Sload uint256 length currentContract.set._inner._values.length {
     require ghostLength == length;
 }
 hook Sload bytes32 value currentContract.set._inner._values[INDEX uint256 index] {

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

@@ -122,8 +122,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 {
+hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
     if (newLength > numOfAccounts[user])
         require accountBalanceMirror[user][require_uint256(newLength-1)] == 0 ;   
     numOfAccounts[user] = newLength;
@@ -137,8 +136,7 @@ invariant checkNumOfAccounts(address user)
     numOfAccounts[user] == bank.getNumberOfAccounts(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) {
+hook Sload uint256 length _customers[KEY address user].accounts.length {
     require numOfAccounts[user] == length; 
 }