The Book of Pint

Welcome to The Book of Pint, an introductory book about Pint. Pint is a declarative programming language for building blockchain applications. The term declarative means that code written in Pint is focused on logic and not execution. In Pint, you can describe what your program must accomplish rather than describing how to accomplish it. This is in contrast with imperative blockchain languages, like Solidity, which require implementing algorithms in explicit steps.

In particular, Pint is a constraint-based language. A Pint program is essentially a collection of predicates and each predicate is a collection of constraints. Because blockchain applications are all about state transitions, constraints allow you to restrict how the state is allowed to change. As a result, you do not have to explicitly express how to change the state, but only what state changes are allowed.

In general, this book assumes that you’re reading it in sequence from front to back. Later chapters build on concepts in earlier chapters, and earlier chapters might not delve into details on a particular topic but will revisit the topic in a later chapter. The book can also be used as a reference, though it is not entirely comprehensive.

Getting Started

To get you started, this chapter discusses the following:

• Installing Pint
• Writing your first Pint programs

Installation

Using Nix (Recommended)

The easiest way to get started with Pint and the Essential ecosystem is to use Nix. You first need to install Nix using:

curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install

or using one of these other alternatives.

Then, enter a Nix shell as follows:

nix develop github:essential-contributions/essential-integration#dev

This will make all the tools you need available in your terminal.

Installing from Cargo

Dependencies

A prerequisite for installing Pint from Cargo is the Rust toolchain. Platform-specific instructions for installing rustup can be found here. Then, install the Rust toolchain with:

$ rustup install stable

The Pint toolchain is built and tested against the latest stable Rust toolchain version. Ensure you are using the latest stable version of Rust with:

$ rustup update && rustup default stable

Installation Steps

The Pint toolchain can be installed using Cargo with:

$ cargo install pint-cli

You can update the toolchain with Cargo using:

$ cargo update pint-cli

Syntax Highlighting

Currently, Pint only has syntax highlighting support in Visual Studio Code. We are, however, in the process of adding support for other editors.

Visual Studio Code

To install the Pint plugin, Search the Visual Studio Code market place for pint syntax. Alternatively, use this link.

Quickstart Guide

Now that you’ve installed Pint, it’s time to write your first Pint contract. The first contract we will implement is a counter.

Creating a Project Directory

You'll start by making a directory to store your Pint code. Open a terminal and enter the following commands to make a projects directory:

mkdir ~/projects
cd ~/projects

Now, we will use the pint tool to create a new project in the projects directory:

pint new counter
cd counter

The pint new commands creates a new Pint project with the provided name. In the newly created directory counter, you should find a pint.toml file as well as a src/ directory with a single file in it called contract.pnt:

projects
└── counter
    ├── pint.toml
    └── src
        └── contract.pnt

The auto-generated pint.toml file describes how to build the project. The src/contract.pnt file is the root file of a contract project, i.e., this is where the compilation starts when we build the project.

Open the pint.toml and inspect its content:

[package]
name = "counter"
kind = "contract"

[dependencies]
# Library dependencies go here.

[contract-dependencies]
# Contract dependencies go here.

The one thing to note is that the kind field in this pint.toml is set to contract. This is the default project kind. Alternatively, kind can be a library.

Writing a Pint Program

Next, open the src/contract.pnt file and erase its content. Then, paste the following:

storage {
    counter: int,
}

