Проверка рекурсивных функций в Coq. Проблема с выключением. Топливо

В статье предполагается, что читатель имеет опыт работы с интерактивным инструментом доказательства теорем Coq.

Статья представляет собой адаптированную русскоязычную версию. мой постнаписано во время работы над формальная проверка протокола криптовалюты Tezos.

В этой статье мы рассмотрим прием, используемый для работы с рекурсивными функциями, не прошедшими проверку окончательности (тотальности) в Coq. Под «топливом» мы понимаем натуральное число, которое вводится в качестве дополнительного параметра в тело функции для указания верхней границы числа итераций, которое может выполнить функция. Это превращает функцию в финализируемую, простую в использовании и приветствуется компилятором Coq. В литературе термин встречается под названиями: бензин, топливо, газ и др.

Предположим, перед нами стоит задача проверки функции, написанной на языке программирования. Мы понимаем, что делает эта функция, мы уже думаем о леммах, которые собираемся сформулировать, чтобы доказать, что она ведет себя именно так, как ожидалось. Переводим функцию на Coq (вручную, либо с помощью машинных переводчиков, если они есть для нужного языка), и видим, что проверка завершения Coq для нашей функции (termition check) не удалась.

Это означает, что Coq не может определить, какой аргумент будет уменьшаться с каждым шагом итерации. Вы можете попробовать явно указать Coq на аргумент, который, как мы точно знаем, будет уменьшаться с каждым шагом. {struct уменьшаемый_аргумент}:

Fixpoint my_function 
  (a : A) (b : B) (legacy : bool) {struct a} : C := 
     func_body

Но если это не помогает и функция не может быть скомпилирована, мы вынуждены поставить флаг на функцию #[bypass_check(guard)].

Флажок #[bypass_check(guard)] может только раздражать инженера-доказательства. Это означает, что Coq не может доказать завершение функции. Это означает, что у нас нет гарантии, что программисты не ошиблись при написании этой функции. Возможно, что программа рухнет, даже если мы докажем некоторые свойства этой функции и скажем, что она проверена.

Примечание: мы сталкиваемся с проблемой остановки, описанной Аланом Тьюрингом: не существует универсального алгоритма для определения того, завершается ли конкретная программа. Проверка завершения в Coq консервативна. Это означает, что Coq принимает только функции определенного типа, о которых можно с уверенностью сказать, что эта функция выполнена. Другие функции не проходят тест на завершение, даже если такая функция действительно завершается. Для функций Fixpoint Coq требует, чтобы рекурсивные вызовы выполнялись только для параметров, которые синтаксически уменьшаются на каждый шаг итерации.

Из флажка #[bypass_check(guard)]нужно избавиться. План действий следующий:

1. написать симуляцию нашей функции (её точную копию), которая будет отличаться от оригинала тем, что в неё будет добавлен новый аргумент, так называемый мазут. Это натуральное число, которое будет уменьшаться с каждым шагом итерации.

2. скажите Kok, что это аргумент, по которому компилятор должен судить, завершается ли функция: {struct fuel}

3. уменьшать топливо с каждым шагом итерации (например, на единицу) в теле функции

4. доказать, что для всех возможных входных параметров результат функции моделирования с топливом будет равен результату исходной функции

5. работать с завершенной симуляцией, а не с исходной функцией.

По пункту 4:

Lemma func_eq_funcSym: forall n fuel:nat, func n = funcSym n fuel.

И хотя функция func всегда под флагом #[bypass_check(guard)], эту лемму можно доказать, если провести индукцию по fuel. Вероятно на fuel должны быть введены ограничения.

Возьмем пример из практики:

Ниже начало функции parse_ty. Функция взята из проекта “формальная проверка протокола криптовалюты Tezos.

Функция имеет аннотацию {struct node_value}, который должен указать компилятору Coq, какой из аргументов проверять на «уменьшение с каждым шагом итерации». Но такого рода Alpha_context.Script.node в исходном коде спроектирован таким образом, что Coq не может определить, что на каждом шаге рекурсии будет работать с прямым подтермом аргумента node_value (и в данном случае это действительно не всегда так).

#[bypass_check(guard)]
Fixpoint parse_ty 
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
  (allow_ticket : bool) (ret_value : parse_ty_ret)
  (node_value : Alpha_context.Script.node) {struct node_value}
  : M? (ret * Alpha_context.context) :=
  let parse_passable_ty_aux_with_ret {ret} := 'parse_passable_ty_aux_with_ret
    ret in
  let parse_any_ty_aux := 'parse_any_ty_aux in
  let parse_big_map_value_ty_aux := 'parse_big_map_value_ty_aux in...

Итак, мы хотим избавиться от #[bypass_check(guard)], завершить функцию. Создаем функцию моделирования parse_ty_symпутем добавления натурального числа fuel в качестве аргумента и изменив управление рекурсивным вызовом на {struct fuel}.

Fixpoint parse_ty_sym (fuel : nat)
  (ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
  (allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
  (allow_ticket : bool) {ret_value : parse_ty_ret}
  (node_value : Alpha_context.Script.node) {struct fuel}
  : M? (ret * Alpha_context.context) :=
  match fuel with
  | Datatypes.O =>
    Error_monad.error_value
      (Build_extensible "Typechecking_too_many_recursive_calls" unit tt)
  | Datatypes.S fuel => let parse_passable_ty_aux_with_ret {ret} := 'parse_passable_ty_aux_with_ret
    ret in
  let parse_any_ty_aux := 'parse_any_ty_aux in
  let parse_big_map_value_ty_aux := 'parse_big_map_value_ty_aux in…

В тело функции мы сначала добавляем проверку, равно ли топливо нулю, и если да, то выходим из цикла, иначе продолжаем работать. Уменьшаем топливо в теле функции на единицу и проверка на завершение проходит. Таким образом, нам удается избавиться от #[bypass_check(guard)]теперь мы можем работать с симуляцией.

Заключение

Одной из проблем формальной верификации рекурсивных функций является доказательство завершения. Если проверка завершения компилятором Coq не удалась, вы можете сделать одну из трех вещей, чтобы скомпилировать функцию:

1. поставить флаг на функцию #[bypass_check(guard)],но тогда конец этой функции останется недоказанным. Также могут возникнуть проблемы с доказательствами свойств таких функций.

2. напрямую сообщить компилятору, какой параметр в теле функции рекурсивно уменьшается на каждом шаге итерации {struct param}.

Иногда на практике, если функция очень большая (например, около 3000 строк кода), можно попробовать вставить по очереди в {struct..} все входные параметры, полученные функцией. Это хак, но он не всегда работает. Обычно вам нужно разобрать исходный код функции, чтобы найти параметр, который является тестом завершения для функции (он также может увеличиваться, и условием завершения будет достижение порога, указанного параметром).

if stack_depth >i 10000 then
    Error_monad.error_value

3. Введем в функцию дополнительный параметр, топливо — натуральное число, а в тело функции:

   а) если параметр равен нулю, прервать выполнение функции;

   б) уменьшать параметр на каждом шаге итерации.

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