अब तक, पिछले अध्यायों में, हमने विशिष्ट methods के व्यवहार और contract की state पर उनके प्रभाव को verify करने के लिए rules लिखे हैं। उदाहरण के लिए:

• Chapter 2 में, हमने यह verify करने के लिए एक rule लिखा था कि increment() को कॉल करने से count की वैल्यू एक बढ़ जाती है।
• Chapter 3 में, हमने यह चेक करने के लिए एक rule लिखा था कि increment() और decrement() को लगातार कॉल करने पर count की वैल्यू अपरिवर्तित (unchanged) रहनी चाहिए।

लेकिन क्या होगा यदि हम उन properties के बारे में तर्क (reason) करना चाहते हैं जो इस बात की परवाह किए बिना सत्य (true) रहनी चाहिए कि कौन सा function कॉल किया गया है? उदाहरण के लिए, निम्नलिखित properties पर विचार करें:

• एक साधारण voting contract में, कुल वोटों की संख्या हमेशा पक्ष (favor) और विपक्ष (against) में पड़े वोटों के योग (sum) के बराबर होनी चाहिए।
• एक ERC-20 contract में, किसी user का balance कभी भी token की total supply से अधिक नहीं होना चाहिए।

इस अध्याय में, हम सीखेंगे कि जिन्हें parametric rules के रूप में जाना जाता है, उन्हें कैसे लिखा जाए—ये ऐसे rules हैं जो हमें उन properties को formally verify करने की अनुमति देते हैं जिनके बारे में यह अपेक्षा की जाती है कि वे किसी भी function के कॉल होने की परवाह किए बिना बनी रहें।

Parametric Rules का परिचय

CVL में, एक standard rule अक्सर किसी विशिष्ट (specific) function call के बाद state transitions की जाँच करता है। आप आमतौर पर इस तरह के पैटर्न का उपयोग करके परिभाषित करते हैं कि कौन से state transitions अनुमत (allowed) हैं:

Copy
rule any_general_rule{

  require <setup conditions>;
  
  mySpecificFunction(arg1, arg2);
   
  assert <expected outcome>;     
}

एक parametric rule इसी तरह काम करता है लेकिन इस concept को सामान्य (generalize) करता है। केवल एक function(args) पर ध्यान केंद्रित करने के बजाय, एक parametric rule यह verify करता है कि किसी भी function को किसी भी valid arguments के साथ कॉल करने के बाद कोई property सत्य (true) बनी रहती है।

CVL “Any Function, Any Args” को कैसे हैंडल करता है

“any function with any valid arguments” के इस विचार को व्यक्त करने के लिए, CVL दो विशेष types प्रदान करता है:

1. method: आप जिस contract को verify कर रहे हैं, उसके भीतर किसी भी public या external function को दर्शाता है। method type का एक variable declare करने का अर्थ है कि rule contract में किसी भी function को dynamically reference और execute कर सकता है।
2. calldataarg: किसी function call के लिए arguments को दर्शाता है। चूँकि अलग-अलग functions को अलग-अलग inputs की आवश्यकता होती है, calldataarg यह सुनिश्चित करता है कि जिस भी function (method) को test किया जा रहा है, उसके लिए valid arguments अपने आप प्रदान किए जाएँ।

The Parametric Call Syntax

ये दो विशेष types हमें वह बनाने की अनुमति देते हैं जिसे हम a parametric call कहते हैं, जो verification के अधीन contract के प्रत्येक public या external method को निम्नलिखित syntax का उपयोग करके एक्सेस करने और कॉल करने में एक rule को सक्षम बनाता है:

Copy
rule someParametricRule() { 

    env e;
    
    method f;
    calldataarg args;
    
    f(e,args)
    
    //Any assert statement should go here
    assert <property_1>;
    assert <property_2>;
 }

f(e, args) लाइन को parametric call कहा जाता है। यह हमें मैन्युअल रूप से किसी एक को चुनने के बजाय contract के सभी public या external functions को test करने की अनुमति देता है। यह इस प्रकार काम करता है:

• f contract में किसी भी function को दर्शाता है। किसी विशेष function को specify करने के बजाय, यह variable यह सुनिश्चित करता है कि हर function का एक-एक करके परीक्षण (test) किया जाए।
• args valid input values के एक सेट को दर्शाता है। चूँकि अलग-अलग functions के अलग-अलग parameters होते हैं, args यह सुनिश्चित करता है कि प्रत्येक function के लिए सही प्रकार और संख्या में inputs प्रदान किए गए हैं।
• e: function call सिमुलेशन के लिए आवश्यक environmental context (जैसे sender address, block number) प्रदान करता है।

मूल रूप से, f(e, args); लाइन Certora Prover को बताती है: “इस contract के प्रत्येक function f के लिए, इसे एक simulated environment e में valid arguments args के साथ execute करें।”

