From b68e6c9d88ae353757dada2ec8a7c745b26f7ae6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 10 Dec 2024 15:59:40 +0100 Subject: [PATCH] refactor: remove lastUpdateIsNotNil function --- certora/specs/MarketExists.spec | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/certora/specs/MarketExists.spec b/certora/specs/MarketExists.spec index e11b281..cf5ffee 100644 --- 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