Michelson Reference

Introduction ¶

This is a reference manual of the Michelson language used for smart contract programming for the Tezos blockchain. It contains a reference of the types and instructions of the language. For more information about the Michelson language, such as its design rationale and how it fits in the blockchain, deprecated instructions, macros, and other aspects, see the Michelson language page in the Tezos technical documentation.

The simplest contract is the contract for which the parameter and storage are all of type unit. This empty contract is as follows:

try it!

parameter unit;
storage unit;
code {CDR; NIL operation; PAIR};

The examples used throughout the reference can be executed in the browser using the Try Michelson interpreter. Just click "try it!" in the upper-right corner of the example to load it in the interpeter.

In addition, the stack type of each location of the examples can be displayed by hovering the mouse over that location.

Execution environment ¶

A well-typed Michelson program implements a function which transforms a pair of Michelson values representing the transaction parameter and the contract storage, and returns a pair containing a list of internal operations and the new storage. Some Michelson instructions make implicit use of data from an execution environment, derived from the current state of the blockchain (the context), from the transaction that triggered the contract, and from the block containing this transaction. These instructions are categorized under blockchain operations.

Terminology ¶

Instruction: Instructions refer to Michelson primitives such as ADD. Not to be confused with operations.
Operation: The final stack after a contract execution is a pair containing a new storage and a list of operations. An operation is either a transfer, an account creation, a delegation or the emission of an event.
Numerical type: Refers to any of the numerical types of Michelson: int, nat, timestamp or mutez. Numerical values are values of one these types.
Sequence type: Refers to any of the two sequence types of Michelson: string or bytes.
Structural type: Refers to any of the structural types of Michelson: list, set, map or big_map. Structural values are values of one these types.
Argument: Michelson instructions may be indexed by arguments. For instance, the arguments of PUSH nat 3 are nat and 3. The argument of DIP 2 is 2. Not to be confused with operands and parameters.
Operand: Refers to stack values consumed by instructions. Not to be confused with arguments and parameters.
Parameter: Parameter may refer to three things. First, each contract has a parameter type and when called, takes a parameter value of this type. Second, some Michelson data types, such as list are parametric. For instance, a list of integer list nat is an instance of the list type with the type parameter instantiated to nat. Finally, the input type of a lambda. Not to be confused with arguments and operands.
Return value: Refers either to the stack values produced by an instruction, or the return value of a lambda.
Transaction: The execution of a contract is triggered by a blockchain operation called a transaction, which is part of a block. A transaction has parameters which are made available to the contracts in two different ways. The argument of the transaction (a Michelson value) is passed to the contract as the right side of a pair value, the only element in the initial stack. Other parameters of the transaction (such as its amount, the implicit account or contract that triggered it), and data from the block containing the transaction (its timestamp) can be accessed by specific instructions.
Context: The context is a value representing the state of the blockchain after the application of an operation. A contract execution may access data from the context over which the execution is triggered. It has access to the previous storage of the contract as the left side of a pair value, the only element in the initial stack. Besides, some instructions use or extract information from the context (current contract balance, contracts type).
Storage: The storage of a contract is a Michelson value that represents it state. Initial storage is provided at contract deployement (a.k.a. origination). Subsequently, transactions trigger contract execution, in which a new store is computed, based notably on the previous storage and the transaction argument.

Typing and Semantics Rules ¶

Michelson is a strongly typed language, which greatly participates in its safety.
A type-checking process forbids any Michelson script to be registered on the blockchain if one of its instructions does not operate on operands and a stack of the expected types.

In the Instructions section, the description of an instruction will always come with typing rules characterizing the typing conditions that its operands and the stack must satisfy before applying the instruction, and the resulting stack type after the execution of the instruction.
Semantics rules will also precisely specify the values manipulated by the instruction and its result.

Typing as well as semantics rules have the following form:

condition₁

...

condition_n

conclusion

rule_name

which means that when condition₁, ..., and condition_n are fulfilled, then conclusion holds. As expected, rule_name is the name of the rule. What is expressed in the conditions and in the conclusion depends on whether it is a typing or a semantics rule.

Typing Rules ¶

The typing rules borrow the concept of judgement, which is a notation found in logic to concisely express a proposition under some hypotheses, also called the environment. The general form of judgement when typing Michelson instructions is Γ ⊢ instr :: A ⇒ B, which can be read as follows: under the typing environment Γ, the Michelson instruction instr expects a stack of type A, and transforms it into a stack of type B. A stack type is a sequence of types, where the leftmost type of the sequence is the type for the top value of the stack.

The conditions of a typing rule are usually judgements (but not always, they can be any kind of mathematical condition), and the conclusion is also a judgement.

For instance, the IF rule below:

Γ ⊢ instr₁ :: A ⇒ B

Γ ⊢ instr₂ :: A ⇒ B

Γ ⊢ IF   instr₁   instr₂ :: bool : A ⇒ B

means that under a typing environment Γ, if both the instr₁ and instr₂ Michelson instructions expect a stack of type A and return a stack of type B, then the IF instr₁ instr₂ instruction expects a stack of type bool : A and returns a stack of type B. The intent behind the values of type bool, A and B is not expressed in a typing rule, it is the purpose of the semantics rule.

Semantics Rules ¶

Semantics rules rely on a synctactic convention, whose general form is i / S ⇒ S′, and which means that when applying the instruction i on the stack S, the result is the stack S′.

As for typing rules, the conditions of a semantics rule are usually of the above form (but not always, they can be any kind of mathematical condition), and the conclusion also follows this syntax.

For instance, consider the two rules below:

i₁ / S ⇒ S′

IF   i₁   i₂ / True : S ⇒ S′

IF__tt

i₂ / S ⇒ S′

IF   i₁   i₂ / False : S ⇒ S′

IF__ff

IF__tt means that the result of executing IF i₁ i₂ on the stack True : S is exactly the result of executing i₁ on S.
And similarly, IF__ff means that the result of executing IF i₁ i₂ on the stack False : S is exactly the result of executing i₂ on S.

Types ¶

Michelson data types (and by extension, the values of each type) can be characterized by the following type attributes:

Comparable (C): Comparable values can be stored in sets, can be passed as argument to COMPARE, etc.
Passable (PM): Passable types can be used as a parameter in contracts.
Storable (S): Storable types can be used as a storage in contracts.
Pushable (PU): Literal values of pushable types can be used as the parameter of the PUSH primitive.
Packable (PA): Values of packable types can be serialized using the PACK primitive, and can be emitted using the EMIT primitive.
big_map value (B): big_map values can be stored as values in big_maps.
Duplicable (D): Literal values of duplicable types can be used as the parameter of the DUP primitive.

For compound types, the value of an attribute may depend on the value of the same attribute on subtypes. For example, the type

map kty
vty

is never comparable and it is storable exactly when vty is storable. The following table documents the value of all type attributes for all Michelson types; ✔ means that the attribute always holds for the given type, ✘ means that the attribute never holds for the given type, and ty_1...ty_n means that the attribute holds exactly when the attribute holds for all the ty_i subtypes. The attributes of each type are given in the table below. ¶

