परिचय

ERC-721 नॉन-फंजिबल टोकन्स के लिए Ethereum स्टैंडर्ड है, जिसका उपयोग व्यापक रूप से डिजिटल प्रॉपर्टी को रिप्रेजेंट करने के लिए किया जाता है। किसी भी अन्य प्रॉपर्टी की तरह, यह सप्लाई क्रिएट करने, सप्लाई रिमूव करने और ओनरशिप ट्रांसफर करने के इर्द-गिर्द घूमता है।

यह चैप्टर mint और burn ऑपरेशन्स को फॉर्मली वेरीफाई करने पर केंद्रित है। यह OpenZeppelin’s ERC-721 CVL specification के कोड वॉकथ्रू का पहला भाग (1/5) है।

अपने पूरे स्पेसिफिकेशन्स में, OpenZeppelin तीन प्रकार के असर्शन्स (assertions) को एक सिंगल रूल में कंबाइन करने के एक पैटर्न का उपयोग करता है, जिन्हें इस प्रकार कैटेगराइज़ किया गया है:

1. Liveness — यह उन कंडीशन्स को स्पेसिफाई करता है जिनके तहत फंक्शन रिवर्ट (revert) नहीं होता है।
2. Effect — यह उन स्टेट चेंजेस को स्पेसिफाई करता है जो फंक्शन के रिवर्ट न होने पर होते हैं।
3. No side-effect — यह स्पेसिफाई करता है कि Effect असर्शन में बताए गए स्टेट चेंजेस के अलावा कोई अन्य अनपेक्षित (unintended) स्टेट चेंजेस नहीं होते हैं।

वेरिफिकेशन के लिए internal functions _mint() और _burn() को एक्सपोज़ करना

_mint() और _burn() इंटरनल फंक्शन्स हैं जो डेवलपर्स के लिए इनहेरिट (inherit) करने और NFTs बनाने और नष्ट करने के लिए कस्टम लॉजिक बिल्ड करने के उद्देश्य से बनाए गए हैं। इस स्पेसिफिकेशन में, harness कॉन्ट्रैक्ट उन्हें इनहेरिट करता है और बाहरी (external) फंक्शन्स के रूप में एक्सपोज़ करता है, जो Prover को वेरिफिकेशन के दौरान _mint() और _burn() को इन्वोक (invoke) करने की अनुमति देता है।

निम्नलिखित इनके OpenZeppelin implementations हैं:

• _mint()
• _burn()
• harness जो उन्हें एक्सपोज़ करता है

Copy
// ERC721.sol

function _mint(address to, uint256 tokenId) internal {
    if (to == address(0)) {
        revert ERC721InvalidReceiver(address(0));
    }
    address previousOwner = _update(to, tokenId, address(0));
    if (previousOwner != address(0)) {
        revert ERC721InvalidSender(address(0));
    }
}
...

function _burn(uint256 tokenId) internal {
    address previousOwner = _update(address(0), tokenId, address(0));
    if (previousOwner == address(0)) {
        revert ERC721NonexistentToken(tokenId);
    }
}

Copy
// ERC721Harness.sol

function mint(address account, uint256 tokenId) external {
    _mint(account, tokenId);
}
...

function burn(uint256 tokenId) external {
    _burn(tokenId);
}

mint को फॉर्मली वेरीफाई करना

mint() ऑपरेशन एक नया टोकन क्रिएट करता है और इसे एक रेसिपिएंट (recipient) को असाइन करता है। हम फॉर्मली वेरीफाई करते हैं कि:

• यह तभी रिवर्ट नहीं करता है यदि और केवल यदि टोकन अनमिंटेड (unminted) है और रेसिपिएंट वैलिड है
• यदि यह रिवर्ट नहीं करता है, तो टोटल सप्लाई और रेसिपिएंट का बैलेंस दोनों एक से बढ़ जाते हैं
• रेसिपिएंट ओनर बन जाता है
• किसी अन्य अकाउंट का बैलेंस या टोकन की ओनरशिप नहीं बदलती है

यहाँ CVL रूल दिया गया है जो इन प्रॉपर्टीज़ को साबित करता है:

Copy
// ERC721.spec -- mint (explanation follows)


