Una Zero-Knowledge Virtual Machine (ZKVM) es una máquina virtual que puede crear una prueba ZK (ZK-proof) que verifica que ejecutó correctamente un conjunto de instrucciones de máquina. Esto nos permite tomar un programa (un conjunto de opcodes), una especificación de máquina virtual (cómo se comporta la máquina virtual, qué opcodes utiliza, etc.) y probar que la salida generada es correcta. Un verificador no tiene que volver a ejecutar el programa, sino solo comprobar la prueba ZK generada — esto permite que la verificación sea sucinta. Esta concisión es la base de lo que hace que las blockchains de capa 2 ZK sean escalables. También permite a alguien comprobar que un algoritmo de machine learning se ejecutó como se afirma sin tener que volver a ejecutar todo el algoritmo.

Contrario a lo que sugiere el nombre, las ZKVM rara vez son de “conocimiento cero” (zero knowledge) en el sentido de que mantengan la computación privada. Más bien, utilizan algoritmos ZK para producir una prueba sucinta de que el programa se ejecutó correctamente con una entrada determinada, de modo que un verificador pueda corroborar la computación con un esfuerzo exponencialmente menor. Aunque revelar la entrada del programa es opcional, evitar fugas accidentales de datos y lograr que múltiples partes acuerden un estado privado son problemas de ingeniería muy desafiantes que aún presentan retos sin resolver y limitaciones de escalabilidad.

Una ZKVM “computa” cada paso en el opcode, y luego aplica restricciones (constrains) para garantizar que el opcode se ejecutó correctamente. Las restricciones deben diseñarse de tal manera que podamos trabajar con una secuencia de opcodes arbitraria pero válida.

Podemos pensar en una ZKVM como una serie de transiciones de “estado”. La “función de transición de estado” toma el estado anterior y el opcode actual que se va a ejecutar, y genera un nuevo estado. Una ZKVM implementa la “función de transición de estado” y las restricciones del circuito que modelan su comportamiento. Ten en cuenta que el “estado” puede incluir cosas como el “program counter” u otros registros (bookkeeping) necesarios para que la VM funcione correctamente.

Este tutorial construirá una ZKVM extremadamente simple que solo soporta aritmética básica pero es extensible a otros opcodes. La VM que se presenta aquí solo tiene un stack (pila) y no tiene memoria ni almacenamiento. Al final del artículo ofrecemos sugerencias para profundizar en el estudio de las ZKVM.

Requisitos previos

Este tutorial asume conocimientos básicos sobre el funcionamiento de la EVM (o de alguna otra arquitectura basada en stack, como la Java Virtual Machine). Nos basamos en gran medida en el ejemplo de stack del capítulo anterior, por lo que asumimos su conocimiento.

ZKVM simple basada en stack

Construiremos una ZKVM simple basada en stack con una signal de propósito especial que contiene el resultado de la computación. A la VM se le suministra una serie de opcodes y números, y luego emite el resultado final a una signal especial que llamamos out.

Nuestra ZKVM solo tiene los siguientes opcodes:

• PUSH (introduce el primer argumento en el stack)
• ADD (extrae los dos elementos superiores del stack e introduce su suma)
• MUL (extrae los dos elementos superiores del stack e introduce su producto)
• NOP (sin operación, no hace nada)

Por simplicidad, todos los opcodes toman un único argumento, pero solo PUSH hace uso del argumento. El resto de las instrucciones ignoran el argumento. La razón por la que proporcionamos argumentos a opcodes que no los utilizan es para no tener que comprobar condicionalmente si el argumento está presente o no, en función del opcode.

No existe un opcode STOP ni RETURN (el sustituto se explicará en breve). La VM toma un argumento steps y devuelve cualquier valor que se encuentre en la parte inferior del stack después de ejecutar tantas instrucciones como indique steps.

La siguiente animación muestra un ejemplo sencillo de la suma de dos números en esta arquitectura:

En Circom, los bucles no pueden ser de longitud variable, siempre deben ejecutarse durante un número fijo de iteraciones, ya que el propio Rank 1 Constraint System (R1CS) subyacente debe ser de tamaño fijo. Del mismo modo, los programas no pueden ser de tamaño variable. Sin embargo, deben tener el mismo número de opcodes independientemente del programa que se ejecute.

