Add formal verification for ERC-4626

fv/harnesses/ERC4626Harness.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.24;
+
+import {ERC4626, ERC20, IERC20} from "../patched/token/ERC20/extensions/ERC4626.sol";
+
+contract ERC4626Harness is ERC4626 {
+    constructor(IERC20 asset_, string memory name_, string memory symbol_) ERC20(name_, symbol_) ERC4626(asset_) {}
+
+    /// @dev Not part of ERC-4626. Models an asset donation: an external actor sending assets to the vault without
+    /// minting shares. Present so parametric rules and invariants range over it.
+    function donate(uint256 assets) public {
+        _transferIn(_msgSender(), assets);
+    }
+}

fv/harnesses/ERC4626OffsetHarness.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.24;
+
+import {ERC4626, ERC20, IERC20} from "../patched/token/ERC20/extensions/ERC4626.sol";
+
+/// @dev ERC4626Harness with the decimals offset left symbolic instead of pinned to zero. The offset
+/// is an immutable the prover treats as an unconstrained constant, so rules verified here hold for
+/// every offset a deployment could choose, not just the default.
+contract ERC4626OffsetHarness is ERC4626 {
+    uint8 private immutable _offset;
+
+    constructor(
+        IERC20 asset_,
+        string memory name_,
+        string memory symbol_,
+        uint8 offset_
+    ) ERC20(name_, symbol_) ERC4626(asset_) {
+        _offset = offset_;
+    }
+
+    function _decimalsOffset() internal view override returns (uint8) {
+        return _offset;
+    }
+
+    /// @dev Exposed so rules can constrain the offset and state the range they hold over.
+    function decimalsOffset() public view returns (uint8) {
+        return _offset;
+    }
+
+    /// @dev The virtual share supply, 10**offset. Exposed so rules can state bounds in terms of the
+    /// quantity the conversions actually use, rather than re-deriving the exponentiation in CVL.
+    function virtualShares() public view returns (uint256) {
+        return 10 ** _decimalsOffset();
+    }
+
+    /// @dev Not part of ERC-4626. Models an asset donation: an external actor sending assets to the
+    /// vault without minting shares. Present so parametric rules and invariants range over it.
+    function donate(uint256 assets) public {
+        _transferIn(_msgSender(), assets);
+    }
+}

fv/specs/ERC4626.conf

@@ -0,0 +1,24 @@
+{
+    "build_cache": true,
+    "exclude_rule": [
+        "depositIsNotSplittable",
+        "withdrawIsNotSplittable",
+        "holdingBackAcrossDonationDoesNotPay"
+    ],
+    "files": [
+        "fv/harnesses/ERC4626Harness.sol"
+    ],
+    "global_timeout": 600,
+    "msg": "ERC4626 tier 1: everything but the anti-splitting rules",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/contracts=fv/patched"
+    ],
+    "parametric_contracts": [
+        "ERC4626Harness"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "url_visibility": "public",
+    "verify": "ERC4626Harness:fv/specs/ERC4626.spec"
+}

fv/specs/ERC4626Base.spec

