Certora #126
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
| # Github action for verifying the contracts under src/contracts/voting | |
| name: certora-review-mainnet | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| jobs: | |
| verify: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v2 | |
| 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.20.3 | |
| - name: Install solc | |
| run: | | |
| wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux | |
| chmod +x solc-static-linux | |
| sudo mv solc-static-linux /usr/local/bin/solc8.19 | |
| - name: Verify rule ${{ matrix.rule }} | |
| run: | | |
| certoraRun --disable_auto_cache_key_gen security/certora/confs/${{ matrix.rule }} | |
| env: | |
| CERTORAKEY: ${{ secrets.CERTORAKEY }} | |
| strategy: | |
| fail-fast: false | |
| max-parallel: 16 | |
| matrix: | |
| rule: | |
| - verifyVotingStrategy_unittests.conf | |
| - verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance | |
| - verifyGovernancePowerStrategy.conf --rule transferPowerCompliance | |
| - verifyGovernancePowerStrategy.conf --rule powerlessCompliance method_reachability | |
| - verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal | |
| - verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal | |
| - verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero | |
| - verifyGovernance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease | |
| - verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives | |
| - verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal | |
| - verifyGovernance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant | |
| - verifyGovernance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period | |
| - verifyGovernance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel | |
| - verifyGovernance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness | |
| - verifyGovernance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal | |
| - verifyGovernance.conf --rule proposal_after_voting_portal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed | |
| - verifyGovernance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence | |
| - verifyGovernance.conf --rule insufficient_proposition_power_witness_time_elapsed | |
| - verifyGovernance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal | |
| - verifyGovernance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash | |
| - verifyGovernance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state | |
| - verifyGovernance.conf --rule only_state_changing_function_initiate_transitions__post_state | |
| - verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_first check_new_representative_set_size_after_updateRepresentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second | |
| - verifyGovernance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state |