Optz is an optimizer of Michelson programs, the base language for Tezos smart contract. It takes a Michelson code as input and then returns a smaller and more efficient equivalent code.

## Optimization of Michelson opcode sequences

The optimization consists of 2 parts: rule-based transformation and optimal stack manipulation search by A* algorithm.

### Rule based code transformation

Dozens of rewriting rules replace opcodes with better ones, such as:

```
PAIR; CDR => DROP
DIP n { a }; DIP n { b } => DIP n { a; b }
SWAP; op => op // when op is a commutative binary operator
NOT; IF { a } { b } => IF { b } { a }
```

### Search for the optimal stack manipulation sequences

After the rule-based transformation, A* algorithm finds the most optimal sequence of stack manipulation opcodes such as `DROP`

, `SWAP`

, `DIG`

, `DUG`

, `DIP`

, `DUP`

, `CAR`

, `CDR`

, `PAIR`

, `UNPAIR`

, and the push only opcodes like `PUSH`

and `EMPTY_SET`

. For example, the following opcode sequence found in an existing contract in Tezos mainnet:

```
DIG 1; DUP 1; DUG 2; PUSH c0; DIG 2; PUSH c1; DIG 4
```

is replaced with a shorter equivalent one:

```
PUSH c0; DIG 1; PUSH c1; DUP 4
```

The search space explodes exponentially when the range of the stack touched by the target opcodes and the number of constants in it grows. To finish the optimization in a reasonable time, the maximum size of the search space is introduced.

#### Special case for drop-only sequence

Compilers from higher-level languages to Michelson clean the stack when the program execution exits each functional and variable scope. We have observed some compilers tend to produce very long inefficient stack cleaning opcode sequences. They are too big for the above A* algorithm to optimize.

To optimize these stack cleaners, a special case of stack manipulation optimization is introduced for “drop only sequences”, which never push nor reorder stack elements but only drop some of them. The optimal opcodes are easily constructible for these drop-only sequences, therefore no size restriction is necessary. For example, the following code found in a smart contract in Tezos Mainnet:

```
DROP 2; DIG 1; DROP 1; DIG 1; DROP 1; DIG 3; DROP 1; DIG 3; DROP 1; DIG 4; DROP 1; DIG 4; DROP 1; DIG 4; DROP 1; DIG 4; DROP 1; DIG 4; DROP 1; DIG 4; DROP 1
```

can be optimized to the following much shorter efficient code:

```
DROP 2; DUG 2; DROP 2; DIG 3; DIG 4; DROP 2; DIP 4 { DROP 6 }
```

### Optimization of Tezos Mainnet contracts

We have tested Optz against 1711 different Michelson contracts deployed on Tezos Mainnet between 2021-02-18 and 2022-02-17.

All the contracts are optimized within 1 second by a laptop (Mac Book Pro 13-inch 2017) and the output Michelson encoding size is 92.8% of the inputs in average. Some are reduced by over 30%:

The optimization performance highly depends on how hard the original high-level language to Michelson compilers optimizes its code.

### What we learned

The drop-only sequence optimization greatly reduces the code sizes of outputs of some compilers. We recommend these compilers implement this optimization. It is cheap since the optimal opcodes can be constructed without a heavy A* search. All we need is a stack operation simulator.

### Presentation

For in-depth explanation, slides are available:

## Try Optz

### Web app

You can try the web interface of Optz at https://dailambda.jp/optz-js. It is compiled to JavaScript and optimizes the input in your web browser.

### Docker image

You can also use our Docker image. Use the following script as `optz.sh`

:

```
#!/bin/sh
docker run --rm \
-v `pwd`:/work dailambda/scaml:master \
/root/.opam/4.12.1/bin/optz $1
```

then give your script at the current directory to the script to optimize:

```
$ ./optz.sh your_contract.tz
# optimized: bytes: 2516 -> 2438
parameter
(...
```

### Source code

The source code is available at https://gitlab.com/dailambda/scaml. Optz was originally written as the last phase of optimization in SCaml compiler, an OCaml backend for Michelson. Since this phase is a pure conversion from Michelson to Michelson, we made it an independent tool. The build is quite straightforward if you have already set up OPAM environment correctly:

```
$ git clone https://gitlab.com/dailambda/scaml
$ cd scaml
$ opam switch create . ocaml-base-compiler.4.12.1 --deps-only -y
$ dune build
$ dune build install
```

## Related work

The idea of A* algorithm to optimize Tezos stack operations was originally published by Arthur Breitman. We did not notice this post when we started writing the optimizer using simple Dijkstra search. Later we extended our algorithm to A* and reduced the optimization times of some very heavy cases in Dijkstra.

## Updates (2022-05-06): Pair support of the optimal stack operation search

Optz’s optimal stack operation search now supports `CAR`

, `CDR`

, `PAIR`

, and `UNPAIR`

opcodes. For example, `UNPAIR; SWAP; DROP`

is now rewritten to `CAR`

. The longest rewrite we found in Mainnet contracts is as follows:

```
DUP 1; CAR; DIP 1 { CDR }; DUP 1; CAR; DIP 1 { CDR }; DUP 1; CAR; DIP 1 { CDR; } DIG 2; DUP 1; CAR; DIP 1 { CDR }; DIG 4; DUG 2
=> UNPAIR; UNPAIR; UNPAIR; DIG 3; DIG 3; UNPAIR
```

This support of the pair opcodes improves the average reduction rate of optimization from 94.0% to 92.8%.

`UNPAIR; PAIR => NOP`

is not always valid rewriting

At a first glance, the opcode sequence `UNPAIR; PAIR`

is trivially contractable to NOP, but it is *not* always valid due to the field annotation (`%name`

) of Michelson, therefore special care is required.

`UNPAIR; PAIR`

clears the field annotations of the pair type of the top stack element: ex. `pair (int %x) (int %y) => pair int int`

. Once the field annotations are removed, the pair type becomes compatible with other pair types with *any* field annotations, for example, `pair (int %a) (int %b)`

. If `UNPAIR; PAIR`

is removed, the result stack type keeps the original field annotations and becomes no longer compatible with pair types with other field annotations.

Indeed, we have found several Michelson codes in Tezos Mainnet whose `UNPAIR; PAIR`

cannot be removed away. For example,

```
IF { DIP { DROP } } { DROP; UNPAIR; PAIR }
```

is well-typed under the initial stack type `pair (int %a) (int %b); pair (int %x) (int %y); A`

and the result typestack type is `pair (int %a) (int %b); A`

. If `UNPAIR; PAIR`

is removed from the code, it is no longer well typed under the initial stack type, since `pair (int %a) (int %b)`

and `pair (int %x) (int %y)`

are incompatible.

It requires type analysis to know exactly whether `UNPAIR; PAIR`

and similar sequences are safely contractable, but Optz’s optimal stack operation search does not use types. Instead, it uses a conservative workaround: its rewriting has the following restriction: if a pair is formed by `PAIR`

in the input opcode sequence, it must be also created by `PAIR`

in the output. It makes sure the pair has a type without field annotations.