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

Allow including lemmas dynamically into APRProver #4681

Merged
merged 29 commits into from
Nov 21, 2024

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented Nov 12, 2024

In order to include lemmas dynamically in the Kontrol prover, we need an option for passing the extra module into the APRProver so that it can be fed into the booster's add-module endpoint. This also requires being able to translate functional rules to Kore in pyk using krule_to_kore. This PR:

  • Adds the extra_module parameter to the APRProver initialization, which allows passing a new module with lemmas into the prover at initialization time. It will pass this module on to the add-module endpoint and make sure it's used on all future requests.
  • Adds the symbolic and smt-lemma attributes to the list of attributes recognized by pyk.
  • Renames KProve.get_claims_modules to KProve.parse_modules, and renames some of its parameters.
  • Adds support to specifying the sort to use in bool_to_ml_pred for converting boolean predicates to matching logic ones.
  • Makes adjustments to _krule_to_kore to make it support translating some functional/simplification rules to Kore which were not supported before (and adds tests):
    • Factors out _krule_att_to_kore method for converting attributes of KRule to kore.
    • Adds a pass to process the rule attributes a bit in krule_to_kore (eg. handle owise => priority(200) and simplification vs priority).
    • Sort the attributes before sending to Kore (for reliable ordering of the Kore output).
    • Refactors the production of Kore axiom to differentiate between semantic and functional rules, and to convert functional rules as matching-logic implies axioms.

@ehildenb ehildenb self-assigned this Nov 13, 2024
@ehildenb ehildenb marked this pull request as ready for review November 13, 2024 07:25
@ehildenb ehildenb requested a review from tothtamas28 November 13, 2024 07:25
pyk/src/pyk/kast/manip.py Outdated Show resolved Hide resolved
pyk/src/pyk/kast/outer.py Outdated Show resolved Hide resolved
pyk/src/pyk/konvert/_kast_to_kore.py Show resolved Hide resolved
pyk/src/pyk/konvert/_kast_to_kore.py Show resolved Hide resolved
@@ -255,19 +255,19 @@ def prove_claim(
depth=depth,
)

def get_claim_modules(
def parse_modules(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the module parser exposed by kprove general enough to parse an arbitrary module?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmmmm, I think it should be? But I'm not 100% on that.

@rv-jenkins rv-jenkins merged commit 8aade39 into develop Nov 21, 2024
18 checks passed
@rv-jenkins rv-jenkins deleted the custom-modules-for-proofs branch November 21, 2024 13:44
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