Creusot 0.14.0: مواصفات الترتيب الجزئي، شروط التحقق للقطات وتصفح rust-analyzer

الترتيب الجزئي

Creusot 0.14.0 هو إصدار من أداة التحقق الشكلي للغة Rust. تذكر ملاحظات الإصدار أن الترتيب الجزئي جزء صغير من ميزات جديدة؛ والباقي في changelog الكامل.

في السابق كانت مواصفات PartialOrd تقيدها بالترتيب الكامل. منذ 0.13.0 تخفف هذا القيد للسماح أيضًا بالترتيب الجزئي. trait الترتيب الكامل السابق OrdLogic كان يعتمد على cmp_log، النظير المنطقي لـ cmp الذي يعيد Ordering. وهذا فرض كمًّا صارمًا: يجب مقارنة أي عنصرين كـ Less أو Equal أو Greater.

trait الجزئي الصارم الجديد PartialOrdLogic يعتمد بدلًا من ذلك على lt_log، دالة المقارنة المنطقية، مع قوانين الانعكاس والتعدي. أصبح الكمّ الكامل قانونًا منفصلًا في OrdLogic باسم lt_log_total، يضمن self < other || self == other || other < self. يقول المطورون إن لا إثباتًا موجودًا تضرر، وإن التحقق الآلي تعامل مع التغيير.

شروط التحقق للقطات

يولّد Creusot الآن شروط تحقق للقطات: تعبيرات منطقية مضمّنة في برامج Rust. هذا يحسّن استخدام lemma، أي أسلوب مشابه لأدوات التحقق من Creusot.

يمكن كتابة lemma كدالة منطقية بمتطلبات requires وشروط ensures، أي أن hyp(x) تستلزم concl(x) لكل x. استدعاؤها داخل snapshot! يتحول الآن إلى تأكيد أن hyp(n) صحيحة، وافتراض أن concl(n) صحيحة عند وسيط n المحدد. ولا يفرض هذا تطبيق مُكمِّم كلي.

تقارن الملاحظات ذلك باستدعاء lemma إجرائية عادية. الأسلوب القديم أيضًا يستخدم requires وensures، لكنه يحتاج استدعاء دالة Rust ويجب أن يجتاز borrow checker، مما قد يتطلب boilerplate إذا كان الهدف مجرد تسجيل حقائق. تُحذف القطات، لذا توجد للإثبات الشكلي فقط. لم تُولَّد شروط التحقق لـ snapshot! سابقًا لأنها لم تكن ضرورية للصحة، لكنها تساعد على اكتشاف أخطاء المواصفات مبكرًا، مثل الفهرسة خارج الحدود، وتتيح تقنيات جديدة.

دعم rust-analyzer

يعمل Go to definition الآن في مواصفات Pearlite. لتمكين ذلك تم توسيع ماكرو المواصفات requires وensures وproof_assert! وsnapshot! من أجل rust-analyzer بدلًا من حذفها في التجميع العادي. يمرر Creusot معلمات الدليل إلى rust-analyzer للخيارات المطلوبة.

لا يُقصد بكود Pearlite الموسّع أن يعمل مع rustc، لأنه يتجاوز مدقق الأنواع ولا يتجاوز borrow checker. لم تكن هذه مشكلة لأن rust-analyzer لا ينفّذ borrow checking. بقيت مشكلة أن رموز ماكرو Pearlite كانت ذات spans خشنة جدًا: في المثال يتوسع a + b إلى AddLogic::add_logic(a, b)، ويحصل كل رمز مولّد على span كامل للتعبير. لذلك كان Go to definition يبحث عن التعريفات من أي نقطة داخل التعبير من أجل creusot_std وlogic وops وAddLogic وadd_logic.

يعطي الإصلاح span لعلامة + في add_logic، والمعرّفات الأخرى span بعرض صفري يتجاهله rust-analyzer. تُنسب هذه التوضيحات إلى Sara Kiniones. ويقول المطورون إن التنقل داخل مواصفات Creusot أصبح أكثر متعة بكثير.

الأسئلة

يمكن لمن لديه أسئلة عن Creusot الانضمام إلى قناة Zulip للمشروع، أو فتح نقاش أو issue في مستودع Creusot.

المصادر: Lobsters