runtimeverification / runtimeverification/haskell-backend

Haskell backend fails to apply `==Int` equality

Open
#3,060 2 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

bug needs-reproducing
Dominant language
Haskell
Stars
224
Forks
43
No merged PRs in 30d

Description

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

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the failing proof in tests/specs/mcd/flipper-bids-pass-rough-spec.k and the simplification rule in tests/specs/mcd/word-pack.k. Reproduce the stuck equality using the attached kevm-bug-flipper-bids-pass-rough.tar.gz report, then trace the Haskell backend's handling of the equality and confirm that the original proof reaches #Top without changing the specification workaround.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
backend
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
38/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.