एक इनवेरिएंट (invariant) एक ऐसी प्रॉपर्टी है जिसे स्मार्ट कॉन्ट्रैक्ट के डिप्लॉय होने के बाद और इसके पूरे एक्ज़ीक्यूशन के दौरान हमेशा सत्य (true) होना चाहिए। पहली नज़र में, किसी इनवेरिएंट को वेरिफाई करना सीधा लग सकता है: यह मान लें कि किसी फ़ंक्शन कॉल से पहले इनवेरिएंट सत्य है, फ़ंक्शन को रन करें, और पुष्टि करें कि यह बाद में भी सत्य रहता है।

व्यवहार में, यह प्रक्रिया शायद ही कभी इतनी सरल होती है। Certora Prover एक सिम्बॉलिक दुनिया में काम करता है जहाँ यह कॉन्ट्रैक्ट के सभी संभावित स्टेट्स को एक्सप्लोर करता है, न कि केवल उन स्टेट्स को जो वास्तविक रूप से डिप्लॉय किए गए सिस्टम में होंगे। यह विस्तृत, सिम्बॉलिक एक्सप्लोरेशन इसके डिज़ाइन का मूल है; यही कारण है कि Prover उन परिदृश्यों में बग ढूंढ पाता है जिन पर शायद डेवलपर्स कभी विचार न करें।

हालाँकि, Prover द्वारा एक्सप्लोर किया गया हर सिम्बॉलिक स्टेट कॉन्ट्रैक्ट के बिज़नेस लॉजिक के संदर्भ में एक वैध (valid) या पहुँच योग्य (reachable) स्टेट नहीं होता है। बिना किसी अतिरिक्त मार्गदर्शन के, Prover “असंभव” स्टेट्स या स्थितियों से शुरुआत कर सकता है या उनके बारे में तर्क कर सकता है जो एक वास्तविक ब्लॉकचेन एक्ज़ीक्यूशन में कभी पैदा नहीं हो सकते। जब ऐसा होता है, तो Prover किसी वायलेशन (उल्लंघन) को फ़्लैग कर सकता है, भले ही कॉन्ट्रैक्ट स्वयं सही हो, केवल इसलिए क्योंकि विश्लेषण एक अमान्य धारणा (invalid assumption) से शुरू हुआ था।

ऐसे फॉल्स वायलेशन को रोकने के लिए, CVL preserved block प्रदान करता है, जो एक ऐसा मैकेनिज्म है जो हमें यथार्थवादी (realistic) कॉन्ट्रैक्ट व्यवहार के बारे में अतिरिक्त धारणाएं (extra assumptions) निर्दिष्ट करने की अनुमति देता है। ये धारणाएं Prover को वैध और प्रासंगिक एक्ज़ीक्यूशन पाथ्स पर ध्यान केंद्रित करने में मदद करती हैं, और उन स्टेट्स को बाहर कर देती हैं जो तार्किक या प्रासंगिक रूप से असंभव हैं।

इस अध्याय में, हम फॉर्मल वेरिफिकेशन में preserved blocks की भूमिका का पता लगाएंगे। हम चर्चा करेंगे कि वे क्यों आवश्यक हैं, उन्हें CVL में कैसे लिखना है, और वे यह सुनिश्चित करने में कैसे मदद करते हैं कि इनवेरिएंट की जाँच केवल यथार्थवादी परिस्थितियों में की जाए। हम इस अवधारणा को एक व्यावहारिक उदाहरण पर लागू करेंगे जहाँ हम वेरिफाई करेंगे कि, WETH कॉन्ट्रैक्ट में, कॉन्ट्रैक्ट का ETH बैलेंस हमेशा इसकी कुल टोकन सप्लाई (total token supply) के बराबर या उससे अधिक होना चाहिए।

उनकी भूमिका को अधिक स्पष्ट रूप से समझने के लिए, आइए पहले यह फिर से देखें कि Prover यह कैसे जांचता है कि कोई फ़ंक्शन किसी इनवेरिएंट को प्रिजर्व (preserve) करता है या नहीं, और यह प्रक्रिया कभी-कभी क्यों टूट सकती है।

Invariants को अतिरिक्त धारणाओं (Additional Assumptions) की आवश्यकता क्यों होती है

जैसा कि हम जानते हैं, इनवेरिएंट्स को वेरिफाई करते समय, Prover गणितीय इंडक्शन के समान एक संरचित तर्क प्रक्रिया (structured reasoning process) का पालन करता है:

1. Initial-state Check (Base Case): Prover सबसे पहले यह वेरिफाई करता है कि कॉन्ट्रैक्ट के कंस्ट्रक्टर का एक्ज़ीक्यूशन समाप्त होने के तुरंत बाद इनवेरिएंट सत्य है। यह इनवेरिएंट को शुरुआती बिंदु पर सत्य के रूप में स्थापित करता है।
2. Assumption (Pre-state): प्रत्येक पब्लिक और एक्सटर्नल फ़ंक्शन के लिए, Prover यह मान लेता है कि फ़ंक्शन के एक्ज़ीक्यूट होने से पहले इनवेरिएंट सत्य है।
3. Symbolic Execution and Post-state Check: इसके बाद यह सभी संभावित इनपुट्स और कंट्रोल-फ़्लो पाथ्स में फ़ंक्शन को सिम्बॉलिक रूप से एक्ज़ीक्यूट करता है, और वेरिफाई करता है कि इसके बाद भी इनवेरिएंट सत्य रहता है।

यदि इनवेरिएंट इन सभी चेक्स को संतुष्ट करता है, तो इसे सभी कॉन्ट्रैक्ट एक्ज़ीक्यूशन के लिए संरक्षित (preserved) माना जाता है। लेकिन कठिनाई यहीं है: Prover खुद को यथार्थवादी एक्ज़ीक्यूशन पाथ्स तक सीमित नहीं रखता है। यह अत्यधिक असंभावित, और यहाँ तक कि असंभव, स्टेट्स को भी एक्सप्लोर करता है।

