optimism icon indicating copy to clipboard operation
optimism copied to clipboard

Published 20 hours ago • verified publisher icon ethereum-optimism

Final version for Kontrol pausability proofs

Open JuanCoRo opened this issue 1 year ago • 0 comments

Description

Building on #9183, this PR wraps up the existing pausability proofs by adding the following:

  • Native symbolic support for arguments of type bytes and bytes[]
  • Replace mockCall workaround with the vm.mockCall cheatcode
  • Replace startPrank workaround with the appropriate vm.prank cheatcode

Tests

No additional tests are added so far. This PR modifies the existing proofs to include all the latest and necessary improvements.

Additional context

Before this PR, a number of workarounds were in place to have these proofs pass. These workarounds didn't threaten the soundness of the proofs, but they affected long-term maintainability, execution performance, and the generality of the proofs.

JuanCoRo avatar Feb 13 '24 20:02 JuanCoRo