Skip to content

Commit

Permalink
feat: new positive cap and new supply queue cap
Browse files Browse the repository at this point in the history
  • Loading branch information
QGarchery committed Feb 26, 2024
1 parent b9c89a8 commit 99e611f
Showing 1 changed file with 28 additions and 0 deletions.
28 changes: 28 additions & 0 deletions certora/specs/ConsistentState.spec
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,34 @@ methods {
function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
}

rule newPositiveCapEnsuresUpdated(env e, method f, calldataarg args) {
MetaMorphoHarness.Id id;

uint192 supplyCap;
supplycap, _, _ = config(id)
require supplyCap == 0;

f(e, args);

supplycap, _, _ = config(id)
require supplyCap > 0;

assert Morpho.lastUpdate(id) > 0;
}

rule newSupplyQueueEnsuresPositiveCap(env e, method f, calldataarg args) {
MetaMorphoHarness.Id id;
uint256 i;

f(e, args);

require supplyQueue(i) == id;

uint192 supplyCap;
supplycap, _, _ = config(id)
assert supplyCap == 0;
}

// Check that fee cannot accrue to an unset fee recipient.
invariant noFeeToUnsetFeeRecipient()
feeRecipient() == 0 => fee() == 0;
Expand Down

0 comments on commit 99e611f

Please sign in to comment.