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

Add option to use booster-dev binary for execution of proofs #2466

Merged
merged 13 commits into from
Jun 7, 2024

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented Jun 5, 2024

Blocked on: #2468

Currently, we have the option to add --use-booster to enable using the booster in KEVM proofs, and in the proof test-suite. This enables --use-booster-dev, which uses the development version of the booster (which disables fallback to kore entirely).

This is blocked on getting the booster-dev binary exported in the K nix package.

  • Add option --use-booster-dev to kevm prove ...
  • Enable the same option for the test_pyk_prove test harness.
  • Start a failing list with all the currently failing tests using the booster-dev backend.
  • Enable running this list on CI, so we can begin to tackle it.

Currently single-digit proofs are passing on this version of the job.

@ehildenb ehildenb self-assigned this Jun 5, 2024
@ehildenb
Copy link
Member Author

ehildenb commented Jun 5, 2024

Ping @goodlyrottenapple .

@goodlyrottenapple
Copy link
Contributor

this can be merged once runtimeverification/k#4424 makes it through

@ehildenb ehildenb marked this pull request as ready for review June 7, 2024 16:43
@ehildenb
Copy link
Member Author

ehildenb commented Jun 7, 2024

@goodlyrottenapple you can produce bug reports for all the executions that are failing with:

  • Empty the file tests/failing-symbolic.haskell-booster-dev (except leave 1 line, perhaps, to avoid weird errors).
  • Run make test-prove-pyk PYTEST_PARALLEL=8 PYTEST_ARGS='-vv --timeout=7200 --use-booster-dev --bug-report-dir dev-bug-reports' PYTEST_MAXFAIL=5000

This should produce bug reports for all the executions, and you can run each request and see which ones cause crashes in the backend, and triage them into a list.

@ehildenb ehildenb requested a review from nwatson22 June 7, 2024 19:01
@rv-jenkins rv-jenkins merged commit 908b61b into master Jun 7, 2024
12 checks passed
@rv-jenkins rv-jenkins deleted the conf-test-booster-dev branch June 7, 2024 21:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants