### Quick Start: Docker Image Setup and Solver Execution

Source: https://github.com/a16z/halmos/blob/main/packages/solvers/README.md

Follow these steps to pull the Docker image, tag it, and run individual solvers to check their versions. It also includes creating an SMT2 file and invoking each solver on it.

```sh
# Step 1: Pull the image
docker pull ghcr.io/a16z/solvers:latest

# Step 2: Tag the image with a shorter name
docker tag ghcr.io/a16z/solvers:latest solvers

# Step 3: Run the container using the shorter name,
for solver in bitwuzla boolector cvc5 stp yices z3 ; do \
    echo --- $solver && \
    docker run --rm solvers $solver --version ; \
done

# Step 4: create an example smt2 file:
cat << EOF > checkSanity.smt2
(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)
EOF

# Step 5: invoke each solver on the file
# (`-v .:/workspace` mounts the current working directory under /workspace on the container, making the files available there)
for solver in bitwuzla boolector cvc5 stp yices-smt2 z3 ; do \
    echo -n "$solver: " && \
    docker run --rm -v .:/workspace solvers $solver checkSanity.smt2 ; \
done
```

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

### Alternative Development Setup with pip

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Manual setup using Python's venv and pip for managing the virtual environment and dependencies. Includes installing pre-commit hooks.

```sh
python3.12 -m venv .venv && source .venv/bin/activate
```

```sh
python -m pip install -e ".[dev]"
```

```sh
pre-commit install
```

```sh
pre-commit run --all-files
```

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

### Install Halmos

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Installs Halmos using the `uv tool install` command. This is a quick way to get started if you haven't installed Halmos yet.

```sh
uv tool install halmos
```

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

### Set Up Development Environment with uv

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Steps to install uv and synchronize project dependencies, including development dependencies. Also covers installing and running pre-commit hooks.

```sh
curl -LsSf https://astral.sh/uv/install.sh | sh
```

```sh
uv sync --extra dev
```

```sh
uv run pre-commit install
```

```sh
uv run pre-commit run --all-files
```

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

### Symbolic Test Setup with Halmos

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Demonstrates how to write a `setUp()` function for symbolic testing with Halmos. It creates a `MyToken` contract instance with a symbolic initial supply using `svm.createUint256()`.

```solidity
import {SymTest} from "halmos-cheatcodes/SymTest.sol";
import {Test} from "forge-std/Test.sol";
import {MyToken} from "../src/MyToken.sol";

contract MyTokenTest is SymTest, Test {
    MyToken token;

    function setUp() public {
        uint256 initialSupply = svm.createUint256('initialSupply');
        token = new MyToken(initialSupply);
    }
}
```

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

### Install Halmos with uv

Source: https://github.com/a16z/halmos/blob/main/README.md

Installs the latest version of Halmos for the current user using the uv package manager. Ensure uv is installed first.

```sh
# install uv if you don't have it already
curl -LsSf https://astral.sh/uv/install.sh | sh

# install the latest version of halmos for the current user and add it to PATH
uv tool install --python 3.12 halmos

# or, install the development version from the repository
# uv tool install --python 3.12 git+https://github.com/a16z/halmos

# after installing, you can update halmos to the latest version with:
uv tool upgrade halmos
```

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

### Creating a Dynamic Array of Symbols

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This example demonstrates how to create a dynamic array of symbolic uint256 elements using a loop and svm.createUint256.

```solidity
uint256[] memory arr = new uint256[3];
for (uint i = 0; i < 3; i++) {
    arr[i] = svm.createUint256('element');
}
```

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

### Handle constructor pathing issues in Halmos

Source: https://github.com/a16z/halmos/wiki/errors

Halmos requires a single path from the constructor. Move complex logic to `setUp()` and use `vm.assume()` to prune unwanted paths, or run with `--solver-timeout-branching 0`.

```solidity
function check_NoBackdoor(bytes4 selector) {
    bytes memory args = svm.createBytes(1024, 'args');
    (bool success,) = address(token).call(abi.encodePacked(selector, args)); // may fail with the error "symbolic CALLDATALOAD offset"
}
```

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

### Install Halmos with pip

