Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

WIP: Add GH Application #31

Closed
wants to merge 3 commits into from
Closed

WIP: Add GH Application #31

wants to merge 3 commits into from

Conversation

H00N24
Copy link
Collaborator

@H00N24 H00N24 commented Jan 8, 2025

No description provided.

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Execution Chain)

  • Group ID: ca4239ac-8d34-4184-a204-17e5163ac87b
Config Status Link Log File
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-da2f010395d5.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_callData_immutable Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-a01925256925.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-f8a5135e9e7a.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_signature_immutable Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-3c55e4340ec1.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-05ff215ece7c.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-4156837c33ce.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executedAt_is_zero_before_executed Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-06c2370932cf.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-05f8f3db5fb6.log
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 Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-0a8fa34332af.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_after_createPayload Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-ead2970f56fb.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_if_action_not_null Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-0470117a2c89.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_iff_action_not_null Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-7f93d6d5e682.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-dba67dc455ff.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero Submited link security/certora/confs/payloads/verifyPayloadsController.conf-74571c08e531.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-2d363badce4e.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-7c7c354e15a2.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule nonempty_actions Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-83e908ae3acf.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule null_access_level_iff_state_is_none Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-6d7a6d4b4812.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_delay_within_range Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-c6764d6cae74.log
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 Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-da6df546d342.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_state_transition_post_state payload_state_transition_pre_state Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-0b59017a4472.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-05714d928001.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule zero_executedAt_if_not_executed Failed (1) - security/certora/confs/payloads/verifyPayloadsController.conf-91408d0288b8.log

Certora Run Summary

  • Started 1 jobs
  • 22 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Voting Chain)

  • Group ID: fe295282-193e-4da3-935b-42d78b98480d
Config Status Link Log File
security/certora/confs/voting/verifyLegality.conf --rule createdVoteHasNonZeroHash Failed (1) - security/certora/confs/voting/verifyLegality.conf-1a438300a2fc.log
security/certora/confs/voting/verifyLegality.conf --rule legalVote Failed (1) - security/certora/confs/voting/verifyLegality.conf-8a407de94377.log
security/certora/confs/voting/verifyLegality.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyLegality.conf-644aa0200e72.log
security/certora/confs/voting/verifyLegality.conf --rule onlyValidProposalCanChangeTally Failed (1) - security/certora/confs/voting/verifyLegality.conf-7b7c14fb7c20.log
security/certora/confs/voting/verifyLegality.conf --rule votedPowerIsImmutable Failed (1) - security/certora/confs/voting/verifyLegality.conf-463b3b8297cc.log
security/certora/confs/voting/verifyMisc.conf Failed (1) - security/certora/confs/voting/verifyMisc.conf-f552c1c7341c.log
security/certora/confs/voting/verifyPower_summary.conf --rule method_reachability Submited link security/certora/confs/voting/verifyPower_summary.conf-32cffa07bc4c.log
security/certora/confs/voting/verifyPower_summary.conf --rule onlyThreeTokens Failed (1) - security/certora/confs/voting/verifyPower_summary.conf-abb4a020350c.log
security/certora/confs/voting/verifyProposal_config.conf --rule createdProposalHasRoots Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-59076381c317.log
security/certora/confs/voting/verifyProposal_config.conf --rule getProposalsConfigsDoesntRevert Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-a5b9513e5dbb.log
security/certora/confs/voting/verifyProposal_config.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-dd76d740f354.log
security/certora/confs/voting/verifyProposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-8bc5d77fa1a9.log
security/certora/confs/voting/verifyProposal_config.conf --rule startedProposalHasConfig Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-7dbd91fde486.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalHasNonzeroDuration method_reachability Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-b104b5bc3c8b.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalIdIsImmutable Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-137b3758f12b.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalImmutability Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-710b6fb9356a.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalLegalStates Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-907af13189ad.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalMethodStateTransitionCompliance Submited link security/certora/confs/voting/verifyProposal_states.conf-64b81e106118.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalTimeStateTransitionCompliance Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-157d5484a437.log
security/certora/confs/voting/verifyProposal_states.conf --rule startedProposalHasConfig Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-13ac9f0f3d20.log
security/certora/confs/voting/verifyProposal_states.conf --rule startsBeforeEnds Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-46e96af05652.log
security/certora/confs/voting/verifyProposal_states.conf --rule startsStrictlyBeforeEnds Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-2569daa9b5a4.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-0f83f606876d.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-c587dc5f5346.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-695ac88901d2.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-ad36f735dd96.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule onlyVoteCanChangeResult Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-b45f4373f44a.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule otherProposalUnchanged Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-8a5acc574f02.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule otherVoterUntouched Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-dc8ecd47e8d2.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule strangerVoteUnchanged Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-7773a8a06fb5.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule sumOfVotes Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-6d1f40fca1d0.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-b940f321f210.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule voteUpdatesTally Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-6f168702c100.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule votingPowerGhostIsVotingPower Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-4d5e8d2bf0fc.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule votingTallyCanOnlyIncrease Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-2e835a709cc7.log

