Modelando la estructura de datos Stack en ZK

Last updated on Jan 3, 2026

Este tutorial muestra cómo crear un stack en Circom.

Advertencia: este capítulo es largo.

Sin embargo, la estrategia para crear pruebas ZK sobre stacks será esencial cuando creemos una Máquina Virtual ZK (ZKVM) simple en el próximo capítulo. La mayor parte del trabajo para comprender cómo funciona una ZKVM se ha adelantado en este capítulo.

El stack es capaz de hacer push de un número a la cima del stack, hacer pop de la cima del stack, o no hacer ningún cambio.

Los stacks son inherentemente mutables, pero en Circom, solo se nos permite usar un array inmutable. Por lo tanto, un stack debe modelarse con un array inmutable. Cada vez que el stack cambia (mediante pop o push), creamos un nuevo array que representa el nuevo estado del stack.

Esto podría parecer ineficiente, pero no hay otra forma de evitarlo ya que las signals en ZK son inmutables (técnicas ZK más avanzadas tienen formas de optimizar esto, pero esa discusión está fuera del alcance de este artículo).

El primer requisito es que el stack tenga una “altura máxima” fija, que es la longitud del array inmutable. Para rastrear cuánto del stack está “usado”, empleamos una variable separada llamada “puntero del stack” (stack pointer), que es un índice basado en cero y nos dice dónde hacer push del siguiente elemento. sp apunta a un lugar no utilizado en el array donde se debe hacer push a un nuevo valor, que está un índice por encima de la cima del stack. El siguiente diagrama ilustra un stack con tres elementos, 10, 16 y 20:

\begin{align*}\texttt{sp}=3\\ \begin{array}{|c|c|c|c|c|c|c|} \hline \text{array}&10 & 16 & 20 & \circ & \space & \space \\ \hline \text{index}&0 & 1 &2 &3 &4 &5\\ \hline \end{array} \end{align*}

El puntero del stack sp apunta al índice 3, que está vacío y se denota con $\circ$ . El stack ignora cualquier valor en el índice 3 (el sp actual) o superior. Podrían tener valores distintos de cero, pero el circuito no los consideraría.

Supongamos que hacemos push del elemento 21 en el stack. Esto significa que incrementamos el puntero del stack y copiamos todos los valores anteriores. El stack actualizado ahora tiene sp = 4.

\begin{align*}\texttt{sp}=4\\ \begin{array}{|c|c|c|c|c|c|} \hline 10& 16 & 20 & \circ & \space \\ \hline 10 & 16 & 20 & 21& \circ & \space \\ \hline \end{array} \end{align*}

Si hacemos pop del stack, el sp se decrementa y no copiamos el valor 21 en el siguiente stack:

\begin{align*}\texttt{sp}=3\\ \begin{array}{|c|c|c|c|c|c|} \hline 10 & 16 & 20 & \circ & \space \\ \hline 10 & 16 & 20 & 21& \circ & \space \\ \hline 10 & 16 & 20 & \circ& \space & \space \\ \hline \end{array} \end{align*}

Si no ocurren cambios en el stack, de todos modos pasamos por algún tipo de paso de cálculo, donde simplemente copiamos todos los valores anteriores al siguiente stack.

\begin{align*}\texttt{sp}=3\\ \begin{array}{|c|c|c|c|c|c|} \hline 10 & 16 & 20 & \circ & \space \\ \hline 10 & 16 & 20 & 21& \circ & \space \\ \hline 10 & 16 & 20 & \circ& \space & \space \\ \hline 10 & 16 & 20 & \circ& \space & \space \\ \hline \end{array} \end{align*}

Dado que sp cambia con cada iteración, necesitamos almacenar el nuevo valor en una nueva signal cada vez porque el valor de una signal no puede actualizarse una vez asignado. Por lo tanto, usamos un array para rastrear el valor de sp en cada iteración:

\begin{array}{|c||c|c|c|c|c|c|} \hline \texttt{sp}\downarrow & \\ \hline 3 & 10 & 16 & 20 & \circ & \space \\ \hline 4 & 10 & 16 & 20 & 21& \circ & \space \\ \hline 3 &10 & 16 & 20 & \circ& \space & \space \\ \hline 3 &10 & 16 & 20 & \circ& \space & \space \\ \hline \end{array}

