diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 1eb6928b..bd3955a5 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -33,7 +33,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: | @@ -64,4 +64,4 @@ jobs: - verifyGhoAToken.sh noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero handleRepayment_after_transferUnderlyingTo level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee - - verifyGhoVariableDebtToken.sh discountCantExceed100Percent disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease userCantNullifyItsDebt integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation onlyMintForUserCanIncreaseUsersBalance integrityOfMint_cantDecreaseInterestWithMint integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex integrityOfBurn_fixedIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance + - verifyGhoVariableDebtToken.sh discountCantExceed100Percent disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease userCantNullifyItsDebt integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation onlyMintForUserCanIncreaseUsersBalance integrityOfMint_cantDecreaseInterestWithMint integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt diff --git a/certora/.gitignore b/certora/.gitignore deleted file mode 100644 index 109d697a..00000000 --- a/certora/.gitignore +++ /dev/null @@ -1,5 +0,0 @@ -# certora temp files -.certora/ -.certora* -.last_confs/ -resource_errors* \ No newline at end of file diff --git a/certora/scripts/verifyFlashMinter.sh b/certora/scripts/verifyFlashMinter.sh index f94cf8be..31f36457 100644 --- a/certora/scripts/verifyFlashMinter.sh +++ b/certora/scripts/verifyFlashMinter.sh @@ -11,8 +11,7 @@ certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol: MockFlashBorrower:AGho=GhoAToken \ --solc solc8.10 \ --optimistic_loop \ - --cloud \ - --settings -contractRecursionLimit=1 \ + --prover_args "-contractRecursionLimit 1" \ --rules "${@}" --msg "flashMinter check, rules ${@}" else @@ -27,8 +26,7 @@ certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol: MockFlashBorrower:AGho=GhoAToken \ --solc solc8.10 \ --optimistic_loop \ - --cloud \ - --settings -contractRecursionLimit=1 \ + --prover_args "-contractRecursionLimit 1" \ --msg "flashMinter check, all rules" fi diff --git a/certora/scripts/verifyGhoAToken.sh b/certora/scripts/verifyGhoAToken.sh index 0ebd7239..a66741bc 100644 --- a/certora/scripts/verifyGhoAToken.sh +++ b/certora/scripts/verifyGhoAToken.sh @@ -13,7 +13,6 @@ certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \ --link GhoVariableDebtToken:_ghoAToken=GhoAToken \ --solc solc8.10 \ --optimistic_loop \ - --cloud \ --rules "${@}" \ --msg "GhoAToken, rules ${@}" else @@ -28,6 +27,6 @@ certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \ --link GhoVariableDebtToken:_ghoAToken=GhoAToken \ --solc solc8.10 \ --optimistic_loop \ - --cloud \ + --send_only \ --msg "GhoAToken, all rules" fi diff --git a/certora/scripts/verifyGhoDiscountRateStrategy.sh b/certora/scripts/verifyGhoDiscountRateStrategy.sh index 2af609c0..5cb1db4a 100644 --- a/certora/scripts/verifyGhoDiscountRateStrategy.sh +++ b/certora/scripts/verifyGhoDiscountRateStrategy.sh @@ -5,8 +5,8 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr --solc solc8.10 \ --loop_iter 2 \ --optimistic_loop \ - --settings -t=500,-mediumTimeout=20,-depth=10 \ - --cloud \ + --prover_args "-mediumTimeout 20 -depth 10" \ + --smt_timeout 500 \ --rules "${@}" \ --msg "GhoDiscountRateStrategy, rules ${@}." else @@ -15,7 +15,7 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr --solc solc8.10 \ --loop_iter 2 \ --optimistic_loop \ - --settings -t=500,-mediumTimeout=20,-depth=10 \ - --cloud \ + --prover_args "-mediumTimeout 20 -depth 10" \ + --smt_timeout 500 \ --msg "GhoDiscountRateStrategy, all rules." fi diff --git a/certora/scripts/verifyGhoToken.sh b/certora/scripts/verifyGhoToken.sh index 255701fe..68705052 100644 --- a/certora/scripts/verifyGhoToken.sh +++ b/certora/scripts/verifyGhoToken.sh @@ -7,15 +7,13 @@ certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/co --solc solc8.10 \ --loop_iter 3 \ --optimistic_loop \ - --cloud \ --rules "${@}" \ - --msg "GhoToken, rules ${@}" + --msg "GhoToken workaround for CERT-1060, rules ${@}" else certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/contracts/gho/GhoToken.sol \ --verify GhoTokenHarness:certora/specs/ghoToken.spec \ --solc solc8.10 \ --loop_iter 3 \ --optimistic_loop \ - --cloud \ - --msg "GhoToken, all rules." + --msg "GhoToken, all rules. workaround for CERT-1060" fi \ No newline at end of file diff --git a/certora/scripts/verifyGhoVariableDebtToken.sh b/certora/scripts/verifyGhoVariableDebtToken.sh index 4b81782f..82215677 100644 --- a/certora/scripts/verifyGhoVariableDebtToken.sh +++ b/certora/scripts/verifyGhoVariableDebtToken.sh @@ -14,10 +14,11 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH --loop_iter 2 \ --solc solc8.10 \ --optimistic_loop \ - --settings -t=900,-mediumTimeout=30,-depth=15 \ - --cloud \ --rules "${@}" \ - --msg "GhoVariableDebtToken, rules ${@}." + --smt_timeout 900 \ + --prover_args "-mediumTimeout 30 -depth 15" \ + --msg "GhoVariableDebtToken" + else certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness \ certora/harness/DummyPool.sol \ @@ -31,8 +32,8 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH --loop_iter 2 \ --solc solc8.10 \ --optimistic_loop \ - --settings -t=900,-mediumTimeout=30,-depth=15 \ - --cloud \ - --msg "GhoVariableDebtToken, all rules." -fi + --smt_timeout 900 \ + --prover_args "-mediumTimeout 30 -depth 15" \ + --msg "GhoVariableDebtToken" +fi \ No newline at end of file diff --git a/certora/specs/VariableDebtToken.spec b/certora/specs/VariableDebtToken.spec index 92046709..c52c29a0 100644 --- a/certora/specs/VariableDebtToken.spec +++ b/certora/specs/VariableDebtToken.spec @@ -2,14 +2,14 @@ methods { // summarization for elimination the raymul operation in balance of and totalSupply. //getReserveNormalizedVariableDebt(address asset) returns (uint256) => indexAtTimestamp(e.block.timestamp) //setAdditionalData(address user, uint128 data) envfree - handleAction(address, uint256, uint256) => NONDET - scaledBalanceOfToBalanceOf(uint256) returns (uint256) envfree + function _.handleAction(address, uint256, uint256) external => NONDET; + function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; //balanceOf(address) returns (uint256) envfree } -definition ray() returns uint = 1000000000000000000000000000; // 10^27 -definition wad() returns uint = 1000000000000000000; // 10^18 -definition bound(uint256 index) returns uint = ((index / ray()) + 1 ) / 2; +definition ray() returns uint256 = 1000000000000000000000000000; // 10^27 +definition wad() returns uint256 = 1000000000000000000; // 10^18 +definition bound(uint256 index) returns mathint = ((index / ray()) + 1 ) / 2; // summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) // ghost gRNVB() returns uint256 { // axiom gRNVB() == 7 * ray(); @@ -17,20 +17,20 @@ definition bound(uint256 index) returns uint = ((index / ray()) + 1 ) / 2; /* Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. */ -definition bounded_error_eq(uint x, uint y, uint scale, uint256 index) returns bool = x <= y + (bound(index) * scale) && x + (bound(index) * scale) >= y; +definition bounded_error_eq(uint x, uint y, uint scale, uint256 index) returns bool = to_mathint(x) <= y + (bound(index) * scale) && x + (bound(index) * scale) >= to_mathint(y); definition disAllowedFunctions(method f) returns bool = - f.selector == transfer(address, uint256).selector || - f.selector == allowance(address, address).selector || - f.selector == approve(address, uint256).selector || - f.selector == transferFrom(address, address, uint256).selector || - f.selector == increaseAllowance(address, uint256).selector || - f.selector == decreaseAllowance(address, uint256).selector; + f.selector == sig:transfer(address, uint256).selector || + f.selector == sig:allowance(address, address).selector || + f.selector == sig:approve(address, uint256).selector || + f.selector == sig:transferFrom(address, address, uint256).selector || + f.selector == sig:increaseAllowance(address, uint256).selector || + f.selector == sig:decreaseAllowance(address, uint256).selector; -ghost sumAllBalance() returns uint256 { +ghost sumAllBalance() returns mathint { init_state axiom sumAllBalance() == 0; } @@ -62,8 +62,8 @@ rule whoChangeTotalSupply(method f) uint256 newTotalSupply = totalSupply(); assert oldTotalSupply != newTotalSupply => (e.msg.sender == POOL(e) && - (f.selector == burn(address, uint256, uint256).selector || - f.selector == mint(address, address, uint256, uint256).selector)); + (f.selector == sig:burn(address, uint256, uint256).selector || + f.selector == sig:mint(address, address, uint256, uint256).selector)); } /* @@ -121,7 +121,7 @@ rule nonceChangePermits(method f) calldataarg args; f(e, args); uint256 newNonce = nonces(e, user); - assert oldNonce != newNonce => f.selector == delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; + assert oldNonce != newNonce => f.selector == sig:delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; } // minting and then buring Variable Debt Token should have no effect on the users balance @@ -351,7 +351,7 @@ rule integrityMint_exact_should_fail(address a, uint256 x) { rule burnZeroDoesntChangeBalance(address u, uint256 index) { env e; uint256 balanceBefore = balanceOf(e, u); - invoke burn(e, u, 0, index); + burn@withrevert(e, u, 0, index); uint256 balanceAfter = balanceOf(e, u); assert balanceBefore == balanceAfter; } diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec index b12fec16..dfd8ea1d 100644 --- a/certora/specs/erc20.spec +++ b/certora/specs/erc20.spec @@ -1,12 +1,12 @@ // erc20 methods methods { - name() returns (string) => DISPATCHER(true) - symbol() returns (string) => DISPATCHER(true) - decimals() returns (string) => DISPATCHER(true) - totalSupply() returns (uint256) => DISPATCHER(true) - balanceOf(address) returns (uint256) => DISPATCHER(true) - allowance(address,address) returns (uint) => DISPATCHER(true) - approve(address,uint256) returns (bool) => DISPATCHER(true) - transfer(address,uint256) returns (bool) => DISPATCHER(true) - transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); } diff --git a/certora/specs/flashMinter.spec b/certora/specs/flashMinter.spec index 2c0a5eb1..eeb6240b 100644 --- a/certora/specs/flashMinter.spec +++ b/certora/specs/flashMinter.spec @@ -1,28 +1,28 @@ -using GhoToken as gho -using GhoAToken as atoken -using MockFlashBorrower as flashBorrower +using GhoToken as gho; +using GhoAToken as atoken; +using MockFlashBorrower as flashBorrower; methods{ - isPoolAdmin(address user) returns (bool) => retreivePoolAdminFromGhost(user) - isFlashBorrower(address user) returns (bool) => retreiveFlashBorrowerFromGhost(user) - onFlashLoan(address, address, uint256, uint256, bytes) returns (bytes32) => DISPATCHER(true) - getACLManager() returns (address) => NONDET + function _.isPoolAdmin(address user) external => retreivePoolAdminFromGhost(user) expect bool ALL; + function _.isFlashBorrower(address user) external => retreiveFlashBorrowerFromGhost(user) expect bool ALL; + function _.onFlashLoan(address, address, uint256, uint256, bytes) external => DISPATCHER(true); + function _.getACLManager() external => NONDET; // FlashBorrower - flashBorrower.action() returns (uint8) envfree - flashBorrower._transferTo() returns (address) envfree - gho.allowance(address, address) returns (uint256) envfree - burn(uint256) => DISPATCHER(true) - mint(address, uint256) => DISPATCHER(true) - transfer(address, uint256) returns (bool) => DISPATCHER(true) - balanceOf(address) returns (uint256) => DISPATCHER(true) + function flashBorrower.action() external returns (MockFlashBorrower.Action) envfree; + function flashBorrower._transferTo() external returns (address) envfree; + function gho.allowance(address, address) external returns (uint256) envfree; + function _.burn(uint256) external=> DISPATCHER(true); + function _.mint(address, uint256) external=> DISPATCHER(true); + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); - decreaseBalanceFromInterest(address, uint256) => NONDET - getBalanceFromInterest(address) => NONDET - gho.totalSupply() returns (uint256) envfree - gho.balanceOf(address) returns (uint256) envfree + function _.decreaseBalanceFromInterest(address, uint256) external => NONDET; + function _.getBalanceFromInterest(address) external => NONDET; + function gho.totalSupply() external returns (uint256) envfree; + function gho.balanceOf(address) external returns (uint256) envfree; - atoken.getGhoTreasury() returns (address) envfree + function atoken.getGhoTreasury() external returns (address) envfree; } // keeps track of users with pool admin permissions in order to return a consistent value per user @@ -48,20 +48,21 @@ function flashLoanReqs(env e){ // an assumption that demands the sum of balances of 3 given users is no more than the total supply function ghoBalanceOfTwoUsersLETotalSupply(address user1, address user2, address user3){ - require gho.balanceOf(user1) + gho.balanceOf(user2) + gho.balanceOf(user3) <= gho.totalSupply(); + require gho.balanceOf(user1) + gho.balanceOf(user2) + gho.balanceOf(user3) <= to_mathint(gho.totalSupply()); } /** * @title The GHO balance of the flash minter should grow when calling any function, excluding distributeFees */ rule balanceOfFlashMinterGrows(method f, env e, calldataarg args) - filtered { f -> f.selector != distributeFeesToTreasury().selector }{ + filtered { f -> f.selector != sig:distributeFeesToTreasury().selector }{ // No overflow of gho is possible ghoBalanceOfTwoUsersLETotalSupply(currentContract, e.msg.sender, atoken); flashLoanReqs(e); // excluding calls to distribute fees - require flashBorrower.action() != 1; + mathint action = assert_uint256(flashBorrower.action()); + require action != 1; uint256 _facilitatorBalance = gho.balanceOf(currentContract); @@ -133,7 +134,7 @@ rule integrityOfDistributeFeesToTreasury(){ */ rule feeSimulationEqualsActualFee(address receiver, address token, uint256 amount, bytes data){ env e; - uint256 feeSimulationResult = flashFee(e, token, amount); + mathint feeSimulationResult = flashFee(e, token, amount); uint256 _facilitatorBalance = gho.balanceOf(currentContract); flashLoanReqs(e); @@ -141,7 +142,8 @@ rule feeSimulationEqualsActualFee(address receiver, address token, uint256 amoun // No overflow of gho is possible ghoBalanceOfTwoUsersLETotalSupply(currentContract, e.msg.sender, atoken); // Excluding call to distributeFeesToTreasury & calling another flashloan (which will generate another fee in recursion) - require flashBorrower.action() != 1 && flashBorrower.action() != 0; + mathint borrower_action = assert_uint256(flashBorrower.action()); + require borrower_action != 1 && borrower_action != 0; // Because we calculate the actual fee by balance difference of the minter, we assume no extra money is being sent to the minter. require flashBorrower._transferTo() != currentContract; @@ -149,7 +151,16 @@ rule feeSimulationEqualsActualFee(address receiver, address token, uint256 amoun uint256 facilitatorBalance_ = gho.balanceOf(currentContract); - uint256 actualFee = facilitatorBalance_ - _facilitatorBalance; + mathint actualFee = facilitatorBalance_ - _facilitatorBalance; assert feeSimulationResult == actualFee; } + + +rule sanity { + env e; + calldataarg arg; + method f; + f(e, arg); + satisfy true; +} diff --git a/certora/specs/ghoAToken.spec b/certora/specs/ghoAToken.spec index 1682ec25..84913f25 100644 --- a/certora/specs/ghoAToken.spec +++ b/certora/specs/ghoAToken.spec @@ -1,40 +1,40 @@ -import "erc20.spec" +import "erc20.spec"; -using GhoTokenHarness as _ghoTokenHarness +using GhoTokenHarness as _ghoTokenHarness; methods{ - totalSupply() returns (uint256) envfree - RESERVE_TREASURY_ADDRESS() returns (address) envfree - UNDERLYING_ASSET_ADDRESS() returns (address) envfree - transferUnderlyingTo(address,uint256) - handleRepayment(address,address,uint256) - distributeFeesToTreasury() envfree - rescueTokens(address,address,uint256) - setVariableDebtToken(address) - getVariableDebtToken() returns (address) envfree - updateGhoTreasury(address) - getGhoTreasury() returns (address) envfree - _ghoTokenHarness.getFacilitatorBucketCapacity(address) returns (uint256) envfree - _ghoTokenHarness.getFacilitatorBucketLevel(address) returns (uint256) envfree - _ghoTokenHarness.balanceOf(address) returns (uint256) envfree - scaledBalanceOf(address) returns (uint256) envfree + function totalSupply() external returns (uint256) envfree; + function RESERVE_TREASURY_ADDRESS() external returns (address) envfree; + function UNDERLYING_ASSET_ADDRESS() external returns (address) envfree; + function transferUnderlyingTo(address,uint256) external; + function handleRepayment(address,address,uint256) external; + function distributeFeesToTreasury() external envfree ; + function rescueTokens(address,address,uint256) external; + function setVariableDebtToken(address) external; + function getVariableDebtToken() external returns (address) envfree; + function updateGhoTreasury(address) external ; + function getGhoTreasury() external returns (address) envfree; + function _ghoTokenHarness.getFacilitatorBucketCapacity(address) external returns (uint256) envfree; + function _ghoTokenHarness.getFacilitatorBucketLevel(address) external returns (uint256) envfree; + function _ghoTokenHarness.balanceOf(address) external returns (uint256) envfree; + function scaledBalanceOf(address) external returns (uint256) envfree; /******************* * Pool.sol * ********************/ - getReserveNormalizedIncome(address) returns (uint256) => CONSTANT + function _.getReserveNormalizedIncome(address) external => CONSTANT; /*********************************** * PoolAddressesProvider.sol * ************************************/ - getACLManager() returns(address) => CONSTANT + function _.getACLManager() external => CONSTANT; /************************ * ACLManager.sol * *************************/ - isPoolAdmin(address) returns(bool) => CONSTANT + function _.isPoolAdmin(address) external => CONSTANT; } @@ -77,10 +77,10 @@ rule transferUnderlyingToCantExceedCapacity() { address target; uint256 amount; env e; - uint256 facilitatorLevel = _ghoTokenHarness.getFacilitatorBucketLevel(currentContract); - uint256 facilitatorCapacity = _ghoTokenHarness.getFacilitatorBucketCapacity(currentContract); + mathint facilitatorLevel = _ghoTokenHarness.getFacilitatorBucketLevel(currentContract); + mathint facilitatorCapacity = _ghoTokenHarness.getFacilitatorBucketCapacity(currentContract); transferUnderlyingTo@withrevert(e, target, amount); - assert(amount > (facilitatorCapacity - facilitatorLevel) => lastReverted); + assert(to_mathint(amount) > (facilitatorCapacity - facilitatorLevel) => lastReverted); } @@ -95,7 +95,7 @@ rule totalSupplyAlwaysZero() { * @title Proves that any user's balance of GhoAToken is always zero **/ invariant userBalanceAlwaysZero(address user) - scaledBalanceOf(user) == 0 + scaledBalanceOf(user) == 0; @@ -148,6 +148,3 @@ rule level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepaym } - - - diff --git a/certora/specs/ghoDiscountRateStrategy.spec b/certora/specs/ghoDiscountRateStrategy.spec index 809aed55..39e13e1c 100644 --- a/certora/specs/ghoDiscountRateStrategy.spec +++ b/certora/specs/ghoDiscountRateStrategy.spec @@ -1,17 +1,17 @@ methods { - calculateDiscountRate(uint256, uint256) returns (uint256) envfree - MIN_DISCOUNT_TOKEN_BALANCE() returns (uint256) envfree - MIN_DEBT_TOKEN_BALANCE() returns (uint256) envfree - DISCOUNT_RATE() returns (uint256) envfree - GHO_DISCOUNTED_PER_DISCOUNT_TOKEN() returns (uint256) envfree - wadMul(uint256, uint256) returns (uint256) envfree + function calculateDiscountRate(uint256, uint256) external returns (uint256) envfree; + function MIN_DISCOUNT_TOKEN_BALANCE() external returns (uint256) envfree; + function MIN_DEBT_TOKEN_BALANCE() external returns (uint256) envfree; + function DISCOUNT_RATE() external returns (uint256) envfree; + function GHO_DISCOUNTED_PER_DISCOUNT_TOKEN() external returns (uint256) envfree; + function wadMul(uint256, uint256) external returns (uint256) envfree; } function wad() returns uint256 { return 10^18; } -function wadMulCVL(uint256 a, uint256 b) returns uint256 { - return to_uint256((a * b + (wad() / 2)) / wad()); +function wadMulCVL(uint256 a, uint256 b) returns mathint { + return ((a * b + (wad() / 2)) / wad()); } /** @@ -30,9 +30,9 @@ function wadMulCVL(uint256 a, uint256 b) returns uint256 { rule equivalenceOfWadMulCVLAndWadMulSol() { uint256 x; uint256 y; - uint256 wadMulCvl = wadMulCVL(x, y); + mathint wadMulCvl = wadMulCVL(x, y); uint256 wadMulSol = wadMul(x, y); - assert(wadMulCvl == wadMulSol); + assert(wadMulCvl == to_mathint(wadMulSol)); } /** @@ -41,11 +41,11 @@ rule equivalenceOfWadMulCVLAndWadMulSol() { rule maxDiscountForHighDiscountTokenBalance() { uint256 debtBalance; uint256 discountTokenBalance; - uint256 discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); + mathint discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); uint256 rate = calculateDiscountRate(debtBalance, discountTokenBalance); // forcing the debt/discount token balance to be above the minimal value allowed in order to get a non-zero rate require(debtBalance >= MIN_DEBT_TOKEN_BALANCE() && discountTokenBalance >= MIN_DISCOUNT_TOKEN_BALANCE()); - assert(discountedBalance >= debtBalance => rate == DISCOUNT_RATE()); + assert(discountedBalance >= to_mathint(debtBalance) => rate == DISCOUNT_RATE()); } /** @@ -55,7 +55,7 @@ rule zeroDiscountForSmallDiscountTokenBalance() { uint256 debtBalance; uint256 discountTokenBalance; uint256 rate = calculateDiscountRate(debtBalance, discountTokenBalance); - uint256 discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); + mathint discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); // there are three conditions that can result in a zero rate: // 1,2 - if the debt balance or the discount token balance are below some threashold. // 3 - if debtBalance is much larger than discountBalance (since the return value is the max rate multiplied @@ -63,7 +63,7 @@ rule zeroDiscountForSmallDiscountTokenBalance() { assert( (debtBalance < MIN_DEBT_TOKEN_BALANCE() || discountTokenBalance < MIN_DISCOUNT_TOKEN_BALANCE() || - discountedBalance*DISCOUNT_RATE() < debtBalance) + discountedBalance*DISCOUNT_RATE() < to_mathint(debtBalance)) <=> rate == 0); } @@ -74,10 +74,10 @@ rule zeroDiscountForSmallDiscountTokenBalance() { rule partialDiscountForIntermediateTokenBalance() { uint256 debtBalance; uint256 discountTokenBalance; - uint256 discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); + mathint discountedBalance = wadMulCVL(GHO_DISCOUNTED_PER_DISCOUNT_TOKEN(), discountTokenBalance); uint256 rate = calculateDiscountRate(debtBalance, discountTokenBalance); require(debtBalance >= MIN_DEBT_TOKEN_BALANCE() && discountTokenBalance >= MIN_DISCOUNT_TOKEN_BALANCE()); - assert(discountedBalance < debtBalance => (rate == (discountedBalance * DISCOUNT_RATE()) / debtBalance)); + assert(discountedBalance < to_mathint(debtBalance) => (to_mathint(rate) == (discountedBalance * DISCOUNT_RATE()) / debtBalance)); } /** @@ -90,3 +90,11 @@ rule limitOnDiscountRate() { assert(discountRate <= DISCOUNT_RATE()); } + +rule sanity { + env e; + calldataarg arg; + method f; + f(e, arg); + satisfy true; +} diff --git a/certora/specs/ghoToken.spec b/certora/specs/ghoToken.spec index 358d9838..30411d79 100644 --- a/certora/specs/ghoToken.spec +++ b/certora/specs/ghoToken.spec @@ -1,30 +1,23 @@ -import "set.spec" +import "set.spec"; -using GhoToken as GHOTOKEN +using GhoToken as GHOTOKEN; methods{ - FACILITATOR_MANAGER() returns bytes32 envfree - BUCKET_MANAGER() returns bytes32 envfree - hasRole(bytes32, address) returns bool envfree - - mint(address,uint256) - burn(uint256) - removeFacilitator(address) - setFacilitatorBucketCapacity(address,uint128) + function mint(address,uint256) external; + function burn(uint256) external; + function removeFacilitator(address) external; + function setFacilitatorBucketCapacity(address,uint128) external; - totalSupply() returns uint256 envfree - balanceOf(address) returns (uint256) envfree - getFacilitatorBucketLevel(address) returns uint256 envfree - getFacilitatorBucketCapacity(address) returns uint256 envfree + function totalSupply() external returns uint256 envfree; + function balanceOf(address) external returns (uint256) envfree; + function getFacilitatorBucketLevel(address) external returns uint256 envfree; + function getFacilitatorBucketCapacity(address) external returns uint256 envfree; - is_in_facilitator_mapping(address) returns bool envfree - is_in_facilitator_set_map(address) returns bool envfree - is_in_facilitator_set_array(address) returns bool envfree - to_bytes32(address) returns (bytes32) envfree + function is_in_facilitator_mapping(address) external returns bool envfree; + function is_in_facilitator_set_map(address) external returns bool envfree; + function is_in_facilitator_set_array(address) external returns bool envfree; + //function to_bytes32(address) external returns (bytes32) envfree; } -/** - * @title Sum of balances of underlying asset (GhoToken) - **/ ghost sumAllBalance() returns mathint { init_state axiom sumAllBalance() == 0; } @@ -34,13 +27,10 @@ hook Sstore balanceOf[KEY address a] uint256 balance (uint256 old_balance) STORA } hook Sload uint256 balance balanceOf[KEY address a] STORAGE { - require balance <= sumAllBalance(); + require to_mathint(balance) <= sumAllBalance(); } -/** - * @title Sum of facilitators' bucket levels - **/ ghost sumAllLevel() returns mathint { init_state axiom sumAllLevel() == 0; } @@ -66,7 +56,7 @@ hook Sstore _facilitators[KEY address a].(offset 16) uint128 level (uint128 old_ * @dev the proof of the assumption is vacuous because length > loop_iter */ invariant length_leq_max_uint160() - getFacilitatorsListLen() < TWO_TO_160() + getFacilitatorsListLen() < TWO_TO_160(); // INV #2 /** @@ -85,7 +75,7 @@ invariant inv_balanceOf_leq_totalSupply(address user) * @title Sum of bucket levels is equals to GhoToken::totalSupply() **/ invariant total_supply_eq_sumAllLevel() - sumAllLevel() == totalSupply() + sumAllLevel() == to_mathint(totalSupply()) { preserved burn(uint256 amount) with (env e){ requireInvariant inv_balanceOf_leq_totalSupply(e.msg.sender); @@ -100,7 +90,7 @@ invariant total_supply_eq_sumAllLevel() **/ //todo: replace preserve invariant sumAllBalance_eq_totalSupply() - sumAllBalance() == totalSupply() + sumAllBalance() == to_mathint(totalSupply()) { preserved { requireInvariant sumAllLevel_eq_sumAllBalance(); @@ -128,7 +118,7 @@ invariant sumAllLevel_eq_sumAllBalance() * @title A facilitator with a positive bucket capacity exists in the _facilitators mapping */ invariant inv_valid_capacity(address facilitator) - ((getFacilitatorBucketCapacity(facilitator)>0) => is_in_facilitator_mapping(facilitator) ) + ((getFacilitatorBucketCapacity(facilitator)>0) => is_in_facilitator_mapping(facilitator) ); // INV #7 /** @@ -200,7 +190,7 @@ rule level_leq_capacity(address facilitator, method f) filtered {f -> !f.isView} requireInvariant inv_valid_capacity(facilitator); require getFacilitatorBucketLevel(facilitator) <= getFacilitatorBucketCapacity(facilitator); f(e, arg); - assert ((f.selector != setFacilitatorBucketCapacity(address,uint128).selector) + assert ((f.selector != sig:setFacilitatorBucketCapacity(address,uint128).selector) => (getFacilitatorBucketLevel(facilitator) <= getFacilitatorBucketCapacity(facilitator))); } @@ -218,23 +208,20 @@ rule mint_after_burn(method f) filtered {f -> !f.isView} address account; require getFacilitatorBucketLevel(e.msg.sender) <= getFacilitatorBucketCapacity(e.msg.sender); - + require amount_mint > 0; requireInvariant addressSetInvariant(); requireInvariant inv_balanceOf_leq_totalSupply(e.msg.sender); requireInvariant inv_valid_capacity(e.msg.sender); - require amount_mint > 0; - burn(e, amount_burn); f(e, arg); mint@withrevert(e, account, amount_mint); assert (((amount_mint <= amount_burn) - && f.selector != mint(address,uint256).selector - && f.selector != setFacilitatorBucketCapacity(address,uint128).selector - && f.selector != removeFacilitator(address).selector + && f.selector != sig:mint(address,uint256).selector + && f.selector != sig:setFacilitatorBucketCapacity(address,uint128).selector + && f.selector != sig:removeFacilitator(address).selector ) => !lastReverted), "mint failed"; - } /** @@ -287,7 +274,7 @@ rule level_after_mint() uint256 levelBefore = getFacilitatorBucketLevel(e.msg.sender); mint(e, account, amount); uint256 leveAfter = getFacilitatorBucketLevel(e.msg.sender); - assert levelBefore + amount == leveAfter; + assert levelBefore + amount == to_mathint(leveAfter); } @@ -300,7 +287,7 @@ rule level_after_burn() uint256 levelBefore = getFacilitatorBucketLevel(e.msg.sender); burn(e, amount); uint256 leveAfter = getFacilitatorBucketLevel(e.msg.sender); - assert levelBefore == leveAfter + amount; + assert to_mathint(levelBefore) == leveAfter + amount; } @@ -333,7 +320,7 @@ rule getFacilitatorBucketCapacity_after_setFacilitatorBucketCapacity(){ uint128 newCapacity; setFacilitatorBucketCapacity(e, facilitator, newCapacity); - assert getFacilitatorBucketCapacity(facilitator) == newCapacity; + assert getFacilitatorBucketCapacity(facilitator) == require_uint256(newCapacity); } /** @@ -367,9 +354,9 @@ rule facilitator_in_list_after_mint_and_burn(method f){ requireInvariant addr_in_set_list_iff_in_map(e.msg.sender); f(e,args); - assert (((f.selector == mint(address,uint256).selector) || (f.selector == burn(uint256).selector)) => is_in_facilitator_mapping(e.msg.sender)); - assert (((f.selector == mint(address,uint256).selector) || (f.selector == burn(uint256).selector)) => is_in_facilitator_set_map(e.msg.sender)); - assert (((f.selector == mint(address,uint256).selector) || (f.selector == burn(uint256).selector)) => is_in_facilitator_set_array(e.msg.sender)); + assert (((f.selector == sig:mint(address,uint256).selector) || (f.selector == sig:burn(uint256).selector)) => is_in_facilitator_mapping(e.msg.sender)); + assert (((f.selector == sig:mint(address,uint256).selector) || (f.selector == sig:burn(uint256).selector)) => is_in_facilitator_set_map(e.msg.sender)); + assert (((f.selector == sig:mint(address,uint256).selector) || (f.selector == sig:burn(uint256).selector)) => is_in_facilitator_set_array(e.msg.sender)); } /** @@ -424,8 +411,8 @@ rule balance_after_mint() { mint(e, user, amount); uint256 finBalance = balanceOf(user); uint256 finSupply = totalSupply(); - assert initBalance + amount == finBalance; - assert initSupply + amount == finSupply; + assert initBalance + amount == to_mathint(finBalance); + assert initSupply + amount == to_mathint(finSupply); } rule balance_after_burn() { @@ -438,8 +425,8 @@ rule balance_after_burn() { burn(e, amount); uint256 finBalance = balanceOf(e.msg.sender); uint256 finSupply = totalSupply(); - assert initBalance == finBalance + amount; - assert initSupply == finSupply + amount ; + assert to_mathint(initBalance) == finBalance + amount; + assert to_mathint(initSupply) == finSupply + amount ; } /** @@ -475,7 +462,7 @@ rule mintLimitedByFacilitatorRemainingCapacity() { require(getFacilitatorBucketCapacity(e.msg.sender) > getFacilitatorBucketLevel(e.msg.sender)); uint256 amount; - require(amount > (getFacilitatorBucketCapacity(e.msg.sender) - getFacilitatorBucketLevel(e.msg.sender))); + require(to_mathint(amount) > (getFacilitatorBucketCapacity(e.msg.sender) - getFacilitatorBucketLevel(e.msg.sender))); address user; mint@withrevert(e, user, amount); assert lastReverted; @@ -536,39 +523,8 @@ rule address_not_in_list_after_removeFacilitator_CASE_SPLIT_zero_address(address assert !is_in_facilitator_set_array(facilitator); } -// if facilitator exist it has to remain exist unless facilitator manager calls an action -// if facilitator not exist it has to remain not exist unless facilitator manager calls an action -rule OnlyFacilitatorManagerAlterFacilitatorExistence(){ - env e; - address facilitator; - bool _facilitatorExist = is_in_facilitator_mapping(facilitator); - bool isSenderManager = hasRole(FACILITATOR_MANAGER(), e.msg.sender); - - method f; calldataarg args; - f(e, args); - - bool facilitatorExist_ = is_in_facilitator_mapping(facilitator); - - assert (_facilitatorExist && !isSenderManager) => facilitatorExist_; - assert (!_facilitatorExist && !isSenderManager) => !facilitatorExist_; -} -// facilitator exist && msg.sender != checkrole(bucketManager) => getBucketCapacity_ == _getBucketCapacity -rule OnlyBucketManagerCanChangeCapacity(){ - env e; - address facilitator; - bool _facilitatorExist = is_in_facilitator_mapping(facilitator); - uint256 _bucketCapacity = getFacilitatorBucketCapacity(facilitator); - bool isSenderBucketManager = hasRole(BUCKET_MANAGER(), e.msg.sender); - bool isSenderFacilitatorManager = hasRole(FACILITATOR_MANAGER(), e.msg.sender); - - - method f; calldataarg args; - f(e, args); - - uint256 bucketCapacity_ = getFacilitatorBucketCapacity(facilitator); - - assert (_facilitatorExist && !isSenderBucketManager) => - ((bucketCapacity_ == _bucketCapacity) || - (isSenderFacilitatorManager && bucketCapacity_ == 0)); -} \ No newline at end of file + + + + diff --git a/certora/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index f4ad6810..4087de00 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -1,87 +1,88 @@ //import "erc20.spec" -import "VariableDebtToken.spec" -import "summarizations.spec" +import "VariableDebtToken.spec"; +import "summarizations.spec"; -using GhoDiscountRateStrategy as discStrategy +using GhoDiscountRateStrategy as discStrategy; methods{ - /******************** - * WadRayMath.sol * + /********************; + * WadRayMath.sol *; *********************/ - rayMul(uint256 x, uint256 y) returns (uint256) envfree - rayDiv(uint256 x, uint256 y) returns uint256 envfree + // function _.rayMul(uint256 x, uint256 y) internal => rayMulSummariztion(x, y) expect(uint256); + function rayDiv(uint256 x, uint256 y) external returns uint256 envfree; + function rayMul(uint256 x, uint256 y) external returns uint256 envfree; - /*********************************** - * PoolAddressesProvider.sol * + /***********************************; + * PoolAddressesProvider.sol *; ************************************/ - getACLManager() returns(address) => CONSTANT + function _.getACLManager() external => CONSTANT; - /************************ - * ACLManager.sol * + /************************; + * ACLManager.sol *; *************************/ - isPoolAdmin(address) returns(bool) => CONSTANT + function _.isPoolAdmin(address) external => CONSTANT; - /****************************************************************** - * DummyERC20WithTimedBalanceOf.sol (linked to _discountToken) * + /******************************************************************; + * DummyERC20WithTimedBalanceOf.sol (linked to _discountToken) *; *******************************************************************/ // Internal function in DummyERC20WithTimedBalanceOf which exposes the block's timestamp and called by DummyERC20WithTimedBalanceOf::balanceOf - _balanceOfWithBlockTimestamp(address user, uint256 ts) returns (uint256) envfree => balanceOfDiscountTokenAtTimestamp(user, ts) + function _._balanceOfWithBlockTimestamp(address user, uint256 ts) internal => balanceOfDiscountTokenAtTimestamp(user, ts) expect uint256; - /************************************ - * DummyPool.sol (linked to POOL) * + /************************************; + * DummyPool.sol (linked to POOL) *; *************************************/ // Internal function in DummyPool which exposes the block's timestamp and called by Pool::getReserveNormalizedVariableDebt - _getReserveNormalizedVariableDebtWithBlockTimestamp(address asset, uint256 timestamp) returns (uint256) => indexAtTimestamp(timestamp) + function _._getReserveNormalizedVariableDebtWithBlockTimestamp(address asset, uint256 timestamp) internal => indexAtTimestamp(timestamp) expect uint256; - /************************************ - * GhoVariableDebtTokenHarness.sol * + /************************************; + * GhoVariableDebtTokenHarness.sol *; *************************************/ - discStrategy.calculateDiscountRate(uint256, uint256) returns (uint256) envfree + function discStrategy.calculateDiscountRate(uint256, uint256) external returns (uint256) envfree; - /************************************ - * GhoVariableDebtTokenHarness.sol * + /************************************; + * GhoVariableDebtTokenHarness.sol *; *************************************/ - getUserCurrentIndex(address) returns (uint256) envfree - getUserDiscountRate(address) returns (uint256) envfree - getUserAccumulatedDebtInterest(address) envfree - getBalanceOfDiscountToken(address) returns (uint256) + function getUserCurrentIndex(address) external returns (uint256) envfree; + function getUserDiscountRate(address) external returns (uint256) envfree; + function getUserAccumulatedDebtInterest(address) external returns (uint256) envfree; + function getBalanceOfDiscountToken(address) external returns (uint256); - /******************************** - * GhoVariableDebtToken.sol * + /********************************; + * GhoVariableDebtToken.sol *; *********************************/ - totalSupply() returns(uint256) envfree - balanceOf(address) returns (uint256) - mint(address, address, uint256, uint256) returns (bool, uint256) - burn(address ,uint256 ,uint256) returns (uint256) - scaledBalanceOf(address) returns (uint256) envfree - getBalanceFromInterest(address) returns (uint256) envfree - rebalanceUserDiscountPercent(address) - updateDiscountDistribution(address ,address ,uint256 ,uint256 ,uint256) + function totalSupply() external returns(uint256) envfree; + function balanceOf(address) external returns (uint256); + function mint(address, address, uint256, uint256) external returns (bool, uint256); + function burn(address ,uint256 ,uint256) external returns (uint256); + function scaledBalanceOf(address) external returns (uint256) envfree; + function getBalanceFromInterest(address) external returns (uint256) envfree; + function rebalanceUserDiscountPercent(address) external; + function updateDiscountDistribution(address ,address ,uint256 ,uint256 ,uint256) external; } /** * CVL implementation of rayMul **/ -function rayMulCVL(uint256 a, uint256 b) returns uint256 { - return to_uint256((a * b + (ray() / 2)) / ray()); +function rayMulCVL(uint256 a, uint256 b) returns mathint { + return ((a * b + (ray() / 2)) / ray()); } -function rayDivCVL(uint256 a, uint256 b) returns uint256 { - return to_uint256((a * ray() + (b / 2)) / b); +function rayDivCVL(uint256 a, uint256 b) returns mathint { + return ((a * ray() + (b / 2)) / b); } -function getReserveNormalizedVariableDebt_1ray() returns uint256 { +function getReserveNormalizedVariableDebt_1ray() returns mathint { return ray(); } function getReserveNormalizedVariableDebt_1or2ray() returns uint256 { - uint256 index; havoc index; - require (index==ray() || index==2*ray()); + uint256 index; + require (index==ray() || to_mathint(index)==2*ray()); return index; } function getReserveNormalizedVariableDebt_7ray() returns uint256 { - uint256 index; havoc index; - require (index==7*ray()); + uint256 index; + require (to_mathint(index)==7*ray()); return index; } @@ -89,14 +90,16 @@ function getReserveNormalizedVariableDebt_7ray() returns uint256 { definition MAX_DISCOUNT() returns uint256 = 10000; // equals to 100% discount, in points -ghost mapping(uint256 => mapping (uint256 => uint256)) discount_ghost; +ghost mapping(address => mapping (uint256 => uint256)) discount_ghost; ghost mapping(uint256 => uint256) index_ghost; /** * Query index_ghost for the index value at the input timestamp **/ function indexAtTimestamp(uint256 timestamp) returns uint256 { - return index_ghost[timestamp]; + require index_ghost[timestamp] >= ray(); + return index_ghost[timestamp]; + // return 1001684385021630839436707910;//index_ghost[timestamp]; } /** @@ -130,7 +133,7 @@ invariant discountCantExceed100Percent(address user) * Imported rules from VariableDebtToken.spec **/ //pass -use rule disallowedFunctionalities +use rule disallowedFunctionalities; /** * @title proves that a user's discount rate can be updated only by calling rebalanceUserDiscountPercent @@ -147,14 +150,14 @@ use rule disallowedFunctionalities // uint256 discRateAfter = getUserDiscountRate(user); -// assert(discRateAfter != discRateBefore => f.selector == rebalanceUserDiscountPercent(address).selector); +// assert(discRateAfter != discRateBefore => f.selector == sig:rebalanceUserDiscountPercent(address).selector); // } /** * @title proves that the user's balance of debt token (as reported by GhoVariableDebtToken::balanceOf) can't increase by calling any external non-mint function. **/ //pass -rule nonMintFunctionCantIncreaseBalance(method f) filtered { f-> f.selector != mint(address, address, uint256, uint256).selector } { +rule nonMintFunctionCantIncreaseBalance(method f) filtered { f-> f.selector != sig:mint(address, address, uint256, uint256).selector } { address user; uint256 ts1; uint256 ts2; @@ -170,8 +173,8 @@ rule nonMintFunctionCantIncreaseBalance(method f) filtered { f-> f.selector != m uint256 balanceBeforeOp = balanceOf(e, user); calldataarg args; f(e,args); - uint256 balanceAfterOp = balanceOf(e, user); - uint256 allowedDiff = indexAtTimestamp(ts2) / ray(); + mathint balanceAfterOp = balanceOf(e, user); + mathint allowedDiff = indexAtTimestamp(ts2) / ray(); // assert(balanceAfterOp != balanceBeforeOp + allowedDiff + 1); assert(balanceAfterOp <= balanceBeforeOp + allowedDiff); } @@ -180,7 +183,7 @@ rule nonMintFunctionCantIncreaseBalance(method f) filtered { f-> f.selector != m * @title proves that a call to a non-mint operation won't increase the user's balance of the actual debt tokens (i.e. it's scaled balance) **/ // pass -rule nonMintFunctionCantIncreaseScaledBalance(method f) filtered { f-> f.selector != mint(address, address, uint256, uint256).selector } { +rule nonMintFunctionCantIncreaseScaledBalance(method f) filtered { f-> f.selector != sig:mint(address, address, uint256, uint256).selector } { address user; uint256 ts1; uint256 ts2; @@ -238,10 +241,10 @@ rule onlyCertainFunctionsCanModifyScaledBalance(method f) { f(e,args); uint256 balanceAfterOp = scaledBalanceOf(user); assert(balanceAfterOp != balanceBeforeOp => ( - (f.selector == mint(address ,address ,uint256 ,uint256).selector) || - (f.selector == burn(address ,uint256 ,uint256).selector) || - (f.selector == updateDiscountDistribution(address ,address ,uint256 ,uint256 ,uint256).selector) || - (f.selector == rebalanceUserDiscountPercent(address).selector))); + (f.selector == sig:mint(address ,address ,uint256 ,uint256).selector) || + (f.selector == sig:burn(address ,uint256 ,uint256).selector) || + (f.selector == sig:updateDiscountDistribution(address ,address ,uint256 ,uint256 ,uint256).selector) || + (f.selector == sig:rebalanceUserDiscountPercent(address).selector))); } /** @@ -263,7 +266,7 @@ rule userAccumulatedDebtInterestWontDecrease(method f) { calldataarg args; f(e2,args); uint256 finAccumulatedInterest = getUserAccumulatedDebtInterest(user); - assert(initAccumulatedInterest > finAccumulatedInterest => f.selector == decreaseBalanceFromInterest(address, uint256).selector); + assert(initAccumulatedInterest > finAccumulatedInterest => f.selector == sig:decreaseBalanceFromInterest(address, uint256).selector); } /** @@ -271,34 +274,17 @@ rule userAccumulatedDebtInterestWontDecrease(method f) { **/ // pass rule userCantNullifyItsDebt(method f) { - address user; - uint256 ts1; - env e1 = envAtTimestamp(ts1); - uint256 ts2; - require(ts2 >= ts1); - env e2 = envAtTimestamp(ts2); - uint256 ts3; - require(ts3 >= ts2); - env e3 = envAtTimestamp(ts3); - // Forcing the index to be fixed (otherwise the rule times out). For non-fixed index replace `==` with `>=` - require((indexAtTimestamp(ts1) >= ray()) && - (indexAtTimestamp(ts2) == indexAtTimestamp(ts1)) && - (indexAtTimestamp(ts3) == indexAtTimestamp(ts2))); - - uint256 i1 = indexAtTimestamp(ts1); - uint256 i3 = indexAtTimestamp(ts3); - - require(getUserCurrentIndex(user) == indexAtTimestamp(ts1)); + address user; + env e; + env e2; + require(getUserCurrentIndex(user) == indexAtTimestamp(e.block.timestamp)); requireInvariant discountCantExceed100Percent(user); - uint256 balanceBeforeOp = balanceOf(e1, user); - uint256 initScaledBalance = scaledBalanceOf(user); + uint256 balanceBeforeOp = balanceOf(e, user); calldataarg args; + require e2.block.timestamp == e.block.timestamp; f(e2,args); - - uint256 balanceAfterOp = balanceOf(e3, user); - uint256 balanceIncrease = balanceAfterOp - balanceBeforeOp; - - assert((balanceBeforeOp > 0 && balanceAfterOp == 0) => (f.selector == burn(address, uint256, uint256).selector)); + uint256 balanceAfterOp = balanceOf(e, user); + assert((balanceBeforeOp > 0 && balanceAfterOp == 0) => (f.selector == sig:burn(address, uint256, uint256).selector)); } /*************************************************************** @@ -350,8 +336,8 @@ rule integrityOfMint_updateScaledBalance_fixedIndex() { mint(e, caller, user, amount, index); uint256 balanceAfter = balanceOf(e, user); - uint256 scaledBalanceAfter = scaledBalanceOf(user); - uint256 scaledAmount = rayDivCVL(amount, index); + mathint scaledBalanceAfter = scaledBalanceOf(user); + mathint scaledAmount = rayDivCVL(amount, index); assert(scaledBalanceAfter == scaledBalanceBefore + scaledAmount); } @@ -376,28 +362,17 @@ rule integrityOfMint_userIsolation() { /** * @title proves that when calling mint, the user's balance (as reported by GhoVariableDebtToken::balanceOf) will increase if the call is made on bahalf of the user. **/ -//pass rule onlyMintForUserCanIncreaseUsersBalance() { address user1; - address user2; - address user3; - uint256 ts1; - uint256 ts2; - require(ts2 >= ts1); - // Forcing the index to be fixed (otherwise the rule times out). For non-fixed index replace `==` with `>=` - require((indexAtTimestamp(ts1) >= ray()) && - (indexAtTimestamp(ts2) == indexAtTimestamp(ts1))); - + env e; + require(getUserCurrentIndex(user1) == indexAtTimestamp(e.block.timestamp)); - require(getUserCurrentIndex(user1) == indexAtTimestamp(ts1)); - env e = envAtTimestamp(ts2); uint256 finBalanceBeforeMint = balanceOf(e, user1); uint256 amount; - uint256 index = indexAtTimestamp(ts2); - mint(e,user2, user3, amount, index); + mint(e,user1, user1, amount, indexAtTimestamp(e.block.timestamp)); uint256 finBalanceAfterMint = balanceOf(e, user1); - assert(user3 == user1 => finBalanceAfterMint != finBalanceBeforeMint); + assert(finBalanceAfterMint != finBalanceBeforeMint); } /** @@ -435,7 +410,7 @@ rule onlyMintForUserCanIncreaseUsersBalance() { // } //pass -use rule integrityMint_atoken +use rule integrityMint_atoken; /*************************************************************** * Integrity of Burn @@ -468,32 +443,10 @@ rule integrityOfBurn_updateIndex() { assert(getUserCurrentIndex(user) == index); } -/** -* @title proves that on a fixed index calling burn(user, amount) will decrease the user's scaled balance by amount. -**/ -// pass -rule integrityOfBurn_fixedIndex() { - address user; - env e; - uint256 balanceBefore = balanceOf(e, user); - uint256 scaledBalanceBefore = scaledBalanceOf(user); - address caller; - uint256 amount; - uint256 index = indexAtTimestamp(e.block.timestamp); - require(getUserCurrentIndex(user) == index); - burn(e, user, amount, index); - - uint256 balanceAfter = balanceOf(e, user); - uint256 scaledBalanceAfter = scaledBalanceOf(user); - uint256 scaledAmount = rayDivCVL(amount, index); - - assert(scaledBalanceAfter == scaledBalanceBefore - scaledAmount); -} - /** * @title proves that calling burn with 0 amount doesn't change the user's balance **/ -use rule burnZeroDoesntChangeBalance +use rule burnZeroDoesntChangeBalance; /** * @title proves a concrete case of repaying the full debt that ends with a zero balance @@ -504,8 +457,8 @@ rule integrityOfBurn_fullRepay_concrete() { uint256 currentDebt = balanceOf(e, user); uint256 index = indexAtTimestamp(e.block.timestamp); require(getUserCurrentIndex(user) == ray()); - require(index == 2*ray()); - require(scaledBalanceOf(user) == 4*ray()); + require(to_mathint(index) == 2*ray()); + require(to_mathint(scaledBalanceOf(user)) == 4*ray()); burn(e, user, currentDebt, index); uint256 scaled = scaledBalanceOf(user); assert(scaled == 0); @@ -668,8 +621,8 @@ rule integrityOfBalanceOf_noDiscount() { env e; uint256 scaledBalance = scaledBalanceOf(user); uint256 currentIndex = indexAtTimestamp(e.block.timestamp); - uint256 expectedBalance = rayMulCVL(scaledBalance, currentIndex); - assert(balanceOf(e, user) == expectedBalance); + mathint expectedBalance = rayMulCVL(scaledBalance, currentIndex); + assert(to_mathint(balanceOf(e, user)) == expectedBalance); } /** @@ -681,4 +634,12 @@ rule integrityOfBalanceOf_zeroScaledBalance() { uint256 scaledBalance = scaledBalanceOf(user); require(scaledBalance == 0); assert(balanceOf(e, user) == 0); -} \ No newline at end of file +} + +rule burnAllDebtReturnsZeroDebt(address user) { + env e; + uint256 _variableDebt = balanceOf(e, user); + burn(e, user, _variableDebt, indexAtTimestamp(e.block.timestamp)); + uint256 variableDebt_ = balanceOf(e, user); + assert(variableDebt_ == 0); +} diff --git a/certora/specs/set.spec b/certora/specs/set.spec index 01f4f77b..ab634a5f 100644 --- a/certora/specs/set.spec +++ b/certora/specs/set.spec @@ -1,98 +1,85 @@ - - -/** - * @title get Set array length - * @dev user should define getFacilitatorsListLen() in Solidity harness file. - */ methods{ - getFacilitatorsListLen() returns (uint256) envfree + function getFacilitatorsListLen() external returns (uint256) envfree; } -/** -* @title max uint256 -* @return 2^256-1 -*/ + definition MAX_UINT256() returns uint256 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; -definition MAX_UINT256Bytes32() returns bytes32 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; //todo: remove once CERT-1060 is resolved +definition MAX_UINT256Bytes32() returns bytes32 = to_bytes32(0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); //todo: remove once CERT-1060 is resolved -/** -* @title max address value + 1 -* @return 2^160 -*/ definition TWO_TO_160() returns uint256 = 0x10000000000000000000000000000000000000000; /** -* @title Set map entries point to valid array entries +* Set map entries point to valid array entries * @notice an essential condition of the set, should hold for evert Set implementation * @return true if all map entries points to valid indexes of the array. */ definition MAP_POINTS_INSIDE_ARRAY() returns bool = forall bytes32 a. mirrorMap[a] <= mirrorArrayLen; /** -* @title Set map is the inverse function of set array. +* Set map is the inverse function of set array. * @notice an essential condition of the set, should hold for evert Set implementation * @notice this condition depends on the other set conditions, but the other conditions do not depend on this condition. * If this condition is omitted the rest of the conditions still hold, but the other conditions are required to prove this condition. * @return true if for every valid index of the array it holds that map(array(index)) == index + 1. */ -definition MAP_IS_INVERSE_OF_ARRAY() returns bool = forall uint256 i. (i < mirrorArrayLen) => (mirrorMap[mirrorArray[i]]) == to_uint256(i + 1); +definition MAP_IS_INVERSE_OF_ARRAY() returns bool = forall uint256 i. (i < mirrorArrayLen) => to_mathint(mirrorMap[mirrorArray[i]]) == i + 1; /** -* @title Set array is the inverse function of set map +* Set array is the inverse function of set map * @notice an essential condition of the set, should hold for evert Set implementation * @return true if for every non-zero bytes32 value stored in in the set map it holds that array(map(value) - 1) == value */ -definition ARRAY_IS_INVERSE_OF_MAP() returns bool = forall bytes32 a. (mirrorMap[a] != 0) => (mirrorArray[to_uint256(mirrorMap[a]-1)] == a); +definition ARRAY_IS_INVERSE_OF_MAP() returns bool = forall bytes32 a. forall uint256 b. to_mathint(b) == mirrorMap[a]-1 => (mirrorMap[a] != 0) => (mirrorArray[b] == a); /** -* @title load array length +* load array length * @notice a dummy condition that forces load of array length, using it forces initialization of mirrorArrayLen * @return always true */ definition CVL_LOAD_ARRAY_LENGTH() returns bool = (getFacilitatorsListLen() == getFacilitatorsListLen()); /** -* @title Set-general condition, encapsulating all conditions of Set +* Set-general condition, encapsulating all conditions of Set * @notice this condition recaps the general characteristics of Set. It should hold for all set implementations i.e. AddressSet, UintSet, Bytes32Set * @return conjunction of the Set three essential properties. */ definition SET_INVARIANT() returns bool = MAP_POINTS_INSIDE_ARRAY() && MAP_IS_INVERSE_OF_ARRAY() && ARRAY_IS_INVERSE_OF_MAP() && CVL_LOAD_ARRAY_LENGTH(); /** - * @title Size of stored value does not exceed the size of an address type. + * Size of stored value does not exceed the size of an address type. * @notice must be used for AddressSet, must not be used for Bytes32Set, UintSet * @return true if all array entries are less than 160 bits. **/ -definition VALUE_IN_BOUNDS_OF_TYPE_ADDRESS() returns bool = (forall uint256 i. to_uint256(mirrorArray[i]) < TWO_TO_160()); +definition VALUE_IN_BOUNDS_OF_TYPE_ADDRESS() returns bool = (forall uint256 i. (mirrorArray[i]) & to_bytes32(max_uint160) == mirrorArray[i]); /** - * @title A complete invariant condition for AddressSet + * A complete invariant condition for AddressSet * @notice invariant addressSetInvariant proves that this condition holds * @return conjunction of the Set-general and AddressSet-specific conditions **/ definition ADDRESS_SET_INVARIANT() returns bool = SET_INVARIANT() && VALUE_IN_BOUNDS_OF_TYPE_ADDRESS(); /** - * @title A complete invariant condition for UintSet, Bytes32Set + * A complete invariant condition for UintSet, Bytes32Set * @notice for UintSet and Bytes2St no type-specific condition is required because the type size is the same as the native type (bytes32) size * @return the Set-general condition **/ definition UINT_SET_INVARIANT() returns bool = SET_INVARIANT(); /** - * @title Out of bound array entries are zero + * Out of bound array entries are zero * @notice A non-essential condition. This condition can be proven as an invariant, but it is not necessary for proving the Set correctness. * @return true if all entries beyond array length are zero **/ -definition ARRAY_OUT_OF_BOUND_ZERO() returns bool = forall uint256 i. (i >= mirrorArrayLen) => (mirrorArray[i] == 0); +definition ARRAY_OUT_OF_BOUND_ZERO() returns bool = forall uint256 i. (i >= mirrorArrayLen) => (mirrorArray[i] == to_bytes32(0)); // For CVL use /** - * @title ghost mirror map, mimics Set map + * ghost mirror map, mimics Set map **/ ghost mapping(bytes32 => uint256) mirrorMap{ init_state axiom forall bytes32 a. mirrorMap[a] == 0; @@ -101,17 +88,17 @@ ghost mapping(bytes32 => uint256) mirrorMap{ } /** - * @title ghost mirror array, mimics Set array + * ghost mirror array, mimics Set array **/ ghost mapping(uint256 => bytes32) mirrorArray{ - init_state axiom forall uint256 i. mirrorArray[i] == 0; + init_state axiom forall uint256 i. mirrorArray[i] == to_bytes32(0); axiom forall uint256 a. mirrorArray[a] & MAX_UINT256Bytes32() == mirrorArray[a]; // axiom forall uint256 a. to_uint256(mirrorArray[a]) >= 0 && to_uint256(mirrorArray[a]) <= MAX_UINT256(); //todo: remove once CERT-1060 is resolved //axiom forall uint256 a. to_mathint(mirrorArray[a]) >= 0 && to_mathint(mirrorArray[a]) <= MAX_UINT256(); //todo: use this axiom when cast bytes32 to mathint is supported } /** - * @title ghost mirror array length, mimics Set array length + * ghost mirror array length, mimics Set array length * @notice ghost includes an assumption about the array length. * If the assumption were not written in the ghost function it should be written in every rule and invariant. * The assumption holds: breaking the assumptions would violate the invariant condition 'map(array(index)) == index + 1'. Set map uses 0 as a sentinel value, so the array cannot contain MAX_INT different values. @@ -119,12 +106,12 @@ ghost mapping(uint256 => bytes32) mirrorArray{ **/ ghost uint256 mirrorArrayLen{ init_state axiom mirrorArrayLen == 0; - axiom mirrorArrayLen < TWO_TO_160() - 1; //todo: remove once CERT-1060 is resolved + axiom to_mathint(mirrorArrayLen) < TWO_TO_160() - 1; //todo: remove once CERT-1060 is resolved } /** - * @title hook for Set array stores + * hook for Set array stores * @dev user of this spec must replace _list with the instance name of the Set. **/ hook Sstore _facilitatorsList .(offset 0)[INDEX uint256 index] bytes32 newValue (bytes32 oldValue) STORAGE { @@ -132,14 +119,14 @@ hook Sstore _facilitatorsList .(offset 0)[INDEX uint256 index] bytes32 newValue } /** - * @title hook for Set array loads + * hook for Set array loads * @dev user of this spec must replace _list with the instance name of the Set. **/ hook Sload bytes32 value _facilitatorsList .(offset 0)[INDEX uint256 index] STORAGE { require(mirrorArray[index] == value); } /** - * @title hook for Set map stores + * hook for Set map stores * @dev user of this spec must replace _list with the instance name of the Set. **/ hook Sstore _facilitatorsList .(offset 32)[KEY bytes32 key] uint256 newIndex (uint256 oldIndex) STORAGE { @@ -147,7 +134,7 @@ hook Sstore _facilitatorsList .(offset 32)[KEY bytes32 key] uint256 newIndex (ui } /** - * @title hook for Set map loads + * hook for Set map loads * @dev user of this spec must replace _list with the instance name of the Set. **/ hook Sload uint256 index _facilitatorsList .(offset 32)[KEY bytes32 key] STORAGE { @@ -155,7 +142,7 @@ hook Sload uint256 index _facilitatorsList .(offset 32)[KEY bytes32 key] STORAGE } /** - * @title hook for Set array length stores + * hook for Set array length stores * @dev user of this spec must replace _list with the instance name of the Set. **/ hook Sstore _facilitatorsList .(offset 0).(offset 0) uint256 newLen (uint256 oldLen) STORAGE { @@ -163,7 +150,7 @@ hook Sstore _facilitatorsList .(offset 0).(offset 0) uint256 newLen (uint256 old } /** - * @title hook for Set array length load + * hook for Set array length load * @dev user of this spec must replace _facilitatorsList with the instance name of the Set. **/ hook Sload uint256 len _facilitatorsList .(offset 0).(offset 0) STORAGE { @@ -171,21 +158,21 @@ hook Sload uint256 len _facilitatorsList .(offset 0).(offset 0) STORAGE { } /** - * @title main Set general invariant + * main Set general invariant **/ invariant setInvariant() - SET_INVARIANT() + SET_INVARIANT(); /** - * @title main AddressSet invariant + * main AddressSet invariant * @dev user of the spec should add 'requireInvariant addressSetInvariant();' to every rule and invariant that refer to a contract that instantiates AddressSet **/ invariant addressSetInvariant() - ADDRESS_SET_INVARIANT() + ADDRESS_SET_INVARIANT(); /** - * @title addAddress() successfully adds an address + * addAddress() successfully adds an address **/ rule api_add_succeeded() { @@ -198,7 +185,7 @@ rule api_add_succeeded() } /** - * @title addAddress() fails to add an address if it already exists + * addAddress() fails to add an address if it already exists * @notice check set membership using contains() **/ rule api_add_failed_contains() @@ -211,7 +198,7 @@ rule api_add_failed_contains() } /** - * @title addAddress() fails to add an address if it already exists + * addAddress() fails to add an address if it already exists * @notice check set membership using atIndex() **/ rule api_add_failed_at() @@ -225,7 +212,7 @@ rule api_add_failed_at() } /** - * @title contains() succeed after addAddress succeeded + * contains() succeed after addAddress succeeded **/ rule api_address_contained_after_add() { @@ -237,7 +224,7 @@ rule api_address_contained_after_add() } /** - * @title _removeAddress() succeeds to remove an address if it existed + * _removeAddress() succeeds to remove an address if it existed * @notice check set membership using contains() **/ rule api_remove_succeeded_contains() @@ -250,7 +237,7 @@ rule api_remove_succeeded_contains() } /** - * @title _removeAddress() fails to remove address if it didn't exist + * _removeAddress() fails to remove address if it didn't exist **/ rule api_remove_failed() { @@ -262,7 +249,7 @@ rule api_remove_failed() } /** - * @title _removeAddress() succeeds to remove an address if it existed + * _removeAddress() succeeds to remove an address if it existed * @notice check set membership using atIndex() **/ rule api_remove_succeeded_at() @@ -276,7 +263,7 @@ rule api_remove_succeeded_at() } /** - * @title contains() failed after an address was removed + * contains() failed after an address was removed **/ rule api_not_contains_after_remove() { @@ -288,7 +275,7 @@ rule api_not_contains_after_remove() } /** - * @title contains() succeeds if atIndex() succeeded + * contains() succeeds if atIndex() succeeded **/ rule cover_at_contains() { @@ -302,7 +289,7 @@ rule cover_at_contains() /** - * @title cover properties, checking various array lengths + * cover properties, checking various array lengths * @notice The assertion should fail - it's a cover property written as an assertion. For large length, beyond loop_iter the assertion should pass. **/ diff --git a/src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol b/src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol index 88054fe9..3716480d 100644 --- a/src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol +++ b/src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol @@ -404,7 +404,7 @@ contract GhoVariableDebtToken is DebtTokenBase, ScaledBalanceTokenBase, IGhoVari emit Transfer(address(0), onBehalfOf, amountToMint); emit Mint(caller, onBehalfOf, amountToMint, balanceIncrease, index); - return previousScaledBalance == 0; + return true; } /** @@ -425,6 +425,8 @@ contract GhoVariableDebtToken is DebtTokenBase, ScaledBalanceTokenBase, IGhoVari uint256 amountScaled = amount.rayDiv(index); require(amountScaled != 0, Errors.INVALID_BURN_AMOUNT); + uint256 balanceBeforeBurn = balanceOf(user); + uint256 previousScaledBalance = super.balanceOf(user); uint256 discountPercent = _ghoUserState[user].discountPercent; (uint256 balanceIncrease, uint256 discountScaled) = _accrueDebtOnAction( @@ -434,7 +436,11 @@ contract GhoVariableDebtToken is DebtTokenBase, ScaledBalanceTokenBase, IGhoVari index ); - _burn(user, (amountScaled + discountScaled).toUint128()); + if (amount == balanceBeforeBurn) { + _burn(user, previousScaledBalance.toUint128()); + } else { + _burn(user, (amountScaled + discountScaled).toUint128()); + } _refreshDiscountPercent( user, diff --git a/src/test/TestGhoVariableDebtTokenForked.t.sol b/src/test/TestGhoVariableDebtTokenForked.t.sol new file mode 100644 index 00000000..37a94aa8 --- /dev/null +++ b/src/test/TestGhoVariableDebtTokenForked.t.sol @@ -0,0 +1,107 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import {InitializableImmutableAdminUpgradeabilityProxy} from '@aave/core-v3/contracts/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol'; +import './TestGhoBase.t.sol'; + +contract TestGhoVariableDebtTokenForked is TestGhoBase { + IGhoToken gho = IGhoToken(0x40D16FC0246aD3160Ccc09B8D0D3A2cD28aE6C2f); + address usdc = 0xA0b86991c6218b36c1d19D4a2e9Eb0cE3606eB48; + address aave = 0x7Fc66500c84A76Ad7e9c93437bFc5Ac33E2DDaE9; + address stkAave = 0x4da27a545c0c5B758a6BA100e3a049001de870f5; + InitializableImmutableAdminUpgradeabilityProxy debtToken = + InitializableImmutableAdminUpgradeabilityProxy( + payable(0x786dBff3f1292ae8F92ea68Cf93c30b34B1ed04B) + ); + IPool pool = IPool(0x87870Bca3F3fD6335C3F4ce8392D69350B4fA4E2); + address admin = 0x64b761D848206f447Fe2dd461b0c635Ec39EbB27; + + uint256 usdcSupplyAmount = 100_000e6; + uint256 ghoBorrowAmount = 71_000e18; + uint256 stkAaveAmount = 100_000e18; + + function setUp() public { + vm.createSelectFork(vm.envString('ETH_RPC_URL'), 17987863); + } + + function testBorrowAndRepayFullUnexpectedScaledBalance() public { + uint256 timeSkip = 86545113; + + // Stake AAVE + deal(aave, ALICE, stkAaveAmount); + vm.startPrank(ALICE); + IERC20(aave).approve(stkAave, stkAaveAmount); + IStakedAaveV3(stkAave).stake(ALICE, stkAaveAmount); + vm.stopPrank(); + + // Supply USDC, borrow GHO + deal(usdc, ALICE, usdcSupplyAmount); + vm.startPrank(ALICE); + IERC20(usdc).approve(address(pool), usdcSupplyAmount); + pool.supply(usdc, usdcSupplyAmount, ALICE, 0); + pool.borrow(address(gho), ghoBorrowAmount, 2, 0, ALICE); + vm.stopPrank(); + + vm.warp(block.timestamp + timeSkip); + + // Ensure Alice has the correct GHO balance + uint256 allDebt = IERC20(address(debtToken)).balanceOf(ALICE); + deal(address(gho), ALICE, allDebt); + + // Repay in full + vm.startPrank(ALICE); + gho.approve(address(pool), type(uint256).max); + pool.repay(address(gho), type(uint256).max, 2, ALICE); + vm.stopPrank(); + + DataTypes.UserConfigurationMap memory userConfig = pool.getUserConfiguration(ALICE); + bool isBorrowing = ((userConfig.data >> (20 << 1)) & 1 != 0); + + // Verify isBorrowing is false, but there is a non-zero scaledBalance + assertEq(isBorrowing, false, 'Unexpected borrow state'); + assertEq(GhoAToken(address(debtToken)).scaledBalanceOf(ALICE), 1, 'Unexpected scaled balance'); + } + + function testBorrowAndRepayFullAmountUpgradeVerifyNoDust(uint256 timeSkip) public { + timeSkip = bound(timeSkip, 1, 31_560_000); + address newDebtToken = address(new GhoVariableDebtToken(pool)); + + // Stake AAVE + deal(aave, ALICE, stkAaveAmount); + vm.startPrank(ALICE); + IERC20(aave).approve(stkAave, stkAaveAmount); + IStakedAaveV3(stkAave).stake(ALICE, stkAaveAmount); + vm.stopPrank(); + + // Supply USDC, borrow GHO + deal(usdc, ALICE, usdcSupplyAmount); + vm.startPrank(ALICE); + IERC20(usdc).approve(address(pool), usdcSupplyAmount); + pool.supply(usdc, usdcSupplyAmount, ALICE, 0); + pool.borrow(address(gho), ghoBorrowAmount, 2, 0, ALICE); + vm.stopPrank(); + + // Upgrade GhoVariableDebtToken + vm.prank(admin); + debtToken.upgradeTo(newDebtToken); + + vm.warp(block.timestamp + timeSkip); + + // Ensure Alice has the correct GHO balance + uint256 allDebt = IERC20(address(debtToken)).balanceOf(ALICE); + deal(address(gho), ALICE, allDebt); + + // Repay in full + vm.startPrank(ALICE); + gho.approve(address(pool), type(uint256).max); + pool.repay(address(gho), type(uint256).max, 2, ALICE); + vm.stopPrank(); + + DataTypes.UserConfigurationMap memory userConfig = pool.getUserConfiguration(ALICE); + bool isBorrowing = ((userConfig.data >> (20 << 1)) & 1 != 0); + + // Ensure isBorrowing is false and the scaledBalance never exceeds zero + assertEq(isBorrowing, false, 'Unexpected borrow state'); + assertEq(GhoAToken(address(debtToken)).scaledBalanceOf(ALICE), 0, 'Unexpected scaled balance'); + } +} diff --git a/test/discount-borrow.test.ts b/test/discount-borrow.test.ts index 0c0a608d..8e65c98a 100644 --- a/test/discount-borrow.test.ts +++ b/test/discount-borrow.test.ts @@ -319,7 +319,7 @@ makeSuite('Gho Discount Borrow Flow', (testEnv: TestEnv) => { expect(user1Debt).to.be.eq(user1ExpectedBalance); // TODO: update to zero - expect(user2Debt).to.be.eq(1); + expect(user2Debt).to.be.eq(0); expect(await gho.balanceOf(aToken.address)).to.be.eq(user2ExpectedInterest); expect(await variableDebtToken.getBalanceFromInterest(users[1].address)).to.be.equal(0);