ACE chiplet

The following note describes the design and functionality of the Arithmetic Circuit Evaluation (ACE) chiplet.

Given a description of an arithmetic circuit and a set of input values, it ensures this circuit evaluates to zero over these inputs. Its main purpose is to reduce the number of cycles required when recursively verifying a STARK proof in Miden assembly. In particular, it performs the DEEP-ALI constraint composition polynomial check over the evaluations of the trace column polynomials at the out-of-domain point.

The chiplet expects the caller to have prepared a region of memory containing

• inputs to circuit,
• constants which make up the circuit,
• instructions describing the arithmetic operations evaluated by the circuit.

The term variable refers to a value, which is either an input or a constant.

The circuit encoding defines the relation checked by ACE. Callers relying on a specific circuit must authenticate its encoding.

The standard circuit builder represents an arithmetic circuit as a topologically ordered DAG, where leaves correspond to inputs and constants, and the nodes are the operations computing the result (which must be zero). For example, take the following composition polynomial to be evaluated by the chiplet

$$s(s - 1) + \alpha \left[ s \cdot (\text{output} - 42) + (s - 1) \cdot (\text{output} - \text{input}) \right].$$

Given an input selector $s$, and input variables $\alpha, \text{input}, \text{output}$, the two combined constraints ensure that

$$s \in \{0,1\}, \quad \text{output} = \begin{cases} \text{input}, &s = 0, 42, &s = 1. \end{cases}$$

The following graph describes the evaluation of the circuit describing the above polynomial. The leaf nodes correspond to the variables of the polynomial: blue for inputs and green for constants. Note that the circuit is able to reuse evaluation, as is the case for the node $s-1$.

The processor evaluates such a DAG and records its wiring in a typed LogUp relation, which we interpret as a wiring bus. In each row, the processor can either insert a new node with the next fresh identifier and desired value or request a node's value by providing the identifier of a previously inserted node. Whenever the processor creates a new node (when loading a variable or evaluating an operation), it inserts $(id,v)$ onto the wiring bus with its final fan-out count $m$. Each later use of that node consumes one copy of $(id,v)$ from the wiring bus. The message also includes the section's $(clk, ctx)$ pair, so nodes from different circuit evaluations cannot satisfy each other's wiring requests except through a random-encoding collision. The relation balances globally and does not require a wire to be produced before it is used. Together with the local constraints, it enforces two properties:

1. The final output wire has value 0.
2. Every inserted tuple is consumed exactly $m$ times.

Trace layout

The ACE chiplet produces a trace with 16 internal columns. Each section of the trace corresponds to exactly one circuit evaluation.
Within each section, there are two ordered blocks:

1. A READ block, which loads inputs/constants from memory and inserts them into the DAG.
2. An EVAL block, which executes each instruction — fetching two existing DAG nodes, computing $v_{out}$, and inserting a new node.

In what follows, we'll refer to READ/EVAL blocks depending on which operation is being performed in a given row, though we sometimes refer to a row's mode when it would conflict with the term operation.

Columns

The following table describes the 16 columns used by the chiplet, and their interpretation in each block.

BLOCK	$s_{start}$	$s_{block}$	$ctx$	$ptr$	$clk$		$id_0$	$v_{0,0}$	$v_{0,1}$	$id_1$	$v_{1,0}$	$v_{1,1}$				$m_0$
READ	=	=	=	=	=		=	=	=	=	=	=	$n_{eval}$		$m_1$	=
EVAL	=	=	=	=	=	$op$	=	=	=	=	=	=	$id_2$	$v_{2,0}$	$v_{2,1}$	=

• "=" means the interpretation is the same in both READ/EVAL.
• Empty cell means the cell is unused in this block.
• Unlabeled columns appear under a block‐specific heading instead.

While we will later describe the purpose of each comment, we provide some intuition about how to interpret the labels themselves:

• $s_{start}$ is a boolean selector indicating the first row of a section,
• $s_{block}$ is a boolean selector indicating the type of block the row is a part of (0 for READ, and 1 for EVAL),
• $(ctx, ptr, clk)$ identifies the memory request when reading variables or circuit instructions.
• $(id_i, v_{i,0}, v_{i,1})$ refers to a node in the evaluation graph at index $id_i$ whose value is the extension field element $v_i = (v_{i,0}, v_{i,1})$, for $i = 0, 1, 2$.
• $m_i$ is used when inserting a node $(id_i, v_i)$ into the evaluation graph, corresponding to its fan-out degree. It is also interpreted as the multiplicity of the element being added to the wiring bus.

Memory layout

The chiplet trace contains multiple sections, each performing a distinct circuit evaluation.
Within a section, the chiplet reads through a contiguous, word‐aligned memory region that contains:

• $I$ input variables each stored as an extension‐field element, with two elements per word.
• $C$ circuit constants also stored two per word, which are part of the circuit description and hence included in its commitment.
• $N$ circuit instructions each encoded as one field‐element representing a packed triple $(op,id_l,id_r)$.

The caller is responsible for writing the inputs and circuit into memory before invoking the chiplet.
If the same circuit is evaluated multiple times, the caller must overwrite the input region with the new inputs for each evaluation.
To start a circuit evaluation, the caller emits one typed AceInit message:

$$\operatorname{AceInit}(clk,ctx,ptr,n_{read},n_{eval}),$$

where:

• $(ctx,clk)$ identifies the memory‐access context that every row will use.
• $ptr$ is the word-aligned pointer to the first input variable.
• $n_{read} = I + C$ is the total count of input and constant elements that the chiplet will read.
• $n_{eval} = N$ is the total number of arithmetic operations (instructions) the chiplet will evaluate. The chiplet stores $N - 1$ in the trace column so that the READ→EVAL switch triggers when $id_0' = n_{eval}$.

For both inputs and constants, it is permissible to pad their respective regions with zeros.
Any padded zero will simply be ignored by the instructions (they are not referenced by any instruction, so their multiplicity will be set to 0). To ensure the entire region is word-aligned, we add up to three "dummy" instructions which square the last node. This has no effect when the last evaluation is zero, as required.

Circuit evaluation

The evaluation is initialized in the first row of the section by setting

• $id_0 = n_{read} + n_{eval} -1$, indicating the expected number of nodes in the DAG. Whenever the chiplet adds a new wire to the bus, this identifier decrements by 1, until it reaches 0.
• $s_{start} = 1$, indicating the start of the section (it is set to 0 in all remaining rows)
• $s_{block} = 0$, ensuring the evaluation starts by reading variables
• $ctx, clk, n_{eval}, ptr$ provided by the bus request. $(ctx, clk)$ remain constant for the entire section, while $n_{eval}$ (stored as $N-1$ in the trace) is constant only across the READ block.

In every row, the chiplet performs the following actions in each block:

READ (when $s_{block} = 0$):

• Reads a word from memory at $(ctx,ptr,clk)$, containing two extension-field elements $(v_{0},v_{1})$.
• Assigns two new node IDs $(id_0,id_1)$ to those elements, where $id_1 = id_0 - 1$
• Inserts each new node into the evaluation graph (wiring bus) with a specified fan-out count $m_i$.
• Increments $ptr$ by 4 in the next row.
• Decrements $id_0$ by 2 in the next row.
• If $id_0'$ in the next row is equal to $n_{eval}$, it switches to the EVAL operation by setting $s_{block}' = 1$

EVAL (when $s_{block} = 1$):

• Reads a single field-element $instr$ (an encoded instruction) from memory at $(ctx,ptr,clk)$.
• Decodes $(op,id_1,id_2)$ from $instr$.
• Fetches the two input nodes $(id_1,v_1), (id_2, v_2)$ from the wiring bus, consuming one fan-out from each (i.e., with signed updates $e_1 = e_2 = -1$).
• Computes $$v_{0} = \begin{cases} v_1 - v_2, & op = -1, v_1 \times v_2, & op = 0, v_1 + v_2, & op = 1. \end{cases}$$
• Inserts $(id_0,v_{0})$ onto the wiring bus with its final fan-out count $m_0$.
• Increments $ptr$ by 1 in the next row.
• If $id_0 = 0$, checks that $v_0 =0$ and ends the evaluation.
• Otherwise, decrements $id_0$ by 1 in the next row.

