diff --git a/.github/workflows/formal-verifiation.yml b/.github/workflows/formal-verifiation.yml index 1bc886ba4..d28a102df 100644 --- a/.github/workflows/formal-verifiation.yml +++ b/.github/workflows/formal-verifiation.yml @@ -17,7 +17,7 @@ jobs: steps: - uses: actions/checkout@v2 - id: set-matrix - run: echo ::set-output name=matrix::$(cat certora/matrix.json) + run: echo ::set-output name=matrix::$(ls certora/scripts/**/*.sh | jq -Rsc 'split("\n")[:-1]') verify: runs-on: ubuntu-latest @@ -41,24 +41,11 @@ jobs: wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux sudo mv solc-static-linux /usr/local/bin/solc chmod +x /usr/local/bin/solc - - name: Verify rule ${{ matrix.params.spec }} - if: matrix.params.disabled != true + - name: Verify rule ${{ matrix.params }} run: | - echo 'file:' ${{ matrix.params.file }} - echo 'name:' ${{ matrix.params.name }} - echo 'spec:' ${{ matrix.params.spec }} - echo 'args:' ${{ matrix.params.args || '' }} - touch certora/applyHarness.patch make -C certora munged - - certoraRun ${{ matrix.params.file }} \ - --verify ${{ matrix.params.name }}:${{ matrix.params.spec }} \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --cloud \ - ${{ matrix.params.args || '' }} + sh ${{ matrix.params }} env: CERTORAKEY: ${{ secrets.CERTORAKEY }} strategy: diff --git a/certora/matrix.json b/certora/matrix.json deleted file mode 100644 index 2a537f529..000000000 --- a/certora/matrix.json +++ /dev/null @@ -1,29 +0,0 @@ -[{ - "file": "certora/harnesses/ERC1155/ERC1155Harness.sol", - "name": "ERC1155Harness", - "spec": "certora/specs/ERC1155.spec" -},{ - "file": "certora/harnesses/ERC1155/ERC1155BurnableHarness.sol", - "name": "ERC1155BurnableHarness", - "spec": "certora/specs/ERC1155Burnable.spec" -},{ - "file": "certora/harnesses/ERC1155/ERC1155PausableHarness.sol", - "name": "ERC1155PausableHarness", - "spec": "certora/specs/ERC1155Pausable.spec" -},{ - "file": "certora/harnesses/ERC1155/ERC1155SupplyHarness.sol", - "name": "ERC1155SupplyHarness", - "spec": "certora/specs/ERC1155Supply.spec" -},{ - "disabled": true, - "file": "certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol", - "name": "GovernorPreventLateQuorumHarness", - "spec": "certora/specs/GovernorPreventLateQuorum.spec", - "args": "--rule_sanity advanced" -},{ - "disabled": true, - "file": "certora/harnesses/InitializableComplexHarness.sol", - "name": "InitializableComplexHarness", - "spec": "certora/specs/Initializable.spec", - "args": "--rule_sanity advanced" -}]