पिछले अध्याय में, हमने सीखा कि एक specification, CVL में लिखा गया कोड का एक हिस्सा है जो किसी स्मार्ट कॉन्ट्रैक्ट (smart contract) के अपेक्षित व्यवहार का वर्णन करता है। एक specification में मुख्य रूप से शामिल होते हैं:

• Rules
• Methods Block

इन नियमों (rules) और Methods Block के मुख्य भाग CVL स्टेटमेंट्स (statements) से बने होते हैं।

इस अध्याय में, हम CVL स्टेटमेंट्स के बारे में सीखेंगे।

CVL Statements का परिचय

Certora’s official documentation के अनुसार, “Statements उन चरणों (steps) का वर्णन करते हैं जिन्हें किसी रूल (rule) का मूल्यांकन करते समय Prover द्वारा सिमुलेट (simulate) किया जाता है।” दूसरे शब्दों में, स्टेटमेंट्स उन शर्तों और कार्यों को परिभाषित करते हैं जो यह निर्देशित करते हैं कि Certora Prover किसी रूल के आधार पर स्मार्ट कॉन्ट्रैक्ट का परीक्षण कैसे करता है।

नियमों (rules) को लिखने के लिए CVL कई तरह के स्टेटमेंट्स प्रदान करता है, लेकिन अभी के लिए, हम निम्नलिखित पर ध्यान केंद्रित करेंगे:

• require – इसका उपयोग उस शर्त को निर्दिष्ट करने के लिए किया जाता है जिसे रूल चलाने से पहले पूरा होना चाहिए।
• assert – इसका उपयोग उस शर्त को निर्दिष्ट करने के लिए किया जाता है जिसे किसी रूल को सत्यापित (verified) माने जाने के लिए सभी निष्पादन पथों (execution paths) में सत्य होना चाहिए।
• satisfy – इसका उपयोग यह सुनिश्चित करने के लिए किया जाता है कि कम से कम एक वैध निष्पादन पथ (valid execution path) मौजूद है।

“Execution Path” का क्या अर्थ है?

किसी स्मार्ट कॉन्ट्रैक्ट को सत्यापित (verify) करते समय, Prover विभिन्न संभावित अवस्थाओं (states) और ट्रांसिशन्स (transitions) की पड़ताल करता है ताकि यह जाँचा जा सके कि सभी परिदृश्यों (scenarios) में नियम लागू होता है या नहीं। एक execution path का तात्पर्य फ़ंक्शन कॉल और स्टेट परिवर्तनों के एक विशिष्ट अनुक्रम से है जिससे कॉन्ट्रैक्ट सत्यापन के दौरान गुजरता है।

assert के उपयोग को समझना

CVL में assert स्टेटमेंट का उपयोग उस शर्त को सत्यापित करने के लिए किया जाता है जिसका कॉन्ट्रैक्ट के निष्पादन (execution) के दौरान सत्य होना अनिवार्य है। प्रत्येक रूल का अंत या तो assert या satisfy स्टेटमेंट के साथ होना चाहिए।

यदि कोई रूल assert या satisfy स्टेटमेंट के साथ समाप्त नहीं होता है, तो Prover यह निर्धारित नहीं कर सकता कि किस शर्त की जाँच की जानी चाहिए, जिससे एरर (error) उत्पन्न होता है। उदाहरण के लिए, पिछले अध्याय के नीचे दिए गए specification को चलाने पर विचार करें, जिसमें assert स्टेटमेंट्स को कमेंट आउट (commented out) किया गया है:

Copy
methods {
    function count() external returns(uint256) envfree;
    function increment() external envfree;
    function decrement() external envfree;
}


rule checkIncrementCall() {

    //Precall Requirement
    require count() == 0;

    // Call OR Action
    increment();


    // Post-call Expectation
    //assert count() == 1;

}
rule checkCounter() {

    //Retrieval of Pre-call value
    uint256 precallCountValue = count();

    // Call
    increment();
    decrement();

    //Retrieval of Post-call value
    uint256  postcallCountValue = count();

    //Post-call Expectation
    //assert postcallCountValue == precallCountValue;
}

चूंकि उपरोक्त दोनों में से किसी भी रूल के अंत में assert स्टेटमेंट शामिल नहीं है, इसलिए Prover यह तय नहीं कर सकता कि किस प्रॉपर्टी (property) को सत्यापित करना है। इसका परिणाम इस एरर के रूप में होता है “last statement of the rule …… is not an assert or satisfy command (but must be),” जैसा कि नीचे दिखाया गया है।

assert स्टेटमेंट में एक एक्सप्रेशन (expression) के रूप में कॉन्ट्रैक्ट की अपेक्षित स्टेट (expected state) होती है, साथ ही एक्सप्रेशन का वर्णन करने वाली एक वैकल्पिक मैसेज स्ट्रिंग (optional message string) भी होती है, जैसा कि नीचे दिखाया गया है:

Copy
assert Expression, "An Optional Message String";
//OR
assert Expression;

सत्यापन (verification) के दौरान, एक रूल तभी पास होता है जब सभी execution paths उसके assert स्टेटमेंट्स में व्यक्त की गई शर्तों को पूरा करते हैं। हालाँकि, यदि किसी भी execution path में कोई भी assert स्टेटमेंट false का मूल्यांकन करता है, तो रूल का उल्लंघन (violated) माना जाता है।

Counter Contract के लिए वैलिडेशन बेंचमार्क परिभाषित करना

assert स्टेटमेंट कैसे काम करता है, इसे बेहतर ढंग से समझने के लिए, आइए अपने पिछले Counter उदाहरण पर फिर से विचार करें और इसकी कार्यप्रणाली का अधिक विस्तार से पता लगाएं।

Copy
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {

    uint256 public count;
    
    function increment() external {
        count++;
    }
}

ऊपर दिए गए कॉन्ट्रैक्ट को सही ढंग से काम कर रहा माना जा सकता है यदि यह टेस्टिंग के दौरान निम्नलिखित शर्तों को पूरा करता है:

1. कॉन्ट्रैक्ट डिप्लॉय (deploy) होने के बाद, count वेरिएबल को सही ढंग से इनिशियलाइज़ (initialize) होना चाहिए।
2. जब increment() को कॉल किया जाता है, तो count का मान 1 से बढ़ना चाहिए।

अपेक्षाओं को Assertion Checks में बदलना

अब, मान लीजिए कि हम Counter कॉन्ट्रैक्ट के लिए अपनी अपेक्षाओं को औपचारिक रूप से (formally) सत्यापित करना चाहते हैं। ऐसा करने के लिए, हम checkCountValidity() नामक एक रूल परिभाषित करते हैं, जो यह सुनिश्चित करता है कि count वेरिएबल शून्य (zero) से शुरू होता है और प्रत्येक फ़ंक्शन कॉल के साथ सही ढंग से बढ़ता (increment) है।

Copy
rule checkCountValidity(.......)

यहाँ बताया गया है कि यह रूल कैसे काम करता है, चरण दर चरण (step by step):

1. Initial State कैप्चर करना: हम पहले count() गेटर (getter) का उपयोग करके count का वर्तमान मान प्राप्त करते हैं और इसे PrecallCountValue नामक एक वेरिएबल में स्टोर करते हैं। यह हमें कोई भी संशोधन (modification) होने से पहले एक संदर्भ बिंदु (reference point) देता है।

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();
}

2. इंक्रीमेंट करना: फिर हम काउंटर को बढ़ाने के लिए increment() फ़ंक्शन को तीन बार कॉल करते हैं।

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();
}

3. अपडेटेड स्टेट प्राप्त करना: increment() कॉल्स को निष्पादित करने के बाद, हम count का नया मान प्राप्त करते हैं और इसे PostcallCountValue में स्टोर करते हैं। यह हमें फ़ंक्शन निष्पादन से पहले और बाद की स्टेट की तुलना करने की अनुमति देता है।

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

}