predicate Increment {
    state counter: int = mut storage::counter;

    constraint (counter == nil && counter' == 1) || counter' == counter + 1;
}

This is a contract with a single predicate and a single storage variable. The storage variable counter, of type int (i.e. integer), is declared in a storage block. The only predicate in this contract is called Increment and contains two statements:

1. A state declaration which reads the variable counter.
2. A constraint statement which enforces some logic on the state of the contract.

The above constraint is essentially saying: "if counter hasn't been set yet (i.e. is nil), set the new value of counter to 1 (counter' == 1). Otherwise, increment counter by 1".

Don't worry if this looks a bit overwhelming! We will later dive into each feature in this contract separately.

Building the Project

To build the project above, simply run the following command in the counter directory:

pint build

You should get something like this:

   Compiling counter [contract] (/path/to/counter)
    Finished build [debug] in 4.157208ms
    contract counter            C276E4E5EAF789F82B671E53F0B202AE357C511F2B711E4921310946ACE63B7C
         └── counter::Increment 3D7ABBA5C62DF177EFD61CA9D74ED055B29267404112583FA2E4C0D98B828149

Note the two 256-bit numbers in the output. These represent the content hash (i.e. the sha256 of the bytecode) of the counter contract (as a whole) and the Increment predicate, respectively. These "addresses" will be used when referring to the contract or the predicate (in a proposed solution for example).

In the counter directory, you will also notice a new directory called out. Navigate to out/debug and inspect the two json files that you see.

• counter.json represents the compiled bytecode in JSON format, which is the most important artifact produced by the compiler. This file is used when validating a solution. That is, when a solution is submitted, this file contains the bytecode that "runs" and decides whether all the relevant constraints are valid.
• counter-abi.json is the Application Binary Interface (ABI) of the contract. It basically describes how to interact with the contract from an external application or another contract. For example, while crafting a solution, the ABI can be used to figure out where the various storage variables are stored (i.e. their keys) and their types. This information is crucial to form correct solutions.

Note: Appendix C contains the ABI spec.

Now that we have built and inspected the artifacts of our project, we can proceed to build an application that interacts with this contract. We won't cover this topic here, but you can check out this Getting Started with Essential Application book, which covers this exact same "counter" example and how to build a Rust application that interacts with it using the Essential VM.

Example

This chapter includes some basic examples that show how Pint code looks like:

• Counter
• Subcurrency

We will go over each example line-by-line while briefly introducing new concepts. Later, however, we will cover each new concept in depth in its own chapter. Therefore, the goal of this chapter is not to teach you everything about Pint but to get you to (hopefully!) appreciate what Pint is capable off.

Counter

The "counter" is one of the simplest smart contracts that can be written in Pint. It showcases how a contract can have multiple predicates and how it can declare and use storage. This particular implementation of the "counter" contract is different from the one we encountered in the Quickstart Guide

storage {
    counter: int,
}

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

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

The contract starts by declaring a storage block which contains a single storage variable called counter of type int (i.e. integer). The contract later declares two separate predicates, each declaring three statements. Let's walk through the first predicate named Initialize:

1. The first statement declares a decision variable. Decision variables are quite different from "regular" variables which you might be familiar with from imperative languages. Decision variables are variables that the solver is required to find values for. You can think of them as "arguments" that the solver has to set such that every constraint in the predicate evaluates to true. In Initialize, we are declaring a single decision variable called value of type int. This is the value that we want our counter to get initialized to.
2. The second statement declares a state variable and initializes it to mut storage::counter. State variables are special variables that always need to be initialized to a storage access expression. The statement state counter: int = mut storage::counter creates a state variable called counter and initializes it to the current value of counter declared in the storage block. The mut keyword simply indicates that the solver is allowed to propose a new value for counter. If mut is not present, then the storage variable counter cannot be modified by anyone attempting to solve predicate Initialize.
3. The third statement contains the core logic of this predicate. It declares that the "next value" of state counter must be equal to value. Note the ' notation here which can be only applied to a state variable, and means "the next value of the state variable after a valid state transition".

The second predicate, called Increment, has a similar structure to Initialize. However, instead of initializing counter, It increments it by amount. Note that both counter (the current value) and counter' (the next value) are both used in the constraint to enforce that the next value is dependent on the current value, which was not the case in Initialize.

Solution

We won't go too deep into the solving process here but it's worth mentioning what a solution to this predicate might look like. Broadly speaking, a solution contains two things:

1. An assignment of all the decision variables in the predicate.
2. A list of all the state mutations proposed.

For example, if a user wants the value of the counter to be 42 they (or a solver acting on their behalf) can propose a solution to Initialize that looks like this:

# decision variables:
value: 42

# state mutations:
0: 42

This solution proposes a value of 42 for the decision variable value and a new value of 42 for the storage key 0 where counter is stored (we will go over the storage data layout later!). Note that the storage key 0 where counter is stored can be modified by the solution because of the mut keyword added before storage::counter.

A solution must also indicate which predicate is being solved using its address but we're omitting that here for simplicity.

Alternatively, a solution to Increment can be proposed to satisfy the user requirement counter = 42. For example, if the current value of counter happens to be 35, then the following solution to Increment can be proposed:

# decision variables:
amount: 7

# state mutations:
0: 42

It should be easy to verify that this solution satisfies the constraint counter' == counter + amount; from Increment.

Subcurrency

The following contract implements the simplest form of a cryptocurrency. The contract allows the creation of new coins (i.e. minting) as well as sending coins from one address to another.

storage {
    total_supply: int,
    balances: (b256 => int),
}

// Sends an amount of newly created coins to an address
predicate Mint {
    var receiver: b256;
    var amount: int;

    state receiver_balance = mut storage::balances[receiver];
    state total_supply = mut storage::total_supply;

    constraint total_supply' == total_supply + amount;
    constraint receiver_balance' == receiver_balance + amount;
}

// Sends an amount of existing coins from address `from` to address `receiver`
predicate Send {
    var from: b256;
    var receiver: b256;
    var amount: int;

    state from_balance = mut storage::balances[from];
    state receiver_balance = mut storage::balances[receiver];

    constraint amount < from_balance;
    constraint from_balance' == from_balance - amount;
    constraint receiver_balance' == receiver_balance + amount;
}

This contract introduces some new concepts. Let's walk through it line by line.

The contract starts with a storage declaration that contains two storage variables:

1. total_supply is of type int and represents the total supply of coins available at any given point in time.
2. balances is a map from b256 to int and stores balances of addresses as integers. b256 is a primitive type that represents a 256-bit hash value and is used here to represent an address.

The contract also declares two predicates: Mint and Send.

The Mint predicate is fairly simple:

1. It declares two decision variables receiver: b256 and amount: int. The goal of this predicate to mint amount coins and send them to receiver.
2. It initializes a state variable called receiver_balance using the storage access expression mut storage::balances[receiver]. This syntax returns the value in balances that receiver maps to and makes it "mutable". The predicate also initializes another state variable called total_supply to mut storage::total_supply.
3. It enforces two constraints:
   1. the first constraint requires the total supply to be incremented by amount.
   2. The second constraint requires the balance of receiver to be incremented by amount.

The Send predicate has the following structure:

1. It declares three decision variables from: b256, receiver: b256, and amount: int. The goal of this predicate to send amount coins from address from to address receiver.
2. It initializes a state variable called from_balance to the balance of from and another variable called receiver_balance to the balance of receiver. It also makes both balances "mutable".
3. It enforces three constraints
   1. the first constraint requires from_balance to be larger than amount. That is, the address from must currently actually have enough coins to send to receiver.
   2. The second constraint effectively decrements the balance of from by amount, by requiring the next state of from_balance to be from_balance - amount.
   3. The third constraint effectively increments the balance of receiver by amount, by requiring the next state of receiver_balance to be receiver_balance + amount.

Note to make things simpler and easier to understand, this contract has no authentication anywhere in its code. That is, anyone can mint new coins and initiate a transfer from one arbitrary address to another. This, of course, is not the desired behavior for most cryptocurrencies. That being said, we will cover authentication in a later chapter and discuss how to use authentication make this contract more secure.

Common Programming Concepts

This chapter covers concepts that appear in almost every programming language and how they work in Pint. Many programming languages have much in common at their core. None of the concepts presented in this chapter are unique to Pint, but we’ll discuss them in the context of Pint and particularly how they work in a constraint-based environment as opposed to imperative environments that you might be more familiar with.

Specifically, you’ll learn about decision variables, basic types, custom types, comments, and conditionals. These foundations will be in every Pint program, and learning them early will give you a strong core to start from.

Keywords: The Pint language has a set of keywords that are reserved for use by the language only, much as in other languages. Keep in mind that you cannot use these words as names of variables, predicates, types, or macros. Most of the keywords have special meanings, and you’ll be using them to do various tasks in your Pint programs; You can find a list of the keywords in Appendix A.

Decision Variables

A decision variable is a named variable that every solution is required to assign a value for. Decision variables are quite different from "regular" variables that you might be used to in imperative programming languages. Decision variables do not get "computed" or "assigned to" in a Pint program since a Pint program is not actually executed but solved (and later validated against a solution).

Decision variables can be declared using the var keyword and may be annotated with a type. We will go over the available data types in Pint, in detail, in a later chapter.

Here's an example that shows how to declared a decision variable named foo of type int:

var foo: int;

You can actually think of the type annotation as a "constraint" on the decision variable: this decision variable can only take values in the set of signed integers (64-bit signed integers when targeting the EssentialVM). Any solution that proposes a value of foo must satisfy that constraint. We will go over constraints in more detail in Chapter 3.6.

A decision variable can also be "initialized". Initializing a decision variable may seem like an odd concept because decision variables are declared to be solved for. However, an initialized decision variable is simply a decision variable with an extra implicit constraint. Here's how an initialized decision variable can be declared:

var bar: int = 42;

The above is equivalent to:

var bar: int;
constraint bar == 42;

We will go over constraint statements in more details later but it should hopefully be intuitive that this statement enforces bar to be equal to 42. Therefore, every proposed solution must also set bar to 42. Otherwise, this particular constraint will fail and the whole solution will be deemed invalid.

Skipping the type annotation is only allowed if the decision variable is "initialized":

var baz = 43;

In this case, the compiler is able to infer the type of baz by realizing that the initializer 42 is of type int.

Again, the above is equivalent to:

var baz: int;
constraint baz == 43;

Data Types

Every value in Pint is of a certain data type, which tells Pint and solvers what kind of data is being specified so they know how to work with that data. We'll look at two data type subsets: scalar and compound.

Keep in mind that Pint is a statically typed language, which means that it must know the types of all variables at compile time. The compiler can often infer what type we want to use based on the value and how we use it. In cases where many types are possible, we must add a type annotation as described in the chapter on decision variables.

Scalar Types

A scalar type represents a single value. Pint has three primary scalar types: integers, Booleans, and 256-bit hashes.

Integer Type

An integer is a number without a fractional component. Pint has a single integer type called int which, when targeting the EssentialVM, represents a 64-bit signed integer . An int, therefore, can store numbers from $-(2^{n-1})$ to $2^{n-1}-1$ inclusive, where n is the number of bits that represent the integer (64 in the case of EssentialVM).

You can write integer literals in any of the forms shown in the table below. Note that number literals can use _ as a visual separator to make the number easier to read, such as 1_000, which will have the same value as if you had specified 1000.

Numeric Operations

Pint supports the basic mathematical operations you’d expect for integers: addition, subtraction, multiplication, division, and remainder. Integer division truncates toward zero to the nearest integer. The following code shows how you’d use each numeric operation in a var statement:

// addition
var sum = 1 + 2 + 3;

// subtraction
var difference = 15 - 1;

// multiplication
var product = 42 * 42;

// division
var quotient = 3 / 2;
var truncated = -5 / 3; // Results is -1

// remainder
var remainder = 34 % 3;

Note that binary operators in Pint are strict with regards to what types they allow, that is, only identical types can be used in a binary operator. For example, adding an int and a bool is not a valid operation and will result in a compile error.

The Boolean Type

As in most other programming languages, a Boolean type in Pint has two possible values: true and false. The Boolean type in Pint is specified using bool. For example:

var t = true;
var f: bool = false;

The b256 Type

The b256 is a special type that represents a 256-bit hash. It is often used to represent addresses or storage keys and cannot be used as a numerical integers. That is, two b256 values cannot added for example.

A b256 literals can be represented using a Hexadecimal or a Binary literal as follows:

var addr1 = 0x3333333333333333333333333333333333333333333333333333333333333333;
var addr2: b256 = 0b1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111;

Compound Types

Compound types can group multiple values into one type. Pint has two primitive compound types: tuples and arrays.

The Tuple Type

A tuple is a general way of grouping together a number of values with a variety of types into one compound type. Tuples have a fixed length: once declared, they cannot grow or shrink in size.

We create a tuple by writing a comma-separated list of values inside curly brackets { .. }. Each position in the tuple has a type, and the types of the different values in the tuple don’t have to be the same. We’ve added optional type annotations in this example:

var tup_1: { int, int, bool } = { 42, 4, true };

The variable tup binds to the entire tuple because a tuple is considered to be a single compound element. To get the individual values out of a tuple, we can use the period (.) operator followed by the index of the value we want to access. For example:

var tup_2: { int, int, bool } = { 42, 4, true };
var tup_2_first = tup_2.0;
var tup_2_second = tup_2.1;
var tup_2_third = tup_2.2;

This program creates the tuple tup_2 and then accesses each element of the tuple using its respective index. As with most programming languages, the first index in a tuple is 0.

It is also possible to name some or all the fields of a tuple type as follows:

var tup_3: { x: int, int, y: bool } = { 42, 4, true };

Note that, in this example, only two out of the 3 fields are named. In order to access the individual elements of a tuple with named fields, the period (.) can again be used with either the index of the tuple field or its name. For example:

var tup_4: { x: int, int, y: bool } = { 42, 4, true };
var tup_4_first = tup_4.0;
var tup_4_first_named = tup_4.x; // same as `tup_4.0`
var tup_4_second = tup_4.1;
var tup_4_third = tup_4.2;
var tup_4_third_named = tup_4.y; // same as `tup_4.y`

Tuples without any values are not allowed in Pint. That is, the following:

var empty: {} = {};

is disallowed and errors out as follows:

Error: empty tuple types are not allowed
    ╭─[ch_3_2.pnt:43:12]
    │
 43 │ var empty: {} = {};
    │            ─┬
    │             ╰── empty tuple type found
────╯
Error: empty tuple expressions are not allowed
    ╭─[ch_3_2.pnt:43:17]
    │
 43 │ var empty: {} = {};
    │                 ─┬
    │                  ╰── empty tuple expression found
────╯

The Array Type

Another way to have a collection of multiple values is with an array. Unlike a tuple, every element of an array must have the same type. Unlike arrays in some other languages, arrays in Pint have a fixed length.

We write the values in an array as a comma-separated list inside square brackets:

var a = [1, 2, 3, 4, 5];

You write an array's type using the element type followed by its size between square brackets, like so:

var b: int[5] = [1, 2, 3, 4, 5];

Here, int is the type of each element. The number 5 indicates that the array contains five elements.

You can access elements of an array using by indexing into it, like this:

var c: int[5] = [1, 2, 3, 4, 5];
var c_first = c[0];
var c_second = c[1];

In this example, the variable named c_first will get the value 1 because that is the value at index 0 in the array. The variable named c_second will get the value 2 from index 1 in the array.

Comments

All programmers strive to make their code easy to understand, but sometimes extra explanation is warranted. In these cases, programmers leave comments in their source code that the compiler will ignore but people reading the source code may find useful.

Here’s a simple comment:

// hello, world

In Pint, the only comment style supported starts a comment with two slashes, and the comment continues until the end of the line. For comments that extend beyond a single line, you’ll need to include // on each line, like this:

// This is some complicated code that requires multiple lines to explain:
// 1. The first predicate, called `GetRich` ensures that we're getting rich.
// 2. The second predicate, called `BeResponsible` ensures that 
//    we're not gambling all the money away.

Comments can also be placed at the end of lines containing code:

var big_answer = 42; // answer to life, the universe, and everything

But you’ll more often see them used in this format, with the comment on a separate line above the code it’s annotating:

// answer to life, the universe, and everything
var big_answer_too = 42;

Conditionals

Pint has three different ways to express conditionals: select expressions, cond expressions, and if statements. Conditionals allow you to "branch" your code depending on some condition(s). The word "branch" is between quotations because Pint is not an imperative language and does not "execute" code. Therefore, conditionals are simply a way of saying: "choose between some expressions or some constraints based on some condition(s)".

Select Expressions

A select expression allows you to select between two alternatives based on a condition. The two alternatives must have the same type and that type determines the type of the whole select expression. For example:

var number: int;

var y = number < 5 ? 1 : 2;

All select expressions start with a condition followed by the ? symbol. In this case, the condition checks whether or not the decision variable number has a value less than 5. We place the expression that should be chosen if the condition is true immediately after the ? symbol. The symbol : is then added followed by the expression that should be chosen if the condition is false. Both options, 1 and 2, have the same type which is int and so, the type of y must also be int.

If, for example, the types of the two expressions we're selecting from do not match, the compiler will emit a compile error. For example, if we try to compile the following code:

var number: int;

var y = number < 5 ? 1 : true;

we will get the following error:

Error: branches of a select expression must have the same type
   ╭─[test.pnt:3:9]
   │
 3 │ var y = number < 5 ? 1 : true;
   │                      ┬   ──┬─
   │                      ╰───────── 'then' branch has the type `int`
   │                            │
   │                            ╰─── 'else' branch has the type `bool`

The condition of a select expression must be a bool. Otherwise, we will get a compile error. For example, if we try to compile the following code:

var number: int;

var y = number ? 1 : 2;

we will get the following error:

Error: condition for select expression must be a `bool`
   ╭─[test.pnt:3:9]
   │
 3 │ var y = number ? 1 : 2;
   │         ───┬──
   │            ╰──── invalid type `int`, expecting `bool`
───╯

Note that Pint will not automatically try to convert non-Boolean types to a Boolean. You must be explicit and always provide a select expression with a Boolean as its condition.

cond Expressions

Pint provides cond expressions. cond expressions are generalized select expressions that are not limited to only two branches. They provide selection from multiple alternatives, each based on some condition. For example:

var x: int;
var z = cond {
    x == 0 => 0,
    x > 0 && x <= 10 => 1,
    x > 10 && x <= 100 => 2,
    else => 3
};

All cond expressions start with the keyword cond, followed by a comma-separated list of statements in between curly brackets. Each statement describes a condition and an expression that should be returned by the cond if that condition is correct. The branches are evaluated in order and the first one to become active determines the value of the cond expression. If all branches fail, then the cond expression takes the value of the expression in the else branch, which must always be the last branch.

in the example above, z is equal to 0 if x == 0, equal to 1 if x is between 0 and 10, equal to 2 if x is between 10 and 100, and equal to 3 otherwise.

every cond expression can be rewritten using one or more select expressions. however, cond tends to be more compact and more readable than nested select expressions. for example, the cond expression in the example above is equivalent to:

var x: int;
var z = x == 0 ? 0 :
               x > 0 && x <= 10 ? 1
                 : x > 10 && x <= 100 ? 2 : 3;

similarly to select expressions, all candidate expressions must have the same type which determines the type of the whole cond expression. also, every condition must be a bool or else a compile error will be emitted.

if Statements

if statements are the last class of conditionals we will look at. Unlike select and cond expressions, if statements are not expressions, that is, they do not hold any values. Instead, they allow predicating blocks of code based on some condition. A block of code in the context of an if statement is a collection of constraints and other if statements. For example:

if number < 5 {
    constraint x == y;
} else {
    constraint x != y;
}

All if statements start with the keyword if, followed by a condition. In this case, the condition checks whether or not the decision variable number has a value less than 5. The code block that should be "active" if the condition is true is placed immediate after the condition inside curly brackets. Optionally, the keyword else is then added followed by the code block that should be active if the condition is false (also between curly brackets). In the example above, the if statement can be read as follows: "if number is less than 5, then x must be equal to y. Otherwise, x must not be equal to y".

Similarly to select expressions, the condition of an if statement must be a bool. Otherwise we will get a compile error.

if statements can be nested and can contain an arbitrary number of constraints:

if number < 5 {
    constraint x == y;

    if z > 0 {
        constraint x > number;
        constraint y > number;
    }
} else {
    constraint x != y;

    if z > 0 {
        constraint x > number;
        constraint y > number;
    } else {
        constraint x < number;
        constraint y < number;
    }
}

Custom Types

Custom data types are named types that you can define in your program to refer, via an alias, to a primitive type, a compound type, or an enum. Enums are another special class of custom types that define enumerations with named variants.

Both custom type and enum declarations must be made at the top level of a module, and are not allowed inside a predicate declaration.

Type Aliases

Pint provides the ability to declare a type alias to give an existing type another name. For this we use the type keyword. For example, we can create the alias Balance to int like so:

type Balance = int;

Now, the alias Balance is a synonym for int. Values that have the type Balance will be treated the same as values of type int:

var x: int = 5;
var y: Balance = 5;
constraint x == y;

Because Balance and int are the same type, we can compare values of both types.

Defining structs using type

Many programming languages offer the concept of a "struct" which lets you package together and name multiple related values that make up a meaningful group. While Pint does not offer a special struct construct, it does offer a way to name a tuple, name its fields, and access its elements as if it were a struct.

To define a struct-like tuple (which we will just call a struct going forward), we use the type keyword followed by the name chosen for the tuple. We then use the = operator to bind the new type name to a tuple type with all of its fields named.

For example:

type User = {
    status: bool,
    address: b256,
    balance: int,
};

To use a struct after we’ve defined it, we create an instance of that struct by specifying concrete values for each of the fields. We create an instance using the same tuple expression syntax: curly brackets containing key: value pairs, where the keys are the names of the fields and the values are the data we want to store in those fields. We don’t have to specify the fields in the same order in which we declared them in the struct. In other words, the struct definition is like a general template for the type, and instances fill in that template with particular data to create values of the type. For example, we can declare a particular User as shown below:

var user1: User = {
    status: true,
    address: 0x1111111111111111111111111111111111111111111111111111111111111111,
    balance: 42,
};

To get a specific value from a struct, we use the dot notation similarly to tuples. For example, to access this user's balance, we use user1.balance.

Enumerations

Enums allow you to define a type by enumerating its possible variants. Where structs and tuples give you a way of grouping together related fields and data, like a User with its status, address, and balance, enums give you a way of saying a value is one of possible set of values. For example, we may want to say that User is one of a set of possible account types that also includes Contract. To do this, Pint allows us to encode these possibilities as an enum.

Let’s look at a situation we might want to express in code and see why enums are useful. Say we need to work with three possible tokens: DAI, USDC, and USDT. Because these are the only tokens we want to work with, we can enumerate all possible variants, which is where enumeration gets its name:

enum Token = DAI | USDC | USDT;

Note how the possible variants of Token are separated by a |. Token is now a custom data type that we can use elsewhere in our code. Also, we can now create an instance of each of the three variants of Token like this:

var dai: Token = Token::DAI;
var usdc: Token = Token::USDC;
var usdt: Token = Token::USDT;

Note that the variants of the enum are namespaced under its identifier, and we use a double colon to separate the two. This is useful because now all three values Token::DAI, Token::USDC, and Token::USDT are of the same type: Token. We can then, for instance, declare a variable called token_type to be of type Token and assign it to either variants depending on how large some value amount is.

var amount: int;
var token_type: Token = cond {
    amount in 0..1000 => Token::DAI,
    amount in 1001..2000  => Token::USDC,
    else  => Token::USDT,
};

We can even use enums inside structs as follows:

type Bal = {
    token: Token,
    bal: int,
};

predicate balances {
    var user1_bal = {
        token: Token::DAI,
        bal: 42,
    };

    var user2_bal = {
        token: Token::USDC,
        bal: 96,
    };

    var user3_bal = {
        token: Token::USDT,
        bal: 100,
    };
}

Constraints

Constraints are the building blocks of a Pint contract. Simply put, a constraint is a declaration that starts with the keyword constraint followed by a Boolean expression:

var x: int;
constraint x == 0;

The above is a simple constraint which ensures that the value of x is exactly 0. Every proposed solution to this contract must set x to 0. Otherwise, the constraint will fail. If we have multiple constraint declarations, then all of them must be satisfied for a solution to be valid. For example:

var y: int;
constraint y >= 0;
constraint y <= 10;

In the above, every valid solution must set y to a value between 0 and 10.

Note that the above is actually equivalent to:

constraint y >= 0 && y <= 10;

However, you may find it easier to structure your code into multiple separate constraints. Otherwise, you'll find yourself with a giant constraint declaration that is hard to read and maintain.

As mentioned above, the expression of a constraint declaration must be of type boolean. Otherwise, a compile error will be produced. For example:

constraint x + y

will result in the following error:

Error: constraint expression type error
    ╭─[example.pnt:16:1]
    │
 16 │ constraint x + y;
    │ ────────┬───────
    │         ╰───────── constraint expression has unexpected type `int`
    │         │
    │         ╰───────── expecting type `bool`
────╯
Error: could not compile `example.pnt` due to previous error

Constants

Sometimes it may be desirable to use a common constant value for re-use throughout a program which is not a decision variable to be solved. These may be declared in Pint using the const keyword.

const declarations resemble var declarations in that they name an optionally typed value with an initializer.

const minimum: int = 10;
const maximum: int = 20;

predicate Foo {
    var foo: int;

    var size: int;
    constraint size >= minimum && foo <= maximum;
}

Like var declarations the type may be omitted and will be inferred by the Pint compiler, but the const initializer is required and must a constant expression which does not refer to decision variables nor other non-constant values such as state.

Constants of Compound Types

const declarations may refer to values with compound types as long as every element within is a constant value. Constant value initializers may also dereference other array or tuple const declarations or even array or tuple literals.

const counts = [20, 30, 40];

const default_idx = 1;
const next_count = counts[default_idx + 1];

const min_size = { valid: true, size: 10 };

predicate Bar {
    var my_size: int;
    constraint !min_size.valid || my_size >= min_size.size;
}

In the above example next_count is evaluated at compile time to be fixed as 40.

The min_size tuple is adding a flag to a value to mark whether it should be used or not in a constraint. This may be convenient during development for turning the min_size.size constraint on or off.

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.

Storage

Most useful Pint contracts require some sort of persistent storage that represent state. After all, a blockchain is a decentralized distributed database and contracts are a way to enforce rules on how "entries" in this database are allowed to change. Therefore, having the ability to express those database entries using variables and dynamic containers is quite useful. For that reason, Pint offers a way to declare and access a variety of storage types.

In this chapter, we will cover the following:

• How to declare and access storage variables with statically-sized types.
• How to declare and access storage variables with dynamically-sized types.
• How to access storage variables that belong to an external contract.

Statically-Sized Storage Types

All storage variables in a Pint contract must be declared inside a storage block, and there can only be a single storage block in a Pint contract. The storage block is optional and can be skipped if the contract does not need to manage any state, but such contracts are generally not very useful.

Here's an example of a storage block:

storage {
    x: int,
    a: b256,
    t: { int, bool },
    y: bool,
    w: int,
    arr: { int, int }[3],
    v: { int, { bool, b256 } },
}

A storage starts with the keyword storage and followed by a comma-separated list of variable declarations inside curly brackets. Each variable declaration is an identifier annotated with a type. In this chapter, we're only looking at storage variables that have statically-sized types, i.e., types that have known sizes and layouts at compile time. This pretty much covers every type we discussed so far! In the next chapter, we will introduce new storage-only types that are dynamically sized.

Back to the example above, the declared storage block is fairly simple. It contains three variables that have primitive types and one variable that has a compound type (a tuple). Unlike decision variables, storage variables do not accept an initializer and must have a type annotation.

Accessing Storage Variables

Storage variables are not useful unless we can read them and/or propose modifications to them. Recall that Pint is a declarative constraint-based language, and therefore, does not allow "writing" directly to a storage variable. Writing directly to storage is a concept you might be familiar with from other smart contract languages like Solidity, so you might be asking yourself the following question: "if I can't write directly to storage variables, how will their values ever change? How will the state of the blockchain ever change?"

The answer to these questions lies at the core of what makes Pint and declarative blockchains actually declarative. Pint has no concept of "updating" state (or even decision variables for that matter). Pint simply expresses a desired outcome using constraint statements and relies on solutions to actually propose state changes.

In order to express a desired outcome for a given storage variable, two things are needed:

1. A way to read the current value of the variable.
2. A way to express the future value of the variable.

Reading a Storage Variable

Reading a storage variable should not be an unfamiliar concept to you if you've worked with other smart contract languages before like Solidity. The syntax for reading a storage variable in Pint requires the storage keyword again:

state x = storage::x;
state a = storage::a;
state t = storage::t;
state t_1 = storage::t.1;
state arr_2_1 = storage::arr[2].1;

A few things to note here:

1. Storage read expressions always start with storage:: followed by the name of the variable we're trying to read. The storage:: syntax means we're switching namespaces to that of the storage block.
2. Each storage read expression is used to initialize a state variable. In fact, storage read expressions can only ever be used to initialize state variables. Using a storage read expression in other contexts, such as in constraint storage::x == 5, is illegal.
3. Fields or elements of a compound type in storage can be accessed individually, as in storage::t.1 and storage::arr[2].1.

We haven't really explained what a state variable is so this is probably a good time to do so.

State Variables

A state variable is a special type of variables that can only hold values read from storage. A state variable must always have an initializer and that initializer can only be a storage read expression. Type annotations for state declarations are optional:

state not_annotated = storage::x;
state annotated: b256 = storage::a;

Once a state variable is declared, it can be used anywhere in its scope as if it were a decision variable:

state t_0 = storage::t.0;
state y = storage::y;
constraint y && t_0 >= 42;

This is an example where two state variables are declared and later constrained as if they were decision variables. One important distinction to note here is that state variables are not actually unknown. By definition, decision variables are unknown at compile time and at solve-time and they only become known after the solving process is finished (if a solution is found). In contrast, state variables, while unknown at compile time, are actually known at solve-time: right before the solving process starts, every storage read expression is evaluated by directly inspecting the blockchain. The result is then assigned to the corresponding state variable which becomes known in preparation for solving.

Next State

Recall that expressing a desired outcome for a given storage variable also requires a way to express the future value of the variable.

In most imperative languages, statements like x = x + 1 are commonly used to mean "update the value of x to be equal to the current value of x plus 1". Because Pint is a constraint-based declarative language where the order of statements does not matter and there is no sequential execution, statements like x = x + 1 cannot be written and are not logical. Instead, Pint offers a special syntax, reserved for state variables, that means "the future value of". Here's an example:

state bal = mut storage::x;
constraint bal' >= bal + 42;

Here, bal', unlike bal, is actually unknown at solve-time. That is, bal' must be solved for as if it were a decision variable and every solution must include a proposed value for bal'. If, for example, the value of bal was read to be 100 at solve-time, a solver might propose that the next value of bal should be 150 (i.e. bal' = 150) which would be a valid solution because 150 >= 100 + 42 (assuming all other constraints in the predicate are also satisfied).

