Support semantic interpretation of instructions set of a simple contract

Motivation

Objective: Key Result:

Scope

The goal of this milestone is to demonstrate Polyrun on a small Michelson script. More precisely, we want to develop Polyrun to the point where it can generate all the aspects of a Michelson runtime but on a small subset of Michelson.

The contract

parameter string;
storage (map string int);
code
  {
    AMOUNT ;
    PUSH mutez 5000000;
    COMPARE; GT;
    IF { FAIL } {};
    DUP; DIP { CDR; DUP }; CAR; DUP ;
    DIP
      {
        GET; ASSERT_SOME;
        PUSH int 1; ADD; SOME
      };
    UPDATE;
    NIL operation; PAIR
  }

The initial storage could be something like {Elt "Loana" 0; Elt "Steevy" 0}

ASSERT_SOME is a macro for IF_NONE{UNIT;FAILWITH}

So we need to support the following instructions

ADD AMOUNT CAR CDR COMPARE DUP DIP FAILWITH GT GET IF IF_NONE NIL PAIR PUSH SOME UPDATE UNIT

Work breakdown

For each instruction we need to support the generation of

the instruction definition (OCaml GADT)
the instruction typing (Ocaml parse_instr, Rust pop_cast)
the instruction interpretation (Ocaml step function, Rust ?)

For instruction definitions, ToT relies on tezos-rust-sdk crate. So adding/modifying instructions will require either to remove the dependency or to modify concurrently the two projects. We delay that in a future milestone and will rely on existing crate for now.

for each of this component,

first provide a data-model that holds the needed information
write/adapt the backend transformer that produces the relevant part in OCaml and Rust
bridge the data-model with the available description or modify the input structure

Per instruction:

simple operator

`GT`

Algebraic destructors

`CAR`

instruction definition tezos/tezos!8720 (merged)
- Ocaml
the instruction typing
- Ocaml
- Rust !27 (merged)
the instruction interpretation
- (days) semantic rule definition in data-model !35 (merged)
- (hours) Ocaml generation
- (hours) Rust generation !35 (merged)
- (days) from description to semantic rule !43 (closed)

`CDR`

instruction definition tezos/tezos!8720 (merged)
- Ocaml
the instruction typing
- Ocaml
- Rust !27 (merged)
(hour once CAR is done) the instruction interpretation
- (hour) semantic rule definition in data-model
- (free ?) Ocaml generation
- (free) Rust generation
- (free) from description to semantic rule

Constructor

`UNIT`

Polymorph constructor

`SOME`

`NIL`

Polymorph with optional n parameter

`DUP`

instruction definition !2 (merged), !14 (merged), !21 (merged)
- Ocaml
the instruction typing
- Ocaml
- Rust
(days) the instruction interpretation
- (hours) semantic rule definition in data-model
- (hours) Ocaml generation
- (hours) Rust generation
- (hours) from description to semantic rule

Support semantic interpretation of instructions set of a simple contract

Motivation

Scope

Work breakdown

Per instruction:

simple operator

`GT`

Algebraic destructors

`CAR`

`CDR`

Constructor

`UNIT`

Polymorph constructor

`SOME`

`NIL`

Polymorph with optional n parameter

`DUP`

`PAIR`

with data parameter

`PUSH`

Overloading

`ADD`

`GET` (at least on map)

`UPDATE` (on map)

`COMPARE` (at least on mutez)

Chain's context dependent

`AMOUNT`

Control flow

`IF`

`DIP`

`FAILWITH`

Support semantic interpretation of instructions set of a simple contract

Motivation

Scope

Work breakdown

Per instruction:

simple operator

GT

Algebraic destructors

CAR

CDR

Constructor

UNIT

Polymorph constructor

SOME

NIL

Polymorph with optional n parameter

DUP

PAIR

with data parameter

PUSH

Overloading

ADD

GET (at least on map)

UPDATE (on map)

COMPARE (at least on mutez)

Chain's context dependent

AMOUNT

Control flow

IF

DIP

FAILWITH

`GT`

`CAR`

`CDR`

`UNIT`

`SOME`

`NIL`

`DUP`

`PAIR`

`PUSH`

`ADD`

`GET` (at least on map)

`UPDATE` (on map)

`COMPARE` (at least on mutez)

`AMOUNT`

`IF`

`DIP`

`FAILWITH`