# Axiom v0.3.0

## For users of the Axiom fork of the Halo2 stack.

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.

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

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.

## 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`

.

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

This function accepts **the path** of a JSON file and instantiates the circuit input struct.
Note that the function must be callable outside of the package, hence `pub fn`

.

The most important function in our circuit code is `create_circuit`

.
It accepts a `GateThreadBuilder`

which will communicate what mode the circuit is in and a possible set of break points.
Notice this function's dependence on the `LOOKUP_BITS`

environment variable.
See the `config.json`

file explanation below for a more thorough explanation on setting environment variables.
For variety's sake, we hard code the range of rows to configure the builder (`k`

and `minimum_rows`

) within this function rather than passing them through as`config.json`

fields.

After initializing the `FixedPointChip`

with 32 bits of precision, we perform the operations necessary to calculate $\sqrt{x^2+y^2}$.
Finally, a circuit builder is constructed and passed into our `RadiusCircuitBuilder`

struct.

The instance vec holds all of the public variables after a circuit has been synthesized. The API uses this function to return data to users after a proof has successfully executed.

In this tutorial example, our circuit builder struct uses Axiom's halo2-base RangeWithInstanceCircuitBuilder to do all the heavy lifting when it comes to circuit configuration and synthesis.
This struct already comes equipped with functions to return the instance variables (as long as those variables were passed along in the `create_circuit`

function).

Axiom's circuit building API greatly simplifies the way you build a circuit.
In particular, a developer no longer has to manually configure their circuit on the level of matrix coordinates.
Instead, they can specify all the operations they want to take place, and this configuration will occur in the background.
The break points of a circuit represent subdividers of a circuit, and they only need to be determined initially (e.g. during key generation, rather than during every proof).
For this reason, you need to provide a `break_points`

function which facilitates saving these dividers and load them during any proof request.

In this tutorial example, our circuit builder struct uses Axiom's halo2-base RangeWithInstanceCircuitBuilder to do all the heavy lifting when it comes to circuit configuration and synthesis. This struct already comes equipped with a function that returns the circuit break points.

There are two JSON files specific to the Sindri API that this circuit upload includes. Below, we will outline what each field accomplishes.

- sindri.json
- config.json

The package and class name fields correspond to what you have called your Cargo package (in the `.toml`

file) and the full import path to your circuit input struct.
You have two choices for the `threadBuilder`

field: either `GateThreadBuilder`

or `RlcThreadBuilder`

from the axiom-eth package.
See Axiom's halo2-lib documentation here for more information on thread builders.
Finally, the degree you specify allows Sindri to pull the correct size trusted setup file during circuit compilation.

The `config.json`

file is optional but provides a way of passing environment variables to various functions during circuit creation.
Since the functions described above (`create_circuit`

, `from_json`

, etc.) must have explicit function signatures, it would otherwise be difficult to write one circuit prototype that can have multiple concrete synthesized versions.

For the radius circuit in this walkthrough, we have a single environment variable that we will pass: `lookup_bits`

.
In the prover binary, we call `std::env::set_var(LOOKUP_BITS, "12");`

as a precursor to anything else.
This implicitly passes through the `create_circuit`

function anytime a concrete circuit is configured and determines the size of the lookup table associated with this circuit.

A good way to ensure that your circuit is compatible with the Sindri's Halo2 prover is to copy the code in `src/bin/test_proof.rs`

and revise any of the relevant circuit struct names.
If you can successfully execute that code locally, then it should be compatible.

## Sindri API

We'll walk through the steps to upload the packaged circuit to Sindri, generate proofs, and verify those proofs locally.
The following codeblock will pull the necessary code, install any dependencies, and run circuit compilation through (client-side) verification.
You will need to replace `<my-key>`

with your Sindri API key to authenticate all requests to the API (see Api Authentication).

`# Clone the sindri-resources repository and move into the `float_radius` tutorial.`

git clone https://github.com/Sindri-Labs/sindri-resources.git

cd sindri-resources/circuit_tutorials/halo2/axiom-v0.3.0/float_radius/

# Replace <my-key> with your own Sindri API key and save as an env var

export SINDRI_API_KEY=<my-key>

cargo run --bin compile

cargo run --bin prove

cargo run --bin verify

The following sections will describe what took place as you invoked the last three lines in the codeblock above.
The three binaries are defined in the `zk-execute`

package which shares a workspace with our circuit code described in the previous section.
While `compile`

and `prove`

communicate with Sindri's API, the `verify`

binary only loads the required arguments produced from the previous two steps and calls the `halo2`

method `verify_proof`

to check the validity of the returned data.

### Upload & Compile

To compile our circuit, we first need to create a gzipped tar archive of our circuit directory and upload it to the circuit create endpoint.
Our `sindri.json`

file will be included in the tarball and indicates that the `circuitType`

is `halo2`

and that `float-radius`

is the name of the circuit.
Uploading this tarball will automatically trigger circuit compilation.
After sending the compilation request, we initiate polling.
Since compiling a circuit and requesting a proof from that circuit will both involve the same functionality, we feature that function inside our common utility code: `lib.rs`

.

`loading...`

