Introduction

Biconditional ऑपरेटर हमें बूलियन (boolean) वैल्यूज़ के बीच if-and-only-if (केवल और केवल यदि) संबंधों को assert (दावा) करने में सक्षम बनाता है। Implication (P => Q) यह बताता है कि यदि स्थिति P संतुष्ट होती है, तो Q देखा जाता है। Biconditional इसमें विपरीत आवश्यकता को जोड़ता है: यदि Q देखा जाता है, तो स्थिति P को भी संतुष्ट होना चाहिए। दूसरे शब्दों में, P <=> Q, P => Q और Q => P दोनों को एक साथ assert करने के बराबर है।

नोट: यह माना जाता है कि पाठक ने पहले ही “Implication Operator” अध्याय पढ़ लिया है, क्योंकि यह इस अध्याय की नींव रखता है।

setX() Function

आइए एक बेसिक सेटर (setter) फ़ंक्शन से शुरू करें। यह एक uint256 इनपुट लेता है और स्टोरेज वेरिएबल x को अपडेट करता है, लेकिन केवल तभी जब नई वैल्यू वर्तमान वैल्यू से सख्ती से अधिक हो। यह प्रतिबंध एक require स्टेटमेंट का उपयोग करके लागू किया जाता है, जो स्थिति पूरी न होने पर ट्रांज़ेक्शन को रिवर्ट (revert) कर देता है:

Copy
/// Solidity

uint256 public x;

function setX(uint256 _x) external {
    require(_x > x, "x must be greater than the previous value");
    x = _x;
}

Implication ऑपरेटर का उपयोग करके इस फ़ंक्शन को formally verify (औपचारिक रूप से सत्यापित) करने के लिए, हम ट्रांज़ेक्शन की सफलता और उसके परिणामस्वरूप होने वाले स्टेट (state) परिवर्तन के बीच के संबंध को दो assert implication स्टेटमेंट्स के रूप में व्यक्त कर सकते हैं:

Copy
rule setX_usingImplication() {
    uint256 _x;
    
    mathint xBefore = x();
    
    setX@withrevert(_x);
    bool success = !lastReverted;
    
    mathint xAfter = x();

    assert success => xAfter > xBefore; // If the call succeeds, then x increased (P => Q)
    assert xAfter > xBefore => success; // If x increased, then the call must have succeeded (Q => P)
}

Prover रन: link

हालांकि यह तार्किक रूप से सही है, लेकिन दो एक-तरफा implications (P => Q और Q => P) लिखना अनावश्यक रूप से लंबा (verbose) है।

Biconditional (<=>) in CVL

यहाँ उद्देश्य एक सटीक नियम व्यक्त करना है: “ट्रांज़ेक्शन केवल और केवल तभी सफल होता है जब इनपुट वैल्यू x की वर्तमान वैल्यू से अधिक हो।”

इसे अधिक स्पष्ट रूप से इस प्रकार लिखा जा सकता है:

Copy
rule setX_TxSucceeds_iff_XIncreases() {
    uint256 _x;
    
    mathint xBefore = x();
    
    setX@withrevert(_x);
    bool success = !lastReverted;
    
    mathint xAfter = x();
    assert success <=> xAfter > xBefore;
}

यह अकेला assert biconditional स्टेटमेंट अधिक संक्षिप्त है और कॉल की सफलता और स्टेट x (वृद्धि) में परिवर्तन के बीच दो-तरफा संबंध को सीधे व्यक्त करता है। दूसरे शब्दों में, फ़ंक्शन केवल तभी सफल होता है जब x बढ़ता है, और x केवल तभी बढ़ता है जब कॉल सफल होता है।

जैसी उम्मीद थी, यह नियम सत्यापित (verify) हो जाता है:

Prover रन: link

अंतर्निहित (Implicitly) रूप से, हम यह भी तर्क दे सकते हैं कि: यदि कॉल विफल हो जाता है, तो x नहीं बढ़ा:

Copy
assert !success <=> !(xAfter > xBefore);

