Merge pull request bgd-labs#39 from Certora/certora-squashed

Certora review - move to prover version 7.20.3
Certora · Dec 4, 2024 · be377dd · be377dd
2 parents 70865bf + d6be91f
commit be377dd
Show file tree

Hide file tree

Showing 32 changed files with 1,821 additions and 543 deletions.
diff --git a/.github/workflows/certora-review-execution-chain.yml b/.github/workflows/certora-review-execution-chain.yml
@@ -28,7 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==4.13.1
+        run: pip3 install certora-cli==7.20.3
 
       - name: Install solc
         run: |
@@ -47,7 +47,7 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyPayloadsController.conf --rule payload_maximal_access_level_gt_action_access_level no_late_cancel 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 executedAt_is_zero_before_executed queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation guardian_can_cancel executed_when_in_queued_state execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability
+          - 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
@@ -64,4 +64,10 @@ jobs:
           - 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
diff --git a/.github/workflows/certora-review-mainnet.yml b/.github/workflows/certora-review-mainnet.yml
@@ -30,7 +30,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==4.13.1
+        run: pip3 install certora-cli==7.20.3
 
       - name: Install solc
         run: |
@@ -50,17 +50,26 @@ jobs:
       matrix:
         rule:
           - verifyVotingStrategy_unittests.conf
-          - verifyGovernancePowerStrategy.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 empty_payloads_if_uninitialized_proposal null_state_variable_only_if_uninitialized_proposal 
-          - verifyGovernance.conf --rule post_state state_changing_function_self_check state_variable_changing_function_self_check  method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease
+          - 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 at_least_single_payload_active_variable creator_is_not_zero creator_is_not_zero_2 empty_payloads_iff_uninitialized_proposal 
-          - verifyGovernance.conf --rule null_state_iff_uninitialized_proposal null_state_variable_iff_uninitialized_proposal null_state_if_uninitialized_proposal null_state_variable_if_uninitialized_proposal setInvariant addressSetInvariant
-          - verifyGovernance.conf --rule null_state_only_if_uninitialized_proposal pre_state 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_payload_after_creation immutable_after_creation only_guardian_can_cancel guardian_can_cancel 
+          - 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 insufficient_proposition_power_time_elapsed_tight_witness 
-          - verifyGovernance.conf --rule insufficient_proposition_power_allow_time_elapse insufficient_proposition_power proposal_after_voting_portal_invalidate
-
+          - 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
diff --git a/.github/workflows/certora-review-voting-chain.yml b/.github/workflows/certora-review-voting-chain.yml
@@ -1,4 +1,4 @@
-# Github action for verifying the contracts under src/contracts/voting
+# Github action for verifying the contracts under src/contracts/voting using certora-cli-beta 6
 name: certora-review-voting-chain
 
 on:
@@ -30,7 +30,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==4.13.1
+        run: pip3 install certora-cli==7.20.3
 
       - name: Install solc
         run: |
@@ -50,29 +50,37 @@ jobs:
       matrix:
         rule:
           - verifyLegality.conf --rule createdVoteHasNonZeroHash
+          - verifyLegality.conf --rule votedPowerIsImmutable
           - verifyLegality.conf --rule onlyValidProposalCanChangeTally
           - verifyLegality.conf --rule legalVote
-          - verifyLegality.conf --rule votedPowerIsImmutable method_reachability
+          - verifyLegality.conf --rule method_reachability
           - verifyMisc.conf
-          - verifyPower_summary.conf --rule onlyThreeTokens
-          -  verifyPower_summary.conf --rule method_reachability
-          - verifyProposal_config.conf --rule createdProposalHasRoots
+          - verifyPower_summary.conf --rule onlyThreeTokens #TODO: uncomment with certora-cli version 6.0 or higher
+          - verifyPower_summary.conf --rule method_reachability
           - verifyProposal_config.conf --rule startedProposalHasConfig
-          - verifyProposal_config.conf --rule proposalHasNonzeroDuration configIsImmutable newProposalUnusedId method_reachability
-          - verifyProposal_states.conf --rule proposalImmutability
-          - verifyProposal_states.conf --rule startsStrictlyBeforeEnds
+          - verifyProposal_config.conf --rule createdProposalHasRoots
+          - verifyProposal_config.conf --rule proposalHasNonzeroDuration newProposalUnusedId configIsImmutable
+          - verifyProposal_config.conf --rule getProposalsConfigsDoesntRevert
+          - verifyProposal_config.conf --rule method_reachability
           - verifyProposal_states.conf --rule startsBeforeEnds
