पिछले अध्याय में, हमने देखा कि Certora Prover का उपयोग करके formal verification करने के लिए, हमें Prover को निम्नलिखित प्रमुख आइटम प्रदान करने होंगे:

1. Smart Contract (.sol file)
2. Specification (.spec file)

इस अध्याय में, हम चर्चा करेंगे कि specification का सटीक अर्थ क्या है और इसे कैसे लिखा जाता है।

Specification क्या है?

Certora में, एक specification Certora Verification Language (CVL) में लिखा गया कोड का एक हिस्सा है जो उन नियमों का एक सेट परिभाषित करता है जिनका verification के अधीन contract को पालन करना चाहिए।

एक Certora specification या .spec file में कम से कम दो घटक (components) होने चाहिए:

1. एक या अधिक rules
2. एक Methods Block

इसमें अन्य घटक भी होते हैं, लेकिन अभी के लिए, हम इन पर ध्यान केंद्रित करेंगे और बाकी को जैसे-जैसे हम उनका उपयोग करेंगे, वैसे-वैसे पेश करेंगे।

Rules को समझना

एक rule smart contract में एक function call के अपेक्षित “पहले और बाद (before and after)” के व्यवहार को परिभाषित करता है। इसे rule कीवर्ड का उपयोग करके परिभाषित किया जाता है, जिसके बाद इसका नाम आता है, जैसा कि नीचे दिखाया गया है:

Copy
rule nameOfRule{}

CVL में, एक rule निम्नलिखित तीन मूलभूत अवधारणाओं (foundational concepts) का उपयोग करके लिखा जाता है:

1. Pre-conditional Requirement (वैकल्पिक): यह उन स्थितियों को निर्दिष्ट करता है जिनके तहत Prover द्वारा किसी rule का मूल्यांकन किया जाना चाहिए। इसे require स्टेटमेंट का उपयोग करके निर्दिष्ट किया जाता है।
2. Action: एक method call जो contract state को बदलता है।
3. Post-call Expectation: यह भाग action निष्पादित होने के बाद contract की अपेक्षित state को निर्दिष्ट करता है। इसे assert स्टेटमेंट का उपयोग करके निर्दिष्ट किया जाता है।

नोट : हम अगले अध्याय में require और assert स्टेटमेंट्स पर अधिक विस्तार से चर्चा करेंगे।

ऊपर चर्चा की गई अवधारणाओं को बेहतर ढंग से समझने के लिए, नीचे दिए गए Counter contract पर विचार करें।

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

contract Counter {  
    uint256 public count;  

    // Increment the count  
    function increment() public {  
        count += 1;  
    }  

    // Decrement the count  
    function decrement() public {    
        count -= 1;  
    }  

}

अब नीचे दिए गए rule पर विचार करें जो Counter contract के increment() function को formally verify करने के लिए लिखा गया है।

Copy
rule checkIncrementCall() {

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

    // Call OR Action
    increment();


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

}

हमारे checkIncrementCall() rule में:

• लाइन require count() == 0 pre-conditional requirement को परिभाषित करती है, जो Prover को निर्देश देती है कि वह इस rule पर केवल तभी विचार करे जब count का प्रारंभिक मान शून्य हो।
• लाइन increment() contract पर increment() function को invoke करके एक state transition करती है। यह परीक्षण किए जा रहे action को दर्शाता है।
• लाइन assert count() == 1 post-call expectation को परिभाषित करती है, जो action के बाद अपेक्षित state को निर्दिष्ट करती है। यहाँ, यह सुनिश्चित करता है कि शून्य पर सेट किए गए काउंटर पर increment() कॉल करने के बाद, काउंटर का मान अपडेट होकर 1 हो जाता है।

हमें इन तीनों को एक साथ रखने की आवश्यकता है क्योंकि:

• किसी action के बिना, परीक्षण (test) करने के लिए कुछ भी नहीं है, क्योंकि contract की state अपरिवर्तित रहती है।
• यदि हम postcondition checks शामिल नहीं करते हैं, तो हम वास्तव में कुछ भी verify नहीं कर रहे हैं। Assertions (assert स्टेटमेंट्स) checks यह सुनिश्चित करते हैं कि contract के state transitions हमारी अपेक्षाओं के अनुरूप हैं।
• precondition के बिना, rule अनपेक्षित परिदृश्यों (unintended scenarios) पर लागू हो सकता है।

यह ध्यान रखना महत्वपूर्ण है कि preconditions वैकल्पिक हैं। इनका उपयोग सावधानी के साथ किया जाना चाहिए, क्योंकि वे उन महत्वपूर्ण परिदृश्यों को बाहर कर सकते हैं जिन्हें verify करने की आवश्यकता है।

कुछ rules को बिना किसी pre-conditional requirement के भी लागू किया जा सकता है**।** उदाहरण के लिए, नीचे दिया गया rule हमारे Counter contract की अखंडता (integrity) की जाँच यह verify करके करता है कि increment() और decrement() के अनुक्रमिक (sequential) कॉल्स के परिणामस्वरूप count का मान अपरिवर्तित रहता है।

Copy
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;
}

हालाँकि, हमारी specification file में अभी भी methods block गायब है। आइए verification के लिए इसे Prover को सबमिट करने से पहले इसे जोड़ें।

Methods Block और इसका उपयोग

Methods Block में contract methods की एक सूची होती है जिन्हें rules verification के दौरान कॉल करेंगे। आप इसे Solidity में एक इंटरफ़ेस या ABI की तरह मान सकते हैं — यह Prover को बताता है कि कौन से functions मौजूद हैं, वे कैसे दिखते हैं, और उन्हें कैसे कॉल किया जा सकता है। Certora के संस्करण में कभी-कभी सादे Solidity की तुलना में थोड़ा अतिरिक्त सिंटैक्स होता है।

Methods Block को methods कीवर्ड का उपयोग करके परिभाषित किया जाता है, जैसा कि नीचे दिखाया गया है:

Copy
methods {
// Contract methods entries go here
}

Methods Block में प्रत्येक प्रविष्टि (entry) को नीचे दिए गए सिंटैक्स का पालन करना चाहिए:

• method को परिभाषित करने के लिए प्रत्येक प्रविष्टि function कीवर्ड से शुरू होनी चाहिए।
• method का नाम बिल्कुल वैसे ही निर्दिष्ट करें जैसा वह contract में दिखाई देता है।
• इनपुट पैरामीटर्स को कोष्ठक (parentheses) के अंदर सूचीबद्ध करें, कई इनपुट्स को अल्पविराम (commas) से अलग करें। यदि method कोई इनपुट नहीं लेता है, तो कोष्ठक को खाली छोड़ दें।
• एक visibility modifier जोड़ें, जो हमारे उद्देश्यों के लिए सभी methods के लिए external होना चाहिए। अधिक उन्नत specifications internal functions को संक्षेप (summarize) में प्रस्तुत कर सकते हैं, जिन्हें हम बाद में कवर करेंगे।
• यदि method कोई मान (value) लौटाता है, तो returns कीवर्ड का उपयोग करें जिसके बाद return type हो। यदि कोई वापसी मान (return value) नहीं है, तो इस भाग की आवश्यकता नहीं है।
• एक वैकल्पिक टैग जैसे envfree जोड़ें (जैसे-जैसे हम उनका उपयोग करेंगे हम अन्य टैग्स पर चर्चा करेंगे)।
• प्रत्येक method घोषणा (declaration) एक अर्धविराम (;) के साथ समाप्त होनी चाहिए।

