vm.zok

struct Stack {
	u32[21] values
	u32 length
}

struct Memory {
	u32[16] values
}

struct State {
	Stack stack
	Memory memory
	bool error
}

struct Calldata {
	u32[16] values
}

const u32 MEMORY_SIZE = 16
const u32 STACK_SIZE = 16
const u32 PROGRAM_SIZE = 16
const u32 CALLDATA_SIZE = 16
const u32 MAX_INSTR = 16
const u32 STACK_HEAD_START = 5

def has<N>(Stack s) -> bool:
	return s.length >= STACK_HEAD_START + N

def error(State s) -> State:
	s.error = true
	return s

def nth<N>(Stack s) -> u32:
	return s.values[s.length - N]

def first(Stack s) -> u32:
	return nth::<1>(s)

def second(Stack s) -> u32:
	return nth::<2>(s)

def third(Stack s) -> u32:
	return nth::<3>(s)

def decrease<L>(Stack s) -> Stack:
	s.length = s.length - L
	return s

def increase<L>(Stack s) -> Stack:
	s.length = s.length + L
	return s

def writeFirst<L>(State s, u32 n) -> State:
	s.stack = decrease::<L>(s.stack)
	s.stack = increase::<1>(s.stack)
	assert(has::<1>(s.stack))
	s.stack.values[s.stack.length - 1] = n
	return s

def add(State s) -> State:
	return if (!has::<2>(s.stack)) then error(s) else writeFirst::<2>(s, first(s.stack) + second(s.stack)) fi

def calldataload(State s, Calldata c) -> State:
	bool e = !has::<1>(s.stack) || first(s.stack) >= CALLDATA_SIZE
	return if e then error(s) else writeFirst::<1>(s, c.values[first(s.stack)]) fi

def mload(State s) -> State:
	bool e = !has::<1>(s.stack) || first(s.stack) >= MEMORY_SIZE
	return if e then error(s) else writeFirst::<1>(s, s.memory.values[first(s.stack)]) fi

def mstore(State s) -> State:
	bool e = !has::<2>(s.stack) || first(s.stack) >= MEMORY_SIZE
	s.stack = decrease::<2>(s.stack)
	s.memory.values[first(s.stack)] = second(s.stack)
	return if e then error(s) else s fi

def identity(State s) -> State:
	return s

def main(u32 memoryHash, u32 stackHash, u8[16] program, private Calldata calldata):
	State s = State {
		stack: Stack { values: [0; STACK_SIZE], length: STACK_HEAD_START },
		memory: Memory { values: [0; MEMORY_SIZE] },
		error: false
	}

	u32 pc = 0
	for u32 i in 0..MAX_INSTR do
		u8 instr = program[pc]
		State s0 = add(s)
		State s1 = calldataload(s, calldata)

		s = if (instr == 1) then s0 else \
			if (instr == 2) then s1 else \
				error(s) \
			fi fi

		assert(!s.error)

	endfor

	assert(!s.error)
	return