Blocksense Noir

At Blocksense, we’ve enhanced the Noir programming language and compiler with advanced tools designed to simplify and strengthen the creation of secure, verifiable circuits. Our current prototypes include:

Noir time-travel debugging in the CodeTracer environment;
formal verification of Noir circuits, based on the Z3 SMT solver and the IR language of the Verus project; and
Noir compilation support for the PLONKY2 proof system.

All of these developments are expected to reach a production-ready status in the future. We plan on merging them with the upstream codebase as soon as they are accepted by the Noir team.

The Blocksense Noir compiler follows the development of upstream Noir closely and it should be fully compatible.

Noir FV overview

We at Blocksense have created a tool for verifying the correctness of code written in Noir. Building upon Microsoft's open-source verification framework Verus, we're able to prove functional correctness of constrained code, before it is ever ran! Noir FV introduces no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable code will always satisfy some user-provided specifications for all possible inputs.

Constrained Noir is not Turing-complete which simplifies proof writing. Noir’s deterministic nature eliminates the need for complex clauses which appear in other formal verification systems (like invariants and decrease clauses). Alongside the absence of a heap, we see Noir as a strong candidate for formal verification.

This guide

Noir FV reuses Noir's syntax and type system to express specifications for executable code. Basic proficiency with the language is assumed by this guide. Noir's documentation can be found here.

Code specification needs to be written according to a number of predetermined rules, using clauses like forall and requires. Of course, you'll also need to grasp and conform to the required rigor for creating, what is effectively, a mathematical proof. It can be challenging to prove that a Noir function satisfies its postconditions (its ensures clauses) or that a call to a function satisfies the function’s preconditions (its requires clauses).

Therefore, this guide’s tutorial will walk you through the various concepts and techniques, starting with relatively simple concepts (e.g., basic properties about integers), progressing to moderately difficult challenges, and eventually covering advanced topics like proofs about arrays using forall and exists.

All of these proofs are supported by an automated theorem prover (specifically, Z3, a satisfiability-modulo-theories solver, or “SMT solver” for short). The SMT solver will often be able to prove simple properties, such as basic properties about booleans or integer arithmetic, with no additional help from the programmer. However, more complex proofs often require effort from both the programmer and the SMT solver. Therefore, this guide will also help you understand the strengths and limitations of SMT solving, and give advice on how to fill in the parts of proofs that SMT solvers cannot handle automatically.

Getting Started

Installation

NOTE: This installation requires more than 20GBs of drive memory.

First, fetch the source code from our Noir Github fork:

git clone https://github.com/blocksense-network/noir.git -b formal-verification

Nix-powered machines with direnv only need to do:
```
cd noir
direnv allow
cargo build
```

Nix-powered machines without direnv have to do the following:

cd noir
nix develop
cargo build
export PATH=$PATH:$PWD/target/debug

For other systems, you will need to have rustup installed. Follow those instructions:

git clone https://github.com/blocksense-network/Venir.git

pushd Venir
export RUSTC_BOOTSTRAP=1
cargo build
export LD_LIBRARY_PATH="${HOME}/.rustup/toolchains/1.76.0-x86_64-unknown-linux-gnu/lib:${LD_LIBRARY_PATH}"
export PATH=$PATH:$PWD/target/debug
popd

pushd noir
mkdir lib
popd

git clone https://github.com/Aristotelis2002/verus-lib.git

pushd verus-lib/source/
pushd tools
./get-z3.sh
export VERUS_Z3_PATH=$PWD/z3
popd
export RUSTC_BOOTSTRAP=1
export VERUS_IN_VARGO=1
export RUSTFLAGS="--cfg proc_macro_span --cfg verus_keep_ghost --cfg span_locations"
cargo build
cargo run -p vstd_build -- ./target/debug/
cp ./target/debug/vstd.vir ../../noir/lib/
popd

