search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
48 stars 5 forks source link

Consider splitting integration tests between several folders #458

Open palinatolmach opened 6 months ago

palinatolmach commented 6 months ago

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 https://github.com/runtimeverification/kontrol/pull/369) or CSE tests to their own folders. That would likely ensure that lemmas are only applied in relevant contracts while https://github.com/runtimeverification/kontrol/issues/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.

yale-vinson commented 6 months ago

@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".