mps-language.tex

\section{Script Constructors and Evaluation}
\label{sec:mps-lang}


\begin{figure}[htb]
  \begin{align*}
    \fun{validateScript} & \in\Script\to
    \powerset{\KeyHash}\to\TxBody\to\Bool \\
    \fun{validateScript} & ~s~\var{vhks}~\var{txb}~=
                           \begin{cases}
                             \fun{evalMultiSigScript}~s~vhks & \text{if}~s \in\ScriptNI \\
                             \fun{evalFPS}~s~\var{vhks} ~txb & \text{if}~s \in\ScriptMPS \\
                             \mathsf{False} & \text{otherwise}
                           \end{cases}
  \end{align*}
  \caption{Script Validation}
  \label{fig:functions-validate}
\end{figure}

We have updated the
$\fun{validateScripts}$ function, to allow for the validation of both the
multi-signature scripts and forging policy scripts, calling the appropriate
evaluator for each type of script, see Figure~\ref{fig:functions-validate}.

\begin{note}
  This appendix will change if we change anything about the language, it will go
  into the main part once it's more solidified
\end{note}

The arguments that are passed to the $\fun{validateScript}$ function include all those
that are needed for FPS and MSig script evaluation :

\begin{itemize}
\item The script getting evaluated
\item The set of key hashes (needed to use MSig scripts as FPS scripts)
\item The transaction body
\end{itemize}

Because of the extra arguments
(the $\TxBody$), we must also modify the call to this function
within the UTXOW rule, passing it the body of the signal transaction.

The semantics of the FPS language are specified in Figure~\ref{fig:defs:tx-mc-eval}.

\begin{figure*}[htb]
  \emph{FPS Script Constructor Types}
  \begin{align*}
    & \type{evalFPS} & \in\Script\to \powerset{\KeyHash}\to\TxBody\to\Bool & \\
    & \text{The type of the FPS script evaluator} \\~\\
    %
    & \type{JustMSig} & \in \ScriptMSig \to \ScriptMPS & \\
    %
    & \type{Interval} & \in (\Slot^? \times \Slot^?) \to \ScriptMPS &\\
    %
    & \type{AND} & \in \ScriptMPS \to \ScriptMPS \to \ScriptMPS & \\
    %
    & \type{OR} & \in \ScriptMPS \to \ScriptMPS \to \ScriptMPS & \\
  \end{align*}
  %
  \emph{FPS Script Evaluation}
  \begin{align*}
    & \fun{evalFPS}  ~(\type{JustMSig}~s)~\var{vhks}~\var{txb} \\
    &~~~~ =~ \fun{evalMultiSigScript}~s~\var{vhks} \\
    & \text {checks the msig script}\\~\\
    %
    & \fun{evalFPS} ~(\type{Interval}~\var{(i_s, i_f)})~\var{vhks}~\var{txb} \\
    &~~~~ =~
    \begin{cases}
      \True & (i_s = \Nothing)~\wedge~(i_f = \Nothing) \\
      (i_f' \neq \Nothing) \wedge (i_f'~\leq~i_f) & (i_s = \Nothing)~\wedge~(i_f \neq \Nothing) \\
      (i_s' \neq \Nothing) \wedge (i_s~\leq~i_s') & (i_s \neq \Nothing)~\wedge~(i_f = \Nothing)\\
      (i_s~\leq~i_s') \wedge (i_f'~\leq~i_f) & (i_s \neq \Nothing)~\wedge~(i_f \neq \Nothing)
    \end{cases} \\
    &~~~~~~~ \where \\
    &~~~~~~~~~~~ (i_s', i_f') = \fun{txvld}~{txb} \\
    & \text {checks that the tx validity interval is within the interval specified by the script}\\~\\
    %
    & \fun{evalFPS} ~(\type{AND}~s1~s2)~\var{vhks}~\var{txb}\\
    &~~~~ =~ (\fun{evalFPS}~s1~\var{vhks}~\var{txb}) \wedge (\fun{evalFPS}~s2~\var{vhks}~\var{txb})  \\
    & \text {checks that both scripts validate on the given inputs}  \\~\\
    %
    & \fun{evalFPS} ~(\type{OR}~s1~s2)~\var{vhks}~\var{txb}\\
    &~~~~ =~ (\fun{evalFPS}~s1~\var{vhks}~\var{txb}) \vee (\fun{evalFPS}~s2~\var{vhks}~\var{txb}) \\
    & \text{checks that one of the scripts validates on the given inputs}
  \end{align*}
  \caption{FPS Script Constructor Types and Evaluation}
  \label{fig:defs:tx-mc-eval}
\end{figure*}

