Implemented WheelPad (WHEELPAD): 1,000,000,000 tokens, 18 decimals, minted once to the deployer.

Included vendored dependencies, deployment/security documentation, and success, failure, fuzz, and invariant tests.

Verified with Solidity 0.8.26:

• forge build passed.
• forge test passed: 36 tests using the supplied fuzz seed.
• forge fmt --check passed.

The external protected launch harness was unavailable locally.

Created launch.json matching WheelPad’s constructor, supply, and required pool/economics.

forge build succeeded; all 36 tests passed with the supplied fuzz seed. Only launch.json is changed for submission.

The review is complete and written to .imd-findings.json with zero findings and eight coverage rows.

Outcome: WheelPad is a sixteen-line contract that inherits the unmodified OpenZeppelin v5.0.2 ERC20 and mints one billion tokens with 18 decimals to the deployer once. I found no defect in the Math Precision, Boundary or Numerical Gap areas, and none outside them severe enough to report.

What I verified, each with concrete inputs:

• The supply literal folds exactly to 1e27, matches the brief, and the launch splits of 10%, 80% and 10% divide with no remainder, so no launch flow can arrive short by rounding.
• Transfers at 0, 1 wei, the full balance, balance plus one and uint256 max behave as the standard says: exact moves or typed reverts, never a panic or a wrap. Self-transfers at full balance are lossless.
• Allowances at max never decrement, at max minus one decrement exactly, and an allowance short by one reverts with the typed error before any state change.
• The sum of balances equals total supply after two hundred fragmented transfers and a 512-run fuzz, because the contract has no division, scaling, casts or decimals conversion to drift.
• There is no payable, receive, fallback, external call or bytes decoding, so the Boundary guide's call-site and sentinel checks have nothing to reach. Value-bearing calls and unknown selectors revert.
• The vendored ERC20 and Context files hash to the lock file's digests and to upstream v5.0.2 fetched from GitHub, so the arithmetic reviewed is the audited upstream code.

Leads rejected: the aderyn large-numeric-literal note on line 10 is a style warning. The compiler evaluates the literal expression exactly at compile time, and the stored constant is the intended value with ample headroom.

Not reached: the protected floor tests need the v4-core library and launch environment variables that are not in this tree, so I could not run them. The token is a plain ERC20 without transfer hooks, so nothing in its code taxes or blocks the factory, distributor or pool manager flows those tests exercise.

The scratch test directory was removed after the run. The untracked dotfiles in the working tree are environment artifacts that predate this task.

I added two test files on top of the existing suite, and I found no defects in WheelPad. forge build and forge test pass with the verifier's seed: 60 tests across 4 suites, none failing. The token is a plain OpenZeppelin ERC-20 that mints 1,000,000,000 × 10¹⁸ to whoever deploys it and has no owner, mint, burn, pause or upgrade functions. Because there was nothing to report, I didn't write .imd-findings.json.

The existing 36 tests (test/WheelPad.t.sol, test/WheelPad.invariant.t.sol) were already thorough and I left them unchanged.

test/WheelPad.edge.t.sol (20 tests):

• Launch in one call: a helper contract deploys the token at a predictable address and sends the 10% swarm share, the pool seed (any share from 0 to 90%) and the remainder, all in one transaction. The test checks each recipient gets exactly its amount and the deployer keeps nothing. Deploying again with the same address seed reverts.
• Boundaries: spending an exact balance or allowance, then 1 wei more, fails. A maximum allowance can't spend more than the balance. An allowance one below the maximum is reduced on each spend, while the maximum isn't. The address zero can't send or approve.
• Failed calls leave no trace: no events, no balance or allowance changes. Spending an allowance emits only a Transfer event.
• Bad input is rejected: truncated or malformed call data, a dirty address argument, and spending through the token's own address.
• Code scan: the token's deployed code contains no DELEGATECALL, CALLCODE or SELFDESTRUCT the code can actually reach. This mirrors the launch's own check.
• Fuzz properties:
  • random call data from random callers never changes the supply or any balance;
  • transfers between any two addresses, including to oneself, update balances correctly and keep the supply fixed;
  • a new approval replaces the old one rather than adding to it;
  • a maximum allowance survives any spending;
  • a failed transferFrom uses up no allowance;
  • strangers can't move anything.

