diff --git a/certora/mutations/035_withdraw_account_not_deleted.patch b/certora/mutations/035_withdraw_account_not_deleted.patch new file mode 100644 index 0000000..1b12854 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/036_burnAccount_not_deleted.patch b/certora/mutations/036_burnAccount_not_deleted.patch new file mode 100644 index 0000000..ac27759 --- /dev/null +++ b/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); + } + diff --git a/certora/mutations/037_burnDesignated_no_decrement.patch b/certora/mutations/037_burnDesignated_no_decrement.patch new file mode 100644 index 0000000..630b9e1 --- /dev/null +++ b/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); + }