From 2f458d90ce2cf710721196aa2e3b0671aa2d9fde Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Sun, 6 Apr 2025 00:39:55 +0100 Subject: [PATCH 01/27] try to hook on _funds. fixed required --- certora/confs/Vault.conf | 28 ++++++++++++++++++++++++++++ certora/specs/Vault.spec | 29 +++++++++++++++++++++++++++++ remappings.txt | 4 ++++ 3 files changed, 61 insertions(+) create mode 100644 certora/confs/Vault.conf create mode 100644 certora/specs/Vault.spec create mode 100644 remappings.txt diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf new file mode 100644 index 0000000..2847c5b --- /dev/null +++ b/certora/confs/Vault.conf @@ -0,0 +1,28 @@ +{ + "files": [ + "contracts/Vault.sol", + // "certora/harness/MarketplaceHarness.sol", + // "contracts/Marketplace.sol", + // "contracts/Vault.sol", + // "contracts/Groth16Verifier.sol", + "certora/helpers/ERC20A.sol", + ], + "parametric_contracts": ["Vault"], + "link" : [ + "Vault:_token=ERC20A", + // "MarketplaceHarness:_vault=Vault", + // "MarketplaceHarness:_verifier=Groth16Verifier" + ], + "packages": [ + "@openzeppelin/=node_modules/@openzeppelin/", + ], + "msg": "Verifying Vault", + "rule_sanity": "basic", + "verify": "Vault:certora/specs/Vault.spec", + // "optimistic_loop": true, + "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 new file mode 100644 index 0000000..04585e1 --- /dev/null +++ b/certora/specs/Vault.spec @@ -0,0 +1,29 @@ +methods { + +} + +rule sanity(env e, method f) { + calldataarg args; + f(e, args); + satisfy true; +} + +// ghost mapping(Vault.Controller => mapping(Vault.FundId => Vault.Timestamp)) ghostName; + // init_state axiom forall uint256 a. ghostName[a] == 0; + +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) ghostName { + init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. ghostName[controller][fundId] == 0; +} +// mapping(Controller => mapping(FundId => Fund)) private _funds; +hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId] { + require ghostName[Controller][FundId] == require_uint40(defaultValue); +} + + + + +// (∀ controller ∈ Controller, fundId ∈ FundId: +// fund.lockExpiry <= fund.lockMaximum +// where fund = _funds[controller][fundId]) +// STATUS - in progress +// invariant lockExpiryLELockMaximum() diff --git a/remappings.txt b/remappings.txt new file mode 100644 index 0000000..5796d3d --- /dev/null +++ b/remappings.txt @@ -0,0 +1,4 @@ +@ensdomains/=node_modules/@ensdomains/ +@openzeppelin/=node_modules/@openzeppelin/ +hardhat-deploy/=node_modules/hardhat-deploy/ +hardhat/=node_modules/hardhat/ From 6aed0bb07aa3398a3b5a8b1791f8c732a451f97d Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 9 Apr 2025 00:29:56 +0100 Subject: [PATCH 02/27] attempt to use sum ghost --- certora/confs/Vault.conf | 4 +- certora/specs/Vault.spec | 187 +++++++++++++++++++++++++++++++++++++-- 2 files changed, 180 insertions(+), 11 deletions(-) diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index 2847c5b..c1aedc0 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -14,7 +14,7 @@ // "MarketplaceHarness:_verifier=Groth16Verifier" ], "packages": [ - "@openzeppelin/=node_modules/@openzeppelin/", + "@openzeppelin/=node_modules/@openzeppelin", ], "msg": "Verifying Vault", "rule_sanity": "basic", @@ -23,6 +23,6 @@ "loop_iter": "3", // "optimistic_hashing": true, // "hashing_length_bound": "512", - + "build_cache": true, "solc": "solc8.28", } diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 04585e1..cc49017 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -8,22 +8,191 @@ rule sanity(env e, method f) { satisfy true; } -// ghost mapping(Vault.Controller => mapping(Vault.FundId => Vault.Timestamp)) ghostName; - // init_state axiom forall uint256 a. ghostName[a] == 0; -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) ghostName { - init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. ghostName[controller][fundId] == 0; +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) lockExpiryMirror { + init_state axiom + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + lockExpiryMirror[controller][fundId] == 0; } -// mapping(Controller => mapping(FundId => Fund)) private _funds; -hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId] { - require ghostName[Controller][FundId] == require_uint40(defaultValue); + +hook Sload VaultBase.Timestamp defaultValue + _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry +{ + require lockExpiryMirror[Controller][FundId] == defaultValue; +} + +hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry + VaultBase.Timestamp defaultValue +{ + lockExpiryMirror[Controller][FundId] = defaultValue; } +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) 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] == defaultValue; +} + +hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum + VaultBase.Timestamp defaultValue +{ + lockMaximumMirror[Controller][FundId] = defaultValue; +} // (∀ controller ∈ Controller, fundId ∈ FundId: // fund.lockExpiry <= fund.lockMaximum // where fund = _funds[controller][fundId]) -// STATUS - in progress -// invariant lockExpiryLELockMaximum() +// STATUS - verified +invariant lockExpiryLELockMaximum() + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + lockExpiryMirror[controller][fundId] <= lockMaximumMirror[controller][fundId]; + + + + + + + +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; +} + +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; +} + +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; +} + + + + +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.Timestamp))) 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] == defaultValue; +} + +hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].flow.updated + VaultBase.Timestamp defaultValue +{ + updatedMirror[Controller][FundId][AccountId] = defaultValue; +} + + + +// now for balance = _accounts[controller][fundId][accountId].balance +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint128))) balanceMirror { + init_state axiom + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId accountId. + balanceMirror[controller][fundId][accountId] == 0; +} + +hook Sload uint128 defaultValue + _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.available +{ + require balanceMirror[Controller][FundId][AccountId] == defaultValue; +} + +hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.available + uint128 defaultValue +{ + balanceMirror[Controller][FundId][AccountId] = defaultValue; +} + + + + +// (∀ 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])) +// <= balanceMirror[controller][fundId][accountId]; + +invariant outgoingLEAvailableEasy(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) + // forall VaultBase.Controller controller. + // forall VaultBase.FundId fundId. + // forall VaultBase.AccountId accountId. + (outgoingMirror[controller][fundId][accountId] + * (lockMaximumMirror[controller][fundId] + - updatedMirror[controller][fundId][accountId])) + <= balanceMirror[controller][fundId][accountId]; + + + + + +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; +} + +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; +} + +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; +} + + +// (∀ controller ∈ Controller, fundId ∈ FundId: +// (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = +// (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) +// where accounts = _accounts[controller][fundId]) +invariant incomingEqualsOutgoing() + (sum + VaultBase.Controller controller. + VaultBase.FundId fundId. + VaultBase.AccountId accountId. + outgoingMirror[controller][fundId][accountId]) + == (sum + VaultBase.Controller controller. + VaultBase.FundId fundId. + VaultBase.AccountId accountId. + incomingMirror[controller][fundId][accountId]); \ No newline at end of file From 980ca1676683f1c49c70e9bb3fbda65e1118332e Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 16 Apr 2025 23:09:30 +0100 Subject: [PATCH 03/27] adding CVLStatus to use in quantifiers --- certora/confs/Vault.conf | 11 ++-- certora/harness/VaultHarness.sol | 16 ++++++ certora/specs/Vault.spec | 99 +++++++++++++++++++++++++++----- 3 files changed, 106 insertions(+), 20 deletions(-) create mode 100644 certora/harness/VaultHarness.sol diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index c1aedc0..2c73a9a 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -1,16 +1,17 @@ { "files": [ - "contracts/Vault.sol", + "certora/harness/VaultHarness.sol", + //"contracts/Vault.sol", // "certora/harness/MarketplaceHarness.sol", // "contracts/Marketplace.sol", // "contracts/Vault.sol", // "contracts/Groth16Verifier.sol", "certora/helpers/ERC20A.sol", ], - "parametric_contracts": ["Vault"], + "parametric_contracts": ["VaultHarness"], "link" : [ - "Vault:_token=ERC20A", - // "MarketplaceHarness:_vault=Vault", + "VaultHarness:_token=ERC20A", + // "MarketplaceHarness:_vault=VaultHarness", // "MarketplaceHarness:_verifier=Groth16Verifier" ], "packages": [ @@ -18,7 +19,7 @@ ], "msg": "Verifying Vault", "rule_sanity": "basic", - "verify": "Vault:certora/specs/Vault.spec", + "verify": "VaultHarness:certora/specs/Vault.spec", // "optimistic_loop": true, "loop_iter": "3", // "optimistic_hashing": true, diff --git a/certora/harness/VaultHarness.sol b/certora/harness/VaultHarness.sol new file mode 100644 index 0000000..0756bac --- /dev/null +++ b/certora/harness/VaultHarness.sol @@ -0,0 +1,16 @@ +// 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); + } + +} diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index cc49017..227c879 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -49,6 +49,27 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun } +// frozenAtghost mirror +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) 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] == defaultValue; +} + +hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt + VaultBase.Timestamp defaultValue +{ + frozenAtMirror[Controller][FundId] = defaultValue; +} + + // (∀ controller ∈ Controller, fundId ∈ FundId: // fund.lockExpiry <= fund.lockMaximum // where fund = _funds[controller][fundId]) @@ -66,10 +87,13 @@ invariant lockExpiryLELockMaximum() ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) outgoingMirror { init_state axiom - forall VaultBase.Controller controller. + (forall VaultBase.Controller controller. forall VaultBase.FundId fundId. forall VaultBase.AccountId accountId. - outgoingMirror[controller][fundId][accountId] == 0; + 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 @@ -162,10 +186,13 @@ invariant outgoingLEAvailableEasy(VaultBase.Controller controller, VaultBase.Fun ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) incomingMirror { init_state axiom - forall VaultBase.Controller controller. + (forall VaultBase.Controller controller. forall VaultBase.FundId fundId. forall VaultBase.AccountId accountId. - incomingMirror[controller][fundId][accountId] == 0; + 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 @@ -185,14 +212,56 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = // (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) // where accounts = _accounts[controller][fundId]) -invariant incomingEqualsOutgoing() - (sum - VaultBase.Controller controller. - VaultBase.FundId fundId. - VaultBase.AccountId accountId. - outgoingMirror[controller][fundId][accountId]) - == (sum - VaultBase.Controller controller. - VaultBase.FundId fundId. - VaultBase.AccountId accountId. - incomingMirror[controller][fundId][accountId]); \ No newline at end of file +invariant incomingEqualsOutgoing(env e) + (forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + statusCVL(e, controller, fundId) == VaultBase.FundStatus.Withdrawing + => (sum + VaultBase.AccountId accountId. + outgoingMirror[controller][fundId][accountId]) + == (sum + VaultBase.AccountId accountId. + incomingMirror[controller][fundId][accountId])) + { + preserved with (env e2) { + require e.block.timestamp == e2.block.timestamp; + } + } + + +// copying status implementation from Funds.sol using CVL to use it in quantifier +/* +if (Timestamps.currentTime() < fund.lockExpiry) { + if (fund.frozenAt != Timestamp.wrap(0)) { + return FundStatus.Frozen; + } + return FundStatus.Locked; + } + if (fund.lockMaximum == Timestamp.wrap(0)) { + return FundStatus.Inactive; + } + return FundStatus.Withdrawing; +*/ + +ghost VaultBase.Timestamp zeroValue { + init_state axiom zeroValue == 0; + axiom zeroValue == 0; +} + +function statusCVL(env e, VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus { + if (e.block.timestamp < lockExpiryMirror[controller][fundId]) { + if (frozenAtMirror != zeroValue) { + return VaultBase.FundStatus.Frozen; + } + return VaultBase.FundStatus.Locked; + } + if (lockMaximumMirror[controller][fundId] == 0) { + return VaultBase.FundStatus.Inactive; + } + return VaultBase.FundStatus.Withdrawing; +} + + + + + From 2a46f53a0cd6a1191468316d0116696b5f4dfd4b Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 16 Apr 2025 23:21:47 +0100 Subject: [PATCH 04/27] started implementing solvency --- certora/specs/Vault.spec | 111 +++++++++++++++++++++++++++------------ 1 file changed, 77 insertions(+), 34 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 227c879..a483f24 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -133,28 +133,51 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId -// now for balance = _accounts[controller][fundId][accountId].balance -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint128))) balanceMirror { +// now for balance = _accounts[controller][fundId][accountId].balance.available +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. - balanceMirror[controller][fundId][accountId] == 0; + 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 balanceMirror[Controller][FundId][AccountId] == defaultValue; + require availableBalanceMirror[Controller][FundId][AccountId] == defaultValue; } hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.available uint128 defaultValue { - balanceMirror[Controller][FundId][AccountId] = defaultValue; + availableBalanceMirror[Controller][FundId][AccountId] = defaultValue; } +// now for balance = _accounts[controller][fundId][accountId].balance.designated +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; +} + +hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.designated + uint128 defaultValue +{ + designatedBalanceMirror[Controller][FundId][AccountId] = defaultValue; +} + + + // (∀ controller ∈ Controller, fundId ∈ FundId, accountId ∈ AccountId: @@ -169,7 +192,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // (outgoingMirror[controller][fundId][accountId] // * (lockMaximumMirror[controller][fundId] // - updatedMirror[controller][fundId][accountId])) -// <= balanceMirror[controller][fundId][accountId]; +// <= availableBalanceMirror[controller][fundId][accountId]; invariant outgoingLEAvailableEasy(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) // forall VaultBase.Controller controller. @@ -178,7 +201,7 @@ invariant outgoingLEAvailableEasy(VaultBase.Controller controller, VaultBase.Fun (outgoingMirror[controller][fundId][accountId] * (lockMaximumMirror[controller][fundId] - updatedMirror[controller][fundId][accountId])) - <= balanceMirror[controller][fundId][accountId]; + <= availableBalanceMirror[controller][fundId][accountId]; @@ -212,21 +235,21 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = // (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) // where accounts = _accounts[controller][fundId]) -invariant incomingEqualsOutgoing(env e) - (forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - statusCVL(e, controller, fundId) == VaultBase.FundStatus.Withdrawing - => (sum - VaultBase.AccountId accountId. - outgoingMirror[controller][fundId][accountId]) - == (sum - VaultBase.AccountId accountId. - incomingMirror[controller][fundId][accountId])) - { - preserved with (env e2) { - require e.block.timestamp == e2.block.timestamp; - } - } +// invariant incomingEqualsOutgoing(env e) +// (forall VaultBase.Controller controller. +// forall VaultBase.FundId fundId. +// statusCVL(e, controller, fundId) == VaultBase.FundStatus.Withdrawing +// => (sum +// VaultBase.AccountId accountId. +// outgoingMirror[controller][fundId][accountId]) +// == (sum +// VaultBase.AccountId accountId. +// incomingMirror[controller][fundId][accountId])) +// { +// preserved with (env e2) { +// require e.block.timestamp == e2.block.timestamp; +// } +// } // copying status implementation from Funds.sol using CVL to use it in quantifier @@ -248,18 +271,38 @@ ghost VaultBase.Timestamp zeroValue { axiom zeroValue == 0; } -function statusCVL(env e, VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus { - if (e.block.timestamp < lockExpiryMirror[controller][fundId]) { - if (frozenAtMirror != zeroValue) { - return VaultBase.FundStatus.Frozen; - } - return VaultBase.FundStatus.Locked; - } - if (lockMaximumMirror[controller][fundId] == 0) { - return VaultBase.FundStatus.Inactive; - } - return VaultBase.FundStatus.Withdrawing; -} +// function statusCVL(env e, VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus { +// if (e.block.timestamp < lockExpiryMirror[controller][fundId]) { +// if (frozenAtMirror != zeroValue) { +// return VaultBase.FundStatus.Frozen; +// } +// return VaultBase.FundStatus.Locked; +// } +// if (lockMaximumMirror[controller][fundId] == 0) { +// return VaultBase.FundStatus.Inactive; +// } +// return VaultBase.FundStatus.Withdrawing; +// } + + + + + + + +// account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == fund.value +invariant solvency() + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId accountId. + availableBalanceMirror[controller][fundId][accountId] + + designatedBalanceMirror[controller][fundId][accountId] + + ((incomingMirror[controller][fundId][accountId] + - outgoingMirror[controller][fundId][accountId]) + * (lockMaximumMirror[controller][fundId] + - updatedMirror[controller][fundId][accountId])) + == _funds[controller][fundId].value; + From 3b5bd3d4fc61b76a10f60810077feda77c512413 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Tue, 29 Apr 2025 11:57:37 +0100 Subject: [PATCH 05/27] bug finding invariants --- certora/harness/VaultHarness.sol | 7 ++ certora/specs/Vault.spec | 141 +++++++++++++++++-------------- 2 files changed, 84 insertions(+), 64 deletions(-) diff --git a/certora/harness/VaultHarness.sol b/certora/harness/VaultHarness.sol index 0756bac..66bb0d2 100644 --- a/certora/harness/VaultHarness.sol +++ b/certora/harness/VaultHarness.sol @@ -13,4 +13,11 @@ contract VaultHarness is Vault { return _getFundStatus(controller, fundId); } + function unwrapTimestamp( + Timestamp timestamp + ) public pure returns (uint40) { + return Timestamp.unwrap(timestamp); + } + + } diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index a483f24..4e2be76 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -1,15 +1,15 @@ methods { - + function unwrapTimestamp(VaultBase.Timestamp) external returns (uint40) envfree; } -rule sanity(env e, method f) { - calldataarg args; - f(e, args); - satisfy true; -} +// rule sanity(env e, method f) { +// calldataarg args; +// f(e, args); +// satisfy true; +// } -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) lockExpiryMirror { +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror { init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. @@ -19,17 +19,17 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Time hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry { - require lockExpiryMirror[Controller][FundId] == defaultValue; + require lockExpiryMirror[Controller][FundId] == unwrapTimestamp(defaultValue); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry VaultBase.Timestamp defaultValue { - lockExpiryMirror[Controller][FundId] = defaultValue; + lockExpiryMirror[Controller][FundId] = unwrapTimestamp(defaultValue); } -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) lockMaximumMirror { +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockMaximumMirror { init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. @@ -39,18 +39,18 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Time hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum { - require lockMaximumMirror[Controller][FundId] == defaultValue; + require lockMaximumMirror[Controller][FundId] == unwrapTimestamp(defaultValue); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum VaultBase.Timestamp defaultValue { - lockMaximumMirror[Controller][FundId] = defaultValue; + lockMaximumMirror[Controller][FundId] = unwrapTimestamp(defaultValue); } // frozenAtghost mirror -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Timestamp)) frozenAtMirror { +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) frozenAtMirror { init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. @@ -60,13 +60,13 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => VaultBase.Time hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt { - require frozenAtMirror[Controller][FundId] == defaultValue; + require frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt VaultBase.Timestamp defaultValue { - frozenAtMirror[Controller][FundId] = defaultValue; + frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); } @@ -111,7 +111,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.Timestamp))) updatedMirror { +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint40))) updatedMirror { init_state axiom forall VaultBase.Controller controller. forall VaultBase.FundId fundId. @@ -122,13 +122,13 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultB 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] == defaultValue; + require updatedMirror[Controller][FundId][AccountId] == unwrapTimestamp(defaultValue); } hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].flow.updated VaultBase.Timestamp defaultValue { - updatedMirror[Controller][FundId][AccountId] = defaultValue; + updatedMirror[Controller][FundId][AccountId] = unwrapTimestamp(defaultValue); } @@ -194,16 +194,20 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // - updatedMirror[controller][fundId][accountId])) // <= availableBalanceMirror[controller][fundId][accountId]; -invariant outgoingLEAvailableEasy(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) - // forall VaultBase.Controller controller. - // forall VaultBase.FundId fundId. - // forall VaultBase.AccountId accountId. +invariant outgoingLEAvailableEasy() + 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]; - +invariant outgoingLEAvailableEasySingle(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) + (outgoingMirror[controller][fundId][accountId] + * (lockMaximumMirror[controller][fundId] + - updatedMirror[controller][fundId][accountId])) + <= availableBalanceMirror[controller][fundId][accountId]; @@ -235,21 +239,21 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = // (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) // where accounts = _accounts[controller][fundId]) -// invariant incomingEqualsOutgoing(env e) -// (forall VaultBase.Controller controller. -// forall VaultBase.FundId fundId. -// statusCVL(e, controller, fundId) == VaultBase.FundStatus.Withdrawing -// => (sum -// VaultBase.AccountId accountId. -// outgoingMirror[controller][fundId][accountId]) -// == (sum -// VaultBase.AccountId accountId. -// incomingMirror[controller][fundId][accountId])) -// { -// preserved with (env e2) { -// require e.block.timestamp == e2.block.timestamp; -// } -// } +invariant incomingEqualsOutgoing(env e) + (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])) + { + preserved with (env e2) { + require e.block.timestamp == e2.block.timestamp; + } + } // copying status implementation from Funds.sol using CVL to use it in quantifier @@ -266,23 +270,32 @@ if (Timestamps.currentTime() < fund.lockExpiry) { return FundStatus.Withdrawing; */ -ghost VaultBase.Timestamp zeroValue { - init_state axiom zeroValue == 0; - axiom zeroValue == 0; +ghost mathint ghostLastTimestamp; +hook TIMESTAMP uint256 time { + require to_mathint(time) < max_uint40; // Timestamp type is uint40 that's why we have this require. uint40 is used in the whole contract + require to_mathint(time) >= ghostLastTimestamp; + ghostLastTimestamp = time; } -// function statusCVL(env e, VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus { -// if (e.block.timestamp < lockExpiryMirror[controller][fundId]) { -// if (frozenAtMirror != zeroValue) { -// return VaultBase.FundStatus.Frozen; -// } -// return VaultBase.FundStatus.Locked; -// } -// if (lockMaximumMirror[controller][fundId] == 0) { -// return VaultBase.FundStatus.Inactive; -// } -// return VaultBase.FundStatus.Withdrawing; -// } + + +definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus = + ghostLastTimestamp < lockExpiryMirror[controller][fundId] ? + (frozenAtMirror[controller][fundId] != 0 ? VaultBase.FundStatus.Frozen : VaultBase.FundStatus.Locked) : + (lockMaximumMirror[controller][fundId] == 0 ? VaultBase.FundStatus.Inactive : VaultBase.FundStatus.Withdrawing); + + // if (ghostLastTimestamp < lockExpiryMirror[controller][fundId]) { + // if (frozenAtMirror[controller][fundId] != 0) { + // return VaultBase.FundStatus.Frozen; + // } + // return VaultBase.FundStatus.Locked; + // } + + // if (lockMaximumMirror[controller][fundId] == 0) { + // return VaultBase.FundStatus.Inactive; + // } + // return VaultBase.FundStatus.Withdrawing; + @@ -291,17 +304,17 @@ ghost VaultBase.Timestamp zeroValue { // account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == fund.value -invariant solvency() - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - forall VaultBase.AccountId accountId. - availableBalanceMirror[controller][fundId][accountId] - + designatedBalanceMirror[controller][fundId][accountId] - + ((incomingMirror[controller][fundId][accountId] - - outgoingMirror[controller][fundId][accountId]) - * (lockMaximumMirror[controller][fundId] - - updatedMirror[controller][fundId][accountId])) - == _funds[controller][fundId].value; +// invariant solvency() +// forall VaultBase.Controller controller. +// forall VaultBase.FundId fundId. +// forall VaultBase.AccountId accountId. +// availableBalanceMirror[controller][fundId][accountId] +// + designatedBalanceMirror[controller][fundId][accountId] +// + ((incomingMirror[controller][fundId][accountId] +// - outgoingMirror[controller][fundId][accountId]) +// * (lockMaximumMirror[controller][fundId] +// - updatedMirror[controller][fundId][accountId])) +// == _funds[controller][fundId].value; From 17ebb6909da3ab85fb435cfaba0c3a4a6cb90e68 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 30 May 2025 00:32:25 +0100 Subject: [PATCH 06/27] 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; - - - - - - From 965ae4df1effa9b64b2b2b0fc6d6672dca64969e Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Mon, 2 Jun 2025 10:31:23 +0100 Subject: [PATCH 07/27] spec cleaning --- certora/specs/Vault.spec | 277 +++++++++++++++++---------------------- 1 file changed, 123 insertions(+), 154 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index cb69299..03707ea 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -37,6 +37,10 @@ invariant totalSupplyIsSumOfBalances() + + + +// new ghosts needed in 1 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror { init_state axiom forall VaultBase.Controller controller. @@ -57,6 +61,7 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun } + ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockMaximumMirror { init_state axiom forall VaultBase.Controller controller. @@ -76,43 +81,24 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun lockMaximumMirror[Controller][FundId] = unwrapTimestamp(defaultValue); } - -// frozenAtghost mirror -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); -} - -hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt - VaultBase.Timestamp defaultValue -{ - frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); -} - - +// 1 - verified // (∀ controller ∈ Controller, fundId ∈ FundId: // fund.lockExpiry <= fund.lockMaximum // where fund = _funds[controller][fundId]) -// STATUS - verified invariant lockExpiryLELockMaximum() forall VaultBase.Controller controller. forall VaultBase.FundId fundId. lockExpiryMirror[controller][fundId] <= lockMaximumMirror[controller][fundId]; +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// - - +// new ghosts needed in 2 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) outgoingMirror { init_state axiom (forall VaultBase.Controller controller. @@ -138,7 +124,6 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId - ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint40))) updatedMirror { init_state axiom forall VaultBase.Controller controller. @@ -161,7 +146,6 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId -// now for balance = _accounts[controller][fundId][accountId].balance.available ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => uint128))) availableBalanceMirror { init_state axiom forall VaultBase.Controller controller. @@ -183,46 +167,14 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId } -// now for balance = _accounts[controller][fundId][accountId].balance.designated -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; -} - -hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.designated - uint128 defaultValue -{ - designatedBalanceMirror[Controller][FundId][AccountId] = defaultValue; -} - - - - +// 2 // (∀ 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]; - -invariant outgoingLEAvailableEasy() +invariant outgoingLEAvailable() forall VaultBase.Controller controller. forall VaultBase.FundId fundId. forall VaultBase.AccountId accountId. @@ -230,61 +182,16 @@ invariant outgoingLEAvailableEasy() * (lockMaximumMirror[controller][fundId] - updatedMirror[controller][fundId][accountId])) <= availableBalanceMirror[controller][fundId][accountId]; - -invariant outgoingLEAvailableEasySingle(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) - (outgoingMirror[controller][fundId][accountId] - * (lockMaximumMirror[controller][fundId] - - updatedMirror[controller][fundId][accountId])) - <= availableBalanceMirror[controller][fundId][accountId]; - - - -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() - - - - - +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// +// new ghosts needed in 3 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultBase.AccountId => VaultBase.TokensPerSecond))) incomingMirror { init_state axiom (forall VaultBase.Controller controller. @@ -310,43 +217,29 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) frozenAtMirror { + init_state axiom + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + frozenAtMirror[controller][fundId] == 0; +} -// (∀ controller ∈ Controller, fundId ∈ FundId: -// (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = -// (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) -// where accounts = _accounts[controller][fundId]) -invariant incomingEqualsOutgoing(env e) - (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])) - { - preserved with (env e2) { - require e.block.timestamp == e2.block.timestamp; - } - } +hook Sload VaultBase.Timestamp defaultValue + _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt +{ + require frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue); +} + +hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt + VaultBase.Timestamp defaultValue +{ + frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); +} -// copying status implementation from Funds.sol using CVL to use it in quantifier -/* -if (Timestamps.currentTime() < fund.lockExpiry) { - if (fund.frozenAt != Timestamp.wrap(0)) { - return FundStatus.Frozen; - } - return FundStatus.Locked; - } - if (fund.lockMaximum == Timestamp.wrap(0)) { - return FundStatus.Inactive; - } - return FundStatus.Withdrawing; -*/ ghost mathint ghostLastTimestamp; + hook TIMESTAMP uint256 time { require to_mathint(time) < max_uint40; // Timestamp type is uint40 that's why we have this require. uint40 is used in the whole contract require to_mathint(time) >= ghostLastTimestamp; @@ -360,25 +253,55 @@ definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) r (frozenAtMirror[controller][fundId] != 0 ? VaultBase.FundStatus.Frozen : VaultBase.FundStatus.Locked) : (lockMaximumMirror[controller][fundId] == 0 ? VaultBase.FundStatus.Inactive : VaultBase.FundStatus.Withdrawing); - // if (ghostLastTimestamp < lockExpiryMirror[controller][fundId]) { - // if (frozenAtMirror[controller][fundId] != 0) { - // return VaultBase.FundStatus.Frozen; - // } - // return VaultBase.FundStatus.Locked; - // } - - // if (lockMaximumMirror[controller][fundId] == 0) { - // return VaultBase.FundStatus.Inactive; - // } - // return VaultBase.FundStatus.Withdrawing; +// 3 - verified +// (∀ controller ∈ Controller, fundId ∈ FundId: +// (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = +// (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) +// where accounts = _accounts[controller][fundId]) +invariant incomingEqualsOutgoing(env e) + (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])); +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// + +// new ghosts needed in 4 +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; +} + +hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId][KEY VaultBase.AccountId AccountId].balance.designated + uint128 defaultValue +{ + designatedBalanceMirror[Controller][FundId][AccountId] = defaultValue; +} +// invariant 4 (Certora's solvency) // account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == fund.value // invariant solvency() // forall VaultBase.Controller controller. @@ -391,3 +314,49 @@ definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) r // * (lockMaximumMirror[controller][fundId] // - updatedMirror[controller][fundId][accountId])) // == _funds[controller][fundId].value; +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// +//------------------------------------------------------------// + + + + + +// 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 supporter() + forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId accountId. + lockMaximumMirror[controller][fundId] == 0 => outgoingMirror[controller][fundId][accountId] == 0; + From 3350ab70dc4ac92c261a6a4bb86da71115aa3b57 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Mon, 2 Jun 2025 16:42:31 +0100 Subject: [PATCH 08/27] finished Codex's invariants and more spec cleaning --- certora/specs/Vault.spec | 45 ++++++++++------------------------------ 1 file changed, 11 insertions(+), 34 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 03707ea..307345f 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -168,7 +168,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId -// 2 +// 2 - verified // (∀ controller ∈ Controller, fundId ∈ FundId, accountId ∈ AccountId: // flow.outgoing * (fund.lockMaximum - flow.updated) <= balance.available // where fund = _funds[controller][fundId]) @@ -181,7 +181,12 @@ invariant outgoingLEAvailable() (outgoingMirror[controller][fundId][accountId] * (lockMaximumMirror[controller][fundId] - updatedMirror[controller][fundId][accountId])) - <= availableBalanceMirror[controller][fundId][accountId]; + <= availableBalanceMirror[controller][fundId][accountId] + { + preserved { + requireInvariant supporter(); + } + } //------------------------------------------------------------// //------------------------------------------------------------// //------------------------------------------------------------// @@ -243,6 +248,7 @@ ghost mathint ghostLastTimestamp; hook TIMESTAMP uint256 time { require to_mathint(time) < max_uint40; // Timestamp type is uint40 that's why we have this require. uint40 is used in the whole contract require to_mathint(time) >= ghostLastTimestamp; + require ghostLastTimestamp > 0; // this require is necessary to avoid violation in "supporter" invariant. It happens only when timestamp == 0 and it's safe to require it because it's not 0 in real life. ghostLastTimestamp = time; } @@ -301,7 +307,8 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId } -// invariant 4 (Certora's solvency) + +// invariant 4 (Certora's solvency) - // account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == fund.value // invariant solvency() // forall VaultBase.Controller controller. @@ -323,37 +330,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId -// 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; -// } - - - - - -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// - - - - +// 5 (needed to prove 2) - verified invariant supporter() forall VaultBase.Controller controller. forall VaultBase.FundId fundId. From a217a0476d60371e19aae8182b714c21bd8d8ada Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Thu, 12 Jun 2025 15:09:33 +0100 Subject: [PATCH 09/27] hook check in --- certora/specs/Vault.spec | 291 ++++++++++++++++++++++++++++----------- 1 file changed, 208 insertions(+), 83 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 307345f..c9450d9 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -16,16 +16,22 @@ methods { +ghost mapping(address => uint256) tokenBalanceOfMirror { + init_state axiom forall address a. tokenBalanceOfMirror[a] == 0; +} + ghost mathint sumOfBalances { init_state axiom sumOfBalances == 0; } hook Sload uint256 balance Token._balances[KEY address addr] { require sumOfBalances >= to_mathint(balance); + require tokenBalanceOfMirror[addr] == balance; } hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances - oldValue + newValue; + tokenBalanceOfMirror[addr] = newValue; } invariant totalSupplyIsSumOfBalances() @@ -43,9 +49,9 @@ invariant totalSupplyIsSumOfBalances() // new ghosts needed in 1 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror { init_state axiom - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - lockExpiryMirror[controller][fundId] == 0; + forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + lockExpiryMirror[Controller][FundId] == 0; } hook Sload VaultBase.Timestamp defaultValue @@ -64,31 +70,62 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockMaximumMirror { init_state axiom - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - lockMaximumMirror[controller][fundId] == 0; + 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); + require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum VaultBase.Timestamp defaultValue { lockMaximumMirror[Controller][FundId] = unwrapTimestamp(defaultValue); + // require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + // + designatedBalanceMirror[Controller][FundId][AccountId] + // + ((incomingMirror[Controller][FundId][AccountId] + // - outgoingMirror[Controller][FundId][AccountId]) + // * (lockMaximumMirror[Controller][FundId] + // - updatedMirror[Controller][FundId][AccountId])); + mathint oldSum = usum VaultBase.Controller controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]; + + havoc expectedFunds assuming forall + VaultBase.AccountId AccountId. + expectedFunds[Controller][FundId][AccountId] + == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); + + require (usum VaultBase.Controller controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]) == oldSum; } // 1 - verified -// (∀ controller ∈ Controller, fundId ∈ FundId: +// (∀ Controller ∈ Controller, FundId ∈ FundId: // fund.lockExpiry <= fund.lockMaximum -// where fund = _funds[controller][fundId]) +// where fund = _funds[Controller][FundId]) invariant lockExpiryLELockMaximum() - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - lockExpiryMirror[controller][fundId] <= lockMaximumMirror[controller][fundId]; + forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + lockExpiryMirror[Controller][FundId] <= lockMaximumMirror[Controller][FundId]; //------------------------------------------------------------// //------------------------------------------------------------// //------------------------------------------------------------// @@ -101,87 +138,123 @@ invariant lockExpiryLELockMaximum() // new ghosts needed in 2 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); + (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; + require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - defaultValue) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } 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] = availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - defaultValue) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } 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; + 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); + require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - unwrapTimestamp(defaultValue))); } 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] = availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - unwrapTimestamp(defaultValue))); } 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; + 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; + require expectedFunds[Controller][FundId][AccountId] == defaultValue + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[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] = defaultValue + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } // 2 - verified -// (∀ controller ∈ Controller, fundId ∈ FundId, accountId ∈ AccountId: +// (∀ 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 +// 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] + 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 supporter(); @@ -199,34 +272,46 @@ invariant outgoingLEAvailable() // new ghosts needed in 3 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); + (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; + require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((defaultValue + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } 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] = availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((defaultValue + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) frozenAtMirror { init_state axiom - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - frozenAtMirror[controller][fundId] == 0; + forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + frozenAtMirror[Controller][FundId] == 0; } hook Sload VaultBase.Timestamp defaultValue @@ -254,28 +339,28 @@ hook TIMESTAMP uint256 time { -definition statusCVL(VaultBase.Controller controller, VaultBase.FundId fundId) returns VaultBase.FundStatus = - ghostLastTimestamp < lockExpiryMirror[controller][fundId] ? - (frozenAtMirror[controller][fundId] != 0 ? VaultBase.FundStatus.Frozen : VaultBase.FundStatus.Locked) : - (lockMaximumMirror[controller][fundId] == 0 ? VaultBase.FundStatus.Inactive : VaultBase.FundStatus.Withdrawing); +definition statusCVL(VaultBase.Controller Controller, VaultBase.FundId FundId) returns VaultBase.FundStatus = + ghostLastTimestamp < 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 -// (∀ controller ∈ Controller, fundId ∈ FundId: -// (∑ accountId ∈ AccountId: accounts[accountId].flow.incoming) = -// (∑ accountId ∈ AccountId: accounts[accountId].flow.outgoing) -// where accounts = _accounts[controller][fundId]) -invariant incomingEqualsOutgoing(env e) - (forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - statusCVL(controller, fundId) != VaultBase.FundStatus.Withdrawing +// (∀ 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]) + VaultBase.AccountId AccountId. + outgoingMirror[Controller][FundId][AccountId]) == (sum - VaultBase.AccountId accountId. - incomingMirror[controller][fundId][accountId])); + VaultBase.AccountId AccountId. + incomingMirror[Controller][FundId][AccountId])); //------------------------------------------------------------// //------------------------------------------------------------// //------------------------------------------------------------// @@ -288,39 +373,77 @@ invariant incomingEqualsOutgoing(env e) // new ghosts needed in 4 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; + 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; + require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + defaultValue + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[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] = availableBalanceMirror[Controller][FundId][AccountId] + + defaultValue + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (lockMaximumMirror[Controller][FundId] + - updatedMirror[Controller][FundId][AccountId])); } +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; +} + + + // invariant 4 (Certora's solvency) - -// account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == fund.value -// invariant solvency() -// forall VaultBase.Controller controller. -// forall VaultBase.FundId fundId. -// forall VaultBase.AccountId accountId. -// availableBalanceMirror[controller][fundId][accountId] -// + designatedBalanceMirror[controller][fundId][accountId] -// + ((incomingMirror[controller][fundId][accountId] -// - outgoingMirror[controller][fundId][accountId]) -// * (lockMaximumMirror[controller][fundId] -// - updatedMirror[controller][fundId][accountId])) -// == _funds[controller][fundId].value; +// account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == _token.balanceOf(currentContract) +invariant solvency() + (usum VaultBase.Controller Controller, + VaultBase.FundId FundId, + VaultBase.AccountId AccountId. + expectedFunds[Controller][FundId][AccountId]) == to_mathint(tokenBalanceOfMirror[currentContract]) + // forall VaultBase.Controller Controller. + // forall VaultBase.FundId FundId. + // forall VaultBase.AccountId AccountId. + // availableBalanceMirror[Controller][FundId][AccountId] + // + designatedBalanceMirror[Controller][FundId][AccountId] + // + ((incomingMirror[Controller][FundId][AccountId] + // - outgoingMirror[Controller][FundId][AccountId]) + // * (lockMaximumMirror[Controller][FundId] + // - updatedMirror[Controller][FundId][AccountId])) + // == tokenBalanceOfMirror[currentContract] + { + preserved { + requireInvariant lockExpiryLELockMaximum(); + requireInvariant outgoingLEAvailable(); + requireInvariant incomingEqualsOutgoing(); + requireInvariant supporter(); + } + } //------------------------------------------------------------// //------------------------------------------------------------// //------------------------------------------------------------// @@ -332,8 +455,10 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId // 5 (needed to prove 2) - verified invariant supporter() - forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - forall VaultBase.AccountId accountId. - lockMaximumMirror[controller][fundId] == 0 => outgoingMirror[controller][fundId][accountId] == 0; + forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + forall VaultBase.AccountId AccountId. + lockMaximumMirror[Controller][FundId] == 0 => outgoingMirror[Controller][FundId][AccountId] == 0; + + From 7ca5c8eb777cc22a767fa01dd418e5bf80198a09 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 13 Jun 2025 15:50:05 +0100 Subject: [PATCH 10/27] updated solvency for review --- certora/specs/Vault.spec | 59 +++++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 22 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index c9450d9..c5a35a3 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -83,7 +83,7 @@ hook Sload VaultBase.Timestamp defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -102,15 +102,16 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun VaultBase.AccountId AccountId. expectedFunds[controller][fundId][AccountId]; - havoc expectedFunds assuming forall - VaultBase.AccountId AccountId. - expectedFunds[Controller][FundId][AccountId] - == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] - - updatedMirror[Controller][FundId][AccountId])); + havoc expectedFunds assuming forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId AccountId. + expectedFunds@new[controller][fundId][AccountId] + == availableBalanceMirror[controller][fundId][AccountId] + + designatedBalanceMirror[controller][fundId][AccountId] + + ((incomingMirror[controller][fundId][AccountId] + - outgoingMirror[controller][fundId][AccountId]) + * (flowEndGhost[Controller][FundId] + - updatedMirror[controller][fundId][AccountId])); require (usum VaultBase.Controller controller, VaultBase.FundId fundId, @@ -155,7 +156,7 @@ hook Sload VaultBase.TokensPerSecond defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - defaultValue) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -167,7 +168,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - defaultValue) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -189,7 +190,7 @@ hook Sload VaultBase.Timestamp defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - unwrapTimestamp(defaultValue))); } @@ -201,7 +202,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - unwrapTimestamp(defaultValue))); } @@ -223,7 +224,7 @@ hook Sload uint128 defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -235,7 +236,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -289,7 +290,7 @@ hook Sload VaultBase.TokensPerSecond defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((defaultValue - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -301,7 +302,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((defaultValue - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -318,12 +319,17 @@ hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt { require frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue); + + require frozenAtMirror[Controller][FundId] != 0 => flowEndGhost[Controller][FundId] == frozenAtMirror[Controller][FundId]; + require frozenAtMirror[Controller][FundId] == 0 => flowEndGhost[Controller][FundId] == lockExpiryMirror[Controller][FundId]; } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt VaultBase.Timestamp defaultValue { frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); + + flowEndGhost[Controller][FundId] = frozenAtMirror[Controller][FundId] != 0 ? frozenAtMirror[Controller][FundId] : lockExpiryMirror[Controller][FundId]; } @@ -387,7 +393,7 @@ hook Sload uint128 defaultValue + defaultValue + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -399,7 +405,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + defaultValue + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (lockMaximumMirror[Controller][FundId] + * (flowEndGhost[Controller][FundId] - updatedMirror[Controller][FundId][AccountId])); } @@ -408,8 +414,8 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId 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. + forall VaultBase.FundId FundId. + forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == 0) && (usum VaultBase.AccountId AccountId, VaultBase.Controller Controller, @@ -419,6 +425,15 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultB +ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint256)) flowEndGhost { + init_state axiom + (forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + flowEndGhost[Controller][FundId] == 0); +} + + + // invariant 4 (Certora's solvency) - // account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == _token.balanceOf(currentContract) invariant solvency() From 2e675d31ed1e7afb3c17fa8bce8f49b5c90ceeb2 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 13 Jun 2025 17:24:45 +0100 Subject: [PATCH 11/27] flowEnd as definition --- certora/specs/Vault.spec | 92 +++++++++++++++++++++------------------- 1 file changed, 49 insertions(+), 43 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index c5a35a3..339dffb 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -79,12 +79,12 @@ hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum { require lockMaximumMirror[Controller][FundId] == unwrapTimestamp(defaultValue); - require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] - - updatedMirror[Controller][FundId][AccountId])); + // require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + // + designatedBalanceMirror[Controller][FundId][AccountId] + // + ((incomingMirror[Controller][FundId][AccountId] + // - outgoingMirror[Controller][FundId][AccountId]) + // * (flowEnd(Controller, FundId) + // - updatedMirror[Controller][FundId][AccountId])); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum @@ -97,26 +97,27 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun // - outgoingMirror[Controller][FundId][AccountId]) // * (lockMaximumMirror[Controller][FundId] // - updatedMirror[Controller][FundId][AccountId])); - mathint oldSum = usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]; + + // mathint oldSum = usum VaultBase.Controller controller, + // VaultBase.FundId fundId, + // VaultBase.AccountId AccountId. + // expectedFunds[controller][fundId][AccountId]; - havoc expectedFunds assuming forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - forall VaultBase.AccountId AccountId. - expectedFunds@new[controller][fundId][AccountId] - == availableBalanceMirror[controller][fundId][AccountId] - + designatedBalanceMirror[controller][fundId][AccountId] - + ((incomingMirror[controller][fundId][AccountId] - - outgoingMirror[controller][fundId][AccountId]) - * (flowEndGhost[Controller][FundId] - - updatedMirror[controller][fundId][AccountId])); + // havoc expectedFunds assuming forall VaultBase.Controller controller. + // forall VaultBase.FundId fundId. + // forall VaultBase.AccountId AccountId. + // expectedFunds@new[controller][fundId][AccountId] + // == availableBalanceMirror[controller][fundId][AccountId] + // + designatedBalanceMirror[controller][fundId][AccountId] + // + ((incomingMirror[controller][fundId][AccountId] + // - outgoingMirror[controller][fundId][AccountId]) + // * (flowEnd(Controller, FundId) + // - updatedMirror[controller][fundId][AccountId])); - require (usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]) == oldSum; + // require (usum VaultBase.Controller controller, + // VaultBase.FundId fundId, + // VaultBase.AccountId AccountId. + // expectedFunds[controller][fundId][AccountId]) == oldSum; } // 1 - verified @@ -156,7 +157,7 @@ hook Sload VaultBase.TokensPerSecond defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - defaultValue) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -168,7 +169,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - defaultValue) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -190,7 +191,7 @@ hook Sload VaultBase.Timestamp defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - unwrapTimestamp(defaultValue))); } @@ -202,7 +203,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - unwrapTimestamp(defaultValue))); } @@ -224,7 +225,7 @@ hook Sload uint128 defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -236,7 +237,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -290,7 +291,7 @@ hook Sload VaultBase.TokensPerSecond defaultValue + designatedBalanceMirror[Controller][FundId][AccountId] + ((defaultValue - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -302,7 +303,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + designatedBalanceMirror[Controller][FundId][AccountId] + ((defaultValue - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -320,8 +321,8 @@ hook Sload VaultBase.Timestamp defaultValue { require frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue); - require frozenAtMirror[Controller][FundId] != 0 => flowEndGhost[Controller][FundId] == frozenAtMirror[Controller][FundId]; - require frozenAtMirror[Controller][FundId] == 0 => flowEndGhost[Controller][FundId] == lockExpiryMirror[Controller][FundId]; + // require frozenAtMirror[Controller][FundId] != 0 => flowEndGhost[Controller][FundId] == frozenAtMirror[Controller][FundId]; + // require frozenAtMirror[Controller][FundId] == 0 => flowEndGhost[Controller][FundId] == lockExpiryMirror[Controller][FundId]; } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt @@ -329,7 +330,7 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun { frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); - flowEndGhost[Controller][FundId] = frozenAtMirror[Controller][FundId] != 0 ? frozenAtMirror[Controller][FundId] : lockExpiryMirror[Controller][FundId]; + // flowEndGhost[Controller][FundId] = frozenAtMirror[Controller][FundId] != 0 ? frozenAtMirror[Controller][FundId] : lockExpiryMirror[Controller][FundId]; } @@ -393,7 +394,7 @@ hook Sload uint128 defaultValue + defaultValue + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -405,7 +406,7 @@ hook Sstore _accounts[KEY VaultBase.Controller Controller][KEY VaultBase.FundId + defaultValue + ((incomingMirror[Controller][FundId][AccountId] - outgoingMirror[Controller][FundId][AccountId]) - * (flowEndGhost[Controller][FundId] + * (flowEnd(Controller, FundId) - updatedMirror[Controller][FundId][AccountId])); } @@ -425,12 +426,17 @@ ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => mapping(VaultB -ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint256)) flowEndGhost { - init_state axiom - (forall VaultBase.Controller Controller. - forall VaultBase.FundId FundId. - flowEndGhost[Controller][FundId] == 0); -} +definition flowEnd(VaultBase.Controller Controller, VaultBase.FundId FundId) returns uint256 + = frozenAtMirror[Controller][FundId] != 0 + ? frozenAtMirror[Controller][FundId] + : lockExpiryMirror[Controller][FundId]; + +// ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint256)) flowEndGhost { +// init_state axiom +// (forall VaultBase.Controller Controller. +// forall VaultBase.FundId FundId. +// flowEndGhost[Controller][FundId] == 0); +// } From d99499b1cffbe7646a69cd61a34857733ebe62a9 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Mon, 30 Jun 2025 23:59:10 +0100 Subject: [PATCH 12/27] check in the latest code --- certora/specs/Vault.spec | 84 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 339dffb..5eaaa3b 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -58,12 +58,40 @@ hook Sload VaultBase.Timestamp defaultValue _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry { require lockExpiryMirror[Controller][FundId] == unwrapTimestamp(defaultValue); + + require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (flowEnd(Controller, FundId) + - updatedMirror[Controller][FundId][AccountId])); } 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 controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]; + + havoc expectedFunds assuming forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId AccountId. + expectedFunds@new[controller][fundId][AccountId] + == availableBalanceMirror[controller][fundId][AccountId] + + designatedBalanceMirror[controller][fundId][AccountId] + + ((incomingMirror[controller][fundId][AccountId] + - outgoingMirror[controller][fundId][AccountId]) + * (flowEnd(Controller, FundId) + - updatedMirror[controller][fundId][AccountId])); + + require (usum VaultBase.Controller controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]) == oldSum; } @@ -321,8 +349,25 @@ hook Sload VaultBase.Timestamp defaultValue { require frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue); + // old + // require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] + // + designatedBalanceMirror[Controller][FundId][AccountId] + // + ((incomingMirror[Controller][FundId][AccountId] + // - outgoingMirror[Controller][FundId][AccountId]) + // * (flowEnd(Controller, FundId) + // - updatedMirror[Controller][FundId][AccountId])); + // require frozenAtMirror[Controller][FundId] != 0 => flowEndGhost[Controller][FundId] == frozenAtMirror[Controller][FundId]; // require frozenAtMirror[Controller][FundId] == 0 => flowEndGhost[Controller][FundId] == lockExpiryMirror[Controller][FundId]; + + + require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] + == availableBalanceMirror[Controller][FundId][AccountId] + + designatedBalanceMirror[Controller][FundId][AccountId] + + ((incomingMirror[Controller][FundId][AccountId] + - outgoingMirror[Controller][FundId][AccountId]) + * (flowEnd(Controller, FundId) + - updatedMirror[Controller][FundId][AccountId])); } hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt @@ -330,7 +375,37 @@ hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId Fun { frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); + // old + // expectedFunds[Controller][FundId][AccountId] = availableBalanceMirror[Controller][FundId][AccountId] + // + designatedBalanceMirror[Controller][FundId][AccountId] + // + ((incomingMirror[Controller][FundId][AccountId] + // - outgoingMirror[Controller][FundId][AccountId]) + // * (flowEnd(Controller, FundId) + // - updatedMirror[Controller][FundId][AccountId])); + // flowEndGhost[Controller][FundId] = frozenAtMirror[Controller][FundId] != 0 ? frozenAtMirror[Controller][FundId] : lockExpiryMirror[Controller][FundId]; + + + mathint oldSum = usum VaultBase.Controller controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]; + + havoc expectedFunds assuming forall VaultBase.Controller controller. + forall VaultBase.FundId fundId. + forall VaultBase.AccountId AccountId. + expectedFunds@new[controller][fundId][AccountId] + == availableBalanceMirror[controller][fundId][AccountId] + + designatedBalanceMirror[controller][fundId][AccountId] + + ((incomingMirror[controller][fundId][AccountId] + - outgoingMirror[controller][fundId][AccountId]) + * (flowEnd(Controller, FundId) + - updatedMirror[controller][fundId][AccountId])); + + require (usum VaultBase.Controller controller, + VaultBase.FundId fundId, + VaultBase.AccountId AccountId. + expectedFunds[controller][fundId][AccountId]) == oldSum; } @@ -483,3 +558,12 @@ invariant supporter() + +// 6 +invariant updatedMirrorCheck() + forall VaultBase.Controller Controller. + forall VaultBase.FundId FundId. + forall VaultBase.AccountId AccountId. + updatedMirror[Controller][FundId][AccountId] <= flowEnd(Controller, FundId) + && updatedMirror[Controller][FundId][AccountId] <= ghostLastTimestamp; + From 0f09197806fdbefd1ba9d945278281462b92c5b2 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Mon, 14 Jul 2025 18:21:19 +0200 Subject: [PATCH 13/27] Fix rules and clean ups. Set expectedFunds to 0 if it would be negative. Prove some more auxiliary invariants. Explain requires. Clean-up plus comments. --- certora/harness/VaultHarness.sol | 1 - certora/specs/Vault.spec | 781 ++++++++++++++----------------- 2 files changed, 350 insertions(+), 432 deletions(-) diff --git a/certora/harness/VaultHarness.sol b/certora/harness/VaultHarness.sol index 66bb0d2..72d5497 100644 --- a/certora/harness/VaultHarness.sol +++ b/certora/harness/VaultHarness.sol @@ -19,5 +19,4 @@ contract VaultHarness is Vault { return Timestamp.unwrap(timestamp); } - } diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 5eaaa3b..12a1729 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -2,568 +2,487 @@ 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; } -// rule sanity(env e, method f) { -// calldataarg args; -// f(e, args); -// satisfy true; -// } +// 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 mapping(address => uint256) tokenBalanceOfMirror { - init_state axiom forall address a. tokenBalanceOfMirror[a] == 0; +ghost mathint lastTimestamp { + init_state axiom lastTimestamp > 0; // we must start with a positive timestamp (0 is used to encode "not set") } -ghost mathint sumOfBalances { - init_state axiom sumOfBalances == 0; +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 never check that explicitly, but it follows from the invariant outgoingLEAvailable() that we prove. + +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 sumOfBalances >= to_mathint(balance); - require tokenBalanceOfMirror[addr] == balance; + require(tokenBalanceOfMirror[addr] == balance, "tokenBalance mirror"); } hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) { - sumOfBalances = sumOfBalances - oldValue + newValue; tokenBalanceOfMirror[addr] = newValue; } invariant totalSupplyIsSumOfBalances() - to_mathint(Token.totalSupply()) == sumOfBalances; + Token.totalSupply() == (usum address a. tokenBalanceOfMirror[a]); +//------------------------------------------------------------// +// Mirror variables for storage variables in VaultBase. +//------------------------------------------------------------// +// mirror for lockExpiry. - - - - - - -// new ghosts needed in 1 ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint40)) lockExpiryMirror { init_state axiom - forall VaultBase.Controller Controller. - forall VaultBase.FundId FundId. - lockExpiryMirror[Controller][FundId] == 0; + 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 + _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockExpiry { - require lockExpiryMirror[Controller][FundId] == unwrapTimestamp(defaultValue); - - require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + require(lockExpiryMirror[controller][fundId] == unwrapTimestamp(defaultValue), "lockExpiry mirror"); } -hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockExpiry +hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockExpiry VaultBase.Timestamp defaultValue { - lockExpiryMirror[Controller][FundId] = unwrapTimestamp(defaultValue); + lockExpiryMirror[controller][fundId] = unwrapTimestamp(defaultValue); - mathint oldSum = usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]; + mathint oldSum = usum VaultBase.Controller c, + VaultBase.FundId f, + VaultBase.AccountId a. + expectedFunds[c][f][a]; - havoc expectedFunds assuming forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - forall VaultBase.AccountId AccountId. - expectedFunds@new[controller][fundId][AccountId] - == availableBalanceMirror[controller][fundId][AccountId] - + designatedBalanceMirror[controller][fundId][AccountId] - + ((incomingMirror[controller][fundId][AccountId] - - outgoingMirror[controller][fundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[controller][fundId][AccountId])); + havoc expectedFunds assuming forall VaultBase.Controller c. + forall VaultBase.FundId f. + forall VaultBase.AccountId a. + expectedFunds@new[c][f][a] + == expectedFundsDef(c, f, a); - require (usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]) == oldSum; + // 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; + 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 + _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockMaximum { - require lockMaximumMirror[Controller][FundId] == unwrapTimestamp(defaultValue); - // require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - // + designatedBalanceMirror[Controller][FundId][AccountId] - // + ((incomingMirror[Controller][FundId][AccountId] - // - outgoingMirror[Controller][FundId][AccountId]) - // * (flowEnd(Controller, FundId) - // - updatedMirror[Controller][FundId][AccountId])); + require(lockMaximumMirror[controller][fundId] == unwrapTimestamp(defaultValue), "lockMaximum mirror"); } -hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].lockMaximum +hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].lockMaximum VaultBase.Timestamp defaultValue { - lockMaximumMirror[Controller][FundId] = unwrapTimestamp(defaultValue); - // require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - // + designatedBalanceMirror[Controller][FundId][AccountId] - // + ((incomingMirror[Controller][FundId][AccountId] - // - outgoingMirror[Controller][FundId][AccountId]) - // * (lockMaximumMirror[Controller][FundId] - // - updatedMirror[Controller][FundId][AccountId])); - - // mathint oldSum = usum VaultBase.Controller controller, - // VaultBase.FundId fundId, - // VaultBase.AccountId AccountId. - // expectedFunds[controller][fundId][AccountId]; - - // havoc expectedFunds assuming forall VaultBase.Controller controller. - // forall VaultBase.FundId fundId. - // forall VaultBase.AccountId AccountId. - // expectedFunds@new[controller][fundId][AccountId] - // == availableBalanceMirror[controller][fundId][AccountId] - // + designatedBalanceMirror[controller][fundId][AccountId] - // + ((incomingMirror[controller][fundId][AccountId] - // - outgoingMirror[controller][fundId][AccountId]) - // * (flowEnd(Controller, FundId) - // - updatedMirror[controller][fundId][AccountId])); - - // require (usum VaultBase.Controller controller, - // VaultBase.FundId fundId, - // VaultBase.AccountId AccountId. - // expectedFunds[controller][fundId][AccountId]) == oldSum; + lockMaximumMirror[controller][fundId] = unwrapTimestamp(defaultValue); } -// 1 - verified -// (∀ 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]; -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// - - - - -// new ghosts needed in 2 +// 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); + (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 + _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.outgoing { - require outgoingMirror[Controller][FundId][AccountId] == defaultValue; - require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - defaultValue) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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 +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] = availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - defaultValue) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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; + 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 + _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.updated { - require updatedMirror[Controller][FundId][AccountId] == unwrapTimestamp(defaultValue); - require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - unwrapTimestamp(defaultValue))); -} + 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 +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] = availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - unwrapTimestamp(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; + 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 + _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.available { - require availableBalanceMirror[Controller][FundId][AccountId] == defaultValue; - require expectedFunds[Controller][FundId][AccountId] == defaultValue - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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 +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] = defaultValue - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + availableBalanceMirror[controller][fundId][accountId] = defaultValue; + expectedFunds[controller][fundId][accountId] = expectedFundsDef(controller, fundId, accountId); } - - -// 2 - verified -// (∀ 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 supporter(); - } - } -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// - - - - - -// new ghosts needed in 3 +// 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); + (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 + _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].flow.incoming { - require incomingMirror[Controller][FundId][AccountId] == defaultValue; - require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((defaultValue - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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 +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] = availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((defaultValue - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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; + 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); - - // old - // require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - // + designatedBalanceMirror[Controller][FundId][AccountId] - // + ((incomingMirror[Controller][FundId][AccountId] - // - outgoingMirror[Controller][FundId][AccountId]) - // * (flowEnd(Controller, FundId) - // - updatedMirror[Controller][FundId][AccountId])); - - // require frozenAtMirror[Controller][FundId] != 0 => flowEndGhost[Controller][FundId] == frozenAtMirror[Controller][FundId]; - // require frozenAtMirror[Controller][FundId] == 0 => flowEndGhost[Controller][FundId] == lockExpiryMirror[Controller][FundId]; - - - require forall VaultBase.AccountId AccountId. expectedFunds[Controller][FundId][AccountId] - == availableBalanceMirror[Controller][FundId][AccountId] - + designatedBalanceMirror[Controller][FundId][AccountId] - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + require(frozenAtMirror[Controller][FundId] == unwrapTimestamp(defaultValue), "frozenAt mirror"); } -hook Sstore _funds[KEY VaultBase.Controller Controller][KEY VaultBase.FundId FundId].frozenAt +hook Sstore _funds[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId].frozenAt VaultBase.Timestamp defaultValue { - frozenAtMirror[Controller][FundId] = unwrapTimestamp(defaultValue); + frozenAtMirror[controller][fundId] = unwrapTimestamp(defaultValue); - // old - // expectedFunds[Controller][FundId][AccountId] = availableBalanceMirror[Controller][FundId][AccountId] - // + designatedBalanceMirror[Controller][FundId][AccountId] - // + ((incomingMirror[Controller][FundId][AccountId] - // - outgoingMirror[Controller][FundId][AccountId]) - // * (flowEnd(Controller, FundId) - // - updatedMirror[Controller][FundId][AccountId])); + mathint oldSum = usum VaultBase.Controller c, + VaultBase.FundId f, + VaultBase.AccountId a. + expectedFunds[c][f][a]; - // flowEndGhost[Controller][FundId] = frozenAtMirror[Controller][FundId] != 0 ? frozenAtMirror[Controller][FundId] : lockExpiryMirror[Controller][FundId]; + havoc expectedFunds assuming forall VaultBase.Controller c. + forall VaultBase.FundId f. + forall VaultBase.AccountId a. + expectedFunds@new[c][f][a] + == expectedFundsDef(c, f, a); - - mathint oldSum = usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]; - - havoc expectedFunds assuming forall VaultBase.Controller controller. - forall VaultBase.FundId fundId. - forall VaultBase.AccountId AccountId. - expectedFunds@new[controller][fundId][AccountId] - == availableBalanceMirror[controller][fundId][AccountId] - + designatedBalanceMirror[controller][fundId][AccountId] - + ((incomingMirror[controller][fundId][AccountId] - - outgoingMirror[controller][fundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[controller][fundId][AccountId])); - - require (usum VaultBase.Controller controller, - VaultBase.FundId fundId, - VaultBase.AccountId AccountId. - expectedFunds[controller][fundId][AccountId]) == oldSum; + // 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"); } - - -ghost mathint ghostLastTimestamp; - -hook TIMESTAMP uint256 time { - require to_mathint(time) < max_uint40; // Timestamp type is uint40 that's why we have this require. uint40 is used in the whole contract - require to_mathint(time) >= ghostLastTimestamp; - require ghostLastTimestamp > 0; // this require is necessary to avoid violation in "supporter" invariant. It happens only when timestamp == 0 and it's safe to require it because it's not 0 in real life. - ghostLastTimestamp = time; -} - - - -definition statusCVL(VaultBase.Controller Controller, VaultBase.FundId FundId) returns VaultBase.FundStatus = - ghostLastTimestamp < 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 -// (∀ 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])); -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// - - - - - -// new ghosts needed in 4 +// 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; + 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 + _accounts[KEY VaultBase.Controller controller][KEY VaultBase.FundId fundId][KEY VaultBase.AccountId accountId].balance.designated { - require designatedBalanceMirror[Controller][FundId][AccountId] == defaultValue; - require expectedFunds[Controller][FundId][AccountId] == availableBalanceMirror[Controller][FundId][AccountId] - + defaultValue - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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 +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] = availableBalanceMirror[Controller][FundId][AccountId] - + defaultValue - + ((incomingMirror[Controller][FundId][AccountId] - - outgoingMirror[Controller][FundId][AccountId]) - * (flowEnd(Controller, FundId) - - updatedMirror[Controller][FundId][AccountId])); + 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; -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; +//------------------------------------------------------------// +// 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(); + } +} -definition flowEnd(VaultBase.Controller Controller, VaultBase.FundId FundId) returns uint256 - = frozenAtMirror[Controller][FundId] != 0 - ? frozenAtMirror[Controller][FundId] - : lockExpiryMirror[Controller][FundId]; - -// ghost mapping(VaultBase.Controller => mapping(VaultBase.FundId => uint256)) flowEndGhost { -// init_state axiom -// (forall VaultBase.Controller Controller. -// forall VaultBase.FundId FundId. -// flowEndGhost[Controller][FundId] == 0); -// } - - - -// invariant 4 (Certora's solvency) - -// account.balance.available + account.balance.designated + ((incoming - outgoing) * (fund.flowEnd() - flow.updated)) == _token.balanceOf(currentContract) -invariant solvency() - (usum VaultBase.Controller Controller, - VaultBase.FundId FundId, - VaultBase.AccountId AccountId. - expectedFunds[Controller][FundId][AccountId]) == to_mathint(tokenBalanceOfMirror[currentContract]) - // forall VaultBase.Controller Controller. - // forall VaultBase.FundId FundId. - // forall VaultBase.AccountId AccountId. - // availableBalanceMirror[Controller][FundId][AccountId] - // + designatedBalanceMirror[Controller][FundId][AccountId] - // + ((incomingMirror[Controller][FundId][AccountId] - // - outgoingMirror[Controller][FundId][AccountId]) - // * (lockMaximumMirror[Controller][FundId] - // - updatedMirror[Controller][FundId][AccountId])) - // == tokenBalanceOfMirror[currentContract] - { - preserved { - requireInvariant lockExpiryLELockMaximum(); - requireInvariant outgoingLEAvailable(); - requireInvariant incomingEqualsOutgoing(); - requireInvariant supporter(); - } - } -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// -//------------------------------------------------------------// - - - - - -// 5 (needed to prove 2) - verified -invariant supporter() - forall VaultBase.Controller Controller. - forall VaultBase.FundId FundId. - forall VaultBase.AccountId AccountId. - lockMaximumMirror[Controller][FundId] == 0 => outgoingMirror[Controller][FundId][AccountId] == 0; - - - - -// 6 -invariant updatedMirrorCheck() - forall VaultBase.Controller Controller. - forall VaultBase.FundId FundId. - forall VaultBase.AccountId AccountId. - updatedMirror[Controller][FundId][AccountId] <= flowEnd(Controller, FundId) - && updatedMirror[Controller][FundId][AccountId] <= ghostLastTimestamp; - +// 7 - verified except for timeout in flow +// expectedFundsMirror is always equal to the expectedFundsDef calculation. +// This invariant is needed to prove solvency. +// 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(); + } +} From 191b9b65b74e0c67244722e4fe9a6f3d396e3fe8 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 17 Jul 2025 12:57:53 +0200 Subject: [PATCH 14/27] Minor comment changes --- certora/specs/Vault.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/Vault.spec b/certora/specs/Vault.spec index 12a1729..3f61f8f 100644 --- a/certora/specs/Vault.spec +++ b/certora/specs/Vault.spec @@ -38,7 +38,7 @@ hook TIMESTAMP uint256 time { // 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 never check that explicitly, but it follows from the invariant outgoingLEAvailable() that we prove. +// We check that explicitly in the invariant expectedFundsMirror(). definition max(mathint a, mathint b) returns mathint = a >= b ? a : b; @@ -472,8 +472,8 @@ invariant updatedLETimestampAndFlowEnd() } // 7 - verified except for timeout in flow -// expectedFundsMirror is always equal to the expectedFundsDef calculation. -// This invariant is needed to prove solvency. +// 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) From dee68bd53b0a05c940586d20c5fb7b8315a55d93 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 18 Jul 2025 15:50:00 +0200 Subject: [PATCH 15/27] Added multi_assert_check to avoid timeout --- certora/confs/Vault.conf | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index 2c73a9a..f15730c 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -1,29 +1,20 @@ { "files": [ "certora/harness/VaultHarness.sol", - //"contracts/Vault.sol", - // "certora/harness/MarketplaceHarness.sol", - // "contracts/Marketplace.sol", - // "contracts/Vault.sol", - // "contracts/Groth16Verifier.sol", "certora/helpers/ERC20A.sol", ], "parametric_contracts": ["VaultHarness"], "link" : [ "VaultHarness:_token=ERC20A", - // "MarketplaceHarness:_vault=VaultHarness", - // "MarketplaceHarness:_verifier=Groth16Verifier" ], "packages": [ "@openzeppelin/=node_modules/@openzeppelin", ], "msg": "Verifying Vault", + "multi_assert_check": true, "rule_sanity": "basic", "verify": "VaultHarness:certora/specs/Vault.spec", - // "optimistic_loop": true, "loop_iter": "3", - // "optimistic_hashing": true, - // "hashing_length_bound": "512", "build_cache": true, "solc": "solc8.28", } From c6b4e5e5b5e067ebaa5c657cb1cfdece0af7e1ea Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 18 Jul 2025 17:29:38 +0200 Subject: [PATCH 16/27] Added a README file --- certora/README.md | 64 ++++++++++++++++++++++++++++++++++++++++ certora/confs/Vault.conf | 1 + 2 files changed, 65 insertions(+) create mode 100644 certora/README.md diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..5c8f986 --- /dev/null +++ b/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. + diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index f15730c..4cb4bcb 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -17,4 +17,5 @@ "loop_iter": "3", "build_cache": true, "solc": "solc8.28", + "prover_version": "master" // remove with next Certora release } From a63fcd9b5610f2dcedf9a3d98297b51199212013 Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Tue, 29 Jul 2025 10:48:59 +0300 Subject: [PATCH 17/27] Add mutation 001: accumulateFlows off-by-one --- .../mutations/001_accumulateFlows_off_by_one.patch | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 certora/mutations/001_accumulateFlows_off_by_one.patch diff --git a/certora/mutations/001_accumulateFlows_off_by_one.patch b/certora/mutations/001_accumulateFlows_off_by_one.patch new file mode 100644 index 0000000..538be7d --- /dev/null +++ b/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; + } From d2ca1ae5b189ccaed3fdda574caff7436772d269 Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Tue, 29 Jul 2025 20:09:27 +0300 Subject: [PATCH 18/27] add more mutations --- .../002_flowOut_rate_calculation.patch | 13 ++++++ .../003_status_boundary_condition.patch | 13 ++++++ .../004_isSolventAt_boundary_condition.patch | 13 ++++++ .../005_flowIn_future_timestamp.patch | 13 ++++++ .../mutations/006_flow_prelock_bypass.patch | 13 ++++++ .../007_checkAccountInvariant_bypass.patch | 13 ++++++ .../008_deposit_storage_corruption.patch | 13 ++++++ .../009_transfer_balance_check_removal.patch | 13 ++++++ .../010_burnAccount_logic_inversion.patch | 13 ++++++ .../011_withdraw_reentrancy_ordering.patch | 17 ++++++++ .../012_withdraw_unsafe_transfer.patch | 13 ++++++ .../013_deposit_unsafe_transferFrom.patch | 13 ++++++ .../014_all_unsafe_token_transfers.patch | 40 +++++++++++++++++++ .../015_transfer_authorization_bypass.patch | 14 +++++++ .../016_pause_functions_deleted.patch | 18 +++++++++ 15 files changed, 232 insertions(+) create mode 100644 certora/mutations/002_flowOut_rate_calculation.patch create mode 100644 certora/mutations/003_status_boundary_condition.patch create mode 100644 certora/mutations/004_isSolventAt_boundary_condition.patch create mode 100644 certora/mutations/005_flowIn_future_timestamp.patch create mode 100644 certora/mutations/006_flow_prelock_bypass.patch create mode 100644 certora/mutations/007_checkAccountInvariant_bypass.patch create mode 100644 certora/mutations/008_deposit_storage_corruption.patch create mode 100644 certora/mutations/009_transfer_balance_check_removal.patch create mode 100644 certora/mutations/010_burnAccount_logic_inversion.patch create mode 100644 certora/mutations/011_withdraw_reentrancy_ordering.patch create mode 100644 certora/mutations/012_withdraw_unsafe_transfer.patch create mode 100644 certora/mutations/013_deposit_unsafe_transferFrom.patch create mode 100644 certora/mutations/014_all_unsafe_token_transfers.patch create mode 100644 certora/mutations/015_transfer_authorization_bypass.patch create mode 100644 certora/mutations/016_pause_functions_deleted.patch diff --git a/certora/mutations/002_flowOut_rate_calculation.patch b/certora/mutations/002_flowOut_rate_calculation.patch new file mode 100644 index 0000000..3bf368d --- /dev/null +++ b/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); + } diff --git a/certora/mutations/003_status_boundary_condition.patch b/certora/mutations/003_status_boundary_condition.patch new file mode 100644 index 0000000..a079092 --- /dev/null +++ b/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; + } diff --git a/certora/mutations/004_isSolventAt_boundary_condition.patch b/certora/mutations/004_isSolventAt_boundary_condition.patch new file mode 100644 index 0000000..011a7bb --- /dev/null +++ b/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 diff --git a/certora/mutations/005_flowIn_future_timestamp.patch b/certora/mutations/005_flowIn_future_timestamp.patch new file mode 100644 index 0000000..457efc3 --- /dev/null +++ b/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; + } + diff --git a/certora/mutations/006_flow_prelock_bypass.patch b/certora/mutations/006_flow_prelock_bypass.patch new file mode 100644 index 0000000..828b0c2 --- /dev/null +++ b/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); diff --git a/certora/mutations/007_checkAccountInvariant_bypass.patch b/certora/mutations/007_checkAccountInvariant_bypass.patch new file mode 100644 index 0000000..968d578 --- /dev/null +++ b/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(); diff --git a/certora/mutations/008_deposit_storage_corruption.patch b/certora/mutations/008_deposit_storage_corruption.patch new file mode 100644 index 0000000..072d94d --- /dev/null +++ b/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; + diff --git a/certora/mutations/009_transfer_balance_check_removal.patch b/certora/mutations/009_transfer_balance_check_removal.patch new file mode 100644 index 0000000..0fbf5d1 --- /dev/null +++ b/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); diff --git a/certora/mutations/010_burnAccount_logic_inversion.patch b/certora/mutations/010_burnAccount_logic_inversion.patch new file mode 100644 index 0000000..b52e4e2 --- /dev/null +++ b/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]; diff --git a/certora/mutations/011_withdraw_reentrancy_ordering.patch b/certora/mutations/011_withdraw_reentrancy_ordering.patch new file mode 100644 index 0000000..4b232ec --- /dev/null +++ b/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 { diff --git a/certora/mutations/012_withdraw_unsafe_transfer.patch b/certora/mutations/012_withdraw_unsafe_transfer.patch new file mode 100644 index 0000000..4d7789b --- /dev/null +++ b/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 { diff --git a/certora/mutations/013_deposit_unsafe_transferFrom.patch b/certora/mutations/013_deposit_unsafe_transferFrom.patch new file mode 100644 index 0000000..b5a67e6 --- /dev/null +++ b/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 diff --git a/certora/mutations/014_all_unsafe_token_transfers.patch b/certora/mutations/014_all_unsafe_token_transfers.patch new file mode 100644 index 0000000..b6916d7 --- /dev/null +++ b/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 { diff --git a/certora/mutations/015_transfer_authorization_bypass.patch b/certora/mutations/015_transfer_authorization_bypass.patch new file mode 100644 index 0000000..1cba346 --- /dev/null +++ b/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); + } + diff --git a/certora/mutations/016_pause_functions_deleted.patch b/certora/mutations/016_pause_functions_deleted.patch new file mode 100644 index 0000000..f61fabe --- /dev/null +++ b/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(); + } From a3992bc0c0ad1d84cae314e3e76a73fde835c6db Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Wed, 30 Jul 2025 11:52:01 +0300 Subject: [PATCH 19/27] add encoding and calculation mutations --- .../017_accountId_encoding_corruption.patch | 13 +++++++++++++ .../018_duration_calculation_order_inversion.patch | 12 ++++++++++++ .../mutations/019_period_calculation_round_up.patch | 13 +++++++++++++ 3 files changed, 38 insertions(+) create mode 100644 certora/mutations/017_accountId_encoding_corruption.patch create mode 100644 certora/mutations/018_duration_calculation_order_inversion.patch create mode 100644 certora/mutations/019_period_calculation_round_up.patch diff --git a/certora/mutations/017_accountId_encoding_corruption.patch b/certora/mutations/017_accountId_encoding_corruption.patch new file mode 100644 index 0000000..0befdf6 --- /dev/null +++ b/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 diff --git a/certora/mutations/018_duration_calculation_order_inversion.patch b/certora/mutations/018_duration_calculation_order_inversion.patch new file mode 100644 index 0000000..b27d50d --- /dev/null +++ b/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)); + } + } diff --git a/certora/mutations/019_period_calculation_round_up.patch b/certora/mutations/019_period_calculation_round_up.patch new file mode 100644 index 0000000..aac56d6 --- /dev/null +++ b/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) + ); + } + From e21324f3ffeb35cf4895b0c96ae90eaca815dd2b Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Wed, 30 Jul 2025 12:03:51 +0300 Subject: [PATCH 20/27] add modifier bypass mutations --- certora/mutations/020_withdraw_pause_bypass.patch | 13 +++++++++++++ certora/mutations/021_deposit_pause_bypass.patch | 13 +++++++++++++ certora/mutations/022_transfer_pause_bypass.patch | 13 +++++++++++++ certora/mutations/023_flow_pause_bypass.patch | 13 +++++++++++++ certora/mutations/024_lock_pause_bypass.patch | 13 +++++++++++++ certora/mutations/025_extendLock_pause_bypass.patch | 13 +++++++++++++ certora/mutations/026_designate_pause_bypass.patch | 13 +++++++++++++ .../mutations/027_burnDesignated_pause_bypass.patch | 13 +++++++++++++ .../mutations/028_burnAccount_pause_bypass.patch | 13 +++++++++++++ certora/mutations/029_freezeFund_pause_bypass.patch | 13 +++++++++++++ ..._missing_whenNotPaused_withdrawByRecipient.patch | 13 +++++++++++++ .../mutations/031_pause_access_control_bypass.patch | 13 +++++++++++++ .../032_unpause_access_control_bypass.patch | 13 +++++++++++++ 13 files changed, 169 insertions(+) create mode 100644 certora/mutations/020_withdraw_pause_bypass.patch create mode 100644 certora/mutations/021_deposit_pause_bypass.patch create mode 100644 certora/mutations/022_transfer_pause_bypass.patch create mode 100644 certora/mutations/023_flow_pause_bypass.patch create mode 100644 certora/mutations/024_lock_pause_bypass.patch create mode 100644 certora/mutations/025_extendLock_pause_bypass.patch create mode 100644 certora/mutations/026_designate_pause_bypass.patch create mode 100644 certora/mutations/027_burnDesignated_pause_bypass.patch create mode 100644 certora/mutations/028_burnAccount_pause_bypass.patch create mode 100644 certora/mutations/029_freezeFund_pause_bypass.patch create mode 100644 certora/mutations/030_add_missing_whenNotPaused_withdrawByRecipient.patch create mode 100644 certora/mutations/031_pause_access_control_bypass.patch create mode 100644 certora/mutations/032_unpause_access_control_bypass.patch diff --git a/certora/mutations/020_withdraw_pause_bypass.patch b/certora/mutations/020_withdraw_pause_bypass.patch new file mode 100644 index 0000000..1ddf224 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/021_deposit_pause_bypass.patch b/certora/mutations/021_deposit_pause_bypass.patch new file mode 100644 index 0000000..fa8e898 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/022_transfer_pause_bypass.patch b/certora/mutations/022_transfer_pause_bypass.patch new file mode 100644 index 0000000..670f282 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/023_flow_pause_bypass.patch b/certora/mutations/023_flow_pause_bypass.patch new file mode 100644 index 0000000..220852a --- /dev/null +++ b/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); + } diff --git a/certora/mutations/024_lock_pause_bypass.patch b/certora/mutations/024_lock_pause_bypass.patch new file mode 100644 index 0000000..703594f --- /dev/null +++ b/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); + } diff --git a/certora/mutations/025_extendLock_pause_bypass.patch b/certora/mutations/025_extendLock_pause_bypass.patch new file mode 100644 index 0000000..7353396 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/026_designate_pause_bypass.patch b/certora/mutations/026_designate_pause_bypass.patch new file mode 100644 index 0000000..1bca334 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/027_burnDesignated_pause_bypass.patch b/certora/mutations/027_burnDesignated_pause_bypass.patch new file mode 100644 index 0000000..3c4c696 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/028_burnAccount_pause_bypass.patch b/certora/mutations/028_burnAccount_pause_bypass.patch new file mode 100644 index 0000000..383484e --- /dev/null +++ b/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); + } diff --git a/certora/mutations/029_freezeFund_pause_bypass.patch b/certora/mutations/029_freezeFund_pause_bypass.patch new file mode 100644 index 0000000..99d1815 --- /dev/null +++ b/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); + } diff --git a/certora/mutations/030_add_missing_whenNotPaused_withdrawByRecipient.patch b/certora/mutations/030_add_missing_whenNotPaused_withdrawByRecipient.patch new file mode 100644 index 0000000..73b3ba9 --- /dev/null +++ b/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); diff --git a/certora/mutations/031_pause_access_control_bypass.patch b/certora/mutations/031_pause_access_control_bypass.patch new file mode 100644 index 0000000..bde7261 --- /dev/null +++ b/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(); + } + diff --git a/certora/mutations/032_unpause_access_control_bypass.patch b/certora/mutations/032_unpause_access_control_bypass.patch new file mode 100644 index 0000000..9f9fed8 --- /dev/null +++ b/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(); + } + From 8cdf17987a89713ed19ec9f7b7aa1bc8fd86f1bc Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Wed, 30 Jul 2025 13:08:08 +0300 Subject: [PATCH 21/27] remove holder restriction --- .../033_withdrawByRecipient_auth_bypass.patch | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 certora/mutations/033_withdrawByRecipient_auth_bypass.patch diff --git a/certora/mutations/033_withdrawByRecipient_auth_bypass.patch b/certora/mutations/033_withdrawByRecipient_auth_bypass.patch new file mode 100644 index 0000000..0fcfd7f --- /dev/null +++ b/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); + } + From 2220c6659bdc366829d7ed56a746e427d0dd13c2 Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Wed, 30 Jul 2025 13:10:03 +0300 Subject: [PATCH 22/27] next period logic bug --- .../034_nextPeriod_advancement_failure.patch | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 certora/mutations/034_nextPeriod_advancement_failure.patch diff --git a/certora/mutations/034_nextPeriod_advancement_failure.patch b/certora/mutations/034_nextPeriod_advancement_failure.patch new file mode 100644 index 0000000..d2b607b --- /dev/null +++ b/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) { From 6c96ce84de05f4772745edea8f78cb938a5aa1fd Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Thu, 31 Jul 2025 11:07:39 +0300 Subject: [PATCH 23/27] add the rest mutations --- .../035_withdraw_account_not_deleted.patch | 13 +++++++++++++ certora/mutations/036_burnAccount_not_deleted.patch | 13 +++++++++++++ .../mutations/037_burnDesignated_no_decrement.patch | 13 +++++++++++++ 3 files changed, 39 insertions(+) create mode 100644 certora/mutations/035_withdraw_account_not_deleted.patch create mode 100644 certora/mutations/036_burnAccount_not_deleted.patch create mode 100644 certora/mutations/037_burnDesignated_no_decrement.patch 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); + } From ff6b69caed52885e51a5e0ffd08a978642028455 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 1 Aug 2025 17:33:35 +0200 Subject: [PATCH 24/27] Added mutations to config file --- certora/confs/Vault.conf | 30 +++++++++++++++++-- .../001_accumulateFlows_off_by_one.patch | 1 + .../002_flowOut_rate_calculation.patch | 1 + .../004_isSolventAt_boundary_condition.patch | 1 + .../005_flowIn_future_timestamp.patch | 1 + .../017_accountId_encoding_corruption.patch | 1 + .../Funds/003_status_boundary_condition.patch | 1 + ...duration_calculation_order_inversion.patch | 1 + .../015_transfer_authorization_bypass.patch | 1 + .../Vault/016_pause_functions_deleted.patch | 1 + .../Vault/020_withdraw_pause_bypass.patch | 1 + .../Vault/021_deposit_pause_bypass.patch | 1 + .../Vault/022_transfer_pause_bypass.patch | 1 + .../Vault/023_flow_pause_bypass.patch | 1 + .../Vault/024_lock_pause_bypass.patch | 1 + .../Vault/025_extendLock_pause_bypass.patch | 1 + .../Vault/026_designate_pause_bypass.patch | 1 + .../027_burnDesignated_pause_bypass.patch | 1 + .../Vault/028_burnAccount_pause_bypass.patch | 1 + .../Vault/029_freezeFund_pause_bypass.patch | 1 + ...ng_whenNotPaused_withdrawByRecipient.patch | 1 + .../031_pause_access_control_bypass.patch | 1 + .../032_unpause_access_control_bypass.patch | 1 + .../033_withdrawByRecipient_auth_bypass.patch | 1 + .../VaultBase/006_flow_prelock_bypass.patch | 1 + .../007_checkAccountInvariant_bypass.patch | 1 + .../008_deposit_storage_corruption.patch | 1 + .../009_transfer_balance_check_removal.patch | 1 + .../010_burnAccount_logic_inversion.patch | 1 + .../011_withdraw_reentrancy_ordering.patch | 1 + .../012_withdraw_unsafe_transfer.patch | 1 + .../013_deposit_unsafe_transferFrom.patch | 1 + .../014_all_unsafe_token_transfers.patch | 1 + .../035_withdraw_account_not_deleted.patch | 1 + .../036_burnAccount_not_deleted.patch | 1 + .../037_burnDesignated_no_decrement.patch | 1 + 36 files changed, 62 insertions(+), 3 deletions(-) create mode 120000 certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch create mode 120000 certora/mutations/Accounts/002_flowOut_rate_calculation.patch create mode 120000 certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch create mode 120000 certora/mutations/Accounts/005_flowIn_future_timestamp.patch create mode 120000 certora/mutations/Accounts/017_accountId_encoding_corruption.patch create mode 120000 certora/mutations/Funds/003_status_boundary_condition.patch create mode 120000 certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch create mode 120000 certora/mutations/Vault/015_transfer_authorization_bypass.patch create mode 120000 certora/mutations/Vault/016_pause_functions_deleted.patch create mode 120000 certora/mutations/Vault/020_withdraw_pause_bypass.patch create mode 120000 certora/mutations/Vault/021_deposit_pause_bypass.patch create mode 120000 certora/mutations/Vault/022_transfer_pause_bypass.patch create mode 120000 certora/mutations/Vault/023_flow_pause_bypass.patch create mode 120000 certora/mutations/Vault/024_lock_pause_bypass.patch create mode 120000 certora/mutations/Vault/025_extendLock_pause_bypass.patch create mode 120000 certora/mutations/Vault/026_designate_pause_bypass.patch create mode 120000 certora/mutations/Vault/027_burnDesignated_pause_bypass.patch create mode 120000 certora/mutations/Vault/028_burnAccount_pause_bypass.patch create mode 120000 certora/mutations/Vault/029_freezeFund_pause_bypass.patch create mode 120000 certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch create mode 120000 certora/mutations/Vault/031_pause_access_control_bypass.patch create mode 120000 certora/mutations/Vault/032_unpause_access_control_bypass.patch create mode 120000 certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch create mode 120000 certora/mutations/VaultBase/006_flow_prelock_bypass.patch create mode 120000 certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch create mode 120000 certora/mutations/VaultBase/008_deposit_storage_corruption.patch create mode 120000 certora/mutations/VaultBase/009_transfer_balance_check_removal.patch create mode 120000 certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch create mode 120000 certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch create mode 120000 certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch create mode 120000 certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch create mode 120000 certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch create mode 120000 certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch create mode 120000 certora/mutations/VaultBase/036_burnAccount_not_deleted.patch create mode 120000 certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index 4cb4bcb..d86f19f 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -8,14 +8,38 @@ "VaultHarness:_token=ERC20A", ], "packages": [ - "@openzeppelin/=node_modules/@openzeppelin", + "@openzeppelin/=node_modules/@openzeppelin/", ], - "msg": "Verifying Vault", + //"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 + "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" + } + ] + } } diff --git a/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch new file mode 120000 index 0000000..54ca445 --- /dev/null +++ b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch @@ -0,0 +1 @@ +../001_accumulateFlows_off_by_one.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/002_flowOut_rate_calculation.patch b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch new file mode 120000 index 0000000..544c078 --- /dev/null +++ b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch @@ -0,0 +1 @@ +../002_flowOut_rate_calculation.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch new file mode 120000 index 0000000..c15bd62 --- /dev/null +++ b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch @@ -0,0 +1 @@ +../004_isSolventAt_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/005_flowIn_future_timestamp.patch b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch new file mode 120000 index 0000000..faa53e1 --- /dev/null +++ b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch @@ -0,0 +1 @@ +../005_flowIn_future_timestamp.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/017_accountId_encoding_corruption.patch b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch new file mode 120000 index 0000000..cbc374d --- /dev/null +++ b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch @@ -0,0 +1 @@ +../017_accountId_encoding_corruption.patch \ No newline at end of file diff --git a/certora/mutations/Funds/003_status_boundary_condition.patch b/certora/mutations/Funds/003_status_boundary_condition.patch new file mode 120000 index 0000000..9c4390e --- /dev/null +++ b/certora/mutations/Funds/003_status_boundary_condition.patch @@ -0,0 +1 @@ +../003_status_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch new file mode 120000 index 0000000..14cc89a --- /dev/null +++ b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch @@ -0,0 +1 @@ +../018_duration_calculation_order_inversion.patch \ No newline at end of file diff --git a/certora/mutations/Vault/015_transfer_authorization_bypass.patch b/certora/mutations/Vault/015_transfer_authorization_bypass.patch new file mode 120000 index 0000000..1d43500 --- /dev/null +++ b/certora/mutations/Vault/015_transfer_authorization_bypass.patch @@ -0,0 +1 @@ +../015_transfer_authorization_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/016_pause_functions_deleted.patch b/certora/mutations/Vault/016_pause_functions_deleted.patch new file mode 120000 index 0000000..9ec9fc7 --- /dev/null +++ b/certora/mutations/Vault/016_pause_functions_deleted.patch @@ -0,0 +1 @@ +../016_pause_functions_deleted.patch \ No newline at end of file diff --git a/certora/mutations/Vault/020_withdraw_pause_bypass.patch b/certora/mutations/Vault/020_withdraw_pause_bypass.patch new file mode 120000 index 0000000..8fd710f --- /dev/null +++ b/certora/mutations/Vault/020_withdraw_pause_bypass.patch @@ -0,0 +1 @@ +../020_withdraw_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/021_deposit_pause_bypass.patch b/certora/mutations/Vault/021_deposit_pause_bypass.patch new file mode 120000 index 0000000..e843aed --- /dev/null +++ b/certora/mutations/Vault/021_deposit_pause_bypass.patch @@ -0,0 +1 @@ +../021_deposit_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/022_transfer_pause_bypass.patch b/certora/mutations/Vault/022_transfer_pause_bypass.patch new file mode 120000 index 0000000..be96903 --- /dev/null +++ b/certora/mutations/Vault/022_transfer_pause_bypass.patch @@ -0,0 +1 @@ +../022_transfer_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/023_flow_pause_bypass.patch b/certora/mutations/Vault/023_flow_pause_bypass.patch new file mode 120000 index 0000000..666ad2b --- /dev/null +++ b/certora/mutations/Vault/023_flow_pause_bypass.patch @@ -0,0 +1 @@ +../023_flow_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/024_lock_pause_bypass.patch b/certora/mutations/Vault/024_lock_pause_bypass.patch new file mode 120000 index 0000000..ce642ba --- /dev/null +++ b/certora/mutations/Vault/024_lock_pause_bypass.patch @@ -0,0 +1 @@ +../024_lock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/025_extendLock_pause_bypass.patch b/certora/mutations/Vault/025_extendLock_pause_bypass.patch new file mode 120000 index 0000000..855a17a --- /dev/null +++ b/certora/mutations/Vault/025_extendLock_pause_bypass.patch @@ -0,0 +1 @@ +../025_extendLock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/026_designate_pause_bypass.patch b/certora/mutations/Vault/026_designate_pause_bypass.patch new file mode 120000 index 0000000..9691134 --- /dev/null +++ b/certora/mutations/Vault/026_designate_pause_bypass.patch @@ -0,0 +1 @@ +../026_designate_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch new file mode 120000 index 0000000..d7c9a37 --- /dev/null +++ b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch @@ -0,0 +1 @@ +../027_burnDesignated_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/028_burnAccount_pause_bypass.patch b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch new file mode 120000 index 0000000..a84b025 --- /dev/null +++ b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch @@ -0,0 +1 @@ +../028_burnAccount_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/029_freezeFund_pause_bypass.patch b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch new file mode 120000 index 0000000..93d2574 --- /dev/null +++ b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch @@ -0,0 +1 @@ +../029_freezeFund_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch new file mode 120000 index 0000000..f962414 --- /dev/null +++ b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch @@ -0,0 +1 @@ +../030_add_missing_whenNotPaused_withdrawByRecipient.patch \ No newline at end of file diff --git a/certora/mutations/Vault/031_pause_access_control_bypass.patch b/certora/mutations/Vault/031_pause_access_control_bypass.patch new file mode 120000 index 0000000..7e2845e --- /dev/null +++ b/certora/mutations/Vault/031_pause_access_control_bypass.patch @@ -0,0 +1 @@ +../031_pause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/032_unpause_access_control_bypass.patch b/certora/mutations/Vault/032_unpause_access_control_bypass.patch new file mode 120000 index 0000000..cd222ed --- /dev/null +++ b/certora/mutations/Vault/032_unpause_access_control_bypass.patch @@ -0,0 +1 @@ +../032_unpause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch new file mode 120000 index 0000000..b836cc1 --- /dev/null +++ b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch @@ -0,0 +1 @@ +../033_withdrawByRecipient_auth_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/006_flow_prelock_bypass.patch b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch new file mode 120000 index 0000000..cbad95a --- /dev/null +++ b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch @@ -0,0 +1 @@ +../006_flow_prelock_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch new file mode 120000 index 0000000..ba56833 --- /dev/null +++ b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch @@ -0,0 +1 @@ +../007_checkAccountInvariant_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/008_deposit_storage_corruption.patch b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch new file mode 120000 index 0000000..7bf533d --- /dev/null +++ b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch @@ -0,0 +1 @@ +../008_deposit_storage_corruption.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch new file mode 120000 index 0000000..72391f7 --- /dev/null +++ b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch @@ -0,0 +1 @@ +../009_transfer_balance_check_removal.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch new file mode 120000 index 0000000..3d1dc34 --- /dev/null +++ b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch @@ -0,0 +1 @@ +../010_burnAccount_logic_inversion.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch new file mode 120000 index 0000000..585f2bf --- /dev/null +++ b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch @@ -0,0 +1 @@ +../011_withdraw_reentrancy_ordering.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch new file mode 120000 index 0000000..3a51b46 --- /dev/null +++ b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch @@ -0,0 +1 @@ +../012_withdraw_unsafe_transfer.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch new file mode 120000 index 0000000..4ecfe39 --- /dev/null +++ b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch @@ -0,0 +1 @@ +../013_deposit_unsafe_transferFrom.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch new file mode 120000 index 0000000..faccde9 --- /dev/null +++ b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch @@ -0,0 +1 @@ +../014_all_unsafe_token_transfers.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch new file mode 120000 index 0000000..ece025c --- /dev/null +++ b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch @@ -0,0 +1 @@ +../035_withdraw_account_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch new file mode 120000 index 0000000..84f4792 --- /dev/null +++ b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch @@ -0,0 +1 @@ +../036_burnAccount_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch new file mode 120000 index 0000000..8fba259 --- /dev/null +++ b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch @@ -0,0 +1 @@ +../037_burnDesignated_no_decrement.patch \ No newline at end of file From 4dff946866e35be06cd62da0fa218c444b0c30f4 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 1 Aug 2025 18:10:33 +0200 Subject: [PATCH 25/27] New mutation for extendLock --- certora/mutations/038_extendLock_beyond_max.patch | 12 ++++++++++++ .../VaultBase/038_extendLock_beyond_max.patch | 1 + 2 files changed, 13 insertions(+) create mode 100644 certora/mutations/038_extendLock_beyond_max.patch create mode 120000 certora/mutations/VaultBase/038_extendLock_beyond_max.patch diff --git a/certora/mutations/038_extendLock_beyond_max.patch b/certora/mutations/038_extendLock_beyond_max.patch new file mode 100644 index 0000000..f05200d --- /dev/null +++ b/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; + } + diff --git a/certora/mutations/VaultBase/038_extendLock_beyond_max.patch b/certora/mutations/VaultBase/038_extendLock_beyond_max.patch new file mode 120000 index 0000000..84d4511 --- /dev/null +++ b/certora/mutations/VaultBase/038_extendLock_beyond_max.patch @@ -0,0 +1 @@ +../038_extendLock_beyond_max.patch \ No newline at end of file From 7c2e9e68fca02ba2d9c746fa5b6366050b2bd8d9 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 1 Aug 2025 18:14:20 +0200 Subject: [PATCH 26/27] Fix compile problem in one mutation --- certora/mutations/010_burnAccount_logic_inversion.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/mutations/010_burnAccount_logic_inversion.patch b/certora/mutations/010_burnAccount_logic_inversion.patch index b52e4e2..262b8e6 100644 --- a/certora/mutations/010_burnAccount_logic_inversion.patch +++ b/certora/mutations/010_burnAccount_logic_inversion.patch @@ -7,7 +7,7 @@ index be21481..f22b4ed 100644 Account memory account = _accounts[controller][fundId][accountId]; - require(account.flow.incoming == account.flow.outgoing, VaultFlowNotZero()); -+ 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]; From a7d0332a584653a516fce240008cf5c9c9f0dc52 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 1 Aug 2025 18:30:26 +0200 Subject: [PATCH 27/27] Another mutation: freezeFunds when already withdrawing --- .../039_freezeFunds_when_withdrawing.patch | 13 +++++++++++++ .../039_freezeFunds_when_withdrawing.patch | 1 + 2 files changed, 14 insertions(+) create mode 100644 certora/mutations/039_freezeFunds_when_withdrawing.patch create mode 120000 certora/mutations/VaultBase/039_freezeFunds_when_withdrawing.patch diff --git a/certora/mutations/039_freezeFunds_when_withdrawing.patch b/certora/mutations/039_freezeFunds_when_withdrawing.patch new file mode 100644 index 0000000..6e70f1e --- /dev/null +++ b/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(); + } diff --git a/certora/mutations/VaultBase/039_freezeFunds_when_withdrawing.patch b/certora/mutations/VaultBase/039_freezeFunds_when_withdrawing.patch new file mode 120000 index 0000000..90da36a --- /dev/null +++ b/certora/mutations/VaultBase/039_freezeFunds_when_withdrawing.patch @@ -0,0 +1 @@ +../039_freezeFunds_when_withdrawing.patch \ No newline at end of file