@@ -0,0 +1,76 @@
+// Shared base for the ERC4626 suite: the summary layer plus the scope definitions. Every summary
+// the suite relies on is declared here, so what is assumed here is assumed by every config.
+//
+// ASSUMED, NOT PROVED. Every rule in this suite is conditional on all of the following:
+//   - Math.mulDiv is replaced by a closed form, so rules are conditional on that form matching the
+//     implementation in both value and revert domain. Only the 4-argument overload is bound; it is
+//     the only one ERC4626 calls.
+//   - The underlying asset has no contract in the scene. Its balances and allowances are ghost
+//     state, which under-approximates real tokens: no fee-on-transfer, no rebase-down, no ERC-777
+//     reentrancy.
+//   - _decimalsOffset() is 0 in ERC4626Harness, so nothing verified against it generalizes to a
+//     larger offset. ERC4626Offset.spec proves solvency and the donation attack against a harness
+//     whose offset is symbolic; every other result in the suite is a zero-offset result.
+//   - optimistic_loop is set on every config, so loops are assumed to terminate within the bound.
+//
+// Parametric rules range over the harness, which adds a non-production donate() and deliberately
+// exposes no share mint or burn. Both are part of the claim: a raw asset inflow is the inflation
+// attack's vector and no parametric rule over the production contract can reach it, while an
+// unbacked mint would falsify rate monotonicity.
+//
+// Rules that are not proved at all are marked NOT PROVED where they are declared, with the command
+// to re-attempt them.
+
+import "helpers/helpers.spec";
+import "helpers/math-cvl.spec";
+import "helpers/erc20-cvl.spec";
+
+methods {
+    // ---- shares token (the vault itself) ----
+    function totalSupply()                external returns (uint256) envfree;
+    function balanceOf(address)           external returns (uint256) envfree;
+    function allowance(address,address)   external returns (uint256) envfree;
+
+    // ---- vault views ----
+    function asset()                      external returns (address) envfree;
+    function totalAssets()                external returns (uint256) envfree;
+    function convertToShares(uint256)     external returns (uint256) envfree;
+    function convertToAssets(uint256)     external returns (uint256) envfree;
+    function maxDeposit(address)          external returns (uint256) envfree;
+    function maxMint(address)             external returns (uint256) envfree;
+    function maxWithdraw(address)         external returns (uint256) envfree;
+    function maxRedeem(address)           external returns (uint256) envfree;
+    function previewDeposit(uint256)      external returns (uint256) envfree;
+    function previewMint(uint256)         external returns (uint256) envfree;
+    function previewWithdraw(uint256)     external returns (uint256) envfree;
+    function previewRedeem(uint256)       external returns (uint256) envfree;
+
+    // ---- summaries ----
+    // Trusted, not proved. ERC4626 only calls this overload, so summarizing it bypasses Math
+    // entirely; the 3-arg overload is left unbound because it would never fire.
+    function _.mulDiv(uint256 x, uint256 y, uint256 d, Math.Rounding r) internal
+        => mulDivCVL(x, y, d, r) expect uint256;
+
+    // Asset token, modelled as ghost state. See erc20-cvl.spec for what this leaves out.
+    function _.safeTransfer(address token, address to, uint256 v) internal
+        => safeTransferCVL(token, executingContract, to, v) expect void;
+    function _.safeTransferFrom(address token, address from, address to, uint256 v) internal
+        => safeTransferFromCVL(token, executingContract, from, to, v) expect void;
+    function _.balanceOf(address account) external
+        => balanceByToken[calledContract][account] expect uint256;
+
+    // Constructor-only. Feeds _underlyingDecimals, which only decimals() reads and no rule here does.
+    function _.tryGetDecimals(address token) internal
+        => tryGetDecimalsCVL() expect (bool, uint8);
+}
+
+/// Scope assumptions, applied by every rule. A vault whose asset is itself, or the zero address, is
+/// not a configuration this suite reasons about.
+definition sane() returns bool = asset() != currentContract && asset() != 0;
+
+/// The virtual-asset design computes totalAssets() + 1 and totalSupply() + 10**offset, so a vault
+/// holding the entire uint256 range reverts in every conversion. Value rules prune that state on
+/// their own, because the preview call they compare against is the thing that reverts. Liveness
+/// rules cannot rely on that and must exclude it by name.
+definition noVirtualOverflow() returns bool =
+    totalAssets() < max_uint256 && totalSupply() < max_uint256;

fv/specs/ERC4626Donation.conf

@@ -0,0 +1,23 @@
+{
+    "build_cache": true,
+    "files": [
+        "fv/harnesses/ERC4626Harness.sol"
+    ],
+    "global_timeout": 1800,
+    "msg": "ERC4626 tier 3: donation attack non-profitability",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/contracts=fv/patched"
+    ],
+    "parametric_contracts": [
+        "ERC4626Harness"
+    ],
+    "process": "emv",
+    "prover_args": [
+        "-smt_useLIA false -smt_useNIA true -splitParallel true -dontStopAtFirstSplitTimeout true -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+    ],
+    "rule_sanity": "basic",
+    "smt_timeout": "1200",
+    "url_visibility": "public",
+    "verify": "ERC4626Harness:fv/specs/ERC4626Donation.spec"
+}

fv/specs/ERC4626Donation.spec

