Refuse to apply sort predicates to unevaluated terms #4133
Merged
+3,493
−23
Conversation
This file contains hidden or 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
Sort predicates in K (`isMySort : KItem -> Bool`) only match on the
sort injection of the argument into `KItem`.
Paraphrased:
```
rule isMySort(inj{MySort,KItem}(VAR)) => true
rule isMySort( VAR ) => false [owise]
```
Therefore, the result is wrong in the presence of a function that may
return a super-sort of the target sort.
```
syntax SuperSort ::= MySort | SomethingElse
syntax SuperSort ::= f ( Int ) [function, total]
```
leads to a wrong matching result for a term `isMySort(f(0))`, which in kore would be
`LblisMySort(kseq{}(inj{SortSuperSort{},SortKItem{}}(Lblf{}(\dv{SortInt}("0"))),dotk{}()))`.
The matching routine would report a failed match due to the sorts
being different in the sort injections. However, the sort injection
would change as soon as f(0) gets evaluated (to an `A:MySort`).
See added test for an example K program going wrong without the fix.
The PR changes the evaluation routine to return an indeterminate match
in case it detects a sort predicate applied to a function call. The
iterative evaluation will (bottom-up) evaluate the function call in
the next round and is ultimately able to evaluate the predicate.
tothtamas28
approved these changes
Dec 8, 2025
* switch from poetry to uv (use --directory, not --project!) * remove timeout option from make test-prove-rules calls
…-environment in perf script
Member
Author
|
Holding this back for now because there are a few test failures in evm-semantics that I'd like to understand before merging. |
Member
Author
While not 100% sure which simplification was previously applied, I got all proof failures fixed by adding a new simplification in the Going ahead with the merge now. |
This was referenced Dec 14, 2025
Merged
jberthold
added a commit
that referenced
this pull request
Dec 18, 2025
#4134) The previous fix #4133 checked `isEvaluated` on the term in a sort predicate before applying rules. This is correct but leads to too many fall-backs which slow down symbolic execution when sort predicates are used in rewrite side conditions. The only case that matters is when an _unevaluated function_ is at the _head_ of the term in the sort predicate. This is now matched directly.
jberthold
added a commit
that referenced
this pull request
Jan 29, 2026
) Improves #4117 and removes temporary workaround #4133 The injection matcher was biased towards variable matching before, and returned a `Fail` prematurely if this failed. The new preference is to check for unevaluated functions that return a supersort first (to return indeterminate), before trying to match a rule variable with supersort. If the source sorts are unrelated, the match can immediately fail.
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.
Sort predicates in K (
isMySort : KItem -> Bool) only match on the sort injection of the argument intoKItem.Paraphrased:
Therefore, the result is wrong in the presence of a function that may return a super-sort of the target sort.
leads to a wrong matching result for a term
isMySort(f(0)), which in kore would beLblisMySort(kseq{}(inj{SortSuperSort{},SortKItem{}}(Lblf{}(\dv{SortInt}("0"))),dotk{}())).The matching routine would report a failed match due to the sorts being different in the sort injections. However, the sort injection would change as soon as f(0) gets evaluated (to an
A:MySort).See added test for an example K program going wrong without the fix.
The PR changes the evaluation routine to return an indeterminate match in case it detects a sort predicate applied to a function call. The iterative evaluation will (bottom-up) evaluate the function call in the next round and is ultimately able to evaluate the predicate.
Fixes #4132