docs: Add docs for remote facilitator setup #12
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
|
Certora Run Started (Certora Prover Run)
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
![certora-run[bot]](https://avatars.githubusercontent.com/in/1083145?s=60&v=4){kind=small}
There was a problem hiding this comment.
Verification Results
- Group ID: 39998a6c-5442-4084-a00f-644574fd775e
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| verifyUpgradeableGhoToken.conf | ✅ | 29 | Link |
| verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh | ✅ | 2 | Link |
| verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease | ✅ | 2 | Link |
| verifyGhoVariableDebtToken-rayMulDiv-summarization.conf | ✅ | 8 | Link |
| verifyGhoVariableDebtTokenInternal.conf | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken | ✅ | 4 | Link |
| verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint | ✅ | 2 | Link |
| verifyGhoToken.conf | ✅ | 29 | Link |
| verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate | ✅ | 6 | Link |
| verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment | ✅ | 8 | Link |
| verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee | ✅ | 7 | Link |
| scountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy user_index_up_to_date | ✅ | 28 | Link |
There was a problem hiding this comment.
Verification Results
- Group ID: 2e16de88-b6f4-46b0-98d1-ef0ff1ba3806
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| ssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees | ✅ | 21 | Link |
| OracleSwapFreezer.conf | ✅ | 5 | Link |
| optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2 | ✅ | 6 | Link |
| gho-gsm-inverse.conf | ✅ | 24 | Link |
| gho-gsm-2.conf | ✅ | 6 | Link |
| gho-gsm-1.conf | ✅ | 7 | Link |
| gho-fixedPriceStrategy.conf | ✅ | 5 | Link |
| gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset | ✅ | 7 | Link |
| gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset | ✅ | 2 | Link |
| getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL | ✅ | 3 | Link |
| FixedFeeStrategy.conf | ✅ | 11 | Link |
| fees-sell.conf --rule R3_estimatedSellFeeCanBeHigherThanActualSellFee | ✅ | 2 | Link |
| fees-sell.conf --exclude_rule R3_estimatedSellFeeCanBeHigherThanActualSellFee | ✅ | 8 | Link |
| fees-buy.conf | ✅ | 8 | Link |
| balances-sell.conf --exclude_rule R3_sellAssetUpdatesAssetBalanceCorrectly R4_buyGhoUpdatesGhoBalanceCorrectly | ✅ | 6 | Link |
| balances-buy.conf | ✅ | 11 | Link |
There was a problem hiding this comment.
Verification Results
- Group ID: d032217a-6a8d-4b41-9573-62690e8fb919
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| set R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee | ✅ | 10 | Link |
| orrectness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness | ✅ | 7 | Link |
| optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset | ✅ | 3 | Link |
| optimality4626.conf --rule R3_optimalityOfSellAsset_v1 | ✅ | 2 | Link |
| optimality4626.conf --rule R1_optimalityOfBuyAsset_v1 | ✅ | 2 | Link |
| gho-gsm4626-inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19 | ✅ | 10 | Link |
| gho-gsm4626-2.conf --rule accruedFeesNeverDecrease | ✅ | 2 | Link |
| gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis | ✅ | 2 | Link |
| gho-gsm4626-1.conf | ✅ | 4 | Link |
| getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_optimality | ✅ | 2 | Link |
| getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_correctness | ✅ | 2 | Link |
| getAmount-properties-4626.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty | ✅ | 3 | Link |
| finishedRules-4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth | ✅ | 2 | Link |
| fees-buy-4626.conf | ✅ | 8 | Link |
| edSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure | ✅ | 22 | Link |
| balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange | ✅ | 3 | Link |
| balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly | ✅ | 2 | Link |
| balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq | ✅ | 4 | Link |
| balances-buy-4626.conf | ✅ | 8 | Link |
miguelmtzinf
commented
Nov 4, 2025
miguelmtzinf
commented
Nov 4, 2025
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
There was a problem hiding this comment.
Verification Results
- Group ID: 1f5a0b51-15d9-4df7-bb52-563efd12e221
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| verifyUpgradeableGhoToken.conf | ✅ | 29 | Link |
| verifyGhoVariableDebtToken_summarized.conf --rule accrueAlwaysCalleldBeforeRefresh | ✅ | 2 | Link |
| verifyGhoVariableDebtToken_specialBranch.conf --rule sendersDiscountPercentCannotIncrease | ✅ | 2 | Link |
| verifyGhoVariableDebtToken-rayMulDiv-summarization.conf | ✅ | 8 | Link |
| verifyGhoVariableDebtTokenInternal.conf | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule user_index_after_mint user_index_ge_one_ray nonzeroNewDiscountToken | ✅ | 4 | Link |
| verifyGhoVariableDebtToken.conf --rule userCantNullifyItsDebt | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule onlyMintForUserCanIncreaseUsersBalance | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule discountCantExceedDiscountRate | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule discountCantExceed100Percent | ✅ | 2 | Link |
| verifyGhoVariableDebtToken.conf --rule accumulated_interest_increase_after_mint | ✅ | 2 | Link |
| verifyGhoToken.conf | ✅ | 29 | Link |
| verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate | ✅ | 6 | Link |
| verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment | ✅ | 8 | Link |
| verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee | ✅ | 7 | Link |
| scountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy user_index_up_to_date | ✅ | 28 | Link |
There was a problem hiding this comment.
Verification Results
- Group ID: 4c13185c-f019-4357-a356-1abffafffeaf
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| ssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees | ✅ | 21 | Link |
| OracleSwapFreezer.conf | ✅ | 5 | Link |
| optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2 | ✅ | 6 | Link |
| gho-gsm-inverse.conf | ✅ | 24 | Link |
| gho-gsm-2.conf | ✅ | 6 | Link |
| gho-gsm-1.conf | ✅ | 7 | Link |
| gho-fixedPriceStrategy.conf | ✅ | 5 | Link |
| gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset | ✅ | 7 | Link |
| gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset | ✅ | 2 | Link |
| getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL | ✅ | 3 | Link |
| FixedFeeStrategy.conf | ✅ | 11 | Link |
| fees-sell.conf --rule R3_estimatedSellFeeCanBeHigherThanActualSellFee | ✅ | 2 | Link |
| fees-sell.conf --exclude_rule R3_estimatedSellFeeCanBeHigherThanActualSellFee | ✅ | 8 | Link |
| fees-buy.conf | ✅ | 8 | Link |
| balances-sell.conf --exclude_rule R3_sellAssetUpdatesAssetBalanceCorrectly R4_buyGhoUpdatesGhoBalanceCorrectly | ✅ | 6 | Link |
| balances-buy.conf | ✅ | 11 | Link |
There was a problem hiding this comment.
Verification Results
- Group ID: ce08538d-198e-41ac-88ea-0c12db6d9e25
| Job | Result | VERIFIED | Link |
|---|---|---|---|
| set R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee | ✅ | 10 | Link |
| orrectness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness | ✅ | 7 | Link |
| optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset | ✅ | 3 | Link |
| optimality4626.conf --rule R3_optimalityOfSellAsset_v1 | ✅ | 2 | Link |
| optimality4626.conf --rule R1_optimalityOfBuyAsset_v1 | ✅ | 2 | Link |
| gho-gsm4626-inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19 | ✅ | 10 | Link |
| gho-gsm4626-2.conf --rule accruedFeesNeverDecrease | ✅ | 2 | Link |
| gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis | ✅ | 2 | Link |
| gho-gsm4626-1.conf | ✅ | 4 | Link |
| getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_optimality | ✅ | 2 | Link |
| getAmount-properties-4626.conf --rule getGhoAmountForBuyAsset_correctness | ✅ | 2 | Link |
| getAmount-properties-4626.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty | ✅ | 3 | Link |
| finishedRules-4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth | ✅ | 2 | Link |
| fees-buy-4626.conf | ✅ | 8 | Link |
| edSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure | ✅ | 22 | Link |
| balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange | ✅ | 3 | Link |
| balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly | ✅ | 2 | Link |
| balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq | ✅ | 4 | Link |
| balances-buy-4626.conf | ✅ | 8 | Link |
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Certora Run Started (Certora Prover Run)
Certora Run Summary
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Replaces #11
Thanks @efecarranza for the docs! I used yours as base and expanded with an overview of the setup.