From ffc2c474413211b79bbe354f70916cdb16f69254 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 24 Aug 2026 21:54:50 -0300 Subject: [PATCH 01/20] fv: add ERC4626 harness skeleton CVL syntax spike (certora-cli 8.18.0 local; CI pin 8.6.1 untested): - Q1 tuple-return summary: syntax OK, binding not load-bearing (ledger A3) - Q2 Math.Rounding as CVL param + assert_uint8: works - Q3 wildcard summary on library internal fn: works Q3 was proved by sentinel rather than by typecheck: a summary naming a function that exists nowhere typechecks with exit 0 and no warning, so only a rule that fails when the binding is absent actually answers it. Prover: https://prover.certora.com/output/1392759/75136955b8c64624beeedc3c439083c7 Co-Authored-By: Claude Opus 5 (1M context) --- fv/harnesses/ERC4626Harness.sol | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 fv/harnesses/ERC4626Harness.sol diff --git a/fv/harnesses/ERC4626Harness.sol b/fv/harnesses/ERC4626Harness.sol new file mode 100644 index 00000000000..13feeb12177 --- /dev/null +++ b/fv/harnesses/ERC4626Harness.sol @@ -0,0 +1,16 @@ +// 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 external actor sending assets to the vault without minting shares (a + /// "donation"). Present so parametric rules and invariants range over it. Routes through {ERC4626-_transferIn} so + /// the ghost-backed asset accounting in fv/specs/helpers/erc20-cvl.spec stays consistent. + function donate(uint256 assets) public { + _transferIn(_msgSender(), assets); + } +} From 548fe168699fb3dcba564da5ce185dfd22608562 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 24 Aug 2026 22:22:29 -0300 Subject: [PATCH 02/20] fv: add ERC4626 summary layer and smoke rules Ghost-backed asset model and mulDiv closed form, activated in a leaf base spec. Harness adds donate() to model unbacked asset inflows; deliberately exposes no share mint/burn, since an unbacked share mint is what the solvency and rate-monotonicity properties forbid. Prover: https://prover.certora.com/output/1392759/06cda2c815be46cda4f0e7daaa8c3e25 Co-Authored-By: Claude Opus 5 (1M context) --- fv/harnesses/ERC4626Harness.sol | 5 ++-- fv/specs/ERC4626.conf | 16 ++++++++++++ fv/specs/ERC4626.spec | 17 ++++++++++++ fv/specs/ERC4626Base.spec | 46 +++++++++++++++++++++++++++++++++ fv/specs/helpers/erc20-cvl.spec | 34 ++++++++++++++++++++++++ fv/specs/helpers/math-cvl.spec | 28 ++++++++++++++++++++ 6 files changed, 143 insertions(+), 3 deletions(-) create mode 100644 fv/specs/ERC4626.conf create mode 100644 fv/specs/ERC4626.spec create mode 100644 fv/specs/ERC4626Base.spec create mode 100644 fv/specs/helpers/erc20-cvl.spec create mode 100644 fv/specs/helpers/math-cvl.spec diff --git a/fv/harnesses/ERC4626Harness.sol b/fv/harnesses/ERC4626Harness.sol index 13feeb12177..2781fd4d625 100644 --- a/fv/harnesses/ERC4626Harness.sol +++ b/fv/harnesses/ERC4626Harness.sol @@ -7,9 +7,8 @@ import {ERC4626, ERC20, IERC20} from "../patched/token/ERC20/extensions/ERC4626. 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 external actor sending assets to the vault without minting shares (a - /// "donation"). Present so parametric rules and invariants range over it. Routes through {ERC4626-_transferIn} so - /// the ghost-backed asset accounting in fv/specs/helpers/erc20-cvl.spec stays consistent. + /// @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); } diff --git a/fv/specs/ERC4626.conf b/fv/specs/ERC4626.conf new file mode 100644 index 00000000000..4f631d88a53 --- /dev/null +++ b/fv/specs/ERC4626.conf @@ -0,0 +1,16 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 600, + "msg": "ERC4626 tiers 1-2", + "optimistic_loop": true, + "parametric_contracts": [ + "ERC4626Harness" + ], + "process": "emv", + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626Harness:fv/specs/ERC4626.spec" +} diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec new file mode 100644 index 00000000000..be0eff61c4d --- /dev/null +++ b/fv/specs/ERC4626.spec @@ -0,0 +1,17 @@ +import "ERC4626Base.spec"; + +// Checks that every contract function has at least one non-reverting path. A function that always +// reverts makes every rule calling it vacuous, with no `require` involved. +use builtin rule sanity; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Vacuity guard: if the scope assumptions are unsatisfiable, every rule below passes for free │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule setupIsSatisfiable(env e, uint256 assets, address receiver) { + require sane(); + require nonpayable(e); + deposit(e, assets, receiver); + satisfy true; +} diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec new file mode 100644 index 00000000000..9673882b836 --- /dev/null +++ b/fv/specs/ERC4626Base.spec @@ -0,0 +1,46 @@ +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 deliberately 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; diff --git a/fv/specs/helpers/erc20-cvl.spec b/fv/specs/helpers/erc20-cvl.spec new file mode 100644 index 00000000000..fd0565f87e0 --- /dev/null +++ b/fv/specs/helpers/erc20-cvl.spec @@ -0,0 +1,34 @@ +// Ghost-backed model of the underlying asset token. Definitions only - no methods block. +// +// The asset has no contract in the scene, so its balances live entirely in ghost state. This +// under-approximates real tokens: no fee-on-transfer, no rebase-down, no ERC-777 reentrancy. + +/// token => account => balance +ghost mapping(address => mapping(address => uint256)) balanceByToken; +/// token => owner => spender => allowance +ghost mapping(address => mapping(address => mapping(address => uint256))) allowanceByToken; + +function revertOn(bool b) { if (b) { revert(); } } + +/// SafeERC20 reverts on failure, so these model a revert rather than a false return. +/// require_uint256 on the credit side neglects overflow of the receiving balance; the vault's own +/// balance is bounded by the solvency invariant. Revisit if a counterexample ever turns on it. +function safeTransferCVL(address token, address from, address to, uint256 amount) { + revertOn(balanceByToken[token][from] < amount); + balanceByToken[token][from] = require_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); +} + +function safeTransferFromCVL(address token, address spender, address from, address to, uint256 amount) { + revertOn(allowanceByToken[token][from][spender] < amount); + safeTransferCVL(token, from, to, amount); + allowanceByToken[token][from][spender] = + require_uint256(allowanceByToken[token][from][spender] - amount); +} + +function tryGetDecimalsCVL() returns (bool, uint8) { + return (true, 18); +} + +/// Exchange-rate probe. One share at 18 decimals. +definition ONE_SHARE() returns uint256 = 1000000000000000000; diff --git a/fv/specs/helpers/math-cvl.spec b/fv/specs/helpers/math-cvl.spec new file mode 100644 index 00000000000..009d7eee4e3 --- /dev/null +++ b/fv/specs/helpers/math-cvl.spec @@ -0,0 +1,28 @@ +// Closed-form model of Math.mulDiv. Definitions only - no methods block, so this file is safe to +// import anywhere. Activation lives in ERC4626Base.spec. +// +// Adapted from Certora's AutoProver summaries for 512-bit mulDiv. Trusted, not proved: rules that +// rely on it are conditional on this matching Math.mulDiv in both value and revert domain. + +function mulDivDownSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = x * y / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function mulDivUpSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = (x * y + denominator - 1) / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +/// Mirrors Math.unsignedRoundsUp over Math.Rounding { Floor, Ceil, Trunc, Expand }. +definition roundsUpCVL(Math.Rounding r) returns bool = assert_uint8(r) % 2 == 1; + +function mulDivCVL(uint256 x, uint256 y, uint256 d, Math.Rounding rounding) returns uint256 { + return roundsUpCVL(rounding) ? mulDivUpSummary(x, y, d) : mulDivDownSummary(x, y, d); +} From 631ad6831b6033e5d39e61a5da0136a5eaa6eb88 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 24 Aug 2026 23:39:00 -0300 Subject: [PATCH 03/20] fv: add ERC4626 solvency property (P1) previewRedeem(totalSupply()) <= totalAssets(), stated as a rule rather than an invariant. The property needs no induction: it holds in every state with no relation between totalSupply and totalAssets, since floor(x) <= A iff x < A+1 reduces the obligation to 0 < (A+1)K. Quantifying over all sane states is both stronger than quantifying over reachable ones and far cheaper - as an invariant it returned UNKNOWN on every method. Also adds the shared sum-of-balances ghost. Note that importing a spec makes its invariants assumable but not proved; `use invariant` is what proves them. Verified: https://prover.certora.com/output/1392759/aa28b0f58dd74d49a4bfe3e5138f703a Mutation (_convertToAssets forced to Ceil) correctly VIOLATED: https://prover.certora.com/output/1392759/400c3aee9dad44289661bb075a8a28d4 Co-Authored-By: Claude Opus 5 (1M context) --- fv/specs/ERC4626.spec | 23 +++++++++++++++++++++++ fv/specs/helpers/erc20-supply.spec | 23 +++++++++++++++++++++++ 2 files changed, 46 insertions(+) create mode 100644 fv/specs/helpers/erc20-supply.spec diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index be0eff61c4d..774a419f9eb 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -1,9 +1,13 @@ import "ERC4626Base.spec"; +import "helpers/erc20-supply.spec"; // Checks that every contract function has at least one non-reverting path. A function that always // reverts makes every rule calling it vacuous, with no `require` involved. use builtin rule sanity; +// Proves the imported sum-of-balances invariant here, rather than only assuming it. +use invariant totalSupplyIsSumOfBalances; + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Vacuity guard: if the scope assumptions are unsatisfiable, every rule below passes for free │ @@ -15,3 +19,22 @@ rule setupIsSatisfiable(env e, uint256 assets, address receiver) { deposit(e, assets, receiver); satisfy true; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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: it needs no induction, and quantifying over all sane states is +/// stronger than quantifying over reachable ones. +/// +/// Independent of the decimals offset: 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 - note this needs no +/// relationship between T and A, which is exactly why induction is unnecessary. +rule vaultNeverOvercommitted() { + require sane(); + assert previewRedeem(totalSupply()) <= totalAssets(); +} diff --git a/fv/specs/helpers/erc20-supply.spec b/fv/specs/helpers/erc20-supply.spec new file mode 100644 index 00000000000..c20a73de1a3 --- /dev/null +++ b/fv/specs/helpers/erc20-supply.spec @@ -0,0 +1,23 @@ +// Sum-of-balances ghost for the shares token, extracted so several ERC4626 specs can share it. +// +// ERC20.spec keeps its own copy and is deliberately not imported here: its methods block requires +// mint and burn on the verification target, and exposing unbacked share mint on an ERC4626 harness +// would falsify the solvency and rate-monotonicity properties. + +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} + +// Bounds a balance by the tracked sum. Without it, explicit casting admits a pre-state where one +// balance exceeds totalSupply and overflows on receipt - reachable only by deploying into a dirty +// address. +hook Sload uint256 balance _balances[KEY address addr] { + require sumOfBalances >= to_mathint(balance); +} + +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { + sumOfBalances = sumOfBalances - oldValue + newValue; +} + +invariant totalSupplyIsSumOfBalances() + to_mathint(totalSupply()) == sumOfBalances; From 1c1d1b859d3b9380001c2ba506a03c0cf2df47e3 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 02:40:29 -0300 Subject: [PATCH 04/20] fv: add ERC4626 round-trip and rounding-gap rules (P2) No round trip creates value, and per-operation leakage is bounded at one unit in both directions. The bounds are paired with reachability witnesses, without which `gap <= 1` would be satisfied by a gap that is always zero. Prover run: https://prover.certora.com/output/1392759/1e8a438118444bd7aff1755d2589b57d?anonymousKey=b2b0e29a4f1e586b4eecaa73d5fd247f1c96c407 --- fv/specs/ERC4626.spec | 46 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 774a419f9eb..9e1661b74bb 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -38,3 +38,49 @@ rule vaultNeverOvercommitted() { require sane(); assert previewRedeem(totalSupply()) <= totalAssets(); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P2: round trips never create value, and per-operation leakage is at most one unit │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The no-free-money half. Both directions of a round trip are stated on the preview functions, so +/// this holds for every state rather than only the ones a deposit could reach. +rule roundTripNeverCreatesValue(uint256 assets) { + require sane(); + + // Deposit then redeem never returns more than was put in. + assert previewRedeem(previewDeposit(assets)) <= assets; + // Withdraw then re-mint never costs less than was taken out. + assert previewMint(previewWithdraw(assets)) >= assets; +} + +/// The tightness half. Bounding leakage at one unit is worth far more than a vague `>=`, and it +/// catches a preview override whose rounding direction is transposed, which ERC4626 warns about: +/// overrides to the deposit or withdraw mechanism must be reflected in the preview functions. +/// +/// previewWithdraw and previewDeposit are the same conversion at Ceil and Floor, as are previewMint +/// and previewRedeem, so each gap is a ceil-minus-floor and lands in {0, 1}. +rule roundingGapIsAtMostOne(uint256 assets, uint256 shares) { + require sane(); + + mathint depositGap = previewWithdraw(assets) - previewDeposit(assets); + mathint mintGap = previewMint(shares) - previewRedeem(shares); + + assert depositGap >= 0 && depositGap <= 1; + assert mintGap >= 0 && mintGap <= 1; +} + +/// Witnesses that the bounds above are reachable. Mandatory: `assert gap <= 1` is trivially true of +/// a gap that is always zero, and rule_sanity cannot flag it because the assertion is reached. Kept +/// as separate rules so neither witness can be weakened by sharing a path with the other. +rule depositGapCanBeOne(uint256 assets) { + require sane(); + satisfy previewWithdraw(assets) - previewDeposit(assets) == 1; +} + +rule mintGapCanBeOne(uint256 shares) { + require sane(); + satisfy previewMint(shares) - previewRedeem(shares) == 1; +} From 9f5875ea01995fce60179b452015d59be9a2b4a6 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 02:57:54 -0300 Subject: [PATCH 05/20] fv: add ERC4626 max/preview boundary rules (P3) The max functions agree with the previews, and the limits they advertise are actually reachable: redeem(maxRedeem(o)) and withdraw(maxWithdraw(o)) never revert. Both liveness rules fix owner == msg.sender, so the claim covers self-withdrawals only; the allowance path is left to the conservation rules. Adds a noVirtualOverflow scope definition. The virtual-asset design computes totalAssets() + 1, which reverts when the vault holds the whole uint256 range. Stated on both liveness rules rather than only the one that needs it, so neither relies on a preview call reverting to prune the state for it. Prover run: https://prover.certora.com/output/1392759/46832ab7c6954ba1a471aa24de45b09f?anonymousKey=efa79148b605bc5e1b24e6f092a3f3cb23f65747 --- fv/specs/ERC4626.spec | 54 +++++++++++++++++++++++++++++++++++++++ fv/specs/ERC4626Base.spec | 7 +++++ 2 files changed, 61 insertions(+) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 9e1661b74bb..8f1b42e114c 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -84,3 +84,57 @@ rule mintGapCanBeOne(uint256 shares) { require sane(); satisfy previewMint(shares) - previewRedeem(shares) == 1; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P3: the max/preview boundary - what the limits promise, the operations honour │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// maxWithdraw floors on the way out while previewWithdraw ceils on the way back, so it is not +/// obvious the round trip stays inside the owner's share balance. It does: m = floor(b(A+1)/(T+K)) +/// gives m(T+K)/(A+1) <= b, and b is an integer, so ceil(m(T+K)/(A+1)) <= b. That is what keeps +/// withdraw(maxWithdraw(o)) from reverting on the burn, which is why the third assertion carries +/// the weight of P3. +rule maxBoundaryIsConsistent(address owner) { + require sane(); + requireInvariant totalSupplyIsSumOfBalances(); + + assert maxRedeem(owner) == balanceOf(owner); + assert maxWithdraw(owner) == previewRedeem(maxRedeem(owner)); + assert previewWithdraw(maxWithdraw(owner)) <= balanceOf(owner); +} + +/// Liveness: the advertised limit is actually reachable. No invariant catches this - a max() that +/// over-promises leaves every value rule green while the operation reverts. +/// +/// Both rules fix owner == msg.sender, so no allowance is spent and the claim is narrowed to +/// self-withdrawals; the allowance path belongs to the conservation rules. msg.sender must be +/// nonzero because burning from the zero address reverts regardless of amount. +/// +/// noVirtualOverflow is stated on both, though only redeem needs it to pass: withdraw reaches the +/// same state through maxWithdraw, whose own revert prunes the path before the assertion. Assuming +/// it explicitly keeps the two rules covering the same states. +rule redeemMaxNeverReverts(env e, address receiver) { + require sane(); + require nonpayable(e); + require nonzerosender(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + redeem@withrevert(e, maxRedeem(owner), receiver, owner); + assert !lastReverted; +} + +rule withdrawMaxNeverReverts(env e, address receiver) { + require sane(); + require nonpayable(e); + require nonzerosender(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + withdraw@withrevert(e, maxWithdraw(owner), receiver, owner); + assert !lastReverted; +} diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec index 9673882b836..7aac7fe7b94 100644 --- a/fv/specs/ERC4626Base.spec +++ b/fv/specs/ERC4626Base.spec @@ -44,3 +44,10 @@ methods { /// 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; From f0bd86e41494fcc73df86c2c155e2c67d868ed18 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 03:12:44 -0300 Subject: [PATCH 06/20] fv: add ERC4626 conservation and isolation rules One rule per state-changer: share and asset deltas, allowance spend on the third-party path, and isolation against a free `other` parameter the prover quantifies over universally. Supporting machinery for the value properties, which all assume the operations move the right amounts between the right parties. Previews are read before the operation, since afterwards the operation has moved both sides of the conversion. The allowance assertions treat infinite approval separately, which ERC20 leaves untouched by design. Prover run: https://prover.certora.com/output/1392759/6e66a0d667e945f4b5f5962aa71ac6de?anonymousKey=b5a8cc0780bb79eb02256ee7fed7a386ad74c5bd --- fv/specs/ERC4626.spec | 159 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 8f1b42e114c..9576887cc39 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -138,3 +138,162 @@ rule withdrawMaxNeverReverts(env e, address receiver) { withdraw@withrevert(e, maxWithdraw(owner), receiver, owner); assert !lastReverted; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Conservation and isolation: the state-changers move exactly what they claim, and nothing else │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Supporting machinery rather than a headline property. The value properties all assume the +/// operations move the right amounts between the right parties; without these they can pass for the +/// wrong reason. +/// +/// `other` is a free rule parameter, so the prover quantifies over it universally. That is what +/// makes the isolation assertions meaningful with no disequality assumption and with no way to go +/// vacuous - a fresh symbol pinned by a `require` would give neither. +/// +/// Every preview is read before the operation. Read afterwards it would be a different number, +/// since the operation moves both sides of the conversion. +rule depositConserves(env e, uint256 assets, address receiver, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0; + + mathint expectedShares = previewDeposit(assets); + mathint supplyBefore = totalSupply(); + mathint receiverSharesBefore = balanceOf(receiver); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint callerAssetsBefore = balanceByToken[token][caller]; + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 shares = deposit(e, assets, receiver); + + // effects: shares credited match the preview, assets moved match the request + assert to_mathint(shares) == expectedShares; + assert to_mathint(totalSupply()) == supplyBefore + shares; + assert to_mathint(balanceOf(receiver)) == receiverSharesBefore + shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore + assets; + assert balanceByToken[token][caller] == callerAssetsBefore - assets; + + // isolation: nobody else moved + assert balanceOf(other) != otherSharesBefore => other == receiver; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == caller || other == currentContract); +} + +rule mintConserves(env e, uint256 shares, address receiver, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0; + + mathint expectedAssets = previewMint(shares); + mathint supplyBefore = totalSupply(); + mathint receiverSharesBefore = balanceOf(receiver); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint callerAssetsBefore = balanceByToken[token][caller]; + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 assets = mint(e, shares, receiver); + + assert to_mathint(assets) == expectedAssets; + assert to_mathint(totalSupply()) == supplyBefore + shares; + assert to_mathint(balanceOf(receiver)) == receiverSharesBefore + shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore + assets; + assert balanceByToken[token][caller] == callerAssetsBefore - assets; + + assert balanceOf(other) != otherSharesBefore => other == receiver; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == caller || other == currentContract); +} + +/// Covers the third-party allowance path that the P3 liveness rules deliberately scoped out. +rule withdrawConserves(env e, uint256 assets, address receiver, address owner, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0 && receiver != currentContract; + + mathint expectedShares = previewWithdraw(assets); + mathint supplyBefore = totalSupply(); + mathint ownerSharesBefore = balanceOf(owner); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint recvAssetsBefore = balanceByToken[token][receiver]; + mathint allowanceBefore = allowance(owner, caller); + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 shares = withdraw(e, assets, receiver, owner); + + assert to_mathint(shares) == expectedShares; + assert to_mathint(totalSupply()) == supplyBefore - shares; + assert to_mathint(balanceOf(owner)) == ownerSharesBefore - shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore - assets; + assert balanceByToken[token][receiver] == recvAssetsBefore + assets; + + // A third-party caller spends allowance; the owner acting for themselves does not. Infinite + // approval is left untouched, by ERC20 design. + assert caller != owner && allowanceBefore < to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore - shares; + assert caller != owner && allowanceBefore == to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore; + assert caller == owner => to_mathint(allowance(owner, caller)) == allowanceBefore; + + assert balanceOf(other) != otherSharesBefore => other == owner; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == receiver || other == currentContract); +} + +rule redeemConserves(env e, uint256 shares, address receiver, address owner, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0 && receiver != currentContract; + + mathint expectedAssets = previewRedeem(shares); + mathint supplyBefore = totalSupply(); + mathint ownerSharesBefore = balanceOf(owner); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint recvAssetsBefore = balanceByToken[token][receiver]; + mathint allowanceBefore = allowance(owner, caller); + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 assets = redeem(e, shares, receiver, owner); + + assert to_mathint(assets) == expectedAssets; + assert to_mathint(totalSupply()) == supplyBefore - shares; + assert to_mathint(balanceOf(owner)) == ownerSharesBefore - shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore - assets; + assert balanceByToken[token][receiver] == recvAssetsBefore + assets; + + assert caller != owner && allowanceBefore < to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore - shares; + assert caller != owner && allowanceBefore == to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore; + assert caller == owner => to_mathint(allowance(owner, caller)) == allowanceBefore; + + assert balanceOf(other) != otherSharesBefore => other == owner; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == receiver || other == currentContract); +} From 1b13e6f544575b74b36ba012f9174347ef44854b Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 03:30:37 -0300 Subject: [PATCH 07/20] fv: shard the ERC4626 config with a complement A positive rule list is a coverage claim that decays: a newly added rule is silently unverified and the suite still goes green. The complement shard carries the same list under exclude_rule, so the two tile the rule space and anything not named lands in the complement rather than going unrun. Both confs are identical apart from the selector and the message, so a pass in one and a timeout in the other says something about the rules rather than the configs. The builtin sanity rule lives in the complement: it is a property of the scene rather than of the vault, and it keeps that shard non-empty, which the prover requires. Prover runs: https://prover.certora.com/output/1392759/749da38c0d8f4cf0812116f9c3e12070?anonymousKey=2894d8e2c220b53101eccee6a90ed95ef4033bbd https://prover.certora.com/output/1392759/ac9ea159bfa14eea968d10ef4fe3c082?anonymousKey=675379c58c214b9cd3a882ec08ffea4aadba0e73 --- fv/specs/ERC4626.conf | 18 +++++++++++++++++- fv/specs/ERC4626_rest.conf | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 fv/specs/ERC4626_rest.conf diff --git a/fv/specs/ERC4626.conf b/fv/specs/ERC4626.conf index 4f631d88a53..40d6e759122 100644 --- a/fv/specs/ERC4626.conf +++ b/fv/specs/ERC4626.conf @@ -4,12 +4,28 @@ "fv/harnesses/ERC4626Harness.sol" ], "global_timeout": 600, - "msg": "ERC4626 tiers 1-2", + "msg": "ERC4626 tier 1: invariants, algebra, boundary, conservation", "optimistic_loop": true, "parametric_contracts": [ "ERC4626Harness" ], "process": "emv", + "rule": [ + "setupIsSatisfiable", + "totalSupplyIsSumOfBalances", + "vaultNeverOvercommitted", + "roundTripNeverCreatesValue", + "roundingGapIsAtMostOne", + "depositGapCanBeOne", + "mintGapCanBeOne", + "maxBoundaryIsConsistent", + "redeemMaxNeverReverts", + "withdrawMaxNeverReverts", + "depositConserves", + "mintConserves", + "withdrawConserves", + "redeemConserves" + ], "rule_sanity": "basic", "url_visibility": "public", "verify": "ERC4626Harness:fv/specs/ERC4626.spec" diff --git a/fv/specs/ERC4626_rest.conf b/fv/specs/ERC4626_rest.conf new file mode 100644 index 00000000000..8536b95fc2d --- /dev/null +++ b/fv/specs/ERC4626_rest.conf @@ -0,0 +1,32 @@ +{ + "build_cache": true, + "exclude_rule": [ + "setupIsSatisfiable", + "totalSupplyIsSumOfBalances", + "vaultNeverOvercommitted", + "roundTripNeverCreatesValue", + "roundingGapIsAtMostOne", + "depositGapCanBeOne", + "mintGapCanBeOne", + "maxBoundaryIsConsistent", + "redeemMaxNeverReverts", + "withdrawMaxNeverReverts", + "depositConserves", + "mintConserves", + "withdrawConserves", + "redeemConserves" + ], + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 600, + "msg": "ERC4626 complement shard: the builtin sanity rule, plus anything not named in ERC4626.conf", + "optimistic_loop": true, + "parametric_contracts": [ + "ERC4626Harness" + ], + "process": "emv", + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626Harness:fv/specs/ERC4626.spec" +} From b90b8b0633fd557690bc9adf1f214ceb4f76bbe5 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 06:06:59 -0300 Subject: [PATCH 08/20] fv: add ERC4626 anti-splitting rules (P4) Snapshot replay for deposit and withdraw plus a donation-interleaved variant, with the inequality directions derived from the rounding mode and assert_uint256 on the combined amount so an overflowing sum fails rather than being assumed away. Adds a third shard for these rules. An isolation probe showed the replay machinery is nearly free and the whole cost is the nested-floor share math, so the shard forces nonlinear arithmetic, turns splitting off, and races ten solver seeds. That takes the closed-form obligation from a timeout to a second. depositIsNotSplittable is discharged. The withdraw mirror and the donation variant still exceed the solver budget: both hold under exhaustive and random sampling, so this is cost rather than a defect. Both are annotated in the spec and excluded from every shard, so their absence is not readable as a pass. Prover runs: https://prover.certora.com/output/1392759/8ed8cb59ae59465fbc77462232f52710?anonymousKey=6076baa48f1f53a2de5816970454097a6f57d527 https://prover.certora.com/output/1392759/ac6bd6eb4d204b1e93a4c3768a91a61a?anonymousKey=7843c2de77fbc66261c3113df100673536ec4ec1 https://prover.certora.com/output/1392759/3a96491c44644ff7a907289cf4aa0f0d?anonymousKey=f0d7646fe86dd27462f7e79f2d082a9bdc9bea77 --- fv/specs/ERC4626.spec | 98 +++++++++++++++++++++++++++++++++++++ fv/specs/ERC4626_rest.conf | 5 +- fv/specs/ERC4626_split.conf | 23 +++++++++ 3 files changed, 125 insertions(+), 1 deletion(-) create mode 100644 fv/specs/ERC4626_split.conf diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 9576887cc39..e2ebe801aac 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -297,3 +297,101 @@ rule redeemConserves(env e, uint256 shares, address receiver, address owner, add assert balanceByToken[token][other] != otherAssetsBefore => (other == receiver || other == currentContract); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P4: splitting an operation into steps never beats doing it in one │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Three details carry this rule. The observable is the credited share balance rather than the +/// return value, which is what catches "returned the right number, booked the wrong one". The +/// inequality direction is derived from the rounding mode rather than chosen: previewDeposit floors, +/// so a credit rounds down and the one-shot call must not pay out less than the split. And the +/// combined amount uses assert_uint256, not require_uint256, so an overflowing sum fails the rule +/// instead of being assumed away - that boundary is where a splitting attack would live. +/// +/// Both histories start from the same snapshot, so the receiver's pre-existing balance cancels and +/// comparing absolute balances is sound. +rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + deposit(e, y, receiver); + mathint split = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + mathint combined = balanceOf(receiver); + + assert combined >= split; // credit rounds down => one step favours the depositor + satisfy combined > split; // ... and it actually bites somewhere +} + +/// The mirror. previewWithdraw ceils, so shares burned round up and two burns overcharge by more +/// than one: the split must never burn fewer shares than the one-shot. Burning more leaves less, so +/// in terms of the remaining balance the direction is the same as deposit. +/// +/// NOT CURRENTLY DISCHARGED. The strictness witness passes, but the assertion exceeds the solver +/// budget even with nonlinear arithmetic forced and splitting off - ceil composed with ceil over +/// four symbolic 256-bit unknowns. The property holds under exhaustive small-value and large random +/// sampling, so this is solver cost rather than a defect. Excluded from every shard and carried in +/// the timeout ledger; do not read its absence from the suite as a pass. +rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require nonzerosender(e); + require receiver != 0 && receiver != currentContract && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + storage init = lastStorage; + + withdraw(e, x, receiver, owner); + withdraw(e, y, receiver, owner); + mathint split = balanceOf(owner); + + withdraw(e, assert_uint256(x + y), receiver, owner) at init; + mathint combined = balanceOf(owner); + + assert combined >= split; + satisfy combined > split; +} + +/// The variant only a donation model can express. Both histories spend the same x + y + d assets; +/// only the ordering differs. +/// +/// The baseline is depositing up front, not depositing afterwards. Comparing against a deposit made +/// after the donation would not be a splitting property at all - entering before a donation is +/// simply cheaper than entering after one, by an unbounded margin rather than a rounding unit, and +/// that is what a donation means rather than a flaw. The real claim is that holding part of a +/// deposit back across a donation never gains shares over committing it all at once. +/// +/// NOT CURRENTLY DISCHARGED, for the same reason as the withdraw mirror. Its arithmetic core is +/// trivial in closed form; the cost is the five-operation replay on top. Carried in the ledger. +rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + donate(e, d); + deposit(e, y, receiver); + mathint heldBack = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + donate(e, d); + mathint upfront = balanceOf(receiver); + + assert heldBack <= upfront; +} diff --git a/fv/specs/ERC4626_rest.conf b/fv/specs/ERC4626_rest.conf index 8536b95fc2d..18dbd339697 100644 --- a/fv/specs/ERC4626_rest.conf +++ b/fv/specs/ERC4626_rest.conf @@ -14,7 +14,10 @@ "depositConserves", "mintConserves", "withdrawConserves", - "redeemConserves" + "redeemConserves", + "depositIsNotSplittable", + "withdrawIsNotSplittable", + "holdingBackAcrossDonationDoesNotPay" ], "files": [ "fv/harnesses/ERC4626Harness.sol" diff --git a/fv/specs/ERC4626_split.conf b/fv/specs/ERC4626_split.conf new file mode 100644 index 00000000000..17866402d55 --- /dev/null +++ b/fv/specs/ERC4626_split.conf @@ -0,0 +1,23 @@ +{ + "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, + "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" +} From 299a4fa114309036e3ac1bbc53113386b87c0fe2 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 21:53:23 -0300 Subject: [PATCH 09/20] fv: add ERC4626 rate monotonicity rule (P5) Parametric over every non-view harness method, donate() included, so the raw asset-inflow vector is inside the claim rather than outside it. Deposits round shares minted down and withdrawals round shares burned up, so the rounding residue stays with the vault and the price per share can only rise or hold. Verified RED under a temporary unbacked share mint on the harness, which is the hazard the contract documents. Prover run: https://prover.certora.com/output/1392759/99fd77b65bee4a0bb02d55fcab99af64?anonymousKey=3ef3ce7831c2fea1f8a72abd7e8ce9fc1e7a86e8 --- fv/specs/ERC4626.spec | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index e2ebe801aac..2a6eb8ecc16 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -395,3 +395,29 @@ rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, assert heldBack <= upfront; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P5: no method can lower the exchange rate │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Deposits round shares minted down and withdrawals round shares burned up, so in every direction +/// the rounding residue stays with the vault and the price per share can only rise or hold. +/// +/// Ranges over the harness method set, which includes donate(). That is deliberate and part of the +/// claim: a raw asset inflow is the inflation attack's vector, and on the production contract alone +/// it is not a method any parametric rule can reach. +rule rateNeverDecreases(env e, method f) filtered { f -> !f.isView } { + require sane(); + require noVirtualOverflow(); + require e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + mathint before = convertToAssets(ONE_SHARE()); + + calldataarg args; + f(e, args); + + assert to_mathint(convertToAssets(ONE_SHARE())) >= before; +} From 7fe740998d9c243874a27bfd19ce3cbf8e7ee213 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 22:08:59 -0300 Subject: [PATCH 10/20] fv: add ERC4626 donation-safety rules (P6) Donations never reduce what an existing holder can redeem, and neither do asset inflows arriving by any other means. The second rule writes the asset ghost directly, so it covers inflows no transaction on this contract can produce: yield accrual, a rebase up, a raw transfer from an address that never calls the vault. Verified RED under a transposed mulDiv in _convertToAssets. Note that inflating the denominator or ignoring totalAssets entirely both leave these rules green: a mutation that weakens a quantity uniformly does not test a monotonicity property, only one that reverses the direction does. Prover run: https://prover.certora.com/output/1392759/eb81dc3dd3374756afd34a4d2a1ea03a?anonymousKey=eaf15defb0c27dc27735c935b348f717fa0046aa --- fv/specs/ERC4626.spec | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 2a6eb8ecc16..35d242f3854 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -421,3 +421,45 @@ rule rateNeverDecreases(env e, method f) filtered { f -> !f.isView } { assert to_mathint(convertToAssets(ONE_SHARE())) >= before; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P6: an asset inflow never reduces what an existing holder can redeem │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The transaction-level claim. A donation raises totalAssets and leaves totalSupply alone, so the +/// conversion's denominator is untouched and its numerator only grows. +rule donationNeverHarmsHolders(env e, uint256 d, address holder) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require e.msg.sender != currentContract && holder != currentContract; + // The post-state must convert too, or the second probe reverts and prunes the path invisibly. + require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; + requireInvariant totalSupplyIsSumOfBalances(); + + mathint before = previewRedeem(balanceOf(holder)); + donate(e, d); + assert to_mathint(previewRedeem(balanceOf(holder))) >= before; +} + +/// The same property for an inflow arriving by any means at all, not only a call to donate(): a raw +/// transfer from an address that never touches the vault, yield accrual, a rebase up. Writing the +/// ghost directly is what lets this cover inflows no transaction on this contract can produce. +rule assetInflowNeverHarmsHolders(uint256 d, address holder) { + require sane(); + require noVirtualOverflow(); + require holder != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address token = asset(); + require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; + + mathint before = previewRedeem(balanceOf(holder)); + + balanceByToken[token][currentContract] = + require_uint256(balanceByToken[token][currentContract] + d); + + assert to_mathint(previewRedeem(balanceOf(holder))) >= before; +} From 5b1ca1a595ec1699103127d096796f5839cdf437 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 23:06:47 -0300 Subject: [PATCH 11/20] fv: add ERC4626 donation-sandwich rule (P7) The inflation-attack non-profitability claim, in its own tuned config: enter, inflate the rate with a donation, let a victim deposit, exit, and assert the attacker's asset balance never rises. Scoped to a vault that starts empty. That is what the virtual-shares mitigation claims and the only scope in which the claim holds: from an arbitrary state the sequence is profitable, but only because a vault holding assets against no shares is already manipulated, so the attacker profits on a price someone else paid to inflate. Requiring an empty vault makes them pay for the manipulation themselves. The contract is explicit that the mitigation does not fully prevent the attack and that empty vaults are the hazard, so this records the narrower claim rather than the general one. Verified RED under a mutation restoring pre-v4.9 behaviour without virtual assets and shares. Prover run: https://prover.certora.com/output/1392759/3646df758a544c35aaa4124b06f3b513?anonymousKey=cd942582582f46d66424c98761caf8023ea3b861 --- fv/specs/ERC4626Sandwich.conf | 20 +++++++++++ fv/specs/ERC4626Sandwich.spec | 63 +++++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+) create mode 100644 fv/specs/ERC4626Sandwich.conf create mode 100644 fv/specs/ERC4626Sandwich.spec diff --git a/fv/specs/ERC4626Sandwich.conf b/fv/specs/ERC4626Sandwich.conf new file mode 100644 index 00000000000..9d0e5ffc4ee --- /dev/null +++ b/fv/specs/ERC4626Sandwich.conf @@ -0,0 +1,20 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 1800, + "msg": "ERC4626 tier 3: donation sandwich non-profitability", + "optimistic_loop": true, + "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/ERC4626Sandwich.spec" +} diff --git a/fv/specs/ERC4626Sandwich.spec b/fv/specs/ERC4626Sandwich.spec new file mode 100644 index 00000000000..79797b1446e --- /dev/null +++ b/fv/specs/ERC4626Sandwich.spec @@ -0,0 +1,63 @@ +import "ERC4626Base.spec"; +import "helpers/erc20-supply.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P7: the donation sandwich is not profitable against a fresh vault │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The inflation/donation-frontrunning 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 whole sequence captures "never profits" in one assertion, with no separate accounting +/// of what they paid. +/// +/// Scoped to a vault that starts empty, which is both what the virtual-shares mitigation claims and +/// the only scope in which the claim is true. Starting from an arbitrary (totalSupply, totalAssets) +/// admits states that are already manipulated - one share outstanding against a large asset balance, +/// say - where an attacker profits without donating anything, because the price was inflated before +/// the sequence began. Attributing that to this contract's rounding would be wrong: the contract +/// documents that empty and nearly-empty vaults are the hazard and directs deployers to seed them. +/// +/// Because totalSupply starts at zero, the attacker necessarily starts with no shares, so redeeming +/// their whole balance redeems only what this sequence minted. +rule donationSandwichNeverProfits(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) { + require sane(); + require nonpayable(eAtt) && nonpayable(eVic); + require noVirtualOverflow(); + 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; +} + +/// Vacuity guard for the rule above: the four-call sequence has to be constructible at all, or its +/// green means nothing. +rule sandwichScenarioIsReachable(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) { + require sane(); + require nonpayable(eAtt) && nonpayable(eVic); + require eAtt.msg.sender != eVic.msg.sender; + require eAtt.msg.sender != currentContract && eVic.msg.sender != currentContract; + require totalSupply() == 0 && totalAssets() == 0; + + deposit(eAtt, a1, eAtt.msg.sender); + donate(eAtt, d); + deposit(eVic, a2, eVic.msg.sender); + satisfy true; +} From 03b7af37064d12a5207a17a9e3a9dbd9bc230070 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Thu, 27 Aug 2026 23:41:47 -0300 Subject: [PATCH 12/20] fv: record the ERC4626 suite's ledgers The timeout ledger goes in the workflow, next to the job that would have run the rules it lists, so it is re-read whenever that job changes. The soundness ledger goes in the spec files: what a rule narrows on the rule, what a file assumes at its top. Both halves then travel with the code. Prover runs: https://prover.certora.com/output/1392759/cee60a07375e4f128c3ef351730cab16?anonymousKey=32ec067a5c77139114935c728ee00dc1838af2dc https://prover.certora.com/output/1392759/47a8d21b7b8b495f9ad560a7e6221a71?anonymousKey=1e53632b61bb42e651eafb11afcdaa64945d92bd --- .github/workflows/fv-certora.yml | 20 ++++++++++++++++++++ fv/specs/ERC4626.spec | 5 +++++ fv/specs/ERC4626Base.spec | 21 +++++++++++++++++++++ fv/specs/ERC4626Sandwich.spec | 4 ++++ 4 files changed, 50 insertions(+) diff --git a/.github/workflows/fv-certora.yml b/.github/workflows/fv-certora.yml index 667fa250bd3..218f78410f9 100644 --- a/.github/workflows/fv-certora.yml +++ b/.github/workflows/fv-certora.yml @@ -146,3 +146,23 @@ jobs: run: | [[ $IDENTIFY = success ]] || { echo "::error::could not work out which configs to run"; exit 1; } [[ $VERIFY = success || $VERIFY = skipped ]] || { echo "::error::verification $VERIFY"; exit 1; } + +# ┌────────────────────────────────────────────────────────────────────────────────────────┐ +# │ Timeout ledger: rules that are NOT proved. Excluded from every config, so their │ +# │ absence from a green run is not a pass. Re-attempt manually with the commands below. │ +# └────────────────────────────────────────────────────────────────────────────────────────┘ +# +# ERC4626 -- both hold under exhaustive small-value and large random sampling, so these are +# solver cost rather than defects. Last attempted with nonlinear arithmetic forced, splitting +# off, a ten-seed solver race, smt_timeout 1500 and global_timeout 3600. +# +# certoraRun fv/specs/ERC4626_split.conf --rule withdrawIsNotSplittable +# https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 +# timed out at 3003s; its strictness witness verifies in 9s +# +# certoraRun fv/specs/ERC4626_split.conf --rule holdingBackAcrossDonationDoesNotPay +# https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 +# timed out at 1504s; its arithmetic core verifies in ~1s in closed form, so the cost is +# the five-operation replay rather than the share math +# +# What the suite assumes rather than proves is recorded at the top of fv/specs/ERC4626Base.spec. diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 35d242f3854..4b6bed393f6 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -1,3 +1,8 @@ +// Three configs verify this file. ERC4626.conf names most rules, ERC4626_split.conf takes the one +// needing tuned solver settings for nonlinear share math, and ERC4626_rest.conf is their +// complement, so a rule added here and named in neither list still runs rather than going silently +// unverified. Two rules are excluded from all three and carry a note of their own. + import "ERC4626Base.spec"; import "helpers/erc20-supply.spec"; diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec index 7aac7fe7b94..305c0a2a216 100644 --- a/fv/specs/ERC4626Base.spec +++ b/fv/specs/ERC4626Base.spec @@ -1,3 +1,24 @@ +// Shared base for the ERC4626 suite: the summary layer plus the scope definitions. It holds the +// only methods block, so every config verifying an ERC4626 spec inherits what is assumed here. +// +// 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 the harness, so no result here generalizes to a larger offset. +// - 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 rather than conveniences: 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 recorded in the timeout ledger in the formal-verification +// workflow, not here. + import "helpers/helpers.spec"; import "helpers/math-cvl.spec"; import "helpers/erc20-cvl.spec"; diff --git a/fv/specs/ERC4626Sandwich.spec b/fv/specs/ERC4626Sandwich.spec index 79797b1446e..bc4069594d2 100644 --- a/fv/specs/ERC4626Sandwich.spec +++ b/fv/specs/ERC4626Sandwich.spec @@ -1,3 +1,7 @@ +// Kept out of ERC4626.spec so that its tuned config does not drag the whole tier-1 sweep along with +// it. The scope this rule is proved under is narrower than the property's usual statement; see the +// rule's own note. + import "ERC4626Base.spec"; import "helpers/erc20-supply.spec"; From e389b1f6b36bec2fa03c23707dd67536366fff78 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Fri, 28 Aug 2026 00:29:28 -0300 Subject: [PATCH 13/20] fv: add the symbolic decimals-offset tier for ERC4626 Every other spec in the suite runs at _decimalsOffset() == 0, where the offset is the identity, so nothing proved there says the offset does anything. This tier leaves the offset symbolic and re-proves solvency and the donation sandwich over offsets 0 through 77. It also adds inflationCostScalesWithOffset, the claim only a symbolic offset can state: a deposit rounds to zero shares only when the vault already holds at least 10**offset times that deposit, so the offset is the multiplier between what a victim loses and what robbing them costs. That is the "orders of magnitude more expensive than it is profitable" claim in ERC4626's own documentation, which no zero-offset rule can express. The symbolic exponent needed no ghost abstraction and no bound on the offset, so the tier adds nothing to the suite's assumptions. Prover runs: https://prover.certora.com/output/1392759/9afe1d75a84d4fdb81e362adfca9eb9c?anonymousKey=b9b5fd2f43c56b3309c36eb0b0c34dfdac52a156 https://prover.certora.com/output/1392759/0fe2b8f4b74e473293625695201e1a7b?anonymousKey=c1359ac05eba0704a61961551c864cf982506cb9 Co-Authored-By: Claude Opus 5 (1M context) --- fv/harnesses/ERC4626OffsetHarness.sol | 42 +++++++++++++ fv/specs/ERC4626Base.spec | 10 ++- fv/specs/ERC4626Offset.conf | 16 +++++ fv/specs/ERC4626Offset.spec | 87 +++++++++++++++++++++++++++ fv/specs/ERC4626OffsetSandwich.conf | 20 ++++++ fv/specs/ERC4626Sandwich.spec | 4 ++ 6 files changed, 176 insertions(+), 3 deletions(-) create mode 100644 fv/harnesses/ERC4626OffsetHarness.sol create mode 100644 fv/specs/ERC4626Offset.conf create mode 100644 fv/specs/ERC4626Offset.spec create mode 100644 fv/specs/ERC4626OffsetSandwich.conf diff --git a/fv/harnesses/ERC4626OffsetHarness.sol b/fv/harnesses/ERC4626OffsetHarness.sol new file mode 100644 index 00000000000..89ee4a0da91 --- /dev/null +++ b/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); + } +} diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec index 305c0a2a216..a1b21f710b2 100644 --- a/fv/specs/ERC4626Base.spec +++ b/fv/specs/ERC4626Base.spec @@ -1,5 +1,6 @@ -// Shared base for the ERC4626 suite: the summary layer plus the scope definitions. It holds the -// only methods block, so every config verifying an ERC4626 spec inherits what is assumed here. +// 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. +// ERC4626Offset.spec adds a methods block of its own, but only to declare harness-only views. // // 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 @@ -8,7 +9,10 @@ // - 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 the harness, so no result here generalizes to a larger offset. +// - _decimalsOffset() is 0 in this harness, so no result verified against it generalizes to a +// larger offset. ERC4626Offset.spec re-proves solvency and the donation sandwich against a +// harness whose offset is symbolic, and states the one claim only a symbolic offset can make; +// 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 diff --git a/fv/specs/ERC4626Offset.conf b/fv/specs/ERC4626Offset.conf new file mode 100644 index 00000000000..f2bad60293c --- /dev/null +++ b/fv/specs/ERC4626Offset.conf @@ -0,0 +1,16 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626OffsetHarness.sol" + ], + "global_timeout": 600, + "msg": "ERC4626 tier 4: symbolic decimals offset", + "optimistic_loop": true, + "parametric_contracts": [ + "ERC4626OffsetHarness" + ], + "process": "emv", + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Offset.spec" +} diff --git a/fv/specs/ERC4626Offset.spec b/fv/specs/ERC4626Offset.spec new file mode 100644 index 00000000000..db08679d570 --- /dev/null +++ b/fv/specs/ERC4626Offset.spec @@ -0,0 +1,87 @@ +// Tier 4: the same claims, with 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 symbolic. That turns a constant +// into an EXP over a symbolic exponent, a shape the rest of the suite never exercises. It turned +// out to be tractable unaided: nothing here abstracts 10**offset behind a ghost and no rule needs +// the offset bounded, so the tier carries no assumption the rest of the suite does not already. +// +// Offsets from 78 up make 10**offset overflow uint256, so every conversion reverts and the prover +// prunes those paths. The rules here are therefore claims about offsets 0 through 77. +// +// The donation sandwich is also re-proved at a symbolic offset, by ERC4626OffsetSandwich.conf +// pointing the unchanged ERC4626Sandwich.spec at this file's harness. + +import "ERC4626Base.spec"; + +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 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Without this, a rule below could pass because the scene admits no nonzero offset at all, which +/// would make the whole 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 at a symbolic offset: the vault is never over-committed │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The zero-offset proof of this reduces to 0 < (A+1)K, which holds for every K >= 1, so P1 should +/// carry to a symbolic offset unchanged, which is what makes it the right first check: it is the +/// cheapest rule in the suite, so a red here would mean the prover cannot handle a symbolic +/// exponent rather than that the property is harder. +rule vaultNeverOvercommittedAnyOffset() { + require sane(); + assert previewRedeem(totalSupply()) <= totalAssets(); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ What the offset is FOR: it prices the inflation attack, and only a symbolic offset can say so │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The suite's other rules establish that the vault is sound. None of them establishes that the +/// offset buys anything, because at offset 0 it is the identity - and soundness is not what the +/// offset is for. 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. +/// +/// Stated exactly: 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. So the victim loses a, and whoever set the vault up to do it had +/// already sunk at least a * 10^offset into it. The offset is the multiplier between the two. +/// +/// The bound is tight rather than slack - A = a*K is reachable - so it is not passing for free. +/// At offset 0 it degrades to A >= a, which is true and worthless. Its strength IS the offset, and +/// 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()); +} + +/// Guards the rule above against vacuity: if no state lets a nonzero deposit round to zero shares, +/// the bound holds over an empty set. It has to be reachable, because ERC4626 is explicit that the +/// mitigation does not fully prevent the attack. +rule victimCanBeRobbedAtAnyOffset(uint256 assets) { + require sane(); + require assets > 0; + satisfy previewDeposit(assets) == 0; +} diff --git a/fv/specs/ERC4626OffsetSandwich.conf b/fv/specs/ERC4626OffsetSandwich.conf new file mode 100644 index 00000000000..b12d1e8fbe9 --- /dev/null +++ b/fv/specs/ERC4626OffsetSandwich.conf @@ -0,0 +1,20 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626OffsetHarness.sol" + ], + "global_timeout": 1800, + "msg": "ERC4626 tier 4: donation sandwich at a symbolic decimals offset", + "optimistic_loop": true, + "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/ERC4626Sandwich.spec" +} diff --git a/fv/specs/ERC4626Sandwich.spec b/fv/specs/ERC4626Sandwich.spec index bc4069594d2..2da148ead2a 100644 --- a/fv/specs/ERC4626Sandwich.spec +++ b/fv/specs/ERC4626Sandwich.spec @@ -1,6 +1,10 @@ // Kept out of ERC4626.spec so that its tuned config does not drag the whole tier-1 sweep along with // it. The scope this rule is proved under is narrower than the property's usual statement; see the // rule's own note. +// +// Two configs verify this file against two harnesses: ERC4626Sandwich.conf at a zero decimals +// offset, ERC4626OffsetSandwich.conf at a symbolic one. Nothing here mentions the offset, so the +// same rule text carries over unchanged. import "ERC4626Base.spec"; import "helpers/erc20-supply.spec"; From 05d6b43b3d4a67159a80c664c91658c3f94b9218 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Fri, 28 Aug 2026 19:27:05 -0300 Subject: [PATCH 14/20] fv: rename ERC4626Sandwich to ERC4626Donation and tighten the suite Drop the vacuity guards rule_sanity already provides, the donate()-only inflow rule subsumed by the ghost-write one, and the zero-offset solvency rule subsumed by the symbolic-offset proof. Merge ERC4626_rest.conf into ERC4626.conf via exclude_rule so the shards tile by construction. Dedupe and trim the spec prose. Co-Authored-By: Claude Fable 5 --- fv/specs/ERC4626.conf | 23 +- fv/specs/ERC4626.spec | 381 ++++++++---------- fv/specs/ERC4626Base.spec | 16 +- ...4626Sandwich.conf => ERC4626Donation.conf} | 4 +- fv/specs/ERC4626Donation.spec | 51 +++ fv/specs/ERC4626Offset.spec | 82 ++-- ...ndwich.conf => ERC4626OffsetDonation.conf} | 4 +- fv/specs/ERC4626Sandwich.spec | 71 ---- fv/specs/ERC4626_rest.conf | 35 -- 9 files changed, 274 insertions(+), 393 deletions(-) rename fv/specs/{ERC4626Sandwich.conf => ERC4626Donation.conf} (83%) create mode 100644 fv/specs/ERC4626Donation.spec rename fv/specs/{ERC4626OffsetSandwich.conf => ERC4626OffsetDonation.conf} (82%) delete mode 100644 fv/specs/ERC4626Sandwich.spec delete mode 100644 fv/specs/ERC4626_rest.conf diff --git a/fv/specs/ERC4626.conf b/fv/specs/ERC4626.conf index 40d6e759122..cd92df735b9 100644 --- a/fv/specs/ERC4626.conf +++ b/fv/specs/ERC4626.conf @@ -1,31 +1,20 @@ { "build_cache": true, + "exclude_rule": [ + "depositIsNotSplittable", + "withdrawIsNotSplittable", + "holdingBackAcrossDonationDoesNotPay" + ], "files": [ "fv/harnesses/ERC4626Harness.sol" ], "global_timeout": 600, - "msg": "ERC4626 tier 1: invariants, algebra, boundary, conservation", + "msg": "ERC4626 tier 1: everything but the anti-splitting rules", "optimistic_loop": true, "parametric_contracts": [ "ERC4626Harness" ], "process": "emv", - "rule": [ - "setupIsSatisfiable", - "totalSupplyIsSumOfBalances", - "vaultNeverOvercommitted", - "roundTripNeverCreatesValue", - "roundingGapIsAtMostOne", - "depositGapCanBeOne", - "mintGapCanBeOne", - "maxBoundaryIsConsistent", - "redeemMaxNeverReverts", - "withdrawMaxNeverReverts", - "depositConserves", - "mintConserves", - "withdrawConserves", - "redeemConserves" - ], "rule_sanity": "basic", "url_visibility": "public", "verify": "ERC4626Harness:fv/specs/ERC4626.spec" diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 4b6bed393f6..687d050850b 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -1,7 +1,11 @@ -// Three configs verify this file. ERC4626.conf names most rules, ERC4626_split.conf takes the one -// needing tuned solver settings for nonlinear share math, and ERC4626_rest.conf is their -// complement, so a rule added here and named in neither list still runs rather than going silently -// unverified. Two rules are excluded from all three and carry a note of their own. +// Two configs verify this file. ERC4626_split.conf takes depositIsNotSplittable, which needs tuned +// solver settings for nonlinear share math; ERC4626.conf excludes the three anti-splitting rules and +// runs everything else, so a rule added here runs without being named anywhere. The other two +// anti-splitting rules are excluded from both and carry a note of their own. +// +// Every config sets rule_sanity, so no rule here needs a hand-written reachability guard. +// +// P1 (solvency) lives in ERC4626Offset.spec, where the decimals offset is symbolic. import "ERC4626Base.spec"; import "helpers/erc20-supply.spec"; @@ -14,40 +18,9 @@ use builtin rule sanity; use invariant totalSupplyIsSumOfBalances; /* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Vacuity guard: if the scope assumptions are unsatisfiable, every rule below passes for free │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule setupIsSatisfiable(env e, uint256 assets, address receiver) { - require sane(); - require nonpayable(e); - deposit(e, assets, receiver); - satisfy true; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ 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: it needs no induction, and quantifying over all sane states is -/// stronger than quantifying over reachable ones. -/// -/// Independent of the decimals offset: 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 - note this needs no -/// relationship between T and A, which is exactly why induction is unnecessary. -rule vaultNeverOvercommitted() { - require sane(); - assert previewRedeem(totalSupply()) <= totalAssets(); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P2: round trips never create value, and per-operation leakage is at most one unit │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P2: round trips never create value, and per-operation leakage is at most one unit │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ /// The no-free-money half. Both directions of a round trip are stated on the preview functions, so @@ -61,9 +34,9 @@ rule roundTripNeverCreatesValue(uint256 assets) { assert previewMint(previewWithdraw(assets)) >= assets; } -/// The tightness half. Bounding leakage at one unit is worth far more than a vague `>=`, and it -/// catches a preview override whose rounding direction is transposed, which ERC4626 warns about: -/// overrides to the deposit or withdraw mechanism must be reflected in the preview functions. +/// The tightness half. Bounding leakage at one unit catches a preview override whose rounding +/// direction is transposed, which ERC4626 warns about: overrides to the deposit or withdraw +/// mechanism must be reflected in the preview functions. /// /// previewWithdraw and previewDeposit are the same conversion at Ceil and Floor, as are previewMint /// and previewRedeem, so each gap is a ceil-minus-floor and lands in {0, 1}. @@ -91,9 +64,9 @@ rule mintGapCanBeOne(uint256 shares) { } /* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P3: the max/preview boundary - what the limits promise, the operations honour │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P3: the max/preview boundary - what the limits promise, the operations honour │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ /// maxWithdraw floors on the way out while previewWithdraw ceils on the way back, so it is not @@ -145,9 +118,157 @@ rule withdrawMaxNeverReverts(env e, address receiver) { } /* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Conservation and isolation: the state-changers move exactly what they claim, and nothing else │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P4: splitting an operation into steps never beats doing it in one │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Three details carry this rule. The observable is the credited share balance rather than the +/// return value, which is what catches "returned the right number, booked the wrong one". The +/// inequality direction is derived from the rounding mode: previewDeposit floors, so a credit rounds +/// down and the one-shot call must not pay out less than the split. And the combined amount uses +/// assert_uint256, not require_uint256, so an overflowing sum fails the rule instead of being +/// assumed away - that boundary is where a splitting attack would live. +/// +/// Both histories start from the same snapshot, so the receiver's pre-existing balance cancels and +/// comparing absolute balances is sound. +rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + deposit(e, y, receiver); + mathint split = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + mathint combined = balanceOf(receiver); + + assert combined >= split; // credit rounds down => one step favours the depositor + satisfy combined > split; // ... and it actually bites somewhere +} + +/// The mirror. previewWithdraw ceils, so shares burned round up and two burns overcharge by more +/// than one: the split must never burn fewer shares than the one-shot. Burning more leaves less, so +/// in terms of the remaining balance the direction is the same as deposit. +/// +/// NOT DISCHARGED: excluded from every config, see the +/// [ledger](../../.github/workflows/formal-verification.yml#L61-L79). +rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require nonzerosender(e); + require receiver != 0 && receiver != currentContract && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + storage init = lastStorage; + + withdraw(e, x, receiver, owner); + withdraw(e, y, receiver, owner); + mathint split = balanceOf(owner); + + withdraw(e, assert_uint256(x + y), receiver, owner) at init; + mathint combined = balanceOf(owner); + + assert combined >= split; + satisfy combined > split; +} + +/// The variant only a donation model can express. Both histories spend the same x + y + d assets; +/// only the ordering differs. +/// +/// The baseline is depositing up front, not depositing after the donation: entering before a +/// donation is cheaper than entering after one by an unbounded margin, which is what a donation +/// means rather than a flaw. The claim is that holding part of a deposit back across a donation +/// never gains shares over committing it all at once. +/// +/// NOT DISCHARGED: excluded from every config, see the +/// [ledger](../../.github/workflows/formal-verification.yml#L61-L79). +rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + donate(e, d); + deposit(e, y, receiver); + mathint heldBack = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + donate(e, d); + mathint upfront = balanceOf(receiver); + + assert heldBack <= upfront; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P5: no method can lower the exchange rate │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Deposits round shares minted down and withdrawals round shares burned up, so in every direction +/// the rounding residue stays with the vault and the price per share can only rise or hold. +/// +/// Ranges over the harness method set, which includes donate(); see ERC4626Base.spec for why. +rule rateNeverDecreases(env e, method f) filtered { f -> !f.isView } { + require sane(); + require noVirtualOverflow(); + require e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + mathint before = convertToAssets(ONE_SHARE()); + + calldataarg args; + f(e, args); + + assert to_mathint(convertToAssets(ONE_SHARE())) >= before; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P6: an asset inflow never reduces what an existing holder can redeem │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// An inflow raises totalAssets and leaves totalSupply alone, so the conversion's denominator is +/// untouched and its numerator only grows. +/// +/// Stated on the ghost rather than on donate() so it covers an inflow arriving by any means: a raw +/// transfer from an address that never touches the vault, yield accrual, a rebase up. donate() +/// itself is covered by rateNeverDecreases. +rule assetInflowNeverHarmsHolders(uint256 d, address holder) { + require sane(); + require noVirtualOverflow(); + require holder != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address token = asset(); + // The post-state must convert too, or the second probe reverts and prunes the path invisibly. + require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; + + mathint before = previewRedeem(balanceOf(holder)); + + balanceByToken[token][currentContract] = + require_uint256(balanceByToken[token][currentContract] + d); + + assert to_mathint(previewRedeem(balanceOf(holder))) >= before; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Conservation and isolation: the state-changers move exactly what they claim, and nothing else │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ /// Supporting machinery rather than a headline property. The value properties all assume the @@ -302,169 +423,3 @@ rule redeemConserves(env e, uint256 shares, address receiver, address owner, add assert balanceByToken[token][other] != otherAssetsBefore => (other == receiver || other == currentContract); } - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P4: splitting an operation into steps never beats doing it in one │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -/// Three details carry this rule. The observable is the credited share balance rather than the -/// return value, which is what catches "returned the right number, booked the wrong one". The -/// inequality direction is derived from the rounding mode rather than chosen: previewDeposit floors, -/// so a credit rounds down and the one-shot call must not pay out less than the split. And the -/// combined amount uses assert_uint256, not require_uint256, so an overflowing sum fails the rule -/// instead of being assumed away - that boundary is where a splitting attack would live. -/// -/// Both histories start from the same snapshot, so the receiver's pre-existing balance cancels and -/// comparing absolute balances is sound. -rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { - require sane(); - require nonpayable(e); - require noVirtualOverflow(); - require receiver != 0 && e.msg.sender != currentContract; - requireInvariant totalSupplyIsSumOfBalances(); - - storage init = lastStorage; - - deposit(e, x, receiver); - deposit(e, y, receiver); - mathint split = balanceOf(receiver); - - deposit(e, assert_uint256(x + y), receiver) at init; - mathint combined = balanceOf(receiver); - - assert combined >= split; // credit rounds down => one step favours the depositor - satisfy combined > split; // ... and it actually bites somewhere -} - -/// The mirror. previewWithdraw ceils, so shares burned round up and two burns overcharge by more -/// than one: the split must never burn fewer shares than the one-shot. Burning more leaves less, so -/// in terms of the remaining balance the direction is the same as deposit. -/// -/// NOT CURRENTLY DISCHARGED. The strictness witness passes, but the assertion exceeds the solver -/// budget even with nonlinear arithmetic forced and splitting off - ceil composed with ceil over -/// four symbolic 256-bit unknowns. The property holds under exhaustive small-value and large random -/// sampling, so this is solver cost rather than a defect. Excluded from every shard and carried in -/// the timeout ledger; do not read its absence from the suite as a pass. -rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { - require sane(); - require nonpayable(e); - require noVirtualOverflow(); - require nonzerosender(e); - require receiver != 0 && receiver != currentContract && e.msg.sender != currentContract; - requireInvariant totalSupplyIsSumOfBalances(); - - address owner = e.msg.sender; - storage init = lastStorage; - - withdraw(e, x, receiver, owner); - withdraw(e, y, receiver, owner); - mathint split = balanceOf(owner); - - withdraw(e, assert_uint256(x + y), receiver, owner) at init; - mathint combined = balanceOf(owner); - - assert combined >= split; - satisfy combined > split; -} - -/// The variant only a donation model can express. Both histories spend the same x + y + d assets; -/// only the ordering differs. -/// -/// The baseline is depositing up front, not depositing afterwards. Comparing against a deposit made -/// after the donation would not be a splitting property at all - entering before a donation is -/// simply cheaper than entering after one, by an unbounded margin rather than a rounding unit, and -/// that is what a donation means rather than a flaw. The real claim is that holding part of a -/// deposit back across a donation never gains shares over committing it all at once. -/// -/// NOT CURRENTLY DISCHARGED, for the same reason as the withdraw mirror. Its arithmetic core is -/// trivial in closed form; the cost is the five-operation replay on top. Carried in the ledger. -rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { - require sane(); - require nonpayable(e); - require noVirtualOverflow(); - require receiver != 0 && e.msg.sender != currentContract; - requireInvariant totalSupplyIsSumOfBalances(); - - storage init = lastStorage; - - deposit(e, x, receiver); - donate(e, d); - deposit(e, y, receiver); - mathint heldBack = balanceOf(receiver); - - deposit(e, assert_uint256(x + y), receiver) at init; - donate(e, d); - mathint upfront = balanceOf(receiver); - - assert heldBack <= upfront; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P5: no method can lower the exchange rate │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -/// Deposits round shares minted down and withdrawals round shares burned up, so in every direction -/// the rounding residue stays with the vault and the price per share can only rise or hold. -/// -/// Ranges over the harness method set, which includes donate(). That is deliberate and part of the -/// claim: a raw asset inflow is the inflation attack's vector, and on the production contract alone -/// it is not a method any parametric rule can reach. -rule rateNeverDecreases(env e, method f) filtered { f -> !f.isView } { - require sane(); - require noVirtualOverflow(); - require e.msg.sender != currentContract; - requireInvariant totalSupplyIsSumOfBalances(); - - mathint before = convertToAssets(ONE_SHARE()); - - calldataarg args; - f(e, args); - - assert to_mathint(convertToAssets(ONE_SHARE())) >= before; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P6: an asset inflow never reduces what an existing holder can redeem │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -/// The transaction-level claim. A donation raises totalAssets and leaves totalSupply alone, so the -/// conversion's denominator is untouched and its numerator only grows. -rule donationNeverHarmsHolders(env e, uint256 d, address holder) { - require sane(); - require nonpayable(e); - require noVirtualOverflow(); - require e.msg.sender != currentContract && holder != currentContract; - // The post-state must convert too, or the second probe reverts and prunes the path invisibly. - require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; - requireInvariant totalSupplyIsSumOfBalances(); - - mathint before = previewRedeem(balanceOf(holder)); - donate(e, d); - assert to_mathint(previewRedeem(balanceOf(holder))) >= before; -} - -/// The same property for an inflow arriving by any means at all, not only a call to donate(): a raw -/// transfer from an address that never touches the vault, yield accrual, a rebase up. Writing the -/// ghost directly is what lets this cover inflows no transaction on this contract can produce. -rule assetInflowNeverHarmsHolders(uint256 d, address holder) { - require sane(); - require noVirtualOverflow(); - require holder != currentContract; - requireInvariant totalSupplyIsSumOfBalances(); - - address token = asset(); - require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; - - mathint before = previewRedeem(balanceOf(holder)); - - balanceByToken[token][currentContract] = - require_uint256(balanceByToken[token][currentContract] + d); - - assert to_mathint(previewRedeem(balanceOf(holder))) >= before; -} diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec index a1b21f710b2..826fd85f98b 100644 --- a/fv/specs/ERC4626Base.spec +++ b/fv/specs/ERC4626Base.spec @@ -1,6 +1,5 @@ // 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. -// ERC4626Offset.spec adds a methods block of its own, but only to declare harness-only views. // // 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 @@ -9,16 +8,15 @@ // - 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 this harness, so no result verified against it generalizes to a -// larger offset. ERC4626Offset.spec re-proves solvency and the donation sandwich against a -// harness whose offset is symbolic, and states the one claim only a symbolic offset can make; -// every other result in the suite is a zero-offset result. +// - _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 rather than conveniences: 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. +// 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 recorded in the timeout ledger in the formal-verification // workflow, not here. @@ -49,7 +47,7 @@ methods { // ---- summaries ---- // Trusted, not proved. ERC4626 only calls this overload, so summarizing it bypasses Math - // entirely; the 3-arg overload is deliberately left unbound because it would never fire. + // 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; diff --git a/fv/specs/ERC4626Sandwich.conf b/fv/specs/ERC4626Donation.conf similarity index 83% rename from fv/specs/ERC4626Sandwich.conf rename to fv/specs/ERC4626Donation.conf index 9d0e5ffc4ee..3a403f67a80 100644 --- a/fv/specs/ERC4626Sandwich.conf +++ b/fv/specs/ERC4626Donation.conf @@ -4,7 +4,7 @@ "fv/harnesses/ERC4626Harness.sol" ], "global_timeout": 1800, - "msg": "ERC4626 tier 3: donation sandwich non-profitability", + "msg": "ERC4626 tier 3: donation attack non-profitability", "optimistic_loop": true, "parametric_contracts": [ "ERC4626Harness" @@ -16,5 +16,5 @@ "rule_sanity": "basic", "smt_timeout": "1200", "url_visibility": "public", - "verify": "ERC4626Harness:fv/specs/ERC4626Sandwich.spec" + "verify": "ERC4626Harness:fv/specs/ERC4626Donation.spec" } diff --git a/fv/specs/ERC4626Donation.spec b/fv/specs/ERC4626Donation.spec new file mode 100644 index 00000000000..03250c0573e --- /dev/null +++ b/fv/specs/ERC4626Donation.spec @@ -0,0 +1,51 @@ +// 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(); + 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; +} diff --git a/fv/specs/ERC4626Offset.spec b/fv/specs/ERC4626Offset.spec index db08679d570..b8ff582f6b0 100644 --- a/fv/specs/ERC4626Offset.spec +++ b/fv/specs/ERC4626Offset.spec @@ -1,17 +1,16 @@ -// Tier 4: the same claims, with the decimals offset left symbolic. +// 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 symbolic. That turns a constant -// into an EXP over a symbolic exponent, a shape the rest of the suite never exercises. It turned -// out to be tractable unaided: nothing here abstracts 10**offset behind a ghost and no rule needs -// the offset bounded, so the tier carries no assumption the rest of the suite does not already. +// 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 therefore claims about offsets 0 through 77. +// prunes those paths. The rules here are claims about offsets 0 through 77. // -// The donation sandwich is also re-proved at a symbolic offset, by ERC4626OffsetSandwich.conf -// pointing the unchanged ERC4626Sandwich.spec at this file's harness. +// 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"; @@ -21,13 +20,13 @@ methods { } /* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Vacuity guard: the offset is genuinely symbolic, and a live vault is reachable at a nonzero one │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Vacuity guard: the offset is genuinely symbolic, and a live vault is reachable at a nonzero one │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -/// Without this, a rule below could pass because the scene admits no nonzero offset at all, which -/// would make the whole tier a restatement of what the zero-offset harness already proves. +/// 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; @@ -36,52 +35,47 @@ rule offsetIsGenuinelySymbolic(uint256 shares) { } /* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P1 at a symbolic offset: the vault is never over-committed │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P1: the vault is never over-committed - every outstanding share is redeemable simultaneously │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -/// The zero-offset proof of this reduces to 0 < (A+1)K, which holds for every K >= 1, so P1 should -/// carry to a symbolic offset unchanged, which is what makes it the right first check: it is the -/// cheapest rule in the suite, so a red here would mean the prover cannot handle a symbolic -/// exponent rather than that the property is harder. -rule vaultNeverOvercommittedAnyOffset() { +/// 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 │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ What the offset is FOR: it prices the inflation attack, and only a symbolic offset can say so │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -/// The suite's other rules establish that the vault is sound. None of them establishes that the -/// offset buys anything, because at offset 0 it is the identity - and soundness is not what the -/// offset is for. 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. +/// 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. /// -/// Stated exactly: a victim is only robbed if their deposit rounds to zero shares, and +/// 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. So the victim loses a, and whoever set the vault up to do it had -/// already sunk at least a * 10^offset into it. The offset is the multiplier between the two. +/// T >= 0 that forces A >= a*K: the victim loses a, and whoever set the vault up had already sunk at +/// least a * 10^offset into it. The offset is the multiplier between the two. /// -/// The bound is tight rather than slack - A = a*K is reachable - so it is not passing for free. -/// At offset 0 it degrades to A >= a, which is true and worthless. Its strength IS the offset, and -/// it is violated by a mutation that drops the offset from the share conversion. +/// 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()); } - -/// Guards the rule above against vacuity: if no state lets a nonzero deposit round to zero shares, -/// the bound holds over an empty set. It has to be reachable, because ERC4626 is explicit that the -/// mitigation does not fully prevent the attack. -rule victimCanBeRobbedAtAnyOffset(uint256 assets) { - require sane(); - require assets > 0; - satisfy previewDeposit(assets) == 0; -} diff --git a/fv/specs/ERC4626OffsetSandwich.conf b/fv/specs/ERC4626OffsetDonation.conf similarity index 82% rename from fv/specs/ERC4626OffsetSandwich.conf rename to fv/specs/ERC4626OffsetDonation.conf index b12d1e8fbe9..568198749b6 100644 --- a/fv/specs/ERC4626OffsetSandwich.conf +++ b/fv/specs/ERC4626OffsetDonation.conf @@ -4,7 +4,7 @@ "fv/harnesses/ERC4626OffsetHarness.sol" ], "global_timeout": 1800, - "msg": "ERC4626 tier 4: donation sandwich at a symbolic decimals offset", + "msg": "ERC4626 tier 4: donation attack at a symbolic decimals offset", "optimistic_loop": true, "parametric_contracts": [ "ERC4626OffsetHarness" @@ -16,5 +16,5 @@ "rule_sanity": "basic", "smt_timeout": "1200", "url_visibility": "public", - "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Sandwich.spec" + "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Donation.spec" } diff --git a/fv/specs/ERC4626Sandwich.spec b/fv/specs/ERC4626Sandwich.spec deleted file mode 100644 index 2da148ead2a..00000000000 --- a/fv/specs/ERC4626Sandwich.spec +++ /dev/null @@ -1,71 +0,0 @@ -// Kept out of ERC4626.spec so that its tuned config does not drag the whole tier-1 sweep along with -// it. The scope this rule is proved under is narrower than the property's usual statement; see the -// rule's own note. -// -// Two configs verify this file against two harnesses: ERC4626Sandwich.conf at a zero decimals -// offset, ERC4626OffsetSandwich.conf at a symbolic one. Nothing here mentions the offset, so the -// same rule text carries over unchanged. - -import "ERC4626Base.spec"; -import "helpers/erc20-supply.spec"; - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ P7: the donation sandwich is not profitable against a fresh vault │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -/// The inflation/donation-frontrunning 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 whole sequence captures "never profits" in one assertion, with no separate accounting -/// of what they paid. -/// -/// Scoped to a vault that starts empty, which is both what the virtual-shares mitigation claims and -/// the only scope in which the claim is true. Starting from an arbitrary (totalSupply, totalAssets) -/// admits states that are already manipulated - one share outstanding against a large asset balance, -/// say - where an attacker profits without donating anything, because the price was inflated before -/// the sequence began. Attributing that to this contract's rounding would be wrong: the contract -/// documents that empty and nearly-empty vaults are the hazard and directs deployers to seed them. -/// -/// Because totalSupply starts at zero, the attacker necessarily starts with no shares, so redeeming -/// their whole balance redeems only what this sequence minted. -rule donationSandwichNeverProfits(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) { - require sane(); - require nonpayable(eAtt) && nonpayable(eVic); - require noVirtualOverflow(); - 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; -} - -/// Vacuity guard for the rule above: the four-call sequence has to be constructible at all, or its -/// green means nothing. -rule sandwichScenarioIsReachable(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) { - require sane(); - require nonpayable(eAtt) && nonpayable(eVic); - require eAtt.msg.sender != eVic.msg.sender; - require eAtt.msg.sender != currentContract && eVic.msg.sender != currentContract; - require totalSupply() == 0 && totalAssets() == 0; - - deposit(eAtt, a1, eAtt.msg.sender); - donate(eAtt, d); - deposit(eVic, a2, eVic.msg.sender); - satisfy true; -} diff --git a/fv/specs/ERC4626_rest.conf b/fv/specs/ERC4626_rest.conf deleted file mode 100644 index 18dbd339697..00000000000 --- a/fv/specs/ERC4626_rest.conf +++ /dev/null @@ -1,35 +0,0 @@ -{ - "build_cache": true, - "exclude_rule": [ - "setupIsSatisfiable", - "totalSupplyIsSumOfBalances", - "vaultNeverOvercommitted", - "roundTripNeverCreatesValue", - "roundingGapIsAtMostOne", - "depositGapCanBeOne", - "mintGapCanBeOne", - "maxBoundaryIsConsistent", - "redeemMaxNeverReverts", - "withdrawMaxNeverReverts", - "depositConserves", - "mintConserves", - "withdrawConserves", - "redeemConserves", - "depositIsNotSplittable", - "withdrawIsNotSplittable", - "holdingBackAcrossDonationDoesNotPay" - ], - "files": [ - "fv/harnesses/ERC4626Harness.sol" - ], - "global_timeout": 600, - "msg": "ERC4626 complement shard: the builtin sanity rule, plus anything not named in ERC4626.conf", - "optimistic_loop": true, - "parametric_contracts": [ - "ERC4626Harness" - ], - "process": "emv", - "rule_sanity": "basic", - "url_visibility": "public", - "verify": "ERC4626Harness:fv/specs/ERC4626.spec" -} From d50cf9b21fba0c7ea668412212c9ef4baa34c336 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Fri, 28 Aug 2026 19:44:32 -0300 Subject: [PATCH 15/20] fv: clarify the offset-pricing note in ERC4626Offset.spec Co-Authored-By: Claude Fable 5 --- fv/specs/ERC4626Offset.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fv/specs/ERC4626Offset.spec b/fv/specs/ERC4626Offset.spec index b8ff582f6b0..6e8a22f9eca 100644 --- a/fv/specs/ERC4626Offset.spec +++ b/fv/specs/ERC4626Offset.spec @@ -68,8 +68,8 @@ rule vaultNeverOvercommitted() { /// /// 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: the victim loses a, and whoever set the vault up had already sunk at -/// least a * 10^offset into it. The offset is the multiplier between the two. +/// 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. From 9227618ca1b61ca565ea8368c794f92e3ea2a769 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Fri, 28 Aug 2026 20:06:47 -0300 Subject: [PATCH 16/20] fv: link the timeout ledger without line anchors Co-Authored-By: Claude Fable 5 --- fv/specs/ERC4626.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 687d050850b..d12f521c480 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -157,7 +157,7 @@ rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// in terms of the remaining balance the direction is the same as deposit. /// /// NOT DISCHARGED: excluded from every config, see the -/// [ledger](../../.github/workflows/formal-verification.yml#L61-L79). +/// [timeout ledger](../../.github/workflows/formal-verification.yml). rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { require sane(); require nonpayable(e); @@ -189,7 +189,7 @@ rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// never gains shares over committing it all at once. /// /// NOT DISCHARGED: excluded from every config, see the -/// [ledger](../../.github/workflows/formal-verification.yml#L61-L79). +/// [timeout ledger](../../.github/workflows/formal-verification.yml). rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { require sane(); require nonpayable(e); From eea5a38552c9f3b5b710e195c55359dffaed52c3 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Sat, 29 Aug 2026 02:35:42 -0300 Subject: [PATCH 17/20] fv: point the timeout-ledger links at fv-certora.yml Co-Authored-By: Claude Fable 5 --- fv/specs/ERC4626.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index d12f521c480..21f65eb2af2 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -157,7 +157,7 @@ rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// in terms of the remaining balance the direction is the same as deposit. /// /// NOT DISCHARGED: excluded from every config, see the -/// [timeout ledger](../../.github/workflows/formal-verification.yml). +/// [timeout ledger](../../.github/workflows/fv-certora.yml). rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { require sane(); require nonpayable(e); @@ -189,7 +189,7 @@ rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// never gains shares over committing it all at once. /// /// NOT DISCHARGED: excluded from every config, see the -/// [timeout ledger](../../.github/workflows/formal-verification.yml). +/// [timeout ledger](../../.github/workflows/fv-certora.yml). rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { require sane(); require nonpayable(e); From 600561b52d403d7f989ac764a250e671963f2ba9 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 28 Sep 2026 13:07:45 -0300 Subject: [PATCH 18/20] fv: declare the patched package in the ERC4626 configs Matches the other configs: declaring a package skips certora-cli's package auto-detection, which aborts on the duplicated `hardhat` key whenever forge is on PATH. Co-Authored-By: Claude Opus 5.5 --- fv/specs/ERC4626.conf | 3 +++ fv/specs/ERC4626Donation.conf | 3 +++ fv/specs/ERC4626Offset.conf | 3 +++ fv/specs/ERC4626OffsetDonation.conf | 3 +++ fv/specs/ERC4626_split.conf | 3 +++ 5 files changed, 15 insertions(+) diff --git a/fv/specs/ERC4626.conf b/fv/specs/ERC4626.conf index cd92df735b9..abcff5f6c6b 100644 --- a/fv/specs/ERC4626.conf +++ b/fv/specs/ERC4626.conf @@ -11,6 +11,9 @@ "global_timeout": 600, "msg": "ERC4626 tier 1: everything but the anti-splitting rules", "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], "parametric_contracts": [ "ERC4626Harness" ], diff --git a/fv/specs/ERC4626Donation.conf b/fv/specs/ERC4626Donation.conf index 3a403f67a80..e80179f58f0 100644 --- a/fv/specs/ERC4626Donation.conf +++ b/fv/specs/ERC4626Donation.conf @@ -6,6 +6,9 @@ "global_timeout": 1800, "msg": "ERC4626 tier 3: donation attack non-profitability", "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], "parametric_contracts": [ "ERC4626Harness" ], diff --git a/fv/specs/ERC4626Offset.conf b/fv/specs/ERC4626Offset.conf index f2bad60293c..eb5018ca2d8 100644 --- a/fv/specs/ERC4626Offset.conf +++ b/fv/specs/ERC4626Offset.conf @@ -6,6 +6,9 @@ "global_timeout": 600, "msg": "ERC4626 tier 4: symbolic decimals offset", "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], "parametric_contracts": [ "ERC4626OffsetHarness" ], diff --git a/fv/specs/ERC4626OffsetDonation.conf b/fv/specs/ERC4626OffsetDonation.conf index 568198749b6..c2849c91c7a 100644 --- a/fv/specs/ERC4626OffsetDonation.conf +++ b/fv/specs/ERC4626OffsetDonation.conf @@ -6,6 +6,9 @@ "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" ], diff --git a/fv/specs/ERC4626_split.conf b/fv/specs/ERC4626_split.conf index 17866402d55..8fd78e2baed 100644 --- a/fv/specs/ERC4626_split.conf +++ b/fv/specs/ERC4626_split.conf @@ -7,6 +7,9 @@ "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" ], From f4b085e9a29b0b608048778fdcc999024864c7a3 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 28 Sep 2026 14:14:35 -0300 Subject: [PATCH 19/20] fv: move the ERC4626 timeout notes onto the rules The two rules that time out now say so where they are declared, with the command to re-attempt them. The command carries the timeouts of the recorded run, which ERC4626_split.conf does not set. The workflow is left untouched. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/fv-certora.yml | 20 -------------------- fv/specs/ERC4626.spec | 13 +++++++++---- fv/specs/ERC4626Base.spec | 4 ++-- 3 files changed, 11 insertions(+), 26 deletions(-) diff --git a/.github/workflows/fv-certora.yml b/.github/workflows/fv-certora.yml index 218f78410f9..667fa250bd3 100644 --- a/.github/workflows/fv-certora.yml +++ b/.github/workflows/fv-certora.yml @@ -146,23 +146,3 @@ jobs: run: | [[ $IDENTIFY = success ]] || { echo "::error::could not work out which configs to run"; exit 1; } [[ $VERIFY = success || $VERIFY = skipped ]] || { echo "::error::verification $VERIFY"; exit 1; } - -# ┌────────────────────────────────────────────────────────────────────────────────────────┐ -# │ Timeout ledger: rules that are NOT proved. Excluded from every config, so their │ -# │ absence from a green run is not a pass. Re-attempt manually with the commands below. │ -# └────────────────────────────────────────────────────────────────────────────────────────┘ -# -# ERC4626 -- both hold under exhaustive small-value and large random sampling, so these are -# solver cost rather than defects. Last attempted with nonlinear arithmetic forced, splitting -# off, a ten-seed solver race, smt_timeout 1500 and global_timeout 3600. -# -# certoraRun fv/specs/ERC4626_split.conf --rule withdrawIsNotSplittable -# https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 -# timed out at 3003s; its strictness witness verifies in 9s -# -# certoraRun fv/specs/ERC4626_split.conf --rule holdingBackAcrossDonationDoesNotPay -# https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 -# timed out at 1504s; its arithmetic core verifies in ~1s in closed form, so the cost is -# the five-operation replay rather than the share math -# -# What the suite assumes rather than proves is recorded at the top of fv/specs/ERC4626Base.spec. diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec index 21f65eb2af2..dd2e473c953 100644 --- a/fv/specs/ERC4626.spec +++ b/fv/specs/ERC4626.spec @@ -156,8 +156,10 @@ rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// than one: the split must never burn fewer shares than the one-shot. Burning more leaves less, so /// in terms of the remaining balance the direction is the same as deposit. /// -/// NOT DISCHARGED: excluded from every config, see the -/// [timeout ledger](../../.github/workflows/fv-certora.yml). +/// NOT PROVED: times out (3003s) and is excluded from every config. Holds under exhaustive +/// small-value and large random sampling; the `satisfy` alone verifies in 9s. Re-attempt with: +/// certoraRun fv/specs/ERC4626_split.conf --rule withdrawIsNotSplittable --global_timeout 3600 --smt_timeout 1500 +/// https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { require sane(); require nonpayable(e); @@ -188,8 +190,11 @@ rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { /// means rather than a flaw. The claim is that holding part of a deposit back across a donation /// never gains shares over committing it all at once. /// -/// NOT DISCHARGED: excluded from every config, see the -/// [timeout ledger](../../.github/workflows/fv-certora.yml). +/// NOT PROVED: times out (1504s) and is excluded from every config. Holds under exhaustive +/// small-value and large random sampling; the share math alone verifies in ~1s, so the cost is +/// replaying five calls. Re-attempt with: +/// certoraRun fv/specs/ERC4626_split.conf --rule holdingBackAcrossDonationDoesNotPay --global_timeout 3600 --smt_timeout 1500 +/// https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { require sane(); require nonpayable(e); diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec index 826fd85f98b..ca57d509100 100644 --- a/fv/specs/ERC4626Base.spec +++ b/fv/specs/ERC4626Base.spec @@ -18,8 +18,8 @@ // 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 recorded in the timeout ledger in the formal-verification -// workflow, not here. +// 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"; From f14223e85d6b2f4f271519ac9399ebbf88bd85e1 Mon Sep 17 00:00:00 2001 From: Ezequiel Perez Date: Mon, 28 Sep 2026 14:15:09 -0300 Subject: [PATCH 20/20] fv: prove the sum-of-balances invariant for the offset harness donationAttackNeverProfits assumes totalSupplyIsSumOfBalances, but only the zero-offset harness proved it, so ERC4626OffsetDonation.conf relied on an unchecked premise. ERC4626Offset.conf now proves it for the offset harness, under its default solver settings rather than the donation configs' tuned ones. Co-Authored-By: Claude Opus 5.5 --- fv/specs/ERC4626Donation.spec | 1 + fv/specs/ERC4626Offset.spec | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/fv/specs/ERC4626Donation.spec b/fv/specs/ERC4626Donation.spec index 03250c0573e..73a1bd44750 100644 --- a/fv/specs/ERC4626Donation.spec +++ b/fv/specs/ERC4626Donation.spec @@ -28,6 +28,7 @@ rule donationAttackNeverProfits(env eAtt, env eVic, uint256 a1, uint256 d, uint2 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; diff --git a/fv/specs/ERC4626Offset.spec b/fv/specs/ERC4626Offset.spec index 6e8a22f9eca..5624654d8fa 100644 --- a/fv/specs/ERC4626Offset.spec +++ b/fv/specs/ERC4626Offset.spec @@ -13,6 +13,11 @@ // 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;