Certora · tadeas-kucera · May 25, 2022 · May 25, 2022 · May 25, 2022 · May 25, 2022
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -7,6 +7,7 @@ on:
   pull_request:
     branches:
       - main
+      - certora-to-main-fork
 
   workflow_dispatch:
 
@@ -32,13 +33,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 +50,7 @@ jobs:
           sh certora/scripts/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
-          
+
     strategy:
       fail-fast: false
       max-parallel: 16

diff --git a/.github/workflows/temp.yml b/.github/workflows/temp.yml
@@ -0,0 +1,36 @@
+# This is a basic workflow to help you get started with Actions
+
+name: CI
+
+# Controls when the workflow will run
+on:
+  # Triggers the workflow on push or pull request events but only for the "main" branch
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+  # This workflow contains a single job called "build"
+  build:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
+      - uses: actions/checkout@v3
+
+      # Runs a single command using the runners shell
+      - name: Run a one-line script
+        run: echo Hello, world!
+
+      # Runs a set of commands using the runners shell
+      - name: Run a multi-line script
+        run: |
+          echo Add other actions to build,
+          echo test, and deploy your project.
diff --git a/.gitmodules b/.gitmodules
@@ -1,9 +1,9 @@
-[submodule "lib/openzeppelin-contracts"]
-	path = lib/openzeppelin-contracts
-	url = https://github.com/OpenZeppelin/openzeppelin-contracts
 [submodule "lib/aave-token-v2"]
 	path = lib/aave-token-v2
 	url = https://github.com/aave/aave-token-v2
 [submodule "lib/forge-std"]
 	path = lib/forge-std
 	url = https://github.com/foundry-rs/forge-std
+[submodule "lib/openzeppelin-contracts"]
+	path = lib/openzeppelin-contracts
+	url = https://github.com/OpenZeppelin/openzeppelin-contracts
diff --git a/README.md b/README.md
@@ -1,6 +1,6 @@
 # $AAVE V3
 
-Next iteration of the AAVE token, optimized for its usage on the upcoming new iteration of the Aave Governance.
+Nex#t 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
diff --git a/certora/Makefile b/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

diff --git a/certora/applyHarness.patch b/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,32 +49,18 @@ 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;
+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 @@
 
--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 {
-@@ -18,7 +18,7 @@
+   // reorder fields to make hooks syntax simpler
+   struct DelegationAwareBalance {
+-    DelegationState delegationState;
      uint104 balance;
      uint72 delegatedPropositionBalance;
      uint72 delegatedVotingBalance;
--    DelegationState delegationState;
 +    uint8 delegationState; // refactored from enum
    }
 
    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
diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/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) {

diff --git a/certora/scripts/erc20.sh b/certora/scripts/erc20.sh
@@ -10,4 +10,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     --optimistic_loop \
     --cloud \
     --msg "AaveTokenV3:erc20.spec $1"
- 
+
diff --git a/certora/scripts/verifyCommunity.sh b/certora/scripts/verifyCommunity.sh
@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessCommunity.sol:AaveTokenV3Harness \
     --cloud \
     --msg "AaveTokenV3HarnessCommunity:community.spec $1"
 # --sanity
- 
+
diff --git a/certora/scripts/verifyDelegate.sh b/certora/scripts/verifyDelegate.sh
@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3Harness \
     --cloud \
     --msg "AaveTokenV3Harness:delegate.spec $1"
 # --sanity
- 
+
diff --git a/certora/scripts/verifyGeneral.sh b/certora/scripts/verifyGeneral.sh
@@ -11,4 +11,4 @@ certoraRun certora/harness/AaveTokenV3HarnessStorage.sol:AaveTokenV3Harness \
     --settings -smt_bitVectorTheory=true \
     --cloud \
     --msg "AaveTokenV3:general.spec $1"
- 
+
diff --git a/certora/specs/community.spec b/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

diff --git a/foundry.toml b/foundry.toml
@@ -3,7 +3,7 @@ src = 'src'
 out = 'out'
 libs = ['lib']
 remappings = [
-    'openzeppelin-contracts/=lib/openzeppelin-contracts/contracts'
+  'openzeppelin-contracts/=lib/openzeppelin-contracts/contracts'
 ]
 
-# See more config options https://github.com/gakonst/foundry/tree/master/config
+# See more config options https://github.com/gakonst/foundry/tree/master/config
diff --git a/lib/aave-token-v2 b/lib/aave-token-v2
diff --git a/lib/forge-std b/lib/forge-std
diff --git a/lib/openzeppelin-contracts b/lib/openzeppelin-contracts
diff --git a/lib/openzeppelin-contracts/.codecov.yml b/lib/openzeppelin-contracts/.codecov.yml