Comment fonctionne le processus de preuve d'exécution basé sur STARK sur Miden V1 ?

Miden est une solution d'implémentation ZKVM basée sur la technologie.

Dans sa couche de base, la preuve brute est générée sur la base de la bibliothèque ZKP et la preuve sera vérifiée. La partie pointillée dans la figure 1 suivante est la fonction principale implémentée par Miden. Il se compose principalement de trois éléments.

1. Un ensemble de compilateurs de syntaxe lexicale, c'est-à-dire l'analyseur lexical et l'analyseur syntaxique de la figure 1. Ils peuvent programmer les instructions d'assemblage définies par Miden dans le bloc de code ou l'opcode et la valeur op contenus dans le bloc.

2. Un ensemble d'exécuteurs d'instructions, c'est-à-dire l'exécuteur de la figure 1. Il exécutera le bloc de code et l'opcode et la valeur op contenus dans le bloc selon les règles définies. Et les résultats exécutés seront la trace d'exécution utilisée pour générer la preuve.

3. Un ensemble d'AIR (Abstract Inter-mediate Representation), satisfaisant aux exigences de la preuve absolue, c'est l'AIR de la figure 1. Il exerce des contraintes sur le processus d'exécution de la machine virtuelle Miden.

Figure 1. Composantes du projet Miden

Dessin de conception structurelle AIR

Les contraintes d'AIR se divisent en pile et décodeur : la figure 2 montre les contraintes de la pile, réparties avec une pile avec une profondeur supérieure de 8 à l'initialisation.

Le max_depth est incrémenté au besoin si la distribution initiale peut être dépassée lors de l'exécution, selon les besoins du programme, mais il ne doit pas dépasser la profondeur maximale de 16, sinon, une erreur est signalée.

Figure 2 : Colonne de contrainte de pile

Comme on peut le voir ci-dessous, la figure 3 montre les contraintes du décodeur. Parmi ces contraintes, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS et hd_OP_bits sont des longueurs de colonne fixes.

L'op_sponge est utilisé pour contraindre l'ordre et l'exactitude des instructions. Le cf_op_bits contraint le flow_ops 3 bits. Les ld_op_bits et hd_op_bits contraignent les 5 bits de poids faible et les 2 bits de poids fort de user_ops, respectivement.

Les ld_op_bits et hd_op_bits se combinent pour former un user_op exécutable qui est également utilisé comme sélecteur pour chaque étape des contraintes d'état de la pile !

Figure 3 : Colonne de contrainte du décodeur

Exemple de processus d'exécution de Miden VM

Cette section montre une logique Miden simple pour illustrer l'exécution de la machine virtuelle et la génération de la trace d'exécution de stark.

Le segment de code suivant 1 est le segment à exécuter : Sa logique d'exécution est de pousser 3 et 5 sur la pile. Ensuite, lisez le drapeau sur la bande.

Vérifiez si le drapeau est 1 ou 0. Si c'est 1, exécutez la "logique if.true" pour prendre les deux nombres 3 et 5 qui sont poussés sur la pile, additionnez-les, ce qui donne 8, et poussez 8 sur le empiler. Si c'est 0, exécutez la "logique sinon" pour prendre les nombres 3 et 5 et les multiplier ensemble, ce qui donne 15, puis poussez 15 sur la pile.

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

Segment de code 1

Le code d'instruction final analysé par l'analyseur lexical et l'analyseur syntaxique de Miden est présenté dans le segment de code 2 suivant :

 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]

Segment de code 2

La figure 4 montre le processus de la machine virtuelle exécutant le segment de code 2.

La partie centrale est l'organigramme de l'exécuteur exécutant les opcodes. Les lignes pointillées de gauche font référence à la trace du décodeur générée lors de l'exécution du code. Les lignes droites en pointillés font référence à la trace de pile générée lors de l'exécution du code.

Dans la figure, l'exécuteur effectue les exécutions bloc par bloc selon le bloc de code. Dans cet exemple, un bloc span est exécuté en premier.

Ensuite, la structure if-else-end à l'étape 32 est exécutée pour entrer dans le bloc de commutation et presser le hachage éponge généré par la dernière exécution du bloc d'étendue précédent dans le ctx_stack. Une fois le bloc de commutation exécuté, insérez-le dans l'éponge à l'étape 49.

