Minified KWasm proof that should pass

[ehildenb]

I believe this proof should pass, but it doesn't seem to.

File data.k (kompile --backend haskell --main-module WASM-DATA --syntax-module WASM-DATA data.k:

require "domains.k" 

module WASM-DATA 
    imports INT 
    imports BOOL 

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

    syntax ByteMap
 // --------------

    syntax Int ::= #getRange (ByteMap, Int , Int) [function, functional, smtlib(getRange)] 
 // -------------------------------------------------------------------------------------- 
    rule #getRange( _, _, 0) => 0
endmodule

And the accompanying proof file (functions-spec.k):

requires "data.k"

module FUNCTIONS-LEMMAS
    imports WASM-DATA

    rule X modInt N => X requires 0 <=Int X andBool X <Int N [simplification]

    rule 0 <=Int #getRange(_, _, _)                    => true                                                                                [simplification]
    rule #getRange(_, _, WIDTH)               <Int MAX => true requires 2 ^Int (8 *Int WIDTH)              <=Int MAX                          [simplification]
    rule (#getRange(_, _, WIDTH) <<Int SHIFT) <Int MAX => true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX                          [simplification]
    rule VAL1 +Int VAL2                       <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool #distinctBits(VAL1, VAL2) [simplification]

    syntax Bool ::= #distinctBits ( Int , Int ) [function]
 // ------------------------------------------------------
    rule #distinctBits(#getRange(_, _, WIDTH), #getRange(_, _, _) <<Int SHIFT) => true requires WIDTH *Int 8 <=Int SHIFT
endmodule

module FUNCTIONS-SPEC
    imports FUNCTIONS-LEMMAS

    rule <k> (#getRange(BM, ADDR +Int 1, 1) +Int (#getRange (BM, ADDR, 1) <<Int 8)) modInt 65536
          =>  #getRange(BM, ADDR +Int 1, 1) +Int (#getRange (BM, ADDR, 1) <<Int 8)
         ...
         </k>
endmodule

Running kprove --directory ./.build/defn/haskell tests/proofs/functions-spec.k --format-failures --def-module FUNCTIONS-LEMMAS produces output:

  #Not ( {
    ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) ) modInt 65536
  #Equals
    #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 )
  } )
#And
  <k>
    ( #getRange ( BM , ADDR +Int 1 , 1 ) +Int ( #getRange ( BM , ADDR , 1 ) <<Int 8 ) ) modInt 65536 ~> DotVar1
  </k>

But simplifying the term is pretty straightforward to do using the simplification rules provided.

I've attached the kore files produced by kprove --debug, and in this tarball (named a txt file for GitHub) I have added the file command which kprove --verbose outputs (so you can run kore-exec directly).

functions-proof.tar.txt

[ehildenb]

This is blocking an update to KWasm to switch to Bytes type, which is blocking an update to Polkadot repository to take advantage of faster KWasm. Otherwise everything is working fine with the update, except this simple proof.

[ehildenb]

I've minified the example even further to really focus on the exact problem.

[ehildenb]

I figured it out. I needed simplification lemmas about the lower bound 0 <=Int VAL1 +Int VAL2 and 0 <=Int VAL <<Int SHIFT as well as the ones for upper bounds.