search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
210 stars 42 forks source link

Haskell backend fails to apply `==Int` equality #3060

Open goodlyrottenapple opened 2 years ago

goodlyrottenapple commented 2 years ago

In the following version of K and kore-exec:

K version:    5.3.0
Build date:   Wed May 18 09:50:57 BST 2022

Kore version 0.60.0.0

The following proof from the evm-semantics repo fails to discharge this final equality:

#buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 1 ) ) ++ #buf ( 32 , maxUInt160 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) ) ++ #buf ( 32 , maxUInt48 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) /Int pow160 ) ++ #buf ( 32 , maxUInt48 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) /Int pow208 ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 3 ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 4 ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 5 ) )
#Equals
#buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 1 ) ) ++ #buf ( 32 , Guy:Int ) ++ #buf ( 32 , Tic:Int ) ++ #buf ( 32 , End:Int ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 3 ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 4 ) ) ++ #buf ( 32 , #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 5 ) )

specifically, it gets stuck trying to prove

#buf ( 32 , maxUInt160 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) ) ++ 
#buf ( 32 , maxUInt48 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) /Int pow160 ) ++ 
#buf ( 32 , maxUInt48 &Int #lookup ( ACCT_ID_STORAGE:Map , keccak ( #buf ( 32 , ABI_n:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) +Int 2 ) /Int pow208 )
  #Equals
#buf ( 32 , Guy:Int ) ++ 
#buf ( 32 , Tic:Int ) ++ 
#buf ( 32 , End:Int )

Given that the claim contains the following clause

#lookup(ACCT_ID_STORAGE, #Flipper.bids[ABI_n].guy_tic_end) ==Int #WordPackAddrUInt48UInt48(Guy, Tic, End)

and wordpack.k contains the following simplification

    rule    ADDR_UINT48_UINT48 ==Int #WordPackAddrUInt48UInt48(ADDR, UINT48_1, UINT48_2)
         => ADDR     ==Int maxUInt160 &Int  ADDR_UINT48_UINT48
    andBool UINT48_1 ==Int maxUInt48  &Int (ADDR_UINT48_UINT48 /Int pow160)
    andBool UINT48_2 ==Int maxUInt48  &Int (ADDR_UINT48_UINT48 /Int pow208)
    andBool #rangeUInt(256, ADDR_UINT48_UINT48)
      [simplification]

the backend should be able to simplify the above goal. Even attempting to rewrite the above to use the #Equals (using a version of K with https://github.com/runtimeverification/haskell-backend/pull/3042) doesn't work.

However, tweaking the above #WordPackAddrUInt48UInt48 function symbol from

    syntax Int ::= #WordPackAddrUInt48UInt48 ( Int , Int , Int ) [function, no-evaluators, smtlib(WordPackAddrUInt48UInt48)]

to

    syntax Bool ::= #WordPackAddrUInt48UInt48Prop ( Int , Int , Int, Int ) [function, smtlib(WordPackAddrUInt48UInt48Bool)]

where the simplification rule now becomes

    rule     #WordPackAddrUInt48UInt48Prop(ADDR_UINT48_UINT48, ADDR, UINT48_1, UINT48_2)
          => true
     ensures ADDR     ==Int maxUInt160 &Int  ADDR_UINT48_UINT48
     andBool UINT48_1 ==Int maxUInt48  &Int (ADDR_UINT48_UINT48 /Int pow160)
     andBool UINT48_2 ==Int maxUInt48  &Int (ADDR_UINT48_UINT48 /Int pow208)
     andBool #rangeUInt(256, ADDR_UINT48_UINT48)
       [simplification]

we now get #Top when running the modified proof.

Attached below is the generated bug report. I tried minimizing the proof, but could not re-create the conditions of the proof, such that the prover would get stuck on this claim.

kevm-bug-flipper-bids-pass-rough.tar.gz

ana-pantilie commented 2 years ago

I'd try to minimize the spec again, which means doing a "run-lemma/done-lemma" style proof:

claim run-lemma(relevant-part-of-config) => done-lemma(what-you-expect-to-get)

You can then use https://github.com/runtimeverification/haskell-backend/wiki/Debugging#function-evaluation to see if that simplification rule is actually getting applied or not.

We need to get this minimized before we can figure out if it's a Haskell backend bug or not.

Sereja313 commented 1 year ago

@ana-pantilie I managed to reproduce this error. backend version:

Kore version 0.60.0.0
Git:
  revision: 74bc7a963a825d0f0f034b5d3412dc59448e51bb (dirty)
  branch:   master
  last commit:  Tue Feb 7 05:02:49 2023 -0700