परिचय

पिछले अध्याय में, हमने parametric rules के बारे में सीखा, जो हमें उन properties को formally verify करने की अनुमति देते हैं जिनके बारे में यह अपेक्षा की जाती है कि वे लागू रहें, चाहे कोई भी function कॉल किया गया हो। यह universal invariants को verify करने के लिए विशेष रूप से उपयोगी है। लेकिन क्या होगा यदि अपेक्षित व्यवहार universal न हो, और इसके बजाय कॉल किए जा रहे विशिष्ट function पर निर्भर हो? उदाहरण के लिए, इन परिदृश्यों पर विचार करें:

• किसी भी contract का owner समान रहना चाहिए, सिवाय उस स्थिति के जब owner changeOwner या renounceOwnership को कॉल करता है।
• एक ERC-20 token की कुल सप्लाई (total supply) समान रहनी चाहिए, सिवाय उस स्थिति के जब tokens को मिंट (mint) या बर्न (burn) किया जा रहा हो।

हम ऐसे मामलों को कैसे संभालते हैं जहाँ एक property आम तौर पर लागू होती है लेकिन function के आधार पर ज्ञात अपवाद (exceptions) होते हैं? या क्या होगा यदि आप बस कुछ प्रशासनिक (administrative) methods को सामान्य invariant जांच से पूरी तरह से बाहर करना चाहते हैं?

इस अध्याय में, हम सीखेंगे कि parametric rules में function-specific assertions को लागू करने के लिए method properties का उपयोग कैसे किया जाता है। हम यह भी देखेंगे कि जब वे नियम लागू नहीं होते हैं तो verification से कुछ functions को कैसे बाहर किया जाए।

Method Properties क्या हैं?

नीचे दिया गया कोड एक parametric rule दिखाता है — एक ऐसा नियम जो सभी functions पर लागू होता है।

Copy
rule someParametricRule() {  
    env e;
      
    method f;  
    calldataarg args;  
    f(e, args);  

    assert property_1;  
}

चाहे आपको function-specific assertions लागू करने हों या कुछ functions को नियम से बाहर करना हो, आपको एक function को दूसरे से अलग करने के लिए एक तरीके की आवश्यकता होती है। यहीं पर method properties काम आती हैं।

CVL में, method properties ऐसे attributes होते हैं जिन्हें field-like सिंटैक्स (जैसे, f.propertyName) का उपयोग करके method वेरिएबल (जैसे f) पर एक्सेस किया जा सकता है। ये properties उस function के बारे में जानकारी प्रदान करती हैं जिसे रनटाइम पर f संदर्भित करता है, जिससे आपके नियम का लॉजिक (rule logic) कॉल किए जा रहे विशिष्ट method के आधार पर अनुकूलित हो सकता है।

उपलब्ध method properties में शामिल हैं:

• f.selector : यह 4-byte function selector (function signature का एक हैश, उदाहरण के लिए, 0xa9059cbb) लौटाता है, जिसका उपयोग विशिष्ट नामित functions की पहचान करने के लिए किया जा सकता है (जैसे, f.selector == sig:transfer(address,uint256).selector) ताकि parametric rule में function-specific assertions लागू किए जा सकें।
• f.isPure : यदि function f को Solidity में pure कीवर्ड के साथ घोषित किया गया है, तो यह true लौटाता है। यह विशुद्ध रूप से गणनात्मक (computational) functions को उन नियमों से बाहर करने के लिए उपयोगी हो सकता है जो केवल state-modifying लॉजिक के लिए सार्थक हैं।
• f.isView : यदि function f को view कीवर्ड के साथ घोषित किया गया है, तो यह true लौटाता है। state परिवर्तन से संबंधित नियम लिखते समय read-only functions को छोड़ने के लिए इसका उपयोग किया जा सकता है। हम बाद के अनुभाग में इसके लाभों का पता लगाएंगे।
• f.isFallback : यदि f किसी fallback() या receive() function को दर्शाता है, तो यह true लौटाता है। यह तब मददगार होता है जब आपको fallback व्यवहार को नियंत्रित करने वाले नियम लिखने होते हैं—जैसे payable आवश्यकताएं या low-level कॉल के लिए विशेष हैंडलिंग।
• f.numberOfArguments : यह उन arguments की संख्या (number of arguments) लौटाता है जिनकी अपेक्षा function f करता है।
• f.contract : यह उस contract को लौटाता है जिसमें function परिभाषित है। यह तब उपयोगी होता है जब आप एक ही समय में कई contracts को verify कर रहे होते हैं, या inheritance से निपट रहे होते हैं—जैसे जब दो contracts में समान नाम और arguments वाले functions होते हैं। यह कुछ ऐसा है जिसका पता हम बाद के अध्यायों में लगाएंगे, क्योंकि हमारे वर्तमान उदाहरणों में केवल एक ही contract शामिल है।

