Skip to content

Specification of the built-in value type and functions #7810

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kwxm wants to merge 8 commits into
base: master
Choose a base branch
from
+618 −88
Open

Specification of the built-in value type and functions #7810

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
8bfa1fd
WIP
kwxm Jun 1, 2026
ca81c12
WIP
kwxm Jun 4, 2026
59c7df5
Clarify flat encoding of values
kwxm Jun 8, 2026
a1a43b3
Almost finished
kwxm Jun 8, 2026
a734713
Ready for PR
kwxm Jun 9, 2026
b7fb698
Update data
kwxm Jun 9, 2026
9e517ac
Add alternative names for currency and token IDs
kwxm Jun 15, 2026
e54a514
Update semantics of valueData to include size bound
kwxm Jun 18, 2026
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
4 changes: 2 additions & 2 deletions doc/plutus-core-spec/builtins.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -494,7 +494,7 @@ \subsubsection{Denotations of built-in functions}
\subsubsection{Results of built-in functions.}
\label{sec:builtin-results}
Recall from Section~\ref{sec:builtin-outputs} that the result of the
evaluation of a built-in function lies in the set
evaluation of a built-in function lies in the set
$$
(\R^+)_{\errorX} = \left(\bigdisj\left\{\denote{\tn}: \tn \in \Uni \right\} \disj \Inputs \right)^+ \disj \{\errorX\}.
$$
Expand All @@ -506,7 +506,7 @@ \subsubsection{Results of built-in functions.}
$$
which converts elements $r \in \R$ back into inputs by
$$
\reify{r} =
\reify{r} =
\begin{cases}
\reify{r}_{\tn} \in \Con{\tn} \subseteq \Inputs & \text{if $r \in \denote{\tn}$}\\
r & \text{if $r \in \Inputs$}
Expand Down
3 changes: 2 additions & 1 deletion doc/plutus-core-spec/cardano/builtins1.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -238,7 +238,8 @@ \subsubsection{Built-in functions}
\TT{sliceByteString} & $[\ty{integer}, \ty{integer}, \ty{bytestring]} $ \text {$\;\; \to \ty{bytestring}$}
& $(s,k,[c_1,\ldots,c_n])$ \text{$\;\;\mapsto [c_{\max(s+1,1)},\ldots,c_{\min(s+k,n)}]$}
& No & \ref{note:slicebytestring}\\[2mm]
\TT{lengthOfByteString} & $[\ty{bytestring}] \to \ty{integer}$ & $[] \mapsto 0, [c_1,\ldots, c_n] \mapsto n$ & No & \\[2mm]
\TT{lengthOfByteString} & $[\ty{bytestring}] \to \ty{integer}$
& $[] \mapsto 0, [c_1,\ldots, c_n] \mapsto n \ (n \geq 1)$ & No & \\[2mm]
\TT{indexByteString} & $[\ty{bytestring}, \ty{integer}] $ \text{$\;\; \to \ty{integer}$}
& $([c_1,\ldots,c_n],i)$ \text{$\;\;\mapsto
\begin{cases}
Expand Down
2 changes: 1 addition & 1 deletion doc/plutus-core-spec/cardano/builtins3.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ \subsubsection{Built-in functions}
imposed by Bitcoin (see~\cite{BIP-146},
\texttt{LOW\_S}) and \textbf{only accept the smaller signature};
\texttt{verifyEcdsa\-Secp\-256k1Signature} will return $\false$ if the larger
one is supplied.
one is supplied.

% For more on the lower signature business, see
% https://github.com/IntersectMBO/plutus/pull/4591#issuecomment-1120797931
Expand Down
Loading
Loading