Axiom v0.3.0

For users of the Axiom fork of the Halo2 stack.

info

This tutorial corresponds to the circuit type Halo2 based on Axiom v0.3.0. In particular, follow the guidelines described below if your circuitry is built on the v0.3.0 version of Axiom's halo2-base.

Introduction

In this tutorial, we will work with a circuit that accepts some two-dimensional point and computes the distance from the origin to that point. This distance is made public, so that anyone can know what circle the point lies on, but not the point itself. Our Halo2 circuit is written via Axiom's simplified API v0.3.0 and makes use of this gadget for fixed precision operations. For the full circuit definition, consult this example in the sindri-resources repository. The remainder of this introduction will describe the operations taking place inside the circuit in greater detail; however, feel free to skip to the Circuit Configuration section to learn more about our Halo2 circuit requirements.

The public and private variables of the radius circuit.

Quantized Arithmetic

Initially, the circuit may seem quite trivial; it calculates one simple formula $\sqrt{x^2+y^2}$ . The principal complication is that $x$ and $y$ need not be integers, while all calculations must take place in a large finite field $\mathbb{F}_q$ . Before the pair $x$ and $y$ are passed into the circuit, they must be quantized. In other words, these floating point numbers pass through a map which finds their approximate counterparts in the field. An important feature of this map is that it reversible, so that we can dequantize any result from the circuit without a major loss in precision.

Quantization generally takes place over binary representations, rather than the base 10 decimal representations depicted here.

As for operations that take place inside our circuit, $x*x$ , $y*y$ , and their sum are straightforward. However, there is no parallel operation within a finite field for square roots of floating point numbers. The diagram below shows how the circuit approximates this value. Our basic strategy is to break the square root operation down into fundamental pieces, exponentiation and logarithms, and use polynomial approximation on those pieces. Calculating the value of a polynomial at any input is a sequence of multiplication and addition which we can readily implement over a finite field.

You may observe that we could have applied the polynomial approximation trick to the original square root curve. However, this strategy (approximating 2^x and log2(x)) is more versatile. You could easily calculate any non-integer power of a number with the same two polynomials.

Circuit Configuration

Sindri's Halo2 prover functions very similar to PSE's fork of Halo2; it will produce a zk-SNARK based on the SHPLONK commitment scheme using Blake2B as the hash function for the proof transcript. The only difference is that Sindri's version incorporates performance optimizations which include GPU acceleration. The Halo2 prover is a rust package of its own that specifies your circuit, called float-radius in this example, as an external dependency.

Here is what the circuit directory would look like before you compress everything and upload. There are some differences between the tree displayed below and what your local development directory might look like. You might use code in /src/bin that we won't need. However if your manifest needs that code to build, keep it in! We also do not need any executable targets. Including compiled code, such as anything in debug/ or target/ will cause an error during compilation.

📦circuit
 ┣ 📂src
 ┃ ┣ 📂bin
 ┃ ┃ ┗ 📜test_proof.rs
 ┃ ┣ 📜circuit_def.rs
 ┃ ┣ 📜gadgets.rs
 ┃ ┗ 📜lib.rs
 ┣ 📜Cargo.lock
 ┣ 📜Cargo.toml
 ┣ 📜sindri.json
 ┣ 📜config.json
 ┣ 📜input.json
 ┗ 📜rust-toolchain

Any circuit you submit with type Axiom v0.3.0 should look similar to a halo2-scaffold circuit. In particular, you will need to implement the five functions depicted in grey blocks below. The CircuitInput struct (which may be renamed in your project) contains all of the input to a circuit. Sindri's proving backend will instantiate this with the default constructor for key generation, and then via the from_json function for any proof request. The create_circuit function is where you define your circuit operation given the inputs from CircuitInput. If you have previously developed a circuit based on Axiom's halo2-scaffold, the create_circuit function will absorb all of the code you wrote for some_algorithm_in_zk. The circuit used for proving should be returned by create_circuit which returns a builder either in keygen or prove mode. Finally, you'll need to implement the instance and break_points functions which are relatively straightforward assuming you've created a builder struct on top of the RangewithInstanceCircuitBuilder.

High level schematic of the radius circuit, as defined in circuit_def.rs.

Below, we offer some more guidance on the five required functions and their signatures.

Default
from_json
create_circuit
instance
break_points

The default constructor is invoked during key generation while your circuit is being compiled. Here, we pass the pair $(1.0,1.0)$ to the circuit input struct. We also pass the dummy field variable _marker since our circuit is over a finite field but this dependence is not explicit during the initial input phase (since $x$ and $y$ are floats).