A new Michelson interpretation in DCPS_AStack style
This MR replaces metastatedev/tezos!382 (closed)
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)).
Known limitations
This is still an intermediate step since the elaboration is not migrated yet to the new IR. As a consequence, a translation from the original IR to the new one is given temporarily. This translation is well-typed but still quite complex and not satisfying. Fortunately, it will not be required anymore when the new typechecker will be integrated through a subsequent MR.
Checklist
-
Document the interface of any function added or modified (see the coding guidelines) [ ] Provide automatic testing (see the testing guide).[ ] Add item in theDevelopment Versionsection ofCHANGES.md(only for new features and bug fixes).
Acks
- @tomjack has implemented the *MAP and *ITER tail-recursive evaluation rules.