diff --git a/.gitignore b/.gitignore index 3a5e7e7..937b7c7 100644 --- a/.gitignore +++ b/.gitignore @@ -14,7 +14,11 @@ docs/ # Dotenv file .env -#Fuzzers +# Fuzzers medusa echidna -crytic-export \ No newline at end of file +crytic-export +cloudexec.toml + +# Halmos +halmos-output.json diff --git a/.gitmodules b/.gitmodules index 1fea4e1..cbdcf10 100644 --- a/.gitmodules +++ b/.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 diff --git a/README.md b/README.md index 5dff99d..aaaea9c 100644 --- a/README.md +++ b/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: diff --git a/foundry.toml b/foundry.toml index 33723fa..2d9f839 100644 --- a/foundry.toml +++ b/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 diff --git a/lib/forge-std b/lib/forge-std index bb4ceea..ae570fe 160000 --- a/lib/forge-std +++ b/lib/forge-std @@ -1 +1 @@ -Subproject commit bb4ceea94d6f10eeb5b41dc2391c6c8bf8e734ef +Subproject commit ae570fec082bfe1c1f45b0acca4a2b4f84d345ce diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes new file mode 160000 index 0000000..c0d8655 --- /dev/null +++ b/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/remappings.txt b/remappings.txt deleted file mode 100644 index acd9c60..0000000 --- a/remappings.txt +++ /dev/null @@ -1,2 +0,0 @@ -forge-std/=lib/forge-std/src/ -@chimera/=lib/chimera/src/ \ No newline at end of file diff --git a/test/Counter.t.sol b/test/Counter.t.sol index 0422ad1..0189ea4 100644 --- a/test/Counter.t.sol +++ b/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); } } } diff --git a/test/recon/CryticTester.sol b/test/recon/CryticTester.sol index 332659e..f3f7a93 100644 --- a/test/recon/CryticTester.sol +++ b/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(); } diff --git a/test/recon/HalmosTargetFunctions.sol b/test/recon/HalmosTargetFunctions.sol new file mode 100644 index 0000000..9353d7e --- /dev/null +++ b/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); + } + } +} diff --git a/test/recon/HalmosTester.sol b/test/recon/HalmosTester.sol new file mode 100644 index 0000000..6f57df2 --- /dev/null +++ b/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(); + } +} diff --git a/test/recon/TargetFunctions.sol b/test/recon/TargetFunctions.sol index 3d77934..76836db 100644 --- a/test/recon/TargetFunctions.sol +++ b/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);