rule mint(env e, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	// requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);
    
	// pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
		
	// method call
    mint@withrevert(e, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

हम ऊपर दिए गए रूल के सेक्शन्स पर इस प्रकार चर्चा करेंगे:

• Preconditions
• Pre-call state
• Mint कॉल
• Assertions
  • liveness
  • effect
  • no side-effect

Preconditions

एक precondition रूल में एक कंस्ट्रेंट (constraint) है जो यह स्पेसिफाई करता है कि Prover द्वारा mint() मेथड को एग्जीक्यूट करने से पहले क्या सत्य होना चाहिए। यह मेथड के कारण होने वाले स्टेट चेंजेस के आधार पर, कॉल के “बाद” होल्ड (hold) कर भी सकता है और नहीं भी।

mint रूल के लिए preconditions निम्नलिखित हैं:

Copy
require nonpayable(e);
// requireInvariant notMintedUnset(tokenId); // intentionally commented out
...

require balanceLimited(to);

नोट: चर्चा की सरलता के लिए, इनवैरिएंट precondition notMintedUnset(tokenId) को कमेंट आउट कर दिया गया है, क्योंकि mint रूल इसके बिना सफलतापूर्वक वेरीफाई हो जाता है। हम अगले चैप्टर में ERC-721 कोडबेस के CVL इनवैरिएंट्स को कवर करेंगे।

• require nonpayable(e)

  यह रिक्वायर करता है कि कॉल बिना कोई ETH भेजे की जाए क्योंकि mint() नॉन-पेयेबल (nonpayable) है। nonpayable(e) को एक definition के रूप में एक्सप्रेस किया गया है जो e.msg.value == 0 होने पर true और अन्यथा false रिटर्न करता है:

  Copy
  definition nonpayable(env e) returns bool = e.msg.value == 0;
  

  यह कंडीशन e.msg.value == 0 को nonpayable(e) नामक एक रीयूज़ेबल एक्सप्रेशन (reusable expression) से बाइंड करके यह चेक करने के लॉजिक को एनकैप्सुलेट (encapsulate) करता है कि कॉल में कोई ETH नहीं है। यह परिभाषा हमें हर बार नॉन-पेयेबल फंक्शन को इन्वोक करते समय बार-बार e.msg.value == 0 लिखने के बजाय पूरे स्पेसिफिकेशन में कंडीशन को रेफरेंस करने की अनुमति देती है।

  नोट: definition CVL में एक व्यापक विषय है। अधिक जानकारी के लिए, Certora documentation_ देखें। इस सीरीज़ में, कोड की रीडेबिलिटी को बेहतर बनाने के लिए डेफिनिशन्स का उपयोग सीधे रीयूज़ेबल एक्सप्रेशन्स के रूप में किया जाता है।_

• require balanceLimited(to)

  यह रिक्वायर करता है कि रेसिपिएंट का बैलेंस max_uint256 से कम हो। इसे भी एक definition के रूप में एक्सप्रेस किया गया है जो balanceOf(account) < max_uint256 होने पर true रिटर्न करता है:

  Copy
  definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
  

  OpenZeppelin ERC-721 इम्प्लीमेंटेशन गैस एफिशिएंसी (gas efficiency) के लिए जानबूझकर एक unchecked ब्लॉक के अंदर बैलेंस को इंक्रीमेंट करता है। ओवरफ्लो सैद्धांतिक रूप से संभव है लेकिन व्यावहारिक रूप से असंभव है, क्योंकि max_uint256 तक पहुँचने के लिए यथार्थवादी रूप से मौजूद हो सकने वाले NFTs से अधिक NFTs को मिंट करने की आवश्यकता होगी। इसलिए, precondition require balanceLimited(to) उचित है।

  precondition balanceLimited(to) के बिना, Prover ओवरफ्लो केसेस पर विचार करेगा, क्योंकि mint() _update() फंक्शन को कॉल करता है, जहाँ बैलेंस इंक्रीमेंट एक unchecked ब्लॉक के अंदर होता है:

  Copy
  // ERC721.sol
  
  function _mint(address to, uint256 tokenId) internal {
      ...
      address previousOwner = _update(to, tokenId, address(0));
      ...
  }
  

  Copy
  /// ERC721.sol
  
  function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
      ...
  
      if (to != address(0)) {
          unchecked {
              _balances[to] += 1;
          }
      }
  	  ...
  }
  

Pre-call state को रिकॉर्ड करना — mint कॉल से पहले टोटल सप्लाई, बैलेंस और ओनरशिप

mint() फंक्शन को इन्वोक करने से पहले निम्नलिखित स्टेट्स रिकॉर्ड की जाती हैं। फिर असर्शन्स सेक्शन में इन वैल्यूज़ की तुलना पोस्ट-कॉल वैल्यूज़ से की जाती है:

Copy
mathint supplyBefore         = _supply;
uint256 balanceOfToBefore    = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore          = unsafeOwnerOf(tokenId);
address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

• mathint supplyBefore = _supply

  यह मिंट कॉल से पहले टोटल सप्लाई को रिकॉर्ड करता है, ताकि इसकी तुलना पोस्ट-मिंट सप्लाई से की जा सके और पुष्टि की जा सके कि यह 1 से बढ़ गई है।

  _supply एक ghost वेरिएबल है जो टोटल सप्लाई को ट्रैक करता है और एक Sstore हुक (hook) के माध्यम से अपडेट किया जाता है क्योंकि नए बैलेंस जोड़े जाते हैं और पुराने बैलेंस घटाए जाते हैं।

  ghost वेरिएबल _supply को एक mathint के रूप में डिक्लेयर किया गया है, इसलिए supplyBefore भी एक mathint होना चाहिए। यदि supplyBefore को uint256 के रूप में डिक्लेयर किया गया होता, तो Prover एक टाइप एरर रिपोर्ट करता। यह एरर इसलिए उत्पन्न होता है क्योंकि mathint एक अनबाउंडेड (unbounded) मैथमेटिकल इंटीजर को रिप्रेजेंट करता है, जबकि uint256 एक बाउंडेड (bounded) इंटीजर को रिप्रेजेंट करता है। किसी mathint वैल्यू को uint256 में असाइन करने से यह मान लिया जाएगा कि वैल्यू 256 बिट्स के भीतर फिट बैठती है, जिसे Prover सुरक्षित रूप से नहीं मान सकता।

  यहाँ Sstore हुक इम्प्लीमेंटेशन है जो ghost वेरिएबल _supply को अपडेट करता है:

  Copy
  ghost mathint _supply {
      init_state axiom _supply == 0;
  }
  
  hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
      _supply = _supply - oldValue + newValue;
  }
  

