Introducing Test Scenarios in SmartPy.io

Proving properties of smart contracts is of paramount importance and one of Tezos’ moto is about formally verifying its infrastructure and smart contracts.

We claim that formal verification is not the only tool to understand a smart contract and before formally proving properties, one should first perform unit-tests or scenario tests. It has a few very useful consequences: we may discover bugs, we may discover properties that we want to formally prove and, finally, it may also be the case that, for a given smart contract, we only need a few tests to be convinced of what it’s doing and do not need the full formal verification machinery.

From day one, SmartPy.io has used test scenarios for this very purpose.

This small document explains a new version of these test scenarios that brings new nice capabilities.

An example

We start by an example.

Here is a very simple example of a smart contract doing something pretty useless: it stores two values and provides an entry point that can change its first value (called myParameter1) as long as it is bounded by 123.

import smartpy as sp
# A class of contracts
class MyContract(sp.Contract):
    def __init__(self, myParameter1, myParameter2):
        self.init(myParameter1 = myParameter1,
                  myParameter2 = myParameter2)
    # An entry point, i.e., a message receiver
    # (contracts react to messages)
    @sp.entryPoint
    def myEntryPoint(self, params):
        sp.verify(self.data.myParameter1 <= 123)
        self.data.myParameter1 += params

This can be tested by defining the following test and scenario in the same script.

@addTest(name = "First test")
def test():
    # We define a test scenario, called scenario,
    # together with some outputs and checks
    scenario = sp.testScenario()
    # We first define a contract and add it to the scenario
    c1 = MyContract(12, 123)
    scenario += c1
    # And send messages to some entry points of c1
    scenario += c1.myEntryPoint(12)
    scenario += c1.myEntryPoint(13)
    scenario += c1.myEntryPoint(14)
    scenario += c1.myEntryPoint(50)
    scenario += c1.myEntryPoint(50)
    scenario += c1.myEntryPoint(50) ### This will be refused
    # Finally, we check the final storage of c1
    scenario.verify(c1.data.myParameter1 == 151)

This definition can be evaluated in-browser in SmartPy.io or out-of-browser with SmartPyBasic and both compute the scenario.

In SmartPy.io, the scenario is computed and then displayed as an html document.
With SmartPyBasic, this is first computed as a .json scenario file that is then evaluated.

Scenarios

As seen in the previous example, a scenario in a test is introduced by sp.testScenario(). We interact with it by using several constructions.

• Registering and displaying contracts.

scenario += c1
# This is identical to doing
scenario.register(c1, show = True)
# To only register the smart contract but not show it
scenario.register(c1)

• Registering and displaying calls to entry points.

scenario += c1.myEntryPoint(12)
scenario += c1.myEntryPoint(...).run(sender = ..., amount = ..., now = ...)
# To only execute a call to an entry point but not show it
scenario.register(c1.myEntryPoint(12))

• Adding document informations

scenario.h1("a title")
scenario.h2("a subtitle")
scenario.h3(..)
scenario.h4(..)
scenario.p("Some text")

• Computing expressions.

scenario.compute(c1.data.myParameter1 * 12)
scenario.compute(c1.data)

• Checking assertions.

scenario.verify(self.data.myParameter == 51)