Merge pull request #4 from Certora/certora/erc1155ext

fix erc1155supply vacuity, change CI solc version to 8.4

.github/workflows/verify.yml

@@ -28,9 +28,9 @@ jobs:
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.2/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.4/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.2
+          sudo mv solc-static-linux /usr/local/bin/solc8.4
 
       - name: Verify rule ${{ matrix.script }}
         run: |

certora/harnesses/ERC1155/ERC1155SupplyHarness.sol

@@ -1,14 +1,61 @@
 import "../../munged/token/ERC1155/extensions/ERC1155Supply.sol";
 
+
 contract ERC1155SupplyHarness is ERC1155Supply {
-    constructor(string memory uri_)
-        ERC1155(uri_)
-    {}
+    address public owner;
+    constructor(string memory uri_) ERC1155(uri_) {
+        owner = msg.sender;
+    }
 
     // workaround for problem caused by `exists` being a CVL keyword
     function exists_wrapper(uint256 id) public view virtual returns (bool) {
         return exists(id);
     }
 
+    // These rules were not implemented in the base but there are changes in supply 
+    // that are affected by the internal contracts so we implemented them. We assume 
+    // only the owner can call any of these functions to be able to test them but also 
+    // limit false positives.
+
+    modifier onlyOwner {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function burn( address from, uint256 id, uint256 amount) public virtual onlyOwner {
+        _burn(from, id, amount);
+    }
+    function burnBatch(
+        address from,
+        uint256[] memory ids,
+        uint256[] memory amounts
+    ) public virtual onlyOwner {
+        _burnBatch(from, ids, amounts);
+    }
+
+    function mint(
+        address to,
+        uint256 id,
+        uint256 amount,
+        bytes memory data
+    ) public virtual onlyOwner {
+        _mint(to, id, amount, data);
+    }
+
+    function mintBatch(
+        address to,
+        uint256[] memory ids,
+        uint256[] memory amounts,
+        bytes memory data
+    ) public virtual onlyOwner { 
+        _mintBatch(to, ids, amounts, data);
+    }
+
+    // In order to check the invariant that zero address never holds any tokens, we need to remove the require
+    // from this function.
+    function balanceOf(address account, uint256 id) public view virtual override returns (uint256) {
+        // require(account != address(0), "ERC1155: address zero is not a valid owner");
+        return _balances[id][account];
+    }
 }
 

certora/scripts/Round3/verifyERC1155Burnable.sh

@@ -1,7 +1,7 @@
 certoraRun \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
-    --solc solc8.2 \
+    --solc solc8.4 \
     --optimistic_loop \
     --loop_iter 3 \
     --msg "ERC1155 Burnable verification all rules"

certora/scripts/Round3/verifyERC1155Pausable.sh

@@ -1,7 +1,7 @@
 certoraRun \
     certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
     --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
-    --solc solc8.2 \
+    --solc solc8.4 \
     --optimistic_loop \
     --loop_iter 3 \
     --msg "ERC1155 Pausable verification all rules"

certora/scripts/Round3/verifyERC1155Supply.sh

@@ -1,7 +1,7 @@
 certoraRun \
     certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
     --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
-    --solc solc8.2 \
+    --solc solc8.4 \
     --optimistic_loop \
     --loop_iter 3 \
     --msg "ERC1155 Supply verification all rules"

certora/scripts/Round3/verifyGovernorPreventLateQuorum.sh

@@ -1,7 +1,7 @@
 certoraRun \
     certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
-    --solc solc8.2 \
+    --solc solc8.4 \
     --optimistic_loop \
     --loop_iter 1 \
     --msg "GovernorPreventLateQuorum verification all rules" \

certora/scripts/Round3/verifyInitializable.sh

@@ -1,7 +1,7 @@
 certoraRun \
     certora/harnesses/InitializableComplexHarness.sol \
     --verify InitializableComplexHarness:certora/specs/Initializable.spec \
-    --solc solc8.2 \
+    --solc solc8.4 \
     --optimistic_loop \
     --loop_iter 3 \
     --msg "Initializable verificaiton all rules on complex harness" \

certora/specs/ERC1155Supply.spec

@@ -3,6 +3,7 @@ methods {
     totalSupply(uint256) returns uint256 envfree
     balanceOf(address, uint256) returns uint256 envfree
     exists_wrapper(uint256) returns bool envfree
+    owner() returns address envfree
 }
  
 /// given two different token ids, if totalSupply for one changes, then
@@ -19,6 +20,7 @@ filtered {
     uint256 token2_before = totalSupply(token2);
 
     env e; calldataarg args;
+    require e.msg.sender != owner(); // owner can call mintBatch and burnBatch in our harness
     f(e, args);
 
     uint256 token1_after = totalSupply(token1);