उदाहरण के लिए, ERC-20 इनवेरिएंट “the sum of all account balances must always equal the total token supply,” को वेरिफाई करते समय Prover एक ऐसे एक्ज़ीक्यूशन पाथ का एक्सप्लोर कर सकता है जहाँ कॉन्ट्रैक्ट अंततः अपने स्वयं के कार्यों (functions) को कॉल कर लेता है। व्यवहार में, यह स्थिति कभी नहीं होती है, क्योंकि transfer जैसे ERC-20 फ़ंक्शंस को केवल बाहरी उपयोगकर्ताओं या अन्य कॉन्ट्रैक्ट्स द्वारा कॉल किए जाने का इरादा होता है। हालाँकि, क्योंकि Prover व्यवस्थित रूप से सभी संभावित कॉलर्स को एक्सप्लोर करता है, यह उन ट्रेसेस (traces) पर भी विचार करता है जहाँ कॉन्ट्रैक्ट अपने स्वयं के फ़ंक्शंस को इन्वोक (invoke) करता है।

इस तरह के सेल्फ-कॉल्स बेतुके परिदृश्य पैदा कर सकते हैं जहाँ बैलेंस और कुल टोकन सप्लाई असंगत (inconsistent) प्रतीत होते हैं, जिसके कारण Prover एक वायलेशन की रिपोर्ट करता है, भले ही कोई वास्तविक एक्ज़ीक्यूशन इसे ट्रिगर नहीं कर सकता। ये फॉल्स वायलेशन (false violations) के क्लासिक उदाहरण हैं: इनवेरिएंट केवल इसलिए टूटा हुआ दिखाई देता है क्योंकि Prover ने उन स्टेट्स के बारे में तर्क किया है जो वास्तविकता में नहीं हो सकते हैं।

यहीं पर preserved blocks काम आते हैं। Preserved blocks हमें इनवेरिएंट वेरिफिकेशन के दौरान अतिरिक्त धारणाएं पेश करने की अनुमति देते हैं, जो Prover को असंभव या अप्रासंगिक स्टेट्स को अनदेखा करने और केवल यथार्थवादी स्टेट्स पर ध्यान केंद्रित करने के लिए निर्देशित करते हैं।

अब जब हम समझ गए हैं कि preserved blocks क्यों आवश्यक हैं, तो आइए आगे बढ़ते हैं कि उन्हें CVL में कैसे लिखा जाता है।

Preserved Block को कैसे डिफाइन करें?

एक preserved block, CVL में एक विशेष कंस्ट्रक्ट है जो हमें किसी इनवेरिएंट को साबित (prove) करते समय अतिरिक्त धारणाएं (extra assumptions) जोड़ने की सुविधा देता है। इसे Prover को एक छोटा सा “हिंट” देने के रूप में सोचें कि सिस्टम वास्तव में कैसे व्यवहार करता है, ताकि यह असंभव परिदृश्यों को एक्सप्लोर करने में समय बर्बाद न करे।

हम इनवेरिएंट एक्सप्रेशन के ठीक बाद preserved कीवर्ड का उपयोग करके एक preserved block डिफाइन करते हैं। इसका सबसे सरल रूप इस तरह दिखता है:

Copy
invariant invariant_name()
    invariant_expression
{
    preserved {
        // assumptions about the invariant
    }

}

कभी-कभी, हम नहीं चाहते कि एक preserved block हर जगह लागू हो — केवल किसी विशेष फ़ंक्शन के लिए, या केवल कुछ एनवायर्नमेंटल विवरणों (जैसे msg.sender या msg.value) के साथ। उस स्थिति में, हम एक वैकल्पिक फ़ंक्शन सिग्नेचर और एक वैकल्पिक with क्लॉज (ट्रांजेक्शन एनवायर्नमेंट तक पहुंचने के लिए) के साथ सिंटैक्स का विस्तार कर सकते हैं:

Copy
invariant invariant_name(param_1, param_2,...)
    invariant_expression;
{
    preserved functionName(type arg, ...) with (env e) {
        // additional assumptions applicable only for this particular function
    }

}

जेनेरिक (generic) preserved blocks और फ़ंक्शन-विशिष्ट (function-specific) preserved blocks दोनों ही इनवेरिएंट चेकिंग के इंडक्शन स्टेप के दौरान लागू होते हैं। वे प्री-स्टेट में इनवेरिएंट के सत्य होने की धारणा (assumption) के बाद लेकिन संबंधित मेथड के सिम्बॉलिक रूप से एक्ज़ीक्यूट होने से पहले एक्ज़ीक्यूट किए जाते हैं, जिससे यह सुनिश्चित होता है कि Prover प्रत्येक इंडक्शन स्टेप को एक ऐसे स्टेट से शुरू करता है जो गणितीय रूप से वैध (mathematically valid) और प्रासंगिक रूप से यथार्थवादी (contextually realistic) दोनों है।

अब तक, preserved blocks उन धारणाओं को निर्धारित करते हैं जिनके तहत प्रत्येक प्रासंगिक फ़ंक्शन का विश्लेषण किया जाता है। हालाँकि, कुछ मामलों में, हम यह भी प्रतिबंधित करना चाह सकते हैं कि इनवेरिएंट को शुरुआत में किन फ़ंक्शंस के विरुद्ध जांचा जाए। इस उद्देश्य के लिए CVL एक फ़िल्टर ब्लॉक प्रदान करता है, जिसे filtered { … } के रूप में लिखा जाता है। (आप फ़िल्टर ब्लॉक के बारे में यहाँ अधिक पढ़ सकते हैं)

Copy
invariant invariant_name()
    invariant_expression;
    filtered {
        // restrict which functions are checked
    }
{
    preserved functionName(type arg, ...) with (env e) {
        // assumptions or requireInvariant statements
    }

}

जब एक फ़िल्टर ब्लॉक मौजूद होता है, तो इनवेरिएंट को केवल फ़िल्टर में शामिल फ़ंक्शंस के खिलाफ चेक किया जाता है, और कोई भी preserved block उस प्रतिबंधित सेट के भीतर लागू होता है। इस कारण से, preserved block को फ़िल्टर ब्लॉक के बाद लिखा जाता है।

एक फ़िल्टर ब्लॉक यह प्रतिबंधित करता है कि इनवेरिएंट को किन फ़ंक्शंस के विरुद्ध चेक किया जाए। एक जेनेरिक preserved ब्लॉक (preserved with (env e) { ... }) फिर उस फ़िल्टर्ड सेट के हर फ़ंक्शन पर लागू होता है। एक फ़ंक्शन-विशिष्ट preserved ब्लॉक (preserved functionName(…) with (env e) { ... }) केवल तभी लागू होता है जब Prover उस नामित (named) फ़ंक्शन की जाँच कर रहा हो। यदि नामित फ़ंक्शन फ़िल्टर द्वारा शामिल नहीं किया गया है, तो उस preserved block का कोई प्रभाव नहीं पड़ता है।

संक्षेप में, फ़िल्टर्स यह सीमित करते हैं कि एक इनवेरिएंट कहाँ लागू किया गया है, और preserved blocks यह वर्णन करते हैं कि जब वे फ़ंक्शंस एक्ज़ीक्यूट होते हैं तो क्या सत्य रहना चाहिए। एक साथ उपयोग किए जाने पर, वे Prover को अप्रासंगिक या असंभव स्टेट्स से विचलित हुए बिना इनवेरिएंट्स की जांच करने के लिए एक स्पष्ट मार्ग (clear path) देते हैं।

हालाँकि, व्यवहार में, जब कोई इनवेरिएंट अवास्तविक सिम्बॉलिक एक्ज़ीक्यूशन के कारण विफल हो जाता है तो आमतौर पर फ़िल्टर ब्लॉक्स की तुलना में preserved blocks को प्राथमिकता दी जाती है। दोनों मैकेनिज्म Prover के सर्च स्पेस को प्रतिबंधित करते हैं और किसी प्रमाण (proof) को कमजोर होने से बचाने के लिए उनका सावधानीपूर्वक उपयोग किया जाना चाहिए, लेकिन फ़िल्टर अधिक जोखिम भरे (riskier) होते हैं क्योंकि वे इनवेरिएंट चेकिंग से पूरे फ़ंक्शंस को हटा देते हैं।

Preserved blocks आमतौर पर अधिक सुरक्षित होते हैं क्योंकि वे व्यवहार को पूरी तरह से बाहर करने के बजाय स्टेट या एक्ज़ीक्यूशन एनवायर्नमेंट के बारे में धारणाओं (assumptions) को विवश (constrain) करते हैं। परिणामस्वरूप, वे असंभव स्टेट्स को बाहर करने के लिए अधिक उपयुक्त हैं, जबकि यह सुनिश्चित करते हैं कि इनवेरिएंट को सभी प्रासंगिक कॉन्ट्रैक्ट कार्यक्षमता के खिलाफ जाँचा जाए।

अब जब हमने थ्योरी और सिंटैक्स को कवर कर लिया है, तो आइए देखें कि एक वास्तविक कॉन्ट्रैक्ट: Solady’s WETH पर लागू करके व्यवहार में preserved blocks कैसे काम करते हैं।

सबको एक साथ रखना: एक WETH Invariant को वेरिफाई करना

सब कुछ संदर्भ में रखने के लिए, आइए Solady WETH कॉन्ट्रैक्ट — एक ERC-20 इम्प्लीमेंटेशन जो WETH टोकन के साथ 1:1 के अनुपात में ईथर (ETH) को रिप्रेजेंट करता है — के एक इनवेरिएंट को वेरिफाई करें। इस कॉन्ट्रैक्ट की एक प्रमुख विशेषता यह है कि इसका ETH बैलेंस हमेशा सर्कुलेशन में मौजूद WETH टोकन की कुल संख्या के बराबर या उससे अधिक होना चाहिए।

हमारे WETH Invariant को डिफाइन करना

इस इनवेरिएंट को वेरिफाई करने के लिए, नीचे दिए गए स्टेप्स का पालन करें:

1. अपनी Certora प्रोजेक्ट डायरेक्टरी के अंदर, contracts सबडायरेक्टरी में ERC20.sol नाम की एक नई फ़ाइल बनाएँ, और Solady से इस कोड को कॉपी करें और इसमें पेस्ट करें।
2. उसी contracts सबडायरेक्टरी में WETH.sol नाम की एक और फ़ाइल बनाएँ, और इस कोड को इसमें कॉपी करें।
3. specs सबडायरेक्टरी में, weth.spec नाम की एक नई फ़ाइल बनाएँ।
4. weth.spec के अंदर, इनवेरिएंट tokenIntegrity() को इस प्रकार डिफाइन करें:

Copy
invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();

नोट: CVL में, nativeBalances नेटिव टोकन बैलेंस की एक मैपिंग है — उदाहरण के लिए, एथेरियम पर ETH। किसी एड्रेस a के बैलेंस को nativeBalances[a] का उपयोग करके व्यक्त किया जा सकता है। आइडेंटिफ़ायर currentContract वेरिफाई किए जा रहे मुख्य कॉन्ट्रैक्ट को संदर्भित करता है। इसलिए, nativeBalances[currentContract] वेरिफाई किए जा रहे कॉन्ट्रैक्ट के नेटिव टोकन बैलेंस को दर्शाता है।

