for PR (aave-dao#52)

Author: nisnislevi

.github/workflows/certora.yml

@@ -1,10 +1,15 @@
 name: certora
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
-  push:
+  pull_request:
     branches:
       - main
-  pull_request:
+      - certora
+  push:
     branches:
       - main
 
@@ -13,42 +18,36 @@ on:
 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@v2
+      - uses: actions/checkout@v4
         with:
           submodules: recursive
 
-      - name: Install python
-        uses: actions/setup-python@v2
-        with: { python-version: 3.9 }
-
-      - name: Install java
-        uses: actions/setup-java@v1
-        with: { java-version: "11", java-package: jre }
-
-      - name: Install certora cli
-        run: pip3 install certora-cli==7.6.3
-
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.27/solc-static-linux
-          chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.27
-
-      - name: Verify rule ${{ matrix.rule }}
+      - name: Munged
         run: |
-          cd certora
+          cd certora/
           touch applyHarness.patch
           make munged
-          cd ..
-          certoraRun certora/confs/${{ matrix.rule }}
+
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.31.0
+          configurations: |-
+            certora/confs/rules.conf
+          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:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
-
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - rules.conf
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+

certora/specs/rules.spec

@@ -81,7 +81,8 @@ rule updateCaps_validity(env e) {
   require capsUpdate.length <= 2; // The length of the array is either 1 or 2.
                                   // Accordingly loop_iter==2
   uint i; // this is the entry of the array that we shall look at
-  require i==1 || i==2; 
+  //  require i==1 || i==2; 
+  require i<capsUpdate.length;
 
   require capsUpdate[i].supplyCap != KEEP_CURRENT;
   require capsUpdate[i].borrowCap != KEEP_CURRENT;
@@ -112,7 +113,8 @@ rule updateRates_validity(env e) {
   require ratesUpdate.length <= 2; // The length of the array is either 1 or 2.
                                   // Accordingly loop_iter==2
   uint i; // this is the entry of the array that we shall look at
-  require i==1 || i==2; 
+  //  require i==1 || i==2; 
+  require i<ratesUpdate.length;
 
   require ratesUpdate[i].params.optimalUsageRatio != KEEP_CURRENT;
   require ratesUpdate[i].params.baseVariableBorrowRate != KEEP_CURRENT;
@@ -147,7 +149,8 @@ rule updateCollateralSide_validity(env e) {
   require collateralUpdate.length <= 2; // The length of the array is either 1 or 2.
                                         // Accordingly loop_iter==2
   uint i; // this is the entry of the array that we shall look at
-  require i==1 || i==2; 
+  //  require i==1 || i==2; 
+  require i<collateralUpdate.length;
 
   require collateralUpdate[i].ltv != KEEP_CURRENT;
   require collateralUpdate[i].liqThreshold != KEEP_CURRENT;
@@ -185,7 +188,8 @@ rule updateLstPriceCaps_validity(env e) {
   require priceCapUpdates.length <= 2; // The length of the array is either 1 or 2.
                                        // Accordingly loop_iter==2
   uint i; // this is the entry of the array that we shall look at
-  require i==1 || i==2; 
+  //  require i==1 || i==2; 
+  require i<priceCapUpdates.length;
 
   updateLstPriceCaps(e,priceCapUpdates);
 
@@ -214,7 +218,8 @@ rule updateStablePriceCaps_validity(env e) {
   require priceCapUpdates.length <= 2; // The length of the array is either 1 or 2.
                                        // Accordingly loop_iter==2
   uint i; // this is the entry of the array that we shall look at
-  require i==1 || i==2; 
+  //  require i==1 || i==2; 
+  require i<priceCapUpdates.length;
 
 
   updateStablePriceCaps(e,priceCapUpdates);