Al igual que hay una altura máxima del stack, también hay un número máximo de veces que podemos actualizarlo, ya que la tabla que modela el stack (un array 2D de Circom internamente) debe tener un tamaño fijo.

El tamaño máximo depende de nuestra aplicación. En un entorno blockchain, es muy poco probable que se puedan ejecutar 1 millón de instrucciones, pero al crear circuitos para aplicaciones más intensivas podríamos necesitar asignar un circuito más grande para acomodar posibles tamaños del stack.

Restricciones para el stack

Independientemente de si hacemos push, pop o no hacemos nada, los elementos desde 0 hasta sp - 2 inclusive necesitan copiarse (y estar restringidos para ser iguales) en el siguiente stack. En el ejemplo a continuación, el puntero del stack estaba en 4, luego ejecutamos una operación pop, y el puntero del stack pasó a ser 3. Los elementos en el índice del puntero del stack 0, 1, 2 (en naranja) fueron copiados.

\begin{array}{|c||c|c|c|c|c|c|} \hline \texttt{sp} & 0 & 1 & 2 &3 & 4 & 5\\ \hline 4 & \color{orange}{10} & \color{orange}{16} & \color{orange}{20} & 21& \circ & \space \\ \hline 3 &\color{orange}{10} & \color{orange}{16} & \color{orange}{20} & \circ& \space & \space \space \\ \hline \end{array}

Si la instrucción es pop, entonces también requerimos que el nuevo puntero del stack sea 1 menos que el anterior.

Restricciones para push

Durante un push, todos los valores hasta sp - 1 deben copiarse en el nuevo stack (nota que el puntero del stack apunta a una región vacía, por lo que no hay necesidad de copiarlo). El valor en sp - 1 debe estar restringido a ser el valor al que se le hizo push.

\begin{array}{|c||c|c|c|c|c|c|} \hline \texttt{sp} & 0 & 1 & 2 &3 & 4 & 5\\ \hline 3 &\color{orange}{10} & \color{orange}{16} & \color{orange}{20} & \circ& \space & \space \space \\ \hline 4 & \color{orange}{10} & \color{orange}{16} & \color{orange}{20} & 24& \circ & \space \\ \hline \end{array}

En el ejemplo anterior, el puntero del stack era 3, y copiamos los elementos en 0, 1, 2. También restringimos que el puntero del stack se incremente en 1. Además, debemos restringir que el puntero del stack sea uno mayor de lo que era anteriormente.

Restricciones para pop

Durante un pop, todos los valores hasta sp - 2 deben copiarse en el nuevo stack. Restringimos que el puntero del stack se decremente en uno.

\begin{array}{|c||c|c|c|c|c|c|} \hline \texttt{sp} & 0 & 1 & 2 &3 & 4 & 5\\ \hline 3 &\color{orange}{10} & \color{orange}{16} & \color{orange}{20} & \circ& \space & \space \space \\ \hline 2 & \color{orange}{10} & \color{orange}{16} & \circ & & & \space \\ \hline \end{array}

Restricciones para nop (no hacer nada)

Todos los valores hasta sp - 1 deben estar restringidos para ser los mismos. El sp debe estar restringido a igualar el valor de la iteración anterior.

\begin{array}{|c||c|c|c|c|c|c|} \hline \texttt{sp} & 0 & 1 & 2 &3 & 4 & 5\\ \hline 3 &\color{orange}{10} & \color{orange}{16} & \color{orange}{20} & \circ& \space & \space \space \\ \hline 3 & \color{orange}{10} & \color{orange}{16} & \color{orange}{20} & \circ& & \space \\ \hline \end{array}

Actualizando un stack según un conjunto de instrucciones

En cada iteración de las instrucciones, necesitamos saber si vamos a hacer push a un número, hacer pop a la cima o no hacer nada, lo cual denotaremos con “opcodes” o “instrucciones” PUSH, POP o NOP.

Por ejemplo, supongamos que nos dan las instrucciones PUSH 10 POP PUSH 16 PUSH 15 PUSH 4 NOP POP. Podríamos representar este conjunto de instrucciones como un array:

[PUSH, 10, POP, 0, PUSH, 16, PUSH, 15, PUSH, 4, NOP, 0, POP, 0]

