Доказательства сценариев с использованием тактики и метапрограммирования имеют давние традиции в интерактивных провайдерских теорем (ITP), начиная с Эдинбургского LCF Мильнера.
Эти свойства чистых программ задаются экспрессивной логикой более высокого порядка (и часто зависящей от типа), а доказательства выполняются с использованием различных обязательных языков программирования, начиная с языка ML.
Программные верификаторы, такие как Dafny, VCC, Why3 и Liquid Haskell, ориентированы как на чистые, так и на эффективные программы с побочными эффектами от расхождения до параллелизма, но обеспечивают относительно слабую логическую спецификацию (например, логику первого порядка с несколькими выбранными теориями, такими как линейная арифметика). Они работают главным образом путем вычисления условий верификации (VCs) из программ, обычно опираясь на аннотации, такие как предварительные и постусловия, и кодирования их в автоматические теоремопровайдеры (ATP), такие как решатели модулей удовлетворительности (SMT), что часто обеспечивает отличную автоматизацию.
Эти два подполя оказали влияние друг на друга, хотя ситуация несколько асимметрична. С одной стороны, большинство интерактивных провайдеров получили поддержку для использования SMT-растворителей или других ATP, обеспечивающих автоматизацию определенных типов утверждений. С другой стороны, признавая важность интерактивных пробных оттисков, объясняя, почему интерфейсы с ITP, такими как Coq. Однако, работа над доказательством в переводе с английского языка Why3 требуется, чтобы пользователи были знакомы не только с обеими системами, но и с особенностями перевода.
И кроме Why3 и инструментов, основанных на нем, ни один другой программный верификатор на базе SMT не имеет полноценной поддержки интерактивной тестации, что приводит к нескольким недостаткам:
-Пределы экспрессивности. Выразительность программных верификаторов может быть ограничена используемым протоколом ATP. При работе с теориями, которые не поддаются определению и трудно автоматизации (нелинейная арифметика или логика разделения), доказательства в системах на базе ATP могут стать невозможными или, в лучшем случае, чрезвычайно утомительными.
-Бойлер. Чтобы обойти эту проблему с отсутствием автоматизации, программистам приходится вручную создавать подробные пробные оттиски, часто повторяя утомительные, но подверженные ошибкам шаги, чтобы дать подсказки основному решающему устройству, и найти доказательства. И наоборот, ИТП с метапрограммированием преуспели в автоматизации выражения специфических для домена данных, чтобы выполнить такие утомительные проверки.
-Неявный контекст доказательства. В большинстве программных верификаторов логический контекст доказательства неявно присутствует в тексте программы и зависит от потока управления и предварительных постусловий предыдущих вычислений. В отличие от интерактивных помощников, программисты не имеют прямого доступа, ни визуального, ни программного, к этому контексту, что крайне затрудняет структурирование и исследование доказательств.
В ответ на эти недостатки ищется система, которая успешно сочетает в себе удобство автоматического программного верификатора для обычного случая. И плавно переходящая к интерактивному испытательному опыту для тех частей доказательства, которые трудно автоматизировать. Для этого предлагается Meta-F ⋆, тактику и структуру метапрограммирования для программного верификатора F ⋆.
Основные моменты и вклад Meta-F ⋆
F ⋆ исторически более глубоко укоренился как программный верификатор на базе SMT. До сих пор F ⋆ выпускал VC исключительно с помощью SMT-решения, обеспечивая хорошую автоматизацию для многих общих задач проверки программы, но также демонстрируя недостатки, описанные выше.
Meta-F ⋆ - это платформа, позволяющая пользователям F ⋆ манипулировать виртуальными валютами с помощью тактики. В более общем плане, он поддерживает метапрограммирование, позволяя программистам писать сценарии построения программ, манипулируя их синтаксисом и настраивая способ проверки типа. Это позволяет программистам реализовать специальные процедуры для манипулирования виртуальными валютами; устранить шаблон в цветопробах и программах; визуально осмотреть состояние цветопробы и программно манипулировать им, устраняя недостатки, описанные выше.
SMT по-прежнему играет центральную роль в Meta-F ⋆: типичное использование включает реализацию тактики трансформации виртуальных валют, чтобы превратить их в теории, хорошо поддерживаемые SMT, без необходимости (пере)внедрения полных процедур принятия решений. Кроме того, универсальность Meta-F ⋆ позволяет полностью реализовать нетривиальные расширения языка в виде библиотек метапрограммирования, без изменений в системе проверки типа F ⋆.
Технический вклад работы включает в себя следующее:
"Мета-" - это просто эффект. Meta-F ⋆ реализуется с помощью системы расширяемых эффектов F ⋆, которая обеспечивает надлежащую изоляцию программ и метапрограмм. Являясь первоклассными программами F ⋆, метапрограммы печатаются, звонят по стоимости, прямые, функциональные программы более высокого порядка, как и оригинальные программы ML. Кроме того, метапрограммы могут быть проверены и запрограммированы самостоятельно.
Согласование тактики с генерацией виртуальных валют.
В программных верификаторах программист часто направляет растворителя к доказательствам, предоставляя промежуточные утверждения. Meta-F ⋆ сохраняет этот стиль, но дополнительно позволяет решать задачи тактикой. С этой целью, вклад этой работы заключается в извлечении из виртуальной валюты доказательства, охватывающего все соответствующие гипотезы, включая те, которые подразумеваются в тексте программы.
Эффективное выполнение метапрограмм.
Метапрограммы выполняются во время проверки типа. В качестве исходных данных их можно интерпретировать с помощью существующей (но медленной) абстрактной машины F ⋆ для нормализации термина, или более быстрого нормализатора, основанного на нормализации путем оценки (NbE). Для гораздо более высокой скорости выполнения метапрограммы можно запускать и на родном языке. Это достигается за счет сочетания существующего механизма извлечения файлов F ⋆ в OCaml с новой структурой для безопасного расширения проверки типа F ⋆ с помощью такого родного кода.
Примеры и оценка.
Оцениваем Meta-F ⋆ по нескольким тематическим исследованиям.
Во-первых, представляем доказательства функциональной корректности кода аутентификации сообщений Poly1305, используя новую комбинацию доказательств путем отражения для работы с нелинейной арифметикой и SMT-решения для линейной арифметики. Измеряем явный выигрыш в доказательной прочности. Только SMT-доказательства успешны лишь в редких случаях (при разумных таймаутах), в то время как тактика + SMT-доказательство лаконично, никогда не подводит, и работает быстрее.
Во -вторых, демонстрируя улучшение выразительности, разработав небольшую библиотеку для проверки программ-манипуляторов в логике разделения кучи, которая ранее была недоступна для F ⋆. Наконец, иллюстрируем возможность автоматического построения проверенных эффективных программ, представив библиотеку для метапрограммирования проверенных низкоуровневых парсеров и сериализаторов с приложениями для сетевого программирования, где проверка ускоряется за счет обработки виртуальной валюты с помощью тактики и программной настройки SMT контекста.
Вывод напрашивается такой, что тактика и метапрограммирование могут успешно сочетаться с генерацией виртуальных валют и решением SMT для построения проверенных программ с лучшей, масштабируемой и более надежной автоматизацией.
Ключевой проблемой в верификации программы является обеспечение баланса между автоматизацией и выразительностью. В то время как ITP, основанные на тактике, поддерживают высокоэкспрессивную логику, автор тактики отвечает за всю автоматизацию. И наоборот, программные верификаторы на базе SMT обеспечивают хорошую масштабируемую автоматизацию для сравнительно слабой логики, но при сбое верификации предоставляют мало возможностей. Конструкция, позволяющая подобрать правильный инструмент, с гранулярностью каждой верификационной подзадачи, является достойной областью исследования. Meta-F ⋆ представляет собой новую точку в этом пространстве: используя рукописную тактику наряду с SMT-автоматизацией, получили письменные доказательства, которые ранее были непрактичны в F ⋆, и в других SMT-верификаторах программ.