Source: https://github.com/a16z/halmos/blob/main/README.md

Installs Halmos using pip within a virtual environment. Requires manual management of Python versions and virtual environments.

```sh
# make sure you have a suitable python version installed, e.g.:
python3.12 --version

# create and activate a virtual environment with an explicit python version
python3.12 -m venv .venv && source .venv/bin/activate

# install the latest version of halmos
pip install halmos

# or, install the development version from the repository
pip install git+https://github.com/a16z/halmos
```

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

### Install Halmos Cheatcodes

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Installs the Halmos cheatcodes using the `forge install` command. This is necessary for using symbolic cheatcodes in your tests.

```sh
forge install a16z/halmos-cheatcodes
```

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

### Dynamically Creating Address Symbols

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This example demonstrates how to dynamically create symbolic address inputs within a test function using the svm.createAddress cheatcode.

```solidity
address sender = svm.createAddress("sender");
address receiver = svm.createAddress("receiver");
```

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

### Run Halmos Docker Container Interactively

Source: https://github.com/a16z/halmos/blob/main/packages/halmos/README.md

Start the Halmos Docker container interactively with a bash shell for debugging purposes. Mounts the current directory to /workspace.

```sh
# run the container interactively (for debugging)
docker run --rm -v .:/workspace -it --entrypoint bash halmos

```

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

### Define a simple contract for testing

Source: https://github.com/a16z/halmos/wiki/FAQ

This contract is used as an example for demonstrating mainnet forking simulation. It includes a simple state variable and a mapping.

```solidity
contract Counter {
    uint public total; // slot 0

    mapping (address => uint) public map; // slot 1

    function increment(address user) public {
        map[user]++;
        total++;
    }
}
```

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

### Run Halmos with Docker

Source: https://github.com/a16z/halmos/blob/main/README.md

Executes the Halmos Docker image, mounting the current directory as a workspace. This allows running Halmos without local installation.

```sh
cd /path/to/src

# mount '.' under /workspace in the container
docker run -v .:/workspace ghcr.io/a16z/halmos:latest
```

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

### Creating a Fixed-Size Bytes Array

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Halmos requires dynamically-sized arrays like bytes and string to be given a fixed size. This example shows how to create a bytes array of a specific size using svm.createBytes.

```solidity
bytes memory data = svm.createBytes(96, 'data');
```

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

### Symbolic Test for Token Transfer

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

An example symbolic test for a token transfer function. It includes specifying input conditions using vm.assume, recording balances, executing the transfer using vm.prank, and asserting the final balances.

```solidity
function check_transfer(address sender, address receiver, uint256 amount) public {
    // specify input conditions
    vm.assume(receiver != address(0));
    vm.assume(token.balanceOf(sender) >= amount);

    // record the current balance of sender and receiver
    uint256 balanceOfSender = token.balanceOf(sender);
    uint256 balanceOfReceiver = token.balanceOf(receiver);

    // call target contract
    vm.prank(sender);
    token.transfer(receiver, amount);

    // check output state
    assert(token.balanceOf(sender) == balanceOfSender - amount);
    assert(token.balanceOf(receiver) == balanceOfReceiver + amount);
}
```

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

### Avoid 'symbolic CALLDATALOAD offset' with explicit ERC721 arguments

Source: https://github.com/a16z/halmos/wiki/errors

When making arbitrary external calls, ensure dynamic array sizes are explicit. This example shows how to construct arguments for `safeTransferFrom` to avoid symbolic size issues.

```solidity
function check_NoBackdoor(bytes4 selector) {
    bytes memory args;
    if (selector == bytes4(0xb88d4fde)) { // bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)"))
        args = abi.encode(svm.createAddress('from'), svm.createAddress('to'), svm.createUint256('tokenId'), svm.createBytes(96, 'data'));
    } else {
        args = svm.createBytes(1024, 'args');
    }
    (bool success,) = address(token).call(abi.encodePacked(selector, args));
}
```

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

### Initialize storage slots for mainnet forking simulation

Source: https://github.com/a16z/halmos/wiki/FAQ

Demonstrates how to use `vm.store()` to set specific storage slot values for a mock contract, simulating mainnet state. Note that mapping slots must be hashed using `keccak256`.

