Specification of the built-in value type and functions#7810
Conversation
kwxm
added
Specification
Builtins
No Changelog Required
| of currency and token identifiers appear, but for specification purposes it is | ||
| convenient to allow a \texttt{value} to contain \textit{all} identifiers, but | ||
| with only a finite number of quantities nonzero. In practice we only allow | ||
| values $v$ such that for $c, t \in \B$ with $v(c,t) \neq 0$, it is the case that |
There was a problem hiding this comment.
Should this be c, t \in \B^* ?
| \item $c_1 < c_2 < \cdots <c_n$ | ||
| \item $k_i \geq 1$ for $1 \leq i \leq n$ | ||
| \item $t_{i1} < t_{i2} < \cdots < t_{ik_i}$ for $1 \leq i \leq n$ | ||
| \item $q \in [-2^{127}, 2^{127}-1]\setminus 0$ for all $i$ and $j$ |
There was a problem hiding this comment.
Should this be q_{ij} \in instead of q \in?
| \noindent | ||
| We have $\unflatten{\flatten{v}} = v$ for all small values $v$ and | ||
| $\flatten{\unflatten{l}} = l$ for all well-formed $l$, the latter because | ||
| well-formed lists are a canonical representation of the function |
There was a problem hiding this comment.
What is meant here with a canonical representation of a function?
There was a problem hiding this comment.
What is meant here with a canonical representation of a function?
Hmmm. That sentence is a bit garbled. I guess I meant that for each value v, there's a unique well-formed list l with l↑ = v: without the well-formedness restriction there'd be many lists that represent the same function. I should probably just say that.
|
|
||
| \noindent where each $C_i$ and $T_i$ are literal bytestrings | ||
| described by the regular expression \texttt{\#([0-9A-Fa-f][0-9A-Fa-f])*} with at | ||
| most 32 pairs of hexadecimal digits and each $Q_i$ is a non-zero literal integer |
| \noindent | ||
| The expressions | ||
| \begin{verbatim} | ||
| (con value [(#33,[(#1234, 455]), (#2222, [(#9a, -7))])]) |
There was a problem hiding this comment.
The first entry is missing a closing parenthesis on the inner pair. The second has one too many.
| in its inputs, provided that all of the added values are in the 127-bit range: its denotation | ||
| \textsf{unionValue} is defined by | ||
| $$ | ||
| \mathsf{unionValue}(n, v) = |
There was a problem hiding this comment.
Should this be v, w instead of n, v?
There was a problem hiding this comment.
Should this be
v, winstead ofn, v?
Yep. I think I was being lazy and cutting and pasting.
| \note{Semantics of \texttt{scaleValue}.} | ||
| \label{note:scaleValue-semantics} | ||
| The result of \texttt{scaleValue} $n$ $v$ is $v$ with all quantities multiplied | ||
| by $n$, provided that all of the scaled values are in the 127-bit range: its denotation |
There was a problem hiding this comment.
Should this be 128-bit range?
There was a problem hiding this comment.
That's a good question. It's 128 bits, but signed, so I think I was thinking of that as really being 127 bits of actual number. Maybe it should say "signed 128-bit range" or something.
There was a problem hiding this comment.
Maybe it should say "signed 128-bit range" or something.
I eventually went with that.
| \note{Semantics of \texttt{unionValue}.} | ||
| \label{note:unionValue-semantics} | ||
| The result of \texttt{unionValue} is obtained by adding together corresponding quantities | ||
| in its inputs, provided that all of the added values are in the 127-bit range: its denotation |
There was a problem hiding this comment.
Same question about 128 bit here
I've gone through these sections, and I only found a few typo's and left a few questions. |
|
Thanks for spotting all the typos @basetunnel . I've fixed them and tried to clarify the discussion of the flattened form of values. |
|
There is one more minor comment that didn't get through because of github's review system. It should be visible now I hope (about serialization). |
2 participants
This updates the UPLC specification to include the
valuetype and builtins. I've attached a rendered PDF: the main things to look at are Section 4.3.6, in particular 4.3.6.3 and 4.6.3.4 (from page 50 onwards) and the flat encoding in Appendix C (pp 73/74). There's also a CBOR encoding forvaluebut I haven't added that because we won't need it until we add avaluefield todata. The parser is currently more permissive than what's described here, but I'll fix that shortly.We also need to specify casing on constants and update the section on versions (PV/LL etc). I'll do those in separate PRs.
plutus-core-specification.pdf