From 95731c7d6e33ce66ed4b8de19bf19457ec1d0837 Mon Sep 17 00:00:00 2001 From: shellygr Date: Thu, 18 Dec 2025 10:16:45 +0200 Subject: [PATCH 1/2] Certora formal verification rules (#1069) --- .github/workflows/certora.yml | 79 +++ .gitignore | 3 +- certora/README.md | 384 +++++++++++++++ certora/compileAll.sh | 7 + certora/conf/Hub.conf | 17 + certora/conf/HubAccrueIntegrity.conf | 27 + certora/conf/HubAccrueSupplyRate.conf | 19 + certora/conf/HubAccrueUnrealizedFee.conf | 13 + certora/conf/HubAdditivity.conf | 15 + certora/conf/HubIntegrity.conf | 14 + certora/conf/HubValidState.conf | 15 + certora/conf/HubValidState_totalAssets.conf | 18 + certora/conf/Liquidation.conf | 20 + certora/conf/Spoke.conf | 21 + certora/conf/SpokeHealthCheck.conf | 19 + certora/conf/SpokeUserIntegrity.conf | 18 + certora/conf/SpokeWithHub.conf | 30 ++ certora/conf/Spoke_noCollateralNoDebt.conf | 27 + certora/conf/libs/LibBit.conf | 14 + certora/conf/libs/Math.conf | 9 + certora/conf/libs/PositionStatus.conf | 12 + certora/conf/libs/Premium.conf | 10 + certora/conf/libs/SharesMath.conf | 17 + .../libs/VerifySymbolicPositionStatus.conf | 17 + certora/harness/HubHarness.sol | 57 +++ certora/harness/LibBitHarness.sol | 25 + certora/harness/MathWrapper.sol | 88 ++++ certora/harness/PremiumWrapper.sol | 15 + certora/runAll.sh | 7 + certora/spec/Hub.spec | 210 ++++++++ certora/spec/HubAccrueIntegrity.spec | 288 +++++++++++ certora/spec/HubAccrueSupplyRate.spec | 208 ++++++++ certora/spec/HubAccrueUnrealizedFee.spec | 71 +++ certora/spec/HubAdditivity.spec | 236 +++++++++ certora/spec/HubBase.spec | 31 ++ certora/spec/HubIntegrityRules.spec | 107 ++++ certora/spec/HubValidState.spec | 466 ++++++++++++++++++ certora/spec/Spoke.spec | 293 +++++++++++ certora/spec/SpokeBase.spec | 129 +++++ certora/spec/SpokeHealthCheck.spec | 71 +++ certora/spec/SpokeHubIntegrity.spec | 240 +++++++++ certora/spec/SpokeUserIntegrity.spec | 107 ++++ certora/spec/common.spec | 57 +++ certora/spec/libs/LibBit.spec | 59 +++ certora/spec/libs/Math.spec | 231 +++++++++ certora/spec/libs/PositionStatus.spec | 187 +++++++ certora/spec/libs/Premium.spec | 40 ++ certora/spec/libs/SharesMath.spec | 147 ++++++ certora/spec/liquidation.spec | 1 + .../symbolicRepresentation/ERC20s_CVL.spec | 100 ++++ .../spec/symbolicRepresentation/Math_CVL.spec | 82 +++ .../symbolicRepresentation/SymbolicHub.spec | 134 +++++ .../SymbolicPositionStatus.spec | 137 +++++ .../VerifySymbolicPositionStatus.spec | 25 + 54 files changed, 4673 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/README.md create mode 100755 certora/compileAll.sh create mode 100644 certora/conf/Hub.conf create mode 100644 certora/conf/HubAccrueIntegrity.conf create mode 100644 certora/conf/HubAccrueSupplyRate.conf create mode 100644 certora/conf/HubAccrueUnrealizedFee.conf create mode 100644 certora/conf/HubAdditivity.conf create mode 100644 certora/conf/HubIntegrity.conf create mode 100644 certora/conf/HubValidState.conf create mode 100644 certora/conf/HubValidState_totalAssets.conf create mode 100644 certora/conf/Liquidation.conf create mode 100644 certora/conf/Spoke.conf create mode 100644 certora/conf/SpokeHealthCheck.conf create mode 100644 certora/conf/SpokeUserIntegrity.conf create mode 100644 certora/conf/SpokeWithHub.conf create mode 100644 certora/conf/Spoke_noCollateralNoDebt.conf create mode 100644 certora/conf/libs/LibBit.conf create mode 100644 certora/conf/libs/Math.conf create mode 100644 certora/conf/libs/PositionStatus.conf create mode 100644 certora/conf/libs/Premium.conf create mode 100644 certora/conf/libs/SharesMath.conf create mode 100644 certora/conf/libs/VerifySymbolicPositionStatus.conf create mode 100644 certora/harness/HubHarness.sol create mode 100644 certora/harness/LibBitHarness.sol create mode 100644 certora/harness/MathWrapper.sol create mode 100644 certora/harness/PremiumWrapper.sol create mode 100755 certora/runAll.sh create mode 100644 certora/spec/Hub.spec create mode 100644 certora/spec/HubAccrueIntegrity.spec create mode 100644 certora/spec/HubAccrueSupplyRate.spec create mode 100644 certora/spec/HubAccrueUnrealizedFee.spec create mode 100644 certora/spec/HubAdditivity.spec create mode 100644 certora/spec/HubBase.spec create mode 100644 certora/spec/HubIntegrityRules.spec create mode 100644 certora/spec/HubValidState.spec create mode 100644 certora/spec/Spoke.spec create mode 100644 certora/spec/SpokeBase.spec create mode 100644 certora/spec/SpokeHealthCheck.spec create mode 100644 certora/spec/SpokeHubIntegrity.spec create mode 100644 certora/spec/SpokeUserIntegrity.spec create mode 100644 certora/spec/common.spec create mode 100644 certora/spec/libs/LibBit.spec create mode 100644 certora/spec/libs/Math.spec create mode 100644 certora/spec/libs/PositionStatus.spec create mode 100644 certora/spec/libs/Premium.spec create mode 100644 certora/spec/libs/SharesMath.spec create mode 100644 certora/spec/liquidation.spec create mode 100644 certora/spec/symbolicRepresentation/ERC20s_CVL.spec create mode 100644 certora/spec/symbolicRepresentation/Math_CVL.spec create mode 100644 certora/spec/symbolicRepresentation/SymbolicHub.spec create mode 100644 certora/spec/symbolicRepresentation/SymbolicPositionStatus.spec create mode 100644 certora/spec/symbolicRepresentation/VerifySymbolicPositionStatus.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 000000000..abbb3bbd2 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,79 @@ +name: Certora Prover Workflow + +env: + CONFIGS: | + certora/conf/libs/LibBit.conf + certora/conf/libs/Math.conf + certora/conf/libs/Premium.conf + certora/conf/libs/SharesMath.conf + certora/conf/libs/VerifySymbolicPositionStatus.conf + certora/conf/libs/PositionStatus.conf + certora/conf/Hub.conf --exclude_rule noChangeToOtherSpoke supplyExchangeRateIsMonotonic + certora/conf/HubAdditivity.conf --exclude_rule drawAdditivity restoreAdditivity reportDeficitAdditivity + certora/conf/HubAccrueIntegrity.conf + certora/conf/HubAccrueUnrealizedFee.conf + certora/conf/HubAccrueSupplyRate.conf --exclude_rule previewRemoveByShares_withoutAccrue_time_monotonic previewAddByShares_withoutAccrue_time_monotonic + certora/conf/HubAccrueSupplyRate.conf --rule previewRemoveByShares_withoutAccrue_time_monotonic + certora/conf/HubAccrueSupplyRate.conf --rule previewRemoveByShares_withoutAccrue_time_monotonic + certora/conf/HubIntegrity.conf + certora/conf/HubValidState.conf --exclude_rule totalAssetsVsShares_eliminateDeficit + certora/conf/HubValidState.conf --rule totalAssetsVsShares_eliminateDeficit + certora/conf/HubValidState_totalAssets.conf + certora/conf/Spoke.conf --rule drawnSharesZero + certora/conf/Spoke.conf --exclude_rule noCollateralNoDebt drawnSharesZero increaseCollateralOrReduceDebtFunctions + certora/conf/SpokeHealthCheck.conf + certora/conf/SpokeUserIntegrity.conf + certora/conf/SpokeWithHub.conf --rule userDrawnShareConsistency + certora/conf/SpokeWithHub.conf --rule userPremiumShareConsistency + certora/conf/SpokeWithHub.conf --rule userPremiumOffsetConsistency + certora/conf/SpokeWithHub.conf --rule userSuppliedShareConsistency + certora/conf/SpokeWithHub.conf --exclude_rule userDrawnShareConsistency userPremiumShareConsistency userPremiumOffsetConsistency userSuppliedShareConsistency + ######### rules that are too long/flaky to run in ci, run manually ######### + #certora/conf/Hub.conf --rule supplyExchangeRateIsMonotonic + #certora/conf/Hub.conf --rule noChangeToOtherSpoke + #certora/conf/Spoke.conf --rule noCollateralNoDebt + #certora/conf/HubAdditivity.conf --rule drawAdditivity + #certora/conf/HubAdditivity.conf --rule restoreAdditivity + #certora/conf/HubAdditivity.conf --rule reportDeficitAdditivity + #certora/conf/HubAccrueSupplyRate.conf --rule previewRemoveByShares_withoutAccrue_time_monotonic previewAddByShares_withoutAccrue_time_monotonic + #### rules that are failing and waiting for fix + #certora/conf/Spoke.conf --rule increaseCollateralOrReduceDebtFunctions + +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 }} diff --git a/.gitignore b/.gitignore index 619603d4d..2898693f9 100644 --- a/.gitignore +++ b/.gitignore @@ -22,4 +22,5 @@ lcov* report/ .DS_Store -.venv/ \ No newline at end of file +.venv/ +.certora_internal/ diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..48a119a42 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,384 @@ +# Certora Formal Verification + +This folder contains the formal verification specifications for the Aave V4 protocol using the Certora Prover. + +## Folder Structure + +``` +certora/ +├── conf/ # Configuration files for running the prover +│ ├── libs/ # Library-specific configurations +│ └── *.conf # Main configuration files +├── harness/ # Solidity harness contracts for verification +│ ├── HubHarness.sol # Hub contract harness exposing internal functions +│ ├── LibBitHarness.sol # LibBit library harness +│ ├── MathWrapper.sol # Math library wrapper for verification +│ └── PremiumWrapper.sol # Premium library wrapper for verification +├── spec/ # CVL specification files +│ ├── libs/ # Library specifications +│ └── symbolicRepresentation/ # Symbolic representations for CVL +├── runAll.sh # Script to run all conf files +└── compileAll.sh # Script to compile all contracts +``` + +## Key Properties Verified + +The formal verification focuses on the following critical safety properties: + +### Solvency & Share Rate +- **Share Rate Monotonicity** - The exchange rate between shares and assets never decreases, protecting LP token holders +- **Total Assets ≥ Total Shares** - Ensures the protocol remains solvent +- **External Solvency** - Hub underlying balance always covers total added assets + +### Position Safety +- **No Collateral → No Debt** - Users without collateral cannot accumulate debt +- **Borrowing Flag Consistency** - Borrowing status accurately reflects drawn shares +- **Health Factor Maintenance** - User health stays above liquidation threshold after operations + +### State Consistency +- **Spoke Isolation** - Operations on one spoke don't affect other spokes +- **Sum Invariants** - Sum of spoke supplies/drawn shares equals totals +- **Reserve ID Validity** - Reserve mappings remain consistent + +### Accrue Integrity +- **Idempotency** - Calling accrue twice is equivalent to calling once +- **Index Monotonicity** - Interest indices only increase + +## Prerequisites + +1. Install the Certora Prover CLI: + ```bash + pip install certora-cli + ``` + +2. Set your Certora API key: + ```bash + export CERTORAKEY= + ``` + +## Running the Prover + +### Run All Configurations +```bash +./certora/runAll.sh +``` + +### Run a Single Configuration +```bash +certoraRun certora/conf/.conf +``` + +### Run a Specific Rule +```bash +certoraRun certora/conf/.conf --rule --msg "" +``` + +### Documentation +For more information on the Certora Prover and CVL specification language, see: +- [Certora Documentation](https://docs.certora.com/) +- [CVL Language Reference](https://docs.certora.com/en/latest/docs/cvl/index.html) +- [Certora Prover CLI](https://docs.certora.com/en/latest/docs/prover/cli/index.html) + +--- + +## Hub Specifications + +### `HubBase.spec` +**Base definitions for Hub specifications.** + +- **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `common.spec` +- **Purpose:** Contains safe assumptions and summarizations used across all Hub spec files +- **Key Summaries:** + - `calculateInterestRate` → NONDET + - `Premium.calculatePremiumRay` → CVL implementation + +### `Hub.spec` +**Main Hub verification rules.** + +- **Config:** `certora/conf/Hub.conf` +- **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `HubValidState.spec` +- **Purpose:** State change rules where validation functions are ignored, assuming `accrue` has been called +- **Key Summaries:** All `_validate*` functions → NONDET +- **Key Rules:** + - `supplyExchangeRateIsMonotonic` - Share exchange rate never decreases (critical for LP token safety) + - `noChangeToOtherSpoke` - Operations on one spoke don't affect other spokes' state + - `totalAssetsCompareToSuppliedAmount` - Total assets always >= total shares (solvency) + - `accrueWasCalled` - Ensures accrue is called before state-changing operations + + +### `HubValidState.spec` +**Hub valid state properties and invariants.** + +- **Config:** `certora/conf/HubValidState.conf`, `certora/conf/HubValidState_totalAssets.conf` +- **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `HubBase.spec` +- **Purpose:** Verifies invariants about the Hub's state, assuming a given drawnIndex and accrue was called +- **Key Features:** + - Ghost variables for tracking spoke supply, drawn amounts, and premium offsets + - Hooks on storage operations to maintain ghost consistency + - Sum invariants for spoke data +- **Key Rules/Invariants:** + - `solvency_external` - Hub underlying balance >= total added assets (external solvency) + - `totalAssetsVsShares` - Total assets always >= total shares (share rate >= 1) + - `sumOfSpokeSupply` - Sum of all spoke supplies equals total supply + - `sumOfSpokeDrawnShares` - Sum of all spoke drawn shares equals total drawn + - `premiumOffset_Integrity` - Premium offset tracking consistency +- **Additional Config:** `HubValidState_totalAssets.conf` runs `totalAssetsVsShares` with parallel splitting + +### `HubIntegrityRules.spec` +**Hub integrity verification rules.** + +- **Config:** `certora/conf/HubIntegrity.conf` +- **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `HubValidState.spec` +- **Purpose:** Verifies that state changes are consistent (e.g., add increases balances, remove decreases them) +- **Key Rules:** + - `nothingForZero_add` - Add operation increases balances + - `nothingForZero_remove` - Remove operation decreases balances + + +### `HubAccrueIntegrity.spec` +**Accrue function integrity proofs.** + +- **Config:** `certora/conf/HubAccrueIntegrity.conf` +- **Imports:** `HubBase.spec` +- **Purpose:** Unit test properties of `AssetLogic.accrue()` function +- **Key Rules:** + - `runningTwiceIsEquivalentToOne` - Idempotency of accrue + - Index monotonicity rules + - Interest rate calculation rules + +### `HubAccrueSupplyRate.spec` +**Supply rate verification.** + +- **Config:** `certora/conf/HubAccrueSupplyRate.conf` +- **Purpose:** Verifies supply rate calculations + +### `HubAccrueUnrealizedFee.spec` +**Unrealized fee verification.** + +- **Config:** `certora/conf/HubAccrueUnrealizedFee.conf` +- **Purpose:** Verifies unrealized fee calculations + +### `HubAdditivity.spec` +**Additivity properties of Hub operations.** + +- **Config:** `certora/conf/HubAdditivity.conf` +- **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `SharesMath.spec` +- **Purpose:** Verifies that splitting operations is less beneficial than single operations +- **Key Rules:** Additivity proofs for `add`, `remove`, `draw`, `restore`, `reportDeficit`, `eliminateDeficit` + + +--- + +## Spoke Specifications + +### `SpokeBase.spec` +**Base definitions for Spoke specifications.** + +- **Imports:** `Math_CVL.spec`, `SymbolicPositionStatus.spec`, `ERC20s_CVL.spec` +- **Purpose:** Safe assumptions and summarizations for all Spoke spec files +- **Key Summaries:** + - Sorting functions → CVL implementation + - Price functions → Symbolic representation + - Authority checks → NONDET + +### `Spoke.spec` +**Main Spoke verification rules.** + +- **Config:** `certora/conf/Spoke.conf`, `certora/conf/Spoke_noCollateralNoDebt.conf` +- **Imports:** `SpokeBase.spec` +- **Purpose:** Spoke-independent verification (no link to Hub) +- **Key Features:** + - Symbolic Hub summaries for external calls + - Index tracking per asset per block + - User position invariants +- **Key Rules/Invariants:** + - `isBorrowingIFFdrawnShares` - Borrowing flag set iff user has drawn shares + - `drawnSharesZero` - Zero drawn shares implies zero premium shares + - `noCollateralNoDebt` - User with no collateral cannot have debt (critical safety property) + - `validReserveId` - Reserve ID validity and consistency + - `increaseCollateralOrReduceDebtFunctions` - Functions either increase collateral or reduce debt + - `collateralFactorNotZero` - Borrowed reserves must have non-zero collateral factor + - `uniqueAssetIdPerReserveId` - Each reserve maps to unique asset +- **Additional Config:** `Spoke_noCollateralNoDebt.conf` runs `noCollateralNoDebt` with parallel splitting prover args + +### `SpokeHealthCheck.spec` +**Health factor verification.** + +- **Config:** `certora/conf/SpokeHealthCheck.conf` +- **Imports:** `SpokeBase.spec`, `SymbolicHub.spec` +- **Purpose:** Verifies that health factor is checked after position updates +- **Key Rules:** + - `userHealthStaysAboveThreshold` - Health factor maintained after operations + +### `SpokeUserIntegrity.spec` +**User position integrity.** + +- **Config:** `certora/conf/SpokeUserIntegrity.conf` +- **Purpose:** Verifies that only one user's account is updated at a time + +### `SpokeHubIntegrity.spec` +**Spoke-Hub integration verification.** + +- **Config:** `certora/conf/SpokeWithHub.conf` +- **Imports:** `SpokeBase.spec`, `HubValidState.spec` +- **Purpose:** Verifies consistency between Spoke user positions and Hub spoke data +- **Key Invariants:** + - `userDrawnShareConsistency` - User drawn shares match Hub records + - `userSuppliedShareConsistency` - User supplied shares match Hub records + - `userPremiumShareConsistency` - Premium shares consistency + - `userPremiumOffsetConsistency` - Premium offset consistency + +--- + +## Library Specifications + +### `libs/Math.spec` +**Mathematical function verification.** + +- **Config:** `certora/conf/libs/Math.conf` +- **Purpose:** Proves CVL representations match Solidity implementations +- **Verified Functions:** + - `mulDivDown`, `mulDivUp` + - `rayMulDown`, `rayMulUp`, `rayDivDown`, `rayDivUp` + - `wadDivDown`, `wadDivUp` + - `percentMulDown`, `percentMulUp` + - `fromRayUp`, `toRay` + +### `libs/SharesMath.spec` +**Shares math library verification.** + +- **Config:** `certora/conf/libs/SharesMath.conf` +- **Purpose:** Proves mathematical properties of share calculations +- **Key Rules:** + - Monotonicity of `toSharesUp`, `toSharesDown`, `toAssetsUp`, `toAssetsDown` + - Additivity properties + - Inverse relationships + +### `libs/LibBit.spec` +**Bit manipulation library verification.** + +- **Config:** `certora/conf/libs/LibBit.conf` + +### `libs/PositionStatus.spec` +**Position status verification.** + +- **Config:** `certora/conf/libs/PositionStatus.conf` + +### `libs/Premium.spec` +**Premium calculation verification.** + +- **Config:** `certora/conf/libs/Premium.conf` +- **Imports:** `HubBase.spec`, `common.spec` +- **Purpose:** Verifies that `Premium.calculatePremiumRay` matches its CVL summarization +- **Key Rules:** + - `calculatePremiumRay_equivalence` - Solidity matches CVL implementation + +--- + +## Symbolic Representations + +### `symbolicRepresentation/Math_CVL.spec` +**CVL implementations of math functions.** + +- **Purpose:** Provides CVL equivalents of Solidity math functions for use in summaries +- **Functions:** `mulDivDownCVL`, `mulDivUpCVL`, `mulDivRayDownCVL`, `mulDivRayUpCVL`, `divRayUpCVL`, `mulRayCVL` + +### `symbolicRepresentation/ERC20s_CVL.spec` +**ERC20 symbolic representations.** + +- **Purpose:** Symbolic handling of ERC20 token interactions + +### `symbolicRepresentation/SymbolicHub.spec` +**Symbolic Hub for Spoke verification.** + +- **Purpose:** Allows verifying Spoke independently of Hub implementation + +### `symbolicRepresentation/SymbolicPositionStatus.spec` +**Symbolic position status handling.** + +--- + +## Common Specifications + +### `common.spec` +**Shared method summaries.** + +- **Purpose:** Common summaries used in both Hub and Spoke specifications +- **Key Summaries:** + - `mulDivDown`, `mulDivUp` → CVL implementations + - `rayMulDown`, `rayMulUp`, `rayDivDown` → CVL implementations + - `wadDivUp`, `wadDivDown` → CVL implementations + - `percentMulDown`, `percentMulUp` → CVL implementations +- **Ghost Variables:** + - `RAY` = 10^27 + - `WAD` = 10^18 + - `PERCENTAGE_FACTOR` = 10000 + +--- + +## Dependency Graph + +``` +common.spec + ├── HubBase.spec + │ ├── Hub.spec + │ ├── HubValidState.spec + │ │ ├── HubIntegrityRules.spec + │ │ └── SpokeHubIntegrity.spec + │ ├── HubAccrueIntegrity.spec + │ ├── HubAccrueSupplyRate.spec + │ ├── HubAccrueUnrealizedFee.spec + │ └── HubAdditivity.spec (via SharesMath.spec) + │ + └── SpokeBase.spec + ├── Spoke.spec + ├── SpokeHealthCheck.spec + ├── SpokeUserIntegrity.spec + └── SpokeHubIntegrity.spec + +symbolicRepresentation/ + ├── Math_CVL.spec (used by most specs) + ├── ERC20s_CVL.spec (used by most specs) + ├── SymbolicHub.spec (used by SpokeHealthCheck) + └── SymbolicPositionStatus.spec (used by SpokeBase, SpokeHubIntegrity) +``` + +--- + +## Harness Contracts + +### `HubHarness.sol` +Exposes internal Hub functions for verification: +- `accrueInterest()` - Exposes `AssetLogic.accrue()` + +### `MathWrapper.sol` +Wraps math library functions for direct verification: +- Exposes `WadRayMath` functions: `rayMulDown`, `rayMulUp`, `rayDivDown`, `rayDivUp`, `wadDivDown`, `wadDivUp` +- Exposes `MathUtils` functions: `mulDivDown`, `mulDivUp` +- Exposes `PercentageMath` functions: `percentMulDown`, `percentMulUp` + +### `LibBitHarness.sol` +Wraps LibBit library for verification. + +### `PremiumWrapper.sol` +Wraps Premium library for verification: +- Exposes `Premium.calculatePremiumRay()` for CVL equivalence testing + +--- + +## Tips for Running Verification + +1. **Use Build Cache:** Most conf files have `"build_cache": true` to speed up repeated runs. + +2. **Split Long-Running Rules:** Use `--split_rules` for rules that may timeout: + ```bash + certoraRun certora/conf/Spoke.conf --split_rules drawnSharesZero noCollateralNoDebt + ``` + +3. **Run Specific Rules:** Use `--rule` to run individual rules: + ```bash + certoraRun certora/conf/Hub.conf --rule totalAssetsCompareToSuppliedAmount --msg "Hub totalAssets" + ``` + +5. **View Results:** Check the Certora Prover dashboard at https://prover.certora.com + diff --git a/certora/compileAll.sh b/certora/compileAll.sh new file mode 100755 index 000000000..eb87b8031 --- /dev/null +++ b/certora/compileAll.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +for FILE in certora/conf/*.conf +do + echo ${FILE} + certoraRun ${FILE} --compilation_steps_only +done diff --git a/certora/conf/Hub.conf b/certora/conf/Hub.conf new file mode 100644 index 000000000..e0f0db544 --- /dev/null +++ b/certora/conf/Hub.conf @@ -0,0 +1,17 @@ +{ + "files": [ + "src/hub/Hub.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 + //"split_rules": ["noChangeToOtherSpoke","supplyExchangeRateIsMonotonic"], + "independent_satisfy" : true + } \ No newline at end of file diff --git a/certora/conf/HubAccrueIntegrity.conf b/certora/conf/HubAccrueIntegrity.conf new file mode 100644 index 000000000..4ff28860a --- /dev/null +++ b/certora/conf/HubAccrueIntegrity.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "certora/harness/HubHarness.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, + "build_cache": true + } \ No newline at end of file diff --git a/certora/conf/HubAccrueSupplyRate.conf b/certora/conf/HubAccrueSupplyRate.conf new file mode 100644 index 000000000..211e9ef41 --- /dev/null +++ b/certora/conf/HubAccrueSupplyRate.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "certora/harness/HubHarness.sol" + ], + "loop_iter": 3, + "msg": "HubAccrue supply rate", + "multi_assert_check": true, + "optimistic_loop": true, + "parametric_contracts": [ + "HubHarness" + ], + "prover_args": [ + " -destructiveOptimizations twostage -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}]" + ], + "smt_timeout": 7200, + "solc_via_ir": true, + "verify": "HubHarness:certora/spec/HubAccrueSupplyRate.spec", + "build_cache": true +} \ No newline at end of file diff --git a/certora/conf/HubAccrueUnrealizedFee.conf b/certora/conf/HubAccrueUnrealizedFee.conf new file mode 100644 index 000000000..7af3864ca --- /dev/null +++ b/certora/conf/HubAccrueUnrealizedFee.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "certora/harness/HubHarness.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, + "build_cache": true + } \ No newline at end of file diff --git a/certora/conf/HubAdditivity.conf b/certora/conf/HubAdditivity.conf new file mode 100644 index 000000000..4c521877a --- /dev/null +++ b/certora/conf/HubAdditivity.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harness/HubHarness.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, + "build_cache": true + //"split_rule": ["drawAdditivity","restoreAdditivity","reportDeficitAdditivity"] + } \ No newline at end of file diff --git a/certora/conf/HubIntegrity.conf b/certora/conf/HubIntegrity.conf new file mode 100644 index 000000000..2fd7a74b4 --- /dev/null +++ b/certora/conf/HubIntegrity.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "src/hub/Hub.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, + "build_cache": true + } \ No newline at end of file diff --git a/certora/conf/HubValidState.conf b/certora/conf/HubValidState.conf new file mode 100644 index 000000000..731fd0e03 --- /dev/null +++ b/certora/conf/HubValidState.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "src/hub/Hub.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, + "exclude_rule": ["totalAssetsVsShares"], + "smt_timeout": "7200", + } \ No newline at end of file diff --git a/certora/conf/HubValidState_totalAssets.conf b/certora/conf/HubValidState_totalAssets.conf new file mode 100644 index 000000000..9becf463f --- /dev/null +++ b/certora/conf/HubValidState_totalAssets.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "src/hub/Hub.sol" + ], + "verify": "Hub:certora/spec/HubValidState.spec", + "optimistic_loop": true, + "loop_iter": "3", + "rule_sanity" : "none", + "msg": "AAVE V4 Hub - totalAssetsVsShares ", + "parametric_contracts" : "Hub", + "solc_via_ir" : true, + "build_cache" : true, + "smt_timeout": "7200", + "rule" : "totalAssetsVsShares", + "prover_args": [ + " -destructiveOptimizations twostage -splitParallel true -splitParallelInitialDepth 4 -splitParallelTimelimit 7200" + ], + } \ No newline at end of file diff --git a/certora/conf/Liquidation.conf b/certora/conf/Liquidation.conf new file mode 100644 index 000000000..10ec67452 --- /dev/null +++ b/certora/conf/Liquidation.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "src/spoke/instances/SpokeInstance.sol" + ], + "msg": "Liquidation", + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ + "SpokeInstance" + ], + "independent_satisfy" : true, + "verify": "SpokeInstance:certora/spec/liquidation.spec", + "build_cache" : true +} + diff --git a/certora/conf/Spoke.conf b/certora/conf/Spoke.conf new file mode 100644 index 000000000..dc3f8bb17 --- /dev/null +++ b/certora/conf/Spoke.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "src/spoke/instances/SpokeInstance.sol" + ], + "msg": "Spoke", + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ + "SpokeInstance" + ], + "independent_satisfy" : true, + "verify": "SpokeInstance:certora/spec/Spoke.spec", + // when running manually better to split the rules + //"split_rules" : ["drawnSharesZero","noCollateralNoDebt"], + "build_cache" : true +} diff --git a/certora/conf/SpokeHealthCheck.conf b/certora/conf/SpokeHealthCheck.conf new file mode 100644 index 000000000..d1d201faf --- /dev/null +++ b/certora/conf/SpokeHealthCheck.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "src/spoke/instances/SpokeInstance.sol" + ], + "msg": "SpokeHealthCheck", + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ + "SpokeInstance" + ], + "verify": "SpokeInstance:certora/spec/SpokeHealthCheck.spec", + "build_cache" : true +} + diff --git a/certora/conf/SpokeUserIntegrity.conf b/certora/conf/SpokeUserIntegrity.conf new file mode 100644 index 000000000..014dc2993 --- /dev/null +++ b/certora/conf/SpokeUserIntegrity.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "src/spoke/instances/SpokeInstance.sol", + ], + "msg": "SpokeUserIntegrity", + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ + "SpokeInstance" + ], + "verify": "SpokeInstance:certora/spec/SpokeUserIntegrity.spec", + "build_cache" : true +} \ No newline at end of file diff --git a/certora/conf/SpokeWithHub.conf b/certora/conf/SpokeWithHub.conf new file mode 100644 index 000000000..bfbebe29a --- /dev/null +++ b/certora/conf/SpokeWithHub.conf @@ -0,0 +1,30 @@ +{ + "files": [ + "src/hub/Hub.sol", + "src/spoke/instances/SpokeInstance.sol" + ], + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "1", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ "SpokeInstance", "Hub" ], + "verify": "SpokeInstance:certora/spec/SpokeHubIntegrity.spec", + "msg": "Spoke Hub Integrity", + "build_cache" : true, + "struct_link": [ + "SpokeInstance:hub=Hub", + ], + "independent_satisfy" : true, + // when running manually better to split the rules + //"split_rules" : ["user*"], + "prover_args": [ + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ], + +} \ No newline at end of file diff --git a/certora/conf/Spoke_noCollateralNoDebt.conf b/certora/conf/Spoke_noCollateralNoDebt.conf new file mode 100644 index 000000000..2b19e90e3 --- /dev/null +++ b/certora/conf/Spoke_noCollateralNoDebt.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "src/spoke/instances/SpokeInstance.sol" + ], + "msg": "Spoke noCollateralNoDebt", + "optimistic_hashing": true, + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "prettier=node_modules/prettier", + "prettier-plugin-solidity=node_modules/prettier-plugin-solidity" + ], + "parametric_contracts": [ + "SpokeInstance" + ], + "independent_satisfy" : true, + "verify": "SpokeInstance:certora/spec/Spoke.spec", + "rule": ["noCollateralNoDebt"], + "build_cache" : true, + "prover_args": [ + "-splitParallel", + "true", + "-dontStopAtFirstSplitTimeout", + "true" + ] +} + diff --git a/certora/conf/libs/LibBit.conf b/certora/conf/libs/LibBit.conf new file mode 100644 index 000000000..51f90c03a --- /dev/null +++ b/certora/conf/libs/LibBit.conf @@ -0,0 +1,14 @@ +{ + "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" + ], + "build_cache": true +} \ No newline at end of file diff --git a/certora/conf/libs/Math.conf b/certora/conf/libs/Math.conf new file mode 100644 index 000000000..18f6b1ffe --- /dev/null +++ b/certora/conf/libs/Math.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MathWrapper.sol" + ], + "verify": "MathWrapper:certora/spec/libs/Math.spec", + "rule_sanity" : "basic", + "msg": "Math function equivalence", + "build_cache": true + } \ No newline at end of file diff --git a/certora/conf/libs/PositionStatus.conf b/certora/conf/libs/PositionStatus.conf new file mode 100644 index 000000000..bc96b87a3 --- /dev/null +++ b/certora/conf/libs/PositionStatus.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "tests/mocks/PositionStatusMapWrapper.sol" + ], + "precise_bitwise_ops" : true, + "msg" : "PositionStatus library", + "verify": "PositionStatusMapWrapper:certora/spec/libs/PositionStatus.spec", + "smt_timeout": "7200", + "loop_iter": "3", + "optimistic_loop": true, + "build_cache": true +} diff --git a/certora/conf/libs/Premium.conf b/certora/conf/libs/Premium.conf new file mode 100644 index 000000000..b17954c7c --- /dev/null +++ b/certora/conf/libs/Premium.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "certora/harness/PremiumWrapper.sol" + ], + "verify": "PremiumWrapper:certora/spec/libs/Premium.spec", + "rule_sanity" : "basic", + "msg": "Premium calculatePremiumRay equivalence", + "build_cache": true +} + diff --git a/certora/conf/libs/SharesMath.conf b/certora/conf/libs/SharesMath.conf new file mode 100644 index 000000000..94a48e2f3 --- /dev/null +++ b/certora/conf/libs/SharesMath.conf @@ -0,0 +1,17 @@ +{ + "files": [ + "certora/harness/HubHarness.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, + "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}]" + ], + } \ No newline at end of file diff --git a/certora/conf/libs/VerifySymbolicPositionStatus.conf b/certora/conf/libs/VerifySymbolicPositionStatus.conf new file mode 100644 index 000000000..6986c0af9 --- /dev/null +++ b/certora/conf/libs/VerifySymbolicPositionStatus.conf @@ -0,0 +1,17 @@ +{ + "files": [ + "tests/mocks/PositionStatusMapWrapper.sol", + "src/spoke/instances/SpokeInstance.sol", + ], + "precise_bitwise_ops" : true, + "msg" : "PositionStatus check summary", + "verify": "PositionStatusMapWrapper:certora/spec/symbolicRepresentation/VerifySymbolicPositionStatus.spec", + "smt_timeout": "7200", + "loop_iter": "3", + "optimistic_loop": true, + "prover_args": [ + "-split", + "false" + ], + "build_cache": true +} diff --git a/certora/harness/HubHarness.sol b/certora/harness/HubHarness.sol new file mode 100644 index 000000000..86f50b06a --- /dev/null +++ b/certora/harness/HubHarness.sol @@ -0,0 +1,57 @@ +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(); + } + + 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 getUnrealizedFees(uint256 assetId) external view returns (uint256) { + Asset storage asset = _assets[assetId]; + + return asset.getUnrealizedFees(asset.getDrawnIndex()); + } +} diff --git a/certora/harness/LibBitHarness.sol b/certora/harness/LibBitHarness.sol new file mode 100644 index 000000000..b50368c21 --- /dev/null +++ b/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); + } + } +} diff --git a/certora/harness/MathWrapper.sol b/certora/harness/MathWrapper.sol new file mode 100644 index 000000000..275d333dc --- /dev/null +++ b/certora/harness/MathWrapper.sol @@ -0,0 +1,88 @@ +import {Math} from '../../src/dependencies/openzeppelin/Math.sol'; +import {WadRayMath} from '../../src/libraries/math/WadRayMath.sol'; +import {PercentageMath} from '../../src/libraries/math/PercentageMath.sol'; +import {MathUtils} from '../../src/libraries/math/MathUtils.sol'; + +pragma solidity ^0.8.0; + +contract MathWrapper { + function SECONDS_PER_YEAR() external pure returns (uint256) { + return 365 days; + } + + function mulDiv( + uint256 x, + uint256 y, + uint256 denominator + ) external pure returns (uint256 result) { + return Math.mulDiv(x, y, denominator); + } + + function mulDivDown( + uint256 x, + uint256 y, + uint256 denominator + ) external pure returns (uint256 result) { + return MathUtils.mulDivDown(x, y, denominator); + } + + function mulDivUp( + uint256 x, + uint256 y, + uint256 denominator + ) external pure returns (uint256 result) { + return MathUtils.mulDivUp(x, y, denominator); + } + + function RAY() public pure returns (uint256) { + return WadRayMath.RAY; + } + + function WAD() public pure returns (uint256) { + return WadRayMath.WAD; + } + + function rayMulDown(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.rayMulDown(a, b); + } + + function rayMulUp(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.rayMulUp(a, b); + } + + function rayDivDown(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.rayDivDown(a, b); + } + + function rayDivUp(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.rayDivUp(a, b); + } + + function wadDivDown(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.wadDivDown(a, b); + } + + function wadDivUp(uint256 a, uint256 b) public pure returns (uint256) { + return WadRayMath.wadDivUp(a, b); + } + + function percentMulDown(uint256 percentage, uint256 value) public pure returns (uint256) { + return PercentageMath.percentMulDown(percentage, value); + } + + function percentMulUp(uint256 percentage, uint256 value) public pure returns (uint256) { + return PercentageMath.percentMulUp(percentage, value); + } + + function PERCENTAGE_FACTOR() public pure returns (uint256) { + return PercentageMath.PERCENTAGE_FACTOR; + } + + function fromRayUp(uint256 a) public pure returns (uint256) { + return WadRayMath.fromRayUp(a); + } + + function toRay(uint256 a) public pure returns (uint256) { + return WadRayMath.toRay(a); + } +} diff --git a/certora/harness/PremiumWrapper.sol b/certora/harness/PremiumWrapper.sol new file mode 100644 index 000000000..5d3a8cbf0 --- /dev/null +++ b/certora/harness/PremiumWrapper.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.20; + +import {Premium} from '../../src/hub/libraries/Premium.sol'; + +contract PremiumWrapper { + function calculatePremiumRay( + uint256 premiumShares, + int256 premiumOffsetRay, + uint256 drawnIndex + ) external pure returns (uint256) { + return Premium.calculatePremiumRay(premiumShares, premiumOffsetRay, drawnIndex); + } +} + diff --git a/certora/runAll.sh b/certora/runAll.sh new file mode 100755 index 000000000..bcf7e47cd --- /dev/null +++ b/certora/runAll.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +for FILE in certora/conf/*.conf +do + echo ${FILE} + certoraRun ${FILE} +done \ No newline at end of file diff --git a/certora/spec/Hub.spec b/certora/spec/Hub.spec new file mode 100644 index 000000000..576d59cce --- /dev/null +++ b/certora/spec/Hub.spec @@ -0,0 +1,210 @@ + +/*** + +Verify Hub + +State changes rules in which the validate functions are ignored. +Assuming accrue has been called on the current block timestamp. + + +***/ + +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./symbolicRepresentation/Math_CVL.spec"; +import "./HubValidState.spec"; + +methods { + function _validateAdd( + IHub.Asset storage asset, + IHub.SpokeData storage spoke, + uint256 amount + ) internal => NONDET; + + function _validateRemove( + IHub.SpokeData storage spoke, + uint256 amount, + address to + ) internal => NONDET; + + function _validateDraw( + IHub.Asset storage asset, + IHub.SpokeData storage spoke, + uint256 amount, + address to + ) internal => NONDET; + + function _validateRestore( + IHub.Asset storage asset, + IHub.SpokeData storage spoke, + uint256 drawnAmount, + uint256 premiumAmountRay + ) internal => NONDET; + + function _validateReportDeficit( + IHub.Asset storage asset, + IHub.SpokeData storage spoke, + uint256 drawnAmount, + uint256 premiumAmountRay + ) internal => NONDET; + + function _validateEliminateDeficit( + IHub.SpokeData storage spoke, + uint256 amount + ) internal => NONDET; + + function _validatePayFeeShares( + IHub.SpokeData storage senderSpoke, + uint256 feeShares + ) internal => NONDET; + + function _validateTransferShares( + IHub.Asset storage asset, + IHub.SpokeData storage sender, + IHub.SpokeData storage receiver, + uint256 shares + ) internal => NONDET; + + function _validateSweep( + IHub.Asset storage asset, + address caller, + uint256 amount + ) internal => NONDET; + + function _validateReclaim( + IHub.Asset storage asset, + address caller, + uint256 amount + ) internal => NONDET; +} + + +/** @title supply rate is never decreasing +when not accruing interest, every function should never decrease supply exchange rate +*/ +rule supplyExchangeRateIsMonotonic(env e, method f, calldataarg args) +filtered { + f -> !f.isView +} +{ + uint256 assetId; + uint256 OneM = 1000000; + + requireAllInvariants(assetId, e); + // use ghost to avoid repeating complex computation + mathint assetsBefore = addedAssetsBefore; + mathint sharesBefore = supplyShareBefore; + + require hub._assets[assetId].lastUpdateTimestamp == e.block.timestamp; + + + f(e, args); + + mathint assetsAfter = getAddedAssets(e,assetId); + mathint sharesAfter = getAddedShares(e,assetId); + require assetsAfter >= sharesAfter, "based on rule totalAssetsVsShares(assetId,e) and to help the prover"; + assert (assetsAfter + OneM) * (sharesBefore + OneM) >= (assetsBefore + OneM )* (sharesAfter + OneM); +} + + + +/** @title No change to a spoke's asset or debt. assume accrue has been called. +**/ +rule noChangeToOtherSpoke(address spoke, uint256 assetId, address otherSpoke, method f) + filtered { f -> !f.isView } + { + env e; + env eOther; + require e.block.timestamp == eOther.block.timestamp; + require otherSpoke != spoke && eOther.msg.sender == otherSpoke; + address feeReceiver = hub._assets[assetId].feeReceiver; + + require hub._assets[assetId].lastUpdateTimestamp == e.block.timestamp; + requireAllInvariants(assetId, e); + + uint256 cumulativeDebt_ = getSpokeTotalOwed(e, assetId, spoke); + + uint256 shares_ = getSpokeAddedShares(e, assetId, spoke); + uint256 assets = getSpokeAddedAssets(e, assetId, spoke); + + address toOnTransfer; + uint256 x; + if (f.selector == sig:transferShares(uint256,uint256,address).selector) { + transferShares(eOther, assetId, x, toOnTransfer); + } + + else { + calldataarg args; + f(eOther,args); + } + assert cumulativeDebt_ >= getSpokeTotalOwed(e, assetId, spoke); + assert (spoke != feeReceiver && spoke != toOnTransfer) => shares_ == getSpokeAddedShares(e, assetId, spoke); + // cases where shares can increase + assert (spoke == feeReceiver || spoke == toOnTransfer) => shares_ <= getSpokeAddedShares(e, assetId, spoke); + // asset can increase due to other's operations + assert assets <= getSpokeAddedAssets(e, assetId, spoke); +} + + +/** +@title Accrue must be called before updating shares or debt. +Transferring shares is safe without accrue, as it stays the same behavior +Also adding an asset is safe without accrue, as there is nothing to update. +*/ +rule accrueWasCalled(uint256 assetId, method f) filtered { f-> !f.isView && + f.selector != sig:addAsset(address,uint8,address,address,bytes).selector && + f.selector != sig:transferShares(uint256,uint256,address).selector} +{ + require !unsafeAccessBeforeAccrue; + + env e; + calldataarg args; + f(e,args); + + assert !unsafeAccessBeforeAccrue; + +} + +/** +@title lastUpdateTimestamp is never in the future +*/ +rule lastUpdateTimestamp_notInFuture(uint256 assetId, method f) filtered { f-> !f.isView} { + env e; + require hub._assets[assetId].lastUpdateTimestamp <= e.block.timestamp; + + calldataarg args; + f(e,args); + + assert hub._assets[assetId].lastUpdateTimestamp <= e.block.timestamp; + + +} + +/** +@title total assets is equal to the supplied amount when taking into account the virtual assets and shares +**/ +rule totalAssetsCompareToSuppliedAmount_virtual(uint256 assetId, env e){ + requireAllInvariants(assetId, e); + uint256 oneM = 1000000; + + mathint addedAssets = getAddedAssets(e,assetId) + oneM; + mathint addedShares = getAddedShares(e,assetId) + oneM; + + // rounding down + assert addedAssets == previewRemoveByShares(e, assetId, require_uint256(addedShares)); + // rounding up + assert addedAssets == previewAddByShares(e, assetId, require_uint256(addedShares)); +} + +/** +@title total assets is equal to or greater than the supplied amount without taking into account the virtual assets and shares +**/ +rule totalAssetsCompareToSuppliedAmount_noVirtual(uint256 assetId, env e){ + requireAllInvariants(assetId, e); + mathint addedAssets = getAddedAssets(e,assetId); + mathint addedShares = getAddedShares(e,assetId); + + assert addedAssets >= previewRemoveByShares(e, assetId, require_uint256(addedShares)); + satisfy addedAssets > previewRemoveByShares(e, assetId, require_uint256(addedShares)); + assert addedAssets >= previewAddByShares(e, assetId, require_uint256(addedShares)); + satisfy addedAssets > previewAddByShares(e, assetId, require_uint256(addedShares)); +} \ No newline at end of file diff --git a/certora/spec/HubAccrueIntegrity.spec b/certora/spec/HubAccrueIntegrity.spec new file mode 100644 index 000000000..5426590ec --- /dev/null +++ b/certora/spec/HubAccrueIntegrity.spec @@ -0,0 +1,288 @@ + +/** +@title Prove unit test properties of AssetLogic.accrue() function +This is proven on HubHarness which expose accure() as an external function + +**/ + +import "./HubBase.spec"; + +using HubHarness as hub; +using MathWrapper as mathWrapper; + +methods { + // envfree functions + function mathWrapper.SECONDS_PER_YEAR() external returns (uint256) envfree; +} + +/** +@title Two invocations of accure() at the same block result in a state exactly the same as the first execution +**/ +rule runningTwiceIsEquivalentToOne() { + env e; + uint256 assetId; + accrueInterest(e,assetId); + storage afterOne = lastStorage; + accrueInterest(e,assetId); + assert lastStorage == afterOne; +} + +/** +@title Once baseDebtIndex is set it is at least Ray +Proved also in invariant baseDebtIndexMin on all Hub functions +**/ +rule baseDebtIndexMin_accrue(){ + env e; + uint256 assetId; + require hub._assets[assetId].drawnIndex == 0 || hub._assets[assetId].drawnIndex >= RAY; + + accrueInterest(e,assetId); + assert hub._assets[assetId].drawnIndex == 0 || hub._assets[assetId].drawnIndex >= RAY; + +} + +/** +@title lastUpdateTimestamp is not in the future +**/ +rule lastUpdateTimestamp_notInFuture(){ + env e; + uint256 assetId; + require hub._assets[assetId].lastUpdateTimestamp <= e.block.timestamp; + accrueInterest(e,assetId); + assert hub._assets[assetId].lastUpdateTimestamp == e.block.timestamp; +} + + +definition emptyAsset(uint256 assetId) returns bool = + hub._assets[assetId].addedShares == 0 && + hub._assets[assetId].liquidity == 0 && + hub._assets[assetId].addedShares == 0 && + hub._assets[assetId].deficitRay == 0 && + hub._assets[assetId].swept == 0 && + hub._assets[assetId].premiumShares == 0 && + hub._assets[assetId].premiumOffsetRay == 0 && + hub._assets[assetId].drawnShares == 0 && + hub._assets[assetId].drawnIndex == 0 && + hub._assets[assetId].drawnRate == 0 && + hub._assets[assetId].lastUpdateTimestamp == 0 && + ( forall address spoke. + hub._spokes[assetId][spoke].addedShares == 0 && + hub._spokes[assetId][spoke].drawnShares == 0 && + hub._spokes[assetId][spoke].premiumShares == 0 && + hub._spokes[assetId][spoke].premiumOffsetRay == 0 + ) && + hub._assets[assetId].underlying == 0; + + +/** +@title BaseDebtIndex is increasing on block change when baseRate is at least SECONDS_PER_YEAR and index is set +Fails on cases in which baseBorrowRate <= SECONDS_PER_YEAR +**/ +rule baseDebtIndex_increasing(uint256 assetId) { + //Proved in invariant baseDebtIndexMin and baseDebtIndexMin_accrue + require hub._assets[assetId].drawnIndex >= RAY; + + uint256 before = hub._assets[assetId].drawnIndex; + + env e; + require e.block.timestamp > hub._assets[assetId].lastUpdateTimestamp && e.block.timestamp <= max_uint40; + uint256 baseDebt = getAssetTotalOwed(e, assetId); + + accrueInterest(e,assetId); + + assert hub._assets[assetId].drawnIndex >= before; + // if there is debt then the drawnIndex should not increase + assert (hub._assets[assetId].drawnRate >= mathWrapper.SECONDS_PER_YEAR() + && baseDebt > -hub._assets[assetId].premiumOffsetRay) => + hub._assets[assetId].drawnIndex > before; + satisfy hub._assets[assetId].drawnRate == mathWrapper.SECONDS_PER_YEAR(); +} + +/** +@title Prove premiumOffset is always less than or equal to premiumShares * drawnIndex / RAY rounded up. +This is important to avoid revert on accrue +**/ +rule premiumOffset_Integrity_accrue(uint256 assetId, address spokeId) { + + env e; + require hub._assets[assetId].lastUpdateTimestamp <= e.block.timestamp; + + //requireInvariant baseDebtIndexMin(assetId); + require hub._assets[assetId].drawnIndex == 0 || hub._assets[assetId].drawnIndex >= RAY; + + require previewRestoreByShares(e,assetId,hub._assets[assetId].premiumShares) >= hub._assets[assetId].premiumOffsetRay && + previewRestoreByShares(e,assetId,hub._spokes[assetId][spokeId].premiumShares) >= hub._spokes[assetId][spokeId].premiumOffsetRay; + + accrueInterest(e, assetId); + + assert previewRestoreByShares(e,assetId,hub._assets[assetId].premiumShares) >= hub._assets[assetId].premiumOffsetRay && + previewRestoreByShares(e,assetId,hub._spokes[assetId][spokeId].premiumShares) >= hub._spokes[assetId][spokeId].premiumOffsetRay; + +} + +/** +@title View functions are isomorphic to accrue, they return the same value if accrue was called or not +**/ + +rule viewFunctionsIntegrity(uint256 assetId, method f) filtered { f-> f.isView && + + f.selector != sig:authority().selector && + f.selector != sig:isConsumingScheduledOp().selector && + f.selector != sig:isSpokeListed(uint256,address).selector && + // returns a struct + f.selector != sig:getAsset(uint256).selector && + f.selector != sig:getAssetConfig(uint256).selector && + f.selector != sig:getSpoke(uint256,address).selector && + f.selector != sig:getSpokeConfig(uint256,address).selector && + f.selector != sig:getSpokeAddress(uint256,uint256).selector && + // harness functions + f.selector != sig:toSharesDown(uint256,uint256,uint256).selector && + f.selector != sig:toAssetsDown(uint256,uint256,uint256).selector && + f.selector != sig:toSharesUp(uint256,uint256,uint256).selector && + f.selector != sig:toAssetsUp(uint256,uint256,uint256).selector && + f.selector != sig:getUnrealizedFees(uint256).selector && + f.selector != sig:MAX_ALLOWED_UNDERLYING_DECIMALS().selector && + f.selector != sig:MAX_ALLOWED_SPOKE_CAP().selector && + f.selector != sig:MAX_RISK_PREMIUM_THRESHOLD().selector && + f.selector != sig:getAssetUnderlyingAndDecimals(uint256).selector + } +{ + env e; + calldataarg args; + storage init = lastStorage; + + + // lastUpdateTimestamp can not be in the future, prove... + require hub._assets[assetId].lastUpdateTimestamp <= e.block.timestamp; + + //requireInvariant baseDebtIndexMin(assetId); + require hub._assets[assetId].drawnIndex == 0 || hub._assets[assetId].drawnIndex >= RAY; + + + accrueInterest(e, assetId); + mathint ret_withAccrue = callViewFunction(f, e, args); + + // get back to init + getAsset(e, assetId) at init; + mathint ret_withoutAccrue = callViewFunction(f, e, args); + + assert ret_withAccrue == ret_withoutAccrue; +} + +//* helper function for calling view functions and fetching the return value as mathint */ +function callViewFunction(method f, env e, calldataarg args) returns mathint { + if (f.selector == sig:getAssetCount().selector) { + return getAssetCount(e, args); + } + else if (f.selector == sig:getSpokeCount(uint256).selector) { + return getSpokeCount(e, args); + } + else if (f.selector == sig:getSpoke(uint256,address).selector) { + // skip or handle as needed (returns struct) + } + else if (f.selector == sig:previewAddByAssets(uint256,uint256).selector) { + return previewAddByAssets(e, args); + } + else if (f.selector == sig:previewAddByShares(uint256,uint256).selector) { + return previewAddByShares(e, args); + } + else if (f.selector == sig:previewRemoveByAssets(uint256,uint256).selector) { + return previewRemoveByAssets(e, args); + } + else if (f.selector == sig:previewRemoveByShares(uint256,uint256).selector) { + return previewRemoveByShares(e, args); + } + else if (f.selector == sig:previewDrawByAssets(uint256,uint256).selector) { + return previewDrawByAssets(e, args); + } + else if (f.selector == sig:previewDrawByShares(uint256,uint256).selector) { + return previewDrawByShares(e, args); + } + else if (f.selector == sig:previewRestoreByAssets(uint256,uint256).selector) { + return previewRestoreByAssets(e, args); + } + else if (f.selector == sig:previewRestoreByShares(uint256,uint256).selector) { + return previewRestoreByShares(e, args); + } + else if (f.selector == sig:getAssetDrawnIndex(uint256).selector) { + return getAssetDrawnIndex(e, args); + } + else if (f.selector == sig:getAssetOwed(uint256).selector) { + uint256 a; uint256 b; (a, b) = getAssetOwed(e, args); return a + b; + } + else if (f.selector == sig:getAssetTotalOwed(uint256).selector) { + return getAssetTotalOwed(e, args); + } + else if (f.selector == sig:getSpokeOwed(uint256,address).selector) { + uint256 a; uint256 b; (a, b) = getSpokeOwed(e, args); return a + b; + } + else if (f.selector == sig:getSpokeTotalOwed(uint256,address).selector) { + return getSpokeTotalOwed(e, args); + } + else if (f.selector == sig:getAssetDrawnRate(uint256).selector) { + return getAssetDrawnRate(e, args); + } + else if (f.selector == sig:getAddedAssets(uint256).selector) { + return getAddedAssets(e, args); + } + else if (f.selector == sig:getAddedShares(uint256).selector) { + return getAddedShares(e, args); + } + else if (f.selector == sig:getSpokeAddedAssets(uint256,address).selector) { + return getSpokeAddedAssets(e, args); + } + else if (f.selector == sig:getSpokeAddedShares(uint256,address).selector) { + return getSpokeAddedShares(e, args); + } + else if (f.selector == sig:getAssetDrawnShares(uint256).selector) { + return getAssetDrawnShares(e, args); + } + else if (f.selector == sig:getAssetPremiumData(uint256).selector) { + uint256 a; int256 b; + (a, b) = getAssetPremiumData(e, args); + return a + to_mathint(b); + } + else if (f.selector == sig:getSpokePremiumData(uint256,address).selector) { + uint256 a; int256 b; + (a, b) = getSpokePremiumData(e, args); + return a + to_mathint(b); + } + else if (f.selector == sig:getAssetPremiumRay(uint256).selector) { + return getAssetPremiumRay(e, args); + } + else if (f.selector == sig:getSpokePremiumRay(uint256,address).selector) { + return getSpokePremiumRay(e, args); + } + else if (f.selector == sig:getSpokeDrawnShares(uint256,address).selector) { + return getSpokeDrawnShares(e, args); + } + else if (f.selector == sig:MIN_ALLOWED_UNDERLYING_DECIMALS().selector) { + return MIN_ALLOWED_UNDERLYING_DECIMALS(e, args); + } + else if (f.selector == sig:getAssetDeficitRay(uint256).selector) { + return getAssetDeficitRay(e, args); + } + else if (f.selector == sig:getAssetLiquidity(uint256).selector) { + return getAssetLiquidity(e, args); + } + else if (f.selector == sig:getAssetSwept(uint256).selector) { + return getAssetSwept(e, args); + } + else if (f.selector == sig:getSpokeDeficitRay(uint256,address).selector) { + return getSpokeDeficitRay(e, args); + } + else if (f.selector == sig:getAssetAccruedFees(uint256).selector) { + return getAssetAccruedFees(e, args); + } + else if (f.selector == sig:isUnderlyingListed(address).selector) { + return isUnderlyingListed(e, args) ? 1 : 0; + } + else + { + assert false, "unknown view function"; + return 0; + } + return 0; + + +} diff --git a/certora/spec/HubAccrueSupplyRate.spec b/certora/spec/HubAccrueSupplyRate.spec new file mode 100644 index 000000000..5b46d50ee --- /dev/null +++ b/certora/spec/HubAccrueSupplyRate.spec @@ -0,0 +1,208 @@ + +/** +@title Prove that accrue can not decrease the share rate + +assets / shares is increasing + + +**/ + +import "./HubBase.spec"; + +using HubHarness as hub; + +methods { + + function AssetLogic.getDrawnIndex(IHub.Asset storage asset) internal returns (uint256) with (env e) => symbolicDrawnIndex(e.block.timestamp); + + +} + + +// symbolic representation of drawnIndex that is a function of the block timestamp. +ghost symbolicDrawnIndex(uint256) returns uint256; + +/* +@title Prove that accrue can not decrease the share rate + +Given e1, a timestamp last accrue, we prove that the share rate is the same or increasing at e2 +We prove this for the maximum value of getUnrealizedFees, as proved in HubAccrueIntegrityUnrealizedFee.spec +Therefore, it holds for any smaller value of getUnrealizedFees, as shares_e2 will be smaller +**/ + + +rule accrueSupplyRate(uint256 assetId){ + env e1; env e2; + uint256 oneM = 1000000; + require e1.block.timestamp < e2.block.timestamp; + + + // e1 is the last accrued timestamp + require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e1.block.timestamp; + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + + //correlate the drawn index with the symbolic one, assume increasing and min value as proved in + // HubAccrueIntegrityDrawnIndex.spec + require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e1.block.timestamp); + //based on rule drawnIndex_increasing(assetId); + require symbolicDrawnIndex(e1.block.timestamp) <= symbolicDrawnIndex(e2.block.timestamp); + //based on requireInvariant baseDebtIndexMin(assetId); + require symbolicDrawnIndex(e1.block.timestamp) >= RAY; + + + mathint assets_e1 = getAddedAssets(e1, assetId); + mathint shares_e1 = hub._assets[assetId].addedShares; + //requireInvariant totalAssetsVsShares(assetId,e); + require assets_e1 >= shares_e1 ; + + //accrue interest + accrueInterest(e2, assetId); + mathint assets_e2 = getAddedAssets(e2, assetId); + mathint shares_e2 = hub._assets[assetId].addedShares; + + assert (assets_e2 + oneM) * (shares_e1 + oneM) >= (assets_e1 + oneM) * (shares_e2 + oneM); + satisfy (assets_e2 + oneM) * (shares_e1 + oneM) > (assets_e1 + oneM) * (shares_e2 + oneM); + +} + +function setup_three_timestamps(uint256 assetId, env e1, env e2, env e3){ + require e1.block.timestamp < e2.block.timestamp && e2.block.timestamp < e3.block.timestamp; + + require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e1.block.timestamp; + //correlate the drawn index with the symbolic one, assume increasing and min value as proved in + // HubAccrueIntegrityDrawnIndex.spec + require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e1.block.timestamp); + //based on rule drawnIndex_increasing(assetId); + require symbolicDrawnIndex(e1.block.timestamp) <= symbolicDrawnIndex(e2.block.timestamp); + require symbolicDrawnIndex(e2.block.timestamp) <= symbolicDrawnIndex(e3.block.timestamp); + //based on requireInvariant baseDebtIndexMin(assetId); + require symbolicDrawnIndex(e1.block.timestamp) >= RAY; +} + + +rule shareRate_withoutAccrue_time_monotonic(uint256 assetId){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint assets_e1 = getAddedAssets(e1, assetId); + mathint shares = hub._assets[assetId].addedShares; + //requireInvariant totalAssetsVsShares(assetId,e); + require assets_e1 >= shares; + + // get the fee shares and asset at e2 + mathint assets_e2 = getAddedAssets(e2, assetId); + assert shares == hub._assets[assetId].addedShares; + + // get the fee shares and asset at e2; + mathint assets_e3 = getAddedAssets(e3, assetId); + + assert assets_e3 >= assets_e2 ; +} + + +rule previewRemoveByShares_withoutAccrue_time_monotonic(uint256 assetId, uint256 shares){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint assets_e1 = previewRemoveByShares(e1, assetId, shares); + mathint assets_e2 = previewRemoveByShares(e2, assetId, shares); + mathint assets_e3 = previewRemoveByShares(e3, assetId, shares); + + assert assets_e3 >= assets_e2 && assets_e2 >= assets_e1 ; +} + + +rule previewAddByAssets_withoutAccrue_time_monotonic(uint256 assetId, uint256 assets){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint shares_e1 = previewAddByAssets(e1, assetId, assets); + mathint shares_e2 = previewAddByAssets(e2, assetId, assets); + mathint shares_e3 = previewAddByAssets(e3, assetId, assets); + + assert shares_e3 <= shares_e2 && shares_e2 <= shares_e1 ; +} + + +rule previewAddByShares_withoutAccrue_time_monotonic(uint256 assetId, uint256 shares){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint assets_e1 = previewAddByShares(e1, assetId, shares); + mathint assets_e2 = previewAddByShares(e2, assetId, shares); + mathint assets_e3 = previewAddByShares(e3, assetId, shares); + + assert assets_e3 >= assets_e2 && assets_e2 >= assets_e1 ; +} + + +rule previewRemoveByAssets_withoutAccrue_time_monotonic(uint256 assetId, uint256 assets){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint shares_e1 = previewRemoveByAssets(e1, assetId, assets); + mathint shares_e2 = previewRemoveByAssets(e2, assetId, assets); + mathint shares_e3 = previewRemoveByAssets(e3, assetId, assets); + + assert shares_e3 <= shares_e2 && shares_e2 <= shares_e1 ; +} + + + +rule previewDrawByAssets_withoutAccrue_time_monotonic(uint256 assetId, uint256 assets){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint shares_e1 = previewDrawByAssets(e1, assetId, assets); + mathint shares_e2 = previewDrawByAssets(e2, assetId, assets); + mathint shares_e3 = previewDrawByAssets(e3, assetId, assets); + + assert shares_e3 <= shares_e2 && shares_e2 <= shares_e1 ; +} + + +rule previewDrawByShares_withoutAccrue_time_monotonic(uint256 assetId, uint256 shares){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint assets_e1 = previewDrawByShares(e1, assetId, shares); + mathint assets_e2 = previewDrawByShares(e2, assetId, shares); + mathint assets_e3 = previewDrawByShares(e3, assetId, shares); + + assert assets_e3 >= assets_e2 && assets_e2 >= assets_e1 ; +} + + + +rule previewRestoreByAssets_withoutAccrue_time_monotonic(uint256 assetId, uint256 assets){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint shares_e1 = previewRestoreByAssets(e1, assetId, assets); + mathint shares_e2 = previewRestoreByAssets(e2, assetId, assets); + mathint shares_e3 = previewRestoreByAssets(e3, assetId, assets); + + assert shares_e3 <= shares_e2 && shares_e2 <= shares_e1 ; +} + + +rule previewRestoreByShares_withoutAccrue_time_monotonic(uint256 assetId, uint256 shares){ + env e1; env e2; env e3; + setup_three_timestamps(assetId, e1, e2, e3); + require hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR, "invariant liquidityFee_upper_bound"; + + mathint assets_e1 = previewRestoreByShares(e1, assetId, shares); + mathint assets_e2 = previewRestoreByShares(e2, assetId, shares); + mathint assets_e3 = previewRestoreByShares(e3, assetId, shares); + + assert assets_e3 >= assets_e2 && assets_e2 >= assets_e1 ; +} \ No newline at end of file diff --git a/certora/spec/HubAccrueUnrealizedFee.spec b/certora/spec/HubAccrueUnrealizedFee.spec new file mode 100644 index 000000000..33403f983 --- /dev/null +++ b/certora/spec/HubAccrueUnrealizedFee.spec @@ -0,0 +1,71 @@ + +/** +@title Prove unit test properties of getUnrealizedFees: +**/ + +import "./HubBase.spec"; + +using HubHarness as hub; + +methods { + function AssetLogic.getDrawnIndex(IHub.Asset storage asset) internal returns (uint256) with (env e) => symbolicDrawnIndex(e.block.timestamp); + +} + +// symbolic representation of drawnIndex that is a function of the block timestamp. +ghost symbolicDrawnIndex(uint256) returns uint256; + +/** +@title feeAmount increase in accrue is equal to the unrealized fee at this timestamp +**/ +rule feeAmountIncrease(uint256 assetId){ + env e1; env e2; + + require e1.block.timestamp < e2.block.timestamp; + + //assume accrue was called at e1.block.timestamp + require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e1.block.timestamp; + require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e1.block.timestamp); + require symbolicDrawnIndex(e1.block.timestamp) <= symbolicDrawnIndex(e2.block.timestamp); + require symbolicDrawnIndex(e1.block.timestamp) >= RAY; + uint256 feeAssetsBefore = hub._assets[assetId].realizedFees; + uint256 feeAssets = getUnrealizedFees(e2,assetId); + accrueInterest(e2,assetId); + assert hub._assets[assetId].realizedFees == feeAssetsBefore + feeAssets; +} + +/** +@title Prove that the maximum value of getUnrealizedFees is at 100% liquidityFee +**/ +rule maxgetUnrealizedFees(uint256 assetId){ + env e1; env e2; + require e1.block.timestamp < e2.block.timestamp; + require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e1.block.timestamp; + + require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e1.block.timestamp); + require symbolicDrawnIndex(e1.block.timestamp) <= symbolicDrawnIndex(e2.block.timestamp); + require symbolicDrawnIndex(e1.block.timestamp) >= RAY; + assert getUnrealizedFees(e1,assetId) == 0 ; + + storage init_state = lastStorage; + require hub._assets[assetId].liquidityFee == PERCENTAGE_FACTOR; + uint256 feesAtMax = getUnrealizedFees(e2,assetId); + + //assume any value that can be set in updateAssetConfig + // must be called at e1 as accrue is happening in updateAssetConfig + IHub.AssetConfig config; + bytes irData; + updateAssetConfig(e1,assetId,config,irData) at init_state; + assert getUnrealizedFees(e2,assetId) <= feesAtMax; + +} + +/** +@title Prove that when the lastUpdateTimestamp is the same as the block timestamp, the unrealized fees are 0 +**/ +rule lastUpdateTimestampSameAsBlockTimestamp(uint256 assetId){ + env e; + require hub._assets[assetId].lastUpdateTimestamp!=0 && hub._assets[assetId].lastUpdateTimestamp == e.block.timestamp; + require hub._assets[assetId].drawnIndex == symbolicDrawnIndex(e.block.timestamp); + assert getUnrealizedFees(e,assetId) == 0; +} \ No newline at end of file diff --git a/certora/spec/HubAdditivity.spec b/certora/spec/HubAdditivity.spec new file mode 100644 index 000000000..945085a11 --- /dev/null +++ b/certora/spec/HubAdditivity.spec @@ -0,0 +1,236 @@ + +/** +Verify the additivity of the operation: add, remove, draw, restore, reportDeficit, eliminateDeficit. +For each operation, we verify that splitting an operation to two operations is less beneficial to the user than doing it in one step. + +This spec uses summarization to the shareMath library. The summarization follow the proof in ShareMath.spec. The rules of SharesMath.spec are verified on the CVL representation. + +To run this spec file: + certoraRun certora/conf/HubAdditivity.conf + +**/ + +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./symbolicRepresentation/Math_CVL.spec"; +import "./libs/SharesMath.spec"; +import "./common.spec"; + +methods { + function SharesMath.toSharesDown(uint256 assets, uint256 totalAssets, uint256 totalShares) internal returns (uint256) => + symbolic_toSharesDown(assets, totalAssets, totalShares) ; + function SharesMath.toAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) internal returns (uint256) => + symbolic_toAssetsDown(shares, totalAssets, totalShares) ; + function SharesMath.toSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) internal returns (uint256) => + symbolic_toSharesUp(assets, totalAssets, totalShares) ; + function SharesMath.toAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) internal returns (uint256) => + symbolic_toAssetsUp(shares, totalAssets, totalShares) ; + +} +ghost symbolic_toSharesDown(mathint /*assets*/, mathint /*totalAssets*/, mathint /*totalShares*/) returns uint256 { + // monotonicity + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + x > y => symbolic_toSharesDown(x, ta, ts) >= symbolic_toSharesDown(y, ta, ts); + // additivity with respect to side effect + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + symbolic_toSharesDown(x, ta, ts) + symbolic_toSharesDown(y, ta + x, ts + symbolic_toSharesDown(x, ta, ts)) <= symbolic_toSharesDown(x + y, ta, ts); +} + +ghost symbolic_toAssetsDown(mathint /*shares*/, mathint /*totalAssets*/, mathint /*totalShares*/) returns uint256 { + // monotonicity + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + x > y => symbolic_toAssetsDown(x, ta, ts) >= symbolic_toAssetsDown(y, ta, ts); + // additivity with respect to side effect + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + symbolic_toAssetsDown(x, ta, ts) + symbolic_toAssetsDown(y, ta + symbolic_toAssetsDown(x, ta, ts), ts + x) <= symbolic_toAssetsDown(x + y, ta, ts); +} + +ghost symbolic_toSharesUp(mathint /*assets*/, mathint /*totalAssets*/, mathint /*totalShares*/) returns uint256 { + // monotonicity + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + x > y => symbolic_toSharesUp(x, ta, ts) >= symbolic_toSharesUp(y, ta, ts); + // additivity with respect to side effect + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + symbolic_toSharesUp(x, ta, ts) + symbolic_toSharesUp(y, ta - x, ts - symbolic_toSharesUp(x, ta, ts)) >= symbolic_toSharesUp(x + y, ta, ts); + axiom forall mathint x. forall mathint ta. forall mathint ts. symbolic_toSharesUp(x, ta, ts) == 0 <=> x == 0; +} + + +ghost symbolic_toAssetsUp(mathint /*shares*/, mathint /*totalAssets*/, mathint /*totalShares*/) returns uint256 { + // monotonicity + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + x > y => symbolic_toAssetsUp(x, ta, ts) >= symbolic_toAssetsUp(y, ta, ts); + // additivity with respect to side effect + axiom forall mathint x. forall mathint y. forall mathint ta. forall mathint ts. + symbolic_toAssetsUp(x, ta, ts) + symbolic_toAssetsUp(y, ta + symbolic_toAssetsUp(x, ta, ts), ts + x) >= symbolic_toAssetsUp(x + y, ta, ts); +} + +/*** verify that the ghost variables and axioms preserve the rules *****/ +use rule toSharesDown_additivity; +use rule toSharesDown_monotonicity; +use rule toAssetsDown_additivity; +use rule toAssetsDown_monotonicity; +use rule toSharesUp_additivity; +use rule toSharesUp_monotonicity; +use rule toSharesUp_nonZero; +use rule toAssetsUp_additivity; +use rule toAssetsUp_monotonicity; + +/** +@title Prove that adding in two steps is less beneficial to the user than doing it in one step +**/ +rule addAdditivity(uint256 assetId, uint256 amountX, uint256 amountY, address from) { + env e; + address spoke = e.msg.sender; + requireAllInvariants(assetId,e); + storage init = lastStorage; + + add(e, assetId, amountX); + add(e, assetId, amountY); + uint256 afterTwoSteps = getSpokeAddedShares(e, assetId, spoke); + + //expecting the code to enforce that amountX+amountY can not overflow + add(e, assetId, assert_uint256(amountX + amountY)) at init; + uint256 afterOneStep = getSpokeAddedShares(e, assetId, spoke); + + //rounding should be in favor of the house + assert afterOneStep >= afterTwoSteps; + satisfy afterOneStep > afterTwoSteps; +} + +/** +@title Prove that removing in two steps is less beneficial to the user than doing it in one step +**/ +rule removeAdditivity(uint256 assetId, uint256 amountX, uint256 amountY, address from) { + env e; + address spoke = e.msg.sender; + requireAllInvariants(assetId,e); + storage init = lastStorage; + + remove(e, assetId, amountX, from); + remove(e, assetId, amountY, from); + uint256 afterTwoSteps = getSpokeAddedShares(e, assetId, spoke); + + //expecting the code to enforce that amountX+amountY can not overflow + remove(e, assetId, assert_uint256(amountX + amountY), from)at init; + uint256 afterOneStep = getSpokeAddedShares(e, assetId, spoke); + + //rounding should be in favor of the house + assert afterOneStep >= afterTwoSteps; + satisfy afterOneStep > afterTwoSteps; +} + + +/** +@title Prove that drawing in two steps is less beneficial to the user than doing it in one step +**/ +rule drawAdditivity(uint256 assetId, uint256 amountX, uint256 amountY, address from) { + env e; + address spoke = e.msg.sender; + requireAllInvariants(assetId,e); + storage init = lastStorage; + + draw(e, assetId, amountX, from); + draw(e, assetId, amountY, from); + uint256 afterTwoSteps = getSpokeTotalOwed(e, assetId, spoke); + //expecting the code to enforce that amountX+amountY can not overflow + draw(e, assetId, assert_uint256(amountX + amountY), from)at init; + uint256 afterOneStep = getSpokeTotalOwed(e, assetId, spoke); + + //rounding should be in favor of the house + assert afterOneStep <= afterTwoSteps; + satisfy afterOneStep < afterTwoSteps; +} + +/** +@title Prove that restoring in two steps is less beneficial to the user than doing it in one step +**/ +rule restoreAdditivity(uint256 assetId, uint256 amountX, uint256 amountY, address from) { + env e; + address spoke = e.msg.sender; + requireAllInvariants(assetId,e); + storage init = lastStorage; + + IHubBase.PremiumDelta premiumDeltaX; + IHubBase.PremiumDelta premiumDeltaY; + IHubBase.PremiumDelta premiumDeltaXY; + require premiumDeltaXY.sharesDelta == premiumDeltaX.sharesDelta + premiumDeltaY.sharesDelta; + require premiumDeltaXY.offsetRayDelta == premiumDeltaX.offsetRayDelta + premiumDeltaY.offsetRayDelta; + require premiumDeltaXY.restoredPremiumRay == premiumDeltaX.restoredPremiumRay + premiumDeltaY.restoredPremiumRay; + + restore(e, assetId, amountX, premiumDeltaX); + restore(e, assetId, amountY, premiumDeltaY); + uint256 afterTwoSteps = getSpokeTotalOwed(e, assetId, spoke); + //expecting the code to enforce that amountX+amountY can not overflow + restore(e, assetId, assert_uint256(amountX + amountY), premiumDeltaXY) at init; + uint256 afterOneStep = getSpokeTotalOwed(e, assetId, spoke); + assert afterOneStep <= afterTwoSteps; + satisfy afterOneStep < afterTwoSteps; +} + +/** +@title Prove that reporting deficit in two steps is less beneficial to the user than doing it in one step +**/ +rule reportDeficitAdditivity(uint256 assetId, uint256 amountX, uint256 amountY) { + env e; + address spoke = e.msg.sender; + requireAllInvariants(assetId,e); + storage init = lastStorage; + IHubBase.PremiumDelta premiumDeltaX; + IHubBase.PremiumDelta premiumDeltaY; + IHubBase.PremiumDelta premiumDeltaXY; + + require premiumDeltaXY.sharesDelta == premiumDeltaX.sharesDelta + premiumDeltaY.sharesDelta; + require premiumDeltaXY.offsetRayDelta == premiumDeltaX.offsetRayDelta + premiumDeltaY.offsetRayDelta; + require premiumDeltaXY.restoredPremiumRay == premiumDeltaX.restoredPremiumRay + premiumDeltaY.restoredPremiumRay; + + reportDeficit(e, assetId, amountX, premiumDeltaX); + reportDeficit(e, assetId, amountY, premiumDeltaY); + uint256 afterTwoSteps = getSpokeTotalOwed(e, assetId, spoke); + //expecting the code to enforce that amountX+amountY can not overflow + reportDeficit(e, assetId, assert_uint256(amountX + amountY), premiumDeltaXY) at init; + uint256 afterOneStep = getSpokeTotalOwed(e, assetId, spoke); + assert afterOneStep <= afterTwoSteps; + satisfy afterOneStep < afterTwoSteps; +} + +/** +@title Prove that eliminating deficit in two steps is less beneficial to the user than doing it in one step +**/ +rule eliminateDeficitAdditivity(uint256 assetId, uint256 amountX, uint256 amountY, address spoke) { + env e; + + requireAllInvariants(assetId,e); + storage init = lastStorage; + eliminateDeficit(e, assetId, amountX, spoke); + eliminateDeficit(e, assetId, amountY, spoke); + uint256 afterTwoSteps = getSpokeAddedShares(e, assetId, spoke); + //expecting the code to enforce that amountX+amountY can not overflow + eliminateDeficit(e, assetId, require_uint256(amountX + amountY), spoke)at init; + uint256 afterOneStep = getSpokeAddedShares(e, assetId, spoke); + assert afterOneStep >= afterTwoSteps; + satisfy afterOneStep > afterTwoSteps; +} + +/** @title Draw operation increases debt shares and transfers assets to recipient */ +rule restore_debtDecrease(uint256 assetId, uint256 drawnAmount, IHubBase.PremiumDelta premiumDelta) { + env e; + requireAllInvariants(assetId,e); + address spoke = e.msg.sender; + uint256 beforeDebt = getSpokeTotalOwed(e, assetId, spoke); + //expecting the code to enforce that amountX+amountY can not overflow + restore(e, assetId, drawnAmount, premiumDelta); + uint256 afterDebt = getSpokeTotalOwed(e, assetId, spoke); + assert beforeDebt >= afterDebt; +} + +// optimize the calls to certain function and save in ghost (global) variable) +ghost uint256 supplyAmountBefore; +ghost uint256 supplyShareBefore; + +function requireAllInvariants(uint256 assetId, env e) { + // optimize the calls to + supplyAmountBefore = getAddedAssets(e,assetId); + supplyShareBefore = getAddedShares(e,assetId); + //requireInvariant totalAssetsVsShares(assetId,e); + require supplyAmountBefore >= supplyShareBefore; +} diff --git a/certora/spec/HubBase.spec b/certora/spec/HubBase.spec new file mode 100644 index 000000000..e780f8876 --- /dev/null +++ b/certora/spec/HubBase.spec @@ -0,0 +1,31 @@ + +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./symbolicRepresentation/Math_CVL.spec"; +import "./common.spec"; + + +/*** + +Base definitions used in all of Hub spec files + +Here we have only safe assumptions, safe summarization that are either proved in math.spec or a nondet summary + +***/ + +methods { + + function _.calculateInterestRate(uint256 assetId, uint256 liquidity, uint256 drawn, uint256 deficit, uint256 swept) external => NONDET; + + function Premium.calculatePremiumRay( + uint256 premiumShares, + int256 premiumOffsetRay, + uint256 drawnIndex + ) internal returns (uint256)=> calculatePremiumRayCVL(premiumShares, premiumOffsetRay, drawnIndex); + +} + +function calculatePremiumRayCVL(uint256 premiumShares, int256 premiumOffsetRay, uint256 drawnIndex) returns uint256 { + return require_uint256((premiumShares * drawnIndex) - premiumOffsetRay); +} + + \ No newline at end of file diff --git a/certora/spec/HubIntegrityRules.spec b/certora/spec/HubIntegrityRules.spec new file mode 100644 index 000000000..3b71a00a9 --- /dev/null +++ b/certora/spec/HubIntegrityRules.spec @@ -0,0 +1,107 @@ +/** +Hub verification integrity rules that verify that change is consistent. +Accrue is assumed to be called already. + +To run this spec file: + certoraRun certora/conf/HubIntegrityRules.conf +**/ + +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./symbolicRepresentation/Math_CVL.spec"; +import "./HubValidState.spec"; + + +/** @title Add operation increases external balances and increases internal accounting +while decreasing from balance */ +rule nothingForZero_add(uint256 assetId, uint256 amount, address from) { + + env e; + address asset = hub._assets[assetId].underlying; + address spoke = e.msg.sender; + uint256 internalBalanceBefore = hub._assets[assetId].liquidity; + uint256 spokeSharesBefore = hub._spokes[assetId][spoke].addedShares; + + add(e, assetId, amount); + + assert hub._assets[assetId].liquidity > internalBalanceBefore && hub._spokes[assetId][spoke].addedShares > spokeSharesBefore; +} + + +/** @title Remove operation decreases external balances and decreases internal accounting while increasing to balance*/ +rule nothingForZero_remove(uint256 assetId, uint256 amount, address to) { + + env e; + address asset = hub._assets[assetId].underlying; + address spoke = e.msg.sender; + uint256 externalBalanceBefore = balanceByToken[asset][hub]; + uint256 toBalanceBefore = balanceByToken[asset][to]; + uint256 spokeSharesBefore = hub._spokes[assetId][spoke].addedShares; + + remove(e, assetId, amount, to); + + assert balanceByToken[asset][hub] < externalBalanceBefore && hub._spokes[assetId][spoke].addedShares < spokeSharesBefore && toBalanceBefore < balanceByToken[asset][to]; + // no fee and no asset lost + assert balanceByToken[asset][hub] + balanceByToken[asset][to] == externalBalanceBefore + toBalanceBefore; +} + +/** @title Draw operation increases debt shares and transfers assets to recipient */ +rule nothingForZero_draw(uint256 assetId, uint256 amount, address to) { + env e; + address asset = hub._assets[assetId].underlying; + address spoke = e.msg.sender; + uint256 spokeDrawnSharesBefore = hub._spokes[assetId][spoke].drawnShares; + uint256 externalBalanceBefore = balanceByToken[asset][hub]; + uint256 toBalanceBefore = balanceByToken[asset][to]; + uint256 liquidityBefore = hub._assets[assetId].liquidity; + + draw(e,assetId,amount,to); + + assert hub._spokes[assetId][spoke].drawnShares > spokeDrawnSharesBefore && + balanceByToken[asset][hub] < externalBalanceBefore && + balanceByToken[asset][to] > toBalanceBefore && + hub._assets[assetId].liquidity < liquidityBefore; +} + +/** @title Draw operation increases debt shares and transfers assets to recipient */ +rule restore_debtDecrease(uint256 assetId, uint256 drawnAmount, IHubBase.PremiumDelta premiumDelta) { + env e; + requireAllInvariants(assetId,e); + address spoke = e.msg.sender; + uint256 beforeDebt = getSpokeTotalOwed(e, assetId, spoke); + + restore(e, assetId, drawnAmount, premiumDelta); + + uint256 afterDebt = getSpokeTotalOwed(e, assetId, spoke); + assert beforeDebt >= afterDebt; +} + + +/// @title reportDeficit return same value as previewRestoreByAssetsCVL +rule reportDeficitSameAsPreviewRestoreByAssets(uint256 assetId, uint256 drawnAmount) { + env e; + address spoke = e.msg.sender; + IHubBase.PremiumDelta premiumDelta; + requireAllInvariants(assetId,e); + storage init = lastStorage; + uint256 resultPreview = previewRestoreByAssets(e, assetId, drawnAmount); + uint256 resultReportDeficit = reportDeficit(e, assetId, drawnAmount, premiumDelta); + assert resultReportDeficit == resultPreview; +} + +/// @title only valid spoke can call the function +rule validSpokeOnly(uint256 assetId, method f) { + env e; + calldataarg args; + address spoke = e.msg.sender; + uint256 drawnShares = hub._spokes[assetId][spoke].drawnShares; + uint256 addedShares = hub._spokes[assetId][spoke].addedShares; + uint256 premiumShares = hub._spokes[assetId][spoke].premiumShares; + int200 premiumOffsetRay = hub._spokes[assetId][spoke].premiumOffsetRay; + + bool active = hub._spokes[assetId][spoke].active; + f(e,args); + assert drawnShares < hub._spokes[assetId][spoke].drawnShares => active ; + assert addedShares < hub._spokes[assetId][spoke].addedShares => active ; + assert premiumShares < hub._spokes[assetId][spoke].premiumShares => active ; + assert premiumOffsetRay != hub._spokes[assetId][spoke].premiumOffsetRay => active ; +} diff --git a/certora/spec/HubValidState.spec b/certora/spec/HubValidState.spec new file mode 100644 index 000000000..5beef2ad0 --- /dev/null +++ b/certora/spec/HubValidState.spec @@ -0,0 +1,466 @@ + +/*** + +Verify Hub - valid state properties +Where we assume a given single drawnIndex and that accrue was called on the asset + +To run this spec file: + certoraRun certora/conf/HubValidState.conf +***/ + +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./symbolicRepresentation/Math_CVL.spec"; +import "./HubBase.spec"; + + +using Hub as hub; + + +methods { + + // assume that drawn rate was already updated. + //rules concerning updateDrawnRate are in HubAccrueIntegrity.spec + function AssetLogic.updateDrawnRate( + IHub.Asset storage asset, + uint256 assetId + ) internal => NONDET; + + //assume a given single drawnIndex + //rules concerning getDrawnIndex are in HubAccrueIntegrity.spec + function AssetLogic.getDrawnIndex(IHub.Asset storage asset) internal returns (uint256) => cachedIndex; + + //rules concerning accrue are in HubAccrueIntegrity.spec + // In this spec we assume that the asset is not being used for fees, so getUnrealizedFees returns 0 + function AssetLogic.accrue(IHub.Asset storage asset) internal => accrueCalled(); + function AssetLogic.getUnrealizedFees( + IHub.Asset storage asset, + uint256 drawnIndex + ) internal returns (uint256) => 0; +} + +/************ Ghost Variables ************/ + +// assume a given single drawnIndex +ghost uint256 cachedIndex; + + +ghost mapping(uint256 /*assetId*/ => mapping(address /*spokeId*/ => uint256 )) spokeSupplyPerAssetMirror { + init_state axiom forall uint256 X. forall address Y. spokeSupplyPerAssetMirror[X][Y] == 0 ; + init_state axiom forall uint256 X. (usum address a. spokeSupplyPerAssetMirror[X][a]) == 0; +} + +ghost mapping(uint256 /*assetId*/ => mapping(address /*spokeId*/ => uint256 )) spokePremiumDrawnSharesPerAssetMirror { + init_state axiom forall uint256 X. forall address Y. spokePremiumDrawnSharesPerAssetMirror[X][Y] == 0 ; + init_state axiom forall uint256 X. (usum address a. spokePremiumDrawnSharesPerAssetMirror[X][a]) == 0; +} + +ghost mapping(uint256 /*assetId*/ => mapping(address /*spokeId*/ => uint256 )) spokeBaseDrawnPerAssetMirror { + init_state axiom forall uint256 X. forall address Y. spokeBaseDrawnPerAssetMirror[X][Y] == 0 ; + init_state axiom forall uint256 X. (usum address a. spokeBaseDrawnPerAssetMirror[X][a]) == 0; +} + +ghost mapping(uint256 /*assetId*/ => mapping(address /*spokeId*/ => int200 )) spokePremiumOffsetPerAssetMirror { + init_state axiom forall uint256 X. forall address Y. spokePremiumOffsetPerAssetMirror[X][Y] == 0 ; + init_state axiom forall uint256 X. (sum address a. spokePremiumOffsetPerAssetMirror[X][a]) == 0; +} + +ghost mapping(uint256 /*assetId*/ => mapping(address /*spokeId*/ => uint256 )) spokeDeficitPerAssetMirror { + init_state axiom forall uint256 X. forall address Y. spokeDeficitPerAssetMirror[X][Y] == 0 ; + init_state axiom forall uint256 X. (usum address a. spokeDeficitPerAssetMirror[X][a]) == 0; +} +ghost bool accrueCalledOnAsset; +//record accessed to debt fields before accrue +ghost bool unsafeAccessBeforeAccrue; + +/********** Function summary *****/ +function accrueCalled() { + accrueCalledOnAsset = true; +} + +/************ Hooks ************/ + +hook Sstore hub._assets[KEY uint256 assetId].drawnIndex uint120 new_value (uint120 old_value) { + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint120 value hub._assets[KEY uint256 assetId].drawnIndex { + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} +hook Sstore hub._assets[KEY uint256 assetId].addedShares uint120 new_value (uint120 old_value) { + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint120 value hub._assets[KEY uint256 assetId].addedShares { + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sstore hub._spokes[KEY uint256 assetId][KEY address spokeId].drawnShares uint120 new_value (uint120 old_value) { + spokeBaseDrawnPerAssetMirror[assetId][spokeId] = new_value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint120 value hub._spokes[KEY uint256 assetId][KEY address spokeId].drawnShares { + require spokeBaseDrawnPerAssetMirror[assetId][spokeId] == value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sstore hub._spokes[KEY uint256 assetId][KEY address spokeId].addedShares uint120 new_value (uint120 old_value) { + spokeSupplyPerAssetMirror[assetId][spokeId] = new_value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint120 value hub._spokes[KEY uint256 assetId][KEY address spokeId].addedShares { + require spokeSupplyPerAssetMirror[assetId][spokeId] == value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sstore hub._spokes[KEY uint256 assetId][KEY address spokeId].premiumShares uint120 new_value (uint120 old_value) { + spokePremiumDrawnSharesPerAssetMirror[assetId][spokeId] = new_value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint120 value hub._spokes[KEY uint256 assetId][KEY address spokeId].premiumShares { + require spokePremiumDrawnSharesPerAssetMirror[assetId][spokeId] == value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sstore hub._spokes[KEY uint256 assetId][KEY address spokeId].premiumOffsetRay int200 new_value (int200 old_value) { + spokePremiumOffsetPerAssetMirror[assetId][spokeId] = new_value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload int200 value hub._spokes[KEY uint256 assetId][KEY address spokeId].premiumOffsetRay { + require spokePremiumOffsetPerAssetMirror[assetId][spokeId] == value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sstore hub._spokes[KEY uint256 assetId][KEY address spokeId].deficitRay uint200 new_value (uint200 old_value) { + spokeDeficitPerAssetMirror[assetId][spokeId] = new_value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} + +hook Sload uint200 value hub._spokes[KEY uint256 assetId][KEY address spokeId].deficitRay { + require spokeDeficitPerAssetMirror[assetId][spokeId] == value; + unsafeAccessBeforeAccrue = unsafeAccessBeforeAccrue || !accrueCalledOnAsset; +} +/**** Valid State Rules *******/ + + +definition emptyAsset(uint256 assetId) returns bool = + hub._assets[assetId].addedShares == 0 && + hub._assets[assetId].liquidity == 0 && + hub._assets[assetId].addedShares == 0 && + hub._assets[assetId].deficitRay == 0 && + hub._assets[assetId].swept == 0 && + hub._assets[assetId].premiumShares == 0 && + hub._assets[assetId].premiumOffsetRay == 0 && + hub._assets[assetId].drawnShares == 0 && + hub._assets[assetId].drawnIndex == 0 && + hub._assets[assetId].drawnRate == 0 && + hub._assets[assetId].lastUpdateTimestamp == 0 && + hub._assets[assetId].underlying == 0 && + ( forall address spokeId. + hub._spokes[assetId][spokeId].addedShares == 0 && + hub._spokes[assetId][spokeId].drawnShares == 0 && + hub._spokes[assetId][spokeId].premiumShares == 0 && + hub._spokes[assetId][spokeId].premiumOffsetRay == 0 && + !hub._spokes[assetId][spokeId].active && + assetToSpokeIndexes[assetId][to_bytes32(spokeId)] == 0 + ); + + + +/** @title integrity of a validAsset +**/ +invariant validAssetId(uint256 assetId, address asset ) + // ensure that the asset is empty + (assetId >= hub._assetCount => emptyAsset(assetId)) && + // existence of the asset + (assetId < hub._assetCount => + // uniqueness of underlying + (forall uint256 otherAssetId. otherAssetId != assetId => hub._assets[assetId].underlying != hub._assets[otherAssetId].underlying ) && + // in list of underlying assets + (underlyingAssetsIndexes[to_bytes32(hub._assets[assetId].underlying)] != 0)) && + // not in underlyingAssetsIndexes implies no assetId with this underlying + (forall address asset1. asset1!=0 && underlyingAssetsIndexes[to_bytes32(asset1)] == 0 => (forall uint256 anyAssetId. hub._assets[anyAssetId].underlying != asset1 )) + { + preserved { + requireInvariant assetToSpokesIntegrity(assetId); + requireInvariant underlyingAssetsIntegrity(); + //requireInvariant validAssetId(otherAssetId, assetId); + } + preserved addAsset(address underlying, uint8 _decimals, address _feeReceiver, address _irStrategy, bytes _irData) with (env e) { + requireInvariant assetToSpokesIntegrity(assetId); + requireInvariant underlyingAssetsIntegrity(); + require underlying == asset; + } + } + + + + +/** +* @title the sum of hub._spokes[assetId][spoke].addedShares for all spoke equals to hub._assets[assetId].addedShares +*/ +invariant sumOfSpokeSupplyShares(uint256 assetId) + hub._assets[assetId].addedShares == (usum address spokeId. spokeSupplyPerAssetMirror[assetId][spokeId]) + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** +* @title the sum of hub._spokes[assetId][spoke].drawnShares for all spoke equals to hub._assets[assetId].drawnShares +*/ +invariant sumOfSpokeDrawnShares(uint256 assetId) + hub._assets[assetId].drawnShares == (usum address spokeId. spokeBaseDrawnPerAssetMirror[assetId][spokeId]) + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** +* @title the sum of hub._spokes[assetId][spoke].premiumShares for all spoke equals to hub._assets[assetId].premiumShares +*/ +invariant sumOfSpokePremiumDrawnShares(uint256 assetId) + hub._assets[assetId].premiumShares == (usum address spokeId. spokePremiumDrawnSharesPerAssetMirror[assetId][spokeId]) + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** +* @title the sum of hub._spokes[assetId][spoke].premiumOffsetRay for all spoke equals to hub._assets[assetId].premiumOffsetRay +*/ +invariant sumOfSpokePremiumOffset(uint256 assetId) + hub._assets[assetId].premiumOffsetRay == (sum address spokeId. spokePremiumOffsetPerAssetMirror[assetId][spokeId]) + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** +* @title the sum of hub._spokes[assetId][spoke].deficitRay for all spoke equals to hub._assets[assetId].deficitRay +*/ +invariant sumOfSpokeDeficit(uint256 assetId) + hub._assets[assetId].deficitRay == (usum address spokeId. spokeDeficitPerAssetMirror[assetId][spokeId]) + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** +* @title drawnIndex is greater than or equal to RAY on regular assets +**/ +invariant drawnIndexMin(uint256 assetId) + assetId < hub._assetCount => hub._assets[assetId].drawnIndex >= RAY + { + preserved { + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + } + } + +/** + * @title liquidityFee upper bound: config.liquidityFee must not exceed PercentageMathExtended.PERCENTAGE_FACTOR + */ +invariant liquidityFee_upper_bound(uint256 assetId) + hub._assets[assetId].liquidityFee <= PERCENTAGE_FACTOR; + + +/** + * @title premiumOffsetRay integrity: premiumOffsetRay must not exceed the premiumShares when converted to assets rounding up + */ +invariant premiumOffset_Integrity(uint256 assetId, address spokeId, env e) + hub.previewRestoreByShares(e,assetId,hub._assets[assetId].premiumShares) * hub._assets[assetId].drawnIndex >= hub._assets[assetId].premiumOffsetRay && + hub.previewRestoreByShares(e,assetId,hub._spokes[assetId][spokeId].premiumShares) * hub._assets[assetId].drawnIndex >= hub._spokes[assetId][spokeId].premiumOffsetRay + { + preserved with (env e1) { + requireAllInvariants(assetId, e1); + } + + } + + +/** +@title External balance is at least as internal accounting +**/ +strong invariant solvency_external(uint256 assetId ) + balanceByToken[hub._assets[assetId].underlying][hub] >= hub._assets[assetId].liquidity + { + preserved with (env e1) { + requireAllInvariants(assetId, e1); + } + preserved reclaim(uint256 assetId2, uint256 amount) with (env e2) + { + require hub._assets[assetId2].reinvestmentController != hub; + requireAllInvariants(assetId, e2); + } + + } + +/** +* @title the sum of added assets is greater than or equal to the sum of added shares +*/ +invariant totalAssetsVsShares(uint256 assetId, env e) + hub.getAddedAssets(e,assetId) >= hub.getAddedShares(e,assetId) + filtered { f-> f.selector != sig:hub.eliminateDeficit(uint256,uint256,address).selector }{ + + preserved with (env eInv) { + require eInv.block.timestamp == e.block.timestamp; + requireAllInvariants(assetId, e); + } + } + +rule totalAssetsVsShares_eliminateDeficit(uint256 assetId, uint256 amount, address spokeId) { + env e; + requireAllInvariants(assetId, e); + requireInvariant premiumOffset_Integrity(assetId, e.msg.sender,e); + eliminateDeficit(e, assetId, amount, spokeId); + assert hub.getAddedAssets(e,assetId) >= hub.getAddedShares(e,assetId); +} + + +///@title ghosts for _assetToSpokes EnumerableSet to keep track of the spokes for an asset +// part of proving validAssetId invariant +// For every storage variable we add a ghost field that is kept synchronized by hooks. +// The ghost fields can be accessed by the spec, even inside quantifiers. + +// ghost field for the _values array +ghost mapping(uint256 => mapping(mathint => bytes32)) assetToSpokeValues { + init_state axiom forall uint256 assetId. forall mathint x. assetToSpokeValues[assetId][x] == to_bytes32(0); +} +// ghost field for the _positions map +ghost mapping(uint256 => mapping(bytes32 => uint256)) assetToSpokeIndexes { + init_state axiom forall uint256 assetId. forall bytes32 x. assetToSpokeIndexes[assetId][x] == 0; +} +// ghost field for the length of the values array (stored in offset 0) +ghost mapping(uint256 => uint256) assetToSpokeLength { + init_state axiom forall uint256 assetId. assetToSpokeLength[assetId] == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom forall uint256 assetId. assetToSpokeLength[assetId] < max_uint256; +} + +ghost mapping(bytes32 => uint256) underlyingAssetsIndexes { + init_state axiom forall bytes32 x. underlyingAssetsIndexes[x] == 0; +} +ghost mapping(mathint => bytes32) underlyingAssetsValues { + init_state axiom forall mathint x. underlyingAssetsValues[x] == to_bytes32(0); +} +ghost uint256 underlyingAssetsLength { + init_state axiom underlyingAssetsLength == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom underlyingAssetsLength < max_uint256; +} + +// HOOKS +// Store hook to synchronize assetToSpokeLength with the length of the set._inner._values array. +hook Sstore hub._assetToSpokes[KEY uint256 assetId]._inner._values.length uint256 newLength { + assetToSpokeLength[assetId] = newLength; +} +// Store hook to synchronize assetToSpokeValues array with set._inner._values. +hook Sstore hub._assetToSpokes[KEY uint256 assetId]._inner._values[INDEX uint256 index] bytes32 newValue { + assetToSpokeValues[assetId][index] = newValue; +} +// Store hook to synchronize assetToSpokeIndexes array with set._inner._positions. +hook Sstore hub._assetToSpokes[KEY uint256 assetId]._inner._positions[KEY bytes32 value] uint256 newIndex { + assetToSpokeIndexes[assetId][value] = newIndex; +} + +// The load hooks can use require to ensure that the ghost field has the same information as the storage. +// The require is sound, since the store hooks ensure the contents are always the same. However we cannot +// prove that with invariants, since this would require the invariant to read the storage for all elements +// and neither storage access nor function calls are allowed in quantifiers. +// +// By following this simple pattern it is ensured that the ghost state and the storage are always the same +// and that the solver can use this knowledge in the proofs. + +// Load hook to synchronize assetToSpokeLength with the length of the set._inner._values array. +hook Sload uint256 length hub._assetToSpokes[KEY uint256 assetId]._inner._values.length { + require assetToSpokeLength[assetId] == length; +} +hook Sload bytes32 value hub._assetToSpokes[KEY uint256 assetId]._inner._values[INDEX uint256 index] { + require assetToSpokeValues[assetId][index] == value; +} +hook Sload uint256 index hub._assetToSpokes[KEY uint256 assetId]._inner._positions[KEY bytes32 value] { + require assetToSpokeIndexes[assetId][value] == index; +} + + +// Store hook to synchronize underlyingAssetsLength with the length of the set._inner._values array. +hook Sstore hub._underlyingAssets._inner._values.length uint256 newLength { + underlyingAssetsLength = newLength; +} +// Store hook to synchronize underlyingAssetsValues array with set._inner._values. +hook Sstore hub._underlyingAssets._inner._values[INDEX uint256 index] bytes32 newValue { + underlyingAssetsValues[index] = newValue; +} +// Store hook to synchronize underlyingAssetsIndexes array with set._inner._positions. +hook Sstore hub._underlyingAssets._inner._positions[KEY bytes32 value] uint256 newIndex { + underlyingAssetsIndexes[value] = newIndex; +} + +hook Sload uint256 length hub._underlyingAssets._inner._values.length { + require underlyingAssetsLength == length; +} +hook Sload bytes32 value hub._underlyingAssets._inner._values[INDEX uint256 index] { + require underlyingAssetsValues[index] == value; +} +hook Sload uint256 index hub._underlyingAssets._inner._positions[KEY bytes32 value] { + require underlyingAssetsIndexes[value] == index; +} + +// INVARIANTS + +// This is the main invariant stating that the indexes and values always match: +// values[indexes[v] - 1] = v for all values v in the set +// and indexes[values[i]] = i+1 for all valid indexes i. + +invariant assetToSpokesIntegrity(uint256 assetId) + (forall uint256 index. 0 <= index && index < assetToSpokeLength[assetId] => to_mathint(assetToSpokeIndexes[assetId][assetToSpokeValues[assetId][index]]) == index + 1) + && (forall bytes32 value. assetToSpokeIndexes[assetId][value] == 0 || + (assetToSpokeValues[assetId][assetToSpokeIndexes[assetId][value] - 1] == value && assetToSpokeIndexes[assetId][value] >= 1 && assetToSpokeIndexes[assetId][value] <= assetToSpokeLength[assetId])); + +invariant underlyingAssetsIntegrity() + (forall uint256 index. 0 <= index && index < underlyingAssetsLength => to_mathint(underlyingAssetsIndexes[underlyingAssetsValues[index]]) == index + 1) + && (forall bytes32 value. underlyingAssetsIndexes[value] == 0 || + (underlyingAssetsValues[underlyingAssetsIndexes[value] - 1] == value && underlyingAssetsIndexes[value] >= 1 && underlyingAssetsIndexes[value] <= underlyingAssetsLength)); + + + +// optimize the calls to certain function and save in ghost (global) variable) +ghost uint256 addedAssetsBefore; +ghost uint256 supplyShareBefore; + +function requireAllInvariants(uint256 assetId, env e) { + // optimize (reuse) the calls to getAddedAssets() and getTotalAddedShares() + addedAssetsBefore = hub.getAddedAssets(e,assetId); + supplyShareBefore = hub.getAddedShares(e,assetId); + //requireInvariant totalAssetsVsShares(assetId,e); + require addedAssetsBefore >= supplyShareBefore, "optimization"; + + + requireInvariant solvency_external(assetId); + requireInvariant sumOfSpokeDrawnShares(assetId); + requireInvariant sumOfSpokeSupplyShares(assetId); + requireInvariant sumOfSpokePremiumDrawnShares(assetId); + requireInvariant sumOfSpokePremiumOffset(assetId); + requireInvariant drawnIndexMin(assetId); + requireInvariant assetToSpokesIntegrity(assetId); + address anyAsset; + requireInvariant validAssetId(assetId, anyAsset); + requireInvariant liquidityFee_upper_bound(assetId); + requireInvariant underlyingAssetsIntegrity(); + require cachedIndex == hub._assets[assetId].drawnIndex; + +} \ No newline at end of file diff --git a/certora/spec/Spoke.spec b/certora/spec/Spoke.spec new file mode 100644 index 000000000..a73c5aea2 --- /dev/null +++ b/certora/spec/Spoke.spec @@ -0,0 +1,293 @@ + +/** + +Verify Spoke.sol + +Spoke internal properties using a symbolic representation of the Hub. + +To run this spec, run: +certoraRun certora/conf/Spoke.conf + +**/ +import "./SpokeBase.spec"; +import "./symbolicRepresentation/SymbolicHub.spec"; + +/* Assumption: userGhost is the user who is interacting with the Spoke contract. +It is used to track the user who is interacting with the Spoke contract. +In SpokeUserIntegrity.spec, we prove that only one user's account is updated and used at a time. +*/ +// Hooks to track userGhost +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares uint120 newValue (uint120 oldValue) { + require userGhost == user; +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares { + require userGhost == user; +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].drawnShares uint120 newValue (uint120 oldValue) { + require userGhost == user; +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].drawnShares { + require userGhost == user; +} + +/** +Verify functions that increase collateral or reduce debt and therefore do not need to perform a health check +**/ +rule increaseCollateralOrReduceDebtFunctions(method f) filtered {f -> !outOfScopeFunctions(f) && !f.isView && increaseCollateralOrReduceDebtFunctions(f)} { + uint256 reserveId; uint256 slot; + address user; + env e; + setup(); + requireInvariant validReserveId_single(reserveId); + require userGhost == user; + + //user state before the operation + bool beforePositionStatus_borrowing = isBorrowing[user][reserveId]; + bool beforePositionStatus_usingAsCollateral = isUsingAsCollateral[user][reserveId]; + uint120 beforeUserPosition_drawnShares = spoke._userPositions[user][reserveId].drawnShares; + uint120 beforeUserPosition_premiumShares = spoke._userPositions[user][reserveId].premiumShares; + int200 beforeUserPosition_premiumOffsetRay = spoke._userPositions[user][reserveId].premiumOffsetRay; + uint120 beforeUserPosition_suppliedShares = spoke._userPositions[user][reserveId].suppliedShares; + uint24 beforeUserPosition_dynamicConfigKey = spoke._userPositions[user][reserveId].dynamicConfigKey; + + + mathint premiumDebtBefore = (spoke._userPositions[user][reserveId].premiumShares * getAssetDrawnIndexCVL(spoke._reserves[reserveId].assetId, e))- spoke._userPositions[user][reserveId].premiumOffsetRay; + + // Execute the operation + calldataarg args; + f(e, args); + + // user state after the operation + bool afterPositionStatus_borrowing = isBorrowing[user][reserveId]; + bool afterPositionStatus_usingAsCollateral = isUsingAsCollateral[user][reserveId]; + uint120 afterUserPosition_drawnShares = spoke._userPositions[user][reserveId].drawnShares; + uint120 afterUserPosition_premiumShares = spoke._userPositions[user][reserveId].premiumShares; + int200 afterUserPosition_premiumOffsetRay = spoke._userPositions[user][reserveId].premiumOffsetRay; + uint120 afterUserPosition_suppliedShares = spoke._userPositions[user][reserveId].suppliedShares; + uint24 afterUserPosition_dynamicConfigKey = spoke._userPositions[user][reserveId].dynamicConfigKey; + + mathint premiumDebtAfter = (spoke._userPositions[user][reserveId].premiumShares * getAssetDrawnIndexCVL(spoke._reserves[reserveId].assetId, e)) - spoke._userPositions[user][reserveId].premiumOffsetRay; + + assert beforePositionStatus_borrowing == afterPositionStatus_borrowing || + (beforePositionStatus_borrowing && !afterPositionStatus_borrowing && afterUserPosition_drawnShares == 0 && afterUserPosition_premiumShares == 0 && afterUserPosition_premiumOffsetRay == 0); + + assert beforePositionStatus_usingAsCollateral == afterPositionStatus_usingAsCollateral; + assert beforeUserPosition_drawnShares >= afterUserPosition_drawnShares; + /* repay is proved in SpokeHubIntegrity.spec that it reduces the premium debt and drawn shares */ + if (f.selector != sig:repay(uint256, uint256, address).selector) { + assert premiumDebtBefore >= premiumDebtAfter; + } + assert beforeUserPosition_suppliedShares <= afterUserPosition_suppliedShares; + assert beforeUserPosition_dynamicConfigKey == afterUserPosition_dynamicConfigKey; +} + +/** +Verify that borrowing flag is set if and only if there are drawn shares +**/ +invariant isBorrowingIFFdrawnShares() +forall uint256 reserveId. forall address user. + spoke._userPositions[user][reserveId].drawnShares > 0 <=> isBorrowing[user][reserveId] +filtered {f -> !outOfScopeFunctions(f)} + + +/** +Verify that if there are no drawn shares, then there are no premium shares or offset +**/ +invariant drawnSharesZero(address user, uint256 reserveId) + spoke._userPositions[user][reserveId].drawnShares == 0 => ( spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0) + filtered {f -> !outOfScopeFunctions(f) && + // repay is proved in SpokeHubIntegrity.spec repay_zeroDebt + f.selector != sig:repay(uint256, uint256, address).selector + } + { + preserved with (env e) { + setup(); + } + } + + + + +invariant validReserveId() +forall uint256 reserveId. forall address user. + // exists + (reserveId < spoke._reserveCount => + // has underlying and hub + (spoke._reserves[reserveId].underlying != 0 && spoke._reserves[reserveId].hub != 0 && spoke._reserveExists[spoke._reserves[reserveId].hub][spoke._reserves[reserveId].assetId] ) + && + // not exists + (reserveId >= spoke._reserveCount => ( + // no one borrowed or used as collateral + !isBorrowing[user][reserveId] && !isUsingAsCollateral[user][reserveId] + // no supplied or drawn shares + && spoke._userPositions[user][reserveId].suppliedShares == 0 && spoke._userPositions[user][reserveId].drawnShares == 0 && + // no premium shares or offset + spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0 && + + // has no underlying, hub, assetId + spoke._reserves[reserveId].underlying == 0 && spoke._reserves[reserveId].assetId == 0 && spoke._reserves[reserveId].hub == 0 && spoke._reserves[reserveId].dynamicConfigKey == 0 && spoke._reserves[reserveId].flags == 0 && spoke._reserves[reserveId].collateralRisk == 0 ))) + + filtered {f -> f.selector != sig:multicall(bytes[]).selector && f.selector != sig:liquidationCall(uint256, uint256, address, uint256, bool).selector} + + +invariant validReserveId_single(uint256 reserveId) + + // exists + (reserveId < spoke._reserveCount => + // has underlying and hub + (spoke._reserves[reserveId].underlying != 0 && spoke._reserves[reserveId].hub != 0 && spoke._reserveExists[spoke._reserves[reserveId].hub][spoke._reserves[reserveId].assetId] )) + && + // not exists + (reserveId >= spoke._reserveCount => + // has no underlying, hub, assetId + spoke._reserves[reserveId].underlying == 0 && spoke._reserves[reserveId].assetId == 0 && spoke._reserves[reserveId].hub == 0 && spoke._reserves[reserveId].dynamicConfigKey == 0 && spoke._reserves[reserveId].flags == 0 && spoke._reserves[reserveId].collateralRisk == 0 && + + (forall address user. + // no one borrowed or used as collateral + !isBorrowing[user][reserveId] && !isUsingAsCollateral[user][reserveId] + // no supplied or drawn shares + && spoke._userPositions[user][reserveId].suppliedShares == 0 && spoke._userPositions[user][reserveId].drawnShares == 0 && + // no premium shares or offset + spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0 )) + + filtered {f -> !outOfScopeFunctions(f)} + { + preserved { + requireInvariant validReserveId_single(reserveId); + } + } + +// need to help the grounding, proven in validReserveId_single +function validReserveId_singleUser(uint256 reserveId, address user) { + require + (reserveId < spoke._reserveCount => + // has underlying and hub + (spoke._reserves[reserveId].underlying != 0 && spoke._reserves[reserveId].hub != 0 && spoke._reserveExists[spoke._reserves[reserveId].hub][spoke._reserves[reserveId].assetId] )) + && + // not exists + (reserveId >= spoke._reserveCount => + // has no underlying, hub, assetId + spoke._reserves[reserveId].underlying == 0 && spoke._reserves[reserveId].assetId == 0 && spoke._reserves[reserveId].hub == 0 && spoke._reserves[reserveId].dynamicConfigKey == 0 && spoke._reserves[reserveId].flags == 0 && spoke._reserves[reserveId].collateralRisk == 0 && + spoke._dynamicConfig[reserveId][0].collateralFactor == 0 && + // no one borrowed or used as collateral + !isBorrowing[user][reserveId] && !isUsingAsCollateral[user][reserveId] + // no supplied or drawn shares + && spoke._userPositions[user][reserveId].suppliedShares == 0 && spoke._userPositions[user][reserveId].drawnShares == 0 && + // no premium shares or offset + spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0 ); +} + + +/** +Verify that the assetId and hub are unique to a reserveId +**/ +invariant uniqueAssetIdPerReserveId(uint256 reserveId, uint256 otherReserveId) + (reserveId < spoke._reserveCount && otherReserveId < spoke._reserveCount && reserveId != otherReserveId ) => (spoke._reserves[reserveId].assetId != spoke._reserves[otherReserveId].assetId || spoke._reserves[reserveId].hub != spoke._reserves[otherReserveId].hub) + filtered {f -> !outOfScopeFunctions(f)} + { + preserved { + requireInvariant validReserveId_single(reserveId); + requireInvariant validReserveId_single(otherReserveId); + } + + } + +/** +Verify that the realized premium ray is consistent with the premium shares and drawn index +**/ +rule realizedPremiumRayConsistency(uint256 reserveId, address user, method f) + filtered {f -> !outOfScopeFunctions(f) && !f.isView} +{ + env e; + setup(); + requireInvariant validReserveId_single(reserveId); + require userGhost == user; + require spoke._userPositions[user][reserveId].premiumOffsetRay <= spoke._userPositions[user][reserveId].premiumShares * getAssetDrawnIndexCVL(spoke._reserves[reserveId].assetId, e); + calldataarg args; + f(e, args); + assert spoke._userPositions[user][reserveId].premiumOffsetRay <= spoke._userPositions[user][reserveId].premiumShares * getAssetDrawnIndexCVL(spoke._reserves[reserveId].assetId, e); +} + +/** +Verify that if there is no collateral, then there is no debt +**/ +rule noCollateralNoDebt(uint256 reserveIdUsed, address user, method f) + filtered {f -> !outOfScopeFunctions(f) && !f.isView && increaseCollateralOrReduceDebtFunctions(f)} { + env e; + setup(); + requireInvariant validReserveId_single(reserveIdUsed); + requireInvariant dynamicConfigKeyConsistency(reserveIdUsed,user); + validReserveId_singleUser(reserveIdUsed, user); + validReserveId_singleUser(spoke._reserveCount, user); + require userGhost == user; + ISpoke.UserAccountData beforeUserAccountData = getUserAccountData(e,user); + uint24 dynamicConfigKey = spoke._reserves[reserveIdUsed].dynamicConfigKey; + uint16 beforeCollateralFactor = spoke._dynamicConfig[reserveIdUsed][dynamicConfigKey].collateralFactor; + require beforeUserAccountData.totalCollateralValue == 0 => beforeUserAccountData.totalDebtValue == 0; + + calldataarg args; + f(e, args); + + ISpoke.UserAccountData afterUserAccountData = getUserAccountData(e,user); + uint24 dynamicConfigKeyAfter = spoke._reserves[reserveIdUsed].dynamicConfigKey; + uint16 afterCollateralFactor = spoke._dynamicConfig[reserveIdUsed][dynamicConfigKeyAfter].collateralFactor; + if (f.selector == sig:addDynamicReserveConfig(uint256, ISpoke.DynamicReserveConfig).selector) { + // assume we are working on reserveIdUsed + require dynamicConfigKeyAfter != dynamicConfigKey; + } + require beforeCollateralFactor > 0 => afterCollateralFactor > 0, "rule collateralFactorNotZero"; + assert afterUserAccountData.totalCollateralValue == 0 => afterUserAccountData.totalDebtValue == 0; +} + +/** +Verify that the collateral factor is not zero once set to a non-zero value +**/ + +rule collateralFactorNotZero(uint256 reserveId, address user, method f) filtered {f -> !outOfScopeFunctions(f) && !f.isView} { + env e; + setup(); + requireInvariant dynamicConfigKeyConsistency(reserveId,user); + validReserveId_singleUser(reserveId, user); + require userGhost == user; + uint24 dynamicConfigKey; + require dynamicConfigKey <= spoke._reserves[reserveId].dynamicConfigKey; + require spoke._dynamicConfig[reserveId][dynamicConfigKey].collateralFactor > 0; + calldataarg args; + f(e, args); + assert spoke._dynamicConfig[reserveId][dynamicConfigKey].collateralFactor > 0; +} + + + +/** +Verify that the user debt value is deterministic +**/ +rule deterministicUserDebtValue(uint256 reserveId, address user) { + env e; + setup(); + require userGhost == user; + uint256 drawnDebt; uint256 premiumDebt; + (drawnDebt, premiumDebt) = spoke.getUserDebt(e, reserveId, user); + uint256 drawnDebt2; uint256 premiumDebt2; + (drawnDebt2, premiumDebt2) = spoke.getUserDebt(e, reserveId, user); + assert drawnDebt == drawnDebt2; + assert premiumDebt == premiumDebt2; +} + +/** +Verify that the dynamic config key is consistent with the reserve dynamic config key +**/ +invariant dynamicConfigKeyConsistency(uint256 reserveId, address user) + spoke._userPositions[user][reserveId].dynamicConfigKey <= spoke._reserves[reserveId].dynamicConfigKey + filtered {f -> !outOfScopeFunctions(f)} +{ + preserved { + setup(); + requireInvariant validReserveId_single(reserveId); + } +} + + diff --git a/certora/spec/SpokeBase.spec b/certora/spec/SpokeBase.spec new file mode 100644 index 000000000..63cc21bca --- /dev/null +++ b/certora/spec/SpokeBase.spec @@ -0,0 +1,129 @@ +import "./symbolicRepresentation/Math_CVL.spec"; +import "./symbolicRepresentation/SymbolicPositionStatus.spec"; +import "./symbolicRepresentation/ERC20s_CVL.spec"; +import "./common.spec"; + +using SpokeInstance as spoke; + +/*** + +Base definitions used in all of Spoke spec files + +***/ +methods { + + function _.sortByKey(KeyValueList.List memory array) internal + => CVL_sort(array) expect void; + + function _._hashTypedData(bytes32 structHash) internal => NONDET; + + /* assumes a deterministic price for the reserve pre block.timestamp */ + function _.getReservePrice(uint256 reserveId) external with (env e)=> symbolicPrice(reserveId, e.block.timestamp) expect uint256; + + function MathUtils.uncheckedExp(uint256 a, uint256 b) internal returns (uint256) => limitedExp(a,b); + + function _.consumeScheduledOp(address caller, bytes data) external => NONDET ALL; + + // assume setReserveSource is trusted and does not call back into spoke or hub or any of the assets + function _.setReserveSource(uint256 reserveId, address source) external => NONDET ALL; + + function AuthorityUtils.canCallWithDelay( + address authority, + address caller, + address target, + bytes4 selector + ) internal returns (bool, uint32) => NONDET ALL; + + function SignatureChecker.isValidERC1271SignatureNow( + address signer, + bytes32 hash, + bytes memory signature + ) internal returns (bool) => NONDET ALL; +} + + +definition increaseCollateralOrReduceDebtFunctions(method f) returns bool = + f.selector != sig:withdraw(uint256, uint256, address).selector && + f.selector != sig:liquidationCall(uint256, uint256, address, uint256, bool).selector && + f.selector != sig:borrow(uint256, uint256, address).selector && + f.selector != sig:setUsingAsCollateral(uint256, bool, address).selector && + //f.selector != sig:repay(uint256,uint256,address).selector && + f.selector != sig:updateUserDynamicConfig(address).selector; + + + +function CVL_sort(KeyValueList.List array) { + if (array._inner.length > 1) { + require(array._inner[0] < array._inner[1]); + } + if (array._inner.length > 2) { + require(array._inner[1] < array._inner[2]); + } + if (array._inner.length > 3) { + require(array._inner[2] < array._inner[3]); + } +} + + +//deterministic non-zero value for each reserveId and timestamp +ghost symbolicPrice(uint256 /*reserveId*/, uint256 /*timestamp*/) returns uint256 { + axiom forall uint256 reserveId. forall uint256 timestamp. symbolicPrice(reserveId,timestamp) > 0; +} + + +function limitedExp(uint256 a, uint256 b) returns (uint256){ + // assumes that b is always the decimals of an asset + // computes 10^b + assert a == 10; + require ( b == 1 || b == 2 || b == 6 || b == 128, "limiting exp, used as decimals only"); + if (b == 1) { + return 10; + } + else if (b == 2) { + return 100; + } + else if (b == 6) { + return 1000000; + } + else if (b == 128) { + return require_uint256(10 ^ 128); + } + else { + require false; + return 0; + } +} + + + +definition outOfScopeFunctions(method f) returns bool = + f.selector == sig:multicall(bytes[]).selector || + f.selector == sig:liquidationCall(uint256, uint256, address, uint256, bool).selector; + + +function setup() { + + //requireInvariant validReserveId(); + require forall uint256 reserveId. forall address user. + // exists + (reserveId < spoke._reserveCount => + // has underlying and hub + (spoke._reserves[reserveId].underlying != 0 && spoke._reserves[reserveId].hub != 0 && spoke._reserveExists[spoke._reserves[reserveId].hub][spoke._reserves[reserveId].assetId] ) + && + // not exists + (reserveId >= spoke._reserveCount => ( + // no one borrowed or used as collateral + !isBorrowing[user][reserveId] && !isUsingAsCollateral[user][reserveId] + // no supplied or drawn shares + && spoke._userPositions[user][reserveId].suppliedShares == 0 && spoke._userPositions[user][reserveId].drawnShares == 0 && + // no premium shares or offset + spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0 && + + // has no underlying, hub, assetId + spoke._reserves[reserveId].underlying == 0 && spoke._reserves[reserveId].assetId == 0 && spoke._reserves[reserveId].hub == 0 && spoke._reserves[reserveId].dynamicConfigKey == 0 && spoke._reserves[reserveId].flags == 0 && spoke._reserves[reserveId].collateralRisk == 0 ))); + + //requireInvariant isBorrowingIFFdrawnShares(); + require forall uint256 reserveId. forall address user. + spoke._userPositions[user][reserveId].drawnShares > 0 <=> isBorrowing[user][reserveId]; + +} \ No newline at end of file diff --git a/certora/spec/SpokeHealthCheck.spec b/certora/spec/SpokeHealthCheck.spec new file mode 100644 index 000000000..822891d43 --- /dev/null +++ b/certora/spec/SpokeHealthCheck.spec @@ -0,0 +1,71 @@ +import "./SpokeBase.spec"; +import "./symbolicRepresentation/SymbolicHub.spec"; + +// Methods block for Spoke contract for proving that health factor is checked after updates to the user position which can reduce the health factor +// Note that this does not prove the health check logic itself +methods { + + function Spoke._processUserAccountData(address user, bool refreshConfig) internal returns (ISpoke.UserAccountData memory) => processUserAccountDataCVL(user, refreshConfig); + + + // proved in Spoke.spec that this function does not change the user position + // rule updateUserDynamicConfig_noChangeToDebtValue + function UserPositionDebt.applyPremiumDelta(ISpoke.UserPosition storage userPosition, IHubBase.PremiumDelta memory premiumDelta) internal => NONDET; +} + +persistent ghost mapping(address => uint256) ghostHealthFactor { + init_state axiom forall address user. ghostHealthFactor[user] == 0; +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].drawnShares uint120 newValue (uint120 oldValue) { + needHealthCheck(user); +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares uint120 newValue (uint120 oldValue) { + if (isUsingAsCollateral[user][reserveId]) { + needHealthCheck(user); + } +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumShares uint120 newValue (uint120 oldValue) { + needHealthCheck(user); +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumOffsetRay int200 newValue (int200 oldValue) { + needHealthCheck(user); +} + +hook Sstore _positionStatus[KEY address user].map[KEY uint256 slot] uint256 value { + needHealthCheck(user); +} + +function needHealthCheck(address user) { + uint256 newHealthFactor; + ghostHealthFactor[user] = newHealthFactor; +} + +function processUserAccountDataCVL(address user, bool refreshConfig) returns (ISpoke.UserAccountData) { + ISpoke.UserAccountData userAccountData; + require userAccountData.healthFactor == ghostHealthFactor[user]; + return userAccountData; +} + +rule userHealthStaysAboveThreshold(method f) filtered {f -> !outOfScopeFunctions(f) && !increaseCollateralOrReduceDebtFunctions(f)} { + uint256 HEALTH_FACTOR_LIQUIDATION_THRESHOLD = 10 ^ 18; + // Get the user address from the method call + address user; + env e; + setup(); + require userGhost == user; + + // Check health factor before the operation + require ghostHealthFactor[user] >= HEALTH_FACTOR_LIQUIDATION_THRESHOLD; + + // Execute the operation + calldataarg args; + f(e, args); + + // If the operation succeeded, check health factor after + assert ghostHealthFactor[user] >= HEALTH_FACTOR_LIQUIDATION_THRESHOLD; +} + diff --git a/certora/spec/SpokeHubIntegrity.spec b/certora/spec/SpokeHubIntegrity.spec new file mode 100644 index 000000000..5906f7508 --- /dev/null +++ b/certora/spec/SpokeHubIntegrity.spec @@ -0,0 +1,240 @@ +/** +Verify SpokeHubIntegrity.spec + +Verify the integrity of the Spoke contract related to Hub. +Assumption the Hub is the specific implementation in Hub.sol. + +To run this spec, run: +certoraRun certora/conf/SpokeWithHub.conf + +**/ + +import "./SpokeBase.spec"; +import "./HubValidState.spec"; +import "./symbolicRepresentation/SymbolicPositionStatus.spec"; +import "./symbolicRepresentation/ERC20s_CVL.spec"; + +// Note: 'spoke' alias is declared in SpokeBase.spec +// Note: 'hub' alias is declared in HubValidState.spec + + +/// Sum of all user supplied shares per reserveId +ghost mapping(uint256 /*reserveId*/ => mathint /*source*/) sumUserSuppliedSharesPerReserveId { + init_state axiom forall uint256 reserveId. sumUserSuppliedSharesPerReserveId[reserveId] == 0; +} + +// Hook on sstore and sload to synchronize the ghost with storage changes +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares uint120 newValue (uint120 oldValue) { + sumUserSuppliedSharesPerReserveId[reserveId] = sumUserSuppliedSharesPerReserveId[reserveId] + newValue - oldValue; +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares { + require sumUserSuppliedSharesPerReserveId[reserveId] >= value; +} + +/// Sum of all user drawn shares per reserveId +ghost mapping(uint256 /*reserveId*/ => mathint /*source*/) sumUserDrawnSharesPerReserveId { + init_state axiom forall uint256 reserveId. sumUserDrawnSharesPerReserveId[reserveId] == 0; +} + +// Hook on sstore and sload to synchronize the ghost with storage changes +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].drawnShares uint120 newValue (uint120 oldValue) { + sumUserDrawnSharesPerReserveId[reserveId] = sumUserDrawnSharesPerReserveId[reserveId] + newValue - oldValue; +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].drawnShares { + require sumUserDrawnSharesPerReserveId[reserveId] >= value; +} + +/// Sum of all user premium shares per reserveId +ghost mapping(uint256 /*reserveId*/ => mathint /*source*/) sumUserPremiumSharesPerReserveId { + init_state axiom forall uint256 reserveId. sumUserPremiumSharesPerReserveId[reserveId] == 0; +} + +// Hook on sstore and sload to synchronize the ghost with storage changes +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumShares uint120 newValue (uint120 oldValue) { + sumUserPremiumSharesPerReserveId[reserveId] = sumUserPremiumSharesPerReserveId[reserveId] + newValue - oldValue; +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].premiumShares { + require sumUserPremiumSharesPerReserveId[reserveId] >= value; +} + +/// Sum of all user premium offset per reserveId +ghost mapping(uint256 /*reserveId*/ => mathint /*source*/) sumUserPremiumOffsetPerReserveId { + init_state axiom forall uint256 reserveId. sumUserPremiumOffsetPerReserveId[reserveId] == 0; +} + +// Hook on sstore and sload to synchronize the ghost with storage changes +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumOffsetRay int200 newValue (int200 oldValue) { + sumUserPremiumOffsetPerReserveId[reserveId] = sumUserPremiumOffsetPerReserveId[reserveId] + to_mathint(newValue) - to_mathint(oldValue); +} + + + +/// Verify that the user drawn shares are consistent with the Hub drawn shares +invariant userDrawnShareConsistency(uint256 reserveId) + sumUserDrawnSharesPerReserveId[reserveId] == hub._spokes[spoke._reserves[reserveId].assetId][spoke].drawnShares && + ( reserveId >= spoke._reserveCount => + sumUserDrawnSharesPerReserveId[reserveId] == 0 + ) + filtered {f -> !outOfScopeFunctions(f)} + { + preserved with (env e) { + require e.msg.sender != spoke; + safeAssumptions(); + } + preserved constructor() { + require hub._spokes[spoke._reserves[reserveId].assetId][spoke].drawnShares == 0; + } + preserved addReserve(address hub_, uint256 assetId_arg, address priceSource, ISpoke.ReserveConfig config, ISpoke.DynamicReserveConfig dynamicConfig) with (env e) { + require hub_ == hub && assetId_arg == spoke._reserves[reserveId].assetId; + safeAssumptions(); + } + preserved repay(uint256 otherReserveId, uint256 amount, address onBehalfOf) with (env e) { + safeAssumptions(); + //proved in spoke.spec : uniqueAssetIdPerReserveId + require (reserveId < spoke._reserveCount && otherReserveId < spoke._reserveCount && reserveId != otherReserveId ) => (spoke._reserves[reserveId].assetId != spoke._reserves[otherReserveId].assetId ); + } + preserved borrow(uint256 otherReserveId, uint256 amount, address onBehalfOf) with (env e) { + safeAssumptions(); + //proved in spoke.spec : uniqueAssetIdPerReserveId + require (reserveId < spoke._reserveCount && otherReserveId < spoke._reserveCount && reserveId != otherReserveId ) => (spoke._reserves[reserveId].assetId != spoke._reserves[otherReserveId].assetId ); + } + + } + +/// Verify that the user premium shares are consistent with the Hub premium shares +invariant userPremiumShareConsistency(uint256 reserveId) + sumUserPremiumSharesPerReserveId[reserveId] == hub._spokes[spoke._reserves[reserveId].assetId][spoke].premiumShares && + ( reserveId >= spoke._reserveCount => + sumUserPremiumSharesPerReserveId[reserveId] == 0 + ) + filtered {f -> !outOfScopeFunctions(f)} + { + preserved with (env e) { + require e.msg.sender != spoke; + safeAssumptions(); + } + preserved constructor() { + require hub._spokes[spoke._reserves[reserveId].assetId][spoke].premiumShares == 0; + } + preserved addReserve(address hub_, uint256 assetId_arg, address priceSource, ISpoke.ReserveConfig config, ISpoke.DynamicReserveConfig dynamicConfig) with (env e) { + require hub_ == hub && assetId_arg == spoke._reserves[reserveId].assetId; + safeAssumptions(); + } + } + +/// Verify that the user premium offset is consistent with the Hub premium offset +invariant userPremiumOffsetConsistency(uint256 reserveId) + sumUserPremiumOffsetPerReserveId[reserveId] == hub._spokes[spoke._reserves[reserveId].assetId][spoke].premiumOffsetRay && + ( reserveId >= spoke._reserveCount => + sumUserPremiumOffsetPerReserveId[reserveId] == 0 + ) + filtered {f -> !outOfScopeFunctions(f)} + { + preserved with (env e) { + require e.msg.sender != spoke; + safeAssumptions(); + } + preserved constructor() { + require hub._spokes[spoke._reserves[reserveId].assetId][spoke].premiumOffsetRay == 0; + } + preserved addReserve(address hub_, uint256 assetId_arg, address priceSource, ISpoke.ReserveConfig config, ISpoke.DynamicReserveConfig dynamicConfig) with (env e) { + require hub_ == hub && assetId_arg == spoke._reserves[reserveId].assetId; + safeAssumptions(); + } + } + + +/// Verify that the user supplied shares are consistent with the Hub supplied shares +invariant userSuppliedShareConsistency(uint256 reserveId, uint256 assetId_) + sumUserSuppliedSharesPerReserveId[reserveId] <= hub._spokes[spoke._reserves[reserveId].assetId][spoke].addedShares + && + ( reserveId >= spoke._reserveCount => + sumUserSuppliedSharesPerReserveId[reserveId] == 0 + ) + filtered {f -> !outOfScopeFunctions(f)} + { + preserved with (env e) { + require e.msg.sender != spoke; + safeAssumptions(); + require hub._assets[spoke._reserves[reserveId].assetId].feeReceiver != spoke; + require hub._assets[assetId_].feeReceiver != spoke; + } + preserved addReserve(address hub_, uint256 assetId_arg, address priceSource, ISpoke.ReserveConfig config, ISpoke.DynamicReserveConfig dynamicConfig) with (env e) { + require hub_ == hub && assetId_arg == assetId_; + safeAssumptions(); + require hub._assets[spoke._reserves[reserveId].assetId].feeReceiver != spoke; + require hub._assets[assetId_].feeReceiver != spoke; + } + } + + + +// repay function reduces the debt of a user. Part of the rule increaseCollateralOrReduceDebtFunctions proven in spoke.spec for all functions. +rule repay_debtDecrease(uint256 reserveId, uint256 amount, address user) { + env e; + safeAssumptions(); + requireAllInvariants(spoke._reserves[reserveId].assetId, e); + requireInvariant premiumOffset_Integrity(spoke._reserves[reserveId].assetId, spoke,e); + + require userGhost == user; + + uint120 beforeUserPosition_drawnShares = spoke._userPositions[user][reserveId].drawnShares; + + mathint premiumDebtBefore = (spoke._userPositions[user][reserveId].premiumShares * cachedIndex)- spoke._userPositions[user][reserveId].premiumOffsetRay; + spoke.repay(e, reserveId, amount, user); + + uint120 afterUserPosition_drawnShares = spoke._userPositions[user][reserveId].drawnShares; + + mathint premiumDebtAfter = (spoke._userPositions[user][reserveId].premiumShares * cachedIndex)- spoke._userPositions[user][reserveId].premiumOffsetRay; + + + assert premiumDebtBefore >= premiumDebtAfter; + assert beforeUserPosition_drawnShares >= afterUserPosition_drawnShares; + +} + +/// Verify that if the user has no drawn shares, then there are no premium shares or offset. Part of the rule drawnSharesZero proven in spoke.spec for all functions. +rule repay_zeroDebt(uint256 reserveId, uint256 amount, address user) { + env e; + require spoke._userPositions[user][reserveId].drawnShares == 0 => ( spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0); + + spoke.repay(e, reserveId, amount, user); + + assert spoke._userPositions[user][reserveId].drawnShares == 0 => ( spoke._userPositions[user][reserveId].premiumShares == 0 && spoke._userPositions[user][reserveId].premiumOffsetRay == 0); +} + +function safeAssumptions() { + // rules proved in spoke.spec and assuming one hub + require forall uint256 reserveId. forall uint256 otherReserveId. + (reserveId != otherReserveId ) => spoke._reserves[reserveId].assetId != spoke._reserves[otherReserveId].assetId ; + + // a reservid that exists has underlying and hub + require forall uint256 reserveId. (reserveId < spoke._reserveCount => + // has underlying and hub + (spoke._reserves[reserveId].underlying != 0 && spoke._reserves[reserveId].hub == hub && spoke._reserveExists[spoke._reserves[reserveId].hub][spoke._reserves[reserveId].assetId] )); + + // a reservid that does not exist has no underlying, hub, assetId + require forall uint256 reserveId. reserveId >= spoke._reserveCount => ( + // has no underlying, hub, assetId + spoke._reserves[reserveId].underlying == 0 && spoke._reserves[reserveId].assetId == 0 && spoke._reserves[reserveId].hub == 0 && spoke._reserves[reserveId].dynamicConfigKey == 0); + + // based on hubValidState.spec : validAssetId + require forall uint256 assetId. assetId >= hub._assetCount => ( + hub._assets[assetId].addedShares == 0 && + hub._assets[assetId].drawnShares == 0 && + hub._assets[assetId].premiumShares == 0 && + hub._assets[assetId].premiumOffsetRay == 0 && + hub._assets[assetId].drawnIndex == 0 && + hub._assets[assetId].drawnRate == 0 && + hub._assets[assetId].lastUpdateTimestamp == 0 && + hub._spokes[assetId][spoke].addedShares == 0 && + hub._spokes[assetId][spoke].drawnShares == 0 && + hub._spokes[assetId][spoke].premiumShares == 0 && + hub._spokes[assetId][spoke].premiumOffsetRay == 0 && + !hub._spokes[assetId][spoke].active + ); + +} \ No newline at end of file diff --git a/certora/spec/SpokeUserIntegrity.spec b/certora/spec/SpokeUserIntegrity.spec new file mode 100644 index 000000000..32880ed06 --- /dev/null +++ b/certora/spec/SpokeUserIntegrity.spec @@ -0,0 +1,107 @@ +/** +@title Prove that only one user's account is updated and used at a time + +This allows us to assume that the user is the same throughout the operation in the Spoke.spec rules +*/ + +using SpokeInstance as spoke; + +methods { + // Note: _calculateLiquidationAmounts returns a struct, cannot use NONDET with struct return types + // Summary removed - function will be inlined or handled by default summary + + function Math.mulDiv(uint256 x, uint256 y, uint256 denominator) internal returns (uint256) => NONDET ALL; + function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal returns (uint256) => NONDET ALL; + + function LibBit.fls(uint256 x) internal returns (uint256) => NONDET ALL; + function LibBit.popCount(uint256 x) internal returns (uint256) => NONDET ALL; + + + function WadRayMath.rayMulDown(uint256 a, uint256 b) internal returns (uint256) => + NONDET ALL; + + function WadRayMath.rayMulUp(uint256 a, uint256 b) internal returns (uint256) => + NONDET ALL; + + function WadRayMath.rayDivDown(uint256 a, uint256 b) internal returns (uint256) => + NONDET ALL; + + function WadRayMath.rayDivUp(uint256 a, uint256 b) internal returns (uint256) => + NONDET ALL; + + function PercentageMath.percentMulDown(uint256 percentage, uint256 value) internal returns (uint256) => NONDET ALL; + + function PercentageMath.percentMulUp(uint256 percentage, uint256 value) internal returns (uint256) => NONDET ALL; + + function WadRayMath.wadDivUp(uint256 a, uint256 b) internal returns (uint256) => NONDET ALL; + + + function _.sortByKey(KeyValueList.List memory array) internal + => NONDET ALL; + + function _._hashTypedData(bytes32 structHash) internal => NONDET; +} + +persistent ghost address assumeUser; +persistent ghost bool detectedMisuse; + +function checkAndSetUser(address user) { + if (assumeUser != user && assumeUser != 0) { + detectedMisuse = true; + } + assumeUser = user; +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].drawnShares uint120 newValue (uint120 oldValue) { + checkAndSetUser(user); +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].drawnShares { + checkAndSetUser(user); +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares uint120 newValue (uint120 oldValue) { + checkAndSetUser(user); +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].suppliedShares { + checkAndSetUser(user); +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumShares uint120 newValue (uint120 oldValue) { + checkAndSetUser(user); +} + +hook Sload uint120 value _userPositions[KEY address user][KEY uint256 reserveId].premiumShares { + checkAndSetUser(user); +} + +hook Sstore _userPositions[KEY address user][KEY uint256 reserveId].premiumOffsetRay int200 newValue (int200 oldValue) { + checkAndSetUser(user); +} + +hook Sload int200 value _userPositions[KEY address user][KEY uint256 reserveId].premiumOffsetRay { + checkAndSetUser(user); +} + +hook Sload uint256 value _positionStatus[KEY address user].map[KEY uint256 slot] { + checkAndSetUser(user); +} + +hook Sstore _positionStatus[KEY address user].map[KEY uint256 slot] uint256 value { + checkAndSetUser(user); +} + +rule userIntegrity(method f) filtered {f -> f.selector != sig:liquidationCall(uint256, uint256, address, uint256, bool).selector } +{ + env e; + calldataarg args; + + assumeUser = 0 ; + detectedMisuse = false; + + f(e, args); + + assert !detectedMisuse; +} + diff --git a/certora/spec/common.spec b/certora/spec/common.spec new file mode 100644 index 000000000..e6ff6e16b --- /dev/null +++ b/certora/spec/common.spec @@ -0,0 +1,57 @@ +/*** +Common method summaries used in both Hub and Spoke spec files +***/ + +methods { + + function _.mulDivDown(uint256 a, uint256 b, uint256 c) internal => + mulDivDownCVL(a,b,c) expect uint256; + + function _.mulDivUp(uint256 a, uint256 b, uint256 c) internal => + mulDivUpCVL(a,b,c) expect uint256; + + function _.rayMulDown(uint256 a, uint256 b) internal => + mulDivRayDownCVL(a,b) expect uint256; + + function _.rayMulUp(uint256 a, uint256 b) internal => + mulDivRayUpCVL(a,b) expect uint256; + + function _.rayDivDown(uint256 a, uint256 b) internal => + mulDivDownCVL(a,RAY,b) expect uint256; + + function _.fromRayUp(uint256 a) internal => + divRayUpCVL(a) expect uint256; + + function _.toRay(uint256 a) internal => + mulRayCVL(a) expect uint256; + + function _.wadDivUp(uint256 a, uint256 b) internal => + mulDivUpCVL(a,WAD,b) expect uint256; + + function _.wadDivDown(uint256 a, uint256 b) internal => + mulDivDownCVL(a,WAD,b) expect uint256; + + + function PercentageMath.percentMulDown(uint256 percentage, uint256 value) internal returns (uint256) => + mulDivDownCVL(value,percentage,PERCENTAGE_FACTOR); + + function PercentageMath.percentMulUp(uint256 percentage, uint256 value) internal returns (uint256) => + mulDivUpCVL(value,percentage,PERCENTAGE_FACTOR); + + function _._checkCanCall(address caller, bytes calldata data) internal => NONDET; + + function _.setInterestRateData(uint256 assetId, bytes data) external => NONDET; +} + + +persistent ghost uint256 RAY { + axiom RAY == 10^27; + } + +persistent ghost uint256 WAD { + axiom WAD == 10^18; + } + +persistent ghost uint256 PERCENTAGE_FACTOR { + axiom PERCENTAGE_FACTOR == 10000; + } \ No newline at end of file diff --git a/certora/spec/libs/LibBit.spec b/certora/spec/libs/LibBit.spec new file mode 100644 index 000000000..83e1d7ca2 --- /dev/null +++ b/certora/spec/libs/LibBit.spec @@ -0,0 +1,59 @@ + +/** + +Verification of Solady's LibBit.sol +**/ + +methods { + function popCount(uint256 x) external returns (uint256) envfree; + function fls(uint256 x) external returns (uint256) envfree; + function isBitTrue(uint256 x, uint16 pos) external returns (bool) envfree; + function changeOneBit(uint256 x, uint16 pos) external returns (uint256 ) envfree; +} + +/** @title popCount_integrity +popCount(x) is the number of set bits in x. +Prove by proving that by flipping one bit, the popCount changes by at most one. +**/ +rule popCount_integrity(uint256 x, uint16 pos) { + + // base check + assert popCount(0) == 0; + assert popCount(max_uint256) == 256; + + // pos is from 0 to 255 + require pos <= 255; + uint256 x_count = popCount(x); + // flip bit pos + uint256 x_prime = changeOneBit(x,pos); + // count again + uint256 x_prime_count = popCount(x_prime); + // must change by one + assert x_prime_count - 1 == x_count || x_count == x_prime_count + 1; + // if changed from on to off then bit count should increase by one, + // this also implies that if changed from off to on then count must decrease by one + assert isBitTrue(x, pos) <=> x_count == x_prime_count + 1; +} +///@title popCount should never revert +rule popCount_noRevert(uint256 x) { + popCount@withrevert(x); + assert !lastReverted; +} + +/** @title fls(x) is the position of the last (most significant) set bit in x. +Verifying by checking that any bit below the fls(x) is not set. +**/ +rule fls_integrity(uint256 x, uint16 pos) { + // base check + assert x == 0 <=> fls(x) == 256; + + uint256 r = fls(x); + assert (pos > r && pos < 256 ) => !isBitTrue(x, pos); + assert r < 256 => isBitTrue(x, assert_uint16(r)); +} + +/// @title fls should never revert +rule fls_noRevert(uint256 x) { + fls@withrevert(x); + assert !lastReverted; +} diff --git a/certora/spec/libs/Math.spec b/certora/spec/libs/Math.spec new file mode 100644 index 000000000..b8bb1f58e --- /dev/null +++ b/certora/spec/libs/Math.spec @@ -0,0 +1,231 @@ +import "../symbolicRepresentation/Math_CVL.spec"; + + +/** +Prove the summarization of mathematical functions. + +For each summarization prove that the cvl representation is exactly the same of the solidity implementation. +For each summarization there is a rule that proves: +1. same value +2. reverts on the same cases + +To run this spec file: + certoraRun certora/conf/Math.conf + +**/ + + methods { + // envfree functions + function RAY() external returns (uint256) envfree; + function WAD() external returns (uint256) envfree; + function rayMulDown(uint256 a, uint256 b) external returns (uint256) envfree; + function rayMulUp(uint256 a, uint256 b) external returns (uint256) envfree; + function rayDivDown(uint256 a, uint256 b) external returns (uint256) envfree; + function rayDivUp(uint256 a, uint256 b) external returns (uint256) envfree; + function wadDivDown(uint256 a, uint256 b) external returns (uint256) envfree; + function wadDivUp(uint256 a, uint256 b) external returns (uint256) envfree; + function percentMulDown(uint256 percentage, uint256 value) external returns (uint256) envfree; + function percentMulUp(uint256 percentage, uint256 value) external returns (uint256) envfree; + function mulDivDown(uint256 x, uint256 y, uint256 denominator) external returns (uint256) envfree; + function mulDivUp(uint256 x, uint256 y, uint256 denominator) external returns (uint256) envfree; + function fromRayUp(uint256 a) external returns (uint256) envfree; + function toRay(uint256 a) external returns (uint256) envfree; + + } + + +/** @title Prove: + function MathUtils.mulDivDown(uint256 x, uint256 y, uint256 denominator) internal returns (uint256) => + mulDivDownCVL(x,y,denominator); +*/ + rule MathUtils_mulDivDown(uint256 x, uint256 y, uint256 denominator) { + uint256 cvlResult = mulDivDownCVL@withrevert(x, y, denominator); + bool cvlReverted = lastReverted; + uint256 solResult = mulDivDown@withrevert(x, y, denominator); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + + +/** @title Prove: + function MathUtils.mulDivUp(uint256 x, uint256 y, uint256 denominator) internal returns (uint256) => + mulDivUpCVL(x,y,denominator); +*/ + rule MathUtils_mulDivUp(uint256 x, uint256 y, uint256 denominator) { + uint256 cvlResult = mulDivUpCVL@withrevert(x, y, denominator); + bool cvlReverted = lastReverted; + uint256 solResult = mulDivUp@withrevert(x, y, denominator); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.rayMulDown(uint256 a, uint256 b) internal returns (uint256) => + mulDivDownCVL(a,b,wadRayMath.RAY()); +*/ + rule WadRayMathExtended_rayMulDown(uint256 a, uint256 b) { + uint256 cvlResult = mulDivDownCVL@withrevert(a, b, RAY()); + bool cvlReverted = lastReverted; + uint256 solResult = rayMulDown@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + + +/** @title Prove: + function WadRayMathExtended.rayMulUp(uint256 a, uint256 b) internal returns (uint256) => + mulDivUpCVL(a,b,wadRayMath.RAY()); +*/ + rule WadRayMathExtended_rayMulUp(uint256 a, uint256 b) { + uint256 cvlResult = mulDivUpCVL@withrevert(a, b, RAY()); + bool cvlReverted = lastReverted; + uint256 solResult = rayMulUp@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.rayDivDown(uint256 a, uint256 b) internal returns (uint256) => + mulDivDownCVL(a,wadRayMath.RAY(),b); +*/ + rule WadRayMathExtended_rayDivDown(uint256 a, uint256 b) { + uint256 cvlResult = mulDivDownCVL@withrevert(a, RAY(), b); + bool cvlReverted = lastReverted; + uint256 solResult = rayDivDown@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.rayDivUp(uint256 a, uint256 b) internal returns (uint256) => + mulDivUpCVL(a,wadRayMath.RAY(),b); +*/ + rule WadRayMathExtended_rayDivUp(uint256 a, uint256 b) { + uint256 cvlResult = mulDivUpCVL@withrevert(a, RAY(), b); + bool cvlReverted = lastReverted; + uint256 solResult = rayDivUp@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.wadDivDown(uint256 a, uint256 b) internal returns (uint256) => + mulDivDownCVL(a,wadRayMath.WAD(),b); +*/ + rule WadRayMathExtended_wadDivDown(uint256 a, uint256 b) { + uint256 cvlResult = mulDivDownCVL@withrevert(a, WAD(), b); + bool cvlReverted = lastReverted; + uint256 solResult = wadDivDown@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.wadDivUp(uint256 a, uint256 b) internal returns (uint256) => + mulDivUpCVL(a,wadRayMath.WAD(),b); +*/ + rule WadRayMathExtended_wadDivUp(uint256 a, uint256 b) { + uint256 cvlResult = mulDivUpCVL@withrevert(a, WAD(), b); + bool cvlReverted = lastReverted; + uint256 solResult = wadDivUp@withrevert(a, b); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.fromRayUp(uint256 a) internal returns (uint256) => + divRayUpCVL(a) expect uint256; +*/ + rule WadRayMathExtended_fromRayUp(uint256 a) { + uint256 cvlResult = divRayUpCVL@withrevert(a); + bool cvlReverted = lastReverted; + uint256 solResult = fromRayUp@withrevert(a); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function WadRayMathExtended.toRay(uint256 a) internal returns (uint256) => + mulRayCVL(a); +*/ + rule WadRayMathExtended_toRay(uint256 a) { + uint256 cvlResult = mulRayCVL@withrevert(a); + bool cvlReverted = lastReverted; + uint256 solResult = toRay@withrevert(a); + bool solReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: + function PercentageMath.percentMulDown(uint256 value, uint256 percentage) internal returns (uint256) => + mulDivDownCVL(value, percentage, PERCENTAGE_FACTOR); +*/ + rule percentMulDown_integrity(uint256 percentage, uint256 value) { + uint256 solResult = percentMulDown@withrevert(value, percentage); + bool solReverted = lastReverted; + uint256 cvlResult = mulDivDownCVL@withrevert(value, percentage, PERCENTAGE_FACTOR); + bool cvlReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: order of arguments does not matter for percentMulDown +*/ + rule percentMulDown_associativity(uint256 percentage, uint256 value) { + uint256 result1 = percentMulDown@withrevert(percentage, value); + bool result1Reverted = lastReverted; + uint256 result2 = percentMulDown@withrevert(value, percentage); + bool result2Reverted = lastReverted; + assert result1Reverted == result2Reverted; + assert !result1Reverted => result1 == result2; + satisfy value == 0 && !result1Reverted; + satisfy percentage == 0 && !result1Reverted; + } + +/** @title Prove: + function PercentageMath.percentMulUp(uint256 value, uint256 percentage) internal returns (uint256) => + mulDivUpCVL(value, percentage, PERCENTAGE_FACTOR); +*/ + rule percentMulUp_integrity(uint256 percentage, uint256 value) { + uint256 solResult = percentMulUp@withrevert(value, percentage); + bool solReverted = lastReverted; + uint256 cvlResult = mulDivUpCVL@withrevert(value, percentage, PERCENTAGE_FACTOR); + bool cvlReverted = lastReverted; + assert cvlReverted == solReverted; + assert !cvlReverted => cvlResult == solResult; + } + +/** @title Prove: order of arguments does not matter for percentMulUp +*/ + rule percentMulUp_associativity(uint256 percentage, uint256 value) { + uint256 result1 = percentMulUp@withrevert(percentage, value); + bool result1Reverted = lastReverted; + uint256 result2 = percentMulUp@withrevert(value, percentage); + bool result2Reverted = lastReverted; + assert result1Reverted == result2Reverted; + assert !result1Reverted => result1 == result2; + satisfy value == 0 && !result1Reverted; + satisfy percentage == 0 && !result1Reverted; + } + + rule RAY_definition() { + assert RAY() == 10^27; + } + + rule WAD_definition() { + assert WAD() == 10^18; + } + + persistent ghost uint256 PERCENTAGE_FACTOR { + axiom PERCENTAGE_FACTOR == 10000; + } \ No newline at end of file diff --git a/certora/spec/libs/PositionStatus.spec b/certora/spec/libs/PositionStatus.spec new file mode 100644 index 000000000..cd90a551a --- /dev/null +++ b/certora/spec/libs/PositionStatus.spec @@ -0,0 +1,187 @@ +/** + +Verification of the PositionStatusMap.sol library. +Use summarization of the LibBit.sol library that is verified in LibBit.spec. + +To run this spec file: + certoraRun certora/conf/PositionStatus.conf + +The rules here are used as axioms in the SymbolicPositionStatus.spec file. + +**/ + +methods { + function setBorrowing(uint256 reserveId, bool borrowing) external envfree; + function setUsingAsCollateral(uint256 reserveId, bool usingAsCollateral) external envfree ; + function isUsingAsCollateralOrBorrowing(uint256 reserveId) external returns (bool) envfree; + function isBorrowing(uint256 reserveId) external returns (bool) envfree; + function isUsingAsCollateral(uint256 reserveId) external returns (bool) envfree; + function collateralCount(uint256 reserveCount) external returns (uint256) envfree; + function next(uint256 startReserveId) external returns (uint256, bool, bool) envfree; + function nextBorrowing(uint256 startReserveId) external returns (uint256) envfree; + function nextCollateral(uint256 startReserveId) external returns (uint256) envfree; + function getBucketWord(uint256 reserveId) external returns (uint256) envfree; + + function _.fls(uint256 word) internal => flsResult(word) expect uint256; + +} + + +///@dev flsResult(word) is the position of the last (most significant) set bit in word. +// Represented as a ghost based on proof in LibBit.spec rule fls_integrity +ghost flsResult(uint256) returns uint256 { + // zero case + axiom forall uint256 word. word == 0 <=> flsResult(word) == 256; + axiom forall uint256 word. word != 0 => word >> flsResult(word) == 1; +} + + +function getBorrowingBitId(uint256 reserveId) returns uint256 { + return require_uint256(reserveId % 128) << 1; +} + +function getUsingAsCollateralBitId(uint256 reserveId) returns uint256 { + return require_uint256((require_uint256(reserveId % 128) << 1) + 1); +} + +/** @title prove that setBorrowing preserves the flags for any other reserve +and sets the borrowing flag for the given reserve to the given value +**/ +rule setBorrowing(uint256 reserveId1, bool borrowing) { + uint256 reserveId2; uint256 reserveId3; + bool before = isBorrowing(reserveId2); + bool collateralFlag = isUsingAsCollateral(reserveId3); + setBorrowing(reserveId1, borrowing); + bool after = isBorrowing(reserveId2); + assert(reserveId1 != reserveId2 => before == after); + assert(reserveId1 == reserveId2 => borrowing == after); + assert(collateralFlag == isUsingAsCollateral(reserveId3)); +} + +/** @title prove that setUsingAsCollateral preserves the flags for any other reserve +and sets the usingAsCollateral flag for the given reserve to the given value +**/ +rule setUsingAsCollateral(uint256 reserveId1, bool usingAsCollateral) { + uint256 reserveId2; uint256 reserveId3; + bool before = isUsingAsCollateral(reserveId2); + bool borrowingFlag = isBorrowing(reserveId3); + + setUsingAsCollateral(reserveId1, usingAsCollateral); + bool after = isUsingAsCollateral(reserveId2); + assert(reserveId1 != reserveId2 => before == after); + assert(reserveId1 == reserveId2 => usingAsCollateral == after); + assert(borrowingFlag == isBorrowing(reserveId3)); +} + +/** @title prove that isUsingAsCollateralOrBorrowing returns true if the reserve is using as collateral or borrowing +**/ +rule isUsingAsCollateralOrBorrowing(uint256 reserveId) { + assert isUsingAsCollateralOrBorrowing(reserveId) <=> ( isUsingAsCollateral(reserveId) || isBorrowing(reserveId)); +} + +/** @title prove that collateralCount returns the correct number of reserves due to setUsingAsCollateral +**/ +rule collateralCount(uint256 reserveCount, bool usingAsCollateral, uint256 reserveId) { + /// todo prove in spoke that reserveCount is correct + require reserveId < reserveCount; + uint256 countBefore = collateralCount(reserveCount); + bool flagBefore = isUsingAsCollateral(reserveId); + setUsingAsCollateral(reserveId, usingAsCollateral); + uint256 countAfter = collateralCount(reserveCount); + assert(usingAsCollateral == flagBefore => countBefore == countAfter); + assert(usingAsCollateral != flagBefore => countAfter == countBefore + (usingAsCollateral ? 1 : -1)); +} + +/** @title prove that max_uint256 is not a valid reserve id +**/ +invariant maxUintNotValidReserveId() + !isBorrowing(max_uint256) && !isUsingAsCollateral(max_uint256) { + preserved setBorrowing(uint256 _reserveId, bool _borrowing) { + require _reserveId != max_uint256; + } + preserved setUsingAsCollateral(uint256 _reserveId, bool _usingAsCollateral) { + require _reserveId != max_uint256; + } + } + + +/** @title prove that next returns the next reserve id using as collateral or borrowing. +1. compare with nextBorrowing and nextCollateral +2. make sure that any reserve id between the startReserveId and the next reserve id is not using as collateral or borrowing +**/ + +rule next(uint256 startReserveId) { + uint256 NOT_FOUND = max_uint256; + uint256 reserveId; + bool borrowing; + bool collateral; + requireInvariant maxUintNotValidReserveId(); + + reserveId, borrowing, collateral = next(startReserveId); + + uint256 nextBorrowingId = nextBorrowing(startReserveId); + + uint256 nextCollateralId = nextCollateral(startReserveId); + + + assert(reserveId == NOT_FOUND <=> (nextBorrowingId == NOT_FOUND && nextCollateralId == NOT_FOUND)); + assert(reserveId != NOT_FOUND => (nextBorrowingId == reserveId || nextCollateralId == reserveId)); + assert(reserveId != NOT_FOUND => reserveId < startReserveId); + + uint256 reserveIdBetween; + + assert (reserveIdBetween < startReserveId && reserveIdBetween > reserveId)=>(!isBorrowing(reserveIdBetween) && !isUsingAsCollateral(reserveIdBetween)); + + assert(reserveId != NOT_FOUND => (borrowing <=> isBorrowing(reserveId))); + assert(reserveId != NOT_FOUND => (collateral <=> isUsingAsCollateral(reserveId))); + assert(reserveId != NOT_FOUND => (borrowing <=> nextBorrowingId == reserveId)); + assert(reserveId != NOT_FOUND => (collateral <=> nextCollateralId == reserveId)); +} + +/** @title prove that nextBorrowing returns the next reserve id borrowing. +1. make sure that any reserve id between the startReserveId and the next reserve id is not borrowing +2. make sure that the next reserve id is borrowing +**/ +rule nextBorrowing(uint256 startReserveId) { + uint256 NOT_FOUND = max_uint256; + uint256 reserveId; + requireInvariant maxUintNotValidReserveId(); + reserveId = nextBorrowing(startReserveId); + assert(reserveId != NOT_FOUND => reserveId < startReserveId); + assert(reserveId != NOT_FOUND <=> isBorrowing(reserveId)); + + uint256 reserveIdBetween; + assert (reserveIdBetween < startReserveId && reserveIdBetween > reserveId) => !isBorrowing(reserveIdBetween); + + +} + +/** @title prove that nextCollateral returns the next reserve id using as collateral. +1. make sure that any reserve id between the startReserveId and the next reserve id is not using as collateral +2. make sure that the next reserve id is using as collateral +**/ +rule nextCollateral(uint256 startReserveId, uint256 reserveCount) { + uint256 NOT_FOUND = max_uint256; + uint256 reserveId; + requireInvariant maxUintNotValidReserveId(); + reserveId = nextCollateral(startReserveId); + assert(reserveId != NOT_FOUND => reserveId < startReserveId); + assert(reserveId != NOT_FOUND <=> isUsingAsCollateral(reserveId)); + + uint256 reserveIdBetween; + assert (reserveIdBetween < startReserveId && reserveIdBetween > reserveId) => !isUsingAsCollateral(reserveIdBetween); +} + + +/** @title prove that all functions of the PositionStatusMap.sol should never revert. +**/ +rule neverReverts(method f) { + env e; + calldataarg args; + require e.msg.value == 0; + f@withrevert(e, args); + assert !lastReverted; +} + + + diff --git a/certora/spec/libs/Premium.spec b/certora/spec/libs/Premium.spec new file mode 100644 index 000000000..8b27f7dc2 --- /dev/null +++ b/certora/spec/libs/Premium.spec @@ -0,0 +1,40 @@ +/** +@title Prove the summarization of Premium.calculatePremiumRay + +Verify that the CVL representation (calculatePremiumRayCVL) matches the Solidity implementation. + +To run this spec file: + certoraRun certora/conf/libs/Premium.conf + +**/ + +methods { + function calculatePremiumRay(uint256 premiumShares, int256 premiumOffsetRay, uint256 drawnIndex) external returns (uint256) envfree; +} + + +/** +@title CVL implementation of calculatePremiumRay +This is the summarization used in HubBase.spec +*/ +function calculatePremiumRayCVL(uint256 premiumShares, int256 premiumOffsetRay, uint256 drawnIndex) returns uint256 { + return require_uint256((premiumShares * drawnIndex) - premiumOffsetRay); +} + + +/** +@title Prove that calculatePremiumRayCVL matches the Solidity implementation + +The Solidity implementation: + return ((premiumShares * drawnIndex).toInt256() - premiumOffsetRay).toUint256(); + +The CVL implementation: + return require_uint256((premiumShares * drawnIndex) - premiumOffsetRay); +*/ +rule calculatePremiumRay_equivalence(uint256 premiumShares, int256 premiumOffsetRay, uint256 drawnIndex) { + uint256 solidityResult = calculatePremiumRay(premiumShares, premiumOffsetRay, drawnIndex); + + uint256 cvlResult = calculatePremiumRayCVL(premiumShares, premiumOffsetRay, drawnIndex); + assert solidityResult == cvlResult, "Results must be equal when not reverting"; +} + diff --git a/certora/spec/libs/SharesMath.spec b/certora/spec/libs/SharesMath.spec new file mode 100644 index 000000000..0652cea29 --- /dev/null +++ b/certora/spec/libs/SharesMath.spec @@ -0,0 +1,147 @@ +/** +@title Prove mathematical properties of SharesMath.sol library +The rules proven here are used for summarizing additional functions + +**/ + +import "../HubBase.spec"; + +methods { + // envfree functions + function toSharesDown(uint256 assets, uint256 totalAssets, uint256 totalShares) external returns (uint256) envfree ; + function toAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) external returns (uint256) envfree ; + + function toSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) external returns (uint256) envfree ; + function toAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) external returns (uint256) envfree ; + +} + +/** +@title Monotonicity of toSharesUp +x > y => toSharesUp(x) >= toSharesUp(y) +**/ +rule toSharesUp_monotonicity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + assert x < y => + toSharesUp(x, totalAssets, totalShares) <= toSharesUp(y, totalAssets, totalShares); +} + +/** +@title Additivity of toSharesUp +While taking into account changes to totalSupply and totalAssets +toSharesUp(x) + toSharesUp(y) >= toSharesUp(x+y) +**/ +rule toSharesUp_additivity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + require totalAssets == 0 <=> totalShares == 0; //todo : verify this + require totalAssets >= x + y; + + + uint256 sharesForX = toSharesUp(x, totalAssets, totalShares); + + uint256 sharesForYAfterX = toSharesUp(y, require_uint256(totalAssets - x), + require_uint256(totalShares - sharesForX)); + + uint256 sharesForXplusY = toSharesUp(require_uint256(x + y), totalAssets, totalShares); + assert sharesForXplusY <= (sharesForX + sharesForYAfterX); + satisfy sharesForXplusY == (sharesForX + sharesForYAfterX); + satisfy sharesForXplusY < (sharesForX + sharesForYAfterX); +} + +/** +@title toSharesUp non zero +toSharesUp(x) == 0 <=> x == 0 +**/ +rule toSharesUp_nonZero(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + + uint256 sharesForX = toSharesUp(x, totalAssets, totalShares); + assert sharesForX == 0 <=> x ==0; + satisfy x == 0; + satisfy x != 0; +} + +/** +@title Monotonicity of toAssetsUp +x > y => toAssetsUp(x) >= toAssetsUp(y) +**/ +rule toAssetsUp_monotonicity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + assert x < y => + toAssetsUp(x, totalAssets, totalShares) <= toAssetsUp(y, totalAssets, totalShares); +} + +/** +@title Additivity of toAssetsUp +While taking into account changes to totalSupply and totalAssets +toAssetsUp(x) + toAssetsUp(y) >= toAssetsUp(x+y) +**/ +rule toAssetsUp_additivity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + + uint256 assetsForX = toAssetsUp(x, totalAssets, totalShares); + uint256 assetsForYAfterX = toAssetsUp(y, require_uint256(totalAssets + assetsForX), require_uint256(totalShares + x)); + + uint256 assetsForXplusY = toAssetsUp(require_uint256(x + y), totalAssets, totalShares); + assert assetsForXplusY <= assetsForX + assetsForYAfterX; +} + +/** +@title Monotonicity of toSharesDown +x > y => toSharesDown(x) >= toSharesDown(y) +**/ +rule toSharesDown_monotonicity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + assert x < y => + toSharesDown(x, totalAssets, totalShares) <= toSharesDown(y, totalAssets, totalShares); +} + +/** +@title Additivity of toSharesDown +While taking into account changes to totalSupply and totalAssets +toSharesDown(x) + toSharesDown(y) <= toSharesDown(x+y) +**/ +rule toSharesDown_additivity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + + uint256 sharesForX = toSharesDown(x, totalAssets, totalShares); + uint256 sharesForYAfterX = toSharesDown(y, require_uint256(totalAssets + x), require_uint256(totalShares + sharesForX)); + + uint256 sharesForXplusY = toSharesDown(require_uint256(x + y), totalAssets, totalShares); + assert sharesForXplusY >= sharesForX + sharesForYAfterX; +} + +/** +@title Monotonicity of toAssetsDown +x > y => toAssetsDown(x) >= toAssetsDown(y) +**/ +rule toAssetsDown_monotonicity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + assert x < y => + toAssetsDown(x, totalAssets, totalShares) <= toAssetsDown(y, totalAssets, totalShares); +} + +/** +@title Additivity of toAssetsDown +While taking into account changes to totalSupply and totalAssets +toAssetsDown(x) + toAssetsDown(y) <= toAssetsDown(x+y) +**/ +rule toAssetsDown_additivity(uint256 assetId, uint256 x, uint256 y){ + uint256 totalAssets; uint256 totalShares; + require totalAssets >= totalShares; + require totalAssets == 0 <=> totalShares == 0; //todo : verify this + + uint256 assetsForX = toAssetsDown(x, totalAssets, totalShares); + uint256 assetsForYAfterX = toAssetsDown(y, require_uint256(totalAssets + assetsForX), require_uint256(totalShares + x)); + + uint256 assetsForXplusY = toAssetsDown(require_uint256(x + y), totalAssets, totalShares); + assert assetsForXplusY >= assetsForX + assetsForYAfterX; +} diff --git a/certora/spec/liquidation.spec b/certora/spec/liquidation.spec new file mode 100644 index 000000000..38eb79f79 --- /dev/null +++ b/certora/spec/liquidation.spec @@ -0,0 +1 @@ +suppliedCollateralCount > 1 => no defecit ( no collateral and debt) \ No newline at end of file diff --git a/certora/spec/symbolicRepresentation/ERC20s_CVL.spec b/certora/spec/symbolicRepresentation/ERC20s_CVL.spec new file mode 100644 index 000000000..9d7471826 --- /dev/null +++ b/certora/spec/symbolicRepresentation/ERC20s_CVL.spec @@ -0,0 +1,100 @@ + +/** +@title This file represents multiple erc20 tokens. +The functionality it summarize: +- balanceOf +- transfer +- transferFrom + +it simulates the behavior of erc20 tokens including reverting/returning false cases. +**/ +methods { + function _.transfer(address to, uint256 amount) external with (env e) + => transferCVL(calledContract, e.msg.sender, to, amount) expect bool; + function _.transferFrom(address from, address to, uint256 amount) external with (env e) + => transferFromCVL(calledContract, e.msg.sender, from, to, amount) expect bool; + + function _.safeTransfer(address token, address to, uint256 amount) internal with (env e) + => safeTransferCVL(token, executingContract, to, amount) expect bool; + function _.safeTransferFrom(address token, address from, address to, uint256 amount) internal with (env e) + => safeTransferFromCVL(token, executingContract, from, to, amount) expect bool; + function _.balanceOf(address account) external => + tokenBalanceOf(calledContract, account) expect uint256; + function _.balanceOf(address token, address account) internal => balanceByToken[token][account] expect uint256; + + function _.permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external => NONDET ALL; + +} + + + +/// CVL simple implementations of IERC20: +/// token => account => balance +ghost mapping(address => mapping(address => uint256)) balanceByToken; +/// token => owner => spender => allowance +ghost mapping(address => mapping(address => mapping(address => uint256))) allowanceByToken; + + +function tokenBalanceOf(address token, address account) returns uint256 { + return balanceByToken[token][account]; +} + + +function revertOn(bool b) { + if(b) { + revert(); + } +} + +function transferFromCVL(address token, address spender, address from, address to, uint256 amount) returns bool { + revertOn(allowanceByToken[token][from][spender] < amount); + bool success = transferCVL(token, from, to, amount); + if(success) { + allowanceByToken[token][from][spender] = assert_uint256(allowanceByToken[token][from][spender] - amount); + } + return success; +} + +ghost bool revertOrReturnFalse; +function transferCVL(address token, address from, address to, uint256 amount) returns bool { + revertOn(token == 0); + + if (balanceByToken[token][from] < amount) { + if(revertOrReturnFalse) { + revert(); + } + else { + return false; + } + } + balanceByToken[token][from] = assert_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); // We neglect overflows. + return true; +} + +function safeTransferCVL(address token, address from, address to, uint256 amount) returns bool { + if (balanceByToken[token][from] < amount) { + revert(); + } + balanceByToken[token][from] = require_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); // We neglect overflows. + + return true; +} + +function safeTransferFromCVL(address token, address spender, address from, address to, uint256 amount) returns bool { + bool success = safeTransferCVL(token, from, to, amount); + if (allowanceByToken[token][from][spender] < amount){ + revert(); + } + allowanceByToken[token][from][spender] = require_uint256(allowanceByToken[token][from][spender] - amount); + return true; +} \ No newline at end of file diff --git a/certora/spec/symbolicRepresentation/Math_CVL.spec b/certora/spec/symbolicRepresentation/Math_CVL.spec new file mode 100644 index 000000000..741d303cb --- /dev/null +++ b/certora/spec/symbolicRepresentation/Math_CVL.spec @@ -0,0 +1,82 @@ + +/* + Returns floor(x * y / z) + Reverts when z==0 or x*y overflows +*/ +function mulDivDownCVL(uint256 x, uint256 y, uint256 z) returns uint256 { + mathint mul = x * y; + if (z == 0 || mul > max_uint256) { + revert(); + } + mathint res = (mul / z); + return require_uint256(res); +} + +/* + Returns ceil(x * y / z) + Reverts when z==0 or x*y or (x*y + z-1) overflows +*/ + +function mulDivUpCVL(uint256 x, uint256 y, uint256 z) returns uint256 { + mathint mul = x * y; + if (z == 0 || mul > max_uint256) { + revert(); + } + mathint res = ((mul + z - 1) / z); + if (res > max_uint256) + revert(); + return require_uint256(res); +} + + +/* + Returns floor(x * y / z) + Reverts when z==0 or x*y overflows +*/ +function mulDivRayDownCVL(uint256 x, uint256 y) returns uint256 { + mathint mul = x * y; + if ( mul > max_uint256) { + revert(); + } + mathint res = (mul / (10 ^ 27)); + return require_uint256(res); +} + +/* + Returns ceil(x * y / z) + Reverts when z==0 or x*y or (x*y + z-1) overflows +*/ + +function mulDivRayUpCVL(uint256 x, uint256 y) returns uint256 { + mathint mul = x * y; + if ( mul > max_uint256) { + revert(); + } + mathint res = ((mul + (10 ^ 27) - 1) / (10 ^ 27)); + if (res > max_uint256) + revert(); + return require_uint256(res); +} + + +/* + returns ceil(x / RAY). +*/ + +function divRayUpCVL(uint256 x) returns uint256 { + mathint res = ((x + (10 ^ 27) - 1) / (10 ^ 27)); + if (res > max_uint256) + revert(); + return require_uint256(res); +} + +/* + returns x * RAY. +*/ +function mulRayCVL(uint256 x) returns uint256 { + mathint res = x * (10 ^ 27); + if (res > max_uint256) + revert(); + return require_uint256(res); +} + diff --git a/certora/spec/symbolicRepresentation/SymbolicHub.spec b/certora/spec/symbolicRepresentation/SymbolicHub.spec new file mode 100644 index 000000000..22ab93b27 --- /dev/null +++ b/certora/spec/symbolicRepresentation/SymbolicHub.spec @@ -0,0 +1,134 @@ + +methods { + function _.previewRemoveByShares(uint256 assetId, uint256 shares) external with (env e) => previewRemoveBySharesCVL(assetId, shares, e) expect uint256; + + function _.previewAddByAssets(uint256 assetId, uint256 assets) external with (env e) => previewAddByAssetsCVL(assetId, assets, e) expect uint256; + + function _.previewRemoveByAssets(uint256 assetId, uint256 assets) external with (env e) => previewRemoveByAssetsCVL(assetId, assets, e) expect uint256; + + function _.previewDrawByShares(uint256 assetId, uint256 shares) external with (env e) => previewDrawBySharesCVL(assetId, shares, e) expect uint256; + + function _.previewRestoreByShares(uint256 assetId, uint256 shares) external with (env e) => previewRestoreBySharesCVL(assetId, shares, e) expect uint256; + + function _.getAssetDrawnIndex(uint256 assetId) external with (env e) => getAssetDrawnIndexCVL(assetId, e) expect uint256; + + +// Supply Operations + function _.add(uint256 assetId, uint256 amount) external with (env e) => addSummaryCVL(assetId, amount, e) expect uint256; +// Withdraw Operations + function _.remove(uint256 assetId, uint256 amount, address to) external with (env e) => removeSummaryCVL(assetId, amount, to, e) expect uint256; +// Borrow Operations + function _.draw(uint256 assetId, uint256 amount, address to) external with (env e) => drawSummaryCVL(assetId, amount, to, e) expect uint256; +// Repay Operations + function _.restore(uint256 assetId, uint256 drawnAmount, IHubBase.PremiumDelta premiumDelta) external with (env e) => restoreSummaryCVL(assetId, drawnAmount, premiumDelta, e) expect uint256; +// Report Deficit Operations + function _.reportDeficit(uint256 assetId, uint256 drawnAmount, IHubBase.PremiumDelta premiumDelta) external with (env e) => previewRestoreByAssetsCVL(assetId, drawnAmount, e) expect uint256; +// Eliminate Deficit Operations + function _.eliminateDeficit(uint256 assetId, uint256 amount, address spokeAddress) external with (env e) => previewRemoveByAssetsCVL(assetId, amount, e) expect uint256; +//refresh premium + function _.refreshPremium(uint256 assetId, IHubBase.PremiumDelta premiumDelta) external => HAVOC_ECF; + +// Pay Fee Shares Operations + function _.payFeeShares(uint256 assetId, uint256 shares) external => NONDET; + + function _.getAssetUnderlyingAndDecimals(uint256 assetId) external => getAssetUnderlyingAndDecimalsCVL(assetId) expect (address, uint8); + +} + + +// symbolic debt index: for each assetId and block timestamp there is an index +// the index is monotonic increasing +persistent ghost mapping(uint256 /*assetId */ => mapping(uint256 /* blockTimestamp */ => uint256)) indexOfAssetPerBlock { + axiom forall uint256 assetId. forall uint256 blockTimestamp. forall uint256 blockTimestamp2. + blockTimestamp < blockTimestamp2 => indexOfAssetPerBlock[assetId][blockTimestamp] <= indexOfAssetPerBlock[assetId][blockTimestamp2]; + axiom forall uint256 assetId. forall uint256 blockTimestamp. indexOfAssetPerBlock[assetId][blockTimestamp] >= RAY; +} + +// symbolic assets to share ratio: +persistent ghost mapping(uint256 /*assetId */ => mapping(uint256 /*blockTimestamp*/ => uint256)) shareToAssetsRatio { + axiom forall uint256 assetId. forall uint256 blockTimestamp. forall uint256 blockTimestamp2. + blockTimestamp < blockTimestamp2 => shareToAssetsRatio[assetId][blockTimestamp] <= shareToAssetsRatio[assetId][blockTimestamp2]; + // at least RAY assets per share + axiom forall uint256 assetId. forall uint256 blockTimestamp. shareToAssetsRatio[assetId][blockTimestamp] >= RAY; +} + +// toAddedSharesDown : assets.toSharesDown(asset.totalAddedAssets(), asset.totalAddedShares()); +function previewAddByAssetsCVL(uint256 assetId, uint256 assets, env e) returns (uint256) { + uint256 ratio = shareToAssetsRatio[assetId][e.block.timestamp]; + return require_uint256(((assets * RAY) + ratio -1) / ratio); +} + +// toAddedAssetsDown : shares.toAssetsDown(asset.totalAddedAssets(), asset.totalAddedShares()); +function previewRemoveBySharesCVL(uint256 assetId, uint256 shares, env e) returns (uint256) { + uint256 ratio = shareToAssetsRatio[assetId][e.block.timestamp]; + return require_uint256(shares * ratio / RAY); +} + +// toAddedSharesUp :assets.toSharesUp(asset.totalAddedAssets(), asset.totalAddedShares()); +function previewRemoveByAssetsCVL(uint256 assetId, uint256 assets, env e) returns (uint256) { + uint256 ratio = shareToAssetsRatio[assetId][e.block.timestamp]; + return require_uint256(((assets * RAY) + ratio -1) / ratio); +} + +// toDrawnAssetsDown : shares.rayMulDown(asset.getDrawnIndex()) +function previewDrawBySharesCVL(uint256 assetId, uint256 shares, env e) returns (uint256) { + uint256 ratio = indexOfAssetPerBlock[assetId][e.block.timestamp]; + return require_uint256((shares * ratio) / RAY); +} + +// toDrawnSharesUp : assets.rayDivUp(asset.getDrawnIndex()) +function previewDrawByAssetsCVL(uint256 assetId, uint256 assets, env e) returns (uint256) { + uint256 ratio = indexOfAssetPerBlock[assetId][e.block.timestamp]; + return require_uint256(((assets * RAY) + ratio -1) / ratio); + +} +// toDrawnAssetsUp : shares.rayMulUp(asset.getDrawnIndex()); +function previewRestoreBySharesCVL(uint256 assetId, uint256 shares, env e) returns (uint256) { + uint256 ratio = indexOfAssetPerBlock[assetId][e.block.timestamp]; + return require_uint256(((shares * ratio) + RAY - 1) / RAY); +} + +// toDrawnSharesDown : assets.rayDivDown(asset.getDrawnIndex()); +function previewRestoreByAssetsCVL(uint256 assetId, uint256 assets, env e) returns (uint256) { + uint256 ratio = indexOfAssetPerBlock[assetId][e.block.timestamp]; + return require_uint256(((assets * RAY) + ratio -1) / ratio); +} + +// getAssetDrawnIndex: returns the drawn index for an asset at a given block timestamp +function getAssetDrawnIndexCVL(uint256 assetId, env e) returns (uint256) { + return indexOfAssetPerBlock[assetId][e.block.timestamp]; +} + +// CVL function summarizations for Hub operations with zero amount checks +function addSummaryCVL(uint256 assetId, uint256 amount, env e) returns (uint256) { + require amount > 0; + // Return computed shares based on amount and asset using existing preview function + return previewAddByAssetsCVL(assetId, amount, e); +} + +function removeSummaryCVL(uint256 assetId, uint256 amount, address to, env e) returns (uint256) { + require amount > 0; + // Return computed shares based on amount and asset using existing preview function + return previewRemoveByAssetsCVL(assetId, amount, e); +} + +function drawSummaryCVL(uint256 assetId, uint256 amount, address to, env e) returns (uint256) { + require amount > 0; + // Return computed drawn shares based on amount and asset using existing preview function + return previewDrawByAssetsCVL(assetId, amount, e); +} + +function restoreSummaryCVL(uint256 assetId, uint256 drawnAmount, IHubBase.PremiumDelta premiumDelta, env e) returns (uint256) { + require drawnAmount > 0 ; + // Return computed restored shares based on drawn amount using existing preview function + return previewRestoreByAssetsCVL(assetId, drawnAmount, e); +} + + +ghost mapping(uint256 /*assetId*/ => address /*underlying*/) assetUnderlying; + +ghost mapping(uint256 /*assetId*/ => uint8 /*decimals*/) assetDecimals; + +function getAssetUnderlyingAndDecimalsCVL(uint256 assetId) returns (address, uint8) { + return (assetUnderlying[assetId], assetDecimals[assetId]); +} diff --git a/certora/spec/symbolicRepresentation/SymbolicPositionStatus.spec b/certora/spec/symbolicRepresentation/SymbolicPositionStatus.spec new file mode 100644 index 000000000..8b67a5015 --- /dev/null +++ b/certora/spec/symbolicRepresentation/SymbolicPositionStatus.spec @@ -0,0 +1,137 @@ +/** +Symbolic representation of the PositionStatusMap.sol library. +The summarization of the PositionStatus.spec library is verified to obtain the rules of the PositionStatusMap.sol library. + +This summary is used in the Spoke.spec file. + +To run this spec file: + certoraRun certora/conf/VerifySymbolicPositionStatus.conf + + +**/ + +methods { + function _.setBorrowing(ISpoke.PositionStatus storage positionStatus, uint256 reserveId, bool borrowing) internal => setBorrowingCVL(reserveId, borrowing) expect void; + + function _.setUsingAsCollateral(ISpoke.PositionStatus storage positionStatus, uint256 reserveId, bool usingAsCollateral) internal => setUsingAsCollateralCVL(reserveId, usingAsCollateral) expect void; + + function _.isUsingAsCollateralOrBorrowing(ISpoke.PositionStatus storage positionStatus, uint256 reserveId) internal => isUsingAsCollateralOrBorrowingCVL(reserveId) expect bool; + + function _.isBorrowing(ISpoke.PositionStatus storage positionStatus, uint256 reserveId) internal => isBorrowingCVL(reserveId) expect bool; + + function _.isUsingAsCollateral(ISpoke.PositionStatus storage positionStatus, uint256 reserveId) internal => isUsingAsCollateralCVL(reserveId) expect bool; + + function _.collateralCount(ISpoke.PositionStatus storage positionStatus, uint256 reserveCount) internal => collateralCountCVL(reserveCount) expect uint256; + + function _.next(ISpoke.PositionStatus storage positionStatus, uint256 startReserveId) internal => nextCVL(startReserveId) expect (uint256, bool, bool); + + function _.nextBorrowing(ISpoke.PositionStatus storage positionStatus, uint256 startReserveId) internal => nextBorrowingCVL(startReserveId) expect uint256; + + function _.nextCollateral(ISpoke.PositionStatus storage positionStatus, uint256 startReserveId) internal => nextCollateralCVL(startReserveId) expect uint256; +} + +///@dev the user which is updated +// it is safe to assume that there is only one user involved in each function call +// see SpokeUserIntegrity.spec rule userIntegrity +persistent ghost address userGhost; + +///@dev ghost mapping of the borrowing flags for the user +persistent ghost mapping(address /*user */ => mapping(uint256 /*reserveId*/ => bool /*borrowing*/)) isBorrowing { + init_state axiom forall address user. forall uint256 reserveId. !isBorrowing[user][reserveId]; + +} + +///@dev ghost mapping of the using as collateral flags for the user +persistent ghost mapping(address /*user */ => mapping(uint256 /*reserveId*/ => bool /*usingAsCollateral*/)) isUsingAsCollateral { + init_state axiom forall address user. forall uint256 reserveId. !isUsingAsCollateral[user][reserveId]; +} + + + +persistent ghost uint256 reserveCountGhost { + init_state axiom reserveCountGhost == 0; +} + + +function setBorrowingCVL(uint256 reserveId, bool borrowing) { + if (borrowing != isBorrowing[userGhost][reserveId]) { + reserveCountGhost = require_uint256(borrowing ? reserveCountGhost + 1 : reserveCountGhost - 1); + + } + isBorrowing[userGhost][reserveId] = borrowing; + +} + +function isBorrowingCVL(uint256 reserveId) returns (bool) { + return isBorrowing[userGhost][reserveId]; +} + +function setUsingAsCollateralCVL(uint256 reserveId, bool usingAsCollateral) { + if (usingAsCollateral != isUsingAsCollateral[userGhost][reserveId]) { + reserveCountGhost = require_uint256(usingAsCollateral ? reserveCountGhost + 1 : reserveCountGhost - 1); + } + isUsingAsCollateral[userGhost][reserveId] = usingAsCollateral; + } + + +function isUsingAsCollateralCVL(uint256 reserveId) returns (bool) { + return isUsingAsCollateral[userGhost][reserveId]; +} + +function isUsingAsCollateralOrBorrowingCVL(uint256 reserveId) returns (bool) { + return isUsingAsCollateral[userGhost][reserveId] || isBorrowing[userGhost][reserveId]; +} + + +function nextCVL(uint256 startReserveId) returns (uint256, bool, bool) { + uint256 result; + require (result < startReserveId && result >= startReserveId - 3 ) || result == max_uint256; + require isUsingAsCollateral[userGhost][result] || isBorrowing[userGhost][result] || result == max_uint256; + if (result != max_uint256) { + uint256 between_1 = require_uint256(startReserveId - 1); + require result < between_1 => (!isUsingAsCollateral[userGhost][between_1] && !isBorrowing[userGhost][between_1]); + uint256 between_2 = require_uint256(startReserveId - 2); + require result < between_2 => (!isUsingAsCollateral[userGhost][between_2] && !isBorrowing[userGhost][between_2]); + } else { + require startReserveId <= 3; + int end_0 = 0; + require startReserveId > 0 => (!isUsingAsCollateral[userGhost][0] && !isBorrowing[userGhost][0]); + require startReserveId > 1 => (!isUsingAsCollateral[userGhost][1] && !isBorrowing[userGhost][1]); + require startReserveId > 2 => (!isUsingAsCollateral[userGhost][2] && !isBorrowing[userGhost][2]); + + } + return (result, isBorrowing[userGhost][result], isUsingAsCollateral[userGhost][result]); +} + +function nextBorrowingCVL(uint256 startReserveId) returns (uint256) { + uint256 result; + require result < startReserveId || result == max_uint256; + require isBorrowing[userGhost][result] || result == max_uint256; + require !isBorrowing[userGhost][max_uint256]; + if (result != max_uint256) { + require forall uint256 i. i < startReserveId && i > result => !isBorrowing[userGhost][i]; + } else { + // no more bits are set + require forall uint256 i. i < startReserveId => !isBorrowing[userGhost][i]; + } + return result; +} + +function nextCollateralCVL(uint256 startReserveId) returns (uint256) { + uint256 result; + require result < startReserveId || result == max_uint256; + require isUsingAsCollateral[userGhost][result] || result == max_uint256; + + require !isUsingAsCollateral[userGhost][max_uint256]; + if (result != max_uint256) { + require forall uint256 i. i < startReserveId && i > result => !isUsingAsCollateral[userGhost][i]; + } else { + // no more bits are set + require forall uint256 i. i < startReserveId => !isUsingAsCollateral[userGhost][i]; + } + return result; +} +function collateralCountCVL(uint256 ignore) returns (uint256) { + return reserveCountGhost; +} + diff --git a/certora/spec/symbolicRepresentation/VerifySymbolicPositionStatus.spec b/certora/spec/symbolicRepresentation/VerifySymbolicPositionStatus.spec new file mode 100644 index 000000000..629936eca --- /dev/null +++ b/certora/spec/symbolicRepresentation/VerifySymbolicPositionStatus.spec @@ -0,0 +1,25 @@ +import "./SymbolicPositionStatus.spec"; +import "../libs/PositionStatus.spec"; + +use rule setBorrowing; +use rule setUsingAsCollateral; +use rule isUsingAsCollateralOrBorrowing; +use rule collateralCount; +use rule next; +use rule nextBorrowing; +use rule nextCollateral; + + +/* +methods { + function isBorrowing(uint256 reserveId) external returns (bool) envfree; + function setBorrowing(uint256 reserveId, bool borrowing) external envfree; +} +rule setBorrowing(uint256 reserveId1, bool borrowing) { + uint256 reserveId2; + bool before = isBorrowing(reserveId2); + setBorrowing(reserveId1, borrowing); + bool after = isBorrowing(reserveId2); + assert(reserveId1 != reserveId2 => before == after); + assert(reserveId1 == reserveId2 => borrowing == after); +}*/ \ No newline at end of file From 03ffb150629cd5f5768abf115d0f3bf08ebeeb9b Mon Sep 17 00:00:00 2001 From: DhairyaSethi <55102840+DhairyaSethi@users.noreply.github.com> Date: Thu, 18 Dec 2025 15:55:09 +0530 Subject: [PATCH 2/2] chore: fix lint --- .github/workflows/certora.yml | 2 +- certora/README.md | 50 ++++++++++++++++++++++++++++++----- 2 files changed, 45 insertions(+), 7 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index abbb3bbd2..84100139e 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,7 +37,7 @@ env: #certora/conf/HubAdditivity.conf --rule reportDeficitAdditivity #certora/conf/HubAccrueSupplyRate.conf --rule previewRemoveByShares_withoutAccrue_time_monotonic previewAddByShares_withoutAccrue_time_monotonic #### rules that are failing and waiting for fix - #certora/conf/Spoke.conf --rule increaseCollateralOrReduceDebtFunctions + #certora/conf/Spoke.conf --rule increaseCollateralOrReduceDebtFunctions on: pull_request: diff --git a/certora/README.md b/certora/README.md index 48a119a42..8cdebba07 100644 --- a/certora/README.md +++ b/certora/README.md @@ -26,27 +26,32 @@ certora/ The formal verification focuses on the following critical safety properties: ### Solvency & Share Rate + - **Share Rate Monotonicity** - The exchange rate between shares and assets never decreases, protecting LP token holders - **Total Assets ≥ Total Shares** - Ensures the protocol remains solvent - **External Solvency** - Hub underlying balance always covers total added assets ### Position Safety + - **No Collateral → No Debt** - Users without collateral cannot accumulate debt - **Borrowing Flag Consistency** - Borrowing status accurately reflects drawn shares - **Health Factor Maintenance** - User health stays above liquidation threshold after operations ### State Consistency + - **Spoke Isolation** - Operations on one spoke don't affect other spokes - **Sum Invariants** - Sum of spoke supplies/drawn shares equals totals - **Reserve ID Validity** - Reserve mappings remain consistent ### Accrue Integrity + - **Idempotency** - Calling accrue twice is equivalent to calling once - **Index Monotonicity** - Interest indices only increase ## Prerequisites 1. Install the Certora Prover CLI: + ```bash pip install certora-cli ``` @@ -59,22 +64,27 @@ The formal verification focuses on the following critical safety properties: ## Running the Prover ### Run All Configurations + ```bash ./certora/runAll.sh ``` ### Run a Single Configuration + ```bash certoraRun certora/conf/.conf ``` ### Run a Specific Rule + ```bash certoraRun certora/conf/.conf --rule --msg "" ``` ### Documentation + For more information on the Certora Prover and CVL specification language, see: + - [Certora Documentation](https://docs.certora.com/) - [CVL Language Reference](https://docs.certora.com/en/latest/docs/cvl/index.html) - [Certora Prover CLI](https://docs.certora.com/en/latest/docs/prover/cli/index.html) @@ -84,6 +94,7 @@ For more information on the Certora Prover and CVL specification language, see: ## Hub Specifications ### `HubBase.spec` + **Base definitions for Hub specifications.** - **Imports:** `ERC20s_CVL.spec`, `Math_CVL.spec`, `common.spec` @@ -93,6 +104,7 @@ For more information on the Certora Prover and CVL specification language, see: - `Premium.calculatePremiumRay` → CVL implementation ### `Hub.spec` + **Main Hub verification rules.** - **Config:** `certora/conf/Hub.conf` @@ -105,8 +117,8 @@ For more information on the Certora Prover and CVL specification language, see: - `totalAssetsCompareToSuppliedAmount` - Total assets always >= total shares (solvency) - `accrueWasCalled` - Ensures accrue is called before state-changing operations - ### `HubValidState.spec` + **Hub valid state properties and invariants.** - **Config:** `certora/conf/HubValidState.conf`, `certora/conf/HubValidState_totalAssets.conf` @@ -122,9 +134,10 @@ For more information on the Certora Prover and CVL specification language, see: - `sumOfSpokeSupply` - Sum of all spoke supplies equals total supply - `sumOfSpokeDrawnShares` - Sum of all spoke drawn shares equals total drawn - `premiumOffset_Integrity` - Premium offset tracking consistency -- **Additional Config:** `HubValidState_totalAssets.conf` runs `totalAssetsVsShares` with parallel splitting +- **Additional Config:** `HubValidState_totalAssets.conf` runs `totalAssetsVsShares` with parallel splitting ### `HubIntegrityRules.spec` + **Hub integrity verification rules.** - **Config:** `certora/conf/HubIntegrity.conf` @@ -134,8 +147,8 @@ For more information on the Certora Prover and CVL specification language, see: - `nothingForZero_add` - Add operation increases balances - `nothingForZero_remove` - Remove operation decreases balances - ### `HubAccrueIntegrity.spec` + **Accrue function integrity proofs.** - **Config:** `certora/conf/HubAccrueIntegrity.conf` @@ -147,18 +160,21 @@ For more information on the Certora Prover and CVL specification language, see: - Interest rate calculation rules ### `HubAccrueSupplyRate.spec` + **Supply rate verification.** - **Config:** `certora/conf/HubAccrueSupplyRate.conf` - **Purpose:** Verifies supply rate calculations ### `HubAccrueUnrealizedFee.spec` + **Unrealized fee verification.** - **Config:** `certora/conf/HubAccrueUnrealizedFee.conf` - **Purpose:** Verifies unrealized fee calculations ### `HubAdditivity.spec` + **Additivity properties of Hub operations.** - **Config:** `certora/conf/HubAdditivity.conf` @@ -166,12 +182,12 @@ For more information on the Certora Prover and CVL specification language, see: - **Purpose:** Verifies that splitting operations is less beneficial than single operations - **Key Rules:** Additivity proofs for `add`, `remove`, `draw`, `restore`, `reportDeficit`, `eliminateDeficit` - --- ## Spoke Specifications ### `SpokeBase.spec` + **Base definitions for Spoke specifications.** - **Imports:** `Math_CVL.spec`, `SymbolicPositionStatus.spec`, `ERC20s_CVL.spec` @@ -182,6 +198,7 @@ For more information on the Certora Prover and CVL specification language, see: - Authority checks → NONDET ### `Spoke.spec` + **Main Spoke verification rules.** - **Config:** `certora/conf/Spoke.conf`, `certora/conf/Spoke_noCollateralNoDebt.conf` @@ -202,6 +219,7 @@ For more information on the Certora Prover and CVL specification language, see: - **Additional Config:** `Spoke_noCollateralNoDebt.conf` runs `noCollateralNoDebt` with parallel splitting prover args ### `SpokeHealthCheck.spec` + **Health factor verification.** - **Config:** `certora/conf/SpokeHealthCheck.conf` @@ -211,12 +229,14 @@ For more information on the Certora Prover and CVL specification language, see: - `userHealthStaysAboveThreshold` - Health factor maintained after operations ### `SpokeUserIntegrity.spec` + **User position integrity.** - **Config:** `certora/conf/SpokeUserIntegrity.conf` - **Purpose:** Verifies that only one user's account is updated at a time ### `SpokeHubIntegrity.spec` + **Spoke-Hub integration verification.** - **Config:** `certora/conf/SpokeWithHub.conf` @@ -233,6 +253,7 @@ For more information on the Certora Prover and CVL specification language, see: ## Library Specifications ### `libs/Math.spec` + **Mathematical function verification.** - **Config:** `certora/conf/libs/Math.conf` @@ -245,6 +266,7 @@ For more information on the Certora Prover and CVL specification language, see: - `fromRayUp`, `toRay` ### `libs/SharesMath.spec` + **Shares math library verification.** - **Config:** `certora/conf/libs/SharesMath.conf` @@ -255,16 +277,19 @@ For more information on the Certora Prover and CVL specification language, see: - Inverse relationships ### `libs/LibBit.spec` + **Bit manipulation library verification.** - **Config:** `certora/conf/libs/LibBit.conf` ### `libs/PositionStatus.spec` + **Position status verification.** - **Config:** `certora/conf/libs/PositionStatus.conf` ### `libs/Premium.spec` + **Premium calculation verification.** - **Config:** `certora/conf/libs/Premium.conf` @@ -278,22 +303,26 @@ For more information on the Certora Prover and CVL specification language, see: ## Symbolic Representations ### `symbolicRepresentation/Math_CVL.spec` + **CVL implementations of math functions.** - **Purpose:** Provides CVL equivalents of Solidity math functions for use in summaries - **Functions:** `mulDivDownCVL`, `mulDivUpCVL`, `mulDivRayDownCVL`, `mulDivRayUpCVL`, `divRayUpCVL`, `mulRayCVL` ### `symbolicRepresentation/ERC20s_CVL.spec` + **ERC20 symbolic representations.** - **Purpose:** Symbolic handling of ERC20 token interactions ### `symbolicRepresentation/SymbolicHub.spec` + **Symbolic Hub for Spoke verification.** - **Purpose:** Allows verifying Spoke independently of Hub implementation ### `symbolicRepresentation/SymbolicPositionStatus.spec` + **Symbolic position status handling.** --- @@ -301,6 +330,7 @@ For more information on the Certora Prover and CVL specification language, see: ## Common Specifications ### `common.spec` + **Shared method summaries.** - **Purpose:** Common summaries used in both Hub and Spoke specifications @@ -348,20 +378,27 @@ symbolicRepresentation/ ## Harness Contracts ### `HubHarness.sol` + Exposes internal Hub functions for verification: + - `accrueInterest()` - Exposes `AssetLogic.accrue()` ### `MathWrapper.sol` + Wraps math library functions for direct verification: + - Exposes `WadRayMath` functions: `rayMulDown`, `rayMulUp`, `rayDivDown`, `rayDivUp`, `wadDivDown`, `wadDivUp` - Exposes `MathUtils` functions: `mulDivDown`, `mulDivUp` - Exposes `PercentageMath` functions: `percentMulDown`, `percentMulUp` ### `LibBitHarness.sol` + Wraps LibBit library for verification. ### `PremiumWrapper.sol` + Wraps Premium library for verification: + - Exposes `Premium.calculatePremiumRay()` for CVL equivalence testing --- @@ -371,14 +408,15 @@ Wraps Premium library for verification: 1. **Use Build Cache:** Most conf files have `"build_cache": true` to speed up repeated runs. 2. **Split Long-Running Rules:** Use `--split_rules` for rules that may timeout: + ```bash certoraRun certora/conf/Spoke.conf --split_rules drawnSharesZero noCollateralNoDebt ``` 3. **Run Specific Rules:** Use `--rule` to run individual rules: + ```bash certoraRun certora/conf/Hub.conf --rule totalAssetsCompareToSuppliedAmount --msg "Hub totalAssets" ``` -5. **View Results:** Check the Certora Prover dashboard at https://prover.certora.com - +4. **View Results:** Check the Certora Prover dashboard at https://prover.certora.com