all rules are running except 2 from executionchain that get timeout

security/certora/confs/verifyGovernance.conf

@@ -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",
 }

security/certora/confs/verifyGovernancePowerStrategy.conf

@@ -24,5 +24,6 @@
     "solc": "solc8.19",
     "smt_timeout": "6000",
     "rule_sanity": "basic",
+    "build_cache": true,
     "msg": "GovernancePowerStrategy tests"
 }

security/certora/confs/verifyVotingStrategy_unittests.conf

@@ -21,5 +21,6 @@
     "loop_iter": "3",  // Needs 2 for isTokenSlotAccepted (A_AAVE uses 2 slots)
     "solc": "solc8.19",
     "rule_sanity": "basic",
+    "build_cache": true,
     "msg": "VotingStrategy tests"
 }

security/certora/scripts/run-all-mainnet.sh

@@ -0,0 +1,122 @@
+#CMN="--compilation_steps_only"
+
+
+
+echo "******** Running:  mainnet 1 ***************"
+certoraRun $CMN security/certora/confs/verifyVotingStrategy_unittests.conf \
+           --msg "mainnet 1 "
+
+echo "******** Running:  mainnet 2 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernancePowerStrategy.conf --rule delegatePowerCompliance  \
+           --msg "mainnet 2 "
+
+
+echo "******** Running:  mainnet 3 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernancePowerStrategy.conf --rule transferPowerCompliance \
+           --msg "mainnet 3 "
+
+
+echo "******** Running:  mainnet 4 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernancePowerStrategy.conf --rule powerlessCompliance method_reachability \
+           --msg "mainnet 4 "
+
+
+echo "******** Running:  mainnet 5 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal \
+           --msg "mainnet 5 "
+
+
+echo "******** Running:  mainnet 6 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule no_self_representative no_representative_is_zero consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal \
+           --msg "mainnet 6 "
+
+
+echo "******** Running:  mainnet 7 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero \
+           --msg "mainnet 7 "
+
+
+echo "******** Running:  mainnet 8 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule state_changing_function_self_check state_variable_changing_function_self_check method_reachability userFeeDidntChangeImplyNativeBalanceDidntDecrease \
+           --msg "mainnet 8 "
+
+
+echo "******** Running:  mainnet 9 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives \
+           --msg "mainnet 9 "
+
+
+echo "******** Running:  mainnet 10 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule at_least_single_payload_active empty_payloads_iff_uninitialized_proposal \
+           --msg "mainnet 10 "
+
+
+echo "******** Running:  mainnet 11 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule null_state_iff_uninitialized_proposal setInvariant addressSetInvariant \
+           --msg "mainnet 11 "
+
+
+echo "******** Running:  mainnet 12 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period \
+           --msg "mainnet 12 "
+
+
+echo "******** Running:  mainnet 13 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 13 "
+
+
+echo "******** Running:  mainnet 14 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 14 "
+
+
+echo "******** Running:  mainnet 15 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 15 "
+
+
+echo "******** Running:  mainnet 16 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 16 "
+
+
+echo "******** Running:  mainnet 17 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule creator_is_not_zero creator_of_initialized_proposal_is_not_zero null_state_equivalence \
+           --msg "mainnet 17 "
+
+
+echo "******** Running:  mainnet 18 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule insufficient_proposition_power_witness_time_elapsed \
+           --msg "mainnet 18 "
+
+
+echo "******** Running:  mainnet 19 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_creator immutable_after_creation_witness_voting_portal \
+           --msg "mainnet 19 "
+
+
+echo "******** Running:  mainnet 20 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_access_level immutable_after_creation_witness_creation_time immutable_after_creation_witness_ipfs_hash \
+           --msg "mainnet 20 "
+
+
+echo "******** Running:  mainnet 21 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule immutable_after_creation_witness_payload_length immutable_after_activation_witness only_state_changing_function_initiate_transitions__pre_state \
+           --msg "mainnet 21 "
+
+
+echo "******** Running:  mainnet 22 ***************"
+certoraRun $CMN security/certora/confs/verifyGovernance.conf --rule only_state_changing_function_initiate_transitions__post_state \
+           --msg "mainnet 22 "
+
+
+echo "******** Running:  mainnet 23 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 23 "
+
+
+echo "******** Running:  mainnet 24 ***************"
+certoraRun $CMN 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 \
+           --msg "mainnet 24 "
+

security/certora/specs/Governance.spec

@@ -62,20 +62,20 @@ methods {
   function isRepresentativeOfVoter(address,address,uint256) external returns (bool) envfree;
 }
 
-ghost mapping(uint256 => mapping(address => mapping(IGovernancePowerDelegationToken.GovernancePowerType => uint256))) user_type_power;
+persistent ghost mapping(uint256 => mapping(address => mapping(IGovernancePowerDelegationToken.GovernancePowerType => uint256))) user_type_power;
 
 function get_fixed_user_and_type_power(env e, address user, IGovernancePowerDelegationToken.GovernancePowerType type) returns uint256{
   return user_type_power[e.block.timestamp][user][type];
 }
 
 
