10 Commits

Author	SHA1	Message	Date
Aleksander Kryukov	d0e4208854	tmp save	2025-06-12 15:59:40 +02:00
Aleksander Kryukov	3cda5a0ce0	adding CVLStatus to use in quantifiers	2025-06-12 15:59:40 +02:00
Aleksander Kryukov	c35b8b6d74	attempt to use sum ghost	2025-06-12 15:59:40 +02:00
Aleksander Kryukov	ae94d1ebf3	try to hook on _funds. fixed required	2025-06-12 15:59:40 +02:00
Mark Spanbroek	e4348de891	certora: update state changes spec now that we have vault	2025-06-11 16:31:58 +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
r4bbit	0b39274ed5	refactor(certora): extract allowedRequestStateChanges rule into own ... file Closes #192	2024-10-21 15:36:29 +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