Example

The following is a section of the trace representing the evaluation of the expressions

$$s(s - 1) + \alpha \left[ s \cdot (\text{output} - 42) + (s - 1) \cdot (\text{output} - \text{input}) \right].$$

We start by assigning values to both the inputs and constants nodes, stored in memory in addresses 0x0000 - 0x0005

$$\begin{aligned} v_{14} &= \alpha, & v_{10} &= 42, v_{13} &= \text{output}, & v_{9} &= 1. v_{12} &= s, v_{11} &= \text{input}, \end{aligned}$$

We can then write down the values of all evaluated nodes. Their instructions are stored in the memory region 0x0006 - 0x00014

$$\begin{aligned} v_{8} &= v_{12} - v_{9} &&|\ s - 1 v_{7} &= v_{12} \times v_8 &&|\ c_0 = s \times (s - 1) v_{6} &= v_{13} - v_{10} &&|\ \text{case}_{s=1} = \text{output} - 42 v_{5} &= v_{13} - v_{11} &&|\ \text{case}_{s=0} = \text{output} - \text{input} v_{4} &= v_{12} \times v_{6} &&|\ s \times \text{case}_{s=1} v_{3} &= v_{8} \times v_{5} &&|\ (s-1) \times \text{case}_{s=0} v_{2} &= v_{4} + v_{3} &&|\ c_1 = s × \text{case}_{s=1} + (s - 1) \times \text{case}_{s=0} v_{1} &= v_{14} \times v_{2} &&|\ \alpha \times c_1 v_{0} &= v_{7} + v_1 &&|\ \text{result} = c_0 + \alpha × c_1 \end{aligned}$$

$s_{start}$	$s_{block}$	$ctx$	$ptr$	$clk$	$op$	$id_0$	$v_{0}$	$id_1$	$v_{1}$	$n_{eval}$/$id_{2}$	$m_1$/$v_2$	$m_0$
1	0	ctx	0x0000	clk		14	$v_{14} = \alpha$	13	$v_{13} = \text{input}$	8	$m_{13} = 2$	$m_{14} = 1$
0	0	ctx	0x0004	clk		12	$v_{12} = s$	11	$v_{11} = \text{output}$	8	$m_{11} = 1$	$m_{12} = 3$
0	0	ctx	0x0008	clk		10	$v_{10} = 42$	9	$v_{9} = 1$	8	$m_{9} = 1$	$m_{10} = 1$
0	1	ctx	0x000c	clk	$-$	8	$v*{8} = v*{12} - v\_{9}$	12	$v_{12} = s$	9	$v_{9}$	2
0	1	ctx	0x000d	clk	$\times$	7	$v_{7} = v_{12} \times v_8$	12	$v_{12} = s$	8	$v_{8}$	1
0	1	ctx	0x000e	clk	$-$	6	$v_{6} = v_{13} - v_{10}$	13	$v_{13} = \text{output}$	10	$v_{10} = 42$	1
0	1	ctx	0x000f	clk	$-$	5	$v_{5} = v_{13} - v_{11}$	13	$v_{13} = \text{output}$	11	$v_{11} = \text{input}$	1
0	1	ctx	0x0010	clk	$\times$	4	$v_{4} = v_{12} \times v_{6}$	12	$v_{12} = s$	6	$v_{6}$	1
0	1	ctx	0x0011	clk	$\times$	3	$v_{3} = v_{8} \times v_{5}$	8	$v_{8}$	5	$v_{5}$	1
0	1	ctx	0x0012	clk	$+$	2	$v_{2} = v_{4} + v_{3}$	4	$v_{4}$	3	$v_{3}$	1
0	1	ctx	0x0013	clk	$\times$	1	$v_{1} = v_{14} \times v_{2}$	14	$v_{14} = \alpha$	2	$v_{2}$	1
0	1	ctx	0x0014	clk	$+$	0	$v_{0} = v_{7} + v_{1}$	7	$v_{7}$	1	$v_{1}$	0

