परिचय

इस अध्याय में, हम Solmate के ERC-20 इम्प्लीमेंटेशन को formally verify करेंगे, जिसमें निम्नलिखित शामिल हैं:

• स्टैंडर्ड state-changing फंक्शन्स: transfer(), approve(), transferFrom()
• स्टैंडर्ड view फंक्शन्स: totalSupply(), balanceOf(), allowance()
• एक्सटेंडेड internal फंक्शन्स: _mint(), _burn()

ध्यान दें कि हालांकि Solmate के ERC-20 इम्प्लीमेंटेशन में एक permit() फंक्शन शामिल है, हम इसे जानबूझकर छोड़ रहे हैं क्योंकि क्रिप्टोग्राफ़िक सिग्नेचर को formally verify करना अभी इस सीरीज़ में कवर नहीं किया गया है।

Solmate के ERC-20 टोकन को जो बात दिलचस्प बनाती है, वह है total supply और balances में बदलाव के दौरान गैस (gas) बचाने के लिए unchecked ब्लॉक्स का उपयोग। चूंकि unchecked ब्लॉक्स Solidity के बिल्ट-इन ओवरफ्लो (overflow) चेक को बायपास कर देते हैं, इसलिए गणितीय रूप से यह साबित करने के लिए formal verification आवश्यक है कि ओवरफ्लो नहीं हो सकता है।

यहाँ केवल permit() फंक्शन को हटाकर, सरल किया गया Solmate ERC-20 इम्प्लीमेंटेशन दिया गया है:

Copy
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity >=0.8.0;

/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
abstract contract ERC20 {
    /*//////////////////////////////////////////////////////////////
                                 EVENTS
    //////////////////////////////////////////////////////////////*/

    event Transfer(address indexed from, address indexed to, uint256 amount);

    event Approval(address indexed owner, address indexed spender, uint256 amount);

    /*//////////////////////////////////////////////////////////////
                            METADATA STORAGE
    //////////////////////////////////////////////////////////////*/

    string public name;

    string public symbol;

    uint8 public immutable decimals;

    /*//////////////////////////////////////////////////////////////
                              ERC20 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 public totalSupply;

    mapping(address => uint256) public balanceOf;

    mapping(address => mapping(address => uint256)) public allowance;

    /*//////////////////////////////////////////////////////////////
                               CONSTRUCTOR
    //////////////////////////////////////////////////////////////*/

    constructor(
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) {
        name = _name;
        symbol = _symbol;
        decimals = _decimals;
    }

    /*//////////////////////////////////////////////////////////////
                               ERC20 LOGIC
    //////////////////////////////////////////////////////////////*/

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        allowance[msg.sender][spender] = amount;

        emit Approval(msg.sender, spender, amount);

        return true;
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        balanceOf[msg.sender] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(msg.sender, to, amount);

        return true;
    }

    function transferFrom(
        address from,
        address to,
        uint256 amount
    ) public virtual returns (bool) {
        uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

        if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

        balanceOf[from] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                        INTERNAL MINT/BURN LOGIC
    //////////////////////////////////////////////////////////////*/

    function _mint(address to, uint256 amount) internal virtual {
        totalSupply += amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(address(0), to, amount);
    }

    function _burn(address from, uint256 amount) internal virtual {
        balanceOf[from] -= amount;

        // Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

        emit Transfer(from, address(0), amount);
    }
}

ऊपर दिया गया ERC-20 इम्प्लीमेंटेशन एक abstract कॉन्ट्रैक्ट है, जिसे concrete बनाने के लिए एक इनहेरिट करने वाले (inheriting) कॉन्ट्रैक्ट की आवश्यकता होती है। हमें _mint() और _burn() को external फंक्शन्स के माध्यम से एक्सपोज़ करने की भी आवश्यकता है ताकि वेरिफिकेशन के दौरान Prover उन्हें कॉल (invoke) कर सके। इन दोनों आवश्यकताओं को पूरा करने के लिए, हम एक harness कॉन्ट्रैक्ट का उपयोग करते हैं।

एक harness कॉन्ट्रैक्ट, जिस कॉन्ट्रैक्ट का वेरिफिकेशन हो रहा होता है, उसे इनहेरिट करता है ताकि internal फंक्शन्स को external फंक्शन्स के रूप में रैप करके Prover के लिए एक्सेसिबल बनाया जा सके। यह helper view या pure फंक्शन्स को भी परिभाषित कर सकता है जो रूल और इनवैरिएंट (invariant) लॉजिक को आसान बनाने के लिए स्टेट क्वेरीज़ और यूटिलिटी कम्प्यूटेशन्स प्रदान करते हैं।

इस स्पेसिफिकेशन के लिए, harness एक मिनिमल कॉन्ट्रैक्ट है जो abstract ERC-20 इम्प्लीमेंटेशन को इनहेरिट करता है ताकि एक concrete कॉन्ट्रैक्ट प्रदान किया जा सके और वेरिफिकेशन के लिए इसके internal फंक्शन्स (_mint() और _burn()) को एक्सेसिबल बनाया जा सके।

यहाँ harness कॉन्ट्रैक्ट दिया गया है:

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

import "src/Solmate/ERC20.sol";

