Статья предполагает, что читатель имеет опыт работы с интерактивным программным средством доказательства теорем — Coq.
Статья является адаптированной русскоязычной версией моей статьи, написанной во время работы над формальной верификацией протокола криптовалюты Tezos.
В данной статье мы рассмотрим прием, который используется для работы с рекурсивными функциями, которые не проходят проверку завершаемости (тотальности) в Coq. Под «горючим» мы будем понимать натуральное число, которое вводится как дополнительный параметр в тело функции, чтобы обозначить верхнюю границу числа итераций, которые функция может совершить. Таким образом функция трансформируется в завершаемую, удобную для работы, и радушно принимаемую компилятором Coq. В литературе термин встречается под названиями: petrol, fuel, gas и т.д.
Положим, перед нами стоит задача: необходимо верифицировать функцию, написанную на каком-либо языке программирования. Мы разбираемся в том, что делает эта функция, уже прикидываем, какие леммы сформулируем, чтобы доказать, что она ведет себя именно так как ожидается. Переводим функцию на Coq (вручную, или с помощью автоматических переводчиков, если только таковые имеются для требуемого языка), и видим, что проверка Coq на завершаемость нашей функции (termination 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)]нужно избавляться. План действий следующий:
написать симуляцию нашей функции (ее точную копию) которая будет отличаться от оригинала тем, что в нее будет добавлен новый аргумент, так называемое горючее fuel. Это натуральное число, которое будет уменьшаться на каждом шаге итерации.
сказать Коку, что именно по этому аргументу компилятор должен судить, завершается ли функция: {struct fuel}
уменьшать на каждом шаге итерации fuel (на единицу, например) в теле функции
доказать, что для всех возможных входных параметров, результат работы функции-симуляции с горючим будет равен результату исходной функции
работать с завершаемой симуляцией, а не с исходной функцией.
К пункту 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…В теле функции мы первым делом добавляем проверку, не равно ли горючее нулю, и, если равно — выходим из цикла, если нет — продолжаем работу. Уменьшаем в теле функции горючее на единицу, и проверка на завершаемость (termination check) проходит успешно. Таким образом нам удается избавиться от #[bypass_check(guard)], теперь мы можем работать с симуляцией.
Заключение
Одной из задач формальной верификации рекурсивных функций является доказательство завершаемости. Если проверка на завершаемость компилятором Coq провалилась, чтобы скомпилировать функцию можно сделать одно из трех действий:
1. поставить над функцией флаг #[bypass_check(guard)],но тогда останется недоказанной завершаемость этой функции. Кроме того, возможны проблемы с доказательствами свойств таких функций.
2. прямо указать компилятору какой параметр в теле функции рекурсивно уменьшается на каждом шаге итерации {struct param}.
Иногда на практике, если функция очень большая (например, около 3х тысяч строк кода), можно попробовать по очереди вставить в {struct ..} все входные параметры, получаемые функцией. Это лайфхак, но он не всегда срабатывает. Обычно приходится анализировать исходный код функции, чтобы найти параметр, который является для функции проверкой на завершение (он может также и увеличиваться, и условием завершения будет достижение параметром заданного порога).
if stack_depth >i 10000 then
Error_monad.error_valueВвести в функцию дополнительный параметр, горючее — натуральное число, и в теле функции:
a) если параметр равен нулю — осуществлять прерывание работы функции;
б) уменьшать параметр на каждом шаге итерации.
Приведенный в статье способ решения проблемы проверки завершаемости функций довольно трудоемкий. Но в то же самое время, это, наверное, наиболее простой способ из имеющихся.
