Leo: Язык программирования для формально верифицированных приложений с нулевым разглашением

Децентрализованные реестры, поддерживающие сложные приложения, сталкиваются с тремя фундаментальными проблемами: ограниченные вычислительные среды, отсутствие конфиденциальности и слабые гарантии корректности и безопасности. Aleo представляет Leo — новый язык программирования, разработанный для создания формально верифицированных приложений с нулевым разглашением (ZK-приложений). Leo не только обеспечивает конфиденциальность и устраняет риски, связанные с майнерской экстракцией стоимости (MEV), но и предоставляет два ключевых свойства: корректность на этапе построения и верифицируемые вычисления. Это первый язык, который интегрирует в себе тестовый фреймворк, реестр пакетов, формальное определение языка и систему автоматического доказательства теорем для ZK-приложений общего назначения.

1. Введение: проблемы современных децентрализованных систем

1.1. Проблема масштабируемости

В таких системах, как Bitcoin и Ethereum, каждый майнер должен повторно выполнить каждую транзакцию для проверки её корректности. Это приводит к:

• Высоким затратам ресурсов и ограниченной пропускной способности.
• Дилемме верификатора: экономическая нецелесообразность проверки сложных транзакций.
• Ограниченной выразительности: приложения работают в средах с ограниченным временем выполнения, размером стека и набором инструкций.

1.2. Проблема конфиденциальности

Публичная природа реестров приводит к:

• Раскрытию финансовой информации и нарушению принципа взаимозаменяемости (fungibility).
• Фронтраннингу атакам и нестабильности консенсуса из-за MEV.

1.3. Проблема аудируемости

ZK-SNARKs — мощный инструмент для обеспечения конфиденциальности и целостности, но их применение сопряжено с трудностями:

• Сложность разработки: требуется экспертиза в криптографии и низкоуровневом представлении схем.
• Слабые гарантии корректности: ошибки в реализации схем приводят к критическим уязвимостям.

2. Leo: Подход к решению проблем

Leo — это статически типизированный функциональный язык программирования, предназначенный для написания ZK-приложений. Его компилятор одновременно достигает двух фундаментальных свойств:

1. Корректность на этапе построения (Correct-by-construction) Скомпилированная программа может быть формально верифицирована относительно своей высокоуровневой спецификации. Компилятор генерирует доказательство семантической эквивалентности между исходным кодом на Leo и выходной R1CS-схемой.
2. Верифицируемые вычисления (Verifiable computation) Выполнение скомпилированной программы производит неинтерактивное zero-knowledge доказательство (zkSNARK), которое может быть быстро проверено кем угодно, независимо от объёма вычислений.

2.1. Ключевые свойства языка

• Композируемость: Функции из разных скомпилированных программ могут комбинироваться для создания новых программ.
• Разрешимость: Leo является Тьюринг-неполным, что гарантирует завершаемость программ, безопасность по времени и памяти. Это позволяет статически анализировать весь граф вызовов и обнаруживать ошибки на этапе компиляции.
• Универсальность: Leo является универсальным компилятором, способным эффективно генерировать общедоступные параметры (public parameters) для скомпилированной программы без необходимости проведения криптографических церемоний.

Конфиденциальность по умолчанию: В Leo приложения по умолчанию являются приватными, что расширяет класс приложений для децентрализованных реестров и защищает от MEV.

Удалённая компиляция: Пользователь может делегировать дорогостоящие вычисления (генерацию доказательства) недоверенной стороне, а затем быстро и дёшево верифицировать корректность результата.

3. Дизайн языка Leo

3.1. Синтаксис и система типов

Leo имеет знакомый синтаксис, похожий на Rust. Его система типов включает:

• Скалярные типы: bool, целые числа со знаком и без (i8/u8, ..., i128/u128), address, field (элементы поля), group (точки эллиптической кривой).
• Агрегатные типы: кортежи (T1, T2), массивы [T; N], и схемы (circuits).

Схемы — это аналоги классов в ООП. Они содержают переменные-члены и функции-члены. Функции могут быть как методами схем, так и независимыми функциями верхнего уровня.

leo

// Пример объявления схемы в Leo
circuit Point {
    x: i32,
    y: i32,

    function new(x: i32, y: i32) -> Self {
        return Self { x, y };
    }
}

3.2. Статическая семантика: От исходного кода к R1CS

Компиляция в Leo — это многоэтапный процесс трансформации и проверок:

1. Канонизация: Упрощение AST, замена синтаксического сахара (например, Self на имя схемы) для последующей обработки.
2. Проверка и вывод типов: Каждое выражение получает строгий тип. Неявное приведение типов запрещено. Компилятор выводит типы для литералов и переменных, где это возможно.
3. Оптимизации:

• Свёртка констант: Вычисление выражений с константами на этапе компиляции.
• Раскрутка циклов: Все циклы должны быть ограничены и раскручены статически.
• Встраивание функций: Все вызовы функций должны быть встроены, что требует статической ограниченности рекурсии.

