♻️ Use Native halmos createCalldata Cheat Code (#273)

### 🕓 Changelog [`halmos`](https://github.com/a16z/halmos) has released support for the following new cheat codes via PRs [#360](a16z/halmos#360) and (small patch) [#364](a16z/halmos#364): ```solidity createCalldata(string contractName); createCalldata(string contractName, bool includeViewFunctions); createCalldata(string filename, string contractName); createCalldata(string filename, string contractName, bool includeViewFunctions); ``` > Please note that `includeViewFunctions` defaults to `false`, if not provided. This PR refactors the `halmos`-based tests to capitalise on these new cheat codes. To verify the correct behaviour of the Vyper compiler for `view` and `pure` functions, we include read-only functions in the calldata creation. --------- Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
pcaversaccio · Sep 19, 2024 · c41d54c · c41d54c
1 parent 7f2aef7
commit c41d54c
Show file tree

Hide file tree

Showing 6 changed files with 96 additions and 135 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/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();
 

diff --git a/test/utils/halmos/MathTestHalmos.t.sol b/test/utils/halmos/MathTestHalmos.t.sol
@@ -11,8 +11,8 @@ import {FixedPointMathLib} from "solady/utils/FixedPointMathLib.sol";
 import {IMath} from "../interfaces/IMath.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 MathTestHalmos is Test, SymTest {
@@ -21,8 +21,8 @@ contract MathTestHalmos is Test, SymTest {
     IMath private math;
 
     /**
-     * @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 {
@@ -65,9 +65,9 @@ contract MathTestHalmos is Test, SymTest {
     }
 
     /**
-     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
-     * the queries of this test, where the Z3 solver is constantly running and consumes
-     * a lot of memory, causing the CI to crash due to out of memory.
+     * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not
+     * work for the queries of this test, where the Yices 2 SMT solver is constantly
+     * running and consumes a lot of memory, causing the CI to crash due to out of memory.
      */
     // function testHalmosAssertMulDiv(
     //     uint256 x,
@@ -112,27 +112,27 @@ contract MathTestHalmos is Test, SymTest {
     }
 
     /**
-     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
-     * the queries of this test, where the Z3 solver is constantly running and consumes
-     * a lot of memory, causing the CI to crash due to out of memory.
+     * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not
+     * work for the queries of this test, where the Yices 2 SMT solver is constantly
+     * running and consumes a lot of memory, causing the CI to crash due to out of memory.
      */
     // function testHalmosAssertWadLn(int256 x) public view {
     //     assertEq(math.wad_ln(x), FixedPointMathLib.lnWad(x));
     // }
 
     /**
-     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
-     * the queries of this test, where the Z3 solver is constantly running and consumes
-     * a lot of memory, causing the CI to crash due to out of memory.
+     * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not
+     * work for the queries of this test, where the Yices 2 SMT solver is constantly
+     * running and consumes a lot of memory, causing the CI to crash due to out of memory.
      */
     // function testHalmosAssertWadExp(int256 x) public view {
     //     assertEq(math.wad_exp(x), FixedPointMathLib.expWad(x));
     // }
 
     /**
-     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
-     * the queries of this test, where the Z3 solver is constantly running and consumes
-     * a lot of memory, causing the CI to crash due to out of memory.
+     * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not
+     * work for the queries of this test, where the Yices 2 SMT solver is constantly
+     * running and consumes a lot of memory, causing the CI to crash due to out of memory.
      */
     // function testHalmosAssertCbrt(uint256 x, bool roundup) public view {
     //     if (!roundup) {
@@ -146,9 +146,9 @@ contract MathTestHalmos is Test, SymTest {
     // }
 
     /**
-     * @dev Currently commented out, as the timeout for the Z3 solver does not work for
-     * the queries of this test, where the Z3 solver is constantly running and consumes
-     * a lot of memory, causing the CI to crash due to out of memory.
+     * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not
+     * work for the queries of this test, where the Yices 2 SMT solver is constantly
+     * running and consumes a lot of memory, causing the CI to crash due to out of memory.
      */
     // function testHalmosAssertWadCbrt(uint256 x) public view {
     //     assertEq(math.wad_cbrt(x), FixedPointMathLib.cbrtWad(x));