feat: emptyZero

morpho-org · Jul 11, 2024 · 76a0d1d · 76a0d1d
1 parent 26ef413
commit 76a0d1d
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec
@@ -51,6 +51,7 @@ definition hasNoNextIsTail(address addr) returns bool =
     isInDll(addr) && getNext(addr) == 0 => addr == getTail();
 
 function safeAssumptions() {
+    requireInvariant emptyZero();
     requireInvariant emptyEquiv();
     requireInvariant headWellFormed();
     requireInvariant tailWellFormed();
@@ -62,6 +63,9 @@ function safeAssumptions() {
 // or even all of the public functions (in that last case they are still relevant for proving
 // the property at initial state).
 
+invariant emptyZero()
+    ! isInDll(0);
+
 invariant emptyEquiv()
     isEmptyEquiv()
     { preserved remove(address id) {

diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec
@@ -57,6 +57,9 @@ function safeAssumptions() {
 // or even all of the public functions (in that last case they are still relevant for proving
 // the property at initial state).
 
+invariant emptyZero()
+    ! isInDll(0);
+
 invariant emptyEquiv()
     isEmptyEquiv()
     { preserved remove(address id) {