The post has been translated automatically. Original language: Russian
The compiler is usually checked by tests. They take programs with known behavior, compile them, run the resulting code, and compare the result with the expected one. The more such checks, the higher the confidence that the compiler is working correctly.
This was not enough for Sekura JS. The language is created as part of a stack in which the properties of programs must not only be tested on individual examples, but also formally confirmed. If we want to prove the properties of a program after compilation, the natural question arises: how much can we trust the machine code that the compiler created itself?
That is why we have started a formal verification of the results of the Sekura JS compiler.
Where the problem occurs
The source program and the machine code are not the same thing. Between them is a compiler that parses the program, transforms its representation, selects processor instructions, places data, and applies optimizations.
Even if the source code looks correct, an error at any of these stages may change its actual behavior.
A regular test is able to detect such a problem if it appears on the selected input data. But the space of possible values and states of the program can be significantly larger than the test suite.
For systems where a higher level of confidence is required, we are interested in another question: is it possible to verify that the resulting machine code fulfills a given property for the entire defined input data area?
We do not prove the source code of the compiler.
It is important to draw a line here.
We are not trying to mathematically prove the correctness of the entire source code of the Sekura JS compiler. This approach is possible in theory, but it is a separate and much more complex task.
Instead, we check the result of his work.
A formal behavior requirement is set in advance for a specific program. The program is then compiled with a regular Sekura JS compiler, after which the already created machine object is checked.
In a simplified form, the process looks like this:
source program → compiler → machine code → formal verification
If the machine code meets the specified requirement, the verification result can be saved as a separate evidentiary artifact.
This approach does not turn the entire compiler into a proven program. It allows you to confirm that a specific compilation result meets a specific formal requirement.
What exactly is being checked
The source code of the Sekura JS program is stored in the SJS file. After compilation, an executable SOBJ object is created containing the machine code for the Memora8 architecture.
An SJV description is created separately, which specifies the property to be checked. These can be conditions for input values, the state of memory, the result of a function, or a change in the state of a program.
SJV checks the behavior of the already compiled SOBJ with respect to the semantics of the Memora8 commands and the specified contract.
Thus, the object of verification is not an assumption about how the compiler should have worked, but the actual machine code that it created.
How is this different from a regular test?
Let's imagine a function that takes a 32-bit value.
Dozens, thousands, or millions of values can be tested in tests. But it will still be a finite set of examples.
In formal verification, the input value may be symbolic. It represents all the values that meet the specified conditions at once.
If it is necessary to prove, for example, a certain property for the range from 0 to 99, the verifier considers the entire range within the framework of a mathematical model, rather than choosing several individual examples.
If there is a value at which the requirement is violated, the check may return a counterexample. If there is no such condition in the specified model, the property is considered confirmed within the specified conditions.
Why do I need to check optimized code?
The same source text may result in different machine code depending on the compilation mode.
The compiler can delete unnecessary instructions, change the operation of registers, or exclude unreachable parts of the program. At the same time, the external behavior of the program must be maintained within the limits defined by the language and the specific requirement.
Therefore, it is not enough to check only the simplest compilation mode.
In our model, the same requirement can be applied to the results of different levels of optimization. The formal property remains the same, and the machine code is recreated each time and checked separately.
This allows you to check not only the semantics of the language design, but also whether it has been preserved after compiler transformations.
Requirements instead of a general statement
The phrase "the compiler is proven" sounds strong, but it says practically nothing about the limits of such a statement.
We chose a different approach. The semantics of the language is broken down into separate requirements. Programs and formal contracts are prepared for each requirement, which describe a specific verifiable property.
For example, you can check arithmetic operations, comparisons, working with different types, writing to memory, or other language constructs separately.
As the coverage increases, so does the evidence base of a particular compiler version.
At the same time, each result remains limited by its own requirement. If a certain property was not included in the contract, a successful verification does not allow us to assert that it is automatically proven.
The proof must relate to the exact version
The compiler is constantly evolving. Changing even a few lines of its source code can lead to a different machine result.
Therefore, the formal verification should be related not just to the name of the program, but to specific versions of all participating components.
For the result, the versions and checksums of the compiler, the verification tool, the source program, the formal contract, and the resulting machine object are recorded. After successful verification, an SJP packet is generated, which stores the information necessary to reproduce the result.
This allows you to later determine which compiler created the verified code and which means the verification was performed.
Formal verification as part of compiler development
What is important to us is not a one-time experiment, but the opportunity to make such a test part of the normal development process.
When a new version of the compiler is released, a fixed set of programs can be recompiled, new machine objects can be obtained, and formal checks can be repeated. If the compiler changes violated one of the fixed requirements, this should be reflected in the appropriate check.
Thus, together with the compiler, a permanent evidence base for its behavior is being developed.
This does not cancel out the usual tests. Testing remains necessary to verify a large number of practical scenarios, the operation of tools, and the entire system. Formal verification complements it where it is necessary to confirm a specific property for the entire specified range of states.
Why is all this Sekura JS
Sekura JS is being created as a system language for the software layer associated with the Memora8 architecture and the subsequent Sekura stack.
If the ultimate goal is to build a system where it is possible to formally verify properties from the hardware level to the software module, the compiler should not remain a completely opaque intermediate link.
That's why we started building a verifiable chain between the Sekura JS source program and the actual executable machine code.
The goal here is not to put a "compiler proven" mark one day. It is much more useful to have an accurate answer to another question: which properties of a particular version of the compiler have already been confirmed by formal checks, for which compilation modes, and based on which reproducible evidence.
Компилятор обычно проверяют тестами. Берут программы с известным поведением, компилируют их, запускают полученный код и сравнивают результат с ожидаемым. Чем больше таких проверок, тем выше уверенность, что компилятор работает правильно.
Для Sekura JS этого оказалось недостаточно. Язык создаётся как часть стека, в котором свойства программ должны быть не только проверены на отдельных примерах, но и подтверждены формально. Если мы хотим доказывать свойства программы после компиляции, возникает естественный вопрос: насколько можно доверять машинному коду, который создал сам компилятор?
Именно поэтому мы начали формальную проверку результатов работы компилятора Sekura JS.
Где возникает проблема
Исходная программа и машинный код — это не одно и то же. Между ними находится компилятор, который разбирает программу, преобразует её представление, выбирает инструкции процессора, размещает данные и применяет оптимизации.
Даже если исходный код выглядит правильно, ошибка на любом из этих этапов может изменить его фактическое поведение.
Обычный тест способен обнаружить такую проблему, если она проявилась на выбранных входных данных. Но пространство возможных значений и состояний программы может быть значительно больше набора тестов.
Для систем, где требуется более высокий уровень уверенности, нас интересует другой вопрос: можно ли проверить, что полученный машинный код выполняет заданное свойство для всей определённой области входных данных?
Мы не доказываем исходный код компилятора
Здесь важно провести границу.
Мы не пытаемся математически доказать корректность всего исходного кода компилятора Sekura JS. Такой подход возможен в теории, но это отдельная и значительно более сложная задача.
Вместо этого мы проверяем результат его работы.
Для конкретной программы заранее задаётся формальное требование к поведению. Затем программа компилируется обычным компилятором Sekura JS, после чего проверяется уже созданный машинный объект.
В упрощённом виде процесс выглядит так:
исходная программа → компилятор → машинный код → формальная проверка
Если машинный код удовлетворяет заданному требованию, результат проверки можно сохранить как отдельный доказательный артефакт.
Такой подход не превращает весь компилятор в доказанную программу. Он позволяет подтверждать, что конкретный результат компиляции соответствует конкретному формальному требованию.
Что именно проверяется
Исходный текст программы Sekura JS хранится в файле SJS. После компиляции создаётся исполняемый объект SOBJ, содержащий машинный код для архитектуры Memora8.
Отдельно создаётся описание SJV, которое задаёт проверяемое свойство. Это могут быть условия на входные значения, состояние памяти, результат функции или изменение состояния программы.
SJV проверяет поведение уже скомпилированного SOBJ относительно семантики команд Memora8 и заданного контракта.
Таким образом, объектом проверки является не предположение о том, как должен был сработать компилятор, а фактический машинный код, который он создал.
Чем это отличается от обычного теста
Представим функцию, принимающую 32-битное значение.
В тестах можно проверить десятки, тысячи или миллионы значений. Но это всё равно будет конечный набор примеров.
При формальной проверке входное значение может быть символическим. Оно представляет сразу все значения, удовлетворяющие заданным условиям.
Если требуется доказать, например, некоторое свойство для диапазона от 0 до 99, проверяющий рассматривает весь этот диапазон в рамках математической модели, а не выбирает несколько отдельных примеров.
Если существует значение, при котором требование нарушается, проверка может вернуть контрпример. Если такого состояния в заданной модели нет, свойство считается подтверждённым в пределах указанных условий.
Почему проверять нужно и оптимизированный код
Один и тот же исходный текст может приводить к разному машинному коду в зависимости от режима компиляции.
Компилятор может удалять лишние инструкции, менять работу с регистрами или исключать недостижимые участки программы. При этом внешнее поведение программы должно сохраняться в тех пределах, которые определены языком и конкретным требованием.
Поэтому проверять только наиболее простой режим компиляции недостаточно.
В нашей модели одно и то же требование можно применять к результатам разных уровней оптимизации. Формальное свойство остаётся прежним, а машинный код каждый раз создаётся заново и проверяется отдельно.
Это позволяет проверять не только семантику конструкции языка, но и то, сохранилась ли она после преобразований компилятора.
Требования вместо общего утверждения
Фраза «компилятор доказан» звучит сильно, но практически ничего не говорит о границах такого утверждения.
Мы выбрали другой подход. Семантика языка разбивается на отдельные требования. Для каждого требования подготавливаются программы и формальные контракты, которые описывают конкретное проверяемое свойство.
Например, отдельно можно проверять арифметические операции, сравнения, работу с разными типами, запись в память или другие конструкции языка.
По мере роста покрытия увеличивается и доказательная база конкретной версии компилятора.
При этом каждый результат остаётся ограниченным своим требованием. Если некоторое свойство не было включено в контракт, успешная проверка не позволяет утверждать, что оно автоматически доказано.
Доказательство должно относиться к точной версии
Компилятор постоянно развивается. Изменение даже нескольких строк его исходного кода может привести к другому машинному результату.
Поэтому формальная проверка должна быть связана не просто с названием программы, а с конкретными версиями всех участвующих компонентов.
Для результата фиксируются версии и контрольные суммы компилятора, средства проверки, исходной программы, формального контракта и полученного машинного объекта. После успешной проверки формируется SJP — пакет, в котором сохраняются сведения, необходимые для воспроизведения результата.
Это позволяет позже установить, какой именно компилятор создал проверенный код и каким именно средством выполнялась проверка.
Формальная проверка как часть разработки компилятора
Для нас важен не разовый эксперимент, а возможность сделать такую проверку частью обычного процесса разработки.
При выпуске новой версии компилятора можно заново скомпилировать фиксированный набор программ, получить новые машинные объекты и повторить формальные проверки. Если изменения компилятора нарушили одно из зафиксированных требований, это должно проявиться в соответствующей проверке.
Таким образом, вместе с компилятором развивается и постоянная доказательная база его поведения.
Это не отменяет обычные тесты. Тестирование остаётся необходимым для проверки большого количества практических сценариев, работы инструментов и всей системы в целом. Формальная проверка дополняет его там, где необходимо подтвердить конкретное свойство для всей заданной области состояний.
Зачем всё это Sekura JS
Sekura JS создаётся как системный язык для программного слоя, связанного с архитектурой Memora8 и дальнейшим стеком Sekura.
Если конечная цель состоит в построении системы, где можно формально проверять свойства от аппаратного уровня до программного модуля, компилятор не должен оставаться полностью непрозрачным промежуточным звеном.
Поэтому мы начали строить проверяемую цепочку между исходной программой Sekura JS и фактически исполняемым машинным кодом.
Цель здесь не в том, чтобы однажды поставить отметку «компилятор доказан». Гораздо полезнее иметь точный ответ на другой вопрос: какие свойства конкретной версии компилятора уже подтверждены формальными проверками, для каких режимов компиляции и на основании каких воспроизводимых доказательств.
Share
