Nissan with tadeas

.github/workflows/certora.yml

@@ -31,7 +31,7 @@ jobs:
         with: { java-version: '11', java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==3.6.8.post3
+        run: pip install certora-cli
 
       - name: Install solc
         run: |
@@ -46,7 +46,7 @@ jobs:
           make munged
           cd ..
           echo "key length" ${#CERTORAKEY}
-          sh certora/scripts/${{ matrix.rule }}
+          certoraRun certora/conf/${{ matrix.rule }} --wait_for_results
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -55,9 +55,19 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyAToken.sh
-          - verifyPool.sh getReserveNormalizedVariableDebtCheck
-          - verifyReserveConfiguration.sh
-          - verifyStableTokenCLI.sh
-          - verifyUserConfigCLI.sh
-          - verifyVariableTokenCLI.sh
+          - AToken.conf
+          - Pool.conf
+          - ReserveConfiguration.conf
+          - StableTokenCLI.conf
+          - UserConfigCLI.conf
+          - VariableTokenCLI.conf
+          - NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
+          - NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
+          - NEW-pool-simple-properties.conf  --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
+          - NEW-pool-simple-properties.conf  --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
+          - NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
+          - NEW-pool-simple-properties.conf  --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
+          - NEW-pool-simple-properties.conf  --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
+          - NEW-pool-simple-properties.conf  --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
+          - NEW-pool-simple-properties.conf  --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"
+          - NEW-pool-no-summarizations.conf

certora/applyHarness.patch

@@ -1,13 +1,23 @@
 diff -ruN .gitignore .gitignore
---- .gitignore	1970-01-01 02:00:00
-+++ .gitignore	2023-01-25 13:43:43
+--- .gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2024-03-26 12:06:06.824739877 +0200
 @@ -0,0 +1,2 @@
 +*
 +!.gitignore
 diff -ruN protocol/tokenization/AToken.sol protocol/tokenization/AToken.sol
---- protocol/tokenization/AToken.sol	2023-01-29 12:42:35
-+++ protocol/tokenization/AToken.sol	2023-01-29 12:49:56
-@@ -71,16 +71,16 @@
+--- protocol/tokenization/AToken.sol	2024-03-25 19:09:57.942951737 +0200
++++ protocol/tokenization/AToken.sol	2024-03-26 16:40:05.810557503 +0200
+@@ -37,6 +37,9 @@
+   function getRevision() internal pure virtual override returns (uint256) {
+     return ATOKEN_REVISION;
+   }
++  //function MOMO_KOKO() internal pure virtual returns (uint256) {
++  //  return ATOKEN_REVISION;
++  //}
+
+   /**
+    * @dev Constructor.
+@@ -70,16 +73,16 @@
 
      _domainSeparator = _calculateDomainSeparator();
 
@@ -34,15 +44,15 @@ diff -ruN protocol/tokenization/AToken.sol protocol/tokenization/AToken.sol
    }
 
    /// @inheritdoc IAToken
-diff -ruN protocol/tokenization/StableDebtToken.sol protocol/tokenization/StableDebtToken.sol
---- protocol/tokenization/StableDebtToken.sol	2023-01-11 13:38:21
-+++ protocol/tokenization/StableDebtToken.sol	2023-01-29 12:50:20
-@@ -336,7 +336,7 @@
-    * @param avgRate The average rate at which the total supply increases
-    * @return The debt balance of the user since the last burn/mint action
-    */
--  function _calcTotalSupply(uint256 avgRate) internal view returns (uint256) {
-+  function _calcTotalSupply(uint256 avgRate) internal virtual view returns (uint256) {
-     uint256 principalSupply = super.totalSupply();
+diff -ruN protocol/tokenization/base/ScaledBalanceTokenBase.sol protocol/tokenization/base/ScaledBalanceTokenBase.sol
+--- protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-25 19:09:57.942951737 +0200
++++ protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-26 16:43:02.451462373 +0200
+@@ -34,7 +34,7 @@
+   }
+
+   /// @inheritdoc IScaledBalanceToken
+-  function scaledBalanceOf(address user) external view override returns (uint256) {
++  function scaledBalanceOf(address user) public view override returns (uint256) {
+     return super.balanceOf(user);
+   }
 
-     if (principalSupply == 0) {

certora/conf/AToken.conf

@@ -0,0 +1,14 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/SimpleERC20.sol"
+    ],
+    "link": [
+        "ATokenHarness:_underlyingAsset=SimpleERC20"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "ATokenHarness:certora/specs/AToken.spec",
+    "msg": "aToken spec"
+ }

certora/conf/NEW-pool-no-summarizations.conf

@@ -0,0 +1,41 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/PoolHarness.sol",
+        "certora/harness/StableDebtTokenHarness.sol",
+        "certora/harness/SimpleERC20.sol",
+        "certora/munged/protocol/tokenization/VariableDebtToken.sol",
+        "certora/munged/misc/AaveProtocolDataProvider.sol",
+        "certora/munged/protocol/pool/DefaultReserveInterestRateStrategy.sol",
+        "certora/munged/protocol/configuration/ACLManager.sol",
+        "certora/munged/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+        "certora/munged/protocol/configuration/PriceOracleSentinel.sol",
+        "certora/munged/protocol/configuration/PoolAddressesProvider.sol",
+    ],
+    "link": [
+        "ATokenHarness:POOL=PoolHarness",
+        "ATokenHarness:_underlyingAsset=SimpleERC20",
+        "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+        "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider",
+    ],
+    "struct_link": [
+        "PoolHarness:aTokenAddress=ATokenHarness",
+        "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
+        "PoolHarness:variableDebtTokenAddress=VariableDebtToken",
+        "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategy",
+    ],
+    // "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+    "optimistic_loop": true,
+    "process": "emv",
+    "global_timeout": "7198",
+    "prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+    "solc": "solc8.10",
+    "verify": "PoolHarness:certora/specs/NEW-pool-no-summarizations.spec",
+    "rule": ["liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
+             "depositUpdatesUserATokenSuperBalance",
+             "depositCannotChangeOthersATokenSuperBalance"
+            ],
+    "parametric_contracts": ["PoolHarness"],
+    // method repayWithPermit address,uint256,uint256,address,uint256,uint8,bytes32,bytes32 
+    "msg": "pool-no-summarizations::partial rules",
+}

certora/conf/NEW-pool-simple-properties.conf

@@ -0,0 +1,42 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/PoolHarness.sol",
+        "certora/harness/StableDebtTokenHarness.sol",
+        "certora/harness/SimpleERC20.sol",
+        "contracts/protocol/tokenization/VariableDebtToken.sol",
+        "contracts/misc/AaveProtocolDataProvider.sol",
+        "contracts/protocol/pool/DefaultReserveInterestRateStrategy.sol",
+        "contracts/protocol/libraries/types/DataTypes.sol",
+        "contracts/protocol/configuration/PoolAddressesProvider.sol",
+    ],
+    "link": [
+        "ATokenHarness:POOL=PoolHarness",
+        "ATokenHarness:_underlyingAsset=SimpleERC20",
+        "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+    ],
+    "struct_link": [
+        "PoolHarness:aTokenAddress=ATokenHarness",
+        "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
+        "PoolHarness:variableDebtTokenAddress=VariableDebtToken",
+        "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategy",
+    ],
+    "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+    "solc": "solc8.10",
+    "verify": "PoolHarness:certora/specs/NEW-pool-simple-properties.spec",
+    "rule": ["cannotDepositInInactiveReserve",
+            "cannotDepositInFrozenReserve",
+            "cannotDepositZeroAmount",
+            "cannotWithdrawZeroAmount",
+            "cannotWithdrawFromInactiveReserve",
+            "cannotBorrowZeroAmount",
+            "cannotBorrowOnInactiveReserve",
+            "cannotBorrowOnReserveDisabledForBorrowing",
+            "cannotBorrowOnFrozenReserve"
+            ],
+    "parametric_contracts": ["PoolHarness"],
+    "msg": "pool-simple-properties::ALL",
+}

certora/conf/Pool.conf

@@ -0,0 +1,22 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/PoolHarness.sol",
+        "certora/harness/StableDebtTokenHarness.sol",
+        "certora/munged/protocol/tokenization/VariableDebtToken.sol"
+    ],
+    "link": [
+        "ATokenHarness:POOL=PoolHarness"
+    ],
+    "rule": [
+        "getReserveNormalizedVariableDebtCheck"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 40","-mediumTimeout 700"],
+    "smt_timeout": "600",
+    "solc": "solc8.10",
+    "verify": "PoolHarness:certora/specs/pool.spec",
+    "msg": "Pool"
+}
+

