परिचय
अनुबंध (contract) के कुछ व्यवहार (गुण) स्वाभाविक रूप से सशर्त (conditional) होते हैं, और CVL में if/else जैसी संरचनाओं का उपयोग करना सशर्त व्यवहार को औपचारिक रूप से पकड़ने (capture) का एक तरीका है।
CVL में if/else स्टेटमेंट्स उसी तरह काम करते हैं जैसे वे अन्य भाषाओं में करते हैं। हम यहाँ कंडीशनल फीचर्स वाले कोड को औपचारिक रूप से सत्यापित करने के उदाहरण प्रदान करेंगे।
एशर्शन (Assertions) और मेथड इनवोकेशन (Method Invocations)
आइए एक सरल फंक्शन को औपचारिक रूप से सत्यापित करके शुरुआत करें जो दो अनसाइन्ड इंटिजर (uint256) लेता है और उनका योग (uint256) लौटाता है। अपेक्षित परिणाम सशर्त है: यदि जोड़ ओवरफ्लो (overflow) होता है, तो फंक्शन रिवर्ट (revert) हो जाता है; अन्यथा, यह योग लौटाता है।
नीचे add() फंक्शन का Solidity इम्प्लीमेंटेशन दिया गया है:
/// Solidity
function add(uint256 x, uint256 y) external pure returns (uint256) {
return x + y;
}
और यहाँ CVL स्पेसिफिकेशन है (sum प्रोवर (Prover) के संस्करण 7.25.2 के बाद से एक रिज़र्व्ड कीवर्ड है, इसलिए हम इसके बजाय _sum का उपयोग करते हैं।):
/// CVL
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule add_sumWithOverflowRevert() {
uint256 x;
uint256 y;
mathint _sum = x + y;
if (_sum <= max_uint256) { // non-revert case
mathint result = add@withrevert(x, y);
assert !lastReverted;
assert result == _sum;
}
else { // revert case
add@withrevert(x, y);
assert lastReverted;
}
}
आइए समझते हैं कि ऊपर दिए गए स्पेसिफिकेशन कोड में क्या हो रहा है। निम्नलिखित पंक्तियों में,
uint256 x;
uint256 y;
mathint _sum = x + y;
वेरिएबल _sum को एक mathint के रूप में घोषित किया गया है, जो बिना ओवरफ्लो लिमिट वाला एक प्रकार है, जिससे यह x + y को सटीक रूप से दर्शा सकता है, भले ही यह max_uint256 से अधिक हो। यह हमें max_uint256 से _sum की तुलना करके ओवरफ्लो का पता लगाने और यह निर्धारित करने में सक्षम बनाता है कि क्या फंक्शन को रिवर्ट होना चाहिए।
अब निम्नलिखित पंक्तियों में,
if (_sum <= max_uint256) {
mathint result = add@withrevert(x, y);
assert !lastReverted;
assert result == _sum;
}
Solidity का जोड़ (addition) ऑपरेशन तब किया जाता है जब _sum = x + y, max_uint256 की सीमा के भीतर रहता है।
@withrevert टैग को एक फंक्शन में जोड़ा जाता है ताकि प्रोवर (Prover) को उन रिवर्टिंग पाथ (reverting paths) या तर्कों (arguments) को शामिल करने का निर्देश दिया जा सके जो रिवर्ट का कारण बनते हैं। assert !lastReverted का अर्थ है कि यदि योग ओवरफ्लो नहीं हुआ है तो हमें कभी भी रिवर्ट नहीं मिलना चाहिए।
अंत में, नीचे दिखाया गया else ब्लॉक ओवरफ्लो मामलों को संभालता है, जिसमें यह उम्मीद की जाती है कि जहाँ _sum, max_uint256 से अधिक हो वहाँ एक रिवर्ट हो।
else {
add@withrevert(x, y);
assert lastReverted;
}
उम्मीद के मुताबिक, CVL नियम VERIFIED (सत्यापित) है:
प्रोवर रन: link
यह उदाहरण दिखाता है कि कंडीशनल ब्लॉक्स या ब्रांच के भीतर Solidity फंक्शन्स को कॉल (invoke) किया जा सकता है और एशर्शन किए जा सकते हैं।
एक if स्टेटमेंट में वेरिएबल असाइनमेंट (Variable Assignments)
इसके बाद, हम Solady लाइब्रेरी के gas-optimized max function को औपचारिक रूप से सत्यापित करेंगे।
नीचे Solady max फंक्शन का इम्प्लीमेंटेशन दिया गया है। भले ही यह तुरंत स्पष्ट न हो, यह x और y में से बड़ी वैल्यू लौटाता है। यदि x, y के बराबर है, तो फंक्शन बस x लौटाता है।
/// Solidity
function max(uint256 x, uint256 y) external pure returns (uint256 z) {
assembly {
z := xor(x, mul(xor(x, y), gt(y, x)))
}
}
ध्यान दें कि हमने विजिबिलिटी को internal से external में बदल दिया है ताकि हार्नेस फाइल (harness file) की आवश्यकता को समाप्त किया जा सके, जो इस अध्याय के दायरे से बाहर है।
इस असेंबली इम्प्लीमेंटेशन की आंतरिक कार्यप्रणाली को समझाना भी इस अध्याय के दायरे से बाहर है। हालाँकि, यदि आप जानने के लिए उत्सुक हैं, तो यहाँ एक वीडियो है जो पाँच मिनट से भी कम समय में इन विवरणों को कवर करता है: https://www.youtube.com/watch?v=4nDUQIk4oqQ।
अब, आइए Solady max फंक्शन के औपचारिक सत्यापन (formal verification) के साथ आगे बढ़ें। इसके दो रूप (variations) हैं: एक अनसाइन्ड इंटिजर्स के लिए और दूसरा साइन्ड (signed) इंटिजर्स के लिए। चूँकि दोनों एक ही मूल अवधारणा का पालन करते हैं, हम अनसाइन्ड इंटिजर वाले रूप पर ध्यान केंद्रित करेंगे।
Solady max फंक्शन को सत्यापित करने के लिए यहाँ एक शुरुआती CVL नियम दिया गया है, लेकिन हम इसे कुछ ही देर में सरल कर देंगे:
/// CVL
rule max_returnMax() {
uint256 x;
uint256 y;
if (x >= y) {
mathint max = max@withrevert(x, y);
assert !lastReverted;
assert max == x;
}
else {
mathint max = max@withrevert(x, y);
assert !lastReverted;
assert max == y;
}
}
ऊपर दिए गए नियम में, if ब्लॉक यह सत्यापित करता है कि जब x > y होता है, तो अधिकतम वैल्यू x होती है, या यदि x = y है, तो यह केवल x लौटाता है क्योंकि दोनों मान समान हैं। else ब्लॉक बचे हुए मामले को कवर करता है, जहाँ x < y है, जिससे y अधिकतम वैल्यू बन जाता है। किसी भी स्थिति में, हम रिवर्ट की अनुमति नहीं देते हैं क्योंकि फंक्शन को कभी भी रिवर्ट नहीं होना चाहिए।
उम्मीद के मुताबिक यह नियम VERIFIED है:
प्रोवर रन: link
फंक्शन इनवोकेशन और एशर्शन को if/else ब्लॉक के अंदर होना आवश्यक नहीं है। हम फंक्शन कॉल्स को if ब्लॉक के बाहर ले जा सकते हैं और if ब्लॉक के अंदर अपेक्षित परिणामों की गणना कर सकते हैं:
/// CVL
rule max_returnMax_modified() {
uint256 x;
uint256 y;
mathint expectedMax;
if (x >= y) {
expectedMax = x;
} else {
expectedMax = y;
}
mathint resultMax = max@withrevert(x, y);
assert !lastReverted;
assert resultMax == expectedMax;
}
प्रोवर रन: link
किसी if स्टेटमेंट के बाहर फंक्शन इनवोकेशन को ले जाने से CVL कोड अधिक कुशल (efficient) हो जाता है, क्योंकि प्रत्येक कंडीशनल ब्रांच के भीतर कॉल होने के बजाय फंक्शन केवल एक बार कॉल किया जाता है। इसका प्रभाव अभी ध्यान देने योग्य नहीं हो सकता है, लेकिन अधिक जटिल नियमों के लिए, यह दृष्टिकोण फायदेमंद हो सकता है, जैसा कि हम अगले भाग में दिखाएंगे।
वेरिफायर की जटिलता को कम करना, mulDivUp के साथ एक उदाहरण
mulDivUp() एक फंक्शन है जो दो अनसाइन्ड इंटिजर्स को गुणा करता है, गुणनफल (product) को एक अन्य अनसाइन्ड इंटिजर से विभाजित करता है, और यदि कोई शेषफल (remainder) बचता है तो राउंड अप (round up) करता है। यदि कोई शेषफल नहीं है, तो यह भागफल (quotient) को उसी रूप में लौटाता है। उदाहरण के लिए, 5 / 2 का परिणाम 2 है, लेकिन mulDivUp(5, 2) का परिणाम राउंड अप के कारण 3 होता है। इसके विपरीत, 4 / 2 का परिणाम 2 है, और mulDivUp(4, 2) का परिणाम भी 2 होता है, क्योंकि कोई शेषफल नहीं है।
साथ ही, यह दो मामलों में रिवर्ट होता है: जब भाजक (divisor) शून्य होता है या जब अंश (numerator) (x और y का गुणनफल) max_uint256 से अधिक हो जाता है।
हम जो इम्प्लीमेंटेशन उपयोग करेंगे वह Solmate के mulDivUp() से है, जो असेंबली में लिखा गया एक गैस-कुशल (gas-efficient) फंक्शन है। हमने हार्नेस फाइल का उपयोग करने से बचने के लिए इसकी विजिबिलिटी को internal से external में बदलकर कोड को थोड़ा संशोधित किया है।
यहाँ Solmate का 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)
}
यह रिवर्ट व्यवहार को परिभाषित करता है। यह सुनिश्चित करता है कि शून्य से विभाजन को रोकने के लिए भाजक (denominator) शून्य नहीं होना चाहिए। इसके अतिरिक्त, यह गारंटी देता है कि 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))
यदि x * y को denominator से विभाजित करने पर शेषफल शून्य से अधिक है, तो राउंड अप करने के लिए परिणाम में 1 जोड़ा जाता है; अन्यथा, परिणाम अपरिवर्तित रहता है।
अब जब हम जानते हैं कि फंक्शन क्या करने की कोशिश कर रहा है, तो अब हम इसके औपचारिक सत्यापन (formal verification) के साथ आगे बढ़ सकते हैं।
mulDivUp के लिए स्पेसिफिकेशन्स विकसित करना
यहाँ एक प्रारंभिक स्पेसिफिकेशन है जो Solmate mulDivUp() फंक्शन के व्यवहार को दर्शाता है, और स्पष्टीकरण उसके बाद दिया गया है:
/// CVL
rule mulDivUp_roundOrRevert() {
uint256 x;
uint256 y;
uint256 denominator;
if (denominator == 0) { // catches revert condition: if denominator is zero
mulDivUp@withrevert(x, y, denominator);
assert lastReverted;
}
else if (x * y > max_uint256) { // catches revert condition: multiplication overflows a max_uint256 value
mulDivUp@withrevert(x, y, denominator);
assert lastReverted;
}
else { // catches all non-revert conditions
if (x * y % denominator == 0) { // if there's no remainder after x * y and denominator division
mathint result = mulDivUp@withrevert(x, y, denominator);
assert !lastReverted;
assert result == x * y / denominator;
}
else { // if there's a remainder after x * y and denominator division
mathint result = mulDivUp@withrevert(x, y, denominator);
assert !lastReverted;
assert result == (x * y / denominator) + 1;
}
}
}
जब हम Certora Prover चलाते हैं, तो Solmate mulDivUp() का सही होना सत्यापित हो जाता है:
प्रोवर रन: link
ऊपर दिए गए कोड पर ध्यान दें कि हम else if के साथ कई कंडीशनल ब्रांच का उपयोग कर सकते हैं, और हमें नेस्टेड (nested) if/else स्टेटमेंट्स का उपयोग करने से कोई नहीं रोकता है। हालाँकि, नेस्टिंग if स्टेटमेंट्स से बचने के लिए, जो नियम को पढ़ना कठिन बनाता है, हम शर्तों (conditions) को फिर से व्यवस्थित कर सकते हैं।
नीचे दी गई पंक्तियाँ रिवर्ट की शर्तों को संभालती हैं:
if (denominator == 0) {
mulDivUp@withrevert(x, y, denominator);
assert lastReverted;
}
else if (x * y > max_uint256) {
mulDivUp@withrevert(x, y, denominator);
assert lastReverted;
}
यदि इनमें से कोई भी शर्त पूरी होती है, तो ब्रांच lastReverted एशर्ट करती है, जिसका अर्थ है कि फंक्शन रिवर्ट हो जाता है। हालाँकि हम इन दोनों रिवर्ट शर्तों को एक में मिला सकते हैं, लेकिन बाद में कोड ऑप्टिमाइज़ेशन पर चर्चा करते समय हम इस पर ध्यान देंगे।
यदि ये दो रिवर्ट शर्तें पूरी नहीं होती हैं, तो निष्पादन (execution) else स्टेटमेंट पर चला जाता है, जहाँ राउंडिंग व्यवहार को सत्यापित किया जाता है। else ब्लॉक के भीतर, if/else स्टेटमेंट्स का एक और सेट है जो राउंडिंग व्यवहार के लिए स्पेसिफिकेशन को परिभाषित करता है।
जैसा कि आप नीचे देखेंगे, else ब्लॉक में, if शर्त यह जाँचती है कि x और y के गुणनफल को भाजक (denominator) से मॉड्यूलो (modulo) करने पर शेषफल शून्य आता है या नहीं। इस स्थिति में, किसी राउंड अप की आवश्यकता नहीं होती है, इसलिए रिटर्न वैल्यू x * y / denominator होती है। हालाँकि, else ब्रांच में, जहाँ मॉड्यूलो ऑपरेशन का परिणाम शून्य से अधिक शेषफल देता है, x * y / denominator में 1 जोड़कर राउंड अप किया जाता है।
else {
if (x * y % denominator == 0) {
mathint result = mulDivUp@withrevert(x, y, denominator);
assert !lastReverted;
assert result == x * y / denominator;
}
else {
mathint result = mulDivUp@withrevert(x, y, denominator);
assert !lastReverted;
assert result == (x * y / denominator) + 1;
}
}
हमने सीखा कि if/else कई नियम बनाने के बजाय एक ही नियम के भीतर सत्यापन (verifications) को समेकित (consolidate) कर सकता है। हालाँकि, इसकी कुछ कमियाँ भी हैं। जैसे-जैसे सत्यापित किया जाने वाला फंक्शन अधिक जटिल होता जाता है, स्पेसिफिकेशन भी असंगत रूप से जटिल होता जाता है, जिस पर हम आगे चर्चा करेंगे।
पाथ एक्सप्लोजन (Path Explosion)
if/else का उपयोग करने से कंडीशनल ब्रांच बनती हैं, फंक्शन कॉल होते हैं, और कंडीशनल ब्लॉक्स के भीतर ही एशर्शन होते हैं। जब ऐसा होता है, तो प्रोवर (Prover) हर ब्रांच में सभी मामलों का परीक्षण करता है, जिससे उन परिदृश्यों की संख्या बढ़ जाती है जिनका मूल्यांकन किया जाना चाहिए और स्वाभाविक रूप से नियम का निष्पादन (rule execution) धीमा हो जाता है।
mulDivUp के लिए ऑप्टिमाइज़्ड (Optimized) CVL नियम
नीचे ऑप्टिमाइज़्ड नियम दिया गया है, और इसके बाद हम बताएंगे कि हमने क्या बदलाव किए हैं।
/// CVL
rule mulDivUp_roundOrRevert_optimized() {
uint256 x;
uint256 y;
uint256 denominator;
mathint result = mulDivUp@withrevert(x, y, denominator);
if (denominator == 0 || x * y > max_uint256) {
assert lastReverted;
}
else {
if (x * y % denominator == 0) {
assert !lastReverted;
assert result == x * y / denominator;
}
else {
assert !lastReverted;
assert result == (x * y / denominator) + 1;
}
}
}
पहला बदलाव जो हमने किया वह था रिवर्ट शर्तों को एक ही if स्टेटमेंट में मिलाना: if (denominator == 0 || x * y > max_uint256) { … }।
इसके बाद हमने ब्रांच से सभी mulDivUp@withrevert(x, y, denominator) फंक्शन इनवोकेशन्स को हटा दिया और उन्हें एक ही कॉल में अलग कर दिया। यह कंडीशनल ब्लॉक्स के भीतर अनावश्यक (redundant) फंक्शन कॉल्स से बचकर दक्षता (efficiency) में सुधार करता है।
प्रोवर रनटाइम बेंचमार्क (Prover Runtime Benchmarks)
नीचे अक्षम (inefficient) कोड और ऑप्टिमाइज़्ड (optimized) कोड के बीच निष्पादन समय (execution time) की तुलना दी गई है:
प्रोवर रन: link
ऊपर दी गई प्रोवर रिपोर्ट को देखते हुए, if/else का अक्षम उपयोग नियम के निष्पादन को काफी धीमा कर सकता है। अक्षम और ऑप्टिमाइज़्ड संस्करणों की तुलना करने पर, अक्षम कोड को निष्पादित होने में ऑप्टिमाइज़्ड कोड की तुलना में चार गुना अधिक समय लगता है। यह समस्या तब और भी बदतर हो जाती है जब हम जटिल स्मार्ट कॉन्ट्रैक्ट्स के साथ वास्तविक परियोजनाओं के लिए स्पेसिफिकेशन्स विकसित करते हैं।
नोट_:_ उनके निष्पादन समय के आधार पर दो नियमों की तुलना करने के लिए, हमें उन्हें एक साथ चलाना होगा और CLI कमांड में --cache none जोड़कर यह सुनिश्चित करना होगा कि कैश (cache) बंद है।
सभी शर्तों (Conditions) को हैंडल किया जाना चाहिए
if/else संरचना स्वाभाविक रूप से यह मांग करती है कि सभी शर्तों को ध्यान में रखा जाए। if ब्लॉक विशिष्ट मामलों को संभालता है, जबकि else ब्लॉक उन सभी मामलों के लिए एक कैच-ऑल (catch-all) के रूप में कार्य करता है जिनका स्पष्ट रूप से if में उल्लेख नहीं किया गया है।
यह एक अच्छी और बुरी दोनों बात है। यह अच्छा है क्योंकि यह सुनिश्चित करता है कि सभी शर्तों पर विचार किया गया है, जिससे किसी भी मामले के छूटने की संभावना रुकती है। हालाँकि, कभी-कभी हम केवल किसी विशिष्ट शर्त के परिणाम में रुचि रखते हैं, और सभी शर्तों को ध्यान में रखने की बाध्यता हमें पीछे खींच सकती है और बहुत अधिक समय ले सकती है।
उदाहरण के लिए, आइए इस नियम से एक रिवर्ट मामले: x * y > max_uint256 को स्पष्ट रूप से हटा दें (omit कर दें), और प्रोवर वह काउंटर-एग्जांपल (counterexample) दिखाएगा जहाँ x * y, max_uint256 से अधिक हो जाता है।
/// CVL
rule mulDivUp_roundOrRevert_omittedARevertCase() {
uint256 x;
uint256 y;
uint256 denominator;
mathint result = mulDivUp@withrevert(x, y, denominator);
if (denominator == 0) { // intentionally omitted `x * y > max_uint256`
assert lastReverted;
} else {
if (x * y % denominator == 0) {
assert !lastReverted;
assert result == x * y / denominator;
} else {
assert !lastReverted;
assert result == (x * y / denominator) + 1;
}
}
}
यदि हम केवल रिवर्ट शर्त denominator == 0 में रुचि रखते हैं, तो हम केवल if/else संरचना का उपयोग करके विशेष रूप से इस पर विचार नहीं कर सकते (तकनीकी रूप से, हम कर सकते हैं, लेकिन यह हैकी (hacky) तरीका है और इससे बचना ही सबसे अच्छा है)। हमें अन्य सभी रिवर्ट मामलों को भी ध्यान में रखना होगा।
इसे संभालने का सही (idiomatic) तरीका इम्पलिकेशन ऑपरेटर (implication operator) है, जिसे अगले अध्याय में कवर किया जाएगा।
टर्नरी ऑपरेटर (Ternary Operator)
टर्नरी ऑपरेटर (Ternary operator) सरल कंडीशनल लॉजिक के लिए if/else स्टेटमेंट्स का एक संक्षिप्त (concise) विकल्प है। सिंटैक्स condition ? expressionA : expressionB का उपयोग करते हुए, यदि शर्त true है तो यह expressionA लौटाता है; अन्यथा, यह expressionB लौटाता है।
हमारा पिछला उदाहरण, max() फंक्शन, सीधे टर्नरी एक्सप्रेशन का उपयोग करके अनुवादित किया जा सकता है, जैसा कि नीचे दिखाया गया है:
/// CVL
rule max_returnMax_ifElse() {
uint256 x;
uint256 y;
mathint expectedMax;
if (x >= y) {
expectedMax = x;
} else {
expectedMax = y;
}
mathint resultMax = max@withrevert(x, y);
assert !lastReverted;
assert resultMax == expectedMax;
}
rule max_returnMax_ternary() {
uint256 x;
uint256 y;
mathint resultMax = max@withrevert(x, y);
assert !lastReverted;
uint256 expectedMax = x > y ? x : y;
assert resultMax == expectedMax;
}
प्रोवर रन: link
हालाँकि, एक अन्य उदाहरण, add() में, हम भी एक टर्नरी एक्सप्रेशन का उपयोग कर सकते हैं, लेकिन केवल चयनात्मक (selectively) रूप से। हम नीचे दिखाए गए अनुसार सभी संभावित निष्पादन मार्गों (execution paths) को शामिल नहीं कर सकते हैं:
/// CVL
rule add_sumWithOverflowRevert_ifElse() {
uint256 x;
uint256 y;
mathint _sum = x + y;
if (_sum <= max_uint256) {
mathint result = add@withrevert(x, y);
assert !lastReverted;
assert result == _sum;
}
else {
add@withrevert(x, y);
assert lastReverted;
}
}
rule add_sumWithOverflowRevert_ternary() {
uint256 x;
uint256 y;
mathint _sum = x + y;
mathint result = add@withrevert(x, y);
assert _sum <= max_uint256 ? !lastReverted : lastReverted; // selective
}
प्रोवर रन: link
हम अन्य शर्तों को ध्यान में क्यों नहीं रख सकते, इसका कारण यह है कि टर्नरी ऑपरेशन में रिटर्न एक्सप्रेशन्स समान टाइप (type) के होने चाहिए। इसलिए, इसे इस तरह एशर्ट करना: _sum <= max_uint256 ? _sum : lastReverted संभव नहीं है क्योंकि _sum एक mathint टाइप है, जबकि lastReverted एक बूलियन (boolean) है।
अंत में, mulDivUp() के लिए भी, हम इसका सीधा अनुवाद नहीं कर सकते हैं; हमें एक-एक करके गुणों (properties) को चुनना होगा और प्रत्येक पर टर्नरी लागू करना होगा, ठीक वैसे ही जैसे हमने add() के साथ किया था।
सारांश (Summary)
- अन्य प्रोग्रामिंग भाषाओं से परिचित होने के कारण
if/elseसमझना आसान (intuitive) है। - बहुत अधिक कंडीशनल ब्रांच प्रोवर (Prover) को धीमा कर देती हैं, लेकिन ऑप्टिमाइज़ेशन से दक्षता में सुधार हो सकता है।
if/elseमें सभी शर्तों को संभालने की आवश्यकता होती है, जिससे यह अलग-अलग (isolated) मामलों के सत्यापन के लिए अव्यावहारिक हो जाता है।- टर्नरी ऑपरेटर एक संक्षिप्त विकल्प प्रदान करता है लेकिन रिटर्न टाइप भिन्न होने पर यह काम नहीं करता है।
पाठकों के लिए अभ्यास
- औपचारिक रूप से सत्यापित करें कि Solady min हमेशा न्यूनतम (min) लौटाता है।
- औपचारिक रूप से सत्यापित करें कि Solady zeroFloorSub
max(0, x - y)लौटाता है। दूसरे शब्दों में, यदिx,yसे कम है, तो यह0लौटाता है। अन्यथा, यहx - yलौटाता है।
यह लेख Certora Prover का उपयोग करके औपचारिक सत्यापन (formal verification using the Certora Prover) पर एक श्रृंखला का हिस्सा है।