The Noir Programming Language

This version of the book is being released with the public alpha. There will be a lot of features that are missing in this version, however the syntax and the feel of the language will mostly be completed.

What is Noir?

Noir is a domain specific language for creating and verifying proofs. Design choices are influenced heavily by Rust.

What's new about Noir?

Noir is much simple and flexible in design as it does not compile immediately to a fixed NP-complete language. Instead Noir compiles to an intermediate language which itself can be compiled to an arithmetic circuit or a rank-1 constraint system. This in itself brings up a few challenges within the design process, but allows one to decouple the programming language completely from the backend. This is similar in theory to LLVM.

Who is Noir for?

Noir can be used for a variety of purposes.

Ethereum Developers

Noir currently includes a command to publish a contract which verifies your Noir program. This will be modularised in the future, however as of the alpha you can use the contract command to create it.

Protocol Developers

As a protocol developer, you may not want to use the Aztec backend due to it not being a fit for your stack or maybe you simply want to use a different proving system. Since Noir does not compile to a specific proof system, it is possible for protocol developers to replace the PLONK based proving system with a different proving system altogether.

Blockchain developers

As a blockchain developer, you will be constrained by parameters set by your blockchain, ie the proving system and smart contract language has been pre-defined. In order for you to use Noir in your blockchain, a proving system backend must be implemented for it and a smart contract interface must be implemented for it.

Getting Started

In this section we will discuss, installing Noir and running your first program.

Installing Noir

There are two ways to install Noir; from source or from the compiled binary.

Installing Noir from Source

  • Download Rust

  • Now download Noir from Github using Git.

  • cd into the Noir Github directory, then into the nargo directory and use cargo install --locked --path=. to compile the binary and store it in your path.

Before using the cargo install command, you should see a Cargo.toml file.

Installing Noir from the Compiled Binary

  • First navigate to the Github repo for Noir.

  • Click on the Releases tab.

  • Three compiled binaries will be listed named; Linux, MacOS and Windows. Download the binary for your operating system.

  • Add the downloaded binary to your path.

Hello, World

Now that we have installed Noir, it's time to make our first hello world program!

Creating a Project Directory

Noir code can live anywhere on your computer. Lets create a Projects folder in the Home to house our Noir programs.

For Linux, macOS, and PowerShell on Windows, enter this in your terminal:

$ mkdir ~/projects
$ cd ~/projects

For Windwows CMD, enter this:

> mkdir "%USERPROFILE%\projects"
> cd /d "%USERPROFILE%\projects"

Compiling Our First Project

Now that we are in the projects directory, enter the following command:

nargo new hello_world

We use the new command to create a new Noir project. This project will be located in the hello_world folder.

Now cd into the hello_world folder and enter this:

$ nargo build

Now that the project is built, we need to create a proof of correct execution. Edit the file Prover.toml with the following content:

x = "1"
y = "2"

Now you can run the proof generation and verification commands:

$ nargo prove my_proof
$ nargo verify my_proof
true

Congratulations, you have now created and verified a proof for your very first Noir program!

In the next section, we will go into more detail on exactly what just happened.

Breakdown

This section breaks down our hello world program in section 1.2. We elaborate on the project structure and what the prove and verify commands did in the previous section, and usage of the contract command.

Anatomy of a Nargo Project

Upon using the new command, Nargo will create a Noir project.

Noir Projects have the following structure:

- src
- Prover.toml
- Verifier.toml
- Nargo.toml

contract and proofs directories will not be immediately visible until you create a contract or proof respectively.

Source directory

This directory holds the source code for your Noir program.

Inside of the src directory will be a single file:

- main.nr

main.nr

The main.nr file contains a main method, this method is the entry point into your Noir program.

In our sample program, main.nr looks like this:

fn main(x : Field, y : Field) {
    constrain x != y;
}

The parameters x and y can be seen as the API for the program and must be supplied by the prover. Since neither x nor y is marked as public, the verifier does not supply any inputs, when verifying the proof.

The prover supplies the values for x and y in the Prover.toml file.

Prover.toml

The Prover.toml file is a file which the prover uses to supply his witness values(both private and public).

In our hello world program the Prover.toml file looks like this:

x = "5"
y = "10"

