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-04 06:13:09 +00:00
Code Issues Packages Projects Releases Wiki Activity

Minor comment changes

Browse Source
This commit is contained in:
Jochen Hoenicke 2025-07-17 12:57:53 +02:00
parent 0f09197806
commit 191b9b65b7
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
certora/specs/Vault.spec
View File

@ -38,7 +38,7 @@ hook TIMESTAMP uint256 time {
// We recompute expectedFunds in the store hooks whenever one of the dependencies changes. // 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 // 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. // 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; 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 // 7 - verified except for timeout in flow
// expectedFundsMirror is always equal to the expectedFundsDef calculation. // The expectedFunds ghost variable is always equal to the expectedFundsHelper calculation.
// This invariant is needed to prove solvency. // 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: // The expectedFunds for a single account is calculated as:
// availableBalance + designatedBalance + ((incoming - outgoing) * (flowEnd - updated)) // availableBalance + designatedBalance + ((incoming - outgoing) * (flowEnd - updated))
invariant expectedFundsMirror(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId) invariant expectedFundsMirror(VaultBase.Controller controller, VaultBase.FundId fundId, VaultBase.AccountId accountId)