EVMOR is rewritten to |Int

[nrryuya]

I tried to verify a spec of a simple code in written in Vyper(0.1.0b4) and it fails with Halt! Terminating branch. .

• Vyper code

@public
def simpleOR(a: bool, b: bool) -> bool:
    return a or b

• spec

 <output> _ => #asByteStackInWidth(1, 32) </output>

requires
    // omitted...
    andBool (A ==Int 1 orBool B ==Int 1)

full spec (gist)

In the final step, the <output> cell reaches to this.

<output>(_:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"0"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"1"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"2"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"3"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"4"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"5"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"6"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"7"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"8"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"9"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"10"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"11"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"12"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"13"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"14"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"15"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"16"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"17"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"18"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"19"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"20"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"21"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"22"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"23"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"24"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"25"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"26"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"27"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"28"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"29"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"30"),, Int(#"32")),, _:__EVM-DATA(nthbyteof(chop(_|Int__INT(A_1367:Int,, B_1368:Int)),, Int(#"31"),, Int(#"32")),, .WordStack_EVM-DATA(.KList))))))))))))))))))))))))))))))))))
<statusCode>(EVMC_SUCCESS_NETWORK(.KList))
<localMem>

full log of the final step (gist)

My first question is why _|Int__INT(A_1367:Int,, B_1368:Int) is there because in the evm.md, it says:

rule <k> EVMOR W0 W1 => W0 |Word W1   ~> #push ... </k>

i.e. using |Word not |Int` .

I found EVMOR is rewritten to |Int around STEP 941 (gist).

The second question is how to prove the spec correctly. The precondition in eDSL is andBool (A ==Int 1 orBool B ==Int 1) and it's translated to this in the conjunctive formula:

_==K_(_orBool__BOOL(_==K_(A_1367:Int,, Int(#"1")),, _==K_(B_1368:Int,, Int(#"1"))),, Bool(#"true"))

and it doesn't go well with _|Int__INT(A_1367:Int,, B_1368:Int) .

I tried with andBool (A |Int B) ==Int 1, which is translated to _==K_(_|Int__INT(A_1385:Int,, B_1386:Int),, Int(#"1")) but it also failed (==K should be ==Int here?).

Can we prove the spec if we add SMTLib translation for |Int ?

[denis-bogdanas]

|Int appears due to this rule:

rule W0 |Word   W1 => chop( W0 |Int W1 )

You have 2 solutions (from the top of my mind, there might be more):

1. use a custom KEVM version with split() construct like we do here:

https://github.com/kframework/evm-semantics/blob/ac78f8e2bb401cb3940cf540181fe8b9ae0c7bde/evm-symbolic.md#L48

Note that split must be added at semantics level, not as trusted spec rule, because spec rules work differently (see kprove tutorial).

2. Add a lemma for |Int that simplifies the term using the info in path condition.

[nrryuya]

We are using the latest commit at gnosis branch (5d3bbb6d9dd3a2913201071937cb3f00d66832b0) and the split() is already there (and still fails)?

https://github.com/kframework/evm-semantics/blob/5d3bbb6d9dd3a2913201071937cb3f00d66832b0/evm-symbolic.md

We should move to these?
#281
runtimeverification/verified-smart-contracts#99

[denis-bogdanas]

@nrryuya No I don't recommend using KEVM-imap, it is very much work in progress. If you use KEVM-gnosis, then you can USE split() in your spec to force branching on arbitrary expressions, as is explained in evm-symbolic.md. This is a way to help kprove evaluate functions that would otherwise get stuck.

[denis-bogdanas]

In your case you can try (split(A ==Int 1) ~> split(B ==Int 1) => .) Also those A and B probably want a range restriction 0..1.

[nrryuya]

@denis-bogdanas
Ah! Gotcha! :)
The spec with <k> (split(A ==Int 1) ~> split(B ==Int 1) => .) ~> (#execute => #halt) ~> _ </k> still fails but I'll do more investigation, not to bother you here too much. Thank you!