refactor: remove lastUpdateIsNotNil function

morpho-org · Dec 10, 2024 · b68e6c9 · b68e6c9
1 parent fad2351
commit b68e6c9
Showing 1 changed file with 3 additions and 8 deletions.
diff --git a/certora/specs/MarketExists.spec b/certora/specs/MarketExists.spec
@@ -3,8 +3,9 @@
 using Morpho as MORPHO;
 
 methods {
-    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
+    function MORPHO.lastUpdate(PreLiquidation.Id) external returns (uint256) envfree;
     function MORPHO.market(PreLiquidation.Id) external returns (uint128, uint128, uint128, uint128, uint128, uint128) envfree;
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
     function _.price() external => NONDET;
 }
 
@@ -18,13 +19,7 @@ hook TIMESTAMP uint newTimestamp {
     lastTimestamp = newTimestamp;
 }
 
-function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
-    mathint lastUpdate;
-    (_,_,_,_,lastUpdate,_) = MORPHO.market(id);
-    return lastUpdate != 0;
-}
-
 // Ensure that the pre-liquidation contract interacts with a created market.
 
 invariant marketExists()
-    lastUpdateIsNotNil(currentContract.ID);
+    MORPHO.lastUpdate(currentContract.ID) != 0