Type	Description	Examples	C	PM	S	PU	PA	B	D
`address`	Address of an untyped contract	`"KT1ThEdxfUcWUwqsdergy...` , `"KT1BEqzn5Wx8uJrZNvuS9...` , `"tz1KqTpEZ7Yob7QbPE4Hy...` , `"tz2VGBaXuS6rnaa5hpC92...` , `"tz3WEJYwJ6pPwVbSL8FrS...`	✔	✔	✔	✔	✔	✔	✔
`big_map kty vty`	A lazily deserialized map from `kty` to `vty`	`{}` , `{ Elt 0 0xCB ; Elt 1 0...`	✘	`vty`	`vty`	✘	✘	✘	`vty`
`bls12_381_fr`	An element of the BLS12-381 scalar field F_r	`0` , `1` , `0x01` , `0x0001`	✘	✔	✔	✔	✔	✔	✔
`bls12_381_g1`	A point on the BLS12-381 curve G₁	`0x0572cbea904d67468808...`	✘	✔	✔	✔	✔	✔	✔
`bls12_381_g2`	A point on the BLS12-381 curve G₂	`0x0a4edef9c1ed7f729f52...`	✘	✔	✔	✔	✔	✔	✔
`bool`	A boolean	`True` , `False`	✔	✔	✔	✔	✔	✔	✔
`bytes`	A sequence of bytes	`0x` , `0xABCDEF42`	✔	✔	✔	✔	✔	✔	✔
`chain_id`	A chain identifier	`0x7a06a770` , `"NetXynUjJNZm7wi"`	✔	✔	✔	✔	✔	✔	✔
`chest`	A timelocked chest	`0xe0d984a0e19fd7e7a4ac...`	✘	✔	✔	✔	✔	✔	✔
`chest_key`	A key to open a timelocked chest	`0xc7f3caf4c8c2e3e7af8e...`	✘	✔	✔	✔	✔	✔	✔
`contract type`	Address of a contract, where type is the contract's parameter type		✘	✔	✘	✘	✔	✘	✔
`int`	An arbitrary-precision integer	`-99999` , `-1` , `0` , `1` , `99999`	✔	✔	✔	✔	✔	✔	✔
`key`	A public cryptographic key	`"edpkuBknW28nW72KG6RoH...` , `"edpkuJqtDcA2m2muMxViS...`	✔	✔	✔	✔	✔	✔	✔
`key_hash`	A hash of a public cryptographic key	`"tz1KqTpEZ7Yob7QbPE4Hy...` , `"tz1XPTDmvT3vVE5Uunngm...`	✔	✔	✔	✔	✔	✔	✔
`lambda ty1 ty2`	A lambda with given parameter and return types	`{ }` , `{ PUSH nat 1; ADD }` , `Lambda_rec { EXEC }` , `Lambda_rec { PUSH int ...`	✘	✔	✔	✔	✔	✔	✔
`list type`	A single, immutable, homogeneous linked list	`{}` , `{ 0 ; 10 }` , `{ Some 10 ; None }`	✘	`type`	`type`	`type`	`type`	`type`	`type`
`map kty vty`	An immutable map from `kty` to `vty`	`{}` , `{ Elt 0 0xCB ; Elt 1 0...`	✘	`vty`	`vty`	`vty`	`vty`	`vty`	`vty`
`mutez`	A specific type for manipulating tokens	`0` , `1` , `99999`	✔	✔	✔	✔	✔	✔	✔
`nat`	An arbitrary-precision natural number	`0` , `1` , `99999`	✔	✔	✔	✔	✔	✔	✔
`never`	The empty type		✔	✔	✔	✔	✔	✔	✔
`operation`	An internal operation emitted by a contract		✘	✘	✘	✘	✘	✘	✔
`option ty`	An optional value	`None` , `Some "foo"`	`ty`	`ty`	`ty`	`ty`	`ty`	`ty`	`ty`
`or ty1 ty2`	A union of two types	`(Left True)` , `(Right "foo")`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`
`pair ty1 ty2`	A pair or tuple of values	`(Pair 0 True)` , `(Pair 0 (Pair True 0x)...` , `(Pair 0 True 0x)` , `{0; True; 0x}`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`
`sapling_state n`	A Sapling state	`{}`	✘	✔	✔	✘	✘	✘	✔
`sapling_transaction n`	A Sapling transaction		✘	✔	✔	✔	✔	✔	✔
`set cty`	An immutable set of comparable values of type `cty`	`{}` , `{ 0 ; 3 ; 4 }`	✘	`cty`	`cty`	`cty`	`cty`	`cty`	`cty`
`signature`	A cryptographic signature	`"edsigthTzJ8X7MPmNeEwy...` , `"spsig1PPUFZucuAQybs5w...`	✔	✔	✔	✔	✔	✔	✔
`string`	A string of characters	`"foo"` , `"ABC\n123"`	✔	✔	✔	✔	✔	✔	✔
`ticket cty`	A ticket used to authenticate information of type `cty`	`Pair "KT1ThEdxfUcWUwqs...` , `Pair "KT1ThEdxfUcWUwqs...`	✘	✔	✔	✘	✘	✔	✘
`timestamp`	A real-world date.	`"2019-09-26T10:59:51Z"` , `1571659294`	✔	✔	✔	✔	✔	✔	✔
`unit`	The type whose only value is `Unit`	`Unit`	✔	✔	✔	✔	✔	✔	✔

All pushable types are also packable and vice versa. Except for the domain specific types operation, contract, ticket, sapling_state and big_map, all types are passable, storable, pushable, packable and can be used as values in big_maps. The only type that is not duplicable is ticket.

Instructions ¶

Instruction	Description	Type
`ABS`	Obtain the absolute value of an integer	`int : A` — `nat : A`
`ADD`	Add two numerical values	`nat : nat : A` — `nat : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `timestamp : int : A` — `timestamp : A` `int : timestamp : A` — `timestamp : A` `mutez : mutez : A` — `mutez : A` `bls12_381_g1 : bls12_381_g1 : A` — `bls12_381_g1 : A` `bls12_381_g2 : bls12_381_g2 : A` — `bls12_381_g2 : A` `bls12_381_fr : bls12_381_fr : A` — `bls12_381_fr : A`
`ADDRESS`	Push the address of a contract	`contract ty1 : A` — `address : A`
`AMOUNT`	Push the amount of the current transaction	`A` — `mutez : A`
`AND`	Boolean and bitwise AND	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `int : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`
`APPLY`	Partially apply a tuplified function from the stack	`ty1 : lambda ( pair ty1 ty2 ) ty3 : A` — `lambda ty2 ty3 : A`
`BALANCE`	Push the current amount of mutez of the executing contract	`A` — `mutez : A`
`BLAKE2B`	Compute a Blake2B cryptographic hash	`bytes : A` — `bytes : A`
`BYTES`	Encode an integer or a natural number to bytes	`int : A` — `bytes : A` `nat : A` — `bytes : A`
`CAR`	Access the left part of a pair	`pair ty1 ty2 : A` — `ty1 : A`
`CDR`	Access the right part of a pair	`pair ty1 ty2 : A` — `ty2 : A`
`CHAIN_ID`	Push the chain identifier	`A` — `chain_id : A`
`CHECK_SIGNATURE`	Verify `signature` of `bytes` by `key`	`key : signature : bytes : A` — `bool : A`
`COMPARE`	Compare two values	`cty : cty : A` — `int : A`
`CONCAT`	Concatenate strings or byte sequences	`string : string : A` — `string : A` `list string : A` — `string : A` `bytes : bytes : A` — `bytes : A` `list bytes : A` — `bytes : A`
`CONS`	Prepend an element to a list	`ty1 : list ty1 : A` — `list ty1 : A`
`CONTRACT ty`	Cast an address to a typed contract	`address : A` — `option ( contract ty ) : A`
`CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 }`	Push a contract creation operation	`option key_hash : mutez : ty2 : A` — `operation : address : A`
`DIG n`	Retrieve the `n`th element of the stack	`A @ ( ty1 : B )` — `ty1 : ( A @ B )`
`DIP instr`	Run code protecting the top of the stack	`ty : B` — `ty : C`
`DIP n instr`	Run code protecting the `n` topmost elements of the stack	`A @ B` — `A @ C`
`DROP`	Drop the top element of the stack	`ty : A` — `A`
`DROP n`	Drop the top `n` elements of the stack	`A @ B` — `B`
`DUG n`	Insert the top element at depth `n`	`ty1 : ( A @ B )` — `A @ ( ty1 : B )`
`DUP`	Duplicate the top of the stack	`ty1 : A` — `ty1 : ty1 : A`
`DUP n`	Duplicate the `n`th element of the stack	`A @ ty1 : B` — `ty1 : A @ ty1 : B`
`EDIV`	Euclidean division	`nat : nat : A` — `option ( pair nat nat ) : A` `nat : int : A` — `option ( pair int nat ) : A` `int : nat : A` — `option ( pair int nat ) : A` `int : int : A` — `option ( pair int nat ) : A` `mutez : nat : A` — `option ( pair mutez mutez ) : A` `mutez : mutez : A` — `option ( pair nat mutez ) : A`
`EMIT ty`	Write an event into the transaction receipt	`ty : A` — `operation : A`
`EMPTY_BIG_MAP kty vty`	Build a new, empty `big_map` from `kty` to `vty`	`A` — `big_map kty vty : A`
`EMPTY_MAP kty vty`	Build a new, empty `map` from `kty` to `vty`	`A` — `map kty vty : A`
`EMPTY_SET cty`	Build a new, empty set for elements of type `cty`	`A` — `set cty : A`
`EQ`	Check that the top of the stack equals zero	`int : A` — `bool : A`
`EXEC`	Execute a function from the stack	`ty1 : lambda ty1 ty2 : A` — `ty2 : A`
`FAILWITH`	Explicitly abort the current program	`ty1 : A` — `B`
`GE`	Check that the top of the stack is greater than or equal to zero	`int : A` — `bool : A`
`GET`	Access an element in a `map` or `big_map`	`kty : map kty vty : A` — `option vty : A` `kty : big_map kty vty : A` — `option vty : A`
`GET n`	Access an element or a sub comb in a right comb	`ty : A` — `ty : A` `pair ty1 ty2 : A` — `ty1 : A` `pair ty1 ty2 : A` — `ty : A`
`GET_AND_UPDATE`	A combination of the `GET` and `UPDATE` instructions	`kty : option vty : map kty vty : A` — `option vty : map kty vty : A` `kty : option vty : big_map kty vty : A` — `option vty : big_map kty vty : A`
`GT`	Check that the top of the stack is greater than zero	`int : A` — `bool : A`
`HASH_KEY`	Compute the Base58Check of a public key	`key : A` — `key_hash : A`
`IF instr1 instr2`	Conditional branching	`bool : A` — `B`
`IF_CONS instr1 instr2`	Inspect a list	`list ty : A` — `B`
`IF_LEFT instr1 instr2`	Inspect a value of a union	`or ty1 ty2 : A` — `B`
`IF_NONE instr1 instr2`	Inspect an optional value	`option ty1 : A` — `B`
`IMPLICIT_ACCOUNT`	Create an implicit account	`key_hash : A` — `contract unit : A`
`INT`	Convert a natural number, a BLS12-381 field element, or a byte sequence to an integer	`nat : A` — `int : A` `bls12_381_fr : A` — `int : A` `bytes : A` — `int : A`
`ISNAT`	Convert a non-negative integer to a natural number	`int : A` — `option nat : A`
`ITER instr`	Iterate over a `set`, `list` or `map`	`list ty : A` — `A` `set cty : A` — `A` `map kty vty : A` — `A`
`JOIN_TICKETS`	Join two tickets into one	`pair ( ticket cty ) ( ticket cty ) : A` — `option ( ticket cty ) : A`
`KECCAK`	Compute a Keccak-256 cryptographic hash	`bytes : A` — `bytes : A`
`LAMBDA ty1 ty2 instr`	Push a lambda onto the stack	`A` — `lambda ty1 ty2 : A`
`LAMBDA_REC ty1 ty2 instr`	Push a recursive lambda onto the stack	`A` — `lambda ty1 ty2 : A`
`LE`	Check that the top of the stack is less than or equal to zero	`int : A` — `bool : A`
`LEFT ty2`	Wrap a value in a union (left case)	`ty1 : A` — `or ty1 ty2 : A`
`LEVEL`	Push the current block level	`A` — `nat : A`
`LOOP instr`	A generic loop	`bool : A` — `A`
`LOOP_LEFT instr`	Loop with accumulator	`or ty1 ty2 : A` — `ty2 : A`
`LSL`	Logically left shift of a natural number or of a byte sequence	`nat : nat : A` — `nat : A` `bytes : nat : A` — `bytes : A`
`LSR`	Logically right shift of a natural number or of a byte sequence	`nat : nat : A` — `nat : A` `bytes : nat : A` — `bytes : A`
`LT`	Check that the top of the stack is less than zero	`int : A` — `bool : A`
`MAP instr`	Apply `instr` to each element of a `list`, an `option`, or `map`.	`list ty : A` — `list ty2 : A` `option ty : A` — `option ty2 : A` `map kty ty1 : A` — `map kty ty2 : A`
`MEM`	Check for the presence of a binding for a key in a `map`, `set` or `big_map`	`cty : set cty : A` — `bool : A` `kty : map kty vty : A` — `bool : A` `kty : big_map kty vty : A` — `bool : A`
`MIN_BLOCK_TIME`	Push the current minimal block time in seconds.	`A` — `nat : A`
`MUL`	Multiply two numerical values	`nat : nat : A` — `nat : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `mutez : nat : A` — `mutez : A` `nat : mutez : A` — `mutez : A` `bls12_381_g1 : bls12_381_fr : A` — `bls12_381_g1 : A` `bls12_381_g2 : bls12_381_fr : A` — `bls12_381_g2 : A` `bls12_381_fr : bls12_381_fr : A` — `bls12_381_fr : A` `nat : bls12_381_fr : A` — `bls12_381_fr : A` `int : bls12_381_fr : A` — `bls12_381_fr : A` `bls12_381_fr : nat : A` — `bls12_381_fr : A` `bls12_381_fr : int : A` — `bls12_381_fr : A`
`NAT`	Convert bytes to a natural number	`bytes : A` — `nat : A`
`NEG`	Negate a numerical value	`nat : A` — `int : A` `int : A` — `int : A` `bls12_381_g1 : A` — `bls12_381_g1 : A` `bls12_381_g2 : A` — `bls12_381_g2 : A` `bls12_381_fr : A` — `bls12_381_fr : A`
`NEQ`	Check that the top of the stack is not equal to zero	`int : A` — `bool : A`
`NEVER`	Close a forbidden branch	`never : A` — `B`
`NIL ty`	Push an empty list	`A` — `list ty : A`
`NONE ty`	Push the absent optional value	`A` — `option ty : A`
`NOT`	Boolean negation and bitwise complement	`bool : A` — `bool : A` `nat : A` — `int : A` `int : A` — `int : A` `bytes : A` — `bytes : A`
`NOW`	Push block timestamp	`A` — `timestamp : A`
`OPEN_CHEST`	Open a timelocked chest given its key and the time	`chest_key : chest : nat : A` — `option bytes : A`
`OR`	Boolean and bitwise OR	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`
`PACK`	Serialize data	`ty : A` — `bytes : A`
`PAIR`	Build a pair from the stack's top two elements	`ty1 : ty2 : A` — `pair ty1 ty2 : A`
`PAIR n`	Fold `n` values on the top of the stack into a right comb	`ty1 : .... : tyN : A` — `pair ty1 .... tyN : A`
`PAIRING_CHECK`	Check a BLS12-381 pairing	`list ( pair bls12_381_g1 bls12_381_g2 ) : A` — `bool : A`
`PUSH ty x`	Push a constant value of a given type onto the stack	`A` — `ty : A`
`READ_TICKET`	Retrieve the information stored in a ticket. Also return the ticket.	`ticket cty : A` — `pair address cty nat : ticket cty : A`
`RIGHT ty1`	Wrap a value in a union (right case)	`ty2 : A` — `or ty1 ty2 : A`
`SAPLING_EMPTY_STATE ms`	Push an empty Sapling state on the stack	`A` — `sapling_state ms : A`
`SAPLING_VERIFY_UPDATE`	Verify and apply a transaction on a Sapling state	`sapling_transaction ms : sapling_state ms : A` — `option ( pair bytes ( pair int ( sapling_state ms ) ) ) : A`
`SELF`	Push the current contract	`A` — `contract ty : A`
`SELF_ADDRESS`	Push the address of the current contract	`A` — `address : A`
`SENDER`	Push the contract that initiated the current internal transaction	`A` — `address : A`
`SET_DELEGATE`	Push a delegation operation	`option key_hash : A` — `operation : A`
`SHA256`	Compute a SHA-256 cryptographic hash	`bytes : A` — `bytes : A`
`SHA3`	Compute a SHA3-256 cryptographic hash	`bytes : A` — `bytes : A`
`SHA512`	Compute a SHA-512 cryptographic hash	`bytes : A` — `bytes : A`
`SIZE`	Obtain size of a `string`, `list`, `set`, `map` or byte sequence `bytes`	`set cty : A` — `nat : A` `map kty vty : A` — `nat : A` `list ty : A` — `nat : A` `string : A` — `nat : A` `bytes : A` — `nat : A`
`SLICE`	Obtain a substring or subsequence of a `string` respectively byte sequence `bytes`	`nat : nat : string : A` — `option string : A` `nat : nat : bytes : A` — `option bytes : A`
`SOME`	Wrap an existing optional value	`ty1 : A` — `option ty1 : A`
`SOURCE`	Push the contract that initiated the current transaction	`A` — `address : A`
`SPLIT_TICKET`	Split a ticket in two	`ticket cty : pair nat nat : A` — `option ( pair ( ticket cty ) ( ticket cty ) ) : A`
`SUB`	Subtract two numerical values	`nat : nat : A` — `int : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `timestamp : int : A` — `timestamp : A` `timestamp : timestamp : A` — `int : A`
`SUB_MUTEZ`	Subtract two mutez	`mutez : mutez : A` — `option mutez : A`
`SWAP`	Swap the top two elements of the stack	`ty1 : ty2 : A` — `ty2 : ty1 : A`
`TICKET`	Create a ticket	`cty : nat : A` — `option ( ticket cty ) : A`
`TOTAL_VOTING_POWER`	Return the total voting power of all contracts	`A` — `nat : A`
`TRANSFER_TOKENS`	Push a transaction operation	`ty : mutez : contract ty : A` — `operation : A`
`UNIT`	Push the unit value onto the stack	`A` — `unit : A`
`UNPACK ty`	Deserialize data, if valid	`bytes : A` — `option ty : A`
`UNPAIR`	Split a pair into its components	`pair ty1 ty2 : A` — `ty1 : ty2 : A`
`UNPAIR n`	Unfold `n` values from a right comb on the top of the stack	`pair ty1 .... tyN : A` — `ty1 : .... : tyN : A`
`UPDATE`	Add, update, or remove an element in a `map`, `big_map` or `set`	`cty : bool : set cty : A` — `set cty : A` `kty : option vty : map kty vty : A` — `map kty vty : A` `kty : option vty : big_map kty vty : A` — `big_map kty vty : A`
`UPDATE n`	Update an element or a sub comb in a right comb	`ty1 : ty2 : A` — `ty1 : A` `ty : pair ty1 ty2 : A` — `pair ty ty2 : A` `ty : pair ty1 ty2 : A` — `pair ty1 ty' : A`
`VIEW name return_ty`	Call a view	`ty : address : A` — `option return_ty : A`
`VOTING_POWER`	Return the voting power of a given contract	`key_hash : A` — `nat : A`
`XOR`	Boolean and bitwise eXclusive OR	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`
`instr1 ; instr2`	Instruction sequence	`A` — `C`
`{}`	Empty instruction sequence	`A` — `A`

Instructions by Category ¶

Control structures ¶

Instruction	Description	Type
`APPLY`	Partially apply a tuplified function from the stack	`ty1 : lambda ( pair ty1 ty2 ) ty3 : A` — `lambda ty2 ty3 : A`
`EXEC`	Execute a function from the stack	`ty1 : lambda ty1 ty2 : A` — `ty2 : A`
`FAILWITH`	Explicitly abort the current program	`ty1 : A` — `B`
`IF instr1 instr2`	Conditional branching	`bool : A` — `B`
`IF_CONS instr1 instr2`	Inspect a list	`list ty : A` — `B`
`IF_LEFT instr1 instr2`	Inspect a value of a union	`or ty1 ty2 : A` — `B`
`IF_NONE instr1 instr2`	Inspect an optional value	`option ty1 : A` — `B`
`LAMBDA ty1 ty2 instr`	Push a lambda onto the stack	`A` — `lambda ty1 ty2 : A`
`LAMBDA_REC ty1 ty2 instr`	Push a recursive lambda onto the stack	`A` — `lambda ty1 ty2 : A`
`LOOP instr`	A generic loop	`bool : A` — `A`
`LOOP_LEFT instr`	Loop with accumulator	`or ty1 ty2 : A` — `ty2 : A`
`instr1 ; instr2`	Instruction sequence	`A` — `C`
`{}`	Empty instruction sequence	`A` — `A`

Stack manipulation ¶

Instruction	Description	Type
`DIG n`	Retrieve the `n`th element of the stack	`A @ ( ty1 : B )` — `ty1 : ( A @ B )`
`DIP instr`	Run code protecting the top of the stack	`ty : B` — `ty : C`
`DIP n instr`	Run code protecting the `n` topmost elements of the stack	`A @ B` — `A @ C`
`DROP`	Drop the top element of the stack	`ty : A` — `A`
`DROP n`	Drop the top `n` elements of the stack	`A @ B` — `B`
`DUG n`	Insert the top element at depth `n`	`ty1 : ( A @ B )` — `A @ ( ty1 : B )`
`DUP`	Duplicate the top of the stack	`ty1 : A` — `ty1 : ty1 : A`
`DUP n`	Duplicate the `n`th element of the stack	`A @ ty1 : B` — `ty1 : A @ ty1 : B`
`PUSH ty x`	Push a constant value of a given type onto the stack	`A` — `ty : A`
`SWAP`	Swap the top two elements of the stack	`ty1 : ty2 : A` — `ty2 : ty1 : A`

Arithmetic operations ¶

Instruction	Description	Type
`ABS`	Obtain the absolute value of an integer	`int : A` — `nat : A`
`ADD`	Add two numerical values	`nat : nat : A` — `nat : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `timestamp : int : A` — `timestamp : A` `int : timestamp : A` — `timestamp : A` `mutez : mutez : A` — `mutez : A` `bls12_381_g1 : bls12_381_g1 : A` — `bls12_381_g1 : A` `bls12_381_g2 : bls12_381_g2 : A` — `bls12_381_g2 : A` `bls12_381_fr : bls12_381_fr : A` — `bls12_381_fr : A`
`BYTES`	Encode an integer or a natural number to bytes	`int : A` — `bytes : A` `nat : A` — `bytes : A`
`COMPARE`	Compare two values	`cty : cty : A` — `int : A`
`EDIV`	Euclidean division	`nat : nat : A` — `option ( pair nat nat ) : A` `nat : int : A` — `option ( pair int nat ) : A` `int : nat : A` — `option ( pair int nat ) : A` `int : int : A` — `option ( pair int nat ) : A` `mutez : nat : A` — `option ( pair mutez mutez ) : A` `mutez : mutez : A` — `option ( pair nat mutez ) : A`
`EQ`	Check that the top of the stack equals zero	`int : A` — `bool : A`
`GE`	Check that the top of the stack is greater than or equal to zero	`int : A` — `bool : A`
`GT`	Check that the top of the stack is greater than zero	`int : A` — `bool : A`
`INT`	Convert a natural number, a BLS12-381 field element, or a byte sequence to an integer	`nat : A` — `int : A` `bls12_381_fr : A` — `int : A` `bytes : A` — `int : A`
`ISNAT`	Convert a non-negative integer to a natural number	`int : A` — `option nat : A`
`LE`	Check that the top of the stack is less than or equal to zero	`int : A` — `bool : A`
`LSL`	Logically left shift of a natural number or of a byte sequence	`nat : nat : A` — `nat : A` `bytes : nat : A` — `bytes : A`
`LSR`	Logically right shift of a natural number or of a byte sequence	`nat : nat : A` — `nat : A` `bytes : nat : A` — `bytes : A`
`LT`	Check that the top of the stack is less than zero	`int : A` — `bool : A`
`MUL`	Multiply two numerical values	`nat : nat : A` — `nat : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `mutez : nat : A` — `mutez : A` `nat : mutez : A` — `mutez : A` `bls12_381_g1 : bls12_381_fr : A` — `bls12_381_g1 : A` `bls12_381_g2 : bls12_381_fr : A` — `bls12_381_g2 : A` `bls12_381_fr : bls12_381_fr : A` — `bls12_381_fr : A` `nat : bls12_381_fr : A` — `bls12_381_fr : A` `int : bls12_381_fr : A` — `bls12_381_fr : A` `bls12_381_fr : nat : A` — `bls12_381_fr : A` `bls12_381_fr : int : A` — `bls12_381_fr : A`
`NAT`	Convert bytes to a natural number	`bytes : A` — `nat : A`
`NEG`	Negate a numerical value	`nat : A` — `int : A` `int : A` — `int : A` `bls12_381_g1 : A` — `bls12_381_g1 : A` `bls12_381_g2 : A` — `bls12_381_g2 : A` `bls12_381_fr : A` — `bls12_381_fr : A`
`NEQ`	Check that the top of the stack is not equal to zero	`int : A` — `bool : A`
`SUB`	Subtract two numerical values	`nat : nat : A` — `int : A` `nat : int : A` — `int : A` `int : nat : A` — `int : A` `int : int : A` — `int : A` `timestamp : int : A` — `timestamp : A` `timestamp : timestamp : A` — `int : A`
`SUB_MUTEZ`	Subtract two mutez	`mutez : mutez : A` — `option mutez : A`

Boolean operations ¶

Instruction	Description	Type
`AND`	Boolean and bitwise AND	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `int : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`
`NOT`	Boolean negation and bitwise complement	`bool : A` — `bool : A` `nat : A` — `int : A` `int : A` — `int : A` `bytes : A` — `bytes : A`
`OR`	Boolean and bitwise OR	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`
`XOR`	Boolean and bitwise eXclusive OR	`bool : bool : A` — `bool : A` `nat : nat : A` — `nat : A` `bytes : bytes : A` — `bytes : A`

Cryptographic operations ¶

Instruction	Description	Type
`BLAKE2B`	Compute a Blake2B cryptographic hash	`bytes : A` — `bytes : A`
`CHECK_SIGNATURE`	Verify `signature` of `bytes` by `key`	`key : signature : bytes : A` — `bool : A`
`HASH_KEY`	Compute the Base58Check of a public key	`key : A` — `key_hash : A`
`KECCAK`	Compute a Keccak-256 cryptographic hash	`bytes : A` — `bytes : A`
`PAIRING_CHECK`	Check a BLS12-381 pairing	`list ( pair bls12_381_g1 bls12_381_g2 ) : A` — `bool : A`
`SAPLING_EMPTY_STATE ms`	Push an empty Sapling state on the stack	`A` — `sapling_state ms : A`
`SAPLING_VERIFY_UPDATE`	Verify and apply a transaction on a Sapling state	`sapling_transaction ms : sapling_state ms : A` — `option ( pair bytes ( pair int ( sapling_state ms ) ) ) : A`
`SHA256`	Compute a SHA-256 cryptographic hash	`bytes : A` — `bytes : A`
`SHA3`	Compute a SHA3-256 cryptographic hash	`bytes : A` — `bytes : A`
`SHA512`	Compute a SHA-512 cryptographic hash	`bytes : A` — `bytes : A`

Blockchain operations ¶

Instruction	Description	Type
`ADDRESS`	Push the address of a contract	`contract ty1 : A` — `address : A`
`AMOUNT`	Push the amount of the current transaction	`A` — `mutez : A`
`BALANCE`	Push the current amount of mutez of the executing contract	`A` — `mutez : A`
`CHAIN_ID`	Push the chain identifier	`A` — `chain_id : A`
`CONTRACT ty`	Cast an address to a typed contract	`address : A` — `option ( contract ty ) : A`
`CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 }`	Push a contract creation operation	`option key_hash : mutez : ty2 : A` — `operation : address : A`
`EMIT ty`	Write an event into the transaction receipt	`ty : A` — `operation : A`
`IMPLICIT_ACCOUNT`	Create an implicit account	`key_hash : A` — `contract unit : A`
`LEVEL`	Push the current block level	`A` — `nat : A`
`MIN_BLOCK_TIME`	Push the current minimal block time in seconds.	`A` — `nat : A`
`NOW`	Push block timestamp	`A` — `timestamp : A`
`SELF`	Push the current contract	`A` — `contract ty : A`
`SELF_ADDRESS`	Push the address of the current contract	`A` — `address : A`
`SENDER`	Push the contract that initiated the current internal transaction	`A` — `address : A`
`SET_DELEGATE`	Push a delegation operation	`option key_hash : A` — `operation : A`
`SOURCE`	Push the contract that initiated the current transaction	`A` — `address : A`
`TOTAL_VOTING_POWER`	Return the total voting power of all contracts	`A` — `nat : A`
`TRANSFER_TOKENS`	Push a transaction operation	`ty : mutez : contract ty : A` — `operation : A`
`VIEW name return_ty`	Call a view	`ty : address : A` — `option return_ty : A`
`VOTING_POWER`	Return the voting power of a given contract	`key_hash : A` — `nat : A`

Operations on data structures ¶

