Allow introducing semantic rules in kprove #4772
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…user to specify that they want to allow new rules in a proof module
ehildenb
changed the title
|
I was waiting for more features to emerge that I need, but I think this will do for now! |
tothtamas28
approved these changes
Mar 21, 2025
| @@ -113,4 +113,10 @@ public synchronized File specFile(FileUtil files) { | |||
| description = "Allow functional claims to be printed in kore format. Use with --dry-run.", | |||
| hidden = true) | |||
| public boolean allowFuncClaims = false; | |||
|
|
|||
| @Parameter( | |||
| names = "--allow-new-rules", | |||
There was a problem hiding this comment.
I'd just call it --allow-rules to make it shorter.
| @@ -274,7 +274,7 @@ def parse_modules( | |||
| temp_dir=self.use_directory, | |||
| dry_run=True, | |||
| type_inference_mode=type_inference_mode, | |||
| args=['--emit-json-spec', ntf.name], | |||
| args=['--emit-json-spec', ntf.name, '--allow-new-rules'], | |||
There was a problem hiding this comment.
Consider adding an integration test.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Part of: runtimeverification/kontrol#977
Currently,
kprovedoes not allow including new semantic rules in the definition that is being proven, only claims andsimplificationrules. This change allows the user to set a flag--allow-new-ruleswhich disables this check. The intention is for it to be used with--dry-run, so thatkprove ...can be used just to parse some modules basically.In pyk, we add
--allow-new-rulestoKProve.parse_module(...)invocation, so that it can parse new modules that introduce semantic rules. This enables us to use those new rules in the haskell backend booster when doing proofs with Kontrol, which is key to loading loop invariants dynamically to support runtimeverification/kontrol#977.