Loops सबसे आम प्रोग्रामिंग कंस्ट्रक्ट्स में से एक हैं, लेकिन formal verification में इनके बारे में तर्क (reason) करना चुनौतीपूर्ण बना रहता है। जबकि Solidity या किसी अन्य प्रोग्रामिंग भाषा में लूप सरल प्रतीत होता है—जब तक कि कोई शर्त पूरी न हो जाए तब तक केवल एक क्रिया को दोहराना—इसका वेरिफिकेशन घातीय रूप से (exponentially) जटिल हो जाता है। Certora Prover जैसे formal verification इंजन को लूप इटरेशन्स (iterations) की सभी संभावित संख्याओं के बारे में तर्क करना पड़ता है, जो path explosion problem का कारण बनता है: लूप इटरेशन्स या कंडीशनल ब्रांचेज की संख्या बढ़ने के साथ संभावित एग्जीक्यूशन पाथ्स (execution paths) में होने वाली घातीय वृद्धि जिन्हें Prover को एक्सप्लोर करना चाहिए।

इस जटिलता को प्रबंधित करने के लिए, Certora Prover और अन्य formal verification टूल्स bounded loop unrolling नामक तकनीक का उपयोग करते हैं। यह तकनीक यह सीमित करती है कि वेरिफिकेशन के दौरान किसी लूप को सिम्बॉलिक (symbolic) रूप से कितनी बार एक्सप्लोर किया जाता है, जिससे Prover अज्ञात और अनबाउंड (unbounded) लूप इटरेशन्स के कारण होने वाले अन्यथा असंभव सर्च स्पेस (infeasible search space) से बच सकता है।

इस अध्याय में, हम:

• यह समझाएंगे कि loops को verify करना कठिन क्यों है और path explosion problem कैसे उत्पन्न होती है।
• दिखाएंगे कि Prover bounded loop unrolling का उपयोग करके इस समस्या को कैसे कम करता है।
• दो कॉन्फ़िगरेशन फ़्लैग्स, --loop_iter और --optimistic_loop का परिचय देंगे, जो नियंत्रित करते हैं कि लूप्स को कैसे एक्सप्लोर किया जाए।
• इन दृष्टिकोणों की ताकतों और सीमाओं (strengths and limitations) पर चर्चा करेंगे, और यह बताएंगे कि वे अज्ञात और अनबाउंड (unknown and unbounded) लूप्स के लिए पूर्ण और सुदृढ़ (sound) प्रमाण क्यों प्रदान नहीं कर सकते हैं।

Loops को Verify करना कठिन क्यों है

यह समझने के लिए कि लूप्स को verify करना मुश्किल क्यों है, निम्नलिखित Solidity कॉन्ट्रैक्ट पर विचार करें जो collection ऐरे में जोड़े गए सबसे बड़े नंबर को ट्रैक करता है:

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract MaxInCollection {
    uint256[] collection;
    uint256 public maxInCollection = 0;

    function addToCollection(uint256 x) public {
        if (x > maxInCollection) {
            maxInCollection = x;
        }
        collection.push(x);
    }

    function returnMax() public view returns (uint256) {
        uint256 maxTmp = 0;
        for (uint256 i = 0; i < collection.length; i++) {
            if (collection[i] > maxTmp) {
                maxTmp = collection[i];
            }
        }
        return maxTmp;
    }
}

उपरोक्त कॉन्ट्रैक्ट में, फ़ंक्शन addToCollection() collection ऐरे में एक नया एलिमेंट जोड़ता है। यह हर बार जब भी नया एलिमेंट वर्तमान अधिकतम मान से अधिक हो जाता है, तो maxInCollection स्टेट वेरिएबल को भी अपडेट करता है। कॉन्ट्रैक्ट में returnMax() भी शामिल है, जो अधिकतम मान की गणना करने और उसे वापस करने के लिए ऐरे में इटरेशन करता है।

इस कॉन्ट्रैक्ट को जिस मुख्य प्रॉपर्टी (invariant) का पालन करना चाहिए, वह सरल है: maxInCollection हमेशा returnMax() द्वारा लौटाए गए मान के बराबर होना चाहिए।

आइए इसे CVL में एक invariant के रूप में व्यक्त करके औपचारिक रूप से (formally) verify करें:

Copy
methods {
    function maxInCollection() external returns(uint256) envfree;
    function returnMax() external returns(uint256) envfree;
}
invariant maxEqReturnMax()
    maxInCollection() == returnMax();

पहली नज़र में, यह दावा मान्य प्रतीत होता है और हम उम्मीद करते हैं कि Prover इसे सफलतापूर्वक verify करेगा। हालाँकि, जब हम इसे Certora Prover के माध्यम से चलाते हैं, तो वेरिफिकेशन विफल हो जाता है, जैसा कि नीचे दिखाया गया है:

