# Symbolic tests (Halmos)

Bounded symbolic execution of two small pure paths that the fuzzers cannot
exhaust: the Merkle claim binding in `PayoutDistributor` and the reveal
mapping in `Disorderly721`. Every argument of a `check_` function is a
symbolic value, so a passing check is a proof over the whole assumed range,
not a sample.

The tests are plain Solidity contracts (no forge-std); the only cheatcodes
used are `vm.assume`, `vm.deal` and `vm.store`. `contracts/foundry.toml`
points Foundry at the same sources, the same OpenZeppelin copy and the same
compiler settings as Hardhat; Hardhat remains the build and test system, and
`npm test` never compiles these files.

## Run

Halmos has no Windows build; its container carries Foundry. From
`contracts/`:

```sh
docker run --rm -v "$PWD:/work" -w /work ghcr.io/a16z/halmos:latest halmos --solver-timeout-assertion 0 --loop 4
```

On Windows Git Bash prefix with `MSYS_NO_PATHCONV=1` and give the mount as
`C:/.../contracts:/work`. `--loop 4` bounds OpenZeppelin's proof loop; the
tests use proofs of length 0 and 1 so the bound is never reached.

## Claim.t.sol - PayoutDistributor

| check | proves |
|---|---|
| `check_claim_bound_to_exact_triple` | with a one-leaf tree for (cycle, account, amount), the only claim that can succeed is that exact triple: another cycle, account or amount always reverts |
| `check_extra_proof_element_never_verifies` | a one-element proof against a one-leaf tree never verifies, for any sibling and any amount |
| `check_never_pays_beyond_funded_total` | a leaf larger than the funded total is refused (the overdraw guard), and a valid claim pays exactly the leaf, leaving `liabilities` and `claimed` exact |
| `check_two_leaves_independent` | in a two-leaf tree with different amounts, a leaf cannot be claimed with the other leaf's amount or proof, both legitimate claims succeed once, liabilities reach zero, and a second claim is refused |
| `check_two_leaves_equal_amounts` | in a two-leaf tree with the same amount for two accounts, a proof only verifies for its own account, each claims once, liabilities reach zero (added 2026-09-15) |

## Reveal.t.sol - Disorderly721.metadataId

Since 2026-09-15 each tier has its own offset, drawn from the committed
block hash modulo its own size (see `docs/AUDIT-BRIEF.md` section 5). The
offsets are written straight into storage (slots 12, 13 and 14 from
`forge inspect Disorderly721 storage-layout`, verified 2026-09-15) so every
pair the on-chain draw could produce is covered.

| check | proves |
|---|---|
| `check_identity_before_reveal` | before the draw the mapping is the identity for every valid id |
| `check_out_of_range_reverts` | ids 0 and above 1111 revert for every pair of offsets |
| `check_stays_in_tier` | for every council offset in [0, 100), every operator offset in [0, 1011) and every token, a council seat resolves into 1..100 and an operator into 101..1111 |
| `check_injective_in_tier` | for every pair of offsets, two different tokens in the same tier never share artwork; with the range property this is a bijection per tier |
| `check_tiers_independent` | an operator's artwork does not depend on the council offset: the two draws are independent by construction |

The earlier `observe_` functions (per-tier identity reachable for 12 of
1110 single indices) are retired with the single-index scheme: the identity
rotation is now one outcome of each tier's draw like any other, which is
what a fair shuffle requires, and no longer a guard that failed to hold.

These checks establish properties of the MAPPING for every offset pair.
They say nothing about the randomness source: that the offsets are
effectively uniform rests on the block hash being unpredictable at commit
time and on keccak256 behaving as a hash, the same assumptions the
commit-reveal design already makes.

## Claim.t.sol, change of 2026-09-15

The two-leaf check used to let the "wrong amount" attempt succeed when the
two symbolic amounts happened to be equal, which consumed the second
account's claim; the later legitimate claim then reverted outside a `try`
and Halmos pruned the path before the final assertions. It now assumes
unequal amounts, and `check_two_leaves_equal_amounts` covers the equal case
on its own. Found by the additional in-house AI review of the evidence
(2026-09-15).

## Result, 2026-09-15

Halmos image `ghcr.io/a16z/halmos` at digest
`sha256:4076f8929c2d32db7b2120feebb7dff256bb09de371db94c1fa41dd8c32dc0f6`
(Foundry 1.2.3, solc 0.8.24), contracts at the addendum commit. Log:
`docs/audits/fuzz-2026-09-15/halmos.log`.

| suite | checks | outcome | time |
|---|---|---|---|
| ClaimSymTest | 5 | all proved | 5.4 s |
| RevealSymTest | 5 | all proved | 26.9 s (the injectivity proof dominates) |

Bounds: claim amounts up to 50 ETH in the two-leaf checks and 100 ETH in
the single-leaf ones, one- and two-leaf trees, proofs of length 0 and 1.
The keccak function is modelled as collision-free, which is the standard
assumption. Nothing here covers trees of production size or the off-chain
builder; those are the fuzzing harnesses' and the rehearsals' job.

## Result, 2026-09-11 (previous scheme, kept for the record)

Halmos 0.1.dev1, Foundry 1.2.3, solc 0.8.24, contracts at commit `a44d93f`:
ClaimSymTest 4 checks proved in 3.6 s; RevealSymTest 4 checks proved in
83 s; the two observations found their counterexamples (800 and 1011).