Finish Ownable and Ownable2Step

certora/diff/access_Ownable.sol.patch

@@ -0,0 +1,11 @@
+--- access/Ownable.sol	2023-08-09 11:45:05
++++ access/Ownable.sol	2023-08-11 11:37:19
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {Context} from "../utils/Context.sol";
+ 

certora/diff/access_Ownable2Step.sol.patch

@@ -0,0 +1,11 @@
+--- access/Ownable2Step.sol	2023-08-09 11:45:05
++++ access/Ownable2Step.sol	2023-08-11 11:37:27
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (access/Ownable2Step.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {Ownable} from "./Ownable.sol";
+ 

certora/harnesses/Ownable2StepHarness.sol

@@ -1,9 +1,11 @@
 // SPDX-License-Identifier: MIT
 
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-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 {}
 }

certora/harnesses/OwnableHarness.sol

@@ -1,9 +1,11 @@
 // SPDX-License-Identifier: MIT
 
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-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 {}
 }

certora/specs/Ownable.spec

@@ -1,78 +1,77 @@
-import "helpers/helpers.spec"
-import "methods/IOwnable.spec"
-
-methods {
-    restricted()
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: transferOwnership changes ownership                                                           │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule transferOwnership(env e) {
-    require nonpayable(e);
-
-    address newOwner;
-    address current = owner();
-
-    transferOwnership@withrevert(e, newOwner);
-    bool success = !lastReverted;
-
-    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
-    assert success => owner() == newOwner, "current owner changed";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: renounceOwnership removes the owner                                                           │
-
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule renounceOwnership(env e) {
-    require nonpayable(e);
-
-    address current = owner();
-
-    renounceOwnership@withrevert(e);
-    bool success = !lastReverted;
-
-    assert success <=> e.msg.sender == current, "unauthorized caller";
-    assert success => owner() == 0, "owner not cleared";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Access control: only current owner can call restricted functions                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
-    require nonpayable(e);
-
-    address current = owner();
-
-    calldataarg args;
-    restricted@withrevert(e, args);
-
-    assert !lastReverted <=> e.msg.sender == current, "access control failed";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: ownership can only change in specific ways                                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
-    address oldCurrent = owner();
-
-    method f; calldataarg args;
-    f(e, args);
-
-    address newCurrent = owner();
-
-    // If owner changes, must be either transferOwnership or renounceOwnership
-    assert oldCurrent != newCurrent => (
-        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) ||
-        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector)
-    );
-}
+import "helpers/helpers.spec";
+import "methods/IOwnable.spec";
+
+methods {
+    function restricted() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership changes ownership                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
+    assert success => owner() == newOwner, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership can only change in specific ways                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
+    address oldCurrent = owner();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+
+    // If owner changes, must be either transferOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+}

certora/specs/Ownable2Step.spec

@@ -1,108 +1,108 @@
-import "helpers/helpers.spec"
-import "methods/IOwnable2Step.spec"
-
-methods {
-    restricted()
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: transferOwnership sets the pending owner                                                      │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule transferOwnership(env e) {
-    require nonpayable(e);
-
-    address newOwner;
-    address current = owner();
-
-    transferOwnership@withrevert(e, newOwner);
-    bool success = !lastReverted;
-
-    assert success <=> e.msg.sender == current, "unauthorized caller";
-    assert success => pendingOwner() == newOwner, "pending owner not set";
-    assert success => owner() == current, "current owner changed";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: renounceOwnership removes the owner and the pendingOwner                                      │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule renounceOwnership(env e) {
-    require nonpayable(e);
-
-    address current = owner();
-
-    renounceOwnership@withrevert(e);
-    bool success = !lastReverted;
-
-    assert success <=> e.msg.sender == current, "unauthorized caller";
-    assert success => pendingOwner() == 0, "pending owner not cleared";
-    assert success => owner() == 0, "owner not cleared";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: acceptOwnership changes owner and reset pending owner                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule acceptOwnership(env e) {
-
-    require nonpayable(e);
-
-    address current = owner();
-    address pending = pendingOwner();
-
-    acceptOwnership@withrevert(e);
-    bool success = !lastReverted;
-
-    assert success <=> e.msg.sender == pending, "unauthorized caller";
-    assert success => pendingOwner() == 0, "pending owner not cleared";
-    assert success => owner() == pending, "owner not transferred";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Access control: only current owner can call restricted functions                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
-    require nonpayable(e);
-
-    address current = owner();
-
-    calldataarg args;
-    restricted@withrevert(e, args);
-
-    assert !lastReverted <=> e.msg.sender == current, "access control failed";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rule: ownership and pending ownership can only change in specific ways                                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule ownerOrPendingOwnerChange(env e, method f) {
-    address oldCurrent = owner();
-    address oldPending = pendingOwner();
-
-    calldataarg args;
-    f(e, args);
-
-    address newCurrent = owner();
-    address newPending = pendingOwner();
-
-    // If owner changes, must be either acceptOwnership or renounceOwnership
-    assert oldCurrent != newCurrent => (
-        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
-        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
-    );
-
-    // If pending changes, must be either acceptance or reset
-    assert oldPending != newPending => (
-        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == transferOwnership(address).selector) ||
-        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
-        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
-    );
-}
+import "helpers/helpers.spec";
+import "methods/IOwnable2Step.spec";
+
+methods {
+    function restricted() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership sets the pending owner                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == newOwner, "pending owner not set";
+    assert success => owner() == current, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner and the pendingOwner                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: acceptOwnership changes owner and reset pending owner                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule acceptOwnership(env e) {
+
+    require nonpayable(e);
+
+    address current = owner();
+    address pending = pendingOwner();
+
+    acceptOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == pending, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == pending, "owner not transferred";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership and pending ownership can only change in specific ways                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule ownerOrPendingOwnerChange(env e, method f) {
+    address oldCurrent = owner();
+    address oldPending = pendingOwner();
+
+    calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+    address newPending = pendingOwner();
+
+    // If owner changes, must be either acceptOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == sig:acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+
+    // If pending changes, must be either acceptance or reset
+    assert oldPending != newPending => (
+        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == sig:transferOwnership(address).selector) ||
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == sig:acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == sig:renounceOwnership().selector)
+    );
+}

certora/specs/methods/IOwnable.spec

@@ -1,5 +1,5 @@
 methods {
-    owner() returns (address) envfree
-    transferOwnership(address)
-    renounceOwnership()
+    function owner() external returns (address) envfree;
+    function transferOwnership(address) external;
+    function renounceOwnership() external;
 }

certora/specs/methods/IOwnable2Step.spec

@@ -1,7 +1,7 @@
 methods {
-    owner() returns (address) envfree
-    pendingOwner() returns (address) envfree
-    transferOwnership(address)
-    acceptOwnership()
-    renounceOwnership()
+    function owner() external returns (address) envfree;
+    function pendingOwner() external returns (address) envfree;
+    function transferOwnership(address) external;
+    function acceptOwnership() external;
+    function renounceOwnership() external;
 }