# EMO explainer

EMO stands for Ethereum Machine Oracle. The goal of the project is to make it easy to verify large computations off-chain, using an abstract machine of your choice. This is done by implementing a version of the [truebit verification game](https://people.cs.uchicago.edu/~teutsch/papers/truebit.pdf) that uses a generic abstract machine. Thus one only needs to implement the abstract Machine interface for their chosen machine to move their computations off-chain.

In this document we will attempt to give a semi-visual explainer of the internals of the project.

## The Machine

We model computation as something that is executed on an abstract machine we defined. This is a rough specification of the machine:

State   : Type
Seed    : Type
Image   : Type
bytes32 : Type (array of 32 bytes)
bool    : Type  = {true, false}

next       : State -> (State, bool)
project    : State -> Image
create     : Seed  -> State
isTerminal : State -> bool
stateHash  : State -> bytes32
imageHash  : Image -> bytes32

fst : forall a. (a, b) -> a
snd : forall b. (a, b) -> b

$$ \forall s1, s2 \in State : \\ stateHash(s1) = stateHash(s2) \land \\ snd(next(s1)) \ne false \land \\ snd(next(s2)) \ne false \implies \\ stateHash(fst(next(s1))) = stateHash(fst(next(s2)))$$

$$ \forall s \in State : isTerminal(s) = true \land \\ snd(next(s1)) \ne false \land \\ snd(next(s2)) \ne false \implies \\ stateHash(s) = stateHash(fst(next(s))) $$

$$ \forall s1, s2 \in State : \\ stateHash(s1) = stateHash(s2) \implies \\ imageHash(project(s1)) = imageHash(project(s2)) $$

To clarify this, let us consider an example machine which conforms to this interface. Imagine a simple adder machine, that gets a list of numbers as input and outputs their sum. Internallty, the machine uses a stack to store the remaining numbers it needs to sum. At each step of computation, the machine pops the top number and adds it to the running sum. So:

State = (int, Stack<int>) // the running sum and the remaining numbers
Seed  = List<int>         // the list of numbers to be summed
Image = int               // the final sum

// next       : pops the top number and adds it to the running sum
// project    : just retutns the running sum
// create     : creates a stack out of the input list and sets the running sum to 0
// isTerminal : returns true if stack is empty
// stateHash and imageHash commit to their respective types

For a visualization of this see the gif below.

## The stage

Now let us set the stage. Imagine 3 actors, Achilles, Bellerophon and Cadmus. Achilles is computationally limited and wants to know the sum of a list of numbers. So he asks his friends to compute it for him. Bellerophon is a good friend and does the following (if you find the gif too small, right click on the image and select open in new tab to get a larger version):


Cadmus however, wants to cheat and does the following:


Since Achilles can not run the computation himself, he has no way of knowing which of the 2 results is correct. What he can do though, is ask an oracle for the answer.

## The Oracle

The Oracle answers question of the type: "What is the Image that the execution of this Seed here produces?". In our example, Achilles would ask the Oracle: "What is the sum of 2, 3, 1, 2, 6 and 7?".

Internally, the Oracle works in the following simple fashion:

1. Achilles asks a question
2. Anyone can come and submit answers to the question
3. All the wrong answers are falsified by an entity called The Court
4. In the end only one correct answer will remain and will be given to Achilles

This is demonstarted visually in the GIF bellow

(asker should say answerer in the GIF)

Now the only thing left to clarify is how do we make sure only false answers actually get falsified.

## The Court

From the outside, all the Court does is observe the answers given to the Oracle and falsifies the wrong ones. Let us take a look into how this is achieved internally.

The Court works by handling disputes. A dispute is about whether an answer given to the Oracle is false. A dispute involves 2 parties - a prosecutor, who claims a specific answer is false, and a defendant, the actor who gave the answer to the Oracle.

Every dispute begins by a prosecutor, Diomedes for example, coming to the Court and saying: "The answer given by Cadmus - 0x1234aab..., is false!". Now the defendant - Cadmus, has a fixed period of time to respond. If he does not, the answer he gave is considered false and is falsified in the Oracle by the Court.

If you look at gifs 1 and 2, you can see every execution of a machine leaves behind a list of States. In his response, Cadmus has to bring a commitment in the form of a Merkle tree to a list of States, in which the first element is the State that is created from the Seed, and the last element is the State that projects into the Image that hashes to 0x1234aab...