TinyRAM बाइट-लेवल एड्रेसेबल रैंडम-एक्सेस मेमोरी और इनपुट टेप के साथ एक साधारण रिड्यूस्ड इंस्ट्रक्शन सेट कंप्यूटर (RISC) है।
टाइनीराम के दो प्रकार हैं: एक हार्वर्ड (एचवी) वास्तुकला का अनुसरण करता है, और दूसरा वॉन न्यूमैन (वीएन) वास्तुकला का अनुसरण करता है (इस लेख में, हम मुख्य रूप से वॉन न्यूमैन वास्तुकला पर ध्यान केंद्रित करते हैं)।
सक्सिडेंट कम्प्यूटेशनल इंटीग्रिटी एंड प्राइवेसी रिसर्च (SCIPR) प्रोजेक्ट TinyRAM प्रोग्राम्स के सही निष्पादन को साबित करने के लिए तंत्र का निर्माण करता है, और TinyRAM को इस सेटिंग में दक्षता के लिए डिज़ाइन किया गया है। यह दो विरोधी आवश्यकताओं के बीच संतुलन बनाता है - "पर्याप्त अभिव्यक्ति" और "छोटे निर्देश सेट":
उच्च स्तरीय प्रोग्रामिंग भाषाओं से संकलित होने पर लघु, कुशल असेंबली कोड का समर्थन करने के लिए पर्याप्त अभिव्यक्ति,
एससीआईपीआर के एल्गोरिदम और क्रिप्टोग्राफिक तंत्र का उपयोग करके अंकगणितीय सर्किट और कुशल सत्यापन के माध्यम से सरल सत्यापन का समर्थन करने के लिए छोटा निर्देश सेट।
इस लेख में, हम दोहराए जाने वाले TinyRAM परिचय के बजाय पिछले लेख को पूरक करेंगे, और फिर निर्देशों और सर्किट बाधाओं की शुरूआत पर ध्यान केंद्रित करेंगे।
TinyRAM के मूल परिचय के लिए, कृपया हमारा पिछला लेख देखें: Tinyram简介-中文TinyRAM Review-English
TinyRAM 29 निर्देशों का समर्थन करता है, प्रत्येक एक opcode द्वारा निर्दिष्ट और 3 ऑपरेंड तक। ऑपरेंड या तो एक रजिस्टर का नाम हो सकता है (अर्थात, 0 से K-1 तक के पूर्णांक) या तत्काल मान (यानी, W-बिट स्ट्रिंग्स)।
जब तक अन्यथा निर्दिष्ट न हो, प्रत्येक निर्देश ध्वज को अलग से संशोधित नहीं करता है और vnTinyRAM के लिए डिफ़ॉल्ट रूप से i (i% 2^W), i=2W/8 द्वारा पीसी को बढ़ाता है।
सामान्य तौर पर, पहला ऑपरेंड निर्देश गणना के लिए लक्ष्य रजिस्टर होता है और अन्य ऑपरेंड निर्देशों के लिए आवश्यक पैरामीटर निर्दिष्ट करते हैं। अंत में, सभी निर्देशों को निष्पादित करने के लिए मशीन का एक चक्र लगता है।
और : निर्देश and ri rj A
, [rj] और [A] के बिट्स और परिणामों को ri रजिस्टर में संग्रहीत करेगा। साथ ही, यदि परिणाम 0^{W} है, तो flag
को 1 पर सेट करें और अन्यथा इसे 0 पर सेट करें।
या निर्देश or ri rj A
[rj] और [A] के बिट्स और परिणामों को ri रजिस्टर में संग्रहीत करेगा। साथ ही, यदि परिणाम 0^{W} है, तो flag
को 1 पर सेट करें और अन्यथा इसे 0 पर सेट करें।
xor निर्देश xor ri rj A
, [rj] और [A] के बिट्स और परिणामों को ri रजिस्टर में संग्रहीत करेगा। साथ ही, यदि परिणाम 0^{W} है, तो flag
को 1 पर सेट करें और अन्यथा इसे 0 पर सेट करें।
निर्देश नहीं not ri A
, आरआई रजिस्टर में [आरजे] और [ए] के बिट्स और परिणामों को स्टोर करेगा। साथ ही, यदि परिणाम 0^{W} है, तो flag
को 1 पर सेट करें और अन्यथा इसे 0 पर सेट करें।
ये विभिन्न अहस्ताक्षरित और हस्ताक्षरित पूर्णांक-संबंधित संचालन हैं। प्रत्येक सेटिंग में, यदि कोई अंकगणितीय अतिप्रवाह या त्रुटि होती है (जैसे कि शून्य से विभाजित करना), flag
को 1 पर सेट करें, और अन्यथा इसे 0 पर सेट करें।
निम्नलिखित भाग में, U_{W} पूर्णांकों की एक श्रृंखला का प्रतिनिधित्व करता है {0*,…,* $2^{W} -1 $}; ये पूर्णांक W-बिट स्ट्रिंग्स से बने होते हैं। S_{W} पूर्णांकों की एक श्रृंखला का प्रतिनिधित्व करता है {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1। ये पूर्णांक भी W-बिट स्ट्रिंग्स से बने होते हैं।
जोड़ें: निर्देश add ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा। a_{W−1}⋯a_{0}, G = [rj]_u + [A]_u का W कम से कम महत्वपूर्ण बिट (LSB) है। इसके अलावा, flag
को G_{W} पर सेट किया जाएगा। G_{W} , G का सबसे महत्वपूर्ण बिट (MSB) है।
उप: निर्देश sub ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा। a_{W−1}⋯a_{0}, G = [rj]_u + 2^W - [A]_u का W कम से कम महत्वपूर्ण बिट (LSB) है। इसके अतिरिक्त, flag
को 1−G_{W} पर सेट किया जाएगा। G_{W} , G का सबसे महत्वपूर्ण बिट (MSB) है।
मूल निर्देश mull ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा। a_{W−1}⋯a_{0}, G=[rj]_u∗[A]_u का W कम से कम महत्वपूर्ण बिट (LSB) है। इसके अलावा, flag
को 1 if . पर सेट किया जाएगा
[rj]_u × [A] u U {W} , और अन्यथा इसे 0 पर सेट करें।
umulh निर्देश umulh ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा। a_{W−1}⋯a_{0}, G = [rj]_u [A]_u का W सबसे महत्वपूर्ण बिट (MSB) है। इसके अलावा, flag
को 1 पर सेट किया जाएगा यदि [rj]_u × [A] u U {W} , और अन्यथा इसे 0 पर सेट करें।
smulh निर्देश smulh ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा। a_{W−1} [rj] u ∗ [A]u का साइन बिट है, a {W−2}⋯a{0} [rj]_u ∗ [A]_u का W-1 MSB है। इसके अलावा, flag
को 1 पर सेट किया जाएगा यदि [rj]_u × [A] u ∉ S {W } , और अन्यथा इसे 0 पर सेट करें।
udiv निर्देश udiv ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा।
यदि [A] u = 0, a {W−1}⋯a_{0} = 0^W ।
यदि [A] u∣ 0, a {W−1}⋯a_{0} पूर्णांक Q का एकमात्र बाइनरी एन्कोडिंग है, जो इसे कुछ पूर्णांकों R ∈ {0,…,[A]_u − 1} के लिए बनाता है, सूत्र [rj]_u = [A]_u × Q + R व्यावहारिक है। इसके अतिरिक्त, केवल जब [A]_u=0 , flag
को 1 पर सेट किया जाएगा।
umod निर्देश umod ri rj A
, W-बिट स्ट्रिंग a_{W−1}⋯a_{0} को ri में संग्रहीत करेगा।
यदि [A] u = 0, a {W−1}⋯a_{0} = 0^W ।
यदि [A] u∣ 0, a {W−1}⋯a_{0} पूर्णांक R का एकमात्र बाइनरी एन्कोडिंग है, जिसका मान श्रेणी है
{0,…,[A]_u−1} , सूत्र [rj]_u = [A]_u × Q+R को कुछ Q मानों के लिए चलने योग्य बनाते हैं। इसके अलावा, केवल जब [A]_u = 0 , flag
को 1 पर सेट किया जाएगा।
एसएचएल निर्देश shl ri rj A
[आरजे] द्वारा प्राप्त डब्ल्यू-बिट स्ट्रिंग को आरआई रजिस्टर में [ए] यू बिट के लिए बाएं स्थानांतरण में संग्रहीत करेगा। स्थानांतरण के बाद रिक्त पदों को 0 से भर दिया जाता है। इसके अलावा, ध्वज को [rj] के MSB पर सेट किया जाता है।
shr निर्देश shr ri rj A
, [rj] द्वारा प्राप्त W-बिट स्ट्रिंग को [A] u बिट के लिए ri रजिस्टर में राइट शिफ्टिंग में स्टोर करेगा। स्थानांतरण के बाद रिक्त स्थान 0 से भरे जाते हैं। इसके अलावा, ध्वज को [rj] के LSB पर सेट किया जाता है।
तुलना-संबंधित ऑपरेशन में प्रत्येक निर्देश किसी भी रजिस्टर को संशोधित नहीं करता है; तुलना परिणाम flag
में संग्रहीत किए जाएंगे।
cmpe निर्देश cmpe ri A
ध्वज को 1 पर सेट करेगा यदि [ri] = [A], और अन्यथा इसे 0 पर सेट करें
cmpa निर्देश cmpa ri A
ध्वज को 1 पर सेट करेगा यदि [ri]_u > [A]_u , और अन्यथा इसे 0 पर सेट करें
cmpae निर्देश cmpae ri A
ध्वज को 1 पर सेट करेगा यदि [ri]_u ≥ [A]_u , और अन्यथा इसे 0 पर सेट करें
cmpg निर्देश cmpg ri A
ध्वज को 1 पर सेट करेगा यदि [ri]_s > [A]_s , और अन्यथा इसे 0 पर सेट करें
cmpge निर्देश cmpge ri A
ध्वज को 1 पर सेट करेगा यदि [ri]_S ≥ [A]_S , और अन्यथा इसे 0 पर सेट करें
mov निर्देश mov ri A
, [A] को ri रजिस्टर में संग्रहीत करेगा।
cmov निर्देश cmov ri A
फ्लैग = 1 होने पर [A] को ri रजिस्टर में स्टोर करेगा और अन्यथा ri रजिस्टर का मान नहीं बदलेगा।
ये कूद और सशर्त कूद निर्देश रजिस्टर और flag
को संशोधित नहीं करेंगे, लेकिन pc
को संशोधित करेंगे।
जंप निर्देश jmp A
[ए] को पीसी में स्टोर करेगा।
सीजेएमपी निर्देश cjmp A
flag
= 1 पर [ए] पीसी में स्टोर करेगा, और अन्यथा पीसी को 1 से बढ़ा देगा
cnjmp निर्देश cnjmp A
flag
= 0 होने पर [ए] को पीसी में स्टोर करेगा, और अन्यथा पीसी को 1 से बढ़ा देगा
ये सरल मेमोरी लोड ऑपरेशन और स्टोर ऑपरेशन हैं, जहां मेमोरी का पता तत्काल संख्या या रजिस्टर की सामग्री से निर्धारित होता है।
TinyRAM में ये एकमात्र एड्रेसिंग मेथड हैं। (TinyRAM सामान्य "आधार + ऑफसेट" एड्रेसिंग मोड का समर्थन नहीं करता है)।
store.b इंस्ट्रक्शन store A ri
[ri] के LSB को [A] U-th बाइट एड्रेस पर मेमोरी में स्टोर करेगा।
load.b निर्देश load ri A
, [A] U-वें बाइट पते की सामग्री को मेमोरी में ri रजिस्टर (फ्रंट बाइट्स में 0 से भरकर) में संग्रहीत करेगा।
store.w निर्देश store.w A ri
स्मृति में [ए] डब्ल्यू-वें बाइट के साथ गठबंधन शब्द स्थिति में [आरआई] स्टोर करेगा।
load.w निर्देश load.w ri A
ने अपनी मेमोरी में शब्द को [A]w बाइट के साथ संरेखित करके ri रजिस्टर में संग्रहीत किया है।
यह निर्देश केवल एक ही है जो किसी भी टेप तक पहुंच सकता है। 0वें टेप का उपयोग प्राथमिक इनपुट के लिए और पहला टेप उपयोगकर्ता सहायक इनपुट के लिए किया गया था।
read ri A
अगले डब्ल्यू-बिट शब्द को [ए] यू टेप पर आरआई रजिस्टर में स्टोर करेगा। अधिक सटीक होने के लिए, यदि [ए] यू टेप में कोई आराम शब्द है, तो अगला शब्द उपभोग किया जाएगा और री में संग्रहीत किया जाएगा, और flag
= 0 सेट करें; अन्यथा (यदि [ए] यू टेप पर कोई आराम इनपुट शब्द नहीं हैं), 0 ^ डब्ल्यू को री में स्टोर करें और flag
= 1 सेट करें।
चूँकि TinyRAM में केवल दो इनपुट टेप हैं, सभी
विशेष रूप से, यदि [ए] यू 0 या 1 नहीं है, तो हम 0 ^ डब्ल्यू को री में स्टोर करते हैं और flag
= 1 सेट करते हैं।
इस निर्देश का अर्थ है कि कार्यक्रम ने अपनी गणना पूरी कर ली है और किसी अन्य संचालन की अनुमति नहीं है।
answer A
राज्य मशीन को "स्टाल" (बिना पीसी वृद्धि के) या "हॉल्ट" (कंप्यूटिंग रोकें) होने का कारण होगा, और [ए] यू पर वापस आ जाएगा। स्टॉल या हॉल्ट के बीच चुनाव को परिभाषित नहीं किया गया है। वापसी मान 0 का उपयोग स्वीकृति को इंगित करने के लिए किया जाता है।TinyRAM ने सर्किट बाधाओं को पूरा करने के लिए R1CS बाधा का उपयोग किया है, और विशिष्ट रूप इस प्रकार है:
(ऐ एस) ∗ (द्वि ∗ एस) - सीआई ∗ एस = 0
अब, अगर हम यह साबित करना चाहते हैं कि हम मूल गणना का समाधान जानते हैं, तो हमें यह साबित करना होगा कि मैट्रिक्स ए, बी और सी में, प्रत्येक पंक्ति वेक्टर और आंतरिक उत्पाद मूल्य के समाधान वेक्टर एस आर 1 सीएस बाधाओं के अनुरूप हैं A_i, B_i , C_i मैट्रिक्स में पंक्ति वेक्टर का प्रतिनिधित्व करता है)।
प्रत्येक R1CS बाधा को रैखिक_संयोजन a, b, या c द्वारा दर्शाया जा सकता है। R1CS प्रणाली में सभी चरों के असाइनमेंट को दो भागों में विभाजित किया जा सकता है: प्राथमिक इनपुट और सहायक इनपुट। प्राथमिक वह है जिसे हम अक्सर "कथन" कहते हैं और सहायक "गवाह" होता है।
प्रत्येक R1CS बाधा प्रणाली में कई R1CS बाधाएँ होती हैं। प्रत्येक बाधा के लिए वेक्टर लंबाई निश्चित है (प्राथमिक इनपुट आकार + सहायक इनपुट आकार + 1)।
TinyRAM ने vm बाधाओं के साथ-साथ opcode निष्पादन और स्मृति बाधाओं को व्यक्त करने के लिए libsnark कोड कार्यान्वयन में बहुत से कस्टम गैजेट्स का उपयोग किया है। विशिष्ट कोड गैजेट्सलिब1/गैजेट्स/cpu_checkers/tinyram फ़ोल्डर में है।
और बाधा सूत्र:
a * b = c
पैरामीटर 1 और पैरामीटर 2 की R1CS बाधा और सत्यापित करती है और गणना के परिणाम बिट-बाय-बिट गुणा में होते हैं। बाधा कदम इस प्रकार हैं:
गणना प्रक्रिया बाधा, और कोड इस प्रकार है:
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));
परिणाम कोडिंग बाधा
गणना परिणाम सभी शून्य बाधाएं नहीं हैं (निर्देश परिभाषा के अनुरूप, और प्रक्रिया मुख्य रूप से बाधा ध्वज तैयार करने के लिए है)
/* 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} */
ध्वज बाधा
/* 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"));
या बाधा सूत्र:
(1 - a) * (1 - b) = (1 - c)
विशिष्ट बाधा चरण इस प्रकार हैं:
गणना प्रक्रिया बाधा, और कोड इस प्रकार है:
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));
परिणाम कोडिंग बाधा
गणना परिणाम सभी शून्य बाधाएं नहीं हैं (निर्देश परिभाषा के अनुरूप, और यह प्रक्रिया मुख्य रूप से बाधा ध्वज की तैयारी में है)
ध्वज बाधा
/* 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"));
xor बाधा सूत्र:
c = a ^ b <=> c = a + b - 2*a*b, (2*b)*a = a+b - c
विशिष्ट बाधा चरण इस प्रकार हैं:
गणना प्रक्रिया बाधा, और कोड इस प्रकार है:
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));
परिणाम कोडिंग बाधा
गणना परिणाम सभी शून्य बाधाएं नहीं हैं (निर्देश परिभाषा के अनुरूप, और यह प्रक्रिया मुख्य रूप से बाधा ध्वज की तैयारी में है)
ध्वज बाधा
/* 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"));
बाधा नहीं सूत्र:
1 * (1 - b) = c
विशिष्ट बाधा चरण इस प्रकार हैं:
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));
परिणाम कोडिंग बाधा
गणना परिणाम सभी शून्य बाधाएं नहीं हैं (निर्देश परिभाषा के अनुरूप, और यह प्रक्रिया मुख्य रूप से बाधा ध्वज की तैयारी में है)
ध्वज बाधा
/* 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"));
जोड़ें: बाधा सूत्र:
1 * (a + b) = c
विशिष्ट बाधा चरण इस प्रकार हैं:
गणना प्रक्रिया बाधा, कोड इस प्रकार है:
this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result"));
डिकोडिंग परिणाम बाधा और बूलियन बाधा
कोडिंग परिणाम बाधा
उप: बाधा सूत्र:
उप-बाधा जोड़ने की तुलना में थोड़ी अधिक जटिल है, जिसमें एक मध्यवर्ती चर ab परिणाम का प्रतिनिधित्व करता है, और यह सुनिश्चित करने के लिए 2 ^ w जोड़ा जाता है कि परिणाम की गणना एक सकारात्मक पूर्णांक और एक संकेत के रूप में की जाती है। विशिष्ट बाधा चरण इस प्रकार हैं:
intermediate_result = 2^w + a -b
गणना प्रक्रिया बाधा:
/* 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"));
डिकोडिंग परिणाम बाधा और बूलियन बाधा
साइन बिट बाधा
मल, umulh और smulh बाधा सूत्र:
c = a * b
मुल-संबंधित बाधाओं में सभी निम्नलिखित चरण शामिल हैं:
udiv और umod बाधा सूत्र:
B * q + r = A r <= B
'B' भाजक है, 'q' भागफल है, और 'r' शेषफल है। शेष भाजक से अधिक नहीं होना चाहिए। विशिष्ट बाधा कोड इस प्रकार हैं:
/* 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();
तुलना संचालन में प्रत्येक निर्देश किसी भी रजिस्टर को संशोधित नहीं करेगा; तुलना परिणाम flag
में संग्रहीत हैं। तुलना निर्देशों में शामिल हैं cmpe , cmpa , cmpae । cmpg और cmpge , जिन्हें दो प्रकारों में विभाजित किया जा सकता है: हस्ताक्षरित संख्या तुलना और अहस्ताक्षरित संख्या तुलना, जो दोनों अपने बाधा प्रक्रिया कोर में comparison_gadget
के वास्तविक तुलना_गैजेट का उपयोग करते हैं।
अहस्ताक्षरित संख्या तुलना बाधा सूत्र:
cmpe_flag = cmpae_flag * (1-cmpa_flag)
सीएमपी और बाधा कोड इस प्रकार है:
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"));
हस्ताक्षरित संख्या तुलना बाधा सूत्र:
अहस्ताक्षरित संख्या बाधा हस्ताक्षरित संख्या तुलना बाधा से अधिक जटिल है क्योंकि अधिक साइन बिट बाधा प्रसंस्करण है।
साइन बिट बाधा इस प्रकार है:
/* 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"));
शेष चरण हस्ताक्षरित संख्या तुलना बाधा के समान हैं।
मूव बाधा सूत्र:
मूव बाधा अपेक्षाकृत सरल है क्योंकि इसे केवल यह सुनिश्चित करने की आवश्यकता है कि [ए] री रजिस्टर में संग्रहीत है। Mov ऑपरेशन flag
को संशोधित नहीं करेगा, इसलिए बाधा को यह सुनिश्चित करने की आवश्यकता है कि ध्वज मान नहीं बदलता है। बाधा कोड इस प्रकार है:
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"));
cmov बाधा सूत्र:
flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval
cmov की बाधा स्थिति mov की तुलना में अधिक जटिल है, क्योंकि mov व्यवहार ध्वज मान के परिवर्तन से संबंधित हैं, और cmov ध्वज को संशोधित नहीं करेगा, इसलिए बाधा को यह सुनिश्चित करने की आवश्यकता है कि ध्वज का मान नहीं बदलता है, और
/* 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"));
ये कूद और सशर्त कूद निर्देश रजिस्टरों और flag
को संशोधित नहीं करेंगे बल्कि pc
को संशोधित करेंगे।
जेएमपी
पीसी मान जेएमपी ऑपरेशन बाधा में निर्देश के निष्पादन परिणाम के अनुरूप है, और विशिष्ट बाधा कोड इस प्रकार है:
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 ध्वज की स्थिति के अनुसार कूद जाएगा जब ध्वज = 1, और अन्यथा पीसी को 1 से बढ़ाता है।
बाधा सूत्र इस प्रकार है:
flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1
बाधा कोड इस प्रकार है:
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"));
सीएनजेएमपी
सीएनजेएमपी ध्वज की स्थिति के अनुसार कूद जाएगा। यदि ध्वज = 0, पीसी कूदता है और अन्यथा, पीसी को 1 से बढ़ाता है।
बाधा सूत्र इस प्रकार है:
flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2
बाधा कोड इस प्रकार है:
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"));
ये साधारण मेमोरी लोड और स्टोर ऑपरेशन हैं, जहां मेमोरी का पता तत्काल संख्या या रजिस्टर की सामग्री से निर्धारित होता है।
TinyRAM में ये एकमात्र एड्रेसिंग मेथड हैं। (TinyRAM सामान्य "आधार + ऑफसेट" एड्रेसिंग मोड का समर्थन नहीं करता है)।
store.b और store.w
store.w के लिए, arg1val के सभी मान लें, और store.b opcodes के लिए, केवल arg1val (जैसे, अंतिम बाइट) का आवश्यक हिस्सा लें, और बाधा कोड इस प्रकार है:
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"));
load.b और load.w
इन दो निर्देशों के लिए, हम चाहते हैं कि मेमोरी से लोड की गई सामग्री को निर्देश_परिणाम में संग्रहीत किया जाए, और बाधा कोड इस प्रकार है:
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"));
पढ़ना
रीड ऑपरेशन टेप से संबंधित है, और विशिष्ट बाधाएं इस प्रकार हैं:
जब पिछला टेप समाप्त हो जाता है और पढ़ने के लिए सामग्री होती है, तो अगले टेप को पढ़ने की अनुमति नहीं होती है।
जब पिछला टेप समाप्त हो जाता है और पढ़ने के लिए सामग्री होती है, तो flag
1 . पर सेट हो जाता है
यदि read
निर्देश अभी अपेक्षित है, तो सामग्री पठन कैच टेप की इनपुट सामग्री के अनुरूप है
टाइप 1 के बाहर से सामग्री पढ़ें, flag
1 पर सेट है
क्या result
0 है इसका मतलब है कि flag
0 है
बाधा कोड:
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"));
यह निर्देश इंगित करता है कि कार्यक्रम ने अपनी गणना पूरी कर ली है और इसलिए आगे के संचालन की अनुमति नहीं है
जब प्रोग्राम का आउटपुट मान स्वीकार किया जाता है, has_accepted को 1 पर सेट किया जाता है, और प्रोग्राम का रिटर्न मान सामान्य रूप से स्वीकार किया जाता है, जिसका अर्थ है कि वर्तमान निर्देश answer
है और arg2 मान 0 है।
बाधा कोड इस प्रकार है:
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"));
बेशक, ऊपर उल्लिखित कुछ निर्देश-संबंधी बाधाओं के अलावा, TinyRAM में पीसी स्थिरता, पैरामीटर कोडेक, मेमोरी चेकिंग आदि पर भी कुछ बाधाएं हैं। इन बाधाओं को R1CS सिस्टम के माध्यम से एक पूर्ण TinyRAM बाधा प्रणाली बनाने के लिए जोड़ा जाता है। इसलिए, यही मूल कारण है कि R1CS के रूप में बड़ी संख्या में TinyRAM बाधाएं उत्पन्न होती हैं।
यहां हम टिनीराम समीक्षा पीपीटी के एक आंकड़े का उल्लेख करते हैं, जो कि TinyRAM के माध्यम से एक प्रमाण उत्पन्न करने के लिए ERC20 हस्तांतरण के लिए आवश्यक समय की खपत को दर्शाता है।
यह ऊपर के उदाहरण से निष्कर्ष निकाला जा सकता है: vnTinyRam + zk-SNARks के साथ सभी ईवीएम संचालन को सत्यापित करना संभव नहीं है और यह केवल कम संख्या में निर्देशों के कम्प्यूटेशनल सत्यापन के लिए उपयुक्त है। vnTinyram का उपयोग ईवीएम के आंशिक गणना प्रकारों के लिए ओपकोड को सत्यापित करने के लिए किया जा सकता है।