The post has been translated automatically. Original language: Russian
Formal compiler validation can mean different things. You can try to mathematically prove the correctness of the compiler's source code itself, or you can check its specific results — the machine code that it actually creates for a given program.
In Sekura JS, we use the second approach. For each verifiable language construct, the source program is taken, the expected behavior is formulated, then the program is compiled and the executable object already obtained is checked.
In a simplified form, the chain looks like this:
SJS → Sekura JS → SOBJ → SJV → SJP compiler
Each element of this chain has its own role.
The original program
SJS is the source file of the Sekura JS program. It contains the usual code: functions, operations, working with variables, memory, and other language constructs.
For formal verification, it is important that the source program is not in itself a proof. It only defines a specific case that must be passed through a real compiler.
After compilation, we get the same result that should be used during normal program execution.
SOBJ — the actual compilation result
The Sekura JS compiler converts the source SJS into a machine object SOBJ. It contains code designed to run on the Memora8 architecture.
SOBJ is the main object of further verification.
This is an important difference from the approach in which only the source program is formally analyzed. We are interested not only in what the developer wrote, but also in what the compiler actually transformed this code into.
If an error occurs during the generation of machine instructions, a formal SOBJ check should be able to detect it.
SJV sets the required behavior
An SJV description is created separately from the source program. It sets a formal contract — that is, the conditions that the behavior of the code being tested must meet.
The contract can define a valid initial state and an expected state after the function is executed. In this case, the values can be symbolic, that is, they represent not one specific number, but many acceptable values at once.
For example, if the value < 100 condition is set for the input u32, the check applies to all values from 0 to 99, and not to several pre-selected examples.
Thus, SJV answers the question: what exactly do we want to prove about the compilation result.
How does SJV validate machine code
SJV binds a formal contract to functions in SOBJ and symbolically executes machine code relative to the semantics of Memora8 commands.
Instead of one specific state, symbolic meanings and expressions are used. At each step, a mathematical model is formed of what the state of the program may be under given conditions.
The examiner then looks for the possibility of a breach of contract.
If such a condition exists, the result is a counterexample. It shows a specific set of conditions under which the machine code does not behave as required.
If a violation in the specified area is not possible, the checked property is considered confirmed.
Why is the machine code being checked?
This allows you to separate the two issues.
First, have we formulated the program property correctly?
Second: has the compiler created machine code that actually corresponds to this property?
If you check only the source text, the error in generating instructions may remain beyond the proof. SOBJ verification allows you to include the result of the compiler's work in the proof chain.
During the development of Sekura JS, this approach already made it possible to identify code generation errors, which, after correction, were added to permanent verification scripts.
The role of Z3
After symbolic execution, the verification conditions are transformed into a problem for the Z3 solver.
In a simplified way, the possibility of a condition violating the contract is checked. If the solver finds such a state, SJV gets a counterexample. If the violation is impossible within the formed model, the task confirms the corresponding property.
At the same time, Z3 does not know anything about the Sekura JS language or the SOBJ format. His task is to solve an already formed logical expression.
The responsibility for correctly converting machine code and contract into this model lies with SJV.
What is recorded after verification
A successful launch by itself is not enough. After some time, it is necessary to be able to establish exactly what was tested and on which source data the result was obtained.
To do this, an SJP is formed — an evidentiary verification package.
It captures the relationship with the original artifacts and startup parameters. Checksums of SJS, SJV, SOBJ and the tools used are also stored for the results.
This allows you to link the proof not to the abstract phrase "this function has been verified," but to a specific version of the program, a specific machine object, and a specific contract.
Why do we need different levels of optimization?
The same SJS can generate different SOBJ depending on the optimization level.
Optimization can change the sequence of instructions, work with registers, delete unreachable code, and perform other transformations. At the same time, the required external behavior of the program must be preserved.
Therefore, the same formal contract can be checked separately for several variants of the machine code.
The meaning of the requirement does not change. Only the specific SOBJ that needs to match it changes.
This is how formal verification begins to cover not only individual language constructs, but also transformations performed by the compiler.
What does a successful check mean?
A successful outcome has limited meaning.
It means that a specific SOBJ satisfies a specific SJV contract under the specified preconditions and within the limits of the model used.
It does not automatically mean that the entire compiler, the entire Sekura JS language, or any program that this compiler can ever process has been proven.
That is why the verification is built as a set of separate requirements. Each requirement must have a clear scope and its own evidentiary materials.
Why is this approach convenient for compiler development?
The compiler can continue to be developed in the usual engineering way. Code generation is changing, new features and optimizations are being added, and bugs are being fixed.
After the changes, the fixed source programs are compiled anew, and their results are formally checked again.
If the new version of the compiler has changed the behavior in the area of an already fixed requirement, this should manifest itself as a violation of the relevant contract.
As a result, formal verification becomes not a separate experiment, but a repeatable part of the development.
The main thing
In our approach, the proof is not based around trusting the compiler as a single complex object.
We connect four specific things.:
the source program, the machine result of compilation, the formal requirement, and the reproducible verification result.
This makes it possible to gradually accumulate verifiable language coverage and understand exactly which properties of a particular compiler version have already been confirmed and which have not yet been confirmed.
Формальная проверка компилятора может означать разные вещи. Можно пытаться математически доказать корректность самого исходного кода компилятора, а можно проверять его конкретные результаты — тот машинный код, который он реально создаёт для заданной программы.
В Sekura JS мы используем второй подход. Для каждой проверяемой конструкции языка берётся исходная программа, формулируется ожидаемое поведение, затем программа компилируется и проверяется уже полученный исполняемый объект.
В упрощённом виде цепочка выглядит так:
SJS → компилятор Sekura JS → SOBJ → SJV → SJP
Каждый элемент этой цепочки имеет свою роль.
Исходная программа
SJS — это исходный файл программы на Sekura JS. В нём находится обычный код: функции, операции, работа с переменными, памятью и другими конструкциями языка.
Для формальной проверки важно, что исходная программа не является сама по себе доказательством. Она лишь задаёт конкретный случай, который должен пройти через реальный компилятор.
После компиляции мы получаем тот же результат, который должен использоваться при обычном выполнении программы.
SOBJ — фактический результат компиляции
Компилятор Sekura JS преобразует исходный SJS в машинный объект SOBJ. В нём находится код, предназначенный для выполнения на архитектуре Memora8.
Именно SOBJ является главным объектом дальнейшей проверки.
Это важное отличие от подхода, при котором формально анализируется только исходная программа. Нас интересует не только то, что написано разработчиком, но и то, во что компилятор фактически преобразовал этот код.
Если на этапе генерации машинных инструкций произошла ошибка, формальная проверка SOBJ должна иметь возможность её обнаружить.
SJV задаёт требуемое поведение
Отдельно от исходной программы создаётся описание SJV. Оно задаёт формальный контракт — то есть условия, которым должно соответствовать поведение проверяемого кода.
В контракте можно определить допустимое начальное состояние и ожидаемое состояние после выполнения функции. Значения при этом могут быть символическими, то есть представлять не одно конкретное число, а сразу множество допустимых значений.
Например, если для входного u32 задано условие value < 100, проверка относится ко всем значениям от 0 до 99, а не к нескольким заранее выбранным примерам.
Таким образом, SJV отвечает на вопрос: что именно мы хотим доказать о результате компиляции.
Как SJV проверяет машинный код
SJV связывает формальный контракт с функциями в SOBJ и символически исполняет машинный код относительно семантики команд Memora8.
Вместо одного конкретного состояния используются символические значения и выражения. На каждом шаге формируется математическая модель того, каким может быть состояние программы при заданных условиях.
Затем проверяющий ищет возможность нарушения контракта.
Если такое состояние существует, результатом становится контрпример. Он показывает конкретный набор условий, при котором машинный код ведёт себя не так, как требуется.
Если нарушение в заданной области невозможно, проверяемое свойство считается подтверждённым.
Почему проверяется именно машинный код
Это позволяет отделить два вопроса.
Первый: правильно ли мы сформулировали свойство программы?
Второй: создал ли компилятор машинный код, который этому свойству действительно соответствует?
Если проверять только исходный текст, ошибка генерации инструкций может остаться за пределами доказательства. Проверка SOBJ позволяет включить результат работы компилятора в доказательную цепочку.
В ходе развития Sekura JS такой подход уже позволял выявлять ошибки генерации кода, которые после исправления добавлялись в постоянные проверочные сценарии.
Роль Z3
После символического исполнения условия проверки преобразуются в задачу для решателя Z3.
Упрощённо проверяется возможность существования состояния, нарушающего контракт. Если решатель находит такое состояние, SJV получает контрпример. Если нарушение невозможно в пределах сформированной модели, задача подтверждает соответствующее свойство.
При этом Z3 не знает ничего о языке Sekura JS или формате SOBJ. Его задача — решить уже сформированное логическое выражение.
Ответственность за правильное преобразование машинного кода и контракта в эту модель лежит на SJV.
Что фиксируется после проверки
Успешный запуск сам по себе недостаточен. Через некоторое время необходимо иметь возможность установить, что именно проверялось и на каких исходных данных был получен результат.
Для этого формируется SJP — доказательный пакет проверки.
В нём фиксируется связь с исходными артефактами и параметрами запуска. Для результатов также сохраняются контрольные суммы SJS, SJV, SOBJ и используемых инструментов.
Это позволяет связать доказательство не с абстрактной фразой «эта функция проверена», а с конкретной версией программы, конкретным машинным объектом и конкретным контрактом.
Зачем нужны разные уровни оптимизации
Один и тот же SJS может порождать разный SOBJ в зависимости от уровня оптимизации.
Оптимизация может менять последовательность инструкций, работу с регистрами, удалять недостижимый код и выполнять другие преобразования. При этом требуемое внешнее поведение программы должно сохраняться.
Поэтому один и тот же формальный контракт можно проверять отдельно для нескольких вариантов машинного кода.
Смысл требования не меняется. Меняется только конкретный SOBJ, который должен ему соответствовать.
Так формальная проверка начинает охватывать не только отдельные конструкции языка, но и преобразования, выполняемые компилятором.
Что означает успешная проверка
Успешный результат имеет ограниченный смысл.
Он означает, что конкретный SOBJ удовлетворяет конкретному SJV-контракту при заданных предусловиях и в пределах используемой модели.
Он не означает автоматически, что доказан весь компилятор, весь язык Sekura JS или любая программа, которую этот компилятор может когда-либо обработать.
Именно поэтому проверка строится как набор отдельных требований. Каждое требование должно иметь понятную область действия и собственные доказательные материалы.
Почему такой подход удобен для развития компилятора
Компилятор можно продолжать разрабатывать обычным инженерным способом. Меняется генерация кода, добавляются новые возможности и оптимизации, исправляются ошибки.
После изменений фиксированные исходные программы компилируются заново, а их результаты снова проходят формальную проверку.
Если новая версия компилятора изменила поведение в области уже зафиксированного требования, это должно проявиться как нарушение соответствующего контракта.
В результате формальная проверка становится не отдельным экспериментом, а повторяемой частью разработки.
Главное
В нашем подходе доказательство строится не вокруг доверия к компилятору как к единому сложному объекту.
Мы связываем четыре конкретные вещи:
исходную программу, машинный результат компиляции, формальное требование и воспроизводимый результат проверки.
Так появляется возможность постепенно накапливать проверяемое покрытие языка и точно понимать, какие свойства конкретной версии компилятора уже подтверждены, а какие ещё нет.
Share