-ghost mathint totalCancellationFee{
+persistent ghost mathint totalCancellationFee{
     init_state axiom totalCancellationFee == 0;
 }
-ghost bool isCancellationChanged;
+persistent ghost bool isCancellationChanged;
 
 hook Sstore _proposals[KEY uint256 proposalId].cancellationFee uint256 newFee
-    (uint256 oldFee) STORAGE
+    (uint256 oldFee) 
 {
     if (newFee != oldFee){
         isCancellationChanged = true;
@@ -1260,10 +1260,11 @@ filtered { f -> !state_changing_function(f)}
 
 
 // self-check - all external functions are reachability
-rule method_reachability {
+rule method_reachability(method f)
+filtered {f -> f.contract == currentContract}
+{
   env e;
   calldataarg arg;
-  method f;
 
   f(e, arg);
   satisfy true;

security/certora/specs/VotingStrategy_unittests.spec

@@ -190,10 +190,11 @@ rule wrongAssetYieldsZeroPower(
 }
 
 // setup self check - reachability of currentContract external functions
-rule method_reachability {
+rule method_reachability(method f)
+filtered {f -> f.contract == currentContract}
+{
   env e;
   calldataarg arg;
-  method f;
   f(e, arg);
   satisfy true;
 }

security/certora/specs/votersRepresentedAddressSet.spec

@@ -90,15 +90,15 @@ definition ARRAY_OUT_OF_BOUND_ZERO() returns bool = forall address rep. forall u
 /**
  * ghost mirror map, mimics Set map
  **/
-ghost mapping(address => mapping(uint256 => mapping(bytes32 => uint256))) mirrorMap{ 
+persistent ghost mapping(address => mapping(uint256 => mapping(bytes32 => uint256))) mirrorMap{ 
     init_state axiom forall address rep. forall uint256 chain. forall bytes32 a. mirrorMap[rep][chain][a] == 0;
 
 }
 
 /**
  * ghost mirror array, mimics Set array
  **/
-ghost mapping(address => mapping(uint256 => mapping(uint256 => bytes32))) mirrorArray{
+persistent ghost mapping(address => mapping(uint256 => mapping(uint256 => bytes32))) mirrorArray{
     init_state axiom forall address rep. forall uint256 chain. forall uint256 i. mirrorArray[rep][chain][i] == to_bytes32(0);
 }
 
@@ -109,7 +109,7 @@ ghost mapping(address => mapping(uint256 => mapping(uint256 => bytes32))) mirror
   * The assumption holds: breaking the assumptions would violate the invariant condition 'map(array(index)) == index + 1'. Set map uses 0 as a sentinel value, so the array cannot contain MAX_INT different values.  
   * The assumption is necessary: if a value is added when length==MAX_INT then length overflows and becomes zero.
  **/
-ghost mapping(address => mapping(uint256 => uint256)) mirrorArrayLen{
+persistent ghost mapping(address => mapping(uint256 => uint256)) mirrorArrayLen{
     init_state axiom forall address rep. forall uint256 chain. mirrorArrayLen[rep][chain] == 0;
     axiom forall address rep. forall uint256 chain. mirrorArrayLen[rep][chain] < max_uint256;
 }
@@ -119,46 +119,46 @@ ghost mapping(address => mapping(uint256 => uint256)) mirrorArrayLen{
  * hook for Set array stores
  * @dev user of this spec must replace _list with the instance name of the Set.
  **/
-hook Sstore _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 0)[INDEX uint256 index] bytes32 newValue (bytes32 oldValue) STORAGE {
+hook Sstore _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 0)[INDEX uint256 index] bytes32 newValue (bytes32 oldValue) {
     mirrorArray[rep][chain][index] = newValue;
 }
 
 /**
  * hook for Set array loads
  * @dev user of this spec must replace _list with the instance name of the Set.
  **/
-hook Sload bytes32 value _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 0)[INDEX uint256 index] STORAGE {
+hook Sload bytes32 value _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 0)[INDEX uint256 index] {
     require(mirrorArray[rep][chain][index] == value);
 }
 /**
  * hook for Set map stores
  * @dev user of this spec must replace _list with the instance name of the Set.
  **/
-hook Sstore _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 32)[KEY bytes32 key] uint256 newIndex (uint256 oldIndex) STORAGE {
+hook Sstore _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 32)[KEY bytes32 key] uint256 newIndex (uint256 oldIndex) {
       mirrorMap[rep][chain][key] = newIndex;
 }
 
 /**
  * hook for Set map loads
  * @dev user of this spec must replace _list with the instance name of the Set.
  **/
-hook Sload uint256 index _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 32)[KEY bytes32 key] STORAGE {
+hook Sload uint256 index _votersRepresented [KEY address rep] [KEY uint256 chain] .(offset 32)[KEY bytes32 key] {
     require(mirrorMap[rep][chain][key] == index);
 }
 
 /**
  * hook for Set array length stores
  * @dev user of this spec must replace _list with the instance name of the Set.
  **/
-hook Sstore _votersRepresented  [KEY address rep] [KEY uint256 chain] .(offset 0).(offset 0) uint256 newLen (uint256 oldLen) STORAGE {
+hook Sstore _votersRepresented  [KEY address rep] [KEY uint256 chain] .(offset 0).(offset 0) uint256 newLen (uint256 oldLen) {
         mirrorArrayLen[rep][chain] = newLen;
 }
 
 /**
  * hook for Set array length load
  * @dev user of this spec must replace _votersRepresented with the instance name of the Set.
  **/
-hook Sload uint256 len _votersRepresented  [KEY address rep] [KEY uint256 chain] .(offset 0).(offset 0) STORAGE {
+hook Sload uint256 len _votersRepresented  [KEY address rep] [KEY uint256 chain] .(offset 0).(offset 0) {
     require mirrorArrayLen[rep][chain] == len;
 }