4. प्रारंभिक स्टेट को वैलिडेट करना: शुद्धता (correctness) सुनिश्चित करने के लिए, हम यह सत्यापित करने के लिए assert स्टेटमेंट का उपयोग करते हैं कि count प्रारंभ में 0 था—यह पुष्टि करते हुए कि कॉन्ट्रैक्ट एक ज्ञात, अपेक्षित स्टेट (expected state) से शुरू होता है।

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Assertions 
    assert PrecallCountValue == 0;
}

5. इंक्रीमेंट व्यवहार को सत्यापित करना: अंत में, हम यह assert करते हैं कि count ठीक 3 से बढ़ गया है, यह पुष्टि करते हुए कि increment() की प्रत्येक कॉल ने सफलतापूर्वक मान में 1 जोड़ा है।

Copy
rule checkCountValidity() {
    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Assertions
    assert PrecallCountValue == 0;
    assert PostcallCountValue == PrecallCountValue + 3;
}

हम देख सकते हैं कि कॉन्ट्रैक्ट के व्यवहार के बारे में अपनी अपेक्षाओं को लागू करने के लिए हमने assert स्टेटमेंट्स का उपयोग कैसे किया।

अपेक्षित परिणाम (Expected Result) क्या है?

पहली नज़र में, आप उम्मीद कर सकते हैं कि checkCountValidity सत्यापन पास कर लेगा क्योंकि:

1. डिफ़ॉल्ट इनिशियलाइज़ेशन (Default Initialization): Counter कॉन्ट्रैक्ट स्पष्ट रूप से count स्टेट वेरिएबल को इनिशियलाइज़ नहीं करता है, इसलिए Solidity स्वचालित रूप से इसे 0 पर सेट कर देता है। परिणामस्वरूप, जब रूल count() का उपयोग करके प्रारंभिक मान प्राप्त करता है, तो इसे 0 वापस करना चाहिए, जिससे किसी भी execution path के लिए assertion PrecallCountValue == 0 मान्य हो जाता है।
2. इंक्रीमेंट व्यवहार (Increment Behavior): increment() की प्रत्येक कॉल count वेरिएबल को 1 से बढ़ा देती है। चूंकि रूल increment() को तीन बार कॉल करता है, count का अपेक्षित अंतिम मान PrecallCountValue + 3 होना चाहिए। इसलिए, यह उम्मीद की जाती है कि assertion PostcallCountValue == PrecallCountValue + 3 किसी भी execution path के लिए सत्य होगा।

Verification चलाना

हालाँकि, जब आप वेरिफिकेशन प्रक्रिया चलाते हैं, तो आपको एक अप्रत्याशित परिणाम का सामना करना पड़ेगा जैसा कि नीचे दिखाया गया है।

ऊपर दिए गए परिणाम में, हम स्पष्ट रूप से देख सकते हैं कि Prover checkCountValidity() रूल को सत्यापित करने में विफल रहा। यह बताता है कि निम्नलिखित में से कम से कम एक शर्त का मूल्यांकन false के रूप में हुआ, जिसके परिणामस्वरूप रूल का उल्लंघन (violation) हुआ:

• assert PrecallCountValue == 0
• assert PostcallCountValue == PrecallCountValue + 3

उल्लंघन (violation) के मामले में, Prover उल्लंघन को रेखांकित करने वाली एक विस्तृत रिपोर्ट जनरेट करता है, जिसमें इस बात की जानकारी होती है कि कौन सा assertion विफल हुआ, संबंधित वेरिएबल्स के मान क्या थे, और विफलता (failure) तक ले जाने वाले निष्पादन चरण (execution steps) क्या थे।

Counterexample के माध्यम से Verification Failures की व्याख्या करना