5. एक methods ब्लॉक जोड़ें जिसमें totalSupply() का फ़ंक्शन सिग्नेचर शामिल हो:

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();

6. confs सबडायरेक्टरी में, weth.conf नाम की एक कॉन्फ़िगरेशन फ़ाइल बनाएँ:

Copy
{
    "files": [
        "contracts/WETH.sol:WETH"
    ],
    "verify": "WETH:specs/weth.spec",
    "optimistic_loop" : true,
    "msg": "Check WETH contract integrity"
}

वेरिफिकेशन रन करना

एक बार जब आप उपरोक्त सभी स्टेप्स एक्ज़ीक्यूट कर लेते हैं, तो हमारे स्पेसिफिकेशन को वेरिफाई करने के लिए certoraRun confs/weth.conf कमांड रन करें और नीचे दी गई छवि के समान एक परिणाम देखें:

हमारे वेरिफिकेशन रन का उपरोक्त परिणाम दर्शाता है कि tokenIntegrity इनवेरिएंट विफल (fail) हो गया क्योंकि Prover को एक ऐसा परिदृश्य मिला जहाँ कॉन्ट्रैक्ट का ETH बैलेंस रिपोर्ट की गई कुल सप्लाई से कम हो सकता है।

वायलेशन (Violation) को समझना

हमारी विस्तृत विश्लेषण रिपोर्ट (detailed analysis report) में पाया गया है कि हमारा इनवेरिएंट tokenIntegrity, “Induction base: After the constructor” ✅ को पास कर चुका है, जिसका अर्थ है कि डिप्लॉयमेंट के तुरंत बाद प्रॉपर्टी सत्य रहती है। हालाँकि, यह “Induction step: after external (non-view/pure) method execution” ❌ के दौरान विफल हो गया, जो यह इंगित करता है कि हालांकि इनवेरिएंट शुरुआत में वैध (valid) होता है, लेकिन यह कुछ स्टेट-बदलने वाले (state-changing) फ़ंक्शन कॉल्स के बाद लगातार सत्य नहीं रहता है।

वायलेशन के कारण को समझने के लिए, हमें विफल होने वाले फ़ंक्शंस के कॉल ट्रेसेस (call traces) का विश्लेषण करने की आवश्यकता है।

आइए deposit() फ़ंक्शन से शुरुआत करें।

deposit() कॉल के वायलेशन को समझना

deposit() फ़ंक्शन के कॉल ट्रेस के हमारे विश्लेषण से कुछ असामान्य बात सामने आती है: सेंडर और रिसीवर दोनों कॉन्ट्रैक्ट स्वयं (WETH) ही है।

यह परिदृश्य — जहाँ कॉन्ट्रैक्ट अपने स्वयं के deposit() को कॉल करता है — व्यावहारिक दृष्टिकोण से एक बेतुका मामला (absurd case) है, क्योंकि WETH कॉन्ट्रैक्ट में ऐसा कोई कोड पाथ नहीं है जो सीधे या अप्रत्यक्ष रूप से deposit() को कॉल कर सके। जबकि Prover इसे सैद्धांतिक रूप से संभावित इंटरैक्शन के रूप में सही ढंग से पहचानता है, हम preserved ब्लॉक के माध्यम से स्पष्ट रूप से इसे ऐसे मामलों को अनदेखा करने के लिए कह सकते हैं।

receive() कॉल के वायलेशन को समझना

Solidity कॉन्ट्रैक्ट में receive() फ़ंक्शन एक विशेष फ़ंक्शन होता है जो तब स्वचालित रूप से एक्ज़ीक्यूट होता है जब कॉन्ट्रैक्ट को खाली कॉलबेटा (empty calldata) के साथ ईथर प्राप्त होता है। एक कॉन्ट्रैक्ट केवल एक ही ऐसा फ़ंक्शन परिभाषित कर सकता है, और इसका रूप निम्नलिखित होना चाहिए:

Copy
receive() external payable { ... }

receive() फ़ंक्शन आर्ग्यूमेंट्स नहीं ले सकता, मान नहीं लौटा सकता, और साधारण ETH ट्रांसफ़र (जैसे .send, .transfer, या कच्चे (raw) ETH ट्रांसफ़र के माध्यम से) पर ट्रिगर होता है।

WETH इम्प्लीमेंटेशन में receive() फ़ंक्शन केवल deposit() फ़ंक्शन को कॉल्स फॉरवर्ड करता है:

Copy
// @dev Equivalent to `deposit()`.
receive() external payable virtual {
    deposit();
}

इस कारण से, कोई भी अवास्तविक एक्ज़ीक्यूशन पाथ जो deposit() को ब्रेक करता है, वह receive() को भी ब्रेक कर सकता है। Prover receive() को केवल एक अन्य एक्सटर्नल एंट्री पॉइंट के रूप में मानता है, इसलिए यह प्रतीकात्मक रूप से मान सकता है कि कॉन्ट्रैक्ट अपने स्वयं के receive() फ़ंक्शन को कॉल करता है।

विफल ट्रेस में ठीक ऐसा ही हुआ: deposit() की तरह ही, Prover ने एक ऐसा पाथ चुना जहाँ सेंडर और रिसीवर दोनों कॉन्ट्रैक्ट स्वयं (WETH) है, जिससे एक असंभव सेल्फ-कॉल परिदृश्य पैदा हुआ जो वास्तविक एक्ज़ीक्यूशन में नहीं होता है लेकिन इनवेरिएंट को सिम्बॉलिक रूप से विफल करने का कारण बनता है।

