Merge branch 'main' into ci/add-venom-tests

pcaversaccio · Sep 19, 2024 · 21a1bcf · 21a1bcf
2 parents 5134939 + 7ed440d
commit 21a1bcf
Show file tree

Hide file tree

Showing 7 changed files with 97 additions and 136 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -18,6 +18,13 @@
   - [`eip712_domain_separator`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/utils/eip712_domain_separator.vy): Use relative `interfaces` `import`s. ([#263](https://github.com/pcaversaccio/snekmate/pull/263))
   - [`math`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/utils/math.vy): Use mutable `internal` function parameters. ([#267](https://github.com/pcaversaccio/snekmate/pull/267))
 
+### 🥢 Test Coverage
+
+- **Tokens**
+  - [`erc20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc20.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273))
+  - [`erc721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc721.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273))
+  - [`erc1155`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc1155.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273))
+
 ### 👀 Full Changelog
 
 - [`v0.1.0...v0.1.1`](https://github.com/pcaversaccio/snekmate/compare/v0.1.0...v0.1.1)

diff --git a/README.md b/README.md
@@ -215,7 +215,7 @@ Eventually, the [`halmos`](https://github.com/a16z/halmos)-based symbolic tests
 # Run Halmos ERC-721 symbolic tests. Be careful, this is a (very!) time-consuming operation.
 ~$ FOUNDRY_PROFILE=halmos halmos --contract ERC721TestHalmos --config test/halmos.toml
 
-# Run Halmos ERC-1155 symbolic tests. Be careful, this is a time-consuming operation.
+# Run Halmos ERC-1155 symbolic tests. Be careful, this is a (very!) time-consuming operation.
 ~$ FOUNDRY_PROFILE=halmos halmos --contract ERC1155TestHalmos --config test/halmos.toml
 
 # Run Halmos math symbolic tests.

diff --git a/test/halmos.toml b/test/halmos.toml
@@ -1,14 +1,16 @@
 [global]
 # Test settings.
-function = "testHalmos"       # Run tests matching the given prefix.
-storage-layout = "generic"    # Set the generic storage layout model.
-early-exit = true             # Stop after a counterexample is found.
-ffi = true                    # Enable the foreign function interface (ffi) cheatcode.
+function = "testHalmos"                # Run tests matching the given prefix.
+loop = 5                               # Set the loop unrolling bound.
+default-bytes-lengths = "0,32,96,1024" # Set the default length candidates for `bytes` and `string` types.
+storage-layout = "generic"             # Set the generic storage layout model.
+ffi = true                             # Enable the foreign function interface (ffi) cheatcode.
 
 # Debugging settings.
-statistics = true             # Print the statistics.
-verbose = 1                   # Set the verbosity level for the tests.
+verbose = 1                            # Set the verbosity level for the tests.
+statistics = true                      # Print the statistics.
+early-exit = true                      # Stop after a counterexample is found.
 
 # Solver settings.
-solver-command = "yices-smt2" # Use the Yices 2 SMT solver.
-cache-solver = true           # Cache unsatisfiable queries using unsatisfiable cores.
+solver-command = "yices-smt2"          # Use the Yices 2 SMT solver.
+cache-solver = true                    # Cache unsatisfiable queries using unsatisfiable cores.
diff --git a/test/tokens/halmos/ERC1155TestHalmos.t.sol b/test/tokens/halmos/ERC1155TestHalmos.t.sol
@@ -6,12 +6,13 @@ import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {VyperDeployer} from "utils/VyperDeployer.sol";
 
 import {IERC1155} from "openzeppelin/token/ERC1155/IERC1155.sol";
+import {IERC1155MetadataURI} from "openzeppelin/token/ERC1155/extensions/IERC1155MetadataURI.sol";
 
 import {IERC1155Extended} from "../interfaces/IERC1155Extended.sol";
 
 /**
- * @dev Sets the timeout (in milliseconds) for solving assertion
- * violation conditions; `0` means no timeout.
+ * @dev Set the timeout (in milliseconds) for solving assertion violation
+ * conditions; `0` means no timeout.
  * @custom:halmos --solver-timeout-assertion 0
  */
 contract ERC1155TestHalmos is Test, SymTest {
@@ -25,6 +26,11 @@ contract ERC1155TestHalmos is Test, SymTest {
     uint256[] private tokenIds;
     uint256[] private amounts;
 
+    /**
+     * @dev Set the timeout (in milliseconds) for solving branching conditions;
+     * `0` means no timeout.
+     * @custom:halmos --solver-timeout-branching 1000
+     */
     function setUp() public {
         bytes memory args = abi.encode(_BASE_URI);
         /**
@@ -124,25 +130,32 @@ contract ERC1155TestHalmos is Test, SymTest {
         vm.stopPrank();
     }
 
-    function testHalmosAssertNoBackdoor(
-        bytes4 selector,
-        address caller,
-        address other
-    ) public {
+    /**
+     * Set the length of the dynamically-sized arrays in the `IERC1155` interface.
+     * @custom:halmos --array-lengths ids=5,values=5,amounts=5
+     */
+    function testHalmosAssertNoBackdoor(address caller, address other) public {
+        /**
+         * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure`
+         * functions, we include read-only functions in the calldata creation.
+         */
+        bytes memory data = svm.createCalldata(
+            "IERC1155Extended.sol",
+            "IERC1155Extended",
+            true
+        );
+        bytes4 selector = bytes4(data);
+
         /**
          * @dev Using a single `assume` with conjunctions would result in the creation of
          * multiple paths, negatively impacting performance.
          */
         vm.assume(caller != other);
+        vm.assume(selector != IERC1155MetadataURI.uri.selector);
+        vm.assume(selector != IERC1155Extended.set_uri.selector);
         vm.assume(selector != IERC1155Extended._customMint.selector);
         vm.assume(selector != IERC1155Extended.safe_mint.selector);
         vm.assume(selector != IERC1155Extended.safe_mint_batch.selector);
-
-        /**
-         * @dev For convenience, ignore `view` functions that use dynamic arrays.
-         */
-        vm.assume(selector != IERC1155.balanceOfBatch.selector);
-
         for (uint256 i = 0; i < holders.length; i++) {
             vm.assume(!erc1155.isApprovedForAll(holders[i], caller));
         }
@@ -164,61 +177,8 @@ contract ERC1155TestHalmos is Test, SymTest {
         );
 
         vm.startPrank(caller);
-        bool success;
-        if (selector == IERC1155.safeTransferFrom.selector) {
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = token.call(
-                abi.encodeWithSelector(
-                    selector,
-                    svm.createAddress("owner"),
-                    svm.createAddress("to"),
-                    svm.createUint256("tokenId"),
-                    svm.createUint256("amount"),
-                    svm.createBytes(96, "YOLO")
-                )
-            );
-        } else if (
-            selector == IERC1155.safeBatchTransferFrom.selector ||
-            selector == IERC1155Extended.burn_batch.selector
-        ) {
-            uint256[] memory ids = new uint256[](5);
-            uint256[] memory values = new uint256[](5);
-            for (uint256 i = 0; i < ids.length; i++) {
-                ids[i] = svm.createUint256("ids");
-                values[i] = svm.createUint256("values");
-            }
-            bytes memory data = (selector ==
-                IERC1155.safeBatchTransferFrom.selector)
-                ? abi.encodeWithSelector(
-                    selector,
-                    svm.createAddress("owner"),
-                    svm.createAddress("to"),
-                    ids,
-                    values,
-                    svm.createBytes(96, "YOLO")
-                )
-                : abi.encodeWithSelector(
-                    selector,
-                    svm.createAddress("owner"),
-                    ids,
-                    values
-                );
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = token.call(data);
-        } else if (selector == IERC1155Extended.set_uri.selector) {
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = token.call(
-                abi.encodeWithSelector(
-                    selector,
-                    svm.createUint256("id"),
-                    svm.createBytes(96, "uri")
-                )
-            );
-        } else {
-            bytes memory args = svm.createBytes(1_024, "WAGMI");
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = address(token).call(abi.encodePacked(selector, args));
-        }
+        // solhint-disable-next-line avoid-low-level-calls
+        (bool success, ) = token.call(data);
         vm.assume(success);
         vm.stopPrank();
 

diff --git a/test/tokens/halmos/ERC20TestHalmos.t.sol b/test/tokens/halmos/ERC20TestHalmos.t.sol
@@ -8,8 +8,8 @@ import {VyperDeployer} from "utils/VyperDeployer.sol";
 import {IERC20} from "openzeppelin/token/ERC20/IERC20.sol";
 
 /**
- * @dev Sets the timeout (in milliseconds) for solving assertion
- * violation conditions; `0` means no timeout.
+ * @dev Set the timeout (in milliseconds) for solving assertion violation
+ * conditions; `0` means no timeout.
  * @custom:halmos --solver-timeout-assertion 0
  */
 contract ERC20TestHalmos is Test, SymTest {
@@ -25,8 +25,8 @@ contract ERC20TestHalmos is Test, SymTest {
     address[] private holders;
 
     /**
-     * @dev Sets timeout (in milliseconds) for solving branching
-     * conditions; `0` means no timeout.
+     * @dev Set the timeout (in milliseconds) for solving branching conditions;
+     * `0` means no timeout.
      * @custom:halmos --solver-timeout-branching 1000
      */
     function setUpSymbolic(uint256 initialSupply_) public {
@@ -86,20 +86,21 @@ contract ERC20TestHalmos is Test, SymTest {
      * @notice Forked and adjusted accordingly from here:
      * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC20/test/ERC20Test.sol.
      */
-    function testHalmosAssertNoBackdoor(
-        bytes4 selector,
-        address caller,
-        address other
-    ) public {
-        bytes memory args = svm.createBytes(1_024, "WAGMI");
+    function testHalmosAssertNoBackdoor(address caller, address other) public {
         vm.assume(other != caller);
 
         uint256 oldBalanceOther = erc20.balanceOf(other);
         uint256 oldAllowance = erc20.allowance(other, caller);
 
         vm.startPrank(caller);
         // solhint-disable-next-line avoid-low-level-calls
-        (bool success, ) = token.call(abi.encodePacked(selector, args));
+        (bool success, ) = token.call(
+            /**
+             * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure`
+             * functions, we include read-only functions in the calldata creation.
+             */
+            svm.createCalldata("IERC20Extended.sol", "IERC20Extended", true)
+        );
         vm.assume(success);
         vm.stopPrank();
 

diff --git a/test/tokens/halmos/ERC721TestHalmos.t.sol b/test/tokens/halmos/ERC721TestHalmos.t.sol
@@ -6,12 +6,13 @@ import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 import {VyperDeployer} from "utils/VyperDeployer.sol";
 
 import {IERC721} from "openzeppelin/token/ERC721/IERC721.sol";
+import {IERC721Metadata} from "openzeppelin/token/ERC721/extensions/IERC721Metadata.sol";
 
 import {IERC721Extended} from "../interfaces/IERC721Extended.sol";
 
 /**
- * @dev Sets the timeout (in milliseconds) for solving assertion
- * violation conditions; `0` means no timeout.
+ * @dev Set the timeout (in milliseconds) for solving assertion violation
+ * conditions; `0` means no timeout.
  * @custom:halmos --solver-timeout-assertion 0
  */
 contract ERC721TestHalmos is Test, SymTest {
@@ -29,8 +30,8 @@ contract ERC721TestHalmos is Test, SymTest {
     uint256[] private tokenIds;
 
     /**
-     * @dev Sets timeout (in milliseconds) for solving branching
-     * conditions; `0` means no timeout.
+     * @dev Set the timeout (in milliseconds) for solving branching conditions;
+     * `0` means no timeout.
      * @custom:halmos --solver-timeout-branching 1000
      */
     function setUp() public {
@@ -95,16 +96,24 @@ contract ERC721TestHalmos is Test, SymTest {
      * @notice Forked and adjusted accordingly from here:
      * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC721/test/ERC721Test.sol.
      */
-    function testHalmosAssertNoBackdoor(
-        bytes4 selector,
-        address caller,
-        address other
-    ) public {
+    function testHalmosAssertNoBackdoor(address caller, address other) public {
+        /**
+         * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure`
+         * functions, we include read-only functions in the calldata creation.
+         */
+        bytes memory data = svm.createCalldata(
+            "IERC721Extended.sol",
+            "IERC721Extended",
+            true
+        );
+        bytes4 selector = bytes4(data);
+
         /**
          * @dev Using a single `assume` with conjunctions would result in the creation of
          * multiple paths, negatively impacting performance.
          */
         vm.assume(caller != other);
+        vm.assume(selector != IERC721Metadata.tokenURI.selector);
         vm.assume(selector != IERC721Extended._customMint.selector);
         vm.assume(selector != IERC721Extended.safe_mint.selector);
         for (uint256 i = 0; i < holders.length; i++) {
@@ -118,26 +127,8 @@ contract ERC721TestHalmos is Test, SymTest {
         uint256 oldBalanceOther = erc721.balanceOf(other);
 
         vm.startPrank(caller);
-        bool success;
-        if (
-            selector ==
-            bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)"))
-        ) {
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = token.call(
-                abi.encodeWithSelector(
-                    selector,
-                    svm.createAddress("owner"),
-                    svm.createAddress("to"),
-                    svm.createUint256("tokenId"),
-                    svm.createBytes(96, "YOLO")
-                )
-            );
-        } else {
-            bytes memory args = svm.createBytes(1_024, "WAGMI");
-            // solhint-disable-next-line avoid-low-level-calls
-            (success, ) = address(token).call(abi.encodePacked(selector, args));
-        }
+        // solhint-disable-next-line avoid-low-level-calls
+        (bool success, ) = token.call(data);
         vm.assume(success);
         vm.stopPrank();