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.