Figure 4 : la figure de changement d'état de l'opcode d'exécution de la machine virtuelle

Remarque : Ce document décrit la dernière version de la branche principale pour les projets Miden au 2022-05-27. Jusqu'à présent, la branche suivante de Miden a fait beaucoup de refonte des instructions, et AIR n'a mis en place que quelques contraintes.

Conditions de contrainte de la pile

Dans cette section, nous montrerons les conditions de contrainte des principales instructions d'opération utilisateur, parmi lesquelles, old_stack_x fait référence à la valeur stockée à la position x de la pile avant l'exécution de l'instruction, new_stack_x fait référence à la valeur stockée à la position x de la pile. pile après l'exécution de l'instruction, "–>" fait référence à la copie de la valeur du côté gauche de la pile vers la droite, et "==" fait référence à la contrainte d'équation. Les contraintes de la pile sont relativement simples et aucune explication n'est requise.

Instruction d'état

Choisir

Contrainte:

 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 condition est 1, x est en haut de la pile. Si la condition est 0, y est en haut de la pile.

Enseignement de l'arithmétique

ajouter

Contrainte:

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

mul

Contrainte:

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

inv

Contrainte:

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

négatif

Contrainte:

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

Instruction booléenne

ne pas

Contrainte:

 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

et

Contrainte:

 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

Contrainte:

 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

Instruction de hachage

RESCR

Limiter le hachage de la fonction satisfaisant au protocole de la fonction de hachage
Occupant 6 registres.

Contrainte:

 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

Comparer les instructions

éq

Contrainte:

 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

Comparez en fonction du cycle de longueur en bits des deux nombres à comparer, par exemple :

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

Les instructions de comparaison doivent être exécutées quatre fois.

Contrainte:

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

Instruction d'opération de pile

dup.n

Contrainte:

 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

échanger

Contrainte:

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

ROULEAU4

Contrainte:

 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

Condition de contrainte du commentaire du décodeur

Dans cette section, nous montrerons les conditions de contrainte de l'instruction d'opération Flow principale.

Exécution du code utilisateur

op_bits

Pour les contraintes de cf_op_bits, ld_op_bits et hd_op_bits
Contrainte 1 : chaque bit ne peut être que 0 ou 1.
Contrainte 2 : lorsque op_counter n'est pas 0, ld_ops et hd_ops ne peuvent pas être tous les deux 0.
Contrainte 3 : lorsque cf_op_bits est hacc, l'état op_counter augmentera de 1.
Contrainte 4 : Les instructions BEGIN, LOOP, BREAK et WRAP doivent être alignées selon 16.
Contrainte 5 : Les instructions TEND et FEND doivent être alignées selon 16.
Contrainte 6 : L'instruction PUSH doit être alignée selon 8.

Contrainte:

 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 Commentaire

Hacc, comme le flowOps, provoquera toujours le changement d'état de l'éponge lors de l'exécution de cette instruction, et il est donc nécessaire d'effectuer les contraintes.

Contrainte:

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

Jugement conditionnel

tendre

En tant que contrainte de la vraie fin de branche de if, elle est divisée en deux parties :
Contrainte 1 : est la contrainte de l'état éponge.

La valeur en haut de la pile est égale à new_sponge_0. L'éponge après la dernière exécution de la vraie branche de if est égale à new_sponge_1. New_sponge_3 est égal à 0.

Contrainte 2 : est la contrainte de ctx_stack. La valeur en haut de la pile est égale à new_sponge_0. Tout autre élément de la pile se déplacera d'une position vers le haut de la pile.

Contrainte 3 : est la contrainte de loop_stack. L'état de loop_stack est immuable.

Contrainte:

 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

repousser

Quant à la contrainte de fin de fausse branche de if, elle est divisée en deux parties :
Contrainte 1 : est la contrainte de l'état éponge. La valeur en haut de la pile est égale à new_sponge_0.

L'éponge après la dernière exécution de la vraie branche de if est égale à new_sponge_2. new_sponge_3 est égal à 0.

Contrainte 2 : est la contrainte de ctx_stack. La valeur en haut de la pile est égale à new_sponge_0. Tout autre élément de la pile se déplacera d'une position vers le haut de la pile.

Contrainte 3 : est la contrainte de loop_stack. L'état de loop_stack est inchangé.

Contrainte:

 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