From 0f21d22e6ae6a834a38ca8686849c8ae843a6f24 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Tue, 6 Dec 2022 11:23:38 -0800
Subject: [PATCH 1/4] Add symbolic tests with Halmos

---
 .github/workflows/run_halmos.yml |  32 +++
 halmos/ERC721A.t.sol             | 378 +++++++++++++++++++++++++++++++
 2 files changed, 410 insertions(+)
 create mode 100644 .github/workflows/run_halmos.yml
 create mode 100644 halmos/ERC721A.t.sol

diff --git a/.github/workflows/run_halmos.yml b/.github/workflows/run_halmos.yml
new file mode 100644
index 000000000..1cd86482d
--- /dev/null
+++ b/.github/workflows/run_halmos.yml
@@ -0,0 +1,32 @@
+name: ERC721A CI - Halmos
+
+on:
+  push:
+    branches: [main]
+    paths-ignore:
+      - 'docs/**'
+      - '**.md'
+  pull_request:
+    branches: [main]
+    paths-ignore:
+      - 'docs/**'
+      - '**.md'
+
+jobs:
+  run-halmos:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Use Node.js 16.x
+        uses: actions/setup-node@v2
+        with:
+          node-version: 16.x
+      - name: Install dependencies
+        run: npm ci
+      - name: Install halmos
+        run: python3 -m pip install --upgrade halmos
+      - name: Run halmos
+        run: |
+          sed -i 's/\bprivate\b/internal/g' contracts/ERC721A.sol
+          cp halmos/ERC721A.t.sol contracts/
+          halmos
diff --git a/halmos/ERC721A.t.sol b/halmos/ERC721A.t.sol
new file mode 100644
index 000000000..239a98cc7
--- /dev/null
+++ b/halmos/ERC721A.t.sol
@@ -0,0 +1,378 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.4;
+
+import './ERC721A.sol';
+
+contract ERC721ATest is ERC721A {
+
+    constructor(string memory name_, string memory symbol_) ERC721A(name_, symbol_) { }
+
+    function isBurned(uint tokenId) public view returns (bool) {
+        return _packedOwnershipOf(tokenId) & _BITMASK_BURNED != 0;
+    }
+
+    //
+    // invariant
+    //
+
+    // inv1: the balance of the owner of an existing token is non-zero.
+    function inv1(uint tokenId) public view returns (bool) {
+        return !_exists(tokenId) || balanceOf(ownerOf(tokenId)) > 0;
+    }
+
+    // inv2: the ownership slot of unminted tokens is uninitialized.
+    function inv2(uint tokenId) public view returns (bool) {
+        return !(_packedOwnerships[tokenId] != 0) || tokenId < _nextTokenId();
+    }
+
+    // inv3: if the ownership slot is uninitialized, their parent token's _BITMASK_NEXT_INITIALIZED is unset.
+    function inv3(uint tokenId) public view returns (bool) {
+        return !(_packedOwnerships[tokenId] == 0) || _packedOwnershipOf(tokenId) & _BITMASK_NEXT_INITIALIZED == 0;
+    }
+
+    // inv4: if _BITMASK_NEXT_INITIALIZED is set, the ownership slot of the next token (if any) is initialized.
+    function inv4(uint tokenId) public view returns (bool) {
+        return !(_packedOwnershipOf(tokenId) & _BITMASK_NEXT_INITIALIZED != 0)
+            || !(tokenId + 1 < _nextTokenId())
+            || _packedOwnerships[tokenId + 1] != 0;
+    }
+
+    // inv5: the uninitialized token is not burned.
+    function inv5(uint tokenId) public view returns (bool) {
+        return !(_packedOwnerships[tokenId] == 0) || !isBurned(tokenId);
+    }
+
+    function testInvariant1(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv1(tokenId), addr1, addr2, num, rand); }
+    function testInvariant2(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv2(tokenId), addr1, addr2, num, rand); }
+    function testInvariant3(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv3(tokenId), addr1, addr2, num, rand); }
+    function testInvariant4(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv4(tokenId), addr1, addr2, num, rand); }
+    function testInvariant5(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv5(tokenId), addr1, addr2, num, rand); }
+
+    function _testInvariant(
+        bool inv,
+        address addr1, address addr2, uint num,
+        uint rand
+    ) internal {
+        require(inv);
+
+        if (rand == 0) {
+            mint(addr1, num);
+        } else if (rand == 1) {
+            burn(num);
+        } else {
+            transfer(addr1, addr2, num);
+        }
+
+        assert(inv);
+    }
+
+    //
+    // mint
+    //
+
+    // TODO: duplicate spec for _mintERC2309 and _safeMint
+    function mint(address to, uint quantity) public {
+        _mint(to, quantity);
+      //_mintERC2309(to, quantity);
+      //_safeMint(to, quantity);
+      //_safeMint(to, quantity, data);
+    }
+
+    function testMintRequirements(address to, uint quantity) public {
+        mint(to, quantity);
+
+        assert(to != address(0));
+        assert(quantity > 0);
+    }
+
+    function testMintNextTokenIdUpdate(address to, uint quantity) public {
+        uint oldNextTokenId = _nextTokenId();
+        require(oldNextTokenId <= type(uint96).max); // practical assumption needed for overflow/underflow not occurring
+
+        mint(to, quantity);
+
+        uint newNextTokenId = _nextTokenId();
+
+        assert(newNextTokenId >= oldNextTokenId); // ensuring no overflow
+        assert(newNextTokenId == oldNextTokenId + quantity);
+    }
+
+    function testMintBalanceUpdate(address to, uint quantity) public {
+        uint oldBalanceTo = balanceOf(to);
+        require(oldBalanceTo <= type(uint64).max / 2); // practical assumption needed for balance staying within uint64
+
+        mint(to, quantity);
+
+        uint newBalanceTo = balanceOf(to);
+
+        assert(newBalanceTo >= oldBalanceTo); // ensuring no overflow
+        assert(newBalanceTo == oldBalanceTo + quantity);
+    }
+
+    function testMintOwnershipUpdate(address to, uint quantity, uint _newNextTokenId) public {
+        uint oldNextTokenId = _nextTokenId();
+        require(oldNextTokenId <= type(uint96).max); // practical assumption needed for overflow/underflow not occurring
+
+        // local instances of inv2
+        for (uint i = oldNextTokenId; i < _newNextTokenId; i++) {
+            require(_packedOwnerships[i] == 0); // assumption for uninitialized mappings (i.e., no hash collision for hashed storage addresses)
+        }
+
+        mint(to, quantity);
+
+        uint newNextTokenId = _nextTokenId();
+        require(_newNextTokenId == newNextTokenId);
+
+        for (uint i = oldNextTokenId; i < newNextTokenId; i++) {
+            assert(ownerOf(i) == to);
+            assert(!isBurned(i));
+        }
+    }
+
+    function testMintOtherBalancePreservation(address to, uint quantity, address others) public {
+        require(others != to); // consider other addresses
+
+        uint oldBalanceOther = balanceOf(others);
+
+        mint(to, quantity);
+
+        uint newBalanceOther = balanceOf(others);
+
+        assert(newBalanceOther == oldBalanceOther); // the balance of other addresses never change
+    }
+
+    function testMintOtherOwnershipPreservation(address to, uint quantity, uint existingTokenId) public {
+        uint oldNextTokenId = _nextTokenId();
+        require(oldNextTokenId <= type(uint96).max); // practical assumption needed for overflow/underflow not occurring
+
+        require(existingTokenId < oldNextTokenId); // consider other token ids
+
+        address oldOwnerExisting = ownerOf(existingTokenId);
+        bool oldBurned = isBurned(existingTokenId);
+
+        mint(to, quantity);
+
+        address newOwnerExisting = ownerOf(existingTokenId);
+        bool newBurned = isBurned(existingTokenId);
+
+        assert(newOwnerExisting == oldOwnerExisting); // the owner of other token ids never change
+        assert(newBurned == oldBurned);
+    }
+
+    //
+    // burn
+    //
+
+    // TODO: duplicate spec for both modes
+    function burn(uint tokenId) public {
+      //_burn(tokenId, true);
+        _burn(tokenId, false);
+    }
+
+    function testBurnRequirements(uint tokenId) public {
+        require(inv2(tokenId));
+        require(inv5(tokenId));
+
+        bool exist = _exists(tokenId);
+        bool burned = isBurned(tokenId);
+
+        address owner = ownerOf(tokenId);
+        bool approved = msg.sender == _tokenApprovals[tokenId].value || isApprovedForAll(owner, msg.sender);
+
+        _burn(tokenId, true);
+
+        assert(exist); // it should have reverted if the token id does not exist
+        assert(!burned);
+
+        assert(msg.sender == owner || approved);
+
+        assert(_tokenApprovals[tokenId].value == address(0)); // getApproved(tokenId) reverts here
+    }
+
+    function testBurnNextTokenIdUnchanged(uint tokenId) public {
+        uint oldNextTokenId = _nextTokenId();
+
+        burn(tokenId);
+
+        uint newNextTokenId = _nextTokenId();
+
+        assert(newNextTokenId == oldNextTokenId);
+    }
+
+    function testBurnBalanceUpdate(uint tokenId) public {
+        require(inv1(tokenId));
+        require(inv2(tokenId));
+
+        address from = ownerOf(tokenId);
+        uint oldBalanceFrom = balanceOf(from);
+
+        burn(tokenId);
+
+        uint newBalanceFrom = balanceOf(from);
+
+        assert(newBalanceFrom < oldBalanceFrom); // ensuring no overflow
+        assert(newBalanceFrom == oldBalanceFrom - 1);
+    }
+
+    function testBurnOwnershipUpdate(uint tokenId) public {
+        burn(tokenId);
+
+        assert(!_exists(tokenId));
+        assert(_packedOwnerships[tokenId] & _BITMASK_BURNED != 0); // isBurned reverts here
+    }
+
+    function testBurnOtherBalancePreservation(uint tokenId, address others) public {
+        address from = ownerOf(tokenId);
+        require(others != from); // consider other addresses
+
+        uint oldBalanceOther = balanceOf(others);
+
+        burn(tokenId);
+
+        uint newBalanceOther = balanceOf(others);
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+
+    function testBurnOtherOwnershipPreservation(uint tokenId, uint otherTokenId) public {
+        require(inv2(tokenId));
+        require(inv3(tokenId));
+        require(inv4(tokenId));
+
+        require(_nextTokenId() <= type(uint96).max); // practical assumption needed for avoiding overflow/underflow
+
+        require(otherTokenId != tokenId); // consider other token ids
+
+        address oldOtherTokenOwner = ownerOf(otherTokenId);
+        bool oldBurned = isBurned(otherTokenId);
+
+        burn(tokenId);
+
+        address newOtherTokenOwner = ownerOf(otherTokenId);
+        bool newBurned = isBurned(otherTokenId);
+
+        assert(newOtherTokenOwner == oldOtherTokenOwner);
+        assert(newBurned == oldBurned);
+    }
+
+    //
+    // transfer
+    //
+
+    // TODO: duplicate spec for safeTransferFrom
+    function transfer(address from, address to, uint tokenId) public {
+        transferFrom(from, to, tokenId);
+      //safeTransferFrom(from, to, tokenId);
+      //safeTransferFrom(from, to, tokenId, data);
+    }
+
+    function testTransferRequirements(address from, address to, uint tokenId) public {
+        require(inv2(tokenId));
+        require(inv5(tokenId));
+
+        bool exist = _exists(tokenId);
+        bool burned = isBurned(tokenId);
+
+        address owner = ownerOf(tokenId);
+        bool approved = msg.sender == _tokenApprovals[tokenId].value || isApprovedForAll(owner, msg.sender);
+
+        transfer(from, to, tokenId);
+
+        assert(exist); // it should have reverted if the token id does not exist
+        assert(!burned);
+
+      //assert(from != address(0)); // NOTE: ERC721A doesn't explicitly check this condition
+        assert(to != address(0));
+
+        assert(from == owner);
+        assert(msg.sender == owner || approved);
+
+        assert(_tokenApprovals[tokenId].value == address(0));
+    }
+
+    function testTransferNextTokenIdUnchanged(address from, address to, uint tokenId) public {
+        uint oldNextTokenId = _nextTokenId();
+
+        transfer(from, to, tokenId);
+
+        uint newNextTokenId = _nextTokenId();
+
+        assert(newNextTokenId == oldNextTokenId);
+    }
+
+    function testTransferBalanceUpdate(address from, address to, uint tokenId) public {
+        require(inv1(tokenId));
+        require(inv2(tokenId));
+
+        require(from != to); // consider normal transfer case (see below for the self-transfer case)
+
+        uint oldBalanceFrom = balanceOf(from);
+        uint oldBalanceTo   = balanceOf(to);
+
+        require(oldBalanceTo <= type(uint64).max / 2); // practical assumption needed for balance staying within uint64
+
+        transfer(from, to, tokenId);
+
+        uint newBalanceFrom = balanceOf(from);
+        uint newBalanceTo   = balanceOf(to);
+
+        assert(newBalanceFrom < oldBalanceFrom);
+        assert(newBalanceFrom == oldBalanceFrom - 1);
+
+        assert(newBalanceTo > oldBalanceTo);
+        assert(newBalanceTo == oldBalanceTo + 1);
+    }
+
+    function testTransferBalanceUnchanged(address from, address to, uint tokenId) public {
+        require(from == to); // consider self-transfer case
+
+        uint oldBalance = balanceOf(from); // == balanceOf(to);
+
+        transfer(from, to, tokenId);
+
+        uint newBalance = balanceOf(from); // == balanceOf(to);
+
+        assert(newBalance == oldBalance);
+    }
+
+    function testTransferOwnershipUpdate(address from, address to, uint tokenId) public {
+        transfer(from, to, tokenId);
+
+        assert(ownerOf(tokenId) == to);
+        assert(!isBurned(tokenId));
+    }
+
+    function testTransferOtherBalancePreservation(address from, address to, uint tokenId, address others) public {
+        require(others != from); // consider other addresses
+        require(others != to);
+
+        uint oldBalanceOther = balanceOf(others);
+
+        transfer(from, to, tokenId);
+
+        uint newBalanceOther = balanceOf(others);
+
+        assert(newBalanceOther == oldBalanceOther);
+    }
+
+    function testTransferOtherOwnershipPreservation(address from, address to, uint tokenId, uint otherTokenId) public {
+        require(inv2(tokenId));
+        require(inv3(tokenId));
+        require(inv4(tokenId));
+
+        require(_nextTokenId() <= type(uint96).max); // practical assumption needed for avoiding overflow/underflow
+
+        require(otherTokenId != tokenId); // consider other token ids
+
+        address oldOtherTokenOwner = ownerOf(otherTokenId);
+        bool oldBurned = isBurned(otherTokenId);
+
+        transfer(from, to, tokenId);
+
+        address newOtherTokenOwner = ownerOf(otherTokenId);
+        bool newBurned = isBurned(otherTokenId);
+
+        assert(newOtherTokenOwner == oldOtherTokenOwner);
+        assert(newBurned == oldBurned);
+    }
+}

