-
Notifications
You must be signed in to change notification settings - Fork 2
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
Updating prover #260
Updating prover #260
Conversation
kmir/k-src/mir.md
Outdated
syntax KItem ::= runLemma ( Step ) | doneLemma ( Step ) | ||
// ------------------------------------------------------- | ||
rule <k> runLemma(S) => doneLemma(S) ... </k> | ||
|
||
syntax Step ::= Bool | Int | MIRValue |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I imagine it is not ideal to have this in MIR-SYMBOLIC
, in truth I was running into errors trying to add this in any other file because of adding declarations in proof module. Exactly how to avoid that error I am unsure of.
Error occurs from `pyk` internal call to `is_terminal`
8c1b612
to
1cb379d
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good!
// imports MIR-FINALIZATION | ||
imports MIR | ||
|
||
syntax KItem ::= runLemma ( Step ) | doneLemma ( Step ) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I believe that the RPC-based prover supports functional claims directly these days, so this run / done workaround is only strictly needed for the text-based kprove
workflow. Feel free to leave it in for your own development purposes, but just making you aware!
This PR:
booster
as backend optionrunLemma
doneLemma
paradigmCTerm
MIR-SYMBOLIC
now includes moduleMIR