From 2b10037547bc8341b1d5166eb8ef76dea9e70cfb Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 16 Nov 2022 19:47:53 +0000 Subject: [PATCH] solidity content --- .devcontainer/devcontainer.json | 4 + .gitignore | 8 ++ EnglishAuction.sol | 168 +++++++++++++++++++++++++++++++ dependencies/DummyERC20A.sol | 6 ++ dependencies/DummyERC20Impl.sol | 80 +++++++++++++++ dependencies/DummyERC721A.sol | 6 ++ dependencies/DummyERC721Impl.sol | 66 ++++++++++++ dependencies/IERC721Receiver.sol | 27 +++++ erc20.spec | 12 +++ resource_errors.json | 3 + verifySpec.sh | 8 ++ 11 files changed, 388 insertions(+) create mode 100644 .devcontainer/devcontainer.json create mode 100644 .gitignore create mode 100644 EnglishAuction.sol create mode 100644 dependencies/DummyERC20A.sol create mode 100644 dependencies/DummyERC20Impl.sol create mode 100644 dependencies/DummyERC721A.sol create mode 100644 dependencies/DummyERC721Impl.sol create mode 100644 dependencies/IERC721Receiver.sol create mode 100644 erc20.spec create mode 100644 resource_errors.json create mode 100644 verifySpec.sh diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 0000000..60290f0 --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,4 @@ +{ + "name": "certora-prover", + "image": "certora/certora-prover:ubuntu" +} \ No newline at end of file diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c1bb69f --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +# Certora +.certora* +.last_confs +certora_* + +# mac +.DS_Store +.zip-output-url.txt diff --git a/EnglishAuction.sol b/EnglishAuction.sol new file mode 100644 index 0000000..831327f --- /dev/null +++ b/EnglishAuction.sol @@ -0,0 +1,168 @@ +// SPDX-License-Identifier: MIT +/* + +English auction for NFT. + +Auction Process: +- Seller of NFT deploys this contract, setting the initial bid, the NFT to be sold, and the + Token to be sold against. +- Auction lasts for 7 days (auction window). +- Participants can bid Token to become the new highest bid. + It's possible to increase the bid marginally, as long as the new position still becomes highest. + The participants have to pre-approve this contract for Token, in order to succesfully bid(). +- All bidders but the highest one can withdraw their bid. + +After the auction window +- Bids are no longer possible +- A call to end() moves the NFT to the highest bidder, and the highest bid amount to the seller. + + +Additional features: +- BidFor() - can send tokens to increase a bid for another user (address). +- withdrawAmount() - partially withdraw the position by 'amount', to a chosen 'receiver'. +- withdrawFor() - an allowed operator could call this for the user that allowed them, + and withdraw their position (also by 'amount'). +- setOperator() - set or revoke an address as an operator for the sender. + +*/ + +pragma solidity ^0.8.13; + +interface IERC721 { + function transferFrom( + address, + address, + uint + ) external; +} + +interface IERC20 { + function transferFrom( + address from, + address to, + uint amount + ) external returns(bool); +} + +contract EnglishAuction { + event Start(); + event Bid(address indexed sender, uint amount); + event Withdraw(address indexed bidder, uint amount); + event End(address winner, uint amount); + + IERC721 public nft; + IERC20 public token; + uint public nftId; + + address payable public seller; + uint public endAt; + bool public started; + bool public ended; + + address public highestBidder; + uint public highestBid; + mapping(address => uint) public bids; + mapping(address => mapping(address => bool)) public operators; + + constructor( + address _nft, + address _erc20, + uint _nftId, + uint _startingBid + ) { + nft = IERC721(_nft); + nftId = _nftId; + + token = IERC20(_erc20); + + seller = payable(msg.sender); + highestBid = _startingBid; + } + + function start() external { + require(!started, "started"); + require(msg.sender == seller, "not seller"); + ended = false; + nft.transferFrom(msg.sender, address(this), nftId); + started = true; + endAt = block.timestamp + 7 days; + + emit Start(); + } + + function setOperator(address operator, bool trusted) external { + operators[msg.sender][operator] = trusted; + } + + function bidFor(address bidder, uint amount) external { + _bid(bidder, msg.sender, amount); + } + + function bid(uint amount) external { + _bid(msg.sender, msg.sender, amount); + } + + function _bid(address bidder, address payer, uint amount) internal { + require(started, "not started"); + require(block.timestamp < endAt, "ended"); + uint previousBid = highestBid; + + require(token.transferFrom(payer, address(this), amount), "token transfer failed"); + + bids[bidder] += amount; + highestBidder = bidder; + highestBid = bids[highestBidder]; + + require(bids[highestBidder] > previousBid, "new high value < highest"); + emit Bid(bidder, amount); + } + + // Withdraw implementation. + // Bidder's credits are downed by 'amount', and those 'amount' tokens are sent ot the recipient. + function _withdraw(address bidder, address recipient, uint256 amount) internal { + require(bidder != highestBidder, "bidder cannot withdraw"); + bids[bidder] -= amount; + + bool success = token.transferFrom(address(this), recipient, amount); + require(success, "token transfer failed"); + + emit Withdraw(bidder, amount); + } + + // A basic default withdraw function. + function withdraw() external { + _withdraw(msg.sender, msg.sender, bids[msg.sender]); + } + + // A more controlled withdraw function + function withdrawAmount(address recipient, uint amount) external { + _withdraw(msg.sender, recipient, amount); + } + + // WithdrawFor() can be called by a trusted operator. Funds are transfered back to the operator. + function withdrawFor(address operated, uint amount) external { + require(operators[operated][msg.sender] || msg.sender == operated, "that operator was not allowed"); + _withdraw(operated, msg.sender, amount); + } + + // The end() functions marks the end of the auction. + // It would transfer the nft to the winning bidder, and the highest bid to the seller. + function end() external { + require(started, "not started"); + require(block.timestamp >= endAt, "not ended"); + require(!ended, "ended"); + bool _success; + + ended = true; + if (highestBidder != address(0)) { + nft.transferFrom(address(this), highestBidder, nftId); + _success = token.transferFrom(address(this), seller, bids[highestBidder]); + require(_success, "token transfer failed"); + } else { + nft.transferFrom(address(this), seller, nftId); + } + + emit End(highestBidder, highestBid); + } + +} diff --git a/dependencies/DummyERC20A.sol b/dependencies/DummyERC20A.sol new file mode 100644 index 0000000..735f66c --- /dev/null +++ b/dependencies/DummyERC20A.sol @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.13; +import "./DummyERC20Impl.sol"; + +// contract DummyERC20A is DummyERC20Impl {} +contract DummyERC20A is DummyERC20Impl {} \ No newline at end of file diff --git a/dependencies/DummyERC20Impl.sol b/dependencies/DummyERC20Impl.sol new file mode 100644 index 0000000..0fb0b32 --- /dev/null +++ b/dependencies/DummyERC20Impl.sol @@ -0,0 +1,80 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.13; + + +// With approval checks +contract DummyERC20Impl { + + uint256 private _totalSupply; + mapping (address => uint256) private balances; + mapping (address => mapping (address => uint256)) private _allowance; + + string public name; + string public symbol; + uint public decimals; + + + /*----------------------------------------------- + | getters | + -----------------------------------------------*/ + + function myAddress() public returns (address) { + return address(this); + } + + function totalSupply() public view returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view returns (uint256) { + return balances[account]; + } + + function allowance(address owner, address spender) public view returns (uint256) { + return _allowance[owner][spender]; + } + + + /*----------------------------------------------- + | operations | + -----------------------------------------------*/ + + function transfer(address recipient, uint256 amount) external returns (bool) { + require(msg.sender != address(0), "ERC20: transfer from the zero address"); + require(recipient != address(0), "ERC20: transfer to the zero address"); + + balances[msg.sender] -= amount; + balances[recipient] += amount; + return true; + } + + function approve(address spender, uint256 amount) external returns (bool) { + require(spender != address(0), "ERC20: approve to the zero address"); + + _allowance[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + require(recipient != address(0), "ERC20: transfer to the zero address"); + require(sender != address(0), "ERC20: transfer from the zero address"); + + return _transferFrom(sender, recipient, amount); + } + + function _transferFrom(address sender, address recipient, uint256 amount) internal returns (bool) { + balances[sender] -= amount; + balances[recipient] += amount; + + // Update _allowance + if (sender != msg.sender) { + _allowance[sender][msg.sender] -= amount; + } + + return true; + } +} diff --git a/dependencies/DummyERC721A.sol b/dependencies/DummyERC721A.sol new file mode 100644 index 0000000..cacc477 --- /dev/null +++ b/dependencies/DummyERC721A.sol @@ -0,0 +1,6 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +import "./DummyERC721Impl.sol"; + +contract DummyERC721A is DummyERC721Impl {} \ No newline at end of file diff --git a/dependencies/DummyERC721Impl.sol b/dependencies/DummyERC721Impl.sol new file mode 100644 index 0000000..ac6a498 --- /dev/null +++ b/dependencies/DummyERC721Impl.sol @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.13; + +import "./IERC721Receiver.sol"; + +/* + An incomplete implementation of ERC721 that only foscuses on transferFrom and ownership tracking. + Lacks support for approvals, and some other checks. +*/ +contract DummyERC721Impl { + string public name; + string public symbol; + + // Mapping from token ID to owner address + mapping(uint256 => address) private _owners; + + // Mapping owner address to token count + mapping(address => uint256) private _balances; + + + function balanceOf(address owner) external view returns (uint256) { + require(owner != address(0), "ERC721: Zero Address is invalid"); + return _balances[owner]; + } + + function ownerOf(uint256 tokenId) public view returns (address) { + address owner = _owners[tokenId]; + require(owner != address(0), "ERC721: invalid token ID"); + return owner; + } + + function _transferFrom(address from, address to, uint256 tokenId) internal { + require(_owners[tokenId] == from); + require(to != address(0)); + + _balances[from] -= 1; + _balances[to] += 1; + _owners[tokenId] = to; + } + + function transferFrom(address from, address to, uint256 tokenId) external payable { + _transferFrom(from, to, tokenId); + } + + function safeTransferFrom( + address from, + address to, + uint256 tokenId + ) public virtual { + _transferFrom(from, to, tokenId); + require(_checkOnERC721Received(from, to, tokenId), "ERC721: transfer to non ERC721Receiver implementer"); + } + + function _checkOnERC721Received( + address from, + address to, + uint256 tokenId + ) private returns (bool) { + if (to.code.length > 0) { + bytes4 retval = IERC721Receiver(to).onERC721Received(msg.sender, from, tokenId, ""); + return retval == IERC721Receiver.onERC721Received.selector; + } else { + return true; + } + } +} \ No newline at end of file diff --git a/dependencies/IERC721Receiver.sol b/dependencies/IERC721Receiver.sol new file mode 100644 index 0000000..de67209 --- /dev/null +++ b/dependencies/IERC721Receiver.sol @@ -0,0 +1,27 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC721/IERC721Receiver.sol) + +pragma solidity ^0.8.0; + +/** + * @title ERC721 token receiver interface + * @dev Interface for any contract that wants to support safeTransfers + * from ERC721 asset contracts. + */ +interface IERC721Receiver { + /** + * @dev Whenever an {IERC721} `tokenId` token is transferred to this contract via {IERC721-safeTransferFrom} + * by `operator` from `from`, this function is called. + * + * It must return its Solidity selector to confirm the token transfer. + * If any other value is returned or the interface is not implemented by the recipient, the transfer will be reverted. + * + * The selector can be obtained in Solidity with `IERC721Receiver.onERC721Received.selector`. + */ + function onERC721Received( + address operator, + address from, + uint256 tokenId, + bytes calldata data + ) external returns (bytes4); +} diff --git a/erc20.spec b/erc20.spec new file mode 100644 index 0000000..b12fec1 --- /dev/null +++ b/erc20.spec @@ -0,0 +1,12 @@ +// erc20 methods +methods { + name() returns (string) => DISPATCHER(true) + symbol() returns (string) => DISPATCHER(true) + decimals() returns (string) => DISPATCHER(true) + totalSupply() returns (uint256) => DISPATCHER(true) + balanceOf(address) returns (uint256) => DISPATCHER(true) + allowance(address,address) returns (uint) => DISPATCHER(true) + approve(address,uint256) returns (bool) => DISPATCHER(true) + transfer(address,uint256) returns (bool) => DISPATCHER(true) + transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) +} diff --git a/resource_errors.json b/resource_errors.json new file mode 100644 index 0000000..d9bd792 --- /dev/null +++ b/resource_errors.json @@ -0,0 +1,3 @@ +{ + "topics": [] +} \ No newline at end of file diff --git a/verifySpec.sh b/verifySpec.sh new file mode 100644 index 0000000..050f7fa --- /dev/null +++ b/verifySpec.sh @@ -0,0 +1,8 @@ +certoraRun EnglishAuction.sol dependencies/DummyERC20A.sol dependencies/DummyERC721A.sol \ + --verify EnglishAuction:exampleSpec.spec \ + --link EnglishAuction:token=DummyERC20A \ + --link EnglishAuction:nft=DummyERC721A \ + --optimistic_loop \ + --send_only \ + --rule_sanity basic \ + --msg "EnglishAuction"