The Book of Pint

Smart Contracts

Pint is a language for writing "smart contracts". If you're familiar with smart contract languages like Solidity, then many elements of a Pint contract should feel familiar. Of course, at its core, Pint is fundamentally different from imperative smart contract languages. Writing smart contracts in Pint requires a different way of thinking about how to express the rules that the smart contract must enforce.

A Pint contract is a collection of predicates. Each predicate has a name and contains a list of constraints. A contract may also contain a storage declaration which contain all the storage variable that the contract owns. Contract storage is effectively the database of the contract where persistent state lives. We will discuss storage in details in Chapter 5.

Contract Structure

The structure of a Pint smart contract is fairly simple. We simply lay out all the code blocks as follows:

storage {
    // storage variables
}

predicate Foo {
    // variables, constraints, etc.     
}

predicate Bar {
    // variables, constraints, etc.     
}

// other constraint sets

The order of the different blocks is not important, and the storage block is optional but most useful smart contracts will need it.

Unlike imperative smart contracts where the logic lives in contract methods that can be called to make state updates, Pint contracts have predicates (not methods/functions!) and nothing is ever "called". Instead, solutions have to submitted that satisfy one of the predicates in the contract. A solution must specify concrete values for all the decision variables in the predicate, as well as propose changes to the state. If the proposed state changes and the decision variables satisfy all the constraints in that particular predicate, then the solution is deemed valid and the proposed state changes are committed.

Contract Interfaces

Each smart contract has an interface which can be easily generated from the contract. The interface is not required to write the smart contract but is required to interact with the contract from external contexts. For example, one smart contract can propose an update to a storage variables that is owned by another contract. Will will go over how to do that in Chapter 5.

A contract interface has the following structure:

interface ExternalContract {
    storage {
        // storage variables
    }

    predicate Foo {
        // all **public** decision variables     
    }

    predicate Bar {
        // all **public** decision variables     
    }

    // other constraint sets
}

You can see the similarities between the structure of the interface and the structure of the smart contract. An interface starts with interface keyword followed by the name of the interface which can be used when referring the interface from external contexts. Inside the interface declaration, an optional storage block can be declared as well as a list of predicate interfaces. These predicate interfaces contain all the public decision variables that the predicates expose. We will discuss public decision variables in detail in Chapter 7.1, but for now, you can think of these variables as regular decision variable except that they can be read from an external context.

Let's revisit the counter example but with a small modification where we have made all decision variables pub, which marks them as public:

storage {
    counter: int,
}

predicate Initialize {
    pub var value: int;
    state counter: int = mut storage::counter;
    constraint counter' == value;
}

predicate Increment {
    pub var amount: int;
    state counter: int = mut storage::counter;
    constraint counter' == counter + amount;
}

An interface for the contract above looks like this:

interface Counter {
    storage {
        counter: int,
    }

    predicate Initialize {
        pub var value: int;
    }

    predicate Increment {
        pub var amount: int;
    }
}

Hopefully nothing here is surprising! The key point is that an interface must expose everything that is public in a contract, and that includes the storage block and all public decision variables in each predicate.

Note that, if a predicate Foo has no public decision variables, both predicate Foo { } and predicate Foo; can be used when adding it to the interface.

Note in the future, Pint will have a tool that will auto-generate interfaces.