Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions Paper.tex
Original file line number Diff line number Diff line change
Expand Up @@ -850,7 +850,8 @@ \subsection{Execution Overview}

The empty sequence, denoted $()$, is not equal to the empty set, denoted $\varnothing$; this is important when interpreting the output of $H$, which evaluates to $\varnothing$ when execution is to continue but a series (potentially empty) when execution should halt.
\begin{eqnarray}
\Xi(\boldsymbol{\sigma}, g, I) & \equiv & X_{0,1,2,4}\big((\boldsymbol{\sigma}, \boldsymbol{\mu}, A^0, I)\big) \\
\Xi(\boldsymbol{\sigma}, g, I) & \equiv & (\boldsymbol{\sigma}'\!, \boldsymbol{\mu}'_g, A, \mathbf{o}) \\
(\boldsymbol{\sigma}, \boldsymbol{\mu}'\!, A, ..., \mathbf{o}) & \equiv & X\big((\boldsymbol{\sigma}, \boldsymbol{\mu}, A^0\!, I)\big) \\
\boldsymbol{\mu}_g & \equiv & g \\
\boldsymbol{\mu}_{pc} & \equiv & 0 \\
\boldsymbol{\mu}_\mathbf{m} & \equiv & (0, 0, ...) \\
Expand All @@ -868,10 +869,10 @@ \subsection{Execution Overview}
where
\begin{eqnarray}
\mathbf{o} & \equiv & H(\boldsymbol{\mu}, I) \\
(a, b, c) \cdot d & \equiv & (a, b, c, d)
(a, b, c, d) \cdot e & \equiv & (a, b, c, d, e)
\end{eqnarray}

Note that we must drop the fourth value in the tuple returned by $X$ to correctly evaluate $\Xi$, hence the subscript $X_{0,1,2,4}$.
Note that, when we evaluate $\Xi$, we drop the fourth element $I'$ and extract the remaining gas $\boldsymbol{\mu}'_g$ from the resultant machine state $\boldsymbol{\mu}'$.

$X$ is thus cycled (recursively here, but implementations are generally expected to use a simple iterative loop) until either $Z$ becomes true indicating that the present state is exceptional and that the machine must be halted and any changes discarded or until $H$ becomes a series (rather than the empty set) indicating that the machine has reached a controlled halt.

Expand Down