hevm

https://hevm.dev
Admin
hevm is an implementation of the Ethereum Virtual Machine (EVM) focused on symbolic analysis,...
Tokens:20,348
Snippets:268
Trust Score:6
Update:2 months ago
Show doc for...
Tokens:
Raw
### Install dependencies and initialize project

Source: https://hevm.dev/getting-started.html

Commands to install Z3, Foundry, and initialize a project for Hevm testing.

```bash
$ sudo apt-get install z3  # install z3
$ curl -L https://foundry.paradigm.xyz | bash # install foundryup
$ foundryup # install forge and other foundry binaries
$ mkdir mytest && cd mytest
$ wget https://github.com/argotorg/hevm/releases/download/release/0.55.1/hevm-x86_64-linux
$ chmod +x ./hevm-x86_64-linux
$ forge init .
$ cat <<EOF > src/contract.sol
pragma solidity ^0.8.19;
import "forge-std/Test.sol";

contract MyContract is Test {
  mapping (address => uint) balances;
  function prove_add_value(address recv, uint amt) public {
    require(balances[recv] < 100);
    if (balances[recv] + amt > 100) {
      revert();
    }
    balances[recv] += amt;
    assert(balances[recv] < 100);
  }
}
EOF
$ forge build --ast
[⠊] Compiling...
[⠒] Compiling 1 files with 0.8.19
[⠢] Solc 0.8.19 finished in 14.27ms
Compiler run successful!
```

--------------------------------

### Sequence storage writes with SStore

Source: https://hevm.dev/architecture.html

Example of sequencing symbolic and concrete writes to storage starting from an EmptyStore state.

```text
(SStore (Lit 0) (Var "b") (Lit 1)
(SStore (Lit 0) (Lit 2) (Var "c")
EmptyStore))
```

--------------------------------

### Install Foundry

Source: https://hevm.dev/install.html

Use the official curl script to install the Foundry toolchain.

```bash
curl -L https://foundry.paradigm.xyz | bash
```

--------------------------------

### Install SMT Solvers on macOS

Source: https://hevm.dev/install.html

Install Z3 and cvc5 using Homebrew.

```bash
brew install z3
brew install --cask cvc5
```

--------------------------------

### Install SMT Solvers on Linux

Source: https://hevm.dev/install.html

Install Z3 and cvc5 using the apt package manager.

```bash
$ sudo apt-get install z3 cvc5
```

--------------------------------

### Install SMT Solvers

Source: https://hevm.dev/print.html

Install Z3 and cvc5 solvers required for symbolic execution.

```bash
$ sudo apt-get install z3 cvc5
```

```bash
brew install z3
brew install --cask cvc5
```

--------------------------------

### Echidna test contract setup

Source: https://hevm.dev/when-to-use.html

A minimal contract structure required for running Echidna fuzzing tests.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
 // the rest is the same
}
```

--------------------------------

### Compare EVM bytecode snippets

Source: https://hevm.dev/equivalence.html

Examples of EVM bytecode that are either equivalent or non-equivalent based on return data and execution status.

```evm
PUSH1 3
```

```evm
PUSH1 4
```

```evm
PUSH1 3
PUSH1 0x20
MSTORE
PUSH1 0x40
PUSH1 0x00
RETURN
```

```evm
PUSH1 4
PUSH1 0x20
MSTORE
PUSH1 0x40
PUSH1 0x00
RETURN
```

```evm
PUSH1 0x00
PUSH1 0x00
RETURN
```

```evm
PUSH1 0x00
PUSH1 0x00
REVERT
```

--------------------------------

### Symbolic execution example contract

Source: https://hevm.dev/architecture.html

A sample Solidity contract used to demonstrate symbolic execution and the resulting Expr End.

```solidity
contract MyContract {
  mapping(uint => uint) items;
  function test(uint val1) public {
    require(val1 > 10);
    unchecked {
      items[4] = val1+1;
      assert(items[4] > 10);
    }
  }
}
```

--------------------------------

### Define a test contract with setup and assertions

Source: https://hevm.dev/std-test-tutorial.html

Uses the Test contract to initialize a vault and verify state changes using cheat codes like vm.deal and vm.prank.

```solidity
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";