Constraints

Flags

In this section, we derive boolean flags that indicate whether a row is at the boundary (first, last, or transition) of the ACE chiplet trace, a section, or a READ/EVAL block.

Chiplet flags

The chiplet trace activates different chiplet constraints using a common set of binary selectors $s_1, \ldots$. While it is likely that the ACE chiplet will appear in third position, we derive the flags and boundary constraints for the general case where the chiplet appears in the d-th position. Accounting for this degree allows us to evaluate whether we need a separate degree-1 internal selector for activating the chiplet's constraints. The layout of the chiplet trace will look something like the following.

Chiplet	$s_1, \ldots, s_{d-1}$	$s_{d}$	...
Previous	$[1, ..., 1, 0]$	$cols_{prev}$	$cols_{prev}$
ACE	$[1, ..., 1, 1]$	$0$	$cols_{ace}$
Next	$[1, ..., 1, 1]$	$1$	$0$

From these common selectors, we derive the following binary flags which indicate which portion of the ACE chiplet is active.

• $f_{prev}$: The previous chiplet is active.
• $f_{ace}$: The ACE chiplet is active.
• $f_{ace, first}'$: Next row is the first row in ACE chiplet.
• $f_{ace, next}$: Current and next rows are in ACE chiplet.
• $f_{ace, last}$: Last row in ACE chiplet.

$$\begin{aligned} f_{prev} &\gets (1 - s_{d-1}) \cdot \prod_{i=1}^{d-2} s_{i} && | \deg = d-1 f_{ace} &\gets (1 - s_{d}) \cdot \prod_{i=1}^{d-1} s_{i} && | \deg = d f_{ace, first}' &\gets f_{prev} \cdot s_{d-1}' \cdot (1 - s_d') && | \deg = d + 1 f_{ace, next} &\gets f_{ace} \cdot (1 - s_{d}') && | \deg = d + 1 f_{ace, last} &\gets f_{ace} \cdot s_{d}' && | \deg = d + 1 \end{aligned}$$

Section and block flags

The selector $s_{start}$ indicates the start of a new section, from which we can derive the following flags indicating which part of the section the current row is in:

• $f_{start}$: the current row initializes the section.
• $f_{next}$: the current and next rows are in the same section.
• $f_{end}$: the current row finalizes the section.

$$\begin{aligned} f_{start} &\gets f_{ace} \cdot s_{start} && | \deg = d+1 f_{next} &\gets f_{ace, next} \cdot (1 - s_{start}') && | \deg = d+2 f_{end} &\gets f_{ace, next} \cdot s_{start}' + f_{ace,last} && | \deg = d+2 \end{aligned}$$

These flags require the following constraints on $s_{start}$.

• it is binary.
• it must equal 1 in the first row.
• it must equal 0 in the last row.
• two consecutive rows cannot initialize a section, so a section contains at least two rows.

$$\begin{aligned} f_{ace} \cdot s_{start} \cdot (1 - s_{start}) &= 0 && | \deg = d + 2 f_{ace, first}' \cdot (1 - s_{start}') &= 0 && | \deg = d + 1 f_{ace, last} \cdot s_{start} &= 0 && | \deg = d + 2 f_{ace, next} \cdot s_{start} \cdot s_{start}' &= 0 && | \deg = d + 2. \end{aligned}$$

A section is composed of a READ block followed by an EVAL block. The flag indicating which block is active is derived from the binary selector $s_{block}$. These constraints ensure they are mutually exclusive

$$\begin{aligned} f_{read} \gets (1-s_{block}) & &&| \deg = 1 f_{eval} \gets s_{block} & &&| \deg = 1 f_{ace} \cdot (1-s_{block}) \cdot s_{block} = 0 && &| \deg = d + 2 \end{aligned}$$

The following constraints ensure the proper layout of the trace. In particular, it contains one or more sections each with consecutive READ and EVAL blocks.

