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 proof exploration and display options to CLI #4245

Merged
merged 16 commits into from
Apr 16, 2024

Conversation

Baltoli
Copy link
Contributor

@Baltoli Baltoli commented Apr 13, 2024

Transfer of: runtimeverification/pyk#1043

This PR is for making it easier to work on proofs with default pyk prove ... functionalities.

  • Factor out and reuse SpecOptions in ProveOptions class.
  • Add options to pyk prove:
    • --max-iterations: control how many iterations of proof extension to do.
    • --max-depth: control the maximum number of steps to take in an execute request.
    • --save-directory: allow saving off the proof state after executing it.
    • --temp-directory: allow setting the temporary directory to use for intermediate artifacts.
    • --show-kcfg: display the resulting proof KCFG after executing the proof.
    • Handle the RuntimeError thrown by crashes of the call to kprove --dry-run ... directly and more gracefully, instead of printing a stack trace.
  • Add command pyk show which reuses a lot of the same options as pyk prove, and calls pyk prove in a way that it just loads the proof from disk and displays the KCFG.
  • Changes to the KProve.prove_rpc functionality:
    • Source many of the options from the ProveOptions class, which contains the above options and more.
    • Only initialize a CTermSymbolic (and thus an RPC server) if it's needed (will take more than 0 proof steps, and the proof isn't already passed).
    • Allow setting the prefix of the temporary file parsed to for get_claims_modules.
  • Modify a test in regression-new to exercise the new pyk prove --show-kcfg ... option.

@ehildenb ehildenb marked this pull request as ready for review April 16, 2024 16:40
pyk/src/pyk/__main__.py Outdated Show resolved Hide resolved
@rv-jenkins rv-jenkins merged commit 3f42235 into develop Apr 16, 2024
18 checks passed
@rv-jenkins rv-jenkins deleted the proof-functionalities branch April 16, 2024 21:22
rv-jenkins pushed a commit that referenced this pull request Apr 17, 2024
This PR #4172 adds
`--spec-module` to `definition_args`, but it really belongs in
`spec_args` (which this PR adds:
#4245). But now we have two
`--spec-module` arguments present, both included into the KEVM CLI,
which causes it to fail to build.

This removes the now redundant `--spec-module` there.
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