contract MyVault {
    mapping(address => uint256) public balance;
    function deposit() external payable {
        balance[msg.sender] += msg.value;
    }
}
contract MySetupTest is Test {
    MyVault vault;
    function setUp() public {
        vault = new MyVault();

        address user1 = address(42);
        vm.deal(user1, 7 ether);
        vm.prank(user1);
        vault.deposit{value: 7 ether}();
    }

    function prove_correct(uint8 amt) public {
        address k = address(42);
        uint pre = vault.balance(k);
        assert(pre == 7 ether);
        vm.prank(k);
        vault.deposit{value: amt}();
        assert(vault.balance(k) == pre + amt);
      }
}
```

--------------------------------

### Assembly Push Instruction

Source: https://hevm.dev/equivalence-checking-tutorial.html

Example of a PUSH32 instruction used in assembly.

```evm-assembly
PUSH32 0x0
```

```evm-assembly
PUSH32 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
```

--------------------------------

### Handle missing AST configuration error

Source: https://hevm.dev/std-test-tutorial.html

Example of the error message displayed when the AST flag is missing during compilation.

```text
Error: unable to parse Foundry project JSON: [...]/out/Base.sol/CommonBase.json Contract: "CommonBase"
```

--------------------------------

### hevm test

Source: https://hevm.dev/test.html

Executes unit tests for Foundry- and Dapptools-based projects on functions starting with prove_.

```APIDOC
## hevm test

### Description
Executes all unit tests that make use of the std-test assertion library on functions that start with prove_. This command supports both Foundry- and Dapptools-based projects.

### Usage
hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT] [--number W256] [--verb INT] [--match STRING] [--solver TEXT] [--num-solvers NATURAL] ...

### Parameters
- **--root** (STRING) - Optional - Project root directory.
- **--project-type** (PROJECTTYPE) - Optional - Type of project (Foundry or Dapptools).
- **--rpc** (TEXT) - Optional - RPC endpoint for testing.
- **--number** (W256) - Optional - Block number.
- **--verb** (INT) - Optional - Verbosity level.
- **--match** (STRING) - Optional - Filter tests by name.
- **--solver** (TEXT) - Optional - Solver configuration.
- **--num-solvers** (NATURAL) - Optional - Number of solvers to use.
```

--------------------------------

### Defining Custom Errors in Solidity

Source: https://hevm.dev/std-test-tutorial.html

Example of defining and reverting with a custom error when a balance check fails.

```solidity
error InsufficientBalance(uint256 requested, uint256 available);
....
uint reqested = ...;
uint available = ...;
if (requested > available) {
    revert InsufficientBalance(requested, available);
}
```

--------------------------------

### Define contracts for equivalence testing

Source: https://hevm.dev/equivalence.html

Example Solidity contracts used to demonstrate functional equivalence checking.

```solidity
contract MyContract {
  mapping (address => uint) balances;
  function my_adder(address recv, uint amt) public {
    if (balances[recv] + amt >= 100) { revert(); }
    balances[recv] += amt;
  }
}
```

```solidity
contract MyContract {
  mapping (address => uint) balances;
  function my_adder(address recv, uint amt) public {
    if (balances[recv] + amt >= 100) { revert(); }
    balances[recv] += amt/2;
    balances[recv] += amt/2;
  }
}
```

--------------------------------

### Get function signature with cast

Source: https://hevm.dev/symbolic-execution-tutorial.html

Retrieve the function signature hash using the cast tool from Foundry.

```bash
$ cast sig "simple_symb1()"
0x85c2fc71

$cast sig "simple_symb2()"
0x86ae3309
```

--------------------------------

### Raw Assembly Contract Example

Source: https://hevm.dev/equivalence-checking-tutorial.html

An assembly contract that multiplies the first byte of calldata by zero and returns the result.

```evm-assembly
PUSH1 0x00
CALLDATALOAD
PUSH1 0x00
MUL
PUSH1 0x00
MSTORE
PUSH1 0x01
PUSH1 0x00
RETURN
```

--------------------------------

### Define a Solidity contract for equivalence testing

Source: https://hevm.dev/equivalence-checking-tutorial.html

Example contract designed to handle odd-numbered amounts by incrementing the balance, intended for comparison with an existing contract.

```solidity
//SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;
contract MyContract {
  mapping (address => uint) balances;
  function my_adder(address recv, uint amt) public {
    if (balances[recv] + amt >= 100) { revert(); }
    balances[recv] += amt/2;
    balances[recv] += amt/2;
    if (amt % 2 != 0) balances[recv]++;
  }
}
```

--------------------------------

### Represent EVM branching with Expr End

Source: https://hevm.dev/architecture.html

Example of an Expr End list representing a program that branches based on the equality of two symbolic words.

```text
[ Success [PEq (Var "a") (Var "b")] ...,
, Failure [PNeg (PEq (Var "a") (Var "b"))] ...]
```

--------------------------------

### Symbolic execution loop limitation example

Source: https://hevm.dev/limitations-and-workarounds.html

A Solidity function containing a loop that is difficult to analyze symbolically when the iteration count is a symbolic parameter.

```solidity
function loop(uint n) {
  for(uint i = 0; i < n; i++) {
    mystate[i]++;
  }
}
```

--------------------------------

### Initialize a Foundry Project

Source: https://hevm.dev/std-test-tutorial.html

Create a new directory and initialize a project without git tracking.

```bash
mkdir myproject
cd myproject
forge init --no-git .
```

--------------------------------

### Compile and Run Tests

Source: https://hevm.dev/std-test-tutorial.html

Build the project with AST generation and execute the test using hevm.

```bash
$ forge build --ast
$ hevm test --match "prove_mytest"
Checking 1 function(s) in contract src/example-test.sol:Example
[RUNNING] prove_mytest(uint256)
   [PASS] prove_mytest(uint256)
```

--------------------------------

### hevm test usage help

Source: https://hevm.dev/test.html

Displays the command-line interface options and arguments for the hevm test command.

```text
Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
                 [--number W256] [--verb INT] [--match STRING]
                 [--solver TEXT] [--num-solvers NATURAL] ...
```

--------------------------------

### Define a test that reverts

Source: https://hevm.dev/std-test-tutorial.html

A contract example where all branches revert, causing hevm to report a failure.

```solidity
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract MyContract is Test {
  uint256 cntr;
  function prove_allrevert(uint256 val) public {
      if(val < 0) {
          unchecked { cntr = val; }
          revert();
      } else revert();
  }
}
```

--------------------------------

### Execute hevm with abstract storage

Source: https://hevm.dev/symbolic-execution-tutorial.html

Run symbolic execution with an empty initial storage configuration, which may reveal counterexamples due to abstract state exploration.

```bash
$ cabal hevm symbolic --initial-storage Empty --code "60806040523...."

Discovered the following counterexamples:

Calldata:
  0x881fc77c

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x1)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0
```

--------------------------------

### Compile Solidity contract to runtime bytecode

Source: https://hevm.dev/symbolic-execution-tutorial.html

Use solc to generate the runtime binary required for hevm execution.

```bash
solc --bin-runtime contract-symb-3.sol

======= contract-symb-3.sol:MyContract =======
Binary of the runtime part:
6080604052348015600e575f80fd5b50600436106026575f3560e01c806388....
```

--------------------------------

### Run Tests with hevm

Source: https://hevm.dev/install.html

Rebuild a Foundry project with AST generation and execute tests using hevm.

```bash
$ forge clean
$ forge build --ast
[⠒] Compiling...
[⠆] Compiling 34 files with 0.8.19
[⠔] Solc 0.8.19 finished in 2.12s
Compiler run successful.
$ hevm test
Checking 1 function(s) in contract src/contract-pass.sol:MyContract
[RUNNING] prove_pass(address,uint256)
   [PASS] prove_pass(address,uint256)
