Fully qualify claim labels/dependencies, include dependencies in output #842

ehildenb · 2024-01-26T00:22:47Z

We were having trouble in runtimeverification/evm-semantics#2272 selecting the correct claims because they can be unqualified by the user. This PR:

Fully qualifies all claim labels and dependency labels returned by KProve.get_claim_modules.
Makes sure that we return not only the user-selected claims, but their dependencies (unless the user turns that off), from KProve.get_claims.
Adds a test-suite for the claim selection functionality.

There is a bug in this code, and a test added (and skipped using pytest.skip()) which demonstrates a (probably minor) issue where we are not checking that claim dependencies are in a module imported by the current module.

…ims too

src/pyk/ktool/kprove.py

ehildenb · 2024-01-26T15:36:13Z

I'm redoing the logic here completely, I agree that the original way was very fragile.

…harness for claim selector functionality

…inputs

tothtamas28

Please add a docstring for the method that specifies how the module names and claim labels in spec_file relate to claim_labels and the claim labels in the result.

src/pyk/ktool/kprove.py

…epeated claim label

ehildenb · 2024-01-29T19:05:39Z

@tothtamas28 I'm going to get this merged to unblock KEVM stuffs, we can discuss more improvements as follow-up.

nwatson22

Is adding a depends with an unqualified label supposed to only work if a claim with that label exists in the current module, or should you be allowed to specify as a dependency an unqualified claim label from an imported module?

ehildenb · 2024-01-29T22:53:40Z

It should only work in the current module I suppose. But I guess overall it's ill-defined, we don't have a reference or spec for it.

Here: #842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

Here: runtimeverification/pyk#842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

