some fixes

Amxx · Amxx · commit 231e5d82e662 · 2025-08-18T16:52:01.000+02:00
diff --git a/certora/specs/AccessControl.conf b/certora/specs/AccessControl.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/AccessControlHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "AccessControlHarness:certora/specs/AccessControl.spec"
 }
diff --git a/certora/specs/AccessControlDefaultAdminRules.conf b/certora/specs/AccessControlDefaultAdminRules.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec"
 }
diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec
@@ -70,8 +70,11 @@ invariant defaultAdminRoleAdminConsistency()
 │ Invariant: owner is the defaultAdmin                                                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant ownerConsistency()
+// Writting this as an invariant would be flagged by Certora as trivial. Writting it as a rule is just as valid: we
+// verify the is true for any state of the storage
+rule ownerConsistency() {
   defaultAdmin() == owner();
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
diff --git a/certora/specs/AccessManaged.conf b/certora/specs/AccessManaged.conf
@@ -9,5 +9,6 @@
     "optimistic_hashing": true,
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "AccessManagedHarness:certora/specs/AccessManaged.spec"
 }
diff --git a/certora/specs/AccessManager.conf b/certora/specs/AccessManager.conf
@@ -5,5 +5,6 @@
     "optimistic_hashing": true,
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "AccessManagerHarness:certora/specs/AccessManager.spec"
 }
diff --git a/certora/specs/Account.conf b/certora/specs/Account.conf
diff --git a/certora/specs/DoubleEndedQueue.conf b/certora/specs/DoubleEndedQueue.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/DoubleEndedQueueHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "DoubleEndedQueueHarness:certora/specs/DoubleEndedQueue.spec"
 }
diff --git a/certora/specs/DoubleEndedQueue.spec b/certora/specs/DoubleEndedQueue.spec
@@ -26,22 +26,22 @@ definition full() returns bool = length() == max_uint128;
 │ Invariant: empty() is length 0 and no element exists                                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant emptiness()
-    empty() <=> length() == 0
-    filtered { f -> !f.isView }
+rule emptiness() {
+    assert empty() <=> length() == 0;
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Invariant: front points to the first index and back points to the last one                                          │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant queueFront()
-    at_(0) == front()
-    filtered { f -> !f.isView }
+rule queueFront() {
+    assert at_(0) == front();
+}
 
-invariant queueBack()
-    at_(require_uint256(length() - 1)) == back()
-    filtered { f -> !f.isView }
+rule queueBack() {
+    assert at_(require_uint256(length() - 1)) == back();
+}
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
diff --git a/certora/specs/ERC20.conf b/certora/specs/ERC20.conf
@@ -4,5 +4,6 @@
     ],
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "ERC20PermitHarness:certora/specs/ERC20.spec"
 }
diff --git a/certora/specs/ERC20FlashMint.conf b/certora/specs/ERC20FlashMint.conf
@@ -5,5 +5,6 @@
     ],
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec"
 }
diff --git a/certora/specs/ERC20Wrapper.conf b/certora/specs/ERC20Wrapper.conf
@@ -8,5 +8,6 @@
     ],
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec"
 }
diff --git a/certora/specs/ERC721.conf b/certora/specs/ERC721.conf
@@ -5,5 +5,6 @@
     ],
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "ERC721Harness:certora/specs/ERC721.spec"
 }
diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec
@@ -24,7 +24,7 @@ definition authSanity(env e) returns bool = e.msg.sender != 0;
 // Could be broken in theory, but not in practice
 definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
 