Certora Run Summary

  • Started 2 jobs
  • 33 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Mainnet)

  • Group ID: 8ecdb414-0085-4d7d-8c31-3202c5986cf6
Config Status Link Log File
security/certora/confs/verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal Submited link security/certora/confs/verifyGovernance.conf-64abec452044.log
security/certora/confs/verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal Failed (1) - security/certora/confs/verifyGovernance.conf-9d38825fea5b.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-3d7e3533eaae.log
security/certora/confs/verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives Failed (1) - security/certora/confs/verifyGovernance.conf-81f2cbcb2d92.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-3a887f5e376b.log
security/certora/confs/verifyGovernance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence Failed (1) - security/certora/confs/verifyGovernance.conf-efc3e3368673.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash Failed (1) - security/certora/confs/verifyGovernance.conf-686ce1db5921.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal Failed (1) - security/certora/confs/verifyGovernance.conf-b7b345cbaf0d.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state Failed (1) - security/certora/confs/verifyGovernance.conf-e73c207b7c90.log
security/certora/confs/verifyGovernance.conf --rule insufficient_proposition_power_witness_time_elapsed Failed (1) - security/certora/confs/verifyGovernance.conf-f2be2a99fe1a.log
security/certora/confs/verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero Failed (1) - security/certora/confs/verifyGovernance.conf-da0fe9b556ff.log
security/certora/confs/verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal Failed (1) - security/certora/confs/verifyGovernance.conf-57d815c0db33.log
security/certora/confs/verifyGovernance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant Failed (1) - security/certora/confs/verifyGovernance.conf-e7007ee782d2.log
security/certora/confs/verifyGovernance.conf --rule only_state_changing_function_initiate_transitions__post_state Failed (1) - security/certora/confs/verifyGovernance.conf-2690ebece136.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-46788332d539.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-57a05fe897e9.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-ef847c902580.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-55321df32223.log
security/certora/confs/verifyGovernance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period Failed (1) - security/certora/confs/verifyGovernance.conf-ad706bb5465f.log
security/certora/confs/verifyGovernance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease Failed (1) - security/certora/confs/verifyGovernance.conf-809bffacfed2.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-ae92e1a3bff5.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule powerlessCompliance method_reachability Failed (1) - security/certora/confs/verifyGovernancePowerStrategy.conf-b0617aa783eb.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule transferPowerCompliance Failed (1) - security/certora/confs/verifyGovernancePowerStrategy.conf-a02b118577ed.log
security/certora/confs/verifyVotingStrategy_unittests.conf Submited link security/certora/confs/verifyVotingStrategy_unittests.conf-9527b65cdc8a.log

Certora Run Summary

  • Started 3 jobs
  • 21 jobs failed

Download Logs

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: ca4239ac-8d34-4184-a204-17e5163ac87b
Job Status Result VERIFIED Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero SUCCEEDED ✅ 3 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 8ecdb414-0085-4d7d-8c31-3202c5986cf6
Job Status Result VERIFIED Link
security/certora/confs/verifyVotingStrategy_unittests.conf SUCCEEDED ✅ 8 Link
security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance SUCCEEDED ✅ 2 Link
security/certora/confs/verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal SUCCEEDED ✅ 3 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: fe295282-193e-4da3-935b-42d78b98480d
Job Status Result VERIFIED Link
security/certora/confs/voting/verifyProposal_states.conf --rule proposalMethodStateTransitionCompliance SUCCEEDED ✅ 2 Link
security/certora/confs/voting/verifyPower_summary.conf --rule method_reachability SUCCEEDED ✅ 2 Link

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Mainnet)

  • Group ID: c20c58b6-e0fc-45d5-abef-345b900bddee
