💻 computer science

Formal Verification of Imperative First-Class Functions in Move

यह शोध पत्र मूव प्रोवर (Move Prover) का एक विस्तार प्रस्तुत करता है जो व्यवहारिक विधेयकों (behavioral predicates), अवस्था लेबल (state labels) और एक एसएमटी एनकोडिंग रणनीति (SMT encoding strategy) को पेश करके मूव भाषा में इम्पैरेटिव फर्स्ट-क्लास फंक्शन्स के औपचारिक सत्यापन को सक्षम बनाता है, जो कुशल सत्यापन और स्वचालित विनिर्देश अनुमान (automated specification inference) के लिए मूव के स्टैटिक मेमोरी सेपरेशन का लाभ उठाता है।

मूल लेखक: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

प्रकाशित 2026-05-14

📖 7 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

यहाँ सरल भाषा और रचनात्मक उपमाओं (analogies) का उपयोग करके पेपर की व्याख्या दी गई है।

बड़ी तस्वीर: "स्मार्ट कॉन्ट्रैक्ट" फैक्ट्री

कल्पना कीजिए कि Aptos एक उच्च-सुरक्षा वाली फैक्ट्री है जो Move नामक एक विशेष भाषा का उपयोग करके डिजिटल संपत्ति (जैसे पैसा या टिकट) बनाती है। यह सुनिश्चित करने के लिए कि ये संपत्तियां चोरी न हों या टूट न जाएं, फैक्ट्री एक रोबोट इंस्पेक्टर का उपयोग करती है जिसे Move Prover (MVP) कहा जाता है। यह रोबोट ब्लूप्रिंट (कोड) को पढ़ता है और गणितीय रूप से सिद्ध करता है कि फैक्ट्री चलने से पहले सब कुछ सही ढंग से काम करेगा।

लंबे समय तक, यह रोबोट सरल निर्देशों की जांच करने में बहुत अच्छा था। लेकिन हाल ही में, फैक्ट्री ने एक नया, पेचीदा फीचर जोड़ा है: First-Class Functions।

इन नए फंक्शन्स को जादुई छड़ी (magic wands) की तरह समझें।

पुराना तरीका: आपको जादू करने के लिए छड़ी खुद पकड़नी पड़ती थी। रोबोट को पता होता था कि आप कौन सा जादू कर रहे हैं।
नया तरीका: आप छड़ी को एक बॉक्स में रख सकते हैं, उसे एक दोस्त को दे सकते हैं, उसे एक तिजोरी में स्टोर कर सकते हैं, या उसे ऐसी मशीन को सौंप सकते हैं जिसे यह नहीं पता कि उसके अंदर क्या है। मशीन बस यह जानती है, "मुझे एक छड़ी घुमाने की ज़रूरत है," लेकिन उसे आखिरी क्षण तक यह नहीं पता होता कि वह कौन सी छड़ी है।

इसे Dynamic Dispatch कहा जाता है। यह शक्तिशाली है, लेकिन यह रोबोट इंस्पेक्टर को परेशान कर देता है क्योंकि वह भविष्य देख नहीं सकता कि कौन सा विशिष्ट जादू किया जा रहा है।

समस्या: "ब्लैक बॉक्स" की दुविधा

पेपर बताता है कि लेखकों ने इन जादुई छड़ियों को संभालने के लिए रोबोट इंस्पेक्टर (MVP) को कैसे अपग्रेड किया ताकि वह घबराए नहीं।

पहले, यदि कोई फंक्शन एक "ब्लैक बॉक्स" (एक वेरिएबल जो एक फंक्शन को धारण करता है) था, तो रोबोट को या तो अनुमान लगाना पड़ता था या एक साथ हर संभावना की जांच करनी पड़ती थी, जिससे गणित बहुत जटिल हो जाता था और रोबोट धीमा हो जाता था।

लेखकों ने इसे हल करने के लिए दो नए उपकरण पेश किए:

1. व्यवहार संबंधी प्रेडिकेट्स (Behavioral Predicates): "वारंटी कार्ड"

जादुई छड़ी के अंदर कैसे काम होता है, यह देखने के लिए अंदर झांकने के बजाय, रोबोट अब छड़ी से जुड़े वारंटी कार्ड को देखता है।

पुराना तरीका: "मुझे यह जानने की ज़रूरत है कि यह calculate_price छड़ी कोड की हर लाइन तक कैसे काम करती है, इससे पहले कि मैं आपको इसे उपयोग करने दूँ।"
नया तरीका: "मुझे इस बात की परवाह नहीं है कि छड़ी अंदर कैसे काम करती है। मुझे बस इसके वारंटी कार्ड को पढ़ने की ज़रूरत है। कार्ड कहता है: 'यदि आप मुझे 5 सिक्के देंगे, तो मैं आपको 3 सिक्के वापस कर दूँगा, और मैं कभी टूटूंगा नहीं।'"

पेपर इन्हें Behavioral Predicates कहता है। ये एक अनुबंध (contract) की तरह हैं जो वर्णन करते हैं:

Pre-conditions: छड़ी चलाने से पहले क्या सच होना चाहिए।
Post-conditions: छड़ी चलाने के बाद क्या सच होगा।
Abort conditions: कब छड़ी फट सकती है (विफल हो सकती है)।

यह रोबोट को छड़ी की गुप्त रेसिपी जानने की आवश्यकता के बिना उसके वादे की जांच करने की अनुमति देता है।

2. स्टेट लेबल्स (State Labels): "टाइम-स्टैम्पिंग कैमरा"

कभी-कभी घटनाओं का एक क्रम होता है। कल्पना कीजिए कि एक फैक्ट्री लाइन है जहाँ एक रोबोट कार को पेंट करता है, और फिर दूसरा रोबोट पहिए लगाता है।

यदि आप कार को सुरक्षित साबित करना चाहते हैं, तो आपको पेंटिंग के बाद लेकिन पहिए लगाने से पहले की स्थिति (state) का पता होना चाहिए।

लेखकों ने State Labels पेश किए हैं। इन्हें प्रक्रिया के विशिष्ट बिंदुओं पर रखे गए टाइम-स्टैम्पिंग कैमरों के रूप में समझें।

कैमरा A (शुरुआत): कार कच्चा लोहा (bare metal) है।
कैमरा B (मध्य): कार पेंट की हुई है।
कैमरा C (अंत): पहिए लगे हुए हैं।

रोबोट अब कह सकता है: "मैं जानता हूँ कि पेंटिंग कैमरा A और कैमरा B के बीच हुई थी, और पहिए कैमरा B और कैमरा C के बीच लगाए गए थे।" यह रोबोट को किसी भी क्षण दुनिया कैसी दिख रही थी, इस बारे में भ्रमित हुए बिना जटिल घटनाओं के क्रम के बारे में तर्क करने में मदद करता है।

रोबोट वास्तव में कैसे काम करता है (द "स्विचबोर्ड")

पेपर बताता है कि कैसे लेखक इन विचारों को गणित (SMT logic) में अनुवाद करते हैं जिसे एक कंप्यूटर हल कर सके।

कल्पना कीजिए कि रोबोट के पास एक स्विचबोर्ड है।

परिदृश्य A (ज्ञात छड़ी): यदि रोबोट एक विशिष्ट, ज्ञात छड़ी (जैसे product फंक्शन) देखता है, तो वह स्विच को "डायरेक्ट मोड" पर सेट करता है। वह वारंटी कार्ड को अनदेखा करता है और उस विशिष्ट छड़ी के वास्तविक कोड की जांच करता है।
परिदृश्य B (अज्ञात छड़ी): यदि रोबोट एक जेनेरिक बॉक्स (एक वेरिएबल) देखता है, तो वह स्विच को "एब्स्ट्रैक्ट मोड" पर सेट करता है। वह कोड को पूरी तरह से अनदेखा करता है और केवल वारंटी कार्ड (व्यवहार संबंधी प्रेडिकेट्स) पर भरोसा करता है ताकि सिस्टम को सुरक्षित साबित किया जा सके।