• The first row cannot be EVAL, so it must be READ.
• A row after EVAL cannot be READ.
• The last row cannot be READ, so it must be EVAL.

$$\begin{aligned} f_{start} \cdot f_{eval} &= 0 && | \deg = d + 2 f_{next} \cdot f_{eval} \cdot f_{read}' &= 0 && | \deg = d + 4 f_{end} \cdot f_{read} &= 0 && | \deg = d + 3 \end{aligned}$$

In particular, we can infer from the above that

• each section contains at least two rows (a READ and an EVAL row), and,
• a row following a READ is always in the same section.

A READ row checks whether $id_0'$ in the next row is equal to $n_{eval}$ (the value stored in the trace, i.e. $N-1$), in which case we ensure the following row is an EVAL. Otherwise, $n_{eval}$ remains the same.

$$f_{ace} \cdot f_{read} \cdot \big[f_{read}' \cdot n_{eval}' + f_{eval}' \cdot id_0' - n_{eval}\big] = 0 \quad | \deg = d + 3.$$

Section constraints

These constraints apply to all rows within the same section:

• Across the section, $ctx$ and $clk$ are constant.
• A READ/EVAL block requests a word/element from memory, so the $ptr$ increases by 4/1, respectively in the next row.
• A READ/EVAL block adds 2/1 new nodes to the evaluation graph, so $id_0$ decreases by that amount in the next row.

$$\begin{aligned} f_{next} \cdot (ctx' - ctx) &= 0 && | \deg = d + 3 f_{next} \cdot (clk' - clk) &= 0 && | \deg = d + 3 f_{next} \cdot \big[ptr' - ptr - 4 \cdot f_{read} - f_{eval}\big] &= 0 && | \deg = d + 3 f_{next} \cdot \big[id_0 - id_0' - 2 \cdot f_{read} - f_{eval}\big] &= 0 && | \deg = d + 3 \end{aligned}$$

READ constraints

In a READ block, each row requests from memory a word containing two extension-field elements $v_0 = (v_{0,0}, v_{0,1})$ and $v_1 = (v_{1,0}, v_{1,1})$. The wire bus section describes how both of these nodes are inserted into the wire bus.

The only constraint we enforce is that $id_0$ and $id_1$ are consecutive

$$\begin{aligned} f_{ace} \cdot f_{read} \cdot (id_1 - id_0 + 1) &= 0 && | \deg = d + 2 \end{aligned}$$

EVAL constraints

An EVAL block checks that the arithmetic operation $op$ was correctly applied to inputs $v_1, v_2$ and results in $v_0$. The result is given by the degree-4 expression

$$v_{out} \gets op^2 \cdot \big[ v_1 + op\cdot v_2 \big] + (1 - op^2) \cdot \big[ v_1 \cdot v_2 \big] = \begin{cases} v_1 - v_2, & op = -1, v_1 \times v_2, & op = 0, v_1 + v_2, & op = 1. \end{cases}$$

The output node is correctly evaluated when:

• $op \in \{-1, 0, 1\}$ is a valid arithmetic operation, and,
• $v_0$ is equal to $v_{out}$.

$$\begin{aligned} f_{ace} \cdot f_{eval} \cdot op \cdot (op^2 - 1) &= 0 && | \deg = d + 4 f_{ace} \cdot f_{eval} \cdot (v_0 - v_{out}) &= 0 && | \deg = d + 5 \end{aligned}$$

The actual instruction is given by the field element $instr$ read from memory. It encodes

• the operation $op$ using 2 bits
• the IDs of $v_1$ and $v_2$, using 30 bits each and packed as

  $$instr \gets id_1 + id_2 \cdot 2^{30} + (op+1)\cdot 2^{60}.$$

It is clear from the constraint on $op$ that $op+1$ will always require 2 bits, and that range constraints on $id_1, id_2$ are unnecessary. These IDs are consumed as-is from the wire bus with multiplicity $-1$. Bus balance requires a matching node provider with the same identifier and value. The section bounds supplied by the initialization message and the constrained node-ID sequence ensure that the provider uses the corresponding $id_0$. Therefore, as long as the trusted circuit contains fewer than $2^{30}$ IDs, the $id_1$ and $id_2$ values can never overflow this bound.

