Migrate FV specs to CVL2 (#4527)

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
OpenZeppelin · Sep 11, 2023 · 36bf1e4 · 36bf1e4
1 parent b6111fa
commit 36bf1e4
Show file tree

Hide file tree

Showing 42 changed files with 1,002 additions and 907 deletions.
diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch
diff --git a/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol b/certora/harnesses/AccessControlDefaultAdminRulesHarness.sol
@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/AccessControlDefaultAdminRules.sol";
+import {AccessControlDefaultAdminRules} from "../patched/access/extensions/AccessControlDefaultAdminRules.sol";
 
 contract AccessControlDefaultAdminRulesHarness is AccessControlDefaultAdminRules {
     uint48 private _delayIncreaseWait;

diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol
@@ -1,7 +1,6 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/AccessControl.sol";
+import {AccessControl} from "../patched/access/AccessControl.sol";
 
 contract AccessControlHarness is AccessControl {}
diff --git a/certora/harnesses/DoubleEndedQueueHarness.sol b/certora/harnesses/DoubleEndedQueueHarness.sol
@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/DoubleEndedQueue.sol";
+import {DoubleEndedQueue} from "../patched/utils/structs/DoubleEndedQueue.sol";
 
 contract DoubleEndedQueueHarness {
     using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque;

diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol
@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import {ERC20Permit, ERC20} from "../patched/token/ERC20/extensions/ERC20Permit.sol";
 
 contract ERC20PermitHarness is ERC20Permit {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}

diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol
@@ -2,10 +2,15 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
+import {ERC20Permit} from "../patched/token/ERC20/extensions/ERC20Permit.sol";
+import {ERC20Wrapper, IERC20, ERC20} from "../patched/token/ERC20/extensions/ERC20Wrapper.sol";
 
-contract ERC20WrapperHarness is ERC20Wrapper {
-    constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {}
+contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper {
+    constructor(
+        IERC20 _underlying,
+        string memory _name,
+        string memory _symbol
+    ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {}
 
     function underlyingTotalSupply() public view returns (uint256) {
         return underlying().totalSupply();
@@ -22,4 +27,8 @@ contract ERC20WrapperHarness is ERC20Wrapper {
     function recover(address account) public returns (uint256) {
         return _recover(account);
     }
+
+    function decimals() public view override(ERC20Wrapper, ERC20) returns (uint8) {
+        return super.decimals();
+    }
 }
diff --git a/certora/harnesses/ERC3156FlashBorrowerHarness.sol b/certora/harnesses/ERC3156FlashBorrowerHarness.sol
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: MIT
 
-import "../patched/interfaces/IERC3156FlashBorrower.sol";
+import {IERC3156FlashBorrower} from "../patched/interfaces/IERC3156FlashBorrower.sol";
 
 pragma solidity ^0.8.20;
 

diff --git a/certora/harnesses/ERC721Harness.sol b/certora/harnesses/ERC721Harness.sol
@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/token/ERC721/ERC721.sol";
+import {ERC721} from "../patched/token/ERC721/ERC721.sol";
 
 contract ERC721Harness is ERC721 {
     constructor(string memory name, string memory symbol) ERC721(name, symbol) {}
@@ -23,10 +23,6 @@ contract ERC721Harness is ERC721 {
         _burn(tokenId);
     }
 
-    function tokenExists(uint256 tokenId) external view returns (bool) {
-        return _exists(tokenId);
-    }
-
     function unsafeOwnerOf(uint256 tokenId) external view returns (address) {
         return _ownerOf(tokenId);
     }

diff --git a/certora/harnesses/EnumerableMapHarness.sol b/certora/harnesses/EnumerableMapHarness.sol
@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/EnumerableMap.sol";
+import {EnumerableMap} from "../patched/utils/structs/EnumerableMap.sol";
 
 contract EnumerableMapHarness {
     using EnumerableMap for EnumerableMap.Bytes32ToBytes32Map;

diff --git a/certora/harnesses/EnumerableSetHarness.sol b/certora/harnesses/EnumerableSetHarness.sol
@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.20;
 
-import "../patched/utils/structs/EnumerableSet.sol";
+import {EnumerableSet} from "../patched/utils/structs/EnumerableSet.sol";
 
 contract EnumerableSetHarness {
     using EnumerableSet for EnumerableSet.Bytes32Set;

diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol
@@ -1,19 +1,19 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.20;
 
-import "../patched/proxy/utils/Initializable.sol";
+import {Initializable} from "../patched/proxy/utils/Initializable.sol";
 
 contract InitializableHarness is Initializable {
-    function initialize()          public initializer      {}
-    function reinitialize(uint8 n) public reinitializer(n) {}
-    function disable()             public { _disableInitializers(); }
+    function initialize()           public initializer      {}
+    function reinitialize(uint64 n) public reinitializer(n) {}
+    function disable()              public { _disableInitializers(); }
 
-    function nested_init_init()                     public initializer      { initialize();    }
-    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
-    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
-    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
+    function nested_init_init()                       public initializer      { initialize();    }
+    function nested_init_reinit(uint64 m)             public initializer      { reinitialize(m); }
+    function nested_reinit_init(uint64 n)             public reinitializer(n) { initialize();    }
+    function nested_reinit_reinit(uint64 n, uint64 m) public reinitializer(n) { reinitialize(m); }
 
-    function version() public view returns (uint8) {
+    function version() public view returns (uint64) {
         return _getInitializedVersion();
     }
 

diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol
@@ -1,9 +1,10 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/Ownable2Step.sol";
+import {Ownable2Step, Ownable} from "../patched/access/Ownable2Step.sol";
 
 contract Ownable2StepHarness is Ownable2Step {
-  function restricted() external onlyOwner {}
+    constructor(address initialOwner) Ownable(initialOwner) {}
+
+    function restricted() external onlyOwner {}
 }
diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol
@@ -1,9 +1,10 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/access/Ownable.sol";
+import {Ownable} from "../patched/access/Ownable.sol";
 
 contract OwnableHarness is Ownable {
-  function restricted() external onlyOwner {}
+    constructor(address initialOwner) Ownable(initialOwner) {}
+
+    function restricted() external onlyOwner {}
 }
diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol
@@ -1,8 +1,7 @@
 // SPDX-License-Identifier: MIT
-
 pragma solidity ^0.8.20;
 
-import "../patched/utils/Pausable.sol";
+import {Pausable} from "../patched/utils/Pausable.sol";
 
 contract PausableHarness is Pausable {
     function pause() external {

diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol
@@ -1,6 +1,7 @@
+// SPDX-License-Identifier: MIT
 pragma solidity ^0.8.20;
 
-import "../patched/governance/TimelockController.sol";
+import {TimelockController} from "../patched/governance/TimelockController.sol";
 
 contract TimelockControllerHarness is TimelockController {
     constructor(

diff --git a/certora/run.js b/certora/run.js
@@ -64,7 +64,13 @@ if (process.exitCode) {
 }
 
 for (const { spec, contract, files, options = [] } of specs) {
-  limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...argv.options]);
+  limit(
+    runCertora,
+    spec,
+    contract,
+    files,
+    [...options, ...argv.options].flatMap(opt => opt.split(' ')),
+  );
 }
 
 // Run certora, aggregate the output and print it at the end