यह ध्यान रखना बहुत महत्वपूर्ण है कि methods block में functions जोड़ने से verification तेज़ या अधिक प्रभावी नहीं होगा जब तक कि उन functions को envfree, optional के रूप में चिह्नित नहीं किया जाता है, या उनका कोई summary नहीं होता है। यदि इनमें से कोई भी शर्त पूरी नहीं होती है, तो function जोड़ने का कोई प्रभाव नहीं पड़ेगा, और verifier संभवतः रिपोर्ट में इसके बारे में चेतावनी (warning) जारी करेगा।

चीजों को सरल और समझने में आसान रखने के लिए, इस अध्याय में हम केवल envfree पर ध्यान केंद्रित करेंगे। हम एक अलग अध्याय में optional और summarization का पता लगाएंगे।

envfree टैग का उपयोग कब करें?

Methods Block में किसी method को तब envfree घोषित किया जाता है जब उसका निष्पादन (execution) Solidity के ग्लोबल वेरिएबल्स, जैसे msg.sender, block.number, या tx.origin पर निर्भर नहीं करता है।

उदाहरण के लिए, नीचे दिए गए add() function पर विचार करें:

Copy
function add(uint256 x, uint256 y) external returns (uint256) {
    return x + y;
}

चूंकि add() विशेष रूप से अपने इनपुट पैरामीटर्स पर काम करता है और इसे अपने निष्पादन के लिए block.timestamp, msg.sender, msg.value या tx.origin जैसी किसी भी वैश्विक ब्लॉकचेन state तक पहुंच की आवश्यकता नहीं है, इसका मतलब है कि हम इसे Methods Block में envfree के रूप में घोषित कर सकते हैं, जैसा कि नीचे दिखाया गया है:

Copy
methods {  
    add(uint256, uint256) external returns(uint256) envfree;  
}

इसके विपरीत, कुछ functions को अपने निष्पादन के लिए वैश्विक ब्लॉकचेन state तक पहुंच की आवश्यकता होती है और इसलिए उन्हें envfree घोषित नहीं किया जा सकता है। उदाहरण के लिए, नीचे दिया गया balance() function कॉलर का बैलेंस प्राप्त करता है:

Copy
function balance() external view returns(uint256) {
    return balances[msg.sender];
}

चूंकि balance(), msg.sender पर निर्भर करता है, इसलिए इसे envfree घोषित नहीं किया जा सकता है। नीचे दिया गया है कि हमें इसे Methods Block में कैसे परिभाषित करना चाहिए:

Copy
methods {  
    balance() external returns(uint256);  
}

हमारे spec में Methods Block जोड़ना

चूंकि हमारे rules (checkIncrementCall और checkCounter) Counter contract के count(), increment(), और decrement() methods को कॉल करते हैं, इसलिए हमारे specification के लिए Methods Block में इन functions को सूचीबद्ध किया जाना चाहिए, जैसा कि नीचे दिखाया गया है:

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

इनमें से किसी भी functions को अपने निष्पादन के लिए Solidity के ग्लोबल वेरिएबल्स तक पहुंच की आवश्यकता नहीं है, इसलिए हमने उन्हें envfree के रूप में चिह्नित किया है। यदि contract में अन्य functions हैं जो हमारे specification में उपयोग नहीं किए गए हैं, तो हमें उन्हें Methods Block में शामिल करने की आवश्यकता नहीं है।

Verification चलाना

ऊपर चर्चा किए गए rules को verify करने के लिए, नीचे दिए गए निर्देशों का पालन करें:

• एक टर्मिनल खोलें और सुनिश्चित करें कि आप उस certora-counter डायरेक्टरी में हैं जिसे हमने पिछले अध्याय में बनाया था।
• VS Code या अपनी पसंद के किसी अन्य कोड एडिटर में certora-counter डायरेक्टरी खोलें।
• दो खाली फाइलें बनाएं: contracts सबडायरेक्टरी के अंदर Counter2.sol और specs सबडायरेक्टरी के अंदर counter-2.spec।
• नीचे दिए गए smart contract को कॉपी करें और Counter2.sol में पेस्ट करें।

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

contract Counter {  
    uint256 public count;  

    // Increment the count  
    function increment() public {  
        count += 1;  
    }  

    // Decrement the count  
    function decrement() public {    
        count -= 1;  
    }  

}

• नीचे दिए गए specification को कॉपी करें और counter-2.spec में पेस्ट करें।

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;
}

• अपने टर्मिनल में नीचे दिए गए कमांड को चलाकर Python वर्चुअल वातावरण (virtual environment) को सक्रिय करें:

Copy
source certora-env/bin/activate

• अपने टर्मिनल में Certora एक्सेस कुंजी को पर्यावरण चर (environment variable) के रूप में लोड करें:

Copy
source .profile  # For Bash
# OR
source .zshenv  # For Zsh

• नीचे दिए गए कमांड को चलाकर सही Solidity कंपाइलर संस्करण सेट करें:

Copy
solc-select use 0.8.25

• अंत में, निम्नलिखित कमांड चलाकर verification के लिए specification और contract को Prover को सबमिट करें:

Copy
certoraRun contracts/Counter2.sol:Counter --verify Counter:specs/counter-2.spec

Verification Result को समझना

यदि Prover बिना किसी त्रुटि के कोड को सफलतापूर्वक कंपाइल करता है, तो यह आपके टर्मिनल में verification परिणामों का लिंक प्रिंट करेगा।

Verification परिणामों को देखने के लिए, ब्राउज़र का उपयोग करके अपने टर्मिनल में प्रिंट किए गए लिंक को खोलें। परिणाम नीचे दी गई छवि के समान दिखने चाहिए:

हमारे मामले में, यह तीन rules के लिए परिणाम दिखाता है:

• checkCounter : यह हमारे spec से checkCounter rule के लिए verification परिणाम दिखाता है।
• checkIncrementCall : यह हमारे spec से checkIncrementCall rule के लिए verification परिणाम दिखाता है।
• envfreeFuncsStaticCheck : जब Methods Block में envfree के रूप में चिह्नित functions होते हैं, तो Prover यह verify करता है कि वे Solidity के ग्लोबल वेरिएबल्स पर निर्भर नहीं हैं। इस verification के परिणाम envfreeFuncsStaticCheck के रूप में प्रकाशित किए जाते हैं।

हरा चेक मार्क (✅) इंगित करता है कि Prover को कोई उल्लंघन (violations) नहीं मिला है, जिसका अर्थ है कि हमारे rules सफलतापूर्वक verify हो गए हैं। किसी उल्लंघन के मामले में, लाल क्रॉस मार्क (❌) प्रदर्शित किया जाएगा।

भले ही सभी rules verify हो गए हों, इसका मतलब यह नहीं है कि पूरा contract बग-मुक्त है। कोड के अन्य हिस्सों में बग हो सकते हैं। ऐसा भी हो सकता है कि हमारा spec हमारी सभी अपेक्षाओं को कैप्चर न करता हो। उदाहरण के लिए, हमने यह निर्दिष्ट नहीं किया कि यदि काउंटर 0 पर होने पर हम decrement() को कॉल करते हैं तो क्या होना चाहिए। अगले अध्यायों में, हम दिखाएंगे कि यहाँ चर्चा किए गए नियम की तुलना में अधिक जटिल rules कैसे व्यक्त किए जाते हैं।

निष्कर्ष

इस अध्याय में, हमने इंटरफ़ेस परिभाषा के लिए Methods Block और लॉजिक परीक्षण के लिए Rule Block पर ध्यान केंद्रित करते हुए एक .spec फ़ाइल की संरचना (anatomy) का पता लगाया। हमने यह भी देखा कि envfree जैसे टैग verification प्रक्रिया को परिष्कृत (refine) करने में कैसे मदद करते हैं। अगले अध्याय में, हम require और assert स्टेटमेंट्स पर विस्तृत नज़र डालकर इस आधार को आगे बढ़ाएंगे।

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