Merge branch 'main' of github.com:safe-global/safe-contracts into cer…

…tora/treshold-ownercount
safe-global · Jul 4, 2023 · b2006f7 · b2006f7
2 parents d2d87c3 + 325aa47
commit b2006f7
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
@@ -24,11 +24,15 @@ contract SafeHarness is Safe {
         return getGuard();
     }
 
+    function getNativeTokenBalance() public view returns (uint256) {
+        return address(this).balance;
+    }
+
     function getOwnersCount() public view returns (uint256) {
         return ownerCount;
     }
 
-    function getNativeTokenBalance() public view returns (uint256) {
-        return address(this).balance;
+    function getOwnersCountFromArray() public view returns (uint256) {
+        return getOwners().length;
     }
 }
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -10,6 +10,7 @@ methods {
     function getSafeGuard() external returns (address) envfree;
     function getNativeTokenBalance() external returns (uint256) envfree;
     function getOwnersCount() external returns (uint256) envfree;
+    function getOwnersCountFromArray() external returns (uint256) envfree;
 
     // optional
     function execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation) external returns (bool, bytes memory);
@@ -261,3 +262,12 @@ rule nativeTokenBalanceSpendingExecTransactionFromModuleReturnData(
     assert balanceAfter < balanceBefore => 
         to_mathint(balanceBefore - value) <= to_mathint(balanceAfter);
 }
+
+rule safeOwnerCountConsistency(method f) filtered {
+    f -> reachableOnly(f)
+} {
+    calldataarg args; env e;
+    f(e, args);
+
+    assert getOwnersCount() == getOwnersCountFromArray();
+}