उल्लंघन को समझने के लिए, Certora Prover counterexamples प्रदान करता है। सरल शब्दों में, एक counterexample एक विशिष्ट execution path है जहाँ किसी रूल का सत्यापन विफल हो जाता है।

हमारे उल्लिखित रूल के counterexample को देखने के लिए, नीचे दिए गए दृश्य के समान दृश्य प्राप्त करने के लिए रिपोर्ट पेज पर उल्लिखित रूल (checkCountValidity) के नाम पर क्लिक करें।

एक बार जब आप ऐसा करते हैं, तो यह रूल के पैरामीटर और वेरिएबल के मान (दाईं ओर), और एक कॉल ट्रेस (call trace) (बीच में) दिखाता है, जैसा कि नीचे दिखाया गया है।

किसी उल्लंघन (violation) की जाँच करते समय, call trace अत्यंत सहायक होता है क्योंकि यह रूल के निष्पादन की शुरुआत में स्टेट वेरिएबल्स के बारे में विस्तृत जानकारी प्रदान करता है और पूरे निष्पादन के दौरान उन वेरिएबल्स में होने वाले अपडेट को भी ट्रैक करता है, जैसा कि नीचे दिखाया गया है:

Certora Prover द्वारा प्रदान किए गए counterexample में, हम स्पष्ट रूप से देख सकते हैं कि हमारा रूल वेरिफिकेशन में विफल रहा क्योंकि रूल को यह उम्मीद थी कि count 0 से शुरू होगा, लेकिन इसके बजाय यह 10 से शुरू हुआ, जिसके कारण assert PrecallCountValue == 0 विफल हो गया।

यह एक महत्वपूर्ण प्रश्न खड़ा करता है: count को अपेक्षित डिफ़ॉल्ट 0 के बजाय 10 पर क्यों सेट किया गया है? इसे समझने के लिए, हमें यह समझना होगा कि Solidity और CVL अनइनिशियलाइज़्ड (uninitialized) वेरिएबल्स को अलग-अलग तरीके से कैसे हैंडल करते हैं।

count का मान 0 के बजाय 10 पर सेट क्यों है?

जैसा कि हम जानते हैं, यदि कोई Solidity स्मार्ट कॉन्ट्रैक्ट किसी स्टेट वेरिएबल को स्पष्ट रूप से इनिशियलाइज़ नहीं करता है, तो उसे उसके प्रकार (type) के आधार पर स्वचालित रूप से एक डिफ़ॉल्ट मान असाइन किया जाता है। उदाहरण के लिए:

• uint256 के लिए, डिफ़ॉल्ट मान 0 है।
• bool के लिए, डिफ़ॉल्ट मान false है।
• address के लिए, डिफ़ॉल्ट मान शून्य एड्रेस (zero address) है।

Solidity के विपरीत, CVL स्वचालित रूप से वेरिएबल्स को डिफ़ॉल्ट मान असाइन नहीं करता है। इसके बजाय, CVL में अनइनिशियलाइज़्ड वेरिएबल्स अप्रतिबंधित (unconstrained) रहते हैं, जिसका अर्थ है कि वे सत्यापन (verification) के दौरान अपनी परिभाषित सीमा (defined range) के भीतर कोई भी संभव मान ले सकते हैं। यह एक महत्वपूर्ण अवधारणा से जुड़ा है: CVL रूल्स कॉन्ट्रैक्ट की विशिष्ट प्रारंभिक डिप्लॉयमेंट स्टेट (जैसा कि Solidity निष्पादन अक्सर मान लेता है) से वेरिफिकेशन शुरू नहीं करते हैं, बल्कि एक arbitrary (मनमानी) स्टेट से शुरू करते हैं। यह एक प्रमुख अंतर है और औपचारिक सत्यापन (formal verification) का एक मूलभूत पहलू है।

इस व्यवहार के कारण, वेरिफिकेशन के दौरान count का प्रारंभिक मान 10 पर सेट हो गया था, जिससे रूल विफल हो गया क्योंकि हमने count के 0 से शुरू होने की उम्मीद की थी।

