test(certora): timestamp back with uint64 with require

codex-storage · Jan 27, 2025 · 4740c86 · 4740c86
1 parent 79c60e7
commit 4740c86
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
@@ -45,11 +45,12 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25
     totalSent = totalSent + defaultValue - defaultValue_old;
 }
 
-ghost mathint lastBlockTimestampGhost;
+ghost uint64 lastBlockTimestampGhost;
 
 hook TIMESTAMP uint v {
-    require lastBlockTimestampGhost <= to_mathint(v);
-    lastBlockTimestampGhost = to_mathint(v);
+    require v < max_uint64;
+    require lastBlockTimestampGhost <= assert_uint64(v);
+    lastBlockTimestampGhost = assert_uint64(v);
 }
 
 ghost mapping(MarketplaceHarness.SlotId => mapping(Periods.Period => bool)) _missingMirror {