pushd noir
cargo build
export PATH=$PATH:$PWD/target/debug

If you encounter any issues, refer to our Github discussions. If it's not listed, don't hesitate to report it—we're happy to assist

Running Noir FV

Let's first create a Noir project in a new directory:

nargo new my_project
cd my_project

Now, let's try running Noir FV on the following simple Noir program. Copy the following in src/main.nr:

#[requires(x >= 100)]
#[ensures(result >= 20)]
fn main(x: u32) -> pub u32 {
    let y = x / 5;
    y
}

To formally verify the code run the following command while inside of the project directory:

nargo fv

If the verification is successful, you should see the following output:

Verification successful!

Specifications

Noir FV programs contain specifications (in the form of annotations) above all functions to define the intended behavior of the code. These specifications include preconditions, postconditions and assertions. Specifications are a form of ghost code — instructions that appear in the Noir program for verification purposes, but are not included in the compiled executable.

This chapter covers the syntax and usage of these specifications through basic examples of preconditions, postconditions, and assertions.

Pre- and postconditions

Preconditions ("requires" annotations)

Let’s start with a simple example. Suppose we want to verify a function main that multiplies a number by 4:

fn main(x1: i8) -> pub i8 {
    let x2 = x1 + x1;
    x2 + x2 
}

If we run nargo fv to verify the code we will get the following output:

error: possible arithmetic underflow/overflow
  ┌─ src/main.nr:2:14
  │
2 │     let x2 = x1 + x1;
  │              --------
  │

Error: Verification failed!

Noir FV cannot prove that the result of x1 + x1 fits in an i8 value, i.e. is in the range -128…127. For example, if x1 were 100, then x1 + x1 would be 200, which exceeds 127. We need to make sure that the argument x1 stays within a safe range.

We can do this by adding preconditions (also known as requires annotations) to main specifying which values for x1 are allowed. Preconditions are written using Noir's attributes syntax and they have a boolean body expression which can utilize the function's arguments:

#[requires(-64 <= x1 & x1 < 64)]
fn main(x1: i8) -> pub i8 {
    let x2 = x1 + x1;
    x2 + x2 
}

The precondition above says that x1 must be at least -64 and less than 64, so that x1 + x1 will fit in the range -128…127. This fixes the error about x1 + x1, but we still get an error about x2 + x2:

error: possible arithmetic underflow/overflow
  ┌─ src/main.nr:4:5
  │  
4 │ ╭     x2 + x2
5 │ │ }
  │ ╰'
  │  

Error: Verification failed!

If we want both x1 + x1 and x2 + x2 to succeed, we need a stricter bound on x1:

#[requires(-32 <= x1 & x1 < 32)]
fn main(x1: i8) -> pub i8 {
    let x2 = x1 + x1;
    x2 + x2 
}

Now the code verifies successfully!

Checking Preconditions at Call Sites

Let's rename the function main to quadruple. Now suppose we try to call quadruple with a value that does not satisfy quadruple's precondition.

fn main() {
    let n = quadruple(40);
}

For this call Noir FV reports an error, since 40 is not less than 32:

error: precondition not satisfied
  ┌─ src/main.nr:1:12
  │
1 │ #[requires(-32 <= x1 & x1 < 32)]
  │            -------------------- failed precondition
  │

Error: Verification failed!

If we pass 25 instead of 40, verification succeeds:

fn main() {
    let n = quadruple(25);
}

Postconditions ("ensures" annotations)

Postconditions allow us to specify properties about the return value of a function. Let’s revisit the quadruple function and verify that its return value is indeed four times the input argument. Let's try putting an assertion in main to check that quadruple(10) returns 40:

fn main() {
    let n = quadruple(10);
    assert(n == 40);
}

Although quadruple(10) does return 40, Noir FV nevertheless reports an error:

error: assertion failed
   ┌─ src/main.nr:10:12
   │
10 │     assert(n == 40);
   │            -------- assertion failed
   │

Error: Verification failed!

The error occurs because, even though quadruple multiplies its argument by 4, quadruple doesn’t publicize this fact to the other functions in the program. To do this, we can add postconditions (ensures annotations) to quadruple specifying some properties of quadruple’s return value. In Noir FV, the return value is referred with the variable name result:

#[requires(-32 <= x1 & x1 < 32)]
#[ensures(result == 4 * x1)]
fn quadruple(x1: i8) -> pub i8 {
    let x2 = x1 + x1;
    x2 + x2 
}

With this postcondition, Noir FV can now prove that quadruple behaves as intended. When main calls quadruple, the SMT solver uses the postcondition to verify the assertion n == 40.

Modular Verification

Preconditions and postconditions enable modular verification, a key feature of Noir FV. This approach establishes a clear contract between functions:

When main calls quadruple, Noir FV checks that the arguments satisfy quadruple’s preconditions.
When verifying quadruple’s body, Noir FV assumes the preconditions hold and ensures the postconditions are satisfied.
When verifying main, Noir FV relies on quadruple’s postconditions without needing to inspect its implementation.

This modularity breaks verification into smaller, manageable pieces, making it more efficient than verifying the entire program at once. However, writing precise preconditions and postconditions requires effort. For large programs, you’ll likely spend significant time crafting these specifications to ensure correctness.

Assert and SMT Solvers

During verification with nargo fv, the assert keyword is used to make local requests to the SMT solver (Z3) to prove a specific fact. Importantly, Noir's assert behaves differently depending on whether you’re running nargo fv (verification) or nargo execute (execution).

Quantifiers

Logical implication

To improve readability, Noir FV supports the implication operator ==>. The expression a ==> b (reads as “a implies b”) is logically equivalent to !a | b.

For example, the expression:

forall|i, j| (0 <= i) & (i <= j) & (j < len) ==> f(i, j)

means that for every pair i and j such that 0 <= i <= j < len, f(i, j) must hold.

Note that ==> has lower precedence than other Boolean operators. For instance, a ==> b & c is interpreted as a ==> (b & c).

Forall

Suppose we need to specify that all the elements of an array are powers of 2. If the array is small, we could write a specification for every element separately:

fn is_power_of_2(x: i32) -> bool {
  if x <= 0 { 
      false
    } else {
      (x & (x - 1)) == 0
    }
}

#[requires(is_power_of_2(arr[0]))]
#[requires(is_power_of_2(arr[1]))]
#[requires(is_power_of_2(arr[2]))]
#[ensures(is_power_of_2(result))]
fn main(arr: [i32; 3]) -> pub i32 {
    arr[1]
}

However, this approach doesn't scale well for larger arrays.

Fortunately, Noir FV and SMT solvers support the universal(forall) and existential(exists) quantifiers, which we can think of as infinite conjunctions or disjunctions:

forall(|i| f(i)) = ... f(-2) & f(-1) & f(0) & f(1) & f(2) & ...
exists(|i| f(i)) = ... f(-2) | f(-1) | f(0) | f(1) | f(2) | ...

By default the bound variables (i in forall|i|) are of type int, representing all mathematical integers, both positive and negative. The SMT solver contains direct support for reasoning about int values.

With quantifiers, it's much more convenient to write a specification about all elements of an array:

#[requires(
    forall(|i|
     (0 <= i) & (i < 3) ==> is_power_of_2(arr[i])
    ))]
#[ensures(is_power_of_2(result))]
fn main(arr: [i32; 3]) -> pub i32 {
    arr[1]
}

Exists

exists expressions are the dual of forall. While forall(|i| f(i)) means that f(i) is true for all i, exists(|i| f(i)) asserts that f(i) holds for at least one i. To prove exists(|i| f(i)), an SMT solver has to find one value for i such that f(i) is true. This value is called a witness for exists(|i| f(i)).

