Introducing SmartPy and SmartPy.io, an Intuitive and Effective Language and Development Platform for Tezos Smart Contracts

Overview

Smart contracts are scripts stored on a blockchain that enable users to define custom rules and protocols for various purposes. Some typical examples include escrow accounts, insurance-like contracts, decentralized applications — frequently called dApps, multi-signatures (multi-sig) contracts, security tokens, and virtual or physical tokenized assets.

  • Functional programming for clean and effective formal manipulations in OCaml as is already done in Michelson.
  • Static analysis and automatic proofs. The need for proofs is well understood in mission-critical industries and highly recognized in the Tezos community. A specific focus in the larger blockchain ecosystem is performed here with fully automatic proofs, especially through abstract interpretation.

Motivations

Smart contracts have a mixed history, simultaneously generating a huge interest from programmers and enthusiasts on one hand but also showing some limitations and shortcomings on the other: an inability to fully understand and analyze what will or may happen, unexpected bugs that yield to forks and disrupt network effects, obscure compilation phases to low level virtual machines, decompilation limitations, etc. These shortcomings limit the trust developers can have in smart contracts and ultimately the adoption of this technology by end-users.

  • A Python library, SmartPy, providing a very intuitive and effective syntax that programmers can fully understand and use to directly access SmartML definitions. Today, Python is one of, if not the most, popular languages to do meta-programming in numerical analysis and machine learning with the multitude of Python frameworks: NumPy, TensorFlow, PyTorch, Scikit-learn, etc. SmartPy functions in a similar fashion: a programmer has access to the full power of Python and describes computational models with a regular Python library. These models are then evaluated elsewhere: on Tezos with SmartPy, in the cloud, on other CPUs or GPUs, etc. for numerical analysis or machine learning.
  • A compiler to translate SmartML contracts to Michelson.
  • Analytics — Analytics are elements of the user interface that provide some automatic procedures in SmartPy.io to analyze and prove properties of smart contracts. They are not required to define smart contracts, but we believe that they are absolutely necessary for smart contracts to gain mainstream adoption by building trust among both developers and end-users.

Timeline

SmartPy.io is an in-browser editor based on SmartPy that brings simulation, debugging, tests, and analytics capabilities straight to developers. It is under active development and a first public version is expected to be released in summer 2019. Analytics are expected to be publicly available in a second version.

SmartPy.io

SmartPy.io is an in-browser development platform with advanced capabilities to develop, test, and prove properties of smart contracts.

Technical overview

The SmartPy definition library is a Python library that has a single purpose: offer a simple, intuitive, and powerful syntax to define Tezos smart contracts.

Overview of SmartPy.io: from SmartPy to Michelson, Tests, and Analytics

SmartPy

An example

We can start with an example: a very simple contract StoreValue that stores some value that we call storedValue and enable its users to either replace it by calling replace, double it by calling double or divide it by calling divide.

import smartpy as spclass StoreValue(sp.Contract):
def __init__(self, value):
self.init(storedValue = value)
@sp.entry_point
def replace(self, params):
self.data.storedValue = params.value
@sp.entry_point
def double(self, params):
self.data.storedValue = self.data.storedValue * 2
@sp.entry_point
def divide(self, params):
sp.verify(params.divisor != 0)
self.data.storedValue = self.data.storedValue / params.divisor

A few SmartPy constructions

Here are some typical constructions in SmartPy.

@sp.entry_point
def messageName(self, params):
...
a = 3 * b + 2 # operations and affectations
a <= b # comparisons
# Retrieving
a.b
a[element]
# Setting
data.attribute = value

Types

SmartML contracts are fully typed but initial SmartPy contracts need not be. The typing occurs in the OCaml world and type inference is used to determine the type of every element, parameters, and storage of a contract for every type including on records, constructors, arrays, etc.

[sp.TRecord(groups = [sp.TRecord(contractWeight = sp.TInt,
ok = sp.TBool,
participants = [Rec(hasVoted = sp.TBool,
id = sp.address,
weight = sp.TInt)],
thresholdVoters = sp.TInt,
thresholdWeight = sp.TInt,
voters = sp.TInt,
weight = sp.TInt)],
groupsOK = sp.TInt,
name = sp.TString,
ok = sp.TBool,
thresholdGroupsOK = sp.TInt,
thresholdWeight = sp.TInt,
weight = sp.TInt)]
[...]                     # list/array
sp.TRecord(...) # record type
sp.TInt, sp.TBool, sp.TAddress, sp.TString # basic types
# for list
sp.list([v1, v2 , v3], t = ...)
# for any expression
sp.set_type(group.weight, sp.TInt)

Evaluation of SmartPy

The evaluation of these constructions is not completely standard: SmartPy creates a SmartML value which represents some computation that will execute in a simulation or on Tezos at a later stage.

An elementary example