• uint256 balanceOfToBefore = balanceOf(to)

  यह मिंट कॉल से पहले रेसिपिएंट के बैलेंस को रिकॉर्ड करता है, ताकि इसकी तुलना पोस्ट-मिंट बैलेंस से की जा सके और पुष्टि की जा सके कि यह भी 1 से बढ़ गया है।

• uint256 balanceOfOtherBefore = balanceOf(otherAccount)

  यह मिंट कॉल से पहले किसी भी अन्य अकाउंट के बैलेंस को रिकॉर्ड करता है, ताकि इसकी तुलना पोस्ट-मिंट बैलेंस से की जा सके और पुष्टि की जा सके कि यह नहीं बदला है, इसलिए कोई साइड इफेक्ट नहीं है।

• address ownerBefore = unsafeOwnerOf(tokenId)

  यह मिंट कॉल से पहले टोकन के ओनर को रिकॉर्ड करता है। मिंट को सफल होने के लिए, यह वैल्यू शून्य होनी चाहिए, जो कि liveness कंडीशन्स (ownerBefore == 0 और to != 0) में से एक है।

  unsafeOwnerOf() एक harness फंक्शन है जो बिना वैलिड ओनर वाले टोकन्स के लिए भी ओनरशिप को एक्सपोज़ करता है। यह अनमिंटेड टोकन्स के लिए शून्य एड्रेस (zero address) रिटर्न करता है, ownerOf() के विपरीत, जो उन मामलों में रिवर्ट हो जाएगा। यह रूल को मिंटिंग से पहले और बाद में ओनरशिप की तुलना करने में सक्षम बनाता है क्योंकि उन ओनरशिप ट्रांज़िशन्स में शून्य एड्रेस (अनमिंटेड स्टेट) से एक वैलिड ओनर एड्रेस शामिल होता है।