The following example demonstrates how exists successfully finds a witness

#[requires(is_power_of_2(arr[0]))] // Potential witness
#[requires(!is_power_of_2(arr[1]))]
#[requires(is_power_of_2(arr[2]))] // Potential witness
#[ensures(exists(|i| (0 <= i) & (i < 3) ==> is_power_of_2(result[i])))] // i is going to be either 0 or 2
fn main(arr: [i32; 3]) -> pub [i32; 3] {
    arr
}

This verification succeeds because at least one element (arr[0] or arr[2]) is a power of 2, allowing exists to identify a witness.

Ghost Functions

In many formal verification systems, there is a strict separation between code for mathematical proofs and for execution. Some systems, like Verus, introduce explicit "ghost functions"—special functions used purely for proofs and omitted from compiled code. Others, like Prusti, allow calling regular functions inside specifications without requiring them to be ghost functions.

Noir FV does not have ghost functions. Instead, we prioritize executable code while ensuring that functions used in specifications are pure—they must have no side effects and always return the same output for the same input.

The traditional approach of using ghost functions, proofs, and lemmas has its benefits, especially for reasoning about complex systems like distributed systems. However, it also has drawbacks, such as reduced code reusability and increased mathematical complexity, which can make the verification process less user-friendly.

With Noir FV, we take a different path—focusing on executable code and usability. Our approach simplifies formal verification, making it more intuitive without compromising rigorous correctness guarantees.

Recursion and loops

Noir FV streamlines formal verification by eliminating the need for loop invariants and termination proofs.
Unlike traditional frameworks that rely on techniques like induction, decrease clauses, and invariants to prove correctness for recursive functions and loops, constrained Noir avoids these complexities altogether.

Why?

No Recursion – Noir does not support recursion, eliminating the need for termination proofs.
Bounded Loops – All loops in constrained Noir have fixed bounds, meaning they always terminate.

Example: Verifying a Loop

The following Noir function increments sum in a loop and successfully verifies without needing invariants:

#[requires((0 <= x) & (x <= y) 
    & (y < 1000000))] // Prevent overflow when adding numbers
fn main(x: u32, y: u32) {
    let mut sum = y;
    for i in 0..100 {
        sum += x;
    }
    assert(sum >= y);
}

Since sum is always increasing and x is non-negative, the assertion sum >= y holds for all valid inputs. Noir FV can verify this automatically without requiring additional annotations.

Recursion

In Noir FV you can prove statements for recursive functions but this is not beneficial because programs with recursion can not be built by the standard Noir compiler.

Additional Features

Noir FV supports formal verification for structures, tuples, and generic functions, enabling proofs for more complex data types and abstractions. These features are seamless—no additional syntax, complex attributes, or overhead is required.

Verifying Structs

Example: Verifying a Student’s Scholarship Eligibility

This program returns true if the student is qualified for a scholarship.

global MIN_GRADE: u8 = 8;
global MAX_GRADE: u8 = 10;

struct Student {
    id: Field,
    grade: u8,
}

// Returns true if the student qualifies for the scholarship 
#[requires(student.grade <= MAX_GRADE)] // Max possible grade
#[ensures(student.grade >= MIN_GRADE ==> result == true)]
#[ensures(student.grade < MIN_GRADE ==> result == false)]
fn main(student: Student) -> pub bool{
    student.grade >= MIN_GRADE
}

Verifying Traits and Generic Functions

Example: Verifying a Banking System

This example defines a BankAccount trait and verifies that different account types correctly implement it. We are receiving as arguments two types of accounts. They have in common a value amount and we want to sum them.

trait BankAccount {
  fn get_amount(self) -> u64;
}

struct NamedAccount {
  name: str<10>,
  amount: u32,
}

impl BankAccount for NamedAccount {
  #[ensures(result == self.amount as u64)]
  fn get_amount(self) -> u64 {
    self.amount as u64
  }
}