Instruction	Description	Type
`CAR`	Access the left part of a pair	`pair ty1 ty2 : A` — `ty1 : A`
`CDR`	Access the right part of a pair	`pair ty1 ty2 : A` — `ty2 : A`
`CONCAT`	Concatenate strings or byte sequences	`string : string : A` — `string : A` `list string : A` — `string : A` `bytes : bytes : A` — `bytes : A` `list bytes : A` — `bytes : A`
`CONS`	Prepend an element to a list	`ty1 : list ty1 : A` — `list ty1 : A`
`EMPTY_BIG_MAP kty vty`	Build a new, empty `big_map` from `kty` to `vty`	`A` — `big_map kty vty : A`
`EMPTY_MAP kty vty`	Build a new, empty `map` from `kty` to `vty`	`A` — `map kty vty : A`
`EMPTY_SET cty`	Build a new, empty set for elements of type `cty`	`A` — `set cty : A`
`GET`	Access an element in a `map` or `big_map`	`kty : map kty vty : A` — `option vty : A` `kty : big_map kty vty : A` — `option vty : A`
`GET n`	Access an element or a sub comb in a right comb	`ty : A` — `ty : A` `pair ty1 ty2 : A` — `ty1 : A` `pair ty1 ty2 : A` — `ty : A`
`GET_AND_UPDATE`	A combination of the `GET` and `UPDATE` instructions	`kty : option vty : map kty vty : A` — `option vty : map kty vty : A` `kty : option vty : big_map kty vty : A` — `option vty : big_map kty vty : A`
`ITER instr`	Iterate over a `set`, `list` or `map`	`list ty : A` — `A` `set cty : A` — `A` `map kty vty : A` — `A`
`LEFT ty2`	Wrap a value in a union (left case)	`ty1 : A` — `or ty1 ty2 : A`
`MAP instr`	Apply `instr` to each element of a `list`, an `option`, or `map`.	`list ty : A` — `list ty2 : A` `option ty : A` — `option ty2 : A` `map kty ty1 : A` — `map kty ty2 : A`
`MEM`	Check for the presence of a binding for a key in a `map`, `set` or `big_map`	`cty : set cty : A` — `bool : A` `kty : map kty vty : A` — `bool : A` `kty : big_map kty vty : A` — `bool : A`
`NEVER`	Close a forbidden branch	`never : A` — `B`
`NIL ty`	Push an empty list	`A` — `list ty : A`
`NONE ty`	Push the absent optional value	`A` — `option ty : A`
`PACK`	Serialize data	`ty : A` — `bytes : A`
`PAIR`	Build a pair from the stack's top two elements	`ty1 : ty2 : A` — `pair ty1 ty2 : A`
`PAIR n`	Fold `n` values on the top of the stack into a right comb	`ty1 : .... : tyN : A` — `pair ty1 .... tyN : A`
`RIGHT ty1`	Wrap a value in a union (right case)	`ty2 : A` — `or ty1 ty2 : A`
`SIZE`	Obtain size of a `string`, `list`, `set`, `map` or byte sequence `bytes`	`set cty : A` — `nat : A` `map kty vty : A` — `nat : A` `list ty : A` — `nat : A` `string : A` — `nat : A` `bytes : A` — `nat : A`
`SLICE`	Obtain a substring or subsequence of a `string` respectively byte sequence `bytes`	`nat : nat : string : A` — `option string : A` `nat : nat : bytes : A` — `option bytes : A`
`SOME`	Wrap an existing optional value	`ty1 : A` — `option ty1 : A`
`UNIT`	Push the unit value onto the stack	`A` — `unit : A`
`UNPACK ty`	Deserialize data, if valid	`bytes : A` — `option ty : A`
`UNPAIR`	Split a pair into its components	`pair ty1 ty2 : A` — `ty1 : ty2 : A`
`UNPAIR n`	Unfold `n` values from a right comb on the top of the stack	`pair ty1 .... tyN : A` — `ty1 : .... : tyN : A`
`UPDATE`	Add, update, or remove an element in a `map`, `big_map` or `set`	`cty : bool : set cty : A` — `set cty : A` `kty : option vty : map kty vty : A` — `map kty vty : A` `kty : option vty : big_map kty vty : A` — `big_map kty vty : A`
`UPDATE n`	Update an element or a sub comb in a right comb	`ty1 : ty2 : A` — `ty1 : A` `ty : pair ty1 ty2 : A` — `pair ty ty2 : A` `ty : pair ty1 ty2 : A` — `pair ty1 ty' : A`

Operations on tickets ¶

Instruction	Description	Type
`JOIN_TICKETS`	Join two tickets into one	`pair ( ticket cty ) ( ticket cty ) : A` — `option ( ticket cty ) : A`
`READ_TICKET`	Retrieve the information stored in a ticket. Also return the ticket.	`ticket cty : A` — `pair address cty nat : ticket cty : A`
`SPLIT_TICKET`	Split a ticket in two	`ticket cty : pair nat nat : A` — `option ( pair ( ticket cty ) ( ticket cty ) ) : A`
`TICKET`	Create a ticket	`cty : nat : A` — `option ( ticket cty ) : A`

Operations on timelock ¶

Instruction	Description	Type
`OPEN_CHEST`	Open a timelocked chest given its key and the time	`chest_key : chest : nat : A` — `option bytes : A`

Type Reference ¶

`address` ¶

Address of an untyped contract

Description

The address type merely gives the guarantee that the value has the form of a Tezos address, as opposed to contract that guarantees that the value is indeed a valid, existing account.

A valid Tezos address is a string prefixed by either tz1, tz2, tz3 or KT1 and followed by a Base58 encoded hash and terminated by a 4-byte checksum.

The prefix designates the type of address:

tz1 addresses are followed by a ed25519 public key hash
tz2 addresses are followed by a Secp256k1 public key hash
tz3 addresses are followed by a NIST p256r1 public key hash
KT1 addresses are followed by a contract hash

Addresses prefixed by tz1, tz2 and tz3 designate implicit accounts, whereas those prefixed KT1 designate originated accounts.

Finally, addresses can specify an entrypoint, with a %entrypoint suffix.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


"KT1ThEdxfUcWUwqsdergy...


"KT1BEqzn5Wx8uJrZNvuS9...


"tz1KqTpEZ7Yob7QbPE4Hy...


"tz2VGBaXuS6rnaa5hpC92...


"tz3WEJYwJ6pPwVbSL8FrS...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`big_map kty vty` ¶

A lazily deserialized map from `kty` to `vty`

Description

Lazily deserialized maps from keys of type kty of values of type vty. These maps should be used if you intend to store large amounts of data in a map. Using big_map can reduce gas costs significantly compared to standard maps, as data is lazily deserialized. Note however that individual operations on big_map have higher gas costs than those over standard maps. A big_map also has a lower storage cost than a standard map of the same size, when large keys are used, since only the hash of each key is stored in a big_map.

The behavior of GET, UPDATE, GET_AND_UPDATE and MEM is the same on big_maps as on normal maps, except that under the hood, elements are loaded and deserialized on demand.

Literal big_maps cannot be pushed directly in contract code. Instead, they must be created using EMPTY_BIG_MAP and manipulated using GET, UPDATE, GET_AND_UPDATE and MEM.

Big maps have three possible representations. A map literal is always a valid representation for a big map, and is used when originating and calling contracts using octez-client. The two other representations are internal only: big maps can also be represented by integers called big-map identifiers, or as pairs of a big-map identifier (an integer) and a big-map diff (written in the same syntax as a map whose values are options).

So for example, { Elt "bar" True ; Elt "foo" False }, 42, and Pair 42 { Elt "foo" (Some False) } could all be valid representations of type big_map string bool.

Values of the big_map type cannot be serialized using PACK.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

{}