Config Status Link Log File
security/certora/confs/verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal Failed (1) - security/certora/confs/verifyGovernance.conf-5dac0e1cf89d.log
security/certora/confs/verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal Failed (1) - security/certora/confs/verifyGovernance.conf-79d13a93086d.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-3ab1c631c191.log
security/certora/confs/verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives Failed (1) - security/certora/confs/verifyGovernance.conf-c0aefee29b10.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-50f4920d5717.log
security/certora/confs/verifyGovernance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence Failed (1) - security/certora/confs/verifyGovernance.conf-59c05c74686d.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash Failed (1) - security/certora/confs/verifyGovernance.conf-ce406a971003.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal Failed (1) - security/certora/confs/verifyGovernance.conf-89455de846b3.log
security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state Failed (1) - security/certora/confs/verifyGovernance.conf-b43abdaad717.log
security/certora/confs/verifyGovernance.conf --rule insufficient_proposition_power_witness_time_elapsed Failed (1) - security/certora/confs/verifyGovernance.conf-4ac99fcc3e9e.log
security/certora/confs/verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero Failed (1) - security/certora/confs/verifyGovernance.conf-5216f70b7449.log
security/certora/confs/verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal Submited link security/certora/confs/verifyGovernance.conf-fdda711aa366.log
security/certora/confs/verifyGovernance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant Failed (1) - security/certora/confs/verifyGovernance.conf-c728c6ca0984.log
security/certora/confs/verifyGovernance.conf --rule only_state_changing_function_initiate_transitions__post_state Failed (1) - security/certora/confs/verifyGovernance.conf-4bffaf49c6fd.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-fb73ddcd97f2.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-a20f2d35922b.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-76f0db97d8ba.log
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 Failed (1) - security/certora/confs/verifyGovernance.conf-d93164c87305.log
security/certora/confs/verifyGovernance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period Failed (1) - security/certora/confs/verifyGovernance.conf-25bd2f26a7ea.log
security/certora/confs/verifyGovernance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease Failed (1) - security/certora/confs/verifyGovernance.conf-8a7e28dacc3a.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance Submited link security/certora/confs/verifyGovernancePowerStrategy.conf-0c3396677b2e.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule powerlessCompliance method_reachability Failed (1) - security/certora/confs/verifyGovernancePowerStrategy.conf-bd6977f3c2ca.log
security/certora/confs/verifyGovernancePowerStrategy.conf --rule transferPowerCompliance Failed (1) - security/certora/confs/verifyGovernancePowerStrategy.conf-22ff79939e51.log
security/certora/confs/verifyVotingStrategy_unittests.conf Submited link security/certora/confs/verifyVotingStrategy_unittests.conf-08811e8b6b86.log

Certora Run Summary

  • Started 3 jobs
  • 21 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Execution Chain)

  • Group ID: c86a121c-d614-4763-b1fe-8069b9109be8
Config Status Link Log File
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3704ae503f68.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_callData_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-8eca07f72c5a.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields Submited link security/certora/confs/payloads/verifyPayloadsController.conf-dac1f92509d2.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_signature_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-08cde762c7a8.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-2d95bde8eb1b.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3e2c6ff86d87.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executedAt_is_zero_before_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-0639f7fa6ad2.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-5d0d15d7ac23.log
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 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-a6a74ba51b82.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ae353be58f7c.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-8fa30848a0fa.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_iff_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-4325eb56c3c9.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-fba26c9af8f4.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero Submited link security/certora/confs/payloads/verifyPayloadsController.conf-343e52ce1c6a.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists Submited link security/certora/confs/payloads/verifyPayloadsController.conf-822aecaf6d63.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3f400b20b32b.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule nonempty_actions Submited link security/certora/confs/payloads/verifyPayloadsController.conf-238646732a37.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule null_access_level_iff_state_is_none Submited link security/certora/confs/payloads/verifyPayloadsController.conf-d2e23cd4b586.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_delay_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-272253f2984d.log
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 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-3d9442af2e93.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_state_transition_post_state payload_state_transition_pre_state Submited link security/certora/confs/payloads/verifyPayloadsController.conf-af1daf9791c6.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence Submited link security/certora/confs/payloads/verifyPayloadsController.conf-30e3708d0e59.log
security/certora/confs/payloads/verifyPayloadsController.conf --rule zero_executedAt_if_not_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-5b504561f398.log

