BitVector Operations

[DavePearce]

There are various situations where eliminating bitvectors can be quite helpful. Specifically, something like this:

 st := Push4(st,0xffffffff);
 st := And(st);

is replaced with something like this:

 st := Push4(st,0xffffffff);
 st := AndU32(st);

where we have:

    /**
     * Provides an alternative implementation of Bytecode.And specialised to the
     * particular case of converting an arbitrary u256 into a u32 (i.e.
     * stripping out a 4byte function signature for dispatch).
     */
    function AndU32(st: EvmState.ExecutingState): (st': EvmState.State)
    requires st.Operands() >= 2 && st.Peek(0) == (Int.MAX_U32 as u256) {
        var rhs := st.Peek(1);
        var res := rhs % (Int.TWO_32 as u256);
        st.Pop(2).Push(res).Next()
    }