Welcome to Melodeon!

Melodeon is a non-Turing-complete, yet powerful and general covenant language for the Themelio blockchain.

About Themelio covenants

Covenants are Themelio’s equivalent of “smart contracts” in its coin-based model. A covenant, somewhat analogous to a Bitcoin script, is a program attached to a coin (UTXO) that takes in a transaction and its execution context and decides whether or not that transaction can spend. On the blockchain itself, contracts are written in MelVM, a low-level stack-based “machine” language fulfilling a similar role as EVM in Ethereum.

Unlike coin scripts in most other UTXO blockchains, MelVM covenants are general-purpose, meaning that they can arbitrarily control the spending of a coin and are not limited to simple spending conditions like multi-signature requirements. This allows for essentially all on-chain constructs to be built on top of Themelio, such as naming systems, DeFi contracts, etc. (Note, though that the UTXO model is generally much more suited for event-focused logic that commits to rather than directly encodes application actions and data, rather than highly stateful business logic. This is an intentional choice to encourage using Themelio as a root of trust rather than an execution platform.)

About Melodeon

Melodeon is a high-level language that compiles to MelVM. It is:

Purely functional and stateless: There is no mutation, storage, or I/O, mirroring Themelio’s stateless, coin-based covenants. This avoids many subtle correctness issues that can emerge in traditional, Solidity-style blockchain contracts, and has the additional benefit of making the language easier to reason about.
Total: All programs in Melodeon provably terminate. This allows us to calculate the amount of computation each covenant requires and exactly how much fees to charge well in advance, avoiding the complexity of runtime gas accounting common in smart-contract languages. (This does mean Melodeon is not Turing complete, but we promise that it will feel like writing a normal, Turing-complete language)
Type-safe: All types must be known at compile-time and all the safety guarantees that come with it. Similar to languages like TypeScript, Typed Racket, and (some aspects of) ML, we use a structural typing system where types correspond to sets of values, rather than forcing a fixed hierarchy of type names.

This guide assumes some prior programming experience. Let’s dive right in!

Getting Started

While developing Melodeon covenants, we want to be able to run and test our code without deploying it onto a blockchain. Generally, this means using a REPL or read-eval-print-loop.

There are currently two official REPL tools: an offline, command-line tool called melorun, as well as an online playground.

Installing melorun

To install melorun, first make sure your machine has Rust installed. Then, open a terminal and enter the following command:

cargo install melorun

Quick start

Once melorun is installed, enter

melorun -i

in a terminal to fire up the REPL in interactive mode. Your terminal should display this prompt:

melorun>

Now, you can type any Melodeon expression following the prompt, hit enter, and the REPL will tell you what the expression evaluates to. It will also tell you the type of the expression after - :, something we will discuss shortly.

Examples:

melorun> 5
- : Nat [more specifically: {5}]
5

melorun> 1 + 7
- : Nat [more specifically: {8}]
8

melorun> (1 + 2) * 3
- : Nat [more specifically: {9}]
9

Executing covenants

To execute a complete covenant file (these must end in .melo) in the REPL, attach the file’s path to the end of the melorun command:

melorun filename.melo

To interact with definitions from a .melo file, add the -i flag:

melorun -i filename.melo

Before going into two examples, recall that covenants are run in an execution environment consisting of, in part, the transaction that is trying to spend the coin locked by the covenant. What value the covenant produces then determines whether the transaction is valid.

Trivial example

Here’s an example of a very simple covenant. First, create a file named demo.melo, with contents

def double(x: Nat) = 2*x

---

double(1)

This defines a function double that takes in a non-negative number and doubles it. In the main body of the covenant (separated by ---), we then call double with 1.

Then, open a fresh terminal and make sure you’re in the same directory as demo.melo. Next, type

melorun -i demo.melo

We see this output:

- : Nat
2 (truthy)
melorun>

This indicates that this covenant returned 2, which is a truthy value. In short, this means that this covenant will allow whatever transaction tries to spend a coin locked by it.

💡 Aside: Since we used melorun’s interactive mode, you can play with the double function in this REPL session:
melorun> double(2)
- : Nat
4

melorun> double(4+1)
- : Nat
10

More interesting example

Edit demo.melo to contain the following instead:

def double(x: Nat) = 2*x

---

double(vlen(env_spender_tx().outputs)) == 4

Now, this covenant instead requires that whatever transaction that spends the coin contain exactly 2 outputs. (see TODO documentation on env_spender_tx and Transaction)

Now if we run the covenant like this, we get a falsy value (meaning “transaction is rejected”):

$ melorun -i demo.melo
- : Nat [more specifically: {0..1}]
0 (falsy)

Hmm… what transaction is melorun handing to the covenant and getting rejected? It turns out that melorun by default populates the environment with a dummy transaction (more info in TODO):

melorun> env_spender_tx()
- : Transaction
[0, [[x"0000000000000000000000000000000000000000000000000000000000000000", 0]], [], 0, [x"420000"], "", []]
melorun> env_spender_tx().outputs
- : [CoinData;]
[]

We can instead specify a spend context, which contains further information about the transaction to generate for testing the covenant. Make a file context.yaml containing:

spender_outputs:
  0:
    covhash: t48dn3f3k4xfevwwx97hzrgxmgcz3b6xw2sdnkfb6c6e3erqjq2sh0
    denom: MEL
    value: 10000
    additional_data: ""
  1:
    covhash: t48dn3f3k4xfevwwx97hzrgxmgcz3b6xw2sdnkfb6c6e3erqjq2sh0
    denom: MEL
    value: 10000
    additional_data: ""

This specifies two transaction outputs. Now, if we run

$ melorun -i demo.melo -s context.yaml
- : Nat [more specifically: {0..1}]
1 (truthy)

we get a “truthy” result. We can see that the dummy transaction now has outputs:

melorun> env_spender_tx().outputs
- : [CoinData;]
[[x"436a378e64ebddbe73a93c7f88769067c6b37782cb6b37accc3386ec5e571662", 10000, "m", ""],
 [x"436a378e64ebddbe73a93c7f88769067c6b37782cb6b37accc3386ec5e571662", 10000, "m", ""]]

Simple Types

The most important thing about types in Melodeon is that types are sets of values. Here are a few example types:

{1}: the set containing the single number 1
[{1}, {2}, {3}]: the set containing the single vector [1, 2, 3]
Nat: the set of all natural numbers
Any: all values belong to the type Any
Nothing: no values belong to the type Nothing

An immediate consequence is that every value belongs to an infinite number of types. This means that it doesn’t make sense to say a type T is the type of a value x, only that T is a type of x or that T contains x.

Thus, let’s begin our discussion of Melodeon’s types with the different kinds of possible values.

Values

Melodeon has three kinds of values:

Naturals: any integer between 0 and 2^256-1, inclusive
Vectors: any fixed-length list. An example is [1, 2, 3]. Members of a vector can be of different types, like in [1, 2, [1, 2]].
Byte strings: any string of bytes. A byte string doesn’t have to be a valid string or be printable. There are two kinds of byte strings: ASCII strings and hex strings.
1. ASCII strings are enclosed by double quotes, like "melodeon"
2. Hex strings are enclosed by x"..", like x"deadbeef"

