fixing patch for CI

.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

.gitignore

@@ -9,5 +9,4 @@ package-lock.json
 .certora_config/
 .last_confs/
 .certora_*
-certora/munged
 resource_errors.json

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,14 @@
-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 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 02:00:00
++++ .gitignore	2023-03-29 13:05:55
+@@ -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;
@@ -10,7 +17,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 +26,7 @@ diff -uN AaveTokenV3.sol /AaveTokenV3.sol
          _governancePowerTransferByType(
            toBalanceBefore,
            toUserState.balance,
-@@ -288,7 +288,7 @@
+@@ -293,7 +293,7 @@
            : address(0);
      }
      return
@@ -28,7 +35,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 +55,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-29 13:12:02
++++ src/BaseAaveToken.sol	2023-03-29 13:07:15
 @@ -18,7 +18,7 @@
      uint104 balance;
      uint72 delegatedPropositionBalance;
@@ -73,7 +67,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

@@ -12,7 +12,7 @@
 
 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) public view returns (uint104) {

certora/harness/README.md

@@ -4,4 +4,4 @@ We use two harnesses:
 
 - AaveTokenV3HarnessStorage is used to verify general.spec. It changes delegationState field in _balances
 to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which
-patches the original code with `applyHarness.patch` patch.
+patches the original code with `applyHarness.patch` patch.

certora/munged/.gitignore

@@ -0,0 +1,2 @@
+*
+!.gitignore

certora/scripts/erc20.sh

@@ -10,4 +10,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     --optimistic_loop \
     --cloud \
     --msg "AaveTokenV3:erc20.spec $1"
- 
+

certora/scripts/verifyCommunity.sh

@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \
     --cloud \
     --msg "AaveTokenV3HarnessCommunity:community.spec $1"
 # --sanity
- 
+

certora/scripts/verifyDelegate.sh

@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     --cloud \
     --msg "AaveTokenV3Harness:delegate.spec $1"
 # --sanity
- 
+

certora/scripts/verifyGeneral.sh

@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \
     --settings -smt_bitVectorTheory=true \
     --cloud \
     --msg "AaveTokenV3:general.spec $1"
- 
+

certora/specs/community.spec

@@ -1,5 +1,5 @@
 /*
-    This is a specification file for the verification of AaveTokenV3.sol 
+    This is a specification file for the verification of AaveTokenV3.sol
     smart contract using the Certora prover. The rules in this spec have been
     contributed by the community. Individual attribution is given in the comments
     to each rule.
@@ -189,7 +189,7 @@ rule metaDelegateNonRepeatable(env e1, env e2, address delegator, address delega
 */
 rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, address bob) {
 
-    require e.msg.sender != ZERO_ADDRESS(); 
+    require e.msg.sender != ZERO_ADDRESS();
     require e.msg.sender != alice && e.msg.sender != bob;
     require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS();
 
@@ -321,11 +321,11 @@ rule delegateIndependence(method f) {
         isVotingDelegatorAfter = getDelegatingVoting(a);
         isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0
 
-        votingPowerBefore < votingPowerAfter <=> 
+        votingPowerBefore < votingPowerAfter <=>
         (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) ||
         (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0))
         &&
-        votingPowerBefore > votingPowerAfter <=> 
+        votingPowerBefore > votingPowerAfter <=>
         (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) ||
         (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0))
     }
@@ -355,12 +355,12 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) {
 
     require !isVotingDelegateeBefore && !isVotingDelegateeAfter;
 
-    /* 
+    /*
     If you're not a delegatee, your voting power only increases when
         1. You're not delegating and your balance increases
         2. You're delegating and stop delegating and your balanceBefore != 0
     */
-    assert votingPowerBefore < votingPowerAfter <=> 
+    assert votingPowerBefore < votingPowerAfter <=>
         (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) ||
         (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0));
 
@@ -369,7 +369,7 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) {
         1. You're not delegating and your balance decreases
         2. You're not delegating and start delegating and your balanceBefore != 0
     */
-    assert votingPowerBefore > votingPowerAfter <=> 
+    assert votingPowerBefore > votingPowerAfter <=>
         (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) ||
         (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0));
 }
@@ -396,11 +396,11 @@ rule votingPowerChangesWhileNotBeingADelegatee(address a) {
         isPropositionDelegatorAfter = getDelegatingProposition(a);
         isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0
 
-        propositionPowerBefore < propositionPowerAfter <=> 
+        propositionPowerBefore < propositionPowerAfter <=>
         (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) ||
         (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0))
         &&
-        propositionPowerBefore > propositionPowerAfter <=> 
+        propositionPowerBefore > propositionPowerAfter <=>
         (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) ||
         (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0))
     }
@@ -435,16 +435,16 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) {
         1. You're not delegating and your balance increases
         2. You're delegating and stop delegating and your balanceBefore != 0
     */
-    assert propositionPowerBefore < propositionPowerAfter <=> 
+    assert propositionPowerBefore < propositionPowerAfter <=>
         (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) ||
         (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0));
-    
+
     /*
     If you're not a delegatee, your proposition power only decreases when
         1. You're not delegating and your balance decreases
         2. You're not delegating and start delegating and your balanceBefore != 0
     */
-    assert propositionPowerBefore > propositionPowerAfter <=> 
+    assert propositionPowerBefore > propositionPowerAfter <=>
         (!isPropositionDelegatorBefore && !isPropositionDelegatorBefore && (balanceBefore > balanceAfter)) ||
         (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0));
 }
@@ -463,7 +463,7 @@ rule propositionPowerChangesWhileNotBeingADelegatee(address a) {
         f(e, args)
     >
     {
-       allowance(owner, spender) != allowanceBefore =>f.selector==approve(address,uint256).selector 
+       allowance(owner, spender) != allowanceBefore =>f.selector==approve(address,uint256).selector
             || f.selector==increaseAllowance(address,uint256).selector
             || f.selector==decreaseAllowance(address,uint256).selector
             || f.selector==transferFrom(address,address,uint256).selector
@@ -486,7 +486,7 @@ rule allowanceStateChange(env e){
     f(e, args);
     uint256 allowanceAfter=allowance(owner,user);
 
-    assert allowanceBefore!=allowanceAfter => f.selector==approve(address,uint256).selector 
+    assert allowanceBefore!=allowanceAfter => f.selector==approve(address,uint256).selector
     || f.selector==increaseAllowance(address,uint256).selector
     || f.selector==decreaseAllowance(address,uint256).selector
     || f.selector==transferFrom(address,address,uint256).selector