「Michelson：Tezosのスマートコントラクト言語」を編集中

= Michelson: the language of Smart Contracts in Tezos =

The language is stack based, with high level data types and primitives and strict static type checking. Its design cherry picks traits from several language families. Vigilant readers will notice direct references to Forth, Scheme, ML and Cat.

A Michelson program is a series of instructions that are run in sequence: each instruction receives as input the stack resulting of the previous instruction, and rewrites it for the next one. The stack contains both immediate values and heap allocated structures. All values are immutable and garbage collected.

A Michelson program receives as input a single element stack containing an input value and the contents of a storage space. It must return a single element stack containing an output value and the new contents of the storage space. Alternatively, a Michelson program can fail, explicitly using a specific opcode, or because something went wrong that could not be caught by the type system (e.g.?division by zero, gas exhaustion).

The types of the input, output and storage are fixed and monomorphic, and the program is typechecked before being introduced into the system. No smart contract execution can fail because an instruction has been executed on a stack of unexpected length or contents.

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 - Semantics
* II - Type system
* III - Core data types
* IV - Core instructions
* V - Operations
* VI - Domain specific data types
* VII - Domain specific operations
* VIII - Macros
* IX - Concrete syntax
* X - JSON syntax
* XI - Examples
* XII - Full grammar
* XIII - Reference implementation

== I - Semantics ==

This specification gives a detailed formal semantics of the Michelson language. It explains in a symbolic way the computation performed by the Michelson interpreter on a given program and initial stack to produce the corresponding resulting stack. The Michelson interpreter is a pure function: it only builds a result stack from the elements of an initial one, without affecting its environment. This semantics is then naturally given in what is called a big step form: a symbolic definition of a recursive reference interpreter. This definition takes the form of a list of rules that cover all the possible inputs of the interpreter (program and stack), and describe the computation of the corresponding resulting stacks.

Rules form and selection <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>

The rules have the main following form.

::

<pre>&gt; (syntax pattern) / (initial stack pattern)  =&gt;  (result stack pattern)
    iff (conditions)
    where (recursions)
and (more recursions)</pre>
The left hand side of the <code>=&gt;</code> sign is used for selecting the rule. Given a program and an initial stack, one (and only one) rule can be selected using the following process. First, the toplevel structure of the program must match the syntax pattern. This is quite simple since there is only a few non trivial patterns to deal with instruction sequences, and the rest is made of trivial pattern that match one specific instruction. Then, the initial stack must match the initial stack pattern. Finally, some rules add extra conditions over the values in the stack that follow the <code>iff</code> keyword. Sometimes, several rules may apply in a given context. In this case, the one that appears first in this specification is to be selected. If no rule applies, the result is equivalent to the one for the explicit <code>FAIL</code> instruction. This case does not happen on well-typed programs, as explained in the next section.

The right hand side describes the result of the interpreter if the rule applies. It consists in a stack pattern, whose part are either constants, or elements of the context (program and initial stack) that have been named on the left hand side of the <code>=&gt;</code> sign.

Recursive rules (big step form) <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>

Sometimes, the result of interpreting a program is derived from the result of interpreting another one (as in conditionals or function calls). In these cases, the rule contains a clause of the following form.

::

<pre>where (intermediate program) / (intermediate stack)  =&gt;  (partial result)</pre>
This means that this rules applies in case interpreting the intermediate state on the left gives the pattern on the right.

The left hand sign of the <code>=&gt;</code> sign is constructed from elements of the initial state or other partial results, and the right hand side identify parts that can be used to build the result stack of the rule.

If the partial result pattern does not actually match the result of the interpretation, then the result of the whole rule is equivalent to the one for the explicit <code>FAIL</code> instruction. Again, this case does not happen on well-typed programs, as explained in the next section.

Format of patterns <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

Code patterns are of one of the following syntactical forms.

* <code>INSTR</code> (an uppercase identifier) is a simple instruction (e.g. <code>DROP</code>);
* <code>INSTR (arg) ...</code> is a compound instruction, whose arguments can be code, data or type patterns (e.g. <code>PUSH nat 3</code>) ;
* <code>{ (instr) ; ... }</code> is a possibly empty sequence of instructions, (e.g. <code>IF { SWAP ; DROP } { DROP }</code>), nested sequences can drop the braces ;
* <code>name</code> is a pattern that matches any program and names a part of the matched program that can be used to build the result ;
* <code>_</code> is a pattern that matches any instruction.

Stack patterns are of one of the following syntactical forms.

* <code>[FAIL]</code> is the special failed state ;
* <code>[]</code> is the empty stack ;
* <code>(top) : (rest)</code> is a stack whose top element is matched by the data pattern <code>(top)</code> on the left, and whose remaining elements are matched by the stack pattern <code>(rest)</code> on the right (e.g. <code>x : y : rest</code>) ;
* <code>name</code> is a pattern that matches any stack and names it in order to use it to build the result ;
* <code>_</code> is a pattern that matches any stack.

Data patterns are of one of the following syntactical forms.

* integer/natural number literals, (e.g. <code>3</code>) ;
* string literals, (e.g. <code>&quot;contents&quot;</code>) ;
* <code>Tag</code> (capitalized) is a symbolic constant, (e.g. <code>Unit</code>, <code>True</code>, <code>False</code>) ;
* <code>(Tag (arg) ...)</code> tagged constructed data, (e.g. <code>(Pair 3 4)</code>) ;
* a code pattern for first class code values ;
* <code>name</code> to name a value in order to use it to build the result ;
* <code>_</code> to match any value.

The domain of instruction names, symbolic constants and data constructors is fixed by this specification. Michelson does not let the programmer introduce its own types.

Be aware that the syntax used in the specification may differ a bit from the concrete syntax, which is presented in Section IX. In particular, some instructions are annotated with types that are not present in the concrete language because they are synthesized by the typechecker.

Shortcuts <sub>~<sub>~</sub></sub>~

Sometimes, it is easier to think (and shorter to write) in terms of program rewriting than in terms of big step semantics. When it is the case, and when both are equivalents, we write rules of the form:

::

<pre>p / S  =&gt;  S''
where   p' / S'  =&gt;  S''</pre>
using the following shortcut:

::

<pre>p / S  =&gt;  p' / S'</pre>
The concrete language also has some syntax sugar to group some common sequences of operations as one. This is described in this specification using a simple regular expression style recursive instruction rewriting.

== II - Introduction to the type system and notations ==

This specification describes a type system for Michelson. To make things clear, in particular to readers that are not accustomed to reading formal programming language specifications, it does not give a typechecking or inference algorithm. It only gives an intentional definition of what we consider to be well-typed programs. For each syntactical form, it describes the stacks that are considered well-typed inputs, and the resulting outputs.

The type system is sound, meaning that if a program can be given a type, then if run on a well-typed input stack, the interpreter will never apply an interpretation rule on a stack of unexpected length or contents. Also, it will never reach a state where it cannot select an appropriate rule to continue the execution. Well-typed programs do not block, and do not go wrong.

Type notations <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~

The specification introduces notations for the types of values, terms and stacks. Apart from a subset of value types that appear in the form of type annotations in some places throughout the language, it is important to understand that this type language only exists in the specification.

A stack type can be written:

* <code>[]</code> for the empty stack ;
* <code>(top) : (rest)</code> for the stack whose first value has type <code>(top)</code> and queue has stack type <code>(rest)</code>.

Instructions, programs and primitives of the language are also typed, their types are written:

::

<pre>(type of stack before) -&gt; (type of stack after)</pre>
The types of values in the stack are written:

* <code>identifier</code> for a primitive data-type (e.g. <code>bool</code>),
* <code>identifier (arg)</code> for a parametric data-type with one parameter type <code>(arg)</code> (e.g. <code>list nat</code>),
* <code>identifier (arg) ...</code> for a parametric data-type with several parameters (e.g. <code>map string int</code>),
* <code>[ (type of stack before) -&gt; (type of stack after) ]</code> for a code quotation, (e.g. <code>[ int : int : [] -&gt; int : [] ]</code>),
* <code>lambda (arg) (ret)</code> is a shortcut for <code>[ (arg) : [] -&gt; (ret) : [] ]</code>.

Meta type variables <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>

The typing rules introduce meta type variables. To be clear, this has nothing to do with polymorphism, which Michelson does not have. These variables only live at the specification level, and are used to express the consistency between the parts of the program. For instance, the typing rule for the <code>IF</code> construct introduces meta variables to express that both branches must have the same type.

Here are the notations for meta type variables:

* <code>'a</code> for a type variable,
* <code>'A</code> for a stack type variable,
* <code>_</code> for an anonymous type or stack type variable.

Typing rules <sub><sub><sub><sub>~</sub></sub></sub>~</sub>

The system is syntax directed, which means here that it defines a single typing rule for each syntax construct. A typing rule restricts the type of input stacks that are authorized for this syntax construct, links the output type to the input type, and links both of them to the subexpressions when needed, using meta type variables.

Typing rules are of the form:

::

<pre>(syntax pattern)
:: (type of stack before) -&gt; (type of stack after) [rule-name]
   iff (premises)</pre>
Where premises are typing requirements over subprograms or values in the stack, both of the form <code>(x) :: (type)</code>, meaning that value <code>(x)</code> must have type <code>(type)</code>.

A program is shown well-typed if one can find an instance of a rule that applies to the toplevel program expression, with all meta type variables replaced by non variable type expressions, and of which all type requirements in the premises can be proven well-typed in the same manner. For the reader unfamiliar with formal type systems, this is called building a typing derivation.

Here is an example typing derivation on a small program that computes <code>(x+5)*10</code> for a given input <code>x</code>, obtained by instantiating the typing rules for instructions <code>PUSH</code>, <code>ADD</code> and for the sequence, as found in the next sections. When instantiating, we replace the <code>iff</code> with <code>by</code>.

::

<pre>{ PUSH nat 5 ; ADD ; PUSH nat 10 ; SWAP ; MUL }
:: [ nat : [] -&gt; nat : [] ]
   by { PUSH nat 5 ; ADD }
      :: [ nat : [] -&gt; nat : [] ]
         by PUSH nat 5
            :: [ nat : [] -&gt; nat : nat : [] ]
               by 5 :: nat
        and ADD
            :: [ nat : nat : [] -&gt; nat : [] ]
  and { PUSH nat 10 ; SWAP ; MUL }
      :: [ nat : [] -&gt; nat : [] ]
         by PUSH nat 10
            :: [ nat : [] -&gt; nat : nat : [] ]
               by 10 :: nat
        and { SWAP ; MUL }
            :: [ nat : nat : [] -&gt; nat : [] ]
               by SWAP
                  :: [ nat : nat : [] -&gt; nat : nat : [] ]
              and MUL
                  :: [ nat : nat : [] -&gt; nat : [] ]</pre>
Producing such a typing derivation can be done in a number of manners, such as unification or abstract interpretation. In the implementation of Michelson, this is done by performing a recursive symbolic evaluation of the program on an abstract stack representing the input type provided by the programmer, and checking that the resulting symbolic stack is consistent with the expected result, also provided by the programmer.

Annotations <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>

Most instructions in the language can optionally take an annotation. Annotations allow you to better track data, on the stack and within pairs and unions.

If added on the components of a type, the annotation will be propagated by the typechecker througout access instructions.

Annotating an instruction that produces a value on the stack will rewrite the annotation an the toplevel of its type.

Trying to annotate an instruction that does not produce a value will result in a typechecking error.

At join points in the program (<code>IF</code>, <code>IF_LEFT</code>, <code>IF_CONS</code>, <code>IF_NONE</code>, <code>LOOP</code>), annotations must be compatible. Annotations are compatible if both elements are annotated with the same annotation or if at least one of the values/types is unannotated.

Stack visualization tools like the Michelson’s Emacs mode print annotations associated with each type in the program, as propagated by the typechecker. This is useful as a debugging aid.

Side note <sub>~<sub>~</sub></sub>~

As with most type systems, it is incomplete. There are programs that cannot be given a type in this type system, yet that would not go wrong if executed. This is a necessary compromise to make the type system usable. Also, it is important to remember that the implementation of Michelson does not accept as many programs as the type system describes as well-typed. This is because the implementation uses a simple single pass typechecking algorithm, and does not handle any form of polymorphism.

== III - Core data types and notations ==

* <code>string</code>, <code>nat</code>, <code>int</code>: The core primitive constant types.
* <code>bool</code>: The type for booleans whose values are <code>True</code> and <code>False</code>
* <code>unit</code>: The type whose only value is <code>Unit</code>, to use as a placeholder when some result or parameter is non necessary. For instance, when the only goal of a contract is to update its storage.
* <code>list (t)</code>: A single, immutable, homogeneous linked list, whose elements are of type <code>(t)</code>, and that we note <code>{}</code> for the empty list or <code>{ first ; ... }</code>. In the semantics, we use chevrons to denote a subsequence of elements. For instance <code>{ head ; &lt;tail&gt; }</code>.
* <code>pair (l) (r)</code>: A pair of values <code>a</code> and <code>b</code> of types <code>(l)</code> and <code>(r)</code>, that we write <code>(Pair a b)</code>.
* <code>option (t)</code>: Optional value of type <code>(t)</code> that we note <code>None</code> or <code>(Some v)</code>.
* <code>or (l) (r)</code>: A union of two types: a value holding either a value <code>a</code> of type <code>(l)</code> or a value <code>b</code> of type <code>(r)</code>, that we write <code>(Left a)</code> or <code>(Right b)</code>.
* <code>set (t)</code>: Immutable sets of values of type <code>(t)</code> that we note as lists <code>{ item ; ... }</code>, of course with their elements unique, and sorted.
* <code>map (k) (t)</code>: Immutable maps from keys of type <code>(k)</code> of values of type <code>(t)</code> that we note <code>{ Elt key value ; ... }</code>, with keys sorted.
* <code>big_map (k) (t)</code>: Lazily deserialized maps from keys of type <code>(k)</code> of values of type <code>(t)</code> that we note <code>{ Elt key value ; ... }</code>, with keys sorted. These maps should be used if you intend to store large amounts of data in a map. They have higher gas costs than standard maps as data is lazily deserialized. You are limited to a single <code>big_map</code> per program, which must appear on the left hand side of a pair in the contract's storage.

== IV - Core instructions ==

Control structures <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

* <code>FAIL</code>: Explicitly abort the current program.

:: _ -&gt; _

This special instruction is callable in any context, since it does not use its input stack (first rule below), and makes the output useless since all subsequent instruction will simply ignore their usual semantics to propagate the failure up to the main result (second rule below). Its type is thus completely generic.

::

<pre>&gt; FAIL / _  =&gt;  [FAIL]
&gt; _ / [FAIL]  =&gt;  [FAIL]</pre>
* <code>{ I ; C }</code>: Sequence.

::

<pre>:: 'A   -&gt;   'C
   iff   I :: [ 'A -&gt; 'B ]
         C :: [ 'B -&gt; 'C ]

&gt; I ; C / SA  =&gt;  SC
    where   I / SA  =&gt;  SB
    and   C / SB  =&gt;  SC</pre>
* <code>IF bt bf</code>: Conditional branching.

::

<pre>:: bool : 'A   -&gt;   'B
   iff   bt :: [ 'A -&gt; 'B ]
         bf :: [ 'A -&gt; 'B ]

&gt; IF bt bf / True : S  =&gt;  bt / S
&gt; IF bt bf / False : S  =&gt;  bf / S</pre>
* <code>LOOP body</code>: A generic loop.

::

<pre>:: bool : 'A   -&gt;   'A
   iff   body :: [ 'A -&gt; bool : 'A ]

&gt; LOOP body / True : S  =&gt;  body ; LOOP body / S
&gt; LOOP body / False : S  =&gt;  S</pre>
* <code>LOOP_LEFT body</code>: A loop with an accumulator

::

<pre>:: (or 'a 'b) : 'A   -&gt;   'A
   iff   body :: [ 'a : 'A -&gt; (or 'a 'b) : 'A ]

&gt; LOOP_LEFT body / (Left a)  : S  =&gt;  body ; LOOP_LEFT body / (or 'a 'b) : S
&gt; LOOP_LEFT body / (Right b) : S  =&gt;  b : S</pre>
* <code>DIP code</code>: Runs code protecting the top of the stack.

::

<pre>:: 'b : 'A   -&gt;   'b : 'C
   iff   code :: [ 'A -&gt; 'C ]

&gt; DIP code / x : S  =&gt;  x : S'
    where    code / S  =&gt;  S'</pre>
* <code>EXEC</code>: Execute a function from the stack.

::

<pre>:: 'a : lambda 'a 'b : 'C   -&gt;   'b : 'C

&gt; EXEC / a : f : S  =&gt;  r : S
    where f / a : []  =&gt;  r : []</pre>
Stack operations ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>

* <code>DROP</code>: Drop the top element of the stack.

::

<pre>:: _ : 'A   -&gt;   'A

&gt; DROP / _ : S  =&gt;  S</pre>
* <code>DUP</code>: Duplicate the top of the stack.

::

<pre>:: 'a : 'A   -&gt;   'a : 'a : 'A

&gt; DUP / x : S  =&gt;  x : x : S</pre>
* <code>SWAP</code>: Exchange the top two elements of the stack.

::

<pre>:: 'a : 'b : 'A   -&gt;   'b : 'a : 'A

&gt; SWAP / x : y : S  =&gt;  y : x : S</pre>
* <code>PUSH 'a x</code>: Push a constant value of a given type onto the stack.

::

<pre>:: 'A   -&gt;   'a : 'A
   iff   x :: 'a

&gt; PUSH 'a x / S  =&gt;  x : S</pre>
* <code>UNIT</code>: Push a unit value onto the stack.

::

<pre>:: 'A   -&gt;   unit : 'A

&gt; UNIT / S  =&gt;  Unit : S</pre>
* <code>LAMBDA 'a 'b code</code>: Push a lambda with given parameter and return types onto the stack.

::

<pre>:: 'A -&gt;  (lambda 'a 'b) : 'A

&gt; LAMBDA _ _ code / S  =&gt;  code : S</pre>
Generic comparison <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

Comparison only works on a class of types that we call comparable. A <code>COMPARE</code> operation is defined in an ad hoc way for each comparable type, but the result of compare is always an <code>int</code>, which can in turn be checked in a generic manner using the following combinators. The result of <code>COMPARE</code> is <code>0</code> if the top two elements of the stack are equal, negative if the first element in the stack is less than the second, and positive otherwise.

* <code>EQ</code>: Checks that the top of the stack EQuals zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; EQ / 0 : S  =&gt;  True : S
&gt; EQ / v : S  =&gt;  False : S
    iff v &lt;&gt; 0</pre>
* <code>NEQ</code>: Checks that the top of the stack does Not EQual zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; NEQ / 0 : S  =&gt;  False : S
&gt; NEQ / v : S  =&gt;  True : S
    iff v &lt;&gt; 0</pre>
* <code>LT</code>: Checks that the top of the stack is Less Than zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; LT / v : S  =&gt;  True : S
    iff  v &lt; 0
&gt; LT / v : S  =&gt;  False : S
    iff v &gt;= 0</pre>
* <code>GT</code>: Checks that the top of the stack is Greater Than zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; GT / v : S  =&gt;  C / True : S
    iff  v &gt; 0
&gt; GT / v : S  =&gt;  C / False : S
    iff v &lt;= 0</pre>
* <code>LE</code>: Checks that the top of the stack is Less Than of Equal to zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; LE / v : S  =&gt;  True : S
    iff  v &lt;= 0
&gt; LE / v : S  =&gt;  False : S
    iff v &gt; 0</pre>
* <code>GE</code>: Checks that the top of the stack is Greater Than of Equal to zero.

::

<pre>:: int : 'S   -&gt;   bool : 'S

&gt; GE / v : S  =&gt;  True : S
    iff  v &gt;= 0
&gt; GE / v : S  =&gt;  False : S
    iff v &lt; 0</pre>
== V - Operations ==

Operations on booleans <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~

* <code>OR</code>

::

<pre>:: bool : bool : 'S   -&gt;   bool : 'S

&gt; OR / x : y : S  =&gt;  (x | y) : S</pre>
* <code>AND</code>

::

<pre>:: bool : bool : 'S   -&gt;   bool : 'S

&gt; AND / x : y : S  =&gt;  (x &amp; y) : S</pre>
* <code>XOR</code>

::

<pre>:: bool : bool : 'S   -&gt;   bool : 'S

&gt; XOR / x : y : S  =&gt;  (x ^ y) : S</pre>
* <code>NOT</code>

::

<pre>:: bool : 'S   -&gt;   bool : 'S

&gt; NOT / x : S  =&gt;  ~x : S</pre>
Operations on integers and natural numbers <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub><sub><sub><sub><sub>~</sub></sub></sub></sub><sub>~</sub>~</sub>~~

Integers and naturals are arbitrary-precision, meaning the only size limit is fuel.

* <code>NEG</code>

::

<pre>:: int : 'S   -&gt;   int : 'S
:: nat : 'S   -&gt;   int : 'S

&gt; NEG / x : S  =&gt;  -x : S</pre>
* <code>ABS</code>

::

<pre>:: int : 'S   -&gt;   nat : 'S

&gt; ABS / x : S  =&gt;  abs (x) : S</pre>
* <code>ADD</code>

::

<pre>:: int : int : 'S   -&gt;   int : 'S
:: int : nat : 'S   -&gt;   int : 'S
:: nat : int : 'S   -&gt;   int : 'S
:: nat : nat : 'S   -&gt;   nat : 'S

&gt; ADD / x : y : S  =&gt;  (x + y) : S</pre>
* <code>SUB</code>

::

<pre>:: int : int : 'S   -&gt;   int : 'S
:: int : nat : 'S   -&gt;   int : 'S
:: nat : int : 'S   -&gt;   int : 'S
:: nat : nat : 'S   -&gt;   int : 'S

&gt; SUB / x : y : S  =&gt;  (x - y) : S</pre>
* <code>MUL</code>

::

<pre>:: int : int : 'S   -&gt;   int : 'S
:: int : nat : 'S   -&gt;   int : 'S
:: nat : int : 'S   -&gt;   int : 'S
:: nat : nat : 'S   -&gt;   nat : 'S

&gt; MUL / x : y : S  =&gt;  (x * y) : S</pre>
* <code>EDIV</code> Perform Euclidian division

::

<pre>:: int : int : 'S   -&gt;   option (pair int nat) : 'S
:: int : nat : 'S   -&gt;   option (pair int nat) : 'S
:: nat : int : 'S   -&gt;   option (pair int nat) : 'S
:: nat : nat : 'S   -&gt;   option (pair nat nat) : 'S

&gt; EDIV / x : 0 : S  =&gt;  None : S
&gt; EDIV / x : y : S  =&gt;  Some (Pair (x / y) (x % y)) : S
    iff y &lt;&gt; 0</pre>
Bitwise logical operators are also available on unsigned integers.

* <code>OR</code>

::

<pre>:: nat : nat : 'S   -&gt;   nat : 'S

&gt; OR / x : y : S  =&gt;  (x | y) : S</pre>
* <code>AND</code>

::

<pre>:: nat : nat : 'S   -&gt;   nat : 'S

&gt; AND / x : y : S  =&gt;  (x &amp; y) : S</pre>
* <code>XOR</code>

::

<pre>:: nat : nat : 'S   -&gt;   nat : 'S

&gt; XOR / x : y : S  =&gt;  (x ^ y) : S</pre>
* <code>NOT</code> The return type of <code>NOT</code> is an <code>int</code> and not a <code>nat</code>. This is because the sign is also negated. The resulting integer is computed using two’s complement. For instance, the boolean negation of <code>0</code> is <code>-1</code>.

::

<pre>:: nat : 'S   -&gt;   int : 'S
:: int : 'S   -&gt;   int : 'S

&gt; NOT / x : S  =&gt;  ~x : S</pre>
* <code>LSL</code>

::

<pre>:: nat : nat : 'S   -&gt;   nat : 'S

&gt; LSL / x : s : S  =&gt;  (x &lt;&lt; s) : S
    iff   s &lt;= 256
&gt; LSL / x : s : S  =&gt;  [FAIL]
    iff   s &gt; 256</pre>
* <code>LSR</code>

::

<pre>:: nat : nat : 'S   -&gt;   nat : 'S

&gt; LSR / x : s : S  =&gt;  (x &gt;&gt;&gt; s) : S</pre>
* <code>COMPARE</code>: Integer/natural comparison

::

<pre>:: int : int : 'S   -&gt;   int : 'S
:: nat : nat : 'S   -&gt;   int : 'S

&gt; COMPARE / x : y : S  =&gt;  -1 : S
    iff x &lt; y
&gt; COMPARE / x : y : S  =&gt;  0 : S
    iff x = y
&gt; COMPARE / x : y : S  =&gt;  1 : S
    iff x &gt; y</pre>
Operations on strings <sub><sub><sub><sub><sub>~</sub></sub></sub></sub><sub>~</sub>~</sub>~~

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.

* <code>CONCAT</code>: String concatenation.

::

<pre>:: string : string : 'S   -&gt; string : 'S

&gt; CONCAT / s : t : S  =&gt;  (s ^ t) : S</pre>
* <code>COMPARE</code>: Lexicographic comparison.

::

<pre>:: string : string : 'S   -&gt;   int : 'S

&gt; COMPARE / s : t : S  =&gt;  -1 : S
    iff s &lt; t
&gt; COMPARE / s : t : S  =&gt;  0 : S
    iff s = t
&gt; COMPARE / s : t : S  =&gt;  1 : S
    iff s &gt; t</pre>
Operations on pairs <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>

* <code>PAIR</code>: Build a pair from the stack’s top two elements.

::

<pre>:: 'a : 'b : 'S   -&gt;   pair 'a 'b : 'S

&gt; PAIR / a : b : S  =&gt;  (Pair a b) : S</pre>
* <code>CAR</code>: Access the left part of a pair.

::

<pre>:: pair 'a _ : 'S   -&gt;   'a : 'S

&gt; CAR / (Pair a _) : S  =&gt;  a : S</pre>
* <code>CDR</code>: Access the right part of a pair.

::

<pre>:: pair _ 'b : 'S   -&gt;   'b : 'S

&gt; CDR / (Pair _ b) : S  =&gt;  b : S</pre>
Operations on sets <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

* <code>EMPTY_SET 'elt</code>: Build a new, empty set for elements of a given type.

The <code>'elt</code> type must be comparable (the <code>COMPARE</code> primitive must be defined over it).

::

<pre>:: 'S   -&gt;   set 'elt : 'S

&gt; EMPTY_SET _ / S  =&gt;  {} : S</pre>
* <code>MEM</code>: Check for the presence of an element in a set.

::

<pre>:: 'elt : set 'elt : 'S   -&gt;  bool : 'S

&gt; MEM / x : {} : S  =&gt;  false : S
&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  r : S
    iff COMPARE / x : hd : []  =&gt;  1 : []
    where MEM / x : v : { &lt;tl&gt; } : S  =&gt;  r : S
&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  true : S
    iff COMPARE / x : hd : []  =&gt;  0 : []
&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  false : S
    iff COMPARE / x : hd : []  =&gt;  -1 : []</pre>
* <code>UPDATE</code>: Inserts or removes an element in a set, replacing a previous value.

::

<pre>:: 'elt : bool : set 'elt : 'S   -&gt;   set 'elt : 'S

&gt; UPDATE / x : false : {} : S  =&gt;  {} : S
&gt; UPDATE / x : true : {} : S  =&gt;  { x } : S
&gt; UPDATE / x : v : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl'&gt; } : S
    iff COMPARE / x : hd : []  =&gt;  1 : []
    where UPDATE / x : v : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S
&gt; UPDATE / x : false : { hd ; &lt;tl&gt; } : S  =&gt;  { &lt;tl&gt; } : S
    iff COMPARE / x : hd : []  =&gt;  0 : []
&gt; UPDATE / x : true : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl&gt; } : S
    iff COMPARE / x : hd : []  =&gt;  0 : []
&gt; UPDATE / x : false : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl&gt; } : S
    iff COMPARE / x : hd : []  =&gt;  -1 : []
&gt; UPDATE / x : true : { hd ; &lt;tl&gt; } : S  =&gt;  { x ; hd ; &lt;tl&gt; } : S
    iff COMPARE / x : hd : []  =&gt;  -1 : []</pre>
* <code>REDUCE</code>: Apply a function on a set passing the result of each application to the next one and return the last.

::

<pre>:: lambda (pair 'elt * 'b) 'b : set 'elt : 'b : 'S   -&gt;   'b : 'S

&gt; REDUCE / f : {} : b : S  =&gt;  b : S
&gt; REDUCE / f : { hd : &lt;tl&gt; } : b : S  =&gt;  REDUCE / f : { &lt;tl&gt; } : c : S
    where f / Pair hd b : []  =&gt;  c : []</pre>
* <code>ITER body</code>: Apply the body expression to each element of a set. The body sequence has access to the stack.

::

<pre>:: (set 'elt) : 'A   -&gt;  'A
   iff body :: [ 'elt : 'A -&gt; 'A ]

&gt; ITER body / {} : S  =&gt;  S
&gt; ITER body / { hd ; &lt;tl&gt; } : S  =&gt;  body; ITER body / hd : { &lt;tl&gt; } : S</pre>
* <code>SIZE</code>: Get the cardinality of the set.

::

<pre>:: set 'elt : 'S -&gt; nat : 'S

&gt; SIZE / {} : S  =&gt;  0 : S
&gt; SIZE / { _ ; &lt;tl&gt; } : S  =&gt;  1 + s : S
    where SIZE / { &lt;tl&gt; } : S  =&gt;  s : S</pre>
Operations on maps <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

* <code>EMPTY_MAP 'key 'val</code>: Build a new, empty map from keys of a given type to values of another given type.

The <code>'key</code> type must be comparable (the <code>COMPARE</code> primitive must be defined over it).

::

<pre>:: 'S -&gt; map 'key 'val : 'S

&gt; EMPTY_MAP _ _ / S  =&gt;  {} : S</pre>
* <code>GET</code>: Access an element in a map, returns an optional value to be checked with <code>IF_SOME</code>.

::

<pre>:: 'key : map 'key 'val : 'S   -&gt;   option 'val : 'S

&gt; GET / x : {} : S  =&gt;  None : S
&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  opt_y : S
    iff COMPARE / x : k : []  =&gt;  1 : []
where GET / x : { &lt;tl&gt; } : S  =&gt;  opt_y : S
&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  Some v : S
    iff COMPARE / x : k : []  =&gt;  0 : []
&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  None : S
    iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
* <code>MEM</code>: Check for the presence of a binding for a key in a map.

::

<pre>:: 'key : map 'key 'val : 'S   -&gt;  bool : 'S

&gt; MEM / x : {} : S  =&gt;  false : S
&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  r : S
    iff COMPARE / x : k : []  =&gt;  1 : []
    where MEM / x : { &lt;tl&gt; } : S  =&gt;  r : S
&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  true : S
    iff COMPARE / x : k : []  =&gt;  0 : []
&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  false : S
    iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
* <code>UPDATE</code>: Assign or remove an element in a map.

::

<pre>:: 'key : option 'val : map 'key 'val : 'S   -&gt;   map 'key 'val : 'S

&gt; UPDATE / x : None : {} : S  =&gt;  {} : S
&gt; UPDATE / x : Some y : {} : S  =&gt;  { Elt x y } : S
&gt; UPDATE / x : opt_y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k v ; &lt;tl'&gt; } : S
    iff COMPARE / x : k : []  =&gt;  1 : []
where UPDATE / x : opt_y : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S
&gt; UPDATE / x : None : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { &lt;tl&gt; } : S
    iff COMPARE / x : k : []  =&gt;  0 : []
&gt; UPDATE / x : Some y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k y ; &lt;tl&gt; } : S
    iff COMPARE / x : k : []  =&gt;  0 : []
&gt; UPDATE / x : None : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k v ; &lt;tl&gt; } : S
    iff COMPARE / x : k : []  =&gt;  -1 : []
&gt; UPDATE / x : Some y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt x y ; Elt k v ; &lt;tl&gt; } : S
    iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
* <code>MAP</code>: Apply a function on a map and return the map of results under the same bindings.

::

<pre>:: lambda (pair 'key 'val) 'b : map 'key 'val : 'S   -&gt;   map 'key 'b : 'S

&gt; MAP / f : {} : S  =&gt;  {} : S
&gt; MAP / f : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k (f (Pair k v)) ; &lt;tl'&gt; } : S
    where MAP / f : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S</pre>
* <code>MAP body</code>: Apply the body expression to each element of a map. The body sequence has access to the stack.

::

