Postconditions for Stack Behavior of Opcode And

[gaxiiiiiiiiiiii]

To establish the postconditions for the stack behavior of the opcode And, I wrote the following AndSpec method. However, it causes a timeout during verification.

method AndSpec(st : ExecutingState) returns (st' : ExecutingState)
  requires st.Operands() >= 2 && st.Fork() == EvmFork.BERLIN
  ensures st'.Operands() >= 1
  ensures st'.Peek(0) == ((st.Peek(0) as bv256 & st.Peek(1) as bv256) ) as u256
{
  st' := And(st);  
}

I also attempted to add the desired postconditions to the existing And function, but this approach also led to a timeout.

function newAnd(st: ExecutingState): (st': State)
    ensures st'.EXECUTING? || st' == ERROR(STACK_UNDERFLOW)
    ensures st'.EXECUTING? <==> st.Operands() >= 2
    ensures st'.EXECUTING? ==> st'.Operands() == st.Operands() - 1    
    ensures st'.EXECUTING? ==> st'.Peek(0) == ((st.Peek(0) as bv256 & st.Peek(1) as bv256) ) as u256 // new postcondition

Original Definition

function And(st: ExecutingState): (st': State)
ensures st'.EXECUTING? || st' == ERROR(STACK_UNDERFLOW)
ensures st'.EXECUTING? <==> st.Operands() >= 2
ensures st'.EXECUTING? ==> st'.Operands() == st.Operands() - 1
{
    if st.Operands() >= 2
    then
        var lhs := st.Peek(0) as bv256;
        var rhs := st.Peek(1) as bv256;
        var res := (lhs & rhs) as u256;
        st.Pop(2).Push(res).Next()
    else
        ERROR(STACK_UNDERFLOW)
}

However, when I modified the function body to define res directly without using lhs and rhs, the verification succeeded.

{
    if st.Operands() >= 2
        then
        // var lhs := st.Peek(0) as bv256;
        // var rhs := st.Peek(1) as bv256;
        // var res := (lhs & rhs) as u256;
        var res := (st.Peek(0) as bv256 & st.Peek(1) as bv256) as u256;
        st.Pop(2).Push(res).Next()
    else
        ERROR(STACK_UNDERFLOW)
}

My question is, to achieve the desired postconditions, is such a modification of And necessary, or is there a way to achieve this without modification?

Any insights or guidance you could provide on this issue would be greatly appreciated. Thanks in advance.

[DavePearce]

Unfortunately, And is a real problem when attempting to verify real-world contracts. The problem stems from the use of bitvectors (i.e. bv256) which are simply not well supported. In the WETH proof, we use alternative implementations (e.g. AndU1(), AndU160(), etc) when it makes sense to do so. These do not use bv256, but are only applicable in certain (albeit quite common) situations.

Realistically the changes you made above, whilst they may work in a particular situation, are likely to be very brittle. That is, they won't work in many other situations. Its not clear to me even why that change (i.e. inlining lhs, rhs) would make any difference. But, it probably just affects the ordering of e.g. variable declarations going into the Z3 theorem prover.