feat: Add support for Remote GSM (#1) #9
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
* feat: initial commit * feat: finish tests * fix: safecast overflow * feat: overflow tests * feat: add entity checks and delete usage * fix: update test * feat: add limit check on remove entity * chore: remove unnecesarry check * chore: remove deletion * feat: add audit * chore: run lint * for PR * chore: lint certora * chore: run ci without if * chore: add all certora ci * chore: explicit certora key --------- Co-authored-by: nisnislevi <[email protected]>
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: 5740019b-5e49-4e94-b15a-5c18e82752e6
| 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: f38b11d4-a6c6-419b-9f58-4d7939e43648
| 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: c168b9f0-102e-49d8-baed-12ee58e807e2
| 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 |
DhairyaSethi
approved these changes
Aug 28, 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
|
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.
This update enables GSM support for remote chain deployments. Since GHO is only minted on Ethereum, the DAO must pre-mint liquidity and bridge it to destination chains for later use.
To support this flow, the following contracts are introduced:
Modifications were made to Gsm and Gsm4626 to decouple from GhoToken direct mint/burn logic. Instead, they now interact with GhoReserve, enabling a unified and maintainable architecture for both Ethereum and remote chains.
These new contracts are reusable for other facilitator strategies, regardless of the network.
Contributors: