enforce slippage

[DhairyaSethi]

No description provided.

[github-actions]

Certora Run Started (Certora Prover Run)

• Group ID: 238cd51f-8930-4c57-b165-7284d5c660d5

Config	Status	Link	Log File
R1_optimalityOfBuyAsset_v1	Submitted	link	certora/gsm/conf/gsm4626/optimality4626.conf-14dda2cdde78.log
R3_optimalityOfSellAsset_v1	Submitted	link	certora/gsm/conf/gsm4626/optimality4626.conf-263d35ccd230.log

Certora Run Summary

• Started 2 jobs
• 0 jobs failed

Download Logs

[github-actions]

Certora Run Started (Certora Prover Run)

• Group ID: 8c81ad2c-4b24-4d6f-96ec-5fa9b9dbb56b

Config	Status	Link	Log File
GhoAaveSteward.conf	Submitted	link	certora/steward/conf/GhoAaveSteward.conf-5c487384c659.log
GhoBucketSteward.conf	Submitted	link	certora/steward/conf/GhoBucketSteward.conf-47982df43cd0.log
GhoCcipSteward.conf	Submitted	link	certora/steward/conf/GhoCcipSteward.conf-8f427cf699e0.log
GhoGsmSteward.conf	Submitted	link	certora/steward/conf/GhoGsmSteward.conf-fdc68db9bd14.log

Certora Run Summary

• Started 4 jobs
• 0 jobs failed

Download Logs

[github-actions]

Certora Run Started (Certora Prover Run)

• Group ID: 1f960bbc-6f03-470f-aedc-3814b067c32b

Config	Status	Link	Log File
verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee	Submitted	link	certora/gho/conf/verifyFlashMinter.conf-ef7612f600ac.log
verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment	Submitted	link	certora/gho/conf/verifyGhoAToken.conf-8b074adc84e7.log
verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate	Submitted	link	certora/gho/conf/verifyGhoDiscountRateStrategy.conf-056c40de02d7.log
verifyGhoToken.conf	Submitted	link	certora/gho/conf/verifyGhoToken.conf-87ae1f32bfe6.log
verifyGhoVariableDebtToken-rayMulDiv-summarization.conf	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken-rayMulDiv-summarization.conf-58e0f5b6e6bf.log
verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-067488e5c22b.log
verifyGhoVariableDebtToken.conf --rule disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation 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 integrityOfUpdateDiscountRateStrategy user_index_up_to_date	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-c682706f0c9f.log
verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-5c94b1a2f3d9.log
verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-26ba0a5978c2.log
verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-9db4b3a28b36.log
verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-892fc06a3799.log
verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken.conf-c730e5b29fce.log
verifyGhoVariableDebtTokenInternal.conf	Submitted	link	certora/gho/conf/verifyGhoVariableDebtTokenInternal.conf-097b52a8963e.log
verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken_specialBranch.conf-19f37a294380.log
verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh	Submitted	link	certora/gho/conf/verifyGhoVariableDebtToken_summarized.conf-7f3e6a94e166.log
verifyUpgradeableGhoToken.conf	Submitted	link	certora/gho/conf/verifyUpgradeableGhoToken.conf-d818bd8d50e6.log

Certora Run Summary

• Started 16 jobs
• 0 jobs failed

Download Logs

[github-actions]

Certora Run Started (Certora Prover Run)

• Group ID: 582d7ffb-2997-463d-9b84-f2a280a79d12

Config	Status	Link	Log File
FixedFeeStrategy.conf	Submitted	link	certora/gsm/conf/gsm/FixedFeeStrategy.conf-08fdcf5d962e.log
OracleSwapFreezer.conf	Submitted	link	certora/gsm/conf/gsm/OracleSwapFreezer.conf-f39c999fec96.log
balances-buy.conf	Submitted	link	certora/gsm/conf/gsm/balances-buy.conf-b0f5f37379eb.log
balances-sell.conf --exclude_rule R3_sellAssetUpdatesAssetBalanceCorrectly R4_buyGhoUpdatesGhoBalanceCorrectly	Submitted	link	certora/gsm/conf/gsm/balances-sell.conf-b3cda3c6e30a.log
fees-buy.conf	Submitted	link	certora/gsm/conf/gsm/fees-buy.conf-6481bf9fdbb6.log
fees-sell.conf --exclude_rule R3_estimatedSellFeeCanBeHigherThanActualSellFee	Submitted	link	certora/gsm/conf/gsm/fees-sell.conf-a7e5cc5f6c27.log
fees-sell.conf --rule R3_estimatedSellFeeCanBeHigherThanActualSellFee	Submitted	link	certora/gsm/conf/gsm/fees-sell.conf-a18ba918d26d.log
finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees	Submitted	link	certora/gsm/conf/gsm/finishedRules.conf-d7943bd92b78.log
getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL	Submitted	link	certora/gsm/conf/gsm/getAmount_properties.conf-009defa8d18d.log
gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset	Submitted	link	certora/gsm/conf/gsm/gho-assetToGhoInvertibility.conf-570e5677202e.log
gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset	Submitted	link	certora/gsm/conf/gsm/gho-assetToGhoInvertibility.conf-3269e61a3baf.log
gho-fixedPriceStrategy.conf	Submitted	link	certora/gsm/conf/gsm/gho-fixedPriceStrategy.conf-abb49f99c520.log
gho-gsm-1.conf	Submitted	link	certora/gsm/conf/gsm/gho-gsm-1.conf-c4c6947ca49e.log
gho-gsm-2.conf	Submitted	link	certora/gsm/conf/gsm/gho-gsm-2.conf-f45503c02c16.log
gho-gsm-inverse.conf	Submitted	link	certora/gsm/conf/gsm/gho-gsm-inverse.conf-e9871f38a90a.log
optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2	Submitted	link	certora/gsm/conf/gsm/optimality.conf-8e21e9face63.log

Certora Run Summary

• Started 16 jobs
• 0 jobs failed

Download Logs