contract ERC20Harness is ERC20 {    
    constructor (
        string memory _name, 
        string memory _symbol, 
        uint8 _decimals
    ) ERC20(_name, _symbol, _decimals) {}
    
    /// Left without access controls; integrators are expected to implement their own.
    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
	
    /// Left without access controls; integrators are expected to implement their own.
    function burn(address _from, uint256 _amount) external {
        _burn(_from, _amount);
    }
}

ERC-20 प्रॉपर्टीज़ को formally verify करने के लिए सिक्वेंस्ड (Sequenced) दृष्टिकोण

इस अध्याय में, हम ERC-20 कॉन्ट्रैक्ट की प्रॉपर्टीज़ को formally verify करने के लिए एक सिक्वेंस्ड (sequenced) दृष्टिकोण अपनाते हैं। रूपरेखा इस प्रकार है:

• इंटेंट (intent) क्या है? यूज़र क्या चाहता है?
  • कौन सा/से फंक्शन इस इंटेंट को पूरा करते हैं?
    • यदि कॉल सफल होती है, तो इच्छित स्टेट चेंज (state change) कैसे परिलक्षित (reflect) होता है?
    • यदि कॉल सफल होती है, तो शामिल न होने वाली पार्टीज़ के लिए कौन से अनपेक्षित साइड इफेक्ट्स या स्टेट चेंज नहीं होने चाहिए?
    • यदि कॉल रिवर्ट (revert) होती है, तो रिवर्ट का कारण क्या है?
• कौन से इनवैरिएंट्स (invariants) हमेशा लागू होने चाहिए?
• किन अनधिकृत एक्शन्स (फंक्शन्स या कॉलर्स द्वारा) की अनुमति नहीं होनी चाहिए?

इस प्रक्रिया को नीचे दिए गए आरेख (diagram) में दर्शाया गया है:

फिर, हम नीचे दिए गए नंबर वाले क्रम में दिखाए गए प्रत्येक चरण (step) से गुज़रते हैं:

1. फंक्शन की सत्यता (correctness) को वेरिफाई करना (कॉल्स सफल होती हैं या रिवर्ट होती हैं)

transfer()

आइए टोकन भेजने के इंटेंट से शुरू करते हैं — हम यह वेरिफाई करते हैं कि जब कोई सेंडर (sender) टोकन ट्रांसफर करता है, तो रिसीवर (receiver) को सटीक रूप से निर्दिष्ट (specified) अमाउंट प्राप्त होता है। यह transfer() फंक्शन के माध्यम से प्राप्त किया जाता है।

यहाँ transfer() फंक्शन का इम्प्लीमेंटेशन दिया गया है:

Copy
function transfer(address to, uint256 amount) public virtual returns (bool) {
    balanceOf[msg.sender] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

यहाँ वह CVL रूल दिया गया है जो वेरिफाई करता है कि सेंडर का बैलेंस कम होता है और रिसीवर का बैलेंस सटीक अमाउंट से बढ़ता है:

Copy
rule transfer_effectOnBalances(env e) {
    address receiver;
    uint256 amount;

    require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // will be replaced by an invariant
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

आइए इस रूल को और स्पष्ट करते हैं।

प्रीकंडीशन (precondition) Prover को ऐसे बैलेंस असाइन करने से रोकती है जिनका योग (sum) max_uint256 की सीमा से अधिक हो, जैसा कि नीचे देखा गया है:

Copy
require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // will be replaced by an invariant

यह आवश्यक है क्योंकि जब transfer() फंक्शन ट्रांसफर अमाउंट को balanceOf[address] में जोड़ता है तो यह एक unchecked ब्लॉक का उपयोग करता है, जिससे Prover ओवरफ्लो को “संभव” मानता है और फ़ॉल्स पॉज़िटिव्स (false positives) रिपोर्ट करता है।

हालाँकि, क्योंकि यह प्रीकंडीशन वैल्यूज़ को max_uint256 तक सीमित करती है, Prover उन ओवरफ्लो स्थितियों का परीक्षण नहीं कर सकता है जो वास्तव में हो सकती हैं, जो ओवरफ्लो बग्स को छिपा सकता है। इसलिए, इसे एक वेरीफाइड इनवैरिएंट के साथ औपचारिक रूप से खारिज किया जाना चाहिए, जिसे हम “requireInvariant” अनुभाग में संबोधित करेंगे।

प्रीकंडीशन के बाद, हम निम्नलिखित चरणों के साथ आगे बढ़ते हैं:

• transfer() कॉल से पहले सेंडर और रिसीवर के बैलेंस को रिकॉर्ड करें।
• transfer() कॉल को इनवोक (invoke) करें।
• कॉल के बाद सेंडर और रिसीवर के बैलेंस को फिर से रिकॉर्ड करें। हम इन वैल्यूज़ का उपयोग assertion में सेंडर और रिसीवर दोनों के बैलेंस परिवर्तन के बारे में तर्क (reasoning) करने के लिए करेंगे।

Copy
mathint senderBalanceBefore = balanceOf(e.msg.sender);
mathint receiverBalanceBefore = balanceOf(receiver);

transfer(e, receiver, amount);

mathint senderBalanceAfter = balanceOf(e.msg.sender);
mathint receiverBalanceAfter = balanceOf(receiver);

अब, assertions:

• यदि सेंडर और रिसीवर अलग-अलग हैं, तो हम यह assert करते हैं कि:
  • सेंडर का बैलेंस amount से कम हो जाता है।
  • रिसीवर का बैलेंस amount से बढ़ जाता है।
• यदि सेंडर और रिसीवर एक ही हैं, तो हम assert करते हैं कि बैलेंस अपरिवर्तित (unchanged) रहते हैं:

Copy
if (receiver != e.msg.sender) {
    assert senderBalanceAfter == senderBalanceBefore - amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
} 
else {
    assert senderBalanceAfter == senderBalanceBefore;
    assert receiverBalanceAfter == receiverBalanceBefore;
}

यह assertion बिना किसी कटौती के डायरेक्ट वैल्यू ट्रांसफर की पुष्टि करता है, जैसा कि इस Prover run में दिखाया गया है।

transfer() रिवर्ट्स (reverts)

हमने अभी सफल ट्रांसफर पाथ (path) को कवर किया है। आगे, हम यह वेरिफाई करते हैं कि transfer() विफलता (failure) की स्थितियों में रिवर्ट होता है।

निम्नलिखित CVL रूल assertions में सभी रिवर्ट स्थितियों को ध्यान में रखता है। यह बायकंडीशनल ऑपरेटर (<=>) का उपयोग यह बताने के लिए करता है कि रिवर्ट केवल और केवल तभी होता है जब सूचीबद्ध (listed) शर्तों में से कोई एक सत्य हो। ये शर्तें हैं:

• सेंडर के पास पर्याप्त बैलेंस नहीं है।
• नॉन-पेएबल (non-payable) फंक्शन कॉल के साथ ETH भेजा गया है।

Copy
rule transfer_reverts(env e) {
    address receiver;
    uint256 amount;

    mathint senderBalance = balanceOf(e.msg.sender);

    transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        senderBalance < amount || // sender doesn't have enough balance
        e.msg.value != 0 // sending ETH with a call to transfer (non-payable)
    );
}

इस रूल के लिए, हम कोई प्रीकंडीशन परिभाषित नहीं करते हैं, इसलिए हम सीधे transfer कॉल से पहले स्टेट को रिकॉर्ड करने पर जाते हैं। निम्नलिखित लाइन transfer कॉल से पहले की वैल्यू को कैप्चर करती है:

Copy
mathint senderBalance = balanceOf(e.msg.sender);

Assertion के लिए, रिवर्ट होने के कारणों के रूप में केवल दो परिदृश्य (scenarios) सूचीबद्ध हैं। पहला तब होता है जब सेंडर का बैलेंस ट्रांसफर किए जाने वाले अमाउंट से कम होता है, क्योंकि किसी सेंडर को अपने पास मौजूद टोकन से अधिक भेजने में सक्षम नहीं होना चाहिए:

Copy
assert isLastReverted <=> (
    senderBalance < amount || // not enough balance
    e.msg.value != 0
);

दूसरा मामला (e.msg.value != 0) रिवर्ट का कारण बनता है क्योंकि फंक्शन नॉन-पेएबल है। कोई भी नॉनजीरो msg.value इसके विफल होने का कारण बनता है। यह नॉन-पेएबल फंक्शन्स के लिए एक रिवर्ट कंडीशन है और ERC-20 के formal verification के दौरान बार-बार दिखाई देगी।

Assertion यह गारंटी देने के लिए बायकंडीशनल ऑपरेटर का उपयोग करता है कि फंक्शन केवल और केवल तभी रिवर्ट होता है जब दोनों मामलों में से कोई एक होता है। इसका मतलब है कि किसी अन्य शर्त के कारण फंक्शन को रिवर्ट नहीं होना चाहिए। यहाँ Prover run दिया गया है।

transferFrom()

यहाँ, हम यह वेरिफाई करते हैं कि जब कोई अधिकृत (authorized) spender किसी होल्डर की ओर से टोकन ट्रांसफर करता है, तो रिसीवर को सटीक रूप से निर्दिष्ट अमाउंट प्राप्त होता है। यह नीचे दिए गए Solidity इम्प्लीमेंटेशन में दिखाए गए अनुसार transferFrom() फंक्शन का उपयोग करके किया जाता है। इस ट्रांसफर से allowance में होने वाले बदलाव का विश्लेषण बाद के अनुभाग में किया जाएगा।

Copy
function transferFrom(
    address from,
    address to,
    uint256 amount
) public virtual returns (bool) {
    uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

    if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

    balanceOf[from] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(from, to, amount);

    return true;
}

निम्नलिखित रूल लगभग transfer_effectOnBalances रूल के समान है — एकमात्र अंतर यह है कि यह transferFrom() को कॉल करता है। यह निम्नलिखित कार्य करता है:

• प्रीकंडीशन्स (Preconditions): होल्डर और रिसीवर के बैलेंस के योग को max_uint256 के भीतर रखने के लिए सीमित करता है ताकि Prover को unchecked ब्लॉक में ओवरफ्लो परिदृश्यों को एक्सप्लोर करने से रोका जा सके।
• प्री-कॉल (Pre-call) और पोस्ट-कॉल (post-call) स्टेट्स: transferFrom() कॉल से पहले और बाद में दोनों अकाउंट्स के बैलेंस को रिकॉर्ड करता है ताकि हम assertions में सटीक बैलेंस परिवर्तन को वेरिफाई कर सकें।
• Assertions:
  • यदि receiver != holder, तो assert करें कि उनके बैलेंस में amount का अंतर है।
  • यदि receiver == holder, तो assert करें कि बैलेंस अपरिवर्तित रहता है।

Copy
rule transferFrom_effectOnBalances(env e) {
    address holder;
    address receiver;
    uint256 amount;
    
    require balanceOf(holder) + balanceOf(receiver) <= max_uint256; // will be formally verified later

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

Prover run देखें।

transferFrom() रिवर्ट्स (reverts)

transferFrom() रिवर्ट रूल पैटर्न भी transfer() रूल के समान है, सिवाय इसके कि इसमें spender से जुड़ा एक अतिरिक्त मामला शामिल है। जैसा कि नीचे दिखाया गया है, यदि spender के पास पर्याप्त allowance नहीं है (अर्थात, यदि spenderAllowance < amount), तो ट्रांजेक्शन रिवर्ट हो जाता है:

Copy
rule transferFrom_reverts(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint holderBalance = balanceOf(holder);
    mathint spenderAllowance = allowance(holder, e.msg.sender); 
 
 

    transferFrom@withrevert(e, holder, receiver, amount); // spender is the msg.sender
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        holderBalance < amount || 
        spenderAllowance < amount || 
        e.msg.value != 0 
    );
}

अन्य सभी रिवर्ट परिदृश्य transfer() रूल के समान ही हैं। यहाँ Prover run दिया गया है।

allowance में बदलाव

जब कोई transferFrom() कॉल सफल होती है, तो spender के लिए होल्डर द्वारा अप्रूव्ड (approved) allowance बदल जाता है। transferFrom() इम्प्लीमेंटेशन में यह कंडीशन (conditional) शामिल है:

Copy
if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

इसका मतलब यह है कि यदि वर्तमान allowance अधिकतम uint256 वैल्यू पर सेट नहीं है, तो खर्च किया गया अमाउंट उसमें से काट लिया जाता है। यदि allowance अधिकतम पर सेट है, तो यह इनफिनिट (infinite) allowance की तरह व्यवहार करता है और अपरिवर्तित रहता है।

यह व्यवहार नीचे दिखाए गए CVL रूल के assertion अनुभाग में कैप्चर किया गया है:

Copy
rule transferFrom_allowanceChange(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint spenderAllowanceBefore = allowance(holder, e.msg.sender);

    transferFrom(e, holder, receiver, amount);
    mathint spenderAllowanceAfter = allowance(holder, e.msg.sender);

    if (spenderAllowanceBefore != max_uint256) {
        assert spenderAllowanceAfter == spenderAllowanceBefore - amount;
    }
    else {
        assert spenderAllowanceAfter == spenderAllowanceBefore;
    }
}

Prover run: link

approve()

transferFrom() फंक्शन के भीतर allowances में से कटौती की जाती है, लेकिन वास्तविक allowance अप्रूवल approve() फंक्शन में सेट किया जाता है। नीचे इसका इम्प्लीमेंटेशन दिया गया है:

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount;

    emit Approval(msg.sender, spender, amount);

    return true;
}