## Output - compile.rs

`Compiling circuit`

Circuit ID: "d01ceedf-329d-4df8-8b2d-d0679732df25"

Polling

........................

Polling exited after 25 seconds with status: "Ready"

Saving circuit details locally

## Abridged ./data/compile_out.json

`{`

"circuit_id": "d01ceedf-329d-4df8-8b2d-d0679732df25",

"circuit_name": "float-radius",

"circuit_type": "halo2",

"class_name": "radius_circuit::circuit_def::CircuitInput",

"compute_times": {

"clean_up": 0.0961455386132002,

"compile": 25.735420921817425,

"download_trusted_setup_file": 0.00015453435480594635,

"file_setup": 1.4096760787069798,

"generate_keys": 0.7937725819647312,

"queued": 1.330564,

"save_results": 0.05844421312212944,

"total": 28.093873316422105

},

"curve": "KZG bn254",

"date_created": "2023-12-08T17:59:51.679Z",

"degree": 13,

"error": null,

"halo2_version": "axiom-v0.3.0",

"metadata": {

"api_version": "v1.5.17",

"prover_backend_version": "v0.3.0"

},

"package_name": "radius-circuit",

"status": "Ready",

"thread_builder": "GateThreadBuilder",

"trusted_setup_file": "kzg_bn254_15.srs",

"verification_key": {

"data": "AAAADwAAAAXjd..."

}

}

Circuit compilation has accomplished three things:

- The prover binary executable has been built utilizing the uploaded circuit code.
- Proving and verification keys have been produced and serialized; if our polling request had set
`include_verification_key`

to`True`

then we could have extracted that key (encoded as a base64 string) for local verification. - The breakpoints of the circuit have been serialized and are available for each subsequent proof.

### Prove

For this proof we will submit the following two float values. After Sindri's API returns the instance vector, we can decode and dequantize this result to ensure that it matches what we expect: $\sqrt{x^2+y^2} =6.152642$.

`loading...`

The file above is loaded into a JSON formatted string and sent to the prove endpoint. Right after we send the request for a proof, we start polling. Details about the proof are requested every second until the proof status field indicates the proof is ready.

`loading...`

## Output - prove.rs

`Reading circuit details locally`

Reading proof input from example-input.json

Requesting a proof

Polling

...

Polling exited after 4 seconds with status: "Ready"

Saving proof details locally

## Abridged ./data/prove_out.json

`{`

"circuit_id": "d01ceedf-329d-4df8-8b2d-d0679732df25",

"circuit_name": "float-radius",

"circuit_type": "halo2",

"compute_times": {

"clean_up": 0.008553169667720795,

"create_proof": 0.878308658,

"file_setup": 1.5205974914133549,

"prove": 1.0356456451117992,

"queued": 0.950894,

"read_proving_key": 0.04658151,

"read_setup": 0.004306668,

"save_results": 0.001869363710284233,

"total": 2.5671290811151266

},

"date_created": "2023-12-08T18:01:40.451Z",

"error": null,

"metadata": {

"api_version": "v1.5.17",

"prover_backend_version": "v0.3.0"

},