-function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
+function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) returns bool {
     if (f.selector == sig:transferFrom(address,address,uint256).selector) {
         transferFrom@withrevert(e, from, to, tokenId);
     } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
@@ -37,9 +37,10 @@ function helperTransferWithRevert(env e, method f, address from, address to, uin
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
-function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
+function helperMintWithRevert(env e, method f, address to, uint256 tokenId) returns bool {
     if (f.selector == sig:mint(address,uint256).selector) {
         mint@withrevert(e, to, tokenId);
     } else if (f.selector == sig:safeMint(address,uint256).selector) {
@@ -51,6 +52,7 @@ function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
     } else {
         require false;
     }
+    return !lastReverted;
 }
 
 function helperSoundFnCall(env e, method f) {
@@ -466,8 +468,7 @@ rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId
     address approvalBefore       = unsafeGetApproved(tokenId);
     address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
 
-    helperTransferWithRevert(e, f, from, to, tokenId);
-    bool success = !lastReverted;
+    bool success = helperTransferWithRevert(e, f, from, to, tokenId);
 
     assert success <=> (
         from == ownerBefore &&
@@ -554,8 +555,7 @@ rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
     address ownerBefore          = unsafeOwnerOf(tokenId);
     address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
 
-    helperMintWithRevert(e, f, to, tokenId);
-    bool success = !lastReverted;
+    bool success = helperMintWithRevert(e, f, to, tokenId);
 
     assert success <=> (
         ownerBefore == 0 &&
diff --git a/certora/specs/EnumerableMap.conf b/certora/specs/EnumerableMap.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/EnumerableMapHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "EnumerableMapHarness:certora/specs/EnumerableMap.spec"
 }
diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec
@@ -75,19 +75,15 @@ invariant atUniqueness(uint256 index1, uint256 index2)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant consistencyIndex(uint256 index)
-    index < length() => to_mathint(_positionOf(key_at(index))) == index + 1
+    index < length() <=> to_mathint(_positionOf(key_at(index))) == index + 1
     {
         preserved remove(bytes32 key) {
             requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
 invariant consistencyKey(bytes32 key)
-    contains(key) => (
-        _positionOf(key) > 0 &&
-        _positionOf(key) <= length() &&
-        key_at(require_uint256(_positionOf(key) - 1)) == key
-    )
+    (contains(key) <=> key_at(require_uint256(_positionOf(key) - 1)) == key) && _positionOf(key) <= length()
     {
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
diff --git a/certora/specs/EnumerableSet.conf b/certora/specs/EnumerableSet.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/EnumerableSetHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "EnumerableSetHarness:certora/specs/EnumerableSet.spec"
 }
diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec
@@ -58,19 +58,15 @@ invariant atUniqueness(uint256 index1, uint256 index2)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant consistencyIndex(uint256 index)
-    index < length() => _positionOf(at_(index)) == require_uint256(index + 1)
+    index < length() <=> _positionOf(at_(index)) == require_uint256(index + 1)
     {
         preserved remove(bytes32 key) {
             requireInvariant consistencyIndex(require_uint256(length() - 1));
         }
     }
 
 invariant consistencyKey(bytes32 key)
-    contains(key) => (
-        _positionOf(key) > 0 &&
-        _positionOf(key) <= length() &&
-        at_(require_uint256(_positionOf(key) - 1)) == key
-    )
+    (contains(key) <=> at_(require_uint256(_positionOf(key) - 1)) == key) && _positionOf(key) <= length()
     {
         preserved remove(bytes32 otherKey) {
             requireInvariant consistencyKey(otherKey);
diff --git a/certora/specs/Initializable.conf b/certora/specs/Initializable.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/InitializableHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "InitializableHarness:certora/specs/Initializable.spec"
 }
diff --git a/certora/specs/Nonces.conf b/certora/specs/Nonces.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/NoncesHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "NoncesHarness:certora/specs/Nonces.spec"
 }
diff --git a/certora/specs/Ownable.conf b/certora/specs/Ownable.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/OwnableHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "OwnableHarness:certora/specs/Ownable.spec"
 }
diff --git a/certora/specs/Ownable2Step.conf b/certora/specs/Ownable2Step.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/Ownable2StepHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "Ownable2StepHarness:certora/specs/Ownable2Step.spec"
 }
diff --git a/certora/specs/Pausable.conf b/certora/specs/Pausable.conf
@@ -3,5 +3,6 @@
         "certora/harnesses/PausableHarness.sol"
     ],
     "process": "emv",
+    "url_visibility": "public",
     "verify": "PausableHarness:certora/specs/Pausable.spec"
 }
diff --git a/certora/specs/TimelockController.conf b/certora/specs/TimelockController.conf
@@ -5,5 +5,6 @@
     "optimistic_hashing": true,
     "optimistic_loop": true,
     "process": "emv",
+    "url_visibility": "public",
     "verify": "TimelockControllerHarness:certora/specs/TimelockController.spec"
 }
diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec
@@ -30,7 +30,7 @@ methods {
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 // Uniformly handle scheduling of batched and non-batched operations.
-function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
+function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) returns bool {
     if (f.selector == sig:schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) {
         address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
@@ -43,10 +43,11 @@ function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) {
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
 // Uniformly handle execution of batched and non-batched operations.
-function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) {
+function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) returns bool {
     if (f.selector == sig:execute(address, uint256, bytes, bytes32, bytes32).selector) {
         address target; uint256 value; bytes data; bytes32 salt;
         require hashOperation(target, value, data, predecessor, salt) == id; // Correlation
@@ -59,6 +60,7 @@ function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecesso
         calldataarg args;
         f@withrevert(e, args);
     }
+    return !lastReverted;
 }
 
 /*
@@ -187,8 +189,7 @@ rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f ->
     bool  isDelaySufficient = delay >= getMinDelay();
     bool  isProposerBefore  = hasRole(PROPOSER_ROLE(), e.msg.sender);
 
-    helperScheduleWithRevert(e, f, id, delay);
-    bool success = !lastReverted;
+    bool success = helperScheduleWithRevert(e, f, id, delay);
 
     // liveness
     assert success <=> (
@@ -221,8 +222,7 @@ rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f ->
     bool  isExecutorOrOpen       = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0);
     bool  predecessorDependency  = predecessor == to_bytes32(0) || isDone(e, predecessor);
 
-    helperExecuteWithRevert(e, f, id, predecessor);
-    bool success = !lastReverted;
+    bool success = helperExecuteWithRevert(e, f, id, predecessor);
 
     // The underlying transaction can revert, and that would cause the execution to revert. We can check that all non
     // reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency.

Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,6 @@`
`3`	`3`	`"certora/harnesses/AccessControlHarness.sol"`
`4`	`4`	`],`
`5`	`5`	`"process": "emv",`
	`6`	`+ "url_visibility": "public",`
`6`	`7`	`"verify": "AccessControlHarness:certora/specs/AccessControl.spec"`
`7`	`8`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,6 @@`
`3`	`3`	`"certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"`
`4`	`4`	`],`
`5`	`5`	`"process": "emv",`
	`6`	`+ "url_visibility": "public",`
`6`	`7`	`"verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec"`
`7`	`8`	`}`
Original file line number	Diff line number	Diff line change
`@@ -9,5 +9,6 @@`
`9`	`9`	`"optimistic_hashing": true,`
`10`	`10`	`"optimistic_loop": true,`
`11`	`11`	`"process": "emv",`
	`12`	`+ "url_visibility": "public",`
`12`	`13`	`"verify": "AccessManagedHarness:certora/specs/AccessManaged.spec"`
`13`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -5,5 +5,6 @@`
`5`	`5`	`"optimistic_hashing": true,`
`6`	`6`	`"optimistic_loop": true,`
`7`	`7`	`"process": "emv",`
	`8`	`+ "url_visibility": "public",`
`8`	`9`	`"verify": "AccessManagerHarness:certora/specs/AccessManager.spec"`
`9`	`10`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,6 @@`
`3`	`3`	`"certora/harnesses/DoubleEndedQueueHarness.sol"`
`4`	`4`	`],`
`5`	`5`	`"process": "emv",`
	`6`	`+ "url_visibility": "public",`
`6`	`7`	`"verify": "DoubleEndedQueueHarness:certora/specs/DoubleEndedQueue.spec"`
`7`	`8`	`}`
Original file line number	Diff line number	Diff line change
`@@ -4,5 +4,6 @@`
`4`	`4`	`],`
`5`	`5`	`"optimistic_loop": true,`
`6`	`6`	`"process": "emv",`
	`7`	`+ "url_visibility": "public",`
`7`	`8`	`"verify": "ERC20PermitHarness:certora/specs/ERC20.spec"`
`8`	`9`	`}`