```solidity
// counter.total = 12
vm.store(address(counter), bytes32(counter_total_slot), bytes32(uint(12)));

// counter.map[0x1001] = 7
vm.store(address(counter), keccak256(abi.encode(address(0x1001), counter_map_slot)), bytes32(uint(7)));

// counter.map[0x1002] = 5
vm.store(address(counter), keccak256(abi.encode(address(0x1002), counter_map_slot)), bytes32(uint(5)));
```

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

### Manually Update Environment with uv

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Instructions for manually synchronizing the environment and activating the virtual environment.

```sh
uv sync
```

```sh
source .venv/bin/activate
```

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

### Running Symbolic Testing with Halmos

Source: https://github.com/a16z/halmos/blob/main/examples/simple/README.md

This command initiates symbolic testing using Halmos to verify properties for all possible inputs within a given limit. It aims to find counterexamples that fuzz testing might miss.

```bash
$ halmos --function test
[FAIL] testTotalPriceBuggy(uint96,uint32) (paths: 6, time: 0.10s, bounds: [])
Counterexample: [p_price_uint96 = 39614081294025656978550816768, p_quantity_uint32 = 1073741824]
```

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

### Run Halmos and Tests with uv

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Commands to run the Halmos application and execute tests using uv.

```sh
uv run halmos
```

```sh
uv run pytest
```

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

### Run Halmos CLI

Source: https://github.com/a16z/halmos/blob/main/README.md

Executes the Halmos command-line tool from the project's root directory. Use --help for available options.

```sh
cd /path/to/src
halmos
```

```sh
halmos --help
```

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

### Run All Invariant Tests with Halmos

Source: https://github.com/a16z/halmos/blob/main/examples/invariants/README.md

Execute all invariant tests within the examples/invariants directory. This command is a simple way to run a comprehensive suite of tests.

```bash
cd examples/invariants

# Run all invariant tests
halmos
```

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

### Build Halmos Docker Image

Source: https://github.com/a16z/halmos/blob/main/packages/halmos/README.md

Build the Docker image for Halmos. Ensure you are in the root directory of the project.

```sh
# build it
docker build -t halmos --file packages/halmos/Dockerfile .

```

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

### Manage Dependencies with uv

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Commands for adding, removing, and updating project dependencies using uv.

```sh
uv add <dependency>
```

```sh
uv remove <dependency>
```

```sh
uv lock --upgrade-package <dependency>
```

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

### Call Target Contracts with vm.prank()

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Invoke target contract functions with symbolic inputs and set `msg.sender` using the `vm.prank()` cheatcode. This prepares the environment for testing contract interactions.

```solidity
vm.prank(sender);
token.transfer(receiver, amount);
```

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

### Download Halmos Docker Image

Source: https://github.com/a16z/halmos/blob/main/README.md

Pulls the latest pre-built Docker image containing Halmos and its dependencies.

```sh
docker pull ghcr.io/a16z/halmos:latest
```

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

### Define a dummy contract for vm.etch

Source: https://github.com/a16z/halmos/wiki/FAQ

An empty contract used as a placeholder when setting the bytecode of a mock contract using `vm.etch()`.

```solidity
contract EmptyContract { }
```

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

### Clone or Fork Halmos Repository

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Instructions for cloning the repository for local development or forking to submit pull requests.

```sh
gh repo fork a16z/halmos
```

```sh
git clone git@github.com:a16z/halmos.git
```

```sh
cd halmos
```

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

### Run Ruff Formatter

Source: https://github.com/a16z/halmos/blob/main/CONTRIBUTING.md

Command to manually run the Ruff code formatter on the source directory.

```sh
python -m ruff check src/
```

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

### Specify Valid Input Conditions with vm.assume()

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Use `vm.assume()` to filter out irrelevant or invalid input combinations in symbolic tests. This ensures that only inputs satisfying the specified conditions are considered, improving test efficiency.

```solidity
vm.assume(receiver != address(0));
vm.assume(token.balanceOf(sender) >= amount);
```

```solidity
uint256 tokenId = svm.createUint256("tokenId");

// ↑↑↑ don't do this
// tokenId = bound(tokenId, 1, MAX_TOKEN_ID);

// ↑↑↑ do this
vm.assume(1 <= tokenId && tokenId <= MAX_TOKEN_ID);
```

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

### Running Fuzz Testing with Forge

Source: https://github.com/a16z/halmos/blob/main/examples/simple/README.md

This command executes fuzz testing on the Solidity contract using the Forge testing framework. It runs a set of random inputs to check the defined properties.

```bash
$ forge test
[PASS] testTotalPriceBuggy(uint96,uint32) (runs: 256, μ: 462, ~: 466)
```

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

### Verify mock contract initialization

Source: https://github.com/a16z/halmos/wiki/FAQ

Asserts that the storage slots of the mock contract have been correctly initialized to the desired values, including checking default zero values for uninitialized slots.

```solidity
assertEq(counter.total(), 12);
assertEq(counter.map(address(0x1001)), 7);
assertEq(counter.map(address(0x1002)), 5);
assertEq(counter.map(address(0x1003)), 0); // uninitialized storage slots default to a zero value
```

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

### Test contract invariants with mock contract

Source: https://github.com/a16z/halmos/wiki/FAQ

Demonstrates testing contract invariants using a mock contract initialized for mainnet forking. This checks if a condition holds true for any user.

```solidity
assertLe(counter.map(user), counter.total());
```

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

### Structure of a Symbolic Test

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This is a general template for structuring symbolic tests in Halmos. It outlines the typical sections: specifying input conditions, calling target contracts, and checking output states.

```solidity
function check_<function-name>_<behavior-description> ( <parameters> ) {
    // specify input conditions
    ...

    // call target contracts
    ...

    // check output states
    ...
}
```

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

### Basic ERC20 Token Contract

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

A simple ERC20 token contract using OpenZeppelin's implementation. It includes a constructor that accepts an initial supply.

```solidity
import {ERC20} from "openzeppelin/token/ERC20/ERC20.sol";

contract MyToken is ERC20 {
    constructor(uint256 initialSupply) ERC20("MyToken", "MT") {
        _mint(msg.sender, initialSupply);
    }
}
```

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

### Use Low-Level Call for Revert Condition Checks

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Employ a low-level `call` for testing revert conditions, allowing execution to continue even if the external call fails. The `success` return value can be used to check for failures.

```solidity
vm.prank(sender);
(bool success,) = address(token).call(
    abi.encodeWithSelector(token.transfer.selector, receiver, amount)
);
if (!success) {
    // check conditions for transfer failure
}
```

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

### Declaring Symbolic Inputs for Transfer

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This snippet shows how input parameters are declared in a symbolic test. These parameters represent symbolic values that Halmos will explore.

```solidity
function check_transfer(address sender, address receiver, uint256 amount) ...
```

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

### Conceptual Effect of Symbolic Testing

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This code illustrates the conceptual effect of symbolic testing by showing an exhaustive loop over all possible input combinations. Note that this is computationally infeasible and symbolic execution is used instead.

```solidity
// conceptual effect of symbolic testing of `check_transfer()`
for (uint160 sender = 0; sender < type(uint160).max; sender++) {
    for (uint160 receiver = 0; receiver < type(uint160).max; receiver++) {
        for (uint256 amount = 0; amount < type(uint256).max; amount++) {
            check_transfer(address(sender), address(receiver), amount);
        }
    }
}
```

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

### Run Halmos Docker Container for Regression Tests

Source: https://github.com/a16z/halmos/blob/main/packages/halmos/README.md

Execute regression tests using the Halmos Docker container. Mounts the current directory to /workspace inside the container.

```sh
# run it
docker run --rm -v .:/workspace halmos --root tests/regression --function check_log_string

```

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

### Check Output States with Assertions

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Write assertions to verify the contract's output state after executing target functions. Halmos reports inputs that violate these assertions as counterexamples.

```solidity
assert(token.balanceOf(sender) == balanceOfSender - amount);
assert(token.balanceOf(receiver) == balanceOfReceiver + amount);
```

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

### Dynamically Creating Uint256 Symbol

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

This snippet shows how to dynamically create a symbolic uint256 input using the svm.createUint256 cheatcode.