{ Elt 0 0xCB ; Elt 1 0...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	`vty`	`vty`	✘	✘	✘	`vty`

`bls12_381_fr` ¶

An element of the BLS12-381 scalar field F_r

Description

An element of the scalar field F_r, used for scalar multiplication on the BLS12-381 curves G₁ and G₂.

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values


 0x01


 0x0001

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`bls12_381_g1` ¶

A point on the BLS12-381 curve G₁

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values


0x0572cbea904d67468808...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`bls12_381_g2` ¶

A point on the BLS12-381 curve G₂

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values


0x0a4edef9c1ed7f729f52...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`bool` ¶

A boolean

Description

The type for booleans whose values are True and False.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 True


 False

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`bytes` ¶

A sequence of bytes

Description

Bytes are used for serializing data, in order to check signatures and compute hashes on them. They can also be used to incorporate data from the wild and untyped outside world.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

0x


 0xABCDEF42

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`chain_id` ¶

A chain identifier

Description

An identifier for a chain, used to distinguish the test and the main chains.

The value is derived from the genesis block hash and will thus be different on the main chains of different networks and on the test chains for which the value depends on the first block of the testchain.

Available since mainnet protocol

Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

Proposed in protocol

Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

Example values


 0x7a06a770


 "NetXynUjJNZm7wi"

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`chest` ¶

A timelocked chest

Description

A timelocked chest containing bytes and information to open it.

See Timelock for more information.

Proposed in protocol

Oxford (ProxfordSW2S7fvchT1Zgj2avb5UES194neRyYVXoaDGvF9egt8)

Example values


0xe0d984a0e19fd7e7a4ac...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`chest_key` ¶

A key to open a timelocked chest

Description

Used to open a chest, also contains a proof to check the correctness of the opening.

See Timelock for more information.

Proposed in protocol

Oxford (ProxfordSW2S7fvchT1Zgj2avb5UES194neRyYVXoaDGvF9egt8)

Example values


0xc7f3caf4c8c2e3e7af8e...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`contract type` ¶

Address of a contract, where type is the contract's parameter type

Description

A value of type contract t is guaranteed to be a valid, existing account whose parameter type is t. This can be opposed to the address type, that merely gives the guarantee that the value has the form of a Tezos address. Values of the contract type cannot be stored. There are not literal values of type contract. Instead, such values are created using instructions such as CONTRACT or IMPLICIT_ACCOUNT.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

There are no literal values of this type.

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✘	✘	✔	✘	✔

`int` ¶

An arbitrary-precision integer

Description

Integers are arbitrary-precision, meaning that the only size limit is gas.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 -99999

-1

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`key` ¶

A public cryptographic key

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


"edpkuBknW28nW72KG6RoH...


"edpkuJqtDcA2m2muMxViS...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`key_hash` ¶

A hash of a public cryptographic key

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


"tz1KqTpEZ7Yob7QbPE4Hy...


"tz1XPTDmvT3vVE5Uunngm...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`lambda ty1 ty2` ¶

A lambda with given parameter and return types

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

{ }


 { PUSH nat 1; ADD }


 Lambda_rec { EXEC }


Lambda_rec { PUSH int ...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`list type` ¶

A single, immutable, homogeneous linked list

Description

A single, immutable, homogeneous linked list, whose elements are of type type, and that we note {} for the empty list or { first ; ... }. In the semantics, we use the less-than and greater-than sign (< and >) to denote a subsequence of elements. For instance { head ; <tail> }.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

{}


 { 0 ; 10 }


 { Some 10 ; None }

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	`type`	`type`	`type`	`type`	`type`	`type`

`map kty vty` ¶

An immutable map from `kty` to `vty`

Description

Immutable maps from keys of type kty and values of type vty that we note { Elt key value ; ... }, with keys sorted by increasing order.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

{}


{ Elt 0 0xCB ; Elt 1 0...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	`vty`	`vty`	`vty`	`vty`	`vty`	`vty`

`mutez` ¶

A specific type for manipulating tokens

Description

Mutez (micro-Tez) are internally represented by 64-bit signed integers. These are restricted to prevent creating a negative amount of mutez. Instructions are limited to prevent overflow and mixing them with other numerical types by mistake. They are also mandatorily checked for overflows.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`nat` ¶

An arbitrary-precision natural number

Description

Naturals are arbitrary-precision, meaning that the only size limit is gas.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`never` ¶

The empty type

Description

The empty type. Since never has no inhabitant, no value of this type is allowed to occur in a well-typed program.

The type never is the type of forbidden values. The most prominent scenario in which never is used is when implementing a contract template with no additional entrypoint. A contract template defines a set of basic entrypoints, and its parameter declaration contains a type variable for additional entrypoints in some branch of an union type, or wrapped inside an option type. Letting this type variable be never in a particular implementation indicates that the contract template has not been extended, and turns the branch in the code that processes the additional entrypoints into a forbidden branch.

Values of type never cannot occur in a well-typed program. However, they can be abstracted in the parameter declaration of a contract—or by using the LAMBDA operation—thus indicating that the corresponding branches in the code are forbidden. The type never also plays a role when introducing values of union or option type with LEFT never, RIGHT never, or NONE never. In such cases, the created values can be inspected with the operations IF_LEFT, IF_RIGHT, or IF_NONE, and the corresponding branches in the code are forbidden branches.

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values

There are no literal values of this type.

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`operation` ¶

An internal operation emitted by a contract

Description

There are no literal values of type operation. Instead, such values are created using the instructions TRANSFER_TOKENS, SET_DELEGATE and CREATE_CONTRACT.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

There are no literal values of this type.

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✘	✘	✘	✘	✘	✔

`option ty` ¶

An optional value

Description

Optional value of type ty that we note None or (Some v).

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 None


 Some "foo"

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
`ty`	`ty`	`ty`	`ty`	`ty`	`ty`	`ty`

`or ty1 ty2` ¶

A union of two types

Description

A union of two types: a value holding either a value a of type ty1 or a value b of type ty2, that we write (Left a) or (Right b).

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 (Left True)


 (Right "foo")

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`

`pair ty1 ty2` ¶

A pair or tuple of values

Description

The type pair ty1 ty2 is the type of binary pairs composed of a left element of type ty1 and a right element of type ty2. A value of type pair ty1 ty2 is written Pair x1 x2 where x1 is a value of type ty1 and x2 is a value of type ty2.

To build tuples of length greater than 2, right combs have specific optimized operations. For any n > 2, the compact notation pair t{0} t{1} ... t{n-2} t{n-1} is provided for the type of right combs pair t{0} (pair t{1} ... (pair t{n-2} t{n-1}) ...). Similarly, the compact notation Pair x{0} x{1} ... x{n-2} x{n-1} is provided for the right-comb value Pair x{0} (Pair x{1} ... (Pair x{n-2} x{n-1})...). Right-comb values can also be written using sequences; Pair x{0} x{1} ... x{n-2} x{n-1} can be written {x{0}; x{1}; ...; x{n-2}; x{n-1}}.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 (Pair 0 True)


(Pair 0 (Pair True 0x)...


 (Pair 0 True 0x)


 {0; True; 0x}

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`	`ty1` `ty2`

`sapling_state n` ¶

A Sapling state

Description

sapling_state ms is the type of Sapling states of memo-size ms.

Please see the Sapling integration page for a more comprehensive description of the Sapling protocol.

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values

{}

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✘	✘	✘	✔

`sapling_transaction n` ¶

A Sapling transaction

Description

sapling_transaction ms is the type of Sapling transactions of memo-size ms.

Please see the Sapling integration page for a more comprehensive description of the Sapling protocol.

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values

There are no literal values of this type.

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✔	✔	✔	✔

`set cty` ¶

An immutable set of comparable values of type `cty`

Description

Immutable sets of comparable values of type cty that we note as lists { item ; ... }, of course with their elements unique, and sorted by increasing order.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values

{}


 { 0 ; 3 ; 4 }

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	`cty`	`cty`	`cty`	`cty`	`cty`	`cty`

`signature` ¶

A cryptographic signature

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


"edsigthTzJ8X7MPmNeEwy...


"spsig1PPUFZucuAQybs5w...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`string` ¶

A string of characters

Description

Strings are mostly used for naming things without having to rely on external ID databases. Michelson restricts strings to the printable subset of 7-bit ASCII, namely characters with codes within the range [32, 126], plus the following escape characters: \n, \\, \". Unescaped line breaks (ASCII code point 10) are not allowed in the textual concrete syntax of strings. It must be escaped. In other words,

"foo
bar"

is not allowed and "foo\nbar" should be used instead.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 "foo"


 "ABC\n123"

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`ticket cty` ¶

A ticket used to authenticate information of type `cty`

Description

Tickets are a way for smart contracts to authenticate data with respect to a Tezos address. This authentication can then be used to build composable permission systems.

A contract can create a ticket from a comparable value and an amount. The ticket, when inspected, reveals the value, the amount, and the address of the ticketer (the contract that created the ticket). It is impossible for a contract to “forge” a ticket that appears to have been created by another ticketer.

The amount is a metadata that can be used to implement UTXOs.

Tickets cannot be duplicated using the DUP instruction.

For example, a ticket could represent a Non-Fungible Token (NFT) or a Unspent Transaction Output (UTXO) which can then be passed around and behave like a value. This process can happen without the need to interact with a centralized NFT contract, simplifying the code.

Proposed in protocol

Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example values


Pair "KT1ThEdxfUcWUwqs...


Pair "KT1ThEdxfUcWUwqs...

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✘	✔	✔	✘	✘	✔	✘

`timestamp` ¶

A real-world date.

Description

Literal timestamps are written either using RFC3339 notation in a string (readable), or as the number of seconds since Epoch in a natural (optimized).

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 "2019-09-26T10:59:51Z"

1571659294

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

`unit` ¶

The type whose only value is `Unit`

Description

The type whose only value is Unit, 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.

Available since mainnet protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Proposed in protocol

Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example values


 Unit

Related instructions

Attributes

Comparable	Passable	Storable	Pushable	Packable	big_map value	Duplicable
✔	✔	✔	✔	✔	✔	✔

Instruction Reference ¶

`ABS` ¶

Obtain the absolute value of an integer

ABS consumes an integer and pushes its absolute value, with type nat, on the stack.

Typing

Γ ⊢ ABS :: int : A ⇒ nat : A

ABS

Semantics

ABS / z : S ⇒ abs   z : S

ABS

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: `ABS` is the reverse of `NEG` on natural numbers ¶

This examples negates a natural number, takes the absolute value and asserts that the final value equals the initial parameter.

Note that this is true for any natural number, since Michelson numbers are arbitrary-precision.

try it!

parameter nat;
storage unit;
code { CAR;
       DUP; NEG; ABS; COMPARE; ASSERT_EQ;
       UNIT; NIL operation; PAIR}

`ADD` ¶

Add two numerical values

Adds numerical values. This instruction is polymorphic and accepts any combination of natural numbers and integers as operands. The return value is a natural number if both operands are natural. Otherwise, it is an integer.

Furthermore, integers can be added to timestamps in which case the return value is a timestamp offset with the integer number of seconds.

A mutez can also be added to a mutez, in which case the return value is a mutez. In this case, the operation triggers a run-time error if the sum of the mutez values overflows.

Finally, ADD can be used to add two BLS12-381 curve points (values of type bls12_381_g1 and bls12_381_g2) or two BLS-381 field elements (values of type bls12_381_fr).

Typing

Γ ⊢ ADD :: nat : nat : A ⇒ nat : A

ADD__nat_nat

Γ ⊢ ADD :: nat : int : A ⇒ int : A

ADD__nat_int

Γ ⊢ ADD :: int : nat : A ⇒ int : A

ADD__int_nat

Γ ⊢ ADD :: int : int : A ⇒ int : A

ADD__int_int

Γ ⊢ ADD :: timestamp : int : A ⇒ timestamp : A

ADD__timestamp_int

Γ ⊢ ADD :: int : timestamp : A ⇒ timestamp : A

ADD__int_timestamp

Γ ⊢ ADD :: mutez : mutez : A ⇒ mutez : A

ADD__mutez_mutez_mutez

Γ ⊢ ADD :: bls12_381_g1 : bls12_381_g1 : A ⇒ bls12_381_g1 : A

ADD__g1

Γ ⊢ ADD :: bls12_381_g2 : bls12_381_g2 : A ⇒ bls12_381_g2 : A

ADD__g2

Γ ⊢ ADD :: bls12_381_fr : bls12_381_fr : A ⇒ bls12_381_fr : A

ADD__fr

Semantics

ADD / z₁ : z₂ : S ⇒ ( z₁   +   z₂ ) : S

ADD

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Various additions ¶

This example demonstrates the addition of different types of numbers and domain specific types.

try it!

parameter unit;
storage unit;
code
  {
    CAR;

    PUSH int 2; PUSH int 2; ADD; PUSH int 4; ASSERT_CMPEQ;
    PUSH int 2; PUSH int 2; ADD; PUSH int 4; ASSERT_CMPEQ;
    PUSH int 2; PUSH nat 2; ADD; PUSH int 4; ASSERT_CMPEQ;
    PUSH nat 2; PUSH int 2; ADD; PUSH int 4; ASSERT_CMPEQ;
    PUSH nat 2; PUSH nat 2; ADD; PUSH nat 4; ASSERT_CMPEQ;

    # Offset a timestamp by 60 seconds
    PUSH int 60; PUSH timestamp "2019-09-09T12:08:37Z"; ADD;
    PUSH timestamp "2019-09-09T12:09:37Z"; ASSERT_CMPEQ;

    PUSH timestamp "2019-09-09T12:08:37Z"; PUSH int 60; ADD;
    PUSH timestamp "2019-09-09T12:09:37Z"; ASSERT_CMPEQ;

    PUSH mutez 1000; PUSH mutez 1000; ADD;
    PUSH mutez 2000; ASSERT_CMPEQ;

    NIL operation;
    PAIR;
  }

`ADDRESS` ¶

Push the address of a contract

This instruction consumes a contract value and produces the address of that contract.

Typing

Γ ⊢ ADDRESS :: contract   ty₁ : A ⇒ address : A

ADDRESS

Semantics

ADDRESS / c : S ⇒ address   c : S

ADDRESS

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Address ¶

This example takes a contract by parameter, and then stores its address.

try it!

parameter (contract unit);
storage (option address);
code {CAR; ADDRESS; SOME; NIL operation; PAIR }

If called with the initial storage None and the parameter "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv" then the final storage will be (Some "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv").

`AMOUNT` ¶

Push the amount of the current transaction

Push the amount of the current transaction, in mutez.

Typing

Γ ⊢ AMOUNT :: A ⇒ mutez : A

AMOUNT

Semantics

AMOUNT / S ⇒ amount : S

AMOUNT

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Store `AMOUNT` ¶

This contract stores the amount of its last received transaction.

try it!

parameter unit;
storage mutez;
code { DROP; AMOUNT; NIL operation; PAIR };

`AND` ¶

Boolean and bitwise AND

The instruction AND is defined on boolean, natural number and bytes operands. In the boolean case, the result is the logical AND of the operands. In the natural number and bytes cases, the result is the bitwise AND of the operands.

AND is also defined when the top operand is an int. Negative numbers are considered in two's complement representation, starting with a virtual infinite number of 1s.

When AND is used for bytes operands, the bytes result has the same length as the shorter operand. The prefix of the longer operand is cut to match with the length of the shorter one before taking the bitwise AND.

Typing

Γ ⊢ AND :: bool : bool : A ⇒ bool : A

AND__bool

Γ ⊢ AND :: nat : nat : A ⇒ nat : A

AND__nat_nat

Γ ⊢ AND :: int : nat : A ⇒ nat : A

AND__int_nat

Γ ⊢ AND :: bytes : bytes : A ⇒ bytes : A

AND__bytes

Semantics

AND / True : True : S ⇒ True : S

AND__1

AND / False : x : S ⇒ False : S

AND__2

AND / x : False : S ⇒ False : S

AND__3

AND / z₁ : z₂ : S ⇒ ( z₁   &   z₂ ) : S

AND__bit

AND / bs₁ : bs₂ : S ⇒ ( bs₁   &   bs₂ ) : S

AND__bytes

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Boolean AND ¶

This contracts takes a pair of booleans, and computes and stores their conjunction.

try it!

parameter (pair bool bool);
storage bool;
code { CAR ; UNPAIR; AND @and; NIL @noop operation; PAIR; };

If called with the initial storage False and the parameter (Pair True False) then the final storage will be False.

Example: Bitwise AND on natural numbers ¶

This contract demonstrates bitwise AND on numerical values.

try it!

parameter unit;
storage unit;
code { DROP;

       # 0101 & 0110 = 0100
       PUSH nat 5; PUSH nat 6; AND; PUSH nat 4; ASSERT_CMPEQ;

       # 0110 & 0101 = 0100
       PUSH nat 6; PUSH int 5; AND; PUSH nat 4; ASSERT_CMPEQ;

       # Negative numbers are represented as with a initial virtual
       # infinite series of 1's.
       # Hence, AND with -1 (1111...) is identity:

       #   12 = ...1100
       # & -1 = ...1111
       #   ----
       # = 12 = ...1100
       PUSH nat 12; PUSH int -1; AND; PUSH nat 12; ASSERT_CMPEQ;

       #   12 = ...0001100
       # & -5 = ...1111011
       # -----------------
       #    8 = ...0001000
       PUSH nat 12; PUSH int -5; AND; PUSH nat 8; ASSERT_CMPEQ;

       UNIT; NIL @noop operation; PAIR; };

Example: Bitwise AND on bytes ¶

This contract demonstrates bitwise AND on bytes.

try it!

parameter unit;
storage unit;
code { DROP;

       # 0x05 & 0x06 = 0x04
       PUSH bytes 0x05; PUSH bytes 0x06; AND; PUSH bytes 0x04; ASSERT_CMPEQ;

       # 0x0005 & 0x0106 = 0x0004, not 0x04
       PUSH bytes 0x0005; PUSH bytes 0x0106; AND; PUSH bytes 0x0004; ASSERT_CMPEQ;

       # Longer bytes is cut its prefix to have the same length as the shorter one
       # 0x05 & 0x0106 = 0x05 & 0x06 = 0x04, not 0x0004
       PUSH bytes 0x05; PUSH bytes 0x0106; AND; PUSH bytes 0x04; ASSERT_CMPEQ;

       UNIT; NIL @noop operation; PAIR; };

`APPLY` ¶

Partially apply a tuplified function from the stack

Partially apply a tuplified function from the stack. That is, the APPLY instruction consumes a value d of type ty1 and a value i of type lambda (Pair ty1 ty2) ty3. It partially applies the lambda to d, hence producing a new lambda of type lambda ty2 ty3 on the stack. Intuitively, this amounts to creating a new function that acts like i but with the first parameter fixed to d.

Values that are not both pushable and storable (values of type operation, contract _ and big_map _ _) cannot be captured by APPLY (cannot appear in ty1).

Typing

Γ ⊢ APPLY :: ty₁ : lambda   ( pair   ty₁   ty₂ )   ty₃ : A ⇒ lambda   ty₂   ty₃ : A

APPLY

Semantics

APPLY / d : { i : ( pair   ty₁   ty₂ ) → ty₃ } : S ⇒ { PUSH   ty₁   d ; PAIR ; i : ty₂ → ty₃ } : S

APPLY

APPLY / d : Lambda_rec   i : S ⇒ { PUSH   ty₁   d ; PAIR ; LAMBDA_REC   ty₁   ty₂   i ; SWAP ; EXEC : ty₁ → ty₂ } : S

APPLY__rec

Related types

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

`BALANCE` ¶

Push the current amount of mutez of the executing contract

Push the current amount of mutez held by the executing contract, including any mutez added by the calling transaction.

Typing

Γ ⊢ BALANCE :: A ⇒ mutez : A

BALANCE

Semantics

BALANCE / S ⇒ balance : S

BALANCE

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Store `BALANCE` ¶

This contract stores its balance after its latest received transaction.

try it!

parameter unit;
storage mutez;
code {DROP; BALANCE; NIL operation; PAIR};

`BLAKE2B` ¶

Compute a Blake2B cryptographic hash

Compute the cryptographic hash of the top of the stack using the Blake2b-256 cryptographic hash function.

Typing

Γ ⊢ BLAKE2B :: bytes : A ⇒ bytes : A

BLAKE2B

Semantics

BLAKE2B / byt : S ⇒ hash_blake2b byt : S

BLAKE2B

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Hash and store ¶

This example computes the BLAKE2B hash of the string passed as parameter and puts it in storage.

try it!

parameter string;
storage bytes;
code {CAR; PACK ; BLAKE2B; NIL operation; PAIR};

If called with the initial storage 0x and the parameter "foobar" then the final storage will be 0xc5b7e76c15ce98128a840b54c38f462125766d2ed3a6bff0e76f7f3eb415df04.

`BYTES` ¶

Encode an integer or a natural number to bytes

BYTES encodes an integer or a natural number to bytes using the big-endian encoding. For integers, negative numbers are considered in two's complement representation.

Typing

Γ ⊢ BYTES :: int : A ⇒ bytes : A

BYTES__int

Γ ⊢ BYTES :: nat : A ⇒ bytes : A

BYTES__nat

Semantics

BYTES / n : S ⇒ encode_nat_be : S

BYTES__nat

BYTES / z : S ⇒ encode_int_be : S

BYTES__int

Related types

Available since mainnet protocol: Mumbai (PtMumbai2TmsJHNGRkD8v8YDbtao7BLUC3wjASn1inAKLFCjaH1)
Proposed in protocol: Mumbai (PtMumbai2TmsJHNGRkD8v8YDbtao7BLUC3wjASn1inAKLFCjaH1)

`CAR` ¶

Access the left part of a pair

CAR destructs the pair on top of the stack and leaves only the left part of it.

Typing

Γ ⊢ CAR :: pair   ty₁   ty₂ : A ⇒ ty₁ : A

CAR

Semantics

CAR / ( Pair   d₁   d₂ ) : S ⇒ d₁ : S

CAR

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Store left parameter ¶

This contract takes a pair as parameter. It selects the left part of the parameter and stores it.

try it!

parameter (pair (nat :l) (nat :r));
storage nat;
code { CAR; CAR ; NIL operation ; PAIR }

If called with the initial storage 0 and the parameter (Pair 15 9) then the final storage will be 15.

`CDR` ¶

Access the right part of a pair

CDR destructs the pair on top of the stack and leaves only the right part of it.

Typing

Γ ⊢ CDR :: pair   ty₁   ty₂ : A ⇒ ty₂ : A

CDR

Semantics

CDR / ( Pair   d₁   d₂ ) : S ⇒ d₂ : S

CDR

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Store right part of the parameter ¶

This contract takes a pair as parameter. It selects the right part of the parameter and stores it.

try it!

parameter (pair (nat :l) (nat :r));
storage nat;
code { CAR; CDR ; NIL operation ; PAIR }

If called with the initial storage 0 and the parameter (Pair 15 9) then the final storage will be 9.

`CHAIN_ID` ¶

Push the chain identifier

This instruction pushes on the stack the identifier of the chain on which the smart contract is executed.

The chain identifier is designed to prevent replay attacks between the main chain and the test chain forked during amendement exploration, where contract addresses and storages are identical.

The value is derived from the genesis block hash and will thus be different on the main chains of different networks and on the test chains on which the value depends on the first block of the testchain.

Typing

Γ ⊢ CHAIN_ID :: A ⇒ chain_id : A

CHAIN_ID

Semantics

CHAIN_ID / S ⇒ chain_id : S

CHAIN_ID

Related types

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

Example: Push the chain identifier ¶

This contract pushes and then stores the chain identifier.

try it!

parameter unit;
storage (option chain_id);
code { DROP; CHAIN_ID; SOME; NIL operation; PAIR }

In case this example is executed using mockup mode, with the initial storage None and the parameter Unit then the final storage will be (Some "NetXynUjJNZm7wi").

`CHECK_SIGNATURE` ¶

Verify `signature` of `bytes` by `key`

Verifies that a byte sequence has been signed with a given key. This instruction consumes three operands: a key, a signature and a byte sequence bytes. It pushes True if and only if the signature is a valid signature of the byte sequence created with the given key.

Typing

Γ ⊢ CHECK_SIGNATURE :: key : signature : bytes : A ⇒ bool : A

CHECK_SIGNATURE

Semantics

CHECK_SIGNATURE / s : sig : byt : S ⇒ check_signature   s   sig   byt : S

CHECK_SIGNATURE

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Check signature ¶

This contract stores a signature and a string. It takes a key as parameter and runs successfully if the stored signature is a valid signature of the BLAKE2B hash of the stored string by that key.

try it!

parameter key;
storage (pair signature string);
code {
       DUP; DUP;
       DIP{ CDR; DUP; CAR;
            DIP{CDR; PACK}};
       CAR; CHECK_SIGNATURE;
       IF {} {FAIL} ;
       CDR; NIL operation ; PAIR};

If called with the initial storage (Pair "edsigu3QszDjUpeqYqbvhyRxMpVFamEnvm9FYnt7YiiNt9nmjYfh8ZTbsybZ5WnBkhA7zfHsRVyuTnRsGLR6fNHt1Up1FxgyRtF" "hello") and the parameter "edpkuBknW28nW72KG6RoHtYW7p12T6GKc7nAbwYX5m8Wd9sDVC9yav" then the final storage will be (Pair "edsigu3QszDjUpeqYqbvhyRxMpVFamEnvm9FYnt7YiiNt9nmjYfh8ZTbsybZ5WnBkhA7zfHsRVyuTnRsGLR6fNHt1Up1FxgyRtF" "hello").

`COMPARE` ¶

Compare two values

Comparison only works on a class of types that we call comparable. The COMPARE instruction is defined in an ad hoc way for each comparable type, but the result of COMPARE is always an int, which can in turn be checked in a generic manner using the EQ, NEQ, LT, GT, LE and GE combinators.

The result of COMPARE is 0 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.

string, bytes, key_hash, key, signature, chain_id values are compared lexicographically.
address values are compared as follows:
- addresses of implicit accounts are strictly less than addresses of originated accounts
- addresses of the same type are compared lexicographically
pair values (Pair d1 d2) are compared component-wise, starting with the left component.
nat, int, mutez and timestamp values are compared numerically
comparison for type unit always returns 0
bool values are compared so that False is strictly less than True
option-al values are compared as follows:
- None is strictly less than any Some x,
- Some x and Some y are compared as x and y.
values of union types built with or are compared as follows:
- any Left x is smaller than any Right y,
- Left x and Left y are compared as x and y,
- Right x and Right y are compared as x and y.
comparison for type never is defined with no implementation as it is never executed.

Typing

Γ ⊢ COMPARE :: cty : cty : A ⇒ int : A

COMPARE

Semantics

z₁ < z₂

COMPARE / z₁ : z₂ : S ⇒ − 1 : S

COMPARE__num_lt

z₁ = z₂

COMPARE / z₁ : z₂ : S ⇒ 0 : S

COMPARE__num_eq

z₁ > z₂

COMPARE / z₁ : z₂ : S ⇒ 1 : S

COMPARE__num_gt

s < t

COMPARE / s : t : S ⇒ − 1 : S

COMPARE__string_lt

s = t

COMPARE / s : t : S ⇒ 0 : S

COMPARE__string_eq

s > t

COMPARE / s : t : S ⇒ 1 : S

COMPARE__string_gt

COMPARE / d₁ : d₃ : S ⇒ − 1 : S

COMPARE / ( Pair   d₁   d₂ ) : ( Pair   d₃   d₄ ) : S ⇒ − 1 : S

COMPARE__pair_left_lt

COMPARE / d₁ : d₃ : S ⇒ 1 : S

COMPARE / ( Pair   d₁   d₂ ) : ( Pair   d₃   d₄ ) : S ⇒ 1 : S

COMPARE__pair_left_gt

COMPARE / d₁ : d₃ : S ⇒ 0 : S

COMPARE / d₂ : d₄ : S ⇒ z : S

COMPARE / ( Pair   d₁   d₂ ) : ( Pair   d₃   d₄ ) : S ⇒ z : S

COMPARE__pair_right

COMPARE / False : False : S ⇒ 0 : S

COMPARE__false_false

COMPARE / False : True : S ⇒ − 1 : S

COMPARE__false_true

COMPARE / True : True : S ⇒ 0 : S

COMPARE__true_true

COMPARE / True : False : S ⇒ 1 : S

COMPARE__true_false

COMPARE / None : None : S ⇒ 0 : S

COMPARE__none_none

COMPARE / None : Some   d : S ⇒ − 1 : S

COMPARE__none_some

COMPARE / d₁ : d₂ : S ⇒ z : S

COMPARE / Some   d₁ : Some   d₂ : S ⇒ z : S

COMPARE__some_some

COMPARE / Some   d : None : S ⇒ 1 : S

COMPARE__some_none

COMPARE / d₁ : d₂ : S ⇒ z : S

COMPARE / Left   d₁ : Left   d₂ : S ⇒ z : S

COMPARE__left_left

COMPARE / Left   d₁ : Right   d₂ : S ⇒ − 1 : S

COMPARE__left_right

COMPARE / d₁ : d₂ : S ⇒ z : S

COMPARE / Right   d₁ : Right   d₂ : S ⇒ z : S

COMPARE__right_right

COMPARE / Right   d₁ : Left   d₂ : S ⇒ 1 : S

COMPARE__right_left

COMPARE / Unit : Unit : S ⇒ 0 : S

COMPARE__unit_unit

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: A variety of comparisons ¶

This contract demonstrate several types of comparisons over different values.

try it!

parameter unit;
storage unit;
code {
       DROP;

       # bool
       PUSH bool True; DUP; COMPARE; ASSERT_EQ;
       PUSH bool False; DUP; COMPARE; ASSERT_EQ;
       PUSH bool False; PUSH bool True; COMPARE; ASSERT_GT;
       PUSH bool True; PUSH bool False; COMPARE; ASSERT_LT;

       # bytes
       PUSH bytes 0xAABBCC; DUP; COMPARE; ASSERT_EQ;
       PUSH bytes 0x; PUSH bytes 0x; COMPARE; ASSERT_EQ;
       PUSH bytes 0x; PUSH bytes 0x01; COMPARE; ASSERT_GT;
       PUSH bytes 0x01; PUSH bytes 0x02; COMPARE; ASSERT_GT;
       PUSH bytes 0x02; PUSH bytes 0x01; COMPARE; ASSERT_LT;

       # int
       PUSH int 1; DUP; COMPARE; ASSERT_EQ;
       PUSH int 10; PUSH int 5; COMPARE; ASSERT_LT;
       PUSH int -4; PUSH int 1923; COMPARE; ASSERT_GT;

       # nat
       PUSH nat 1; DUP; COMPARE; ASSERT_EQ;
       PUSH nat 10; PUSH nat 5; COMPARE; ASSERT_LT;
       PUSH nat 4; PUSH nat 1923; COMPARE; ASSERT_GT;

       # key_hash
       PUSH key_hash "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx"; DUP; COMPARE; ASSERT_EQ;
       PUSH key_hash "tz1ddb9NMYHZi5UzPdzTZMYQQZoMub195zgv"; PUSH key_hash "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx"; COMPARE; ASSERT_LT;
       PUSH key_hash "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx"; PUSH key_hash "tz1ddb9NMYHZi5UzPdzTZMYQQZoMub195zgv"; COMPARE; ASSERT_GT;

       # mutez
       PUSH mutez 1; DUP; COMPARE; ASSERT_EQ;
       PUSH mutez 10; PUSH mutez 5; COMPARE; ASSERT_LT;
       PUSH mutez 4; PUSH mutez 1923; COMPARE; ASSERT_GT;

       # string
       PUSH string "AABBCC"; DUP; COMPARE; ASSERT_EQ;
       PUSH string ""; PUSH string ""; COMPARE; ASSERT_EQ;
       PUSH string ""; PUSH string "a"; COMPARE; ASSERT_GT;
       PUSH string "a"; PUSH string "b"; COMPARE; ASSERT_GT;
       PUSH string "b"; PUSH string "a"; COMPARE; ASSERT_LT;

       # timestamp
       PUSH timestamp "2019-09-16T08:38:05Z"; DUP; COMPARE; ASSERT_EQ;
       PUSH timestamp "2017-09-16T08:38:04Z"; PUSH timestamp "2019-09-16T08:38:05Z"; COMPARE; ASSERT_GT;
       PUSH timestamp "2019-09-16T08:38:05Z"; PUSH timestamp "2019-09-16T08:38:04Z"; COMPARE; ASSERT_LT;

       UNIT; NIL operation; PAIR;
     }

If called with the initial storage Unit and the parameter Unit then the final storage will be Unit.

`CONCAT` ¶

Concatenate strings or byte sequences

The CONCAT operator exists in four variants:

The first version takes two string operands and pushes their concatenation, as a string.

The second takes a list of strings and pushes the concatenation of all strings in the list, as a string.

The third version takes two byte sequences and pushes their concatenation, as a byte sequence.

The fourth version takes a list of byte sequences and pushes the concatenation of all byte sequences in the list, as a byte sequence.

Typing

Γ ⊢ CONCAT :: string : string : A ⇒ string : A

CONCAT__string

Γ ⊢ CONCAT :: list   string : A ⇒ string : A

CONCAT__string_list

Γ ⊢ CONCAT :: bytes : bytes : A ⇒ bytes : A

CONCAT__bytes

Γ ⊢ CONCAT :: list   bytes : A ⇒ bytes : A

CONCAT__bytes_list

Semantics

CONCAT / s : t : S ⇒ s ^ t : S

CONCAT__string

CONCAT / {} : S ⇒ "" : S

CONCAT__string_list_nil

CONCAT / tl : S ⇒ t : S

CONCAT / { s ; < tl > } : S ⇒ s ^ t : S

CONCAT__string_list_cons

CONCAT / byt₁ : byt₂ : S ⇒ byt₁ ^ byt₂ : S

CONCAT__bytes

CONCAT / {} : S ⇒ 0x : S

CONCAT__bytes_list_nil

CONCAT / tl : S ⇒ byt₂ : S

CONCAT / { byt₁ ; < tl > } : S ⇒ byt₁ ^ byt₂ : S

CONCAT__bytes_list_cons

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Concatenation of two strings ¶

This example takes a list of strings as parameter. It prepends "Hello " to each of them and stores the result.

try it!

parameter (list string);
storage (list string);
code{ CAR;
      MAP { PUSH @hello string "Hello "; CONCAT }; NIL operation; PAIR};

If called with the initial storage {} and the parameter { "John" ; "Jane" } then the final storage will be { "Hello John" ; "Hello Jane" }.

Example: Concatenation of list of strings ¶

This example takes a list of strings as parameter and concatenates them, and prepends value in storage and stores the resulting string.

try it!

parameter (list string);
storage string;
code { UNPAIR ; SWAP ; CONS ; CONCAT; NIL operation; PAIR}

If called with the initial storage "Hello" and the parameter { " " ; "World" ; "!" } then the final storage will be "Hello World!".

Example: Concatenation of two byte sequences ¶

This example takes a list of byte sequences as parameter. It prepends 0xff to each of them and stores the result.

try it!

parameter (list bytes);
storage (list bytes);
code{ CAR;
      MAP { PUSH bytes 0xFF; CONCAT }; NIL operation; PAIR};

If called with the initial storage {} and the parameter { 0xab ; 0xcd } then the final storage will be { 0xffab ; 0xffcd }.

Example: Concatenation of list of byte sequences ¶

This example takes a list of byte sequences as parameter and concatenates them, and prepends the value in storage and stores the resulting byte sequence.

try it!

parameter (list bytes);
storage bytes;
code { UNPAIR ; SWAP ; CONS ; CONCAT; NIL operation; PAIR}

If called with the initial storage 0xdead and the parameter { 0xbe ; 0xef } then the final storage will be 0xdeadbeef.

`CONS` ¶

Prepend an element to a list

Prepends the element at the top of the stack to the list that is the second element of the stack.

Typing

Γ ⊢ CONS :: ty₁ : list   ty₁ : A ⇒ list   ty₁ : A

CONS

Semantics

CONS / d : tl : S ⇒ { d ; < tl > } : S

CONS

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Prepend to storage ¶

This contracts keeps a list of integers in storage and takes an integer as parameter. It prepends the parameter to the stored list.

try it!

parameter int;
storage (list int);
code { UNPAIR; CONS; NIL operation; PAIR; };

If called with the initial storage { 99 } and the parameter 5 then the final storage will be { 5 ; 99 }.

`CONTRACT ty` ¶

Cast an address to a typed contract

Casts from an address to a typed contract ty. If and only if the address is a valid Tezos contract address with the type ty, then the result Some contract is pushed. If the address belongs to an implicit contract, then the type parameter ty must be unit or ticket ty' for some ty' type. The behavior of the instruction for smart rollup addresses is the same as for originated contracts. If any of these conditions is not fulfilled, None is pushed.

The CONTRACT ty instruction has a variant CONTRACT %entrypoint ty. It allows the specification of a specific entrypoint. In addition to the requirements above, this variant is only well-typed if the address is a contract with an entrypoint named %entrypoint. This works as follows, where we also introduce the predicates that are referenced in the semantics rules:

input address instruction output contract predicate

"addr" CONTRACT t None if addr does not exist no_contract "addr" holds

"addr" CONTRACT t None if addr exists, but has a default entrypoint not of type t, or has no default entrypoint and parameter is not of type t invalid_contract_type "addr" t holds

"addr%name" CONTRACT t None if addr does not exist, or exists but does not have a name entrypoint no_contract "addr%name" holds

"addr" CONTRACT %name t

"addr%name" CONTRACT t None if addr exists, but has an entrypoint name not of type t invalid_contract_type "addr%name" t holds

"addr" CONTRACT %name t

"addr%name1" CONTRACT %name2 t None entrypoint_ambiguity "addr%name1" "name2" holds

"addr" CONTRACT t (Some "addr") if contract exists, has a default entrypoint of type t, or has no default entrypoint and parameter type t valid_contract_type "addr" t holds

"addr%name" CONTRACT t (Some "addr%name") if addr exists and has an entrypoint name of type t valid_contract_type "addr%name" t holds

"addr" CONTRACT %name t

Note that CONTRACT ty is strictly equivalent to CONTRACT %default ty, and for clarity, the second variant is forbidden in the concrete syntax.

Typing

Γ ⊢ CONTRACT   ty :: address : A ⇒ option   ( contract   ty ) : A

CONTRACT

Semantics

valid_contract_type   addr   ty

CONTRACT   ty / addr : S ⇒ Some   ( contract   ty   addr ) : S

CONTRACT__ok

no_contract   addr

CONTRACT   ty / addr : S ⇒ None : S

CONTRACT__fail_ex

invalid_contract_type   addr   ty

CONTRACT   ty / addr : S ⇒ None : S

CONTRACT__fail_ty

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: From `address` to `contract` ¶

This contract receives an address by parameter, and converts it to a contract unit.

try it!

parameter address;
storage unit;
code {
       CAR;
       CONTRACT unit;
       ASSERT_SOME;
       DROP;
       UNIT;
       NIL operation;
       PAIR
     };

If called with the initial storage Unit and the parameter "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv" then the final storage will be Unit.

Example: Using `contract` with entrypoint annotations ¶

When this contract is called by anyone except itself, it originates a new contract with three entrypoints: add, sub and default and saves its address in its storage. It then emits a transaction to itself.

When the contract receives a transaction from itself, it verifies that the stored address can be converted to a contract for each of the entrypoints add, sub and default with the respective types nat, nat and unit using the CONTRACT instruction annotated with the respective entrypoint. It verifies that the entrypoint default has the type unit, and that this is equivalent to to using CONTRACT with no entrypoint annotation. It also emits transactions to these entrypoints.

try it!

{ parameter unit ;
  storage (option address) ;
  code { SENDER ; SELF ; ADDRESS ;
         IFCMPEQ
           { CDR ; ASSERT_SOME ;
             DIP { NIL operation } ;
             DUP ; CONTRACT %add unit ; ASSERT_NONE ;
             DUP ; CONTRACT %fact nat ; ASSERT_NONE ;
             DUP ; CONTRACT %add nat ; ASSERT_SOME ; PUSH mutez 0 ; PUSH nat 12 ; TRANSFER_TOKENS ; SWAP ; DIP { CONS } ;
             DUP ; CONTRACT unit ; ASSERT_SOME ; PUSH mutez 0 ; PUSH unit Unit ; TRANSFER_TOKENS ; SWAP ; DIP { CONS } ;
             DUP ; CONTRACT %sub nat ; ASSERT_SOME ; PUSH mutez 0 ; PUSH nat 3 ; TRANSFER_TOKENS ; SWAP ; DIP { CONS } ;
             DUP ; CONTRACT %add nat ; ASSERT_SOME ; PUSH mutez 0 ; PUSH nat 5 ; TRANSFER_TOKENS ; SWAP ; DIP { CONS } ;
             DROP ; DIP { NONE address } ; PAIR }
           { CAR ; DUP ;
             DIP
               { DIP { PUSH int 0 ; PUSH mutez 0 ; NONE key_hash } ;
                 DROP ;
                 CREATE_CONTRACT
                   { parameter (or (or (nat %add) (nat %sub)) (unit %default)) ;
                     storage int ;
                     code { AMOUNT ; PUSH mutez 0 ; ASSERT_CMPEQ ;
                            UNPAIR ;
                            IF_LEFT
                              { IF_LEFT { ADD } { SWAP ; SUB } }
                              { DROP ; DROP ; PUSH int 0 } ;
                            NIL operation ; PAIR } } } ;
             DIP { SELF ; PUSH mutez 0 } ; TRANSFER_TOKENS ;
             NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
             DIP { SOME } ; PAIR } } }

`CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 }` ¶

Push a contract creation operation

Push a contract creation operation (an origination) based on a script literal. The operands are the optional delegate, the initial amount taken from the currently executed contract, and the initial storage of the originated contract. Along with the origination operation, the contract's address is also returned as a first-class value (to be dropped, passed as parameter or stored).

The CONTRACT 'p instruction applied to this resulting address will return None until the contract is actually originated, that is, after the generated operation is applied. It follows that a contract cannot directly return a list of operations that creates a contract, and call it immediately after. However, a contract A creating a contract B will get its address, so it can return a list of operations that first originates the contract B, and then calls a contract which in turns calls B: B's address being either stored in A's storage or passed as parameter, the executions following B's origination can use CONTRACT 'p on B's address in order to call it.

Similarly to the SET_DELEGATE instruction, the execution of CREATE_CONTRACT never fails but the origination operation it produces fails at application if the provided optional delegate does not point to a registered delegate. In particular, since tz4 addresses cannot be registered as delegates, the origination operation will fail if the delegate is a tz4 address. The origination operation also fails if the initial balance of the originated contract cannot be debited from the balance of the originator contract.

Typing

Some   ty₁ ⊢ instr₁ :: pair   ty₁   ty₂ : [ ] ⇒ pair   ( list   operation )   ty₂ : [ ]

Γ ⊢ CREATE_CONTRACT   {   parameter   ty₁ ;   storage   ty₂ ;   code   instr₁ } :: option   key_hash : mutez : ty₂ : A ⇒ operation : address : A

CREATE_CONTRACT

Semantics

create_contract   ty₁   ty₂   instr₁   kh   z   x = ( op , addr )

CREATE_CONTRACT   {   parameter   ty₁ ;   storage   ty₂ ;   code   instr₁ } / kh : z : x : S ⇒ op : addr : S

CREATE_CONTRACT

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Originate a dummy contract ¶

This contract originates a dummy contract.

try it!

parameter unit;
storage (option address);
code { DROP;
       UNIT; # starting storage for contract
       AMOUNT;                   # Push the starting balance
       NONE key_hash;                 # No delegate
       CREATE_CONTRACT          # Create the contract
         { parameter unit ;
           storage unit ;
           code
             { CDR;
               NIL operation;
               PAIR; } };
       DIP {SOME;NIL operation};CONS ; PAIR} # Ending calling convention stuff

The final storage will be (Some addr) where addr is the fresh address of the originated contract.

Example: Originate and call ¶

This contract originate a contract and then call itself after the application of the origination operation, with the address of the contract, to call it.

The execution order is thus

call A with None
originate B
call A with (Some B)
call B with "abcdefg"

try it!

parameter (option address) ;
storage unit ;
code { CAR ;
       IF_NONE
         { PUSH string "dummy" ;
           PUSH mutez 100000000 ; NONE key_hash ;
           CREATE_CONTRACT
             { parameter string ;
               storage string ;
               code { CAR ; NIL operation ; PAIR } } ;
           DIP { SOME ; DIP { SELF ; PUSH mutez 0 } ; TRANSFER_TOKENS ;
                 NIL operation ; SWAP ; CONS } ;
           CONS ; UNIT ; SWAP ; PAIR }
         { SELF ; ADDRESS ; SENDER ; IFCMPNEQ { FAIL } {} ;
           CONTRACT string ; IF_SOME {} { FAIL } ;
           PUSH mutez 0 ; PUSH string "abcdefg" ; TRANSFER_TOKENS ;
           NIL operation; SWAP; CONS ; UNIT ; SWAP ; PAIR } } ;

`DIG n` ¶

Retrieve the `n`th element of the stack

DIG n consumes a stack that contains at least n elements. It moves the nth element of the stack to the top of the stack. The element on top of the stack is the 0th element, so that DIG 0 is a no-op, and DIG 1 is equivalent to SWAP. In other words, DIG n transforms a stack on the form x1 : ... : xn : y : ... into the stack y : x1 : ... : xn : ....

The inverse of DIG is DUG.

Typing

length   A = n

Γ ⊢ DIG   n :: A @ ( ty₁ : B ) ⇒ ty₁ : ( A @ B )

DIG

Semantics

length   S₁ = n

DIG   n / S₁ ++ ( d : S₂ ) ⇒ d : ( S₁ ++ S₂ )

DIG

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

`DIP instr` ¶

Run code protecting the top of the stack

DIP instr runs instr protecting the top element of the stack.

Typing

Γ ⊢ instr :: B ⇒ C

Γ ⊢ DIP   instr :: ty : B ⇒ ty : C

DIP

Semantics

instr / S ⇒ S′

DIP   instr / d : S ⇒ d : S′

DIP

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: ¶

This examples takes a pair of integers (a, b) as parameter, and stores (a, a + b)

try it!

parameter (pair nat nat);
storage (pair nat nat);
code{
      CAR; UNPAIR;
      DUP; DIP { ADD };
      PAIR;
      NIL operation;
      PAIR};

If called with the initial storage (Pair 0 0) and the parameter (Pair 15 9) then the final storage will be (Pair 15 24).

`DIP n instr` ¶

Run code protecting the `n` topmost elements of the stack

DIP n instr runs instr protecting the n topmost elements of the stack. In particular, DIP 0 instr is equivalent to instr and DIP 1 instr is equivalent to DIP instr.

Typing

length   A = n

Γ ⊢ instr :: B ⇒ C

Γ ⊢ DIP   n   instr :: A @ B ⇒ A @ C

DIPN

Semantics

length   S₁ = n

instr / S₂ ⇒ S₃

DIP   n   instr / S₁ ++ S₂ ⇒ S₁ ++ S₃

DIPN

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

Example: ¶

This example builds a stack of size 5 by calling UNPAIR 4 times, then inserts the value 6 at the bottom of the stack using DIP 5, discards all the stack elements but the last one using several DROP and finally stores the bottom element.

try it!

parameter (pair (pair (pair (pair nat nat) nat) nat) nat);
storage nat;
code {CAR; UNPAIR ; UNPAIR ; UNPAIR ; UNPAIR ; DIP 5 {PUSH nat 6} ; DROP ; DROP ; DROP ; DROP ; DROP ; NIL operation; PAIR};

If called with the initial storage 0 and the parameter (Pair (Pair (Pair (Pair 1 2) 3) 4) 5) then the final storage will be 6.

`DROP` ¶

Drop the top element of the stack

Typing

Γ ⊢ DROP :: ty : A ⇒ A

DROP

Semantics

DROP / d : S ⇒ S

DROP

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`DROP n` ¶

Drop the top `n` elements of the stack

DROP n drops the n topmost elements of the stack. In particular, DROP 0 is a noop and DROP 1 is equivalent to DROP.

Typing

length   A = n

Γ ⊢ DROP   n :: A @ B ⇒ B

DROPN

Semantics

length   S₁ = n

DROP   n / S₁ ++ S₂ ⇒ S₂

DROPN

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

`DUG n` ¶

Insert the top element at depth `n`

DUG n consumes a stack that contains at least n elements. It removes the top element of the stack, and inserts it at the nth level in the stack. The element on top of the stack is at depth 0 so that DUG 0 is a no-op and DUG 1 is equivalent to SWAP. In other words, DUG n transforms a stack on the form y : x1 : ... : xn : ... into the stack x1 : ... : xn : y : ....

The inverse of DUG is DIG.

Typing

length   A = n

Γ ⊢ DUG   n :: ty₁ : ( A @ B ) ⇒ A @ ( ty₁ : B )

DUG

Semantics

length   S₁ = n

DUG   n / d : ( S₁ ++ S₂ ) ⇒ S₁ ++ ( d : S₂ )

DUG

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

`DUP` ¶

Duplicate the top of the stack

Typing

Γ ⊢ DUP :: ty₁ : A ⇒ ty₁ : ty₁ : A

DUP

Semantics

DUP / d : S ⇒ d : d : S

DUP

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`DUP n` ¶

Duplicate the `n`th element of the stack

DUP n consumes a stack that contains at least n elements. It duplicates the nth element of the stack and pushes the duplicate at the top of the stack leaving a copy at its original position. The element on top of the initial stack is the first element, so that DUP 1 is equivalent to DUP. DUP 0 is forbidden. In other words, DUP n transforms a stack on the form x1 : ... : xn : ... into the stack xn : x1 : ... : xn : ....

`EDIV` ¶

Euclidean division

Consumes two numbers z1 and z2 (of either int or nat). It returns None if z2 is zero, otherwise, it returns Some (Pair q r), where q = z1 / z2 and r = z1 mod z2, such that q * z2 + r = z1, and 0 ≤ r < |z2|.

Conventions for integer division vary between programming languages. Michelson uses the mathematical convention of the Euclidian division. That is, the remainder r is always non-negative. This remainder is canonical in the sense that to test if two integers a and b are congruent modulo some modulus c it is enough to test if a mod c and b mod c are equal. Moreover, the direction toward which the quotient is rounded is determined by the signs of z1 and z2: it is rounded toward 0 if and only if z1 is positive and it is rounded down if and only if z2 is positive.

`z1`	`z2`	Results
`13`	`3`	`Some (Pair 4 1)`
`-13`	`3`	`Some (Pair -5 2)`
`13`	`-3`	`Some (Pair -4 1)`
`-13`	`-3`	`Some (Pair 5 2)`
`13`	`0`	`None`

Furthermore, values of type mutez can be divided by values of types nat or mutez.

Typing

Γ ⊢ EDIV :: nat : nat : A ⇒ option   ( pair   nat   nat ) : A

EDIV__nat_nat

Γ ⊢ EDIV :: nat : int : A ⇒ option   ( pair   int   nat ) : A

EDIV__nat_int

Γ ⊢ EDIV :: int : nat : A ⇒ option   ( pair   int   nat ) : A

EDIV__int_nat

Γ ⊢ EDIV :: int : int : A ⇒ option   ( pair   int   nat ) : A

EDIV__int_int

Γ ⊢ EDIV :: mutez : nat : A ⇒ option   ( pair   mutez   mutez ) : A

EDIV__mutez_nat

Γ ⊢ EDIV :: mutez : mutez : A ⇒ option   ( pair   nat   mutez ) : A

EDIV__mutez_mutez

Semantics

EDIV / z₁ : 0 : S ⇒ None : S

EDIV__0

z₂ ≠ 0

EDIV / z₁ : z₂ : S ⇒ Some   ( Pair   ( z₁   /   z₂ )   ( z₁   %   z₂ ) ) : S

EDIV

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`EMIT ty` ¶

Write an event into the transaction receipt

Construct an operation that will write an event into the transaction receipt after the successful execution of this contract. The general form of the instruction is EMIT %tag ty: it accepts as arguments an optional annotation as a tag to the emitted event and the type of data attachment. The type is also optional; if omitted, the type of the topmost element of the stack is used. Only values of packable types can be emitted.

See Event for more information.

Typing

Γ ⊢ EMIT   ty :: ty : A ⇒ operation : A

EMIT

Semantics

EMIT   ty / d : S ⇒ emit   d : S

EMIT

Related types

Available since mainnet protocol: Kathmandu (PtKathmankSpLLDALzWw7CGD2j2MtyveTwboEYokqUCP4a1LxMg)
Proposed in protocol: Kathmandu (PtKathmankSpLLDALzWw7CGD2j2MtyveTwboEYokqUCP4a1LxMg)

`EMPTY_BIG_MAP kty vty` ¶

Build a new, empty `big_map` from `kty` to `vty`

Build a new, empty map from keys of a given type kty to values of the other given type vty.

The cty type must be comparable. The vty type cannot be a operation or big_map.

Typing

Γ ⊢ EMPTY_BIG_MAP   kty   vty :: A ⇒ big_map   kty   vty : A

EMPTY_BIG_MAP

Semantics

EMPTY_BIG_MAP   kty   vty / S ⇒ {} : S

EMPTY_BIG_MAP

Related types

Available since mainnet protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Proposed in protocol: Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)

`EMPTY_MAP kty vty` ¶

Build a new, empty `map` from `kty` to `vty`

Build a new, empty map from keys of a given type kty to values of the other given type vty.

The kty type must be comparable.

Typing

Γ ⊢ EMPTY_MAP   kty   vty :: A ⇒ map   kty   vty : A

EMPTY_MAP

Semantics

EMPTY_MAP   kty   vty / S ⇒ {} : S

EMPTY_MAP

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`EMPTY_SET cty` ¶

Build a new, empty set for elements of type `cty`

Build a new, empty set for elements of a given type cty.

The cty type must be comparable.

Typing

Γ ⊢ EMPTY_SET   cty :: A ⇒ set   cty : A

EMPTY_SET

Semantics

EMPTY_SET   cty / S ⇒ {} : S

EMPTY_SET

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`EQ` ¶

Check that the top of the stack equals zero

The EQ instruction consumes an integer and leaves True on the stack if it is 0 and False otherwise.

It is typically composed with COMPARE: the instruction sequence COMPARE; EQ leaves True on the stack if the two top stack elements are equal, and False otherwise.

Typing

Γ ⊢ EQ :: int : A ⇒ bool : A

Semantics

EQ / 0 : S ⇒ True : S

EQ__tt

z ≠ 0

EQ / z : S ⇒ False : S

EQ__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`EXEC` ¶

Execute a function from the stack

The EXEC instruction consumes a value x of type a and a value f of type lambda a b, applies the lambda to x and leaves the results, of type b, on the stack.

Typing

Γ ⊢ EXEC :: ty₁ : lambda   ty₁   ty₂ : A ⇒ ty₂ : A

EXEC

Semantics

i / d₁ : [ ] ⇒ d₂ : [ ]

EXEC / d₁ : { i : ty₁ → ty₂ } : S ⇒ d₂ : S

EXEC

i / d₁ : Lambda_rec   i : [ ] ⇒ d₂ : [ ]

EXEC / d₁ : Lambda_rec   i : S ⇒ d₂ : S

EXEC__rec

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`FAILWITH` ¶

Explicitly abort the current program

This instruction aborts the current program exposing the top element of the stack, which must be of a packable type, in its error message. It makes the output useless since all subsequent instructions will simply ignore their usual semantics to propagate the failure up to the main result. Its type is thus completely generic.

Typing

Γ ⊢ FAILWITH :: ty₁ : A ⇒ B

FAILWITH

Semantics

FAILWITH / d : stack ⇒ [FAILED]

FAILWITH

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`GE` ¶

Check that the top of the stack is greater than or equal to zero

The GE instruction consumes an integer and leaves True on the stack if it is greater than or equal to 0 and False otherwise.

It is typically composed with COMPARE: the instruction sequence COMPARE; GE leaves True on the stack if the first stack element is greater than or equal to the second, and False otherwise.

Typing

Γ ⊢ GE :: int : A ⇒ bool : A

Semantics

z ≥ 0

GE / z : S ⇒ True : S

GE__tt

z < 0

GE / z : S ⇒ False : S

GE__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`GET` ¶

Access an element in a `map` or `big_map`

The instruction GET consumes a key and a map or big_map and returns an optional value: None if the key is not present in the data structure, and Some v if it is present and mapped to v.

Typing

Γ ⊢ GET :: kty : map   kty   vty : A ⇒ option   vty : A

GET__map

Γ ⊢ GET :: kty : big_map   kty   vty : A ⇒ option   vty : A

GET__big_map

Semantics

GET / x : {} : S ⇒ None : S

GET__empty

COMPARE / x : k : [ ] ⇒ 1 : [ ]

GET / x : m : S ⇒ opt_y : S

GET / x : { Elt   k   v ; < m > } : S ⇒ opt_y : S

GET__later

COMPARE / x : k : [ ] ⇒ 0 : [ ]

GET / x : { Elt   k   v ; < m > } : S ⇒ Some   v : S

GET__now

COMPARE / x : k : [ ] ⇒ − 1 : [ ]

GET / x : { Elt   k   v ; < m > } : S ⇒ None : S

GET__nexists

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`GET n` ¶

Access an element or a sub comb in a right comb

The nodes of a right comb of size n are canonically numbered as follows:

    0
  /   \
1       2
      /   \
    3       4
          /   \
        5       ...
                     2n-4
                   /      \
              2n-3          2n-2

Or in plain English:

The root is numbered 0,

The left child of the node numbered k is numbered k+1, and

The right child of the node numbered k is numbered k+2.

The GET k instruction accesses the node numbered k. In particular, for a comb of size n, the n-1 first elements are accessed by GET 1, GET 3, ..., and GET (2n-3) and the last element is accessed by GET (2n-2). Thus, odd numbers are used to get the fields of the comb (except the last one), and even numbers are used to get sub-combs and the last field.

Typing

Γ ⊢ GET   0 :: ty : A ⇒ ty : A

GETN__0

Γ ⊢ GET   1 :: pair   ty₁   ty₂ : A ⇒ ty₁ : A

GETN__1

Γ ⊢ GET   n :: ty₂ : A ⇒ ty : A

Γ ⊢ GET   ( n   +   2 ) :: pair   ty₁   ty₂ : A ⇒ ty : A

GETN__ind

Semantics

GET   0 / d : S ⇒ d : S

GETN__0

GET   1 / Pair   d   d′ : S ⇒ d : S

GETN__1

GET   n / d₂ : S ⇒ d : S

GET   ( n   +   2 ) / Pair   d₁   d₂ : S ⇒ d : S

GETN__ind

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`GET_AND_UPDATE` ¶

A combination of the `GET` and `UPDATE` instructions

This instruction is similar to UPDATE but it also returns the value that was previously stored in the map or big_map at the same key as GET would.

Typing

Γ ⊢ GET_AND_UPDATE :: kty : option   vty : map   kty   vty : A ⇒ option   vty : map   kty   vty : A

GET_AND_UPDATE__map

Γ ⊢ GET_AND_UPDATE :: kty : option   vty : big_map   kty   vty : A ⇒ option   vty : big_map   kty   vty : A

GET_AND_UPDATE___big_map

Semantics

GET_AND_UPDATE / x : None : {} : S ⇒ None : {} : S

GET_AND_UPDATE__empty_none

GET_AND_UPDATE / x : Some   y : {} : S ⇒ None : { Elt   x   y } : S

GET_AND_UPDATE__empty_some

COMPARE / x : k : [ ] ⇒ 1 : [ ]

GET_AND_UPDATE / x : opt_y : m : S ⇒ opt_y′ : m′ : S

GET_AND_UPDATE / x : opt_y : { Elt   k   v ; < m > } : S ⇒ opt_y′ : { Elt   k   v ; < m′ > } : S

GET_AND_UPDATE__later

COMPARE / x : k : [ ] ⇒ 0 : [ ]

GET_AND_UPDATE / x : None : { Elt   k   v ; < m > } : S ⇒ Some   v : m : S

GET_AND_UPDATE__now_none

COMPARE / x : k : [ ] ⇒ 0 : [ ]

GET_AND_UPDATE / x : Some   y : { Elt   k   v ; < m > } : S ⇒ Some   v : { Elt   k   y ; < m > } : S

GET_AND_UPDATE__now_some

COMPARE / x : k : [ ] ⇒ − 1 : [ ]

GET_AND_UPDATE / x : None : { Elt   k   v ; < m > } : S ⇒ None : { Elt   k   v ; < m > } : S

GET_AND_UPDATE__nexists_none

COMPARE / x : k : [ ] ⇒ − 1 : [ ]

GET_AND_UPDATE / x : Some   y : { Elt   k   v ; < m > } : S ⇒ None : { Elt   x   y ; < { Elt   k   v ; < m > } > } : S

GET_AND_UPDATE__nexists_some

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`GT` ¶

Check that the top of the stack is greater than zero

The GT instruction consumes an integer and leaves True on the stack if it is greater than 0 and False otherwise.

It is typically composed with COMPARE: the instruction sequence COMPARE; GT leaves True on the stack if the first stack element is greater than the second, and False otherwise.

Typing

Γ ⊢ GT :: int : A ⇒ bool : A

Semantics

z > 0

GT / z : S ⇒ True : S

GT__tt

z ≤ 0

GT / z : S ⇒ False : S

GT__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`HASH_KEY` ¶

Compute the Base58Check of a public key

The HASH_KEY instruction computes the Base58Check of a public key.

Typing

Γ ⊢ HASH_KEY :: key : A ⇒ key_hash : A

HASH_KEY

Semantics

HASH_KEY / s : S ⇒ hash_key   s : S

HASH_KEY

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`IF instr1 instr2` ¶

Conditional branching

The IF bt bf instruction consumes a stack whose top element b is of type bool and an arbitrary remaining stack S.

This instruction executes the bt branch if b is True, and the bf branch otherwise.

Note that both branches must return a stack of the same type.

Typing

Γ ⊢ instr₁ :: A ⇒ B

Γ ⊢ instr₂ :: A ⇒ B

Γ ⊢ IF   instr₁   instr₂ :: bool : A ⇒ B

Semantics

i₁ / S ⇒ S′

IF   i₁   i₂ / True : S ⇒ S′

IF__tt

i₂ / S ⇒ S′

IF   i₁   i₂ / False : S ⇒ S′

IF__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`IF_CONS instr1 instr2` ¶

Inspect a list

The IF_CONS instr1 instr2 instruction consumes a stack whose top element l has a list type list ty1 and an arbitrary remaining stack S.

If the list l has at least one element d followed by (a possibly empty) list tl, then the instr1 branch is executed on the stack d : tl : S. Otherwise, the instr2 branch is executed on the stack S.

Note that both branches must return a stack of the same type.

Typing

Γ ⊢ instr₁ :: ty : list   ty : A ⇒ B

Γ ⊢ instr₂ :: A ⇒ B

Γ ⊢ IF_CONS   instr₁   instr₂ :: list   ty : A ⇒ B

IF_CONS

Semantics

instr₂ / S ⇒ S′

IF_CONS   instr₁   instr₂ / {} : S ⇒ S′

IF_CONS__nil

instr₁ / d : tl : S ⇒ S′

IF_CONS   instr₁   instr₂ / { d ; < tl > } : S ⇒ S′

IF_CONS__cons

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`IF_LEFT instr1 instr2` ¶

Inspect a value of a union

The IF_LEFT instr1 instr2 instruction consumes a stack whose top element v has an union type or ty1 ty2 and an arbitrary remaining stack S.

If the union v stack is Left d1, then the instr1 branch is executed on the stack d1 : S. If it is Right d2, then the instr2 branch is executed on the stack d2 : S.

Note that both branches must return a stack of the same type.

Typing

Γ ⊢ instr₁ :: ty₁ : A ⇒ B

Γ ⊢ instr₂ :: ty₂ : A ⇒ B

Γ ⊢ IF_LEFT   instr₁   instr₂ :: or   ty₁   ty₂ : A ⇒ B

IF_LEFT

Semantics

instr₁ / d₁ : S ⇒ S′

IF_LEFT   instr₁   instr₂ / ( Left   d₁ ) : S ⇒ S′

IF_LEFT__left

instr₂ / d₂ : S ⇒ S′

IF_LEFT   instr₁   instr₂ / ( Right   d₂ ) : S ⇒ S′

IF_LEFT__right

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`IF_NONE instr1 instr2` ¶

Inspect an optional value

The IF_NONE instr1 instr2 instruction consumes a stack whose top element v has an option type option ty1 and an arbitrary remaining stack S.

If the optional value v is None, then the instr1 branch is executed on the stack S. If v is Some d, then the instr2 branch is executed on the stack d : S.

Note that both branches must return a stack of the same type.

Typing

Γ ⊢ instr₁ :: A ⇒ B

Γ ⊢ instr₂ :: ty₁ : A ⇒ B

Γ ⊢ IF_NONE   instr₁   instr₂ :: option   ty₁ : A ⇒ B

IF_NONE

Semantics

instr₁ / S ⇒ S′

IF_NONE   instr₁   instr₂ / None : S ⇒ S′

IF_NONE__none

instr₂ / d : S ⇒ S′

IF_NONE   instr₁   instr₂ / ( Some   d ) : S ⇒ S′

IF_NONE__some

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`IMPLICIT_ACCOUNT` ¶

Create an implicit account

Push on the stack the contract value corresponding to the implicit account of a public key hash. These contracts always have type unit.

Typing

Γ ⊢ IMPLICIT_ACCOUNT :: key_hash : A ⇒ contract   unit : A

IMPLICIT_ACCOUNT

Semantics

IMPLICIT_ACCOUNT / s : S ⇒ implicit_account   s : S

IMPLICIT_ACCOUNT

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`INT` ¶

Convert a natural number, a BLS12-381 field element, or a byte sequence to an integer

For natural numbers, INT is the identity cast from nat to int. For BLS12-381 field elements, the returned value is always between 0 (inclusive) and the order of the BLS12-381 field (exclusive). For bytes, INT decodes the bytes using the big-endian encoding, where negative numbers are considered in two's complement representation.

Typing

Γ ⊢ INT :: nat : A ⇒ int : A

INT__nat

Γ ⊢ INT :: bls12_381_fr : A ⇒ int : A

INT__bls12_381_fr

Γ ⊢ INT :: bytes : A ⇒ int : A

INT__bytes

Semantics

INT / z : S ⇒ z : S

INT

INT / byt : S ⇒ decode_int_be byt : S

INT__bytes

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`ISNAT` ¶

Convert a non-negative integer to a natural number

The ISNAT instruction consumes an integer z and returns a value of type option nat. If the integer is non-negative, Some n is returned, where n is equal to z but represented as a natural number. Otherwise, None is returned.

Typing

Γ ⊢ ISNAT :: int : A ⇒ option   nat : A

ISNAT

Semantics

z ≥ 0

ISNAT / z : S ⇒ Some   ( tonat   z ) : S

ISNAT__ok

z < 0

ISNAT / z : S ⇒ None : S

ISNAT__fail

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`ITER instr` ¶

Iterate over a `set`, `list` or `map`

Iterate on a set, list or map.

Consume a structure by applying the instr expression to each of its elements:

In the case of a list or set of elements of type ty1, instr is applied to each element, and must thus have the type ty1 : A => A.

In the case of a map of keys of type kty and values of type vty, instr is applied to each binding k to value v in the form of a pair Pair k v. Thus, instr must have the type pair kty vty : A => A.

In each case, instr has access to and can modify the underlying stack as long as its type is preserved. It cannot however access the full structure but only a single element at a time (on top of the stack); when access to the full structure is needed, DUP; ITER {instr} should be used.

Iteration on list goes from the head of the list to the tail. Iteration on set is done in increasing order of elements. Iteration on map is done in increasing order of keys.

Typing

Γ ⊢ instr :: ty : A ⇒ A

Γ ⊢ ITER   instr :: list   ty : A ⇒ A

ITER__list

Γ ⊢ instr :: cty : A ⇒ A

Γ ⊢ ITER   instr :: set   cty : A ⇒ A

ITER__set

Γ ⊢ instr :: ( pair   kty   vty ) : A ⇒ A

Γ ⊢ ITER   instr :: map   kty   vty : A ⇒ A

ITER__map

Semantics

ITER   instr / {} : S ⇒ S

ITER__list_nil

instr / d : S ⇒ S′

ITER   instr / tl : S′ ⇒ S″

ITER   instr / { d ; < tl > } : S ⇒ S″

ITER__list_cons

ITER   instr / {} : S ⇒ S

ITER__set_nil

instr / x : S ⇒ S′

ITER   instr / tl : S′ ⇒ S″

ITER   instr / { x ; < tl > } : S ⇒ S″

ITER__set_cons

ITER   instr / {} : S ⇒ S

ITER__map_nil

instr / ( Pair   k   v ) : S ⇒ S′

ITER   instr / m : S′ ⇒ S″

ITER   instr / { Elt   k   v ; < m > } : S ⇒ S″

ITER__map_cons

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`JOIN_TICKETS` ¶

Join two tickets into one

The inverse of SPLIT_TICKET. Delete the given tickets and create a ticket with an amount equal to the sum of the amounts of the input tickets. (This can be used to consolidate UTXOs.) Return None iff the input tickets have a different ticketer or content.

Typing

Γ ⊢ JOIN_TICKETS :: pair   ( ticket   cty )   ( ticket   cty ) : A ⇒ option   ( ticket   cty ) : A

JOIN_TICKETS

Semantics

JOIN_TICKETS / Pair   ( Pair   s   x   n₁ )   ( Pair   s   x   n₂ ) : S ⇒ Some   ( Pair   s   x   ( n₁   +   n₂ ) ) : S

JOIN_TICKETS__some

s₁ ≠ s₂

JOIN_TICKETS / Pair   ( Pair   s₁   x₁   n₁ )   ( Pair   s₂   x₂   n₂ ) : S ⇒ None : S

JOIN_TICKETS__none_ticketer

x₁ ≠ x₂

JOIN_TICKETS / Pair   ( Pair   s₁   x₁   n₁ )   ( Pair   s₂   x₂   n₂ ) : S ⇒ None : S

JOIN_TICKETS__none_content

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`KECCAK` ¶

Compute a Keccak-256 cryptographic hash

Compute the cryptographic hash of the top of the stack using the Keccak-256 cryptographic hash function.

Typing

Γ ⊢ KECCAK :: bytes : A ⇒ bytes : A

KECCAK

Semantics

KECCAK / byt : S ⇒ hash_keccak   byt : S

KECCAK

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`LAMBDA ty1 ty2 instr` ¶

Push a lambda onto the stack

Push a lambda with parameter type ty1, return type ty2 and body instr onto the stack.

Typing

None ⊢ instr :: ty₁ : [ ] ⇒ ty₂ : [ ]

Γ ⊢ LAMBDA   ty₁   ty₂   instr :: A ⇒ lambda   ty₁   ty₂ : A

LAMBDA

Semantics

LAMBDA   ty₁   ty₂   instr / S ⇒ { instr : ty₁ → ty₂ } : S

LAMBDA

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`LAMBDA_REC ty1 ty2 instr` ¶

Push a recursive lambda onto the stack

Same as LAMBDA but the instruction sequence instr can call itself recursively.

instr expects two parameters: the top of the stack is some value that the function is applied to, and the second element of the stack is Lambda_rec {instr}, the recursive lambda itself which can be used for recursive calls.

Typing

None ⊢ instr :: ty₁ : lambda   ty₁   ty₂ : [ ] ⇒ ty₂ : [ ]

Γ ⊢ LAMBDA_REC   ty₁   ty₂   instr :: A ⇒ lambda   ty₁   ty₂ : A

LAMBDA_REC

Semantics

LAMBDA_REC   ty₁   ty₂   instr / S ⇒ Lambda_rec   instr : S

LAMBDA_REC

Related types

Available since mainnet protocol: Lima (PtLimaPtLMwfNinJi9rCfDPWea8dFgTZ1MeJ9f1m2SRic6ayiwW)
Proposed in protocol: Lima (PtLimaPtLMwfNinJi9rCfDPWea8dFgTZ1MeJ9f1m2SRic6ayiwW)

Example: Recursive factorial ¶

This contract takes a natural as parameter, and applies a recursive lambda to return its factorial. Notice how the lambda is able to reference itself as the second value from the top of the stack.

try it!

# This is a recursive implementation of the factorial function illustrating the
# LAMBDA_REC instruction.

parameter nat;
storage nat;
code
  {
    CAR;
    LAMBDA_REC nat nat
               # Let us call f the block below.
               { # Stack is: n, f
                 # where n is the factorial's parameter.
                 PUSH int -1;
                 ADD;
                 # Stack is: n-1, f.
                 ISNAT;
                 IF_NONE
                   # If n-1 is not a natural, i.e. n = 0, return 1.
                   { DROP; PUSH nat 1 }
                   # Else, run f(n-1) and multiply the result by n (= n-1 + 1).
                   { DUP; DIP {EXEC}; PUSH nat 1; ADD; MUL }
               };
    SWAP;
    EXEC;
    NIL operation;
    PAIR
  }

If called with the initial storage 0 and the parameter 5 then the final storage will be 120.

`LE` ¶

Check that the top of the stack is less than or equal to zero

The LE instruction consumes an integer and leaves True on the stack if it is less than or equal to 0 or False otherwise.

It typically follows a COMPARE instruction. The sequence of instructions COMPARE; LE leaves True on the stack if the first stack element is less than or equal to the second, and False otherwise.

Typing

Γ ⊢ LE :: int : A ⇒ bool : A

Semantics

z ≤ 0

LE / z : S ⇒ True : S

LE__tt

z > 0

LE / z : S ⇒ False : S

LE__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`LEFT ty2` ¶

Wrap a value in a union (left case)

Typing

Γ ⊢ LEFT   ty₂ :: ty₁ : A ⇒ or   ty₁   ty₂ : A

LEFT

Semantics

LEFT   ty₂ / v : S ⇒ ( Left   v ) : S

LEFT

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`LEVEL` ¶

Push the current block level

Typing

Γ ⊢ LEVEL :: A ⇒ nat : A

LEVEL

Semantics

LEVEL / S ⇒ level : S

LEVEL

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`LOOP instr` ¶

A generic loop

The instruction LOOP consumes a stack b : S of type bool : A, i.e. where b is boolean and the rest of the stack is of any type A. The body of the loop, instr, is executed as long as b is True. The body has access to the stack S but must produce a stack of type bool : A. If b is False, then the loop is terminated with the resulting stack S.

Typing

Γ ⊢ instr :: A ⇒ bool : A

Γ ⊢ LOOP   instr :: bool : A ⇒ A

LOOP

Semantics

instr ; LOOP   instr / S ⇒ S′

LOOP   instr / True : S ⇒ S′

LOOP__tt

LOOP   instr / False : S ⇒ S

LOOP__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`LOOP_LEFT instr` ¶

Loop with accumulator

The LOOP_LEFT body instruction executes body as long as the top element of the stack is (Left a). The body of the loop must consume a value of type a and produce a value of type (or a b).

If the top element is (Right b), at the beginning of the loop or at the end of an iteration, then the loop is terminated and this value is left on the top of the stack.

Typing

Γ ⊢ instr :: ty₁ : A ⇒ or   ty₁   ty₂ : A

Γ ⊢ LOOP_LEFT   instr :: or   ty₁   ty₂ : A ⇒ ty₂ : A

LOOP_LEFT

Semantics

i₁ ; LOOP_LEFT   i₁ / d : S ⇒ S′

LOOP_LEFT   i₁ / Left   d : S ⇒ S′

LOOP_LEFT__tt

LOOP_LEFT   i₁ / Right   d : S ⇒ d : S′

LOOP_LEFT__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Sum list ¶

This contract reverses the list of strings passed by parameter and stores it.

try it!

parameter (list string);
storage (list string);
code { CAR; NIL string; SWAP; PAIR; LEFT (list string);
       LOOP_LEFT { DUP; CAR; DIP{CDR};
                   IF_CONS { SWAP; DIP{CONS}; PAIR; LEFT (list string) }
                           { RIGHT (pair (list string) (list string)) }; };
       NIL operation; PAIR }

If called with the initial storage {} and the parameter { "a" ; "b" ; "c" } then the final storage will be { "c" ; "b" ; "a" }.

`LSL` ¶

Logically left shift of a natural number or of a byte sequence

For natural numbers, the LSL instruction consumes two natural numbers and produces the first number logically left-shifted by the second number. This instruction is only defined if the second number is less than or equal to 256.

For bytes, the LSL instruction consumes one byte sequence and one natural number and produces the bytes logically left-shifted by the natural number. The vacated bits on the right are filled with 0s. The shifted bits are minimally 0-padded on the left in order to keep all the original bits, regardless if they are 0 or 1: for example, 0x1234 LSL 1 is 0x002468, instead of 0x2468 (even though in this case no significant bit would be lost) or 0x00002468 (where padding is not minimal). The length of the bytes returned by LSL is l + (s + 7) / 8 bytes where l is the length of the original bytes and s is the natural number. This instruction is only defined if the second number is less than or equal to 64000.

Typing

Γ ⊢ LSL :: nat : nat : A ⇒ nat : A

LSL__nat

Γ ⊢ LSL :: bytes : nat : A ⇒ bytes : A

LSL__bytes

Semantics

z₂ ≤ 256

LSL / z₁ : z₂ : S ⇒ ( z₁   ≪   z₂ ) : S

LSL__nat

z₂ > 256

LSL / z₁ : z₂ : S ⇒ [FAILED]

LSL__nat_fail

n ≤ 64000

LSL / bs₁ : n : S ⇒ ( bs₁ << n ) : S

LSL__bytes

n > 64000

LSL / bs₁ : n : S ⇒ [FAILED]

LSL__bytes_fail

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: LSL on bytes ¶

This contract demonstrates LSL on bytes.

try it!

parameter unit;
storage unit;
code { DROP;

       # If shift is 0, LSL returns the bytes untouched
       # 0x06 LSL 0 = 0x06
       PUSH nat 0; PUSH bytes 0x06; LSL; PUSH bytes 0x06; ASSERT_CMPEQ;

       # If shift is not 0, LSL returns a bytes longer than the original
       # 0x06 LSL 1 = 0x000c  (not 0x0c)
       PUSH nat 1; PUSH bytes 0x06; LSL; PUSH bytes 0x000c; ASSERT_CMPEQ;

       # 0x06 LSL 8 = 0x0600
       PUSH nat 8; PUSH bytes 0x06; LSL; PUSH bytes 0x0600; ASSERT_CMPEQ;

       # 0x0006 LSL 1 = 0x00000c  (not 0x0c nor 0x000c)
       PUSH nat 1; PUSH bytes 0x0006; LSL; PUSH bytes 0x00000c; ASSERT_CMPEQ;

       UNIT; NIL @noop operation; PAIR; };

`LSR` ¶

Logically right shift of a natural number or of a byte sequence

For natural numbers, The LSR instruction consumes two natural numbers and produces the first number logically right-shifted by second number. This instruction is only defined if the second number is less than or equal to 256.

For bytes, the LSR instruction consumes one chunk of bytes and one natural number and produces the bytes logically right-shifted by the natural number. The shifted bits are minimally 0-padded on the left. For example, 0x012349 LSR 9 is 0x0091, instead of 0x91 (where the 7 left-most bits are lost) or 0x000091 (not minimal padding). The length of the returned bytes by LSR is max 0 (l - s / 8) bytes where l is the length of the original bytes and s is the natural number.

Typing

Γ ⊢ LSR :: nat : nat : A ⇒ nat : A

LSR__nat

Γ ⊢ LSR :: bytes : nat : A ⇒ bytes : A

LSR__bytes

Semantics

z₂ ≤ 256

LSR / z₁ : z₂ : S ⇒ ( z₁   ≫   z₂ ) : S

LSR__nat

z₂ > 256

LSR / z₁ : z₂ : S ⇒ [FAILED]

LSR__nat_fail

LSR / bs : n : S ⇒ ( bs >> n ) : S

LSR__bytes

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: LSR on bytes ¶

This contract demonstrates LSR on bytes.

try it!

parameter unit;
storage unit;
code { DROP;

       # 0x06 LSR 1 = 0x03
       PUSH nat 1; PUSH bytes 0x06; LSR; PUSH bytes 0x03; ASSERT_CMPEQ;

       # 0x06 LSR 8 = 0x (empty bytes)
       PUSH nat 8; PUSH bytes 0x06; LSR; PUSH bytes 0x; ASSERT_CMPEQ;

       # 0x0006 LSR 1 = 0x0003  (not 0x03)
       PUSH nat 1; PUSH bytes 0x0006; LSR; PUSH bytes 0x0003; ASSERT_CMPEQ;

       # 0x0006 LSR 8 = 0x00
       PUSH nat 8; PUSH bytes 0x0006; LSR; PUSH bytes 0x00; ASSERT_CMPEQ;

       # 0x001234 LSR 0 = 0x001234
       PUSH nat 0; PUSH bytes 0x001234; LSR; PUSH bytes 0x001234; ASSERT_CMPEQ;

       # 0x001234 LSR 30 = 0x
       PUSH nat 30; PUSH bytes 0x001234; LSR; PUSH bytes 0x; ASSERT_CMPEQ;

       UNIT; NIL @noop operation; PAIR; };

`LT` ¶

Check that the top of the stack is less than zero

The LT instruction consumes an integer and leaves True on the stack if it is less than 0 and False otherwise.

It is typically composed with COMPARE: the instruction sequence COMPARE; LT leaves True on the stack if the first stack element is less than the second, and False otherwise.

Typing

Γ ⊢ LT :: int : A ⇒ bool : A

Semantics

z < 0

LT / z : S ⇒ True : S

LT__tt

z ≥ 0

LT / z : S ⇒ False : S

LT__ff

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`MAP instr` ¶

Apply `instr` to each element of a `list`, an `option`, or `map`.

Map over a data structure, either a list, an option, or map.

Update a structure by applying the instr expression to each of its elements:

In the case of a list of elements of type ty1, instr is applied to each element, and must thus have the type ty1 : A => ty2 : A.

Similarly, in the case of an option with an element of type ty1, instr is applied to the element inside the option, and it must thus have the type ty1 : A => ty2 : A. The stack is left unchanged otherwise, i.e. if the top value is None.

In the case of a map of keys of type kty and values of type ty1, instr is applied to each binding k to value v in the form of a pair Pair k v. Thus, instr must have the type pair kty ty1 : A => ty2 : A.

Iteration on list goes from the head of the list to the tail. Iteration on map is done in increasing order of keys.

Typing

Γ ⊢ instr :: ty : A ⇒ ty₂ : A

Γ ⊢ MAP   instr :: list   ty : A ⇒ list   ty₂ : A

MAP__list

Γ ⊢ instr :: ty : A ⇒ ty₂ : A

Γ ⊢ MAP   instr :: option   ty : A ⇒ option   ty₂ : A

MAP__option

Γ ⊢ instr :: ( pair   kty   ty₁ ) : A ⇒ ty₂ : A

Γ ⊢ MAP   instr :: map   kty   ty₁ : A ⇒ map   kty   ty₂ : A

MAP__map

Semantics

MAP   instr / {} : S ⇒ {} : S

MAP__list_nil

instr / d : S ⇒ d′ : S′

MAP   instr / tl : S′ ⇒ tl′ : S″

MAP   instr / { d ; < tl > } : S ⇒ { d′ ; < tl′ > } : S″

MAP__list_cons

MAP   instr / None : S ⇒ None : S

MAP__option_none

instr / d : S ⇒ d′ : S′

MAP   instr / Some   d : S ⇒ Some   d′ : S′

MAP__option_some

MAP   body / {} : S ⇒ {} : S

MAP__map_nil

body / ( Pair   k   v ) : S ⇒ v′ : S′

MAP   body / m : S′ ⇒ m′ : S″

MAP   body / { Elt   k   v ; < m > } : S ⇒ { Elt   k   v′ ; < m′ > } : S″

MAP__map_cons

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`MEM` ¶

Check for the presence of a binding for a key in a `map`, `set` or `big_map`

The instruction MEM consumes a value and a data structure of type map, set or big_map.

For map and big_map, MEM returns True if the value is a bound key in the data structure, and False otherwise.

For set, True is returned if the value is a member of the set, and False otherwise.

Typing

Γ ⊢ MEM :: cty : set   cty : A ⇒ bool : A

MEM__set

Γ ⊢ MEM :: kty : map   kty   vty : A ⇒ bool : A

MEM__map

Γ ⊢ MEM :: kty : big_map   kty   vty : A ⇒ bool : A

MEM__big_map

Semantics

MEM / x : {} : S ⇒ False : S

MEM__set_empty

COMPARE / x : y : [ ] ⇒ 1 : [ ]

MEM / x : tl : S ⇒ b : S

MEM / x : { y ; < tl > } : S ⇒ b : S

MEM__set_later

COMPARE / x : y : [ ] ⇒ 0 : [ ]

MEM / x : { y ; < tl > } : S ⇒ True : S

MEM__set_found

COMPARE / x : y : [ ] ⇒ − 1 : [ ]

MEM / x : { y ; < tl > } : S ⇒ False : S

MEM__set_nexists

MEM / x : {} : S ⇒ False : S

MEM__map_empty

COMPARE / x : k : [ ] ⇒ 1 : [ ]

MEM / x : m : S ⇒ b : S

MEM / x : { Elt   k   v ; < m > } : S ⇒ b : S

MEM__map_later

COMPARE / x : k : [ ] ⇒ 0 : [ ]

MEM / x : { Elt   k   v ; < m > } : S ⇒ True : S

MEM__map_now

COMPARE / x : k : [ ] ⇒ − 1 : [ ]

MEM / x : { Elt   k   v ; < m > } : S ⇒ False : S

MEM__map_nexists

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`MIN_BLOCK_TIME` ¶

Push the current minimal block time in seconds.

Returns the minimal delay between two consecutive blocks in the chain.

Typing

Γ ⊢ MIN_BLOCK_TIME :: A ⇒ nat : A

MIN_BLOCK_TIME

Semantics

MIN_BLOCK_TIME / S ⇒ min_block_time : S

MIN_BLOCK_TIME

Related types

Available since mainnet protocol: Ithaca (Psithaca2MLRFYargivpo7YvUr7wUDqyxrdhC5CQq78mRvimz6A)
Proposed in protocol: Ithaca (Psithaca2MLRFYargivpo7YvUr7wUDqyxrdhC5CQq78mRvimz6A)

`MUL` ¶

Multiply two numerical values

The MUL instruction consumes two numbers (int or nat) and produces their product.

MUL can also be used to multiply a mutez with a natural number. In this case, the operation triggers a run-time error if the product overflows.

MUL can also be used to multiply a BLS12-381 curve point or field element by a scalar field element.

Finally, MUL can multiply together a BLS12-381 field element and a natural or integer. In particular, field elements can be built from naturals by multiplying by the unit of bls12_381_fr using PUSH bls12_381_fr 1; MUL. Note that the product will be computed using the natural modulo the order of the field.

Typing

Γ ⊢ MUL :: nat : nat : A ⇒ nat : A

MUL__nat_nat

Γ ⊢ MUL :: nat : int : A ⇒ int : A

MUL__nat_int

Γ ⊢ MUL :: int : nat : A ⇒ int : A

MUL__int_nat

Γ ⊢ MUL :: int : int : A ⇒ int : A

MUL__int_int

Γ ⊢ MUL :: mutez : nat : A ⇒ mutez : A

MUL__mutez_nat

Γ ⊢ MUL :: nat : mutez : A ⇒ mutez : A

MUL__nat_mutez

Γ ⊢ MUL :: bls12_381_g1 : bls12_381_fr : A ⇒ bls12_381_g1 : A

MUL__g1_fr

Γ ⊢ MUL :: bls12_381_g2 : bls12_381_fr : A ⇒ bls12_381_g2 : A

MUL__g2_fr

Γ ⊢ MUL :: bls12_381_fr : bls12_381_fr : A ⇒ bls12_381_fr : A

MUL__fr_fr

Γ ⊢ MUL :: nat : bls12_381_fr : A ⇒ bls12_381_fr : A

MUL__nat_fr

Γ ⊢ MUL :: int : bls12_381_fr : A ⇒ bls12_381_fr : A

MUL__int_fr

Γ ⊢ MUL :: bls12_381_fr : nat : A ⇒ bls12_381_fr : A

MUL__fr_nat

Γ ⊢ MUL :: bls12_381_fr : int : A ⇒ bls12_381_fr : A

MUL__fr_int

Semantics

MUL / z₁ : z₂ : S ⇒ ( z₁   *   z₂ ) : S

MUL

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NAT` ¶

Convert bytes to a natural number

NAT decodes the bytes using the big-endian encoding.

Typing

Γ ⊢ NAT :: bytes : A ⇒ nat : A

NAT__bytes

Semantics

NAT / byt : S ⇒ decode_nat_be byt : S

NAT__bytes

Related types

Available since mainnet protocol: Mumbai (PtMumbai2TmsJHNGRkD8v8YDbtao7BLUC3wjASn1inAKLFCjaH1)
Proposed in protocol: Mumbai (PtMumbai2TmsJHNGRkD8v8YDbtao7BLUC3wjASn1inAKLFCjaH1)

`NEG` ¶

Negate a numerical value

The NEG instruction consumes a number and returns its negation. The input can be any numerical type except timestamp and mutez. In particular, NEG can be used on the BLS12-381 curves and field. The output has the same type as the input except in the case of nat where the output has type int.

Typing

Γ ⊢ NEG :: nat : A ⇒ int : A

NEG__nat

Γ ⊢ NEG :: int : A ⇒ int : A

NEG__int

Γ ⊢ NEG :: bls12_381_g1 : A ⇒ bls12_381_g1 : A

NEG__g1

Γ ⊢ NEG :: bls12_381_g2 : A ⇒ bls12_381_g2 : A

NEG__g2

Γ ⊢ NEG :: bls12_381_fr : A ⇒ bls12_381_fr : A

NEG__fr

Semantics

NEG / z : S ⇒ − z : S

NEG

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NEQ` ¶

Check that the top of the stack is not equal to zero

The NEQ instruction consumes an integer and leaves True on the stack if it is not 0 and False otherwise.

It is typically composed with COMPARE: the instruction sequence COMPARE; NEQ leaves True on the stack if the two top stack elements are not equal, and False otherwise.

Typing

Γ ⊢ NEQ :: int : A ⇒ bool : A

NEQ

Semantics

NEQ / 0 : S ⇒ False : S

NEQ__ff

z ≠ 0

NEQ / z : S ⇒ True : S

NEQ__tt

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NEVER` ¶

Close a forbidden branch

Typing

Γ ⊢ NEVER :: never : A ⇒ B

NEVER

Semantics

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`NIL ty` ¶

Push an empty list

The NIL ty1 instruction produces the empty list of type list ty1. It is functionally equivalent to PUSH (list ty1) {}.

Typing

Γ ⊢ NIL   ty :: A ⇒ list   ty : A

NIL

Semantics

NIL   ty / S ⇒ {} : S

NIL

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NONE ty` ¶

Push the absent optional value

The NONE ty1 instruction produces the absent optional value None of type option ty1.

It is functionally equivalent to PUSH (option ty1) None.

Typing

Γ ⊢ NONE   ty :: A ⇒ option   ty : A

NONE

Semantics

NONE   ty / S ⇒ None : S

NONE

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NOT` ¶

Boolean negation and bitwise complement

The NOT instruction is defined for bool, nat, int and bytes.

For bool, it returns the logical negation of its operand.

For numerical values, it returns the two's complement as an int. The return type is int and not nat because the sign is also negated. For instance, the boolean negation of 0 is -1. To get a natural back, a possibility is to use AND with an unsigned mask afterwards.

For bytes, it returns the bytes whose contents are the bitwise negations of the original.

Typing

Γ ⊢ NOT :: bool : A ⇒ bool : A

NOT__bool

Γ ⊢ NOT :: nat : A ⇒ int : A

NOT__nat

Γ ⊢ NOT :: int : A ⇒ int : A

NOT__int

Γ ⊢ NOT :: bytes : A ⇒ bytes : A

NOT__bytes

Semantics

NOT / True : S ⇒ False : S

NOT__1

NOT / False : S ⇒ True : S

NOT__2

NOT / z : S ⇒ ∼ z : S

NOT__bit

NOT / bs : S ⇒ ∼ bs : S

NOT__bytes

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`NOW` ¶

Push block timestamp

Push the minimal injection time for the current block, namely the block whose application triggered this execution. On Mainnet, the minimal injection time is MINIMAL_BLOCK_DELAY seconds after the timestamp of the predecessor block. This value does not change during the execution of the contract.

The minimal injection time constitutes an estimate of the moment when the current block is injected, hence the name NOW.

Typing

Γ ⊢ NOW :: A ⇒ timestamp : A

NOW

Semantics

NOW / S ⇒ now : S

NOW

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`OPEN_CHEST` ¶

Open a timelocked chest given its key and the time

Opens a timelocked chest given its key and the time. The result is a byte option depending if the opening is correct or not.

See Timelock for more

Typing

Γ ⊢ OPEN_CHEST :: chest_key : chest : nat : A ⇒ option   bytes : A

OPEN_CHEST

Semantics

OPEN_CHEST / chk : ch : n : S ⇒ open_chest chk ch n : S

OPEN_CHEST

Related types

Proposed in protocol: Oxford (ProxfordSW2S7fvchT1Zgj2avb5UES194neRyYVXoaDGvF9egt8)

`OR` ¶

Boolean and bitwise OR

The instruction OR is defined on boolean, natural number and bytes operands. In the boolean case, the result is the logical OR of the operands. In the natural number and bytes cases, the result is the bitwise OR of the operands.

When OR is used for bytes operands, the result bytes has the same length as the longer operand. The shorter operand is 0-padded on the left to match with the length of the longer one before taking the bitwise OR.

Typing

Γ ⊢ OR :: bool : bool : A ⇒ bool : A

OR__bool

Γ ⊢ OR :: nat : nat : A ⇒ nat : A

OR__nat

Γ ⊢ OR :: bytes : bytes : A ⇒ bytes : A

OR__bytes

Semantics

OR / True : x : S ⇒ True : S

OR__1

OR / x : True : S ⇒ True : S

OR__2

OR / False : False : S ⇒ False : S

OR__3

OR / z₁ : z₂ : S ⇒ ( z₁   ∣   z₂ ) : S

OR__bit

OR / bs₁ : bs₂ : S ⇒ ( bs₁   ∣   bs₂ ) : S

OR__bytes

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`PACK` ¶

Serialize data

Serializes any value of packable type to its optimized binary representation, of type bytes.

Typing

Γ ⊢ PACK :: ty : A ⇒ bytes : A

PACK

Semantics

PACK / d : S ⇒ pack   d : S

PACK

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: `PACK` -- `UNPACK` ¶

This example packs the left part of the parameter, and asserts that it is equal to the right part of the parameter. It then verifies that the right part unpacks to a valid Michelson value.

try it!

parameter (pair (pair (pair string (list int)) (set nat)) bytes) ;
storage unit ;
code { CAR ; UNPAIR ; DIP { DUP } ;
       PACK ; ASSERT_CMPEQ ;
       UNPACK (pair (pair string (list int)) (set nat)) ; ASSERT_SOME ; DROP ;
       UNIT ; NIL operation ; PAIR }

If called with the initial storage Unit and the parameter (Pair (Pair (Pair "toto" {3;7;9;1}) {1;2;3}) 0x05070707070100000004746f746f020000000800030007000900010200000006000100020003) then the final storage will be Unit.

`PAIR` ¶

Build a pair from the stack's top two elements

Typing

Γ ⊢ PAIR :: ty₁ : ty₂ : A ⇒ pair   ty₁   ty₂ : A

PAIR

Semantics

PAIR / d₁ : d₂ : S ⇒ ( Pair   d₁   d₂ ) : S

PAIR

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`PAIR n` ¶

Fold `n` values on the top of the stack into a right comb

Fold n values on the top of the stack into a right comb. PAIR 0 and PAIR 1 are rejected. PAIR 2 is equivalent to PAIR.

Typing

n ≥ 2

Γ ⊢ PAIR   n :: ty₁ :   ....   : ty_N : A ⇒ pair   ty₁   ....   ty_N : A

PAIRN

Semantics

n ≥ 2

PAIR   n / d₁ :   ....   : d_N : S ⇒ ( Pair   d₁   ....   d_N ) : S

PAIRN

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

Example: Demonstration of n-ary `PAIR` ¶

This contract demonstrates the use of the PAIR instruction with an arity of 4. This contract ignores both its parameter and storage and uses PAIR 4 to simultaneously build the final storage (a comb of size 3) and pair it with an empty list of operations to conform to the Michelson call convention. Indeed, when the storage is a comb of 3 nats, the contract code must end with a stack of type pair (list operation) (pair nat nat nat) which is exactly the same type as pair (list operation) nat nat nat.

try it!

parameter unit;
storage (pair nat nat nat);
code { DROP ;
       PUSH nat 3 ;
       PUSH nat 2 ;
       PUSH nat 1 ;
       NIL operation ;
       PAIR 4
     }

If called with the initial storage (Pair 4 5 6) and the parameter Unit then the final storage will be (Pair 1 2 3).

`PAIRING_CHECK` ¶

Check a BLS12-381 pairing

Verify that the product of pairings of the given list of points is equal to 1 in the field Fq12. Returns True if the list is empty. This instruction can be used to verify if two pairings P1 and P2 are equal by verifying P1 * P2^(-1) = 1.

Typing

Γ ⊢ PAIRING_CHECK :: list   ( pair   bls12_381_g1   bls12_381_g2 ) : A ⇒ bool : A

PAIRING_CHECK

Semantics

PAIRING_CHECK / {} : S ⇒ True : S

PAIRING_CHECK__empty

bls12_381_pairing_check ( l ) = b

PAIRING_CHECK / l : S ⇒ b : S

PAIRING_CHECK__l

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`PUSH ty x` ¶

Push a constant value of a given type onto the stack

Typing

Γ ⊢ x :: ty

Γ ⊢ PUSH   ty   x :: A ⇒ ty : A

PUSH

Semantics

PUSH   ty   d / S ⇒ d : S

PUSH

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`READ_TICKET` ¶

Retrieve the information stored in a ticket. Also return the ticket.

Typing

Γ ⊢ READ_TICKET :: ticket   cty : A ⇒ pair   address   cty   nat : ticket   cty : A

READ_TICKET

Semantics

READ_TICKET / Pair   s   x   n : S ⇒ Pair   s   x   n : Pair   s   x   n : S

READ_TICKET

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`RIGHT ty1` ¶

Wrap a value in a union (right case)

Typing

Γ ⊢ RIGHT   ty₁ :: ty₂ : A ⇒ or   ty₁   ty₂ : A

RIGHT

Semantics

RIGHT   ty₁ / v : S ⇒ ( Right   v ) : S

RIGHT

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

`SAPLING_EMPTY_STATE ms` ¶

Push an empty Sapling state on the stack

SAPLING_EMPTY_STATE ms pushes the empty Sapling state (i.e. no one can spend tokens from it) with memo size ms.

Please see the Sapling integration page for a more comprehensive description of the Sapling protocol.

Typing

Γ ⊢ SAPLING_EMPTY_STATE   ms :: A ⇒ sapling_state   ms : A

SAPLING_EMPTY_STATE

Semantics

SAPLING_EMPTY_STATE   n / S ⇒ {} : S

SAPLING_EMPTY_STATE

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`SAPLING_VERIFY_UPDATE` ¶

Verify and apply a transaction on a Sapling state

If the given sapling transaction can successfully be applied to the given state, then SAPLING_VERIFY_UPDATE returns the bound data and the difference between the outputs and the inputs of the transaction, along with the updated state.

Please see the Sapling integration page for a more comprehensive description of the Sapling protocol.

Typing

Γ ⊢ SAPLING_VERIFY_UPDATE :: sapling_transaction   ms : sapling_state   ms : A ⇒ option   ( pair   bytes   ( pair   int   ( sapling_state   ms ) ) ) : A

SAPLING_VERIFY_UPDATE

Semantics

sapling_verify_update   ( t , s , d , b , s′ ) = True

SAPLING_VERIFY_UPDATE / t : s : S ⇒ Some   ( Pair   d   ( Pair   b   s′ ) ) : S

SAPLING_VERIFY_UPDATE__some

sapling_verify_update   ( t , s , d , b , s′ ) = False

SAPLING_VERIFY_UPDATE / t : s : S ⇒ None : S

SAPLING_VERIFY_UPDATE__none

Related types

Proposed in protocol: Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)

`SELF` ¶

Push the current contract

The SELF contract pushes the current contract, of type contract ty1 where ty1 is the type of the current contract.

Note that SELF is forbidden in lambdas because it cannot be type-checked; the type of the contract executing the lambda cannot be known at the point of type-checking the lambda's body. To access the address of the contract executing a lambda, see SELF_ADDRESS.

Like CONTRACT, the SELF instruction has a variant SELF %entrypoint, that is only well-typed if the current contract has an entrypoint named %entrypoint. It returns the contract ty1 corresponding to a specific entrypoint of the current contract, where ty1 is the type of the %entrypoint. Unlike for CONTRACT, SELF %default is allowed and is strictly equal to SELF.

This works as follows:

instruction output contract

SELF "addr_of_current_contract"

SELF %default

SELF %A "addr_of_current_contract%A" if current contract has an entrypoint %A (and A <> default)

Typing

Γ = Some   ty

Γ ⊢ SELF :: A ⇒ contract   ty : A

SELF

Semantics

SELF / S ⇒ self : S

SELF

Related types

Available since mainnet protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Proposed in protocol: Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)

Example: Callback self at entrypoint ¶

This contract has two entrypoints: have_fun and default. The default entrypoint emits a transfer token operation that calls back the contract itself, at the have_fun entrypoint, passing a big_map as parameter. The have_fun entrypoint unthankfully drops the received big_map.

try it!

parameter (or (pair %have_fun (big_map string nat) unit) (unit %default));
storage (big_map string nat);
code {
       UNPAIR;
       DIP {NIL operation};
       IF_LEFT {
                 DROP
               }
               {
                 DROP;
                 SELF %have_fun;
                 PUSH mutez 0;
                 DUP 4;
                 PUSH (option nat) (Some 8);
                 PUSH string "hahaha";
                 UPDATE;
                 UNIT; SWAP; PAIR;
                 TRANSFER_TOKENS;
                 CONS
               };
       PAIR
     }

Example: Self with default entrypoint ¶

This example demonstrates using SELF with and without entrypoint annotations, as well as the default entrypoint.

try it!

parameter (or (or (nat %A) (bool %B)) (or %maybe_C (unit %default) (string %C)));
storage unit;
code {
       DROP;
       SELF; DROP;
       # Refers to entrypoint A of the current contract.
       SELF %A; DROP;
       # Refers to the default entry of the current contract
       SELF %default; PACK;
       # "SELF" w/o annotation also refers to the default
       # entry of the current contract. Internally, they are equal.
       SELF; PACK; ASSERT_CMPEQ;
       # The following instruction would not typecheck:
       #    SELF %D,
       # since there is no entrypoint D.
       UNIT;
       NIL

input address	instruction	output contract	predicate
`"addr"`	`CONTRACT t`	`None` if `addr` does not exist	`no_contract "addr"` holds
`"addr"`	`CONTRACT t`	`None` if `addr` exists, but has a `default` entrypoint not of type `t`, or has no `default` entrypoint and parameter is not of type `t`	`invalid_contract_type "addr" t` holds
`"addr%name"`	`CONTRACT t`	`None` if `addr` does not exist, or exists but does not have a `name` entrypoint	`no_contract "addr%name"` holds
`"addr"`	`CONTRACT %name t`		`no_contract "addr%name"` holds
`"addr%name"`	`CONTRACT t`	`None` if `addr` exists, but has an entrypoint `name` not of type `t`	`invalid_contract_type "addr%name" t` holds
`"addr"`	`CONTRACT %name t`		`invalid_contract_type "addr%name" t` holds
`"addr%name1"`	`CONTRACT %name2 t`	`None`	`entrypoint_ambiguity "addr%name1" "name2"` holds
`"addr"`	`CONTRACT t`	`(Some "addr")` if contract exists, has a `default` entrypoint of type `t`, or has no `default` entrypoint and parameter type `t`	`valid_contract_type "addr" t` holds
`"addr%name"`	`CONTRACT t`	`(Some "addr%name")` if `addr` exists and has an entrypoint `name` of type `t`	`valid_contract_type "addr%name" t` holds
`"addr"`	`CONTRACT %name t`		`valid_contract_type "addr%name" t` holds

instruction	output contract
`SELF`	`"addr_of_current_contract"`
`SELF %default`	`"addr_of_current_contract"`
`SELF %A`	`"addr_of_current_contract%A"` if current contract has an entrypoint `%A` (and `A` <> `default`)

Michelson Reference

Introduction ¶

Execution environment ¶

Terminology ¶

Typing and Semantics Rules ¶

Typing Rules ¶

Semantics Rules ¶

Types ¶

Instructions ¶

Instructions by Category ¶

Control structures ¶

Stack manipulation ¶

Arithmetic operations ¶

Boolean operations ¶

Cryptographic operations ¶

Blockchain operations ¶

Operations on data structures ¶

Operations on tickets ¶

Operations on timelock ¶

Type Reference ¶

address ¶

Address of an untyped contract

big_map kty vty ¶

A lazily deserialized map from kty to vty

bls12_381_fr ¶

An element of the BLS12-381 scalar field Fr

bls12_381_g1 ¶

A point on the BLS12-381 curve G1

bls12_381_g2 ¶

A point on the BLS12-381 curve G2

bool ¶

A boolean

bytes ¶

A sequence of bytes

chain_id ¶

A chain identifier

chest ¶

A timelocked chest

chest_key ¶

A key to open a timelocked chest

contract type ¶

Address of a contract, where type is the contract's parameter type

int ¶

An arbitrary-precision integer

key ¶

A public cryptographic key

key_hash ¶

A hash of a public cryptographic key

lambda ty1 ty2 ¶

A lambda with given parameter and return types

list type ¶

A single, immutable, homogeneous linked list

map kty vty ¶

An immutable map from kty to vty

mutez ¶

A specific type for manipulating tokens

nat ¶

An arbitrary-precision natural number

never ¶

The empty type

operation ¶

An internal operation emitted by a contract

option ty ¶

An optional value

or ty1 ty2 ¶

A union of two types

pair ty1 ty2 ¶

A pair or tuple of values

sapling_state n ¶

A Sapling state

sapling_transaction n ¶

A Sapling transaction

set cty ¶

An immutable set of comparable values of type cty

signature ¶

A cryptographic signature

string ¶

A string of characters

ticket cty ¶

A ticket used to authenticate information of type cty

`address` ¶

`big_map kty vty` ¶

A lazily deserialized map from `kty` to `vty`

`bls12_381_fr` ¶

An element of the BLS12-381 scalar field F_r

`bls12_381_g1` ¶

A point on the BLS12-381 curve G₁

`bls12_381_g2` ¶

A point on the BLS12-381 curve G₂

`bool` ¶

`bytes` ¶

`chain_id` ¶

`chest` ¶

`chest_key` ¶

`contract type` ¶

`int` ¶

`key` ¶

`key_hash` ¶

`lambda ty1 ty2` ¶

`list type` ¶

`map kty vty` ¶

An immutable map from `kty` to `vty`

`mutez` ¶

`nat` ¶

`never` ¶

`operation` ¶

`option ty` ¶

`or ty1 ty2` ¶

`pair ty1 ty2` ¶

`sapling_state n` ¶

`sapling_transaction n` ¶

`set cty` ¶

An immutable set of comparable values of type `cty`

`signature` ¶

`string` ¶

`ticket cty` ¶

A ticket used to authenticate information of type `cty`

`timestamp` ¶

`unit` ¶

The type whose only value is `Unit`

`ABS` ¶

Example: `ABS` is the reverse of `NEG` on natural numbers ¶

`ADD` ¶

`ADDRESS` ¶

`AMOUNT` ¶

Example: Store `AMOUNT` ¶

`AND` ¶

`APPLY` ¶

`BALANCE` ¶

Example: Store `BALANCE` ¶

`BLAKE2B` ¶

`BYTES` ¶

`CAR` ¶

`CDR` ¶

`CHAIN_ID` ¶

`CHECK_SIGNATURE` ¶

Verify `signature` of `bytes` by `key`

`COMPARE` ¶

`CONCAT` ¶

`CONS` ¶

`CONTRACT ty` ¶

Example: From `address` to `contract` ¶

Example: Using `contract` with entrypoint annotations ¶

`CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 }` ¶

`DIG n` ¶

Retrieve the `n`th element of the stack

`DIP instr` ¶

`DIP n instr` ¶