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-03 13:53:10 +00:00
Code Issues Packages Projects Releases Wiki Activity

updated solvency for review

Browse Source
This commit is contained in:
Aleksander Kryukov 2025-06-13 15:50:05 +01:00 committed by Jochen Hoenicke
parent a217a0476d
commit 7ca5c8eb77
1 changed files with 37 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
certora/specs/Vault.spec
View File

@ -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()