यह कुशल है क्योंकि रोबोट को हर संभव बॉक्स खोलने की कोशिश नहीं करनी पड़ती। वह केवल उन्हीं को खोलता है जिन्हें वह जानता है, और बाकी के लिए, वह अनुबंध (contract) पर भरोसा करता है।

"ऑटो-इंस्पेक्टर" (स्पेसिफिकेशन इन्फरेंस)

पेपर का सबसे शानदार हिस्सा यह है कि रोबोट अब अपने स्वयं के वारंटी कार्ड लिख सकता है।

आमतौर पर, इंसानों को ये कार्ड मैन्युअल रूप से लिखने पड़ते हैं, जो थकाऊ है। लेखकों ने रोब में इसे अपग्रेड किया है ताकि वह कोड को देख सके, यह पता लगा सके कि वारंटी कार्ड को क्या कहना चाहिए, और आपके लिए इसे लिख सके।

इनपुट: जादुई छड़ी वाला एक अस्त-व्यस्त कोड।
रोबोट की कार्रवाई: "मैं देखता हूँ कि यह कोड चेक करता है कि क्या कोई शुल्क (fee) मौजूद है। मैं एक वारंटी कार्ड लिखूँगा जो कहता है: 'यह छड़ी फट जाएगी यदि शुल्क गायब है।'"
परिणाम: रोबोट अपने काम की जांच करता है। यदि कोड कार्ड से मेल खाता है, तो यह पास हो जाता है।

इसे पेपर में एक ऑटोमेटेड मार्केट मेकर (AMM) उदाहरण के साथ प्रदर्शित किया गया है। यह एक ऐसा सिस्टम है जो संपत्तियों का व्यापार करता है। रोबोट ने सिद्ध किया कि भले ही उपयोगकर्ता द्वारा मूल्य निर्धारण नियम (जादुई छड़ी) को बदला जा सकता है, फिर भी सिस्टम कभी क्रैश नहीं होगा या पैसा नहीं खोएगा, बशर्ते कि नई छड़ी वारंटी कार्ड पर लिखे नियमों का पालन करती हो।

उपलब्धि का सारांश

पेपर का दावा है कि उन्होंने स्मार्ट कॉन्ट्रैक्ट्स को सत्यापित करने के एक बड़े सिरदर्द को हल कर दिया है:

इसने "जादुई छड़ियों" (फंक्शन्स) को सुरक्षित रूप से उपयोग करने योग्य बनाया, जिससे उन्हें गतिशील रूप से स्टोर करना, पास करना और बदलना संभव हुआ।
इसने एक नई भाषा (Behavioral Predicates + State Labels) बनाई जो रोबोट को उनके अंदर देखे बिना इन छड़ियों के बारे में बात करने की अनुमति देती है।
इसने "स्विचबोर्ड" दृष्टिकोण का उपयोग करके रोबोट को तेज़ और स्मार्ट बनाया, जो कोड को देखने और अनुबंध को देखने के बीच स्विच करता है।
इसने कागजी कार्रवाई को स्वचालित किया क्योंकि अब रोबोट आपके लिए आवश्यक अनुबंध उत्पन्न कर सकता है।

संक्षेप में, उन्होंने रोबोट इंस्पेक्टर को सिखाया कि किसी अजनबी के रहस्यों को जाने बिना उसके वादे (अनुबंध) पर भरोसा कैसे किया जाए, जिससे फैक्ट्री अधिक सुरक्षित और लचीली बन गई।

तकनीकी सारांश: Move में इम्पैरेटिव फर्स्ट-क्लास फंक्शन्स का औपचारिक सत्यापन (Formal Verification)