require के उपयोग को समझना

जैसा कि ऊपर देखा गया है, Prover वेरिफिकेशन प्रक्रिया के दौरान स्टेट वेरिएबल्स को arbitrary मान असाइन करता है, जिससे अप्रत्याशित प्रारंभिक मान आ सकते हैं और यदि रूल Solidity के डिफ़ॉल्ट मानों को मान कर चलता है तो assertions विफल हो सकते हैं।

ऐसे मामलों में, हम अपने वेरिफिकेशन सेटअप में स्टेट वेरिएबल्स पर स्पष्ट रूप से बाधाएं (constraints) परिभाषित करना चाह सकते हैं, यह सुनिश्चित करते हुए कि रूल को निष्पादित करने से पहले वे अपेक्षित मानों के साथ शुरू हों। यहीं पर CVL में require स्टेटमेंट उपयोगी हो जाता है।

CVL में require स्टेटमेंट का उपयोग किसी रूल के लिए पूर्व-शर्तों (preconditions) को निर्दिष्ट करने के लिए किया जाता है, यह सुनिश्चित करते हुए कि रूल को मान्य (valid) मानने से पहले कुछ शर्तें पूरी होती हैं।

जब किसी रूल में require स्टेटमेंट शामिल किया जाता है, तो यह एक फ़िल्टर के रूप में कार्य करता है जो Prover को किसी भी ऐसे execution path को अनदेखा करने के लिए कहता है जहाँ निर्दिष्ट शर्त लागू नहीं होती है। इसका मतलब यह है कि Prover केवल उन्हीं परिदृश्यों (scenarios) पर विचार करेगा जिनमें require एक्सप्रेशन का मूल्यांकन true के रूप में होता है, जिससे अन्य सभी परिदृश्यों को विश्लेषण (analysis) से प्रभावी ढंग से बाहर कर दिया जाता है।

उदाहरण के लिए, हम count के प्रारंभिक मान को शून्य (zero) तक सीमित (constrain) करने के लिए अपने checkCountValidity रूल में require स्टेटमेंट का उपयोग कर सकते हैं, जैसा कि नीचे दिखाया गया है:

Copy
rule checkCountValidity() {

    // We just added this 
    
require count() == 0;


    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    //Call to increment()
    increment();
    increment();
    increment();

    //Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Asserting that the initial value of count is 0
    assert PrecallCountValue == 0;
    assert PostcallCountValue == PrecallCountValue + 3;

}

यदि आप उपरोक्त परिवर्तन के साथ Prover को फिर से चलाते हैं और अपने टर्मिनल में प्रिंट किए गए वेरिफिकेशन लिंक को खोलते हैं, तो आपको एक वेरिफाइड (verified) रूल मिलेगा, जैसा कि नीचे दिखाया गया है।

इस बार, हम देख सकते हैं कि Prover ने हमारे रूल को सफलतापूर्वक सत्यापित (verify) कर लिया है। ऐसा इसलिए है, क्योंकि require कंस्ट्रेंट (constraint) के साथ, prover किसी भी ऐसे execution path को अनदेखा कर देगा जहाँ count का प्रारंभिक मान शून्य नहीं है।

डिफ़ॉल्ट रूप से, Prover किसी वेरिफाइड रूल के लिए कॉल ट्रेस प्रदान नहीं करता है क्योंकि रूल की शर्तों को पूरा करने वाले मान्य निष्पादन ट्रेसेस (valid execution traces) की संख्या बहुत बड़ी हो सकती है। चूँकि एक वेरिफाइड रूल इस बात की पुष्टि करता है कि कोई counterexamples मौजूद नहीं हैं, इसलिए सभी संभावित मान्य ट्रेसेस को उत्पन्न और प्रदर्शित करना अनावश्यक और अव्यावहारिक दोनों होगा।

satisfy के उपयोग को समझना

