Apply claim LHS substitution to RHS after simplification

[virgil-serbanuta]

Tested with commit 07c0fc8

The final configuration on one of the two proof branches contains this (the other branch fails in a similar way):

  #Not ( {
    empty
  #Equals
    copy ( empty , I )
  } )
...
#And
  {
    true
  #Equals
    I >Int 0
  }

The semantics has a rule for evaluating copy that should make this branch succeed:

  rule  copy(empty, I:Int) => empty
    requires I >Int 0

and the side condition contains true #Equals I >Int 0 since the start configuration, however, that rule is not applied. After staring at the function evaluation logs for a while, I think it's because the side condition is not used when attempting to apply the rule above.

To reproduce:

tmp.k

module TMP
  imports INT
  imports K-EQUAL

  syntax IntList  ::= "empty" | concat(Int, IntList)

  syntax IntList ::= copy(IntList, Int)  [function, functional]

  rule  copy(empty, I:Int) => empty
    requires I >Int 0
  rule  copy(concat(E:Int, Es:IntList), I:Int) => concat(E, copy(Es, I -Int 1))
    requires I >Int 0
  rule  copy(Es:IntList, _:Int) => Es
    [owise]

  syntax KItem ::= iterateList(IntList, Int)

  rule  iterateList(empty, _:Int) => .K  [label(i1)]
  rule  iterateList(concat(_:Int, L:IntList), A:Int) => iterateList(L, A)  [label(i2)]

endmodule

tmp-proof.k

module TMP-PROOF
  imports TMP

  claim iterateList(Es, I) => .K
    requires I >Int 0
    ensures copy(Es:IntList, I:Int) ==K Es

endmodule

[ana-pantilie]

We should quickly take a look at simplifyRightHandSide, after the step where Es #Equals empty there should be an attempt here to simplify the ensures clause.

[JKTKops]

I'm able to reproduce this behavior with the following more straightforward proof:
tmp.k:

module TMP
  imports INT

  syntax KItem ::= run ( Either, Int ) | done ( Either )
  rule run(Left(),  _I) => done(Left())
  rule run(Right(), _I) => done(Right())

  syntax Either ::= Left() | Right()
  syntax Bool ::= P( Either , Int ) [function]

  rule P(Left(),I) => true
    requires I >Int 0
  rule P(Right(),I) => true
    requires I >Int 0
  rule P(E,I) => false
    requires I <=Int 0
endmodule

tmp-proof.k:

module TMP-PROOF
  imports TMP

  claim <k> run(E,I) => done(E) ... </k>
    requires I >Int 0
    ensures P(E,I)
endmodule

I think the run => done rule has to be written this way to cause branching, otherwise the backend cannot simplify the ensures clause regardless. If we write the proof without anything to branch on, it passes. I tried a few variations of smaller examples without branching but they did not exhibit this behavior. This probably reinforces the idea that the problem has to do with substitutions.

[JKTKops]

I can also confirm that our proposed change makes my proof pass.

@virgil-serbanuta would you mind trying your proof on the issue-2740 branch? I'm not sure if the proof is actually incorrect, or if there's a further issue with Kore. When I try it, I see this output:

kore-exec: [477578] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/max/scratch/kore/2740/tmp-proof.k:5:9-7:31
  #Not ( {
    L
  #Equals
    copy ( L , I +Int -1 )
  } )
#And
  <k>
    _DotVar1
  </k>
#And
  {
    L
  #Equals
    copy ( L , I )
  }
#And
  {
    true
  #Equals
    I >Int 0
  }

and I'm not actually sure if we expect this to get further, because I don't think we can reason about I +Int -1 with the information we have. However I'm new at this, so maybe I'm missing something.

[virgil-serbanuta]

I will try it, but when I submit issues for the Haskell backend I usually (though not always) try to minimize the proof such that it still shows the issue I'm trying to report, without trying too much to make a valid minimized claim (that's hard to do anyway because I can't really test it).

IIRC the non-minimized claim worked on an older Haskell backend, but did not work at the commit mentioned above. Would you have preferred to debug the original claim (the semantics would be much larger, perhaps the claim would also be more complex)? Or, would it be better to post both the minimized version and the original one?

[JKTKops]

If you don't know if it's correct, then that's fine. I'd guess that it needs further lemmas and that we have a fix for the problem demonstrated. Thanks!

Incidentally, do you know a commit that the non-minimized claim used to work on? When we started looking at this we had a guess for a commit that might've broken it, but when we tested this minimized claim on that commit, we got the same results as you did in the original comment.

[virgil-serbanuta]

I think it worked on 1724c5c

[virgil-serbanuta]

FWIW, I didn't find the issue-2740 branch on the main repository, and I didn't find any fork of the kore repository that belongs to you.

[JKTKops]

I thought I must've pushed it because at some point I switched from working locally to in a container, but perhaps not. It's all good, thanks for looking :)