---
title: "سمارٹ کنٹریکٹس کی رسمی تصدیق"
description: "ایتھیریم سمارٹ کنٹریکٹس کے لیے رسمی تصدیق کا ایک جائزہ"
lang: ur
---

[سمارٹ کنٹریکٹس](/developers/docs/smart-contracts/) لامركزی، بلا اعتماد، اور مضبوط ایپلی کیشنز بنانا ممکن بنا رہے ہیں جو نئے استعمال کے کیسز متعارف کراتے ہیں اور صارفین کے لیے قدر کو کھولتے ہیں۔ چونکہ سمارٹ کنٹریکٹس بڑی مقدار میں قدر کو سنبھالتے ہیں، اس لیے سیکیورٹی ڈیولپرز کے لیے ایک اہم غور طلب بات ہے۔

رسمی تصدیق [سمارٹ کنٹریکٹ کی سیکیورٹی](/developers/docs/smart-contracts/security/) کو بہتر بنانے کے لیے تجویز کردہ تکنیکوں میں سے ایک ہے۔ رسمی تصدیق، جو پروگراموں کی تخصیص، ڈیزائن، اور تصدیق کے لیے [رسمی طریقوں](https://www.brookings.edu/techstream/formal-methods-as-a-path-toward-better-cybersecurity/) کا استعمال کرتی ہے، سالوں سے اہم ہارڈویئر اور سافٹ ویئر سسٹمز کی درستگی کو یقینی بنانے کے لیے استعمال ہو رہی ہے۔

جب سمارٹ کنٹریکٹس میں لاگو کیا جاتا ہے، تو رسمی تصدیق یہ ثابت کر سکتی ہے کہ کنٹریکٹ کی بزنس لاجک پہلے سے طے شدہ تخصیص پر پورا اترتی ہے۔ کنٹریکٹ کوڈ کی درستگی کا اندازہ لگانے کے دیگر طریقوں، جیسے کہ ٹیسٹنگ، کے مقابلے میں، رسمی تصدیق مضبوط ضمانتیں دیتی ہے کہ ایک سمارٹ کنٹریکٹ عملی طور پر درست ہے۔

## رسمی تصدیق کیا ہے؟ {#what-is-formal-verification}

رسمی تصدیق سے مراد کسی رسمی تخصیص کے حوالے سے سسٹم کی درستگی کا جائزہ لینے کا عمل ہے۔ آسان الفاظ میں، رسمی تصدیق ہمیں یہ جانچنے کی اجازت دیتی ہے کہ آیا کسی سسٹم کا رویہ کچھ تقاضوں کو پورا کرتا ہے (یعنی، یہ وہی کرتا ہے جو ہم چاہتے ہیں)۔

سسٹم کے متوقع رویوں (اس معاملے میں ایک سمارٹ کنٹریکٹ) کو رسمی ماڈلنگ کا استعمال کرتے ہوئے بیان کیا جاتا ہے، جبکہ تخصیص کی زبانیں رسمی خصوصیات کی تخلیق کو قابل بناتی ہیں۔ رسمی تصدیق کی تکنیکیں پھر اس بات کی تصدیق کر سکتی ہیں کہ کنٹریکٹ کا نفاذ اس کی تخصیص کے مطابق ہے اور اس کی درستگی کا ریاضیاتی ثبوت اخذ کر سکتی ہیں۔ جب کوئی کنٹریکٹ اپنی تخصیص کو پورا کرتا ہے، تو اسے "عملی طور پر درست"، "ڈیزائن کے لحاظ سے درست"، یا "تعمیر کے لحاظ سے درست" کے طور پر بیان کیا جاتا ہے۔

### رسمی ماڈل کیا ہے؟ {#what-is-a-formal-model}

کمپیوٹر سائنس میں، ایک [رسمی ماڈل](https://en.wikipedia.org/wiki/Model_of_computation) ایک کمپیوٹیشنل عمل کی ریاضیاتی وضاحت ہے۔ پروگراموں کو ریاضیاتی افعال (مساوات) میں مجرد کیا جاتا ہے، جس میں ماڈل یہ بیان کرتا ہے کہ ان پٹ دیے جانے پر افعال کے آؤٹ پٹس کا حساب کیسے لگایا جاتا ہے۔

رسمی ماڈلز تجرید کی ایک سطح فراہم کرتے ہیں جس پر پروگرام کے رویے کے تجزیے کا جائزہ لیا جا سکتا ہے۔ رسمی ماڈلز کی موجودگی ایک _رسمی تخصیص_ کی تخلیق کی اجازت دیتی ہے، جو زیر بحث ماڈل کی مطلوبہ خصوصیات کو بیان کرتی ہے۔

رسمی تصدیق کے لیے سمارٹ کنٹریکٹس کی ماڈلنگ کے لیے مختلف تکنیکیں استعمال کی جاتی ہیں۔ مثال کے طور پر، کچھ ماڈلز کا استعمال سمارٹ کنٹریکٹ کے اعلیٰ سطحی رویے کے بارے میں استدلال کرنے کے لیے کیا جاتا ہے۔ یہ ماڈلنگ تکنیکیں سمارٹ کنٹریکٹس پر بلیک باکس ویو کا اطلاق کرتی ہیں، انہیں ایسے سسٹمز کے طور پر دیکھتی ہیں جو ان پٹس کو قبول کرتے ہیں اور ان ان پٹس کی بنیاد پر کمپیوٹیشن کو انجام دیتے ہیں۔

اعلیٰ سطحی ماڈلز سمارٹ کنٹریکٹس اور بیرونی ایجنٹس، جیسے کہ بیرونی ملکیت والے اکاؤنٹس (<span dir="ltr">EOAs</span>)، کنٹریکٹ اکاؤنٹس، اور بلاک چین ماحول کے درمیان تعلق پر توجہ مرکوز کرتے ہیں۔ اس طرح کے ماڈلز ان خصوصیات کی وضاحت کے لیے مفید ہیں جو یہ بتاتی ہیں کہ صارف کے مخصوص تعاملات کے جواب میں کنٹریکٹ کو کیسا برتاؤ کرنا چاہیے۔

اس کے برعکس، دیگر رسمی ماڈلز سمارٹ کنٹریکٹ کے نچلی سطح کے رویے پر توجہ مرکوز کرتے ہیں۔ اگرچہ اعلیٰ سطحی ماڈلز کنٹریکٹ کی فعالیت کے بارے میں استدلال کرنے میں مدد کر سکتے ہیں، لیکن وہ نفاذ کے اندرونی کام کے بارے میں تفصیلات حاصل کرنے میں ناکام ہو سکتے ہیں۔ نچلی سطح کے ماڈلز پروگرام کے تجزیے پر وائٹ باکس ویو کا اطلاق کرتے ہیں اور سمارٹ کنٹریکٹ ایپلی کیشنز کی نچلی سطح کی نمائندگیوں پر انحصار کرتے ہیں، جیسے کہ پروگرام ٹریسز اور [کنٹرول فلو گرافس](https://en.wikipedia.org/wiki/Control-flow_graph)، تاکہ کنٹریکٹ کے نفاذ سے متعلق خصوصیات کے بارے میں استدلال کیا جا سکے۔

نچلی سطح کے ماڈلز کو مثالی سمجھا جاتا ہے کیونکہ وہ ایتھیریم کے ایگزیکیوشن ماحول (یعنی، [<span dir="ltr">EVM</span>](/developers/docs/evm/)) میں سمارٹ کنٹریکٹ کے اصل نفاذ کی نمائندگی کرتے ہیں۔ نچلی سطح کی ماڈلنگ تکنیکیں خاص طور پر سمارٹ کنٹریکٹس میں اہم حفاظتی خصوصیات قائم کرنے اور ممکنہ کمزوریوں کا پتہ لگانے میں مفید ہیں۔

### رسمی تخصیص کیا ہے؟ {#what-is-a-formal-specification}

تخصیص محض ایک تکنیکی تقاضا ہے جسے کسی خاص سسٹم کو پورا کرنا چاہیے۔ پروگرامنگ میں، تخصیصات پروگرام کے نفاذ کے بارے میں عمومی خیالات کی نمائندگی کرتی ہیں (یعنی، پروگرام کو کیا کرنا چاہیے)۔

سمارٹ کنٹریکٹس کے تناظر میں، رسمی تخصیصات سے مراد _خصوصیات_ ہیں—ان تقاضوں کی رسمی وضاحتیں جنہیں کنٹریکٹ کو پورا کرنا چاہیے۔ ایسی خصوصیات کو "<span dir="ltr">invariants</span>" کے طور پر بیان کیا جاتا ہے اور یہ کنٹریکٹ کے نفاذ کے بارے میں منطقی دعووں کی نمائندگی کرتی ہیں جنہیں ہر ممکنہ صورتحال میں، بغیر کسی استثنا کے، درست رہنا چاہیے۔

اس طرح، ہم ایک رسمی تخصیص کو رسمی زبان میں لکھے گئے بیانات کے مجموعے کے طور پر سوچ سکتے ہیں جو سمارٹ کنٹریکٹ کے مطلوبہ نفاذ کو بیان کرتے ہیں۔ تخصیصات کنٹریکٹ کی خصوصیات کا احاطہ کرتی ہیں اور اس بات کی وضاحت کرتی ہیں کہ مختلف حالات میں کنٹریکٹ کو کیسا برتاؤ کرنا چاہیے۔ رسمی تصدیق کا مقصد یہ تعین کرنا ہے کہ آیا سمارٹ کنٹریکٹ میں یہ خصوصیات (<span dir="ltr">invariants</span>) موجود ہیں اور یہ کہ نفاذ کے دوران ان خصوصیات کی خلاف ورزی نہیں ہوتی ہے۔

سمارٹ کنٹریکٹس کے محفوظ نفاذ کو تیار کرنے میں رسمی تخصیصات اہم ہیں۔ وہ کنٹریکٹس جو <span dir="ltr">invariants</span> کو نافذ کرنے میں ناکام رہتے ہیں یا نفاذ کے دوران ان کی خصوصیات کی خلاف ورزی ہوتی ہے، وہ ایسی کمزوریوں کا شکار ہوتے ہیں جو فعالیت کو نقصان پہنچا سکتی ہیں یا بدنیتی پر مبنی استحصال کا سبب بن سکتی ہیں۔

## سمارٹ کنٹریکٹس کے لیے رسمی تخصیصات کی اقسام {#formal-specifications-for-smart-contracts}

رسمی تخصیصات پروگرام کے نفاذ کی درستگی کے بارے میں ریاضیاتی استدلال کو قابل بناتی ہیں۔ رسمی ماڈلز کی طرح، رسمی تخصیصات یا تو اعلیٰ سطحی خصوصیات یا کنٹریکٹ کے نفاذ کے نچلی سطح کے رویے کو حاصل کر سکتی ہیں۔

رسمی تخصیصات [پروگرام لاجک](https://en.wikipedia.org/wiki/Logic_programming) کے عناصر کا استعمال کرتے ہوئے اخذ کی جاتی ہیں، جو پروگرام کی خصوصیات کے بارے میں رسمی استدلال کی اجازت دیتی ہیں۔ پروگرام لاجک میں رسمی اصول ہوتے ہیں جو (ریاضیاتی زبان میں) پروگرام کے متوقع رویے کا اظہار کرتے ہیں۔ رسمی تخصیصات بنانے میں مختلف پروگرام لاجکس استعمال کی جاتی ہیں، جن میں [ریچ ایبلٹی لاجک](https://en.wikipedia.org/wiki/Reachability_problem)، [ٹیمپورل لاجک](https://en.wikipedia.org/wiki/Temporal_logic)، اور [<span dir="ltr">Hoare</span> لاجک](https://en.wikipedia.org/wiki/Hoare_logic) شامل ہیں۔

سمارٹ کنٹریکٹس کے لیے رسمی تخصیصات کو وسیع پیمانے پر **اعلیٰ سطحی** یا **نچلی سطح** کی تخصیصات کے طور پر درجہ بند کیا جا سکتا ہے۔ اس بات سے قطع نظر کہ کوئی تخصیص کس زمرے سے تعلق رکھتی ہے، اسے تجزیہ کے تحت سسٹم کی خصوصیت کو مناسب اور غیر مبہم طور پر بیان کرنا چاہیے۔

### اعلیٰ سطحی تخصیصات {#high-level-specifications}

جیسا کہ نام سے ظاہر ہے، ایک اعلیٰ سطحی تخصیص (جسے "ماڈل پر مبنی تخصیص" بھی کہا جاتا ہے) پروگرام کے اعلیٰ سطحی رویے کو بیان کرتی ہے۔ اعلیٰ سطحی تخصیصات ایک سمارٹ کنٹریکٹ کو [فائنائٹ اسٹیٹ مشین](https://en.wikipedia.org/wiki/Finite-state_machine) (<span dir="ltr">FSM</span>) کے طور پر ماڈل کرتی ہیں، جو آپریشنز انجام دے کر حالتوں کے درمیان منتقل ہو سکتی ہے، جس میں <span dir="ltr">FSM</span> ماڈل کے لیے رسمی خصوصیات کی وضاحت کے لیے ٹیمپورل لاجک کا استعمال کیا جاتا ہے۔

[ٹیمپورل لاجکس](https://en.wikipedia.org/wiki/Temporal_logic) "وقت کے لحاظ سے اہل تجاویز کے بارے میں استدلال کے اصول ہیں (مثلاً، "میں _ہمیشہ_ بھوکا رہتا ہوں" یا "میں _بالآخر_ بھوکا ہو جاؤں گا")۔" جب رسمی تصدیق پر لاگو کیا جاتا ہے، تو ٹیمپورل لاجکس کا استعمال اسٹیٹ مشینوں کے طور پر ماڈل کیے گئے سسٹمز کے درست رویے کے بارے میں دعوے بیان کرنے کے لیے کیا جاتا ہے۔ خاص طور پر، ایک ٹیمپورل لاجک ان مستقبل کی حالتوں کو بیان کرتی ہے جن میں ایک سمارٹ کنٹریکٹ ہو سکتا ہے اور یہ حالتوں کے درمیان کیسے منتقل ہوتا ہے۔

اعلیٰ سطحی تخصیصات عام طور پر سمارٹ کنٹریکٹس کے لیے دو اہم وقتی خصوصیات کو حاصل کرتی ہیں: **حفاظت** اور **<span dir="ltr">liveness</span>**۔ حفاظتی خصوصیات اس خیال کی نمائندگی کرتی ہیں کہ "کبھی کچھ برا نہیں ہوتا" اور عام طور پر ناقابلِ تغیر کا اظہار کرتی ہیں۔ ایک حفاظتی خصوصیت عام سافٹ ویئر کے تقاضوں کی وضاحت کر سکتی ہے، جیسے کہ [ڈیڈلاک](https://www.techtarget.com/whatis/definition/deadlock) سے آزادی، یا کنٹریکٹس کے لیے ڈومین کے لحاظ سے مخصوص خصوصیات کا اظہار کر سکتی ہے (مثلاً، افعال کے لیے رسائی کنٹرول پر <span dir="ltr">invariants</span>، حالت کے متغیرات کی قابل قبول اقدار، یا ٹوکن کی منتقلی کے لیے شرائط)۔

مثال کے طور پر اس حفاظتی تقاضے کو لیں جو <span dir="ltr">ERC-20</span> ٹوکن کنٹریکٹس میں `transfer()` یا `transferFrom()` استعمال کرنے کی شرائط کا احاطہ کرتا ہے: _"بھیجنے والے کا بیلنس کبھی بھی بھیجے جانے والے ٹوکنز کی مطلوبہ مقدار سے کم نہیں ہوتا ہے۔"_۔ کنٹریکٹ <span dir="ltr">invariant</span> کی اس قدرتی زبان کی وضاحت کو ایک رسمی (ریاضیاتی) تخصیص میں ترجمہ کیا جا سکتا ہے، جسے پھر درستگی کے لیے سختی سے جانچا جا سکتا ہے۔

<span dir="ltr">liveness</span> کی خصوصیات اس بات کی تصدیق کرتی ہیں کہ "بالآخر کچھ اچھا ہوتا ہے" اور ان کا تعلق کنٹریکٹ کی مختلف حالتوں میں آگے بڑھنے کی صلاحیت سے ہے۔ <span dir="ltr">liveness</span> کی خصوصیت کی ایک مثال "سیالیت" ہے، جس سے مراد کنٹریکٹ کی درخواست پر صارفین کو اپنے بیلنس منتقل کرنے کی صلاحیت ہے۔ اگر اس خصوصیت کی خلاف ورزی ہوتی ہے، تو صارفین کنٹریکٹ میں محفوظ اثاثے نکالنے سے قاصر ہوں گے، جیسا کہ [<span dir="ltr">Parity</span> والیٹ کے واقعے](https://www.cnbc.com/2017/11/08/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-wallet.html) کے ساتھ ہوا تھا۔

### نچلی سطح کی تخصیصات {#low-level-specifications}

اعلیٰ سطحی تخصیصات ایک کنٹریکٹ کے فائنائٹ اسٹیٹ ماڈل کو نقطہ آغاز کے طور پر لیتی ہیں اور اس ماڈل کی مطلوبہ خصوصیات کی وضاحت کرتی ہیں۔ اس کے برعکس، نچلی سطح کی تخصیصات (جنہیں "خصوصیت پر مبنی تخصیصات" بھی کہا جاتا ہے) اکثر پروگراموں (سمارٹ کنٹریکٹس) کو ریاضیاتی افعال کے مجموعے پر مشتمل سسٹمز کے طور پر ماڈل کرتی ہیں اور ایسے سسٹمز کے درست رویے کو بیان کرتی ہیں۔

آسان الفاظ میں، نچلی سطح کی تخصیصات _پروگرام ٹریسز_ کا تجزیہ کرتی ہیں اور ان ٹریسز پر سمارٹ کنٹریکٹ کی خصوصیات کی وضاحت کرنے کی کوشش کرتی ہیں۔ ٹریسز سے مراد فنکشن کے نفاذ کی وہ ترتیب ہے جو سمارٹ کنٹریکٹ کی حالت کو تبدیل کرتی ہے؛ لہذا، نچلی سطح کی تخصیصات کنٹریکٹ کے اندرونی نفاذ کے لیے تقاضوں کی وضاحت کرنے میں مدد کرتی ہیں۔

نچلی سطح کی رسمی تخصیصات کو یا تو <span dir="ltr">Hoare</span> طرز کی خصوصیات یا ایگزیکیوشن پاتھس پر <span dir="ltr">invariants</span> کے طور پر دیا جا سکتا ہے۔

### <span dir="ltr">Hoare</span> طرز کی خصوصیات {#hoare-style-properties}

[<span dir="ltr">Hoare</span> لاجک](https://en.wikipedia.org/wiki/Hoare_logic) سمارٹ کنٹریکٹس سمیت پروگراموں کی درستگی کے بارے میں استدلال کے لیے رسمی اصولوں کا ایک مجموعہ فراہم کرتی ہے۔ ایک <span dir="ltr">Hoare</span> طرز کی خصوصیت کو <span dir="ltr">Hoare</span> ٹرپل `{P}c{Q}` کے ذریعے ظاہر کیا جاتا ہے، جہاں `c` ایک پروگرام ہے اور `P` اور `Q` `c` (یعنی، پروگرام) کی حالت پر پیشین گوئیاں ہیں، جنہیں بالترتیب _پری کنڈیشنز_ اور _پوسٹ کنڈیشنز_ کے طور پر رسمی طور پر بیان کیا گیا ہے۔

ایک پری کنڈیشن ایک پیشین گوئی ہے جو کسی فنکشن کے درست نفاذ کے لیے درکار شرائط کو بیان کرتی ہے؛ کنٹریکٹ میں کال کرنے والے صارفین کو اس تقاضے کو پورا کرنا چاہیے۔ ایک پوسٹ کنڈیشن ایک پیشین گوئی ہے جو اس شرط کو بیان کرتی ہے جو ایک فنکشن درست طریقے سے نافذ ہونے پر قائم کرتا ہے؛ صارفین فنکشن میں کال کرنے کے بعد اس شرط کے درست ہونے کی توقع کر سکتے ہیں۔ <span dir="ltr">Hoare</span> لاجک میں ایک _<span dir="ltr">invariant</span>_ ایک پیشین گوئی ہے جو کسی فنکشن کے نفاذ سے محفوظ رہتی ہے (یعنی، یہ تبدیل نہیں ہوتی)۔

<span dir="ltr">Hoare</span> طرز کی تخصیصات یا تو _جزوی درستگی_ یا _مکمل درستگی_ کی ضمانت دے سکتی ہیں۔ کنٹریکٹ فنکشن کا نفاذ "جزوی طور پر درست" ہوتا ہے اگر فنکشن کے نافذ ہونے سے پہلے پری کنڈیشن درست ہو، اور اگر نفاذ ختم ہو جائے، تو پوسٹ کنڈیشن بھی درست ہو۔ مکمل درستگی کا ثبوت اس وقت حاصل ہوتا ہے جب فنکشن کے نافذ ہونے سے پہلے ایک پری کنڈیشن درست ہو، نفاذ کے ختم ہونے کی ضمانت دی گئی ہو اور جب ایسا ہوتا ہے، تو پوسٹ کنڈیشن درست ثابت ہوتی ہے۔

مکمل درستگی کا ثبوت حاصل کرنا مشکل ہے کیونکہ کچھ نفاذ ختم ہونے سے پہلے تاخیر کا شکار ہو سکتے ہیں، یا کبھی ختم ہی نہیں ہوتے۔ اس کے باوجود، یہ سوال کہ آیا نفاذ ختم ہوتا ہے، بحث طلب ہے کیونکہ ایتھیریم کا گیس میکانزم لامحدود پروگرام لوپس کو روکتا ہے (نفاذ یا تو کامیابی کے ساتھ ختم ہوتا ہے یا '<span dir="ltr">out-of-gas</span>' ایرر کی وجہ سے ختم ہوتا ہے)۔

<span dir="ltr">Hoare</span> لاجک کا استعمال کرتے ہوئے بنائی گئی سمارٹ کنٹریکٹ کی تخصیصات میں کنٹریکٹ میں افعال اور لوپس کے نفاذ کے لیے پری کنڈیشنز، پوسٹ کنڈیشنز، اور <span dir="ltr">invariants</span> کی وضاحت کی جائے گی۔ پری کنڈیشنز میں اکثر کسی فنکشن میں غلط ان پٹس کا امکان شامل ہوتا ہے، جس میں پوسٹ کنڈیشنز ایسے ان پٹس کے متوقع ردعمل کو بیان کرتی ہیں (مثلاً، ایک مخصوص استثنا پھینکنا)۔ اس طرح <span dir="ltr">Hoare</span> طرز کی خصوصیات کنٹریکٹ کے نفاذ کی درستگی کو یقینی بنانے کے لیے موثر ہیں۔

بہت سے رسمی تصدیق کے فریم ورکس افعال کی معنوی درستگی کو ثابت کرنے کے لیے <span dir="ltr">Hoare</span> طرز کی تخصیصات کا استعمال کرتے ہیں۔ <span dir="ltr">Solidity</span> میں `require` اور `assert` اسٹیٹمنٹس کا استعمال کر کے براہ راست کنٹریکٹ کوڈ میں <span dir="ltr">Hoare</span> طرز کی خصوصیات (بطور دعوے) شامل کرنا بھی ممکن ہے۔

`require` اسٹیٹمنٹس ایک پری کنڈیشن یا <span dir="ltr">invariant</span> کا اظہار کرتی ہیں اور اکثر صارف کے ان پٹس کی توثیق کے لیے استعمال ہوتی ہیں، جبکہ `assert` حفاظت کے لیے ضروری پوسٹ کنڈیشن کو حاصل کرتی ہے۔ مثال کے طور پر، افعال کے لیے مناسب رسائی کنٹرول (حفاظتی خصوصیت کی ایک مثال) کال کرنے والے اکاؤنٹ کی شناخت پر پری کنڈیشن چیک کے طور پر `require` کا استعمال کر کے حاصل کیا جا سکتا ہے۔ اسی طرح، کنٹریکٹ میں حالت کے متغیرات کی قابل قبول اقدار پر ایک <span dir="ltr">invariant</span> (مثلاً، گردش میں ٹوکنز کی کل تعداد) کو فنکشن کے نفاذ کے بعد کنٹریکٹ کی حالت کی تصدیق کرنے کے لیے `assert` کا استعمال کر کے خلاف ورزی سے بچایا جا سکتا ہے۔

### ٹریس لیول کی خصوصیات {#trace-level-properties}

ٹریس پر مبنی تخصیصات ان آپریشنز کو بیان کرتی ہیں جو ایک کنٹریکٹ کو مختلف حالتوں کے درمیان منتقل کرتے ہیں اور ان آپریشنز کے درمیان تعلقات کو بیان کرتے ہیں۔ جیسا کہ پہلے بتایا گیا ہے، ٹریسز ان آپریشنز کی ترتیب ہیں جو کسی خاص طریقے سے کنٹریکٹ کی حالت کو تبدیل کرتے ہیں۔

یہ نقطہ نظر سمارٹ کنٹریکٹس کے ماڈل پر انحصار کرتا ہے جو کہ کچھ پہلے سے طے شدہ حالتوں (حالت کے متغیرات کے ذریعے بیان کردہ) کے ساتھ ساتھ پہلے سے طے شدہ ٹرانزیشنز (کنٹریکٹ کے افعال کے ذریعے بیان کردہ) کے ایک سیٹ کے ساتھ اسٹیٹ ٹرانزیشن سسٹمز کے طور پر کام کرتے ہیں۔ مزید برآں، ایک [کنٹرول فلو گراف](https://www.geeksforgeeks.org/software-engineering-control-flow-graph-cfg/) (<span dir="ltr">CFG</span>)، جو کہ پروگرام کے ایگزیکیوشن فلو کی گرافیکل نمائندگی ہے، اکثر کنٹریکٹ کے آپریشنل سیمینٹکس کو بیان کرنے کے لیے استعمال ہوتا ہے۔ یہاں، ہر ٹریس کو کنٹرول فلو گراف پر ایک راستے کے طور پر دکھایا گیا ہے۔

بنیادی طور پر، ٹریس لیول کی تخصیصات کا استعمال سمارٹ کنٹریکٹس میں اندرونی نفاذ کے پیٹرنز کے بارے میں استدلال کرنے کے لیے کیا جاتا ہے۔ ٹریس لیول کی تخصیصات بنا کر، ہم سمارٹ کنٹریکٹ کے لیے قابل قبول ایگزیکیوشن پاتھس (یعنی، اسٹیٹ ٹرانزیشنز) کی تصدیق کرتے ہیں۔ علامتی نفاذ جیسی تکنیکوں کا استعمال کرتے ہوئے، ہم رسمی طور پر تصدیق کر سکتے ہیں کہ نفاذ کبھی بھی ایسے راستے پر نہیں چلتا جس کی رسمی ماڈل میں وضاحت نہ کی گئی ہو۔

آئیے ایک [<span dir="ltr">DAO</span>](/dao/) کنٹریکٹ کی مثال استعمال کریں جس میں ٹریس لیول کی خصوصیات کو بیان کرنے کے لیے کچھ عوامی طور پر قابل رسائی افعال موجود ہیں۔ یہاں، ہم فرض کرتے ہیں کہ <span dir="ltr">DAO</span> کنٹریکٹ صارفین کو درج ذیل آپریشنز انجام دینے کی اجازت دیتا ہے:

- فنڈز جمع کرنا

- فنڈز جمع کرنے کے بعد کسی تجویز پر ووٹ دینا

- اگر وہ کسی تجویز پر ووٹ نہیں دیتے ہیں تو ریفنڈ کا دعویٰ کرنا

ٹریس لیول کی خصوصیات کی مثال یہ ہو سکتی ہے _"وہ صارفین جو فنڈز جمع نہیں کرتے وہ کسی تجویز پر ووٹ نہیں دے سکتے"_ یا _"وہ صارفین جو کسی تجویز پر ووٹ نہیں دیتے انہیں ہمیشہ ریفنڈ کا دعویٰ کرنے کے قابل ہونا چاہیے"_۔ دونوں خصوصیات نفاذ کی ترجیحی ترتیب کی تصدیق کرتی ہیں (فنڈز جمع کرنے سے _پہلے_ ووٹنگ نہیں ہو سکتی اور کسی تجویز پر ووٹ دینے کے _بعد_ ریفنڈ کا دعویٰ نہیں کیا جا سکتا)۔

## سمارٹ کنٹریکٹس کی رسمی تصدیق کے لیے تکنیکیں {#formal-verification-techniques}

### ماڈل چیکنگ {#model-checking}

ماڈل چیکنگ ایک رسمی تصدیق کی تکنیک ہے جس میں ایک الگورتھم سمارٹ کنٹریکٹ کے رسمی ماڈل کو اس کی تخصیص کے خلاف جانچتا ہے۔ ماڈل چیکنگ میں سمارٹ کنٹریکٹس کو اکثر اسٹیٹ ٹرانزیشن سسٹمز کے طور پر پیش کیا جاتا ہے، جبکہ قابل قبول کنٹریکٹ کی حالتوں پر خصوصیات کو ٹیمپورل لاجک کا استعمال کرتے ہوئے بیان کیا جاتا ہے۔

ماڈل چیکنگ کے لیے سسٹم (یعنی، ایک کنٹریکٹ) کی ایک مجرد ریاضیاتی نمائندگی بنانے اور [پروپوزیشنل لاجک](https://www.baeldung.com/cs/propositional-logic) میں جڑے فارمولوں کا استعمال کرتے ہوئے اس سسٹم کی خصوصیات کا اظہار کرنے کی ضرورت ہوتی ہے۔ یہ ماڈل چیکنگ الگورتھم کے کام کو آسان بناتا ہے، یعنی یہ ثابت کرنا کہ ایک ریاضیاتی ماڈل دیے گئے منطقی فارمولے کو پورا کرتا ہے۔

رسمی تصدیق میں ماڈل چیکنگ بنیادی طور پر وقتی خصوصیات کا جائزہ لینے کے لیے استعمال ہوتی ہے جو وقت کے ساتھ کنٹریکٹ کے رویے کو بیان کرتی ہیں۔ سمارٹ کنٹریکٹس کے لیے وقتی خصوصیات میں _حفاظت_ اور _<span dir="ltr">liveness</span>_ شامل ہیں، جن کی ہم نے پہلے وضاحت کی تھی۔

مثال کے طور پر، رسائی کنٹرول سے متعلق ایک سیکیورٹی خصوصیت (مثلاً، _صرف کنٹریکٹ کا مالک `selfdestruct` کو کال کر سکتا ہے_) کو رسمی لاجک میں لکھا جا سکتا ہے۔ اس کے بعد، ماڈل چیکنگ الگورتھم اس بات کی تصدیق کر سکتا ہے کہ آیا کنٹریکٹ اس رسمی تخصیص کو پورا کرتا ہے۔

ماڈل چیکنگ اسٹیٹ اسپیس ایکسپلوریشن کا استعمال کرتی ہے، جس میں سمارٹ کنٹریکٹ کی تمام ممکنہ حالتوں کی تعمیر اور قابل رسائی حالتوں کو تلاش کرنے کی کوشش شامل ہے جو خصوصیت کی خلاف ورزیوں کا باعث بنتی ہیں۔ تاہم، یہ لامحدود تعداد میں حالتوں کا باعث بن سکتا ہے (جسے "اسٹیٹ ایکسپلوژن پرابلم" کہا جاتا ہے)، اس لیے ماڈل چیکرز سمارٹ کنٹریکٹس کے موثر تجزیے کو ممکن بنانے کے لیے تجرید کی تکنیکوں پر انحصار کرتے ہیں۔

### تھیورم پرونگ (Theorem proving) {#theorem-proving}

تھیورم پرونگ سمارٹ کنٹریکٹس سمیت پروگراموں کی درستگی کے بارے میں ریاضیاتی طور پر استدلال کرنے کا ایک طریقہ ہے۔ اس میں کنٹریکٹ کے سسٹم کے ماڈل اور اس کی تخصیصات کو ریاضیاتی فارمولوں (منطقی بیانات) میں تبدیل کرنا شامل ہے۔

تھیورم پرونگ کا مقصد ان بیانات کے درمیان منطقی مساوات کی تصدیق کرنا ہے۔ "منطقی مساوات" (جسے "منطقی دو طرفہ مفہوم" بھی کہا جاتا ہے) دو بیانات کے درمیان تعلق کی ایک قسم ہے جس میں پہلا بیان درست ہوتا ہے _اگر اور صرف اگر_ دوسرا بیان درست ہو۔

کنٹریکٹ کے ماڈل اور اس کی خصوصیت کے بارے میں بیانات کے درمیان مطلوبہ تعلق (منطقی مساوات) کو ایک قابل ثبوت بیان (جسے تھیورم کہا جاتا ہے) کے طور پر وضع کیا جاتا ہے۔ استدلال کے ایک رسمی نظام کا استعمال کرتے ہوئے، خودکار تھیورم ثابت کنندہ تھیورم کی درستگی کی تصدیق کر سکتا ہے۔ دوسرے الفاظ میں، ایک تھیورم ثابت کنندہ حتمی طور پر ثابت کر سکتا ہے کہ سمارٹ کنٹریکٹ کا ماڈل بالکل اس کی تخصیصات سے میل کھاتا ہے۔

جبکہ ماڈل چیکنگ کنٹریکٹس کو محدود حالتوں کے ساتھ ٹرانزیشن سسٹمز کے طور پر ماڈل کرتی ہے، تھیورم پرونگ لامحدود حالت والے سسٹمز کے تجزیے کو سنبھال سکتی ہے۔ تاہم، اس کا مطلب یہ ہے کہ ایک خودکار تھیورم ثابت کنندہ ہمیشہ یہ نہیں جان سکتا کہ آیا کوئی منطقی مسئلہ "قابل فیصلہ" ہے یا نہیں۔

نتیجے کے طور پر، درستگی کے ثبوت اخذ کرنے میں تھیورم ثابت کنندہ کی رہنمائی کے لیے اکثر انسانی مدد کی ضرورت ہوتی ہے۔ تھیورم پرونگ میں انسانی کوشش کا استعمال اسے ماڈل چیکنگ کے مقابلے میں استعمال کرنے کے لیے زیادہ مہنگا بناتا ہے، جو کہ مکمل طور پر خودکار ہے۔

### علامتی نفاذ (Symbolic execution) {#symbolic-execution}

علامتی نفاذ ٹھوس اقدار (مثلاً، `x == 5`) کے بجائے علامتی اقدار (مثلاً، `x > 5`) کا استعمال کرتے ہوئے افعال کو نافذ کر کے سمارٹ کنٹریکٹ کا تجزیہ کرنے کا ایک طریقہ ہے۔ ایک رسمی تصدیق کی تکنیک کے طور پر، علامتی نفاذ کا استعمال کنٹریکٹ کے کوڈ میں ٹریس لیول کی خصوصیات کے بارے میں رسمی طور پر استدلال کرنے کے لیے کیا جاتا ہے۔

علامتی نفاذ ایک ایگزیکیوشن ٹریس کو علامتی ان پٹ اقدار پر ایک ریاضیاتی فارمولے کے طور پر پیش کرتا ہے، جسے بصورت دیگر _پاتھ پریڈیکیٹ_ کہا جاتا ہے۔ ایک [<span dir="ltr">SMT</span> حل کنندہ](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) کا استعمال یہ جانچنے کے لیے کیا جاتا ہے کہ آیا پاتھ پریڈیکیٹ "قابل اطمینان" ہے (یعنی، کوئی ایسی قدر موجود ہے جو فارمولے کو پورا کر سکے)۔ اگر کوئی کمزور راستہ قابل اطمینان ہے، تو <span dir="ltr">SMT</span> حل کنندہ ایک ٹھوس قدر پیدا کرے گا جو نفاذ کو اس راستے کی طرف لے جائے گا۔

فرض کریں کہ ایک سمارٹ کنٹریکٹ کا فنکشن ان پٹ کے طور پر ایک `uint` قدر (`x`) لیتا ہے اور جب `x` `5` سے زیادہ اور `10` سے کم ہو تو ریورٹ (<span dir="ltr">revert</span>) ہو جاتا ہے۔ ایک عام ٹیسٹنگ کے طریقہ کار کا استعمال کرتے ہوئے `x` کے لیے ایسی قدر تلاش کرنا جو ایرر کو متحرک کرے، درجنوں ٹیسٹ کیسز (یا اس سے زیادہ) کو چلانے کی ضرورت ہوگی، اس یقین دہانی کے بغیر کہ واقعی کوئی ایرر پیدا کرنے والا ان پٹ مل جائے گا۔

اس کے برعکس، ایک علامتی نفاذ کا ٹول علامتی قدر کے ساتھ فنکشن کو نافذ کرے گا: `X > 5 ∧ X < 10` (یعنی، `x` <span dir="ltr">5</span> سے زیادہ ہے اور `x` <span dir="ltr">10</span> سے کم ہے)۔ اس سے وابستہ پاتھ پریڈیکیٹ `x = X > 5 ∧ X < 10` پھر حل کرنے کے لیے <span dir="ltr">SMT</span> حل کنندہ کو دیا جائے گا۔ اگر کوئی خاص قدر فارمولہ `x = X > 5 ∧ X < 10` کو پورا کرتی ہے، تو <span dir="ltr">SMT</span> حل کنندہ اس کا حساب لگائے گا—مثال کے طور پر، حل کنندہ `x` کے لیے ایک قدر کے طور پر `7` پیدا کر سکتا ہے۔

چونکہ علامتی نفاذ پروگرام کے ان پٹس پر انحصار کرتا ہے، اور تمام قابل رسائی حالتوں کو دریافت کرنے کے لیے ان پٹس کا سیٹ ممکنہ طور پر لامحدود ہے، اس لیے یہ اب بھی ٹیسٹنگ کی ایک شکل ہے۔ تاہم، جیسا کہ مثال میں دکھایا گیا ہے، علامتی نفاذ ان ان پٹس کو تلاش کرنے کے لیے باقاعدہ ٹیسٹنگ سے زیادہ موثر ہے جو خصوصیت کی خلاف ورزیوں کو متحرک کرتے ہیں۔

مزید برآں، علامتی نفاذ دیگر خصوصیت پر مبنی تکنیکوں (مثلاً، فزنگ (<span dir="ltr">fuzzing</span>)) کے مقابلے میں کم غلط مثبت پیدا کرتا ہے جو تصادفی طور پر کسی فنکشن کے لیے ان پٹس پیدا کرتی ہیں۔ اگر علامتی نفاذ کے دوران کوئی ایرر اسٹیٹ متحرک ہوتی ہے، تو ایک ٹھوس قدر پیدا کرنا ممکن ہے جو ایرر کو متحرک کرے اور مسئلے کو دوبارہ پیدا کرے۔

علامتی نفاذ درستگی کا کچھ حد تک ریاضیاتی ثبوت بھی فراہم کر سکتا ہے۔ اوور فلو تحفظ کے ساتھ کنٹریکٹ فنکشن کی درج ذیل مثال پر غور کریں:

```
function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}
```

ایک ایگزیکیوشن ٹریس جس کے نتیجے میں انٹیجر اوور فلو ہوتا ہے اسے اس فارمولے کو پورا کرنے کی ضرورت ہوگی: `z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y)` اس طرح کے فارمولے کے حل ہونے کا امکان نہیں ہے، اس لیے یہ ایک ریاضیاتی ثبوت کے طور پر کام کرتا ہے کہ فنکشن `safe_add` کبھی اوور فلو نہیں ہوتا ہے۔

### سمارٹ کنٹریکٹس کے لیے رسمی تصدیق کیوں استعمال کریں؟ {#benefits-of-formal-verification}

#### قابل اعتمادی کی ضرورت {#need-for-reliability}

رسمی تصدیق کا استعمال ان حفاظتی لحاظ سے اہم سسٹمز کی درستگی کا جائزہ لینے کے لیے کیا جاتا ہے جن کی ناکامی کے تباہ کن نتائج ہو سکتے ہیں، جیسے کہ موت، چوٹ، یا مالی تباہی۔ سمارٹ کنٹریکٹس اعلیٰ قدر والی ایپلی کیشنز ہیں جو بہت زیادہ قدر کو کنٹرول کرتی ہیں، اور ڈیزائن میں سادہ غلطیاں [صارفین کے لیے ناقابل تلافی نقصان](https://www.freecodecamp.org/news/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce/amp/) کا باعث بن سکتی ہیں۔ تاہم، تعیناتی سے پہلے کنٹریکٹ کی رسمی تصدیق کرنے سے اس بات کی ضمانت بڑھ سکتی ہے کہ بلاک چین پر چلنے کے بعد یہ توقع کے مطابق کارکردگی دکھائے گا۔

کسی بھی سمارٹ کنٹریکٹ میں قابل اعتمادی ایک انتہائی مطلوبہ خوبی ہے، خاص طور پر اس لیے کہ [ایتھیریم](/) ورچوئل مشین (<span dir="ltr">EVM</span>) میں تعینات کیا گیا کوڈ عام طور پر ناقابلِ تبدیلی ہوتا ہے۔ لانچ کے بعد اپ گریڈز آسانی سے قابل رسائی نہ ہونے کی وجہ سے، کنٹریکٹس کی قابل اعتمادی کی ضمانت دینے کی ضرورت رسمی تصدیق کو ضروری بناتی ہے۔ رسمی تصدیق پیچیدہ مسائل کا پتہ لگانے کے قابل ہے، جیسے کہ انٹیجر انڈر فلو اور اوور فلو، ری اینٹرنسی (<span dir="ltr">re-entrancy</span>)، اور ناقص گیس آپٹیمائزیشنز، جو آڈیٹرز اور ٹیسٹرز کی نظروں سے بچ سکتے ہیں۔

#### عملی درستگی کو ثابت کرنا {#prove-functional-correctness}

پروگرام ٹیسٹنگ یہ ثابت کرنے کا سب سے عام طریقہ ہے کہ ایک سمارٹ کنٹریکٹ کچھ تقاضوں کو پورا کرتا ہے۔ اس میں اس ڈیٹا کے نمونے کے ساتھ کنٹریکٹ کو نافذ کرنا شامل ہے جسے سنبھالنے کی اس سے توقع کی جاتی ہے اور اس کے رویے کا تجزیہ کرنا شامل ہے۔ اگر کنٹریکٹ نمونے کے ڈیٹا کے لیے متوقع نتائج واپس کرتا ہے، تو ڈیولپرز کے پاس اس کی درستگی کا معروضی ثبوت ہوتا ہے۔

تاہم، یہ نقطہ نظر ان ان پٹ اقدار کے لیے درست نفاذ کو ثابت نہیں کر سکتا جو نمونے کا حصہ نہیں ہیں۔ لہذا، کنٹریکٹ کی ٹیسٹنگ بگز کا پتہ لگانے میں مدد کر سکتی ہے (یعنی، اگر کچھ کوڈ پاتھس نفاذ کے دوران مطلوبہ نتائج واپس کرنے میں ناکام رہتے ہیں)، لیکن **یہ حتمی طور پر بگز کی عدم موجودگی کو ثابت نہیں کر سکتی**۔

اس کے برعکس، رسمی تصدیق رسمی طور پر یہ ثابت کر سکتی ہے کہ ایک سمارٹ کنٹریکٹ کنٹریکٹ کو بالکل چلائے _بغیر_ نفاذ کی لامحدود رینج کے تقاضوں کو پورا کرتا ہے۔ اس کے لیے ایک رسمی تخصیص بنانے کی ضرورت ہوتی ہے جو کنٹریکٹ کے درست رویوں کو واضح طور پر بیان کرتی ہو اور کنٹریکٹ کے سسٹم کا ایک رسمی (ریاضیاتی) ماڈل تیار کرتی ہو۔ پھر ہم کنٹریکٹ کے ماڈل اور اس کی تخصیص کے درمیان مطابقت کی جانچ کرنے کے لیے ایک رسمی ثبوت کے طریقہ کار پر عمل کر سکتے ہیں۔

رسمی تصدیق کے ساتھ، اس بات کی تصدیق کرنے کا سوال کہ آیا کنٹریکٹ کی بزنس لاجک تقاضوں کو پورا کرتی ہے، ایک ریاضیاتی تجویز ہے جسے ثابت یا غلط ثابت کیا جا سکتا ہے۔ کسی تجویز کو رسمی طور پر ثابت کر کے، ہم محدود تعداد میں اقدامات کے ساتھ لامحدود تعداد میں ٹیسٹ کیسز کی تصدیق کر سکتے ہیں۔ اس طرح رسمی تصدیق میں یہ ثابت کرنے کے بہتر امکانات ہیں کہ ایک کنٹریکٹ تخصیص کے حوالے سے عملی طور پر درست ہے۔

#### مثالی تصدیق کے اہداف {#ideal-verification-targets}

تصدیق کا ہدف اس سسٹم کو بیان کرتا ہے جس کی رسمی تصدیق کی جانی ہے۔ رسمی تصدیق کا بہترین استعمال "ایمبیڈڈ سسٹمز" (سافٹ ویئر کے چھوٹے، سادہ ٹکڑے جو کسی بڑے سسٹم کا حصہ بنتے ہیں) میں ہوتا ہے۔ وہ ان مخصوص ڈومینز کے لیے بھی مثالی ہیں جن کے چند اصول ہوتے ہیں، کیونکہ اس سے ڈومین کے لحاظ سے مخصوص خصوصیات کی تصدیق کے لیے ٹولز میں ترمیم کرنا آسان ہو جاتا ہے۔

سمارٹ کنٹریکٹس—کم از کم، کچھ حد تک—دونوں تقاضوں کو پورا کرتے ہیں۔ مثال کے طور پر، ایتھیریم کنٹریکٹس کا چھوٹا سائز انہیں رسمی تصدیق کے قابل بناتا ہے۔ اسی طرح، <span dir="ltr">EVM</span> سادہ اصولوں کی پیروی کرتی ہے، جو <span dir="ltr">EVM</span> میں چلنے والے پروگراموں کے لیے معنوی خصوصیات کی وضاحت اور تصدیق کو آسان بناتا ہے۔

### تیز تر ڈیولپمنٹ سائیکل {#faster-development-cycle}

رسمی تصدیق کی تکنیکیں، جیسے کہ ماڈل چیکنگ اور علامتی نفاذ، عام طور پر سمارٹ کنٹریکٹ کوڈ کے باقاعدہ تجزیے (جو ٹیسٹنگ یا آڈیٹنگ کے دوران کیا جاتا ہے) سے زیادہ موثر ہوتی ہیں۔ اس کی وجہ یہ ہے کہ رسمی تصدیق دعووں کو جانچنے کے لیے علامتی اقدار پر انحصار کرتی ہے ("کیا ہوگا اگر کوئی صارف _<span dir="ltr">n</span>_ ایتھر نکالنے کی کوشش کرے؟") ٹیسٹنگ کے برعکس جو ٹھوس اقدار کا استعمال کرتی ہے ("کیا ہوگا اگر کوئی صارف <span dir="ltr">5</span> ایتھر نکالنے کی کوشش کرے؟")۔

علامتی ان پٹ متغیرات ٹھوس اقدار کی متعدد کلاسوں کا احاطہ کر سکتے ہیں، اس لیے رسمی تصدیق کے طریقے کم وقت میں زیادہ کوڈ کوریج کا وعدہ کرتے ہیں۔ جب مؤثر طریقے سے استعمال کیا جائے، تو رسمی تصدیق ڈیولپرز کے لیے ڈیولپمنٹ سائیکل کو تیز کر سکتی ہے۔

رسمی تصدیق مہنگی ڈیزائن کی غلطیوں کو کم کر کے غیر مرکزی ایپلی کیشنز (<span dir="ltr">dapps</span>) بنانے کے عمل کو بھی بہتر بناتی ہے۔ کمزوریوں کو دور کرنے کے لیے کنٹریکٹس کو اپ گریڈ کرنے (جہاں ممکن ہو) کے لیے کوڈ بیسز کو وسیع پیمانے پر دوبارہ لکھنے اور ڈیولپمنٹ پر زیادہ کوشش صرف کرنے کی ضرورت ہوتی ہے۔ رسمی تصدیق کنٹریکٹ کے نفاذ میں بہت سی ایسی غلطیوں کا پتہ لگا سکتی ہے جو ٹیسٹرز اور آڈیٹرز کی نظروں سے بچ سکتی ہیں اور کنٹریکٹ کی تعیناتی سے پہلے ان مسائل کو حل کرنے کا کافی موقع فراہم کرتی ہے۔

## رسمی تصدیق کی خامیاں {#drawbacks-of-formal-verification}

### دستی مشقت کی لاگت {#cost-of-manual-labor}

رسمی تصدیق، خاص طور پر نیم خودکار تصدیق جس میں ایک انسان درستگی کے ثبوت اخذ کرنے کے لیے ثابت کنندہ کی رہنمائی کرتا ہے، کافی دستی مشقت کی ضرورت ہوتی ہے۔ مزید برآں، رسمی تخصیص بنانا ایک پیچیدہ سرگرمی ہے جس کے لیے اعلیٰ سطح کی مہارت درکار ہوتی ہے۔

یہ عوامل (کوشش اور مہارت) کنٹریکٹس میں درستگی کا اندازہ لگانے کے معمول کے طریقوں، جیسے کہ ٹیسٹنگ اور آڈٹ کے مقابلے میں رسمی تصدیق کو زیادہ مشکل اور مہنگا بناتے ہیں۔ اس کے باوجود، سمارٹ کنٹریکٹ کے نفاذ میں غلطیوں کی لاگت کو دیکھتے ہوئے، مکمل تصدیقی آڈٹ کی لاگت ادا کرنا عملی ہے۔

### غلط منفی (False negatives) {#false-negatives}

رسمی تصدیق صرف یہ جانچ سکتی ہے کہ آیا سمارٹ کنٹریکٹ کا نفاذ رسمی تخصیص سے میل کھاتا ہے۔ اس طرح، یہ یقینی بنانا ضروری ہے کہ تخصیص سمارٹ کنٹریکٹ کے متوقع رویوں کو مناسب طریقے سے بیان کرے۔

اگر تخصیصات ناقص طور پر لکھی گئی ہیں، تو خصوصیات کی خلاف ورزیوں—جو کمزور نفاذ کی طرف اشارہ کرتی ہیں—کا رسمی تصدیقی آڈٹ کے ذریعے پتہ نہیں لگایا جا سکتا۔ اس صورت میں، ایک ڈیولپر غلطی سے یہ فرض کر سکتا ہے کہ کنٹریکٹ بگ فری ہے۔

### کارکردگی کے مسائل {#performance-issues}

رسمی تصدیق کو کارکردگی کے متعدد مسائل کا سامنا کرنا پڑتا ہے۔ مثال کے طور پر، بالترتیب ماڈل چیکنگ اور علامتی چیکنگ کے دوران پیش آنے والے اسٹیٹ اور پاتھ ایکسپلوژن کے مسائل تصدیق کے طریقہ کار کو متاثر کر سکتے ہیں۔ اس کے علاوہ، رسمی تصدیق کے ٹولز اکثر اپنی بنیادی تہہ میں <span dir="ltr">SMT</span> حل کنندگان اور دیگر کنسٹرینٹ حل کنندگان کا استعمال کرتے ہیں، اور یہ حل کنندگان کمپیوٹیشنل طور پر انتہائی گہرے طریقہ کار پر انحصار کرتے ہیں۔

اس کے علاوہ، پروگرام کی تصدیق کرنے والوں کے لیے ہمیشہ یہ تعین کرنا ممکن نہیں ہوتا کہ آیا کوئی خصوصیت (جسے منطقی فارمولے کے طور پر بیان کیا گیا ہے) پوری کی جا سکتی ہے یا نہیں ("[فیصلہ پذیری کا مسئلہ](https://en.wikipedia.org/wiki/Decision_problem)") کیونکہ ہو سکتا ہے کہ کوئی پروگرام کبھی ختم نہ ہو۔ اس طرح، کسی کنٹریکٹ کے لیے کچھ خصوصیات کو ثابت کرنا ناممکن ہو سکتا ہے یہاں تک کہ اگر اس کی اچھی طرح سے تخصیص کی گئی ہو۔

## ایتھیریم سمارٹ کنٹریکٹس کے لیے رسمی تصدیق کے ٹولز {#formal-verification-tools}

### رسمی تخصیصات بنانے کے لیے تخصیص کی زبانیں {#specification-languages}

**<span dir="ltr">Act</span>**: _*<span dir="ltr">Act</span> اسٹوریج اپ ڈیٹس، پری/پوسٹ کنڈیشنز اور کنٹریکٹ <span dir="ltr">invariants</span> کی تخصیص کی اجازت دیتا ہے۔ اس کے ٹول سویٹ میں پروف بیک اینڈز بھی ہیں جو <span dir="ltr">Coq</span>، <span dir="ltr">SMT</span> حل کنندگان، یا <span dir="ltr">hevm</span> کے ذریعے بہت سی خصوصیات کو ثابت کرنے کے قابل ہیں۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/ethereum/act)
- [دستاویزات](https://github.com/argotorg/act)

**<span dir="ltr">Scribble</span>** - _*<span dir="ltr">Scribble</span> تخصیص کی زبان میں کوڈ تشریحات کو ٹھوس دعووں میں تبدیل کرتا ہے جو تخصیص کی جانچ کرتے ہیں۔*_

- [دستاویزات](https://docs.scribble.codes/)

**<span dir="ltr">Dafny</span>** - _*<span dir="ltr">Dafny</span> ایک تصدیق کے لیے تیار پروگرامنگ زبان ہے جو کوڈ کی درستگی کے بارے میں استدلال کرنے اور ثابت کرنے کے لیے اعلیٰ سطحی تشریحات پر انحصار کرتی ہے۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/dafny-lang/dafny)

### درستگی کی جانچ کے لیے پروگرام کی تصدیق کرنے والے {#program-verifiers}

**<span dir="ltr">Certora Prover</span>** - _<span dir="ltr">Certora Prover</span> سمارٹ کنٹریکٹس میں کوڈ کی درستگی کی جانچ کے لیے ایک خودکار رسمی تصدیق کا ٹول ہے۔ تخصیصات <span dir="ltr">CVL</span> (<span dir="ltr">Certora Verification Language</span>) میں لکھی جاتی ہیں، جس میں جامد تجزیہ اور کنسٹرینٹ سالونگ کے امتزاج کا استعمال کرتے ہوئے خصوصیت کی خلاف ورزیوں کا پتہ لگایا جاتا ہے۔_

- [ویب سائٹ](https://www.certora.com/)
- [دستاویزات](https://docs.certora.com/en/latest/index.html)

**<span dir="ltr">Solidity SMTChecker</span>** - _*<span dir="ltr">Solidity</span> کا <span dir="ltr">SMTChecker</span> ایک بلٹ ان ماڈل چیکر ہے جو <span dir="ltr">SMT</span> (<span dir="ltr">Satisfiability Modulo Theories</span>) اور <span dir="ltr">Horn</span> سالونگ پر مبنی ہے۔ یہ اس بات کی تصدیق کرتا ہے کہ آیا کنٹریکٹ کا سورس کوڈ تالیف کے دوران تخصیصات سے میل کھاتا ہے اور حفاظتی خصوصیات کی خلاف ورزیوں کی جامد طور پر جانچ کرتا ہے۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/ethereum/solidity)

**<span dir="ltr">solc-verify</span>** - _*<span dir="ltr">solc-verify</span> <span dir="ltr">Solidity</span> کمپائلر کا ایک توسیعی ورژن ہے جو تشریحات اور ماڈیولر پروگرام کی تصدیق کا استعمال کرتے ہوئے <span dir="ltr">Solidity</span> کوڈ پر خودکار رسمی تصدیق انجام دے سکتا ہے۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/SRI-CSL/solidity)

**<span dir="ltr">KEVM</span>** - _*<span dir="ltr">KEVM</span> <span dir="ltr">K</span> فریم ورک میں لکھی گئی ایتھیریم ورچوئل مشین (<span dir="ltr">EVM</span>) کی ایک رسمی سیمینٹکس ہے۔ <span dir="ltr">KEVM</span> قابل عمل ہے اور ریچ ایبلٹی لاجک کا استعمال کرتے ہوئے خصوصیت سے متعلق کچھ دعووں کو ثابت کر سکتا ہے۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/runtimeverification/evm-semantics)
- [دستاویزات](https://jellopaper.org/)

### تھیورم پرونگ کے لیے منطقی فریم ورکس {#theorem-provers}

**<span dir="ltr">Isabelle</span>** - _<span dir="ltr">Isabelle/HOL</span> ایک پروف اسسٹنٹ ہے جو ریاضیاتی فارمولوں کو رسمی زبان میں ظاہر کرنے کی اجازت دیتا ہے اور ان فارمولوں کو ثابت کرنے کے لیے ٹولز فراہم کرتا ہے۔ اس کا بنیادی اطلاق ریاضیاتی ثبوتوں کو رسمی شکل دینا اور خاص طور پر رسمی تصدیق ہے، جس میں کمپیوٹر ہارڈویئر یا سافٹ ویئر کی درستگی کو ثابت کرنا اور کمپیوٹر زبانوں اور پروٹوکولز کی خصوصیات کو ثابت کرنا شامل ہے۔_

- [<span dir="ltr">GitHub</span>](https://github.com/isabelle-prover)
- [دستاویزات](https://isabelle.in.tum.de/documentation.html)

**<span dir="ltr">Rocq</span>** - _<span dir="ltr">Rocq</span> ایک انٹرایکٹو تھیورم ثابت کنندہ ہے جو آپ کو تھیورمز کا استعمال کرتے ہوئے پروگراموں کی وضاحت کرنے اور انٹرایکٹو طور پر درستگی کے مشین سے چیک شدہ ثبوت تیار کرنے دیتا ہے۔_

- [<span dir="ltr">GitHub</span>](https://github.com/rocq-prover/rocq)
- [دستاویزات](https://rocq-prover.org/docs)

### سمارٹ کنٹریکٹس میں کمزور پیٹرنز کا پتہ لگانے کے لیے علامتی نفاذ پر مبنی ٹولز {#symbolic-execution-tools}

**مینٹیکور** - _*علامتی نفاذ پر مبنی <span dir="ltr">EVM</span> بائٹ کوڈ کے تجزیے کا ایک ٹول*۔_

- [<span dir="ltr">GitHub</span>](https://github.com/trailofbits/manticore)
- [دستاویزات](https://github.com/trailofbits/manticore/wiki)

**<span dir="ltr">hevm</span>** - _*<span dir="ltr">hevm</span> <span dir="ltr">EVM</span> بائٹ کوڈ کے لیے ایک علامتی نفاذ کا انجن اور مساوات چیکر ہے۔*_

- [<span dir="ltr">GitHub</span>](https://github.com/dapphub/dapptools/tree/master/src/hevm)

**<span dir="ltr">Mythril</span>** - _ایتھیریم سمارٹ کنٹریکٹس میں کمزوریوں کا پتہ لگانے کے لیے ایک علامتی نفاذ کا ٹول_

- [<span dir="ltr">GitHub</span>](https://github.com/ConsenSysDiligence/mythril)
- [دستاویزات](https://github.com/ConsenSysDiligence/mythril/tree/develop/docs/source)

## مزید مطالعہ {#further-reading}

- [سمارٹ کنٹریکٹس کی رسمی تصدیق کیسے کام کرتی ہے](https://runtimeverification.com/blog/how-formal-verification-of-smart-contracts-works/)
- [ایتھیریم ایکو سسٹم میں رسمی تصدیق کے پروجیکٹس کا ایک جائزہ](https://github.com/leonardoalt/ethereum_formal_verification_overview)
- [ایتھیریم <span dir="ltr">2.0</span> ڈپازٹ سمارٹ کنٹریکٹ کی اینڈ ٹو اینڈ رسمی تصدیق](https://runtimeverification.com/blog/end-to-end-formal-verification-of-ethereum-2-0-deposit-smart-contract/)
- [دنیا کے مقبول ترین سمارٹ کنٹریکٹ کی رسمی تصدیق](https://www.zellic.io/blog/formal-verification-weth)
- [<span dir="ltr">SMTChecker</span> اور رسمی تصدیق](https://docs.soliditylang.org/en/v0.8.15/smtchecker.html)