f(e, args); लाइन के बाद assert statements रखकर, हम उन properties को परिभाषित करते हैं जिन्हें किसी भी function call के पूरा होने के बाद सार्वभौमिक रूप से (universally) सत्य (true) होना चाहिए। यह parametric rules को smart contracts के मुख्य invariants और सामान्य safety properties को verify करने के लिए आदर्श बनाता है।

ERC-20 में Invariants की पहचान करना

आइए हमने जो कुछ सीखा है उसे नीचे दिखाए गए एक ERC-20 Implementation के एक invariant को formally verify करने के लिए लागू करें:

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

contract RareToken {
    uint8 public immutable decimals = 18;
    uint256 public immutable totalSupply;

    mapping(address => uint256) private balances;
    mapping(address => mapping(address => uint256)) private allowances;

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

    constructor(uint256 _initialSupply) {
        require(_initialSupply > 0, "Invalid initial supply");
        
        totalSupply = _initialSupply * 10 ** uint256(decimals);
        balances[msg.sender] = totalSupply;
        
        emit Transfer(address(0), msg.sender, totalSupply);
    }

    function balanceOf(address account) public view returns (uint256) {
        return balances[account];
    }

    function transfer(address recipient, uint256 amount) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[msg.sender] >= amount, "Insufficient balance");
        
        balances[msg.sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(msg.sender, recipient, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public returns (bool) {
        require(spender != address(0), "ERC20: approve to zero address");
        
        allowances[msg.sender][spender] = amount;
        emit Approval(msg.sender, spender, amount);
        return true;
    }

    function allowance(address owner_, address spender) public view returns (uint256) {
        return allowances[owner_][spender];
    }

    function transferFrom(
        address sender,
        address recipient,
        uint256 amount
    ) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[sender] >= amount, "Insufficient balance");
        
        uint256 currentAllowance = allowances[sender][msg.sender];
        require(currentAllowance >= amount, "ERC20: insufficient allowance");
        
        if (currentAllowance != type(uint256).max) {
            allowances[sender][msg.sender] = currentAllowance - amount;
        }
        
        balances[sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(sender, recipient, amount);
        return true;
    }
}

जैसा कि हमने सीखा है, parametric rules लिखने का उद्देश्य उन smart contract properties को verify करना है जिन्हें हमेशा अलग-अलग function calls में सत्य (true) रहना चाहिए। हमारे RareToken contract के मामले में, एक प्रमुख invariant है: Total Supply Stability (कुल आपूर्ति स्थिरता)।

चूँकि contract में mint या burn कार्यक्षमता (functionality) शामिल नहीं है, total supply को डिप्लॉयमेंट के समय एक बार initialize किया जाता है और इसे contract के पूरे जीवनकाल में स्थिर (constant) रहना चाहिए। दूसरे शब्दों में, किसी भी function को totalSupply() द्वारा लौटाई गई वैल्यू को कभी modify नहीं करना चाहिए।

आइए देखें कि total supply की अखंडता (integrity) को verify करने के लिए हम एक parametric rule कैसे लिख सकते हैं।

Total Supply Consistency को Formally Verify करना

एक बार जब हम contract के उन प्रमुख invariants की पहचान कर लेते हैं जिन्हें हम verify करना चाहते हैं, तो एक parametric rule लिखने के लिए इन चरणों का पालन करें:

1. Rule को परिभाषित करें (Define the Rule)

rule कीवर्ड का उपयोग करें, जिसके बाद rule का एक वर्णनात्मक (descriptive) नाम हो:

Copy
rule totalSupplyIsConstant() { }

2. Execution Environment घोषित करें (Declare the Execution Environment)

Function के execution environment को दर्शाने के लिए एक env variable को परिभाषित करें:

Copy
rule totalSupplyIsConstant() {
    env e;
}

3. Pre-Call State को कैप्चर करें

चूँकि हमें function execution से पहले और बाद में totalSupply की वैल्यू की तुलना करने की आवश्यकता है, हम इसकी प्रारंभिक (initial) state को स्टोर करते हैं:

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);
}

4. Function Execution को मॉडल करें

किसी भी function call को दर्शाने के लिए एक method variable घोषित करें और उन arguments को परिभाषित करें जिन्हें पास किया जा सकता है:

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args); // Execute the function call with the given arguments
}

5. Post-Call State को कैप्चर करें

Function को execute करने के बाद, हम totalSupply की अपडेटेड वैल्यू को स्टोर करेंगे:

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);
}

6. Total Supply Consistency को लागू करें (Enforce the Total Supply Consistency)

