Using Sequence instead of Peek for Stack

[DavePearce]

Idea suggested by @booleanfunction to optimise how the stack works.

[booleanfunction]

example:

method block_0_0x06c3(src: u160, dst: u160, wad: u256, st': EvmState.ExecutingState) returns (st'': EvmState.State)
    requires st'.evm.code == Code.Create(BYTECODE_0)
    requires st'.WritesPermitted() && st'.PC() == 0x06c3
    // Free memory pointer
    requires st'.MemSize() >= 0x60 && st'.Read(0x40) == 0x60 && st'.Read(0x0) == src as u256
    // Stack height(s)
    requires st'.Operands() == 9
    // Stack items
    requires st'.evm.stack.contents == [0,0x03,wad,0x0,wad,dst as u256,src as u256,0x229,st'.Peek(8)] 
    {
        var st := st';
        stackLemma9(st);
        //|fp=0x0060|0x0,0x03,wad,0x0,wad,dst*,src*,0x229,transferFrom| 
        st := Push1(st,0x20);
        //|fp=0x0060|0x20,0x0,0x03,wad,0x0,wad,dst*,src*,0x229,transferFrom|
        assert (st.Peek(0) + st.Peek(1)) <= (Int.MAX_U256 as u256);
        st := Add(st);
        //|fp=0x0060|0x20,0x03,wad,0x0,wad,dst*,src*,0x229,transferFrom|
        st := Swap(st,1);
        //|fp=0x0060|0x03,0x20,wad,0x0,wad,dst*,src*,0x229,transferFrom|
        st := Dup(st,2);
        //|fp=0x0060|0x20,0x03,0x20,wad,0x0,wad,dst*,src*,0x229,transferFrom|
        stackLemma10(st);
        st := block_0_0x06c8(src,dst,wad,st);
        return st;
    }

I have the stack lemmas setup individually but plan to try a version with stack size as a parameter.

lemma stackLemma9(st: EvmState.ExecutingState)
    requires st.Operands() >= 9
    ensures st.evm.stack.contents[0..9] == [st.Peek(0),st.Peek(1),st.Peek(2),st.Peek(3),st.Peek(4),st.Peek(5),st.Peek(6),st.Peek(7),st.Peek(8)]
{}

lemma stackLemma10(st: EvmState.ExecutingState)
    requires st.Operands() >= 10
    ensures st.evm.stack.contents[0..10] == [st.Peek(0),st.Peek(1),st.Peek(2),st.Peek(3),st.Peek(4),st.Peek(5),st.Peek(6),st.Peek(7),st.Peek(8),st.Peek(9)]
{}

[booleanfunction]

PS - the stack lemmas were written before I starting using the whole stack ... I will adjust them to be for specific stack sizes rather than using a lower size bound.