<pre>:: (map 'key 'val) : 'A   -&gt;  (map 'key 'b) : 'A
   iff   body :: [ (pair 'key 'val) : 'A -&gt; 'b : 'A ]

&gt; MAP body / {} : S  =&gt;  {} : S
&gt; MAP body / { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k (body (Pair k v)) ; &lt;tl'&gt; } : S
    where MAP body / { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S</pre>
* <code>REDUCE</code>: Apply a function on a map passing the result of each application to the next one and return the last.

::

<pre>:: lambda (pair (pair 'key 'val) 'b) 'b : map 'key 'val : 'b : 'S   -&gt;   'b : 'S

&gt; REDUCE / f : {} : b : S  =&gt;  b : S
&gt; REDUCE / f : { Elt k v ; &lt;tl&gt; } : b : S  =&gt;  REDUCE / f : { &lt;tl&gt; } : c : S
    where f / Pair (Pair k v) b : []  =&gt;  c</pre>
* <code>ITER body</code>: Apply the body expression to each element of a map. The body sequence has access to the stack.

::

<pre>:: (map 'elt 'val) : 'A   -&gt;  'A
   iff   body :: [ (pair 'elt 'val) : 'A -&gt; 'A ]

&gt; ITER body / {} : S  =&gt;  S
&gt; ITER body / { Elt k v ; &lt;tl&gt; } : S  =&gt;  body ; ITER body / (Pair k v) : { &lt;tl&gt; } : S</pre>
* <code>SIZE</code>: Get the cardinality of the map.

::

<pre>:: map 'key 'val : 'S -&gt; nat : 'S

&gt; SIZE / {} : S  =&gt;  0 : S
&gt; SIZE / { _ ; &lt;tl&gt; } : S  =&gt;  1 + s : S
    where  SIZE / { &lt;tl&gt; } : S  =&gt;  s : S</pre>
Operations on <code>big_maps</code> <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub>~</sub>~~

The behaviour of these operations is the same as if they were normal maps, except that under the hood, the elements are loaded and deserialized on demand.

* <code>GET</code>: Access an element in a <code>big_map</code>, returns an optional value to be checked with <code>IF_SOME</code>.

::

<pre>:: 'key : big_map 'key 'val : 'S   -&gt;   option 'val : 'S</pre>
* <code>MEM</code>: Check for the presence of an element in a <code>big_map</code>.

::

<pre>:: 'key : big_map 'key 'val : 'S   -&gt;  bool : 'S</pre>
* <code>UPDATE</code>: Assign or remove an element in a <code>big_map</code>.

::

<pre>:: 'key : option 'val : big_map 'key 'val : 'S   -&gt;   big_map 'key 'val : 'S</pre>
Operations on optional values <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>~~

* <code>SOME</code>: Pack a present optional value.

::

<pre>:: 'a : 'S   -&gt;   option 'a : 'S

&gt; SOME / v : S  =&gt;  (Some v) : S</pre>
* <code>NONE 'a</code>: The absent optional value.

::

<pre>:: 'S   -&gt;   option 'a : 'S

&gt; NONE / v : S  =&gt;  None : S</pre>
* <code>IF_NONE bt bf</code>: Inspect an optional value.

::

<pre>:: option 'a : 'S   -&gt;   'b : 'S
   iff   bt :: [ 'S -&gt; 'b : 'S]
         bf :: [ 'a : 'S -&gt; 'b : 'S]

&gt; IF_NONE bt bf / (None) : S  =&gt;  bt / S
&gt; IF_NONE bt bf / (Some a) : S  =&gt;  bf / a : S</pre>
Operations on unions <sub><sub><sub><sub>~</sub></sub></sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>

* <code>LEFT 'b</code>: Pack a value in a union (left case).

::

<pre>:: 'a : 'S   -&gt;   or 'a 'b : 'S

&gt; LEFT / v : S  =&gt;  (Left v) : S</pre>
* <code>RIGHT 'a</code>: Pack a value in a union (right case).

::

<pre>:: 'b : 'S   -&gt;   or 'a 'b : 'S

&gt; RIGHT / v : S  =&gt;  (Right v) : S</pre>
* <code>IF_LEFT bt bf</code>: Inspect a value of a variant type.

::

<pre>:: or 'a 'b : 'S   -&gt;   'c : 'S
   iff   bt :: [ 'a : 'S -&gt; 'c : 'S]
         bf :: [ 'b : 'S -&gt; 'c : 'S]

&gt; IF_LEFT bt bf / (Left a) : S  =&gt;  bt / a : S
&gt; IF_LEFT bt bf / (Right b) : S  =&gt;  bf / b : S</pre>
* <code>IF_RIGHT bt bf</code>: Inspect a value of a variant type.

::

<pre>:: or 'a 'b : 'S   -&gt;   'c : 'S
   iff   bt :: [ 'b : 'S -&gt; 'c : 'S]
         bf :: [ 'a : 'S -&gt; 'c : 'S]

&gt; IF_RIGHT bt bf / (Right b) : S  =&gt;  bt / b : S
&gt; IF_RIGHT bt bf / (Left a) : S  =&gt;  bf / a : S</pre>
Operations on lists <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>

* <code>CONS</code>: Prepend an element to a list.

::

<pre>:: 'a : list 'a : 'S   -&gt;   list 'a : 'S

&gt; CONS / a : { &lt;l&gt; } : S  =&gt;  { a ; &lt;l&gt; } : S</pre>
* <code>NIL 'a</code>: The empty list.

::

<pre>:: 'S   -&gt;   list 'a : 'S

&gt; NIL / S  =&gt;  {} : S</pre>
* <code>IF_CONS bt bf</code>: Inspect an optional value.

::

<pre>:: list 'a : 'S   -&gt;   'b : 'S
   iff   bt :: [ 'a : list 'a : 'S -&gt; 'b : 'S]
         bf :: [ 'S -&gt; 'b : 'S]

&gt; IF_CONS bt bf / { a ; &lt;rest&gt; } : S  =&gt;  bt / a : { &lt;rest&gt; } : S
&gt; IF_CONS bt bf / {} : S  =&gt;  bf / S</pre>
* <code>MAP</code>: Apply a function on a list from left to right and return the list of results in the same order.

::

<pre>:: lambda 'a 'b : list 'a : 'S -&gt; list 'b : 'S

&gt; MAP / f : { a ; &lt;rest&gt; } : S  =&gt;  { f a ; &lt;rest'&gt; } : S
    where MAP / f : { &lt;rest&gt; } : S  =&gt;  { &lt;rest'&gt; } : S
&gt; MAP / f : {} : S  =&gt;  {} : S</pre>
* <code>MAP body</code>: Apply the body expression to each element of the list. The body sequence has access to the stack.

::

<pre>:: (list 'elt) : 'A   -&gt;  (list 'b) : 'A
   iff   body :: [ 'elt : 'A -&gt; 'b : 'A ]

&gt; MAP body / { a ; &lt;rest&gt; } : S  =&gt;  { body a ; &lt;rest'&gt; } : S
    where MAP body / { &lt;rest&gt; } : S  =&gt;  { &lt;rest'&gt; } : S
&gt; MAP body / {} : S  =&gt;  {} : S</pre>
* <code>REDUCE</code>: Apply a function on a list from left to right passing the result of each application to the next one and return the last.

::

<pre>:: lambda (pair 'a 'b) 'b : list 'a : 'b : 'S -&gt; 'b : 'S

&gt; REDUCE / f : { a : &lt;rest&gt; } : b : S  =&gt;  REDUCE / f : { &lt;rest&gt; } : c : S
    where f / Pair a b : []  =&gt;  c
&gt; REDUCE / f : {} : b : S  =&gt;  b : S</pre>
* <code>SIZE</code>: Get the number of elements in the list.

::

<pre>:: list 'elt : 'S -&gt; nat : 'S

&gt; SIZE / { _ ; &lt;rest&gt; } : S  =&gt;  1 + s : S
    where  SIZE / { &lt;rest&gt; } : S  =&gt;  s : S
&gt; SIZE / {} : S  =&gt;  0 : S</pre>
* <code>ITER body</code>: Apply the body expression to each element of a list. The body sequence has access to the stack.

::

<pre>:: (list 'elt) : 'A   -&gt;  'A
     iff body :: [ 'elt : 'A -&gt; 'A ]
&gt; ITER body / { a ; &lt;rest&gt; } : S  =&gt;  body ; ITER body / a : { &lt;rest&gt; } : S
&gt; ITER body / {} : S  =&gt;  S</pre>
== VI - Domain specific data types ==

* <code>timestamp</code>: Dates in the real world.
* <code>tez</code>: A specific type for manipulating tokens.
* <code>contract 'param 'result</code>: A contract, with the type of its code.
* <code>key</code>: A public cryptography key.
* <code>key_hash</code>: The hash of a public cryptography key.
* <code>signature</code>: A cryptographic signature.

== VII - Domain specific operations ==

Operations on timestamps <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>

Current Timestamps can be obtained by the <code>NOW</code> operation, or retrieved from script parameters or globals.

* <code>ADD</code> Increment / decrement a timestamp of the given number of seconds.

::

<pre>:: timestamp : int : 'S -&gt; timestamp : 'S
:: int : timestamp : 'S -&gt; timestamp : 'S

&gt; ADD / seconds : nat (t) : S  =&gt;  (seconds + t) : S
&gt; ADD / nat (t) : seconds : S  =&gt;  (t + seconds) : S</pre>
* <code>SUB</code> Subtract a number of seconds from a timestamp.

::

<pre>:: timestamp : int : 'S -&gt; timestamp : 'S

&gt; SUB / seconds : nat (t) : S  =&gt;  (seconds - t) : S</pre>
* <code>SUB</code> Subtract two timestamps.

::

<pre>:: timestamp : timestamp : 'S -&gt; int : 'S

&gt; SUB / seconds(t1) : seconds(t2) : S  =&gt;  (t1 - t2) : S</pre>
* <code>COMPARE</code>: Timestamp comparison.

::

<pre>:: timestamp : timestamp : 'S   -&gt;   int : 'S

&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  -1 : S
    iff t1 &lt; t2
&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  0 : S
    iff t1 = t2
&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  1 : S
    iff t1 &gt; t2</pre>
Operations on Tez <sub>~<sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~

Tez are internally represented by a 64 bit signed integer. There are restrictions to prevent creating a negative amount of tez. Operations are limited to prevent overflow and mixing them with other numerical types by mistake. They are also mandatory checked for under/overflows.

* <code>ADD</code>:

::

<pre>:: tez : tez : 'S   -&gt;   tez : 'S

&gt; ADD / x : y : S  =&gt;  [FAIL]   on overflow
&gt; ADD / x : y : S  =&gt;  (x + y) : S</pre>
* <code>SUB</code>:

::

<pre>:: tez : tez : 'S   -&gt;   tez : 'S

&gt; SUB / x : y : S  =&gt;  [FAIL]
    iff   x &lt; y
&gt; SUB / x : y : S  =&gt;  (x - y) : S</pre>
* <code>MUL</code>

::

<pre>:: tez : nat : 'S   -&gt;   tez : 'S
:: nat : tez : 'S   -&gt;   tez : 'S

&gt; MUL / x : y : S  =&gt;  [FAIL]   on overflow
&gt; MUL / x : y : S  =&gt;  (x * y) : S</pre>
* <code>EDIV</code>

::

<pre>:: tez : nat : 'S   -&gt;   option (pair tez tez) : 'S
:: tez : tez : 'S   -&gt;   option (pair nat tez) : 'S

&gt; EDIV / x : 0 : S  =&gt;  None
&gt; EDIV / x : y : S  =&gt;  Some (Pair (x / y) (x % y)) : S
    iff y &lt;&gt; 0</pre>
* <code>COMPARE</code>

::

:: tez : tez : ’S -&gt; int : ’S

<blockquote>COMPARE / x : y : S =&gt; -1 : S iff x &lt; y COMPARE / x : y : S =&gt; 0 : S iff x = y COMPARE / x : y : S =&gt; 1 : S iff x &gt; y
</blockquote>
Operations on contracts <sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>~<sub><sub><sub>~</sub></sub></sub>

* <code>MANAGER</code>: Access the manager of a contract.

::

<pre>:: contract 'p 'r : 'S   -&gt;   key_hash : 'S</pre>
* <code>CREATE_CONTRACT</code>: Forge a new contract.

::

<pre>:: key_hash : option key_hash : bool : bool : tez : lambda (pair 'p 'g) (pair 'r 'g) : 'g : 'S
   -&gt; contract 'p 'r : 'S</pre>
As with non code-emitted originations the contract code takes as argument the transferred 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: <code>(Pair arg globals)) -&gt; (Pair ret globals)</code>, as extrapolatable 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.

* <code>CREATE_CONTRACT { storage 'g ; parameter 'p ; return 'r ; code ... }</code>: Forge a new contract from a literal.

::

<pre>:: key_hash : option key_hash : bool : bool : tez : 'g : 'S
   -&gt; contract 'p 'r : 'S</pre>
Originate a contract based on a literal. This is currently the only way to include transfers inside of an originated contract. 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.

* <code>CREATE_ACCOUNT</code>: Forge an account (a contract without code).

::

<pre>:: key_hash : option key_hash : bool : tez : 'S   -&gt;   contract unit unit : 'S</pre>
Take as argument the manager, optional delegate, the delegatable flag and finally the initial amount taken from the currently executed contract.

* <code>TRANSFER_TOKENS</code>: Forge and evaluate a transaction.

::

<pre>:: 'p : tez : contract 'p 'r : 'g : []   -&gt;   'r : 'g : []</pre>
The parameter and return value must be consistent with the ones expected by the contract, unit 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).

* <code>BALANCE</code>: Push the current amount of tez of the current contract.

::

<pre>:: 'S   -&gt;   tez : 'S</pre>
* <code>SOURCE 'p 'r</code>: Push the source contract of the current transaction.

::

<pre>:: 'S   -&gt;   contract 'p 'r : 'S</pre>
* <code>SELF</code>: Push the current contract.

::

<pre>:: 'S   -&gt;   contract 'p 'r : 'S
   where   contract 'p 'r is the type of the current contract</pre>
* <code>AMOUNT</code>: Push the amount of the current transaction.

::

<pre>:: 'S   -&gt;   tez : 'S</pre>
* <code>DEFAULT_ACCOUNT</code>: Return a default contract with the given public/private key pair. Any funds deposited in this contract can immediately be spent by the holder of the private key. This contract cannot execute Michelson code and will always exist on the blockchain.

::

<pre>:: key_hash : 'S   -&gt;   contract unit unit : 'S</pre>
Special operations <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

* <code>STEPS_TO_QUOTA</code>: Push the remaining steps before the contract execution must terminate.

::

<pre>:: 'S   -&gt;   nat : 'S</pre>
* <code>NOW</code>: Push the timestamp of the block whose validation triggered this execution (does not change during the execution of the contract).

::

<pre>:: 'S   -&gt;   timestamp : 'S</pre>
Cryptographic primitives <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>

* <code>HASH_KEY</code>: Compute the b58check of a public key.

::

<pre>:: key : 'S   -&gt;   key_hash : 'S</pre>
* <code>H</code>: Compute a cryptographic hash of the value contents using the Blake2B cryptographic hash function.

::

<pre>:: 'a : 'S   -&gt;   string : 'S</pre>
* <code>CHECK_SIGNATURE</code>: Check that a sequence of bytes has been signed with a given key.

::

<pre>:: key : pair signature string : 'S   -&gt;   bool : 'S</pre>
* <code>COMPARE</code>:

::

<pre>:: key_hash : key_hash : 'S   -&gt;   int : 'S

&gt; COMPARE / x : y : S  =&gt;  -1 : S
    iff x &lt; y
&gt; COMPARE / x : y : S  =&gt;  0 : S
    iff x = y
&gt; COMPARE / x : y : S  =&gt;  1 : S
    iff x &gt; y</pre>
== VIII - Macros ==

In addition to the operations above, several extensions have been added to the language’s concrete syntax. If you are interacting with the node via RPC, bypassing the client, which expands away these macros, you will need to de-surgar them yourself.

These macros are designed to be unambiguous and reversible, meaning that errors are reported in terms of de-sugared syntax. Below you’ll see these macros defined in terms of other syntactic forms. That is how these macros are seen by the node.

Compare <sub><sub><sub>~</sub></sub></sub>

Syntactic sugar exists for merging <code>COMPARE</code> and comparison combinators, and also for branching.

* <code>CMP{EQ|NEQ|LT|GT|LE|GE}</code>

::

<pre>&gt; CMP(\op) / S  =&gt;  COMPARE ; (\op) / S</pre>
* <code>IF{EQ|NEQ|LT|GT|LE|GE} bt bf</code>

::

<pre>&gt; IF(\op) bt bf / S  =&gt;  (\op) ; IF bt bf / S</pre>
* <code>IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf</code>

::

<pre>&gt; IFCMP(\op) / S  =&gt;  COMPARE ; (\op) ; IF bt bf / S</pre>
Assertion Macros ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>

All assertion operations are syntactic sugar for conditionals with a <code>FAIL</code> instruction in the appropriate branch. When possible, use them to increase clarity about illegal states.

* <code>ASSERT</code>:

::

<pre>&gt; ASSERT  =&gt;  IF {} {FAIL}</pre>
* <code>ASSERT_{EQ|NEQ|LT|LE|GT|GE}</code>:

::

<pre>&gt; ASSERT_(\op)  =&gt;  IF(\op) {} {FAIL}</pre>
* <code>ASSERT_CMP{EQ|NEQ|LT|LE|GT|GE}</code>:

::

<pre>&gt; ASSERT_CMP(\op)  =&gt;  IFCMP(\op) {} {FAIL}</pre>
* <code>ASSERT_NONE</code>

::

<pre>&gt; ASSERT_NONE  =&gt;  IF_NONE {} {FAIL}</pre>
* <code>ASSERT_SOME</code>

::

<pre>&gt; ASSERT_SOME  =&gt;  IF_SOME {FAIL} {}</pre>
* <code>ASSERT_LEFT</code>:

::

<pre>&gt; ASSERT_LEFT  =&gt;  IF_LEFT {} {FAIL}</pre>
* <code>ASSERT_RIGHT</code>:

::

<pre>&gt; ASSERT_RIGHT  =&gt;  IF_LEFT {FAIL} {}</pre>
Syntactic Conveniences <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~

These are macros are simply more convenient syntax for various common operations.

* <code>DII+P code</code>: A syntactic sugar for working deeper in the stack.

::

<pre>&gt; DII(\rest=I*)P code / S  =&gt;  DIP (DI(\rest)P code) / S</pre>
* <code>DUU+P</code>: A syntactic sugar for duplicating the <code>n</code>?th element of the stack.

::

<pre>&gt; DUU(\rest=U*)P / S  =&gt;  DIP (DU(\rest)P) ; SWAP / S</pre>
* <code>P(A*AI)+R</code>: A syntactic sugar for building nested pairs in bulk.

::

<pre>&gt; P(\fst=A*)AI(\rest=(A*AI)+)R / S  =&gt;  P(\fst)AIR ; P(\rest)R / S
&gt; PA(\rest=A*)AIR / S  =&gt;  DIP (P(\rest)AIR) / S</pre>
* <code>C[AD]+R</code>: A syntactic sugar for accessing fields in nested pairs.

::

<pre>&gt; CA(\rest=[AD]+)R / S  =&gt;  CAR ; C(\rest)R / S
&gt; CD(\rest=[AD]+)R / S  =&gt;  CDR ; C(\rest)R / S</pre>
* <code>IF_SOME bt bf</code>: Inspect an optional value.

::

<pre>:: option 'a : 'S   -&gt;   'b : 'S
   iff   bt :: [ 'a : 'S -&gt; 'b : 'S]
         bf :: [ 'S -&gt; 'b : 'S]

&gt; IF_SOME / (Some a) : S  =&gt;  bt / a : S
&gt; IF_SOME / (None) : S  =&gt;  bf / S</pre>
* <code>SET_CAR</code>: Set the first value of a pair.

::

<pre>&gt; SET_CAR  =&gt;  CDR ; SWAP ; PAIR</pre>
* <code>SET_CDR</code>: Set the first value of a pair.

::

<pre>&gt; SET_CDR  =&gt;  CAR ; PAIR</pre>
* <code>SET_C[AD]+R</code>: A syntactic sugar for setting fields in nested pairs.

::

<pre>&gt; SET_CA(\rest=[AD]+)R / S   =&gt;
    { DUP ; DIP { CAR ; SET_C(\rest)R } ; CDR ; SWAP ; PAIR } / S
&gt; SET_CD(\rest=[AD]+)R / S   =&gt;
    { DUP ; DIP { CDR ; SET_C(\rest)R } ; CAR ; PAIR } / S</pre>
* <code>MAP_CAR</code> code: Transform the first value of a pair.

::

<pre>&gt; MAP_CAR code  =&gt;  DUP ; CDR ; SWAP ; code ; CAR ; PAIR</pre>
* <code>MAP_CDR</code> code: Transform the first value of a pair.

::

<pre>&gt; MAP_CDR code  =&gt;  DUP ; CDR ; code ; SWAP ; CAR ; PAIR</pre>
* <code>MAP_C[AD]+R</code> code: A syntactic sugar for transforming fields in nested pairs.

::

<pre>&gt; MAP_CA(\rest=[AD]+)R / S   =&gt;
    { DUP ; DIP { CAR ; MAP_C(\rest)R code } ; CDR ; SWAP ; PAIR } / S
&gt; MAP_CD(\rest=[AD]+)R / S   =&gt;
    { DUP ; DIP { CDR ; MAP_C(\rest)R code } ; CAR ; PAIR } / S</pre>
== IX - Concrete syntax ==

The concrete language is very close to the formal notation of the specification. Its structure is extremely simple: an expression in the language can only be one of the four following constructs.

# An integer.
# A character string.
# The application of a primitive to a sequence of expressions.
# A sequence of expressions.

This simple four cases notation is called Micheline.

Constants <sub>~<sub>~</sub></sub>~

There are two kinds of constants:

# Integers or naturals in decimal (no prefix), hexadecimal (0x prefix), octal (0o prefix) or binary (0b prefix).
# Strings with usual escapes <code>\n</code>, <code>\t</code>, <code>\b</code>, <code>\r</code>, <code>\\</code>, <code>\&quot;</code>. The encoding of a Michelson source file must be UTF-8, and non-ASCII characters can only appear in comments. No line break can appear in a string. Any non-printable characters must be escaped using two hexadecimal characters, as in <code>\xHH</code> or the predefine escape sequences above..

Primitive applications <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~

A primitive application is a name followed by arguments

::

<pre>prim arg1 arg2</pre>
When a primitive application is the argument to another primitive application, it must be wrapped with parentheses.

::

<pre>prim (prim1 arg11 arg12) (prim2 arg21 arg22)</pre>
Sequences <sub>~<sub>~</sub></sub>~

Successive expression can be grouped as a single sequence expression using curly braces as delimiters and semicolon as separators.

::

<pre>{ expr1 ; expr2 ; expr3 ; expr4 }</pre>
A sequence can be passed as argument to a primitive.

::

<pre>prim arg1 arg2 { arg3_expr1 ; arg3_expr2 }</pre>
Primitive applications right inside a sequence cannot be wrapped.

::

<pre>{ (prim arg1 arg2) } # is not ok</pre>
Indentation <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>

To remove ambiguities for human readers, the parser enforces some indentation rules.

* For sequences:
* All expressions in a sequence must be aligned on the same column.
* An exception is made when consecutive expressions fit on the same line, as long as the first of them is correctly aligned.
* All expressions in a sequence must be indented to the right of the opening curly brace by at least one column.
* The closing curly brace cannot be on the left of the opening one.
* For primitive applications:
* All arguments in an application must be aligned on the same column.
* An exception is made when consecutive arguments fit on the same line, as long as the first of them is correctly aligned.
* All arguments in a sequence must be indented to the right of the primitive name by at least one column.

.. _annotations-1:

Annotations <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>

Sequences and primitive applications can receive an annotation.

An annotation is a lowercase identifier that starts with an <code>@</code> sign. It comes after the opening curly brace for sequence, and after the primitive name for primitive applications.

::

<pre>{ @annot
  expr ;
  expr ;
  ... }

(prim @annot arg arg ...)</pre>
Differences with the formal notation <sub><sub><sub><sub>~</sub></sub></sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>~<sub>~</sub>

The concrete syntax follows the same lexical conventions as the specification: instructions are represented by uppercase identifiers, type constructors by lowercase identifiers, and constant constructors are Capitalized.

All domain specific constants are Micheline strings with specific formats:

* <code>tez</code> amounts are written using the same notation as JSON schemas and the command line client: thousands are optionally separated by commas, and so goes for mutez.
* in regexp form: <code>([0-9]{1,3}(,[0-9]{3})+)|[0-9]+(\.[0.9]{2})?</code>
* <code>&quot;1234567&quot;</code> means 1234567 tez
* <code>&quot;1,234,567&quot;</code> means 1234567 tez
* <code>&quot;1234567.89&quot;</code> means 1234567890000 mutez
* <code>&quot;1,234,567.0&quot;</code> means 123456789 tez
* <code>&quot;10,123.456,789&quot;</code> means 10123456789 mutez
* <code>&quot;1234,567&quot;</code> is invalid
* <code>&quot;1,234,567.123456&quot;</code> is invalid
* <code>timestamp</code>?s are written using <code>RFC 339</code> notation.
* <code>contract</code>?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.
* <code>key</code>?s are <code>Blake2B</code> hashes of <code>ed25519</code> public keys encoded in <code>base58</code> format with the following custom alphabet: <code>&quot;eXMNE9qvHPQDdcFx5J86rT7VRm2atAypGhgLfbS3CKjnksB4&quot;</code>.
* <code>signature</code>?s are <code>ed25519</code> signatures as a series of hex-encoded bytes.

To prevent errors, control flow primitives that take instructions as parameters require sequences in the concrete syntax.

::

<pre>IF { instr1_true ; instr2_true ; ... }
   { instr1_false ; instr2_false ; ... }</pre>
Main program structure <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~

The toplevel of a smart contract file must be an un-delimited sequence of four primitive applications (in no particular order) that provide its <code>parameter</code>, <code>return</code> and <code>storage</code> types, as well as its <code>code</code>.

See the next section for a concrete example.

Comments ~<sub><sub><sub>~</sub></sub></sub>

A hash sign (<code>#</code>) anywhere outside of a string literal will make the rest of the line (and itself) completely ignored, as in the following example.

::

<pre>{ PUSH nat 1 ; # pushes 1
  PUSH nat 2 ; # pushes 2
  ADD }        # computes 2 + 1</pre>
Comments that span on multiple lines or that stop before the end of the line can also be written, using C-like delimiters (<code>/* ... */</code>).

== X - JSON syntax ==

Micheline expressions are encoded in JSON like this:

* An integer <code>N</code> is an object with a single field <code>&quot;int&quot;</code> whose valus is the decimal representation as a string.

<code>{ &quot;int&quot;: &quot;N&quot; }</code>

* A string <code>&quot;contents&quot;</code> is an object with a single field <code>&quot;string&quot;</code> whose valus is the decimal representation as a string.

<code>{ &quot;string&quot;: &quot;contents&quot; }</code>

* A sequence is a JSON array.

<code>[ expr, ... ]</code>

* A primitive application is an object with two fields <code>&quot;prim&quot;</code> for the primitive name and <code>&quot;args&quot;</code> for the arguments (that must contain an array). A third optionnal field <code>&quot;annot&quot;</code> may contains an annotation, including the <code>@</code> sign.

{ “prim”: “pair”, “args”: [ { “prim”: “nat”, args: [] }, { “prim”: “nat”, args: [] } ], “annot”: “@numbers” }`

As in the concrete syntax, all domain specific constants are encoded as strings.

== XI - 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 type <code>lambda (pair ’arg ’global) -&gt; (pair ’ret ’global)</code> where <code>’global</code> is the type of the original global store given on origination. The contract also takes a parameter and returns a value, hence the complete calling convention above.

Empty contract <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~

Any contract with the same <code>parameter</code> and <code>return</code> types may be written with an empty sequence in its <code>code</code> section. The simplest contract is the contract for which the <code>parameter</code>, <code>storage</code>, and <code>return</code> are all of type <code>unit</code>. This contract is as follows:

::

<pre>code {};
storage unit;
parameter unit;
return unit;</pre>
Reservoir contract <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~

We want to create a contract that stores tez until a timestamp <code>T</code> or a maximum amount <code>N</code> is reached. Whenever <code>N</code> is reached before <code>T</code>, all tokens are reversed to an account <code>B</code> (and the contract is automatically deleted). Any call to the contract’s code performed after <code>T</code> will otherwise transfer the tokens to another account <code>A</code>.

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 <code>(Pair (Pair T N) (Pair A B))</code>.

Hence, the global data of the contract has the following type

::

<pre>'g =
  pair
    (pair timestamp tez)
    (pair (contract unit unit) (contract unit unit))</pre>
Following the contract calling convention, the code is a lambda of type

::

<pre>lambda
  (pair unit 'g)
  (pair unit 'g)</pre>
written as

::

<pre>lambda
  (pair
     unit
     (pair
       (pair timestamp tez)
       (pair (contract unit unit) (contract unit unit))))
  (pair
     unit
     (pair
        (pair timestamp tez)
        (pair (contract unit unit) (contract unit unit))))</pre>
The complete source <code>reservoir.tz</code> is:

::

<pre>parameter timestamp ;
storage
  (pair
     (pair timestamp tez) # T N
     (pair (contract unit unit) (contract unit unit))) ; # A B
return unit ;
code
  { DUP ; CDAAR ; # T
    NOW ;
    COMPARE ; LE ;
    IF { DUP ; CDADR ; # N
         BALANCE ;
         COMPARE ; LE ;
         IF { CDR ; UNIT ; PAIR }
            { DUP ; CDDDR ; # B
              BALANCE ; UNIT ;
              DIIIP { CDR } ;
              TRANSFER_TOKENS ;
              PAIR } }
       { DUP ; CDDAR ; # A
         BALANCE ;
         UNIT ;
         DIIIP { CDR } ;
         TRANSFER_TOKENS ;
         PAIR } }</pre>
Reservoir contract (variant with broker and status) <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>

We basically want the same contract as the previous one, but instead of destroying it, we want to keep it alive, storing a flag <code>S</code> so that we can tell afterwards if the tokens have been transferred to <code>A</code> or <code>B</code>. We also want a broker <code>X</code> to get some fee <code>P</code> in any case.

We thus add variables <code>P</code> and <code>S</code> and <code>X</code> to the global data of the contract, now <code>(Pair (S, Pair (T, Pair (Pair P N) (Pair X (Pair A B)))))</code>. <code>P</code> is the fee for broker <code>A</code>, <code>S</code> is the state, as a string <code>&quot;open&quot;</code>, <code>&quot;timeout&quot;</code> or <code>&quot;success&quot;</code>.

At the beginning of the transaction:

::

<pre> S is accessible via a CDAR
 T               via a CDDAR
 P               via a CDDDAAR
 N               via a CDDDADR
 X               via a CDDDDAR
 A               via a CDDDDDAR
 B               via a CDDDDDDR</pre>
For the contract to stay alive, we test that all least <code>(Tez &quot;1.00&quot;)</code> is still available after each transaction. This value is given as an example and must be updated according to the actual Tezos minimal value for contract balance.

The complete source <code>scrutable_reservoir.tz</code> is:

::

<pre>parameter timestamp ;
storage
  (pair
     string # S
     (pair
        timestamp # T
        (pair
           (pair tez tez) ; # P N
           (pair
              (contract unit unit) # X
              (pair (contract unit unit) (contract unit unit)))))) ; # A B
return unit ;
code
  { DUP ; CDAR # S
    PUSH string &quot;open&quot; ;
    COMPARE ; NEQ ;
    IF { FAIL } # on &quot;success&quot;, &quot;timeout&quot; 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 &quot;1.00&quot; ;
              DIP { DUP ; CDDDAAR } ; ADD ; # P
              DIP { DUP ; CDDDADR } ; ADD ; # N
              # We compare to the cumulated amount
              BALANCE ;
              COMPARE; LT ;
              IF { # Not enough cash, we just accept the transaction
                   # and leave the global untouched
                   CDR }
                 { # Enough cash, successful ending
                   # We update the global
                   CDDR ; PUSH string &quot;success&quot; ; PAIR ;
                   # We transfer the fee to the broker
                   DUP ; CDDAAR ; # P
                   DIP { DUP ; CDDDAR } # X
                   UNIT ; TRANSFER_TOKENS ; DROP ;
                   # We transfer the rest to A
                   DUP ; CDDADR ; # N
                   DIP { DUP ; CDDDDAR } # A
                   UNIT ; TRANSFER_TOKENS ; DROP } }
            { # After timeout, we refund
              # We update the global
              CDDR ; PUSH string &quot;timeout&quot; ; PAIR ;
              # We try to transfer the fee to the broker
              PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
              DIP { DUP ; CDDAAR } ; # P
              COMPARE ; LT ; # available &lt; P
              IF { PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
                   DIP { DUP ; CDDDAR } # X
                   UNIT ; TRANSFER_TOKENS ; DROP }
                 { DUP ; CDDAAR ; # P
                   DIP { DUP ; CDDDAR } # X
                   UNIT ; TRANSFER_TOKENS ; DROP }
              # We transfer the rest to B
              PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
              DIP { DUP ; CDDDDDR } # B
              UNIT ; TRANSFER_TOKENS ; DROP } }
    # return Unit
    UNIT ; PAIR }</pre>
Forward contract ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>

We want to write a forward contract on dried peas. The contract takes as global data the tons of peas <code>Q</code>, the expected delivery date <code>T</code>, the contract agreement date <code>Z</code>, a strike <code>K</code>, a collateral <code>C</code> per ton of dried peas, and the accounts of the buyer <code>B</code>, the seller <code>S</code> and the warehouse <code>W</code>.

These parameters as grouped in the global storage as follows:

::

<pre>Pair
  (Pair (Pair Q (Pair T Z)))
  (Pair
     (Pair K C)
     (Pair (Pair B S) W))</pre>
of type

::

<pre>pair
  (pair nat (pair timestamp timestamp))
  (pair
     (pair tez tez)
     (pair (pair account account) account))</pre>
The 24 hours after timestamp <code>Z</code> are for the buyer and seller to store their collateral <code>(Q * C)</code>. For this, the contract takes a string as parameter, matching <code>&quot;buyer&quot;</code> or <code>&quot;seller&quot;</code> indicating the party for which the tokens are transferred. 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 <code>(pair tez tez)</code> where the left component is the buyer and the right one the seller.

After the first day, nothing cam happen until <code>T</code>.

During the 24 hours after <code>T</code>, the buyer must pay <code>(Q * K)</code> 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 <code>Q</code> tons of dried peas to the warehouse, in the next 24 hours. When the amount is equal to or exceeds <code>Q</code>, all the tokens are transferred to the seller and the contract is destroyed. For storing the quantity of peas already delivered, we add a counter of type <code>nat</code> 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.

::

<pre>Pair
  (Pair 0 (Pair 0_00 0_00))
  (Pair
     (Pair (Pair Q (Pair T Z)))
     (Pair
        (Pair K C)
        (Pair (Pair B S) W)))</pre>
of type

::

<pre>pair
  (pair nat (pair tez tez))
  (pair
     (pair nat (pair timestamp timestamp))
     (pair
        (pair tez tez)
        (pair (pair account account) account)))</pre>
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 <code>(or string nat)</code>.

At the beginning of the transaction:

::

<pre>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 seller via a CDADDR
the argument via a CAR</pre>
The contract returns a unit value, and we assume that it is created with the minimum amount, set to <code>(Tez &quot;1.00&quot;)</code>.

The complete source <code>forward.tz</code> is:

::

<pre>parameter (or string nat) ;
return unit ;
storage
  (pair
     (pair nat (pair tez tez)) # counter from_buyer from_seller
     (pair
        (pair nat (pair timestamp timestamp)) # Q T Z
        (pair
           (pair tez tez) # K C
           (pair
              (pair (contract unit unit) (contract unit unit)) # B S
              (contract unit unit))))) ; # W
code
  { DUP ; CDDADDR ; # Z
    PUSH nat 86400 ; SWAP ; ADD ; # one day in second
    NOW ; COMPARE ; LT ;
    IF { # Before Z + 24
         DUP ; CAR ; # we must receive (Left &quot;buyer&quot;) or (Left &quot;seller&quot;)
         IF_LEFT
           { DUP ; PUSH string &quot;buyer&quot; ; COMPARE ; EQ ;
             IF { DROP ;
                  DUP ; CDADAR ; # amount already versed by the buyer
                  DIP { AMOUNT } ; ADD ; # transaction
                  #  then we rebuild the globals
                  DIP { DUP ; CDADDR } ; PAIR ; # seller amount
                  PUSH nat 0 ; PAIR ; # delivery counter at 0
                  DIP { CDDR } ; PAIR ; # parameters
                  # and return Unit
                  UNIT ; PAIR }
                { PUSH string &quot;seller&quot; ; COMPARE ; EQ ;
                  IF { DUP ; CDADDR ; # amount already versed by the seller
                       DIP { AMOUNT } ; ADD ; # transaction
                       #  then we rebuild the globals
                       DIP { DUP ; CDADAR } ; SWAP ; PAIR ; # buyer amount
                       PUSH nat 0 ; PAIR ; # delivery counter at 0
                       DIP { CDDR } ; PAIR ; # parameters
                       # and return Unit
                       UNIT ; PAIR }
                     { FAIL } } } # (Left _)
           { FAIL } } # (Right _)
       { # After Z + 24
         # test if the required amount is reached
         DUP ; CDDAAR ; # Q
         DIP { DUP ; CDDDADR } ; MUL ; # C
         PUSH nat 2 ; MUL ;
         PUSH tez &quot;1.00&quot; ; ADD ;
         BALANCE ; COMPARE ; LT ; # balance &lt; 2 * (Q * C) + 1
         IF { # refund the parties
              CDR ; DUP ; CADAR ; # amount versed by the buyer
              DIP { DUP ; CDDDAAR } # B
              UNIT ; TRANSFER_TOKENS ; DROP
              DUP ; CADDR ; # amount versed by the seller
              DIP { DUP ; CDDDADR } # S
              UNIT ; TRANSFER_TOKENS ; DROP
              BALANCE ; # bonus to the warehouse to destroy the account
              DIP { DUP ; CDDDDR } # W
              UNIT ; TRANSFER_TOKENS ; DROP
              # return unit, don't change the global
              # since the contract will be destroyed
              UNIT ; PAIR }
            { # otherwise continue
              DUP ; CDDADAR # T
              NOW ; COMPARE ; LT
              IF { FAIL } # Between Z + 24 and T
                 { # after T
                   DUP ; CDDADAR # T
                   PUSH nat 86400 ; ADD # one day in second
                   NOW ; COMPARE ; LT
                   IF { # Between T and T + 24
                        # we only accept transactions from the buyer
                        DUP ; CAR ; # we must receive (Left &quot;buyer&quot;)
                        IF_LEFT
                          { PUSH string &quot;buyer&quot; ; COMPARE ; EQ ;
                            IF { DUP ; CDADAR ; # amount already versed by the buyer
                                 DIP { AMOUNT } ; ADD ; # transaction
                                 # The amount must not exceed Q * K
                                 DUP ;
                                 DIIP { DUP ; CDDAAR ; # Q
                                        DIP { DUP ; CDDDAAR } ; MUL ; } ; # K
                                 DIP { COMPARE ; GT ; # new amount &gt; Q * K
                                       IF { FAIL } { } } ; # abort or continue
                                 #  then we rebuild the globals
                                 DIP { DUP ; CDADDR } ; PAIR ; # seller amount
                                 PUSH nat 0 ; PAIR ; # delivery counter at 0
                                 DIP { CDDR } ; PAIR ; # parameters
                                 # and return Unit
                                 UNIT ; PAIR }
                               { FAIL } } # (Left _)
                          { FAIL } } # (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
                             DIIP { CDR } ;
                             UNIT ; TRANSFER_TOKENS ; DROP ;
                             # and return Unit
                             UNIT ; PAIR }
                           { # otherwise continue
                             DUP ; CDDADAR # T
                             PUSH nat 86400 ; ADD ;
                             PUSH nat 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 unit unit ; MANAGER ;
                                  COMPARE ; NEQ ;
                                  IF { FAIL } {} # fail if not the warehouse
                                  DUP ; CAR ; # we must receive (Right amount)
                                  IF_LEFT
                                    { FAIL } # (Left _)
                                    { # We increment the counter
                                      DIP { DUP ; CDAAR } ; ADD ;
                                      # And rebuild the globals in advance
                                      DIP { DUP ; CDADR } ; PAIR ;
                                      DIP { CDDR } ; PAIR ;
                                      UNIT ; PAIR ;
                                      # We test if enough have been delivered
                                      DUP ; CDAAR ;
                                      DIP { DUP ; CDDAAR } ;
                                      COMPARE ; LT ; # counter &lt; Q
                                      IF { CDR } # wait for more
                                         { # Transfer all the money to the seller
                                           BALANCE ; # and destroy the contract
                                           DIP { DUP ; CDDDDADR } # S
                                           DIIP { CDR } ;
                                           UNIT ; TRANSFER_TOKENS ; DROP } } ;
                                  UNIT ; PAIR }
                                { # after T + 48, transfer everything to the buyer
                                  BALANCE ; # and destroy the contract
                                  DIP { DUP ; CDDDDAAR } # B
                                  DIIP { CDR } ;
                                  UNIT ; TRANSFER_TOKENS ; DROP ;
                                  # and return unit
                                  UNIT ; PAIR } } } } } } }</pre>
== XII - Full grammar ==

::

<pre>&lt;data&gt; ::=
  | &lt;int constant&gt;
  | &lt;natural number constant&gt;
  | &lt;string constant&gt;
  | &lt;timestamp string constant&gt;
  | &lt;signature string constant&gt;
  | &lt;key string constant&gt;
  | &lt;key_hash string constant&gt;
  | &lt;tez string constant&gt;
  | &lt;contract string constant&gt;
  | Unit
  | True
  | False
  | Pair &lt;data&gt; &lt;data&gt;
  | Left &lt;data&gt;
  | Right &lt;data&gt;
  | Some &lt;data&gt;
  | None
  | { &lt;data&gt; ; ... }
  | { Elt &lt;data&gt; &lt;data&gt; ; ... }
  | instruction
&lt;instruction&gt; ::=
  | { &lt;instruction&gt; ... }
  | DROP
  | DUP
  | SWAP
  | PUSH &lt;type&gt; &lt;data&gt;
  | SOME
  | NONE &lt;type&gt;
  | UNIT
  | IF_NONE { &lt;instruction&gt; ... } { &lt;instruction&gt; ... }
  | PAIR
  | CAR
  | CDR
  | LEFT &lt;type&gt;
  | RIGHT &lt;type&gt;
  | IF_LEFT { &lt;instruction&gt; ... } { &lt;instruction&gt; ... }
  | NIL &lt;type&gt;
  | CONS
  | IF_CONS { &lt;instruction&gt; ... } { &lt;instruction&gt; ... }
  | EMPTY_SET &lt;type&gt;
  | EMPTY_MAP &lt;comparable type&gt; &lt;type&gt;
  | MAP
  | MAP { &lt;instruction&gt; ... }
  | REDUCE
  | ITER { &lt;instruction&gt; ... }
  | MEM
  | GET
  | UPDATE
  | IF { &lt;instruction&gt; ... } { &lt;instruction&gt; ... }
  | LOOP { &lt;instruction&gt; ... }
  | LOOP_LEFT { &lt;instruction&gt; ... }
  | LAMBDA &lt;type&gt; &lt;type&gt; { &lt;instruction&gt; ... }
  | EXEC
  | DIP { &lt;instruction&gt; ... }
  | FAIL
  | CONCAT
  | ADD
  | SUB
  | MUL
  | DIV
  | ABS
  | NEG
  | MOD
  | LSL
  | LSR
  | OR
  | AND
  | XOR
  | NOT
  | COMPARE
  | EQ
  | NEQ
  | LT
  | GT
  | LE
  | GE
  | INT
  | MANAGER
  | SELF
  | TRANSFER_TOKENS
  | CREATE_ACCOUNT
  | CREATE_CONTRACT
  | DEFAULT_ACCOUNT
  | NOW
  | AMOUNT
  | BALANCE
  | CHECK_SIGNATURE
  | H
  | HASH_KEY
  | STEPS_TO_QUOTA
  | SOURCE &lt;type&gt; &lt;type&gt;
&lt;type&gt; ::=
  | &lt;comparable type&gt;
  | key
  | unit
  | signature
  | option &lt;type&gt;
  | list &lt;type&gt;
  | set &lt;comparable type&gt;
  | contract &lt;type&gt; &lt;type&gt;
  | pair &lt;type&gt; &lt;type&gt;
  | or &lt;type&gt; &lt;type&gt;
  | lambda &lt;type&gt; &lt;type&gt;
  | map &lt;comparable type&gt; &lt;type&gt;
  | big_map &lt;comparable type&gt; &lt;type&gt;
&lt;comparable type&gt; ::=
  | int
  | nat
  | string
  | tez
  | bool
  | key_hash
  | timestamp</pre>
== XIII - 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: <code>String</code>, <code>Int</code>, <code>Seq</code> and <code>Prim</code>. 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 input and output of the program, of lambdas and of uninitialized maps and sets). 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 <code>Prim (&quot;If&quot;, ...)</code> into an <code>If</code>, a <code>Prim (&quot;Dup&quot;, ...)</code> into a <code>Dup</code>, etc.
@@ 1行目: / 1行目: @@
-=マイケルソン：Tezosのスマート契約の言語=
+= Michelson: the language of Smart Contracts in Tezos =
-言語はスタックベースで、高レベルのデータ型とプリミティブと厳格な静的型チェックがあります。そのデザインチェリーは、いくつかの言語科の特徴を選んでいます。注意深い読者は、Forth、Scheme、ML、Catへの直接参照に気付くでしょう。
+The language is stack based, with high level data types and primitives and strict static type checking. Its design cherry picks traits from several language families. Vigilant readers will notice direct references to Forth, Scheme, ML and Cat.
-マイケルソンプログラムは、順番に実行される一連の命令です。各命令は、前の命令の結果のスタックを入力として受け取り、次の命令のために書き換えます。スタックには、即値とヒープ割り当て構造の両方が含まれます。すべての値は不変で、ガーベジコレクションされます。
+A Michelson program is a series of instructions that are run in sequence: each instruction receives as input the stack resulting of the previous instruction, and rewrites it for the next one. The stack contains both immediate values and heap allocated structures. All values are immutable and garbage collected.
-マイケルソンプログラムは、入力値と記憶空間の内容とを含む単一の要素スタックを入力として受け取る。出力値と格納領域の新しい内容を含む単一の要素スタックを返す必要があります。あるいは、マイケルソンプログラムは、特定のオペコードを明示的に使用して失敗したり、タイプシステムによって捕らえられなかった何かが間違ってしまったりすることがあります（ゼロ、ガス枯渇など）。
+A Michelson program receives as input a single element stack containing an input value and the contents of a storage space. It must return a single element stack containing an output value and the new contents of the storage space. Alternatively, a Michelson program can fail, explicitly using a specific opcode, or because something went wrong that could not be caught by the type system (e.g.?division by zero, gas exhaustion).
-入力、出力、および記憶のタイプは固定であり、単相性であり、プログラムはシステムに導入される前にタイプチェックされる。予期しない長さや内容のスタック上で命令が実行されたため、スマートコントラクトの実行に失敗することはありません。
+The types of the input, output and storage are fixed and monomorphic, and the program is typechecked before being introduced into the system. No smart contract execution can fail because an instruction has been executed on a stack of unexpected length or contents.
-この仕様は、言語の完全な命令セット、タイプシステム、およびセマンティクスを示す。簡単な紹介ではなく、正確なリファレンスマニュアルを意味します。しかし、いくつかの例は文書の終わりに提供され、最初に、または仕様書と同時に読むことができます。
+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 - セマンティクス
+* I - Semantics
-* II - タイプシステム
+* II - Type system
-* III - コアデータ型
+* III - Core data types
-* IV - コア命令
+* IV - Core instructions
-* V - 操作
+* V - Operations
-* VI - ドメイン固有のデータ型
+* VI - Domain specific data types
-* VII - ドメイン固有の操作
+* VII - Domain specific operations
-* VIII - マクロ
+* VIII - Macros
-* IX - 具体的な構文
+* IX - Concrete syntax
-* X - JSON構文
+* X - JSON syntax
-* XI - 例
+* XI - Examples
-* XII - 完全な文法
+* XII - Full grammar
-* XIII - リファレンス実装
+* XIII - Reference implementation
-== I - セマンティクス==
+== I - Semantics ==
-この仕様は、マイケルソン語の詳細な形式的意味論を提供する。与えられたプログラムと初期スタックでマイケルソンインタプリタによって実行された計算をシンボリックな方法で説明し、対応する結果スタックを生成する。 Michelsonインタプリタは、純粋な関数です。環境に影響を与えることなく、最初の要素から結果スタックを作成するだけです。このセマンティクスは、大きなステップフォームと呼ばれるもので自然に与えられます。これは、再帰的参照インタープリタのシンボリックな定義です。この定義は、インタプリタ（プログラムおよびスタック）のすべての可能な入力をカバーする規則のリストの形をとり、対応する結果のスタックの計算を記述する。
+This specification gives a detailed formal semantics of the Michelson language. It explains in a symbolic way the computation performed by the Michelson interpreter on a given program and initial stack to produce the corresponding resulting stack. The Michelson interpreter is a pure function: it only builds a result stack from the elements of an initial one, without affecting its environment. This semantics is then naturally given in what is called a big step form: a symbolic definition of a recursive reference interpreter. This definition takes the form of a list of rules that cover all the possible inputs of the interpreter (program and stack), and describe the computation of the corresponding resulting stacks.
-ルールの形式と選択<sub> <sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> / sub> </sub> </sub> </sub>
+Rules form and selection <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>
-ルールには、主に次のような形式があります。
+The rules have the main following form.
 ::
-<pre>＆gt; （構文パターン）/（初期スタックパターン）=＆gt; （結果スタックパターン）
+<pre>&gt; (syntax pattern) / (initial stack pattern)  =&gt;  (result stack pattern)
-     iff（条件）
+     iff (conditions)
-     ここで（再帰）
+     where (recursions)
-と（より多くの再帰）</pre>
+and (more recursions)</pre>
-<code> =＆gt; </code>記号の左側がルールの選択に使用されます。プログラムと最初のスタックが与えられた場合、次のプロセスを使用して1つのルールのみを選択できます。まず、プログラムの最上位構造が構文パターンと一致していなければなりません。これは、命令シーケンスを処理するためのほんの些細なパターンが少なくて済むので、非常に単純であり、残りは、特定の1つの命令に一致する簡単なパターンから成り立っています。その後、最初のスタックは最初のスタックパターンと一致しなければなりません。最後に、<code> iff </code>キーワードに続くスタックの値に余分な条件を追加するルールもあります。時には、いくつかのルールが特定のコンテキストで適用されることがあります。この場合、この仕様の最初に現れるものが選択されます。ルールが適用されない場合、結果は明示的な<code> FAIL </code>命令の結果と同等です。この場合は、次のセクションで説明するように、型付きのプログラムでは発生しません。
+The left hand side of the <code>=&gt;</code> sign is used for selecting the rule. Given a program and an initial stack, one (and only one) rule can be selected using the following process. First, the toplevel structure of the program must match the syntax pattern. This is quite simple since there is only a few non trivial patterns to deal with instruction sequences, and the rest is made of trivial pattern that match one specific instruction. Then, the initial stack must match the initial stack pattern. Finally, some rules add extra conditions over the values in the stack that follow the <code>iff</code> keyword. Sometimes, several rules may apply in a given context. In this case, the one that appears first in this specification is to be selected. If no rule applies, the result is equivalent to the one for the explicit <code>FAIL</code> instruction. This case does not happen on well-typed programs, as explained in the next section.
-右側には、ルールが適用される場合のインタープリタの結果が記述されています。スタックパターンは、<code> =＆gt; </code>記号の左側に名前が付けられた定数（定数）とコンテキストの要素（プログラムと初期スタック）のいずれかです。
-再帰的規則（大きなステップ形式）<sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> sub>?</sub> </sub> </sub> </sub> </sub> </sub> > </sub> </sub> </sub>
+The right hand side describes the result of the interpreter if the rule applies. It consists in a stack pattern, whose part are either constants, or elements of the context (program and initial stack) that have been named on the left hand side of the <code>=&gt;</code> sign.
-場合によっては、プログラムを解釈した結果が、別のプログラムを解釈した結果（条件呼び出しや関数呼び出しのように）から得られることもあります。このような場合、ルールには次の形式の句が含まれます。
+Recursive rules (big step form) <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>
+Sometimes, the result of interpreting a program is derived from the result of interpreting another one (as in conditionals or function calls). In these cases, the rule contains a clause of the following form.
 ::
-<pre>ここで（中間プログラム）/（中間スタック）=＆gt; （部分的な結果）</pre>
+<pre>where (intermediate program) / (intermediate stack)  =&gt;  (partial result)</pre>
-これは、左の中間状態を解釈する場合にこのルールが適用されることを意味し、右のパターンを与える。
+This means that this rules applies in case interpreting the intermediate state on the left gives the pattern on the right.
-<code> =＆gt; </code>記号の左側の記号は、初期状態の要素または他の部分的な結果から構成され、右側はルールの結果スタックを構築するために使用できる部分を示します。
+The left hand sign of the <code>=&gt;</code> sign is constructed from elements of the initial state or other partial results, and the right hand side identify parts that can be used to build the result stack of the rule.
-部分的な結果パターンが解釈の結果と実際には一致しない場合、ルール全体の結果は明示的な<code> FAIL </code>命令の結果と同等です。この場合も、次のセクションで説明するように、型付きのプログラムでは発生しません。
+If the partial result pattern does not actually match the result of the interpretation, then the result of the whole rule is equivalent to the one for the explicit <code>FAIL</code> instruction. Again, this case does not happen on well-typed programs, as explained in the next section.
-パターンの形式<sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
+Format of patterns <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-コードパターンは、次の構文形式のいずれかです。
+Code patterns are of one of the following syntactical forms.
-* <code> INSTR </code>（大文字の識別子）は単純な命令です（例：<code> DROP </code>）。
+* <code>INSTR</code> (an uppercase identifier) is a simple instruction (e.g. <code>DROP</code>);
-* <code> INSTR（arg）... </code>は複合命令で、その引数はコード、データ、または型パターン（例：<code> PUSH nat 3 </code>）です。
+* <code>INSTR (arg) ...</code> is a compound instruction, whose arguments can be code, data or type patterns (e.g. <code>PUSH nat 3</code>) ;
-* <code> {（instr）; （例えば<code> IF {SWAP; DROP} {DROP} </code>）、ネストされたシーケンスは中カッコを削除することができます。
+* <code>{ (instr) ; ... }</code> is a possibly empty sequence of instructions, (e.g. <code>IF { SWAP ; DROP } { DROP }</code>), nested sequences can drop the braces ;
-* <code> name </code>は、任意のプログラムと一致し、結果を構築するために使用できる一致したプログラムの一部を指定するパターンです。
+* <code>name</code> is a pattern that matches any program and names a part of the matched program that can be used to build the result ;
-* <code> _ </code>は、どの命令にも一致するパターンです。
+* <code>_</code> is a pattern that matches any instruction.
-スタックパターンは、次の構文形式のいずれかです。
+Stack patterns are of one of the following syntactical forms.
-* <code> [FAIL] </code>は特別な失敗状態です。
+* <code>[FAIL]</code> is the special failed state ;
-* <code> [] </code>は空のスタックです。
+* <code>[]</code> is the empty stack ;
-* <code>（top）：（rest）</code>は、左上のデータパターン<code>（top）</code>によって一番上の要素がマッチし、残りの要素がスタックによってマッチしたスタックです右側の<code>（rest）</code>パターン（<code> x：y：rest </code>など）。
+* <code>(top) : (rest)</code> is a stack whose top element is matched by the data pattern <code>(top)</code> on the left, and whose remaining elements are matched by the stack pattern <code>(rest)</code> on the right (e.g. <code>x : y : rest</code>) ;
-* <code> name </code>は、任意のスタックにマッチし、結果をビルドするためにスタックに名前を付けるパターンです。
+* <code>name</code> is a pattern that matches any stack and names it in order to use it to build the result ;
-* <code> _ </code>は、どのスタックにも一致するパターンです。
+* <code>_</code> is a pattern that matches any stack.
-データパターンは、次の構文形式のいずれかです。
+Data patterns are of one of the following syntactical forms.
-*整数/自然数リテラル（例：<code> 3 </code>）;
+* integer/natural number literals, (e.g. <code>3</code>) ;
-*文字列リテラル（例：<code> "contents" </code>）;
+* string literals, (e.g. <code>&quot;contents&quot;</code>) ;
-* <code>タグ</code>、<code> False </code>）; <code>タグ</code>は大文字の定数です（例：<code> Unit </code>
+* <code>Tag</code> (capitalized) is a symbolic constant, (e.g. <code>Unit</code>, <code>True</code>, <code>False</code>) ;
-* <code>（Tag（arg）...）</code>タグ付き構築データ（例：<code>（Pair 3 4）</code>）;
+* <code>(Tag (arg) ...)</code> tagged constructed data, (e.g. <code>(Pair 3 4)</code>) ;
-*第1クラスのコード値のコードパターン。
+* a code pattern for first class code values ;
-* <code> name </code>を使用して値を命名し、結果を構築します。
+* <code>name</code> to name a value in order to use it to build the result ;
-* <code> _ </code>を使用して任意の値に一致させることができます。
+* <code>_</code> to match any value.
-命令名、記号定数、およびデータコンストラクタの領域は、この仕様で修正されています。マイケルソンは、プログラマが独自の型を導入することはできません。
+The domain of instruction names, symbolic constants and data constructors is fixed by this specification. Michelson does not let the programmer introduce its own types.
-仕様で使用されている構文は、第IX節で示されている具体的な構文と少し異なる場合があることに注意してください。特に、いくつかの命令には、タイプチェッカーによって合成されるため、具体的な言語には存在しないタイプの注釈が付けられます。
+Be aware that the syntax used in the specification may differ a bit from the concrete syntax, which is presented in Section IX. In particular, some instructions are annotated with types that are not present in the concrete language because they are synthesized by the typechecker.
-ショートカット<sub>?<sub>?</sub> </sub>?
+Shortcuts <sub>~<sub>~</sub></sub>~
-時には、大きなステップのセマンティクスよりもプログラム書き換えの観点から考えるのが簡単です（書き込む方が簡単です）。それが当てはまり、両方が等価である場合は、次の形式のルールを記述します。
+Sometimes, it is easier to think (and shorter to write) in terms of program rewriting than in terms of big step semantics. When it is the case, and when both are equivalents, we write rules of the form:
 ::
-<pre> p / S =＆gt; S ''
+<pre>p / S  =&gt;  S''
-ここで、p '/ S' =＆gt; S '' </pre>
+where   p' / S'  =&gt;  S''</pre>
-次のショートカットを使用します。
+using the following shortcut:
 ::
-<pre> p / S =＆gt; p '/ S' </pre>
+<pre>p / S  =&gt;  p' / S'</pre>
-具体的な言語には、いくつかの一般的な操作シーケンスを1つにまとめるシンタックス・シュガーがあります。これは、単純な正規表現スタイルの再帰的命令書き換えを使用して、この仕様書で説明されています。
+The concrete language also has some syntax sugar to group some common sequences of operations as one. This is described in this specification using a simple regular expression style recursive instruction rewriting.
-== II - 型システムと表記法の紹介==
+== II - Introduction to the type system and notations ==
-この仕様は、マイケルソンのタイプシステムについて説明します。特に正式なプログラミング言語仕様の読解に慣れていない読者にとっては、型チェックや推論のアルゴリズムを提供していません。それは、型付きの良いプログラムであると考えるものを意図的に定義するだけです。構文形式ごとに、型付きの良い入力と見なされるスタックとその結果の出力が記述されます。
+This specification describes a type system for Michelson. To make things clear, in particular to readers that are not accustomed to reading formal programming language specifications, it does not give a typechecking or inference algorithm. It only gives an intentional definition of what we consider to be well-typed programs. For each syntactical form, it describes the stacks that are considered well-typed inputs, and the resulting outputs.
-型システムは健全です。つまり、プログラムに型を与えることができれば、適切に型付けされた入力スタック上で実行すると、予期しない長さや内容のスタックに解釈規則を適用することはありません。また、実行を継続するための適切なルールを選択できない状態にはなりません。よくタイプされたプログラムはブロックされず、間違っていません。
+The type system is sound, meaning that if a program can be given a type, then if run on a well-typed input stack, the interpreter will never apply an interpretation rule on a stack of unexpected length or contents. Also, it will never reach a state where it cannot select an appropriate rule to continue the execution. Well-typed programs do not block, and do not go wrong.
-タイプ記法<sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub>?
+Type notations <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~
-この仕様では、値、用語、スタックの種類の表記を紹介しています。言語全体のいくつかの場所で型注釈の形式で表示される値型のサブセットを除いて、この型言語は仕様にのみ存在することを理解することが重要です。
+The specification introduces notations for the types of values, terms and stacks. Apart from a subset of value types that appear in the form of type annotations in some places throughout the language, it is important to understand that this type language only exists in the specification.
-スタックタイプを記述することができます：
+A stack type can be written:
-*空のスタックの[<code> [] </code>;
+* <code>[]</code> for the empty stack ;
-最初の値のタイプが<code>（top）</code>で、キューのスタックタイプが<code>（rest）</code>のスタックの* <code>（top）:( rest）</code>
+* <code>(top) : (rest)</code> for the stack whose first value has type <code>(top)</code> and queue has stack type <code>(rest)</code>.
-言語の命令、プログラムおよびプリミティブもタイプされ、そのタイプは以下のように書かれる：
+Instructions, programs and primitives of the language are also typed, their types are written:
 ::
-<pre>（前にスタックのタイプ） - ＆gt; （後のスタックの種類）</pre>
+<pre>(type of stack before) -&gt; (type of stack after)</pre>
-スタック内の値の型は次のようになります。
+The types of values in the stack are written:
-プリミティブデータ型（例：<code> bool </code>）の* <code>識別子</code>
+* <code>identifier</code> for a primitive data-type (e.g. <code>bool</code>),
-<code>（arg）</code>（<code> list nat </code>）などのパラメータタイプを持つパラメトリックデータ型の場合、<code> identifier（arg）</code>
+* <code>identifier (arg)</code> for a parametric data-type with one parameter type <code>(arg)</code> (e.g. <code>list nat</code>),
-いくつかのパラメータ（例：<code> map string int </code>）を持つパラメトリックデータ型の* <code> identifier（arg）... </code>
+* <code>identifier (arg) ...</code> for a parametric data-type with several parameters (e.g. <code>map string int</code>),
-* <code> [（前のスタックのタイプ） - ＆gt;コード引用（例：<code> [int：int：[] - > int：[]] </code>）の場合は、
+* <code>[ (type of stack before) -&gt; (type of stack after) ]</code> for a code quotation, (e.g. <code>[ int : int : [] -&gt; int : [] ]</code>),
-* <code> lambda（arg）（ret）</code>は、<code> [（arg）：[] - ＆gt; （ret）：[]] </code>。
+* <code>lambda (arg) (ret)</code> is a shortcut for <code>[ (arg) : [] -&gt; (ret) : [] ]</code>.
-メタタイプ変数<sub> <sub>?</sub> </sub>?</sub>?</sub>
+Meta type variables <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>
-型定義規則は、メタ型変数を導入する。明らかにするために、これはマイケルソンにはない多型性とは関係がありません。これらの変数は、仕様レベルでのみ存在し、プログラムの各部分間の一貫性を表現するために使用されます。たとえば、<code> IF </code>構文の型定義ルールは、両方のブランチが同じ型を持たなければならないことを表すメタ変数を導入します。
+The typing rules introduce meta type variables. To be clear, this has nothing to do with polymorphism, which Michelson does not have. These variables only live at the specification level, and are used to express the consistency between the parts of the program. For instance, the typing rule for the <code>IF</code> construct introduces meta variables to express that both branches must have the same type.
-メタタイプ変数の表記法は次のとおりです。
-*型変数の<code> '</code>
+Here are the notations for meta type variables:
-スタック型変数の場合は<code> '</code>
-* <code> _ </code>は、匿名型またはスタック型変数です。
-入力ルール<sub> <sub> <sub> <sub>?</sub> </sub> </sub>?</sub>
+* <code>'a</code> for a type variable,
+* <code>'A</code> for a stack type variable,
+* <code>_</code> for an anonymous type or stack type variable.
-システムはシンタックスディレクティブです。ここでは、シンタックスコンストラクトごとに1つのタイピングルールが定義されています。入力規則は、この構文構文に対して承認された入力スタックのタイプを制限し、出力タイプを入力タイプにリンクし、必要に応じてメタタイプ変数を使用してそれらの両方をサブ式にリンクします。
+Typing rules <sub><sub><sub><sub>~</sub></sub></sub>~</sub>
-入力規則の形式は次のとおりです。
+The system is syntax directed, which means here that it defines a single typing rule for each syntax construct. A typing rule restricts the type of input stacks that are authorized for this syntax construct, links the output type to the input type, and links both of them to the subexpressions when needed, using meta type variables.
+Typing rules are of the form:
 ::
-<pre>（構文パターン）
+<pre>(syntax pattern)
-::（前にスタックのタイプ） - ＆gt; （スタックの種類）[ルール名]
+:: (type of stack before) -&gt; (type of stack after) [rule-name]
-    iff（敷地内）</pre>
+    iff (premises)</pre>
-<code>（x）</code>という形式の<code>（type）</code>という形式は、コード>（タイプ）</code>
+Where premises are typing requirements over subprograms or values in the stack, both of the form <code>(x) :: (type)</code>, meaning that value <code>(x)</code> must have type <code>(type)</code>.
-プログラムはトップレベルプログラム式に適用されるルールのインスタンスを見つけることができ、すべてのメタタイプ変数が非変数タイプ式に置き換えられ、そのタイプのすべてのタイプ要件が十分に証明されている場合、同じ方法でタイプされます。正式型システムに精通していない読者にとっては、これを型定義派生と呼びます。
+A program is shown well-typed if one can find an instance of a rule that applies to the toplevel program expression, with all meta type variables replaced by non variable type expressions, and of which all type requirements in the premises can be proven well-typed in the same manner. For the reader unfamiliar with formal type systems, this is called building a typing derivation.
-<code>（x + 5）* 10 </code>を計算する小さなプログラム上での派生型の例を次に示します。<code> x </code> PUSH </code>、<code> ADD </code>、およびシーケンスについては、次のセクションを参照してください。インスタンス化する際、<code> iff </code>を<code> by </code>に置き換えます。
+Here is an example typing derivation on a small program that computes <code>(x+5)*10</code> for a given input <code>x</code>, obtained by instantiating the typing rules for instructions <code>PUSH</code>, <code>ADD</code> and for the sequence, as found in the next sections. When instantiating, we replace the <code>iff</code> with <code>by</code>.
 ::
-<pre> {プッシュナット5; ADD;プッシュナット10; SWAP; MUL}
+<pre>{ PUSH nat 5 ; ADD ; PUSH nat 10 ; SWAP ; MUL }
-:: [nat：[] - ＆gt; nat：[]]
+:: [ nat : [] -&gt; nat : [] ]
-    ?によって{PUSH nat 5;追加}
+    by { PUSH nat 5 ; ADD }
-       :: [nat：[] - ＆gt; nat：[]]
+       :: [ nat : [] -&gt; nat : [] ]
-          プッシュナット5
+          by PUSH nat 5
-             :: [nat：[] - ＆gt; nat：nat：[]]
+             :: [ nat : [] -&gt; nat : nat : [] ]
-:: nat
+                by 5 :: nat
-         ADD
+         and ADD
-             :: [nat：nat：[] - ＆gt; nat：[]]
+             :: [ nat : nat : [] -&gt; nat : [] ]
-   および{プッシュナット10; SWAP; MUL}
+   and { PUSH nat 10 ; SWAP ; MUL }
-       :: [nat：[] - ＆gt; nat：[]]
+       :: [ nat : [] -&gt; nat : [] ]
-          プッシュナット10
+          by PUSH nat 10
-             :: [nat：[] - ＆gt; nat：nat：[]]
+             :: [ nat : [] -&gt; nat : nat : [] ]
-:: natで
+                by 10 :: nat
-         と{SWAP; MUL}
+         and { SWAP ; MUL }
-             :: [nat：nat：[] - ＆gt; nat：[]]
+             :: [ nat : nat : [] -&gt; nat : [] ]
-                スワップ
+                by SWAP
-                   :: [nat：nat：[] - ＆gt; nat：nat：[]]
+                   :: [ nat : nat : [] -&gt; nat : nat : [] ]
-               とMUL
+               and MUL
-                   :: [nat：nat：[] - ＆gt; nat：[]] </pre>
+                   :: [ nat : nat : [] -&gt; nat : [] ]</pre>
-このようなタイピングの導出を生成することは、統一または抽象的解釈のような多くの方法で行うことができる。マイケルソンの実装では、プログラマが提供する入力タイプを表す抽象スタック上でプログラムの再帰的な記号評価を実行し、結果のシンボリックスタックがプログラマによって提供される期待された結果。
+Producing such a typing derivation can be done in a number of manners, such as unification or abstract interpretation. In the implementation of Michelson, this is done by performing a recursive symbolic evaluation of the program on an abstract stack representing the input type provided by the programmer, and checking that the resulting symbolic stack is consistent with the expected result, also provided by the programmer.
-注釈<sub> <sub>?</sub> </sub> </sub>?<sub>?</sub>
+Annotations <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>
-言語のほとんどの命令は、オプションでアノテーションを取ることができます。アノテーションを使用すると、データ、スタック、ペア、およびユニオン内のデータをより正確に追跡できます。
+Most instructions in the language can optionally take an annotation. Annotations allow you to better track data, on the stack and within pairs and unions.
-あるタイプのコンポーネントに追加された場合、注釈は型チェッカーのアクセス指示に従って型チェッカーによって伝播されます。
+If added on the components of a type, the annotation will be propagated by the typechecker througout access instructions.
-スタックに値を生成する命令に注釈を付けると、その型のトップレベルに注釈が書き換えられます。
+Annotating an instruction that produces a value on the stack will rewrite the annotation an the toplevel of its type.
-値を生成しない命令に注釈を付けると、型チェックエラーが発生します。
-プログラムの<code> IF </code>、<code> IF_LEFT </code>、<code> IF_CONS </code>、<code> IF_NONE </code>、<code> LOOP </code> >）、注釈は互換性がなければなりません。注釈は、両方の要素が同じ注釈で注釈付けされている場合、または値/型の少なくとも1つに注釈が付けられていない場合に互換性があります。
+Trying to annotate an instruction that does not produce a value will result in a typechecking error.
-プログラムの各タイプに関連付けられているマイケルソンのEmacsモードの印刷注釈のようなスタックビジュアライゼーションツールは、型チェッカーによって伝播されます。これはデバッグの助けとして役立ちます。
+At join points in the program (<code>IF</code>, <code>IF_LEFT</code>, <code>IF_CONS</code>, <code>IF_NONE</code>, <code>LOOP</code>), annotations must be compatible. Annotations are compatible if both elements are annotated with the same annotation or if at least one of the values/types is unannotated.
-サイドノート<sub>?<sub>?</sub> </sub>?
+Stack visualization tools like the Michelson’s Emacs mode print annotations associated with each type in the program, as propagated by the typechecker. This is useful as a debugging aid.
-ほとんどの型システムと同様、不完全です。この型のシステムに型を与えることができないプログラムがありますが、それが実行されると間違ってはいけません。これは、型システムを使用可能にするために必要な妥協点です。また、マイケルソンの実装では、タイプ・システムが記述するタイプのプログラムほど多くのプログラムを受け入れないことを覚えておくことが重要です。これは、実装が単純なシングルパス型検査アルゴリズムを使用しており、多態性の形式を処理しないためです。
+Side note <sub>~<sub>~</sub></sub>~
-== III - コアのデータ型と表記法==
+As with most type systems, it is incomplete. There are programs that cannot be given a type in this type system, yet that would not go wrong if executed. This is a necessary compromise to make the type system usable. Also, it is important to remember that the implementation of Michelson does not accept as many programs as the type system describes as well-typed. This is because the implementation uses a simple single pass typechecking algorithm, and does not handle any form of polymorphism.
-* <code> string </code>、<code> nat </code>、<code> int </code>：コアプリミティブ定数型。
+== III - Core data types and notations ==
-* <code> True </code>と<code> False </code>のブール値の型は、
-* <code> unit </code>：結果やパラメータが不要な場合にプレースホルダとして使用する<code> Unit </code>の型だけです。たとえば、契約の唯一の目的はストレージを更新することです。
-* <code>（t）</code>の要素を持ち、<code> {} </code>と書かれた単一で不変な同質のリンクリスト。 >空リストまたは<code> {first; ...} </code>。セマンティクスでは、シェブロンを使用して要素のサブシーケンスを示します。たとえば、<code> {head; ＆lt; tail＆gt; } </code>
-* <code>（l）</code>型の<code> a </code>と<code> b </code>のペアと、 <code>（r）</code>、<code>（Pair ab）</code>と書いてあります。
-* <code> None </code>または<code>（Some v）</code>に注意する<code>（t）</code> 。
-* <code>（l）</code>の値<code> a </code>を保持する値と、 <code>（左a）</code>または<code>（右b）</code>という<code>（r）</code>型の<code> b </code>
-* <code> set（t）</code>：<code>（t）</code>型の値の不変集合を<code> {item; ...} </code>、要素は一意でソートされています。
-* <code>（t）</code>型の値の<code>（k）</code>型のキーからの不変のマップは、コード> {Eltキー値; ...} </code>、キーはソートされています。
-* <code>（k）（t）</code>：<code>（k）</code>のタイプのキーから、 <code> {Elt key value; ...} </code>、キーはソートされています。大量のデータをマップに保存する場合は、これらのマップを使用する必要があります。データが遅延デシリアライズされるため、標準マップよりもガスコストが高くなります。プログラムごとに1つの<code> big_map </code>に限定されています。契約のストレージのペアの左側に表示する必要があります。
-== IV - コア命令==
+* <code>string</code>, <code>nat</code>, <code>int</code>: The core primitive constant types.
+* <code>bool</code>: The type for booleans whose values are <code>True</code> and <code>False</code>
+* <code>unit</code>: The type whose only value is <code>Unit</code>, to use as a placeholder when some result or parameter is non necessary. For instance, when the only goal of a contract is to update its storage.
+* <code>list (t)</code>: A single, immutable, homogeneous linked list, whose elements are of type <code>(t)</code>, and that we note <code>{}</code> for the empty list or <code>{ first ; ... }</code>. In the semantics, we use chevrons to denote a subsequence of elements. For instance <code>{ head ; &lt;tail&gt; }</code>.
+* <code>pair (l) (r)</code>: A pair of values <code>a</code> and <code>b</code> of types <code>(l)</code> and <code>(r)</code>, that we write <code>(Pair a b)</code>.
+* <code>option (t)</code>: Optional value of type <code>(t)</code> that we note <code>None</code> or <code>(Some v)</code>.
+* <code>or (l) (r)</code>: A union of two types: a value holding either a value <code>a</code> of type <code>(l)</code> or a value <code>b</code> of type <code>(r)</code>, that we write <code>(Left a)</code> or <code>(Right b)</code>.
+* <code>set (t)</code>: Immutable sets of values of type <code>(t)</code> that we note as lists <code>{ item ; ... }</code>, of course with their elements unique, and sorted.
+* <code>map (k) (t)</code>: Immutable maps from keys of type <code>(k)</code> of values of type <code>(t)</code> that we note <code>{ Elt key value ; ... }</code>, with keys sorted.
+* <code>big_map (k) (t)</code>: Lazily deserialized maps from keys of type <code>(k)</code> of values of type <code>(t)</code> that we note <code>{ Elt key value ; ... }</code>, with keys sorted. These maps should be used if you intend to store large amounts of data in a map. They have higher gas costs than standard maps as data is lazily deserialized. You are limited to a single <code>big_map</code> per program, which must appear on the left hand side of a pair in the contract's storage.
-制御構造<sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
+== IV - Core instructions ==
-* <code> FAIL </code>：現在のプログラムを明示的に中止します。
+Control structures <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-:: _ - ＆gt; _
+* <code>FAIL</code>: Explicitly abort the current program.
-この特別な命令は、入力スタック（以下の第1の規則）を使用せず、その後のすべての命令が通常のセマンティクスを単に無視してメインの結果まで障害を伝播するため、出力を無用にするので、以下）。したがってそのタイプは完全に汎用的です。
+:: _ -&gt; _
+This special instruction is callable in any context, since it does not use its input stack (first rule below), and makes the output useless since all subsequent instruction will simply ignore their usual semantics to propagate the failure up to the main result (second rule below). Its type is thus completely generic.
 ::
-<pre>＆gt; FAIL / _ =＆gt; [失敗します]
+<pre>&gt; FAIL / _  =&gt;  [FAIL]
-＆gt; _ / [FAIL] =＆gt; [FAIL] </pre>
+&gt; _ / [FAIL]  =&gt;  [FAIL]</pre>
-* <code> {I; C} </code>：シーケンス。
+* <code>{ I ; C }</code>: Sequence.
 ::
-<pre> :: 'A - ＆gt; 'C
-   I :: ['A - ＆gt; 'B]
-         C :: ['B - ＆gt; 'C]
-＆gt;私 ; C / SA =＆gt; SC
+<pre>:: 'A   -&gt;   'C
-     I / SA =＆gt; SB
+   iff   I :: [ 'A -&gt; 'B ]
-     C / SB =＆gt; SC </pre>
+         C :: [ 'B -&gt; 'C ]
-* <code> IF bt bf </code>：条件分岐。
+&gt; I ; C / SA  =&gt;  SC
+     where   I / SA  =&gt;  SB
+     and   C / SB  =&gt;  SC</pre>
+* <code>IF bt bf</code>: Conditional branching.
 ::
-<pre> :: bool： 'A - ＆gt; 'B
+<pre>:: bool : 'A   -&gt;   'B
-    iff bt :: ['A - ＆gt; 'B]
+    iff   bt :: [ 'A -&gt; 'B ]
-          bf :: ['A - ＆gt; 'B]
+          bf :: [ 'A -&gt; 'B ]
-＆gt; IF bt bf / True：S =＆gt; bt / S
+&gt; IF bt bf / True : S  =&gt;  bt / S
-＆gt; IF bt bf / False：S =＆gt; bf / S </pre>
+&gt; IF bt bf / False : S  =&gt;  bf / S</pre>
-* <code>ループ本体</code>：一般的なループ。
+* <code>LOOP body</code>: A generic loop.
 ::
-<pre> :: bool： 'A - ＆gt; 'A
+<pre>:: bool : 'A   -&gt;   'A
-    if body :: ['A - ＆gt;ブール： 'A'
+    iff   body :: [ 'A -&gt; bool : 'A ]
-＆gt; LOOP body / True：S =＆gt;体 ;ループボディ/ S
+&gt; LOOP body / True : S  =&gt;  body ; LOOP body / S
-＆gt; LOOP body / False：S =＆gt; S </pre>
+&gt; LOOP body / False : S  =&gt;  S</pre>
-* <code> LOOP_LEFT本体</code>：アキュムレータを持つループ
+* <code>LOOP_LEFT body</code>: A loop with an accumulator
 ::
-<pre> ::（または 'a' b）： 'A - ＆gt; 'A
+<pre>:: (or 'a 'b) : 'A   -&gt;   'A
-    if body :: ['a：' A - ＆gt; （または 'a' b）： 'A'
+    iff   body :: [ 'a : 'A -&gt; (or 'a 'b) : 'A ]
-＆gt; LOOP_LEFT本体/（左a）：S =＆gt;体 ; LOOP_LEFT本体/（または 'a' b）：S
+&gt; LOOP_LEFT body / (Left a)  : S  =&gt;  body ; LOOP_LEFT body / (or 'a 'b) : S
-＆gt; LOOP_LEFT本体/（右b）：S =＆gt; b：S </pre>
+&gt; LOOP_LEFT body / (Right b) : S  =&gt;  b : S</pre>
-* <code> DIP code </code>：スタックの先頭を保護するコードを実行します。
+* <code>DIP code</code>: Runs code protecting the top of the stack.
 ::
-<pre> :: 'b：' A - ＆gt; 'b：' C
+<pre>:: 'b : 'A   -&gt;   'b : 'C
-    iff code :: ['A - ＆gt; 'C]
+    iff   code :: [ 'A -&gt; 'C ]
-＆gt; DIPコード/ x：S =＆gt; x：S '
+&gt; DIP code / x : S  =&gt;  x : S'
-     ここでcode / S =＆gt; S '</pre>
+     where    code / S  =&gt;  S'</pre>
-* <code> EXEC </code>：スタックから関数を実行します。
+* <code>EXEC</code>: Execute a function from the stack.
 ::
-<pre> :: 'a：lambda' a 'b：' C - ＆gt; 'b：' C
+<pre>:: 'a : lambda 'a 'b : 'C   -&gt;   'b : 'C
-＆gt; EXEC / a：f：S =＆gt; r：S
+&gt; EXEC / a : f : S  =&gt;  r : S
-     ここで、f / a：[] =＆gt; r：[] </pre>
+     where f / a : []  =&gt;  r : []</pre>
-スタック操作?<sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub> / sub>
+Stack operations ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>
-* <code> DROP </code>：スタックの一番上の要素を削除します。
+* <code>DROP</code>: Drop the top element of the stack.
 ::
-<pre> :: _： 'A - ＆gt; 'A
+<pre>:: _ : 'A   -&gt;   'A
-＆gt; DROP / _：S =＆gt; S </pre>
+&gt; DROP / _ : S  =&gt;  S</pre>
-* <code> DUP </code>：スタックの上部を複製します。
+* <code>DUP</code>: Duplicate the top of the stack.
 ::
-<pre> :: 'a：' A - ＆gt; 'a：' a： 'A
+<pre>:: 'a : 'A   -&gt;   'a : 'a : 'A
-＆gt; DUP / x：S =＆gt; x：x：S </pre>
+&gt; DUP / x : S  =&gt;  x : x : S</pre>
-* <code> SWAP </code>：スタックの上位2つの要素を交換します。
+* <code>SWAP</code>: Exchange the top two elements of the stack.
 ::
-<pre> :: 'a：' b： 'A - ＆gt; 'b：' a： 'A
+<pre>:: 'a : 'b : 'A   -&gt;   'b : 'a : 'A
-＆gt; SWAP / x：y：S =＆gt; y：x：S </pre>
+&gt; SWAP / x : y : S  =&gt;  y : x : S</pre>
-* <code> PUSH 'a x </code>：与えられた型の定数値をスタックにプッシュします。
+* <code>PUSH 'a x</code>: Push a constant value of a given type onto the stack.
 ::
-<pre> :: 'A - ＆gt; 'a：' A
+<pre>:: 'A   -&gt;   'a : 'A
-    iff x :: 'a
+    iff   x :: 'a
-＆gt; PUSH 'a x / S =＆gt; x：S </pre>
+&gt; PUSH 'a x / S  =&gt;  x : S</pre>
-* <code> UNIT </code>：ユニットの値をスタックにプッシュします。
+* <code>UNIT</code>: Push a unit value onto the stack.
 ::
-<pre> :: 'A - ＆gt;ユニット： 'A
+<pre>:: 'A   -&gt;   unit : 'A
-＆gt; UNIT / S =＆gt;単位：S </pre>
+&gt; UNIT / S  =&gt;  Unit : S</pre>
-* <code> LAMBDA 'a' b code </code>：与えられたパラメータでラムダをプッシュし、型をスタックに返します。
+* <code>LAMBDA 'a 'b code</code>: Push a lambda with given parameter and return types onto the stack.
 ::
-<pre> :: 'A - ＆gt; （λ 'a' b）： 'A
+<pre>:: 'A -&gt;  (lambda 'a 'b) : 'A
-＆gt; LAMBDA _ _ code / S =＆gt;コード：S </pre>
+&gt; LAMBDA _ _ code / S  =&gt;  code : S</pre>
-一般的な比較<sub> <sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
+Generic comparison <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-比較は、私たちがcomparableと呼ぶ種類のクラスに対してのみ機能します。比較演算子は、比較可能な型ごとに特別な方法で定義されますが、compareの結果は常に<code> int </code>です。これは一般的な方法で以下のコンビネータ。スタックの上位2つの要素が等しい場合は<code> COMPARE </code>の結果は<code> 0 </code>であり、スタックの最初の要素が2番目の要素でない場合は負で、それ以外の場合は負です。
+Comparison only works on a class of types that we call comparable. A <code>COMPARE</code> operation is defined in an ad hoc way for each comparable type, but the result of compare is always an <code>int</code>, which can in turn be checked in a generic manner using the following combinators. The result of <code>COMPARE</code> is <code>0</code> if the top two elements of the stack are equal, negative if the first element in the stack is less than the second, and positive otherwise.
-* <code> EQ </code>：スタックEQualsの先頭がゼロであることを確認します。
+* <code>EQ</code>: Checks that the top of the stack EQuals zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
+<pre>:: int : 'S   -&gt;   bool : 'S
-＆gt; EQ / 0：S =＆gt;真：S
+&gt; EQ / 0 : S  =&gt;  True : S
-＆gt; EQ / v：S =＆gt; False：S
+&gt; EQ / v : S  =&gt;  False : S
-     if v < 0 </pre>
+     iff v &lt;&gt; 0</pre>
-* <code> NEQ </code>：スタックの一番上がEQualでないことをチェックします。
+* <code>NEQ</code>: Checks that the top of the stack does Not EQual zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
+<pre>:: int : 'S   -&gt;   bool : 'S
-＆gt; NEQ / 0：S =＆gt; False：S
+&gt; NEQ / 0 : S  =&gt;  False : S
-＆gt; NEQ / v：S =＆gt;真：S
+&gt; NEQ / v : S  =&gt;  True : S
-     if v < 0 </pre>
+     iff v &lt;&gt; 0</pre>
-* <code> LT </code>：スタックの一番上がゼロよりも小さいかどうかをチェックします。
+* <code>LT</code>: Checks that the top of the stack is Less Than zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
+<pre>:: int : 'S   -&gt;   bool : 'S
-＆gt; LT / v：S =＆gt;真：S
+&gt; LT / v : S  =&gt;  True : S
-     if <v < 0
+     iff  v &lt; 0
-＆gt; LT / v：S =＆gt; False：S
+&gt; LT / v : S  =&gt;  False : S
-     if v> = 0 </pre>
+     iff v &gt;= 0</pre>
-* <code> GT </code>：スタックの先頭がゼロより大きいかどうかをチェックします。
+* <code>GT</code>: Checks that the top of the stack is Greater Than zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
+<pre>:: int : 'S   -&gt;   bool : 'S
-＆gt; GT / v：S =＆gt; C / True：S
+&gt; GT / v : S  =&gt;  C / True : S
-     if v>＆gt; 0
+     iff  v &gt; 0
-＆gt; GT / v：S =＆gt; C / False：S
+&gt; GT / v : S  =&gt;  C / False : S
-     if v <= 0 </pre>
+     iff v &lt;= 0</pre>
-* <code> LE </code>：スタックの一番上が0より小さいかどうかをチェックします。
+* <code>LE</code>: Checks that the top of the stack is Less Than of Equal to zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
-＆gt; LE / v：S =＆gt;真：S
+<pre>:: int : 'S   -&gt;   bool : 'S
-     v≠0の場合
-＆gt; LE / v：S =＆gt; False：S
+&gt; LE / v : S  =&gt;  True : S
-     if v>＆gt; 0 </pre>
+     iff  v &lt;= 0
-* <code> GE </code>：スタックの最上部がゼロより大きいかどうかをチェックします。
+&gt; LE / v : S  =&gt;  False : S
+     iff v &gt; 0</pre>
+* <code>GE</code>: Checks that the top of the stack is Greater Than of Equal to zero.
 ::
-<pre> :: int： 'S - ＆gt;ブール： 'S
+<pre>:: int : 'S   -&gt;   bool : 'S
-＆gt; GE / v：S =＆gt;真：S
+&gt; GE / v : S  =&gt;  True : S
-     if≠v> = 0
+     iff  v &gt;= 0
-＆gt; GE / v：S =＆gt; False：S
+&gt; GE / v : S  =&gt;  False : S
-     if <v < 0 </pre>
+     iff v &lt; 0</pre>
-== V - 操作==
+== V - Operations ==
-ブール演算子<sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub>?<sub>?</sub > </sub>?
+Operations on booleans <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~
-* <code> OR </code>
+* <code>OR</code>
 ::
-<pre> :: bool：bool： 'S - ＆gt;ブール： 'S
+<pre>:: bool : bool : 'S   -&gt;   bool : 'S
-＆gt; OR / x：y：S =＆gt; （x | y）：S </pre>
+&gt; OR / x : y : S  =&gt;  (x | y) : S</pre>
-* <code> AND </code>
+* <code>AND</code>
 ::
-<pre> :: bool：bool： 'S - ＆gt;ブール： 'S
+<pre>:: bool : bool : 'S   -&gt;   bool : 'S
-＆gt; AND / x：y：S =＆gt; （x＆y）：S </pre>
+&gt; AND / x : y : S  =&gt;  (x &amp; y) : S</pre>
-* <code> XOR </code>
+* <code>XOR</code>
 ::
-<pre> :: bool：bool： 'S - ＆gt;ブール： 'S
+<pre>:: bool : bool : 'S   -&gt;   bool : 'S
-＆gt; XOR / x：y：S =＆gt; （x ^ y）：S </pre>
+&gt; XOR / x : y : S  =&gt;  (x ^ y) : S</pre>
-* <code> NOT </code>
+* <code>NOT</code>
 ::
-<pre> :: bool： 'S - ＆gt;ブール： 'S
+<pre>:: bool : 'S   -&gt;   bool : 'S
-＆gt; NOT / x：S =＆gt; ?x：S </pre>
+&gt; NOT / x : S  =&gt;  ~x : S</pre>
-整数と自然数の操作<sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> / sub> </sub> </sub> </sub> </sub> </sub> </sub> sub> <sub>?</sub>?</sub> ~~
+Operations on integers and natural numbers <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub><sub><sub><sub><sub>~</sub></sub></sub></sub><sub>~</sub>~</sub>~~
-整数と自然体は任意の精度です。つまり、サイズ制限は燃料だけです。
+Integers and naturals are arbitrary-precision, meaning the only size limit is fuel.
-* <code> NEG </code>
+* <code>NEG</code>
 ::
-<pre> :: int： 'S - ＆gt; int： 'S
+<pre>:: int : 'S   -&gt;   int : 'S
-:: nat： 'S - ＆gt; int： 'S
+:: nat : 'S   -&gt;   int : 'S
-＆gt; NEG / x：S =＆gt; -x：S </pre>
+&gt; NEG / x : S  =&gt;  -x : S</pre>
-* <code> ABS </code>
+* <code>ABS</code>
 ::
-<pre> :: int： 'S - ＆gt;ナット： 'S
+<pre>:: int : 'S   -&gt;   nat : 'S
-＆gt; ABS / x：S =＆gt; abs（x）：S </pre>
+&gt; ABS / x : S  =&gt;  abs (x) : S</pre>
-* <code>追加</code>
+* <code>ADD</code>
 ::
-<pre> :: int：int： 'S - ＆gt; int： 'S
-:: int：nat： 'S - ＆gt; int： 'S
-:: nat：int： 'S - ＆gt; int： 'S
-:: nat：nat： 'S - ＆gt;ナット： 'S
-＆gt; ADD / x：y：S =＆gt; （x + y）：S </pre>
+<pre>:: int : int : 'S   -&gt;   int : 'S
-* <code> SUB </code>
+:: int : nat : 'S   -&gt;   int : 'S
+:: nat : int : 'S   -&gt;   int : 'S
+:: nat : nat : 'S   -&gt;   nat : 'S
+&gt; ADD / x : y : S  =&gt;  (x + y) : S</pre>
+* <code>SUB</code>
 ::
-<pre> :: int：int： 'S - ＆gt; int： 'S
+<pre>:: int : int : 'S   -&gt;   int : 'S
-:: int：nat： 'S - ＆gt; int： 'S
+:: int : nat : 'S   -&gt;   int : 'S
-:: nat：int： 'S - ＆gt; int： 'S
+:: nat : int : 'S   -&gt;   int : 'S
-:: nat：nat： 'S - ＆gt; int： 'S
+:: nat : nat : 'S   -&gt;   int : 'S
-＆gt; SUB / x：y：S =＆gt; （x-y）：S </pre>
+&gt; SUB / x : y : S  =&gt;  (x - y) : S</pre>
-* <code> MUL </code>
+* <code>MUL</code>
 ::
-<pre> :: int：int： 'S - ＆gt; int： 'S
+<pre>:: int : int : 'S   -&gt;   int : 'S
-:: int：nat： 'S - ＆gt; int： 'S
+:: int : nat : 'S   -&gt;   int : 'S
-:: nat：int： 'S - ＆gt; int： 'S
+:: nat : int : 'S   -&gt;   int : 'S
-:: nat：nat： 'S - ＆gt;ナット： 'S
+:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; MUL / x：y：S =＆gt; （x * y）：S </pre>
+&gt; MUL / x : y : S  =&gt;  (x * y) : S</pre>
-* <code> EDIV </code>ユークリッド分割を実行する
+* <code>EDIV</code> Perform Euclidian division
 ::
-<pre> :: int：int： 'S - ＆gt;オプション（ペアint nat）： 'S
+<pre>:: int : int : 'S   -&gt;   option (pair int nat) : 'S
-:: int：nat： 'S - ＆gt;オプション（ペアint nat）： 'S
+:: int : nat : 'S   -&gt;   option (pair int nat) : 'S
-:: nat：int： 'S - ＆gt;オプション（ペアint nat）： 'S
+:: nat : int : 'S   -&gt;   option (pair int nat) : 'S
-:: nat：nat： 'S - ＆gt;オプション（ペアナット）： 'S
+:: nat : nat : 'S   -&gt;   option (pair nat nat) : 'S
-＆gt; EDIV / x：0：S =＆gt;なし：S
+&gt; EDIV / x : 0 : S  =&gt;  None : S
-＆gt; EDIV / x：y：S =＆gt;いくつか（ペア（x / y）（x％y））：S
+&gt; EDIV / x : y : S  =&gt;  Some (Pair (x / y) (x % y)) : S
-     if <y < 0 </pre>
+     iff y &lt;&gt; 0</pre>
-ビット単位の論理演算子は、符号なし整数でも使用できます。
+Bitwise logical operators are also available on unsigned integers.
-* <code> OR </code>
+* <code>OR</code>
 ::
-<pre> :: nat：nat： 'S - ＆gt;ナット： 'S
+<pre>:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; OR / x：y：S =＆gt; （x | y）：S </pre>
+&gt; OR / x : y : S  =&gt;  (x | y) : S</pre>
-* <code> AND </code>
+* <code>AND</code>
 ::
-<pre> :: nat：nat： 'S - ＆gt;ナット： 'S
+<pre>:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; AND / x：y：S =＆gt; （x＆y）：S </pre>
+&gt; AND / x : y : S  =&gt;  (x &amp; y) : S</pre>
-* <code> XOR </code>
+* <code>XOR</code>
 ::
-<pre> :: nat：nat： 'S - ＆gt;ナット： 'S
+<pre>:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; XOR / x：y：S =＆gt; （x ^ y）：S </pre>
+&gt; XOR / x : y : S  =&gt;  (x ^ y) : S</pre>
-* <code> NOT </code>の戻り値の型は<code> nat </code>ではなく<code> int </code>です。これは、符号も否定されているためです。結果の整数は、2の補数を使用して計算されます。たとえば、<code> 0 </code>のブール値の否定は<code> -1 </code>です。
+* <code>NOT</code> The return type of <code>NOT</code> is an <code>int</code> and not a <code>nat</code>. This is because the sign is also negated. The resulting integer is computed using two’s complement. For instance, the boolean negation of <code>0</code> is <code>-1</code>.
 ::
-<pre> :: nat： 'S - ＆gt; int： 'S
+<pre>:: nat : 'S   -&gt;   int : 'S
-:: int： 'S - ＆gt; int： 'S
+:: int : 'S   -&gt;   int : 'S
-＆gt; NOT / x：S =＆gt; ?x：S </pre>
+&gt; NOT / x : S  =&gt;  ~x : S</pre>
-* <code> LSL </code>
+* <code>LSL</code>
 ::
-<pre> :: nat：nat： 'S - ＆gt;ナット： 'S
+<pre>:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; LSL / x：s：S =＆gt; （x <s）：S
+&gt; LSL / x : s : S  =&gt;  (x &lt;&lt; s) : S
-     iff≦256
+     iff   s &lt;= 256
-＆gt; LSL / x：s：S =＆gt; [失敗します]
+&gt; LSL / x : s : S  =&gt;  [FAIL]
-     iff＆gt; 256 </pre>
+     iff   s &gt; 256</pre>
-* <code> LSR </code>
+* <code>LSR</code>
 ::
-<pre> :: nat：nat： 'S - ＆gt;ナット： 'S
+<pre>:: nat : nat : 'S   -&gt;   nat : 'S
-＆gt; LSR / x：s：S =＆gt; （x> s）：S </pre>
+&gt; LSR / x : s : S  =&gt;  (x &gt;&gt;&gt; s) : S</pre>
-* <code> COMPARE </code>：整数/自然比較
+* <code>COMPARE</code>: Integer/natural comparison
 ::
-<pre> :: int：int： 'S - ＆gt; int： 'S
+<pre>:: int : int : 'S   -&gt;   int : 'S
-:: nat：nat： 'S - ＆gt; int： 'S
+:: nat : nat : 'S   -&gt;   int : 'S
-＆gt; COMPARE / x：y：S =＆gt; -1：S
+&gt; COMPARE / x : y : S  =&gt;  -1 : S
-     iff < y
+     iff x &lt; y
-＆gt; COMPARE / x：y：S =＆gt; 0：S
+&gt; COMPARE / x : y : S  =&gt;  0 : S
      iff x = y
-＆gt; COMPARE / x：y：S =＆gt; 1：S
+&gt; COMPARE / x : y : S  =&gt;  1 : S
-     iff x> y </pre>
+     iff x &gt; y</pre>
-文字列<sub> <sub> <sub> <sub>?</sub> </sub> </sub>?</sub>?</sub> ~~
+Operations on strings <sub><sub><sub><sub><sub>~</sub></sub></sub></sub><sub>~</sub>~</sub>~~
-文字列は、ほとんどの場合、外部IDデータベースに頼ることなく名前を付けるために使用されます。ですから、基本的には文字列定数をそのまま使用し、連結してキーとして使用します。
+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.
-* <code> CONCAT </code>：文字列の連結。
+* <code>CONCAT</code>: String concatenation.
 ::
-<pre> :: string：string： 'S - ＆gt;文字列： 'S
+<pre>:: string : string : 'S   -&gt; string : 'S
-＆gt; CONCAT / s：t：S =＆gt; （s ^ t）：S </pre>
+&gt; CONCAT / s : t : S  =&gt;  (s ^ t) : S</pre>
-* <code> COMPARE </code>：辞書順比較。
+* <code>COMPARE</code>: Lexicographic comparison.
 ::
-<pre> :: string：string： 'S - ＆gt; int： 'S
+<pre>:: string : string : 'S   -&gt;   int : 'S
-＆gt; COMPARE / s：t：S =＆gt; -1：S
+&gt; COMPARE / s : t : S  =&gt;  -1 : S
-     if <s < t
+     iff s &lt; t
-＆gt; COMPARE / s：t：S =＆gt; 0：S
+&gt; COMPARE / s : t : S  =&gt;  0 : S
      iff s = t
-＆gt; COMPARE / s：t：S =＆gt; 1：S
+&gt; COMPARE / s : t : S  =&gt;  1 : S
-     iff＆gt; t </pre>
+     iff s &gt; t</pre>
-ペア<sub> <sub> <sub>?</sub> </sub>?<sub> <sub> </sub> </sub>?</sub>
+Operations on pairs <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>
-* <code> PAIR </code>：スタックの上位2つの要素からペアを作成します。
+* <code>PAIR</code>: Build a pair from the stack’s top two elements.
 ::
-<pre> :: 'a：' b： 'S - ＆gt;ペア 'a' b： 'S
+<pre>:: 'a : 'b : 'S   -&gt;   pair 'a 'b : 'S
-＆gt; PAIR / a：b：S =＆gt; （ペアa b）：S </pre>
+&gt; PAIR / a : b : S  =&gt;  (Pair a b) : S</pre>
-* <code> CAR </code>：ペアの左部分にアクセスします。
+* <code>CAR</code>: Access the left part of a pair.
 ::
-<pre> ::ペア 'a _：' S - ＆gt; 'a：' S
+<pre>:: pair 'a _ : 'S   -&gt;   'a : 'S
-＆gt; CAR /（ペアa）：S =＆gt; a：S </pre>
+&gt; CAR / (Pair a _) : S  =&gt;  a : S</pre>
-* <code> CDR </code>：ペアの右部分にアクセスします。
+* <code>CDR</code>: Access the right part of a pair.
 ::
-<pre> ::ペア_ 'b：' S - ＆gt; 'b：' S
+<pre>:: pair _ 'b : 'S   -&gt;   'b : 'S
-＆gt; CDR /（ペア_b）：S =＆gt; b：S </pre>
+&gt; CDR / (Pair _ b) : S  =&gt;  b : S</pre>
-セット<sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub>??
+Operations on sets <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-* <code> EMPTY_SET 'elt </code>：指定された型の要素に対して新しい空のセットを作成します。
+* <code>EMPTY_SET 'elt</code>: Build a new, empty set for elements of a given type.
-<code> 'elt </code>型は同等でなければなりません（<code> COMPARE </code>プリミティブはその上に定義する必要があります）。
+The <code>'elt</code> type must be comparable (the <code>COMPARE</code> primitive must be defined over it).
 ::
-<pre> :: 'S - ＆gt; 'elt：'を設定してください
+<pre>:: 'S   -&gt;   set 'elt : 'S
-＆gt; EMPTY_SET _ / S =＆gt; {}：S </pre>
+&gt; EMPTY_SET _ / S  =&gt;  {} : S</pre>
-* <code> MEM </code>：セット内の要素の存在を確認します。
+* <code>MEM</code>: Check for the presence of an element in a set.
 ::
-<pre> :: 'elt：set' elt： 'S - ＆gt;ブール： 'S
-＆gt; MEM / x：{}：S =＆gt;偽：S
+<pre>:: 'elt : set 'elt : 'S   -&gt;  bool : 'S
-＆gt; MEM / x：{hd; <tl> }：S =＆gt; r：S
-     iff COMPARE / x：hd：[] =＆gt; 1：[]
+&gt; MEM / x : {} : S  =&gt;  false : S
-     ここで、MEM / x：v： }：S =＆gt; r：S
+&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  r : S
-＆gt; MEM / x：{hd; <tl> }：S =＆gt; true：S
+     iff COMPARE / x : hd : []  =&gt;  1 : []
-     iff COMPARE / x：hd：[] =＆gt; 0：[]
+     where MEM / x : v : { &lt;tl&gt; } : S  =&gt;  r : S
-＆gt; MEM / x：{hd; <tl> }：S =＆gt;偽：S
+&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  true : S
-     iff COMPARE / x：hd：[] =＆gt; -1：[] </pre>
+     iff COMPARE / x : hd : []  =&gt;  0 : []
-* <code> UPDATE </code>：セット内の要素を挿入または削除し、以前の値を置き換えます。
+&gt; MEM / x : { hd ; &lt;tl&gt; } : S  =&gt;  false : S
+     iff COMPARE / x : hd : []  =&gt;  -1 : []</pre>
+* <code>UPDATE</code>: Inserts or removes an element in a set, replacing a previous value.
 ::
-<pre> :: 'elt：bool：set' elt： 'S - ＆gt; 'elt：'を設定してください
+<pre>:: 'elt : bool : set 'elt : 'S   -&gt;   set 'elt : 'S
-＆gt; UPDATE / x：false：{}：S =＆gt; {}：S
+&gt; UPDATE / x : false : {} : S  =&gt;  {} : S
-＆gt; UPDATE / x：true：{}：S =＆gt; {x}：S
+&gt; UPDATE / x : true : {} : S  =&gt;  { x } : S
-＆gt; UPDATE / x：v：{hd; <tl> }：S =＆gt; {hd; ＆lt; tl＆gt; }：S
+&gt; UPDATE / x : v : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl'&gt; } : S
-     iff COMPARE / x：hd：[] =＆gt; 1：[]
+     iff COMPARE / x : hd : []  =&gt;  1 : []
-     ここで、UPDATE / x：v：{tl> }：S =＆gt; {t1 ' }：S
+     where UPDATE / x : v : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S
-＆gt; UPDATE / x：false：{hd; <tl> }：S =＆gt; { }：S
+&gt; UPDATE / x : false : { hd ; &lt;tl&gt; } : S  =&gt;  { &lt;tl&gt; } : S
-     iff COMPARE / x：hd：[] =＆gt; 0：[]
+     iff COMPARE / x : hd : []  =&gt;  0 : []
-＆gt; UPDATE / x：true：{hd; <tl> }：S =＆gt; {hd; <tl> }：S
+&gt; UPDATE / x : true : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl&gt; } : S
-     iff COMPARE / x：hd：[] =＆gt; 0：[]
+     iff COMPARE / x : hd : []  =&gt;  0 : []
-＆gt; UPDATE / x：false：{hd; <tl> }：S =＆gt; {hd; <tl> }：S
+&gt; UPDATE / x : false : { hd ; &lt;tl&gt; } : S  =&gt;  { hd ; &lt;tl&gt; } : S
-     iff COMPARE / x：hd：[] =＆gt; -1：[]
+     iff COMPARE / x : hd : []  =&gt;  -1 : []
-＆gt; UPDATE / x：true：{hd; <tl> }：S =＆gt; { バツ ; hd; <tl> }：S
+&gt; UPDATE / x : true : { hd ; &lt;tl&gt; } : S  =&gt;  { x ; hd ; &lt;tl&gt; } : S
-     iff COMPARE / x：hd：[] =＆gt; -1：[] </pre>
+     iff COMPARE / x : hd : []  =&gt;  -1 : []</pre>
-* <code> REDUCE </code>：セットに関数を適用し、各アプリケーションの結果を次のものに渡し、最後のものを返します。
+* <code>REDUCE</code>: Apply a function on a set passing the result of each application to the next one and return the last.
 ::
-<pre> :: lambda（ペア 'elt *' b） 'b：' elt： 'b：' S - ＆gt; 'b：' S
+<pre>:: lambda (pair 'elt * 'b) 'b : set 'elt : 'b : 'S   -&gt;   'b : 'S
-＆gt; REDUCE / f：{}：b：S =＆gt; b：S
+&gt; REDUCE / f : {} : b : S  =&gt;  b : S
-＆gt; REDUCE / f：{hd：＆lt; tl＆gt; }：b：S =＆gt; REDUCE / f：{tl＆gt; }：c：S
+&gt; REDUCE / f : { hd : &lt;tl&gt; } : b : S  =&gt;  REDUCE / f : { &lt;tl&gt; } : c : S
-     ここで、f /ペアhd b：[] =＆gt; c：[] </pre>
+     where f / Pair hd b : []  =&gt;  c : []</pre>
-* <code> ITER body </code>：セットの各要素にボディ式を適用します。ボディシーケンスはスタックにアクセスできます。
+* <code>ITER body</code>: Apply the body expression to each element of a set. The body sequence has access to the stack.
 ::
-<pre> ::（set 'elt）：' A - ＆gt; 'A
+<pre>:: (set 'elt) : 'A   -&gt;  'A
-    if body :: ['elt：' A - ＆gt; 'A]
+    iff body :: [ 'elt : 'A -&gt; 'A ]
-＆gt; ITER本体/ {}：S =＆gt; S
+&gt; ITER body / {} : S  =&gt;  S
-＆gt; ITER本体/ {hd; <tl> }：S =＆gt;体; ITER本体/ hd：{＆lt; }：S </pre>
+&gt; ITER body / { hd ; &lt;tl&gt; } : S  =&gt;  body; ITER body / hd : { &lt;tl&gt; } : S</pre>
-* <code> SIZE </code>：セットの基数を取得します。
+* <code>SIZE</code>: Get the cardinality of the set.
 ::
-<pre> :: set 'elt：' S - ＆gt;ナット： 'S
-＆gt; SIZE / {}：S =＆gt; 0：S
+<pre>:: set 'elt : 'S -&gt; nat : 'S
-＆gt; SIZE / {_; <tl> }：S =＆gt; 1 + s：S
-    ここで、SIZE / { }：S =＆gt; s：S </pre>
-マップ<sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
-* <code> EMPTY_MAP 'key' val </code>：指定された型のキーから別の型の値まで、新しい空のマップを構築します。
+&gt; SIZE / {} : S  =&gt;  0 : S
+&gt; SIZE / { _ ; &lt;tl&gt; } : S  =&gt;  1 + s : S
+    where SIZE / { &lt;tl&gt; } : S  =&gt;  s : S</pre>
+Operations on maps <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-<code> 'key </code>型は同等でなければなりません（<code> COMPARE </code>プリミティブはその上に定義する必要があります）。
+* <code>EMPTY_MAP 'key 'val</code>: Build a new, empty map from keys of a given type to values of another given type.
+The <code>'key</code> type must be comparable (the <code>COMPARE</code> primitive must be defined over it).
 ::
-<pre> :: 'S - ＆gt;マップ 'key' val： 'S
+<pre>:: 'S -&gt; map 'key 'val : 'S
-＆gt; EMPTY_MAP _ / S =＆gt; {}：S </pre>
+&gt; EMPTY_MAP _ _ / S  =&gt;  {} : S</pre>
-* <code> GET </code>：マップ内の要素にアクセスし、<code> IF_SOME </code>でチェックするオプションの値を返します。
+* <code>GET</code>: Access an element in a map, returns an optional value to be checked with <code>IF_SOME</code>.
 ::
-<pre> :: 'key：map' key 'val：' S - ＆gt;オプション 'val：' S
+<pre>:: 'key : map 'key 'val : 'S   -&gt;   option 'val : 'S
-＆gt; GET / x：{}：S =＆gt;なし：S
+&gt; GET / x : {} : S  =&gt;  None : S
-＆gt; GET / x：{Elt k v; <tl> }：S =＆gt; opt_y：S
+&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  opt_y : S
-     iff COMPARE / x：k：[] =＆gt; 1：[]
+     iff COMPARE / x : k : []  =&gt;  1 : []
-ここで、GET / x：{tl> }：S =＆gt; opt_y：S
+where GET / x : { &lt;tl&gt; } : S  =&gt;  opt_y : S
-＆gt; GET / x：{Elt k v; <tl> }：S =＆gt;いくつかのv：S
+&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  Some v : S
-     iff COMPARE / x：k：[] =＆gt; 0：[]
+     iff COMPARE / x : k : []  =&gt;  0 : []
-＆gt; GET / x：{Elt k v; <tl> }：S =＆gt;なし：S
+&gt; GET / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  None : S
-     iff COMPARE / x：k：[] =＆gt; -1：[] </pre>
+     iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
-* <code> MEM </code>：マップ内のキーのバインディングが存在するかどうかを確認します。
+* <code>MEM</code>: Check for the presence of a binding for a key in a map.
 ::
-<pre> :: 'key：map' key 'val：' S - ＆gt;ブール： 'S
+<pre>:: 'key : map 'key 'val : 'S   -&gt;  bool : 'S
-＆gt; MEM / x：{}：S =＆gt;偽：S
+&gt; MEM / x : {} : S  =&gt;  false : S
-＆gt; MEM / x：{Elt k v; <tl> }：S =＆gt; r：S
+&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  r : S
-     iff COMPARE / x：k：[] =＆gt; 1：[]
+     iff COMPARE / x : k : []  =&gt;  1 : []
-     ここで、MEM / x：{tl }：S =＆gt; r：S
+     where MEM / x : { &lt;tl&gt; } : S  =&gt;  r : S
-＆gt; MEM / x：{Elt k v; <tl> }：S =＆gt; true：S
+&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  true : S
-     iff COMPARE / x：k：[] =＆gt; 0：[]
+     iff COMPARE / x : k : []  =&gt;  0 : []
-＆gt; MEM / x：{Elt k v; <tl> }：S =＆gt;偽：S
+&gt; MEM / x : { Elt k v ; &lt;tl&gt; } : S  =&gt;  false : S
-     iff COMPARE / x：k：[] =＆gt; -1：[] </pre>
+     iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
-* <code> UPDATE </code>：マップ内の要素を割り当てまたは削除します。
+* <code>UPDATE</code>: Assign or remove an element in a map.
 ::
-<pre> :: 'key：option' val：マップ 'key' val： 'S - ＆gt;マップ 'key' val： 'S
+<pre>:: 'key : option 'val : map 'key 'val : 'S   -&gt;   map 'key 'val : 'S
-＆gt; UPDATE / x：なし：{}：S =＆gt; {}：S
+&gt; UPDATE / x : None : {} : S  =&gt;  {} : S
-＆gt; UPDATE / x：Some y：{}：S =＆gt; {Elt x y}：S
+&gt; UPDATE / x : Some y : {} : S  =&gt;  { Elt x y } : S
-＆gt; UPDATE / x：opt_y：{Elt k v; <tl> }：S =＆gt; {Elt k v; ＆lt; tl＆gt; }：S
+&gt; UPDATE / x : opt_y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k v ; &lt;tl'&gt; } : S
-     iff COMPARE / x：k：[] =＆gt; 1：[]
+     iff COMPARE / x : k : []  =&gt;  1 : []
-ここで、UPDATE / x：opt_y：{＆lt; }：S =＆gt; {t1 ' }：S
+where UPDATE / x : opt_y : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S
-＆gt; UPDATE / x：なし：{Elt k v; <tl> }：S =＆gt; { }：S
+&gt; UPDATE / x : None : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { &lt;tl&gt; } : S
-     iff COMPARE / x：k：[] =＆gt; 0：[]
+     iff COMPARE / x : k : []  =&gt;  0 : []
-＆gt; UPDATE / x：いくつかのy：{Elt k v; <tl> }：S =＆gt; {Elt k y; <tl> }：S
+&gt; UPDATE / x : Some y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k y ; &lt;tl&gt; } : S
-     iff COMPARE / x：k：[] =＆gt; 0：[]
+     iff COMPARE / x : k : []  =&gt;  0 : []
-＆gt; UPDATE / x：なし：{Elt k v; <tl> }：S =＆gt; {Elt k v; <tl> }：S
+&gt; UPDATE / x : None : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k v ; &lt;tl&gt; } : S
-     iff COMPARE / x：k：[] =＆gt; -1：[]
+     iff COMPARE / x : k : []  =&gt;  -1 : []
-＆gt; UPDATE / x：いくつかのy：{Elt k v; <tl> }：S =＆gt; {Elt x y; Elt k v; <tl> }：S
+&gt; UPDATE / x : Some y : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt x y ; Elt k v ; &lt;tl&gt; } : S
-     iff COMPARE / x：k：[] =＆gt; -1：[] </pre>
+     iff COMPARE / x : k : []  =&gt;  -1 : []</pre>
-* <code> MAP </code>：マップ上に関数を適用し、同じバインディングで結果のマップを返します。
+* <code>MAP</code>: Apply a function on a map and return the map of results under the same bindings.
 ::
-<pre> :: lambda（ペア 'キー' val） 'b：マップ'キー 'val：' S - ＆gt;マップ 'キー' b： 'S
+<pre>:: lambda (pair 'key 'val) 'b : map 'key 'val : 'S   -&gt;   map 'key 'b : 'S
-＆gt; MAP / f：{}：S =＆gt; {}：S
+&gt; MAP / f : {} : S  =&gt;  {} : S
-＆gt; MAP / f：{Elt k v; <tl> }：S =＆gt; {Elt k（f（Pair k v））; ＆lt; tl＆gt; }：S
+&gt; MAP / f : { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k (f (Pair k v)) ; &lt;tl'&gt; } : S
-     ここで、MAP / f：{tl }：S =＆gt; {t1 ' }：S </pre>
+     where MAP / f : { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S</pre>
-* <code> MAP body </code>：マップの各要素にボディ式を適用します。ボディシーケンスはスタックにアクセスできます。
+* <code>MAP body</code>: Apply the body expression to each element of a map. The body sequence has access to the stack.
 ::
-<pre> ::（map 'key' val）： 'A - ＆gt; （マップ 'キー' b）： 'A
+<pre>:: (map 'key 'val) : 'A   -&gt;  (map 'key 'b) : 'A
-    if body :: [（pair 'key' val）： 'A - ＆gt; 'b：' A]
+    iff   body :: [ (pair 'key 'val) : 'A -&gt; 'b : 'A ]
-＆gt; MAP body / {}：S =＆gt; {}：S
+&gt; MAP body / {} : S  =&gt;  {} : S
-＆gt; MAPボディ/ {Elt k v; <tl> }：S =＆gt; {Elt k（body（Pair k v））; ＆lt; tl＆gt; }：S
+&gt; MAP body / { Elt k v ; &lt;tl&gt; } : S  =&gt;  { Elt k (body (Pair k v)) ; &lt;tl'&gt; } : S
-     ここで、MAPボディ/ { }：S =＆gt; {t1 ' }：S </pre>
+     where MAP body / { &lt;tl&gt; } : S  =&gt;  { &lt;tl'&gt; } : S</pre>
-* <code> REDUCE </code>：マップ上に関数を適用し、各アプリケーションの結果を次のものに渡し、最後のものを返します。
+* <code>REDUCE</code>: Apply a function on a map passing the result of each application to the next one and return the last.
 ::
-<pre> :: lambda（pair（pair 'key' val） 'b）' b：map 'キー' val： 'b：' S - ＆gt; 'b：' S
-＆gt; REDUCE / f：{}：b：S =＆gt; b：S
+<pre>:: lambda (pair (pair 'key 'val) 'b) 'b : map 'key 'val : 'b : 'S   -&gt;   'b : 'S
-＆gt;減退/ f：{エルt k; <tl> }：b：S =＆gt; REDUCE / f：{tl＆gt; }：c：S
-     ここで、f /ペア（ペアk v）b：[] =＆gt; c </pre>
+&gt; REDUCE / f : {} : b : S  =&gt;  b : S
-* <code> ITER body </code>：マップの各要素にボディ式を適用します。ボディシーケンスはスタックにアクセスできます。
+&gt; REDUCE / f : { Elt k v ; &lt;tl&gt; } : b : S  =&gt;  REDUCE / f : { &lt;tl&gt; } : c : S
+     where f / Pair (Pair k v) b : []  =&gt;  c</pre>
+* <code>ITER body</code>: Apply the body expression to each element of a map. The body sequence has access to the stack.
 ::
-<pre> ::（マップ 'elt' val）： 'A - ＆gt; 'A
+<pre>:: (map 'elt 'val) : 'A   -&gt;  'A
-    if body :: [（ペア 'elt' val）： 'A - ＆gt; 'A]
+    iff   body :: [ (pair 'elt 'val) : 'A -&gt; 'A ]
-＆gt; ITER本体/ {}：S =＆gt; S
+&gt; ITER body / {} : S  =&gt;  S
-＆gt; ITER本体/ {Elt k v; <tl> }：S =＆gt;体 ; ITER本体/（対k v）：{ }：S </pre>
+&gt; ITER body / { Elt k v ; &lt;tl&gt; } : S  =&gt;  body ; ITER body / (Pair k v) : { &lt;tl&gt; } : S</pre>
-* <code> SIZE </code>：地図のカーディナリティを取得します。
+* <code>SIZE</code>: Get the cardinality of the map.
 ::
-<pre> :: map 'key' val： 'S - ＆gt;ナット： 'S
+<pre>:: map 'key 'val : 'S -&gt; nat : 'S
-＆gt; SIZE / {}：S =＆gt; 0：S
+&gt; SIZE / {} : S  =&gt;  0 : S
-＆gt; SIZE / {_; <tl> }：S =＆gt; 1 + s：S
+&gt; SIZE / { _ ; &lt;tl&gt; } : S  =&gt;  1 + s : S
-     ここで、SIZE / { }：S =＆gt; s：S </pre>
+     where  SIZE / { &lt;tl&gt; } : S  =&gt;  s : S</pre>
-<code> big_maps </code> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> / sub> </sub> </sub> </sub> </sub>
+Operations on <code>big_maps</code> <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub>~</sub>~~
-これらの操作の動作は、通常のマップの場合と同じですが、フードの下では、要素がオンデマンドでロードされ、デシリアライズされます。
+The behaviour of these operations is the same as if they were normal maps, except that under the hood, the elements are loaded and deserialized on demand.
-* <code> GET </code>：<code> big_map </code>の要素にアクセスし、<code> IF_SOME </code>でチェックするオプションの値を返します。
+* <code>GET</code>: Access an element in a <code>big_map</code>, returns an optional value to be checked with <code>IF_SOME</code>.
 ::
-<pre> :: 'key：big_map' key 'val：' S - ＆gt;オプション 'val：' S </pre>
+<pre>:: 'key : big_map 'key 'val : 'S   -&gt;   option 'val : 'S</pre>
-* <code> MEM </code>：<code> big_map </code>で要素の存在を確認します。
+* <code>MEM</code>: Check for the presence of an element in a <code>big_map</code>.
 ::
-<pre> :: 'key：big_map' key 'val：' S - ＆gt; bool： 'S </pre>
+<pre>:: 'key : big_map 'key 'val : 'S   -&gt;  bool : 'S</pre>
-* <code> UPDATE </code>：<code> big_map </code>で要素を割り当てたり削除したりします。
+* <code>UPDATE</code>: Assign or remove an element in a <code>big_map</code>.
 ::
-<pre> :: 'key：オプション' val：big_map 'key' val： 'S - ＆gt; big_map 'key' val： 'S </pre>
+<pre>:: 'key : option 'val : big_map 'key 'val : 'S   -&gt;   big_map 'key 'val : 'S</pre>
-オプション値<sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub>?</sub> sub> </sub> </sub> </sub> </sub> </sub> </sub>
+Operations on optional values <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>~~
-* <code> SOME </code>：現在のオプション値をパックします。
+* <code>SOME</code>: Pack a present optional value.
 ::
-<pre> :: 'a：' S - ＆gt;オプション 'a：' S
+<pre>:: 'a : 'S   -&gt;   option 'a : 'S
-＆gt; SOME / v：S =＆gt; （一部v）：S </pre>
+&gt; SOME / v : S  =&gt;  (Some v) : S</pre>
-* <code> NONE 'a </code>：省略可能なオプションの値。
+* <code>NONE 'a</code>: The absent optional value.
 ::
-<pre> :: 'S - ＆gt;オプション 'a：' S
+<pre>:: 'S   -&gt;   option 'a : 'S
-＆gt; NONE / v：S =＆gt;なし：S </pre>
+&gt; NONE / v : S  =&gt;  None : S</pre>
-* <code> IF_NONE bt bf </code>：オプションの値を調べます。
+* <code>IF_NONE bt bf</code>: Inspect an optional value.
 ::
-<pre> ::オプション 'a：' S - ＆gt; 'b：' S
-   iff bt :: ['S - ＆gt; 'b：' S]
-         bf :: ['a：' S - ＆gt; 'b：' S]
-＆gt; IF_NONE bt bf /（なし）：S =＆gt; bt / S
+<pre>:: option 'a : 'S   -&gt;   'b : 'S
-＆gt; IF_NONE bt bf /（あるa）：S =＆gt; bf / a：S </pre>
+   iff   bt :: [ 'S -&gt; 'b : 'S]
-組合<sub> <sub> <sub>?</sub> </sub> <sub>?</sub> </sub> </sub>?<sub >?</sub>
+         bf :: [ 'a : 'S -&gt; 'b : 'S]
+&gt; IF_NONE bt bf / (None) : S  =&gt;  bt / S
+&gt; IF_NONE bt bf / (Some a) : S  =&gt;  bf / a : S</pre>
+Operations on unions <sub><sub><sub><sub>~</sub></sub></sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>
-* <code> LEFT 'b </code>：ユニオンに値をパックします（左のケース）。
+* <code>LEFT 'b</code>: Pack a value in a union (left case).
 ::
-<pre> :: 'a：' S - ＆gt;または 'a' b： 'S
+<pre>:: 'a : 'S   -&gt;   or 'a 'b : 'S
-＆gt; LEFT / v：S =＆gt; （左v）：S </pre>
+&gt; LEFT / v : S  =&gt;  (Left v) : S</pre>
-* <code> RIGHT 'a </code>：ユニオンに値をパックします（右のケース）。
+* <code>RIGHT 'a</code>: Pack a value in a union (right case).
 ::
-<pre> :: 'b：' S - ＆gt;または 'a' b： 'S
+<pre>:: 'b : 'S   -&gt;   or 'a 'b : 'S
-＆gt; RIGHT / v：S =＆gt; （右v）：S </pre>
+&gt; RIGHT / v : S  =&gt;  (Right v) : S</pre>
-* <code> IF_LEFT bt bf </code>：バリアント型の値を検査します。
+* <code>IF_LEFT bt bf</code>: Inspect a value of a variant type.
 ::
-<pre> ::または 'a' b： 'S - ＆gt; 'c：' S
+<pre>:: or 'a 'b : 'S   -&gt;   'c : 'S
-    iff bt :: ['a：' S - ＆gt; 'c：' S]
+    iff   bt :: [ 'a : 'S -&gt; 'c : 'S]
-          bf :: ['b：' S - ＆gt; 'c：' S]
+          bf :: [ 'b : 'S -&gt; 'c : 'S]
-＆gt; IF_LEFT bt bf /（左a）：S =＆gt; bt / a：S
+&gt; IF_LEFT bt bf / (Left a) : S  =&gt;  bt / a : S
-＆gt; IF_LEFT bt bf /（右b）：S =＆gt; bf / b：S </pre>
+&gt; IF_LEFT bt bf / (Right b) : S  =&gt;  bf / b : S</pre>
-* <code> IF_RIGHT bt bf </code>：バリアント型の値を検査します。
+* <code>IF_RIGHT bt bf</code>: Inspect a value of a variant type.
 ::
-<pre> ::または 'a' b： 'S - ＆gt; 'c：' S
+<pre>:: or 'a 'b : 'S   -&gt;   'c : 'S
-    iff bt :: ['b：' S - ＆gt; 'c：' S]
+    iff   bt :: [ 'b : 'S -&gt; 'c : 'S]
-          bf :: ['a：' S - ＆gt; 'c：' S]
+          bf :: [ 'a : 'S -&gt; 'c : 'S]
-＆gt; IF_RIGHT bt bf /（右b）：S =＆gt; bt / b：S
+&gt; IF_RIGHT bt bf / (Right b) : S  =&gt;  bt / b : S
-＆gt; IF_RIGHT bt bf /（左a）：S =＆gt; bf / a：S </pre>
+&gt; IF_RIGHT bt bf / (Left a) : S  =&gt;  bf / a : S</pre>
-リスト<sub> <sub> <sub>?</sub> </sub>?<sub> <sub>?</sub> </sub>?</sub>
+Operations on lists <sub><sub><sub>~</sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>
-* <code> CONS </code>：要素をリストの前に追加します。
+* <code>CONS</code>: Prepend an element to a list.
 ::
-<pre> :: 'a：list' a： 'S - ＆gt;リスト 'a：' S
+<pre>:: 'a : list 'a : 'S   -&gt;   list 'a : 'S
-＆gt; CONS / a：{1＆gt; }：S =＆gt; {a; ＆lt; 1＆gt; }：S </pre>
+&gt; CONS / a : { &lt;l&gt; } : S  =&gt;  { a ; &lt;l&gt; } : S</pre>
-* <code> NIL 'a </code>：空のリスト。
+* <code>NIL 'a</code>: The empty list.
 ::
-<pre> :: 'S - ＆gt;リスト 'a：' S
+<pre>:: 'S   -&gt;   list 'a : 'S
-＆gt; NIL / S =＆gt; {}：S </pre>
+&gt; NIL / S  =&gt;  {} : S</pre>
-* <code> IF_CONS bt bf </code>：オプションの値を調べます。
+* <code>IF_CONS bt bf</code>: Inspect an optional value.
 ::
-<pre> :: list 'a：' S - ＆gt; 'b：' S
+<pre>:: list 'a : 'S   -&gt;   'b : 'S
-    iff bt :: ['a：list' a： 'S - ＆gt; 'b：' S]
+    iff   bt :: [ 'a : list 'a : 'S -&gt; 'b : 'S]
-          bf :: ['S - ＆gt; 'b：' S]
+          bf :: [ 'S -&gt; 'b : 'S]
-＆gt; IF_CONS bt bf / {a; ＆lt; rest＆gt; }：S =＆gt; bt / a：{＆lt; rest＆gt; }：S
+&gt; IF_CONS bt bf / { a ; &lt;rest&gt; } : S  =&gt;  bt / a : { &lt;rest&gt; } : S
-＆gt; IF_CONS bt bf / {}：S =＆gt; bf / S </pre>
+&gt; IF_CONS bt bf / {} : S  =&gt;  bf / S</pre>
-* <code> MAP </code>：リストの関数を左から右に適用し、結果のリストを同じ順序で返します。
+* <code>MAP</code>: Apply a function on a list from left to right and return the list of results in the same order.
 ::
-<pre> :: lambda 'a' b：list 'a：' S - ＆gt;リスト 'b：' S
-＆gt; MAP / f：{a; ＆lt; rest＆gt; }：S =＆gt; {f a; ＆lt;休憩＆gt; }：S
+<pre>:: lambda 'a 'b : list 'a : 'S -&gt; list 'b : 'S
-     ここで、MAP / f：{＆lt; rest＆gt; }：S =＆gt; {＆lt; rest＆gt; }：S
-＆gt; MAP / f：{}：S =＆gt; {}：S </pre>
+&gt; MAP / f : { a ; &lt;rest&gt; } : S  =&gt;  { f a ; &lt;rest'&gt; } : S
-* <code> MAP body </code>：リストの各要素にボディ式を適用します。ボディシーケンスはスタックにアクセスできます。
+     where MAP / f : { &lt;rest&gt; } : S  =&gt;  { &lt;rest'&gt; } : S
+&gt; MAP / f : {} : S  =&gt;  {} : S</pre>
+* <code>MAP body</code>: Apply the body expression to each element of the list. The body sequence has access to the stack.
 ::
-<pre> ::（list 'elt）：' A - ＆gt; （リスト 'b）：' A
+<pre>:: (list 'elt) : 'A   -&gt;  (list 'b) : 'A
-    if body :: ['elt：' A - ＆gt; 'b：' A]
+    iff   body :: [ 'elt : 'A -&gt; 'b : 'A ]
-＆gt; MAPボディ/ {a; ＆lt; rest＆gt; }：S =＆gt; {body a; ＆lt;休憩＆gt; }：S
+&gt; MAP body / { a ; &lt;rest&gt; } : S  =&gt;  { body a ; &lt;rest'&gt; } : S
-     ここでMAP本体/ {＆lt; rest＆gt; }：S =＆gt; {＆lt; rest＆gt; }：S
+     where MAP body / { &lt;rest&gt; } : S  =&gt;  { &lt;rest'&gt; } : S
-＆gt; MAP body / {}：S =＆gt; {}：S </pre>
+&gt; MAP body / {} : S  =&gt;  {} : S</pre>
-* <code> REDUCE </code>：リストの関数を左から右に適用し、各アプリケーションの結果を次のものに渡して最後のものを返します。
+* <code>REDUCE</code>: Apply a function on a list from left to right passing the result of each application to the next one and return the last.
 ::
-<pre> :: lambda（ペア 'a' b） 'b：リスト' a： 'b：' S - ＆gt; 'b：' S
+<pre>:: lambda (pair 'a 'b) 'b : list 'a : 'b : 'S -&gt; 'b : 'S
-＆gt; REDUCE / f：{a：＆lt; rest＆gt; }：b：S =＆gt;減退/ f：{＆lt; rest＆gt; }：c：S
+&gt; REDUCE / f : { a : &lt;rest&gt; } : b : S  =&gt;  REDUCE / f : { &lt;rest&gt; } : c : S
-     ここで、f /ペアa b：[] =＆gt; c
+     where f / Pair a b : []  =&gt;  c
-＆gt; REDUCE / f：{}：b：S =＆gt; b：S </pre>
+&gt; REDUCE / f : {} : b : S  =&gt;  b : S</pre>
-* <code> SIZE </code>：リスト内の要素の数を取得します。
+* <code>SIZE</code>: Get the number of elements in the list.
 ::
-<pre> :: list 'elt：' S - ＆gt;ナット： 'S
+<pre>:: list 'elt : 'S -&gt; nat : 'S
-＆gt; SIZE / {_; ＆lt; rest＆gt; }：S =＆gt; 1 + s：S
+&gt; SIZE / { _ ; &lt;rest&gt; } : S  =&gt;  1 + s : S
-     SIZE / {＆lt; rest＆gt; }：S =＆gt; s：S
+     where  SIZE / { &lt;rest&gt; } : S  =&gt;  s : S
-＆gt; SIZE / {}：S =＆gt; 0：S </pre>
+&gt; SIZE / {} : S  =&gt;  0 : S</pre>
-* <code> ITER body </code>：リストの各要素にボディ式を適用します。ボディシーケンスはスタックにアクセスできます。
+* <code>ITER body</code>: Apply the body expression to each element of a list. The body sequence has access to the stack.
 ::
-<pre> ::（list 'elt）：' A - ＆gt; 'A
+<pre>:: (list 'elt) : 'A   -&gt;  'A
-      if body :: ['elt：' A - ＆gt; 'A]
+      iff body :: [ 'elt : 'A -&gt; 'A ]
-＆gt; ITER本体/ {a; ＆lt; rest＆gt; }：S =＆gt;体 ; ITER本体/ a：{＆lt; rest＆gt; }：S
+&gt; ITER body / { a ; &lt;rest&gt; } : S  =&gt;  body ; ITER body / a : { &lt;rest&gt; } : S
-＆gt; ITER本体/ {}：S =＆gt; S </pre>
+&gt; ITER body / {} : S  =&gt;  S</pre>
-== VI - ドメイン固有のデータ型==
+== VI - Domain specific data types ==
-* <code> timestamp </code>：現実世界の日付。
+* <code>timestamp</code>: Dates in the real world.
-* <code> tez </code>：トークンを操作するための特定のタイプ。
+* <code>tez</code>: A specific type for manipulating tokens.
-* <code> contract 'param' result </code>：契約のコードのタイプ。
+* <code>contract 'param 'result</code>: A contract, with the type of its code.
-* <code> key </code>：公開暗号鍵です。
+* <code>key</code>: A public cryptography key.
-* <code> key_hash </code>：公開暗号鍵のハッシュ。
+* <code>key_hash</code>: The hash of a public cryptography key.
-* <code>署名</code>：暗号署名。
+* <code>signature</code>: A cryptographic signature.
-== VII - ドメイン固有の操作==
-タイムスタンプの操作<sub> <sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> sub> </sub> </sub> </sub>
+== VII - Domain specific operations ==
-現在のタイムスタンプは、<code> NOW </code>操作で取得するか、スクリプトパラメータまたはグローバルから取得します。
+Operations on timestamps <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>
-* <code> ADD </code>指定された秒数のタイムスタンプを増減します。
+Current Timestamps can be obtained by the <code>NOW</code> operation, or retrieved from script parameters or globals.
+* <code>ADD</code> Increment / decrement a timestamp of the given number of seconds.
 ::
-<pre> :: timestamp：int： 'S - ＆gt;タイムスタンプ： 'S
+<pre>:: timestamp : int : 'S -&gt; timestamp : 'S
-:: int：タイムスタンプ： 'S - ＆gt;タイムスタンプ： 'S
+:: int : timestamp : 'S -&gt; timestamp : 'S
-＆gt; ADD /秒：nat（t）：S =＆gt; （秒+ t）：S
+&gt; ADD / seconds : nat (t) : S  =&gt;  (seconds + t) : S
-＆gt; ADD / nat（t）：秒：S =＆gt; （t +秒）：S </pre>
+&gt; ADD / nat (t) : seconds : S  =&gt;  (t + seconds) : S</pre>
-* <code> SUB </code>タイムスタンプから秒数を減算します。
+* <code>SUB</code> Subtract a number of seconds from a timestamp.
 ::
-<pre> :: timestamp：int： 'S - ＆gt;タイムスタンプ： 'S
+<pre>:: timestamp : int : 'S -&gt; timestamp : 'S
-＆gt; SUB /秒：nat（t）：S =＆gt; （秒 - t）：S </pre>
+&gt; SUB / seconds : nat (t) : S  =&gt;  (seconds - t) : S</pre>
-* <code> SUB </code> 2つのタイムスタンプを減算します。
+* <code>SUB</code> Subtract two timestamps.
 ::
-<pre> :: timestamp：タイムスタンプ： 'S - ＆gt; int： 'S
+<pre>:: timestamp : timestamp : 'S -&gt; int : 'S
-＆gt; SUB /秒（t1）：秒（t2）：S =＆gt; （t1-t2）：S </pre>
+&gt; SUB / seconds(t1) : seconds(t2) : S  =&gt;  (t1 - t2) : S</pre>
-* <code> COMPARE </code>：タイムスタンプの比較。
+* <code>COMPARE</code>: Timestamp comparison.
 ::
-<pre> :: timestamp：タイムスタンプ： 'S - ＆gt; int： 'S
+<pre>:: timestamp : timestamp : 'S   -&gt;   int : 'S
-＆gt; COMPARE /秒（t1）：秒（t2）：S =＆gt; -1：S
+&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  -1 : S
-     iff <t1 < t2
+     iff t1 &lt; t2
-＆gt; COMPARE /秒（t1）：秒（t2）：S =＆gt; 0：S
+&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  0 : S
      iff t1 = t2
-＆gt; COMPARE /秒（t1）：秒（t2）：S =＆gt; 1：S
+&gt; COMPARE / seconds(t1) : seconds(t2) : S  =&gt;  1 : S
-     iff1> t2 </pre>
+     iff t1 &gt; t2</pre>
-Tez <sub>?<sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub>?
+Operations on Tez <sub>~<sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~
-Tezは内部で64ビット符号付き整数で表されます。負の量のtezを作成しないようにする制限があります。オーバーフローを防止し、間違って他の数値型と混同されないように操作が制限されています。アンダーフロー/オーバーフローのチェックも必須です。
+Tez are internally represented by a 64 bit signed integer. There are restrictions to prevent creating a negative amount of tez. Operations are limited to prevent overflow and mixing them with other numerical types by mistake. They are also mandatory checked for under/overflows.
-* <code>追加</code>：
+* <code>ADD</code>:
 ::
-<pre> :: tez：tez： 'S - ＆gt; tez： 'S
+<pre>:: tez : tez : 'S   -&gt;   tez : 'S
-＆gt; ADD / x：y：S =＆gt;オーバーフロー時に[FAIL]
+&gt; ADD / x : y : S  =&gt;  [FAIL]   on overflow
-＆gt; ADD / x：y：S =＆gt; （x + y）：S </pre>
+&gt; ADD / x : y : S  =&gt;  (x + y) : S</pre>
-* <code> SUB </code>：
+* <code>SUB</code>:
 ::
-<pre> :: tez：tez： 'S - ＆gt; tez： 'S
+<pre>:: tez : tez : 'S   -&gt;   tez : 'S
-＆gt; SUB / x：y：S =＆gt; [失敗します]
+&gt; SUB / x : y : S  =&gt;  [FAIL]
-     iff < y
+     iff   x &lt; y
-＆gt; SUB / x：y：S =＆gt; （x-y）：S </pre>
+&gt; SUB / x : y : S  =&gt;  (x - y) : S</pre>
-* <code> MUL </code>
+* <code>MUL</code>
 ::
-<pre> :: tez：nat： 'S - ＆gt; tez： 'S
+<pre>:: tez : nat : 'S   -&gt;   tez : 'S
-:: nat：tez： 'S - ＆gt; tez： 'S
+:: nat : tez : 'S   -&gt;   tez : 'S
-＆gt; MUL / x：y：S =＆gt;オーバーフロー時に[FAIL]
+&gt; MUL / x : y : S  =&gt;  [FAIL]   on overflow
-＆gt; MUL / x：y：S =＆gt; （x * y）：S </pre>
+&gt; MUL / x : y : S  =&gt;  (x * y) : S</pre>
-* <code> EDIV </code>
+* <code>EDIV</code>
 ::
-<pre> :: tez：nat： 'S - ＆gt;オプション（ペアtez tez）： 'S
+<pre>:: tez : nat : 'S   -&gt;   option (pair tez tez) : 'S
-:: tez：tez： 'S - ＆gt;オプション（pair nat tez）： 'S
+:: tez : tez : 'S   -&gt;   option (pair nat tez) : 'S
-＆gt; EDIV / x：0：S =＆gt;なし
+&gt; EDIV / x : 0 : S  =&gt;  None
-＆gt; EDIV / x：y：S =＆gt;いくつか（ペア（x / y）（x％y））：S
+&gt; EDIV / x : y : S  =&gt;  Some (Pair (x / y) (x % y)) : S
-     if <y < 0 </pre>
+     iff y &lt;&gt; 0</pre>
-* <code> COMPARE </code>
+* <code>COMPARE</code>
 ::
-:: tez：tez： 'S - ＆gt; int： 'S
+:: tez : tez : ’S -&gt; int : ’S
-<blockquote> COMPARE / x：y：S =＆gt; -1：S iff x < y COMPARE / x：y：S =＆gt; 0：S iff x = y COMPARE / x：y：S =＆gt; 1：S iff x> y
+<blockquote>COMPARE / x : y : S =&gt; -1 : S iff x &lt; y COMPARE / x : y : S =&gt; 0 : S iff x = y COMPARE / x : y : S =&gt; 1 : S iff x &gt; y
 </blockquote>
-契約に関する操作<sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub> / sub>?<sub> </sub> </sub>
+Operations on contracts <sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>~<sub><sub><sub>~</sub></sub></sub>
-* <code> MANAGER </code>：契約のマネージャにアクセスします。
+* <code>MANAGER</code>: Access the manager of a contract.
 ::
-<pre> ::契約 'p' r： 'S - ＆gt; key_hash： 'S </pre>
+<pre>:: contract 'p 'r : 'S   -&gt;   key_hash : 'S</pre>
-* <code> CREATE_CONTRACT </code>：新しい契約を締結します。
+* <code>CREATE_CONTRACT</code>: Forge a new contract.
 ::
-<pre> :: key_hash：オプションkey_hash：bool：bool：tez：lambda（ペア 'p' g）（ペア 'r' g）： 'g：' S
+<pre>:: key_hash : option key_hash : bool : bool : tez : lambda (pair 'p 'g) (pair 'r 'g) : 'g : 'S
-    - ＆gt;契約 'p' r： 'S </pre>
+   -&gt; contract 'p 'r : 'S</pre>
-非コード発行元の場合と同様に、契約コードは、転送された金額にアドホック引数を加えたものを引数とし、アドホック値を返します。また、コードはグローバルデータを受け取り、次のトランザクションで格納および検索するためにグローバルデータを返します。これらのデータは別のパラメータで初期化されます。コードの呼び出し規約は次のとおりです。<code>（Pair arg globals））＆gt; （Pair ret globals）</code>を、命令タイプから外挿することができます。最初のパラメータは、マネージャ、オプションのデリゲート、消費可能で委任可能なフラグ、最後に現在実行されている契約から取られた初期の金額です。契約は、すぐに呼び出される、または格納されるファーストクラスの値として返されます。
+As with non code-emitted originations the contract code takes as argument the transferred 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: <code>(Pair arg globals)) -&gt; (Pair ret globals)</code>, as extrapolatable 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.
-* <code> CREATE_CONTRACT {storage 'g;パラメータ 'p; return 'r; code ...} </code>：新しい契約をリテラルから作成します。
+* <code>CREATE_CONTRACT { storage 'g ; parameter 'p ; return 'r ; code ... }</code>: Forge a new contract from a literal.
 ::
-<pre> :: key_hash：オプションkey_hash：bool：bool：tez： 'g：' S
+<pre>:: key_hash : option key_hash : bool : bool : tez : 'g : 'S
-    - ＆gt;契約 'p' r： 'S </pre>
+   -&gt; contract 'p 'r : 'S</pre>
-リテラルに基づいて契約を結ぶ。これは、現在のところ、発信契約の内部に転送を含める唯一の方法です。最初のパラメータは、マネージャ、オプションのデリゲート、消費可能で委任可能なフラグ、最後に現在実行されている契約から取られた初期の金額です。契約は、すぐに呼び出される、または格納されるファーストクラスの値として返されます。
+Originate a contract based on a literal. This is currently the only way to include transfers inside of an originated contract. 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.
-* <code> CREATE_ACCOUNT </code>：アカウントを作成します（コードなしの契約）。
+* <code>CREATE_ACCOUNT</code>: Forge an account (a contract without code).
 ::
-<pre> :: key_hash：オプションkey_hash：bool：tez： 'S - ＆gt;契約単位： 'S </pre>
+<pre>:: key_hash : option key_hash : bool : tez : 'S   -&gt;   contract unit unit : 'S</pre>
-manager、optional delegate、delegatableフラグ、そして最後に現在実行されている契約から取られた最初の金額を引数としてとります。
+Take as argument the manager, optional delegate, the delegatable flag and finally the initial amount taken from the currently executed contract.
-* <code> TRANSFER_TOKENS </code>：トランザクションを偽造して評価します。
+* <code>TRANSFER_TOKENS</code>: Forge and evaluate a transaction.
 ::
-<pre> :: 'p：tez：contract' p 'r：' g：[] - ＆gt; 'r：' g：[] </pre>
+<pre>:: 'p : tez : contract 'p 'r : 'g : []   -&gt;   'r : 'g : []</pre>
-パラメータと戻り値は、契約で想定されるもの、アカウントの単位と一致していなければなりません。システムのグローバル整合性を保持するには、現在のコントラクトのストレージを更新してから、別のスクリプトに制御を渡す必要があります。そのためには、スクリプトは部分的に更新されたストレージをスタックに置く必要があります（ 'gは契約のストレージのタイプです）。現在のコントラクトへの再帰呼び出しが行われた場合、更新された記憶域は戻り値の横のスタックに置かれます。ネストされたコール中にスタックに残るものは何もありません。ネストされた呼び出しの後にいくつかのローカル値を保持する必要がある場合は、それらを明示的にストレージの一時的な部分に格納する必要があります。その例は、ストレージにブール値を確保し、falseに初期化し、各契約実行の最後にfalseにリセットし、ネストされた呼び出し中にtrueに設定するという簡単な例です。これにより、契約で再帰呼び出しを防ぐ簡単な方法が提供されます（ブール値が真の場合、契約は失敗します）。
+The parameter and return value must be consistent with the ones expected by the contract, unit 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).
-* <code> BALANCE </code>：現在の契約の現在の金額を押します。
+* <code>BALANCE</code>: Push the current amount of tez of the current contract.
 ::
-<pre> :: 'S - ＆gt; tez： 'S </pre>
-* <code> SOURCE 'p' r </code>：現在のトランザクションのソース契約をプッシュします。
+<pre>:: 'S   -&gt;   tez : 'S</pre>
+* <code>SOURCE 'p 'r</code>: Push the source contract of the current transaction.
 ::
-<pre> :: 'S - ＆gt;契約 'p' r： 'S </pre>
+<pre>:: 'S   -&gt;   contract 'p 'r : 'S</pre>
-* <code> SELF </code>：現在の契約をプッシュします。
+* <code>SELF</code>: Push the current contract.
 ::
-<pre> :: 'S - ＆gt;契約 'p' r： 'S
+<pre>:: 'S   -&gt;   contract 'p 'r : 'S
-    契約 'p' rは現在の契約の種類です</pre>
+    where   contract 'p 'r is the type of the current contract</pre>
-* <code> AMOUNT </code>：現在のトランザクションの金額を押します。
+* <code>AMOUNT</code>: Push the amount of the current transaction.
 ::
-<pre> :: 'S - ＆gt; tez： 'S </pre>
+<pre>:: 'S   -&gt;   tez : 'S</pre>
-* <code> DEFAULT_ACCOUNT </code>：指定された公開鍵/秘密鍵のペアでデフォルトの契約を返します。この契約で預けられた資金は、秘密鍵の所有者が直ちに費やすことができます。この契約はマイケルソンコードを実行することはできず、常にブロックチェーン上に存在します。
+* <code>DEFAULT_ACCOUNT</code>: Return a default contract with the given public/private key pair. Any funds deposited in this contract can immediately be spent by the holder of the private key. This contract cannot execute Michelson code and will always exist on the blockchain.
 ::
-<pre> :: key_hash： 'S - ＆gt;契約単位： 'S </pre>
+<pre>:: key_hash : 'S   -&gt;   contract unit unit : 'S</pre>
-特別な操作<sub> <sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
+Special operations <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-* <code> STEPS_TO_QUOTA </code>：契約の実行を終了する前に残りの手順を実行します。
+* <code>STEPS_TO_QUOTA</code>: Push the remaining steps before the contract execution must terminate.
 ::
-<pre> :: 'S - ＆gt; nat： 'S </pre>
+<pre>:: 'S   -&gt;   nat : 'S</pre>
-* <code> NOW </code>：検証を実行したブロックのタイムスタンプをプッシュします（契約の実行中は変更されません）。
+* <code>NOW</code>: Push the timestamp of the block whose validation triggered this execution (does not change during the execution of the contract).
 ::
-<pre> :: 'S - ＆gt;タイムスタンプ： 'S </pre>
+<pre>:: 'S   -&gt;   timestamp : 'S</pre>
-暗号プリミティブ<sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub > </sub> <sub> <sub>?</sub> </sub> </sub>
+Cryptographic primitives <sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub><sub><sub>~</sub></sub></sub>
-* <code> HASH_KEY </code>：公開鍵のb58checkを計算します。
+* <code>HASH_KEY</code>: Compute the b58check of a public key.
 ::
-<pre> :: key： 'S - ＆gt; key_hash： 'S </pre>
+<pre>:: key : 'S   -&gt;   key_hash : 'S</pre>
-* <code> H </code>：Blake2B暗号ハッシュ関数を使用して、値の内容の暗号化ハッシュを計算します。
+* <code>H</code>: Compute a cryptographic hash of the value contents using the Blake2B cryptographic hash function.
 ::
-<pre> :: 'a：' S - ＆gt;文字列： 'S </pre>
+<pre>:: 'a : 'S   -&gt;   string : 'S</pre>
-* <code> CHECK_SIGNATURE </code>：指定されたキーで一連のバイトが署名されていることを確認します。
+* <code>CHECK_SIGNATURE</code>: Check that a sequence of bytes has been signed with a given key.
 ::
-<pre> :: key：ペア署名文字列： 'S - ＆gt; bool： 'S </pre>
+<pre>:: key : pair signature string : 'S   -&gt;   bool : 'S</pre>
-* <code> COMPARE </code>：
+* <code>COMPARE</code>:
 ::
-<pre> :: key_hash：key_hash： 'S - ＆gt; int： 'S
+<pre>:: key_hash : key_hash : 'S   -&gt;   int : 'S
-＆gt; COMPARE / x：y：S =＆gt; -1：S
+&gt; COMPARE / x : y : S  =&gt;  -1 : S
-     iff < y
+     iff x &lt; y
-＆gt; COMPARE / x：y：S =＆gt; 0：S
+&gt; COMPARE / x : y : S  =&gt;  0 : S
      iff x = y
-＆gt; COMPARE / x：y：S =＆gt; 1：S
+&gt; COMPARE / x : y : S  =&gt;  1 : S
-     iff x> y </pre>
+     iff x &gt; y</pre>
-== VIII - マクロ==
+== VIII - Macros ==
-上記の操作に加えて、言語の具体的な構文にいくつかの拡張が追加されています。これらのマクロを展開するクライアントをバイパスしてRPC経由でノードと対話している場合は、それらのマクロを展開する必要があります。
+In addition to the operations above, several extensions have been added to the language’s concrete syntax. If you are interacting with the node via RPC, bypassing the client, which expands away these macros, you will need to de-surgar them yourself.
-これらのマクロはあいまいではなく、可逆的に設計されています。つまり、エラーはデュアグラス構文で報告されます。これらのマクロは、他の構文形式で定義されています。それが、これらのマクロがノードによってどのように見えるかです。
+These macros are designed to be unambiguous and reversible, meaning that errors are reported in terms of de-sugared syntax. Below you’ll see these macros defined in terms of other syntactic forms. That is how these macros are seen by the node.
-<sub> <sub> <sub>?</sub> </sub>を比較する</sub>
+Compare <sub><sub><sub>~</sub></sub></sub>
-シンタックスシュガーは、<code> COMPARE </code>と比較コンビネータをマージするために、また分岐のために存在します。
+Syntactic sugar exists for merging <code>COMPARE</code> and comparison combinators, and also for branching.
-* <code> CMP {EQ | NEQ | LT | GT | LE | GE} </code>
+* <code>CMP{EQ|NEQ|LT|GT|LE|GE}</code>
 ::
-<pre>＆gt; CMP（\ op）/ S =＆gt; COMPARE; （\ op）/ S </pre>
+<pre>&gt; CMP(\op) / S  =&gt;  COMPARE ; (\op) / S</pre>
-* <code> IF {EQ | NEQ | LT | GT | LE | GE} bt bf </code>
+* <code>IF{EQ|NEQ|LT|GT|LE|GE} bt bf</code>
 ::
-<pre>＆gt; IF（\ op）bt bf / S =＆gt; （\ op）; IF bt bf / S </pre>
+<pre>&gt; IF(\op) bt bf / S  =&gt;  (\op) ; IF bt bf / S</pre>
-* <code> IFCMP {EQ | NEQ | LT | GT | LE | GE} bt bf </code>
+* <code>IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf</code>
 ::
-<pre>＆gt; IFCMP（\ op）/ S =＆gt; COMPARE; （\ op）; IF bt bf / S </pre>
+<pre>&gt; IFCMP(\op) / S  =&gt;  COMPARE ; (\op) ; IF bt bf / S</pre>
-アサーションマクロ?<sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub> / sub>
+Assertion Macros ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>
-すべてのアサーション演算は、適切な分岐で<code> FAIL </code>命令を持つ条件式の構文的砂糖です。可能であれば、それらを使用して違法状態についての明確性を高める。
+All assertion operations are syntactic sugar for conditionals with a <code>FAIL</code> instruction in the appropriate branch. When possible, use them to increase clarity about illegal states.
-* <code> ASSERT </code>：
+* <code>ASSERT</code>:
 ::
-<pre>＆gt; ASSERT =＆gt; IF {} {FAIL} </pre>
+<pre>&gt; ASSERT  =&gt;  IF {} {FAIL}</pre>
-* <code> ASSERT_ {EQ | NEQ | LT | LE | GT | GE} </code>：
+* <code>ASSERT_{EQ|NEQ|LT|LE|GT|GE}</code>:
 ::
-<pre>＆gt; ASSERT _（\ op）=＆gt; IF（\ op）{} {FAIL} </pre>
+<pre>&gt; ASSERT_(\op)  =&gt;  IF(\op) {} {FAIL}</pre>
-* <code> ASSERT_CMP {EQ | NEQ | LT | LE | GT | GE} </code>：
+* <code>ASSERT_CMP{EQ|NEQ|LT|LE|GT|GE}</code>:
 ::
-<pre>＆gt; ASSERT_CMP（\ op）=＆gt; IFCMP（\ op）{} {FAIL} </pre>
+<pre>&gt; ASSERT_CMP(\op)  =&gt;  IFCMP(\op) {} {FAIL}</pre>
-* <code> ASSERT_NONE </code>
+* <code>ASSERT_NONE</code>
 ::
-<pre>＆gt; ASSERT_NONE =＆gt; IF_NONE {} {FAIL} </pre>
+<pre>&gt; ASSERT_NONE  =&gt;  IF_NONE {} {FAIL}</pre>
-* <code> ASSERT_SOME </code>
+* <code>ASSERT_SOME</code>
 ::
-<pre>＆gt; ASSERT_SOME =＆gt; IF_SOME {FAIL} {} </pre>
+<pre>&gt; ASSERT_SOME  =&gt;  IF_SOME {FAIL} {}</pre>
-* <code> ASSERT_LEFT </code>：
+* <code>ASSERT_LEFT</code>:
 ::
-<pre>＆gt; ASSERT_LEFT =＆gt; IF_LEFT {} {FAIL} </pre>
+<pre>&gt; ASSERT_LEFT  =&gt;  IF_LEFT {} {FAIL}</pre>
-* <code> ASSERT_RIGHT </code>：
+* <code>ASSERT_RIGHT</code>:
 ::
-<pre>＆gt; ASSERT_RIGHT =＆gt; IF_LEFT {FAIL} {} </pre>
+<pre>&gt; ASSERT_RIGHT  =&gt;  IF_LEFT {FAIL} {}</pre>
-サブコンビネーション</sub> </sub>?<sub>?</sub> </sub>?
+Syntactic Conveniences <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~
-これらのマクロは、さまざまな一般的な操作に便利な構文です。
+These are macros are simply more convenient syntax for various common operations.
-* <code> DII + P code </code>：スタックの深いところで作業するための構文的砂糖。
+* <code>DII+P code</code>: A syntactic sugar for working deeper in the stack.
 ::
-<pre>＆gt; DII（\ rest = I *）Pコード/ S =＆gt; DIP（DI（\ rest）Pコード）/ S </pre>
+<pre>&gt; DII(\rest=I*)P code / S  =&gt;  DIP (DI(\rest)P code) / S</pre>
-* <code> DUU + P </code>：スタックの<code> n </code>番目の要素を複製するための構文的砂糖。
+* <code>DUU+P</code>: A syntactic sugar for duplicating the <code>n</code>?th element of the stack.
 ::
-<pre>＆gt; DUU（\ rest = U *）P / S =＆gt; DIP（DU（\ rest）P）; SWAP / S </pre>
+<pre>&gt; DUU(\rest=U*)P / S  =&gt;  DIP (DU(\rest)P) ; SWAP / S</pre>
-* <code> P（A * AI）+ R </code>：ネストされたペアを一括して構築するための構文的砂糖。
+* <code>P(A*AI)+R</code>: A syntactic sugar for building nested pairs in bulk.
 ::
-<pre>＆gt; P（\ fst = A *）AI（\ rest =（A * AI）+）R / S = P（\ fst）AIR; P（\ rest）R / S
-＆gt; PA（\ rest = A *）AIR / S =＆gt; DIP（P（\ rest）AIR）/ S </pre>
+<pre>&gt; P(\fst=A*)AI(\rest=(A*AI)+)R / S  =&gt;  P(\fst)AIR ; P(\rest)R / S
-* <code> C [AD] + R </code>：ネストされたペアのフィールドにアクセスするための構文的な砂糖。
+&gt; PA(\rest=A*)AIR / S  =&gt;  DIP (P(\rest)AIR) / S</pre>
+* <code>C[AD]+R</code>: A syntactic sugar for accessing fields in nested pairs.
 ::
-<pre>＆gt; CA（\ rest = [AD] +）R / S =＆gt;車 ; C（\ rest）R / S
+<pre>&gt; CA(\rest=[AD]+)R / S  =&gt;  CAR ; C(\rest)R / S
-＆gt; CD（\ rest = [AD] +）R / S =＆gt; CDR; C（\ rest）R / S </pre>
+&gt; CD(\rest=[AD]+)R / S  =&gt;  CDR ; C(\rest)R / S</pre>
-* <code> IF_SOME bt bf </code>：オプションの値を調べます。
+* <code>IF_SOME bt bf</code>: Inspect an optional value.
 ::
-<pre> ::オプション 'a：' S - ＆gt; 'b：' S
+<pre>:: option 'a : 'S   -&gt;   'b : 'S
-    iff bt :: ['a：' S - ＆gt; 'b：' S]
+    iff   bt :: [ 'a : 'S -&gt; 'b : 'S]
-          bf :: ['S - ＆gt; 'b：' S]
+          bf :: [ 'S -&gt; 'b : 'S]
-＆gt; IF_SOME /（Some a）：S =＆gt; bt / a：S
+&gt; IF_SOME / (Some a) : S  =&gt;  bt / a : S
-＆gt; IF_SOME /（なし）：S =＆gt; bf / S </pre>
+&gt; IF_SOME / (None) : S  =&gt;  bf / S</pre>
-* <code> SET_CAR </code>：ペアの最初の値を設定します。
+* <code>SET_CAR</code>: Set the first value of a pair.
 ::
-<pre>＆gt; SET_CAR =＆gt; CDR; SWAP; PAIR </pre>
+<pre>&gt; SET_CAR  =&gt;  CDR ; SWAP ; PAIR</pre>
-* <code> SET_CDR </code>：ペアの最初の値を設定します。
+* <code>SET_CDR</code>: Set the first value of a pair.
 ::
-<pre>＆gt; SET_CDR =＆gt;車 ; PAIR </pre>
+<pre>&gt; SET_CDR  =&gt;  CAR ; PAIR</pre>
-* <code> SET_C [AD] + R </code>：ネストされたペアのフィールドを設定するための構文的な砂糖です。
+* <code>SET_C[AD]+R</code>: A syntactic sugar for setting fields in nested pairs.
 ::
-<pre>＆gt; SET_CA（\ rest = [AD] +）R / S =＆gt;
+<pre>&gt; SET_CA(\rest=[AD]+)R / S   =&gt;
-     {DUP; DIP {CAR; SET_C（\ rest）R}; CDR; SWAP; PAIR} / S
+     { DUP ; DIP { CAR ; SET_C(\rest)R } ; CDR ; SWAP ; PAIR } / S
-＆gt; SET_CD（\ rest = [AD] +）R / S =＆gt;
+&gt; SET_CD(\rest=[AD]+)R / S   =&gt;
-     {DUP; DIP {CDR; SET_C（\ rest）R};車 ; PAIR} / S </pre>
+     { DUP ; DIP { CDR ; SET_C(\rest)R } ; CAR ; PAIR } / S</pre>
-* <code> MAP_CAR </code>コード：ペアの最初の値を変換します。
+* <code>MAP_CAR</code> code: Transform the first value of a pair.
 ::
-<pre>＆gt; MAP_CARコード=＆gt; DUP; CDR; SWAP;コード。車 ; PAIR </pre>
+<pre>&gt; MAP_CAR code  =&gt;  DUP ; CDR ; SWAP ; code ; CAR ; PAIR</pre>
-* <code> MAP_CDR </code>コード：ペアの最初の値を変換します。
+* <code>MAP_CDR</code> code: Transform the first value of a pair.
 ::
-<pre>＆gt; MAP_CDRコード=＆gt; DUP; CDR;コード。 SWAP;車 ; PAIR </pre>
+<pre>&gt; MAP_CDR code  =&gt;  DUP ; CDR ; code ; SWAP ; CAR ; PAIR</pre>
-* <code> MAP_C [AD] + R </code>コード：ネストしたペアのフィールドを変換するための構文的砂糖。
+* <code>MAP_C[AD]+R</code> code: A syntactic sugar for transforming fields in nested pairs.
 ::
-<pre>＆gt; MAP_CA（\ rest = [AD] +）R / S =＆gt;
+<pre>&gt; MAP_CA(\rest=[AD]+)R / S   =&gt;
-     {DUP; DIP {CAR; MAP_C（\ rest）Rコード}; CDR; SWAP; PAIR} / S
+     { DUP ; DIP { CAR ; MAP_C(\rest)R code } ; CDR ; SWAP ; PAIR } / S
-＆gt; MAP_CD（\ rest = [AD] +）R / S =＆gt;
+&gt; MAP_CD(\rest=[AD]+)R / S   =&gt;
-     {DUP; DIP {CDR; MAP_C（\ rest）Rコード};車 ; PAIR} / S </pre>
+     { DUP ; DIP { CDR ; MAP_C(\rest)R code } ; CAR ; PAIR } / S</pre>
-== IX - 具体的な構文==
+== IX - Concrete syntax ==
+The concrete language is very close to the formal notation of the specification. Its structure is extremely simple: an expression in the language can only be one of the four following constructs.
-具体的な言語は仕様の正式表記に非常に近い。その構造は非常に単純です：言語の式は、次の4つの構文のうちの1つに過ぎません。
+# An integer.
+# A character string.
+# The application of a primitive to a sequence of expressions.
+# A sequence of expressions.
-＃整数。
+This simple four cases notation is called Micheline.
-＃文字列。
-＃一連の式へのプリミティブの適用。
-＃一連の式。
-このシンプルな4つの表記法はMichelineと呼ばれています。
-定数<sub>?<sub>?</sub> </sub>?
+Constants <sub>~<sub>~</sub></sub>~
-定数には2種類あります。
+There are two kinds of constants:
-＃10進数（接頭辞なし）、16進数（0x接頭辞）、8進数（0接頭辞）またはバイナリ（0接頭辞）の整数または自然体。
+# Integers or naturals in decimal (no prefix), hexadecimal (0x prefix), octal (0o prefix) or binary (0b prefix).
-＃通常のエスケープ文字列\ n </code>、<code> \ t </code>、<code> \ b </code>、<code> \ r </code>、<コード> \ </code>、<code> \＆quot; </code>マイケルソンソースファイルのエンコーディングはUTF-8でなければならず、ASCII以外の文字はコメントにしか表示されません。文字列に改行を入れることはできません。印刷できない文字は、<code> \ xHH </code>や上記のエスケープシーケンスのように、2桁の16進文字を使用してエスケープする必要があります。
+# Strings with usual escapes <code>\n</code>, <code>\t</code>, <code>\b</code>, <code>\r</code>, <code>\\</code>, <code>\&quot;</code>. The encoding of a Michelson source file must be UTF-8, and non-ASCII characters can only appear in comments. No line break can appear in a string. Any non-printable characters must be escaped using two hexadecimal characters, as in <code>\xHH</code> or the predefine escape sequences above..
-プリミティブアプリケーション<sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub>?<sub>?</sub> </sub>?
+Primitive applications <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~
-基本的なアプリケーションは引数の後に続く名前です
+A primitive application is a name followed by arguments
 ::
-<pre> prim arg1 arg2 </pre>
+<pre>prim arg1 arg2</pre>
-プリミティブ・アプリケーションが別のプリミティブ・アプリケーションへの引数である場合、それはかっこでラップされなければなりません。
+When a primitive application is the argument to another primitive application, it must be wrapped with parentheses.
 ::
-<pre> prim（prim1 arg11 arg12）（prim2 arg21 arg22）</pre>
+<pre>prim (prim1 arg11 arg12) (prim2 arg21 arg22)</pre>
-シーケンス<sub>?<sub>?</sub> </sub>?
+Sequences <sub>~<sub>~</sub></sub>~
-逐次式は、区切り文字として中括弧を使用し、セパレータとしてセミコロンを使用する単一のシーケンス式としてグループ化できます。
+Successive expression can be grouped as a single sequence expression using curly braces as delimiters and semicolon as separators.
 ::
-<pre> {expr1; expr2; expr3; expr4} </pre>
+<pre>{ expr1 ; expr2 ; expr3 ; expr4 }</pre>
-シーケンスは、引数としてプリミティブに渡すことができます。
+A sequence can be passed as argument to a primitive.
 ::
-<pre>プリムarg1 arg2 {arg3_expr1; arg3_expr2} </pre>
+<pre>prim arg1 arg2 { arg3_expr1 ; arg3_expr2 }</pre>
-シーケンス内のプリミティブなアプリケーションは、ラップすることはできません。
+Primitive applications right inside a sequence cannot be wrapped.
 ::
-<pre> {（prim arg1 arg2）}＃は大丈夫です</pre>
-インデント<sub> <sub>?</sub> </sub> </sub>?<sub>?</sub>
-人間の読者のあいまいさを取り除くために、パーサーはいくつかのインデント規則を適用します。
+<pre>{ (prim arg1 arg2) } # is not ok</pre>
+Indentation <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>
+To remove ambiguities for human readers, the parser enforces some indentation rules.
-*シーケンスの場合：
+* For sequences:
-*シーケンス内のすべての式は、同じ列に配置する必要があります。
+* All expressions in a sequence must be aligned on the same column.
-*連続した式が最初に正しく整列されている限り、同じ行に収まる場合は例外が発生します。
+* An exception is made when consecutive expressions fit on the same line, as long as the first of them is correctly aligned.
-*シーケンス内のすべての式は、開始中括弧の右側に少なくとも1つの列だけインデントされている必要があります。
+* All expressions in a sequence must be indented to the right of the opening curly brace by at least one column.
-*中括弧は開き始めの左にはできません。
+* The closing curly brace cannot be on the left of the opening one.
-*原始的なアプリケーションの場合：
+* For primitive applications:
-*アプリケーション内のすべての引数は、同じ列に配置する必要があります。
+* All arguments in an application must be aligned on the same column.
-*連続した引数が最初の行が正しく整列されている限り、同じ行に収まる場合は例外が発生します。
+* An exception is made when consecutive arguments fit on the same line, as long as the first of them is correctly aligned.
-*シーケンス内のすべての引数は、少なくとも1つの列によってプリミティブ名の右に字下げする必要があります。
+* All arguments in a sequence must be indented to the right of the primitive name by at least one column.
-..注釈-1：
+.. _annotations-1:
-注釈<sub> <sub>?</sub> </sub> </sub>?<sub>?</sub>
+Annotations <sub><sub><sub>~</sub></sub></sub>~<sub>~</sub>
-シーケンスおよびプリミティブアプリケーションはアノテーションを受け取ることができます。
+Sequences and primitive applications can receive an annotation.
-アノテーションは、<code> @ </code>記号で始まる小文字の識別子です。それはシーケンスの開始中括弧の後に来て、プリミティブなアプリケーションのプリミティブな名前の後に来ます。
+An annotation is a lowercase identifier that starts with an <code>@</code> sign. It comes after the opening curly brace for sequence, and after the primitive name for primitive applications.
 ::
-<pre> {@annot
+<pre>{ @annot
-   expr;
+   expr ;
-   expr;
+   expr ;
-   ...}
+   ... }
-（prim @annot arg arg ...）</pre>
+(prim @annot arg arg ...)</pre>
-正式記法<sub> <sub> <sub>?</sub> </sub> <sub> <sub> <sub> <sub> <sub> <sub> <subとの相違点> <sub> </sub> </sub> </sub> </sub> </sub> </sub> </sub> </sub> </sub> > </sub>?<sub>?</sub>
+Differences with the formal notation <sub><sub><sub><sub>~</sub></sub></sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub>~<sub>~</sub>
-具体的な構文は、仕様と同じ字句規則に従います。命令は大文字の識別子で表され、型のコンストラクタは小文字の識別子で、定数のコンストラクタは大文字で表されます。
+The concrete syntax follows the same lexical conventions as the specification: instructions are represented by uppercase identifiers, type constructors by lowercase identifiers, and constant constructors are Capitalized.
-すべてのドメイン固有の定数は、特定の形式のMicheline文字列です。
+All domain specific constants are Micheline strings with specific formats:
-* <code> tez </code>の金額は、JSONスキーマやコマンドラインクライアントと同じ表記法を使って書かれています：千はオプションでカンマで区切られています。
+* <code>tez</code> amounts are written using the same notation as JSON schemas and the command line client: thousands are optionally separated by commas, and so goes for mutez.
-* [0-9] {1,3}（、[0-9] {3}）+）| [0-9] +（\。[0.9] {2}）？ </code>
+* in regexp form: <code>([0-9]{1,3}(,[0-9]{3})+)|[0-9]+(\.[0.9]{2})?</code>
-* <code> "1234567" </code>は1234567 tezを意味します
+* <code>&quot;1234567&quot;</code> means 1234567 tez
-* <code> "1,234,567" </code>は1234567 tezを意味します
+* <code>&quot;1,234,567&quot;</code> means 1234567 tez
-* <code> "1234567.89" </code>は1234567890000を意味します
+* <code>&quot;1234567.89&quot;</code> means 1234567890000 mutez
-* <code> "1,234,567.0" </code>は123456789 tezを意味します
+* <code>&quot;1,234,567.0&quot;</code> means 123456789 tez
-* <code> "10,123.456,789" </code>は10123456789を意味します
+* <code>&quot;10,123.456,789&quot;</code> means 10123456789 mutez
-* <code> "1234,567" </code>は無効です
+* <code>&quot;1234,567&quot;</code> is invalid
-* <code> "1,234,567.123456" </code>は無効です
+* <code>&quot;1,234,567.123456&quot;</code> is invalid
-* <code> timestamp </code>は<code> RFC 339 </code>表記を使って書かれています。
+* <code>timestamp</code>?s are written using <code>RFC 339</code> notation.
-* <code> contract </code>はJSON RPCやコマンドラインインターフェイスから返される生の文字列であり、手で偽造することはできません。
+* <code>contract</code>?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.
-* <code> key </code>は、<code> base58 </code>形式でエンコードされた<code> ed25519 </code>公開鍵の<code> Blake2B </code>コード> "eXMNE9qvHPQDdcFx5J86rT7VRm2atAypGhgLfbS3CKjnksB4" </code>である。
+* <code>key</code>?s are <code>Blake2B</code> hashes of <code>ed25519</code> public keys encoded in <code>base58</code> format with the following custom alphabet: <code>&quot;eXMNE9qvHPQDdcFx5J86rT7VRm2atAypGhgLfbS3CKjnksB4&quot;</code>.
-* <code> signature </code>は、16進数の一連のバイトとして<code> ed25519 </code>の署名です。
+* <code>signature</code>?s are <code>ed25519</code> signatures as a series of hex-encoded bytes.
-エラーを防ぐために、命令をパラメータとする制御フロープリミティブは、具体的な構文のシーケンスを必要とします。
+To prevent errors, control flow primitives that take instructions as parameters require sequences in the concrete syntax.
 ::
-<pre> IF {instr1_true; instr2_true; ...}
+<pre>IF { instr1_true ; instr2_true ; ... }
-    {instr1_false; instr2_false; ...} </pre>
+    { instr1_false ; instr2_false ; ... }</pre>
-メインプログラムの構造<sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub>?<sub>?</sub > </sub>?
+Main program structure <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~<sub>~</sub></sub>~
-スマートコントラクトファイルのトップレベルは、その<code>パラメータ</code>、<code> return </code>、および<code> storage </code>を提供する4つのプリミティブアプリケーション（特定の順序ではない） / code>型だけでなく、その<code> code </code>型も含みます。
+The toplevel of a smart contract file must be an un-delimited sequence of four primitive applications (in no particular order) that provide its <code>parameter</code>, <code>return</code> and <code>storage</code> types, as well as its <code>code</code>.
-具体的な例については、次のセクションを参照してください。
+See the next section for a concrete example.
-コメント?<sub> <sub> <sub>?</sub> </sub> </sub>
+Comments ~<sub><sub><sub>~</sub></sub></sub>
-文字列リテラルの外側の任意の場所にあるハッシュ記号（<code>＃</code>）は、次の例のように、残りの行（およびそれ自身）を完全に無視します。
+A hash sign (<code>#</code>) anywhere outside of a string literal will make the rest of the line (and itself) completely ignored, as in the following example.
 ::
-<pre> {PUSH nat 1; ＃プッシュ1
+<pre>{ PUSH nat 1 ; # pushes 1
-   プッシュナット2; ＃プッシュ2
+   PUSH nat 2 ; # pushes 2
-   ADD}＃は2 + 1を計算する</pre>
+   ADD }        # computes 2 + 1</pre>
-Cのような区切り文字（<code> / * ... * / </code>）を使用して、複数の行にまたがる行または行の終わりの前に停止するコメントも記述できます。
+Comments that span on multiple lines or that stop before the end of the line can also be written, using C-like delimiters (<code>/* ... */</code>).
-== X - JSON構文==
+== X - JSON syntax ==
-ミシェリンの式はJSONで次のようにコード化されています：
+Micheline expressions are encoded in JSON like this:
-*整数<code> N </code>は、valusが文字列としての10進表現である<code> "int" </code>という単一フィールドを持つオブジェクトです。
+* An integer <code>N</code> is an object with a single field <code>&quot;int&quot;</code> whose valus is the decimal representation as a string.
-<code> {"int"： "N" } </code>
+<code>{ &quot;int&quot;: &quot;N&quot; }</code>
-*文字列<code> "contents" </code>は、valusが文字列としての10進表現である<code> "string" </code>という単一フィールドを持つオブジェクトです。
+* A string <code>&quot;contents&quot;</code> is an object with a single field <code>&quot;string&quot;</code> whose valus is the decimal representation as a string.
-<code> {＆quot; string＆quot;：＆quot; contents＆quot; } </code>
+<code>{ &quot;string&quot;: &quot;contents&quot; }</code>
-*シーケンスはJSON配列です。
+* A sequence is a JSON array.
-<code> [expr、...] </code>
+<code>[ expr, ... ]</code>
-*プリミティブアプリケーションは、プリミティブ名の2つのフィールド<code> "prim" </code>と引数（配列を含む必要がある）の<code> "args" </code>という2つのフィールドを持つオブジェクトです。第3のオプションフィールド<code> "annot" </code>は、<code> @ </code>記号を含むアノテーションを含むことができる。
+* A primitive application is an object with two fields <code>&quot;prim&quot;</code> for the primitive name and <code>&quot;args&quot;</code> for the arguments (that must contain an array). A third optionnal field <code>&quot;annot&quot;</code> may contains an annotation, including the <code>@</code> sign.
-{"prim"： "pair"、 "args"：[{"prim"： "nat"、args：[]}、{"prim"： "nat"、args：[]}]、 "annot" @numbers "}`
+{ “prim”: “pair”, “args”: [ { “prim”: “nat”, args: [] }, { “prim”: “nat”, args: [] } ], “annot”: “@numbers” }`
-具体的な構文と同様に、すべてのドメイン固有の定数は文字列としてエンコードされます。
+As in the concrete syntax, all domain specific constants are encoded as strings.
-== XI - 例==
+== XI - Examples ==
-システム内の契約は、コードとグローバルデータストレージとして保存されます。ストレージのグローバルデータのタイプは、開始時に契約ごとに固定されます。これは、コードがグローバルデータのタイプを保持することを発信元でチェックすることによって、静的に保証されます。このため、契約のコードは<code> lambda（pair 'arg' global）型であるとチェックされます。 （pair 'ret' global）</code> <code> 'global </code>は、発信時に指定された元のグローバルストアのタイプです。契約はパラメータをとり、値を返します。したがって、上記の完全な呼び出し規約。
+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 type <code>lambda (pair ’arg ’global) -&gt; (pair ’ret ’global)</code> where <code>’global</code> is the type of the original global store given on origination. The contract also takes a parameter and returns a value, hence the complete calling convention above.
-空の契約</sub> </sub> </sub>
+Empty contract <sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub>~
-同じ<code>パラメータ</code>および<code> return </code>タイプの契約は、<code> code </code>セクションに空のシーケンスで書き込むことができます。最も単純な契約は、<code>パラメータ</code>、<code> storage </code>、および<code> return </code>がすべて<code> unit </code>型の契約です。この契約は次のとおりです。
+Any contract with the same <code>parameter</code> and <code>return</code> types may be written with an empty sequence in its <code>code</code> section. The simplest contract is the contract for which the <code>parameter</code>, <code>storage</code>, and <code>return</code> are all of type <code>unit</code>. This contract is as follows:
 ::
-<pre>コード{};
-記憶装置;
-パラメータ単位。
-戻り単位; </pre>
-貯水池契約<sub> <sub>?</sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> ~~
-タイムスタンプ<code> T </code>または最大量<code> N </code>に達するまでtezを保存する契約を作成したいとします。 <code> T </code>の前に<code> N </code>に達すると、すべてのトークンが<code> B </code>というアカウントに逆転され（契約は自動的に削除されます）。 <code> T </code>の後に実行される契約コードへの呼び出しは、トークンを別のアカウント<code> A </code>に転送します。
+<pre>code {};
+storage unit;
+parameter unit;
+return unit;</pre>
+Reservoir contract <sub><sub>~</sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub>~~
-この契約を再利用可能な方法で構築したいので、パラメータをハードコードしません。代わりに、契約のグローバルデータは<code>（Pair（ペアT N）（ペアA B））</code>であると仮定します。
+We want to create a contract that stores tez until a timestamp <code>T</code> or a maximum amount <code>N</code> is reached. Whenever <code>N</code> is reached before <code>T</code>, all tokens are reversed to an account <code>B</code> (and the contract is automatically deleted). Any call to the contract’s code performed after <code>T</code> will otherwise transfer the tokens to another account <code>A</code>.
-したがって、契約のグローバルデータは以下のタイプ
+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 <code>(Pair (Pair T N) (Pair A B))</code>.
+Hence, the global data of the contract has the following type
 ::
-<pre> 'g =
+<pre>'g =
-   ペア
+   pair
-     （ペアタイムスタンプtez）
+     (pair timestamp tez)
-     （ペア（契約単位単位）（契約単位単位））</pre>
+     (pair (contract unit unit) (contract unit unit))</pre>
-契約呼び出し規約に従い、コードはラムダ型です
+Following the contract calling convention, the code is a lambda of type
 ::
-<前>ラムダ
+<pre>lambda
-   （ペア単位 'g）
+   (pair unit 'g)
-   （ペア単位 'g）</pre>
+   (pair unit 'g)</pre>
-として書かれている
+written as
 ::
-<前>ラムダ
+<pre>lambda
-   （ペア
+   (pair
-      単位
+      unit
-      （ペア
+      (pair
-        （ペアタイムスタンプtez）
+        (pair timestamp tez)
-        （ペア（契約単位単位）（契約単位単位））））
+        (pair (contract unit unit) (contract unit unit))))
-   （ペア
+   (pair
-      単位
+      unit
-      （ペア
+      (pair
-         （ペアタイムスタンプtez）
+         (pair timestamp tez)
-         （ペア（契約単位単位）（契約単位単位））））</pre>
+         (pair (contract unit unit) (contract unit unit))))</pre>
-完全なソース<code> reservoir.tz </code>は次のとおりです：
+The complete source <code>reservoir.tz</code> is:
 ::
-<pre>パラメータのタイムスタンプ。
+<pre>parameter timestamp ;
-ストレージ
+storage
-   （ペア
+   (pair
-      （ペアタイムスタンプtez）＃T N
+      (pair timestamp tez) # T N
-      （ペア（契約単位単位）（契約単位単位）））; ＃A B
+      (pair (contract unit unit) (contract unit unit))) ; # A B
-戻り単位;
+return unit ;
-コード
+code
-   {DUP; CDAAR; ＃T
+   { DUP ; CDAAR ; # T
-     NOW;
+     NOW ;
-     COMPARE; LE;
+     COMPARE ; LE ;
-     IF {DUP; CDADR; ＃N
+     IF { DUP ; CDADR ; # N
-          バランス。
+          BALANCE ;
-          COMPARE; LE;
+          COMPARE ; LE ;
-          IF {CDR;単位 ; PAIR}
+          IF { CDR ; UNIT ; PAIR }
-             {DUP; CDDDR; ＃B
+             { DUP ; CDDDR ; # B
-               バランス。単位 ;
+               BALANCE ; UNIT ;
-               DIIIP {CDR};
+               DIIIP { CDR } ;
-               TRANSFER_TOKENS;
+               TRANSFER_TOKENS ;
-               PAIR}}
+               PAIR } }
-        {DUP; CDDAR; ＃A
+        { DUP ; CDDAR ; # A
-          バランス。
+          BALANCE ;
-          単位 ;
+          UNIT ;
-          DIIIP {CDR};
+          DIIIP { CDR } ;
-          TRANSFER_TOKENS;
+          TRANSFER_TOKENS ;
-          PAIR}} </pre>
+          PAIR } }</pre>
-リザーブ契約（ブローカーとステータスが異なるバリアント）<sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub> <sub > </sub> </sub> </sub> </sub> </sub> </sub> </sub> / sub> </sub> </sub> </sub> </sub> </sub> </sub> / sub> </sub> </sub>?</sub>
+Reservoir contract (variant with broker and status) <sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub></sub><sub><sub><sub>~</sub></sub></sub>~</sub>
-基本的には前回と同じ契約が必要ですが、破棄するのではなく、トークンが<code>に転送されたかどうかを知るために<code> S </code>フラグを保存して、 > A </code>または<code> B </code>をクリックします。いずれにしても、ブローカー<code> X </code>にはある程度の手数料<code> P </code>が必要です。
+We basically want the same contract as the previous one, but instead of destroying it, we want to keep it alive, storing a flag <code>S</code> so that we can tell afterwards if the tokens have been transferred to <code>A</code> or <code>B</code>. We also want a broker <code>X</code> to get some fee <code>P</code> in any case.
-したがって、契約のグローバルデータに<code> P </code>と<code> S </code>と<code> X </code>という変数を追加します（Pair（S、Pair（T 、ペア（ペアPN）（ペアX（ペアAB）））））</code> <code> S </code>はブローカ<code> A </code>の料金であり、<code> S </code>は文字列<code> "open" </code> code>＆quot;タイムアウト＆quot; </code>または<code>＆quot; success＆quot; </code>
+We thus add variables <code>P</code> and <code>S</code> and <code>X</code> to the global data of the contract, now <code>(Pair (S, Pair (T, Pair (Pair P N) (Pair X (Pair A B)))))</code>. <code>P</code> is the fee for broker <code>A</code>, <code>S</code> is the state, as a string <code>&quot;open&quot;</code>, <code>&quot;timeout&quot;</code> or <code>&quot;success&quot;</code>.
-トランザクションの開始時に：
+At the beginning of the transaction:
 ::
-<pre> SはCDAR経由でアクセス可能
+<pre> S is accessible via a CDAR
-  CDDARを介してT
+  T               via a CDDAR
-  CDDDAARを介してP
+  P               via a CDDDAAR
-  CDDDADRを介してN
+  N               via a CDDDADR
-  CDDDDARを介してX
+  X               via a CDDDDAR
-  CDDDDDAR経由で
+  A               via a CDDDDDAR
-  CDDDDDDR経由でB </pre>
+  B               via a CDDDDDDR</pre>
-契約を有効にするために、トランザクションごとに少なくとも<code>（Tez "1.00"）</code>が利用可能であることをテストします。この値は一例として示されており、契約残高の実際のTezos最小値に従って更新する必要があります。
+For the contract to stay alive, we test that all least <code>(Tez &quot;1.00&quot;)</code> is still available after each transaction. This value is given as an example and must be updated according to the actual Tezos minimal value for contract balance.
-完全なソース<code> scrutable_reservoir.tz </code>は次のとおりです：
+The complete source <code>scrutable_reservoir.tz</code> is:
 ::
-<pre>パラメータのタイムスタンプ。
-ストレージ
-  （ペア
-     文字列＃S
-     （ペア
-        タイムスタンプ＃T
-        （ペア
-           （ペアtez tez）; ＃P N
-           （ペア
-              （契約単位）＃X
-              （ペア（契約単位単位）（契約単位単位）））））））））; ＃A B
-戻り単位;
-コード
-  {DUP; CDAR＃S
-    PUSH文字列 "open" ;
-    COMPARE; NEQ;
-    IF {FAIL}＃が「成功」、「タイムアウト」、または不正な初期値
-       {DUP; CDDAR; ＃T
-         NOW;
-         COMPARE; LT;
-         IF {＃タイムアウト前
-              ＃私たちは（1 + P）+ N）tezを計算して、契約を生かしておく
-              PUSH tez "1.00" ;
-              DIP {DUP; CDDDAAR}; ADD; #P
-              DIP {DUP; CDDDADR}; ADD; ＃N
-              ＃累積金額と比較します
-              バランス。
-              COMPARE; LT;
-              IF {＃現金が足りない場合は、取引を受け入れるだけです
-                   ＃グローバルなままにしておく
-                   CDR}
-                 {＃十分な現金、成功した終了
-                   ＃グローバルを更新する
-                   CDDR;プッシュ文字列 "success" ; PAIR;
-                   ＃私たちはブローカーに手数料を譲渡します
-                   DUP; CDDAAR; #P
-                   DIP {DUP; CDDDAR}＃X
-                   単位 ; TRANSFER_TOKENS;ドロップ ;
-                   ＃残りはAに転送されます
-                   DUP; CDDADR; ＃N
-                   DIP {DUP; CDDDDAR}＃A
-                   単位 ; TRANSFER_TOKENS;ドロップ } }
-            {＃タイムアウト後、私たちは払い戻します
-              ＃グローバルを更新する
-              CDDR;プッシュ文字列「タイムアウト」は、 ; PAIR;
-              ＃私たちはブローカーに料金を移そうとします
-              PUSH tez "1.00" ;バランス。サブ ; ＃利用可能
-              DIP {DUP; CDDAAR}; #P
-              COMPARE; LT; ＃利用可能＆lt; P
-              IF {PUSH tez "1.00" ;バランス。サブ ; ＃利用可能
-                   DIP {DUP; CDDDAR}＃X
-                   単位 ; TRANSFER_TOKENS;ドロップ }
-                 {DUP; CDDAAR; #P
-                   DIP {DUP; CDDDAR}＃X
-                   単位 ; TRANSFER_TOKENS;ドロップ }
-              ＃残りをBに転送する
-              PUSH tez "1.00" ;バランス。サブ ; ＃利用可能
-              DIP {DUP; CDDDDDR}＃B
-              単位 ; TRANSFER_TOKENS;ドロップ } }
-    ＃戻り単位
-    単位 ; PAIR} </pre>
-フォワード契約?<sub> <sub> <sub> <sub> <sub> <sub>?</sub> </sub> </sub> </sub> </sub> / sub>
-我々は、乾燥エンドウ豆に先渡契約を結びたいと思っています。この契約では、大量のエンドウ豆の<code> Q </code>、予想配送日<code> T </code>、契約締結日<code> Z </code>、ストライキ<code>乾燥エンドウ豆1トンあたりの担保<code> C </code>、買い手<code> B </code>、売り手<code> S </code>、倉庫<code> W </code>。
-これらのパラメータは、グローバルストレージに次のようにグループ化されています。
+<pre>parameter timestamp ;
+storage
+  (pair
+     string # S
+     (pair
+        timestamp # T
+        (pair
+           (pair tez tez) ; # P N
+           (pair
+              (contract unit unit) # X
+              (pair (contract unit unit) (contract unit unit)))))) ; # A B
+return unit ;
+code
+  { DUP ; CDAR # S
+    PUSH string &quot;open&quot; ;
+    COMPARE ; NEQ ;
+    IF { FAIL } # on &quot;success&quot;, &quot;timeout&quot; 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 &quot;1.00&quot; ;
+              DIP { DUP ; CDDDAAR } ; ADD ; # P
+              DIP { DUP ; CDDDADR } ; ADD ; # N
+              # We compare to the cumulated amount
+              BALANCE ;
+              COMPARE; LT ;
+              IF { # Not enough cash, we just accept the transaction
+                   # and leave the global untouched
+                   CDR }
+                 { # Enough cash, successful ending
+                   # We update the global
+                   CDDR ; PUSH string &quot;success&quot; ; PAIR ;
+                   # We transfer the fee to the broker
+                   DUP ; CDDAAR ; # P
+                   DIP { DUP ; CDDDAR } # X
+                   UNIT ; TRANSFER_TOKENS ; DROP ;
+                   # We transfer the rest to A
+                   DUP ; CDDADR ; # N
+                   DIP { DUP ; CDDDDAR } # A
+                   UNIT ; TRANSFER_TOKENS ; DROP } }
+            { # After timeout, we refund
+              # We update the global
+              CDDR ; PUSH string &quot;timeout&quot; ; PAIR ;
+              # We try to transfer the fee to the broker
+              PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
+              DIP { DUP ; CDDAAR } ; # P
+              COMPARE ; LT ; # available &lt; P
+              IF { PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
+                   DIP { DUP ; CDDDAR } # X
+                   UNIT ; TRANSFER_TOKENS ; DROP }
+                 { DUP ; CDDAAR ; # P
+                   DIP { DUP ; CDDDAR } # X
+                   UNIT ; TRANSFER_TOKENS ; DROP }
+              # We transfer the rest to B
+              PUSH tez &quot;1.00&quot; ; BALANCE ; SUB ; # available
+              DIP { DUP ; CDDDDDR } # B
+              UNIT ; TRANSFER_TOKENS ; DROP } }
+    # return Unit
+    UNIT ; PAIR }</pre>
+Forward contract ~<sub><sub><sub><sub><sub><sub><sub>~</sub></sub></sub></sub></sub></sub></sub>
+We want to write a forward contract on dried peas. The contract takes as global data the tons of peas <code>Q</code>, the expected delivery date <code>T</code>, the contract agreement date <code>Z</code>, a strike <code>K</code>, a collateral <code>C</code> per ton of dried peas, and the accounts of the buyer <code>B</code>, the seller <code>S</code> and the warehouse <code>W</code>.
+These parameters as grouped in the global storage as follows:
 ::
-<ペア>ペア
+<pre>Pair
-   （ペア（ペアQ（ペアT Z）））
+   (Pair (Pair Q (Pair T Z)))
-   （ペア
+   (Pair
-      （対K C）
+      (Pair K C)
-      （ペア（ペアB S）W））</pre>
+      (Pair (Pair B S) W))</pre>
-タイプの
+of type
 ::
-<pre>ペア
+<pre>pair
-   （ペアナット（ペアタイムスタンプタイムスタンプ））
+   (pair nat (pair timestamp timestamp))
-   （ペア
+   (pair
-      （ペアtez tez）
+      (pair tez tez)
-      （ペアアカウントアカウント））</pre>
+      (pair (pair account account) account))</pre>
-タイムスタンプ<code> Z </code>の24時間後に、買い手と売り手が担保<code>（Q * C）</code>を保存します。このため、契約では、トークンが転送される相手を示す<code> "buyer" </code>または<code> "seller" </code>と一致する文字列をパラメータとして使用します。この日の終わりには、それぞれがトランザクションを送信してトークンを送り返すことができます。そのためには、左のコンポーネントがバイヤーであり、右のコンポーネントが売り手である<code>（ペアtez tez）</code>として、既に支払った人とその額を保存する必要があります。
+The 24 hours after timestamp <code>Z</code> are for the buyer and seller to store their collateral <code>(Q * C)</code>. For this, the contract takes a string as parameter, matching <code>&quot;buyer&quot;</code> or <code>&quot;seller&quot;</code> indicating the party for which the tokens are transferred. 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 <code>(pair tez tez)</code> where the left component is the buyer and the right one the seller.
-最初の日の後、<code> T </code>までカムは何も起こりません。
+After the first day, nothing cam happen until <code>T</code>.
-<code> T </code>の24時間後に、買い手は契約に（<code>（Q * K）</code>）支払った金額を支払う必要があります。
+During the 24 hours after <code>T</code>, the buyer must pay <code>(Q * K)</code> 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.
-それ以外の場合、売り手は24時間以内に少なくとも<code> Q </code>トンの乾燥エンドウ豆を倉庫に配送する必要があります。金額が<code> Q </code>以上であれば、すべてのトークンが売り手に転送され、契約は破棄されます。すでに配信されたエンドウ豆の量を保存するために、グローバルストレージに<code> nat </code>タイプのカウンタを追加します。この量を知るために、私たちは引数としてエンドウ豆の部分量でWからのメッセージを受け取ります。
+Otherwise, the seller must deliver at least <code>Q</code> tons of dried peas to the warehouse, in the next 24 hours. When the amount is equal to or exceeds <code>Q</code>, all the tokens are transferred to the seller and the contract is destroyed. For storing the quantity of peas already delivered, we add a counter of type <code>nat</code> 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.
 ::
-<ペア>ペア
+<pre>Pair
-   （ペア0（ペア0_00 0_00））
+   (Pair 0 (Pair 0_00 0_00))
-   （ペア
+   (Pair
-      （ペア（ペアQ（ペアT Z）））
+      (Pair (Pair Q (Pair T Z)))
-      （ペア
+      (Pair
-         （対K C）
+         (Pair K C)
-         （ペア（ペアB S）W）））</pre>
+         (Pair (Pair B S) W)))</pre>
-タイプの
+of type
 ::
-<pre>ペア
+<pre>pair
-   （pair nat（pair tez tez））
+   (pair nat (pair tez tez))
-   （ペア
+   (pair
-      （ペアナット（ペアタイムスタンプタイムスタンプ））
+      (pair nat (pair timestamp timestamp))
-      （ペア
+      (pair
-         （ペアtez tez）
+         (pair tez tez)
-         （ペアアカウントアカウント））））</pre>
+         (pair (pair account account) account)))</pre>
-トランザクションのパラメータは、買い手または売り手からの転送か、タイプ<code>（または文字列nat）</code>の倉庫からの配送通知です。
+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 <code>(or string nat)</code>.
-トランザクションの開始時に：
+At the beginning of the transaction:
 ::
-<pre> QはCDDAARを介してアクセス可能です
+<pre>Q is accessible via a CDDAAR
-CDDADARを介してT
+T               via a CDDADAR
-CDDADDRを介してZ
+Z               via a CDDADDR
-CDDDAARを介してK
+K               via a CDDDAAR
-CDDDADRを介してC
+C               via a CDDDADR
-B CDDDDAARを介して
+B               via a CDDDDAAR
-CDDDDADRを介してS
+S               via a CDDDDADR
-CDDDDDRを介してW
+W               via a CDDDDDR
-CDAARを介した配送カウンタ
+the delivery counter via a CDAAR
-CDADDRを介して売り手が精通した金額
+the amount versed by the seller via a CDADDR
-CARを介した引数</pre>
+the argument via a CAR</pre>
-コントラクトは単価を返し、<code>（Tez "1.00"）</code>に設定された最小金額で作成されたものとみなします。
+The contract returns a unit value, and we assume that it is created with the minimum amount, set to <code>(Tez &quot;1.00&quot;)</code>.
-完全なソース<code> forward.tz </code>は次のとおりです：
+The complete source <code>forward.tz</code> is:
 ::
 <pre>parameter (or string nat) ;
 return unit ;
@@ 1,878行目: / 1,899行目: @@
    | key_hash
    | timestamp</pre>
-== XIII - リファレンス実装==
+== XIII - Reference implementation ==
-言語はOCamlで次のように実装されています：
+The language is implemented in OCaml as follows:
-*下位の内部表現は、型パラメータがこの仕様で与えられた型付け規則を正確に符号化するGADTとして記述されています。言い換えれば、この表現で書かれたプログラムがOCamlの型検査器によって受け入れられるなら、それは強制的に型安全です。これはもちろん、手書きではなくOCamlコードで生成されたプログラムにも有効です。したがって、操作されたコードは型保証されていると確信しています。
+* 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.
-結局、チェックされるべきことは、各命令のコード行の半分になるOCaml型として型定義規則をコード化することです。他のすべては、由緒ある、信頼できるOCamlに委ねられています。
+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.
-*インタプリタは、基本的に上記の書き換え規則の直接転写です。それは命令、スタックを取り、それを変換する。 OCamlの型検査器は、各命令のGADTケースで宣言されたプリスタック型とポストスタック型の変換を確実に行います。
+* 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.
-ここでは、If命令を解釈するときにTrueとFalseを入れ替えないなど、値に依存する選択肢のみを検討しました。
+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.
-<code> String </code>、<code> Int </code>、<code> Seq </code>、および<code> Prim </code>の5つの文法構造を持つOCaml ADTです。 / code>すべての解析可能なプログラムが型付けされているわけではないので、GADTを使用して単純に構築することはできないため、パーサのターゲット言語です。
+* The input, untyped internal representation is an OCaml ADT with the only 5 grammar constructions: <code>String</code>, <code>Int</code>, <code>Seq</code> and <code>Prim</code>. 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.
-*型チェッカーは、パターンマッチングによってセクションXで説明した抽象文法を認識し、適切に型付けされた対応するGADT式を生成する単純な関数です。これは主に完全なインプラタではなくチェッカーであるため、いくつかの注釈（基本的にプログラムの入力と出力、ラムダと初期化されていないマップとセット）の入力が必要です。プログラムのシンボリック評価を行い、シンボリックスタックを変換することで動作します。プログラム全体に1回のパスが必要です。
+* 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 input and output of the program, of lambdas and of uninitialized maps and sets). It works by performing a symbolic evaluation of the program, transforming a symbolic stack. It only needs one pass over the whole program.
-ここでもOCamlはほとんどのチェックを行いますが、関数の構造は非常に単純です。チェックする必要があるのは、<code> Prim（ "If"、...）</code>を< <code> If </code>の場合は、<code> Dup </code>などの<code> Prim（ "Dup"、...）</code>
+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 <code>Prim (&quot;If&quot;, ...)</code> into an <code>If</code>, a <code>Prim (&quot;Dup&quot;, ...)</code> into a <code>Dup</code>, etc.