समस्या विवरण
मूव प्रूवर (Move Prover - MVP) एक औपचारिक सत्यापन उपकरण है जिसे मूव स्मार्ट कॉन्ट्रैक्ट्स के लिए डिज़ाइन किया गया है, जो मूल रूप से एक मॉड्यूलर, स्टैटिक-डिस्पैच स्पेसिफिकेशन शैली पर आधारित है। हाल ही में मूव भाषा के एक विस्तार में हायर-ऑर्डर फंक्शन्स (higher-order functions) पेश किए गए हैं, जो फंक्शन्स को फर्स्ट-क्लास वैल्यूज के रूप में अनुमति देते हैं जिन्हें तर्क (arguments) के रूप में पास किया जा सकता है, डेटा संरचनाओं में संग्रहीत किया जा सकता है, और ग्लोबल स्टोरेज में सुरक्षित रखा जा सकता है। यह क्षमता डायनेमिक डिस्पैच को सक्षम बनाती है लेकिन उन धारणाओं को तोड़ देती है जिन पर MVP निर्भर था। विशेष रूप से, जब एक फंक्शन को डायनेमिक रूप से कॉल किया जाता है, तो उसके प्री-कंडीशन्स (pre-conditions) और पोस्ट-कंडीशन्स (post-conditions) को कॉल साइट पर हल नहीं किया जा सकता है। कॉलर को फंक्शन-वैल्यू आर्गुमेंट्स के व्यवहार के बारे में अमूर्त रूप से तर्क देना चाहिए, जबकि सत्यापनकर्ता को इन अमूर्त स्पेसिफिकेशनों को उन ठोस (concrete) फंक्शन्स के साथ सामंजस्य बिठाना चाहिए जो कॉल साइट तक पहुँच सकते हैं। अन्य भाषाओं (जैसे Dafny, F*, Verus) के मौजूदा समाधान या तो स्टेट को संशोधित करने वाले इम्पैरेटिव फर्स्ट-क्लास फंक्शन्स का समर्थन करने में विफल रहते हैं या सेपरेशन लॉजिक (separation logic) पर निर्भर करते हैं, जिससे जटिल SMT एनकोडिंग हो सकती है। चुनौती इन डायनेमिक फीचर्स को कुशलतापूर्वक सपोर्ट करने की है, यह सुनिश्चित करते हुए कि सत्यापन तेज़, प्रासंगिक मामलों के लिए पूर्ण, और SMT ट्रिगर अस्थिरता से मुक्त रहे।

कार्यप्रणाली (Methodology)
लेखक तीन प्राथमिक तंत्रों के माध्यम से हायर-ऑर्डर फंक्शन्स को सपोर्ट करने के लिए MVP और मूव स्पेसिफिकेशन भाषा का विस्तार करते हैं:

व्यवहार संबंधी विधेय (Behavioral Predicates): स्पेसिफिकेशन भाषा को ऐसे विधेयों के साथ विस्तारित किया गया है जो विशिष्ट तर्कों ( $\bar{x}$ ) और परिणामों ( $\bar{y}$ ) पर फंक्शन वैल्यूज ( $f$ ) के व्यवहार को लक्षणित करते हैं। इनमें शामिल हैं:
- requires_of<f>(x): प्री-कंडीशन्स।
- aborts_of<f>(x): एबॉर्ट (abort) स्थितियाँ।
- ensures_of<f>(x, y): पोस्ट-कंडीशन्स।
  ये विधेय स्पष्ट रूप से रीड (read) और रीड/राइट (read/write) स्टेट डिपेंडेंसीज़ को ट्रैक करते हैं, जिससे स्पेसिफिकेशन फंक्शन बॉडी को इनलाइन किए बिना अमूर्त रूप से फंक्शन आर्गुमेंट्स को संदर्भित कर सकते हैं।
