Погружение в Core Solidity. Часть 5

SAIL, десахаризация и стандартная библиотека

Помимо расширения поверхностного языка, переход на Core Solidity также введёт новый промежуточный язык среднего уровня, доступный пользователям: SAIL (Solidity Algebraic Intermediate Language — Алгебраический промежуточный язык Solidity). Это и есть «ядро» Core Solidity. SAIL представляет собой максимально упрощённый язык, на котором можно выразить всё разнообразие высокоуровневых конструкций, присутствующих в классической Solidity. Он состоит из следующих примитивных конструкций:

- Функции
- Контракты
- Блоки ассемблера (Yul)
- Объявление и присваивание переменных SAIL
- Выражение условного ветвления с коротким замыканием (if-then-else)
- Алгебраические типы данных и сопоставление с образцом
- Классы типов (type classes)
- Обобщения (generics)

Переменная SAIL концептуально похожа на переменную Yul: компилятор связывает её с ячейкой в стеке EVM. В SAIL существует единственный встроенный тип (word), диапазон значений которого совпадает с типами bytes32 или uint256 в классической Solidity и который семантически можно рассматривать как тип, соответствующий одному слоту стека EVM. Контракты в SAIL крайне низкоуровневы — по сути, это просто точки входа времени выполнения и инициализационного кода (initcode).

Хотя в текущей реализации SAIL используется Yul в качестве языка ассемблера, с теоретической точки зрения этот выбор в значительной степени произволен, и вместо него можно было бы использовать, например, ассемблер на основе RISC-V.

Мы уверены, что SAIL достаточно выразителен, чтобы реализовать все высокоуровневые функции и типы языка как комбинацию определений из стандартной библиотеки и проходов десахаризации — то есть синтаксических преобразований времени компиляции в примитивы SAIL. Core Solidity, таким образом, представляет собой SAIL, дополненный дополнительным «синтаксическим сахаром» и библиотеками. Он схож с Yul в своей двойной роли как промежуточного представления компилятора и низкоуровневого языка, доступного пользователю, и все примитивы SAIL будут непосредственно доступны при написании кода на Core Solidity. Подобный подход к построению языков широко применяется в других областях, требующих высокой надёжности (например, в системах автоматического доказательства теорем), и, по нашему мнению, он приносит существенные преимущества как для пользователей языка, так и для безопасности и корректности его реализации.

Мы ожидаем, что сможем создать исполняемую формальную семантику для SAIL. Это позволит нам математически гарантировать ключевые свойства системы типов Solidity, предоставить эталонную реализацию для дифференциального фаззинга, а также формально верифицировать как стандартную библиотеку, так и высокоуровневые языковые конструкции. Мы считаем, что это станет неотъемлемой частью нашей общей стратегии обеспечения корректности, особенно по мере роста сложности языка и масштабов систем, создаваемых с его помощью.

Авторы библиотек получат практически ту же выразительную мощность, что и разработчики языка, и смогут создавать абстракции, ощущающиеся как встроенные в сам язык («язык на основе библиотек»). Появится возможность определять и использовать альтернативные реализации стандартной библиотеки или полностью отключать стандартную библиотеку. При отключённой стандартной библиотеке можно будет писать код на Core Solidity с почти таким же уровнем контроля, как при использовании низкоуровневых ассемблерных языков вроде Yul или Huff, но при этом с современной и выразительной системой типов, основанной на математически строгих принципах.