🦀 Как доказать, что Rust-код работает правильно: Amazon рассказывает о Verus

Rust предотвращает многие ошибки работы с памятью, но программа всё ещё может вернуть неверный результат. Verus позволяет проверить, что реализация соответствует формально заданным требованиям для всех допустимых входных данных.

Разработчик описывает прямо в исходниках:

* requires - условия перед выполнением функции.
* ensures — свойства результата.
* Инварианты циклов и вспомогательные доказательства.

Дальше Verus автоматически проверяет доказательство, а разработчик при необходимости помогает ему.

В статье есть показательный пример с бинарным поиском. Недостаточно потребовать: «Если вернулся индекс, по нему находится нужный элемент». Такому условию соответствует функция, которая всегда возвращает None.

Нужно добавить второе требование: если вернулся `None`, искомого элемента действительно нет в массиве.

Amazon уже использует Verus для проверки ключевых примитивов Nitro Isolation Engine, отвечающего за изоляцию виртуальных машин. Инструмент также позволяет доказывать свойства конкурентного кода и безопасность поддерживаемых конструкций unsafe.

Гарантии относятся к заданной спецификации и принятым допущениям: полнота самих требований остаётся ответственностью разработчика.

📖 https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

#Rust #Разработка #FormalVerification

🦀 Кто должен доказывать корректность реализации трейта в Rust: сама реализация или код, который её использует?

Нико Матсакис разобрал этот вопрос на примере циклических зависимостей, когда доказательство может замкнуться само на себя.

Допустим, есть трейт Magic: Copy. Любой тип с Magic обязан реализовывать Copy.

Два подхода:

• Модульный: проверяем обязательства при проверке impl. Поэтому impl Magic for String недопустим: String не реализует Copy.

• Внешний: разрешаем такой impl, но при его использовании требуем отдельно доказать String: Copy. Реализация есть, воспользоваться ей нельзя.

Второй вариант помогал обойти проблему циклических доказательств. Но упирался в unsafe-трейты.

Когда автор пишет unsafe impl, остальной код доверяет его гарантиям. Если реализация ошибочно обещает, что Box<T> может содержать нулевой указатель, ответственность лежит на ней.

Выходит странная модель: гарантии безопасности у impl принимаем, а выполнение требований супертрейтов заставляем перепроверять вызывающий код.

Вывод Нико: реализация должна сама устанавливать выполнение своего контракта. Следующая часть будет о том, как совместить этот подход с циклами.

https://smallcultfollowing.com/babysteps/blog/2026/10/10/modular-vs-external-proofs/

#Rust