Loading...
السلسلة: التحقق الشكلي · الجزء 3 من 3 الجمهور: المبتدئون. يقدّم الجزءان 1 و2 التحقق الشكلي وخطأ Orchard؛ وتُظهر هذه الخاتمة التقاء الفكرتين في نظام حقيقي. سنستعيد كل ما نحتاجه أثناء التقدم. ما ستخرج به: فهم دقيق لما أثبته Zcash فعليًا بشأن تجمّعه الجديد "Ironwood"، وكيف يُنظّم البرهان، وما الذي يغطيه وما الذي لا يغطيه، وكيف أُوقف التجمّع القديم بأمان، ولماذا يشير ذلك إلى معيار جديد لبناء المال التشفيري.
في الجزء 1 تعلّمنا ما معنى أن نثبت صحة نظام. وفي الجزء 2 رأينا خللًا حقيقيًا فات الاختبارات لأربع سنوات: ضربًا غير مقيّد بما يكفي على منحنى إهليلجي كان يمكن أن يسمح بتزوير غير محدود وغير مرئي. هذه المقالة هي الحل: كيف استجاب Zcash ليس بمجرد رقعة، بل ببرهان متحقق منه آليًا يثبت زوال فئة الخطأ بأكملها.
عندما يهدد خطأٌ المال، تكون الاستجابة المعتادة هي إصلاحه والمضي قدمًا. فعل Zcash شيئًا أكثر طموحًا. فإلى جانب تجمّع محمي جديد يسمى Ironwood، فُعّل في 28 يوليو 2026، نشر مهندسوه برهانًا رياضيًا متحققًا منه آليًا، يضم أكثر من 2,700 مبرهنة مكتوبة في مساعد البرهان Lean، يثبت أن التجمّع الجديد لا يمكنه إنشاء عملات مزيفة ضمن افتراضاته المعلنة. البرهان علني، في مستودع ironwood مفتوح المصدر، واستغرق إتمامه من ثلاثة فرق من الباحثين وعلماء التشفير أكثر من شهر بكثير.
تتجاوز أهمية ذلك Zcash. فهو أحد أوضح العروض الواقعية لإمكانية أخذ نظام مالي حي، وكتابة معنى "عدم وجود تزوير" بدقة، ثم إثباته، بدل الأمل بأن تكون اختباراتك شاملة. إنه يحوّل الوعد إلى مبرهنة.
انتهى الجزء 2 إلى الفكرة التي جعلت ذلك ممكنًا. استعدها، لأن كل ما هنا يقوم عليها:
لا يمكن أن يوجد خطأ تزوير غير قابل للاكتشاف إلا في مواصفة البروتوكول، أي الوصف الرياضي لما يجب أن تفرضه الدائرة. فأي شيء قابل للاكتشاف سيظهر في المحاسبة العامة. لذا فإن إثبات سلامة المواصفة يلغي فئة أخطاء التزوير الخفي بأكملها دفعة واحدة.
لماذا "فقط في المواصفة"؟ لأن كل كتلة تسجل بصورة دائمة المحتويات الكاملة لكل معاملة، بما في ذلك براهينها. لو أن البرنامج قبل معاملة سيئة على نحو خاطئ، لاستطاع أي شخص إعادة تشغيل السجل التاريخي عبر برنامج مصحح ورؤيتها. ذلك الدليل دائم وعلني. أما العيب في الرياضيات الكامنة وحده فيستطيع الاختباء إلى الأبد، إذ لا توجد "نسخة صحيحة" لإعادة التشغيل مقابلها. وهذا هو العيب الذي يستهدفه التحقق الشكلي.
الاختبار يفحص السلوك على مدخلات مأخوذة كعينات، وقد اختفى خطأ Orchard تحديدًا لأن أي مدخل مأخوذ كعينة لم يصبه. أما البرهان المتعلق بالمواصفة فيغطي كل المدخلات في آن واحد، بما فيها الحالات الطرفية التي لن يفكر أحد في تجربتها. وذلك هو النوع الوحيد من الضمان القوي بما يكفي لإحالة عيب غير مرئي عمره أربع سنوات إلى التقاعد بثقة.
يثبت البرهان خاصية رئيسية واحدة، مبنية على خاصية أعمق تحتها.
سلامة الرصيد: لا تتجاوز القيمة المخفية المخزنة في التجمّع المحمي صافي القيمة العامة التي تدفقت إليه.
هذه هي خاصية مكافحة التزوير بصيغة بسيطة. يمكن للمال أن يدخل التجمّع المحمي (بصورة مرئية علنًا) وأن يخرج منه (بصورة مرئية علنًا)، لكن لا يمكن استحضار قيمة من العدم في الداخل حيث تكون المبالغ مخفية. لنجعل ذلك ملموسًا بدفتر أستاذ صغير (حساب متحقق منه):
5 + 3 = 8 تنتج مخرجات قيمتها 4 + 4 = 8. القيمة الداخلة تساوي القيمة الخارجة. تتحقق سلامة الرصيد. ✓8، لكن بمخرجات قدرها 4 + 4 + 2 = 10. سيؤدي ذلك إلى سك 2 وحدة من العدم. تمنع سلامة الرصيد ذلك: لا يجوز للتجمّع أن يدفع أكثر مما دخله. ✗سلامة الرصيد هي البيان الرياضي الذي يفيد بأن السيناريو الثاني لا يمكنه أبدًا إنتاج معاملة صالحة.
لضمان سلامة الرصيد، كان على الباحثين أولًا إثبات خاصية أعمق وأكثر دقة بشأن نظام برهان المعرفة الصفرية نفسه. اتضح أن السلامة العادية (عبارة الجزء 2: "للتصريحات الصحيحة فقط شاهد") لا تكفي لتجمّع محمي، لسبب شيق: إذ إن المعاملة المخفية قد تحتوي على أي شيء، ولذلك فإن كل تصريح تقريبًا له شاهد من الناحية التقنية. لذا أثبت الباحثون خاصية أقوى:
سلامة المعرفة: أي شخص يستطيع إنتاج برهان معاملة صالح يجب أن يمتلك فعليًا شاهدًا صالحًا، أي عملات حقيقية، مشتقة بصورة صحيحة، عند العنوان الصحيح.
الأداة الشكلية لذلك هي مستخرج: إجراء يمكنه، إذا أُعطي أي مُثبت يستطيع إقناع المتحقق، أن يستخرج الشاهد الفعلي منه. وإذا أمكن دائمًا استخراج شاهد، فلا بد أن المُثبت المقنع كان يملكه حقًا. بلغة الجزء 2، سلامة المعرفة هي الوعد الشكلي بأنه لا توجد فجوة سلامة، ولا قيد مفقود يسمح لتصريح زائف بالمرور. وهي الخاصية نفسها التي كان غيابها خطأ Orchard. وإثبات وجودها، لكل المُثبتين الممكنين، هو ما يغلق ذلك الباب بإحكام.
كان التحقق جهدًا بشريًا جادًا، لا نتيجة زر واحد:
ironwood.للاستدلال على الخاصية، يصف نموذج Lean دفتر أستاذ كاملًا بوصفه قائمة من المعاملات، تحمل كل منها إجراءاتها وقيمتها العامة المعلنة وتوقيعاتها. وتنقل مسندة يسميها الباحثون ValidLedger قواعد إجماع الشبكة مباشرة: يجب أن يحقق شاهد كل إجراء الشروط المطلوبة، ولا يجوز أن تظهر أي علامة إنفاق (nullifier) مرتين، ويجب أن تكون كل حالة شجرة مشار إليها حالة وصل إليها النظام بالفعل، كما يجب أن يتحقق كل توقيع. ثم تكمّم المبرهنات على كل دفتر أستاذ صالح. وتلك العبارة، "كل دفتر أستاذ صالح"، هي المغزى كله: ليست عينة، بل جميعها، وهي مجموعة فائقة لأي شيء قد يتمكن مهاجم حقيقي من تجميعه.
تُركّب نتيجة سلامة الرصيد من عدة مبرهنات على مستوى دفتر الأستاذ، تثبت كل منها أن مسارًا للتزوير مغلق: أن كل إنفاق يقابل مخرجًا حقيقيًا سابقًا، وأن إجمالي القيمة محفوظ، وأن المذكرة المستلمة تبقى قابلة للإنفاق ولا يمكن سرقتها، وأن الإنفاق يتطلب تفويضًا صحيحًا. وتربط قطعة منفصلة، هي توقيع الربط، القيم المخفية لكل معاملة بالمبلغ العام الذي تعلنه، حتى لا تختلف المحاسبة المخفية والعامة بصمت.
سؤال دقيق وصادق: البرهان يتعلق بنموذج رياضي، لكن الشبكة تشغّل شيفرة Rust. فكيف نعرف أن الشيفرة تطابق النموذج؟
رسم الفريق حدًا دقيقًا يسمونه بصمة المتحقق. فوق الحد، تستدل براهين Lean على المتحقق بوصفه كائنًا رياضيًا دقيقًا. وتحته يقع تنفيذ Rust العادي. والحجة الأساسية هي ذاتها من الجزء 2:
أي طريقة يمكن أن تنحرف بها البرمجيات الحقيقية عن النموذج المثبت ستكون خطأ تنفيذ، وأخطاء التنفيذ لا يمكنها إلا أن تنتج تزويرًا قابلًا للاكتشاف، لأن كل برهان مقبول يُسجل بصورة دائمة ويمكن إعادة تشغيله عبر برمجيات مصححة.
لذلك يعالج البرهان الفئة غير القابلة للاكتشاف (المواصفة)، ويعالج السجل العام الدائم الفئة القابلة للاكتشاف (التنفيذ). وبينهما، لا مكان يختبئ فيه خطأ تزوير غير قابل للاكتشاف. كما أجرى الفريق تحققًا متقاطعًا بتشغيل المتحقق الحقيقي وتأكيد أنه يعيد إنتاج البصمة تمامًا في الحالات الملتقطة.
أصر الجزء 1 على أن البرهان يضمن أن النظام يفي بالمواصفة ضمن الافتراضات المعلنة، ولا يعني أبدًا "لا أخطاء على الإطلاق". وكان فريق Zcash دقيقًا على نحو محمود بشأن ذلك تمامًا، وينبغي للكتابة التعليمية الصادقة أن تكون كذلك.
يختزل البرهان أمان Ironwood إلى مجموعة صغيرة من الافتراضات القياسية المسماة بوضوح. وعلى وجه الخصوص، تستند سلامته إلى صعوبة مسألة اللوغاريتم المتقطع على المنحنى الإهليلجي الذي يستخدمه Ironwood (وهو افتراض مدروس جيدًا، حيث يتطلب أفضل هجوم معروف ما يقارب 2^126 عملية، أي ما يتجاوز بكثير أي حوسبة قابلة للتنفيذ)، إلى جانب افتراضات نمذجة قياسية لدالة التجزئة. ويجدر توضيح حدين:
بعيدًا عن تقويض الإنجاز، فإن تسمية هذه الحدود هي ما يجعله جديرًا بالثقة. الادعاء دقيق: ضمن افتراضات تشفيرية قياسية، لا يستطيع هذا التجمّع إنشاء عملات مزيفة غير قابلة للاكتشاف. إنها مبرهنة، وليست أمنية، ونطاقها الدقيق معلن بصراحة.
لا يزال إثبات سلامة التجمّع الجديد يترك سؤالًا: ماذا عن تجمّع Orchard القديم، حيث عاش العيب لأربع سنوات؟ لا يمكنك كشف ماضيه. لكن يمكنك تقييد مستقبله.
قدّم Zcash آلية تسمى البوابة الدوارة. والقاعدة بسيطة وقوية:
لا يجوز أن تخرج قيمة من التجمّع القديم إلا بقدر القيمة التي دخلته بشكل قابل للتحقق.
لأن الأموال التي تنتقل إلى تجمّع محمي وخارجه مرئية علنًا (وحده النشاط داخل التجمّع مخفي)، تسمح البوابة الدوارة للشبكة كلها بالتحقق من عدم خروج أكثر مما دخل على الإطلاق. ولو أُنشئت عملات مزيفة داخل التجمّع القديم، فستصطدم بهذا الحد وتعجز عن الخروج. ومع انتقال الأموال الصادقة إلى الخارج وعدم ظهور فائض، يكتسب المجتمع دليلًا عامًا قويًا على أن العيب لم يُستغل قط. إنها أقرب ما يكون إلى تدقيق معروض تجمّع خاص من دون كسر خصوصيته، وتقرب سلامة المعروض من النموذج الشفاف لسلسلة مثل Bitcoin مع الحفاظ على خصوصية Zcash.
يعيد Ironwood نفسه استخدام دائرة البرهان المصححة، ويبدأ من جديد بتجمّع فارغ، ويضيف حمايات استشرافية (بما فيها ترتيبات تتيح بقاء الأموال قابلة للاسترداد إذا هددت حواسيب الكم المستقبلية تشفير اليوم). يتدفق النشاط المحمي الجديد الآن عبر Ironwood، بينما يقتصر تجمّع Orchard القديم على عمليات السحب.
Ironwood جزء من تحول أوسع في طريقة بناء Zcash. ويجري تطوير جهده لتوسيع الجيل التالي (بنية تسمى Tachyon، مبنية على البراهين التكرارية ومجموعة أدوات تسمى Ragu) وفق فلسفة تسمى أحيانًا التشفير عالي الضمان: أي التعامل مع التحقق الشكلي المتحقق منه آليًا لا بوصفه فكرة لاحقة، بل جزءًا قياسيًا من إطلاق أنظمة تشفيرية جديدة.
المنطق مقنع. فالتشفير المتطور هو تحديدًا المجال الذي يكون فيه الحدس البشري أضعف، وحيث يمكن لحالة طرفية دقيقة غير مختبرة أن تختبئ لسنوات، كما أظهر Orchard. وإثبات المواصفة هو التقنية الوحيدة التي تتسع لـ"كل المدخلات الممكنة" وتغلق هذه الفجوات بالتصميم. وقد أشار الفريق إلى نيته توسيع هذا التدقيق مع الوقت، نحو التنفيذ وما بعده. توقّع اعتماد هذا المعيار على نطاق أوسع، داخل Zcash وخارجه.
بسّطنا بغرض الوضوح. فتنفيذ Lean الحقيقي أكثر تفصيلًا بكثير من الرسم التخطيطي هنا، مع تعريفات دقيقة للإجراءات والتصريحات والالتزامات وnullifiers والتوقيعات؛ و"سلامة الرصيد" و"سلامة المعرفة" لهما تعريفات شكلية دقيقة لم نذكرها إلا بالكلمات؛ والاختزال إلى صعوبة اللوغاريتم المتقطع يمر عبر عدة نماذج وسيطة (نموذج جبري للمُثبت ونموذج oracle عشوائي لدالة التجزئة) ضغطناها في عبارة "افتراضات قياسية"؛ ووصفنا البصمة والبوابة الدوارة على مستوى مفاهيمي. لا يغير أي من ذلك القصة الجوهرية: مواصفة لـ"عدم التزوير"، وبرهان متحقق منه آليًا على كل دفاتر الأستاذ الصالحة، وبيان صريح وصادق للنطاق والافتراضات، وإحالة آمنة للتجمّع المعيب إلى التقاعد. وللحساب المرجعي، راجع تقارير التحقق المنشورة لـProject Tachyon ومستودع برهان ironwood.
| المصطلح | المعنى بلغة بسيطة |
|---|---|
| Ironwood | تجمّع Zcash المحمي الجديد (2026)، الذي يستبدل تجمّع Orchard المعيب |
| Balance integrity | لا يدفع التجمّع أبدًا قيمة أكبر مما دخله علنًا |
| Knowledge soundness | يتطلب البرهان الصالح أن يحمل المُثبت شاهدًا حقيقيًا |
| Extractor | إجراء يسحب الشاهد من أي مُثبت مقنع |
| Lean | مساعد البرهان المستخدم للتحقق الآلي من عملية التحقق |
| ValidLedger | النموذج الشكلي لقواعد الإجماع الذي تستدل عليه المبرهنات |
| Fingerprint | الحد الفاصل بين الرياضيات المثبتة وبرمجيات Rust العاملة |
| Under stated assumptions | ينطبق البرهان بشرط صحة الافتراضات التشفيرية المسماة |
| Turnstile | قاعدة تحدّ مخارج التجمّع عند ودائعه القابلة للتحقق |
| High-assurance cryptography | بناء التشفير مع التحقق الشكلي كخطوة قياسية |
هل يعني البرهان أن Ironwood خالٍ من الأخطاء؟ لا، ولا يدّعي ذلك. إنه يثبت خاصية دقيقة واحدة، هي سلامة الرصيد، ضمن الافتراضات المعلنة. وهذا يستبعد التزوير غير القابل للاكتشاف، لا كل خطأ يمكن تصوره.
هل يضمن البرهان أن معاملاتي خاصة؟ لا. يغطي التحقق سلامة المعروض (عدم وجود مال مزيف)، لا ضمانات الخصوصية المنفصلة للتجمّع. وهذه تُبرهن بطرق مختلفة.
لماذا نثق ببرهان كتبه البشر (والذكاء الاصطناعي)؟ لأنه متحقق منه آليًا. يتحقق مساعد البرهان Lean من كل خطوة ميكانيكيًا، لذا تستند الثقة إلى المواصفة والافتراضات المسماة، لا إلى عناية أي إنسان أو ذكاء اصطناعي في كل خطوة.
ماذا يحدث للعملات التي لا تزال في تجمّع Orchard القديم؟ يمكن سحبها، ولكن فقط حتى المبلغ الذي دخل بصورة قابلة للتحقق، كما تفرضه البوابة الدوارة. ويحمي هذا سلامة المعروض ويساعد كذلك على إظهار أن العيب القديم لم يُستغل قط.
هل هذه نهاية القصة؟ إنها محطة بارزة، لا خط نهاية. فبنية Zcash المستقبلية (Tachyon، مع مجموعة أدوات Ragu) تُبنى مع التحقق الشكلي بوصفه ممارسة قياسية، لتوسيع هذا النهج أكثر.
يدعي شخص: "بما أن Ironwood متحقق منه شكليًا، أصبح من المستحيل الآن أن يحدث أي خطأ على الإطلاق في Zcash." باستخدام أفكار الأجزاء الثلاثة، اذكر سببين مختلفين يجعلان هذا الادعاء أقوى مما ينبغي. (الإجابة أدناه.)
أولًا، يغطي البرهان خاصية محددة (سلامة الرصيد) ضمن افتراضات معلنة (صعوبة اللوغاريتم المتقطع ونمذجة التجزئة القياسية). فإذا انكسر افتراض تشفيري، أو ظهرت مشكلة خارج ما حُدد في المواصفة (مثلًا في الخصوصية، أو في برمجيات المحفظة، أو في مكوّن غير مثبت)، فلا يقول البرهان شيئًا عنها. ثانيًا، يضمن التحقق الشكلي أن النظام يفي بالمواصفة التي كُتبت؛ فإذا أخفقت تلك المواصفة نفسها في التقاط متطلب حقيقي ما، فسيشهد البرهان بأمانة لصحة الشيء الخطأ. والنقطتان معًا تعيدان صياغة تحفظ الجزء 1: البرهان دقيق ومحدود، وقوي تحديدًا لأن نطاقه صادق، لا لأنه ضمان شامل بأن شيئًا لن يخطئ أبدًا.
عبر ثلاثة أجزاء انتقلنا من فكرة عامة إلى تطبيق حي: ما معنى إثبات صحة البرمجيات بدل اختبارها (الجزء 1)، وكيف كان يمكن لدائرة حقيقية غير مقيّدة بما يكفي أن تسك مالًا غير مرئي (الجزء 2)، وكيف أحال برهان متحقق منه آليًا لـسلامة الرصيد تلك الفئة من الأخطاء إلى التقاعد نهائيًا (الجزء 3). والخيط الناظم هو وعد واحد صادق: ليس "لا أخطاء على الإطلاق"، بل "هذه الخاصية الدقيقة تنطبق في كل حالة، ضمن الافتراضات المعلنة." وبالنسبة إلى المال الذي يخفي مبالغه الخاصة، فهذا الوعد هو بالضبط ما يستحق الإثبات.
جزء من سلسلة التحقق الشكلي لـZecHub.