Como o processo de prova de execução baseado em STARK funciona no Miden V1?

Miden é uma solução de implementação ZKVM totalmente baseada em tecnologia.

Em sua camada básica, a prova stark é gerada com base na biblioteca ZKP e a prova será verificada. A parte pontilhada na Figura 1 a seguir é a principal função implementada pelo Miden. Consiste principalmente em três componentes.

1. Um conjunto de compiladores de sintaxe léxica, que é o analisador léxico e o analisador de sintaxe na Figura 1. Eles podem programar as instruções de montagem definidas por Miden em codeblock ou o opcode e o valor op contidos no bloco.

2. Um conjunto de executores de instruções, que é o executor da Figura 1. Ele executará o codeblock e o opcode e op value contidos no bloco de acordo com as regras definidas. E os resultados executados serão o trace de execução usado para gerar a prova.

3. Um conjunto de AIR (Abstract Intermediate Representation), satisfazendo os requisitos da prova total, ou seja, o AIR da Figura 1. Conduz restrições ao processo de execução da Máquina Virtual Miden.

Figura 1. Componentes do projeto Miden

Desenho de Projeto Estrutural AIR

As restrições do AIR se dividem em pilha e decodificador: A Figura 2 mostra as restrições da pilha, distribuídas com uma pilha com profundidade superior de 8 na inicialização.

O max_depth é incrementado conforme necessário caso a distribuição inicial possa ser excedida durante a execução, dependendo da necessidade do programa, mas não deve ultrapassar a profundidade máxima de 16, caso contrário, um erro é reportado.

Figura 2: Coluna de restrição de pilha

Como pode ser visto abaixo, a Figura 3 mostra as restrições do decodificador. Entre essas restrições, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS e hd_OP_bits são comprimentos de coluna fixos.

O op_sponge é usado para restringir a ordem e a exatidão das instruções. O cf_op_bits restringe o flow_ops de 3 bits. Os ld_op_bits e hd_op_bits restringem os 5 bits baixos e os 2 bits altos de user_ops, respectivamente.

Os ld_op_bits e hd_op_bits se combinam para formar um user_op executável que também é usado como um seletor para cada etapa das restrições de estado da pilha!

Figura 3: Coluna de restrição do decodificador

Exemplo de processo de execução da VM Miden

Esta seção mostra a lógica Miden simples para ilustrar a execução da máquina virtual e a geração do rastreamento de execução de stark.

O seguinte segmento de código 1 é o segmento a ser executado: Sua lógica de execução é empurrar 3 e 5 na pilha. Em seguida, leia a bandeira da fita.

Verifique se o sinalizador é 1 ou 0. Se for 1, execute a "lógica if.true" para pegar os dois números 3 e 5 que são colocados na pilha, some-os, resultando em 8, e empurre 8 no pilha. Se for 0, execute a "lógica else" para pegar os números 3 e 5 e multiplicá-los, resultando em 15 e, em seguida, empurre 15 na pilha.

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

Segmento de código 1

O código de instrução final analisado pelo analisador léxico e pelo analisador de sintaxe de Miden é mostrado no seguinte 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

A Figura 4 mostra o processo da máquina virtual executando o segmento de código 2.

A parte do meio é o fluxograma do executor executando opcodes. As linhas pontilhadas à esquerda referem-se ao rastreamento do decodificador gerado na execução do código. As linhas pontilhadas à direita referem-se ao rastreamento de pilha gerado na execução do código.

Na figura, o executor conduz as execuções bloco a bloco de acordo com o bloco de código. Neste exemplo, um bloco span é executado primeiro.

Em seguida, a estrutura if-else-end na etapa 32 é executada para inserir o bloco switch e pressionar o hash de esponja gerado pela última execução do bloco span anterior no ctx_stack. Depois que o bloco switch for executado, coloque-o na esponja na etapa 49.

Figura 4: a figura de mudança de estado da VM executando o opcode

