Introduction
इम्प्लीकेशन ऑपरेटर (implication operator) का उपयोग अक्सर if स्टेटमेंट के विकल्प के रूप में किया जाता है क्योंकि यह अधिक स्पष्ट (cleaner) होता है।
निम्नलिखित उदाहरण पर विचार करें: एक फ़ंक्शन mod(x, y) जो दो अनसाइंड इंटीजर्स (unsigned integers) को पैरामीटर के रूप में लेता है और x मॉड्यूलो (modulo) y रिटर्न करता है। मॉड्यूलो ऑपरेशन x को y से विभाजित करने पर शेषफल (remainder) की गणना करता है।
इस फ़ंक्शन का Solidity कार्यान्वयन (implementation) इस प्रकार है:
/// Solidity
function mod(uint256 x, uint256 y) external pure returns (uint256) {
return x % y;
}
मान लीजिए कि हम इस प्रॉपर्टी को औपचारिक रूप से (formally) वेरीफाई करना चाहते हैं: “यदि x < y है, तो मॉड्यूलो x के बराबर होना चाहिए।” इसे CVL में व्यक्त करने के लिए if स्टेटमेंट का उपयोग करने से एक कम्पाइलेशन एरर (compilation error) होता है, क्योंकि किसी रूल का अंतिम स्टेटमेंट या तो assert या satisfy होना चाहिए:
/// this rule will not compile
rule mod_ifXLessThanY_resultIsX_usingIf() {
uint256 x;
uint256 y;
mathint result = mod(x, y);
if (x < y) {
assert result == x;
}
}
ERROR
: Failed to run Certora Prover locally. Please check the errors below for problems in the specifications (.spec files) or the prover_args defined in the .conf file.
CRITICAL
: [main] ERROR ALWAYS - Found errors in certora/specs/ImplicationOperator.spec:
CRITICAL
: [main] ERROR ALWAYS - Error in spec file (ImplicationOperator.spec:15:5): last statement of the rule mod_ifXLessThanY_resultIsX_usingIf is not an assert or satisfy command (but must be)
इसे हल करने के लिए, एक उपाय (workaround) अंत में एक सामान्य (trivial) assertion जोड़ना है:
if (P) {
assert Q;
}
assert true;
rule mod_ifXLessThanY_resultIsX_usingIf() {
uint256 x;
uint256 y;
mathint result = mod(x, y);
if (x < y) {
assert result == x;
}
assert true; // trivially TRUE
}
हालाँकि, यह समाधान एक अर्थहीन assertion पेश करता है जो स्पेसिफिकेशन (specification) को अव्यवस्थित (clutter) कर देता है। एक और उपाय if-else स्टेटमेंट का उपयोग करना है, जहाँ else ब्रांच सार्थक assertions को एक्सीक्यूट करती है:
if (P) {
assert Q;
} else {
assert (something_else);
}
rule mod_ifXLessThanY_resultIsX_usingIfElse() {
uint256 x;
uint256 y;
mathint result = mod(x, y);
if (x < y) {
assert result == x;
} else {
assert result != x;
}
}
हालाँकि, हम मूल रूप से यह assert करने में रुचि नहीं रखते थे कि: “यदि x >= y है, तो result != x।” कई मामलों में, जैसा कि ऊपर दिखाया गया है, हम हर संभव ब्रांच के लिए एक assertion बनाने में रुचि नहीं रखते हैं।
Implication (=>) In CVL
इसे शानदार ढंग से (elegantly) संभालने के लिए, हम इम्प्लीकेशन ऑपरेटर (=>) का उपयोग करते हैं। इम्प्लीकेशन के साथ, हम if-else स्टेटमेंट्स की कंट्रोल फ्लो जटिलता (control flow complexity) से बचते हुए शर्तों को संक्षेप में व्यक्त कर सकते हैं।
इस प्रकार, if (P) assert Q लिखने के बजाय (जो कम्पाइल नहीं होता है), हम समान रूप से assert P => Q का उपयोग कर सकते हैं:
rule mod_ifXLessThanY_thenResultIsX() {
uint256 x;
uint256 y;
mathint result = mod(x, y);
assert x < y => result == x;
}
Prove run: link
P => Q के रूप को “यदि P, तो Q”, या सरलता से, “P, Q को इम्प्लाई करता है (P implies Q)” के रूप में पढ़ा जाता है। ध्यान दें कि Q => P आवश्यक रूप से समतुल्य (equivalent) नहीं है, जैसा कि हम अगले सेक्शन में देखेंगे।
P Implies Q P => Q
आइए एक और उदाहरण लें: Solady’s gas-optimized max function। जैसा कि पिछले अध्याय में चर्चा की गई है, यह दो इनपुट्स, x और y में से बड़ा मान रिटर्न करता है, और यदि वे बराबर हैं तो डिफ़ॉल्ट रूप से x रिटर्न करता है।
नीचे कार्यान्वयन (implementation) दिया गया है, और पिछले अध्याय की तरह, हमने हार्नेसिंग (harnessing) की आवश्यकता से बचने के लिए विज़िबिलिटी को internal से external में बदल दिया है (जो इस अध्याय के दायरे से बाहर है):
/// Solidity
function max(uint256 x, uint256 y) external pure returns (uint256 z) {
assembly {
z := xor(x, mul(xor(x, y), gt(y, x)))
}
}
आइए अब निम्नलिखित प्रॉपर्टी को औपचारिक रूप से (formally) वेरीफाई करें: “यदि x, y से बड़ा है, तो max(x, y) का रिटर्न मान x होना चाहिए।” हम इसे CVL में इस प्रकार व्यक्त कर सकते हैं:
rule max_ifXGreaterThanY_resultX() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert x > y => result == x;
}
इस रूल में, शर्त (x > y) और अपेक्षित परिणाम (result == x) इम्प्लीकेशन P => Q बनाते हैं। जैसी कि उम्मीद थी, प्रॉपर्टी VERIFIED (सत्यापित) है।
Prover run: link
नोट: max फ़ंक्शन का वेरिफिकेशन अभी पूरा नहीं हुआ है। हम इसे अगले सेक्शन में कवर करेंगे।
P => Q Is Not Equivalent To Q => P
अब आइए विपरीत इम्प्लीकेशन (reverse implication) पर विचार करें: “यदि max(x, y) का रिटर्न मान x है, तो x > y” या result == x => x > y। यह पहली बार में वैध (valid) लग सकता है; हालाँकि, जब x == y होता है, तब भी फ़ंक्शन x रिटर्न करता है। यह इस assertion का खंडन करता है कि x > y, जो उस मामले में इम्प्लीकेशन को गलत बना देता है।
यहाँ वह रूल है जो विफल हो जाता है:
rule max_ifResultIsX_thenXGreaterThanY() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert result == x => x > y;
}
Counterexample
जब किसी रूल का उल्लंघन होता है (violated), तो Prover एक काउंटरएग्जांपल (counterexample) दिखाता है। इस मामले में, result == x केवल तभी नहीं होता है जब x > y होता है — यह तब भी होता है जब x == y होता है। काउंटरएग्जांपल विशेष रूप से x = 3 और y = 3 दिखाता है:
इसे ठीक करने के लिए, हमें शर्त को संशोधित करने की आवश्यकता है ताकि उन सभी मामलों को शामिल किया जा सके जहाँ result == x वैध है: जब x > y हो और जब x == y हो।
यहाँ संशोधित रूल है, जहाँ || OR ऑपरेटर है:
rule max_ifResultIsX_thenXGreaterOrEqualToY() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert result == x => x > y || x == y;
}
या, अधिक सरलता से:
rule max_ifResultIsX_thenXGreaterOrEqualToY_simplified() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert result == x => x >= y;
}
और अब यह VERIFIED है:
Prover run: link
अब, वेरिफिकेशन को पूरा करने के लिए, हम इस प्रॉपर्टी को भी वेरीफाई करेंगे कि max(x, y), y रिटर्न करता है जब y, x से बड़ा या उसके बराबर होता है। यहाँ रूल है:
rule max_ifResultIsY_thenYGreaterOrEqualToX() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert result == y => y >= x;
}
जैसी कि उम्मीद थी, यह VERIFIED है:
Prover run: link
P => Q Is Equivalent to !Q => !P
एक इम्प्लीकेशन P => Q को इसके कॉन्ट्रापॉज़िटिव (contrapositive) रूप !Q => !P में फिर से लिखना, स्पेसिफिकेशन के बारे में सोचने का एक वैकल्पिक तरीका सुझाता है।
आइए assertion: x > y => result == x के साथ अपने पिछले रूल पर फिर से विचार करें:
rule max_ifXGreaterThanY_resultX() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert x > y => result == x;
}
अपने मूल रूप में, यह रूल इस बात से संबंधित है कि जब x, y से बड़ा होता है तो क्या होता है, जो यह है कि max(x, y) का रिटर्न मान x है।
कॉन्ट्रापॉज़िटिव रूप assert !(result == x) => !(x > y) में, इसके बजाय हम इस बात से चिंतित हैं कि यदि max(x, y) का रिटर्न मान x नहीं है तो क्या होगा। उस स्थिति में, हम उम्मीद करते हैं कि x, y से बड़ा नहीं है (या सरलता से, x <= y):
rule max_ifResultNotX_thenXNotGreaterThanY() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert result != x => x <= y;
}
Prover run: link
दोनों रूप एक ही तार्किक सत्य (logical truth) को व्यक्त करते हैं, लेकिन अलग-अलग दृष्टिकोण से।
इसे बेहतर ढंग से समझने के लिए, आइए एक सामान्य एनालॉजी (analogy) का उपयोग करें:
- “यदि बारिश हुई, तो ज़मीन गीली है,” या
hasRained => isGroundWet
इसका कॉन्ट्रापॉज़िटिव है:
- “यदि ज़मीन गीली नहीं है, तो निश्चित रूप से बारिश नहीं हुई है,” या
!isGroundWet => !hasRained
हालाँकि, यह तथ्य कि बारिश नहीं हुई है, इस बात की गारंटी नहीं देता कि ज़मीन गीली नहीं है। किसी ने उस पर पानी डाल दिया हो सकता है। इसलिए, !hasRained => !isGroundWet तार्किक रूप से वैध (logically valid) नहीं है।
Vacuous Truth and Tautology In Implication
अब जब हम समझ गए हैं कि इम्प्लीकेशन कैसे काम करता है, तो हमें इन स्टेटमेंट्स को लिखते समय भी सतर्क रहना चाहिए। हम अनजाने में झूठे आश्वासनों (false assurances) के साथ इम्प्लीकेशन लिख सकते हैं, एक विषय जिसे हम आगे एक्सप्लोर करेंगे।
When P is always FALSE, P => Q is TRUE regardless of Q (vacuous)
एक इम्प्लीकेशन वैक्यूअस रूप से (vacuously) सत्य हो जाता है जब शर्त (P) अगम्य (unreachable) होती है (हमेशा असत्य होती है), जिसका अर्थ है कि ऐसी कोई संभावित स्थिति नहीं है जहाँ P लागू होता हो। ऐसे मामलों में, संपूर्ण स्टेटमेंट P => Q को स्वचालित रूप से सत्य माना जाता है, चाहे परिणाम (Q) कुछ भी हो।
ऐसा इसलिए होता है क्योंकि यदि P कभी सत्य नहीं हो सकता है, तो ऐसा कोई उदाहरण नहीं है जिसमें इम्प्लीकेशन का उल्लंघन (violated) किया जा सके। इसलिए, कोई काउंटरएग्जांपल मौजूद नहीं है।
आइए इस उदाहरण का उपयोग करें: “यदि x < 0 है, तो result == y।” चूँकि x एक uint256 है, यह कभी भी नेगेटिव (negative) नहीं हो सकता। यह x < 0 को एक अगम्य स्थिति (unreachable state) बनाता है। इससे कोई फर्क नहीं पड़ता कि हम दाईं ओर (Q) क्या assert करते हैं, इम्प्लीकेशन हमेशा वेरीफाई होगा।
यहाँ CVL वैक्यूअस (vacuous) रूल है:
rule max_unreachableCondition_vacuouslyTrue() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert x < 0 => result == y;
}
यह रूल VERIFIED है, लेकिन इसलिए नहीं कि x < 0 के कारण result == y होता है। यह केवल इसलिए वेरीफाई होता है क्योंकि x < 0 किसी भी वैध एक्सीक्यूशन पाथ (execution path) में अगम्य है, जो इम्प्लीकेशन को वैक्यूअस रूप से सत्य (vacuously true) बनाता है। यह पुष्टि करता है कि कोई काउंटरएग्जांपल मौजूद नहीं है क्योंकि यह शर्त कभी घटित नहीं हो सकती:
Prover run: link
चूँकि शर्त (P) कभी घटित नहीं हो सकती है, परिणाम (Q) कुछ भी हो सकता है — यहाँ तक कि 1 == 2 जैसा कुछ बेतुका (nonsensical) भी, जैसा कि नीचे दिखाया गया है:
rule max_unreachableCondition_vacuouslyTrueObvious() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert x < 0 => 1 == 2;
}
Prover run: link
When Q is always TRUE_,_ P => Q is TRUE regardless of P (tautology)
एक इम्प्लीकेशन टॉटोलॉजिकली (tautologically) सत्य हो जाता है जब परिणाम (Q) हमेशा सत्य होता है, चाहे शर्त (P) कुछ भी हो। ऐसे मामलों में, संपूर्ण स्टेटमेंट P => Q को स्वचालित रूप से सत्य माना जाता है, भले ही शर्त अप्रासंगिक (irrelevant) या भ्रामक हो।
ऐसा इसलिए होता है क्योंकि यदि Q हमेशा सत्य है, तो परिणाम की गारंटी होती है; इसलिए, इम्प्लीकेशन कभी गलत नहीं हो सकता।
आइए इस उदाहरण का उपयोग करें: “यदि x > y है, तो result >= 0।”
पहली नज़र में, ऐसा लगता है कि x > y एक नॉन-नेगेटिव परिणाम की गारंटी देता है। लेकिन result एक uint256 है, जो टाइप के अनुसार हमेशा शून्य से बड़ा या उसके बराबर होता है। इसलिए एक्सप्रेशन result >= 0 हमेशा सत्य होता है।
यहाँ CVL टॉटोलॉजिकल (tautological) रूल है:
rule max_outcomeIsAlwaysTrue_tautology() {
uint256 x;
uint256 y;
mathint result = max(x, y);
assert x > y => result >= 0;
}
यह रूल VERIFIED है, इसलिए नहीं कि x > y के कारण result >= 0 होता है, बल्कि इसलिए कि result >= 0 टाइप के अनुसार हमेशा सत्य होता है, जो इम्प्लीकेशन को टॉटोलॉजिकली सत्य बनाता है:
Prover run: link
Formally Verifying Solmate’s mulDivUp()
अब जब हम मूल बातें जानते हैं, तो हम इम्प्लीकेशन ऑपरेटर का उपयोग करके Solmate के mulDivUp() को औपचारिक रूप से वेरीफाई कर रहे हैं। जैसा कि नाम से पता चलता है, यह फ़ंक्शन दो अनसाइंड इंटीजर्स (unsigned integers) को गुणा करता है, परिणाम को एक अन्य अनसाइंड इंटीजर से विभाजित करता है, और यदि कोई शेषफल (remainder) बचता है तो राउंड अप (round up) करता है। यदि कोई शेषफल नहीं है, तो यह बस भागफल (quotient) रिटर्न करता है।
जिन प्रॉपर्टीज़ को हम औपचारिक रूप से वेरीफाई करेंगे, वे दो श्रेणियों में आती हैं: राउंडिंग बिहेवियर (rounding behavior) और रिवर्ट बिहेवियर (revert behavior)। लेकिन ऐसा करने से पहले, हम मूल mulDivUp() कोड में एक छोटा सा बदलाव करेंगे।
Solmate के mulDivUp() फ़ंक्शन में internal विज़िबिलिटी है, और हम सुविधा के लिए इसे external में बदल देंगे। अन्यथा, एक हार्नेस कॉन्ट्रैक्ट (harness contract) स्थापित करना आवश्यक होगा, जो इस अध्याय के दायरे से बाहर है और इस स्तर पर अनावश्यक मानसिक भार (mental overhead) पैदा कर सकता है।
यहाँ mulDivUp() फ़ंक्शन है:
/// Solidity
uint256 internal constant MAX_UINT256 = 2**256 - 1;
function mulDivUp(
uint256 x,
uint256 y,
uint256 denominator
) external pure returns (uint256 z) {
assembly {
// Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
revert(0, 0)
}
// If x * y modulo the denominator is strictly greater than 0,
// 1 is added to round up the division of x * y by the denominator.
z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))
}
}
असेंबली कोड की व्याख्या इस अध्याय के दायरे से बाहर है। हालाँकि, टिप्पणियाँ (comments) हमें यह समझने में मदद करती हैं कि कोड क्या कर रहा है।
नीचे दी गई ये पंक्तियाँ,
// Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
revert(0, 0)
}
जैसा कि कमेंट सुझाता है, एक require स्टेटमेंट का प्रतिनिधित्व करती हैं जो निम्नलिखित शर्तों को लागू करता है:
denominator != 0, जो शून्य से विभाजन (division by zero) को रोकता है, क्योंकि शून्य से विभाजन की अनुमति नहीं है।y == 0 || x <= type(uint256).max / y, जिसका अर्थ है:- यदि
y == 0है, तो शर्त लागू होती है क्योंकिx * yस्वाभाविक रूप से0के रूप में मूल्यांकन करता है। इस मामले में, ओवरफ्लो (overflow) चेक अनावश्यक है। - अन्यथा, यदि
y != 0है, तोxकोtype(uint256).max / yसे कम या उसके बराबर होना चाहिए, यह सुनिश्चित करते हुए किx * y,type(uint256).maxसे अधिक न हो, जिससे ओवरफ्लो को रोका जा सके।
- यदि
अब हम यह निष्कर्ष निकालते हैं कि औपचारिक रूप से वेरीफाई की जाने वाली प्रॉपर्टीज़ निम्नलिखित हैं:
- यदि
denominator == 0है, तो फ़ंक्शन रिवर्ट (reverts) होता है। - यदि
x * y > MAX_UINT256है, तो फ़ंक्शन रिवर्ट होता है।
अगली पंक्ति में,
// If x * y modulo the denominator is strictly greater than 0,
// 1 is added to round up the division of x * y by the denominator.
z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))
जैसा कि कमेंट सुझाता है, फ़ंक्शन इस प्रकार राउंडिंग (rounding) को संभालता है:
- यदि
x * y % denominator > 0है, तोx * y / denominatorमें1जोड़ा जाता है ताकि इंटीजर विभाजन में Solidity के ट्रंकेशन (truncation) की भरपाई की जा सके। चूँकि Solidity राउंड डाउन (rounds down) करता है, इसलिए1जोड़ना प्रभावी रूप से मान को राउंड अप (rounds up) करता है। - यदि
x * y % denominator == 0है, तो किसी राउंडिंग एडजस्टमेंट की आवश्यकता नहीं है, और परिणाम वैसे ही रिटर्न किया जाता है।
अब हम यह निष्कर्ष निकालते हैं कि औपचारिक रूप से वेरीफाई की जाने वाली प्रॉपर्टीज़ निम्नलिखित हैं:
- यदि
x * y % denominator > 0है, तो परिणामx * y / denominator + 1है। - यदि
x * y % denominator == 0है, तो परिणामx * y / denominatorहै।
चूँकि अब हम समझते हैं कि फ़ंक्शन कैसे काम करता और किन प्रॉपर्टीज़ को औपचारिक रूप से वेरीफाई करना है, हम नियम लिखने के साथ आगे बढ़ सकते हैं। आइए राउंडिंग बिहेवियर के नियमों से शुरू करें।
Rounding Behavior
राउंडिंग बिहेवियर प्रॉपर्टी के लिए CVL रूल स्पेसिफिकेशन नीचे दिया गया है।
रूल mulDivUp_roundUp() का assertion बताता है कि जब x और y के गुणनफल (product) को denominator से विभाजित किया जाता है और एक शेषफल (remainder) बचता है, तो परिणाम में 1 की वृद्धि (incremented) की जाती है।
इसी तरह, रूल mulDivUp_noRoundUp() में assertion बताता है कि जब x और y के गुणनफल को denominator से विभाजित किया जाता है और कोई शेषफल नहीं बचता है, तो परिणाम वैसे ही रिटर्न किया जाता है।
जैसी कि उम्मीद थी, ये नियम VERIFIED हैं:
rule mulDivUp_roundUp() {
uint256 x;
uint256 y;
uint256 denominator;
mathint result = mulDivUp(x, y, denominator);
assert ((x * y) % denominator > 0) => (result == (x * y / denominator) + 1);
}
rule mulDivUp_noRoundUp() {
uint256 x;
uint256 y;
uint256 denominator;
mathint result = mulDivUp(x, y, denominator);
assert ((x * y) % denominator == 0) => (result == x * y / denominator);
}
Prover run: link
अब, आइए इस फ़ंक्शन के लिए प्रॉपर्टीज़ की अगली श्रेणी पर चलते हैं: रिवर्ट बिहेवियर (revert behavior)।
Revert Behavior
जैसा कि पहले चर्चा की गई है, दो मामले हैं जहाँ mulDivUp() रिवर्ट होता है:
- यदि
denominator == 0 - यदि
x * y > MAX_UINT256
रिवर्ट्स को औपचारिक रूप से वेरीफाई करते समय, हमें फ़ंक्शंस को कॉल करते समय @withrevert टैग शामिल करना चाहिए। डिफ़ॉल्ट रूप से, Prover केवल नॉन-रिवर्टिंग पाथ (non-reverting paths) को एक्सीक्यूट करता है, जिसका अर्थ है कि mulDivUp(x, y, denominator) को पास किए गए सभी आर्गुमेंट्स (arguments) नॉन-रिवर्टिंग हैं। हालाँकि, फ़ंक्शन में @withrevert जोड़ने से Prover को उन आर्गुमेंट्स पर भी विचार करने का निर्देश मिलता है जो रिवर्ट का कारण बनते हैं। यह हमें अपने इम्प्लीकेशन स्टेटमेंट्स में रिवर्टिंग मामलों को ध्यान में रखने की अनुमति देता है।
नीचे CVL रूल स्पेसिफिकेशन है:
rule mulDivUp_ifDenominatorIsZero_revert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
bool isReverted = lastReverted;
assert (denominator == 0) => isReverted;
}
rule mulDivUp_ifXYExceedsMaxUint_revert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
bool isReverted = lastReverted;
assert (x * y > max_uint256) => isReverted;
}
जैसी कि उम्मीद थी, ये नियम VERIFIED हैं:
Prover run: link
इसके लिए एक और भी दिलचस्प दृष्टिकोण (approach) है। अब तक, हमने P => Q कंस्ट्रक्ट का उपयोग किया है, जिसका अर्थ है (P) शर्त का परिणाम (Q) होता है। लेकिन अगर हम इसे Q => P में उलट देते हैं, तो इसका अर्थ है कि (Q) परिणाम (P) शर्तों से उत्पन्न होता है; इसलिए, हमें उन सभी संभावित मामलों का हिसाब रखना चाहिए जहाँ P, Q की ओर ले जाता है।
नीचे कार्यान्वयन दिया गया है जहाँ, पहले रूल में, हम जानबूझकर एक रिवर्ट मामले को छोड़ देते हैं, जबकि दूसरे रूल में, हम सभी मामलों का हिसाब रखते हैं। परिणामस्वरूप, पहले रूल के कारण VIOLATION (उल्लंघन) होता है, जबकि दूसरा रूल VERIFIED होता है:
rule mulDivUp_allRevertCases_violated() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
bool isReverted = lastReverted;
assert isReverted => (denominator == 0);
}
rule mulDivUp_allRevertCases() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
bool isReverted = lastReverted;
assert isReverted => (denominator == 0 || x * y > max_uint256);
}
Prover run: link
अगले उप-खंड (sub-section) में, हम औपचारिक रूप से नॉन-रिवर्ट्स (non-reverts) को वेरीफाई करेंगे, जो एक वैकल्पिक कदम है क्योंकि हमने सभी रिवर्ट मामलों को कवर कर लिया है। हालाँकि, हम अभी भी ऐसा करेंगे क्योंकि भविष्य में इसके उपयोग के मामले हो सकते हैं।
Non-Revert Behavior (Optional)
यदि हम रिवर्टिंग पाथ को औपचारिक रूप से वेरीफाई कर सकते हैं, तो हम नॉन-रिवर्टिंग पाथ को भी वेरीफाई कर सकते हैं। ऐसा करने के लिए, हमें स्टेटमेंट्स को इस प्रकार फिर से फ्रेम (reframe) करने की आवश्यकता है:
denominator != 0x * y <= MAX_UINT256
और उन्हें नीचे CVL रूल कार्यान्वयन में दिखाए अनुसार जोड़ें (combine):
rule mulDivUp_noRevert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
bool isReverted = lastReverted;
assert ((denominator != 0) && (x * y <= max_uint256)) => !isReverted;
}
जैसी कि उम्मीद थी, रूल VERIFIED है:
Prover run: link
Summary
- एक इम्प्लीकेशन स्टेटमेंट में एक शर्त
P, एक परिणामQऔर इम्प्लीकेशन ऑपरेटर (=>) होता है। - इम्प्लीकेशन ऑपरेटर एक तरफ़ा (one-way) सशर्त संबंध को परिभाषित करता है, जिसका अर्थ है कि
P => Qका मतलबQ => Pनहीं है। P => Qऔर इसका कॉन्ट्रापॉज़िटिव!Q => !Pतार्किक रूप से समतुल्य (logically equivalent) हैं, लेकिन अलग-अलग दृष्टिकोण प्रदान करते हैं, जिससे ध्यान इस बात से हट जाता है कि शर्त कब लागू होती है और कब नहीं।- एक इम्प्लीकेशन के सार्थक होने के लिए (न तो वैक्यूअस और न ही टॉटोलॉजिकल),
Q(परिणाम) का निर्भर होना आवश्यक हैP(शर्त) के सत्य होने पर। - एक वैक्यूअस सत्य तब होता है जब
Pअगम्य (हमेशा असत्य) होता है, जो काउंटरएग्जांपल की कमी के कारणQकी परवाह किए बिनाP => Qको सत्य बनाता है। - एक टॉटोलॉजी तब होती है जब
Qहमेशा सत्य होता है, जोPकी परवाह किए बिनाP => Qको सत्य बनाता है। - वैक्यूअस सत्य और टॉटोलॉजी औपचारिक वेरिफिकेशन (formal verification) में भ्रामक आश्वासन (misleading assurance) पैदा करते हैं।
पाठकों के लिए अभ्यास (Exercises)
- औपचारिक रूप से वेरीफाई करें कि Solady min हमेशा min रिटर्न करता है।
- औपचारिक रूप से वेरीफाई करें कि Solady zeroFloorSub
max(0, x - y)रिटर्न करता है। दूसरे शब्दों में, यदिx,yसे कम है, तो यह0रिटर्न करता है। अन्यथा, यहx - yरिटर्न करता है।
यह लेख formal verification using the Certora Prover पर एक श्रृंखला का हिस्सा है