fix: lint certora harness (#7)

* fix: lint certora harness

* fix: limit concurrency on test

* fix: limit concurrency on certora

* fix: bump upload to v4

* fix: lint README

* fix: try passing the token

.github/workflows/certora.yml

@@ -1,5 +1,9 @@
 name: certora
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
   pull_request:
     branches:

.github/workflows/comment.yml

@@ -16,6 +16,7 @@ jobs:
           name: pr_number
           path: pr/
           run-id: ${{ github.event.workflow_run.id }}
+          github-token: ${{ github.token }}
 
       - name: Read pr number
         id: get_pr_number
@@ -26,6 +27,7 @@ jobs:
           name: ${{ github.event.workflow_run.head_sha }}
           path: tmp/
           run-id: ${{ github.event.workflow_run.id }}
+          github-token: ${{ github.token }}
 
       - name: Find Comment
         uses: peter-evans/find-comment@782f37b1a8a2b3e2eb9e86a994f0871e9dc146e3

.github/workflows/report-pages.yml

@@ -37,7 +37,7 @@ jobs:
         uses: actions/upload-pages-artifact@v3
         with:
           # Upload only report folder
-          path: './report'
+          path: "./report"
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v4

.github/workflows/test.yml

@@ -1,5 +1,9 @@
 name: Test
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
   pull_request:
   push:
@@ -60,7 +64,7 @@ jobs:
           printf "<details><summary>Build log</summary>\n\n\`\`\`shell\n$(cat /tmp/foundry_build)\n\`\`\`\n</details>\n\n" >> /tmp/template.md
           printf "<details><summary>Test ${{ env.testStatus == 0 && 'success :rainbow:' || 'error :finnadie::x:'}}</summary>\n\n\`\`\`shell\n$(cat /tmp/foundry_test)\n\`\`\`\n</details>\n\n" >> /tmp/template.md
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         with:
           name: ${{ github.event.pull_request.head.sha || github.sha }}
           path: /tmp/template.md
@@ -73,7 +77,7 @@ jobs:
           mkdir -p ./pr
           echo $PR_NUMBER > ./pr/pr_number.txt
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: github.event_name == 'pull_request'
         with:
           name: pr_number

.prettierignore

@@ -2,3 +2,4 @@ out
 lib
 cache
 node_modules
+report

README.md

@@ -7,8 +7,6 @@ Aave v3.1 complete codebase, Foundry-based.
 [![Coverage badge](./report/coverage.svg)](https://aave-dao.github.io/aave-v3-origin)
 <br>
 
-
-
 ## Dependencies
 
 - Foundry, [how-to install](https://book.getfoundry.sh/getting-started/installation) (we recommend also update to the last version with `foundryup`)

certora/README.md

@@ -9,8 +9,8 @@ Documentation for CVT and the specification language are available
 
 Initial step: if certora prover is not installed follow the steps [here](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html)
 
-
 First step is to create the munged/ directory. Enter the certora/ directory and run the following:
+
 ```sh
 touch applyHarness.patch
 ```

certora/harness/ATokenHarness.sol

@@ -13,29 +13,33 @@ import {IScaledBalanceToken} from '../munged/core/contracts/interfaces/IScaledBa
  * @dev Certora's harness contract for the verification of Aave ERC20 AToken.
  */
 contract ATokenHarness is ATokenInstance {
-
-using WadRayMath for uint256;
+  using WadRayMath for uint256;
 
   constructor(Pool pool) public ATokenInstance(pool) {}
 
-  function scaledTotalSupply() public view override(IScaledBalanceToken,ScaledBalanceTokenBase) returns (uint256) {
-      uint256 val = super.scaledTotalSupply();
-      return val;
+  function scaledTotalSupply()
+    public
+    view
+    override(IScaledBalanceToken, ScaledBalanceTokenBase)
+    returns (uint256)
+  {
+    uint256 val = super.scaledTotalSupply();
+    return val;
   }
 
   function additionalData(address user) public view returns (uint128) {
-      return _userState[user].additionalData;
+    return _userState[user].additionalData;
   }
-  
+
   function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) {
-      return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset));
+    return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset));
   }
-  
+
   function ATokenBalanceOf(address user) public view returns (uint256) {
-      return super.balanceOf(user);
+    return super.balanceOf(user);
   }
 
   function superBalance(address user) public view returns (uint256) {
-      return scaledBalanceOf(user);
+    return scaledBalanceOf(user);
   }
 }

certora/harness/PoolHarness.sol

@@ -9,72 +9,76 @@ import {IPoolAddressesProvider} from '../munged/core/contracts/interfaces/IPoolA
 import {IERC20} from '../../src/core/contracts/dependencies/openzeppelin/contracts/IERC20.sol';
 import {ReserveConfiguration} from '../munged/core/contracts/protocol/libraries/configuration/ReserveConfiguration.sol';
 
