Certora

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

@@ -28,13 +28,13 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==7.20.3
+        run: pip3 install certora-cli==7.21.1
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
+          sudo mv solc-static-linux /usr/local/bin/solc8.20
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
@@ -47,27 +47,4 @@ jobs:
       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
+          - 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 executor_exists_if_action_not_null executor_exists_only_if_action_not_null  payload_delay_within_range  delay_of_executor_of_max_access_level_within_range  nonempty_actions  executor_exists_iff_action_not_null  null_access_level_iff_state_is_none  executor_of_maximumAccessLevelRequired_exists  executor_of_maximumAccessLevelRequired_exists_after_createPayload   action_access_level_isnt_null_after_createPayload  executor_exists_after_createPayload  action_callData_immutable  action_signature_immutable  action_immutable_check_only_fixed_size_fields  zero_executedAt_if_not_executed  executor_isnt_used_twice executor_of_level_null_is_zero  executed_after_queue_state_variable zero_executedAt_if_not_executed_state_variable  queuedAt_is_zero_before_queued_state_variable executedAt_is_zero_before_executed_state_variable null_state_equivalence  executedAt_is_zero_before_executed  executed_when_in_queued_state executed_when_in_queued_state_variable guardian_can_cancel no_late_cancel state_variable_cant_decrease  checkUpdateExecutors checkUpdateExecutors_witness_1 checkUpdateExecutors_witness_2 checkUpdateExecutors_witness_3 checkUpdateExecutors_witness_4  payload_state_transition_post_state payload_state_transition_pre_state

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

@@ -30,13 +30,13 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==7.20.3
+        run: pip3 install certora-cli==7.21.1
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
+          sudo mv solc-static-linux /usr/local/bin/solc8.20
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
@@ -50,26 +50,6 @@ jobs:
       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 
+          - verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance transferPowerCompliance powerlessCompliance method_reachability
+          - verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal  no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal  no_representative_is_zero_2 no_representative_of_zero  state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease  check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives  at_least_single_payload_active empty_payloads_iff_uninitialized_proposal  null_state_iff_uninitialized_proposal setInvariant addressSetInvariant  state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period  only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_after_creation only_guardian_can_cancel guardian_can_cancel  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  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  creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence  insufficient_proposition_power_witness_time_elapsed  immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal  immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash  immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state  only_state_changing_function_initiate_transitions__post_state  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  proposal_voting_duration_lt_expiration_time config_voting_duration_lt_expiration_time proposal_state_transition_post_state proposal_state_transition_pre_state
           - 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/workflows/certora-review-voting-chain.yml

@@ -30,13 +30,13 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==7.20.3
+        run: pip3 install certora-cli==7.21.1
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
+          sudo mv solc-static-linux /usr/local/bin/solc8.20
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
@@ -49,38 +49,13 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyLegality.conf --rule createdVoteHasNonZeroHash
-          - verifyLegality.conf --rule votedPowerIsImmutable
-          - verifyLegality.conf --rule onlyValidProposalCanChangeTally
-          - verifyLegality.conf --rule legalVote
-          - verifyLegality.conf --rule method_reachability
+          - verifyLegality.conf --rule createdVoteHasNonZeroHash  votedPowerIsImmutable  onlyValidProposalCanChangeTally  legalVote  method_reachability
           - verifyMisc.conf
-          - 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 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 startsStrictlyBeforeEnds
-          - verifyProposal_states.conf --rule proposalLegalStates
-          - verifyProposal_states.conf --rule proposalMethodStateTransitionCompliance
-          - 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 onlyVoteCanChangeResult
-          - 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
+          - verifyPower_summary.conf --rule onlyThreeTokens method_reachability
+          - verifyProposal_config.conf --rule startedProposalHasConfig  createdProposalHasRoots  proposalHasNonzeroDuration newProposalUnusedId configIsImmutable  getProposalsConfigsDoesntRevert  method_reachability 
+          - verifyProposal_states.conf --rule startsBeforeEnds  startsStrictlyBeforeEnds  proposalLegalStates  proposalMethodStateTransitionCompliance  proposalTimeStateTransitionCompliance  proposalIdIsImmutable  proposalImmutability  startedProposalHasConfig  proposalHasNonzeroDuration method_reachability 
+          - verifyVoting_and_tally.conf --rule votingPowerGhostIsVotingPower  sumOfVotes  voteTallyChangedOnlyByVoting  voteUpdatesTally  onlyVoteCanChangeResult  votingTallyCanOnlyIncrease  strangerVoteUnchanged  otherProposalUnchanged  otherVoterUntouched  method_reachability
+          - 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 cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote
-          - verifyVoting_and_tally.conf --rule method_reachability
+

.gitmodules

@@ -1,21 +1,4 @@
-[submodule "lib/forge-std"]
-	path = lib/forge-std
-	url = https://github.com/foundry-rs/forge-std
-[submodule "lib/solidity-utils"]
-	path = lib/solidity-utils
-	url = https://github.com/bgd-labs/solidity-utils
-	branch = feat/zksync
-[submodule "lib/aave-token-v3"]
-	path = lib/aave-token-v3
-	url = https://github.com/bgd-labs/aave-token-v3
-[submodule "lib/openzeppelin-contracts"]
-	path = lib/openzeppelin-contracts
-	url = https://github.com/OpenZeppelin/openzeppelin-contracts
-	branch = release-v4.9
-[submodule "lib/aave-address-book"]
-	path = lib/aave-address-book
-	url = https://github.com/bgd-labs/aave-address-book
-[submodule "lib/aave-delivery-infrastructure"]
-	path = lib/aave-delivery-infrastructure
-	url = https://github.com/bgd-labs/aave-delivery-infrastructure
-	branch = feat/zksync
+[submodule "lib/adi-deploy"]
+	path = lib/adi-deploy
+	url = https://github.com/bgd-labs/adi-deploy
+	branch = feat/deploy-celo

Makefile

@@ -100,7 +100,7 @@ write-json-addresses :; forge script scripts/WriteAddresses.s.sol:WriteDeployedA
 
 
 deploy-initial-test:
-	$(call deploy_fn,InitialDeployments,zksync)
+	$(call deploy_fn,InitialDeployments,celo)
 
 # Deploy Governance contracts
 deploy-governance-test:
@@ -131,7 +131,7 @@ deploy-executor-lvl2-test:
 
 ## Deploy execution chain contracts
 deploy-payloads-controller-chain-test:
-	$(call deploy_fn,Payloads/Deploy_PayloadsController,zksync)
+	$(call deploy_fn,Payloads/Deploy_PayloadsController,celo)
 
 ## Deploy Governance Voting Portal
 deploy-voting-portals-test:
@@ -148,7 +148,7 @@ set-vp-as_ccf-senders-test:
 
 ## Deploy Contract Helpers
 deploy-helper-contracts-test:
-	$(call deploy_fn,Deploy_ContractHelpers,zksync)
+	$(call deploy_fn,Deploy_ContractHelpers,celo)
 
 deploy-full-key-test:
 		make deploy-initial-test