```solidity
uint256 amount = svm.createUint256("amount");
```

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

### Adjust SMT Exponentiation by Constant

Source: https://github.com/a16z/halmos/wiki/warnings

If invalid counterexamples are generated due to nonlinear arithmetic, specifically exponentiation, you can adjust the SMT exponentiation by constant interpretation using --smt-exp-by-const N. N specifies the upper limit for constant powers.

```bash
--smt-exp-by-const N
```

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

### Run Specific Invariant Function with Halmos

Source: https://github.com/a16z/halmos/blob/main/examples/invariants/README.md

Execute a specific invariant function within a contract. This allows for granular testing of individual invariant properties.

```bash
# Run specific invariant
halmos --function invariant_sumOfBalancesEqualsTotalSupply
```

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

### Run Specific Invariant Test with Halmos

Source: https://github.com/a16z/halmos/blob/main/examples/invariants/README.md

Execute invariant tests for a specific contract. This is useful for focusing on a particular contract's invariants.

```bash
# Run specific test
halmos --contract ERC20Test
```

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

### Configure Halmos to eliminate solver nondeterminism

Source: https://github.com/a16z/halmos/wiki/FAQ

This command-line option disables the timeout for the branching solver, forcing it to complete its execution (sat or unsat) and thus improving determinism.

```bash
halmos --solver-timeout-branching 0
```

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

### Increase Loop Bound with --loop Option

Source: https://github.com/a16z/halmos/wiki/warnings

When Halmos hits a loop bound due to path explosion, you can try increasing this bound using the --loop option. Be aware that this may increase analysis time.

```bash
--loop
```

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

### Run Halmos Docker Container for Pytest

Source: https://github.com/a16z/halmos/blob/main/packages/halmos/README.md

Execute pytest within the Halmos Docker container to run specific tests. Mounts the current directory to /workspace.

```sh
# run tests
docker run -v .:/workspace --entrypoint pytest halmos -k test_config.py

```

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

### Define storage slot variables

Source: https://github.com/a16z/halmos/wiki/FAQ

These variables define the storage slot indices for the `Counter` contract's state variables, used in conjunction with `vm.store()`.

```solidity
uint counter_total_slot = 0;
uint counter_map_slot = 1;
```

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

### Solidity Property-Based Test for Contract Function

Source: https://github.com/a16z/halmos/blob/main/examples/simple/README.md

This Solidity test contract defines a property to check for the `totalPriceBuggy` function. It asserts that the calculated total price is always greater than or equal to the individual price when the quantity is not zero.

```solidity
contract ExampleTest is Example {
    function testTotalPriceBuggy(uint96 price, uint32 quantity) public pure {
        uint128 total = totalPriceBuggy(price, quantity);
        assert(quantity == 0 || total >= price);
    }
}
```

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

### Disable Assertion Solver Timeout

Source: https://github.com/a16z/halmos/wiki/warnings

To address 'counterexample-unknown' errors caused by assertion solver timeouts, you can increase the timeout or disable it entirely by setting --solver-timeout-assertion to 0.

```bash
--solver-timeout-assertion 0
```

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

### Custom Assertion for Older Compiler Versions

Source: https://github.com/a16z/halmos/blob/main/docs/getting-started.md

Implement a custom assertion function that reverts with `Panic(1)` for compatibility with older Solidity compiler versions (< 0.8.0) where assertion violations used the `INVALID` opcode.

```solidity
function myAssert(bool cond) internal pure {
    if (!cond) {
        assembly {
            mstore(0x00, 0x4e487b71) // Panic()
            mstore(0x20, 0x01)       // 1
            revert(0x1c, 0x24)       // revert Panic(1)
        }
    }
}
```

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

### Solidity Contract with a Buggy Type Cast

Source: https://github.com/a16z/halmos/blob/main/examples/simple/README.md

This Solidity contract contains a function with a potential bug due to incorrect type casting during multiplication. It's intended to be tested for correctness.

```solidity
contract Example {
    function totalPriceBuggy(uint96 price, uint32 quantity) public pure returns (uint128) {
        unchecked {
            return uint120(price) * quantity; // buggy type casting: uint120 vs uint128
        }
    }
}
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.