या

Copy
assert !success <=> xAfter <= xBefore;

यह पहले से ही biconditional द्वारा निहित (implied) है और इसे अलग से लिखने की आवश्यकता नहीं है।

Formally Verifying Solmate’s mulDivUp()

पिछले अध्याय (Implication Operator) में, हमने Solmate के mulDivUp() फ़ंक्शन के व्यवहार, इसके ओवरफ़्लो (overflow) चेक और राउंडिंग (rounding) लॉजिक पर चर्चा की थी। यहाँ एक संक्षिप्त पुनरावृत्ति (recap) दी गई है:

• यह रिवर्ट हो जाता है यदि denominator == 0 (शून्य से विभाजन) या यदि x * y > MAX_UINT256 (ओवरफ़्लो)।
• mulDivUp(x, y, denominator) x और y को गुणा करता है, परिणाम को denominator से विभाजित करता है, और यदि कोई शेष (remainder) बचता है तो राउंड अप (round up) करता है; अन्यथा, यह सटीक भागफल (quotient) लौटाता है।

अब आइए biconditional ऑपरेटर का उपयोग करके इन व्यवहारों को formally verify करें।

Revert Behavior

आइए रिवर्ट (revert) व्यवहार से शुरू करते हैं। हम सबसे सरल रिवर्ट स्थिति, denominator == 0 लिखने से शुरू करते हैं, और फिर एक पूर्ण नियम की ओर बढ़ते हैं।

जैसा कि हम जानते हैं, यह विफल हो जाएगा, क्योंकि यह सभी रिवर्ट परिदृश्यों (scenarios) को कैप्चर नहीं करता है, लेकिन यह एक अच्छी शुरुआत के रूप में कार्य करता है:

Copy
rule mulDivUp_denominatorIsZero_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator; 

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 <=> lastReverted;
}

नियम एक counterexample (प्रति-उदाहरण) के कारण विफल हो जाता है जहाँ x और y का गुणनफल max_uint256 से अधिक हो जाता है। हमें इसे एक अतिरिक्त रिवर्ट स्थिति के रूप में शामिल करने की आवश्यकता है:

यहाँ सही किया गया CVL नियम है:

Copy
rule mulDivUp_allConditions_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator; 

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 || x * y > max_uint256 <=> lastReverted;
}

Prover रन: link

ध्यान दें कि biconditional प्रतिवर्ती (reversible) है (implication के विपरीत), इसलिए हम assertion को इस तरह फिर से लिख सकते हैं:

Copy
rule mulDivUp_allConditions_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator; 

    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted <=> denominator == 0 || x * y > max_uint256;
}

Prover रन: link

इसके अलावा, चूंकि एक biconditional एक संयुक्त दो-तरफा implication (P => Q और Q => P) है, इसलिए ये दोनों तार्किक रूप से एक साथ बंधे हैं; अतः <=> के माध्यम से तर्क किए गए एक्सप्रेशन्स (expressions) अविभाज्य (inseparable) हैं।

Rounding Behavior

नीचे दिया गया नियम mulDivUp() फ़ंक्शन के राउंडिंग (rounding) व्यवहार को निर्दिष्ट करता है। यह assert करता है कि फ़ंक्शन केवल और केवल तभी राउंड-अप वैल्यू लौटाता है जब कोई शेष (remainder) मौजूद हो। Biconditional ऑपरेटर यह गारंटी देता है कि शेषफल एकमात्र ऐसी स्थिति है जो राउंडिंग अप को ट्रिगर करती है और कोई अन्य स्थिति रिटर्न वैल्यू को प्रभावित नहीं कर सकती है:

Copy
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);
}

Prover रन: link

नीचे दिया गया नियम “अन्य” (“other”) मामले को कवर करता है। यह assert करता है कि फ़ंक्शन सटीक भागफल (quotient) केवल और केवल तभी लौटाता है जब कोई शेष (remainder) न हो। Biconditional ऑपरेटर यह गारंटी देता है कि बिना राउंड किए गए परिणाम को लौटाने का एकमात्र कारण शेषफल की अनुपस्थिति है:

Copy
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 रन: link

When To Use Biconditional Over Implication

Exclude Uncertainty

उपरोक्त नियम, जैसा कि हमने पिछले अध्याय में देखा, => का उपयोग करके लिखा जा सकता है क्योंकि सत्यापित की जा रही प्रॉपर्टी में केवल एक ही स्थिति होती है जो परिणाम की ओर ले जाती है। ऐसे मामलों में, => को <=> से बदला जा सकता है। यह प्रतिस्थापन (replacement) बेहतर है क्योंकि <=> यह बताता है कि निर्दिष्ट स्थिति के अलावा कोई और चीज़ परिणाम का कारण नहीं बन सकती। Implication ऑपरेटर यह गारंटी प्रदान नहीं करता है, इसलिए ऐसे मामलों में, इस गारंटी को स्पष्ट करने के लिए biconditional का उपयोग करना बेहतर है।

पिछले उदाहरण (max फ़ंक्शन) में, हमने सभी रिवर्ट स्थितियों को ध्यान में रखा था क्योंकि हम समग्र रूप से फ़ंक्शन की शुद्धता (correctness) को सत्यापित कर रहे थे। हालाँकि, जब किसी ऐसे फ़ंक्शन से निपटना हो जो कई इंटरनल फ़ंक्शन्स को कॉल करता है, जिनमें से प्रत्येक संभावित रूप से विभिन्न रिवर्ट स्थितियों का कारण बन सकता है, तो implication का उपयोग करना अधिक व्यावहारिक हो सकता है। यह दृष्टिकोण हर संभावित विफलता परिदृश्य से व्यापक रूप से निपटने के बजाय, रिवर्ट करने के लिए केवल आवश्यक स्थिति (स्थितियों) पर केंद्रित होता है।

Verify Mutual Dependency

पारस्परिक निर्भरता तब होती है जब दो वेरिएबल एक-दूसरे पर निर्भर होते हैं, जिसका अर्थ है कि एक में परिवर्तन दूसरे में संबंधित परिवर्तन को ट्रिगर करता है, और इसके विपरीत।

उदाहरण के रूप में एक AMM WETH/USDC पूल लें: स्वैप (swaps) के दौरान, WETH बैलेंस केवल और केवल तभी बढ़ता है जब USDC बैलेंस घटता है, और इसके विपरीत। यह एक दो-तरफा निर्भरता बनाता है जहाँ एक टोकन का बैलेंस दूसरे में बदलाव के जवाब में समायोजित होना चाहिए, जो यह दर्शाता है कि कोई भी बैलेंस स्वतंत्र रूप से नहीं बदल सकता है।

Summary

• Biconditional (<=>) स्पष्ट रूप से दोनों दिशाओं में implication की गारंटी देता है। यदि स्थिति P संतुष्ट है, तो Q लागू होता है, और यदि Q लागू होता है, तो स्थिति P को भी संतुष्ट होना चाहिए।
• Implication ऑपरेटर (=>) तब काम करता है जब स्थिति(याँ) किसी परिणाम की ओर ले जाती हैं, लेकिन यह गारंटी नहीं देता है कि परिणाम केवल उसी स्थिति के कारण हो सकता है।
• Biconditional का उपयोग करना तब अव्यावहारिक हो सकता है जब परिणाम की ओर ले जाने वाली कई संभावित स्थितियाँ हों।

Exercises for the reader

1. Formally verify करें कि Solady min हमेशा न्यूनतम (min) लौटाता है।
2. Formally verify करें कि Solady zeroFloorSub max(0, x - y) लौटाता है। दूसरे शब्दों में, यदि x, y से कम है, तो यह 0 लौटाता है। अन्यथा, यह x - y लौटाता है।

यह लेख Certora Prover का उपयोग करके formal verification पर एक श्रृंखला का हिस्सा है।