The post has been translated automatically. Original language: Russian
In Sekura JS, the next stage of formal verification of compilation results has been completed — the SJS-REQ-002 requirement, dedicated to comparison operations and control constructs of the language.
Six separate behavior profiles have been prepared for this test. Each of them contains the source code for Sekura JS and a permanent formal description of SJV. For optimization levels from O0 to O4, programs are compiled into machine objects, after which their behavior is checked relative to the specified requirements.
The current result is 30 SJP proof packages that have successfully passed formal verification and re—verification of the signature and content.
These are six profiles that have been tested at five optimization levels.
What was included in the verification
SJS-REQ-002 covers several groups of language constructs.
The first group is comparison operations. All six basic comparisons for signed and unsigned 32-bit values have been tested, as well as individual cases of mixed signed and unsigned comparisons, zero comparisons, and boundary values for narrow integer types.
The second group is conditional constructions. The behavior of the if(x) condition has been verified by the zero or non-zero rule for signed and unsigned values, as well as if/else constructions, else if chains, and nested branches.
A separate set of checks is devoted to cycles, early exit from them, and the switch design.
Checking cycles
Counting and summation scenarios have been prepared for while and for. The formal condition uses the constraint n <= 3.
It is important that this does not mean checking multiple selected values of n. The formal system considers all valid input values within a given range and must confirm the final condition for each achievable execution path.
The check is performed directly on the SOBJ machine object. The SJV tool symbolically traverses possible paths inside loops and verifies the result of a function relative to a given formal condition.
Thus, for the region n <= 3, the entire specified range is checked, and not a set of test cases.
Break, continue, and early return
The control structures that change the normal course of the cycle are checked separately.
The coverage includes break, continue, exit via break from a nested loop, and early return from a function.
For such constructions, it is especially important to check not only the final numeric value, but also which execution path was actually selected after compilation.
The machine code may differ at different optimization levels, but the formally defined behavior must be preserved.
Checking the switch
SJS-REQ-002 formally covers the switch design in an explicitly defined area.
The selection of a matching case, several case variants, the default branch, an explicit break, and the absence of executing the next statement after completing the selected branch were checked.
In other words, the current result confirms the switch behavior for branches with an explicit break.
Only the transition from one case to the next without a break is not included in this check. This option should be checked separately if it is included in the next coverage area.
The goto construction is also not included in SJS-REQ-002.
Why are O0–O4 checked?
The same Sekura JS program is compiled separately for optimization levels O0, O1, O2, O3, and O4.
At each level, the machine code may be different. The compiler can change the sequence of instructions, work with registers, and the structure of transitions.
The formal requirement remains the same.
Therefore, all six profiles are checked separately at each optimization level. As a result, 30 independent SJP packets were generated for SJS-REQ-002.
This approach allows you to check the persistence of behavior not only in the basic compilation mode, but also after optimizing transformations.
How are cycles checked?
Symbolic execution has finite technical limits.
The current implementation limits the number of visits to a single machine instruction, the total number of steps on a single execution path, and the size of the symbolic expression.
These limits are not used as part of the proof.
If the verifier reaches an internal constraint and there remains a possible execution path corresponding to the initial conditions of the function, the result is not considered successful. Such verification gets the status of unsupported, rather than formally proven.
For the current SJS-REQ-002 examples, all loops terminate inside the supported symbolic execution area.
The constraint parameters are stored in evidence packages so that the verification boundaries remain explicit.
What does the result mean?
All 30 SJP packages contain a confirmed functional result and are successfully retested.
This means that the machine objects created by the compiler for the specified programs and optimization levels meet their formal conditions within the specified prerequisites.
SJS-REQ-002 confirms comparison operations, conditional constructions, loops in the declared area, break, continue, early return, nested break and switch with explicit break.
Beyond this requirement, there are goto, the transition between switch branches without a break, as well as properties that were not checked here at all: general memory safety, MMU operation, stack, and calling convention.
This is not a limitation of the evidence already obtained, but the exact boundary of what is included in SJS-REQ-002.
Reproducibility
For each optimization level, machine objects, character descriptions, signed SJP packets, and re-validation logs are saved.
The versions of the tools used and the checksums of the input and output files are also recorded.
The complete SJS-REQ-002 matrix can be retrieved automatically by running the appropriate verification script. This allows us to consider the result not as a one-time report, but as a reproducible part of the evidence base of a particular version of the compiler.
The next stage
SJS-REQ-002 closes another major area of the language: comparisons, conditions, loops, and basic execution control constructs.
Further work will be continued according to the following requirements of Sekura JS. Each of them should expand the formally verified coverage of the language and compiler without blurring the boundaries of the results already obtained.
After completing the entire planned set of checks, we will separately publish the overall result: which compiler properties have been confirmed, which optimization levels have been covered, and how much evidence has been generated by this point.
So far, the result of SJS-REQ-002 can be formulated precisely: 30 machine compilation results for six behavior profiles and five optimization levels were formally and re-checked within the stated conditions.
В Sekura JS завершён следующий этап формальной проверки результатов компиляции — требование SJS-REQ-002, посвящённое операциям сравнения и управляющим конструкциям языка.
Для этой проверки подготовлено шесть отдельных профилей поведения. Каждый из них содержит исходную программу на Sekura JS и постоянное формальное описание SJV. Для уровней оптимизации от O0 до O4 программы компилируются в машинные объекты, после чего их поведение проверяется относительно заданных требований.
Текущий результат — 30 доказательных пакетов SJP, успешно прошедших формальную проверку и повторную проверку подписи и содержимого.
Это шесть профилей, проверенных на пяти уровнях оптимизации.
Что вошло в проверку
SJS-REQ-002 охватывает несколько групп конструкций языка.
Первая группа — операции сравнения. Проверены все шесть основных сравнений для знаковых и беззнаковых 32-разрядных значений, а также отдельные случаи смешанного знакового и беззнакового сравнения, сравнения с нулём и граничные значения для узких целочисленных типов.
Вторая группа — условные конструкции. Проверено поведение условия if (x) по правилу ноль или неноль для знаковых и беззнаковых значений, а также конструкции if/else, цепочки else if и вложенные ветвления.
Отдельный набор проверок посвящён циклам, досрочному выходу из них и конструкции switch.
Проверка циклов
Для while и for подготовлены сценарии подсчёта и суммирования. В формальном условии используется ограничение n <= 3.
Важно, что это не означает проверку нескольких выбранных значений n. Формальная система рассматривает все допустимые входные значения внутри заданной области и должна подтвердить итоговое условие для каждого достижимого пути выполнения.
Проверка выполняется непосредственно по машинному объекту SOBJ. Средство SJV символически проходит возможные пути внутри циклов и проверяет результат функции относительно заданного формального условия.
Таким образом, для области n <= 3 проверяется весь заданный диапазон, а не набор тестовых примеров.
Break, continue и досрочный return
Отдельно проверены управляющие конструкции, которые изменяют обычный ход выполнения цикла.
В покрытие вошли break, continue, выход через break из вложенного цикла и досрочный return из функции.
Для таких конструкций особенно важно проверять не только конечное числовое значение, но и то, какой путь выполнения фактически был выбран после компиляции.
Машинный код может отличаться на разных уровнях оптимизации, но формально заданное поведение должно сохраняться.
Проверка switch
SJS-REQ-002 формально покрывает конструкцию switch в явно заданной области.
Проверены выбор совпавшего case, несколько вариантов case, ветвь default, явный break и отсутствие выполнения следующего оператора после завершения выбранной ветви.
То есть текущий результат подтверждает поведение switch для ветвей с явным break.
Не входит в эту проверку только переход из одного case в следующий без break. Такой вариант должен проверяться отдельно, если будет включён в следующую область покрытия.
Конструкция goto в SJS-REQ-002 также не входит.
Почему проверяются O0–O4
Одна и та же программа на Sekura JS компилируется отдельно для уровней оптимизации O0, O1, O2, O3 и O4.
На каждом уровне машинный код может отличаться. Компилятор может менять последовательность инструкций, работу с регистрами и структуру переходов.
Формальное требование при этом остаётся прежним.
Поэтому все шесть профилей проверяются отдельно на каждом уровне оптимизации. В результате для SJS-REQ-002 сформировано 30 независимых SJP-пакетов.
Такой подход позволяет проверять сохранение поведения не только в базовом режиме компиляции, но и после оптимизирующих преобразований.
Как проверяются циклы
Символическое выполнение имеет конечные технические пределы.
В текущей реализации ограничено количество посещений одной машинной инструкции, общее количество шагов на одном пути выполнения и размер символического выражения.
Эти пределы не используются как часть доказательства.
Если проверяющий достигает внутреннего ограничения и при этом остаётся возможный путь выполнения, соответствующий исходным условиям функции, результат не считается успешным. Такая проверка получает статус неподдерживаемой, а не формально доказанной.
Для текущих примеров SJS-REQ-002 все циклы завершаются внутри поддерживаемой области символического выполнения.
Параметры ограничений сохраняются в доказательных пакетах, чтобы границы проверки оставались явными.
Что означает полученный результат
Все 30 SJP-пакетов содержат подтверждённый функциональный результат и успешно проходят повторную проверку.
Это означает, что машинные объекты, созданные компилятором для заданных программ и уровней оптимизации, соответствуют своим формальным условиям в пределах указанных предусловий.
SJS-REQ-002 подтверждает операции сравнения, условные конструкции, циклы в заявленной области, break, continue, досрочный return, вложенный break и switch с явным break.
За пределами этого требования остаются goto, переход между ветвями switch без break, а также свойства, которые здесь вообще не проверялись: общая безопасность памяти, работа MMU, стек и соглашение о вызовах.
Это не ограничение уже полученных доказательств, а точная граница того, что входит в SJS-REQ-002.
Воспроизводимость
Для каждого уровня оптимизации сохраняются машинные объекты, описания символов, подписанные SJP-пакеты и журналы повторной проверки.
Также фиксируются версии используемых инструментов и контрольные суммы входных и выходных файлов.
Полную матрицу SJS-REQ-002 можно повторно получить автоматическим запуском соответствующего сценария проверки. Это позволяет рассматривать результат не как разовый отчёт, а как воспроизводимую часть доказательной базы конкретной версии компилятора.
Следующий этап
SJS-REQ-002 закрывает ещё одну крупную область языка: сравнения, условия, циклы и основные конструкции управления выполнением.
Дальше работа будет продолжена по следующим требованиям Sekura JS. Каждое из них должно расширять формально проверенное покрытие языка и компилятора без размывания границ уже полученных результатов.
После завершения всего запланированного набора проверок мы отдельно опубликуем общий итог: какие свойства компилятора подтверждены, какие уровни оптимизации охвачены и какой объём доказательной базы сформирован к этому моменту.
Пока результат SJS-REQ-002 можно сформулировать точно: 30 машинных результатов компиляции по шести профилям поведения и пяти уровням оптимизации прошли формальную и повторную проверку в пределах заявленных условий.
Share
