Automating Bitvector and Finite Field Equivalence Proofs in Lean
यह शोध पत्र BitModEq को प्रस्तुत करता है, जो एक नवीन Lean टैक्टिक है जो रेंज लेम्मा (range lemmas) और केस एनालिसिस (case analysis) का उपयोग करके बिटवेक्टर्स (bitvectors) और परिमित क्षेत्रों (finite fields) के बीच समानता प्रमाणों को स्वचालित करता है, जो ज़ीरो-नॉलेज प्रूफ (Zero-Knowledge Proof) सर्किट एनकोडिंग को सत्यापित करने में अत्याधुनिक SMT सॉल्वर से बेहतर प्रदर्शन करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
यहाँ "Automating Bitvector and Finite Field Equivalence Proofs in Lean" पेपर का सरल भाषा और रोज़मर्रा के उदाहरणों के साथ हिंदी अनुवाद दिया गया है।
बड़ी तस्वीर: गणित के दो अलग-अलग रूप (भाषाएँ)
कल्पना कीजिए कि आप यह सत्यापित करने की कोशिश कर रहे हैं कि एक गुप्त रेसिपी (एक ज़ीरो-नॉलेज प्रूफ) सही ढंग से काम करती है या नहीं। समस्या यह है कि रेसिपी दो अलग-अलग भाषाओं में लिखी गई है जो आपस में अच्छी तरह मेल नहीं खातीं:
- फाइनाइट फील्ड्स (Finite Fields): इसे "घड़ी वाले गणित" (Clock Math) की दुनिया के रूप में सोचें। यदि आपके पास 17 घंटों वाली एक घड़ी है, तो 10 और 10 जोड़ने से 20 नहीं मिलता; बल्कि 3 मिलता है (क्योंकि यह वापस घूमकर शुरू पर आ जाता है)। आधुनिक क्रिप्टोग्राफिक सिस्टम (जैसे क्रिप्टोकरेंसी में उपयोग किए जाने वाले) इसी तरह का गणित करते हैं।
- बिटवेक्टर्स (Bitvectors): इसे "कंप्यूटर गणित" के रूप में सोचें। कंप्यूटर घड़ी की तरह वापस नहीं घूमते; उनके पास बस स्विचों की एक निश्चित संख्या होती है जो या तो 'ऑन' होती हैं या 'ऑफ'। यदि आप नंबर जोड़ते हैं और स्विच खत्म हो जाते हैं, तो अतिरिक्त बिट्स को बस काट दिया जाता है।
समस्या:
जब डेवलपर्स इन क्रिप्टोग्राफिक सिस्टम को बनाते हैं, तो उन्हें "घड़ी वाले गणित" को "कंप्यूटर गणित" में अनुवादित करना पड़ता है ताकि वह वास्तविक हार्डवेयर पर चल सके। इस अनुवाद को अरिथमिटाइजेशन (arithmetization) कहा जाता है।
- यदि अनुवाद गलत है, तो पूरा सुरक्षा सिस्टम टूट जाता है।
- इस अनुवाद की जाँच करना अविश्वसनीय रूप से कठिन है।
- मैन्युअल चेकिंग (Manual checking) एक उपन्यास को हर शब्द को आवर्धक लेंस (magnifying glass) से पढ़कर प्रूफरीड करने जैसा है: यह सटीक तो है लेकिन इसमें बहुत समय लगता है और मानवीय त्रुटियों की संभावना बनी रहती है।
- ऑटोमैटिक चेकिंग (Automatic checking) (मानक कंप्यूटर सॉल्वर का उपयोग करके) एक स्पेल-चेकर (वर्तनी सुधारक) का उपयोग करने जैसा है: यह तेज़ है, लेकिन यह अजीब "घड़ी वाले गणित" के नियमों से भ्रमित होकर हार मान लेता है।
समाधान: "BitModEq" ट्रांसलेटर
लेखकों ने Lean नामक एक सिस्टम के भीतर एक नया टूल बनाया है जिसे BitModEq कहा जाता है (Lean एक बहुत ही सख्त गणित शिक्षक की तरह है जो प्रमाण के हर चरण की जाँच करता है)।
BitModEq को एक विशेष अनुवादक के रूप में समझें जो केवल शब्दों को नहीं बदलता; बल्कि यह शब्दों के पीछे के तर्क (logic) को भी समझता है। यह यह साबित करने के लिए कि "घड़ी वाला गणित" वाली रेसिपी और "कंप्यूटर गणित" वाली रेसिपी बिल्कुल समान है, तीन-चरणीय प्रक्रिया का उपयोग करता है:
चरण 1: "अनरैपिंग" (अनुवाद)
टूल "घड़ी वाले गणित" (फाइनाइट फील्ड्स) को लेता है और इसे सामान्य संख्याओं (Natural Numbers) में "अनरैप" करने की कोशिश करता है।
- चुनौती: घड़ी वाले गणित में, $5 - 10$ एक धनात्मक संख्या हो सकती है क्योंकि यह वापस घूम जाती है। सामान्य गणित में, यह ऋणात्मक होती है।
- ट्रिक: टूल नंबरों को देखता है और पूछता है, "क्या इस नंबर के लिए वापस घूमना (wrap around) संभव है?" यदि नंबर छोटे हैं (जैसे कंप्यूटर के बिट्स), तो वह जानता है कि घूमना नहीं होगा। वह सुरक्षित रूप से "घड़ी" के नियमों को हटा देता है और उन्हें सामान्य गणित की तरह मानता है। यदि वह सुनिश्चित नहीं है, तो वह "घड़ी" के नियमों को बनाए रखता है लेकिन एक सुरक्षा जाँच जोड़ देता है।
चरण 2: "सेफ्टी नेट" (रेंज एनालिसिस)
यही इस पेपर का मुख्य आकर्षण (secret sauce) है। गणित को कंप्यूटर बिट्स में बदलने से पहले, यह टूल एक रेंज एनालिसिस (Range Analysis) करता है।
- उपमा: कल्पना कीजिए कि आप एक सूटकेस पैक कर रहे हैं। आप केवल कपड़े नहीं फेंकते; आप सूटकेस का आकार और कपड़ों का आकार भी देखते हैं।
- यह कैसे काम करता है: टूल वेरिएबल्स को देखता है और पूछता है, "यह नंबर अधिकतम कितना बड़ा हो सकता है?"
- यदि वह जानता है कि एक नंबर 0 और 1 के बीच है (जैसे एक सिंगल लाइट स्विच), तो वह जटिल "घड़ी" के नियमों को पूरी तरह से अनदेखा कर सकता है।
- यह चरण समस्या को इतना सरल बना देता है कि कंप्यूटर इसे आसानी से हल कर सके। इस "सेफ्टी नेट" जाँच के बिना, कंप्यूटर जटिलता से घबराकर हार मान लेता है।
चरण 3: "बिट-ब्लास्टिंग" (अंतिम प्रमाण)
एक बार जब टूल समस्या को शुद्ध "कंप्यूटर गणित" (बिट्स) में सरल बना देता है, तो वह बिट-ब्लास्टिंग (bit-blasting) नामक तकनीक का उपयोग करता है।
- उपमा: यह एक जटिल ताले को खोलने के लिए हर एक चाबी के संयोजन (combination) को आज़माने जैसा है।
- चूंकि टूल ने चरण 2 में समस्या को सरल बना दिया है, इसलिए "ताला" अब इतना छोटा है कि कंप्यूटर हर संयोजन को तुरंत आज़मा सके और गणित को सही साबित कर सके।
यह क्यों महत्वपूर्ण है (परिणाम)
लेखकों ने अपने टूल का परीक्षण वास्तविक दुनिया के क्रिप्टोग्राफिक सिस्टम (विशेष रूप से Jolt और CirC) पर किया।
- प्रतिस्पर्धा: उन्होंने अपने टूल की तुलना सबसे अच्छे मौजूदा ऑटोमैटिक सॉल्वरों (जैसे
cvc5) से की। - परिणाम: मौजूदा सॉल्वर अक्सर बड़े होने पर (जैसे 32-बिट नंबर) अटक जाते थे या समय समाप्त (timeout) हो जाते थे। वे एक डिक्शनरी पढ़ने की कोशिश कर रहे स्पेल-चेकर की तरह थे।
- BitModEq की जीत: नए टूल ने मौजूदा उपकरणों की तुलना में 19% अधिक समस्याओं को हल किया। यह उन बड़े नंबरों (32 बिट्स तक) को भी संभाल सका जहाँ अन्य उपकरण विफल हो गए थे।
- बोनस: क्योंकि यह Lean के अंदर चलता है, प्रमाण कर्नेल-चेक्ड (kernel-checked) है। इसका मतलब है कि कंप्यूटर ने केवल अनुमान नहीं लगाया; इसने तर्क के एक सख्त सेट का पालन किया जो गारंटी के साथ सही है, जिससे छिपे हुए बग्स का जोखिम कम हो जाता है।
एक वास्तविक खोज
अपने परीक्षण के दौरान, टूल ने वास्तव में CirC कंपाइलर में एक बग (त्रुटि) खोज निकाला। कंपाइलर में बड़े नंबरों (विशेष रूप से 32-बिट राइट शिफ्ट) को संभालने में एक गलती थी। यह बग केवल बड़े नंबरों के साथ दिखाई दिया, यही कारण है कि पिछले छोटे-स्तर के परीक्षणों ने इसे मिस कर दिया। लेखकों द्वारा रिपोर्ट किए जाने के बाद डेवलपर्स ने इस बग को ठीक कर दिया।
सारांश
यह पेपर एक नया तरीका प्रस्तुत करता है जिससे यह स्वचालित रूप से सत्यापित किया जा सके कि क्रिप्टोग्राफिक गणित सही ढंग से काम करता है। "घड़ी वाले गणित" और "कंप्यूटर गणित" के बीच संघर्ष करने के बजाय, उन्होंने एक स्मार्ट अनुवादक बनाया है जो:
- पहले नंबरों के आकार की जाँच करता है (रेंज एनालिसिस)।
- अनावश्यक "घड़ी" के नियमों को हटाकर गणित को सरल बनाता है।
- अंतिम परिणाम को सिद्ध करने के लिए ब्रूट-फोर्स लॉजिक का उपयोग करता है।
यह जटिल सुरक्षा प्रणालियों को सत्यापित करना तेज़, अधिक विश्वसनीय और सक्षम बनाता है, जिससे ऐसे बग पकड़े जा सकते हैं जिन्हें अन्य उपकरण छोड़ देते हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।