withdraw() कॉल के वायलेशन को समझना

withdraw() के कॉल ट्रेस से Prover द्वारा एक अत्यधिक अवास्तविक परिदृश्य (wildly unrealistic scenario) का परीक्षण करने के कारण होने वाली समस्या का पता चलता है। यह समझने के लिए कि यह विफल क्यों होता है, आइए उन सटीक वैल्यूज़ का उपयोग करके कॉल ट्रेस का चरण दर चरण विश्लेषण करें जिनका उपयोग Prover ने किया था।

द प्री-स्टेट चेक (Global State #1)

प्री-स्टेट चेक के दौरान, Prover यह मान लेता है कि फ़ंक्शन के चलने से पहले इनवेरिएंट सत्य है। इस बिंदु पर—जिसे Global State #1 के रूप में कैप्चर किया गया है—यह withdraw() फ़ंक्शन के सिम्बॉलिक एक्ज़ीक्यूशन से पहले संभावित प्रारंभिक स्थितियों (starting conditions) का प्रतिनिधित्व करने वाला एक सिम्बॉलिक एनवायर्नमेंट स्थापित करता है।

इस स्टेट में, कॉन्ट्रैक्ट का ETH बैलेंस 2^256 − 3 पर सेट है, जबकि कुल टोकन सप्लाई केवल 2 है।

इसका मतलब है कि कॉन्ट्रैक्ट एक असंभव स्टेट में शुरू होता है—इसके पास बड़ी मात्रा में ETH है लेकिन कुल टोकन सप्लाई केवल 2 है। कोई भी वास्तविक दुनिया का डिप्लॉयमेंट ऐसी स्थिति तक नहीं पहुंच सकता, लेकिन चूंकि हमने प्रारंभिक स्टेट को विवश (constrain) नहीं किया, इसलिए Prover आर्बिटरेरी वैल्यूज़ (arbitrary values) चुनने के लिए स्वतंत्र था।

इस बिंदु पर, हमारा इनवेरिएंट सत्य है क्योंकि:

Copy
2^256 − 3 ≥ 2  ✅

withdraw() का सिम्बॉलिक एक्ज़ीक्यूशन (Global State #2)

इसके बाद, Prover सिम्बॉलिक रूप से withdraw() फ़ंक्शन को एक्ज़ीक्यूट करता है:

यहाँ, कॉलर (0x8200) 2^256 − 6 निकालने (withdraw) का प्रयास करता है। withdraw() फ़ंक्शन इंटरनल _burn(from, amount) को कॉल करता है। एक वास्तविक एक्ज़ीक्यूशन में, यदि amount > balanceOf(from) हो, तो _burn() तुरंत रिवर्ट (revert) हो जाएगा।

हालाँकि, Prover सिम्बॉलिक रूप से तर्क करता है। जब यह if (amount > balanceOf(from)) चेक पर पहुँचता है, तो यह balanceOf(0x8200) को एक अनबाउंड सिम्बॉलिक वेरिएबल (unbounded symbolic variable) के रूप में मानता है। नॉन-रिवर्टिंग पाथ को एक्सप्लोर करने के लिए, इसे इस बैलेंस के लिए एक ऐसी वैल्यू माननी चाहिए जो इस चेक को पास करने के लिए पर्याप्त बड़ी हो।

हम Global State #3 के नीचे _burn ऑपरेशन्स को देखकर इस मानी गई वैल्यू का पता लगा सकते हैं। ट्रेस एक सिंगल स्टोरेज स्लॉट (कॉलर के बैलेंस) पर क्लासिक “read-modify-write” पैटर्न दिखाता है:

यहाँ बताया गया है कि यह हमें क्या बताता है:

• Prover कॉलर का बैलेंस लोड (loads) करता है। आगे बढ़ने के लिए, यह मान लेता है कि बैलेंस 2^256 - 2 है।
• फिर यह घटाव (subtraction) के बाद नया बैलेंस (0x4) स्टोर (stores) करता है।

हम साधारण गणित से इसकी पुष्टि कर सकते हैं:

Copy
Precall Balance of 0x8200 =  2^256
Withdrawal Amount = 2^256 - 6
Postcall Balance of 0x8200 should be = (2^256 - 2) - (2^256 - 6) = 4

कैलकुलेट किया गया परिणाम 4, Store वैल्यू 0x4 से पूरी तरह मेल खाता है।

द अर्थमेटिक अंडरफ्लो (Arithmetic Underflow) (Global State #3)

एक बार जब _burn() कॉलर के WETH बैलेंस को अपडेट कर देता है, तो यह WETH की कुल सप्लाई (total supply) को अपडेट करता है।

इस बिंदु पर, totalSupply 2 से 8 हो जाती है क्योंकि 2 − (2^256 − 6) का uint256 में अंडरफ्लो (underflow) होता है और यह मॉड्यूलो 2^256 के साथ रैप (wrap) हो जाता है।

नोट: Solidity वर्ज़न ≥0.8.0 में, totalSupply -= amount जैसी सामान्य गणितीय प्रक्रिया अंडरफ्लो होने पर रिवर्ट हो जाएगी। हालाँकि, जब कॉन्ट्रैक्ट unchecked ब्लॉक का उपयोग करता है या इनलाइन असेंबली में ऑपरेशन करता है तो ऐसा नहीं होता है, क्योंकि दोनों लो-लेवल अर्थमेटिक अर्थशास्त्र (low-level arithmetic semantics) का पालन करते हैं जहाँ वैल्यूज़ मॉड्यूलो 2^256 के साथ रैप अराउंड हो जाती हैं।

द अनरिज़ॉल्व्ड ETH ट्रांसफर और AUTO-Havoc (Global State #5)

_burn() पूरा होने के बाद, withdraw() एक लो-लेवल call का उपयोग करके कॉलर को ETH ट्रांसफर करने का प्रयास करता है:

Copy
call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)

withdraw() को कॉल करने से पहले, WETH कॉन्ट्रैक्ट के पास 2^256 − 3 wei थे। withdraw() पर एक सफल कॉल के परिणामस्वरूप कॉलर को 2^256 − 6 wei ट्रांसफर होंगे और कॉन्ट्रैक्ट का ETH बैलेंस 2^256 − 3 से घटकर 3 हो जाना चाहिए।

यदि हम Global State #5 के लिए ट्रेस को देखते हैं, तो हम देखते हैं कि Prover पहले इस कैलकुलेशन को सही ढंग से करता है:

हालाँकि, Prover वहीं नहीं रुकता। कॉल एक बाहरी, अज्ञात (external, unknown) एड्रेस (caller()) पर है। Prover इस कैली (callee) के व्यवहार (यानी, कॉलर के फॉलबैक फ़ंक्शन) को निर्धारित नहीं कर सकता है।

जब Prover को ऐसे अनरिज़ॉल्व्ड एक्सटर्नल कॉल्स (unresolved external calls) का सामना करना पड़ता है, तो यह स्वचालित रूप से एक AUTO-havoc समरी लागू करता है।

AUTO-havoc के तहत, Prover यह मान (assumes) लेता है कि एक्सटर्नल कॉल सफल हो गई है, लेकिन कॉल से संबंधित स्टेट वेरिएबल्स को मनमाने ढंग से बदल सकता है। यह ऐसा इसलिए करता है क्योंकि इसके पास कैली (callee) के कोड का कोई ठोस मॉडल (concrete model) नहीं होता है।

कॉल ट्रेस में, हम देखते हैं कि यह सही कैलकुलेशन के तुरंत बाद होता है:

यह havoc कैलकुलेटेड बैलेंस को ओवरराइट (overwrites) कर देता है। अगले स्टेट (Global State #6) में, कॉन्ट्रैक्ट का बैलेंस है:

इसका मतलब है कि Prover ने कैलकुलेटेड परिणाम (3) को नज़रअंदाज़ कर दिया और havoc समरी के हिस्से के रूप में एक आर्बिटरेरी वैल्यू (5) असाइन कर दी। इसी havoc की गई वैल्यू का उपयोग पोस्ट-स्टेट चेक में किया जाएगा।

पोस्ट-स्टेट और इनवेरिएंट की विफलता (Global State #7)

withdraw फ़ंक्शन के पूरा होने के बाद, Prover पोस्ट-स्टेट में इनवेरिएंट की जाँच करता है:

nativeBalances[currentContract] >= totalSupply()

इस बिंदु पर, सिम्बॉलिक वैल्यूज़ हैं:

• WETH.balance = 0x5 (AUTO-havoc द्वारा सेट)
• WETH.totalSupply() = 0x8 (अंडरफ्लो द्वारा करप्ट (Corrupted) किया गया)

इसलिए इनवेरिएंट का मूल्यांकन होता है:

Copy
5 >= 8 ❌ (false)

Prover निष्कर्ष निकालता है कि इनवेरिएंट का वायलेशन हुआ है।

मूल कारण (The Root Cause)

यह वायलेशन एक क्लासिक फॉल्स पॉज़िटिव (false positive) है। यह WETH कॉन्ट्रैक्ट के withdraw() इम्प्लीमेंटेशन में किसी तार्किक खामी (logical flaw) के कारण नहीं हुआ। इसके बजाय, यह Prover की कम-विवाश (under-constrained) सिम्बॉलिक रीज़निंग का परिणाम था:

1. संपूर्ण एक्ज़ीक्यूशन पाथ केवल इसलिए संभव हुआ क्योंकि Prover ने एक असंभव प्री-स्टेट मान लिया था जहाँ balanceOf(msg.sender) (2^256 - 2), totalSupply (2) से बहुत अधिक बड़ा था।
2. यह अवास्तविक धारणा, जिसे एक अनकंस्ट्रेंड सिम्बॉलिक वेरिएबल (unconstrained symbolic variable) द्वारा अनुमति दी गई थी, ने सीधे totalSupply वेरिएबल में एक अर्थमेटिक अंडरफ्लो को ट्रिगर किया, जिससे यह 2 से 8 में करप्ट हो गया।

auto-havoc स्टेप ने भी अंतिम वैल्यूज़ में योगदान दिया, लेकिन अंडरफ्लो से स्टेट पहले ही अपूरणीय (irrecoverably) रूप से प्रभावित हो चुका था।

Preserved Blocks का उपयोग करके False Violations को ठीक करना

अब जब यह स्पष्ट हो गया है कि Prover ने वायलेशन्स को इसलिए फ़्लैग नहीं किया क्योंकि WETH कॉन्ट्रैक्ट में कोई खामी थी, बल्कि इसलिए किया क्योंकि इसने उन सिम्बॉलिक स्टेट्स को एक्सप्लोर किया जो वास्तविक एक्ज़ीक्यूशन में कभी नहीं हो सकते हैं, हमारा अगला कदम Prover को यथार्थवादी व्यवहार की ओर वापस निर्देशित करना है।

हम preserved blocks जोड़कर ऐसा करते हैं, जो प्री-स्टेट चेक और सिम्बॉलिक एक्ज़ीक्यूशन के बीच अतिरिक्त धारणाएं (assumptions) पेश करते हैं। ये धारणाएं Prover को असंभव एक्ज़ीक्यूशन पाथ्स जैसे कॉन्ट्रैक्ट सेल्फ-इन्वोकेशन या बेतुके टोकन बैलेंस में प्रवेश करने से रोकती हैं।

deposit() और receive() वायलेशन को ठीक करना

दोनों वायलेशन्स Prover द्वारा सेल्फ-कॉल्स (self-calls) मानने के कारण हुए थे, जहाँ WETH कॉन्ट्रैक्ट को अपने स्वयं के कॉलर के रूप में मॉडल किया गया था। यह वास्तविक एक्ज़ीक्यूशन में असंभव है लेकिन सिम्बॉलिक एक्ज़ीक्यूशन में तब तक वैध है जब तक कि इसे प्रतिबंधित (restricted) न किया जाए।

हम एक preserved block जोड़कर इसे ठीक करते हैं जो किसी भी ऐसे परिदृश्य को खारिज करता है जहाँ कॉन्ट्रैक्ट अपने स्वयं के फ़ंक्शंस को कॉल करता है:

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with(env e) {
        require e.msg.sender != currentContract;
    }
}

यह एकल धारणा (single assumption) सभी सेल्फ-कॉल ट्रेसेस को हटा देती है, और तुरंत deposit() और receive() (Prover UI में receiveOrFallback() के रूप में रिपोर्ट किया गया) दोनों में फॉल्स पॉज़िटिव्स को समाप्त कर देती है।

deposit() और receive() दोनों के लिए सेल्फ-कॉल समस्या हल होने के साथ, अब हम फॉल्स वायलेशन्स के दूसरे स्रोत की ओर मुड़ सकते हैं: withdraw() के अंदर अवास्तविक सिम्बॉलिक धारणाएं।

withdraw() वायलेशन को ठीक करना

withdraw() में विफलता किसी अलग कारण से हुई थी: Prover ने यह मान लिया था कि balanceOf(msg.sender) मनमाने ढंग से बड़ा हो सकता है, यहाँ तक कि कुल सप्लाई (total supply) से भी अधिक। इससे _burn() को एक ऐसे पाथ पर एक्ज़ीक्यूट होने के लिए मजबूर होना पड़ा जिसे रिवर्ट होना चाहिए, जिससे अंडरफ्लो ट्रिगर हुआ और totalSupply करप्ट हो गई।

इसे रोकने के लिए, हम विशेष रूप से withdraw() के लिए एक preserved block जोड़ते हैं:

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
    //we also added the signature of balanceOf()
    function balanceOf(address) external returns(uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    // Generic Block
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    // Function-Specific Block
    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

उपरोक्त अपडेटेड स्पेसिफिकेशन में, require balanceOf(e.msg.sender) <= totalSupply(); लाइन Prover को किसी भी ऐसे एक्ज़ीक्यूशन पाथ को अनदेखा करने का निर्देश देती है जहाँ उपयोगकर्ता का टोकन बैलेंस कुल सप्लाई (total supply) से अधिक हो।

एक साथ मिलकर, ये preserved blocks हर अवास्तविक एक्ज़ीक्यूशन पाथ को समाप्त कर देते हैं जो पहले एक फॉल्स वायलेशन का कारण बना था। इन बाधाओं (constraints) के लागू होने के साथ, हम अब यह जांचने के लिए Prover को फिर से रन कर सकते हैं कि क्या यथार्थवादी धारणाओं के तहत इनवेरिएंट सत्य रहता है।

वेरिफिकेशन को फिर से रन करना

दोनों फिक्सेस लागू करने के बाद, Prover को फिर से रन करें और नीचे दी गई छवि के समान आउटपुट देखने के लिए वेरिफिकेशन रिज़ल्ट लिंक खोलें।

इस बार, Prover पुष्टि करता है कि tokenIntegrity इनवेरिएंट सभी वेरिफिकेशन चरणों में सत्य रहता है, जो इंडक्शन बेस (induction base) और इंडक्शन स्टेप (induction step) दोनों को पास करता है।

रिपोर्ट दिखाती है कि सभी प्रासंगिक फ़ंक्शंस — जिसमें deposit(), withdraw(), transfer(), और approve() शामिल हैं — अब इनवेरिएंट को प्रिजर्व करते हैं।

इस बिंदु पर, इनवेरिएंट सफलतापूर्वक वेरिफाई हो गया है, और स्पेसिफिकेशन सही है। हालाँकि, हम इसे और सरल बना सकते हैं। हमने पहले जो दोनों धारणाएं (assumptions) जोड़ी थीं, वे समान संरचना (structure) साझा करती हैं और किसी भी फ़ंक्शन आर्ग्यूमेंट पर निर्भर नहीं करती हैं, जिसका अर्थ है कि हम उन्हें एक सिंगल, क्लीन (clean) preserved block में समेकित (consolidate) कर सकते हैं।

एक अधिक क्लीन (Cleaner) और यूनिफाइड (Unified) स्पेसिफिकेशन

हमारे मामले में, हमने पहले जो दोनों धारणाएं जोड़ी थीं, वे एक महत्वपूर्ण प्रॉपर्टी साझा करती हैं:

“वे केवल ट्रांजेक्शन एनवायर्नमेंट (env) और कॉन्ट्रैक्ट के ग्लोबल स्टेट पर निर्भर करती हैं। वे किसी विशेष फ़ंक्शन के पैरामीटर्स पर निर्भर नहीं करती हैं।”

इसका मतलब है कि वे कॉन्ट्रैक्ट के बारे में वैश्विक सत्य (global truths) हैं:

1. कॉन्ट्रैक्ट कभी भी अपना खुद का कॉलर नहीं होता है।
2. किसी कॉलर का बैलेंस कभी भी कुल सप्लाई (total supply) से अधिक नहीं होता है।

चूंकि दोनों में से कोई भी शर्त किसी फ़ंक्शन के आर्ग्यूमेंट्स पर निर्भर नहीं करती है, इसलिए दोनों को सुरक्षित रूप से एक सिंगल जेनेरिक (generic) preserved block में रखा जा सकता है, जैसा कि नीचे दिखाया गया है:

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

जब हम इस कंबाइंड ब्लॉक का उपयोग करके Prover को रन करते हैं, तो स्पेसिफिकेशन बिना किसी त्रुटि (errors) के स्वीकार कर लिया जाता है और इनवेरिएंट सभी वेरिफिकेशन चरणों में सत्य रहता है, जैसा कि नीचे दी गई छवि में दिखाया गया है:

Constructor Preserved Blocks (Base-Step Assumptions)

अब तक, हमने इनवेरिएंट वेरिफिकेशन के इंडक्शन स्टेप के दौरान Prover को विवश (constrain) करने के एक तरीके के रूप में preserved blocks पर चर्चा की है—अर्थात, यह जांचते समय कि पब्लिक और एक्सटर्नल फ़ंक्शंस किसी इनवेरिएंट को प्रिजर्व करते हैं, यह मानते हुए कि यह पहले से ही सत्य है।

Prover वर्ज़न 8.5.1 से शुरू करते हुए, CVL कंस्ट्रक्टर (constructor) preserved blocks का भी समर्थन करता है, जो इनवेरिएंट वेरिफिकेशन के बेस स्टेप (base step) पर लागू होते हैं।

बेस स्टेप के दौरान, Prover यह वेरिफाई करने के लिए कंस्ट्रक्टर को सिम्बॉलिक रूप से एक्ज़ीक्यूट करता है कि डिप्लॉयमेंट के तुरंत बाद इनवेरिएंट सत्य है। मुख्य कॉन्ट्रैक्ट का स्टोरेज (currentContract) शून्य (zero) पर इनिशियलाइज़ होता है, लेकिन मल्टी-कॉन्ट्रैक्ट सीन्स में, वेरिफिकेशन सीन में अन्य कॉन्ट्रैक्ट्स आर्बिटरेरी सिम्बॉलिक स्टेट्स में शुरू होते हैं।

यह पुराने Prover वर्ज़न्स से एक बदलाव है, जहाँ सभी कॉन्ट्रैक्ट्स का स्टोरेज शून्य माना जाता था—जो पूरे सिस्टम को एक साथ नए सिरे से डिप्लॉय करने के अनुरूप है। वर्तमान व्यवहार डिप्लॉय किए गए सिस्टम की अधिक यथार्थवादी मॉडलिंग (realistic modeling) को सक्षम बनाता है, लेकिन इसका अर्थ यह भी है कि बेस-स्टेप वेरिफिकेशन उन स्टेट्स से शुरू हो सकता है जो वास्तविक डिप्लॉयमेंट में कभी उत्पन्न नहीं होंगे।

जब कोई इनवेरिएंट इन बाहरी कॉन्ट्रैक्ट्स (external contracts) के साथ संबंधों पर निर्भर करता है, तो सिम्बॉलिक एनवायर्नमेंट उन धारणाओं का उल्लंघन कर सकता है जो व्यवहार में सत्य होती हैं, जिसके कारण बेस स्टेप विशुद्ध रूप से सिम्बॉलिक कारणों से विफल हो जाता है। कंस्ट्रक्टर (constructor) preserved blocks हमें इन धारणाओं को स्पष्ट रूप से फिर से पेश करने की अनुमति देते हैं, यह सुनिश्चित करते हुए कि बेस स्टेप एक यथार्थवादी डिप्लॉयमेंट संदर्भ (deployment context) को दर्शाता है।

सिंटैक्स अन्य preserved blocks के समान ही है लेकिन इसका स्कोप कंस्ट्रक्टर तक ही सीमित होता है:

Copy
preserved constructor() with (env e) {
    require e.block.timestamp != 0;
}

यह ब्लॉक केवल बेस स्टेप पर लागू होता है और इसका इंडक्शन स्टेप या इंडिविजुअल फ़ंक्शन वेरिफिकेशन पर कोई प्रभाव नहीं पड़ता है।

इस अध्याय में, WETH केस स्टडी में फॉल्स वायलेशन्स इंडक्शन स्टेप के दौरान उत्पन्न होते हैं, इसलिए उन्हें जेनेरिक और फ़ंक्शन-लेवल preserved blocks का उपयोग करके हल किया जाता है। कंस्ट्रक्टर (constructor) preserved blocks सबसे उपयोगी तब होते हैं जब प्रारंभिक सिम्बॉलिक एनवायर्नमेंट के बारे में अवास्तविक धारणाओं के कारण डिप्लॉयमेंट के तुरंत बाद कोई इनवेरिएंट विफल हो जाता है।

निष्कर्ष (Conclusion)

CVL में इनवेरिएंट वेरिफिकेशन को रिफाइन करने के लिए Preserved blocks एक शक्तिशाली टूल हैं। फ़ंक्शन एक्ज़ीक्यूशन के दौरान और, जब आवश्यक हो, डिप्लॉयमेंट के दौरान Prover को यथार्थवादी धारणाओं तक सीमित करके—वे प्रमाण (proof) की मजबूती को बनाए रखते हुए फॉल्स पॉज़िटिव्स को समाप्त करते हैं।

WETH केस स्टडी के माध्यम से, हमने देखा कि सावधानीपूर्वक चुने गए preserved blocks किस प्रकार Prover को असंभव सिम्बॉलिक स्टेट्स से दूर और सार्थक एक्ज़ीक्यूशंस की ओर निर्देशित कर सकते हैं, यह सुनिश्चित करते हुए कि इनवेरिएंट्स को उन परिस्थितियों में वेरिफाई किया जाता है जो वास्तविक दुनिया के व्यवहार को सटीक रूप से दर्शाती हैं।

यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर आधारित एक श्रृंखला का हिस्सा है।