From ec84089c2472d6cff68f18e083d5dc6826731992 Mon Sep 17 00:00:00 2001
From: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
Date: Wed, 13 Mar 2024 19:25:01 +0200
Subject: [PATCH] hook on length

---
 .../EnumerableSet/certora/spec/set.spec                   | 8 +++-----
 .../Structs/BankAccounts/certora/specs/structs.spec       | 6 ++----
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
index 25bff479..554a8d8b 100644
--- a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
+++ b/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] {
diff --git a/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec b/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec
index 08da5501..8a5f591e 100644
--- a/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec
+++ b/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; 
 }