वेरिफिकेशन का परिणाम देखने के बाद, आप हैरान हो सकते हैं: यदि दोनों फ़ंक्शंस तार्किक रूप से अपने रिटर्न के मामले में समान हैं, तो Prover इस समानता को स्थापित करने में विफल क्यों होता है?

इसका उत्तर उस बुनियादी अंतर में छिपा है कि EVM एक प्रोग्राम को कैसे एग्जीक्यूट करता है और Prover इसके बारे में कैसे तर्क (reason) करता है: EVM कंक्रीट इनपुट्स के साथ एक विशिष्ट पाथ (path) को एग्जीक्यूट करता है, जबकि Prover सिम्बॉलिक इनपुट्स के साथ सभी संभावित पाथ्स को एक्सप्लोर करता है।

इस अंतर को समझने के लिए, आइए पहले देखें कि कॉन्ट्रैक्ट एग्जीक्यूशन के दौरान क्या होता है, फिर इसकी तुलना इस बात से करें कि Prover प्रतीकात्मक (symbolically) रूप से कैसे तर्क करता है।

एक प्रोग्राम एक कंक्रीट पाथ का अनुसरण करता है

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

उदाहरण के लिए:

• मान लीजिए हम उस क्रम में addToCollection(7), addToCollection(5), और addToCollection(9) कॉल करते हैं।
• ऐरे collection [7, 5, 9] बन जाता है, और maxInCollection 9 में अपडेट हो जाता है।
• जब हम बाद में returnMax() कॉल करते हैं, तो फ़ंक्शन ऐरे पर तीन बार इटरेट करता है और अधिकतम मान 9 की गणना करता है।
• इसलिए maxInCollection और returnMax() दोनों समान परिणाम लौटाते हैं, जो इस बात की पुष्टि करता है कि अधिकतम मान सही ढंग से ट्रैक किया गया है।

तो कंक्रीट एग्जीक्यूशन में, प्रोग्राम दिए गए इनपुट्स और ऐरे सामग्री द्वारा परिभाषित एक एकल, निर्धारक (deterministic) पाथ का अनुसरण करता है, और दोनों फ़ंक्शन समान मान लौटाते हैं।

Prover एक साथ सभी इनपुट्स के बारे में तर्क करता है

Certora Prover एक symbolic execution engine है, जिसका अर्थ है कि यह प्रोग्राम को एक बार में एक इनपुट पर टेस्ट नहीं करता है। इसके बजाय, यह एक साथ सभी संभावित एग्जीक्यूशन्स के बारे में तर्क करता है।

इसे प्राप्त करने के लिए, Prover कंक्रीट मानों के बजाय तार्किक बाधाओं (logical constraints) पर विचार करते हुए, कदम दर कदम प्रोग्राम के व्यवहार को प्रतीकात्मक रूप से अनुकरण (simulate) करता है।

यहाँ बताया गया है कि Prover इनवेरिएंट maxEqReturnMax() को कदम-दर-कदम कैसे हल करता है:

1. Initial State Check (Base Case): पहला कदम यह जाँचना है कि कॉन्ट्रैक्ट का कंस्ट्रक्टर एग्जीक्यूट होने के तुरंत बाद इनवेरिएंट होल्ड करता है या नहीं।
   • इस स्थिति में, collection ऐरे खाली है, इसलिए collection.length 0 है।
   • maxInCollection स्टेट वेरिएबल को 0 पर इनिशियलाइज़ किया गया है।
   • फिर Prover सिम्बॉलिक रूप से returnMax() फ़ंक्शन को एग्जीक्यूट करता है। यह maxTmp को 0 पर इनिशियलाइज़ करता है और लूप का सामना करता है:

Copy
   for (uint256 i = 0; i < collection.length; i++)

चूंकि प्रारंभिक स्थिति में collection.length 0 है, इसलिए लूप बॉडी कभी नहीं चलती है, और फ़ंक्शन बस maxTmp लौटाता है, जो 0 रहता है।

नतीजतन, प्रारंभिक स्थिति में इनवेरिएंट होल्ड करता है, जिसका अर्थ है कि बेस केस (base case) सफलतापूर्वक verify हो गया है, जैसा कि नीचे दिखाया गया है:

