Skip to content

Commit 0512fac

Browse files
committed
upd: sync change with certora
1 parent 2e2eec9 commit 0512fac

File tree

1 file changed

+0
-18
lines changed

1 file changed

+0
-18
lines changed

certora/steward/specs/GhoAaveSteward.spec

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ methods {
3232

3333

3434
function getGhoTimelocks() external returns (IGhoAaveSteward.GhoDebounce) envfree;
35-
function GHO_BORROW_RATE_MAX() external returns uint32 envfree;
3635
function MINIMUM_DELAY() external returns uint256 envfree;
3736
function RISK_COUNCIL() external returns address envfree;
3837

@@ -225,23 +224,6 @@ rule updateGhoSupplyCap__correctness() {
225224
}
226225

227226

228-
rule updateGhoBorrowRate__correctness() {
229-
env e; uint16 optimalUsageRatio; uint32 baseVariableBorrowRate;
230-
uint32 variableRateSlope1; uint32 variableRateSlope2;
231-
232-
uint16 optimalUsageRatio_before = OPTIMAL_USAGE_RATIO;
233-
uint32 baseVariableBorrowRate_before = BASE_VARIABLE_BORROW_RATE;
234-
uint32 variableRateSlope1_before = VARIABLE_RATE_SLOPE1;
235-
uint32 variableRateSlope2_before = VARIABLE_RATE_SLOPE2;
236-
237-
updateGhoBorrowRate(e,optimalUsageRatio, baseVariableBorrowRate, variableRateSlope1, variableRateSlope2);
238-
239-
240-
assert baseVariableBorrowRate + variableRateSlope1 + variableRateSlope2 <= to_mathint(GHO_BORROW_RATE_MAX());
241-
}
242-
243-
244-
245227

246228

247229

0 commit comments

Comments
 (0)