पिछले अध्याय में, हमने non-payable संदर्भों में msg.sender पर ध्यान केंद्रित करके CVL में environment-dependent फ़ंक्शंस के बारे में तर्क (reasoning) करने का तरीका कवर किया था। उन उदाहरणों में, एक्सेस कंट्रोल कॉलर के एड्रेस पर निर्भर करता था। हमने यह भी समझाया कि अप्रत्याशित (unexpected) non-zero msg.value के कारण होने वाले रिवर्ट्स (reverts) को कैसे हैंडल किया जाए।

इस अध्याय में हम निम्नलिखित को कवर करेंगे:

• उन फ़ंक्शंस के लिए रूल्स लिखना जो non-zero पेमेंट की उम्मीद करते हैं (यानी, वे फ़ंक्शंस जिन्हें payable के रूप में मार्क किया गया है)
• अकाउंट बैलेंसेज़ के बारे में assertions कैसे बनाएँ
• वर्तमान कॉन्ट्रैक्ट का बैलेंस कैसे प्राप्त करें, जो Solidity में address(this).balance के समान है

e.msg.sender और e.msg.value (payable)

एक whitelisting कॉन्ट्रैक्ट पर विचार करें जहाँ यूज़र्स register() फ़ंक्शन को कॉल करके रजिस्टर करते हैं, जिसे payable के रूप में मार्क किया गया है, और कम से कम 0.05 ETH भेजते हैं। एक बार रजिस्टर हो जाने पर, whitelisted मैपिंग में इसकी वैल्यू को true पर सेट करके कॉलर के एड्रेस (msg.sender) को whitelisted के रूप में मार्क कर दिया जाता है:

Copy
/// Solidity

contract PayableWhitelist {
    mapping(address => bool) public whitelisted;

    function register() external payable {
        require(msg.value >= 0.05 ether, "whitelist fee is 0.05 eth");
        require(!whitelisted[msg.sender], "already whitelisted");

        whitelisted[msg.sender] = true;
    }

    function isWhitelisted(address _account) external view returns (bool) {
        return whitelisted[_account];
    }
}

हम इस प्रॉपर्टी को formally verify करेंगे: “कॉलर सफलतापूर्वक register() को कॉल कर सकता है, यदि और केवल यदि (if and only if) वे कम से कम 0.05 ETH का भुगतान करते हैं”। इसे verify करने के लिए, हम निम्नलिखित CVL रूल लिखते हैं:

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    register@withrevert(e);
    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

नोट: CVL में घातांक (Exponentiation) के लिए ^_ का उपयोग किया जाता है, जबकि Solidity में_ **_ का उपयोग किया जाता है।_

जैसा कि हम जानते हैं, चूंकि हम biconditional ऑपरेटर का उपयोग कर रहे हैं, इसलिए हमें precondition के माध्यम से अन्य revert केसेस को बाहर (rule out) करना होगा। हम require(!isWhitelisted(e.msg.sender)) को एक precondition के रूप में जोड़ते हैं ताकि उस केस को बाहर किया जा सके जहाँ msg.sender शुरुआत में whitelisted नहीं है।

अब, biconditional assertion के लिए:

assert !lastReverted <=> e.msg.value >= 5 * 10^16.

चूंकि हमने उस केस को बाहर कर दिया है जहाँ सेंडर whitelisted है (require !isWhitelisted(e.msg.sender)), हम उम्मीद करते हैं कि यह VERIFIED होगा, जिसका अर्थ है कि फ़ंक्शन केवल तभी revert नहीं होगा यदि e.msg.value >= 5 * 10^16 हो।

हालाँकि, जैसा कि अक्सर formal verification में होता है, एक अप्रत्याशित (sneaky) counterexample सामने आता है, जो एक violation का कारण बनता है। यह तब होता है जब सेंडर का ETH बैलेंस भेजी जाने वाली निर्धारित राशि से कम होता है या बैलेंस अपर्याप्त (insufficient) होता है:

इसे precondition में require(nativeBalances[e.msg.sender] >= e.msg.value) जोड़कर ठीक किया जा सकता है, जो revert के कारण के रूप में अपर्याप्त बैलेंस को बाहर (rule out) कर देता है।

CVL में nativeBalances

nativeBalances[address] CVL में एक built-in फ़ंक्शन है जो किसी दिए गए एड्रेस का वर्तमान ETH बैलेंस प्राप्त (retrieve) करता है। नीचे, हम यह आवश्यक (require) करते हैं कि सेंडर के लिए nativeBalances कम से कम msg.value जितना बड़ा हो:

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

