From 17ebb6909da3ab85fb435cfaba0c3a4a6cb90e68 Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Fri, 30 May 2025 00:32:25 +0100
Subject: [PATCH] tmp save

---
 certora/confs/Marketplace.conf |  1 +
 certora/specs/Vault.spec       | 82 +++++++++++++++++++++++++++++++---
 2 files changed, 77 insertions(+), 6 deletions(-)

diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf
index 395ebae..63b580a 100644
--- a/certora/confs/Marketplace.conf
+++ b/certora/confs/Marketplace.conf
@@ -19,4 +19,5 @@
     "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
index 4e2be76..cb69299 100644
--- a/certora/specs/Vault.spec
+++ b/certora/specs/Vault.spec
@@ -1,5 +1,9 @@
+using ERC20A as Token;
+
 methods {
     function unwrapTimestamp(VaultBase.Timestamp) external returns (uint40) envfree;
+
+    function Token.totalSupply() external returns (uint256) envfree;
 }
 
 // rule sanity(env e, method f) {
@@ -9,6 +13,30 @@ methods {
 // }
 
 
+
+
+
+ghost mathint sumOfBalances {
+    init_state axiom sumOfBalances == 0;
+}
+
+hook Sload uint256 balance Token._balances[KEY address addr] {
+    require sumOfBalances >= to_mathint(balance);
+}
+
+hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+invariant totalSupplyIsSumOfBalances()
+    to_mathint(Token.totalSupply()) == sumOfBalances;
+
+
+
+
+
+
+
 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror {
     init_state axiom 
         forall VaultBase.Controller controller. 
@@ -211,6 +239,52 @@ invariant outgoingLEAvailableEasySingle(VaultBase.Controller controller, VaultBa
 
     
 
+invariant supporter()
+    forall VaultBase.Controller controller.
+    forall VaultBase.FundId fundId.
+    forall VaultBase.AccountId accountId.
+        lockMaximumMirror[controller][fundId] == 0 => outgoingMirror[controller][fundId][accountId] == 0;
+
+
+
+
+
+
+
+
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint128)) valueMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+            valueMirror[controller][fundId] == 0;
+}
+
+hook Sload uint128 defaultValue 
+    _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].value 
+{
+    require valueMirror[Controller][FundId] == defaultValue;
+}
+
+hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].value 
+    uint128 defaultValue
+{
+    valueMirror[Controller][FundId] = defaultValue;
+}
+
+
+
+invariant fundCorrelation()
+    
+
+
+
+
+
+
+
+
+
 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) incomingMirror {
     init_state axiom 
         (forall VaultBase.Controller controller. 
@@ -235,6 +309,8 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId
 }
 
 
+
+
 // (∀ controller ∈ Controller, fundId ∈ FundId:
 //   (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) =
 //   (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing)
@@ -315,9 +391,3 @@ definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) r
 //                 * (lockMaximumMirror[controller][fundId] 
 //                     - updatedMirror[controller][fundId][accountId])) 
 //         == _funds[controller][fundId].value;    
-
-
-
-
-
-