Синтез и эквивалентность
Защищайте структуру важных вычислений, проверяя сохранение результатов.
Пересинтез самого вычисления#
CEGIS, индуктивный синтез по контрпримерам, ищет альтернативное вычисление на основе поведения и контрпримеров. Для допустимых чистых скалярных регионов кандидаты строятся в другом булево-арифметическом базисе и порядке вычисления. Меняется сам граф выражения, а не только оформление инструкций.
Контрпример направляет следующий кандидат#
Кандидат проходит региональную проверку эквивалентности. Найденный вход с расхождением возвращается в синтез, и следующий кандидат обязан его учитывать. Получается явный цикл поиска и доказательства вместо принятия формулы по нескольким удачным примерам.
Принимается только доказанное преобразование региона#
Валидатор различает PROVED, COUNTEREXAMPLE_FOUND, OUT_OF_SCOPE и UNKNOWN_BUDGET_EXCEEDED. Принимается только PROVED. Исчерпание бюджета решателя не считается успехом; регион вне поддерживаемой модели не может использовать доказательство другого контекста.
Правила решения валидатора. Схема не запускает решатель.
R₀(x)R₁(x)Результаты + traps + предусловия
Кандидат принимается в заданной модели и предусловиях. Решение относится к этому преобразованию, не ко всему приложению.
Конкретный вход обнаруживает различие. Кандидат отклоняется, контрпример возвращается в синтез.
Регион нарушает условия чистоты, владения, frame или границ. Эта модель не позволяет его принять.
Бюджет исчерпан без доказательства. Неопределённый результат не разрешает преобразование и не кешируется как успешное доказательство.
Точный контракт доказательства#
Модель сравнивает точные 32/64-битные результаты и trap-поведение при заданных предусловиях и обязательствах frame. Знаковая разрядность, переполнение и деление на ноль входят в контракт. Регрессии охватывают отсутствующие предусловия, разные trap-каналы, неопределённые результаты и кеш доказательств.
Это ограниченное свойство корректности принятого преобразования, а не доказательство безошибочности всего приложения или невозможности обратного анализа. Проверка приложения и модель безопасности остаются отдельными задачами.