Updated launch.json, preserving all 16 verified constructor arguments and clarifying deployment notes.

Schema and ABI checks passed. forge build succeeded; all 31 tests passed, including the protected deployment check. Runtime: 8,285 bytes.

Only launch.json changed outside permitted scratch files.

The review is complete and the findings file is written. The scratch test directory is removed, and the working tree holds only the findings file beyond the committed state.

Scope

Files read: src/Ochre.sol (357 lines, in full), test/Ochre.t.sol (765 lines), README.md, launch.json, the vendored OpenZeppelin ERC721 transfer and mint paths, and the three assigned Pashov guides plus the Senior Auditor's Mindset. The existing suite passes with 30 tests. Nothing in my area was left unreached.

Severity counts: 0 Critical · 0 High · 0 Medium · 0 Low

I found no defect in the Access Control, Trust Gap or Asymmetry areas. The findings file carries an empty list and a coverage row for all eleven listed entry points plus three invariants, every one marked holds with the reason.

What I checked and how I concluded it holds

• Permission model. The only role is admin, fixed in the constructor with no setter, and its only power is the once-per-cave metadata freeze. Every other state-changing function is permissionless by the brief and gated by time, a Merkle proof bound to the caller, or the one-shot release flag. No storage slot has two writers with different guards: the shared seat cursor is written by claim and leftover, which the release flag makes mutually exclusive.
• Confused deputy and value flow. The single coin call always debits the caller to the constant dead address, so nobody can spend another buyer's allowance and the contract never holds funds. Reentry through the coin finds the sale already recorded. The inherited ERC-721 functions are stock OpenZeppelin, and both safeTransferFrom overloads route through the override that rejects contract recipients without any callback. I confirmed the 3-argument overload empirically.
• Paired surfaces. The buy gate and the sweep gate are exact complements at the cave close, so a cave can never be bought and swept in the same state. Sweep's ownership check excludes sold pieces even after transfer, and burn is not exposed, so no id can return to the unminted state. Sale and free piece sets are disjoint in every mint path.
• Ladder and trust seams. A 256-run fuzz compared the contract's lazily computed opening against a direct implementation of the brief's ladder rule after random buys at random times across the whole week. Every round matched, floor buys never moved an opening, and no buy altered another open round's opening. A predecessor's late line sale can still raise a round's quote before that round opens. The README documents that at line 89 and the brief defines the ladder this way, so it stays an observation, not a finding.

Observations, non-blocking

• Admin may freeze a cave's base before the cave opens and the contract does not verify content. The README states both.
• Static analysis leads on uninitialized locals and timestamp comparisons are intentional zero defaults and the brief's own time gates. None reproduces as a defect.

Findings and coverage are in .imd-findings.json at the repository root.

Review complete. .imd-findings.json is in place with both snippets verified against the tree and all 11 entry points covered (plus 7 invariant rows).

Summary

Area covered in depth: Economic Security, Invariant, and Flow Gap guides against src/Ochre.sol.

Result: the economics hold. I traced every value flow and invariant and found no loss-of-funds, wrong-party, or permanent-breakage defect:

• Piece/sale partition — buy ids are always sale slots (5→1), _takeFree skips exactly those, sweep filters by isSalePiece; per-cave sale counts 21/21/42/63/84/84/85 = 400, 335 free, nothing mintable outside 0..736.
• Halving line — K = smallest with opening>>K ≤ floor; segment boundaries are rational (mulDiv/mulmod), ends land on opening>>k, floor-clamped, monotone.
• Ladder — _opening's walk-back is algebraically identical to the per-round rule (max/halve commute with the 2×floor clamp); a previous round's lastLineSale is frozen the instant the next round opens; a late floor buy storing an older round's opening never shifts later openings.
• Payment path — the only coin call is transferFrom(buyer, dead, price) with the bool checked, after all state writes. I confirmed via public RPC that 0xfFf9…6B14 on Sepolia is WETH9 (symbol()="WETH", 18 decimals, bool-returning), so the periphery assumption is sound.
• sweep / claimSeat / releaseUnclaimed / buyLeftover — windows are disjoint, cursors can't double-mint, seat pieces are never swept.

Two low findings (reproductions confirmed in test/scratch/Leads.t.sol; no proof required at this severity):