Certora Run Summary

  • Started 23 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Voting Chain)

  • Group ID: 221a88a6-6fca-4bc0-8833-a0943f7c160c
Config Status Link Log File
security/certora/confs/voting/verifyLegality.conf --rule createdVoteHasNonZeroHash Failed (1) - security/certora/confs/voting/verifyLegality.conf-a9da298a5f36.log
security/certora/confs/voting/verifyLegality.conf --rule legalVote Submited link security/certora/confs/voting/verifyLegality.conf-9ffe3d9b583f.log
security/certora/confs/voting/verifyLegality.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyLegality.conf-601d84383147.log
security/certora/confs/voting/verifyLegality.conf --rule onlyValidProposalCanChangeTally Failed (1) - security/certora/confs/voting/verifyLegality.conf-2856e052fbca.log
security/certora/confs/voting/verifyLegality.conf --rule votedPowerIsImmutable Failed (1) - security/certora/confs/voting/verifyLegality.conf-8500ca826710.log
security/certora/confs/voting/verifyMisc.conf Submited link security/certora/confs/voting/verifyMisc.conf-e7dd90abd458.log
security/certora/confs/voting/verifyPower_summary.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyPower_summary.conf-a668a7759460.log
security/certora/confs/voting/verifyPower_summary.conf --rule onlyThreeTokens Failed (1) - security/certora/confs/voting/verifyPower_summary.conf-bf967bcfea9d.log
security/certora/confs/voting/verifyProposal_config.conf --rule createdProposalHasRoots Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-38e96b651b0e.log
security/certora/confs/voting/verifyProposal_config.conf --rule getProposalsConfigsDoesntRevert Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-2292c392e028.log
security/certora/confs/voting/verifyProposal_config.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-9fe12f159a13.log
security/certora/confs/voting/verifyProposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-67121b2f981c.log
security/certora/confs/voting/verifyProposal_config.conf --rule startedProposalHasConfig Failed (1) - security/certora/confs/voting/verifyProposal_config.conf-925cf3f1b0fb.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalHasNonzeroDuration method_reachability Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-55dc9d70395e.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalIdIsImmutable Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-639de85f1499.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalImmutability Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-fcc4924b9be6.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalLegalStates Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-a6bed0f8e78d.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalMethodStateTransitionCompliance Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-3cff177f7460.log
security/certora/confs/voting/verifyProposal_states.conf --rule proposalTimeStateTransitionCompliance Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-64acaefa4176.log
security/certora/confs/voting/verifyProposal_states.conf --rule startedProposalHasConfig Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-b31539822838.log
security/certora/confs/voting/verifyProposal_states.conf --rule startsBeforeEnds Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-f0569158c5b3.log
security/certora/confs/voting/verifyProposal_states.conf --rule startsStrictlyBeforeEnds Failed (1) - security/certora/confs/voting/verifyProposal_states.conf-e4ac0f0fe0a2.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-0c92bf879ad1.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-af5e1945b6ba.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-b4243dfa3428.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule method_reachability Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-5e9828854a82.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule onlyVoteCanChangeResult Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-06d4314299b8.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule otherProposalUnchanged Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-7cb5a407bb97.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule otherVoterUntouched Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-6a5725126959.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule strangerVoteUnchanged Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-f8a28dd7b1c8.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule sumOfVotes Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-b99fb3ece651.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-430793878371.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule voteUpdatesTally Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-49739a6ce35d.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule votingPowerGhostIsVotingPower Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-1fa392cc2231.log
security/certora/confs/voting/verifyVoting_and_tally.conf --rule votingTallyCanOnlyIncrease Failed (1) - security/certora/confs/voting/verifyVoting_and_tally.conf-89752b828100.log