स्टेट लेबल्स (State Labels): अनुक्रमिक स्टेट ट्रांज़िशन और मध्यवर्ती मेमोरी स्टेट्स के बारे में तर्क करने के लिए, लेखक स्टेट लेबल्स (जैसे $S$ ) पेश करते हैं। ये लेबल्स निष्पादन के विशिष्ट बिंदुओं को नाम देते हैं। विधेय सिंगल-स्टेट ( $S \mid \sim p$ ) या टू-स्टेट ( $S.. \mid \sim q$ ) हो सकते हैं, जो ऑपरेशन्स के अनुक्रमों का वर्णन करने के लिए व्यवहार संबंधी विधेयों के संयोजन को सक्षम करते हैं (उदाहरण के लिए, एक फंक्शन का पोस्ट-स्टेट दूसरे का प्री-स्टेट बनना)।
वेरिएंट डिस्क्रिमिनेशन के माध्यम से SMT एनकोडिंग: SMT स्तर पर, फंक्शन वैल्यूज को एलजेब्रिक डेटाटाइप्स का उपयोग करके एनकोड किया जाता है जो एक फंक्शन वैल्यू के सभी संभावित स्रोतों (ठोस क्लोजर, फंक्शन पैरामीटर, या स्ट्रक्ट फील्ड्स) का प्रतिनिधित्व करते हैं। जब एक फंक्शन वैल्यू को इनवॉक (invoke) किया जाता है:
- यदि ठोस फंक्शन ज्ञात है (जैसे, एक विशिष्ट क्लोजर), तो इनवोकेशन को उस ठोस फंक्शन के प्रभाव द्वारा प्रतिस्थापित किया जाता है।
- यदि फंक्शन अज्ञात है (जैसे, एक पैरामीटर या स्टोरेज से लोड किया गया क्लोजर), तो इनवोकेशन को उस फंक्शन वैल्यू के प्रकार से जुड़े व्यवहार संबंधी विधेयों का उपयोग करके मॉडल किया जाता है।
- एनकोडिंग मेमोरी संशोधनों को मॉडल करने के लिए "हैवोक" (havoc) और "अज्यूम" (assume) कंस्ट्रक्ट्स का उपयोग करती है और यह सुनिश्चित करती है कि फ्रेम कंडीशंस का सम्मान किया जाए, इसके लिए प्री-स्टेट और पोस्ट-स्टेट मेमोरी मैप्स के बीच अंतर किया जाता है।

मुख्य योगदान
पेपर निम्नलिखित विशिष्ट योगदानों का विवरण देता है:

भाषा विस्तार: व्यवहार संबंधी विधेयों और स्टेट लेबल्स का परिचय, जो मूव स्पेसिफिकेशन भाषा को स्टेट डिपेंडेंसीज़ को ट्रैक करने में सक्षम फर्स्ट-क्लास नागरिक बनाता है।
MVP में कार्यान्वयन: एक बूगी-आधारित (Boogie-based) एनकोडिंग जो कॉल साइटों पर फंक्शन-वैल्यू वेरिएंट्स के बीच भेद करती है। यह दृष्टिकोण मूव के स्टैटिक मेमोरी सेपरेशन (रिसोर्स मॉडल) का लाभ उठाकर सेपरेशन लॉजिक की आवश्यकता को समाप्त करता है, जिससे अधिक कुशल SMT एनकोडिंग प्राप्त होती है।
स्पेसिफिकेशन इन्फरेंस (Specification Inference): हायर-ऑर्डर कोड को संभालने के लिए MVP के वीकेस्ट-प्रीकंडिशन (WP) एनालिसिस टूल का विस्तार। यह टूल मनमाने मूव बाइटकोड से व्यवहार संबंधी-विधेयक-आधारित स्पेसिफिकेशन को अर्ध-स्वचालित रूप से व्युत्पन्न करता है, जिससे मैनुअल एनोटेशन का बोझ कम होता है और नए कंस्ट्रक्ट्स के लिए वैलिडेशन पाइपलाइन प्रदान होती है।
इम्पैरेटिव साइड इफेक्ट्स को संभालना: Dafny जैसे कुछ मौजूदा उपकरणों के विपरीत, यह दृष्टिकोण रस्ट-शैली के रेफरेंस और ग्लोबल वेरिएबल्स के माध्यम से स्टेट को संशोधित करने वाले इम्पैरेटिव फर्स्ट-क्लास फंक्शन्स को सपोर्ट करता है।