Nota: Este documento descreve a versão mais recente da ramificação principal para projetos Miden a partir de 2022-05-27. Até agora, a próxima ramificação de Miden fez muito redesenho de instruções e o AIR implementou apenas algumas restrições.

Condições de Restrição da Pilha

Nesta seção, mostraremos as condições de restrição das principais instruções de operação do usuário, entre as quais, old_stack_x refere-se ao valor armazenado na posição x da pilha antes da execução da instrução, new_stack_x refere-se ao valor armazenado na posição x do pilha após a execução da instrução, “–>” refere-se à cópia do valor do lado esquerdo da pilha para a direita e “==” refere-se à restrição da equação. As restrições da pilha são relativamente simples e nenhuma explicação é necessária.

Instrução de condição

Escolher

Restrição:

 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

Se a condição for 1, x estará no topo da pilha. Se a condição for 0, y está no topo da pilha.

instrução aritmética

adicionar

Restrição:

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

mul

Restrição:

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

inv

Restrição:

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

negativo

Restrição:

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

Instrução Bool

não

Restrição:

 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

e

Restrição:

 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

ou

Restrição:

 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

Instrução Hash

RESCR

Função de limite de hash que satisfaça o protocolo de função de hash
Ocupando 6 registros.

Restrição:

 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

Instrução de Comparação

equação

Restrição:

 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 acordo com o ciclo de comprimento de bit dos dois números a serem comparados, como:

R: [0,1,0,1]
B: [0,0,1,1]

As instruções de comparação precisam ser executadas quatro vezes.

Restrição:

 // 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

Instrução de operação de pilha

dup.n

Restrição:

 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

troca

Restrição:

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

ROLO4

Restrição:

 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

Condição de restrição do comentário do decodificador

Nesta seção, mostraremos as condições de restrição da instrução principal da operação Flow.

Execução do código do usuário

op_bits

Para as restrições de cf_op_bits, ld_op_bits e hd_op_bits
Restrição 1: cada bit só pode ser 0 ou 1.
Restrição 2: quando op_counter não é 0, ld_ops e hd_ops não podem ser ambos 0.
Restrição 3: quando cf_op_bits for hacc, o estado op_counter aumentará em 1.
Restrição 4: As instruções BEGIN, LOOP, BREAK e WRAP precisam ser alinhadas de acordo com 16.
Restrição 5: As instruções TEND e FEND precisam ser alinhadas de acordo com 16.
Restrição 6: A instrução PUSH precisa ser alinhada de acordo com 8.

Restrição:

 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 Comentário

O Hacc, assim como o flowOps, sempre causará a mudança de estado da esponja ao conduzir esta instrução, e por isso é necessário realizar as restrições.

Restrição:

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

Julgamento Condicional

tratar

Como a restrição do verdadeiro final da ramificação de if, ela é dividida em duas partes:
Restrição 1: é a restrição do estado esponja.

O valor no topo da pilha é igual a new_sponge_0. A esponja após a última execução da ramificação verdadeira de if é igual a new_sponge_1. New_sponge_3 é igual a 0.

Restrição 2: é a restrição de ctx_stack. O valor no topo da pilha é igual a new_sponge_0. Qualquer outro elemento na pilha se moverá uma posição para o topo da pilha.

Restrição 3: é a restrição de loop_stack. O estado de loop_stack é imutável.

Restrição:

 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

f_end

Como a restrição do fim do ramo falso de if, ela é dividida em duas partes:
Restrição 1: é a restrição do estado esponja. O valor no topo da pilha é igual a new_sponge_0.

A esponja após a última execução da ramificação verdadeira de if é igual a new_sponge_2. new_sponge_3 é igual a 0.

Restrição 2: é a restrição de ctx_stack. O valor no topo da pilha é igual a new_sponge_0. Qualquer outro elemento na pilha se moverá uma posição para o topo da pilha.

Restrição 3: é a restrição de loop_stack. O estado de loop_stack permanece inalterado.

Restrição:

 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