update init axioms for some specs

Certora · Aug 12, 2024 · 4cd2bbb · 4cd2bbb
1 parent 19c989a
commit 4cd2bbb
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 14 deletions.
diff --git a/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec b/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec
@@ -18,9 +18,12 @@ ghost mapping(address => address) ghostPrev {
 ghost mapping(address => uint256) ghostValue {
     init_state axiom forall address x. ghostValue[x] == 0;
 }
-ghost address ghostHead;
-ghost address ghostTail;
-ghost uint256 ghostLength;
+ghost address ghostHead {
+    init_state axiom ghostHead == 0;
+}
+ghost address ghostTail {
+    init_state axiom ghostTail == 0;
+}
 ghost nextstar(address, address) returns bool {
     init_state axiom forall address x. forall address y. nextstar(x, y) == (x == y);
 }

diff --git a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
@@ -22,12 +22,13 @@ ghost mapping(bytes32 => uint256) ghostIndexes {
 }
 // ghost field for the length of the values array (stored in offset 0)
 ghost uint256 ghostLength {
+    init_state axiom ghostLength == 0;
     // assumption: it's infeasible to grow the list to these many elements.
     axiom ghostLength < max_uint256;
 }
 
 // HOOKS
-// Store hook to synchronize ghostLength with the length of the set._inner._values array. 
+// Store hook to synchronize ghostLength with the length of the set._inner._values array.
 hook Sstore currentContract.set._inner._values.length uint256 newLength {
     ghostLength = newLength;
 }
@@ -48,7 +49,7 @@ hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIn
 // By following this simple pattern it is ensured that the ghost state and the storage are always the same
 // 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. 
+// Load hook to synchronize ghostLength with the length of the set._inner._values array.
 hook Sload uint256 length currentContract.set._inner._values.length {
     require ghostLength == length;
 }
@@ -67,7 +68,7 @@ hook Sload uint256 index currentContract.set._inner._indexes[KEY bytes32 value]
 
 invariant setInvariant()
     (forall uint256 index. 0 <= index && index < ghostLength => to_mathint(ghostIndexes[ghostValues[index]]) == index + 1)
-    && (forall bytes32 value. ghostIndexes[value] == 0 || 
+    && (forall bytes32 value. ghostIndexes[value] == 0 ||
          (ghostValues[ghostIndexes[value] - 1] == value && ghostIndexes[value] >= 1 && ghostIndexes[value] <= ghostLength));
 
 // DEFINITION

diff --git a/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec b/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec
@@ -29,25 +29,27 @@ ghost mapping(bytes32 => bytes32) ghostSucc {
 }
 
 // Our ghost copy of the list head.
-ghost bytes32 ghostHead;
+ghost bytes32 ghostHead {
+    init_state axiom ghostHead == to_bytes32(0);
+}
 
 definition isSucc(bytes32 a, bytes32 b) returns bool = reach(a, b) && a != b && (forall bytes32 X. reach(a, X) && reach(X, b) => (a == X || b == X));
 
 definition reachSuccInvariant(bytes32 key) returns bool =
     (key == to_bytes32(0) && ghostSucc[key] == to_bytes32(0))
     || (key != to_bytes32(0) && isSucc(key, ghostSucc[key]));
 
-definition updateSucc(bytes32 a, bytes32 b) returns bool = forall bytes32 X. forall bytes32 Y. reach@new(X, Y) == 
+definition updateSucc(bytes32 a, bytes32 b) returns bool = forall bytes32 X. forall bytes32 Y. reach@new(X, Y) ==
             (X == Y ||
             (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 {
     bytes32 otherKey;
-    
+
     require reachSuccInvariant(otherKey);
     assert !reach(newNextKey,key), "Setting next introduces cycle";
-    
+
     // update ghost successor
     ghostSucc[key] = newNextKey;
     // update ghost reachability
@@ -87,21 +89,21 @@ invariant inListIffValid()
     }
 
 invariant reach_invariant()
-    forall bytes32 X. forall bytes32 Y. forall bytes32 Z. ( 
+    forall bytes32 X. forall bytes32 Y. forall bytes32 Z. (
         reach(X, X)
         && (reach(X,Y) && reach (Y, X) => X == Y)
         && (reach(X,Y) && reach (Y, Z) => reach(X, Z))
         && (reach(X,Y) && reach (X, Z) => (reach(Y,Z) || reach(Z,Y)))
     )
-    { 
+    {
         preserved {
             requireInvariant inListIffValid();
         }
     }
 
 invariant reach_succ(bytes32 key)
     reachSuccInvariant(key)
-    { 
+    {
         preserved {
             requireInvariant reach_invariant();
             requireInvariant inListIffValid();
@@ -191,4 +193,4 @@ rule checkInsertSucceedsOtherwise {
 
     insertAfter@withrevert(key, afterKey);
     assert !lastReverted, "insert should not revert";
-}
+}