Creusot 0.14.0: ნაწილობრივი წესრიგის სპეციფიკაციები, snapshot-ის VC-ები და rust-analyzer-ის ნავიგაცია

ნაწილობრივი წესრიგები

Creusot 0.14.0 არის Rust-ის ფორმალური ვერიფიკაციის ხელსაწყოს გამოშვება. გამოშვების შენიშვნებში ნათქვამია, რომ ნაწილობრივი წესრიგები ახალი ფუნქციების მცირე ნაწილია, დანარჩენი კი სრულ changelog-ში მოცემულია.

ადრინდელი ვერსიები PartialOrd-ის სპეციფიკაციას სრულ წესრიგებამდე ზღუდავდნენ. 0.13.0 ვერსიიდან ეს შეზღუდვა შეამსუბუქეს, რათა ნაწილობრივი წესრიგებიც დაშვებულიყო. წინა სრული წესრიგის ტრეიტი OrdLogic ეფუძნებოდა cmp_log-ს, cmp-ის ლოგიკურ ანალოგს, რომელიც Ordering-ს აბრუნებს. ეს სისრულეს იმპლიციტურად აქცევდა: ნებისმიერი ორი ელემენტი უნდა შედარებულიყო როგორც Less, Equal ან Greater.

ახალი მკაცრი ნაწილობრივი წესრიგის ტრეიტი PartialOrdLogic სამაგიეროდ ეფუძნება lt_log-ს, ლოგიკურ შედარების ფუნქციას, ირეფლექსიურობისა და ტრანზიტიულობის კანონებით. სისრულე ახლა ცალკე კანონია OrdLogic-ში, სახელად lt_log_total, რომელიც უზრუნველყოფს self < other || self == other || other < self. დეველოპერები აღნიშნავენ, რომ არსებული მტკიცებულებებიდან არცერთი არ დაზარალდა და ავტომატური პროვერები ცვლილებას გაუმკლავდნენ.

ვერიფიკაციის პირობები snapshot-ებისთვის

Creusot ახლა snapshot-ებისთვის ვერიფიკაციის პირობებს აგენერირებს, რომლებიც Rust-ის პროგრამებში ჩაშენებული ლოგიკური გამოსახულებებია. ეს აუმჯობესებს lemma ფუნქციების გამოყენებას, იდიომს Creusot-ის მსგავს ვერიფიკაციის ხელსაწყოებში.

lemma შეიძლება დაიწეროს ლოგიკურ ფუნქციად requires და ensures პირობებით, რაც ნიშნავს წინადადებას, რომ hyp(x) გულისხმობს concl(x)-ს ყველა x-ისთვის. ამ lemma-ს გამოძახება snapshot!-ში ახლა გარდაიქმნება ასერტად, რომ hyp(n) ჭეშმარიტია, და დაშვებად, რომ concl(n) ჭეშმარიტია, კონკრეტულ n არგუმენტზე სპეციალიზებულად. ეს პროვერებს არ აიძულებს უნივერსალური კვანტორის ინსტანცირებას.

შენიშვნები ამას ადარებს ჩვეულებრივი პროგრამული lemma-ს გამოძახებას. იმ ადრინდელ სტილსაც აქვს requires და ensures პირობები, მაგრამ ის ნერგავს Rust-ის ფუნქციის გამოძახებას და უნდა გაიაროს borrow checker-ი, რამაც შეიძლება boilerplate მოითხოვოს, როცა მიზანი მხოლოდ ფაქტების დაფიქსირებაა. snapshot-ები წაიშლება, ამიტომ ისინი მხოლოდ ფორმალური მტკიცებისთვის არსებობენ. snapshot!-ისთვის ვერიფიკაციის პირობები ადრე არ გენერირდებოდა, რადგან soundness-ისთვის საჭირო არ იყო, თუმცა ისინი ეხმარება სპეციფიკაციის შეცდომების უფრო ადრე აღმოჩენას, მაგალითად ინდექსირებას საზღვრებს გარეთ, და ახალი ტექნიკების საშუალებას იძლევა.

rust-analyzer-ის მხარდაჭერა

Go to definition ახლა მუშაობს Pearlite-ის სპეციფიკაციებში. ამის ჩასართავად, სპეციფიკაციის მაკროები, როგორებიცაა requires, ensures, proof_assert! და snapshot!, rust-analyzer-ისთვის გაფართოებულია, ნაცვლად იმისა, რომ ჩვეულებრივი კომპილაციისას წაიშალოს. აუცილებელი იყო rust-analyzer-ისთვის იმ ოპციების გადაცემა, რომლითაც ის ამ მაკროებს Creusot-ის მსგავსად აფართოებს (საჭირო პარამეტრები გიდშია აღწერილი).

გაფართოებული Pearlite კოდი rustc-ისთვის არ არის განკუთვნილი, რადგან ის ტიპების შემმოწმებელს გადის, მაგრამ borrow checker-ს არა. ეს პრობლემა არ ყოფილა, რადგან rust-analyzer borrow checking-ს არ ასრულებს. დარჩენილი პრობლემა ის იყო, რომ Pearlite მაკროებიდან მიღებულ ტოკენებს ზედმეტად უხეში span-ები ჰქონდათ. მაგალითში a + b ფართოვდება AddLogic::add_logic(a, b)-ად, და ყველა გენერირებულ ტოკენს მთელი გამოსახულების span ჰქონდა. შედეგად, Go to definition ამ გამოსახულების შიგნით ნებისმიერი ადგილიდან ეძებდა განმარტებებს creusot_std, logic, ops, AddLogic და add_logic-ისთვის.

შესწორება add_logic-ს +-ის span-ს აძლევს, ხოლო სხვა იდენტიფიკატორებს ნულოვანი სიგანის span-ს, რომელსაც rust-analyzer უგულებელყოფს. სარა კინიონესს მიაწერენ ამის გარკვევას. დეველოპერები ამბობენ, რომ შედეგად Creusot-ში სპეციფიკაციებში ნავიგაცია გაცილებით სასიამოვნოა.

კითხვები

მკითხველებს, რომლებსაც Creusot-ის შესახებ კითხვები აქვთ, შეუძლიათ შეუერთდნენ პროექტის Zulip არხს ან გახსნან დისკუსია ან issue-ს Creusot-ის რეპოზიტორიაში.

წყაროები: Lobsters