Error about claim with universally-quantified var on RHS must show var names

[denis-bogdanas]

One of Haskell backend errors looks like this:

Error:
  module 'GEN-B9B4CAC69636F5AA489AA9CCD4116C5719559854D98BBDCEAC41C2EDC89C0D03-TO-7ABB79081A802ABFBA809B6B97DA08A1BDD820D0A54525EE76FE0EC90D4542E0-SPEC':
  claim declaration:
    Found claim with universally-quantified variables appearing only on the right-hand side

It would be preferred if error also mentions variable name and the claim location.
Also, for all backend crashes like this we would prefer different exit codes for easy debugging and tool integration. At very least, backend crash due to out of memory must give a different exit code than a functional error.

[denis-bogdanas]

kore-exec-flopper-kick1.tar.gz

[JKTKops]

If the universal appears in the source of the claim, the frontend should probably be catching this one. Everett would like to discuss in the frontend meeting. @radumereuta

@denis-bogdanas Can we get the K source of the claim? The Kore source is in the bug report, but we need the K source to establish where in the pipeline the bug actually is.

[denis-bogdanas]

flopper-kick-spec.k

[radumereuta]

We can talk about this at the meeting.
@JKTKops I could still use some help from the backend, since I have no idea what went wrong here just by looking at the claim.
@denis-bogdanas in order to be able to debug this in the front end I will need the entire definition. If this is part of the erc20-verification repo, then just details about how to set it up.

[ana-pantilie]

The backend needs to give more information. After that is done, transfer issue to the frontend.

[ana-pantilie]

Probably is a syntax validation error https://github.com/runtimeverification/haskell-backend/tree/master/kore/src/Kore/Validate

[Sereja313]

@ana-pantilie I managed to reproduce this error.
backend version:

Kore version 0.60.0.0
Git:
  revision:	74bc7a963a825d0f0f034b5d3412dc59448e51bb (dirty)
  branch:	master
  last commit:	Tue Feb 7 05:02:49 2023 -0700

[radumereuta]

Can you post the steps you took to reproduce it?
It would be helpful to fix the issue in the front-end as well.

[Sereja313]

I just ran ./kore-exec.sh from the attached archive and got the same error as in the issue description:

λ ./kore-exec.sh                                                        
kore-exec: [1738164] Error (ErrorVerify):
    Error:
      module 'GEN-B9B4CAC69636F5AA489AA9CCD4116C5719559854D98BBDCEAC41C2EDC89C0D03-TO-7ABB79081A802ABFBA809B6B97DA08A1BDD820D0A54525EE76FE0EC90D4542E0-SPEC':
      claim declaration:
        Found claim with universally-quantified variables appearing only on the right-hand side
Created bug report: kore-exec.tar.gz

The error still has no variable name or claim location information.

I'm just going through needs-reproducing issues and trying to reproduce them to find which ones are outdated and which ones are still relevant.

Sorry, I think I can not provide any useful information on this issue.