Loading...
शृंखला: औपचारिक सत्यापन · 3 में से भाग 3 पाठकवर्ग: नए पाठक। भाग 1 और 2 में औपचारिक सत्यापन तथा Orchard बग की भूमिका बनाई गई थी; यह समापन इन दोनों विचारों को एक वास्तविक प्रणाली में मिलते हुए दिखाता है। आवश्यक हर बात को आगे बढ़ते हुए दोहराया जाएगा। आप क्या समझकर जाएंगे: Zcash ने अपने नए "Ironwood" पूल के बारे में वास्तव में क्या सिद्ध किया, प्रमाण की संरचना क्या है, वह किन चीज़ों को शामिल करता है और किन्हें नहीं, पुराने पूल को सुरक्षित रूप से कैसे हटाया गया, और यह क्रिप्टोग्राफिक धन बनाने के एक नए मानक की ओर क्यों संकेत करता है—इसकी सटीक समझ।
भाग 1 में हमने सीखा कि किसी प्रणाली को सही सिद्ध करने का क्या अर्थ है। भाग 2 में हमने एक वास्तविक खामी देखी जिसे परीक्षण चार वर्षों तक नहीं पकड़ सका—एक अपर्याप्त रूप से बाधित अण्डाकार-वक्र गुणन, जो असीमित अदृश्य नकली धन बनाने की अनुमति दे सकता था। यह लेख उसका समाधान है: Zcash ने केवल पैच के साथ नहीं, बल्कि मशीन-जाँचित प्रमाण के साथ कैसे उत्तर दिया कि बग की पूरी श्रेणी समाप्त हो गई है।
जब कोई बग धन को खतरे में डालता है, तो सामान्य प्रतिक्रिया उसे पैच करके आगे बढ़ जाने की होती है। Zcash ने इससे अधिक महत्वाकांक्षी काम किया। 28 जुलाई, 2026 को सक्रिय किए गए Ironwood नामक नए शील्डेड पूल के साथ, उसके इंजीनियरों ने Lean प्रूफ असिस्टेंट में लिखे 2,700 से अधिक प्रमेयों वाला एक मशीन-जाँचित गणितीय प्रमाण प्रकाशित किया, जो स्थापित करता है कि नया पूल अपनी घोषित मान्यताओं के अंतर्गत नकली सिक्के नहीं बना सकता। प्रमाण सार्वजनिक है, ओपन-सोर्स ironwood रिपॉज़िटरी में उपलब्ध है, और इसे पूरा करने में शोधकर्ताओं तथा क्रिप्टोग्राफरों की तीन टीमों को एक महीने से भी अधिक समय लगा।
यह बात Zcash से आगे भी महत्वपूर्ण है। यह सबसे स्पष्ट वास्तविक उदाहरणों में से एक है कि आप किसी चालू वित्तीय प्रणाली को ले सकते हैं, ठीक-ठीक लिख सकते हैं कि "नकली धन नहीं बन सकता" का क्या अर्थ है, और उसे सिद्ध कर सकते हैं—यह आशा करने के बजाय कि आपके परीक्षण पर्याप्त विस्तृत थे। यह एक वादे को प्रमेय में बदल देता है।
भाग 2 उस अंतर्दृष्टि पर समाप्त हुआ जिसने इसे संभव बनाया। उसे याद करें, क्योंकि आगे की हर बात उसी पर आधारित है:
एक अदृश्य नकली-धन बग केवल प्रोटोकॉल के विनिर्देशन में हो सकता है—वह गणितीय विवरण जिसमें बताया जाता है कि सर्किट को क्या लागू करना चाहिए। जो भी चीज़ पकड़ी जा सकती हो, वह सार्वजनिक लेखांकन में दिखाई देगी। इसलिए विनिर्देशन को सुदृढ़ सिद्ध करने से छिपे नकली-धन बग की पूरी श्रेणी एक साथ समाप्त हो जाती है।
"केवल विनिर्देशन में" क्यों? क्योंकि हर ब्लॉक हर लेनदेन की पूरी सामग्री, उसके प्रमाणों सहित, स्थायी रूप से दर्ज करता है। यदि सॉफ़्टवेयर ने गलती से कोई खराब लेनदेन स्वीकार कर लिया होता, तो कोई भी सुधरे हुए सॉफ़्टवेयर से इतिहास को फिर चला कर उसे देख सकता था। वह साक्ष्य स्थायी और सार्वजनिक है। केवल अंतर्निहित गणित की खामी हमेशा छिपी रह सकती है, क्योंकि उसके विरुद्ध फिर चलाने के लिए कोई "सही संस्करण" नहीं होता। औपचारिक सत्यापन का लक्ष्य इसी खामी पर है।
परीक्षण नमूना इनपुटों पर व्यवहार की जाँच करता है, और Orchard बग ठीक इसलिए छिपा रहा क्योंकि कोई नमूना इनपुट उस तक नहीं पहुँचा। विनिर्देशन का प्रमाण एक साथ सभी इनपुटों को कवर करता है, जिनमें वे किनारी मामले भी शामिल हैं जिन्हें कोई आज़माने के बारे में सोच भी न पाए। चार साल पुरानी अदृश्य खामी को आत्मविश्वास से हटाने के लिए यही एकमात्र पर्याप्त रूप से मजबूत गारंटी है।
प्रमाण एक मुख्य गुण स्थापित करता है, जो उसके नीचे स्थित एक अधिक गहरे गुण से निर्मित है।
बैलेंस इंटीग्रिटी: शील्डेड पूल में संग्रहित छिपा हुआ मूल्य कभी उस शुद्ध सार्वजनिक मूल्य से अधिक नहीं होता जो उसमें प्रवाहित हुआ है।
सादे रूप में यही नकली-धन विरोधी गुण है। धन शील्डेड पूल में प्रवेश कर सकता है (सार्वजनिक रूप से दृश्य) और उससे निकल सकता है (सार्वजनिक रूप से दृश्य), लेकिन अंदर, जहाँ राशियाँ छिपी रहती हैं, कोई मूल्य उत्पन्न नहीं किया जा सकता। इसे एक छोटे लेजर से ठोस बनाते हैं (सत्यापित अंकगणित):
5 + 3 = 8 मूल्य के इनपुट से 4 + 4 = 8 मूल्य के आउटपुट बनते हैं। अंदर आने वाला मूल्य बाहर जाने वाले मूल्य के बराबर है। बैलेंस इंटीग्रिटी बनी रहती है। ✓8 मूल्य के इनपुट, लेकिन 4 + 4 + 2 = 10 के आउटपुट। इससे शून्य से 2 इकाइयाँ निर्मित हो जाएंगी। बैलेंस इंटीग्रिटी इसे निषिद्ध करती है: पूल उसमें प्रवेश किए मूल्य से अधिक कभी भुगतान नहीं कर सकता। ✗बैलेंस इंटीग्रिटी वह गणितीय कथन है कि दूसरी स्थिति कभी वैध लेनदेन उत्पन्न नहीं कर सकती।
बैलेंस इंटीग्रिटी की गारंटी के लिए शोधकर्ताओं को पहले स्वयं शून्य-ज्ञान प्रमाण प्रणाली के बारे में एक अधिक गहरा और सूक्ष्म गुण सिद्ध करना पड़ा। साधारण सुदृढ़ता (भाग 2 का "केवल सत्य कथनों के पास साक्षी होता है") शील्डेड पूल के लिए पर्याप्त नहीं निकलती है, और इसका कारण रोचक है: चूँकि छिपे लेनदेन में कुछ भी हो सकता है, लगभग हर कथन के पास तकनीकी रूप से कोई न कोई साक्षी होता है। इसलिए शोधकर्ताओं ने अधिक मजबूत गुण सिद्ध किया:
ज्ञान सुदृढ़ता: जो भी व्यक्ति वैध लेनदेन प्रमाण बना सकता है, उसके पास वास्तव में एक वैध साक्षी होना चाहिए—अर्थात वास्तविक सिक्के, सही ढंग से व्युत्पन्न, सही पते पर।
इसके लिए औपचारिक उपकरण एक extractor है: ऐसी प्रक्रिया जो किसी भी ऐसे prover से, जो verifier को मना सकता है, वास्तविक साक्षी निकाल सकती है। यदि साक्षी हमेशा निकाला जा सकता है, तो एक विश्वसनीय prover के पास सचमुच वह होना चाहिए था। भाग 2 की भाषा में, ज्ञान सुदृढ़ता औपचारिक वादा है कि कोई सुदृढ़ता अंतराल नहीं है, कोई अनुपस्थित बाधा नहीं है जो झूठे कथन को निकल जाने दे। यह वही सटीक गुण है जिसकी अनुपस्थिति Orchard बग थी। सभी संभावित prover के लिए इसके उपस्थित होने का प्रमाण उस दरवाज़े को पूरी तरह बंद कर देता है।
सत्यापन गंभीर मानवीय प्रयास था, कोई बटन दबाकर मिलने वाला परिणाम नहीं:
ironwood रिपॉज़िटरी में सार्वजनिक रूप से उपलब्ध।इस गुण पर तर्क करने के लिए Lean मॉडल पूरे लेजर को लेनदेनों की सूची के रूप में वर्णित करता है, जिनमें प्रत्येक अपने actions, घोषित सार्वजनिक मूल्य और signatures रखता है। शोधकर्ताओं द्वारा ValidLedger नामक predicate नेटवर्क के consensus नियमों को सीधे लिप्यंतरित करता है: हर action के साक्षी को अपेक्षित शर्तें पूरी करनी होंगी, कोई spend-marker (nullifier) दो बार प्रकट नहीं हो सकता, हर संदर्भित tree state वह होना चाहिए जहाँ प्रणाली वास्तव में पहुँची थी, और हर signature को सत्यापित होना चाहिए। इसके बाद प्रमेय हर वैध लेजर पर परिमाणित होते हैं। यह वाक्यांश—"हर वैध लेजर"—ही पूरा मुद्दा है: नमूना नहीं, बल्कि वे सभी, जो किसी वास्तविक हमलावर द्वारा कभी भी तैयार की जा सकने वाली किसी भी चीज़ का अधिसमूह हैं।
बैलेंस-इंटीग्रिटी परिणाम कई लेजर-स्तरीय प्रमेयों से निर्मित है, जिनमें से प्रत्येक यह सिद्ध करता है कि नकली धन बनाने का एक मार्ग बंद है: हर spend किसी वास्तविक पूर्व आउटपुट से मेल खाता है, कुल मूल्य संरक्षित रहता है, प्राप्त note खर्च करने योग्य रहता है और चोरी नहीं किया जा सकता, तथा खर्च के लिए उचित प्राधिकरण आवश्यक है। एक अलग भाग, binding signature, हर लेनदेन के छिपे मूल्यों को उसके घोषित सार्वजनिक मूल्य से बाँधता है, ताकि छिपा और सार्वजनिक लेखांकन चुपचाप असहमत न हो सके।
एक सूक्ष्म और ईमानदार प्रश्न: प्रमाण एक गणितीय मॉडल के बारे में है, लेकिन नेटवर्क Rust code चलाता है। हम कैसे जानते हैं कि code मॉडल से मेल खाता है?
टीम ने एक सावधानीपूर्वक सीमा निर्धारित की, जिसे वे verifier का fingerprint कहते हैं। सीमा के ऊपर Lean प्रमाण verifier को एक सटीक गणितीय वस्तु के रूप में देखते हैं। उसके नीचे सामान्य Rust implementation है। मुख्य तर्क वही है जो भाग 2 में था:
वास्तविक सॉफ़्टवेयर सिद्ध मॉडल से जिस भी प्रकार भिन्न हो सकता है, वह एक implementation बग होगा, और implementation बग केवल पकड़े जा सकने वाला नकली धन ही उत्पन्न कर सकते हैं, क्योंकि हर स्वीकृत प्रमाण स्थायी रूप से दर्ज होता है और सुधरे हुए सॉफ़्टवेयर से फिर चलाया जा सकता है।
इसलिए प्रमाण अदृश्य श्रेणी (विनिर्देशन) को संभालता है, और स्थायी सार्वजनिक रिकॉर्ड पकड़े जा सकने वाली श्रेणी (implementation) को संभालता है। उनके बीच अदृश्य नकली-धन बग के छिपने की कोई जगह नहीं है। टीम ने वास्तविक verifier चलाकर और यह पुष्टि करके भी cross-check किया कि वह कैप्चर किए गए मामलों में fingerprint को ठीक-ठीक पुनरुत्पादित करता है।
भाग 1 ने जोर दिया था कि प्रमाण केवल घोषित मान्यताओं के अंतर्गत विनिर्देशन पूरा होने की गारंटी देता है, और इसका अर्थ कभी भी "अब कोई बग नहीं होगा" नहीं होता। Zcash की टीम इस बात के बारे में प्रशंसनीय रूप से सटीक थी, और ईमानदार शैक्षिक लेखन को भी ऐसा ही होना चाहिए।
प्रमाण Ironwood की सुरक्षा को मानक और स्पष्ट नाम वाली मान्यताओं के एक छोटे समूह तक सीमित करता है। विशेष रूप से, इसकी सुदृढ़ता उस अण्डाकार वक्र पर discrete logarithm problem की कठिनाई पर आधारित है जिसका Ironwood उपयोग करता है (यह एक अच्छी तरह अध्ययन की गई मान्यता है, जहाँ सर्वोत्तम ज्ञात हमले के लिए लगभग 2^126 operations लगेंगे—किसी भी व्यावहारिक गणना से कहीं अधिक), साथ ही hash function के लिए मानक modeling assumptions पर। दो सीमाएँ स्पष्ट रूप से बताना आवश्यक है:
उपलब्धि को कमज़ोर करने के बजाय, इन सीमाओं का नाम लेना ही इसे भरोसेमंद बनाता है। दावा सटीक है: मानक क्रिप्टोग्राफिक मान्यताओं के अंतर्गत, यह पूल अदृश्य नकली सिक्के नहीं बना सकता। यह आशा नहीं, एक प्रमेय है, और इसका सटीक दायरा खुले रूप से बताया गया है।
नए पूल को सुदृढ़ सिद्ध करना फिर भी एक प्रश्न छोड़ता है: पुराने Orchard पूल का क्या, जहाँ खामी चार वर्षों तक रही? आप उसके अतीत को उजागर नहीं कर सकते। लेकिन उसके भविष्य को सीमित कर सकते हैं।
Zcash ने turnstile नामक एक तंत्र प्रस्तुत किया। नियम सरल और शक्तिशाली है:
मूल्य पुराने पूल से केवल उस राशि तक ही बाहर जा सकता है, जितनी सत्यापनीय रूप से उसमें प्रवेश कर चुकी है।
चूँकि शील्डेड पूल में धन का प्रवेश और निकास सार्वजनिक रूप से दिखाई देता है (केवल अंदर की गतिविधि छिपी होती है), turnstile पूरे नेटवर्क को जाँचने देता है कि कभी जितना गया था, उससे अधिक बाहर नहीं निकला। यदि पुराने पूल के भीतर नकली सिक्के बनाए गए होते, तो वे इस सीमा से टकराते और बाहर निकलने में विफल होते। और जैसे-जैसे ईमानदार धन बाहर स्थानांतरित होता है तथा कोई अतिरिक्त राशि प्रकट नहीं होती, समुदाय को मजबूत सार्वजनिक साक्ष्य मिलता है कि खामी का कभी दुरुपयोग नहीं हुआ। गोपनीयता तोड़े बिना किसी निजी पूल की आपूर्ति का ऑडिट करने के यह सबसे निकट की चीज़ है, और Zcash की गोपनीयता बनाए रखते हुए आपूर्ति इंटीग्रिटी को Bitcoin जैसी chain के पारदर्शी मॉडल के अधिक निकट लाता है।
Ironwood स्वयं सुधारे गए proof circuit का पुनः उपयोग करता है, एक खाली पूल से नई शुरुआत करता है, और भविष्य को ध्यान में रखने वाली सुरक्षा जोड़ता है (जिनमें ऐसे प्रावधान शामिल हैं कि यदि भविष्य के quantum computers आज की क्रिप्टोग्राफी को कभी खतरे में डालें, तो धन वापस पाने योग्य बना रहे)। नई शील्डेड गतिविधि अब Ironwood से प्रवाहित होती है, जबकि पुराना Orchard पूल केवल निकासी तक सीमित है।
Ironwood, Zcash के निर्माण के तरीके में व्यापक बदलाव का हिस्सा है। इसका अगली पीढ़ी का scaling प्रयास (Tachyon नामक architecture, जो recursive proofs और Ragu नामक toolkit पर निर्मित है) उस दर्शन के अंतर्गत विकसित किया जा रहा है जिसे कभी-कभी high-assurance cryptography कहा जाता है: मशीन-जाँचित औपचारिक सत्यापन को बाद में सोचने वाली बात नहीं, बल्कि नए क्रिप्टोग्राफिक systems जारी करने का मानक भाग मानना।
तर्क सम्मोहक है। अत्याधुनिक क्रिप्टोग्राफी ठीक वह क्षेत्र है जहाँ मानवीय अंतर्ज्ञान सबसे कमज़ोर होता है और जहाँ एक सूक्ष्म, अपरिक्षित किनारी मामला वर्षों तक छिप सकता है, जैसा कि Orchard ने दिखाया। विनिर्देशन को सिद्ध करना ही वह एक तकनीक है जो "सभी संभव इनपुटों" तक विस्तृत होती है और निर्माण के आधार पर उन अंतरालों को बंद कर देती है। टीम ने संकेत दिया है कि समय के साथ वह इस जाँच को implementation और उससे आगे तक विस्तृत करना चाहती है। इस मानक को Zcash के भीतर और बाहर अधिक व्यापक रूप से अपनाया जाता देखने की अपेक्षा करें।
स्पष्टता के लिए हमने सरल बनाया है। वास्तविक Lean development यहाँ दिए गए खाके की अपेक्षा कहीं अधिक विस्तृत है, जिसमें actions, statements, commitments, nullifiers और signatures की सटीक परिभाषाएँ हैं; "बैलेंस इंटीग्रिटी" और "ज्ञान सुदृढ़ता" की बिल्कुल औपचारिक परिभाषाएँ हैं जिन्हें हमने केवल शब्दों में बताया; discrete-log कठिनाई तक पहुँचने वाला reduction कई मध्यवर्ती मॉडलों (prover का एक algebraic मॉडल और hash का random-oracle मॉडल) से होकर गुजरता है, जिन्हें हमने "मानक मान्यताओं" में संक्षिप्त कर दिया; और हमने fingerprint तथा turnstile को वैचारिक स्तर पर वर्णित किया। इनमें से कुछ भी मूल कहानी को नहीं बदलता: "नकली धन नहीं" का विनिर्देशन, सभी वैध लेजर पर मशीन-जाँचित प्रमाण, दायरे और मान्यताओं का स्पष्ट एवं ईमानदार कथन, और त्रुटिपूर्ण पूल का सुरक्षित हटाया जाना। आधिकारिक विवरण के लिए Project Tachyon के प्रकाशित सत्यापन लेखों और ironwood proof repository को देखें।
| शब्द | सरल अर्थ |
|---|---|
| Ironwood | Zcash का नया शील्डेड पूल (2026), जो त्रुटिपूर्ण Orchard पूल का स्थान लेता है |
| Balance integrity | पूल उसमें सार्वजनिक रूप से प्रवेश किए मूल्य से अधिक कभी भुगतान नहीं करता |
| Knowledge soundness | वैध प्रमाण के लिए prover के पास वास्तविक साक्षी होना आवश्यक है |
| Extractor | ऐसी प्रक्रिया जो किसी भी विश्वसनीय prover से साक्षी निकालती है |
| Lean | सत्यापन को मशीन से जाँचने के लिए उपयोग किया गया प्रूफ असिस्टेंट |
| ValidLedger | consensus नियमों का औपचारिक मॉडल, जिस पर प्रमेय तर्क करते हैं |
| Fingerprint | सिद्ध गणित और चल रहे Rust सॉफ़्टवेयर के बीच की सीमा |
| Under stated assumptions | प्रमाण तभी लागू होता है जब नामित क्रिप्टोग्राफिक मान्यताएँ लागू रहें |
| Turnstile | नियम जो पूल के निकास को उसके सत्यापनीय deposits तक सीमित करता है |
| High-assurance cryptography | औपचारिक सत्यापन को मानक चरण के रूप में लेकर crypto बनाना |
क्या प्रमाण का अर्थ है कि Ironwood बग-मुक्त है? नहीं, और वह ऐसा दावा भी नहीं करता। यह घोषित मान्यताओं के अंतर्गत एक सटीक गुण, बैलेंस इंटीग्रिटी, सिद्ध करता है। यह अदृश्य नकली धन को असंभव बनाता है, हर कल्पनीय बग को नहीं।
क्या प्रमाण यह गारंटी देता है कि मेरे लेनदेन निजी हैं? नहीं। सत्यापन आपूर्ति सुदृढ़ता (कोई नकली धन नहीं) को कवर करता है, पूल की अलग गोपनीयता गारंटियों को नहीं। उनके लिए अलग तर्क दिए जाते हैं।
मनुष्यों (और AI) द्वारा लिखे प्रमाण पर भरोसा क्यों करें? क्योंकि यह मशीन-जाँचित है। Lean प्रूफ असिस्टेंट हर चरण को यांत्रिक रूप से सत्यापित करता है, इसलिए भरोसा हर चरण में किसी मनुष्य या AI की सावधानी पर नहीं, विनिर्देशन और नामित मान्यताओं पर आधारित है।
पुराने Orchard पूल में अभी भी पड़े सिक्कों का क्या होता है? उन्हें निकाला जा सकता है, लेकिन केवल उस राशि तक जो सत्यापनीय रूप से प्रवेश कर चुकी थी; इसे turnstile लागू करता है। इससे आपूर्ति इंटीग्रिटी की रक्षा होती है और यह प्रदर्शित करने में मदद मिलती है कि पुरानी खामी का कभी दुरुपयोग नहीं हुआ।
क्या कहानी यहीं समाप्त होती है? यह एक मील का पत्थर है, अंतिम रेखा नहीं। Zcash का भविष्य का architecture (Ragu toolkit के साथ Tachyon) औपचारिक सत्यापन को मानक अभ्यास मानकर बनाया जा रहा है, जो इस दृष्टिकोण को और आगे विस्तृत करता है।
कोई दावा करता है: "चूँकि Ironwood औपचारिक रूप से सत्यापित है, इसलिए अब Zcash के साथ कभी कुछ भी गलत होना असंभव है।" तीनों भागों के विचारों का उपयोग करके, दो अलग कारण दें कि यह दावा बहुत व्यापक क्यों है। (उत्तर नीचे है।)
पहला, प्रमाण घोषित मान्यताओं (discrete-log कठिनाई और मानक hash modeling) के अंतर्गत एक विशिष्ट गुण (बैलेंस इंटीग्रिटी) को कवर करता है। यदि कोई क्रिप्टोग्राफिक मान्यता टूट जाए, या विनिर्दिष्ट दायरे से बाहर कोई समस्या उत्पन्न हो (उदाहरण के लिए गोपनीयता, wallet software, या किसी असिद्ध घटक में), तो प्रमाण उसके बारे में कुछ नहीं कहता। दूसरा, औपचारिक सत्यापन यह गारंटी देता है कि प्रणाली लिखे गए विनिर्देशन को पूरा करती है; यदि वह विनिर्देशन स्वयं किसी वास्तविक आवश्यकता को पकड़ने में विफल रहा, तो प्रमाण गलत चीज़ को पूरी निष्ठा से प्रमाणित करेगा। दोनों बातें भाग 1 की सावधानी को दोहराती हैं: प्रमाण सटीक और सीमित होता है, और अपनी शक्ति इसी कारण रखता है कि उसका दायरा ईमानदार है—यह हर चीज़ के कभी गलत न होने की सर्वव्यापी गारंटी नहीं है।
तीन भागों में हम एक सामान्य विचार से एक चालू अनुप्रयोग तक पहुँचे: सॉफ़्टवेयर को केवल परीक्षण करने के बजाय सही सिद्ध करने का अर्थ क्या है (भाग 1), एक वास्तविक अपर्याप्त रूप से बाधित circuit अदृश्य धन कैसे बना सकता था (भाग 2), और बैलेंस इंटीग्रिटी के मशीन-जाँचित प्रमाण ने उस बग की श्रेणी को हमेशा के लिए कैसे हटा दिया (भाग 3)। इन सबको जोड़ने वाला सूत्र एक ही ईमानदार वादा है: "कभी कोई बग नहीं," नहीं; बल्कि "घोषित मान्यताओं के अंतर्गत यह सटीक गुण हर मामले में लागू होता है।" उस धन के लिए जो अपनी राशियाँ स्वयं छिपाता है, यही वह वादा है जिसे सिद्ध करना सार्थक है।
ZecHub के लिए Formal Verification शृंखला का भाग।