From 7044576b3ff2f84c8ce00da2f5ea0a2f521dfb14 Mon Sep 17 00:00:00 2001 From: Benjamin Canou Date: Fri, 9 Sep 2016 18:17:31 +0200 Subject: [PATCH] Docs: add language documentation. --- src/proto/bootstrap/docs/json-notations.md | 265 +++ src/proto/bootstrap/docs/language.md | 1900 ++++++++++++++++++++ 2 files changed, 2165 insertions(+) create mode 100644 src/proto/bootstrap/docs/json-notations.md create mode 100644 src/proto/bootstrap/docs/language.md diff --git a/src/proto/bootstrap/docs/json-notations.md b/src/proto/bootstrap/docs/json-notations.md new file mode 100644 index 000000000..334c60d04 --- /dev/null +++ b/src/proto/bootstrap/docs/json-notations.md @@ -0,0 +1,265 @@ +JSON Notations in the Tezos System +================================== + +I - Constants +------------- + +II - Programs, Data and Types +---------------------------- + +When a new scripted contract is opened in the system, its code must be +given, along with the initial value of its global storage, and the +types of both. For the contract origination RPC, a script is a JSON +object with two fields, as follows. The same format is used when +introspecting the node, returning the current state of the storage. + + { "code": + { "code": [ /* instruction */, ... ], + "argType": /* type */, + "retType": /* type */, + "storageType": /* type */ }, + "storage": + { "storage": /* tagged data */, + "storageType": /* type */ } } + +All the sub fields contain expressions in a common meta JSON format +described in the next section. These expressions map to the syntactic +structure of the (whitespace sensitive) concrete syntax described in +the language specification document. + +### Generic Representation of Expressions + +The language has three basic syntactical constructs (notwithstanding +the small shortcuts and variations allowed by the concrete +syntax). An expression can be a constant, a sequence, or the +application of a primitive. + + * A Constant is encoded as one of these three cases. + + * `{ "float": "f" }` + where `"f"` is the textual representation + of a floating point number in the concrete source language. + * `{ "int": "n" }` + where `"n"` is the textual representation + of a floating point number in the concrete source language. + * `{ "string": f }` + where `s` is a JSON string. + + Constants for timestamps, signatures, keys, tez amounts and + contracts are just strings constants that respect the same + specific string formats as in the concrete language. + + * A sequence is a JSON array: + + [ /* expression 1 */, /* expression 2 */, ... ] + + * A primitive application is of the form: + + { "name": [ /* argument 1 */, /* argument 2 */, ...] } + + If a primitive is not applied to any argument, a shortcut is: + + "name" + + The name of the primitive is expected to be in lowercase. + +### Examples + +Originating a contract with a script that does nothing can be done +with the following JSON script description. + + { "code": + { "code": [ "cdr", + { "push": [ "void" ] } + "pair" ], + "argType": "void", + "retType": "void", + "storageType": "void" }, + "storage": + { "storage": "void", + "storageType": "void" } } + +### Full grammar + + /* tagged data */ ::= + | { "int8": [ /* int constant */ ] } + | { "int16": [ /* int constant */ ] } + | { "int32": [ /* int constant */ ] } + | { "int64": [ /* int constant */ ] } + | { "uint8": [ /* int constant */ ] } + | { "uint16": [ /* int constant */ ] } + | { "uint32": [ /* int constant */ ] } + | { "uint64": [ /* int constant */ ] } + | "void" + | "true" + | "false" + | /* string constant */ + | /* float constant */ + | { "timestamp": [ /* timestamp constant */ ] } + | { "signature": [ /* signature constant */ ] } + | { "tez": [ /* tez constant */ ] } + | { "key": [ /* key constant */ ] } + | { "left": [ /* tagged data */, /* type */ ] } + | { "right": [ /* type */, /* tagged data */ ] } + | { "or": [ /* type */, /* type */, /* untagged data */ ] } + | { "ref": [ /* tagged data */ ] } + | { "ref": [ /* type */, /* untagged data */ ] } + | { "some": [ /* tagged data */ ] } + | { "some": [ /* type */, /* untagged data */ ] } + | { "none": [ /* type */ ] } + | { "option": [ /* type */, /* untagged data */ ] } + | { "pair": [ /* tagged data */, /* tagged data */ ] } + | { "pair": [ /* type */, + /* type */, + /* untagged data */, + /* untagged data */ ] } + | { "list": [ /* type */, /* untagged data */ ... ] } + | { "set": [ /* comparable type */, /* untagged data */ ... ] } + | { "map": [ /* comparable type */, + /* type */, + { "item": [ /* untagged data */, /* untagged data */ ] } ... ] } + | { "contract": [ /* type */, /* type */, /* contract constant */ ] } + | { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] } + /* untagged data */ ::= + | /* int constant */ + | /* string constant */ + | /* float constant */ + | /* timestamp constant */ + | /* signature constant */ + | /* key constant */ + | /* tez constant */ + | /* contract constant */ + | "void" + | "true" + | "false" + | { "pair": [ /* untagged data */, /* untagged data */ ] } + | { "left": [ /* untagged data */ ] } + | { "right": [ /* untagged data */ ] } + | { "ref": [ /* untagged data */ ] } + | { "some": [ /* untagged data */ ] } + | "none" + | { "list": [ /* untagged data */ ... ] } + | { "set": [ /* untagged data */ ... ] } + | { "map": [ { "item": [ /* untagged data */, /* untagged data */ ] } ... ] } + /* instruction */ ::= + | [ /* instruction */ ... ] + | "drop" + | "dup" + | "swap" + | { "push": [ /* tagged data */ ] } + | "some" + | { "none": [ /* type */ ] } + | { "if_none": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } + | "pair" + | "car" + | "cdr" + | { "left": [ /* type */ ] } + | { "right": [ /* type */ ] } + | { "if_left": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } + | { "nil": [ /* type */ ] } + | "cons" + | { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } + | { "empty_set": [ /* type */ ] } + | { "empty_map": [ /* comparable type */, /* type */ ] } + | "iter" + | "map" + | "reduce" + | "mem" + | "get" + | "update" + | "ref" + | "deref" + | "set" + | { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } + | { "loop": [ [ /* instruction */ ... ] ] } + | { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] } + | "exec" + | { "dip": [ [ /* instruction */ ... ] ] } + | "fail" + | "nop" + | "concat" + | "add" + | "sub" + | "mul" + | "div" + | "abs" + | "neg" + | "mod" + | "lsl" + | "lsr" + | "or" + | "and" + | "xor" + | "not" + | "compare" + | "eq" + | "neq" + | "lt" + | "gt" + | "le" + | "ge" + | "cast" + | "checked_abs" + | "checked_neg" + | "checked_add" + | "checked_sub" + | "checked_mul" + | "checked_cast" + | "floor" + | "ceil" + | "inf" + | "nan" + | "isnan" + | "nanan" + | "manager" + | "transfer_funds" + | "create_account" + | "create_contract" + | "now" + | "amount" + | "balance" + | "check_signature" + | "h" + | "steps_to_quota" + | { "source": [ /* type */, /* type */ ] } + /* type */ ::= + | "int8" + | "int16" + | "int32" + | "int64" + | "uint8" + | "uint16" + | "uint32" + | "uint64" + | "void" + | "string" + | "float" + | "tez" + | "bool" + | "key" + | "timestamp" + | "signature" + | { "ref": [ /* type */ ] } + | { "option": [ /* type */ ] } + | { "list": [ /* type */ ] } + | { "set": [ /* comparable type */ ] } + | { "contract": [ /* type */, /* type */ ] } + | { "pair": [ /* type */, /* type */ ] } + | { "union": [ /* type */, /* type */ ] } + | { "lambda": [ /* type */, /* type */ ] } + | { "map": [ /* comparable type */, /* type */ ] } + /* comparable type */ ::= + | "int8" + | "int16" + | "int32" + | "int64" + | "uint8" + | "uint16" + | "uint32" + | "uint64" + | "string" + | "float" + | "tez" + | "bool" + | "key" + | "timestamp" diff --git a/src/proto/bootstrap/docs/language.md b/src/proto/bootstrap/docs/language.md new file mode 100644 index 000000000..e4e85946f --- /dev/null +++ b/src/proto/bootstrap/docs/language.md @@ -0,0 +1,1900 @@ +Tezos Contract Script Language Specification +============================================ + +The language is stack based, with high level data types and primitives +and scrict static type checking. Its design is insipired by Forth, +Scheme, ML and Cat. + +This specification gives the complete instruction set, type system and +semantics of the language. It is meant as a precise reference manual, +not an easy introduction. Even though, some examples are provided at +the end of the document and can be read first or at the same time as +the specification. + + +Table of contents +----------------- + + * I - Type system + * II - Semantics + * III - Core instructions + * IV - Data types + * V - Operations + * VI - Domain specific data types + * VII - Domain specific operations + * VIII - Concrete syntax + * IX - Examples + * X - Full grammar + * XI - Reference implementation + +I - Type system +--------------- + +The types `T` of values in the stack are written using notations + + * `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`, + the core primitive types, + * `identifier` for a primitive data-type, + * `T identifier` for a parametric data-type with one parameter type `T`, + * `identifier T_0 ... T_n` for a parametric data-type with several + parameters, + * `'a` for a type variable, + * `_` for an anonymous type variable, + * `[ P ]` for a code quotation whose program type is `P`, + * `lambda T_arg T_ret` is a shortcut for `[ T_arg :: [] -> T_ret :: []]`. + * other specific notations for compound types, described later. + +Instructions, programs and primitives of the language are also typed, +their types `P` are written using the following notation, where `S` +the type of a stack. + + :: S before -> S after + +A stack type `S` can be written + + * `[]` for the empty stack, + * `T_top : S_rest` for the stack whose first value has type `Ttop` and queue `Srest`, + * `'A` for a stack type variable, + * `_` for an anonymous stack type variable. + + +II - Semantics +-------------- + +The instructions are specified as follows, giving their mnemonic, type +in the previously defined syntax, and small step semantics as a list +of rewriting rules of the form + + > pre state => result state + +where the preconditions of all rules are to be read in order, the first +match selecting the behaviour of the instruction, so that the choice +is deterministic. Only the valid pre states are described, any other +cannot happen thanks to static typing. + + +The pre and post result states are described as + + * pairs `code / stack` for stack manipulation primitives, + * triples `code / stack / memory` for primitives that also manipulate memory, + * `[FAIL]` for a fatal failure state. + +The notations used are + + * `;` to represent the concatenation of instructions or sequences, + * `[]` for the empty code sequence, + * `top : tail` for stack consing, as in types, + * `identifier` for variable stack and code elements, + * `` for variable memory locations, + * `_` for elements whose value does not affect the semantics. + +The memory is described as a relation between locations and constants of +the form `variable = constant, ...`. + +The constants are of one of the following forms. + + * integers with their sign and size, e.g. `(Uint8 3)`, + * floats in libc-style notation, e.g. `(Float 4.5e2)`, + * `Void`, the unique value of type `void` + * booleans `True` and `False`, + * string literals, as in `(String "contents")`, + * structured constants of compound types described later. + + +III - Core instructions +----------------------- + +### Control structures + + * `(I :: [ 'A -> 'B ]) ; (C :: [ 'B -> 'C ])`: Sequence operator. + + :: 'A -> 'C + + > I ; C / SA => C / SB iff I / SA => [] / SB + + * `IF bt bf`: Conditional branching. + + :: bool : 'A -> 'B + iff bt :: [ 'A -> 'B ] + bf :: [ 'A -> 'B ] + + > IF ; C / True : S => bt ; C / S + > IF ; C / False : S => bf ; C / S + + * `LOOP body`: A generic loop. + + :: bool : 'A -> 'A + iff body :: [ 'A -> bool : 'A ] + + > LOOP body ; C / True : S => body ; LOOP body ; C / S + > LOOP body ; C / False : S => C / S + + * `DIP code`: Runs code protecting the top of the stack. + + :: 'b : 'A -> 'b : 'C + iff code :: [ 'A -> 'C ] + + > DIP code ; C / x : S => code ; PUSH x ; C / S + + * `DII+P code`: A sugar syntax for working deeper in the stack. + + > DII(\rest)P code ; C / S => DIP (DI(\rest)P code) ; C / S + + * `LAMBDA 'a 'b code`: Push a function onto the stack. + + :: 'C -> lambda 'a 'b : 'C + iff code :: lambda 'a 'b + + > LAMBDA 'a 'b code ; C / S => C / code : S + + * `EXEC`: Execute a function from the stack. + + :: 'a : lambda 'a 'b : 'C -> 'b : 'C + + > EXEC ; C / a : f : S => f ; C / a : S + +### Stack operations + + * `DROP`: Drop the top element of the stack. + + :: _ : 'A -> 'A + + > DROP ; C / _ : S => C / S + + * `DUP`: Duplicate the top of the stack. + + :: 'a : 'A -> 'a : 'a : 'A + + > DUP ; C / x : S => C / x : x : S + + * `DUP n`: Duplicate the `n`th element of the stack. + + > DUP (n > 0) ; C / S => DIP { DUP (n - 1) } ; SWAP ; C / S + > DUP 0 ; C / S => DUP ; C / S + + This variant of `DUP` with an optional argument is syntactic + sugar for combining `DIP`, `SWAP` and `DUP` in order to access + elements in the stack by their depth, `DUP 0` being equivqlent to + a simple `DUP`. + + * `SWAP`: Exchange the top two elements of the stack. + + :: 'a : 'b : 'A -> 'b : 'a : 'A + + > SWAP ; C / x : y : S => C / y : x : S + + * `PUSH x`: Push a value onto the stack. + + + :: 'A -> 'a : 'A + iff x :: 'a + + > PUSH x ; C / S => C / x : S + + * `DROP`: Drop the top element of the stack. + + :: _ : 'A -> 'A + + > DROP ; C / _ : S => C / S + + * `VOID`: Push a void value onto the stack. + + :: 'A -> void : 'A + + > VOID ; C / S => C / () : S + +### Generic comparison + +Comparison only works on a class of types that we call comparable. A +`COMPARE` operation is defined in an ad hoc way for each comparable +type, but the result of compare is always an `int64`, which can in turn +be checked in a generic manner using the following combinators. The +result of `COMPARE` is `0` if the compared values are equal, negative if +the first is less than the second, and positive otherwise. + + * `EQ`: Checks that the top if the stack EQuals zero. + + :: int64 : 'S -> bool : 'S + + > EQ ; C / Int64 (0) : S => C / True : S + > EQ ; C / _ : S => C / False : S + + + * `NEQ`: Checks that the top if the stack does Not EQual zero. + + :: int64 : 'S -> bool : 'S + + > NEQ ; C / Int64 (0) : S => C / False : S + > NEQ ; C / _ : S => C / True : S + + * `LT`: Checks that the top if the stack is Less Than zero. + + :: int64 : 'S -> bool : 'S + + > LT ; C / Int64 (v) : S => C / True : S iff v < 0 + > LT ; C / _ : S => C / False : S + + * `GT`: Checks that the top if the stack is Greater Than zero. + + :: int64 : 'S -> bool : 'S + + > GT ; C / Int64 (v) : S => C / True : S iff v > 0 + > GT ; C / _ : S => C / False : S + + * `LE`: Checks that the top if the stack is Less Than of Equal to zero. + + :: int64 : 'S -> bool : 'S + + > LE ; C / Int64 (v) : S => C / True : S iff v <= 0 + > LE ; C / _ : S => C / False : S + + * `GE`: Checks that the top if the stack is Greater Than of Equal to zero. + + :: int64 : 'S -> bool : 'S + + > GE ; C / Int64 (v) : S => C / True : S iff v >= 0 + > GE ; C / _ : S => C / False : S + +Syntactic sugar exists for merging `COMPARE` and comparison +combinators, and also for branching. + + * `CMP{EQ|NEQ|LT|GT|LE|GE}` + + > CMP(\op) ; C / S => COMPARE ; (\op) ; C / S + + * `IF{EQ|NEQ|LT|GT|LE|GE} bt bf` + + > IFCMP(\op) ; C / S => (\op) ; IF bt bf ; C / S + + * `IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf` + + > IFCMP(\op) ; C / S => COMPARE ; IF(\op) bt bf ; C / S + + +IV - Data types +--------------- + + * `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`: + The core primitive types. + + * `list 'a`: + A single, immutable, homogeneous linked list, whose elements are + of type 'a, and that we note Nil for the empty list or + (Cons head tail). + + * `pair 'a 'b`: + A pair of values a and b of types 'a and 'b, that we write (Pair a b). + + * `option 'a`: + Optional value that we note (None) or (Some v). + + * `or 'a 'b`: + A union of two types, a value holding either a value a of type 'a + or a value b of type 'b, that we write (Left a) or (Right b). + + * `ref 'a`: + Classical imperative stores, that we note (Ref const). + + * `set 'a`, `map 'a 'b`: + Imperative map and sets, optimized in the db. + + +V - Operations +-------------- + +### Operations on booleans + + * `OR` + + :: bool : bool : 'S -> bool : 'S + + > OR ; C / x : y : S => C / (x | y) : S + + * `AND` + + :: bool : bool : 'S -> bool : 'S + + > AND ; C / x : y : S => C / (x & y) : S + + * `XOR` + + :: bool : bool : 'S -> bool : 'S + + > XOR ; C / x : y : S => C / (x ^ y) : S + + * `NOT` + + :: bool : 'S -> bool : 'S + + > NOT ; C / x : S => C / ~x : S + +### Operations on integers + +Integers can be of size 1, 2, 4 or 8 bytes, signed or unsigned. +Integer Operations are homogeneous, so that performing computations +between values of different int types must be done via explicit casts. + +For specifying arithmetics, we consider that integers are all stored +on 64 bits (the largest integer size) so that we can express the +operations, in particular casts, using usual bitwise masks. In this +context, the type indicator functions are defined as follows (which +can be read both as a constraint on the bitpatttern and as a +conversion operation). + + Uint64 (x) = Int64 (x) = x + Uint32 (x) = x & 0x00000000FFFFFFFF + Int32 (x) = x & 0x00000000FFFFFFFF + | (x & 0x80000000 ? 0xFFFFFFFF00000000 : 0) + Uint16 (x) = x & 0x000000000000FFFF + Int16 (x) = x & 0x000000000000FFFF + | (x & 0x8000 ? 0xFFFFFFFFFFFF0000 : 0) + Uint8 (x) = x & 0x00000000000000FF + Int8 (x) = x & 0x00000000000000FF + | (x & 0x80 ? 0xFFFFFFFFFFFFFF00 : 0) + +We also use the function `bits (t)` that retrieve the meaningful number +of bits for a given integer type (e.g. `bits (int8) = 8`). + + * `NEG` + + :: t : 'S -> t : 'S where t in int{8|16|32|64} + + > NEG ; C / t (x) : S => C / t (-x) : S + + With cycling semantics for overflows (min (t) = -min (t)). + + * `ABS` + + :: t : 'S -> t : 'S where t in int{8|16|32|64} + + > ABS ; C / t (x) : S => C / t (abs (x)) : S + + With cycling semantics for overflows (abs (min (t)) = min (t)). + + * `ADD` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > ADD ; C / t (x) : t (y) : S => C / t (x + y) : S + + With cycling semantics for overflows. + + * `SUB` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > SUB ; C / t (x) : t (y) : S => C / t (x + y) : S + + With cycling semantics for overflows. + + * `MUL` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > MUL ; C / t (x) : t (y) : S => C / t (x + y) : S + + Unckeched for overflows. + + * `DIV` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > DIV ; C / t (x) : t (0) : S => C / [FAIL] + > DIV ; C / t (x) : t (y) : S => C / t (x / y) : S + + * `MOD` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > MOD ; C / t (x) : t (0) : S => C / [FAIL] + > MOD ; C / t (x) : t (y) : S => C / t (x % y) : S + + * `CAST t_to` where `t_to in u?int{8|16|32|64}` + + :: t_from : 'S -> t_to : 'S where t_from in u?int{8|16|32|64} + + > CAST t_to ; C / t_from (x) : S => C / t_to (x) : S + +Alternative operators are defined that check for overflows. + + * `CHECKED_NEG` + + :: t : 'S -> t : 'S where t in int{8|16|32|64} + + > CHECKED_NEG ; C / t (x) : S => [FAIL] on overflow + > CHECKED_NEG ; C / t (x) : S => C / t (-x) : S + + * `CHECKED_ABS` + + :: t : 'S -> t : 'S where t in int{8|16|32|64} + + > CHECKED_ABS ; C / t (x) : S => [FAIL] on overflow + > CHECKED_ABS ; C / t (x) : S => C / t (abs (x)) : S + + * `CHECKED_ADD` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > CHECKED_ADD ; C / t (x) : t (y) : S => [FAIL] on overflow + > CHECKED_ADD ; C / t (x) : t (y) : S => C / t (x + y) : S + + * `CHECKED_SUB` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > CHECKED_SUB ; C / t (x) : t (y) : S => [FAIL] on overflow + > CHECKED_SUB ; C / t (x) : t (y) : S => C / t (x - y) : S + + * `CHECKED_MUL` + + :: t : t : 'S -> t : 'S where t in u?int{8|16|32|64} + + > CHECKED_MUL ; C / t (x) : t (y) : S => [FAIL] on overflow + > CHECKED_MUL ; C / t (x) : t (y) : S => C / t (x * y) : S + + * `CHECKED_CAST t_to` where `t_to in u?int{8|16|32|64}` + + :: t_from : 'S -> t_to : 'S where t_from in u?int{8|16|32|64} + + > CHECKED_CAST t_to ; C / t_from (x) : S => C / t_to (x) : S + iff t_from (x) = t_to (x) + > CHECKED_CAST t_to ; C / t_from (x) : S => [FAIL] + +Bitwise logical operators are also available on unsigned integers. + + * `OR` + + :: t : t : 'S -> t : 'S where t in uint{8|16|32|64} + + > OR ; C / t (x) : t (y) : S => C / t (x | y) : S + + * `AND` + + :: t : t : 'S -> t : 'S where t in uint{8|16|32|64} + + > AND ; C / t (x) : t (y) : S => C / t (x & y) : S + + * `XOR` + + :: t : t : 'S -> t : 'S where t in uint{8|16|32|64} + + > XOR ; C / t (x) : t (y) : S => C / t (x ^ y) : S + + * `NOT` + + :: t : 'S -> t : 'S where t in uint{8|16|32|64} + + > NOT ; C / t (x) : S => C / t (~x) : S + + * `LSL` + + :: t : uint8 (s) : 'S -> t : 'S where t in uint{8|16|32|64} + + > LSL ; C / t (x) : uint8 (s) : S => C / t (x << s) : S + iff s <= bits (t) + > LSL ; C / t (x) : uint8 (s) : S => [FAIL] + + * `LSR` + + :: t : uint8 (s) : 'S -> t : 'S where t in uint{8|16|32|64} + + > LSR ; C / t (x) : uint8 (s) : S => C / t (x >>> s) : S + iff s <= bits (t) + > LSR ; C / t (x) : uint8 (s) : S => [FAIL] + + * `COMPARE`: + Integer comparison (signed or unsigned according to the type) + + :: t : t : 'S -> int64 : 'S where t in uint{8|16|32|64} + +### Operations on Floats + +The float type uses double precision IEEE754 semantics, including NaN +and infinite values. + + * `ADD` + + :: float : float : 'S -> float : 'S + + > ADD ; C / x : y : S => C / (x + y) : S + + * `SUB` + + :: float : float : 'S -> float : 'S + + > SUB ; C / x : y : S => C / (x - y) : S + + * `MUL` + + :: float : float : 'S -> float : 'S + + > MUL ; C / x : y : S => C / (x * y) : S + + * `DIV` + + :: float : float : 'S -> float : 'S + + > DIV ; C / x : y : S => C / (x / y) : S + + * `MOD` + + :: float : float : 'S -> float : 'S + + > MOD ; C / x : y : S => C / (fmod (x, y)) : S + + * `ABS` + + :: float : 'S -> float : 'S + + > ABS ; C / x : S => C / (abs (x)) : S + + * `NEG` + + :: float : 'S -> float : 'S + + > NEG ; C / x : S => C / (-x) : S + + * `FLOOR` + + :: float : 'S -> float : 'S + + > FLOOR ; C / x : S => C / (floor (x)) : S + + * `CEIL` + + :: float : 'S -> float : 'S + + > CEIL ; C / x : S => C / (ceil (x)) : S + + * `INF` + + :: 'S -> float : 'S + + > INF ; C / S => C / +Inf : S + + * `NAN` + + :: 'S -> float : 'S + + > NAN ; C / S => C / NaN : S + + * `ISNAN` + + :: float : 'S -> bool : 'S + + > ISNAN ; C / NaN : S => C / true : S + > ISNAN ; C / _ : S => C / false : S + + * `NANAN` + + :: float : 'S -> 'S + + > NANAN ; C / NaN : S => [FAIL] + > NANAN ; C / _ : S => C / S + + * `CAST float`: + Conversion from integers. + + :: t_from : 'S -> float : 'S where t_from in u?int{8|16|32|64} + + > CAST float ; C / x : S => C / float (x) : S + + * `CAST t_to` where `t_to in u?int{8|16|32|64}`: + Conversion to integers. + + :: float : 'S -> t_to : 'S + + > CAST t_to ; C / NaN : S => C / t_to (0) : S + > CAST t_to ; C / +/-Inf : S => C / t_to (0) : S + > CAST t_to ; C / x : S => C / t_to (floor (x)) : S + + * `CHECKED_CAST float`: + Conversion from integers with overflow checking. + + :: t_from : 'S -> float : 'S where t_from in u?int{8|16|32|64} + + > CHECKED_CAST float ; C / x : S => [FAIL] on overflow + > CHECKED_CAST float ; C / x : S => C / float (x) : S + + * `CHECKED_CAST t_to` where `t_to in u?int{8|16|32|64}`: + Conversion to integers with overflow checking. + + :: float : 'S -> t_to : 'S + + > CHECKED_CAST t_to ; C / x : S => [FAIL] on overflow or NaN + > CHECKED_CAST t_to ; C / x : S => C / t_to (floor (x)) : S + + + * `COMPARE`: + IEEE754 comparison + + :: float : float : 'S -> int64 : 'S + +### Operations on strings + +Strings are mostly used for naming things without having to rely on +external ID databases. So what can be done is basically use string +constants as is, concatenate them and use them as keys. + + * `CONCAT`: + String concatenation. + + :: string : string : 'S -> string : 'S + + * `COMPARE`: + Lexicographic comparison. + + :: string : string : 'S -> int64 : 'S + +### Operations on pairs + + * `PAIR`: + Build a pair from the stack's top two elements. + + :: 'a : 'b : 'S -> pair 'a 'b : 'S + + > PAIR ; C / a : b : S => C / (Pair a b) : S + + * `P(A*AI)+R`: + A syntactic sugar for building nested pairs in bulk. + + > PA{N}AI(\rest)R ; C / S => DIP (PA{n-1}AIR) ; P(\rest)R ; C / S + > PAIR ; C / S => PAIR ; C / S + > PR ; C / S => C / S + + * `CAR`: + Access the left part of a pair. + + :: pair 'a _ : 'S -> 'a : 'S + + > Car ; C / (Pair a _) : S => C / a : S + + * `CDR`: + Access the left part of a pair. + + :: pair _ 'b : 'S -> 'b : 'S + + > Car ; C / (Pair _ b) : S => C / b : S + + * `C[AD]+R`: + A sugary syntax for accessing fields in nested pairs. + + > CA(\rest)R ; C / S => CAR ; C(\rest)R ; C / S + > CD(\rest)R ; C / S => CDR ; C(\rest)R ; C / S + > CR ; C / S => C / S + +### Operations on refs + + * `REF`: + Build a ref from its initial contents. + + :: 'a : 'S -> ref 'a : 'S + + > REF ; C / a : S / M => C / l : S / l = (Ref a), M + + * `DEREF`: + Access the contents of a ref. + + :: ref 'a : 'S -> 'a : 'S + + > DEREF ; C / l : S / l = (Ref a), M => C / a : S / l = (Ref a), M + + * `SET` + Update the contents of a ref. + + :: 'a : ref 'a : 'S -> 'S + + > SET ; C / v :: l : S / l = (Ref _), M => C / S / l = (Ref v), M + + * `INCR step`: + Increments a counter. + + :: ref 'a : 'S -> 'S + iff step :: 'a, operator ADD defined on 'a + + > INCR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; ADD ; Set ; C / S / M + + * `DECR step`: + Decrements a counter. + + :: ref 'a : 'S -> 'S + iff step :: 'a, operator SUB defined on 'a + + > DECR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; SUB ; Set ; C / S / M + +### Operations on sets + + * `EMPTY_SET 'elt`: + Build a new, empty imperative set for elements of a given type. + + :: 'S -> set 'elt : 'S + + The `'elt` type must be comparable (the `COMPARE` primitive must + be defined over it). + + * `MEM`: + Check for the presence of an element in a set. + + :: 'key : set 'elt : 'S -> bool : 'S + + * `UPDATE`: + Inserts or removes an element in a set, replacing a previous value. + + :: 'elt : bool : set 'elt : 'S -> 'S + + * `ITER`: + Apply an imperative function over all the elements of a set. + + :: lambda 'elt void : set 'elt : 'S -> 'S + + * `REDUCE`: + Apply a function on a set passing the result of each + application to the next one and return the last. + + :: lambda (pair 'elt * 'b) 'b : set 'elt : 'b : 'S -> 'b : 'S + +### Operations on maps + + * `EMPTY_MAP 'key 'val`: + Build a new, empty imperative map. + + The `'key` type must be comparable (the `COMPARE` primitive must be + defined over it). + + :: 'S -> map 'key 'val : 'S + + * `GET`: + Access an element in a map, returns an optional value to be + checked with `IF_SOME`. + + :: 'key : map 'key 'val : 'S -> option 'val : 'S + + * `MEM`: + Check for the presence of an element in a map. + + :: 'key : map 'key 'val : 'S -> bool : 'S + + * `UPDATE`: + Assign or remove an element in a map. + + :: 'key : option 'val : map 'key 'val : 'S -> 'S + + * `ITER`: + Apply an imperative function over all the bindings of a map. + + :: lambda (pair 'key 'val) void : map 'key 'val : 'S -> 'S + + * `MAP`: + Apply a function on a map and return the map of results under + the same bindings. + + :: lambda (pair 'key 'val) 'b : map 'key 'val : 'S -> map 'key 'b : 'S + + * `REDUCE`: + Apply a function on a map passing the result of each + application to the next one and return the last. + + :: lambda (pair (pair 'key 'val) 'b) 'b : map 'key 'val : 'b : 'S -> 'b : 'S + +### Operations on optional values + + * `SOME`: + Pack a present optional value. + + :: 'a : 'S -> 'a? : 'S + + > SOME ; C / v :: S => C / (Some v) :: S + + * `NONE 'a`: + The absent optional value. + + :: 'S -> 'a? : 'S + + > NONE ; C / v :: S => C / None :: S + + * `IF_SOME bt bf`: + Inspect an optional value. + + :: 'a? : 'S -> 'b : 'S + iff bt :: [ 'a : 'S -> 'b : 'S] + bf :: [ 'S -> 'b : 'S] + + > IF_SOME ; C / (Some a) : S => bt ; C / a : S + > IF_SOME ; C / (None) : S => bf ; C / S + +### Operations on unions + + * `LEFT 'b`: + Pack a value in a union (left case). + + :: 'a : 'S -> or 'a 'b : 'S + + > LEFT ; C / v :: S => C / (Left v) :: S + + * `RIGHT 'a`: + Pack a value in a union (right case). + + :: 'b : 'S -> or 'a 'b : 'S + + > RIGHT ; C / v :: S => C / (Right v) :: S + + * `IF_LEFT bt bf`: + Inspect an optional value. + + :: or 'a 'b : 'S -> 'c : 'S + iff bt :: [ 'a : 'S -> 'c : 'S] + bf :: [ 'b : 'S -> 'c : 'S] + + > IF_LEFT ; C / (Left a) : S => bt ; C / a : S + > IF_LEFT ; C / (Right b) : S => bf ; C / b : S + +### Operations on lists + + * `CONS`: + Prepend an element to a list. + + :: 'a : list 'a : 'S -> list 'a : 'S + + > CONS ; C / a : l : S => C / (Cons a l) : S + + * `NIL 'a`: + The empty list. + + :: 'S -> list 'a : 'S + + > NIL ; C / S => C / Nil : S + + * `IF_CONS bt bf`: + Inspect an optional value. + + :: list 'a : 'S -> 'b : 'S + iff bt :: [ 'a : list 'a : 'S -> 'b : 'S] + bf :: [ 'S -> 'b : 'S] + + > IF_CONS ; C / (Cons a rest) : S => bt ; C / a : rest : S + > IF_CONS ; C / Nil : S => bf ; C / S + + * `ITER`: + Apply a function on a list from left to right. + + :: lambda 'a void : list 'a : 'S -> 'S + + * `MAP`: + Apply a function on a list from left to right and + return the list of results in the same order. + + :: lambda 'a 'b : list 'a : 'S -> list 'b : 'S + + * `REDUCE`: + Apply a function on a list from left to right + passing the result of each application to the next one + and return the last. + + :: lambda (pair 'a 'b) 'b : list 'a : 'b : 'S -> 'b : 'S + + +VI - Domain specific data types +------------------------------- + + * `timestamp`: + Dates in the real world. + + * `tez`: + A specific type for manipulating tokens. + + * `contract 'param 'result`: + A contract, with the type of its code. + + * `key`: + A public cryptography key. + + * `signature`: + A cryptographic signature. + + +VII - Domain specific operations +-------------------------------- + +### Operations on timestamps + +Timestamp immediates can be obtained by the `NOW` operation, or +retrieved from script parameters or globals. The only valid operations +are the addition of a (positive) number of seconds and the comparison. + + * `ADD` + Increment / decrement a timestamp of the given number of seconds. + + :: timestamp : float : 'S -> timestamp : 'S + + > ADD ; C / t : period : S => [FAIL] iff period < 0 + > ADD ; C / t : period : S => C / (t + period seconds) : S + + * `ADD` + Increment / decrement a timestamp of the given number of seconds. + + :: timestamp : uint{8|16|32|64} : 'S -> timestamp : 'S + + > ADD ; C / t : seconds : S => [FAIL] on overflow + > ADD ; C / t : seconds : S => C / (t + seconds) : S + + * `COMPARE`: + Timestamp comparison. + + :: timestamp : timestamp : 'S -> int64 : 'S + +### Operations on Tez + +Operations on tez are limited to prevent overflow and mixing them with +other numerical types by mistake. They are also mandatorily checked +for under/overflows. + + * `ADD`: + + :: tez : tez : 'S -> tez : 'S + + > Add ; C / x : y : S => [FAIL] on overflow + > Add ; C / x : y : S => C / (x + y) : S + + * `SUB`: + + :: tez : tez : 'S -> tez : 'S + + > Sub ; C / x : y : S => [FAIL] iff x < y + > Sub ; C / x : y : S => C / (x - y) : S + + * `MUL` + + :: tez : u?int{8|16|32|64} : 'S -> tez : 'S + + > Mul ; C / x : y : S => [FAIL] on overflow + > Mul ; C / x : y : S => C / (x * y) : S + + * `COMPARE`: + + :: tez : tez : 'S -> int64 : 'S + +### Operations on contracts + + * `MANAGER`: + Access the manager of a contract. + + :: contract 'p 'r : 'S -> key : 'S + + * `CREATE_CONTRACT`: + Forge a new contract. + + + :: key : key? : bool : bool : tez : lambda (pair (pair tez 'p) 'g) (pair 'r 'g) : 'g : 'S + -> contract 'p 'r : 'S + + As with non code-emitted originations the + contract code takes as argument the transfered amount plus an + ad-hoc argument and returns an ad-hoc value. The code also takes + the global data and returns it to be stored and retrieved on the + next transaction. These data are initialized by another + parameter. The calling convention for the code is as follows: + (Pair (Pair amount arg) globals)) -> (Pair ret globals), as + extrapolable from the instruction type. The first parameters are + the manager, optional delegate, then spendable and delegatable + flags and finally the initial amount taken from the currently + executed contract. The contract is returned as a first class + value to be called immediately or stored. + + * `CREATE_ACCOUNT`: + Forge an account (a contract without code). + + :: key : key? : bool : tez : 'S -> contract void void : 'S + + Take as argument the manager, optional delegate, the delegatable + flag and finally the initial amount taken from the currently + executed contract. + + * `TRANSFER_TOKENS`: + Forge and evaluate a transaction. + + :: 'p : tez : contract 'p 'r : 'g : [] -> 'r : 'g : [] + + The parameter and return value must be consistent with the ones + expected by the contract, void for an account. To preserve the + global consistency of the system, the current contract's storage + must be updated before passing the control to another script. For + this, the script must put the partially updated storage on the + stack ('g is the type of the contract's storage). If a recursive + call to the current contract happened, the updated storage is put + on the stack next to the return value. Nothing else can remain + on the stack during a nested call. If some local values have to + be kept for after the nested call, they have to be stored + explicitly in a transient part of the storage. A trivial example + of that is to reserve a boolean in the storage, initialized to + false, reset to false at the end of each contract execution, and + set to true during a nested call. This thus gives an easy way + for a contract to prevent recursive call (the contract just fails + if the boolean is true). + + * `BALANCE`: + Push the current amount of tez of the current contract. + + :: 'S -> tez :: 'S + + * `SOURCE 'p 'r`: + Push the source contract of the current transaction. + + :: 'S -> contract 'p 'r :: 'S + + * `SELF`: + Push the current contract. + + :: 'S -> contract 'p 'r :: 'S + where contract 'p 'r is the type of the current contract + + * `AMOUNT`: + Push the amount of the current transaction. + + :: 'S -> tez :: 'S + +### Special operations + + * `STEPS_TO_QUOTA`: + Push the remaining steps before the contract execution must terminate. + + :: 'S -> uint32 :: 'S + + * `NOW`: + Push the timestamp of the block whose validation triggered this + execution (does not change during the execution of the contract). + + :: 'S -> timestamp :: 'S + + * `FAIL`: + Explicitly abort the current transaction (and all of its parents). + + :: _ -> _ + + > FAIL ; _ / _ => [FAIL] + +### Cryptographic primitives + + * `H`: + Compute a cryptographic hash of the value contents using the + Sha256 cryptographic algorithm. + + :: 'a : 'S -> string : 'S + + * `CHECK_SIGNATURE` + Check that a sequence of bytes has been signed with a given key. + + :: key : pair signature string : 'S -> bool : 'S + + * `COMPARE` + + :: key : key : 'S -> int64 : 'S + + +VIII - Concrete syntax +---------------------- + +The structure of the concrete language is extremely simple. An +expression in the language can only be one of the three following +constructs. + + 1. A constant. + 2. The application of a primitive to a sequence of expressions. + 3. A sequence of expressions. + +As in Python or Haskell, the concrete syntax of the language is +indentation sensitive. The elements of a syntactical block, such as +all the elements of a sequence, or all the parameters of a primitive, +must be written with the exact same left margin in the program source +code. This is unlike in C-like languages, where blocks are delimited +with braces and the margin is ignored by the compiled. The exact +parsing policy is described just after. + +### Constants + +There are three kinds of constants: + + 1. Integers in decimal (no prefix), hexadecimal (0x prefix), octal + (0o prefix) or binary (0b prefix). + 2. Floating point IEEE754 doubles in libc-style notation, with a + mandatory period character. (`3` is an `int` but `3.` is a + `float`). + 3. Strings with usual escapes `\n`, `\t`, `\b`, `\r`, `\\`, `\"`. + Strings are encoding agnostic sequences of bytes. Non printable + characters can be escaped by 3 digits decimal codes `\ddd` or + 2 digit hexadecimal codes `\xHH`. + +All domain specific constants are strings: + + - `tez` amounts are written using the same notation as JSON schemas + and the command line client: thousands are optionally separated by + comas, and centiles, if present, must be prefixed by a period. + - in regexp form: `([0-9]{1,3}(,[0-9]{3})+)|[0-9]+(\.[0.9]{2})?` + - `"1234567"` means 123456700 tez centiles + - `"1,234,567"` means 123456700 tez centiles + - `"1234567.89"` means 123456789 tez centiles + - `"1,234,567.00"` means 123456789 tez centiles + - `"1234,567"` is invalid + - `"1,234,567."` is invalid + - `"1,234,567.0"` is invalid + - `timestamp`s are written using `RFC 339` notation. + - `contract`s are the raw strings returned by JSON RPCs or the command + line interface and cannot be forged by hand so their format is of + no interest here. + - `key`s are `Sha256` hashes of `ed25519` public keys encoded in + `base48` format with the following custom alphabet: + `"eXMNE9qvHPQDdcFx5J86rT7VRm2atAypGhgLfbS3CKjnksB4"`. + - `signature`s are `ed25519` signatures as a series of hex-encoded bytes. + +### Primitive applications + +The simplest form requires to break the line after the primitive name +and after every argument. Argument must be indented by at least one +more space than the primitive, and all arguments must sit on the exact +same column. + + PRIM + arg1 + arg2 + ... + +If an argument of a primitive application is a primitive application +itself, its arguments must be pushed even further on the right, to +lift any ambiguity, as in the following example. + + PRIM1 + PRIM2 + arg1_prim2 + arg2_prim2 + arg2_prim1 + +It is possible to put successive arguments on a single line using +a semicolon as a separator: + + PRIM + arg1; arg2 + arg3; arg4 + +It is also possible to add arguments on the same line as the primitive +as a lighter way to write simple expressions. An other representation +of the first example is: + + PRIM arg1 arg2 ... + +It is possible to mix both notations as in: + + PRIM arg1 arg2 + arg3 + arg4 + +Or even: + + PRIM arg1 arg2 + arg3; arg4 + +Both equivalent to: + + PRIM + arg1 + arg2 + arg3 + arg4 + +Trayling semicolons are ignored: + + PRIM + arg1; + arg2 + +Calling a primitive with a compound argument on a single line is +allowed by wrapping with parentheses. Another notation for the second +example is: + + PRIM1 (PRIM2 arg1_prim2 arg2_prim2) arg2_prim1 + +### Sequences + +Successive instructions can be grouped as a single one by grouping +them inside braces, separated by semicolons. To prevent errors, +control flow primitives that take instructions as parameters require +sequences in the concrete syntax. + + IF { instr1_true ; instr2_true ; ... } { instr1_false ; instr2_false ; ... } + + IF + { instr1_true ; instr2_true ; ... } + { instr1_false ; instr2_false ; ... } + +A sequence block can be split on several lines. In this situation, the +whole block, including the closing brace, must be indented with +respect to the first instruction. + + LAMBDA t_arg t_ret + { instr1 ; instr2 + instr3 ; instr4 } + +### Lexical conventions + +Instructions are represented by uppercase identifiers, type +constructor are lowercase identifiers and constant constructors are +Capitalised. + + * Types, in lowercase, in prefixed notation as in this specification: + + string + + pair string (pair int8 tez) + + lambda int8 int16 + + Of course, types can be split over multiple lines using the + common indented notation. + + map + string + uint32 + + * Constants are built using constructors (starting with a capital) + followed by the actual value. + + Int8 1 + + Float 3.5e12 + + Compound constants such as lists, in order not to repeat the same + constant constructor for each element, take the type(s) of inner + values as first argument(s), and then the values without their + constructors. + + List int8 1 2 3 4 5 + + Pair int8 int16 1 2 + + For constructors whose type cannot be completely deduced fron a + single value, the free type variables must be specified. For this, + some constant constructors take extra types arguments as follows. + + List int8 + + None tez + + Left (Int8 3) int16 + + Right int16 (Int8 3) + + When the type is already completely specified, by a parent + constructor or as in the instruction PUSH, these annotations must + be omitted. + + Pair int8 (list int16) 1 (List 2 3) + + Pair (option (pair void int8)) void + None + Void + + Pair (or int8 string) (or int8 string) + Left 3 + Right "text" + + * Instructions, in uppercase: + + ADD + +### Comments + +A hash sign (`#`) anywhere outside of a string literal will make the +rest of the line (and itself) completely ignored, as in the following +example. + + PUSH (Int8 1) # pushes 1 + PUSH (Int8 2) # pushes 2 + ADD # computes 2 + 1 + +IX - Examples +------------- + +Contracts in the system are stored as a piece of code and a global +data storage. The type of the global data of the storage is fixed for +each contract at origination time. This is ensured statically by +checking on origination that the code preserves the type of the global +data. For this, the code of the contract is checked to be of the +following type lambda (pair (pair tez 'arg) 'global) -> (pair 'ret +'global) where 'global is the type of the original global store given +on origination. The contract also takes a parameter and an amount, and +returns a value, hence the complete calling convention above. The +global values can be updated either by rewriting the object, or by +putting mutable values in it and performing side effects on them, +allowing both imperative and functional style. + +### Empty contract + +Because of the calling convention, the empty sequence is not a valid +contract of type `(contract void void)`. The code for building a +contract of such a type must take a `void` argument, an amount in `tez`, +and transform a void global storage, and must thus be of type `(lambda +(pair (pair tez void) void) (pair void void))`. + +Such a minimal contract is thus `{ CDR ; VOID ; PAIR }`. + +### Reservoir contract + +We want to create a contract that stores tez until a timestamp `T` or a +maximum amount `N` is reached. Whenever `N` is reached before `T`, all tokens +are reversed to an account `B` (and the contract is automatically +deleted). Any call to the contract's code performed after `T` will +otherwise transfer the tokens to another account `A`. + +We want to build this contract in a reusable manner, so we do not +hard-code the parameters. Instead, we assume that the global data of +the contract are `(Pair (Pair T N) (Pair A B))`. + +Hence, the global data of the contract has the following type + + 'g = + pair + pair timestamp tez + pair (contract void void) (contract void void) + +Following the contract calling convention, the code is a lambda of type + + lambda + pair (pair tez void) 'g + pair void 'g + +writen as + + lambda + pair (pair tez void) + pair + pair timestamp tez + pair (contract void void) (contract void void) + pair void + pair + pair timestamp tez + pair (contract void void) (contract void void) + +its code is + + DUP ; CDAAR # T + NOW + COMPARE ; LE + IF { DUP ; CDADR # N + BALANCE + COMPARE ; LE + IF { } # nothing to do + { DUP ; CDDDR # B + BALANCE ; PUSH Void ; TRANSFER_TOKENS ; DROP } } + { DUP ; CDDAR ; # A + BALANCE ; + PUSH Void ; TRANSFER_TOKENS ; DROP } + CDR ; PUSH Void ; PAIR + +### Reservoir contract (variant with broker and status) + +We basically want the same contract as the previous one, but instead +of destroying it, we want to keep it alive, storing a flag `S` so that +we can afterwards if the tokens have been transfered to `A` or `B`. We also +want the broker `A` to get some fee `P` in any case. + +We thus add variables `P` and `S` to the global data of the contract, +which becomes `(Pair (S, Pair (T, Pair (Pair P N) (Pair A B))))`. `P` +is the fee for broker `A`, `S` is the state, as a string `"open"`, +`"timeout"` or `"success"`. + +At the beginning of the transaction: + + S is accessible via a CDAR + T via a CDDAR + P via a CDDDAAR + N via a CDDDADR + A via a CDDDDAR + B via a CDDDDDR + +For the contract to stay alive, we test that all least `(Tez "1.00")` is +still available after each transaction. This value is given as an +example and must be updated according to the actual Tezos minmal +value for contract balance. + + DUP ; CDAR # S + PUSH (String "open") ; + COMPARE ; NEQ ; + IF { FAIL ; CDR } # on "success", "timeout" or a bad init value + { DUP ; CDDAR ; # T + NOW ; + COMPARE ; LT ; + IF { # Before timeout + # We compute ((1 + P) + N) tez for keeping the contract alive + PUSH (Tez "1.00") ; + DIP { DUP ; CDDDAAR } ; ADD ; # P + DIP { DUP ; CDDDADR } ; ADD ; # N + # We compare to the cumulated amount + BALANCE ; + COMPARE; LT ; + IF { # Not enough cash, we accept the transaction + # and leave the global + CDR } + { # We transfer the fee to the broker + DUP ; CDDDAAR ; # P + DIP { DUP ; CDDDDAR } # A + PUSH Void ; TRANSFER_TOKENS ; DROP ; + # We transfer the rest to the destination + DUP ; CDDDADR ; # N + DIP { DUP ; CDDDDDR } # B + PUSH Void ; TRANSFER_TOKENS ; DROP ; + # We update the global + CDR ; CDR ; PUSH (String "success") ; PAIR } } + { # After timeout + # We try to transfer P tez to A + PUSH (Tez "1.00") ; BALANCE ; SUB ; # available + DIP { DUP ; CDDDAAR } ;# P + COMPARE ; LT ; # available < P + IF { PUSH (Tez "1.00") ; BALANCE ; SUB ; # available + DIP { DUP ; CDDDDAR } # A + PUSH Void ; TRANSFER_TOKENS ; DROP } + { DUP ; CDDDAAR ; # P + DIP { DUP ; CDDDDAR } # A + PUSH Void ; TRANSFER_TOKENS ; DROP } + # We transfer the rest to B + PUSH (Tez "1.00") ; BALANCE ; SUB ; # available + DIP { DUP ; CDDDDDR } # B + PUSH Void ; TRANSFER_TOKENS ; DROP ; + # We update the global + CDR ; CDR ; PUSH (String "timeout") ; PAIR } } + # return Void + PUSH Void ; PAIR + +### Forward contract + +We want to write a forward contract on dried peas. The contract takes +as global data the tons of peas `Q`, the expected delivery date `T`, the +contract agreement date `Z`, a strike `K`, a collateral `C` per ton of dried +peas, and the accounts of the buyer `B`, the seller `S` and the warehouse +`W`. + +These parameters as grouped in the global storage as follows: + + Pair + (pair uint32 (pair timestamp timestamp)) + pair + pair tez tez + pair (pair account account) account + Pair (Pair Q (Pair T Z)) + Pair (Pair K C) (Pair (Pair B S) W) + +The 24 hours after timestamp `Z` are for the buyer and seller to store +their collateral `(Q * C)`. For this, the contract takes a string as +parameter, matching `"buyer"` or `"seller"` indicating the party for which +the tokens are transfered. At the end of this day, each of them can +send a transaction to send its tokens back. For this, we need to store +who already paid and how much, as a `(pair tez tez)` where the left +component is the buyer and the right one the seller. + +After the first day, nothing cam happen until `T`. + +During the 24 hours after `T`, the buyer must pay `(Q * K)` to the +contract, minus the amount already sent. + +After this day, if the buyer didn't pay enough then any transaction +will send all the tokens to the seller. + +Otherwise, the seller must deliver at least `Q` tons of dried peas to +the warehouse, in the next 24 hours. When the amount is equal to or +exceeds `Q`, all the tokens are transfered to the seller and the contract +is destroyed. For storing the quantity of peas already delivered, we +add a counter of type `uint32` in the global storage. For knowing this +quantity, we accept messages from W with a partial amount of delivered +peas as argument. + +After this day, any transaction will send all the tokens to the buyer +(not enough peas have been delivered in time). + +Hence, the global storage is a pair, with the counters on the left, +and the constant parameters on the right, initially as follows. + + Pair + pair unit32 (pair tez tez) + pair + pair uint32 (pair timestamp timestamp) + pair + pair tez tez + pair (pair account account) account + Pair 0 (Pair 0_00 0_00) + Pair + Pair (Pair Q (Pair T Z)) + Pair (Pair K C) (Pair (Pair B S) W) + +The parameter of the transaction will be either a transfer from the +buyer or the seller or a delivery notification from the warehouse of +type `(or string uint32)`. + +At the beginning of the transaction: + + Q is accessible via a CDDAAR + T via a CDDADAR + Z via a CDDADDR + K via a CDDDAAR + C via a CDDDADR + B via a CDDDDAAR + S via a CDDDDADR + W via a CDDDDDR + the delivery counter via a CDAAR + the amount versed by the buyer via a CDADAR + the amount versed by the seller via a CDADDR + the argument via a CADR + +The contract returns a void value, and we assume that it is created +with the minimum amount, set to `(Tez "1.00")`. + +The code of the contract is thus as follows. + + DUP ; CDDADDR ; # Z + PUSH (Uint64 86400) ; SWAP ; ADD ; # one day in second + NOW ; COMPARE ; LT ; + IF { # Before Z + 24 + DUP ; CADR ; # we must receive (Left "buyer") or (Left "seller") + IF_LEFT + { DUP ; PUSH (String "buyer") ; COMPARE ; EQ ; + IF { DROP ; + DUP ; CDADAR ; # amount already versed by the buyer + DIP { DUP ; CAAR } ; ADD ; # transaction + # then we rebuild the globals + DIP { DUP ; CDADDR } ; PAIR ; # seller amount + PUSH (Uint32 0) ; PAIR ; # delivery counter at 0 + DIP { CDDR } ; PAIR ; # parameters + # and return Void + PUSH Void ; PAIR } + { PUSH (String "seller") ; COMPARE ; EQ ; + IF { DUP ; CDADDR ; # amount already versed by the seller + DIP { DUP ; CAAR } ; ADD ; # transaction + # then we rebuild the globals + DIP { DUP ; CDADAR } ; SWAP ; PAIR ; # buyer amount + PUSH (Uint32 0) ; PAIR ; # delivery counter at 0 + DIP { CDDR } ; PAIR ; # parameters + # and return Void + PUSH Void ; PAIR } + { FAIL ; CDR ; PUSH Void ; PAIR }}} # (Left _) + { FAIL ; DROP ; CDR ; PUSH Void ; PAIR }} # (Right _) + { # After Z + 24 + # test if the required amount is reached + DUP ; CDDAAR ; # Q + DIP { DUP ; CDDDADR } ; MUL ; # C + PUSH (Uint8 2) ; MUL ; + PUSH (Tez "1.00") ; ADD ; + BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C) + 1 + IF { # refund the parties + DUP ; CDADAR ; # amount versed by the buyer + DIP { DUP ; CDDDDAAR } # B + PUSH Void ; TRANSFER_TOKENS ; DROP + DUP ; CDADDR ; # amount versed by the seller + DIP { DUP ; CDDDDADR } # S + PUSH Void ; TRANSFER_TOKENS ; DROP + BALANCE ; # bonus to the warehouse to destroy the account + DIP { DUP ; CDDDDDR } # W + PUSH Void ; TRANSFER_TOKENS ; DROP + # return void, don't change the global + # since the contract will be destroyed + CDR ; PUSH Void ; PAIR } + { # otherwise continue + DUP ; CDDADAR # T + NOW ; COMPARE ; LT + IF { FAIL ; CDR ; PUSH Void ; PAIR } # Between Z + 24 and T + { # after T + DUP ; CDDADAR # T + PUSH (Uint64 86400) ; ADD # one day in second + NOW ; COMPARE ; LT + IF { # Between T and T + 24 + # we only accept transactions from the buyer + DUP ; CADR ; # we must receive (Left "buyer") + IF_LEFT + { PUSH (String "buyer") ; COMPARE ; EQ ; + IF { DUP ; CDADAR ; # amount already versed by the buyer + DIP { DUP ; CAAR } ; ADD ; # transaction + # The amount must not exceed Q * K + DUP ; + DIIP { DUP ; CDDAAR ; # Q + DIP { DUP ; CDDDAAR } ; MUL ; } ; # K + DIP { COMPARE ; GT ; # new amount > Q * K + IF { FAIL } { } } ; # abort or continue + # then we rebuild the globals + DIP { DUP ; CDADDR } ; PAIR ; # seller amount + PUSH (Uint32 0) ; PAIR ; # delivery counter at 0 + DIP { CDDR } ; PAIR ; # parameters + # and return Void + PUSH Void ; PAIR } + { FAIL ; CDR ; PUSH Void ; PAIR }} # (Left _) + { FAIL ; DROP ; CDR ; PUSH Void ; PAIR }} # (Right _) + { # After T + 24 + # test if the required payment is reached + DUP ; CDDAAR ; # Q + DIP { DUP ; CDDDAAR } ; MUL ; # K + DIP { DUP ; CDADAR } ; # amount already versed by the buyer + COMPARE ; NEQ ; + IF { # not reached, pay the seller and destroy the contract + BALANCE ; + DIP { DUP ; CDDDDADR } # S + PUSH Void ; TRANSFER_TOKENS ; DROP ; + # and return Void + CDR ; PUSH Void ; PAIR } + { # otherwise continue + DUP ; CDDADAR # T + PUSH (Uint64 86400) ; ADD ; + PUSH (Uint64 86400) ; ADD ; # two days in second + NOW ; COMPARE ; LT + IF { # Between T + 24 and T + 48 + # We accept only delivery notifications, from W + DUP ; CDDDDDR ; MANAGER ; # W + SOURCE void void ; MANAGER ; + COMPARE ; NEQ ; + IF { FAIL } {} # fail if not the warehouse + DUP ; CADR ; # we must receive (Right amount) + IF_LEFT + { FAIL ; DROP ; CDR ; PUSH Void ; PAIR } # (Left _) + { # We increment the counter + DIP { DUP ; CDAAR } ; ADD ; + # And rebuild the globals in advance + DIP { DUP ; CDADR } ; PAIR ; + DIP CDDR ; PAIR ; + PUSH Void ; PAIR ; + # We test if enough have been delivered + DUP ; CDAAR ; + DIP { DUP ; CDDAAR } ; + COMPARE ; LT ; # counter < Q + IF { } # wait for more + { # Transfer all the money to the seller + BALANCE ; # and destroy the contract + DIP { DUP ; CDDDDADR } # S + PUSH Void ; TRANSFER_TOKENS ; DROP }}} + { # after T + 48, transfer everything to the buyer + BALANCE ; # and destroy the contract + DIP { DUP ; CDDDDAAR } # B + PUSH Void ; TRANSFER_TOKENS ; DROP ; + # and return void + CDR ; PUSH Void ; PAIR }}}}}} + +X - Full grammar +---------------- + + ::= + | + | + | Int8 + | Int16 + | Int32 + | Int64 + | Uint8 + | Uint16 + | Uint32 + | Uint64 + | Void + | True + | False + | Timestamp + | Signature + | Tez + | Key + | Left + | Right + | Or + | Ref + | Ref + | Some + | Some + | None + | Option + | Pair + | Pair + | List ... + | Set ... + | Map (Item ) ... + | Contract + | Lambda { ... } + ::= + | + | + | + | + | + | + | + | + | Void + | True + | False + | Pair + | Left + | Right + | Ref + | Some + | None + | List ... + | Set ... + | Map (Item ) ... + ::= + | { ... } + | DROP + | DUP + | SWAP + | PUSH + | SOME + | NONE + | IF_NONE { ... } { ... } + | PAIR + | CAR + | CDR + | LEFT + | RIGHT + | IF_LEFT { ... } { ... } + | NIL + | CONS + | IF_CONS { ... } { ... } + | EMPTY_SET + | EMPTY_MAP + | ITER + | MAP + | REDUCE + | MEM + | GET + | UPDATE + | REF + | DEREF + | SET + | IF { ... } { ... } + | LOOP { ... } + | LAMBDA { ... } + | EXEC + | DIP { ... } + | FAIL + | NOP + | CONCAT + | ADD + | SUB + | MUL + | DIV + | ABS + | NEG + | MOD + | LSL + | LSR + | OR + | AND + | XOR + | NOT + | COMPARE + | EQ + | NEQ + | LT + | GT + | LE + | GE + | CAST + | CHECKED_ABS + | CHECKED_NEG + | CHECKED_ADD + | CHECKED_SUB + | CHECKED_MUL + | CHECKED_CAST + | FLOOR + | CEIL + | INF + | NAN + | ISNAN + | NANAN + | MANAGER + | TRANSFER_TOKENS + | CREATE_ACCOUNT + | CREATE_CONTRACT + | NOW + | AMOUNT + | BALANCE + | CHECK_SIGNATURE + | H + | STEPS_TO_QUOTA + | SOURCE + ::= + | int8 + | int16 + | int32 + | int64 + | uint8 + | uint16 + | uint32 + | uint64 + | void + | string + | float + | tez + | bool + | key + | timestamp + | signature + | ref + | option + | list + | set + | contract + | pair + | union + | lambda + | map + ::= + | int8 + | int16 + | int32 + | int64 + | uint8 + | uint16 + | uint32 + | uint64 + | string + | float + | tez + | bool + | key + | timestamp + +XI - Reference implementation +----------------------------- + +The language is implemented in OCaml as follows: + + * The lower internal representation is written as a GADT whose type + parameters encode exactly the typing rules given in this + specification. In other words, if a program written in this + representation is accepted by OCaml's typechecker, it is + mandatorily type-safe. This of course also valid for programs not + handwritten but generated by OCaml code, so we are sure that any + manipulated code is type-safe. + + In the end, what remains to be checked is the encoding of the + typing rules as OCaml types, which boils down to half a line of + code for each instruction. Everything else is left to the + venerable and well trusted OCaml. + + * The interpreter is basically the direct transcription of the + rewriting rules presented above. It takes an instruction, a stack + and transforms it. OCaml's typechecker ensures that the + transformation respects the pre and post stack types declared by + the GADT case for each instruction. + + The only things that remain to we reviewed are value dependent + choices, such as that we did not swap true and false when + interpreting the If instruction. + + * The input, untyped internal representation is an OCaml ADT with + the only 5 grammar constructions: `String`, `Float`, `Int`, `Seq` + and `Prim`. It is the target language for the parser, since not + all parsable programs are well typed, and thus could simply not be + constructed using the GADT. + + * The typechecker is a simple function that recognizes the abstract + grammar described in section X by pattern matching, producing the + well-typed, corresponding GADT expressions. It is mostly a + checker, not a full inferer, and thus takes some annotations + (basically the inpout and output of the program, of lambdas and of + uninitialized imperative structures). It works by performing a + symbolic evaluation of the program, transforming a symbolic + stack. It only needs one pass over the whole program. + + Here again, OCaml does most of the checking, the structure of the + function is very simple, what we have to check is that we + transform a `Prim ("If", ...)` into an `If`, a `Prim ("Dup", ...)` + into a `Dup`, etc.