Данная статья является переводом моей статьи: 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 и настраиваются для решения конкретных задач. Во время работы над большим проектом, рекомендуется для разработанных тактик выделить отдельную библиотеку. Узко-специализированные тактики, которые используются только однажды, рекомендуется писать непосредственно над Леммой, в которой эти тактики используются (в том же файле, без вынесения их в библиотеку тактик).
