runtimeverification / runtimeverification/haskell-backend

Flaky behavior on `simplify` endpoint

Open
#3,761 1 comment 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Haskell
Stars
224
Forks
43
No merged PRs in 30d

Description

Related:

  • #3730
  • #3731
  • runtimeverification/pyk#1070

runtimeverification/k#4146 removed some symbol attributes from definition.kore (format, color, ...). As a result, TestMiniKEVM started failing in runtimeverification/pyk#1070 (only for the old backend).

The same test failed earlier after adding the symbol attribute to some productions in runtimeverification/k#4024. Then, the fix was to pin hashable to a given version in #3732.

Based on this, I think there might be a hash set or similar somewhere in the code base whose iteration order somehow influences simplify responses.

Bug reports:

First divergent reponse:

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

Start with the TestMiniKEVM failure in runtimeverification/pyk#1070 and compare the attached old and new simplify request/response archives, beginning at the first divergent response. Trace the simplify endpoint's handling of iteration order and the related definition.kore symbol attributes, then reproduce the failure and confirm that responses are stable across the reported versions.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
api, backend
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
30/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.