-          - verifyProposal_states.conf --rule startedProposalHasConfig
+          - verifyProposal_states.conf --rule startsStrictlyBeforeEnds
+          - verifyProposal_states.conf --rule proposalLegalStates
           - verifyProposal_states.conf --rule proposalMethodStateTransitionCompliance
-          - verifyProposal_states.conf --rule proposalIdIsImmutable proposalHasNonzeroDuration proposalTimeStateTransitionCompliance proposalLegalStates method_reachability
+          - verifyProposal_states.conf --rule proposalTimeStateTransitionCompliance
+          - verifyProposal_states.conf --rule proposalIdIsImmutable
+          - verifyProposal_states.conf --rule proposalImmutability
+          - verifyProposal_states.conf --rule startedProposalHasConfig
+          - verifyProposal_states.conf --rule proposalHasNonzeroDuration method_reachability
+          - verifyVoting_and_tally.conf --rule votingPowerGhostIsVotingPower
+          - verifyVoting_and_tally.conf --rule sumOfVotes
+          - verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting
           - verifyVoting_and_tally.conf --rule voteUpdatesTally
-          - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote
           - verifyVoting_and_tally.conf --rule onlyVoteCanChangeResult
-          - verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting
-          - verifyVoting_and_tally.conf --rule  votingTallyCanOnlyIncrease 
-          - verifyVoting_and_tally.conf --rule strangerVoteUnchanged 
-          - verifyVoting_and_tally.conf --rule otherProposalUnchanged 
-          - verifyVoting_and_tally.conf --rule otherVoterUntouched 
+          - verifyVoting_and_tally.conf --rule votingTallyCanOnlyIncrease
+          - verifyVoting_and_tally.conf --rule strangerVoteUnchanged
+          - verifyVoting_and_tally.conf --rule otherProposalUnchanged
+          - verifyVoting_and_tally.conf --rule otherVoterUntouched
           - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative
           - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote
-          - verifyVoting_and_tally.conf --rule method_reachability
+          - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote
+          - verifyVoting_and_tally.conf --rule method_reachability
diff --git a/security/certora/confs/payloads/verifyPayloadsController.conf b/security/certora/confs/payloads/verifyPayloadsController.conf
@@ -1,7 +1,6 @@
 {
     "files": [
         "security/certora/harness/PayloadsControllerHarness.sol",
-        "src/contracts/payloads/Executor.sol",
         "src/contracts/payloads/PayloadsControllerUtils.sol",
         "security/certora/harness/DummyERC20Impl.sol"
     ],
@@ -13,16 +12,11 @@
     "msg": "All payloadControllers rules",
     "optimistic_hashing": true,
     "optimistic_loop": true,
-    "prover_args": [
-        " -smt_LIASolvers [z3:def,z3:lia1,z3:lia2] -smt_NIASolvers [z3:def]"
-    ],
+//    "prover_args": [" -smt_LIASolvers [z3:def,z3:lia1,z3:lia2] -smt_NIASolvers [z3:def]"    ],
+    "prover_args": ["-depth 0"],
     "smt_timeout": "6000",
+    "build_cache": true,
     "solc": "solc8.19",
-    "struct_link": [
-        "PayloadsControllerHarness:executor=Executor"
-    ],
-    //"parametric_contracts":["PayloadsControllerHarness"
-    //],
     //"rule_sanity": "advanced",
     "verify": "PayloadsControllerHarness:security/certora/specs/payloads/PayloadsController.spec"
 }