Sin pérdida de generalidad, podríamos referirnos a PUSH como el número 1, POP como 2 y NOP como 0, por lo que las instrucciones podrían codificarse de la siguiente manera.

\begin{matrix} 1 & 10 & 2 & 0 & 1 & 16 & 1 & 15 & 1 & 4 & 0 & 0 & 2& 0\\ \texttt{PUSH}&&\texttt{POP}&&\texttt{PUSH}&&\texttt{PUSH}&&\texttt{PUSH}&&\texttt{NOP}&&\texttt{POP} \end{matrix}

Nota que cada instrucción siempre tiene una constante después de ella. Para PUSH, este es el valor al cual hacer push, pero para POP y NOP, la constante posterior se ignora. Colocar la instrucción en los índices 0,2,4,… etc., nos permite iterar a través de las instrucciones en pasos de dos. En otras palabras, si las instrucciones pudieran tener o no un argumento, entonces necesitaríamos cambiar el tamaño del paso dependiendo de si hay un argumento. Este tamaño de paso condicional aumenta la complejidad de nuestro ejemplo, por lo que colocamos los opcodes en intervalos pares para que siempre podamos dar un paso de dos.

Ahora, generemos una “metaTable” que nos dice qué operación ocurrirá en cada fila de la ejecución. Si añadimos las columnas is_push, is_pop o is_nop que indican qué instrucción está activa, entonces obtenemos la siguiente tabla.

El resultado final se vería como lo siguiente, pero reconstruiremos esta tabla paso a paso en la próxima sección:

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 10 & - & - & - \\\hline0 & \color{orange}{1} & 0 & - & 1 & - & - & - & - \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 16 & - & - & - \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & 16 & 15 & - & - \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & 16 & 15 & 4 & - \\\hline0 & 0 & \color{orange}{1} & - & 3 & 16 & 15 & 4 & - \\\hline0 & \color{orange}{1} & 0 & - & 3 & 16 & 15 & - & - \\\hline\end{array}

La interpretación de sp es dónde debería escribirse el siguiente valor si la instrucción actual es push. Si la instrucción es pop, entonces sp - 1 es el elemento que no debe copiarse.

Llenando la tabla

Para llenar la tabla desde is_push hasta arg, podemos simplemente copiar las instrucciones en un bucle y establecer is_push en 1 si la instrucción actual es PUSH, y así sucesivamente para las otras instrucciones. Obtendríamos el siguiente resultado:

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & & & & & \\\hline0 & \color{orange}{1} & 0 & - & & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 4 & & & & & \\\hline0 & 0 & \color{orange}{1} & - & & & & & \\\hline0 & \color{orange}{1} & 0 & - & & & & & \\\hline\end{array}

El puntero del stack siempre debe comenzar en cero, por lo que simplemente podemos establecerlo estáticamente (hardcode):

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_apop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & \boxed{0}& & & & \\\hline0 & \color{orange}{1} & 0 & - & & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 4 & & & & & \\\hline0 & 0 & \color{orange}{1} & - & & & & & \\\hline0 & \color{orange}{1} & 0 & - & & & & & \\\hline\end{array}

Podemos llenar el resto de la columna del puntero del stack incrementándolo si la instrucción es PUSH, decrementándolo para POP y manteniéndolo igual para NOP. Nota que actualizamos el siguiente valor de sp según la fila actual. Por lo tanto, en la iteración 0, actualizamos la fila 1 de la siguiente manera:

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_apop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & \boxed{0}& & & & \\\hline0 & \color{orange}{1} & 0 & - & \boxed{1}& & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & & & & & \\\hline\color{orange}{1} & 0 & 0 & 4 & & & & & \\\hline0 & 0 & \color{orange}{1} & - & & & & & \\\hline0 & \color{orange}{1} & 0 & - & & & & & \\\hline\end{array}

Es decir, debido a que el is_push actual es 1 y el sp actual es 0, escribimos 0 + 1 en la siguiente celda. Luego llenamos el resto de la columna sp de la siguiente manera:

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & \\\hline0 & \color{orange}{1} & 0 & - & 3 & & & & \\\hline\end{array}

