Merge pull request #38 from Certora/certora-squash

Certora review
bgd-labs · Oct 19, 2023 · ec80c6d · ec80c6d
2 parents 874ffdb + 2270a94
commit ec80c6d
Show file tree

Hide file tree

Showing 12 changed files with 717 additions and 58 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -28,7 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli-beta
+        run: pip3 install certora-cli
 
       - name: Install solc
         run: |

diff --git a/certora/Makefile b/certora/Makefile
@@ -14,6 +14,8 @@ help:
 munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
 	rm -rf $@
 	mkdir $@
+	cp -r ../lib $@
+	cp -r ../src $@
 	patch -p0 -d $@ < $(PATCH)
 
 record:

diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
@@ -1,7 +1,73 @@
 diff -ruN .gitignore .gitignore
 --- .gitignore	1970-01-01 02:00:00.000000000 +0200
-+++ .gitignore	2023-06-29 18:12:58.710152977 +0300
++++ .gitignore	2023-10-16 10:27:06.956167787 +0300
 @@ -0,0 +1,2 @@
 +*
 +!.gitignore
 \ No newline at end of file
+diff -ruN src/BaseDelegation.sol src/BaseDelegation.sol
+--- src/BaseDelegation.sol	2023-10-16 10:27:36.664745617 +0300
++++ src/BaseDelegation.sol	2023-10-16 10:27:31.640648129 +0300
+@@ -374,17 +374,31 @@
+     bool willDelegate
+   ) internal pure returns (DelegationState memory) {
+     if (willDelegate) {
+-      // Because GovernancePowerType starts from 0, we should add 1 first, then we apply bitwise OR
+-      userState.delegationMode = DelegationMode(
+-        uint8(userState.delegationMode) | (uint8(delegationType) + 1)
+-      );
++      if (delegationType == GovernancePowerType.VOTING) {
++          if (userState.delegationMode==DelegationMode.NO_DELEGATION)
++              userState.delegationMode = DelegationMode.VOTING_DELEGATED;
++          else if (userState.delegationMode==DelegationMode.PROPOSITION_DELEGATED)
++              userState.delegationMode = DelegationMode.FULL_POWER_DELEGATED;
++      }
++      else if (delegationType == GovernancePowerType.PROPOSITION) {
++          if (userState.delegationMode==DelegationMode.NO_DELEGATION)
++              userState.delegationMode = DelegationMode.PROPOSITION_DELEGATED;
++          else if (userState.delegationMode==DelegationMode.VOTING_DELEGATED)
++              userState.delegationMode = DelegationMode.FULL_POWER_DELEGATED;
++      }
+     } else {
+-      // First bitwise NEGATION, ie was 01, after XOR with 11 will be 10,
+-      // then bitwise AND, which means it will keep only another delegation type if it exists
+-      userState.delegationMode = DelegationMode(
+-        uint8(userState.delegationMode) &
+-          ((uint8(delegationType) + 1) ^ uint8(DelegationMode.FULL_POWER_DELEGATED))
+-      );
++      if (delegationType == GovernancePowerType.VOTING) {
++          if (userState.delegationMode==DelegationMode.VOTING_DELEGATED)
++              userState.delegationMode = DelegationMode.NO_DELEGATION;
++          else if (userState.delegationMode==DelegationMode.FULL_POWER_DELEGATED)
++              userState.delegationMode = DelegationMode.PROPOSITION_DELEGATED;
++      }
++      else if (delegationType == GovernancePowerType.PROPOSITION) {
++          if (userState.delegationMode==DelegationMode.PROPOSITION_DELEGATED)
++              userState.delegationMode = DelegationMode.NO_DELEGATION;
++          else if (userState.delegationMode==DelegationMode.FULL_POWER_DELEGATED)
++              userState.delegationMode = DelegationMode.VOTING_DELEGATED;
++      }
+     }
+     return userState;
+   }
+@@ -425,7 +439,11 @@
+
+     _updateDelegateeByType(delegator, delegationType, delegatee);
+
++    ___willDelegateAfter = willDelegateAfter;
++    ___delegatingNow = delegatingNow;
++    
+     if (willDelegateAfter != delegatingNow) {
++        ___delegationState = _updateDelegationModeByType(delegatorState, delegationType, willDelegateAfter);
+       _setDelegationState(
+         delegator,
+         _updateDelegationModeByType(delegatorState, delegationType, willDelegateAfter)
+@@ -434,4 +452,8 @@
+
+     emit DelegateChanged(delegator, delegatee, delegationType);
+   }
++
++  DelegationState ___delegationState;
++  bool ___willDelegateAfter;
++  bool ___delegatingNow;
+ }
diff --git a/certora/conf/delegate.conf b/certora/conf/delegate.conf
@@ -1,14 +1,17 @@
 {
     "files": [
-        "certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness"
+        "certora/harness/AaveTokenV3Harness.sol"
     ],
     "cloud": "",
     "optimistic_loop": true,
     "packages": [
-        "openzeppelin-contracts=lib/openzeppelin-contracts"
+        "openzeppelin-contracts=certora/munged/lib/openzeppelin-contracts"
     ],
+//    "prover_args": ["-smt_bitVectorTheory true","-depth 15","-mediumTimeout 1000"],
+//    "smt_timeout": "2000",
     "process": "emv",
     "solc": "solc8.13",
+    "rule_sanity": "basic",  // rule_sanity accepts: none, basic, advance
     "verify": "AaveTokenV3Harness:certora/specs/delegate.spec",
     "msg": "AaveTokenV3Harness:delegate.spec "
 }
diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol
@@ -8,8 +8,8 @@
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
-import {DelegationMode} from '../../src/DelegationAwareBalance.sol';
+import {AaveTokenV3} from '../munged/src/AaveTokenV3.sol';
+import {DelegationMode} from '../munged/src/DelegationAwareBalance.sol';
 
 contract AaveTokenV3Harness is AaveTokenV3 {
   // returns user's token balance, used in some community rules
@@ -42,17 +42,25 @@ contract AaveTokenV3Harness is AaveTokenV3 {
   }
 
   // returns user's voting delegate
-  function getVotingDelegate(address user) public view returns (address) {
-    return _votingDelegatee[user];
+  function getVotingDelegatee(address user) public view returns (address) {
+      //return _getDelegateeByType(user, _getDelegationState(user), GovernancePowerType.VOTING);
+      return _votingDelegatee[user];
   }
 
   // returns user's proposition delegate
-  function getPropositionDelegate(address user) public view returns (address) {
+  function getPropositionDelegatee(address user) public view returns (address) {
     return _propositionDelegatee[user];
   }
 
   // returns user's delegation state
   function getDelegationMode(address user) public view returns (DelegationMode) {
     return _balances[user].delegationMode;
   }
+
+  function getDelegatedPowerVoting(address user) public view returns (uint256) {
+      DelegationState memory userState = _getDelegationState(user);
+      uint256 userDelegatedPower = _getDelegatedPowerByType(userState, GovernancePowerType.VOTING);
+
+      return userDelegatedPower;
+  }
 }
diff --git a/certora/harness/AaveTokenV3HarnessCommunity.sol b/certora/harness/AaveTokenV3HarnessCommunity.sol
@@ -37,11 +37,11 @@ contract AaveTokenV3Harness is AaveTokenV3 {
       _balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
   }
 
-  function getVotingDelegate(address user) public view returns (address) {
+  function getVotingDelegatee(address user) public view returns (address) {
     return _votingDelegatee[user];
   }
 
-  function getPropositionDelegate(address user) public view returns (address) {
+  function getPropositionDelegatee(address user) public view returns (address) {
     return _propositionDelegatee[user];
   }
 

diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol
@@ -42,11 +42,11 @@ contract AaveTokenV3Harness is AaveTokenV3 {
       state == uint8(DelegationMode.FULL_POWER_DELEGATED);
   }
 
-  function getVotingDelegate(address user) public view returns (address) {
+  function getVotingDelegatee(address user) public view returns (address) {
     return _votingDelegatee[user];
   }
 
-  function getPropositionDelegate(address user) public view returns (address) {
+  function getPropositionDelegatee(address user) public view returns (address) {
     return _propositionDelegatee[user];
   }
 

diff --git a/certora/specs/base.spec b/certora/specs/base.spec
@@ -31,8 +31,8 @@ methods {
     function getDelegatedVotingBalance(address user) external returns (uint72) envfree;
     function getDelegatingProposition(address user) external returns (bool) envfree;
     function getDelegatingVoting(address user) external returns (bool) envfree;
-    function getVotingDelegate(address user) external returns (address) envfree;
-    function getPropositionDelegate(address user) external returns (address) envfree;
+    function getVotingDelegatee(address user) external returns (address) envfree;
+    function getPropositionDelegatee(address user) external returns (address) envfree;
     function getDelegationMode(address user) external returns (AaveTokenV3Harness.DelegationMode) envfree;
 }
 

diff --git a/certora/specs/community.spec b/certora/specs/community.spec
@@ -193,17 +193,17 @@ rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, a
     require e.msg.sender != alice && e.msg.sender != bob;
     require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS();
 
-    require getVotingDelegate(e.msg.sender) != alice;
+    require getVotingDelegatee(e.msg.sender) != alice;
 
     uint72 _votingBalance = getDelegatedVotingBalance(alice);
 
     delegateByType(e, alice, VOTING_POWER());
 
-    assert getVotingDelegate(e.msg.sender) == alice;
+    assert getVotingDelegatee(e.msg.sender) == alice;
 
     delegateByType(e, bob, VOTING_POWER());
 
-    assert getVotingDelegate(e.msg.sender) == bob;
+    assert getVotingDelegatee(e.msg.sender) == bob;
     uint72 votingBalance_ = getDelegatedVotingBalance(alice);
     assert alice != bob => votingBalance_ == _votingBalance;
 }
@@ -268,13 +268,13 @@ rule powerChanges(address alice, method f) {
 
     @Formula:
     {
-        delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender)
+        delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegatee(e.msg.sender)
     }
     <
         delegateByType(e, delegatee, 1 - type)
     >
     {
-       delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender)
+       delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegatee(e.msg.sender)
        delegateBefore == delegateAfter
     }
 
@@ -288,12 +288,12 @@ rule delegateIndependence(method f) {
 
     IGovernancePowerDelegationToken.GovernancePowerType type;
 
-    address delegateBefore = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender);
+    address delegateBefore = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegatee(e.msg.sender) : getVotingDelegatee(e.msg.sender);
 
     IGovernancePowerDelegationToken.GovernancePowerType otherType = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? IGovernancePowerDelegationToken.GovernancePowerType.VOTING : IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION;
     delegateByType(e, _, otherType);
 
-    address delegateAfter = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender);
+    address delegateAfter = type == IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION ? getPropositionDelegatee(e.msg.sender) : getVotingDelegatee(e.msg.sender);
 
     assert delegateBefore == delegateAfter;
 }