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 everyone’s sanity, we must ensure that they behave properly and soundly.
Some basic requirements
In a SmartPy script, writing x + 2 can mean two related but somewhat different things:
- Regular Python, including possibly within a SmartPy script:
xrepresents an integer x, e.g., 3. and we compute x + 2. - SmartPy expression:
xis 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 Python, there is only one type int to represent integers. It is an unbounded domain of signed integers.
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 Michelson a+b or a*b when a and b are of type int or nat are of type int unless both are of type nat and, in this case, a+b and a*b is of type nat.
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 ?
Division is a totally different subject: Python has two different divisions; Michelson has one unique division operation which happens to be euclidian division. Also, there is a disagreement about how division handles negative numbers between all Python implementations and Michelson.
That being said, SmartPy made the following choice:
- We use Python3’s
floordivdenoteda // bto denote division betweennat(and onlynat). Thankfully, Python 3 and Michelson agree on this domain. - Python3 has another division, called
truediv, which yields a float and denoteda / band is useless for us. - SmartPy gives also direct access to Michelson division:
sp.ediv(a, b)of typeoption(t * nat). Thetbeing equal tonatif bothaandbare of typenatandintotherwise. In SmartPy, we further require thataandbare of the same type.
Booleans
As is customary and practical in Python extensions, boolean operations in SmartPy are denoted by & instead of and, | instead of or and ~ instead of not.
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
Control operators in SmartPy look like if, for and while.
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?
We can actually build many contracts and test their behaviors, at least currently to check Python vs SmartPy/SmartML.
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.
