Add Counter Example

[DavePearce]

const COUNTER_CODE : seq<u8> := [
    0x60,0x00,0x54,0x60,0x01,0x01,0x80,0x61,0x00,0x10,0x57,0x60,0x00,0x60,0x00,0xfd,0x5b,0x60,0x00,0x55,0x00
]
const ENTRY_STATE : ExecutingState := EVM.Init(gas:=1000,code:=COUNTER_CODE)

method Counter(st0: ExecutingState) returns (stn:State)
// Require enough space for two stack items
requires st0 == ENTRY_STATE 
// Upon successful execution, counter increases by 1.
ensures stn.EXECUTING? ==> st0.Load(0x0) < stn.Load(0x0) {
    var st := st0;
    st := Bytecode.Push1(st,0x00);
    st := Bytecode.SLoad(st);
    st := Bytecode.Push1(st,0x01);
    st := Bytecode.Add(st);
    st := Bytecode.Dup(st,1);
    st := Bytecode.Push2(st,0x0010);
    st := Bytecode.JumpI(st);
    assert st.PC() in {0x0b,0x10};
    if st.PC() == 0x0b {
        st := Bytecode.Push1(st,0x00);
        st := Bytecode.Push1(st,0x00);
        st := Bytecode.Revert(st);
    } else {
        st := Bytecode.JumpDest(st);
        st := Bytecode.Push1(st,0x00);
        st := Bytecode.SStore(st);
        st := Bytecode.Stop(st);
    }
    return st;
}