Luego escribimos los valores de push en la celda apropiada simplemente usando las columnas sp y arg condicionados a si is_push es 1. Nota que solo las filas donde is_push == 1 se llenan en este paso:

\begin{array}{|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & \\\hline0 & \color{orange}{1} & 0 & - & 3 & & & & \\\hline\end{array}

Nota que los valores anteriores no se copiaron — solucionaremos eso en una sección posterior.

Manejando la fila cero

La fila cero es única porque no copia valores de la fila por encima de ella. Para evitar tener que bifurcar (branch) en base a si estamos en la fila cero o no, hacemos la tabla una fila más grande de lo que necesita ser, y luego empezamos a construir nuestras restricciones en la fila 1. De esa manera, cada fila siempre copia la fila superior.

En la demostración de código a continuación, definimos de forma directa (hardwire) las restricciones en la fila 0 porque más adelante, será inconveniente tratar la fila 0 como un caso especial (corner case) en cuanto a si copiamos o no los valores de la fila anterior.

Copiando la fila anterior

Ahora, necesitamos asegurar que los valores de una fila a la siguiente se copien correctamente. Una celda copia el valor sobre ella hasta el puntero del stack de la fila siguiente menos 1. Recuerda, sp apunta al espacio vacío encima del stack, por lo que sp - 1 apunta a la cima del stack.

Terminología de Columna y Stack

Debido a que estamos almacenando el stack “de lado” en una tabla, nos referiremos al fondo del stack como la columna 0, al elemento encima de esa columna (si existe) como la columna 1, y así sucesivamente. Cuando decimos “columna” nos referimos al “índice” del stack si el del fondo es cero.

Restricciones para copiar

si is_push = 1, entonces todos los elementos del stack 0..sp - 1 inclusive deben copiarse. La celda en sp contendrá el nuevo valor incrementado. Esto copia todo el stack.
si is_nop = 1, entonces todos los elementos del stack 0..sp - 1 inclusive deben copiarse. No se escribe nada en la celda en sp. Esto copia todo el stack.
si is_pop = 1, entonces todos los elementos del stack 0..sp - 2 inclusive deben copiarse. Recuerda, sp apunta a una celda vacía encima del stack, por lo que sp - 1 es el valor al que se le hará pop. Todo desde sp - 2 hacia abajo debe copiarse. Esto copia todo excepto la cima del stack.

Las condiciones en 2 y 3 tienen casos especiales (corner cases) si el puntero del stack es 0 o 1, respectivamente, porque ocurriría un desbordamiento inferior (underflow). Por lo tanto, necesitamos columnas especiales que indiquen si sp es menor que 2 o 1, y necesitamos manejar la copia de forma diferente. Específicamente:

si sp = 0, no se copiará nada
si sp = 1, copiaremos la celda en la columna 0 solo si la instrucción es NOP o PUSH

Creamos columnas adicionales (copy0, copy1, copy2, copy3) que sirven como flags para indicar si el valor para (column0, column1, column2, column3) respectivamente será copiado a la siguiente fila.

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & & & & & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & & & & & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & & & & & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

Manejando las condiciones iniciales

Tenemos otro caso especial al crear las restricciones para la fila 0: si intentamos copiar los valores de la fila anterior, causaremos un underflow en el array. Por lo tanto, necesitamos tratar esta fila de forma diferente: llenamos el valor de la primera fila de una manera más “hardcoded” y luego creamos iterativamente las restricciones comenzando en la fila 1.

Determinando si `copy` debería ser cero o uno

Recuerda las restricciones de antes:

si is_push = 1, entonces todos los valores 0..sp - 1 inclusive deben copiarse. La celda en sp contendrá el nuevo valor.
si is_nop = 1, entonces todos los valores 0..sp - 1 inclusive deben copiarse. No se escribe nada en la celda en sp.
si is_pop = 1, entonces todos los valores 0..sp - 2 inclusive deben copiarse. Recuerda, sp apunta a una celda vacía encima del stack, por lo que sp - 1 es el valor al que se le hará pop. Todo desde sp - 2 hacia abajo debe copiarse.

Podemos resumirlas en dos condiciones A y B:

A. si sp es 1 o mayor, y nuestra columna está 1 índice debajo de sp, y la instrucción actual es PUSH o NOP, deberíamos copiar

B. si sp es 2 o mayor, y nuestra columna está 2 índices debajo de sp, y la instrucción actual es POP, deberíamos copiar

Si nuestra columna no cumple ninguna de las condiciones anteriores, no copiamos. Estas incluyen:

la columna actual está en o por encima del puntero del stack
la columna actual está 1 por debajo del puntero del stack, y la instrucción actual es pop
el puntero del stack = 0

Usando las reglas anteriores, llenemos la tabla. En la fila 0, sp = 0, por lo que todas las columnas de copy serán 0:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & & & & & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & & & & & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

En la fila indexada como 1, sp es 1 o mayor, la instrucción es POP, pero no se cumple la condición A ni la B para ninguna columna, por lo que no copiamos:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & & & & & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & & & & & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

En la 2ª fila, sp es 0, por lo que nada se copia:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 0 & 0 & 0 & 0 & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & & & & & & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

En la 3ª fila, sp es 1 y la instrucción es PUSH, por lo que column0 cumple con la condición A:

“si sp es 1 o mayor, y nuestra columna está 1 índice debajo de sp, y la instrucción actual es PUSH o NOP, deberíamos copiar”

y copy0 se establece en 1:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 0 & 0 & 0 & 0 & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & \boxed{1} & 0 & 0 & 0 & 16 & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & & & & & & & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

En la 4ª fila, sp es 2 y la instrucción es PUSH, por lo que la columna 0 y la columna 1 cumplen con la condición A:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 0 & 0 & 0 & 0 & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & 1 & 0 & 0 & 0 & 16 & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & \boxed{1} & \boxed{1} & 0 & 0 & 16 & 15 & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & & & & & & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & & & & & & & & \\\hline\end{array}

En la 5ª fila, sp es 3 y la instrucción es NOP, por lo que las columnas 0, 1 y 2 cumplen con la condición A, la cual es “si sp es 1 o mayor, y nuestra columna está 1 índice debajo de sp, y la instrucción actual es PUSH o NOP, deberíamos copiar”:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} & & & & \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 &0 & 0& 0&0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0& & & & \\\hline\color{orange}{1} & 0 & 0 & \texttt{16} & 0 & 0 & 0& 0& 0& 16 & & & \\\hline\color{orange}{1} & 0 & 0 & \texttt{15} & 1 & 1& 0& 0& 0& 16& 15 & & \\\hline\color{orange}{1} & 0 & 0 & \texttt{4} & 2 & 1& 1& 0& 0&16 &15 & 4 & \\\hline0 & 0 & \color{orange}{1} & \texttt{-} & 3 &\boxed{1} &\boxed{1} & \boxed{1}&0 & 16& 15& 4& \\\hline0 & \color{orange}{1} & 0 & \texttt{-} & 1 & & & & & & & & \\\hline\end{array}

