Certora adaptation to stata

.github/workflows/certora-stata.yml

@@ -0,0 +1,79 @@
+name: certora-stata
+
+on:
+ push:
+ branches:
+ - main
+ pull_request:
+ branches:
+ - main
+
+ workflow_dispatch:
+
+jobs:
+ verify:
+ runs-on: ubuntu-latest
+
+ steps:
+ - uses: actions/checkout@v2
+ with:
+ submodules: recursive
+
+ - name: Install python
+ uses: actions/setup-python@v2
+ with: { python-version: 3.9 }
+
+ - name: Install java
+ uses: actions/setup-java@v1
+ with: { java-version: "11", java-package: jre }
+
+ - name: Install certora cli
+ run: pip install certora-cli==7.14.2
+
+ - name: Install solc
+ run: |
+ wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
+ chmod +x solc-static-linux
+ sudo mv solc-static-linux /usr/local/bin/solc8.20
+
+ - name: Verify rule ${{ matrix.rule }}
+ run: |
+ cd certora/stata
+ touch applyHarness.patch
+ make munged
+ cd ../..
+ certoraRun certora/stata/conf/${{ matrix.rule }}
+ env:
+ CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+ strategy:
+ fail-fast: false
+ max-parallel: 16
+ matrix:
+ rule:
+ - verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
+ - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
+ # Timeout
+ # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
+ - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
+ - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
+ - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
+ - verifyERC4626Extended.conf --rule maxDepositConstant
+ - verifyERC4626Extended.conf --rule redeemSum
+ - verifyERC4626Extended.conf --rule redeemATokensSum
+ - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
+ - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
+ - verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
+ - verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
+ - verifyStataToken.conf --rule totalClaimableRewards_stable
+ - verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
+ - verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
+ - verifyStataToken.conf --rule singleAssetAccruedRewards
+ - verifyStataToken.conf --rule totalAssets_stable
+ - verifyStataToken.conf --rule getClaimableRewards_stable
+ - verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
+ - verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
+ - verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
+ - verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
+ - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
+ - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient

certora/conf/AToken.conf

@@ -11,5 +11,6 @@
  "process": "emv",
  "solc": "solc8.19",
  "verify": "ATokenHarness:certora/specs/AToken.spec",
+// "build_cache": true,
  "msg": "aToken spec"
 }

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

@@ -36,6 +36,7 @@
  "depositUpdatesUserATokenSuperBalance",
  "depositCannotChangeOthersATokenSuperBalance"
  ],
+// "build_cache": true,
  "parametric_contracts": ["PoolHarness"],
  "msg": "pool-no-summarizations::partial rules",
 }

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

@@ -38,6 +38,7 @@
  "cannotBorrowOnReserveDisabledForBorrowing",
  "cannotBorrowOnFrozenReserve"
  ],
+// "build_cache": true,
  "parametric_contracts": ["PoolHarness"],
  "msg": "pool-simple-properties::ALL",
 }

certora/conf/ReserveConfiguration.conf

@@ -10,5 +10,6 @@
  ],
  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
  "solc": "solc8.19",
+// "build_cache": true,
  "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
 }

certora/conf/StableDebtToken.conf

@@ -14,5 +14,6 @@
  "optimistic_loop": true,
  "process": "emv",
  "solc": "solc8.19",
+// "build_cache": true,
  "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
 }

certora/conf/UserConfiguration.conf

@@ -11,5 +11,6 @@
  "-useBitVectorTheory"
  ],
  "solc": "solc8.19",
+// "build_cache": true,
  "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
 }

certora/conf/VariableDebtToken.conf

@@ -7,5 +7,6 @@
  "optimistic_loop": true,
  "process": "emv",
  "solc": "solc8.19",
+// "build_cache": true,
  "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
 }

certora/scripts/run-all.sh

@@ -1,4 +1,4 @@
-CMN=""
+#CMN="--compilation_steps_only"
 
 
 

certora/specs/NEW-pool-base.spec