जैसा कि पहले उल्लेख किया गया है, जब कोई रूल सफलतापूर्वक सत्यापित हो जाता है तो Prover कॉल ट्रेस जनरेट नहीं करता है। हालाँकि, CVL satisfy स्टेटमेंट प्रदान करता है, जो आपको एक ऐसा निष्पादन ट्रेस (execution trace) तैयार करने की अनुमति देता है जो require और assert स्टेटमेंट्स द्वारा लागू की गई सभी शर्तों को पूरा करता है। यह विशेष रूप से तब उपयोगी होता है जब आप यह पुष्टि करना चाहते हैं कि क्या कॉन्ट्रैक्ट के लॉजिक (logic) के भीतर कोई विशिष्ट परिदृश्य (scenario) घटित हो सकता है।

उदाहरण के लिए, हम एक रूल लिख सकते हैं जो सत्यापित करने के लिए satisfy स्टेटमेंट का उपयोग करता है:

• कि कम से कम एक ऐसा execution path मौजूद है जहाँ एक उपयोगकर्ता LP टोकन जमा करने और मिंट (mint) करने के बाद अपनी तरलता (liquidity) पूरी तरह से वापस ले (withdraw) सकता है।
• कि कम से कम एक ऐसा execution path मौजूद है जहाँ उधारकर्ता (borrower) की पोजीशन को लिक्विडेट (liquidate) कर दिया जाता है यदि उनके कोलैटरल (collateral) का मूल्य एक निर्दिष्ट सीमा (threshold) से नीचे चला जाता है।

जब किसी रूल में satisfy स्टेटमेंट शामिल होता है, तो Prover जाँचता है कि क्या कम से कम एक वैध (valid) execution path शर्त को पूरा करता है। हालाँकि ऐसे कई रास्ते हो सकते हैं, केवल एक संतोषजनक (satisfying) ट्रेस जनरेट किया जाता है—यदि पाया जाता है। परिणाम के आधार पर, रूल को निम्नानुसार वर्गीकृत किया जाता है:

• Verified Rule (सत्यापित रूल): Prover रूल को verified के रूप में रिपोर्ट करता है यदि कम से कम एक वैध निष्पादन satisfy स्टेटमेंट को पूरा करता है।
• Violated Rule (उल्लिखित रूल): Prover रूल को violated के रूप में रिपोर्ट करता है यदि कोई भी execution path satisfy स्टेटमेंट को पूरा नहीं करता है।

रूल में satisfy का उपयोग करना

satisfy स्टेटमेंट कैसे काम करता है, इसे समझने के लिए, नीचे दिए गए specification पर विचार करें जिसमें एक रूल searchValidExecution() है जो satisfy स्टेटमेंट के साथ समाप्त होता है।

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

rule searchValidExecution {

    increment();
    increment();
    increment();

    satisfy count() == 8;
}

चूंकि रूल searchValidExecution एक satisfy स्टेटमेंट के साथ समाप्त होता है, यह Prover को संभावित निष्पादन पथों (execution paths) का पता लगाने और यह निर्धारित करने का निर्देश देता है कि क्या तीन increment() कॉल्स का ऐसा अनुक्रम मौजूद है जिसके परिणामस्वरूप count() 8 के मान तक पहुंच जाएगा। यदि इसे ऐसा कोई पथ मिल जाता है, तो Prover रूल को verified के रूप में रिपोर्ट करता है। अन्यथा, यह इसे violated के रूप में रिपोर्ट करता है।

यह जांचने के लिए कि क्या रूल searchValidExecution लागू होता है, Prover चलाएं और परिणाम देखने के लिए ब्राउज़र में वेरिफिकेशन लिंक खोलें।

उपरोक्त परिणाम बताते हैं कि Certora Prover ने रूल को सफलतापूर्वक सत्यापित (verify) कर लिया है। इसका मतलब है कि इसे कम से कम एक execution path मिला है जो satisfy स्टेटमेंट को पूरा करता है। विशेष रूप से, Prover ने एक ऐसी स्टेट की पहचान की जहाँ increment() को लगातार तीन बार कॉल करने के बाद count() 8 तक पहुँच जाता है।

