Fix applyHarness.patch, scripts, imports in harness and Makefile

.github/workflows/certora.yml

@@ -32,13 +32,13 @@ jobs:
 
       - name: Install certora cli
         run: pip install certora-cli
-        
+
       - name: Install solc
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc8.13
-      
+
       - name: Verify rule ${{ matrix.rule }}
         run: |
           cd certora
@@ -49,7 +49,7 @@ jobs:
           sh certora/scripts/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
-          
+
     strategy:
       fail-fast: false
       max-parallel: 16

README.md

@@ -1,6 +1,6 @@
 # $AAVE V3
 
-Nex#t iteration of the AAVE token, optimized for its usage on the upcoming new iteration of the Aave Governance.
+Next iteration of the AAVE token, optimized for its usage on the upcoming new iteration of the Aave Governance.
 
 More detailed description and specification [HERE](./properties.md)
 
@@ -13,4 +13,4 @@ After having installed Foundry:
 2. `make test` to run the simulation tests.
 
 ## Copyright
-2022 BGD Labs
+2022 BGD Labs

certora/Makefile

@@ -13,12 +13,17 @@ help:
 
 munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
 	rm -rf $@
-	cp -r $(CONTRACTS_DIR) $@
+	mkdir $@
 	cp -r $(LIB_DIR) $@
+	cp -r $(CONTRACTS_DIR) $@
 	patch -p0 -d $@ < $(PATCH)
 
 record:
-	diff -uN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+$(CONTRACTS_DIR)/++g' | sed 's+$(MUNGED_DIR)++g' > $(PATCH)
+	mkdir tmp_make_r
+	cp -r $(LIB_DIR) tmp_make_r
+	cp -r $(CONTRACTS_DIR) tmp_make_r
+	diff -ruN tmp_make_r $(MUNGED_DIR) | sed 's+tmp_make_r/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
+	rm -rf tmp_make_r
 
 clean:
 	git clean -fdX

certora/README.md

@@ -6,17 +6,17 @@ In this directory you will find three subdirectories:
 - `base.spec` contains method declarations, CVL functions and definitions used by the main specification files
 - `delegate.spec` contains rules that prove various delegation properties
 - `erc20.spec` contains rules that prove ERC20 general rules, e.g. correctness of transfer and others
-- `general.spec` contains general delegation invariants, e.g. sum of delegated and undelegated balances equals to 
-total supply  
+- `general.spec` contains general delegation invariants, e.g. sum of delegated and undelegated balances equals to
+total supply
 
-2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings. 
+2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings.
 - `verifyDelegate.sh` is a script for running `delegate.spec`
 - `verifyGeneral.sh` is a script for running `general.spec`
 - `erc20.sh` is a script for running `erc20.spec`
 
 3. harness - Contains all the inheriting contracts that add/simplify functionalities to the original contract.
 We use two harnesses:
-- `AaveTokenV3Harness.sol` used by `erc20.sh` and `delegate.sh`. It inherits from the original AaveV3Token 
+- `AaveTokenV3Harness.sol` used by `erc20.sh` and `delegate.sh`. It inherits from the original AaveV3Token
 contract and adds a few getter functions.
 
 - `AaveTokenV3HarnessStorage.sol` used by `general.sh`. It uses a modified a version of AaveV3Token contract

certora/applyHarness.patch

@@ -1,7 +1,8 @@
-diff -uN AaveTokenV3.sol /AaveTokenV3.sol
---- AaveTokenV3.sol	2022-10-11 16:03:49.000000000 +0300
-+++ /AaveTokenV3.sol	2022-10-11 16:13:48.000000000 +0300
-@@ -210,7 +210,7 @@
+Binary files .DS_Store and .DS_Store differ
+diff -ruN src/AaveTokenV3.sol src/AaveTokenV3.sol
+--- src/AaveTokenV3.sol	2023-03-28 15:10:26
++++ src/AaveTokenV3.sol	2023-03-28 15:05:22
+@@ -215,7 +215,7 @@
          fromBalanceAfter = fromUserState.balance - uint104(amount);
        }
        _balances[from].balance = fromBalanceAfter;
