6 Commits

Author SHA1 Message Date
Mark Spanbroek
cbe52b4934 certora: remove configuration that fixes solidity to solc8.28
Reason: makes certoraRun in the CI fail
2025-06-12 16:55:53 +02:00
Aleksander Kryukov
d0e4208854 tmp save 2025-06-12 15:59:40 +02:00
Mark Spanbroek
2d21d65624 certora: update marketplace spec now that we have vault
- changes to marketplace constructor
- we no longer have _marketplaceTotals
- timestamps have their own type now
- freeSlot no longer takes payout addresses
- slot state 'Paid' no longer exists
- freeSlot can be invoked more than once now
- a failed request no longer ends immediately
2025-06-11 16:31:58 +02:00
Andrea Franz
92ab1e50dd chore(certora): set MarketplaceHarness as parametric_contract config value 2024-08-19 14:07:05 +02:00
r4bbit
2e3f775a0d chore: formally verify request state changes
This commit adds CVL rule that formally verifies the state changes of
any given request in relation to the functions of the contract that can
cause them.

Closes #128
2024-08-12 15:26:59 +02:00
r4bbit
688a8ed929
Set up certora and implement first rules (#122)
Co-authored-by: 0xb337r007 <0xe4e5@proton.me>
Co-authored-by: Adam Uhlíř <adam@uhlir.dev>
2024-07-24 18:50:18 +02:00