Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: fix typos #390

Merged
merged 1 commit into from
Mar 19, 2024
Merged

fix: fix typos #390

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion certora/GSM/mutations/mutants/Gsm/Gsm_M3.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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');
Expand Down
2 changes: 1 addition & 1 deletion certora/GSM/specs/GsmMethods/methods_base-Martin.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
2 changes: 1 addition & 1 deletion certora/GSM/specs/gsm/Dominik-AssetToGhoInvertibility.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
10 changes: 5 additions & 5 deletions certora/GSM/specs/gsm/Martin-gho-gsm.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);

Expand Down
8 changes: 4 additions & 4 deletions certora/GSM/specs/gsm/otakar-gho-gsm-finishedRules.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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() {
Expand All @@ -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() {
Expand Down
6 changes: 3 additions & 3 deletions certora/gho/harness/GhoTokenHarness.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand All @@ -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
*/
Expand All @@ -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);
}

Expand Down
38 changes: 19 additions & 19 deletions certora/gho/specs/VariableDebtToken.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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));
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -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);
Expand Down
10 changes: 5 additions & 5 deletions certora/gho/specs/flashMinter.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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];
}

Expand Down Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions certora/gho/specs/ghoDiscountRateStrategy.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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() {
Expand Down
2 changes: 1 addition & 1 deletion certora/gho/specs/ghoToken.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(){

Expand Down
Loading
Loading