परिचय
यह अध्याय OpenZeppelin’s ERC-721 CVL specification के कोड वॉकथ्रू का अंतिम भाग (5/5) है, जो औपचारिक रूप से (formally) निम्नलिखित नियमों को सत्यापित करता है:
-
supplyChangeTotal supply केवल mint या burn ऑपरेशन्स के माध्यम से बदलती है, और वह भी ठीक एक (exactly one) से।
-
balanceChangeअकाउंट का बैलेंस केवल mint, burn, या transfer ऑपरेशन्स के माध्यम से बदलता है, और वह भी ठीक एक से।
-
ownershipChangeटोकन का स्वामित्व (ownership) केवल mint, burn, या transfer ऑपरेशन्स के माध्यम से बदलता है।
-
approvalChangeप्रति-टोकन अप्रूवल (Per-token approval) केवल
approve()कॉल के माध्यम से या burn या transfer ऑपरेशन्स के साइड इफेक्ट के रूप में बदलता है। -
approvedForAllChangeऑपरेटर अप्रूवल केवल
setApprovalForAll()कॉल के माध्यम से बदलता है।
ये नियम एक partially parametric rule पैटर्न का उपयोग करते हैं (जिस पर अगले भाग में चर्चा की जाएगी), जो “Introduction to Parametric Rules” अध्याय में कवर किए गए parametric rules कॉन्सेप्ट पर आधारित है।
इस अध्याय की प्रॉपर्टीज पिछले अध्यायों से भिन्न हैं। पहले, हमने विशिष्ट मेथड व्यवहारों को सत्यापित किया था: क्या mint() total supply बढ़ाता है? क्या transferFrom() उम्मीद के मुताबिक बैलेंस को अपडेट करता है? उन प्रॉपर्टीज ने सामान्य (non-parametric) नियमों का उपयोग करके व्यक्तिगत मेथड्स का परीक्षण किया।
यहाँ की प्रॉपर्टीज एक अलग सवाल पूछती हैं: कौन से methods किसी विशेष state (जैसे total supply या किसी अकाउंट का बैलेंस) को बदल सकते हैं, और क्या हम यह पुष्टि कर सकते हैं कि कोई अन्य methods ऐसा नहीं करते हैं? सामान्य नियम इसका उत्तर नहीं दे सकते क्योंकि वे एक बार में एक मेथड का परीक्षण करते हैं। यहां तक कि प्रति प्रॉपर्टी प्रति मेथड एक नियम के साथ भी, हम यह सत्यापित नहीं कर सकते कि जो मेथड्स लिस्टेड नहीं हैं, वे बदलाव का कारण नहीं बनते हैं।
कोई पूछ सकता है कि क्या CVL invariants एक ही उद्देश्य की पूर्ति कर सकते हैं। हालाँकि, CVL invariants यहाँ उपयुक्त नहीं हैं क्योंकि वे यह कैप्चर नहीं कर सकते कि किसी मेथड कॉल के दौरान कोई वैल्यू कैसे बदलती है। Invariants pre-call वैल्यूज तक पहुँच नहीं सकते या उनकी तुलना post-call वैल्यूज से नहीं कर सकते, इसलिए वे ऐसी प्रॉपर्टीज को व्यक्त नहीं कर सकते जैसे “यह state केवल तभी बदल सकती है जब विशिष्ट methods को कॉल किया जाता है” या “यह state ठीक इस मात्रा से बदलती है।” ये state-transition प्रॉपर्टीज हैं, जिनके लिए pre-call और post-call state के बारे में तर्क (reasoning) करने की आवश्यकता होती है।
एक parametric पैटर्न सभी कॉन्ट्रैक्ट मेथड्स को एक ही नियम में टेस्ट करके और pre-call और post-call state के बारे में तर्क करके इसे हल करता है। इससे दोनों को सत्यापित करना संभव हो जाता है: किन मेथड्स को state बदलने की अनुमति है और कोई अन्य मेथड्स वही बदलाव नहीं कर सकते हैं।
Partially Parametric Rule
पिछले अध्याय, “Introduction To Parametric Rules” में, हमने सीखा था कि:
“… एक parametric rule यह सत्यापित करता है कि किसी भी फ़ंक्शन को किसी भी मान्य आर्ग्यूमेंट्स के साथ कॉल किए जाने के बाद भी कोई प्रॉपर्टी सही (true) बनी रहती है।”
मुख्य वाक्यांश है: ”after any function is called with any valid arguments,” जो निम्नलिखित कोड पैटर्न के अनुरूप है:
rule parametricExample(env e, method f, calldataarg args) {
/// set precondition
/// record pre-call state
/// parametric call: invokes all functions in the scene with arbitrary arguments
f(e, args);
/// record post-call state
/// assertions
}
यह पैटर्न (fully parametric) तब अच्छी तरह काम करता है जब सभी मेथड्स पर समान preconditions लागू होती हैं। हालाँकि, यह तब उपयुक्त नहीं होता जब अलग-अलग मेथड्स को अलग-अलग बाधाओं (constraints) की आवश्यकता होती है।
Fully parametric f(e, args) के बजाय, हम एक “partially parametric” पैटर्न का उपयोग कर सकते हैं। यह CVL सिंटैक्स नहीं है, बल्कि एक स्पेसिफिकेशन डिज़ाइन पैटर्न है। जैसा कि Certora documentation वर्णन करता है:
“यह partially parametric rule लागू किए गए मेथड के प्रकार के आधार पर कंडीशनल लॉजिक को प्रदर्शित करता है, जो स्मार्ट कॉन्ट्रैक्ट के भीतर विभिन्न परिदृश्यों (scenarios) के अनुरूप विशिष्ट क्रियाओं (actions) और assertions की अनुमति देता है।”
मुख्य वाक्यांश है “specific actions and assertions tailored to different scenarios”, जो निम्नलिखित कोड पैटर्न के अनुरूप है:
rule partiallyParametricExample(env e) {
method f;
if (f.selector == sig:exampleMethod1(uint256, address).selector) {
// method-specific logic
}
else if (f.selector == sig:exampleMethod2(address, address).selector) {
// method-specific logic
}
else {
// method-specific logic
}
}
मेथड-विशिष्ट लॉजिक (method-specific logic) preconditions, मेथड कॉल्स, या यहाँ तक कि assertions भी हो सकते हैं। साफ़ कोड (cleaner code) के लिए, इन कंडीशनल स्टेटमेंट्स को एक CVL फ़ंक्शन में एब्स्ट्रैक्ट किया जा सकता है, जैसा कि नीचे दिखाया गया है:
rule partiallyParametricExample(env e) {
method f;
helperFunction(e, f); // contains all conditional logic
}
OpenZeppelin का स्पेसिफिकेशन इस पैटर्न को लागू करने के लिए हेल्पर फ़ंक्शन helperSoundFnCall() का उपयोग करता है। यहाँ supplyChange नियम का एक उदाहरण दिया गया है (जिसकी हम बाद में विस्तार से जाँच करेंगे):
/// ERC721.spec
rule supplyChange(env e) {
...
method f; helperSoundFnCall(e, f);
...
/// assert
/// assert
}
helperSoundFnCall() में “Sound” जानबूझकर रखा गया है। Soundness का अर्थ है कि वेरिफिकेशन किसी भी वास्तविक बग (real bugs) को नज़रअंदाज़ नहीं करता है, और unsoundness का एक सामान्य कारण अत्यधिक प्रतिबंधात्मक preconditions के माध्यम से मान्य निष्पादन पथों (valid execution paths) को बाहर करना है।
यह हेल्पर f(e, args) को एक sound तरीके से रूट करता है, जिसके लिए यह सभी कॉल्स पर विश्व स्तर (globally) पर preconditions लागू करने के बजाय, लागू किए गए मेथड के आधार पर चुनिंदा रूप से preconditions लगाता है। जिन मेथड्स को इसकी आवश्यकता नहीं है, उन पर precondition लागू करने से मान्य निष्पादन पथ बाहर हो जाएंगे।
अगले भाग में, हम देखेंगे कि कैसे आर्बिट्रेरी मेथड कॉल f(e, args) को उपयुक्त मेथड-विशिष्ट preconditions पर रूट किया जाता है जो स्पेसिफिकेशन को sound बनाए रखते हैं।
helperSoundFnCall() सही मेथड ब्रांच में f(e, args) कॉल को रूट करता है
CVL फ़ंक्शन helperSoundFnCall() फ़ंक्शन सिलेक्टर से मिलान करके आर्बिट्रेरी मेथड कॉल f(e, args) को सही मेथड ब्रांच में रूट करता है। प्रत्येक मिलान किए गए सिलेक्टर के लिए, CVL हेल्पर फ़ंक्शन निम्नलिखित कार्य करता है:
- आवश्यक आर्ग्यूमेंट्स को डिक्लेयर (declare) करता है,
- मेथड-विशिष्ट preconditions लागू करता है, और
- संबंधित कंक्रीट फ़ंक्शन (concrete function) को कॉल करता है।
mint ऑपरेशन्स के लिए — mint(), safeMint(), और safeMint(bytes)
जब लागू किया गया फ़ंक्शन एक mint वैरिएंट होता है, तो हेल्पर फ़ंक्शन:
- आवश्यक आर्ग्यूमेंट्स डिक्लेयर करता है:
address to,uint256 tokenId, और बाइट्स (bytes) वैरिएंट के लिए,bytes data। - मेथड-विशिष्ट preconditions लागू करता है:
require balanceLimited(to)— ओवरफ्लो को रोकने के लिए प्राप्तकर्ता (recipient) के बैलेंस कोmax_uint256के अंतर्गत सीमित करता है।require data.length < 0xffff— Prover निष्पादन के दौरान अवास्तविक रूप से बड़े एरेज़ (arrays) से बचने के लिए डेटा की लंबाई को 65,535 बाइट्स (0xffff) से कम तक सीमित करता है।
- संबंधित फ़ंक्शन्स को कॉल करता है:
mint(e, to, tokenId),safeMint(e, to, tokenId)याsafeMint(e, to, tokenId, data)।
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
}
else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
}
else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
}
...
}
burn ऑपरेशन के लिए — burn()
जब लागू किया गया फ़ंक्शन burn() होता है, तो हेल्पर फ़ंक्शन:
-
आवश्यक आर्ग्यूमेंट
uint256 tokenIdको डिक्लेयर करता है। -
मेथड-विशिष्ट precondition
requireInvariant ownerHasBalance(tokenId)लागू करता है, जिसके लिए यह आवश्यक है कि burn से पहले टोकन मौजूद हो (उसका एक nonzero owner हो)। -
संबंधित फ़ंक्शन
burn(e, tokenId)को कॉल करता है।function helperSoundFnCall(env e, method f) { ... } else if (f.selector == sig:burn(uint256).selector) { uint256 tokenId; requireInvariant ownerHasBalance(tokenId); // requireInvariant notMintedUnset(tokenId); burn(e, tokenId); } ... }
transfer ऑपरेशन्स के लिए — transferFrom(), safeTransferFrom(), और safeTransferFrom(bytes)
जब लागू किया गया फ़ंक्शन एक transfer वैरिएंट होता है, तो हेल्पर फ़ंक्शन:
- आवश्यक आर्ग्यूमेंट्स डिक्लेयर करता है:
address from,address to,uint256 tokenId, और बाइट्स वैरिएंट के लिए,bytes data। - मेथड-विशिष्ट preconditions लागू करता है:
require balanceLimited(to)— Prover को अवास्तविक प्राप्तकर्ता बैलेंस को एक्सप्लोर करने से रोकने के लिए प्राप्तकर्ता के बैलेंस को सख्ती सेmax_uint256से कम तक सीमित करता है।requireInvariant ownerHasBalance(tokenId)— यह सुनिश्चित करता है कि ट्रांसफर किए जाने से पहले टोकन मौजूद है। इसके बिना, Prover उन मामलों पर विचार करेगा जहां टोकन को शून्य पते (zero address) से ट्रांसफर किया जाता है।requireInvariant notMintedUnset(tokenId)— किसी बिना मिंट (unminted) किए गए टोकन के लिए किसी भी अप्रूवल को खारिज करता है। इसके बिना, Prover एक गैर-मौजूद (nonexistent) टोकन को ऐसे मान सकता है जैसे कि इसका कोई अप्रूव्ड ऑपरेटर हो।require data.length < 0xffff— (केवल बाइट्स वैरिएंट के लिए) Prover निष्पादन के दौरान अवास्तविक रूप से बड़े एरेज़ से बचने के लिए डेटा की लंबाई को 65,535 बाइट्स (0xffff) से कम तक सीमित करता है।
- संबंधित फ़ंक्शन्स को कॉल करता है:
transferFrom(),safeTransferFrom(),safeTransferFrom(bytes)
function helperSoundFnCall(env e, method f) {
...
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
...
}
mint, burn और transfer के अलावा अन्य सभी ऑपरेशन्स के लिए
mint, burn, या transfer के अलावा अन्य फ़ंक्शन्स को आर्बिट्रेरी आर्ग्यूमेंट्स के साथ पूरी तरह से पैरामेट्रिक कॉल (fully parametric call) f(e, args) के साथ हैंडल किया जाता है:
function helperSoundFnCall(env e, method f) {
...
} else {
calldataarg args;
f(e, args);
}
}
CVL फ़ंक्शन helperSoundFnCall() का पूर्ण कार्यान्वयन (Complete implementation)
यहाँ पूरा हेल्पर CVL फ़ंक्शन दिया गया है:
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
} else if (f.selector == sig:burn(uint256).selector) {
uint256 tokenId;
requireInvariant ownerHasBalance(tokenId);
// requireInvariant notMintedUnset(tokenId);
burn(e, tokenId);
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
} else {
calldataarg args;
f(e, args);
}
}
नोट: mint और burn ब्रांचेस में हमने requireInvariant notMintedUnset(tokenId) को कमेंट आउट कर दिया है ताकि केवल उन preconditions को दिखाया जा सके जो प्रत्येक लागू किए गए मेथड के लिए सख्त रूप से आवश्यक हैं। इसका मतलब यह नहीं है कि invariant बेकार है — क्योंकि यह स्पेसिफिकेशन में एक अलग invariant के रूप में साबित होता है, यह माना जा सकता है कि यह हमेशा सही होता है और इसे सुरक्षित रूप से फिर से बहाल (reinstate) किया जा सकता है। इसे एक precondition के रूप में जोड़ने से आमतौर पर Prover के रन टाइम कम हो जाते हैं।
helperSoundFnCall() में मेथड-विशिष्ट preconditions को हैंडल करने के साथ, अब हम अगले भाग में नियम चर्चाओं (rule discussions) की ओर बढ़ सकते हैं।
supplyChange — total supply केवल mint(), safeMint(), safeMint(bytes) और burn() के माध्यम से बदल सकती है
यह नियम सत्यापित करता है कि कौन से कॉन्ट्रैक्ट मेथड्स total supply को 1 से बढ़ा या घटा सकते हैं। यहाँ वह नियम है जो इस व्यवहार को कैप्चर करता है, जिस पर हम आगे विस्तार से चर्चा करेंगे:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
assert supplyAfter > supplyBefore => (
supplyAfter == supplyBefore + 1 &&
(
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
)
);
assert supplyAfter < supplyBefore => (
supplyAfter == supplyBefore - 1 &&
f.selector == sig:burn(uint256).selector
);
}
Prover रन: link
Preconditions
-
require nonzerosender(e)यह precondition कॉलर को nonzero होने के लिए बाध्य करती है। इस बाधा के बिना, Prover उन निष्पादनों का पता लगा सकता है जिनमें एक ट्रांसफर
address(0)से उत्पन्न होता है और एक टोकन को nonzero एड्रेस पर ले जाता है, जो प्रभावी रूप से एक ट्रांसफर ऑपरेशन के माध्यम से निष्पादित किया गया एक mint है। -
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)यह invariant precondition
address(0)को ऑपरेटरों को अप्रूव करने से रोकती है। इस बाधा के बिना, Prover उन states का पता लगा सकता है जिनमेंaddress(0)ने nonzero एड्रेसेस को ऑपरेटर अनुमतियां (permissions) दी हैं।
Pre-call और post-call states
-
supplyBefore = _supplyPartially parametric कॉल (
method f; helperSoundFnCall(e, f)) को निष्पादित करने से पहले total supply को रिकॉर्ड करता है। -
method f; helperSoundFnCall(e, f)पहले चर्चा की गई partially parametric कॉल को निष्पादित करता है।
-
mathint supplyAfter = _supplyPartially parametric कॉल को निष्पादित करने के बाद total supply को रिकॉर्ड करता है।
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
ERC-721 total supply को ट्रैक नहीं करता है, इसलिए हम एक घोस्ट वेरिएबल (ghost variable) _supply का उपयोग करते हैं जो एक Sstore हुक के माध्यम से सभी _balances के योग (sum) को ट्रैक करता है:
ghost mathint _supply {
init_state axiom _supply == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
Assertions
-
पहला assertion यह बताता है कि यदि total supply बढ़ती है (
supplyAfter > supplyBefore), तो यह वृद्धि ठीक 1 होनी चाहिए और यह केवलmint(),safeMint(), याsafeMint(bytes)के कारण हो सकती है:rule supplyChange(env e) { ... assert supplyAfter > supplyBefore => ( supplyAfter == supplyBefore + 1 && ( f.selector == sig:mint(address,uint256).selector || f.selector == sig:safeMint(address,uint256).selector || f.selector == sig:safeMint(address,uint256,bytes).selector ) ); ... } -
दूसरा assertion burn केस को कवर करता है। यदि total supply कम हो जाती है (
supplyAfter < supplyBefore), तो यह कमी ठीक 1 होनी चाहिए और यह केवलburn()के कारण हो सकती है:rule supplyChange(env e) { ... assert supplyAfter < supplyBefore => ( supplyAfter == supplyBefore - 1 && f.selector == sig:burn(uint256).selector ); }
balanceChange — अकाउंट के बैलेंस केवल mint, burn और transfer ऑपरेशन्स के माध्यम से ही बदल सकते हैं
निम्नलिखित नियम बैलेंस में बदलाव के बारे में दो प्रॉपर्टीज को सत्यापित करता है:
- बैलेंस प्रति ऑपरेशन ठीक एक टोकन से बदलता है
- केवल mint, burn, या transfer ऑपरेशन्स ही बैलेंस बदल सकते हैं
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
// requireInvariant balanceOfConsistency(account);
// require balanceLimited(account);
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
}
Prover रन: link
Preconditions
requireInvariant balanceOfConsistency(account) और require balanceLimited(account) को कमेंट आउट किया गया है क्योंकि helperSoundFnCall() पहले से ही सभी बैलेंस बदलने वाले मेथड्स के लिए इन preconditions को लागू करता है। balanceOfConsistency को burn और transfer ब्रांचेस में ownerHasBalance invariant के preserved ब्लॉक के माध्यम से लागू किया जाता है।
Pre-call और post-call states
नियम helperSoundFnCall(e, f) कॉल के पहले और बाद में अकाउंट बैलेंस को रिकॉर्ड करता है ताकि वैल्यूज की तुलना की जा सके और यह निर्धारित किया जा सके कि क्या मेथड कॉल ने बैलेंस को बदल दिया है, और कितने से:
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
Assertions
पहला assertion यह बताता है कि यदि helperSoundFnCall(e, f) कॉल के बाद किसी अकाउंट का बैलेंस बदलता है (balanceBefore != balanceAfter), तो परिवर्तन प्लस या माइनस एक होना चाहिए — न उससे अधिक, न कम।
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
दूसरा assertion बताता है कि केवल निम्नलिखित फ़ंक्शन्स ही बैलेंस बदल सकते हैं:
- mint फ़ंक्शन्स (
mint(),safeMint(),safeMint(bytes)) - burn (
burn()) - transfer फ़ंक्शन्स (
transferFrom(),safeTransferFrom(),safeTransferFrom(bytes))
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
यदि लिस्ट में शामिल न होने वाला कोई अन्य फ़ंक्शन बैलेंस में बदलाव का कारण बनता है, तो assertion विफल (fail) हो जाएगा और Prover एक उल्लंघन (violation) की रिपोर्ट करेगा।
ownershipChange() — स्वामित्व (ownership) केवल mint, burn और transfer ऑपरेशन्स के माध्यम से ही बदल सकता है
निम्नलिखित नियम यह सत्यापित करता है कि किसी टोकन का स्वामित्व (ownerOf(tokenId)) केवल mint, burn, या transfer ऑपरेशन्स के माध्यम से ही बदल सकता है। ऑपरेशन का प्रकार इस बात पर निर्भर करता है कि मालिक (owner) का एड्रेस कैसे बदलता है:
- शून्य एड्रेस (zero address) से nonzero एड्रेस तक — एक mint को दर्शाता है, जो केवल
mint(),safeMint(), याsafeMint(bytes)के कारण हो सकता है। - एक nonzero एड्रेस से शून्य एड्रेस तक — एक burn को दर्शाता है, जो केवल
burn()के कारण हो सकता है। - एक nonzero एड्रेस से दूसरे nonzero एड्रेस तक — एक ट्रांसफर को दर्शाता है, जो केवल
transferFrom(),safeTransferFrom(), याsafeTransferFrom(bytes)के कारण हो सकता है।
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
assert ownerBefore == 0 && ownerAfter != 0 => (
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
);
assert ownerBefore != 0 && ownerAfter == 0 => (
f.selector == sig:burn(uint256).selector
);
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);
}
Prover रन: link
Preconditions
-
require nonzerosender(e)यह precondition मांग करती है कि कॉलर (
e.msg.sender) nonzero हो। इसके बिना, Prover उन निष्पादनों को मॉडल कर सकता है जहांaddress(0)सीधेtransferFromको कॉल करता है, जोaddress(0)से स्वामित्व बनाता है, और उस नियम का उल्लंघन करता है कि केवल mint फ़ंक्शन्स ही ऐसा कर सकते हैं। -
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)
यह invariant precondition शून्य एड्रेस को किसी भी ऑपरेटर को अप्रूव करने से रोकती है। इसके बिना, Prover यह मान सकता है किaddress(0)ने एक nonzero ऑपरेटर को अप्रूव कर दिया है। यहtransferFrom(from = address(0), ...)को तब भी सफल होने देता है जब कॉलर nonzero होता है, जो शून्य एड्रेस से एक स्वामित्व ट्रांज़िशन (ownership transition) बनाता है और इस नियम का उल्लंघन करता है कि केवल mint फ़ंक्शन्स ही स्वामित्व बना सकते हैं।
Pre-call और post-call states
ये लाइनें helperSoundFnCall(e, f) से पहले और बाद में टोकन के मालिक (owner) को रिकॉर्ड करती हैं:
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
unsafeOwnerOf(tokenId) का उपयोग करने से नियम को स्वामित्व परिवर्तन के बारे में तर्क करने की अनुमति मिलती है, तब भी जब टोकन मौजूद नहीं होता है, जिस स्थिति में मालिक address(0) होता है।
Assertions
-
assert ownerBefore == 0 && ownerAfter != 0 => (...)यदि स्वामित्व शून्य एड्रेस से nonzero एड्रेस में बदलता है, जिसका अर्थ है कि एक mint हुआ है, तो केवल निम्नलिखित फ़ंक्शन्स ही इसका कारण हो सकते हैं:
mint(),safeMint(), याsafeMint(bytes):assert ownerBefore == 0 && ownerAfter != 0 => ( f.selector == sig:mint(address,uint256).selector || f.selector == sig:safeMint(address,uint256).selector || f.selector == sig:safeMint(address,uint256,bytes).selector ); -
assert ownerBefore != 0 && ownerAfter == 0 => (...)यदि स्वामित्व nonzero से शून्य एड्रेस में बदलता है, जिसका अर्थ है कि burn हुआ है, तो इसके लिए केवल
burn()फ़ंक्शन ज़िम्मेदार है:assert ownerBefore != 0 && ownerAfter == 0 => ( f.selector == sig:burn(uint256).selector ); -
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (...)अंत में, यदि परिवर्तन एक nonzero एड्रेस से दूसरे nonzero एड्रेस पर है, तो एक ट्रांसफर हुआ है। इन परिवर्तनों के लिए केवल
transferFrom(),safeTransferFrom(), औरsafeTransferFrom(bytes)ज़िम्मेदार हैं:assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => ( f.selector == sig:transferFrom(address,address,uint256).selector || f.selector == sig:safeTransferFrom(address,address,uint256).selector || f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector );
approvalChange() — अप्रूवल केवल approve, transferFrom और burn फ़ंक्शन्स के माध्यम से बदलता है
निम्नलिखित नियम सत्यापित करता है कि किसी विशिष्ट टोकन (getApproved(tokenId)) का अप्रूवल केवल तीन तरीकों से बदल सकता है:
- सीधे
approve()फ़ंक्शन को कॉल करके सेट किया गया हो - ट्रांसफर के साइड-इफेक्ट के रूप में
address(0)पर रीसेट किया गया हो - burn के साइड-इफेक्ट के रूप में
address(0)पर रीसेट किया गया हो
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
}
Prover रन: link
Pre-call और post-call states
नीचे दी गई लाइन partially parametric कॉल method f; helperSoundFnCall(e, f) से पहले और बाद में अप्रूव्ड एड्रेस को रिकॉर्ड करती है ताकि यह निर्धारित किया जा सके कि लिस्टेड लागू किए गए मेथड के परिणामस्वरूप अप्रूवल बदला है या नहीं, और क्या इसे address(0) पर क्लियर किया गया था:
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
Assertion
यह assertion बताता है कि अप्रूव्ड एड्रेस में परिवर्तन केवल तभी हो सकता है यदि:
- फ़ंक्शन कॉल
approve()है, जो स्पष्ट रूप से (explicitly) अप्रूव्ड एड्रेस सेट करता है, या - फ़ंक्शन कॉल
transferFrom(),safeTransferFrom()(बाइट्स डेटा के साथ या उसके बिना), याburn()है, और अप्रूव्ड एड्रेस को एक साइड इफेक्ट के रूप मेंaddress(0)(approvalAfter == 0) पर क्लियर किया जाता है।
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
Assertion विफल (fail) हो जाएगा यदि:
- नियम में लिस्टेड न होने वाला कोई फ़ंक्शन अप्रूव्ड एड्रेस को क्लियर या मॉडिफाई करता है।
transferFrom,safeTransferFrom, याburnअप्रूव्ड एड्रेस कोaddress(0)पर क्लियर नहीं करते हैं।
approvedForAllChange — approval for all केवल setApprovalForAll() फ़ंक्शन के माध्यम से ही बदलता है
यह नियम सत्यापित करता है कि किसी स्पेंडर (spender) का approved-for-all स्टेटस (isApprovedForAll(owner, spender)) केवल setApprovalForAll() फ़ंक्शन को स्पष्ट कॉल के माध्यम से ही बदल सकता है:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}
Prover रन: link
Pre-call और post-call states
-
bool approvedForAllBefore = isApprovedForAll(owner, spender);यह
helperSoundFnCall(e, f)कॉल से पहले approved-for-all स्टेटस को रिकॉर्ड करता है। -
bool approvedForAllAfter = isApprovedForAll(owner, spender);यह
helperSoundFnCall(e, f)कॉल के बाद approved-for-all स्टेटस को रिकॉर्ड करता है।
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
Assertion
यदि स्पेंडर के लिए approved-for-all स्टेटस बदलता है, तो इसका एकमात्र कारण setApprovalForAll() को कॉल करना है:
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
approve() के विपरीत, जो ट्रांसफर या burn पर रीसेट हो जाता है, isApprovedForAll mint, ट्रांसफर, या burn के दौरान नहीं बदलता है। केवल setApprovalForAll को किया गया एक स्पष्ट कॉल ही इसे मॉडिफाई कर सकता है। यदि कोई अन्य फ़ंक्शन इस state को बदलता है, तो assertion विफल हो जाता है और Prover एक उल्लंघन की रिपोर्ट करता है।
Full specifications
यहाँ partially parametric नियमों के लिए पूरा स्पेसिफिकेशन दिया गया है:
methods {
function balanceOf(address) external returns (uint256) envfree;
function ownerOf(uint256) external returns (address) envfree;
function isApprovedForAll(address,address) external returns (bool) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function unsafeGetApproved(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helper │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
} else if (f.selector == sig:burn(uint256).selector) {
uint256 tokenId;
requireInvariant ownerHasBalance(tokenId);
// requireInvariant notMintedUnset(tokenId);
burn(e, tokenId);
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
} else {
calldataarg args;
f(e, args);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
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];
// {
// preserved {
// require balanceLimited(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.3.1
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
assert supplyAfter > supplyBefore => (
supplyAfter == supplyBefore + 1 &&
(
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
)
);
assert supplyAfter < supplyBefore => (
supplyAfter == supplyBefore - 1 &&
f.selector == sig:burn(uint256).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
// requireInvariant balanceOfConsistency(account);
// require balanceLimited(account);
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
assert ownerBefore == 0 && ownerAfter != 0 => (
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
);
assert ownerBefore != 0 && ownerAfter == 0 => (
f.selector == sig:burn(uint256).selector
);
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}
Prover रन: link
partially parametric या fully parametric के उपयोग के बीच के अंतर पर एक नोट
इन state-change प्रॉपर्टीज को या तो एक सिंगल partially parametric rule या कई fully parametric rules (प्रति प्रॉपर्टी एक) का उपयोग करके सत्यापित किया जा सकता है। दोनों दृष्टिकोण (approaches) सभी कॉन्ट्रैक्ट मेथड्स में state में बदलाव के बारे में तर्क करने के लिए method f का उपयोग करते हैं, लेकिन वे preconditions के स्कोप के मामले में भिन्न हैं।
एक fully parametric rule में, सभी preconditions नियम के स्तर पर लागू होती हैं और इसलिए हर संभावित मेथड लागूकरण (invocation) को सीमित करती हैं। यह तब अच्छी तरह काम करता है जब सत्यापित की जा रही state को प्रभावित करने वाले सभी मेथड्स पर समान preconditions लागू होती हैं।
दूसरी ओर, एक partially parametric rule लागू किए गए मेथड के आधार पर कंडीशनल लॉजिक का उपयोग करता है। सभी मेथड लागूकरणों (invocations) पर preconditions लगाने के बजाय, यह आर्बिट्रेरी मेथड कॉल को मेथड-विशिष्ट ब्रांचेस में रूट करता है, जिनमें से प्रत्येक की अपनी प्रासंगिक (relevant) preconditions होती हैं। Preconditions केवल वहीं लागू होती हैं जहाँ उनकी आवश्यकता होती है, जो तब अच्छी तरह से काम करता है जब कोई नियम कई assertions को सत्यापित करता है जिन्हें अलग-अलग मेथड-विशिष्ट बाधाओं (constraints) की आवश्यकता होती है।
उनके बीच का चुनाव मुख्य रूप से कोड ऑर्गनाइज़ेशन के बारे में है: partially parametric rules मेथड-विशिष्ट लॉजिक को केंद्रीकृत (centralize) करते हैं, जबकि fully parametric rules चिंताओं (concerns) को स्वतंत्र नियमों में अलग करते हैं। यह संगठनात्मक अंतर मेंटेनेंस (maintainability) और स्पष्टता (clarity) को प्रभावित करता है, लेकिन दोनों दृष्टिकोण (approaches) समान रूप से मान्य हैं जब preconditions को उचित रूप से स्कोप किया जाता है।
यह लेख formal verification using the Certora Prover पर एक श्रृंखला का हिस्सा है।