…ut (runtimeverification/pyk#842) We were having trouble in runtimeverification/evm-semantics#2272 selecting the correct claims because they can be unqualified by the user. This PR: - Fully qualifies all claim labels and dependency labels returned by `KProve.get_claim_modules`. - Makes sure that we return not only the user-selected claims, but their dependencies (unless the user turns that off), from `KProve.get_claims`. - Adds a test-suite for the claim selection functionality. There is a bug in this code, and a test added (and skipped using `pytest.skip()`) which demonstrates a (probably minor) issue where we are not checking that claim dependencies are in a module imported by the current module. --------- Co-authored-by: devops <[email protected]>

…/pyk#866) Here: runtimeverification/pyk#842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

…ut (runtimeverification/pyk#842) We were having trouble in runtimeverification/evm-semantics#2272 selecting the correct claims because they can be unqualified by the user. This PR: - Fully qualifies all claim labels and dependency labels returned by `KProve.get_claim_modules`. - Makes sure that we return not only the user-selected claims, but their dependencies (unless the user turns that off), from `KProve.get_claims`. - Adds a test-suite for the claim selection functionality. There is a bug in this code, and a test added (and skipped using `pytest.skip()`) which demonstrates a (probably minor) issue where we are not checking that claim dependencies are in a module imported by the current module. --------- Co-authored-by: devops <[email protected]>

…/pyk#866) Here: runtimeverification/pyk#842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

…ut (runtimeverification/pyk#842) We were having trouble in runtimeverification/evm-semantics#2272 selecting the correct claims because they can be unqualified by the user. This PR: - Fully qualifies all claim labels and dependency labels returned by `KProve.get_claim_modules`. - Makes sure that we return not only the user-selected claims, but their dependencies (unless the user turns that off), from `KProve.get_claims`. - Adds a test-suite for the claim selection functionality. There is a bug in this code, and a test added (and skipped using `pytest.skip()`) which demonstrates a (probably minor) issue where we are not checking that claim dependencies are in a module imported by the current module. --------- Co-authored-by: devops <[email protected]>

…/pyk#866) Here: runtimeverification/pyk#842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

…ut (runtimeverification/pyk#842) We were having trouble in runtimeverification/evm-semantics#2272 selecting the correct claims because they can be unqualified by the user. This PR: - Fully qualifies all claim labels and dependency labels returned by `KProve.get_claim_modules`. - Makes sure that we return not only the user-selected claims, but their dependencies (unless the user turns that off), from `KProve.get_claims`. - Adds a test-suite for the claim selection functionality. There is a bug in this code, and a test added (and skipped using `pytest.skip()`) which demonstrates a (probably minor) issue where we are not checking that claim dependencies are in a module imported by the current module. --------- Co-authored-by: devops <[email protected]>

…/pyk#866) Here: runtimeverification/pyk#842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <[email protected]>

ehildenb added 4 commits January 25, 2024 23:37

ktool/kprove: make sure to fetch claim dependencies in KProve.get_cla…

9fe3162

…ims too

ktool/kprove: qualify all claim labels at load time with module name

d5aabd0

ktool/kprove: sentences without dependencies shouldnt be asked for them

4d11da3

Merge 4d11da3 into 2042982

077eb7e

ehildenb self-assigned this Jan 26, 2024

Set Version: 0.1.599

4f08e57

ehildenb changed the title ~~Fully qualify claim labels and dependencies when loading from file~~ Fully qualify claim labels/dependencies, include dependencies in output Jan 26, 2024

ehildenb mentioned this pull request Jan 26, 2024

Update dependency: deps/pyk_release runtimeverification/evm-semantics#2272

Merged

ehildenb marked this pull request as ready for review January 26, 2024 00:57

ehildenb requested a review from tothtamas28 January 26, 2024 00:57

tothtamas28 reviewed Jan 26, 2024

View reviewed changes

ehildenb and others added 14 commits January 26, 2024 16:07

ktool/kprove: correctly qualify claim labels passed on CLI

a36d3e4

ktool/kprove: let worklist skip existing claim labels

00cf6b7

ktool/kprove: refactor how claim labels are processed

04c961d

Merge remote-tracking branch 'upstream/master' into claim-labels

e5af7e8

Merge e5af7e8 into 23496d9

885d599

Set Version: 0.1.601

8921a1c

ktool/kprove: correctly exclude claim labels

81309bd

tests/{k-files/multi-claim-spec,kprove/test_get_claims}: add testing …

426ed7a

…harness for claim selector functionality

tests/{k-files/multi-claim-spec,kprove/test_get_claims}: update test …

a411e46

…inputs

ktool/kprove: make sure returned claims have qualified names

2acfdda

ktool/kprove: remove unused function

46a62d7

tests/kprove/test_get_claims: use pytest.skip() to skip bad test

925649a

tests/test_get_claims: correct style

3856863

ktool/kprove: no need for f-string

fdd4010

tothtamas28 reviewed Jan 29, 2024

View reviewed changes

src/pyk/ktool/kprove.py Outdated Show resolved Hide resolved

src/pyk/ktool/kprove.py Outdated Show resolved Hide resolved

ehildenb added 3 commits January 29, 2024 17:12

Merge remote-tracking branch 'upstream/master' into claim-labels

9ae42c9

tests/integration/{test_get_claims,multi-claim-spec.k}: add test of r…

bd9774c

…epeated claim label

ktool/kprove: simplify labelling by only accepting user-labeled claims

a6d8cd2

ehildenb and others added 2 commits January 29, 2024 11:07

Merge a6d8cd2 into 7af0afe

2beb0ea

Set Version: 0.1.602

b9b1164

ehildenb requested a review from tothtamas28 January 29, 2024 19:03

ehildenb added 2 commits January 29, 2024 19:04

Merge remote-tracking branch 'upstream/master' into claim-labels

aeb5c17

Merge aeb5c17 into 7f75017

ee94de6

ehildenb requested a review from nwatson22 January 29, 2024 19:05

Set Version: 0.1.603

25ea5b2

nwatson22 approved these changes Jan 29, 2024

View reviewed changes

Merge remote-tracking branch 'upstream/master' into claim-labels

ecfed2e

ehildenb added the automerge label Jan 30, 2024

ehildenb and others added 2 commits January 30, 2024 23:55

Merge ecfed2e into 5fae467

bad21df

Set Version: 0.1.606

b40c390

rv-jenkins merged commit 14c565a into master Jan 31, 2024

rv-jenkins deleted the claim-labels branch January 31, 2024 00:32

ehildenb mentioned this pull request Feb 7, 2024

Fix claim selection process for unlabeled claims #866

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fully qualify claim labels/dependencies, include dependencies in output #842

Fully qualify claim labels/dependencies, include dependencies in output #842

Uh oh!

ehildenb commented Jan 26, 2024 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ehildenb commented Jan 26, 2024

Uh oh!

tothtamas28 left a comment

Uh oh!

Uh oh!

Uh oh!

ehildenb commented Jan 29, 2024

Uh oh!

nwatson22 left a comment

Uh oh!

ehildenb commented Jan 29, 2024

Uh oh!

Uh oh!

Fully qualify claim labels/dependencies, include dependencies in output #842

Fully qualify claim labels/dependencies, include dependencies in output #842

Uh oh!

Conversation

ehildenb commented Jan 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ehildenb commented Jan 26, 2024

Uh oh!

tothtamas28 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ehildenb commented Jan 29, 2024

Uh oh!

nwatson22 left a comment

Choose a reason for hiding this comment

Uh oh!

ehildenb commented Jan 29, 2024

Uh oh!

Uh oh!

ehildenb commented Jan 26, 2024 •

edited

Loading