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

Flow

Dash

Assembly

Trace

2022 - HackerNoon Contributor of the Year - Algorithms

2022 - HackerNoon Contributor of the Year - Architecture

2022 - HackerNoon Contributor of the Year - Blockchain

2022 - HackerNoon Contributor of the Year - Optimization

2022 - HackerNoon Contributor of the Year - Privacy

Nominated for 2022 - HackerNoon Contributor of the Year - Optimization

Nominated for 2022 - HackerNoon Contributor of the Year - Algorithms

Nominated for 2022 - HackerNoon Contributor of the Year - Privacy

Nominated for 2022 - HackerNoon Contributor of the Year - Architecture

Nominated for 2022 - HackerNoon Contributor of the Year - Blockchain

Este áudio é produzido no idioma original da história!

Muito longo; Para ler

Make resilience your competitive advantage

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

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

About Author

COMENTARIOS

Rótulos

ESTE ARTIGO FOI APRESENTADO EM

Related Stories

Crescimento de Criptomoedas: Criando Personas de Usuários Eficazes

Digital Nomads Ouçam: O que você precisa saber sobre o novo visto DTV da Tailândia

De fóruns a feeds: como os algoritmos de mídia social moldam a interação digital

Toque para ganhar: Telegram pode integrar os próximos 10 bilhões de usuários criptográficos antes de Solana

Crescimento de Criptomoedas: Criando Personas de Usuários Eficazes

Digital Nomads Ouçam: O que você precisa saber sobre o novo visto DTV da Tailândia

De fóruns a feeds: como os algoritmos de mídia social moldam a interação digital

Toque para ganhar: Telegram pode integrar os próximos 10 bilhões de usuários criptográficos antes de Solana

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps