Circuit gadgets

CycleBits overview

CycleBits<T, N> is a cyclic bit array of size N, where exactly one bit is active (1) at a time. It is used to track cyclic state transitions.

Initialization

The bit array is initialized as follows:

• If an index i is provided, bits[i] = 1, and all other bits are set to 0, marking i as the active position.
• If no index is provided, all bits are initialized to 0, meaning no active position.

Example initialization (

$N=4$):

i (Active index)	bits Representation
None	[0, 0, 0, 0]
0	[1, 0, 0, 0]
2	[0, 0, 1, 0]
3	[0, 0, 0, 1]

Key properties

Each row has well-defined constraints that govern state transitions.

Active index computation

The active index is computed as:

$$\text{active\_idx}=\sum _{j=0}^{N-1}\text{bits}[j]\times j$$

bits representation	active_idx
[1, 0, 0, 0]	0
[0, 1, 0, 0]	1
[0, 0, 1, 0]	2
[0, 0, 0, 1]	3

State checks

• is_active: Returns 1 if any bit is active, otherwise 0:
  

  $$\text{is\_active}=\sum _{j=0}^{N-1}\text{bits}[j]$$

• is_transition: Returns 1 if the transition is ongoing, i.e., the sum of the first N-1 bits is 1:
  

  $$\text{is\_transition}=\sum _{j=0}^{N-2}\text{bits}[j]$$

• is_last_row_to_active: Returns 1 if the last bit (bits[N-1]) transitions to the first bit (bits[0]) in the next cycle.

Example transitions (

$N=4$):

Current bits	is_active	is_transition	is_last_row_to_active (Next: [1, 0, 0, 0])
[1, 0, 0, 0]	1	1	0
[0, 1, 0, 0]	1	1	0
[0, 0, 1, 0]	1	1	0
[0, 0, 0, 1]	1	0	1

Evaluation methods

Boolean constraints

• Ensures all bits are either 0 or 1.
• Guarantees that exactly one bit is active per row.

Transition constraints

The transition rules ensure the correct cyclic movement of the active bit across rows.

• Continuous activation progression: If a bit is active in the current row, the active index must increase by 1 in the next row.
• Wraparound or termination condition: If the last bit (bits[N-1]) is 1, then all bits in the next row (except possibly bits[0]) must be 0. This allows two valid transitions:
  1. Wraparound: The next active bit resets to the first position (bits[0] = 1), ensuring cyclic continuity.
  2. Termination: The next row has all bits set to 0, indicating the cycle ends.
• Inactivity rule: If no bit is active in the current state, the next state must also be inactive.

Example state transitions (

$N=4$)

Current bits	Next bits	Transition properties
[1, 0, 0, 0]	[0, 1, 0, 0]	Active index increases: 0 → 1
[0, 1, 0, 0]	[0, 0, 1, 0]	Active index increases: 1 → 2
[0, 0, 1, 0]	[0, 0, 0, 1]	Active index increases: 2 → 3
[0, 0, 0, 1]	[1, 0, 0, 0]	Last bits[3] was active, Only bits[0] is 1 in the next row.
[0, 0, 0, 1]	[0, 0, 0, 0]	Last bits[3] was active, The next row has all bits 0.
[0, 0, 0, 0]	[0, 0, 0, 0]	State remains inactive.

IsZeroCols overview

IsZeroCols<T> is a helper structure that verifies whether an input value is zero and enforces constraints accordingly. It consists of two columns:

• inv: Stores the multiplicative inverse of the input (if nonzero).
• output: Stores a boolean flag indicating whether the input is zero (1 if zero, 0 otherwise).

This gadget is useful to ensure efficient zero-checking without division operations.

Initialization

The columns of IsZeroCols are populated based on the given input:

• If input = 0, then:

  • output = 1
  • inv = 0 (zero value, since division by zero is undefined)

• If input ≠ 0, then:

  • output = 0
  • inv = input⁻¹ (multiplicative inverse of the input)

Example initialization:

Input	output (1 if input is 0)	inv (input⁻¹ if input ≠ 0)
0	1	0 (undefined division)
2	0	1/2
-3	0	-1/3
5	0	1/5

Key properties

The gadget enforces the following algebraic constraints:

1. Zero-product constraint: If input is nonzero, output must be 0, ensuring input * output = 0:
   

   $$\text{input}\cdot \text{output}=0$$

2. Identity constraint: Ensures that when input ≠ 0, inv correctly represents the multiplicative inverse:
   

   $$\text{output}+\text{input}\cdot \text{inv}=1$$

These constraints ensure that output correctly signals whether input is zero and that inv holds a valid inverse when necessary.

The following table illustrates how the constraints hold under different input values:

Input	Expected output	Expected inv	Check: input * output = 0	Check: output + input * inv = 1
0	1	0	0 * 1 = 0 ✅	1 + 0 * 0 = 1 ✅
2	0	1/2	2 * 0 = 0 ✅	0 + 2 * (1/2) = 1 ✅
-3	0	-1/3	-3 * 0 = 0 ✅	0 + (-3) * (-1/3) = 1 ✅
5	0	1/5	5 * 0 = 0 ✅	0 + 5 * (1/5) = 1 ✅

IsEqualCols overview

IsEqualCols<T> is a gadget that determines whether two values are equal by reducing the problem to a zero check. It wraps around the IsZeroCols<T> gadget, leveraging its properties to enforce equality constraints.

Initialization

To determine whether two values

$a$ and

$b$ are equal, we compute:

$$\text{diff}=a-b$$
Then, we apply the IsZeroCols logic to diff, which means:

• If
  $a=b$, then
  $\text{diff}=0$, and the output field of IsZeroCols is set to 1.
• If
  $a\ne b$, then
  $\text{diff}\ne 0$, and output is 0, while inv stores
  ${\text{diff}}^{-1}$.

Example initialization:

a	b	a - b (diff)	output (1 if a = b)	inv ((a - b)⁻¹ if a ≠ b)
3	3	0	1	0
4	2	2	0	1/2
7	-3	10	0	1/10
5	9	-4	0	-1/4

Key properties

The gadget enforces the following constraints using IsZeroCols:

1. Equality constraint: If a = b, then their difference must be 0, leading to:
   
   $$(a-b)\cdot \text{output}=0$$
2. Inverse validation: When a ≠ b, the inverse value must be correctly set:
   
   $$\text{output}+(a-b)\cdot \text{inv}=1$$

These constraints ensure that output correctly represents the equality check.

Example evaluations

This table illustrates how the constraints hold under different values:

a	b	a - b (diff)	Expected output	Expected inv	Check: (a - b) * output = 0	Check: output + (a - b) * inv = 1
3	3	0	1	0	0 * 1 = 0 ✅	1 + 0 * 0 = 1 ✅
4	2	2	0	1/2	2 * 0 = 0 ✅	0 + 2 * (1/2) = 1 ✅
7	-3	10	0	1/10	10 * 0 = 0 ✅	0 + 10 * (1/10) = 1 ✅
5	9	-4	0	-1/4	-4 * 0 = 0 ✅	0 + (-4) * (-1/4) = 1 ✅

CycleInt overview

CycleInt<T, N> is a gadget that represents a cyclic counter ranging from 0 to N-1. It ensures correct step progression and handles wraparound conditions when the last step (N-1) is reached.

Structure

CycleInt<T, N> consists of:

• step: Tracks the current step in the cycle.
• is_last_step: An IsEqualCols<T> gadget that checks if step equals N-1.

Initialization

The gadget initializes as follows:

• step is set to the given step value.
• is_last_step is populated to determine if step == N-1.

Example initialization (

$N=4$):

Step (step)	is_last_step.output (1 if step = N-1, else 0)
0	0
1	0
2	0
3	1

Key properties

State checks

1. First row constraint: The first row must always start at step = 0:
   

   $${\text{step}}_0=0$$

2. Step progression: Every row validates whether the current step is the last step:
   

   $$\text{is\_last\_step}=(\text{step}==N-1)$$

3. Transition constraint: The step increases by 1 unless the last step is reached, in which case it resets to 0:
   

   $${\text{step}}_{\text{next}}=\text{step}+1-\text{is\_last\_step}\cdot N$$

Example step transitions (

$N=4$)

