Cannot simplify proof dealing with indirect equalities

[ehildenb]

I have a module where I want to assert things about a Map in the pre-condition, and use that knowledge to check a post condition. Attached is the generated bug report. This example comes from porting the benchmark proofs of KEVM over to the Haskell backend. Here is the K definition:

module TEST
    imports DOMAINS

    configuration
        <k> $PGM:Foo </k>
        <mem> .Map </mem>

    syntax Foo ::= doIt ( Int , Int )
    rule <k> doIt(K, V) => . ... </k>
         <mem> M => M [ K <- V +Int #lookup(M, K) ] </mem>

    syntax Int ::= #lookup ( Map , Int ) [function, functional, smtlib(lookup)]
 // ---------------------------------------------------------------------------
    rule #lookup( (KEY |-> VAL:Int) _M , KEY ) => VAL modInt 256
    rule #lookup(                    M , KEY ) => 0              requires notBool KEY in_keys(M)
    rule #lookup( (KEY |-> VAL    ) _M , KEY ) => 0              requires notBool isInt(VAL)

endmodule

And the specification module:

requires "test.k"

module TEST-SPEC
    imports TEST

    rule <k> doIt(K, V1) => . ... </k>
         <mem> S => S [ K <- ?V3 ] </mem>
      requires 0 <=Int V1 andBool V1 <Int 256
       andBool #lookup(S, K) ==Int V2
       andBool 0 <=Int V2 andBool V2 <Int 256
       andBool 0 <=Int V2 +Int V1 andBool V2 +Int V1 <Int 256

       ensures ?V3 ==Int V2 +Int V1
endmodule

In the output counterexample, I get this clause in the side-condition (i):

  #Not ( #Exists ?V3 . {
      ?V3 ==Int V2 +Int V1
    #Equals
      true
    }
  #And
    {
      S [ K:Int <- V1 +Int #lookup ( S , K ) ]
    #Equals
      S [ K:Int <- ?V3:Int ]
    } )

But we also have in the path condition (ii):

  {
    true
  #Equals
    #lookup ( S , K ) ==Int V2
  }

So it should be able to simplify (i) using (ii) to see that it's infeasible, and prune this branch, is my thinking.

Here is the generated bug report: test.tar.gz

[ttuegel]

These conditions are not simplified:

  {
    true
  #Equals
    #lookup ( S , K ) ==Int V2
  }

    {
      ?V3 ==Int V2 +Int V1
    #Equals
      true
    }

The first one may not be satisfied because the right-hand side of the equality is partial. I don't know why the second isn't simplified. Simplifying these conditions should give

{ V2 #Equals #lookup ( S , K ) } #And { ?V3 #Equals #lookup ( S , K ) +Int V1 }

and the solver should be happy after that.

[jberthold]

The current version outputs a different remainder, but that remainder is also infeasible and should be discarded as such: (After replacing rule by claim in the above spec module test-spec.k) Running kprove test-spec.k yields

#Not ( {
    S [ K:Int <- #lookup ( S , K ) +Int V1 ]
  #Equals
    S [ K:Int <- V1 +Int #lookup ( S , K ) ]
  } )
#And
  <generatedTop>
    <k>
      _DotVar1
    </k>
    <mem>
      S [ K:Int <- V1 +Int #lookup ( S , K ) ]
    </mem>
  </generatedTop>
#And
  ... Rest

where Rest are constraints about the terms #lookup (S, K) , V1, and V1 +Int #lookup(S, K) being within [0, 2^256).

The two maps S[ K -> #lookup(S,K) +Int V1] and S[ K -> V1 +Int #lookup(S, K)] should probably be recognised as equal.

[ana-pantilie]

I think that for some reason we can't unify #lookup ( S , K ) +Int V1 with V1 +Int #lookup ( S , K ) even though we should know that +Int is commutative.

We should investigate how ^ is implemented.