From 3e3d7b8840652b0e4ba206cc730b7bc3afc247f6 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Thu, 16 Feb 2023 18:23:51 -0800
Subject: [PATCH 2/4] Update Halmos tests for batched burn preparation

---
 halmos/ERC721A.t.sol | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/halmos/ERC721A.t.sol b/halmos/ERC721A.t.sol
index 239a98cc7..e45dfc238 100644
--- a/halmos/ERC721A.t.sol
+++ b/halmos/ERC721A.t.sol
@@ -37,16 +37,17 @@ contract ERC721ATest is ERC721A {
             || _packedOwnerships[tokenId + 1] != 0;
     }
 
+    /* this is no longer required since https://github.com/chiru-labs/ERC721A/pull/447
     // inv5: the uninitialized token is not burned.
     function inv5(uint tokenId) public view returns (bool) {
         return !(_packedOwnerships[tokenId] == 0) || !isBurned(tokenId);
     }
+    */
 
     function testInvariant1(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv1(tokenId), addr1, addr2, num, rand); }
     function testInvariant2(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv2(tokenId), addr1, addr2, num, rand); }
     function testInvariant3(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv3(tokenId), addr1, addr2, num, rand); }
     function testInvariant4(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv4(tokenId), addr1, addr2, num, rand); }
