chain.tex

\section{Blockchain layer}
\label{sec:chain}

\newcommand{\Proof}{\type{Proof}}
\newcommand{\Seedl}{\mathsf{Seed}_\ell}
\newcommand{\Seede}{\mathsf{Seed}_\eta}
\newcommand{\activeSlotCoeff}[1]{\fun{activeSlotCoeff}~ \var{#1}}
\newcommand{\slotToSeed}[1]{\fun{slotToSeed}~ \var{#1}}

\newcommand{\T}{\type{T}}
\newcommand{\vrf}[3]{\fun{vrf}_{#1} ~ #2 ~ #3}
\newcommand{\verifyVrf}[4]{\fun{verifyVrf}_{#1} ~ #2 ~ #3 ~#4}

\newcommand{\HashHeader}{\type{HashHeader}}
\newcommand{\HashBBody}{\type{HashBBody}}
\newcommand{\bhHash}[1]{\fun{bhHash}~ \var{#1}}
\newcommand{\bHeaderSize}[1]{\fun{bHeaderSize}~ \var{#1}}
\newcommand{\bSize}[1]{\fun{bSize}~ \var{#1}}
\newcommand{\bBodySize}[1]{\fun{bBodySize}~ \var{#1}}
\newcommand{\OCert}{\type{OCert}}
\newcommand{\BHeader}{\type{BHeader}}
\newcommand{\BHBody}{\type{BHBody}}

\newcommand{\bheader}[1]{\fun{bheader}~\var{#1}}
\newcommand{\hsig}[1]{\fun{hsig}~\var{#1}}
\newcommand{\bprev}[1]{\fun{bprev}~\var{#1}}
\newcommand{\bhash}[1]{\fun{bhash}~\var{#1}}
\newcommand{\bvkcold}[1]{\fun{bvkcold}~\var{#1}}
\newcommand{\bseedl}[1]{\fun{bseed}_{\ell}~\var{#1}}
\newcommand{\bprfn}[1]{\fun{bprf}_{n}~\var{#1}}
\newcommand{\bseedn}[1]{\fun{bseed}_{n}~\var{#1}}
\newcommand{\bprfl}[1]{\fun{bprf}_{\ell}~\var{#1}}
\newcommand{\bocert}[1]{\fun{bocert}~\var{#1}}
\newcommand{\bnonce}[1]{\fun{bnonce}~\var{#1}}
\newcommand{\bleader}[1]{\fun{bleader}~\var{#1}}
\newcommand{\hBbsize}[1]{\fun{hBbsize}~\var{#1}}
\newcommand{\bbodyhash}[1]{\fun{bbodyhash}~\var{#1}}
\newcommand{\overlaySchedule}[4]{\fun{overlaySchedule}~\var{#1}~\var{#2}~{#3}~\var{#4}}

\newcommand{\PrtclState}{\type{PrtclState}}
\newcommand{\PrtclEnv}{\type{PrtclEnv}}
\newcommand{\OverlayEnv}{\type{OverlayEnv}}
\newcommand{\VRFState}{\type{VRFState}}
\newcommand{\NewEpochEnv}{\type{NewEpochEnv}}
\newcommand{\NewEpochState}{\type{NewEpochState}}
\newcommand{\PoolDistr}{\type{PoolDistr}}
\newcommand{\BBodyEnv}{\type{BBodyEnv}}
\newcommand{\BBodyState}{\type{BBodyState}}
\newcommand{\RUpdEnv}{\type{RUpdEnv}}
\newcommand{\ChainEnv}{\type{ChainEnv}}
\newcommand{\ChainState}{\type{ChainState}}
\newcommand{\ChainSig}{\type{ChainSig}}

No translation between Shelley and Allegra chain state types
are required to transition between the eras.
A Shelley $\Tx$ can be decoded as an Allegra one, including decoding a
multi-sig script as a timelock one (the difference between them
is that timelock scripts have additional constructurs).
The one type that changes during era transition is only part of the transaction,
but does not appear in the chain state.

In Figure~\ref{fig:functions:to-ma}, we give the function $\fun{translateEra}$ that
specifies the translation of an Allegra-era chain state into a chain state that provides multi-asset support
(the Mary era).
We use $\ChainState_{\mathsf{Allegra}}$ to denote the type of the chain state
in the Allegra era, and $\ChainState$ for the Mary era chain state.
We use the notation $\var{chainstate}_x$ to represent
variable $x$ in the chain state. We do not specify the variables that remain
unchanged during the transition.
The only part of the state that is affected by the era transition is the UTxO, as
each UTxO map entry must be updated to contain a $\Value$ instead of $\Coin$.

%%
%% Figure - Allegra to Mary Transition
%%
\begin{figure}[htb]
  \begin{align*}
      & \fun{translateEra} ~\in~ \ChainState_{\mathsf{Allegra}}  \to \ChainState  \\
      & \fun{translateEra}~(\var{chainstate}_{\var{utxo}}) ~=~ \{~ \var{txin} \mapsto (a,\fun{inject}~c) ~\vert~
      \var{txin} \mapsto \var{(a,c)}\in ~\var{utxo}~\}
  \end{align*}
  \caption{Allegra to Multi-Asset Chain State Transtition}
  \label{fig:functions:to-ma}
\end{figure}