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 purpose of the language and where it fits in the blockchain, see the Michelson reference 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 or a delegation.
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)
Comparable values can be stored in sets, can be passed as argument to COMPARE, etc.
Passable (PM)
Passable types are those that can be taken 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 given as parameter to the PUSH primitive.
Packable (PA)
Values of packable types can be given as serialized using the PACK primitive.
big_map value (B)
These are types that be used in the domain of big_maps.
Duplicable (D)
Literal values of duplicable types can be given as parameter to 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. ¶
All pushable types are also packable and vice versa. Except for the domain
specific types operation, contract,
ticket, sapling_state and big_map, all
types are passable, storable, pushable, packable and can be used as values in
big_maps. The only type that is not duplicable is ticket.
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 tezos-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}}.
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 (both \n and \r)
cannot appear in a string. What can be done with strings is basically use
string constants as is, concatenate or splice them, and use them as keys.
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 and natural number operands.
In the former case, the result is the logical AND of the operands.
In the latter case, 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.
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.
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. 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:
+---------------+---------------------+------------------------------------------+
| input address | instruction | output contract |
+---------------+---------------------+------------------------------------------+
| "addr" | CONTRACT t | (Some "addr") if contract exists, has a |
| | | default entrypoint of type t, or has no |
| | | default entrypoint and parameter type t |
+---------------+---------------------+------------------------------------------+
| "addr%name" | CONTRACT t | (Some "addr%name") if addr exists and |
+---------------+---------------------+ has an entrypoint %name of type t |
| "addr" | CONTRACT %name t | |
+---------------+---------------------+------------------------------------------+
| "addr%_" | CONTRACT %_ t | None |
+---------------+---------------------+------------------------------------------+
Note that CONTRACT ty is strictly equivalent to CONTRACT
%default ty, and for clarity, the second variant is forbidden
in the concrete syntax.
Typing
Γ ⊢ CONTRACTty :: address : A ⇒ option ( contractty ) : A
CONTRACT
Semantics
get_contract_typeaddrty
CONTRACTty / addr : S ⇒ Some ( contracttyaddr ) : S
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
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 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.
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 or a BLS12-381 field element 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).
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.
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.
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.
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.
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.
The NOT instruction is defined for bool,
nat and int.
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.
Push the minimal injection time for the current block,
namely the block whose validation triggered this execution. On
mainnet, the minimal injection time is 15 seconds after the timestamp of the
predecessor block. This value does not change during the execution
of the contract.
The instruction OR is defined on boolean and natural number operands.
In the former case, the result is the logical OR of the operands.
In the latter case, the result is the bitwise OR of the operands.
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
SAPLING_VERIFY_UPDATE takes a sapling transaction and a sapling state and returns an
option type that is Some (updated
state and a balance) if the transaction is correct, None otherwise.
A transaction has a list of inputs, outputs, a signature, a balance,
and the root of the Merkle tree containing its inputs.
The verification part checks the zero-knowledge proofs of all inputs
and outputs of the transaction, which guarantees several correctness properties.
It also checks a (randomised) signature associated with each input
(which guarantees that the owner forged the transaction), and the
signature that binds the whole transaction together and guarantees the
correctness of the balance.
All the signatures are over the hash of the data that we wish to sign
and the hash function used is BLAKE2B, prefixed with the anti-replay string.
The anti-replay string is the concatenation of the chain identifier and
the smart contract address. The same string has to be used by the client for
signing.
SAPLING_VERIFY_UPDATE also checks that the root of the Merkle tree appears in
one of the past states and that the nullifiers are not already
present (i.e. no double spending is happening).
If one of the checks fails the instruction returns None.
Otherwise the instruction adds the nullifiers given with each inputs to the new state
and adds the outputs to the Merkle tree, which will produce a new root.
It should be noted that it is possible to generate transactions
referring to an old root, as long as the inputs used were present in
the Merkle tree with that root and were not spent after.
In particular the protocol keeps 120 previous roots and guarantees
that roots are updated at most once per block.
Considering that one block is added to the chain every minute and that each block contains at least
one call to the same contract, a client has 2 hours to have its
transaction accepted before it is considered invalid.
The nullifiers are stored in a set. The ciphertexts and other relevant
information linked to the commitment of the Merkle tree are
stored in a map indexed by the position of the commitment in the
Merkle tree.
Lastly the instruction pushes the updated state and balance as an option
on the stack.
Please see the Sapling integration
page for a more comprehensive description of the Sapling protocol.
Typing
Γ ⊢ SAPLING_VERIFY_UPDATE :: sapling_transactionms : sapling_statems : A ⇒ option ( pairint ( sapling_statems ) ) : A
SAPLING_VERIFY_UPDATE
Semantics
sapling_verify_update ( t , s , b , s′ ) = True
SAPLING_VERIFY_UPDATE / t : s : S ⇒ Some ( Pairbs′ ) : S
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) |
+----------------------+------------------------------------------+
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.