Chiplets

The Chiplets module contains specialized components dedicated to accelerating complex computations. Each chiplet specializes in executing a specific type of computation and is responsible for proving both the correctness of its computations and its own internal consistency.

Miden VM uses five stacked chiplets:

• The Hash Chiplet (also referred to as the Hasher), whose controller records Eidos sequential, control-block, Merkle, and deferred-root compressions. The computation is proved by the separate EidosCompressionAir and And8LookupAir instances.
• The Bitwise Chiplet, used to compute bitwise operations (e.g., AND, XOR) over 32-bit integers.
• The Memory Chiplet, used to support random-access memory in the VM.
• The Arithmetic Circuit Evaluation (ACE), used to ensure that arithmetic circuits evaluate to zero.
• The Kernel ROM Chiplet, used to enable executing kernel procedures during the SYSCALL operation.

Each chiplet executes its computations separately from the rest of the VM and proves the internal correctness of its execution trace in a unique way that is specific to the operation(s) it supports. These methods are described by each chiplet’s documentation.

Chiplets module trace

The execution trace of the Chiplets module is generated by stacking the execution traces of each of its chiplet components. Because each chiplet is expected to generate significantly fewer trace rows than the core trace, stacking them enables the same functionality without adding a separate set of columns for each chiplet.

Each chiplet is identified within the Chiplets module by one or more chiplet selector columns which cause its constraints to be selectively applied.

The result is an execution trace of 24 columns: 23 shared selector/data cells plus the chiplet row clock. Row overlays provide room for the hash controller and for the 20-column AEAD-stream view of the bitwise region without allocating those layouts side by side.

EidosCompressionAir and And8LookupAir are separate trace tables. Dashed arrows show the hash controller's compression link and the compression AIR's byte lookups; other lookup relations are omitted. A controller request occupies one row, while a physical compression block occupies 32 rows. Requests with identical compression inputs may share a block whose provider multiplicity counts the number of those requests. See the hash chiplet for the controller and compression layouts, and the bitwise chiplet for the AEAD stream overlay.

The concatenated chiplet trace is padded independently to the smallest supported power-of-two height that can contain it. Padding rows use the all-ones selector prefix and zero payload columns.

Chiplets order

The order in which the chiplets are stacked is determined by the requirements of each chiplet, including the width of its execution trace and the degree of its constraints.

For simplicity, all of the "cyclic" chiplets which operate in multi-row cycles and require starting at particular row increments should come before any non-cyclic chiplets, and these should be ordered from longest-cycle to shortest-cycle. This avoids any additional alignment padding between chiplets.

After that, chiplets are ordered by degree of constraints so that higher-degree chiplets get lower-degree chiplet selector flags.

The resulting order is as follows:

Chiplet	Row Alignment	Internal Degree	Chiplet Selector Degree	Total Degree	Columns	Chiplet Selector Flag
Hash controller	8	8	1	9	22	$\{0\}$
Bitwise chiplet	8	3	2	5	20	$\{1, 0\}$
Memory	-	6	3	9	17	$\{1, 1, 0\}$
ACE	-	5	4	9	16	$\{1, 1, 1, 0\}$
Kernel ROM	-	-	5	-	5	$\{1, 1, 1, 1, 0\}$
Padding	-	-	-	-	-	$\{1, 1, 1, 1, 1\}$

Additional requirements for stacking execution traces

Internal transition constraints are gated by selectors that identify the rows and transitions owned by each chiplet. Multi-row cyclic chiplets use periodic columns aligned to their cycles. The stacked trace applies the following boundary contracts.

In the hash chiplet: controller constraints delimit the controller region, which is padded to an 8-row boundary before the bitwise region. EidosCompressionAir proves the Eidos compression rows.

In the bitwise chiplet: ordinary operations are row-local, while period-eight selectors gate transitions within each AEAD stream entry.

In the memory chiplet: the next-row selector $1-s'_2$ selects transitions whose next row belongs to the memory region, keeping the selector degree at three as shown below.

In the ACE chiplet: first-row, intra-chiplet transition, and last-row flags gate the corresponding constraints, as described under flags and boundary constraints.

In the kernel ROM chiplet: typed initialization and call messages bind each declared procedure digest and its call multiplicity.

Operation labels

Lookup messages carry an explicit BusId, independent of the physical selector encoding used by the chiplet overlay. A message is reduced with the domain-separated prefix bus_prefix[id] = alpha + (id + 1) * gamma, where gamma = beta^16 in the native VM proof, followed by its typed payload. This prevents two relations with structurally similar payloads from cancelling each other except with the standard random-encoding collision probability.

The following selection covers Core requests and their stacked-chiplet responses:

Interaction	BusId value
Kernel ROM call	3
Hasher full-state input	4
Hasher sequential absorption	6
Hasher result/CV return	7
Merkle verify input	8
Merkle update old/new inputs	9 / 10
Memory element read/write	11 / 12
Memory word read/write	13 / 14
Bitwise	15
ACE initialization	16