"Mutable" Storage Accesses

In the previous section, you may have noticed that we added the mut keyword before storage::x in the state declaration. In Pint, storage locations are non-mutable by default. That is, solvers cannot propose new values for a storage location unless they are solving a predicate that allows the storage location to be mutable. This is accomplished using the mut keyword added before a storage access. In the example of the previous section, because mut was added before storage::x, a solver can now propose a state mutation that updates the value of x.

When the mut keyword as added before a storage access into a compound type, mutability applies only to the portion of the compound type that is being accessed. For example, in the example below:

state inner: { bool, b256 } = mut storage::v.1;

v.1 is a storage access into nested tuple v defined in the storage block declared earlier. Here, both v.1.0 ( a bool) and v.1.1 (a b256) are both allowed to be mutated, but v.0 is not allowed to be.

"Empty" State

You may be wondering what happens if a storage variable was never previously updated but was read anyways. In this case, there is no value stored at that storage variable and nothing can be read. To help you reason about this, Pint provides the literal nil to represent the absence of a value. For example,

state w = mut storage::w;
var value: int = (w == nil ? 0 : w);

In the example above, we first check if w is nil before attempting to read it. If it is nil (i.e. currently has no value), then we constrain value to 0. Otherwise, we constrain it to the non-empty value of w. Without checking if w is nil first, and if we're not sure whether w has a value or not, then it is possible that the state read operation will panic.

