परिचय

यह अध्याय OpenZeppelin’s ERC-721 CVL specification के हमारे कोड वॉकथ्रू के तीसरे भाग (3/5) के रूप में जारी है और टोकन ट्रांसफर और अप्रूवल नियमों पर केंद्रित है, विशेष रूप से:

• transferFrom()
• approve()
• setApprovalForAll()
• zeroAddressBalanceRevert()

ये नियम ओनरशिप (स्वामित्व) ट्रांसफर, प्रति-टोकन अप्रूवल, सभी टोकन के लिए ऑपरेटर अप्रूवल, और यह सत्यापित करते हैं कि balanceOf(0) को क्वेरी करने पर यह रिवर्ट (revert) होता है।

transferFrom() को फॉर्मली वेरिफाई करना

transferFrom() फंक्शन एक NFT की ओनरशिप को दूसरे एड्रेस पर बदल देता है। यह मानकर चलता है कि NFT पहले से ही मिंट (mint) हो चुका है, और इसे केवल ओनर (owner), उस टोकन ID के लिए अप्रूव्ड (approved) एड्रेस, या ओनर के सभी टोकन के लिए अप्रूव्ड ऑपरेटर (operator) द्वारा ही कॉल किया जा सकता है।

यहाँ transferFrom नियम दिया गया है जिसे हम कोड ब्लॉक के बाद सेक्शन-दर-सेक्शन समझाएंगे:

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);
    
    // pre-call state
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

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

Preconditions

ये Preconditions (पूर्व-शर्तें) निर्दिष्ट करती हैं कि Prover द्वारा transferFrom() निष्पादित (execute) करने से पहले क्या सत्य होना चाहिए। हम इसके बाद कोड ब्लॉक की प्रत्येक लाइन को समझाएंगे:

Copy
require nonpayable(e);
require authSanity(e);
...
requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);

require nonpayable(e)

यह आवश्यक करता है कि transferFrom() को बिना ETH भेजे कॉल किया जाए, क्योंकि यह फंक्शन non-payable है। इसे एक definition के रूप में व्यक्त किया गया है:

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

यह कंडीशन e.msg.value == 0 को nonpayable(e) नामक एक पुन: प्रयोज्य (reusable) एक्सप्रेशन के रूप में परिभाषित करता है, जो यह जांचता है कि कॉल में कोई ETH शामिल नहीं है।

यद्यपि ERC-721 standard transferFrom() को payable के रूप में निर्दिष्ट करता है, OpenZeppelin इसे non-payable के रूप में इम्प्लीमेंट (implement) करता है। व्यवहार में, NFT ट्रांसफर के साथ ETH भेजे जाने की उम्मीद नहीं की जाती है, इसलिए यह एक व्यावहारिक परंपरा (practical convention) बन गई है। CVL नियम e.msg.value == 0 को लागू करता है।

require authSanity(e)

यह आवश्यक करता है कि कॉलर (caller) शून्य एड्रेस (zero address) न हो। इसे भी एक definition के रूप में व्यक्त किया गया है:

Copy
definition authSanity(env e) returns bool = e.msg.sender != 0

इस आवश्यकता के बिना, Prover address(0) को एक वैध कॉलर के रूप में मानता है, भले ही address(0) से कोई वास्तविक कॉल उत्पन्न नहीं हो सकती। कॉन्ट्रैक्ट का ऑथराइजेशन लॉजिक कभी भी address(0) को ओनर (owner), अप्रूव्ड एड्रेस (approved address), या ऑपरेटर (operator) के रूप में अनुमति नहीं देता है, इसलिए address(0) के कॉलर के रूप में कार्य करने से होने वाले कोई भी उल्लंघन (violations) फॉल्स पॉजिटिव (false positives) होते हैं।

requireInvariant ownerHasBalance(tokenId)

इस पूर्व-शर्त (precondition) में यह आवश्यक है कि नियम की शुरुआत में ownerHasBalance(tokenId) इनवेरिएंट (invariant) (जो यह गारंटी देता है कि यदि कोई टोकन मौजूद है, तो उसके ओनर का बैलेंस पॉजिटिव है) होल्ड (hold) करे। यह Prover को एक ऐसी स्टेट (state) से शुरू करने के लिए बाध्य करता है जहाँ किसी भी मौजूदा टोकन का एक वैध (गैर-शून्य/nonzero) ओनर होता है:

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

Copy
// invariant as a precondition

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    ...

