fix: upgrade certora prover version to 7.26.0 (#93)

* fix: upgrade prover version to 7.26.0

* test: Fix test with memory accesses

* fix: Upgrade erc4626 tests dep

* test: fix deployer create prediction, always run in isolate mode (#94)

* fix: fix deployer create prediction, always run in isolate mode

* feat: upd ci

---------

Co-authored-by: Nissan Levi <[email protected]>
Co-authored-by: dhairya <[email protected]>

Author: 3 people

.github/workflows/certora.yml

@@ -4,9 +4,11 @@ on:
   push:
     branches:
       - main
+      - certora
   pull_request:
     branches:
       - main
+      - certora
 
   workflow_dispatch:
 
@@ -15,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
@@ -33,7 +35,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==3.6.8.post3
+        run: pip3 install certora-cli==7.26.0
 
       - name: Install solc
         run: |

.github/workflows/foundry-gas-diff.yml

@@ -17,14 +17,14 @@ jobs:
   compare_gas_reports:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
       - name: Install Foundry
         uses: onbjerg/foundry-toolchain@v1
         with:
-          version: nightly
+          version: stable
 
       # Add any step generating a gas report to a temporary file named gasreport.ansi
       # For example:
@@ -38,7 +38,7 @@ jobs:
           FOUNDRY_FUZZ_SEED: 0x${{ github.event.pull_request.base.sha || github.sha }}
 
       - name: Compare gas reports
-        uses: Rubilmax/foundry-gas-diff@v3.11
+        uses: Rubilmax/foundry-gas-diff@v3.21
         with:
           sortCriteria: avg,max # optionnally sort diff rows by criteria
           sortOrders: desc,asc # and directions
@@ -51,4 +51,4 @@ jobs:
         with:
           # delete the comment in case changes no longer impact gas costs
           delete: ${{ !steps.gas_diff.outputs.markdown }}
-          message: ${{ steps.gas_diff.outputs.markdown }}
+          message: ${{ steps.gas_diff.outputs.markdown }}

.github/workflows/tests.yml

@@ -6,12 +6,12 @@ jobs:
   tests:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
 
       - name: Install Foundry
         uses: onbjerg/foundry-toolchain@v1
         with:
-          version: nightly
+          version: stable
 
       - name: Install dependencies
         run: forge install
@@ -23,4 +23,4 @@ jobs:
         env: 
           POLYGON_RPC_URL: ${{ secrets.POLYGON_RPC_URL }}
           AVALANCHE_RPC_URL: ${{ secrets.AVALANCHE_RPC_URL }}
-        run: forge test -vv
+        run: forge test -vvv

.gitignore

@@ -6,4 +6,6 @@
 .env
 .DS_Store
 .gas-snapshot
-lcov.info
+lcov.info
+.certora_internal/
+.certora_recent_jobs.json

.gitmodules

@@ -11,9 +11,6 @@
 	path = lib/aave-v3-core
 	url = https://github.com/aave/aave-v3-core
 	branch = v1.17.1
-[submodule "lib/erc4626-tests"]
-	path = lib/erc4626-tests
-	url = https://github.com/a16z/erc4626-tests
 [submodule "lib/aave-v3-periphery"]
 	path = lib/aave-v3-periphery
 	url = https://github.com/aave/aave-v3-periphery
@@ -22,3 +19,6 @@
 	path = lib/openzeppelin-contracts-upgradeable
 	url = https://github.com/openzeppelin/openzeppelin-contracts-upgradeable
 	branch = v4.8.1
+[submodule "lib/erc4626-tests"]
+	path = lib/erc4626-tests
+	url = https://github.com/a16z/erc4626-tests

certora/conf/accrueYieldCheck.conf

@@ -23,20 +23,14 @@
         "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
         "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
     ],
-    "verify": ["ATokenVaultHarness:certora/specs/accrueYieldCheck.spec"],
-    "rule": ["accrueYieldCheck"],
     "optimistic_loop": true,
+    "build_cache": true,
     "process": "emv",
+    "rule": ["accrueYieldCheck"],
     "rule_sanity": "basic",
-    "settings": [
-        "-assumeUnwindCond",
-        "-depth=15",
-        "-mediumTimeout=1000",
-        "-ruleSanityChecks=basic",
-        "-t=2000"
-    ],
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
     "smt_timeout": "2000",
     "solc": "solc8.10",
-    "cloud": "" ,
+    "verify": "ATokenVaultHarness:certora/specs/accrueYieldCheck.spec",
     "msg": "accrueYieldCheck"
 }

certora/conf/changeInContractBalanceShouldCauseAccrual.conf

@@ -17,6 +17,7 @@
         "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
     ],
     "msg": "changeInContractBalanceShouldCauseAccrual",
+    "build_cache": true,
     "optimistic_loop": true,
     "packages": [
         "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
@@ -30,18 +31,8 @@
         "changeInContractBalanceShouldCauseAccrual"
     ],
     "rule_sanity": "basic",
-    "settings": [
-        "-assumeUnwindCond",
-        "-depth=15",
-        "-mediumTimeout=1000",
-        "-rule=changeInContractBalanceShouldCauseAccrual",
-        "-ruleSanityChecks=basic",
-        "-t=2000"
-    ],
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
     "smt_timeout": "2000",
     "solc": "solc8.10",
-    "cloud": "" ,
-    "verify": [
-        "ATokenVaultHarness:certora/specs/changeInContractBalanceShouldCauseAccrual.spec"
-    ]
+    "verify": "ATokenVaultHarness:certora/specs/changeInContractBalanceShouldCauseAccrual.spec"
 }

certora/conf/erc4626-previewOPERATIONS.conf

@@ -24,21 +24,17 @@
     "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
     "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
   ],
+  "build_cache": true,
   "process": "emv",
   "rule": [
-    "previewMint_amount_check","previewDeposit_amount_check","previewWithdraw_amount_check","previewRedeem_amount_check"
-  ],
-  "settings": [
-    "-assumeUnwindCond",
-    "-depth=15",
-    "-mediumTimeout=1000",
-    "-t=2000"
+    "previewDeposit_amount_check",
+    "previewMint_amount_check",
+    "previewWithdraw_amount_check",
+    "previewRedeem_amount_check"
   ],
+  "prover_args": ["-depth 15","-mediumTimeout 1000"],
   "smt_timeout": "2000",
   "solc": "solc8.10",
-  "cloud": "" ,
-  "verify": [
-    "ATokenVaultHarness:certora/specs/erc4626.spec"
-  ],
-  "msg": "previewOPERATION_amount_check"
+  "verify": "ATokenVaultHarness:certora/specs/erc4626.spec",
+  "msg": "ERC4626: previewOPERATION_amount_check"
 }

certora/conf/fees_LEQ_ATokenBal.conf

@@ -23,18 +23,12 @@
         "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
         "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
     ],
-    "cloud": "",
+    "build_cache": true,
     "optimistic_loop": true,
     "process": "emv",
-    "settings": [
-        "-assumeUnwindCond",
-        "-depth=15",
-        "-mediumTimeout=1000",
-        "-t=2000"
-    ],
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
     "smt_timeout": "2000",
     "solc": "solc8.10",
-    "verify": ["ATokenVaultHarness:certora/specs/fees_LEQ_ATokenBal.spec"],
-    "rule": ["getCLMFees_LEQ_ATokenBAL_DM_other","getCLMFees_LEQ_ATokenBAL_RW"],
-    "msg": "getclaimablefees LEQ Atoken.Balanceof[Vault]"
-}
+    "verify": "ATokenVaultHarness:certora/specs/fees_LEQ_ATokenBal.spec",
+    "msg": "getclaimablefees LEQ Atoken.Balanceof[Vault] getCLMFees_LEQ_ATokenBAL_DM_other for DEV - CVL2"
+}

certora/conf/lastVaultBalance_LEQ_ATokenBalThis.conf

@@ -17,6 +17,8 @@
     "SymbolicLendingPoolL1:aToken=AToken",
     "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
   ],
+  "build_cache": true,
+  "optimistic_loop": true,
   "packages": [
     "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
     "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
@@ -25,19 +27,12 @@
     "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
   ],
   "process": "emv",
-  "optimistic_loop": true,
-  "settings": [
-    "-assumeUnwindCond",
-    "-depth=15",
-    "-mediumTimeout=1000",
-    "-rule=lastVaultBalance_LEQ_ATokenBalThis",
-    "-t=2000"
+  "rule": [
+    "lastVaultBalance_LEQ_ATokenBalThis"
   ],
+  "prover_args": ["-depth 15","-mediumTimeout 1000"],
   "smt_timeout": "2000",
   "solc": "solc8.10",
-  "cloud": "" ,
-  "verify": ["ATokenVaultHarness:certora/specs/lastVaultBal_LEQ_ATokenBalThis.spec"],
-  "disableLocalTypeChecking": false,
-  "rule": ["lastVaultBalance_LEQ_ATokenBalThis"],
-  "msg": "_s.lastVaultBalance LEQ AToken.balance[this] accurate assertion"
+  "verify": "ATokenVaultHarness:certora/specs/lastVaultBal_LEQ_ATokenBalThis.spec",
+  "msg": "_s.lastVaultBalance LEQ AToken.balance[this] example for DEV - CVL2",
 }