# 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:
\begin{equation}
\text{active_idx} = \sum_{j=0}^{N-1} \text{bits}[j] \times j
\end{equation}

| `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`:
\begin{equation}
\text{is_active} = \sum_{j=0}^{N-1} \text{bits}[j]
\end{equation}

- **`is_transition`**: Returns `1` if the transition is ongoing, i.e., the sum of the first `N-1` bits is `1`:
\begin{equation}
\text{is_transition} = \sum_{j=0}^{N-2} \text{bits}[j]
\end{equation}

- **`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`<br>(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,<br> Only `bits[0]` is 1 in the next row. |
| `[0, 0, 0, 1]` | `[0, 0, 0, 0]` | Last `bits[3]` was active,<br> 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`:
\begin{equation}
\text{input} \cdot \text{output} = 0
\end{equation}

2. **Identity constraint**: Ensures that when `input ≠ 0`, `inv` correctly represents the multiplicative inverse:
\begin{equation}
\text{output} + \text{input} \cdot \text{inv} = 1
\end{equation}

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 <br>`output`** | **Expected <br> `inv`** | **Check:** <br> `input * output = 0` | **Check:** <br> `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:
\begin{equation}
\text{diff} = a - b
\end{equation}
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 \neq b$, then $\text{diff} \neq 0$, and `output` is `0`, while `inv` stores $\text{diff}^{-1}$.

### Example initialization:

| **`a`** | **`b`** | **`a - b` <br>(diff)** | **`output`** <br>(`1` if `a = b`) | **`inv`** <br>(`(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:
\begin{equation}
(a - b) \cdot \text{output} = 0
\end{equation}
2. **Inverse validation**: When `a ≠ b`, the inverse value must be correctly set:
\begin{equation}
\text{output} + (a - b) \cdot \text{inv} = 1
\end{equation}

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` <br>(diff)** | **Expected <br>`output`** | **Expected <br>`inv`** | **Check:** <br>`(a - b) * output = 0` | **Check:** <br>`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`** <br>(`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`:
\begin{equation}
\text{step}_0 = 0
\end{equation}

2. **Step progression**: Every row validates whether the current step is the last step:
\begin{equation}
\text{is_last_step} = ( \text{step} == N-1 )
\end{equation}

3. **Transition constraint**: The step increases by `1` unless the last step is reached, in which case it resets to `0`:
\begin{equation}
\text{step}_{\text{next}} = \text{step} + 1 - \text{is_last_step} \cdot N
\end{equation}

#### Example step transitions ($N = 4$)

| **Current Step <br>(`step`)** | **Is last step <br>(`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`):
\begin{equation}
\text{is_active} \in \{0,1\}
\end{equation}

#### Transition constraint
Enforces that once a row is inactive, all subsequent rows must also be inactive:
\begin{equation}
\text{if } \text{is_active} = 0 \text{ then } \text{next.is_active} = 0
\end{equation}
This prevents transitions from inactive → active in later rows.

### Example row transitions
| **Current row <br>(`is_active`)** | **Next row <br>(`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 <br>(`value`)** | **Next value <br>(`value_next`)** | **Difference <br>(`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:
\begin{equation}
\text{diff} = \sum_{i=0}^{\text{MAX_DIFF_BITS}-1} \text{diff_bits}[i] \cdot 2^i
\end{equation}
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`):
\begin{equation}
\text{diff_bits}[i] \in \{0, 1\}, \quad \forall i
\end{equation}

2. **Multiplicative inverse check**
Ensures that `diff_inv` correctly represents the inverse of `diff`:
\begin{equation}
\text{diff_inv} \cdot \text{diff} = 1
\end{equation}
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:
\begin{equation}
\text{value}_{\text{next}} = \text{value} + \text{diff}
\end{equation}
This enforces a strictly increasing sequence.

### Example step transitions (`MAX_DIFF_BITS = 4`)

| **Current <br>`value`** | **Next <br>`value`** | **Binary <br>`diff_bits`** | **Computed <br>`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 ✅ |