From 6769f0b4f5e982ce6de3375f7364432b896527c3 Mon Sep 17 00:00:00 2001 From: ernestognw Date: Mon, 14 Aug 2023 21:52:28 -0600 Subject: [PATCH] Finish ERC20Wrapper --- certora/harnesses/ERC20WrapperHarness.sol | 15 +++++-- certora/specs/ERC20Wrapper.spec | 54 ++++++++++++----------- 2 files changed, 40 insertions(+), 29 deletions(-) diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index 5e55e4b72..ca183ad92 100644 --- 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/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index badfa7a28..ace75d060 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -1,18 +1,18 @@ -import "helpers/helpers.spec" -import "ERC20.spec" +import "helpers/helpers.spec"; +import "ERC20.spec"; methods { - underlying() returns(address) envfree - underlyingTotalSupply() returns(uint256) envfree - underlyingBalanceOf(address) returns(uint256) envfree - underlyingAllowanceToThis(address) returns(uint256) envfree + function underlying() external returns(address) envfree; + function underlyingTotalSupply() external returns(uint256) envfree; + function underlyingBalanceOf(address) external returns(uint256) envfree; + function underlyingAllowanceToThis(address) external returns(uint256) envfree; - depositFor(address, uint256) returns(bool) - withdrawTo(address, uint256) returns(bool) - recover(address) returns(uint256) + function depositFor(address, uint256) external returns(bool); + function withdrawTo(address, uint256) external returns(bool); + function recover(address) external returns(uint256); } -use invariant totalSupplyIsSumOfBalances +use invariant totalSupplyIsSumOfBalances; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -24,7 +24,7 @@ function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool { } function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool { - return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply(); + return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply()); } /* @@ -47,7 +47,7 @@ invariant totalSupplyIsSmallerThanUnderlyingBalance() } invariant noSelfWrap() - currentContract != underlying() + currentContract != underlying(); /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -85,6 +85,7 @@ rule depositFor(env e) { assert success <=> ( sender != currentContract && // invalid sender sender != 0 && // invalid sender + receiver != currentContract && // invalid receiver receiver != 0 && // invalid receiver amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance @@ -92,10 +93,10 @@ rule depositFor(env e) { // effects assert success => ( - balanceOf(receiver) == balanceBefore + amount && - totalSupply() == supplyBefore + amount && - underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount && - underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount + to_mathint(balanceOf(receiver)) == balanceBefore + amount && + to_mathint(totalSupply()) == supplyBefore + amount && + to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount && + to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount ); // no side effect @@ -137,17 +138,18 @@ rule withdrawTo(env e) { // liveness assert success <=> ( - sender != 0 && // invalid sender - receiver != 0 && // invalid receiver - amount <= balanceBefore // withdraw doesn't exceed balance + sender != 0 && // invalid sender + receiver != currentContract && // invalid receiver + receiver != 0 && // invalid receiver + amount <= balanceBefore // withdraw doesn't exceed balance ); // effects assert success => ( - balanceOf(sender) == balanceBefore - amount && - totalSupply() == supplyBefore - amount && - underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && - underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) + to_mathint(balanceOf(sender)) == balanceBefore - amount && + to_mathint(totalSupply()) == supplyBefore - amount && + to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && + to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) ); // no side effect @@ -172,7 +174,7 @@ rule recover(env e) { requireInvariant totalSupplyIsSumOfBalances; requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; - uint256 value = underlyingBalanceOf(currentContract) - totalSupply(); + mathint value = underlyingBalanceOf(currentContract) - totalSupply(); uint256 supplyBefore = totalSupply(); uint256 balanceBefore = balanceOf(receiver); @@ -187,8 +189,8 @@ rule recover(env e) { // effect assert success => ( - balanceOf(receiver) == balanceBefore + value && - totalSupply() == supplyBefore + value && + to_mathint(balanceOf(receiver)) == balanceBefore + value && + to_mathint(totalSupply()) == supplyBefore + value && totalSupply() == underlyingBalanceOf(currentContract) );