Mark Spanbroek
44fcab0fc5
update solidity to version 0.8.28
2025-01-22 11:59:51 +01:00
Andrea Franz
3a074abd20
chore(certora): verify possible slot state transitions
2024-09-30 12:53:06 +02:00
r4bbit
bba8736132
refactor(certora): use ghost variables for requestContext and slots
...
Instead of having additional harness code in `MarketplaceHarness` to
access fields in `requestContext` and `slots` objects, this introduces
dedicated ghost variables that keep track of the field changes and let
us read the values from there.
Prover run: https://prover.certora.com/output/6199/8343693dfc3f4ca38435f5aa10fa2345?anonymousKey=db5eaee6c688651132d1671919fb73544affa269
Closes #165
2024-08-28 10:51:42 +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