Other cross-AIR and virtual-table relations have their own IDs. The authoritative list is the BusId definition in air/src/constraints/lookup/messages.rs.

Chiplets module constraints

Chiplet constraints

Each chiplet's internal constraints are defined in the documentation for the individual chiplets. To ensure that constraints are only ever selected for one chiplet at a time, the module's selector columns $s_0, s_1, s_2, s_3, s_4$ are combined into flags. Each chiplet's internal constraints are multiplied by its chiplet selector flag, and the degree of each constraint is correspondingly increased.

This gives the following sets of constraints:

$$(1 - s_0) \cdot c_{hash} = 0 \text{ | degree} = 1 + \deg(c_{hash})$$

$$s_0 \cdot (1 - s_1) \cdot c_{bitwise} = 0 \text{ | degree} = 2 + \deg(c_{bitwise})$$

$$s_0 \cdot s_1 \cdot (1 - s'_2) \cdot c_{memory} = 0 \text{ | degree} = 3 + \deg(c_{memory})$$

$$s_0 \cdot s_1 \cdot (s_2) \cdot (1 - s'_3) \cdot c_{ace} = 0 \text{ | degree} = 4 + \deg(c_{ace})$$

In the above:

• $c_{hash}, c_{bitwise}, c_{memory}, c_{ace}$ each represent an internal constraint from the indicated chiplet.
• $\deg(c)$ indicates the degree of the specified constraint.
• flags are applied in a like manner for all internal constraints in each respective chiplet.
• the memory selector uses $s'_2$ to select transitions whose next row belongs to the memory region, as described above.

The Kernel ROM selector gates its KernelRomInit and KernelRomCall messages, described below.

Chiplet selector constraints

We also need to ensure that the chiplet selector columns are set correctly. The stacked trace design means that selector columns become active one prefix level at a time. Thus, selector constraints should only be applied to selector columns when they are acting as selectors.

• $s_0$ acts as a selector for the entire trace.
• $s_1$ acts as a selector column when $s_0 = 1$.
• $s_2$ acts as a selector column when $s_0 = 1$ and $s_1 = 1$.
• $s_3$ acts as a selector column when $s_0 = 1$, $s_1 = 1$, and $s_2 = 1$.
• $s_4$ acts as a selector column when $s_0 = 1$, $s_1 = 1$, $s_2 = 1$, and $s_3 = 1$.

Two conditions must be enforced for columns acting as chiplet selectors.

1. When acting as a selector, the value in the selector column must be binary.
2. When acting as a selector, the value in the selector column may only change from $0 \rightarrow 1$.

The following constraints ensure that selector values are binary.

$$s_0^2 - s_0 = 0 \text{ | degree} = 2 s_0 \cdot (s_1^2 - s_1) = 0 \text{ | degree} = 3 s_0 \cdot s_1 \cdot (s_2^2 - s_2) = 0 \text{ | degree} = 4 s_0 \cdot s_1 \cdot s_2 \cdot (s_3^2 - s_3) = 0 \text{ | degree} = 5 s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot (s_4^2 - s_4) = 0 \text{ | degree} = 6$$

The following constraints ensure that the chiplets are stacked correctly by restricting selector values so they can only change from $0 \rightarrow 1$.

$$s_0 \cdot (s'_0 - s_0) = 0 \text{ | degree} = 2 s_0 \cdot s_1 \cdot (s'_1 - s_1) = 0 \text{ | degree} = 3 s_0 \cdot s_1 \cdot s_2 \cdot (s'_2 - s_2) = 0 \text{ | degree} = 4 s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot (s'_3 - s_3) = 0 \text{ | degree} = 5 s_0 \cdot s_1 \cdot s_2 \cdot s_3 \cdot s_4 \cdot (s'_4 - s_4) = 0 \text{ | degree} = 6$$

In other words, the above constraints enforce that if a selector is $0$ in the current row, then it must be either $0$ or $1$ in the next row; if it is $1$ in the current row, it must be $1$ in the next row.

Chiplets bus

The Core and Chiplets AIRs connect offloaded operations through typed LogUp messages. Each message starts with a BusId, so relations with similar payloads remain domain-separated. The Core AIR emits requests from the decoder and stack, and the Chiplets AIR emits the matching responses. Their order in the trace does not affect the lookup argument.

The chiplet response column carries memory, bitwise, hasher, ACE initialization, kernel ROM, and AEAD-stream byte-pair operations. A separate return column carries completed hasher digests and chaining values.

Chiplets bus constraints

The verifier combines the proof-exposed normalized finals across AIRs, weighted by their trace lengths, with the statement boundary corrections and requires the total to be zero. These lookup columns do not use explicit last-row boundary constraints.

Hash-kernel lookup column

The hash-kernel LogUp column multiplexes row-disjoint relations for Merkle siblings, ACE memory reads, AEAD memory I/O, ordinary bitwise AND8 lookups, and memory range checks. Each relation uses its own BusId.

Shared wiring column

The shared wiring column carries ACE wiring, hasher-compression links, and AEAD stream traffic.