Adding invariants after Vault update

certora/README.md

@@ -0,0 +1,64 @@
+# Formal Verification of Vault
+
+All funds in Codex are handled by the Vault contract.  This is a
+small contract that separates funds for different users and checks
+that accounting is done correctly.  In addition it allows the users
+to withdraw their funds after the locks expired, even if the main
+contract breaks.  Thus it gives users a guarantee they can always
+access their funds.
+
+This guarantee requires that the accounting the Vault itself does
+is correct.  This is the goal of the verification project.  It
+formally proves several properties of the Vault contract.
+
+## Usage
+
+Install the Certora Prover.  Then run the verification with
+
+certoraRun certora/confs/Vault.conf
+
+## Properties
+
+We check several properties for the Vault contract:
+
+1. The current lock expiry time is always less or equal the lockMaximum.
+2. The available balance of each account is large enoguh to cover
+   the outgoing flow until the maximum lock time.
+3. The sum of all incoming flows equals the sum of all outgoing flows.
+4. The sum of all expected funds (as defined in property 7) is always less
+   than or equal to the current balance of the contract. 
+5. Before a fund id is locked and flows can start, there is never an
+   outgoing flow for any account in this fund.
+6. The last updated timestamp for flows in each account is never in 
+   the future and always on or before the lock time.
+7. The expected funds for each account is the available balance plus the
+   dedicated balance plus the incoming flows minus the outgoing flows
+   from the last time updated until the end of the flow (either lock
+   time or freeze time).  These funds are always non-negative (i.e. no
+   account can be in debt to the protocol in the future due to outgoing
+   flows).
+
+The forth property (solvency) is the main property we need to show to
+guarantee that the funds are accounted correctly.
+
+## Limitations
+
+We prove the solvency invariant only for a standard ERC20 token as
+implemented in the OpenZepellin library.  In particular, the contract
+assumes that transfering tokens work as expected, that no fee is taken
+by the token contract and that no unexpected balance changes can occur.
+
+To prove that changing the lock time or freezing the funds does not change
+the funds required by the contract, we cannot use the Certora Prover itself
+ as the underlying SMT solvers cannot natively reason about sums over
+all elements in a mapping.  Instead we add this as an assumption to the
+specification and argue its correctness property manually as follows.
+
+Changing the lock time or freezing the funds will change the expected
+balance because the time where the flows end changes.  It will change the
+expected funds of each account by `timedelta*(incoming - outgoing)` where
+`timedelta` is the difference of the previous and the new end time of
+flows.  So the sum of all expected funds is changed by 
+`timedelta*(sum of incoming - sum of outgoing)`.  This is zero because
+of Property 3.
+

certora/confs/Marketplace.conf

@@ -19,4 +19,5 @@
     "loop_iter": "3",
     "optimistic_hashing": true,
     "hashing_length_bound": "512",
+    "solc": "solc8.28",
 }

certora/confs/Vault.conf

@@ -0,0 +1,45 @@
+{
+    "files": [
+        "certora/harness/VaultHarness.sol",
+        "certora/helpers/ERC20A.sol",
+    ],
+    "parametric_contracts": ["VaultHarness"],
+    "link" : [
+        "VaultHarness:_token=ERC20A",
+    ],
+    "packages": [
+        "@openzeppelin/=node_modules/@openzeppelin/",
+    ],
+    //"msg": "Verifying Vault",
+    "multi_assert_check": true,
+    "rule_sanity": "basic",
+    "verify": "VaultHarness:certora/specs/Vault.spec",
+    "loop_iter": "3",
+    "build_cache": true,
+    "solc": "solc8.28",
+    "prover_version": "master", // remove with next Certora release
+    "mutations": {
+        "manual_mutants": [
+            {
+                "file_to_mutate": "contracts/Vault.sol",
+                "mutants_location": "certora/mutations/Vault"
+            },
+            {
+                "file_to_mutate": "contracts/Timestamps.sol",
+                "mutants_location": "certora/mutations/Timestamps"
+            },
+            {
+                "file_to_mutate": "contracts/vault/Accounts.sol",
+                "mutants_location": "certora/mutations/Accounts"
+            },
+            {
+                "file_to_mutate": "contracts/vault/Funds.sol",
+                "mutants_location": "certora/mutations/Funds"
+            },
+            {
+                "file_to_mutate": "contracts/vault/VaultBase.sol",
+                "mutants_location": "certora/mutations/VaultBase"
+            }
+        ]
+    }
+}