अब, रूल VERIFIED है:

Prover रन: link

Whitelist Status को Verify करना

अब जब हमने यह verify कर लिया है कि “कॉलर सफलतापूर्वक register() को कॉल कर सकता है, यदि और केवल यदि वे कम से कम 0.05 ETH का भुगतान करते हैं”, तो आइए यह assert करके भी रूल के स्कोप (scope) में सुधार करें कि एक सफल कॉल के बाद कॉलर isWhitelisted हो जाता है।

यहाँ formally verify करने के लिए अपडेटेड प्रॉपर्टी दी गई है: “ट्रांज़ैक्शन सफल होता है यदि और केवल यदि कॉलर कम से कम 0.05 ETH भेजता है और whitelisted हो जाता है।” इसे प्राप्त करने के लिए, हम पिछले रूल का पुन: उपयोग (reuse) कर सकते हैं और एक अतिरिक्त assertion जोड़ सकते हैं: isWhitelisted।

यहाँ अपडेटेड CVL रूल है:

Copy
rule register_payEthToWhitelist_modified(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16 && isWhitelisted(e.msg.sender);
}

उपरोक्त रूल का अर्थ है कि ट्रांज़ैक्शन revert नहीं होता है (!lastReverted) यदि और केवल यदि सेंडर कम से कम 0.05 ETH भेजता है (e.msg.value >= 5 * 10^16) और whitelisted हो जाता है (isWhitelisted(e.msg.sender))।

दूसरे शब्दों में, यदि !lastReverted सत्य (true) है (ट्रांज़ैक्शन सफल रहा), तो दोनों शर्तें — पर्याप्त ETH और whitelisting — लागू होनी चाहिए (must hold)।

यहाँ Prover की रिपोर्ट है और यह VERIFIED है:

Prover रन: link

<=> के बजाय => के साथ Preconditions में ढील देना (Relaxing)

एक अन्य दृष्टिकोण implication ऑपरेटर का उपयोग करना है। यदि आपका लक्ष्य केवल यह जाँचना है कि जब कोई गलत msg.value भेजी जाती है तो फ़ंक्शन revert हो जाता है, तो निम्नलिखित रूल पर्याप्त है। यह रूल अन्य revert के कारणों को रोकता (preclude) नहीं है, जैसे कि सेंडर के पास पर्याप्त बैलेंस का न होना। यह केवल इतना कहता है कि यदि 0.05 ether से कम भेजा जाता है, तो यह निश्चित रूप से (definitely) revert होता है।

Copy
rule register_payEthToWhitelist_implication(env e) {
    register@withrevert(e);
    assert e.msg.value < 5 * 10^16 => lastReverted;
}

यदि हम इस रूल का उपयोग करते हैं, तो हम देखते हैं कि यह VERIFIED है:

Prover रन: link

ETH Balance Transfers को Verify करना और Self-Transfer Corner Case

मान लीजिए कि हम उन बैलेंस अपडेट्स को formally verify करना चाहते हैं जहाँ msg.sender का बैलेंस msg.value से घट जाता है और कॉन्ट्रैक्ट का बैलेंस समान राशि (same amount) से बढ़ जाता है।

नीचे CVL रूल दिया गया है, जिसे अगले भाग में समझाया जाएगा:

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

currentContract

उपरोक्त रूल में, हम currentContract का पूर्व ETH बैलेंस (balanceBefore) और अंतिम बैलेंस (balanceAfter) प्राप्त करते हैं। currentContract एक built-in वेरिएबल है जो उस कॉन्ट्रैक्ट को संदर्भित (refer) करता है जिसे verify किया जा रहा है। इस वेरिएबल को nativeBalances[currentContract] में पास करने से उक्त कॉन्ट्रैक्ट का बैलेंस प्राप्त होता है। इन retrieval कॉल्स के बीच, register() फ़ंक्शन को invoke किया जाता है, इसलिए हम उम्मीद करते हैं कि बैलेंस msg.value के बराबर राशि से बढ़ जाएगा।

एक अप्रत्याशित (unexpected) counterexample के कारण यह रूल विफल हो जाएगा। Prover एक counterexample जनरेट करेगा जहाँ msg.sender == currentContract होगा। Prover कॉन्ट्रैक्ट के खुद को कॉल करने वाले केसेस सहित सभी संभावित परिदृश्यों (scenarios) का पता लगाता है।

