solidity content

.devcontainer/devcontainer.json

@@ -0,0 +1,4 @@
+{
+    "name": "certora-prover",
+    "image": "certora/certora-prover:ubuntu"
+}

.gitignore

@@ -0,0 +1,8 @@
+# Certora
+.certora*
+.last_confs
+certora_*
+
+# mac
+.DS_Store
+.zip-output-url.txt

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);
+    }
+
+}

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 {}

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;
+    }
+}

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 {}

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;
+        }
+    }
+}

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);
+}

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)
+}

resource_errors.json

@@ -0,0 +1,3 @@
+{
+    "topics": []
+}