Certora Run Summary

  • Started 2 jobs
  • 33 jobs failed

Download Logs

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: c20c58b6-e0fc-45d5-abef-345b900bddee
Job Status Result VERIFIED Link
security/certora/confs/verifyVotingStrategy_unittests.conf SUCCEEDED ✅ 8 Link
security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance SUCCEEDED ✅ 2 Link
security/certora/confs/verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal SUCCEEDED ✅ 6 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: c86a121c-d614-4763-b1fe-8069b9109be8
Job Status Result VERIFIED Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_signature_immutable SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_callData_immutable SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 SUCCEEDED ✅ 6 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executedAt_is_zero_before_executed SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable SUCCEEDED ✅ 3 Link
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 SUCCEEDED ✅ 6 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_after_createPayload SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_if_action_not_null SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_iff_action_not_null SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_isnt_used_twice executor_of_level_null_is_zero SUCCEEDED ✅ 3 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule nonempty_actions SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule null_access_level_iff_state_is_none SUCCEEDED ✅ 2 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_delay_within_range SUCCEEDED ✅ 2 Link
no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability SUCCEEDED ✅ 29 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule payload_state_transition_post_state payload_state_transition_pre_state SUCCEEDED ✅ 3 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence SUCCEEDED ✅ 4 Link
security/certora/confs/payloads/verifyPayloadsController.conf --rule zero_executedAt_if_not_executed SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 221a88a6-6fca-4bc0-8833-a0943f7c160c
Job Status Result VERIFIED Link
security/certora/confs/voting/verifyLegality.conf --rule legalVote SUCCEEDED ✅ 2 Link
security/certora/confs/voting/verifyMisc.conf SUCCEEDED ✅ 6 Link

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Execution Chain)

  • Group ID: dc032367-446a-4df9-b7b5-ab39b4fc7266
Config Status Link Log File
action_access_level_isnt_null_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-bf80cfb200f9.log
action_callData_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-a18aca237e55.log
action_immutable_check_only_fixed_size_fields Submited link security/certora/confs/payloads/verifyPayloadsController.conf-35238cbf99c7.log
action_signature_immutable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-fdc627a79ce3.log
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-80a4c9ff435c.log
delay_of_executor_of_max_access_level_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-ca9bc8f5fc4a.log
executedAt_is_zero_before_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-e39c7c850328.log
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable Submited link security/certora/confs/payloads/verifyPayloadsController.conf-37d27bb4b49d.log
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease Submited link security/certora/confs/payloads/verifyPayloadsController.conf-37d3285570ad.log
executor_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-c7530b908387.log
executor_exists_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-b997f387a534.log
executor_exists_iff_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-f8bb3b5c304c.log
executor_exists_only_if_action_not_null Submited link security/certora/confs/payloads/verifyPayloadsController.conf-41acec5fceab.log
executor_isnt_used_twice executor_of_level_null_is_zero Submited link security/certora/confs/payloads/verifyPayloadsController.conf-a3f883671e3a.log
executor_of_maximumAccessLevelRequired_exists Submited link security/certora/confs/payloads/verifyPayloadsController.conf-dbd32f61c35a.log
executor_of_maximumAccessLevelRequired_exists_after_createPayload Submited link security/certora/confs/payloads/verifyPayloadsController.conf-c9b1676adfa9.log
nonempty_actions Submited link security/certora/confs/payloads/verifyPayloadsController.conf-db0da22192c5.log
null_access_level_iff_state_is_none Submited link security/certora/confs/payloads/verifyPayloadsController.conf-cdd8f00721aa.log
payload_delay_within_range Submited link security/certora/confs/payloads/verifyPayloadsController.conf-990332342eab.log
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 Submited link security/certora/confs/payloads/verifyPayloadsController.conf-9c1bea1a4f12.log
payload_state_transition_post_state payload_state_transition_pre_state Submited link security/certora/confs/payloads/verifyPayloadsController.conf-51fab4576e0b.log
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence Submited link security/certora/confs/payloads/verifyPayloadsController.conf-130b99e45528.log
zero_executedAt_if_not_executed Submited link security/certora/confs/payloads/verifyPayloadsController.conf-1c81e0c39a71.log