En la 6ª fila, sp es 1 y la instrucción es POP, por lo que usamos la condición B:

“si sp es 2 o mayor, y nuestra columna está 2 índices debajo de sp, y la instrucción actual es POP, deberíamos copiar”

Esto significa que las columnas 0 y 1 serán copiadas:

\begin{array}{|c|c|c|c|c|c|c|c|c||c|c|c|c|}\hline\texttt{is\_push} & \texttt{is\_pop} & \texttt{is\_nop} & \texttt{arg} & \texttt{sp} & \texttt{copy0} & \texttt{copy1} & \texttt{copy2} & \texttt{copy3} \\\hline\color{orange}{1} & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 0 & 10 & & & \\\hline0 & \color{orange}{1} & 0 & - & 1 & 0 & 0 & 0 & 0 & & & & \\\hline\color{orange}{1} & 0 & 0 & 16 & 0 & 0 & 0 & 0 & 0 & 16 & & & \\\hline\color{orange}{1} & 0 & 0 & 15 & 1 & 1 & 0 & 0 & 0 & 16 & 15 & & \\\hline\color{orange}{1} & 0 & 0 & 4 & 2 & 1 & 1 & 0 & 0 & 16 & 15 & 4 & \\\hline0 & 0 & \color{orange}{1} & - & 3 & 1 & 1 & 1 & 0 & 16 & 15 & 4 & \\\hline0 & \color{orange}{1} & 0 & - & 1 & \boxed{1}&\boxed{1} & 0& 0& & & & \\\hline\end{array}