ownerHasBalance इनवेरिएंट preserved ब्लॉक के माध्यम से एक अन्य इनवेरिएंट balanceOfConsistency पर निर्भर करता है, जो यह सत्यापित करता है कि balanceOf, _ownedByUser, और ghost _balances समान हैं:

Copy
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved { // invariant as a preserved condition
            requireInvariant balanceOfConsistency(ownerOf(tokenId));  
        }
    }

Copy
// invariant as a preserved condition 

invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

इनवेरिएंट ownerHasBalance(tokenId) को पूर्व-शर्त (precondition) के रूप में उपयोग करके, transferFrom नियम balanceOfConsistency गारंटी को इनहेरिट (inherit) करता है:

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

यदि इस पूर्व-शर्त को हटा दिया जाता है, तो Prover नियम को असंभव स्टेट्स (states) में शुरू कर सकता है जहां ओनरशिप और बैलेंस मेल नहीं खाते हैं — उदाहरण के लिए, किसी एड्रेस को टोकन के ओनर के रूप में दर्ज किया जा सकता है जबकि उसका बैलेंस शून्य है क्योंकि ghost वैल्यूज़ स्टोरेज के साथ अलाइन नहीं होती हैं। इससे फॉल्स पॉजिटिव (false positive) उल्लंघन होते हैं।

require balanceLimited(to)

balanceLimited(to) प्राप्तकर्ता (to) एड्रेस के बैलेंस को max_uint256 से कम रहने तक सीमित करता है, जैसा कि definition में व्यक्त किया गया है:

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

गैस एफिशिएंसी (gas efficiency) के लिए कॉन्ट्रैक्ट एक unchecked ब्लॉक के अंदर बैलेंस बढ़ाता है। हालांकि ओवरफ्लो (overflow) व्यावहारिक रूप से असंभव है, फिर भी Prover ओवरफ्लो मामलों का पता लगाता है क्योंकि transferFrom() _update() को कॉल करता है, जहां बैलेंस में वृद्धि एक unchecked ब्लॉक के अंदर होती है:

Copy
// ERC721.sol

function transferFrom(address from, address to, uint256 tokenId) public virtual {
    ...
    address previousOwner = _update(to, tokenId, _msgSender());
    ..
}

Copy
/// ERC721.sol

function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
    ...

    if (to != address(0)) {
        unchecked {
            _balances[to] += 1;
        }
    }
	  ...
}

require balanceLimited(to) का उपयोग करने से व्यावहारिक रूप से अप्राप्य (unreachable) ओवरफ्लो स्टेट्स को खारिज कर दिया जाता है जो अवास्तविक परिदृश्यों (unrealistic scenarios) में नियम के विफल होने का कारण बन सकती हैं।

प्री-कॉल स्टेट (Pre-call state)

transferFrom() मेथड को इनवोक (invoke) करने से पहले, हम पोस्ट-कॉल वैल्यूज़ (post-call values) के साथ तुलना करने के लिए स्टेट वेरिएबल्स (state variables) रिकॉर्ड करते हैं:

• balanceOfFromBefore ट्रांसफर से पहले सेंडर (from) का बैलेंस है।
• balanceOfToBefore ट्रांसफर से पहले प्राप्तकर्ता (to) का बैलेंस है।
• balanceOfOtherBefore ट्रांसफर से पहले एक गैर-शामिल अकाउंट (otherAccount) का बैलेंस है।
• ownerBefore ट्रांसफर किए जाने वाले टोकन का ओनर है।
• otherOwnerBefore किसी गैर-शामिल टोकन का ओनर है।
• approvalBefore ट्रांसफर किए जाने वाले टोकन के लिए अप्रूवल है।
• otherApprovalBefore किसी गैर-शामिल टोकन का अप्रूवल है।

Copy
uint256 balanceOfFromBefore  = balanceOf(from);
uint256 balanceOfToBefore    = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore          = unsafeOwnerOf(tokenId);
address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
address approvalBefore       = unsafeGetApproved(tokenId);
address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

ध्यान दें कि हम कॉन्ट्रैक्ट के getApproved() के बजाय unsafeGetApproved() का उपयोग करके अप्रूवल (approvals) पढ़ते हैं, जो कि एक हार्नेस (harness) फंक्शन है। हार्नेस वर्ज़न अप्रूवल वैल्यू को तब भी उजागर करता है जब टोकन अनमिंट (unminted) या बर्न (burned) हो चुका हो (owner == address(0)) क्योंकि यह यह जाँचे बिना कि टोकन मौजूद है या उसका कोई ओनर है, _getApproved(tokenId) लौटाता है। इसके विपरीत, वास्तविक कॉन्ट्रैक्ट में getApproved() ओनरशिप चेक करता है और यदि टोकन अनमिंट या बर्न हो गया है तो यह रिवर्ट (revert) हो जाता है:

Copy
// ERC721Harness.sol -- returns approval without checking token existence or ownership

function unsafeGetApproved(uint256 tokenId) external view returns (address) {
    return _getApproved(tokenId);
}

Copy
// ERC721.sol -- performs an ownership check and reverts if the token is unminted or burned

function getApproved(uint256 tokenId) public view virtual returns (address) {
    _requireOwned(tokenId); // reverts if `owner == address(0)`

    return _getApproved(tokenId);
}

यह अनमिंट या बर्न किए गए टोकन की अप्रूवल स्टेट (approval state) को क्वेरी करने से रोकता है क्योंकि getApproved() उन मामलों में रिवर्ट हो जाता है। हालाँकि, नियम को उन स्टेट ट्रांज़िशन (state transitions) में अप्रूवल वैल्यूज़ की तुलना करने की आवश्यकता होती है जो ज़ीरो-एड्रेस स्टेट से होकर गुजरते हैं:

• टोकन निर्माण (अनमिंट से मिंट) — ओनर address(0) से किसी नॉन-ज़ीरो (nonzero) एड्रेस पर ट्रांज़िशन करता है
• टोकन विनाश (मिंट से अनमिंट/बर्न) — ओनर किसी नॉन-ज़ीरो एड्रेस से वापस address(0) पर ट्रांज़िशन करता है

इसलिए, unsafeGetApproved() की आवश्यकता है, ताकि टोकन ज़ीरो-एड्रेस ओनर स्टेट में होने पर भी नियम अप्रूवल वैल्यूज़ को पढ़ सके।

अब जब प्री-कॉल स्टेट रिकॉर्ड कर ली गई है, हम transferFrom() निष्पादित करते हैं और आगे आने वाले असर्शन्स (assertions) में पोस्ट-कॉल वैल्यूज़ के बारे में तर्क (reason) करते हैं।

ट्रांसफर कॉल (Transfer call)

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

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

असर्शन्स (Assertions) — liveness, effect, और no side effect

Liveness:

एक ट्रांसफर रिवर्ट नहीं होता है यदि और केवल यदि (<=>) निम्नलिखित सभी सत्य हों:

• from == ownerBefore

  from एड्रेस (जहाँ से टोकन ट्रांसफर किया जा रहा है) टोकन का पिछला ओनर होना चाहिए।

• from != 0

  from एड्रेस ज़ीरो एड्रेस (zero address) नहीं होना चाहिए।

• to != 0

  to एड्रेस (रिसीवर) ज़ीरो एड्रेस नहीं होना चाहिए।

• (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))

  ऑपरेटर (कॉलर) के पास इनमें से कम से कम एक के माध्यम से ऑथराइजेशन (authorization) होना चाहिए:

  • operator == from — ओनर अपना खुद का टोकन ट्रांसफर करता है
  • operator == approvalBefore — ऑपरेटर के पास इस टोकन के लिए विशिष्ट अप्रूवल है (approve() के माध्यम से)
  • isApprovedForAll(ownerBefore, operator) — ऑपरेटर के पास ओनर के सभी टोकन के लिए ब्लैंकेट अप्रूवल (blanket approval) है (setApprovalForAll() के माध्यम से)

Copy
// liveness
assert success <=> (
    from == ownerBefore &&
    from != 0 &&
    to   != 0 &&
    (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
);

इफेक्ट (Effect):

यदि ट्रांसफर रिवर्ट नहीं होता है, तो निम्नलिखित स्टेट चेंज लागू होते हैं:

• to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0)

  सेंडर (sender) का बैलेंस 1 घट जाता है, सिवाय सेल्फ-ट्रांसफर (from == to) के जहाँ यह अपरिवर्तित रहता है।

• to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1 : 0)

  रिसीवर का बैलेंस 1 बढ़ जाता है, सिवाय सेल्फ-ट्रांसफर (from == to) के जहाँ यह अपरिवर्तित रहता है।

• unsafeOwnerOf(tokenId) == to

  रिसीवर (to) एड्रेस tokenId का नया ओनर बन जाता है।

• unsafeGetApproved(tokenId) == 0

  tokenId के लिए अप्रूवल क्लियर (clear) कर दिया जाता है।

Copy
// effect
assert success => (
    to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
    to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
    unsafeOwnerOf(tokenId)                 == to &&
    unsafeGetApproved(tokenId)             == 0
);

