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

• et : l'instruction and ri rj A stockera les bits et résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est 0^{W} , définissez flag sur 1, sinon définissez-le sur 0.

  
  

• ou l'instruction or ri rj A stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est 0^{W} , définissez flag sur 1, sinon définissez-le sur 0.

  
  

• xor instruction xor ri rj A stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est 0^{W} , définissez flag sur 1, sinon définissez-le sur 0.

  
  

• not instruction not ri A stockera les bits et les résultats de [rj] et [A] dans le registre ri. De plus, si le résultat est 0^{W} , définissez flag sur 1, sinon définissez-le sur 0.

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 flag sur 1 , sinon définissez-le sur 0.

Dans la partie suivante, U_{W} représente une suite d'entiers {0*,…,* $2^{W} -1 $} ; Ces entiers sont constitués de chaînes de W bits. S_{W} 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.

• add : l'instruction add ri rj A 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 G = [rj]_u + [A]_u . De plus, flag sera défini sur G_{W} . G_{W} est le bit le plus significatif (MSB) de G.

  
  

• sub : l' instruction sub ri rj A 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 G = [rj]_u + 2^W − [A]_u . De plus, flag sera défini sur 1−G_{W} . G_{W} est le bit le plus significatif (MSB) de G.

  
  

• L'instruction mull mull ri rj A 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 G=[rj]_u∗[A]_u . De plus, flag sera mis à 1 si

  [rj]_u × [A] u ∉ U {W} , sinon mettez-le à 0.

  
  

• L'instruction umulh umulh ri rj A 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 G = [rj]_u ∗ [A]_u . De plus, flag sera mis à 1 si [rj]_u × [A] u ∉ U {W} , sinon mis à 0.

  
  

• L'instruction smulh smulh ri rj A stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri. a_{W−1} est le bit de signe de [rj] u ∗ [A]u, a {W−2}⋯a{0} est le W - 1 MSB de [rj]_u ∗ [A]_u . De plus, flag sera mis à 1 si [rj]_u × [A] u ∉ S {W } , sinon mis à 0.

  
  

udiv instuction udiv ri rj A stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri.

Si [A] u = 0, a {W−1}⋯a_{0} = 0^W .

Si [A] u∣ ≠ 0, a {W−1}⋯a_{0} est le seul codage binaire de l'entier Q, ce qui fait que pour certains entiers R ∈ {0,…,[A]_u − 1} , la formule [rj]_u = [A]_u × Q + R est réalisable. De plus, uniquement lorsque [A]_u=0 , l' flag sera défini sur 1.

L'instruction umod umod ri rj A stockera la chaîne de W bits a_{W−1}⋯a_{0} dans le ri.

Si [A] u = 0, a {W−1}⋯a_{0} = 0^W .

Si [A] u∣ ≠ 0, a {W−1}⋯a_{0} est le seul codage binaire de l'entier R, dont la plage de valeurs est

{0,…,[A]_u−1} , rendant la formule [rj]_u = [A]_u × Q+R réalisable pour certaines valeurs de Q. De plus, uniquement lorsque [A]_u = 0 , l' flag sera défini sur 1.

Opération liée au quart de travail

• L'instruction shl shl ri rj A 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].

  
  

• L'instruction shr shr ri rj A 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].

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 cmpe cmpe ri A mettra l'indicateur à 1 si [ri] = [A], et sinon le mettra à 0

  
  

• instruction cmpa cmpa ri A définira l'indicateur sur 1 si [ri]_u > [A]_u , et sinon le définira sur 0

  
  

• instruction cmpae cmpae ri A mettra l'indicateur à 1 si [ri]_u ≥ [A]_u , et sinon le mettra à 0

  
  

• cmpg instruction cmpg ri A définira l'indicateur sur 1 si [ri]_s > [A]_s , et sinon le définira sur 0

  
  

• cmpge instruction cmpge ri A mettra le drapeau à 1 si [ri]_S ≥ [A]_S , et sinon le mettra à 0

Opération liée au déménagement

• mov instruction mov ri A stockera [A] dans le registre ri.

  
  

• cmov instruction cmov ri A stockera [A] dans le registre ri si flag = 1 et sinon la valeur du registre ri ne changera pas.

Lié au saut

Ces instructions de saut et de saut conditionnel ne modifieront pas le registre et le flag , mais modifieront le pc .

• instruction de saut jmp A stockera [A] dans pc.

  
  

• cjmp instruction cjmp A stocke [A] dans pc lorsque flag = 1, et sinon incrémente pc de 1

  
  

• L'instruction cnjmp cnjmp A stockera [A] dans pc lorsque flag = 0, et sinon incrémentera pc de 1

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 store.b store A ri stockera le LSB de [ri] à l'adresse [A] U-ième octet en mémoire.

  
  

• L'instruction load.b load ri A 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).

  
  

• instruction store.w store.w A ri stockera [ri] dans la position du mot alignée avec le [A]w-ième octet en mémoire.

  
  