परिणाम और सत्यापन
लेखक एक ऑटोमेटेड मार्केट मेकर (AMM) उदाहरण का उपयोग करके इस दृष्टिकोण का प्रदर्शन करते हैं जहाँ एक प्राइसिंग कर्व को फंक्शन वैल्यू के रूप में संग्रहीत किया जाता है। सिस्टम सफलतापूर्वक सत्यापित करता है:

इनवेरियंट्स (Invariants): "फंक्शन कभी एबॉर्ट नहीं होता," "आउटपुट मोनोटोनिसिटी," और "कांस्टेंट-प्रोडक्ट प्रिजर्वेशन" जैसे गुणों को व्यवहार संबंधी विधेयकों और स्टेट लेबल्स का उपयोग करके सत्यापित किया जाता है।
अनुपालन जाँच (Compliance Checking): स्पेसिफिकेशन इन्फरेंस टूल स्वचालित रूप से प्राइसिंग फंक्शन्स के लिए एबॉर्ट कंडीशन्स को व्युत्पन्न करता है (उदाहरण के लिए, यह पता लगाना कि एक फीस-आधारित प्राइसिंग फंक्शन तब एबॉर्ट होता है जब फीस रिसोर्स गायब होता है), जिससे मैनुअल एनोटेशन के बिना मशीन-रीडेबल अनुपालन जाँच संभव होती है।
टेस्ट सुइट: डायरेक्ट कॉल्स, म्यूचुअल रिकर्सन, हायर-ऑर्डर पैरामीटर्स, और स्टोर्ड-क्लोजर डिस्पैच को कवर करने वाला एक व्यापक टेस्ट सुइट पुष्टि करता है कि एनकोडिंग आंतरिक रूप से सुसंगत है और अनुमानित स्पेसिफिकेशन इतने सटीक हैं कि वे वेरिफायर द्वारा डिस्चार्ज किए जा सकें।

महत्व
पेपर का दावा है कि यह कार्य डायनेमिक डिस्पैच और हायर-ऑर्डर फंक्शन्स वाले मूव स्मार्ट कॉन्ट्रैक्ट्स के नियमित, प्रोडक्शन-ओरिएंटेड सत्यापन को सक्षम बनाता है। MVP के कॉस्ट मॉडल को बनाए रखते हुए—जहाँ सत्यापन प्रति फंक्शन सेकंडों में पूरा हो जाता है—यह विस्तार डेवलपर्स को औपचारिक गारंटी के साथ कॉल-बैक आधारित एसेट फ्लो और एक्सटेंसिबल एसेट मैनेजर जैसे जटिल पैटर्न का उपयोग करने की अनुमति देता है। यह दृष्टिकोण मूव के अंतर्निहित स्टैटिक मेमोरी सेपरेशन का उपयोग करके SMT एनकोडिंग को सरल बनाकर सेपरेशन लॉजिक-आधारित टूल्स से अलग है। इसके अलावा, स्पेसिफिकेशन इन्फरेंस का एकीकरण फंक्शन वैल्यूज के अनुपालन को सत्यापित करने के लिए एक व्यावहारिक मार्ग प्रदान करता है, जो हायर-ऑर्डर फंक्शन्स को अपनाने में एक बड़ी बाधा को दूर करता है। यह कार्य स्वीकार करता है कि जबकि एप्लिकेशन-साइड सत्यापन अब फर्स्ट-ऑर्डर फंक्शन्स के समान है, अनुपालन-साइड सत्यापन (यह सिद्ध करना कि पास किया गया फंक्शन एक अनुबंध को संतुष्ट करता है) के लिए जटिल मामलों में अभी भी मैनुअल प्रूफ हिंट्स या विश्वसनीय धारणाओं की आवश्यकता हो सकती है।