2. The Inductive Step: प्रारंभिक स्थिति में इनवेरिएंट होल्ड करने की पुष्टि करने के बाद, Prover अगले चरण की ओर बढ़ता है — inductive step। यह चरण यह सुनिश्चित करने के बारे में है कि कॉन्ट्रैक्ट में किसी भी स्थिति परिवर्तन (state change) के बाद भी इनवेरिएंट होल्ड करना जारी रखे।

   सरल शब्दों में, Prover निम्नलिखित की जाँच करता है:

   “यदि इनवेरिएंट वर्तमान स्थिति S में होल्ड करता है, तो इसे अगली स्थिति S′ में भी होल्ड करना चाहिए जो किसी भी मान्य फ़ंक्शन कॉल का परिणाम है।”

   इस पर विचार करने के लिए, Prover वैचारिक रूप से तीन चरणों का पालन करता है:

   a. Before the Call Assumption: Prover एक मनमानी, मान्य स्थिति S पर विचार करके शुरू करता है जिसमें इनवेरिएंट पहले से ही होल्ड करता है। यह inductive hypothesis बनाता है, जो इंडक्टिव रीज़निंग में एक मानक कदम है। Prover को collection ऐरे की वास्तविक सामग्री या maxInCollection के मान को जानने की आवश्यकता नहीं है; यह मान लेता है—स्वयं प्रमाण पद्धति (proof method) के हिस्से के रूप में—कि इस स्थिति S में, प्रॉपर्टी maxInCollection() == returnMax() सत्य है।

   b. Symbolic Execution: अगला, Prover एक फ़ंक्शन कॉल को सिमुलेट करता है जो कॉन्ट्रैक्ट की स्थिति को बदल सकता है। हमारे मामले में, यह addToCollection() चुनता है। महत्वपूर्ण बात यह है कि यह addToCollection() में इनपुट के रूप में 5 या 10 जैसे किसी विशिष्ट मान को नहीं चुनता है। इसके बजाय, यह एक symbolic variable, x का उपयोग करता है, जो किसी भी संभावित uint256 मान को दर्शाता है जो फ़ंक्शन प्राप्त कर सकता है।

   फिर Prover addToCollection(x) की बॉडी को प्रतीकात्मक रूप से एग्जीक्यूट करता है:

   • यह if स्टेटमेंट देखता है: if (x > maxInCollection)। चूंकि x और maxInCollection दोनों सिम्बॉलिक हैं, इसलिए Prover ब्रांच करता है, दोनों संभावनाओं पर विचार करता है:

     Case 1: x > maxInCollection। नई स्थिति S' में maxInCollection को x में अपडेट किया जाएगा।

     Case 2: x <= maxInCollection। नई स्थिति S' में maxInCollection अपरिवर्तित रहेगा।

   दोनों ही मामलों में, यह प्रतीकात्मक रूप से collection.push(x) को एग्जीक्यूट करता है। इसका मतलब है कि स्थिति S' में collection ऐरे अब स्थिति S से collection और नया एलिमेंट x है, और collection.length में 1 की वृद्धि हुई है।

   Prover के पास अब पुरानी स्थिति S और सिम्बॉलिक इनपुट x के संदर्भ में नई स्थिति, S', का पूर्ण सिम्बॉलिक विवरण है।

   c. After Call Verification: अंतिम चरण में, Prover को अब यह साबित (prove) करना होगा कि इनवेरिएंट नई स्थिति S' में होल्ड करता है। यह पूछता है: क्या maxInCollection() (स्थिति S’ में) == returnMax() (स्थिति S’ में) है?

   इस चरण को पूरा करने के लिए, Prover इस समीकरण के दोनों पक्षों का विश्लेषण करता है:

   • LHS (maxInCollection()): यह सीधा है। Prover को maxInCollection का नया मान प्रतीकात्मक रूप से ज्ञात है (यह या तो पुराना मान है या x है)।

   • RHS (returnMax()): अगला, यह प्रतीकात्मक रूप से returnMax() फ़ंक्शन को एग्जीक्यूट करेगा। यह वह बिंदु है जहां वेरिफिकेशन चुनौतीपूर्ण हो जाता है, क्योंकि returnMax() में एक लूप होता है:

Copy
   for (uint256 i = 0; i < collection.length; i++) {...}

Loop एक समस्या क्यों है?

जब Prover returnMax() फ़ंक्शन तक पहुँचता है, तो उसे लूप को प्रतीकात्मक रूप से एग्जीक्यूट करना होता है:

Copy
for (uint256 i = 0; i < collection.length; i++) {...}

कंक्रीट एग्जीक्यूशन में, लूप एक विशिष्ट संख्या में चलता है — ऐरे में प्रत्येक एलिमेंट के लिए एक बार।

लेकिन Certora Prover के लिए, ऐरे की लंबाई सिम्बॉलिक है, इसलिए इटरेशन्स की संख्या अज्ञात है।

यह महत्वपूर्ण बिंदु है: Prover को सभी संभावित ऐरे लंबाइयों पर एक साथ विचार करना चाहिए, एक खाली ऐरे से लेकर अधिकतम रिप्रेजेंटेबल आकार तक। यह अकेले ही एक बहुत बड़ा सर्च स्पेस (search space) बना देता है।

लूप के अंदर, एक और कंडीशन (conditional) है:

Copy
if (collection[i] > maxTmp)

सिम्बॉलिक इनपुट्स के लिए, यह शर्त प्रत्येक इटरेशन में true या false हो सकती है।

इसलिए प्रत्येक इटरेशन उन सिम्बॉलिक पाथ्स की संख्या को दोगुना (doubles) कर देता है जिन पर Prover को विचार करना चाहिए।

यदि ऐरे की लंबाई n है, तो Prover को लगभग 2ⁿ पाथ्स का सामना करना पड़ता है।

