4 Commits

Author	SHA1	Message	Date
Andrea Franz	1e5c8df2fb	chore(certora): contract balance increases when new storage requests are added	2024-08-27 16:37:31 +02:00
r4bbit	ebdf9ed366	fix(certora): fix rule that missed slots == number of issed periods	2024-08-23 14:01:43 +02:00
r4bbit	1d36256230	chore(certora): add invariant that proofs cant be missing when in period ... This invariant verifies that any given proof cannot be marked as missing if the slot period has not passed yet.	2024-08-13 09:39:29 +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