The post has been translated automatically. Original language: Russian
Formal verification makes sense only when it helps to find real errors, and not just confirms the expected result in advance.
This week, SJV just discovered such an error in the Sekura JS compiler.
One of the test examples used a global variable of type u32. The program was supposed to add the passed value to it. At the source text level, everything looked simple: a simple arithmetic operation on an integer.
But the compiler mistakenly interpreted this variable as a pointer.
Because of this, the count + value operation turned into machine code with different semantics: the passed value was actually scaled the way it is done with pointer arithmetic.
A normal test could easily miss such an error if the selected values did not randomly show a discrepancy.
SJV did not check a single example, but the compliance of the executable program with a given contract. The contract required a specific relationship between the state before the function was called and the state after it was completed.
And this is where the contradiction arose.
The check showed that the machine code does not satisfy the specified property. After analyzing the cause, the error was found already in the compiler and fixed.
For us, this case is not important for the specific error itself.
It shows why we separated the creation of the program and its verification.
The compiler may be wrong. The programmer may be wrong. The code created by artificial intelligence may also contain an error.
Therefore, reliability cannot be built solely on trust in the one who created the program.
We need a separate mechanism that checks: the resulting program really does what is required of it.
Формальная верификация имеет смысл только тогда, когда помогает находить реальные ошибки, а не просто подтверждает заранее ожидаемый результат.
На этой неделе SJV как раз обнаружила такую ошибку в компиляторе Sekura JS.
В одном из проверочных примеров использовалась глобальная переменная типа u32. Программа должна была прибавить к ней переданное значение. На уровне исходного текста всё выглядело просто: обычная арифметическая операция над целым числом.
Но компилятор ошибочно трактовал эту переменную как указатель.
Из-за этого операция count + value превращалась в машинный код с другой семантикой: переданное значение фактически масштабировалось так, как это делается при арифметике указателей.
Обычный тест мог легко пропустить такую ошибку, если выбранные значения случайно не проявляли расхождение.
SJV проверяла не отдельный пример, а соответствие исполняемой программы заданному контракту. Контракт требовал конкретного отношения между состоянием до вызова функции и состоянием после её завершения.
И именно здесь возникло противоречие.
Проверка показала, что машинный код не удовлетворяет заданному свойству. После разбора причины ошибка была найдена уже в компиляторе и исправлена.
Для нас этот случай важен не самой конкретной ошибкой.
Он показывает, зачем мы разделили создание программы и её проверку.
Компилятор может ошибаться. Программист может ошибаться. Код, созданный искусственным интеллектом, тоже может содержать ошибку.
Поэтому надёжность нельзя строить только на доверии к тому, кто создал программу.
Нужен отдельный механизм, который проверяет: получившаяся программа действительно делает то, что от неё требуется.
Share
