Michelson Reference
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:
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.
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.
- 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.
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:
condition1 |
... |
conditionn |
|
|
conclusion |
| rule_name |
|
which means that when
condition1, ..., and
conditionn 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.
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:
Γ ⊢ instr1 :: A ⇒ B |
Γ ⊢ instr2 :: A ⇒ B |
|
|
Γ ⊢ IF instr1 instr2 :: bool : A ⇒ B |
| IF |
|
means that under a typing environment Γ, if both the
instr1 and
instr2 Michelson instructions expect a stack of type
A and return a stack of type
B, then the
IF instr1 instr2 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 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:
|
|
IF i1 i2 / False : S ⇒ S′ |
| IF__ff |
|
IF__tt means that the result of executing
IF i1 i2 on the stack
True :
S is exactly the result of executing
i1 on
S.
And similarly,
IF__ff means that the result of executing
IF i1 i2 on the stack
False :
S is exactly the result of executing
i2 on
S.
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_map
s.
- 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 Fr |
0
,
1
,
0x01
,
0x0001
|
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
bls12_381_g1 |
A point on the BLS12-381 curve G1 |
0x0572cbea904d67468808...
|
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
bls12_381_g2 |
A point on the BLS12-381 curve G2 |
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_map
s. The only type that is not duplicable is
ticket
.
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 nth 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 nth 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
|
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
|
Instruction |
Description |
Type |
DIG n |
Retrieve the nth 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 nth 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
|
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
|
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
|
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
|
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
|
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
|
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
|
Instruction |
Description |
Type |
OPEN_CHEST |
Open a timelocked chest given its key and the time |
chest_key : chest : nat : A — option bytes : A
|
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
An element of the BLS12-381 scalar field Fr
- Description
An element of the scalar field Fr, used for scalar multiplication on the
BLS12-381 curves G1 and G2.
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
- Example values
-
0
,
1
,
0x01
,
0x0001
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
A point on the BLS12-381 curve G1
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
- Example values
-
0x0572cbea904d67468808...
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
A point on the BLS12-381 curve G2
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
- Example values
-
0x0a4edef9c1ed7f729f52...
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✔ |
✘ |
✘ |
✔ |
✘ |
✔ |
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
,
0
,
1
,
99999
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
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 |
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
-
0
,
1
,
99999
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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
-
0
,
1
,
99999
- Related instructions
-
- Attributes
-
Comparable |
Passable |
Storable |
Pushable |
Packable |
big_map value |
Duplicable |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✘ |
✘ |
✘ |
✘ |
✘ |
✔ |
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 |
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 |
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 |
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 |
✘ |
✔ |
✔ |
✘ |
✘ |
✘ |
✔ |
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 |
✘ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✘ |
✔ |
✔ |
✘ |
✘ |
✔ |
✘ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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 |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
✔ |
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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.
parameter nat;
storage unit;
code { CAR;
DUP; NEG; ABS; COMPARE; ASSERT_EQ;
UNIT; NIL operation; PAIR}
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 / z1 : z2 : S ⇒ ( z1 + z2 ) : S |
| ADD |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This example demonstrates the addition of different types of numbers and domain specific types.
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;
}
Push the address of a contract
This instruction consumes a contract value and produces the address of that contract.
Typing
|
|
Γ ⊢ ADDRESS :: contract ty1 : 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)
This example takes a contract by parameter, and then stores its address.
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").
Push the amount of the current transaction
Push the amount of the current transaction, in mutez.
Typing
|
|
Γ ⊢ AMOUNT :: A ⇒ mutez : A |
| AMOUNT |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract stores the amount of its last received transaction.
parameter unit;
storage mutez;
code { DROP; AMOUNT; NIL operation; PAIR };
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 / z1 : z2 : S ⇒ ( z1 & z2 ) : S |
| AND__bit |
|
|
|
AND / bs1 : bs2 : S ⇒ ( bs1 & bs2 ) : S |
| AND__bytes |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contracts takes a pair of booleans, and computes and stores their conjunction.
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.
This contract demonstrates bitwise AND on numerical values.
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; };
This contract demonstrates bitwise AND on bytes.
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; };
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 :: ty1 : lambda ( pair ty1 ty2 ) ty3 : A ⇒ lambda ty2 ty3 : A |
| APPLY |
|
Semantics
|
|
APPLY / d : { i : ( pair ty1 ty2 ) → ty3 } : S ⇒ { PUSH ty1 d ; PAIR ; i : ty2 → ty3 } : S |
| APPLY |
|
|
|
APPLY / d : Lambda_rec i : S ⇒ { PUSH ty1 d ; PAIR ; LAMBDA_REC ty1 ty2 i ; SWAP ; EXEC : ty1 → ty2 } : S |
| APPLY__rec |
|
- Related types
-
- Available since mainnet protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
- Proposed in protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
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)
This contract stores its balance after its latest received transaction.
parameter unit;
storage mutez;
code {DROP; BALANCE; NIL operation; PAIR};
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)
This example computes the BLAKE2B hash of the string passed as parameter and puts it in storage.
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.
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)
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 ty1 ty2 : A ⇒ ty1 : A |
| CAR |
|
Semantics
|
|
CAR / ( Pair d1 d2 ) : S ⇒ d1 : S |
| CAR |
|
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract takes a pair as parameter. It selects the left
part of the parameter and stores 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.
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 ty1 ty2 : A ⇒ ty2 : A |
| CDR |
|
Semantics
|
|
CDR / ( Pair d1 d2 ) : S ⇒ d2 : S |
| CDR |
|
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract takes a pair as parameter. It selects the right
part of the parameter and stores 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.
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)
This contract pushes and then stores the chain identifier.
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").
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)
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.
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 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
|
|
COMPARE / z1 : z2 : S ⇒ − 1 : S |
| COMPARE__num_lt |
|
|
|
COMPARE / z1 : z2 : S ⇒ 0 : S |
| COMPARE__num_eq |
|
|
|
COMPARE / z1 : z2 : S ⇒ 1 : S |
| COMPARE__num_gt |
|
|
|
COMPARE / s : t : S ⇒ − 1 : S |
| COMPARE__string_lt |
|
|
|
COMPARE / s : t : S ⇒ 0 : S |
| COMPARE__string_eq |
|
|
|
COMPARE / s : t : S ⇒ 1 : S |
| COMPARE__string_gt |
|
COMPARE / d1 : d3 : S ⇒ − 1 : S |
|
|
COMPARE / ( Pair d1 d2 ) : ( Pair d3 d4 ) : S ⇒ − 1 : S |
| COMPARE__pair_left_lt |
|
COMPARE / d1 : d3 : S ⇒ 1 : S |
|
|
COMPARE / ( Pair d1 d2 ) : ( Pair d3 d4 ) : S ⇒ 1 : S |
| COMPARE__pair_left_gt |
|
COMPARE / d1 : d3 : S ⇒ 0 : S |
COMPARE / d2 : d4 : S ⇒ z : S |
|
|
COMPARE / ( Pair d1 d2 ) : ( Pair d3 d4 ) : 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 / d1 : d2 : S ⇒ z : S |
|
|
COMPARE / Some d1 : Some d2 : S ⇒ z : S |
| COMPARE__some_some |
|
|
|
COMPARE / Some d : None : S ⇒ 1 : S |
| COMPARE__some_none |
|
COMPARE / d1 : d2 : S ⇒ z : S |
|
|
COMPARE / Left d1 : Left d2 : S ⇒ z : S |
| COMPARE__left_left |
|
|
|
COMPARE / Left d1 : Right d2 : S ⇒ − 1 : S |
| COMPARE__left_right |
|
COMPARE / d1 : d2 : S ⇒ z : S |
|
|
COMPARE / Right d1 : Right d2 : S ⇒ z : S |
| COMPARE__right_right |
|
|
|
COMPARE / Right d1 : Left d2 : 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)
This contract demonstrate several types of comparisons over different values.
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.
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 ; < tl > } : S ⇒ s ^ t : S |
| CONCAT__string_list_cons |
|
|
|
CONCAT / byt1 : byt2 : S ⇒ byt1 ^ byt2 : S |
| CONCAT__bytes |
|
CONCAT / tl : S ⇒ byt2 : S |
|
|
CONCAT / { byt1 ; < tl > } : S ⇒ byt1 ^ byt2 : S |
| CONCAT__bytes_list_cons |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This example takes a list of strings as parameter. It prepends "Hello " to each of them and stores the result.
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" }.
This example takes a list of strings as parameter and concatenates them, and prepends value in storage and stores the resulting string.
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!".
This example takes a list of byte sequences as parameter. It prepends 0xff to each of them and stores the result.
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 }.
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.
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.
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 :: ty1 : list ty1 : A ⇒ list ty1 : 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)
This contracts keeps a list of integers in storage and takes an integer as parameter. It prepends the parameter to the stored list.
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 }.
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 |
|
|
|
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)
This contract receives an address by parameter, and converts it to a contract unit.
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.
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.
{ 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 } } }
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 ty1 ⊢ instr1 :: pair ty1 ty2 : [ ] ⇒ pair ( list operation ) ty2 : [ ] |
|
|
Γ ⊢ CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 } :: option key_hash : mutez : ty2 : A ⇒ operation : address : A |
| CREATE_CONTRACT |
|
Semantics
create_contract ty1 ty2 instr1 kh z x = ( op , addr ) |
|
|
CREATE_CONTRACT { parameter ty1 ; storage ty2 ; code instr1 } / kh : z : x : S ⇒ op : addr : S |
| CREATE_CONTRACT |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract originates a dummy contract.
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.
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"
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 } } ;
Retrieve the nth 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
|
|
Γ ⊢ DIG n :: A @ ( ty1 : B ) ⇒ ty1 : ( A @ B ) |
| DIG |
|
Semantics
|
|
DIG n / S1 ++ ( d : S2 ) ⇒ d : ( S1 ++ S2 ) |
| DIG |
|
- Available since mainnet protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
- Proposed in protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Run code protecting the top of the stack
DIP instr runs instr protecting the top
element of the stack.
Typing
|
|
Γ ⊢ DIP instr :: ty : B ⇒ ty : C |
| DIP |
|
Semantics
|
|
DIP instr / d : S ⇒ d : S′ |
| DIP |
|
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This examples takes a pair of integers (a, b) as parameter,
and stores (a, a + b)
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).
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 S1 = n |
instr / S2 ⇒ S3 |
|
|
DIP n instr / S1 ++ S2 ⇒ S1 ++ S3 |
| DIPN |
|
- Available since mainnet protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
- Proposed in protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
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.
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 the top element of the stack
Typing
Semantics
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
Semantics
- Available since mainnet protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
- Proposed in protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
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
|
|
Γ ⊢ DUG n :: ty1 : ( A @ B ) ⇒ A @ ( ty1 : B ) |
| DUG |
|
Semantics
|
|
DUG n / d : ( S1 ++ S2 ) ⇒ S1 ++ ( d : S2 ) |
| DUG |
|
- Available since mainnet protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
- Proposed in protocol
-
Babylon (PsBabyM1eUXZseaJdmXFApDSBqj8YBfwELoxZHHW77EMcAbbwAS)
Duplicate the top of the stack
Typing
|
|
Γ ⊢ DUP :: ty1 : A ⇒ ty1 : ty1 : A |
| DUP |
|
Semantics
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Duplicate the nth 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 : ....
See also DIG.
Typing
|
|
Γ ⊢ DUP n :: A @ ty1 : B ⇒ ty1 : A @ ty1 : B |
| DUPN |
|
Semantics
|
|
DUP n / S1 ++ d : S2 ⇒ d : S1 ++ d : S2 |
| DUPN |
|
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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 / z1 : 0 : S ⇒ None : S |
| EDIV__0 |
|
|
|
EDIV / z1 : z2 : S ⇒ Some ( Pair ( z1 / z2 ) ( z1 % z2 ) ) : S |
| EDIV |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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)
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)
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)
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 |
| EQ |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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 :: ty1 : lambda ty1 ty2 : A ⇒ ty2 : A |
| EXEC |
|
Semantics
|
|
EXEC / d1 : { i : ty1 → ty2 } : S ⇒ d2 : S |
| EXEC |
|
i / d1 : Lambda_rec i : [ ] ⇒ d2 : [ ] |
|
|
EXEC / d1 : Lambda_rec i : S ⇒ d2 : S |
| EXEC__rec |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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 :: ty1 : A ⇒ B |
| FAILWITH |
|
Semantics
|
|
FAILWITH / d : stack ⇒ [FAILED] |
| FAILWITH |
|
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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 |
| GE |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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 ty1 ty2 : A ⇒ ty1 : A |
| GETN__1 |
|
Γ ⊢ GET n :: ty2 : A ⇒ ty : A |
|
|
Γ ⊢ GET ( n + 2 ) :: pair ty1 ty2 : A ⇒ ty : A |
| GETN__ind |
|
Semantics
|
|
GET 1 / Pair d d′ : S ⇒ d : S |
| GETN__1 |
|
|
|
GET ( n + 2 ) / Pair d1 d2 : S ⇒ d : S |
| GETN__ind |
|
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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)
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 |
| GT |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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
Γ ⊢ instr1 :: A ⇒ B |
Γ ⊢ instr2 :: A ⇒ B |
|
|
Γ ⊢ IF instr1 instr2 :: bool : A ⇒ B |
| IF |
|
Semantics
|
|
IF i1 i2 / False : S ⇒ S′ |
| IF__ff |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
Γ ⊢ instr1 :: ty : list ty : A ⇒ B |
Γ ⊢ instr2 :: A ⇒ B |
|
|
Γ ⊢ IF_CONS instr1 instr2 :: list ty : A ⇒ B |
| IF_CONS |
|
Semantics
|
|
IF_CONS instr1 instr2 / {} : S ⇒ S′ |
| IF_CONS__nil |
|
|
|
IF_CONS instr1 instr2 / { d ; < tl > } : S ⇒ S′ |
| IF_CONS__cons |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
Γ ⊢ instr1 :: ty1 : A ⇒ B |
Γ ⊢ instr2 :: ty2 : A ⇒ B |
|
|
Γ ⊢ IF_LEFT instr1 instr2 :: or ty1 ty2 : A ⇒ B |
| IF_LEFT |
|
Semantics
|
|
IF_LEFT instr1 instr2 / ( Left d1 ) : S ⇒ S′ |
| IF_LEFT__left |
|
|
|
IF_LEFT instr1 instr2 / ( Right d2 ) : S ⇒ S′ |
| IF_LEFT__right |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
Γ ⊢ instr1 :: A ⇒ B |
Γ ⊢ instr2 :: ty1 : A ⇒ B |
|
|
Γ ⊢ IF_NONE instr1 instr2 :: option ty1 : A ⇒ B |
| IF_NONE |
|
Semantics
|
|
IF_NONE instr1 instr2 / None : S ⇒ S′ |
| IF_NONE__none |
|
|
|
IF_NONE instr1 instr2 / ( Some d ) : S ⇒ S′ |
| IF_NONE__some |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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 / byt : S ⇒ decode_int_be byt : S |
| INT__bytes |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
|
|
ISNAT / z : S ⇒ Some ( tonat z ) : S |
| ISNAT__ok |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
|
|
Γ ⊢ ITER instr :: list ty : A ⇒ A |
| ITER__list |
|
|
|
Γ ⊢ ITER instr :: set cty : A ⇒ A |
| ITER__set |
|
Γ ⊢ instr :: ( pair kty vty ) : A ⇒ A |
|
|
Γ ⊢ ITER instr :: map kty vty : A ⇒ A |
| ITER__map |
|
Semantics
instr / d : S ⇒ S′ |
ITER instr / tl : S′ ⇒ S″ |
|
|
ITER instr / { d ; < tl > } : S ⇒ S″ |
| ITER__list_cons |
|
instr / x : S ⇒ S′ |
ITER instr / tl : S′ ⇒ S″ |
|
|
ITER instr / { x ; < tl > } : S ⇒ S″ |
| ITER__set_cons |
|
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 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 n1 ) ( Pair s x n2 ) : S ⇒ Some ( Pair s x ( n1 + n2 ) ) : S |
| JOIN_TICKETS__some |
|
|
|
JOIN_TICKETS / Pair ( Pair s1 x1 n1 ) ( Pair s2 x2 n2 ) : S ⇒ None : S |
| JOIN_TICKETS__none_ticketer |
|
|
|
JOIN_TICKETS / Pair ( Pair s1 x1 n1 ) ( Pair s2 x2 n2 ) : S ⇒ None : S |
| JOIN_TICKETS__none_content |
|
- Related types
-
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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)
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 :: ty1 : [ ] ⇒ ty2 : [ ] |
|
|
Γ ⊢ LAMBDA ty1 ty2 instr :: A ⇒ lambda ty1 ty2 : A |
| LAMBDA |
|
Semantics
|
|
LAMBDA ty1 ty2 instr / S ⇒ { instr : ty1 → ty2 } : S |
| LAMBDA |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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 :: ty1 : lambda ty1 ty2 : [ ] ⇒ ty2 : [ ] |
|
|
Γ ⊢ LAMBDA_REC ty1 ty2 instr :: A ⇒ lambda ty1 ty2 : A |
| LAMBDA_REC |
|
Semantics
|
|
LAMBDA_REC ty1 ty2 instr / S ⇒ Lambda_rec instr : S |
| LAMBDA_REC |
|
- Related types
-
- Available since mainnet protocol
-
Lima (PtLimaPtLMwfNinJi9rCfDPWea8dFgTZ1MeJ9f1m2SRic6ayiwW)
- Proposed in protocol
-
Lima (PtLimaPtLMwfNinJi9rCfDPWea8dFgTZ1MeJ9f1m2SRic6ayiwW)
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.
# 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.
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 |
| LE |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Wrap a value in a union (left case)
Typing
|
|
Γ ⊢ LEFT ty2 :: ty1 : A ⇒ or ty1 ty2 : A |
| LEFT |
|
Semantics
|
|
LEFT ty2 / v : S ⇒ ( Left v ) : S |
| LEFT |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Push the current block level
Typing
Semantics
- Related types
-
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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 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 :: ty1 : A ⇒ or ty1 ty2 : A |
|
|
Γ ⊢ LOOP_LEFT instr :: or ty1 ty2 : A ⇒ ty2 : A |
| LOOP_LEFT |
|
Semantics
i1 ; LOOP_LEFT i1 / d : S ⇒ S′ |
|
|
LOOP_LEFT i1 / Left d : S ⇒ S′ |
| LOOP_LEFT__tt |
|
|
|
LOOP_LEFT i1 / Right d : S ⇒ d : S′ |
| LOOP_LEFT__ff |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract reverses the list of strings passed by parameter and stores 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" }.
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
|
|
LSL / z1 : z2 : S ⇒ ( z1 ≪ z2 ) : S |
| LSL__nat |
|
|
|
LSL / z1 : z2 : S ⇒ [FAILED] |
| LSL__nat_fail |
|
|
|
LSL / bs1 : n : S ⇒ ( bs1 << n ) : S |
| LSL__bytes |
|
|
|
LSL / bs1 : n : S ⇒ [FAILED] |
| LSL__bytes_fail |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
This contract demonstrates LSL on bytes.
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; };
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
|
|
LSR / z1 : z2 : S ⇒ ( z1 ≫ z2 ) : S |
| LSR__nat |
|
|
|
LSR / z1 : z2 : 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)
This contract demonstrates LSR on bytes.
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; };
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 |
| LT |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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.
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; MAP
{instr} should be used.
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 ⇒ ty2 : A |
|
|
Γ ⊢ MAP instr :: list ty : A ⇒ list ty2 : A |
| MAP__list |
|
Γ ⊢ instr :: ty : A ⇒ ty2 : A |
|
|
Γ ⊢ MAP instr :: option ty : A ⇒ option ty2 : A |
| MAP__option |
|
Γ ⊢ instr :: ( pair kty ty1 ) : A ⇒ ty2 : A |
|
|
Γ ⊢ MAP instr :: map kty ty1 : A ⇒ map kty ty2 : 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 |
|
|
|
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)
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)
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)
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 / z1 : z2 : S ⇒ ( z1 * z2 ) : S |
| MUL |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
Close a forbidden branch
Typing
|
|
Γ ⊢ NEVER :: never : A ⇒ B |
| NEVER |
|
Semantics
- Related types
-
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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 |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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 / z1 : z2 : S ⇒ ( z1 ∣ z2 ) : S |
| OR__bit |
|
|
|
OR / bs1 : bs2 : S ⇒ ( bs1 ∣ bs2 ) : S |
| OR__bytes |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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.
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.
Build a pair from the stack's top two elements
Typing
|
|
Γ ⊢ PAIR :: ty1 : ty2 : A ⇒ pair ty1 ty2 : A |
| PAIR |
|
Semantics
|
|
PAIR / d1 : d2 : S ⇒ ( Pair d1 d2 ) : S |
| PAIR |
|
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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
|
|
Γ ⊢ PAIR n :: ty1 : .... : tyN : A ⇒ pair ty1 .... tyN : A |
| PAIRN |
|
Semantics
|
|
PAIR n / d1 : .... : dN : S ⇒ ( Pair d1 .... dN ) : S |
| PAIRN |
|
- Proposed in protocol
-
Edo (PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA)
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.
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).
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 a constant value of a given type onto the stack
Typing
|
|
Γ ⊢ PUSH ty x :: A ⇒ ty : A |
| PUSH |
|
Semantics
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
Wrap a value in a union (right case)
Typing
|
|
Γ ⊢ RIGHT ty1 :: ty2 : A ⇒ or ty1 ty2 : A |
| RIGHT |
|
Semantics
|
|
RIGHT ty1 / v : S ⇒ ( Right v ) : S |
| RIGHT |
|
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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)
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)
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
|
|
Γ ⊢ SELF :: A ⇒ contract ty : A |
| SELF |
|
Semantics
- Related types
-
- Available since mainnet protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
- Proposed in protocol
-
Alpha I (PtCJ7pwoxe8JasnHY8YonnLYjcVHmhiARPJvqcC6VfHT5s8k8sY)
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.
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
}
This example demonstrates using SELF with and without entrypoint annotations, as well as the default entrypoint.
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