Exemplary ERC4626 specs

.github/workflows/certora.yml

@@ -0,0 +1,107 @@
+# A workflow file for running Certora verification through github actions.
+# Find results for each push in the "Actions" tab on the github website.
+name: Certora verification
+
+on:
+  push: {}
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      # check out the current version
+      - uses: actions/checkout@v2
+
+      # install Certora dependencies and CLI
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+         # cache: 'pip'
+      - name: Install certora
+        run: pip3 install certora-cli
+
+      # the following is only necessary if your project depends on contracts
+      # installed using yarn
+      # - name: Install yarn
+      #   uses: actions/setup-node@v3
+      #   with:
+      #     node-version: 16
+      #     cache: 'yarn'
+      # - name: Install dependencies
+      #   run: yarn
+
+      # Install the appropriate version of solc
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.0/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.0
+          chmod +x /usr/local/bin/solc8.0
+
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.20
+          chmod +x /usr/local/bin/solc8.20
+
+      # Do the actual verification.  The `run` field could be simply
+      #
+      #   certoraRun certora/conf/${{ matrix.params }}
+      # 
+      # but we do a little extra work to get the commit messages into the
+      # `--msg` argument to `certoraRun`
+      #
+      # Here ${{ matrix.params }} gets replaced with each of the parameters
+      # listed in the `params` section below.
+      - name: Verify rule ${{ matrix.params.name }}
+        run: >
+          message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')";
+          cd lesson4_reading/erc4626/ && certoraRun \
+            ${{ matrix.params.command }} \
+            --msg "$(echo $message | sed 's/[^a-zA-Z0-9., _-]/ /g')"
+        env:
+          # For this to work, you must set your CERTORAKEY secret on the github
+          # website (settings > secrets > actions > new repository secret)
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+      # The following two steps save the output json as a github artifact.
+      # This can be useful for automation that collects the output.
+      - name: Download output json
+        if: always()
+        run: >
+          outputLink=$(sed 's/zipOutput/output/g' .zip-output-url.txt | sed 's/?/\/output.json?/g');
+          curl -L -b "certoraKey=$CERTORAKEY;" ${outputLink} --output output.json || true;
+          touch output.json;
+
+      - name: Archive output json
+        if: always()
+        uses: actions/upload-artifact@v3
+        with:
+          name: output for ${{ matrix.params.name }}
+          path: output.json
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params:
+          # each of these commands is passed to the "Verify rule" step above,
+          # which runs certoraRun on certora/conf/<contents of the command>
+          #
+          # Note that each of these lines will appear as a separate run on
+          # prover.certora.com
+          #
+          # It is often helpful to split up by rule or even by method for a
+          # parametric rule, although it is certainly possible to run everything
+          # at once by not passing the `--rule` or `--method` options
+          #- {name: transferSpec,                 command: 'ERC20.conf --rule transferSpec'}
+          #- {name: generalRulesOnERC20, command: 'generalRules_ERC20.conf --debug'}
+          #- {name: generalRulesOnVAULT, command: 'generalRules_VAULT.conf --debug'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-FunctionalAccountingProps.conf'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-MonotonicityInvariant.conf'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-MustNotRevertProps.conf'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-RedeemUsingApprovalProps.conf'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-RoundingProps.conf'}
+          - {name: RulesForERC4626, command: 'src/certora/conf/certoraRun-SecurityProps.conf'}
+
+

.gitignore

@@ -11,3 +11,5 @@
 # vim
 .*.swp
 .*.swo
+
+emv-*

lesson4_reading/erc4626/doIt.sh

@@ -0,0 +1,10 @@
+echo -e  "\n\n\n########### New execution ##########\n\n\n" >> results.out
+echo -e  "\n\n\n########### Started on $(date)  ##########\n\n\n" >> results.out
+git rev-parse HEAD >> results.out
+git status --short >> results.out
+for file in ./src/certora/conf-openzeppelin/*.conf
+do
+  echo -e  "\n\n\n" >> results.out
+  echo -e  "Results for $file can be found at:" >> results.out
+  certoraRun "$file" >> results.out
+done

lesson4_reading/erc4626/gitCertoraRun.sh

@@ -0,0 +1,13 @@
+certoraOutput=$(certoraRun "$@")
+
+echo "$certoraOutput"
+
+if [[ ${certoraOutput} != *"ERROR"* ]];then
+
+  certoraURL=$(echo $certoraOutput | sed -n 's/.*\(https:\/\/prover.certora.com\/output\/\)/\1/p')
+
+  git add -A
+
+  git commit -m "Results for run: $certoraURL with arguments $@"
+  echo $certoraURL
+fi