"proof": {

"data": "/nexFaC3n4taHjK+uzYf1FBbu1a+aBSdY9MdwsQVmyZ22zXHVc57XTqNWr40ImVES2nnU9Etfm20HUjVrWeEr2lxWR9oJaPS/6Fn0jQdaSuYBIS6RyMAEt6DKzxmGhcBTqdkasAI3LHYCLc6XP4MV5qstZU6fLHq5UEiEpRlEhT8254Vuda8b3IUvLu3Feze4ag6SXdRHGjmBt4hNQ04JjLN5oVfFHv0UsTAfiV5xOMYYqlNM1/IiSyE+9x8a0usaz5Zd4eKMFtVpjjMtgb9hJxbNCuIE2Cm9WpBlnZxFCrlyshZ4WKqGjZ4Fcl7841ljuOTr0jiSN4anQ7bdzujnjCyns3ajq7Xd4usNW1LnA/kl1f0RbB3cMVFc/Qb8BsKMkbr045O7gkrtpWVFSXca2mq9vwvb6JiVN2IXliJwCOEuWQaNODzsXfVekMp7EqXitdpwA36mNZKp05tFW8EjJgYr4I4vGcWddL+SxRGkmGvEsQjHoJRLXhxhtttgD8bepBFKS1j586cggXQa9uC8UjYqrKu95J6e08B78BLaRF+JDMV1FYqQQS4cEZ4dvlmVyxTjzglJYZ2OR9oiqGMq+rCIKlQWhdyK9NiRI8PB0A34TgfJXZ+Bs4n/HMBw0Qp9gYrIEjjNQTC+aeKkt6l+QFPAIpJaa04Yrgo9CjWGimfcIJGy3RvSs/PGcGHZeqs27tgzRYBNjt8FRm+Ho5dJZZTfQaWVW8efQwB1fbm41QrAidx9e22zLXDNq46Uc4gRuMsVIUWN0Kpy+DyBCjsxP0toNZP8pDNooE7QttoKy5Ukz/ndQkjJrgPPzjpIBwscy7IGmhGMnxQkOWikBImKM5XU36RnHMRQG3sidaEav36eH/oYHrgv3xp5rphJ3QAJx8IZjWJrlhRztV0KPKbuLOk4LgztmpdE5cl7jWligEDCa1xTqCl046ro9PISSFeqb6/36cjGGAQb+OmpkGXBFWLBaT2Gk6uIOL33FQejqcJH06Ufilfb5m7QUHtDSUF7ibTyKeSd6PSPdnga7EmwHv6WH1cou1Qug/uzpn16gFSAa1VHMf/NdDfJ5Fxb0jq5/G4src+l6DjnvBuhv0DJgRoeNphG6L34klF/ymdSMEPp0jk7zQqj1SRYoHDcbgsvYpb8MtWNRo3dDaE9y+LGHM6y+XLB0xF/c4v66WFlRDifn7DU2Aq5Z5ME7oMXVNnhDu+Em8nAYFBbuguNnsyBbJO1SaiSYKaC4j2zMOpqJwfKkjtcHMPLSwWD2MXZeIvDZKn6OY+Za1/IkHGyV6YQMXKvnV5ujr672V3/5VHDynxUOkGHWdh/eH/BMPDTucoM/k0dtdPRJ0PktxWJ9U9DCCSiKUaYogAvB5XXfmtRa2eszqoob3d28wDzMhs6REJDdTS5MkiGQIiMMlBsf0QxtpnXS2U082cilTiJPMBgg2o59c/XJHFZQ4PXXOcypEDGhfxoJWKvxmMTLa74luhJcw+mB9pF7yMo/OsyXJ+az3yePuo+qG71BQmOtC2yk8YlbOigGvxv1P1ekoPDSxQlchLXRjuLljW8AJtLyJ2rBwbp9vlM92abx9hVJX7PcKHTgFJmgoRVe0dAZhqbijmLEohYruoL8nsnuzw0af5lx5yBfJEGyMQD5QiBJVGemYZqJwBMx6YDF/wDvOgQ1KS0XSD0zpotzwgD282XodyVRm0rBYCARJeTq2NogZa+VkPq0esuSJPfhrK75hWNrVWCMCq/6NH1YZM1d6gu6ZOABzG7rPImjqf2aPwnUaN5iUc1gsq70kFAEjyNgtJ5cr3lLM0YgX66SoTUg2r9Opa3SbPkdm8BTebX8+riqO1+qK0xHg3BPjP7cezZq/hgf2KLbCg1B9jfwo5Itr3AfqCo0PxB8AlL8P7VJiVggLN8wAkbGdiWMmRZHdC+wgnofmJTO94+zMLkwa448KMkGy+Kgg3cdQQjjQ7ziaaarQDlAxtegXe50Sf5CQxnnqTCpbSKSi40OPF7l1nMboWYZMu88uPdFt+K+FZd5+jtWxjGucsTfcKfABxVAuVT9jBPyeIasP/CMILgHiSNKg/EP8OFR/REkxi3vvT3++fuGFfnLhL96u3jUcNPUJ6TkJOkxKDJDdcl+nhOyhBaca3nhDLx46vULFxEXvi8cROKo9JzJwqXpDvmNzaOXW0Nyy4Pm9XQrF7eqKXKM9gxyZV2AVxLwLGM+20+oy2rUwLaB/xbOUD2eqTdb4F65CSiT9gkrI9p+FTPInC4YQqh61iCARE4AaigcsCrd0094uiZ6LnSM2M"

},

"proof_id": "391dd53c-0d55-43c2-b1e9-2075755d62d0",

"public": {

"data": [["MNMOJwYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA="]]

},

"status": "Ready",

"verification_key": {

"data": "AAAADwAAAAXjd..."

}

}

## Verify

In order to decode the `public`

data field returned from the API, we use the same `FixedPointChip`

from our circuit definition source code.
As a final check, we also load the `proof`

and `verification_key`

fields from the proof detail output and use the `halo2_proofs`

package to verify the proof.

`loading...`

## Output - verify.rs

`Reading proof details locally`

The claimed radius for this proof: 6.1525699608027935

k: 15, extended_k: 17

Verifying Proof + Public

Verification Successful!

We expected $6.152642$ given the input, so our floating point circuit result is accurate up to three significant figures.
Recall that the circuit's implementation of the square root function involves approximations of both $2^k$ and $\log_2(k)$which account for most of the difference.
If our application required more precision than this, we could have increased the `PRECISION_BITS`

field in our original circuit code.

The `verify.rs`

code above sets two environment variables: `LOOKUP_BITS`

and `FLEX_GATE_CONFIG_PARAMS`

.
These values are required so that the `VerifyingKey`

struct has the correct format when we load it from the base64 byte-encoded value returned from the API.
As you develop with `halo2-lib`

, using Axiom's halo2-scaffold as a starting point, you may find it useful to examine all environment variables which are set as you perform various functions of the circuit (e.g. key generation, proof generation, etc.).
Once you determine the values of these variables locally, you can reproduce the exact same circuit configuration parameters within Sindri's API via the `config.json`

file described at the end of the Circuit Configuration section.