Кто-нибудь пробовал доказывать Z3 с самим Z3?

Question

Кто-нибудь пробовал доказывать Z3 с самим Z3?

Можно ли даже доказать, что Z3 является правильным, используя Z3?

Более теоретически, возможно ли доказать, что инструмент X является правильным, используя сам X?

Answer 1

Краткий ответ: "Нет, никто не пытался доказать Z3, используя сам Z3":-)

Предложение "мы доказали правильность программы X" очень вводит в заблуждение. Основная проблема: что значит быть правильным. В случае Z3 можно сказать, что Z3 является правильным, если, по крайней мере, он никогда не возвращает "sat" для неудовлетворительной задачи и "unsat" для удовлетворительной. Это определение может быть улучшено за счет включения дополнительных свойств, таких как: Z3 не должен падать; функция X в API Z3 имеет свойство Y и т. д.

После того, как мы договоримся о том, что мы должны доказать, нам нужно создать модели среды выполнения, семантики языка программирования (C++ в случае Z3) и т. Д. Затем инструмент (он же верификатор) используется для преобразования фактического кода в набор формул, которые мы должны проверить с помощью средства доказательства теорем, такого как Z3. Нам нужен верификатор, потому что Z3 не "понимает" C++. Verifying C Compiler ( VCC) является примером такого рода инструмента. Обратите внимание, что доказательство правильности Z3 с использованием этого подхода не дает однозначной гарантии того, что Z3 действительно является правильным, поскольку наши модели могут быть неверными, верификатор может быть неправильным, Z3 может быть неправильным и т. Д.

Чтобы использовать верификаторы, такие как VCC, нам нужно аннотировать программу свойствами, которые мы хотим проверить, зацикливать инварианты и т. Д. Некоторые аннотации используются для указания того, что должны делать фрагменты кода. Другие аннотации используются для "помощи / руководства" в доказательстве теоремы. В некоторых случаях количество аннотаций превышает проверяемую программу. Итак, процесс не полностью автоматический.

Другая проблема - это стоимость, процесс будет очень дорогим. Это будет гораздо больше времени, чем реализация Z3. Z3 имеет 300 тыс. Строк кода, часть этого кода основана на очень тонких алгоритмах и хитростях реализации. Еще одной проблемой является техническое обслуживание, мы регулярно добавляем новые функции и улучшаем производительность. Эти модификации повлияют на доказательство.

Хотя стоимость может быть очень высокой, VCC использовался для проверки нетривиальных фрагментов кода, таких как гипервизор Microsoft Hyper-V.

Теоретически, любой верификатор для языка программирования X может быть использован для подтверждения себя, если он также реализован на языке X. Верификатор SpeC# является примером такого инструмента. SpeC# реализован в SpeC#, и несколько частей SpeC# были проверены с использованием SpeC#. Обратите внимание, что SpeC# использует Z3 и предполагает, что это правильно. Конечно, это большое предположение.

Вы можете найти более подробную информацию об этих проблемах и приложениях Z3 на бумаге: http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf

Answer 2

Нет, невозможно доказать, что нетривиальный инструмент является правильным, используя сам инструмент. Это было в основном заявлено во второй теореме Гёделя о неполноте:

Для любой формально эффективно сгенерированной теории T, включающей в себя основные арифметические истины, а также определенные истины о формальной доказуемости, если T включает в себя утверждение своей собственной непротиворечивости, то T не согласуется.

Поскольку Z3 включает в себя арифметику, он не может доказать свою последовательность.

Поскольку это было упомянуто в комментарии выше: даже если пользователь предоставляет инварианты, теорема Гедельса все еще применяется. Это не вопрос вычислимости. Теорема утверждает, что в последовательной системе такого доказательства не может быть.

Однако вы можете проверить части Z3 с Z3.

Редактировать через 5 лет:

На самом деле аргумент проще, чем теорема Гёделя о неполноте.

Допустим, Z3 верен, если он возвращает UNSAT только для неудовлетворительных формул.

Предположим, мы находим формулу A, такую, что если A неудовлетворительно, то Z3 является правильным (и мы каким-то образом доказали это соотношение).

Мы можем дать эту формулу Z3, но

1. если Z3 возвращает UNSAT, это может быть из-за правильности Z3 или из-за ошибки в Z3. Так что мы ничего не проверяли.
2. если Z3 возвращает SAT и контрмодель, мы могли бы найти ошибку в Z3, проанализировав модель
3. в противном случае мы ничего не знаем.

Таким образом, мы можем использовать Z3, чтобы находить ошибки в Z3 и повышать достоверность Z3 (до чрезвычайно высокого уровня), но не для формальной проверки этого.