¿Cómo funciona el proceso de prueba de ejecución basado en STARK en Miden V1?

Miden es una solución de implementación de ZKVM basada en tecnología rígida.

En su capa básica, la prueba cruda se genera en base a la biblioteca ZKP y la prueba será verificada. La parte punteada en la siguiente Figura 1 es la función principal implementada por Miden. Consta principalmente de tres componentes.

1. Un conjunto de compiladores de sintaxis léxica, que es el analizador léxico y el analizador sintáctico de la Figura 1. Pueden programar las instrucciones de ensamblaje definidas por Miden en el bloque de código o el código de operación y el valor de operación contenidos en el bloque.

2. Un conjunto de ejecutores de instrucciones, que es el ejecutor de la Figura 1. Ejecutará el bloque de código y el código de operación y el valor de operación contenidos en el bloque de acuerdo con las reglas definidas. Y los resultados ejecutados serán el seguimiento de ejecución utilizado para generar la prueba.

3. Un conjunto de AIR (Representación intermedia abstracta), que satisface los requisitos de la prueba estricta, que es el AIR en la Figura 1. Conduce restricciones al proceso de ejecución de la máquina virtual de Miden.

Figura 1. Componentes del proyecto Miden

Dibujo de diseño estructural de AIRE

Las restricciones de AIR se dividen en pila y decodificador: la Figura 2 muestra las restricciones de la pila, distribuidas con una pila con una profundidad superior de 8 en la inicialización.

La profundidad máxima se incrementa según sea necesario si la distribución inicial se puede exceder durante la ejecución, según las necesidades del programa, pero no debe exceder la profundidad máxima de 16, de lo contrario, se informa un error.

Figura 2: columna de restricción de pila

Como se puede ver a continuación, la Figura 3 muestra las limitaciones del decodificador. Entre estas restricciones, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS y hd_OP_bits son longitudes de columna fijas.

El op_sponge se usa para restringir el orden y la corrección de las instrucciones. El cf_op_bits restringe el flow_ops de 3 bits. Los ld_op_bits y hd_op_bits restringen los 5 bits bajos y los 2 bits altos de user_ops, respectivamente.

¡Los ld_op_bits y hd_op_bits se combinan para formar un user_op ejecutable que también se usa como selector para cada paso de las restricciones de estado de la pila!

Figura 3: Columna de la restricción del decodificador

Ejemplo de proceso de ejecución de Miden VM

Esta sección muestra la lógica Miden simple para ilustrar la ejecución de la máquina virtual y la generación del seguimiento de ejecución de Stark.

El siguiente segmento de código 1 es el segmento a ejecutar: Su lógica de ejecución es empujar 3 y 5 en la pila. Luego lea la bandera de la cinta.

Verifique si el indicador es 1 o 0. Si es 1, ejecute la "lógica if.true" para tomar los dos números 3 y 5 que están en la pila, súmelos, lo que da como resultado 8, y presione 8 en el pila. Si es 0, ejecute la "lógica de lo contrario" para tomar los números 3 y 5 y multiplíquelos dando como resultado 15, y luego empuje 15 en la pila.

 begin push.3 push.5 read if.true add else mul end end

Segmento de código 1

El código de instrucción final analizado por el analizador léxico y el analizador de sintaxis de Miden se muestra en el siguiente segmento de código 2:

 begin noop noop noop noop noop noop noop push(3) noop noop noop noop noop noop noop push(5) read noop noop noop noop noop noop noop noop noop noop noop noop noop, if assert add noop noop noop noop noop noop noop noop noop noop noop noop noop else not assert mul noop noop noop noop noop noop noop noop noop noop noop noop end]

Segmento de código 2

La figura 4 muestra el proceso de la máquina virtual que ejecuta el segmento de código 2.

La parte central es el diagrama de flujo del ejecutor ejecutando códigos de operación. Las líneas punteadas de la izquierda se refieren al seguimiento del decodificador generado en la ejecución del código. Las líneas de puntos y rayas de la derecha se refieren al seguimiento de la pila generado en la ejecución del código.

