logos-storage/logos-storage-contracts-eth
1
0
Fork 0
mirror of https://github.com/logos-storage/logos-storage-contracts-eth.git synced 2026-01-05 06:43:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

check in the latest code

Browse Source
This commit is contained in:
Aleksander Kryukov 2025-06-30 23:59:10 +01:00 committed by Jochen Hoenicke
parent 2e675d31ed
commit d99499b1cf
1 changed files with 84 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
certora/specs/Vault.spec
View File

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