Prover is unable to prove a simple claim

[ehildenb]

The following definition fails to be proven (or take any steps) with the prover:

module ITEMS-SYNTAX
  imports DOMAINS-SYNTAX

  syntax Item ::= "A"
  syntax Items ::= List{Item, "|"}

endmodule

module ITEMS
  imports ITEMS-SYNTAX
  imports K-EQUAL
  imports INT

  configuration <k> $PGM:Items </k>

  rule <k> _ | IS => IS ... </k>

endmodule

module TEST-SPEC
  imports ITEMS

  claim <k> _:Items => .Items ... </k>
endmodule

To reproduce (K 5.1.156):

% kompile --version
K version:    5.1.165
Build date:   Fri Aug 27 00:41:16 UTC 2021

% kompile --backend haskell test.k --main-module ITEMS

% kprovex test.k --spec-module TEST-SPEC
kore-exec: [329391] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/dev/src/k/test.k:23:9-23:39
  #Not ( {
    _0
  #Equals
    .Items
  } )
#And
  <k>
    _0:Items ~> _DotVar1 ~> .
  </k>

Intuitively, what I expect to happen is this:

• The prover looks for rules that can apply to the LHS of the claim. The rule _ | IS => IS should be able to apply, which collects the path condition that #Exists I:Item . #Exists IS:Items . { _0:Items #Equals I | IS }, and then the prover can co-inductively apply the claim to the new state which discharges the proof.
• A second path is produced which has #Not (#Exists I:Item . #Exists IS:Items . { _0:Items #Equals I:Item | IS:Items }) (the remainder from applying the rule in step 1). I'm not sure if this step is possible, but then what the prover should do is show that this path condition means that _0:Items #Equals .Items (would require reasoning over all the available constructors). Then the prover can see that the proof immediately follows.

So I'm not sure if the second reasoning step (where we reason over available constructors to determine that _0:Items) is a desirable thing to add, but at the very least it seems that given the initial LHS, it should at least try the rule given in the semantics, which I cannot see that it's even attempting this rule.

Attached is the generated bug-report for this proof: test.tar.gz

[dopamane]

@ana-pantilie @andreiburdusa Unable to reproduce when running kompile --backend haskell test.k --main-module ITEMS, error message:

[Error] Inner Parser: Parse error: unexpected token 'A'.
        Source(/home/davos/github.com/kframework/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)
        Location(1079,8,1079,9)
[Error] Inner Parser: Parse error: unexpected token 'A' following token '('.
        Source(/home/davos/github.com/kframework/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)
        Location(1081,9,1081,10)
[Error] Compiler: Had 2 parsing errors.

$ kompile --version
K version:    v5.1.250-0-g07918e142fBuild date:   Mon Nov 08 09:38:38 PST 2021

Using master Kore: d4239d97f5b53188460e7399b683111b5687661c

[ana-pantilie]

That parse error is weird, it appears like there's something wrong with domains.k. Do you get the same error when kompiling other semantics?

[andreiburdusa]

I got the same error as David. But I'm able to kompile other definitions like lesson-06-a.k

$ kompile --backend haskell lesson-06-a.k --main-module LESSON-06-A
[Warning] Compiler: Could not find main syntax module with name
LESSON-06-A-SYNTAX in definition.  Use --syntax-module to specify one. Using
LESSON-06-A as default.

$ kompile --version
K version:    v5.1.250-0-g07918e142
Build date:   Mon Nov 08 14:24:51 EET 2021

[andreiburdusa]

Not sure if this is helpful, but I was able to reproduce the issue by removing imports INT and then I found a simpler example which I think shows the same behavior.

test.k:

module XY-SYNTAX
  imports DOMAINS-SYNTAX

  syntax XY ::= "X" | "Y"

endmodule

module XY
  imports XY-SYNTAX
  imports K-EQUAL

  rule <k> X => Y ... </k>

endmodule

module TEST-SPEC
  imports XY

  claim <k> _:XY => Y ... </k>
endmodule

How to run:

$ kompile --backend haskell test.k --main-module XY
$ kprovex test.k --spec-module TEST-SPEC
kore-exec: [334344] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/andrei/Desktop/issue-2822/new/test.k:19:9-19:31
  #Not ( {
    _0
  #Equals
    Y
  } )
#And
  <k>
    _0:XY ~> _DotVar1 ~> .
  </k>

[ana-pantilie]

@andreiburdusa could you explain what you think should happen every execution step for your minimized example?

[andreiburdusa]

If we don't have reasoning over all the available constructors I don't see why the rule should be tried. My impression is that the current behavior is correct.

[virgil-serbanuta]

I hope that what I remember is correct (though, most likely, the HB team can easily check whether most of the things below are true):

The Haskell backend does not try to continue running after the RHS of the claim unifies with the current configuration, even when it's a "partial" unification (i.e. a configuration variable becomes more concrete) like this one.

I think that I argued with Tom that we should continue because of cases like this one, but I think that Tom was right - usually, continuing execution would make it harder to debug the much more common case when reaching the final configuration does, indeed, mean that we want to stop execution (though there are ways to mitigate some of the issues, e.g. 'step n' could stop when the RHS unifies with the configuration, also notifying the user; also, graph could color the configuration differently or something).

It could be argued that we could try to distinguish between [being able to continue because unification was partial] and [continuing because unification worked as expected, but the requires clause was not fully satisfied], and that we should try to continue in the former case, but not the latter, but, if that seems like an interesting idea, we should probably try to make sure that it actually makes sense.

[ana-pantilie]

Thank you @virgil-serbanuta , I think you're correct. I will also point out the code which does this detection: https://github.com/kframework/kore/blob/33c83f95f16b12170d6248d2c1525d02fa9fa031/kore/src/Kore/Reachability/Claim.hs#L591. That is the case I believe is getting triggered with, at least, @andreiburdusa 's example.

Your proposal is very interesting! Let's think about it, because I agree that this proof getting stuck is very counterintuitive.

@andreiburdusa I don't understand, why do you think that the rule itself shouldn't apply? I mean, I'd expect it to unify and branch on the remainder. So, one branch would be Var #Equals x, the rule applies and we get to y, the other branch would be #Not (Var #Equals x). In theory, we have no-junk axioms for sorts and their constructors. The one for sort XY should help prove that Var can only be y. Then, the claim is proven on this branch as well. To make sure this understanding is not incorrect, could you look for the code which does this reasoning?

[ana-pantilie]

@andreiburdusa https://github.com/kframework/kore/blob/master/docs/2020-06-17-Checking-Implication.md