```

--------------------------------

### Compile contract with solc

Source: https://hevm.dev/symbolic-execution-tutorial.html

Generate the runtime binary for a Solidity contract using the solc compiler.

```bash
$ solc --bin-runtime contract-symb-1.sol
======= contract-symb-1.sol:MyContract =======
Binary:
6080604052348015600e575f80f....
```

```bash
$ solc --bin-runtime contract-symb-2.sol

======= contract-symb-2.sol:MyContract =======
Binary of the runtime part:
6080604052348015600e57....
```

--------------------------------

### Compile and execute symbolic analysis

Source: https://hevm.dev/symbolic-execution-tutorial.html

Use Forge to build the contract and Hevm to run symbolic execution on the deployed bytecode.

```bash
$ forge build --ast
[⠒] Compiling...
[⠢] Compiling 1 files with Solc 0.8.19
[⠆] Solc 0.8.19 finished in 11.46ms

$ hevm symbolic --code $(jq -r '.deployedBytecode.object' out/abs_storage.sol/AbsStorage.json )
Discovered the following 1 counterexample(s):

Calldata:
  0xb1712ffd

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x2)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0
```

--------------------------------

### Symbolic Execution Error Warning

Source: https://hevm.dev/limitations-and-workarounds.html

Example of the warning message generated by hevm when encountering symbolic arguments in restricted opcodes.

```text
WARNING: hevm was only able to partially explore the call prefix 0x[...] due to the following issue(s):
  - Attempting to transfer eth to a symbolic address that is not present in the state
```

--------------------------------

### Execute tests via command line

Source: https://hevm.dev/std-test-tutorial.html

Runs the test suite using the hevm CLI tool.

```bash
$ hevm test
Checking 1 function(s) in contract src/setup-test.sol:MySetupTest
[RUNNING] prove_correct(uint8)
   [PASS] prove_correct
```

--------------------------------

### Construct an ABI encoded call with Buf

Source: https://hevm.dev/architecture.html

Demonstrates using Buf expressions to represent an ABI encoded call to foo(uint256 a) by sequencing writes.

```text
(WriteWord (Lit 0x4) (Var "a")
(WriteByte (Lit 0x3) (LitByte 56)
(WriteByte (Lit 0x2) (LitByte 189)
(WriteByte (Lit 0x1) (LitByte 190)
(WriteByte (Lit 0x0) (LitByte 47)
(AbstractBuf "txdata")))))
```

--------------------------------

### Run Symbolic Execution

Source: https://hevm.dev/print.html

Execute hevm with different storage configurations to verify contract properties.

```bash
$ cabal hevm symbolic --initial-storage Empty --code "60806040523...."

Discovered the following counterexamples:

Calldata:
  0x881fc77c

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x1)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0
```

```bash
cabal run exe:hevm -- symbolic --initial-storage Empty --code "60806040...."

QED: No reachable property violations discovered
```

--------------------------------

### Run equivalence check on creation bytecode

Source: https://hevm.dev/equivalence.html

Compiles contracts using --bin and compares them using the --create flag.

```bash
solc --bin create1.sol | tail -n1 > create1.bin
solc --bin create2.sol | tail -n1 > create2.bin
hevm equivalence --code-a-file create1.bin --code-b-file create2.bin --create
```

--------------------------------

### Run Hevm test

Source: https://hevm.dev/getting-started.html

Execute the verification test using the Z3 solver.

```bash
$ hevm test --solver z3
Running 1 tests for src/contract.sol:MyContract
[FAIL] prove_add_value(address,uint256)
  Counterexample:
    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_add_value(0x0000000000000000000000000000000000000000,100)
```

--------------------------------

### Inspect symbolic execution branch models

Source: https://hevm.dev/symbolic-execution-tutorial.html

Use the --get-models flag to view detailed state information for branches, including failure conditions.

```text
=== Models for 8 branches ===
[...]

--- Branch ---

