Function in the main condition not (re-)evaluated when the main condition changes

[virgil-serbanuta]

I think that there are two issues with the proof below, the title of the issue contains the first one that is encountered when debugging. The other issue is that rewriting stops at a random point for no apparent reason.

To reproduce:

Kore version 0.51.0.0 Git: revision: 0521b0ea0ca6c2f61192822edf45a2ace7a52310 branch: master last commit: Thu Aug 5 08:10:21 2021 -0600

The --bug-report file: condition-reevaluation.tar.gz

Also:

tmp.k:

module TMP
  imports BOOL
  imports INT

  syntax ExpressionList ::= "nil" | cons(KItem, ExpressionList)

  syntax Bool ::= listElementsAreDistinct(ExpressionList)  [function, functional]

  rule listElementsAreDistinct(nil) => true
  rule listElementsAreDistinct(cons(E:KItem, Es:ExpressionList))
      => true
          andBool notBool #listContains(Es, E)
          andBool listElementsAreDistinct(Es)

  syntax Bool ::= #listContains(ExpressionList, KItem)  [function, functional]

  rule  #listContains(nil, _) => false
  rule  #listContains(cons(E:KItem, _:ExpressionList), E) => true
  rule  #listContains(cons(_:KItem, Es:ExpressionList), X:KItem)
          => #listContains(Es, X)  [owise]

  syntax KItem ::= lemmaLastDistinct(KItem, KItem, ExpressionList)

  rule lemmaLastDistinct(E1:KItem, E2:KItem, nil) => concretizeValue(E1 ==K E2)
  rule lemmaLastDistinct(E:KItem, E1:KItem, cons(E2:KItem, Es:ExpressionList))
      =>  concretizeValue(E ==K E2)
          ~> concretizeValue(E ==K E1)
          ~> concretizeValue(E1 ==K E2)
          ~> lemmaLastDistinct(E, E2, Es)

  syntax KItem ::= concretizeValue(KItem)
  rule concretizeValue(false) => .K  [label(concretizeValueFalse)]
  rule concretizeValue(true) => .K  [label(concretizeValueTrue)]

  syntax KItem ::= #last(KItem, ExpressionList)  [function, functional]
  syntax KItem ::= #last0(ExpressionList)  [function, functional]

  rule #last(E:KItem, nil) => E
  rule #last(_:KItem, Es:ExpressionList) => #last0(Es)
    requires pListLen(Es) >Int 0

  rule #last0(cons(E:KItem, Es:ExpressionList)) => #last(E, Es)

  syntax Int ::= pListLen(ExpressionList)  [function, functional, smtlib(pListLen)]
  rule pListLen(nil) => 0
  rule pListLen(cons(_:KItem, Es:ExpressionList)) => 1 +Int pListLen(Es)

endmodule

tmp-proof.k:

module TMP-PROOF
  imports TMP

  claim lemmaLastDistinct(E1, E2, Es) => .K
      requires listElementsAreDistinct(cons(E1, cons(E2, Es)))
      ensures E1 =/=K #last(E2, Es)

endmodule

Command line:

kompile tmp.k --backend haskell && kprove tmp-proof.k

The problem:

The command line above produces the output below. There are two issues here:

• In the predicate, #listContains ( cons ( E3 , nil ) , E2 ) is not evaluated, although the predicate also contains #Not ( { E2 #Equals E3 } ), which should be enough to allow it to be evaluated. Note that the #Not ( { E2 #Equals E3 } ) part of the condition appeared during rewriting, when the configuration was split by concretizeValue. Similarly, #listContains ( cons ( E2 , cons ( E3 , nil ) ) , E3 ) is not evaluated, although there is enough information to evaluate it.
• The prover thinks that this is the final configuration, although it should attempt to still rewrite concretizeValue ( true )

kore-exec: [985441] Warning (WarnClaimRHSIsBottom):
    (InfoReachability) while checking the implication:
    The right-hand side of the claim is bottom: /mnt/data/runtime-verification/elrond-multisig/tmp/tmp-proof.k:4:9-6:36
