برهانك الأول

عشر دقائق · ثلاث خطوات · لا شيء عليك أن تأخذه على الثقة

هذا مسار المبتدئين. لست بحاجة إلى أن تكون مبرمجًا، ولا إلى حساب، ولا إلى أن تخبرنا بوجودك. وفي نهايته يكون حاسوبك أنت — لا حاسوبنا، ولا كلمتنا وحدها — قد تحقق من الرياضيات وراء قاعدة حقيقية من المكتبة.

إن كنت تعرف طريقك في التعامل مع أداة إثبات بالفعل، فإن الجولة الكاملة تذهب أبعد: بناء الواجهة والتحقق من كل صف في جدول حقيقتها. تتوقف هذه الصفحة عند البرهان، وهو الجزء الأهم والجزء الذي لا يحتاج إلى أي تثبيت.

ما أنت على وشك التحقق منه

تُسمّى القاعدة سياسة brief-fill. وهي تقرر متى يجوز للمساعد أن يجيب نيابة عن صاحبه بدلًا من سؤاله. تُطرَح أربعة ادّعاءات عنها، وجميعها على وشك أن تُختبَر على جهازك:

هذه ليست وعودًا في تدوينة. إنها نظريات، وأداة إثبات على وشك أن تحاول كسرها.

الخطوة 1 — احصل على أداة الإثبات

github.com/alire-project/GNAT-FSF-builds/releases

خذ ملف gnatprove الخاص بجهازك — -x86_64-linux، أو -darwin لجهاز ماك، أو -windows64. فُكّه في أي مكان. لا يوجد مُثبِّت، ولا يدخل شيء إلى نظامك، ولا يعمل شيء في الخلفية. احذف المجلد عند الانتهاء وكأن شيئًا لم يكن.

إنها مجانية وليست ملكنا — تأتي من مجتمع Ada، لا منا. هذه هي الفكرة: الشيء الذي يتحقق من عملنا يجب ألا يكون شيئًا سلّمناه نحن لك.

الخطوة 2 — احصل على القاعدة

brief-fill-policy.tar.gz (6,918 بايت)

sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

فُكّه. بداخله الشيفرة المصدرية، والبرهان، ووصف بإنجليزية بسيطة لما تفعله القاعدة.

يمكنك تجاهل مجموع التحقق في أول مرة — فبرهان الخطوة 3 لا يعتمد عليه. إنه موجود لوقت تريد فيه أن تتأكد من أن الملف الذي تلقيته هو الملف الذي نشرناه، وأنه الملف نفسه الذي يسمّيه الكتالوج.

الخطوة 3 — اطلب من حاسوبك أن يتحقق منها

افتح طرفية في المجلد الذي فككته، وشغّل سطرين:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

انتظر. حين تنتهي، ابحث عن هاتين الكلمتين:

0 unproved

هذا كل شيء. هذا هو التمرين بأكمله. لا شيء آخر يحتاج إلى تثبيت، وهذه الخطوة تعمل على جهاز عادي لا يحمل شيئًا آخر عليه — فأداة الإثبات التي نزّلتها تحمل كل ما يحتاجه البرهان.

ما الذي حدث للتو

أخذ حاسوبك الادّعاءات الأربعة أعلاه، وحاول أن يجد حالة يفشل فيها أي منها، فلم يستطع — لأنه لا توجد واحدة. ليس “اختبرناه وبدا سليمًا”. وليس “القائم على الصيانة يقول ذلك”. آلة لا يمكن إقناعها بالكلام ذهبت تبحث عن مثال مضاد وعادت خالية الوفاض.

لم تثق بنا لنخبرك بذلك. شاهدته يحدث على عتاد تملكه أنت.

اختياري — اكسرها عمدًا

هذا هو الجزء الذي يستحق فعله إن كان لديك خمس دقائق أخرى، لأن التحقق الذي لا يقول إلا “نعم” لا يساوي كثيرًا.

افتح brief_fill_policy_pkg.ads في أي محرر نصوص، وغيّر القاعدة بحيث يسمح مخزن مفقود بمرور إجابة رغم ذلك. شغّل الأمر نفسه مرة أخرى. سترفض — وستسمّي بالضبط النظرية التي كسرتها للتو.

ذلك الرفض هو نموذج الأمان بأكمله. لا يثبّت Ghillie شيئًا لا يجتاز هذا، فما فعلته للتو بيدك هو ما يفعله هو نيابة عنك في كل مرة.

ما لا يُثبته هذا

نفضّل أن نقول لك هذا على أن تكتشفه بنفسك لاحقًا. تغطي البراهين قواعد القرار — من يجوز له رؤية ماذا، وما الذي يجوز أن يغادر، وما الذي يجب أن تجتازه أي إرسالية. لا تجعل هذه البراهين بقية البرمجية سحرًا، ولا ندّعي ذلك. هذه الصراحة هي الاتفاق، وهي الاتفاق كله.

إلى أين تذهب بعد ذلك

إن لم تنجح، فتلك نتيجة ونودّ أن نسمع بها. الرفض الذي لا يمكنك تفسيره أكثر إثارة لاهتمامنا من النجاح.