From 76a0d1d2494323f24427c89370f21e56277341bf Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 11 Jul 2024 13:10:38 +0200
Subject: [PATCH] feat: emptyZero

---
 certora/specs/DllFifo.spec   | 4 ++++
 certora/specs/DllSimple.spec | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec
index c8498bd..fd1f605 100644
--- 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
index 175aeb0..c560d07 100644
--- 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) {