kore-exec: [986977] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /mnt/data/runtime-verification/elrond-multisig/tmp/tmp-proof.k:4:9-6:36
  #Not ( {
    E2
  #Equals
    E3
  } )
#And
  <k>
    concretizeValue ( true ) ~> _DotVar1 ~> .
  </k>
#And
  {
    false
  #Equals
    #listContains ( cons ( E2 , cons ( E3 , nil ) ) , E3 )
  }
#And
  {
    false
  #Equals
    #listContains ( cons ( E3 , nil ) , E2 )
  }

Information for myself: this was minimized from protocol-correctness/proof/lemmas/list/contains/proof-last-distinct.k

[ana-pantilie]

This is not the same issue as https://github.com/kframework/kore/issues/2785, so we should investigate separately.

[andreiburdusa]

I tried running this on fix-condition-simplifier branch an got

andrei@q:~/Desktop/issue-2786$ kompile tmp.k --backend haskell && kprove tmp-proof.k --haskell-backend-command "/home/andrei/kore/.build/kore/bin/kore-exec"
[Warning] Compiler: Could not find main syntax module with name TMP-SYNTAX in
definition.  Use --syntax-module to specify one. Using TMP as default.
  #Not ( {
    E2
  #Equals
    E3
  } )
#And
  <k>
    lemmaLastDistinct ( E3 , E3 , Es0 ) ~> _DotVar1 ~> .
  </k>
#And
  {
    false
  #Equals
    #listContains ( Es0 , E3 )
  }
#And
  {
    false
  #Equals
    #listContains ( cons ( E2 , cons ( E3 , Es0 ) ) , E3 )
  }
#And
  {
    false
  #Equals
    #listContains ( cons ( E3 , Es0 ) , E2 )
  }
#And
  {
    true
  #Equals
    listElementsAreDistinct ( Es0 )
  }

concretizeValue ( true ) is no longer present. I think the next step is investigating why #listContains (...) are not evaluated.

[ana-pantilie]

Looks like the problems @virgil-serbanuta pointed out aren't there anymore, right? Virgil, did you expect the proof to pass with those issues fixed?

[virgil-serbanuta]

It's fine if the proof does not pass.

Note that one of the two issue mentioned in the initial bug report is still not fixed: the backend thinks that a non-final configuration is final, without any obvious reason about why that would be.

See this repl session (commit a53c565d2bf5c7155aac231f7ebeac8698dc3eb4 is part of the fix-condition-simplifier branch) for more details:

Kore version 0.52.0.0
Git:
  revision:     a53c565d2bf5c7155aac231f7ebeac8698dc3eb4
  branch:       fix-condition-simplifier
  last commit:  Tue Aug 31 13:15:33 2021 +0000
Welcome to the Kore Repl! Use 'help' to get started.

Kore (0)> step 10
Stopped after 0 step(s) due to branching on [1,2]
Kore (0)> select 2
Kore (2)> step 10
Stopped after 0 step(s) due to branching on [3,4]
Kore (2)> select 3
Kore (3)> step 10
Stopped after 2 step(s) due to reaching end of proof on current branch.
Kore (6)> proof-status
Current proof status: 
  claim 0: InProgress [1,4,6]
Kore (6)> step
Stopped after 0 step(s) due to reaching end of proof on current branch.
Kore (6)> proof-status
Current proof status: 
  claim 0: InProgress [1,4,6]

Note that, on taking a step from node 6, the repl will say reaching end of proof on current branch., while proof-status will mention node 6 as in-progress.

[ana-pantilie]

Oh, that's weird. @andreiburdusa can you investigate ^?

[andreiburdusa]

method: After investigating what happens in transitionRule when we run step from node 6, the next step would be investigating what happens in applyAxioms.

[ana-pantilie]

I'm going to close this because we used it to track the second problem, and the fix for that one got merged (https://github.com/kframework/kore/pull/2842). We are tracking the first problem on https://github.com/kframework/kore/issues/2785.