From aaad1f4a4ffdba7da789d93a28030e5c411f0181 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 8 Mar 2023 19:30:07 +0100 Subject: [PATCH 1/4] Add FV specs for Ownable and Ownable2Steps (#4094) Co-authored-by: Santiago Palladino Co-authored-by: Francisco --- certora/harnesses/Ownable2StepHarness.sol | 9 ++ certora/harnesses/OwnableHarness.sol | 9 ++ certora/run.js | 4 +- certora/specs.json | 10 ++ certora/specs/Ownable.spec | 78 ++++++++++++++++ certora/specs/Ownable2Step.spec | 108 ++++++++++++++++++++++ certora/specs/methods/IOwnable.spec | 5 + certora/specs/methods/IOwnable2Step.spec | 7 ++ 8 files changed, 228 insertions(+), 2 deletions(-) create mode 100644 certora/harnesses/Ownable2StepHarness.sol create mode 100644 certora/harnesses/OwnableHarness.sol create mode 100644 certora/specs/Ownable.spec create mode 100644 certora/specs/Ownable2Step.spec create mode 100644 certora/specs/methods/IOwnable.spec create mode 100644 certora/specs/methods/IOwnable2Step.spec diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol new file mode 100644 index 00000000000..4d30e504189 --- /dev/null +++ b/certora/harnesses/Ownable2StepHarness.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/access/Ownable2Step.sol"; + +contract Ownable2StepHarness is Ownable2Step { + function restricted() external onlyOwner {} +} diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol new file mode 100644 index 00000000000..93cbb4770c2 --- /dev/null +++ b/certora/harnesses/OwnableHarness.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/access/Ownable.sol"; + +contract OwnableHarness is Ownable { + function restricted() external onlyOwner {} +} diff --git a/certora/run.js b/certora/run.js index 1da238d4ff9..16146525874 100644 --- a/certora/run.js +++ b/certora/run.js @@ -64,7 +64,7 @@ async function runCertora(spec, contract, files, options = []) { stream.end(); // write results in markdown format - writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)[0]); + writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)?.[0]); // write all details console.error(`+ certoraRun ${args.join(' ')}\n` + (await output)); @@ -103,7 +103,7 @@ function writeEntry(spec, contract, success, url) { contract, success ? ':x:' : ':heavy_check_mark:', `[link](${url})`, - `[link](${url.replace('/jobStatus/', '/output/')})`, + `[link](${url?.replace('/jobStatus/', '/output/')})`, ), ); } diff --git a/certora/specs.json b/certora/specs.json index 4d3e1fb9005..c22b1ebba38 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -4,6 +4,16 @@ "contract": "AccessControlHarness", "files": ["certora/harnesses/AccessControlHarness.sol"] }, + { + "spec": "Ownable", + "contract": "OwnableHarness", + "files": ["certora/harnesses/OwnableHarness.sol"] + }, + { + "spec": "Ownable2Step", + "contract": "Ownable2StepHarness", + "files": ["certora/harnesses/Ownable2StepHarness.sol"] + }, { "spec": "ERC20", "contract": "ERC20PermitHarness", diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec new file mode 100644 index 00000000000..48bd84d13fc --- /dev/null +++ b/certora/specs/Ownable.spec @@ -0,0 +1,78 @@ +import "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, method f) { + address oldCurrent = owner(); + + 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) + ); +} diff --git a/certora/specs/Ownable2Step.spec b/certora/specs/Ownable2Step.spec new file mode 100644 index 00000000000..70c520a03f5 --- /dev/null +++ b/certora/specs/Ownable2Step.spec @@ -0,0 +1,108 @@ +import "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) + ); +} diff --git a/certora/specs/methods/IOwnable.spec b/certora/specs/methods/IOwnable.spec new file mode 100644 index 00000000000..cfa15f95ff1 --- /dev/null +++ b/certora/specs/methods/IOwnable.spec @@ -0,0 +1,5 @@ +methods { + owner() returns (address) envfree + transferOwnership(address) + renounceOwnership() +} diff --git a/certora/specs/methods/IOwnable2Step.spec b/certora/specs/methods/IOwnable2Step.spec new file mode 100644 index 00000000000..c8e671d272c --- /dev/null +++ b/certora/specs/methods/IOwnable2Step.spec @@ -0,0 +1,7 @@ +methods { + owner() returns (address) envfree + pendingOwner() returns (address) envfree + transferOwnership(address) + acceptOwnership() + renounceOwnership() +} From a55013e742d0673394192e3df36c58778f8d8a59 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 8 Mar 2023 19:31:46 +0100 Subject: [PATCH 2/4] Add effect checks on the accesscontrol specs (#4099) --- certora/specs/AccessControl.spec | 85 +++++++++++++++++++------------- 1 file changed, 50 insertions(+), 35 deletions(-) diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index 170d56fd403..8e8f6ac9d86 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -44,22 +44,27 @@ rule onlyGrantCanGrant(env e, bytes32 role, address account) { rule grantRoleEffect(env e) { require nonpayable(e); - bytes32 role1; bytes32 role2; - address account1; address account2; + bytes32 role; + bytes32 otherRole; + address account; + address otherAccount; - bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender); - bool hasRoleBefore = hasRole(role1, account1); + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - grantRole@withrevert(e, role2, account2); - assert !lastReverted <=> isCallerAdmin; + grantRole@withrevert(e, role, account); + bool success = !lastReverted; - bool hasRoleAfter = hasRole(role1, account1); + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - assert ( - hasRoleBefore != hasRoleAfter - ) => ( - hasRoleAfter == true && role1 == role2 && account1 == account2 - ); + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); } /* @@ -70,22 +75,27 @@ rule grantRoleEffect(env e) { rule revokeRoleEffect(env e) { require nonpayable(e); - bytes32 role1; bytes32 role2; - address account1; address account2; + bytes32 role; + bytes32 otherRole; + address account; + address otherAccount; - bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender); - bool hasRoleBefore = hasRole(role1, account1); + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - revokeRole@withrevert(e, role2, account2); - assert !lastReverted <=> isCallerAdmin; + revokeRole@withrevert(e, role, account); + bool success = !lastReverted; - bool hasRoleAfter = hasRole(role1, account1); + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - assert ( - hasRoleBefore != hasRoleAfter - ) => ( - hasRoleAfter == false && role1 == role2 && account1 == account2 - ); + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => !hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); } /* @@ -96,19 +106,24 @@ rule revokeRoleEffect(env e) { rule renounceRoleEffect(env e) { require nonpayable(e); - bytes32 role1; bytes32 role2; - address account1; address account2; + bytes32 role; + bytes32 otherRole; + address account; + address otherAccount; - bool hasRoleBefore = hasRole(role1, account1); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - renounceRole@withrevert(e, role2, account2); - assert !lastReverted <=> account2 == e.msg.sender; + renounceRole@withrevert(e, role, account); + bool success = !lastReverted; - bool hasRoleAfter = hasRole(role1, account1); + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - assert ( - hasRoleBefore != hasRoleAfter - ) => ( - hasRoleAfter == false && role1 == role2 && account1 == account2 - ); + // liveness + assert success <=> account == e.msg.sender; + + // effect + assert success => !hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); } From b952a82d29661995d75c476501f977b716860e58 Mon Sep 17 00:00:00 2001 From: Francisco Date: Wed, 8 Mar 2023 18:16:37 -0300 Subject: [PATCH 3/4] Throw error when requested specs are not found (#4101) --- certora/run.js | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/certora/run.js b/certora/run.js index 16146525874..172309e198c 100644 --- a/certora/run.js +++ b/certora/run.js @@ -8,7 +8,7 @@ const MAX_PARALLEL = 4; -const specs = require(__dirname + '/specs.json'); +let specs = require(__dirname + '/specs.json'); const proc = require('child_process'); const { PassThrough } = require('stream'); @@ -20,14 +20,20 @@ if (request.startsWith('-')) { extraOptions.unshift(request); request = ''; } -const [reqSpec, reqContract] = request.split(':').reverse(); -for (const { spec, contract, files, options = [] } of Object.values(specs)) { - if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) { - limit(runCertora, spec, contract, files, [...options, ...extraOptions]); +if (request) { + const [reqSpec, reqContract] = request.split(':').reverse(); + specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract)); + if (specs.length === 0) { + console.error(`Error: Requested spec '${request}' not found in specs.json`); + process.exit(1); } } +for (const { spec, contract, files, options = [] } of Object.values(specs)) { + limit(runCertora, spec, contract, files, [...options, ...extraOptions]); +} + // Run certora, aggregate the output and print it at the end async function runCertora(spec, contract, files, options = []) { const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; From 5f7f660c6e247cf0e91d87c6d64635908997f738 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 8 Mar 2023 22:17:35 +0100 Subject: [PATCH 4/4] Add FV specs for Initializable (#4095) Co-authored-by: Francisco --- certora/harnesses/InitializableHarness.sol | 23 +++ certora/specs.json | 5 + certora/specs/Initializable.spec | 165 +++++++++++++++++++++ 3 files changed, 193 insertions(+) create mode 100644 certora/harnesses/InitializableHarness.sol create mode 100644 certora/specs/Initializable.spec diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol new file mode 100644 index 00000000000..19437e0fc7e --- /dev/null +++ b/certora/harnesses/InitializableHarness.sol @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../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 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 version() public view returns (uint8) { + return _getInitializedVersion(); + } + + function initializing() public view returns (bool) { + return _isInitializing(); + } +} diff --git a/certora/specs.json b/certora/specs.json index c22b1ebba38..8e4fe21f4cc 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -28,5 +28,10 @@ "certora/harnesses/ERC3156FlashBorrowerHarness.sol" ], "options": ["--optimistic_loop"] + }, + { + "spec": "Initializable", + "contract": "InitializableHarness", + "files": ["certora/harnesses/InitializableHarness.sol"] } ] diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec new file mode 100644 index 00000000000..1ba8d54e81f --- /dev/null +++ b/certora/specs/Initializable.spec @@ -0,0 +1,165 @@ +import "helpers.spec" + +methods { + // initialize, reinitialize, disable + initialize() envfree + reinitialize(uint8) envfree + disable() envfree + + nested_init_init() envfree + nested_init_reinit(uint8) envfree + nested_reinit_init(uint8) envfree + nested_reinit_reinit(uint8,uint8) envfree + + // view + version() returns uint8 envfree + initializing() returns bool envfree +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Definitions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition isUninitialized() returns bool = version() == 0; +definition isInitialized() returns bool = version() > 0; +definition isDisabled() returns bool = version() == 255; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant notInitializing() + !initializing() + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: The version cannot decrease & disable state is irrevocable. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule increasingVersion(env e) { + uint8 versionBefore = version(); + bool disabledBefore = isDisabled(); + + method f; calldataarg args; + f(e, args); + + assert versionBefore <= version(), "_initialized must only increase"; + assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot initialize a contract that is already initialized. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotInitializeTwice() { + require isInitialized(); + + initialize@withrevert(); + + assert lastReverted, "contract must only be initialized once"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot initialize once disabled. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotInitializeOnceDisabled() { + require isDisabled(); + + initialize@withrevert(); + + assert lastReverted, "contract is disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot reinitialize once disabled. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotReinitializeOnceDisabled() { + require isDisabled(); + + uint8 n; + reinitialize@withrevert(n); + + assert lastReverted, "contract is disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot nest initializers (after construction). │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotNestInitializers_init_init() { + nested_init_init@withrevert(); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_init_reinit(uint8 m) { + nested_init_reinit@withrevert(m); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_reinit_init(uint8 n) { + nested_reinit_init@withrevert(n); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) { + nested_reinit_reinit@withrevert(n, m); + assert lastReverted, "nested initializers"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Initialize correctly sets the version. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule initializeEffects() { + requireInvariant notInitializing(); + + bool isUninitializedBefore = isUninitialized(); + + initialize@withrevert(); + bool success = !lastReverted; + + assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts"; + assert success => version() == 1, "initialize must set version() to 1"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Reinitialize correctly sets the version. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule reinitializeEffects() { + requireInvariant notInitializing(); + + uint8 versionBefore = version(); + + uint8 n; + reinitialize@withrevert(n); + bool success = !lastReverted; + + assert success <=> versionBefore < n, "can only reinitialize to a latter versions"; + assert success => version() == n, "reinitialize must set version() to n"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Can disable. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule disableEffect() { + requireInvariant notInitializing(); + + disable@withrevert(); + bool success = !lastReverted; + + assert success, "call to _disableInitializers failed"; + assert isDisabled(), "disable state not set"; +}