Add an invariant for singleton address

certora/specs/Safe.spec

@@ -22,6 +22,7 @@ definition reachableOnly(method f) returns bool =
     f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector
     && f.selector != sig:simulateAndRevert(address,bytes).selector;
 
+
 /// Nonce must never decrease
 rule nonceMonotonicity(method f) filtered {
     f -> noHavoc(f) && reachableOnly(f)
@@ -81,4 +82,22 @@ invariant noDeadEnds(address dead, address lost)
             requireInvariant noDeadEnds(dead, module);
             requireInvariant noDeadEnds(module, dead);
         }
-    }
+    }
+
+
+// The singleton is a private variable, so we need to use a ghost variable to track it.
+ghost address ghostSingletonAddress {
+    init_state axiom ghostSingletonAddress == 0;
+}
+
+hook Sstore SafeHarness.(slot 0) address newSingletonAddress STORAGE {
+    ghostSingletonAddress = newSingletonAddress;
+}
+
+hook Sstore SafeHarness.(slot 24440054405305269366569402256811496959409073762505157381672968839269610695612) address newSingletonAddress STORAGE {
+    ghostSingletonAddress = newSingletonAddress;
+}
+
+invariant sigletonAddressNeverChanges()
+    ghostSingletonAddress == 0
+    filtered { f ->  reachableOnly(f) }