निष्पादन प्रक्रिया का STARK-आधारित प्रमाण Miden V1 पर कैसे कार्य करता है?

मिडन एक प्रमुख प्रौद्योगिकी-आधारित ZKVM कार्यान्वयन समाधान है।

इसकी मूल परत में, ZKP लाइब्रेरी के आधार पर स्टार्क प्रूफ जेनरेट किया जाता है और प्रूफ को वेरिफाई किया जाएगा। निम्नलिखित चित्र 1 में बिंदीदार भाग मिडन द्वारा कार्यान्वित मुख्य कार्य है। इसमें मुख्य रूप से तीन घटक होते हैं।

1. लेक्सिकल सिंटैक्स कंपाइलर्स का एक सेट, जो कि चित्र 1 में लेक्सिकल एनालाइज़र और सिंटैक्स पार्सर है। वे मिडन द्वारा परिभाषित असेंबली निर्देशों को कोडब्लॉक या ब्लॉक में निहित ओपकोड और ऑप वैल्यू में प्रोग्राम कर सकते हैं।

2. निर्देश निष्पादकों का एक सेट, जो चित्र 1 में निष्पादक है। यह परिभाषित नियमों के अनुसार ब्लॉक में निहित कोडब्लॉक और ऑपकोड और ऑप वैल्यू को निष्पादित करेगा। और निष्पादित परिणाम प्रमाण उत्पन्न करने के लिए उपयोग किए जाने वाले निष्पादन ट्रेस होंगे।

3. एआईआर (सार इंटर-मीडिएट रिप्रेजेंटेशन) का एक सेट, स्टार्क प्रूफ की आवश्यकताओं को पूरा करता है, जो कि चित्र 1 में एआईआर है। यह मिडन वर्चुअल मशीन की निष्पादन प्रक्रिया में बाधाओं का संचालन करता है।

चित्रा 1. मिडन परियोजना घटक

आकाशवाणी संरचनात्मक डिजाइन ड्राइंग

AIR की बाधाएं स्टैक और डिकोडर में विभाजित होती हैं: चित्र 2 स्टैक की बाधाओं को दिखाता है, जो प्रारंभ में 8 की शीर्ष गहराई के साथ स्टैक के साथ वितरित किया जाता है।

मैक्स_डेप्थ को आवश्यकतानुसार बढ़ाया जाता है यदि प्रारंभिक वितरण कार्यक्रम की जरूरतों के आधार पर निष्पादन के दौरान पार किया जा सकता है, लेकिन यह 16 की अधिकतम गहराई से अधिक नहीं होना चाहिए, अन्यथा, एक त्रुटि की सूचना दी जाती है।

चित्र 2: स्टैक बाधा का स्तंभ

जैसा कि नीचे देखा जा सकता है, चित्र 3 डिकोडर की बाधाओं को दर्शाता है। इन बाधाओं के बीच, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS, और hd_OP_bits निश्चित स्तंभ लंबाई हैं।

op_sponge का उपयोग निर्देशों के क्रम और शुद्धता को बाधित करने के लिए किया जाता है। cf_op_bits 3-बिट प्रवाह_ऑप्स को बाधित करता है। Ld_op_bits और hd_op_bits क्रमशः user_ops के निम्न 5 बिट्स और उच्च 2 बिट्स को बाधित करते हैं।

Ld_op_bits और hd_op_bits एक साथ मिलकर एक एक्ज़ीक्यूटेबल user_op बनाते हैं, जिसका उपयोग स्टैक की स्थिति की कमी के प्रत्येक चरण के लिए चयनकर्ता के रूप में भी किया जाता है!

चित्र 3: डिकोडर बाधा का स्तंभ

मिडन वीएम का निष्पादन प्रक्रिया उदाहरण

यह खंड वर्चुअल मशीन के निष्पादन और स्टार्क के निष्पादन ट्रेस की पीढ़ी को स्पष्ट करने के लिए सरल मिडेन तर्क दिखाता है।

निम्नलिखित कोड खंड 1 निष्पादित करने के लिए खंड है: इसका निष्पादन तर्क स्टैक पर 3 और 5 को धक्का देना है। फिर टेप से झंडा पढ़ें।

