Cleanup book and extended documentation about UPLC
This commit is contained in:
KtorZ
parent
c1a9eff5d0
commit
c5b1316d8e
|
|
@ -4,3 +4,6 @@ language = "en"
|
||||||
multilingual = false
|
multilingual = false
|
||||||
src = "src"
|
src = "src"
|
||||||
title = "The Aiken Programming Language"
|
title = "The Aiken Programming Language"
|
||||||
|
|
||||||
|
[output.html]
|
||||||
|
mathjax-support = true
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,8 @@
|
||||||
# Summary
|
# Summary
|
||||||
|
|
||||||
- [Intro](./introduction.md)
|
- [Introduction](./introduction.md)
|
||||||
- [Untyped Plutus Core](./uplc.md)
|
- [Untyped Plutus Core](./uplc.md)
|
||||||
- [Guides](./guides.md)
|
- [Syntax](./uplc/syntax.md)
|
||||||
- [Transactions](./guides/transactions.md)
|
- [Command-line utilities](./uplc/cli.md)
|
||||||
- [Fee estimation without a node](./guides/transactions/fee_estimation.md)
|
- [Builtins](./uplc/builtins.md)
|
||||||
- [Resources](./resources.md)
|
- [Resources](./resources.md)
|
||||||
|
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
# Guides
|
|
||||||
|
|
||||||
- [Transactions](./guides/transactions.md)
|
|
||||||
- [Fee estimation without a node](./guides/transactions/fee_estimation.md)
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
||||||
# Transactions
|
|
||||||
|
|
||||||
- [Fee estimation without a node](./transactions/fee_estimation.md)
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
# Fee estimation without a node
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
# Intro
|
# Introduction
|
||||||
|
|
||||||
Aiken is a new programming language and toolchain for developing
|
Aiken is a new programming language and toolchain for developing
|
||||||
smart contracts on the [Cardano](https://cardano.org) blockchain.
|
smart contracts on the [Cardano](https://cardano.org) blockchain.
|
||||||
|
|
@ -43,6 +43,4 @@ The Aiken project is made up of a few different components. The two most importa
|
||||||
ones are the high level Aiken language for writing smart contracts and a rust library
|
ones are the high level Aiken language for writing smart contracts and a rust library
|
||||||
for working with Untyped Plutus Core.
|
for working with Untyped Plutus Core.
|
||||||
|
|
||||||
### The Language
|
Learn more about them in the next sections of this book.
|
||||||
|
|
||||||
### Untyped Plutus Core
|
|
||||||
|
|
|
||||||
|
|
@ -1,35 +1,23 @@
|
||||||
# Untyped Plutus Core
|
# Untyped Plutus Core
|
||||||
|
|
||||||
## Usage
|
One key feature of Aiken is how it helps you manipulate Untyped Plutus Core
|
||||||
|
(abbrev. UPLC in short). UPLC is ultimately the format whereby codes gets
|
||||||
|
executed on-chain. This is pretty-much as low-level as you can get when it
|
||||||
|
comes to Cardano smart-contracts.
|
||||||
|
|
||||||
For now the command line application can only encode/decode Untyped Plutus Core
|
Understanding how UPLC works, and having the right tools to troubleshoot
|
||||||
to/from it's on chain format. See the roadmap below for a list of planned features and goals.
|
UPLC programs can be handy when developing contracts on Cardano. Fortunately,
|
||||||
|
this is something Aiken can help you with.
|
||||||
|
|
||||||
```sh
|
> **Note**
|
||||||
# help
|
>
|
||||||
aiken help
|
> While UPLC has erased any _explicit_ notion of types; functions, variables and
|
||||||
|
> constants are still _implicitly_ typed and, an interpreter will raise errors
|
||||||
# compile an untyped plutus core program to flat
|
> when encountering a type mismatch.
|
||||||
aiken uplc flat program.uplc
|
>
|
||||||
|
> For the sake of simplicity, we might speak about the type-signature of
|
||||||
aiken uplc flat program.uplc --print
|
> builtin functions such as `addInteger` which, in principle, only has a
|
||||||
|
> concrete meaning in Typed Plutus Core. Hence, even though they are _untyped_,
|
||||||
# output
|
> we often think of UPLC programs has having implicit types, as if they were
|
||||||
00001011 00010110 00100001 01001000
|
> originally _typed_ programs whose types had simply been erased (in fact,
|
||||||
00000101 10000001
|
> that's exactly what they are).
|
||||||
|
|
||||||
aiken uplc flat program.uplc --out=something.flat
|
|
||||||
|
|
||||||
# decode an untyped plutus core program from flat
|
|
||||||
aiken uplc unflat program.flat
|
|
||||||
|
|
||||||
aiken uplc unflat program.flat --print
|
|
||||||
|
|
||||||
# output
|
|
||||||
(program
|
|
||||||
11.22.33
|
|
||||||
(con integer 11)
|
|
||||||
)
|
|
||||||
|
|
||||||
aiken uplc unflat program.flat --out=something.uplc
|
|
||||||
```
|
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,80 @@
|
||||||
|
# Builtins
|
||||||
|
|
||||||
|
| Builtins | Type Args | Term Args | Result |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `ifThenElse`[^1] | \\(α\\) | (bool, \\(α\\), \\(α\\)) | \\(α\\) |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `addInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `subtractInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `multiplyInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `divideInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `modInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `quotientInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `remainderInteger` | \- | (integer, integer) | integer |
|
||||||
|
| `equalsInteger` | \- | (integer, integer) | bool |
|
||||||
|
| `lessThanInteger` | \- | (integer, integer) | bool |
|
||||||
|
| `lessThanEqualsInteger` | \- | (integer, integer) | bool |
|
||||||
|
| `greaterThanInteger` | \- | (integer, integer) | bool |
|
||||||
|
| `greaterThanEqualsInteger` | \- | (integer, integer) | bool |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `appendString` | \- | (string, string) | string |
|
||||||
|
| `emptyString` | \- | (string) | bool |
|
||||||
|
| `equalsString` | \- | (string, string) | bool |
|
||||||
|
| `encodeUtf8` | \- | (string) | bytestring |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `appendByteString` | \- | (bytestring, bytestring) | bytestring |
|
||||||
|
| `consByteString` | \- | (integer, bytestring) | bytestring |
|
||||||
|
| `indexByteString` | \- | (integer, bytestring) | integer |
|
||||||
|
| `sliceByteString` | \- | (integer, integer, bytestring) | bytestring |
|
||||||
|
| `lengthOfByteString` | \- | (bytestring) | integer |
|
||||||
|
| `emptyByteString` | \- | (bytestring) | bool |
|
||||||
|
| `equalsByteString` | \- | (bytestring, bytestring) | bool |
|
||||||
|
| `lessThanByteString` | \- | (bytestring, bytestring) | bool |
|
||||||
|
| `lessThanEqualsByteString` | \- | (bytestring, bytestring) | bool |
|
||||||
|
| `greaterThanByteString` | \- | (bytestring, bytestring) | bool |
|
||||||
|
| `greaterThanEqualsByteString` | \- | (bytestring, bytestring) | bool |
|
||||||
|
| `decodeUtf8` | \- | (bytestring) | string |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `chooseData`[^2] | \\(α\\) | (data, \\(α\\), \\(α\\), \\(α\\), \\(α\\), \\(α\\)) | \\(α\\) |
|
||||||
|
| `constrData` | \- | (integer, list data) | data |
|
||||||
|
| `unConstrData` | \- | data | (integer, list data) |
|
||||||
|
| `iData` | \- | (integer) | data |
|
||||||
|
| `unIData` | \- | (data) | integer |
|
||||||
|
| `bData` | \- | (bytestring) | data |
|
||||||
|
| `unBData` | \- | (data) | bytestring |
|
||||||
|
| `mapData` | \- | (list (pair data data)) | data |
|
||||||
|
| `unMapData` | \- | (data) | list (pair data data) |
|
||||||
|
| `listData` | \- | (list data) | data |
|
||||||
|
| `unListData` | \- | (data) | list data |
|
||||||
|
| `equalsData` | \- | (data, data) | bool |
|
||||||
|
| `serialiseData` | \- | (data) | bytestring |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `chooseList`[^3] | \\(α, β\\) | (list \\(α\\), \\(β\\), \\(β\\)) | \\(β\\) |
|
||||||
|
| `mkNilData` | \\(α\\) | (unit) | list \\(α\\) |
|
||||||
|
| `mkCons` | \\(α\\) | (\\(α\\), list \\(α\\)) | list \\(α\\) |
|
||||||
|
| `headList` | \\(α\\) | (list \\(α\\)) | \\(α\\) |
|
||||||
|
| `tailList` | \\(α\\) | (list \\(α\\)) | list \\(α\\) |
|
||||||
|
| `nullList` | \\(α\\) | (list \\(α\\)) | bool |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `mkPairData` | \\(α, β\\) | (\\(α\\), \\(β\\)) | pair \\(α\\) \\(β\\) |
|
||||||
|
| `fstPair` | \\(α, β\\) | pair \\(α\\) \\(β\\) | \\(α\\) |
|
||||||
|
| `sndPair` | \\(α, β\\) | pair \\(α\\) \\(β\\) | \\(β\\) |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `sha2_256` | \- | (bytestring) | bytestring |
|
||||||
|
| `sha3_256` | \- | (bytestring) | bytestring |
|
||||||
|
| `blake2b_256` | \- | (bytestring) | bytestring |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `verifyEd25519Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
|
||||||
|
| `verifyEcdsaSecp256k1Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
|
||||||
|
| `verifySchnorrSecp256k1Signature`[^4] | \- | (bytestring, bytestring, bytestring) | bytestring |
|
||||||
|
| --- | --- | --- | --- |
|
||||||
|
| `error` | \\(α\\) | (unit) | \\(α\\) |
|
||||||
|
| `trace` | \\(α\\) | (string, \\(α\\)) | \\(α\\) |
|
||||||
|
|
||||||
|
[^1]: Returns the second argument when the predicate is `True`, and the third argument when `False`.
|
||||||
|
|
||||||
|
[^2]: Each argument corresponds to each of the constructors of a builtin data (in this order): constr, map, list, integer and bytestring. The evaluation will continue with whatever branch actually corresponds to the given term value.
|
||||||
|
|
||||||
|
[^3]: Returns the second argument when the list is empty, and the third argument otherwise.
|
||||||
|
|
||||||
|
[^4]: Arguments are respectively: the public key, the message and the signature
|
||||||
|
|
@ -0,0 +1,128 @@
|
||||||
|
# Command-line utilities
|
||||||
|
|
||||||
|
## Evaluation
|
||||||
|
|
||||||
|
Let's consider the following basic program:
|
||||||
|
|
||||||
|
<p align="right"><strong>program_1.uplc</strong></p>
|
||||||
|
|
||||||
|
```
|
||||||
|
(program
|
||||||
|
2.0.0
|
||||||
|
[ [ (builtin addInteger) (con integer 16) ] (con integer 26) ]
|
||||||
|
)
|
||||||
|
```
|
||||||
|
|
||||||
|
We can evaluate this program using Aiken's cli via:
|
||||||
|
|
||||||
|
```console
|
||||||
|
$ aiken uplc eval program_1.uplc
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
Result
|
||||||
|
------
|
||||||
|
(con integer 42)
|
||||||
|
|
||||||
|
Costs
|
||||||
|
-----
|
||||||
|
cpu: 321577
|
||||||
|
memory: 602
|
||||||
|
|
||||||
|
Budget
|
||||||
|
------
|
||||||
|
cpu: 9999678423
|
||||||
|
memory: 13999398
|
||||||
|
```
|
||||||
|
|
||||||
|
The output indicates the result of the evaluation (`42`) as well as the
|
||||||
|
execution cost of that program, both in terms of CPU and memory usage.
|
||||||
|
|
||||||
|
Note that the command also accepts arguments. So, for example, if we modify our
|
||||||
|
program into a function that accepts an argument as follows:
|
||||||
|
|
||||||
|
<p align="right"><strong>program_2.uplc</strong></p>
|
||||||
|
|
||||||
|
```
|
||||||
|
(program
|
||||||
|
2.0.0
|
||||||
|
(lam x [ [ (builtin addInteger) (con integer 16) ] x ])
|
||||||
|
)
|
||||||
|
```
|
||||||
|
|
||||||
|
You can then instrument Aiken to provide arguments upon calling the program by
|
||||||
|
simply appending them to the `eval` command:
|
||||||
|
|
||||||
|
```console
|
||||||
|
$ aiken uplc eval program_2.uplc "(con integer 26)"
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
Result
|
||||||
|
------
|
||||||
|
(con integer 42)
|
||||||
|
```
|
||||||
|
|
||||||
|
## Formatting
|
||||||
|
|
||||||
|
Because writing UPLC by hand can be a tedious task, Aiken provides a quick way to automatically format
|
||||||
|
a UPLC program via the `fmt` command. By default, the command override the file given as input, but you
|
||||||
|
can also simply prints the result to stdout using `--print`. For example:
|
||||||
|
|
||||||
|
```console
|
||||||
|
$ aiken uplc fmt program_2.uplc --print
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
(program
|
||||||
|
2.0.0
|
||||||
|
(lam x [ [ (builtin addInteger) (con integer 16) ] x ])
|
||||||
|
)
|
||||||
|
```
|
||||||
|
|
||||||
|
## Converting to/from bytecode
|
||||||
|
|
||||||
|
So far, we've been representing UPLC programs using a high-level syntax. In
|
||||||
|
practice, however, UPLC programs are compiled into bytecode when submitted
|
||||||
|
on-chain.
|
||||||
|
|
||||||
|
Aiken provides means to convert a high-level UPLC program into a low-level flat
|
||||||
|
bytecode − and vice-versa, via the `flat` and `unflat` commands. For example:
|
||||||
|
|
||||||
|
```console
|
||||||
|
$ aiken uplc flat program_1.uplc --print
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
00000010 00000000 00000000 00110011
|
||||||
|
01110000 00001001 00000001 00000010
|
||||||
|
01000000 01101001
|
||||||
|
```
|
||||||
|
|
||||||
|
The `--print` flag instruments the command-line to print everything on stdout
|
||||||
|
in a readable way. Without the flag, the command creates a file `program_1.flat`
|
||||||
|
next to `program_1.uplc`.
|
||||||
|
|
||||||
|
> **Note**
|
||||||
|
>
|
||||||
|
> `aiken uplc flat program.uplc`
|
||||||
|
>
|
||||||
|
> and
|
||||||
|
>
|
||||||
|
> `aiken uplc flat program.uplc --out program.flat`
|
||||||
|
>
|
||||||
|
> are therefore equivalent.
|
||||||
|
|
||||||
|
From there, one can recover a UPLC high-level syntax from a flat program using
|
||||||
|
`unflat` as such:
|
||||||
|
|
||||||
|
```console
|
||||||
|
$ aiken uplc unflat program_1.flat --print
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
(program
|
||||||
|
2.0.0
|
||||||
|
[ [ (builtin addInteger) (con integer 16) ] (con integer 26) ]
|
||||||
|
)
|
||||||
|
```
|
||||||
|
|
@ -0,0 +1,74 @@
|
||||||
|
# Syntax
|
||||||
|
|
||||||
|
Let's start with a little reminder about the syntax. The complete syntax for Untyped Plutus Core comes from the original [Formal Specification of the Plutus Core Language](https://hydra.iohk.io/build/14133599/download/1/plutus-core-specification.pdf).
|
||||||
|
|
||||||
|
## Primitive Types
|
||||||
|
|
||||||
|
Plutus Core has 5 primitive types: `unit`, `bool`, `integer`, `string` and
|
||||||
|
`bytestring`. One can construct constants using the `con` keyword, followed by
|
||||||
|
the name of the primitive type and its value.
|
||||||
|
|
||||||
|
- Unit is denoted `()`;
|
||||||
|
- Bool are `True` or `False`;
|
||||||
|
- Bytestrings are denoted with a leading `#` followed by an hexadecimal sequence;
|
||||||
|
- Strings are UTF-8 text strings, between double quotes `"`.
|
||||||
|
|
||||||
|
| Primitive Type | Example |
|
||||||
|
| --- | --- |
|
||||||
|
| `unit` | `con unit ()` |
|
||||||
|
| `bool` | `con bool True` |
|
||||||
|
| `integer` | `con integer 42` |
|
||||||
|
| `bytestring` | `con bytestring #41696b656e` |
|
||||||
|
| `string` | `con string "Aiken"` |
|
||||||
|
|
||||||
|
## Functions
|
||||||
|
|
||||||
|
A function (or simply, lambda) is constructed with the keyword `lam` followed
|
||||||
|
by a variable name, and a term (i.e. a constant, another function, etc..). One
|
||||||
|
can apply variables to a function using squared brackets `[ ]`.
|
||||||
|
|
||||||
|
For example: `[ (lam x x) (con integer 42) ]`.
|
||||||
|
|
||||||
|
This little excerpt constructs a function that takes an argument `x` and returns
|
||||||
|
it; to which we immediately apply the constant `42`. If we were to evaluate this
|
||||||
|
program, it would simply output: `42`.
|
||||||
|
|
||||||
|
## Builtins
|
||||||
|
|
||||||
|
Plutus Core comes with a set of builtins functions which comes in handy to
|
||||||
|
define certain operations. Incidentally, there's no _operator_ even for basic
|
||||||
|
arithmetic operations, everything comes as a builtin.
|
||||||
|
|
||||||
|
You'll notice also that some builtins are very domain specific and tailored to
|
||||||
|
operations you'd expect a smart-contract to perform on a blockchain. Hence, new
|
||||||
|
builtins may be added in the future to address specific use cases that emerge.
|
||||||
|
|
||||||
|
Builtins are called with the keyword `builtin` followed by their names. They may
|
||||||
|
take one, two, three or really any number of arguments. The complete list of builtins
|
||||||
|
is given [in annexe](./uplc/builtins.md).
|
||||||
|
|
||||||
|
## Delay & Force
|
||||||
|
|
||||||
|
Plutus Core has the notion of type abstractions and type instantiations. That is, like lambdas are functions over term values, abstractions are functions over types. These abstractions allow to represent polymorphic types (such as, a list of elements, or an option type). UPLC has gotten rid of the types, but introduces two new keywords in order to preserve the abstractions in some form.
|
||||||
|
|
||||||
|
- `force` can be used on a polymorphic function to instantiate one type-parameter. For example, the branches of a builtin `ifThenElse` can be of any type -- though they have to be the same for both branches. In fact, `ifThenElse` has one type parameter. To be called, it must therefore be forced once: `[ [ [ force (builtin ifThenElse) p ] x ] y ]`
|
||||||
|
|
||||||
|
- Similarly, `delay` can be used to defer the evaluation of a certain term; this allows to artificially construct or preserve type abstractions, but also, to introduce a certain level of laziness in parts of the program.
|
||||||
|
|
||||||
|
## Data
|
||||||
|
|
||||||
|
In addition to primitive types, Plutus Core also has a more generalized `data`
|
||||||
|
data-type which is meant to represent any possible data-type in a program.
|
||||||
|
|
||||||
|
> **TODO**: Give additional detail about how the serialization is done and how
|
||||||
|
> to construct a Data.
|
||||||
|
>
|
||||||
|
> In particular, revisit after [#34](https://github.com/txpipe/aiken/issues/34)
|
||||||
|
> since the introduction of "list" and "pair" keywords may come in handy.
|
||||||
|
|
||||||
|
## Programs
|
||||||
|
|
||||||
|
Finally, UPLC programs are wraps in a `program` declaration, which indicates
|
||||||
|
the version (e.g. `1.0.0`) of Plutus Core that this programs uses. You don't
|
||||||
|
have to worry about that too much. Aiken supports the latest Plutus version
|
||||||
|
(`2.0.0`).
|
||||||
Loading…
Reference in New Issue