State and State Transition

Definition (State)

A state $S$ represents the state of a virtual machine.

Definition (State Transition)

• One-step transition function $F(S_{n}) = S_{n+1}$, where $S_n$ is pre-state, and $S_{n+1}$ is post-state. A verifier of the one-step transition is available on-chain (e.g., MIPS.sol)
• Multi-step transition function $F(F(….F(S_n))) = F^{(m)}(S_n) = S_{n+m}$

Definition (State Hash)

• Hash of state $H(S)$
• Initial state $S_0$ and initial state hash $H_0 = H(S_0)$ where both defender and challenger agree with

Claim and Counter Sub-Claims

Definition (Claim)

Given an pre-state hash $H_{pre}$, the post-state hash $H_{pst}$$H_{post}$after $m$ steps, $H_{post}$

• Type A Claim: claim that the post-state is correct, i.e. $C^{(m)} (H_{pre}) = H_{pst}$; or
• Type B Claim: claim that the post-state is not-correct $C^{(m)} (H_{pre}) \neq H_{pst}$

Definition (Validity of a Claim)

• A type A claim $C^{(m)} (H_{pre}) = H_{pst}$  is valid iff $H_{pst} = H(F^{(m)}(S_{pre}))$
• A type B claim $C^{(m)} (H_{pre}) \neq H_{pst}$ is valid iff $H_{pst} \neq H(F^{(m)}(S_{pre}))$

Definition (Root Claim)

The root claim is $C_1: C^{(M)} (H_0) = H_{M}$, where $M$ is the maximum steps of the fault proof game and $H_M$ the hash of end state. The defender agrees with the claim but the challenger disagrees with the post state and its hash $H_M$ and thus counters the root claim with a list of sub-claims.

Definition (N-section Counter Sub-claims)

Assuming $m$ can be fully divided by $N$ with $l = m / N$, a N-section counter sub-claims of a claim $C^{(m)}(H_{n}) \overset{\neq}{=} H_{n+m}$ are

• $C^{(l)}(H_{n}) = H'_{n+l}$