यह परिणाम अपेक्षाओं के अनुरूप है क्योंकि, आदर्श रूप से, यदि प्रारंभिक मान 5 है तो increment() को लगातार तीन बार कॉल करने के बाद count() का मान 8 तक पहुँच सकता है (यह मानते हुए कि प्रत्येक कॉल गिनती (count) को 1 से बढ़ा देती है)। चूंकि रूल एक वैध निष्पादन पथ (valid execution path) की तलाश करता है, Prover ने इसके अस्तित्व की पुष्टि की, जिससे सफल वेरिफिकेशन हुआ।

Linear Equations (रैखिक समीकरणों) के सिस्टम्स को हल करने और सत्यापित करने के लिए Prover का उपयोग करना

चूँकि Prover किसी ऐसे रूल को प्रोसेस करते समय केवल एक ही निष्पादन पथ (execution path) का मूल्यांकन करता है जिसमें satisfy स्टेटमेंट होता है, यह एक सॉल्वर (solver) के रूप में कार्य करता है, जो दिए गए constraints (बाधाओं) को पूरा करने वाले इनपुट मानों को निर्धारित करता है। इस क्षमता को प्रदर्शित करने के लिए, आइए समीकरणों (equations) की एक प्रणाली का समाधान खोजने के लिए satisfy का उपयोग करें।

उदाहरण के लिए, निम्नलिखित समीकरणों पर विचार करें:

• $2x + 3y = 22$
• $4x - y = 2$

अब, मान लीजिए कि हम $x$ और $y$ के ऐसे पूर्णांक मान (integer values) खोजना चाहते हैं जो दोनों समीकरणों को संतुष्ट करते हों। इसे प्राप्त करने के लिए, हमें सबसे पहले एक Solidity फ़ंक्शन को परिभाषित करने की आवश्यकता है जो समीकरणों की प्रणाली को एन्कोड (encode) करता है**:**

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

contract Math {

    function eqn(uint256 x, uint256 y) external pure returns (bool) {
        return (2 * x + 3 * y == 22) && (4 * x - y == 2);
    }

}

एक बार जब हम Solidity फ़ंक्शन को परिभाषित कर लेते हैं, तो हम Prover को $x$ और $y$ के वैध (valid) मानों की खोज करने का निर्देश देने के लिए एक रूल बना सकते हैं जो constraints (बाधाओं) को पूरा करते हैं जैसा कि नीचे दिखाया गया है:

Copy
methods {

    function eqn(uint256, uint256) external returns (bool) envfree;
}

rule checkEqn() {

    uint256 x; 
    uint256 y;

    satisfy eqn(x, y) == true;
}

वैकल्पिक रूप से, वेरिएबल्स को रूल बॉडी के अंदर घोषित (declare) करने के बजाय सीधे रूल डिक्लेरेशन (declaration) में परिभाषित किया जा सकता है, जैसा कि नीचे दिखाया गया है:

Copy
rule checkEqn(uint256 x, uint256 y) {
    satisfy eqn(x, y) == true;
}

जब रूल निष्पादित (execute) किया जाता है, तो Prover $x$ और $y$ के ऐसे मान खोजने का प्रयास करता है जो फ़ंक्शन को true लौटाने योग्य बनाते हैं। इस मामले में, सही पूर्णांक समाधान $x = 2$ और $y = 6$ है।

इसके अतिरिक्त, यदि समीकरणों को इस तरह से संशोधित किया जाता है जो उन्हें असंगत (inconsistent) बनाता है—जैसे कि समानांतर रेखाओं (parallel lines) को परिभाषित करना—तो Prover यह पता लगा लेगा कि कोई समाधान मौजूद नहीं है। संशोधित प्रणाली पर विचार करें:

• $2x + 3y = 22$
• $4x + 6y = 50$