-
-
 contract PoolHarness is PoolInstance {
-
-    using ReserveLogic for DataTypes.ReserveData;
-    using ReserveLogic for DataTypes.ReserveCache;
-
-    constructor(IPoolAddressesProvider provider) public PoolInstance(provider){}
-
-    function getCurrScaledVariableDebt(address asset) public view returns (uint256){
-        DataTypes.ReserveData storage reserve = _reserves[asset];
-        DataTypes.ReserveCache memory reserveCache = reserve.cache();
-        return reserveCache.currScaledVariableDebt;
-    }
-
-    function getTotalDebt(address asset) public view returns (uint256) {
-        uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply();
-        uint256 totalStable = IERC20(_reserves[asset].stableDebtTokenAddress).totalSupply();
-        return totalVariable + totalStable;
-    }
-
-    function getTotalATokenSupply(address asset) public view returns (uint256) {
-        return IERC20(_reserves[asset].aTokenAddress).totalSupply();
-    }
-
-    function getReserveLiquidityIndex(address asset) public view returns (uint256) {
-        return _reserves[asset].liquidityIndex;
-    }
-
-    function getReserveStableBorrowRate(address asset) public view returns (uint256) {
-        return _reserves[asset].currentStableBorrowRate;
-    }
-
-    function getReserveVariableBorrowIndex(address asset) public view returns (uint256) {
-        return _reserves[asset].variableBorrowIndex;
-    }
-
-    function getReserveVariableBorrowRate(address asset) public view returns (uint256) {
-        return _reserves[asset].currentVariableBorrowRate;
-    }
-
-    function updateReserveIndexes(address asset) public returns (bool) {
-        ReserveLogic._updateIndexes(_reserves[asset], _reserves[asset].cache());
-        return true;
-    }
-
-    function updateReserveIndexesWithCache(address asset, DataTypes.ReserveCache memory cache) public returns (bool) {
-        ReserveLogic._updateIndexes(_reserves[asset], cache);
-        return true;
-    }
-
-    function cumulateToLiquidityIndex(address asset, uint256 totalLiquidity, uint256 amount) public returns (uint256) {
-        return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount);
-    }
-
-    function getActive(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
-        return ReserveConfiguration.getActive(self);
-    }
-
-    function getFrozen(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
-        return ReserveConfiguration.getFrozen(self);
-    }
-
-    function getBorrowingEnabled(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
-        return ReserveConfiguration.getBorrowingEnabled(self);
-    }
-
-
+  using ReserveLogic for DataTypes.ReserveData;
+  using ReserveLogic for DataTypes.ReserveCache;
+
+  constructor(IPoolAddressesProvider provider) public PoolInstance(provider) {}
+
+  function getCurrScaledVariableDebt(address asset) public view returns (uint256) {
+    DataTypes.ReserveData storage reserve = _reserves[asset];
+    DataTypes.ReserveCache memory reserveCache = reserve.cache();
+    return reserveCache.currScaledVariableDebt;
+  }
+
+  function getTotalDebt(address asset) public view returns (uint256) {
+    uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply();
+    uint256 totalStable = IERC20(_reserves[asset].stableDebtTokenAddress).totalSupply();
+    return totalVariable + totalStable;
+  }
+
+  function getTotalATokenSupply(address asset) public view returns (uint256) {
+    return IERC20(_reserves[asset].aTokenAddress).totalSupply();
+  }
+
+  function getReserveLiquidityIndex(address asset) public view returns (uint256) {
+    return _reserves[asset].liquidityIndex;
+  }
+
+  function getReserveStableBorrowRate(address asset) public view returns (uint256) {
+    return _reserves[asset].currentStableBorrowRate;
+  }
+
+  function getReserveVariableBorrowIndex(address asset) public view returns (uint256) {
+    return _reserves[asset].variableBorrowIndex;
+  }
+
+  function getReserveVariableBorrowRate(address asset) public view returns (uint256) {
+    return _reserves[asset].currentVariableBorrowRate;
+  }
+
+  function updateReserveIndexes(address asset) public returns (bool) {
+    ReserveLogic._updateIndexes(_reserves[asset], _reserves[asset].cache());
+    return true;
+  }
+
+  function updateReserveIndexesWithCache(
+    address asset,
+    DataTypes.ReserveCache memory cache
+  ) public returns (bool) {
+    ReserveLogic._updateIndexes(_reserves[asset], cache);
+    return true;
+  }
+
+  function cumulateToLiquidityIndex(
+    address asset,
+    uint256 totalLiquidity,
+    uint256 amount
+  ) public returns (uint256) {
+    return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount);
+  }
+
+  function getActive(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
+    return ReserveConfiguration.getActive(self);
+  }
+
+  function getFrozen(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
+    return ReserveConfiguration.getFrozen(self);
+  }
+
+  function getBorrowingEnabled(
+    DataTypes.ReserveConfigurationMap memory self
+  ) external pure returns (bool) {
+    return ReserveConfiguration.getBorrowingEnabled(self);
+  }
 }