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