certora/harness/VaultHarness.sol

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.28;
+
+import "../../contracts/Vault.sol";
+
+contract VaultHarness is Vault {
+  constructor(IERC20 token) Vault(token) {}
+
+    function publicStatus(
+        Controller controller,
+        FundId fundId
+    ) public view returns (FundStatus) {
+        return _getFundStatus(controller, fundId);
+    }
+
+    function unwrapTimestamp(
+        Timestamp timestamp
+    ) public pure returns (uint40) {
+        return Timestamp.unwrap(timestamp);
+    }
+
+}

certora/mutations/001_accumulateFlows_off_by_one.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol
+index 3066e7d..c93554d 100644
+--- a/contracts/vault/Accounts.sol
++++ b/contracts/vault/Accounts.sol
+@@ -81,7 +81,7 @@ library Accounts {
+     Timestamp timestamp
+   ) internal pure {
+     Duration duration = account.flow.updated.until(timestamp);
+-    account.balance.available -= account.flow.outgoing.accumulate(duration);
++    account.balance.available -= account.flow.outgoing.accumulate(duration) + 1;
+     account.balance.designated += account.flow.incoming.accumulate(duration);
+     account.flow.updated = timestamp;
+   }

certora/mutations/002_flowOut_rate_calculation.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol
+index 3066e7d..7ddae11 100644
+--- a/contracts/vault/Accounts.sol
++++ b/contracts/vault/Accounts.sol
+@@ -102,7 +102,7 @@ library Accounts {
+     if (rate <= account.flow.incoming) {
+       account.flow.incoming = account.flow.incoming - rate;
+     } else {
+-      account.flow.outgoing = account.flow.outgoing + rate;
++      account.flow.outgoing = account.flow.outgoing + rate + TokensPerSecond.wrap(1);
+       account.flow.outgoing = account.flow.outgoing - account.flow.incoming;
+       account.flow.incoming = TokensPerSecond.wrap(0);
+     }

certora/mutations/003_status_boundary_condition.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Funds.sol b/contracts/vault/Funds.sol
+index 471c2d9..1b0e7b9 100644
+--- a/contracts/vault/Funds.sol
++++ b/contracts/vault/Funds.sol
+@@ -37,7 +37,7 @@ enum FundStatus {
+
+ library Funds {
+   function status(Fund memory fund) internal view returns (FundStatus) {
+-    if (Timestamps.currentTime() < fund.lockExpiry) {
++    if (Timestamps.currentTime() <= fund.lockExpiry) {
+       if (fund.frozenAt != Timestamp.wrap(0)) {
+         return FundStatus.Frozen;
+       }

certora/mutations/004_isSolventAt_boundary_condition.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol
+index 3066e7d..c4db427 100644
+--- a/contracts/vault/Accounts.sol
++++ b/contracts/vault/Accounts.sol
+@@ -69,7 +69,7 @@ library Accounts {
+   ) internal pure returns (bool) {
+     Duration duration = account.flow.updated.until(timestamp);
+     uint128 outgoing = account.flow.outgoing.accumulate(duration);
+-    return outgoing <= account.balance.available;
++    return outgoing < account.balance.available;
+   }
+
+   /// Updates the available and designated balances by accumulating the

certora/mutations/005_flowIn_future_timestamp.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol
+index 3066e7d..1d2ff07 100644
+--- a/contracts/vault/Accounts.sol
++++ b/contracts/vault/Accounts.sol
+@@ -89,7 +89,7 @@ library Accounts {
+   /// Starts an incoming flow of tokens at the specified rate. If there already
+   /// is a flow of incoming tokens, then its rate is increased accordingly.
+   function flowIn(Account memory account, TokensPerSecond rate) internal view {
+-    account.accumulateFlows(Timestamps.currentTime());
++    account.accumulateFlows(Timestamps.currentTime().add(Duration.wrap(1)));
+     account.flow.incoming = account.flow.incoming + rate;
+   }
+

certora/mutations/006_flow_prelock_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..22deafc 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -189,7 +189,7 @@ abstract contract VaultBase {
+     TokensPerSecond rate
+   ) internal {
+     Fund memory fund = _funds[controller][fundId];
+-    require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
++    require(fund.status() == FundStatus.Locked || fund.status() == FundStatus.Inactive, VaultFundNotLocked());
+
+     Account memory sender = _accounts[controller][fundId][from];
+     sender.flowOut(rate);

certora/mutations/007_checkAccountInvariant_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..c90a675 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -268,7 +268,7 @@ abstract contract VaultBase {
+     Account memory account,
+     Fund memory fund
+   ) private pure {
+-    require(account.isSolventAt(fund.lockMaximum), VaultInsufficientBalance());
++    // require(account.isSolventAt(fund.lockMaximum), VaultInsufficientBalance());
+   }
+
+   error VaultInsufficientBalance();

certora/mutations/008_deposit_storage_corruption.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..9e22028 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -130,7 +130,7 @@ abstract contract VaultBase {
+     Fund storage fund = _funds[controller][fundId];
+     require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
+
+-    Account storage account = _accounts[controller][fundId][accountId];
++    Account memory account = _accounts[controller][fundId][accountId];
+
+     account.balance.available += amount;
+

certora/mutations/009_transfer_balance_check_removal.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..94fca9a 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -171,7 +171,7 @@ abstract contract VaultBase {
+     require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
+
+     Account memory sender = _accounts[controller][fundId][from];
+-    require(amount <= sender.balance.available, VaultInsufficientBalance());
++    // require(amount <= sender.balance.available, VaultInsufficientBalance());
+
+     sender.balance.available -= amount;
+     _checkAccountInvariant(sender, fund);

certora/mutations/010_burnAccount_logic_inversion.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..f22b4ed 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -227,7 +227,7 @@ abstract contract VaultBase {
+     require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
+
+     Account memory account = _accounts[controller][fundId][accountId];
+-    require(account.flow.incoming == account.flow.outgoing, VaultFlowNotZero());
++    require(!(account.flow.incoming == account.flow.outgoing), VaultFlowNotZero());
+     uint128 amount = account.balance.available + account.balance.designated;
+
+     delete _accounts[controller][fundId][accountId];

certora/mutations/011_withdraw_reentrancy_ordering.patch

@@ -0,0 +1,17 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..ddfaad7 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -254,10 +254,10 @@ abstract contract VaultBase {
+     account.accumulateFlows(fund.flowEnd());
+     uint128 amount = account.balance.available + account.balance.designated;
+
+-    delete _accounts[controller][fundId][accountId];
+-
+     (address owner, ) = Accounts.decodeId(accountId);
+     _token.safeTransfer(owner, amount);
++
++    delete _accounts[controller][fundId][accountId];
+   }
+
+   function _checkLockInvariant(Fund memory fund) private pure {

certora/mutations/012_withdraw_unsafe_transfer.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..f3eef7d 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -257,7 +257,7 @@ abstract contract VaultBase {
+     delete _accounts[controller][fundId][accountId];
+
+     (address owner, ) = Accounts.decodeId(accountId);
+-    _token.safeTransfer(owner, amount);
++    _token.transfer(owner, amount);
+   }
+
+   function _checkLockInvariant(Fund memory fund) private pure {

certora/mutations/013_deposit_unsafe_transferFrom.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..30c52fd 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -134,7 +134,7 @@ abstract contract VaultBase {
+
+     account.balance.available += amount;
+
+-    _token.safeTransferFrom(
++    _token.transferFrom(
+       Controller.unwrap(controller),
+       address(this),
+       amount

certora/mutations/014_all_unsafe_token_transfers.patch

@@ -0,0 +1,40 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..5efdc8e 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -134,7 +134,7 @@ abstract contract VaultBase {
+
+     account.balance.available += amount;
+
+-    _token.safeTransferFrom(
++    _token.transferFrom(
+       Controller.unwrap(controller),
+       address(this),
+       amount
+@@ -215,7 +215,7 @@ abstract contract VaultBase {
+
+     account.balance.designated -= amount;
+
+-    _token.safeTransfer(address(0xdead), amount);
++    _token.transfer(address(0xdead), amount);
+   }
+
+   function _burnAccount(
+@@ -232,7 +232,7 @@ abstract contract VaultBase {
+
+     delete _accounts[controller][fundId][accountId];
+
+-    _token.safeTransfer(address(0xdead), amount);
++    _token.transfer(address(0xdead), amount);
+   }
+
+   function _freezeFund(Controller controller, FundId fundId) internal {
+@@ -257,7 +257,7 @@ abstract contract VaultBase {
+     delete _accounts[controller][fundId][accountId];
+
+     (address owner, ) = Accounts.decodeId(accountId);
+-    _token.safeTransfer(owner, amount);
++    _token.transfer(owner, amount);
+   }
+
+   function _checkLockInvariant(Fund memory fund) private pure {

certora/mutations/015_transfer_authorization_bypass.patch

@@ -0,0 +1,14 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..5dd18c8 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -164,7 +164,8 @@ contract Vault is VaultBase, Pausable, Ownable {
+     AccountId to,
+     uint128 amount
+   ) public whenNotPaused {
+-    Controller controller = Controller.wrap(msg.sender);
++    (address holder, ) = Accounts.decodeId(from);
++    Controller controller = Controller.wrap(holder);
+     _transfer(controller, fundId, from, to, amount);
+   }
+