Creusot 0.14.0: часткові порядки, умови верифікації snapshot і навігація 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 замість того, щоб видалятися під час звичайної компіляції. Creusot передає параметри guide в rust-analyzer для потрібних опцій.

Розширений код 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