# Task 5 Report: V1 Stateful Accounting Invariants

## Status

Complete. Commit `6dcbb03` (`test: prove V1 accounting invariants`) adds only the two task-listed test files. Production contracts were not modified.

## Handler design

- `BankHandler` owns four fixed immutable actor addresses (`0x1001` through `0x1004`) and exposes the bounded actor set through `actorCount()` and `actorAt()`.
- `deposit` selects an actor from the seed, bounds the amount to `[1, 10_000e6]`, mints test liquidity, performs actor approval/deposit inside a balanced prank scope, and increments `ghostDeposited` only after success.
- `withdraw` selects an actor, returns early only for a zero bank balance, bounds the amount to `[1, balance]`, performs the withdrawal inside a balanced prank scope, and increments `ghostWithdrawn` only after success.
- `donate` selects an actor, bounds the amount to `[1, 1_000e6]`, mints test liquidity, directly transfers it to the proxy inside a balanced prank scope, and increments `ghostDonated` without touching liabilities.
- In setup, `MockUSDC` ownership transfers from the token owner to the handler. Bank ownership remains unchanged.
- The handler is registered with `targetContract(address(handler))`, and `targetSelector` restricts generated calls to exactly `deposit`, `withdraw`, and `donate`.

## Invariant derivations

1. Ledger conservation: the test independently enumerates the four actors and sums `bank.balanceOf(actor)`. That sum must equal `bank.totalLiabilities()`.
2. Solvency: the token's actual proxy balance must be greater than or equal to total liabilities. Direct donations create only surplus.
3. Independent flow accounting:
   - `ghostDeposited - ghostWithdrawn == totalLiabilities` because only customer custody flows create or extinguish liabilities.
   - `ghostDeposited + ghostDonated - ghostWithdrawn == proxy token reserves` because donations increase reserves without increasing liabilities.

Ghost counters record successful handler inputs, while expected chain state is read from the real proxy and token. The handler does not mirror per-account bank balances, and the invariant test—not the handler—sums on-chain actor balances.

## Changed files

- `test/helpers/BankHandler.sol`: bounded V1 stateful action handler and independent ghost counters.
- `test/BankInvariant.t.sol`: handler setup, selector targeting, and three conservation/solvency invariants.

## TDD evidence

PATH was set in a separate persistent shell step:

```text
export PATH=/tmp/codius-node-v24.18.0/bin:/home/golem/.foundry/bin:$PATH
```

### RED

Exact command:

```text
npm_config_offline=true forge test --match-path test/BankInvariant.t.sol -vvv --force
```

Output before either requested file existed:

```text
[⠒] Compiling 28 files with Solc 0.8.35
Compiler run successful!
No tests found in project! Forge looks for functions that start with `test`
```

This was the expected feature-absent failure: no invariant target or handler existed.

### GREEN

Exact command:

```text
npm_config_offline=true forge test --match-path test/BankInvariant.t.sol -vvv --force
```

Key verbatim output:

```text
Ran 3 tests for test/BankInvariant.t.sol:BankInvariantTest
[PASS] invariant_ghostAccountingMatchesChain() (runs: 128, calls: 8192, reverts: 0)
[PASS] invariant_liabilitiesEqualTrackedBalances() (runs: 128, calls: 8192, reverts: 0)
[PASS] invariant_reservesCoverLiabilities() (runs: 128, calls: 8192, reverts: 0)

| Contract    | Selector | Calls | Reverts | Discards |
| BankHandler | deposit  | 2666  | 0       | 0        |
| BankHandler | donate   | 2791  | 0       | 0        |
| BankHandler | withdraw | 2735  | 0       | 0        |

Suite result: ok. 3 passed; 0 failed; 0 skipped; finished in 3.43s (4.86s CPU time)
Ran 1 test suite in 3.43s (3.43s CPU time): 3 tests passed, 0 failed, 0 skipped (3 total tests)
```

The configured `128` runs and depth `64` produced `8,192` calls per invariant. The fixed seed yielded the same selector counts in the later full-suite run, proving all three actions were exercised.

## Formatting and full-suite validation

Formatting check after applying `forge fmt`:

```text
forge fmt --check test/helpers/BankHandler.sol test/BankInvariant.t.sol
```

Output: empty, exit success.

Full relevant suite command:

```text
npm_config_offline=true forge test -vvv --force
```

Result:

```text
Ran 4 test suites in 6.23s (12.11s CPU time): 43 tests passed, 0 failed, 0 skipped (43 total tests)
```