@@ -0,0 +1,52 @@
+// Kept out of ERC4626.spec so its tuned solver settings do not slow the tier-1 sweep.
+//
+// Verified by two configs: ERC4626Donation.conf against the zero-offset harness and
+// ERC4626OffsetDonation.conf against the symbolic-offset one. Nothing here mentions the offset.
+
+import "ERC4626Base.spec";
+import "helpers/erc20-supply.spec";
+
+/*
+┌────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ P7: the donation attack is not profitable against a fresh vault                                    │
+└────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+/// The inflation attack: enter, inflate the share price with a donation, let a victim deposit at the
+/// manipulated rate, exit. Asserting the attacker's asset balance never rises across the sequence
+/// captures "never profits" in one assertion, with no separate accounting of what they paid.
+///
+/// Scoped to a vault that starts empty: that is what the virtual-shares mitigation claims, and the
+/// only scope in which the claim is true. An arbitrary (totalSupply, totalAssets) start admits states
+/// that are already manipulated - one share outstanding against a large asset balance - where an
+/// attacker profits without donating anything. ERC4626 documents that empty and nearly-empty vaults
+/// are the hazard and directs deployers to seed them.
+///
+/// Because totalSupply starts at zero, the attacker starts with no shares, so redeeming their whole
+/// balance redeems only what this sequence minted.
+rule donationAttackNeverProfits(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) {
+    require sane();
+    require nonpayable(eAtt) && nonpayable(eVic);
+    require noVirtualOverflow();
+    // Proved by ERC4626.conf for the zero-offset harness and ERC4626Offset.conf for the offset one.
+    requireInvariant totalSupplyIsSumOfBalances();
+
+    address attacker = eAtt.msg.sender;
+    address victim   = eVic.msg.sender;
+    address token    = asset();
+    require attacker != victim;
+    require attacker != currentContract && victim != currentContract;
+    require attacker != 0 && victim != 0;
+
+    // A fresh vault: no shares outstanding and no assets held.
+    require totalSupply() == 0 && totalAssets() == 0;
+
+    mathint attackerAssetsBefore = balanceByToken[token][attacker];
+
+    deposit(eAtt, a1, attacker);                            // attacker enters
+    donate(eAtt, d);                                        // inflate the rate
+    deposit(eVic, a2, victim);                              // victim deposits at the new rate
+    redeem(eAtt, balanceOf(attacker), attacker, attacker);  // attacker exits fully
+
+    assert balanceByToken[token][attacker] <= attackerAssetsBefore;
+}

fv/specs/ERC4626Offset.conf

@@ -0,0 +1,19 @@
+{
+    "build_cache": true,
+    "files": [
+        "fv/harnesses/ERC4626OffsetHarness.sol"
+    ],
+    "global_timeout": 600,
+    "msg": "ERC4626 tier 4: symbolic decimals offset",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/contracts=fv/patched"
+    ],
+    "parametric_contracts": [
+        "ERC4626OffsetHarness"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "url_visibility": "public",
+    "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Offset.spec"
+}

fv/specs/ERC4626Offset.spec

@@ -0,0 +1,86 @@
+// Tier 4: the decimals offset left symbolic.
+//
+// Every other spec in this suite runs against a harness whose _decimalsOffset() is 0, so K = 1 in
+// both conversion denominators and nothing proved there generalizes. Here the offset is an
+// immutable the prover leaves unconstrained, so K = 10**offset is a symbolic exponentiation. No rule
+// abstracts it behind a ghost or needs the offset bounded, so this tier carries no assumption the
+// rest of the suite does not.
+//
+// Offsets from 78 up make 10**offset overflow uint256, so every conversion reverts and the prover
+// prunes those paths. The rules here are claims about offsets 0 through 77.
+//
+// The donation attack is also re-proved at a symbolic offset: ERC4626OffsetDonation.conf points the
+// unchanged ERC4626Donation.spec at this file's harness.
+
+import "ERC4626Base.spec";
+import "helpers/erc20-supply.spec";
+
+// ERC4626OffsetDonation.conf assumes this invariant, so it is proved here for the offset harness.
+// Its Sload hook bounds every balance read; no rule below reads one.
+use invariant totalSupplyIsSumOfBalances;
+
+methods {
+    function decimalsOffset() external returns (uint8) envfree;
+    function virtualShares()  external returns (uint256) envfree;
+}
+
+/*
+┌────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Vacuity guard: the offset is genuinely symbolic, and a live vault is reachable at a nonzero one    │
+└────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+/// rule_sanity cannot catch this: every rule below is satisfiable at offset 0 alone, which would
+/// make the tier a restatement of what the zero-offset harness already proves.
+rule offsetIsGenuinelySymbolic(uint256 shares) {
+    require sane();
+    require decimalsOffset() > 0;
+    require totalSupply() > 0 && totalAssets() > 0;
+    satisfy previewRedeem(shares) > 0;
+}
+
+/*
+┌────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ P1: the vault is never over-committed - every outstanding share is redeemable simultaneously       │
+└────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+/// Holds in every state, with no assumption about how that state was reached, so this is stated as a
+/// rule rather than an invariant: quantifying over all sane states is stronger than quantifying over
+/// reachable ones.
+///
+/// With K = 10^offset >= 1, previewRedeem(T) = floor(T(A+1)/(T+K)), and floor(x) <= A iff x < A+1,
+/// so the obligation reduces to T(A+1) < (A+1)(T+K), i.e. 0 < (A+1)K. True for all T, A and K >= 1
+/// with no relationship between T and A, which is why induction is unnecessary. The bound is not
+/// trivially tight: equality (T = A = 0) and strict inequality are both reachable.
+///
+/// Proved here rather than on the zero-offset harness because the argument is offset-independent
+/// only on paper; this is the harness on which the prover checks it for every K.
+rule vaultNeverOvercommitted() {
+    require sane();
+    assert previewRedeem(totalSupply()) <= totalAssets();
+}
+
+/*
+┌────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ What the offset is FOR: it prices the inflation attack, and only a symbolic offset can say so      │
+└────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+/// ERC4626 does not claim the virtual shares prevent the inflation attack; it claims they make it
+/// "orders of magnitude more expensive than it is profitable". That is a claim about a quantity, and
+/// it is invisible to any rule that pins the quantity to 1.
+///
+/// A victim is only robbed if their deposit rounds to zero shares, and
+/// previewDeposit(a) = floor(a(T+K)/(A+1)) is zero only when a(T+K) < A+1. With K = 10^offset and
+/// T >= 0 that forces A >= a*K: for a deposit of a to mint nothing, the vault must already hold at
+/// least a * 10^offset assets, so the attack costs 10^offset times what it takes from the victim.
+///
+/// The bound is tight (A = a*K is reachable) and degrades to the trivially true A >= a at offset 0.
+/// It is violated by a mutation that drops the offset from the share conversion.
+rule inflationCostScalesWithOffset(uint256 assets) {
+    require sane();
+    require assets > 0;
+    require previewDeposit(assets) == 0;
+    assert to_mathint(totalAssets()) >= to_mathint(assets) * to_mathint(virtualShares());
+}

fv/specs/ERC4626OffsetDonation.conf

@@ -0,0 +1,23 @@
+{
+    "build_cache": true,
+    "files": [
+        "fv/harnesses/ERC4626OffsetHarness.sol"
+    ],
+    "global_timeout": 1800,
+    "msg": "ERC4626 tier 4: donation attack at a symbolic decimals offset",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/contracts=fv/patched"
+    ],
+    "parametric_contracts": [
+        "ERC4626OffsetHarness"
+    ],
+    "process": "emv",
+    "prover_args": [
+        "-smt_useLIA false -smt_useNIA true -splitParallel true -dontStopAtFirstSplitTimeout true -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+    ],
+    "rule_sanity": "basic",
+    "smt_timeout": "1200",
+    "url_visibility": "public",
+    "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Donation.spec"
+}

fv/specs/ERC4626_split.conf

@@ -0,0 +1,26 @@
+{
+    "build_cache": true,
+    "files": [
+        "fv/harnesses/ERC4626Harness.sol"
+    ],
+    "global_timeout": 900,
+    "independent_satisfy": true,
+    "msg": "ERC4626 anti-splitting shard: nonlinear share math, splitting off, seed race",
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin/contracts=fv/patched"
+    ],
+    "parametric_contracts": [
+        "ERC4626Harness"
+    ],
+    "process": "emv",
+    "prover_args": [
+        "-destructiveOptimizations twostage -backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+    ],
+    "rule": [
+        "depositIsNotSplittable"
+    ],
+    "rule_sanity": "basic",
+    "url_visibility": "public",
+    "verify": "ERC4626Harness:fv/specs/ERC4626.spec"
+}