When the command nargo prove my_proof is executed, two processes happen:

  • First, Noir creates a proof that x which holds the value of 5 and y which holds the value of 10 is not equal.This not equal constraint is due to the line constrain x != y.

Note: We have not expanded on the meaning of the syntax constrain x != y as it is not the focus of this chapter.

  • Second, Noir creates and stores the proof of this statement in the proofs directory and names the proof file my_proof. Opening this file will display the proof in hex format.

Verifying a Proof

When the command nargo verify my_proof is executed, two processes happen:

  • Noir checks in the proofs directory for a file called my_proof

  • If that file is found, the proof's validity is checked.

Note: The validity of the proof is linked to the current Noir program; if the program is changed and the verifier verifies the proof, it will fail because the proof is not valid for the modified Noir program.

Contract

This directory holds the compiled Ethereum contract for the current Noir program. The contract is not automatically compiled when the prove or verify command is ran. To compile execute the following:

Note: At the time of pre-alpha, Nargo supports only one backend which is Aztec-Barretenberg. This backend only allows you to compile from a Noir program to an Ethereum contract. It is possible for Noir to compile to another smart contract platform as long as the backend supplies an implementation.

$ nargo contract

TornadoCash

Let's show an example of the TornadoCash circuit in Noir.

fn main(message : [62]u8, index : Field, hashpath : [40]Field, root : Field) {

    priv leaf = std::hash::hash_to_field(message);

    priv is_member = std::merkle::check_membership(root, leaf, index, hashpath);

    constrain is_member == 1;
}

The TornadoCash circuit involves a merkle membership proof that a leaf is in a merkle tree.

The above code uses the noir standard library to call both of the aforementioned components.

   priv leaf = std::hash::hash_to_field(message);

The message is hashed using hash_to_field. The specific hash function that is being used is chosen by the backend. The only requirement is that this hash function can heuristically be used as a random oracle. If only collision resistance is needed, then one can call std::hash::pedersen instead.

    priv is_member = std::merkle::check_membership(root, leaf, index, hashpath);

The leaf is then passed to a check_membership proof with the root, index and hashpath. is_member returns 1 if the leaf is a member of the merkle tree with the specified root, at the given index.

Note: It is possible to re-implement the merkle tree implementation without standard library. However, for most usecases, it is enough. In general, the standard library will always opt to be as conservative as possible, while striking a balance between efficiency.

An example, the merkle membership proof, only requires a hash function that has collision resistance, hence a hash function like Pedersen is allowed, which in most cases is more efficient than the even more conservative sha256.

    constrain is_member == 1;

This last line, constrains the variable to be equal to 1. If 1 was changed to 0, this would create a proof that the leaf was not present at that specific index for that specific root. Importantly, it would not prove that this leaf was not in the merkle tree.

Language Concepts

In this chapter, we will go over the concepts that are being used in Noir. Specifically, we will learn about types, control flow, comments, functions and declarations. For some concepts, we also explain the rationale as to why they were designed in this particular way. Recurring themes you will encounter in this section are simplicity and safety.

Mutability

All variables in Noir are immutable and cannot be made mutable. Due to this, Noir will at some stages borrow functional programming concepts.

Why immutability?

Witnesses in a proving system are immutable in nature. Noir aims to closely mirror this setting without applying additional overhead to the user. If a developer encounters a variable a he can lookup its definition to deduce its value.

The last section may be somewhat invalidated, if temporary scopes and shadowing is introduced.

Data types

There are two subsets of data types that each datatype will fall into; fundamental and compound.

A fundamental type is a data type which is defined in the core language. This is not specific to Noir. Examples in modern programming languages such as Rust are u32, usize and char.

A compound type is a type in the core language which must be defined using another type. Examples in modern programming languages are arrays, tuples and functions.

Although each value in a constraint system is fundamentally a field element, we add a layer of abstraction over this; each value can be concealed or revealed.

A concealed value is known only to the Prover, while, a revealed value is known by the Prover and Verifier. All concealed and revealed values are fundamental types.

Fundamental Types

Concealed Types

Concealed types are generally referred to as witnesses.

Witness Type

A Witness type is the default concealed type. Here's an example that shows declaration and usage of the Witness type.

fn main(x : Field, y : Field) {
    priv z = x + y;
}

x, y and z are Witness types. Using the priv keyword we derived a new Witness type z which is constrained to be equal to x + y.