Эти этапы подготавливают программу к “сплющиванию” в плоскую структуру R1CS.

3.3. R1CS-семантика

Конечная цель компиляции — преобразование программы Leo в систему ранговых ограничений 1-го порядка (R1CS). R1CS представляет собой набор квадратичных ограничений над переменными, которые должны выполняться для корректного вычисления.

Математически, если динамическая семантика Leo определяет функцию y = F(x), то R1CS-семантика определяет отношение R(x, y, a), где a — вспомогательные переменные. Корректность компиляции выражается как: ∀x,y. [y = F(x)] ⇔ [∃a. R(x, y, a)]

Это означает, что R1CS-схема представляет все и только те вычисления, которые описываются исходным кодом на Leo.

4. Дизайн компилятора Leo: Формальная верификация на каждом шаге

Архитектура компилятора представляет собой конвейер фаз, преобразующих исходный код в R1CS. Уникальность подхода Leo — в верифицирующей компиляции (verifying compilation).

• Верифицирующий компилятор vs. Верифицированный компилятор:
• Верифицированный компилятор (например, CompCert) один раз доказывает, что сам компилятор всегда работает корректно.
• Верифицирующий компилятор генерирует доказательство семантической эквивалентности для каждого запуска компиляции конкретной программы.

4.1. Генерация доказательств

Каждая фаза компилятора (парсинг, канонизация, проверка типов и т.д.) не только выполняет преобразование, но и генерирует машиночитаемое доказательство своей корректности. Эти доказательства проверяются с помощью теоретико-доказательной системы ACL2, в которой формализованы синтаксис и семантика Leo.

Доказательства для отдельных фаз объединяются в сквозное (end-to-end) доказательство того, что итоговая R1CS-схема семантически эквивалентна исходному коду на Leo.

4.2. Фазы компилятора

1. Парсинг: Преобразование текста в AST на основе формальной ABNF-грамматики.
2. Преобразование в ASG: AST преобразуется в Абстрактный Семантический Граф (ASG), который содержит информацию об областях видимости и контексте типов.
3. Канонизация, проверка типов, оптимизации: Выполняются этапы, описанные в статической семантике.
4. Синтез схемы: ASG транслируется в R1CS с использованием библиотеки R1-гаджетов. Каждой языковой конструкции (например, оператору + или типу u8) ставится в соответствие предопределённый набор ограничений.

5. Инструменты разработчика и экосистема

Leo предоставляет полный набор инструментов для удобной разработки:

• Тестовый фреймворк: Поддержка модульного и интеграционного тестирования с аннотацией @test, утверждениями (console.assert) и логированием.
• Реестр пакетов: Первый в мире реестр для ZK-схем. Разработчики могут публиковать и использовать библиотеки схем, что способствует повторному использованию кода и предотвращает “раздувание” транзакций.
• Резолвер импорта: Позволяет импортировать функции и схемы из других файлов и пакетов.

6. Оценка и примеры

В документе представлены три примера программ на Leo, демонстрирующие выразительность языка:

1. Хэш Педерсена: Криптографическая хэш-функция на группах.
2. Сортировка пузырьком: Классический алгоритм, показывающий работу с массивами и циклами.
3. Линейная регрессия по методу наименьших квадратов: Пример более сложного алгоритма машинного обучения.

Оценка производительности компилятора показывает, что основное время занимает фаза синтеза R1CS-схемы, в то время как ранние фазы (парсинг, анализ) выполняются быстро.

Также проведена формальная верификация R1-гаджета для хэш-функции Blake2s с использованием инструментария Axe. Это доказывает, что низкоуровневая реализация криптографического примитива соответствует своей формальной спецификации.

7. Ограничения и будущая работа

• Эффективность zkSNARK-проверяющих: Генерация доказательств для больших схем остается дорогой операцией, требующей исследований в области аппаратного ускорения (GPU, FPGA) и распределённых вычислений.
• Масштабируемость теоретико-доказательных систем: Необходимы улучшения в скорости и автоматизации таких систем, как ACL2.

Направления будущего развития:

• Оптимизация R1CS на уровне ограничений.
• Внедрение символьного выполнения для статического выявления ошибок (переполнение, выход за границы массива).
• Развитие форматов сериализации для состояний приложений и R1CS-схем.

Заключение

Leo представляет собой значительный шаг вперёд в области программирования для децентрализованных систем. Он объединяет в себе мощь zero-knowledge доказательств и строгость формальных методов, предлагая разработчикам привычную среду для создания безопасных, корректных и приватных приложений. Подход с верифицирующей компиляцией обеспечивает беспрецедентный уровень доверия к скомпилированным ZK-схемам. Несмотря на существующие ограничения в производительности, Leo закладывает основу для следующего поколения доверенных и масштабируемых децентрализованных приложений.