Specify casing on built-in types - #7933
Conversation
kwxm
added
Plutus Core
Specification
Builtins
No Changelog Required
| \label{sec:builtin-casing} | ||
| In concrete implementations, some built-in types may admit \textit{casing}, | ||
| which allows them to be used as the scrutinee of the \texttt{case} construct. | ||
| One can write $\kase{M}{M_1 \ldots M_n}$ where $M$ evaluates to a |
There was a problem hiding this comment.
I've numbered branches from 1 to n here, rather than 0 to n-1. This allows us to use the case n=0 for the empty sequence, and avoids a lot of ?-1's elsewhere. What's annoying is that when we case on an integer, 0 selects the first branch, 1 the second branch, and so on, so we we have to have a k+1 there. That's only needed in one place though, as opposed to multiple -1's if we start from 0.
| built-in type $T \in \Uni$ we assume that there is a \textit{branch bound} | ||
| $\maxbranch(T) \in \N \disj \{\infty\}$ and a \textit{matching function} | ||
| $$ | ||
| \match{T}: \denote{T} \rightarrow \N \times \denote{\Uni}^* \disj \{\errorX\}. |
There was a problem hiding this comment.
I'm allowing the matching functions to return ⨯ here, signalling an error. We don't actually need that at the moment, but I think we will when/if @SeungheonOh's PR #7914 gets merged, since that will only work for Constr, and that'll have to be dealt with inside the matching function.
| % here. \ContinuedFloat makes the second part keep the same figure number and | ||
| % continue the subfigure lettering. | ||
| \begin{figure}[H]\ContinuedFloat | ||
| \begin{subfigure}[c]{\linewidth} |
There was a problem hiding this comment.
This renders pretty badly, taking up almost the entire width of the page. I couldn't think of a more compact way to do it though.
| \caption[]{A CEK machine for Plutus Core (continued)} | ||
| \end{figure} | ||
|
|
||
| \paragraph{Optimisations.} The machine presented above is suboptimal in a number |
There was a problem hiding this comment.
We talked about whether to include the implementation's optimisations in the specification, and I think we decided against it. This is my excuse for the discrepancies between the specification and the implementation. If we were really keen we could formalise both versions in Agda and prove that they produce the same results (although costs will unfortunately differ).
| the stack for each of the values $\reify{V_1}, \ldots, \reify{V_m}$ and these | ||
| then have to be popped off and processed one by one. It would be more efficient | ||
| to have a single frame which contains all of the values, and in fact this | ||
| optimisation is implemented in Cardano's production CEK machine. However we |
There was a problem hiding this comment.
| optimisation is implemented in Cardano's production CEK machine. However we | |
| optimisation is implemented in the Haskell implementation of Cardano's production CEK machine. However we |
Perhaps the above should also include a reference to where the implementation resides.
| \AxiomC{$\match{T}(c) = (i,(v_1, \ldots, v_k))$} | ||
| \AxiomC{$1 \leq i \leq n$} | ||
| % \RightLabel{\textsf{case-of-constr}} | ||
| \TrinaryInfC{$\step{\kase{\con{T}{c}{}}{M_1 \ldots M_n}}{\app{M_{i}}{\reify{v_1} \ldots \reify{v_k}}}$} |
There was a problem hiding this comment.
The way this rule is written indicates that evaluation gets stuck when the precondition isn't satisfied. However, in reality evaluation returns error in this case.
I think one way to fix this is to remove the precondition there, and the reduction rule rewrites to some function like 𝖤𝗏𝖺𝗅′ in the builtin evaluation case. The predicates in the precondition should be moved to the 𝖤𝗏𝖺𝗅′-like function, and if they are false the 𝖤𝗏𝖺𝗅′-like function returns error, if they are true they return the result you currently specified on the RHS of the reduction arrow.
There was a problem hiding this comment.
The way this rule is written indicates that evaluation gets stuck when the precondition isn't satisfied. in this case.
Oh, you're absolutely right. For some reason I was thinking that if there was no rule that matches the situation you're in then you get (error), but that's not the case at all: you've just got a value. I'll fix that. It probably needs to be dealt with in a way similar to how it's handled in the CEK machine.
There was a problem hiding this comment.
@ana-pantilie I think the rule for case on constr needs to be fixed as well: it branches on M_1 ... M_n according to the value of i and should fail if i doesn't lie between 1 and n, but at present it'll just get stuck.
2 participants
This adds a specification of the built-in casing mechanism. There's a PDF attached. The main changes are
data, which isn't merged yet and definitely isn't available on the chain).A later PR will update the stuff about versions (PV/LL/etc) at the start of Chapter 4 since that's now a bit out of date.
plutus-core-specification.pdf
I was going to add a changelog entry for this, but we don't have a changelog for documentation and the specification isn't included in the release.