certora-gsm-4626

certora: Add Gsm4626 specs and review report (#442) #5

Sign in to view logs

Triggered via push January 28, 2025 12:42

main

Status Success

Total duration 45m 1s

Artifacts –

certora-gsm-4626.yml

on: push

Matrix: verify

Annotations

17 warnings

verify (balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (fees-sell-4626.conf --rule R3a_estimatedSellFeeCanBeLowerThanActualSellFee R2_getAssetAmo...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpda...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (gho-gsm_4626_inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySe...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoB...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (gho-gsm4626.conf --rule enoughULtoBackGhoNonBuySell NonZeroFeeCheckSellAsset NonZeroFeeCh...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyA...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_optimality)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_correctness)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (getAmount_4626_properties.conf --rule getAssetAmountForSellAsset_optimality getAssetAmoun...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (balances-buy-4626.conf)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (finishedRules4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (getAmount_4626_properties.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAss...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis accruedFeesNeverDecrease systemBa...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (optimality4626.conf --rule R3_optimalityOfSellAsset_v1)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (fees-buy-4626.conf)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

verify (finishedRules4626.conf --rule cantBuyOrSellWhenSeized cantBuyOrSellWhenFrozen sellAssetIn...

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636