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