1. safeTransferFrom (src/Ochre.sol:272) reverts for every contract recipient, including ones implementing onERC721Received — an ERC-721 compliance deviation affecting Safe/4337 wallets and safe-path marketplaces. transferFrom still works, so nothing is stuck.
2. buy (src/Ochre.sol:175) has no maxPrice/expected-id guard. A buy pre-submitted for the opening block of round r+1 can pay up to 4× the openingPrice quoted moments earlier (e.g. quoted 0.002, charged 0.008 when a line sale lands at round 1's opening), and in k>1 rounds a front-run silently swaps the gathering for a line piece. Griefing/UX only — the coin is burned, so no one profits.

Not reached / out of area: OZ ERC-721 internals (approve, setApprovalForAll, transferFrom) were accepted as unmodified upstream code; I did not re-audit them beyond their interaction with sweep's owner check.

The review is complete. The findings file is written and validated, the scratch directory is removed, and the working tree holds only the review output.

Outcome: one low-severity finding, no fund-safety defects. The control-flow area (execution trace, periphery, first principles) was covered in depth, and the contract's core logic held under both static tracing and differential fuzzing.

What I verified

• Ladder and halving line match the brief exactly. A scratch differential test drove random buy patterns (none, floor, one or two line buys) across all 147 rounds for 64 seeds and compared every round's opening against an independent reference. All matched, and openings were stable once the successor round opened.
• Buy, sweep, claim, leftover paths were traced for guards, id arithmetic, state ordering and failure rollback. Mint and all state writes precede the single coin call, and both a false return and a revert from the coin roll back the whole purchase.
• Periphery is sound. OpenZeppelin 5.0.2 and forge-std are vendored as plain files with no submodules, the ERC-721 closure has no revert strings, runtime is 8,285 bytes, and the launch checker passes. The live Sepolia coin was confirmed to be WETH9 with 18 decimals whose transferFrom returns a bool, matching the interface the contract requires.
• Static-analysis leads (uninitialized locals, timestamp use, unchecked returns) were all checked and are false positives or intended design.

The one finding (low)

The override of safeTransferFrom in src/Ochre.sol:272 reverts for every recipient with code, including a fully compliant IERC721Receiver. The contract advertises ERC-721 support, and the standard requires the safe path to succeed when the receiver returns the magic value. No pieces are lost since transferFrom still works, but integrators that only use safeTransferFrom into a contract will fail. The README documents this as deliberate, so the judge needs to decide whether the brief's "no receiver callbacks anywhere" was meant to extend beyond minting.

Coverage record: all 11 verifier-listed entry points have rows (9 hold, 2 carry the finding), plus four invariant and constructor rows. Nothing was left unreached.

The review is complete. .imd-findings.json is written; no project files were changed (scratch tests removed, build artifacts are gitignored).

Summary — Math Precision / Boundary / Numerical Gap audit of src/Ochre.sol

Result: no reproducible defect in the assigned area. One info note recorded.

What I verified (and how)

• Halving line _price (src/Ochre.sol:294-308): K = smallest k with opening>>k <= floor; segment index and remainder come from the same (elapsed·K, roundLength) pair, so boundaries are exact rationals and segment ends land exactly on opening>>k. I wrote an independent reference model and fuzzed it (256 runs; floor 1..1e30, opening 2·floor..1e40, roundLength 1..1e6, every elapsed) — exact match, monotone, clamped at floor, floor from elapsed >= roundLength. Odd openings (3·floor) also checked.
• Ladder _opening (:276-292): random buy/quiet/floor patterns across all 147 rounds matched an off-chain model in 256 runs. Confirmed the subtle seam: a round's line can never still be active once the next round opens (line length == round spacing), so a stored opening never diverges from a prior quote; late floor buys in quiet rounds don't shift anything; cross-cave step uses contiguous keys; 2×/round for 147 rounds stays ≈2^198 with rehearsal args.
• Id/slot/sale-count arithmetic, windows, constructor guards, sweep cursor, _takeFree cursor, payment boundary (bool required, single external call last, revert/false rolls back, no-code coin reverts), label edge cases (32 full ASCII bytes, interior zero, >127), same-second cave boundary (buy < close, sweep ≥ close).
• Existing suite: 30/30 pass; runtime 8,286 bytes (< 9,000).

Finding (info)

src/Ochre.sol:285 — the constructor bounds floorPrice_ ≤ max/2 but not firstPrice_; with firstPrice = 2^256-1, floor = 1 one line sale makes 2 * lastLineSale overflow and every later round's openingPrice/priceNow/buy revert (sweep still recovers pieces). Requires paying >2^255 coin, so unreachable with any real token — reported only for guard consistency.

Coverage

All 11 listed entry points are holds, plus 6 invariant rows (price line, ladder, piece arithmetic, schedule guards, payment boundary, worst-case walk-back gas ≈534k for buy(7,21) after a fully quiet week — bounded, caller-paid, not a defect).

Slither/Aderyn leads (uninitialized locals segments/padding, timestamp comparisons, unchecked _key return) were checked and are intentional/benign.

Added tests and documentation under test/, covering failure paths, pricing boundaries, fuzzing, and lifecycle invariants.

• forge build passed.
• forge test: 45 passed, none failed or skipped.
• Invariants passed 32,768 random calls.

No reproducible defects found. Verification used offline mocks; live Sepolia was not tested.

The review is complete and .imd-findings.json is written. The working tree is otherwise unchanged apart from that file.

Outcome: no critical, high or medium defects. The Ochre contract matches the brief in every mechanism I traced, and the 45-test suite passes with the runtime at 8,285 bytes.

Findings kept (2):

• Low, merged from audit_economics and audit_flow: both safeTransferFrom overloads revert for any recipient with code, so a compliant ERC-721 receiver such as a Safe or an escrow cannot receive a piece through the safe path. Pieces are not stuck because transferFrom works. The README documents it as deliberate, so the author should either record it as an explicit ERC-721 deviation or drop the override. Reproduced in a scratch test.
• Info, from audit_math: the constructor caps floorPrice against doubling overflow but not firstPrice. With firstPrice above 2^255 one line sale makes all later openings revert. Unreachable with WETH or the rehearsal arguments. Reproduced.

Dropped (1): audit_economics' "no maxPrice guard in buy" lead. The brief fixes the buy(c, r) signature, the README states a quote is not a reservation, and payment is burned so nobody profits. That is a design property, not a defect.

Own verification beyond the specialists:

• Fuzzed all 147 rounds per run, 256 runs, against an independent recursive model of the ladder from the brief: 2x last line sale, never below half the prior opening, half after a quiet round, floor at 2x floorPrice, floor buys ignored, cross-cave carry. Every opening and every sampled halving-line price matched.
• Traced id arithmetic, sale counts, sweep cursor, free-piece cursor shared by claim and leftover, Merkle leaf domain separation, payment path, and freeze and tokenURI logic by hand. Slither's two uninitialized-local lines are false positives on default-zero locals.

Coverage: all 11 entry points answered, 9 hold and 2 carry finding 1, plus four invariant rows. The scratch test directory was removed since no finding warranted an attached proof.