Para ejecutar un programa con menos opcodes que el número fijo, simplemente lo rellenamos con NOP hasta que el programa alcance el tamaño máximo. Para saber cuándo “detener la ejecución”, el usuario debe suministrar el argumento steps mencionado anteriormente para determinar en qué momento se devolverá el valor de la parte inferior del stack.

Un par de notas sobre nuestra arquitectura:

• La VM está basada en stack, como la EVM, la Java Virtual Machine o (para los entendidos) una Reverse Polish Notation calculator.
• No hay instrucciones de salto (jump), por lo que el program counter solo se incrementa.
• Todos los opcodes toman un único argumento, pero ADD, MUL y NOP ignoran el argumento que se les pasa. Esto nos permite incrementar siempre el program counter en la misma cantidad cada vez — no tenemos que actualizar el program counter en 2 para un PUSH y en 1 para un ADD, y así sucesivamente. Siempre avanzamos el contador de 2 en 2.
• Para leer el argumento de PUSH, simplemente “miramos hacia adelante” (look ahead) un índice respecto al program counter.
• La suma y la multiplicación se realizan utilizando aritmética modular (el estándar por defecto en Circom). Utilizamos el orden del campo por defecto de Circom como nuestro “tamaño de palabra” (word size) — no intentamos emular VM que tienen tamaños de palabra tradicionales como 64 bits o 256 bits. Emular la computación con bits de un tamaño fijo es el tema del próximo capítulo.

Actualización de nuestro código de stack

Podemos hacer algunos cambios clave en nuestro código de stack del capítulo anterior para construir una ZKVM que cumpla con la especificación descrita anteriormente.

• Eliminamos el opcode POP ya que no es necesario.
• Añadimos un opcode ADD y MUL.

Recuerda que las reglas anteriores para copiar el stack previo eran:

• A. Si el sp es 1 o mayor, y la columna j está 1 índice por debajo de sp, y la instrucción actual es PUSH o NOP, debemos copiar la columna j
• B. Si el sp es 2 o mayor, y la columna j está 2 índices por debajo de sp, y la instrucción actual es POP, debemos copiar la columna j

La regla A permanece inalterada, pero la B necesita actualizarse a lo siguiente:

• B. si el sp es 2 o mayor, y la columna j está 3 índices por debajo de sp, y la instrucción actual es ADD o MUL, debemos copiar la columna j

La razón de este cambio es que la instrucción POP anterior no alteraba el penúltimo elemento del stack, solo eliminaba el elemento superior. Sin embargo, ADD efectivamente extrae dos elementos del stack y apila la suma. Del mismo modo, MUL extrae dos elementos del stack y apila el producto.

La implementación anterior del stack solo escribía nuevos valores en el stack pointer. Sin embargo, la nueva implementación puede escribir la suma o el producto dos índices por debajo del stack pointer. Por ejemplo, el 12 en el stack a continuación se convertirá en 15 después de la suma, y esa ubicación está dos índices por debajo del stack pointer:

Antes de la suma:

[12 , 3, sp] (sp = 3)

Después de la suma:

[15, sp] (sp = 2)

Aquí, tenemos 12 en el fondo del stack y sp apuntando al espacio vacío por encima del stack.

Por lo tanto, necesitamos una signal para indicar que una columna particular está dos elementos por debajo del stack pointer.

El siguiente código se deriva en gran medida del stack del capítulo anterior, pero implementa las actualizaciones descritas en este capítulo. Específicamente:

• Hemos reemplazado NOP, PUSH y POP con NOP, PUSH, ADD y MUL. ADD y MUL decrementan el stack pointer en uno, NOP mantiene el stack pointer igual, y PUSH incrementa el stack pointer en uno y copia su argumento en la parte superior del stack.

Copy
pragma circom 2.1.6;

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];
}

