Merge a7d0332a584653a516fce240008cf5c9c9f0dc52 into b5ab3869b949f651a3ed9aeb914feed7bd0dfd47

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);
+   }
+ 

certora/mutations/016_pause_functions_deleted.patch

@@ -0,0 +1,18 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..185ed83 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -240,13 +240,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     _withdraw(controller, fund, accountId);
+   }
+ 
+-  function pause() public onlyOwner {
+-    _pause();
+-  }
+ 
+-  function unpause() public onlyOwner {
+-    _unpause();
+-  }
+ 
+   error VaultOnlyAccountHolder();
+ }

certora/mutations/017_accountId_encoding_corruption.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol
+index 3066e7d..ae138ae 100644
+--- a/contracts/vault/Accounts.sol
++++ b/contracts/vault/Accounts.sol
+@@ -50,7 +50,7 @@ library Accounts {
+   ) internal pure returns (AccountId) {
+     bytes32 left = bytes32(bytes20(holder));
+     bytes32 right = bytes32(uint256(uint96(discriminator)));
+-    return AccountId.wrap(left | right);
++    return AccountId.wrap(left & right);
+   }
+ 
+   /// Extracts the account holder and the discriminator from the the account id

certora/mutations/018_duration_calculation_order_inversion.patch

@@ -0,0 +1,12 @@
+diff --git a/contracts/Timestamps.sol b/contracts/Timestamps.sol
+index 945eced..3132942 100644
+--- a/contracts/Timestamps.sol
++++ b/contracts/Timestamps.sol
+@@ -65,6 +65,6 @@ library Timestamps {
+     Timestamp start,
+     Timestamp end
+   ) internal pure returns (Duration) {
+-    return Duration.wrap(Timestamp.unwrap(end) - Timestamp.unwrap(start));
++    return Duration.wrap(Timestamp.unwrap(start) - Timestamp.unwrap(end));
+   }
+ }

certora/mutations/019_period_calculation_round_up.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Periods.sol b/contracts/Periods.sol
+index 189fb02..a54c439 100644
+--- a/contracts/Periods.sol
++++ b/contracts/Periods.sol
+@@ -20,7 +20,7 @@ contract Periods {
+   function _periodOf(Timestamp timestamp) internal view returns (Period) {
+     return
+       Period.wrap(
+-        Timestamp.unwrap(timestamp) / Duration.unwrap(_secondsPerPeriod)
++        (Timestamp.unwrap(timestamp) + Duration.unwrap(_secondsPerPeriod) - 1) / Duration.unwrap(_secondsPerPeriod)
+       );
+   }
+ 

certora/mutations/020_withdraw_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..8397373 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -221,7 +221,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+   /// ⚠️ The account holder can also withdraw itself, so when designing a smart
+   /// contract that controls funds in the vault, don't assume that only this
+   /// smart contract can initiate a withdrawal ⚠️
+-  function withdraw(FundId fund, AccountId accountId) public whenNotPaused {
++  function withdraw(FundId fund, AccountId accountId) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _withdraw(controller, fund, accountId);
+   }

certora/mutations/021_deposit_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..ac8b1cd 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -138,7 +138,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     FundId fundId,
+     AccountId accountId,
+     uint128 amount
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _deposit(controller, fundId, accountId, amount);
+   }

certora/mutations/022_transfer_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..42a3b9b 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -163,7 +163,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     AccountId from,
+     AccountId to,
+     uint128 amount
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _transfer(controller, fundId, from, to, amount);
+   }

certora/mutations/023_flow_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..52b7db0 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -180,7 +180,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     AccountId from,
+     AccountId to,
+     TokensPerSecond rate
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _flow(controller, fundId, from, to, rate);
+   }

certora/mutations/024_lock_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..26a17b0 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -116,7 +116,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     FundId fundId,
+     Timestamp expiry,
+     Timestamp maximum
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _lock(controller, fundId, expiry, maximum);
+   }

certora/mutations/025_extendLock_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..f8fcddf 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -125,7 +125,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+   /// the existing expiry, but no later than the maximum timestamp that was
+   /// provided when locking the fund.
+   /// Only allowed when the lock has not unlocked yet.
+-  function extendLock(FundId fundId, Timestamp expiry) public whenNotPaused {
++  function extendLock(FundId fundId, Timestamp expiry) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _extendLock(controller, fundId, expiry);
+   }