Integer Type

An integer type is a witness type which has been constrained using a range constraint. The Noir front-end currently supports arbitrary sized integer types.

Below we show the integer type in action:

fn main(x : Field) {
    priv y = x as u24;
}

x and y are both concealed types, however y is an integer type. If y exceeds the range \([0,2^{24}-1]\) then any proof created will output false by the verifier.

Note: The Aztec backend only supports even sized integer types currently, so while using the Aztec backend, only even sized integer types such as u32, u48 will produce proofs.

Revealed Types

Constants

A constant type is a value that does not change per circuit instance. This is different to a concealed type which changes per proof. If a constant type that is being used in your program in changed, then your circuit will also change.

Below we show how to declare a constant value:

fn main() {
    const a = 5;
}

Public Types

A public type is a value that may change per circuit instance. Unlike Constants, changing a public value will not change the circuit.

fn main(x : pub Field) {

}

As of the beta release, public types can only be declared through type parameters. In the code, they are treated no differently to witness types.

Note: This behaviour and type will change in future releases, to catch a linearity bug in user code.

Compound Types

Compound types are declared using the let keyword. Currently arrays are the only supported compound type.

Arrays

An array is a data structure which allows you to group together data types. All values in an array must be of the same type; homogeneous.

fn main(x : Field, y : Field) {
    let my_arr = [x, y];
}

Example: An array of Witness types cannot be grouped together with an array of Integer types.

Functions

Functions in Noir follow the same semantics of Rust, Noir does not support early returns.

To declare a function the fn keyword is used.

fn foo() {}

All parameters in a function must have a type and all types are known at compile time. The parameter is pre-pended with a colon and the parameter type. Multiple parameters are separated using a comma.

fn foo(x : Field, y : pub Field){}

The return type of a function can be stated by using the -> arrow notation. The function below states that the foo function must return a Witness. If the function returns no value, then the arrow is omitted.

fn foo(x : Field, y : pub Field) -> Field {
    x + y
}

Call Expressions

Calling a function in Rust is executed by using the function name and passing the necessary arguments the function header.

Below we show how to call the foo function from the main function using a call expression:

fn main(x : Field, y : Field) {
    priv z = foo(x);
}

fn foo(x : Field) -> Field {
    x + x
}

Comments

A comment is a line in your codebase which the compiler ignores, however it can be seen read by programmers.

Here is a single line comment:

// This is a comment and is ignored

// is used to tell the compiler to ignore the whole line.

A multi-line comment can be made by including // on each line

// This is a multi line
// comment, that is ignored by 
// the compiler

Control Flow

Loops

Noir has one kind of loop, the for-loop. For loops allow you to repeat a block of code multiple times.

The following block of code between the braces is ran 10 times.

for i in 0..10 {
    // do something
}

For loops are expressions, so each iteration of the loop produces a value which is collected into an array.

The following code produces an array of 10 values, each element contains the same values from 0 to 9.

let my_arr = for i in 0..10 {
    i
};

If Expressions

Currently, these are not supported in the language.

Operations

Table of Supported Operations

OperationDescriptionRequirements
+Adds two concealed types togetherTypes must be concealed
-Subtracts two concealed types togetherTypes must be concealed
*Multiplies two concealed types togetherTypes must be concealed
/Divides two concealed types togetherTypes must be concealed
^XOR two concealed types togetherTypes must be integer
&AND two concealed types togetherTypes must be integer
<constrains one value to be less than the otherUpper bound must have a known bit size
<=constrains one value to be less than or equal to the otherUpper bound must have a known bit size
>constrains one value to be more than the otherUpper bound must have a known bit size
>=constrains one value to be more than or equal to the otherUpper bound must have a known bit size
==constrains one value to be equal to the otherBoth types must not be constants
!=constrains one value to not be equal to the otherBoth types must not be constants

Predicate Operators

<,<=, !=, == , >, >= are known are predicate/comparison operations because they compare two values. This differs from the operations such as + where the operands are used in computation.

Bitwise Operations Example

fn main(x : Field) {
    priv y = x as u32;
    priv z = y & y;
}

z is implicitly constrained to be the result of y & y. The & operand is used to denote bitwise &.

x & x would not compile as x is a Witness and not an integer type.

Constrain Statement