• address otherOwnerBefore = unsafeOwnerOf(otherTokenId)

  यह मिंट कॉल से पहले एक आर्बिट्रेरी (arbitrary) टोकन (मिंट किए जा रहे टोकन के अलावा) के ओनर को रिकॉर्ड करता है ताकि हम पुष्टि कर सकें कि यह पोस्ट-मिंट नहीं बदला है, इसलिए कोई साइड इफेक्ट नहीं है।

Mint कॉल

@withrevert टैग Prover को रिवर्टिंग (reverting) और नॉन-रिवर्टिंग (non-reverting) दोनों पाथ्स को एक्सप्लोर करने की अनुमति देता है। !lastReverted कंडीशन यह कैप्चर करती है कि क्या कॉल रिवर्ट नहीं हुई और इसे success के रूप में स्टोर करती है:

Copy
mint@withrevert(e, to, tokenId);
bool success = !lastReverted;

Assertions — liveness, effect, और no side effect

जैसा कि पहले उल्लेख किया गया है, पूरे स्पेसिफिकेशन में उपयोग किया गया रूल पैटर्न liveness, effect और no side-effect को एक सिंगल रूल में कंबाइन करता है। यहाँ वह कोड ब्लॉक है जिसे हम बाद में विस्तार से समझाएंगे:

Copy
// liveness
assert success <=> (
    ownerBefore == 0 &&
    to != 0
);

// effect
assert success => (
    _supply                   == supplyBefore + 1 &&
    to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
    unsafeOwnerOf(tokenId)    == to
);

// no side effect
assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;

Liveness:

नीचे दिया गया असर्शन बताता है कि _mint() रिवर्ट नहीं करता है यदि और केवल यदि टोकन अनमिंटेड (ownerBefore == 0) है और रेसिपिएंट वैलिड (to != 0) है:

Copy
// liveness
assert success <=> (
    ownerBefore == 0 &&
    to != 0
);

हमने पिछले दो चैप्टर्स में रिवर्ट और disjunction पैटर्न का उपयोग किया था। यदि हम ऊपर दिए गए असर्शन को उस पैटर्न में कनवर्ट करते हैं, तो यह बन जाता है:

_mint() रिवर्ट करता है यदि और केवल यदि टोकन पहले से ही मिंटेड है (ownerBefore != 0) या रेसिपिएंट वैलिड नहीं है (to == 0)।

Copy
// reverts
assert !success <=> (
    ownerBefore != 0 ||
    to == 0
);

जबकि “success + conjunction” (liveness) पैटर्न उन सभी कंडीशन्स को सूचीबद्ध करता है जिनके तहत फंक्शन सफल होता है, “revert + disjunction” पैटर्न उन सभी कंडीशन्स को सूचीबद्ध करता है जिनके तहत यह रिवर्ट होता है। वे तार्किक रूप से (logically) समान हैं।

Effect:

यदि mint() फंक्शन रिवर्ट नहीं होता है, तो परिणामस्वरूप होने वाले स्टेट चेंजेस हैं:

• टोटल सप्लाई ठीक एक से बढ़ जाती है (_supply == supplyBefore + 1)
• रेसिपिएंट का बैलेंस ठीक एक से बढ़ जाता है (balanceOf(to) == balanceOfToBefore + 1)
• टोकन का ओनर अब रेसिपिएंट है (unsafeOwnerOf(tokenId) == to)

Copy
// effect
assert success => (
    _supply                   == supplyBefore + 1 &&
    to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
    unsafeOwnerOf(tokenId)    == to
);

No side effect:

निम्नलिखित असर्शन्स चेक करते हैं कि mint() फंक्शन कोई अनपेक्षित साइड इफेक्ट्स का कारण नहीं बनता है:

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to

  यह चेक करता है कि केवल इच्छित रेसिपिएंट (intended recipient) का बैलेंस बदलता है, जबकि अन्य सभी अकाउंट्स अप्रभावित रहते हैं। यदि मिंट कॉल के बाद किसी अकाउंट का बैलेंस बदलता है, तो वह अकाउंट रेसिपिएंट (to) है। यदि किसी अकाउंट का बैलेंस नहीं बदलता है, तो वह अकाउंट रेसिपिएंट नहीं है, इसलिए मिंट कॉल से अप्रभावित है।

• assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId

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

Copy
// no side effect
assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;

अब, यहाँ पूरा स्पेसिफिकेशन दिया गया है, जिसमें मिंट रूल, डेफिनिशन्स, ghosts और हुक्स शामिल हैं:

Copy
methods {
    function balanceOf(address) external returns (uint256) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mathint _supply {
    init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: mint behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule mint(env e, address to, uint256 tokenId) {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    mint@withrevert(e, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

यहाँ Prover रन (run) है।

burn को फॉर्मली वेरीफाई करना

burn ऑपरेशन मिंट के विपरीत स्टेट चेंजेस करता है।

मिंट करते समय, स्टेट चेंजेस होते हैं:

• _supply 1 से बढ़ जाता है
• balanceOf(to) 1 से बढ़ जाता है
• ownerOf(tokenId) पिछली वैल्यू address(0) से एक नॉन-जीरो (nonzero) एड्रेस में बदल जाता है

बर्न करते समय, इसके विपरीत होता है:

• _supply 1 से घट जाता है
• balanceOf(from) 1 से घट जाता है
• ownerOf(tokenId) अपने पिछले नॉन-जीरो एड्रेस से वापस address(0) में बदल जाता है

मिंट के विपरीत, जहाँ टोकन बिना किसी मौजूदा अप्रूवल (approvals) के नए बनाए जाते हैं, बर्न ऑपरेशन्स को टोकन क्लियर करने के हिस्से के रूप में किसी भी मौजूदा अप्रूवल को हटाना होगा।

इन बिहेवियर्स को ध्यान में रखते हुए, हम फॉर्मली वेरीफाई करते हैं कि:

• यह रिवर्ट नहीं करता है यदि और केवल यदि टोकन मौजूद है (अर्थात ओनर address(0) नहीं है)
• यदि कॉल सफल होती है, तो टोटल सप्लाई एक से घट जाती है और पिछले ओनर का बैलेंस एक से घट जाता है
• ओनर address(0) पर सेट हो जाता है, जिसका अर्थ है कि टोकन का कोई ओनर नहीं है
• टोकन अप्रूवल (token approval) क्लियर हो जाता है
• कोई अन्य अकाउंट बैलेंस, टोकन ओनरशिप, या अप्रूवल्स नहीं बदलते हैं

यहाँ CVL रूल दिया गया है जो इन प्रॉपर्टीज़ को साबित करता है:

Copy
// ERC721.spec -- burn (explanation follows) 

rule burn(env e, uint256 tokenId) {
	// preconditions
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);
    
    // pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Preconditions

mint रूल के समान, यह रूल भी नॉन-पेयेबल है। इसलिए, require nonpayable(e) आवश्यक है:

Copy
require nonpayable(e);
...

Pre-call state को रिकॉर्ड करना — burn कॉल से पहले टोटल सप्लाई, बैलेंस, ओनरशिप और अप्रूवल

mint रूल में रिकॉर्ड की गई सभी प्री-कॉल स्टेट्स burn रूल में भी दिखाई देती हैं, निम्नलिखित को छोड़कर:

• uint256 balanceOfFromBefore = balanceOf(from)

  मिंट रिसीवर (balanceOf(to)) के प्री-कॉल स्टेट को रिकॉर्ड करने के बजाय, बर्न रूल ओनर के बैलेंस (balanceOf(from)) को रिकॉर्ड करता है ताकि यह वेरीफाई किया जा सके कि बर्न कॉल के अंत में, बैलेंस 1 से घट जाता है।

• address otherApprovalBefore = unsafeGetApproved(otherTokenId)

  बर्न फंक्शन में अप्रूवल आवश्यक है; इसलिए, यह एक आर्बिट्रेरी अन्य टोकन के अप्रूवल को रिकॉर्ड करता है ताकि यह वेरीफाई किया जा सके कि यह अपरिवर्तित (unchanged) रहता है।

Burn कॉल

पिछले रूल्स की तरह, कॉल @withrevert टैग का उपयोग करती है। बूलियन (boolean) success कैप्चर करता है कि क्या कॉल रिवर्ट नहीं हुई (!lastReverted), जिसका उपयोग प्री-कॉल और पोस्ट-कॉल स्टेट्स के बीच अपेक्षित (expected) बदलावों को वेरीफाई करने के लिए किया जाता है:

Copy
burn@withrevert(e, tokenId);
bool success = !lastReverted;

Assertions — liveness, effect**, और no side effect**

यहाँ प्राप्त की गई सभी वैल्यूज़ पोस्ट-कॉल स्टेट्स हैं जिनकी तुलना प्री-कॉल स्टेट्स से की जाती है:

Copy
// liveness
assert success <=> (
    ownerBefore != 0
);

// effect
assert success => (
    unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
    to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
    unsafeOwnerOf(tokenId)      == 0 &&
    unsafeGetApproved(tokenId)  == 0
);

// no side effect
assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

Liveness:

यह असर्ट (assert) करता है कि बर्न कॉल रिवर्ट नहीं होती है यदि और केवल यदि बर्न किए जाने वाले tokenId का एक ओनर हो।

Effect:

यदि बर्न कॉल रिवर्ट नहीं होती है, तो इसका मतलब है कि निम्नलिखित सभी स्टेट चेंजेस अवश्य हुए होंगे:

• unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1)

  यदि टोकन मिंटेड है (जिसका एक नॉन-जीरो ओनर है), तो सप्लाई ठीक 1 से घट जाती है। इसका मतलब है कि सप्लाई में कमी की जांच केवल तभी की जाती है जब कम से कम एक मिंटेड टोकन हो।

• to_mathint(balanceOf(from)) == balanceOfFromBefore - 1

  from एड्रेस (टोकन ओनर) का बैलेंस 1 से घट गया है।

• unsafeOwnerOf(tokenId) == 0

  टोकन की ओनरशिप क्लियर कर दी गई है, इसलिए unsafeOwnerOf(tokenId) 0 रिटर्न करता है।

• unsafeGetApproved(tokenId) == 0

  टोकन के लिए कोई भी मौजूदा अप्रूवल हटा दिया गया है, इसलिए unsafeGetApproved(tokenId) 0 रिटर्न करता है।

No side effect:

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == from

  यह चेक करता है कि केवल प्री-बर्न ओनर का बैलेंस बदलता है, जबकि अन्य सभी अकाउंट्स अप्रभावित रहते हैं। यदि बर्न कॉल के बाद किसी अकाउंट का बैलेंस बदलता है, तो वह अकाउंट बर्न से पहले का ओनर है।

• assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId

  यह चेक करता है कि केवल बर्न किए गए टोकन की ओनरशिप बदलती है, जबकि अन्य सभी टोकन्स अप्रभावित रहते हैं। यदि बर्न कॉल के बाद किसी टोकन का ओनर बदलता है, तो वह टोकन बर्न किया गया टोकन है।

• assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId

  यह चेक करता है कि केवल बर्न किए गए टोकन का अप्रूवल क्लियर किया जाता है, जबकि अन्य सभी टोकन अप्रूवल्स अप्रभावित रहते हैं। यदि बर्न कॉल के बाद किसी टोकन के लिए अप्रूवल बदलता है, तो वह टोकन बर्न किया गया टोकन है।

यहाँ burn रूल के लिए पूरा स्पेसिफिकेशन दिया गया है:

Copy
methods {
    function ownerOf(uint256) external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mathint _supply {
    init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: burn behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule burn(env e, uint256 tokenId) {
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);

    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => otherAccount == from;
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

नोट: लाइन requireInvariant ownerHasBalance(tokenId) को कमेंट आउट कर दिया गया है क्योंकि Prover 8.3.1 इस इनवैरिएंट (invariant) के वायलेशन्स की रिपोर्ट करता है, इसलिए इसे इस स्पेसिफिकेशन में लागू नहीं किया जा सकता है। इसके कारण "effect” असर्शन को _supply == supplyBefore - 1 से unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1) में एडजस्ट किया गया। ownerHasBalance(tokenId) सहित सभी इनवैरिएंट्स पर अगले चैप्टर में चर्चा की जाएगी।

यहाँ burn रूल के लिए Prover रन (run) है।

mint और burn के लिए पूर्ण स्पेसिफिकेशन्स

यहाँ पूरा स्पेसिफिकेशन और Prover रन (run) है।

यह आर्टिकल Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर एक सीरीज़ का हिस्सा है