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/AaveTokenV3Harness.sol

@@ -8,50 +8,48 @@
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
+import {AaveTokenV3} from "../../src/AaveTokenV3.sol";
 
 contract AaveTokenV3Harness is AaveTokenV3 {
-  // returns user's token balance, used in some community rules
-  function getBalance(address user) public view returns (uint104) {
-    return _balances[user].balance;
-  }
 
-  // returns user's delegated proposition balance
-  function getDelegatedPropositionBalance(address user) public view returns (uint72) {
+    // returns user's token balance, used in some community rules
+    function getBalance(address user) view public returns (uint104) {
+    return _balances[user].balance;
+   }
+   // returns user's delegated proposition balance
+   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
     return _balances[user].delegatedPropositionBalance;
-  }
+   }
 
-  // returns user's delegated voting balance
-  function getDelegatedVotingBalance(address user) public view returns (uint72) {
+   // returns user's delegated voting balance
+   function getDelegatedVotingBalance(address user) view public returns (uint72) {
     return _balances[user].delegatedVotingBalance;
-  }
-
-  //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;
-  }
-
-  // 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;
-  }
-
-  // returns user's voting delegate
-  function getVotingDelegate(address user) public view returns (address) {
+   }
+
+   //returns user's delegating proposition status
+   function getDelegatingProposition(address user) view public returns (bool) {
+    return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
+   // returns user's delegating voting status
+   function getDelegatingVoting(address user) view public returns (bool) {
+     return _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
+   // returns user's voting delegate
+   function getVotingDelegate(address user) view public returns (address) {
     return _votingDelegateeV2[user];
-  }
+   }
 
-  // returns user's proposition delegate
-  function getPropositionDelegate(address user) public view returns (address) {
+   // returns user's proposition delegate
+   function getPropositionDelegate(address user) view public returns (address) {
     return _propositionDelegateeV2[user];
-  }
+   }
 
-  // returns user's delegation state
-  function getDelegationState(address user) public view returns (DelegationState) {
+   // returns user's delegation state
+   function getDelegationState(address user) view public returns (DelegationState) {
     return _balances[user].delegationState;
-  }
-}
+   }
+}

certora/harness/AaveTokenV3HarnessCommunity.sol

@@ -2,56 +2,57 @@
 
 /**
 
-  This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for
+  This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for 
   community-written rules
  */
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
+import {AaveTokenV3} from "../../src/AaveTokenV3.sol";
 
 contract AaveTokenV3Harness is AaveTokenV3 {
-  function getBalance(address user) public view returns (uint104) {
+    function getBalance(address user) view public returns (uint104) {
     return _balances[user].balance;
-  }
+   }
 
-  function getDelegatedPropositionBalance(address user) public view returns (uint72) {
+   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
     return _balances[user].delegatedPropositionBalance;
-  }
+   }
 
-  function getDelegatedVotingBalance(address user) public view returns (uint72) {
+
+   function getDelegatedVotingBalance(address user) view public returns (uint72) {
     return _balances[user].delegatedVotingBalance;
-  }
+   }
 
-  function getDelegatingProposition(address user) public view returns (bool) {
-    return
-      _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
-      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-  }
 
-  function getDelegatingVoting(address user) public view returns (bool) {
-    return
-      _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
-      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-  }
+   function getDelegatingProposition(address user) view public returns (bool) {
+    return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
 
-  function getVotingDelegate(address user) public view returns (address) {
+   function getDelegatingVoting(address user) view public returns (bool) {
+     return _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
+   function getVotingDelegate(address user) view public returns (address) {
     return _votingDelegateeV2[user];
-  }
+   }
 
-  function getPropositionDelegate(address user) public view returns (address) {
+   function getPropositionDelegate(address user) view public returns (address) {
     return _propositionDelegateeV2[user];
-  }
+   }
 
-  function getDelegationState(address user) public view returns (DelegationState) {
+   function getDelegationState(address user) view public returns (DelegationState) {
     return _balances[user].delegationState;
-  }
+   }
 
-  function getNonce(address user) public view returns (uint256) {
+   function getNonce(address user) view public returns (uint256) {
     return _nonces[user];
-  }
+   }
 
-  function ecrecoverWrapper(
+   function ecrecoverWrapper(
     bytes32 hash,
     uint8 v,
     bytes32 r,
@@ -60,7 +61,7 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     return ecrecover(hash, v, r, s);
   }
 
-  function computeMetaDelegateHash(
+   function computeMetaDelegateHash(
     address delegator,
     address delegatee,
     uint256 deadline,
@@ -76,7 +77,7 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     return digest;
   }
 
-  function computeMetaDelegateByTypeHash(
+    function computeMetaDelegateByTypeHash(
     address delegator,
     address delegatee,
     GovernancePowerType delegationType,
@@ -101,4 +102,5 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     );
     return digest;
   }
-}
+
+}