Merge branch 'master' into update/certora-7.3.0

.github/workflows/formal-verification.yml

@@ -12,7 +12,7 @@ on:
 env:
   PIP_VERSION: '3.11'
   JAVA_VERSION: '11'
-  SOLC_VERSION: '0.8.20'
+  SOLC_VERSION: '0.8.25'
 
 concurrency: ${{ github.workflow }}-${{ github.ref }}
 

certora/harnesses/AccessManagedHarness.sol

@@ -10,27 +10,30 @@ contract AccessManagedHarness is AccessManaged {
 
     constructor(address initialAuthority) AccessManaged(initialAuthority) {}
 
-    function someFunction() public restricted() {
+    function someFunction() public restricted {
         // Sanity for FV: the msg.data when calling this function should be the same as the data used when checking
         // the schedule. This is a reformulation of `msg.data == SOME_FUNCTION_CALLDATA` that focuses on the operation
         // hash for this call.
         require(
-            IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data)
-            ==
-            IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA)
+            IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data) ==
+                IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA)
         );
     }
 
     function authority_canCall_immediate(address caller) public view returns (bool result) {
-        (result,) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+        (result, ) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
     }
 
     function authority_canCall_delay(address caller) public view returns (uint32 result) {
-        (,result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+        (, result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
     }
 
     function authority_getSchedule(address caller) public view returns (uint48) {
         IAccessManager manager = IAccessManager(authority());
         return manager.getSchedule(manager.hashOperation(caller, address(this), SOME_FUNCTION_CALLDATA));
     }
+
+    function _hasCode(address account) public view returns (bool) {
+        return account.code.length > 0;
+    }
 }

certora/specs/AccessManaged.spec

@@ -7,6 +7,10 @@ methods {
     function authority_canCall_immediate(address) external returns (bool);
     function authority_canCall_delay(address)     external returns (uint32);
     function authority_getSchedule(address)       external returns (uint48);
+    function _hasCode(address)                    external returns (bool) envfree;
+
+    // Summaries
+    function _.setAuthority(address)              external => DISPATCHER(true);
 }
 
 invariant isConsumingScheduledOpClean()
@@ -32,3 +36,25 @@ rule callRestrictedFunction(env e) {
         )
     );
 }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Only valid authorities can be set by the current authority                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule setAuthority(env e) {
+    require nonpayable(e);
+
+    address newAuthority;
+
+    address previousAuthority = authority();
+
+    setAuthority@withrevert(e, newAuthority);
+    bool success = !lastReverted;
+
+    assert success <=> (
+        previousAuthority == e.msg.sender &&
+        _hasCode(newAuthority)
+    );
+    assert success => newAuthority == authority();
+}

certora/specs/ERC20.spec

@@ -23,11 +23,11 @@ ghost mathint sumOfBalances {
 // overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an 
 // already used address (or upgraded from corrupted state).
 // We restrict such behavior by making sure no balance is greater than the sum of balances.
-hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+hook Sload uint256 balance _balances[KEY address addr] {
     require sumOfBalances >= to_mathint(balance);
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 

certora/specs/ERC721.spec

@@ -113,7 +113,7 @@ ghost mapping(address => mathint) _ownedByUser {
     init_state axiom forall address a. _ownedByUser[a] == 0;
 }
 
-hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
+hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
     _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
     _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
     _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
@@ -132,13 +132,13 @@ ghost mapping(address => mathint) _balances {
     init_state axiom forall address a. _balances[a] == 0;
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     _supply = _supply - oldValue + newValue;
 }
 
 // TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add
 // many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved.
-hook Sload uint256 value _balances[KEY address user] STORAGE {
+hook Sload uint256 value _balances[KEY address user] {
     require _balances[user] == to_mathint(value);
 }
 

requirements.txt

@@ -0,0 +1 @@
+certora-cli==7.3.0