kprove crashes on claims without <k> tag or with repeated <k> tags

[jberthold]

With K version 6.2.24 (and probably others after 6.0.181), the command kprove may crash in one of two different ways when trying to process claims that used to work in earlier versions.

claim without <k> tags around the claim

spec-no-k-tag.k

module SPEC-NO-K-TAG
  imports TEST

  claim (_X => ?_) ~> .K
endmodule

The command kprove spec-no-k-tag.k crashes when calling the backend kore-exec because the generated kore contains null where a Sort should be.

$ kprove spec-no-k-tag.k 
kore-exec: [37802] Error (ErrorVerify):
    Error:
      module 'SPEC-NO-K-TAG':
      claim declaration:
      \implies (/tmp/.kprove-2024-02-16-13-48-35-222-904ec37e-072a-4a20-b563-6c83b247e774/spec.kore 10:20):
      (/tmp/.kprove-2024-02-16-13-48-35-222-904ec37e-072a-4a20-b563-6c83b247e774/spec.kore 10:20):
        Sort variable null not declared.

Using `kprove spec-no-k-tag.k --dry-run`, one can inspect the intermediate kore from the claim.

$ kprove spec-no-k-tag.k --dry-run
kore-exec /home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/./test-kompiled/definition.kore --module TEST --prove /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/spec.kore --spec-module SPEC-NO-K-TAG --output /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/result.kore

$ cat /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/spec.kore
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)")]
module SPEC-NO-K-TAG

// imports
import TEST []


// claims
// claim _X=>?_Gen0 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3761007019618ccc9ec3f08d7970ea9fd82125e826fed962533b93a9bf5565cc), org.kframework.attributes.Location(Location(4,9,4,25)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  claim{} \implies{null} (
      \and{null} (
      \top{null}(), Var'Unds'X:SortK{}), weakAlwaysFinally{null} (
       \exists{null} (Var'QuesUnds'Gen0:SortK{}, 
      \and{null} (
      Var'QuesUnds'Gen0:SortK{}, \top{null}()))))
  [UNIQUE'Unds'ID{}("3761007019618ccc9ec3f08d7970ea9fd82125e826fed962533b93a9bf5565cc"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(4,9,4,25)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]

endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,5,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)")]

Claim using the tags <k> twice

spec-repeated-k-tag.k

module SPEC-REPEATED-K-TAG
  imports TEST

  claim <k> _X </k> => <k> ?_ </k>
endmodule

The command kprove spec-repeated-k-tag.k fails in the frontend with a NoSuchElement exception.

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(NoSuchElementException: None.get)

---

The definition file for both is an empty test.k

module TEST
endmodule

$ kompile --backend haskell test.k

[Baltoli]

Running an automatic bisection between 9cc71d6 (master at time of writing) and af105e4 (v6.0.181) with the following setup (where Jost's example above is in ~/code/scratch on my machine):

repro.sh:

#!/usr/bin/env bash

set -euxo pipefail

git submodule update --init --recursive
mvn package -DskipTests || exit 125

BIN=/Users/brucecollie/code/k/k-distribution/target/release/k/bin

cd ~/code/scratch
rm -rf *-kompiled
"$BIN/kompile" --backend haskell test.k || exit 125
"$BIN/kprove" spec-repeated-k-tag.k```

```console
$ git bisect start HEAD v6.0.181
$ git bisect run ./repro.sh

[Baltoli]

As I suspected, the bad change is: #3812 (for both broken specs). I'll investigate further on Monday

[Baltoli]

I've done a time-boxed investigation of this based on #3812, where Radu did indeed observe that ModuleToKore breaks in a few different ways after the changes there. The underlying causes here are:

• (no cell) The implementation of getRuleInfo doesn't accommodate for the LHS of a rule being a variable with no surrounding production; the specific error here goes away if you modify the code there to just infer variables to have sort K. This doesn't seem sound or hygienic to me.
• (duplicate cells) This case is more complicated; it seems to break a few different places in the compilation pipeline that rely on cells having been concretized properly before later steps are run. It's not clear to me what a correct fix is here; I suspect that it will involve touching a lot of ModuleToKore.

The real issue is that we have a tension between two different designs / uses here:

• The kprove tool operates at the KORE level, and requires the full compilation pipeline to have been run in order to get sound KORE generated.
• The pyk-based prover is not doing this, but is rather constructing claims at the JSON KAST level and so doesn't need nor want the full compilation pipeline to have been run.

I'm not sure what the moral solution is; we probably need to either more explicitly bifurcate (and document!) the behaviour of the compilation pipeline in JSON / KORE modes, or add a check that requires claims have a surrounding cell.

[jberthold]

Thanks for investigating this! It looks to me as if these changes to require the <k> tags in a certain shape were made for a good reason but they result in a few problems by not catching common mistakes.

• (no cell) The implementation of getRuleInfo doesn't accommodate for the LHS of a rule being a variable with no surrounding production;

Just FWIW in the test that I had to change to work around the Sort variable null not declared error ("no cell"), there isn't a single variable on the LHS but rather a symbol application (with a hooked symbol).

What should definitely not happen is the compiler failing or the compiler producing output that the backend fails on. Maybe this can be avoided just by adding some additional checks (rather than trying to accept the input at any cost).

[Baltoli]

... isn't a single variable on the LHS ...

Indeed; the code here includes a few cases (#as, applications) but excludes everything else implicitly. Variables are just one such instance.

What should definitely not happen is the compiler failing or the compiler producing output that the backend fails on.

100% agree; just need to figure out what those extra checks or restrictions look like in practice.

[Baltoli]

I think we want to add a --legacy-claims flag to kprove to reinstate the old behaviour.