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

..

confs

chore(certora): set MarketplaceHarness as parametric_contract config value

2024-08-19 14:07:05 +02:00

harness

refactor(certora): use ghost variables for requestContext and slots

2024-08-28 10:51:42 +02:00

helpers

Set up certora and implement first rules (#122)

2024-07-24 18:50:18 +02:00

specs

refactor(certora): use ghost variables for requestContext and slots

2024-08-28 10:51:42 +02:00