certora: update state changes spec now that we have vault

Author: markspanbroek

certora/confs/StateChanges.conf

@@ -2,12 +2,14 @@
     "files": [
         "certora/harness/MarketplaceHarness.sol",
         "contracts/Marketplace.sol",
+        "contracts/Vault.sol",
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
     ],
     "parametric_contracts": ["MarketplaceHarness"],
     "link" : [
-        "MarketplaceHarness:_token=ERC20A",
+        "Vault:_token=ERC20A",
+        "MarketplaceHarness:_vault=Vault",
         "MarketplaceHarness:_verifier=Groth16Verifier"
     ],
     "msg": "Verifying StateChanges",

certora/specs/StateChanges.spec

@@ -20,7 +20,7 @@ rule allowedRequestStateChanges(env e, method f) {
     // we need to check for `freeSlot(slotId)` here to ensure it's being called with
     // the slotId we're interested in and not any other slotId (that may not pass the
     // required invariants)
-    if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) {
+    if (f.selector == sig:freeSlot(Marketplace.SlotId).selector) {
         freeSlot(e, slotId);
     } else {
         f(e, args);