certora update

pavelvm5 · pavelvm5 · commit 469318157036 · 2025-06-25T20:48:47.000+05:00
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -0,0 +1,66 @@
+name: certora
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+on:
+  pull_request:
+    branches:
+      - certora
+      - main
+  push:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    if:
+      github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
+      github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.29.3
+          configurations: |-
+            certora/conf/stakeToken/rules.conf
+            certora/conf/stakeToken/invariants.conf
+            certora/conf/rewards/mirrors.conf
+            certora/conf/rewards/invariants.conf --rule distributionEnd_NEQ_0
+            certora/conf/rewards/invariants.conf --rule all_rewars_are_different
+            certora/conf/rewards/invariants.conf --rule same_distributionEnd_values
+            certora/conf/rewards/invariants.conf --rule lastUpdateTimestamp_LEQ_current_time
+            certora/conf/rewards/invariants.conf --rule accrued_is_0_for_non_existing_reward
+            certora/conf/rewards/invariants.conf --rule userIndex_is_0_for_non_existing_reward
+            certora/conf/rewards/invariants.conf --rule distributionEnd_is_0_for_non_existing_reward
+            certora/conf/rewards/invariants.conf --rule rewardIndex_is_0_for_non_existing_reward
+            certora/conf/rewards/invariants.conf --rule userIndex_LEQ_rewardIndex
+            certora/conf/rewards/invariants.conf --rule targetLiquidity_NEQ_0
+            certora/conf/rewards/double_reward.conf
+            certora/conf/rewards/single_reward.conf --exclude_rule bob_cant_DOS_alice_to_claim bob_cant_DOS_alice_to_claim__claimSelectedRewards bob_cant_DOS_alice_to_claim__claimAllRewards bob_cant_affect_the_claimed_amount_of_alice
+            certora/conf/rewards/single_reward-depth0.conf --rule bob_cant_DOS_alice_to_claim
+            certora/conf/rewards/single_reward-depth0.conf --rule bob_cant_DOS_alice_to_claim__claimAllRewards
+            certora/conf/rewards/single_reward-depth0.conf --rule bob_cant_DOS_alice_to_claim__claimSelectedRewards
+            certora/conf/rewards/single_reward-special_config.conf --rule bob_cant_affect_the_claimed_amount_of_alice
+            certora/conf/umbrella/invariants.conf
+            certora/conf/umbrella/Umbrella.conf --rule slashing_cant_DOS_other_functions
+            certora/conf/umbrella/Umbrella.conf --rule slashing_cant_DOS__coverDeficitOffset
+            certora/conf/umbrella/Umbrella.conf --exclude_rule slashing_cant_DOS_other_functions slashing_cant_DOS__coverDeficitOffset
+          solc-versions: 0.8.27
+          comment-fail-only: false
+          solc-remove-version-prefix: "0."
+          job-name: "Certora Prover Run"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          install-java: true
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/certora/conf/rewards/double_reward.conf b/certora/conf/rewards/double_reward.conf
@@ -15,7 +15,7 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/rewards/invariants.conf b/certora/conf/rewards/invariants.conf
@@ -15,16 +15,17 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "3",
     "optimistic_loop": true,
     "optimistic_fallback": true,
     "optimistic_hashing": true,
     "process": "emv",
     "solc": "solc8.27",
     "verify": "RewardsControllerHarness:certora/specs/rewards/invariants.spec",
-   "prover_args": ["-depth 0 -treeViewLiveStats false -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on"],
-    "smt_timeout": "2000",
+"prover_args": ["-depth 0 -treeViewLiveStats false -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on"],
+//  "prover_args": ["-treeViewLiveStats false -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on"],
+    "smt_timeout": "8000",
     "rule_sanity": "basic",
     "multi_assert_check" : true,
     "msg": "Umbrella-Rewards::invariants "
diff --git a/certora/conf/rewards/mirrors.conf b/certora/conf/rewards/mirrors.conf
@@ -15,7 +15,7 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "1",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/rewards/sanity.conf b/certora/conf/rewards/sanity.conf
@@ -16,7 +16,7 @@
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
 //     "coverage_info": "basic",
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/rewards/single_reward-depth0.conf b/certora/conf/rewards/single_reward-depth0.conf
@@ -15,7 +15,7 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/rewards/single_reward-special_config.conf b/certora/conf/rewards/single_reward-special_config.conf
@@ -15,7 +15,7 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "1",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/rewards/single_reward.conf b/certora/conf/rewards/single_reward.conf
@@ -15,7 +15,7 @@
        "solidity-utils=lib/aave-v3-origin/lib/solidity-utils/src",
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/stakeToken/invariants.conf b/certora/conf/stakeToken/invariants.conf
@@ -10,7 +10,7 @@
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
        "aave-v3-origin/=lib/aave-v3-origin/src",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "3",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/stakeToken/rules.conf b/certora/conf/stakeToken/rules.conf
@@ -10,7 +10,7 @@
        "@openzeppelin/contracts/=lib/aave-v3-origin/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
        "aave-v3-origin/=lib/aave-v3-origin/src",
     ],
-    "build_cache": true,
+//    "build_cache": true,
     "loop_iter": "3",
     "optimistic_loop": true,
     "optimistic_fallback": true,
