fix: fix typos

certora/GSM/mutations/mutants/Gsm/Gsm_M3.sol

@@ -194,7 +194,7 @@ contract Gsm is AccessControl, VersionedInitializable, EIP712, IGsm {
   ) external onlyRole(TOKEN_RESCUER_ROLE) {
     require(amount > 0, 'INVALID_AMOUNT');
     if (token == GHO_TOKEN) {
-      // Mutation: not setting aside the ammount of accrued  fee
+      // Mutation: not setting aside the amount of accrued  fee
       // uint256 rescuableBalance = IERC20(token).balanceOf(address(this)) - _accruedFees;
       uint256 rescuableBalance = IERC20(token).balanceOf(address(this));
       require(rescuableBalance >= amount, 'INSUFFICIENT_GHO_TO_RESCUE');

certora/GSM/specs/GsmMethods/methods_base-Martin.spec

@@ -72,7 +72,7 @@ function erc20_mint_assumption(address token, env e, address account, uint256 am
 }
 
 /**
-* Maps shares to an arbirtary value
+* Maps shares to an arbitrary value
 ghost mapping(uint256 => mapping(uint256 => uint256)) shares_ghost {
     axiom (forall uint256 timestamp. forall uint256 shares1. forall uint256 shares2. (!(shares1 <= shares2) => !(shares_ghost[timestamp][shares1] <= shares_ghost[timestamp][shares2]))
 	&& shares_ghost[timestamp][0] == 0 && (shares_ghost[timestamp][shares1]/shares1 == shares_ghost[timestamp][shares2]/shares2));

certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec

@@ -241,7 +241,7 @@ rule buyAssetInverse_all() {
 
 // @title getAssetAmountForSellAsset is inverse of getGhoAmountForSellAsset
 // STATUS: VIOLATED
-// Value from getGhoAmountForSellAsset can be smaller by 1 (the difference is the same as for gross amount - their respecitve differences are equal to ghoAmount).
+// Value from getGhoAmountForSellAsset can be smaller by 1 (the difference is the same as for gross amount - their respective differences are equal to ghoAmount).
 // https://prover.certora.com/output/11775/e6a4acd004b6450bbc109f6dc30288ef?anonymousKey=57eb2fef7c06c14a84f14f4e2c1e206f4b884269
 // rule sellAssetInverse_fee() {
 //     env e;

certora/GSM/specs/gsm/Martin-gho-gsm.spec

@@ -12,7 +12,7 @@ methods {
 
     function _priceStrategy.getAssetPriceInGho(uint256, bool) external returns(uint256) envfree;
     function _priceStrategy.getUnderlyingAssetUnits() external returns(uint256) envfree;
-	function _priceStrategy.getUnderlyginAssetDecimals() external returns(uint256) envfree;
+	function _priceStrategy.getUnderlyingAssetDecimals() external returns(uint256) envfree;
 
     // feeStrategy
 
@@ -74,7 +74,7 @@ rule totalAssetsNotIncrease(method f) filtered {f -> f.selector != sig:seize().s
 	!harnessOnlyMethods(f)} {
 	env e;
 
-	// we focuse on a user so remove address of contracts
+	// we focus on a user so remove address of contracts
 	require e.msg.sender != currentContract;
 
 	require(getPriceRatio() == 10^18);
@@ -120,9 +120,9 @@ rule systemBalanceStabilityBuy() {
 	// require(getPriceRatio() == 10^18);
 	// uint8 underlyingAssetDecimals;
 	// require underlyingAssetDecimals <= 25;
-	// require to_mathint(_priceStrategy.getunderlyingAssetUnits()) == 10^underlyingAssetDecimals;
-	// require _priceStrategy.getUnderlyginAssetDecimals() <= 25;
-	// require to_mathint(_priceStrategy.getUnderlyingAssetUnits()) == 10^_priceStrategy.getUnderlyginAssetDecimals();
+	// require to_mathint(_priceStrategy.getUnderlyingAssetUnits()) == 10^underlyingAssetDecimals;
+	// require _priceStrategy.getUnderlyingAssetDecimals() <= 25;
+	// require to_mathint(_priceStrategy.getUnderlyingAssetUnits()) == 10^_priceStrategy.getUnderlyingAssetDecimals();
 	feeLimits(e);
 	priceLimits(e);
 

certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec

@@ -193,7 +193,7 @@ definition canIncreaseAccruedFees(method f) returns bool =
 definition canDecreaseAccruedFees(method f) returns bool =
 	f.selector == sig:distributeFeesToTreasury().selector;
 
-// @title Only specific methods can increase / decrease acrued fees
+// @title Only specific methods can increase / decrease accrued fees
 // STATUS: PASS
 // https://prover.certora.com/output/11775/d2998f74795f45eea2ac8da86fd9a481?anonymousKey=6382a56072f63e64436d7af2b5c1800e07a0be9e
 rule whoCanChangeAccruedFees(method f)
@@ -313,7 +313,7 @@ rule getAssetAmountForSellAsset_optimality()
 	assert suggestedAssetToSell <= reallySold;
 }
 
-// @title Exposure bellow cap is preserved by all methods except updateExposureCap and initialize
+// @title Exposure below cap is preserved by all methods except updateExposureCap and initialize
 // STATUS: PASS
 // https://prover.certora.com/output/6893/14a1440d3114460f8b64b388a706ca46/?anonymousKey=bb420c63b5b5b11810d5d72026ed6cb6baec43ac
 rule exposureBellowCap(method f)
@@ -387,7 +387,7 @@ rule giftingGhoDoesntAffectStorageSIMPLE()
 	assert storageAfter[currentContract] == initialStorage[currentContract];
 }
 
-// @title Return values of sellAsset are monotonically inreasing
+// @title Return values of sellAsset are monotonically increasing
 // STATUS: TIMEOUT
 // https://prover.certora.com/output/11775/abdd5e8dc1634d0a91e6a35647b06412?anonymousKey=8ae78b0142eba6819674647e6e41e1f264df6a12
 rule monotonicityOfSellAsset() {
@@ -411,7 +411,7 @@ rule monotonicityOfSellAsset() {
     assert a1 <= a2 <=> g1 <= g2;
 }
 
-// @title Return values of buyAsset are monotonically inreasing
+// @title Return values of buyAsset are monotonically increasing
 // STATUS: PASS
 // https://prover.certora.com/output/6893/a4e2f473e8e8464db7528615287b19dc/?anonymousKey=52f6539bd09a3ed26235b922ad83c9737b01fd3d
 rule monotonicityOfBuyAsset() {

certora/gho/harness/GhoTokenHarness.sol

@@ -10,7 +10,7 @@ contract GhoTokenHarness is GhoToken {
   constructor() GhoToken(msg.sender) {}
 
   /**
-   * @notice Returns the backet capacity
+   * @notice Returns the bucket capacity
    * @param facilitator The address of the facilitator
    * @return The facilitator bucket capacity
    */
@@ -20,7 +20,7 @@ contract GhoTokenHarness is GhoToken {
   }
 
   /**
-   * @notice Returns the backet level
+   * @notice Returns the bucket level
    * @param facilitator The address of the facilitator
    * @return The facilitator bucket level
    */
@@ -45,7 +45,7 @@ contract GhoTokenHarness is GhoToken {
    */
   function is_in_facilitator_mapping(address addr) external view returns (bool) {
     Facilitator memory facilitator = _facilitators[addr];
-    return facilitator.isLabelNonempty; //TODO: remove workaroun when CERT-977 is resolved
+    return facilitator.isLabelNonempty; //TODO: remove workaround when CERT-977 is resolved
     //  return (bytes(facilitator.label).length > 0);
   }
 

certora/gho/specs/VariableDebtToken.spec

@@ -10,12 +10,12 @@ methods {
 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)
+// summarization for scaledBalanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul)
 // ghost gRNVB() returns uint256 {
 // 	axiom gRNVB() == 7 * ray();
 // }
 /*
-Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2.
+Due to rayDiv and RayMul Rounding (+ 0.5) - balance could increase by (gRNI() / Ray() + 1) / 2.
 */
 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);
 
@@ -124,7 +124,7 @@ rule nonceChangePermits(method f)
     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
+// minting and then burning Variable Debt Token should have no effect on the users balance
 rule inverseMintBurn(address a, address delegatedUser, uint256 amount, uint256 index) {
 	env e;
 	uint256 balancebefore = balanceOf(e, a);
@@ -158,10 +158,10 @@ rule integrityOfBurn(address u, uint256 amount) {
 	uint256 totalSupplyAfter = totalSupply();
 
     assert bounded_error_eq(totalSupplyAfter, totalSupplyBefore - amount, 1, index), "total supply integrity"; // total supply reduced
-    assert bounded_error_eq(balanceAfterUser, balanceBeforeUser - amount, 1, index), "integrity break";  // user burns ATokens to recieve underlying
+    assert bounded_error_eq(balanceAfterUser, balanceBeforeUser - amount, 1, index), "integrity break";  // user burns ATokens to receive underlying
 }
 
-rule integrityOfBurn_exact_suply_should_fail(address u, uint256 amount) {
+rule integrityOfBurn_exact_supply_should_fail(address u, uint256 amount) {
 	env e;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	uint256 balanceBeforeUser = balanceOf(e, u);
@@ -249,7 +249,7 @@ rule additiveMint(address user1, address user2, address user3, uint256 x, uint25
 }
 
 //using exact comparison
-rule additiveMint_excact_should_fail(address user1, address user2, address user3, uint256 x, uint256 y) {
+rule additiveMint_exact_should_fail(address user1, address user2, address user3, uint256 x, uint256 y) {
 	env e;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
     require (user1 != user2  && balanceOf(e, user1) == balanceOf(e, user2));
@@ -274,15 +274,15 @@ rule integrityMint(address a, uint256 x) {
 	address delegatedUser;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	uint256 underlyingBalanceBefore = balanceOf(e, a);
-	uint256 atokenBlanceBefore = scaledBalanceOf(a);
+	uint256 atokenBalanceBefore = scaledBalanceOf(a);
 	uint256 totalATokenSupplyBefore = scaledTotalSupply(e);
 	mint(e, delegatedUser, a, x, index);
 
 	uint256 underlyingBalanceAfter = balanceOf(e, a);
-	uint256 atokenBlanceAfter = scaledBalanceOf(a);
+	uint256 atokenBalanceAfter = scaledBalanceOf(a);
 	uint256 totalATokenSupplyAfter = scaledTotalSupply(e);
 
-	assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
+	assert atokenBalanceAfter - atokenBalanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
 	assert totalATokenSupplyAfter > totalATokenSupplyBefore;
     assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1, index);
     // assert balanceAfter == balancebefore+x;
@@ -294,15 +294,15 @@ rule integrityMint_underlying(address a, uint256 x) {
 	address delegatedUser;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	uint256 underlyingBalanceBefore = balanceOf(e, a);
-	uint256 atokenBlanceBefore = scaledBalanceOf(a);
+	uint256 atokenBalanceBefore = scaledBalanceOf(a);
 	uint256 totalATokenSupplyBefore = scaledTotalSupply(e);
 	mint(e, delegatedUser, a, x, index);
 
 	uint256 underlyingBalanceAfter = balanceOf(e, a);
-	uint256 atokenBlanceAfter = scaledBalanceOf(a);
+	uint256 atokenBalanceAfter = scaledBalanceOf(a);
 	uint256 totalATokenSupplyAfter = scaledTotalSupply(e);
 
-	//assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
+	//assert atokenBalanceAfter - atokenBalanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
 	//assert totalATokenSupplyAfter > totalATokenSupplyBefore;
     assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1, index);
     // assert balanceAfter == balancebefore+x;
@@ -313,15 +313,15 @@ rule integrityMint_atoken(address a, uint256 x) {
 	address delegatedUser;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	uint256 underlyingBalanceBefore = balanceOf(e, a);
-	uint256 atokenBlanceBefore = scaledBalanceOf(a);
+	uint256 atokenBalanceBefore = scaledBalanceOf(a);
 	uint256 totalATokenSupplyBefore = scaledTotalSupply(e);
 	mint(e, delegatedUser, a, x, index);
 
 	uint256 underlyingBalanceAfter = balanceOf(e, a);
-	uint256 atokenBlanceAfter = scaledBalanceOf(a);
+	uint256 atokenBalanceAfter = scaledBalanceOf(a);
 	uint256 totalATokenSupplyAfter = scaledTotalSupply(e);
 
-	assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
+	assert atokenBalanceAfter - atokenBalanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
 	//assert totalATokenSupplyAfter > totalATokenSupplyBefore;
     //assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1, index);
     // assert balanceAfter == balancebefore+x;
@@ -333,21 +333,21 @@ rule integrityMint_exact_should_fail(address a, uint256 x) {
 	address delegatedUser;
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	uint256 underlyingBalanceBefore = balanceOf(e, a);
-	uint256 atokenBlanceBefore = scaledBalanceOf(a);
+	uint256 atokenBalanceBefore = scaledBalanceOf(a);
 	uint256 totalATokenSupplyBefore = scaledTotalSupply(e);
 	mint(e, delegatedUser, a, x, index);
 
 	uint256 underlyingBalanceAfter = balanceOf(e, a);
-	uint256 atokenBlanceAfter = scaledBalanceOf(a);
+	uint256 atokenBalanceAfter = scaledBalanceOf(a);
 	uint256 totalATokenSupplyAfter = scaledTotalSupply(e);
 
-	assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
+	assert atokenBalanceAfter - atokenBalanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore;
 	assert totalATokenSupplyAfter > totalATokenSupplyBefore;
     assert underlyingBalanceAfter == underlyingBalanceBefore+x;
 
 }
 
-// Buring zero amount of tokens should have no effect.
+// Burning zero amount of tokens should have no effect.
 rule burnZeroDoesntChangeBalance(address u, uint256 index) {
 	env e;
 	uint256 balanceBefore = balanceOf(e, u);

certora/gho/specs/flashMinter.spec

@@ -3,8 +3,8 @@ using GhoAToken as atoken;
 using MockFlashBorrower as flashBorrower;
 
 methods{
-    function _.isPoolAdmin(address user) external => retreivePoolAdminFromGhost(user) expect bool ALL;
-    function _.isFlashBorrower(address user) external => retreiveFlashBorrowerFromGhost(user) expect bool ALL;
+    function _.isPoolAdmin(address user) external => retrievePoolAdminFromGhost(user) expect bool ALL;
+    function _.isFlashBorrower(address user) external => retrieveFlashBorrowerFromGhost(user) expect bool ALL;
     function _.onFlashLoan(address, address, uint256, uint256, bytes) external => DISPATCHER(true);
     function _.getACLManager() external => NONDET;
 
@@ -31,12 +31,12 @@ ghost mapping(address => bool) poolAdmin_ghost;
 ghost mapping(address => bool) flashBorrower_ghost;
 
 // returns whether the user is a pool admin
-function retreivePoolAdminFromGhost(address user) returns bool{
+function retrievePoolAdminFromGhost(address user) returns bool{
     return poolAdmin_ghost[user];
 }
 
 // returns whether the user is a flash borrower
-function retreiveFlashBorrowerFromGhost(address user) returns bool{
+function retrieveFlashBorrowerFromGhost(address user) returns bool{
     return flashBorrower_ghost[user];
 }
 
@@ -94,7 +94,7 @@ rule integrityOfFeeSet(uint256 new_fee){
 }
 
 /**
- * @title Checks that the available liquidity, retreived by maxFlashLoan, stays the same after any action 
+ * @title Checks that the available liquidity, retrieved by maxFlashLoan, stays the same after any action 
  */
 rule availableLiquidityDoesntChange(method f, address token){
     env e; calldataarg args;

certora/gho/specs/ghoDiscountRateStrategy.spec

@@ -49,15 +49,15 @@ rule maxDiscountForHighDiscountTokenBalance() {
 }
 
 /**
-* @title proves that the discount balance below the threashold leads to zero discount rate
+* @title proves that the discount balance below the threshold leads to zero discount rate
 **/
 rule zeroDiscountForSmallDiscountTokenBalance() {
     uint256 debtBalance;
     uint256 discountTokenBalance;
     uint256 rate = calculateDiscountRate(debtBalance, 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.
+    // 1,2 - if the debt balance or the discount token balance are below some threshold.
     // 3 - if debtBalance is much larger than discountBalance (since the return value is the max rate multiplied
     //     by the ratio between debtBalance and discountBalance)
     assert(
@@ -68,7 +68,7 @@ rule zeroDiscountForSmallDiscountTokenBalance() {
 }
 
 /**
-* @title if the discounted blance is above the threashold and below the current debt, the discount rate will be according to the ratio
+* @title if the discounted balance is above the threshold and below the current debt, the discount rate will be according to the ratio
 * between the debt balance and the discounted balance
 **/
 rule partialDiscountForIntermediateTokenBalance() {

certora/gho/specs/ghoToken.spec

@@ -311,7 +311,7 @@ rule facilitator_in_list_after_setFacilitatorBucketCapacity(){
 }
 
 /**
-* @title getFacilitatorBucketCapacity() called after setFacilitatorBucketCapacity() retrun the assign bucket capacity
+* @title getFacilitatorBucketCapacity() called after setFacilitatorBucketCapacity() return the assign bucket capacity
 */
 rule getFacilitatorBucketCapacity_after_setFacilitatorBucketCapacity(){