# circom-auditor Audit Circom circuits for soundness, completeness, privacy, and constraint bugs. Use when the user asks to audit, review, check, or find vulnerabilities in Circom code, or when they ask to run circom-auditor on a repo or specific .circom files. - **Kind:** skill - **Source:** https://github.com/zksecurity/zk-skills - **Page:** https://forefy.com/skills/f51f66f4-645b-4e44-9981-92420f658a10 - **API (JSON + files):** https://forefy.com/api/asr/f51f66f4-645b-4e44-9981-92420f658a10 --- ## README.md # Circom Auditor A runtime-neutral skill for security review of Circom circuits. It audits for soundness, completeness, privacy, and constraint bugs while keeping an efficient path for both Codex and Claude-style agent runtimes. Built for: - Circom developers who want a soundness check before a commit. - ZK security researchers looking for fast witness-manipulation leads. - Protocol teams that want repeatable local or delegated circuit review. This is not a replacement for a formal audit. Treat it as a high-signal review assistant that still needs human validation. For deep AI scans focused on vulnerability discovery in any cryptography code, visit [zkao.io](https://zkao.io). ## Runtime Behavior - **Codex:** defaults to delegated mode when `spawn_agent`-style subagents are available. Codex delegated mode uses the same 17 generated audit bundles as the Claude workflow, with at most 6 agents running at once. If subagents are unavailable, or if you ask for "local mode", "no subagents", or "single-agent pass", Codex uses the deterministic local workflow. - **Claude-style runtimes:** default to the high-throughput 17-agent workflow when `Agent`, `Read`, `Glob`, and `Grep` are available. Ask for "local mode", "no subagents", or "single-agent pass" to avoid spawning agents. - **Unknown runtimes:** use the local Codex fallback workflow. Parallel/subagent review is the default in Codex and Claude-style runtimes when subagent tooling is available. Every audit starts with the circom-auditor banner and a visible markdown progress console. Local audits show phase-level progress. Delegated audits show one row per selected agent, including the agent lens, current status, and final result. Delegated audits run at most 6 agents in parallel; remaining selected agents stay queued until a worker slot opens. Native subagent UI is runtime-dependent, so the markdown console is the portable fallback. ## Usage Audit every in-scope `.circom` file in a repo: ```text Use $circom-auditor to audit the Circom circuits in this repo. ``` Audit specific files: ```text Use $circom-auditor to audit circuits/Spend.circom circuits/MerkleRoot.circom. ``` Run a delegated audit when the runtime supports subagents: ```text Use $circom-auditor to run a delegated parallel audit of this repo. ``` Run a local-only audit in Codex or Claude: ```text Use $circom-auditor to audit this repo in local mode with no subagents. ``` Also write the final report to `assets/findings/`: ```text Use $circom-auditor --file-output to audit this repo. ``` ## What Gets Scanned Default scope is all in-scope `.circom` files under the current repo. If files are named explicitly, only those files and their in-scope local includes are audited. Excluded by default: ```text node_modules/ circuits/test/ tests/ __tests__/ dependencies/circomlib/ lib/circomlib/ build/ dist/ artifacts/ out/ *.test.circom *_test.circom *-test.circom *.witness.json *.r1cs *.zkey ``` Vendored and external circomlib files are treated as peripheral context. The auditor focuses on your in-scope code and flags caller-side misuse of library preconditions. ## Context Builder The shared helper script discovers scope, resolves includes, collects local docs and prior findings, and creates audit bundles: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" ``` For specific files: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" --files path/to/A.circom path/to/B.circom ``` If the script is run from outside the skill directory layout, pass `--skill-dir /path/to/skills/circom-auditor` so bundled references resolve correctly. Generated files include: - `source.md`: source bundle plus include graph and peripheral manifest. - `docs-context.md`: local `assets/docs/` markdown/text files, if present. - `prior-findings.md`: local `assets/findings/*.md`, if present. - `agent-1-bundle.md` through `agent-17-bundle.md`: delegated audit bundles. URL lists in `assets/docs/` are not fetched automatically. Fetch external docs only when the user explicitly authorizes network access. ## Version Checks Normal audits do not perform remote version checks. This keeps Codex runs deterministic and avoids network failures in restricted environments. When you want to check for updates, ask explicitly, for example: ```text Check whether $circom-auditor is up to date. ``` ## References The main skill keeps runtime selection and core workflow in `SKILL.md`. Detailed runtime-specific instructions live in: - `references/orchestration/codex.md` - `references/orchestration/claude.md` Audit judgment and output format live in: - `references/judging.md` - `references/report-formatting.md` Specialized audit lenses live in `references/hacking-agents/`, and broad attack catalogs live in `references/attack-vectors/`. ## Tips - Target hot circuits when possible. Smaller scopes leave more context for concrete witness paths. - Put protocol notes and threat models in `assets/docs/`; the auditor uses them to understand intended semantics. - Keep previous reports in `assets/findings/`; the auditor revalidates still relevant issues. - Prefer strict primitives such as `Num2Bits_strict` and `Bits2Num_strict`. - Run more than once for high-risk code. LLM review is non-deterministic and different passes may surface different witness paths. ## SKILL.md --- name: circom-auditor description: "Audit Circom circuits for soundness, completeness, privacy, and constraint bugs. Use when the user asks to audit, review, check, or find vulnerabilities in Circom code, or when they ask to run circom-auditor on a repo or specific .circom files." --- # Circom Auditor Use this skill to review Circom circuits for exploitable constraint bugs. The skill directory is the directory containing this `SKILL.md`; bundled references live under `references/`, and deterministic helper scripts live under `scripts/`. ## Runtime Selection - In Codex with `spawn_agent`-style subagents available, default to delegated mode in `references/orchestration/codex.md`. Delegated Codex runs use the same generated agent bundles as the Claude workflow, adapted to Codex subagent tooling. Use local Codex mode only when subagents are unavailable or when the user explicitly asks for local mode, no subagents, or a single-agent pass. - In Claude with `Agent`/`Read`/`Glob`/`Grep` tools available, default to the 17-agent workflow in `references/orchestration/claude.md`. Use a local single-agent Claude audit only when the user explicitly asks for local mode, no subagents, or a single-agent pass. - If the runtime is unclear, follow the Codex local fallback workflow. Do not run a remote version check during ordinary audits. Network may be restricted; keep the audit deterministic from local files unless the user explicitly asks to check for updates. ## Audit Console Start every audit by printing this banner exactly, unless the user explicitly asks for no banner: ```text ███████╗██╗ ██╗███████╗███████╗ ██████╗██╗ ██╗██████╗ ██╗████████╗██╗ ██╗ ╚══███╔╝██║ ██╔╝██╔════╝██╔════╝██╔════╝██║ ██║██╔══██╗██║╚══██╔══╝╚██╗ ██╔╝ ███╔╝ █████╔╝ ███████╗█████╗ ██║ ██║ ██║██████╔╝██║ ██║ ╚████╔╝ ███╔╝ ██╔═██╗ ╚════██║██╔══╝ ██║ ██║ ██║██╔══██╗██║ ██║ ╚██╔╝ ███████╗██║ ██╗███████║███████╗╚██████╗╚██████╔╝██║ ██║██║ ██║ ██║ ╚══════╝╚═╝ ╚═╝╚══════╝╚══════╝ ╚═════╝ ╚═════╝ ╚═╝ ╚═╝╚═╝ ╚═╝ ╚═╝ c i r c o m · a u d i t o r ``` Then show a visible markdown progress console. In local mode, show audit phases. In delegated mode, show one row per agent with its lens, status, and result. Delegated mode uses a bounded worker pool: at most 6 agents may be `Running` at once, and the remaining selected agents must stay `Queued` until a slot opens. Update the console as phases or agents move from `Pending` to `Queued`, `Running`, `Done`, `Skipped`, or `Blocked`. If the runtime has a native subagent UI, use it, but still print a compact markdown summary so transcripts record which agents ran and when they finished. If the runtime only returns parallel agent results after the whole batch finishes, spawn at most 6 agents in that batch, print the table before spawning, then print an updated table before starting the next queued batch. ## Inputs - Default scope: all in-scope `.circom` files under the current repo. - Specific scope: if the user names one or more files, audit only those files plus local includes that are in scope. - `--file-output`: also write the final report to `assets/findings/{project-name}-zksec-circom-audit-report-{timestamp}.md`. - Delegated mode: default in Codex and Claude when subagent tooling is available; local mode is an explicit opt-out or fallback. Exclude directories and artifacts matching: ```text node_modules/ circuits/test/ tests/ __tests__/ dependencies/circomlib/ lib/circomlib/ build/ dist/ artifacts/ out/ *.test.circom *_test.circom *-test.circom *.witness.json *.r1cs *.zkey ``` ## Build Audit Context Prefer the bundled helper script to ad hoc shell pipelines: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" ``` For specific files: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" --files path/to/A.circom path/to/B.circom ``` When the skill is installed somewhere else, resolve the script relative to the directory containing this `SKILL.md`. The script writes a scratch directory under `/tmp` unless `--out` is supplied. It creates: - `source.md`: in-scope Circom files plus an include graph and peripheral manifest. - `docs-context.md`: local `assets/docs/` markdown/text context, if present. - `prior-findings.md`: local `assets/findings/*.md`, if present. - `agent-1-bundle.md` through `agent-17-bundle.md`: source plus specialized reference instructions for delegated mode. If Python is unavailable, fall back to `rg --files -g '*.circom'` or `find` with the exclude list above, then read includes manually with: ```bash rg -n '^\s*include\s+"[^"]+"' ``` ## Required References Always read: - `references/judging.md` before validating candidates. - `references/report-formatting.md` before producing a report. For broad audits, also read: - `references/attack-vectors/attack-vectors.md` For targeted passes, load only the relevant file from `references/hacking-agents/`: - `vector-scan-agent.md`: classify templates and risky dependencies. - `signal-flow-agent.md`: unconstrained witness flow and public/private binding. - `range-check-agent.md`: aliasing, comparator inputs, limb bounds. - `arithmetic-field-agent.md`: field wraparound, inverse/division patterns. - `selector-mux-agent.md`: boolean selectors, disabled constraints, muxes. - `invariant-agent.md`: cross-template invariants. - `intent-binding-agent.md`: nullifier, replay, domain separation, docs. - `first-principles-agent.md`: end-to-end semantic attacks. - `free-flow-agent.md`: independent adversarial pass. ## Local Audit Workflow 1. Resolve scope with `scripts/build_audit_context.py`. 2. Read `source.md`, `references/judging.md`, and `references/report-formatting.md`. 3. For broad audits, read `references/attack-vectors/attack-vectors.md`. 4. Read project docs from `docs-context.md` if present; use them only to understand intended semantics, never to excuse missing constraints. 5. Revalidate any still-relevant issues from `prior-findings.md`. 6. Inspect the in-scope files for concrete witness manipulation paths: - `<--` assignments without paired constraints. - `assert(...)` used where a runtime constraint was intended. - missing `Num2Bits_strict`, `Bits2Num_strict`, comparator input bounds, or limb bounds. - division/inverse constraints without nonzero checks and multiplication pins. - selector, mux, and enable signals missing booleanity constraints. - public inputs, nullifiers, commitments, or signatures not bound to the intended domain/action. - field wraparound or aliasing near `p`, especially when values are later interpreted as integers. - peripheral library preconditions that callers fail to enforce. 7. For every candidate, apply the four gates in `judging.md` exactly once: refutation, reachability, trigger, impact. 8. Report confirmed findings and high-signal leads. Do not report style, optimization, deployer-intent assumptions, or self-harm-only issues. ## Delegated Audit Workflow Build context with `scripts/build_audit_context.py`, then follow the runtime-specific orchestration: - Codex delegated mode: default when `spawn_agent`-style subagents are available; see `references/orchestration/codex.md`. - Claude delegated mode: the default Claude workflow when `Agent`/`Read`/`Glob` /`Grep` are available; see `references/orchestration/claude.md`. Worker outputs must be deduplicated by `group_key`, validated with `references/judging.md`, and formatted with `references/report-formatting.md`. Every confirmed finding needs a concrete proof or witness path. No proof means the item remains a lead. Preserve detector provenance: tag every raw worker `FINDING` and `LEAD` with the source agent id, union those ids during deduplication, and include the final detector set in every reported finding and lead. ## Output Use `references/report-formatting.md`. - In local mode, omit delegated-triage fields and sections. - In delegated mode, include triage verdicts and reasoning only when triage workers were actually run. - If there are no confirmed findings, say so plainly and include any leads or residual test gaps. - If `--file-output` was requested, write the same report to the report path specified in `references/report-formatting.md` and mention the path in the final answer. ## VERSION ``` ``` ## agents ``` ``` ## agents/openai.yaml ```yaml interface: display_name: "Circom Auditor" short_description: "Audit Circom circuits for constraint bugs" default_prompt: "Use $circom-auditor to audit the Circom circuits in this repo for soundness and privacy bugs." policy: allow_implicit_invocation: true ``` ## assets ``` ``` ## assets/docs ``` ``` ## assets/docs/README.md # Project Docs Drop any context that helps the auditor understand what the protocol is supposed to do: - Design docs and specs - Intended invariants (what the prover must prove, what the verifier learns) - Threat model (who's malicious, what they can do off-chain) - Plain-English descriptions of circuit behavior - Known limitations or accepted tradeoffs Files can be plain text or markdown. To reference online docs, create a file containing one URL per line — they will be fetched and read automatically. At bundle-build time, the orchestrator materializes a `docs-context` file for the `free-flow-agent`: - Local text/markdown files are appended as-is with path headers. - Files whose non-empty lines are all `http://` or `https://` URLs are treated as fetch lists; each URL is fetched and appended under a URL header. - Failed fetches are noted and skipped so the audit can continue. The `free-flow-agent` (agent #9) reads that bundled docs context to build a mental model of the protocol. A 1-page README with the threat model dramatically improves protocol-level findings. ## assets/findings ``` ``` ## assets/findings/README.md # Findings This directory holds two kinds of reports: - **Reports from previous `/circom-auditor` runs** — written automatically as `{project-name}-zksec-circom-audit-report-{timestamp}.md` each time the skill runs with `--file-output`. - **External audit reports** — drop any third-party or manual audit `.md` files here. On each run the orchestrator builds a `prior-findings` bundle from the markdown files in this directory and re-verifies those issues against the current code during the final dedup/output pass. - Issues still present are carried forward with a `Previously reported — still present` note. - Issues that are no longer present are silently skipped. - Revalidation works best for reports already in the skill's own markdown format, but the orchestrator also makes a best-effort pass over other markdown audit reports. ## evals ``` ``` ## evals/benchmarks ``` ``` ## evals/benchmarks/circomlib-decoder.md --- repo_url: https://github.com/zksecurity/zkbugs repo_ref: main contracts_dir: dataset/circom/iden3/circomlib/veridise_decoder_accepting_bogus_output_signal --- # Ground Truth — circomlib Decoder Accepting Bogus Output Source: https://github.com/zksecurity/zkbugs/tree/main/dataset/circom/iden3/circomlib/veridise_decoder_accepting_bogus_output_signal The canonical V-D6 (`one-sided-decoder` / `Decoder` not enforcing one-hot) instance from the iden3/circomlib core library. The original template enforces `out[i] * (inp - i) === 0` (i.e. `out[i] = 0 OR inp = i`) but does NOT enforce `sum_i out[i] === 1` and does NOT enforce `out[i] ∈ {0, 1}`. The prover supplies `out = [0, 0, ..., 0]` regardless of `inp`, and a `success` output signal that should reflect "is `inp` in domain" can be set to anything. ## Findings FINDING | id: H-1 | severity: High | template: Decoder | signal: out | bug_class: one-sided-decoder description: `Decoder` enforces only the one-sided constraint `out[i] * (inp - i) === 0` for each index — which holds when `out[i] = 0` for every `i` regardless of `inp`. There is no booleanity constraint (`out[i] * (out[i] - 1) === 0`) and no one-hot sum constraint (`sum_i out[i] === 1`), so the prover can produce `out = [0, 0, 0, 0]` (or any field-element vector that satisfies the one-sided product) and an arbitrary `success` flag, breaking every consumer of `Decoder` for one-hot / membership selection. Fix: add both booleanity and sum-to-one constraints, or use `IsEqual(inp, i).out` per slot to derive `out[i]` from a constraint-bound source. Cross-reference: every circomlib consumer (`Multiplexer`-style templates) inherits this bug until either the consumer adds the missing constraints or the library template is fixed. ## evals/benchmarks/selfxyz-packbytes.md --- repo_url: https://github.com/zksecurity/zkbugs repo_ref: main contracts_dir: dataset/circom/selfxyz/self/zksecurity_second_pre_image_attacks_on_packbytesandposeidon_may_be_used_to_register_arbitrary_passports_and_dsc_certificates --- # Ground Truth — selfxyz/Self PackBytesAndPoseidon Second-Preimage Source: https://github.com/zksecurity/zkbugs/tree/main/dataset/circom/selfxyz/self/zksecurity_second_pre_image_attacks_on_packbytesandposeidon_may_be_used_to_register_arbitrary_passports_and_dsc_certificates The canonical V-B5 (`packbytes-input-byte-range-missing`) instance: `PackBytes(k)` packs an input byte array into a single field element by computing `sum_i bytes[i] * 256^i`, but does NOT enforce `bytes[i] < 256` for each index. Combined with a Poseidon hash downstream, this enables second-preimage collisions on certificate / passport commitments. ## Findings FINDING | id: H-1 | severity: High | template: PackBytesAndPoseidon | signal: bytes[i] | bug_class: packbytes-input-byte-range-missing description: `PackBytes` consumes its input array as raw field elements without `Num2Bits(8)` on each entry. A malicious prover supplies one byte equal to 256 (or any value with a 9th bit set), which packs to the same field element as a different byte sequence with carry propagated into the next slot. Two distinct passport / DSC byte sequences therefore hash to the same Poseidon commitment, allowing the attacker to register an arbitrary passport under a legitimate-looking certificate root. Fix: insert `Num2Bits(8)(bytes[i])` for every input byte before passing to `PackBytes`. ## evals/benchmarks/wormprivacy-spend.md --- repo_url: https://github.com/zksecurity/zkbugs repo_ref: main contracts_dir: dataset/circom/worm-privacy/proof-of-burn/koukyosyumei_spend_missing_range_check --- # Ground Truth — worm-privacy proof-of-burn `Spend` (Missing Range Check on GreaterEqThan) Source: https://github.com/zksecurity/zkbugs/tree/main/dataset/circom/worm-privacy/proof-of-burn/koukyosyumei_spend_missing_range_check The canonical V-B1 (`comparator-input-not-range-checked`) instance with **both comparator operands free**: `Spend()` checks `balance >= withdrawnBalance` with `GreaterEqThan(252)` but never constrains `balance` or `withdrawnBalance` to fit in 252 bits. Unlike a constant-pinned comparator, both operands are prover-influenced (`balance` is a witness input, `withdrawnBalance` is a public input the prover picks), so the field-overflow attack is directly reachable in this exact instantiation. The vulnerable `Spend` template is fully inlined in `circuit.circom`; the only includes are circomlib (`comparators.circom`, `mimcsponge.circom`). ## Findings FINDING | id: H-1 | severity: High | template: Spend | signal: balance | bug_class: comparator-input-not-range-checked description: `GreaterEqThan(252)` is invoked on `balance` and `withdrawnBalance` with no upstream `Num2Bits` (or equivalent) range check on either operand. `GreaterEqThan(n)` is only correct when both inputs are `< 2^n`; here both are arbitrary BN254 field elements. A malicious prover sets `balance = 0` and `withdrawnBalance = p - 38` (any value just below the prime): internally `LessThan(252)` computes `withdrawnBalance + 2^252 - (balance + 1) ≡ 2^252 - 39 (mod p)`, whose bit 252 is 0, so `sufficientBalanceChecker.out === 1` is satisfied even though `balance < withdrawnBalance` in the integer domain. The prover thus produces a valid `Spend` proof withdrawing more than the burned balance, breaking soundness. The fix is to range-check both inputs before the comparison — e.g. `Num2Bits(maxAmountBits)(balance)` and `Num2Bits(maxAmountBits)(withdrawnBalance)` with `maxAmountBits` well below 252 (the upstream fix parameterizes `Spend(maxAmountBits)` and swaps in `AssertGreaterEqThan(maxAmountBits)`, instantiated as `Spend(200)`). ## evals/compare.md # Eval Compare Compare an audit report against ground truth findings. You will be given two files: 1. **Ground truth** — the benchmark file with known findings (FINDING blocks in the frontmatter region). 2. **Report** — the audit output (`final-report.md` or `full-output.txt`). ## Steps 1. Read the ground truth file. Parse each `FINDING` line and its `description:` line. 2. Read the report file. Identify two sections: - **Findings** — between `## Findings` and `## Leads` - **Leads** — from `## Leads` to end of file 3. For each ground truth finding, determine if the report caught it. Use semantic matching — the report doesn't need to use the exact same words, but must describe the same vulnerability in the same template/signal/bug-class. Classify each as: - **FOUND** — the vulnerability appears in the Findings section. The report identifies the same template, the same signal or local entry point, and the same root cause (even if described differently). - **LEAD** — the vulnerability appears only in the Leads section with the same criteria above. - **MISSED** — not present in either section. ## Output Write `summary.md` to the run directory with this exact format: ``` ## Eval Results | Metric | Value | |--------|-------| | Recall (findings) | {found} / {total} ({pct}%) | | In leads only | {leads} | | Missed | {missed} | | High | {high_found} / {high_total} | | Medium | {med_found} / {med_total} | | Reported findings | {count from report} | ### Per-finding breakdown | Status | Severity | ID | Template.Signal | Bug Class | |--------|----------|----|------------------|-----------| | FOUND | High | H-1 | Template.signal | bug-class | | LEAD | Medium | M-2 | Template.signal | bug-class | | MISSED | Medium | M-3 | Template.signal | bug-class | ``` ## Rules - Match semantically, not by keyword grep. "LessThan operands not range-checked" matches "comparator-input-not-range-checked" even without those exact words. - A finding in the Leads section is NOT a finding — it's a lead. Don't count it toward recall. - If the report describes the same root cause but attributes it to a different signal in the same template, still count it as FOUND. - If the report merges two ground-truth findings into one reported finding, count both as FOUND. - Treat the V-X.Y `vector_id` as canonical when both sides supply it; otherwise rely on (template, signal, bug-class) triple. ## evals/runner.md # Eval Runner Run the circom-auditor skill against a **sanitized copy** of each benchmark's zkbugs minimal-reproducer subdir (circuit sources only — the dataset's `README.md` / `zkbugs_config.json` / `zkbugs_*.sh` answer-key files are stripped) and compare results to ground truth. The auditor must never see those files: they name the bug class, root cause, fix, and a `Reproduced` flag, which would contaminate the audit. `Reproduced: false` is a dataset tooling status (no reproduction harness shipped), **not** a security signal. ## Usage These examples assume you invoke `claude` from the repo root. ``` claude "read skills/circom-auditor/evals/runner.md and run all benchmarks" claude "read skills/circom-auditor/evals/runner.md and run wormprivacy-spend" ``` ## Setup Resolve paths, create the plugin symlink, get the commit hash, and generate a timestamp. `SKILL_DIR` is the `skills/circom-auditor/` directory (parent of `evals/`). `REPO_ROOT` is the git repo root. Both must be absolute paths. ```bash REPO_ROOT="$(git rev-parse --show-toplevel)" SKILL_DIR="$REPO_ROOT/skills/circom-auditor" mkdir -p /tmp/audit-plugin/skills && ln -sfn "$SKILL_DIR" /tmp/audit-plugin/skills/circom-auditor COMMIT=$(git -C "$REPO_ROOT" rev-parse --short=7 HEAD) TIMESTAMP=$(date +%Y%m%d-%H%M%S) echo "commit=$COMMIT timestamp=$TIMESTAMP" ``` ## Run Each `.md` file in `evals/benchmarks/` is a benchmark with frontmatter: `repo_url`, `repo_ref` (optional), `contracts_dir` (the path under the cloned repo to a single zkbugs minimal-reproducer subdir). For each benchmark, clone the repo (shallow, skip if `/tmp/eval-{name}` exists), build a sanitized source tree at `/tmp/eval-clean-{name}` (see **Sanitize** below), and create `{run_dir}` at `evals/results/{name}/{timestamp}-{commit}`. Run benchmarks **sequentially** in this fixed order: **wormprivacy-spend → selfxyz-packbytes → circomlib-decoder**. Each run gets a fresh `claude` process so context does not carry over between benchmarks. **Sanitize (anti-contamination).** The auditor runs in `/tmp/eval-clean-{name}`, which contains only the slice's `.circom` files plus circomlib as read-on-demand peripheral context under `node_modules/circomlib/` (kept out of the in-scope scan by the skill's `node_modules/` exclude rule). The zkbugs `README.md`, `zkbugs_config.json`, `zkbugs_*.sh`, and `*_input.json` files are never copied — running the auditor in the raw slice leaks the entire answer key. A benchmark whose vulnerable template lives in a missing app-level `include` (not inlined and not circomlib) is **not self-contained**: the auditor cannot see the bug without hunting outside the tree, so it cannot be scored honestly — fix the benchmark, do not re-expose the metadata. The `--plugin-dir /tmp/audit-plugin` flag is **required** — it makes the skill discoverable via the symlink created in Setup. Without it, `claude` will report "Unknown skill: circom-auditor". ```bash BENCHMARKS_DIR="$SKILL_DIR/evals/benchmarks" RESULTS_DIR="$SKILL_DIR/evals/results" for name in wormprivacy-spend selfxyz-packbytes circomlib-decoder; do BENCH="$BENCHMARKS_DIR/$name.md" [ -f "$BENCH" ] || continue # Read repo_url and contracts_dir from frontmatter REPO_URL=$(grep '^repo_url:' "$BENCH" | sed 's/repo_url: *//') CONTRACTS_DIR=$(grep '^contracts_dir:' "$BENCH" | sed 's/contracts_dir: *//' || true) CLONE_DIR="/tmp/eval-$name" WORK_DIR="$CLONE_DIR${CONTRACTS_DIR:+/$CONTRACTS_DIR}" CLEAN_DIR="/tmp/eval-clean-$name" CIRCOMLIB="$CLONE_DIR/dataset/circom/dependencies/circomlib" RUN_DIR="$RESULTS_DIR/$name/$TIMESTAMP-$COMMIT" # Clone (shallow) once; reuse on subsequent runs [ -d "$CLONE_DIR" ] || git clone --depth 1 "$REPO_URL" "$CLONE_DIR" # Sanitize: copy ONLY the .circom sources into a clean tree — never the zkbugs # answer-key files (README.md, zkbugs_config.json, zkbugs_*.sh, *_input.json). # Provide circomlib under node_modules/ as read-on-demand peripheral context # (the skill's node_modules/ rule keeps it out of the in-scope scan, and find's # default no-symlink-follow keeps it out of the find sweep). [ -d "$CLEAN_DIR" ] && rm -r "$CLEAN_DIR" # fresh tree each run (no stale assets/findings) rsync -a -m --include='*/' --include='*.circom' --exclude='*' "$WORK_DIR/" "$CLEAN_DIR/" mkdir -p "$CLEAN_DIR/node_modules" [ -d "$CIRCOMLIB" ] && ln -sfn "$CIRCOMLIB" "$CLEAN_DIR/node_modules/circomlib" echo "=== Starting $name ===" mkdir -p "$RUN_DIR" && \ cd "$CLEAN_DIR" && mkdir -p assets/audit-logs && \ claude --print --plugin-dir /tmp/audit-plugin --dangerously-skip-permissions \ "run circom auditor with --file-output" 2>&1 | tee "$RUN_DIR/full-output.txt" && \ cp -r "$(ls -dt assets/findings/*-zksec-circom-audit-report-*.md | head -1)" "$RUN_DIR/final-report.md" 2>/dev/null; \ cp "$BENCH" "$RUN_DIR/ground-truth.md" echo "=== Finished $name ===" done echo "All benchmarks complete." ``` After all complete, for each `{run_dir}`: read `skills/circom-auditor/evals/compare.md`, compare `{run_dir}/ground-truth.md` against `{run_dir}/final-report.md`, write `summary.md` to `{run_dir}/`. Print each summary and `=== All done. {count} benchmarks. ===` ## references ``` ``` ## references/attack-vectors ``` ``` ## references/attack-vectors/attack-vectors.md # Circom Attack Vectors — Index A curated library of 48 soundness, completeness, and privacy vectors for Circom circuits. Each vector is grounded in at least one real audit finding from the zkbugs dataset or a published audit report. Per-vector format: **D** description / **FP** false-positive guard / **Source** real-bug citation. The vectors are organized by **code shape** (the kind of Circom construct you grep for), not by abstract bug class. To keep each scanning agent's context focused, the catalog is split across **six slice files** — a vector-scan agent reads only its slice, never the whole catalog. ## Categories - **A. Signal flow** — `<--` vs `<==` / `===` mismatches, unassigned outputs, decompositions without recomposition. - **B. Range checks** — comparators, packers, bit-decompositions whose operands aren't bounded. - **C. Arithmetic / field** — division-by-zero, EC degeneracies, modular reduction not enforced. - **D. Selector / mux** — conditional gate collapse, mux selectors not boolean, assert-vs-constraint. - **E. Accumulator** — wrong init seeds, wrong-side keying. - **G. Regex / encoding** — sentinel-byte abuse, regex overlap, base64 mismatch. - **H. Protocol binding** — replay, unbound public input, sentinel leaf, low-entropy nullifier. - **L. Language-level footguns** — Circom-language pitfalls that don't show up in real audits often but bite developers at write-time. ## Slice manifest | Slice file | Categories | Vectors | Count | | ---------- | ---------- | ------- | ----- | | `attack-vectors/signal-field.md` | A + C | V-A1–A5, V-C1, V-C3–C6 | 10 | | `attack-vectors/range.md` | B | V-B1–B7 | 7 | | `attack-vectors/selector-accumulator.md` | D + E | V-D1–D7, V-E1–E2 | 9 | | `attack-vectors/binding-1.md` | H | V-H1–H8 | 8 | | `attack-vectors/binding-2.md` | H | V-H9–H16 | 8 | | `attack-vectors/regex-language.md` | G + L | V-G1, V-L1–L5 | 6 | Total: 48 vectors. Categories: A:5, B:7, C:5, D:7, E:2, G:1, H:16, L:5. (V-C2 retired — folded into V-A3; its id is not reused.) ## Cross-cutting auditor mantras - **Every `<--` is a constraint hole until proven otherwise.** - **Every `LessThan(N)` operand must come from a `Num2Bits(M ≤ N)` chain.** - **Every `Num2Bits(254)` over BN254 needs `_strict` or an alias check.** - **Every divisor in `<-- a/b` needs `IsZero(b).out === 0` upstream.** - **Every `Mux*` selector needs `s * (s - 1) === 0` upstream.** - **Every public input must appear in at least one `===` / `<==` constraint.** - **`assert(...)` is not a constraint — it's a compile-time check the verifier never sees.** Each slice file repeats the mantras relevant to its categories, so an agent reading only its slice has the discipline it needs. ## references/attack-vectors/binding-1.md # Circom Attack Vectors — Protocol-binding slice I (replay, nullifiers, public inputs, privacy) Your slice of the catalog: category **H (protocol binding)**, part 1 of 2 — vectors **H1–H8** (8 vectors). These cover the gap between *what the protocol intends a proof to mean* and *what the circuit actually pins down*: replay, unbound public inputs, sentinel leaves, disabled verifiers, low-entropy nullifiers, and privacy leaks. Part 2 (signatures, merkle, sponge, format) is the `binding-2` slice. Format: **D** defect / **FP** false-positive guard. Organized by **code shape**. Mantra for this slice: - **Every public input must appear in at least one `===` / `<==` constraint.** --- ## H. Protocol binding (H1–H8) **V-H1. Proof not bound to caller intent** - **D:** A nullifier-burning / state-mutating verifier exposes only protocol-state public inputs (`pubRoot`, `pubNullifierHash`, `pubCreditType`) and no caller-controlled binding (`msg.sender`, intent hash, transaction nonce). An observer of the mempool re-broadcasts the proof from their own address, burning the nullifier and stealing the funds. - **FP:** A `pubIntentHash` (or `pubReceiver`, `pubCallData`) public input is constrained inside the circuit and bound to caller-controllable context on-chain (e.g. `keccak256(msg.sender, callData)` mirrored as the public input). **V-H2. Static issuer commitment omits per-action variable** - **D:** A Poseidon commitment `H(sig[0..2])` computed identically across all actions of one issuer is constant per issuer. Deanonymising one token deanonymises every other — privacy leak by linkability. - **FP:** Commitment binds a per-action variable (`tokenId`, `epoch`, `slot`) that is publicly exposed: `Poseidon(4)(sig[0], sig[1], sig[2], tokenId)`. **V-H3. Sentinel zero leaf admitted as valid membership proof** - **D:** Merkle-tree templates that use `zeroValue` for empty leaves but never assert `leaf != zeroValue` admit anyone whose identity-commitment hashes to the sentinel as an unremovable group member. With Semaphore's empty-tree zero, computing `Poseidon(Poseidon(n, t)) == zeroValue` brute-force grants universal membership. - **FP:** Explicit `IsEqual()([leaf, zeroValue]).out === 0` in the membership circuit. Or the tree uses a non-cryptographic distinguishing value for empty leaves (e.g. domain-tagged sentinel that can never collide with a valid commitment). **V-H4. Public input declared but never constrained** - **D:** A `signal input` listed in `public [...]` (or top-level `main` declaration) that never appears on either side of `===` / `<==` / `<--` is a free public variable. The prover proves any value; the verifier accepts any value. Particularly insidious when the host language (Solidity / `verifier.sol`) trusts the public input and the linear "dummy use" is optimised away by `circom -O2`. - **FP:** Public input appears in at least one non-linear constraint (`signal dummy <== x * x;` is the canonical anti-`-O2` pattern). Or public input is folded into a hash whose digest is independently constrained (`Poseidon(pub, secret)`). **V-H5. Verifier gadget toggle hard-coded to `0`** - **D:** Circomlib gadgets (`EdDSAPoseidonVerifier`, `ForceEqualIfEnabled`, `BabyCheck`) take an `enabled` toggle. Hard-coding `eddsa.enabled <== 0` turns off the entire signature check while leaving the gadget visually present in the source. Pattern: any imported verifier with an `enabled` set to a constant zero or a witness-derived signal that can be zeroed. - **FP:** `enabled <== 1` for security-critical checks; or `enabled` is bound to a publicly-committed flag whose zero-branch is independently re-enforced (V-D1). **V-H6. Low-entropy / non-context-binding nullifier** - **D:** A nullifier `H(privKey)` (or `H(name, DOB, last4)`) without a per-action / per-context binding lets an identity holder re-register after small mutations (case, ordering, initials) — Sybil. In Panther's case, the renewal nullifier `H(privKey, commitment)` is replayable when `commitment` doesn't bind `privKey` to the public identity. Generalisation: nullifier preimage must include high-entropy per-context data plus a `privKey ↔ pubKey` consistency proof. - **FP:** Nullifier is `H(s, ctx)` with `ctx` publicly committed AND a `BabyPbk(s).Ax === pubKey[0]; BabyPbk(s).Ay === pubKey[1];` consistency constraint. Or per-token / per-epoch normalisation hashes high-entropy fields. **V-H7. Time-bound credential fed only into a hash, never compared** - **D:** A signal named `*Timestamp` / `*Expiry` / `*Time` that is folded into a Poseidon hash but never compared (`LessThan`, `LessEqThan`, `ForceLessThan`) against current block time / chain header timestamp. The prover produces an indistinguishable proof for an expired credential. - **FP:** `kycSignedMessageTimestamp + kycExpiryPeriod >= spendTime` (or `<= currentBlockTime`) enforced via `GreaterEqThan` / `ForceLessThan`; the comparator's input is range-checked (V-B1). **V-H8. Privacy leak via comparison constraint not fully gated by privacy flag** - **D:** `LessEqThan(252)([statementValue, sourceValue]).out === 1` is an unconditional inequality, while a paired `(statementValue - sourceValue) * statementComparator === 0` equality is gated by a privacy flag. When the protocol advertises an "anonymous mode", the always-on inequality leaks `sourceValue >= statementValue` even when comparison is supposedly disabled. - **FP:** Multiply the residue `(leq.out - 1)` by the enable flag so the inequality also becomes a no-op when disabled; or collapse equality and inequality into a single `Mux1`-gated branch where the disabled output is a known canonical value. --- Slice total: 8 vectors (H1–H8). ## references/attack-vectors/binding-2.md # Circom Attack Vectors — Protocol-binding slice II (signatures, merkle, sponge, format) Your slice of the catalog: category **H (protocol binding)**, part 2 of 2 — vectors **H9–H16** (8 vectors). These cover signature-gadget preconditions, affine ECDSA, merkle/SMT construction footguns, Poseidon/sponge collisions, inter-circuit and circuit↔host format mismatches, liveness/DoS via prover-controlled commitments, and compiler/parameter footguns. Part 1 (replay, nullifiers, public inputs, privacy) is the `binding-1` slice. Format: **D** defect / **FP** false-positive guard. Organized by **code shape**. Mantra for this slice: - **A signature/merkle gadget enforces only what its body constrains — every precondition (on-curve, in-subgroup, `< order`, fixed depth, domain tag) is the caller's job until proven otherwise.** --- ## H. Protocol binding (H9–H16) **V-H9. Affine relation with free precomputed points and no message binding** - **D:** An "efficient ECDSA" circuit accepts precomputed points `T`, `U` as private inputs and only checks `pubKey = s*T + U` (an affine relation). Without per-point constraints tying `T` and `U` to the message and randomness (`U = -m * r^-1 * G`, `T = r^-1 * R`), the prover treats `(T, U, s)` as three free variables and solves for any target `pubKey` in the membership tree. - **FP:** Expose `m` and the signature components publicly; constrain each precomputed point against the message inside the circuit; or reject the "efficient" gadget in favour of a direct EC scalar-mult formulation. **V-H10. Replicated intermediate with `_temp` / `_final` / `_intermediate` suffix confusion** - **D:** Two intermediate signals differ only by a `_temp` / `_final` suffix (e.g. `drv_mGrY[j].xout` vs `drv_mGrY_final[j].xout`). A consumer references the wrong stage — typically the pre-padding intermediate when the post-padding one was intended — and the resulting ciphertext / commitment is computed from stale data. Mechanical bug, easy to grep, easy to miss in review. - **FP:** Mechanical rename + grep audit: every consumer of `_temp` is independently justified, every consumer of `_final` is justified. Pair-suffix suspicion is itself a flag. **V-H11. Signature gadget precondition not enforced at call site** - **D:** EdDSA / BLS / ECDSA verifier gadgets accept (`pubKey`, `message`, `signature`) without checking on-curve, in-subgroup, less-than-curve-order, less-than-modulus. Caller assumes the gadget enforces these; gadget assumes the caller does. Examples: `R8X, R8Y` not `BabyCheck`'d before `EdDSAPoseidonVerifier`; `r, s` not in `[1, n-1]` for ECDSA; signature limbs not range-checked against modulus; suborder tag not actually enforcing `< suborder`. - **FP:** Each canonical precondition is enforced at the boundary: `BabyCheck()(R8X, R8Y)`, `BigLessThan(...)(r, n).out === 1`, `BigLessThan(...)(s, n).out === 1`, suborder reduction. Or the precondition is provably inherited from upstream (signature was just hashed from a trusted source). **V-H12. Domain-separation / variable-length Poseidon collisions** - **D:** Poseidon used over variable-length input without folding the length and a domain tag into the capacity / state hashes the same digest for `[a, b, 0]` and `[a, b]`, or for two protocol-distinct messages with the same field elements. Pattern: any `PoseidonFieldArray` / hand-rolled Merkle-Damgård chaining over Poseidon, or `SpongeHash` that doesn't follow the SAFE API padding rules. - **FP:** `PoseidonEx(t, capacity)` with `initialState = DOMAIN_TAG | length`; or the SAFE API. Length is part of the public input set and committed by the verifier. **V-H13. Merkle construction footguns (depth, intermediate-as-leaf, truncated leaves)** - **D:** Cluster of Merkle-tree implementation bugs that don't fit V-D2 / V-H3 / V-E1: (a) branch length not validated against the fixed tree depth — `restoreMerkleRoot` accepts forged inclusion at the wrong depth; (b) `MerkleRootCalculator` accepts an intermediate node as a leaf because no leaf-vs-node distinguisher is enforced; (c) SMT stores 64-bit truncated hashes — collision risk at 2^32 leaves; (d) generic length / depth fields not bound to the tree contract. - **FP:** Tree depth is a compile-time parameter and `assert(depth == MAX_DEPTH)`; leaf hashes carry a domain tag distinguishing them from internal nodes; SMT uses full-width digests. **V-H14. Inter-circuit / circuit ↔ host data-format mismatch** - **D:** A public input that is computed off-circuit, consumed by a different circuit, or returned to/from Solidity has a precise byte/bit format. When the two ends disagree — `data[SUM_FIELD_COUNT]` interpreted differently in `ProveReputation` vs `UserStateTransition`, or `ZSwap.sol` skipping a deposit transfer the circuit assumed happened, or the circuit trusting the prover's `start_offset` for public-key location — a soundness or correctness bug appears at the boundary. - **FP:** Both ends share a generated specification or a property-tested binding; format invariants are documented and tested with fuzz/randomised inputs. **V-H15. Liveness / DoS via prover-controlled commitment data** - **D:** A multi-step protocol where step `N`'s output commitment is computed by the prover and consumed in step `N+1`. A malicious step-`N` prover commits to ill-formed data (BigInts whose limbs exceed `2^n`, sync-committee aggregates with `(0,0)` "infinity" pubkeys, 96-bit caps applied to 112-bit products) that satisfies step-N constraints by accident but provably cannot satisfy any honest step-`N+1` proof. Honest provers in subsequent rounds are bricked. - **FP:** Every commitment-input limb is `Num2Bits(n)` checked at step `N`; aggregator outputs an explicit `is_infinity` / `is_well_formed` flag that downstream rounds consume; comparator widths conservatively dominate every reachable product width. **V-H16. Compiler / parameter footguns (hardcoded array sizes, implicit parameter relations)** - **D:** Circom helpers with hardcoded array dimensions (`bigInt[50]`) silently overflow when called with `k > 50`; templates with implicit parameter relations (`BigMult` assumes `k ≤ 2^n`; `Split`/`SplitThree` assume `n + m + k < 254`; `ModSumFour` requires `n + 3 ≤ 253`) emit no compile-time check and produce silently-wrong constraints when violated. `SSZLayer` silently no-ops for `numBytes < 64`. - **FP:** Top-of-template `assert(k < 50)` / `assert(n + m + k < 254)` block making implicit relations explicit; treat hardcoded magic numbers (50, 32, 512, 254) as audit flags whose surrounding parameter relations must be documented. --- Slice total: 8 vectors (H9–H16). ## references/attack-vectors/range.md # Circom Attack Vectors — Range-check slice Your slice of the catalog: category **B (range checks)** — 7 vectors. Each vector is grounded in a real audit finding. Format: **D** defect / **FP** false-positive guard. Vectors are organized by **code shape** — the construct you grep for, not an abstract bug class. This is the most prolific class of Circom soundness bugs in the wild. Mantras for this slice: - **Every `LessThan(N)` operand must come from a `Num2Bits(M ≤ N)` chain.** - **Every `Num2Bits(254)` over BN254 needs `_strict` or an alias check.** --- ## B. Range checks **V-B1. Comparator input not range-checked** - **D:** `LessThan(N)` / `LessEqThan(N)` / `GreaterThan(N)` / `GreaterEqThan(N)` assume each operand fits in `N` bits. With un-range-checked inputs, the prover supplies values like `p − k` for small `k`; the internal `Num2Bits(N+1)` of `(1<`) is **not** "if flag then check" — it's "the disabled branch trivially satisfies the check at zero". Whenever `flag = 0`, both sides go to zero and the constraint is `0 === 0`. The author intended graceful disablement; the actual semantics are silent bypass. ```circom // panther: nullifier-verification-can-be-disabled zAccountUtxoInNullifierHasherProver.enabled <== zAccountUtxoInSpendPrivKey; // attacker sets spendPrivKey = 0 → ForceEqualIfEnabled disabled → any nullifier accepts ``` - **FP:** `flag` is hard-bounded by an upstream boolean constraint AND the disabled-branch outcome is the protocol-intended one (re-enforced via a `Mux1` to a known-canonical value); or the gating uses `ForceEqualIfEnabled` correctly with both branches independently constrained. **V-D2. Merkle-path / mux selector not boolean-constrained** - **D:** `MultiMux1(2)(c, indices[i])` computes `out = (c[1] - c[0]) * s + c[0]`. When `s` is not constrained to `{0, 1}`, the prover linearly interpolates between the two branches and forges any leaf at any path. Same trap with custom Merkle templates whose `path_index[i]` array is fed straight from `signal input` without `path_index[i] * (path_index[i] - 1) === 0`. - **FP:** Selector is derived from another comparator's `.out` (already boolean), or `s * (s - 1) === 0` is enforced locally before the mux. **V-D3. Array selector via `LessThan(idx, n)` instead of sum-of-equality** - **D:** Array indexing gadgets that gate `out[i] = (idx == i) ? arr[i] : 0` via `LessThan(idx, n)` silently return all-zero output for out-of-range `idx` (or for `idx + p`-style aliases). Downstream "if out is zero, treat as default" logic accepts the invalid index. - **FP:** Selector built as `out[i] <== IsEqual()([i, idx]).out * arr[i]` with `Σ IsEqual()([i, idx]).out === 1` enforced (exactly-one match). **V-D4. Loop bound strictly less than tag/index domain** - **D:** `assert(offset < 16)` followed by `for (var i = 0; i < 15; i++) { is_equal[i].in[1] <== offset; }` — the loop never visits `i = 15`, so `offset = 15` matches no iteration and the entire chained `enabled` accumulator stays at its initial value (often `0` or `1`), bypassing the inclusion check. Combine with V-D5 (assert-vs-constraint) for a complete bypass. - **FP:** Loop bound covers the full domain of the index's tag/range (e.g. `for i < 16` for a 4-bit tag); or the index domain is hard-bounded by a `ForceLessThan(bits)` matching the loop bound. **V-D5. `assert(...)` mistaken for a constraint** - **D:** Circom's `assert` is a witness-generator-time check. It does **not** emit an R1CS constraint and is not enforced by the verifier. Common misuses: bounding offsets (`assert(offset < 16)`), validating padding bytes (`assert(eM[0] === 188)` for RSA-PSS 0xBC trailer), or anti-replay guards. The host prover crashes during witness generation if the assert fails honestly, but a malicious prover constructs a witness directly and bypasses the assert entirely. - **FP:** Each `assert(...)` is paired with a real constraint gadget (`ForceLessThan`, `IsZero(...).out === 0`, `Num2Bits`, `===`) that mirrors the same predicate. **V-D6. One-hot decoder without IsZero pairing** - **D:** `out[i] <-- (inp == i) ? 1 : 0; out[i] * (inp - i) === 0;` is one-sided: the constraint forces `out[i] = 0` when `inp != i`, but the matching slot is never forced to `1`. The prover can set every `out[i] = 0` and `success = 0` to make the decoder accept any `inp`. - **FP:** Replace the witness hint and one-sided constraint with `out[i] <== IsZero(inp - i).out;` — the IsZero template emits both directions. **V-D7. Non-determinism / multiple valid witnesses for one public output** - **D:** A template's public output can be produced by more than one witness assignment — typically because length / padding / leading-zero data can vary while hashing to the same digest. A nonce extractor that admits both `0x0001` and `0x000001` decodings produces distinct `packedNonce` values for the same JWT, breaking equality checks the host language relies on. - **FP:** Length / offset signals are themselves public and bound to a unique canonicalisation; or a tight `Num2Bits` width prevents leading-zero / trailing-zero ambiguity. Picus-style determinism checks pass. --- ## E. Accumulator **V-E1. Multiplicative accumulator seeded with input data instead of `1`** - **D:** `product[0] <== element` instead of `product[0] <== 1` makes a set-membership product `Π (set[i] - element)` collapse to zero whenever `element = 0`, regardless of set contents. Generalisation: every iterated accumulator must seed with the algebraic identity for its operation (`*` → `1`, `+` → `0`, `XOR` → `0`). - **FP:** Seed is the operation's identity element, or the accumulator carries a known-safe domain-separator value, and any seed that depends on input data is independently constrained. **V-E2. Per-key accumulator filtered by the wrong side's key** - **D:** Per-address-sum accumulator `Σ_{addr=k} amount[i]` keyed by the *input* address while aggregating the *output* side (or vice versa) lets one side smuggle entries past the equality check. Concretely: outflow ERC20 sum keyed by `spending_note_token_addr` instead of an outflow address admits any output-side entry whose token addr never appears in the input. - **FP:** Filter key comes from the same side the accumulator aggregates; or the accumulator iterates over the union and rejects mis-matched-side entries explicitly. --- Slice total: 9 vectors (D:7, E:2). ## references/attack-vectors/signal-field.md # Circom Attack Vectors — Signal-flow & Field-arithmetic slice Your slice of the catalog: categories **A (signal flow)** and **C (arithmetic / field)** — 10 vectors. Each vector is grounded in a real audit finding. Format: **D** defect / **FP** false-positive guard. Vectors are organized by **code shape** — the construct you grep for, not an abstract bug class. Mantras for this slice: - **Every `<--` is a constraint hole until proven otherwise.** - **Every divisor in `<-- a/b` needs `IsZero(b).out === 0` upstream.** --- ## A. Signal flow **V-A1. Assigned-but-unconstrained (`<--` without paired `===`)** - **D:** A signal is computed via the witness-only operator `<--` but never tied back to the constraint system with `<==` / `===`. The R1CS therefore admits any field value for the signal and the prover wins. Especially dangerous when the RHS uses a non-quadratic op (`>>`, `<<`, `\`, `%`, `&`, `^`, `?:`), these cannot be expressed as a single quadratic constraint. - **FP:** The signal is later pinned by a structurally parallel set of constraints — e.g. `q <-- a \ k; r <-- a % k; q*k + r === a; Num2Bits(log2(k))(r); LessThan(...)([r, k]).out === 1`. The pattern is "computed-then-bound", not "computed-then-used". The `out <-- 1/x; out * x === 1` inverse witness is sound when paired with `IsZero(x).out === 0`. **V-A2. Output signal declared but never assigned** - **D:** A `signal output Y` is declared but no `Y <==` or `=== Y` ever runs in the template body — typically because the assignment was commented out or replaced with an unrelated expression (variable-name typo). The R1CS compiles cleanly and the prover sets `Y` to any field element. - **Sub-pattern (variable-name typo on the recomposition target):** the final constraint accidentally references the input instead of the locally-recomposed sum, leaving the per-slot output free: ```circom // BinSum-style example, with the recomposition typo'd: for (var k = 0; k < nout; k++) { out[k] <-- (lin >> k) & 1; out[k] * (out[k] - 1) === 0; lout += out[k] * e2; e2 = e2 + e2; } lin === nout; // BUG: should be `lin === lout`; out[] is unconstrained ``` - **FP:** `Y` is assigned via a sub-component output (`Y <== sub.out`) or inside a loop branch — both count. Witness mutation immediately exposes truly-free outputs. **V-A3. Witness-only division paired with one polynomial check** - **D:** Pattern `out <-- num/div; out * div === num` collapses to `0 === 0` whenever `div = 0`, leaving `out` free. Recurs across every Circom EC primitive that computes a slope as `<-- (Δy)/(Δx)` — e.g. Montgomery `λ <-- (y2-y1)/(x2-x1); λ * (x2-x1) === (y2-y1)`, and the Edwards-to-Montgomery / Montgomery-to-Edwards conversions. The divisor reaches zero on a degenerate point pair, point-at-infinity, or sentinel input; the slope then becomes a free variable and the EC operation is forged. - **FP:** An explicit non-zero check on the divisor — `signal isz <== IsZero(div).out; isz === 0;` — or a hard-coded non-zero constant divisor (the `IsZero` template internally provides a non-zero witness, so its output `=== 0` is a valid guard); or the call is dispatched through a wrapper (`EllipticCurveAdd`) that detects degenerate inputs and routes to a doubling formula (see also V-C3). **V-A4. XOR via `a + b - 2ab` without booleanity and recomposition** - **D:** The identity `a + b - 2ab` computes XOR only when `a, b ∈ {0, 1}`. When the per-bit decomposition is written as `a_bits[i] <-- (a >> i) & 1` with the booleanity check (`a_bits[i] * (a_bits[i] - 1) === 0`) commented out, AND the recomposition (`Σ a_bits[i] * 2^i === a`) missing, the prover can pick arbitrary field values for `a_bits[i]` and forge any "xor" output. - **FP:** Inputs are already provably boolean (output of an upstream `IsZero` / `IsEqual` / `Num2Bits` slot) AND the bits are recomposed back to the source: both legs are required if the bits feed an output sum. **V-A5. Shift / rotation reconstructed from one linear identity in two free `<--` signals** - **D:** A 32-bit rotation written as `signal part1 <-- (in << L) & 0xFFFFFFFF; signal part2 <-- in >> (32 - L); (part1 / 2**L) + (part2 * 2**(32-L)) === in;` is one linear equation in two free unknowns. The prover picks any `part2`, computes `part1 = 2^L * (in − part2 * 2^(32-L))`, and `out <== part1 + part2` is an arbitrary 33-bit value. - **FP:** Both halves are individually width-bounded by tight `Num2Bits(L)(part2); Num2Bits(32-L)(part1);` calls upstream — the bit constraint pins each half uniquely. --- ## C. Arithmetic / field **V-C1. Field-element overflow on narrow accumulator** - **D:** A loop accumulating `acc[i] <== base * acc[i-1] + chunk[i]` followed by `acc[N-1] === in` is mod-p arithmetic, not over Z. When `log2(base) * N >= 248`, two distinct chunk vectors hash to the same field element (one canonical, one wrapping `+ p`). Same trap with `BigInt(==)` evaluated as a single accumulated `=== 0` over chunks. - **FP:** The total bit width of the accumulation is provably `< 248` (assert it); each chunk is `Num2Bits(width)`-checked; or the equality is performed limb-by-limb after carry propagation rather than via a single accumulated comparison. **V-C3. AddUnequal-style EC formula collapses on equal inputs / point-at-infinity** - **D:** Any `EllipticCurveAddUnequal` formula (BLS12-381, BN254 Montgomery) keys a polynomial constraint on `(b - a)`. When `a == b` the polynomial reduces to `0 === 0` and the slope/output is unconstrained. Same shape with point-at-infinity inputs to non-affine adders, or aggregations whose all-zero participation bits produce `(0, 0)` instead of identity. - **FP:** Caller dispatches through a safe wrapper that checks `IsEqual(a, b).out === 0` before the AddUnequal call (or routes equal-x inputs to a `Double` template); aggregator emits an explicit `is_infinity` output flag that callers must consume. **V-C4. EC scalar `s = 0` accepted into curve multiplication** - **D:** A scalar `s` feeding `s * T` (curve multiplier) without `IsZero(s).out === 0` collapses to identity for `s = 0`. In `EfficientECDSA`, `pubKey = s*T + U` then equals `U` for any chosen target `U`, forging signature verification. - **FP:** Explicit `IsZero(s).out === 0`, plus a range check `BigLessThan(n, k)(s, q).out === 1` against the curve order; or the scalar is derived from a hashed message that the protocol proves non-zero by other means. **V-C5. "Already reduced" / "no scaling required" comment with no constraint** - **D:** Comments claiming a value is in canonical form, scaled, or pre-reduced rarely emit the matching constraint. When the surrounding code right-shifts by more bits than the value's intended width, the value is silently zeroed (panther `forTxReward` is shifted away by 60 bits when its bit-width is 40); when leaves are claimed representable in 254 bits but `p < 2^254`, some leaves are unrepresentable (completeness bug). - **FP:** Cross-reference the comment with the surrounding `Num2Bits`/`Bits2Num` widths: if `bitwidth(value) <= shift_amount`, flag. If the comment is paired with an explicit `assert(bitwidth(value) > shift_amount)` or with a constraint-emitting scaling step, accept. **V-C6. Accumulator sum overflows mod p before comparison or hashing** - **D:** Chained sums `a + b + c ...` feeding a comparator or hasher without a bound on the total width: when individual operands are 250-bit values, two such sums overflow `p` and wrap. The comparator then mis-classifies, or the hasher collides on inputs that disagree only by a multiple of `p`. - **FP:** Apply `Num2Bits(n)` to the *result* with `n` strictly less than `log2(p) ≈ 254`; or ensure operand bit-widths sum to `< 253` by static analysis. --- Slice total: 10 vectors (A:5, C:5). ## references/hacking-agents ``` ``` ## references/hacking-agents/arithmetic-field-agent.md # Arithmetic Field Agent You are an attacker that exploits field arithmetic. Every division, every elliptic-curve formula, every modular reduction has edge cases where the constraint collapses to `0 === 0` or where the witness-time computation diverges from the constraint-time semantics. Your job is to find them. Other agents cover signal flow, range checks, selectors, invariants, intent binding, and protocol semantics. You exploit **arithmetic-field corner cases**. ## Attack surfaces **Division-by-zero degeneracy (the V-A3 pattern).** Circom's `/` is field-inverse, computed by the prover via `<--`. The corresponding constraint `out * b === a` is sound *only if `b ≠ 0`* — otherwise `0 === 0` is trivially satisfied and `out` is free. Hunt every `<-- num / den` pattern. For each: - Find the corresponding constraint (it's usually 1-3 lines down). - Determine: can `den` be zero in any reachable witness? - If yes and there's no `IsZero(den).out === 0` upstream, finding. Common Circom locations: `MontgomeryAdd.lambda`, `Edwards2Montgomery.u_division`, custom inverse gadgets, ecdsa scalar inversions. **Elliptic-curve edge cases (V-C3, V-C4, V-C5).** `EllipticCurveAddUnequal(a, b)` assumes `a.x ≠ b.x` and reduces to `0 === 0` when they're equal. `MontgomeryDouble(in)` assumes `in.y ≠ 0` and breaks at the curve's 2-torsion point. `EllipticCurveAdd` (the dispatch wrapper) handles both correctly — its absence is a smell. For every EC-add / EC-double callsite: - If `EllipticCurveAddUnequal`: prove the two inputs cannot be equal-x (often they CAN be — e.g. doubling a point produces equal-x). Finding if not provably guarded. - If `MontgomeryDouble`: check whether `in.y` can be zero (always possible if the prover controls `in`). Finding. **EC scalar = 0 / scalar at order (V-C4).** `Secp256k1Mul(s, T)` collapses to point-at-infinity when `s = 0`, and the unguarded `EfficientECDSA` constraint becomes `pubKey = 0 + U`, letting the prover choose `U` to make `pubKey` anything. Hunt every scalar-mul callsite for missing `s != 0` (and `s < curve_order`) checks. **A.3 division-witness-only (cross-cuts signal-flow).** `signal x <-- (in[1] - 1) / (in[0]);` followed by `x * (in[0]) === (in[1] - 1)` looks safe — but if `in[0]` can be 0, the constraint trivially holds for any `x`. Same shape as division-by-zero above. **Field-mod arithmetic mismatches.** Code that assumes integer arithmetic (`a + b`, `a * b`) but is evaluated mod `p`. Especially dangerous when summing many bytes, decimals, or limbs — overflow wraps silently. Always think: "can this sum exceed `p`?". If yes and downstream code assumes the integer value, finding. **Modular-reduction-claimed-but-not-enforced.** `BigMod(a, modulus)` outputs `(quotient, remainder)`. The constraint chain pins `quotient * modulus + remainder === a`, but is the remainder constrained to be `< modulus`? Often not — see V-C5. The prover supplies a remainder ≥ modulus that mathematically satisfies the equation but breaks downstream usage that expects a canonical mod result. ## Break guards An arithmetic-field corner case is safe if: - A division `out <-- a / b` is paired with `IsZero(b).out === 0` (or `b` is a non-zero constant), AND `out * b === a` holds. - An EC-add caller uses `EllipticCurveAdd` (not `*Unequal`), OR proves the inputs cannot be equal-x. - A scalar-mul caller checks `0 < s < curve_order`. - A `BigMod` caller follows up with `BigLessThan(remainder, modulus).out === 1`. Don't trust: - Comments saying "non-zero by construction" without a circuit-level constraint to back it up. - Per-template invariants that hold only in honest execution. ## Output fields Add to FINDINGs: ``` degeneracy_input: concrete field value(s) that trigger the constraint to collapse to 0===0 or that produce an unconstrained witness propagation_chain: which transitive consumers inherit the bug (e.g. Pedersen depends on EscalarMulFix depends on MontgomeryDouble) proof: concrete witness (e.g. lambda = 999, in[0] = 0, out[1] = anything; constraint holds vacuously) ``` ## references/hacking-agents/binding-gap-agent.md # Binding Gap Agent You are an attacker that hunts bugs in the GAPS between three "what does the proof mean" lenses: **intent binding** (what the proof is tied to), **privacy** (what the proof must not reveal), and **conditional gating** (the flags and selectors that switch checks on and off). Each lens has a single-specialty agent — intent-binding, free-flow, selector-mux — running in parallel. They will catch the bare unbound public input, the bare missing intent hash, the bare non-boolean selector. You are NOT here to redo that work. You are here for the bugs that REQUIRE two or three of these lenses at once — where a signal IS constrained (so signal-flow clears it) and IS in range (so range-check clears it), yet the *binding* between the proof and the protocol's intent has a hole that only appears when you combine the lenses. ## Your hunting ground **Seam 1 — gating × intent.** A check that binds the proof to intent (a nullifier, an intent hash, a recipient) is *gated* by a flag, and the prover sets the flag to disable the binding while keeping the rest of the proof valid. Example (the V-D1 × V-H1 seam): `enabled * (nullifier - Poseidon(secret, intentHash)) === 0` — fully constrained, fully in range — but `enabled` is prover-controlled, so `enabled = 0` produces a valid proof bound to *nothing*. The selector agent sees a gate-collapse but reads it as "a check is skipped"; the intent agent sees a present binding and clears it; the seam is that the *binding itself* is the skippable check. **Seam 2 — privacy × gating.** A flag meant to *disable* a comparison only gates one side and leaks the other through the proof or a public output. Example (the V-H8 pattern, sismo hydra-s2): `statementComparator = 0` is supposed to turn a range check off, but only the equality branch is gated — the inequality still constrains a public signal, leaking a lower bound on a private value. The selector agent sees a partial gate; the privacy lens sees a leak; neither alone names that the *leak survives precisely because the disable is one-sided*. **Seam 3 — intent × range (binding through aliasing).** A signal that is correctly recomposed from bits (signal-flow clears it) and feeds an intent/nullifier hash, but the recomposition uses `Num2Bits(254)`/`Bits2Num(254)` so two distinct field elements alias to the same bit-pattern — letting the prover bind the proof to one identity while the verifier reads another. Example: `nullifier = Poseidon(Bits2Num(254)(idBits))` where `idBits` aliases — the spend proof is "bound," but to an ambiguous preimage. The range agent sees a `Num2Bits` it might flag in isolation; the intent agent sees a present `Poseidon` binding and clears it; the seam is binding-to-an-aliased-value. **Seam 4 — three-way.** Gating × intent × privacy: a prover disables an intent binding via a flag AND the disabled path leaks or forges a private attribute. Look for any "proof of X bound to Y, unless flag Z" structure where Z is witness-controlled and the unbound path still produces an accepted, meaningful public output. ## What this looks like in code - A `Poseidon(.., msg.sender)` / `Poseidon(.., intentHash)` binding multiplied by an `enabled` / `selector` signal that is `<--` or a raw private input. - A "disable" flag that gates `a === b` but leaves `a` or `b` constrained against a public signal on the other branch. - A nullifier or commitment built from `Bits2Num(n≥254)` output, where aliasing lets two identities share a nullifier (double-spend) or one identity forge another's. - A sentinel/zero-leaf membership path (V-H3) that is *also* reachable only when a mode selector is zero — the backdoor leaf and the disabled check compound. - A signature-verification gate (`EdDSAPoseidonVerifier` enabled-flag) where disabling verification still emits a public "verified" signal downstream. - A privacy flag whose two branches have asymmetric constraint counts — one branch pins a public output the other leaves free, leaking which branch ran. ## Discipline Do NOT report a bare unbound public input or bare missing intent hash — that's the intent-binding agent. Do NOT report a bare non-boolean selector or bare gate-collapse — that's the selector-mux agent. Do NOT report a bare privacy leak with no gating or binding interaction — that's free-flow's protocol scope. **If a finding can be expressed with one lens alone, drop it.** Your output is bugs where a signal is constrained and in range, yet the binding-to-intent or the privacy guarantee fails at the seam with a flag or an aliased value. Every finding needs a concrete attacker scenario: the witness values for the gate/alias, what the proof ends up bound to (or what it leaks), and why the verifier accepts it. ## Output fields Add to FINDINGs: ``` seam: which two or three lenses combine (gating×intent / privacy×gating / intent×range / three-way) binding_target: what the proof is actually bound to under the attack (vs. what intent requires) — or what it leaks proof: concrete witness — the flag/alias values, the resulting binding-to-nothing or leak, and why the verifier accepts (e.g. enabled = 0 → nullifier binding collapses, proof reusable by any third party) ``` ## references/hacking-agents/composition-gap-agent.md # Composition Gap Agent You are an attacker that hunts bugs in the GAPS between templates — where every template is sound in isolation but the *composition* breaks. Each single-specialty agent reads constraints locally: signal-flow follows one `<--` to its closure, range-check bounds one operand, selector-mux checks one gate. They are blind to the seam where template A satisfies its own contract, template B satisfies its own contract, and the **handoff between them** leaves a signal under-constrained. You are NOT here to redo local work. You are here for the bugs that only exist *across* the template boundary — the ones where reading either template alone shows nothing wrong. ## Your hunting ground **Seam 1 — tag/domain mismatch across the boundary.** Template A produces a signal valid in domain D_A (e.g. a tag `{uint8}`, or "output of `Num2Bits(8)`"); template B consumes it assuming domain D_B (e.g. "fits in 16 bits", or "already `< curve_order`"). Each template is internally consistent. The seam: D_A ⊊ D_B is assumed but never enforced at the handoff. Example: a sub-circuit guarantees `out ∈ [0, 2^8)` and a caller feeds `out` into a `LessThan(4)` that needs `[0, 2^4)` — the producer is sound, the consumer is sound for its domain, the *connection* is unsound. **Seam 2 — constraint assumed "upstream" by one template and "downstream" by the other.** Template A omits a check, commenting/assuming "the caller validates the range"; template B omits the same check, assuming "the sub-circuit already constrained it." Neither emits the constraint. The single-template agents each see a plausible local contract; the seam is the shared assumption that nobody discharges. Hunt every `signal input` whose template body never constrains it AND whose every call-site also never constrains it before passing it in. **Seam 3 — primitive used outside the assumptions of its composition.** A circomlib (or vendored) primitive is sound under its documented preconditions, but the composing template wires it into a context that violates them — `EllipticCurveAddUnequal` fed two outputs of the same doubling, `MultiMux` selector sourced from another template's unconstrained output, `Decoder` consumed for one-hot membership without the caller adding `sum(out) === 1`. The primitive is correct; the *composition* supplies an input outside its contract. Trace the include graph: for each peripheral primitive consumed in scope, list its precondition and find the call-site that breaks it. **Seam 4 — loop / instantiation boundary across templates.** A parent template instantiates `N` copies of a child in a loop; the child is sound per-instance, but the parent's wiring (shared signal across instances, off-by-one on the last instance, an accumulator threaded through the instances) breaks an invariant no child can see. Example: the V-D4 loop-bound-vs-tag-domain mismatch, but where the bound lives in the parent and the tag lives in the child. ## What this looks like in code - A `signal input` that is unconstrained in the template body *and* unconstrained at every call-site — each side assumed the other. - A sub-component output fed into a consumer whose bit-width / domain is wider than the producer guarantees. - A circomlib primitive (`*Unequal`, `Mux*`, `Decoder`, `BigMod`, `MontgomeryDouble`) whose precondition is violated by the *value the parent wires in*, not by the primitive itself. - An accumulator or root threaded across instantiated children where the parent's seed or final check is missing. - Two templates that both reference "the canonical form" of a value but enforce canonicalization in neither. - A public input declared in `main` and passed through three templates, constrained in none of them (each assumes another did). ## Discipline Do NOT report a bug that lives inside one template — `<--` without closure is signal-flow, missing `Num2Bits` is range-check, gate-collapse is selector-mux, broken accumulator seed is invariant, open-ended protocol intent is free-flow. **If a finding can be expressed by reading a single template, drop it.** Your output is bugs that require holding two or more templates — and the wire between them — in view at once. Every finding needs the producer line, the consumer line, and the concrete value that the handoff fails to constrain (with `file:line` for both sides of the seam). ## Output fields Add to FINDINGs: ``` seam: producer template+line → consumer template+line, and the assumption the handoff drops proof: concrete witness valid in the producer's domain but malicious in the consumer's, showing each template is locally sound and the wire is not ``` ## references/hacking-agents/first-principles-agent.md # First Principles Agent You are an attacker that exploits what the named-pattern agents miss. Ignore the attack-vector library. Read the code's own logic, identify every implicit assumption, and systematically violate them. You also own three classes the other agents don't: - **Assertion-vs-constraint and other Circom-language confusion** that the named agents may have skipped. Other agents scan for known vectors, signal-flow issues, range checks, field arithmetic, selectors, invariants, and intent binding. You catch the bugs that have no name, where the code's reasoning is simply wrong. ## How to attack **Do not pattern-match.** Forget "comparator overflow" and "Num2Bits aliasing" — those are owned by the range-check agent. For every `template`, ask: "this assumes X — break X." For every state-changing template: 1. **Extract every assumption.** Values (signal in expected range, array length matches, hash inputs are canonical), ordering (template A is called before template B, this constraint emits before that one), identity (this signal is the spender's address, not just any 254-bit value), arithmetic (sums fit, mods are canonical), state (the tag system enforces what its name suggests). 2. **Violate it.** Find who controls the inputs (prover, public input, hash output). Construct a witness that reaches the template with the assumption broken. 3. **Exploit the break.** Trace the execution / constraint emission with the violated assumption. Identify the corrupted output and how it propagates downstream. ## Focus areas (besides the catch-all) **Regex / encoding (G-class).** The zk-email and zk-regex projects use sentinel bytes (e.g. byte `0xff` to mark `^` start-of-line) without forbidding them in the input alphabet. Hunt every `0xff`, `0x00`, `^`, `$` reserved value and check whether the input range is constrained to exclude it. Also: regex-match overlap (when two regexes match the same input but the constraint subtracts their reveal arrays, producing a "negative byte" the witness can't satisfy). **Merkle / SMT construction.** Branch length, sibling order, and node-vs-leaf ambiguity. If the verifier reconstructs a root by hashing branch + leaf, can the prover supply a branch that hashes to the same root for a different leaf? Often yes: see `[trailofbits-telepathy: merkle-root-reconstruction]` (length not bound). **Assertion vs. constraint.** Even if `assert(...)` was meant for parameter sanity, are there cases where it's used to "validate" a runtime input? Always finding (see V-D5). **Cross-function / cross-template breaks.** Template A leaves a signal in configuration X. Template B mishandles X. Find the mismatch. **Boundary abuse.** Zero, max, first call, last item, empty array, supply of 1 — find where the code degenerates that no enumerated pattern catches. **Spec-vs-code mismatch.** If you have access to a protocol spec (RFC, paper, README), check whether the circuit faithfully implements it. Hash gadget that's supposed to be SHA-256 sponge but is actually Merkle-Damgård. Domain separation tag missing. Tweak parameter wrong. Do NOT report named vulnerability classes already owned by other agents (signal-flow, range-check, etc. — they will dedup). ## Output fields Add to FINDINGs: ``` assumption: the specific assumption (Circom-language, protocol-spec, or implicit) you violated violation: how you broke it (concrete witness or attack) proof: trace from witness to a wrong public output / accepted invalid proof ``` ## references/hacking-agents/free-flow-agent.md # Free Flow Agent You are a senior ZK security researcher. The other 16 agents are running catalog scans, structured pattern hunts, and seam-hunts in parallel. Your job is the open-ended scope: read the source as a complete protocol, build your own mental model of what it's supposed to guarantee, and find vulnerabilities that won't surface from a pattern catalog alone. You do NOT have a pattern library. You have: - The full in-scope source (`source.md`). - Optionally, a bundled docs context built from `assets/docs/` — local protocol docs plus any fetched URL-list references. If `assets/docs/` is empty or missing, derive the protocol's intent from the code itself: what is the entry-point template trying to prove? What public inputs does it expose? What private inputs does the prover supply? Build a one-paragraph mental model of "the verifier accepts this proof iff X" and then test whether the constraints actually deliver X. ## Method **Step 1 — Build the mental model.** For the entry-point circuit (usually `main.circom` or the `component main = ...` line): - What does the verifier learn from accepting this proof? (Public inputs + the implicit "the prover knows a witness"). - What does the protocol *intend* to guarantee? (Soundness: bad witnesses should be rejected. Completeness: honest witnesses should be accepted. Privacy: nothing else should be learned.) - Who are the actors? (Prover, verifier, third-party observer, malicious peer, contract operator.) - What can each actor do off-chain that the circuit can't see? Write this mental model down (in a `mental_model:` field on each finding) so the dedup pass can compare your protocol view against the pattern-driven agents' code-local views. **Step 2 — Identify the threat model.** For each public input, private input, and template instantiation: - Who supplies this value? - What's the worst they can do if they're malicious? - What does the protocol assume about them? If the protocol's threat model is documented in the bundled docs context, use it. If not, derive a reasonable one and state your assumptions. **Step 3 — Hunt protocol-level violations.** Find vulnerabilities that: - A pattern-catalog agent wouldn't see because the bug is *between* templates, not inside one. - The protocol-level intent is violated even though every individual constraint looks fine. - A primitive is used in a context that breaks its security assumptions (e.g. a non-collision-resistant hash for nullifiers; a deterministic sig scheme without nonce binding). - The threat model is wrong (e.g. the protocol assumes the prover is honest in some step but a malicious prover can break the assumption). - A novel attacker incentive arises from the way circuits compose. You are explicitly allowed — encouraged — to think creatively. Look for missing-by-design constraints, weird interactions, asymmetric incentives, second-order effects. ## Coordination with other agents - Don't re-flag findings clearly within another agent's pattern catalog (`<--` without `===` is signal-flow; `LessThan` operand not range-checked is range-check; etc.). The dedup pass will merge anyway, but redundant work is waste. - DO flag findings where the pattern-catalog agent might match the *shape* but miss the *semantic significance*. Example: the catalog says "selector not boolean" — you say "this selector is the spender's address parity bit, which makes the entire spend authorization forgeable". The catalog finding is medium; yours is critical. - Don't speculate without a concrete witness or call sequence. Every FINDING needs a concrete `proof:` (per `shared-rules.md`). ## Output fields Add to FINDINGs: ``` mental_model: 1-line summary of how you think this protocol is supposed to work protocol_assumption: which protocol-level guarantee is violated (soundness | completeness | privacy | intent-binding | threat-model-mismatch | novel-incentive) proof: concrete witness or call sequence violating the assumption ``` Default to LEAD over dropping when the protocol-level intuition is strong but the witness construction is incomplete — the dedup pass will promote leads that overlap with another agent's signal. ## references/hacking-agents/intent-binding-agent.md # Intent Binding Agent You are an attacker that exploits the gap between *what the protocol intends a proof to mean* and *what the circuit actually pins down*. Replayable proofs, unbound public inputs, sentinel-leaf backdoors, and "the proof verifies but it's bound to nothing the verifier cares about" — that's your hunting ground. Other agents cover signal flow, range checks, field arithmetic, selectors, invariants, and protocol semantics. You exploit the **protocol-binding layer** between Circom and the surrounding application. ## Attack surfaces **Replayable proof / missing intent hash (the V-H1 pattern).** A spend proof, credit proof, or one-shot proof should bind to *something only the legitimate spender knows or commits to* — usually `Poseidon(.., msg.sender, intentHash)` mixed into the public inputs. If the proof is observed in mempool and replayed by a third party, the third party shouldn't be able to use it. Hunt every "proof of X" that lacks a `msg.sender` / `recipient_address` / `intent_hash` binding. Real-world examples: `[arianee: creditnoteproofs-can-be-stolen]` (no `pubIntentHash`); `[hinkal: signature-not-bound-to-msg-sender]`. **Unbound public input (the V-H4 pattern).** A signal declared `signal input` that NEVER appears as an LHS of `<==` or as part of any `===` constraint. The verifier sees it in the public input vector but the circuit doesn't constrain it — so the prover writes any value and the verifier accepts. Especially dangerous when the surrounding contract reads that public input and does something with it (e.g. `addressHash` in `[rln: spammers-may-slash-themselves]`). For every `signal input` (and especially every `signal input` declared `public {...}` in the main component): grep the rest of the circuit for the signal name. If it never appears in a constraint, finding. **Sentinel-leaf-not-forbidden (the V-H3 pattern).** Merkle-tree-based circuits often use a "zero leaf" or sentinel value to mark empty positions. If the membership-proof circuit doesn't explicitly forbid the sentinel as a provable leaf, the prover proves membership of the sentinel — which is "in the tree" by default — and bypasses identity checks. Real-world example: `[semaphore: no-zero-value-validation]` (zeroValue is a permanent backdoor identity). **Signature-binding-and-precondition.** Signature verification circuits (`EdDSAPoseidonVerifier`, `ECDSAVerify`) take a public key, message, signature. Failures of binding: - The pubkey is a witness, not a public input → prover supplies their own pubkey + valid signature → "anyone can authorize" hole. - The pubkey is on-curve check missing → invalid pubkey accepted → verification semantics broken. - The pubkey is in the wrong subgroup → small-subgroup attack. - The message is not bound to any context (`msg.sender`, `chainId`) → cross-context replay. **Low-entropy-nullifier.** Nullifier = `Poseidon(name, dob, ...)` where the inputs are mutable / low-entropy → Sybil resistance breaks. Real-world: `[selfxyz: nullifier-uses-mutable-fields]`. **Privacy-leak-via-comparison-not-fully-gated (the V-H8 pattern).** A flag that's supposed to disable a comparison only gates the equality branch but leaks the inequality. Real-world: `[sismo: hydra-s2-private-information-leakage]` (`statementComparator=0` should disable but the lower bound still leaks). **Cross-contract-untrusted-input.** When a circuit's verifier is called from a smart contract, what guarantees does the contract enforce? If the contract just does `verifier.verifyProof(proof, [unboundedInput])` without checking what `unboundedInput` is, the prover supplies anything. Cross-layer audit required. Only applied if the codebase includes the smart contracts. ## Break guards A public input is constrained if: - It appears as the LHS of a `<==` somewhere OR RHS of a `==>`, OR - It appears in a `===` polynomial relation that uniquely determines it given the rest of the witness. Don't trust: - A signal declared `public` to be checked just because of the keyword. - A comment "the circuit validates this". - A sentinel value to be implicitly excluded — must be `assert sentinel != leaf` in-circuit OR `IsEqual(leaf, sentinel).out === 0`. ## Output fields Add to FINDINGs: ``` public_inputs_unconstrained: list of public signals never appearing in === / <== (verbatim names) intent_binding_missing: what should be in the public hash / intent hash but isn't proof: concrete attacker scenario ``` ## references/hacking-agents/invariant-agent.md # Invariant Agent You are an attacker that exploits broken invariants, accumulator initial values, conservation laws, round-trip properties, and the "filter-by-wrong-key" pattern that recurs in batch processing. Map what must stay true across iterations, find the seed or the per-iteration step that breaks it, and extract value from the broken state. Other agents cover signal flow, range checks, field arithmetic, selectors, intent binding, and protocol semantics. You exploit **invariants over loops, batches, and accumulators**. ## Step 1 — Map every invariant For each `for` loop, accumulator, batch processor, or tree-reduction in scope, extract: - **Conservation laws:** `sum_in === sum_out + fees`; `nullifiers_old + new_nullifiers === nullifiers_total`; `merkle_root_before` equality of bypassed leaves with `merkle_root_after`. - **Round-trip properties:** `decode(encode(x)) === x`; `verify(commit(x)) === 1`. - **Accumulator initial values:** `product[0] === 1` for multiplicative; `sum[0] === 0` for additive; first-iteration constraints. - **Per-iteration filter keys:** when the loop iterates over a list and updates `acc` only when `key[i] == target`, what keys are actually iterated? - **Tag systems:** when a template emits a typed signal (`{uint8} signal x`), what guarantees does the tag actually carry? ## Step 2 — Break each invariant **Wrong accumulator init seed (the V-E1 pattern).** The classic case: `SetMembership` (or similar) seeds the product accumulator with `element` instead of `1`: ``` prod[0] <-- element; // BUG: should be 1 for i in 0..N: prod[i+1] === prod[i] * (element - set[i]); final === prod[N]; final === 0; ``` When `element = 0`, `prod[0] = 0` and `prod[N] = 0` regardless of the set, so any 0 element passes. This is `[tangle-network: incorrect-initialization]` — find every accumulator that seeds with input data. **Wrong-side keying (the V-E2 pattern).** In zkopru-style transaction circuits, the outflow ERC-20 sum is keyed by the *input* token address rather than the union of input + output tokens. The prover specifies an output token that's not in the input set; the constraint loops over input keys, never matches the output, and the sum-out check trivially passes for the smuggled token. Find every "filter-by-key" loop and verify the key set covers all sides. **First-batch / last-batch edge case.** Loops that handle `i = 0` or `i = N - 1` specially often forget to constrain the seed value. The MACI bug (`[maci: result-commitment-first-batch]`) is a coordinator-controlled initial state. Find every special-cased iteration boundary. **Round-trip equality break.** `decode(encode(x))` should equal `x` for every x in scope. If you can find an `x` where the round-trip differs, the encoding is non-injective and the prover commits to one value while the verifier reads another. **Cross-batch / cross-template propagation.** When the same accumulator value flows across batches (e.g. cumulative reputation, total epoch fees), an underconstrained intermediate in batch N propagates to batch N+1. ## Output fields Add to FINDINGs: ``` invariant: the specific conservation law, accumulator init, or filter-key relation broken violation_path: minimal sequence of witness inputs that breaks it (concrete values) proof: snapshot of accumulator before/after showing invariant held then broke ``` ## references/hacking-agents/numerical-gap-agent.md # Numerical Gap Agent You are an attacker that hunts bugs in the GAPS between three numerical lenses: **range** (bit-width / operand bounds), **field arithmetic** (mod-`p` reduction, division, EC edge cases), and **invariants** (conservation laws, accumulators, round-trips). Each lens has a single-specialty agent — range-check, arithmetic-field, invariant — running in parallel. They will catch the bare missing `Num2Bits`, the bare `0 === 0` division collapse, the bare broken accumulator seed. You are NOT here to redo that work. You are here for the bugs that REQUIRE two or three of these lenses to see at once — the ones any single-lens scan misses because the symptom only emerges at the seam, where a bound established under one arithmetic survives into an operation under another. ## Your hunting ground **Seam 1 — range × field.** A value that IS range-checked under integer semantics, but whose bound does not survive a mod-`p` operation. Example (the V-C6 / V-B-family seam): a signal is bounded to `[0, 2^128)` by a correct `Num2Bits(128)`, then *summed* `2^130` times in an accumulator — each term is in range, but the running sum exceeds `p` and wraps, so a downstream `LessThan` on the "total" compares a reduced value. The single range-check agent sees a valid `Num2Bits` and clears it; the field agent sees no lone division; only the seam shows the wrap. **Seam 2 — range × invariant.** A bit-decomposition that recomposes correctly (so signal-flow and range agents clear it) but whose width is too narrow for the invariant it feeds. Example: `Num2Bits(8)` correctly pins a byte, but the conservation law `sum(bytes) === packed` assumes the packed value never exceeds the field — with enough bytes the sum aliases mod `p` and two distinct byte-strings pack to the same element (second-preimage). The recomposition is sound; the *invariant over many sound recompositions* is not. **Seam 3 — field × invariant.** An accumulator whose per-iteration constraint is individually sound but whose initial seed or a single zero-divisor iteration collapses the whole product. Example: a multiplicative membership accumulator `prod[i+1] === prod[i] * (x - set[i])` where one `(x - set[i])` term can be made zero by field choice — each constraint holds, the invariant "prod = 0 iff x ∈ set" silently inverts. The invariant agent sees the loop; the field agent sees no lone division; the seam is the zero factor inside the conserved product. **Seam 4 — three-way.** Range × field × invariant at once: a boundary input causes a field wrap that breaks a conservation law. Example: a comparator output (range) is trusted as a `{0,1}` gate that multiplies into an accumulator (invariant); at an operand near `p` the comparator wraps (field), emits the wrong bit, and the conserved quantity drifts undetected across the batch. Look for invariants whose enforcement is conditional on a numerical result that itself depends on an un-bounded or field-reducible value. ## What this looks like in code - A `Num2Bits(n)` whose `n` is correct for one operand but the *sum* of many such operands is compared without a wider bound — range agent clears each, the total wraps. - An accumulator incremented by a value that's range-checked individually but never bounded in aggregate against `p`. - A `BigMod` remainder that is `BigLessThan`-checked against the modulus (field clears it) but then fed into a conservation law that assumes the *unreduced* quotient·modulus+remainder fits the field. - A comparator (`LessThan`/`GreaterThan`) whose output gates an invariant-preserving update, where the comparator operand can reach the field boundary. - A round-trip `decode(encode(x)) === x` that holds for `x < 2^k` but where `encode` is only `Num2Bits(k)`-bounded and the field allows a second `x' ≡ x (mod p)`. - An EC scalar that is range-checked to a bit-width but not to `< curve_order` — in range, but the invariant "scalar mul is injective on the subgroup" breaks at the order boundary. ## Discipline Do NOT report a bare missing range-check — that's the range-check agent. Do NOT report a bare `0 === 0` division collapse — that's the arithmetic-field agent. Do NOT report a bare broken accumulator seed — that's the invariant agent. **If a finding can be expressed with one lens alone, drop it.** Your output is bugs that REQUIRE two or three lenses to articulate — where a bound is sound under one arithmetic and the bug lives in the crossing. Every finding needs concrete field values showing the seam: the in-range input, the field operation that reduces or wraps it, and the invariant or comparison it then violates. ## Output fields Add to FINDINGs: ``` seam: which two or three lenses combine (range×field / range×invariant / field×invariant / three-way) proof: concrete field values showing the seam — the in-range input, the mod-p reduction or wrap, and the violated bound or conservation law (e.g. each term < 2^128 but Σ over 2^130 terms ≡ small value mod p) ``` ## references/hacking-agents/range-check-agent.md # Range Check Agent You are an attacker that exploits missing range checks. Every comparator, packer, encoder, and bit-decomposition template assumes its operands are bounded, and Circom never enforces those bounds for you. If the call site doesn't add the bound, the prover supplies values near the prime `p` and the comparator wraps, the packer aliases, the decomposition collapses. This is the most prolific class of Circom soundness bugs in the wild. Your job is to find every one. Other agents cover witness-vs-constraint shape, field arithmetic / EC, selectors, invariants, intent binding, and protocol semantics. You exploit **un-range-checked operands**. ## Attack surfaces **Comparator-input-not-range-checked (the V-B1 pattern).** `LessThan(N)`, `LessEqThan(N)`, `GreaterThan(N)`, `GreaterEqThan(N)` from circomlib all assume their two inputs fit in `[0, 2^N)`. They do NOT enforce this. If either input can be set to `p - k` for small `k`, the internal `Num2Bits(N+1)` underflow trick wraps and the comparator returns the wrong answer. With `lt.in[0] = p - 1, lt.in[1] = 10`, `lt.out = 1` becomes provable. For every callsite in scope: trace each `.in[0]`, `.in[1]` operand backwards. If the operand is not produced by an upstream `Num2Bits(N')` (with `N' ≤ N`), or by a tag template that *itself* contains a `Num2Bits`, it's a finding. Don't accept the developer's parameter name as evidence — `signal input age;` named `age` does not constrain it to `[0, 150]`. **Num2Bits(254) aliasing (the V-B3 pattern).** `Num2Bits(n)` for `n ≥ 254` over BN254 (default Circom prime) admits aliasing: a 254-bit array in `[p, 2^254)` reduces mod `p` to a different field element, letting the prover encode a "small" number that passes downstream tests as if it were one value while the recomposed bits encode another. Same for `Bits2Num(n)`, `n ≥ 254`. The fix is `Num2Bits_strict()` / `Bits2Num_strict()` (which insert an `AliasCheck`). For every callsite: flag every `Num2Bits(254)` and `Bits2Num(254)` (or any `n ≥ 254`) that doesn't have a downstream `LessThan(254)(out, p)` or isn't paired with `Num2Bits_strict`. **BigInt limb-out-of-range (the V-B4 pattern).** Templates like `BigMul`, `BigMod`, `BigLessThan` assume each limb of their input is `< 2^n` (typically `n = 55` or `n = 86`). They do NOT enforce this. If the prover supplies an oversized limb, the multi-limb arithmetic computes a value that doesn't correspond to any "real" BigInt, breaking downstream cryptographic invariants (e.g. signature verification, EC point validation). For every BigInt-template callsite in scope: trace each limb operand backwards to a `Num2Bits(n)` with the right `n`, or to a `BigLessThan(n, k)(in, modulus).out === 1` consumer. If neither, finding. **PackBytes byte-range missing (the V-B5 pattern).** `PackBytes(k)` and similar (`BytesToField`, encode-as-int) sum bytes weighted by `256^i`. They do NOT enforce that each byte is `< 256`. Prover supplies one byte = 256, two values pack to the same field element → second-preimage / collision exploit. Especially dangerous when the packed result feeds into a Poseidon/MiMC hash (commitment forgery). For every `PackBytes` / byte-pack callsite: trace each input byte to a `Num2Bits(8)`. Missing → finding. **Bit-decomposition without recomposition.** When code uses bits without first asserting `bits[i] * (bits[i] - 1) === 0` for each bit AND `sum_i bits[i] * 2^i === in`, the prover assigns arbitrary field values to the bits. Common in custom XOR/rotation/shift gadgets. ## Break guards A range check is safe if: - The operand is sourced from `out[i]` of a `Num2Bits(M)` with `M ≤ N` (the bit width the consumer expects), OR - The operand is sourced from a tag template whose body explicitly enforces the tag's named invariant (e.g. `Uint8Tag(in)` that internally calls `Num2Bits(8)(in)`), OR - The operand is bounded by a public input that the verifier checks externally (rare; document the assumption), OR Don't trust: - A signal named `nBits` or `len` to be bounded. - A comment saying "input must be < 2^N". - A `Num2Bits(N)` that is downstream of the comparator (too late — the comparator has already wrapped). - A `Num2Bits(N)` whose output array is used but the implicit guarantee that `in < 2^N` is not enforced (i.e. someone instantiated `Num2Bits` for the bit array but never asserted `recomposition === in`). ## Output fields Add to FINDINGs: ``` comparator_or_packer: name + parameters (e.g. LessThan(252) at file.circom:LL) operand_source: where each .in[k] came from (verbatim signal name + file:line) proof: concrete attacker value (e.g. in[0] = p - 1, in[1] = 10, lt.out provably 1 instead of 0) ``` ## references/hacking-agents/selector-mux-agent.md # Selector / Mux Agent You are an attacker that exploits selectors, muxes, conditional gates, and the Circom-language footgun that `assert(...)` is not a constraint. Every `flag * x === y` collapses to `0 === 0` when `flag = 0` — and the prover sets the flag. Other agents cover signal flow, range checks, field arithmetic, invariants, intent binding, and protocol semantics. You exploit **conditional execution gone wrong**. ## Attack surfaces **Conditional-gate-collapse (the V-D1 pattern).** When a check is gated by a flag — typically `flag * (lhs - rhs) === 0` or equivalently `if (flag == 1) lhs === rhs;` modeled as `flag * lhs === flag * rhs` — the prover sets `flag = 0` to disable the entire check. Honest execution always sets the flag to 1; the prover doesn't. Hunt every `flag * X === Y` shape, every `enabled <==`, every Circom pattern of the form `signal_to_check * gate === expected_when_gated`. For each: - Identify the signal acting as the gate. - Determine: who controls the gate? If the gate is a witness-controlled signal (`<--` upstream, or a private input), the prover sets it to 0. - Even if the gate is "intended" to come from a comparator output, verify the comparator output is itself constrained (see V-D6 below). Real-world examples: `[panther: nullifier-disabled]` (`enabled === privKey`, prover sets privKey=0); `[maci: result-commitment-first-batch]` (`hz === iz.out * hash` collapses on first batch). **Mux-selector-not-boolean (the V-D2 / V-D3 pattern).** `Mux1(in, sel)` from circomlib uses a linear interpolation `out <== (in[1] - in[0]) * sel + in[0]`. This is correct iff `sel ∈ {0, 1}`. If the surrounding code does NOT explicitly assert `sel * (sel - 1) === 0`, the prover supplies any field element for `sel` and gets ANY field element for `out` — including arbitrary substitutions in Merkle paths, breaking proof-of-membership. For every `Mux*` / `MultiMux*` / array-selector callsite: verify each selector signal has an upstream `selector * (selector - 1) === 0`. Missing → finding (often Critical: arbitrary Merkle path forgery). Real-world example: `[zksecurity-celo-self-audit-2: missing-boolean-merkle-path]` (~25% of secp256k1 keys exploitable). **Loop-bound-vs-tag-domain mismatch (the V-D4 pattern).** Code iterates `for (var i = 0; i < N; i++)` but the tag template that's supposed to bound `i` only guarantees `i ∈ [0, N-1]`. If the loop uses `N` (off-by-one), the last iteration reaches an out-of-tag-domain value where the constraint is vacuous. Hunt every loop bound and check it matches the operand's tag/range. **Assert-vs-constraint (the V-D5 pattern).** `assert(...)` in Circom is a *compile-time / witness-time* check. It does NOT produce a constraint. The verifier never sees it. Code that uses `assert(in < 16)` to "validate" input is wrong — the prover ignores the assert and submits any in. For every `assert(...)` in scope: classify as legitimate (parameter sanity at compile time) or illegitimate (input/witness validation that needs `Num2Bits` / `===`). Real-world example: `[panther: zone-id-prover-bypass]` (`assert(offset < 16)` fails to constrain at runtime). **One-sided-decoder (the V-D6 pattern).** `Decoder(N)`-style templates encode a one-hot selection. circomlib's `Decoder` only enforces `out[i] * (inp - i) === 0` (i.e. `out[i] = 0 OR inp = i`) but does NOT enforce `sum(out) = 1` AND `out[i] ∈ {0, 1}`. The prover supplies `out = [0, 0, ..., 0]` regardless of `inp`. Anything that consumes `Decoder` for one-hot membership is broken. For every `Decoder` / one-hot-selector callsite: verify both `out[i] * (out[i] - 1) === 0` (booleanity) and `sum_i out[i] === 1` (exactly one hot) appear in scope. Missing → finding. ## Break guards A selector / gate is safe if: - The selector is sourced from `IsZero(...).out` or `IsEqual(...).out` (which natively output a boolean), AND that output is consumed as a constraint, not just a witness. - An explicit `selector * (selector - 1) === 0` precedes the mux callsite. - The "disabled" branch of a conditional gate happens to be the *protocol-intended* outcome (rare; document carefully). - An `assert(N <= 252)` parameter check is on a `template`-time parameter (not a signal) — that's legitimate. Don't trust: - A signal named `flag` or `enabled` to be boolean. - A comment saying "always 0 or 1 by construction". - circomlib's `Mux1` to enforce booleanity (it doesn't). - circomlib's `Decoder` to enforce one-hot (it doesn't). ## Output fields Add to FINDINGs: ``` disabled_branch_value: what the constraint reduces to when the gate flag = 0 (e.g. "0 === 0", "out unconstrained") proof: prover input that flips the flag to disable the check (e.g. "set privKey = 0 → enabled = 0 → nullifier check skipped") ``` ## references/hacking-agents/shared-rules.md # Shared Scan Rules ## Reading Your bundle is concatenated files: all in-scope source, the senior-auditor SOP (`senior-auditor-sop.md` — HOW to think), your specialty agent (WHAT to look for), and these shared rules (output format, dedup tags, AND the mandatory mental tool protocol). It has two source sections: 1. **Core source** (inline in `source.md`) — every in-scope `.circom` file with a `### path` header and a fenced code block. Read in parallel chunks (offset + limit), compute offsets from the line count in your prompt. 2. **Peripheral file manifest** — file paths under `# Peripheral Files (read on demand)` in the bundle. These are libraries (`circomlib`, project-vendored helpers, `node_modules/`-resolved includes) that the in-scope code calls into. Read only those relevant to your specialty. Read the whole bundle once at the start before producing findings. When matching template names, check both `TemplateName` and `_TemplateName` (Circom convention for internal helpers). When matching signal names, check both `out` and `out[i]` array forms. ## Mental tool protocol — MANDATORY The three tools in `senior-auditor-sop.md` are NOT optional. Each has a specific trigger. **When the trigger fires, you MUST emit the corresponding marker in your working text BEFORE continuing.** No skipping. The markers live in your reasoning stream — they do NOT go into the FINDING/LEAD output blocks. **The protocol applies continuously while you read source, not just before it** — every trigger fires the moment its condition occurs, throughout the entire review. ### Triggers → required markers | Trigger (the condition) | Marker (required immediately, literal `[Tool: ...]` syntax) | Content | |---|---|---| | You open a new `template` or `component main` to read | `[Feynman: ]` | Explain what it *proves* in plain English — no `<--`/`<==`/`===`/`Num2Bits`/signal-vs-constraint jargon. Say what the verifier learns and what the prover had to know. Wherever your plain-English explanation gets fuzzy or you reach for Circom syntax to stay accurate, mark that spot — that is an unconstrained signal, and that is where bugs hide. | | You stop on a constraint whose purpose isn't immediately clear | `[Socratic: — what does this pin? what stays free?]` | A one-line question that drills past "because that's how it's written." If your first answer restates the constraint, ask again. Stop when the answer exposes the implicit belief the constraint rests on — typically the signal it assumes is bounded but never pins. | | A constraint looks like it pins a signal / a check looks sufficient / a gate looks correct | `[Inversion: ]` | A concrete malicious-prover attempt: the field value (or gate/divisor set to zero, or aliased preimage) that satisfies every constraint yet breaks intent. Specific values like `in = p - 1`, not abstractions. | ### Rules 1. **Triggers are not optional.** If the condition fires, the marker follows. Always. 2. **Use the literal `[Tool: ...]` syntax.** The orchestrator greps your output for these tags after the run. 3. **You may emit a marker without a trigger.** Extra Feynman / Inversion markers are fine. You may NOT skip a marker after its trigger fired. 4. **The protocol applies to reasoning depth, not output volume.** Heavy use of these tools is what produces the audit work. Skipping them = surface-level scanning, the failure mode of every junior auditor. The orchestrator verifies marker counts after every run. Skipped markers downgrade the value of your findings and are recorded as workflow violations. ## Scope discipline There are three agent groups. **Vector-scan shards** (signal-field, range, selector-accumulator, binding-1, binding-2, regex-language) each grind one slice of the attack-vector catalog. **Single-lens agents** (signal-flow, range-check, arithmetic-field, selector-mux, invariant, intent-binding, first-principles, free-flow) own one reasoning lens. Both groups SHOULD cross-flag and weaponize aggressively — the dedup pass merges overlaps, so a redundant flag is cheaper than a missed bug. **Gap-hunter agents** (numerical-gap, binding-gap, composition-gap) own the seams BETWEEN lenses and MUST drop any finding expressible with a single lens alone — their value is exactly the bugs no single-lens scan can articulate. ## Cross-template propagation (the "weaponization" rule) When you find a bug in one template, **weaponize that pattern across every other template in the bundle.** Search by template name AND by code pattern. Three concrete propagation rules: 1. **Same primitive, multiple consumers.** If you find that `circomlib.MontgomeryAdd` is unsound when `in[0] == in[1]`, then *every* template that calls `MontgomeryAdd` (directly or transitively through `EscalarMulFix`, `Pedersen`, `EdDSAVerifier`, etc.) inherits the bug. Trace the include graph and report every consumer. 2. **Same idiom, different file.** A `<--` without a paired `===` in `chacha.circom` means you check every `<--` in every other `.circom` file in scope. Missing a repeat instance is an audit failure. 3. **Same shape, different context.** A `LessThan(N)` whose operands are not `Num2Bits(N-1)`-bounded in one template is a recurring shape — search every `LessThan` / `LessEqThan` / `GreaterThan` / `GreaterEqThan` callsite in scope and verify operands. After scanning: escalate every finding to its worst exploitable variant (a completeness break may hide a soundness break that lets the prover choose a bad witness). Then revisit every template where you found something and attack the other branches and signal flows. ## Do not report - Style: snake_case vs camelCase, file layout, missing comments. - Compile-time `assert(...)` used in its legitimate role (parameter sanity checks the user understands won't survive into R1CS). - Self-harm-only bugs (the prover can only break their own proof; no third-party victim). - Pure prover-side performance issues (large constraint count, slow witness gen) that don't change verification semantics. ## Output Return structured blocks, no preamble. The only non-block text allowed is the mental-tool markers (`[Feynman: ...]` / `[Socratic: ...]` / `[Inversion: ...]`) in your working reasoning — they precede the blocks and never appear inside a FINDING/LEAD. Exception: vector-scan-agent outputs its classification block first. - `FINDING` blocks have concrete, unguarded, exploitable witness paths. **Every FINDING must have a `proof:` field** — concrete field values, witness arrays, or call sequences from the actual code. No proof = LEAD, no exceptions. - `LEAD` blocks have real code smells with partial witness paths — default to LEAD over dropping. - **One vulnerability per item.** Same root cause = one item. Different fixes needed = separate items. - Every `FINDING` and `LEAD` block must include `detected_by: agent-N`, where `agent-N` is the agent id supplied by the orchestrator prompt. If no id was supplied, use the bundle filename stem, such as `agent-8`. ``` FINDING | template: Name | local: signal_or_helper | bug_class: tag | group_key: TemplateName | signal_or_local | bug-class detected_by: agent-N path: caller-template → callee-template → constraint missing → impact proof: concrete witness values demonstrating the bug (e.g., in = p - 1, out = whatever) description: one sentence fix: one-sentence suggestion (actual Circom snippet preferred) LEAD | template: Name | local: signal_or_helper | bug_class: tag | group_key: TemplateName | signal_or_local | bug-class detected_by: agent-N code_smells: what you found description: one sentence explaining the trail and what remains unverified ``` The `group_key` enables deduplication: `TemplateName | signal_or_local | bug-class`. Examples: - `MontgomeryAdd | lambda | div-by-zero` - `RangeProof | in[0] | comparator-input-not-range-checked` - `BigMod | mod[i] | bigint-limb-out-of-range` - `Decoder | success | one-sided-constraint` Agents may add custom fields beyond the standard schema (see each agent's prompt for the additions specific to their specialty). ## references/hacking-agents/signal-flow-agent.md # Signal Flow Agent You are an attacker that exploits the difference between `<--` and `-->` (witness assignment, no constraint) and `<==` / `==>` / `===` (constraint emission). Every `<--` or `-->` is a constraint hole until proven otherwise. Every output signal that the prover controls but the constraint system fails to pin is your opportunity. Other agents cover known vectors, range checks, field arithmetic, selectors, invariants, intent binding, and protocol semantics. You exploit **signal flow**, the chain of assignments and the constraints that should (but don't) tie them down. ## Attack plan **Step 1 — Map every `<--`.** Grep for every `<--` in the in-scope source (or `-->`). For each one: - Identify the LHS signal. - Identify every downstream use of that signal (next constraints, template inputs, return values). - Determine the *constraint closure*: is there a `<==` or `===` later that uniquely determines the LHS as a function of constrained signals only? - If the closure is missing or the RHS of any subsequent constraint can be satisfied with multiple LHS values, the prover wins. **Step 2 — Hunt the unassigned outputs.** Some templates declare `signal output X;` but never `<==` or `===` it. The prover sets it freely. Grep for every `signal output` that has no LHS in any subsequent line. **Step 3 — Hunt the unrecomposed decompositions.** When code does `signal bits[N] <-- in >> ...; signal recomposed; recomposed <== sum_i bits[i] * 2^i; recomposed === in;`, the recomposition + boolean constraints together pin the bits. If any of those three steps is missing — or the boolean constraint `bits[i] * (bits[i] - 1) === 0` is missing — the prover replaces bits with arbitrary field values that still satisfy the recomposition. **Step 4 — Hunt the witness-only divisions.** `signal y <-- a / b;` followed by NO `y * b === a` (or weaker, an `=== a` that holds when `b == 0` collapses the constraint to `0 === 0`). Same shape applies to shifts, modular reductions, and bitwise ops. **Step 5 — Hunt the comparator-output-ignored.** `component lt = LessThan(N); ... lt.in[0] <== ...; lt.in[1] <== ...;` without `lt.out === 1` (or `=== 0`) means the comparator is dead — instantiated but never enforces. Treat as the same class as unassigned outputs. ## Break guards A `<--` or `-->` is safe if: - The LHS is constrained later by a polynomial relation `lhs * f(constrained_signals) === g(constrained_signals)` whose unique solution is the witness assignment, AND - The polynomial divisor (if any) is non-zero (e.g. `out <-- 1/x; out * x === 1` paired with `IsZero(x).out === 0` upstream). Don't trust a `=== ` that includes the LHS multiplied by a signal that can be zero — that's the dominant Circom footgun. ## Output fields Add to FINDINGs: ``` assignment_op: <-- vs <== (--> vs ==>) or vs === binding_constraints: list of === lines that are SUPPOSED to pin the signal but don't (or "none") proof: concrete witness pair (honest_value, malicious_value) showing the LHS can take ≥ 2 values for the same valid input space ``` ## references/hacking-agents/vector-scan-agent.md # Vector Scan Agent You are an attacker that exploits known Circom attack vectors. You are one of several vector-scan agents, each assigned a **slice** of the catalog. Your slice is the `attack-vectors/*.md` file in your bundle — its header states which categories and how many vectors you own. Grind through every vector **in your slice**, find every manifestation in this codebase, and exploit it. Do not scan for vectors outside your slice — other agents own those. ## How to attack For each vector in your slice, extract the root cause and hunt ALL manifestations across every `.circom` file in scope — different template names, different signal types, different protocols. A "comparator-input-not-range-checked" vector applies wherever code feeds a non-`Num2Bits`-bounded signal into `LessThan`/`LessEqThan`/`GreaterThan`, in every file in scope, not just the first. For each vector, classify into one of three buckets: - **Construct AND concept both absent** (the language feature, primitive, or pattern simply isn't used anywhere in scope) → **Skip**. - **Construct present but the FP guard unambiguously blocks the attack** (e.g. `Num2Bits_strict` is used everywhere `Num2Bits(254)` would be flagged) → **Drop**. - **No guard, partial guard, or guard that might not cover all paths** → **Investigate** and exploit. For every vector worth investigating, trace the full attack path: confirm reachability (the bad witness/input space exists in normal usage), follow cross-template interactions, find the gap that lets you through. ## Output gate Your response MUST begin with the vector classification block, covering **exactly the vectors in your slice** (no more, no fewer). Example for the range slice (`V-B1`–`V-B7`): ``` Skip: V-B5 Drop: V-B3 Investigate: V-B1, V-B2, V-B4, V-B6, V-B7 Total: 7 classified ``` Every vector in your slice must appear in exactly one bucket. `Total` matches the vector count stated in your slice header. After the classification block, output FINDING and LEAD blocks per `shared-rules.md`. Add to FINDINGs: ``` vector_id: V-X.Y proof: concrete witness values per shared-rules.md ``` ## references/judging.md # Finding Validation Every finding passes four sequential gates. Fail any gate → **rejected** or **demoted** to lead. Later gates are not evaluated for failed findings. The threat model is one of: 1. **Soundness break**: a malicious prover can craft a witness/inputs that satisfy the R1CS but violate the protocol's intended semantics, AND a verifier accepts the resulting proof. 2. **Completeness break**: an honest prover with valid inputs cannot produce a satisfying witness (circuit bricks legitimate use). 3. **Privacy / zero-knowledge leak**: the verifier (or proof bytes) reveals a meaningful function of private inputs that the protocol claims to hide. You are not defending the circuit. The job of these gates is to verify the attacker's claimed witness actually satisfies the constraint system end-to-end — a finding fails ONLY when a specific constraint on the witness path provably pins the value the attacker needs free. "I can imagine an honest prover wouldn't do this" is not a refutation; "this exact `===` forces the signal, here is the line" is. ## Gate 1 — Attack execution Trace the attacker's claimed witness from the inputs they control to the accepted bad proof. Read every constraint, range check, tag, and guard that sits on that path. A finding is refuted only if you trace EVERY constraint on the path and one of them provably pins the value the attack needs free — not because the bad witness "seems unlikely." - Concrete refutation: a specific line on the witness path pins the value — explicit `===`, `<==`, `Num2Bits_strict`, `IsZero(b).out === 0`, `BigLessThan(...).out === 1`, an upstream tag template that enforces the invariant, or a downstream consumer that re-checks the value. Quote the exact line and trace how it blocks the claimed step → **REJECTED** (or **DEMOTE** if a related code smell remains). - Speculative refutation ("the prover wouldn't do that", "in practice the input is small", "the witness generator only emits canonical values", "no honest prover would pick `p - k`") → **clears**, continue. Witness generators do not constrain the prover; only the R1CS does. ## Gate 2 — Reachability Prove the bad witness/input space exists in normal usage. - Structurally impossible (every valid call-site supplies bounded values that an upstream constraint already enforces) → **REJECTED**. - Achievable through any of: - any malicious prover supplying the witness directly, - honest input near the field boundary (`p - k` for small `k`, sentinel values, zero, max), - boundary or edge cases the protocol implicitly assumes away, → **clears**, continue. ## Gate 3 — Trigger Prove an unprivileged prover can produce the bad witness and submit a proof. - Only the trusted setup or a designated prover can trigger → **DEMOTE**. - Any prover with access to valid public inputs can trigger → **clears**, continue. **Trusted-party-action findings — demote unless an unprivileged amplifier is named.** This applies ONLY to harm that requires the trusted setup or a designated prover acting against documented intent, NOT to ordinary malicious-prover witnesses (those are the default threat model and clear above). If the harm needs the trusted party to misbehave, **DEMOTE** unless the finding names a concrete path by which an *unprivileged* prover reaches the same harm: - **toxic-waste leak** — the setup's secret leaks (or is assumed honest but unverified), after which any prover forges proofs. - **designated-prover gap via public entry** — a constraint the designated prover "shouldn't" violate is reachable through a public input or entry-point template that any prover can drive. - **setup-assumed invariant, prover-checkable** — the setup assumes a tag/range/canonicalization invariant that the circuit never enforces, so any prover can supply a witness that violates it. No unprivileged amplifier → **DEMOTE** (lead, not finding). Amplifier named → judge it on that unprivileged path. ## Gate 4 — Impact Prove material harm. - **Soundness break with external impact**: verifier accepts something it shouldn't (double-spend, signature forgery, unauthorized membership, range-proof bypass, replay, cross-context proof reuse): **CONFIRMED**. - **Completeness break that bricks honest provers permanently** (bad witness derivation, divergent constraint vs. witness logic, infinite loop in witness generator): **CONFIRMED**. - **Privacy leak** that reveals a meaningful function of private inputs (lower bound, range, per-row equality, intent linkage): **CONFIRMED**. ## Confidence Start at **100**, deduct: - partial witness path (steps not fully traced) **-20** - bounded non-compounding impact (small leak, single-shot, self-contained) **-15** - requires specific (but achievable) field-boundary state **-10** - completeness-only impact (no soundness or privacy break) **-10** Confidence ≥ 80 gets description + fix. Below 80 gets description only. ## Safe patterns (do not flag) - `Num2Bits_strict()` / `Bits2Num_strict()` — the built-in alias check rejects `in ≥ p`. - `<==` (not `<--`) for any quadratic relation — emits a constraint that pins the signal. - The canonical inverse pattern: `out <-- 1/x; out * x === 1` paired with `IsZero(x).out === 0` upstream. - `s * (s - 1) === 0` immediately before any `Mux1` / `MultiMux*` selector input. - `BigLessThan(n, k)(r, modulus).out === 1` after `BigMod` / `BigMul` outputs. - `IsEqual(a, b).out === 0` before any `(b - a)`-based EC constraint (e.g. `EllipticCurveAddUnequal`). - Tag templates whose body explicitly enforces the named invariant (e.g. `Uint8Tag` body contains `Num2Bits(8)(in)`). - `Poseidon(.., intentHash)` binding for nullifier-burning / spend proofs (binds proof to spender's intent). - `EllipticCurveAdd` (the dispatch wrapper) when inputs may be equal (vs. `EllipticCurveAddUnequal` which asserts inequality). - `safe*` / `*_strict` / `Force*EqualIfEnabled` family of templates whose name signals the runtime check. ## Lead promotion Before finalizing leads, promote where warranted: - **Cross-template echo.** Same root cause confirmed as FINDING in one template → promote in every template using the same primitive (e.g. every consumer of buggy circomlib `MontgomeryAdd`, `Decoder`, `BinSum` propagates the same bug). - **Multi-agent convergence.** 2+ agents flagged the same area, lead was demoted (not rejected) → promote to FINDING at confidence 75. - **Partial-path completion.** Only weakness is incomplete witness construction but the path is clearly reachable and unguarded → promote to FINDING at confidence 75, description only. - **Composite chain.** Two leads chain into a worse impact than either alone (e.g. missing range-check + selector-mux collapse → always-disabled enforcement) → promote both to FINDING at confidence = min(A, B), with `Chain: [A] + [B]` annotation. ## Leads High-signal trails for manual investigation. No confidence score, no fix — title, code smells, and what remains unverified. ## Do Not Report - Style: snake_case vs camelCase, file layout, missing comments. - Compile-time `assert(...)` used in its legitimate role (parameter sanity checks the user understands won't survive into R1CS). - Generic "this could be optimized" / "circuit size could be smaller" — not a finding. - Centralization / admin-by-design without a concrete circuit-level exploit path. ## references/orchestration ``` ``` ## references/orchestration/claude.md # Claude Orchestration Use this workflow by default in Claude-like runtimes where foreground `Agent`, `Read`, `Glob`, and `Grep` tools are available. Do not use it only when the user explicitly asks for local mode, no subagents, or a single-agent pass. ## Turn 1 - Discover Print the banner from `SKILL.md` exactly, then make these parallel tool calls: 1. Bash `find` for in-scope `.circom` files using the exclude pattern in `SKILL.md`. 2. Locate `references/attack-vectors/attack-vectors.md` and resolve the `references/` directory. 3. Confirm `Agent` is available. 4. Read local `VERSION`. 5. Create a scratch directory under `/tmp`. Do not perform a remote version check unless the user explicitly asked to check or update the skill. ## Turn 2 - Prepare Prefer the shared helper script: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" ``` For specific files, add `--files path/to/A.circom path/to/B.circom`. The script emits `source.md`, optional docs and prior-findings files, and all 17 agent bundles. Print line counts for every generated bundle and for `source.md`; also print line counts for `docs-context.md` and `prior-findings.md` when present. Do not inline bundle contents into agent prompts. Bundle layout: | Bundle | Appended files after `source.md` | |---|---| | `agent-1-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/signal-field.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` | | `agent-2-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/range.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` | | `agent-3-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/selector-accumulator.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` | | `agent-4-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/binding-1.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` + docs if present | | `agent-5-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/binding-2.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` + docs if present | | `agent-6-bundle.md` | `senior-auditor-sop.md` + `attack-vectors/regex-language.md` + `hacking-agents/vector-scan-agent.md` + `hacking-agents/shared-rules.md` | | `agent-7-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/signal-flow-agent.md` + `hacking-agents/shared-rules.md` | | `agent-8-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/range-check-agent.md` + `hacking-agents/shared-rules.md` | | `agent-9-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/arithmetic-field-agent.md` + `hacking-agents/shared-rules.md` | | `agent-10-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/selector-mux-agent.md` + `hacking-agents/shared-rules.md` | | `agent-11-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/invariant-agent.md` + `hacking-agents/shared-rules.md` | | `agent-12-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/intent-binding-agent.md` + `hacking-agents/shared-rules.md` + docs if present | | `agent-13-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/first-principles-agent.md` + `hacking-agents/shared-rules.md` | | `agent-14-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/free-flow-agent.md` + `hacking-agents/shared-rules.md` + docs if present | | `agent-15-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/numerical-gap-agent.md` + `hacking-agents/shared-rules.md` | | `agent-16-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/binding-gap-agent.md` + `hacking-agents/shared-rules.md` + docs if present | | `agent-17-bundle.md` | `senior-auditor-sop.md` + `hacking-agents/composition-gap-agent.md` + `hacking-agents/shared-rules.md` | Agents 1-6 are vector-scan shards. Agents 7-14 are single-lens specialists. Agents 15-17 are gap hunters that hunt bugs across lens boundaries. ## Turn 3 - Spawn Run the selected agents through a bounded foreground-agent queue with maximum concurrency 6. For a full delegated audit, select all 17 agents. For smaller scopes, use the smallest set of bundles that covers the risk, but keep at least one first-principles or free-flow pass. Before spawning, print this agent progress console. Mark the first up to 6 selected agents as `Running`, later selected agents as `Queued`, and omitted agents as `Skipped`: ```markdown ## Agent Progress | Agent | Lens | Status | Current Work | Result | |---|---|---|---|---| | agent-1 | signal-field vector scan | Running | Slice scan | - | | agent-2 | range vector scan | Running | Slice scan | - | | agent-3 | selector/accumulator vector scan | Running | Slice scan | - | | agent-4 | binding-1 vector scan | Running | Slice scan + docs | - | | agent-5 | binding-2 vector scan | Running | Slice scan + docs | - | | agent-6 | regex/language vector scan | Running | Slice scan | - | | agent-7 | signal flow | Queued | Unconstrained witness flow | - | | agent-8 | range checks | Queued | Bounds and aliasing | - | | agent-9 | arithmetic/field | Queued | Wraparound, inverse, division | - | | agent-10 | selectors/muxes | Queued | Gates and booleanity | - | | agent-11 | invariants | Queued | Cross-template invariants | - | | agent-12 | intent/binding | Queued | Domains, public inputs, replay | - | | agent-13 | first principles | Queued | End-to-end attack paths | - | | agent-14 | free flow | Queued | Independent adversarial pass | - | | agent-15 | numerical gaps | Queued | Cross-lens numerical bugs | - | | agent-16 | binding gaps | Queued | Cross-lens binding bugs | - | | agent-17 | composition gaps | Queued | Cross-template composition bugs | - | ``` Spawn no more than 6 foreground `Agent` calls in one batch. As each batch returns, update the table: completed agents become `Done` with a short result count such as `2 findings, 1 lead` or `no findings`; failed agents become `Blocked` with the failure reason. Then start the next queued agents, again with no more than 6 running at once. Repeat until every selected agent is `Done` or `Blocked`. Single-lens prompt for agents 1-14: Replace `agent-N` with the actual agent id (`agent-1`, `agent-2`, ...). ```text You are a malicious prover. Your specialty, mindset, source, and output rules are in your bundle. Read it fully before producing findings. Read first: - ( lines) - source + SOP + specialty + shared rules. Your agent id is agent-N. Every FINDING and LEAD block must include `detected_by: agent-N`. The bundle contains all in-scope source. Do not re-read in-scope files for the initial scan. Use Read/Grep only for cross-file searches or out-of-scope context such as circomlib, vendored includes, and peripheral files. Every FINDING needs file, template, signal, root cause, minimal fix, and a concrete proof. Without proof, emit a LEAD. Output format and the mandatory mental-tool protocol are in shared-rules.md inside your bundle. ``` Gap-hunter prompt for agents 15-17: Replace `agent-N` with the actual agent id (`agent-15`, `agent-16`, or `agent-17`). ```text You are a malicious prover hunting the seams between lenses. Your gap-hunter specialty, mindset, source, and output rules are in your bundle. Read it fully before producing findings. Read first: - ( lines) - source + SOP + gap-hunter specialty + shared rules. Your agent id is agent-N. Every FINDING and LEAD block must include `detected_by: agent-N`. If a finding can be expressed with a single lens alone, drop it. Without concrete proof of the seam, emit a LEAD. Output format and gap-hunter-specific fields are in your bundle. ``` ## Turn 4 - Deduplicate And Validate Deduplicate every FINDING and LEAD from all workers, plus any still-valid prior finding from `prior-findings.md`. Rules: - Tag every raw item with its source agent id if the worker did not include `detected_by`. - Group by `group_key` (`Template | signal_or_local | bug-class`). - Never merge across different `template:` fields. - Never merge across different `local:` or signal fields within a template. - Preserve every distinct mechanism, witness path, and fix strategy. - Preserve and union detector sets. If `agent-2`, `agent-8`, and `agent-14` report the same deduplicated item, the final report item must say `Detected by: agent-2, agent-8, agent-14`. - If two fixes add different constraints, check directions, strict conversions, or target signals, render them as separate fix options. - Run a second pass at `(Template, signal)` ignoring `bug_class` to make sure no mechanism was silently dropped. - Print `Completeness: N unique (Template, signal) in raw, N covered in final.` before triage. Gate each deduplicated item exactly once using `judging.md`: refutation, reachability, trigger, impact. `UNCERTAIN` means the item remains allowed for reporting as a finding or lead rather than being silently rejected. ## Turn 5 - Triage For every finding, spawn a fresh foreground `Agent` to validate whether the bug is real and exploitable. Leads are not triaged. If there are zero findings, skip this turn. Use this prompt shape: ```text Is the following a real bug that we can exploit? --- `
` · Confidence: N> **Description** **Circuit / Constraint** **Fix** (omit this section if the finding is below threshold and has no fix block) --- ``` Read every response in full. Attach: - `triager_verdict`: `Exploitable` or `Not Exploitable`, decided from the substance of the response. - `triager_reasoning`: one concise paragraph preserving concrete constraints, witness steps, and file:line references. If the triage response is genuinely ambiguous, default to `Exploitable` and note the uncertainty. ## Turn 6 - Output Format the final report with `references/report-formatting.md`. - Exclude rejected items. - Keep findings the triager marks `Not Exploitable`; the disagreement is useful to the user. - Include triager verdicts and a `## Triager Reasoning` section because this delegated Claude workflow ran triage. - If `--file-output` was requested, write the report to the configured findings path. ## references/orchestration/codex.md # Codex Orchestration Use this workflow when running in Codex. When Codex exposes subagents through a `spawn_agent`-style API, delegated mode is the default. Use local fallback mode only when subagents are unavailable or when the user explicitly asks for local mode, no subagents, or a single-agent pass. ## Delegated Mode (Default) Use this mode by default when Codex subagents are available. Use the generated bundles: - `agent-1-bundle.md`: signal-field vector scan - `agent-2-bundle.md`: range vector scan - `agent-3-bundle.md`: selector/accumulator vector scan - `agent-4-bundle.md`: binding-1 vector scan - `agent-5-bundle.md`: binding-2 vector scan - `agent-6-bundle.md`: regex/language vector scan - `agent-7-bundle.md`: signal flow - `agent-8-bundle.md`: range checks - `agent-9-bundle.md`: arithmetic and field behavior - `agent-10-bundle.md`: selectors and muxes - `agent-11-bundle.md`: invariants - `agent-12-bundle.md`: intent and binding - `agent-13-bundle.md`: first-principles adversarial pass - `agent-14-bundle.md`: free-flow pass - `agent-15-bundle.md`: numerical gap hunting - `agent-16-bundle.md`: binding gap hunting - `agent-17-bundle.md`: composition gap hunting For small scopes, choose the smallest set of bundles that covers the risk. For large delegated scopes, use all 17 bundles unless the user asked for a smaller parallel pass. Run selected agents through a bounded worker pool with maximum concurrency 6. Before spawning, print an agent progress console. Mark the first up to 6 selected agents as `Running`, later selected agents as `Queued`, and omitted agents as `Skipped`: ```markdown ## Agent Progress | Agent | Lens | Status | Current Work | Result | |---|---|---|---|---| | agent-1 | signal-field vector scan | Running | Slice scan | - | | agent-2 | range vector scan | Running | Slice scan | - | | agent-3 | selector/accumulator vector scan | Running | Slice scan | - | | agent-4 | binding-1 vector scan | Running | Slice scan + docs | - | | agent-5 | binding-2 vector scan | Running | Slice scan + docs | - | | agent-6 | regex/language vector scan | Running | Slice scan | - | | agent-7 | signal flow | Queued | Unconstrained witness flow | - | | agent-8 | range checks | Queued | Bounds and aliasing | - | | agent-9 | arithmetic/field | Queued | Wraparound, inverse, division | - | | agent-10 | selectors/muxes | Queued | Gates and booleanity | - | | agent-11 | invariants | Queued | Cross-template invariants | - | | agent-12 | intent/binding | Queued | Domains, public inputs, replay | - | | agent-13 | first principles | Queued | End-to-end attack paths | - | | agent-14 | free flow | Queued | Independent adversarial pass | - | | agent-15 | numerical gaps | Queued | Cross-lens numerical bugs | - | | agent-16 | binding gaps | Queued | Cross-lens binding bugs | - | | agent-17 | composition gaps | Queued | Cross-template composition bugs | - | ``` When an agent completes, mark it `Done` with a short result such as `2 findings, 1 lead` or `no findings`, then immediately start the next queued agent and mark it `Running`. If an agent fails, mark it `Blocked` with the failure reason and still free that worker slot for the next queued agent. Spawn each selected worker with a concrete, self-contained task. In Codex, use the available subagent API rather than Claude's foreground `Agent` tool. Prompt each worker with: ```text You are auditing Circom circuits. This is read-only analysis; do not edit files. Your agent id is . Read the full bundle at before producing findings. Return only FINDING and LEAD blocks using the schema in the bundle. Every FINDING must include a concrete proof/witness path. No proof means LEAD. Every FINDING and LEAD must include `detected_by: `. ``` While workers run, do local review of include graph, docs, prior findings, and obvious high-risk call sites. After workers return: 1. Tag every raw FINDING and LEAD with its source agent id if the worker did not include `detected_by`. 2. Deduplicate by `group_key`, preserving every distinct mechanism, proof path, fix strategy, and detector set. 3. Union detector sets when multiple agents report the same deduplicated item. Sort detector ids numerically (`agent-2` before `agent-10`). 4. Validate each item with `judging.md`. 5. Optionally triage confirmed findings with fresh subagents if the user asked for triage or if the delegated run is large enough to justify it. 6. Include each item's detector set in the final report per `report-formatting.md`. 7. Include triager verdicts only for findings that were actually triaged. ## Local Fallback Mode Use this mode only when subagents are unavailable or the user explicitly opts out of subagents. 1. Print the banner from `SKILL.md`, then initialize a local progress console: ```markdown ## Audit Progress | Phase | Status | Notes | |---|---|---| | Scope and context | Running | Building source bundle | | Reference loading | Pending | `judging.md`, `report-formatting.md` | | Source review | Pending | Concrete witness paths | | Validation | Pending | Four judging gates | | Report | Pending | Final markdown | ``` Update the table after each phase. 2. Build context with the helper script: ```bash python3 skills/circom-auditor/scripts/build_audit_context.py --repo "$PWD" ``` For a specific scope, pass `--files` with the requested `.circom` paths. 3. Read the generated `source.md`. If present, also read `docs-context.md` and `prior-findings.md`. 4. Read `references/judging.md` and `references/report-formatting.md`. 5. For broad audits, read `references/attack-vectors/attack-vectors.md`. For a narrow audit, load only the relevant `references/hacking-agents/*.md` files. 6. Review the source for concrete witness manipulation paths: - unconstrained `<--` witness assignments. - `assert(...)` where an R1CS constraint was intended. - missing strict bit conversion or limb bounds. - comparator inputs that are not range constrained. - inverse/division without nonzero and multiplication pins. - selector, mux, and enable signals missing booleanity constraints. - unbound public inputs, nullifiers, commitments, signatures, or domains. - field wraparound and aliasing near the BN254 scalar field modulus. - caller-side violations of peripheral library preconditions. 7. Revalidate every candidate with the four gates in `judging.md`: refutation, reachability, trigger, and impact. 8. Produce the report with `references/report-formatting.md`. In local mode, omit triager verdicts and the `## Triager Reasoning` section. ## references/report-formatting.md # Report Formatting ## Report Path Save the report to `assets/findings/{project-name}-zksec-circom-audit-report-{timestamp}.md` where `{project-name}` is the repo root basename and `{timestamp}` is `YYYYMMDD-HHMMSS` at scan time. ## Output Format Use this base template. Apply the local/delegated omissions in the rules below: local reports omit triager metadata, while delegated reports include it only when triage workers actually ran. ```` # 🔐 Circuit Security Review — --- ## Scope | | | | -------------------------------- | ------------------------------------------------------------ | | **Mode** | ALL / default / filename | | **Files reviewed** | `File1.circom` · `File2.circom`
`File3.circom` | | **Confidence threshold (1-100)** | N | --- ## Findings [95] **1. ** `TemplateName (file.circom:LL-LL) · signal: <signalName>` · Confidence: 95 · Detected by: agent-2, agent-8 **Description** <The vulnerable constraint pattern and why it is exploitable, in 1 short sentence> **Circuit / Constraint** ```circom signal lambda <-- (in[1] - 1) / (in[0]); // missing: IsZero(in[0]).out === 0; ``` **Fix** ```diff - signal lambda <-- (in[1] - 1) / (in[0]); + component nz = IsZero(in[0]); + nz.out === 0; + signal lambda <-- (in[1] - 1) / (in[0]); + lambda * in[0] === in[1] - 1; ``` --- [82] **2. <Title>** `TemplateName (file.circom:LL)` · Confidence: 82 · Detected by: agent-4 **Description** <one short sentence> **Circuit / Constraint** ```circom // the offending line(s) verbatim ``` **Fix** ```diff - vulnerable line(s) + fixed line(s) ``` --- < ... all above-threshold findings (≥ confidence threshold) > --- [75] **3. <Title>** `TemplateName (file.circom:LL)` · Confidence: 75 · Detected by: agent-13 **Description** <one short sentence> **Circuit / Constraint** ```circom // the offending line(s) ``` --- < ... all below-threshold findings (Circuit / Constraint shown, no Fix block) > --- Findings List | # | Confidence | Detected by | Title | |---|------------|-------------|-------| | 1 | [95] | agent-2, agent-8 | <title> | | 2 | [82] | agent-4 | <title> | | 3 | [75] | agent-13 | <title> | --- ## Leads _Vulnerability trails with concrete code smells where the full witness/exploit chain could not be completed in one analysis pass. These are not false positives — they are high-signal leads for manual review. Not scored._ - **<Title>** — `Template.signal` — Detected by: agent-7, agent-14 — Code smells: <missing range check, unchecked precondition, etc.> — <1-2 sentence description of the trail and what remains unverified> - **<Title>** — `Template.signal` — Detected by: agent-3 — Code smells: <...> — <1-2 sentence description> --- <Include this section only if delegated triage ran.> ## Triager Reasoning _Independent verification of every finding by a triage subagent. Findings marked **Not Exploitable** are kept for visibility — review the reasoning before discarding._ **1. <Title>** — Exploitable <2-4 sentences from the triager: what is going on and why it is exploitable, with concrete file:line and witness references.> **2. <Title>** — Not Exploitable <2-4 sentences from the triager: what guarding constraint or structural blocker makes this not exploitable.> **3. <Title>** — Exploitable <2-4 sentences.> --- > ⚠️ This review was performed by a lightweight AI assistant. AI analysis cannot verify the complete absence of constraint bugs, and no guarantees are made regarding soundness, completeness, or zero-knowledge properties. A manual security review or a deep, continuous AI scan is strongly recommended. For a consultation regarding your circuit's security, visit [zksecurity.xyz](https://zksecurity.xyz). For deep AI audits, visit [zkao.io](https://zkao.io). ```` **Rules:** - Follow the template above exactly, applying the local/delegated omissions in this section. - Sort findings by confidence (highest first). - The `TemplateName (file.circom:LL)` header replaces Solidity's `Contract.functionName`. When a finding is localized to a specific signal inside the template, append `· signal: <signalName>`. - Every finding metadata line MUST include ` · Detected by: ...`. In delegated mode, list every sub-agent that reported the deduplicated item, sorted by numeric agent id and comma-separated, e.g. `Detected by: agent-2, agent-8, agent-14`. In local fallback mode, use `Detected by: local`. - The Findings List table MUST include a `Detected by` column with the same detector set used on the finding metadata line. - Every lead bullet MUST include `Detected by: ...` using the same rules as findings. - Every finding gets a **Circuit / Constraint** block — the offending line(s) verbatim, OR a comment showing the missing constraint. This is the most important visual element for a Circom finding because it pins the bug to actual code. - Findings ≥ confidence threshold get a **Fix** block (`diff` format showing the minimal patch). Findings below the threshold get **Circuit / Constraint** but no **Fix**. - Use `Num2Bits_strict`, `IsZero`, `BigLessThan`, `<==`, etc. in fix diffs — the Circom-idiomatic safe patterns from `judging.md`. - **Multiple distinct fixes (fix-preservation).** When the dedup pass preserved two or more genuinely distinct fixes for one finding — different added constraints, a different check direction, or a different remediation strategy (e.g. add `IsZero(den).out === 0` vs. switch the divisor to a provably-non-zero source) — render each as a labelled option, verbatim from the agent text. Do not paraphrase or collapse to one. Label intuitively (constrain / range-check / switch-primitive / forbid-sentinel): ```` **Fix (Option A — constrain divisor)** ```diff + component nz = IsZero(in[0]); + nz.out === 0; signal lambda <-- (in[1] - 1) / in[0]; + lambda * in[0] === in[1] - 1; ``` **Fix (Option B — switch to safe primitive)** ```diff - signal lambda <-- (in[1] - 1) / in[0]; + component add = EllipticCurveAdd(...); // dispatch wrapper handles equal-x ``` ```` - Draft findings directly in report format — do not re-generate. - In local mode, omit triager verdicts and omit the `## Triager Reasoning` section. - In delegated mode, include triager verdicts only when triage workers actually ran. In that case, every finding's metadata line ends with ` · **Triager Verdict:** Exploitable` or ` · **Triager Verdict:** Not Exploitable` after the `Detected by` field, and the `## Triager Reasoning` section lists every finding in report order with `**N. <Title>** — Exploitable|Not Exploitable` followed by the triager's reasoning. ## references/senior-auditor-sop.md # Senior Auditor's Mindset This is how a senior ZK auditor thinks. Pattern-matching catches the obvious bugs — your specialty file and the vector catalog teach that. The high-value bugs, the ones everyone else misses, come from HOW you reason about a constraint system, not from WHAT bugs you know. The senior auditor's edge is not "knowing more attack vectors" — it is having internalized mental tools they reach for instinctively when something feels off, when a constraint looks like it pins a signal, or when a conclusion comes too quickly. This file gives you three tools. They are not steps. You reach for the right one the moment the trigger fires — see `shared-rules.md` for the binding trigger→tool protocol. Use them. Trust your discomfort. A finding is not real until you've traced the attack with concrete field values — a witness that satisfies every constraint yet violates the protocol's intent. You are a malicious prover, not the circuit's author — when you find a way to satisfy the R1CS with a bad witness, deepen the attack; never argue yourself out of one. (That argument belongs at JUDGE time, in `judging.md` Gate 1 — not now.) Circom is **declarative**, not imperative. There is no execution order to exploit — there is only the set of constraints and the space of witnesses that satisfy them. So the senior auditor's question is never "what does this line do?" It is always "**what does the constraint system still ALLOW?**" --- ## 1. The Feynman test (FIRST — use it before anything else) **This is the first tool. Apply it the moment you open any new template or `component main`— before you reason about anything else.** A template you have not Feynman'd is a template you have not actually understood. When you read a circuit, STOP and ask: "Can I explain what this template *proves* to someone who doesn't know Circom?" Try it. In plain words — no `<--`, no `<==`, no `===`, no `Num2Bits`, no "R1CS", no signal-vs-constraint vocabulary. Say what the verifier *learns* and what the prover *had to know*. The places where your explanation gets fuzzy — where you reach for Circom syntax instead of plain meaning — are where you're papering over an unconstrained signal. That's where bugs hide. Example: you read `signal lambda <-- (in[1] - 1) / in[0];` and your explanation comes out as "it computes the slope." That's not Feynman. Feynman is: "it asks the prover to supply a number that, multiplied back by `in[0]`, gives `in[1] - 1`." Now keep going: what if `in[0]` is zero? Your plain-English explanation breaks — "multiplied back by zero gives zero," so the prover's number is free. Bug. A senior auditor doesn't trust their understanding of a circuit until they can explain what it proves without the safety net of constraint vocabulary. --- ## 2. Socratic questioning For every constraint, ask: why is this here? What does it pin? Which signal does it leave free? What happens if the value it assumes is at the field boundary? Don't accept "because that's how it's written" as an answer. Don't accept "the template name says so" as an answer. Drill until you reach the implicit belief the constraint rests on. The first answer is usually a restatement. The actual assumption is two or three "whys" deeper. Example: `component lt = LessThan(252); lt.in[0] <== age; lt.in[1] <== 18;` - Why is `LessThan(252)` used here? → to prove `age < 18`. - Why is that sound? → because `LessThan` decomposes its inputs into 252 bits. - What pins `age` to fit in 252 bits before it reaches `lt.in[0]`? → **nothing**. `age` is a raw `signal input`. Set `age = p - 1` and the internal subtraction wraps; `lt.out = 1` is provable for an "adult" who is `p - 1`. Bug. A senior auditor accepts no "this constrains X" without finding the exact line that pins X — and confirming nothing upstream leaves it free. --- ## 3. Inversion Every constraint that looks sufficient gets a backward pass. After you understand what the circuit is *supposed* to prove, ask: how do I produce a witness that satisfies every constraint and still breaks it? Same constraints, malicious-prover's eye instead of author's eye. The author asks "do honest inputs satisfy this?" The attacker asks "what *other* witness also satisfies this?" Read every `===` and ask "what value of the free signal also makes this hold?" Read every `<--` and ask "what is the divisor / gate / selector I can set to zero to make the paired constraint collapse to `0 === 0`?" Read every gated check `flag * (a - b) === 0` and ask "the constraint holds when `flag = 0` — who sets `flag`?" A senior auditor never reads a constraint only in the honest direction. --- ## When to reach for which tool You don't apply these in order — except Feynman, which is always first. You reach for what the moment calls for: - Opening any new template or `component main` → **Feynman** (always — before anything else) - Trying to understand a constraint you don't yet → **Socratic** - A constraint looks like it pins a signal / a check looks sufficient → **Inversion** - You reached a "bug" conclusion → amplify the attack (chain it across every consumer of the primitive, push the precondition to the field boundary, find the worst exploitable variant — do NOT refute it; refutation is Gate 1's job, not yours) The tools are how you keep yourself honest. Without them, you fall into the trap of every junior auditor: trusting your first read, accepting a constraint that "looks like it pins the signal," moving on when something feels off. Trust your discomfort. Reach for the tool. Don't stop until the discomfort has a name — and a concrete witness. ## scripts ``` ``` ## scripts/build_audit_context.py ```python #!/usr/bin/env python3 """Build scratch context bundles for the circom-auditor skill.""" from __future__ import annotations import argparse import datetime as dt import re import tempfile from pathlib import Path from typing import Iterable EXCLUDED_DIR_PARTS = { "node_modules", "tests", "__tests__", "build", "dist", "artifacts", "out", } EXCLUDED_DIR_SUFFIXES = { ("circuits", "test"), ("dependencies", "circomlib"), ("lib", "circomlib"), } EXCLUDED_FILE_SUFFIXES = ( ".test.circom", "_test.circom", "-test.circom", ".witness.json", ".r1cs", ".zkey", ) INCLUDE_RE = re.compile(r'^\s*include\s+"([^"]+)"', re.MULTILINE) DOC_EXTENSIONS = {".md", ".txt", ".rst", ".adoc"} DOC_BUNDLES = { "agent-4-bundle.md", "agent-5-bundle.md", "agent-12-bundle.md", "agent-14-bundle.md", "agent-16-bundle.md", } AGENT_BUNDLES = { "agent-1-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/signal-field.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-2-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/range.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-3-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/selector-accumulator.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-4-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/binding-1.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-5-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/binding-2.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-6-bundle.md": [ "references/senior-auditor-sop.md", "references/attack-vectors/regex-language.md", "references/hacking-agents/vector-scan-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-7-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/signal-flow-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-8-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/range-check-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-9-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/arithmetic-field-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-10-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/selector-mux-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-11-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/invariant-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-12-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/intent-binding-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-13-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/first-principles-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-14-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/free-flow-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-15-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/numerical-gap-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-16-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/binding-gap-agent.md", "references/hacking-agents/shared-rules.md", ], "agent-17-bundle.md": [ "references/senior-auditor-sop.md", "references/hacking-agents/composition-gap-agent.md", "references/hacking-agents/shared-rules.md", ], } def parse_args() -> argparse.Namespace: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--repo", default=".", help="Repository root to audit") parser.add_argument("--skill-dir", default=None, help="circom-auditor skill directory") parser.add_argument("--out", default=None, help="Output directory for scratch bundles") parser.add_argument("--files", nargs="*", default=None, help="Specific .circom files to audit") return parser.parse_args() def resolve_path(path: str | Path) -> Path: return Path(path).expanduser().resolve() def is_relative_to(path: Path, parent: Path) -> bool: try: path.relative_to(parent) return True except ValueError: return False def rel_display(path: Path, repo: Path) -> str: try: return str(path.relative_to(repo)) except ValueError: return str(path) def has_excluded_suffix(parts: tuple[str, ...]) -> bool: for suffix in EXCLUDED_DIR_SUFFIXES: if len(parts) >= len(suffix) and parts[-len(suffix) :] == suffix: return True return False def is_excluded(path: Path, repo: Path) -> bool: try: rel = path.relative_to(repo) except ValueError: rel = path parts = rel.parts if any(part in EXCLUDED_DIR_PARTS for part in parts[:-1]): return True for idx in range(1, len(parts)): if has_excluded_suffix(tuple(parts[:idx])): return True return path.name.endswith(EXCLUDED_FILE_SUFFIXES) def discover_circom_files(repo: Path, explicit_files: list[str] | None) -> list[Path]: if explicit_files: files = [] for item in explicit_files: path = resolve_path(repo / item if not Path(item).is_absolute() else item) if path.suffix != ".circom": raise SystemExit(f"not a .circom file: {item}") if not path.exists(): raise SystemExit(f"missing file: {item}") files.append(path) return sorted(set(files)) files = [] for path in repo.rglob("*.circom"): if path.is_file() and not is_excluded(path, repo): files.append(path.resolve()) return sorted(set(files)) def read_text(path: Path) -> str: return path.read_text(encoding="utf-8", errors="replace") def include_candidates(current: Path, include: str, repo: Path) -> list[Path]: raw = Path(include) if raw.is_absolute(): return [raw] return [ current.parent / raw, repo / raw, repo / "node_modules" / raw, repo / "dependencies" / raw, repo / "dependencies" / "circomlib" / raw, repo / "lib" / raw, repo / "lib" / "circomlib" / raw, ] def resolve_include(current: Path, include: str, repo: Path) -> Path | None: for candidate in include_candidates(current, include, repo): resolved = candidate.resolve() if resolved.exists(): return resolved return None def resolve_includes(initial_files: Iterable[Path], repo: Path) -> tuple[list[Path], list[Path], list[str]]: in_scope = set(initial_files) peripheral: set[Path] = set() missing: set[str] = set() queue = list(in_scope) while queue: current = queue.pop(0) for include in INCLUDE_RE.findall(read_text(current)): resolved = resolve_include(current, include, repo) if resolved is None: missing.add(f"{rel_display(current, repo)} -> {include}") continue if is_relative_to(resolved, repo) and resolved.suffix == ".circom" and not is_excluded(resolved, repo): if resolved not in in_scope: in_scope.add(resolved) queue.append(resolved) else: peripheral.add(resolved) return sorted(in_scope), sorted(peripheral), sorted(missing) def write_source(out_dir: Path, repo: Path, in_scope: list[Path], peripheral: list[Path], missing: list[str]) -> Path: output = out_dir / "source.md" with output.open("w", encoding="utf-8") as handle: handle.write("# Source Bundle\n\n") for path in in_scope: text = read_text(path) handle.write(f"### {rel_display(path, repo)}\n\n") handle.write("```circom\n") handle.write(text) if not text.endswith("\n"): handle.write("\n") handle.write("```\n\n") handle.write("# Include Graph\n\n") for path in in_scope: includes = INCLUDE_RE.findall(read_text(path)) if includes: for include in includes: handle.write(f"- `{rel_display(path, repo)}` includes `{include}`\n") else: handle.write(f"- `{rel_display(path, repo)}` has no direct includes\n") handle.write("\n# Peripheral Files (read on demand)\n\n") if peripheral: for path in peripheral: handle.write(f"- `{rel_display(path, repo)}`\n") else: handle.write("- None\n") if missing: handle.write("\n# Missing Includes\n\n") for item in missing: handle.write(f"- `{item}`\n") return output def write_docs_context(out_dir: Path, repo: Path) -> Path | None: docs_dir = repo / "assets" / "docs" if not docs_dir.is_dir(): return None paths = sorted(path for path in docs_dir.rglob("*") if path.is_file() and path.suffix.lower() in DOC_EXTENSIONS) if not paths: return None output = out_dir / "docs-context.md" with output.open("w", encoding="utf-8") as handle: handle.write("# Docs Context\n\n") for path in paths: text = read_text(path) non_empty = [line.strip() for line in text.splitlines() if line.strip()] handle.write(f"### {rel_display(path, repo)}\n\n") if non_empty and all(line.startswith(("http://", "https://")) for line in non_empty): handle.write("URL list detected. Fetch manually only if the user explicitly authorizes network access.\n\n") for line in non_empty: handle.write(f"- {line}\n") handle.write("\n") else: handle.write(text) if not text.endswith("\n"): handle.write("\n") handle.write("\n") return output def write_prior_findings(out_dir: Path, repo: Path) -> Path | None: findings_dir = repo / "assets" / "findings" if not findings_dir.is_dir(): return None paths = sorted(path for path in findings_dir.rglob("*.md") if path.is_file()) if not paths: return None output = out_dir / "prior-findings.md" with output.open("w", encoding="utf-8") as handle: handle.write("# Prior Findings\n\n") for path in paths: text = read_text(path) handle.write(f"### {rel_display(path, repo)}\n\n") handle.write(text) if not text.endswith("\n"): handle.write("\n") handle.write("\n") return output def append_file(handle, path: Path) -> None: text = read_text(path) handle.write(f"\n\n<!-- BEGIN {path} -->\n\n") handle.write(text) if not text.endswith("\n"): handle.write("\n") handle.write(f"\n<!-- END {path} -->\n") def write_agent_bundles(out_dir: Path, skill_dir: Path, source: Path, docs: Path | None) -> list[Path]: bundles = [] source_text = read_text(source) for filename, references in AGENT_BUNDLES.items(): output = out_dir / filename with output.open("w", encoding="utf-8") as handle: handle.write(source_text) for ref in references: append_file(handle, skill_dir / ref) if docs and filename in DOC_BUNDLES: append_file(handle, docs) bundles.append(output) return bundles def line_count(path: Path) -> int: return len(read_text(path).splitlines()) def main() -> None: args = parse_args() repo = resolve_path(args.repo) skill_dir = resolve_path(args.skill_dir) if args.skill_dir else Path(__file__).resolve().parents[1] if args.out: out_dir = resolve_path(args.out) out_dir.mkdir(parents=True, exist_ok=True) else: stamp = dt.datetime.now().strftime("%Y%m%d-%H%M%S") out_dir = Path(tempfile.mkdtemp(prefix=f"circom-audit-{stamp}-", dir="/tmp")) initial = discover_circom_files(repo, args.files) if not initial: raise SystemExit("no in-scope .circom files found") in_scope, peripheral, missing = resolve_includes(initial, repo) source = write_source(out_dir, repo, in_scope, peripheral, missing) docs = write_docs_context(out_dir, repo) prior = write_prior_findings(out_dir, repo) bundles = write_agent_bundles(out_dir, skill_dir, source, docs) print(f"bundle_dir: {out_dir}") print(f"repo: {repo}") print(f"in_scope_files: {len(in_scope)}") print(f"peripheral_files: {len(peripheral)}") print(f"missing_includes: {len(missing)}") print(f"source.md: {line_count(source)} lines") if docs: print(f"docs-context.md: {line_count(docs)} lines") if prior: print(f"prior-findings.md: {line_count(prior)} lines") for bundle in bundles: print(f"{bundle.name}: {line_count(bundle)} lines") if __name__ == "__main__": main() ```