add more mutations

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