Michelson injection

If you have an existing piece of Michelson code that you want to use as-is, LIGO provides the ability to embed (inject) Michelson code. This feature can be useful when you need to have a deep level of control over the generated code, for example for optimisation, or if you need to use a feature from Michelson that is not yet supported by high-level constructions in LIGO.

Internal injection

The syntax for embedding Michelson is by means of the (Michelson ...) hook. The ellipsis is meant to denote a verbatim string annotated with a type, which contains the Michelson code to be injected in the generated Michelson and the type (that of a function) of the Michelson code.

const michelson_add = n =>

(Michelson `{ UNPAIR ; ADD }` as ((n: [nat, nat]) => nat))(n);

Note that the type annotation is required, because the embedded Michelson code is not type-checked by the LIGO compiler, which therefore assumes that the given type is correct.

In the example above, the notation ` ... ` is used to represent a verbatim string literal, that is, an uninterpreted string, which here contains a piece of Michelson code. The type annotation describes the behaviour of the Michelson code:

• It starts working on a stack consisting of a tuple of nats: [ nat * nat ].

• The tuple is destructured using UNPAIR: [ nat ] [ nat ].

• The two top values of the stack are added using ADD, and stops working on a stack consisting of a single nat: [ nat ].

The compiler will prevent changes to the embedded Michelson code if the function resulting from the embedded code is not applied. For example, let us see what happens when we compile an embedded Michelson expression that pushes some value on the stack, then drops it immediately, and then continues as a regular increment function.

The following command-line:

ligo compile expression jsligo "(Michelson `{ PUSH nat 42; DROP; PUSH nat 1; ADD }` : nat -> nat)"

outputs:

{ PUSH nat 42 ; DROP ; PUSH nat 1 ; ADD }

As we can see, the embedded Michelson code was not modified. However, if the resulting function is applied, then the embedded Michelson code could be modified/optimised by the compiler. To demonstrate this behaviour, a function call can be introduced in the example above by creating a lambda around the Michelson code. In this case, the first two instructions will be removed by the LIGO compiler because they have no effect on the final result.

The following command-line:

ligo compile expression jsligo "fun n -> (Michelson `{ PUSH nat 42; DROP ; PUSH nat 1; ADD }` : nat -> nat) n"

outputs:

{ PUSH nat 1 ; ADD }

External injection

Sometimes the Michelson code we wish to inject is better maintained externally, perhaps by a third-party, in which case we need to load the Michelson code in order to inject it.

This is achieved by the special hook (of_file ...), where the ellipsis is a verbatim string containing a file path to a Michelson file with extension .tz.

Injection of Michelson contracts

This is achieved by the special hook (create_contract_of_file ...), where the ellipsis is a verbatim string containg the file path to a Michelson file with extension .tz.

@entry

const main = (param: unit, _storage: unit) : [list<operation>, unit] => {

const [op, _addr] =

(create_contract_of_file `gitlab-pages/docs/mavryk/contracts/src/compiled.tz`)

(None(), 1mav, param)

return [list([op]), []];

}

where compiled.tz contains

{ parameter unit ;

storage unit ;

code { DROP ; UNIT ; NIL operation ; PAIR } }