run certora scripts
This commit is contained in:
19
.github/workflows/formal-verifiation.yml
vendored
19
.github/workflows/formal-verifiation.yml
vendored
@ -17,7 +17,7 @@ jobs:
|
|||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v2
|
- uses: actions/checkout@v2
|
||||||
- id: set-matrix
|
- 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:
|
verify:
|
||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
@ -41,24 +41,11 @@ jobs:
|
|||||||
wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux
|
wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux
|
||||||
sudo mv solc-static-linux /usr/local/bin/solc
|
sudo mv solc-static-linux /usr/local/bin/solc
|
||||||
chmod +x /usr/local/bin/solc
|
chmod +x /usr/local/bin/solc
|
||||||
- name: Verify rule ${{ matrix.params.spec }}
|
- name: Verify rule ${{ matrix.params }}
|
||||||
if: matrix.params.disabled != true
|
|
||||||
run: |
|
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
|
touch certora/applyHarness.patch
|
||||||
make -C certora munged
|
make -C certora munged
|
||||||
|
sh ${{ matrix.params }}
|
||||||
certoraRun ${{ matrix.params.file }} \
|
|
||||||
--verify ${{ matrix.params.name }}:${{ matrix.params.spec }} \
|
|
||||||
--solc solc \
|
|
||||||
--optimistic_loop \
|
|
||||||
--loop_iter 3 \
|
|
||||||
--cloud \
|
|
||||||
${{ matrix.params.args || '' }}
|
|
||||||
env:
|
env:
|
||||||
CERTORAKEY: ${{ secrets.CERTORAKEY }}
|
CERTORAKEY: ${{ secrets.CERTORAKEY }}
|
||||||
strategy:
|
strategy:
|
||||||
|
|||||||
@ -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"
|
|
||||||
}]
|
|
||||||
Reference in New Issue
Block a user