नो साइड इफेक्ट (No side effect):

इच्छित स्टेट चेंज (इफेक्ट) को असर्ट (assert) करने के बाद, हम यह भी जांचते हैं कि बैलेंस, ओनरशिप या अप्रूवल पर कोई अनपेक्षित प्रभाव (unintended effects) न हो:

• बैलेंस पर (On balance)

  balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to)

  यदि किसी अकाउंट का बैलेंस बदलता है, तो इसका तात्पर्य (=>) है कि वह अकाउंट या तो सेंडर है या रिसीवर। किसी अन्य गैर-शामिल अकाउंट का बैलेंस संशोधित (modified) नहीं हुआ।

• ओनरशिप पर (On ownership)

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

  यदि किसी टोकन की ओनरशिप बदलती है, तो इसका तात्पर्य (=>) है कि वह टोकन वही था जिसे ट्रांसफर किया गया था। किसी अन्य गैर-शामिल टोकन की ओनरशिप नहीं बदली।

• अप्रूवल पर (On approval)

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

  यदि किसी टोकन का अप्रूवल बदलता है, तो इसका तात्पर्य (=>) है कि वह टोकन वही था जिसे ट्रांसफर किया गया था। किसी अन्य गैर-शामिल टोकन का अप्रूवल संशोधित नहीं हुआ।

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

यहाँ transferFrom नियम के लिए संपूर्ण स्पेसिफिकेशन्स (specifications) दी गई हैं:

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

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
}

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

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

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

यहाँ Prover run है।

अब जब हमने transferFrom() को वेरिफाई कर लिया है, तो हम अप्रूवल मैकेनिज़्म (approval mechanisms) पर आगे बढ़ सकते हैं जो इन ट्रांसफर को ऑथराइज़ करते हैं।

याद रखें कि transferFrom() तभी सफल होता है जब कॉलर के पास उचित ऑथराइजेशन हो: टोकन ओनर के रूप में, उस टोकन के लिए अप्रूव्ड एड्रेस के रूप में, या ओनर के सभी टोकन के लिए अप्रूव्ड ऑपरेटर के रूप में। अगले दो नियम उन फंक्शन्स को वेरिफाई करते हैं जो ये अनुमतियाँ (permissions) प्रदान करते हैं: प्रति-टोकन ऑथराइजेशन के लिए approve() और ऑपरेटर-लेवल ऑथराइजेशन के लिए setApprovalForAll()।

approve() को फॉर्मली वेरिफाई करना

approve() कॉन्ट्रैक्ट फंक्शन किसी एड्रेस को एक विशिष्ट टोकन ट्रांसफर करने की अनुमति देता है। यह केवल तभी सफल होता है जब टोकन मौजूद हो और कॉलर ओनर या ऑपरेटर हो (जिसके पास ब्लैंकेट अप्रूवल हो)।

यहाँ वह नियम है जो इस व्यवहार को वेरिफाई करता है:

Copy
rule approve(env e, address spender, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);
		
	// pre-call state
    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Preconditions

अब तक, हम पहले से ही जानते हैं कि nonpayable(e) के लिए यह आवश्यक है कि कॉल बिना ईथर (Ether) के भेजी जाए, और authSanity(e) के लिए यह आवश्यक है कि msg.sender ज़ीरो एड्रेस न हो:

Copy
require nonpayable(e);
require authSanity(e);

अप्रूव कॉल (Approve call)

OpenZeppelin के ERC-721 नियम स्पेसिफिकेशन्स में एक सामान्य पैटर्न (pattern) के रूप में, approve मेथड को @withrevert के साथ कॉल किया जाता है, और !lastReverted का परिणाम success वेरिएबल में स्टोर किया जाता है ताकि उस स्थिति के बारे में तर्क किया जा सके जहां कॉल सफल होती है:

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

असर्शन्स (Assertions) — liveness, effect, और no side effect

Liveness:

इसका मतलब है कि फंक्शन कॉल “यदि और केवल यदि (if and only if)” निम्नलिखित शर्तें पूरी होती हैं, तो रिवर्ट नहीं होती है:

• owner != 0

  टोकन ओनर ज़ीरो एड्रेस नहीं होना चाहिए। यह किसी ऐसे टोकन को अप्रूव करने से रोकता है जो मौजूद नहीं है या बर्न (burn) हो गया है।

• (owner == caller || isApprovedForAll(owner, caller))

  यह एक ऑथराइजेशन चेक है जहाँ कॉलर को या तो:

  • टोकन ओनर (owner) होना चाहिए, या
  • isApprovedForAll(owner, caller) (true लौटाता है) के माध्यम से अप्रूव्ड ऑपरेटर होना चाहिए