The following elementary example represents part of a contract from the game, Nim.

    def remove(self, params):
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell < self.data.size)
sp.verify(1 <= k)
sp.verify(k <= self.data.deck[cell])
self.data.deck[cell] = self.data.deck[cell] - k
self.data.nextPlayer = 3 - self.data.nextPlayer

A little further with meta-programming

We can add the following code to the previous example to see the two stages of programming at play:

        if self.bound is not None:
sp.verify(k <= self.bound)

A complete example

Here is a more complete Nim game example.

import smartpy as spclass NimGame(sp.Contract):
def __init__(self, size, bound = None, winnerIsLast = False):
self.bound = bound
self.winnerIsLast = winnerIsLast
self.init(deck = sp.range(1, size + 1),
size = size,
nextPlayer = 1,
claimed = False,
winner = 0)
@sp.entry_point
def remove(self, params):
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell < self.data.size)
sp.verify(1 <= k)
if self.bound is not None:
sp.verify(k <= self.bound)
sp.verify(k <= self.data.deck[cell])
self.data.deck[cell] = self.data.deck[cell] - k
self.data.nextPlayer = 3 - self.data.nextPlayer
@sp.entry_point
def claim(self, params):
sp.verify(sp.sum(self.data.deck) == 0)
self.data.claimed = True
if self.winnerIsLast:
self.data.winner = 3 - self.data.nextPlayer
else:
self.data.winner = self.data.nextPlayer

Tests

To interact with and test this contract, we can write a test. Here we simply create an html document that is directly visible in SmartPy.io. This can be done in the same editor where we defined the contract. It is also regular Python code.

@addTest(name = "Test Store Value")
def test():
c1 = StoreValue(12)
html = c1.fullHtml()
html += c1.execMessage('replace', value = 15).html()
html += c1.execMessage('replace', value = 25).html()
html += c1.execMessage('double').html()
html += c1.execMessage('divide', divisor = 2).html()
html += c1.execMessage('divide', divisor = 0).html()
html += c1.execMessage('divide', divisor = 3).html()
setOutput(html)
@addTest(name = "Test Nim Game")
def test():
# Define of a contract
c1 = NimGame(size = 5, bound = 2)
# Show its representation
html = h2("Contract")
html += c1.fullHtml()
# Interact with the contract
html += h2("Message execution")
html += h3("A first move")
result = c1.execMessage("remove", cell = 2, k = 1)
# and update the html document we're creating
html += result.html()
html += h3("A second move")
result = c1.execMessage("remove", cell = 2, k = 2).html()
html += h3("An illegal move")
result = c1.execMessage("remove", cell = 2, k = 1).html()
html += h3("Another illegal move")
result = c1.execMessage("claim").html()
html += h3("A third move")
result = c1.execMessage("remove", cell = 1, k = 2).html()
html += h3("More moves")
html += c1.execMessage("remove", cell = 0, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 1).html()
html += c1.execMessage("remove", cell = 3, k = 2).html()
html += c1.execMessage("remove", cell = 4, k = 1).html()
html += c1.execMessage("remove", cell = 4, k = 2).html()
html += h3("A failed attempt to claim")
html += c1.execMessage("claim").html()
html += h3("A last removal")
html += c1.execMessage("remove", cell = 4, k = 2).html()
html += h3("And a final claim")
html += c1.execMessage("claim").html()
setOutput(html)
c1.execMessage("remove", cell = 4, k = 1).html()
Executing: remove by [] at time [0].
Params:
cell = 0
k = 1
Balance:0
Result: OK
Effects:
Data:
Claimed Deck NextPlayer Size Winner
False [0, 0, 0, 4, 5] 1 5 0

Taking this example further

The NimGame example can be taken further in several directions:

sp.verify(data.id == sp.sender)
    @sp.entry_point
def remove(self, params):
gameId = params.gameId
game = self.data.games[gameId]
cell = params.cell
k = params.k
sp.verify(0 <= cell)
sp.verify(cell < game.size)
sp.verify(1 <= k)
sp.verify(k <= game.bound)
sp.verify(k <= game.deck[cell])
game.deck[cell] = game.deck[cell] - k
game.nextPlayer = 3 - game.nextPlayer
@sp.entry_point
def claim(self, params):
gameId = params.gameId
game = self.data.games[gameId]
sp.verify(sp.sum(game.deck) == 0)
game.claimed = True
sp.if game.lastWins:
game.winner = 3 - game.nextPlayer
sp.else:
game.winner = game.nextPlayer
with sp.if_(...):
...

Translating SmartPy to SmartML

The Python interpreter evaluates Python code containing SmartPy definitions. It creates a very simple expression, called a S-expression, that is parsed and typed while some properties are verified in the SmartEngine backend.