चूंकि दूसरा समीकरण पहले समीकरण का केवल एक गुणक (multiple) है लेकिन एक अलग स्थिरांक (constant) के साथ है, प्रणाली का कोई समाधान नहीं है क्योंकि दोनों रेखाएं अब समानांतर हैं और कभी प्रतिच्छेद (intersect) नहीं करती हैं। समतुल्य (equivalent) Solidity फ़ंक्शन है:

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

contract Math {

    function eqn(uint256 x, uint256 y) external pure returns (bool) {
        return (2 * x + 3 * y == 22) && (4 * x + 6 * y == 50);
    }

}

जब हम इस संशोधित फ़ंक्शन पर checkEqn() रूल को फिर से चलाते हैं, तो वेरिफिकेशन परिणाम इंगित करता है कि Prover सही ढंग से एक वैध समाधान की अनुपस्थिति की पहचान करता है।

उपरोक्त परिणाम Prover की क्षमता को उजागर करते हैं जो न केवल मौजूदा वैध समाधान खोजने में सक्षम है बल्कि यह पता लगाने और पुष्टि करने में भी सक्षम है कि कब constraints (बाधाओं) का एक सेट स्वाभाविक रूप से असंतोषजनक (unsatisfiable) है, जैसे असंगत (inconsistent) या समानांतर समीकरणों के मामले में।

satisfy Statements का उपयोग करते समय मुख्य विचार (Key Considerations)

किसी भी रूल में satisfy स्टेटमेंट का उपयोग करते समय कुछ महत्वपूर्ण बारीकियों (nuances) को ध्यान में रखना चाहिए:

• यदि किसी रूल में कई satisfy स्टेटमेंट्स हैं, तो Prover इसे केवल तभी सत्यापित (verified) के रूप में रिपोर्ट करेगा यदि सभी निष्पादित (executed) satisfy स्टेटमेंट्स कम से कम एक निष्पादन पथ (execution path) के लिए सत्य हों; अन्यथा, रूल को उल्लंघन (violated) माना जाएगा (डिफ़ॉल्ट Prover मोड में) जैसा कि नीचे दिखाया गया है:

• किसी कंडीशनल ब्रांच (conditional branch) पर एक satisfy स्टेटमेंट जिसे निष्पादित नहीं किया गया है, उसका सत्य होना आवश्यक नहीं है, क्योंकि वेरिफिकेशन के दौरान वहां तक कभी नहीं पहुंचा जाता है। Prover प्रत्येक execution path को स्वतंत्र रूप से सत्यापित करता है और निष्पादित पथों के लिए परिणाम की रिपोर्ट करता है, जैसा कि नीचे दिखाया गया है।

assert और satisfy के बीच अंतर

पहली नज़र में, assert और satisfy स्टेटमेंट्स कार्यक्षमता (functionality) में समान लग सकते हैं, क्योंकि दोनों का उपयोग रूल के भीतर शर्तों (conditions) को मान्य करने के लिए किया जाता है। हालाँकि, उनके उद्देश्य और उपयोग काफी भिन्न हैं, जैसा कि नीचे दिखाया गया है:

निष्कर्ष (Conclusion)

इस अध्याय में, हमने देखा कि वेरिफिकेशन के दौरान CVL स्टेटमेंट्स Certora Prover को कैसे निर्देशित करते हैं। हमने सीखा कि assert कैसे सभी निष्पादन पथों (execution paths) में प्रॉपर्टीज को लागू करता है, require कैसे उन अवस्थाओं (states) को सीमित करता है जिन पर Prover विचार करता है, और satisfy कैसे वैध निष्पादन पथों के अस्तित्व को प्रदर्शित करता है। इन स्टेटमेंट्स को समझना और यह जानना कि Prover arbitrary अवस्थाओं (states) के बारे में कैसे तर्क करता है, सही और प्रभावी CVL रूल्स लिखने के लिए आवश्यक है।

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