Feat/base delegation isolation cvl2

.github/workflows/certora.yml

@@ -17,11 +17,6 @@ jobs:
     steps:
       - uses: actions/checkout@v2
 
-      - name: Check key
-        env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
-        run: echo "key length" ${#CERTORAKEY}
-
       - name: Install python
         uses: actions/setup-python@v2
         with: { python-version: 3.9 }
@@ -46,7 +41,7 @@ jobs:
           make munged
           cd ..
           echo "key length" ${#CERTORAKEY}
-          sh certora/scripts/${{ matrix.rule }}
+          certoraRun certora/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -55,6 +50,8 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyGeneral.sh
-          - verifyDelegate.sh
-          - verifyCommunity.sh
+          - verifyGeneral.conf
+          - verifyDelegate.conf
+          - verifyCommunity.conf
+          - erc20.conf
+

certora/applyHarness.patch

@@ -1,69 +1,74 @@
 diff -ruN .gitignore .gitignore
---- .gitignore	1970-01-01 02:00:00
-+++ .gitignore	2023-03-29 13:05:55
+--- .gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2023-06-22 20:09:19.161398598 +0300
 @@ -0,0 +1,2 @@
 +*
 +!.gitignore
 \ No newline at end of file
-diff -ruN src/AaveTokenV3.sol src/AaveTokenV3.sol
---- src/AaveTokenV3.sol	2023-03-29 13:12:02
-+++ src/AaveTokenV3.sol	2023-03-29 13:07:15
-@@ -215,7 +215,7 @@
-         fromBalanceAfter = fromUserState.balance - uint104(amount);
-       }
-       _balances[from].balance = fromBalanceAfter;
--      if (fromUserState.delegationState != DelegationState.NO_DELEGATION) {
-+      if (fromUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) {
+diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol
+--- src/BaseAaveToken.sol	2023-06-25 18:38:16.779424218 +0300
++++ src/BaseAaveToken.sol	2023-06-25 18:14:50.283889216 +0300
+@@ -12,7 +12,7 @@
+     uint104 balance;
+     uint72 delegatedPropositionBalance;
+     uint72 delegatedVotingBalance;
+-    DelegationMode delegationMode;
++    uint8 delegationMode;
+   }
+
+   mapping(address => DelegationAwareBalance) internal _balances;
+diff -ruN src/BaseDelegation.sol src/BaseDelegation.sol
+--- src/BaseDelegation.sol	2023-06-25 18:38:16.779424218 +0300
++++ src/BaseDelegation.sol	2023-06-25 18:37:40.099385958 +0300
+@@ -22,7 +22,7 @@
+   struct DelegationState {
+     uint72 delegatedPropositionBalance;
+     uint72 delegatedVotingBalance;
+-    DelegationMode delegationMode;
++    uint8 delegationMode;
+   }
+
+   mapping(address => address) internal _votingDelegatee;
+@@ -262,7 +262,7 @@
+     if (from != address(0)) {
+       DelegationState memory fromUserState = _getDelegationState(from);
+       uint256 fromBalanceAfter = fromBalanceBefore - amount;
+-      if (fromUserState.delegationMode != DelegationMode.NO_DELEGATION) {
++      if (fromUserState.delegationMode != uint8(DelegationMode.NO_DELEGATION)) {
          _governancePowerTransferByType(
-           fromUserState.balance,
+           fromBalanceBefore,
            fromBalanceAfter,
-@@ -237,7 +237,7 @@
-       toUserState.balance = toBalanceBefore + uint104(amount);
-       _balances[to] = toUserState;
+@@ -282,7 +282,7 @@
+       DelegationState memory toUserState = _getDelegationState(to);
+       uint256 toBalanceAfter = toBalanceBefore + amount;
 
--      if (toUserState.delegationState != DelegationState.NO_DELEGATION) {
-+      if (toUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) {
+-      if (toUserState.delegationMode != DelegationMode.NO_DELEGATION) {
++      if (toUserState.delegationMode != uint8(DelegationMode.NO_DELEGATION)) {
          _governancePowerTransferByType(
            toBalanceBefore,
-           toUserState.balance,
-@@ -293,7 +293,7 @@
+           toBalanceAfter,
+@@ -338,7 +338,7 @@
            : address(0);
      }
      return
--      userState.delegationState >= DelegationState.PROPOSITION_DELEGATED
-+      userState.delegationState >= uint8(DelegationState.PROPOSITION_DELEGATED)
-         ? _propositionDelegateeV2[delegator]
+-      userState.delegationMode >= DelegationMode.PROPOSITION_DELEGATED
++      userState.delegationMode >= uint8(DelegationMode.PROPOSITION_DELEGATED)
+         ? _propositionDelegatee[delegator]
          : address(0);
    }
-@@ -330,16 +330,12 @@
-   ) internal pure returns (DelegationAwareBalance memory) {
+@@ -375,13 +375,13 @@
+   ) internal pure returns (DelegationState memory) {
      if (willDelegate) {
        // Because GovernancePowerType starts from 0, we should add 1 first, then we apply bitwise OR
--      userState.delegationState = DelegationState(
--        uint8(userState.delegationState) | (uint8(delegationType) + 1)
--      );
-+      userState.delegationState = userState.delegationState | (uint8(delegationType) + 1);
+-      userState.delegationMode = DelegationMode(
++      userState.delegationMode = uint8 (
+         uint8(userState.delegationMode) | (uint8(delegationType) + 1)
+       );
      } 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.delegationState = DelegationState(
--        uint8(userState.delegationState) &
--          ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED))
--      );
-+      userState.delegationState = userState.delegationState &
-+          ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED));
-     }
-     return userState;
-   }
-diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol
---- src/BaseAaveToken.sol	2023-03-29 13:12:02
-+++ src/BaseAaveToken.sol	2023-03-29 13:07:15
-@@ -18,7 +18,7 @@
-     uint104 balance;
-     uint72 delegatedPropositionBalance;
-     uint72 delegatedVotingBalance;
--    DelegationState delegationState;
-+    uint8 delegationState; // refactored from enum
-   }
-
-   mapping(address => DelegationAwareBalance) internal _balances;
+-      userState.delegationMode = DelegationMode(
++      userState.delegationMode = uint8(
+         uint8(userState.delegationMode) &
+           ((uint8(delegationType) + 1) ^ uint8(DelegationMode.FULL_POWER_DELEGATED))
+       );

certora/conf/community.conf

@@ -0,0 +1,14 @@
+{
+    "files": [
+        "certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness"
+    ],
+    "optimistic_loop": true,
+    "packages": [
+        "openzeppelin-contracts=lib/openzeppelin-contracts"
+    ],
+    "cloud": "",
+    "process": "emv",
+    "solc": "solc8.13",
+    "verify": "AaveTokenV3Harness:certora/specs/community.spec",
+    "msg": "AaveTokenV3HarnessCommunity:community.spec "
+}

certora/conf/delegate.conf

@@ -0,0 +1,14 @@
+{
+    "files": [
+        "certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness"
+    ],
+    "cloud": "",
+    "optimistic_loop": true,
+    "packages": [
+        "openzeppelin-contracts=lib/openzeppelin-contracts"
+    ],
+    "process": "emv",
+    "solc": "solc8.13",
+    "verify": "AaveTokenV3Harness:certora/specs/delegate.spec",
+    "msg": "AaveTokenV3Harness:delegate.spec "
+}

certora/conf/erc20.conf

@@ -0,0 +1,14 @@
+{
+    "files": [
+        "certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness"
+    ],
+    "packages": [
+        "openzeppelin-contracts=lib/openzeppelin-contracts"
+    ],
+    "cloud": "",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.13",
+    "verify": "AaveTokenV3Harness:certora/specs/erc20.spec",
+    "msg": "AaveTokenV3:erc20.spec "
+}

certora/conf/general.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness"
+    ],
+    "packages": [
+        "openzeppelin-contracts=lib/openzeppelin-contracts"
+    ],
+    "cloud": "",
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [" -smt_bitVectorTheory true"],
+    "solc": "solc8.13",
+    "verify": "AaveTokenV3Harness:certora/specs/general.spec",
+    "msg": "AaveTokenV3:general.spec "
+}

certora/harness/AaveTokenV3Harness.sol

@@ -9,6 +9,7 @@
 pragma solidity ^0.8.0;
 
 import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
+import {DelegationMode} from '../../src/DelegationAwareBalance.sol';
 
 contract AaveTokenV3Harness is AaveTokenV3 {
   // returns user's token balance, used in some community rules
@@ -29,15 +30,15 @@ contract AaveTokenV3Harness is AaveTokenV3 {
   //returns user's delegating proposition status
   function getDelegatingProposition(address user) public view returns (bool) {
     return
-      _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
-      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+      _balances[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED ||
+      _balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
   }
 
   // returns user's delegating voting status
   function getDelegatingVoting(address user) public view returns (bool) {
     return
-      _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
-      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+      _balances[user].delegationMode == DelegationMode.VOTING_DELEGATED ||
+      _balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
   }
 
   // returns user's voting delegate
@@ -51,7 +52,7 @@ contract AaveTokenV3Harness is AaveTokenV3 {
   }
 
   // returns user's delegation state
-  function getDelegationState(address user) public view returns (DelegationMode) {
-    return _balances[user].delegationState;
+  function getDelegationMode(address user) public view returns (DelegationMode) {
+    return _balances[user].delegationMode;
   }
 }