Z3 не удается найти удовлетворяющее назначение для простой формулы с кванторами и шаблонами

В настоящее время я пишу автоматический верификатор для моего языка программирования поверх Z3 как забавный проект, и я пытаюсь использовать его, чтобы доказать, что реализация Фибоначчи с использованием цикла эквивалентна реализации с рекурсией.

Кажется, что это работает, если входная программа правильна, то есть она генерирует разумный вход для Z3, и Z3 говорит, что она неудовлетворительна, что означает в моем контексте, что программа правильна. Но когда я изменил одну переменную инициализации и тем самым рендерить неверная программа, Мой верификатор придумал следующую формулу Z3, которая мне не кажется слишком сложной, но Z3 говорит "неизвестно".

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
   (! (= (fib n)
         (ite (= n 0) 0
            (ite (= n 1) 1
               (+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
      :pattern ((fib n)))))
(assert (forall ((n Int))
   (! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)
Обратите внимание, что два квантора представляют собой рекурсивное определение Фибоначчи. Один мой друг рассказал мне об этом трюке, чтобы избежать совпадающего цикла: вместо определения fib как рекурсивной функции я ввожу другую функцию fakeFib, для которой я не даю определения, и я использую ее в рекурсивном определении fib. Кроме того, я говорю: верификатор, что они равны, но этот квантификатор получает только шаблон для fib, а не для fakeFib. Из-за ограничительных паттернов он является неполным, то есть он может доказать правильность программы только до тех пор, пока достаточно взглянуть на один уровень рекурсии, чтобы доказать это (но он может быть легко расширен до k уровней). Но я могу жить с этим ограничением, чтобы избежать совпадающих петель.

"ошибка" кода заключалась в том, что я неправильно инициализировал переменную, и это в конечном итоге привело к неверный компонент (= 1 (fib 0)) в последнем утверждении. Для правильной программы это будет (= 0 (fib 0)).

Некоторые наблюдения:

  • если я заменю (= 1 (fib 0)) на (= 0 (fib 0)), то Z3 сразу же обнаружит, что она неудовлетворительна.
  • раньше у меня не было опций (set-option :smt.auto-config false) и (set-option :smt.mbqi false), а затем у меня закончилась память на моей машине и закончилось время на rise4fun.
  • установка (set-option :smt.macro-finder true), которая, кажется, сработала для людей с подобными вопросами, не сработала для меня. Я догадываюсь что это вызвано тем, что у меня есть два квантора для fib, а не только один.
  • я попытался использовать cvc4 в качестве сравнения, и он сразу же сказал "неизвестно". Так что мои проблемы не кажутся специфичными для Z3.
  • Формула явно неразрешимой. (= 1 (fib 0)) является false, поэтому все последнее утверждение автоматически истинно. (>= n 0) также легко удовлетворить.
1 2
formal-verification

1 ответ:

Я не специалист по Z3, но, возможно, смогу пролить немного света.

Отключая MBQI, вы отключаете способность Z3 создавать модели для количественных формул, поэтому я предполагаю, что когда Z3 не может найти способ доказать, что ваша проблема неудовлетворительна, он быстро сообщает об этом как unknown.

Обратите внимание, что модель для вашей задачи должна удовлетворяться четырьмя утверждениями, а не только двумя последними. Как вы указываете, Z3 не может устранить ваше первое утверждение, как если бы это был макрос, потому что вы приведите два определения для fib n.

Если вы включите MBQI, вы увидите, что Z3 пытается найти модель и потребляет на нее довольно много памяти! Я предполагаю, что это потому, что единственный способ удовлетворить вашу спецификацию требует построения рекурсивной функции fib, функции, которую Z3 не поддерживает.

Как я буду подходить к этому

То, что вы делаете прямо сейчас, это хороший трюк, который позволяет Z3 расширить определение fib настолько, насколько это необходимо для доказательства проблема unsat. Но это не очень хорошо работает с моделью finder, потому что вы косвенно вводите рекурсивное определение.

Итак, если Z3 сообщает unsat, то вы знаете, что ваша программа верна. Если он сообщает unknown, вы должны запустить итерационный процесс. Перед этим вы удаляете второе утверждение (= (fib n) (fakeFib n)), чтобы предотвратить бесконечный цикл построения модели.

  1. в каждой итерации вы обеспечиваете k-разложение fib, где fib(k+1) абстрагируется в терминах fakeFib. Вы можете оставьте fakeFib n неограниченным, или вы можете наложить на него легкие ограничения (например, должно быть положительное целое число), не добавляя рекурсии.
  2. Если Z3 сообщает unsat, то ваша программа верна.
  3. Если Z3 сообщает sat, Необходимо проверить, соответствует ли возвращенная модель fib. Если она последовательна, то вы получили контрпример. Если он не последователен,то вы увеличиваете k и переходите к шагу 1.

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

2