[K-Bug] kprove generates kore claims that do not correspond to the K version
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 32/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers
Research direction
Reproduce the issue with kompile a.k --backend haskell && kprove spec.k, using the supplied a.k and spec.k definitions. Inspect the generated Kore claim and its RHS sort; done means the claim is rejected as invalid or kprove proves it without producing a term outside MyList.
Written by the indexing model from the issue text.
Description
What component is the issue in?
None
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v6.3.45-0-g736e297aa9-dirty
Operating System
Linux
K Definitions (If Possible)
a.k:
module A
imports BOOL
imports BYTES
imports INT
syntax MyList ::= List{Int, ""}
syntax A ::= a(KItem) | b(KItem)
rule a(_:Int L:MyList) => b(L)
endmodule
spec.k:
module SPEC
imports A
claim <k> a(1 2) => b(2:MyList) ... </k>
endmodule
Steps to Reproduce
kompile a.k --backend haskell && kprove spec.k
Note that the Kore RHS of the claim contains this subterm, which has nothing of sort MyList as specified in the claim.
Lblb'LParUndsRParUnds'A'Unds'A'Unds'KItem{}(
inj{SortInt{}, SortKItem{}}(
\dv{SortInt{}}("2")
)
)
Expected Results
Either there should be an error in the claim file, or kprove should prove the claim.
- Dominant language
- Python
- Stars
- 591
- Forks
- 163
- PR merge metrics
- No merged PRs in 30d
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from runtimeverification/k
-
runtimeverification/k#4939 · 1 assignee ·
-
Concolic Explorer Open
Difficulty 5/5 Over a week Newbie friendliness 32/100
runtimeverification/k#4937 ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
runtimeverification/k#4936 ·
-
type:epic
runtimeverification/k#4934 · 4 comments · 1 assignee ·
-
runtimeverification/k#4924 · 1 assignee ·
All issues in runtimeverification/k
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
bancolombia/sentinel#23 ·
-
test md OpenCI
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
-
integration:quickjs org:external priority:backlog topic:code-interpreter topic:middleware type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
langchain-ai/deepagents#6450 ·
-
bug client
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100