# fizz Generate Echidna/Medusa-compatible Solidity fuzz suites from Foundry or Hardhat projects. Trigger on "fizz", "generate fuzz suite", "build fuzz harness", "stateful fuzzing", "fuzzing harness", "property testing", and "invariant suite". - **Kind:** skill - **Source:** https://github.com/pashov/skills - **Page:** https://forefy.com/skills/2ebae719-8e05-496e-9350-692ca825eede - **API (JSON + files):** https://forefy.com/api/asr/2ebae719-8e05-496e-9350-692ca825eede --- ## README.md # Fizz A full fuzz testing suite for your smart contracts in minutes, not weeks — works with any Foundry or Hardhat project, on both Echidna and Medusa. Built for: - **Solidity devs** who know they should fuzz but don't have weeks to set it up - **Security researchers** who want a full suite generated in minutes, not days ## What You Get One command produces: | Output | What's Inside | |--------|--------------| | `test/fizz/` | Full harness — setup, handlers, and invariants in plain, editable Solidity | | `PROPERTIES.md` | Every invariant in plain English, each with a stable ID and status | | `Reproduction tests` | A deterministic Foundry test for each distinct violation found | | `report.md` | Campaign summary — coverage reached and violations surfaced | ## Demo _Part of a Fizz run shown below_ ![Running Fizz in the terminal](../static/fizz.gif) ## Usage ``` Install https://github.com/pashov/skills/ and run fizz on the codebase ``` ``` Generate a fuzz suite for this lending protocol. Focus on solvency and liquidation invariants. ``` ``` update skill to latest version ``` ## Tips - **Run guided on first use.** Reviewing entry points and properties once shows exactly what the suite covers — then switch to automatic. - **Keep it in sync.** After changing contracts, run `/fizz-sync` to update the suite instead of regenerating it. - **Write properties in English.** Drop plain-English invariants into `PROPERTIES.md` and `/fizz-convert` turns them into Solidity. ## SKILL.md --- name: fizz description: Generate Echidna/Medusa-compatible Solidity fuzz suites from Foundry or Hardhat projects. Trigger on "fizz", "generate fuzz suite", "build fuzz harness", "stateful fuzzing", "fuzzing harness", "property testing", and "invariant suite". --- # Fizz Generate a stateful Solidity fuzz suite under `{SUITE_DIR}` (default: `test/fizz/`), with metadata and fuzzer runtime files under `{META_DIR}` (default: `fizz_data/`). Use `Echidna` and `Medusa` for invariant campaigns. Use `Foundry` for compilation, smoke testing, and quick debugging. ## Workflow Rules - Follow the steps in order. Do not skip forward if a required artifact for the current step does not exist yet. - If a step fails, stop there and report the blocker. - If tooling is missing, say exactly what was attempted and what is missing. - Keep the generated Solidity suite isolated under `test/fizz/` and the metadata/runtime files under `fizz_data/` unless the user explicitly asks for different paths. - Reuse existing project setup and test logic whenever possible; do not invent a deployment flow if the repo already has one. ## Parameters - `PROJECT_ROOT`: user-provided path, otherwise the current working directory. - `SKILL_PATH`: the directory containing this `SKILL.md`. - `SUITE_DIR`: `test/fizz` relative to `PROJECT_ROOT`. Pass `--suite-dir` to suite-generation steps. - `META_DIR`: `fizz_data` relative to `PROJECT_ROOT`. Pass `--meta-dir` to metadata steps. - Optional contract arguments narrow handler generation to specific contracts. - `--no-invariants` skips Step 9 only. - `--max` (or `--opus`, or "max quality") upgrades every subagent in this run from Sonnet to Opus. See "Subagent Model" below. - `--guided` / `--automatic` selects the run mode. See "Run Mode" below. ## Run Mode The skill runs in one of two modes, resolved once at the start of the run and reused for every checkpoint below: - `{MODE} = "guided"` — the parent agent pauses for user input at key checkpoints: Step 3 (additional docs), Step 4 (interactive function picker UI), Step 4.5 (cost confirmation), Step 6 (setup review), Step 8 (per-cycle coverage decision), Step 9c (property review), Step 10 (fuzzer choice). - `{MODE} = "automatic"` — the parent agent never pauses. Step 4 runs with `--auto`, Step 8 loops up to 3 coverage cycles then proceeds, Step 10 defaults to Medusa, and the cost estimate from Step 4.5 is printed but not gated on user confirmation. ### Resolving `{MODE}` - If the user invoked with `--guided` / "guided mode" / "walk me through" / "let me review" → `{MODE} = "guided"`. - If the user invoked with `--automatic` / `--auto` / "unguided" / "run the whole thing" / "no prompts" → `{MODE} = "automatic"`. - Otherwise, leave `{MODE}` unresolved; Step 0 asks for it via the selection prompt **after** printing the banner. Every subsequent instruction referencing `{MODE}` must substitute the resolved value. Do NOT switch modes mid-run. ## Subagent Model All subagents spawned by this skill (Step 3 fallback Protocol Analyzer, the 5 Step 9b discovery agents, the Step 9c Synthesizer, the 2 Step 9d Implementers, and the Step 11 Report Writer) default to **Sonnet** for cost and latency. The parent agent orchestrating the pipeline is whatever model the user's Claude Code session is running (this skill does not control it). Only the delegated subagents are covered by `{AGENT_MODEL}`. ### Resolving `{AGENT_MODEL}` Resolve once at the start of the run and reuse it for every spawn below: - If the user invoked with `--max` / `--opus` / "max quality" / "run on opus" / similar → `{AGENT_MODEL} = "opus"`. - If the user invoked with `--sonnet` / "use sonnet" / "default model" → `{AGENT_MODEL} = "sonnet"`. - Otherwise, leave `{AGENT_MODEL}` unresolved; Step 0 asks for it via the selection prompt **after** printing the banner. Every subsequent spawn instruction below references `{AGENT_MODEL}` — substitute the resolved value when making the actual tool call. Do NOT mix tiers within a single run. ## Step 0: Print Banner At the start of every skill run, **first** print this ASCII banner once before any other output — including any selection prompt: ```text ██████╗ █████╗ ███████╗██╗ ██╗ ██████╗ ██╗ ██╗ ███████╗██╗ ██╗██╗██╗ ██╗ ███████╗ ██╔══██╗██╔══██╗██╔════╝██║ ██║██╔═══██╗██║ ██║ ██╔════╝██║ ██╔╝██║██║ ██║ ██╔════╝ ██████╔╝███████║███████╗███████║██║ ██║██║ ██║ ███████╗█████╔╝ ██║██║ ██║ ███████╗ ██╔═══╝ ██╔══██║╚════██║██╔══██║██║ ██║╚██╗ ██╔╝ ╚════██║██╔═██╗ ██║██║ ██║ ╚════██║ ██║ ██║ ██║███████║██║ ██║╚██████╔╝ ╚████╔╝ ███████║██║ ██╗██║███████╗███████╗███████║ ╚═╝ ╚═╝ ╚═╝╚══════╝╚═╝ ╚═╝ ╚═════╝ ╚═══╝ ╚══════╝╚═╝ ╚═╝╚═╝╚══════╝╚══════╝╚══════╝ ``` After the banner, resolve `{MODE}` per the "Run Mode" section and `{AGENT_MODEL}` per the "Subagent Model" section. For any value still unresolved from invocation flags, ask the user via a single `AskUserQuestion` tool call containing only the unresolved questions (skip the call entirely if both were resolved from flags). **Output discipline (mandatory)**: Between the banner block and the `AskUserQuestion` invocation, emit **no user-facing text whatsoever** — no "I'll ask about…", no "loading the tool…", no acknowledgement that flags were missing. If `AskUserQuestion`'s schema needs to be fetched via `ToolSearch` first, do that silently as well. The user should see banner → selection UI → resolved-values lines, with nothing in between. This overrides the default behavior of narrating intent before tool calls. - **Question for `{MODE}`** — `header: "Run mode"`, `question: "How should I run?"`, options: - `label: "Automatic (Recommended)"`, `description: "Run end-to-end with no prompts."` - `label: "Guided"`, `description: "Pause at 7 checkpoints: extra docs, entry-point picker (browser UI), cost confirm, setup review, per-cycle coverage decision, property review, fuzzer choice."` - **Question for `{AGENT_MODEL}`** — `header: "Subagent model"`, `question: "Which model should drive the subagents?"`, options: - `label: "Sonnet (Recommended)"`, `description: "Default. Faster and cheaper for the 5 discovery agents, synthesizer, and 2 implementers."` - `label: "Opus"`, `description: "Higher quality but ~10× the cost. Equivalent to passing --max / --opus."` Map the user's selections back to `{MODE}` (`automatic` / `guided`) and `{AGENT_MODEL}` (`sonnet` / `opus`), then print these two lines so the resolved values are visible in transcript: - `Mode: guided` or `Mode: automatic` — the resolved `{MODE}`. - `Subagent model: sonnet` (default) or `Subagent model: opus (--max)` (if `--max` / `--opus` / "max quality" / "use opus" / Opus selection was requested). ## Step 1: Verify Tooling And Environment Run sequentially: 1. Read [template-map.md](./references/template-map.md). 2. Run `forge --version`. 3. If `forge --version` fails, tell the user that Foundry is missing and suggest installing it using the official documentation: Foundry install guide: `https://www.getfoundry.sh/introduction/installation` 4. If `forge --version` fails, stop here. Foundry is required before proceeding with the rest of the workflow. 5. Run `bash {SKILL_PATH}/scripts/ensure_foundry.sh {PROJECT_ROOT}`. 6. If `foundry.toml` is missing, allow `ensure_foundry.sh` to create one. If it fails, stop and report the error. 7. Run `medusa --version`. 8. Run `echidna --version`. 9. If either command fails, tell the user which tool is missing and suggest installing it using the official documentation: Medusa install guide: `https://secure-contracts.com/program-analysis/medusa/docs/src/getting_started/installation.html` Echidna install guide: `https://secure-contracts.com/program-analysis/echidna/introduction/installation.html` 10. If `medusa --version` fails, stop here. Medusa is required before proceeding with the rest of the workflow. 11. If `echidna --version` fails but Foundry and Medusa are installed, you may continue, but keep the installation recommendation in the user-facing summary because Echidna is still expected for the full workflow. ## Step 2: Compile And Extract Run sequentially: 1. Read `{PROJECT_ROOT}/foundry.toml`. 2. Run `cd {PROJECT_ROOT} && forge build`. 3. Run `node {SKILL_PATH}/scripts/extract_abis.js {PROJECT_ROOT} --meta-dir {META_DIR}`. ## Step 3: Understand The Protocol This step exists to drive setup, handler selection, and invariant generation quality. If `{MODE} = "guided"`, before touching any analysis source first ask the user: *"Any additional docs, links, whitepapers, spec files, or prior-audit notes I should consider? (paste paths or URLs, or reply 'none')"*. If the user provides anything, write the raw list to `{PROJECT_ROOT}/{META_DIR}/additional-context.md` (one entry per line, include URLs verbatim). Later sub-steps of this step — and Step 9a — must read that file if it exists and fold it into the protocol-understanding context. Start by checking whether `{PROJECT_ROOT}/x-ray/` exists and contains `x-ray.md`. `x-ray.md` is REQUIRED — without it, x-ray output is considered unavailable regardless of which other files are present. If `{PROJECT_ROOT}/x-ray/x-ray.md` exists, read it first as the primary project-understanding source. Then also read any of these supplementary files present in `{PROJECT_ROOT}/x-ray/`: If `{PROJECT_ROOT}/x-ray/x-ray.md` does NOT exist, you MUST run the **x-ray Acquisition Protocol** below. The Protocol Analyzer fallback (Attempt 4) is FORBIDDEN until Attempts 1–3 have each been executed and their outcomes recorded in `/tmp/x-ray-attempts.md`. "I think x-ray isn't available" is NOT a valid skip — only the recorded output of an actual tool/command counts. ### x-ray Acquisition Protocol Before Attempt 1, delete `/tmp/x-ray-attempts.md` if it exists (`rm -f /tmp/x-ray-attempts.md`) — stale entries from a previous run would falsely satisfy the Attempt 4 gate. Then create a fresh `/tmp/x-ray-attempts.md` and append one entry per attempt: timestamp, attempt name, command/tool invoked, exact output (or "no output"), outcome (`SUCCESS` / `FAILED: {reason}` / `SKIPPED: {reason}`). Attempt 4 requires the file to contain exactly 3 entries (one per Attempt 1, 2, 3) — `SKIPPED` entries count toward this total. - **Attempt 1 — invoke the skill.** Call the `x-ray` skill via the `Skill` tool with `args="{PROJECT_ROOT}"`. Do NOT pre-judge availability — invoke it. Only a runtime error of the form "skill not found" / "unknown skill" counts as unavailable. If it runs, wait for completion, then verify `{PROJECT_ROOT}/x-ray/x-ray.md` was written. If yes → SUCCESS, exit Protocol. - **Attempt 2 — install from the official source and re-invoke.** Run: ```bash git clone --depth 1 https://github.com/pashov/skills.git /tmp/pashov-skills-xray-install \ && mkdir -p ~/.claude/skills \ && cp -r /tmp/pashov-skills-xray-install/x-ray ~/.claude/skills/x-ray ``` Then re-invoke `Skill('x-ray', args="{PROJECT_ROOT}")`. If `{PROJECT_ROOT}/x-ray/x-ray.md` is produced → SUCCESS, exit Protocol. If the re-invocation still returns "skill not found" / "unknown skill" (auto-discovery did not pick up the freshly installed skill mid-session), do NOT mark this attempt failed yet — instead read `~/.claude/skills/x-ray/SKILL.md` (or `/tmp/pashov-skills-xray-install/x-ray/SKILL.md`) and execute its instructions inline against `{PROJECT_ROOT}`. If that produces `{PROJECT_ROOT}/x-ray/x-ray.md` → SUCCESS, exit Protocol. Only if ALL of (Skill re-invocation, inline execution) fail does this attempt count as FAILED. - **Attempt 3 — guided-mode user gate (guided only).** If `{MODE} = "guided"` AND Attempts 1–2 both failed, ASK the user: *"Could not obtain x-ray automatically (logs in `/tmp/x-ray-attempts.md`). Options: (a) paste an x-ray.md path, (b) authorize Protocol Analyzer fallback, (c) abort. Choose a/b/c."* Record their answer. If (a) and the file exists → copy to `{PROJECT_ROOT}/x-ray/x-ray.md`, SUCCESS. If (c) → halt the skill. Only (b) — explicit user authorization — permits Attempt 4. In `{MODE} = "automatic"`, skip this attempt and record `SKIPPED: automatic mode`. - **Attempt 4 — Protocol Analyzer fallback.** Permitted ONLY after Attempts 1–3 are recorded in `/tmp/x-ray-attempts.md` (with status FAILED, SKIPPED, or — for Attempt 3 only — `(b) authorized`). Before spawning, confirm the file exists and contains 3 entries; if not, GO BACK to the missing attempt — do not proceed. Fallback: Read `{SKILL_PATH}/agents/protocol-analyzer.md`, replace `{SKILL_PATH}` with the actual `{SKILL_PATH}`, `{PROJECT_ROOT}` with the actual `{PROJECT_ROOT}`, and `{META_DIR}` with the actual `{META_DIR}`, then spawn as a `general-purpose` agent with `model: "{AGENT_MODEL}"`. The agent reads the source files, then writes the analysis to `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md` so that later steps can read it back instead of relying on conversation context. From the `x-ray` documentation or `protocol-understanding.md` infer and summarize: - deployment order - constructor parameter meaning - required post-deploy initialization - actor roles and permissioned actions - approvals, liquidity, or other state needed before handlers will be useful - which external functions are real fuzzing entry points versus protocol-internal plumbing - candidate invariants to carry forward into Step 9 If something is still ambiguous after those reads, keep going with a conservative assumption and leave a targeted TODO later instead of guessing broadly. Do not plan full ghost-variable layouts, snapshot structs, or final implementation details here. Do record the likely invariants clearly so Step 9 can reuse them from `{PROJECT_ROOT}/x-ray/` or `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md` as its starting point. ## Step 4: Select Entry Points Read [selection-policy.md](./references/selection-policy.md). Create `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` as a filtered copy of `{PROJECT_ROOT}/{META_DIR}/contracts.json` that keeps the functions most likely to produce useful state transitions. Build the preselection from the protocol understanding gathered in Step 3 — primarily the x-ray entry-point map (if available) and source-level access control observations. If Step 3 produced an entry-point map with caller or access annotations, use that as the primary filter: exclude functions marked as internal-caller-only or contract-to-contract plumbing. Use `{PROJECT_ROOT}/{META_DIR}/contracts.json` only as the structural template for the output JSON format, not to decide which functions to include. Then run: - If `{MODE} = "automatic"`: `node {SKILL_PATH}/scripts/select_functions.js {PROJECT_ROOT} --contracts {PROJECT_ROOT}/{META_DIR}/contracts.json --selection {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json --meta-dir {META_DIR} --auto` - If `{MODE} = "guided"`: `node {SKILL_PATH}/scripts/select_functions.js {PROJECT_ROOT} --contracts {PROJECT_ROOT}/{META_DIR}/contracts.json --selection {PROJECT_ROOT}/{META_DIR}/entry-point-selection.json --meta-dir {META_DIR}` The `--auto` flag accepts the inferred selection and exits immediately. Without it, the script opens a browser UI with the inferred selection pre-checked so the user can adjust and confirm. Both paths write `entry-point-selection.json`. After the script completes, read `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json`. If the script exits before writing `entry-point-selection.json`, stop and report that failure. Print a short summary: - selected contracts - selected functions by contract - notable excluded functions ### Dispatcher for Low-Frequency Functions After reading the selection, classify the selected functions into two tiers: - **Primary**: core user flows that should be called frequently by the fuzzer (deposit, withdraw, mint, redeem, borrow, repay, swap, stake, unstake, claim, liquidate, etc.) - **Secondary**: less common functions that are still useful but should be called less often (admin setters, configuration changes, pause/unpause, role grants, parameter tuning, etc.) Write this classification to `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` by adding a `"tier": "primary"` or `"tier": "secondary"` field to each function entry. In Step 7, secondary-tier functions will be wrapped in a dispatcher handler that groups them behind a single entry point with an enum selector. This reduces call frequency naturally without excluding them entirely — the fuzzer picks a random selector value, so secondary functions get exercised occasionally but don't dominate the call sequence. If the user already excluded a function during selection, it stays excluded. The dispatcher is only for functions the user chose to keep but that should be deprioritized. `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` limits handler generation only. It does not limit the setup dependency graph. ## Step 4.5: Cost Estimate Run: `node {SKILL_PATH}/scripts/estimate_cost.js {PROJECT_ROOT} --meta-dir {META_DIR} --model {AGENT_MODEL} --mode {MODE}` The script reads `entry-point-selection.json`, applies a size bucket based on selected-function count, and writes `{PROJECT_ROOT}/{META_DIR}/cost-estimate.md` with a per-stage breakdown plus a total and an expected range. The numbers are Anthropic list-price ballparks; actual cost varies with coverage cycles, re-runs, and prompt-cache hit rate. Print the cost estimate table to the user. Then: - If `{MODE} = "automatic"`: continue to Step 5 without pausing. - If `{MODE} = "guided"`: ask the user *"Proceed with this estimate, or abort?"* and wait for confirmation before continuing. If the user aborts, stop the run and report where the artifacts so far were written. ## Step 5: Generate Scaffold Run: `node {SKILL_PATH}/scripts/generate_suite.js {PROJECT_ROOT} --suite-dir {SUITE_DIR} --meta-dir {META_DIR}` This copies the full template scaffold into `{PROJECT_ROOT}/{SUITE_DIR}/`, including core harness files and utility files such as `utils/MockERC20.sol`. It also writes the fuzzer config files (`echidna.yaml`, `medusa.json`) into `{PROJECT_ROOT}/`. It also reads `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` and generates one stub handler file per selected contract under `{PROJECT_ROOT}/{SUITE_DIR}/handlers/`. Those stubs include the clamped and unclamped section headers but no sample handler functions. `Handlers.sol` is scaffolded to import and inherit from all generated handler stubs. Treat the copied files as the starting point only. The next steps must modify them to fit the target protocol. ## Step 6: Modify Core Files And Wire Setup Read [setup-playbook.md](./references/setup-playbook.md) and [template-map.md](./references/template-map.md). Modify the scaffolded core files under `{PROJECT_ROOT}/{SUITE_DIR}/`. Use [template-map.md](./references/template-map.md) as the source of truth for the inheritance chain, file roles, and which scaffolded files are expected to be refined in this step versus later steps. Use [setup-playbook.md](./references/setup-playbook.md) as the source of truth for: - proxy and upgradeability detection - setup requirements and good defaults - mock-versus-real dependency choices - signature-dependent setup guidance - `Base.sol` integration points and TODO/FIXME policy When the target protocol depends on simple external ERC20s that are not part of the in-scope deployment graph, prefer the scaffolded `utils/MockERC20.sol` helper unless the project already includes a more faithful token mock. The key output of this step is a **compiling** scaffold with a realistic `Base.sol::setup()` function and the rest of the core scaffold adjusted to match it. If `{MODE} = "guided"`, after the edits to `Base.sol` are complete and before running `forge build`, print a **Setup Review** block summarising what was wired: - Contracts deployed in `setup()` (name + address variable + constructor args source) - Proxies detected and which implementation each wraps - Mocks vs real dependencies used, with the reason for each mock - Actors configured (addresses + role), and which ones the fuzzer will impersonate via handler caller selection - Seeded balances (token, recipient, amount) - Roles / access-control grants (role, grantee) - Approvals (token, owner, spender, amount) Then ask the user: *"Setup looks right? Reply 'proceed' to build, or tell me what to adjust."* If the user requests adjustments, apply them and re-print the review block; loop until they approve. In `{MODE} = "automatic"`, skip the review block and continue directly. Run `cd {PROJECT_ROOT} && forge build` before moving on. ## Step 7: Generate Handlers Read [handler-patterns.md](./references/handler-patterns.md). First, run the handler generation script to produce pre-populated stubs with correct function signatures and type mappings: `node {SKILL_PATH}/scripts/generate_handlers.js {PROJECT_ROOT} --suite-dir {SUITE_DIR} --meta-dir {META_DIR}` Then read these in parallel: - `{PROJECT_ROOT}/{SUITE_DIR}/handlers/Handlers.sol` - each generated `{PROJECT_ROOT}/{SUITE_DIR}/handlers/Handler.sol` - each selected contract source file Then refine the generated `{PROJECT_ROOT}/{SUITE_DIR}/handlers/Handler.sol` for the selected contracts. The stubs already contain correct signatures and clamping hints — focus on wiring the actual protocol calls, adding semantic clamping, and implementing boundary-value stress variants. Use [handler-patterns.md](./references/handler-patterns.md) as the source of truth for: - clamped versus unclamped handler structure - handler shaping and semantic action selection - caller context - clamping strategy - edge-case and signature-dependent handler guidance Update `Handlers.sol` to import and inherit from all generated handlers. Run `cd {PROJECT_ROOT} && forge build` and fix compile issues before moving on. ## Step 8: Reach Coverage With Medusa Before generating invariants, ensure the generated harness can drive enough protocol coverage under Medusa. ### Via-IR Coverage Deflation Handling When `via_ir = true` is set in `foundry.toml`, the Yul IR optimizer aggressively merges and eliminates branches. This deflates Medusa's coverage numbers — you may be at 85% source coverage but Medusa reports 65%. This must be handled before the first Medusa run. **Step 8.0: Detect and configure fuzz profile.** 1. Read `{PROJECT_ROOT}/foundry.toml` and check whether `via_ir = true` is set under `[profile.default]` or at the top level. 2. If `via_ir` is not enabled, skip this subsection — no fuzz profile is needed. 3. If `via_ir` is enabled, run: ``` bash {SKILL_PATH}/scripts/setup_fuzz_profile.sh {PROJECT_ROOT} ``` This script: - Appends a `[profile.fuzz]` section to `foundry.toml` with `via_ir = false` - Runs `FOUNDRY_PROFILE=fuzz forge build` - If compilation succeeds: exits 0, prints `FUZZ_PROFILE=no-ir` - If "stack too deep" error: retries with `via_ir = true` and `optimizer_runs = 0`, exits 0, prints `FUZZ_PROFILE=ir-no-opt` - If both fail: exits 1 (use default profile, accept deflated coverage) 4. Read the script output to determine the fuzz profile mode: - `FUZZ_PROFILE=no-ir` → accurate coverage, use standard targets - `FUZZ_PROFILE=ir-no-opt` → reduced deflation but still some; lower coverage targets by ~10% - Script failed → fall back to default profile; lower coverage targets by ~15-20% 5. Record the profile mode in `{PROJECT_ROOT}/{META_DIR}/coverage-targets.md` at the top: - `no-ir`: "Fuzz profile: via_ir disabled — coverage numbers are accurate" - `ir-no-opt`: "Fuzz profile: via_ir required (stack too deep), optimizer_runs=0 — coverage deflated ~10%, targets adjusted" - default fallback: "Fuzz profile: via_ir required with optimizer — coverage deflated ~15-20%, targets adjusted" 6. For all subsequent `forge build` commands in Steps 8–11, use: - `cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge build` (if fuzz profile was created) - `cd {PROJECT_ROOT} && forge build` (if no fuzz profile needed) Store the build command in a variable `{FUZZ_BUILD_CMD}` for reuse in later steps. ### Medusa Runs Every Medusa run in this step must use `run_medusa.js`, including reruns after harness changes. Do not switch to raw `medusa fuzz` for later cycles in this step. Before launching Medusa, rebuild with the fuzz profile if one was configured: ``` {FUZZ_BUILD_CMD} ``` Run the Medusa script asynchronously using the agent's command-execution tool. This is critical — do NOT use shell backgrounding (`&`), do NOT use `sleep` + `tail` to poll, and do NOT wait synchronously in a single blocking command. Start the process in a way the agent runtime can track and notify on completion. ``` node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --coverage-mode ``` The wrapper starts a temporary local browser log viewer and prints its URL, but does not open the browser by default. Read the viewer URL from the wrapper output and provide it to the user. Add `--logs` to the command only if the user asks for the viewer to open in their browser automatically. When the background command completes and you are notified, inspect the resulting coverage with focus on the core protocol contracts, not peripheral mocks or helper libraries. ### Dynamic Coverage Targets Not all contracts require the same coverage. Assign per-contract targets based on the contract's role: | Contract Role | Target (no-ir) | Target (ir-no-opt) | Target (ir fallback) | |---|---|---|---| | Core protocol logic (vault, pool, lending core, staking engine) | 80%+ | 70%+ | 65%+ | | Access control / role management | 60%+ | 50%+ | 45%+ | | Peripheral helpers (routers, views, adapters) | 50%+ | 40%+ | 35%+ | | Libraries and math utilities | Coverage inherited from callers | Same | Same | Use the column matching the fuzz profile mode determined in Step 8.0. After the first Medusa run, review the per-contract coverage report and classify each contract. If a contract has legitimately unreachable paths in the harness context (e.g., fork-only branches, multi-block MEV paths, oracle-failure paths), note them and adjust that contract's target downward rather than wasting cycles on unreachable code. Write the per-contract targets and any skip justifications to `{PROJECT_ROOT}/{META_DIR}/coverage-targets.md` so the user can review them. ### Coverage Iteration Loop - with `--coverage-mode`, the wrapper runs `medusa fuzz --timeout 300`, allows at least 60 seconds of fuzzing, then stops earlier if 5 consecutive progress lines show no increase in `branches hit`, and prints the coverage report path when finished (add `--logs` to also open it in the browser) - if coverage is below target, improve handler shapes, clamping, setup, approvals, seed balances, caller roles, and any missing lifecycle actions - when debugging why a specific handler or call sequence is not reaching the expected code paths, or when validating a hypothesis, use `FoundryTester.sol` to quickly PoC it - rerun `{FUZZ_BUILD_CMD}` before each new Medusa run - treat one cycle as: run `node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --coverage-mode`, inspect coverage, adjust the harness, then rebuild After each cycle, build and print a per-contract coverage summary table from the Medusa coverage report: | Contract | Role | Target | Hit | Status | |---|---|---|---|---| `Status` is `✅` if Hit ≥ Target, else `❌`. Append the same table to `{PROJECT_ROOT}/{META_DIR}/coverage-targets.md` under a timestamped `## Cycle N` heading so the history is preserved. Then branch on `{MODE}`: - `{MODE} = "automatic"`: if all contracts meet target, give a brief summary and proceed. Otherwise loop; cap at 3 cycles total, then log remaining gaps in `coverage-targets.md` and proceed to the next step with the current harness. - `{MODE} = "guided"`: after every cycle (including cycle 1), ask the user *"iterate / adjust targets / proceed"*. `iterate` = run another cycle with the current harness adjustments. `adjust targets` = let the user edit per-contract targets in `coverage-targets.md` before the next cycle. `proceed` = exit the loop regardless of gaps. Honour the user's choice; there is no hard cap in guided mode. After exiting the loop, provide the coverage report path for optional review: `{PROJECT_ROOT}/{META_DIR}/corpus_medusa/coverage/coverage_report.html`. ### Acceptable Skip Reasons It is acceptable to skip coverage for specific functions or paths when: - the function requires external state that cannot be simulated (e.g., specific oracle prices from a live feed) - the path is a revert-only guard that is intentionally unreachable in the harness (e.g., `require(msg.sender == bridgeContract)`) - the function is behind a time-lock or multi-sig that the harness doesn't simulate - the function interacts with an external protocol that is not mocked Document each skip in `{PROJECT_ROOT}/{META_DIR}/coverage-targets.md` with the reason. Do not move to invariant generation while Medusa coverage is still clearly too low for the selected flows, unless the user explicitly tells you to proceed anyway. ## Step 9: Generate Invariants (5 Parallel Discovery Agents + Synthesizer + 2 Implementers) Skip this step only when the user passed `--no-invariants`. This is the make-or-break step. It uses **5 specialized discovery agents in parallel**, each applying a different invariant discovery approach drawn from 50+ real DeFi bugs caught by fuzzers. ### Step 9a: Build Invariant Context Read [property-generation.md](./references/property-generation.md), then build `INVARIANT_CONTEXT` by reading: - the invariant notes captured in Step 3 from `{PROJECT_ROOT}/x-ray/x-ray.md` when available, otherwise `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md` - `{PROJECT_ROOT}/{META_DIR}/additional-context.md` if it exists (guided-mode supplementary docs/links from Step 3) - all in-scope source files - `Base.sol`, `Snapshots.sol`, `Properties.sol` - all generated handler files Extract from the codebase: - **AGGREGATE_VARIABLES**: grep for variables named `total*`, `sum*`, `accumulated*`, or any variable that multiple functions write to - **PAIRED_OPERATIONS**: match function pairs (deposit/withdraw, mint/burn, add/remove, lock/unlock, open/close, stake/unstake, borrow/repay, create/destroy, join/exit) - **CONVERSION_FUNCTIONS**: grep for `convertTo*`, `preview*`, `toAssets`, `toShares`, or any function mapping between two unit systems - **ACCESS_CONTROL**: grep for `onlyOwner`, `onlyAdmin`, `onlyRole`, `require(msg.sender`, custom role modifiers ### Step 9b: Spawn 5 Discovery Agents in Parallel **CRITICAL**: All 5 agents MUST be spawned in a SINGLE message (one tool call per agent, all in the same response). | Agent | File | Discovery Approach | |-------|------|-------------------| | 1. Conservation Auditor | `{SKILL_PATH}/agents/invariant-discovery/conservation-auditor.md` | Sum-of-parts = tracked-whole for every aggregate variable | | 2. Round-Trip & Rounding Analyst | `{SKILL_PATH}/agents/invariant-discovery/roundtrip-rounding-analyst.md` | Forward+inverse operations, directional rounding | | 3. State Transition Mapper | `{SKILL_PATH}/agents/invariant-discovery/state-transition-mapper.md` | Postconditions, monotonicity, entity counts, state machine | | 4. Adversarial Profit Maximizer | `{SKILL_PATH}/agents/invariant-discovery/adversarial-profit-maximizer.md` | Attacker thinking — DoS, value extraction, edge states | | 5. Protocol-Type Specialist | `{SKILL_PATH}/agents/invariant-discovery/protocol-type-specialist.md` | Auto-detect type, apply domain templates (vault/lending/AMM/etc.) | Read each agent file, replace `{INVARIANT_CONTEXT}` and `{FILE_PATHS}` with actual values, spawn as `general-purpose` agent with `model: "{AGENT_MODEL}"`. ### Step 9c: Synthesize Property Plan After all 5 agents return, read the Synthesizer agent file: | Agent | File | |-------|------| | 6. Synthesizer | `{SKILL_PATH}/agents/invariant-discovery/synthesizer.md` | Replace `{AGENT_OUTPUTS}` with the outputs from agents 1-5, `{META_DIR}` with the actual `{META_DIR}` path, `{PROJECT_ROOT}` with the actual `{PROJECT_ROOT}` path, and `{SUITE_DIR}` with the actual `{SUITE_DIR}` path, then spawn as `general-purpose` agent with `model: "{AGENT_MODEL}"`. The Synthesizer merges, deduplicates, prioritizes, and writes BOTH: - `{PROJECT_ROOT}/{META_DIR}/property-plan.md` — implementation tables with stable Spec IDs (`GL-NN`, `SP-NN`) - `{PROJECT_ROOT}/PROPERTIES.md` — English-language spec with `[ ]` checkboxes, one entry per property, identified by the same Spec IDs. This is the artifact that the `/fizz-convert` command and the implementers in Step 9d operate on. Each property carries a **Guarantee** tag set at generation time — `SHOULD-HOLD` (explicitly guaranteed by docs/spec/standard or an exact identity, with evidence cited) or `EXPLORATORY` (inferred). This tag is what lets Step 10 triage a violation without post-campaign severity guessing: a violated SHOULD-HOLD property is a confirmed bug, a violated EXPLORATORY property is a lead for human review. Print a summary: "Generated X properties (N HIGH, N MEDIUM, N LOW; P SHOULD-HOLD, Q EXPLORATORY)" with a brief list of the top properties by priority. If `{MODE} = "guided"`, pause here: tell the user the file path (`{PROJECT_ROOT}/PROPERTIES.md`), summarise what the Synthesizer produced, and ask *"Review `PROPERTIES.md` and edit freely — rename, add, remove, or reword properties. Keep the Spec IDs (`GL-NN` / `SP-NN`) on entries you want implemented, and leave `[ ]` checkboxes unchanged. Reply 'proceed' when done, or 'regenerate' to re-run the Synthesizer with additional guidance."* If they reply `regenerate`, ask what to change, then re-spawn the Synthesizer (Step 9c) with the extra guidance appended to its input. If they reply `proceed`, continue to Step 9d. In `{MODE} = "automatic"`, skip the pause and proceed directly. ### Step 9d: Implement Properties (2 Parallel Agents) Read each agent file: | Agent | File | Scope | |-------|------|-------| | 7A. Global Property Implementer | `{SKILL_PATH}/agents/implementers/global-property-implementer.md` | Ghosts in Base.sol, State in Snapshots.sol, global properties in Properties.sol, harness contracts if needed | | 7B. Specific Property Implementer | `{SKILL_PATH}/agents/implementers/specific-property-implementer.md` | Specific properties in Properties.sol, handler wiring (ghost updates + snapshot calls + property assertions) | Replace `{META_DIR}` with the actual `{META_DIR}` path, `{SKILL_PATH}` with the actual `{SKILL_PATH}` path, `{PROJECT_ROOT}` with the actual `{PROJECT_ROOT}` path, and `{SUITE_DIR}` with the actual `{SUITE_DIR}` path, then spawn both as `general-purpose` agents with `model: "{AGENT_MODEL}"` in parallel. Both implementers MUST flip `[ ]` → `[x]` in `{PROJECT_ROOT}/PROPERTIES.md` for each property they actually implement (matching by Spec ID `GL-NN` / `SP-NN`). Properties left as TODO stubs stay `[ ]` so `/fizz-convert` can pick them up later. ### Step 9e: Validate Run `{FUZZ_BUILD_CMD}` after the edits. Fix any compilation errors. If a property is low-confidence after implementation, prefer a commented TODO over a brittle assertion. ## Step 10: Run Campaigns After invariant generation and validation, run a full fuzzing campaign to find property violations. ### Fuzzer Selection - `{MODE} = "automatic"`: default to **Medusa** — faster with multi-worker parallelism and better suited for initial runs. - `{MODE} = "guided"`: ask the user *"Which fuzzer for this campaign — Medusa (default, parallel workers) or Echidna?"* and use their answer. If they express no preference, default to Medusa. Do not run both fuzzers simultaneously — this consumes excessive resources and can cause system instability or crashes. Campaign Iteration (below) is where a complementary run on the other fuzzer is offered. ### Running the Campaign Run the wrapper for the chosen fuzzer, either **Medusa** or **Echidna** (ONLY ONE), asynchronously using the agent's command-execution tool, then wait for that tracked background job to finish — the wrapper exits when the fuzzer's own stop condition triggers or the `--timeout` is reached. Both wrappers start a temporary local browser log viewer and print its URL, but do not open the browser by default; read the viewer URL from the wrapper output and provide it to the user. Add `--logs` to the command only if the user asks for the viewer to open in their browser automatically. For **Medusa**, run this command: ``` node {SKILL_PATH}/scripts/run_medusa.js {PROJECT_ROOT} --meta-dir {META_DIR} --timeout 600 ``` For **Echidna**, run this command: ``` node {SKILL_PATH}/scripts/run_echidna.js {PROJECT_ROOT} --meta-dir {META_DIR} --timeout 600 ``` If Echidna fails with `unlinked libraries detected in bytecode`, link the libraries in `echidna.yaml`: ```yaml deployContracts: [["0xf1", "Lib1"], ["0xf2", "Lib2"]] cryticArgs: ["--compile-libraries=(Lib1,0xf1), (Lib2,0xf2)"] ``` Replace `Lib1`, `Lib2` with the actual library names and `0xf1`, `0xf2` with the desired deployment addresses. ### Interpreting Results After the campaign completes: - check for property violations (failed assertions) - for each violation, extract the call sequence that triggered it - verify the violation is a real bug, not a harness issue — if the property or handler has a bug, fix it and rerun - **triage by the violated property's Guarantee tag** (from `PROPERTIES.md`): a violated **SHOULD-HOLD** property is a confirmed bug — the protocol broke a documented/mathematical guarantee, so report it as such; a violated **EXPLORATORY** property is flagged for human review — it may be a real bug or an over-strong inferred assumption, so present the call sequence and let a human judge rather than asserting a bug. Always rule out a harness/property bug first regardless of tag. - if no violations were found, report that the campaign completed cleanly with the coverage achieved - if violations were found, document each one with the failing property name, its Guarantee tag, the call sequence, and the contract state at failure ### Campaign Iteration If the user wants to explore further after the first campaign: - offer to run the other fuzzer (Echidna if Medusa was used, or vice versa) for a complementary pass - offer to increase the timeout or test limit - offer to adjust handler shapes based on coverage gaps observed during the campaign ## Step 11: Validate And Report Run: 1. `{FUZZ_BUILD_CMD}` 2. If `FoundryTester.sol` exists, `cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge test --match-contract FoundryTester` (or without `FOUNDRY_PROFILE` if no fuzz profile was created) If validation fails: - fix the specific broken files - do not regenerate the whole suite unless the user asks - limit repair retries to 3 cycles, then report the remaining issues cleanly ### Generate Violation Repros If the campaign in Step 10 found property violations, generate a Foundry reproduction test for each distinct violation in `FoundryTester.sol`. This turns fuzzer output into deterministic, one-command proof that the violation is real. **When to run**: only when `{PROJECT_ROOT}/{META_DIR}/corpus_medusa/test_results/` contains violation JSON files (Medusa) or the Echidna log contains `failed!` lines with call sequences. If the campaign found no violations, skip this sub-step entirely. **How to generate repros**: 1. Read each violation file (Medusa: one JSON per violation in `test_results/`; Echidna: parse call sequences from the log after each `failed!` line). 2. For each distinct violated property (group multiple reproductions of the same property — use only the shortest call sequence): - Create a `test_repro_()` function in `FoundryTester.sol`. - Replay the shrunk call sequence by calling the handler functions from the JSON `methodSignature` and `inputValues` fields directly. - Between calls, use `vm.roll()` and `vm.warp()` to advance block number and timestamp by the `blockNumberDelay` and `blockTimestampDelay` from each call entry. - The fuzzer's `from` addresses map to actors by index: `0x10000` → `actors[0]`, `0x20000` → `actors[1]`, `0x30000` → `actors[2]`. The clamped handlers accept an actor seed parameter that runs through `toActor()`, so pass the raw fuzzer input values — the seed modulus selects the right actor. - **Two violation patterns require different test structures**: - **Global property violations** (`property_*` functions that return `bool`): replay the full call sequence, then assert the property returns `false`: `assertFalse(property_xxx(), "property should be violated");`. The test **passes** when the property is violated. - **Inline assertion violations** (`_prop_*` / `_check*` assertions inside handlers that revert via `assert()` / `t()`): the violating handler call will revert with `panic(0x01)` before any post-call assertion can run. Wrap the violating call in `try this._repro_helperN() { revert("assertion should have fired"); } catch {}`, where `_repro_helperN()` is an `external` helper function that calls the handler. The `try/catch` proves the assertion fired. The test **passes** when the catch triggers. 3. Run `{FUZZ_BUILD_CMD}` and then `cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge test --match-contract FoundryTester -vvv` to confirm all repro tests pass. 4. If a repro test fails to compile or does not reproduce the violation, fix it (max 2 attempts per test). If it still fails, comment out the test body with a `// TODO: manual repro needed — fuzzer sequence did not reproduce under Foundry` note and move on. **Repro naming convention**: `test_repro_` (e.g., `test_repro_property_solvency`, `test_repro_prop_depositIncreasesShares`). If the same property was violated by multiple distinct root causes (different call sequences hitting different code paths), suffix with `_1`, `_2`. ### Final Report After validation succeeds, spawn the Report Writer subagent to synthesize the final report. Read `{SKILL_PATH}/agents/report-writer.md`, replace `{SKILL_PATH}` with the actual `{SKILL_PATH}`, `{PROJECT_ROOT}` with the actual `{PROJECT_ROOT}`, `{META_DIR}` with the actual `{META_DIR}`, and `{SUITE_DIR}` with the actual `{SUITE_DIR}`, then spawn as a `general-purpose` agent with `model: "{AGENT_MODEL}"`. The agent reads the campaign outputs (coverage, corpus, `medusa-run.log`, `PROPERTIES.md`, `Properties.sol`, handler files, open TODOs) and writes `{PROJECT_ROOT}/{META_DIR}/report.md`. The report-writer agent will also print the report content to the conversation (so the user sees it inline) and remind the user of the commands to run campaigns manually: - `medusa fuzz` (from project root) - `echidna . --contract FuzzTester --config echidna.yaml` ### Snapshot For Future Re-Use After the final report is written, capture a sync snapshot so the `/fizz-sync` skill can detect drift on subsequent source changes without re-running the full pipeline: ``` node {SKILL_PATH}/scripts/fizz_sync.js {PROJECT_ROOT} --init --meta-dir {META_DIR} --suite-dir {SUITE_DIR} ``` If the snapshot already exists (because a prior run already initialised it), re-run with `--refresh-snapshot` instead so the new baseline reflects the current state: ``` node {SKILL_PATH}/scripts/fizz_sync.js {PROJECT_ROOT} --refresh-snapshot --meta-dir {META_DIR} --suite-dir {SUITE_DIR} ``` This writes `{PROJECT_ROOT}/{META_DIR}/last-run.json` — a hash+signature snapshot of the in-scope contracts, handlers, and `PROPERTIES.md` entries. Later, when the user modifies sources and invokes `/fizz-sync`, that skill diffs against this file to detect added/removed/changed functions, quarantine stale properties, and regenerate only the drifted handler stubs. ## VERSION ``` ``` ## agents ``` ``` ## agents/implementers ``` ``` ## agents/implementers/global-property-implementer.md # Agent 7A: Global Property & Ghost/Snapshot Implementer **Role**: Implement global properties into Properties.sol, wire ghost variables into Base.sol, and populate Snapshots.sol. These are checked by the fuzzer after every handler call. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned in parallel with Agent 7B. --- ## Prompt You implement the GLOBAL properties and the ghost/snapshot infrastructure from the property plan. ## Your Inputs - Read: `{SKILL_PATH}/references/property-generation.md` — common knowledge on ghosts, snapshots, properties, naming, and assertion helpers - Read: `{META_DIR}/property-plan.md` — implement ONLY Global Properties section - Read: Ghost Variable Plan and Snapshot State Plan sections - Read + Edit: `{SUITE_DIR}/Base.sol` (add ghost variables to Ghosts struct) - Read + Edit: `{SUITE_DIR}/Snapshots.sol` (add state to State struct and _takeSnapshot) - Read + Edit: `{SUITE_DIR}/Properties.sol` (add global property functions) - Read + Edit: `{PROJECT_ROOT}/PROPERTIES.md` (flip `[ ]` → `[x]` for each GL-* property you actually implement with a real assertion; flip `[ ]` → `[-]` for any GL-* property you skip or leave as a TODO/commented stub — `[-]` means "do not auto-touch", so `/fizz-convert` will not retry it later) - Read: `{SUITE_DIR}/handlers/` (all handler files — for context on what operations exist) - Read: Source contract files (for actual function signatures and state variables) ## Implementation Rules These rules expand on the general property implementation instructions in `property-generation.md` with specifics for the global properties and wiring. Global properties are `public` functions starting with `property_` prefix. The fuzzer calls them directly after every handler. ### MANDATORY: Spec ID doctag Every property function you write MUST have its Spec ID as the first thing in its natspec, on its own line, in this exact form: ```solidity /// @notice GL-NN: function property_() public { ... } ``` The `GL-NN:` token (with the colon) is how `/fizz-convert` and future runs locate the existing implementation of a Spec ID for re-generation or deletion. Without it, automation cannot reconcile the spec with the code. This is a hard requirement, not a style preference. ```solidity // ―――――――――――――――――――― Global properties ――――――――――――――――――――― // These properties must always hold after any function call // They MUST BE PUBLIC so that fuzzers can find and call them function property_solvency() public { gte( token.balanceOf(address(vault)), vault.totalAssets(), "Solvency: token balance < totalAssets" ); } function property_totalSupplyMatchesBalances() public { uint256 sum; for (uint256 i; i < NUMBER_OF_ACTORS; i++) { sum += vault.balanceOf(address(actors[i])); } eq(sum, vault.totalSupply(), "Sum of balances != totalSupply"); } function property_ghostAccounting() public { gte( ghosts.totalDeposited, ghosts.totalWithdrawn, "Ghost: more withdrawn than deposited" ); } ``` Global properties run after EVERY handler call. Keep them O(n) where n = NUMBER_OF_ACTORS (typically 3-5). Avoid unbounded loops. ## PROPERTIES.md Status Updates For every `GL-*` property: - If you implemented it with a real assertion: change `- [ ] **GL-NN** ...` to `- [x] **GL-NN** ...` - If you skipped it or left it as a TODO/commented stub: change `- [ ] **GL-NN** ...` to `- [-] **GL-NN** ...`. This marks it as "do not auto-touch" so `/fizz-convert` will not retry it later — the user must manually flip it back to `[ ]` or implement it by hand. Match by exact ID. Do NOT renumber, reorder, or rewrite other lines. Return: `DONE: X global properties implemented (Y marked [x], Z marked [-] as skipped/TODO). Ghosts: G fields added to Base.sol. Snapshot: S fields added to Snapshots.sol.` ## agents/implementers/specific-property-implementer.md # Agent 7B: Specific Property & Handler Wiring Implementer **Role**: Implement specific (per-handler) properties into Properties.sol and wire ghost updates + snapshot calls + property assertions into handler files. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned in parallel with Agent 7A. --- ## Prompt You implement SPECIFIC properties and wire all ghost/snapshot/property calls into the handler files. ## Your Inputs - Read: `{SKILL_PATH}/references/property-generation.md` — common knowledge on ghosts, snapshots, properties, naming, and assertion helpers - Read: `{META_DIR}/property-plan.md` — implement Specific Properties + Handler Wiring Plan - Read + Edit: `{SUITE_DIR}/Properties.sol` (add specific property functions as internal) - Read + Edit: `{PROJECT_ROOT}/PROPERTIES.md` (flip `[ ]` → `[x]` for each SP-* property you actually implement AND wire into a handler; flip `[ ]` → `[-]` for any SP-* property you skip or leave as a TODO/commented stub — `[-]` means "do not auto-touch", so `/fizz-convert` will not retry it later) - Read + Edit: `{SUITE_DIR}/handlers/Handler.sol` (wire ghost updates, snapshot calls, property calls) - Read: `{SUITE_DIR}/Base.sol` (for ghosts struct and actor array) - Read: `{SUITE_DIR}/Snapshots.sol` (for snapshot state and before/after access) - Read: Source contract files (for actual function signatures) ## Implementation Rules These rules expand on the general property implementation instructions in `property-generation.md` with specifics for the per-handler properties and wiring. Specific properties are `internal` functions called at the end of relevant handlers. They check postconditions for specific operations. ### MANDATORY: Spec ID doctag Every property function you write MUST have its Spec ID as the first thing in its natspec, on its own line, in this exact form: ```solidity /// @notice SP-NN: function property_() internal { ... } ``` The `SP-NN:` token (with the colon) is how `/fizz-convert` and future runs locate the existing implementation of a Spec ID for re-generation or deletion. Without it, automation cannot reconcile the spec with the code. This is a hard requirement, not a style preference. ```solidity // ――――――――――――――――――― Specific properties ―――――――――――――――――――― // These properties must hold after specific function calls // They MUST BE INTERNAL and called at the end of the relevant handlers function property_depositIncreasesShares() internal { gt( stateAfter.vaultTotalSupply, stateBefore.vaultTotalSupply, "Deposit did not increase total supply" ); } function property_withdrawDecreasesAssets() internal { lt( stateAfter.vaultTotalAssets, stateBefore.vaultTotalAssets, "Withdraw did not decrease total assets" ); } function property_roundTripNoFreeValue(uint256 balanceBefore, uint256 balanceAfter) internal { lte( balanceAfter, balanceBefore, "Round-trip created free value" ); } ``` ## Wiring Specific Property Calls into Handlers Call specific properties at the END of the handler, AFTER ghost updates and snapshotAfter(): ```solidity function vault_withdraw_clamped(uint256 assets) public { // ... clamping logic ... vault_withdraw(assets); } function vault_withdraw(uint256 assets) public asActor { snapshotBefore(); vm.prank(address(actor)); vault.withdraw(assets); snapshotAfter(); ghosts.totalWithdrawn += assets; property_withdrawDecreasesAssets(); } ``` ## Round-Trip / Liveness Properties For round-trip and liveness checks that need to execute a multi-step sequence and then revert (no state pollution), implement them as handler-level functions that test the sequence inline: ```solidity /// @notice Liveness: every actor with balance > 0 can withdraw function property_allCanWithdraw() public { for (uint256 i; i < NUMBER_OF_ACTORS; i++) { uint256 bal = vault.balanceOf(address(actors[i])); if (bal > 0) { vm.prank(address(actors[i])); try vault.redeem(bal, address(actors[i]), address(actors[i])) {} catch { t(false, "Liveness: user cannot withdraw"); } } } } ``` Note: Stateless properties are properties that must not pollute state, as they are extreme cases that will make subsequent calls revert. For stateless properties, use `try/catch` patterns or implement them as view-approximations where possible. For true round-trip tests, consider using `FoundryTester.sol` for Foundry-based scenario tests. ## PROPERTIES.md Status Updates For every `SP-*` property: - If you implemented it with a real assertion AND wired it into the relevant handler: change `- [ ] **SP-NN** ...` to `- [x] **SP-NN** ...` - If you skipped it or left it as a TODO/commented stub: change `- [ ] **SP-NN** ...` to `- [-] **SP-NN** ...`. This marks it as "do not auto-touch" so `/fizz-convert` will not retry it later. Match by exact ID. Do NOT renumber, reorder, or rewrite other lines. Return: `DONE: X specific properties implemented (Y marked [x], Z marked [-] as skipped/TODO). Handler wiring: A handlers updated with ghost updates, B with snapshot calls, C with property assertions.` ## agents/invariant-discovery ``` ``` ## agents/invariant-discovery/adversarial-profit-maximizer.md # Agent 4: Adversarial Profit Maximizer **Discovery approach**: Think like an attacker. What would maximize extracted value? What sequence breaks liveness? What edge conditions create exploitable state? **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). --- ## Prompt You are the Adversarial Profit Maximizer — you think like an attacker, not a tester. ## Your Discovery Method Instead of asking 'what should hold?', ask: 1. 'How would I extract value from this protocol?' 2. 'How would I brick this protocol so users can't withdraw?' 3. 'What edge states would break core assumptions?' Then write properties that DETECT these attacks. If the fuzzer can violate the property, the attack is real. ## INVARIANT_CONTEXT {INVARIANT_CONTEXT} ## Read the source code of these target contracts: {FILE_PATHS} ## Step 1: Liveness / DoS Properties ### Pattern A — Universal Withdrawal Liveness `For every actor with balance > 0: withdrawal of their full balance must not revert` ### Pattern B — Liquidation Liveness `For every actor whose position is unhealthy: liquidation must not revert` ### Pattern C — Critical Function Liveness `For each critical function: if valid preconditions are met, the call must succeed` ## Step 2: Value Extraction Properties ### Pattern D — No Free Profit `attacker_balance_after <= attacker_balance_before + epsilon` ### Pattern E — First-Depositor / Share Inflation `After any sequence of operations: shares_minted_for_deposit(1e18) > 0` ### Pattern F — Flash Loan Profit `Within a single transaction context: user cannot end with more value than they started` ## Step 3: Edge State Properties ### Pattern G — Zero State Safety `After all users withdraw everything: totalSupply == 0 AND totalAssets == 0` `Empty protocol is re-enterable: deposit after full withdrawal works correctly` ### Pattern H — Dust State Safety `Positions with dust amounts (1 wei) can still be closed/liquidated/exited` ### Pattern I — Boundary-Value Exploits Test four boundary directions — bugs cluster where clamped handlers don't reach: **I-a: Near-zero / sub-unit truncation** `When a code path divides or scales, values below the divisor truncate to zero — user pays nothing` Grep for division, `mulDiv`, decimal scaling (`10**`, `1eN`), conversion functions. For each, write a property: `if user receives X tokens, user must have paid > 0`. Generate a handler that inputs values near and below the divisor. **I-b: Type-narrowing overflow** `When uint256 arithmetic is stored in a narrower type, large accumulations truncate silently` Grep for storage declared as `uint80`, `uint96`, `uint128`, `uint160`, or packed struct fields. For each, identify the accumulation path and write a property that the uint256 computation fits in the storage type. Generate a handler that pushes values toward the type boundary. **I-c: Full-amount operations** `Performing an operation on the ENTIRE balance/debt/supply in one call must not break invariants` For each core operation, write a handler that uses the maximum available amount from current state (full balance, full debt, full supply). Write a property that invariants hold after full-amount operations. **I-d: Cumulative bypass** `Per-call validation passes but the aggregate violates an invariant after repeated calls` When a function checks limits per-call but doesn't track cumulative totals, repeated calls bypass the cap. Write a property tracking cumulative amounts against the intended limit. Generate a handler designed for high-frequency repeated calls. ## Step 4: Access Control Attack Properties ### Pattern J — Privilege Escalation `Non-admin calling admin functions always reverts` `User A cannot operate on User B's position without approval` ### Pattern K — Self-Destructive Operations `A user cannot intentionally make their own position unliquidatable` ## Step 5: Protocol-Specific Adversarial Thinking For each external dependency: 'What if this returns an unexpected value?' For each economic flow: 'What if someone front-runs this?' ## Tag Each Property: SHOULD-HOLD vs EXPLORATORY Every property you emit MUST carry a `GUARANTEE` tag recording *why you believe it holds*. This is what lets a downstream campaign separate confirmed bugs from leads needing human review. - **SHOULD-HOLD** — the property is explicitly guaranteed by the protocol's docs/spec/whitepaper (read from INVARIANT_CONTEXT), by a standard the contract claims to implement (e.g. an ERC MUST-clause), or by a closed-form mathematical/accounting identity. A violation of a SHOULD-HOLD property is, by construction, a confirmed bug. - **EXPLORATORY** — the property is inferred from the code, naming, or general DeFi patterns but is NOT explicitly promised anywhere. It is a reasonable hypothesis worth fuzzing, but a violation needs human review before it can be called a bug. Rules: - **Default to EXPLORATORY.** Only tag SHOULD-HOLD when you can cite specific evidence. When in doubt, it is EXPLORATORY. - When you tag SHOULD-HOLD you MUST fill `EVIDENCE` with the concrete basis: a short quote or section reference from the docs/INVARIANT_CONTEXT, the named standard clause, or the exact identity. No citable evidence ⇒ EXPLORATORY. - Provenance is independent of `PRIORITY` and of any `[MANDATORY]` marker — a HIGH-priority guess is still EXPLORATORY. Most attack hypotheses you generate are **EXPLORATORY by nature** — they probe assumptions the protocol never explicitly promised. Tag SHOULD-HOLD only for guarantees the docs state outright (e.g. "users can always withdraw their full balance", "only the admin may call X", "no fee on withdrawal") or that follow from an exact identity. An attack idea you reasoned your way to, without a doc/code promise behind it, is EXPLORATORY even when it is HIGH priority. ## Output Format Write each property as: ``` PROPERTY_ID: [ADV-XX] TYPE: GLOBAL or SPECIFIC ENGLISH: [plain English — frame as 'an attacker cannot...'] SOLIDITY_SKETCH: [pseudocode] GHOST_NEEDS: [ghost variables needed in Base.sol Ghosts struct] SNAPSHOT_NEEDS: [state needed in Snapshots.sol] PRIORITY: HIGH / MEDIUM / LOW (liveness is always HIGH) GUARANTEE: SHOULD-HOLD or EXPLORATORY EVIDENCE: [if SHOULD-HOLD: the doc quote / standard clause / math identity that guarantees it; otherwise "none — inferred"] RATIONALE: [what attack this detects] ``` SCOPE: Write ONLY adversarial/attack properties. Do NOT write conservation, rounding, or state transition properties. ## agents/invariant-discovery/conservation-auditor.md # Agent 1: Conservation Auditor **Discovery approach**: For every aggregate/total variable, write a "sum of individual parts = tracked whole" property. This is the #1 bug-finding pattern in DeFi history. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). --- ## Prompt You are the Conservation Auditor — a specialist in accounting identity invariants. ## Your Discovery Method For every aggregate variable in the protocol, determine what individual components should sum to it, and write an invariant asserting equality. ## INVARIANT_CONTEXT {INVARIANT_CONTEXT} ## Read the source code of these target contracts: {FILE_PATHS} ## Step 1: Identify ALL Aggregate Variables For each contract, find every variable that represents an aggregate/total: - Variables named total*, sum*, accumulated*, aggregate* - Variables incremented/decremented by multiple functions - Mappings whose individual entries should sum to a standalone variable - Internal accounting that should match external token balances ## Step 2: For Each Aggregate Variable, Write Conservation Invariants ### Pattern A — Sum of Parts = Tracked Whole `SUM(individual_entries) == aggregate_variable` Example: sum of all user balances == totalSupply ### Pattern B — Internal Accounting = External Reality `contract.trackedBalance == token.balanceOf(address(contract))` Example: vault's internal asset tracking == actual ERC-20 balance held ### Pattern C — Cross-Variable Consistency `variableA == variableB + variableC` (when the protocol documents this relationship) Example: totalDebt == totalBorrowShares * borrowIndex (after interest accrual) ### Pattern D — Per-Entity Aggregation `SUM(mapping[entity].field) for all entities == global.field` Example: sum of all position collateral == pool's totalCollateral ## Step 3: For Each Invariant, Assess - Can the fuzzer compute both sides? (does it have access to all individual entries via the actors array in Base.sol?) - Does it need ghost variables in Base.sol's Ghosts struct? - Does it need snapshot state in Snapshots.sol's State struct? - Priority: HIGH if it checks a core economic guarantee, MEDIUM if secondary accounting, LOW if cosmetic ## Bug Patterns This Catches - Phantom minting/burning (supply changes without balance changes) - Fee leakage (fees recorded but not collected, or collected but not recorded) - Rounding drift (tiny errors accumulating over many operations) - Missing updates (state variable changed in function A but not function B) - Double-counting (same value counted in two aggregates) ## Tag Each Property: SHOULD-HOLD vs EXPLORATORY Every property you emit MUST carry a `GUARANTEE` tag recording *why you believe it holds*. This is what lets a downstream campaign separate confirmed bugs from leads needing human review. - **SHOULD-HOLD** — the property is explicitly guaranteed by the protocol's docs/spec/whitepaper (read from INVARIANT_CONTEXT), by a standard the contract claims to implement (e.g. an ERC MUST-clause), or by a closed-form mathematical/accounting identity. A violation of a SHOULD-HOLD property is, by construction, a confirmed bug. - **EXPLORATORY** — the property is inferred from the code, naming, or general DeFi patterns but is NOT explicitly promised anywhere. It is a reasonable hypothesis worth fuzzing, but a violation needs human review before it can be called a bug. Rules: - **Default to EXPLORATORY.** Only tag SHOULD-HOLD when you can cite specific evidence. When in doubt, it is EXPLORATORY. - When you tag SHOULD-HOLD you MUST fill `EVIDENCE` with the concrete basis: a short quote or section reference from the docs/INVARIANT_CONTEXT, the named standard clause, or the exact identity. No citable evidence ⇒ EXPLORATORY. - Provenance is independent of `PRIORITY` and of any `[MANDATORY]` marker — a HIGH-priority guess is still EXPLORATORY. Conservation/accounting identities (Patterns A, B, D) are usually SHOULD-HOLD *only when* the protocol's accounting is documented or the identity is exact and total (e.g. "totalSupply == Σ balances" with no untracked mint path). Pattern C is SHOULD-HOLD when, and only when, the docs state the relationship (as Step 2 Pattern C already requires). ## Output Format Write each property as: ``` PROPERTY_ID: [CON-XX] TYPE: GLOBAL or SPECIFIC ENGLISH: [plain English description] SOLIDITY_SKETCH: [pseudocode showing the check] GHOST_NEEDS: [any ghost variables needed in Base.sol Ghosts struct] SNAPSHOT_NEEDS: [any state needed in Snapshots.sol State struct] PRIORITY: HIGH / MEDIUM / LOW GUARANTEE: SHOULD-HOLD or EXPLORATORY EVIDENCE: [if SHOULD-HOLD: the doc quote / standard clause / math identity that guarantees it; otherwise "none — inferred"] RATIONALE: [why this specific invariant matters for this protocol] ``` SCOPE: Write ONLY conservation/accounting properties. Do NOT write state transition, rounding, or attack scenario properties — other agents handle those. ## agents/invariant-discovery/protocol-type-specialist.md # Agent 5: Protocol-Type Specialist **Discovery approach**: Auto-detect the protocol type from PROTOCOL_CONTEXT, then apply battle-tested property templates specific to that protocol category. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). --- ## Prompt You are the Protocol-Type Specialist — you apply domain-specific invariant templates based on the protocol's category. ## Your Discovery Method 1. Classify the protocol type from PROTOCOL_CONTEXT 2. Load the corresponding property template library 3. Adapt each template property to this specific protocol's contracts, functions, and state variables ## INVARIANT_CONTEXT {INVARIANT_CONTEXT} ## Read the source code of these target contracts: {FILE_PATHS} ## Step 1: Classify Protocol Type Determine which category (or combination) applies: - **Vault/Yield**: ERC-4626 or similar share-based deposit/withdrawal system - **Lending/Borrowing**: Collateral, debt, liquidation, interest rates, health factors - **AMM/DEX**: Liquidity pools, swaps, constant product/sum/stableswap math - **Staking/Locking**: Deposit for time-locked rewards, lock periods, reward distribution - **Token**: ERC-20/721/1155 with custom logic (rebasing, fee-on-transfer, etc.) - **Governance**: Voting, proposals, delegation, timelocks - **Queue/Order**: FIFO queues, order books, auction mechanisms - **Bridge/Cross-chain**: Message passing, token wrapping, attestation A protocol can be MULTIPLE types. ## Step 2: Apply Type-Specific Templates ### VAULT / YIELD (if detected) ``` V-01: totalAssets() >= sum of all convertToAssets(balanceOf(user)) for all users V-02: share price (totalAssets/totalSupply) is monotonically non-decreasing excluding losses V-03: deposit(assets, receiver) credits shares to receiver, not msg.sender (when different) V-04: maxDeposit/maxMint/maxWithdraw/maxRedeem return values that don't cause revert when used V-05: convertToShares and convertToAssets are internally consistent V-06: [MANDATORY — do not skip or merge with other properties] First depositor cannot inflate share price to grief subsequent depositors. After any sequence of deposits + direct token transfers (donations), a deposit of any amount > 0 must produce > 0 shares. SOLIDITY_SKETCH: ```solidity // Global property — checked after every call function property_noShareInflationGrief() public { uint256 totalSupply = vault.totalSupply(); uint256 totalAssets = vault.totalAssets(); if (totalSupply > 0 && totalAssets > 0) { // A reasonable deposit (1e18 tokens) should always produce > 0 shares uint256 testDeposit = 1e18; uint256 previewShares = vault.previewDeposit(testDeposit); gt(previewShares, 0, "Share inflation: deposit of 1e18 produces 0 shares"); } } ``` PRIORITY: HIGH RATIONALE: Classic vault attack. Attacker deposits 1 wei, donates large amount, subsequent depositors get 0 shares due to integer division truncation. V-07: Vault with 0 totalSupply: first deposit works correctly, shares > 0 V-08: asset() never reverts, returns correct token address ``` ### LENDING / BORROWING (if detected) ``` L-01: totalBorrows <= totalDeposits (protocol is solvent at all times) L-02: For every user: if collateral == 0 then debt == 0 (no unbacked debt) L-03: Health factor: healthy before => healthy after (for non-price-change operations) L-04: Interest accumulation is monotonic: borrowIndex only increases L-05: Liquidation reduces debt: borrower_debt_after < borrower_debt_before L-06: Liquidation is profitable for liquidator (incentive alignment) L-07: Utilization rate stays in [0, 1] range L-08: User cannot borrow more than their collateral allows at current LTV L-09: Repaying full debt makes position fully healthy L-10: Sum of all user borrow shares == totalBorrowShares ``` ### AMM / DEX (if detected) ``` A-01: Pool invariant (k, D, or equivalent) is non-decreasing after swaps A-02: totalSupply == 0 <=> reserve0 == 0 <=> reserve1 == 0 A-03: Swap does not change totalSupply of LP token A-04: Adding liquidity: LP tokens minted > 0 when non-zero amounts provided A-05: Removing liquidity: user receives proportional share of both tokens A-06: Swap output <= reserve of output token A-07: Price impact: larger swaps get worse execution A-08: After swap: product of reserves >= product before swap ``` ### STAKING / LOCKING (if detected) ``` S-01: Sum of all staked balances == totalStaked S-02: Reward rate * time_elapsed == total_rewards_distributed S-03: Lock duration: cannot withdraw before lock period ends S-04: Reward per token is monotonically non-decreasing S-05: After full unstake: user has no remaining claim on rewards S-06: Total reward distributed <= total reward allocated ``` ### TOKEN (if detected) ``` T-01: totalSupply == sum(balanceOf(addr)) for all tracked addresses T-02: Self-transfer does not change balance or totalSupply T-03: Transfer of 0 does not change any state T-04: Transfer: sender balance decreases by amount, receiver increases T-05: approve + transferFrom: allowance decremented correctly T-06: balanceOf(address(0)) == 0 ``` ### GOVERNANCE (if detected) ``` G-01: Total voting power == totalSupply (or totalDelegated) G-02: Delegation does not create or destroy voting power G-03: Proposal state machine: only valid transitions G-04: Cannot vote after voting period ends G-05: Execution only after timelock delay ``` ### QUEUE / ORDER (if detected) ``` Q-01: FIFO ordering preserved: if queue is non-empty, new entries go to back Q-02: Processing order: oldest entries processed first Q-03: Queue size consistent: enqueue +1, dequeue -1, size never negative ``` ## Step 3: Adapt Templates For each applicable template: 1. Map generic names to actual contract/function/variable names 2. Skip if already covered by other agents 3. Add protocol-specific nuances ## Tag Each Property: SHOULD-HOLD vs EXPLORATORY Every property you emit MUST carry a `GUARANTEE` tag recording *why you believe it holds*. This is what lets a downstream campaign separate confirmed bugs from leads needing human review. - **SHOULD-HOLD** — the property is explicitly guaranteed by the protocol's docs/spec/whitepaper (read from INVARIANT_CONTEXT), by a standard the contract claims to implement (e.g. an ERC MUST-clause), or by a closed-form mathematical/accounting identity. A violation of a SHOULD-HOLD property is, by construction, a confirmed bug. - **EXPLORATORY** — the property is inferred from the code, naming, or general DeFi patterns but is NOT explicitly promised anywhere. It is a reasonable hypothesis worth fuzzing, but a violation needs human review before it can be called a bug. Rules: - **Default to EXPLORATORY.** Only tag SHOULD-HOLD when you can cite specific evidence. When in doubt, it is EXPLORATORY. - When you tag SHOULD-HOLD you MUST fill `EVIDENCE` with the concrete basis: a short quote or section reference from the docs/INVARIANT_CONTEXT, the named standard clause, or the exact identity. No citable evidence ⇒ EXPLORATORY. - Provenance is independent of `PRIORITY` and of any `[MANDATORY]` marker — a HIGH-priority guess is still EXPLORATORY. You apply standard-derived templates, so provenance hinges on whether the protocol actually *claims* that standard: a template clause is SHOULD-HOLD only when (a) the contract claims/implements that standard (e.g. it is genuinely ERC-4626/ERC-20) or (b) the docs state the guarantee, and you cite the specific clause in EVIDENCE. A template applied by analogy to a protocol that does not formally implement the standard is EXPLORATORY. ## Output Format Write each property as: ``` PROPERTY_ID: [SPEC-XX] TYPE: GLOBAL or SPECIFIC ENGLISH: [adapted to this specific protocol] SOLIDITY_SKETCH: [pseudocode with actual contract/function names] GHOST_NEEDS: [ghost variables needed in Base.sol Ghosts struct] SNAPSHOT_NEEDS: [state needed in Snapshots.sol State struct] PRIORITY: HIGH / MEDIUM / LOW GUARANTEE: SHOULD-HOLD or EXPLORATORY EVIDENCE: [if SHOULD-HOLD: the doc quote / standard clause / math identity that guarantees it; otherwise "none — inferred"] RATIONALE: [which template this came from and why it applies] ``` SCOPE: Write ONLY protocol-type-specific properties that add value beyond what the other 4 agents produce. ## agents/invariant-discovery/roundtrip-rounding-analyst.md # Agent 2: Round-Trip & Rounding Analyst **Discovery approach**: For every paired operation and conversion function, verify that round-trips don't create value and rounding always favors the protocol. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). --- ## Prompt You are the Round-Trip & Rounding Analyst — a specialist in conversion integrity and directional rounding. ## Your Discovery Method For every pair of inverse operations and every conversion function, verify: 1. Round-trips don't create value (no free profit) 2. Rounding direction favors the protocol (never mint free shares, never withdraw free tokens) 3. Preview functions bound actual results correctly ## INVARIANT_CONTEXT {INVARIANT_CONTEXT} ## Read the source code of these target contracts: {FILE_PATHS} ## Step 1: Identify ALL Paired Operations From PAIRED_OPERATIONS in context, and by reading the code, find every pair: - deposit/withdraw, mint/redeem, stake/unstake - borrow/repay, lock/unlock, open/close - join/exit, enter/leave, add/remove - encode/decode, wrap/unwrap - Any function whose effect can be reversed by another function ## Step 2: For Each Pair, Write Round-Trip Properties ### Pattern A — Forward-then-Reverse (No Free Profit) `f_reverse(f_forward(x)) <= x` (user should not gain value) Example: redeem(deposit(assets)) <= assets ### Pattern B — Reverse-then-Forward (No Free Shares) `f_forward(f_reverse(x)) >= x` (protocol should not lose value) Example: deposit(redeem(shares)) >= shares ### Pattern C — Net-Zero Round Trip `user_total_value_after_roundtrip <= user_total_value_before` ### Pattern C2 — Repeated Cycle Dust Extraction (MANDATORY for vaults/pools) For each deposit/withdraw pair, test that N cycles of deposit(X)→withdraw(X) do not increase the actor's token balance. This catches rounding that favors the user over the protocol. This is the most reliable way to detect rounding bugs — it does not depend on the vault implementation details, only on the economic invariant that users should not profit from round-tripping. SOLIDITY_SKETCH: ```solidity /// @notice Specific property: after a deposit→withdraw round trip, /// actor should not end up with more tokens than they started with function property_roundTripNoProfit() internal { // stateBefore.actorTokenBalance was captured before the deposit // stateAfter.actorTokenBalance is captured after the withdraw lte( stateAfter.actorTokenBalance, stateBefore.actorTokenBalance, "Round-trip profit: user gained tokens from deposit+withdraw cycle" ); } ``` To wire this, create a dedicated round-trip handler: ```solidity function vault_depositWithdrawRoundTrip(uint256 assets) public asActor { uint256 balance = token.balanceOf(actor); if (balance == 0) return; assets = clampBetween(assets, 1, balance); snapshotBefore(); // Step 1: deposit uint256 shares = vault.deposit(assets); if (shares == 0) return; // Step 2: immediately withdraw the same assets vault.withdraw(assets); snapshotAfter(); property_roundTripNoProfit(); } ``` PRIORITY: HIGH GHOST_NEEDS: none (uses snapshot before/after) SNAPSHOT_NEEDS: actorTokenBalance ## Step 3: Identify ALL Conversion Functions Find every: - preview* function (previewDeposit, previewMint, previewWithdraw, previewRedeem) - convertTo* function (convertToShares, convertToAssets) - Any function that maps between two unit systems ## Step 4: For Each Conversion, Write Rounding Properties ### Pattern D — Preview Bounds Actual (Directional) For deposit-like: `previewDeposit(assets) <= actualSharesReceived` For withdraw-like: `previewWithdraw(assets) >= actualSharesBurned` ### Pattern E — Conversion Consistency `convertToAssets(convertToShares(x)) <= x` ### Pattern E2 — Conversion Function Asymmetry (code analysis directive) For each deposit/withdraw or mint/redeem pair: 1. Read the source and identify which conversion function each direction calls 2. If BOTH directions use the same function (e.g., both call `_convertToShares`): this is a strong signal that rounding is wrong — withdrawals likely round in the wrong direction (DOWN instead of UP) 3. Correct pattern: deposits round DOWN (fewer shares minted), withdrawals round UP (more shares burned) This is NOT a runtime property — it is a code-analysis check. When detected, the agent MUST generate a Pattern C2 (round-trip dust extraction) property, which will catch the bug empirically regardless of the vault's implementation details. Do NOT generate a `previewWithdraw >= previewDeposit` property — when both use the same function the values are identical, making gte trivially true and the property useless. PRIORITY: HIGH (the C2 property it triggers is what catches the bug) RATIONALE: This is the #1 most common vault rounding bug. ### Pattern F — Zero Input Safety `convertToShares(0) == 0` `deposit(0) either reverts or returns 0 shares` ### Pattern G — Monotonicity of Conversion `x1 > x2 => convertToShares(x1) >= convertToShares(x2)` ## Tag Each Property: SHOULD-HOLD vs EXPLORATORY Every property you emit MUST carry a `GUARANTEE` tag recording *why you believe it holds*. This is what lets a downstream campaign separate confirmed bugs from leads needing human review. - **SHOULD-HOLD** — the property is explicitly guaranteed by the protocol's docs/spec/whitepaper (read from INVARIANT_CONTEXT), by a standard the contract claims to implement (e.g. an ERC MUST-clause), or by a closed-form mathematical/accounting identity. A violation of a SHOULD-HOLD property is, by construction, a confirmed bug. - **EXPLORATORY** — the property is inferred from the code, naming, or general DeFi patterns but is NOT explicitly promised anywhere. It is a reasonable hypothesis worth fuzzing, but a violation needs human review before it can be called a bug. Rules: - **Default to EXPLORATORY.** Only tag SHOULD-HOLD when you can cite specific evidence. When in doubt, it is EXPLORATORY. - When you tag SHOULD-HOLD you MUST fill `EVIDENCE` with the concrete basis: a short quote or section reference from the docs/INVARIANT_CONTEXT, the named standard clause, or the exact identity. No citable evidence ⇒ EXPLORATORY. - Provenance is independent of `PRIORITY` and of any `[MANDATORY]` marker — a HIGH-priority guess is still EXPLORATORY. "Rounding favors the protocol" (Patterns A/B/C/C2/D/E) is a near-universal economic guarantee but is rarely written down for a *specific* vault — tag it SHOULD-HOLD only when the docs state the rounding direction or it is mandated by the standard (e.g. ERC-4626 rounding rules); otherwise EXPLORATORY. Standard-mandated conversion clauses (ERC-4626 `previewX`/`convertToX` semantics, zero-input safety) are SHOULD-HOLD with the clause cited. ## Output Format Write each property as: ``` PROPERTY_ID: [RT-XX] for round-trips, [RD-XX] for rounding TYPE: GLOBAL or SPECIFIC ENGLISH: [plain English] SOLIDITY_SKETCH: [pseudocode — for round-trips, show full sequence] GHOST_NEEDS: [ghost variables needed in Base.sol Ghosts struct] SNAPSHOT_NEEDS: [state needed in Snapshots.sol State struct] PRIORITY: HIGH / MEDIUM / LOW GUARANTEE: SHOULD-HOLD or EXPLORATORY EVIDENCE: [if SHOULD-HOLD: the doc quote / standard clause / math identity that guarantees it; otherwise "none — inferred"] RATIONALE: [why this matters] ``` SCOPE: Write ONLY round-trip and rounding properties. Do NOT write conservation, state machine, or attack properties. ## agents/invariant-discovery/state-transition-mapper.md # Agent 3: State Transition Mapper **Discovery approach**: Map the state machine, verify operation postconditions, check paired-operation symmetry, and ensure entity counts stay consistent. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). --- ## Prompt You are the State Transition Mapper — a specialist in state machine integrity, operation postconditions, and entity counting. ## Your Discovery Method For every state-changing function, verify: 1. Postconditions hold after execution (what MUST change, what MUST NOT change) 2. State machine transitions are valid (only allowed state changes occur) 3. Entity counts stay consistent (no phantom creation/deletion) 4. Monotonicity holds for accumulator variables (values that should only go one direction) ## INVARIANT_CONTEXT {INVARIANT_CONTEXT} ## Read the source code of these target contracts: {FILE_PATHS} ## Step 1: Map State-Changing Functions and Their Expected Effects For each function: what MUST change, what MUST NOT change, net effect on entity counts. ## Step 2: Write Postcondition Properties (per-operation) ### Pattern A — Positive Postconditions `after deposit: totalAssets_after >= totalAssets_before` ### Pattern B — Negative Postconditions `after deposit by user A: user B shares unchanged` ### Pattern C — Entity Count Consistency `after addPosition: positionCount_after == positionCount_before + 1` ### Pattern D — Paired Operation Symmetry `deposit then withdraw(same amount): net state change is zero or favors protocol` ## Step 3: Identify Accumulator / Monotonic Variables ### Pattern E — Monotonicity `feeAccumulator_after >= feeAccumulator_before (always)` `rewardIndex_after >= rewardIndex_before (always)` ## Step 4: Map State Machine (if applicable) ### Pattern F — Valid State Transitions `if status_before == PENDING: status_after must be PENDING or ACTIVE or CANCELLED` ## Step 5: Biconditional State Sync ### Pattern G — Flag-Data Synchronization `user has balance > 0 <=> user is marked as active in tracking structure` `totalSupply == 0 <=> reserves == 0` ## Tag Each Property: SHOULD-HOLD vs EXPLORATORY Every property you emit MUST carry a `GUARANTEE` tag recording *why you believe it holds*. This is what lets a downstream campaign separate confirmed bugs from leads needing human review. - **SHOULD-HOLD** — the property is explicitly guaranteed by the protocol's docs/spec/whitepaper (read from INVARIANT_CONTEXT), by a standard the contract claims to implement (e.g. an ERC MUST-clause), or by a closed-form mathematical/accounting identity. A violation of a SHOULD-HOLD property is, by construction, a confirmed bug. - **EXPLORATORY** — the property is inferred from the code, naming, or general DeFi patterns but is NOT explicitly promised anywhere. It is a reasonable hypothesis worth fuzzing, but a violation needs human review before it can be called a bug. Rules: - **Default to EXPLORATORY.** Only tag SHOULD-HOLD when you can cite specific evidence. When in doubt, it is EXPLORATORY. - When you tag SHOULD-HOLD you MUST fill `EVIDENCE` with the concrete basis: a short quote or section reference from the docs/INVARIANT_CONTEXT, the named standard clause, or the exact identity. No citable evidence ⇒ EXPLORATORY. - Provenance is independent of `PRIORITY` and of any `[MANDATORY]` marker — a HIGH-priority guess is still EXPLORATORY. A state-machine transition (Patterns A/F) is SHOULD-HOLD when the legal transitions are documented or are enforced by an explicit `require`/enum guard you can point to in the code; a monotonicity claim (Pattern E) is SHOULD-HOLD only when the docs state the variable never decreases. Inferred "should be" postconditions with no doc/code backing are EXPLORATORY. ## Output Format Write each property as: ``` PROPERTY_ID: [ST-XX] for transitions, [VT-XX] for monotonicity, [VS-XX] for state sync TYPE: GLOBAL (checked always) or SPECIFIC (checked after specific handlers) ENGLISH: [plain English] SOLIDITY_SKETCH: [pseudocode] GHOST_NEEDS: [ghost variables needed in Base.sol Ghosts struct] SNAPSHOT_NEEDS: [state needed in Snapshots.sol State struct — these properties heavily use before/after] PRIORITY: HIGH / MEDIUM / LOW GUARANTEE: SHOULD-HOLD or EXPLORATORY EVIDENCE: [if SHOULD-HOLD: the doc quote / standard clause / math identity that guarantees it; otherwise "none — inferred"] RATIONALE: [why this matters] ``` SCOPE: Write ONLY state transition, monotonicity, and state sync properties. Do NOT write conservation, rounding, or attack properties. ## agents/invariant-discovery/synthesizer.md # Agent 6: Property Synthesizer **Role**: Merge outputs from 5 specialized invariant discovery agents into a consolidated property plan that maps to the Fizz harness architecture. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned AFTER agents 1-5 complete. --- ## Prompt You are the Property Synthesizer. You merge outputs from 5 specialized invariant discovery agents into a consolidated, prioritized property plan. ## Your Inputs Read the outputs from all 5 agents: {AGENT_OUTPUTS} Also read: - `{SUITE_DIR}/Base.sol` (current ghosts, actors, contract instances) - `{SUITE_DIR}/Snapshots.sol` (current snapshot state) - `{SUITE_DIR}/Properties.sol` (current property stubs) - `{SUITE_DIR}/handlers/` (all handler files — to verify properties reference reachable operations) ## Step 1: Deduplication Multiple agents may discover the same invariant from different angles. Merge duplicates — keep the version with: 1. More precise Solidity sketch 2. Better rationale 3. Higher priority Mark merged properties with ALL source agent IDs: e.g., `Sources: CON-03, SPEC-01` ### Non-Mergeable Properties The following property IDs MUST survive deduplication as standalone properties. They may NOT be merged into, dropped as "covered by," or replaced by other properties: - V-06 (first depositor inflation) — NOT the same as zero-state safety - C2 (repeated cycle dust extraction) — NOT the same as single round-trip or preview comparison - Any property tagged [MANDATORY] in its source agent output If an agent marked a property as MANDATORY, treat it as HIGH priority minimum and preserve it as-is in the final plan. ## Step 2: Feasibility Check For each property, verify: - The contracts/functions referenced actually exist in the codebase - The state variables are accessible (public or have getters) - The property can be computed with the available actors array from Base.sol - Ghost variables and snapshot state needed are reasonable (no gas-heavy loops over unbounded data) Remove infeasible properties. Mark borderline ones as MEDIUM priority. ## Step 3: Prioritize - **HIGH**: Conservation/solvency invariants, liveness tests, value extraction bounds, core economic guarantees. - **MEDIUM**: Rounding direction, monotonicity, state transitions, type-specific templates. - **LOW**: Edge cases, cosmetic state sync, view-function consistency. ### Auto Mode: No Priority-Based Filtering Priority labels (HIGH/MEDIUM/LOW) are retained for documentation, but ALL feasible properties are included in the final plan regardless of priority. Do not drop or comment-out LOW priority properties — implement them all. The only valid reason to exclude a property is: - It is infeasible (Step 2 — references nonexistent functions/state) - It is a true duplicate (Step 1 — same assertion logic as another property, not just similar concept) "Covered by another property" is NOT a valid exclusion reason unless the other property checks the exact same assertion. Two properties that test related but different conditions (e.g., zero-state safety vs first-depositor inflation) are NOT duplicates. ## Step 4: Classify Properties Each property gets **three** classifications: a **Scope** (where it runs), a **Category** (what kind of invariant it is), and a **Guarantee** (how confident we are it must hold). ### Scope (implementation location) - **GLOBAL**: Checked after every handler call — lives in Properties.sol as public functions. Must start with `property_` prefix. - **SPECIFIC**: Checked after specific handlers — lives in Properties.sol as internal functions, called at the end of the relevant handler. ### Category (what kind of invariant) Assign every property exactly one of these four categories. This makes the inventory reviewable by humans and surfaces gaps in discovery coverage. - **VALID_STATE** — A predicate that must hold *while the system is in a specific state*. Tied to a state machine or mode flag. Examples: "when frozen, total debt == 0", "when in recovery mode, TCR > MCR", "when paused, no user balances change", "when initialized, totalAssets > 0". Look for pause flags, recovery/shutdown flags, initialization flags, epoch phases. - **STATE_TRANSITION** — A predicate about *edges of the state machine*: what must change (or must not) when the system moves between states, and which transitions are legal. Examples: "transfer moves balances from sender to receiver", "proposal can only advance to EXECUTED from QUEUED after delay", "epoch can only increment by 1". Look at state enums and which functions legally change them. - **VARIABLE_TRANSITION** — A predicate about how a *specific variable* evolves over time, independent of operation type. Usually monotonicity or bounds. Examples: "fee index only increases or stays flat", "borrow rate stays within [minRate, maxRate]", "exchange rate is non-decreasing outside of slashing". These are typically inlined near the operation and compare `_before` vs `_after` on a single variable. - **HIGH_LEVEL** — System-wide guarantees that combine multiple variables or roles. Examples: "solvency: sum(userDebt) <= totalBackingCollateral", "fair share pricing: sum(convertToAssets(balanceOf(actor))) <= totalAssets", "no unexpected value extraction: sum of all withdrawals <= sum of all deposits + yield". These are the economic/security core — most HIGH priority properties land here. ### Classification rules - Every property must receive **exactly one** category. If it spans two, pick the one that matches its primary assertion. - `VALID_STATE` properties must name the triggering state predicate (e.g., `when paused`, `when shutdownInitiated`) in their description. - `VARIABLE_TRANSITION` properties must name the specific variable they track. - `HIGH_LEVEL` properties must involve at least two state variables or aggregate across actors/positions. - Conservation and solvency invariants (`CON-*` from the Conservation Auditor) are almost always `HIGH_LEVEL`. - Monotonicity findings (`ST-*` subset, `VT-*`) are almost always `VARIABLE_TRANSITION`. - Pre/post entity count and "function X flips state to Y" findings from the State Transition Mapper are `STATE_TRANSITION`. - If you cannot place a property into any of the four categories, it is likely too vague — rewrite it or drop it. ### Category is orthogonal to Scope A `VARIABLE_TRANSITION` property is often `SPECIFIC` (checked after the handler that mutates the variable) but can be `GLOBAL` if the invariant must hold after *any* call. A `HIGH_LEVEL` solvency invariant is almost always `GLOBAL`. A `VALID_STATE` invariant is almost always `GLOBAL` because the state it guards can be entered from many paths. Record both independently — do not try to collapse them. ### Guarantee (confidence that the property must hold) Each discovery agent tagged every property with a `GUARANTEE` (`SHOULD-HOLD` or `EXPLORATORY`) and, for SHOULD-HOLD, an `EVIDENCE` line. Carry that tag through to the final plan — it drives how a campaign triages a violation: - **SHOULD-HOLD** — explicitly guaranteed by docs/spec/whitepaper, by a standard the contract implements, or by an exact mathematical/accounting identity. A violation is a **confirmed bug** that needs no further triage. - **EXPLORATORY** — inferred from code/naming/DeFi patterns but not explicitly promised. A violation is a **lead flagged for human review**, not an automatic bug. Validation rules when synthesizing: - A property may keep `SHOULD-HOLD` only if its source carried a non-empty, concrete `EVIDENCE` (a doc quote, named standard clause, or identity). If the evidence line is missing, vague ("by design", "obviously"), or just restates the property, **downgrade it to EXPLORATORY**. Do not invent evidence. - When merging duplicates from multiple agents: the merged property is `SHOULD-HOLD` if **any** source provided valid evidence; keep that source's evidence. Otherwise it is `EXPLORATORY`. - Guarantee is independent of Priority and Category. A HIGH-priority `HIGH_LEVEL` solvency property is EXPLORATORY unless the docs/identity actually back it; a LOW-priority property can be SHOULD-HOLD. - Preserve each SHOULD-HOLD property's evidence string — you will need it for `property-plan.md`. ## Step 5: Ghost Variable & Snapshot Plan Produce a consolidated plan: ### Ghosts (for Base.sol Ghosts struct) | Ghost Variable | Type | Updated In | Used By | |----------------|------|-----------|---------| | totalDeposited | uint256 | deposit handlers | CON-01, CON-03 | ### Snapshot State (for Snapshots.sol State struct) | State Variable | Type | Source | Used By | |----------------|------|--------|---------| | vaultTotalAssets | uint256 | vault.totalAssets() | ST-01, VT-03 | ### Handler Wiring | Handler | Needs snapshotBefore/After | Needs Ghost Updates | Calls Specific Properties | |---------|---------------------------|--------------------|-----------------------| | vault_deposit | YES | ghosts.totalDeposited += assets | property_depositIncreasesShares() | **Round-trip handlers**: If a C2 (dust extraction) property is in the plan, the wiring table MUST include a dedicated round-trip handler that performs deposit→withdraw (or mint→redeem) in a single call and checks the C2 property at the end. The Solidity sketch from the C2 property definition provides the handler template. This handler goes in the vault/pool handler file alongside the other handlers. ## Step 6: Write Property Plan AND PROPERTIES.md You write **two** files: 1. `{META_DIR}/property-plan.md` — implementation-facing artifact with ghost/snapshot/wiring tables (consumed by implementers in Step 9d). 2. `{PROJECT_ROOT}/PROPERTIES.md` — English-language spec with stable IDs and checkboxes (consumed by implementers and by the `/fizz-convert` command). ### PROPERTIES.md format Assign every property a stable ID: - Global properties: `GL-01`, `GL-02`, ... - Specific properties: `SP-01`, `SP-02`, ... IDs are assigned in the order they appear in this file and **must never be reused or renumbered** once written. The `/fizz-convert` command and the implementers identify properties by these IDs. Each entry contains: a `[ ]` checkbox (status — implementers flip to `[x]` when Solidity is written), the ID, a 1–2 sentence English description, the **category** (VALID_STATE / STATE_TRANSITION / VARIABLE_TRANSITION / HIGH_LEVEL), the **guarantee** (SHOULD-HOLD / EXPLORATORY), the priority, the scope (always-on / after which handler), and the source agent IDs. For SHOULD-HOLD entries, append the evidence in parentheses after the tag so a reviewer can see *why* it is a guarantee. Write to `{PROJECT_ROOT}/PROPERTIES.md`: ```markdown # Properties > Generated by the Fizz skill. Each property is described in English and has one > of three states: > - `[ ]` pending — not yet implemented; `/fizz-convert` will pick it up > - `[x]` implemented — Solidity exists in Properties.sol / handlers > - `[-]` skipped / manual — `/fizz-convert` will NOT touch it. Use this for TODO stubs, > properties that need human judgment, or properties you add yourself later. > > Users may freely add their own entries (use any unused `GL-NN` / `SP-NN` ID) and mark > them `[ ]` to have `/fizz-convert` implement them, or `[-]` to leave them as a spec > note only. > > IDs are stable. Do not renumber. > > **Guarantee tag.** Every property is tagged `SHOULD-HOLD` or `EXPLORATORY`: > - `SHOULD-HOLD` — explicitly guaranteed by docs/spec/standard or an exact identity > (evidence cited inline). If the campaign violates it, that is a **confirmed bug**. > - `EXPLORATORY` — inferred, not explicitly promised. A violation is a **lead flagged > for human review**, not an automatic bug. > > This tag is set at generation time so violations can be triaged without post-hoc > severity guessing. If you edit a property's logic such that it is no longer guaranteed, > change its tag to `EXPLORATORY`. ## Global Properties > Always-on invariants. Implemented as `public function property_*()` in `{SUITE_DIR}/Properties.sol`. - [ ] **GL-01** — Solvency: the vault's underlying token balance is always at least `vault.totalAssets()`. (Category: HIGH_LEVEL; Guarantee: SHOULD-HOLD — whitepaper §4 "the vault never holds fewer assets than it accounts for"; Priority: HIGH; Sources: CON-01) - [ ] **GL-02** — Sum of per-actor share balances equals `vault.totalSupply()`. (Category: HIGH_LEVEL; Guarantee: SHOULD-HOLD — exact accounting identity: every mint/burn updates both a balance and totalSupply; Priority: HIGH; Sources: CON-02) - [ ] **GL-03** — Share price (`totalAssets/totalSupply`) is monotonically non-decreasing between handler calls. (Category: VARIABLE_TRANSITION; Guarantee: EXPLORATORY; Priority: MEDIUM; Sources: VT-02) ... ## Specific Properties > Operation-gated postconditions. Implemented as `internal function property_*()` in `Properties.sol` and called from the relevant handler after `snapshotAfter()`. - [ ] **SP-01** — After `vault_deposit`, `vault.totalSupply()` strictly increases. (Category: STATE_TRANSITION; Guarantee: SHOULD-HOLD — ERC-4626: `deposit` MUST mint shares to the receiver; After: `vault_deposit`; Priority: HIGH; Sources: ST-01) - [ ] **SP-02** — After a deposit→withdraw round-trip in a single call, the actor's underlying balance does not increase (no free value). (Category: HIGH_LEVEL; Guarantee: EXPLORATORY; After: `vault_roundTrip`; Priority: HIGH; Sources: C2) ... ``` ### Category distribution guidance A healthy property plan usually has at least one property in each category. If after synthesis you have zero `VALID_STATE` properties, re-check whether the protocol has pause/shutdown/recovery/initialization flags that should have generated some — a missing category is usually a gap in discovery, not a property-less protocol. ### property-plan.md (unchanged structure, but now includes IDs) When you write the existing tables in `{META_DIR}/property-plan.md`, prefix each property's row with its PROPERTIES.md ID so implementers can cross-reference. Keep the rest of the format identical: ```markdown # Property Plan > Generated by 5 specialized discovery agents. X properties total. > Priority distribution: N HIGH, N MEDIUM, N LOW ## Global Properties (public, checked by fuzzer after every call) | Spec ID | Function Name | Property | Category | Guarantee | Evidence | Priority | |---------|--------------|----------|----------|-----------|----------|----------| | GL-01 | property_solvency | token.balanceOf(vault) >= vault.totalAssets() | HIGH_LEVEL | SHOULD-HOLD | whitepaper §4 | HIGH | ## Specific Properties (internal, called at end of relevant handlers) | Spec ID | Function Name | Property | Category | Guarantee | Evidence | Called After | Priority | |---------|--------------|----------|----------|-----------|----------|-------------|----------| | SP-01 | property_depositIncreasesShares | totalSupply increased after deposit | STATE_TRANSITION | SHOULD-HOLD | ERC-4626 deposit clause | vault_deposit | HIGH | (`Evidence` is the SHOULD-HOLD justification; leave it blank / `—` for EXPLORATORY rows.) ## Ghost Variable Plan [table from Step 5] ## Snapshot State Plan [table from Step 5] ## Handler Wiring Plan [table from Step 5] ``` Return: `DONE: X properties (N HIGH, N MEDIUM, N LOW). Guarantee: P SHOULD-HOLD, Q EXPLORATORY. Categories: A VALID_STATE, B STATE_TRANSITION, C VARIABLE_TRANSITION, D HIGH_LEVEL. Ghosts: Y variables. Snapshot fields: Z. Handler wiring: W handlers. PROPERTIES.md written with G global + S specific entries (all [ ]).` ## agents/protocol-analyzer.md # Agent: Protocol Analyzer (Step 3 Fallback) **Role**: Perform manual protocol analysis when `x-ray` is unavailable, and produce a `protocol-understanding.md` file that downstream steps (4, 6, 7, 9) can read back as their protocol context. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned ONLY in the Step 3 fallback path when `x-ray` cannot be obtained or did not produce usable documents. --- ## Prompt You are executing the Step 3 fallback for the Fizz skill. The `x-ray` skill was either unavailable or did not produce usable documents, so you must perform manual protocol analysis from source code and write a `protocol-understanding.md` file that downstream steps will read back as their single source of truth for this protocol. ## Your Inputs - Read: `{PROJECT_ROOT}/{META_DIR}/contracts.json` — the in-scope contract inventory produced by Step 2. - Read: all in-scope Solidity source files under `{PROJECT_ROOT}/src/` (or whichever directories are referenced by `contracts.json`). - Read: any existing setup/fixture/deployment scripts under `{PROJECT_ROOT}/` that clarify deployment order or seed state. - Read: protocol-specific helper contracts used by tests (mocks, oracles, etc.) when they clarify real dependencies vs. injected test doubles. ## Your Output Write `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md` with the following sections in this exact order. Downstream steps grep for these headings, so keep them stable. ```markdown # Protocol Understanding: {Protocol Name} ## Summary One paragraph describing what this protocol does, its core primitives, and the actor model. Keep it tight — downstream agents read this to orient themselves. ## Deployment Order Numbered list of the exact order contracts must be deployed and initialized, including any cross-contract dependencies (e.g. "OmniPool must be initialized before any OmniToken.initialize runs, because OmniToken's initialize reads omniPool.reserveReceiver()"). ## Constructor / Init Parameters Per-contract table or sub-section listing every constructor/initialize parameter and what it means. Include validation rules (what the contract requires the value to be) — downstream steps use this to seed realistic fuzzing state. ## Required Post-Deploy Initialization Ordered list of admin/configurator calls that must happen before user-facing handlers will succeed. Examples: `setIRMForMarket`, `setMarketConfiguration`, `setLiquidationBonusConfiguration`, oracle config, approvals, seed deposits. Call out any `assert`/`require` guards in the target contract that a skipped init would trip. ## Actor Roles and Permissioned Actions Table mapping role → holder → permitted actions. Include contract-address-as-caller relationships (e.g. "only OmniPool can call OmniToken.borrow") — downstream handler generation depends on this. ## Required Approvals, Liquidity, and Seed State Bulleted list of everything the harness needs to do BEFORE any handler will produce useful state transitions. Examples: ERC-20 approvals, minted balances, at least one seed deposit per tranche, entered markets, configured oracle prices. ## Real External Entry Points vs Internal Plumbing Three sub-sections: - **Real fuzzing targets**: user-callable state-changing functions that belong in handlers. - **Admin / configurator**: privileged functions to call occasionally from an `asAdmin` handler. - **Internal plumbing**: functions gated on contract-only callers or that are pure helpers — do NOT put these in handlers, they will always revert or do nothing. ## Candidate Invariants Numbered list of AT LEAST 15 candidate invariants in clear English, precise enough that Step 9 agents can turn them into Solidity assertions. Group them by category (Solvency/Accounting, Health/Liquidation, State Transitions, Rounding, Mode/Isolation, IRM, etc.) when the protocol naturally supports the split. Each invariant should state WHAT must hold and WHY a violation would matter. Do not plan ghost variables or snapshot structs yet — Step 9 does that. ``` ## Analysis Guidance Follow these biases: - **Prefer real code evidence over speculation.** If a guard is `msg.sender == omniPool`, say so; don't paraphrase it as "only admin". - **Prefer existing project setup over invented harness logic.** If the project has a deployment script or test fixture that already sequences init, mirror that order. - **Prefer conservative assumptions and targeted TODOs over broad guessing.** If something is ambiguous after reading the source, write `TODO: {specific question}` inline rather than making up an answer. Step 6/7 can resolve it later with more context. - **Cite file paths and line numbers** in the rationale for candidate invariants when they point to a specific assertion or require statement. This makes Step 9 agents much more efficient because they can jump straight to the relevant code. ## Scope Boundaries Do NOT: - Plan full ghost variable layouts, snapshot structs, or implementation details — that is Step 9's job. - Write Solidity sketches for invariants — English descriptions are enough. - Modify any files other than `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md`. - Run `forge build`, `medusa fuzz`, or any other command — you are a pure analysis step. ## Return Value After writing the file, return a one-line summary to the caller: `DONE: protocol-understanding.md written ({N} candidate invariants, {M} entry points identified, {K} post-deploy init steps).` ## agents/report-writer.md # Agent: Report Writer (Step 11) **Role**: Read the completed fuzzing suite outputs (coverage, corpus, campaign logs, properties, handlers) and produce the final `report.md`. This agent runs AFTER `forge build` and the `FoundryTester` sanity test have already passed — it is a pure synthesis/reporting step that does not modify suite files. **Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`). Spawned at the end of Step 11 after validation succeeds. --- ## Prompt You are writing the final fuzzing suite report. Validation (`forge build` and `FoundryTester` sanity test) has already passed — do NOT run those yourself. Your job is to read the generated suite outputs and write `{PROJECT_ROOT}/{META_DIR}/report.md` using the exact structure below. Then print the report content to the caller so it is visible in the main conversation. ## Your Inputs Read these files (skip gracefully if any are missing and write `N/A` in the corresponding report cell): - `{PROJECT_ROOT}/{META_DIR}/protocol-understanding.md` — protocol context (for the Suite Overview name and contracts list) - `{PROJECT_ROOT}/{META_DIR}/contracts.json` — full contract inventory - `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` — the handlers' entry points - `{PROJECT_ROOT}/{META_DIR}/coverage-targets.md` — coverage targets and achieved percentages from Step 8 - `{PROJECT_ROOT}/{META_DIR}/property-plan.md` — synthesized property plan from Step 9c - `{PROJECT_ROOT}/PROPERTIES.md` — English property spec with `[x]` / `[-]` implementation status - `{PROJECT_ROOT}/{META_DIR}/corpus_medusa/medusa-run.log` — campaign log (read the last 200 lines if the file is large) - `{PROJECT_ROOT}/{META_DIR}/corpus_medusa/test_results/` — per-test violation JSON files (list and summarize) - `{PROJECT_ROOT}/{SUITE_DIR}/Properties.sol` — to enumerate implemented properties by function name - `{PROJECT_ROOT}/{SUITE_DIR}/Base.sol` — for setup context (actors, ghosts) - `{PROJECT_ROOT}/{SUITE_DIR}/handlers/` — list handler files with Glob, read each briefly for handler count - `{PROJECT_ROOT}/{SUITE_DIR}/FoundryTester.sol` — for violation repro test results (look for `test_repro_*` functions and whether they passed validation) If the paths above are wrong for this project (e.g. a different fuzzer was used, or files live under a different meta dir), adapt — prefer reading whatever exists over erroring out. ## Report Structure Write `{PROJECT_ROOT}/{META_DIR}/report.md` with these exact sections in this exact order. Downstream tooling and humans both scan for these headings. ```markdown # Fuzzing Suite Report ## Suite Overview - **Project**: {protocol name from protocol-understanding.md} - **Suite location**: {SUITE_DIR, typically `test/fizz/`} - **Contracts targeted**: {comma-separated list of in-scope contracts} - **Total handlers**: {count} ({primary} primary, {secondary} secondary/dispatcher) - **Properties**: {count} ({global} global, {specific} function-specific) ## Coverage Results | Contract | Target | Achieved | Status | |----------|--------|----------|--------| | ... | 80% | 85% | ✅ | | ... | 80% | 71% | ⚠️ | | ... | 80% | 47% | ❌ | Status legend: ✅ if achieved ≥ target (or intentional skip), ⚠️ if within 10 points below target, ❌ if more than 10 points below target. ## Skipped Paths | Contract | Function / Path | Reason | |----------|----------------|--------| | ... | ... | ... | Populate with contracts/functions that were intentionally excluded (mock substitutions, out-of-scope dependencies, admin-only paths not wired to handlers). ## Campaign Results - **Fuzzer used**: {Medusa/Echidna} - **Duration**: {time} - **Total calls**: {if available from log} - **Branches hit**: {if available} - **Corpus size**: {if available} - **Violations found**: {count} ### Violation Details For each distinct violation root cause (NOT each reproduction), write a sub-section with: - **Property violated**: {name} - **Guarantee**: `SHOULD-HOLD` | `EXPLORATORY` (look up the violated property's tag in `PROPERTIES.md` by its Spec ID / function name) - **Assertion**: {the exact check that failed} - **Root cause**: {your best-guess explanation based on the reproducing call sequence} - **Severity assessment**: `protocol bug` | `test harness false positive` | `needs human review` - **Reproducing sequence**: {shrunk call sequence from the corpus} - **Foundry repro**: `test_repro_{propertyName}` in `FoundryTester.sol` — `PASS` (violation reproduces) / `FAIL` (did not reproduce, see TODO in test) / `N/A` (no violations) **Use the Guarantee tag to anchor the severity assessment** (after first ruling out a harness/property bug): - A violated **SHOULD-HOLD** property means a documented or mathematically-guaranteed invariant broke → default to `protocol bug` unless the repro proves the assertion itself is wrong (then `test harness false positive`, with the fix). - A violated **EXPLORATORY** property is an inferred assumption that did not hold → default to `needs human review`; only call it `protocol bug` when the root cause clearly shows real value loss / broken safety, and only `test harness false positive` when the inferred property was simply too strong (say so explicitly). If multiple stored failures share the same root cause, group them under one sub-section and note the count. ## Properties Implemented | # | Property | Type | Guarantee | Confidence | |---|----------|------|-----------|------------| | ... | property_solvency | Global | SHOULD-HOLD | HIGH | | ... | _prop_depositIncreasesShares | Specific | EXPLORATORY | MEDIUM | Enumerate every property that appears in `Properties.sol` (both `property_*` global functions and `_prop_*` internal specifics). `Guarantee` is the generation-time tag — copy it verbatim from `PROPERTIES.md` (`SHOULD-HOLD` / `EXPLORATORY`) by matching the property's Spec ID / function name; write `N/A` if the property is not in `PROPERTIES.md`. It records whether a violation would be a confirmed bug (SHOULD-HOLD) or a human-review lead (EXPLORATORY). `Confidence` is your own assessment of how robustly the *assertion is written* (orthogonal to Guarantee) — HIGH/MEDIUM/LOW: - **HIGH**: strict assertion, correct tolerance, exercises a meaningful invariant. - **MEDIUM**: assertion is correct but has soft tolerances (e.g. `+1` wei slack, `110%` of cap), or does not cover all reachable actors. - **LOW**: property is a stub that returns `true` without asserting anything, or the assertion is trivially satisfied. If `PROPERTIES.md` exists, cross-reference implementation status: `[x]` implemented, `[-]` skipped/manual, `[ ]` pending. ## Open TODOs Scan the generated suite files under `{PROJECT_ROOT}/{SUITE_DIR}/` (Base.sol, Snapshots.sol, Properties.sol, all handler files) for `TODO` comments and list them with file:line references. ## Next Steps Actionable recommendations ordered by priority. At minimum, address: 1. Any `test harness false positive` violations found in Campaign Results — specify the exact fix. 2. Any LOW-confidence properties from the Properties Implemented table — specify how to strengthen them. 3. Any contract with ❌ coverage status — specify which uncovered functions would most improve coverage. 4. Any open TODO that blocks production readiness. 5. Recommended campaign duration for production validation (current run vs. recommended). ``` ## Writing Style - Be precise with numbers. Do NOT invent figures. If a number is missing from the inputs, write `N/A` or `Not Available`. - Keep the tone factual and terse — this is a report, not marketing. One-sentence bullets are usually enough. - When you classify a violation as `test harness false positive`, cite the specific timing/rounding/accounting reason and propose the fix. Never classify a real protocol bug as a false positive. - When you assign a property confidence level, cite the specific reason in a trailing note (e.g. "1-wei tolerance may mask small drift", "iterates only the 3 fuzzed actors — misses liquidator/reserve accounts"). ## After Writing the File Also remind the user of the commands to run campaigns manually, exactly as SKILL.md Step 11 specifies: - `medusa fuzz` (from project root) - `echidna {SUITE_DIR}/FuzzTester.sol --contract FuzzTester --config echidna.yaml` (if echidna is configured) ## Return Value After writing the file, print the full report content to the caller (so the human sees it in the main conversation without needing to open the file), then return a one-line summary: `DONE: report.md written ({N} properties, {M} violations, {K} contracts, overall status: {PASS / FAIL / PARTIAL}).` ## evals ``` ``` ## evals/evals.json ```json { "skill_name": "fizz", "evals": [ { "id": 0, "name": "full-run", "prompt": "Generate a fuzz suite for the project at {TARGET_PROJECT_PATH}", "expected_output": "A complete fuzz suite under test/fizz/ with handlers, properties, and a passing Medusa campaign", "files": [], "assertions": [] }, { "id": 1, "name": "targeted-no-invariants", "prompt": "Generate fuzz handlers for the Vault and StakingRewards contracts in {TARGET_PROJECT_PATH}, skip invariants", "expected_output": "Handlers for Vault and StakingRewards under test/fizz/handlers/, no properties generated, Medusa coverage run completed", "files": [], "assertions": [] } ] } ``` ## references ``` ``` ## references/handler-patterns.md # Handler Patterns Use this guide during Step 7. ## Shape Each handler file should have two sections: - `Unclamped`: raw protocol-action functions that perform the target call with unrestricted parameters - `Clamped`: handlers that restrict arbitrary fuzz input into sensible, high-signal calls Both sections may be called by the fuzzer. The unclamped section is not just an internal helper layer: unclamped handlers are also direct fuzz entry points, specifically so the campaign can still hit edge cases that the clamped layer intentionally filters out. The clamped layer should stay thin and usually forward into the corresponding unclamped function. The unclamped layer should usually just perform the target call with the appropriate acting modifier. ## Unclamped The `Unclamped` section is the raw-call layer. Use it to: - perform the real target function call with unrestricted parameters - expose edge-case behavior that clamped variants intentionally avoid - apply the correct acting modifier or caller role - stay as close as possible to a raw call wrapper These functions are meant to be called both: - directly by the fuzzer, with unrestricted parameters - indirectly by the clamped handlers, after those handlers have prepared sensible inputs Unclamped handlers should stay close to the actual protocol surface. They should usually be thin raw calls plus the necessary role modifier and call to internal specific properties, if applicable. "Unclamped" describes their role in the handler structure, not their Solidity visibility. ### Caller Context Use the acting context that matches the real role here: - `asActor` for users - `asAdmin` for owner or admin operations - role-specific modifiers for keepers, operators, reward distributors, or liquidators If the scaffold lacks a needed role modifier, add it. This is required even for raw unclamped handlers. Unrestricted parameters do not mean unrestricted caller identity. ## Clamped The `Clamped` section is the restricted-input layer of the handler. Use it to: - expose the small set of high-signal protocol actions that the fuzzer should call - normalize arbitrary fuzz inputs into values that can reach meaningful code paths - prepare derived values before dispatching into the unclamped implementation - prepare preconditions that the target action expects, then forward into the corresponding unclamped function whenever practical ### Clamped Design Do not mirror the ABI mechanically if a higher-signal handler shape is better. Good transformations: - merge preparatory steps and the main user action into one handler if the protocol expects them together - split one overloaded or ambiguous flow into clearer variants if that improves coverage - derive parameters from current state when raw fuzzed values mostly cause trivial reverts ### Clamped Input Handling Prefer semantic bounds over arbitrary caps. Clamp toward values that are realistic for the protocol and likely to reach meaningful state transitions. Use the helper functions from `utils/Clamp.sol` for this layer. Those helpers are part of the scaffold specifically so clamped handlers can bound fuzz inputs consistently with functions such as `clampBetween`, `clampLte`, `clampLt`, `clampGte`, and `clampGt`. Examples: - map arbitrary addresses to known actors with `toActor(...)` and `toActorNotCurrent(...)` - if a function expects a valid identifier such as an order id, position id, market id, or pool id, pick from known valid values instead of passing arbitrary garbage - if a function will pull ERC20s from the caller, bound the amount by the caller's token balance and set the needed approval before calling the unclamped function - bound spend amounts by balances or allowances - bound share burns by owned shares - bound deadlines so the call can reach meaningful code paths - use source constants and require guards when they expose real bounds Clamped handlers should usually avoid doing the raw protocol call inline. Prefer to finish argument preparation and then call the unclamped version. If the correct bound is unclear, keep the clamp loose and leave a targeted `// TODO: tighten bound`. ### Donation Handlers - If the protocol manages native tokens, include a special `_donateETH` handler that accepts an arbitrary amount and sends it to the protocol using `Actor.forceSendETH(...)`. - If the protocol manages ERC20 tokens, include a special `_donateERC20` handler that accepts an arbitrary amount and (optionally) token address and sends it to the protocol. ## Boundary-Value Stress Handlers For every clamped handler, generate **stress variants** that target the extremes of the input domain. Clamped handlers focus on "sensible" ranges to maximize meaningful state transitions, but bugs cluster at the boundaries those clamps filter out. Stress handlers exist to hit those boundaries. The approach is always the same: read the function's code path, identify where the math can degenerate, and write a handler that drives input to that boundary. There are four directions to check. ### 1. Near-Zero / Sub-Unit Values When a code path involves division or decimal conversion, values near or below the divisor truncate to zero. This creates free-value bugs (user pays nothing, receives tokens) or division-by-zero reverts. **How to detect**: grep the target contracts for division (`/`), `mulDiv`, decimal scaling (`10**`, `1eN`), or conversion functions. Note the divisor. Any input smaller than that divisor will truncate. ```solidity // Generic pattern: if the function divides by SCALE_FACTOR, test below it function contract_action_smallAmount(uint256 amount) public { // Clamp to values near the truncation boundary amount = clampBetween(amount, 1, SCALE_FACTOR); contract_action(amount); } ``` ### 2. Full-Amount / Max-State Operations Protocols often work fine for partial operations but break when the entire balance, debt, or supply flows through a single path. Generate handlers that use the maximum available amount from current state: ```solidity function contract_fullWithdraw() public { uint256 fullBalance = contract.balanceOf(actor); if (fullBalance == 0) return; contract_withdraw(fullBalance); } function contract_fullAction(uint256 auxParam) public { uint256 maxAmount = contract.totalAvailable(); if (maxAmount == 0) return; contract_action(maxAmount, auxParam); } ``` ### 3. Type-Boundary Values Before writing handlers, grep the target contracts for storage variables that use types narrower than uint256 — `uint8`, `uint80`, `uint96`, `uint128`, `uint160`, or packed struct fields. When a value accumulates via uint256 arithmetic but is stored or cast to a narrower type, the truncation is invisible until the accumulated value exceeds the type's max. For each narrow-typed accumulator, create a handler that pushes values large enough to approach or exceed the type boundary through the accumulation path. Derive the bound from the type max (e.g., `type(uint80).max` is ~1.2e24), not from hardcoded protocol-specific constants. ### How to Apply For each clamped handler, ask: 1. Does this path involve division or scaling? → add a **near-zero** variant 2. Can this be called with the full available amount? → add a **full-amount** variant 3. Does this path write to a narrow-typed storage variable? → add a **type-boundary** variant Not every handler needs all three — only add variants where the code path has the relevant pattern. ### Admin Handlers For admin/owner functions, always use the correct caller context: ```solidity function protocol_setFee(uint256 fee) public asAdmin { protocol.setFee(fee); } ``` Admin handlers must use `asAdmin` (or the appropriate role modifier) — not `asActor`. If no `asAdmin` modifier exists in the scaffold, add one that pranks as the contract owner. ## Dispatcher for Secondary-Tier Functions Secondary-tier functions appear as `internal` stubs (prefixed `_`) in the Unclamped section, and a single public dispatcher at the end of the Clamped section. The dispatcher is a single clamped entry point that uses a `uint8 selector` parameter to pick which secondary function to call: ```solidity function vault_secondary(uint8 selector, uint256 arg0, address arg1) public { selector = uint8(selector % 3); if (selector == 0) _vault_setPaused(arg0 > 0); else if (selector == 1) _vault_setFee(arg0); else _vault_setAdmin(arg1); } ``` The unclamped secondary functions are all `internal` and not direct fuzz entry points. This reduces the secondary functions' call frequency naturally — the fuzzer reaches them only when it happens to pick the matching selector value. Primary-tier functions get their own individual clamped + unclamped handlers as normal. ## Example ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import "../Base.sol"; import {Properties} from "../Properties.sol"; /// @notice Handles the interaction with a specific contract abstract contract VaultHandler is Properties { // ――――――――――――――――――――――――― Clamped ―――――――――――――――――――――――――― function vault_deposit_clamped(uint256 amount) public { uint256 balance = token.balanceOf(actor); if (balance == 0) return; amount = clampBetween(amount, 1, balance); vault_deposit(amount); } function vault_donateETH(uint256 amount) public { if (actor.balance == 0) return; amount = clampBetween(amount, 1, actor.balance); Actor(actor).forceSendETH{value: amount}(address(vault)); } function vault_donateERC20(uint256 amount) public { uint256 balance = token.balanceOf(actor); if (balance == 0) return; amount = clampBetween(amount, 1, balance); vm.prank(actor); token.transfer(address(vault), amount); } // ―――――――――――――――――――――――― Unclamped ――――――――――――――――――――――――― function vault_deposit(uint256 amount) public asActor { vault.deposit(amount); } } ``` ## references/property-generation.md # Property Generation Common instructions for generating properties, ghost variables, snapshot state, and harness contracts after handlers are in place. These rules apply to both global properties and specific properties. This phase runs after handler generation. The agent reads the target contract source files and the generated handlers to produce: **Ghost variables** in `Base.sol` — track cumulative state not directly readable from the contract. **Ghost updates** wired into per-contract handler files (`handlers/Handler.sol`). **Snapshot state** in `Snapshots.sol` — before/after state for delta-based properties. **Harness contracts** in `{SUITE_DIR}/harness/` — for accessing private/internal state when necessary. **Properties** in `Properties.sol` — global and function-specific invariant checks, called explicitly from handlers or shared helper functions. ## 1. Naming convention All property functions must start with `property_` prefix. ## 2. Ghost Variables ### What they are Ghost variables track state that the contract doesn't expose directly but that is needed to write meaningful invariants. Common examples: - `ghosts.totalDeposited` — sum of all deposits across all actors - `ghosts.totalWithdrawn` — sum of all withdrawals - `ghosts.totalMinted` — cumulative minted amount - `ghosts.lastTimestamp` — timestamp of last state-changing call ### Where they go In `Base.sol`, inside the `Ghosts` struct: ```solidity struct Ghosts { uint256 totalDeposited; uint256 totalWithdrawn; uint256 totalMinted; } ``` Replace the placeholder `uint256 _placeholder;` with real ghost variables. ### How to choose ghosts Read the source contracts and identify: - **Accumulative operations**: deposits, withdrawals, mints, burns, transfers — track running totals. - **Counter operations**: number of users, number of positions — track counts. - **Extreme values**: max/min seen amounts — track with `max()`/`min()` in handlers. Only add ghosts that are needed by at least one property. Don't add speculative ghosts. ### Wiring ghost updates into handlers Add ghost updates AFTER the external call in each handler (so they only execute on success). For clamped handlers that forward to unclamped: put ghost updates in the UNCLAMPED handler (since both clamped and direct fuzzer calls go through it). Ghost updates go in the per-contract handler files (`handlers/Handler.sol`). Example: ```solidity function vault_deposit(uint256 assets) public asActor { assets = clampBetween(assets, 1, token.balanceOf(address(actor))); vm.prank(address(actor)); vault.deposit(assets); ghosts.totalDeposited += assets; } ``` ## 3. Snapshot State ### Purpose `Snapshots.sol` captures state before and after a handler call, enabling delta-based properties like "user balance decreased by exactly the deposit amount." ### What to track Read the target contracts and populate the `State` struct with: - Key balances: `token.balanceOf(address)`, `contract.balanceOf(address)` - Protocol state: `totalSupply`, `totalAssets`, `totalShares` - Actor state: balances of the current actor Example: ```solidity struct State { uint256 actorTokenBalance; uint256 vaultTotalAssets; uint256 vaultTotalSupply; } function _takeSnapshot(State storage state) private { state.actorTokenBalance = token.balanceOf(actor); state.vaultTotalAssets = vault.totalAssets(); state.vaultTotalSupply = vault.totalSupply(); } ``` Snapshot reads must NOT revert. Use try/catch for any call that could fail. ### Wiring snapshots into handlers For handlers that need before/after comparison, call `snapshotBefore()` before the external call and `snapshotAfter()` after it. The full wiring sequence in an unclamped handler is: 1. `snapshotBefore()` — capture state before the call 2. External call — the actual protocol interaction 3. `snapshotAfter()` — capture state after the call 4. Ghost updates — track derived state (only executes on success) 5. Property assertions — call specific properties that check deltas ```solidity function vault_deposit(uint256 assets) public asActor { snapshotBefore(); vm.prank(address(actor)); vault.deposit(assets); snapshotAfter(); ghosts.totalDeposited += assets; property_depositIncreasesShares(assets); } ``` Do NOT add snapshot calls to every handler — only where delta-based properties exist. They cost gas and slow fuzzing. ## 4. Harness Contracts If a property requires access to `private` or `internal` state that is not reachable via the public interface, create a harness contract: - Place it at `{SUITE_DIR}/harness/{TargetContract}Harness.sol` - The harness inherits from the target contract and adds only the minimal getter(s) needed - Update `Base.sol` to declare and instantiate `{TargetContract}Harness` instead of `{TargetContract}` — the harness is ABI-compatible so handlers and properties continue to work unchanged - Only create a harness when strictly necessary — prefer public interface access ## 5. Assertion helpers These are the assertion helpers from `utils/PropertiesAsserts.sol`: | Function | Check | |---|---| | `t(bool, string)` | assert true | | `eq(a, b, reason)` | `a == b` | | `neq(a, b, reason)` | `a != b` | | `gt(a, b, reason)` | `a > b` | | `gte(a, b, reason)` | `a >= b` | | `lt(a, b, reason)` | `a < b` | | `lte(a, b, reason)` | `a <= b` | All have both `uint256` and `int256` overloads. All emit descriptive failure events before `assert(false)`. ## references/selection-policy.md # Entry-Point Selection Policy Use this policy when creating the initial `entry-point-selection.json`. ## Goal Select the smallest handler surface that still exercises the protocol's real state machine. ## Prefer By Default - core user flows such as `deposit`, `withdraw`, `mint`, `redeem`, `borrow`, `repay`, `stake`, `unstake`, `swap`, `claim` - recurring permissioned flows such as `harvest`, `liquidate`, `rollover`, `notifyRewardAmount`, `rebalance`, `settle` - edge-case actions that plausibly break accounting, mode transitions, or fund safety ## Exclude By Default - `view` and `pure` functions - one-time migration and bootstrap functions - internal plumbing exposed as `external` only for contract-to-contract calls - routine parameter setters that mostly tune config without creating meaningful state-machine pressure ## Include Carefully Keep a permissioned or config-like action when one of these is true: - it changes fund routing, fee accounting, caps, oracle state, or collateral rules - it toggles pause, shutdown, or mode flags - sequencing it against user flows is plausibly dangerous - it is part of normal operations for keepers, liquidators, or reward distributors ## Decision Heuristics For each candidate function, ask: 1. Would a real user, admin, keeper, operator, or liquidator call this directly? 2. Does this function create or unlock important state transitions? 3. Would omitting it make the fuzz campaign miss an important lifecycle edge? 4. Is it mostly internal wiring that should instead be exercised indirectly through another entry point? If confidence is low, prefer excluding protocol-internal plumbing and keeping the higher-signal external flows. ## Tier Classification After selection, classify each included function as **primary** or **secondary**: - **Primary**: core user flows that the fuzzer should call frequently (deposit, withdraw, mint, redeem, borrow, repay, swap, stake, unstake, claim, liquidate, etc.) - **Secondary**: less common functions that are still useful but should be called less often (admin setters, configuration changes, pause/unpause, role grants, parameter tuning, etc.) Secondary functions are grouped into a dispatcher handler in Step 7, reducing their call frequency without excluding them entirely. ## references/setup-playbook.md # Setup Playbook Use this guide during Step 6 when wiring `Base.sol` and `Actor.sol`. ## Base.sol FIXMEs The scaffolded `Base.sol` contract contains `FIXME` comments that indicate where protocol-specific setup logic should be implemented. Treat those `FIXME`s as required integration points. ## Source Priority Look for existing project setup logic before inventing new deployment code. Read in this order when available: 1. integration tests 2. base test fixtures 3. deployment scripts 4. helper contracts used by tests If none of the above exist, scan for initialize() signatures and constructor arguments directly in source files. ## Extract From Existing Setup - deployment order - constructor argument meaning - role grants and ownership transfers - initialization or upgrade calls - seed state such as approvals, liquidity, balances, oracle values, and reward funding ## Good Defaults - reuse real in-protocol dependencies when the protocol already contains them - use mocks only for genuinely external systems or missing infrastructure - use mock contracts when appropriate for dependencies that are external to the protocol or unnecessarily complex for the harness - good mock candidates include external tokens, external oracles, and complex third-party contracts that are not the main subject of the fuzz campaign - when the missing dependency is a simple external ERC20 token, prefer the scaffolded `utils/MockERC20.sol` helper unless the project already contains a more faithful token mock - grant actors enough balances and approvals to reach meaningful state transitions - prefer deterministic constants over random setup branches ## Upgradeable Contracts Before writing setup logic, check whether the target contracts use upgradeable proxies. Strong signals: - `_disableInitializers()` in a constructor - an `initialize()` function protected by `initializer` - versioned initialization functions protected by `reinitializer` If the contract is upgradeable: - use the project's proxy pattern such as `TransparentUpgradeableProxy` or `ERC1967Proxy` - deploy the implementation first, then the proxy with initialization calldata - use a dedicated proxy admin address that never calls implementation functions directly If the contract is not upgradeable, plain `new Contract(args)` deployment is fine. ## Setup Checklist At minimum, wire: - deployment order - constructor arguments - proxy deployment and initialization when needed - registry or service-locator wiring - role grants and ownership transfers, including scoped roles when applicable - token approvals and seed balances - any required initialization calls - market, pool, or strategy configuration needed for handlers to reach meaningful states Deploy all in-protocol dependencies needed by the selected entry points, even if those dependencies do not get handlers. ## Signature-Dependent Setup If selected entry points require cryptographic signatures such as signed prices, signed orders, or permit signatures: - store a known private key constant in `Base.sol` for the signer or publisher role - register the corresponding address as an approved signer during setup - expect handlers in Step 7 to use `vm.sign(privateKey, digest)` to construct valid payloads - if router-layer signature construction is too complex for the harness, consider targeting the underlying manager functions directly and document that tradeoff ## TODO Rule Leave `// TODO` only when: - the dependency is truly external and the correct mock or fork source is project-specific - the constructor needs a business value that cannot be inferred safely - the protocol needs a privileged operational decision that should come from the user Every TODO should say what is missing and why it blocks a safe default. ## references/template-map.md # Template Map Maps each generated file to its role in the inheritance chain and generation phase. ## Inheritance Chain ``` Base (is StringUtils, Clamp, Deployer, Math) └─► Snapshots (is Base) └─► Properties (is PropertiesAsserts, Snapshots) └─► Handler (is Properties) — one per target contract └─► Handlers (is ) — aggregator + actor switching ├─► FuzzTester (is Handlers) — Echidna/Medusa entry point └─► FoundryTester (is Test, Handlers) — Foundry quick debug/PoC entry point ``` ## File Descriptions ### Core files (scaffolded, then refined) | File | Phase | Role | |---|---|---| | `Actor.sol` | Step 5 + Step 6 | Actor contract representing a user. Holds ETH, has `forceSendETH`, ERC-721/1155 receivers, flash loan callback. Copied in Step 5 and then modified with protocol-specific approvals and setup needs. | | `Base.sol` | Step 5 + Step 6 + Step 9 | Constants, state variables, ghost struct, actor management, contract instances. Copied in Step 5, wired in Step 6, and extended in Step 9. | | `README.md` | Step 5 | Reader-facing overview of the generated suite, its key files, and the standard commands to run it. Intended for users or agents who did not build the harness originally. | | `Snapshots.sol` | Step 5 + Step 6 + Step 9 | Before/after state tracking. Copied in Step 5, kept minimal in Step 6, and populated during invariant generation. | | `Properties.sol` | Step 5 + Step 6 + Step 9 | Property container. Copied in Step 5, kept minimal in Step 6, and populated with checks in Step 9. | | `handlers/Handlers.sol` | Step 5 + Step 6 + Step 7 | Aggregator copied in Step 5, then populated from the selected contracts so it imports and inherits all generated handler stubs. It can be adjusted in Step 6 if needed and refined again in Step 7. | | `handlers/Handler.sol` | Step 5 + Step 7 | Per-contract handler file in `{SUITE_DIR}`. Stub handler templates are generated in Step 5 from `fizz_data/entry-point-selection.json`, then replaced or rewritten in Step 7. | | `harness/Harness.sol` | Step 9 (conditional) | Harness contract that inherits from a target contract and exposes private/internal state needed by a property. Created only when strictly necessary. When present, `Base.sol` instantiates the harness instead of the target contract. | | `FuzzTester.sol` | Step 5 | Echidna/Medusa entry point. Copied in Step 5 and never modified. Inherits everything through `Handlers`. | | `FoundryTester.sol` | Step 5 | Foundry quick debug and PoC harness. Copied in Step 5 and never modified structurally, but used actively during Step 8 and Step 10 to debug coverage gaps and validate hypotheses. Inherits everything through `Handlers`. | ### Workflow metadata (generated during the workflow) | File | Phase | Role | |---|---|---| | `fizz_data/contracts.json` | Step 2 | Extracted contract/function inventory used as the structural input for selection and later analysis. | | `fizz_data/entry-point-selection.json` | Step 4 | Auto-accepted selection of contracts and functions that limits handler generation only. | | `fizz_data/protocol-understanding.md` | Step 3 fallback | Persisted protocol understanding notes when `x-ray` is unavailable or insufficient. | ### Utility files (static, not edited) | File | Role | |---|---| | `utils/Clamp.sol` | Clamping functions: `clampBetween`, `clampLt`, `clampLte`, `clampGt`, `clampGte` (uint256 + int256). | | `utils/Hevm.sol` | Cheatcode interface (`vm.prank`, `vm.roll`, `vm.warp`, `vm.label`, etc.). | | `utils/PropertiesAsserts.sol` | Assertion helpers for properties: `t()`, `eq()`, `neq()`, `gt()`, `gte()`, `lt()`, `lte()`. | | `utils/Logger.sol` | Event-based logging for fuzzer trace output. | | `utils/Math.sol` | Math helpers (`abs`, etc.). | | `utils/StringUtils.sol` | Number-to-string conversion for log messages. | | `utils/Deployer.sol` | Deployment helpers. | | `utils/DecimalPrinter.sol` | Decimal formatting for uint values. | | `utils/EnumerableSet.sol` | OpenZeppelin-style enumerable set for tracking addresses/uints. | | `utils/MockERC20.sol` | Simple mintable ERC20 mock for external token dependencies, seeded balances, and token-donation edge cases in the generated harness. | ### Config files (project root) | File | Role | |---|---| | `echidna.yaml` | Echidna fuzzer configuration. Points to `FuzzTester` as test target. | | `medusa.json` | Medusa fuzzer configuration. Points to `FuzzTester` as test target. | ## Output Structure ``` fizz_data/ ├── contracts.json # Extracted contract/function inventory ├── entry-point-selection.json # Auto-accepted handler-generation scope ├── protocol-understanding.md # Fallback understanding notes when needed ├── corpus_echidna/ ├── corpus_medusa/ ├── crytic-export/ ├── logs_medusa/ └── ... ./ ├── echidna.yaml ├── medusa.json └── ... test/fizz/ ├── README.md # Human/agent-oriented suite overview and runbook ├── Actor.sol ├── Base.sol # Contract declarations, setup, ghosts, helpers ├── Properties.sol # Invariant checks ├── Snapshots.sol # Before/after state tracking ├── FuzzTester.sol # Echidna/Medusa entry point ├── FoundryTester.sol # Foundry quick debug/PoC harness ├── handlers/ │ ├── Handlers.sol # Aggregator — inherits all per-contract handlers │ ├── VaultHandler.sol # Example: handlers for Vault contract │ └── TokenHandler.sol # Example: handlers for Token contract ├── harness/ # Optional — only created when properties need private/internal access │ └── VaultHarness.sol # Example: exposes internal state from Vault └── utils/ ├── Clamp.sol # Clamping helpers (clampBetween, clampLt, etc.) ├── DecimalPrinter.sol ├── Deployer.sol ├── EnumerableSet.sol ├── Hevm.sol # Cheatcode interface ├── Logger.sol ├── Math.sol ├── MockERC20.sol # Mintable ERC20 mock for external token dependencies ├── PropertiesAsserts.sol └── StringUtils.sol ``` ## Generation Phases Summary 1. **Template copy** — The full template scaffold and fuzzer config are copied into place. 2. **Core refinement** — `Base.sol`, `Actor.sol`, `Snapshots.sol`, `Properties.sol`, and `Handlers.sol` are modified to match the target protocol. `FuzzTester.sol` is the static fuzzer entry point — copied once and never modified. `FoundryTester.sol` is the debugging harness — also never modified structurally, but used actively in Steps 8 and 10. 3. **Handler gen** — Selected-contract handler stubs are replaced with protocol-specific handlers, and `Handlers.sol` is refined with the final imports and inheritance. 4. **Invariant gen** — `Properties.sol` gets invariant checks, `Snapshots.sol` gets tracked state, `Base.sol` gets ghosts, and handler files get ghost and snapshot wiring. ## scripts ``` ``` ## scripts/ensure_foundry.sh ```bash ``` ## scripts/estimate_cost.js ```js ``` ## scripts/extract_abis.js ```js ``` ## scripts/fizz_sync.js ```js ``` ## scripts/generate_handlers.js ```js ``` ## scripts/generate_suite.js ```js ``` ## scripts/lib ``` ``` ## scripts/lib/log-viewer.js ```js ``` ## scripts/run_echidna.js ```js ``` ## scripts/run_medusa.js ```js ``` ## scripts/select_functions.js ```js ``` ## scripts/setup_fuzz_profile.sh ```bash ``` ## skills ``` ``` ## skills/fizz-convert ``` ``` ## skills/fizz-convert/SKILL.md --- name: fizz-convert description: Convert English-language properties in PROPERTIES.md (produced by the Fizz skill) into Solidity assertions inside the existing fuzz harness, then flip their checkboxes. Trigger on "fizz-convert", "convert properties", "implement properties from PROPERTIES.md", "convert PROPERTIES.md to Solidity". --- # Property Conversion Skill — fizz-convert You are an expert Solidity fuzzing engineer working inside a project that was set up by the **Fizz** skill. Your job is to convert English-language properties in `PROPERTIES.md` (project root) into Solidity code inside the existing harness, then flip their checkboxes from `[ ]` to `[x]`. **Arguments**: optional space-separated property IDs (e.g., `GL-01 SP-03`) passed when the user invokes the skill. If no IDs are given, convert ALL properties currently marked `[ ]`. ## Parameters - `SUITE_DIR`: Solidity suite directory relative to project root (default: `test/fizz`). Use the same value that was passed to the `fizz` skill when the harness was generated. - `META_DIR`: Metadata directory relative to project root (default: `fizz_data`). Use the same value that was passed to the `fizz` skill. ## Checkbox states and how they map to actions `PROPERTIES.md` uses three states. The action you take depends on BOTH the current checkbox AND whether tagged Solidity for that Spec ID already exists in `Properties.sol` / handlers. **Tagged Solidity** = a function whose natspec starts with `/// @notice :` (e.g. `/// @notice GL-05:`). The implementer agents are required to emit this doctag for every property they write, so it is the canonical way to find the existing code for any Spec ID. Search both `{SUITE_DIR}/Properties.sol` and every file under `{SUITE_DIR}/handlers/`. Action matrix: | Current checkbox | Tagged Solidity exists? | Action | |---|---|---| | `[ ]` | NO | **Implement fresh.** Normal pending case. On success → `[x]`. On infeasible/skip → `[-]`. | | `[ ]` | YES | **Regenerate.** The user manually downgraded `[x]`→`[ ]` because they want it re-implemented (description changed, prior impl was wrong, etc.). Delete the existing tagged function AND any handler call sites (for `SP-*`), then implement fresh as if it were the row above. On success → `[x]`. | | `[x]` | YES | **Skip.** Already implemented. Never re-implement, never overwrite. If the user explicitly listed this ID in arguments, warn and skip. | | `[x]` | NO | **DRIFT — stop and warn.** The spec claims it's done but no tagged Solidity exists. This means either the user deleted the function manually without updating PROPERTIES.md, or the doctag was lost. Do NOT silently rewrite the spec. Print a warning naming the ID and ask the user to either restore the function, flip the checkbox to `[ ]`, or flip it to `[-]`. Skip this ID for the rest of this run. | | `[-]` | NO | **Leave alone.** Manual / do-not-touch. Never read as a target, never flip, never write Solidity. If the user explicitly listed a `[-]` ID, refuse and tell them to flip it to `[ ]` first. | | `[-]` | YES | **Drop.** The user manually downgraded `[x]`→`[-]` because they want the property removed entirely. Delete the existing tagged function AND any handler call sites (for `SP-*`). Leave the checkbox as `[-]`. Report under "Dropped" in the summary. | **Hard rule**: never modify a `[x]`+YES line and never flip `[x]`→anything automatically except as part of a build-failure rollback for a property you generated in the same run. --- ## STEP 1: READ CURRENT STATE Read in parallel: 1. `PROPERTIES.md` (project root) — the source of truth for what needs to be converted 2. `{SUITE_DIR}/Properties.sol` — where property functions live 3. `{SUITE_DIR}/Base.sol` — for the `Ghosts` struct, `actors` array, `NUMBER_OF_ACTORS`, available contract instances 4. `{SUITE_DIR}/Snapshots.sol` — for the `State` struct, `stateBefore` / `stateAfter`, and `_takeSnapshot` 5. `{SUITE_DIR}/handlers/` — every handler file, to see existing function names, `snapshotBefore()` / `snapshotAfter()` placement, and ghost update conventions 6. `{META_DIR}/property-plan.md` if it exists — for the ghost/snapshot/wiring tables that back each Spec ID 7. The relevant in-scope source contracts (only the ones referenced by the properties you are about to convert) If `PROPERTIES.md` does not exist at the project root, stop and tell the user to run the Fizz skill (Step 9) first. --- ## STEP 1.5: RECONCILE SPEC WITH CODE For every Spec ID in `PROPERTIES.md` (regardless of checkbox state), check whether tagged Solidity exists. The doctag pattern is exact: ``` /// @notice GL-NN: /// @notice SP-NN: ``` Grep `{SUITE_DIR}/Properties.sol` and `{SUITE_DIR}/handlers/**/*.sol` for each pattern. Build a single in-memory map: `spec_id → {checkbox, has_tagged_solidity, function_name_if_found, file_if_found, handler_call_sites_if_SP}`. Then classify each ID against the action matrix above. The four action types are: - **IMPLEMENT** (`[ ]` + NO Solidity) — process in STEP 4 normally. - **REGENERATE** (`[ ]` + Solidity) — first delete, then process in STEP 4. - **DROP** (`[-]` + Solidity) — delete only, no STEP 4 work. - **DRIFT_WARN** (`[x]` + NO Solidity) — print a warning and skip this ID. Do NOT touch the checkbox. - **SKIP** (`[x]` + Solidity, or `[-]` + NO Solidity) — no work. ### Deletion procedure (used by REGENERATE and DROP) For a Spec ID whose tagged Solidity must be removed: 1. **Locate the function block** in `Properties.sol`. Start at the line `/// @notice :` and read upward to capture any preceding `///` natspec lines that belong to the same block. Read downward through the function signature and body until the matching closing `}` at the function's brace depth. Delete the entire span (natspec + signature + body), plus any single blank line immediately following. 2. **For `SP-*` only**, scan every file under `{SUITE_DIR}/handlers/` for call sites of the deleted function name. The grep target is the bare function name followed by `(` (e.g. `property_depositIncreasesTotalSupply(`). Delete each such call line. If the call has surrounding comments specific to that property (e.g. `// SP-01 postcondition`), delete those too. 3. **Do not touch** any other functions, ghost variables, or snapshot fields. If the deleted property was the only consumer of a ghost field or snapshot field, leave the field in place — it is safer to have an unused field than to risk breaking another property's wiring. 4. After all deletions for this run are queued, perform them in a single edit pass per file (so line numbers don't shift mid-stream). ### Argument-list handling If the user passed explicit IDs: - Apply the matrix above to each requested ID. - Requested ID is `DRIFT_WARN` → warn, skip, continue with the others. - Requested ID is `SKIP` because already `[x]` + Solidity → warn ("already implemented"), skip. - Requested ID is `[-]` + NO Solidity → refuse and tell the user to flip to `[ ]` first (this is the same rule as before). - Requested ID does not exist in `PROPERTIES.md` → stop and report. --- ## STEP 2: IDENTIFY PROPERTIES TO CONVERT Parse `PROPERTIES.md`. The format is: ``` - [ ] **GL-01** — . (Category: ...; Guarantee: SHOULD-HOLD|EXPLORATORY; Priority: ...; Sources: ...) - [ ] **SP-01** — . (Category: ...; Guarantee: SHOULD-HOLD|EXPLORATORY; After: ; Priority: ...; Sources: ...) ``` The parenthetical fields are metadata; only `After:` affects wiring. **Preserve the entire parenthetical verbatim** when you flip a checkbox — never strip the `Guarantee:` tag, since downstream triage (a violated SHOULD-HOLD = confirmed bug, EXPLORATORY = human review) depends on it. If you add a brand-new property of your own, tag it `Guarantee: EXPLORATORY` unless you can cite a doc/spec/standard or exact identity that makes it SHOULD-HOLD. Use the action map you built in STEP 1.5. The set of IDs that get Solidity work in STEP 4 is the union of: - All IDs classified as `IMPLEMENT` - All IDs classified as `REGENERATE` (these will have their existing Solidity deleted first) `DROP` IDs get deletion-only in STEP 4 (no new Solidity). `SKIP` and `DRIFT_WARN` IDs do nothing. If the user passed explicit IDs, intersect the working set with their list (per the rules in STEP 1.5). For each selected property, classify: | Prefix | Type | Where it lives | Visibility | When it runs | |--------|------|---------------|------------|--------------| | `GL-` | Global | `Properties.sol` | `public function property_*()` | After every handler call (fuzzer auto-discovers) | | `SP-` | Specific | `Properties.sol` | `internal function property_*()` | Called explicitly at the end of a specific handler, after `snapshotAfter()` | --- ## STEP 3: PLAN EACH IMPLEMENTATION For each selected property, work out: 1. **Function name** — `property_`. If `property-plan.md` already lists a name for this Spec ID, use that exact name. 2. **Reads from `stateBefore` / `stateAfter`?** — if yes, list the snapshot fields. If a needed field is missing from `Snapshots.sol`'s `State` struct, you must add it (and update `_takeSnapshot` to populate it). 3. **Reads from `ghosts`?** — if yes, list the ghost fields. If a needed field is missing from `Base.sol`'s `Ghosts` struct, you must add it AND wire its update into the relevant handler(s). 4. **Assertion helper** — pick the right one: `eq`, `gt`, `gte`, `lt`, `lte`, `t` (boolean). Always include a descriptive failure message string. 5. **For SP-* only** — which handler to wire it into. Match against the `After:` field in PROPERTIES.md and the actual function name in `handlers/Handler.sol`. The call site is **after** `snapshotAfter()` and after any ghost updates. 6. **Loop safety** — no unbounded loops in global properties. Loops over `actors` are fine (NUMBER_OF_ACTORS is small). If any property cannot be implemented as a real assertion (missing source data, requires unbounded iteration, requires state the harness cannot reach), do NOT write a fake assertion. Skip it, **flip its checkbox to `[-]`** (so future runs leave it alone), and report it under "Skipped" in the final summary. --- ## STEP 4: APPLY EDITS Process in this order: ### 4a. Deletions first (REGENERATE + DROP) For every ID classified as `REGENERATE` or `DROP` in STEP 1.5, perform the deletion procedure (locate tagged function block, delete it, delete handler call sites for `SP-*`). Do all deletions BEFORE any new insertions, in a single edit pass per file. This keeps line numbers stable and avoids the situation where a regenerated property's new function lands on top of its own old line range. ### 4b. Insertions (IMPLEMENT + REGENERATE) For each property in the implementation set, in turn: 1. If new ghost fields are needed: edit `Base.sol`'s `Ghosts` struct. 2. If new snapshot fields are needed: edit `Snapshots.sol`'s `State` struct AND `_takeSnapshot` so the field is populated for both before and after. 3. Add the property function to `Properties.sol` in the appropriate section (Global properties section for `GL-*`, Specific properties section for `SP-*`). Match the existing comment-banner style. **MANDATORY**: the natspec MUST start with `/// @notice : ` so future runs can find and reconcile this function. 4. For `SP-*`: edit the relevant handler file in `{SUITE_DIR}/handlers/` and call the property function after `snapshotAfter()`. If ghost updates are needed, add them before the property call. ### 4c. Checkbox flips After STEP 5 (build) confirms success: - For each `IMPLEMENT` or `REGENERATE` ID where the new Solidity compiled and (for `SP-*`) the call site is wired: change its checkbox to `[x]`. - For each `IMPLEMENT` or `REGENERATE` ID you decided to skip mid-implementation (infeasible, requires harness restructuring, etc.): change its checkbox to `[-]`. **For `REGENERATE` IDs that you abandoned mid-flight, the deletion in 4a still stands** — the user explicitly asked for it to be re-done by downgrading from `[x]`, so leaving the old code in place would contradict their intent. - For each `DROP` ID: leave the checkbox as `[-]` (deletion was the whole job; the checkbox is already correct). - For each `DRIFT_WARN` ID: do not modify the checkbox at all. Match by exact Spec ID. Do NOT renumber, reorder, or rewrite other lines. Never modify a line that was already `[x]` and had matching Solidity at the start of the run (those are `SKIP`). Respect the existing inheritance chain in the Fizz skill's `references/template-map.md` if present — do not invent new files. --- ## STEP 5: BUILD Run from the project root: ``` forge build ``` If `foundry.toml` defines a `[profile.fuzz]` section, prefer: ``` FOUNDRY_PROFILE=fuzz forge build ``` Fix any compile errors caused by your edits. Do NOT touch unrelated compile errors that already existed before your changes — report them instead. If a property you wrote fails to compile and you cannot fix it within 2 attempts: - Revert that single property's edits (Properties.sol + any handler wiring + any ghost/snapshot fields you added solely for it) - Flip its checkbox to `[-]` so future runs leave it alone - Report it under "Failed to compile" in the summary For a `REGENERATE` ID whose new Solidity fails to compile: do NOT restore the deleted old version. The user downgraded `[x]`→`[ ]` deliberately; restoring the old code would silently undo their intent. Treat this exactly like an `IMPLEMENT` failure — flip to `[-]` and report. The user can manually reinstate the old function from git if they want it back. --- ## STEP 6: REPORT Print a concise summary: ``` fizz-convert results Implemented (NEW, checkbox flipped to [x]): GL-01 property_solvency SP-03 property_depositIncreasesShares (wired into vault_deposit) Regenerated (deleted + re-implemented, checkbox stays [x]): GL-05 property_oTokenB_perTokenSolvency SP-02 property_roundTripNoFreeValue (wired into vault_roundTrip) Dropped (deleted, checkbox stays [-]): GL-12 removed property_oldHelper Skipped (checkbox flipped to [-]): GL-07 reason: requires unbounded loop over historical state Drift warnings (NO change made): GL-09 PROPERTIES.md says [x] but no /// @notice GL-09: function found. Please restore the function or flip the checkbox to [ ] / [-]. Failed to compile (reverted, flipped to [-]): SP-09 reason: Build: PASS / FAIL ``` Do NOT mark a property `[x]` unless its Solidity exists, the build passes, and (for SP-*) it is actually called from a handler. ## skills/fizz-sync ``` ``` ## skills/fizz-sync/SKILL.md --- name: fizz-sync description: Reconcile an existing Fizz harness with a changed source tree. Detects added/removed/changed contract functions, quarantines stale properties, regenerates drifted handler stubs, and refreshes the snapshot. Trigger on "fizz-sync", "resync fuzzing", "sync fuzz harness", "refresh fuzzing properties", "fuzzing drift check". --- # Fizz Sync Skill — fizz-sync Reconcile a project previously processed by the **Fizz** skill with a changed source tree. This is the re-use entry point: after the user modifies Solidity sources, `fizz-sync` detects drift, quarantines stale properties, regenerates drifted handler stubs, and refreshes the snapshot — WITHOUT re-running the full 11-step pipeline. ## When to use - The source contracts under `src/` changed since `fizz` last ran. - A property in `PROPERTIES.md` fails to compile or references a function that no longer exists. - The user added new external functions they want fuzzed. - The user wants a "is anything stale?" health check before re-running a campaign. ## Parameters - `SUITE_DIR`: Solidity suite directory relative to project root (default: `test/fizz`). Use the same value that was passed to the `fizz` skill when the harness was generated. - `META_DIR`: Metadata directory relative to project root (default: `fizz_data`). Use the same value that was passed to the `fizz` skill. ## Arguments - `--init` — one-time bootstrap: create `{META_DIR}/last-run.json` from the current state. Use this the first time fizz-sync runs on a project (or when adopting fizz-sync on a project that was fuzzed before the snapshot format existed). - `--only ` — scope the sync to a single contract name. - `--apply` — actually perform the automatic fixes. Without `--apply`, fizz-sync runs in dry-run mode and only reports drift. - `--no-property-quarantine` — skip the property quarantine phase (useful if the user wants to handle stale properties manually). The default (no flags) runs a dry-run drift report. ## Preconditions - The project must have been processed by the `fizz` skill at least once. Look for: - `{PROJECT_ROOT}/{META_DIR}/contracts.json` - `{PROJECT_ROOT}/{META_DIR}/entry-point-selection.json` - `{PROJECT_ROOT}/{SUITE_DIR}/` (suite directory) - If any of the above are missing, stop and tell the user to run `fizz` first. --- ## STEP 0: REBUILD CURRENT ABIS The snapshot diff compares against `contracts.json` and `entry-point-selection.json`. Those files reflect the state from the last `fizz` run, NOT the current source tree. You must refresh them first. Run sequentially: 1. `cd {PROJECT_ROOT} && forge build --skip 'test/**/*.sol'` The `--skip` flag is critical: if the user's source change broke downstream call sites in `test/`, a plain `forge build` will fail on the harness code — which is exactly the drift fizz-sync is supposed to fix. Skipping `test/` means we only validate that the SOURCE compiles cleanly, which is all we need to refresh the ABI. If the build still fails with `--skip 'test/**/*.sol'`, the source itself has a compile error. Stop and report it. Fuzz-sync cannot proceed without valid source artifacts. 2. `node {SKILL_PATH}/../../scripts/extract_abis.js {PROJECT_ROOT} --meta-dir {META_DIR}` This refreshes `contracts.json` from the latest artifacts. It overwrites the old file in place. 3. **Do NOT re-run `select_functions.js` automatically.** The existing `entry-point-selection.json` encodes the user's prior tier assignments and selection choices. fizz-sync treats it as the source of truth for what's "in scope" and diffs only within that scope. If new contracts have been added that the user probably wants to fuzz, the drift report will surface them and the user can manually add them to `entry-point-selection.json` and re-run fizz-sync. --- ## STEP 1: HANDLE --init If the user passed `--init`: 1. Run: ``` node {SKILL_PATH}/../../scripts/fizz_sync.js {PROJECT_ROOT} --init ``` 2. If the script reports the snapshot already exists, ask the user whether they want to overwrite with `--force` (they usually do NOT — it would erase drift history). 3. Report the number of contracts and properties captured, then stop. No further steps. --- ## STEP 2: RUN THE DRIFT REPORT Run: ``` node {SKILL_PATH}/../../scripts/fizz_sync.js {PROJECT_ROOT} ``` The script: - Reads `{META_DIR}/last-run.json` (created by `--init` or by Step 11 of the main `fizz` skill). - Builds a fresh snapshot from the current `entry-point-selection.json`, source file hashes, and `PROPERTIES.md`. - Diffs them and writes `{META_DIR}/sync-report.json`. - Prints a human-readable summary. - Exits 0 if no drift, 1 if drift was detected. If exit 0 and no drift, stop and tell the user the harness is already in sync. Read the JSON report: ``` {PROJECT_ROOT}/{META_DIR}/sync-report.json ``` The JSON schema is: ```json { "generatedAt": "...", "hasDrift": true, "contracts": { "added": [{"name":"...", "sourcePath":"...", "functions":[{"signature":"...", "tier":"primary"}]}], "removed": [{"name":"...", "handlerFile":"...Handler.sol"}], "changed": [{"name":"...", "functionsAdded":[...], "functionsRemoved":[...], "functionsChanged":[{"oldSignature":"...","newSignature":"...","handlerMethodName":"..."}], "tierChanged":[...]}], "sourcesChanged": [{"name":"...", "sourcePath":"..."}] }, "handlers": { "orphan": [{"file":"...", "contract":"..."}], "modified": [{"file":"..."}], "missing": [{"file":"..."}] }, "properties": { "referencingRemoved": [{"file":"...", "reference":"lender_oldMethod", "reason":"..."}], "fromSnapshot": [{"id":"GL-01", "checkbox":"x", "functionName":"property_..."}] } } ``` Use this object as the canonical work list for the rest of the skill. --- ## STEP 3: DRY-RUN SUMMARY (ALWAYS) Regardless of whether `--apply` was passed, print a concise summary to the user that mirrors the report: ``` fizz-sync drift report ────────────────────── Added contracts: N Removed contracts: N Drifted contracts: N (M added / M removed / M changed functions) Orphan handlers: N Stale properties: N Modified handlers: N (user-edited since last snapshot) ``` If fizz-sync was invoked WITHOUT `--apply`, stop here and tell the user: > Dry-run complete. Re-run with `--apply` to regenerate handlers and quarantine stale properties, or handle items manually using the report at `{META_DIR}/sync-report.json`. --- ## STEP 4: APPLY — HANDLER REGENERATION Only run this step if `--apply` was passed. ### 4a. Back up user-modified handlers For every entry in `report.handlers.modified`, the user has hand-edited that handler since the last snapshot. Regenerating it would destroy their clamping logic. The script already backs up `.pre-sync.bak`, but the user should be warned. Print a warning listing every modified handler and ask the user whether to proceed. If the user says no, skip to Step 5. ### 4b. Regenerate drifted handlers Run: ``` node {SKILL_PATH}/../../scripts/fizz_sync.js {PROJECT_ROOT} --apply-handlers ``` The script: - Regenerates handler files for contracts listed in `report.contracts.added` and `report.contracts.changed`. - Creates `Handler.sol.pre-sync.bak` backups next to each regenerated file. - Uses the existing `generate_handlers.js` under the hood with a scoped selection file, so tier assignments are respected. After the script runs, for each regenerated handler: 1. Read the `.pre-sync.bak` version and the new version. 2. Port any still-valid clamping bodies and ghost wiring from the backup into the new handler. Functions whose signature did not change can usually be copied verbatim. Functions whose signature changed must be manually rewritten against the new signature. 3. Keep `/// @notice SP-NN:` doctags intact — they are how `fizz-convert` and future `fizz-sync` runs identify which Solidity corresponds to which Spec ID. 4. For functions that were REMOVED from the source contract, delete the corresponding handler method from the regenerated file AND delete any call sites elsewhere. ### 4c. Handle orphan handlers For every entry in `report.handlers.orphan`, the contract no longer exists in the selection. Offer the user two choices: 1. **Delete** — remove the handler file entirely and remove its inheritance line from `handlers/Handlers.sol`. Also remove any `contract_handler` field wiring. 2. **Quarantine** — leave the file in place but rename it `Handler.sol.orphan` so `generate_suite.js` does not re-pick it up, and comment out its inheritance line in `Handlers.sol` with a `// FUZZ-SYNC: orphan — contract removed` marker. Default to quarantine. Only delete if the user explicitly confirms. ### 4d. Handle missing handlers For every entry in `report.handlers.missing`, the file disappeared since the last snapshot. If the contract still exists in `contracts.changed` / unchanged, treat this as a regeneration case — re-run the generate step without `--only` scoping (or manually invoke `generate_handlers.js`) to recreate it. --- ## STEP 5: APPLY — PROPERTY QUARANTINE Skip if `--no-property-quarantine` was passed. This is the most delicate phase. A property can be stale for several reasons: - Its tagged handler function was renamed or removed (detected in `report.properties.referencingRemoved`). - A ghost variable it depends on was deleted. - The source function it asserts against changed semantics without changing signature (`report.contracts.sourcesChanged`). - It no longer compiles at all. ### 5a. Compile-first triage Run the scoped build that skips non-harness test files: ``` cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge build $(find test -maxdepth 1 -name '*.sol' -exec echo --skip {} \;) ``` (fall back to plain `forge build ...` without `FOUNDRY_PROFILE=fuzz` if no `fuzz` profile is configured). The `find ... --skip` wrapper is essential: without it, compile errors in the user's own top-level test files (e.g. `test/MyContract.t.sol`, which is outside the fuzzing harness and NOT managed by this skill) would block the build and prevent fizz-sync from running its quarantine logic. Those top-level test files are the user's responsibility to fix; this skill only owns `{SUITE_DIR}/`. If the build FAILS, parse every error. For each error whose location is inside `{SUITE_DIR}/`: 1. Identify the enclosing function (walk up from the error line until you hit a `function (` header). 2. Check whether that function has a `/// @notice (GL-NN|SP-NN):` doctag — if yes, the Spec ID is the source of truth for reconciliation. 3. Quarantine the function: - Replace the entire function body with a single `revert("FUZZ-SYNC: quarantined");` statement. - Move the old body into a multi-line comment (`/* ... */`) directly above the function so the user can see the original logic and restore it manually when ready. - Add a single-line annotation above the comment: ```solidity // FUZZ-SYNC: quarantined — . Restore by deleting the revert body and uncommenting the block above. ``` - `if (false) { ... }` is NOT a valid quarantine strategy — Solidity type-checks dead branches and the original compile error will persist. 4. If the function had a Spec ID, flip its checkbox in `PROPERTIES.md` from `[x]` to `[~]` and append ` (stale — source changed, re-opened)` to the description. 5. Rebuild. Repeat up to 3 cycles. If errors persist after 3 cycles, stop and report the remaining errors to the user — they need manual help. **Important**: do NOT quarantine handler methods this way. If a handler method fails to compile, the fix belongs in Step 4b (handler regeneration) or 4c (orphan handling), not here. ### 5b. Semantic-drift sweep After the compile triage passes, scan `report.properties.referencingRemoved`. For each entry: 1. Find the enclosing tagged function in the named file. 2. Read the whole function body. 3. If the dead reference is the ONLY purpose of the property (e.g., the property exists solely to check a post-condition of a now-removed handler call), quarantine it per the same procedure as 5a. 4. If the dead reference is incidental (e.g., the property also checks other state), leave it alone but add a `// FUZZ-SYNC: references removed method ` marker at the reference site. Rely on the compile triage to catch it on the next cycle if it actually breaks. ### 5c. Source-hash-only drift For every entry in `report.contracts.sourcesChanged` that did NOT appear in `contracts.changed` (i.e., the source file changed but the ABI did not): - This is a semantic refactor. Properties still compile but might assert the wrong thing. - Do NOT auto-quarantine. Instead, list the affected contracts under a "Review recommended" section in the final report so the user can eyeball the properties tied to those contracts. --- ## STEP 6: REBUILD AND VALIDATE Run: ``` cd {PROJECT_ROOT} && FOUNDRY_PROFILE=fuzz forge build $(find test -maxdepth 1 -name '*.sol' -exec echo --skip {} \;) ``` (fall back to `forge build ...` without the profile variable if no `fuzz` profile is configured). If it fails, go back to Step 5a for one more cycle. If it has already been through 3 cycles, stop and report. If it succeeds, proceed to snapshot refresh. --- ## STEP 7: REFRESH SNAPSHOT Only after Step 6 succeeds and the user is happy with the result: ``` node {SKILL_PATH}/../../scripts/fizz_sync.js {PROJECT_ROOT} --refresh-snapshot ``` This overwrites `{META_DIR}/last-run.json` with the post-sync state. Future `fizz-sync` runs will diff against this new baseline. --- ## STEP 8: REPORT Print a concise summary: ``` fizz-sync results ───────────────── Handlers regenerated: VaultHandler.sol (3 added, 1 removed, 1 signature changed) LendingPoolHandler.sol (2 added) Handlers ported from backup: VaultHandler.sol (5/6 clamping bodies preserved) Orphan handlers: OldStakingHandler.sol quarantined (renamed .orphan) Properties quarantined: SP-04 referenced removed function lender_oldDeposit SP-07 build error on line 128 Properties untouched (review recommended): GL-02 source hash changed but ABI stable — verify semantic intent GL-09 idem Build: PASS Snapshot refreshed: {META_DIR}/last-run.json ``` ### Next actions Tell the user: - For newly added functions without handler bodies: re-run `fizz` Step 7 for just those contracts, or use the `fizz-convert` skill if the user also wants to regenerate properties for them. - For quarantined properties: either rewrite them manually (flip `[~]` back to `[ ]` in `PROPERTIES.md` and run `/fizz-convert`), or leave them quarantined. - For source-changed contracts without ABI drift: read the diff manually to confirm existing properties still encode the intended semantics. --- ## RULES - Never run a full Fizz pipeline as part of a sync. Sync is surgical by design. - Never regenerate ALL handlers — only the drifted subset. - Never auto-delete orphan handlers without user confirmation. - Never flip a `[ ]` or `[-]` checkbox to `[x]` in this skill. Only `[x] → [~]` for quarantining is allowed. - Always back up files before destructive edits. The `.pre-sync.bak` files are the user's safety net. - Always refresh the snapshot at the end of a successful `--apply` run, and NEVER refresh it mid-run before Step 6 passes — that would bake in the broken state. ## templates ``` ``` ## templates/Actor.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; contract ForceSendETH { constructor(address dst) payable { // Use assembly to stay compatible across Solidity versions where // selfdestruct is deprecated or removed assembly { selfdestruct(dst) } } } /// @notice Represents an actor interacting with the system contract Actor { constructor() payable { } receive() external payable {} function forceSendETH(address recipient, uint256 amount) public { new ForceSendETH{value: amount}(recipient); } // ――――――――――――――――――― Flash loan borrower ―――――――――――――――――――― function onFlashLoan(address initiator, address token, uint256 amount, uint256 fee, bytes calldata data) external returns (bytes32) { // Implement here flash loan logic, if needed return keccak256("ERC3156FlashBorrower.onFlashLoan"); } // ――――――――――――――――――――― ERC-721 receiver ――――――――――――――――――――― function onERC721Received(address operator, address from, uint256 tokenId, bytes calldata data) external returns (bytes4) { return this.onERC721Received.selector; } // ―――――――――――――――――――― ERC-1155 receiver ――――――――――――――――――――― function onERC1155Received(address operator, address from, uint256 id, uint256 value, bytes calldata data) external returns (bytes4) { return this.onERC1155Received.selector; } function onERC1155BatchReceived( address operator, address from, uint256[] calldata ids, uint256[] calldata values, bytes calldata data ) external returns (bytes4) { return this.onERC1155BatchReceived.selector; } } ``` ## templates/Base.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import {Actor} from "./Actor.sol"; import {Clamp} from "./utils/Clamp.sol"; import {DecimalPrinter} from "./utils/DecimalPrinter.sol"; import {Deployer} from "./utils/Deployer.sol"; import {vm} from "./utils/Hevm.sol"; import {Logger} from "./utils/Logger.sol"; import {Math} from "./utils/Math.sol"; import {StringUtils} from "./utils/StringUtils.sol"; import {EnumerableSet} from "./utils/EnumerableSet.sol"; /// @notice Base contract with state variables and setup functions abstract contract Base is StringUtils, Clamp, Deployer, Math { using DecimalPrinter for uint256; string[] internal ACTOR_LABELS = ["Alice", "Bob", "Charlie"]; uint256 internal constant BLOCK_INTERVAL = 12 seconds; uint256 internal constant INITIAL_ETH_BALANCE = 1_000 ether; uint256 internal constant INITIAL_TOKEN_BALANCE = 10_000; // ―――――――――――――――――――――――――― Ghosts ―――――――――――――――――――――――――― struct Ghosts { uint256 _placeholder; } Ghosts internal ghosts; // ―――――――――――――――――――――――――― Actors ―――――――――――――――――――――――――― address[] internal actors; address internal actor; address internal admin; modifier asActor() virtual { vm.startPrank(actor); _; vm.stopPrank(); } modifier asAdmin() virtual { vm.startPrank(admin); _; vm.stopPrank(); } // ―――――――――――――――――――――――― Contracts ――――――――――――――――――――――――― // FIXME: Contract instances go here, e.g.: // Foo public foo; // ―――――――――――――――――――――――――― Setup ――――――――――――――――――――――――――― function setup() internal { // FIXME: Add initial setup (e.g. deploy contracts, set initial state, etc.) setupActors(); } function setupActors() internal { admin = address(this); vm.label(admin, "Admin"); for (uint256 i; i < ACTOR_LABELS.length; i++) { address _actor = address(new Actor{value: INITIAL_ETH_BALANCE}()); actors.push(_actor); if (ACTOR_LABELS.length > i) { vm.label(_actor, ACTOR_LABELS[i]); } // FIXME: Add any required actor setup (e.g. minting tokens, setting allowances, etc.) // If needed, Actor's constructor can also be used for this purpose } actor = actors[0]; } // ――――――――――――――――――――――――― Helpers ―――――――――――――――――――――――――― // Maps an arbitrary address to an actor address function toActor(address addy) internal view returns (address) { return actors[uint256(uint160(addy)) % actors.length]; } // Maps an arbitrary address to an actor address that is different from the current actor function toActorNotCurrent(address addy) internal view returns (address) { address _actor = actors[uint256(uint160(addy)) % actors.length]; if (_actor == actor) { _actor = actors[(uint256(uint160(addy)) + 1) % actors.length]; } return _actor; } // Sums the native token balances of all actors function sumActorsBalances() internal view returns (uint256 sumOfBalances) { for (uint256 i; i < actors.length; i++) { sumOfBalances += actors[i].balance; } } // Sums the ERC-20 token balances of all actors for a given token function sumActorsERC20Balances(address _token) internal view returns (uint256 sumOfBalances) { for (uint256 i; i < actors.length; i++) { bytes memory data = abi.encodeWithSignature("balanceOf(address)", actors[i]); (bool success, bytes memory result) = _token.staticcall(data); require(success, "sumActorsERC20Balances: failed to get balance"); sumOfBalances += abi.decode(result, (uint256)); } } function skipBlocks(uint256 blocks) internal { vm.roll(block.number + blocks); vm.warp(block.timestamp + blocks * BLOCK_INTERVAL); } function skipTime(uint256 time) internal { uint256 blocks = (time + BLOCK_INTERVAL - 1) / BLOCK_INTERVAL; vm.roll(block.number + blocks); vm.warp(block.timestamp + time); } } ``` ## templates/FoundryTester.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import {Test} from "forge-std/Test.sol"; import {console} from "forge-std/console.sol"; import {Handlers} from "./handlers/Handlers.sol"; /// @notice Contract to be used for quick testing with Foundry contract FoundryTester is Test, Handlers { modifier asActor() override { vm.startPrank(actor); _; vm.stopPrank(); } function setUp() public { setup(); } // forge test --match-test test_sequence -vvv function test_sequence() public { // Add here call sequence to Handler's functions to reproduce failing property } // ── Violation Repros (auto-generated by Step 11) ────────────────── // Each test_repro_* function below replays a shrunk fuzzer call // sequence that violated a property. Run all with: // forge test --match-contract FoundryTester -vvv } ``` ## templates/FuzzTester.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import {Handlers} from "./handlers/Handlers.sol"; /// @notice Entry point for fuzzing tests contract FuzzTester is Handlers { constructor() payable { setup(); } } ``` ## templates/Properties.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import {Snapshots} from "./Snapshots.sol"; import {PropertiesAsserts} from "./utils/PropertiesAsserts.sol"; /// @notice Contains the functions that check the properties (invariants) abstract contract Properties is PropertiesAsserts, Snapshots { // ―――――――――――――――――――― Global properties ――――――――――――――――――――― // These properties must always hold after any function call. // They MUST BE PUBLIC so that fuzzers can find and call them. // ――――――――――――――――――― Specific properties ―――――――――――――――――――― // These properties must hold after specific function calls. // They MUST BE INTERNAL and called at the end of the relevant handlers. } ``` ## templates/README.md # Fizz Suite ## What Is Here - `Base.sol`: shared setup, deployed contract references, actors, helpers, and ghost state - `Snapshots.sol`: before/after state capture used by properties - `Properties.sol`: global and function-specific invariants - `handlers/`: protocol actions exposed to the fuzzers - `harness/`: (optional) harness contracts that inherit from target contracts to expose private/internal state needed by properties - `utils/`: shared helper libraries, assertions, clamping logic, math helpers, deploy helpers, logging, and mocks - `FuzzTester.sol`: main Echidna/Medusa fuzzing entry point - `FoundryTester.sol`: Foundry harness for quick debugging and local repros ## Inheritance Chain ``` Base (is StringUtils, Clamp, Deployer, Math) └─► Snapshots (is Base) └─► Properties (is PropertiesAsserts, Snapshots) └─► Handler (is Properties) — one per target contract └─► Handlers (is ) — aggregator + actor switching ├─► FuzzTester (is Handlers) — Echidna/Medusa entry point └─► FoundryTester (is Test, Handlers) — Foundry quick debug/PoC entry point ``` ## Related Paths Outside This Directory - `../../fizz_data/`: extracted ABI inventory, entry-point selection, protocol-understanding notes, corpora, logs, and coverage outputs - `../../echidna.yaml`: Echidna config - `../../medusa.json`: Medusa config ## How To Run From the project root: ```bash forge build forge test --match-contract FoundryTester echidna . --contract FuzzTester --config echidna.yaml medusa fuzz --config medusa.json ``` ## How To Read The Suite Recommended order: 1. `README.md` 2. `Base.sol` 3. `handlers/Handlers.sol` 4. individual handler files under `handlers/` 5. `Snapshots.sol` 6. `Properties.sol` 7. `harness/` (if present) — to understand what private/internal state is exposed and why 8. `utils/` when you need to understand helper behavior or mocks 9. `FuzzTester.sol` 10. `FoundryTester.sol` ## templates/Snapshots.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import {Base} from "./Base.sol"; /// @notice Used to take snapshots of the state before and after a function call abstract contract Snapshots is Base { struct State { uint256 _placeholder; } State internal stateBefore; State internal stateAfter; function _takeSnapshot(State storage state) private { state._placeholder = actor.balance; } function snapshotBefore() internal { _takeSnapshot(stateBefore); } function snapshotAfter() internal { _takeSnapshot(stateAfter); } } ``` ## templates/echidna.yaml ```yaml testMode: "assertion" prefix: "property_" seqLen: 100 testLimit: 50000 balanceContract: 0xffffffffffffffffffffffffffffffffffffffffffffffff coverage: true corpusDir: "fizz_data/corpus_echidna" cryticArgs: ["--foundry-compile-all"] contractAddr: "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496" deployer: "0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38" # output format (comment out for TUI) format: "text" # Hide solc stderr output and additional information during the testing. quiet: false stopOnFail: false disableSlither: false # https://secure-contracts.com/program-analysis/echidna/configuration.html ``` ## templates/handlers ``` ``` ## templates/handlers/Handlers.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; import "../Base.sol"; /// @notice Inherits from all the handlers to expose all entry points in a single contract. /// Manages environment changes (e.g. current actor, current token, mocks setup, etc.). abstract contract Handlers { function setCurrentActor(uint256 entropy) public { actor = actors[entropy % actors.length]; } } ``` ## templates/medusa.json ```json { "fuzzing": { "workers": 10, "workerResetLimit": 50, "timeout": 0, "testLimit": 500000, "callSequenceLength": 100, "corpusDirectory": "fizz_data/corpus_medusa", "coverageEnabled": true, "deploymentOrder": [ "FuzzTester" ], "targetContracts": [ "FuzzTester" ], "targetContractsBalances": [ "0xffffffffffffffffffffffffffffffffffffffffffffffff" ], "constructorArgs": {}, "deployerAddress": "0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38", "senderAddresses": [ "0x10000", "0x20000", "0x30000" ], "blockNumberDelayMax": 60480, "blockTimestampDelayMax": 604800, "blockGasLimit": 125000000, "transactionGasLimit": 12500000, "testing": { "stopOnFailedTest": false, "stopOnFailedContractMatching": false, "stopOnNoTests": true, "testAllContracts": false, "traceAll": false, "assertionTesting": { "enabled": true, "testViewMethods": true, "panicCodeConfig": { "failOnCompilerInsertedPanic": false, "failOnAssertion": true, "failOnArithmeticUnderflow": false, "failOnDivideByZero": false, "failOnEnumTypeConversionOutOfBounds": false, "failOnIncorrectStorageAccess": false, "failOnPopEmptyArray": false, "failOnOutOfBoundsArrayAccess": false, "failOnAllocateTooMuchMemory": false, "failOnCallUninitializedVariable": false } }, "propertyTesting": { "enabled": true, "testPrefixes": [ "property_" ] }, "optimizationTesting": { "enabled": false, "testPrefixes": [ "optimize_" ] } }, "chainConfig": { "codeSizeCheckDisabled": true, "cheatCodes": { "cheatCodesEnabled": true, "enableFFI": false } } }, "compilation": { "platform": "crytic-compile", "platformConfig": { "target": ".", "solcVersion": "", "exportDirectory": "fizz_data/crytic-export", "args": [ "--foundry-compile-all" ] } }, "slither": { "enabled": true, "cachePath": "fizz_data/slither_results.json" }, "logging": { "level": "info", "logDirectory": "fizz_data/logs_medusa", "noColor": false } } ``` ## templates/utils ``` ``` ## templates/utils/Clamp.sol ```solidity // SPDX-License-Identifier: Unlicense pragma solidity >=0.6.2 <0.9.0; import {Logger} from "./Logger.sol"; import {StringUtils} from "./StringUtils.sol"; /// @author Modified from Crytic (https://github.com/crytic/properties/blob/main/contracts/util/PropertiesAsserts.sol) contract Clamp is StringUtils { /// @notice Clamps value to be between low and high, both inclusive function clampBetween( uint256 value, uint256 low, uint256 high ) internal returns (uint256) { if (value < low || value > high) { uint256 range = high - low; uint256 ans = low + (value % (range + 1)); // When range == type(uint256).max (low=0, high=max), range+1 overflows // to 0 causing division by zero. In that case any value is already in // range, so this branch is only reachable when range < type(uint256).max. string memory valueStr = toString(value); string memory ansStr = toString(ans); bytes memory message = abi.encodePacked( "Clamping value ", valueStr, " to ", ansStr ); Logger.logString(string(message)); return ans; } return value; } /// @notice int256 version of clampBetween function clampBetween( int256 value, int256 low, int256 high ) internal returns (int256) { if (value < low || value > high) { int range = high - low + 1; int clamped = (value - low) % (range); if (clamped < 0) clamped += range; int ans = low + clamped; string memory valueStr = toString(value); string memory ansStr = toString(ans); bytes memory message = abi.encodePacked( "Clamping value ", valueStr, " to ", ansStr ); Logger.logString(string(message)); return ans; } return value; } /// @notice clamps a to be less than b function clampLt(uint256 a, uint256 b) internal returns (uint256) { if (!(a < b)) { if(b == 0) { Logger.logString("clampLt cannot clamp value a to be less than zero. Check your inputs/assumptions."); assert(false); } uint256 value = a % b; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } /// @notice int256 version of clampLt function clampLt(int256 a, int256 b) internal returns (int256) { if (!(a < b)) { if (b == type(int256).min) { Logger.logString("clampLt cannot clamp value a to be less than int256.min. Check your inputs/assumptions."); assert(false); } int256 value = b - 1; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } /// @notice clamps a to be less than or equal to b function clampLte(uint256 a, uint256 b) internal returns (uint256) { if (!(a <= b)) { // When b == type(uint256).max, a <= b is always true so this // branch is unreachable. Safe to use b + 1 without overflow. uint256 value = a % (b + 1); string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } /// @notice int256 version of clampLte function clampLte(int256 a, int256 b) internal returns (int256) { if (!(a <= b)) { int256 value = b; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } /// @notice clamps a to be greater than b function clampGt(uint256 a, uint256 b) internal returns (uint256) { if (!(a > b)) { if (b == type(uint256).max) { Logger.logString("clampGt cannot clamp value a to be larger than uint256.max. Check your inputs/assumptions."); assert(false); } uint256 value = b + 1; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } else { return a; } } /// @notice int256 version of clampGt function clampGt(int256 a, int256 b) internal returns (int256) { if (!(a > b)) { if (b == type(int256).max) { Logger.logString("clampGt cannot clamp value a to be larger than int256.max. Check your inputs/assumptions."); assert(false); } int256 value = b + 1; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } else { return a; } } /// @notice clamps a to be greater than or equal to b function clampGte(uint256 a, uint256 b) internal returns (uint256) { if (!(a >= b)) { uint256 value = b; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } /// @notice int256 version of clampGte function clampGte(int256 a, int256 b) internal returns (int256) { if (!(a >= b)) { int256 value = b; string memory aStr = toString(a); string memory valueStr = toString(value); bytes memory message = abi.encodePacked( "Clamping value ", aStr, " to ", valueStr ); Logger.logString(string(message)); return value; } return a; } } ``` ## templates/utils/DecimalPrinter.sol ```solidity // SPDX-License-Identifier: UNLICENSED pragma solidity >=0.6.2 <0.9.0; library DecimalPrinter { function toDec(uint256 _value) public pure returns (string memory) { return toDec(_value, 18); } function toDec(int256 _value) public pure returns (string memory) { return toDec(_value, 18); } function toDec(uint256 _value, uint256 decimals) public pure returns (string memory) { uint256 base = 10**decimals; uint256 integerPart = _value / base; uint256 fractionalPart = _value % base; string memory integerPartStr = uintToStr(integerPart); string memory fractionalPartStr = uintToStr(fractionalPart); // Pad fractional part with leading zeros if necessary uint256 numZeros = decimals - bytes(fractionalPartStr).length; for (uint256 i = 0; i < numZeros; i++) { fractionalPartStr = string(abi.encodePacked("0", fractionalPartStr)); } string memory result = string(abi.encodePacked(integerPartStr, ".", fractionalPartStr)); return result; } function toDec(int256 _value, uint256 decimals) public pure returns (string memory) { if (_value < 0) { return string(abi.encodePacked("-", toDec(uint256(-_value), decimals))); } else { return toDec(uint256(_value), decimals); } } function uintToStr(uint256 _value) private pure returns (string memory) { if (_value == 0) { return "0"; } uint256 temp = _value; uint256 digits; while (temp != 0) { digits++; temp /= 10; } bytes memory buffer = new bytes(digits); while (_value != 0) { digits--; buffer[digits] = bytes1(uint8(48 + _value % 10)); _value /= 10; } return string(buffer); } } ``` ## templates/utils/Deployer.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; // Source: https://solidity-by-example.org/app/deploy-any-contract/ contract Deployer { function deploy(bytes memory _code) internal returns (address addr) { return deploy(_code, 0); } function deploy(bytes memory _code, uint256 _value) internal returns (address addr) { assembly { addr := create(_value, add(_code, 0x20), mload(_code)) } require(addr != address(0), "Deployer.sol: deploy failed"); } } ``` ## templates/utils/EnumerableSet.sol ```solidity // SPDX-License-Identifier: MIT // OpenZeppelin Contracts (last updated v5.0.0) (utils/structs/EnumerableSet.sol) pragma solidity >=0.6.2 <0.9.0; /** * @dev Library for managing * https://en.wikipedia.org/wiki/Set_(abstract_data_type)[sets] of primitive * types. * * Sets have the following properties: * * - Elements are added, removed, and checked for existence in constant time * (O(1)). * - Elements are enumerated in O(n). No guarantees are made on the ordering. * * ```solidity * contract Example { * // Add the library methods * using EnumerableSet for EnumerableSet.AddressSet; * * // Declare a set state variable * EnumerableSet.AddressSet private mySet; * } * ``` * * As of v3.3.0, sets of type `bytes32` (`Bytes32Set`), `address` (`AddressSet`) * and `uint256` (`UintSet`) are supported. * * [WARNING] * ==== * Trying to delete such a structure from storage will likely result in data corruption, rendering the structure * unusable. * See https://github.com/ethereum/solidity/pull/11843[ethereum/solidity#11843] for more info. * * In order to clean an EnumerableSet, you can either remove all elements one by one or create a fresh instance using an * array of EnumerableSet. * ==== */ library EnumerableSet { struct Set { bytes32[] _values; mapping(bytes32 value => uint256) _positions; } function _add(Set storage set, bytes32 value) private returns (bool) { if (!_contains(set, value)) { set._values.push(value); set._positions[value] = set._values.length; return true; } else { return false; } } function _remove(Set storage set, bytes32 value) private returns (bool) { uint256 position = set._positions[value]; if (position != 0) { uint256 valueIndex = position - 1; uint256 lastIndex = set._values.length - 1; if (valueIndex != lastIndex) { bytes32 lastValue = set._values[lastIndex]; set._values[valueIndex] = lastValue; set._positions[lastValue] = position; } set._values.pop(); delete set._positions[value]; return true; } else { return false; } } function _contains(Set storage set, bytes32 value) private view returns (bool) { return set._positions[value] != 0; } function _length(Set storage set) private view returns (uint256) { return set._values.length; } function _at(Set storage set, uint256 index) private view returns (bytes32) { return set._values[index]; } function _values(Set storage set) private view returns (bytes32[] memory) { return set._values; } // Bytes32Set struct Bytes32Set { Set _inner; } function add(Bytes32Set storage set, bytes32 value) internal returns (bool) { return _add(set._inner, value); } function remove(Bytes32Set storage set, bytes32 value) internal returns (bool) { return _remove(set._inner, value); } function contains(Bytes32Set storage set, bytes32 value) internal view returns (bool) { return _contains(set._inner, value); } function length(Bytes32Set storage set) internal view returns (uint256) { return _length(set._inner); } function at(Bytes32Set storage set, uint256 index) internal view returns (bytes32) { return _at(set._inner, index); } function values(Bytes32Set storage set) internal view returns (bytes32[] memory) { bytes32[] memory store = _values(set._inner); bytes32[] memory result; /// @solidity memory-safe-assembly assembly { result := store } return result; } // AddressSet struct AddressSet { Set _inner; } function add(AddressSet storage set, address value) internal returns (bool) { return _add(set._inner, bytes32(uint256(uint160(value)))); } function remove(AddressSet storage set, address value) internal returns (bool) { return _remove(set._inner, bytes32(uint256(uint160(value)))); } function contains(AddressSet storage set, address value) internal view returns (bool) { return _contains(set._inner, bytes32(uint256(uint160(value)))); } function length(AddressSet storage set) internal view returns (uint256) { return _length(set._inner); } function at(AddressSet storage set, uint256 index) internal view returns (address) { return address(uint160(uint256(_at(set._inner, index)))); } function values(AddressSet storage set) internal view returns (address[] memory) { bytes32[] memory store = _values(set._inner); address[] memory result; /// @solidity memory-safe-assembly assembly { result := store } return result; } // UintSet struct UintSet { Set _inner; } function add(UintSet storage set, uint256 value) internal returns (bool) { return _add(set._inner, bytes32(value)); } function remove(UintSet storage set, uint256 value) internal returns (bool) { return _remove(set._inner, bytes32(value)); } function contains(UintSet storage set, uint256 value) internal view returns (bool) { return _contains(set._inner, bytes32(value)); } function length(UintSet storage set) internal view returns (uint256) { return _length(set._inner); } function at(UintSet storage set, uint256 index) internal view returns (uint256) { return uint256(_at(set._inner, index)); } function values(UintSet storage set) internal view returns (uint256[] memory) { bytes32[] memory store = _values(set._inner); uint256[] memory result; /// @solidity memory-safe-assembly assembly { result := store } return result; } } ``` ## templates/utils/Hevm.sol ```solidity // SPDX-License-Identifier: Unlicense pragma solidity >=0.6.2 <0.9.0; // source: https://github.com/crytic/properties/blob/main/contracts/util/IHevm.sol interface IHevm { // Set block.timestamp to newTimestamp function warp(uint256 newTimestamp) external; // Set block.number to newNumber function roll(uint256 newNumber) external; // Add the condition b to the assumption base for the current branch // This function is almost identical to require function assume(bool b) external; // Sets the eth balance of usr to amt function deal(address usr, uint256 amt) external; // Loads a storage slot from an address function load(address where, bytes32 slot) external returns (bytes32); // Stores a value to an address' storage slot function store(address where, bytes32 slot, bytes32 value) external; // Signs data (privateKey, digest) => (v, r, s) function sign( uint256 privateKey, bytes32 digest ) external returns (uint8 v, bytes32 r, bytes32 s); // Gets address for a given private key function addr(uint256 privateKey) external returns (address addr); // Performs a foreign function call via terminal function ffi( string[] calldata inputs ) external returns (bytes memory result); // Performs the next smart contract call with specified msg.sender function prank(address newSender) external; // Creates a new fork with the given endpoint and the latest block and returns the identifier of the fork function createFork(string calldata urlOrAlias) external returns (uint256); // Takes a fork identifier created by createFork and sets the corresponding forked state as active function selectFork(uint256 forkId) external; // Returns the identifier of the current fork function activeFork() external returns (uint256); // Labels the address in traces function label(address addr, string calldata label) external; // Sets msg.sender to the specified sender until stopPrank() is called function startPrank(address sender) external; // Resets msg.sender to the default sender function stopPrank() external; } IHevm constant vm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D); ``` ## templates/utils/Logger.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; library Logger { event Log(); function log() internal { emit Log(); } event LogInt(int p0); function logInt(int p0) internal { emit LogInt(p0); } event LogUint(uint p0); function logUint(uint p0) internal { emit LogUint(p0); } event LogString(string p0); function logString(string memory p0) internal { emit LogString(p0); } event LogBool(bool p0); function logBool(bool p0) internal { emit LogBool(p0); } event LogAddress(address p0); function logAddress(address p0) internal { emit LogAddress(p0); } event LogBytes(bytes p0); function logBytes(bytes memory p0) internal { emit LogBytes(p0); } event LogBytes1(bytes1 p0); function logBytes1(bytes1 p0) internal { emit LogBytes1(p0); } event LogBytes2(bytes2 p0); function logBytes2(bytes2 p0) internal { emit LogBytes2(p0); } event LogBytes3(bytes3 p0); function logBytes3(bytes3 p0) internal { emit LogBytes3(p0); } event LogBytes4(bytes4 p0); function logBytes4(bytes4 p0) internal { emit LogBytes4(p0); } event LogBytes5(bytes5 p0); function logBytes5(bytes5 p0) internal { emit LogBytes5(p0); } event LogBytes6(bytes6 p0); function logBytes6(bytes6 p0) internal { emit LogBytes6(p0); } event LogBytes7(bytes7 p0); function logBytes7(bytes7 p0) internal { emit LogBytes7(p0); } event LogBytes8(bytes8 p0); function logBytes8(bytes8 p0) internal { emit LogBytes8(p0); } event LogBytes9(bytes9 p0); function logBytes9(bytes9 p0) internal { emit LogBytes9(p0); } event LogBytes10(bytes10 p0); function logBytes10(bytes10 p0) internal { emit LogBytes10(p0); } event LogBytes11(bytes11 p0); function logBytes11(bytes11 p0) internal { emit LogBytes11(p0); } event LogBytes12(bytes12 p0); function logBytes12(bytes12 p0) internal { emit LogBytes12(p0); } event LogBytes13(bytes13 p0); function logBytes13(bytes13 p0) internal { emit LogBytes13(p0); } event LogBytes14(bytes14 p0); function logBytes14(bytes14 p0) internal { emit LogBytes14(p0); } event LogBytes15(bytes15 p0); function logBytes15(bytes15 p0) internal { emit LogBytes15(p0); } event LogBytes16(bytes16 p0); function logBytes16(bytes16 p0) internal { emit LogBytes16(p0); } event LogBytes17(bytes17 p0); function logBytes17(bytes17 p0) internal { emit LogBytes17(p0); } event LogBytes18(bytes18 p0); function logBytes18(bytes18 p0) internal { emit LogBytes18(p0); } event LogBytes19(bytes19 p0); function logBytes19(bytes19 p0) internal { emit LogBytes19(p0); } event LogBytes20(bytes20 p0); function logBytes20(bytes20 p0) internal { emit LogBytes20(p0); } event LogBytes21(bytes21 p0); function logBytes21(bytes21 p0) internal { emit LogBytes21(p0); } event LogBytes22(bytes22 p0); function logBytes22(bytes22 p0) internal { emit LogBytes22(p0); } event LogBytes23(bytes23 p0); function logBytes23(bytes23 p0) internal { emit LogBytes23(p0); } event LogBytes24(bytes24 p0); function logBytes24(bytes24 p0) internal { emit LogBytes24(p0); } event LogBytes25(bytes25 p0); function logBytes25(bytes25 p0) internal { emit LogBytes25(p0); } event LogBytes26(bytes26 p0); function logBytes26(bytes26 p0) internal { emit LogBytes26(p0); } event LogBytes27(bytes27 p0); function logBytes27(bytes27 p0) internal { emit LogBytes27(p0); } event LogBytes28(bytes28 p0); function logBytes28(bytes28 p0) internal { emit LogBytes28(p0); } event LogBytes29(bytes29 p0); function logBytes29(bytes29 p0) internal { emit LogBytes29(p0); } event LogBytes30(bytes30 p0); function logBytes30(bytes30 p0) internal { emit LogBytes30(p0); } event LogBytes31(bytes31 p0); function logBytes31(bytes31 p0) internal { emit LogBytes31(p0); } event LogBytes32(bytes32 p0); function logBytes32(bytes32 p0) internal { emit LogBytes32(p0); } event Log(uint p0); function log(uint p0) internal { emit Log(p0); } event Log(string p0); function log(string memory p0) internal { emit Log(p0); } event Log(bool p0); function log(bool p0) internal { emit Log(p0); } event Log(address p0); function log(address p0) internal { emit Log(p0); } event Log(uint p0, uint p1); function log(uint p0, uint p1) internal { emit Log(p0, p1); } event Log(uint p0, string p1); function log(uint p0, string memory p1) internal { emit Log(p0, p1); } event Log(uint p0, bool p1); function log(uint p0, bool p1) internal { emit Log(p0, p1); } event Log(uint p0, address p1); function log(uint p0, address p1) internal { emit Log(p0, p1); } event Log(string p0, uint p1); function log(string memory p0, uint p1) internal { emit Log(p0, p1); } event Log(string p0, string p1); function log(string memory p0, string memory p1) internal { emit Log(p0, p1); } event Log(string p0, bool p1); function log(string memory p0, bool p1) internal { emit Log(p0, p1); } event Log(string p0, address p1); function log(string memory p0, address p1) internal { emit Log(p0, p1); } event Log(bool p0, uint p1); function log(bool p0, uint p1) internal { emit Log(p0, p1); } event Log(bool p0, string p1); function log(bool p0, string memory p1) internal { emit Log(p0, p1); } event Log(bool p0, bool p1); function log(bool p0, bool p1) internal { emit Log(p0, p1); } event Log(bool p0, address p1); function log(bool p0, address p1) internal { emit Log(p0, p1); } event Log(address p0, uint p1); function log(address p0, uint p1) internal { emit Log(p0, p1); } event Log(address p0, string p1); function log(address p0, string memory p1) internal { emit Log(p0, p1); } event Log(address p0, bool p1); function log(address p0, bool p1) internal { emit Log(p0, p1); } event Log(address p0, address p1); function log(address p0, address p1) internal { emit Log(p0, p1); } event Log(uint p0, uint p1, uint p2); function log(uint p0, uint p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, uint p1, string p2); function log(uint p0, uint p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, uint p1, bool p2); function log(uint p0, uint p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, uint p1, address p2); function log(uint p0, uint p1, address p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, string p1, uint p2); function log(uint p0, string memory p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, string p1, string p2); function log(uint p0, string memory p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, string p1, bool p2); function log(uint p0, string memory p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, string p1, address p2); function log(uint p0, string memory p1, address p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, bool p1, uint p2); function log(uint p0, bool p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, bool p1, string p2); function log(uint p0, bool p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, bool p1, bool p2); function log(uint p0, bool p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, bool p1, address p2); function log(uint p0, bool p1, address p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, address p1, uint p2); function log(uint p0, address p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, address p1, string p2); function log(uint p0, address p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, address p1, bool p2); function log(uint p0, address p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(uint p0, address p1, address p2); function log(uint p0, address p1, address p2) internal { emit Log(p0, p1, p2); } event Log(string p0, uint p1, uint p2); function log(string memory p0, uint p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(string p0, uint p1, string p2); function log(string memory p0, uint p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(string p0, uint p1, bool p2); function log(string memory p0, uint p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(string p0, uint p1, address p2); function log(string memory p0, uint p1, address p2) internal { emit Log(p0, p1, p2); } event Log(string p0, string p1, uint p2); function log(string memory p0, string memory p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(string p0, string p1, string p2); function log(string memory p0, string memory p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(string p0, string p1, bool p2); function log(string memory p0, string memory p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(string p0, string p1, address p2); function log(string memory p0, string memory p1, address p2) internal { emit Log(p0, p1, p2); } event Log(string p0, bool p1, uint p2); function log(string memory p0, bool p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(string p0, bool p1, string p2); function log(string memory p0, bool p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(string p0, bool p1, bool p2); function log(string memory p0, bool p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(string p0, bool p1, address p2); function log(string memory p0, bool p1, address p2) internal { emit Log(p0, p1, p2); } event Log(string p0, address p1, uint p2); function log(string memory p0, address p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(string p0, address p1, string p2); function log(string memory p0, address p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(string p0, address p1, bool p2); function log(string memory p0, address p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(string p0, address p1, address p2); function log(string memory p0, address p1, address p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, uint p1, uint p2); function log(bool p0, uint p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, uint p1, string p2); function log(bool p0, uint p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, uint p1, bool p2); function log(bool p0, uint p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, uint p1, address p2); function log(bool p0, uint p1, address p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, string p1, uint p2); function log(bool p0, string memory p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, string p1, string p2); function log(bool p0, string memory p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, string p1, bool p2); function log(bool p0, string memory p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, string p1, address p2); function log(bool p0, string memory p1, address p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, bool p1, uint p2); function log(bool p0, bool p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, bool p1, string p2); function log(bool p0, bool p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, bool p1, bool p2); function log(bool p0, bool p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, bool p1, address p2); function log(bool p0, bool p1, address p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, address p1, uint p2); function log(bool p0, address p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, address p1, string p2); function log(bool p0, address p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, address p1, bool p2); function log(bool p0, address p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(bool p0, address p1, address p2); function log(bool p0, address p1, address p2) internal { emit Log(p0, p1, p2); } event Log(address p0, uint p1, uint p2); function log(address p0, uint p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(address p0, uint p1, string p2); function log(address p0, uint p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(address p0, uint p1, bool p2); function log(address p0, uint p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(address p0, uint p1, address p2); function log(address p0, uint p1, address p2) internal { emit Log(p0, p1, p2); } event Log(address p0, string p1, uint p2); function log(address p0, string memory p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(address p0, string p1, string p2); function log(address p0, string memory p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(address p0, string p1, bool p2); function log(address p0, string memory p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(address p0, string p1, address p2); function log(address p0, string memory p1, address p2) internal { emit Log(p0, p1, p2); } event Log(address p0, bool p1, uint p2); function log(address p0, bool p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(address p0, bool p1, string p2); function log(address p0, bool p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(address p0, bool p1, bool p2); function log(address p0, bool p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(address p0, bool p1, address p2); function log(address p0, bool p1, address p2) internal { emit Log(p0, p1, p2); } event Log(address p0, address p1, uint p2); function log(address p0, address p1, uint p2) internal { emit Log(p0, p1, p2); } event Log(address p0, address p1, string p2); function log(address p0, address p1, string memory p2) internal { emit Log(p0, p1, p2); } event Log(address p0, address p1, bool p2); function log(address p0, address p1, bool p2) internal { emit Log(p0, p1, p2); } event Log(address p0, address p1, address p2); function log(address p0, address p1, address p2) internal { emit Log(p0, p1, p2); } } ``` ## templates/utils/Math.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; /// @author Modified from Forge standard lib (https://github.com/foundry-rs/forge-std/blob/master/src/StdMath.sol) contract Math { int256 private constant INT256_MIN = -57896044618658097711785492504343953926634992332820282019728792003956564819968; function abs(int256 a) internal pure returns (uint256) { // Required or it will fail when `a = type(int256).min` if (a == INT256_MIN) { return 57896044618658097711785492504343953926634992332820282019728792003956564819968; } return uint256(a > 0 ? a : -a); } function delta(uint256 a, uint256 b) internal pure returns (uint256) { return a > b ? a - b : b - a; } function delta(int256 a, int256 b) internal pure returns (uint256) { // a and b are of the same sign // this works thanks to two's complement, the left-most bit is the sign bit if ((a ^ b) > -1) { return delta(abs(a), abs(b)); } // a and b are of opposite signs return abs(a) + abs(b); } function percentDelta(uint256 a, uint256 b) internal pure returns (uint256) { uint256 absDelta = delta(a, b); return absDelta * 1e18 / b; } function percentDelta(int256 a, int256 b) internal pure returns (uint256) { uint256 absDelta = delta(a, b); uint256 absB = abs(b); return absDelta * 1e18 / absB; } function max(uint256 a, uint256 b) internal pure returns (uint256) { return a > b ? a : b; } function min(uint256 a, uint256 b) internal pure returns (uint256) { return a < b ? a : b; } } ``` ## templates/utils/MockERC20.sol ```solidity // SPDX-License-Identifier: MIT pragma solidity >=0.6.2 <0.9.0; /// @dev Interface of the ERC20 standard as defined in the EIP. /// @dev This includes the optional name, symbol, and decimals metadata. interface IERC20 { /// @dev Emitted when `value` tokens are moved from one account (`from`) to another (`to`). event Transfer(address indexed from, address indexed to, uint256 value); /// @dev Emitted when the allowance of a `spender` for an `owner` is set, where `value` /// is the new allowance. event Approval(address indexed owner, address indexed spender, uint256 value); /// @notice Returns the amount of tokens in existence. function totalSupply() external view returns (uint256); /// @notice Returns the amount of tokens owned by `account`. function balanceOf(address account) external view returns (uint256); /// @notice Moves `amount` tokens from the caller's account to `to`. function transfer(address to, uint256 amount) external returns (bool); /// @notice Returns the remaining number of tokens that `spender` is allowed /// to spend on behalf of `owner` function allowance(address owner, address spender) external view returns (uint256); /// @notice Sets `amount` as the allowance of `spender` over the caller's tokens. /// @dev Be aware of front-running risks: https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 function approve(address spender, uint256 amount) external returns (bool); /// @notice Moves `amount` tokens from `from` to `to` using the allowance mechanism. /// `amount` is then deducted from the caller's allowance. function transferFrom(address from, address to, uint256 amount) external returns (bool); /// @notice Returns the name of the token. function name() external view returns (string memory); /// @notice Returns the symbol of the token. function symbol() external view returns (string memory); /// @notice Returns the decimals places of the token. function decimals() external view returns (uint8); } /// @notice This is a mock contract of the ERC20 standard for testing purposes only, it SHOULD NOT be used in production. /// @notice Includes open deal function to mint tokens to any address. /// @dev Forked from: https://github.com/transmissions11/solmate/blob/0384dbaaa4fcb5715738a9254a7c0a4cb62cf458/src/tokens/ERC20.sol contract MockERC20 is IERC20 { /*////////////////////////////////////////////////////////////// METADATA STORAGE //////////////////////////////////////////////////////////////*/ string internal _name; string internal _symbol; uint8 internal _decimals; function name() external view override returns (string memory) { return _name; } function symbol() external view override returns (string memory) { return _symbol; } function decimals() external view override returns (uint8) { return _decimals; } /*////////////////////////////////////////////////////////////// ERC20 STORAGE //////////////////////////////////////////////////////////////*/ uint256 internal _totalSupply; mapping(address => uint256) internal _balanceOf; mapping(address => mapping(address => uint256)) internal _allowance; function totalSupply() external view override returns (uint256) { return _totalSupply; } function balanceOf(address owner) external view override returns (uint256) { return _balanceOf[owner]; } function allowance(address owner, address spender) external view override returns (uint256) { return _allowance[owner][spender]; } /*////////////////////////////////////////////////////////////// EIP-2612 STORAGE //////////////////////////////////////////////////////////////*/ uint256 internal INITIAL_CHAIN_ID; bytes32 internal INITIAL_DOMAIN_SEPARATOR; mapping(address => uint256) public nonces; /*////////////////////////////////////////////////////////////// CONSTRUCTOR //////////////////////////////////////////////////////////////*/ constructor(address recipient, uint256 mintAmount, string memory name, string memory symbol, uint8 decimals) { _name = name; _symbol = symbol; _decimals = decimals; INITIAL_CHAIN_ID = _pureChainId(); INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator(); _mint(recipient, mintAmount * 10 ** decimals); } /*////////////////////////////////////////////////////////////// ERC20 LOGIC //////////////////////////////////////////////////////////////*/ function approve(address spender, uint256 amount) public virtual override returns (bool) { _allowance[msg.sender][spender] = amount; emit Approval(msg.sender, spender, amount); return true; } function transfer(address to, uint256 amount) public virtual override returns (bool) { _balanceOf[msg.sender] = _sub(_balanceOf[msg.sender], amount); _balanceOf[to] = _add(_balanceOf[to], amount); emit Transfer(msg.sender, to, amount); return true; } function transferFrom(address from, address to, uint256 amount) public virtual override returns (bool) { uint256 allowed = _allowance[from][msg.sender]; // Saves gas for limited approvals. if (allowed != ~uint256(0)) _allowance[from][msg.sender] = _sub(allowed, amount); _balanceOf[from] = _sub(_balanceOf[from], amount); _balanceOf[to] = _add(_balanceOf[to], amount); emit Transfer(from, to, amount); return true; } /*////////////////////////////////////////////////////////////// DEAL LOGIC //////////////////////////////////////////////////////////////*/ function deal(uint256 amount) public virtual { _mint(msg.sender, amount); } function deal(address to, uint256 amount) public virtual { _mint(to, amount); } /*////////////////////////////////////////////////////////////// EIP-2612 LOGIC //////////////////////////////////////////////////////////////*/ function permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) public virtual { require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED"); address recoveredAddress = ecrecover( keccak256( abi.encodePacked( "\x19\x01", DOMAIN_SEPARATOR(), keccak256( abi.encode( keccak256( "Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)" ), owner, spender, value, nonces[owner]++, deadline ) ) ) ), v, r, s ); require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER"); _allowance[recoveredAddress][spender] = value; emit Approval(owner, spender, value); } function DOMAIN_SEPARATOR() public view virtual returns (bytes32) { return _pureChainId() == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator(); } function computeDomainSeparator() internal view virtual returns (bytes32) { return keccak256( abi.encode( keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"), keccak256(bytes(_name)), keccak256("1"), _pureChainId(), address(this) ) ); } /*////////////////////////////////////////////////////////////// INTERNAL MINT/BURN LOGIC //////////////////////////////////////////////////////////////*/ function _mint(address to, uint256 amount) internal virtual { _totalSupply = _add(_totalSupply, amount); _balanceOf[to] = _add(_balanceOf[to], amount); emit Transfer(address(0), to, amount); } function _burn(address from, uint256 amount) internal virtual { _balanceOf[from] = _sub(_balanceOf[from], amount); _totalSupply = _sub(_totalSupply, amount); emit Transfer(from, address(0), amount); } /*////////////////////////////////////////////////////////////// INTERNAL SAFE MATH LOGIC //////////////////////////////////////////////////////////////*/ function _add(uint256 a, uint256 b) internal pure returns (uint256) { uint256 c = a + b; require(c >= a, "ERC20: addition overflow"); return c; } function _sub(uint256 a, uint256 b) internal pure returns (uint256) { require(a >= b, "ERC20: subtraction underflow"); return a - b; } /*////////////////////////////////////////////////////////////// HELPERS //////////////////////////////////////////////////////////////*/ // We use this complex approach of `_viewChainId` and `_pureChainId` to ensure there are no // compiler warnings when accessing chain ID in any solidity version supported by forge-std. We // can't simply access the chain ID in a normal view or pure function because the solc View Pure // Checker changed `chainid` from pure to view in 0.8.0. function _viewChainId() private view returns (uint256 chainId) { // Assembly required since `block.chainid` was introduced in 0.8.0. assembly { chainId := chainid() } address(this); // Silence warnings in older Solc versions. } function _pureChainId() private pure returns (uint256 chainId) { function() internal view returns (uint256) fnIn = _viewChainId; function() internal pure returns (uint256) pureChainId; assembly { pureChainId := fnIn } chainId = pureChainId(); } } ``` ## templates/utils/PropertiesAsserts.sol ```solidity // SPDX-License-Identifier: Unlicense pragma solidity >=0.6.2 <0.9.0; import {StringUtils} from "./StringUtils.sol"; /// @author Modified from Crytic (https://github.com/crytic/properties/blob/main/contracts/util/PropertiesAsserts.sol) contract PropertiesAsserts is StringUtils { event AssertFail(string); event AssertEqFail(string); event AssertNeqFail(string); event AssertGteFail(string); event AssertGtFail(string); event AssertLteFail(string); event AssertLtFail(string); function t(bool b, string memory reason) internal { if (!b) { emit AssertFail(reason); assert(false); } } /// @notice asserts that a is equal to b. Violations are logged using reason. function eq(uint256 a, uint256 b, string memory reason) internal { if (a != b) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "!=", bStr, ", reason: ", reason ); emit AssertEqFail(string(assertMsg)); assert(false); } } /// @notice int256 version of eq function eq(int256 a, int256 b, string memory reason) internal { if (a != b) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "!=", bStr, ", reason: ", reason ); emit AssertEqFail(string(assertMsg)); assert(false); } } /// @notice asserts that a is not equal to b. Violations are logged using reason. function neq(uint256 a, uint256 b, string memory reason) internal { if (a == b) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "==", bStr, ", reason: ", reason ); emit AssertNeqFail(string(assertMsg)); assert(false); } } /// @notice int256 version of neq function neq(int256 a, int256 b, string memory reason) internal { if (a == b) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "==", bStr, ", reason: ", reason ); emit AssertNeqFail(string(assertMsg)); assert(false); } } /// @notice asserts that a is greater than or equal to b. Violations are logged using reason. function gte(uint256 a, uint256 b, string memory reason) internal { if (!(a >= b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "<", bStr, " failed, reason: ", reason ); emit AssertGteFail(string(assertMsg)); assert(false); } } /// @notice int256 version of gte function gte(int256 a, int256 b, string memory reason) internal { if (!(a >= b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "<", bStr, " failed, reason: ", reason ); emit AssertGteFail(string(assertMsg)); assert(false); } } /// @notice asserts that a is greater than b. Violations are logged using reason. function gt(uint256 a, uint256 b, string memory reason) internal { if (!(a > b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "<=", bStr, " failed, reason: ", reason ); emit AssertGtFail(string(assertMsg)); assert(false); } } /// @notice int256 version of gt function gt(int256 a, int256 b, string memory reason) internal { if (!(a > b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, "<=", bStr, " failed, reason: ", reason ); emit AssertGtFail(string(assertMsg)); assert(false); } } /// @notice asserts that a is less than or equal to b. Violations are logged using reason. function lte(uint256 a, uint256 b, string memory reason) internal { if (!(a <= b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, ">", bStr, " failed, reason: ", reason ); emit AssertLteFail(string(assertMsg)); assert(false); } } /// @notice int256 version of lte function lte(int256 a, int256 b, string memory reason) internal { if (!(a <= b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, ">", bStr, " failed, reason: ", reason ); emit AssertLteFail(string(assertMsg)); assert(false); } } /// @notice asserts that a is less than b. Violations are logged using reason. function lt(uint256 a, uint256 b, string memory reason) internal { if (!(a < b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, ">=", bStr, " failed, reason: ", reason ); emit AssertLtFail(string(assertMsg)); assert(false); } } /// @notice int256 version of lt function lt(int256 a, int256 b, string memory reason) internal { if (!(a < b)) { string memory aStr = toString(a); string memory bStr = toString(b); bytes memory assertMsg = abi.encodePacked( "Invalid: ", aStr, ">=", bStr, " failed, reason: ", reason ); emit AssertLtFail(string(assertMsg)); assert(false); } } } ``` ## templates/utils/StringUtils.sol ```solidity // SPDX-License-Identifier: Unlicense pragma solidity >=0.6.2 <0.9.0; /// @notice Efficient library for creating string representations of integers. /// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/LibString.sol) /// @author Modified from Solady (https://github.com/Vectorized/solady/blob/main/src/utils/LibString.sol) /// @dev Name of the library is modified to prevent collisions with contract-under-test uses of LibString contract StringUtils { function toString(int256 value) internal pure returns (string memory str) { uint256 absValue = value >= 0 ? uint256(value) : uint256(-value); str = toString(absValue); if (value < 0) { str = string(abi.encodePacked("-", str)); } } function toString(uint256 value) internal pure returns (string memory str) { /// @solidity memory-safe-assembly assembly { // The maximum value of a uint256 contains 78 digits (1 byte per digit), but we allocate 160 bytes // to keep the free memory pointer word aligned. We'll need 1 word for the length, 1 word for the // trailing zeros padding, and 3 other words for a max of 78 digits. In total: 5 * 32 = 160 bytes. let newFreeMemoryPointer := add(mload(0x40), 160) // Update the free memory pointer to avoid overriding our string. mstore(0x40, newFreeMemoryPointer) // Assign str to the end of the zone of newly allocated memory. str := sub(newFreeMemoryPointer, 32) // Clean the last word of memory it may not be overwritten. mstore(str, 0) // Cache the end of the memory to calculate the length later. let end := str // We write the string from rightmost digit to leftmost digit. // The following is essentially a do-while loop that also handles the zero case. // prettier-ignore for { let temp := value } 1 {} { // Move the pointer 1 byte to the left. str := sub(str, 1) // Write the character to the pointer. // The ASCII index of the '0' character is 48. mstore8(str, add(48, mod(temp, 10))) // Keep dividing temp until zero. temp := div(temp, 10) // prettier-ignore if iszero(temp) { break } } // Compute and cache the final total length of the string. let length := sub(end, str) // Move the pointer 32 bytes leftwards to make room for the length. str := sub(str, 32) // Store the string's length at the start of memory allocated for our string. mstore(str, length) } } function toString(address value) internal pure returns (string memory str) { bytes memory s = new bytes(40); for (uint i = 0; i < 20; i++) { bytes1 b = bytes1( uint8(uint(uint160(value)) / (2 ** (8 * (19 - i)))) ); bytes1 hi = bytes1(uint8(b) / 16); bytes1 lo = bytes1(uint8(b) - 16 * uint8(hi)); s[2 * i] = char(hi); s[2 * i + 1] = char(lo); } return string(s); } function char(bytes1 b) internal pure returns (bytes1 c) { if (uint8(b) < 10) return bytes1(uint8(b) + 0x30); else return bytes1(uint8(b) + 0x57); } } ```