diff --git a/certora/conf/umbrella/Umbrella.conf b/certora/conf/umbrella/Umbrella.conf
@@ -16,10 +16,10 @@
         "aave-v3-origin=lib/aave-v3-origin/src",
     ],
     "auto_dispatcher": true,
-    "build_cache": true,
-    "prover_args":[
-        "-copyLoopUnroll 8",
-    ],
+//    "build_cache": true,
+    "prover_args": ["-copyLoopUnroll 8",
+                   "-solvers [z3:def{randomSeed=110},z3:def{randomSeed=111},z3:def{randomSeed=112},z3:def{randomSeed=113},z3:def{randomSeed=114},z3:def{randomSeed=115},z3:def{randomSeed=116},z3:def{randomSeed=117},z3:def{randomSeed=118},z3:def{randomSeed=119}]"
+                   ],
     "optimistic_loop": true,
     "loop_iter": "2",
     "optimistic_fallback": true,
diff --git a/certora/conf/umbrella/invariants.conf b/certora/conf/umbrella/invariants.conf
@@ -16,7 +16,7 @@
         "aave-v3-origin=lib/aave-v3-origin/src",
     ],
     "auto_dispatcher": true,
-    "build_cache": true,
+//    "build_cache": true,
     "prover_args":[
         "-copyLoopUnroll 8",
     ],
diff --git a/certora/scripts/run-all-rewards-invariants.sh b/certora/scripts/run-all-rewards-invariants.sh
@@ -0,0 +1,55 @@
+#CMN="--compilation_steps_only"
+#CMN="--server staging"
+
+
+
+echo
+echo "1: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule distributionEnd_NEQ_0 \
+           --msg "invariant 1. distributionEnd_NEQ_0"
+
+echo
+echo "2: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule all_rewars_are_different \
+           --msg "invariant 2. all_rewars_are_different"
+
+echo
+echo "3: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule same_distributionEnd_values \
+           --msg "invariant 3. same_distributionEnd_values"
+
+echo
+echo "4: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule lastUpdateTimestamp_LEQ_current_time \
+           --msg "invariant 4. lastUpdateTimestamp_LEQ_current_time"
+
+echo
+echo "5: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule accrued_is_0_for_non_existing_reward \
+           --msg "invariant 5.accrued_is_0_for_non_existing_reward"
+
+echo
+echo "6: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule userIndex_is_0_for_non_existing_reward \
+           --msg "invariant 6.userIndex_is_0_for_non_existing_reward"
+
+echo
+echo "7: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule distributionEnd_is_0_for_non_existing_reward \
+           --msg "invariant 7.distributionEnd_is_0_for_non_existing_reward"
+
+echo
+echo "8: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule rewardIndex_is_0_for_non_existing_reward \
+           --msg "invariant 8.rewardIndex_is_0_for_non_existing_reward"
+
+echo
+echo "9: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule userIndex_LEQ_rewardIndex \
+           --msg "invariant 9.userIndex_LEQ_rewardIndex"
+
+echo
+echo "10: invariants.conf"
+certoraRun $CMN certora/conf/rewards/invariants.conf --rule targetLiquidity_NEQ_0 \
+           --msg "invariant 10.targetLiquidity_NEQ_0"
+
diff --git a/certora/scripts/run-all-rewards.sh b/certora/scripts/run-all-rewards.sh
@@ -7,10 +7,10 @@ echo "1: mirrors.conf"
 certoraRun $CMN  certora/conf/rewards/mirrors.conf \
             --msg "1. rewards/mirrors.conf"
 
-echo
-echo "2: invariants.conf"
-certoraRun $CMN  certora/conf/rewards/invariants.conf \
-            --msg "2. rewards/invariants.conf"
+#echo
+#echo "2: invariants.conf"
+#certoraRun $CMN  certora/conf/rewards/invariants.conf \
+  #          --msg "2. rewards/invariants.conf"
 
 echo
 echo "3: double_reward.conf"
diff --git a/certora/scripts/run-all-umbrella.sh b/certora/scripts/run-all-umbrella.sh
@@ -1,5 +1,4 @@
 #CMN="--compilation_steps_only"
-#CMN="--server staging"
 
 
 echo
@@ -8,9 +7,20 @@ certoraRun $CMN  certora/conf/umbrella/invariants.conf \
            --msg "1. umbrella::invariants.conf"
 
 echo
-echo "2: Umbrella.conf"
+echo "2: Umbrella.conf: slashing_cant_DOS_other_functions"
+certoraRun $CMN  certora/conf/umbrella/Umbrella.conf --rule slashing_cant_DOS_other_functions \
+            --msg "2. umbrella::Umbrella.conf::slashing_cant_DOS_other_functions"
+
+echo
+echo "3: Umbrella.conf: slashing_cant_DOS__coverDeficitOffset"
+certoraRun $CMN  certora/conf/umbrella/Umbrella.conf --rule slashing_cant_DOS__coverDeficitOffset \
+            --msg "3. umbrella::Umbrella.conf::slashing_cant_DOS__coverDeficitOffset"
+
+echo
+echo "4: Umbrella.conf: other rules"
 certoraRun $CMN  certora/conf/umbrella/Umbrella.conf \
-            --msg "2. umbrella::Umbrella.conf"
+           --exclude_rule slashing_cant_DOS_other_functions slashing_cant_DOS__coverDeficitOffset \
+            --msg "4. umbrella::Umbrella.conf: other rules"
 
 
 
