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:
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.
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
Γ ⊢ IFinstr1instr2 :: 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 IFinstr1instr2 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:
i1 / S ⇒ S′
IFi1i2 / True : S ⇒ S′
IF__tt
i2 / S ⇒ S′
IFi1i2 / False : S ⇒ S′
IF__ff
IF__tt means that the result of executing IFi1i2 on the stack True : S is exactly the result of executing i1 on S.
And similarly, IF__ff means that the result of executing IFi1i2 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)
Values of comparable types can be compared using the COMPARE instruction, can be stored as elements in sets, can index maps and big maps, and can be used as ticket payloads.
Passable (PM)
Values of passable types can be taken as a parameter in contracts.
Storable (S)
Values of storable types are allowed to appear inside the storage of contracts.
Pushable (PU)
Literal values of pushable types can be given as parameter to the PUSH instruction. Values of pushable types can also be emmitted using the EMIT instruction, returned as error value using the FAILWITH instruction, and deserialized using the UNPACK instruction.
Packable (PA)
Values of packable types can be serialized using the PACK instruction.
big_map value (B)
big_map values can be stored as values in big_maps.
Duplicable (D)
Literal values of duplicable types can be given as parameter to the DUP instruction.
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. ¶
All pushable types are also packable but contract is
packable without being pushable. Except for the domain specific
types operation, contract,
ticket, sapling_state and big_map, all
types are passable, storable, pushable, packable and can be used as values in
big_maps. The only type that is not duplicable is ticket.
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
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
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 : 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
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
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
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 : 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
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.
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.
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.
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.
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.
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.
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> }.
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.
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.
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}}.
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.
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.
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.
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.
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
parameterunit;storageunit;code{CAR;PUSHint2;PUSHint2;ADD;PUSHint4;ASSERT_CMPEQ;PUSHint2;PUSHint2;ADD;PUSHint4;ASSERT_CMPEQ;PUSHint2;PUSHnat2;ADD;PUSHint4;ASSERT_CMPEQ;PUSHnat2;PUSHint2;ADD;PUSHint4;ASSERT_CMPEQ;PUSHnat2;PUSHnat2;ADD;PUSHnat4;ASSERT_CMPEQ;# Offset a timestamp by 60 secondsPUSHint60;PUSHtimestamp"2019-09-09T12:08:37Z";ADD;PUSHtimestamp"2019-09-09T12:09:37Z";ASSERT_CMPEQ;PUSHtimestamp"2019-09-09T12:08:37Z";PUSHint60;ADD;PUSHtimestamp"2019-09-09T12:09:37Z";ASSERT_CMPEQ;PUSHmutez1000;PUSHmutez1000;ADD;PUSHmutez2000;ASSERT_CMPEQ;NILoperation;PAIR;}
If called with the initial
storage None and the
parameter "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv" then the final storage
will be (Some "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv").
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.
parameterunit;storageunit;code{DROP;# 0x05 & 0x06 = 0x04PUSHbytes0x05;PUSHbytes0x06;AND;PUSHbytes0x04;ASSERT_CMPEQ;# 0x0005 & 0x0106 = 0x0004, not 0x04PUSHbytes0x0005;PUSHbytes0x0106;AND;PUSHbytes0x0004;ASSERT_CMPEQ;# Longer bytes is cut its prefix to have the same length as the shorter one# 0x05 & 0x0106 = 0x05 & 0x06 = 0x04, not 0x0004PUSHbytes0x05;PUSHbytes0x0106;AND;PUSHbytes0x04;ASSERT_CMPEQ;UNIT;NIL@noopoperation;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 ( pairty1ty2 ) ty3 : A ⇒ lambdaty2ty3 : A
APPLY
Semantics
APPLY / d : { i : ( pairty1ty2 ) → ty3 } : S ⇒ { PUSHty1d ; PAIR ; i : ty2 → ty3 } : S
APPLY
APPLY / d : Lambda_reci : S ⇒ { PUSHty1d ; PAIR ; LAMBDA_RECty1ty2i ; SWAP ; EXEC : ty1 → ty2 } : S
If called with the initial
storage 0x and the
parameter "foobar" then the final storage
will be 0xc5b7e76c15ce98128a840b54c38f462125766d2ed3a6bff0e76f7f3eb415df04.
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.
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.
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_signaturessigbyt : S
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.
If called with the initial
storage (Pair "edsigu3QszDjUpeqYqbvhyRxMpVFamEnvm9FYnt7YiiNt9nmjYfh8ZTbsybZ5WnBkhA7zfHsRVyuTnRsGLR6fNHt1Up1FxgyRtF" "hello") and the
parameter "edpkuBknW28nW72KG6RoHtYW7p12T6GKc7nAbwYX5m8Wd9sDVC9yav" then the final storage
will be (Pair "edsigu3QszDjUpeqYqbvhyRxMpVFamEnvm9FYnt7YiiNt9nmjYfh8ZTbsybZ5WnBkhA7zfHsRVyuTnRsGLR6fNHt1Up1FxgyRtF" "hello").
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.
If called with the initial
storage {} and the
parameter { 0xab ; 0xcd } then the final storage
will be { 0xffab ; 0xffcd }.
Example: Concatenation of list of byte sequences ¶
This example takes a list of byte sequences as parameter and concatenates them, and prepends the value in storage and stores the resulting byte sequence.
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:
If called with the initial
storage Unit and the
parameter "tz1b7tUupMgCNw2cCLpKTkSD1NZzB5TkP2sv" then the final storage
will be Unit.
Example: Using contract with entrypoint annotations ¶
When this contract is called by anyone except itself, it
originates a new contract with three entrypoints: add,
sub and default and saves its address in its
storage. It then emits a transaction to itself.
When the contract receives a transaction from itself, it
verifies that the stored address can be converted to a
contract for each of the entrypoints add, sub and
default with the respective types nat, nat and
unit using the CONTRACT instruction annotated with the
respective entrypoint. It verifies that the entrypoint
default has the type unit, and that this is equivalent
to to using CONTRACT with no entrypoint annotation. It
also emits transactions to these entrypoints.
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.
parameterunit;storage(optionaddress);code{DROP;UNIT;# starting storage for contractAMOUNT;# Push the starting balanceNONEkey_hash;# No delegateCREATE_CONTRACT# Create the contract{parameterunit;storageunit;code{CDR;NILoperation;PAIR;}};DIP{SOME;NILoperation};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.
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 : ....
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.
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.
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 : ....
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 : ....
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 ( pairnatnat ) : A
EDIV__nat_nat
Γ ⊢ EDIV :: nat : int : A ⇒ option ( pairintnat ) : A
EDIV__nat_int
Γ ⊢ EDIV :: int : nat : A ⇒ option ( pairintnat ) : A
EDIV__int_nat
Γ ⊢ EDIV :: int : int : A ⇒ option ( pairintnat ) : A
EDIV__int_int
Γ ⊢ EDIV :: mutez : nat : A ⇒ option ( pairmutezmutez ) : A
EDIV__mutez_nat
Γ ⊢ EDIV :: mutez : mutez : A ⇒ option ( pairnatmutez ) : A
EDIV__mutez_mutez
Semantics
EDIV / z1 : 0 : S ⇒ None : S
EDIV__0
z2 ≠ 0
EDIV / z1 : z2 : S ⇒ Some ( Pair ( z1 / z2 ) ( z1 % z2 ) ) : S
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 pushable types can be emitted.
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.
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.
This instruction aborts the current program exposing the top element of the stack, which must be of a pushable 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.
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.
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 : mapktyvty : A ⇒ optionvty : A
GET__map
Γ ⊢ GET :: kty : big_mapktyvty : A ⇒ optionvty : A
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.
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.
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.
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.
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.
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.
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.
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.
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 ( ticketcty ) ( ticketcty ) : A ⇒ option ( ticketcty ) : A
JOIN_TICKETS
Semantics
JOIN_TICKETS / Pair ( Pairsxn1 ) ( Pairsxn2 ) : S ⇒ Some ( Pairsx ( n1 + n2 ) ) : S
JOIN_TICKETS__some
s1 ≠ s2
JOIN_TICKETS / Pair ( Pairs1x1n1 ) ( Pairs2x2n2 ) : S ⇒ None : S
JOIN_TICKETS__none_ticketer
x1 ≠ x2
JOIN_TICKETS / Pair ( Pairs1x1n1 ) ( Pairs2x2n2 ) : S ⇒ None : S
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.
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.parameternat;storagenat;code{CAR;LAMBDA_RECnatnat# Let us call f the block below.{# Stack is: n, f# where n is the factorial's parameter.PUSHint-1;ADD;# Stack is: n-1, f.ISNAT;IF_NONE# If n-1 is not a natural, i.e. n = 0, return 1.{DROP;PUSHnat1}# Else, run f(n-1) and multiply the result by n (= n-1 + 1).{DUP;DIP{EXEC};PUSHnat1;ADD;MUL}};SWAP;EXEC;NILoperation;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.
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.
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.
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.
parameterunit;storageunit;code{DROP;# If shift is 0, LSL returns the bytes untouched# 0x06 LSL 0 = 0x06PUSHnat0;PUSHbytes0x06;LSL;PUSHbytes0x06;ASSERT_CMPEQ;# If shift is not 0, LSL returns a bytes longer than the original# 0x06 LSL 1 = 0x000c (not 0x0c)PUSHnat1;PUSHbytes0x06;LSL;PUSHbytes0x000c;ASSERT_CMPEQ;# 0x06 LSL 8 = 0x0600PUSHnat8;PUSHbytes0x06;LSL;PUSHbytes0x0600;ASSERT_CMPEQ;# 0x0006 LSL 1 = 0x00000c (not 0x0c nor 0x000c)PUSHnat1;PUSHbytes0x0006;LSL;PUSHbytes0x00000c;ASSERT_CMPEQ;UNIT;NIL@noopoperation;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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
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.
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 ( pairbls12_381_g1bls12_381_g2 ) : A ⇒ bool : A
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.
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 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(or(nat%A)(bool%B))(or%maybe_C(unit%default)(string%C)));storageunit;code{DROP;SELF;DROP;# Refers to entrypoint A of the current contract.SELF%A;DROP;# Refers to the default entry of the current contractSELF%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;NILoperation;PAIR;}
This example demonstrates using SELF with and without entrypoint annotations. In this example, the CAST noop is used to assert the type of the contract pushed by SELF.
parameter(or(or(nat%A)(bool%B))(or%maybe_C(unit%Z)(string%C)));storageunit;code{DROP;# Refers to entrypoint A of the current contract.SELF%A;PACK@Apacked;# Refers to the default entry of the current contractSELF%default;PACK@defpacked;DUP;DIP{SWAP};ASSERT_CMPNEQ;# "SELF" w/o annotation also refers to the default# entry of the current contractSELF;PACK@selfpacked;ASSERT_CMPEQ;# Verify the types of the different entrypoints. CAST is noop# if its argument is convertible with the type of the top of# the stack.SELF%A;CAST(contractnat);DROP;SELF%B;CAST(contractbool);DROP;SELF%maybe_C;CAST(contract(or(unit)(string)));DROP;SELF%Z;CAST(contractunit);DROP;SELF;CAST(contract(or(or(nat%A)(bool%B))(or%maybe_C(unit%Z)(string%C))));DROP;SELF%default;CAST(contract(or(or(nat%A)(bool%B))(or%maybe_C(unit%Z)(string%C))));DROP;UNIT;NILoperation;PAIR;}
Push the address of the current contract. This is
equivalent to SELF; ADDRESS except that it is allowed in
lambdas.
Note that SELF_ADDRESS inside a lambda returns the address of the
contract executing the lambda, which can be different from the address
of the contract in which the SELF_ADDRESS instruction is written.
Push the contract that initiated the current internal transaction
Push the contract that initiated the current
internal transaction. It may be the SOURCE, but may
also not if the source sent an order to an intermediate
smart contract, which then called the current contract.
Consider a scenario involving two contracts, receiver and
proxy. The contract proxy, transfers any amount
received in a call to receiver. Assume a third
contract bootstrap2 creates a transaction to the proxy
contract sending 99 ꜩ . Then proxy creates an internal
transaction that calls receiver:
In this scenario, the source of the internal transaction (from
proxy to receiver) is bootstrap2, whereas the sender
of that transaction is the proxy. That is, if SOURCE is
called in receiver, then the address of bootstrap2 is
returned. If SENDER is called in receiver, then the address
of proxy is returned.
If instead, bootstrap2 calls receiver directly, then
bootstrap2 would be both source and sender.
The SET_DELEGATE instruction is used to add, update or remove a
delegation. It consumes an operand of type option
key_hash.
Using this instruction is the only way to modify the delegation of a
smart contract. If the parameter is None then the delegation of the
current contract is withdrawn. If the contract
has no delegation, then no change occurs.
If the parameter is Some kh where kh is the
key hash of a registered delegate that is not the current delegate of
the contract, then this operation sets the delegate of the contract to
this registered delegate. A failure occurs if kh is the current
delegate of the contract or if kh is not a registered delegate.
However, the instruction in itself does not fail; it procudes an operation
that will fail when applied.
Note that tz4 addresses cannot be registered as delegates.
Typing
Γ ⊢ SET_DELEGATE :: optionkey_hash : A ⇒ operation : A
The SIZE instruction consumes the
top element of the stack and returns its "size" (see below) as a nat. It is defined for values of type string, list, set, map and byte sequences bytes.
For a string value, it returns the number of characters.
Obtain a substring or subsequence of a string respectively byte sequence bytes
The SLICE instruction consumes two natural numbers offset and len
and a character sequence (string) or bytes sequence (bytes).
If offset and len are in bounds, i.e.
offset < length and
offset + len <= length (where length is the length
of the sequence), then it returns a substring, respectively
subsequence, Some v of
length len starting at offset (where offset 0 denotes
the first element) of the sequence.
If offset or len is out of bounds, i.e.
offset >= length or
offset + len > length (where length is the length
of the sequence), then None is returned.
Note that if the offset is out of bounds, None is
returned, even if len is 0. Consequently, SLICE on an
empty string always returns None.
Examples:
sequence
offset
len
output
comment
"foobar"
0
0
Some ""
"foobar"
0
3
Some "foo"
"foobar"
3
3
Some "bar"
"foobar"
3
4
None
offset + len is out of bounds
"foobar"
6
0
None
offset is out of bounds
"foobar"
7
0
None
offset is out of bounds
""
0
0
None
offset is out of bounds
Typing
Γ ⊢ SLICE :: nat : nat : string : A ⇒ optionstring : A
SLICE__string
Γ ⊢ SLICE :: nat : nat : bytes : A ⇒ optionbytes : A
SLICE__bytes
Semantics
offset + len < lengths
SLICE / offset : len : s : S ⇒ Some ( slicesoffsetlen ) : S
SLICE__string_ok
offset + len ≥ lengths
SLICE / offset : len : s : S ⇒ None : S
SLICE__string_fail
offset + len < lengthbyt
SLICE / offset : len : byt : S ⇒ Some ( slicebytoffsetlen ) : S
Push the contract that initiated the current transaction
Push the contract who signed the transaction initiating this
execution. Note that this contract is necessarily an implicit
account since smart contracts can't sign transactions. They can
however emit internal, unsigned, transactions.
Since TRANSFER_TOKENS instructions can be chained,
SOURCE and SENDER are not necessarily the same. See
SENDER for a more detailed discussion of this distinction.
Delete the given ticket and create two tickets with the
same content and ticketer as the original, but with the new provided amounts.
(This can be used to easily implement UTXOs.)
Return None iff the ticket's original amount is not equal to the sum of the
provided amounts, or one of the provided amounts is zero.
Computes the difference between two mutez amounts. If this
difference is negative -- and thus cannot be represented using the mutez
type -- then None is returned. Otherwise, the difference is
returned, wrapped in a Some.
Return the total voting power of all contracts. The total
voting power coincides with the sum of the stake of every contract in
the voting listings. The voting listings is calculated at the beginning of
every voting period.
The TRANSFER_TOKENS instruction consumes a value d of type ty,
an amount z in mutez and a contract c of type contract ty. It returns
a transfer operation that will send z mutez to the
specified contract c with the parameter d.
Consequently, the parameter value must be consistent with the
parameter type of the contract. In the case the contract is an
implicit account, then the parameter must be Unit.
Typing
Γ ⊢ TRANSFER_TOKENS :: ty : mutez : contractty : A ⇒ operation : A
TRANSFER_TOKENS
Semantics
TRANSFER_TOKENS / d : z : c : S ⇒ transfer_tokensdzc : S
Deserialize a value of type bytes into the corresponding
Michelson value of type option ty where ty is a pushable
type. If the top of the stack is not the serialization of a
Michelson value of type ty, then None is pushed.
Otherwise, Some v is pushed, where v is the deserialized
value.
parameter(pairintnatstringbytesmutezboolkey_hashtimestampaddress);storageunit;code{CAR;# Check the intDUP;CAR;DIP{UNPAIR;};PACK;UNPACKint;ASSERT_SOME;ASSERT_CMPEQ;# Check the natDUP;CAR;DIP{UNPAIR;};PACK;UNPACKnat;ASSERT_SOME;ASSERT_CMPEQ;# Check the stringDUP;CAR;DIP{UNPAIR;};PACK;UNPACKstring;ASSERT_SOME;ASSERT_CMPEQ;# Check the bytesDUP;CAR;DIP{UNPAIR;};PACK;UNPACKbytes;ASSERT_SOME;ASSERT_CMPEQ;# Check the mutezDUP;CAR;DIP{UNPAIR;};PACK;UNPACKmutez;ASSERT_SOME;ASSERT_CMPEQ;# Check the boolDUP;CAR;DIP{UNPAIR;};PACK;UNPACKbool;ASSERT_SOME;ASSERT_CMPEQ;# Check the key_hashDUP;CAR;DIP{UNPAIR;};PACK;UNPACKkey_hash;ASSERT_SOME;ASSERT_CMPEQ;# Check the timestampDUP;CAR;DIP{UNPAIR;};PACK;UNPACKtimestamp;ASSERT_SOME;ASSERT_CMPEQ;# Check the addressDUP;PACK;UNPACKaddress;ASSERT_SOME;ASSERT_CMPEQ;# Assert failure modes of unpackPUSHint0;PACK;UNPACKnat;ASSERT_SOME;DROP;PUSHint-1;PACK;UNPACKnat;ASSERT_NONE;# Try deserializing invalid byte sequence (no magic number)PUSHbytes0x;UNPACKnat;ASSERT_NONE;PUSHbytes0x04;UNPACKnat;ASSERT_NONE;# Assert failure for byte sequences that do not correspond to# any micheline valuePUSHbytes0x05;UNPACKnat;ASSERT_NONE;UNIT;NILoperation;PAIR}
If called with the initial
storage Unit and the
parameter (Pair -1 (Pair 1 (Pair "foobar" (Pair 0x00AABBCC (Pair 1000 (Pair False (Pair "tz1cxcwwnzENRdhe2Kb8ZdTrdNy4bFNyScx5" (Pair "2019-09-09T08:35:33Z""tz1cxcwwnzENRdhe2Kb8ZdTrdNy4bFNyScx5")))))))) then the final storage
will be Unit.
This contract demonstrates the use of the UNPAIR instruction
with an arity of 3. This contract takes 3 digits (represented
as natural numbers) as parameter, computes the number
composed of these 3 digits and puts it in its storage.
The 3 inputs are given as a comb of size 3 that is decomposed
into 3 stack elements using the UNPAIR 3 instruction.
Add, update, or remove an element in a map, big_map or set
For values of type map and big_map, the instruction UPDATE consumes
a key, an optional value and a value of type map or big_map.
It returns the same map, but updated in the following way:
If the value is Some y then key is assigned to y in
the resulting map, either adding the binding if key was not present in
the map beforehand, or updating it otherwise.
If the value is None and the key is present in the map,
then it is removed in the resulting map. If the key is not
present, an unmodified map is returned.
For values of type set, the instruction UPDATE consumes
a value x, a boolean flag b and a set s. It returns the same set,
but updated in the following way:
If b is True then the value x is added to the set s.
If x was already present in s, then the original set is returned.
If b is False then the value x is removed from s.
If x is not present in s, then the original set is returned.
Typing
Γ ⊢ UPDATE :: cty : bool : setcty : A ⇒ setcty : A
UPDATE__set
Γ ⊢ UPDATE :: kty : optionvty : mapktyvty : A ⇒ mapktyvty : A
UPDATE__map
Γ ⊢ UPDATE :: kty : optionvty : big_mapktyvty : A ⇒ big_mapktyvty : A
UPDATE__big_map
Semantics
UPDATE / x : False : {} : S ⇒ {} : S
UPDATE__set_false
UPDATE / x : True : {} : S ⇒ { x } : S
UPDATE__set_add_nexists
COMPARE / x : y : [ ] ⇒ 1 : [ ]
UPDATE / x : b : tl : S ⇒ tl′ : S
UPDATE / x : b : { y ; < tl > } : S ⇒ { y ; < tl′ > } : S
UPDATE__set_cont
COMPARE / x : y : [ ] ⇒ 0 : [ ]
UPDATE / x : False : { y ; < tl > } : S ⇒ tl : S
UPDATE__set_remove
COMPARE / x : y : [ ] ⇒ 0 : [ ]
UPDATE / x : True : { y ; < tl > } : S ⇒ { y ; < tl > } : S
UPDATE__set_exists
COMPARE / x : y : [ ] ⇒ − 1 : [ ]
UPDATE / x : False : { y ; < tl > } : S ⇒ { y ; < tl > } : S
UPDATE__set_remove_nexists
COMPARE / x : y : [ ] ⇒ − 1 : [ ]
UPDATE / x : True : { y ; < tl > } : S ⇒ { x ; < { y ; < tl > } > } : S
UPDATE__set_add
UPDATE / x : None : {} : S ⇒ {} : S
UPDATE__map_false
UPDATE / x : Somey : {} : S ⇒ { Eltxy } : S
UPDATE__map_add_nexists
COMPARE / x : k : [ ] ⇒ 1 : [ ]
UPDATE / x : opt_y : m : S ⇒ m′ : S
UPDATE / x : opt_y : { Eltkv ; < m > } : S ⇒ { Eltkv ; < m′ > } : S
UPDATE__map_cont
COMPARE / x : k : [ ] ⇒ 0 : [ ]
UPDATE / x : None : { Eltkv ; < m > } : S ⇒ m : S
UPDATE__map_remove
COMPARE / x : k : [ ] ⇒ 0 : [ ]
UPDATE / x : Somey : { Eltkv ; < m > } : S ⇒ { Eltky ; < m > } : S
UPDATE__map_exists
COMPARE / x : k : [ ] ⇒ − 1 : [ ]
UPDATE / x : None : { Eltkv ; < m > } : S ⇒ { Eltkv ; < m > } : S
UPDATE__map_remove_nexists
COMPARE / x : k : [ ] ⇒ − 1 : [ ]
UPDATE / x : Somey : { Eltkv ; < m > } : S ⇒ { Eltxy ; < { Eltkv ; < m > } > } : S
Update an element or a sub comb in a right comb. The topmost stack element is
the new value to insert in the comb, the second stack element is the right
comb to update. The meaning of n is the same as for the GETN
instruction.
Typing
Γ ⊢ UPDATE 0 :: ty1 : ty2 : A ⇒ ty1 : A
UPDATEN__0
Γ ⊢ UPDATE 1 :: ty : pairty1ty2 : A ⇒ pairtyty2 : A
UPDATEN__1
Γ ⊢ UPDATEn :: ty : ty2 : A ⇒ ty′ : A
Γ ⊢ UPDATE ( n + 2 ) :: ty : pairty1ty2 : A ⇒ pairty1ty′ : A
UPDATEN__ind
Semantics
UPDATE 0 / d1 : d2 : S ⇒ d1 : S
UPDATEN__0
UPDATE 1 / d : Paird1d2 : S ⇒ Pairdd2 : S
UPDATEN__1
UPDATEn / d : d2 : S ⇒ d′ : S
UPDATE ( n + 2 ) / d : Paird1d2 : S ⇒ Paird1d′ : S
Call the view named name from the contract whose address is the
second element of the stack, sending it as input the top element of
the stack.
If the given address is nonexistent or if the contract at that address
does not have a view of the expected name and type, None will be
returned; this is represented by the no_view predicate in the
semantics rules. Otherwise, Some a will be returned where a is the
result of the view call; this is represented by the view predicate in
the semantics rules. This means that the rule's precondition,
view addr name x return a, is true if and only if addr is the
address of a smart contract c with storage s where c has a
toplevel declaration of the form view name arg return { code }, where
arg is the type of x, and running code on the stack
Pair x s : [] yields the stack a : []. Note that if a contract
address containing an entrypoint address%entrypoint is provided, only
the address part will be taken.
Return the voting power of a given contract. This voting power
coincides with the weight of the contract in the voting listings (i.e., the
stake) which is calculated at the beginning of every voting period. For a detailed definition of voting power, see here.
Currently the voting power is proportional to the full staking balance of
the contract, but this might change in future version of the protocol and
developers should not rely on this. Hence, the value returned by
VOTING_POWER should only be considered relative to the one returned by
TOTAL_VOTING_POWER.
The instruction XOR is defined on boolean, natural number and bytes operands.
In the boolean case, the result is the logical XOR of the operands.
In the natural number and bytes cases, the result is the bitwise XOR of the operands.
When XOR 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.