Merge pull request #30 from Certora/certora_squash_2

Certora Review CVL2

.github/workflows/certora.yml

@@ -16,11 +16,8 @@ jobs:
 
     steps:
       - uses: actions/checkout@v2
-
-      - name: Check key
-        env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
-        run: echo "key length" ${#CERTORAKEY}
+        with:
+          submodules: recursive
 
       - name: Install python
         uses: actions/setup-python@v2
@@ -31,7 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli
+        run: pip3 install certora-cli-beta
 
       - name: Install solc
         run: |
@@ -46,7 +43,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 +52,8 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyGeneral.sh
-          - verifyDelegate.sh
-          - verifyCommunity.sh
+          - general.conf
+          - delegate.conf
+          - community.conf
+          - erc20.conf
+

certora/Makefile

@@ -14,8 +14,6 @@ help:
 munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
 	rm -rf $@
 	mkdir $@
-	cp -r $(LIB_DIR) $@
-	cp -r $(CONTRACTS_DIR) $@
 	patch -p0 -d $@ < $(PATCH)
 
 record:

certora/applyHarness.patch

@@ -1,69 +1,7 @@
 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-29 18:12:58.710152977 +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)) {
-         _governancePowerTransferByType(
-           fromUserState.balance,
-           fromBalanceAfter,
-@@ -237,7 +237,7 @@
-       toUserState.balance = toBalanceBefore + uint104(amount);
-       _balances[to] = toUserState;
-
--      if (toUserState.delegationState != DelegationState.NO_DELEGATION) {
-+      if (toUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) {
-         _governancePowerTransferByType(
-           toBalanceBefore,
-           toUserState.balance,
-@@ -293,7 +293,7 @@
-           : address(0);
-     }
-     return
--      userState.delegationState >= DelegationState.PROPOSITION_DELEGATED
-+      userState.delegationState >= uint8(DelegationState.PROPOSITION_DELEGATED)
-         ? _propositionDelegateeV2[delegator]
-         : address(0);
-   }
-@@ -330,16 +330,12 @@
-   ) internal pure returns (DelegationAwareBalance 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);
-     } 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;

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;
   }
 }