% The Figures~\ref{fig:defs:tx-mc-eval},~\ref{fig:defs:tx-mc-eval-2},
% and~\ref{fig:whitelist-example} give
% possible constructors of the FPS language.
%
% %% \begin{note}
% %%   sort out the constructors
% %% \end{note}
%
% \begin{figure*}[htb]
%   \begin{align*}
%     & \fun{evalFPS} \in\ScriptMPS\to\PolicyID\to\Slot\to\powerset\KeyHash \\
%     &~~~~\to\TxBody\to\UTxO \to\Bool  \\
%     & \text{UTxO is only for the outputs THIS tx is spending, not global UTxO, i.e.} \\
%     & \text{when called,}~\var{spentouts}~=~(\fun{txins}~\var{txb}) ~\restrictdom~\var{utxo} \\~\\
%     %
%     & \fun{evalFPS}  ~(\type{JustMSig}~s)~\var{pid}~\var{slot}~\var{vhks}
%      ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \fun{evalMultiSigScript}~s~\var{vhks} \\
%     & \text {checks the msig script}\\~\\
%     %
%     & \fun{evalFPS}
%      ~\type{DoForge}~\var{pid}~ \var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \var{pid} \notin \dom~(\fun{forge}~\var{txb}) \\
%     & \text {checks that script hash of this script is not an asset ID being forged by tx}  \\~\\
%     %
%     & \fun{evalFPS}
%      ~\type{SignedByPIDToken}~\var{pid}~ \var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \exists~t\mapsto ~\_~\in~ \fun{range}~(\var{pid}~ \restrictdom~(\fun{ubalance}~\var{spentouts})) ~:~ t~\in~\var{vhks} \\
%     & \text{checks that tx is signed by a key whose hash is the name of a token in this asset}
%     \\~\\
%     & \fun{evalFPS}
%      ~(\type{SpendsCur}~\var{pid'})~\var{pid}~ \var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ (\var{pid'}~\neq~\Nothing ~\wedge ~\var{pid'}~\in~ \dom~(\fun{ubalance}~\var{spentouts}))\\
%     &~~~~~~ \vee (\var{pid'}~=~\Nothing ~\wedge ~\var{pid}~\in~ \dom~(\fun{ubalance}~\var{spentouts})) \\
%     & \text{checks that this transaction spends asset pid' OR itself if}~\var{pid'}~=~\Nothing
%     \\~\\
%     &\fun{evalFPS}~(\type{Not}~s)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \neg ~\fun{evalFPS}~s~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}\\~\\
%     %
%     &\fun{evalFPS}~(\type{RequireAll}~ls)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \forall ~s'~ \in~ ls~:~\fun{evalFPS}~s'~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}\\~\\
%     %
%     &\fun{evalFPS}~(\type{RequireOr}~ls)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \exists ~s'~ \in~ ls~:~\fun{evalFPS}~s'~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}\\
%   \end{align*}
%   \caption{Multi-asset Script Evaluation}
%   \label{fig:defs:tx-mc-eval}
% \end{figure*}
%
% \begin{figure*}[htb]
%   \begin{align*}
%     & \fun{evalFPS}
%      ~(\type{AssetToAddress}~\var{pid'}~\var{addr})~\var{pid}~ \var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \forall~(a, v)~\in~\fun{range}~(\fun{outs}~txb),~\\
%     &~~~~~~ \var{c}~\in~\dom~v~\Rightarrow~(a~=~ \var{a'} ~\wedge~
%                        v~=~\var{c}~ \restrictdom~(\fun{ubalance}~(\fun{outs}~txb)) \\
%     & \where \\
%     & ~~~~~~~ \var{a'}~=~\fun{if}~ \var{addr}~\neq~\Nothing~\fun{then}~\var{addr}~\fun{else}~\var{(pid',pid')} \\
%     & ~~~~~~~ \var{c}~=~\fun{if}~ \var{pid'}~\neq~\Nothing~\fun{then}~\var{pid'}~\fun{else}~\var{pid} \\
%     & \text{checks that tx outputs any pid tokens by themselves to the specified address} \\
%     & \text {the script address of the given asset when addr unspecified} \\~\\
%     & \fun{evalFPS}
%      ~(\type{TrancheTokens}~\var{tts}~\var{txin})~\var{pid}~\var{slot}~\var{vhks}
%      ~\var{txb}~\var{spentouts}  \\
%     &~~~~ =~(\var{pid}\mapsto\var{tts}~\in~\var{val})~ \wedge~(\var{txin}~\in~\fun{txins}~{txb}) \\
%     & \text{tranche tokens is incomplete} \\~\\
%     %
%     & \fun{evalFPS}
%      ~(\type{FreshTokens})~\var{pid}~\var{slot}~\var{vhks}
%      ~\var{txb}~\var{spentouts}
%       \\
%     &~~~~ =~\forall~\var{pid}~ \mapsto ~tkns ~\in~ \var{val}~:~ \\
%     &~~~~ \forall~t~\in~\var{tkns},~
%         \fun{nameToken}~(\fun{indexof}~\var{t}~\var{tkns},~\fun{txins}~{txb})~=~t
%     \end{align*}
%     \caption{Multi-asset Script Evaluation, cont.}
%     \label{fig:defs:tx-mc-eval-2}
% \end{figure*}
%
% \begin{figure*}[htb]
%   \begin{align*}
%     & \fun{whitelist} \in\ScriptMSig\to\Script  \\~\\
%     %
%     & \type{whitelist}  ~\var{msig}~ =~ \type{RequireOr}~
%       (\type{RequireAll}~(\type{DoForge};~\type{JustMSig}~\var{msig});~\\
%     &~~~~~~ \type{RequireAll}~(\type{AssetToAddress}~\Nothing~\Nothing ;\\
%     &~~~~~~ (\type{Not}~\type{DoForge});~\type{SignedByPIDToken})) \\
%     %
%     & \text{msig is some MSig script containing signatures of some accreditation authority} \\
%     & \text{i.e. this authority can do any forging or spending of this token} \\~\\
%     %
%     & (\fun{hashScript}~(\type{SpendsCur}~(\fun{hashScript}~(\type{whitelist}~\var{msig}))),~ \var{tkns}) \\
%     & \text{an example of an output spending which requires to be on a whitelist made by msig authority}
%   \end{align*}
%   \caption{Whitelist Script Example}
%   \label{fig:whitelist-example}
% \end{figure*}