The post has been translated automatically. Original language: Russian
The first major stage of formal verification of compilation results has been completed in Sekura JS. For the SJS-REQ-001 requirement, a permanent set of programs, formal contracts, and validation results has been prepared for optimization levels from O0 to O4.
As a result, 225 signed SJP packages were generated. All of them were retested, and the tool versions, build parameters, and checksums of the participating files were recorded along with the results.
This does not mean that the entire Sekura JS compiler is formally proven. The result relates to a specific set of requirements and shows which part of the compiler's behavior we already know how to check in a reproducible way.
What is SJS-REQ-001?
For formal verification, the semantics of Sekura JS is broken down into separate requirements. Each requirement defines a set of language properties that must be preserved after compilation.
SJS-REQ-001 was the first such large profile. It includes basic integer operations, comparisons, working with different types, shifts, bitwise and logical operations, compound assignments, increments and decrements, as well as operations with narrow values.
For each test case, there is a Sekura JS source program and a corresponding SJV contract. The program is compiled into a SOBJ machine object, after which the actual machine code is checked.
Thus, the result does not refer to an abstract description of the language, but to the specific code that the compiler created.
Why check all optimization levels?
The same source text can lead to different machine code depending on the chosen optimization level.
In simple mode, the compiler tries to maintain as direct a relationship as possible between the source program and the generation result. At higher levels, it can remove unnecessary instructions, change the distribution of values across registers, eliminate unreachable code, and perform other transformations.
At the same time, the meaning of the program must be preserved.
Therefore, a formal contract is checked more than once. For the same requirement, machine objects obtained at O0, O1, O2, O3, and O4 are created and checked separately.
This allows you to check not only a single language construct, but also whether the compiler has preserved its behavior after optimization.
What is included in the coverage
The first set includes arithmetic operations and combinations of integer types i8, u8, i16, u16, i32 and u32. For operations where the types of the left and right operands may differ, a 6×6 combination matrix is checked.
The usual comparisons and the CMP machine operation, bitwise and logical operations, shifts, compound assignments, as well as prefix and postfix increments and decrements are checked separately.
A significant part of the work is related to narrow types. It is important for them not only to get the correct arithmetic value, but also to correctly write it back into memory without changing the neighboring data.
In a recent expansion of the evidence-based verification, all 36 combinations of types for mixed multiplication were closed. Checks for composite records and increments of narrow values in local arrays, packed fields, global variables, and global arrays have also been added.
For arrays, the safety of neighboring elements is additionally checked.
System Bus as a separate area
SJS-REQ-001 also includes a portable System Bus area limited to the SB_ECHO device.
This is important in terms of the boundaries of the proof. We do not claim that all processor-dependent System Bus commands are already included in the formally verified coverage.
In the current requirement, only the explicitly designated portable area is checked. The remaining teams remain outside this requirement and must receive their own formal conditions if they are included in the evidence base.
This approach allows you to avoid mixing confirmed behavior with what has only been implemented or tested so far.
Why did we get 225 packages?
Each SJP package refers to a specific combination of the source program, the formal contract, the compilation result, and the optimization level.
After successful verification, a separate SJP is created, which is associated with the exact input data and tools. Therefore, the evidence base does not consist of one general report, but of a large number of independent results.
There were 225 such packages for SJS-REQ-001.
Their quantity alone is not an indicator of quality. More importantly, each package is associated with a specific requirement and can be checked repeatedly.
Re-checking the results
All 225 SJPS have been retested.
Checksums of the source program, the contract, the machine object, and the evidence package itself are stored for each result. The versions of the compiler and the testing tool are also recorded.
This is necessary so that the result can be linked to a specific version of the system.
If the source program, compiler, optimization level, or the testing tool itself are changed, the old result cannot be automatically considered valid for the new version. The check must be performed again.
That is why we consider formal verification as a constantly reproducible process, and not as a one-time report.
What does this result show?
The 225 successful packages mean that the corresponding machine objects satisfy their formal contracts within the specified preconditions and the model used.
From this, we cannot conclude that the entire Sekura JS compiler is fully proven.
Not all language constructs are included in SJS-REQ-001. Not all properties of the memory, system environment, and hardware platform automatically follow from these checks.
But now there is a specific and measurable area for which source programs, requirements, compilation results, and evidence packages can be shown.
This is much more accurate than the general statement about the quality of the compiler.
Public repository of results
The next important step is to make the evidence base available for independent study.
It is planned to open a public repository in GitLab, where the SJS source programs, formal SJV contracts, compilation results, SJP packages, checksums, information about tool versions and other materials necessary for re-verification will be hosted.
The repository is planned to be published under the Apache License 2.0.
The idea here is simple: if the result of a formal verification cannot be independently studied and repeated, its value as engineering evidence is limited.
An open set of artifacts will allow other developers to see exactly which property was checked, which machine code was obtained, and which result was verified.
Why make the evidence base open?
Formal verification is especially useful when its result can be verified independently of the author.
An open repository allows you to separate the developer's approval from the materials themselves. Instead of saying "we checked the compiler", it becomes possible to show a specific requirement, a specific source code, a specific SOBJ and the corresponding SJP.
It also makes it easier to re-check new versions.
If the compiler has changed, you can reassemble the same set of source programs, get new machine objects, and compare the results with the previous version.
Gradually, such a database can become a history of the development of formally proven Sekura JS coverage.
What's next
SJS-REQ-001 is only the first major profile.
The following requirements should expand the scope of the language and system capabilities. New designs will be added not just as tests, but as separate properties with formal contracts and reproducible results.
The main goal at this stage is not to maximize the number of evidence packages.
It is much more important to build a process in which, for each version of the compiler, it is possible to show exactly which properties have already been confirmed, at which optimization levels they have been tested, and where the artifacts are located that allow the result to be repeated.
225 SJP packets are the first major result of this approach.
В Sekura JS завершён первый крупный этап формальной проверки результатов компиляции. Для требования SJS-REQ-001 подготовлен постоянный набор программ, формальных контрактов и результатов проверки для уровней оптимизации от O0 до O4.
В результате сформировано 225 подписанных пакетов SJP. Все они прошли повторную проверку, а версии инструментов, параметры сборки и контрольные суммы участвующих файлов были зафиксированы вместе с результатами.
Это ещё не означает, что весь компилятор Sekura JS формально доказан. Результат относится к конкретному набору требований и показывает, какую часть поведения компилятора мы уже умеем проверять воспроизводимым способом.
Что такое SJS-REQ-001
Для формальной проверки семантика Sekura JS разбивается на отдельные требования. Каждое требование определяет набор свойств языка, которые должны сохраняться после компиляции.
SJS-REQ-001 стал первым таким крупным профилем. В него вошли основные целочисленные операции, сравнения, работа с разными типами, сдвиги, побитовые и логические операции, составные присваивания, инкременты и декременты, а также операции с узкими значениями.
Для каждого проверяемого случая существует исходная программа Sekura JS и соответствующий контракт SJV. Программа компилируется в машинный объект SOBJ, после чего проверяется уже фактический машинный код.
Таким образом, результат относится не к абстрактному описанию языка, а к конкретному коду, который создал компилятор.
Зачем проверять все уровни оптимизации
Один и тот же исходный текст может приводить к разному машинному коду в зависимости от выбранного уровня оптимизации.
В простом режиме компилятор старается сохранить максимально прямую связь между исходной программой и результатом генерации. На более высоких уровнях он может удалять лишние инструкции, менять распределение значений по регистрам, исключать недостижимый код и выполнять другие преобразования.
При этом смысл программы должен сохраняться.
Поэтому формальный контракт проверяется не один раз. Для одного и того же требования отдельно создаются и проверяются машинные объекты, полученные на O0, O1, O2, O3 и O4.
Это позволяет проверять не только отдельную конструкцию языка, но и то, сохранил ли компилятор её поведение после оптимизации.
Что вошло в покрытие
В первый набор вошли арифметические операции и сочетания целочисленных типов i8, u8, i16, u16, i32 и u32. Для операций, где типы левого и правого операндов могут различаться, проверяется матрица сочетаний 6×6.
Отдельно проверяются обычные сравнения и машинная операция CMP, побитовые и логические операции, сдвиги, составные присваивания, а также префиксные и постфиксные инкременты и декременты.
Значительная часть работы связана с узкими типами. Для них важно не только получить правильное арифметическое значение, но и корректно записать его обратно в память, не изменив соседние данные.
В свежем расширении доказательной проверки были закрыты все 36 сочетаний типов для смешанного умножения. Также добавлены проверки составных записей и инкрементов узких значений в локальных массивах, упакованных полях, глобальных переменных и глобальных массивах.
Для массивов дополнительно проверяется сохранность соседних элементов.
System Bus как отдельная область
В SJS-REQ-001 также включена переносимая область System Bus, ограниченная устройством SB_ECHO.
Это важно с точки зрения границ доказательства. Мы не заявляем, что все процессорозависимые команды System Bus уже входят в формально проверенное покрытие.
В текущем требовании проверяется только явно обозначенная переносимая область. Остальные команды остаются за пределами этого требования и должны получать собственные формальные условия, если будут включаться в доказательную базу.
Такой подход позволяет не смешивать подтверждённое поведение с тем, что пока только реализовано или протестировано.
Почему получилось 225 пакетов
Каждый пакет SJP относится к конкретной комбинации исходной программы, формального контракта, результата компиляции и уровня оптимизации.
После успешной проверки создаётся отдельный SJP, который связывается с точными входными данными и инструментами. Поэтому доказательная база состоит не из одного общего отчёта, а из большого количества независимых результатов.
Для SJS-REQ-001 таких пакетов получилось 225.
Их количество само по себе не является показателем качества. Важнее то, что каждый пакет связан с конкретным требованием и может быть проверен повторно.
Повторная проверка результатов
Все 225 SJP прошли повторную проверку.
Для каждого результата сохраняются контрольные суммы исходной программы, контракта, машинного объекта и самого доказательного пакета. Также фиксируются версии компилятора и проверяющего инструмента.
Это необходимо для того, чтобы результат можно было связать с конкретной версией системы.
Если изменяется исходная программа, компилятор, уровень оптимизации или сам проверяющий инструмент, старый результат нельзя автоматически считать действующим для новой версии. Проверку нужно выполнить заново.
Именно поэтому мы рассматриваем формальную верификацию как постоянно воспроизводимый процесс, а не как одноразовый отчёт.
Что показывает этот результат
225 успешных пакетов означают, что соответствующие машинные объекты удовлетворяют своим формальным контрактам в рамках заданных предусловий и используемой модели.
Из этого нельзя делать вывод, что весь компилятор Sekura JS полностью доказан.
Не все конструкции языка входят в SJS-REQ-001. Не все свойства памяти, системного окружения и аппаратной платформы автоматически следуют из этих проверок.
Но теперь есть конкретная и измеримая область, для которой можно показать исходные программы, требования, результаты компиляции и доказательные пакеты.
Это значительно точнее, чем общее утверждение о качестве компилятора.
Публичный репозиторий результатов
Следующий важный шаг — сделать доказательную базу доступной для независимого изучения.
Предполагается открыть публичный репозиторий в GitLab, где будут размещаться исходные программы SJS, формальные контракты SJV, результаты компиляции, SJP-пакеты, контрольные суммы, сведения о версиях инструментов и другие материалы, необходимые для повторной проверки.
Репозиторий планируется публиковать под лицензией Apache License 2.0.
Идея здесь проста: если результат формальной проверки нельзя независимо изучить и повторить, его ценность как инженерного доказательства ограничена.
Открытый набор артефактов позволит другим разработчикам посмотреть, какое именно свойство проверялось, какой машинный код был получен и каким результатом завершилась проверка.
Зачем делать доказательную базу открытой
Формальная проверка особенно полезна тогда, когда её результат можно проверить независимо от автора.
Открытый репозиторий позволяет отделить утверждение разработчика от самих материалов. Вместо фразы «мы проверили компилятор» появляется возможность показать конкретное требование, конкретный исходный код, конкретный SOBJ и соответствующий ему SJP.
Это также упрощает повторную проверку новых версий.
Если компилятор изменился, можно заново собрать тот же набор исходных программ, получить новые машинные объекты и сравнить результаты с предыдущей версией.
Постепенно такая база может стать историей развития формально проверенного покрытия Sekura JS.
Что дальше
SJS-REQ-001 — только первый крупный профиль.
Следующие требования должны расширять область покрытия языка и системных возможностей. Новые конструкции будут добавляться не просто как тесты, а как отдельные свойства с формальными контрактами и воспроизводимыми результатами.
Главная цель на этом этапе не в максимальном количестве доказательных пакетов.
Гораздо важнее построить процесс, при котором для каждой версии компилятора можно точно показать, какие свойства уже подтверждены, на каких уровнях оптимизации они проверялись и где находятся артефакты, позволяющие повторить результат.
225 SJP-пакетов — первый крупный результат такого подхода.
Share