It is also possible to update a state variable to nil using the "next state" operator:

if w != nil {
    constraint w' == nil;
}

Here, if w currently has a value, then we constrain the next value of w to be nil.

This concludes our overview on storage which only focused on statically-sized storage types. In the next chapter, we will cover dynamically-sized storage types which offer a lot more flexibility.

Dynamically-sized Storage Types

Pint includes a number of very useful data structures called storage collections. Most other data types represent one specific value, but storage collections can contain multiple values. Unlike the built-in array and tuple types, the amount of data that these collections hold does not need to be known at compile time and can grow or shrink as the blockchain state evolve. Each kind of collection has different capabilities and costs, and choosing an appropriate one highly depends on the situation at hand. In this chapter, we'll discuss two collections that are used very often in Pint contracts:

• Storage Map: allows you to associated a value with a particular key.
• Storage Vector: allows you to store a variable number of values.

We'll discuss how to create and update storage maps and storage vectors.

Storage Map

The first collection we will look at is the storage map. A storage map stores a mapping of keys of some type K to values of some type V using a hashing function, which determines how it places these keys and values in storage. Hash maps are useful when you want to look up data by using a key that can be of any type. For example, in the Subcurrency contract, we kept track of each user’s token balance in a map in which each key is a user’s address and the values are each user’s balance. Given a user address, you can retrieve their balance.

Creating a New Storage Map

Because storage maps are a storage type, they must always be declared inside a storage block. The storage map type is a built-in type with a specific syntax:

storage {
    // ...
    balances: (b256 => int),
    // ...
}

Here, a new storage map, called balances, is declared that maps b256 keys to int values. The storage map type is always declared using parentheses that contain two types separated by a =>. It should be clear that storage maps are homogeneous, that is, all of the keys must have the same type as each other, and all of the values must have the same type as well.

Accessing Values in a HashMap

We can get a value out of the storage map by providing its key in between square brackets, similar to how arrays are accessed:

var from_address: b256;
var receiver_address: b256;
state from_balance = storage::balances[from_address];
state receiver_balance = storage::balances[receiver_address];

Here, from_balance will have the value that's associated with from_address and receiver_balance will have the value that's associated with receiver_address. Because the values returned are storage values, we must assign them to state variables. Using a storage map access expression in any other context results in a compile error.

"Updating" a Storage Map

As we've mentioned a few times already, explicitly "updating" anything in Pint is not a valid operation because Pint has no sequential execution. However, as in the case with statically-sized storage types, we can require that the next value of a specific entry in a storage map satisfy some constraint(s):

var my_address: b256;
state my_bal = mut storage::balances[my_address];
constraint my_bal' == my_bal + 1000000;

Here, we're requiring that our balance go up by 1 million, by applying the "prime" operator on the state variable that holds our current balance. Of course, requiring a change in state does not mean it will actually happen! Otherwise, we can all become instantly rich by submitting predicates like this. Unless a solution that does not violate any of the deployed rules (i.e. constraints) is submitted by a solver, the desired state change will never be satisfied.

"Missing" Keys

Now, you may be wondering what happens if a key is missing from a storage map and we try to access it anyways. In Pint, a nil is returned. In the previous example, if the balance of my_address was never actually modified in the past, then my_bal would be equal to nil and therefore, the expression my_bal + 1000000 would panic. To avoid this problem, we can first check if my_bal is nil before trying to use it in an arithmetic operation:

if my_bal != nil {
    constraint my_bal' == my_bal + 1000000;
} else {
    constraint my_bal' == 1000000;
}

Here, if my_bal is not nil, then the constraint remains the same as before. Otherwise, we simply update my_bal to 1000000 (as if my_bal was previously 0!).

Complex Maps

Storage maps can be declared to be arbitrarily complex. They can also be nested!

storage {
    // ...
    complex_map: ( { int, int } => { bool, b256 } ),
    nested_map: (b256 => (int => bool)),
    // ...
}

In the example above, the fist storage map maps a tuple to another tuple. The second storage map maps a b256 to another map! The way to access entries in these maps should is fairly intuitive and is exactly what you'd expect:

state complex_read: b256 = storage::complex_map[{42, 69}].1;

var addr1: b256;
state nested_read: bool = storage::nested_map[addr1][100];

The first storage access reads a tuple value using a key that itself is a tuple, and then accesses its second field. The second storage access is a nested map access using two index operators. Note that the first index operator accesses the first key (b256 in this case) and the second index operator accesses the second key (int in this case).

Illegal Uses of the Storage Map Type

It may be tempting to write code like this:

storage {
    // ...
    nested_map: (b256 => (int => bool)),
    // ...
}

predicate test {
    var addr: b256;

    state nested_map = storage::nested_map; // Expecting to return the "whole" map
    state nested_map_inner = storage::nested_map[addr]; // Expecting to return the "whole" inner map
}

However, the compiler will disallow this by emitting the following errors:

Error: state variables cannot have storage map type
   ╭─[bad.pnt:8:1]
   │
 8 │ state nested_map = storage::nested_map; // Expecting to return the "whole" map
   │ ───────────────────┬──────────────────
   │                    ╰──────────────────── found state variable of type storage map here
───╯
Error: state variables cannot have storage map type
   ╭─[bad.pnt:9:1]
   │
 9 │ state nested_map_inner = storage::nested_map[addr]; // Expecting to return the "whole" inner map
   │ ─────────────────────────┬────────────────────────
   │                          ╰────────────────────────── found state variable of type storage map here
