Формальная верификация кода на Coq: тактики

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