उदाहरण के लिए:

• 2 एलिमेंट्स ⇒ 4 पाथ्स (2²)
• 3 एलिमेंट्स ⇒ 8 पाथ्स (2³)
• 10 एलिमेंट्स ⇒ 1024 पाथ्स (2¹⁰)
• सिम्बॉलिक (unbounded) लंबाई के लिए → यह प्रभावी रूप से प्रबंधनीय (unmanageable) है

यह घातीय वृद्धि (exponential growth) ही है जो Prover के लिए उचित समय या संसाधनों के भीतर सभी पाथ्स को एक्सप्लोर करना व्यावहारिक रूप से असंभव (practically infeasible) बना देती है।

Path Explosion Problem से निपटने के लिए Prover का दृष्टिकोण

जैसा कि पहले उल्लेख किया गया है, Certora Prover इस समस्या को संभालने के लिए bounded loop unrolling का उपयोग करता है। यह तकनीक यह सीमित करती है कि वेरिफिकेशन के दौरान लूप को कितनी बार एक्सप्लोर किया जाता है, जिसमें डिफ़ॉल्ट बाउंड एक इटरेशन पर सेट होता है। एक बार जब यह सीमा पहुँच जाती है, तो Prover आगे खोजना बंद कर देता है क्योंकि प्रत्येक अतिरिक्त इटरेशन उन सिम्बॉलिक पाथ्स की संख्या को दोगुना कर देता है जिनका उसे विश्लेषण करना है। नतीजतन, शेष पाथ्स अप्रमाणित (unproven) रह जाते हैं।

formal verification में, किसी इनवेरिएंट को साबित करने के लिए यह दिखाना आवश्यक है कि यह हर संभावित स्थिति परिवर्तन (state transition) के लिए होल्ड करता है, जिसमें किसी भी लूप के सभी इटरेशन्स शामिल हैं। यदि एक भी संभावित पाथ बिना जाँचे छूट जाता है, तो प्रमाण का inductive step अधूरा हो जाता है। यही कारण है कि Prover इनवेरिएंट maxEqReturnMax() को failed के रूप में चिह्नित करता है:

यह समझना बहुत महत्वपूर्ण है कि इटरेशन्स की अनबाउंड संख्या वाली किसी भी गणना के बारे में प्रतीकात्मक रूप से तर्क करना Prover के लिए कठिन है। और यह कठिनाई केवल आपके Solidity कोड के for/while लूप्स तक सीमित नहीं है। यही समस्या उन जगहों पर भी दिखाई देती है जहां कोई स्पष्ट लूप दिखाई नहीं देता है। आइए ऐसे हिडन लूप्स (hidden loops) के एक ठोस उदाहरण की जाँच करें: Solidity strings।

Solidity string: Hidden Loops का क्लासिक उदाहरण

यह समझने के लिए कि स्ट्रिंग्स “unwinding condition in a loop” त्रुटियों (errors) का कारण कैसे बनती हैं, नीचे दिए गए स्मार्ट कॉन्ट्रैक्ट पर विचार करें जो स्टेट वेरिएबल txt में एक स्ट्रिंग संग्रहीत करता है और किसी को भी इसे setTxt() के माध्यम से अपडेट करने देता है:

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Example {
    string public txt;

    function setTxt(string memory _txt) external {
        txt = _txt;
    }
}

अब, निम्नलिखित स्पेसिफिकेशन (specification) पर विचार करें जो यह साबित करने का प्रयास करता है कि संग्रहीत स्ट्रिंग हमेशा इनपुट के बराबर होती है:

Copy
methods{
    function setTxt(string) external envfree;
    function txt() external returns(string) envfree;
}

rule storedStringShouldEqualToInput() {

    string _txt;

    //call
    setTxt(_txt);

    //assertions
    assert _txt == txt();

}

यदि आप इस स्पेसिफिकेशन के साथ Prover चलाते हैं, तो रूल विफल हो जाता है:

और आपको परिचित “Unwinding condition in a loop” त्रुटि दिखाई देगी, ठीक वैसे ही जैसे एक स्पष्ट लूप वाले पिछले उदाहरण में।

आप सोच रहे होंगे कि यह त्रुटि तब क्यों दिखाई देती है जब कोड में कोई स्पष्ट (explicit) लूप नहीं होता है।

इसका कारण सरल है: एक hidden loop (हिडन लूप)।

Solidity में, एक स्ट्रिंग एक एकल मान नहीं है बल्कि बाइट्स (bytes) का एक गतिशील ऐरे (dynamic array) है। हालाँकि, EVM के 256-बिट वर्ड आर्किटेक्चर के कारण, जब आप डायनामिक ऐरेज़ के साथ काम करते हैं, तो कंपाइलर और EVM उन्हें एक बार में 32-बाइट चंक्स (chunks) कॉपी करके संभालते हैं।

यह दोहराई जाने वाली, वर्ड-आधारित कॉपी करने की प्रक्रिया ही वह hidden loop है जिसका सामना Prover संकलित (compiled) बाइटकोड में करता है।

