No split on KEVM JUMPI

[denis-bogdanas]

Steps to reproduce:

cd evm-semantics
make tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k.prove

Expected behavior: should pass

Actual behavior: Execution gets stuck with the following content of k cell:

JUMPI 559 bool2Word ( 0 <Int maxUInt160 &Int #asWord ( #range ( 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\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\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\x00\x01`" [ 128 := #buf ( 32 , SIGV0:Int ) ++ #buf ( 32 , SIGV1:Int ) ] [ 192 := #buf ( 32 , SIGR0:Int ) ++ #buf ( 32 , SIGR1:Int ) ] [ 256 := #buf ( 32 , SIGS0:Int ) ++ #buf ( 32 , SIGS1:Int ) ] [ 320 := 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\x00" ] [ 320 := #ecrec ( #buf ( 32 , HASH:Int ) , #buf ( 32 , SIGV0:Int ) , #buf ( 32 , SIGR0:Int ) , #buf ( 32 , SIGS0:Int ) ) [ 0 .. minInt ( 32 , #sizeByteArray ( #ecrec ( #buf ( 32 , HASH:Int ) , #buf ( 32 , SIGV0:Int ) , #buf ( 32 , SIGR0:Int ) , #buf ( 32 , SIGS0:Int ) ) ) ) ] ] , 320 , 32 ) ) )

It should split on JUMPI insteadm, based on these rules:

    rule <k> JUMPI _DEST I => . ... </k>
      requires I ==Int 0

    rule <k> JUMPI  DEST I => JUMP DEST ... </k>
      requires I =/=Int 0

[andreiburdusa]

I already investigated this some time ago, but couldn't solve it. From what I see, the proof does branch, like this

Axiom 42 is

    rule <k> JUMPI _DEST I => . ... </k>
      requires I ==Int 0

Axiom 43 is

    rule <k> JUMPI  DEST I => JUMP DEST ... </k>
      requires I =/=Int 0

The configuration on node 1763 contains the following

...
#And
  #Not ( {
    true
  #Equals
    0 <Int maxUInt160 &Int #asWord ( #range ( 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\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\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\x00\x01`" [ 128 := #buf ( 32 , SIGV0 ) ++ #buf ( 32 , SIGV1 ) ] [ 192 := #buf ( 32 , SIGR0 ) ++ #buf ( 32 , SIGR1 ) ] [ 256 := #buf ( 32 , SIGS0 ) ++ #buf ( 32 , SIGS1 ) ] [ 320 := 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\x00" ] [ 320 := #ecrec ( #buf ( 32 , HASH ) , #buf ( 32 , SIGV0 ) , #buf ( 32 , SIGR0 ) , #buf ( 32 , SIGS0 ) ) [ 0 .. minInt ( 32 , #sizeByteArray ( #ecrec ( #buf ( 32 , HASH ) , #buf ( 32 , SIGV0 ) , #buf ( 32 , SIGR0 ) , #buf ( 32 , SIGS0 ) ) ) ) ] ] , 320 , 32 ) )
  } )
#And
  #Not ( {
    true
  #Equals
    maxUInt160 &Int #asWord ( #range ( 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\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\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\x00\x01`" [ 128 := #buf ( 32 , SIGV0 ) ++ #buf ( 32 , SIGV1 ) ] [ 192 := #buf ( 32 , SIGR0 ) ++ #buf ( 32 , SIGR1 ) ] [ 256 := #buf ( 32 , SIGS0 ) ++ #buf ( 32 , SIGS1 ) ] [ 320 := 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\x00" ] [ 320 := #ecrec ( #buf ( 32 , HASH ) , #buf ( 32 , SIGV0 ) , #buf ( 32 , SIGR0 ) , #buf ( 32 , SIGS0 ) ) [ 0 .. minInt ( 32 , #sizeByteArray ( #ecrec ( #buf ( 32 , HASH ) , #buf ( 32 , SIGV0 ) , #buf ( 32 , SIGR0 ) , #buf ( 32 , SIGS0 ) ) ) ) ] ] , 320 , 32 ) ) <=Int 0
  } )
#And
...

which basically says that maxUInt160 &Int ... is both <= and > 0.

I think the backend gets stuck because it can't detect that its branch is infeasible.

[ana-pantilie]

@andreiburdusa So is this a problem in the Haskell backend or is it a problem with KEVM in the sense that it's missing some simplification rules?

[andreiburdusa]

I think it's a problem with the backend because some rules that me and Everett expected to make the proof advance didn't help

[ana-pantilie]

Most likely an issue with sending the condition to SMT. Possibly a duplicate of #3032

[ehildenb]

Test is still failing, needs reproducing then: https://github.com/runtimeverification/evm-semantics/blob/master/tests/failing-symbolic.haskell#L1

[goodlyrottenapple]

try to see if a simplified expression

#And
  #Not ( {
    true
  #Equals
    0 <Int foo
  } )
#And
  #Not ( {
    true
  #Equals
    foo <=Int 0
  } )

gets automatically simplified

[jinxinglim]

Hi all, I have made a pull request (runtimeverification/evm-semantics#1408) that address this issue. Basically, I added the following two rules and the proof of ecrecoverloop00-sig1-spec.k succeeded:

rule A  <Int B => #Not ( { true #Equals B <=Int A } ) [simplification]
rule A <=Int B => #Not ( { true #Equals B  <Int A } ) [simplification]

I also documented my many other attempts on the issue but only this one works as of now.

[goodlyrottenapple]

Confirmed that the SMT solver can discharge this goal when simple enough, so likely failing to translate the condition in the actual test. The two rules above seem like a good solution as we don't want to rely on the SMT solver magic when a concrete simplification rule works.

[ana-pantilie]

Re-opening because of #3302 (comment)