allowance वेरिएबल एक public, नेस्टेड (nested) मैपिंग है। इसलिए, Solidity स्वचालित रूप से एक getter फंक्शन जनरेट करता है, जो इसे सीधे CVL (allowance(e.msg.sender, spender)) में कॉल करने की अनुमति देता है:

Copy
rule approve_spenderAllowance(env e) {
    address spender;
    uint256 amount;

    approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;

    mathint approvedAmountAfter = allowance(e.msg.sender, spender);

    assert !isReverted => approvedAmountAfter == amount;
    assert isReverted <=> e.msg.value != 0;
}

Prover run: link

संक्षिप्तता के लिए, उपरोक्त रूल सफल और रिवर्टिंग दोनों मामलों को जोड़ता है, जिसमें प्रत्येक के लिए अलग-अलग रूल बनाने या if/else ब्लॉक का उपयोग करने के बजाय इम्प्लीकेशन (implication) और बायकंडीशनल ऑपरेटर का उपयोग किया गया है।

approve() फंक्शन को env e कॉन्टेक्स्ट के भीतर कॉल किया जाना चाहिए क्योंकि यह ग्लोबल एनवायरनमेंट वेरिएबल्स जैसे msg.sender और msg.value पर निर्भर करता है। विशेष रूप से, फंक्शन यह निर्धारित करने के लिए msg.sender का उपयोग करता है कि कौन सा एड्रेस spender के लिए allowance सेट कर रहा है:

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount; // relies on msg.sender
    ...
}

अब assertion के लिए:

• यदि फंक्शन कॉल सफल होती है, तो allowance निर्दिष्ट अमाउंट पर सेट हो जाता है।
• फंक्शन केवल और केवल तभी रिवर्ट होता है जब e.msg.value नॉनजीरो होता है, जिसका अर्थ है कि approve फंक्शन कॉल के साथ ETH भेजा गया था।

Copy
assert !isReverted => approvedAmountAfter == amount;
assert isReverted <=> e.msg.value != 0;

transfer(), transferFrom() और approve() एक सफल कॉल पर true रिटर्न करते हैं