En la figura, el ejecutor realiza ejecuciones bloque por bloque de acuerdo con el bloque de código. En este ejemplo, primero se ejecuta un bloque de intervalo.

Luego, se realiza la estructura if-else-end en el paso 32 para ingresar al bloque switch y presionar el hash de esponja generado por la última ejecución del bloque span anterior en ctx_stack. Después de ejecutar el bloque de cambio, colóquelo en la esponja en el paso 49.

Figura 4: la figura de cambio de estado de la máquina virtual que ejecuta el código de operación

Nota: Este documento describe la última versión de la rama principal para proyectos de Miden a partir del 27 de mayo de 2022. Hasta ahora, la siguiente rama de Miden ha rediseñado mucho las instrucciones y AIR ha implementado solo algunas restricciones.

Condiciones de restricción de la pila

En esta sección, mostraremos las condiciones de restricción de las principales instrucciones de operación del Usuario, entre las cuales, old_stack_x se refiere al valor almacenado en la posición x de la pila antes de la ejecución de la instrucción, new_stack_x se refiere al valor almacenado en la posición x de la pila. pila después de la ejecución de la instrucción, “–>” se refiere a la copia del valor del lado izquierdo de la pila a la derecha, y “==” se refiere a la restricción de la ecuación. Las restricciones de la pila son relativamente simples y no se requiere explicación.

Instrucción de condición

Elegir

Restricción:

 new_stack_0 == (condition * x) + ((1 - condition) * y) old_stack_0 == x old_stack_1 == y old_stack_2 == condition old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2 aux_0 == condition.is_binary == true

Si la condición es 1, x está en la parte superior de la pila. Si la condición es 0, y está en la parte superior de la pila.

instrucción aritmética

agregar

Restricción:

 old_stack_0 + old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

Mul

Restricción:

 old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

inversión

Restricción:

 old_stack_0 * new_stack_0 == 1 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

negativo

Restricción:

 old_stack_0 + new_stack_0 == 0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

Instrucción booleana

no

Restricción:

 aux_0: make sure old_stack_0 is binary 1-old_stack_0 == new_stack_0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

y

Restricción:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

o

Restricción:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary 1- (1-old_stack_0) *(1- old_stack_1) == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

Instrucción hash

RESCR

Hash de función de límite que satisface el protocolo de función de hash
Ocupando 6 registros.

Restricción:

 hash(old_stack0，old_stack1， old_stack2， old_stack3， old_stack3， old_stack5) == （new_stack0，new_stack1， new_stack2， new_stack3， new_stack3， new_stack5） old_stack_6 --> new_stack_6 old_stack_n. --> new_stack_n

Comparar instrucción

equivalente

Restricción:

 aux_0 == new_stack_0 * diff == 0 new_stack_0 == 1- (old_stack_1-old_stack_2)*old_stack_0 old_stack_0 == inv(old_stack_1-old_stack_2) old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2

cmp

Compare de acuerdo con el ciclo de longitud de bit de los dos números a comparar, como:

R: [0,1,0,1]
segundo: [0,0,1,1]

Las instrucciones de comparación deben ejecutarse cuatro veces.

Restricción:

 // layout of first 8 registers // [pow, bit_a, bit_b, not_set, gt, lt, acc_b, acc_a] // x and y bits are binary new_stack_1 == x_big_idx(lg lt flag) （type:binary) new_stack_2 == y_big_idx(lg lt flag) （type:binary) bit_gt = x_big_idx*(1-y_big_idx) bit_lt = y_big_idx*(1-x_big_idx) // comparison trackers were updated correctly new_stack_3 = not_set_idx new_stack_4(gt) == old_stack_4(gt_idx) + bit_gt * not_set_idx new_stack_5(lt) == old_stack_5(lt_idx) + bit_lt * not_set_idx // binary representation accumulators were updated correctly old_stack_0 = POW2_IDX old_stack_6 = Y_ACC_IDX old_stack_7 = X_ACC_IDX new_stack_6 == old_stack_6 + x_big_idx * old_stack_0(power_of_two); new_stack_7 == old_stack_7 + y_big_idx * old_stack_0(power_of_two); // when GT or LT register is set to 1, not_set flag is cleared not_set_check = (1-old_stack_5(lt_idx))*(1-old_stack_4(gt_idx)) not_set_check == new_stack_3(not_set_idx) // power of 2 register was updated correctly new_stack[POW2_IDX] * two == old_stack[POW2_IDX] old_stack_8 --> new_stack_8 old_stack_n --> new_stack_n