यह दर्शाता है कि कॉन्ट्रैक्ट ने किसी बाहरी सेंडर से नया ETH प्राप्त करने के बजाय खुद को ही ETH भेजा है। परिणामस्वरूप, बैलेंस वास्तव में उम्मीद के मुताबिक नहीं बढ़ा (क्योंकि खुद को ETH भेजने से कुल बैलेंस नहीं बदलता है), जिसके कारण balanceAfter == balanceBefore + e.msg.value assertion विफल हो जाता है।

इस समस्या को हल करने के लिए, चूंकि msg.sender स्वयं कॉन्ट्रैक्ट (currentContract) नहीं होना चाहिए, इसलिए हमें एक precondition: require(e.msg.sender != currentContract) जोड़कर ETH बैलेंस में बदलाव को verify करते समय self-transfers को फ़िल्टर (बाहर) करने की आवश्यकता है।

हालाँकि, एक चेतावनी (caveat) है: वास्तविक प्रोजेक्ट्स में, यह सुनिश्चित करें कि कॉन्ट्रैक्ट अपने स्वयं के फ़ंक्शंस को कॉल नहीं कर सकता है, क्योंकि कुछ मामलों में अभी भी self-calls हो सकती हैं। यदि ठीक से जाँच नहीं की गई, तो यह किसी बग (bug) को छिपा सकता है।

यहाँ सही किया गया रूल और Prover रिपोर्ट दी गई है। उम्मीद के मुताबिक, यह VERIFIED है:

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];

    require e.msg.sender != currentContract;
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

Prover रन: link

<=> और || का उपयोग करके सभी Revert Cases को Verify करना

मान लीजिए कि हम यह verify करना चाहते हैं कि revert होने के हर संभव कारण को स्पष्ट रूप से (explicitly) शामिल (account for) किया गया है। हम assertion को एक biconditional (<=>) के रूप में व्यक्त कर सकते हैं और disjunctively (ORs || का उपयोग करके) सभी revert केसेस को सूचीबद्ध कर सकते हैं।

नीचे दिया गया रूल बताता है कि revert होने के एकमात्र संभावित कारण निम्नलिखित हैं:

• सेंडर पहले से ही whitelisted है
• सेंडर का बैलेंस अपर्याप्त (insufficient) है
• सेंडर ने पर्याप्त फ़ंड ट्रांसफर नहीं किया

यदि register() किसी अन्य कारण से revert होता है, तो हमें एक assert violation प्राप्त होगा।

यहाँ रूल है:

Copy
rule register_allRevertCases(env e) {
    bool wasWhitelisted = isWhitelisted(e.msg.sender);
    mathint balanceBefore = nativeBalances[e.msg.sender];

    register@withrevert(e);

    assert lastReverted <=> (
        wasWhitelisted ||              // sender already whitelisted
        balanceBefore < e.msg.value || // sender's balance insufficient
        e.msg.value < 5 * 10^16        // sender's transfer amount insufficient 
    );
}

उम्मीद के मुताबिक, रूल VERIFIED है:

Prover रन: link

सारांश (Summary)

• CVL में, environment वेरिएबल e.msg.value का उपयोग यह व्यक्त करने और verify करने के लिए किया जाता है कि कोई payable फ़ंक्शन सफल होगा या revert होगा, आमतौर पर न्यूनतम या सटीक आवश्यक राशि (required amount) को assert करके।
• nativeBalances[address] एक built-in फ़ंक्शन है जो किसी दिए गए एड्रेस का वर्तमान ETH बैलेंस प्राप्त करता है और इसका उपयोग बैलेंस में बदलाव की जाँच करके ट्रांसफर्स को verify करने के लिए किया जा सकता है।
• currentContract एक built-in वेरिएबल है जो उस कॉन्ट्रैक्ट को संदर्भित (refer) करता है जिसे verify किया जा रहा है।
• Prover द्वारा टेस्ट केसेस में Self-calls शामिल की जाती हैं, इसलिए हमारे उदाहरण में, हम false counterexamples से बचने के लिए require(e.msg.sender != currentContract) जोड़कर उन्हें बाहर (rule out) करते हैं; सावधान रहें, क्योंकि self-calls व्यावहारिक (plausible) हो सकती हैं और वास्तविक दुनिया के कॉन्ट्रैक्ट्स में असली बग्स को उजागर कर सकती हैं।

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