Certora Run Summary

  • Started 23 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Mainnet)

  • Group ID: c40018f3-5fa3-4f5f-9cfb-3a8c7a6298cd
Config Status Link Log File
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal Submited link Governance.conf-693a9ae0b678.log
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal Submited link Governance.conf-a41fdcb25b30.log
Governance.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 Submited link Governance.conf-fbb2373bac13.log
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives Submited link Governance.conf-2c00f2efd811.log
Governance.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 Submited link Governance.conf-8c6bf3cff574.log
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence Submited link Governance.conf-305fb18e7e16.log
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash Submited link Governance.conf-e2f72a8e00b9.log
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal Submited link Governance.conf-8178030fe1f3.log
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state Submited link Governance.conf-d734d18a2912.log
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed Submited link Governance.conf-0b4ac2c4c906.log
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero Submited link Governance.conf-0804b31351ed.log
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal Submited link Governance.conf-4ce26d301b0f.log
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant Submited link Governance.conf-32331467fe12.log
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state Submited link Governance.conf-463b9f8cba92.log
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel Submited link Governance.conf-ae3c1ea2b2fc.log
Governance.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 Submited link Governance.conf-feb0d01320bb.log
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state Submited link Governance.conf-0ccc35a7de4a.log
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal Submited link Governance.conf-134914b801c2.log
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period Submited link Governance.conf-4f078329f3a0.log
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease Submited link Governance.conf-1466e67c3025.log
GovernancePowerStrategy.conf --rule delegatePowerCompliance Submited link GovernancePowerStrategy.conf-7a12193ecdbb.log
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability Submited link GovernancePowerStrategy.conf-81a8468c4d5d.log
GovernancePowerStrategy.conf --rule transferPowerCompliance Submited link GovernancePowerStrategy.conf-965d25de4d21.log
VotingStrategy_unittests.conf Submited link VotingStrategy_unittests.conf-7d484011158b.log

Certora Run Summary

  • Started 24 jobs
  • 0 jobs failed

Download Logs

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 8, 2025

Certora Run Started (AAVE Governance V3 Voting Chain)

  • Group ID: 3529aa34-f611-4483-baf7-b507e3556ca5
