Writing Arithmetic Circuits

💡 Circuit Structure: Original circuit code consists of two key parts:

  • 💻 Computation: Determines how values are calculated during proof generation
  • 🔒 Constraints: Verifies the correctness of those calculations

While we typically write these together in our code, the compiler separates them. The constraints are fixed during the setup phase and become the core verification logic, while the computation part runs with private and public inputs during each proof generation.

Circuit Compilation Plonk Script

Plonkish Arithmetic Circuits

Plonkish arithmetic circuits are different from R1CS-like circuits in that they are designed to resemble a table, rather than a simple list of computations. This design makes the circuit more complex to reason about, but also provides some advantages in terms of computational efficiency.

  • 📊 Table Design
    • A column is a polynomial
    • A row is a root of unity
    • A cell is the evaluation of a polynomial at a root of unity
  • 📋 Column Types
    • 🔒 Advice: Advice columns, private inputs and intermediate data, all private data
    • 📌 Fixed: Constant columns, fixed values when creating the circuit, public data
    • 🔘 Selector: Selector columns, virtual columns, essentially constant columns, binary used to switch custom gate circuits
    • 📢 Instance: Instance columns, store public inputs (and public outputs)
  • 🔄 Arithmetic Circuit
    • ✨ Custom gates
    • 🔍 Lookup table
    • 🔗 Copy constraints
Plonkish Constraints Overview

Custom Gates

  • ✨ Custom gates are expressions that constrain multiple cells
  • 🔘 Selectors are essentially fixed constant columns. They are boolean, used to enable or disable gates
  • 🔄 We can reference cells from the previous row, next row, but max to 7 in halo2.
  • 📝 In our examples, we use b[1] to represent the next row
Custom Gate Constraints

Copy Constraints

  • 🔗 Copy constraints bind two cells together, ensuring their values must be the same
  • ⚡ These are the most efficient constraints. We can use them as much as we want
Copy Constraints

Lookup Tables

Lookup tables are very efficient for range checks and bit operations

⚡ XOR Example:

Instead of using complex constraints to implement XOR, we can use a lookup table:

a b a ⊕ b
0 0 0
0 1 1
1 0 1
1 1 0

Using a lookup gate, we can verify that for any inputs (a, b) and output c, the triplet (a, b, c) appears in our XOR truth table, making bit operations much more efficient than implementing them with arithmetic constraints.

Lookup Tables

Gate Tricks

🎨 Writing circuits in Plonkish is totally different from writing circuits in R1CS (Circom) or zkVM program.

Here are some tricks that might help you write circuits in Plonkish.

Limiting Values

Sometimes we need to limit a value to a specific set of values. For example, we might want to ensure that a value is either 1, 2, or 3.

🔢 Limiting Value Gate:

s × (a - 1)(a - 2)(a - 3) = 0

  • This gate enforces that a can only take one of the values 1, 2, or 3 when s = 1
  • If a = 1, the first term (a - 1) becomes 0, making the entire expression 0
  • If a = 2, the second term (a - 2) becomes 0, making the entire expression 0
  • If a = 4 or a = 99, none of the terms become 0, so the expression will not be 0
  • Similarly, if a is any other value, the gate will not satisfy the equation unless s = 0, which means the selector is disabled
Limiting Value Gate

If-Else Condition

Implementing conditional logic in ZK circuits requires special techniques. Here's how to implement an if-else condition:

🔀 Conditional Output Gate:

s × (c × a + (1 - c) × b - out) = 0

  • This gate enforces that the output out is either a or b depending on the value of c
  • If c = 1, the output will be a
  • If c = 0, the output will be b

🔍 Selector Validity Gate (Boolean Gate):

s × c × (1 - c) = 0

  • This gate ensures that c is a valid boolean value (either 0 or 1)

Together, these gates implement the conditional logic if c then a else b.

If-Else Condition

Is-Zero Check

Checking if a value is zero is a common operation in ZK circuits, but it requires special handling:

🔍 Is-Zero Definition:

The inv value is defined as:

inv = input == 0 ? 0 : 1/input

The output is calculated as:

output = -input × inv + 1

With the constraint:

input × output = 0

This technique allows us to check if a value is zero and produce a boolean result (1 for zero, 0 for non-zero).

Case input inv output input × output
Non-zero input 4 1/4 0 0
Zero input 0 0 1 0
Non-zero input (malicious inv) 4 1/5 1/5 4/5
Zero input (malicious inv) 0 1/5 1 0

If-Equal Condition

The if-equal condition implements: out = a == b ? c : (a - b) . This technique combined the tricks from is-zero and if-else.

🔀 Gate 1: Equality Check (via is-zero)

s × (a - b) × (1 - ((a - b) × inv)) = 0

  • This gate ensures that if a = b, the expression becomes 0
  • From is-zero, we know that input = a - b and inv is the inverse of a - b
  • When a ≠ b, the gate enforces the calculation based on a - b and its inverse

🔀 Gate 2: Output Assignment

s × (1 - (a - b) × inv) × (out - c) = 0

  • This gate enforces that when a = b, the output out must equal c
  • If a ≠ b, this constraint is automatically satisfied

🔀 Gate 3: Alternative Output

s × (1 - (1 - (a - b) × inv)) × (out - (a - b)) = 0

  • This gate enforces that when a ≠ b, the output out is set to a - b
  • If a = b, this constraint is automatically satisfied

💡 Together, these three gates implement the conditional structure:

  • When a = b: The output out is set to c
  • When a ≠ b: The output out is set to a - b
If-Equal Condition
Under Construction

More tricks to come

More circuit tricks and techniques will be added soon.