Данная статья является переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml.
Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и формальной логики.
Статья предназначена для круга читателей, имеющих опыт работы с Coq.
Часто процесс формальной верификации становится утомительным и монотонным из за повторяющихся действий, которые пруф-инженеру (от английского слова proof - доказательство) приходится выполнять. К счастью, в Coq есть инструменты и техники автоматизации доказательств, которые позволяют не только значительно увеличить производительность, но и сделать доказательства короче.
В данной статье мы покажем, как использовать и писать тактики на примере формальной верификации исходного кода криптовалюты Tezos (написанной на OCaml), а именно, мы затронем следующие темы:
презентация некоторых функций Ltac (язык для написания тактик, встроенный в Coq),
рекурсивный поиск доказательств
встроенные тактики Coq
создание собственных тактик
Ltac (язык для написания тактик, встроенный в Coq)
Ltac позволяет писать тактики, которые можно использовать в доказательствах лемм и теорем.
Рассмотрим лемму:
Lemma unparse_ty_parse_ty (loc_value : Alpha_context.Script.location)
(ctxt : Alpha_context.context)
(ty : Script_typed_ir.ty)
(legacy allow_lazy_storage allow_operation allow_contract
allow_ticket : bool) :
match (unparse_ty loc_value ctxt ty) with
| Pervasives.Ok (mich_node, ctxt1) =>
match parse_ty ctxt1 legacy allow_lazy_storage allow_operation
allow_contract allow_ticket mich_node with
| Pervasives.Ok ((Ex_ty ty1), ctxt1) => ty = ty1
| Pervasives.Error _ => True
end
| Pervasives.Error _ => True
end.В этой лемме мы доказываем совместимость двух функций: unparse_ty и parse_ty. Рассмотрим лемму детально. Один из параметров — это тип ty. Это довольно громоздкий тип, содержащий 32 конструктора. Чтобы доказать нашу лемму, нам необходимо доказать ее для каждого из конструкторов ty. Итого, разбивая ty командой destruct, мы имеем к доказательству 32 под-цели.
Некоторые из конструкторов типа ty очень похожи между собой, а именно, это 12 конструкторов, принимающих лишь один аргумент ty_metadata:
| Unit_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty
| Int_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty
| Nat_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty
...Все 12 под-целей могут быть решены очень похожими блоками кода (хотя, для каждого конструктора эти блоки кода будут разниться).
С тем, чтобы автоматизировать решение всех 12 под-целей, мы создаем тактику destr_if и вызываем ее в теле нашего доказательства.
Что мы получаем:
код становится значительно короче
код становится читаемым
мы избегаем повторений в теле доказательства леммы
Ниже приведена тактика destr_if, написанная на Ltac:
Ltac destr_if :=
match goal with
| |- match (let? ' _ := Alpha_context.Gas.consume _ _ in _) with _ => _ end =>
destruct Alpha_context.Gas.consume; [ simpl in * | simpl; trivial]
| |- match (if ?cond then _ else _) with _ => _ end =>
destruct cond; simpl; auto
| |- match (let? ' _ := Script_ir_annot.check_type_annot _ _ in _) with _ =>
_ end => destruct Script_ir_annot.check_type_annot;
[ simpl in * | simpl; trivial]
| |- ?a _ = ?b => unfold b; subst; reflexivity
end.Рекурсивный поиск доказательств
Итак, наша тактика может решить 12 целей. Нам нужно вызвать ее 12 раз? Вовсе нет. В доказательстве леммы мы вызываем ее лишь однажды. Рассмотрим приведенный ниже кусочек кода, который автоматически решает все 12 под-целей.
Proof.
intro H.
destruct ty eqn:TY; simpl;
repeat destr_if.Здесь мы использовали комбинатор тактик repeat. Приведенный выше код (комбинация тактик) пройдет циклом по всем под-целям, пытаясь применить тактики из списка к каждой вновь-сгенерированной цели (заходя, также, и в под-под-цели и т.д., пытаясь их решить с помощью списка тактик). Условие перехода на следующий шаг цикла - это ситуация, когда тактика не может продвинуться в решении очередной цели. При работе с комбинатором repeat следует соблюдать осторожность: если запустить его в купе с тактиками, которые срабатывают всегда, вам, скорее всего, придется перезагружать компьютер. Тактика auto, например, срабатывает всегда (даже если ее применение ничего не меняет). Запуск этой тактики в цикле приведет к проблемам.
Встроенные тактики
Мы можем улучшить нашу тактику destr_if, дополнив ее тактиками, встроенными в систему Coq. В цикле, когда одна из применяемых тактик не срабатывает на каком-либо узле дерева под-целей, к текущей цели автоматически применяется следующая тактика из заданного нами списка, и так далее.
Вот несколько полезных тактик, встроенных в Coq, комбинациями которых можно дополнить собственные тактики или использовать в доказательствах отдельно: lia, nia, intuition, trivial, congruence, ring и т.д.
Иногда для решения конкретных задач, на языке Ltac, программистами на Coq разрабатываются тактики, которые могут давать ощущение, что любая цель в доказательстве может быть решена с их помощью автоматически. И хоть чувство это обманчиво, программисты любят давать своим тактикам говорящие названия: hammer, crush, best…
Заключение
Тактики в Coq — это функции, которые автоматически ищут доказательства и широко применяются в формальной верификации. Мы можем использовать встроенные «родные» тактики Coq, или писать собственные, если нам нужен более высокий уровень автоматизации. Тактики пишутся на встроенном языке Ltac и настраиваются для решения конкретных задач. Во время работы над большим проектом, рекомендуется для разработанных тактик выделить отдельную библиотеку. Узко-специализированные тактики, которые используются только однажды, рекомендуется писать непосредственно над Леммой, в которой эти тактики используются (в том же файле, без вынесения их в библиотеку тактик).