Implementación en Circom de las condiciones de copia

Podemos crear un componente especializado en Circom para determinar si un valor debería copiarse desde arriba.

A. si sp es 1 o mayor, y nuestra columna está 1 índice debajo de sp, y la instrucción actual es PUSH o NOP, deberíamos copiar
B. si sp es 2 o mayor, y nuestra columna está 2 índices debajo de sp, y la instrucción actual es POP, deberíamos copiar

Este componente será usado en un bucle para determinar si una columna particular j debería copiarse. Establece out = 1 si una columna en particular debería copiarse. Este componente se aplica a cada columna para cada fila.

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

// RETURNS 1 IF ALL THE INPUTS ARE 1
template AND3() {
  signal input in[3];
  signal output out;
  
  signal temp;
  temp <== in[0] * in[1];
  out <== temp * in[2];
}

// j is the column number
// bits is how many bits we need
// for the LessEqThan component
template ShouldCopy(j, bits) {
  signal input sp;
  signal input is_pop;
  signal input is_push;
  signal input is_nop;
  
  // out = 1 if should copy
  signal output out;
  
  // sanity checks
  is_pop + is_push + is_nop === 1;
  is_nop * (1 - is_nop) === 0;
  is_push * (1 - is_push) === 0;
  is_pop * (1 - is_pop) === 0;
  
  // it's cheaper to compute ≠ 0 than > 0 to avoid
  // converting the number to binary
  signal spEqZero;
  signal spGteOne;
  spEqZero <== IsZero()(sp);
  spGteOne <== 1 - spEqZero;
  
  // it's cheaper to compute ≠ 0 and ≠ 1 than ≥ 2
  signal spEqOne;
  signal spGteTwo;
  spEqOne <== IsEqual()([sp, 1]);
  spGteTwo <== (1 - spEqOne) * (1 - spEqZero);
  
  // the current column is 1 or more 
  // below the stack pointer
  signal oneBelowSp <== LessEqThan(bits)([j, sp - 1]);
  
  // the current column is 2 or more
  // below the stack pointer
  signal twoBelowSP <== LessEqThan(bits)([j, sp - 2]);
  
  // condition A
  component a3A = AND3();
  a3A.in[0] <== spGteOne;
  a3A.in[1] <== oneBelowSp;
  a3A.in[2] <== is_push + is_nop;
  
  // condition B
  component a3B = AND3();
  a3B.in[0] <== spGteTwo;
  a3B.in[1] <== twoBelowSP;
  a3B.in[2] <== is_pop;
  
  component or = OR();
  or.a <== a3A.out;
  or.b <== a3B.out;  
  out <== or.out;
}

Podemos usar el componente anterior en un bucle para determinar qué partes del stack anterior deberían copiarse al nuevo. El siguiente template retorna un array de 0 o 1 para determinar qué columnas deberían copiarse. Por ejemplo, si hay 4 columnas y las primeras 2 columnas deberían copiarse, entonces retorna [1, 1, 0, 0]:"

template CopyStack(m) {
  var nBits = 4;
    signal output out[m];
    signal input sp;
    signal input is_pop;
    signal input is_push;
    signal input is_nop;

    component ShouldCopys[m];
    
    // loop over the columns
    for (var j = 0; j < m; j++) {
        ShouldCopys[j] = ShouldCopy(j, nBits);
        ShouldCopys[j].sp <== sp;
        ShouldCopys[j].is_pop <== is_pop;
        ShouldCopys[j].is_push <== is_push;
        ShouldCopys[j].is_nop <== is_nop;
        out[j] <== ShouldCopys[j].out;
    }
}

Stack Final

El siguiente código es la implementación final de nuestro stack, que combina todos los componentes juntos. Dado que ya hemos mostrado los componentes para ShouldCopy y CopyStack, el lector puede saltar al componente final StackBuilder. Los componentes anteriores son de las secciones previas. Lo hemos puesto en un único archivo para que el lector pueda copiar y pegarlo convenientemente en zkrepl y probarlo:

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template AND3() {
  signal input in[3];
  signal output out;
  
  signal temp;
  temp <== in[0] * in[1];
  out <== temp * in[2];
}