Instrucción de operación de pila

dup.n

Restricción:

 new_stack_0 == old_stack_0 ... new_stack_n-1 == old_stack_n-1 old_stack_0 --> new_stack_n old_stack_k --> new_stack_n+k

intercambio

Restricción:

 new_stack_0 == old_stack_1 new_stack_1 == old_stack_0 old_stack_2 --> new_stack_2 old_stack_n --> new_stack_n

ROLL4

Restricción:

 new_stack_0 == old_stack_3 new_stack_1 == old_stack_0 new_stack_2 == old_stack_1 new_stack_3 == old_stack_2 old_stack_4 --> new_stack_4 old_stack_n --> new_stack_n

Condición de restricción del comentario del decodificador

En esta sección, mostraremos las condiciones de restricción de la instrucción de operación de Flujo principal.

Ejecución de código de usuario

op_bits

Para las restricciones de cf_op_bits, ld_op_bits y hd_op_bits
Restricción 1: cada bit solo puede ser 0 o 1.
Restricción 2: cuando op_counter no es 0, ld_ops y hd_ops no pueden ser ambos 0.
Restricción 3: cuando cf_op_bits es hacc, el estado de op_counter aumentará en 1.
Restricción 4: las instrucciones BEGIN, LOOP, BREAK y WRAP deben alinearse de acuerdo con 16.
Restricción 5: las instrucciones TEND y FEND deben alinearse de acuerdo con 16.
Restricción 6: la instrucción PUSH debe alinearse de acuerdo con 8.

Restricción:

 cf_op_bits == binary ld_op_bits == binary hd_op_bits == binary // ld_ops and hd_ops can be all 0s at the first step, but cannot be all 0s at any other step op_counter * binary_not(ld_bit_prod) * binary_not(hd_bit_prod) == 0 if op_counter != 0 (1-ld_bit_prod)*(1- hd_bit_prod) == 0 if is_hacc != true op_counter = current.op_counter // BEGIN, LOOP, BREAK, and WRAP are allowed only on one less than multiple of 16 // TEND and FEND is allowed only on multiples of 16 // PUSH is allowed only on multiples of 8

hacc comentario

Hacc, como flowOps, siempre provocará el cambio de estado de la esponja al realizar esta instrucción y, por lo tanto, es necesario realizar las restricciones.

Restricción:

 mds(sbox(old_sponge) + user_opcode(7bits) + op_value(push_flag=1)) == sbox(inv_mds(new_sponge))

Sentencia de condición

tender

Como la restricción del final de la rama verdadera de if, se divide en dos partes:
Restricción 1: es la restricción del estado esponja.

El valor en la parte superior de la pila es igual a new_sponge_0. La esponja después de la última ejecución de la rama verdadera de if es igual a new_sponge_1. New_sponge_3 es igual a 0.

Restricción 2: es la restricción de ctx_stack. El valor en la parte superior de la pila es igual a new_sponge_0. Cualquier otro elemento en la pila se moverá una posición hacia la parte superior de la pila.

Restricción 3: es la restricción de loop_stack. El estado de loop_stack no cambia.

Restricción:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[1] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n

defenderse

Como la restricción del final de la rama falsa de if, se divide en dos partes:
Restricción 1: es la restricción del estado esponja. El valor en la parte superior de la pila es igual a new_sponge_0.

La esponja después de la última ejecución de la rama verdadera de if es igual a new_sponge_2. new_sponge_3 es igual a 0.

Restricción 2: es la restricción de ctx_stack. El valor en la parte superior de la pila es igual a new_sponge_0. Cualquier otro elemento en la pila se moverá una posición hacia la parte superior de la pila.

Restricción 3: es la restricción de loop_stack. El estado de loop_stack no cambia.

Restricción:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[2] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n