• instruction load.w load.w ri A a stocké le mot dans sa mémoire aligné avec l'octet [A]w dans le registre ri.

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 lecture read ri A 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 flag = 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 flag = 1.

Étant donné que TinyRAM n'a que deux bandes d'entrée, toutes bandes sauf que les deux premiers sont supposés vides.

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 flag =1.

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 réponse de l'instruction answer A 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.

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 S de la valeur du produit scalaire est en accord avec les contraintes R1CS A_i, B_i , C_i représente le vecteur ligne dans la matrice).

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

• et formule de contrainte :

  
  

   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 :

  
  

  1. La contrainte de processus de calcul et le code sont les suivants :

     
     

      this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { this->arg1val.bits[i] }, { this->arg2val.bits[i] }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i));

  
  

  2. La contrainte de codage du résultat

     
     

  3. 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} */

  
  

  4. Contrainte de drapeau

     
     

   /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag"));

  
  

• ou formule de contrainte :

  
  

   (1 - a) * (1 - b) = (1 - c)

  
  

  Les étapes de contrainte spécifiques sont les suivantes :

  
  

  1. La contrainte de processus de calcul et le code sont les suivants :

     
     

   this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { 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));

  
  

  2. La contrainte de codage du résultat

     
     

  3. 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)

     
     

  4. Contrainte de drapeau

     
     

   /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { 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 :

  
  

  1. La contrainte de processus de calcul et le code sont les suivants :

     
     

   this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { 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));

  
  

  2. La contrainte de codage du résultat

     
     

  3. 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)

     
     

  4. Contrainte de drapeau

     
     

   /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag"));

  
  

• formule non contrainte :

  
  

   1 * （1 - b） = c

  
  

  Les étapes de contrainte spécifiques sont les suivantes :

  
  

  1. 
     

      this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { ONE, this->arg2val.bits[i] * (-1) }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i));

     
     

  2. La contrainte de codage du résultat

     
     

  3. 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)

     
     

  4. Contrainte de drapeau

     
     

   /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { 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

• ajouter : formule de contrainte :

  
  

   1 * （a + b） = c

  
  

  Les étapes de contrainte spécifiques sont les suivantes :

  
  

  1. La contrainte de processus de calcul, le code est le suivant :

     
     

   this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result"));

  
  

  2. La contrainte de résultat de décodage et la contrainte booléenne

     
     

  3. La contrainte de résultat de codage

     
     

• sous : formule de contrainte :

  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

  
  

  1. La contrainte de processus de calcul :

      /* intermediate_result = 2^w + (arg1val - arg2val) */ FieldT twoi = FieldT::one(); linear_combination<FieldT> a, b, c; a.add_term(0, 1); for (size_t i = 0; i < this->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<FieldT>(a, b, c), FMT(this->annotation_prefix, " main_constraint"));

  
  

  2. La contrainte de résultat de décodage et la contrainte booléenne

     
     

  3. 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 :

  
  

  1. Contraintes du calcul de la multiplication

     
     

  2. Contraintes du codage des résultats de calcul

     
     

  3. Contraintes de drapeau du résultat de calcul

  
  

• formule de contrainte udiv et umod :

  
  

 B * q + r = A r <= B

'B' est le diviseur, 'q' est le quotient et 'r' est le reste. Le reste ne doit pas dépasser le diviseur. Les codes de contraintes spécifiques sont les suivants :

 /* B_inv * B = B_nonzero */ linear_combination<FieldT> 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<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination<FieldT> 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<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination<FieldT> 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<FieldT>(a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination<FieldT> 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<FieldT>(a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination<FieldT> 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<FieldT>(a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A<B_gadget<FieldT>(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 flag . Les instructions de comparaison incluent cmpe , cmpa , cmpae . cmpg et cmpge , 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 comparison_gadget réalisé de libsnark dans leur noyau de processus de contrainte.

• 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<FieldT>( {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<FieldT>( {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<FieldT>( {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 flag , donc la contrainte doit s'assurer que la valeur de flag ne change pas. Le code de contrainte est le suivant :

  
  

   this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {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<FieldT>( {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<FieldT>( {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 flag mais modifieront 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<FieldT>( { ONE }, { pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, this->pc.packed + 1 - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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").

• magasin.b et 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<FieldT>(opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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"));

  
  

• charge.b et 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<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum<FieldT>( pb_variable_array<FieldT>(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 :

1. 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.

   
   

2. Lorsque la bande précédente est terminée et qu'il y a du contenu à lire, le flag est mis à 1

   
   

3. Si l'instruction de read est exécutée maintenant, le contenu lu est cohérent avec le contenu d'entrée de la bande

   
   

4. Lire le contenu de l'extérieur de type1, l' flag est défini sur 1

   
   

5. Que le result soit 0 signifie que le flag est 0

Code de contrainte :

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 answer et que la valeur arg2 est 0.

Le code de contrainte est le suivant :

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 la revue tinyram ppt , montrant la consommation de temps nécessaire à un transfert ERC20 pour générer une preuve via TinyRAM.

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.