From ae94d1ebf33cad022bf22087e4ef8890b47d6726 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Sun, 6 Apr 2025 00:39:55 +0100
Subject: [PATCH] try to hook on _funds. fixed required

---
 certora/confs/Vault.conf | 28 ++++++++++++++++++++++++++++
 certora/specs/Vault.spec | 29 +++++++++++++++++++++++++++++
 remappings.txt           |  4 ++++
 3 files changed, 61 insertions(+)
 create mode 100644 certora/confs/Vault.conf
 create mode 100644 certora/specs/Vault.spec
 create mode 100644 remappings.txt

diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf
new file mode 100644
index 0000000..2847c5b
--- /dev/null
+++ b/certora/confs/Vault.conf
@@ -0,0 +1,28 @@
+{
+    "files": [
+        "contracts/Vault.sol",
+        // "certora/harness/MarketplaceHarness.sol",
+        // "contracts/Marketplace.sol",
+        // "contracts/Vault.sol",
+        // "contracts/Groth16Verifier.sol",
+        "certora/helpers/ERC20A.sol",
+    ],
+    "parametric_contracts": ["Vault"],
+    "link" : [
+        "Vault:_token=ERC20A",
+    //     "MarketplaceHarness:_vault=Vault",
+    //     "MarketplaceHarness:_verifier=Groth16Verifier"
+    ],
+    "packages": [
+        "@openzeppelin/=node_modules/@openzeppelin/",
+    ],
+    "msg": "Verifying Vault",
+    "rule_sanity": "basic",
+    "verify": "Vault:certora/specs/Vault.spec",
+    // "optimistic_loop": true,
+    "loop_iter": "3",
+    // "optimistic_hashing": true,
+    // "hashing_length_bound": "512",
+
+    "solc": "solc8.28",
+}
diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec
new file mode 100644
index 0000000..04585e1
--- /dev/null
+++ b/certora/specs/Vault.spec
@@ -0,0 +1,29 @@
+methods {
+    
+}
+
+rule sanity(env e, method f) {
+    calldataarg args;
+    f(e, args);
+    satisfy true;
+}
+
+// ghost mapping(Vault.Controller => mapping(Vault.FundId => Vault.Timestamp)) ghostName;
+    // init_state axiom forall uint256 a. ghostName[a] == 0;
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) ghostName {
+    init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. ghostName[controller][fundId] == 0;
+}
+// mapping(Controller => mapping(FundId => Fund)) private _funds;
+hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId] {
+    require ghostName[Controller][FundId] == require_uint40(defaultValue);
+}
+
+
+
+
+// (∀ controller ∈ Controller, fundId ∈ FundId:
+//   fund.lockExpiry <= fund.lockMaximum
+//   where fund = _funds[controller][fundId])
+// STATUS - in progress 
+// invariant lockExpiryLELockMaximum()
diff --git a/remappings.txt b/remappings.txt
new file mode 100644
index 0000000..5796d3d
--- /dev/null
+++ b/remappings.txt
@@ -0,0 +1,4 @@
+@ensdomains/=node_modules/@ensdomains/
+@openzeppelin/=node_modules/@openzeppelin/
+hardhat-deploy/=node_modules/hardhat-deploy/
+hardhat/=node_modules/hardhat/