Halmos

.gitignore

@@ -14,7 +14,11 @@ docs/
 # Dotenv file
 .env
 
-#Fuzzers
+# Fuzzers
 medusa
 echidna
-crytic-export
+crytic-export
+cloudexec.toml
+
+# Halmos
+halmos-output.json

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "lib/chimera"]
 	path = lib/chimera
 	url = https://github.com/Recon-Fuzz/chimera
+[submodule "lib/halmos-cheatcodes"]
+	path = lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes

README.md

@@ -6,6 +6,7 @@
 - [Foundry Testing](#foundry-testing)
 - [Echidna Property Testing](#echidna-property-testing)
 - [Medusa Property Testing](#medusa-property-testing)
+- [Halmos Symbolic Execution Testing](#halmos-symbolic-exection)
 - [Uploading Fuzz Job To Recon](#uploading-fuzz-job-to-recon)
 
 This Foundry template allows you to bootstrap a fuzz testing suite using a scaffolding provided by the [Recon](https://getrecon.xyz/) tool.
@@ -61,6 +62,20 @@ To test only in property mode disable assertion mode using:
 
 in [medusa.json](https://github.com/Recon-Fuzz/create-chimera-app/blob/main/medusa.json).
 
+### Halmos Symbolic Exection
+
+Halmos uses symbolic execution to evaluate test cases for all possible input values.See more about this [here](https://github.com/a16z/halmos).
+
+To run halmos:
+
+```shell
+halmos --contract CryticTester --function invariant -vvv  
+```
+
+The two halmos tests implemented in `TargetFunctions` define stateless and stateful property tests, `check_increment` and `check_counter_symbolic`, respectively.
+
+In its normal usage, Halmos performs stateless symbolic execution on individual functions, however it can also be used for stateful invariant testing as is shown in the `check_counter_symbolic` function which uses symbolic values to call multiple target functions based on their selectors. This implementation is based on the example shown [here](https://a16zcrypto.com/posts/article/implementing-stateful-invariant-testing-with-halmos/).
+
 ## Uploading Fuzz Job To Recon
 
 You can offload your fuzzing job to Recon to run long duration jobs and share test results with collaborators using the [jobs page](https://getrecon.xyz/dashboard/jobs) on Recon:

foundry.toml

@@ -3,5 +3,10 @@ src = "src"
 out = "out"
 libs = ["lib"]
 no_match_contract = "CryticTester"
+remappings = [
+    "forge-std/=lib/forge-std/src/",
+    "@chimera/=lib/chimera/src/",
+    "halmos-cheatcodes=lib/halmos-cheatcodes/src/"
+]
 
 # See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options

test/Counter.t.sol

@@ -1,7 +1,9 @@
 // SPDX-License-Identifier: UNLICENSED
 pragma solidity ^0.8.13;
 
+import {Asserts} from "@chimera/Asserts.sol";
 import {Test, console} from "forge-std/Test.sol";
+
 import {Counter} from "../src/Counter.sol";
 
 contract CounterTest is Test {
@@ -11,15 +13,17 @@ contract CounterTest is Test {
         counter = new Counter();
     }
 
+    /// @notice foundry unit test
     function test_Increment() public {
         counter.increment();
         assertEq(counter.number(), 2);
     }
 
-    function testFuzz_SetNumber(uint256 x) public {
-        counter.setNumber(x);
-        if (x != 0) {
-            assertEq(counter.number(), x);
+    /// @notice foundry fuzz test
+    function testFuzz_SetNumber(uint256 newNumber) public {
+        counter.setNumber(newNumber);
+        if (newNumber != 0) {
+            assertEq(counter.number(), newNumber);
         }
     }
 }

test/recon/CryticTester.sol

@@ -2,11 +2,13 @@
 pragma solidity ^0.8.0;
 
 import {TargetFunctions} from "./TargetFunctions.sol";
+import {HalmosTargetFunctions} from "./HalmosTargetFunctions.sol";
 import {CryticAsserts} from "@chimera/CryticAsserts.sol";
 
-// echidna . --contract CryticTester --config echidna.yaml
-// medusa fuzz
-contract CryticTester is TargetFunctions, CryticAsserts {
+// Test with Echidna: echidna . --contract CryticTester --config echidna.yaml
+// Test with Medusa: medusa fuzz
+// Test with Halmos: halmos --contract CryticTester
+contract CryticTester is TargetFunctions, HalmosTargetFunctions, CryticAsserts {
     constructor() payable {
         setup();
     }

test/recon/HalmosTargetFunctions.sol

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: GPL-2.0
+pragma solidity ^0.8.0;
+
+import {BaseTargetFunctions} from "@chimera/BaseTargetFunctions.sol";
+import {vm} from "@chimera/Hevm.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
+import {BeforeAfter} from "./BeforeAfter.sol";
+import {Properties} from "./Properties.sol";
+
+abstract contract HalmosTargetFunctions is
+    BaseTargetFunctions,
+    Properties,
+    BeforeAfter,
+    SymTest
+{
+    ///@notice checks an individual target function
+    function invariant_increment(uint256 newNumber) public {
+        assumeSuccessfulCall(
+            address(counter),
+            calldataFor(counter.setNumber.selector, newNumber)
+        );
+
+        // if (newNumber != 0) {
+        eq(counter.number(), newNumber, "number != newNumber");
+        // }
+    }
+
+    ///@notice stateful symbolic execution test
+    ///@dev executes calls to multiple functions in the target contract then makes an assertion
+    function invariant_counter_symbolic(
+        bytes4[] memory selectors,
+        uint256 newNumber
+    ) public {
+        for (uint256 i = 0; i < selectors.length; ++i) {
+            assumeValidSelector(selectors[i]);
+            assumeSuccessfulCall(
+                address(counter),
+                calldataFor(selectors[i], newNumber)
+            );
+        }
+
+        t(counter.number() != 0, "number == 0");
+    }
+
+    ///@notice utility for returning the target functions selectors from the Counter contract
+    function assumeValidSelector(bytes4 selector) internal {
+        vm.assume(
+            selector == counter.setNumber.selector ||
+                selector == counter.increment.selector
+        );
+    }
+
+    ///@notice utility for making calls to the target contract
+    function assumeSuccessfulCall(address target, bytes memory data) internal {
+        (bool success, ) = target.call(data);
+        vm.assume(success);
+    }
+
+    ///@notice utility for getting calldata for a given function's arguments
+    function calldataFor(
+        bytes4 selector,
+        uint256 newValue
+    ) internal view returns (bytes memory) {
+        if (selector == counter.setNumber.selector) {
+            return abi.encodeWithSelector(selector, newValue);
+        } else if (selector == counter.increment.selector) {
+            return abi.encodeWithSelector(selector);
+        }
+    }
+}

test/recon/HalmosTester.sol

@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import {HalmosAsserts} from "@chimera/HalmosAsserts.sol";
+import {TargetFunctions} from "./TargetFunctions.sol";
+import {Setup} from "./Setup.sol";
+import {Counter} from "../../src/Counter.sol";
+import {Test} from "forge-std/Test.sol";
+
+contract HalmosTester is TargetFunctions, HalmosAsserts {
+    function setUp() public {
+        setup();
+    }
+}

test/recon/TargetFunctions.sol

@@ -2,32 +2,38 @@
 pragma solidity ^0.8.0;
 
 import {BaseTargetFunctions} from "@chimera/BaseTargetFunctions.sol";
+import {vm} from "@chimera/Hevm.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
 import {BeforeAfter} from "./BeforeAfter.sol";
 import {Properties} from "./Properties.sol";
-import {vm} from "@chimera/Hevm.sol";
 
 abstract contract TargetFunctions is
     BaseTargetFunctions,
     Properties,
-    BeforeAfter
+    BeforeAfter,
+    SymTest
 {
+    /**
+        Echidna/Medusa Target Functions 
+    */
     function counter_increment() public {
         counter.increment();
     }
 
+    ///@notice example assertion test replicating testFuzz_SetNumber
     function counter_setNumber1(uint256 newNumber) public {
-        // example assertion test replicating testFuzz_SetNumber
         try counter.setNumber(newNumber) {
             if (newNumber != 0) {
-                t(counter.number() == newNumber, "number != newNumber");
+                eq(counter.number(), newNumber, "number != newNumber");
             }
         } catch {
             t(false, "setNumber reverts");
         }
     }
 
+    ///@notice same example assertion test as counter_setNumber1 using ghost variables
     function counter_setNumber2(uint256 newNumber) public {
-        // same example assertion test as counter_setNumber1 using ghost variables
         __before();
 
         counter.setNumber(newNumber);