Noir includes a special keyword constrain which will explicitly constrain the expression that follows, as long as the operation is a predicate/comparison.

Constrain statement example

fn main(x : Field, y : Field) {
    constrain x == y
}

The above snippet compiles because == is a predicate operation. Conversely, the following will not compile:

fn main(x : Field, y : Field) {
    constrain x + y
}

The rationale behind this not compiling is due to ambiguity. It is not clear if the above should equate to x + y == 0 or if it should check the truthiness of the result.

Modules, Packages, Crates

In this section, we describe the package, crate and module system. As mentioned in the introduction, this will largely follow the design choice chosen by Rust.

Crate

A crate is the compilation unit used in Noir.

Crate Root

Every crate has a root, which is the source file that the compiler starts, this is also known as the root module. The Noir compiler does not enforce any conditions on the name of the file which is the crate root, however if you are compiling via Nargo. The Crate Root, must be called lib.nr or main.nr.

Packages

A Nargo Package is a collection of one of more crates. A Package must include a Nargo.toml file.

A Package must contain either a library or a binary crate.

Creating a new package

A new package is created using the new command.

$ nargo new my-project
$ ls my-project
Nargo.toml
src
$ ls my-project/src
main.nr

Binary vs Library

Similar to Cargo, Nargo follows the convention that if there is a src/main.nr then the project is a binary. If it contains a src/lib.nr then it is a library.

However, note that dissimilar to Cargo, we cannot have both a binary and library in the same project.

Modules

Noir's module system follows the same convention as the newer version of Rust's module system.

Purpose of Modules

Modules are used to organise files. Without modules all of your code would need to live in a single file. In Noir, the compiler foes not automatically scan all of your files to detect modules. This must be done explicitly by the developer.

Examples

Importing a module in the crate root

Filename : src/main.nr

mod foo;

fn main() {
    foo::hello_world();
}

Filename : src/foo.nr

fn from_foo() {}

In the above snippet, the crate root is the src/main.nr file. The compiler sees the module declaration mod foo which prompts it to look for a foo.nr file.

Visually this module hierarchy looks like the following :

crate
 ├── main
 │
 └── foo
      └── from_foo
      

Sub-modules

Filename : src/main.nr

mod foo;

fn main() {
    foo::from_foo();
}

Filename : src/foo.nr

mod bar;
fn from_foo() {}

Filename : src/foo/bar.nr

fn from_bar() {}

In the above snippet, we have added an extra module to the module tree; bar. bar is a submodule of foo hence we declare bar in foo.nr with mod bar. Since foo is not the crate root, the compiler looks for the file associated with the bar module in src/foo/bar.nr

Visually the module hierarchy looks as follows:

crate
 ├── main
 │
 └── foo
      ├── from_foo
      └── bar
           └── from_bar

Dependencies

Nargo allows you to upload packages to GitHub and use them as dependencies.

Specifying a dependency

hello_world = { tag = "v0.5", git = "https://github.com/kevaundray/hello-world-noir"}

Specifying a dependency requires a tag to a specific commit and the git url to the url containing the package.

Currently, there are no requirements on the tag contents. If requirements are added, it would follow semver 2.0 guidelines.

Note: Without a tag , there would be no versioning and dependencies would change each time you compile your project.

ACIR (Abstract Circuit Intermediate Representation)

The purpose of ACIR is to act as an intermediate layer between the proof system that Noir chooses to compile to and the Noir syntax. This separation between proof system and programming language, allows those who want to integrate proof systems to have a stable target, moreover it allows the frontend to compile to any ACIR compatible proof system.

ACIR additionally allows proof systems to supply a fixed list of optimised blackbox functions that the frontend can access. Examples of this would be SHA256, PEDERSEN and SCHNORRSIGVERIFY.

Features Coming Soon

If Statement / Ternary Expression

It is possible to emulate conditional branching with a multiplexer in Noir as of writing. However, this may not be intuitive for most. This can be sugared with an if statement or a ternary expression.

Structures

Currently only primitives types are available. This does not hinder expressiveness, however for large circuits, readability will be harmed without structs.

Isize

Signed integers such as i32 and i64 allow one to express more circuits.

Recursion

Recursion is becoming feasible in circuits, hence Noir will have native support for it. Currently, only composition is supported.

LICENSE

Noir will be dual licensed under MIT/Apache (Version 2.0).