@@ -10,7 +11,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
          _governancePowerTransferByType(
            fromUserState.balance,
            fromBalanceAfter,
-@@ -232,7 +232,7 @@
+@@ -237,7 +237,7 @@
        toUserState.balance = toBalanceBefore + uint104(amount);
        _balances[to] = toUserState;
 
@@ -19,7 +20,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
          _governancePowerTransferByType(
            toBalanceBefore,
            toUserState.balance,
-@@ -288,7 +288,7 @@
+@@ -293,7 +293,7 @@
            : address(0);
      }
      return
@@ -28,7 +29,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
          ? _propositionDelegateeV2[delegator]
          : address(0);
    }
-@@ -325,16 +325,12 @@
+@@ -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
@@ -48,22 +49,9 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
      }
      return userState;
    }
-diff -uN BaseAaveToken.sol /BaseAaveToken.sol
---- BaseAaveToken.sol	2022-10-11 17:36:35.000000000 +0300
-+++ /BaseAaveToken.sol	2022-10-11 16:20:40.000000000 +0300
-@@ -1,9 +1,9 @@
- // SPDX-License-Identifier: MIT
- pragma solidity ^0.8.0;
-
--import {Context} from '../lib/openzeppelin-contracts/contracts/utils/Context.sol';
--import {IERC20} from '../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';
--import {IERC20Metadata} from '../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol';
-+import {Context} from './lib/openzeppelin-contracts/contracts/utils/Context.sol';
-+import {IERC20} from './lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';
-+import {IERC20Metadata} from './lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol';
-
- // Inspired by OpenZeppelin Contracts (last updated v4.5.0) (token/ERC20/ERC20.sol)
- abstract contract BaseAaveToken is Context, IERC20Metadata {
+diff -ruN src/BaseAaveToken.sol src/BaseAaveToken.sol
+--- src/BaseAaveToken.sol	2023-03-28 15:10:26
++++ src/BaseAaveToken.sol	2023-03-28 15:10:24
 @@ -16,10 +16,10 @@
 
    // reorder fields to make hooks syntax simpler
@@ -76,7 +64,3 @@ diff -uN BaseAaveToken.sol /BaseAaveToken.sol
    }
 
    mapping(address => DelegationAwareBalance) internal _balances;
-Common subdirectories: interfaces and /interfaces
-Common subdirectories: lib and /lib
-Common subdirectories: test and /test
-Common subdirectories: utils and /utils

certora/harness/AaveTokenV3HarnessStorage.sol

@@ -4,15 +4,15 @@
 
   This is an extension of the harnessed AaveTokenV3 with added getters on the _balances fields.
   The imported harnessed AaveTokenV3 contract uses uint8 instead of an enum for delegation state.
-  
+
   This modification is introduced to bypass a current Certora Prover limitation on accessing
   enum fields inside CVL hooks
 
  */
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from "../munged/AaveTokenV3.sol";
+import {AaveTokenV3} from "../munged/src/AaveTokenV3.sol";
 
 contract AaveTokenV3Harness is AaveTokenV3 {
     function getBalance(address user) view public returns (uint104) {

certora/scripts/erc20.sh

@@ -8,6 +8,6 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     $RULE \
     --solc solc8.13 \
     --optimistic_loop \
-    --send_only \
+    --cloud \
     --msg "AaveTokenV3:erc20.spec $1"
- 
+

certora/scripts/verifyCommunity.sh

@@ -8,7 +8,7 @@ certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \
     $RULE \
     --solc solc8.13 \
     --optimistic_loop \
-    --send_only \
+    --cloud \
     --msg "AaveTokenV3HarnessCommunity:community.spec $1"
 # --sanity
- 
+

certora/scripts/verifyDelegate.sh

@@ -8,7 +8,7 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     $RULE \
     --solc solc8.13 \
     --optimistic_loop \
-    --send_only \
+    --cloud \
     --msg "AaveTokenV3Harness:delegate.spec $1"
 # --sanity
- 
+

certora/scripts/verifyGeneral.sh

@@ -9,6 +9,6 @@ certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \
     --solc solc8.13 \
     --optimistic_loop \
     --settings -smt_bitVectorTheory=true \
-    --send_only \
+    --cloud \
     --msg "AaveTokenV3:general.spec $1"
- 
+