diff --git a/CVLByExample/ERC20Assembly/ERC20PermitMock.sol b/CVLByExample/ERC20Assembly/ERC20PermitMock.sol new file mode 100644 index 00000000..b4289751 --- /dev/null +++ b/CVLByExample/ERC20Assembly/ERC20PermitMock.sol @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v5.0.0) (token/ERC20/extensions/ERC20Permit.sol) + +pragma solidity 0.8.22; + +import { IERC20 } from "./IERC20.sol"; + +contract ERC20PermitMock is IERC20 { + + bytes32 private immutable PERMIT_TYPEHASH; + + uint256 t; + mapping(address => uint256) b; + mapping(address => mapping(address => uint256)) a; + mapping(address => uint256) public nonces; + + string public name; + string public symbol; + uint public decimals; + + constructor(bytes32 permit_typehash) { + PERMIT_TYPEHASH = permit_typehash; + } + + function myAddress() external view returns (address) { + return address(this); + } + + function totalSupply() external view returns (uint256) { + return t; + } + + function balanceOf(address account) external view returns (uint256) { + return b[account]; + } + + function transfer(address recipient, uint256 amount) external returns (bool) { + b[msg.sender] -= amount; + b[recipient] += amount; + + return true; + } + + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + + function approve(address spender, uint256 amount) external returns (bool) { + return _approve(msg.sender, spender, amount); + } + + function _approve(address owner, address spender, uint256 amount) internal returns (bool) { + a[owner][spender] = amount; + + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + b[sender] -= amount; + b[recipient] += amount; + a[sender][msg.sender] -= amount; + + return true; + } + + function permit(bytes calldata data) external { + ( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) = abi.decode(data, (address,address,uint256,uint256,uint8,bytes32,bytes32)); + permit(owner, spender, value, deadline, v, r, s); + } + + function permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) public virtual { + if (block.timestamp > deadline) revert ("deadline expired"); + nonces[owner]++; + bytes32 hash = keccak256(abi.encode(PERMIT_TYPEHASH, owner, spender, value, nonces[owner], deadline)); + + address signer = ecrecover(hash, v, r, s); + if (signer != owner) revert ("signer is not owner"); + + _approve(owner, spender, value); + } +} + +contract DummyERC20A is ERC20PermitMock { + constructor(bytes32 permit_typehash) ERC20PermitMock(permit_typehash) {} +} + +contract DummyERC20B is ERC20PermitMock { + constructor(bytes32 permit_typehash) ERC20PermitMock(permit_typehash) {} +} + +contract DummyERC20C is ERC20PermitMock { + constructor(bytes32 permit_typehash) ERC20PermitMock(permit_typehash) {} +} \ No newline at end of file diff --git a/CVLByExample/ERC20Assembly/ERC20Utils.sol b/CVLByExample/ERC20Assembly/ERC20Utils.sol new file mode 100644 index 00000000..755498e1 --- /dev/null +++ b/CVLByExample/ERC20Assembly/ERC20Utils.sol @@ -0,0 +1,234 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.22; + +// Interfaces +import { IERC20 } from "./IERC20.sol"; + +/// @title ERC20Utils +/// @notice Optimized functions for ERC20 tokens +library ERC20Utils { + /*////////////////////////////////////////////////////////////// + ERRORS + //////////////////////////////////////////////////////////////*/ + + error IncorrectEthAmount(); + error PermitFailed(); + error TransferFromFailed(); + error TransferFailed(); + error ApprovalFailed(); + + /*////////////////////////////////////////////////////////////// + CONSTANTS + //////////////////////////////////////////////////////////////*/ + + IERC20 internal constant ETH = IERC20(0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE); + + /*////////////////////////////////////////////////////////////// + APPROVE + //////////////////////////////////////////////////////////////*/ + + /// @dev Vendored from Solady by @vectorized - SafeTransferLib.approveWithRetry + /// https://github.com/Vectorized/solady/src/utils/SafeTransferLib.sol#L325 + /// Instead of approving a specific amount, this function approves for uint256(-1) (type(uint256).max). + function approve(IERC20 token, address to) internal { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + mstore(0x14, to) // Store the `to` argument. + mstore(0x34, 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) // Store the `amount` + // argument (type(uint256).max). + mstore(0x00, 0x095ea7b3000000000000000000000000) // `approve(address,uint256)`. + // Perform the approval, retrying upon failure. + if iszero( + and( // The arguments of `and` are evaluated from right to left. + or(eq(mload(0x00), 1), iszero(returndatasize())), // Returned 1 or nothing. + call(gas(), token, 0, 0x10, 0x44, 0x00, 0x20) + ) + ) { + mstore(0x34, 0) // Store 0 for the `amount`. + mstore(0x00, 0x095ea7b3000000000000000000000000) // `approve(address,uint256)`. + pop(call(gas(), token, 0, 0x10, 0x44, codesize(), 0x00)) // Reset the approval. + mstore(0x34, 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) // Store + // type(uint256).max for the `amount`. + // Retry the approval, reverting upon failure. + if iszero( + and( + or(eq(mload(0x00), 1), iszero(returndatasize())), // Returned 1 or nothing. + call(gas(), token, 0, 0x10, 0x44, 0x00, 0x20) + ) + ) { + mstore(0, 0x8164f84200000000000000000000000000000000000000000000000000000000) + // store the selector (error ApprovalFailed()) + revert(0, 4) // revert with error selector + } + } + mstore(0x34, 0) // Restore the part of the free memory pointer that was overwritten. + } + } + + /*////////////////////////////////////////////////////////////// + PERMIT + //////////////////////////////////////////////////////////////*/ + + /// @dev Executes an ERC20 permit and reverts if invalid length is provided + function permit(IERC20 token, bytes calldata data) internal { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + // check the permit length + switch data.length + // 32 * 7 = 224 EIP2612 Permit + case 224 { + let x := mload(64) // get the free memory pointer + mstore(x, 0xd505accf00000000000000000000000000000000000000000000000000000000) // store the selector + // function permit(address owner, address spender, uint256 + // amount, uint256 deadline, uint8 v, bytes32 r, bytes32 s) + calldatacopy(add(x, 4), data.offset, 224) // store the args + pop(call(gas(), token, 0, x, 228, 0, 32)) // call ERC20 permit, skip checking return data + } + // 32 * 8 = 256 DAI-Style Permit + case 256 { + let x := mload(64) // get the free memory pointer + mstore(x, 0x8fcbaf0c00000000000000000000000000000000000000000000000000000000) // store the selector + // function permit(address holder, address spender, uint256 + // nonce, uint256 expiry, bool allowed, uint8 v, bytes32 r, bytes32 s) + calldatacopy(add(x, 4), data.offset, 256) // store the args + pop(call(gas(), token, 0, x, 260, 0, 32)) // call ERC20 permit, skip checking return data + } + default { + mstore(0, 0xb78cb0dd00000000000000000000000000000000000000000000000000000000) // store the selector + // (error PermitFailed()) + revert(0, 4) + } + } + } + + /*////////////////////////////////////////////////////////////// + ETH + //////////////////////////////////////////////////////////////*/ + + /// @dev Returns 1 if the token is ETH, 0 if not ETH + function isETH(IERC20 token, uint256 amount) internal view returns (uint256 fromETH) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + // If token is ETH + if eq(token, 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE) { + // if msg.value is not equal to fromAmount, then revert + if xor(amount, callvalue()) { + mstore(0, 0x8b6ebb4d00000000000000000000000000000000000000000000000000000000) // store the selector + // (error IncorrectEthAmount()) + revert(0, 4) // revert with error selector + } + // return 1 if ETH + fromETH := 1 + } + // If token is not ETH + if xor(token, 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE) { + // if msg.value is not equal to 0, then revert + if gt(callvalue(), 0) { + mstore(0, 0x8b6ebb4d00000000000000000000000000000000000000000000000000000000) // store the selector + // (error IncorrectEthAmount()) + revert(0, 4) // revert with error selector + } + } + } + // return 0 if not ETH + } + + /*////////////////////////////////////////////////////////////// + TRANSFER + //////////////////////////////////////////////////////////////*/ + + /// @dev Executes transfer and reverts if it fails, works for both ETH and ERC20 transfers + function safeTransfer(IERC20 token, address recipient, uint256 amount) internal returns (bool success) { + // solhint-disable-next-line no-inline-assembly + assembly { + switch eq(token, 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE) + // ETH + case 1 { + // transfer ETH + // Cap gas at 10000 to avoid reentrancy + success := call(10000, recipient, amount, 0, 0, 0, 0) + } + // ERC20 + default { + let x := mload(64) // get the free memory pointer + mstore(x, 0xa9059cbb00000000000000000000000000000000000000000000000000000000) // store the selector + // (function transfer(address recipient, uint256 amount)) + mstore(add(x, 4), recipient) // store the recipient + mstore(add(x, 36), amount) // store the amount + success := call(gas(), token, 0, x, 68, 0, 32) // call transfer + if success { + switch returndatasize() + // check the return data size + case 0 { success := gt(extcodesize(token), 0) } + default { success := and(gt(returndatasize(), 31), eq(mload(0), 1)) } + } + } + if iszero(success) { + mstore(0, 0x90b8ec1800000000000000000000000000000000000000000000000000000000) // store the selector + // (error TransferFailed()) + revert(0, 4) // revert with error selector + } + } + } + + /*////////////////////////////////////////////////////////////// + TRANSFER FROM + //////////////////////////////////////////////////////////////*/ + + /// @dev Executes transferFrom and reverts if it fails + function safeTransferFrom( + IERC20 srcToken, + address sender, + address recipient, + uint256 amount + ) + internal + returns (bool success) + { + // solhint-disable-next-line no-inline-assembly + assembly { + let x := mload(64) // get the free memory pointer + mstore(x, 0x23b872dd00000000000000000000000000000000000000000000000000000000) // store the selector + // (function transferFrom(address sender, address recipient, + // uint256 amount)) + mstore(add(x, 4), sender) // store the sender + mstore(add(x, 36), recipient) // store the recipient + mstore(add(x, 68), amount) // store the amount + success := call(gas(), srcToken, 0, x, 100, 0, 32) // call transferFrom + if success { + switch returndatasize() + // check the return data size + case 0 { success := gt(extcodesize(srcToken), 0) } + default { success := and(gt(returndatasize(), 31), eq(mload(0), 1)) } + } + if iszero(success) { + mstore(x, 0x7939f42400000000000000000000000000000000000000000000000000000000) // store the selector + // (error TransferFromFailed()) + revert(x, 4) // revert with error selector + } + } + } + + /*////////////////////////////////////////////////////////////// + BALANCE + //////////////////////////////////////////////////////////////*/ + + /// @dev Returns the balance of an account, works for both ETH and ERC20 tokens + function getBalance(IERC20 token, address account) internal view returns (uint256 balanceOf) { + // solhint-disable-next-line no-inline-assembly + assembly { + switch eq(token, 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE) + // ETH + case 1 { balanceOf := balance(account) } + // ERC20 + default { + let x := mload(64) // get the free memory pointer + mstore(x, 0x70a0823100000000000000000000000000000000000000000000000000000000) // store the selector + // (function balanceOf(address account)) + mstore(add(x, 4), account) // store the account + let success := staticcall(gas(), token, x, 36, x, 32) // call balanceOf + if success { balanceOf := mload(x) } // load the balance + } + } + } +} diff --git a/CVLByExample/ERC20Assembly/ERC20UtilsEquivalence.spec b/CVLByExample/ERC20Assembly/ERC20UtilsEquivalence.spec new file mode 100644 index 00000000..f926e3ac --- /dev/null +++ b/CVLByExample/ERC20Assembly/ERC20UtilsEquivalence.spec @@ -0,0 +1,309 @@ +import "ETH.spec"; + +using main as harness; +using mock as mock; + +methods { + /// permit() data encoding + function harness.encodeForPermit224(address,address,uint256,uint256,uint8,bytes32,bytes32) external returns (bytes memory) envfree; + function harness.encodeForPermit256(address,address,uint256,uint256,bool,uint8,bytes32,bytes32) external returns (bytes memory) envfree; + + /// approve() + function mock.approveTo() external returns (address) envfree; + function mock.approveSuccess() external returns (bool) envfree; + /// permit() + function mock.permitOwner() external returns (address) envfree; + function mock.permitSpender() external returns (address) envfree; + function mock.permitValue() external returns (uint256) envfree; + function mock.permitDeadline() external returns (uint256) envfree; + function mock.permitV() external returns (uint8) envfree; + function mock.permitR() external returns (bytes32) envfree; + function mock.permitS() external returns (bytes32) envfree; + function mock.permitDatahash() external returns (bytes32) envfree; + function mock.permitSuccess() external returns (bool) envfree; + /// safeTransfer() + function mock.safeTransferRecipient() external returns (address) envfree; + function mock.safeTransferAmount() external returns (uint256) envfree; + function mock.safeTransferSuccess() external returns (bool) envfree; + /// safeTransferFrom() + function mock.safeTransferFromSender() external returns (address) envfree; + function mock.safeTransferFromRecipient() external returns (address) envfree; + function mock.safeTransferFromAmount() external returns (uint256) envfree; + function mock.safeTransferFromSuccess() external returns (bool) envfree; + /// getBalance() + function mock.getBalanceAccount() external returns (address) envfree; + function mock.balance() external returns (uint256) envfree; + + /// DISPATCHERS + function _.permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external => DISPATCHER(true); + function _.permit(address,address,uint256,uint256,bool,uint8,bytes32,bytes32) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + + function _._ external => DISPATCH [ + mock.approve(address,uint256), + ] default NONDET; +} + +definition permit224_sig() returns uint32 = 0xd505accf; + //sig:mock.permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; + +definition permit256_sig() returns uint32 = 0x8fcbaf0c; + //sig:mock.permit(address,address,uint256,uint256,bool,uint8,bytes32,bytes32).selector; + +definition transfer_sig() returns uint32 = 0xa9059cbb; + //sig:mock.transfer(address,uint256).selector; + +definition transferFrom_sig() returns uint32 = 0x23b872dd; + //sig:mock.transferFrom(uint256,uint256,address,bytes).selector; + +definition balanceOf_sig() returns uint32 = 0x70a08231; + //sig:mock.balanceOf(address).selector; + +definition approve_sig() returns uint32 = 0x095ea7b3; + //sig:mock.approve(address,uint256).selector; + +/// ghost boolean for "function was called". +persistent ghost bool called_permit224; +persistent ghost bool called_permit256; +persistent ghost bool called_transfer; +persistent ghost bool called_transferFrom; +persistent ghost bool called_balanceOf; +persistent ghost bool called_approve; + +/// ghost address for function callee. +persistent ghost address callee_token_permit224; +persistent ghost address callee_token_permit256; +persistent ghost address callee_token_transfer; +persistent ghost address callee_token_transferFrom; +persistent ghost address callee_token_balanceOf; +persistent ghost address callee_token_approve; + +/// ghost boolean for "permit was successful" +persistent ghost bool permit_succees; + +function nullify_ghosts() { + called_permit224 = false; + called_permit256 = false; + called_transfer = false; + called_transferFrom = false; + called_balanceOf = false; + called_approve = false; + + callee_token_permit224 = 0; + callee_token_permit256 = 0; + callee_token_transfer = 0; + callee_token_transferFrom = 0; + callee_token_balanceOf = 0; + callee_token_approve = 0; + + permit_succees = false; +} + +hook STATICCALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + if (selector == balanceOf_sig()) { + called_balanceOf = true; + callee_token_balanceOf = addr; + } +} + +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + if (selector == transfer_sig()) { + called_transfer = true; + callee_token_transfer = addr; + } else if (selector == transferFrom_sig()) { + called_transferFrom = true; + callee_token_transferFrom = addr; + } else if (selector == permit224_sig()) { + called_permit224 = true; + callee_token_permit224 = addr; + permit_succees = rc > 0; + } else if (selector == permit256_sig()) { + called_permit256 = true; + callee_token_permit256 = addr; + permit_succees = rc > 0; + } else if (selector == approve_sig()) { + called_approve = true; + callee_token_approve = addr; + } +} + +/// @title Validate data for permit() +rule test_call_through_permit(env e, address token) { + nullify_ghosts(); + bytes data; + harness.permit(e, token, data); + + assert permit_succees => called_permit224 || called_permit256; + assert permit_succees => data.length == 224 || data.length == 256; + assert permit_succees => token == callee_token_permit224 || token == callee_token_permit256; +} + +/// @title Validate permit() with encoded data (len=224) +rule test_encoded_call_through_permit224(env e, address token) { + nullify_ghosts(); + address owner; + address spender; + uint256 value; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + bytes data = harness.encodeForPermit224(owner, spender, value, deadline, v, r, s); + + harness.permit(e, token, data); + if(permit_succees) { + assert mock.permitOwner() == owner; + assert mock.permitSpender() == spender; + assert mock.permitValue() == value; + assert mock.permitDeadline() == deadline; + assert mock.permitV() == v; + assert mock.permitR() == r; + assert mock.permitS() == s; + assert keccak256(data) == mock.permitDatahash(); + assert token == callee_token_permit224; + } + else { + assert !(e.msg.value == 0 && mock.permitSuccess()); + } +} + +/// @title Validate permit() with encoded data (len=256) +rule test_encoded_call_through_permit256(env e, address token) { + nullify_ghosts(); + address owner; + address spender; + uint256 value; + uint256 deadline; + bool allowed; + uint8 v; + bytes32 r; + bytes32 s; + bytes data = harness.encodeForPermit256(owner, spender, value, deadline, allowed, v, r, s); + + harness.permit(e, token, data); + if(permit_succees) { + assert mock.permitOwner() == owner; + assert mock.permitSpender() == spender; + assert mock.permitValue() == value; + assert mock.permitDeadline() == deadline; + assert mock.permitV() == v; + assert mock.permitR() == r; + assert mock.permitS() == s; + assert keccak256(data) == mock.permitDatahash(); + assert token == callee_token_permit256; + } + else { + assert !(e.msg.value == 0 && mock.permitSuccess()); + } +} + +/// @title Validate data for transferFrom() +rule test_call_through_transferFrom(env e, address token) { + nullify_ghosts(); + address sender; + address recipient; + uint256 amount; + bool result = harness.safeTransferFrom(e, token, sender, recipient, amount); + + assert called_transferFrom; + assert mock.safeTransferFromSuccess(); + assert token == callee_token_transferFrom; + assert sender == mock.safeTransferFromSender(); + assert recipient == mock.safeTransferFromRecipient(); + assert amount == mock.safeTransferFromAmount(); + satisfy token != ETH(); +} + +/// @title Validate data for approve() +rule test_call_through_approve(env e, address token) { + nullify_ghosts(); + address to; + harness.approve(e, token, to); + + assert called_approve; + assert mock == callee_token_approve => mock.approveSuccess(); + assert mock == callee_token_approve => token == callee_token_approve; + assert mock == callee_token_approve => to == mock.approveTo(); + satisfy token != ETH() && mock == callee_token_approve; +} + +/// @title Validate data for transfer() +rule test_call_through_transfer(env e, address token) { + nullify_ghosts(); + address recipient; + uint256 amount; + + env e1; + mathint recipient_balance_pre = harness.getBalance(e1, token, recipient); + bool result = harness.safeTransfer(e, token, recipient, amount); + mathint recipient_balance_post = harness.getBalance(e1, token, recipient); + + assert token != ETH() => mock.safeTransferSuccess(); + assert called_transfer <=> (token != ETH()); + assert token == callee_token_transfer || token == ETH(); + assert token != ETH() => recipient == mock.safeTransferRecipient(); + assert token != ETH() => amount == mock.safeTransferAmount(); + + /// For ETH() only we don't pass through the mock and call the fallback instead. + if(token == ETH()) { + assert (result && recipient != harness) => + recipient_balance_post - recipient_balance_pre == to_mathint(amount); + assert !(result && recipient != harness) => + recipient_balance_post == recipient_balance_pre; + } + + satisfy token == ETH(); +} + +/// @title Validate revert condition for transfer() +rule test_safeTransfer_revert(env e, address token) { + nullify_ghosts(); + require e.msg.value == 0; + require token != ETH(); + address recipient; + uint256 amount; + harness.safeTransfer@withrevert(e, token, recipient, amount); + bool reverted = lastReverted; + + assert reverted => !mock.safeTransferSuccess(); + satisfy reverted; +} + +/// @title Validate revert condition for transferFrom() +rule test_safeTransferFrom_revert(env e, address token) { + nullify_ghosts(); + require e.msg.value == 0; + address sender; + address recipient; + uint256 amount; + harness.safeTransferFrom@withrevert(e, token, sender, recipient, amount); + bool reverted = lastReverted; + + assert reverted => !mock.safeTransferFromSuccess(); + satisfy reverted; +} + +/// @title Validate data for balanceOf() +rule test_call_through_balanceOf(env e, address token) { + nullify_ghosts(); + address account; + uint256 result = harness.getBalance(e, token, account); + + assert called_balanceOf <=> token != ETH(); + assert token == callee_token_balanceOf || token == ETH(); + assert token != ETH() => result == mock.balance(); + assert token == ETH() => result == nativeBalances[account]; + assert token != ETH() => account == mock.getBalanceAccount(); + satisfy token != ETH(); +} + +/// @title Test for isETH() +rule test_isETH(env e, address token) { + uint256 amount; + uint256 isETH_ = isETH(e, token, amount); + + assert token == ETH() => isETH_ == 1; + assert token != ETH() => isETH_ == 0; +} \ No newline at end of file diff --git a/CVLByExample/ERC20Assembly/ERC20UtilsSummary.spec b/CVLByExample/ERC20Assembly/ERC20UtilsSummary.spec new file mode 100644 index 00000000..832445b0 --- /dev/null +++ b/CVLByExample/ERC20Assembly/ERC20UtilsSummary.spec @@ -0,0 +1,117 @@ +import "ETH.spec"; + +using DummyERC20A as erc20A; +using DummyERC20B as erc20B; +using DummyERC20C as erc20C; +using FallbackCaller as FallbackCaller; + +methods { + function ERC20Utils.getBalance(address token, address account) internal returns (uint256) with (env e) => dispatchBalanceOf(e, calledContract, token, account); + function ERC20Utils.safeTransfer(address token, address recipient, uint256 amount) internal returns (bool) with (env e) => dispatchTransfer(e, calledContract, token, recipient, amount); + function ERC20Utils.safeTransferFrom(address token, address sender, address recipient, uint256 amount) internal returns (bool) with (env e) => dispatchTransferFrom(e, calledContract, token, sender, recipient, amount); + function ERC20Utils.approve(address token, address to) internal with (env e) => dispatchApprove(e, calledContract, token, to); + function ERC20Utils.permit(address token, bytes calldata data) internal with (env e) => dispatchPermit(e, calledContract, token, data); + function ERC20Utils.isETH(address token, uint256 amount) internal returns (uint256) with (env e) => isETHSummary(token, amount, e.msg.value); +} + +definition FALLBACK_GAS() returns uint256 = 10000; + +function isETHSummary(address token, uint256 amount, uint256 msgvalue) returns uint256 { + if (token == ETH()) { + require msgvalue == amount; + return 1; + } else { + require msgvalue == 0; + } + return 0; +} + +function dispatchBalanceOf(env e, address caller, address token, address account) returns uint256 { + env ed; /// Dispatch environment + require ed.msg.sender == caller; + require ed.block.timestamp == e.block.timestamp; + require ed.msg.value == 0; + if (token == erc20A) { + return erc20A.balanceOf(ed, account); + } else if (token == erc20B) { + return erc20B.balanceOf(ed, account); + } else if(token == erc20C) { + return erc20C.balanceOf(ed, account); + } else if (token == ETH()) { + return nativeBalances[account]; + } else { + require false; // optimistic + } + return 0; +} + +function dispatchTransfer(env e, address caller, address token, address recipient, uint256 amount) returns bool { + env ed; /// Dispatch environment + require ed.msg.sender == caller; + require ed.block.timestamp == e.block.timestamp; + /// Only when the token is native, the contract sends ETH with it. + require token != ETH() => ed.msg.value == 0; + if (token == erc20A) { + return erc20A.transfer(ed, recipient, amount); + } else if (token == erc20B) { + return erc20B.transfer(ed, recipient, amount); + } else if (token == erc20C) { + return erc20C.transfer(ed, recipient, amount); + } else if (token == ETH()) { + /// WARNING: Only works for optimistic fallback! + return FallbackCaller.callFallback(ed, recipient, amount, 10000); + } else { + require false; // optimistic + } + return true; +} + +function dispatchTransferFrom(env e, address caller, address token, address sender, address recipient, uint256 amount) returns bool { + env ed; /// Dispatch environment + require ed.msg.sender == caller; + require ed.block.timestamp == e.block.timestamp; + require ed.msg.value == 0; + if (token == erc20A) { + return erc20A.transferFrom(ed, sender, recipient, amount); + } else if (token == erc20B) { + return erc20B.transferFrom(ed, sender, recipient, amount); + } else if (token == erc20C) { + return erc20C.transferFrom(ed, sender, recipient, amount); + } else { + require false; // optimistic + } + return true; +} + +function dispatchApprove(env e, address caller, address token, address to) { + env ed; /// Dispatch environment + require ed.msg.sender == caller; + require ed.block.timestamp == e.block.timestamp; + require ed.msg.value == 0; + if (token == erc20A) { + erc20A.approve(ed, to, max_uint256); + } else if (token == erc20B) { + erc20B.approve(ed, to, max_uint256); + } else if (token == erc20C) { + erc20C.approve(ed, to, max_uint256); + } else { + require false; // optimistic + } +} + +function dispatchPermit(env e, address caller, address token, bytes data) { + env ed; /// Dispatch environment + require ed.msg.sender == caller; + require ed.block.timestamp == e.block.timestamp; + require ed.msg.value == 0; + require data.length == 224; /// Assume only standard permit selector. + if (token == erc20A) { + erc20A.permit(ed, data); + } else if (token == erc20B) { + erc20B.permit(ed, data); + } else if (token == erc20C) { + erc20C.permit(ed, data); + } else { + require false; // optimistic + } +} diff --git a/CVLByExample/ERC20Assembly/ETH.spec b/CVLByExample/ERC20Assembly/ETH.spec new file mode 100644 index 00000000..4fd06f3f --- /dev/null +++ b/CVLByExample/ERC20Assembly/ETH.spec @@ -0,0 +1 @@ +definition ETH() returns address = 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE; \ No newline at end of file diff --git a/CVLByExample/ERC20Assembly/FallbackCaller.sol b/CVLByExample/ERC20Assembly/FallbackCaller.sol new file mode 100644 index 00000000..0b98ecfb --- /dev/null +++ b/CVLByExample/ERC20Assembly/FallbackCaller.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract FallbackCaller { + function callFallback(address to, uint256 amount, uint256 gas) external payable returns (bool) { + require(msg.value == amount, "must transfer native amount"); + (bool success, ) = to.call{gas: gas, value: amount}(""); + /// If call wasn't successful, send ETH back to sender + if(!success) { + payable(msg.sender).transfer(amount); + } + return success; + } +} diff --git a/CVLByExample/ERC20Assembly/IERC20.sol b/CVLByExample/ERC20Assembly/IERC20.sol new file mode 100644 index 00000000..db01cf4c --- /dev/null +++ b/CVLByExample/ERC20Assembly/IERC20.sol @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v5.0.0) (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.20; + +/** + * @dev Interface of the ERC20 standard as defined in the EIP. + */ +interface IERC20 { + /** + * @dev Emitted when `value` tokens are moved from one account (`from`) to + * another (`to`). + * + * Note that `value` may be zero. + */ + event Transfer(address indexed from, address indexed to, uint256 value); + + /** + * @dev Emitted when the allowance of a `spender` for an `owner` is set by + * a call to {approve}. `value` is the new allowance. + */ + event Approval(address indexed owner, address indexed spender, uint256 value); + + /** + * @dev Returns the value of tokens in existence. + */ + function totalSupply() external view returns (uint256); + + /** + * @dev Returns the value of tokens owned by `account`. + */ + function balanceOf(address account) external view returns (uint256); + + /** + * @dev Moves a `value` amount of tokens from the caller's account to `to`. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transfer(address to, uint256 value) external returns (bool); + + /** + * @dev Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) external view returns (uint256); + + /** + * @dev Sets a `value` amount of tokens as the allowance of `spender` over the + * caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + function approve(address spender, uint256 value) external returns (bool); + + /** + * @dev Moves a `value` amount of tokens from `from` to `to` using the + * allowance mechanism. `value` is then deducted from the caller's + * allowance. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transferFrom(address from, address to, uint256 value) external returns (bool); +} diff --git a/CVLByExample/ERC20Assembly/RulesWithSummary.spec b/CVLByExample/ERC20Assembly/RulesWithSummary.spec new file mode 100644 index 00000000..8b85f3cb --- /dev/null +++ b/CVLByExample/ERC20Assembly/RulesWithSummary.spec @@ -0,0 +1,51 @@ +import "ERC20UtilsSummary.spec"; +import "ETH.spec"; + +using main as main; + +function tokensAreNotETH() { + require erc20A != ETH(); + require erc20B != ETH(); + require erc20C != ETH(); +} + +rule call_through_transfer_ERC20(env e, address token) { + tokensAreNotETH(); + require token != ETH(); + + address recipient; + uint256 amount; + env e1; + mathint recipient_balance_pre = main.getBalance(e1, token, recipient); + bool result = main.safeTransfer(e, token, recipient, amount); + mathint recipient_balance_post = main.getBalance(e1, token, recipient); + + /// If the transfer is successful and the recipient is not the contract, + /// then the balance must increase by amount. Otherwise, the balance doesn't change. + assert (result && main != recipient) => recipient_balance_post - recipient_balance_pre == to_mathint(amount); + assert !(result && main != recipient) => recipient_balance_post == recipient_balance_pre; +} + +rule call_through_transfer_ETH(env e, address token) { + tokensAreNotETH(); + require token == ETH(); + + address recipient; + uint256 amount; + mathint recipient_native_pre = nativeBalances[recipient]; + bool result = main.safeTransfer(e, token, recipient, amount); + mathint recipient_native_post = nativeBalances[recipient]; + + /// If the transfer is successful and the recipient is not the contract, + /// then the balance must increase by amount. Otherwise, the balance doesn't change. + assert (result && main != recipient) => recipient_native_post - recipient_native_pre == to_mathint(amount); + assert !(result && main != recipient) => recipient_native_post == recipient_native_pre; +} + +rule call_through_approve(env e, address token, address to) { + tokensAreNotETH(); + + main.approve(e, token, to); + + satisfy token != ETH(); +} \ No newline at end of file diff --git a/CVLByExample/ERC20Assembly/Run.conf b/CVLByExample/ERC20Assembly/Run.conf new file mode 100644 index 00000000..7d511c8b --- /dev/null +++ b/CVLByExample/ERC20Assembly/Run.conf @@ -0,0 +1,17 @@ +{ + "files": [ + "main.sol", + "mock.sol", + ], + "hashing_length_bound": "416", + "rule_sanity":"basic", + "optimistic_fallback": true, + "prover_args":[ + "-copyLoopUnroll 10", + ], + "process": "emv", + "server":"production", + "solc": "solc8.22", + "verify": "main:ERC20UtilsEquivalence.spec", + "msg":"ERC20Utils Assembly-Solidity Equivalence" +} diff --git a/CVLByExample/ERC20Assembly/RunWithSummary.conf b/CVLByExample/ERC20Assembly/RunWithSummary.conf new file mode 100644 index 00000000..472e3fc4 --- /dev/null +++ b/CVLByExample/ERC20Assembly/RunWithSummary.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "main.sol", + "mock.sol", + "FallbackCaller.sol", + "ERC20PermitMock.sol:DummyERC20A", + "ERC20PermitMock.sol:DummyERC20B", + "ERC20PermitMock.sol:DummyERC20C", + ], + "hashing_length_bound": "416", + "rule_sanity":"basic", + "optimistic_fallback": true, + "prover_args":[ + "-copyLoopUnroll 10", + ], + "process": "emv", + "server":"production", + "solc": "solc8.22", + "verify": "main:RulesWithSummary.spec", + "msg":"ERC20Utils dispatch summary" +} diff --git a/CVLByExample/ERC20Assembly/main.sol b/CVLByExample/ERC20Assembly/main.sol new file mode 100644 index 00000000..08b60d83 --- /dev/null +++ b/CVLByExample/ERC20Assembly/main.sol @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MIT + +pragma solidity 0.8.22; + +import { IERC20 } from "./IERC20.sol"; +import { ERC20Utils } from "./ERC20Utils.sol"; + +contract main { + + using ERC20Utils for IERC20; + + function approve(IERC20 token, address to) external { + token.approve(to); + } + + function permit(IERC20 token, bytes calldata data) external { + token.permit(data); + } + + function isETH(IERC20 token, uint256 amount) external payable returns (uint256) { + return token.isETH(amount); + } + + function safeTransfer(IERC20 token, address recipient, uint256 amount) external returns (bool) { + return token.safeTransfer(recipient, amount); + } + + function safeTransferFrom( + IERC20 srcToken, + address sender, + address recipient, + uint256 amount + ) + external + returns (bool success) + { + return srcToken.safeTransferFrom(sender, recipient, amount); + } + + function getBalance(IERC20 token, address account) external view returns (uint256) { + return token.getBalance(account); + } + + function encodeForPermit224( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external pure returns (bytes memory) { + return abi.encode(owner, spender, value, deadline, v, r, s); + } + + function encodeForPermit256( + address owner, + address spender, + uint256 value, + uint256 deadline, + bool allowed, + uint8 v, + bytes32 r, + bytes32 s + ) external pure returns (bytes memory) { + return abi.encode(owner, spender, value, deadline, allowed, v, r, s); + } +} \ No newline at end of file diff --git a/CVLByExample/ERC20Assembly/mock.sol b/CVLByExample/ERC20Assembly/mock.sol new file mode 100644 index 00000000..3642ec56 --- /dev/null +++ b/CVLByExample/ERC20Assembly/mock.sol @@ -0,0 +1,89 @@ +// SPDX-License-Identifier: MIT + +pragma solidity 0.8.22; + +contract mock { + + address public approveTo; + uint256 public approveAmount; + bool public approveSuccess; + + function approve(address to, uint256 amount) external { + approveTo = to; + approveAmount = amount; + assert(approveSuccess || amount == 0); + } + + address public permitOwner; + address public permitSpender; + uint256 public permitValue; + uint256 public permitDeadline; + bool public permitAllowed; + uint8 public permitV; + bytes32 public permitR; + bytes32 public permitS; + bytes32 public permitDatahash; + bool public permitSuccess; + + function permit(address owner, address spender, + uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) + external { + permitOwner = owner; + permitSpender = spender; + permitValue = value; + permitDeadline = deadline; + permitV = v; + permitR = r; + permitS = s; + permitDatahash = keccak256(abi.encode(owner,spender,value,deadline,v,r,s)); + assert(permitSuccess); + } + + function permit(address owner, address spender, + uint256 value, uint256 deadline, bool allowed, uint8 v, bytes32 r, bytes32 s) + external { + permitOwner = owner; + permitSpender = spender; + permitValue = value; + permitDeadline = deadline; + permitAllowed = allowed; + permitV = v; + permitR = r; + permitS = s; + permitDatahash = keccak256(abi.encode(owner,spender,value,deadline,allowed,v,r,s)); + assert(permitSuccess); + } + + address public safeTransferRecipient; + uint256 public safeTransferAmount; + bool public safeTransferSuccess; + + function transfer(address recipient, uint256 amount) external returns (bool) { + safeTransferRecipient = recipient; + safeTransferAmount = amount; + return safeTransferSuccess; + } + + address public safeTransferFromSender; + address public safeTransferFromRecipient; + uint256 public safeTransferFromAmount; + bool public safeTransferFromSuccess; + + function transferFrom(address sender, address recipient, uint256 amount) + external + returns (bool) + { + safeTransferFromSender = sender; + safeTransferFromRecipient = recipient; + safeTransferFromAmount = amount; + return safeTransferFromSuccess; + } + + address public getBalanceAccount; + uint256 public balance; + + function balanceOf(address account) external returns (uint256) { + getBalanceAccount = account; + return balance; + } +} \ No newline at end of file