runtimeverification / runtimeverification/haskell-backend

stepf does not skip splits with succesfull nodes

Open
#3,073 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

needs-reproducing
Dominant language
Haskell
Stars
224
Forks
43
PR merge metrics
No merged PRs in 30d

Description

To reproduce:

Versions:

$ kompile --version test.k --backend haskell && kprove proof.k --haskell-backend-command 'kore-repl --version'
K version:    v5.3.60-0-gbf6c9cb9d0
Build date:   Wed May 25 19:59:21 EEST 2022
Kore version 0.60.0.0
Git:
  revision:     9767a2a2598f2f9e3ad969ac3ba0d81d1a26a9aa
  branch:       HEAD
  last commit:  Fri May 20 09:13:31 2022 -0600
Welcome to the Kore Repl! Use 'help' to get started.
...

test.k

module TEST
  imports BOOL
  imports INT

  syntax KItem ::= split(KItem) | "a" | "b"

  rule split(_:Int) => a
  rule split(K:KItem) => b ensures notBool isInt(K)

  rule a => .K
endmodule

proof.k

module PROOF
  imports TEST

  claim split(A:KItem) => .K requires isInt(A)
endmodule

Command line:

kompile --version test.k --backend haskell && kprove proof.k --haskell-backend-command 'kore-repl --version'

Repl:

step
stepf

Expected result: the current node should be '1'.
Actual result: the current node is '0'.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Reproduce the issue with test.k and proof.k using the listed kompile and kprove commands, then run step followed by stepf in the Kore REPL. Trace how stepf handles splits with successful nodes; done means the current node advances to 1 as expected.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
backend, cli
Issue type
Bug
Difficulty
3/5
Estimated time
1-2 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
42/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.