There are no negative integers, rationals, floating points, or any other sorts of numbers in the core Melodeon language. There are also no dedicated boolean values. In contexts that call for booleans, 0 has the semantic meaning of false, while all other values have the semantic meaning of truth. Hence, any value can be used where a boolean is expected.

Examples:

melorun> 1 == 2
0

melorun> 1 == 1
1

melorun> 3 && 4
4

melorun> if 35 then 1 else 0
1

Note that Bool is an alias for {0..1}.

Type constructors

Types are sets of values, but not every set of values is a type in Melodeon. For instance, the type containing all values except 1 is not a Melodeon type. Melodeon types are what can be expressed by the following type constructors, or by a combination of them with type union. We’ll denote “x is within type T” as x : T below.

Naturals
- Nat: all natural numbers modulo 2^256
- {n}: the type containing a single Nat n.
  
  Examples:
```
1 : {1}

2 : {2}

34 : {34}
```
- {m..n}: the type of the range of Nat’s from m to n, inclusive.
  
  Examples:
```
1, 2, 3, 4 : {1..4}

5, 6, 7 : {5..7}
```
Vectors
- [T_1, T_2, ..., T_n]: the type containing all vectors whose first element is a member of type T_1, second element is a member of type T_2, and so on.
  
  Examples:
```
[1, 2, 3] : [{1..2}, {2..3}, {3..4}]

[1, 3, [5]] : [{1}, {2..3}, [{4..6}]]
```
- [T; n] is an abbreviation for the type of a vector of length n whose members are all of type T. A concrete example is [Nat; 2], the set of all vectors of natural numbers of length 2.
- [T;] is the type containing all vectors of any length, whose members are all a member of type T. Vectors of arbitrary length are called dynamic vectors.
  
  Examples: [Nat;] is the set of all vectors of natural numbers. [Any;] is the set of all possible vectors.