struct AnonymousAccount {
  encrypted_id: Field,
  amount: u32,
}

impl BankAccount for AnonymousAccount {
  #[ensures(result == self.amount as u64)]
  fn get_amount(self) -> u64 {
    self.amount as u64
  }
}

#[ensures(result == (first_account.amount as u64 + second_account.amount as u64) )]
fn main(first_account: NamedAccount, second_account: AnonymousAccount) -> pub u64 {
  sum_accounts(first_account, second_account)
}

#[ensures(result == first.get_amount() + second.get_amount())]
fn sum_accounts<T, U>(first: T, second: U) -> pub u64 
where T: BankAccount,
      U: BankAccount,
{
  first.get_amount() + second.get_amount()
}

Specification syntax

Noir FV specifications are a superset of Noir's Boolean expressions. The key extensions are summarized below:

Syntax	Meaning
`result`	Return value of the function
`... ==> ...`	Right implication
`forall(...)`	Universal quantifier
`exists(...)`	Existential quantifier

`result` Variable

In Noir FV, the special variable result refers to the return value of a function. It can only be used in postconditions (ensures annotations) and must not be used as a regular function parameter name.

Here is an example for returning an integer:

#[ensures(result == 8)]
fn eight() -> i32 {
    8
}

And an example for returning a tuple and accessing individual fields:

#[ensures((result.0 / -2 == result.1.0 as i32) & (result.1.1 == 0))]
fn main() -> pub (i32, (u32, u32)) {
    (-8, (4, 0))
}

Noir Boolean Expressions

Noir does not support the standard logical operators || (OR) and && (AND). Instead, it uses the bitwise operators | and &, which function the same way for Boolean values but do not short-circuit.

One implication of this is the need for additional parentheses to ensure the correct order of operations, as bitwise operators follow different precedence rules.

Type Checking in Annotations

Noir FV enforces type checking within annotation expressions. While this ensures consistency, it may sometimes produce errors that seem unintuitive, especially to users familiar with other formal verification systems.

In some cases, you may need to add explicit type casts to satisfy the type checker. When doing so, always prefer upcasting (from smaller integer type to larger one) rather than downcasting (from larger integer type to smaller one), as downcasting can result in loss of information, leading to incorrect verification results. While downcasting may allow the type checker to accept an expression, it can introduce unintended behavior that prevents the verifier from proving correctness.

Example: Why Upcasting is Necessary

Consider the following function::

#[requires(x >= y)]
#[ensures(result == y + 1)]
fn main(x: u16, y: u32) -> pub u32 {
    y + 1
}

Attempting to verify this code results in a type error:

error: Integers must have the same bit width LHS is 16, RHS is 32
  ┌─ src/main.nr:1:12
  │
1 │ #[requires(x >= y)]
  │            -----
  │

Error: Aborting due to 1 previous error

To fix the error, we might attempt a downcast, converting y to u16:

#[requires(x >= y as u16)]
#[ensures(result == y + 1)]
fn main(x: u16, y: u32) -> pub u32 {
    y + 1
}

However, this leads to a formal verification failure:

error: possible arithmetic underflow/overflow
  ┌─ src/main.nr:4:3
  │  
4 │ ╭   y + 1
5 │ │ }
  │ ╰'
  │  

Error: Verification failed!

This failure is expected. If y were max(u32) = 4,294,967,295, downcasting it to u16 would result in y = 65,535, which is the maximum possible u16 value. This allows for a scenario where x = 65,535 and y = 4,294,967,295, making the precondition (x >= y as u16) true. However, adding 1 to y would cause an overflow.

Instead of downcasting y, the correct approach is to upcast x to match y's bit width::

#[requires(x as u32 >= y)]
#[ensures(result == y + 1)]
fn main(x: u16, y: u32) -> pub u32 {
    y + 1
}

After running nargo fv:

Verification successful!

Limitations

As a prototype, Noir FV has certain limitations and does not yet support some features of Noir. The following features are currently unsupported:

Mutable references as function parameters
Lambda functions
Standard library functions
Unconstrained functions
Vectors (Vec<T>)
Optional types (Option<T>)

These limitations may change as Noir FV evolves.

These examples show the errors produced when using unsupported features in Noir FV.

Mutable Reference Parameters

fn main() {
    let mut x = 5;
    nullify(&mut x);
    assert(x == 0);
}

fn nullify(x: &mut u32) {
  *x = 0;
}

Output after running nargo fv:

Error: Verification crashed!

Lambda Functions

#[ensures(result == x / 2)]
fn main(x: u32) -> pub u32 {
  let divide_by_2 = |val| val / 2; // Lambda function
  divide_by_2(x)
}

Output:

error: postcondition not satisfied
  ┌─ src/main.nr:1:11
  │
1 │ #[ensures(result == x / 2)]
  │           ---------------- failed this postcondition
  │

Error: Verification failed!

Standard Library Functions

#[requires(x.lt(y))]
#[ensures(result == x)]
fn main(x: Field, y: pub Field) -> pub Field {
    if x.lt(y) {
      x
    } else {
      y
    }
}

Output:

The application panicked (crashed).
Message:  called `Option::unwrap()` on a `None` value

Unconstrained Functions

#[requires(num < 100000)]
#[ensures(result == num + 1)]
fn main(num: u32) -> pub u32 {
    let out = unsafe { 
        increment(num) 
    };
    out
}
#[requires(num < 100000)]
#[enusres(result == num + 1)]
unconstrained fn increment(num: u32) -> u32 {
    if num > 100000 {
      0
    } else {
      num + 1
    }
}

Output:

The application panicked (crashed).
Message:  internal error: entered unreachable code

Vectors

fn main(x: Field, y: pub Field) {
  let mut vector: Vec<Field> = Vec::new();
  for i in 0..5 {
    vector.push(i as Field);
  }
  assert(vector.len() == 5);
}

Output:

The application panicked (crashed).
Message:  internal error: entered unreachable code

Optional Types

fn main() {
    let none: Option<u32> = Option::none();
    assert(none.is_none());
    let some = Option::some(3);
    assert(some.unwrap() == 3);
}

Output:

error: assertion failed
  ┌─ src/main.nr:5:12
  │
5 │     assert(some.unwrap() == 3);
  │            ------------------- assertion failed
  │

Error: Verification failed!

Although some of these examples may seem easy to support we have decided to focus on completing our prototype sooner so we can get early feedback on the features that we think matter the most.

Noir PLONKY2 Backend

An essential component of Blocksense are ZK proofs, the primary technology which eliminates bad actors from manipulating truth. In order to make it easier for our ZK engineers to develop this component, we built a PLONKY2 backend for the Noir programming language. While this backend is not completely stable, it already serves as a good proof-of-concept. Since our work is public and open-source, anyone can download it, try it out, and submit feedback.

What is zero-knowledge?

ZK is a method by which any program can have its execution and results mathematically and publicly verified, without exposing any private data. Thus, anyone can be sure some sort of execution was done correctly and honestly, even if any number of secrets were used as input.

The difficulty with this system comes from having to transform arbitrary programs into mathematical expressions (circuits). Since the vast majority of languages are not created with ZK in mind, it's almost impossible to do this step.

What is Noir?

Noir is a programming language, designed by Aztec Labs from the ground up for ZK. Its syntax is based on a small subset of Rust, with all of the limitations which make conversion to circuits possible. To be more precise, code is compiled down to ACIR circuits, which can then be converted to any proving system's native circuits.

The only system which has been adapted for ACIR is barratenberg, also built by Aztec Labs. While it is an impressive project, we wanted to experiment with different proving systems in order to leverage the latest and greatest of ZK research. This is why we built our PLONKY2 backend for the Noir programming language.