certora/mutations/026_designate_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..15af8af 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -151,7 +151,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     FundId fundId,
+     AccountId accountId,
+     uint128 amount
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _designate(controller, fundId, accountId, amount);
+   }

certora/mutations/027_burnDesignated_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..c9b39f2 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -191,7 +191,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     FundId fundId,
+     AccountId accountId,
+     uint128 amount
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _burnDesignated(controller, fundId, accountId, amount);
+   }

certora/mutations/028_burnAccount_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..de9c8d2 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -202,7 +202,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+   function burnAccount(
+     FundId fundId,
+     AccountId accountId
+-  ) public whenNotPaused {
++  ) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _burnAccount(controller, fundId, accountId);
+   }

certora/mutations/029_freezeFund_pause_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..4037209 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -210,7 +210,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+   /// Freezes a fund. Stops all tokens flows and disallows any operations on the
+   /// fund until it unlocks.
+   /// Only allowed when the fund is locked.
+-  function freezeFund(FundId fundId) public whenNotPaused {
++  function freezeFund(FundId fundId) public {
+     Controller controller = Controller.wrap(msg.sender);
+     _freezeFund(controller, fundId);
+   }

certora/mutations/030_add_missing_whenNotPaused_withdrawByRecipient.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..0d76718 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -234,7 +234,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     Controller controller,
+     FundId fund,
+     AccountId accountId
+-  ) public {
++  ) public whenNotPaused {
+     (address holder, ) = Accounts.decodeId(accountId);
+     require(msg.sender == holder, VaultOnlyAccountHolder());
+     _withdraw(controller, fund, accountId);

certora/mutations/031_pause_access_control_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..c98627e 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -240,7 +240,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     _withdraw(controller, fund, accountId);
+   }
+ 
+-  function pause() public onlyOwner {
++  function pause() public {
+     _pause();
+   }
+ 

certora/mutations/032_unpause_access_control_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..6b80271 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -244,7 +244,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     _pause();
+   }
+ 
+-  function unpause() public onlyOwner {
++  function unpause() public {
+     _unpause();
+   }
+ 

certora/mutations/033_withdrawByRecipient_auth_bypass.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Vault.sol b/contracts/Vault.sol
+index 8433a08..e7e012d 100644
+--- a/contracts/Vault.sol
++++ b/contracts/Vault.sol
+@@ -236,7 +236,7 @@ contract Vault is VaultBase, Pausable, Ownable {
+     AccountId accountId
+   ) public {
+     (address holder, ) = Accounts.decodeId(accountId);
+-    require(msg.sender == holder, VaultOnlyAccountHolder());
++    // require(msg.sender == holder, VaultOnlyAccountHolder());
+     _withdraw(controller, fund, accountId);
+   }
+ 

certora/mutations/034_nextPeriod_advancement_failure.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/Periods.sol b/contracts/Periods.sol
+index 189fb02..817d09c 100644
+--- a/contracts/Periods.sol
++++ b/contracts/Periods.sol
+@@ -29,7 +29,7 @@ contract Periods {
+   }
+ 
+   function _nextPeriod(Period period) internal pure returns (Period) {
+-    return Period.wrap(Period.unwrap(period) + 1);
++    return Period.wrap(Period.unwrap(period));
+   }
+ 
+   function _periodStart(Period period) internal view returns (Timestamp) {

certora/mutations/035_withdraw_account_not_deleted.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..ed1fb5f 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -254,8 +254,6 @@ 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);
+   }

certora/mutations/036_burnAccount_not_deleted.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..eb679d1 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -230,8 +230,6 @@ abstract contract VaultBase {
+     require(account.flow.incoming == account.flow.outgoing, VaultFlowNotZero());
+     uint128 amount = account.balance.available + account.balance.designated;
+ 
+-    delete _accounts[controller][fundId][accountId];
+-
+     _token.safeTransfer(address(0xdead), amount);
+   }
+ 