Config Status Link Log File
Legality.conf --rule createdVoteHasNonZeroHash Submited link Legality.conf-fd9e3b90fb1a.log
Legality.conf --rule legalVote Submited link Legality.conf-2b56ec19278e.log
Legality.conf --rule method_reachability Submited link Legality.conf-086f25b9e3f5.log
Legality.conf --rule onlyValidProposalCanChangeTally Submited link Legality.conf-50493eac6ff4.log
Legality.conf --rule votedPowerIsImmutable Submited link Legality.conf-627a5c52270d.log
Misc.conf Submited link Misc.conf-d86996cad9a2.log
Power_summary.conf --rule method_reachability Submited link Power_summary.conf-8c9449c95807.log
Power_summary.conf --rule onlyThreeTokens Submited link Power_summary.conf-5b0b89e5a20a.log
Proposal_config.conf --rule createdProposalHasRoots Submited link Proposal_config.conf-9ce94fccafc7.log
Proposal_config.conf --rule getProposalsConfigsDoesntRevert Submited link Proposal_config.conf-a12cbc687fcd.log
Proposal_config.conf --rule method_reachability Submited link Proposal_config.conf-691a74e9bd20.log
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable Submited link Proposal_config.conf-26d0bd1505e4.log
Proposal_config.conf --rule startedProposalHasConfig Submited link Proposal_config.conf-7b889abcf0ea.log
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability Submited link Proposal_states.conf-82af282b75c2.log
Proposal_states.conf --rule proposalIdIsImmutable Submited link Proposal_states.conf-07c40f693e92.log
Proposal_states.conf --rule proposalImmutability Submited link Proposal_states.conf-7e44e0fc9dbf.log
Proposal_states.conf --rule proposalLegalStates Submited link Proposal_states.conf-0c7ee3deb60a.log
Proposal_states.conf --rule proposalMethodStateTransitionCompliance Submited link Proposal_states.conf-95a03bf06ce1.log
Proposal_states.conf --rule proposalTimeStateTransitionCompliance Submited link Proposal_states.conf-3c9f8c45c443.log
Proposal_states.conf --rule startedProposalHasConfig Submited link Proposal_states.conf-e5ac06f2a1a8.log
Proposal_states.conf --rule startsBeforeEnds Submited link Proposal_states.conf-42d9e5d2f635.log
Proposal_states.conf --rule startsStrictlyBeforeEnds Submited link Proposal_states.conf-a86b6c643a0b.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote Submited link Voting_and_tally.conf-7b4ee7852e92.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote Submited link Voting_and_tally.conf-ebbf82716452.log
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative Submited link Voting_and_tally.conf-8ecbe982e250.log
Voting_and_tally.conf --rule method_reachability Submited link Voting_and_tally.conf-078a27d8b765.log
Voting_and_tally.conf --rule onlyVoteCanChangeResult Submited link Voting_and_tally.conf-aa3791763d2b.log
Voting_and_tally.conf --rule otherProposalUnchanged Submited link Voting_and_tally.conf-22cb31e0345d.log
Voting_and_tally.conf --rule otherVoterUntouched Submited link Voting_and_tally.conf-47ae3b00eb45.log
Voting_and_tally.conf --rule strangerVoteUnchanged Submited link Voting_and_tally.conf-d19e8ca522e4.log
Voting_and_tally.conf --rule sumOfVotes Submited link Voting_and_tally.conf-1f511255778b.log
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting Submited link Voting_and_tally.conf-7cc9b9fe7ddc.log
Voting_and_tally.conf --rule voteUpdatesTally Submited link Voting_and_tally.conf-9693e348ae6b.log
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower Submited link Voting_and_tally.conf-93fd6883f1a9.log
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease Submited link Voting_and_tally.conf-26fb03ec12cf.log

Certora Run Summary

  • Started 35 jobs
  • 0 jobs failed

