test(verifier): repair state can go to filled

codex-storage · Dec 4, 2024 · 2e74f70 · 2e74f70
1 parent 36a86fd
commit 2e74f70
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
@@ -301,7 +301,10 @@ rule functionsCausingSlotStateChanges(env e, method f) {
     assert slotStateBefore == Marketplace.SlotState.Finished && slotStateAfter == Marketplace.SlotState.Paid => canMakeSlotPaid(f);
 
     // SlotState.Free -> SlotState.Filled
-    assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+    assert slotStateBefore != Marketplace.SlotState.Free && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+
+    // SlotState.Repair -> SlotState.Filled
+    assert slotStateBefore != Marketplace.SlotState.Repair && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
 }
 
 rule allowedSlotStateChanges(env e, method f) {