// j is the column number
// bits is how many bits we need
// for the LessEqThan component
template ShouldCopy(j, bits) {
  signal input sp;
  signal input is_pop;
  signal input is_push;
  signal input is_nop;
  
  // out = 1 if should copy
  signal output out;
  
  // sanity checks
  is_pop + is_push + is_nop === 1;
  is_nop * (1 - is_nop) === 0;
  is_push * (1 - is_push) === 0;
  is_pop * (1 - is_pop) === 0;
  
  // it's cheaper to compute ≠ 0 than > 0 to avoid
  // converting the number to binary
  signal spEqZero;
  signal spGteOne;
  spEqZero <== IsZero()(sp);
  spGteOne <== 1 - spEqZero;
  
  // it's cheaper to compute ≠ 0 and ≠ 1 than ≥ 2
  signal spEqOne;
  signal spGteTwo;
  spEqOne <== IsEqual()([sp, 1]);
  spGteTwo <== (1 - spEqOne) * (1 - spEqZero);
  
  // the current column is 1 or more 
  // below the stack pointer
  signal oneBelowSp <== LessEqThan(bits)([j, sp - 1]);
  
  // the current column is 2 or more
  // below the stack pointer
  signal twoBelowSP <== LessEqThan(bits)([j, sp - 2]);
  
  // condition A
  component a3A = AND3();
  a3A.in[0] <== spGteOne;
  a3A.in[1] <== oneBelowSp;
  a3A.in[2] <== is_push + is_nop;
  
  // condition B
  component a3B = AND3();
  a3B.in[0] <== spGteTwo;
  a3B.in[1] <== twoBelowSP;
  a3B.in[2] <== is_pop;
  
  component or = OR();
  or.a <== a3A.out;
  or.b <== a3B.out;  
  out <== or.out;
}

template CopyStack(m) {
  var nBits = 4;
    signal output out[m];
    signal input sp;
    signal input is_pop;
    signal input is_push;
    signal input is_nop;

    component ShouldCopys[m];
    signal copy[m];
    
    // loop over the columns
  for (var j = 0; j < m; j++) {
    ShouldCopys[j] = ShouldCopy(j, nBits);
    ShouldCopys[j].sp <== sp;
    ShouldCopys[j].is_pop <== is_pop;
    ShouldCopys[j].is_push <== is_push;
    ShouldCopys[j].is_nop <== is_nop;
    out[j] <== ShouldCopys[j].out;
  }
}

