Kernel ROM chiplet

The kernel ROM enables executing predefined kernel procedures. These procedures are always executed in the root context and can only be accessed by a SYSCALL operation. The chiplet tracks and enforces correctness of all kernel procedure calls as well as maintaining a list of all the procedures defined for the kernel, whether they are executed or not. More background about Miden VM execution contexts can be found here.

Kernel ROM trace

The kernel ROM table consists of five columns. The following example table shows the execution trace of the kernel ROM with procedure digests $a,b,c$, which were called 1, 2, and 0 times, respectively. Each digest is included once to respond to the initialization request by the public inputs, and then repeated for each call made by the decoder.

The meaning of columns in the above is as follows:

• Column $s_{first}$ specifies the start of a block of rows with identical kernel procedure digests.
• $r_0,...,r_3$ contain the digests of the kernel procedures. The values in these columns can change only when $s_{first}$ is set to 1 in the next row. Otherwise, the values in the $r$ columns remain the same.

Constraints

Note: the following assumes the ACE chiplet is included in the previous slot, whose documentation will be included in a subsequent PR.

The following constraints are required to enforce the correctness of the kernel ROM trace.

Note: Unless otherwise stated, these constraints should also be multiplied by chiplets module's virtual flag $f_{krom}$ which is active in all rows the kernel ROM chiplet.

The $s_{first}$ column is a selector indicating the start of a new digest included in the kernel ROM chiplet trace. In this row, the chiplet responds to a bus request made by the verifier to ensure consistency with the set of kernel procedure digests given as public inputs.

As $s_{first}$ is a selector, it must be binary.

$$s_{first}^2-s_{first}=0\text{ | degree}=2$$

The flag $s_{first}$ must be set to be 1 in the first row of the kernel ROM chiplet. Otherwise, the digest in this row would not be matched with one of the input procedure roots. This constraint is enforced in the last row of the previous trace, using selector columns from the chiplets module. More precisely, we use the virtual $f_{ACE}$ flag from the chiplet selectors $s_0,s_1,\dots ,s_{ACE}$ which is active in all rows of the previous (in this case ACE) chiplet, along with the selector $s_{ACE}$ which transitions from 0 to 1 in the last row, allowing us to target the first row of the kernel ROM trace.

$$f_{ACE}\cdot s_{ACE}^{\prime }\cdot (1-s_{first}^{\prime })=0\text{ | degree}=\mathrm{deg}(f_{prev})+2$$

Note that this selector need not be multiplied by the kernel ROM chiplet flag $chip$s4​, since it is only active when the previous chiplet is active._

The contiguity of the digests in a block is ensured by enforcing equality between digests across two consecutive rows, whenever the next row is not the start of a new block. That is, when $s_{first}^{\prime }=0$, it must hold that $r_i=r_i^{\prime }$. We disable this constraint in the last row of the kernel ROM chiplet trace by using the kernel ROM chiplet selector $s_4^{\prime }$, since the latter transitions from 0 to 1 when the next chiplet starts.

$$(1-s_4^{\prime })\cdot (1-s_{first}^{\prime })\cdot (r_i^{\prime }-r_i)=0\text{ | degree}=3$$

Note: we could technically remove the selector $(1-s_4^{\prime })$ since $s_4$ and $s_{first}$ correspond to the same column. We include it here for completeness though.

Chiplets bus constraints

The kernel ROM chiplet must ensure that all kernel procedure digests requested by the decoder correspond to one of the digests provided by the verifier through public inputs. This is achieved by making use of the chiplet bus $b_{bus}$, responding to requests made by the decoder and by the verifier through public inputs.

In the first row of each new block of hashes in the kernel ROM chiplet trace (i.e., when $s_{first}=1$), the chiplet responds to a message $v_{init}$ requested by the verifier. Since these initialization messages must match, the set of digests across all blocks must be equal to the set of procedure digests provided by the verifier (though not necessarily in the same order).

Whenever a digest is requested by the decoder during program block hashing of the SYSCALL operation, a new row is added to the trace after the first row which is used to respond to one of the initialization requests made by the verifier using public inputs. The chiplet responds to the request with a message $v_{call}$.

In other words, the selector $s_{first}$ indicates whether the chiplet should respond to the decoder or the verifier initialization requests. If a digest is requested $n$ times by the decoder, the same digest appears in a single block of length $n+1$.

The variables $v_{init}$ and $v_{call}$ representing the bus messages contain reduced bus messages containing a kernel procedure digest. Denoting the random values received from the verifier as ${\alpha }_0,{\alpha }_1$, etc., this can be defined as

$$\begin{array}{rl}r& =\sum _{i=0}^3({\alpha }_{i+2}\cdot r_i)\\ v_{init}& ={\alpha }_0+{\alpha }_1\cdot \text{KERNEL\_PROC\_INIT}+r\\ v_{call}& ={\alpha }_0+{\alpha }_1\cdot \text{KERNEL\_PROC\_CALL}+\tilde{r}\end{array}$$

Here, $\text{KERNEL\_PROC\_INIT}$ and $\text{KERNEL\_PROC\_CALL}$ are the unique operation labels for the kernel ROM bus message.

Each row of the kernel ROM chiplet trace responds to either a procedure digest initialization or decoder call request. Since the $s_{first}$ column defines which type of response is sent to the bus, it is used to combine both requests into a single constraint given by

$$b_{chip}^{\prime }=b_{chip}\cdot (s_{first}\cdot v_{init}+(1-s_{first})\cdot v_{call})\text{ | degree}=3.$$

The above simplifies to

• $s_{first}=1$: $b_{chip}^{\prime }=b_{chip}\cdot v_{init}$, when responding to a $\text{KERNEL\_PROC\_INIT}$ request.
• $s_{first}=0$: $b_{chip}^{\prime }=b_{chip}\cdot v_{call}$, when responding to a $\text{KERNEL\_PROC\_CALL}$ request.

The kernel procedure digests initialization requests are implemented by imposing a boundary constraint in the first row of the $b_{chip}$ column. This is described in the chiplets bus constraints.

By using the bus to initialize the kernel ROM procedure digest in this way, the verifier only learns which procedures can be invoked but doesn't learn how often they were called, if at all.

The full set of constraints applied to the $b_{chip}$ are described as part of the chiplets bus constraints.