Byte strings
- %[n] is the type including all byte strings of length n. Examples:
```
"melodeon" : %[8]

x"deadbeef" : %[4]
```
  (x"deadbeef is 4 hexadecimals!) Melodeon does not provide syntax for specifying types of particular byte strings, since such specificity for byte string types is rarely useful.
- %[] is the type including all byte strings. It can also be thought of as the type of dynamic byte strings.

Union types

The union of two Melodeon types is also a type. For example, {1} | {3} is a type that contains two elements 1 and 3 (the pipe symbol means type union in Melodeon). {1} | [{3}] is another type that contains elements 1 and [3].

Note: There are, however, no intersection or complement types, or any other set operations on types. This is because they would make it possible to express all of Boolean algebra in the type system, making typechecking equivalent to the Boolean satisfiability problem. As that problem is NP-complete, type-checking Melodeon programs will also be NP-complete (i.e. very hard). Back when we had type intersection in Melodeon, type-checking small programs took several minutes!

Exercise 3.1. Write down a union type that contains exactly 3 elements.

Subtyping

As you probably guessed, subtyping in Melodeon is the subset relation. That is, type U is a subtype of type T means that the set of values described by U is a subset of those described by T. For example,

{1} <: {1..5} <: Nat <: Nat | %[10]

where <: is notation for “is a subtype of” (it’s not a part of Melodeon syntax).

Every type is a subtype of itself, Nothing is a subtype of every possible type, and every type is a subtype of Any.

Type inference

Melodeon only performs local type inference. This means the type checker only infers the type of a value from its subexpressions, not from how it will be used in the future. A consequence is that the types of all function arguments must be manually annotated—the type checker cannot infer the type of a function argument based on how it will be used in the function body.

But if all values belong to an infinite number of types, what type does type inference assign to values? The answer is: the smallest type the compiler can determine given the context. This is the natural choice because it gives the most information about the value.

Here are a few examples:

melorun> 1
- : Nat [more specifically: {1}]

melorun> [1, 2]
- : [{1}, {2}]

melorun> "melodeon"
- : %[8]

melorun> if 1 == 2 then 3 else 4
- : Nat [more specifically: {3} | {4}]

melorun> [1, x"deadbeef", 3]
- : [{1}, %[4], {3}]

To reiterate, every value without a type annotation is assigned the most specific type that the compiler can determine from the immediate context.

Exercise 3.2. What type will the Melodeon compiler ascribe to the standalone expression

[x"f00d", 517, []]

Alias types

You can define aliases for existing types like this:

type Alias = existing_type

For example, we can rename Nat to Naturals:

type Naturals = Nat

The standard library implements Booleans as type aliases:

type False = {0}
type True = {1}
type Bool = True | False

Like any other type name, type aliases must start with an upper-case letter. Generally, type-level constructs (type alias and structure definitions) must be written in UpperCamelCase, while value-level constructs (variable and function names) should be snake_case. This is the same as Rust’s naming convention.

Expressions and Operators

Because it is a functional language without side effects, all useful computation in Melodeon produces a value. Something that evaluates to a value is an expression: so, everything is an expression in Melodeon.

Operators

Literals representing values are the simplest Melodeon expressions. The following built-in operators provide building-blocks for more complex expressions. As explained below, the operators are grouped by input. In the Precedence field, a larger value signifies a higher order of precedence (“tighter” binding).

Also, try out the operators in the REPL as you read along!

`Nat` operators

Operator	Meaning	Precedence
`x + y`	`x` plus `y`	5
`x - y`	`x` minus `y`	5
`x * y`	`x` times `y`	6
`x ** y`	`x` raised to the power of `y`	6
`x / y`	`x` divided by `y`	6
`x % y`	`x` modulo `y`	6
`>`	greater than	3
`>=`	greater than or equals to	3
`<`	less than	3
`<=`	less than or equals to	3
`==`	is equal to	3

Nat operators take natural numbers. For example, the compiler throws a type error if you try to compare two vectors with <=:

melorun> [1] <= [1, 2]
Melodeon compilation failed
~/.melorun.melo.tmp:3: error: expected a subtype of Nat, got [{1}] instead
    [1] <= [1, 2]
^~~~~~~~~~~~~

Logical operators

Operator	Meaning	Precedence
`!x`	not `x`	7
`x \|\| y`	short-circuiting `x` or `y`	1
`x && y`	short-circuiting `x` and `y`	1

Logical operators take any value as input, interpreting their inputs as booleans. As mentioned in the section on values, 0 is “falsy” and every other value is “truthy”.

Examples:

melorun> 0 || 1
1

melorun> 0 && 1
0

melorun> 1 && 2
2

melorun> !3
0

As you might have noticed from the examples, && and || are implemented with short-circuit evaluation.

x && y is equivalent to

if x then y else x

and x || y is

if x then x else y

Short-circuiting logical operators enable neat JavaScript-style idioms in Melodeon. For instance, suppose we want to multiply x by 2 if it’s a Nat, but x’s most specific type is Nat | %[8] (in other words, we only know x is either a Nat or a byte string of length 8). We can express this logic with

x is Nat && x * 2

In this expression, x is Nat is a boolean expression that evaluates to true if x is a member of type Nat (you can read about the is operator in Advanced Types). Because && has short-circuit logic, if x is Nat, then we’ll get the result of x * 2. If x is Nat is false, then x * 2 will never be evaluated, so we won’t ever get a type error.

Exercise 4.1. What does 0 || ([1] && "hello") evaluate to?

Bitwise operators

Operator	Meaning	Precedence
`<<`	left shift	4
`>>`	right shift	4
`\|`	bitwise or	2
`&`	bitwise and	2
`^`	bitwise xor	2
`~`	bitwise not	7

Bitwise operators take Nat’s as input, interpreting them as bit strings. Here are a few examples:

melorun> 1 << 2
4

melorun> 8 >> 2
2

melorun> 1 ^ 3
2

melorun> 6 & 4
4

melorun> 2 | 4
6

Try them out in the REPL!

Vector operators

Operator	Meaning	Precedence
`v ++ w`	append two vectors	5
`v[i]`	reference: returns element at `i`th index of `v`	8
`v[i..j]`	functional slice: returns a copy of `v` from index `i` to `j-1`	8
`v[i => x]`	functional update: returns a copy of `v` with `x` at index `i`	8

Vector operators take vector inputs. All vectors are 0-indexed. Also, all vector operators return newly created vectors or elements: nothing is ever mutated.

Slice

The slice operator v[i..j] returns a new vector that contains the elements of v between indices i and j, including i but not including j. For example:

melorun> let v = [1, 2, 3] in v[0..1]
[1]

melorun> let v = [1, 2, 3] in v[1..3]
[2, 3]

melorun> let v = [1, 2, 3] in v[0..3]
[1, 2, 3]

(note that let v = expr in body binds the variable v to the expression expr and evaluates body; we will discuss this further later)

Update

Here are a few examples of update. They emphasizes that update does not mutate the vector:

melorun> ([1, 2, 3] :: [Nat; 3])[1 => 3]
[1, 3, 3]

melorun> ([1, 2, 3] :: [Nat; 3])[2 => 5]
[1, 2, 5]

melorun> let v = [1, 2, 3] in (v :: [Nat; 3])[1 => 10] ++ v
[1, 10, 3, 1, 2, 3]

Exercise 4.2. Define vec as follows:

vec = ["melo", "deon"]

What does this expression evaluate to?

vec[1 => "haha"] ++ vec[1..2]

Structure operators

Operator	Meaning	Precedence
`s.x`	field access: returns the value associated with field `x` of structure `s`	8

This operator is analogous to vector reference. It’s included here for completeness; learn about structures and field access in Advanced Types and let expressions below.

For example, given a file containing this definition:

struct Point {
    x: Nat,
    y: Nat
}

we have:

melorun> let p = Point{ x: 1, y: 2 } in p.x
1

melorun> let p = Point{ x: 1, y: 2 } in p.y
2

Byte string operators

In Melodeon, ++ is an overloaded operator (that means it’s multiple functions with the same name). It also works for byte strings:

Operator	Meaning	Precedence
`s ++ t`	concatenates `s` and `t`	5

Exercise 4.3. Is "1" ++ [2] a valid Melodeon expression?

If expressions

Melodeon has an ML-like branching expression:

if x then y else z

This returns y if x is “truthy” (i.e. not 0), otherwise z. The inferred type of an if expression is the inferred type of y union the type of z. For instance,

melorun> if 35 then 1 else [10]
- : {1} | [{10}]
1

Exercise 4.4. What is the type of if 35 then 35 else "melodeon"?

Let expressions

Variable bindings in Melodeon are also expressions. They’re similar to variable bindings in ML languages:

let x = expression_1 in
expression_2

binds variable x to expression_1 in the scope of expression_2. Variable names must begin with a lower-case letter and contain only alphanumeric characters. Idiomatically, variables are written in snake_case. Here is an example:

melorun> let x = 1 in x + 2
3

Because let bindings are themselves expressions, they can be chained. For instance,

melorun> let x = 1 in let y = 2 in let z = 3 in x * y + z
5

You can also define multiple variables in one let expression, using this syntax:

let var_1 = expr_1,
    var_2 = expr_2,
    ...,
    var_n = expr_n
in
    expression

A concrete example:

melorun> let x = 1, y = 2 in x + y
3

Iteration expressions

Melodeon has three bounded iteration constructs: for, fold, and loop. Each has a stopping value that determines how many iterations are executed. This is the vector length in for and fold and the iteration number in loop. To prevent unbounded computation (whose fees cannot be pre-determined!), this stopping value must be known at compile time—that is, it must be a constant expression.

A constant expression is either a number whose value is known at compile time, or such numbers combined with + and * (other operators cannot be used in constant expressions). Numeric constants like 1 and 5 are constant expressions; so are 3 + 5 and 1 * 4. Constant generics are the final kind of constant expressions: learn about them in Advanced Types!

Melodeon does not currently support any form of recursion. We are considering adding provably bounded recursion similar to Fixpoint in Coq in the future.

`for`

for applies an expression to every member of a vector. It’s the equivalent of map in other functional languages. for has two equivalent forms:

for <variable> in <vector> collect <expression>

and also

[<expression> for <x> in <vector>]

which may be familiar from Python.

The collect keyword in the first syntax and the square brackets in the second indicate that the output of for is always a vector.

Examples:

melorun> for x in [1, 2, 3] collect x + 1
[2, 3, 4]

melorun> x && 0 for x in ["melo", "deon"]
[0, 0]

melorun> for n in [1, 2, 3] collect "4"
["4", "4", "4"]

for only works on fixed-length vectors, as we explained above. For example, if we cast the type of [1, 2, 3] in the first example above to a dynamic-length vector, then it will fail to compile.

melorun> for x in ([1, 2, 3] :: [Nat;]) collect x + 1
Melodeon compilation failed
~/.melorun.melo.tmp:15: error: list comprehension needs a list with a definite length, got [Nat;] instead
	for x in ([1, 2, 3] :: [Nat;]) collect x+1
	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Exercise 4.5. Write a for expression, in either syntax, that squares each element of the vector [1, 10, 100].

fold: WIP

Fold takes a vector, a base value, and a “collector” expression. It applies the expression to each element of the vector with the base value, updating the base value as it proceeds. Its syntax is

for x in vec fold accum = base with expr

where for every element of vec, fold computes expr and sets accum to be the new expr, and base is the starting value of accum. It’s typically used to combine the elements of a vector.

Examples:

melorun> for n in [1,2,3] fold y = 0 :: Nat with y + x
6

melorun> for x in [1,2,3] fold accum = 0 :: Nat with 5
5

melorun> for v in [[1], [2], [3]] fold accum = [] with accum ++ v
TODO!

WIP: casting rules for fold

Exercise 4.6. on casting: WIP

`loop`: pseudo-imperative loops

loop n do
    body
return ret

executes body n times and returns ret, where body is a chain of 0 or more pseudo-mutations of the form variable_name <- expression separated by semicolons, and n is a constant expression.

A pseudo-mutation is variable mutation restricted to the scope of the loop:

x <- new_value

sets a special copy of a previously defined variable x to new_value. This copy is in scope only in the loop body. So under the hood, this expression

let x = 0 in
loop 5 do
    x <- x+1
return x

is really

let x = 0 in
let y = 0 in
loop 5 do
    y <- y + 1
return y

Pseudo-mutations are only valid inside loop bodies.

Examples:

melorun> let x = 0 :: Nat in
            loop 5 do
            x <- x+1
            return x
5

melorun> let x = 0 :: Nat in
            loop 5 do
                x <- x + 1;
                x <- x + 1
                return x
10

Note: :: Nat here casts x to type Nat. Upcasting is necessary in these examples because the compiler automatically assigns type {0} to x in both cases (read about Melodeon’s type inference in Simple Types), but clearly the new values assigned to x do not belong to {0}. In general, mutated variables often need to be upcasted before mutation to avoid a type error.

To reiterate, the iteration number following the keyword loop must be a constant expression. An example of a non-constant expression is the argument to a function. To see this fail in action, try running the REPL with a .melo file containing this function:

def f(n: Nat) =
    let x = 0 in
    loop n do
        x <- x + 1
    return x

Here’s what we got:

❯ melorun -i loop.melo
Error: Melodeon compilation failed
~/loop.melo:4: error: expected const_mult_expr
	    loop n do
	         ^

Exercise 4.7. Using a loop, write an expression that produces 4 appended copies of the vector [1, 2] (evaluating to [1, 2, 1, 2, 1, 2, 1, 2]).

Assert and Fail

fail! crashes the program.

Examples:

melorun> fail!
MelVM exection failed

melorun> let x = 1 in (if x is %[] then "great!" else fail!)
MelVM execution failed

assert! expr1 in expr2

returns expr2 if expr1 evaluates to true, otherwise fail!. It’s equivalent to

if expr1 then expr2 else fail!

Examples:

melorun> assert! 1==1 in 3
3

melorun> assert! 1 == 2 in 3
MelVM execution failed

Functions

Unlike in most functional programming languages, functions are not first-class citizens in Melodeon. They cannot be passed as arguments into other functions (that is, Melodeon doesn’t have higher-order functions). Instead, they are always defined at the “top level”.

Here’s how to define a function in Melodeon:

def function_name(arg_1: type_1, arg_2: type_2, ..., arg_n: type_n) =
    expression

Argument type annotations are mandatory, as explained in the section on type inference. The function body must be a single expression.

Examples:

def double(x: Nat) = x * 2

def poly(x: Nat) =
    x ** 2 + quadruple(x) + 8

def quadruple(x: Nat) =
    loop 2 do
        x <- x + x
    return x

def to_point(x: Nat, y: Nat) =
    Point{x: x, y: y}

struct Point {
    x: Nat,
    y: Nat
}

As we see from these examples, the order of definitions does not matter in Melodeon. Furthermore, function and variable names must start with a lower-case letter and are idiomatically written in snake_case.

Optionally, you can annotate the output type, like this:

def double(x: Nat) : Nat = x * 2

def tuplify(x: Nat, y: Nat) : Point =
    Point{x: x, y: y}

Currently, all functions must be defined in .melo files; support for function definitions in the REPL is forthcoming!

Advanced Types

In this section, we’ll cover the somewhat more involved but definitely must-know aspects of Melodeon’s type system. These are type generics, constant generics, casting, and structures.

Generics

Melodeon provides generics in function definitions (see Rust’s explanation for an introduction). They are defined with a familiar syntax, where type variables are placed in angle brackets (<..>) after the function name. Here are a few examples:

def poly_equals<T>(x: T, y: T) =
    x == y


def compare_if_nat<U>(x: U, y: Nat) =
    if x is Nat then x == y else fail!

The purpose of generics is to make a function’s output type depend on its input type. For instance, consider the standard library’s definition of vref (vector reference) versus a similar function where x has the concrete type [Any;] rather than the generic type T:

# returns the nth element of x if it exists, otherwise 0

def vref<T>(x: [T;], n: Nat): T | False =
    if n < vlen(x) then
        unsafe_vref(x, n)
    else
        0

def any_vref(x: [Any;], n: Nat): Any | False =
    if n < vlen(x) then
        unsafe_vref(x, n)
    else
        0

Both functions accept vectors with elements of any type. However, from the return type annotations, we see that vref returns a value of type T | False (remember False is defined as an alias for {0} in the standard library), while any_vref returns an Any | False. This makes a big difference when you try to use the output:

melorun> vref([1, 2], 1) + 2
4

melorun> any_vref([1, 2], 1) + 2
Melodeon compilation failed
/~/.melorun.melo.tmp:58: error: expected a subtype of Nat, got Any instead
	any_vref([1, 2], 1) + 2
	^~~~~~~~~~~~~~~~~~~~~~~

any_vref’s return type Any is so uselessly broad that the compiler can’t tell its output belongs to type Nat. So, be sure to use generics when you want your function to accept arguments of different types and have a meaningfully specific return type.

Exercise 6.1. (TBD)

Const generics

Now, try writing a function that adds 1 to every member of a Nat vector. It should work on Nat vectors of any length. Here’s a first attempt:

def add1(vec: [Nat;]) =
    [x + 1 for x in vec]

Let’s try it out in the REPL…

❯ melorun -i demo.melo
Error: Melodeon compilation failed
/~/demo.melo:2: error: list comprehension needs a list with a definite length, got [Nat;] instead
	    [x + 1 for x in vec]
	    ^~~~~~~~~~~~~~~~~~~~

Ah right. Melodeon won’t iterate over any vector without a known constant length. How should we proceed?

We need something that parameterizes over vector lengths and other constants, not just types. This is are called const generics. In Melodeon, constant generic parameters are variables starting with a $. We can use them to define an add1 function that compiles:

def add1<$n>(vec: [Nat;$n]) =
    [x + 1 for x in vec]

❯ melorun -i demo.melo

melorun> add1([1, 2, 3])
[2, 3, 4]

Here are two more examples of looping with constant generics:

# returns the sum of all the members of a Nat vector

def members_sum_loop<$n>(vec: [Nat; $n]) =
    let x = 0 :: Nat in
    let i = 0 :: Nat in
    loop $n do
    	x <- x + vec[i];
    	i <- i + 1
    	return x

def members_sum_fold<$n>(vec: [Nat; $n]) =
    for x in vec fold
    	accum = 0 :: Nat
    	with accum + x

melorun> members_sum_fold([1,2,3,4])
10

melorun> members_sum_loop([1,2,3,4])
10

Exercise 6.2. Write a function that swaps the ith and jth elements of a vector. It should work on vectors of arbitrary length.

Exercise 6.3. Will this function compile? If not, why not, and rewrite it so that it compiles.

def f(vec: [Nat;]) =
    for i in vec fold accum = 0 :: Nat with accum + i

Statically enforcing function argument properties

We’ve already seen that constant generics are indispensable for looping over variable-length vectors or byte strings. You can also use them to statically enforce certain properties of function arguments. This is very expressive: for example, the function

def f<$n>(x: {2*$n}) = x * 2

has the set of all even Nat’s as its input type. The compiler enforces this restriction:

melorun> f(2)
4

melorun> f(1)
Melodeon compilation failed
/~/.melorun.melo.tmp:8: error: cannot fill type variables in argument type {(2 * $n)}, given concrete {1}
	f(1)
	^~~~

Given an input x to the function f, the compiler tries to find a concrete $n that solves x = 2 * $n. If it succeeds, the compiler replaces $n with that specific value during compilation, getting rid of the constant generic. This way, all constant generics are in fact constant expressions at run-time.

Another example of input specification using constant generics:

# returns the first member of a *non-empty* vector

def head<$n>(vec: [Nat; $n + 1]) =
    vec[0]

Specifying the length of head as $n + 1 restricts its inputs to non-empty vectors, because 1 is the smallest m for which there exists a Nat $n such that $n + 1 = m (alternatively, there is no natural number that satisfies the equation $n + 1 = 0). We see that the code will not compile with an empty vector:

melorun> head([])
Melodeon compilation failed
~/.melorun.melo.tmp:18: error: cannot fill type variables in argument type [Nat; ($n + 1)], given concrete []
	head([])
	^~~~~~~~

melorun> head([1])
1

Exercise 6.4. Write an identity function that statically enforces its input to be an odd-length byte string.

Exercise 6.5. Implement bubble sort in Melodeon. You might find swap from Exercise 6.2 handy.

In the above examples, the compiler tells us it couldn’t find a natural number $n that satisfies 1 = 2 * $n or 2 = 4 * $n or 0 = $n + 1, because none exists!

Manually specifying type variables

In more complicated cases, the compiler might just not be smart enough to figure out the correct types on its own. Here’s an example:

def f<$n>(x: {2*$n}) = x * 2

def g<$n>(x: {4*$n}) = x * 2

def h<$m>(x: {$m}) = g(f(x*2))

❯ melorun -i demo.melo
Error: Melodeon compilation failed
~/demo.melo:5: error: cannot fill type variables in argument type {(2 * $n)}, given concrete {($m * 2)}
	 def h<$m>(x: {$m}) = g(f(x*2))
	                        ^~~~

We can help out by manually specifying the type variables when calling g inside h:

def h<$m>(x: {$m}) = g<$n = $m>(f<$n = $m>(x*2))

Syntax

Finally, if you include both constant generics and type generics in the same function definition, the constant generics must be written before the type variables in the angle brackets.

Examples:


❯ melorun -i demo.melo
Error: Melodeon compilation failed
/home/thisbefruit/demo.melo:42: error: expected type_name
def app_type<T,$n>(x: [T; $n], y: T) =
^

Occurrence typing and `is` expressions

is expressions allow us to check whether a variable is a member of a certain type:


melorun> let x = 1 in x is Nat
1

melorun> let x = [1] in (if x is Nat then x else 0)
0

Note that is expressions do not work on literals (non-variables):


melorun> 1 is Nat
Melodeon compilation failed
~/.melorun.melo.tmp:3: error: expected EOI, add, sub, append, exp, mul, div, modulo, lor, land, lshift, rshift, bor, band, bxor, equal, gt, ge, lt, le, call_args, field_access, vector_ref, vector_slice, vector_update, as_type, or into_type
1 is Nat
^

Importantly, is expressions serve as type tests for occurrence typing in Melodeon. This is a typing technique that uses type tests to assign more specific types to the different occurrences of a variable in different branches of an if expression. Example:


# doubles vec[0] if vec has length 1, otherwise 0

def double_or_0(vec: [Nat;]) =
    if vec is [Nat; 1] then
        vec[0] * 2
    else
        0

melorun> double_or_0([1])
2

melorun> double_or_0([1, 2])
0

The program will not compile without the occurrence typing, since the compiler can’t check that it’s safe to access the 0th index of vec:


def double(x: [Nat;]) =
    x[0] * 2

❯ melorun -i demo.melo
Error: Melodeon compilation failed
error: type [Nat;] cannot be indexed into
x[0] * 2
^~~~

Another example:


melorun> let x = (if 1 == 2 then "contradiction!" else 0) in x + 2
Melodeon compilation failed
error: expected a subtype of Nat, got %[14] | {0} instead
let x = (if 1 == 2 then "contradiction!" else 0) in x + 2
^~~~~

Recall that an if expression is typed as the union of the types of its branches. This means that x has the type %[14] | {0} (i.e., byte strings of length 14 union {0}). That obviously is not a valid input type to +! We can refine the type of x using occurrence typing:


melorun> let x = (if 1 == 2 then "contradiction!" else 0) in
(if x is Nat then x + 2 else fail!)
2

Currently, the only type test supported in Melodeon is the is expression. We look forward to adding support for user-defined type tests (like these of Typed Racket) in future releases.

Exercise 6.6. Fill in the body of the function


def f(x: Any) = ...

so that it returns "bingo!" if x is a byte string of length 5 and "keep trying!" otherwise.

Casting

In the section on type inference, we mentioned that the Melodeon compiler assigns the most specific type it can to all values without type annotations. We can manually change the type ascription of any value or expression by safely casting it to a supertype or unsafely casting it to a subtype of its current type.

Up-casting

We can change the type assignment for a value to any supertype of its current assignment using the double colon operator, ::. Here are a few examples of successful super-casts:


melorun> 1 :: {1}
1

melorun> 1 :: {1..3}
1

melorun> 1 :: {1..3} :: Nat
1

You cannot cast to subtypes of the current type using :::


melorun> 1 :: Nat :: {1..3}
Melodeon compilation failed
~/.melorun.melo.tmp:3: error: cannot cast type Nat to non-supertype {1..3}
1 :: Nat :: {1..3}
^~~~~~~~~~~~~~~~~~

Here 1 :: Nat has type Nat, which is a supertype of {1..3}. Hence the second cast fails.

Up-casting for `loop`

We briefly mentioned up-casting in the introduction to loop. This is in fact a little tricky, because the type of the mutated variable undergoes the same mutation in each loop. So casting to any finite types will not work, even if it contains all the values x will be mutated to. For example:


melorun> let x = 0 :: {0..10} in
loop 5 do
    x <- x + 1
return x
Melodeon compilation failed
error: assigning value of incompatible type {1..11} to variable x of type {0..10}

Here, we cast the type of x to {0..10}, but the compiler inferred the type of x + 1 as {1..11}. So we have to cast x to Nat:


melorun> let x = 0 :: Nat in
loop 5 do
  x <- x + 1
return x
5

Exercise 6.7. Will this expression compile? If not, make the smallest possible change so that it does.


let x = 5 :: {1..10} in
loop 3 do
    x <- 7
return x

Downcasting and `unsafe`

In Melodeon, you can annotate any value x with an arbitrary type T using the transmutation operator, x :! T, except when the compiler can see that x can never be of type T. Transmutation comes in handy when you know for sure that a value belongs to a certain type, but the compiler isn’t smart enough to also know that.

Any expression containing :! must be preceded by the unsafe keyword. This is because changing a value’s type to a subtype is unsafe, as the compiler can’t prove that the value does in fact belong to the new type. Here we see the difference between manual downcasting to a subtype and occurrence typing: in occurrence typing, the down-cast is conditional on passing a runtime type test which proves that our value is a member of the subtype. In manual down-casting, there is no such guarantee.

Examples:


melorun> unsafe 1 :! [{1}]
1

melorun> unsafe let x = 1 in x :! %[]
1

melorun> let x = 1 in (unsafe x :! {2})
1

melorun> unsafe let x = 12 in
let y = 3 :: Nat in
loop 4 do
set! y = y + 1
return (x :! [Any;])
12

We see that the unsafe keyword can be put at any level of an arbitrarily complex nested expression, as long as it comes before any :!. The unsafe scope is the whole expression to the right of unsafe. You can have as many transmutations as you want within the scope of the unsafe keyword:


melorun> unsafe let x = 1 :! {2},
y = 2 :! {3},
z = 3 :! {4} in
"melodeon"
"melodeon"

melorun> unsafe let x = 1 :! {2} in let y = 3 :! {4} in x + y
4

Very importantly, :! only changes a value’s type annotation, not what it is as a value. So :! does not change the interpretation of the raw bits of the value (in contrast, transmutation in Rust and certain types of casting in C do). This is because values are prior to types in Melodeon, and transmutation operates on types. Thus, :! cannot make a value work with functions or operators for an incompatible type. Instead, it’s for when the type system is too restrictive about sound operations.

Examples:


def plus1(x: Nat) =
x + 1


melorun> unsafe let x = [1] :! {1} in plus1(x)
execution failed

melorun> unsafe let x = 1 :! %[1] in x ++ x
execution failed

A consequence is that although type annotations (with :: or :!) can change compile-time behavior (like whether a program type-checks), they do not affect run-time behavior. Here are some examples.

At run-time, x is T checks whether the value x, not its type annotation, is a member of the type T. So transmuting x will not change the result of any is expressions involving x:


melorun> unsafe let x = 1 :! {4} in x is {4}
0

melorun> unsafe let x = 1 :! %[] in x is %[]
0

Exercise 6.8. Recalling that True is the type alias for {1} defined in the standard library, what’s the result of this expression?


unsafe let x = 1 :! {0} in
let y = x is True in
y

Exercise 6.9. Will this expression compile? If so, what does it evaluate to? If not, why not?

WIP

Structures

Melodeon also has built-in structures, which are named vectors with named fields. To define a structure Name with fields var_1, ..., var_n, of types type_1, ..., type_n respectively, write in a file


struct Name {
var_1: type_1,
...,
var_n: type_n
}

Like type aliases, structure names should be in UpperCamelCase (in fact, the compiler enforces that they must begin with an upper-case letter).

An example structure definition is


struct Point {
x: Nat,
y: Nat
}

Here’s a particular instance of Point:


Point{ x: 1, y: 1 }

Field access

You can access a field of a structure s with this syntax:


s.field_name

For example:


melorun> let p = Point{x: 1, y: 10} in p.x
1

melorun> let p = Point{x: 1, y: 10} in p.y
10

Structure type

Structures are the one exception in Melodeon’s type system: they break the rule that types are sets of values. The structure type


struct Name {
var_1: type_1,
...,
var_n: type_n
}

is both the supertype and the subtype of the vector type


[type_1, ..., type_n]

So a structure type and its corresponding vector type correspond to the same set of values. Formally, however, the structure and the vector are distinct types.

Both subtype and supertype of vector types

The fact that one is both the supertype and subtype of the other means that they’re interchangeable when the only requirement is satisfying a subtype relation.

Example 1: because x :: T only asks whether x’s current type is a subtype of T, structs and their corresponding vectors are interchangeable as x. As a concrete example, a Point can be safely cast to [Nat, Nat] and used as one…


melorun> (Point{x: 1, y: 10} :: [Nat, Nat])[0]
1

melorun> for x in (Point{x: 1, y: 10} :: [Nat, Nat]) collect x \* 2
[2, 20]

melorun> let vec = Point{x: 1, y: 10} :: [Nat;] in
loop 2 do
set! vec = vec ++ vec
return vec
[1, 10, 1, 10, 1, 10, 1, 10]

…and vice-versa:


melorun> [1, 10] :: Point
[1, 10]

melorun> let p = [1, 10] :: Point in p.y
10

So any struct can be cast to its corresponding vector and vice versa. This means that with casting, structs and vectors are always compatible.

Example 2: as arguments to functions that don’t involve constant generics, vectors and structs are also compatible without casting:


def double(x: [Nat; 2]) =
    for i in x collect i*2

def slope(p1: Point, p2: Point) : Nat =
    let rise = (p2.y - p1.y) in
    let run = (p2.x - p1.x) in
    rise / run


melorun> double(Point{x: 1, y: 2})
[2, 4]

melorun> slope([0, 0], [1, 1])
1

Distinct from vector types

Then, the fact that structs and their corresponding vectors are distinct types means they’re incompatible in contexts that require more than a subtype relation. For example, you cannot use structs with vector operators or in for loops, because those call for actual vectors, not just a subtype of vectors:


melorun> Point{x: 1, y: 2}[0]
Melodeon compilation failed
~/.melorun.melo.tmp:70: error: type Point cannot be indexed into
Point{x: 1, y: 2}[0]
^~~~~~~~~~~~~~~~~~~~

melorun> Point{x: 1, y: 2}[0..1]
Melodeon compilation failed
(unknown location): error: type Point cannot be sliced into

melorun> for x in (Point{x: 1, y: 10}) collect x _ 2
Melodeon compilation failed
~/.melorun.melo.tmp:66: error: list comprehension needs a list with a definite length, got Point instead
for x in (Point{x: 1, y: 10}) collect x _ 2
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

To wrap up, every structure type corresponds to a vector type that is both its subtype and supertype. It’s distinct from that vector type, but it’s also interchangeable with the vector type where satisfying a subtype relation is the only constraint.

Exercise 6.10. Will the function h below take a Point structure as input? If not, why not?


def h<$n, T>(x: [T; $n+1]) =
    x[0]

Program Structure

An executable .melo file contains 0 or more definitions (these can be of functions, structures, and type aliases) and, optionally, three dashes (---) followed by a single expression.

Here’s an example file fibonacci.melo. It defines a fibonacci function and calls it on 15

# returns the nth fibonacci number, starting from 0
def fibonacci<$n>(n: {$n}) =
    let i = 0 :: Nat in
    let j = 1 :: Nat in
    let tmp = 0 :: Nat in
    loop $n do
        tmp <- j;
        j <- i + j;
        i <- tmp;
    return i

---

fibonacci(15)

When you start a REPL instance with fibonacci.melo, the expression fibonacci(15) is immediately evaluated:

$ melorun -i fibonacci.melo
- : Nat
610 (truthy)
melorun>

The three dashes are needed to end the definitions section because whitespace is insignificant in Melodeon, and Melodeon doesn’t have delimiters. While this makes Melodeon syntax both elegant and flexible, it also means that the compiler cannot tell where the last function definition ends and the standalone expression begins without some help from us.

Comments start with a single #. For an example, see the first line of fibonacci.melo above.

Modules: WIP

require, provide, and nested modules

opening directories in the REPL

Deploying Covenants

Now that we’ve learned the basics of Melodeon programs, we’ll learn how to actually deploy covenants onto the blockchain. Throughout this chapter, we use the following covenant as an example — a 2-of-3 multisignature:

let alice_public_key = x"b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e" in
let bob_public_key = x"37290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b" in
let charlie_public_key = x"315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb" in

(ed25519_signed_by(alice_public_key, 10) +
ed25519_signed_by(bob_public_key, 11) +
ed25519_signed_by(charlie_public_key, 12)) >= 2

More precisely, this checks that at least 2 of the following must be true:

the 11th signature (indices in Melodeon start with 0, so 10 is the 11th signature) of the spending transaction is a valid signature from Alice
the 12th signature is a valid signature from Bob
the 13th signature is a valid signature from Charlie

(see the TODO for ed25519_signed_by)

Testing covenants before deployment

Both melorun and the online playground support specifying the spend context. This is a special, YAML-formatted document that allows you to specify a particular spending transaction without constructing every field of it manually — see its spec.

Here, we only care about the ed25519_signers, which is a mapping betwween an integer n and the private key that signs the nth signature of the transaction. Put this in the spend environment:

ed25519_signers:
  # Alice's PRIVATE key
  10: 85f884fb8400117a29ef65b3a3ace00e7a6e1dde65479361c67e564fd00de417b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e
  # Bob's PRIVATE key
  11: 820384db2898cb4abaa6662de1087c955a7e08b13abcb69c8e7941a69ff372e437290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b
  # Charlie's PRIVATE key
  12: 35f29230304c0f0e0c730758caabd121a312dec4c1c0b859a75b1b59513ab4ca315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb

You can apply this spend environment with the -s flag of melorun, or just use the playground. Here, we sign the transaction with all three signatures that the covenant is looking for, which makes it return 1 (and allow the transaction through).

Feel free to play around by removing some of the signers — the covenant will still return 1 if at least 2 signatures are intact, but not otherwise.

Testing on the testnet

The next step now is to test our covenant live on the official testnet.

Compiling to MelVM bytecode

To do that, we need to first compile our Melodeon program to MelVM bytecode. This can be done with the -c (or --compile) flag of melorun. Run melorun -c -i multisig.melo, where multisig.melo contains the above covenant.

You’ll see something the following two lines on stdout:

t48rt8nvzc1kvc9s1040b7746mdgh8ty8a0pdwqc9kd6d45myq2hx0
f020b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e430021f02037290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b430022f020315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb430023f20102f201064200005043005ef2010c43005f42005e5342005f25a1000442005f42005e50a00001f20043005d42005da1000542005d420023420001320020a00001f200f2010642000050430053f2010b4300544200535342005425a1000442005442005350a00001f200430052420052a10005420052420022420001320020a00001f200f2010642000050430048f2010a4300494200485342004925a1000442004942004850a00001f200430047420047a10005420047420021420001320020a00001f200101024f20102f201064200005043003df2010c43003e42003d5342003e25a1000442003e42003d50a00001f20043003c42003ca1000542003c420023420001320020a00001f200f2010642000050430032f2010b4300334200325342003325a1000442003342003250a00001f200430031420031a10005420031420022420001320020a00001f200f2010642000050430027f2010a4300284200275342002825a1000442002842002750a00001f200430026420026a10005420026420021420001320020a00001f20010102621

The first line is the hash of the covenant in the standard “address” format, while the second line contains the hex-encoded MelVM itself itself.

Sending a coin locked by this covenant

The next step is to send a coin locked by this covenant. Let’s start melwalletd in testnet mode and use melwallet-cli to send some money to this covenant:

(in one terminal tab)

$ melwalletd --wallet-dir ~/.wallets --network testnet

(in another terminal tab)

We make a wallet demo with a bunch of testnet play money:

$ melwallet-cli create -w demo
$ melwallet-cli unlock -w demo

We can now send 100 (fake) MEL to the covenant hash we saw earlier:

$ melwallet-cli send -w demo --to t48rt8nvzc1kvc9s1040b7746mdgh8ty8a0pdwqc9kd6d45myq2hx0,100.0
TRANSACTION RECIPIENTS
Address                                                 Amount          Additional data
t48rt8nvzc1kvc9s1040b7746mdgh8ty8a0pdwqc9kd6d45myq2hx0  100.000000 MEL  ""
t92zte6gh26y5s02g9h31vgmnv0q4vya8paw5vghfe6c5b4hvj28pg  8.187089 MEL    ""
t92zte6gh26y5s02g9h31vgmnv0q4vya8paw5vghfe6c5b4hvj28pg  8.187089 MEL    ""
 (network fees)                                         0.000395 MEL
Proceed? [y/N]
y
Transaction hash:  630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b
(wait for confirmation with melwallet-cli wait-confirmation -w demo 630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b)

After this transaction confirms, this locks up 100 MEL at the first output of the transaction with hash 630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b, that can only be spent by a transaction that satisfies the covenant we wrote earlier. (You can even see it on Melscan — the above is a transcript of an actaul testnet deployment!)

Spending the locked coin

To test our covenant in action, the next step is to create a transaction that satisfies the covenant. This is actually a little tricky, since we must manually create a transaction with the signatures in exactly the right spots, something that’s generally not a built-in functionality of wallets like melwallet-cli/melwalletd. Instead, we need to create a transaction with the signatures from Alice, Bob, and Charlie “left blank”, then sign the transaction manually.

Note that in the following steps, we use bash/zsh syntax for string interpolation to avoid repeatedly typing long strings. On Windows, Git Bash is a good way of accessing bash syntax.

Creating the transaction: using any wallet, run the following melwallet-cli command:

$ melwallet-cli send -w demo --force-spend 630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b-0 --fee-ballast 1000 --add-covenant f020b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e430021f02037290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b430022f020315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb430023f20102f201064200005043005ef2010c43005f42005e5342005f25a1000442005f42005e50a00001f20043005d42005da1000542005d420023420001320020a00001f200f2010642000050430053f2010b4300544200535342005425a1000442005442005350a00001f200430052420052a10005420052420022420001320020a00001f200f2010642000050430048f2010a4300494200485342004925a1000442004942004850a00001f200430047420047a10005420047420021420001320020a00001f200101024f20102f201064200005043003df2010c43003e42003d5342003e25a1000442003e42003d50a00001f20043003c42003ca1000542003c420023420001320020a00001f200f2010642000050430032f2010b4300334200325342003325a1000442003342003250a00001f200430031420031a10005420031420022420001320020a00001f200f2010642000050430027f2010a4300284200275342002825a1000442002842002750a00001f200430026420026a10005420026420021420001320020a00001f20010102621 --dry-run > initial-prepared.hex

Let’s unpack this command a little. It asks the demo wallet to format a transaction that

sends all inputs back to demo’s own address — denoted by the lack of a --to argument
spends the covenant-locked coin we just created earlier — the out-of-wallet coin 630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b-0
adds additional fees to cover the signatures from Alice, Bob, and Charlie we’re gonna add later. A “fee ballast” of 1000 essentially instructs the wallet to calculate the fee level assuming the transaction will grow by at most 1000 bytes, plenty for most multisignature wallets.

Note: We cannot add fees after we obtain the signatures, because A, B, and C’s signatures need to sign off on a transaction that already has a fee.
supplies the content of the covenant inline as a huge hex string

Note: This is because when we created the coin, we locked it with the covenant through referring to the covenant hash. When we spend the coin, we then need to supply the actual contents of the covenant. This construct, borrowed from Bitcoin’s “pay-to-script-hash”, ensures that bulky covenants do not burden the coin state (and instead only need to be archived in the blockchain history, which does not need frequent access).

This does mean that any transaction that wants to spend a coin locked by a covenant must first obtain the full MelVM code for that covenant.
runs in “dry run” mode, which instead of attempting to send the transaction, merely prepares it and dumps it out as a hex string.
redirects the output to initial-prepared.hex, using bash syntax.

After running this command, initial-prepare.hex contains a large hex string representing the prepared transaction:

0001630024d8f526fa15cb53d40aec440e63ae32c636229696e312e66f311fee7c6b000217f4e34222378b900a0988c3b852bb05c9bf2916570bb845ee330ab24772122dfc28effa02016d0017f4e34222378b900a0988c3b852bb05c9bf2916570bb845ee330ab24772122dfc29effa02016d00fbaf020251420009f100000000000000000000000000000000000000000000000000000000000000064200005050f0205df45d38f0727ac106b053986c8f8696b78c57c3adf2f23c75f67144a74050ce420001320020fb0202f020b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e430021f02037290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b430022f020315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb430023f20102f201064200005043005ef2010c43005f42005e5342005f25a1000442005f42005e50a00001f20043005d42005da1000542005d420023420001320020a00001f200f2010642000050430053f2010b4300544200535342005425a1000442005442005350a00001f200430052420052a10005420052420022420001320020a00001f200f2010642000050430048f2010a4300494200485342004925a1000442004942004850a00001f200430047420047a10005420047420021420001320020a00001f200101024f20102f201064200005043003df2010c43003e42003d5342003e25a1000442003e42003d50a00001f20043003c42003ca1000542003c420023420001320020a00001f200f2010642000050430032f2010b4300334200325342003325a1000442003342003250a00001f200430031420031a10005420031420022420001320020a00001f200f2010642000050430027f2010a4300284200275342002825a1000442002842002750a00001f200430026420026a10005420026420021420001320020a00001f20010102621000140dcf2921c7651347bdddf0644e4a3511327733acc444ce73eb59f9e5e7c71424325b271db1b24776ff32085baba606cd8195a0a5b071a0a3577779d55212bbe02

Signing the transaction: we use the themelio-crypttool tool (which can be installed with cargo install themelio-crypttool) to manually sign the transaction. We sign with the three private keys (again, feel free to omit one, as this is a 2-of-3 multisig)

Sign with Alice’s private key, saving the result to signed-alice.hex:

$ themelio-crypttool sign-tx $(cat initial-prepared.hex) --posn 10 --secret 85f884fb8400117a29ef65b3a3ace00e7a6e1dde65479361c67e564fd00de417b5c7302463eda5f951d29ed1c6f7e9c7056628fb967b92653e0f9a1c15b6ad7e > signed-alice.hex

Sign with Bob’s private key, saving the result to signed-bob.hex:

$ themelio-crypttool sign-tx $(cat signed-alice.hex) --posn 11 --secret 820384db2898cb4abaa6662de1087c955a7e08b13abcb69c8e7941a69ff372e437290798b218b2312faa66f91191f6180c530df0fabf3f2791417e48d69d9b8b > signed-alice-bob.hex

Sign with Charlie’s private key, saving the result to signed-bob.hex:

$ themelio-crypttool sign-tx $(cat signed-alice-bob.hex) --posn 12 --secret 35f29230304c0f0e0c730758caabd121a312dec4c1c0b859a75b1b59513ab4ca315a04b0ca34049f5f47621da1b72cdeadbf51c5aacbbe14d88a8b9d77229deb > signed-alice-bob-charlie.hex

Sending the transaction: we use the send-raw verb of melwallet-cli:

$ melwallet-cli send-raw -w demo $(cat signed-alice-bob-charlie.hex)
TRANSACTION RECIPIENTS
Address                                                 Amount         Additional data
t92zte6gh26y5s02g9h31vgmnv0q4vya8paw5vghfe6c5b4hvj28pg  49.999656 MEL  ""
t92zte6gh26y5s02g9h31vgmnv0q4vya8paw5vghfe6c5b4hvj28pg  49.999657 MEL  ""
(network fees)                                         0.000687 MEL
Proceed? [y/N]
y
Transaction hash:  ac810425e235f52cb252bc3a0218688606c012edb29b5b75755019209a4e0812
(wait for confirmation with melwallet-cli wait-confirmation -w demo ac810425e235f52cb252bc3a0218688606c012edb29b5b75755019209a4e0812)

After the transaction confirms, we see on Melscan that the 100 MEL locked up (less fees) is sent back to demo’s address.

Deploying on the mainnet

Following the same steps with a mainnet melwalletd and mainnet money, you can deploy a 2-of-3 multisignature wallet that locks “real money” as well! One warning though — use “Alice”, “Bob”, and “Charlie”’s private keys at your own risk 😉

Covenant Design Patterns (WIP)

Solutions to Exercises

Solution 3.1. There’s no standard answer to this one. Here’s ours:

{1..2} | %[3]

Solution 3.2.

[%[2], {517}, []]

Solution 4.1.

Solution 4.2.

["melo", "haha", "deon"]

Solution 4.3.

Nope. You can only append two values of the same type. "1" ++ [2] fails to type-check and does not compile:

melorun> "1" ++ [2]
Melodeon compilation failed
~/.melorun.melo.tmp:3: error: cannot append values of types %[1] and [{2}]
	"1" ++ [2]
	^~~~~~~~~~

Solution 4.4.

{35} | %[8]

Solution 4.5.

Two alternatives:

[x * x for x in [1, 10, 100]]

for x in [1, 10, 100] collect x * x

Solution 4.6. WIP

Solution 4.7.

let x = [1, 2] in
loop 2 do
    set! x = x ++ x
    return x

Solution 6.1.

def six1<T>(x: T) = 
    if x is Nat then x + 1
    else (if x is [Any;] then x ++ [1]
        else if x is %[] then x ++ "1"
            else fail!)

Solution 6.2.

# swaps the ith and jth indices of vec

def swap<$n, T>(vec: [T; $n], i: Nat, j: Nat) =
    let v_i = vec[i] in
    let v_j = vec[j] in
    vec[i => v_j][j => v_i]

Solution 6.3. The function doesn’t compile, because the length of vec is unknown from its type definition. We can use a constant generic parameter to solve this problem:

def f<$n>(vec: [Nat;$n]) =
    for i in vec fold accum = 0 :: Nat with accum + i

Solution 6.4.

def ident<$n>(s: %[2 * $n + 1]) = 
    s

Solution 6.5.

# swap is defined in Solution 6.2

def bubble_sort<$n>(vec: [Nat; $n]) =
    loop $n do
        set! vec = 
            (let i = $n :: Nat in
            let j = $n-1 :: Nat in
            (loop $n do 
                set! vec =
                (if j > 0 
                then (if vec[$n - i] > vec[$n - j]
                    then swap(vec, $n - i, $n - j)
                    else vec)
                else vec);
                set! i = i - 1;
                set! j = j - 1;
                return vec))
        return vec

Note that the trick with decreasing i and j is for safely indexing into the vector with an expression involving $n, so that the compiler can prove the indices are safe.

Solution 6.6.

def f(x: Any) =
    if x is %[5] then "bingo!" else "keep trying!"

Solution 6.7. Yes, the expression compiles. In each iteration of the loop, x is mutated to the constant 7, which doesn’t depend on x. So the post-mutation type also doesn’t depend on the type of x: it’s the constant {7}. The compiler can check that {7} is a subtype of {1..10}, so all is good.

Solution 6.8.

Solution 6.9.

WIP

Solution 6.10. No, because the input to h needs to satisfy more than a subtype relation. It must satisfy the constraints imposed by the constant generic parameter $n. We can see this in the REPL:

melorun> h(Point{x: 1, y: 2})
Melodeon compilation failed
~/.melorun.melo.tmp:72: error: cannot fill type variables in argument type [T; ($n + 1)], given concrete Point
	h(Point{x: 1, y: 2})
	^~~~~~~~~~~~~~~~~~~~