The post has been translated automatically. Original language: Russian
The Assurance Sekura JS project has prepared the first partial evidence base for the Sekura JS programming language. It relates the requirements for the behavior of a language to specific programs, the results of their compilation, and formal checks.
This is the initial stage: individual properties have now been proven under explicitly specified conditions. Further, the verification area will gradually expand from basic operations to more complex structures and their interaction.
What does it mean to "prove a property of a program"?
Normal testing checks the program on the selected input data. For example, you can pass several pairs of numbers to the addition function and compare the answers with the expected ones.
A formal check allows us to raise a more general question: is there at least one among all acceptable input values in which the program violates the specified condition?
To do this, the behavior of the program is described mathematically. The verifier checks whether there may be a violation of the contract — a formal statement about the result or the state of the program. If the violation is impossible within the framework of the model and the specified conditions, the property is considered proven.
This result can cover all the values of arguments of certain types. At the same time, it refers to a specific program and a specific property: the boundaries of the proof must always be marked.
How Assurance Sekura JS works
The project is based on a sequential chain:
Requirement → source program → compilation result → formal verification → proof package.
The Sekura JS program is compiled into a machine object. A separate specification defines acceptable input conditions and expected behavior. The SJV verifier then verifies these statements for the compiled object.
This is important because the check concerns the result of the compiler. Even a properly written source code may behave incorrectly if an error occurs during compilation.
A contract may state, for example, that a function returns the sum of arguments, that writing to one field of a structure preserves an adjacent field, or that a local variable remains valid after calling another function.
Verification materials are stored for each result: source code, specification, compiled object, proof package, and tool logs.
What is already being checked
The first stage covers several basic areas of the language.
Formal profiles of operations, combinations of types, transformations, and storage of values of different bit sizes have been prepared for integer arithmetic.
In flow control, comparisons, conditional transitions, selected loop scenarios, exits from them, and returns from functions are checked.
For functions, parameters, return values, local variables, and individual call and stack properties are considered.
When working with memory, selected operations with arrays, structures, and pointers are checked, including saving neighboring elements when writing.
Modular mechanisms and interaction with the execution environment have so far been confirmed by test scenarios. These results are taken into account separately and are not designated as formal proofs.
The selected programs are checked at optimization levels O0–O4. Each compilation result is considered separately, which allows you to confirm the declared properties with different compiler settings.
Why is the proof so far partial?
The programming language allows for a huge number of programs and combinations of constructions. Therefore, the first evidence base is built around limited tasks with clear conditions.
For example, some arithmetic examples of loops are checked under the condition n <= 3. All valid inputs and achievable paths represented by the model are considered within this area. This is the finished result for a given range, which can be further expanded.
A similar approach applies to memory and function calls. In some profiles, several aspects of behavior are already being tested, while in others, only the functional result is being tested.
Such restrictions allow you to accurately see the current state of work: which properties have been confirmed, under what assumptions, and which questions are still open.
Why save evidence materials
For engineering applications, not only the final status of the check is important, but also the ability to determine what exactly it refers to.
Assurance Sekura JS saves information about tool versions and file checksums. They link the report to the exact source data and compilation results. Package signatures allow you to verify their origin and integrity, and re—checking saved mathematical queries ensures reproducibility of the solver's results.
At the same time, formal verification also has a basis of trust: the correctness of the execution model and the verifier itself. These components require attention as the project progresses.
How will the work develop
Further expansion involves adding new properties and scenarios, increasing the allowable input data areas, and removing current restrictions.
A separate area is the interaction of language constructs: arithmetic within loops, function calls with memory changes, and the operation of several modules. Verification of such combinations is necessary, since the proof of individual examples does not yet establish the correctness of their arbitrary combination.
As development progresses, a more general rationale for the relationship between language semantics, validation model, and machine execution will be required.
The first stage is already creating a practical basis for this work. Each subsequent extension will have a specific result: a new proven property, a wider range of acceptable conditions, or a closed question about the behavior of the program.
The project materials are available in the Assurance Sekura JS repository.
В проекте Assurance Sekura JS подготовлена первая частичная доказательная база для языка программирования Sekura JS. Она связывает требования к поведению языка с конкретными программами, результатами их компиляции и формальными проверками.
Это начальный этап: сейчас доказаны отдельные свойства в явно заданных условиях. Дальше область проверки будет постепенно расширяться — от базовых операций к более сложным конструкциям и их взаимодействию.
Что означает «доказать свойство программы»
Обычное тестирование проверяет программу на выбранных входных данных. Например, можно передать функции сложения несколько пар чисел и сравнить ответы с ожидаемыми.
Формальная проверка позволяет поставить более общий вопрос: существует ли среди всех допустимых входных значений хотя бы одно, при котором программа нарушит заданное условие?
Для этого поведение программы описывается математически. Верификатор проверяет, может ли возникнуть нарушение контракта — формального утверждения о результате или состоянии программы. Если нарушение невозможно в рамках модели и заданных условий, свойство считается доказанным.
Такой результат может охватывать все значения аргументов определённых типов. При этом он относится к конкретной программе и конкретному свойству: границы доказательства всегда должны быть обозначены.
Как устроен Assurance Sekura JS
В основе проекта лежит последовательная цепочка:
Требование → исходная программа → результат компиляции → формальная проверка → пакет доказательства.
Программа на Sekura JS компилируется в машинный объект. Отдельная спецификация задаёт допустимые входные условия и ожидаемое поведение. Затем верификатор SJV проверяет эти утверждения для скомпилированного объекта.
Это важно, поскольку проверка касается результата работы компилятора. Даже правильно написанный исходный код может вести себя неверно, если при компиляции возникла ошибка.
Контракт может утверждать, например, что функция возвращает сумму аргументов, что запись в одно поле структуры сохраняет соседнее поле или что локальная переменная остаётся корректной после вызова другой функции.
Для каждого результата сохраняются материалы проверки: исходный код, спецификация, скомпилированный объект, пакет доказательства и журналы работы инструментов.
Что уже проверяется
Первый этап охватывает несколько базовых областей языка.
Для целочисленной арифметики подготовлены формальные профили операций, сочетаний типов, преобразований и хранения значений разной разрядности.
В управлении потоком проверяются сравнения, условные переходы, выбранные сценарии циклов, выходов из них и возвратов из функций.
Для функций рассматриваются параметры, возвращаемые значения, локальные переменные и отдельные свойства вызовов и стека.
В работе с памятью проверяются выбранные операции с массивами, структурами и указателями, включая сохранение соседних элементов при записи.
Модульные механизмы и взаимодействие со средой исполнения пока подтверждаются тестовыми сценариями. Эти результаты учитываются отдельно и не обозначаются как формальные доказательства.
Выбранные программы проверяются при уровнях оптимизации O0–O4. Каждый результат компиляции рассматривается отдельно, что позволяет подтверждать заявленные свойства при разных настройках компилятора.
Почему доказательство пока частичное
Язык программирования допускает огромное количество программ и сочетаний конструкций. Поэтому первая доказательная база строится вокруг ограниченных задач с понятными условиями.
Например, некоторые арифметические примеры циклов проверяются при условии n <= 3. Внутри этой области рассматриваются все допустимые входы и достижимые пути, представленные моделью. Это законченный результат для заданного диапазона, который в дальнейшем можно расширять.
Аналогичный подход применяется к памяти и вызовам функций. В одних профилях уже проверяется несколько аспектов поведения, в других — только функциональный результат.
Такие ограничения позволяют точно видеть текущее состояние работы: какие свойства подтверждены, при каких предположениях и какие вопросы ещё открыты.
Зачем сохранять доказательные материалы
Для инженерного применения важен не только итоговый статус проверки, но и возможность установить, к чему именно он относится.
Assurance Sekura JS сохраняет сведения о версиях инструментов и контрольные суммы файлов. Они связывают отчёт с точными исходными данными и результатами компиляции. Подписи пакетов позволяют проверять их происхождение и целостность, а повторная проверка сохранённых математических запросов — воспроизводимость результатов решателя.
При этом формальная верификация тоже имеет основание доверия: корректность модели исполнения и самого верификатора. Эти компоненты требуют внимания по мере развития проекта.
Как будет развиваться работа
Дальнейшее расширение предполагает добавление новых свойств и сценариев, увеличение допустимых областей входных данных и снятие текущих ограничений.
Отдельное направление — взаимодействие конструкций языка: арифметика внутри циклов, вызовы функций с изменением памяти, работа нескольких модулей. Проверка таких сочетаний необходима, поскольку доказательство отдельных примеров ещё не устанавливает корректность их произвольной комбинации.
По мере развития потребуется и более общее обоснование связи между семантикой языка, моделью проверки и машинным исполнением.
Первый этап уже создаёт практическую основу для этой работы. У каждого следующего расширения будет конкретный результат: новое доказанное свойство, более широкий диапазон допустимых условий или закрытый вопрос о поведении программы.
Материалы проекта доступны в репозитории Assurance Sekura JS.
Share