(storage (record (claimed (bool False)) (deck (array "int" (int 1) (int 2) (int 3) (int 4) (int 5))) (nextPlayer (int 1)) (size (int 5)) (winner (int 0))) messages ((claim ((check (eq (sum (attrData "deck")) (int 0))) (set (attrData "claimed") (bool True)) (set (attrData "winner") (attrData "nextPlayer")))) (remove ((define "cell" (unknown 1)) (define "k" (unknown 2)) (check (ge (getParam cell (unknown 1)) (int 0))) (check (lt (getParam cell (unknown 1)) (attrData "size"))) (check (ge (getParam k (unknown 2)) (int 1))) (check (le (getParam k (unknown 2)) (int 2))) (check (le (getParam k (unknown 2)) (getItem (attrData "deck") (getParam cell (unknown 1))))) (set (getItem (attrData "deck") (getParam cell (unknown 1))) (sub (getItem (attrData "deck") (getParam cell (unknown 1))) (getParam k (unknown 2)))) (set (attrData "nextPlayer") (sub (int 3) (attrData "nextPlayer")))))))

Viewing SmartML

Smart contracts in SmartML are abstract syntax trees as typically done in OCaml with values, expressions, commands, etc. Users of SmartPy.io can view such contracts with a simple trick: they are pretty-printed in SmartPy. This is quite efficient and gives great confidence in the meta-programming ability of SmartPy: you see what you get in a simple and understandable form.

@sp.entry_point
def claim(self, params):
sp.verify(sum(self.data.deck) == 0)
self.data.claimed = True
self.data.winner = self.data.nextPlayer
@sp.entry_point
def remove(self, params):
cell = params.cell
k = params.k
sp.verify(cell >= 0)
sp.verify(cell < self.data.size)
sp.verify(k >= 1)
sp.verify(k <= 2)
sp.verify(k <= self.data.deck[cell])
self.data.deck[cell] = self.data.deck[cell] - k
self.data.nextPlayer = 3 - self.data.nextPlayer

Analytics

Several analytics are necessary to help understand and prove Tezos smart contracts. We can view them as shedding light on several orthogonal dimensions of smart contracts.

  • Effects: determination of possible effects such as Payments.
  • Ownership: determination of who can change data in storage. A typical output of this analysis will be to determine a signature or a set of signatures that can change some storage. It would prevent bugs like the so-called MultiSig Parity Bug by construction and will be available for all smart contracts and not only the most important ones where an ad-hoc proof can be developed.
  • Workflow: graph of possible executions. This analysis is concerned with the sequencing of messages: ordering of messages, multiple calls, etc. It works by building a finite automaton approximation of the contract. Having the intended workflow for a contract helps prevent reentrancy or similar attacks.
  • Contract simplification: reduction of gas costs and complexity of contracts and storage.
  • Token conservation: verification of token attribution in a contract so that users know that their tokens cannot be misappropriated by others in contracts. The alternative could be to compute this property at runtime but it would cost gas and it would require a proof as well.
  • Time analysis. There are several notions of time in a blockchain. There is the real time used by every human activity with dates, hours, minutes, seconds, time zones, etc. And then there is “blockchain time” with the block time resulting from the sequence of blocks. Whatever time is used, it is important to check that a message to a contract can be made ‘on time’ and that a future event doesn’t happen either too early or too late in the future. This analysis studies contract execution timing.

Discussion about analytics vs ad-hoc proofs

Automatic analyses as presented in analytics and ad-hoc proofs of a given contract, in e.g. Coq, serve the common purpose to understand what a contract does with the ultimate goal to avoid costly mistakes or bugs.

  • Building an ad-hoc proof for a given contract in Coq is probably doable for every natural question we try to answer on every reasonable contract, but it’s probably quite costly and cannot be reasonably expected outside of a select small list of very important contracts.
  • Some analytics can present a result and may even be able to produce the ad-hoc proof in, e.g., Coq or part of it. We strongly think that this is a very nice research project.
  • These two approaches are non-exclusive in the sense that we can pragmatically start with an automatic analysis and see what it can or cannot do and continue from there to build an ad-hoc proof if deemed necessary.
  • The way analytics are designed in SmartPy.io is really to focus on different dimensions (values, effects, ownership, workflow, etc.). Depending on the contracts, these questions will be useful or not. If a question appears repeatedly and is not answered by one of these analytics, it will probably be reasonable to add a new analysis to study it.

Next steps and tasks

Here are a few items on the roadmap.

  • Editor improvements
  • Full determination of the list of constructions in SmartPy and implementation of all constructions of Michelson
  • Implementation and tests of the compiler to Michelson
  • Documentation and implementation of several example contracts
  • First public version of SmartPy.io
  • Implementation of the analytics framework
  • Open source all software
  • Miscellaneous improvements of SmartPy.io
  • Study and proof or verification of the compiler to Michelson
  • Optimization of compiler to Michelson possibly through Michelson to Michelson optimizations
  • Use of SmartPy / SmartML to research potential improvements to Michelson

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
SmartPy.io

SmartPy.io

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