───╯

Hopefully the errors are clear enough. What the compiler is telling us here is that we cannot declare state variables that hold entire storage maps. A storage map is not exactly an object that we can store a reference to or copy/move around and state variables can only have statically-sized types!

Storage Vector

Note: Storage vectors are work-in-progress

External Storage Access

It is common for one smart contract to want to reason about the state of another external smart contract. For example, a Decentralized Exchange contract typically requires reading and modifying the state (balances!) owned by the external contracts of the tokens that are being traded through the exchange.

In imperative smart contract languages like Solidity, reasoning about external state is typically done by calling some methods in the external contract that access or modify that contract's state. In Pint however, the storage variables of a contract are public and can be accessed from outside the contract using the contract's interface.

Interface Instance

While a contract's interface contains all the public symbols that can be externally accessed, it does not specify the address of the contract. The address of a contract is 256-bit value that uniquely identify the contract on the blockchain. Specifying the address is required because multiple contracts with different addresses may share the same interface.

In order to specify which external contract to actually interact with, we need an interface instance. Consider the counter example that we presented earlier and its interface that looks like this:

interface Counter {
    storage {
        counter: int,
    }

    predicate Initialize;

    predicate Increment;
}

Assume that a contract with that interface has been deployed and has the following address:

const ContractID: b256 = 0x0003000300030003000300030003000300030003000300030003000300030003;

In order to interact with that particular contract, we would first declare an interface instance as follows:

interface CounterInstance = Counter(ContractID);

External Storage Access Using the Interface Instance

Now that we have an instance of the interface, we can use it to create a path to the external storage variable. For example,

state counter = CounterInstance::storage::counter;

Note that the path CounterInstance::storage::counter has three parts:

1. The name of the interface instance CounterInstance that indicates which instance we would like to access. Recall that there could be multiple interface instances, with different addresses, for the same interface, hence the need to start the path with the name of the interface instance and not the name of interface itself.
2. The keyword storage to indicate that we're accessing the storage block of CounterInstance.
3. counter, the name of the storage variable we want to access.

Once we have assigned the external storage expression to a state variable, we can then use that variable as we usually do.

Similarly to local storage access expressions, the expression CounterInstance::storage::counter can only be used on the right-hand side of a state declaration.

Note: The mut keyword cannot be added to external storage accesses. External storage locations belong to the external contract that owns and it's up to the predicates in that contract to control their mutability.

Managine Growing Projects

As you write large programs, organizing your code will become increasingly important. By grouping related functionality and separating code with distinct features, you’ll clarify where to find code that implements a particular feature and where to go to change how a feature works.

As a project grows, you should organize code by splitting it into multiple modules and then multiple files. You can also extract parts of a project into separate packages that become external dependencies. This chapter covers all these techniques.

Pint has a number of features that allow you to manage your code’s organization, including which details are exposed, which details are private, and what names are in each scope in your programs. These features, sometimes collectively referred to as the module system, include:

• Packages: A feature of the pint tool that lets you build, test, and share projects.
• Modules and use: Let you control the organization and scope of paths.
• Paths: A way of naming an item, such as a type, a macro, or a const.

In this chapter, we’ll cover all these features, discuss how they interact, and explain how to use them to manage scope. By the end, you should have a solid understanding of the module system.

Pint Packages

The first part of the module system we’ll cover are packages.

A package is a bundle of one or more modules that provides a set of functionality. A package contains a pint.toml file that describes how to build it.

Packages can come in one of two forms: a "contract" package and a "library" package. Contract packages represent smart contracts that can be compiled to bytecode and deployed to a blockchain. Each contract package must have a contract.pnt file in its src directory, which represents the entry point of the contract. Library packages don't compile to bytecode. Instead, they define functionality intended to be shared with multiple projects. The entry point of a library crate is always a lib.pnt file in the src directory.

Let's walk through what happens when we create a package. First, we enter the command pint new my-project:

$ pint new my-project
     Created my-project [contract] (/path/to/my-project)
$ ls my-project
pint.toml src
$ ls my-project/src
contract.pnt

After we run pint new, we use ls to see what the pint tool creates. In the project directory, there's a pint.toml file, giving us a package. There's also an src directory that contains contract.pnt. Open pint.toml in your text editor, and note there's no mention of src/contract.pnt. The pint tool follows a convention that src/contract.pnt is the root file of a contract package. Likewise, src/lib.pnt is the root file of a library package.

Note that the pint.toml file does contain a field called kind, which is set to contract in the example above, to indicate that this particular package is a contract. In contrast, if we were to create a library package using pint new my-library --lib, then we would find that the kind field in the generated pint.toml is set to library.

Defining Modules

In this section, we’ll talk about modules and other parts of the module system, namely paths that allow you to name items and the use keyword that brings a path into scope.

Modules Cheat Sheet

Here we provide a quick reference on how modules, paths, and the use keyword work in the compiler, and how most developers organize their code. We’ll be going through examples of each of these rules throughout this chapter, but this is a great place to refer to as a reminder of how modules work.

• Start from the package root: When compiling a package, the compiler first looks for code to compile in the package root file, which is src/lib.pnt for a library package or src/contract.rs for a contract package.
• Declaring modules: You can declare new modules by creating files for them in the appropriate directories. Say you want to declare a new garden module. You have two options:
  • You can create the file src/garden.pnt if you want the garden module to be a single file module. That is, if you don't want the module garden to have submodules.
  • You can create the file src/garden/garden.pnt if you want the module to be a multi-file module. That is, if you want the module garden to have submodules. The submodules of garden would then live in the src/garden directory.
• Declaring submodules: In any directory other than the package root directory, you can create new submodules. For example, say you want to declare a submodule of garden named vegetables. You have two options:
  • You can create the file src/garden/vegetables.rs if you want the vegetables submodule to be a single file submodule. That is, if you don't want the submodule vegetables to have its own submodules.
  • You can create the file src/garden/vegetables/vegetables.rs if you want the vegetables submodules to be a multi-file submodule. That is, if you want the submodule vegetables to have its own submodules.
• Paths to code in modules: Once a module is part of your package, you can refer to code in that module from anywhere else in the same package. For example, an enum Asparagus in the garden vegetables module would be found at ::garden::vegetables::Asparagus.
• The use keyword: Within a Pint file, the use keyword creates shortcuts to items to reduce repetition of long paths. For example, you can create a shortcut to ::garden::vegetables::Asparagus using the statement use ::garden::vegetables::Asparagus; declared at global scope in a Pint file. From then on, you only need to write Asparagus to make use of that enum in this file.

Here, we create a contract package named backyard that illustrates these rules. The package's directory, also named backyard, contains these files and directories:

backyard
├── pint.toml
└── src
    ├── contract.pnt
    └── garden
        ├── garden.rs
        └── vegetables.rs

The package root file is src/contract.rs since this is a contract package. It contains:

use garden::vegetables::Asparagus;

predicate Foo {
    var green_asparagus = Asparagus::Green;
}

The submodule vegetables which is defined in src/garden/vegetables.pnt, contains:

enum Asparagus = Green | White | Purple;

Paths for Referring to an item in a Module Tree

To show Pint where to find an item in a module tree, we use a path in the same way we use a path when navigating a filesystem. To use a custom type for example, we need to know its path.

A path can take two forms:

• An absolute path is the full path starting from a package root; for code from an external package, the absolute path begins with the package name, and for code from the current package, it starts with double colons (::).
• A relative path starts from the current module and uses an identifier in the current module.

Both absolute and relative paths are followed by one or more identifiers separated by double colons (::).

Returning to the "backyard" example from the previous chapter, say we want to access the enum Asparagus. This is the same as asking: what's the path of the Asparagus enum. We'll show two ways to access Asparagus from the root file:

predicate Bar {
    var first_asparagus: ::garden::vegetables::Asparagus;

    var second_asparagus: garden::vegetables::Asparagus;
}

The first time we refer to the enum Asparagus we use an absolute path. The enum Asparagus is defined in the same package as our root module above, which means we can use :: to start an absolute path. We then include each of the successive modules until we make our way to Asparagus.

The second time we refer to the enum Asparagus, we use a relative path. The path starts with garden, the name of the module defined at the same level of the module tree as the root module.

Choosing whether to use a relative or absolute path is a decision you’ll make based on your project, and depends on whether you’re more likely to move item definition code separately from or together with the code that uses the item. For example, if we move the garden module to a module named estate, we’d need to update the absolute path to Asparagus, but the relative path would still be valid. However, if we moved var first_asparagus into a module named salad, the absolute path to Asparagus would stay the same, but the relative path would need to be updated. Our preference in general is to specify absolute paths because it’s more likely we’ll want to move code definitions and item calls independently of each other.

Bringing Paths into Scope with the use Keyword

Having to write out the paths to access items can feel inconvenient and repetitive. In the previous chapter, whether we chose the absolute or relative path to Asparagus, every time we wanted to use Asparagus we had to specify the modules garden and vegetables. Fortunately, there’s a way to simplify this process: we can create a shortcut to a path with the use keyword once, and then use the shorter name everywhere else in the scope.

In the example below, we bring the ::garden::vegetables module into the scope of the root file to use the Asparagus enum:

use ::garden::vegetables;

predicate Baz {
    var third_asparagus: vegetables::Asparagus;
}

Adding use and a path in a scope is similar to creating a symbolic link in the filesystem. By adding use ::garden::vegetables in the root file, vegetables is now a valid name in that scope.

Handling conflicting imports

Pint does not allow bringing two items with the same name into scope with use. This name clash makes it impossible for the compiler to distinguish between the two items in the scope. There are two ways to avoid this problem. The first, is to only import the names of the parent modules.

Consider the following two libraries:

// Module data::contract_lib

type Data = { 
    address: b256,
    storage_vars: int,
    predicates: int,
};

// Module data::predicate_lib

type Data = { 
    address: b256,
    decision_vars: int,
    pub_vars: int,
};

Both libraries use the name Data to describe a types. The example below shows how to bring the two Data types into scope and how to refer to them without having a conflict.

use ::data::contract_lib;
use ::data::predicate_lib;

predicate test {
    var contract_data: contract_lib::Data;
    var predicate_data: predicate_lib::Data;
}

