Merge pull request Certora#26 from Certora/shoham/invariants-lesson

Invariants lesson code (Lesson 4).

lesson1_prerequisites/formal_verification/sisters.conf

@@ -3,7 +3,7 @@
         "Empty.sol"
     ],
     "verify": "Empty:sisters.spec",
-    "send_only": false,
-    "solc": "solc8.0",
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
     "msg": "Sisters riddle"
 }

lesson2_started/erc20/Parametric.conf

@@ -3,7 +3,7 @@
         "ERC20.sol"
     ],
     "verify": "ERC20:Parametric.spec",
-    "send_only": false,
-    "solc": "solc8.0",
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
     "msg": "Parametric rule example"
 }

lesson2_started/erc20/TotalGreaterThanUser.conf

@@ -3,7 +3,7 @@
         "ERC20.sol"
     ],
     "verify": "ERC20:TotalGreaterThanUser.spec",
-    "send_only": false,
-    "solc": "solc8.0",
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
     "msg": "Preconditions example"
 }

lesson2_started/erc20/sample_conf.conf

@@ -3,8 +3,8 @@
         "ERC20.sol"
     ],
     "verify": "ERC20:ERC20.spec",
-    "send_only": false,
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
     // Note: json5 supports comments!
-    "solc": "solc8.0",
     "msg": "First run using .conf file"
 }

lesson3_violations/Borda/Borda.conf

@@ -3,7 +3,7 @@
     "Borda.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "wait_for_results": "all",
   "msg": "Verification of Borda",
   "rule_sanity" : "advanced"
 }

lesson3_violations/Borda/BordaBug1.conf

@@ -3,6 +3,7 @@
     "BordaBug1.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "wait_for_results": "all",
+  "rule_sanity": "basic",
   "msg": "Verification of BordaBug1"
 }

lesson3_violations/Borda/BordaBug2.conf

@@ -3,6 +3,7 @@
     "BordaBug2.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "wait_for_results": "all",
+  "rule_sanity": "basic",
   "msg": "Verification of BordaBug2"
 }

lesson3_violations/Borda/BordaBug3.conf

@@ -3,6 +3,7 @@
     "BordaBug3.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "wait_for_results": "all",
+  "rule_sanity": "basic",
   "msg": "Verification of BordaBug3"
 }

lesson3_violations/Borda/BordaBug4.conf

@@ -3,6 +3,7 @@
     "BordaBug4.sol:Borda"
   ],
   "verify": "Borda:Borda.spec",
-  "send_only": false,
+  "wait_for_results": "all",
+  "rule_sanity": "basic",
   "msg": "Verification of BordaBug4"
 }

lesson3_violations/ERC20/ERC20.conf

@@ -3,8 +3,8 @@
         "ERC20.sol"
     ],
     "verify": "ERC20:ERC20.spec",
-    "send_only": false,
+    "wait_for_results": "all",
+    "rule_sanity": "basic",
     "optimistic_loop": true,
-    "solc": "solc8.0",
     "msg": "Verification of ERC20"
 }

lesson4_invariants/auction/EnglishAuction.sol

@@ -0,0 +1,189 @@
+// SPDX-License-Identifier: MIT
+/*
+English auction for NFT
+
+Auction Process:
+1. The seller of the NFT deploys this contract setting the
+   initial bid, the NFT to be sold, and the Token to be
+   sold against in the constructor.
+2. The auction lasts for 7 days (auction window).
+3. Participants can bid `token` to become the new highest
+   bidder. It is possible to increase the bid marginally,
+   as long as the new position still becomes highest.
+   The participants have to pre-approve this contract for
+   the `token`, in order to successfully bid.
+4. All bidders but the highest one can withdraw their bid.
+
+After the auction window is past:
+- Bids are no longer possible
+- A call to `end()` transfers the NFT to the highest bidder,
+  and the highest bid amount to the seller.
+
+Additional features:
+- Bids can be increased, and not only by the bidder
+- Bids can be reduced (partially withdrawn), by the bidder
+  or by a trusted third party operator
+- Trusted operators can be set or unset by the bidder
+*/
+
+pragma solidity ^0.8.13;
+
+
+/// @title Reduced ERC721 interface (NFT)
+interface IERC721 {
+    function transferFrom(
+        address,
+        address,
+        uint
+    ) external;
+}
+
+
+/// @title Reduced ERC20 interface (token)
+interface IERC20 {
+    function transferFrom(
+        address from,
+        address to,
+        uint amount
+    ) external returns(bool);
+}
+
+
+/// @title English auction for NFT
+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;  // The auctioned NFT
+    IERC20 public token;  // Accepted token for bidding
+    uint public nftId;
+
+    address payable public seller;  // The seller of the NFT
+    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;
+
+    /// @param _nft the auctioned NFT
+    /// @param _erc20 the token to be used for bidding
+    /// @param _startingBid minimal bid value
+    constructor(
+        address _nft,
+        address _erc20,
+        uint _nftId,
+        uint _startingBid
+    ) {
+        nft = IERC721(_nft);
+        nftId = _nftId;
+
+        token = IERC20(_erc20);
+
+        seller = payable(msg.sender);
+        highestBid = _startingBid;
+    }
+
+    /// Start the auction
+    function start() external {
+        require(!started, "started");
+        require(!ended, "started");
+        require(msg.sender == seller, "not seller");
+
+        started = true;
+        nft.transferFrom(msg.sender, address(this), nftId);
+        endAt = block.timestamp + 7 days;
+
+        emit Start();
+    }
+
+    /// Set or unset trusted operator for sender. The trusted operator can withdraw
+    /// bidder's funds.
+    function setOperator(address operator, bool trusted) external {
+        operators[msg.sender][operator] = trusted;
+    }
+
+    function bid(uint amount) external {
+        _bid(msg.sender, msg.sender, amount);
+    }
+
+    /// Send tokens to increase the bid of `bidder` 
+    function bidFor(address bidder, uint amount) external {
+        _bid(bidder, msg.sender, amount);
+    }
+
+    /// Bidding implementation.
+    /// @dev Funds are transferred from `payer` to support the bid of `bidder`.
+    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.
+    /// @dev Bid of `bidder` is reduced and funds are sent to 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);
+    }
+
+    /// Withdraw entire bid.
+    function withdraw() external {
+        _withdraw(msg.sender, msg.sender, bids[msg.sender]);
+    }
+
+    /// Reduce sender's bid amount, transferring the funds to recipient.
+    function withdrawAmount(address recipient, uint amount) external {
+        _withdraw(msg.sender, recipient, amount);
+    }
+
+    /// Reduce bid of `bidder`, transferring funds to message sender.
+    /// @notice message sender must be a trusted operator or the bidder.
+    function withdrawFor(address bidder, uint amount) external {
+        require(
+          operators[bidder][msg.sender] || msg.sender == bidder,
+          "that operator was not allowed"
+        );
+        _withdraw(bidder, msg.sender, amount);
+    }
+
+    /// End the auction, transfer the NFT to the winning bidder, and the highest bid
+    /// amount to the seller.
+    /// @notice If there is no winner, the seller receives the NFT and not tokens.
+    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);
+    }
+
+}