The post has been translated automatically. Original language: Russian
Formal verification of a compiler does not mean that the correctness of the entire language and all programs that can be written in it is automatically proven. Any such proof refers to a specific property, a specific implementation version, and predefined conditions.
This is exactly the approach we use in Sekura JS. Instead of a general statement about the complete correctness of the compiler, a set of separate requirements is formed, for each of which you can check the specific behavior of the resulting machine code.
This allows you to accurately separate properties that have already been verified from those that are not yet within the scope of verification.
Requirement as a verification unit
The behavior of the language is broken down into separate requirements. They have designations like SJS-REQ-001, SJS-REQ-002 and further.
Each such requirement describes a specific part of the language's behavior. For example, it can be an arithmetic operation, comparing values of different types, shifting, writing to memory, changing an integer value, or working with a system device.
Small Sekura JS programs and formal conditions describing the expected result are prepared for each requirement. After compilation, the machine code that has already been received is checked.
Thus, the proof does not apply to the entire language at once, but to a specific requirement.
Why can't we just say that the compiler is proven?
The compiler performs many different transformations. It parses the source text, checks the types, forms an intermediate representation, places the data, selects machine instructions, and applies optimizations.
Even if a large number of individual cases have been confirmed, this does not mean that all possible programs and all variants of their behavior have been tested.
Therefore, a successful formal verification means only the following: a specific machine code satisfies a specific formal requirement within the specified conditions.
If a certain property was not included in the check, it is impossible to draw a conclusion about it.
The conditions define the field of proof
A formal requirement may limit the allowed input values.
For example, if a function with a 32-bit unsigned argument is being checked, you can specify a condition that the input value must be less than 100.
In this case, the proof applies to all values from 0 to 99. This is different from regular testing, where only a few individual values could be selected.
But beyond the specified range, such a proof does not assert anything.
If you want to check the behavior for all possible 32-bit values, this must be explicitly specified in the verification conditions.
Only the formulated property is checked
The formal system cannot independently determine which behavior the developer considers correct.
If only the result of an arithmetic operation is checked, a successful result does not automatically mean checking the entire memory, system tables, calling conventions, or other parts of the execution environment.
Each additional property must either be included in a specific requirement or checked separately.
Therefore, it is important not only the positive result itself, but also an accurate description of what exactly was included in the test.
One source code can produce different machine code.
The Sekura JS compiler supports several levels of optimization.
The same source program may look different at the machine level after compilation. The compiler can remove unnecessary instructions, otherwise use registers, exclude unreachable sections, and perform other transformations.
At the same time, the required program behavior must be maintained.
Therefore, the same formal requirement is checked separately for different optimization levels.
The meaning of the requirement does not change. Only the machine code that must meet this requirement is being changed.
What does a positive result mean?
A positive result refers to a specific chain:
requirement → source program → machine code → formal condition → verification result
If one of these elements has changed, the previous proof cannot be automatically transferred to the new version.
For example, a new version of the compiler can create different machine code even from the same source text. In this case, the check must be performed again.
Therefore, tool versions and checksums of all participating files are saved along with the result.
This allows you to determine exactly which version of the compiler a particular proof belongs to.
What a positive result does not mean
Successful verification of a single requirement does not mean proof of the entire compiler source code.
It also does not mean proof of all Sekura JS programs, the entire memory model, or the entire hardware and software system.
If the check did not include a specific feature of the language or part of the execution environment, the successful result does not mean anything about it.
It is important to keep this restriction explicit. It allows you not to confuse confirmed properties with assumptions.
How is the compiler version profile formed?
A mandatory set of requirements can be defined for each compiler version.
Each requirement is checked for supported optimization levels. If all the mandatory checks have been completed successfully, you can make a limited statement: this version of the compiler meets the published set of requirements.
This is much more accurate than talking about the full proof of the compiler.
As new language features become available, the set of requirements can be expanded. If a new optimization level is added, the existing requirements can be re-checked for a new version of the machine code.
This is how the evidence base develops along with the compiler itself.
Why is a counterexample useful?
Formal verification is useful not only when completed successfully.
If there is a condition in which the machine code violates a given requirement, the verification tool can show the specific input values and the system state at which the error occurs.
Such an example helps to find the cause of the violation and reproduce it.
After correcting the compiler, the same requirement can be left in a permanent set of checks. If a similar error appears again, a formal check should detect it.
Why are proof boundaries important?
Formal methods give a strong result only when it is precisely determined what exactly has been proved.
If a certain property is confirmed for the entire specified range of values, this is significantly stronger than the usual set of tests for the same property. But if the other part of the behavior was not included in the formal description at all, no conclusions can be drawn about it.
Therefore, it is not only the fact of successful verification that is important for Sekura JS. It is necessary to always be able to answer four questions: what was checked, for which version, under what conditions, and with what result it was confirmed.
It is from such separate and reproducible checks that the evidence base of the compiler is gradually being formed.
Our goal is not to declare the entire compiler fully proven as early as possible. It is much more important to consistently expand the scope of confirmed requirements and at any moment accurately see the boundary between the behavior that has already been verified and what remains to be verified.
Формальная проверка компилятора не означает, что автоматически доказана правильность всего языка и всех программ, которые на нём можно написать. Любое такое доказательство относится к конкретному свойству, определённой версии реализации и заранее заданным условиям.
В Sekura JS мы используем именно такой подход. Вместо общего утверждения о полной корректности компилятора формируется набор отдельных требований, для каждого из которых можно проверить конкретное поведение полученного машинного кода.
Это позволяет точно отделять уже подтверждённые свойства от тех, которые ещё не входят в область проверки.
Требование как единица проверки
Поведение языка разбивается на отдельные требования. Они имеют обозначения вида SJS-REQ-001, SJS-REQ-002 и далее.
Каждое такое требование описывает определённую часть поведения языка. Например, это может быть арифметическая операция, сравнение значений разных типов, сдвиг, запись в память, изменение целочисленного значения или работа с системным устройством.
Для каждого требования подготавливаются небольшие программы на Sekura JS и формальные условия, описывающие ожидаемый результат. После компиляции проверяется уже полученный машинный код.
Таким образом, доказательство относится не ко всему языку сразу, а к конкретному требованию.
Почему нельзя просто сказать, что компилятор доказан
Компилятор выполняет много разных преобразований. Он разбирает исходный текст, проверяет типы, формирует промежуточное представление, размещает данные, выбирает машинные инструкции и применяет оптимизации.
Даже если подтверждено большое количество отдельных случаев, это ещё не означает, что проверены все возможные программы и все варианты их поведения.
Поэтому успешная формальная проверка означает только следующее: конкретный машинный код удовлетворяет конкретному формальному требованию в пределах заданных условий.
Если некоторое свойство не входило в проверку, делать вывод о нём нельзя.
Условия определяют область доказательства
Формальное требование может ограничивать допустимые входные значения.
Например, если проверяется функция с 32-разрядным беззнаковым аргументом, можно указать условие, что входное значение должно быть меньше 100.
В этом случае доказательство относится ко всем значениям от 0 до 99. Это отличается от обычного тестирования, где могли бы быть выбраны только несколько отдельных значений.
Но за пределами указанного диапазона такое доказательство ничего не утверждает.
Если требуется проверить поведение для всех возможных 32-разрядных значений, это должно быть явно задано в условиях проверки.
Проверяется только сформулированное свойство
Формальная система не может самостоятельно определить, какое поведение разработчик считает правильным.
Если проверяется только результат арифметической операции, успешный результат не означает автоматическую проверку всей памяти, системных таблиц, соглашения о вызовах или других частей среды исполнения.
Каждое дополнительное свойство должно быть либо включено в конкретное требование, либо проверено отдельно.
Поэтому важен не только сам положительный результат, но и точное описание того, что именно входило в проверку.
Один исходный код может давать разный машинный код
Компилятор Sekura JS поддерживает несколько уровней оптимизации.
Одна и та же исходная программа может после компиляции выглядеть по-разному на машинном уровне. Компилятор может удалять лишние инструкции, иначе использовать регистры, исключать недостижимые участки и выполнять другие преобразования.
При этом требуемое поведение программы должно сохраняться.
Поэтому одно и то же формальное требование проверяется отдельно для разных уровней оптимизации.
Смысл требования при этом не меняется. Меняется только машинный код, который должен этому требованию соответствовать.
Что означает положительный результат
Положительный результат относится к конкретной цепочке:
требование → исходная программа → машинный код → формальное условие → результат проверки
Если один из этих элементов изменился, прежнее доказательство нельзя автоматически переносить на новую версию.
Например, новая версия компилятора может создать другой машинный код даже из того же исходного текста. В таком случае проверку необходимо выполнить заново.
Поэтому вместе с результатом сохраняются версии инструментов и контрольные суммы всех участвующих файлов.
Это позволяет точно установить, к какой версии компилятора относится конкретное доказательство.
Чего положительный результат не означает
Успешная проверка отдельного требования не означает доказательство всего исходного кода компилятора.
Она также не означает доказательство всех программ на Sekura JS, всей модели памяти или всей программно-аппаратной системы.
Если в проверку не входила определённая возможность языка или часть среды исполнения, успешный результат ничего о ней не говорит.
Такое ограничение важно сохранять явно. Оно позволяет не смешивать подтверждённые свойства с предположениями.
Как формируется профиль версии компилятора
Для каждой версии компилятора можно определить обязательный набор требований.
Каждое требование проверяется для поддерживаемых уровней оптимизации. Если все обязательные проверки завершились успешно, можно сделать ограниченное утверждение: эта версия компилятора соответствует опубликованному набору требований.
Это гораздо точнее, чем говорить о полной доказанности компилятора.
При появлении новых возможностей языка набор требований можно расширять. Если добавляется новый уровень оптимизации, существующие требования можно повторно проверить уже для нового варианта машинного кода.
Так доказательная база развивается вместе с самим компилятором.
Почему полезен контрпример
Формальная проверка полезна не только тогда, когда завершается успешно.
Если существует состояние, в котором машинный код нарушает заданное требование, проверяющий инструмент может показать конкретные входные значения и состояние системы, при которых возникает ошибка.
Такой пример помогает найти причину нарушения и воспроизвести её.
После исправления компилятора то же требование можно оставить в постоянном наборе проверок. Если похожая ошибка появится снова, формальная проверка должна обнаружить её.
Почему важны границы доказательства
Формальные методы дают сильный результат только тогда, когда точно определено, что именно было доказано.
Если некоторое свойство подтверждено для всей заданной области значений, это значительно сильнее обычного набора тестов для того же свойства. Но если другая часть поведения вообще не входила в формальное описание, никаких выводов о ней делать нельзя.
Поэтому для Sekura JS важен не только сам факт успешной проверки. Необходимо всегда иметь возможность ответить на четыре вопроса: что проверялось, для какой версии, при каких условиях и каким результатом это подтверждено.
Именно из таких отдельных и воспроизводимых проверок постепенно формируется доказательная база компилятора.
Наша цель не в том, чтобы как можно раньше объявить весь компилятор полностью доказанным. Гораздо важнее последовательно расширять область подтверждённых требований и в любой момент точно видеть границу между уже проверенным поведением и тем, что ещё предстоит проверить.
Share