test/WheelPad.ghost.invariant.t.sol (4 invariants, random call sequences):

• What the handler does: it acts as the deployer, the token's own address, named users and up to 12 random addresses. It mixes valid calls with invalid ones (zero address, over balance, over allowance) and also sends random call data. Every outcome is checked against the rules, and the handler never reverts itself.
• What must hold after every sequence:
  • the supply stays fixed and all of it is held by the tracked addresses;
  • each balance equals its starting amount plus what came in minus what went out;
  • no call broke the balance or allowance rules;
  • the token never holds ETH.
• No empty runs: a final check fails any run where no transfer succeeded or no invalid call was attempted.

I didn't install anything, and all edits are under test/. The two new files are not committed.

The permissions review of WheelPad is complete and found no defects. The findings file at .imd-findings.json holds an empty findings list and nine coverage rows, all holds. No tracked file was changed, and the scratch test directory was removed.

What the token is. A single contract inheriting unmodified OpenZeppelin v5.0.2 ERC20, with one constructor that mints 1,000,000,000 tokens at 18 decimals to the immediate caller. I verified all five vendored library files byte-for-byte against upstream v5.0.2 over the network. The compiled ABI has exactly three state-changing functions, the ones the verifier listed, plus views, with no owner, initializer, receive or fallback.

Access Control pass. There are no roles, modifiers or inline permission checks to map. The only writers of balances and allowances are reached through transfer, transferFrom and approve, each keyed on msg.sender through the stock Context contract. The mint branch inside the library is unreachable after construction because a zero sender is rejected both by the allowance check and by the transfer helper, which I confirmed with a probe calling transferFrom from the zero address at amounts 0 and 1. No deployer, factory or other address can pull a holder's balance without that holder's allowance.

Asymmetry pass. The approve and transferFrom pair writes the same allowance slot in mirror directions. The two deviations are OpenZeppelin's standard behaviour: an unlimited allowance never decrements, and spending emits no Approval event. Both are documented in the README and are not defects. Self-transfer, zero-amount and failure paths are atomic and symmetric.

Trust Gap pass. There is no privileged actor, price, fee or formula, so none of the access-by-economics seams exist. The factory holds the supply as an ordinary balance with no powers over other holders.

What I could not run. The protected launch test needs the network's Uniswap v4 PoolManager harness, which this tree does not vendor. I reproduced the parts that do not need it: a CREATE2 deploy credits the factory with the whole supply, launch-style transfers are exact, and the runtime contains no reachable DELEGATECALL, CALLCODE or SELFDESTRUCT. The pool seed and swap paths were not executed here. The project's own 36 unit, fuzz and invariant tests pass, and the formatting check passes. The one static-analysis lead, a large numeric literal, is a compile-time constant of 10^27 and is style only.

The review is complete. .imd-findings.json holds an empty findings list and nine coverage rows, and no tracked source, library or config file was changed.

Result: no defects in the economics area. WheelPad is a 15-line contract inheriting the vendored OpenZeppelin v5.0.2 ERC20 with one constructor mint. Every vendored OZ file matched its SHA-256 in the lock file, so the inherited transfer logic is the audited upstream code.

What I verified against the Economic Security, Invariant and Flow Gap guides, with a scratch Foundry suite that passed in full:

• Supply invariant. The constructor is the only writer of total supply and mints exactly 1e27 to its immediate caller. Deployed through a CREATE2 factory, the factory held everything and no other address held anything.
• Conservation. Sum of balances equals total supply under fuzzed transfer, transferFrom, self-transfer and infinite allowance, in addition to the project's own stateful invariant run with zero reverts.
• Launch flows arrive whole. Swarm share to a distributor, distributor claim, pool seed, remainder transfer, and a pool-manager style push and pull all moved the exact amounts. There is no exemption logic, fee, hook or callback to get wrong.
• No external surface. The reachable runtime contains no CALL-family, CREATE or SELFDESTRUCT opcode, so there is no reentrancy or dependency-failure path. ETH and unknown selectors revert.
• Sentinels. Transfers and approvals to the zero address revert. Tokens sent to the token's own address are stranded by design and the README says so.

