Basic Computations in SmartPy, Python and Michelson

SmartPy is a Python library, accessible in an online editor SmartPy.io, that comes together with its SmartML backend. It enables developers to define and analyse smart contracts. These smart contracts are compiled into Michelson, the Tezos virtual machine.

Meta-programming in SmartPy means that, in SmartPy, we not only manipulate integers and other basic types, but also, and as smoothly as possible, computations.

Another feature of SmartPy is its ability to be executed or simulated.

We have a powerful ecosystem with several execution possibilities:
Python — SmartPy/SmartML — Michelson.

For everyones sanity, we must ensure that they behave properly and soundly.

Some basic requirements

  • Regular Python, including possibly within a SmartPy script: x represents an integer x, e.g., 3. and we compute x + 2.
  • SmartPy expression: x is an expression that represents some computation on the blockchain that will later compute an integer on the bakers’ nodes.

In the first case, x + 2 is really equivalent to 5 when x is 3. In the second case, x is not an integer, it really represents some computation that will happen on-chain.

There is some ambiguity between the two and this renders the SmartPy experience really smooth and somewhat magical. This ambiguity is only acceptable if the correspondance between these two worlds is precise: when evaluating the SmartPy expression in a context where x evaluates to 3, it must evaluate to 5. Similarly, when compiled to Michelson and then executed, it must evaluate to 5.

Integers and Naturals

In Michelson, int and nat are used almost interchangeably except that nat are always non negative. These types are unbounded.

In SmartPy/SmartML, we have only one kind of values int, which are also signed and unbounded but three possible types: int, nat, and intOrNat. When writing an integer 12, we don’t know whether it is an int or a nat so we type it as intOrNat. Its exact type will be determined at a later stage. This determination is necessary for the Michelson compiler because Michelson needs to make this precise determination but is usually not important in SmartPy.

Examples of int are -10, 0, 250, 123456789023456789012345678 and examples of nat or intOrNat are 0, 250, 123456789023456789012345678.

The Case of Addition, Multiplication and Subtraction

In SmartPy, we currently use the additional constraint that a and b are required to be of the same type. This is useful for type inference.

In Michelson and SmartPy, a-b is of type int when a and b are both of type int or nat.

How Many Divisions ?

That being said, SmartPy made the following choice:

  • We use Python3’s floordiv denoted a // b to denote division between nat (and only nat). Thankfully, Python 3 and Michelson agree on this domain.
  • Python3 has another division, called truediv, which yields a float and denoted a / b and is useless for us.
  • SmartPy gives also direct access to Michelson division: sp.ediv(a, b) of type option(t * nat). The t being equal to nat if both a and b are of type nat and int otherwise. In SmartPy, we further require that a and b are of the same type.

Booleans

Please note that ~ has the property to be used customarily for this purpose and is seldom used in Python. A drawback is that it doesn’t preserve the property that ~ True == False (it is an integer). This is not deemed important since we don’t expect SmartPy developers to use it in another context.

A subtle point about laziness. In regular Python, binary boolean operators are expected to be lazy, i.e., a and b only evaluates b if a is True. This is not the case for regular | and & but we wish to treat them in the same lazy way: a & b in SmartPy is compiled in Michelson into a lazy code that first evaluates a and then b only if a is True. For these reasons, the compilation of a & b in Michelson doesn’t use the AND operator but the following strategy:

<eval a>
IF
{ <eval b> }
{ PUSH bool False }

Control Operators

They can be used in SmartPy.io with some syntactic sugar: sp.if, sp.for and sp.while. There are also pure Python versions that are used in the following, slightly less intuitive, way:

if:

sp.if condition:
...
with sp.ifBlock(condition):
...

for:

sp.for x in expression:
...
with sp.forBlock('var', expression) as var:
...

and while:

sp.while condition:
...
with sp.whileBlock(condition):
...

How do we ensure that this is correct?

The precise implementation need not be fully understood but the idea might be interesting for some readers: we define a contract that takes some parameters and calls a Python function f. This function can be evaluated in pure Python or through SmartPy/SmartML.

Here is the skeleton of the solution.

import smartpy as spclass CheckOperator(sp.Contract):
def __init__(self, default, f, *args):
self.f = f
self.length = len(args)
self.init(result = default)
@sp.entryPoint
def run(self, params):
args = [getattr(params, "x_%i" % i) for i in range(0, self.length)]
self.data.result = self.f(*args)

It can be demonstrated on SmartPy.io by using the template called ‘Check Language Constructions’ or by clicking here.

An intuitive and effective smart contracts language and development platform for Tezos. In Python.