Generate equations for `==K`
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 25/100
Research direction
The issue names the Haskell backend, LLVM backend, Booster, ==K, and #Equals, but no files, tests, or entry points. Start by tracing how ==K is handled in the Haskell and LLVM backends, then determine whether generated equations can replace that built-in behavior and what inherent limitations apply.
Written by the indexing model from the issue text.
Description
We have recently noticed that both the haskell backend and llvm backend hook the ==K symbol directly (LLVM) or rewrite to #Equals (haskell backend), both of which are internal simplification/evaluation strategies which are opaque to the user (i.e. the question of why some ... ==K ... term was simplified to something else cannot be traced easily in the haskell backend, because we simplified to { ... #Equals ... } and afterwards, no kore rules were applied because the internal logic of #Equals was used). In booster, we are trying to minimise the amount of built in behaviour and it would make sense for the backend to use generated equations for ==K, rather than rely on a builtin simplifier. Would it be possible to generate rules for ==K or is there some inherent limitation that would prevent us form doing this?
- 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