जांचें कि क्या ध्वज 1 या 0 है। यदि यह 1 है, तो "if.true तर्क" दो संख्याओं 3 और 5 को लेने के लिए चलाएँ, जो स्टैक पर धकेले गए हैं, उन्हें एक साथ जोड़ें, जिसके परिणामस्वरूप 8, और 8 को धक्का दें। ढेर। यदि यह 0 है, तो संख्या 3 और 5 लेने के लिए "अन्य तर्क" चलाएँ और उन्हें एक साथ गुणा करके 15 प्राप्त करें, और फिर स्टैक पर 15 पुश करें।

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

कोड खंड 1

मिडन के लेक्सिकल एनालाइज़र और सिंटैक्स पार्सर द्वारा पार्स किया गया अंतिम निर्देश कोड निम्नलिखित कोड सेगमेंट 2 में दिखाया गया है:

 begin noop noop noop noop noop noop noop push(3) noop noop noop noop noop noop noop push(5) read noop noop noop noop noop noop noop noop noop noop noop noop noop, if assert add noop noop noop noop noop noop noop noop noop noop noop noop noop else not assert mul noop noop noop noop noop noop noop noop noop noop noop noop end]

कोड खंड 2

चित्र 4 वर्चुअल मशीन के कोड खंड 2 को निष्पादित करने की प्रक्रिया को दर्शाता है।

मध्य भाग ऑपकोड निष्पादित करने वाले निष्पादक का फ़्लोचार्ट है। बाईं बिंदीदार रेखाएं कोड निष्पादन में उत्पन्न डिकोडर ट्रेस को संदर्भित करती हैं। सही डॉट-डैश लाइनें कोड निष्पादन में उत्पन्न स्टैक ट्रेस को संदर्भित करती हैं।

चित्र में, निष्पादक कोड ब्लॉक के अनुसार ब्लॉक द्वारा ब्लॉक निष्पादन करता है। इस उदाहरण में, पहले एक स्पैन ब्लॉक निष्पादित किया जाता है।

फिर चरण 32 पर if-else-end संरचना को स्विच ब्लॉक में प्रवेश करने के लिए किया जाता है और पिछले स्पैन ब्लॉक के अंतिम निष्पादन द्वारा ctx_stack में उत्पन्न स्पंज हैश को दबाया जाता है। स्विच ब्लॉक निष्पादित होने के बाद, इसे चरण 49 पर स्पंज में डालें।

चित्रा 4: वीएम निष्पादन ओपकोड का राज्य परिवर्तन आंकड़ा

नोट: यह दस्तावेज़ 2022-05-27 तक मिडन परियोजनाओं के लिए मुख्य शाखा के नवीनतम संस्करण का वर्णन करता है। अब तक मिडेन की अगली शाखा ने निर्देशों की बहुत सारी पुनर्रचना की है, और आकाशवाणी ने केवल कुछ बाधाओं को लागू किया है।

ढेर की बाधा शर्तें

इस खंड में, हम मुख्य उपयोगकर्ता संचालन निर्देशों की बाधा शर्तों को दिखाएंगे, जिनमें से, old_stack_x निर्देश निष्पादन से पहले स्टैक की x स्थिति में संग्रहीत मान को संदर्भित करता है, new_stack_x x स्थिति में संग्रहीत मान को संदर्भित करता है निर्देश निष्पादन के बाद स्टैक, "–>" स्टैक के बाईं ओर से दाईं ओर मूल्य की प्रतिलिपि को संदर्भित करता है, और "==" समीकरण बाधा को संदर्भित करता है। स्टैक की बाधाएं अपेक्षाकृत सरल हैं, और किसी स्पष्टीकरण की आवश्यकता नहीं है।

शर्त निर्देश

चुनना

बाधा:

 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

यदि स्थिति 1 है, तो x स्टैक के शीर्ष पर है। यदि शर्त 0 है, तो y स्टैक के शीर्ष पर है।

अंकगणित निर्देश

जोड़ें

बाधा:

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

