certora setup #1
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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 | |
| ln -s /usr/local/bin/solc8.0 /usr/local/bin/solc | |
| wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux | |
| sudo mv solc-static-linux /usr/local/bin/solc8.17 | |
| chmod +x /usr/local/bin/solc8.17 | |
| # 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 ${{ matrix.params.name }} | |
| run: > | |
| message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')"; | |
| certoraRun \ | |
| certora/confs/${{ 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: ghostTemplate, command: 'ghost.conf' } | |
| - {name: ghostWithERC20, command: 'ghosWithERC20s.conf' } | |