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-07 07:43:08 +00:00
Code Issues Packages Projects Releases Wiki Activity

certora: remove check on ERC20 token

Browse Source 
No need to test the token itself
This commit is contained in:
Mark Spanbroek 2025-03-06 10:22:46 +01:00
parent 2d21d65624
commit 51862f67e9
1 changed files with 0 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
certora/specs/Marketplace.spec
View File

@ -3,8 +3,6 @@ import "./shared.spec";
using ERC20A as Token;
methods {
function Token.balanceOf(address) external returns (uint256) envfree;
function Token.totalSupply() external returns (uint256) envfree;
function publicPeriodEnd(Periods.Period) external returns (Marketplace.Timestamp) envfree;
function generateSlotId(Marketplace.RequestId, uint64) external returns (Marketplace.SlotId) envfree;
}
@ -13,18 +11,6 @@ methods {
| Ghosts and hooks |
--------------------------------------------*/
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sload uint256 balance Token._balances[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
sumOfBalances = sumOfBalances - oldValue + newValue;
}
ghost Marketplace.Timestamp lastBlockTimestampGhost;
hook TIMESTAMP uint v {
@ -147,9 +133,6 @@ function slotAttributesAreConsistent(env e, Marketplace.SlotId slotId) {
| Invariants |
--------------------------------------------*/
invariant totalSupplyIsSumOfBalances()
to_mathint(Token.totalSupply()) == sumOfBalances;
invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
currentContract.requestState(e, requestId) == Marketplace.RequestState.Started => to_mathint(currentContract.getRequest(e, requestId).ask.slots) - slotsFilledGhost[requestId] <= to_mathint(currentContract.getRequest(e, requestId).ask.maxSlotLoss);