[go: up one dir, main page]

A new interpreter for Michelson

Yann Regis-Gianasrequested to merge
nomadic-labs/tezos:yrg@optimize-michelson-elaboration-and-execution into master

Preliminary remark

This MR is the merge of two previously closed MRs !2335 (closed) and !2374 (closed), which have been reviewed a bit already. To clean up the history, I have squashed lots of commits, probably a bit too much. I can rewrite the history if needed, do not hesitate to ask.

Context

This MR introduces a new datatype for Michelson intermediate representation as discussed in:

https://hackmd.io/@yrg/H1KC0PSdv

as well as a new interpreter based on that new IR.

This new interpreter is more efficient than the previous one.

It enjoys the following properties:

  • The interpreter is tail-recursive, hence it is robust to stack overflow. This property is checked by the compiler thanks to the [@ocaml.tailcall] annotation of each recursive calls.

  • The interpreter is type-preserving. Thanks to GADTs, the typing rules of Michelson are statically checked by the OCaml typechecker: a Michelson program cannot go wrong.

  • The interpreter is tagless. Thanks to GADTs, the exact shape of the stack is known statically so the interpreter does not have to check that the input stack has the shape expected by the instruction to be executed.

Dependency

This MR depends on !2329 (merged) and !2330 (merged) (and transitively on !2328 (merged) and !2327 (merged)).

Checklist

  • Document the interface of any function added or modified (see the coding guidelines)
  • [ ] Provide automatic testing (see the testing guide).
  • [ ] Add item in the Development Version section of CHANGES.md (only for new features and bug fixes).

Acks

  • @tomjack has implemented the *MAP and *ITER tail-recursive evaluation rules.

Reviewers

Edited by Yann Regis-Gianas

Merge request reports