उनके state-changing ऑपरेशन्स के अलावा, transfer(), transferFrom() और approve() को सफल एक्ज़ीक्यूशन पर true रिटर्न करना चाहिए, जैसा कि ERC-20 मानक (standard) द्वारा आवश्यक है।

निम्नलिखित रूल्स अपने संबंधित फंक्शन्स को @withrevert के साथ कॉल करते हैं ताकि यह कैप्चर किया जा सके कि क्या वे रिवर्ट होते हैं, परिणाम को isLastReverted में स्टोर करते हैं, और यह assert करते हैं कि यदि कॉल रिवर्ट नहीं हुई, तो उसे true रिटर्न करना चाहिए:

Copy
rule transfer_successReturnsTrue(env e) {
    address receiver;
    uint256 amount;

    bool retVal = transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule transferFrom_successReturnsTrue(env e) {
    address holder;
    address receiver;
    uint256 amount;

    bool retVal = transferFrom@withrevert(e, holder, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule approve_successReturnsTrue(env e) {
    address spender;
    uint256 amount;

    bool retVal = approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;
    
    assert !isReverted => (retVal == true);
}

Prover run: link

ये रूल्स वेरिफाई करते हैं कि transfer(), transferFrom() और approve() सफल कॉल्स पर true रिटर्न करते हैं।

mint()

मिंटिंग (minting) का इंटेंट total supply बढ़ाना है। साथ ही, नए मिंट किए गए टोकन एक रिसीवर को असाइन किए जाते हैं, जिससे उनका बैलेंस बढ़ जाता है। नीचे दिया गया Solidity इम्प्लीमेंटेशन दिखाता है कि totalSupply और balanceOf[to] दोनों को amount से बढ़ाया जा रहा है:

Copy
function _mint(address to, uint256 amount) internal virtual {
    totalSupply += amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }
    ...
}

balanceOf[address] में वृद्धि एक unchecked ब्लॉक के अंदर होती है, जबकि totalSupply में वृद्धि unchecked ब्लॉक के बाहर होती है और Solidity कंपाइलर के ओवरफ्लो चेक द्वारा सुरक्षित होती है।

unchecked ब्लॉक के कारण, Prover बैलेंस ओवरफ्लो की संभावना का एक्सप्लोर करता है, भले ही यह वास्तव में नहीं हो सकता है क्योंकि बैलेंस totalSupply के साथ कदम मिलाकर बढ़ते हैं। फ़ॉल्स पॉज़िटिव्स को रोकने के लिए, हम require totalSupply() >= balanceOf(receiver) प्रीकंडीशन जोड़ते हैं।

यहाँ वह CVL रूल दिया गया है जो total supply में वृद्धि और रिसीवर के बैलेंस में संबंधित वृद्धि दोनों को कैप्चर करता है:

Copy
rule mint_increasesTotalSupplyAndBalance() {
    address receiver;
    uint256 amount;

    require totalSupply() >= balanceOf(receiver); // will be replaced by an invariant

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}

Prover run: link

स्थापित पैटर्न का पालन करते हुए, हम mint() मेथड कॉल से पहले और बाद की स्टेट को कैप्चर करते हैं:

Copy
mathint totalSupplyBefore = totalSupply();
mathint receiverBalanceBefore = balanceOf(receiver);

mint(receiver, amount);

mathint totalSupplyAfter = totalSupply();
mathint receiverBalanceAfter = balanceOf(receiver);

और अब assertion, जहाँ total supply में वृद्धि और रिसीवर के बैलेंस में संबंधित वृद्धि दोनों amount के बराबर हैं:

Copy
assert totalSupplyAfter == totalSupplyBefore + amount;
assert receiverBalanceAfter == receiverBalanceBefore + amount;

mint() रिवर्ट्स (reverts)

mint() फंक्शन केवल और केवल तभी रिवर्ट होता है जब total supply और मिंट अमाउंट का योग max_uint256 से अधिक हो जाता है। यह एक ओवरफ्लो परिदृश्य को दर्शाता है। यहाँ वह CVL रूल दिया गया है जो इस व्यवहार को कैप्चर करता है:

Copy
rule mint_reverts() {
    address receiver;
    uint256 amount;

    mathint totalSupply = totalSupply();

    mint@withrevert(receiver, amount);
    bool isReverted = lastReverted;

    assert isReverted <=> totalSupply + amount > max_uint256;
}

Prover run: link

burn()

जहाँ मिंटिंग total supply को बढ़ाती है, वहीं बर्निंग (burning) का इंटेंट इसे कम करना है। प्रत्येक बर्न (burn) ऑपरेशन total supply और टोकन ओनर (owner) के बैलेंस दोनों को कम करता है।

यहाँ इम्प्लीमेंटेशन दिया गया है:

Copy
function _burn(address from, uint256 amount) internal virtual {
    balanceOf[from] -= amount;

    // Cannot underflow because a user's balance
    // will never be larger than the total supply.
    unchecked {
        totalSupply -= amount;
    }

    emit Transfer(from, address(0), amount);
}

यहाँ वह रूल दिया गया है जो total supply में कमी और टोकन ओनर के बैलेंस में कमी दोनों को कैप्चर करता है:

Copy
rule burn_decreasesTotalSupplyAndBalance() {
    address holder;
    uint256 amount;
			
	require totalSupply() >= balanceOf(holder); // will be replaced by an invariant
		
    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover run: link

_burn() फंक्शन में, ऑपरेशन totalSupply -= amount एक unchecked ब्लॉक के अंदर है। इसलिए, Prover अंडरफ्लो (underflow) की संभावना को एक्सप्लोर करता है, भले ही यह वास्तव में नहीं हो सकता है। इसे रोकने के लिए, हम रूल में require totalSupply() >= balanceOf(holder) प्रीकंडीशन जोड़ते हैं।

बाकी कोड के लिए, पैटर्न mint() के समान ही है, सिवाय इसके कि बैलेंस और total supply दोनों निर्दिष्ट अमाउंट से कम हो जाते हैं, जैसा कि बर्निंग के समय अपेक्षित होता है।

burn() रिवर्ट्स (reverts)

burn() फंक्शन केवल और केवल तभी रिवर्ट होता है जब होल्डर का बैलेंस बर्न किए जाने वाले अमाउंट से कम होता है। यह Solidity द्वारा लागू किया गया एक सुरक्षा चेक है जो तब रिवर्ट को ट्रिगर करता है जब balanceOf[from] -= amount (एक unchecked ब्लॉक के बाहर एग्ज़ीक्यूट किया गया) उपलब्ध बैलेंस से अधिक घटाने का प्रयास करता है।

यहाँ वह CVL रूल दिया गया है जो इस व्यवहार को वेरिफाई करता है:

Copy
rule burn_reverts(env e) {
	address holder;
	uint256 amount;

	mathint holderBalance = balanceOf(holder);

	burn@withrevert(holder, amount);
	bool isReverted = lastReverted;

	assert isReverted <=> holderBalance < amount;
}

Prover run: link

2. transfer, transferFrom, mint और burn के अनपेक्षित साइड इफेक्ट्स

यह वेरिफाई करने के बाद कि फंक्शन्स सफल और रिवर्ट दोनों परिदृश्यों में सही ढंग से व्यवहार करते हैं, अब हम यह वेरिफाई करते हैं कि शामिल न होने वाली पार्टीज़ के लिए कोई अनपेक्षित साइड इफेक्ट्स या स्टेट चेंज नहीं हैं।

एक फंक्शन अनजाने में उन अकाउंट्स के लिए स्टोरेज में बदलाव कर सकता है जो ऑपरेशन में शामिल नहीं हैं। इस कॉन्ट्रैक्ट के लिए, हम formally verify करते हैं कि किसी भी शामिल न होने वाले अकाउंट का बैलेंस transfer(), transferFrom(), mint(), या burn() द्वारा संशोधित नहीं किया गया है।

प्रत्येक रूल समान पैटर्न का पालन करता है: हम एक एड्रेस को uninvolved के रूप में नामित करते हैं (require स्टेटमेंट्स के माध्यम से), ऑपरेशन से पहले उसके बैलेंस को कैप्चर करते हैं, फंक्शन को एग्ज़ीक्यूट करते हैं, फिर assert करते हैं कि बैलेंस अपरिवर्तित रहता है। यह साबित करता है कि केवल आर्गुमेंट्स के रूप में स्पष्ट रूप से पास किए गए अकाउंट्स ही प्रभावित होते हैं:

Copy
rule noUninvolvedBalancesAreAffectedByDirectTransfer(env e) {
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != e.msg.sender;

    mathint otherBalanceBefore = balanceOf(other);
    transfer(e, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByTransferFrom(env e) {
    address holder;
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != holder;

    mathint otherBalanceBefore = balanceOf(other);
    transferFrom(e, holder, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByMint() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    mint(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByBurn() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    burn(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

Prover run: link

3. इनवैरिएंट्स (Invariants)

अब जब हमने सफल और रिवर्टिंग दोनों पाथ्स को वेरिफाई कर लिया है, और यह भी कि कोई अनपेक्षित साइड इफेक्ट नहीं होता है, हम इनवैरिएंट्स पर आगे बढ़ सकते हैं — ऐसी शर्तें जो हमेशा लागू होनी चाहिए, चाहे कौन सा फंक्शन कॉल किया गया हो, कौन से आर्गुमेंट्स उपयोग किए गए हों, या सीक्वेंस में कितनी वैलिड कॉल्स की गई हों।

बैलेंस का योग total supply के बराबर होना चाहिए

किसी भी परिस्थिति में सभी बैलेंस का योग total supply से भिन्न नहीं होना चाहिए, क्योंकि कोई भी भिन्नता (divergence) यह दर्शाती है कि टोकन mint() या burn() के बाहर बनाए या नष्ट किए गए हैं— या तो यूज़र्स को वास्तव में मौजूद टोकन से अधिक दे रहे हैं या सिस्टम से टोकन गायब कर रहे हैं। निम्नलिखित CVL स्पेसिफिकेशन औपचारिक रूप से इस इनवैरिएंट को वेरिफाई करता है:

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

Prover run: link

आइए आगे चर्चा करते हैं।

पहला ब्लॉक एक ghost वेरिएबल g_sumOfBalances को mathint के रूप में डिक्लेयर (declare) करता है और इसे शून्य (zero) पर इनिशियलाइज़ (initialize) करता है। इस इनिशियलाइज़ेशन के बिना, Prover आर्बिट्रेरी (arbitrary) स्टार्टिंग वैल्यूज़ असाइन करता है, जिससे फ़ॉल्स पॉज़िटिव वायलेशंस (violations) हो सकते हैं:

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

अब, यहाँ Sstore हुक दिया गया है जहाँ ghost वेरिएबल g_sumOfBalances का उपयोग कुल अकाउंट बैलेंस में बदलावों को स्टोर और ट्रैक करने के लिए किया जाता है:

Copy
hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

नीचे दिया गया Sload हुक बैलेंस रीड्स (reads) को सीमित करता है ताकि Prover को ट्रैक किए गए बैलेंस के योग से अधिक वैल्यू असाइन करने से रोका जा सके:

Copy
hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

अंत में, हम formally verify करते हैं कि total supply सभी बैलेंस के योग के बराबर है:

Copy
invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

requireInvariant — प्रीकंडीशन के रूप में इनवैरिएंट

इनवैरिएंट totalSupplyEqualsSumOfBalances न केवल एक यूनिवर्सल प्रॉपर्टी के रूप में उपयोगी है, बल्कि हम प्रीकंडीशन्स के स्थान पर एक प्रूवन (proven) असंप्शन (assumption) के रूप में भी इस पर भरोसा करते हैं।

इसके स्पष्ट अर्थ के अलावा कि total supply सभी बैलेंस के योग के बराबर है, इनवैरिएंट totalSupply() == g_sumOfBalances का यह भी अर्थ है:

• total supply हमेशा किसी भी व्यक्तिगत बैलेंस से अधिक या उसके बराबर होती है।
• total supply और बैलेंस का योग दोनों max_uint256 के भीतर रहते हैं।

याद करें कि पहले के transfer और transferFrom रूल्स में एक प्रीकंडीशन शामिल थी जिसमें बैलेंस को max_uint256 के भीतर रहने की आवश्यकता थी। यह एक ओवरफ्लो बग को छिपा सकता था क्योंकि प्रीकंडीशन ने बैलेंस को assumed और कंस्ट्रेन (constrain) किया था, जो अनजाने में उन स्टेट्स को फ़िल्टर कर सकता था जहाँ बग दिखाई दे सकता था।

इसलिए, वेरीफाइड इनवैरिएंट totalSupplyEqualsSumOfBalances का प्रीकंडीशन के रूप में उपयोग करना अधिक सुरक्षित है, क्योंकि यह सुनिश्चित करता है कि रूल को एक ऐसी प्रॉपर्टी के साथ एग्ज़ीक्यूट किया जाता है जो “सभी” रिचेबल (reachable) स्टेट्स में लागू होती है।

अब हम require स्टेटमेंट्स को requireInvariant totalSupplyEqualsSumOfBalances से रिप्लेस करते हैं, जैसा कि नीचे दिखाया गया है:

Copy
rule transfer_effectOnBalances_requireInvariant(env e) {
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

rule transferFrom_effectOnBalances_requireInvariant(env e) {
    address holder;
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

इसके अलावा, burn और mint रूल्स में एक प्रीकंडीशन शामिल है जिसमें यह आवश्यक है कि total supply क्रमशः होल्डर और रिसीवर के बैलेंस से अधिक या उसके बराबर हो। यह require प्रीकंडीशन एक assumed कंस्ट्रेंट (constraint) है, और सुरक्षित रहने के लिए, हम इसे एक प्रूवन इनवैरिएंट से रिप्लेस करते हैं।

चूंकि invariant totalSupplyEqualsSumOfBalances का यह भी अर्थ है कि total supply सभी व्यक्तिगत बैलेंस से अधिक या उसके बराबर है, हम require प्रीकंडीशन को requireInvariant totalSupplyEqualsSumOfBalances से रिप्लेस कर सकते हैं:

Copy
rule mint_increasesTotalSupplyAndBalance_requireInvariant() {
    address receiver;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(receiver)`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}


rule burn_decreasesTotalSupplyAndBalance_requireInvariant() {

    address holder;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(holder)`
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover run: link

4. अनधिकृत एक्शन्स (Unauthorized actions) — स्टेट को बदलने की अनुमति न प्राप्त मेथड्स और कॉलर्स

यह वेरिफाई करता है कि कुछ विशिष्ट स्टेट चेंजेस या एक्शन्स स्पष्ट रूप से अनुमत (permitted) फंक्शन्स या कॉलर्स के बाहर नहीं होने चाहिए।

केवल कुछ मेथड्स ही स्टोरेज / स्टेट को बदल सकते हैं

आइए इस प्रॉपर्टी के साथ शुरू करते हैं: “केवल mint() और burn() ही total supply को बदल सकते हैं।”

नीचे दिया गया रूल एक पैरामेट्रिक रूल (parametric rule) है (अध्याय “Introduction to Parametric Rules” देखें) जहाँ फंक्शन्स को आर्बिट्रेरी तरीके से (f(e, args) के माध्यम से) कॉल किया जा सकता है, लेकिन केवल mint() और burn() को totalSupply बदलने की अनुमति है। इसे उस assertion द्वारा लागू किया जाता है जहाँ totalSupplyAfter != totalSupplyBefore यह इम्प्लाई (=>) करता है कि केवल ये दो फंक्शन्स ही इस तरह के बदलाव का कारण बन सकते हैं:

Copy
rule onlyMethodsCanChangeTotalSupply(env e, method f, calldataarg args) {
    mathint totalSupplyBefore = totalSupply();

    f(e, args);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter != totalSupplyBefore => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:burn(address,uint256).selector
    );
}

हालाँकि यह assert करता है कि किन फंक्शन्स को totalSupply को संशोधित करने की अनुमति है, इसका यह भी अर्थ है कि अन्य सभी फंक्शन्स ऐसा करने के लिए अनधिकृत हैं।

इस श्रेणी के शेष रूल्स नीचे दिखाए गए हैं और समान पैटर्न का पालन करते हैं:

• केवल mint(), burn(), transfer() और transferFrom() ही अकाउंट बैलेंस को बदल सकते हैं:

  Copy
  rule onlyMethodsCanChangeAccountBalances(env e, method f, calldataarg args) {
      address account;
      mathint balanceBefore = balanceOf(account);
      
      f(e, args);
      mathint balanceAfter = balanceOf(account);
  
      assert balanceBefore != balanceAfter => (
          f.selector == sig:transfer(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector ||
          f.selector == sig:mint(address,uint256).selector ||
          f.selector == sig:burn(address,uint256).selector
      );
  }
  

• केवल approve() और transferFrom() ही allowances को बदल सकते हैं:

  Copy
  rule onlyMethodsCanChangeAllowance(env e, method f, calldataarg args) {
      address holder;
      address spender;
  
      mathint allowanceBefore = allowance(holder, spender);
  
      f(e, args);
      mathint allowanceAfter = allowance(holder, spender);
  
      assert allowanceAfter != allowanceBefore => (
          f.selector == sig:approve(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector
      );
  }
  

अब जब हमने ऐसे रूल्स लिख लिए हैं जो यह वेरिफाई करते हैं कि कौन से मेथड्स स्टेट को संशोधित कर सकते हैं, तो हम वह रूल लिख सकते हैं जो वेरिफाई करता है कि किन कॉलर्स को होल्डर का बैलेंस कम करने की अनुमति है।

केवल होल्डर्स और स्पेंडर्स ही होल्डर का बैलेंस कम कर सकते हैं

एक अन्य अनधिकृत एक्शन तब बैलेंस को कम करना है जब कॉलर होल्डर या अप्रूव्ड spender नहीं है। निम्नलिखित रूल इस प्रॉपर्टी को वेरिफाई करता है:

Copy
rule onlyHolderAndSpenderCanReduceHolderBalance(env e, method f, calldataarg args) filtered {
	// `burn()` is excluded since permission checks are left to the integrator / developer
    f -> f.selector != sig:burn(address,uint256).selector                                                   
} {
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    address account;

    mathint spenderAllowanceBefore = allowance(account, e.msg.sender);
	mathint holderBalanceBefore = balanceOf(account);
    
    f(e, args);
	mathint holderBalanceAfter = balanceOf(account);

    assert (holderBalanceAfter < holderBalanceBefore) => (
        e.msg.sender == account ||
        holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
    );
}

नीचे दी गई लाइन यह बताती है कि हम पैरामेट्रिक कॉल्स में burn() फंक्शन को बाहर (exclude) कर रहे हैं:

Copy
f -> f.selector != sig:burn(address,uint256).selector

burn() को फ़िल्टर कर दिया गया है क्योंकि, जैसा कि पहले उल्लेख किया गया है, इसे जानबूझकर अनुमति चेक (permission checks) के बिना छोड़ दिया गया है। इसे रूल में शामिल करने से यह विफल हो जाएगा, क्योंकि कोई भी कॉलर होल्डर के बैलेंस को कम कर सकता है, जो रूल के इंटेंट को विफल कर देगा।

हमने इनवैरिएंट्स अनुभाग में requireInvariant को पहले ही कवर कर लिया है, और हम पहले के अनुभागों से मेथड कॉल के पहले और बाद में स्टेट रिकॉर्ड करने से परिचित हैं, इसलिए हम सीधे assertion पर जा सकते हैं।

नीचे दिए गए assertion का मतलब है कि यदि होल्डर का बैलेंस कम होता है, तो यह दो कारणों में से किसी एक के कारण होना चाहिए:

• e.msg.sender == account

  होल्डर ने एक्शन शुरू किया, या

• holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)

  कमी एक अप्रूव्ड allowance की सीमा के भीतर आती है, जिसका अर्थ यह भी है कि कॉलर एक नॉनजीरो allowance के साथ अप्रूव्ड spender है।

Copy
assert (holderBalanceAfter < holderBalanceBefore) => (
    e.msg.sender == account ||
    holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
);

यह विशिष्ट रूल OpenZeppelin के onlyAuthorizedCanTransfer का एक संशोधित संस्करण है। परिवर्तन यह है कि मूल रूल में, sig:burn(address,uint256).selector assertion में था, जबकि इस onlyHolderAndSpenderCanReduceHolderBalance रूल में हमने इसे फ़िल्टर (filtered) कर दिया है।

यहाँ इस अनुभाग के सभी रूल्स के लिए Prover run दिया गया है।

ERC-20 के लिए पूर्ण CVL स्पेसिफिकेशन

यहाँ पूर्ण CVL स्पेसिफिकेशन और Prover run दिया गया है।

यह लेख Certora Prover का उपयोग करके formal verification पर एक सीरीज़ का हिस्सा है