हमारे RareToken contract के मामले में, हम यह सुनिश्चित करना चाहते हैं कि किसी भी function execution के बाद totalSupply variable कभी नहीं बदलना चाहिए। हम इस शर्त (condition) को स्पष्ट रूप से लागू करने के लिए assert स्टेटमेंट (assert beforeSupply == afterSupply) का उपयोग करते हैं:

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);

    assert beforeSupply == afterSupply; 
}

Verification को रन करना

हमारे parametric rule के परिणाम (results) देखने के लिए, पिछले अध्यायों में आपने जो सीखा है उसे लागू करें: RareToken contract और उससे जुड़ी specification को Certora Prover एनवायरनमेंट में रखें।

एक बार सेटअप पूरा हो जाने पर, verification प्रक्रिया शुरू करें। यदि contract rule द्वारा परिभाषित सभी शर्तों को पूरा करता है, तो Certora Prover बिना किसी detected violations के एक सफल verification रन की पुष्टि करेगा, जैसा कि नीचे दी गई छवि (image) में दिखाया गया है:

Verification के परिणाम (results) इस बात की पुष्टि करते हैं कि RareToken contract के सभी functions का परीक्षण totalSupplyIsConstant() rule के विरुद्ध किया गया था। प्रत्येक function के आगे हरे चेकमार्क (✅) यह दर्शाते हैं कि rule हर संभव execution के लिए सही है, जिससे यह सुनिश्चित होता है कि किसी भी function call के तहत totalSupply variable अपरिवर्तित (unchanged) रहता है।

Parametric Rule के Scope को समझना

एक parametric rule के बारे में समझने वाली एक महत्वपूर्ण बात यह है कि इसे एक बार में केवल एक function call के प्रभाव का विश्लेषण (analyze) करने के लिए डिज़ाइन किया गया है। इसका मतलब है कि Prover यह जाँच नहीं कर रहा है कि calls की एक सीरीज़ (श्रृंखला) के बाद क्या होता है—इसका संबंध केवल किसी एक function के single कॉल से है और उसके ठीक बाद contract की state कैसी दिखती है।

यहाँ बताया गया है कि जब Prover एक parametric rule का मूल्यांकन (evaluate) करता है तो क्या होता है:

1. यह एक initial contract state से शुरू होता है—यह किसी भी function के कॉल होने से पहले की state है।
2. यह contract से एक function चुनता है और जाँचता है कि क्या—दी गई preconditions के तहत—कोई ऐसा valid input मौजूद है जो rule के assertions का उल्लंघन (violation) कर सकता है।
3. यह प्रक्रिया contract के प्रत्येक function के लिए दोहराई जाती है।
4. Rule verification को तभी पास (✅) करता है जब किसी भी valid inputs के तहत कोई भी function किसी assertion के विफल (fail) होने का कारण न बने।

Parametric rule की मूल्यांकन (evaluation) प्रक्रिया को अधिक स्पष्ट रूप से समझने के लिए, Counter contract पर विचार करें। इसमें दो external functions शामिल हैं: increment(), जो count को बढ़ाता है, और transferOwnership(), जो owner एड्रेस को अपडेट करता है। Ownership से संबंधित कार्यक्षमता (functionality) केवल अतिरिक्त functions पेश करने के लिए शामिल की गई है, ताकि हम देख सकें कि विभिन्न प्रकार के functions पर लागू होने पर एक parametric rule कैसा व्यवहार करता है।

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

contract Counter {
    uint256 public count;
    address public owner;
    
    // Define custom errors
    error Unauthorized();
    error InvalidAddress();
    
    // Emit events for important state changes
    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);
    event CountUpdated(uint256 newCount);

    constructor() {
        owner = msg.sender;
        emit OwnershipTransferred(address(0), msg.sender);
    }
    
  
  modifier onlyOwner() {

        if (msg.sender != owner) revert Unauthorized();
        _;
    }

    function increment() external {
        count += 1;
        emit CountUpdated(count);
    }

    function transferOwnership(address _newOwner) external onlyOwner {
        if (_newOwner == address(0)) revert InvalidAddress();
        emit OwnershipTransferred(owner, _newOwner);
        owner = _newOwner;
    }
}

अब नीचे दी गई specification पर विचार करें जो counterParametricCall() नामक एक parametric rule को परिभाषित करती है।

Copy
rule counterParametricCall() {
    env e;

    require count(e) == 0;

    method f;
    calldataarg args;

    f(e,args);

    satisfy count(e) == 2 ;
}

चूँकि हमारे rule counterParametricCall() में satisfy स्टेटमेंट satisfy count(e) == 2; शामिल है, हम Prover से पूछ रहे हैं कि क्या ऐसी प्रारंभिक अवस्था (initial state) से शुरू करते हुए जहाँ count 0 है, ऐसी state तक पहुँचने का कम से कम एक संभावित (possible) तरीका है जहाँ count 2 हो।

लेकिन इसमें और भी बहुत कुछ है—rule में require और satisfy स्टेटमेंट्स के बीच एक parametric function call (f(e, args)) भी शामिल है। यह प्रश्न को एक सामान्य reachability जाँच से हटाकर अधिक केंद्रित (focused) क्वेरी में बदल देता है:

“क्या contract में कोई एक ऐसा function f मौजूद है जिसे, जब कुछ valid arguments args के साथ एक बार execute किया जाता है, तो यह state को सीधे count == 0 से count == 2 में बदल (transition) देता है?”

हमारे Counter contract के मामले में, उपलब्ध एकमात्र function increment() है, जो प्रति कॉल काउंटर को 1 से बढ़ाता है। चूँकि कोई भी function एक ही execution में काउंटर को 2 से नहीं बढ़ा सकता है, इसलिए Prover को ऐसा कोई function नहीं मिल सकता जो count(e) == 2 की शर्त (condition) को पूरा करता हो (satisfy करता हो)।

इसलिए, rule verification में विफल (fail) हो जाएगा, जो अपेक्षित और सही परिणाम है—जैसा कि नीचे दर्शाया गया है:

यह ध्यान रखना बहुत महत्वपूर्ण है कि एक parametric rule केवल आइसोलेशन (isolation) में एक external function call के प्रभाव का विश्लेषण करता है। यह calls के सीक्वेंस (क्रम) या एक ही ट्रांजैक्शन (transaction) के भीतर जटिल इंटरैक्शन (complex interactions) की जाँच नहीं करता है। उदाहरण के लिए, जबकि उपरोक्त rule यह साबित करता है कि कोई एक कॉल count == 2 नहीं कर सकती है, एक ट्रांजैक्शन के भीतर count == 2 तक पहुँचना संभव है यदि कोई अन्य smart contract increment() function को लगातार दो बार कॉल करे। उस परिदृश्य (scenario) में एक ट्रांजैक्शन के भीतर शुरू किए गए कई function calls (multiple function calls) शामिल होते हैं, जो इस अध्याय के दायरे (scope) से बाहर है।

हालाँकि, भले ही हम satisfy count(e) == 2 के बजाय satisfy count(e) == 1 चेक करने के लिए rule में ढील दे दें, फिर भी rule पास नहीं होगा, जैसा कि नीचे दिखाया गया है:

ऐसा इसलिए हुआ क्योंकि, background (under the hood) में, एक parametric rule का मूल्यांकन करते समय, Prover contract के प्रत्येक function के लिए rule का एक इंस्टेंस (instance) बनाता है। यह इन rule इंस्टेंस में से प्रत्येक का व्यक्तिगत रूप से assertions के विरुद्ध परीक्षण करता है। Rule verification को केवल तभी पास करता है जब प्रत्येक function इंस्टेंस assert और satisfy स्टेटमेंट्स द्वारा निर्दिष्ट (specified) सभी शर्तों (conditions) को पूरा करता हो। यदि एक भी function मानदंडों (criteria) को पूरा करने में विफल रहता है, तो पूरा rule विफल हो जाता है।

Counter contract में, केवल increment() function ही count variable को modify करता है, जिससे यह एकमात्र ऐसा उम्मीदवार (candidate) बन जाता है जो संभावित रूप से satisfy condition (उदा., count == 1) को पूरा कर सकता है। इसके विपरीत, transferOwnership() और getter functions count() तथा owner() count को बिल्कुल प्रभावित नहीं करते हैं। जब Prover इन functions के लिए rule का मूल्यांकन करता है, तो वह पाता है कि उनमें से कोई भी आवश्यक state परिवर्तन (change) उत्पन्न नहीं कर सकता है। परिणामस्वरूप, उनके rule इंस्टेंस विफल हो जाते हैं, और चूँकि rule के सफल होने के लिए सभी इंस्टेंस का पास होना आवश्यक है, इसलिए पूरा rule verification में विफल हो जाता है।

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

इस प्रकार हम उन smart contract properties को verify करने के लिए एक parametric rule का उपयोग कर सकते हैं जिनके सभी function executions में सत्य (true) रहने की उम्मीद होती है। हालाँकि, ऐसे मामले हो सकते हैं जहाँ हम rule से कुछ functions को बाहर (exclude) करना चाहते हैं या उन्हें अलग तरह से हैंडल करना चाहते हैं। अगले अध्याय में, हम सीखेंगे कि विशिष्ट (specific) function calls के आधार पर constraints को चुनिंदा रूप से (selectively) लागू करने के लिए parametric rules को फाइन-ट्यून (fine-tune) कैसे किया जाए।

यह लेख Certora Prover का उपयोग करके formal verification श्रृंखला का हिस्सा है।