timelock-language.tex

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


\begin{figure}[htb]
  \begin{align*}
    \fun{validateScript} & \in\Script\to\Tx\to\Bool \\
    \fun{validateScript} ~s~\var{tx}~& =~
                             \fun{evalTimelock}~\var{vhks} ~\var{itr}~\var{s} \\
                         & ~~~~\where \\
                         & ~~~~~~~~\var{vhks}\leteq \{\fun{hashKey}~vk \vert
                           vk \in \dom(\fun{txwitsVKey}~\var{tx})\} \\
                         & ~~~~~~~~\var{itr} \leteq \fun{txvldt}~ (\txbody~ \var{tx})
  \end{align*}
  \caption{Script Validation}
  \label{fig:functions-validate}
\end{figure}

In the ShelleyMA era, the
$\fun{validateScript}$ function performs validation of only timelock scripts,
see Figure~\ref{fig:functions-validate}. Note that while there is no explicit
support for validating multi-signature scripts in $\fun{validateScript}$,
these scripts remain effectively usable as the encodings of multi-sig and timelock
scripts are compatible. An existing multi-sig script-locked output is
spent by interpreting the encoded script as a timelock script (one without
any validity interval clauses), then validating it. For details, see the CDDL
specification.

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

\begin{itemize}
\item The script getting evaluated
\item The transaction
\end{itemize}

The semantics of the Timelock language are specified in Figure~\ref{fig:defs:tx-mc-eval}.
The evaluation of the scripts constructed by $\type{Signature}, \type{AllOf},
\type{AnyOf}, \type{MOfN}$ is done the same as for their
$\ScriptNI$ counterparts. The $\type{RequireTimeStart}$ evaluation
checks that the start of the transaction validity interval is not $\Nothing$, and is in or after
the slot specified by the constructor. The $\type{RequireTimeExpire}$ evaluation
checks that the end of the transaction validity interval is not $\Nothing$, and is in or before
the slot specified by the constructor.

\begin{figure*}[htb]
  \emph{Timelock Script Constructor Types}
  \begin{align*}
    & \type{evalTimelock} & \in \powerset{\KeyHash}\to(\Slot^? \times \Slot^?)\to\Timelock \to \Bool & \\
    & \text{The type of the Timelock script evaluator} \\~\\
    %
    & \type{Signature} & \in \KeyHash \to \Timelock & \\
    %
    & \type{AllOf} & \in \seqof{\Timelock} \to \Timelock & \\
    %
    & \type{AnyOf} & \in \seqof{\Timelock} \to \Timelock & \\
    %
    & \type{MOfN} & \in \N \to \seqof{\Timelock} \to \Timelock & \\
    %
    & \type{RequireTimeStart} & \in \Slot \to \Timelock &\\
    %
    & \type{RequireTimeExpire} & \in \Slot \to \Timelock &\\
  \end{align*}
  %
  \emph{Timelock Script Evaluation}
  \begin{align*}
    \fun{evalTimelock} & ~(\type{Signature}~hk)~\var{vhks}~\wcard =  hk \in vhks \\
    \fun{evalTimelock} & ~(\type{AllOf}~ts)~\var{vhks}~\wcard =
                              \forall t \in ts: \fun{evalTimelock}~t~vhks\\
    \fun{evalTimelock} & ~(\type{AnyOf}~ts)~\var{vhks}~\wcard =
                              \exists t \in ts: \fun{evalTimelock}~t~vhks\\
    \fun{evalTimelock} & ~(\type{MOfN}~m~ts)~\var{vhks}~\wcard = \\
                             & m \leq \Sigma
                               (\textrm{card} \{ t s.t. t \leftarrow ts \wedge \fun{evalTimelock}~\var{t}~\var{vhks} \}) \\
    \fun{evalTimelock} &~(\type{RequireTimeStart}~\var{lockStart})~\var{vhks}~\var{(\var{txStart}, \wcard)} \\
    & =~
    \begin{cases}
      \False & \var{txStart} = \Nothing \\
      \var{lockStart} \leq \var{txStart} & \text{otherwise}
    \end{cases} \\
    \fun{evalTimelock} &~(\type{RequireTimeExpire}~\var{lockExp})~\var{vhks}~\var{(\wcard, \var{txExp})} \\
    & =~
    \begin{cases}
      \False & \var{txExp} = \Nothing \\
      \var{txExp} \leq \var{lockExp} & \text{otherwise}
    \end{cases} \\
  \end{align*}
  \caption{Timelock 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 Timelock language.
%
% %% \begin{note}
% %%   sort out the constructors
% %% \end{note}
%
% \begin{figure*}[htb]
%   \begin{align*}
%     & \fun{evalTimelock} \in\Timelock\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{evalTimelock}  ~(\type{JustMSig}~s)~\var{pid}~\var{slot}~\var{vhks}
%      ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \fun{evalMultiSigScript}~s~\var{vhks} \\
%     & \text {checks the msig script}\\~\\
%     %
%     & \fun{evalTimelock}
%      ~\type{DoMint}~\var{pid}~ \var{slot}~\var{vhks} ~\var{txb}~\var{spentouts} \\
%     &~~~~ =~ \var{pid} \notin \dom~(\fun{mint}~\var{txb}) \\
%     & \text {checks that script hash of this script is not an asset ID being minted by tx}  \\~\\
%     %
%     & \fun{evalTimelock}
%      ~\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{evalTimelock}
%      ~(\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{evalTimelock}~(\type{Not}~s)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \neg ~\fun{evalTimelock}~s~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}\\~\\
%     %
%     &\fun{evalTimelock}~(\type{RequireAll}~ls)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \forall ~s'~ \in~ ls~:~\fun{evalTimelock}~s'~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}\\~\\
%     %
%     &\fun{evalTimelock}~(\type{RequireOr}~ls)~\var{pid}~\var{slot}~\var{vhks}
%     ~\var{txb}~\var{spentouts}
%    \\
%     &~~~~ = \exists ~s'~ \in~ ls~:~\fun{evalTimelock}~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{evalTimelock}
%      ~(\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{evalTimelock}
%      ~(\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{evalTimelock}
%      ~(\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{DoMint};~\type{JustMSig}~\var{msig});~\\
%     &~~~~~~ \type{RequireAll}~(\type{AssetToAddress}~\Nothing~\Nothing ;\\
%     &~~~~~~ (\type{Not}~\type{DoMint});~\type{SignedByPIDToken})) \\
%     %
%     & \text{msig is some MSig script containing signatures of some accreditation authority} \\
%     & \text{i.e. this authority can do any minting 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*}