The invariant portion again passed all three properties for `128` runs and `8,192` calls each, with `2,666` deposits, `2,791` donations, `2,735` withdrawals, and zero reverts/discards. Compilation emitted only two pre-existing OpenZeppelin Foundry Upgrades mutability warnings in `StringFinder.sol` and `DefenderDeploy.sol`.

## Mutation and self-review

Mentally checked realistic mutations:

- Omitting or mis-sizing a deposit/withdraw liability update breaks the ghost-liability equality.
- Updating aggregate liabilities without the selected account balance (or vice versa) breaks the summed-ledger equality.
- Failing to transfer reserves on deposit/withdraw breaks reserve ghost accounting and may break solvency.
- Treating donations as liabilities breaks both the ghost-liability equation and the intended surplus model.
- Draining or under-crediting proxy reserves breaks exact reserve ghost accounting and the solvency inequality.

`git diff --check` and the final formatting check passed. Pre-commit status contained only the two task-listed files. The commit contains exactly those files and 122 inserted test lines. No production files changed.

## Concerns

None. The only warnings are existing third-party mutability warnings noted above.

## Fix Round 1: Genuine handler-absent RED evidence

The original RED evidence above is superseded by this fix round. A missing invariant test only established that Forge had no matching tests; it did not establish that the invariant specification failed when the handler feature was absent.

### Covering test state

An isolated temporary project was created at `/tmp/task-5-red.dLa7CJ`. It contained the committed `test/BankInvariant.t.sol` unchanged but deliberately excluded `test/helpers/BankHandler.sol`. The real worktree remained at commit `6dcbb03f3c79979416c2f0dd37556539276a4e29`, with its tracked files untouched.

Exact isolation command:

```text
rsync -a --exclude=.git --exclude=out --exclude=cache --exclude=test/helpers/BankHandler.sol ./ /tmp/task-5-red.dLa7CJ/
```

Precondition checks confirmed:

```text
isolated invariant test: present
isolated handler: absent
```

PATH was set separately in the isolated shell:

```text
export PATH=/tmp/codius-node-v24.18.0/bin:/home/golem/.foundry/bin:$PATH
```

### Genuine RED

The brief's command was then run literally in the isolated project:

```text
npm_config_offline=true forge test --match-path test/BankInvariant.t.sol -vvv --force
```

Relevant verbatim output:

```text
Compiler run failed:
Error (6275): Source "test/helpers/BankHandler.sol" not found: File not found. Searched the following locations: "/tmp/task-5-red.dLa7CJ".
ParserError: Source "test/helpers/BankHandler.sol" not found: File not found. Searched the following locations: "/tmp/task-5-red.dLa7CJ".
 --> test/BankInvariant.t.sol:5:1:
  |
5 | import {BankHandler} from "./helpers/BankHandler.sol";
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Error: Compilation failed
```

Exit status was captured immediately afterward with `echo $?`:

```text
1
```

This is a genuine RED because the completed invariant test is present and compilation fails specifically at its dependency on the absent stateful handler. Adding `BankHandler.sol` is the production-of-the-test-suite change that makes this exact specification compile and run.

### Fresh GREEN in the real worktree

PATH was again set separately in a new shell rooted at the real worktree:

```text
export PATH=/tmp/codius-node-v24.18.0/bin:/home/golem/.foundry/bin:$PATH
```

The brief's GREEN command was run literally:

```text
npm_config_offline=true forge test --match-path test/BankInvariant.t.sol -vvv --force
```

Relevant verbatim output, repeated for each of the three invariants:

```text
Ran 3 tests for test/BankInvariant.t.sol:BankInvariantTest
[PASS] invariant_ghostAccountingMatchesChain() (runs: 128, calls: 8192, reverts: 0)

| Contract    | Selector | Calls | Reverts | Discards |
| BankHandler | deposit  | 2666  | 0       | 0        |
| BankHandler | donate   | 2791  | 0       | 0        |
| BankHandler | withdraw | 2735  | 0       | 0        |

[PASS] invariant_liabilitiesEqualTrackedBalances() (runs: 128, calls: 8192, reverts: 0)
[PASS] invariant_reservesCoverLiabilities() (runs: 128, calls: 8192, reverts: 0)

Suite result: ok. 3 passed; 0 failed; 0 skipped; finished in 3.53s (4.76s CPU time)
Ran 1 test suite in 3.53s (3.53s CPU time): 3 tests passed, 0 failed, 0 skipped (3 total tests)
```

Exit status captured immediately with `echo $?`:

```text
0
```

All three selectors were exercised over `128` runs at depth `64` (`8,192` calls per invariant), with no revert or discard. No tracked commit was needed for Fix Round 1 because the implementation was already correct; only the ignored evidence report changed. The deferred `actorAt` minor was not addressed.