[Bug] [kprovex] - Lemma not applied to term if term contains function with side-condition

[david-k]

K Version

$ kompile --version
K version:    v5.2.21-10-g958561d3c
Build date:   Thu Dec 02 20:14:27 CET 2021

Description

If a term matches the LHS of a lemma, but the term contains a partial function that rewrites to some concrete function, then the lemma is not applied, even if the partial function is actually defined for the given arguments. This problem occurs when using the Haskell backend but not when using the Java backend.

Input Files

I found this bug while trying to prove tests/specs/mcd/flipper-bids-pass-rough-spec.k from the KEVM repo. The following definitions represent a simplified version of that proof.

module LEMMA-NOT-APPLIED
  imports INT
  imports BOOL

  // Intuitively, `Pack16` stores two 8-bit integers into a single 16-bit word
  syntax Int ::= Pack16(Int, Int) [function, no-evaluators, smtlib(Pack16)]

  // This is the lemma that is not applied but that I expected to be applied when proving the claim below
  rule
      WORD ==Int Pack16(A, B)
    =>
      A ==Int (WORD &Int 255) andBool
      B ==Int ((WORD >>Int 8) &Int 255)
    [simplification]

  syntax Int ::= PartialId(Int) [function]
               | ConcreteId(Int) [function, functional]

  rule PartialId(I) => ConcreteId(I) requires 0 <=Int I andBool I <=Int 255 // Arbitrary side-condition
  rule ConcreteId(I) => I [concrete]

  // Proof helpers
  syntax ProofStep ::= runLemma(Int)
                     | doneLemma(Int)

  rule <k>runLemma(A) => doneLemma(A) ...</k>
endmodule


module LEMMA-NOT-APPLIED-SPEC
  imports LEMMA-NOT-APPLIED

  // This claim fails when using the Haskell backend but I would have expected it to pass
  claim
    <k>
      runLemma((PartialId(WORD) &Int 255) +Int ((PartialId(WORD) >>Int 8) &Int 255))
    =>
      doneLemma(A +Int B)
    </k>
    requires
      0 <=Int WORD andBool // To satisfy the side-condition of PartialId()
      PartialId(WORD) ==Int Pack16(A, B)

endmodule

Reproduction Steps

When trying to prove the above claim with kprovex I get the following output:

kore-exec: [464007] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/david/Documents/RV/k-snippets/lemma-not-applied/lemma-not-applied-spec.k:5:5-12:41
  #Not ( {
    ( ConcreteId ( WORD ) &Int 255 ) +Int ( ConcreteId ( WORD ) >>Int 8 &Int 255 )
  #Equals
    A +Int B
  } )
#And
  <k>
    doneLemma ( ( ConcreteId ( WORD ) &Int 255 ) +Int ( ConcreteId ( WORD ) >>Int 8 &Int 255 ) ) ~> .
  </k>
#And
  {
    ConcreteId ( WORD )
  #Equals
    Pack16 ( A , B )
  }
#And
  {
    true
  #Equals
    0 <=Int WORD
  }

As can be seen by the fact that the path condition { ConcreteId ( WORD ) #Equals Pack16 ( A , B ) } is still there it seems that the lemma has not been applied. However, when removing the requires clause from the rule for PartialId() the proof goes through. The proof also goes through when replacing PartialId with ConcreteId in the claim.

Also interesting is that when removing [concrete] from the rule for ConcreteId(), then the path condition { ConcreteId ( WORD ) #Equals Pack16 ( A , B ) } goes away, but the proof still fails.

Finally (and I don't know if this is a separate issue), if I remove the requires clause from PartialId() (making the proof pass) and instead add a requires clause to the lemma, then the proof again fails to go through, even if the side-condition is met.

Expected Behavior

The above claim should be successfully proven by kprovex when using the Haskell backend.