As you can see, using the parent module distinguishes the two Data types. If instead we specified use data::contract_lib::Data and use data::predicate_lib::Data, we'd have two Data types in the same scope and Pint wouldn't know which one we meant when we used Data.

There’s another solution to the problem of bringing two types of the same name into the same scope with use: after the path, we can specify as and a new local name, or alias, for the type. The example below shows another way to write the code in the previous example by renaming the two Data types using as.

use ::data::contract_lib::Data as ContractData;
use ::data::predicate_lib::Data as PredicateData;

predicate test {
var contract_data: ContractData;
var predicate_data: PredicateData;

In each use statement, we choose a new name for Data. That guarantees that no conflicts arise. This also has the side benefit of giving Data a more meaningful name in the current context.

Using Nested Paths to Clean Up Large use Lists

If we’re using multiple items defined in the same module, listing each item on its own line can take up a lot of vertical space in our files. For example, these two use statements we had in the previous example bring two items into scope:

use ::data::contract_lib::Data as ContractData;
use ::data::predicate_lib::Data as PredicateData;

Instead, we can use nested paths to bring the same items into scope in one line. We do this by specifying the common part of the path, followed by two colons, and then curly brackets around a list of the parts of the paths that differ, as shown below.

use ::data::{contract_lib::Data as ContractData, predicate_lib::Data as PredicateData};

In bigger programs, bringing many items into scope from the same module using nested paths can reduce the number of separate use statements needed by a lot!

We can use a nested path at any level in a path, which is useful when combining two use statements that share a subpath. For example, the code snippet below shows two use statements: one that brings data::contract_lib into scope and one that brings data::contract_lib::Data into scope.

use ::data::contract_lib;
use ::data::contract_lib::Data;

The common part of these two paths is data::contract_lib, and that’s the complete first path. To merge these two paths into one use statement, we can use self in the nested path, as shown below.

use ::data::contract_lib::{self, Data};

This line brings data::contract_lib and data::contract_lib::Data into scope.

Advanced Features

By now, you’ve learned the most commonly used parts of the Pint programming language. We will look at a few aspects of the language you might run into every once in a while, but may not use every day. The features covered here are useful in very specific situations. Although you might not reach for them often, we want to make sure you have a grasp of all the features Pint has to offer.

In this chapter, we'll cover:

• Public decision variables: how to declare decision variables that are public and how to access them from external contexts.
• Macros: how to write reusable code using macros.

Public Decision Variables

By default, all decision variables are private. That is, they are only accessible from within the predicate that declares them. There is no way to reason about the value of a private decision variable from outside the predicate. This, however, may not be sufficient to build certain applications. It also imposes limitations on how contracts are written: if a predicate requires data from another predicate, then the two predicates must be combined.

We've already looked at one class of variables that are always public: storage variables. While storage variables allow us to share data between predicates, they are the wrong tool for our use case because they are persistent. What we want is a class of variables that can be shared between predicates but that are temporary. That is, their value should no longer be relevant after a solution is submitted and validated. Pint solves this problem by allow decision variables to be public via the pub keyword.

Declaring Public Decision Variables

Declaring public decision variables is fairly simple. All you have to do is prefix the var declaration with the keyword pub:

predicate Foo {
    pub var x: int;
    pub var y: b256;
    pub var t: { int, bool, b256 };

    var a: int;
    var b: bool;
    var c: int[4];

    constraint a + x > 3;
    constraint y == 0x1111111111111111111111111111111111111111111111111111111111111111;
    constraint !t.1 && b;
}

In the predicate above, we are declaring 3 public decision variables and 3 private decision variables.

Accessing public decision variables within the predicate that defines them is no different from accessing private decision variables. The example above also declares 3 constraints that access both types of decision variables in various ways.

Public Decision Variables in Interfaces

Recall that for each contract, an interface can be produced that exposes all public elements of a contract: the storage block as well as all the predicates and their public decision variables. For example, the following interface can be produced from the contract above:

interface MyInterface {
    // storage block, if present

    predicate Foo {
        pub var x: int;
        pub var y: b256;
        pub var t: { int, bool, b256 };
    }

    // other predicates, if present
}

Note that everything in predicate Foo was dropped except for pub var declarations.

Next, we will show how to use an interface to access public decision variables of an external predicate.

External Access to Public Decision Variables

In Chapter 5.3 we covered how to use interfaces to access storage variables from an external context. Accessing public decision variables from an external context requires similar steps.

First, we need to declare an interface instance using the syntax we learned in Chapter 5.3

    interface MyInterfaceInstance = MyInterface(ContractID);

where ContractID is the address of the contract where the public decision variables are declared. Then, and because the public decision variables live inside a predicate, we need to declare a predicate instance as follows:

    predicate FooInstance = MyInterfaceInstance::Foo(PredicateID);

Similarly to interface instance declarations, a predicate instance declaration requires an address. Each predicate has a 256-bit address that identifies it on the blockchain. The above declares an interface instance called FooInstance of predicate Foo and with address PredicateID. Note that we refer to the predicate Foo in the declaration using the interface instance name followed by ::Foo.

Now that we have an instance of Foo, we are able to access its public decision variables using a path that contains the predicate instance name and the name of the variable:

    var m: int;
    var n: bool;

    constraint m * FooInstance::x > 8;
    constraint FooInstance::y == 0x2222222222222222222222222222222222222222222222222222222222222222;
    constraint FooInstance::t.1 && n;

Public Decision Variables in Solutions

Sharing data between two predicates using public decision variables only makes sense if the solution that we are trying to validate actually solves both predicates. For example, if predicate Foo exposes pub var x; and predicate Bar uses x, then a solution that solves Bar must also solve Foo since Bar requires data from Foo, namely x.

Every solution contains a list of the predicates it solves. Some predicates might even be solved multiple times in the same solution! This may be surprising to you but you can imagine multiple instances of the same predicate being solved with different values. After all, predicates can generally be solved in many different ways depending on how restrictive their constraints are.

As a result, each predicate instance declaration must somehow specify which part of the solution it is referring to. The Pint compiler accomplishes this by adding an implicit decision variable that represents the index of the solved predicate in the solution. An implicit decision variable is added for each predicate instance declaration. Therefore, in the example below:

    interface MyInterfaceInstance = MyInterface(ContractID);
    predicate FooInstance1 = MyInterfaceInstance::Foo(PredicateID);
    predicate FooInstance2 = MyInterfaceInstance::Foo(PredicateID);
    
    var x1 = FooInstance1::x;
    var x2 = FooInstance2::x;

the variables x1 and x2 may not be the same since they may refer to two different values of x in the solution (if Foo is solved multiple times).

Accessing Public Decision Variables From a Sibling Contract

Public decision variables, being public, are also visible from predicates in the same contract as the predicate that declares them. While working within a single contract, you may want one predicate to access another predicate's public decision variables. This can be done, again, using predicate instances. The difference here is that, because we're working in the same contract, there is no need to declare an interface for that contract and an interface instance. There is also no need to specify an address for the predicate instance because the compiler can figure that out on its own! Here's an example:

predicate A {
    pub var x: int;    
}

predicate B {
    predicate AI1 = A();
    predicate AI2 = A();
    constraint AI1::x == AI2::x * 2;
}

Here, AI1 and AI2 are two instances of predicate A which exposes a single public decision variable called x. We are then requiring that the value of x in the first instance is double the value of x in the second instance.

One important caveat of the above is that you are not allowed to have cyclical dependencies between predicates. For example:

predicate A {
    pub var x: int;    

    predicate BI = B();
    constraint BI::y == 69;
}

predicate B {
    pub var y: int;    

    predicate AI = A();
    constraint AI::x == 42;
}

Here, predicate A requires predicate B and predicate B requires predicate A. This causes a cycle where the addresses of a predicate cannot be determined and used by the other. The compiler will emit the following error to prevent you from proceeding:

Error: dependency cycle detected between predicates
   ╭─[ch_7_1_b.pnt:3:1]
   │
 3 │ predicate A {
   │ ─────┬─────
   │      ╰─────── this predicate is on the dependency cycle
   │
10 │ predicate B {
   │ ─────┬─────
   │      ╰─────── this predicate is on the dependency cycle
   │
   │ Note: dependency between predicates is typically created via predicate instances
───╯

Another caveat is that a predicate cannot reference itself:

predicate C {
    pub var x: int;    

    predicate CI = C();
    constraint CI::x == 69;
}

The compiler will complain as follows:

Error: self referential predicate `C`
   ╭─[ch_7_1_c.pnt:6:5]
   │
 6 │     predicate CI = C();
   │     ─────────┬────────
   │              ╰────────── this predicate instance references the predicate it's declared in
───╯

Macros

Macros are a way of writing code that writes other code, which is known as metaprogramming. Metaprogramming is useful for reducing the amount of code you have to write and maintain. Most programming languages have "functions" which somewhat serve a similar purpose. Macros, however, are a lot more powerful. While Pint does not have "functions", its macro system is powerful enough to cover their use case.

Macro expansion is the very first operation performed by the compiler. This property implies that macros can contain anything as long as the code they produce is parsable, i.e. does not violate the grammar of Pint. Later stages of the compiler will then validate the semantics of the code.

Macros in Pint have two main forms:

• Simple Macros: these are macros that accept a fixed number of parameters and do not support recursion.
• Variadic Macros: these are macros that accept a variable number of parameters and can support recursion.

Simple Macros

Simple macros take a fixed number of parameters, each starting with $. Consider the following simple macro:

macro @in_range($v, $num) {
    constraint $v >= $num;
    constraint $v < ($num * $num);
}

Macro definitions always start with the keyword macro followed by the name of the macro, which must start with @. Then, a list of named parameters is provided in between parentheses. The body of the macro is provided in between curly braces and can contain any code that uses the macro parameters.

The macro above is named @in_range and takes 2 parameters named $v and $num. In the body of this macro, these parameters are used as expressions but this is not always necessarily the case! When this macro is used, two constraints are always produced. Let's use this macro as follows:

var x: int;
@in_range(x; 10);

To call the macro, we write its name followed by a list of arguments, separated by a semicolon (;), in between parentheses. The number of arguments must match the number of parameters that the macro expects.

Note: yes, the arguments are separated by a semicolon (;) and not a comma (,).

After the macro gets expanded, the compiler will produce code that is equivalent to the following:

var x: int;
constraint x >= 10;
constraint x < (10 * 10);

It should hopefully be quite clear to you how this substitution happened. The compiler simply rewrote the body of the macro by replacing $v with x and $num with 10. The resulting code is then pasted exactly where the macro was called.

Arbitrary Tokens as Macro Arguments

The arguments to a macro call may be collections of tokens which do not necessarily parse to a proper expression, as in the previous example. For example, an operator like + or a type name such as int are valid!. If the token is an identifier, then it may be used as a name, such as the name of a decision variable or a new type. Here's an example:

macro @do_decls($a, $b, $ty, $op) {
    var $a: $ty;
    var $b: $ty;
    constraint $b $op $a;
}

The author of this macro likely expects:

• $a and $b to be identifiers.
• $ty to be a type.
• op to be a binary operator such as +, -, etc.

In fact, if the rules above are not respected when calling the macro, the program will likely fail to parse correctly resulting in a failed compilation.

If we call the macro above with:

@do_decls(x1; x2; int; >);

the compiler will expand the macro call to:

var x1: int;
var x2: int;
constraint x2 > x1;

Hopefully this gives you an idea of how powerful macros can be.

Macro Expressions

So far, we've only looked at example macros where the body is a list of declarations (such as var declarations or constraints). Macros are even more versatile than that! Macros can, in fact, produce an expression. This would be akin to functions that return values in other programming languages.

The expression that you want produced by the macro must always be the last statement in the macro body. For example:

macro @quotion($a, $b) {
    constraint $b > 0;  // Declaration.
    $a / $b             // Final expression.
}

Because this macro produces an expression, a call to it can be used as an expression as well. For example:

var e: int;
var f: int;
var q: int = @quotion(e; f);

As a result, the compiler will expand the macro call to:

var e: int;
var f: int;
constraint f > 0;
var q: int = e / f;

Note that the expression is always inserted at the exact location where the macro was called, but any declaration items in the macro body are inserted before the call.

Declaring Variables in Macro Bodies

Earlier, we looked at an example macro that uses some of its parameters as identifiers to declare some decision variables. When that macro is called multiple times with different arguments, the resulting var declarations will not cause any name conflicts. Now, what happens if, instead, we were to directly use an identifier in a macro body when declaring new variables? Here's an example:

macro @is_even($a) {
    var half: int;
    constraint $a == half * 2;
}

In a naive macro system, if @is_even was called more than once within the same module, then after expansion there would be multiple half variable declarations, resulting a name clash error.

To avoid this problem Pint's macro expansion aims to be hygienic and places newly declared symbols into a unique anonymous namespace. Note that this is only done for symbols which are not macro parameters. To illustrate this, consider the following:

macro @var_decls($a) {
    var foo: int;       // Hygienic anonymous binding for `foo`.
    var $a: bool;       // Lexical binding for `$a`.
}

If we call the macro above using @let_decls(foo) there would not be an error as the expansion would be equivalent to:

var anon_0::foo: int;
var foo: int;

And even when called multiple times with different arguments there would be no error:

@var_decls(foo);
@var_decls(bar);

Becomes equivalent to:

var anon_0::foo: int;
var foo: int;
var anon_1::foo: int;
var bar: int;

Of course, if @let_decls was called with the argument foo multiple times there would be an error!

Recursion and Variadic Macros

The second type of macros we will look at is "Variadic Macros". Variadic macros allow a special type of recursion via variadic parameters. Such special parameters allow macros to call themselves, essentially entering an expansion loop. Think of this as recursive code generation.

The term "variadic" means that the macro accepts a variable number of parameters. In the parameter list of the macro definition this is indicated using a special parameter whose name starts with an &. Recursion may be performed via one or more recursing macros and at least one non-recursing, or terminating macros. The recursing macros call other versions of itself but with a different number of - usually fewer - arguments. The terminating macros do not call another version of itself. This is best explained with an example, so let's consider the following macro which implements a sum operation over an arbitrary number of named variables:

// Recursive Macro
macro @sum($x, $y, &rest) {
    // Called only when `&rest` is not empty.  
    // We recurse by adding `$x` and `$y` and using `&rest` as the second argument.
    @sum($x + $y; &rest)
}

// Terminating Macro
macro @sum($x, $y) {
    // Called only when the number of arguments is exactly 2.
    $x + $y
}

We have two versions of the @sum macro. Despite the apparent name clash, this is actually okay because the two macros accept a different number of parameters. The first version of @sum accepts $x, $y, and &rest while the second version accepts only $x and $y. The parameter &rest is special and is referred to as a "parameter pack". The parameter pack is never empty, therefore in order to call the first version of @sum, we must pass 3 or more arguments.

Note: The parameter pack is not addressable in any way. It may only be used as an argument to another macro call.

Now let's walk through how the compiler would expand a call to @sum. You will notice that the compiler will always try to match the number of arguments provided to the number of parameters in each macro, and the best match will be selected.

Calling @sum(a; b) will expand directly using the terminating macro to the expression a + b.

Calling @sum(a; b; c; d) will expand as follows:

• @sum(a; b; c; d) calls the recursive macro as @sum(a; b; [c, d]) where [c, d] is &rest.
• @sum(a; b; [c, d]) expands to @sum(a + b; c; d).
• @sum(a + b; c; d) calls the recursive macro again, as @sum(a + b; c; [d]).
• @sum(a + b; c; [d]) expands to @sum(a + b + c; d).
• @sum(a + b + c; d) calls the terminating macro.
• @sum(a + b + c; d) expands to a + b + c + d, which is the final expanded form of the macro call.

Note that, since the &rest parameter pack is passed in its expanded form, the above @sum macros could instead be rewritten as follows, to the same effect:

// Recursive Macro
macro @sum_v2($x, &rest) {
    @sum_v2($x + &rest)
}

// Terminating Macro
macro @sum_v2($x) {
    $x
}

Parameter packs can also be used by non-recursive macros which wish to call other recursive macros. A more interesting use of variadic macros might be to chain variables together in relative constraints:

macro @chain($a, &rest) {
    // Add the first link in the chain, then move to the rest.
    var $a: int;
    @chain_next($a; &rest)
}

macro @chain_next($prev, $next, &rest) {
    // Add the next link, constrain based on the previous link and continue.
    var $next: int;
    constraint $next > $prev + 10;
    @chain_next($next; &rest)
}

macro @chain_next($prev, $last) {
    // Just expand to the final link.
    var $last: int;
    constraint $last > $prev + 10;
    $last
}

When called as var r = @chain(m; n; p), the following code would be produced:

var m: int;
var n: int;
constraint n > m + 10;
var p: int;
constraint p > n + 10;
var r = p;

Array Argument Splicing

An extension to macro argument packing the the concept of array splicing. Array splicing allows passing the elements of an array variable, in place, as the arguments to a macro call. This is done by prefixing the array name with a tilde ~.

Say we want to find the sum of the elements of some array of integers. If we were to use the variadic macro @sum from earlier, we would have to write something like:

var array: int[4];
var sum_of_array = @sum(array[0]; array[1]; array[2]; array[3]);

The issue with the above is that it's quite verbose, especially when the array size is large. Instead, array splicing allows us to write this instead:

var sum_of_array_v2 = @sum(~array);

The compiler will then split array into its individual elements and pass them as separate arguments to @sum, so that the resulting expansion is

var sum_of_array_v2 = @sum(array[0]; array[1]; array[2]; array[3]);

Array splicing is usually only useful with variadic macros which can handle arrays of different sizes, though a non-variadic macro may be called with array splicing if the array size exactly matches the number of required arguments.

An important property of array splicing is that the array element accesses are expanded in place and the argument separators are only placed between them and not at their ends! The following:

var two: int[2];
@foo(~two + ~two + ~two);

expands to:

@foo(two[0]; two[1] + two[0]; two[1] + two[0]; two[1]);

This may be a bit surprising at first, but what is really happening here is that each ~two gets replaced verbatim with two[0]; two[1] and the + signs stay exact where they were. So, the three spliced arrays make up a total of 4 separate arguments in this specific case.

Similarly,

var nums = [1, 2, 3];
constraint @sum(100 + ~nums * 200) < 1000;

expands to:

constraint @sum(100 + nums[0]; nums[1]; nums[2] * 200) < 1000;

The arithmetic add and multiply are applied to the first and last elements of the array in this example.

Pint Reference

Reference docs for the pint command line tool.

• The Command Reference shows the available commands.
• The Manifest Reference provides a description of all manifest fields.

Commands

The following inlines the --help output for each command so that you can get an idea of what pint is capable of prior to downloading the tool and running it yourself.

Overview

$ pint --help
Pint's package manager and CLI plugin host

Usage: pint <COMMAND>

Commands:
  build    Build a package, writing the generated artifacts to `out/`
  new      Create a new package
  plugins  Print all pint plugins found in `PATH`
  help     Print this message or the help of the given subcommand(s)

Options:
  -h, --help     Print help
  -V, --version  Print version

pint build

$ pint build --help
Build a package, writing the generated artifacts to `out/`

Usage: pint build [OPTIONS]

Options:
      --manifest-path <MANIFEST_PATH>
          The path to the package manifest.

          If not provided, the current directory is checked and then each parent recursively until a manifest is found.

  -h, --help
          Print help (see a summary with '-h')

pint new

$ pint new --help
Create a new package

Usage: pint new [OPTIONS] <PATH>

Arguments:
  <PATH>
          The directory path in which the package should be created

Options:
      --contract
          Specify the "contract" package kind.

          This is the default behaviour.

      --lib
          Specify the "library" package kind.

          By default, new packages are created with the "contract" kind.

      --name <NAME>
          Optionally provide a name.

          By default, the package name is the last directory in the canonicalized representation of the given path.

  -h, --help
          Print help (see a summary with '-h')

pint plugins

$ pint plugins --help
Print all pint plugins found in `PATH`

Usage: pint plugins

Options:
  -h, --help  Print help

Manifest

The pint.toml manifest provides a high-level description of a package and its dependencies. All projects built with the pint tool must have a pint.toml manifest file.

The following provides a description of each of the tables and fields within the manifest.

[package]

The package table declares high-level information about the pint package. It includes the following entries:

name

The name of the package.

name = "foo"

license

Optionally specify the license for the package.

license = "MIT"

kind

Describes whether the package is a "contract" (the default) or a "library".

• library packages allow for sharing types, macros and constants between multiple different packages.
• contract packages describe a top-level contract that may be deployed.

kind = "contract"

entry-point

Optionally specify the path to the entry-point module for the package relative to the src/ directory.

By default this is:

• "contract.pnt" for contracts and
• "library.pnt" for libraries.

entry-point = "path/to/my/contract.pnt"

[dependencies]

Describes the list of external library packages that the package depends on.

Library packages allow for sharing types, macros and constants between multiple different packages.

Dependencies are declared as follows:

[dependencies]
<dependency-name-1> = { <source-type> = "<source-value>" }
<dependency-name-2> = { <source-type> = "<source-value>" }
# etc

For example:

[dependencies]
bar = { path = "path/to/bar" }

Source types

Currently only path dependencies are supported, though we plan to support more source types in the future (e.g. git).

package field

By default, the dependency name is assumed to match the name of the package that we're depending on.

In some cases we may want to give a dependency a name that differs from its package name (i.e. if multiple packages have the same name).

We can do this using the package field. In the following, we depend on a package named barney, but give it the dependency name bar:

[dependencies]
bar = { path = "../path/to/bar", package = "barney" }

[contract-dependencies]

Describes the list of external contract packages that the package depends on.

These are similar to [dependencies], however rather than providing a module of items like library dependencies do, contract dependencies only provide the contract's address, along with the address of each of its predicates. E.g.

[contract-dependencies]
baz = { path = "path/to/baz" }

Now in our package, we can refer to baz's content address with the baz::ADDRESS constant. Similarly, if baz has a predicate called Foo, we can access Foo's predicate address with baz::Foo::ADDRESS.

Full Example

The following is an example of a Pint package manifest:

[package]
name = "foo"
license = "MIT"
kind = "contract"
entry-point = "path/to/my/contract.pnt"

[dependencies]
bar = { path = "../relative/path/to/bar", package = "barney" }

[contract-dependencies]
baz = { path = "/absolute/path/to/baz" }

Developer Notes

The pint.toml manifest is implemented in the pint-manifest crate within the pint repostiory. Rust developers looking to build pint-package aware tools or plugins downstream might find this library useful.

Appendix

The following sections contain reference material you may find useful in your Pint journey. Specifically, we will cover the following:

• Keywords: A list of all the keywords in Pint, which are reserved and cannot be used as names of macros, variables, etc.
• Compiler Intrinsics: A list of all available builtin intrinsics in Pint, which can be used to perform low level operations.
• Application Binary Interface (ABI) Spec: A specification of the JSON ABI, which is a condensed representation of a smart contract that only exposes its data.

Appendix A: Keywords

The following list contains keywords that are reserved for current use by the Pint language. As such, they cannot be used as identifiers. Identifiers are names of macros, variables, tuple fields, modules, or types.

• as - perform primitive casting or rename items in use statements
• bool - the Boolean type
• b256 - the 256-bit hash type
• cond - select between multiple expressions based on some conditions
• const -
• constraint - define a Boolean constraint that a proposed solution must satisfy
• else - fallback for if and cond conditionals
• enum - define an enumeration
• exists - existential quantification: checks whether a statements is true for at least one element in a domain.
• false -
• forall - universal quantification: checks whether a statement is true for all elements in a domain
• if - branch based on the result of a conditional expression
• in - checks if an element belongs to a range or to an array
• int - basic integer type
• interface - declare an external interface
• macro - define a macro
• mut - allows a storage location to be mutable
• nil - an empty storage value
• predicate - define a predicate
• pub -
• self - used in use statements
• state - bind a state variable
• storage - declare a storage block
• true -
• type - define a new type
• use - bring symbols into scope
• var - bind a decision variable
• where - denote clauses that constraint generator indices

Appendix B: Compiler Intrinsics

The Pint compiler supports a list of intrinsics that perform various low level operations that are mostly useful for building libraries. Intrinsics are generally target-specific. They give library authors access to VM-specific instructions while preserving type safety. Below is a list of all available compiler intrinsics for the Essential VM:

__this_address() -> b256

Description: Returns the content hash of this predicate.

__this_contract_address() -> b256

Description: Returns the content hash of the contract that this predicate belongs to.

__this_pathway() -> int

Description: Returns the "pathway" of this predicate. The pathway of a predicate is the index of the solution data currently being used to check the predicate.

__predicate_at(pathway: int) -> { b256, b256 }

Description: Returns the full address of predicate at pathway <pathway>. The pathway of a predicate is the index of the solution data currently being used to check the predicate. The full address contains both the content hash of the contract to which the predicate belongs and the content hash of the predicate itself

__address_of(name: string) -> b256

Description: Returns the content hash of predicate named name in the same contract. The name must be the full absolute path to the predicate, such as ::Foo, and cannot be the name of the predicate it's used in.

__sha256(data: _) -> b256

Description: Returns a SHA 256 hash from the specified data.

__state_len(data: _) -> int

Description: Returns the length of a state variable. the argument data must be a state variable or a "next state" expression but can have any type.

__vec_len(vec: _[]) -> int

Description: Returns the length of a storage vector.

__verify_ed25519(data: _, sig: { b256, b256 }, pub_key: b256) -> bool

Description: Validate an Ed25519 signature against a public key.

__recover_secp256k1(data_hash: b256, sig: { b256, b256, int }) -> { b256, int }

Description: Recover the public key from a secp256k1 signature.

Appendix C: Application Binary Interface (ABI) Spec

The Application Binary Interface (ABI) is a condensed representation of a smart contract that exposes enough information about the contract to allow external contexts to interact with it. The ABI does not contain any contract logic but only its data such as its storage variables, its predicates, its decision variables, and so on. The ABI is serialized in JSON format, making it both human readable and easily parsable by relevant tools.

Note This particular ABI specification is mostly relevant for the EssentialVM. Other virtual machines may have different architectures, requiring a completely different ABI format.

JSON ABI Specification

The ABI of a contract is represented as a JSON object containing the following properties:

"storage"

This is an array that describes every storage variable in the contract, i.e., every variable declared in the storage { .. } block. Each entry in this array is a JSON object that contains the following properties:

• "name": a string representing the name of the storage variable.
• "ty": a JSON object representing the type of the storage variable. This is further explained in JSON Representation of Types.

"predicates"

This is an array that describes every predicate in the contract. Each entry in this array is a JSON object that contains the following properties:

• "name": a string representing the name of the predicate.
• "vars": an array that contains every private (i.e. non-pub) decision variable in the contract. Each entry in this array is a JSON object that contains the following properties:
  • "name": a string representing the name of the decision variable.
  • "ty": a JSON object representing the type of the decision variable. This is further explained in JSON Representation of Types.
• "pub_vars": an array that contains every public decision variable in the contract. Each entry in this array is a JSON object that contains the following properties:
  • "name": a string representing the name of the public decision variable.
  • "ty": a JSON object representing the type of the public decision variable. This is further explained in JSON Representation of Types.

Note: The order in which private decision variables show up in the JSON is important and must match the order in which they are declared in the Pint code. When constructing a solution, that same order should also be respected.

JSON Representation of Types

Each possible Pint type is represented in the ABI as a JSON object with properties that depend on the type. Below is a list of the JSON objects for each possible type:

int

"Int"

bool

"Bool"

b256

"B256"

Tuple

{
  "Tuple": [
    {
      "name": <field1_name>,
      "ty": <field1_ty>
    }
    {
      "name": <field2_name>,
      "ty": <field2_ty>
    }
    ...
  ]
}

In the above, <field1_name>, <field2_name>, ... are strings representing the names of the tuple fields. These are optional, that is, they can be set to null if the tuple field has no name. <field1_ty., <field2_ty>, ... are JSON objects representing the types of the tuple fields, formatted according to the rules of this section.

Array

{
  "Array": {
    "ty": <element_ty>,
    "size": <array_size>
  }
}

In the above, <element_ty> is a JSON object representing the type of each element in the array, formatted according to the rules of this section. <array_size> is an integer representing the size of the array.

Storage Map

{
  "Map": {
    "ty_from": <ty_from>,
    "ty_to": <ty_to>,
  }
}

In the above, <ty_from> and <ty_to> are JSON objects representing the "from" type and the "to" type in the map, formatted according to the rules of this section.

Example

Here's an example contract and its corresponding JSON ABI:

storage {
    s0: b256,
    s1: { int, int },
    my_map: ( int => { int, int } ),
}

predicate Foo {
    var v0: int;
    var v1: bool[5];

    pub var t0: { int, int }[5];
    pub var t1: b256[3];
}

{
  "predicates": [
    {
      "name": "::Foo",
      "vars": [
        {
          "name": "::v0",
          "ty": "Int"
        },
        {
          "name": "::v1",
          "ty": {
            "Array": {
              "ty": "Bool",
              "size": 5
            }
          }
        }
      ],
      "pub_vars": [
        {
          "name": "::t0",
          "ty": {
            "Array": {
              "ty": {
                "Tuple": [
                  {
                    "name": null,
                    "ty": "Int"
                  },
                  {
                    "name": null,
                    "ty": "Int"
                  }
                ]
              },
              "size": 5
            }
          }
        },
        {
          "name": "::t1",
          "ty": {
            "Array": {
              "ty": "B256",
              "size": 3
            }
          }
        }
      ]
    }
  ],
  "storage": [
    {
      "name": "s0",
      "ty": "B256"
    },
    {
      "name": "s1",
      "ty": {
        "Tuple": [
          {
            "name": null,
            "ty": "Int"
          },
          {
            "name": null,
            "ty": "Int"
          }
        ]
      }
    },
    {
      "name": "my_map",
      "ty": {
        "Map": {
          "ty_from": "Int",
          "ty_to": {
            "Tuple": [
              {
                "name": null,
                "ty": "Int"
              },
              {
                "name": null,
                "ty": "Int"
              }
            ]
          }
        }
      }
    }
  ]
}

Here's how we would interpret this JSON ABI:

• This contract has a single predicate called ::Foo, which is the full path of the Foo predicate in the contract above.
• Predicate ::Foo has two private decision variables:
  • At index 0, we have ::v0 of type int.
  • At index 1, we have ::v1 of type bool[5].
• Predicate ::Foo has two public decision variables:
  • The first is called ::t0. Its an array of 5 tuples, where each tuple contains two ints with no field names.
  • The second is called ::t1 and is an array of 3 b256s.
• The contract also has three storage variables:
  • The first is called s0 and is of type b256.
  • The second is called s1 and is a tuple of two ints.
  • The third is called my_map and is a storage map from int to a tuple of two ints.