WIP: New Michelson language reference

Goal is the replace / improve the existing Michelson language reference with documentation that is generated from the source with static checks enforcing completeness and coherence.

Requirements

1. It should be possible to overview instructions / data types by category (core operations / domain specific operations / ...)
2. The semantics should be presented (semantics and typing) and it should be coherent with formalization in Ott / Coq. However, intuition and example should come before formalism.
3. All instructions and data types should be documented & all documented instructions should be implemented.
4. All examples should be coherent with interpreter & formalization.
5. It would be nice to have an overview of instructions and concrete_data types.

Current state of this branch

It contains a Michelson reference which is generated by a fragment of the Ott formalization as developed in the mi-cho-coq project.

An example of the generated documentation is available here.

More specifically:

1. The Ott file is transformed to a json language definition by a patched version of Ott (based on Basil's Ott)
2. For each Michelson primitive in the language definition, the following is added from the auxiliary michelson-meta.yaml file. Its format is described in docs/doc_gen/michelson_reference/README.org.
3. Using this language definition and meta data, a reference document is generated (in HTML) that contains:
   1. An overview of the primitives in alphabetical order.
   2. An overview of the primitives by category.
   3. For each primitive: its short and long description, stack effect, semantics, typing and the example.

Examples

Examples shoud be taken from the unit tests in src/bin_client/tests/contracts/. Eventually, the tezos unit tests should verify that the example is coherent with the specified input, initial_storage and final_storage as detailed docs/doc_gen/michelson_reference/README.org.

Try michelson integration

For each example, a link is added that when clicked loads the example in the try-michelson IDE. However, this feature relies on running a patched version of try-michelson (forthcoming merge request) locally.

Todo

1. Make it exhaustive by filling in the documentation for each primitive
   1. Also requires making Ott formalization exhaustive
2. Improve stack effects (by including the conclusion of all rules?)
3. Move examples to tests as described above

Proposed work distribution

Basically, for each primitive:

1. Fill out the format as described above, using "LOOP_LEFT" as example for each of the following primitives, using the existing michelson documentation when available
2. Use examples from src/bin_client/tests/contracts/ when available

• Arvid: PACK, UNPACK, BLAKE2B, SHA256, SHA512, ABS, ADD, AMOUNT, AND, BALANCE, CAR, CDR, CHECK_SIGNATURE, CONCAT, CONS, DIP,
• Bruno:
  • CREATE_ACCOUNT
  • CREATE_CONTRACT
  • IMPLICIT_ACCOUNT
  • DROP
  • DUP
  • EDIV
  • EQ
  • EXEC
  • FAILWITH
  • GE
  • GET
  • GT
  • HASH_KEY
  • LT
  • LE
  • COMPARE
• Charles:
  • IF
  • IF_CONS
  • IF_LEFT
  • IF_NONE
  • INT
  • LAMBDA
  • LEFT
  • LOOP
  • LSL
  • LSR
  • MAP
  • MEM
  • MUL
  • NEG
  • EMPTY_MAP
  • EMPTY_SET
• Julien:
  • NEQ
  • NIL
  • NONE
  • NOT
  • NOW
  • OR
  • PAIR
  • PUSH
  • RIGHT
  • SIZE
  • SOME
  • SOURCE
  • SENDER
  • SELF
  • SLICE
  • STEPS_TO_QUOTA
• Raphaël:
  • SUB
  • SWAP
  • TRANSFER_TOKENS
  • SET_DELEGATE
  • UNIT
  • UPDATE
  • XOR
  • ITER
  • LOOP_LEFT
  • ADDRESS
  • CONTRACT
  • ISNAT
  • CAST
  • RENAME
  • CHAIN_ID

Future nice to haves

• Documentation on macros.
• Link between OCaml code and reference so that adding a primitive without documentation to node should break the CI.
• In examples contracts, hovering instruction should display the stack type at that program point
• Reference for data types

How to make the documentation

See docs/README.org under "Michelson reference". After building, the reference will be available at docs/_build/whitedoc/michelson_reference.html.