From 89962af16311ab1bdab848dae5a25c8e81d44e36 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 5 Oct 2022 15:23:26 +0200 Subject: [PATCH] Fix ERC20Wrapper.spec --- certora/applyHarness.patch | 128 ++++++++---------- .../Round2 => passes}/verifyERC20Wrapper.sh | 0 certora/specs/ERC20Wrapper.spec | 69 ++++++---- 3 files changed, 104 insertions(+), 93 deletions(-) rename certora/scripts/{noCI/Round2 => passes}/verifyERC20Wrapper.sh (100%) diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index b36796bb5..a0d61ef51 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -6,20 +6,20 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol * _Available since v4.6._ */ - function _checkRole(bytes32 role) internal view virtual { -+ function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public ++ function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public _checkRole(role, _msgSender()); } - + diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol --- governance/extensions/GovernorCountingSimple.sol 2022-09-27 10:26:58.548890299 +0200 +++ governance/extensions/GovernorCountingSimple.sol 2022-09-27 17:51:32.011301116 +0200 @@ -27,7 +27,7 @@ mapping(address => bool) hasVoted; } - + - mapping(uint256 => ProposalVote) private _proposalVotes; -+ mapping(uint256 => ProposalVote) internal _proposalVotes; - ++ mapping(uint256 => ProposalVote) internal _proposalVotes; // HARNESS: private -> internal + /** * @dev See {IGovernor-COUNTING_MODE}. diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol @@ -28,24 +28,24 @@ diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensi @@ -21,8 +21,8 @@ using SafeCast for uint256; using Timers for Timers.BlockNumber; - + - uint64 private _voteExtension; - mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines; -+ uint64 internal _voteExtension; // PRIVATE => INTERNAL -+ mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; // PRIVATE => INTERNAL - ++ uint64 internal _voteExtension; // HARNESS: private -> internal ++ mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines; // HARNESS: private -> internal + /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period. event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline); diff -ruN governance/Governor.sol governance/Governor.sol --- governance/Governor.sol 2022-09-29 10:07:27.126075551 +0200 +++ governance/Governor.sol 2022-09-27 17:51:32.014634743 +0200 @@ -44,7 +44,7 @@ - + string private _name; - + - mapping(uint256 => ProposalCore) private _proposals; -+ mapping(uint256 => ProposalCore) internal _proposals; - ++ mapping(uint256 => ProposalCore) internal _proposals; // HARNESS: private -> internal + // This queue keeps track of the governor operating on itself. Calls to functions protected by the // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, diff -ruN governance/TimelockController.sol governance/TimelockController.sol @@ -56,12 +56,12 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); bytes32 public constant CANCELLER_ROLE = keccak256("CANCELLER_ROLE"); - uint256 internal constant _DONE_TIMESTAMP = uint256(1); -+ uint256 public constant _DONE_TIMESTAMP = uint256(1); - ++ uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public + mapping(bytes32 => uint256) private _timestamps; - uint256 private _minDelay; -+ uint256 public _minDelay; - ++ uint256 public _minDelay; // HARNESS: private -> public + /** * @dev Emitted when a call is scheduled as part of operation `id`. diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol @@ -70,7 +70,7 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - + - mapping(address => address) private _delegation; + // HARNESS : Hooks cannot access any information from Checkpoints yet, so I am also updating votes and fromBlock in this struct + struct Ckpt { @@ -90,19 +90,19 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol + return _delegateCheckpoints[account]._checkpoints[pos]._value; + } + -+ mapping(address => address) public _delegation; ++ mapping(address => address) public _delegation; // HARNESS: private -> public mapping(address => Checkpoints.History) private _delegateCheckpoints; Checkpoints.History private _totalCheckpoints; - + @@ -124,7 +142,7 @@ * * Emits events {DelegateChanged} and {DelegateVotesChanged}. */ - function _delegate(address account, address delegatee) internal virtual { -+ function _delegate(address account, address delegatee) public virtual { ++ function _delegate(address account, address delegatee) public virtual { // HARNESS: internal -> public address oldDelegate = delegates(account); _delegation[account] = delegatee; - + @@ -142,10 +160,10 @@ uint256 amount ) internal virtual { @@ -121,13 +121,13 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol if (from != to && amount > 0) { if (from != address(0)) { - (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_subtract, amount); -+ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // HARNESSED TO REMOVE FUNCTION POINTERS ++ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[from].push(_delegateCheckpoints[from].latest() - amount); // Harnessed to remove function pointers + _checkpoints[from] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS emit DelegateVotesChanged(from, oldValue, newValue); } if (to != address(0)) { - (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_add, amount); -+ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // HARNESSED TO REMOVE FUNCTION POINTERS ++ (uint256 oldValue, uint256 newValue) = _delegateCheckpoints[to].push(_delegateCheckpoints[to].latest() + amount); // Harnessed to remove function pointers + _checkpoints[to] = Ckpt({fromBlock: SafeCast.toUint32(block.number), votes: SafeCast.toUint224(newValue)}); // HARNESS emit DelegateVotesChanged(to, oldValue, newValue); } @@ -143,17 +143,17 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol --- mocks/SafeERC20Helper.sol 2022-09-26 19:10:21.166619395 +0200 +++ mocks/SafeERC20Helper.sol 2022-09-27 17:51:32.014634743 +0200 @@ -4,7 +4,6 @@ - + import "../utils/Context.sol"; import "../token/ERC20/IERC20.sol"; -import "../token/ERC20/extensions/draft-ERC20Permit.sol"; import "../token/ERC20/utils/SafeERC20.sol"; - + contract ERC20ReturnFalseMock is Context { @@ -106,42 +105,43 @@ } } - + -contract ERC20PermitNoRevertMock is - ERC20("ERC20PermitNoRevertMock", "ERC20PermitNoRevertMock"), - ERC20Permit("ERC20PermitNoRevertMock") @@ -227,7 +227,7 @@ diff -ruN mocks/SafeERC20Helper.sol mocks/SafeERC20Helper.sol +// } +// } +// } - + contract SafeERC20Wrapper is Context { using SafeERC20 for IERC20; diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol @@ -238,14 +238,14 @@ diff -ruN proxy/utils/Initializable.sol proxy/utils/Initializable.sol * @custom:oz-retyped-from bool */ - uint8 private _initialized; -+ uint8 internal _initialized; - ++ uint8 internal _initialized; // HARNESS: private -> internal + /** * @dev Indicates that the contract is in the process of being initialized. */ - bool private _initializing; -+ bool internal _initializing; - ++ bool internal _initializing; // HARNESS: private -> internal + /** * @dev Triggered when the contract has been initialized or reinitialized. diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol @@ -253,11 +253,11 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol +++ token/ERC1155/ERC1155.sol 2022-09-27 17:51:32.014634743 +0200 @@ -21,7 +21,7 @@ using Address for address; - + // Mapping from token ID to account balances - mapping(uint256 => mapping(address => uint256)) private _balances; -+ mapping(uint256 => mapping(address => uint256)) internal _balances; // MUNGED private => internal - ++ mapping(uint256 => mapping(address => uint256)) internal _balances; // HARNESS: private -> internal + // Mapping from account to operator approvals mapping(address => mapping(address => bool)) private _operatorApprovals; @@ -471,7 +471,7 @@ @@ -265,7 +265,7 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol uint256 amount, bytes memory data - ) private { -+ ) public { // HARNESS: private -> public ++ ) public { // HARNESS: private -> public if (to.isContract()) { try IERC1155Receiver(to).onERC1155Received(operator, from, id, amount, data) returns (bytes4 response) { if (response != IERC1155Receiver.onERC1155Received.selector) { @@ -274,7 +274,7 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol uint256[] memory amounts, bytes memory data - ) private { -+ ) public { // HARNESS: private -> public ++ ) public { // HARNESS: private -> public if (to.isContract()) { try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns ( bytes4 response @@ -288,7 +288,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol - function _mint(address account, uint256 amount) internal virtual { + function _mint(address account, uint256 amount) public virtual { // HARNESS: internal -> public require(account != address(0), "ERC20: mint to the zero address"); - + _beforeTokenTransfer(address(0), account, amount); @@ -282,7 +282,7 @@ * - `account` cannot be the zero address. @@ -297,7 +297,7 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol - function _burn(address account, uint256 amount) internal virtual { + function _burn(address account, uint256 amount) public virtual { // HARNESS: internal -> public require(account != address(0), "ERC20: burn from the zero address"); - + _beforeTokenTransfer(account, address(0), amount); diff -ruN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol --- token/ERC20/extensions/ERC20Capped.sol 2022-08-31 13:44:36.381058287 +0200 @@ -319,10 +319,10 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20 token; amount; - return 0; -+ return fee; // HARNESS: made "return" nonzero ++ return fee; // HARNESS: made "return" nonzero } - -+ uint256 public fee; // HARNESS: added it to simulate random fee amount + ++ uint256 public fee; // HARNESS: added it to simulate random fee amount + /** * @dev Returns the receiver address of the flash fee. By default this @@ -333,23 +333,23 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); - + - mapping(address => address) private _delegates; - mapping(address => Checkpoint[]) private _checkpoints; -+ mapping(address => address) public _delegates; -+ mapping(address => Checkpoint[]) public _checkpoints; ++ mapping(address => address) public _delegates; // HARNESS: private -> public ++ mapping(address => Checkpoint[]) public _checkpoints; // HARNESS: private -> public Checkpoint[] private _totalSupplyCheckpoints; - + /** @@ -165,27 +165,27 @@ /** * @dev Maximum token supply. Defaults to `type(uint224).max` (2^224^ - 1). */ - function _maxSupply() internal view virtual returns (uint224) { -+ function _maxSupply() public view virtual returns (uint224) { //harnessed to public ++ function _maxSupply() public view virtual returns (uint224) { // HARNESS: internal -> public return type(uint224).max; } - + /** * @dev Snapshots the totalSupply after it has been increased. */ @@ -357,29 +357,29 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + function _mint(address account, uint256 amount) public virtual override { // HARNESS: internal -> public super._mint(account, amount); require(totalSupply() <= _maxSupply(), "ERC20Votes: total supply risks overflowing votes"); - + - _writeCheckpoint(_totalSupplyCheckpoints, _add, amount); -+ _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer ++ _writeCheckpointAdd(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } - + /** * @dev Snapshots the totalSupply after it has been decreased. */ - function _burn(address account, uint256 amount) internal virtual override { + function _burn(address account, uint256 amount) public virtual override { // HARNESS: internal -> public (to comply with the ERC20 harness) super._burn(account, amount); - + - _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount); -+ _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer ++ _writeCheckpointSub(_totalSupplyCheckpoints, amount); // HARNESS: new version without pointer } - + /** @@ -208,7 +208,7 @@ * * Emits events {DelegateChanged} and {DelegateVotesChanged}. */ - function _delegate(address delegator, address delegatee) internal virtual { -+ function _delegate(address delegator, address delegatee) public virtual { // HARNESSED TO MAKE PUBLIC ++ function _delegate(address delegator, address delegatee) public virtual { // HARNESS: internal -> public address currentDelegate = delegates(delegator); uint256 delegatorBalance = balanceOf(delegator); _delegates[delegator] = delegatee; @@ -392,7 +392,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote + emit DelegateVotesChanged(src, oldWeight, newWeight); } - + if (dst != address(0)) { - (uint256 oldWeight, uint256 newWeight) = _writeCheckpoint(_checkpoints[dst], _add, amount); + (uint256 oldWeight, uint256 newWeight) = _writeCheckpointAdd(_checkpoints[dst], amount); // HARNESS: new version without pointer @@ -402,7 +402,7 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote @@ -255,6 +256,55 @@ } } - + + // HARNESS: split _writeCheckpoint() to two functions as a workaround for function pointers that cannot be managed by the tool + function _writeCheckpointAdd( + Checkpoint[] storage ckpts, @@ -475,18 +475,8 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/ * @dev Returns the balance of `account`. */ - function _getVotingUnits(address account) internal view virtual override returns (uint256) { -+ function _getVotingUnits(address account) public view virtual override returns (uint256) { ++ function _getVotingUnits(address account) public view virtual override returns (uint256) { // HARNESS: internal -> public return balanceOf(account); } } -diff -ruN utils/Address.sol utils/Address.sol ---- utils/Address.sol 2022-09-29 10:07:27.126075551 +0200 -+++ utils/Address.sol 2022-09-27 17:51:32.014634743 +0200 -@@ -131,6 +131,7 @@ - uint256 value, - string memory errorMessage - ) internal returns (bytes memory) { -+ return ""; // external calls havoc - require(address(this).balance >= value, "Address: insufficient balance for call"); - (bool success, bytes memory returndata) = target.call{value: value}(data); - return verifyCallResultFromTarget(target, success, returndata, errorMessage); + diff --git a/certora/scripts/noCI/Round2/verifyERC20Wrapper.sh b/certora/scripts/passes/verifyERC20Wrapper.sh similarity index 100% rename from certora/scripts/noCI/Round2/verifyERC20Wrapper.sh rename to certora/scripts/passes/verifyERC20Wrapper.sh diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index a7da353ed..b052e3c87 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -1,29 +1,41 @@ -import "erc20.spec" +import "ERC20.spec" methods { - underlying() returns(address) envfree - underlyingTotalSupply() returns(uint256) envfree + underlying() returns(address) envfree + underlyingTotalSupply() returns(uint256) envfree underlyingBalanceOf(address) returns(uint256) envfree + depositFor(address, uint256) returns(bool) withdrawTo(address, uint256) returns(bool) - _recover(address) returns(uint256) + _recover(address) returns(uint256) } /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// // Invariants // /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +use invariant totalSupplyIsSumOfBalances + // totalsupply of wrapped should be less than or equal to underlying (assuming no external transfer) - solvency invariant whatAboutTotal(env e) totalSupply() <= underlyingTotalSupply() filtered { f -> f.selector != certorafallback_0().selector && !f.isView } { - preserved { + preserved with (env e2) { require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); + requireInvariant totalSupplyIsSumOfBalances; + require e.msg.sender == e2.msg.sender; } - preserved depositFor(address account, uint256 amount) with (env e2) { + preserved depositFor(address account, uint256 amount) with (env e3){ require totalSupply() + amount <= underlyingTotalSupply(); } + preserved _mint(address account, uint256 amount) with (env e4){ + require totalSupply() + amount <= underlyingTotalSupply(); + } + preserved _burn(address account, uint256 amount) with (env e5){ + require balanceOf(account) >= amount; + requireInvariant totalSupplyIsSumOfBalances; + } } // totalsupply of wrapped should be less than or equal to the underlying balanceOf contract (assuming no external transfer) - solvency @@ -34,6 +46,15 @@ invariant underTotalAndContractBalanceOfCorrelation(env e) require underlying() != currentContract; require e.msg.sender != currentContract; require e.msg.sender == e2.msg.sender; + requireInvariant totalSupplyIsSumOfBalances; + } + preserved _mint(address account, uint256 amount) with (env e4){ + require totalSupply() + amount <= underlyingBalanceOf(currentContract); + require underlying() != currentContract; + } + preserved _burn(address account, uint256 amount) with (env e5){ + require balanceOf(account) >= amount; + requireInvariant totalSupplyIsSumOfBalances; } } @@ -59,9 +80,9 @@ rule depositForSpecBasic(env e) { uint256 underlyingTotalAfter = underlyingTotalSupply(); uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); - assert wrapperTotalBefore == wrapperTotalAfter - amount, "wrapper total wrong update"; + assert wrapperTotalBefore == to_uint256(wrapperTotalAfter - amount), "wrapper total wrong update"; assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; - assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update"; + assert underlyingThisBalanceBefore == to_uint256(underlyingThisBalanceAfter - amount), "underlying this balance wrong update"; } // Check that values are updated correctly by `depositFor()` @@ -81,10 +102,10 @@ rule depositForSpecWrapper(env e) { assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount + && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - amount) , "wrapper balances wrong update"; - assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount + assert account != e.msg.sender => wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - amount) && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter , "wrapper balances wrong update"; } @@ -107,17 +128,17 @@ rule depositForSpecUnderlying(env e) { assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore && underlyingSenderBalanceAfter == underlyingUserBalanceAfter - && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount) , "underlying balances wrong update"; assert account != e.msg.sender - && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount - && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + && account == currentContract => underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount) + && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount) , "underlying balances wrong update"; assert account != e.msg.sender - && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount - && underlyingUserBalanceBefore == underlyingUserBalanceAfter + && account != currentContract => underlyingSenderBalanceBefore == to_uint256(underlyingSenderBalanceAfter + amount) + && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter) , "underlying balances wrong update"; } @@ -136,7 +157,7 @@ rule withdrawToSpecBasic(env e) { uint256 wrapperTotalAfter = totalSupply(); uint256 underlyingTotalAfter = underlyingTotalSupply(); - assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update"; + assert wrapperTotalBefore == to_uint256(wrapperTotalAfter + amount), "wrapper total wrong update"; assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; } @@ -156,10 +177,10 @@ rule withdrawToSpecWrapper(env e) { assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount + && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter + amount) , "wrapper user balance wrong update"; - assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount + assert account != e.msg.sender => wrapperSenderBalanceBefore == to_uint256(wrapperSenderBalanceAfter + amount) && wrapperUserBalanceBefore == wrapperUserBalanceAfter , "wrapper user balance wrong update"; } @@ -185,16 +206,16 @@ rule withdrawToSpecUnderlying(env e) { assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore && underlyingSenderBalanceAfter == underlyingUserBalanceAfter - && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + && underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount) , "underlying balances wrong update (acc == sender)"; assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter , "underlying balances wrong update (acc == contract)"; - assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == to_uint256(underlyingUserBalanceAfter - amount) && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter - && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount + && underlyingThisBalanceBefore == to_uint256(underlyingThisBalanceAfter + amount) , "underlying balances wrong update (acc != contract)"; } @@ -216,14 +237,14 @@ rule recoverSpec(env e) { uint256 wrapperUserBalanceAfter = balanceOf(account); uint256 wrapperSenderBalanceAfter = balanceOf(e.msg.sender); - assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update"; + assert wrapperTotalBefore == to_uint256(wrapperTotalAfter - value), "wrapper total wrong update"; assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore && wrapperUserBalanceAfter == wrapperSenderBalanceAfter - && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value + && wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - value) , "wrapper balances wrong update"; - assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value + assert e.msg.sender != account => wrapperUserBalanceBefore == to_uint256(wrapperUserBalanceAfter - value) && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter , "wrapper balances wrong update"; }