एमयूएल

बाधा:

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

निवेश संबंधी निर्णय

बाधा:

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

नकारात्मक

बाधा:

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

बूल निर्देश

नहीं

बाधा:

 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

तथा

बाधा:

 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

या

बाधा:

 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

हैश निर्देश

आरईएससीआर

लिमिट फंक्शन हैश संतोषजनक हैश फंक्शन प्रोटोकॉल
6 रजिस्टरों पर कब्जा।

बाधा:

 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

निर्देश की तुलना करें

eq के

बाधा:

 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

सीएमपी

तुलना की जाने वाली दो संख्याओं के बिट लंबाई चक्र के अनुसार तुलना करें, जैसे:

ए: [0,1,0,1]
बी: [0,0,1,1]

तुलना निर्देशों को चार बार निष्पादित करने की आवश्यकता है।

बाधा:

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

स्टैक ऑपरेशन निर्देश

dup.n

बाधा:

 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

बदलना

बाधा:

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

रोल4

बाधा:

 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

डिकोडर टिप्पणी की बाधा शर्त

इस खंड में, हम मुख्य प्रवाह संचालन निर्देश की बाधा शर्तों को दिखाएंगे।

उपयोगकर्ता कोड निष्पादन

op_bits

cf_op_bits, ld_op_bits और hd_op_bits की बाधाओं के लिए
बाधा 1: प्रत्येक बिट केवल 0 या 1 हो सकता है।
बाधा 2: जब op_counter 0 नहीं है, ld_ops और hd_ops दोनों 0 नहीं हो सकते।
बाधा 3: जब cf_op_bits hcc है, तो op_counter स्थिति 1 से बढ़ जाएगी।
बाधा 4: BEGIN, LOOP, BREAK, और WRAP निर्देशों को 16 के अनुसार संरेखित करने की आवश्यकता है।
बाधा 5: TEND और FEND निर्देशों को 16 के अनुसार संरेखित करने की आवश्यकता है।
बाधा 6: PUSH निर्देश को 8 के अनुसार संरेखित करने की आवश्यकता है।

बाधा:

 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

एचएसी टिप्पणी

फ्लोऑप्स के रूप में एचएसीसी, इस निर्देश का संचालन करते समय हमेशा स्पंज के राज्य परिवर्तन का कारण बनता है, और इसलिए बाधाओं को पूरा करने की आवश्यकता होती है।

बाधा:

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

शर्त निर्णय

प्रवृत्त होना

सच्ची शाखा के अंत की बाधा के रूप में, इसे दो भागों में विभाजित किया गया है:
बाधा 1: स्पंज राज्य की बाधा है।

स्टैक के शीर्ष पर मान new_sponge_0 के बराबर है। अगर की सही शाखा के अंतिम निष्पादन के बाद स्पंज new_sponge_1 के बराबर है। New_sponge_3 0 के बराबर है।

बाधा 2: ctx_stack की बाधा है। स्टैक के शीर्ष पर मान new_sponge_0 के बराबर है। स्टैक में कोई अन्य तत्व एक स्थिति से स्टैक के शीर्ष पर चला जाएगा।

बाधा 3: लूप_स्टैक की बाधा है। लूप_स्टैक की स्थिति परिवर्तनहीन है।

बाधा:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[1] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n

f_end

झूठी शाखा के अंत की बाधा के रूप में, इसे दो भागों में विभाजित किया गया है:
बाधा 1: स्पंज राज्य की बाधा है। स्टैक के शीर्ष पर मान new_sponge_0 के बराबर है।

अगर की सही शाखा के अंतिम निष्पादन के बाद स्पंज new_sponge_2 के बराबर है। new_sponge_3 0 के बराबर है।

बाधा 2: ctx_stack की बाधा है। स्टैक के शीर्ष पर मान new_sponge_0 के बराबर है। स्टैक में कोई अन्य तत्व एक स्थिति से स्टैक के शीर्ष पर चला जाएगा।

बाधा 3: लूप_स्टैक की बाधा है। लूप_स्टैक की स्थिति अपरिवर्तित रहती है।

बाधा:

 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