इन सभी में से, सबसे अधिक उपयोग की जाने वाली method properties f.selector, f.isView, और f.isPure हैं। ये सबसे विशिष्ट उपयोग के मामलों (use cases) को कवर करती हैं—जैसे किसी विशिष्ट function की पहचान करना (selector का उपयोग करके) या state में बदलाव पर केंद्रित नियम लिखते समय read-only और computational functions (isView और isPure) को छोड़ना। चीजों को व्यावहारिक (practical) रखने के लिए, हम आगामी उदाहरणों में इन properties पर ध्यान केंद्रित करेंगे और दिखाएंगे कि वे अधिक सटीक और कुशल parametric rules लिखने में कैसे मदद करते हैं।

Parametric Rule में Function-Dependent Assertion लागू करना

यह समझने के लिए कि एक parametric rule के भीतर function-dependent assertions को लागू करने के लिए method properties का उपयोग कैसे किया जा सकता है, नीचे दिए गए ERC-20 implementation RareToken पर विचार करें, जिसमें mint और burn दोनों कार्यक्षमताएं (functionality) शामिल हैं:

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

contract RareToken {
    uint256 public totalSupply;
    address public owner;
    
    mapping(address => uint256) public balanceOf;
    mapping(address => mapping(address => uint256)) public allowance;

    event Transfer(address indexed from, address indexed to, uint256 value);
    event Approval(address indexed owner, address indexed spender, uint256 value);

    modifier onlyOwner() {
        require(msg.sender == owner, "Unauthorized");
        _;
    }

    constructor(uint256 _initialSupply) {
        owner = msg.sender;
        if (_initialSupply > 0) {
            _mint(msg.sender, _initialSupply);
        }
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        _transfer(msg.sender, to, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        _approve(msg.sender, spender, amount);
        return true;
    }

    function transferFrom(address from, address to, uint256 amount) public virtual returns (bool) {
        address spender = msg.sender;
        uint256 currentAllowance = allowance[from][spender];
        require(currentAllowance >= amount, "Allowance exceeded");
        
        if (currentAllowance != type(uint256).max) {
            _approve(from, spender, currentAllowance - amount);
        }
        
        _transfer(from, to, amount);
        return true;
    }

    function mint(address account, uint256 amount) public onlyOwner {
        _mint(account, amount);
    }

    function burn(uint256 amount) public virtual {
        _burn(msg.sender, amount);
    }

    function _transfer(address from, address to, uint256 amount) internal virtual {
        require(from != address(0), "Invalid sender");
        require(to != address(0), "Invalid recipient");
        
        uint256 fromBalance = balanceOf[from];
        require(fromBalance >= amount, "Insufficient balance");
        
        balanceOf[from] = fromBalance - amount;
        balanceOf[to] += amount;
        emit Transfer(from, to, amount);
    }

    function _mint(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid recipient");
        
        totalSupply += amount;
        balanceOf[account] += amount;
        emit Transfer(address(0), account, amount);
    }

    function _burn(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid burner");
        
        uint256 accountBalance = balanceOf[account];
        require(accountBalance >= amount, "Burn exceeds balance");
        
        balanceOf[account] = accountBalance - amount;
        totalSupply -= amount;
        emit Transfer(account, address(0), amount);
    }

    function _approve(address ownerAccount, address spender, uint256 amount) internal virtual {
        require(ownerAccount != address(0), "Invalid owner");
        require(spender != address(0), "Invalid spender");
        
        allowance[ownerAccount][spender] = amount;
        emit Approval(ownerAccount, spender, amount);
    }
}

चूँकि उपरोक्त ERC-20 implementation में mint() और burn() शामिल हैं, इसलिए उन function कॉल के दौरान totalSupply मूल्य के बदलने की उम्मीद है—पिछले अध्याय में उपयोग किए गए ERC-20 implementation के विपरीत, जहाँ किसी भी function को सप्लाई (supply) बदलने की अनुमति नहीं थी।

अब, मान लीजिए कि हम RareToken contract के लिए एक parametric rule लिखना चाहते हैं जो निम्नलिखित व्यवहार लागू करता है:

• जब mint() function को कॉल किया जाता है, तो totalSupply घटना नहीं चाहिए (यह या तो बढ़ सकता है या समान रह सकता है यदि राशि शून्य है)।
• जब burn() function को कॉल किया जाता है, तो totalSupply बढ़ना नहीं चाहिए (यह या तो घट सकता है या समान रह सकता है यदि राशि शून्य है)।
• किसी भी अन्य function (जैसे transfer, approve, transferFrom) के लिए, totalSupply अपरिवर्तित रहना चाहिए।

उपरोक्त व्यवहार को लागू करने वाले एक parametric rule को परिभाषित करने के लिए, नियम को निम्नलिखित सुनिश्चित करना चाहिए:

1. state की तुलना के लिए एक संदर्भ बिंदु (reference point) स्थापित करने के लिए नियम को किसी भी function execution से पहले totalSupply वेरिएबल के प्रारंभिक मान (initial value) को रिकॉर्ड करना चाहिए।
2. totalSupply state पर कई functions के प्रभाव का मूल्यांकन करने के लिए, नियम को एक parametric framework का उपयोग करना चाहिए जो प्रत्येक लक्ष्य function (target function) को एक-एक करके निष्पादित (execute) करता है।
3. प्रत्येक function का निष्पादन (execution) पूरा होने के बाद, state संशोधनों (modifications) को ट्रैक करने के लिए नियम को totalSupply के अद्यतन मान (updated value) को रिकॉर्ड करना चाहिए।
4. अंत में, नियम को निष्पादित function के आधार पर तीन महत्वपूर्ण assertions को लागू करना चाहिए।

निम्नलिखित नियम, totalSupplyIntegrityCheck, इन सभी चरणों को लागू करता है। यह प्रत्येक function निष्पादन के पहले और बाद में totalSupply को कैप्चर करता है, एक parametric सेटअप का उपयोग करके किसी भी method को लागू करता है, और फिर कौन सा function कॉल किया गया था, उसके आधार पर अपेक्षित व्यवहार (expected behavior) लागू करता है:

Copy
rule totalSupplyIntegrityCheck() {

    env e;

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    method f;
    calldataarg args;
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

उपरोक्त नियम में, हमने f.selector का उपयोग करके एक arbitrary function (f) के function selector को एक्सेस किया, और हमने sig:functionName(...).selector नोटेशन का उपयोग करके एक ज्ञात function के function selector को प्राप्त किया। फिर हमने इसका उपयोग यह तुलना करने के लिए किया कि निष्पादित (executed) function f किसी विशिष्ट नामित function जैसे mint() या burn() से मेल खाता है या नहीं, ताकि हमारे parametric rule के भीतर function-specific assertions लागू किए जा सकें।

उपरोक्त नियम बस निम्नलिखित व्यवहार को लागू करता है:

1. यदि mint() function निष्पादित होता है (जिसे f.selector == sig:mint(address,uint256).selector द्वारा पहचाना जाता है), तो totalSupply का मान अपने प्रारंभिक मान की तुलना में घटना नहीं चाहिए।
2. यदि burn() function निष्पादित होता है (जिसे f.selector == sig:burn(uint256).selector द्वारा पहचाना जाता है), तो totalSupply का मान अपने प्रारंभिक मान की तुलना में बढ़ना नहीं चाहिए।
3. अन्य सभी function कॉल्स के लिए, नियम यह लागू करता है कि totalSupply का मान अपरिवर्तित रहना चाहिए, यह सुनिश्चित करते हुए कि कोई भी अनपेक्षित (unintended) function totalSupply वेरिएबल को संशोधित न करे।

हमारे parametric rule के परिणाम देखने के लिए, RareToken contract और उसके specification को उचित डायरेक्टरी में रखकर Certora Prover वातावरण (environment) सेट करें। इसके बाद, verification प्रक्रिया चलाएँ। यदि contract नियम की शर्तों को पूरा करता है, तो prover बिना किसी उल्लंघन (violations) का पता लगाए एक सफल verification की पुष्टि करेगा, जैसा कि नीचे दिए गए परिणामों में दिखाया गया है।

Verification परिणाम पुष्टि करते हैं कि totalSupplyIntegrityCheck नियम सफलतापूर्वक निष्पादित किया गया था, और सभी नौ जाँचें (checks) बिना किसी उल्लंघन का पता लगाए पास हो गईं। यह मान्य करता है कि RareToken contract में mint(), burn(), और अन्य functions का व्यवहार नियम की अपेक्षाओं के अनुरूप है—totalSupply, mint() के बाद बढ़ता है, burn() के बाद घटता है, और अन्य सभी functions के लिए अपरिवर्तित रहता है।

उपरोक्त नियम प्रत्येक function f को निष्पादित (execute) करने के बाद सही assertions लागू करने के लिए f.selector पर आधारित conditional लॉजिक का सफलतापूर्वक उपयोग करता है। यह सुनिश्चित करता है कि नियम के parameters के अनुकूल प्रत्येक function को उसकी पहचान के आधार पर उचित अपेक्षा (expectation) के विरुद्ध जांचा जाता है।

filtered Blocks के साथ Parametric Rule को Optimize करना

जब हम verification रिपोर्ट की समीक्षा करते हैं, तो हम देखते हैं कि Certora Prover ने हमारे assertion चेक को contract के हर function पर लागू किया है—जिसमें totalSupply(), balanceOf(), और owner() जैसे read-only functions भी शामिल हैं। इन functions को Solidity में view के रूप में चिह्नित किया गया है, जिसका अर्थ है कि वे केवल ब्लॉकचेन state से पढ़ते हैं और कुछ भी संशोधित नहीं करते हैं। इस कारण से, इन functions पर state-change नियम चलाना बहुत अधिक मायने नहीं रखता है और हमें सार्थक (meaningful) बग पकड़ने में मदद नहीं करता है।

भले ही उन्हें verify करना तकनीकी रूप से गलत नहीं है, लेकिन यह अतिरिक्त कम्प्यूटेशनल काम का कारण बनता है और प्रक्रिया को धीमा कर देता है। इसलिए उन functions को बाहर करना महत्वपूर्ण है जो परीक्षण किए जा रहे नियम के लिए प्रासंगिक (relevant) नहीं होने पर contract state को प्रभावित नहीं करते हैं। यहीं पर filter ब्लॉक काम आता है।

फ़िल्टर (filter) ब्लॉक हमें isView, isPure आदि जैसी method properties के आधार पर किसी parametric rule द्वारा विश्लेषण किए जाने वाले methods को चयनात्मक रूप से शामिल करने या बाहर करने (selectively include or exclude) की अनुमति देता है।

View Functions को बाहर करने के लिए filtered Block का उपयोग करना

फ़िल्टर ब्लॉक की कार्यप्रणाली को समझने के लिए, नीचे दिए गए specification पर विचार करें जिसमें एक ऐसा नियम शामिल है जिसमें एक फ़िल्टर ब्लॉक होता है।

Copy
rule totalSupplyIntegrityCheck(env e, method f, calldataarg args) filtered {
    f -> !f.isView
} {

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

उपरोक्त नियम में, फ़िल्टर ब्लॉक filtered {} के अंदर की लाइन f -> !f.isView एक फ़िल्टर के रूप में कार्य करती है जो Prover को बताती है: "इस नियम को केवल उन functions पर चलाएं जहां f.isView false है।" दूसरे शब्दों में, यह view के रूप में चिह्नित सभी functions को verification से बाहर कर देता है।

यदि हम उपरोक्त specification के साथ Prover को फिर से चलाते हैं, तो हम देख सकते हैं कि totalSupply(), balanceOf(), और owner() जैसे view functions अब इस नियम के verification में शामिल नहीं हैं, जैसा कि नीचे दी गई छवि (image) में दिखाया गया है:

एक parametric rule के अंदर फ़िल्टर ब्लॉक का उपयोग करने से हमें दो चीजें प्राप्त करने में मदद मिलती है:

1. यह उन अप्रासंगिक (irrelevant) functions को छोड़कर कम्प्यूटेशनल ओवरहेड (computational overhead) को कम करता है जिनके बारे में गारंटी है कि वे contract के state को नहीं बदलेंगे।
2. यह verification आउटपुट को सरल बनाता है, जिससे हम केवल state-changing functions के परिणामों पर ध्यान केंद्रित कर पाते हैं।

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

इस प्रकार हम function-specific assertions को लागू करने के साथ-साथ फ़िल्टर किए गए ब्लॉक (filtered blocks) का उपयोग करके verification से अप्रासंगिक (irrelevant) functions को बाहर करने के लिए method properties का उपयोग कर सकते हैं।

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