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 program

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() {
    let 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 let 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 5.470625ms
    contract counter            1899743AA94972DDD137D039C2E670ADA63969ABF93191FA1A4506304D4033A2
         └── counter::Increment 355A12DCB600C302FFD5D69C4B7B79E60BA3C72DDA553B7D43F4C36CB7CC0948

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(value: int) {
    let counter: int = mut storage::counter;
    constraint counter' == value;
}

predicate Increment(amount: int) {
    let 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 having a single parameter and declaring two statements. Let's walk through the first predicate named Initialize:

1. Predicate Initialize has a single parameter called value of type int. The parameters of a predicate are essentially decision variables that a solver is required to find values for such that every constraint in the predicate evaluates to true. The expression "decision variable" is commonly used in constraint programming languages to refer to unknowns that a solver must find given some constraints. In Initialize, the parameter value is the value that we want our counter to get initialized to.
2. The second statement declares a local variable and initializes it to mut storage::counter. The statement let counter: int = mut storage::counter creates a local 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 counter must be equal to value. Note the ' notation here which can be only applied to a local 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 parameters of 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:

# parameters:
value: 42

# state mutations:
0: 42

This solution proposes a value of 42 for parameter 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:

# parameters:
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(receiver: b256, amount: int) {
    let receiver_balance = mut storage::balances[receiver];
    let 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(from: b256, receiver: b256, amount: int) {
    let from_balance = mut storage::balances[from];
    let 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 has two parameters receiver: b256 and amount: int. The goal of this predicate to mint amount coins and send them to receiver.
2. It initializes a local 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 local 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 has three parameters 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 local 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, examples of authentication can be found in this Github repository.

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, a list of typed parameters, and a list of constraints. Predicates of a smart contract describe the various ways state can be mutated in order to accomplish certain tasks (e.g. token transfer). 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(
    // parameters 
) {
    // local variables, constraints, etc.     
}

predicate Bar(
    // parameters 
) {
    // local variables, constraints, etc.     
}

// other predicates

The order of the code 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 even though they look like ones!) and nothing is ever "called". Instead, solutions have to submitted that satisfy one or more predicates in the contract. A solution must specify concrete values for the parameters of the solved predicates, as well as propose changes to the state if necessary.

If the proposed values for the parameters and the proposed state changes satisfy all the constraints for each solved predicate (potentially including predicates from other contracts), then the solution is deemed valid and the proposed state changes should be accepted.

Predicate Parameters

A predicate parameter is a named parameter that every solution is required to assign a value for. Predicate parameters are quite different from "regular" function parameters that you might be used to in imperative programming languages since predicates of a smart contract are not called!. Instead, they are solved by proposing values for these parameters such that all the constraints are satisfied.

All predicate parameters have to 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 declare a predicate named test with three parameters foo, bar, and baz with three different types:

predicate test(
    foo: int, 
    bar: bool, 
    baz: b256, 
) {
    constraint foo * foo <= 1024;

    // other constraints
}

The predicate test also declares a constraint that enforces that the square of foo is at most 1024, meaning that any proposed solution must assign a value for foo that satisfies this condition. For example, if foo is set to 7, this is constraint would be satisfied. If foo is set to 42, this constraint would not be satisfied. We will go over constraints in more detail in Chapter 4.6.

You can think of the type annotation on each predicate parameter as an implicit "constraint". For example, parameter foo can only take values in the set of signed integers (64-bit signed integers when targeting the EssentialVM) while bar can only take two values: false or true (i.e. 0 or 1 in the EssentialVM).

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. Another example is invoking external predicates which is a more advanced topic that we will cover in Chapter 7.1.

A contract interface has the following structure:

interface ExternalContract {
    storage {
        // storage variables
    }

    predicate Foo(
        //  parameters
    );

    predicate Bar(
        // parameters     
    );

    // other predicate interfaces 
}

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, each with its own list of typed parameters. The storage block and the predicate signatures of an interface should always match the corresponding storage block and predicate signatures of the deployed contract. Otherwise, correct behavior cannot be guaranteed.

For example, an interface for the counter example looks like this:

interface Counter {
    storage {
        counter: int,
    }

    predicate Initialize(value: int);

    predicate Increment(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 the predicate signatures.

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

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 local variables, basic types, custom types, match constructs, 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.

Local Variables

Local variables in Pint are similar to local variables in other languages with a few restrictions. In Pint, variables must be initialized and are immutable. They basically hold values and help you write readable code, but are not meant to be modified. This is an important property that allows Pint to be fully declarative with no control flow. In Pint, the order in which you write your statements (variable declarations, constraints, etc.) is unimportant and has no impact on the behavior of the code.

In order to declare a new variable, we use the let keyword:

predicate foo() {
    let x = 5;
    let y: int = 6;

    constraint y - x == 1;
}

The first let declares a variable named x and assigns its value to 5. The second let declares a variable named y and assigns its value to 6. The constraint y - x == 1 references x and y using their names and is obviously always true in this case since 6 - 5 == 1.

Note that, while y is annotated with type int, we opted to omit a type annotation for x; we're relying on the compiler to infer its type to be int since the initializing expression is 5 which is an int.

If we were to declare y as follows:

let y: int = true;

then the compiler would emit an error because the type annotation int and the type of the initializing expressions true do not match:

Error: variable initialization type error
   ╭─[variables.pnt:4:18]
   │
 4 │     let y: int = true;
   │            ─┬─   ──┬─
   │             ╰────────── expecting type `int`
   │                    │
   │                    ╰─── initializing expression has unexpected type `bool`
───╯

Shadowing

Name shadowing is not allowed in Pint. Declaring two variables with the same name will result in a compiler error. For example, the following code fails to compile:

let y = 5;
let y: int = 6;

and the following error is emitted:

Error: symbol `y` has already been declared
   ╭─[variables.pnt:4:9]
   │
 3 │     let y = 5;
   │     ────┬────
   │         ╰────── previous declaration of the symbol `y` here
 4 │     let y: int = 6;
   │         ┬
   │         ╰── `y` redeclared here
   │
   │ Note: `y` must be declared or imported only once in this scope
───╯

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 local 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 let statement:

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

// subtraction
let difference = 15 - 1;

// multiplication
let product = 42 * 42;

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

// remainder
let 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:

let t = true;
let 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:

let addr1 = 0x3333333333333333333333333333333333333333333333333333333333333333;
let 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:

let 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:

let tup_2: { int, int, bool } = { 42, 4, true };
let tup_2_first = tup_2.0;
let tup_2_second = tup_2.1;
let 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:

let 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:

let tup_4: { x: int, int, y: bool } = { 42, 4, true };
let tup_4_first = tup_4.0;
let tup_4_first_named = tup_4.x; // same as `tup_4.0`
let tup_4_second = tup_4.1;
let tup_4_third = tup_4.2;
let 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:

let empty: {} = {};

is disallowed and errors out as follows:

Error: empty tuple types are not allowed
    ╭─[data_types.pnt:43:12]
    │
 43 │ let empty: {} = {};
    │            ─┬
    │             ╰── empty tuple type found
────╯
Error: empty tuple expressions are not allowed
    ╭─[data_types.pnt:43:17]
    │
 43 │ let 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:

let 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:

let 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:

let c: int[5] = [1, 2, 3, 4, 5];
let c_first = c[0];
let 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:

let 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
let 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)".

Pint also has match statements that are useful to reason about unions. Both unions and match will be discussed separately in Chapter 3.5

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:

let 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 local 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:

predicate test(number: int) {
    let y = number < 5 ? 1 : true;
}

we will get the following error:

Error: branches of a select expression must have the same type
   ╭─[test.pnt:2:13]
   │
 2 │     let 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:

predicate test(number: int) {
    let y = number ? 1 : 2;
}

we will get the following error:

Error: condition for select expression must be a `bool`
   ╭─[test.pnt:2:13]
   │
 2 │     let 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:

let 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:

let 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 local 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 a union. Unions are another special class of custom types that allow you to define a type by enumerating its possible variants.

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

This chapter covers type aliases and unions. It also covers match expressions and match statements which help reason about unions and their variants.

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:

let x: int = 5;
let 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:

let 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.

Unions

Unions 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, unions 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 a union.

Let’s look at a situation we might want to express in code and see why unions are useful and more appropriate that structs in this case. Say we need to describe token ownership of one of three available tokens on an exchange: DAI, USDC, and USDT. Because these are the only tokens we can work with, we can enumerate them all as different variants:

union 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. Any Token can now be DAI, USDC, or USDT but never 2 or more of these at the same time. That property of Token makes the union data structure appropriate because a union variant can only be one of its variants. All three tokens are still fundamentally tokens, so they should be treated as the same type when the code is handling situations that apply to any of these tokens.

Union Values

We can now create an instance of each of the three variants of Token like this:

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

Note that the variants of the union 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 some token ID:

let token_type: Token = cond {
    token_id == 0 => Token::DAI,
    token_id == 1  => Token::USDC,
    else => Token::USDT,
};

Using unions has even more advantages. Thinking more about our Token type, at the moment we don’t have a way to store the actual token amount; we only know what kind it is. Given what you know about structs and tuples, you might be tempted to tackle this problem with structs as follows:

type Balance = {
    token: Token,
    balance: int,
};

predicate balances_1() {
    let alice_bal: Balance = {
        token: Token::DAI,
        balance: 42,
    };

    let bob_bal: Balance = {
        token: Token::USDC,
        balance: 96,
    };
}

Here, we've defined a new type called Balance that has two fields: a token field that is of type Token (the union we defined previously) and a balance field of type int that represents the balance. We have two instances of this type. The first is alice_bal, and it has the value Token::DAI as its token with associated balance of 42. The second instance is bob_bal. It has another variant of Token as its kind value, Token::USDC, and has a balance of 96 associated with it. We've used a struct to bundle the token and balance values together, so now the variant is associated with the value.

However, representing the same concept using just a union is more concise: rather than a union inside a struct, we can put data directly into each union variant. This new definition of the Token union says that the variants DAI, USDC, and USDT will have associated int values:

union TokenBalance = DAI(int) | USDC(int) | USDT(int);

predicate balances_2() {
    let alice_bal: TokenBalance = TokenBalance::DAI(42);
    let bob_bal: TokenBalance = TokenBalance::USDC(96);
}

We attach data to each variant of the union directly, so there is no need for an extra struct. Also notice the syntax for constructing an instance of the union where the value held by a variant is added between parentheses after the variant name.

There's another advantage to using a union rather than a struct: each variant can have different types and amounts of associated data. Let's look at another example of a union that has a wide variety of types embedded in its variants:

union Action =   Quit                                // Quit the application
               | Buy (TokenBalance)                  // Buy some amount of a token
               | Sell({TokenBalance, price: int})    // sell some amount of a token at some price
               | Swap({TokenBalance, TokenBalance}); // Swap some amount of a token for another amount of some other token

This union has four variants with different types:

• Quit has no data associated with it at all.
• Buy includes a TokenBalance.
• Sell and Swap includes tuples.

Defining a union with variants such as the ones above is similar to defining different kinds of struct definitions, except the union variants are grouped together under the Action type which makes it easier to reason about them as part of a single type.

The match Construct

Pint has the powerful construct match that allows you to inspect a value that has a union type and conditionally execute some code based on which union variant that union value matches. The power of match comes from the introduction of the union variant datum into a specific scope, and the fact that the compiler confirms that all possible variants are handled.

Pint has both match expressions and match statements, the distinction between which is illustrated below.

match as an Expression

Consider the following example which takes an unknown US coin and determines which coin it is and returns its value in cents:

union Coin = Penny | Nickel | Dime | Quarter;

predicate CoinConversion1(coin: Coin) {
    let coin_in_cents = match coin {
        Coin::Penny => 1,
        Coin::Nickel => 5,
        Coin::Dime => 10,
        Coin::Quarter => 25,
    };
}

Let’s break down the match expression above. First we list the match keyword followed by an expression, which in this case is the value coin. This seems very similar to a conditional expression used with cond, but there’s a big difference: with cond, the condition needs to evaluate to a Boolean value, but here it has to be a union variant of Coin because this is the type of the value coin.

Next are the match arms. An arm has two parts: a pattern and some code. The first arm here has a pattern that is the value Coin::Penny and then the => operator that separates the pattern and the code to run. The code in this case is just the value 1. Each arm is separated from the next with a comma.

In this particular example, the code associated with each arm is an expression, and the resultant value of the expression in the matching arm is the value that gets returned for the entire match expression.

It is also possible to include constraints in the match arm code, but you must use curly brackets. For example, the following code requires the Boolean variable is_lucky_penny to be true if the value coin is a Coin::Penny.

predicate CoinConversion2(coin: Coin, is_lucky_penny: bool) {
    let coin_in_cents = match coin {
        Coin::Penny => {
            constraint is_lucky_penny;
            1
        },
        Coin::Nickel => 5,
        Coin::Dime => 10,
        Coin::Quarter => 25,
    };
}

Patterns that Bind to Values

Another useful feature of match arms is that they can bind to the value that match the pattern. This is how we can extract values out of union variants.

As an example, let's change our union variants to hold data inside them. Namely, we want each variant to hold an int that represents the number of coins available:

union Coins = Penny(int) | Nickel(int) | Dime(int) | Quarter(int);

Now, given a value coins of type Coins, we can compute the total number of cents that coins is equivalent to as follows:

predicate CoinConversion3(coins: Coins) {
    let coins_in_cents = match coins {
        Coins::Penny(n) => n,
        Coins::Nickel(n) => n * 5,
        Coins::Dime(n) => n * 10,
        Coins::Quarter(n) => n * 25,
    };
}

In the match expression above, we add a variable called n for each of the patterns. In each pattern, n will bind to the value that the union variant holds. For example, if coins is equal to Coin::Nickel(42), then we expect coins_in_cents to be equal to 42 * 5 == 210.

Note that match expressions can be nested. Here's an example that has nested unions and nested match expressions to compute a prize given a coin and the face it landed on in a head-or-tails game.

union Face = Head | Tail;
union CoinFace =  Penny(Face)
                | Nickel(Face)
                | Dime (Face)
                | Quarter(Face);

predicate CoinGame1(coin: CoinFace) {
    let prize = match coin {
        CoinFace::Penny(f) => match f {
            Face::Head => 100,
            Face::Tail => 200,
        },
        CoinFace::Nickel(f) => 5 * match f {
            Face::Head => 10,
            Face::Tail => 20,
        },
        CoinFace::Dime(f) => 10 * match f {
            Face::Head => 5,
            Face::Tail => 10,
        },
        CoinFace::Quarter(f) => 25 * match f {
            Face::Head => 1,
            Face::Tail => 2,
        },
    };
}

match as a Statement

In some cases, you may not need a match to return a value. Instead, you may simply want to enforce conditional constraints based on which pattern matches the given value. Below is a rewrite of the previous example that uses match statements. The code exhibits the exact same behavior as before but written different to showcase match statements.

predicate CoinGame2(coin: CoinFace, prize: int) {
    match coin {
        CoinFace::Penny(f) => {
            match f {
                Face::Head => {
                    constraint prize == 100;
                }
                Face::Tail => {
                    constraint prize == 200;
                }
            }
        }
        CoinFace::Nickel(f) => {
            if f == Face::Head {
                constraint prize == 5 * 10;
            } else {
                constraint prize == 5 * 20;
            }
        }
        CoinFace::Dime(f) => {
            constraint f == Face::Head ? 10 * 5 : 10 * 10;
        }
        CoinFace::Quarter(f) => {
            constraint prize == 25 * match f {
                Face::Head => 1,
                Face::Tail => 2,
            };
        }
    }
}

Here, the top level match is a statement, not an expression; it does not return any value. Instead, it declares some constraints, each based on one or more conditions. .

• If coin matches CoinFace::Penny(f), then we add another match statement that includes different constraints based on what pattern f matches.
• If coin matches CoinFace::Nickel(f), then we add an if statement that also includes different constraints based on whether f is equal to Face::Head or not.
• If coin matches CoinFace::Dime(f), then we add a single constraint that uses a select expression to compute the prize.
• If coin matches CoinFace::Quarter(f), then we add a single constraint that relies on a match expression.

As shown, nested if statements and match statements are allowed within match statement arms, as are constraint statements.

Matches are Exhaustive

There’s one other aspect of match we need to discuss: the arms’ patterns must cover all possibilities. Consider the following version of variables coins and coins_in_cents previously declared:

let coins_in_cents = match coins {
    Coins::Penny(n) => n,
    Coins::Nickel(n) => n * 5,
    Coins::Quarter(n) => n * 25,
};

We didn't handle the Coins::Dime(n) case, so this code will cause a bug. Luckily, it's a bug the Pint compiler knows how to catch. If we try to compile this code, we'll get this error:

Error: not all match variants are covered
    ╭─[match.pnt:42:26]
    │
 42 │ ╭─▶     let coins_in_cents = match coins {
    ┆ ┆
 46 │ ├─▶     };
    │ │
    │ ╰──────────── not all variants for union `::Coins` are covered by match
    │
    │     Help: branches and/or bindings are required for variant `Coins::Dime`
────╯
Error: could not compile `match.pnt` due to previous error

The Pint compiler knows that we didn't cover every possible case, and even knows which pattern we forgot. Matches in Pint are exhaustive: we must exhaust every last possibility in order for the code to be valid. This is true for both match expressions and match statements!

Catch-all Patterns

In the case where not every variant is significant, match expressions and statements may employ an else arm. It must be declared last and will obviously have no value bound, and is useful to evaluate to a default value for match expressions, or to contain default declarations (or none) for match statements.

To get the above example to compile with a default value of zero, implying any other coins actually have no value, an else may be used as follows:

    let coins_in_cents = match coins {
        Coins::Penny(n) => n,
        Coins::Nickel(n) => n * 5,
        Coins::Quarter(n) => n * 25,
        else => 0,
    };

The code compiles, even though we haven't listed all the possible values a Coins can have, because the last pattern will match all values not specifically listed. This catch-all pattern meets the requirement that match must be exhaustive.

Constraints

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

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 statements, then all of them must be satisfied for a solution to be valid. For example:

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 statement that is hard to read and maintain.

As mentioned above, the expression of a constraint statement 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 parameter to be solved or variable to be computed. 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(foo: int, 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 predicate parameter variables nor other non-constant values.

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(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.

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:

union TokenBalance = DAI(int) | USDC(int) | USDT(int);
storage {
    x: int,
    bal: int,
    a: b256,
    t: { int, bool },
    y: bool,
    w: int,
    arr: { int, int }[3],
    v: { int, { bool, b256 } },
    u: TokenBalance,
}

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 several variables with different primitive and compound types. Similarly to predicate parameters, storage variables 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 predicate parameters or local 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:

let a = storage::a;
let t = storage::t;
let t_1 = storage::t.1;
let arr_2_1: int = storage::arr[2].1;

let x = storage::x;
let incremented = storage::x + 1;

constraint incremented == x + 1; // always true!

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 in the initializer of a local variable. In fact, storage read expressions can only ever be used in initializers of local variables. Using a storage read expression in other contexts, such as in constraint storage::x == 5, is currently 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.
4. Arbitrary expressions that include storage read expressions can also be used to initialize local variables. Variable incremented is an example of that.

Note that, while storage read expressions cannot be evaluated at compile time, they 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 used in the corresponding local variable initializer expression 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 local variables, that means "the future value of". Here's an example:

let bal = mut storage::bal;
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 predicate parameter 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).

The ' operator can also be used for variables that have arbitrary initializers. For example:

let bal_in_dollars = price * mut storage::bal;
constraint bal_in_dollars' == price * bal'; // always true!

Basically, when validating a solution, bal_in_dollars' is computed by plugging in the new value of storage::bal into the expression price * storage::bal. That is, a valid solution must satisfy bal_in_dollars' == price * bal' where bal_in_dollars is computed in this way (this just happens to be always true in this case!).

As you can imagine, using the ' operator for variables that do not depend on storage accesses is a no-op. For example

let z = 42;
constraint z' == z; // always true

"Mutable" Storage Accesses

In the previous section, you may have noticed that we added the mut keyword before storage::bal in the declaration of bal. 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::bal, 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:

let 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,

let w = mut storage::w;
let value_1 = (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 initialize value_1 to 0. Otherwise, we initialize 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 fail causing a panic in the VM.

The following is also a valid approach for handling nil checks:

let value_2 = (mut storage::w == nil) ? 0 : storage::w;
constraint value_2 == value_1; // always true!

It is also possible to update a 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. Storage 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 Storage Map

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

let from_balance = storage::balances[from_address];
let 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, they must be used in the initializers of some local 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):

let my_bal = mut storage::balances[my_address];
constraint my_bal' == my_bal + 1_000_000;

Here, we are 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 deploying 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 + 1_000_000;
} else {
    constraint my_bal' == 1_000_000;
}

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 is fairly intuitive and is exactly what you'd expect:

predicate foo(addr1: b256) {
    let complex_read: b256 = storage::complex_map[{42, 69}].1;

    let 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(addr: b256, my_map: (int => bool)) {
    let nested_map: (b256 => (int => bool)) = storage::nested_map;
    let nested_map_inner: (int => bool) = storage::nested_map[addr];
}

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

Error: predicate parameters cannot have storage types
   ╭─[bad.pnt:7:28]
   │
 7 │ predicate test(addr: b256, my_map: (int => bool)) {
   │                            ──────────┬──────────
   │                                      ╰──────────── found parameter of storage type ( int => bool ) here
───╯
Error: local variables cannot have storage types
   ╭─[bad.pnt:8:5]
   │
 8 │     let nested_map: (b256 => (int => bool)) = storage::nested_map;
   │     ──────────────────────────────┬──────────────────────────────
   │                                   ╰──────────────────────────────── found local variable of storage type ( b256 => ( int => bool ) ) here
───╯
Error: local variables cannot have storage types
   ╭─[bad.pnt:9:5]
   │
 9 │     let nested_map_inner: (int => bool) = storage::nested_map[addr];
   │     ───────────────────────────────┬───────────────────────────────
   │                                    ╰───────────────────────────────── found local variable of storage type ( int => bool ) here
───╯

Hopefully the error messages are clear enough. What the compiler is telling us here is that we cannot have predicate parameters or local 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.

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 to be 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.

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 a 256-bit value that uniquely identify the contract on the blockchain. Specifying the address is required because multiple contracts with different implementations may share the same interface.

Recall the interface of the counter example that we presented earlier:

interface Counter {
    storage {
        counter: int,
    }

    predicate Initialize(value: int);

    predicate Increment(amount: int);
}

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

const ContractID: b256 = 0x6D05CB94739FFB92CA96750EBF262A82C3ED8F05262DD26B503D732F0B74777E;

In order to access storage variable counter from interface Counter, we can create a path to conter as follows:

let counter = Counter@[ContractID]::storage::counter;

The path Counter@[ContractID]::storage::counter has three parts separated by :::

1. The name of the interface Counter followed by the address of the corresponding deployed contract in between @[..].
2. The keyword storage to indicate that we're accessing the storage block of Counter.
3. counter, the name of the storage variable we want to access.

We can now use the local variable counter as usual. For example, we can constrain it as follows:

constraint counter' >= 100;

This implies that we want that new value of the counter (which is owned by the external contract) to be at least 100. This could be accomplished in different ways:

1. If the current value of the counter is at least 100, then nothing needs to be done. We don't even need to propose a solution for any predicates in the external contract.
2. If the current value of the counter is less than 100, then the solution must:
   1. Either solve predicate Initialize with parameter value set to 100 or more.
   2. Or solve predicate Increment with parameter amount set to 100 - counter or more.

Similarly to local storage access expressions, the expression Counter@[ContractID]::storage::counter can only be used in the right-hand side of a let 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.pnt 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.pnt 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.pnt 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.pnt
        └── vegetables.pnt

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

use garden::vegetables::Asparagus;

predicate Foo(green_asparagus: Asparagus) {
    constraint green_asparagus == Asparagus::Green;
}

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

union 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(
    first_asparagus: ::garden::vegetables::Asparagus,
    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 the parameter 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(
    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,
    parameters: 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(
    contract_data: contract_lib::Data,
    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(
    contract_data: ContractData,
    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:

• Invoking Predicates: how to invoke external local and external predicates.
• Macros: how to write reusable code using macros.

Invoking Predicates

If you've worked with imperative smart contract languages like Solidity in the past, you know that interactions between smart contracts are essential for many applications. One way to do this is by calling one contract from another contract. Pint has a similar concept where one predicate can invoke another predicate with some arguments. We use the word "invoke" here instead of "call" because, unlike imperative languages, predicates in Pint are not called in the traditional sense since that would imply the existence of a control flow (a "call" followed by a "return"). Instead, in Pint, predicate A can invoke predicate B with some arguments to indicate that B has to be present in the solution with this particular set of arguments, if A is also present in the solution. If this sounds confusing, don't worry. It will all be clear by the end of this chapter.

We cover two types of predicate invocations:

1. External predicate invocation.
2. Sibling predicate invocation.

Invoking External Predicates

Similar to accessing external storage, a predicate in an external contract can be invoked through an interface declaration corresponding to the external contract. When invoking the external predicate, the following are needed:

1. The address of the external contract.
2. The address of the predicate we want to access in that contract.
3. A list of arguments.

Consider the following external smart contract that we would like interact with:

predicate foo(
    x: int,
    y: bool,
    t: { int, bool },
) {
    // predicate logic
}

// other predicates

To interact with this contract, we first need to generate its interface:

interface MyInterface {
    predicate foo(
        x: int,
        y: bool,
        t: { int, bool },
    );

    // other predicates
}

Now, we can invoke predicate foo as follows:

const CONTRACT_ADDR = 0xEB87FCE275A9AB10996D212F39221A56B90E01C37FA9D16EE04A3FE8E17DEED9;
const FOO_ADDR = 0xBA6595C5C75346E6C82BED0CE770D0758ADD1712163FCE45E38E5E8EAC6AA153;

predicate bar(
    a: int,
    b: bool,
) {
    let tuple = { 42, b };
    constraint MyInterface@[CONTRACT_ADDR]::foo@[FOO_ADDR](a, true, tuple);
}

The predicate invocation expression has three parts separated by :::

1. The name of the interface MyInterface followed by the address of the corresponding deployed contract in between @[..]. This is quite similar to what we had to do to access external storage variables.
2. The name of the predicate foo followed by the address of the corresponding predicate in the deployed contract.
3. A list of arguments that must match the list parameters of foo in the interface.

In the above, the constraint:

    constraint MyInterface@[CONTRACT_ADDR]::foo@[FOO_ADDR](a, true, tuple);

can be interpreted as follows: any solution that solves predicate bar must also contain a solution for predicate foo such that:

1. The address of foo is FOO_ADDR.
2. The address of the contract that contains foo is CONTRACT_ADDR.
3. The arguments provided for foo in the solution are equal to a, true, and tuple respectively.

Of course, for foo to be actually satisfied, the containing contract must exist and be deployed, the addresses must be correct, and the arguments must match (in number and types) what the deployed bytecode of foo actually expects.

Invoking Sibling Predicates

A special case for invoking predicates is when the invoked predicate is in the same contract as the predicate that is invoking it. There is no conceptual difference between this special case and the generalized case above expect that, because we are working in the same contract, there is no need to declare an interface for the contract. There is also no need to specify the address of the invoked predicate because the compiler can figure that out on its own! Here's an example:

predicate A(
    a: { bool, int },
    b: bool,
    c: int[3], 
) {
    // predicate logic
}

predicate B() {
    constraint A@[]( { true, 42 }, false, [1, 2, 3]);
}

Here, predicate B invokes sibling predicate A by using its path (just A) and empty square brackets @[] to indicate that the address is to be computed by the compiler. The constraint constraint A@[](..) should be interpreted exactly as in the case of external predicate invocation: any solution that solves B should also contain a solution for A with the provided listed arguments.

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

predicate A(x: int) {
    constraint B@[](0);
}

predicate B(y: int) {
    constraint A@[](0);
}

Here, predicate A invokes predicate B and predicate B invokes predicate A. This causes a cycle where the address 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
   ╭─[invoking_predicates_3.pnt:1:1]
   │
 1 │ predicate A(x: int) {
   │ ─────┬─────
   │      ╰─────── this predicate is on the dependency cycle
   │
 7 │ predicate B(y: int) {
   │ ─────┬─────
   │      ╰─────── 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(x: int) {
    constraint C@[](x);
}

The compiler will complain as follows:

Error: self referential predicate `::C`
   ╭─[invoking_predicates_4.pnt:2:16]
   │
 2 │     constraint C@[](x);
   │                ───┬───
   │                   ╰───── this predicate call 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 expanded 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:

let x = 42;
@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:

let x = 42;
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, $a_expr, $b, $b_expr, $ty, $op) {
    let $a: $ty = $a_expr;
    let $b: $ty = $b_expr;
    constraint $b $op $a;
}

The author of this macro likely expects:

• $a and $b to be identifiers.
• $a_expr and $b_expr to be expressions.
• $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; 42; x2; 69; int; >);

the compiler will expand the macro call to:

let x1: int = 42;
let x2: int = 69;
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 let 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:

let e: int = 4;
let f: int = 2;
let q: int = @quotion(e; f);

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

let e: int = 4;
let f: int = 2;
constraint f > 0;
let 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 right 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 local variables. When that macro is called multiple times with different arguments, the resulting variable 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) {
    let half: int = $a / 2;
    constraint $a == half * 2 || $a == half * 2 + 1;
}

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 @let_decls($a) {
    let foo: int = 42;     // Hygienic anonymous binding for `foo`.
    let $a: bool = true;   // 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:

let anon@0::foo: int = 42;
let foo: bool = true;

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

@let_decls(foo);
@let_decls(bar);

Becomes equivalent to:

let anon@0::foo: int = 42;
let foo: bool = true;
let anon@1::foo: int = 42;
let bar: bool = true;

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 array accesses together in relative constraints:

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

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

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

When called as:

predicate chain(array: int[4]) {
    let r = @chain(array; 0; 1; 2; 3);
}

The following code would be produced:

predicate chain(
    array: int[4],
) {
    let r = array[3];
    constraint (array[1] > (array[0] + 10));
    constraint (array[2] > (array[1] + 10));
    constraint (array[3] > (array[2] + 10));
}

Array Argument Splicing

An extension to macro argument packing is 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:

let 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:

let 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

let 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:

@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,

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.

Debugging Macros

The easiest way to debug macros is to inspect the code they expand to and compare the result to your expectations. The way to do this is using flag --print-parsed as follows:

pint build --print-parsed

For example, consider the following contract:

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

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)
}

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

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

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

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

predicate test4(x: int, array: int[4]) {
    @in_range(x; 10);
    let sum_of_array = @sum(array[0]; array[1]; array[2]; array[3]);
    let r = @chain(array; 0; 1; 2; 3);
}

Building this contract with the flag --print-parsed results in the following:

$ pint build --print-parsed
   Compiling to_debug [contract] (/path/to/to_debug)
   Printing parsed to_debug [contract] (/path/to/to_debug)


predicate ::test4(
    ::x: int,
    ::array: int[4],
) {
    let ::sum_of_array = (((::array[0] + ::array[1]) + ::array[2]) + ::array[3]);
    let ::r = ::array[3];
    constraint (::x >= 10);
    constraint (::x < (10 * 10));
    constraint (::array[1] > (::array[0] + 10));
    constraint (::array[2] > (::array[1] + 10));
    constraint (::array[3] > (::array[2] + 10));
}

    Finished build [debug] in 8.914417ms
    contract to_debug        2C7EF76D670086B5A3FA185490A8C596043319A1AA8AC496B9DCF0043B8101F5
         └── to_debug::test4 2E4456C7268C180898A0CE5C4C3F0445D613AD79A0E6E73CF8319F8B2C3EFB3B

which has no macro calls left! The compiler has already expanded all the macro calls and inlined the resulting code in the appropriate locations.

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.

      --salt <SALT>
          A 256-bit unsigned integer in hexadeciaml format that represents the contract "salt". The value is left padded with zeros if it has less than 64 hexadecimal digits.

          The "salt" is hashed along with the contract's bytecode in order to make the address of the contract unique.

          If "salt" is provided for a library package, an error is emitted.

      --print-parsed
          Print the parsed package

      --print-flat
          Print the flattened package

      --print-optimized
          Print the optimized package

      --print-asm
          Print the assembly generated for the package

      --silent
          Don't print anything that wasn't explicitly requested

  -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
• let - declare a local variable
• macro - define a macro
• match - match a value to patterns
• mut - allows a storage location to be mutable
• nil - an empty storage value
• predicate - define a predicate
• self - used in use statements
• storage - declare a storage block
• true -
• type - define a new type
• union - declare a new union
• use - bring symbols into scope
• 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:

__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.

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

Description: Recover the public key from a secp256k1 signature.

__sha256(data: _) -> b256

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

__size_of(data: _) -> int

Description: Returns the size, in words, of an expression. This is often the same as the size of the type of the expression (e.g. 1 word for int, 4 words for b256, 3 words for {int, int, bool}, and so on). However, it can also be different, namely for expressions that can be nil such as storage accesses and paths to local variables.

__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.

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

Description: Validate an Ed25519 signature against a public key.

Appendix C: Application Binary Interface (ABI)

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 public data such as its storage variables and its predicates. 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.

In this chapter, we will cover the following:

1. The ABI specification.
2. How to construct solutions using the ABI.

Appendix C.1: Application Binary Interface (ABI) Specification

In this chapter, we will cover the specification of the Application Binary Interface (ABI) and provide an example that showcase how the final ABI looks like in JSON 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.
• "params": an array that contains the parameters of the predicate. Each entry in this array is a JSON object that contains the following properties:
  • "name": a string representing the name of the parameter.
  • "ty": a JSON object representing the type of the parameter. This is further explained in JSON Representation of Types.

Note: The order in which the predicate parameters 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"

Union

{
  "Union": {
    "name": <union_name>,
    "variants": [
      {
        "name": <variant1_name>,
        "ty": <variant1_ty>
      },
      {
        "name": <variant2_name>,
        "ty": <variant2_ty>
      },
      ...
    ]
  }
}

In the above, <variant1_name>, <variant2_name>, ... are strings representing the names of the union variants. <variant1_ty>, <variant2_ty>, ... are JSON objects representing the types of the tuple fields, formatted according to the rules of this section. These are optional, that is, they can be set to null if the corresponding variants don't hold any values.

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 corresponding tuple fields have no names. <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:

union U = A(int) | B | C(int[3]);

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

predicate foo(
    v0: int,
    v1: bool[5],
    v2: U,
    v3: { int, int }[5], 
) {
}

{
  "predicates": [
    {
      "name": "::foo",
      "params": [
        {
          "name": "::v0",
          "ty": "Int"
        },
        {
          "name": "::v1",
          "ty": {
            "Array": {
              "ty": "Bool",
              "size": 5
            }
          }
        },
        {
          "name": "::v2",
          "ty": {
            "Union": {
              "name": "::U",
              "variants": [
                {
                  "name": "U::A",
                  "ty": "Int"
                },
                {
                  "name": "U::B",
                  "ty": null
                },
                {
                  "name": "U::C",
                  "ty": {
                    "Array": {
                      "ty": "Int",
                      "size": 3
                    }
                  }
                }
              ]
            }
          }
        },
        {
          "name": "::v3",
          "ty": {
            "Array": {
              "ty": {
                "Tuple": [
                  {
                    "name": null,
                    "ty": "Int"
                  },
                  {
                    "name": null,
                    "ty": "Int"
                  }
                ]
              },
              "size": 5
            }
          }
        }
      ]
    }
  ],
  "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"
              }
            ]
          }
        }
      }
    },
    {
      "name": "my_union",
      "ty": {
        "Union": {
          "name": "::U",
          "variants": [
            {
              "name": "U::A",
              "ty": "Int"
            },
            {
              "name": "U::B",
              "ty": null
            },
            {
              "name": "U::C",
              "ty": {
                "Array": {
                  "ty": "Int",
                  "size": 3
                }
              }
            }
          ]
        }
      }
    }
  ]
}

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 three parameters:
  • At index 0, we have ::v0 of type int.
  • At index 1, we have ::v1 of type bool[5].
  • At index 2, we have ::v2 of type U which is a union with three variants U::A, U::B, and U::C.
  • At index 3, we have ::v3. It's an array of 5 tuples, where each tuple contains two ints with no field names.
• The contract also has four 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.
  • The fourth is called my_union and is a union with three variants U::A, U::B, and U::C.

Appendix C.2: Constructing Solutions using the ABI

The Application Binary Interface (ABI) of a contract provides all the essential information needed to construct a solution for one or more predicates within the contract. Although you could perform this manually, the pint-abi crate makes it much more ergonomic in Rust. The pint-abi crate includes the gen_from_file macro, which automatically generates the modules, types, and builder methods required to accomplish this.

The gen_from_file Macro

Consider the following simple contract in Pint:

storage {
    s_x: int,
    s_y: bool,
    s_z: {int, b256},
    s_a: {bool, int}[2],
    s_u: MyUnion,
    m1: (int => b256),
    m2: (int => (int => {bool, int})),
}

union MyUnion = A(int) | B;

predicate MyPredicate(
    x: int,
    y: bool,
    z: {int, b256},
    a: {bool, int}[2],
    u: MyUnion,
) {
    // Check arguments
    constraint x == 42;
    constraint y == true;
    constraint z == {2, 0x1111111100000000111111110000000011111111000000001111111100000000};
    constraint a == [{true, 1}, {false, 2}];
    constraint u == MyUnion::A(3);

    let s_x = mut storage::s_x;
    let s_y = mut storage::s_y;
    let s_z = mut storage::s_z;
    let s_a = mut storage::s_a;
    let s_u = mut storage::s_u;
    let m1_42 = mut storage::m1[42];
    let m2_5_6 = mut storage::m2[5][6];

    // Update state
    constraint s_x' == 7;
    constraint s_y' == true;
    constraint s_z' == {8, 0x2222222200000000222222220000000022222222000000002222222200000000};
    constraint s_a' == [{false, 3}, {true, 4}];
    constraint s_u' == MyUnion::B;
    constraint m1_42' == 0x3333333300000000333333330000000033333333000000003333333300000000;
    constraint m2_5_6' == {true, 69};
}

If you have pint-abi added as dependency in your Rust project, you'll have access to the gen_from_file macro which can be called as follows:

#![allow(unused)]
fn main() {
pint_abi::gen_from_file! {
    abi: "abi_gen_example/out/debug/abi_gen_example-abi.json",
    contract: "abi_gen_example/out/debug/abi_gen_example.json",
}
}

The macro takes two arguments:

1. abi: a path to the ABI of the contract in JSON format
2. contract: a path to the bytecode of the contract in JSON format

The macro above expands to a set of modules, types, and builder methods that allow creating data for solutions directly using Rust types without having to do the encoding manually.

In order to construct a solution to a predicate, you need construct two vectors:

1. A vector of all the predicate arguments.
2. A vector of all the state mutations.

Predicate Arguments

In order to construct a vector of arguments for the predicate above, you can use the following syntax:

#![allow(unused)]
fn main() {
    let arguments = MyPredicate::Vars {
        x: 42,
        y: true,
        z: (2, [0x1111111100000000; 4]),
        a: [(true, 1), (false, 2)],
        u: MyUnion::A(3),
    };
}

The module MyPredicate (which clearly corresponds to the predicate MyPredicate in our contract above) and the struct Vars are readily available to us from the expansion of the gen_from_file macro. The fields of the struct Vars exactly match the list of parameters of MyPredicate, both in name and type.

Each predicate parameter Pint type has a corresponding Rust type as follows:

State Mutations

In order to construct a vector of proposed state mutations for the contract above, you can use the following syntax:

#![allow(unused)]
fn main() {
    let state_mutations: Vec<essential_types::solution::Mutation> = storage::mutations()
        .s_x(7)
        .s_y(true)
        .s_z(|tup| tup._0(8)._1([0x2222222200000000; 4]))
        .s_a(|arr| {
            arr.entry(0, |tup| tup._0(false)._1(3))
                .entry(1, |tup| tup._0(true)._1(4))
        })
        .s_u(MyUnion::B)
        .m1(|map| map.entry(42, [0x3333333300000000; 4]))
        .m2(|map| map.entry(5, |map| map.entry(6, |tup| tup._0(true)._1(69))))
        .into();
}

The module storage and the function mutations() are readily available for us from the expansion of the gen_from_file macro. The resulting object is of type Vec<essential_types::solution::Mutation> from the essential_types crate.

Because all state mutations are optional, they need to be set individually using their own builder methods (unlike predicate arguments). For simple types like int, bool, b256, and unions, the syntax is self explanatory. Those types have corresponding Rust types as for predicate arguments:

For more complex types like tuples, arrays, and storage maps, you need to provide closures that specify how to set each part of the compound type:

1. For tuples, you have available the builder methods _0(..), _1(..), etc. that specify a value for each individual entry of the tuple. you may skip some of these methods if you do not want to propose any mutations to the corresponding tuple field.
2. For arrays, you have the builder method entry(..) which takes an integer index and a value to set the array value at that particular index. Not all array indices need to be set.
3. For storage maps, you also have the builder method entry(..) which takes a key and a value to set the map value at that particularly key. The types of the key and the value must match the types of the key and the value of the map.

Contract and Predicate Addresses

The expansion of the macro gen_from_file also provides the address of the contract and the address of each predicate as constants:

#![allow(unused)]
fn main() {
    let contract_address = ADDRESS;
    let my_predicate_address = MyPredicate::ADDRESS;
}

These constants can be used to construct solutions when specifying what predicate is being solved.

Producing Solutions

We now have everything we need to produce a solution. When working with the EssentialVM, a Solution object can be constructed as follows:

#![allow(unused)]
fn main() {
    let solution = essential_types::solution::Solution {
        data: vec![essential_types::solution::SolutionData {
            predicate_to_solve: MyPredicate::ADDRESS,
            decision_variables: arguments.into(),
            state_mutations,
        }],
    };
}

where we have used the address of the MyPredicate to specify which predicate to solve, the vector arguments to specify values for decision_variables (recall that we sometimes refer to predicate parameters as decision variables), and the vector state_mutations to specify the proposed state mutations.

Note that this solutions only has a single SolutionsData. In general, solutions may contain multiple SolutionData objects which can all be produced by following the steps above.

Storage Keys

It is sometimes useful to know the storage keys where a particular storage variable (or some of its parts) are stored. The expansion of the gen_from_file macro also provides the builder method storage::keys() which can be used as follows:

#![allow(unused)]
fn main() {
    let keys: Vec<essential_types::Key> = storage::keys()
        .s_x()
        .s_y()
        .s_z(|tup| tup._0()._1())
        .s_a(|arr| {
            arr.entry(0, |tup| tup._0()._1())
                .entry(1, |tup| tup._0()._1())
        })
        .s_u()
        .m1(|map| map.entry(42))
        .m2(|map| map.entry(5, |map| map.entry(6, |tup| tup._0()._1())))
        .into();
}

The method keys() is readily available in the module storage. Similarly to mutations(), the key(s) for each storage variable must be appended using the corresponding builder method and the syntax is fairly similarly to the builder methods for state mutations. The result is a vector of Keys which can be used to query the state for example.

Appendix D: Storage Keys Assignment

In the Essential VM, contract storage is organized as a key-value map, where both keys and values can consist of an arbitrary number of 64-bit words. In Pint, storage variables declared within storage { .. } blocks are implemented using this key-value structure. This appendix explains how the Pint compiler determines storage keys based on the types of storage variables.

Primitive Types and Unions

Primitive types and unions are always stored in a single storage slot with a single key. The key chosen has a single word which is equal to the index of the variable in the storage block.

Arrays and Tuples

Arrays and tuples are flattened and spread out across multiple consecutive slots such that each slot contains a primitive type or a union. The key for each slot consists of two words. The first word is the index of the tuple or array variable in the storage block and the second word is the index of the tuple field or array element in the flattened list.

Storage Maps

Entries of storage maps are stored in one or more storage slots depending on their types:

Primitive Types and Unions in Storage Maps

Primitive types and unions in a storage map are stored in a single storage slot with a single key. The key chosen has two components. The first component (1 word) is the index of the storage map in the storage block and the second component is storage map key (which can have multiple words).

Arrays and Tuples in Storage Maps

Arrays and tuples in storage maps are flattened and spread out across multiple consecutive slots such that each slot contains a primitive type or a union. The key for each slot consists of three components. The first component (1 word) is the index of the storage map in the storage block, the second component is storage map key (which can have multiple words), and the third component (1 word) is the tuple field or array element in the flattened list.

Nested Types

Nested types in storage adhere to the outlined rules above recursively. For instance, in the case of nested maps, the storage key is constructed by appending map keys at each level, followed by handling the inner type according to the same rules. This process is illustrated more clearly in the example below.

Example

Consider the following storage block:

union MyUnion = A | B({ int, b256 });

storage {
    x: int,
    y: bool,
    z: b256,
    u: MyUnion,
    c: { int[3], { b256, bool }},
    m1: ( int => int ),
    m2: (int => { b256, ({ int, int } => { int, b256 }) }),
}

In the above, here are some storage accesses and the corresponding storage keys according to the rules laid out above.

Note that the keys produced by the storage::keys() abstraction explained in the Storage Keys from the Appendix C.2 follow the same rules above and will produce the exact same keys.

Appendix E: Known Issues and Missing Features

Known Issues

• #913: type checker sometimes misses type errors in const initializers.

Missing Features

• Strings
• Dynamic arrays, i.e., array types where the size is a value that is not known at compile time.
• Morphisms such that map, fold, filter, etc. that will allow morphing arrays.
• Storage vectors