review governance spec #22

nd-certora · 2023-11-22T07:52:08Z

my review:
notice that some comments are regarding the pdf verification report

security/certora/specs/Governance.spec

gadicer · 2023-11-23T15:40:57Z

security/certora/specs/Governance.spec

+   => getPayloadLength(proposalId) > 0
+
+  Can this be an issue? 
+  usually time dependnet properties should be proven as a rule 


Converted to rules

gadicer · 2023-11-23T15:47:52Z

security/certora/specs/Governance.spec

+
+getProposalStateVariable(proposalId) != getProposalState(e,proposalId)
+
+I see many of our rules are on getProposalState() and some are also on getProposalStateVariable() but when and why? 


We really need getProposalState() - that's the contract function that retrieves the state. All contract functions use this function.

getProposalStateVariable() is a getter to the storage. It's an extra check.

gadicer · 2023-11-26T10:25:28Z

security/certora/specs/Governance.spec

@@ -222,7 +246,10 @@ rule proposal_after_voting_portal_invalidate{
  IGovernanceCore.State state_after = getProposalState(e3, proposalId);

  assert !voting_portal_approved_after => (state_before != state_after => isTerminalState(state_after));
-
+  /* ND- what about the other direction


The 2 properties are equivalent.
P1: !voting_portal_approved_after => (state_before != state_after => isTerminalState(state_after))
P2: (state_before != state_after && !isTerminalState(state_after)) => voting_portal_approved_after
They have the same truth table.

voting_portal_approved_after | state_before != state_after | isTerminalState(state_after) | P1 | P2

0 | 0 | 0 | T | T 0 | 0 | 1 | T | T 0 | 1 | 0 | F | F 0 | 1 | 1 | T | T 1 | 0 | 0 | T | T 1 | 0 | 1 | T | T 1 | 1 | 0 | T | T 1 | 1 | 1 | T | T

not easy to see that so maybe just add a comment that this is also implied by this rule

security/certora/specs/Governance.spec

gadicer · 2023-11-26T13:44:15Z

security/certora/specs/Governance.spec

  require state1 != state2; 
  require creator_power <= voting_config_min_power;
  assert state2 == IGovernanceCore.State.Cancelled || state2 == IGovernanceCore.State.Failed;

 }

 //pass
+/* ND - is insufficient_proposition_power jsut a subcase of insufficient_proposition_power_allow_time_elapse? 
+ok to have both but maybe share the code in cvl function ? */


code shared

security/certora/specs/Governance.spec

gadicer · 2023-11-26T13:56:55Z

security/certora/specs/Governance.spec

@@ -266,7 +304,10 @@ rule insufficient_proposition_power_allow_time_elapse(method f) filtered { f ->
  state2 == IGovernanceCore.State.Cancelled || state2 == IGovernanceCore.State.Failed || state2 == IGovernanceCore.State.Expired;

 }
+/*
+ND: missign rule that only state_advancing_function are indeed such 


rule state_changing_function_self_check checks that

security/certora/specs/Governance.spec

gadicer · 2023-11-26T16:06:35Z

security/certora/specs/Governance.spec

@@ -283,17 +324,19 @@ rule insufficient_proposition_power_time_elapsed_tight_witness(method f) filtere

  require state1 != state2; 
  require creator_power <= (voting_config_min_power);
+  /* so you are looking for state2 == IGovernanceCore.State.Expired ? why not just satisfy that ? */


security/certora/specs/Governance.spec

nd-certora · 2023-11-27T10:49:45Z

Thinking about missing specs: I wonder if the following mutations will be caught:

in updateRepresentativesForChain move
_representatives[msg.sender][chainId] = newRepresentative; line 186 before:
address oldRepresentative = _representatives[msg.sender][chainId];
only_guardian_can_cancel has many cases so:
2.1 change

    proposalCreator != msg.sender &&
    _isPropositionPowerEnough(
      _votingConfigs[proposal.accessLevel],
      _powerStrategy.getFullPropositionPower(proposalCreator)
    ```
    to 
    ```
      isVotingPortalApproved(proposal.votingPortal) ||
    proposalCreator != msg.sender ||
    _isPropositionPowerEnough(
      _votingConfigs[proposal.accessLevel],
      _powerStrategy.getFullPropositionPower(proposalCreator)
    ```
2.2 remove onlyGuardian from rescueVotingPortal

gadicer · 2023-11-28T13:46:47Z

security/certora/specs/Governance.spec

@@ -668,7 +715,8 @@ filtered {f -> !f.isView}
  f(e2, args);
  uint40 voting_activation_time_after = getProposalVotingActivationTime(proposalId);
  bytes32 snapshot_blockhash_after = getProposalSnapshotBlockHash(proposalId);
-
+  /* ND - we are not proving the "can only be set once... " we are proving "can not be changed after activateVoting"
+  either rephrase of add a satisfy rule that shows it can be set */


Added satisfy.

gadicer · 2023-11-28T16:02:35Z

security/certora/specs/Governance.spec

@@ -725,7 +773,7 @@ rule proposal_executes_after_cooldown_period(){
 //              From its perspective, execution is sent to a Portal.
 //Property #18: VOTING_TOKENS_CAP in GovernanceCore should be big enough to account for tokens that need to pass multiple slots,
 //               and big enough for at least mig to long term
-
+// ND - what are the above 16 - 18 properties? 


Property #17 We summarize CrossChainForwarder.forwardMessage to NONDET. This function sends payloads to execution chain, and it's called by executeProposal(). I added a comment about the summarization to the "assumptions and simplifications" section of the report. So the property seems to hold.
Property #18: VOTING_TOKENS_CAP is not relevant anymore, the constant is not used now. I'll notify the customer.

gadicer · 2023-11-28T16:14:41Z

security/certora/specs/Governance.spec

 invariant cancellationFeeZeroForFutureProposals(uint256 proposalId) 
    proposalId >= getProposalCount() => getProposalCancellationFee(proposalId) == 0;

 // Property: eth balance can cover the total cancellation fee of users
 invariant totalCancellationFeeEqualETHBalance()
+// ND - the report regard fee of live proposals, this is all proposals, no? 


report is fixed

gadicer · 2023-11-28T16:18:57Z

security/certora/specs/Governance.spec

@@ -871,6 +921,7 @@ rule userFeeDidntChangeImplyNativeBalanceDidntDecrease(){
 //

 // A voter cannot represent himself
+// ND - this is not in the report, why? 


added to report

gadicer · 2023-11-28T18:44:54Z

security/certora/specs/Governance.spec

@@ -176,20 +196,20 @@ invariant creator_is_not_zero_2(uint256 proposalId)
 invariant empty_payloads_iff_uninitialized_proposal(uint256 proposalId)
      proposalId >= getProposalsCount() <=> getPayloadLength(proposalId) == 0;

+/* ND - this is just a subset of the above ? */


gadicer · 2023-11-28T18:49:22Z

security/certora/specs/Governance.spec

 invariant null_state_if_uninitialized_proposal(env e, uint256 proposalId)
      proposalId >= getProposalsCount() => getProposalState(e, proposalId) == IGovernanceCore.State.Null;
-
+/* ND - subset of null_state_variable_iff_uninitialized_proposal */


review governance spec

b1d04c9

nd-certora requested a review from gadicer November 22, 2023 07:52

gadicer reviewed Nov 23, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 23, 2023

View reviewed changes

gadicer reviewed Nov 26, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 26, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 26, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 26, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 26, 2023

View reviewed changes

security/certora/specs/Governance.spec Show resolved Hide resolved

gadicer reviewed Nov 28, 2023

View reviewed changes

gadicer merged commit 2a180c7 into certora Dec 11, 2023
1 check passed

nisnislevi deleted the nurit/review branch December 3, 2024 16:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

review governance spec #22

review governance spec #22

nd-certora commented Nov 22, 2023

gadicer Nov 23, 2023

gadicer Nov 23, 2023

gadicer Nov 26, 2023

nd-certora Nov 27, 2023

gadicer Nov 26, 2023 •

edited

Loading

gadicer Nov 26, 2023

gadicer Nov 26, 2023

nd-certora commented Nov 27, 2023

gadicer Nov 28, 2023

gadicer Nov 28, 2023

gadicer Nov 28, 2023

gadicer Nov 28, 2023

gadicer Nov 28, 2023

gadicer Nov 28, 2023


		getProposalStateVariable(proposalId) != getProposalState(e,proposalId)

		I see many of our rules are on getProposalState() and some are also on getProposalStateVariable() but when and why?

review governance spec #22

review governance spec #22

Conversation

nd-certora commented Nov 22, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

voting_portal_approved_after | state_before != state_after | isTerminalState(state_after) | P1 | P2

Choose a reason for hiding this comment

gadicer Nov 26, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nd-certora commented Nov 27, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gadicer Nov 26, 2023 •

edited

Loading