search

codex-storage / codex-contracts-eth

Ethereum smart contracts for Codex
Other
6 stars 9 forks source link

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

Closed 0x-r4bbit closed 1 month ago

0x-r4bbit commented 1 month ago

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