हमारे स्पेसिफिकेशन में, स्ट्रिंग को हैंडल करते समय चार हिडन लूप्स ट्रिगर होते हैं:

1. calldata से memory में कॉपी करना (The Entrance)

   • क्या होता है: जब आप setTxt(_txt) कॉल करते हैं, तो इनपुट स्ट्रिंग calldata नामक एक अस्थायी, केवल-पठनीय (read-only) होल्डिंग एरिया में आती है। फ़ंक्शन के अंदर उस स्ट्रिंग का वास्तव में उपयोग या प्रोसेस करने के लिए, EVM को पहले इसे फ़ंक्शन के वर्कस्पेस में ले जाना चाहिए, जिसे memory कहा जाता है।
   • लूप: यह ट्रांसफर एक बार में 32 बाइट्स में किया जाता है। EVM तब तक लूप करता है जब तक कि पूरी स्ट्रिंग calldata से memory में स्थानांतरित नहीं हो जाती।

2. memory से storage में कॉपी करना (The Assignment)

   • क्या होता है: असाइनमेंट txt = _txt; स्ट्रिंग को स्थायी रूप से सेव करता है। यह डेटा को अस्थायी memory वर्कस्पेस से कॉन्ट्रैक्ट के storage में ले जाता है, जो वह स्थान है जहाँ आपके कॉन्ट्रैक्ट का स्टेट ब्लॉकचेन पर रहता है।
   • लूप: चूँकि यह एक स्थायी राइट (write) है, इसलिए EVM स्ट्रिंग को वर्ड-बाय-वर्ड (एक बार में 32 बाइट्स) कॉन्ट्रैक्ट के निर्दिष्ट स्टोरेज स्लॉट्स में कॉपी करने के लिए एक लूप चलाता है। यह वेरिफिकेशन की विफलता का मुख्य बिंदु है।

3. storage से वापस memory में कॉपी करना (The Read)

   • क्या होता है: जब आप पब्लिक गेटर (getter) txt() कॉल करते हैं, तो कॉन्ट्रैक्ट को संग्रहीत स्ट्रिंग डेटा को फेच (fetch) करना होता है। यह स्ट्रिंग को उसके स्थायी storage स्थान से वापस अस्थायी memory में लोड करता है ताकि इसे लौटाया जा सके।
   • लूप: एक और आंतरिक लूप चलता है, जो स्ट्रिंग के 32-बाइट वर्ड्स को स्टोरेज से एक-एक करके पढ़ता है।

4. स्ट्रिंग्स की तुलना करना (The Assertion)

   • क्या होता है: आपके एसरशन (assertion), assert _txt == txt(); में, Prover को यह जाँचना होगा कि क्या दोनों सिम्बॉलिक स्ट्रिंग्स बराबर हैं।
   • लूप: दो डायनामिक ऐरेज़ के लिए समानता जाँचने का एकमात्र तरीका उनकी वर्ड-बाय-वर्ड शुरुआत से अंत तक तुलना करना है, जो एक अंतिम हिडन लूप की परिभाषा है।

कंक्रीट एग्जीक्यूशन के लिए (एक विशिष्ट इनपुट के साथ कोड चलाना, जैसे कि स्ट्रिंग "Hello"), यह हिडन लूप सरल है। स्ट्रिंग की लंबाई एक ज्ञात, निश्चित संख्या है, इसलिए लूप एक निश्चित संख्या में चलता है। सब कुछ पूर्वानुमानित (predictable) है।

हालाँकि, Certora Prover जैसे symbolic execution engine के लिए, इनपुट _txt एक निश्चित स्ट्रिंग नहीं है। यह एक सिम्बॉलिक मान है, जिसका अर्थ है कि यह एक साथ हर संभावित स्ट्रिंग का प्रतिनिधित्व करता है—एक खाली स्ट्रिंग से लेकर अधिकतम आकार वाले स्ट्रिंग तक।

Prover को अब एग्जीक्यूशन्स के एक अनबाउंड परिवार (unbounded family) के बारे में तर्क करने के लिए मजबूर होना पड़ता है। उसे यह जाँचना होगा कि क्या प्रॉपर्टी होल्ड करती है, चाहे स्ट्रिंग की लंबाई कुछ भी हो या उसमें कौन से बाइट्स हों। इससे दो बड़ी समस्याएं उत्पन्न होती हैं:

समस्या 1: Unknown Loop Size (The Unbounded Search)

पहली चुनौती इसलिए उत्पन्न होती है क्योंकि स्ट्रिंग की लंबाई सिम्बॉलिक (अज्ञात) है। इसका मतलब है कि लूप काउंटर जो 32-बाइट कॉपी करने की प्रक्रिया को नियंत्रित करता है, वह भी सिम्बॉलिक है।

