NEW-pool-no-summarizations.conf

{
  "files": [
    "certora/basic/harness/ATokenHarness.sol",
    "certora/basic/harness/PoolHarness.sol",
    "certora/basic/harness/SimpleERC20.sol",
    "certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol",
    "certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol",
    "certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
    "certora/basic/munged/contracts/protocol/configuration/ACLManager.sol",
    "certora/basic/munged/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
    "certora/basic/munged/contracts/misc/PriceOracleSentinel.sol",
    "certora/basic/munged/contracts/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:variableDebtTokenAddress=VariableDebtTokenInstance",
    "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
  ],
  "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.19",
  "verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec",
  "rule": [
    "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
    "depositUpdatesUserATokenSuperBalance",
    "depositCannotChangeOthersATokenSuperBalance"
  ],
  "build_cache": true,
  "parametric_contracts": ["PoolHarness"],
  "msg": "pool-no-summarizations::partial rules",
}