What is PLONKY2?

PLONKY2 is a zkSNARK built by Polygon Labs, with efficiency, decomposition and size in mind. Recursive proofs can be generated faster than other systems. This enables proofs to be split into subproofs and distributed across hundreds or thousands of machines, and it provides the ability to shrink proofs down dramatically in seconds.

A simple programming language to write ZK programs, with fast-to-generate, distributed and small in size proofs gives us the best of both worlds. The consensus mechanism can be developed and maintained without much difficulty, while it's execution can be distributed on the blockchain with vast assuredness of the result's correctness, all for a small cost.

Getting Started

Installation

Install dependencies, you'll only need two things: the nix package manager and direnv. They're compatible with most OSes and will not collide with your system.

After installing direnv do not forget to add the hook!

Clone our repository with SSH:

git clone https://github.com/blocksense-network/noir.git

Navigate to the folder noir.
```
cd noir
```
Run direnv command:
```
direnv allow
```
Depending on your nix installation, you may get a Permission denied error. In that case, it's best to start a superuser shell and continue from there:
```
sudo su                      # Start superuser shell
eval "$(direnv hook bash)"   # Setup the direnv hook
direnv allow
```
This should result in a plethora of things happening in the background and foreground. Sit back, relax, and wait it out. By the end you'll have everything ready to start work.
Test if everything works:
```
cargo test zk_dungeon
```
This will also take a little bit of time, until the project fully compiles.

Using

We're now ready to create our first proof!

Create a new project:
```
nargo new my_program
```
Navigate to the folder:
```
cd my_program
```

Update the program with your favorite text editor to:

fn main(x: pub u64, y: u64) {
    assert(x % y == 0);
}

This program allows one to prove that they know of a private factor y of a public integer x.

Run a small check to generate what you need:
```
nargo check
```

We're almost there, change prove inputs to:

x = "4611686014132420609"
y = "2147483647"

Finally, we're ready to start proving:
```
nargo prove
```
Congratulations 🎉, you've made your first proof! Now we can verify it:
```
nargo verify
```

You've now successfully written and proven a Noir program! Feel free to play around, for example, if you change y to 3 in Prover.toml, you'll get a prove error.

Once you're done, head over to noir-lang.org and start learning about the language.

Noir Tracer

A useful tool when debugging Noir programs is one that can generate an execution trace of the program for the given inputs. Such a trace can be loaded in a specialized program that visualizes the execution timeline and gives insights into the behavior of the program during execution.

At Blocksense, we have built such a tool and integrated it in the nargo command line interface. Note that the project is still an early-alpha prototype, so there is still much to improve. Yet, it is already powerful enough to handle a broad range of Noir programs.

We are using the runtime tracing Rust library for the tracing format. Thanks to this, we have enabled the use of the time traveling debugger CodeTracer. With it you may traverse the execution timeline forwards and backwards in an intuitive GUI. More details about it can be found in the subpage Debugging with CodeTracer.

Installation

As already mentioned, the tool is integrated in the nargo CLI, but you need to fetch our fork of the Noir programming language in order to get it. Follow the installation guide for the Noir PLONKY2 backend, as it describes how to fetch the fork and build the system. Once you have nargo set up, you can use it in the following way.

Using

In order to generate a trace for a Noir program, you need to navigate to its root directory (the directory containing Nargo.toml). You also need to specify the directory where the trace should be generated.

You could try one of the programs included in test_programs. Alternatively, you can create a new one in the usual way:

nargo new simple_loop
cd simple_loop

Once that's done, write some text for the program (in src/main.nr):

fn main(x: pub u64, y: u64) {
    let mut z: u64 = y;
    for _ in 0..3 {
        z *= y;
    }
    assert(x % z == 0);
}

Generate a Prover.toml using nargo check.

nargo check