diff --git a/security/certora/confs/verifyGovernance.conf b/security/certora/confs/verifyGovernance.conf
@@ -1,7 +1,7 @@
 {
     "files": [
         "security/certora/harness/GovernanceHarness.sol",
-        "src/contracts/VotingPortal.sol",
+    //    "src/contracts/VotingPortal.sol",
         "src/contracts/voting/VotingStrategy.sol",
         "lib/aave-token-v3/src/AaveTokenV3.sol",
         "src/contracts/GovernancePowerStrategy.sol",
@@ -18,9 +18,9 @@
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "GovernanceHarness:security/certora/specs/Governance.spec",
-    "struct_link": [
-        "GovernanceHarness:votingPortal=VotingPortal"
-    ],
+    //"struct_link": [
+    //    "GovernanceHarness:votingPortal=VotingPortal"
+    //],
     "loop_iter": "3",
     "optimistic_loop": true,
     "prover_args": [
@@ -29,7 +29,8 @@
     "solc": "solc8.19",
     //"parametric_contracts":["GovernanceHarness"
     //],
-    "disable_auto_cache_key_gen" :true,
+//    "disable_auto_cache_key_gen" :true,
     //"rule_sanity": "advanced",
+    "build_cache": true,
     "msg": "All Governance rules",
 }
diff --git a/security/certora/confs/verifyGovernancePowerStrategy.conf b/security/certora/confs/verifyGovernancePowerStrategy.conf
@@ -1,6 +1,6 @@
 {
     "files": [
-        "src/contracts/GovernancePowerStrategy.sol",
+        "security/certora/harness/GovernancePowerStrategyHarness.sol",
         "security/certora/harness/tokens/AaveTokenV3_DummyA.sol",
         "security/certora/harness/tokens/AaveTokenV3_DummyB.sol",
         "security/certora/harness/tokens/AaveTokenV3_DummyC.sol"
@@ -15,10 +15,15 @@
         "openzeppelin-contracts=lib/openzeppelin-contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
-    "verify": "GovernancePowerStrategy:security/certora/specs/GovernancePowerStrategy.spec",
+    "verify": "GovernancePowerStrategyHarness:security/certora/specs/GovernancePowerStrategy.spec",
     "optimistic_loop": true,
     "loop_iter": "3",  // Needs 3 for the 3 tokens
+    "prover_args": [
+        " -smt_LIASolvers [z3:def,z3:lia1,z3:lia2] -smt_NIASolvers [z3:def]"
+    ],
     "solc": "solc8.19",
-    //"rule_sanity": "advanced",
+    "smt_timeout": "6000",
+    "rule_sanity": "basic",
+    "build_cache": true,
     "msg": "GovernancePowerStrategy tests"
 }
diff --git a/security/certora/confs/verifyVotingStrategy_unittests.conf b/security/certora/confs/verifyVotingStrategy_unittests.conf
@@ -20,5 +20,7 @@
     "optimistic_loop": true,
     "loop_iter": "3",  // Needs 2 for isTokenSlotAccepted (A_AAVE uses 2 slots)
     "solc": "solc8.19",
+    "rule_sanity": "basic",
+    "build_cache": true,
     "msg": "VotingStrategy tests"
 }
diff --git a/security/certora/confs/voting/verifyLegality.conf b/security/certora/confs/voting/verifyLegality.conf
@@ -28,7 +28,13 @@
     "loop_iter": "3",
     "optimistic_hashing": true,
     "solc": "solc8.19",
-    //"parametric_contracts":["VotingMachineHarness"
-    //],
+    "parametric_contracts": [
+        // Excluding DataWarehouse!
+	    "VotingMachineHarness",
+	    "VotingStrategyHarness",
+	    "CrossChainController"
+    ],
+    "build_cache": true,
+    "rule_sanity": "basic",
     "msg": "VotingMachine - legality rules"
 }
diff --git a/security/certora/confs/voting/verifyMisc.conf b/security/certora/confs/voting/verifyMisc.conf
@@ -28,5 +28,14 @@
     "loop_iter": "3",  // Needs 3 for `submitVoteTripleProof`
     "optimistic_hashing": true,
     "solc": "solc8.19",
+    "parametric_contracts": [
+        // Excluding DataWarehouse!
+        "VotingMachineHarnessTriple",
+        "VotingStrategyHarness",
+        "CrossChainController"
+    ],
+    "build_cache": true,
+    "smt_timeout": "6000",
+    "rule_sanity": "basic",
     "msg": "VotingMachine - miscellaneous rules"
 }
diff --git a/security/certora/confs/voting/verifyPower_summary.conf b/security/certora/confs/voting/verifyPower_summary.conf
@@ -28,5 +28,12 @@
     "loop_iter": "3",  // 3 is needed for `submitVoteTripleProof`; 2 for `isTokenSlotAccepted` (A_AAVE uses two slots)
     "optimistic_hashing": true,
     "solc": "solc8.19",
+    "parametric_contracts": [
+        // Excluding all other contracts
+        "VotingMachineHarnessTriple"
+    ],
+    // NOTE: not using sanity since onlyThreeTokens fails sanity on being tautologucal
+    //"rule_sanity": "basic",
+    "build_cache": true,
     "msg": "VotingMachine setup - basic tests"
 }
diff --git a/security/certora/confs/voting/verifyProposal_config.conf b/security/certora/confs/voting/verifyProposal_config.conf
@@ -28,7 +28,13 @@
     "loop_iter": "3",
     "optimistic_hashing": true,
     "solc": "solc8.19",
-    //"parametric_contracts":["VotingMachineHarness"
-    //],
+    "parametric_contracts": [
+        // Excluding DataWarehouse!
+        "VotingMachineHarness",
+        "VotingStrategyHarness",
+        "CrossChainController"
+    ],
+    "rule_sanity": "basic",
+    "build_cache": true,
     "msg": "VotingMachine - proposal configuration"
 }