Copy
// liveness
assert success <=> (
    owner != 0 &&
    (owner == caller || isApprovedForAll(owner, caller))
);

इफेक्ट (Effect):

• assert success => unsafeGetApproved(tokenId) == spender

  यदि कॉल सफल रही (success == true), तो tokenId के लिए अप्रूव्ड एड्रेस अब spender के बराबर होना चाहिए।

Copy
// effect
assert success => unsafeGetApproved(tokenId) == spender;

नो साइड इफेक्ट (No side effect):

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

  यदि otherTokenId के लिए अप्रूव्ड एड्रेस बदलता है, तो otherTokenId, tokenId के समान होना चाहिए। इसका मतलब है कि केवल tokenId (इच्छित लक्ष्य/intended target) का अप्रूवल अपडेट किया गया है और कोई अन्य टोकन (otherTokenId) गलती से प्रभावित नहीं हुआ है।

Copy
// no side effect
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

यहाँ approve नियम के लिए संपूर्ण स्पेसिफिकेशन है:

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

यहाँ Prover run है।

फॉर्मली वेरिफाई करें setApprovalForAll()

setApprovalForAll() फंक्शन किसी एड्रेस को कॉलर के स्वामित्व वाले सभी टोकन प्रबंधित (manage) करने के लिए अधिकृत (authorizes) करता है। यहाँ नियम है:

Copy
rule setApprovalForAll(env e, address operator, bool approved) {
	// preconditions
    require nonpayable(e);
		
	// pre-call state
    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

इस बिंदु पर, हम पहले से ही Preconditions, प्री-कॉल और पोस्ट-कॉल स्टेट्स, और मेथड कॉल के पैटर्न से परिचित हैं, इसलिए हम उन्हें छोड़ देंगे और सीधे असर्शन्स पर जाएंगे।

असर्शन्स (Assertions) — liveness, effect, और no side effect

Liveness:

• assert success <=> operator != 0

  कॉल तभी सफल होती है यदि और केवल यदि ऑपरेटर ज़ीरो एड्रेस नहीं है। ERC-721 ज़ीरो एड्रेस को ऑपरेटर के रूप में अप्रूव करने पर रोक लगाता है, इसलिए यह असर्शन (assertion) operator == 0 होने पर कॉल को विफल होने की आवश्यकता बताता है:

Copy
// liveness
assert success <=> operator != 0;

इफेक्ट (Effect):

• assert success => isApprovedForAll(owner, operator) == approved

  यदि कॉल सफल रही, तो (owner, operator) पेयर (pair) की अप्रूवल स्थिति approved बूलियन वैल्यू (boolean value) से मेल खानी चाहिए। इसका मतलब है कि अप्रूवल वैल्यू (true या false) सही ढंग से सेट की गई थी।

  Copy
  // effect
  assert success => isApprovedForAll(owner, operator) == approved;
  

नो साइड इफेक्ट (No side effect):

• यदि किसी (otherOwner, otherOperator) की अप्रूवल स्थिति बदलती है, तो वे एड्रेस कॉलर (owner) और निर्दिष्ट ऑपरेटर (operator) से मेल खाने चाहिए। किसी भिन्न अप्रूवल एंट्री (entry) में कोई भी बदलाव इस असर्शन को विफल कर देता है।

Copy
// no side effect
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
    otherOwner    == owner &&
    otherOperator == operator
);

यहाँ setApprovalForAll नियम के लिए पूर्ण CVL स्पेसिफिकेशन है:

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

यहाँ Prover run है।

फॉर्मली वेरिफाई करें कि balanceOf(0) रिवर्ट होता है

निम्नलिखित नियम यह वेरिफाई करता है कि ज़ीरो एड्रेस को क्वेरी करने पर balanceOf फंक्शन हमेशा रिवर्ट (revert) होता है।

नीचे balanceOf का कॉन्ट्रैक्ट इम्प्लीमेंटेशन है। यदि owner == address(0) हो, तो यह रिवर्ट होता है:

Copy
function balanceOf(address owner) public view virtual returns (uint256) {
    if (owner == address(0)) {
        revert ERC721InvalidOwner(address(0));

    }
    return _balances[owner];
}

यहाँ वह नियम है जो इस व्यवहार को वेरिफाई करता है:

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

यहाँ Prover run है:

ट्रांसफर और अप्रूवल के लिए पूर्ण स्पेसिफिकेशन

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

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

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
}

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

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

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