You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As @anvacaru suggested, in KEVM, tests are split between several proof folders depending on the project, where each project can have a separate lemma file.
In Kontrol, there's a single Foundry project under tests/integration, while it might make sense to move, e.g., the Optimism test with a dedicate set of lemmas (will be added in #369) or CSE tests to their own folders. That would likely ensure that lemmas are only applied in relevant contracts while #442 is being investigated. In addition, it would make individual definitions more compact than the current common one, which might be easier to inspect.
At the same time, this should also be coordinated with the Haskell Backend team who use our tests for profiling.
The text was updated successfully, but these errors were encountered:
@palinatolmach & @anvacaru Once you guys discuss this issue in the Monday Standup, I would move it to "Next Up", unless someone wants to jump right on it and move it to "In Progress".
As @anvacaru suggested, in KEVM, tests are split between several proof folders depending on the project, where each project can have a separate lemma file.
In Kontrol, there's a single Foundry project under
tests/integration
, while it might make sense to move, e.g., the Optimism test with a dedicate set of lemmas (will be added in #369) or CSE tests to their own folders. That would likely ensure that lemmas are only applied in relevant contracts while #442 is being investigated. In addition, it would make individual definitions more compact than the current common one, which might be easier to inspect.At the same time, this should also be coordinated with the Haskell Backend team who use our tests for profiling.
The text was updated successfully, but these errors were encountered: