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
- It should be possible to overview instructions / data types by category (core operations / domain specific operations / ...)
- 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.
- All instructions and data types should be documented & all documented instructions should be implemented.
- All examples should be coherent with interpreter & formalization.
- 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:
- The Ott file is transformed to a json language definition by a patched version of Ott (based on Basil's Ott)
- For each Michelson primitive in the language definition, the
following is added from the auxiliary
michelson-meta.yaml
file. Its format is described indocs/doc_gen/michelson_reference/README.org
. - Using this language definition and meta data, a reference document
is generated (in HTML) that contains:
- An overview of the primitives in alphabetical order.
- An overview of the primitives by category.
- 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
-
Make it exhaustive by filling in the documentation for each primitive -
Also requires making Ott formalization exhaustive
-
-
Improve stack effects (by including the conclusion of all rules?) -
Move examples to tests as described above
Proposed work distribution
Basically, for each primitive:
- 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
- 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
.