Implemented EthRefund: ETH returns to the caller in the same transaction; failed refunds revert. Includes reentrancy protection, tests, vendored dependencies, and deployment documentation.

Verified with Solidity 0.8.26:

• forge build passes.
• Seeded forge test passes: 22 tests, including fuzz and invariants.
• forge fmt --check passes.

README documents gas costs, deployment assumptions, limitations, and two reviewed heuristic lint warnings.

Created launch.json listing only EthRefund with empty constructor arguments.

Manifest structure and compiled ABI checks passed. forge build succeeded with lint warnings; forge test passed all 22 tests. Only the manifest changed outside permitted scratch output.

I found no defects in EthRefund's permissions, so the findings list is empty. The project's existing tests all pass (22 of 22, run with the README's fuzz seed), and I didn't change any project files.

Coverage: all three entry points (receive(), fallback(), refund()) are marked holds, and I added three invariant rows.

• Access Control: the contract has no roles and no initializer, and anyone may call it by design. The one guard (nonReentrant) runs on all three entry points through _refund(), so none of them has weaker protection. It can't be used to act for someone else: it only ever sends ETH to the address that paid it. It has no upgrade, delegatecall or selfdestruct path, and the deploying factory gets no powers.
• Asymmetry: the three entry points run the same checks, change the same single stored value and make the same call. The success and failure cases match: either the refund and its event both happen, or everything is undone.
• Trust Gap: there is no admin setting, fee, beneficiary or oracle, and payer and payee are always the same address. No one can move value from one user to another.
• Invariants checked: the reentrancy lock can't stay set after a call or be held across transactions. ETH already sitting in the contract (for example, force-sent) is never paid out, since zero-value calls revert and nested calls can't reuse a payment. No privileged role exists.

Static analysis leads:

• I rejected aderyn's high-severity "ETH sent without address checks" warning. The recipient is always the caller who supplied the ETH and can't be chosen. A caller that rejects the refund only reverts its own payment, and existing tests cover this.
• aderyn's low-severity "modifier used only once" warning is about style, not a defect.

Not covered: gas cost is outside this area. The lock uses ordinary storage, where the newer transient storage would be cheaper. That costs more gas but isn't a defect, so I didn't report it. As always, a clean review doesn't prove there are no defects.

The coverage record and these notes are in .imd-findings.json, which is valid JSON.

The review is complete and written to .imd-findings.json. No defects were found in the assigned economic area.

Outcome. The contract is economically sound for its stated purpose. Every call returns exactly its own value to the immediate caller or reverts atomically, and no path pays out any pre-existing balance. One info-level note was recorded, and it is an optimization rather than a defect.

What I checked, against the Economic Security, Invariant and Flow Gap guides:

• Conservation and round trips. Contract balance is unchanged by every call. Forced ETH of 5 ether, planted with selfdestruct, stayed untouched under direct reentry, cross-contract reentry through a second sender, and zero-value calls.
• Sender principal. Rejecting, non-payable and gas-exhausting receivers, a 2300-gas stipend send, uncaught reentry, and a 1 MiB return-data bomb all either revert atomically or leave the sender's balance unchanged. Only gas is spent, and only by that sender.
• Lock state. The lock is set before the external call and cleared after the event. Every failure path reverts and rolls the write back, so no sequence strands it.
• Griefing across senders. There is no shared state beyond the lock, no queue, fee, owner or balance accounting, so one sender's callback can only revert its own call.
• Entry-point equivalence. All three entry points reach the same private function. Odd calldata (1 byte, 3 bytes, selector plus extra bytes) and a max uint256 value all refund cleanly.
• Static-analysis leads. The aderyn "unchecked address" lead is by design, since the recipient is msg.sender and cannot be zero for an executing call. Not a defect.

Info note recorded. The reentrancy lock lives in persistent storage. On the pinned Cancun target, a transient-storage lock would do the same job for far less gas, and gas is the only economic cost this design imposes on senders.

Lock type	First refund()	Later refund()
Storage bool (current)	63,778 gas	59,278 gas
Transient storage	41,595 gas	37,095 gas

Coverage. All three listed entry points are marked holds, with seven extra rows for the invariants and leads above. The existing 22 project tests pass with the pinned fuzz seed. My scratch probe tests were removed and no project file was changed.

The review is complete and the findings file is in place.

Outcome: no exploitable defect in src/EthRefund.sol. The file .imd-findings.json holds one info-level note and seven coverage rows, all three listed entry points marked holds.

What I checked in my area (Execution Trace, Periphery, First Principles):

• Traced every path through the single private _refund body: the guard is set before the value call, zero value reverts, a failed refund reverts the whole payment, and only the current call's value ever leaves the contract. The pre-existing balance is unreachable by any path.
• Cross-entry reentrancy (receive, fallback and refund in every combination) is rejected and the guard is always cleared afterwards, including when the receiver swallows the inner revert.
• There are no parameters other than the sent value, no calldata decoding and no sentinel branches, so the parameter-divergence, encoding and stale-read failure modes have no surface here.
• Scratch probes confirmed three edges the suite does not state explicitly: a caller still inside its constructor gets its refund, a call under roughly 31k gas reverts with nothing lost, and forge-std assertions are not stubbed.
• Build, the full suite with the README seed and the format check all pass. The aderyn "unchecked address" lead is a false positive since the recipient is msg.sender by design.

The one note: the guard is a persistent storage bool on a Cancun build. A measured refund costs about 64k frame gas versus 37k with a transient-storage guard. This is a design tradeoff, not a defect, and I reported it as info only.

Not reached: nothing in the assigned area. There is no launch manifest yet and none is required at this stage.

The review is complete. The findings file holds an empty findings list and a nine-row coverage record, and the scratch tests are removed.

Result: no defects found in the assigned area. The contract has no arithmetic beyond forwarding msg.value verbatim, so the Math Precision and Numerical Gap checklists have nothing to bite on: no division, multiplication, subtraction, narrowing cast, unchecked block or fixed-point scale exists. The Boundary pass reduced to one external call and three payable entry points, and every corner case held.

What I verified concretely, with the existing suite and my own scratch tests:

• All three entry points route through the same guarded _refund(). Zero value reverts before any transfer. The refund is exactly msg.value, and the contract balance always covers it because value is credited before code runs.
• Receiver corner cases. An EOA receives the ETH. A rejecting receiver, a receiver that runs out of gas, and a receiver that succeeds but starves the outer code of its remaining 1/64 gas all revert the whole payment with the sender's balance unchanged and the guard slot back to zero.
• Calldata corner cases. One-byte calldata, eight-byte garbage, fuzzed bytes, and the refund() selector with trailing bytes all refund correctly. Nothing is ever decoded.
• Pre-existing balance stays untouched across 4096 mixed invariant calls, and reentrancy during the callback is rejected on every entry point.
• Deployment. No constructor, nonpayable creation, no owner, and no forbidden opcodes in the runtime.

One row is marked unreached: the protected ownership floor test imports a file absent from this tree, so it could not be run, though the contract exposes no owner and should trivially satisfy it. Static-analysis leads (unchecked address on the ETH send, single-use modifier) were examined and do not represent defects, since the recipient is msg.sender by design and the call result is checked.

Added nine tests covering same-transaction reuse, failure recovery, rollback, value boundaries, events, and forced ETH. Expanded invariants to 256 sequences and 16,384 calls.

forge build and forge test pass with the required seed: 31 tests passed, zero failures.

Only test/ files changed. No reproducible contract defects found.

The review is complete. The findings file is written and the tree has no other changes.

Outcome: The EthRefund contract holds. No correctness or safety defect was found. The one finding kept is informational.

Specialist findings, settled

• audit_economics and audit_flow both reported the same root cause: the reentrancy lock is a persistent storage bool on a Cancun build where a transient-storage lock would do the same job for far less gas. I merged them into one info finding and reproduced it with a scratch test. My measurements matched the economics specialist's numbers exactly, and the flow specialist's figures differ only by probe structure. The guard itself is sound on every entry point and every failure path, so this stays at info and does not block release.
• write_foundry_tests, audit_math and audit_permissions reported nothing, and my own pass agreed.
• The aderyn high lead about unchecked recipient addresses does not reproduce. The recipient is always msg.sender, which cannot be the zero address.

My own pass

• All 31 project tests pass with the pinned fuzz seed, including the 256-run invariant suite. Formatting passes.
• A cross-entry reentry probe confirmed that a callback into a different entry point mid-refund reverts with ReentrantCall and leaves balances untouched.
• The manifest is schema-valid, matches the argument-less nonpayable constructor, and the runtime is 333 bytes with no forbidden opcodes. There is no owner, so nothing can be trapped at the factory.
• Forge lint's reentrancy warnings are the documented sites that the lock covers.

Coverage: all three entry points answered as holds, plus two invariant rows for conservation and deployment. The only thing left for the author to decide is whether to switch the lock to transient storage for the gas saving.