Add formal verification for ERC-4626

.github/workflows/fv-certora.yml

@@ -44,6 +44,10 @@ jobs:
           java: 'on'
           python: 'on'
           python-requirements: 'fv-requirements.txt'
+          # certoraRun reads `forge remappings` when forge is present, which emits a `hardhat`
+          # key that package.json also provides, and it rejects the duplicate. This job has no
+          # use for forge.
+          foundry: 'off'
       - name: identify specs that need to be run
         id: arguments
         env:
@@ -52,13 +56,32 @@ jobs:
         run: |
           if [[ ${{ github.event_name }} = 'pull_request_target' && ${{ contains(github.event.pull_request.labels.*.name, 'formal-verification-force-all') }} = 'false' ]];
           then
-            # Spec names come from the file names of a pull request that may be untrusted, and end
-            # up on a command line downstream. Anything that is not a plain name is dropped here.
-            RESULT=$(git diff "$HEAD_SHA".."$BASE_SHA" --name-only -- 'fv/specs/*.spec' | while IFS= read -r file; do
-              [[ -f $file ]] || continue
-              name=$(basename "${file%.spec}")
-              [[ $name =~ ^[A-Za-z0-9_-]+$ ]] && echo "$name" || echo "Ignoring spec with unexpected name: $name" >&2
-            done | tr "\n" " ")
+            # Map each changed spec to the configs that verify it, following imports: a spec that
+            # no config names (a base, a helper, a methods file) is verified through the specs that
+            # import it, transitively. Imports are relative to the importing file's directory.
+            importers() {
+              find fv/specs -name '*.spec' | while IFS= read -r spec; do
+                dir=${spec%/*}
+                sed -n 's/^import "\([^"]*\)".*/\1/p' "$spec" | while IFS= read -r imp; do
+                  if [[ "$dir/${imp#./}" == "$1" ]]; then echo "$spec"; fi
+                done
+              done
+            }
+            specs=$(git diff "$HEAD_SHA".."$BASE_SHA" --name-only -- 'fv/specs/*.spec' | while IFS= read -r file; do if [[ -f $file ]]; then echo "$file"; fi; done)
+            while :; do
+              next=$({ echo "$specs"; while IFS= read -r file; do if [[ -n $file ]]; then importers "$file"; fi; done <<< "$specs"; } | sort -u)
+              if [[ $next == "$specs" ]]; then break; fi
+              specs=$next
+            done
+            confs=$(while IFS= read -r file; do if [[ -n $file ]]; then grep -lF "$file" fv/specs/*.conf || true; fi; done <<< "$specs" | sort -u)
+            if [[ -n $specs && -z $confs ]]; then echo "Changed specs are verified by no config, directly or through an importer." >&2; fi
+            # Config names come from the file names of a pull request that may be untrusted, and
+            # end up on a command line downstream. Anything that is not a plain name is dropped.
+            RESULT=$(while IFS= read -r conf; do
+              if [[ -z $conf ]]; then continue; fi
+              name=${conf##*/}; name=${name%.conf}
+              if [[ $name =~ ^[A-Za-z0-9_-]+$ ]]; then echo "$name"; else echo "Ignoring config with unexpected name: $name" >&2; fi
+            done <<< "$confs" | tr "\n" " ")
           else
             RESULT='--all'
           fi
@@ -71,3 +94,23 @@ jobs:
           make -C fv apply
           read -r -a specs <<< "$SPEC_ARGUMENTS"
           node fv/run.js "${specs[@]}" -p 1 -v >> "$GITHUB_STEP_SUMMARY"
+
+      # ┌────────────────────────────────────────────────────────────────────────────────────────┐
+      # │ 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.

fv/harnesses/ERC4626Harness.sol

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

fv/harnesses/ERC4626OffsetHarness.sol

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

fv/specs/ERC4626.conf

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