certora/conf/ReserveConfiguration.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harness/ReserveConfigurationHarness.sol"
+    ],
+    "msg": "ReserveConfiguration",
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [
+        "-useBitVectorTheory"
+    ],
+    "solc": "solc8.10",
+    "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
+}

certora/conf/StableTokenCLI.conf

@@ -0,0 +1,12 @@
+{
+    "cache": "StableToken",
+    "files": [
+        "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness"
+    ],
+    "loop_iter": "4",
+    "msg": "stableTokenCLI",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
+}

certora/conf/UserConfigCLI.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harness/UserConfigurationHarness.sol"
+    ],
+    "msg": "UserConfiguration All spec",
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [
+        "-useBitVectorTheory"
+    ],
+    "solc": "solc8.10",
+    "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
+}

certora/conf/VariableTokenCLI.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "certora/harness/VariableDebtTokenHarness.sol"
+    ],
+    "msg": "variable debt token",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
+}

certora/harness/ATokenHarness.sol

@@ -4,6 +4,7 @@ pragma solidity 0.8.10;
 import {Pool} from '../munged/protocol/pool/Pool.sol';
 import {AToken} from '../munged/protocol/tokenization/AToken.sol';
 import {WadRayMath} from '../munged/protocol/libraries/math/WadRayMath.sol';
+import {ScaledBalanceTokenBase} from '../munged/protocol/tokenization/base/ScaledBalanceTokenBase.sol';
 
 /**
  * @title Certora harness for Aave ERC20 AToken
@@ -28,4 +29,12 @@ using WadRayMath for uint256;
   function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) {
     return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset));
   }
-}
+
+  function ATokenBalanceOf(address user) public view returns (uint256) {
+    return super.balanceOf(user);
+  }
+
+  function superBalance(address user) public view returns (uint256) {
+      return scaledBalanceOf(user);
+  }
+}

certora/harness/PoolHarness.sol

@@ -6,6 +6,11 @@ import {DataTypes} from '../munged/protocol/libraries/types/DataTypes.sol';
 import {ReserveLogic} from '../munged/protocol/libraries/logic/ReserveLogic.sol';
 import {IPoolAddressesProvider} from '../munged/interfaces/IPoolAddressesProvider.sol';
 
+import {IERC20} from '../../contracts/dependencies/openzeppelin/contracts/IERC20.sol';
+import {ReserveConfiguration} from '../munged/protocol/libraries/configuration/ReserveConfiguration.sol';
+
+
+
 contract PoolHarness is Pool {
 
     using ReserveLogic for DataTypes.ReserveData;
@@ -18,4 +23,58 @@ contract PoolHarness is Pool {
         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);
+    }
+
+
 }