The static-analysis lead on the large numeric literal evaluates to exactly 1e27 and is a style note only. Trust assumptions are minimal: there is no owner, minter, pauser or upgrade path, and the deployer's only distinction is receiving the supply, which the factory launch requires.

Both protected tests remain outside what this standalone tree can run, since they import the network's LaunchLiquidity and PoolManager harness. Nothing in the token gives them a path to fail.

The review is complete and the findings file is written. No tracked file was changed.

Outcome: no defects found in the control-flow area. .imd-findings.json holds an empty findings list and eight coverage rows, one per listed entry point plus five invariant rows.

What was checked

• Execution Trace. Both state-changing paths were traced through the vendored OpenZeppelin base. The allowance is spent before the balance moves, but both happen in one frame, so a failing transfer leaves the allowance untouched. Self-transfer, zero-value, zero-address sentinels, and the sticky max allowance all behave as the standard specifies. There are no external calls, hooks, fees, or stale reads.
• Periphery. The six vendored OpenZeppelin files hash identically to the lock file and to the upstream v5.0.2 release fetched from GitHub. No extra files sit in the library directory. The runtime bytecode contains no DELEGATECALL, CALLCODE, SELFDESTRUCT, CALL or STATICCALL in reachable code.
• First Principles. The constructor's only assumption is that its immediate caller is the factory. The protected harness deploys via CREATE2 from the factory address, so that holds. The supply constant equals ten to the twenty-seventh, matching the brief. The ABI exposes nothing but the three standard mutators, and a 22-signature privileged-call battery from both the factory and a stranger reverts without moving supply or balances.

Leads from static analysis. The aderyn "large numeric literal" note is a compile-time constant that evaluates correctly. It is not a defect and was not reported.

Not reached. The Uniswap v4 seed and swap cannot run here because v4-core is not vendored. Since the token has no transfer customisation, nothing in my area can affect those flows, but only the network's harness executes them. This is recorded as an unreached row.

The existing suite of 36 tests and my seven scratch tests all pass. The scratch file lives under test/scratch/, which is ignored and not submitted.

The review is complete and the findings file is written. No tracked file was changed.

Outcome. The WheelPad token is a plain, unmodified OpenZeppelin v5.0.2 ERC20 with a parameterless constructor that mints the full supply to the deployer. I found no code defect. All five specialists reported no findings, so there was nothing to reproduce or merge, and my own pass agrees with them.

What I verified against the code and by running it:

• Build is clean and all 60 existing tests pass, including the two invariant suites.
• A scratch test deployed the token through a CREATE2 factory and confirmed exact supply, decimals, name and symbol, whole transfers factory to distributor to claimant, the approve and transferFrom revert and success paths, infinite-allowance handling, and that every admin selector in the protected floor's lists reverts.
• The reachable-opcode scan from the protected test finds no DELEGATECALL, CALLCODE or SELFDESTRUCT in the runtime.
• Creation and runtime bytecode are far below the size limits, and the empty constructorArgs in launch.json match the constructor.
• The six vendored OpenZeppelin files hash-match the lock file, so the compiled ERC20 is upstream.
• The aderyn large-literal lead evaluates to exactly the manifest supply and is style only.

One info finding kept. Six test-only forge-std files in lib/forge-std differ from the digests recorded in dependencies.lock.json, which claims unmodified v1.9.6. This does not touch the token's bytecode. It is a provenance-record inconsistency, cited at the lock file's Vm.sol entry with the actual versus recorded hash.

Coverage record. All three entry points are marked holds with reasons, plus five invariant rows covering fixed supply, factory deployability, forbidden opcodes and privileged calls, the aderyn lead, and dependency provenance.