This command will generate the following Prover.toml:

x = ""
y = ""

Edit Prover.toml so that it contains an input for which the program will work:

x = "3072"
y = "4"

At this point, you can run nargo prove and nargo verify to check that the program is valid using our PLONKY2 backend. You can also execute it via nargo execute or run it in a debugger via nargo debug which are both upstream features.

That said, this page is about nargo trace. Using this new command, you can generate a recording (a trace) of the execution of the program and save that in a file. In order for this to work, you need to specify a directory where the recording should be stored via the --trace-dir command line parameter.

mkdir traces
nargo trace --trace-dir traces

The traces directory will now contain three files, two of which are metadata. The main file containing the trace is trace.json. You could inspect the files as is, but they are optimized for minimal whitespace, so you can use another convenience command we have added to the nargo CLI: nargo format-trace.

nargo format-trace traces/trace.json traces/formatted_trace.json

This generates the traces/formatted_trace.json file, which at the time of writing of this document looks like this:

[
  { "Type": { "kind": 30, "lang_type": "None", "specific_info": { "kind": "None" } } },
  { "Path": "<relative-to-this>/src/main.nr" },
  { "Function": { "path_id": 0, "line": 1, "name": "main" } },
  { "Type": { "kind": 7, "lang_type": "u64", "specific_info": { "kind": "None" } } },
  { "VariableName": "x" },
  { "VariableName": "y" },
  { "Call": { "function_id": 0, "args": [
    { "variable_id": 0, "value": { "kind": "Int", "i": 3072, "type_id": 1 } },
    { "variable_id": 1, "value": { "kind": "Int", "i": 4, "type_id": 1 } }
  ] } },
  { "Step": { "path_id": 0, "line": 2 } },
  { "Value": { "variable_id": 0, "value": { "kind": "Int", "i": 3072, "type_id": 1 } } },
  { "Value": { "variable_id": 1, "value": { "kind": "Int", "i": 4, "type_id": 1 } } },
  { "Step": { "path_id": 0, "line": 4 } },
  { "Value": { "variable_id": 0, "value": { "kind": "Int", "i": 3072, "type_id": 1 } } },
  { "Value": { "variable_id": 1, "value": { "kind": "Int", "i": 4, "type_id": 1 } } },
  { "VariableName": "z" },
  { "Value": { "variable_id": 2, "value": { "kind": "Int", "i": 4, "type_id": 1 } } },
  { "Step": { "path_id": 0, "line": 6 } },
  { "Value": { "variable_id": 0, "value": { "kind": "Int", "i": 3072, "type_id": 1 } } },
  { "Value": { "variable_id": 1, "value": { "kind": "Int", "i": 4, "type_id": 1 } } },
  { "Value": { "variable_id": 2, "value": { "kind": "Int", "i": 256, "type_id": 1 } } },
  { "Step": { "path_id": 0, "line": 7 } },
  { "Value": { "variable_id": 0, "value": { "kind": "Int", "i": 3072, "type_id": 1 } } },
  { "Value": { "variable_id": 1, "value": { "kind": "Int", "i": 4, "type_id": 1 } } },
  { "Value": { "variable_id": 2, "value": { "kind": "Int", "i": 256, "type_id": 1 } } }
]

Do note that this tool is at an early-alpha stage and the output is likely to change. That said, this guide should have given you an idea of how it is supposed to behave.

Specifically, from this trace, we can see that the trace contains all the steps that are taken during the execution of the program, as well as the contents of all the variables live at each step. Again, this is an early prototype and we are in the process of heavily optimizing it, including smart tracking of variables and reducing unnecessary repetition so that we keep the file size to a minimum.

Debugging with CodeTracer

After installing CodeTracer, you can launch any Noir program with ct run <program-folder> to benefit from the powerful debugging experience.

An example of using CodeTracer with Noir can be found in the demonstration video:

The Blocksense Noir Compiler