// i is the column number
// bits is how many bits we need
// for the LessEqThan component
template ShouldCopy(i, bits) {
  signal input sp;
  signal input is_push;
  signal input is_nop;
  signal input is_add;
  signal input is_mul;
  
  // out = 1 if should copy
  signal output out;
  
  // sanity checks
  is_add + is_mul + is_push + is_nop === 1;
  is_nop * (1 - is_nop) === 0;
  is_push * (1 - is_push) === 0;
  is_add * (1 - is_add) === 0;
  is_mul * (1 - is_mul) === 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 * spEqZero;
  
  // the current column is 1 or more 
  // below the stack pointer
  signal oneBelowSp <== LessEqThan(bits)([i, sp - 1]);
  
  // the current column is 3 or more
  // below the stack pointer
  signal threeBelowSP <== LessEqThan(bits)([i, sp - 3]);
  
  // 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] <== threeBelowSP;
  a3B.in[2] <== is_add + is_mul;
  
  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_add;
    signal input is_mul;
    signal input is_push;
    signal input is_nop;

    component ShouldCopys[m];
    signal copy[m];
    
    // loop over the columns
    for (var i = 0; i < m; i++) {
      ShouldCopys[i] = ShouldCopy(i, nBits);
      ShouldCopys[i].sp <== sp;
      ShouldCopys[i].is_add <== is_add;
      ShouldCopys[i].is_mul <== is_mul;
      ShouldCopys[i].is_push <== is_push;
      ShouldCopys[i].is_nop <== is_nop;
      out[i] <== ShouldCopys[i].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 ZKVM(n) {
  var NOP = 0;
  var PUSH = 1;
  var ADD = 2;
  var MUL = 3;

  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_ADD = 2;
  var IS_MUL = 3;
  var ARG = 4;
  signal metaTable[n][5];

  // 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
  sp[0] <== 0;
  sp[1] <== first_op_is_push;
  metaTable[0][IS_PUSH] <== first_op_is_push;
  metaTable[0][IS_NOP] <== 1 - first_op_is_push;
  metaTable[0][IS_ADD] <== 0;
  metaTable[0][IS_MUL] <== 0;
  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 metaTable and the stack pointer
  component EqPush[n];
  component EqNop[n];
  component EqAdd[n];
  component EqMul[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;
  }

  component eqSPMinus2[n][n];
  signal eqSPMinus2AndIsAdd[n][n];
  signal eqSPMinus2AndIsMul[n][n];
  for (var i = 0; i < n; i++) {
    eqSPMinus2AndIsAdd[0][i] <== 0;
    eqSPMinus2AndIsMul[0][i] <== 0;
  }

  // (the current column = sp - 2 and is_add) * sum
  signal eqSPMinus2AndIsAddWithValue[n][n];
  signal eqSPMinus2AndIsMulWithValue[n][n];

  signal sum_result[n][n];
  signal mul_result[n][n];
  for (var i = 0; i < n; i++) {
    eqSPMinus2AndIsAddWithValue[0][i] <== 0;
    eqSPMinus2AndIsMulWithValue[0][i] <== 0;
    sum_result[0][i] <== 0;
    mul_result[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;

    EqAdd[i] = IsEqual();
    EqAdd[i].in[0] <== instr[2 * i];
    EqAdd[i].in[1] <== ADD;
    metaTable[i][IS_ADD] <== EqAdd[i].out;

    EqMul[i] = IsEqual();
    EqMul[i].in[0] <== instr[2 * i];
    EqMul[i].in[1] <== MUL;
    metaTable[i][IS_MUL] <== EqMul[i].out;

    // carry out the sums and muls
    for (var j = 0; j < n - 1; j++) {
      sum_result[i][j] <== stack[i - 1][j] + stack[i - 1][j + 1];
      mul_result[i][j] <== stack[i - 1][j] * stack[i - 1][j + 1];
    }

    // these values cannot be used in practice because
    // the stack doesn't go that high.
    // However, we still need to initialize
    // them because every column checks
    // if it is sp - 1, even the last 2
    for (var j = n - 1; j < n; j++) {
      sum_result[i][j] <== 0;
      mul_result[i][j] <== 0;
    }

    // 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_add <== metaTable[i][IS_ADD];
    CopyStack[i].is_mul <== metaTable[i][IS_MUL];
    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];

      // check if the column is two less
      // than the stack pointer
      // if so, we prepare to write the sum or
      // product here
      // if the current instruction is add or mul
      eqSPMinus2[i][j] = IsEqual();
      eqSPMinus2[i][j].in[0] <== j;
      eqSPMinus2[i][j].in[1] <== sp[i] - 2; // underflow doesn't matter

      eqSPMinus2AndIsAdd[i][j] <== eqSPMinus2[i][j].out * metaTable[i][IS_ADD];
      eqSPMinus2AndIsMul[i][j] <== eqSPMinus2[i][j].out * metaTable[i][IS_MUL];

      eqSPMinus2AndIsAddWithValue[i][j] <== eqSPMinus2AndIsAdd[i][j] * sum_result[i][j];
      eqSPMinus2AndIsMulWithValue[i][j] <== eqSPMinus2AndIsMul[i][j] * mul_result[i][j];
      // we will either
      // - PUSH 
      // - COPY or implicilty assign 0
      // - ADD
      // - MUL
      stack[i][j] <== eqSPAndIsPush[i][j] * metaTable[i][ARG] + previousCellIfShouldCopy[i][j] + eqSPMinus2AndIsAddWithValue[i][j] + eqSPMinus2AndIsMulWithValue[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_ADD] + metaTable[i][IS_MUL]) * (sp[i] - 1);
    sp[i + 1] <== spBranch[i][INC] + spBranch[i][SAME] + spBranch[i][DEC];
  }
}

component main = ZKVM(5);

/* INPUT = {
    "instr": [1,3,1,6,1,2,3,0,3,0]
} */

¿No es ineficiente tener una restricción para cada opcode si solo usamos uno?

En nuestra ZKVM, realizamos una suma y una multiplicación para cada elemento del stack, aunque en realidad solo usemos uno de ellos. Esto no tiene gran impacto para una operación muy ligera como la suma o la multiplicación. Sin embargo, si tuviéramos un opcode para una operación pesada como un hashing, esto generaría significativamente más restricciones (constraints); tendríamos que instanciar un circuito de hashing para cada elemento del stack, aunque solo sea necesario aplicar el hash en la parte superior del stack. Todo esto resultará en cálculos innecesarios y una alta sobrecarga computacional.

Podemos mejorar la eficiencia utilizando un selector Quin (o dos) para determinar qué elementos del stack serán las entradas para el opcode, pero esto todavía significa que cada iteración del stack necesita restricciones para un hash, incluso si no los usa.

Dejamos como ejercicio para el lector implementar dos selectores Quin para sumar o multiplicar únicamente los dos elementos superiores del stack en lugar de todo el stack.

Esta ineficiencia de repetir innecesariamente restricciones no utilizadas es un inconveniente grave del R1CS estándar (vanilla), el cual no permite el uso condicional de restricciones.

Soluciones para mejorar la eficiencia

Dos enfoques modernos para mejorar drásticamente la eficiencia son las restricciones basadas en lookup tables (tablas de búsqueda) y las recursive proofs (pruebas recursivas).

• Una lookup table es un esquema de aritmetización donde solo las restricciones que realmente se usan forman parte de una tabla, y luego la prueba ZK demuestra que utilizó la entrada correcta de la tabla en cada instrucción.
• Una recursive proof crea una prueba ZK independiente para cada instrucción y luego combina la prueba con otra prueba ZK que verifica que las pruebas de entrada son válidas. (Ten en cuenta que el algoritmo de verificación en ZK puede modelarse en sí mismo con un circuito aritmético).

Estas mejoras son el tema de partes posteriores del libro de ZK. Sin embargo, el proceso de pensamiento detrás de modelar cómo se ve una transición de estado válida en una VM se generaliza a las VM actuales.

Aprende más sobre las ZKVM

La primera propuesta para una ZKVM fue TinyRAM, propuesta en un documento Snarks for C: verifying Program Executions Succinctly and in Zero Knowledge. Los autores crearon, en sus palabras “una máquina de acceso aleatorio RISC minimalista con una Harvard architecture y memoria de acceso aleatorio direccionable por palabras”. La TinyRAM specification requiere solo 29 opcodes.

Dado que este artículo impulsó la investigación sobre las ZKVM, es un documento de alto impacto que vale la pena entender.

La mayoría de las ZKVM modernas están basadas en la arquitectura RISC-V, pero también existen ZKVM con arquitectura MIPS. Las blockchains de capa 2 ZK a menudo utilizan su propia arquitectura personalizada.

El video de Ye Zhang sobre cómo Scroll creó una ZKEVM también es bastante accesible para lograr una comprensión de alto nivel.