certora/mutations/037_burnDesignated_no_decrement.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..29725dc 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -213,7 +213,7 @@ abstract contract VaultBase {
+     Account storage account = _accounts[controller][fundId][accountId];
+     require(account.balance.designated >= amount, VaultInsufficientBalance());
+ 
+-    account.balance.designated -= amount;
++    // account.balance.designated -= amount;
+ 
+     _token.safeTransfer(address(0xdead), amount);
+   }

certora/mutations/038_extendLock_beyond_max.patch

@@ -0,0 +1,12 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..e461233 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -117,7 +117,6 @@ abstract contract VaultBase {
+     require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
+     require(fund.lockExpiry <= expiry, VaultInvalidExpiry());
+     fund.lockExpiry = expiry;
+-    _checkLockInvariant(fund);
+     _funds[controller][fundId] = fund;
+   }
+ 

certora/mutations/039_freezeFunds_when_withdrawing.patch

@@ -0,0 +1,13 @@
+diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol
+index be21481..04e914f 100644
+--- a/contracts/vault/VaultBase.sol
++++ b/contracts/vault/VaultBase.sol
+@@ -237,7 +237,7 @@ abstract contract VaultBase {
+ 
+   function _freezeFund(Controller controller, FundId fundId) internal {
+     Fund storage fund = _funds[controller][fundId];
+-    require(fund.status() == FundStatus.Locked, VaultFundNotLocked());
++    require(fund.status() == FundStatus.Locked || fund.status() == FundStatus.Withdrawing, VaultFundNotLocked());
+ 
+     fund.frozenAt = Timestamps.currentTime();
+   }

certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch

@@ -0,0 +1 @@
+../001_accumulateFlows_off_by_one.patch

certora/mutations/Accounts/002_flowOut_rate_calculation.patch

@@ -0,0 +1 @@
+../002_flowOut_rate_calculation.patch

certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch

@@ -0,0 +1 @@
+../004_isSolventAt_boundary_condition.patch

certora/mutations/Accounts/005_flowIn_future_timestamp.patch

@@ -0,0 +1 @@
+../005_flowIn_future_timestamp.patch

certora/mutations/Accounts/017_accountId_encoding_corruption.patch

@@ -0,0 +1 @@
+../017_accountId_encoding_corruption.patch

certora/mutations/Funds/003_status_boundary_condition.patch

@@ -0,0 +1 @@
+../003_status_boundary_condition.patch

certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch

@@ -0,0 +1 @@
+../018_duration_calculation_order_inversion.patch

certora/mutations/Vault/015_transfer_authorization_bypass.patch

@@ -0,0 +1 @@
+../015_transfer_authorization_bypass.patch

certora/mutations/Vault/016_pause_functions_deleted.patch

@@ -0,0 +1 @@
+../016_pause_functions_deleted.patch

certora/mutations/Vault/020_withdraw_pause_bypass.patch

@@ -0,0 +1 @@
+../020_withdraw_pause_bypass.patch

certora/mutations/Vault/021_deposit_pause_bypass.patch

@@ -0,0 +1 @@
+../021_deposit_pause_bypass.patch

certora/mutations/Vault/022_transfer_pause_bypass.patch

@@ -0,0 +1 @@
+../022_transfer_pause_bypass.patch

certora/mutations/Vault/023_flow_pause_bypass.patch

@@ -0,0 +1 @@
+../023_flow_pause_bypass.patch

certora/mutations/Vault/024_lock_pause_bypass.patch

@@ -0,0 +1 @@
+../024_lock_pause_bypass.patch

certora/mutations/Vault/025_extendLock_pause_bypass.patch

@@ -0,0 +1 @@
+../025_extendLock_pause_bypass.patch

certora/mutations/Vault/026_designate_pause_bypass.patch

@@ -0,0 +1 @@
+../026_designate_pause_bypass.patch

certora/mutations/Vault/027_burnDesignated_pause_bypass.patch

@@ -0,0 +1 @@
+../027_burnDesignated_pause_bypass.patch

certora/mutations/Vault/028_burnAccount_pause_bypass.patch

@@ -0,0 +1 @@
+../028_burnAccount_pause_bypass.patch

certora/mutations/Vault/029_freezeFund_pause_bypass.patch

@@ -0,0 +1 @@
+../029_freezeFund_pause_bypass.patch

certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch

@@ -0,0 +1 @@
+../030_add_missing_whenNotPaused_withdrawByRecipient.patch

certora/mutations/Vault/031_pause_access_control_bypass.patch

@@ -0,0 +1 @@
+../031_pause_access_control_bypass.patch

certora/mutations/Vault/032_unpause_access_control_bypass.patch

@@ -0,0 +1 @@
+../032_unpause_access_control_bypass.patch

certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch

@@ -0,0 +1 @@
+../033_withdrawByRecipient_auth_bypass.patch

certora/mutations/VaultBase/006_flow_prelock_bypass.patch

@@ -0,0 +1 @@
+../006_flow_prelock_bypass.patch

certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch

@@ -0,0 +1 @@
+../007_checkAccountInvariant_bypass.patch

certora/mutations/VaultBase/008_deposit_storage_corruption.patch

@@ -0,0 +1 @@
+../008_deposit_storage_corruption.patch

certora/mutations/VaultBase/009_transfer_balance_check_removal.patch

@@ -0,0 +1 @@
+../009_transfer_balance_check_removal.patch

certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch

@@ -0,0 +1 @@
+../010_burnAccount_logic_inversion.patch

certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch

@@ -0,0 +1 @@
+../011_withdraw_reentrancy_ordering.patch

certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch

@@ -0,0 +1 @@
+../012_withdraw_unsafe_transfer.patch

certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch

@@ -0,0 +1 @@
+../013_deposit_unsafe_transferFrom.patch

certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch

@@ -0,0 +1 @@
+../014_all_unsafe_token_transfers.patch

certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch

@@ -0,0 +1 @@
+../035_withdraw_account_not_deleted.patch

certora/mutations/VaultBase/036_burnAccount_not_deleted.patch

@@ -0,0 +1 @@
+../036_burnAccount_not_deleted.patch

certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch

@@ -0,0 +1 @@
+../037_burnDesignated_no_decrement.patch

certora/mutations/VaultBase/038_extendLock_beyond_max.patch

@@ -0,0 +1 @@
+../038_extendLock_beyond_max.patch

certora/mutations/VaultBase/039_freezeFunds_when_withdrawing.patch

@@ -0,0 +1 @@
+../039_freezeFunds_when_withdrawing.patch

certora/specs/Vault.spec

@@ -0,0 +1,488 @@
+using ERC20A as Token;
+
+methods {
+    function unwrapTimestamp(VaultBase.Timestamp) external returns (uint40) envfree;
+    function decodeAccountId(VaultBase.AccountId) external returns (address, bytes12) envfree;
+
+    function Token.totalSupply() external returns (uint256) envfree;
+}
+
+// Timestamp reasoning.
+//
+// We use a ghost variable lastTimestamp to keep track of the last timestamp recorded in the contract.
+// This is used to ensure that timestamps are always increasing.  We also ensure that the timestamp
+// does not exceed the uint40 range, which is sufficient for our use case (up to year 36812).
+
+ghost mathint lastTimestamp {
+    init_state axiom lastTimestamp > 0; // we must start with a positive timestamp (0 is used to encode "not set")
+}
+
+hook TIMESTAMP uint256 time {
+    require(to_mathint(time) < max_uint40, "timestamp must not exceed uint40 range (year 36812)");
+    require(to_mathint(time) >= lastTimestamp, "timestamp must be increasing");
+    lastTimestamp = time;
+}
+
+
+//
+// Expected Funds - needed for proving solvency.
+//
+// expectedFunds[controller][fundId][accountId] is a ghost variable that represents the expected funds for a given account in a fund.
+// It is calculated as:
+// availableBalance + designatedBalance + ((incoming - outgoing) * (flowEnd - updated))
+//
+// Here flowEnd is either frozenAt or lockExpiry, depending on whether the fund is frozen or not.
+// The variable updated is the last time the flow was updated for the account in the fund, so all flows before
+// are already considered in the availableBalance.
+//
+// We recompute expectedFunds in the store hooks whenever one of the dependencies changes.
+// To avoid negative values, we cap the expectedFunds to 0.  It can only temporarily go negative and will
+// either revert (e.g. when setting outflow too high), or be corrected by another updated to a different variable.
+// We check that explicitly in the invariant expectedFundsMirror().
+
+definition max(mathint a, mathint b) returns mathint = a >= b ? a : b;
+
+definition flowEnd(VaultBase.Controller controller, VaultBase.FundId fundId) returns uint256 
+                                                                = frozenAtMirror[controller][fundId] != 0 
+                                                                    ? frozenAtMirror[controller][fundId] 
+                                                                    : lockExpiryMirror[controller][fundId];
+definition expectedFundsHelper(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) returns mathint =
+    availableBalanceMirror[controller][fundId][accountId]
+    + designatedBalanceMirror[controller][fundId][accountId]
+    + ((incomingMirror[controller][fundId][accountId] 
+    - outgoingMirror[controller][fundId][accountId]) 
+    * (flowEnd(controller, fundId) 
+        - updatedMirror[controller][fundId][accountId]));
+definition expectedFundsDef(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) returns mathint =
+    max(expectedFundsHelper(controller, fundId, accountId), 0);
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => mathint))) expectedFunds {
+    init_state axiom 
+        (forall VaultBase.Controller controller. 
+         forall VaultBase.FundId fundId. 
+         forall VaultBase.AccountId accountId. 
+            expectedFunds[controller][fundId][accountId] == 0) && 
+        (usum VaultBase.AccountId accountId, 
+                VaultBase.Controller controller, 
+                VaultBase.FundId fundId. 
+                    expectedFunds[controller][fundId][accountId]) == 0;
+}
+
+definition sumOfExpectedFunds() returns mathint =
+    (usum VaultBase.Controller controller, 
+            VaultBase.FundId fundId, 
+            VaultBase.AccountId accountId. 
+                expectedFunds[controller][fundId][accountId]);
+
+
+// mirror variables of balances in our dummy token.
+//
+// also prove that totalSupply equals the sum of all balances in the mirror.  This is needed
+// to prevent overflows in transfer().
+
+ghost mapping(address => uint256) tokenBalanceOfMirror {
+    init_state axiom (forall address a. tokenBalanceOfMirror[a] == 0)
+        && (usum address a. tokenBalanceOfMirror[a]) == 0;
+}
+
+hook Sload uint256 balance Token._balances[KEY address addr] {
+    require(tokenBalanceOfMirror[addr] == balance, "tokenBalance mirror");
+}
+
+hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
+    tokenBalanceOfMirror[addr] = newValue;
+}
+
+invariant totalSupplyIsSumOfBalances()
+    Token.totalSupply() == (usum address a. tokenBalanceOfMirror[a]);
+
+
+//------------------------------------------------------------//
+// Mirror variables for storage variables in VaultBase.
+//------------------------------------------------------------//
+
+// mirror for lockExpiry.
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+            lockExpiryMirror[controller][fundId] == 0;
+}
+
+hook Sload VaultBase.Timestamp defaultValue 
+    _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockExpiry 
+{
+    require(lockExpiryMirror[controller][fundId] == unwrapTimestamp(defaultValue), "lockExpiry mirror");
+}
+
+hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockExpiry 
+    VaultBase.Timestamp defaultValue
+{
+    lockExpiryMirror[controller][fundId] = unwrapTimestamp(defaultValue);
+
+    mathint oldSum = usum VaultBase.Controller c, 
+                            VaultBase.FundId f, 
+                            VaultBase.AccountId a. 
+                                expectedFunds[c][f][a];
+
+    havoc expectedFunds assuming forall VaultBase.Controller c. 
+                                 forall VaultBase.FundId f. 
+                                 forall VaultBase.AccountId a. 
+                                        expectedFunds@new[c][f][a] 
+                                            == expectedFundsDef(c, f, a);
+
+    // The above update of expectedFunds changes the individual funds for each account, because the
+    // flowEnd changes, but the sum of expected funds should not change, because the net flow between all funds is zero.
+    // This would require advanced reasoning over sums:  
+    // The individual expectedFunds change by the amount
+    //    deltaTime * (incoming - outgoing)
+    // The sum of these changes is 
+    //    deltaTime * ((sum AccountId a. incoming[a]) - (sum AccountId a. outgoing[a]))
+    // and that is zero, because of the invariant incomingEqualsOutgoing().
+    //
+    // This reasoning cannot be done by the certora prover and it's underlying SMT solvers.  Instead, we
+    // just require that this is true.
+    require((usum VaultBase.Controller c, 
+                            VaultBase.FundId f, 
+                            VaultBase.AccountId a. 
+                                expectedFunds[c][f][a]) == oldSum, 
+                                "sum of expected funds should not change as net flow between all funds is zero");
+}
+
+
+// mirror for lockMaximum.
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockMaximumMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+            lockMaximumMirror[controller][fundId] == 0;
+}
+
+hook Sload VaultBase.Timestamp defaultValue 
+    _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockMaximum 
+{
+    require(lockMaximumMirror[controller][fundId] == unwrapTimestamp(defaultValue), "lockMaximum mirror");
+}
+
+hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockMaximum 
+    VaultBase.Timestamp defaultValue
+{
+    lockMaximumMirror[controller][fundId] = unwrapTimestamp(defaultValue);
+}
+
+
+// mirror for outgoing flow
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) outgoingMirror {
+    init_state axiom 
+        (forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        forall VaultBase.AccountId accountId. 
+            outgoingMirror[controller][fundId][accountId] == 0) && 
+        (forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        (sum VaultBase.AccountId accountId. outgoingMirror[controller][fundId][accountId]) == 0);
+}
+
+hook Sload VaultBase.TokensPerSecond defaultValue 
+    _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.outgoing
+{
+    require(outgoingMirror[controller][fundId][accountId] == defaultValue, "outgoing mirror");
+}
+
+hook Sstore _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.outgoing
+    VaultBase.TokensPerSecond defaultValue
+{
+    outgoingMirror[controller][fundId][accountId] = defaultValue;
+    expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId);
+}
+
+// mirror for updated  (last time the flow was updated for the account).
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint40))) updatedMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        forall VaultBase.AccountId accountId. 
+            updatedMirror[controller][fundId][accountId] == 0;
+}
+
+hook Sload VaultBase.Timestamp defaultValue
+    _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.updated
+{
+    require(updatedMirror[controller][fundId][accountId] == unwrapTimestamp(defaultValue), "updated mirror");
+}
+
+hook Sstore _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.updated
+    VaultBase.Timestamp defaultValue
+{
+    updatedMirror[controller][fundId][accountId] = unwrapTimestamp(defaultValue);
+    expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId);
+}   
+
+
+// mirror for available balance
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint128))) availableBalanceMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        forall VaultBase.AccountId accountId. 
+            availableBalanceMirror[controller][fundId][accountId] == 0;
+}
+
+hook Sload uint128 defaultValue
+    _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.available
+{
+    require(availableBalanceMirror[controller][fundId][accountId] == defaultValue, "available balance mirror"); 
+    requireInvariant expectedFundsMirror(controller, fundId, accountId);
+}   
+
+hook Sstore _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.available
+    uint128 defaultValue
+{
+    availableBalanceMirror[controller][fundId][accountId] = defaultValue;
+    expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId);
+}   
+
+// mirror for incoming flow
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) incomingMirror {
+    init_state axiom 
+        (forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        forall VaultBase.AccountId accountId. 
+            incomingMirror[controller][fundId][accountId] == 0) && 
+        (forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        (sum VaultBase.AccountId accountId. incomingMirror[controller][fundId][accountId]) == 0);
+}
+
+hook Sload VaultBase.TokensPerSecond defaultValue 
+    _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.incoming
+{
+    require(incomingMirror[controller][fundId][accountId] == defaultValue, "incoming mirror");
+}
+
+hook Sstore _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.incoming 
+    VaultBase.TokensPerSecond defaultValue
+{
+    incomingMirror[controller][fundId][accountId] = defaultValue;
+    expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId);
+}
+
+// mirror for frozenAt
+
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) frozenAtMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+            frozenAtMirror[controller][fundId] == 0;
+}
+
+hook Sload VaultBase.Timestamp defaultValue
+    _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt
+{
+    require(frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue), "frozenAt mirror");
+}
+
+hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].frozenAt
+    VaultBase.Timestamp defaultValue
+{
+    frozenAtMirror[controller][fundId] = unwrapTimestamp(defaultValue);
+
+    mathint oldSum = usum VaultBase.Controller c, 
+                            VaultBase.FundId f, 
+                            VaultBase.AccountId a. 
+                                expectedFunds[c][f][a];
+
+    havoc expectedFunds assuming forall VaultBase.Controller c. 
+                                 forall VaultBase.FundId f. 
+                                 forall VaultBase.AccountId a. 
+                                        expectedFunds@new[c][f][a] 
+                                            == expectedFundsDef(c, f, a);
+
+    // See the comment in the store hook for lockExpiry for an explanation of why this is true.
+    require((usum VaultBase.Controller c, 
+                            VaultBase.FundId f, 
+                            VaultBase.AccountId a. 
+                                expectedFunds[c][f][a]) == oldSum,
+                                "sum of expected funds should not change as net flow between all funds is zero");
+}
+
+// mirror for designated balance
+ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint128))) designatedBalanceMirror {
+    init_state axiom 
+        forall VaultBase.Controller controller. 
+        forall VaultBase.FundId fundId. 
+        forall VaultBase.AccountId accountId. 
+            designatedBalanceMirror[controller][fundId][accountId] == 0;
+}
+
+hook Sload uint128 defaultValue
+    _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.designated
+{
+    require(designatedBalanceMirror[controller][fundId][accountId] == defaultValue, "designated balance mirror");
+    requireInvariant expectedFundsMirror(controller, fundId, accountId);
+}   
+
+hook Sstore _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.designated
+    uint128 defaultValue
+{
+    designatedBalanceMirror[controller][fundId][accountId] = defaultValue;
+    expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId);
+} 
+
+// Auxiliary invariants
+
+// Timestamp must always be positive (non-zero).
+invariant timestampPositive() lastTimestamp > 0;
+
+
+//------------------------------------------------------------//
+// Invariants of the Vault
+//------------------------------------------------------------//
+
+// 1 - verified
+// lockExpiry is always less than or equal to lockMaximum.
+// (∀ controller ∈ Controller, fundId ∈ FundId:
+//   fund.lockExpiry <= fund.lockMaximum
+//   where fund = _funds[controller][fundId])
+invariant lockExpiryLELockMaximum()
+    forall VaultBase.Controller controller.
+    forall VaultBase.FundId fundId.
+        lockExpiryMirror[controller][fundId] <= lockMaximumMirror[controller][fundId];
+
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+
+// 2 - verified
+// the available balance of an account is large enough to cover the outgoing flow until the maximum lock time.  
+// (∀ controller ∈ Controller, fundId ∈ FundId, accountId ∈ AccountId:
+//   flow.outgoing * (fund.lockMaximum - flow.updated) <= balance.available
+//   where fund = _funds[controller][fundId])
+//   and flow = _accounts[controller][fundId][accountId].flow
+//   and balance = _accounts[controller][fundId][accountId].balance
+invariant outgoingLEAvailable()
+    forall VaultBase.Controller controller.
+    forall VaultBase.FundId fundId.
+    forall VaultBase.AccountId accountId.
+        (outgoingMirror[controller][fundId][accountId] 
+            * (lockMaximumMirror[controller][fundId] 
+                - updatedMirror[controller][fundId][accountId])) 
+        <= availableBalanceMirror[controller][fundId][accountId]
+{
+    preserved {
+            requireInvariant noOutflowBeforeLocked();
+    }
+}
+
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+
+definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus = 
+    lastTimestamp < lockExpiryMirror[controller][fundId] ? 
+        (frozenAtMirror[controller][fundId] != 0 ? VaultBase.FundStatus.Frozen : VaultBase.FundStatus.Locked) :
+            (lockMaximumMirror[controller][fundId] == 0 ? VaultBase.FundStatus.Inactive : VaultBase.FundStatus.Withdrawing);
+
+// 3 - verified
+// the sum of incoming flows equals the sum of outgoing flows each controller and fundId.
+// (∀ controller ∈ Controller, fundId ∈ FundId:
+//   (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) =
+//   (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing)
+//   where accounts = _accounts[controller][fundId])
+invariant incomingEqualsOutgoing()
+    (forall VaultBase.Controller controller.
+     forall VaultBase.FundId fundId.
+    statusCVL(controller, fundId) != VaultBase.FundStatus.Withdrawing
+        => (sum 
+                VaultBase.AccountId accountId. 
+                    outgoingMirror[controller][fundId][accountId]) 
+            == (sum
+                VaultBase.AccountId accountId. 
+                    incomingMirror[controller][fundId][accountId]));
+
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+
+// invariant 4 (Certora's solvency) - timeout in flow, all others varified
+// This is the solvency invariant:
+// sum of expected funds for all accounts in all funds must be less than or equal to the token balance of the contract.
+invariant solvency()
+    sumOfExpectedFunds() <= to_mathint(tokenBalanceOfMirror[currentContract])
+{
+    preserved {
+        requireInvariant updatedLETimestampAndFlowEnd();
+        requireInvariant lockExpiryLELockMaximum();
+        requireInvariant outgoingLEAvailable();
+        requireInvariant incomingEqualsOutgoing();
+        requireInvariant noOutflowBeforeLocked();
+    }
+
+    preserved deposit
+        (VaultBase.FundId fundId, 
+            VaultBase.AccountId accountId, uint128 amount) with (env e) {
+        requireInvariant totalSupplyIsSumOfBalances();
+        requireInvariant updatedLETimestampAndFlowEnd();
+        requireInvariant lockExpiryLELockMaximum();
+        requireInvariant outgoingLEAvailable();
+        requireInvariant incomingEqualsOutgoing();
+        requireInvariant noOutflowBeforeLocked();
+        require(e.msg.sender != currentContract, "deposit from vault not allowed");
+    }
+}
+
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+//------------------------------------------------------------//
+
+// 5 (needed to prove 2) - verified
+// as long as the funds are not yet locked, there must be not be any flows at all.
+// This is needed to ensure that setting the lock does not cause the flow invariant to break.
+invariant noOutflowBeforeLocked()
+    forall VaultBase.Controller controller.
+    forall VaultBase.FundId fundId.
+    forall VaultBase.AccountId accountId.
+        lockMaximumMirror[controller][fundId] == 0 => outgoingMirror[controller][fundId][accountId] == 0
+{
+    preserved {
+        requireInvariant timestampPositive();
+    }
+}
+
+
+// 6 - verified
+// the last updated timestamp does never exceed the current timestamp or the end of the flow.
+// This is needed to ensure that there is no negative time for the flow calculations in expectedFundsDef.
+invariant updatedLETimestampAndFlowEnd()
+    forall VaultBase.Controller controller. 
+    forall VaultBase.FundId fundId. 
+    forall VaultBase.AccountId accountId. 
+        updatedMirror[controller][fundId][accountId] <= flowEnd(controller, fundId) 
+        && updatedMirror[controller][fundId][accountId] <= lastTimestamp
+{
+    preserved {
+        requireInvariant lockExpiryLELockMaximum();
+    }
+}
+
+// 7 - verified except for timeout in flow
+// The expectedFunds ghost variable is always equal to the expectedFundsHelper calculation.
+// This invariant is needed to prove solvency and included in the store hooks for available/designated balances.
+// The expectedFunds for a single account is calculated as:
+//    availableBalance + designatedBalance + ((incoming - outgoing) * (flowEnd - updated))
+invariant expectedFundsMirror(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId)
+        expectedFunds[controller][fundId][accountId] == expectedFundsHelper(controller, fundId, accountId)
+{
+    preserved {
+        requireInvariant lockExpiryLELockMaximum();
+        requireInvariant outgoingLEAvailable();
+        requireInvariant noOutflowBeforeLocked();
+        requireInvariant updatedLETimestampAndFlowEnd();
+    }
+}

remappings.txt

@@ -0,0 +1,4 @@
+@ensdomains/=node_modules/@ensdomains/
+@openzeppelin/=node_modules/@openzeppelin/
+hardhat-deploy/=node_modules/hardhat-deploy/
+hardhat/=node_modules/hardhat/