Plutus-core spec inconsistencies

[christianschmitz]

The file plutus-core-spec/draft-new-specification/plutus-core-specification.pdf (20th-may-2022) is much more recent than plutus-core-spec/plutus-core-spec.tex (6th-april-2021), and contains many updates which already seem to be in production. I suggest updating the latex file as quickly as possible, and updating the link in the repo root README.adoc file to point to the more recent pdf document.

Additionally there are some inconsistencies in the pdf document (mostly related to the flat encoding). In the remainder of this issue I will thus refer to the pdf document instead of the latex file.

I used the scripts in chris-moreton/plutus-scripts as a reference of correct compiler output.

• Page 23, section D.1, bottom paragraph: 'for ByteStrings and Strings we use a byte aligned array of bytes...', but on page 25, first bullet-point: `unsigned values of type integer and bytestring are encoded...'. So which is it? ByteStrings are like Strings, or like Integers? I'm assuming like Integers because Ascii only needs 7 bits.
• Page 23, section D.1, bottom paragraph: 'The structure is pre-aligned to the byte boundary...'. Is this really true? This byte boundary alignment is also mentioned on page 25, bottom paragraph of D.2, but I couldn't find any evidence of this in the reference scripts. I only noticed that the serialized plutus-core program is padded at the end using filler bits.
• It would be nice to know why the final filler bit is 1 and not simply 0.
• Page 23, section D.1, bottom paragraph: 'final 0 length block (the byte '0')'. This is very confusing: is the 'final' block something empty (i.e. length 0), or is it exactly 1 byte (i.e. '0')? I'm assuming something empty due to the heavy focus on not wasting space. If it is something empty it can simply not be mentioned at all?
• Page 25, section D.2, second-to-last paragraph: non-Haskell programs wouldn't know that 'Nil' and 'Cons' are linked list constructors, and would be very confused by this paragraph. In their minds 'Cons' could be short for 'constructor', 'constant, etc.. I suggest clarifying that the constants type-list is a linked list in the second paragraph of section D.2 (page 24), and more clearly stating that the second-to-last paragraph of D.2 (page 25) refers to linked lists (and that all lists in Plutus-Core are linked lists).
• Page 25, secion D.3, figure 14: the Lambda abstraction 'name' argument is absent in serialized form (they are unnecessary when using De Bruijn indices). I suggest removing 'name' from the Arguments column, or clearly stating that 'name' is empty in the serialized format.
• Page 25, section D.4, first paragraph: 'built-in functions use 8 bits' should be 'built-in functions use 7 bits'.
• Page 27, section D.5.2: 'using 3 bits to store the type of constant' should be 'using 4 bits to store the type of constant'. This mistake was probably made because type tags in Typed Plutus-Core use 3 bits. So I also suggest adopting clearer wording throughout the documentation to distinguish 'primitive constant'-type from the more abstract type tags which are only used in Typed Plutus-Core.
• Page 31, sections D.4.1 and D.4.2: labeling some leading 0 bits as Unused is confusing and unnecessary. I suggest removing these labels and including those bits as part of their tags/values.
• Appendix D: it would be nice if the real-world AlwaysSucceeds script was included as an example. Right now it isn't clear at all how exactly Datum, Redeemer, and ScriptContext are accessed in a plutus-core program.

Some cosmetic issues:

• Page 26, figure 15: MkNilPairData first letter capitalized, but page 19, table 3: mkNilPairData first letter not capitalized.
• Page 26, figure 15: doesn't include the Vasil builtin-functions mentioned on page 22, table 5. So I suggest including them, and adding some superscript symbols in figure 15 denoting from which version of Plutus-Core certain functions are available (assuming everything remains backwards compatible).
• Sometimes tables have a caption 'table', sometimes they have a caption 'figure'. I suggest always giving them a caption 'table'.
• The spec document should clearly note the version of Plutus-Core it describes. Past versions with non-backwards compatible features should be mentioned in appendices.

[kwxm]

Thank you for your comments. As it happens, we've been working on a more precise specification of the flat format recently and hope to make it public later this week. I think that should address most of the issues you mentioned. I'll add a message here when the updated document is available.

[kwxm]

@christianschmitz We've now updated the draft specification with a more detailed specification of the flat format which I hope will address most of your comments. It still lacks a proper specification of the CBOR encoding for the data type, but we'll add that in a week or two.

We're continuing to work on this and plan to replace the existing specification relatively soon. In the meantime we'll update the links in README.adoc as you suggested, but that requires a little work to get the right files in the right places.

Please let us know if you spot any more problems!

[christianschmitz]

Nice work! Looks like a pretty major rewrite.

All inconsistencies I mentioned have been resolved, and once the encoding of data has been elaborated this issue can probably be closed.

A few remarks:

• a small typo on page 34, first sentence of section D.4.1: 'hte' -> 'the'
• the new example (secton D.5) is much better, but perhaps a second example of a real-world script should be included in order to illustrate the handling of Datum, Redeemer and ScriptContext.

[christianschmitz]

I noticed something else:

The first tag of the Data type on the bottom of page 17 reads Constr Integer [Data]: so second argument is a list of Data (presumably the arguments of the constructor).

In table 3, page 19, constrData shows a similar interface: [integer, list(data)] -> data.

However in table 3, page 20, unConstrData isn't the exact inverse of constrData: [data] -> pair(integer, data). I was expecting pair(integer, [data]) as the return type of that function.

[christianschmitz]

Table 3, page 19: How exactly does mkCons fail? (consByteString doesn't fail for example).

[kwxm]

Table 3, page 19: How exactly does mkCons fail? (consByteString doesn't fail for example).

You had me worried there, but in a built-in list all of the elements have to be of the same (built-in) type, and mkCons will fail if you try to cons (for example) a boolean value onto a list of integers.

[christianschmitz]

Ok, I thought that might be why mkCons can fail.

Follow-up questions:

• Does ifThenElse throw a type error if its branches don't have the same type?
• I guess any Plutus-Core function can fail if one of its args has the wrong type?
• Would it be sensible to distinguish between type errors and other errors in table 3?

[kwxm]

Does ifThenElse throw a type error if its branches don't have the same type?

No. We have this (admittedly confusing) business with type variables a*, which are polymorphic over all terms, and type variables a#, which are polymorphic only over built-in types. The branches of ifThenElse are Plutus Core terms and there's an a* in the signature. In the typed version of the language (which we haven't added to this specification yet), the typechecker will reject calls to ifThenElse where the branches have different types (note that the signature of ifThenElse has two a*s, not an a* and a b*: that'll come into play in the specification of the typed language). However in the untyped language it's OK for the branches to be built-in constants of different types (a* effectively means "anything at all" in untyped Plutus Core). So in untyped Plutus Core you can have an ifThenElse where one branch is a string constant and another is an integer constant and that's OK. You might run into problems later if you try to use the result as an argument to multiplyInteger or something though. If you see a# in a signature it means that you can only supply built-in constants for the corresponding argument, and all arguments of type a# have to have the same built-in type at runtime (but if you also had an argument of type b# it could belong to some different built-in type).

I guess any Plutus-Core function can fail if one of its args has the wrong type?

Yes, at least for arguments which are of built-in types. The rules for the semantics and the evaluator use the ~ and ≈ relations to check that arguments are of the expected types, and evaluation fails if they're not.

Would it be sensible to distinguish between type errors and other errors in table 3?

Almost anything can fail because of a type error, so putting it in the table wouldn't be too helpful. It wouldn't do any harm to add a remark mentioning that somewhere near the table of builtins though; I'll do that the next time I'm editing the document.

[christianschmitz]

Page 21, note 3, second bullet point: now the condition is c_i == d_i, should it be c_i <= d_i ?

[kwxm]

Page 21, note 3, second bullet point: now the condition is c_i == d_i, should it be c_i <= d_i ?

Thanks, that was completely wrong! It should be fixed now.

[kwxm]

@christianschmitz We've now added a description of the CBOR format for Data, which I think should deal with almost all of the things you raised earlier.

However, you did suggest

perhaps a second example of a real-world script should be included in order to illustrate the handling of Datum, Redeemer and ScriptContext

I think that's probably out of scope for this document since it's talking about Cardano/EUTXO-specific issues and this document's only supposed to be about the language. Handling these objects is quite difficult though, and I don't know if we describe it anywhere: the plutus-tx compiler plugin generates the necessary code for us, so we don't really need to worry about that. However it would be difficult to work out what to do if you wanted to compiled some other language to Plutus Core, for example. I did look at the AlwaysSucceeds script but I think that that doesn't actually look at the Datum etc. and so doesn't generate the code to do so.

If you really want more information on how to handle these things then you could open another issue. I can't promise that we would do anything about it though!

[christianschmitz]

I've been using the Plutus-Core spec to develop an alternative smart contract DSL (https://github.com/Hyperion-BT/Helios/tree/dev).

AlwaysSucceeds in the DSL is:

func main() -> Bool {
    true
}

Which compiles down to the following (unoptimized) Plutus-Core (the DSL program is wrapped with ifThenElse/error):

(program 1.0.0 [
    (Λ 
        (Λ (Λ (Λ [
            [
                [
                    [(force (builtin ifThenElse)) [x4 ()]] 
                    (Λ ())
                ] 
                (Λ (error))
            ] 
            ()
        ])))
    ) 
    (Λ true)
])

Associated script address: addr_test1wzlmzvrx48rnk9js2z6c0gnul2063hl2ptadw9cdzvvq7vgy4qmsu (so you can kind of verify that it works with a block explorer)

I understand that handling of Datum/Redeemer/ScriptContext isn't related to the Plutus-Core spec and probably shouldn't be included as an example in the spec. But it would be nice to at least show what a real-world entry-point would look like, similar to the example above (basically an expression that evaluates to a triple nested lambda, where Datum would be applied to the outer lambda etc.).

This example is also nice because it shows:

• how force is necessary to use builtins with type parameters (1xforce per type parameter, so 2xforce for fstPair and sndPair)
• an implementation of ifThenElse branch deferral
• a Debruijn index in action

[kwxm]

I understand that handling of Datum/Redeemer/ScriptContext isn't related to the Plutus-Core spec and probably shouldn't be included as an example in the spec. But it would be nice to at least show what a real-world entry-point would look like, similar to the example above (basically an expression that evaluates to a triple nested lambda, where Datum would be applied to the outer lambda etc.).

@christianschmitz Apologies for neglecting this for so long: I was working on other things and lost track. I appreciate that it would be useful to have more examples of how to use this stuff for blockchain use, but it is a bit out of scope for the specification. May I suggest that you close this issue and open a new one that's specifically about how to use Plutus on the blockchain? I can't promise anything, but we are trying to improve our documentation at the moment. The response may be that we don't officially support low-level Plutus Core programming, but it's worth a try. At least if there's an indication that there's interest in how to use Plutus Core in real applications then it may steer us towards thinking about it a bit more.

[christianschmitz]

Seems fair. The documentation has come a long way. The .tex file will be made part of the repository at some point? Will close the issue now. Good job, thanks!

[kwxm]

The .tex file will be made part of the repository at some point?

Yes. We still need to finalise a few things, but we will make this the "official" version some time soon I hope.

Thanks for the comments, and come back if you have any more.