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

certora: update state changes spec now that we have vault

Browse Source
This commit is contained in:
Mark Spanbroek 2025-03-06 14:17:47 +01:00
parent 51862f67e9
commit e4348de891
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
certora/confs/StateChanges.conf
View File

@ -2,12 +2,14 @@
"files": [
"certora/harness/MarketplaceHarness.sol",
"contracts/Marketplace.sol",
"contracts/Vault.sol",
"contracts/Groth16Verifier.sol",
"certora/helpers/ERC20A.sol",
],
"parametric_contracts": ["MarketplaceHarness"],
"link" : [
"MarketplaceHarness:_token=ERC20A",
"Vault:_token=ERC20A",
"MarketplaceHarness:_vault=Vault",
"MarketplaceHarness:_verifier=Groth16Verifier"
],
"msg": "Verifying StateChanges",

2
certora/specs/StateChanges.spec
View File

@ -20,7 +20,7 @@ rule allowedRequestStateChanges(env e, method f) {
// we need to check for `freeSlot(slotId)` here to ensure it's being called with
// the slotId we're interested in and not any other slotId (that may not pass the
// required invariants)
if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) {
if (f.selector == sig:freeSlot(Marketplace.SlotId).selector) {
freeSlot(e, slotId);
} else {
f(e, args);