Current Step (step)	Is last step (is_last_step.output)	Calculation for next step (step_next)
0	0	step_next = 0 + 1 - 0 × 4 = 1
1	0	step_next = 1 + 1 - 0 × 4 = 2
2	0	step_next = 2 + 1 - 0 × 4 = 3
3	1	step_next = 3 + 1 - 1 × 4 = 0 (wraparound)

LowerRowsFilterCols overview

LowerRowsFilterCols<T> is a simple filtering gadget that controls whether a row is active in an AIR trace. It ensures that once a row is marked as inactive, all subsequent rows must also remain inactive.

Initialization

The gadget consists of a single column:

• is_active: A boolean flag indicating whether the current row is active (1) or inactive (0).

The column is populated as follows:

• If a row is active, is_active = 1.
• If a row is inactive, is_active = 0.

Key properties

Boolean constraint

Ensures that is_active is always a valid boolean (0 or 1):

$$\text{is\_active}\in \{0,1\}$$

Transition constraint

Enforces that once a row is inactive, all subsequent rows must also be inactive:

$$\text{if }\text{is\_active}=0\text{ then }\text{next.is\_active}=0$$
This prevents transitions from inactive → active in later rows.

Example row transitions

Current row (is_active)	Next row (is_active)	Constraint applied
1	1	Row remains active ✅
1	0	Row becomes inactive ✅
0	0	Stays inactive ✅
0	1	❌ Invalid (violates constraint)

StrictlyIncreasingCols overview

StrictlyIncreasingCols<T, MAX_DIFF_BITS> is a gadget that enforces a strictly increasing sequence of values across rows in an AIR trace. It ensures that each value is strictly greater than the previous one and encodes the difference between consecutive values using binary decomposition.

Structure

StrictlyIncreasingCols<T, MAX_DIFF_BITS> consists of:

• value: The value at the current row.
• diff_bits: A binary representation of the difference between the current and next values.
• diff_inv: The multiplicative inverse of the difference, used to enforce constraints.

Initialization

For each row:

• Compute diff: The difference between the next and current values (diff = value_next - value).
• Encode diff_bits: The binary decomposition of diff using MAX_DIFF_BITS bits.
• Set diff_inv:
  • If diff = 0, set diff_inv = 0 (not allowed, but needed for handling padding).
  • If diff = 1, set diff_inv = 1.
  • If diff = 2, set diff_inv = 1/2.
  • Otherwise, set diff_inv = 1/diff (multiplicative inverse).

Example initialization (MAX_DIFF_BITS = 4)

Current value (value)	Next value (value_next)	Difference (diff)	Binary Representation (diff_bits)	Inverse (diff_inv)
3	5	2	[0, 0, 1, 0]	1/2
5	8	3	[0, 0, 1, 1]	1/3
8	9	1	[0, 0, 0, 1]	1
9	9 (Padding)	0	[0, 0, 0, 0]	0 (invalid)

Key properties

Difference calculation

The difference between consecutive values is computed as:

$$\text{diff}=\sum _{i=0}^{\text{MAX\_DIFF\_BITS}-1}\text{diff\_bits}[i]\cdot 2^i$$
This ensures that the difference is encoded correctly in binary form.

Constraints enforced

1. Boolean constraint for diff_bits
   Each bit in diff_bits must be a valid boolean (0 or 1):
   

   $$\text{diff\_bits}[i]\in \{0,1\},\mathrm{\forall }i$$

2. Multiplicative inverse check
   Ensures that diff_inv correctly represents the inverse of diff:
   

   $$\text{diff\_inv}\cdot \text{diff}=1$$
   This constraint enforces that diff_inv is correctly set when diff ≠ 0.

3. Strictly increasing condition
   Ensures that the next value is obtained by adding diff to the current value:
   

   $${\text{value}}_{\text{next}}=\text{value}+\text{diff}$$
   This enforces a strictly increasing sequence.

Example step transitions (MAX_DIFF_BITS = 4)

Current value	Next value	Binary diff_bits	Computed diff	Constraint applied
3	5	[0, 0, 1, 0]	2	next.value = 3 + 2 = 5 ✅
5	8	[0, 0, 1, 1]	3	next.value = 5 + 3 = 8 ✅
8	9	[0, 0, 0, 1]	1	next.value = 8 + 1 = 9 ✅
9	9 (Padding)	[0, 0, 0, 0]	0	Padding: No change required ✅