Download Logs

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: dc032367-446a-4df9-b7b5-ab39b4fc7266
Job Status Result VERIFIED Link
action_immutable_check_only_fixed_size_fields SUCCEEDED ✅ 2 Link
action_callData_immutable SUCCEEDED ✅ 2 Link
action_signature_immutable SUCCEEDED ✅ 2 Link
checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4 SUCCEEDED ✅ 6 Link
action_access_level_isnt_null_after_createPayload SUCCEEDED ✅ 2 Link
executedAt_is_zero_before_executed SUCCEEDED ✅ 2 Link
delay_of_executor_of_max_access_level_within_range SUCCEEDED ✅ 2 Link
executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease SUCCEEDED ✅ 6 Link
executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable SUCCEEDED ✅ 3 Link
executor_exists_after_createPayload SUCCEEDED ✅ 2 Link
executor_exists_iff_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_if_action_not_null SUCCEEDED ✅ 2 Link
executor_exists_only_if_action_not_null SUCCEEDED ✅ 2 Link
executor_of_maximumAccessLevelRequired_exists SUCCEEDED ✅ 2 Link
executor_isnt_used_twice executor_of_level_null_is_zero SUCCEEDED ✅ 3 Link
nonempty_actions SUCCEEDED ✅ 2 Link
executor_of_maximumAccessLevelRequired_exists_after_createPayload SUCCEEDED ✅ 2 Link
payload_delay_within_range SUCCEEDED ✅ 2 Link
null_access_level_iff_state_is_none SUCCEEDED ✅ 2 Link
queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence SUCCEEDED ✅ 4 Link
payload_state_transition_post_state payload_state_transition_pre_state SUCCEEDED ✅ 3 Link
no_early_cancellation execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability SUCCEEDED ✅ 29 Link
zero_executedAt_if_not_executed SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: c40018f3-5fa3-4f5f-9cfb-3a8c7a6298cd
Job Status Result VERIFIED Link
Governance.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 SUCCEEDED ✅ 5 Link
Governance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal SUCCEEDED ✅ 4 Link
Governance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal SUCCEEDED ✅ 3 Link
Governance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives SUCCEEDED ✅ 3 Link
Governance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence SUCCEEDED ✅ 4 Link
esentatives_witness_antecedent_second check_new_representative_set_size_after_updateRepresentatives_witness_consequent_first check_new_representative_set_size_after_updateRepresentatives_witness_consequent_second SUCCEEDED ✅ 5 Link
VotingStrategy_unittests.conf SUCCEEDED ✅ 8 Link
Governance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash SUCCEEDED ✅ 4 Link
Governance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal SUCCEEDED ✅ 3 Link
Governance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state SUCCEEDED ✅ 4 Link
Governance.conf --rule insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 2 Link
Governance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal SUCCEEDED ✅ 6 Link
Governance.conf --rule no_representative_is_zero_2 no_representative_of_zero SUCCEEDED ✅ 3 Link
Governance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant SUCCEEDED ✅ 4 Link
Governance.conf --rule only_state_changing_function_initiate_transitions__post_state SUCCEEDED ✅ 2 Link
Governance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel SUCCEEDED ✅ 6 Link
ortal_invalidate insufficient_proposition_power insufficient_proposition_power_witness_state_is_failed insufficient_proposition_power_witness_state_is_cancelled insufficient_proposition_power_witness_time_elapsed SUCCEEDED ✅ 6 Link
Governance.conf --rule proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state SUCCEEDED ✅ 5 Link
Governance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period SUCCEEDED ✅ 3 Link
Governance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal SUCCEEDED ✅ 5 Link
Governance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease SUCCEEDED ✅ 5 Link
GovernancePowerStrategy.conf --rule transferPowerCompliance SUCCEEDED ✅ 2 Link
GovernancePowerStrategy.conf --rule powerlessCompliance method_reachability SUCCEEDED ✅ 3 Link
GovernancePowerStrategy.conf --rule delegatePowerCompliance SUCCEEDED ✅ 2 Link

certora-run[bot]
certora-run bot reviewed Jan 8, 2025
View reviewed changes
Copy link

@certora-run certora-run bot left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verification Results

  • Group ID: 3529aa34-f611-4483-baf7-b507e3556ca5
Job Status Result VERIFIED Link
Legality.conf --rule legalVote SUCCEEDED ✅ 2 Link
Legality.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Legality.conf --rule onlyValidProposalCanChangeTally SUCCEEDED ✅ 2 Link
Legality.conf --rule votedPowerIsImmutable SUCCEEDED ✅ 2 Link
Legality.conf --rule createdVoteHasNonZeroHash SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule createdProposalHasRoots SUCCEEDED ✅ 2 Link
Misc.conf SUCCEEDED ✅ 6 Link
Proposal_config.conf --rule getProposalsConfigsDoesntRevert SUCCEEDED ✅ 2 Link
Power_summary.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Power_summary.conf --rule onlyThreeTokens SUCCEEDED ✅ 2 Link
Proposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable SUCCEEDED ✅ 4 Link
Proposal_config.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalHasNonzeroDuration method_reachability SUCCEEDED ✅ 3 Link
Proposal_config.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalIdIsImmutable SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalImmutability SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalLegalStates SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalMethodStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startedProposalHasConfig SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule proposalTimeStateTransitionCompliance SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsBeforeEnds SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Proposal_states.conf --rule startsStrictlyBeforeEnds SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule method_reachability SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherVoterUntouched SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule onlyVoteCanChangeResult SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule otherProposalUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule strangerVoteUnchanged SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule sumOfVotes SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingTallyCanOnlyIncrease SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteTallyChangedOnlyByVoting SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule voteUpdatesTally SUCCEEDED ✅ 2 Link
Voting_and_tally.conf --rule votingPowerGhostIsVotingPower SUCCEEDED ✅ 2 Link

@H00N24 H00N24 mentioned this pull request Jan 8, 2025
Merged
@H00N24 H00N24 closed this Jan 9, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@certora-run certora-run[bot] certora-run[bot] left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@H00N24