uupl-smart-contract/.superpowers/sdd/2026-08-17-uups-bank-demo/task-5-report.md

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:

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

RED

Exact command:

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

Output before either requested file existed:

[⠒] 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:

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

Key verbatim output:

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:

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

Output: empty, exit success.

Full relevant suite command:

npm_config_offline=true forge test -vvv --force

Result:

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:

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

Precondition checks confirmed:

isolated invariant test: present
isolated handler: absent

PATH was set separately in the isolated shell:

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:

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

Relevant verbatim output:

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 $?:

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:

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

The brief's GREEN command was run literally:

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

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

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 $?:

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.