// n is how many instructions we can handle
// since all the instructions might be push,
// our stack needs capacity of up to n
template StackBuilder(n) {
  var NOP = 0;
  var PUSH = 1;
  var POP = 2;

  signal input instr[2 * n];
  
  // we add one extra row for sp because
  // our algorithm always writes to the
  // next row and we don't want to conditionally
  // check for an array-out-of-bounds
  signal output sp[n + 1];

  signal output stack[n][n];

  var IS_NOP = 0;
  var IS_PUSH = 1;
  var IS_POP = 2;
  var ARG = 3;
  
  // metaTable is the columns IS_NOP, IS_PUSH, IS_POP, ARG
  signal metaTable[n][4];

  // first instruction must be PUSH or NOP
  (instr[0] - PUSH) * (instr[0] - NOP) === 0;

  signal first_op_is_push;
  first_op_is_push <== IsEqual()([instr[0], PUSH]);

  // if the first op is NOP, we are forcing the first
  // value to be zero, but this is where the stack
  // pointer is, so it doesn't matter
  stack[0][0] <== first_op_is_push * instr[1];

  // initialize the rest of the first stack to be zero
  for (var i = 1; i < n; i++) {
      stack[0][i] <== 0;
  }

  // we fill out the 0th elements to avoid
  // uninitialzed signals. For a particular
  // execution, we only want one possible witness
  // to correspond to a particular execution
  sp[0] <== 0;
  sp[1] <== first_op_is_push;
  metaTable[0][IS_PUSH] <== first_op_is_push;
  metaTable[0][IS_POP] <== 0;
  metaTable[0][IS_NOP] <== 1 - first_op_is_push;
  metaTable[0][ARG] <== instr[1];

  // spBranch is what we add to the previous
  // stack pointer based on the opcode.
  // Could be 1, 0, or -1 depending on the
  // opcode. Since the first opcode
  // cannot be POP, -1 is not an option here.
  var SAME = 0;
  var INC = 1;
  var DEC = 2;
  signal spBranch[n][3];
  spBranch[0][INC] <== first_op_is_push * 1;
  spBranch[0][SAME] <== (1 - first_op_is_push) * 0;
  spBranch[0][DEC] <== 0;

  // populate the first row of the metaTable
  // and the stack pointer
  component EqPush[n];
  component EqNop[n];
  component EqPop[n];

  component eqSP[n][n];
  signal eqSPAndIsPush[n][n];
  for (var i = 0; i < n; i++) {
      eqSPAndIsPush[0][i] <== 0;
  }

  // signals and components for copying
  component CopyStack[n];
  signal previousCellIfShouldCopy[n][n];
  for (var i = 0; i < n; i++) {
    previousCellIfShouldCopy[0][i] <== 0;
  }
  for (var i = 1; i < n; i++) {
    // check which opcode we are executing
    EqPush[i] = IsEqual();
    EqPush[i].in[0] <== instr[2 * i];
    EqPush[i].in[1] <== PUSH;
    metaTable[i][IS_PUSH] <== EqPush[i].out;

    EqNop[i] = IsEqual();
    EqNop[i].in[0] <== instr[2 * i];
    EqNop[i].in[1] <== NOP;
    metaTable[i][IS_NOP] <== EqNop[i].out;

    EqPop[i] = IsEqual();
    EqPop[i].in[0] <== instr[2 * i];
    EqPop[i].in[1] <== POP;
    metaTable[i][IS_POP] <== EqPop[i].out;

    // get the instruction argument
    metaTable[i][ARG] <== instr[2 * i + 1];

    // if it is a push, write to the stack
    // if it is a copy, write to the stack
    CopyStack[i] = CopyStack(n);
    CopyStack[i].sp <== sp[i];
    CopyStack[i].is_push <== metaTable[i][IS_PUSH];
    CopyStack[i].is_nop <== metaTable[i][IS_NOP];
    CopyStack[i].is_pop <== metaTable[i][IS_POP];
    for (var j = 0; j < n; j++) {
      previousCellIfShouldCopy[i][j] <== CopyStack[i].out[j] * stack[i - 1][j];

      eqSP[i][j] = IsEqual();
      eqSP[i][j].in[0] <== j;
      eqSP[i][j].in[1] <== sp[i];
      eqSPAndIsPush[i][j] <== eqSP[i][j].out * metaTable[i][IS_PUSH];

      // we will either PUSH or COPY or implicilty assign 0
      stack[i][j] <== eqSPAndIsPush[i][j] * metaTable[i][ARG] + previousCellIfShouldCopy[i][j];
    }

    // write to the next row's stack pointer
    spBranch[i][INC] <== metaTable[i][IS_PUSH] * (sp[i] + 1);
    spBranch[i][SAME] <== metaTable[i][IS_NOP] * (sp[i]);
    spBranch[i][DEC] <== metaTable[i][IS_POP] * (sp[i] - 1);
    sp[i + 1] <== spBranch[i][INC] + spBranch[i][SAME] + spBranch[i][DEC];
  }
}

component main = StackBuilder(3);

/* INPUT = {
  "instr": [1, 16, 1, 20, 1, 22]
} */

Resumen

Para modelar una estructura de datos que cambia con el tiempo, escribimos restricciones para todas las posibles transiciones de estado, luego activamos esas transiciones de estado en función de flags. Los flags están restringidos para que coincidan con la instrucción de esa transición de estado en particular.

Aunque entender la aritmetización de la estructura de datos del stack puede ser intimidante, ahora sabemos casi todo lo que necesitamos saber para entender cómo construir una ZKVM basada en stack, lo cual cubrimos en el próximo capítulo. Para crear una ZKVM basada en stack, simplemente modificamos las instrucciones y sus respectivas restricciones presentadas en este capítulo para que coincidan con el opcode para la ZKVM.

En general, la mayoría de los cálculos significativos pueden modelarse como un estado inicial que se actualiza incrementalmente hasta que se alcanza un resultado final. El stack que mostramos en este capítulo es solo un caso especial de esto.