Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make booster the default #75

Merged
merged 25 commits into from
Dec 15, 2023
Merged

Make booster the default #75

merged 25 commits into from
Dec 15, 2023

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented Oct 4, 2023

EDIT by @palinatolmach: this PR only makes --use-booster default and adds --no-use-booster (both for Kontrol executable and tests) which can be used to switch to legacy backend. This PR doesn't disable legacy tests on CI for integration (considering that the the longer running ones were disabled by #171 and, as mentioned in the comment, there're tests that are skipped if the booster is used, the updated output is not compared for booster runs, and there's discrepancy between backends on the output of test_foundry_auto_abstraction). I factored disabling legacy CI tests into a separate issue.

Original PR description by @ehildenb:

The tests on the legacy backend take very long, and we are already testing conformance in KEVM.

Any discrepancies between booster and legacy should be upstreamed as KClaim style tests to KEVM.

  • Make it so --use-booster is default, pass --no-use-booster to disable (both main executable and tests).
  • Disables legacy tests on CI, for integration, maintain them for profiling (faster).
  • Updates timeouts.
  • Update required status checks.

@ehildenb ehildenb self-assigned this Oct 4, 2023
@nwatson22
Copy link
Member

Before we disable the booster tests, there is a discrepancy between the output of test_foundry_auto_abstraction when the booster is used vs. not. This is mostly due to ensures and requires conditions being ordered differently, also sometimes using the booster seems to add ensures clauses to rule blocks in generated modules where the legacy backend does not, for example here.

There are also other tests in test_foundry_prove.py that are skipping if the booster is used. I guess in the case of test_foundry_kompile it was because there is no need to run it with both.

@ehildenb
Copy link
Member Author

ehildenb commented Oct 5, 2023

I don't think there are any remaining tests that skip if the booster is turned on, are there?

@lucasmt
Copy link
Contributor

lucasmt commented Oct 5, 2023

From the perspective of the current engagement, we have been mostly using the booster, but recently we had to revert to the legacy backend for one of the proofs because of an expression that the booster was not simplifying. However, this shouldn't be a problem as long as there is still an option to switch back to the legacy backend if necessary.

Regarding disabling the tests, I would prefer if we could wait until the engagement is over, just to be safe. If we need to temporarily switch back to the legacy backend, I would prefer not to risk the possibility of an update that breaks something having sneaked by undetected. But that depends on how likely it would be for that to happen.

@yale-vinson yale-vinson added the enhancement New feature or request label Oct 11, 2023
@palinatolmach palinatolmach self-assigned this Nov 14, 2023
@palinatolmach
Copy link
Collaborator

@ehildenb currently, after an update, this PR doesn't disable legacy tests — instead, the longer running ones are disabled by #171, and I'm wondering if that's sufficient. Please let me know if you think we should disable all legacy tests, and I'll bring that change back. ty!

@palinatolmach palinatolmach changed the title Make booster the default, disable tests on legacy backend Make booster the default, ~~disable tests on legacy backend~~ Nov 14, 2023
@palinatolmach palinatolmach changed the title Make booster the default, ~~disable tests on legacy backend~~ Make booster the default, ~disable tests on legacy backend~ Nov 14, 2023
@palinatolmach palinatolmach changed the title Make booster the default, ~disable tests on legacy backend~ Make booster the default Nov 14, 2023
@palinatolmach palinatolmach marked this pull request as ready for review December 14, 2023 16:16
@rv-jenkins rv-jenkins merged commit 921005c into master Dec 15, 2023
11 checks passed
@rv-jenkins rv-jenkins deleted the booster-default branch December 15, 2023 08:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
automerge enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants