Certora formal verification rules (#1069)

.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 }}

.gitignore

@@ -22,4 +22,5 @@ lcov*
 report/
 
 .DS_Store
-.venv/
+.venv/
+.certora_internal/