• एक विशिष्ट स्ट्रिंग के लिए, लूप एक निर्धारित संख्या में चलता है (उदाहरण के लिए, ठीक 3 बार)।
• Prover के लिए, लूप कितनी भी बार चल सकता है (उदाहरण के लिए, 0, 1, 10, या 100 बार)।

इसलिए Prover को न केवल एक एग्जीक्यूशन पाथ, बल्कि पाथ्स के पूरे परिवार (family) की जाँच करनी चाहिए, जो उस हर संभावित लंबाई से संबंधित है जो स्ट्रिंग ले सकती है। यद्यपि यह अकेला ही एक बहुत बड़ा, तकनीकी रूप से अनबाउंड सर्च स्पेस बनाता है, यह समस्या दूसरी समस्या: लूप के अंदर ब्रांचिंग (branching inside the loop) से घातीय रूप से और भी बदतर हो जाती है।

समस्या 2: Exponential Branching (The Doubling Effect)

पाथ्स की कुल संख्या में विस्फोट (explode) होता है क्योंकि हिडन लूप अक्सर कंडीशनल चेक्स (जैसे वर्तमान 32-बाइट वर्ड की तुलना करना) से टकराता है। चूँकि Prover को सिम्बॉलिक स्ट्रिंग की सामग्री नहीं पता है, इसलिए वह चेक के परिणाम का निर्धारण नहीं कर सकता है।

शुद्धता (correctness) की गारंटी के लिए, Prover को एक साथ दोनों संभावनाओं का पता लगाना चाहिए। यह एग्जीक्यूशन पाथ को विभाजित होने (split) के लिए मजबूर करता है, जिसके लिए Prover को कंडीशन के true होने और कंडीशन के false होने के परिणामों का पता लगाने की आवश्यकता होती है। यह एक्सप्लोरेशन लूप के हर एक इटरेशन के साथ एग्जीक्यूशन पाथ्स की संख्या को प्रभावी ढंग से दोगुना (doubles) कर देता है।

उदाहरण के लिए:

• यदि हिडन लूप केवल 3 बार चलता है, और प्रत्येक इटरेशन में एक कंडीशनल चेक है, तो Prover को 2 x 2 x 2 = 8 अलग-अलग पाथ्स का विश्लेषण करना होगा।
• यदि सिम्बॉलिक स्ट्रिंग इतनी लंबी है कि 10 लूप इटरेशन्स को ट्रिगर कर सके, तो Prover को 2^10 = 1,024 पाथ्स का विश्लेषण करना होगा।

अनबाउंड लंबाई (unbounded length) और एक्सपोनेंशियल ब्रांचिंग (exponential branching) का यह संयोजन ही वह चीज़ है जो path explosion problem पैदा करता है, जो वेरिफिकेशन प्रक्रिया को जल्दी ही कम्प्यूटेशनल रूप से असंभव बना देता है।

Prover संभावित एग्जीक्यूशन पाथ्स की विशाल और तेजी से बढ़ती संख्या से अभिभूत (overwhelmed) हो जाता है और bounded loop unrolling का उपयोग करके एक निश्चित संख्या में इटरेशन्स के बाद लूप की खोज बंद करने के लिए मजबूर हो जाता है।

क्योंकि Prover सभी संभावित पाथ्स की जाँच नहीं कर सकता (यानी, यह सभी सिम्बॉलिक लंबाइयों के लिए लूप को पूरी तरह से अनरोल नहीं कर सकता), प्रमाण को अधूरा (incomplete) माना जाता है। इसलिए, यह साबित नहीं कर सकता कि प्रॉपर्टी सभी संभावित स्ट्रिंग्स के लिए होल्ड करती है, यही कारण है कि रूल storedStringShouldEqualToInput() सफलतापूर्वक verify होने में विफल रहता है।

“कारण” पर पुनर्विचार (Revisiting the “Cause”)

हम देख सकते हैं कि Prover दोनों रूल्स को verify करने में विफल रहा: maxEqReturnMax() और storedStringShouldEqualToInput(), इसलिए नहीं कि प्रॉपर्टीज़ झूठी (false) हैं, बल्कि इसलिए कि Prover उनके बारे में तर्क पूरा नहीं कर सकता है।

• maxEqReturnMax() के मामले में, returnMax() के अंदर का लूप सैद्धांतिक रूप से, 2²⁵⁶−1 बार तक चल सकता है — ऐरे में हर संभावित एलिमेंट के लिए एक बार। यदि हम ऐरे की लंबाई को n से दर्शाते हैं, तो Prover को n के हर संभावित मान के लिए लूप को अनरोल करने का प्रयास करना चाहिए, जो कम्प्यूटेशनल रूप से असंभव है।
• storedStringShouldEqualToInput() के मामले में, txt = _txt के अंदर हिडन लूप स्ट्रिंग में प्रत्येक 32 बाइट्स के लिए एक बार चल सकता है। चूँकि इनपुट की लंबाई सिम्बॉलिक है, इसलिए Prover को सभी संभावित स्ट्रिंग लंबाइयों पर विचार करना चाहिए, जो फिर से अनबाउंड एक्सप्लोरेशन की ओर ले जाता है।

