Certora Run Github Application

.github/workflows/certora-review-execution-chain.yml

@@ -7,67 +7,47 @@ on:
   pull_request:
     branches:
       - main
-
   workflow_dispatch:
 
 jobs:
   verify:
     runs-on: ubuntu-latest
-
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
         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/payloads/${{ matrix.rule }}
+      - uses: Certora/certora-run-action@v1
+        with:
+          # --disable_auto_cache_key_gen
+          #  security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists
+          configurations: |-
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_maximal_access_level_gt_action_access_level state_cant_decrease no_transition_beyond_state_gt_3 no_transition_beyond_state_variable_gt_3 no_queue_after_expiration empty_actions_if_out_of_bound_payload expirationTime_equal_to_createAt_plus_EXPIRATION_DELAY empty_actions_iff_uninitialized null_access_level_if_out_of_bound_payload null_creator_and_zero_expiration_time_if_out_of_bound_payload empty_actions_only_if_uninitialized_payload executor_access_level_within_range consecutiveIDs empty_actions_if_uninitialized_payload queued_before_expiration_delay payload_grace_period_eq_global_grace_period null_access_level_only_if_out_of_bound_payload null_state_variable_if_out_of_bound_payload created_in_the_past queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_if_action_not_null
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_delay_within_range
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule nonempty_actions
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_iff_action_not_null
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule null_access_level_iff_state_is_none
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_after_createPayload
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule action_callData_immutable
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule action_signature_immutable
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule zero_executedAt_if_not_executed
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executedAt_is_zero_before_executed
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4
+            security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_state_transition_post_state payload_state_transition_pre_state
+          solc-versions: 0.8.19
+          solc-remove-version-prefix: "0."
+          cli-version: 7.20.3
+          job-name: "AAVE Governance V3 Execution Chain"
+          certora-key: ${{ secrets.CERTORAKEY }}
         env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
-
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - verifyPayloadsController.conf --rule payload_maximal_access_level_gt_action_access_level state_cant_decrease no_transition_beyond_state_gt_3 no_transition_beyond_state_variable_gt_3 no_queue_after_expiration empty_actions_if_out_of_bound_payload expirationTime_equal_to_createAt_plus_EXPIRATION_DELAY empty_actions_iff_uninitialized null_access_level_if_out_of_bound_payload null_creator_and_zero_expiration_time_if_out_of_bound_payload empty_actions_only_if_uninitialized_payload executor_access_level_within_range consecutiveIDs empty_actions_if_uninitialized_payload queued_before_expiration_delay payload_grace_period_eq_global_grace_period null_access_level_only_if_out_of_bound_payload null_state_variable_if_out_of_bound_payload created_in_the_past queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability
-        #  - verifyPayloadsController.conf --rule executor_exists
-          - verifyPayloadsController.conf --rule executor_exists_if_action_not_null
-          - verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null
-          - verifyPayloadsController.conf --rule payload_delay_within_range
-          - verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range
-          - verifyPayloadsController.conf --rule nonempty_actions
-          - verifyPayloadsController.conf --rule executor_exists_iff_action_not_null
-          - verifyPayloadsController.conf --rule null_access_level_iff_state_is_none
-          - verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists
-          - verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload
-          - verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload
-          - verifyPayloadsController.conf --rule executor_exists_after_createPayload
-          - verifyPayloadsController.conf --rule action_callData_immutable
-          - verifyPayloadsController.conf --rule action_signature_immutable
-          - verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields
-          - verifyPayloadsController.conf --rule zero_executedAt_if_not_executed
-          - verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero
-          - verifyPayloadsController.conf --rule executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable
-          - verifyPayloadsController.conf --rule queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence
-          - verifyPayloadsController.conf --rule executedAt_is_zero_before_executed
-          - verifyPayloadsController.conf --rule executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease
-          - verifyPayloadsController.conf --rule checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 
-          - verifyPayloadsController.conf --rule payload_state_transition_post_state payload_state_transition_pre_state
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-review-mainnet.yml

@@ -8,68 +8,47 @@ on:
   pull_request:
     branches:
       - main
-
   workflow_dispatch:
 
 jobs:
   verify:
     runs-on: ubuntu-latest
-
     steps:
-      - name: Checkout
-        uses: actions/checkout@v2
+      - uses: actions/checkout@v4
         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 }}
+      - uses: Certora/certora-run-action@v1
+        with:
+          # --disable_auto_cache_key_gen
+          configurations: |-
+            security/certora/confs/verifyVotingStrategy_unittests.conf
+            security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance
+            security/certora/confs/verifyGovernancePowerStrategy.conf --rule transferPowerCompliance
+            security/certora/confs/verifyGovernancePowerStrategy.conf --rule powerlessCompliance method_reachability
+            security/certora/confs/verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal
+            security/certora/confs/verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal
+            security/certora/confs/verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero
+            security/certora/confs/verifyGovernance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease
+            security/certora/confs/verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives
+            security/certora/confs/verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal
+            security/certora/confs/verifyGovernance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant
+            security/certora/confs/verifyGovernance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period
+            security/certora/confs/verifyGovernance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel
+            security/certora/confs/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
+            security/certora/confs/verifyGovernance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal
+            security/certora/confs/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
+            security/certora/confs/verifyGovernance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence
+            security/certora/confs/verifyGovernance.conf --rule insufficient_proposition_power_witness_time_elapsed
+            security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal
+            security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash
+            security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state
+            security/certora/confs/verifyGovernance.conf --rule only_state_changing_function_initiate_transitions__post_state
+            security/certora/confs/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
+            security/certora/confs/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
+          solc-versions: 0.8.19
+          solc-remove-version-prefix: "0."
+          cli-version: 7.20.3
+          job-name: "AAVE Governance V3 Mainnet"
+          certora-key: ${{ secrets.CERTORAKEY }}
         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
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}