From a27da9738ae72dad66baa1c154c3a3c697709c29 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Tue, 13 Aug 2024 14:16:12 +0200
Subject: [PATCH] chore(certora): verify SlotState and RequestState changes
 count

This adds a rule to formally verify that the `SlotState` and
`RequestState` of any given `Slot` or `Request` does not change more
than once per function call.

Closes #129
---
 certora/specs/Marketplace.spec | 43 ++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index eab3619..b9feb97 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -63,6 +63,27 @@ hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period pe
     _missingMirror[slotId][period] = defaultValue;
 }
 
+ghost mathint requestStateChangesCount {
+    init_state axiom requestStateChangesCount == 0;
+}
+
+hook Sstore _requestContexts[KEY Marketplace.RequestId requestId].state Marketplace.RequestState newState (Marketplace.RequestState oldState) {
+    if (oldState != newState) {
+        requestStateChangesCount = requestStateChangesCount + 1;
+    }
+}
+
+ghost mathint slotStateChangesCount {
+    init_state axiom slotStateChangesCount == 0;
+}
+
+hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState newState (Marketplace.SlotState oldState) {
+    if (oldState != newState) {
+        slotStateChangesCount = slotStateChangesCount + 1;
+    }
+}
+
+
 /*--------------------------------------------
 |              Helper functions              |
 --------------------------------------------*/
@@ -180,3 +201,25 @@ rule finishedRequestCannotBeStartedAgain(env e, method f) {
 
     assert requestStateBefore == requestStateAfter;
 }
+
+rule requestStateChangesOnlyOncePerFunctionCall(env e, method f) {
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    mathint requestStateChangesCountBefore = requestStateChangesCount;
+    f(e, args);
+    mathint requestStateChangesCountAfter = requestStateChangesCount;
+
+    assert requestStateChangesCountAfter <= requestStateChangesCountBefore + 1;
+}
+
+rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
+    calldataarg args;
+    Marketplace.SlotId slotId;
+
+    mathint slotStateChangesCountBefore = slotStateChangesCount;
+    f(e, args);
+    mathint slotStateChangesCountAfter =slotStateChangesCount; 
+
+    assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
+}