दोनों मामलों में, मूल कारण एक ही है: Prover प्रतीकात्मक (symbolically) रूप से लूप इटरेशन्स की एक अनबाउंड संख्या का पता नहीं लगा सकता है।

यह हमारे सामने एक प्रश्न छोड़ देता है: इन मामलों को संभालने के लिए हमारे पास क्या विकल्प हैं?

“समाधान”: Configuration Flags

Certora Prover लूप्स से निपटने में मदद करने के लिए दो कॉन्फ़िगरेशन विकल्प प्रदान करता है। हालाँकि ये शुद्धता (correctness) का पूर्ण प्रमाण (complete proofs) प्रदान नहीं करते हैं, लेकिन ये Prover के व्यवहार को नियंत्रित करने के लिए उपयोगी उपकरण हैं।

1. loop_iter के साथ Unrolling Bound बढ़ाना

पहला और सबसे सीधा विकल्प --loop_iter फ़्लैग का उपयोग करके Prover को लूप को अधिक बार अनरोल करने के लिए कहना है। यह या तो टर्मिनल से या कॉन्फ़िगरेशन फ़ाइल के माध्यम से किया जा सकता है।

टर्मिनल से:

Copy
certoraRun confs/<your-config-file>.conf --loop_iter <N>

या एक कॉन्फ़िगरेशन फ़ाइल के अंदर:

Copy
{
    "files": [
        "contracts/<YourContract>.sol:<ContractName>"
    ],
    "verify": "<ContractName>:specs/<your-spec-file>.spec",
    "loop_iter": "<N>"
}

ऊपर दिए गए टर्मिनल कमांड और कॉन्फ़िगरेशन फ़ाइल उदाहरणों में, <N> लूप इटरेशन्स की अधिकतम संख्या निर्दिष्ट करता है जिसे Prover रुकने से पहले एक्सप्लोर करेगा**।**

हमारे रूल में loop_iter फ़्लैग का उपयोग करना

यह समझने के लिए कि --loop_iter फ़्लैग व्यवहार में कैसे काम करता है, आइए इसे अपने स्ट्रिंग उदाहरण पर लागू करें और निम्नलिखित कमांड के साथ Prover चलाएँ:

Copy
certoraRun confs/example.conf --loop_iter 3

जब हम उपरोक्त कमांड के साथ Prover चलाते हैं, तो व्यवहार में ऐसा होने वाला है:

• Prover अब हिडन लूप के 3 इटरेशन्स तक अनरोल करेगा (txt = _txt के अंदर बाइट-कॉपी करने वाला लूप)।
• चूँकि प्रत्येक इटरेशन एक 32-बाइट वर्ड की प्रतिलिपि बनाता है, इसका मतलब है कि Prover 96 बाइट्स (3 × 32 = 96) तक की लंबाई वाले स्ट्रिंग्स के लिए प्रॉपर्टी को सफलतापूर्वक verify कर सकता है।
• हालाँकि, 96 बाइट्स से लंबी स्ट्रिंग्स के लिए, Prover अपनी अनरोलिंग बाउंड (unrolling bound) तक पहुँच जाता है। उस बिंदु पर, वे पाथ्स अप्रमाणित (unproven) रह जाते हैं।
• परिणामस्वरूप, रूल storedStringShouldEqualToInput() अभी भी सामान्य मामले में विफल रहेगा क्योंकि Prover सभी स्ट्रिंग लंबाइयों के लिए शुद्धता साबित नहीं कर सकता है।

परिणाम वही रहेगा चाहे आप बाउंड को कितना भी बढ़ा दें: कोई भी परिमित (finite) --loop_iter प्रॉपर्टी को केवल 32-बाइट वर्ड्स की उस संख्या तक के स्ट्रिंग्स के लिए साबित करता है। बड़ी स्ट्रिंग्स अप्रमाणित रहती हैं, और बाउंड बढ़ाने से Prover तेज़ी से धीमा हो जाता है।

2. optimistic_loop के साथ बाउंड के पार छोड़ना (Skipping Beyond the Bound)

दूसरा विकल्प बहुत अलग दृष्टिकोण अपनाता है। बाउंड को बढ़ाने के बजाय, Prover को यह मान लेने (assume) के लिए कहा जा सकता है कि बाउंड के बाहर सब कुछ ठीक काम करता है। --optimistic_loop यही करता है।

टर्मिनल से:

Copy
certoraRun confs/<your-config-file>.conf --optimistic_loop

या एक कॉन्फ़िगरेशन फ़ाइल के अंदर:

Copy
{
    "files": [
        "contracts/<YourContract>.sol:<ContractName>"
    ],
    "verify": "<ContractName>:specs/<your-spec-file>.spec",
    "optimistic_loop": true
}

आमतौर पर, जब Prover अपनी लूप बाउंड को हिट करता है और देखता है कि लूप जारी रह सकता है, तो वह उस पाथ को अप्रमाणित (unproven) के रूप में चिह्नित करता है।

--optimistic_loop के साथ, Prover रणनीति बदलता है:

• बाउंड के भीतर (within the bound) इटरेशन्स के लिए, यह सामान्य रूप से व्यवहार करता है और हर मामले की जाँच करता है।
• बाउंड के बाहर (beyond the bound) इटरेशन्स के लिए, यह मान लेता है (assumes) कि उन पाथ्स को वास्तव में एक्सप्लोर किए बिना प्रॉपर्टी होल्ड करना जारी रखेगी।

हमारे रूल में optimistic_loop फ़्लैग का उपयोग करना

यह समझने के लिए कि --optimistic_loop फ़्लैग व्यवहार में कैसे काम करता है, आइए इसे अपने स्ट्रिंग उदाहरण पर लागू करें और निम्नलिखित कमांड के साथ Prover चलाएँ:

Copy
certoraRun confs/example.conf --optimistic_loop

जब हम उपरोक्त कमांड के साथ Prover चलाते हैं, तो व्यवहार में ऐसा होने वाला है:

• Prover अभी भी इटरेशन्स की एक छोटी संख्या (इसकी डिफ़ॉल्ट अनरोलिंग बाउंड) के लिए लूप का एक्सप्लोर करता है।
• एक बार जब यह उस बाउंड पर पहुँच जाता है, तो एक “unwinding condition in a loop” त्रुटि रिपोर्ट करने के बजाय, यह मान लेता है कि प्रॉपर्टी शेष सभी मामलों के लिए होल्ड करना जारी रखती है।
• परिणामस्वरूप, रूल storedStringShouldEqualToInput() अब वेरिफिकेशन पास कर लेता है, भले ही लंबी स्ट्रिंग लंबाइयों की कभी पूरी तरह से जाँच नहीं की गई हो।

इस दृष्टिकोण को “आशावादी (optimistic)” कहा जाता है क्योंकि Prover अनिवार्य रूप से यह उम्मीद करता है कि उसने पहले कुछ इटरेशन्स में जो देखा, वह भविष्य के सभी इटरेशन्स के लिए सत्य बना रहेगा।
हम देख सकते हैं कि --loop_iter के साथ, Prover केवल बाउंड तक (हमारे उदाहरण में 3 इटरेशन्स) एक्सप्लोर करता है। इससे लंबा कुछ भी अप्रमाणित रहता है, इसलिए वेरिफिकेशन विफल हो जाता है। हालाँकि, --optimistic_loop के साथ, Prover एक शॉर्टकट लेता है: यह मानता है कि यदि प्रॉपर्टी एक्सप्लोर किए गए बाउंड के भीतर होल्ड करती है, तो वह इसके बाहर भी होल्ड करती है। यह अनवाइंडिंग विफलता को दूर करता है और रूल को पास कर देता है।

हालाँकि ये फ़्लैग्स डिबगिंग और वेरिफिकेशन के प्रबंधन के लिए उपयोगी हैं, लेकिन इनमें से कोई भी अज्ञात और अनबाउंड लूप्स के लिए पूर्ण, सुदृढ़ (sound) प्रमाण प्रदान नहीं करता है।

• --loop_iter अपूर्ण (incomplete) है।
• --optimistic_loop अनुचित/अविश्वसनीय (unsound) है (यह धारणाएं बनाता है)।

निष्कर्ष (Wrapping Up)

इस अध्याय में, हमने देखा कि स्पष्ट (explicit) और हिडन (hidden) दोनों तरह के लूप्स formal verification में इतनी बड़ी चुनौती क्यों पैदा करते हैं। दोनों ही स्थितियों में, Prover प्रतीकात्मक रूप से इटरेशन्स की अज्ञात और अनबाउंड संख्या का एक्सप्लोर नहीं कर सकता है। आगे बढ़ने के लिए, यह दो कॉन्फ़िगरेशन फ़्लैग्स पर निर्भर करता है: --loop_iter और --optimistic_loop

--loop_iter फ़्लैग एक्सप्लोर किए गए इटरेशन्स की संख्या को बढ़ाता है, लेकिन यह केवल छोटे इनपुट्स के लिए शुद्धता साबित करता है और इसलिए अधूरा (incomplete) रहता है। --optimistic_loop फ़्लैग Prover को शुद्धता मानकर बाउंड से आगे जाने (skip) की अनुमति देता है, लेकिन वह धारणा गलत हो सकती है, जिससे यह unsound हो जाता है।

ये वर्कअराउंड (workarounds) डिबगिंग, त्वरित जाँच, या सतही (shallow) बग्स को पकड़ने में सहायक होते हैं। हालाँकि, जब अनबाउंड लूप्स से निपटना हो तो वे एक पूर्ण प्रमाण प्रदान नहीं कर सकते हैं।

यह लेख formal verification using the Certora Prover पर एक श्रृंखला का हिस्सा है।