To ensure the circuit has finished evaluating and that the final output value is 0, we enforce that the node with $id_0 = 0$ has value $v_0 = 0$ in the last row of the section.

$$\begin{aligned} f_{end} \cdot id_0 &= 0 && | \deg = d + 3 f_{end} \cdot v_0 &= 0 && | \deg = d + 3 \end{aligned}$$

Wire bus

Each ACE row contributes up to three messages to the circuit's wire bus. For $i = 0, 1, 2$, the typed AceWiring payload is $(clk, ctx, id_i, v_{i,0}, v_{i,1})$. Contributing this message updates the represented fan-out balance of the node. When performing a READ operation, a node is added to the graph, and we set its degree update $e_i$ to be equal to its final fan-out degree at the end of the evaluation. This value is also referred to as the multiplicity $m_i$. When a node is used as an input of an arithmetic operation, we set $e_i = - 1$.

The expression $e_i$ is derived from $m_i$ and the operation flag, so that the wire bus update is uniform across all rows of the chiplet's trace.

• $v_0$ always defines a new node, and each operation defines its identifier $id_0$ and multiplicity $m_0$ using the same columns.

  $$e_0 \gets m_0 \quad \text{| degree} = 1$$

• $v_1$ defines a new node when the operation is a READ, but is an input during an EVAL. Again, the columns for these values are identical.

  $$e_1 \gets f_{read} \cdot m_1 - f_{eval} \quad \text{| degree} = 2$$

• $v_2$ is unused during a READ, and an input during EVAL

  $$e_2 \gets - f_{eval} \quad \text{| degree} = 1$$

With the verifier challenges, the message denominator is

$$d_i = \operatorname{bus\_prefix}[\mathsf{AceWiring}] + \beta^0 clk + \beta^1 ctx + \beta^2 id_i + \beta^3 v_{i,0} + \beta^4 v_{i,1}.$$

The row contributes $\sum_{i=0}^2 e_i/d_i$. Thus, positive $e_i$ values provide a node's declared fan-out and negative values consume it. The shared LogUp construction supplies the denominator clearing, cyclic recurrence, and global closure.

ACE initialization and memory reads

On each $f_{start}$ row, the ACE chiplet provides one AceInit message with payload

$$(clk, ctx, ptr, n_\text{read}, n_\text{eval}).$$

The Core AIR's EVALCIRCUIT operation consumes the same message. On the first row, $id_0$ is the total number of nodes minus one, while the trace stores $n_\text{eval} - 1$. The response therefore reconstructs $n_\text{eval}$ and computes $n_\text{read} = id_0 + 1 - n_\text{eval}$. The AceInit domain separates this payload from other chiplet-bus interactions.

ACE memory requests occupy the hash-kernel LogUp column, where they are row-disjoint from its other relations and remain within the column's degree bound.

In each row, the chiplet makes one of the two following requests to the memory chiplet depending on which block it is in:

• MemoryReadWord with payload $(ctx, ptr, clk, v_{0,0}, v_{0,1}, v_{1,0}, v_{1,1})$ when $f_{read} = 1$.
• MemoryReadElement with payload $(ctx, ptr, clk, instr)$ when $f_{eval} = 1$.

The values are obtained as-is from the current row, except for the instruction which is given by

$$instr \gets id_1 + id_2 \cdot 2^{30} + (op+1)\cdot 2^{60}.$$

As mentioned earlier, it encodes a circuit instruction applying the arithmetic operation $op \in \{- ,\times, +\}$ (mapped to the range $[0,1,2]$) to the nodes with identifiers $id_1, id_2 \in [0, 2^{30}[$.

The READ payload is encoded under MemoryReadWord; the EVAL payload is encoded under MemoryReadElement. Each ACE row consumes one matching memory message with contribution $-1/d$, and the memory chiplet provides the corresponding $+1/d$. The message domains and complete payload encoding are described in memory row value.