Add Compiler Optimisation Examples

[DavePearce]

predicate equiv(l: State, r: State) {
    if l.EXECUTING? && r.EXECUTING?
    then
        l.evm.stack == r.evm.stack &&
        l.evm.memory == r.evm.memory &&
        l.evm.world == r.evm.world &&
        l.evm.context == r.evm.context &&
        l.evm.substate == r.evm.substate &&
        l.evm.gas == r.evm.gas
    else if l.RETURNS? && r.RETURNS?
    then
        l.data == r.data && l.world == r.world
    else if l.ERROR? && r.ERROR?
    then
        l.data == r.data
    else
        false
}

method pushpush_dup(st: ExecutingState, w: u8)
// Require enough space for two stack items
requires st.Capacity() > 2 {
    // Original Code Path
    var s1 := Bytecode.Push1(st,w);
    var s2 := Bytecode.Push1(s1,w);
    // Optimised Code Path
    var o1 := Bytecode.Push1(st,w);
    var o2 := Bytecode.Dup(o1,1);
    // Should be Equivalent
    assert equiv(s2,o2);
}

method addcc_push(st: ExecutingState, m: u8, n: u8)
// Require enough space for two stack items
requires st.Capacity() > 2 
// No overflow
requires (m as nat) + (n as nat) <= MAX_U8 {
    // Original Code Path
    var s1 := Bytecode.Push1(st,m);
    var s2 := Bytecode.Push1(s1,n);
    var s3 := Bytecode.Add(s2);
    // Optimised Code Path
    var o1 := Bytecode.Push1(st,m+n);
    // Should be Equivalent
    assert equiv(s3,o1);
}