Certora/hub verification

.github/workflows/certora.yml

@@ -0,0 +1,51 @@
+name: Certora Prover Workflow
+
+env:
+  CONFIGS: |
+    certora/conf/libs/LibBit.conf
+    certora/conf/libs/Math.conf
+    certora/conf/libs/SharesMath.conf
+    certora/conf/Hub.conf
+    certora/conf/HubAdditivity.conf
+    certora/conf/HubAccrueIntegrity.conf
+    certora/conf/HubAccrueUnrealizedFee.conf
+    certora/conf/HubIntegrity.conf
+    certora/conf/HubValidState.conf
+on:
+  pull_request:
+    branches:
+      - main
+      - certora
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      # (Optional) Add installation steps for your project
+      - name: Setup Node.js
+        uses: actions/setup-node@v4
+      - name: Install dependencies
+        run: npm install
+
+      # Run Certora Prover
+      - uses: Certora/certora-run-action@v2
+        with:
+          # Add your configurations as lines, each line is separated.
+          # Specify additional options for each configuration by adding them after the configuration.
+          configurations: ${{ env.CONFIGS }}
+          solc-versions: 0.8.28
+          job-name: "Verified Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.gitignore

@@ -20,5 +20,8 @@ broadcast/
 lcov*
 
 report/
-
 .DS_Store
+π
+# certora internal artifacts
+.certora_internal/
+

certora/compileAll.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+for FILE in certora/conf/*.conf
+do
+    echo ${FILE}
+    certoraRun ${FILE} --compilation_steps_only
+done

certora/conf/Hub.conf

@@ -0,0 +1,18 @@
+{
+  "files": [
+    "src/hub/Hub.sol",
+    "tests/mocks/WadRayMathWrapper.sol" ,
+    "certora/harness/SummaryLibrary.sol"
+  ],
+  "verify": "Hub:certora/spec/Hub.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "AAVE V4 Hub",
+  "parametric_contracts" : "Hub",
+  "solc_via_ir" : true,  
+  "build_cache" : true,
+  "smt_timeout": "7200",
+  // rules that are timing out and processed separately
+  "exclude_rule": ["noChangeToOtherSpoke","supplyExchangeRateIsMonotonic"]
+  }

certora/conf/HubAccrueIntegrity.conf

@@ -0,0 +1,27 @@
+{
+  "files": [
+    "certora/harness/HubHarness.sol",
+    "tests/mocks/WadRayMathWrapper.sol",
+    "certora/harness/MathWrapper.sol",
+  ],
+  "verify": "HubHarness:certora/spec/HubAccrueIntegrity.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "HubHarness - AccrueIntegrity",
+  "parametric_contracts" : ["HubHarness"],
+  "solc_via_ir" : true,
+  "prover_args": [
+		"-oldSplitParallel",
+		"true",
+		"-dontStopAtFirstSplitTimeout",
+		"true",
+		"-splitParallelTimelimit",
+		"7000",
+		"-splitParallelInitialDepth",
+		"3",
+		"-numOfParallelSplits",
+		"7"
+	],
+  "independent_satisfy" : true
+  }

certora/conf/HubAccrueSupplyRate.conf

@@ -0,0 +1,28 @@
+{
+	"files": [
+		"certora/harness/HubHarness.sol",
+		"tests/mocks/WadRayMathWrapper.sol",
+		"certora/harness/MathWrapper.sol"
+	],
+	"loop_iter": 3,
+	"msg": "HubAccrue supply rate",
+	"multi_assert_check": true,
+	"optimistic_loop": true,
+	"parametric_contracts": [
+		"HubHarness"
+	],
+	"prover_args": [
+		"-splitParallel",
+		"true",
+		"-dontStopAtFirstSplitTimeout",
+		"true"
+	],
+	"rule": [
+		"unrealizedFeeSharesSupplyRate"
+	],
+	// no need for sanity check as the rule ends in a satisfy command	
+	"rule_sanity": "none",
+	"smt_timeout": 7200,
+	"solc_via_ir": true,
+	"verify": "HubHarness:certora/spec/HubAccrueSupplyRate.spec"
+}

certora/conf/HubAccrueUnrealizedFee.conf

@@ -0,0 +1,14 @@
+{
+  "files": [
+    "certora/harness/HubHarness.sol",
+    "tests/mocks/WadRayMathWrapper.sol",
+    "certora/harness/MathWrapper.sol",
+  ],
+  "verify": "HubHarness:certora/spec/HubAccrueUnrealizedFee.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "HubHarness - AccrueIntegrity Unrealized Fee",
+  "parametric_contracts" : ["HubHarness"],
+  "solc_via_ir" : true,
+  }

certora/conf/HubAdditivity.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/harness/HubHarness.sol",
+    "tests/mocks/WadRayMathWrapper.sol",
+    "certora/harness/SummaryLibrary.sol"
+  ],
+  "verify": "HubHarness:certora/spec/HubAdditivity.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "Hub Additivity",
+  "parametric_contracts" : "HubHarness",
+  "solc_via_ir" : true,
+  "independent_satisfy" : true,
+  "exclude_rule": ["drawAdditivity","restoreAdditivity","reportDeficitAdditivity"]
+  }

certora/conf/HubIntegrity.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "src/hub/Hub.sol",
+    "tests/mocks/WadRayMathWrapper.sol",
+    "certora/harness/SummaryLibrary.sol"
+  ],
+  "verify": "Hub:certora/spec/HubIntegrityRules.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "Hub  integrityRules",
+  "parametric_contracts" : "Hub",
+  "solc_via_ir" : true,
+  "independent_satisfy" : true
+  }

certora/conf/HubValidState.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "src/hub/Hub.sol",
+    "tests/mocks/WadRayMathWrapper.sol" ,
+    "certora/harness/SummaryLibrary.sol"
+  ],
+  "verify": "Hub:certora/spec/HubValidState.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "AAVE V4 Hub - validState  invariants",
+  "parametric_contracts" : "Hub",
+  "solc_via_ir" : true,  
+  "build_cache" : true
+  }

certora/conf/libs/LibBit.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harness/LibBitHarness.sol"
+    ],
+    "precise_bitwise_ops" : true,
+    "msg" : "LibBit library",
+    "verify": "LibBitHarness:certora/spec/libs/LibBit.spec",
+    "smt_timeout": "7200",
+	"prover_args": [
+		"-split",
+		"false"
+	]
+}

certora/conf/libs/Math.conf

@@ -0,0 +1,8 @@
+{
+  "files": [
+    "certora/harness/MathWrapper.sol" 
+  ],
+  "verify": "MathWrapper:certora/spec/libs/Math.spec",
+  "rule_sanity" : "basic",
+  "msg": "Math function equivalence",
+  }

certora/conf/libs/SharesMath.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "certora/harness/HubHarness.sol",
+    "tests/mocks/WadRayMathWrapper.sol",
+  ],
+  "verify": "HubHarness:certora/spec/libs/SharesMath.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "msg": "HubHarness - SharesMath",
+  "parametric_contracts" : ["HubHarness"],
+  "solc_via_ir" : true,
+  "independent_satisfy" : true,
+  "build_cache" : true
+  }

certora/harness/HubHarness.sol

@@ -0,0 +1,60 @@
+import '../../src/hub/Hub.sol';
+import {AssetLogic} from 'src/hub/libraries/AssetLogic.sol';
+import {SharesMath} from 'src/hub/libraries/SharesMath.sol';
+
+pragma solidity ^0.8.0;
+
+contract HubHarness is Hub {
+  using AssetLogic for Asset;
+
+  constructor(address authority_) Hub(authority_) {
+    // Intentionally left blank
+  }
+
+  function accrueInterest(uint256 assetId) external {
+    Asset storage asset = _assets[assetId];
+
+    asset.accrue(_spokes, assetId);
+  }
+
+  function toSharesDown(
+    uint256 assets,
+    uint256 totalAssets,
+    uint256 totalShares
+  ) external pure returns (uint256) {
+    return SharesMath.toSharesDown(assets, totalAssets, totalShares);
+  }
+
+  function toAssetsDown(
+    uint256 shares,
+    uint256 totalAssets,
+    uint256 totalShares
+  ) external pure returns (uint256) {
+    return SharesMath.toAssetsDown(shares, totalAssets, totalShares);
+  }
+
+  function toSharesUp(
+    uint256 assets,
+    uint256 totalAssets,
+    uint256 totalShares
+  ) external pure returns (uint256) {
+    return SharesMath.toSharesUp(assets, totalAssets, totalShares);
+  }
+
+  function toAssetsUp(
+    uint256 shares,
+    uint256 totalAssets,
+    uint256 totalShares
+  ) external pure returns (uint256) {
+    return SharesMath.toAssetsUp(shares, totalAssets, totalShares);
+  }
+
+  function getAssetSuppliedAmountUp(uint256 assetId) external view returns (uint256) {
+    return _assets[assetId].toAddedAssetsUp(_assets[assetId].addedShares);
+  }
+
+  function unrealizedFeeShares(uint256 assetId) external view returns (uint256) {
+    Asset storage asset = _assets[assetId];
+    return asset.unrealizedFeeShares();
+  }
+}

certora/harness/LibBitHarness.sol

@@ -0,0 +1,25 @@
+import {LibBit} from '../../src/dependencies/solady/LibBit.sol';
+
+pragma solidity ^0.8.0;
+
+contract LibBitHarness {
+  function popCount(uint256 x) external pure returns (uint256 c) {
+    return LibBit.popCount(x);
+  }
+
+  function fls(uint256 x) external pure returns (uint256 r) {
+    return LibBit.fls(x);
+  }
+
+  function isBitTrue(uint256 x, uint16 pos) public pure returns (bool) {
+    return ((x >> pos) & 1) == 1;
+  }
+
+  function changeOneBit(uint256 x, uint16 pos) external pure returns (uint256 c) {
+    if (isBitTrue(x, pos)) {
+      return x & ~(1 << pos);
+    } else {
+      return x | (1 << pos);
+    }
+  }
+}