Inputs:

  Calldata:
    0xb1712ffd

  Storage:
    Addr SymAddr "entrypoint": [(0x0,0x2)]

  Transaction Context:
    TxValue: 0x0


End State:

  (Failure
    Error:
      (Revert
        (ConcreteBuf
          Length: 36 (0x24) bytes
          0000:   4e 48 7b 71  00 00 00 00  00 00 00 00  00 00 00 00   NH{q............
          0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
          0020:   00 00 00 01                                          ....
        )
      )
      [...]
)
```

--------------------------------

### Run hevm with Custom Root

Source: https://hevm.dev/std-test-tutorial.html

Execute hevm by specifying the project root directory if it is not in the global path.

```bash
./hevm test --root /path/to/foundry/project
```

--------------------------------

### Run Echidna fuzzer

Source: https://hevm.dev/when-to-use.html

Command to execute the Echidna fuzzer on a specific Solidity test file.

```bash
echidna --test-mode assertion src/multiply-test.sol
```

--------------------------------

### Profile hevm test suite

Source: https://hevm.dev/print.html

Run the test suite with profiling enabled to generate a time profile report in a .prof file.

```bash
cabal run test --enable-profiling -- +RTS -p
```

--------------------------------

### Define a sample Solidity contract for symbolic execution

Source: https://hevm.dev/symbolic-execution-tutorial.html

A simple contract with an assertion that can be tested using symbolic execution.

```solidity
contract AbsStorage {
    uint256 public a;
    function not2() public {
      assert(a != 2);
    }
}
```

--------------------------------

### Profile hevm application

Source: https://hevm.dev/for-hevm-developers.html

Build with profiling enabled and generate time profile reports using GHC runtime system flags.

```bash
cabal run test --enable-profiling -- +RTS -p
```

```bash
cabal run test --enable-profiling -- +RTS -p -RTS -p <test_to_profile>
```

--------------------------------

### Compare contract equivalence via CLI

Source: https://hevm.dev/print.html

Commands to verify equivalence between contracts using compiled bytecode or raw hex strings.

```bash
$ hevm equivalence \
    --code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
    --code-b $(solc --bin-runtime "contract3.sol" | tail -n1)
```

```bash
$ hevm equivalence --code-a "$(<a.txt)" --code-b "$(<b.txt)"
```

```bash
$ hevm equivalence --code-a "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212208c57ae04774d9ebae7d1d11f9d5e730075068bc7988d4c83c6fed85b7f062e7b64736f6c634300081a0033" --code-b "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220bd2f8a1ba281308f845e212d2b5eceab85e029909fa2409cdca7ede039bae26564736f6c634300081a0033"
```

--------------------------------

### Non-Equivalent Bytecode Check

Source: https://hevm.dev/equivalence-checking-tutorial.html

Command demonstrating the output when two bytecode sequences are not equivalent.

```bash
$ hevm equivalence --code-a "60003560000260005260016000f3" --code-b "7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60005260016000f3"
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
Not equivalent. The following inputs result in differing behaviours:
-----
Calldata:
  Empty
```

--------------------------------

### Run equivalence check on runtime bytecode

Source: https://hevm.dev/equivalence.html

Compiles two Solidity files and compares their runtime bytecode for functional equivalence.

```bash
solc --bin-runtime "contract1.sol" | tail -n1 > a.bin
solc --bin-runtime "contract2.sol" | tail -n1 > b.bin
hevm equivalence --code-a-file a.bin --code-b-file b.bin
```

--------------------------------

### Configure Foundry for AST generation

Source: https://hevm.dev/std-test-tutorial.html

Enable AST generation in foundry.toml to ensure hevm can parse the project JSON.

```toml
ast = true
```

--------------------------------

### Execute hevm with empty initial state

Source: https://hevm.dev/symbolic-execution-tutorial.html

Run symbolic execution ensuring the default storage value is zero, preventing the assertion failure.

```bash
cabal run exe:hevm -- symbolic --initial-storage Empty --code "60806040...."

QED: No reachable property violations discovered
```

--------------------------------

### Run equivalence check using solc output

Source: https://hevm.dev/equivalence-checking-tutorial.html

Compares two contracts by compiling them on the fly and passing the runtime bytecode to hevm.

```bash
$ hevm equivalence \
    --code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
    --code-b $(solc --bin-runtime "contract3.sol" | tail -n1)
Found 108 total pairs of endstates
Asking the SMT solver for 74 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found
```

--------------------------------

### View hevm equivalence usage

Source: https://hevm.dev/equivalence.html

Displays the command-line interface options for the equivalence checker.

```text
Usage: hevm equivalence [--code-a TEXT] [--code-b TEXT] [--code-a-file STRING]
                        [--code-b-file STRING] [--sig TEXT] [--arg STRING]...
                        [--calldata TEXT] [--smttimeout NATURAL]
                        [--max-iterations INTEGER] [--solver TEXT]
                        [--num-solvers NATURAL] ...
```

--------------------------------

### Instantiate specific function arguments

Source: https://hevm.dev/symbolic.html

Provides concrete values for specific function arguments while keeping others symbolic.

```bash
hevm symbolic --sig "transfer(address,uint256)" --arg 0x7cFA93148B0B13d88c1DcE8880bd4e175fb0DeDF --code $(<dstoken.bin-runtime)
```

```bash
hevm symbolic --sig "transfer(address,uint256)" --arg "<symbolic>" --arg 0 --code $(<dstoken.bin-runtime)
```

--------------------------------

### Execute hevm equivalence command

Source: https://hevm.dev/equivalence-checking-tutorial.html

Command to compare the runtime bytecode of two Solidity files using hevm.

```bash
$ hevm equivalence \
      --code-a $(solc --bin-runtime "contract1.sol" | tail -n1) \
      --code-b $(solc --bin-runtime "contract2.sol" | tail -n1)
Found 90 total pairs of endstates
Asking the SMT solver for 58 pairs
Reuse of previous queries was Useful in 0 cases
Not equivalent. The following inputs result in differing behaviours:
-----
Calldata:
  0xafc2c94900000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000023
Storage:
  Addr SymAddr "entrypoint": [(0x0,0x10)]
Transaction Context:
  TxValue: 0x0
```

--------------------------------

### Run Hevm symbolic execution

Source: https://hevm.dev/when-to-use.html

Command to run Hevm to find counterexamples for contract test cases.

```bash
$ hevm test
Checking 1 function(s) in contract src/multiply-test.sol:MyContract
[RUNNING] prove_multiply(uint256,uint256)
   [FAIL] prove_multiply(uint256,uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_multiply(9479,12583)

Checking 1 function(s) in contract src/overflow-test.sol:MyContract
[RUNNING] prove_overflow(uint256)
   [FAIL] prove_overflow(uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_overflow(00000000000000000000000000000000000000000000000100000000000000000182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)
```

--------------------------------

### hevm exec command usage

Source: https://hevm.dev/exec.html

Displays the full list of available flags and options for the hevm exec command.

```bash
Usage: hevm exec [--code ARG] [--code-file ARG] [--project-type ARG] [--create]
                 [--json-trace] [--address ARG] [--caller ARG] [--origin ARG]
                 [--coinbase ARG] [--value ARG] [--nonce ARG] [--gas ARG]
                 [--number ARG] [--timestamp ARG] [--basefee ARG]
                 [--priority-fee ARG] [--gaslimit ARG] [--gasprice ARG]
                 [--maxcodesize ARG] [--prev-randao ARG] [--chainid ARG]
                 [--rpc ARG] [--block ARG] [--ask-smt-iterations ARG]
                 [--loop-detection-heuristic ARG] [--no-decompose]
                 [--solver ARG] [--debug] [--calldata ARG] [--trace]
                 [--verb ARG] [--root ARG] [--assertion-type ARG]
                 [--smt-timeout ARG] [--smt-memory ARG] [--smtdebug]
                 [--dump-unsolved ARG] [--num-solvers ARG]
                 [--max-iterations ARG] [--promise-no-reent]
                 [--max-buf-size ARG] [--max-width ARG] [--max-depth ARG]
                 [--no-simplify] [--only-deployed] [--cache-dir ARG]
```

--------------------------------

### View hevm symbolic usage

Source: https://hevm.dev/symbolic.html

Displays the command-line interface options for the symbolic execution tool.

```bash
Usage: hevm symbolic [--code TEXT] [--code-file STRING] [--calldata TEXT] [--address ADDR]
                     [--caller ADDR] [--origin ADDR] [--coinbase ADDR]
                     [--value W256] [--nonce WORD64] [--gas WORD64]
                     [--number W256] [--timestamp W256] [--basefee W256] ...
```

--------------------------------

### Compare pre-compiled hex strings from files

Source: https://hevm.dev/equivalence-checking-tutorial.html

Reads hex-encoded bytecode from text files to perform the equivalence check.

```bash
$ hevm equivalence --code-a "$(<a.txt)" --code-b "$(<b.txt)"
```

--------------------------------

### Run tests with Cabal

Source: https://hevm.dev/for-hevm-developers.html

Execute the test suite using cabal, optionally with development flags or additional test runner parameters.

```bash
cabal run test
```

```bash
cabal run -f devel test
```

--------------------------------

### Configure QuickCheck test options

Source: https://hevm.dev/for-hevm-developers.html

Adjust the number of QuickCheck tests dynamically for test groups or individual properties.

```haskell
adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50))
```

```haskell
testProperty <property_name> $ withMaxSuccess 20 $ ...
```

--------------------------------

### Define create1.sol for creation code equivalence

Source: https://hevm.dev/print.html

Contract used to demonstrate creation code comparison.

```solidity
contract C {
  uint private immutable NUMBER;
  constructor(uint a) {
    NUMBER = 2;
  }
  function stuff(uint b) public returns (uint256) {
    unchecked {return 2+NUMBER+b;}
  }
}
```

--------------------------------

### Benchmark hevm performance

Source: https://hevm.dev/for-hevm-developers.html

Measure execution time and memory usage, or compare performance against a baseline CSV file.

```bash
# Measure time and memory usage
$ cabal run bench-perf -- +RTS -T

# Collect timings for a base version
$ cabal run bench-perf  -- --csv baseline.csv

# Perform some changes on the hevm code
# ...

# Benchmark changed code and compare with baseline
$ cabal run bench-perf  -- --baseline baseline.csv
```

--------------------------------

### Define a Test Contract

Source: https://hevm.dev/std-test-tutorial.html

Create a Solidity contract inheriting from Test, with test functions prefixed by prove_.

```solidity
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract Example is Test {
  function prove_mytest() public {
  // (1) environment setup, preconditions
  // (2) calls to test
  // (3) postcondition checks
  }
}
```

--------------------------------

### Define create2.sol for creation code equivalence

Source: https://hevm.dev/print.html

Contract used to demonstrate creation code comparison.

```solidity
contract C {
  uint private immutable NUMBER;
  constructor(uint a) {
    NUMBER = 4;
  }
  function stuff(uint b) public returns (uint256) {
    unchecked {return NUMBER+b;}
  }
}
```

--------------------------------

### Execute contract symbolically with hevm

Source: https://hevm.dev/symbolic-execution-tutorial.html

Run hevm in symbolic mode to identify potential assertion violations in the provided bytecode.

```bash
$ hevm symbolic --sig "simple_symb()" --code "6080604052348015...."

Discovered the following counterexamples:

Calldata:
  0x881fc77c

Storage:
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0
```

```bash
$ hevm symbolic --code "608060405234...."

Discovered the following counterexamples:

Calldata:
  0x85c2fc71

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0


Calldata:
  0x86ae3309

Storage:
  Addr SymAddr "entrypoint": [(0x0,0x0)]
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []

Transaction Context:
  TxValue: 0x0
```

--------------------------------

### Verify function signature with Cast

Source: https://hevm.dev/symbolic-execution-tutorial.html

Use the Cast tool to verify the function signature hash discovered by Hevm.

```bash
cast keccak "not2()"
0xb1712ffd...
```

--------------------------------

### Re-verify the corrected contract

Source: https://hevm.dev/getting-started.html

Re-build the project and run the verification test again to confirm the fix.

```bash
$ forge build --ast
[⠰] Compiling...
[⠔] Compiling 1 files with 0.8.19
[⠒] Solc 0.8.19 finished in 985.32ms
Compiler run successful!

$ hevm test --solver z3
Running 1 tests for src/contract.sol:MyContract
[PASS] prove_add_value(address,uint256)
```

--------------------------------

### Execute tests in a forge project

Source: https://hevm.dev/test.html

Runs tests within a project previously built with forge build --ast.

```bash
$ hevm test
Checking 1 function(s) in contract src/badvault-test.sol:BadVault
[RUNNING] prove_mytest(uint256)
   [PASS] prove_mytest(uint256)
```

--------------------------------

### Execute hevm test and view failure output

Source: https://hevm.dev/std-test-tutorial.html

Run hevm test to see the failure report and the specific calldata that triggered the revert.

```bash
$ hevm test
Checking 1 function(s) in contract src/contract-fail.sol:MyContract
[RUNNING] prove_single_fail(address,uint256)
   [FAIL] prove_single_fail(address,uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100)
```

--------------------------------

### Equivalence Check Command

Source: https://hevm.dev/equivalence-checking-tutorial.html

Command to compare two bytecode sequences for functional equivalence.

```bash
$ hevm equivalence --code-a "60003560000260005260016000f3" --code-b "7f000000000000000000000000000000000000000000000000000000000000000060005260016000f3"
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
No discrepancies found
```

--------------------------------

### Execute EVM bytecode

Source: https://hevm.dev/exec.html

Executes a specific sequence of EVM bytecode with a defined gas limit.

```bash
$ hevm exec --code 0x647175696e6550383480393834f3 --gas 0xff
"Return: 0x647175696e6550383480393834f3"
```

--------------------------------

### Profile specific tests with arguments

Source: https://hevm.dev/print.html

Pass arguments to the executable during profiling by using -RTS to terminate the RTS options.

```bash
cabal run test --enable-profiling -- +RTS -p -RTS -p <test_to_profile>
```

--------------------------------

### Compare hex strings directly in command line

Source: https://hevm.dev/equivalence-checking-tutorial.html

Passes raw hex strings directly as arguments to the equivalence command.

```bash
$ hevm equivalence --code-a "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212208c57ae04774d9ebae7d1d11f9d5e730075068bc7988d4c83c6fed85b7f062e7b64736f6c634300081a0033" --code-b "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220bd2f8a1ba281308f845e212d2b5eceab85e029909fa2409cdca7ede039bae26564736f6c634300081a0033"
```

--------------------------------

### Define a test with expected revert

Source: https://hevm.dev/std-test-tutorial.html

Use the proveFail_ prefix to indicate that a test is expected to revert, allowing it to pass.

```solidity
pragma solidity ^0.8.19;
import {Test} from "forge-std/Test.sol";
contract MyContract is Test {
  uint256 cntr;
  function proveFail_allrevert_expected(uint256 val) public {
      if(val < 0) {
          unchecked {
            cntr = val;
            cntr += 1;
          }
          revert();
      }
      else revert();
  }
}
```

--------------------------------

### Define contracts for creation code equivalence

Source: https://hevm.dev/equivalence.html

Solidity contracts demonstrating immutable state differences during creation.

```solidity
contract C {
  uint private immutable NUMBER;
  constructor(uint a) {
    NUMBER = 2;
  }
  function stuff(uint b) public returns (uint256) {
    unchecked {return 2+NUMBER+b;}
  }
}
```

```solidity
contract C {
  uint private immutable NUMBER;
  constructor(uint a) {
    NUMBER = 4;
  }
  function stuff(uint b) public returns (uint256) {
    unchecked {return NUMBER+b;}
  }
}
```
Tokens:
Raw