@@ -30,19 +30,19 @@ methods {
  function _.transfer(address, uint256) external => DISPATCHER(true);
  function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
  function _.approve(address, uint256) external => DISPATCHER(true);
- function _.mint(address, uint256) external => DISPATCHER(true);
- function _.burn(uint256) external => DISPATCHER(true);
+ //function _.mint(address, uint256) external => DISPATCHER(true);
+ //function _.burn(uint256) external => DISPATCHER(true);
  function _.balanceOf(address) external => DISPATCHER(true);
 
  function _.totalSupply() external => DISPATCHER(true);
 
  // ATOKEN
- function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true);
- function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true);
+ //function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true);
+ //function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true);
  function _.mintToTreasury(uint256 amount, uint256 index) external => DISPATCHER(true);
  function _.transferOnLiquidation(address from, address to, uint256 value) external => DISPATCHER(true);
  function _.transferUnderlyingTo(address user, uint256 amount) external => DISPATCHER(true);
- function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true);
+ // function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true);
  function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external => DISPATCHER(true);
  function _.ATokenBalanceOf(address user) external => DISPATCHER(true);
 
@@ -62,7 +62,7 @@ methods {
  function _.getReserveNormalizedIncome(address asset) external => DISPATCHER(true);
  function _.getReserveNormalizedVariableDebt(address asset) external => DISPATCHER(true);
  function _.getACLManager() external => DISPATCHER(true);
- function _.isBridge(address) external => DISPATCHER(true);
+ //function _.isBridge(address) external => DISPATCHER(true);
 
  // StableDebt
  function _.mint(address user, address onBehalfOf, uint256 amount, uint256 rate) external => DISPATCHER(true);

certora/specs/NEW-pool-no-summarizations.spec

@@ -9,7 +9,7 @@ methods {
  function _.symbol() external => DISPATCHER(true);
  function _.isFlashBorrower(address a) external => DISPATCHER(true);
 
- function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true);
+ // function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true);
 
  function _.getAverageStableRate() external => DISPATCHER(true);
  function _.isPoolAdmin(address a) external => DISPATCHER(true);

certora/stata/Makefile

@@ -0,0 +1,33 @@
+default: help
+
+PATCH = applyHarness.patch
+CONTRACTS_DIR = ../../src
+LIBS_DIR = ../../lib
+MUNGED_SRC = munged/src
+MUNGED_LIB = munged/lib
+MUNGED_DIR = munged
+
+help:
+ @echo "usage:"
+ @echo " make clean: remove all generated files (those ignored by git)"
+ @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+ @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+ rm -rf $@
+ mkdir $@
+ cp -r ../../lib $@
+ cp -r ../../src $@
+ patch -p0 -d $@ < $(PATCH)
+
+record:
+ mkdir tmp
+ cp -r ../../lib tmp
+ cp -r ../../src tmp
+ diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
+ rm -rf tmp
+
+clean:
+ git clean -fdX
+ touch $(PATCH)
+

certora/stata/applyHarness.patch

@@ -0,0 +1,48 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore 1970-01-01 02:00:00
++++ .gitignore 2024-09-04 13:59:46
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
+diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstance.sol
+--- src/core/instances/ATokenInstance.sol 2024-09-05 19:01:54
++++ src/core/instances/ATokenInstance.sol 2024-09-05 11:33:23
+@@ -35,15 +35,15 @@
+
+ _domainSeparator = _calculateDomainSeparator();
+
+- emit Initialized(
+- underlyingAsset,
+- address(POOL),
+- treasury,
+- address(incentivesController),
+- aTokenDecimals,
+- aTokenName,
+- aTokenSymbol,
+- params
+- );
++ // emit Initialized(
++ // underlyingAsset,
++ // address(POOL),
++ // treasury,
++ // address(incentivesController),
++ // aTokenDecimals,
++ // aTokenName,
++ // aTokenSymbol,
++ // params
++ // );
+ }
+ }
+diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol
+--- src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54
++++ src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31
+@@ -147,7 +147,7 @@
+ }
+
+ ///@inheritdoc IERC20AaveLM
+- function rewardTokens() external view returns (address[] memory) {
++ function rewardTokens() public view returns (address[] memory) {
+ ERC20AaveLMStorage storage $ = _getERC20AaveLMStorage();
+ return $._rewardTokens;
+ }

certora/stata/conf/verifyAToken.conf

@@ -0,0 +1,40 @@
+{
+ "files": [
+ "certora/stata/harness/StataTokenV2Harness.sol",
+ "certora/stata/harness/pool/SymbolicLendingPool.sol",
+ "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+ "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+ "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+ "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+ "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+ ],
+ "link": [
+ "SymbolicLendingPool:aToken=ATokenInstance",
+ "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+ "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+ "ATokenInstance:POOL=SymbolicLendingPool",
+ "ATokenInstance:_incentivesController=RewardsControllerHarness",
+ "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+ "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "StataTokenV2Harness:POOL=SymbolicLendingPool",
+ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+ ],
+ "packages": [
+ "aave-v3-core/=certora/stata/munged/src/core",
+ "aave-v3-periphery/=certora/stata/munged/src/periphery",
+ "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+ "forge-std/=certora/stata/munged/lib/forge-std/src",
+ "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+ "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+ "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+ ],
+ "loop_iter": "1",
+ "msg": "aToken properties",
+ "optimistic_hashing": true,
+ "optimistic_loop": true,
+ "solc": "solc8.20",
+ "smt_timeout": "1400",
+ "verify": "StataTokenV2Harness:certora/stata/specs/StataToken/aTokenProperties.spec",
+ "build_cache": true,
+}

certora/stata/conf/verifyDoubleClaim.conf

@@ -0,0 +1,40 @@
+{
+ "files": [
+ "certora/stata/harness/StataTokenV2Harness.sol",
+ "certora/stata/harness/pool/SymbolicLendingPool.sol",
+ "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+ "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+ "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+ "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+ "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+ ],
+ "link": [
+ "SymbolicLendingPool:aToken=ATokenInstance",
+ "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+ "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+ "ATokenInstance:POOL=SymbolicLendingPool",
+ "ATokenInstance:_incentivesController=RewardsControllerHarness",
+ "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+ "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "StataTokenV2Harness:POOL=SymbolicLendingPool",
+ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+ ],
+ "packages": [
+ "aave-v3-core/=certora/stata/munged/src/core",
+ "aave-v3-periphery/=certora/stata/munged/src/periphery",
+ "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+ "forge-std/=certora/stata/munged/lib/forge-std/src",
+ "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+ "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+ "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+],
+ "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/double_claim.spec",
+ "solc": "solc8.20",
+ "msg": "Multi rewards - double claim properties",
+ "optimistic_loop": true,
+ "smt_timeout": "2000",
+ "loop_iter": "2",
+ "optimistic_hashing": true,
+ "build_cache": true,
+}

certora/stata/conf/verifyERC4626.conf

@@ -0,0 +1,40 @@
+{
+ "files": [
+ "certora/stata/harness/StataTokenV2Harness.sol",
+ "certora/stata/harness/pool/SymbolicLendingPool.sol",
+ "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+ "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+ "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+ "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+ "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+ ],
+ "link": [
+ "SymbolicLendingPool:aToken=ATokenInstance",
+ "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+ "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+ "ATokenInstance:POOL=SymbolicLendingPool",
+ "ATokenInstance:_incentivesController=RewardsControllerHarness",
+ "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+ "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+ "StataTokenV2Harness:POOL=SymbolicLendingPool",
+ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+ ],
+ "packages": [
+ "aave-v3-core/=certora/stata/munged/src/core",
+ "aave-v3-periphery/=certora/stata/munged/src/periphery",
+ "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+ "forge-std/=certora/stata/munged/lib/forge-std/src",
+ "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+ "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+ "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+],
+ "verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626.spec",
+ "solc": "solc8.20",
+ "msg": "ERC4626 properties",
+ "optimistic_loop": true,
+ "smt_timeout": "3600",
+ "loop_iter": "1",
+ "optimistic_hashing": true,
+ "build_cache": true,
+}