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
..
Marketplace.spec	refactor(certora): use ghost variables for `requestContext` and `slots`	2024-08-28 10:51:42 +02:00