Qu'est-ce qu'un jeu d'instructions TinyRAM ?

Introduction TinyRAM est un simple ordinateur à jeu d'instructions réduit (RISC) avec une mémoire à accès aléatoire adressable au niveau de l'octet et des bandes d'entrée. Il existe deux variantes de TinyRAM : l'une suit l'architecture Harvard (hv) et l'autre suit l'architecture von Neumann (vn) (dans cet article, nous nous concentrons principalement sur l'architecture von Neumann). Le projet SCIPR (Succinct Computational Integrity and Privacy Research) construit des mécanismes pour prouver l'exécution correcte des programmes TinyRAM, et TinyRAM est conçu pour être efficace dans ce contexte. Il établit un équilibre entre deux exigences opposées - "expressibilité suffisante" et "petit jeu d'instructions": Une expressibilité suffisante pour prendre en charge un code d'assemblage court et efficace lorsqu'il est compilé à partir de langages de programmation de haut niveau, Petit jeu d'instructions pour prendre en charge une vérification simple via des circuits arithmétiques et une vérification efficace à l'aide des algorithmes et des mécanismes cryptographiques de SCIPR. Dans cet article, nous compléterons l'article précédent plutôt qu'une introduction répétitive de TinyRAM, puis nous nous concentrerons sur l'introduction des instructions et des contraintes de circuit. Pour une introduction de base à TinyRAM, veuillez vous référer à notre article précédent : tinyram简介-中文 TinyRAM Review-English Jeu d'instructions TinyRAM TinyRAM prend en charge 29 instructions, chacune spécifiée par un opcode et jusqu'à 3 opérandes. L'opérande peut être soit le nom d'un registre (c'est-à-dire des entiers de 0 à K-1) soit une valeur immédiate (c'est-à-dire des chaînes de W bits). Sauf indication contraire, chaque instruction ne modifie pas le drapeau séparément et incrémente pc de i (i % 2^W) par défaut, i=2W/8 pour la vnTinyRAM. En général, le premier opérande est le registre cible pour le calcul des instructions et les autres opérandes spécifient les paramètres requis par les instructions. Enfin, toutes les instructions prennent un cycle de la machine pour s'exécuter. Opération liée aux bits : l'instruction stockera les bits et résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est , définissez sur 1, sinon définissez-le sur 0. et and ri rj A 0^{W} flag l'instruction stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est , définissez sur 1, sinon définissez-le sur 0. ou or ri rj A 0^{W} flag instruction stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est , définissez sur 1, sinon définissez-le sur 0. xor xor ri rj A 0^{W} flag instruction stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est , définissez sur 1, sinon définissez-le sur 0. not not ri A 0^{W} flag Opération relative aux entiers Il s'agit d'opérations liées à des nombres entiers non signés et signés. Dans chaque paramètre, si un débordement ou une erreur arithmétique se produit (comme une division par zéro), définissez sur 1 , sinon définissez-le sur 0. flag Dans la partie suivante, représente une suite d'entiers {0*,…,* $2^{W} -1 $} ; Ces entiers sont constitués de chaînes de W bits. représente une suite d'entiers {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1. Ces entiers sont également constitués de chaînes de W bits. U_{W} S_{W} l'instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1}⋯a_{0} est le W bit le moins significatif (LSB) de . De plus, sera défini sur . est le bit le plus significatif (MSB) de G. add : add ri rj A G = [rj]_u + [A]_u flag G_{W} G_{W} instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1}⋯a_{0} est le W bit le moins significatif (LSB) de . De plus, sera défini sur . est le bit le plus significatif (MSB) de G. sub : l' sub ri rj A G = [rj]_u + 2^W − [A]_u flag 1−G_{W} G_{W} L'instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1}⋯a_{0} est le W bit le moins significatif (LSB) de . De plus, sera mis à 1 si mull mull ri rj A G=[rj]_u∗[A]_u flag , sinon mettez-le à 0. [rj]_u × [A] {W} u ∉ U L'instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1}⋯a_{0} est le W bit le plus significatif (MSB) de . De plus, sera mis à 1 si , sinon mis à 0. umulh umulh ri rj A G = [rj]_u ∗ [A]_u flag [rj]_u × [A] {W} u ∉ U L'instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1} est le bit de signe de est le W - 1 MSB de . De plus, sera mis à 1 si } , sinon mis à 0. smulh smulh ri rj A [rj] {W−2}⋯a{0} u ∗ [A]u, a [rj]_u ∗ [A]_u flag [rj]_u × [A] {W u ∉ S instuction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. udiv udiv ri rj A Si . [A] {W−1}⋯a_{0} = 0^W u = 0, a Si est le seul codage binaire de l'entier Q, ce qui fait que pour certains entiers , la formule est réalisable. De plus, uniquement lorsque , l' sera défini sur 1. [A] {W−1}⋯a_{0} u∣ ≠ 0, a R ∈ {0,…,[A]_u − 1} [rj]_u = [A]_u × Q + R [A]_u=0 flag L'instruction stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. umod umod ri rj A Si . [A] {W−1}⋯a_{0} = 0^W u = 0, a Si dont la plage de valeurs est [A] {W−1}⋯a_{0} u∣ ≠ 0, a est le seul codage binaire de l'entier R, , rendant la formule réalisable pour certaines valeurs de Q. De plus, uniquement lorsque , l' sera défini sur 1. {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 flag Opération liée au quart de travail L'instruction stockera la chaîne de W bits obtenue par [rj] décalage vers la gauche pour [A] u bit dans le registre ri. Les positions vides après le décalage sont remplies de 0. De plus, l'indicateur est défini sur le MSB de [rj]. shl shl ri rj A L'instruction stockera la chaîne de W bits obtenue par [rj] décalage vers la droite pour [A] u bit dans le registre ri. Les positions vides après le décalage sont remplies de 0. De plus, l'indicateur est défini sur le LSB de [rj]. shr shr ri rj A Opération liée à la comparaison Chaque instruction de l'opération liée à la comparaison ne modifie aucun registre ; Les résultats de la comparaison seront stockés dans . flag instruction mettra l'indicateur à 1 si [ri] = [A], et sinon le mettra à 0 cmpe cmpe ri A instruction définira l'indicateur sur 1 si , et sinon le définira sur 0 cmpa cmpa ri A [ri]_u > [A]_u instruction mettra l'indicateur à 1 si , et sinon le mettra à 0 cmpae cmpae ri A [ri]_u ≥ [A]_u instruction définira l'indicateur sur 1 si , et sinon le définira sur 0 cmpg cmpg ri A [ri]_s > [A]_s instruction mettra le drapeau à 1 si , et sinon le mettra à 0 cmpge cmpge ri A [ri]_S ≥ [A]_S Opération liée au déménagement instruction stockera [A] dans le registre ri. mov mov ri A instruction stockera [A] dans le registre ri si flag = 1 et sinon la valeur du registre ri ne changera pas. cmov cmov ri A Lié au saut Ces instructions de saut et de saut conditionnel ne modifieront pas le registre et le , mais modifieront le . flag pc instruction de stockera [A] dans pc. saut jmp A instruction stocke [A] dans pc lorsque = 1, et sinon incrémente pc de 1 cjmp cjmp A flag L'instruction stockera [A] dans pc lorsque = 0, et sinon incrémentera pc de 1 cnjmp cnjmp A flag Opération liée à la mémoire Ce sont de simples opérations de chargement de mémoire et des opérations de stockage, où l'adresse de la mémoire est déterminée par le nombre immédiat ou le contenu du registre. Ce sont les seules méthodes d'adressage dans TinyRAM. (TinyRAM ne prend pas en charge le mode d'adressage commun "base + décalage"). L'instruction stockera le LSB de [ri] à l'adresse [A] U-ième octet en mémoire. store.b store A ri L'instruction stockera le contenu de l'adresse U-ième octet [A] en mémoire dans le registre ri (remplissant avec 0 dans les octets avant). load.b load ri A instruction stockera [ri] dans la position du mot alignée avec le [A]w-ième octet en mémoire. store.w store.w A ri instruction a stocké le mot dans sa mémoire aligné avec l'octet [A]w dans le registre ri. load.w load.w ri A Opération liée à l'entrée Cette instruction est la seule qui puisse accéder à l'une ou l'autre des bandes. La 0e bande a été utilisée pour l'entrée principale et la première bande pour l'entrée auxiliaire de l'utilisateur. l'instruction de stockera le mot de bit W suivant sur la bande [A] U dans le registre ri. Pour être plus précis, si la bande [A]u contient un mot de repos, le mot suivant sera consommé et stocké dans ri, et définira = 0 ; Sinon (s'il n'y a pas de mots d'entrée restants sur la bande [A]u), stockez 0^W dans ri et définissez = 1. lecture read ri A flag flag Étant donné que TinyRAM n'a que deux bandes d'entrée, toutes sauf que les deux premiers sont supposés vides. bandes Plus précisément, si [A]u n'est pas 0 ou 1, alors nous stockons 0^W dans le ri et définissons le =1. flag Opération liée à la sortie Cette instruction signifie que le programme a terminé son calcul et qu'aucune autre opération n'est autorisée. La de l'instruction entraînera le "blocage" de la machine d'état (sans augmentation de pc) ou "l'arrêt" (arrêt du calcul) et le retour à [A] u. Le choix entre décrochage ou arrêt n'est pas défini. La valeur de retour 0 est utilisée pour indiquer l'acceptation. réponse answer A Contrainte du jeu d'instructions TinyRAM a utilisé la contrainte R1CS pour effectuer des contraintes de circuit, et la forme spécifique est la suivante : (Ai ∗ S) ∗ (Bi ∗ S) − Ci ∗ S = 0 Maintenant, si nous voulons prouver que nous connaissons une solution du calcul original, nous devrons prouver que dans les matrices A, B et C, chaque vecteur ligne et vecteur solution de la valeur du produit scalaire est en accord avec les contraintes R1CS représente le vecteur ligne dans la matrice). S A_i, B_i , C_i Chaque contrainte R1CS peut être représentée par linear_combination a, b ou c. Les affectations de toutes les variables d'un système R1CS peuvent être divisées en deux parties : entrée primaire et entrée auxiliaire. Le Primaire est ce que nous appelons souvent une "déclaration" et l'auxiliaire est un "témoin". Chaque système de contraintes R1CS contient plusieurs contraintes R1CS. La longueur du vecteur pour chaque contrainte est fixe (taille d'entrée primaire + taille d'entrée auxiliaire + 1). TinyRAM a utilisé de nombreux gadgets personnalisés dans l'implémentation du code libsnark pour exprimer les contraintes vm ainsi que les contraintes d'exécution et de mémoire de l'opcode. Le code spécifique se trouve dans le dossier gadgetslib1/ Gadgets /cpu_checkers/tinyram. Contrainte liée aux bits formule de contrainte : et a * b = c La contrainte R1CS de et vérifie le paramètre 1 et le paramètre 2 et le calcul aboutit à une multiplication bit à bit. Les étapes de contrainte sont les suivantes : La contrainte de processus de calcul et le code sont les suivants : this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] }, { this->arg2val.bits[i] }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); La contrainte de codage du résultat Les résultats de calcul ne sont pas tous des contraintes nulles (conformément à la définition de l'instruction, et le processus consiste principalement à préparer le drapeau de contrainte) /* the gadgets below are Fp specific: I * X = R (1-R) * X = 0 if X = 0 then R = 0 if X != 0 then R = 1 and I = X^{-1} */ Contrainte de drapeau /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); formule de contrainte : ou (1 - a) * (1 - b) = (1 - c) Les étapes de contrainte spécifiques sont les suivantes : La contrainte de processus de calcul et le code sont les suivants : this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE, this->arg1val.bits[i] * (-1) }, { ONE, this->arg2val.bits[i] * (-1) }, { ONE, this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); La contrainte de codage du résultat Les résultats de calcul ne sont pas tous des contraintes nulles (conformément à la définition de l'instruction, et ce processus est principalement en préparation pour le drapeau de contrainte) Contrainte de drapeau /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); formule de contrainte : xor c = a ^ b c = a + b - 2*a*b, (2*b)*a = a+b - c Les étapes de contrainte spécifiques sont les suivantes : La contrainte de processus de calcul et le code sont les suivants : this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] * 2}, { this->arg2val.bits[i] }, { this->arg1val.bits[i], this->arg2val.bits[i], this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); La contrainte de codage du résultat Les résultats de calcul ne sont pas tous des contraintes nulles (conformément à la définition de l'instruction, et ce processus est principalement en préparation pour le drapeau de contrainte) Contrainte de drapeau /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); formule contrainte : non 1 * （1 - b） = c Les étapes de contrainte spécifiques sont les suivantes : this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->arg2val.bits[i] * (-1) }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); La contrainte de codage du résultat Les résultats de calcul ne sont pas tous des contraintes nulles (conformément à la définition de l'instruction, et ce processus est principalement en préparation pour le drapeau de contrainte) Contrainte de drapeau /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); Contrainte d'opération liée aux nombres entiers formule de contrainte : ajouter : 1 * （a + b） = c Les étapes de contrainte spécifiques sont les suivantes : La contrainte de processus de calcul, le code est le suivant : this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); La contrainte de résultat de décodage et la contrainte booléenne La contrainte de résultat de codage formule de contrainte : sous : La sous-contrainte est légèrement plus complexe que celle de add, avec une variable intermédiaire représentant le résultat ab, et 2^ w ajouté pour s'assurer que le résultat est calculé comme un entier positif et un signe. Les étapes de contrainte spécifiques sont les suivantes : intermediate_result = 2^w + a -b La contrainte de processus de calcul : /* intermediate_result = 2^w + (arg1val - arg2val) */ FieldT twoi = FieldT::one(); linear_combination a, b, c; a.add_term(0, 1); for (size_t i = 0; i pb.ap.w; ++i) { twoi = twoi + twoi; } b.add_term(0, twoi); b.add_term(this->arg1val.packed, 1); b.add_term(this->arg2val.packed, -1); c.add_term(intermediate_result, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a, b, c), FMT(this->annotation_prefix, " main_constraint")); La contrainte de résultat de décodage et la contrainte booléenne Contrainte de bit de signe formule de contrainte : mull, umulh et smulh c = a * b Les contraintes liées à Mull impliquent toutes les étapes suivantes : Contraintes du calcul de la multiplication Contraintes du codage des résultats de calcul Contraintes de drapeau du résultat de calcul formule de contrainte : udiv et umod B * q + r = A r a1, b1, c1; a1.add_term(B_inv, 1); b1.add_term(this->arg2val.packed, 1); c1.add_term(B_nonzero, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination a2, b2, c2; a2.add_term(ONE, 1); a2.add_term(B_nonzero, -1); b2.add_term(this->arg2val.packed, 1); c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination a3, b3, c3; a3.add_term(this->arg2val.packed, 1); b3.add_term(udiv_result, 1); c3.add_term(A_aux, 1); c3.add_term(umod_result, -; this->pb.add_r1cs_constraint(r1cs_constraint (a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination a4, b4, c4; a4.add_term(this->arg1val.packed, 1); b4.add_term(B_nonzero, 1); c4.add_term(A_aux, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination a5, b5, c5; a5.add_term(udiv_result, 1); b5.add_term(ONE, 1); b5.add_term(B_nonzero, -1); c5.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A (B, r, less=B_nonzero, leq=ONE) */ r_less_B->generate_r1cs_constraints(); Comparer l'opération Chaque instruction dans les opérations de comparaison ne modifiera aucun registre ; Les résultats de la comparaison sont stockés dans . Les instructions de comparaison incluent , , . et , qui peuvent être divisés en deux types : la comparaison de nombres signés et la comparaison de nombres non signés, qui utilisent tous deux le réalisé de libsnark dans leur noyau de processus de contrainte. flag cmpe cmpa cmpae cmpg cmpge comparison_gadget Formule de contrainte de comparaison de nombres non signés : cmpe_flag = cmpae_flag * (1-cmpa_flag) cmp et le code de contrainte sont les suivants : comparator.generate_r1cs_constraints(); this->pb.add_r1cs_constraint( r1cs_constraint ( {cmpae_result_flag}, {ONE, cmpa_result_flag * (-1)}, {cmpe_result_flag}), FMT(this->annotation_prefix, " cmpa_result_flag")); Formule de contrainte de comparaison de nombres signés : La contrainte de nombre non signé est plus complexe que la contrainte de comparaison de nombre signé car il y a plus de traitement de contrainte de bit de signe. La contrainte de bit de signe est la suivante : /* negate sign bits */ this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg1val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg1val_sign}), FMT(this->annotation_prefix, " negated_arg1val_sign")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg2val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg2val_sign}), FMT(this->annotation_prefix, " negated_arg2val_sign")); Les étapes restantes sont les mêmes que la contrainte de comparaison de nombres signés. Contrainte d'opération de déplacement formule de contrainte : mov La contrainte mov est relativement simple car il suffit de s'assurer que [A] est stocké dans le registre ri. L'opération mov ne modifiera pas , donc la contrainte doit s'assurer que la valeur de flag ne change pas. Le code de contrainte est le suivant : flag this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " mov_result_flag")); formule de contrainte : cmov flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval La condition de contrainte de cmov est plus complexe que celle de mov, car les comportements mov sont liés au changement de la valeur du drapeau, et cmov ne modifiera pas le drapeau, donc la contrainte doit s'assurer que la valeur du drapeau ne change pas, et Le code est comme suit: /* flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval */ this->pb.add_r1cs_constraint( r1cs_constraint ( {this->flag}, {this->arg2val.packed, this->desval.packed * (-1)}, {this->result, this->desval.packed * (-1)}), FMT(this->annotation_prefix, " cmov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " cmov_result_flag")); Contrainte d'opération de saut Ces instructions de saut et de saut conditionnel ne modifieront pas les registres et le mais modifieront . flag pc jmp La valeur pc est cohérente avec le résultat d'exécution de l'instruction dans la contrainte d'opération Jmp, et le code de contrainte spécifique est le suivant : this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) }, { this->result }), FMT(this->annotation_prefix, " jmp_result")); cjmp cjmp sautera en fonction de la condition du drapeau lorsque drapeau = 1, et sinon incrémentera pc de 1. La formule de contrainte est la suivante : flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1 Le code de contrainte est le suivant : this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) - this->pc.packed - 1, this->result - this->pc.packed - 1), FMT(this->annotation_prefix, " cjmp_result")); cnjmp Le cnjmp sautera selon les conditions du drapeau. Si flag = 0, le PC saute et sinon, incrémente pc de 1. La formule de contrainte est la suivante : flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2 Le code de contrainte est le suivant : this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, this->pc.packed + 1 - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end()))), FMT(this->annotation_prefix, " cnjmp_result")); Contrainte d'opération de mémoire Il s'agit de simples opérations de chargement et de stockage de la mémoire, où l'adresse de la mémoire est déterminée par le nombre immédiat ou le contenu d'un registre. Ce sont les seules méthodes d'adressage dans TinyRAM. (TinyRAM ne prend pas en charge le mode d'adressage commun "base + décalage"). et magasin.b magasin.w Pour store.w, prenez toutes les valeurs de arg1val , et pour les opcodes store.b, ne prenez que la partie nécessaire de arg1val (par exemple, le dernier octet), et le code de contrainte est le suivant : this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint (1 - (opcode_indicators[tinyram_opcode_STOREB] + opcode_indicators[tinyram_opcode_STOREW]), ls_prev_val_as_doubleword_variable->packed - ls_next_val_as_doubleword_variable->packed, 0), FMT(this->annotation_prefix, " non_store_instructions_dont_change_memory")); et charge.b charge.w Pour ces deux instructions, nous exigeons que le contenu chargé depuis la mémoire soit stocké dans instruction_results, et le code de contrainte est le suivant : this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADB], memory_subcontents - instruction_results[tinyram_opcode_LOADB], 0), FMT(this->annotation_prefix, " handle_loadb")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADW], memory_subcontents - instruction_results[tinyram_opcode_LOADW], 0), FMT(this->annotation_prefix, " handle_loadw")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum ( pb_variable_array (desval->bits.begin(), desval->bits.begin() + 8)), 0), FMT(this->annotation_prefix, " handle_storeb")); Contrainte d'opération d'entrée lis L'opération de lecture est liée à la bande et les contraintes spécifiques sont les suivantes : Lorsque la bande précédente est terminée et qu'il y a du contenu à lire, la bande suivante n'est pas autorisée à être lue. Lorsque la bande précédente est terminée et qu'il y a du contenu à lire, le est mis à 1 flag Si l'instruction de est exécutée maintenant, le contenu lu est cohérent avec le contenu d'entrée de la bande read Lire le contenu de l'extérieur de type1, l' est défini sur 1 flag Que le soit 0 signifie que le est 0 result flag Code de contrainte : this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - next_tape1_exhausted, 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_next_tape1_exhausted")); this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint (read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (instruction_flags[tinyram_opcode_READ], instruction_results[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " read_flag_implies_result_0")); Contraintes d'opération de sortie Cette instruction indique que le programme a terminé son calcul et qu'aucune autre opération n'est donc autorisée réponse Lorsque la valeur de sortie du programme est acceptée, has_accepted est défini sur 1 et la valeur de retour du programme est acceptée normalement, ce qui signifie que l'instruction actuelle est et que la valeur arg2 est 0. answer Le code de contrainte est le suivant : this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, arg2val->packed, 0), FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero")); Autre Bien sûr, en plus de certaines des contraintes liées aux instructions mentionnées ci-dessus, TinyRAM a également des contraintes sur la cohérence du PC, le codec des paramètres, la vérification de la mémoire, etc. Ces contraintes sont combinées via le système R1CS pour former un système de contraintes TinyRAM complet. Par conséquent, c'est la cause principale pour laquelle un grand nombre de contraintes TinyRAM sont générées sous la forme de R1CS. Nous nous référons ici à une figure de , montrant la consommation de temps nécessaire à un transfert ERC20 pour générer une preuve via TinyRAM. la revue tinyram ppt On peut conclure de l'exemple ci-dessus : il n'est pas possible de vérifier toutes les opérations EVM avec vnTinyRam + zk-SNARks et il ne convient que pour la vérification informatique d'un petit nombre d'instructions. Le vnTinyram peut être utilisé pour vérifier l'opcode pour les types de calcul partiels d'EVM.

Qu'est-ce qu'un jeu d'instructions TinyRAM ?

Trop long; Pour lire

Companies Mentioned

Coin Mentioned

@sin7y

HISTOIRES CONNEXES