Lesson 6 — Capstone — port openhl-liquidation's InsuranceFund to Solidity, prove the 4 invariants

Question

The Capstone = port openhl-liquidation Stage 10b's InsuranceFund from Rust to Solidity (adapted into an EVM contract), write four conservation-law invariants in Foundry, and run them with invariant testing (256 runs × depth 50 by default, 2,000 runs × depth 100 in the CI profile). Same theorem proved twice, in two languages, mechanically. Discipline transfer complete.

Principle (minimum model)

• Capstone target. openhl-liquidation Stage 10b's InsuranceFund (Rust, crates/liquidation/src/insurance.rs at openhl 260883b: one balance: i64, deposit, withdraw_shortfall) → InsuranceFund.sol. withdraw_shortfall becomes absorb(loss) returns (absorbed, remaining); running totals, an owner and an owner-only withdraw are added for the EVM version.
• Four invariants (in the companion repository's examples/foundry-capstone/). (1) invariant_Conservation: balance == deposits − withdrawn − absorbed. (2) invariant_DepositAccounting: totalDeposited == ghostSumDeposits. (3) invariant_WithdrawAccounting: totalWithdrawn == ghostSumWithdrawn. (4) invariant_AbsorbDecomposition: absorbed + unabsorbed == loss requested — the sequence-level form of the liquidation course's withdraw_shortfall lesson's amount + unfilled == shortfall.
• InsuranceFund.sol shape. uint256 state (balance, totalDeposited, totalWithdrawn, totalAbsorbed) + address immutable owner; deposit(uint256), withdraw(uint256) (owner-only), absorb(uint256). Solidity 0.8 checked arithmetic (overflow reverts) instead of Rust's saturating_add.
• Test harness. InsuranceFundHandler exposes wrappedDeposit / wrappedWithdraw / wrappedAbsorb and keeps five ghost variables. InsuranceFundInvariantTest registers targetContract(address(handler)) + four invariant_* functions.
• Run sizes. Default [invariant] runs = 256, depth = 50 → 12,800 calls per invariant; [profile.ci.invariant] runs = 2000, depth = 100 → 200,000 calls per invariant.
• Answer key. The course's companion repository (psyto/rethlab, examples/foundry-capstone/) holds the same three files; check out a companion-repository commit to get a fixed copy.
• The Capstone is the proof. All four invariants pass = the Solidity invariant test checks, over call sequences, the shortfall law the Rust proptest checked (invariant 4), plus the EVM version's own bookkeeping (invariants 1–3). Discipline crosses the language boundary — proven mechanically.

Worked example + steps

Lesson 6 — Capstone — port openhl-liquidation's InsuranceFund to Solidity, prove the 4 invariants

Goal

Concepts you'll grasp in this lesson:

• The capstone proves the course's thesis with code, not prose. Everything Lesson 0–Lesson 5 set up was about one claim: the conservation-law discipline you used in the openhl liquidation course transfers mechanically to Solidity, and invariant testing proves it the same way proptest! did. Lesson 6 is where you stop reading that claim and execute it. You'll take openhl-liquidation Stage 10b's InsuranceFund — the Rust type that holds the system's last-line-of-defense capital — and port it to Solidity, keeping its shortfall logic and adding the bookkeeping an EVM contract needs. You'll write a Handler that turns single operations into random call sequences, the shape of the balance_never_negative proptest from the liquidation course's withdraw_shortfall lesson. And you'll prove four conservation invariants, one of which is the sequence-level version of the property the liquidation course's withdraw_shortfall lesson proved in Rust. When the green (runs: 256, calls: 12800, reverts: 0) line prints, the course is over — you've demonstrated that the discipline survives the language boundary.
• Four invariants, one shape: conservation laws as equalities between contract state and ghost accounting. Every invariant in this capstone takes the form <contract observable> == <function of ghost variables>. (1) Conservation: fund.balance() == ghostSumDeposits - ghostSumWithdrawn - ghostSumAbsorbed. (2) Deposit accounting: fund.totalDeposited() == ghostSumDeposits. (3) Withdraw accounting: fund.totalWithdrawn() == ghostSumWithdrawn. (4) Absorb decomposition: ghostSumAbsorbed + ghostSumUnabsorbed == ghostSumLossRequested. Invariant 4 carries over the liquidation course's withdraw_shortfall lesson's amount + unfilled == shortfall; invariants 1–3 check the Solidity-side bookkeeping (the Rust fund stores only balance, so it has no totals to check). One conservation-law shape, used four times against four different observables.
• The Handler is where the Rust↔Solidity isomorphism lives. The InsuranceFundHandler is a Solidity contract that exposes wrappedDeposit(uint256) / wrappedWithdraw(uint256) / wrappedAbsorb(uint256) and maintains five ghost variables. The methods bound inputs (so invariant testing's random parameters always produce productive calls, not vm.assume rejections) and update ghosts in lockstep with the target. The closest Rust counterpart is the balance_never_negative proptest in insurance.rs, which runs a random Vec<(bool, i64)> of deposits and shortfall withdrawals; the Handler extends that idea to three operations with ghost accounting. Same idea — random sequences of operations against a model — with the bookkeeping made explicit.
• The lesson deliverable is permanent: examples/foundry-capstone/. Everything you build in this lesson — src/InsuranceFund.sol, test/InsuranceFundHandler.sol, test/InsuranceFund.invariant.t.sol — lives in-repo as the course's answer key. Future readers who graduate Lesson 5 will check their own work against this exact directory. The capstone isn't disposable; it's the final artifact that proves the course works.

Verification:

cd examples/foundry-capstone
forge test --match-contract InsuranceFundInvariantTest -vvv

…prints [PASS] invariant_Conservation() (runs: 256, calls: 12800, reverts: 0) for each of the 4 invariants. After this lesson you'll have built the full capstone, watched the invariants hold across 12,800 random calls, deliberately broken one to see the multi-call counterexample, and compared it side-by-side with the Rust proptest! properties in openhl's insurance.rs.

Specific changes:

• New directory: examples/foundry-capstone/ — forge init-shape Foundry project pinned to the course's pragma ^0.8.35. Treated as a sub-project, not part of the lesson website's build.
• 3 new Solidity files in that directory: src/InsuranceFund.sol (51 lines), test/InsuranceFundHandler.sol (57 lines), test/InsuranceFund.invariant.t.sol (58 lines). Total ~166 lines across the capstone.

Lesson 6 is dense. 60 minutes is the time budget — half spent porting the Solidity, half watching invariant testing run and comparing with the Rust source. The payoff is the moment 4 green invariants print and you realize the conservation-law discipline carried across.

Recap

After Lesson 5:

• Lesson 0: Foundry positioned as commodity prerequisite + REVM as the unifying engine
• Lesson 1–Lesson 3: Solidity testing discipline — forge test, fuzz testing, invariant testing (Handler pattern, ghost variables, sequence counterexamples)
• Lesson 4: cast as the CLI surface over alloy::Provider
• Lesson 5: anvil as the local mainnet clone + the three-surface REVM architecture

Lesson 6 closes the loop. Every concept from Lesson 0–Lesson 5 is used in the capstone:

• vm.prank from Lesson 1 / Lesson 5 (the Handler withdraws as the owner)
• Invariant testing from Lesson 3 (the multi-call sequencing engine)
• The Handler pattern from Lesson 3 (InsuranceFundHandler mirrors CounterHandler's shape)
• Ghost-variable accounting from Lesson 3 (five ghosts in InsuranceFundHandler)

The course was always pointed at this artifact. The intermediate lessons were the prerequisites.

Plan

Seven steps across three Solidity files:

1. Set up the capstone project — mkdir examples/foundry-capstone && cd examples/foundry-capstone && forge init --no-git. Pin the pragma. Delete the default Counter.
2. Read openhl-liquidation Stage 10b's InsuranceFund source — the Rust type at crates/liquidation/src/insurance.rs (openhl commit 260883b). Identify its single field (balance: i64), its two operations (deposit, withdraw_shortfall) and the WithdrawOutcome enum.
3. Write src/InsuranceFund.sol — absorb translates withdraw_shortfall; totals, an owner and withdraw are added for the EVM version.
4. Write test/InsuranceFundHandler.sol — Handler with wrappedDeposit / wrappedWithdraw / wrappedAbsorb and 5 ghost variables (ghostSumDeposits, ghostSumWithdrawn, ghostSumAbsorbed, ghostSumUnabsorbed, ghostSumLossRequested).
5. Write test/InsuranceFund.invariant.t.sol — 4 invariants: invariant_Conservation, invariant_DepositAccounting, invariant_WithdrawAccounting, invariant_AbsorbDecomposition.
6. Run the invariant tests — all 4 invariants should hold at the default 256 runs × 50 depth = 12,800 calls. Use the CI profile (200,000 calls per invariant) for the heavy run.
7. Deliberate-break demo + side-by-side with the Rust proptests — break one ghost update in the Handler, watch the multi-call counterexample appear. Then put the Solidity invariants next to the Rust proptest! properties in insurance.rs.

Quick check: how would you write "balance equals deposits minus withdrawals minus absorbed" as a Solidity assertion?

(Answer: assertEq(fund.balance(), handler.ghostSumDeposits() - handler.ghostSumWithdrawn() - handler.ghostSumAbsorbed()); — the same shape as a Rust prop_assert_eq!(left, right). The main difference: the ghost accessors are explicit handler.X() calls because one Solidity contract can't read another's fields directly. The transformation is mechanical because the underlying theorem is language-agnostic — conservation laws are math, not syntax.)

The deliverable file tree

examples/foundry-capstone/
├── foundry.toml                              ← invariant runs, depth, fail_on_revert
├── src/
│   └── InsuranceFund.sol                     ← 51 lines — the Solidity port
├── test/
│   ├── InsuranceFundHandler.sol              ← 57 lines — Handler with 3 wrapped methods + 5 ghosts
│   └── InsuranceFund.invariant.t.sol         ← 58 lines — 4 invariant_* functions
└── lib/forge-std/                            ← standard forge-std submodule

When you finish Lesson 6, every file in this tree exists and forge test passes 4 invariant assertions at 12,800+ random sequences.

The Rust ↔ Solidity field mapping

┌────────────────────────────────────────┬──────────────────────────────────────────┐
│  openhl Stage 10b (Rust, 260883b)      │  examples/foundry-capstone (Solidity)    │
│  crates/liquidation/src/insurance.rs   │                                          │
├────────────────────────────────────────┼──────────────────────────────────────────┤
│  struct InsuranceFund { balance: i64 } │  contract InsuranceFund                  │
│                                        │    uint256 public balance;               │
│  (no counterpart)                      │    totalDeposited / totalWithdrawn /     │
│                                        │    totalAbsorbed; immutable owner        │
├────────────────────────────────────────┼──────────────────────────────────────────┤
│  fn deposit(&mut self, fee: i64) -> i64│  function deposit(uint256 amount)        │
│    (fee <= 0 is a no-op; saturating)   │    (reverts on 0; checked arithmetic)    │
│  fn withdraw_shortfall(&mut self,      │  function absorb(uint256 loss)           │
│    shortfall: i64) -> WithdrawOutcome  │    returns (absorbed, remaining)         │
│    amount + unfilled == shortfall      │    absorbed + remaining == loss          │
│  (no counterpart)                      │  function withdraw(uint256) — owner-only │
├────────────────────────────────────────┼──────────────────────────────────────────┤
│  4 proptest! properties in mod tests   │  4 invariant_* functions (this lesson)   │
└────────────────────────────────────────┴──────────────────────────────────────────┘

The mapping is not one-to-one. The core that carries the conservation law — withdraw_shortfall → absorb, with amount + unfilled == shortfall → absorbed + remaining == loss — translates directly. The running totals, the owner and the owner-only withdraw are additions for the EVM version (they give the invariants contract-side bookkeeping to check). Translate the core; mark the additions as additions.

Walk-through

Step 1: Set up the capstone project

From the companion repository's root:

mkdir -p examples/foundry-capstone
cd examples/foundry-capstone
forge init --no-git

--no-git because we want this capstone to be a subdirectory of the companion repository, not its own git project (forge still installs lib/forge-std). The result (plus a README.md):

examples/foundry-capstone/
├── foundry.toml
├── src/Counter.sol          ← delete this
├── test/Counter.t.sol       ← delete this
├── script/Counter.s.sol     ← delete this (optional)
└── lib/forge-std/

Delete the Counter templates:

rm src/Counter.sol test/Counter.t.sol script/Counter.s.sol

Update foundry.toml to pin the pragma + invariant defaults:

[profile.default]
src = "src"
out = "out"
libs = ["lib"]
solc = "0.8.35"

[invariant]
runs = 256
depth = 50
fail_on_revert = false

[profile.ci.invariant]
runs = 2000
depth = 100

Clean slate ready.

Step 2: Read the Rust source-of-truth

Open crates/liquidation/src/insurance.rs in openhl at commit 260883b (Stage 10b). Identify the structural elements:

• 1 state field: balance: i64 (private, read through fn balance()); new(initial) clamps negative initial balances to 0
• 2 operations: deposit(fee: i64) -> i64 (non-positive fee is a no-op; saturating_add caps at i64::MAX) and withdraw_shortfall(shortfall: i64) -> WithdrawOutcome
• No errors: bad inputs are no-ops, not Errs (a non-positive shortfall returns Covered { amount: 0 })
• Decomposition shape for withdraw_shortfall: Covered { amount } / PartiallyDrained { amount, unfilled } / Depleted { unfilled }, with amount + unfilled == shortfall

The Solidity version keeps that decomposition as absorb(loss) -> (absorbed, remaining) with absorbed = min(loss, balance) and remaining = loss - absorbed, and adds what an EVM contract with invariant tests needs: running totals, an owner, an owner-only withdraw, and custom-error reverts.

Step 3: Write src/InsuranceFund.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.35;

/// @notice Solidity adaptation of openhl-liquidation Stage 10b's InsuranceFund.
/// `absorb` mirrors Rust's `withdraw_shortfall` (absorbed + remaining == loss);
/// the totals, `owner` and `withdraw` are Solidity-side additions.
contract InsuranceFund {
    uint256 public balance;
    uint256 public totalDeposited;
    uint256 public totalWithdrawn;
    uint256 public totalAbsorbed;
    address public immutable owner;

    error ZeroAmount();
    error NotOwner();
    error InsufficientBalance(uint256 requested, uint256 available);

    constructor(address _owner) {
        owner = _owner;
    }

    /// Counterpart of Rust's `fn deposit(&mut self, fee: i64) -> i64`.
    /// Anyone can deposit; zero reverts (Rust treats fee <= 0 as a no-op).
    function deposit(uint256 amount) external {
        if (amount == 0) revert ZeroAmount();
        balance += amount;
        totalDeposited += amount;
    }

    /// No Rust counterpart: an owner-only withdrawal added for the EVM version.
    /// Reverts on zero, non-owner, or insufficient balance.
    function withdraw(uint256 amount) external {
        if (msg.sender != owner) revert NotOwner();
        if (amount == 0) revert ZeroAmount();
        if (amount > balance) revert InsufficientBalance(amount, balance);
        balance -= amount;
        totalWithdrawn += amount;
    }

    /// Counterpart of Rust's `fn withdraw_shortfall(&mut self, shortfall: i64) -> WithdrawOutcome`.
    /// Absorbs as much loss as the balance allows; returns (absorbed, remaining)
    /// where absorbed + remaining == loss. Remaining is what the fund
    /// couldn't cover — in the real system, this flows to ADL.
    function absorb(uint256 loss) external returns (uint256 absorbed, uint256 remaining) {
        if (loss == 0) revert ZeroAmount();
        absorbed = loss > balance ? balance : loss;
        remaining = loss - absorbed;
        balance -= absorbed;
        totalAbsorbed += absorbed;
    }
}

Seven things to notice — these are the load-bearing translation decisions:

1. i64 → uint256. The Rust fund stores balance: i64 and clamps negative inputs to zero; the Solidity version uses unsigned uint256, so negative amounts can't be expressed at all. The conservation-law shape is unchanged. An unsigned type turns Rust's balance >= 0 property into a type guarantee.

2. Rust no-ops → Solidity reverts. The Rust fund never returns an error: non-positive deposits and shortfalls are silent no-ops. The Solidity version reverts with custom errors (ZeroAmount, NotOwner, InsufficientBalance) — the usual EVM style, and an intentional behaviour difference to keep in mind when comparing the two.

3. WithdrawOutcome enum → (absorbed, remaining) tuple. Rust's three variants collapse into one tuple: Covered { amount } = (loss, 0), PartiallyDrained { amount, unfilled } = (balance, loss - balance), Depleted { unfilled } = (0, loss). The equation amount + unfilled == shortfall becomes absorbed + remaining == loss.

4. Rust getter → public storage. Rust keeps balance private behind fn balance(); Solidity's public keyword generates the same kind of getter (balance()), so the Handler and invariant contracts can read state without custom view functions.

5. owner is new. The Rust fund has no owner (in Stage 10c it is owned by LiquidationScanner). The Solidity contract adds an immutable owner so withdraw can be access-controlled.

6. Saturating vs checked arithmetic. Rust's deposit uses saturating_add (caps at i64::MAX). Solidity 0.8 arithmetic is checked: an overflow reverts with Panic(0x11) instead of saturating. The Handler bounds inputs to type(uint96).max, so overflow doesn't occur in these tests. Same safety goal (no silent wrap-around), different failure mode.

   [!NOTE] Mimicking Rust's Wrapping Behavior and Gas Optimization via unchecked In Solidity 0.8+, if you want to bypass the default safety checks to mimic Rust's wrapping arithmetic behavior (like wrapping_add or wrapping_sub), or if you need to optimize gas efficiency to match the performance profile of the Rust implementation, you can wrap operations inside an unchecked { ... } block:

   unchecked {
       balance -= amount; // Gas saving, or intentional wrapping behavior
   }
   

   Since unchecked disables the compiler-generated overflow/underflow checks (which throw Panic(0x11)), it reduces transaction gas costs. For infrastructure engineers, it is a key discipline to explicitly separate safe, boundary-checked arithmetic (the default) from performance-critical sections where checks have already been manually verified and can be skipped (unchecked).

7. uint256 public balance is intentionally a storage variable, not EVM-native address(this).balance. The Rust source maintains its own explicit balance field; the port mirrors that field. This isn't redundant — it's isolation. A forced ETH transfer to the contract address (e.g., via selfdestruct from another contract) would mutate address(this).balance without going through deposit, breaking the conservation invariant if the fund relied on the EVM-native balance. By tracking balance as a private bookkeeping variable, the conservation law verifies the fund's own accounting, immune to external ETH-injection side effects. The Rust-faithful storage variable is also a deliberate safety choice; EVM-native balance is reachable by external mutators that bypass the contract's invariants.

Step 4: Write test/InsuranceFundHandler.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.35;

import {Test} from "forge-std/Test.sol";
import {InsuranceFund} from "../src/InsuranceFund.sol";

/// @notice Handler for InsuranceFund invariant testing.
/// Wraps the 3 fund operations, bounds inputs to productive ranges,
/// maintains 5 ghost variables that mirror the conservation-law expectations.
contract InsuranceFundHandler is Test {
    InsuranceFund public fund;
    address public immutable owner;

    // Five ghost variables — the shadow specification of the fund's accounting.
    uint256 public ghostSumDeposits;
    uint256 public ghostSumWithdrawn;
    uint256 public ghostSumAbsorbed;
    uint256 public ghostSumUnabsorbed;        // total of `remaining` returns from absorb
    uint256 public ghostSumLossRequested;     // total of `loss` parameters passed to absorb

    constructor(InsuranceFund _fund, address _owner) {
        fund = _fund;
        owner = _owner;
    }

    /// Wraps fund.deposit(). Bounds input to a reasonable range so the
    /// random uint256 from forge-invariant doesn't blow past uint96.
    /// Updates the deposit ghost in lockstep.
    function wrappedDeposit(uint256 amount) public {
        amount = bound(amount, 1, type(uint96).max);
        fund.deposit(amount);
        ghostSumDeposits += amount;
    }

    /// Wraps fund.withdraw(). Only callable when there's balance to withdraw.
    /// Uses vm.prank to simulate owner authorization (the handler is not the
    /// owner; the owner is a separate constructor-set address).
    function wrappedWithdraw(uint256 amount) public {
        uint256 currentBalance = fund.balance();
        if (currentBalance == 0) return;  // can't withdraw from empty fund
        amount = bound(amount, 1, currentBalance);
        vm.prank(owner);
        fund.withdraw(amount);
        ghostSumWithdrawn += amount;
    }

    /// Wraps fund.absorb(). Tracks both the requested loss and the actual
    /// decomposition (absorbed + remaining). This is the trickiest ghost
    /// update — three counters must move in lockstep.
    function wrappedAbsorb(uint256 loss) public {
        loss = bound(loss, 1, type(uint96).max);
        ghostSumLossRequested += loss;
        (uint256 absorbed, uint256 remaining) = fund.absorb(loss);
        ghostSumAbsorbed += absorbed;
        ghostSumUnabsorbed += remaining;
    }
}

Five things to notice — these are the Handler-discipline patterns:

1. The Handler inherits Test to get bound() and vm.* access. bound(x, min, max) is forge-std's helper that maps any uint256 into [min, max] (values already in range pass through unchanged; others are wrapped in with a modulo). vm.prank(owner) makes the next call appear to come from the owner address (impersonation inside a test, learned in Lesson 1 + Lesson 5). Inheriting Test is the standard Handler pattern — it gives you cheatcode access for input bounding + authorization simulation.
2. Every wrapped method updates ghosts in lockstep with the call. wrappedDeposit increments ghostSumDeposits after fund.deposit(amount) succeeds. If the call were to revert, the increment wouldn't happen — that's correct, because the fund's state didn't change. The lockstep is per-method; reverts unwind both the fund state and the would-be ghost update.
3. wrappedWithdraw short-circuits when balance is zero. Without this, the bound to [1, currentBalance=0] would fail (min > max), or worse, the fund.withdraw(amount) would revert with InsufficientBalance, and fail_on_revert = false would just count the revert and move on (which is fine, but wastes iterations). Defensive short-circuit inside the Handler beats wasted iterations.
4. wrappedAbsorb updates THREE ghosts: ghostSumLossRequested (the input), ghostSumAbsorbed (what the fund actually absorbed), ghostSumUnabsorbed (the remaining = excess loss that the fund couldn't cover). This is what makes invariant_AbsorbDecomposition provable — the handler tracks all three quantities so the invariant can assert their conservation. More ghosts isn't a code smell; it's how invariants become provable.
5. The owner is constructor-set and immutable. The Handler doesn't become the owner; it impersonates the owner via vm.prank for each withdraw. Neither the test nor the handler should be the owner, because that would mask access-control bugs. Authorization simulation, not authorization replacement.

Step 5: Write test/InsuranceFund.invariant.t.sol

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.35;

import {Test} from "forge-std/Test.sol";
import {InsuranceFund} from "../src/InsuranceFund.sol";
import {InsuranceFundHandler} from "./InsuranceFundHandler.sol";

/// @notice 4 conservation invariants for the Solidity InsuranceFund.
/// Invariant 4 is the sequence-level form of the Rust
/// `withdraw_amount_plus_unfilled_equals_shortfall` proptest.
contract InsuranceFundInvariantTest is Test {
    InsuranceFund public fund;
    InsuranceFundHandler public handler;
    address constant OWNER = address(0xBABE);

    function setUp() public {
        fund = new InsuranceFund(OWNER);
        handler = new InsuranceFundHandler(fund, OWNER);
        targetContract(address(handler));
    }

    /// Invariant 1: Conservation of capital.
    /// fund.balance() == ghostSumDeposits - ghostSumWithdrawn - ghostSumAbsorbed
    /// This is the load-bearing conservation law — every wei that entered as a
    /// deposit either still sits in the fund, or left via withdraw, or was
    /// consumed by absorb. No wei appears or disappears unaccounted-for.
    function invariant_Conservation() public view {
        assertEq(
            fund.balance(),
            handler.ghostSumDeposits() - handler.ghostSumWithdrawn() - handler.ghostSumAbsorbed()
        );
    }

    /// Invariant 2: Deposit-side accounting consistency.
    /// The fund's view of total deposits matches the handler's accounting.
    /// Catches: double-counting in deposit, ghost update missing or wrong scale.
    function invariant_DepositAccounting() public view {
        assertEq(fund.totalDeposited(), handler.ghostSumDeposits());
    }

    /// Invariant 3: Withdraw-side accounting consistency.
    /// The fund's view of total withdrawals matches the handler's accounting.
    /// Catches: similar bugs on the withdraw path.
    function invariant_WithdrawAccounting() public view {
        assertEq(fund.totalWithdrawn(), handler.ghostSumWithdrawn());
    }

    /// Invariant 4: Absorb-decomposition equivalence.
    /// For every absorb(loss): absorbed + remaining == loss.
    /// Aggregated: ghostSumAbsorbed + ghostSumUnabsorbed == ghostSumLossRequested.
    /// Catches: the fund's absorb math being wrong (e.g., remaining = loss - balance
    /// instead of loss - absorbed), or the handler forgetting to track unabsorbed.
    function invariant_AbsorbDecomposition() public view {
        assertEq(
            handler.ghostSumAbsorbed() + handler.ghostSumUnabsorbed(),
            handler.ghostSumLossRequested()
        );
    }
}

Four things to notice — these are the load-bearing invariant patterns:

1. Each invariant_* is one line of assertEq. No control flow, no branching, no exception handling — just an arithmetic equality. This is the conservation-law shape made concrete in Solidity. Conservation laws are equalities; equalities are one-liners.

2. The invariants reference both fund state and ghost state. Invariant 1 reads fund.balance() (the actual contract observable) and the 3 ghosts. The discrepancy between the two surfaces is what catches bugs. The ghost is the spec; the contract is the implementation; the invariant is the equality between them.

3. Invariant 2 and 3 are accounting cross-checks. The fund has its own totalDeposited and totalWithdrawn fields (matching the Rust struct). Invariants 2 and 3 verify the handler and the fund agree on these values. If the fund's deposit accidentally double-incremented totalDeposited, invariant 2 would catch it. Cross-checking the contract's own bookkeeping against the handler's bookkeeping catches contract-internal bugs.

4. "Multi-Layered Invariants" Design Pattern

   In this test suite, we are deliberately combining invariants of different architectural scopes. This is known as a "Multi-Layered Invariants" design pattern, which is extremely helpful for partitioning bugs and eliminating false positives:

   • System-Level Conservation Laws (Invariant 1): Cross-checks the actual balance of the contract (the observable state) against the net inputs/outputs recorded by the ghosts. This checks the global economic sanity of the system (e.g., that no capital is created or destroyed).

   • Component-Level Internal Invariants (Invariant 4): Only compares ghost states against each other without referencing contract state (e.g., ghostSumAbsorbed + ghostSumUnabsorbed == ghostSumLossRequested). This ensures the mathematical relationships within operations are consistent.

   • "Watching the Watchers" Defense: Bugs in your test logic (ghost updates) are the primary source of flaky invariant failures. Invariant 4 purely verifies that the handler's internal accounting behaves correctly, thus serving as a self-validation layer for the test suite.

   • Narrowing down a failure: When a run fails:

     • If Invariant 4 fails: it only involves ghosts and the values absorb returned, so look at the handler's absorb accounting first (or at absorb's return values).
     • If only Invariant 1 fails, while Invariant 4 passes: the decomposition is consistent, so look at how the contract's balance moves (or at the deposit / withdraw ghosts).
     • Both can fail for one bug: Step 7 drops one ghost update in the handler, and Invariants 1 and 4 both fail.

     This narrows where to look; it doesn't replace reading the counterexample.

Step 6: Run the invariants

cd examples/foundry-capstone
forge test --match-contract InsuranceFundInvariantTest -vvv

Expected output:

Ran 4 tests for test/InsuranceFund.invariant.t.sol:InsuranceFundInvariantTest
[PASS] invariant_AbsorbDecomposition() (runs: 256, calls: 12800, reverts: 0)
[PASS] invariant_Conservation() (runs: 256, calls: 12800, reverts: 0)
[PASS] invariant_DepositAccounting() (runs: 256, calls: 12800, reverts: 0)
[PASS] invariant_WithdrawAccounting() (runs: 256, calls: 12800, reverts: 0)
Suite result: ok. 4 passed; 0 failed; 0 skipped; finished in ...

(Foundry 1.7.1; with -vvv each result is also followed by a per-selector table of calls / reverts / discards.)

4 invariants, 12,800 random call sequences, all green. Each invariant has been checked after every one of those 12,800 random calls — a total of 51,200 individual assertEq evaluations — and all held.

For the heavy proof, bump to the CI profile (2,000 runs × depth 100 = 200,000 calls per invariant):

FOUNDRY_PROFILE=ci forge test --match-contract InsuranceFundInvariantTest -vvv

It prints (runs: 2000, calls: 200000, reverts: 0) for each invariant and took about 13 seconds on the machine used to check this lesson. 4 × 200,000 = 800,000 invariant checks, all green.

Step 7: Deliberate-break demo + the Rust proptest side-by-side

Break invariant 1 by introducing a subtle bug: in wrappedAbsorb, forget to update ghostSumAbsorbed:

function wrappedAbsorb(uint256 loss) public {
    loss = bound(loss, 1, type(uint96).max);
    ghostSumLossRequested += loss;
    (uint256 absorbed, uint256 remaining) = fund.absorb(loss);
    // ghostSumAbsorbed += absorbed;    // ← deliberately commented out
    ghostSumUnabsorbed += remaining;
}

Re-run:

[FAIL: assertion failed: 79228162514264337593543950336 != 79228162514264337593543998142]
    [Sequence] (original: 8, shrunk: 2)
        sender=0x...171f addr=[test/InsuranceFundHandler.sol:InsuranceFundHandler]0x2e23... calldata=wrappedDeposit(uint256) args=[74161 [7.416e4]]
        sender=0x...14C4 addr=[test/InsuranceFundHandler.sol:InsuranceFundHandler]0x2e23... calldata=wrappedAbsorb(uint256) args=[47806 [4.78e4]]
 invariant_AbsorbDecomposition() (runs: 0, calls: 0, reverts: 0)
[FAIL: assertion failed: 79228162514264337593543976689 != 79228162514264337593544024495]
    [Sequence] (original: 8, shrunk: 2)
        (same two calls)
 invariant_Conservation() (runs: 0, calls: 0, reverts: 0)
[PASS] invariant_DepositAccounting() (runs: 256, calls: 12800, reverts: 0)
[PASS] invariant_WithdrawAccounting() (runs: 256, calls: 12800, reverts: 0)
Suite result: FAILED. 2 passed; 2 failed; 0 skipped; ...

(Real Foundry 1.7.1 output, addresses shortened. The fuzzer is randomly seeded, so your arguments and numbers will differ; the compiler also warns that absorbed is now unused.)

Read the shrunk counterexample:

1. wrappedDeposit(74161) — bound leaves an in-range value unchanged, so fund.balance = 74161, ghostSumDeposits = 74161
2. wrappedAbsorb(47806) — the fund absorbs 47806 → fund.balance = 26355; ghostSumAbsorbed not updated (the bug!); ghostSumUnabsorbed = 0; ghostSumLossRequested = 47806

Now invariant 1 checks fund.balance() (26355) == ghostSumDeposits (74161) - ghostSumWithdrawn (0) - ghostSumAbsorbed (0, buggy!) → FAIL, and invariant 4 checks ghostSumAbsorbed (0) + ghostSumUnabsorbed (0) == ghostSumLossRequested (47806) → FAIL.

The shrinker reduced the original 8-call failing sequence to these 2 calls (the values in the assertion failed line come from that original sequence, which included much larger amounts). Re-running forge test replays the saved 2-call sequence and prints exactly the numbers above: assertion failed: 26355 != 74161 for invariant 1 and assertion failed: 0 != 47806 for invariant 4. Invariants 1 and 4 both caught the bug; 2 and 3 don't involve absorb and still pass.

Restore the commented-out line. Re-run. All 4 green.

Now compare with the Rust side. Open crates/liquidation/src/insurance.rs in openhl at commit 260883b (Stage 10b); its mod tests ends with four proptest! properties. Put them next to our InsuranceFund.invariant.t.sol:

┌────────────────────────────────────────┬──────────────────────────────────────────┐
│  openhl insurance.rs (Rust, proptest!) │  Lesson 6 capstone (invariant tests)     │
├────────────────────────────────────────┼──────────────────────────────────────────┤
│  withdraw_amount_plus_unfilled_        │  invariant_AbsorbDecomposition           │
│    equals_shortfall                    │    (summed over a call sequence)         │
│  withdraw_amount_matches_balance_delta │  invariant_Conservation (balance moves   │
│                                        │    by exactly what went in and out)      │
│  deposit_is_additive                   │  invariant_DepositAccounting (closest)   │
│  balance_never_negative                │  (guaranteed by uint256 + checked math)  │
│  (no counterpart)                      │  invariant_WithdrawAccounting            │
├────────────────────────────────────────┼──────────────────────────────────────────┤
│  ops: Vec<(bool, i64)> — each step is  │  Handler methods:                        │
│    deposit or withdraw_shortfall       │    wrappedDeposit / wrappedWithdraw /    │
│                                        │    wrappedAbsorb                         │
└────────────────────────────────────────┴──────────────────────────────────────────┘

Different names, and not a 1:1 set: two properties carry over directly, one becomes a type guarantee, and the Solidity side adds checks for its extra bookkeeping. The conservation law at the centre — what came in equals what is still there plus what went out — is the same. That is the part of the discipline that survives the language boundary.

Common errors

• StdUtils bound(uint256,uint256,uint256): Max is less than min. — your bound(amount, min, max) has min > max. Usually means you passed bound(x, 1, 0). Check for short-circuit conditions before calling bound.
• All invariants pass but forge test still fails — there's a non-invariant test in the same file that's failing. Add --match-test invariant to scope.
• failed to set up invariant testing environment: No contracts to fuzz. — e.g. targetContract(address(handler)) was called before handler was instantiated, so it targeted address(0). Always new the Handler before calling targetContract.
• reverts: 12800 — every Handler call is reverting. Your bound(...) ranges are wrong, or your wrappers are passing through invalid inputs. Tighten the bounds or add early returns like wrappedWithdraw's.
• Invariant fails immediately on --match-contract — the invariant is wrong, not the contract. Write a single function test_X() that calls the operations manually and verify the arithmetic by hand before trusting the invariant.

Design retrospective

Three load-bearing decisions in the capstone's design:

1. Translate the core, label the additions. The part that carries the theorem — withdraw_shortfall → absorb, amount + unfilled == shortfall → absorbed + remaining == loss — is translated directly. Everything the EVM version adds (totals, owner, withdraw, reverts instead of no-ops) is called out as an addition. Being explicit about which parts are translated and which are new is what lets readers compare the two implementations honestly. A cross-language port is only checkable if its differences are written down.

2. Five ghosts, not four. The Handler tracks ghostSumLossRequested separately from ghostSumAbsorbed + ghostSumUnabsorbed so invariant 4 can prove their equality. A more compact design would track only the 4 invariant-relevant ghosts; the 5th ghost exists to make invariant 4 a meaningful assertion (not a tautology). The fifth ghost is the spec for invariant 4.

3. No vm.assume inside the Handler. All input bounding is done with bound(x, min, max) — every random parameter is mapped into a valid range, not filtered out. This keeps invariant testing's iteration count productive (no wasted iterations on rejections) and makes the test fast at scale. bound over vm.assume is the Handler-pattern discipline.

Answer key

After Lesson 6 the directory looks exactly like:

examples/foundry-capstone/
├── foundry.toml                              ← invariant config + pragma pin
├── src/
│   └── InsuranceFund.sol                     ← 51 lines, 3 ops + 5 fields
├── test/
│   ├── InsuranceFundHandler.sol              ← 57 lines, 3 wrappers + 5 ghosts
│   └── InsuranceFund.invariant.t.sol         ← 58 lines, 4 invariants
└── lib/forge-std/                            ← standard submodule

forge test --match-contract InsuranceFundInvariantTest prints 4 [PASS] lines with (runs: 256, calls: 12800, reverts: 0).

FOUNDRY_PROFILE=ci forge test --match-contract InsuranceFundInvariantTest does the same at runs: 2000, calls: 200000 per invariant.

Compare it with the four proptest! properties at the bottom of openhl's crates/liquidation/src/insurance.rs (commit 260883b), using the side-by-side table in Step 7.

Q&A

Q1: Why port to Solidity at all, instead of staying in Rust?

Different deployment surfaces. Rust + openhl is for chains where you control the execution environment (your own L1/L2). Solidity + invariant testing is for the EVM, where you have to compile to a fixed bytecode target. The capstone exists because production-deployable insurance funds on EVM chains (Aave's safety module, Compound's reserve, etc.) are Solidity — and the same conservation discipline applies. The port proves that the discipline is platform-agnostic; the deployment target dictates the language.

Q2: How do I know my port is correct and not just my own design?

Two cross-checks: (a) Break the same rule on both sides (for example, compute the Solidity remaining and the Rust unfilled with the same mistake) and check that the corresponding property fails in both. (b) The mapping table is the contract you compare against; any semantic difference that isn't listed there as an intentional addition or change is a porting bug. Mechanical correspondence is verifiable; "feeling right" is not.

Q3: Can I add more invariants?

Yes. The 4 here are a starting set. Real insurance funds add more: access-control invariants (only owner can withdraw), upper-bound invariants (total absorbed never exceeds total deposited - balance), rate-limit invariants (no more than X% withdrawn per Y blocks). Each follows the same shape: pick an observable, write an equality against ghost state, add to the invariant test. Invariants compound; the test file grows linearly with safety properties.

Q4: What does the examples/foundry-capstone/ directory ship with — committed code or template?

Committed working code. The directory is the course's answer key. New readers who complete Lesson 0–Lesson 5 can compare their own Lesson 6 work against this exact source. The capstone is a reference implementation; you build your own version following the walk-through, and the answer key is there for verification (or for skipping ahead if you're already comfortable). Committed reference implementations are how courses scale to multiple readers without each one needing instructor review.

Q5: Why isn't examples/foundry-capstone/ part of the lesson website's Next.js build?

It's a sub-project with its own foundry.toml and lib/forge-std. Including it in the Next.js build would require either pulling it into Vercel's deployment (waste of build time) or vendoring forge-std (waste of disk + git churn). The arrangement: the lessons are on the web; the executable artifact lives in the companion repository's examples/foundry-capstone/ sub-project. Readers clone the companion repository to run it. Web site for the curriculum; sub-project for the proof.

Q6: Can the same Handler pattern prove invariants against deployed contracts (forking + impersonation)?

Yes — that's the Lesson 5 + Lesson 6 synthesis. You can write an InvariantTest that uses --fork-url <mainnet> and points targetContract at a deployed Aave reserve. The Handler impersonates the reserve's role-holders via vm.prank and calls real methods. Your invariants then prove conservation laws against the actual deployed system, not against your local port. The capstone is a contained example; the same pattern scales to "prove invariants against real production contracts" — that's what the Lesson 5 forking work was setting up.

Q7: What happens to invariant testing when the fund is upgraded (proxy pattern)?

Invariants survive upgrades that preserve the public ABI and storage layout. If the upgrade changes either, the invariants must be updated to match. The pattern: store the invariant tests alongside the contract source; on every upgrade, re-run the full invariant suite against the new implementation. CI integration ensures no upgrade ships without re-proving the conservation laws. Invariants are part of the contract's specification; upgrades must preserve them or explicitly version them.

Course conclusion

This is the final lesson of this course. Six lessons in, you've moved from "what's a Foundry pragma" (Lesson 1) to "I just proved 4 conservation invariants against a Rust-to-Solidity port, mechanically, in 60 minutes." That's this course's thesis: discipline transfers across languages because the underlying math doesn't care which compiler runs it.

Where to go next:

• Run the capstone against more invariants. Add access-control, rate-limit, and upper-bound invariants to InsuranceFund.invariant.t.sol. Each one is ~3 lines of Solidity.
• Port one more component from openhl. Pick LiquidationScanner (crates/liquidation/src/scanner.rs) or the pure margin math in compute.rs from openhl-liquidation. Same pattern: identify state + operations + invariants, write the Solidity, prove with invariant testing.
• Apply the discipline to your own production code. Any contract you've written that has conservation-law-shaped properties (token balances, accumulating fees, vesting schedules) is a candidate. The Handler pattern + 1-line assertEq invariants scale to anything.
• Read openhl's liquidation crate (crates/liquidation/) one more time. Now that you've ported one component, the patterns will read differently. The proptest! macro will look like invariant_*, just in Rust.
• Read the openhl ADL course's capstone — the Rust-side sibling of this lesson. Its five invariant proptests carry the same conservation-law discipline across the whole cascade (scanner → insurance fund → ADL), with proptest! in Rust where this lesson uses invariant testing; it closes with the Stage 10 quartet retrospective. Read side by side, the two capstones show the discipline in both languages.

Foundry is a tool. The discipline is the product.

Summary (3 lines)

• Capstone = port openhl-liquidation Stage 10b's InsuranceFund (withdraw_shortfall → absorb, plus EVM-side totals / owner / withdraw) to Solidity, prove four conservation-law invariants via invariant testing (12,800 calls per invariant by default, 200,000 in the CI profile). End of the discipline-transfer arc.
• Test harness has three pieces: InsuranceFund.sol + InsuranceFundHandler (five ghost variables) + InsuranceFundInvariantTest (targetContract + four invariant_*). Solidity 0.8 checked arithmetic replaces Rust's saturating add.
• All four invariants pass; invariant 4 is the sequence-level form of the liquidation course's withdraw_shortfall lesson's amount + unfilled == shortfall. The companion repository's examples/foundry-capstone/ is the answer key. Discipline transfer complete.