-    function testInvariant5(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv5(tokenId), addr1, addr2, num, rand); }
 
     function _testInvariant(
         bool inv,
@@ -171,7 +172,6 @@ contract ERC721ATest is ERC721A {
 
     function testBurnRequirements(uint tokenId) public {
         require(inv2(tokenId));
-        require(inv5(tokenId));
 
         bool exist = _exists(tokenId);
         bool burned = isBurned(tokenId);
@@ -268,7 +268,6 @@ contract ERC721ATest is ERC721A {
 
     function testTransferRequirements(address from, address to, uint tokenId) public {
         require(inv2(tokenId));
-        require(inv5(tokenId));
 
         bool exist = _exists(tokenId);
         bool burned = isBurned(tokenId);

From 0d7b2e46c0dac1e42cec509709a4a7b2ed2f6e91 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 17 Feb 2023 10:39:41 -0800
Subject: [PATCH 3/4] Split Halmos run into two

---
 .github/workflows/run_halmos.yml |  1 +
 halmos/ERC721A.t.sol             | 10 +++++-----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/run_halmos.yml b/.github/workflows/run_halmos.yml
index 1cd86482d..10ca2c50a 100644
--- a/.github/workflows/run_halmos.yml
+++ b/.github/workflows/run_halmos.yml
@@ -29,4 +29,5 @@ jobs:
         run: |
           sed -i 's/\bprivate\b/internal/g' contracts/ERC721A.sol
           cp halmos/ERC721A.t.sol contracts/
+          halmos --function prove
           halmos
diff --git a/halmos/ERC721A.t.sol b/halmos/ERC721A.t.sol
index e45dfc238..ef2e49ffb 100644
--- a/halmos/ERC721A.t.sol
+++ b/halmos/ERC721A.t.sol
@@ -44,12 +44,12 @@ contract ERC721ATest is ERC721A {
     }
     */
 
-    function testInvariant1(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv1(tokenId), addr1, addr2, num, rand); }
-    function testInvariant2(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv2(tokenId), addr1, addr2, num, rand); }
-    function testInvariant3(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv3(tokenId), addr1, addr2, num, rand); }
-    function testInvariant4(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _testInvariant(inv4(tokenId), addr1, addr2, num, rand); }
+    function proveInvariant1(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _proveInvariant(inv1(tokenId), addr1, addr2, num, rand); }
+    function proveInvariant2(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _proveInvariant(inv2(tokenId), addr1, addr2, num, rand); }
+    function proveInvariant3(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _proveInvariant(inv3(tokenId), addr1, addr2, num, rand); }
+    function proveInvariant4(uint tokenId, address addr1, address addr2, uint num, uint rand) public { _proveInvariant(inv4(tokenId), addr1, addr2, num, rand); }
 
-    function _testInvariant(
+    function _proveInvariant(
         bool inv,
         address addr1, address addr2, uint num,
         uint rand

From 6b8f2122ce35e1142f7947b1286116f92eceff8d Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 17 Feb 2023 11:09:30 -0800
Subject: [PATCH 4/4] Split Halmos runs

---
 .github/workflows/run_halmos.yml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/run_halmos.yml b/.github/workflows/run_halmos.yml
index 10ca2c50a..31b0ed15d 100644
--- a/.github/workflows/run_halmos.yml
+++ b/.github/workflows/run_halmos.yml
@@ -25,9 +25,15 @@ jobs:
         run: npm ci
       - name: Install halmos
         run: python3 -m pip install --upgrade halmos
-      - name: Run halmos
+      - name: Prepare for halmos
         run: |
           sed -i 's/\bprivate\b/internal/g' contracts/ERC721A.sol
           cp halmos/ERC721A.t.sol contracts/
-          halmos --function prove
-          halmos
+      - name: Run halmos - mint
+        run: halmos --function testMint
+      - name: Run halmos - burn
+        run: halmos --function testBurn
+      - name: Run halmos - transfer
+        run: halmos --function testTransfer
+      - name: Run halmos - invariant
+        run: halmos --function prove