Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMT

При дедуктивной верификации Си-программ как с помощью различных платформ верификации (Why3, Frama-C/WP, F*), так и с помощью систем интерактивного доказательства теорем (Isabelle, HOL4, Coq) достаточно широко используются SMT-решатели. Их разрешающие алгоритмы полны для некоторых комбинаций логических теорий (логик), в частности для логики QF_UFLIA. В то же время при верификации Си-программ часто необходимо оперировать формулами в других разрешимых логиках, поддерживаемых не всеми SMT-решателями. Типичными примерами таких логик могут служить комбинации QF_UFLIA c теориями ограниченных целых как с переполнением (для беззнаковых целых в Си), так и без переполнения (для знаковых целых), а также теорией конечных интерпретируемых множеств (для поддержки рамочных условий) и др. Одним из возможных способов поддержки таких логик является их непосредственная реализация в SMT-решателях, однако этот способ часто является трудоемким, а также недостаточно гибким и универсальным. Другим способом является реализация пользовательских стратегий инстанцирования кванторов для сведения формул в неподдерживаемых логиках к формулам в широко распространенных разрешимых логиках, таких как QF_UFLIA. В данной статье представлена процедура инстанцирования лемм для трансляции формул в теории ограниченных целых без переполнения в логику QF_UFLIA. Для процедуры трансляции даны доказательства корректности и полноты, а также описана формализация этих доказательств в системе Isabelle/HOL. Аналогичный подход можно использовать для формулирования и доказательства полноты процедур трансляции формул в других теориях, таких как теория ограниченных целых с переполнением и теория ограниченной адресной арифметики.