RFC-027：Компиляторные предикаты и унифицированная статическая верификация

См. также:

• RFC-009: Модель владения
• RFC-010: Унифицированный синтаксис типов - модель name: type = value
• RFC-011: Проектирование системы обобщённых типов
• RFC-024：Модель параллелизма на основе блоков spawn

Заменяет: RFC-022: Поддержка статической верификации на основе логики Хоара (аннотации спецификаций и типы спецификаций) — упразднено

Аннотация

В данном документе предлагается ввести в YaoXiang компиляторные предикаты как объекты первого класса, объединив все виды статической компиляторной верификации в единый конвейер доказательств. Компиляторный предикат — это не внешняя аннотация спецификации — это функция. Функция, возвращающая Type, которую можно использовать в позиции типа; компилятор вызывает её во время компиляции и проверяет возвращаемое значение. Тип — это высказывание, компиляция — это доказательство.

Ключевой тезис: единственная задача проверки типов во время компиляции — это конструирование и верификация доказательственных объектов. Типовые равенства, конфликты токенов, редукция зависимых типов, вычисление компиляторных предикатов, импликации в логике Хоара — всё это различные виды проверки типов в едином конвейере доказательств. SMT-решатель — это ускоряющий модуль проверщика типов, а не独立ная граница доверия. Когда компилятор возвращает Unproven, программист пишет функцию на YaoXiang в качестве доказательства — проверщик типов верифицирует её точно так же, как верифицирует тип возврата любой другой функции. Всё — код YaoXiang, всё верифицируется проверщиком типов.

Мотивация

Почему RFC-022 упраздняется?

RFC-022 проектировала спецификации в форме комментариев //!:

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0          ← это независимый от типа комментарий
    //! ensures: ExistsMax(result, arr[0..n])   ← это независимый от типа комментарий
}

Это фундаментальная ошибка в отношении изоморфизма Карри-Ховарда: спецификации и типы разделены на два слоя. Комментарии — не типы. Комментарии не участвуют в проверке типов. Комментарии — это модель мышления для «внешних инструментов».

Белая книга выражается ясно:

«Нет комментариев //!. Нет отдельного языка спецификаций. Всё внутри системы типов».

Текущие проблемы

• Комментарии //! из RFC-022 — это внешний синтаксис, отделённый от системы типов
• Типы спецификаций и обычные типы — два разных механизма, создающие концептуальную избыточность
• Разделение Debug Build верификация / Release Build игнорирование нарушает единство
• В традиционном понимании SMT-решатель позиционируется как внешний инструмент — YaoXiang встраивает его как ускоряющий модуль проверщика типов
• Проверка типов, верификация заимствований, проверка компиляторных предикатов, раскрытие макросов идут разными путями

Правильная модель мышления

Проверка типов может быть абстрагирована как функция:

verify : Program → Proved | Disproved(Model) | Unproven

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

Когда компилятор возвращает Unproven, программист предоставляет доказательственную функцию — тип возврата этой функции равен доказываемому высказыванию. Проверщик типов верифицирует её. Это та же операция, что и обычная проверка типов.

Предложение

1. {} — пространство доказательств: тип — это утверждение, верификация — это проверка типов

{} в YaoXiang — это пространство доказательств времени компиляции. Всё внутри — утверждения, компилятор гарантирует истинность каждого — либо автоматически доказывает, либо программист предоставляет доказательственную функцию.

Point: Type = { x: Float, y: Float }
#               ^^^^^^^^^^^^^^^^^^^^^  компилятор гарантирует, что x — Float, y — Float

List: (T: Type) -> Type = { data: Array(T) }
#                           ^^^^^^^^^^^^^^^  компилятор гарантирует, что data — Array(T)

Обобщённые типы — это частный случай компиляторных предикатов.

Positive: (x: Int) -> Type = { x > 0 }
#          ^^^^^^              ^^^^^^
#          параметр в сигнатуре   внутри {} только утверждение
#          компилятор вызывает при компиляции и верифицирует x > 0

List: (T: Type) -> Type = { data: Array(T) }
#      ^^^^^^^^              ^^^^^^^^^^^^^^^
#      параметр в сигнатуре   компилятор верифицирует type_of(T) == Type, type_of(data) == Array(T)

Единый паттерн: name: (params) -> Type = { утверждения }. Компилятор не различает «типовые утверждения» и «утверждения о значениях» — всё это цели для вычисления в конвейере доказательств.

Инварианты циклов не нужно писать отдельно. Типовые аннотации на переменных — это инварианты Флойда-Хоара.

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # аннотация ссылается на i — сообщает компилятору, что тип s зависит от i
    mut i: UpTo(arr.len) = 0     # при инициализации i=0, верификация: 0 == sum(arr[0..0]) → True
    while i < arr.len {
        s += arr[i]  # компилятор верифицирует: s_new == sum(arr[0..i+1])
        i += 1       # i изменяется → триггер повторной верификации зависимости s: s удовлетворяет SumUpTo(arr, i_new)
    }
    return s  # s: SumUpTo(arr, arr.len) = sum(arr[0..arr.len])
}

Компилятор генерирует для тела цикла одну verification condition — индукционная гипотеза (типовая аннотация) → операция присваивания → удовлетворяет ли новое значение типовая аннотация. После того как конвейер доказательств установит истинность индукционного шага, все итерации автоматически покрываются. Не нужно : decreases, не нужно : Invariant, не нужно индуктивное доказательство — компилятор разлагает индукцию на локальные VC для каждого присваивания.

2. Предусловия/постусловия: компиляторные предикаты в типах параметров и возвращаемого типа

Отказ от //! requires///! ensures из RFC-022. Компиляторные предикаты используются как типы параметров или возвращаемого типа.

Сторона параметров — это вызов функции. Компиляторный предикат — это функция, возвращающая Type, и использование на стороне параметров — это просто её вызов — как factorial(5). На стороне возвращаемого значения появляется новая концепция: параметр возвращаемого значения.

# Предусловие: вызов компиляторного предиката в типе параметра
Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b
#                       ^^^^^^^^^^  b — имя текущего формального параметра, передаётся в Positive как аргумент
#                       компилятор в точке вызова извлекает фактическое значение, подставляет в b, верифицирует Positive(фактическое)
#                       пример: divide(10, 2) → верификация Positive(2) = { 2 > 0 } → True
#                       пример: divide(10, 0) → верификация Positive(0) = { 0 > 0 } → False → ошибка компиляции

# Постусловие: параметр возвращаемого значения + компиляторный предикат
IsMax: (T: Ord, arr: Array(T), result: T) -> Type = {
    forall j in 0..arr.len: result >= arr[j]
}

NonEmpty: (arr: Array(T)) -> Type = { arr.len > 0 }

max: (T: Ord) -> ((arr: NonEmpty(arr))) -> (result: IsMax(T, arr, result)) = {
#                                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
#                                            result — параметр возвращаемого значения, значение предоставляется return
#                                            компилятор в точке return подставляет возвращаемое значение, верифицирует постусловие
    candidate = arr[0]
    for i in 1..arr.len {
        if arr[i] > candidate { candidate = arr[i] }
    }
    return candidate
}

Ключевые правила:

• Сторона параметров: b: Positive(b) —— b — имя текущего формального параметра, передаётся в Positive как аргумент. Синтаксис вызова функции, ноль неявности.
• Сторона возврата: -> (result: IsMax(T, arr, result)) —— result — параметр возвращаемого значения, значение предоставляется оператором return. result существует только в сигнатуре типа, только предикат ссылается на него, не входит в область видимости тела функции, не появляется у вызывающей стороны.
• Параметр возвращаемого значения опционален: без постусловия сигнатура полностью совпадает с обычной функцией (-> Int).
• Единство: параметры и параметры возвращаемого значения — одна концепция — имя_параметра: вызов_предиката(имя_параметра), разница лишь в том, кто предоставляет значение — вызывающая сторона или return.

3. Распространение путевых условий: верификация значений времени выполнения во время компиляции

При использовании компиляторных предикатов в позиции связывания параметры явно передаются программистом. Когда значения времени выполнения попадают в параметры уточнённого типа, компилятор завершает верификацию через collection путевых условий и импликативную проверку SMT — без явной передачи доказательства программистом.

3.1 Явные вызовы функций

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

Positive: (x: Int) -> Type = { x > 0 } — это конструктор компиляторного предиката. Когда он появляется в позиции связывания (объявление параметра, объявление переменной, тип возврата), программист явно передаёт связанное имя переменной:

b: Positive(b)
// b уже объявлен как текущий формальный параметр, Positive(b) — это вызов функции
// после нормализации: b: { b > 0 }

Компилятору не нужно неявно подставлять параметры — b: Positive(b) — это то же самое, что f(5), просто вызов функции. b связывается как имя параметра, его типовая аннотация Positive(b) ссылается на самого b — это стандартный паттерн зависимых типов, не правило неявного раскрытия.

Унификация с self из RFC-010: RFC-010 установила, что self — не ключевое слово, просто договорённость об именовании параметров («написав p, this, x получишь тот же эффект»). b: Positive(b) использует тот же механизм — имя параметра может быть использовано в его типовой аннотации. self появляется в позиции self: Point, b появляется в позиции b: Positive(b), обе типовые аннотации ссылаются на параметр. Разница только в сложности типовой аннотации, механизм полностью идентичен — после связывания имени тип может зависеть от этого имени.

Тип возврата также использует явный вызов функции:

Sorted: (arr: Array(T)) -> Type = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }

sort: (arr: Array(T)) -> (result: Sorted(result)) = { ... }
//                        ^^^^^^^^^^^^^^^^^^^^^^^
//                        result — параметр возвращаемого значения, Sorted(result) — вызов функции
//                        компилятор в точке return подставляет возвращаемое значение в result, верифицирует Sorted(возвращаемое)

Так же применимо к объявлению локальных переменных:

let x: Positive(x) = 5
// x связывается с 5, Positive(5) → { 5 > 0 } → True → проходит

// let y: Positive(y) = 0
// y связывается с 0, Positive(0) → { 0 > 0 } → False → ошибка компиляции

3.2 Сбор путевых условий

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

if y > 0 {
    // компилятор автоматически получает в этой ветке предположение: { y > 0 }
    let result = divide(x, y)
    // Условие верификации: (y > 0) ⇒ (y > 0)
    // Конвейер доказательств判定 импликация成立 → Proved
} else {
    // В этой ветке предположение: { !(y > 0) }
    // Если вызвать divide(x, y), условие верификации !(y > 0) ⇒ y > 0
    // Конвейер доказательств判定 импликация не成立 → Disproved
}

Это не встроенный компилятором особый паттерн — это естественное поведение компиляторного конвейера доказательств. При каждой проверке типа в точке вызова в конвейер отправляется:

{фоновые предположения} ⇒ {цель верификации}

Конвейер доказательств проверяет импликативность. Proved → проходит, Disproved → ошибка компиляции + контрпример, Unproven → ошибка компиляции + недоказанное высказывание. Фоновые предположения происходят из путевых условий текущей точки программы.

3.3 Стек предположений

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

• if-guard: if y > 0 → в true-ветку помещается y > 0, в false-ветку помещается !(y > 0) (если есть else)
• match-паттерн: if let Some(v) = opt → в ветке помещается opt == Some(v)
• Логические связки: if x > 0 && y < 10 → в ветке помещаются x > 0 и y < 10
• Предусловия функций: при вызове divide(a, b), доказательство того, что b удовлетворяет Positive, должно либо происходить из текущих предположений, либо из уточнённого типа самого аргумента (если b уже аннотирован как Positive, его тип несёт b > 0)
• Присваивание: при let z = y, уточнённые условия на y передаются на z

Все предположения попадают в компиляторный конвейер доказательств. При входе на путь с SMT-ускорением они транслируются как фоновые assert'ы в SMT-LIB.

3.4 Без статического доказательства — ошибка компиляции

Если программист напишет напрямую:

divide_user_input: (x: Int, y: Int) -> Int = divide(x, y)

В текущей точке программы нет предположения y > 0, и сам аргумент y не имеет типовой аннотации Positive. Условие верификации:

{} ⇒ { y > 0 }

Конвейер возвращает Disproved (не имплицирует) → ошибка компиляции:

Не удалось доказать, что параметр b удовлетворяет Positive при вызове divide. y происходит из пользовательского ввода, без доказанных границ. Рассмотрите вызов с охранением if-ветки: if y > 0 { divide(x, y) }.

YaoXiang не принимает значения времени выполнения, напрямую попадающие в параметры уточнённого типа без предоставления статического доказательства. Это не ограничение — это ядро философии жёсткой безопасности. Код, который компилятор не может статически доказать, не компилируется.

3.5 Связь с унифицированным конвейером

Распространение путевых условий — это не дополнительный механизм. Это прямое расширение компиляторного конвейера доказательств на анализ потока управления:

Фаза	Ответственность
Сбор путевых условий	Компилятор анализирует поток управления, аннотирует каждый базовый блок множеством предположений
Генерация условий верификации	При встрече типа constraints для верификации, объединяются путевые условия + информация о типах аргументов
Вычисление в конвейере доказательств	Ядро компилятора → SMT-ускорение → результат Proved / Disproved / Unproven
Результат	Proved → проходит; Disproved → ошибка компиляции + контрпример; Unproven → ошибка компиляции + недоказанное высказывание (программист может предоставить доказательственную функцию)

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

4. Компиляторный конвейер доказательств

Все виды компиляторных проверок используют единый конвейер. Ядро конвейера — это проверка типов — проверка того, равен ли тип доказательственного объекта доказываемому высказыванию. Всё — проверка типов.

Компилятор встречает Bool-выражение, требующее вычисления (нужно сконструировать доказательский объект)
        │
        ├── Типовое равенство (T1 == T2)
        │   → компилятор решает напрямую (структурная эквивалентность)
        │
        ├── Условия конфликта токенов (!conflicting(tokens))
        │   → потоково-чувствительный анализ активности (отслеживание атрибутов Dup/Linear)
        │
        ├── Редукция зависимых типов (n + m упрощение)
        │   → система переписывания термов времени компиляции (βδι-редукция)
        │
        ├── Компиляторные предикаты (x > 0, forall...)
        │   → сам компилятор + модуль SMT-ускорения
        │
        └── Импликации в логике Хоара (P ⇒ Q)
            → компилятор + модуль SMT-ускорения
                    │
                    ▼
             ┌──────────┐
             │ Proved   │  → компиляция успешна
             │ Disproved│  → ошибка компиляции + контрпример
             │ Unproven │  → ошибка компиляции + недоказанное высказывание
             └────┬─────┘
                  │
                  ▼
         Программист пишет доказательственную функцию (код YaoXiang)
                  │
                  ▼
         Проверщик типов верифицирует ──→ Proved ──→ компиляция успешна
                  │
                  ▼
            Верификация неудачна → ошибка компиляции: «доказательство не выполняется»

4.1 Результаты доказательства: трёхзначная алгебра

Компиляторное вычисление возвращает три результата — это неизбежный вывод из проблемы остановки, а также естественное разделение в теории доказательств:

eval_compile_time : BoolExpr → Proved | Disproved(Model) | Unproven

• Proved → остановка, доказательственный объект сконструирован, проверка типов прошла. Компиляция продолжается.
• Disproved(M) → остановка, существует контрпример M. Ошибка компиляции + контрпример + позиция в исходном коде.
• Unproven → в пределах заданного бюджета ресурсов доказательство не сконструировано. Ошибка компиляции + недоказанное высказывание + отчёт о потреблении бюджета.

Unproven ≠ False. Когда компилятор говорит «я не могу доказать», это не эквивалентно ложности высказывания — просто это выходит за пределы текущих возможностей автоматического доказательства. Это честность, а не недостаток.

Жёсткие бюджетные ограничения — это инженерное решение проблемы остановки. Никаких ручек — дать их означает спросить пользователя «как вы думаете, ваша программа остановится?», но пользователь не знает, и компилятор не знает.

4.2 После Unproven: программист пишет доказательство

Когда компилятор возвращает Unproven, программист может написать доказательственную функцию — просто функцию на YaoXiang, тип возврата которой равен доказываемому высказыванию. Проверщик типов верифицирует эту функцию — это тот же механизм, что и верификация add(a, b): Int.

Высказывание = тип
Доказательство = программа (значение этого типа)
Верификация = проверка типов (единственный корень доверия)

SMT-решатель — не独立ная граница доверия — это ускоряющий модуль проверщика типов. SMT помогает найти доказательство, но верифицирует доказательство всегда проверщик типов. Когда SMT возвращает unsat, компилятор реконструирует результат как доказательственный объект, верифицируемый проверщиком типов. Если реконструкция не удалась (шаги рассуждения SMT выходят за пределы правил вывода ядра компилятора), происходит откат к Unproven — программист может вручную написать доказательственную функцию.

# Высказывание: уточнённое свойство, которое компилятор не может автоматически доказать
FirstIsMin: (T: Ord, arr: Sorted(T)) -> Type = {
    forall i in 0..arr.len: arr[0] <= arr[i]
}

# Доказательство: программист пишет функцию, тип возврата которой — высказывание выше
# Проверщик типов верифицирует эту функцию — точно так же, как верифицирует add(a,b): Int
first_is_min: (T: Ord, arr: Sorted(T)) -> FirstIsMin(T, arr) = {
    # компилятор здесь верифицирует: тип тела функции = FirstIsMin(T, arr)
    ...
}

Не нужно AI, не нужно экспорта в Coq, не нужны новые концепции. Свойства, которые нельзя автоматически доказать во время компиляции → программист пишет доказательство кодом YaoXiang → проверщик типов верифицирует. Весь процесс — плавный градиент — компилятор делает простые доказательства за тебя, сложные оставляет мозгу.

4.3 Слоистая зависимость внутри конвейера

Вышеупомянутые вычислители используют общий интерфейс, но существует порядок вычисления. Типовое равенство — предпосылка для всего последующего анализа; проверка владения/токенов зависит от информации о типах; верификация уточнённых предикатов зависит от результатов предыдущих двух слоёв. Компилятор вычисляет послойно; выражения с ошибками на нижнем уровне не попадают на верхний — чтобы не тратить бюджет решения на программы с ошибками типов.

Порядок вычисления (единый конвейер, послойное планирование)
├── Уровень 0: Типовое равенство (T1 == T2)
│   └── Структурная унификация → при неудаче дальнейшее бессмысленно, сразу возврат Disproved
├── Уровень 1: Владение/конфликт токенов
│   └── Потоково-чувствительный анализ активности → при неудаче безопасность памяти не成立, сразу возврат Disproved
└── Уровень 2: Уточнённые предикаты/импликации Хоара
    └── сам компилятор → SMT-ускорение → результат Proved / Disproved / Unproven

Каждый уровень по-прежнему возвращает Proved/Disproved/Unproven, используя общий интерфейс и общую бюджетную систему.

5. Трёхуровневое единство функций

Уровень	Время выполнения	Вход	Выход	Пример
Функция значения	Время выполнения	Значение	Значение	add: (a: Int, b: Int) -> Int = a + b
Конструктор типа	Время компиляции	Тип/значение	Type	List: (T: Type) -> Type = { data: Array(T) }
Компиляторный предикат	Время компиляции	Значение	Type	Positive: (x: Int) -> Type = { x > 0 }

Все используют идентичный синтаксис name: type = value. Компиляторные предикаты и конструкторы типов идут по единому компиляторному конвейеру доказательств — {} — пространство доказательств.

6. Циклы: генерация условий верификации по Флойду-Хоару

Для циклов не нужны отдельные аннотации : Invariant(...) или : decreases(...). Типовые аннотации с компиляторными предикатами на переменных определяют утверждения в стиле Флойда-Хоара — компилятор генерирует из типовых аннотаций условия верификации, конвейер доказательств проверяет, сохраняет ли каждое присваивание тип.

Основной механизм: каждая операция присваивания соответствует тройке Хоара {P} x := e {Q}, условие верификации — P ⇒ Q[e/x]. Компилятор генерирует для тела цикла одно условие верификации — после того как конвейер доказательств установит истинность индукционного шага, все итерации автоматически покрываются.

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # аннотация ссылается на i; при инициализации i=0, верификация: 0 == sum(arr[0..0]) → True
    mut i: UpTo(arr.len) = 0     # верификация: 0 <= 0 <= arr.len → True
    while i < arr.len {
        # компилятор генерирует одну VC для тела цикла. Предпосылка: s удовлетворяет SumUpTo(arr, i), i удовлетворяет UpTo(arr.len).
        #
        # s += arr[i]:
        #   Верификационное обязательство: s_new удовлетворяет SumUpTo(arr, i) (текущее i не меняется)
        #   Подстановка s_new = s_old + arr[i]:
        #     Нужно s_old + arr[i] == sum(arr[0..i+1])
        #     Из индукционной гипотезы s_old == sum(arr[0..i]), добавив arr[i] к обеим сторонам:
        #     sum(arr[0..i]) + arr[i] == sum(arr[0..i+1])
        #   Компилятор + SMT: линейная арифметика, миллисекунды → Proved
        #
        # i += 1:
        #   i изменяется → в графе зависимостей типовая аннотация s ссылается на i → триггер повторной верификации
        #   Новая цель верификации: s удовлетворяет SumUpTo(arr, i_new)
        #   То есть s == sum(arr[0..i_new]), гарантировано предыдущим шагом → Proved
        s += arr[i]
        i += 1
    }
    return s  # в этот момент s: SumUpTo(arr, arr.len), то есть s == sum(arr[0..arr.len])
}

Инвариант цикла — это типовая аннотация на переменной — программист пишет тип, компилятор проверяет индукционный шаг. Компилятору не нужно «обнаруживать» инвариант и не нужно «автоматически делать индукцию» — он разлагает индуктивное доказательство на локальные условия верификации для каждой операции присваивания, передавая их в конвейер доказательств для покомпонентного решения.

6.1 Отслеживание зависимостей: зависимые типы на изменяемых переменных

Предпосылка вышеизложенного механизма: компилятор знает, что типовая аннотация SumUpTo(arr, i) переменной s ссылается на i — когда i изменяется, ограничение типа s также меняется. Для этого компилятор должен поддерживать граф типовых зависимостей между переменными.

Структура данных:

TypeDepGraph: Map<VarName, Set<VarName>>
# ключ — зависимая переменная, значение — множество переменных, на которые ссылается её типовая аннотация
# пример: { i: {s}, j: {s, t}, ... }

Построение: при обработке mut v: Pred(... x ...) = init проверщик типов анализирует свободные переменные в параметрах Pred(...). Если в параметрах есть ссылка на другую изменяемую переменную x текущей области видимости, в графе зависимостей записывается x → v.

Триггер: когда зависимой переменной x присваивается значение, компилятор:

1. Находит в графе зависимостей все переменные, зависящие от x: {v₁, v₂, ...}
2. Для каждого v, генерирует условие верификации: удовлетворяет ли текущее значение v обновлённому типу Pred(... x_new ...)
3. Отправляет VC в конвейер доказательств

Порядок присваивания чувствителен: отслеживание зависимостей естественным образом обеспечивает правильный порядок присваивания. На примере SumUpTo(arr, i):

# Правильный порядок
s += arr[i]   # s_new удовлетворяет SumUpTo(arr, i+1)
i += 1        # i изменяется → повторная верификация s удовлетворяет SumUpTo(arr, i_new) → True

# Неправильный порядок — компилятор отклоняет
i += 1        # i изменяется → повторная верификация s удовлетворяет SumUpTo(arr, i_new)
              # s ещё не обновлён, s_old == sum(arr[0..i_old]) ≠ sum(arr[0..i_new])
              # → ошибка компиляции: переменная s не удовлетворяет типу SumUpTo(arr, i_new)
s += arr[i]   # недостижимо

Комбинированные зависимости: переменная может зависеть от нескольких переменных. Типовая аннотация { v: Int; v == x + y } одновременно зависит от x и y — изменение любой из них триггерит повторную верификацию.

Связь с конвейером доказательств: отслеживание зависимостей — это триггер генерации VC, а не独立мый механизм верификации. Оно отвечает на вопрос «когда нужно генерировать VC» — конвейер доказательств отвечает на вопрос «выполняется ли VC».

7. Проверка завершимости

Полностью автоматическая во время компиляции. Циклы, которые компилятор может доказать, проходят; те, что не может — выдают ошибку компиляции — программист должен сделать так, чтобы компилятор мог автоматически анализировать завершимость цикла. Никаких полуавтоматических аннотаций.

6.1 Принципы проектирования

Компилятор автоматически извлекает информацию, необходимую для доказательства завершимости, из двух источников:

1. Типовые аннотации переменных: граничные ограничения в уточнённых типах (например, UpTo(n) даёт верхнюю границу n и нижнюю границу 0)
2. Операции в теле цикла: операции, применяемые к переменным при каждой итерации

Компилятор пытается по приоритету四种 стратегии синтеза меры, останавливается на первой найденной.

6.2 Стратегия 1: Автоматический синтез линейной ранк-функции

Когда переменные имеют линейные граничные аннотации, компилятор перечисляет кандидатов линейных мер и верифицирует через SMT.

Вход:
  переменные v₁: UpTo(u₁), v₂: UpTo(u₂), ... (переменные с верхней и нижней границами)
  условие цикла cond
  множество присваиваний в теле цикла

Алгоритм:
  1. Извлечение границ каждой переменной из типовой аннотации: [low_i, high_i]
  2. Перечисление кандидатов мер: v_i, u_i - v_i, v_i - v_j, и другие линейные комбинации
  3. Для каждого кандидата меры m:
     - SMT-верификация m ≥ 0 (из типовых границ)
     - Для каждого пути выполнения в теле цикла, SMT-верификация m' < m (строго убывание)
  4. Найдена линейная комбинация, удовлетворяющая условиям → завершимость доказана

Покрытие: произвольные переменные, присваиваемые линейным выражениям (v = a·v + b) с ограниченными типовыми аннотациями. Включает i += const, i -= const, а также сжатие интервала в стиле бинарного поиска:

# Бинарный поиск: low = mid + 1 или high = mid
# Мера high - low строго убывает на обоих путях
binary_search: (arr: Sorted(Int, arr), key: Int) -> Option(Int) = {
    mut low: UpTo(arr.len) = 0
    mut high: UpTo(arr.len) = arr.len
    while low < high {
        let mid = (low + high) / 2
        if arr.data[mid] < key { low = mid + 1 }
        else if arr.data[mid] > key { high = mid }
        else { return Some(mid) }
    }
    return None
}

6.3 Стратегия 2: Подсчёт нарушений предиката — автоматическое извлечение меры из целевого типа 【Экспериментальная стратегия】

⚠️ Текущий статус: экспериментальная стратегия, при реализации Phase 3 решение о включении принимается на основе практической осуществимости. Данная стратегия эффективна для соседних перестановок (пузырьковая сортировка, сортировка вставкой), не может автоматически доказать для дальних операций (partition в быстрой сортировке, sift-down в пирамидальной сортировке). Таблица границ покрытия — ниже. Если Phase 3 покажет неосуществимость, стратегия будет удалена или понижена до будущей работы.

Ключевая идея: спецификации, написанные пользователем, — это материал для рассуждений компилятора. Компилятору не нужно встраивать «что такое сортировка» — он читает определение Sorted, автоматически извлекает меру из определения.

Вход:
  Целевой тип: Sorted(arr) = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }
  Операции в теле цикла: обмен соседних элементов

Алгоритм:
  1. Разбор определения предиката: forall i in range: cond(i, arr)
  2. Автогенерация меры: violation_count = |{ i | ¬cond(i, arr) }|
  3. Анализ влияния операций на меру:
     - Обмен соседних arr[j], arr[j+1] = arr[j+1], arr[j]
     - Затрагивает только три пары индексов j-1, j, j+1
     - Если arr[j] > arr[j+1] (нарушение предиката), после обмена эта пара удовлетворяет предикату
     - violation_count уменьшается как минимум на 1
  4. Верхняя граница: n·(n-1)/2 (максимальное число соседних инверсий), нижняя граница: 0
  → завершимость доказана

Текущее покрытие:

Алгоритм	Модель операций	Стратегия 2 доказуема?	Причина
Пузырьковая	Соседние обмены	✅	violation_count при каждом обмене строго убывает
Сортировка вставкой	Соседние перемещения	✅	Каждая перестановка устраняет одно нарушение
Сортировка выбором	Дальние обмены	❌	Один обмен может увеличить violation_count
Быстрая сортировка	partition-секционирование	❌	Дальние обмены, нет гарантии монотонного убывания
Пирамидальная	sift-down	❌	Древовидные операции, violation_count не монотонен

Дополняющие стратегии: для быстрой сортировки сжатие интервала low < high покрывается стратегией 1 (линейная ранк-функция) — внешний partition-рекурс, каждое уполовинивание интервала. Стратегии 1 и 2 взаимодополняющи, завершимость большинства практических алгоритмов доказуема одной из них. Однако расширение стратегии 2 (дальние операции, древовидные операции) остаётся открытой проблемой.

sort: (arr: Array(Int)) -> (result: Sorted(result)) = {
    mut i: UpTo(arr.len) = 0
    while i < arr.len - 1 {
        mut j: UpTo(arr.len - i - 1) = 0
        while j < arr.len - i - 1 {
            if arr.data[j] > arr.data[j+1] {
                arr.data[j], arr.data[j+1] = arr.data[j+1], arr.data[j]
            }
            j += 1
        }
        i += 1
    }
    return arr
}

6.4 Стратегия 3: Модель ограниченного возрастания/убывания

v += const (положительная константа), переменная имеет верхнеграничную типовую аннотацию → мера upper_bound - v убывает каждый раз на const, нижняя граница 0. Это вырожденный случай стратегии 1, компилятор обрабатывает его первым в быстром пути.

6.5 Стратегия 4: Шаблон меры с мультипликативным масштабированием

v *= const (const > 1), переменная имеет верхнюю и нижнюю границы. Компилятор имеет встроенный шаблон логарифмической меры ceil(log_const(upper/v)), каждый умножение на const уменьшает меру на 1.

mut i: Positive(i) = 1
while i < n {
    # компилятор автоматически выводит: мера ceil(log₂(n/i)), каждое умножение на 2 уменьшает меру на 1
    i *= 2
}

6.6 Разделение завершимости и корректности

Доказательство завершимости и доказательство корректности независимы:

• Завершимость: четыре стратегии выше автоматически доказывают, что цикл завершается за конечное число шагов
• Корректность: продвигает ли тело цикла к целевому типу, проверяется компиляторным конвейером доказательств через условия верификации

Оба прошли → компиляция успешна. Завершимость доказана, но корректность не прошла → ошибка компиляции + контрпример. Корректность доказана, но завершимость не доказана → ошибка компиляции с указанием неанализируемой переменной или операции. Оба не прошли → отдельные отчёты об обеих неудачах.

6.7 Проверка завершимости рекурсивных функций

Для рекурсивных функций, которые должны вычисляться во время компиляции, компилятор проверяет убывание параметров:

factorial: (n: Int) -> Int = {
    if n <= 1 { return 1 }
    return n * factorial(n - 1)  # компилятор анализирует: n-1 < n → убывает → завершается
}

# Использование во время компиляции — компилятор гарантирует завершение factorial во время компиляции
vec: Vec(factorial(5)) = Vec(120)()  # 5! = 120, вычислено во время компиляции

Сценарий	Поведение
Компилятор может проанализировать убывание рекурсии (например, n-1)	Вычисление во время компиляции
Не убывает / невозможно判定 убывание	Ошибка компиляции
Вызов во время выполнения (не в типовой позиции)	Проверка завершимости не нужна

6.8 Жёсткие границы

i = f(i) где f необратима, неограниченна, не сохраняет монотонность — математически невозможно автоматически доказать завершимость. Ошибка компиляции:

Данный цикл невозможно автоматически доказать завершающимся. Цикловая переменная зависит от неанализируемой функции f. Используйте итерационный паттерн, анализируемый компилятором.

Это не неудача компилятора. Код, безопасность которого невозможно статически доказать, не компилируется.

8. SMT-решатель: ускоряющий модуль проверщика типов

В традиционных языках SMT-решатель — это внешний инструмент (как F* вызывает Z3, Dafny вызывает Z3). В YaoXiang это ускоряющий модуль проверщика типов — вызывается только когда ядро компилятора само не может напрямую определить результат. SMT помогает найти доказательство, но верифицирует доказательство проверщик типов.

Модель доверия: проверщик типов — единственный корень доверия. SMT-решатель — ускоряющий модуль — он помогает найти доказательство, но SMT — не独立ная граница доверия. Компилятор доверяет результату Z3 unsat (в соответствии с подходом F*/Dafny — вероятность ошибки Z3 ниже вероятности бага самого компилятора, это прагматичный инженерный выбор). Настоящий контроль над ненадёжностью — на уровне трансляции в SMT. Если в трансляции баг, компилятор выявит его на других тестах.

Интерфейс: компилятор внутренне транслирует в формат SMT-LIB 2.6, а не привязывается к API特定ного решателя. SMT-LIB — стандарт ISO, Z3, CVC5, MathSAT, Yices все нативно поддерживают.

Бэкенд по умолчанию: Z3 (лицензия MIT, наиболее широко документирован и сообществом верифицирован). CVC5 как SMT-LIB-совместимый альтернативный — пользователь может переключить через флаг компилятора.

Никакого «универсального слоя абстракции решателя» — SMT-LIB уже является таким слоем. Если в будущем CVC5 совершит прорыв в特定ной теории, переключение — это просто замена бинарника, без изменения кода компилятора.

Компиляторное Bool-выражение
        │
        ├── Ядро компилятора может определить напрямую (структурная эквивалентность, простая арифметика,
        │   тривиальные формулы после константной свёртки)
        │   → напрямую возврат Proved / Disproved
        │
        └── Ядро компилятора не может определить (кванторы, символьные переменные)
            → предварительная редукция зависимых типов (factorial(5) → 120)
            → трансляция в формат SMT-LIB
            → отправка в Z3/CVC5 (с ограничением бюджета)
            → возврат: unsat → Proved  │  sat + модель → Disproved  │  unknown → Unproven

Бюджет решения — жёсткое ограничение, как глубина стека:

Измерение бюджета	По умолчанию	Описание
Число шагов решения	10,000	Z3 для линейной арифметики обычно возвращается за сотни шагов. 10,000 покрывает 99% практических предикатов.
Время	100ms	Один предикат >100ms = пользователь пишет компиляторную программу, а не типовую аннотацию. 100ms × 50 предикатов = верхний предел времени компиляции 5 секунд.
Глубина инстанцирования кванторов	3	Три уровня вложенности кванторов покрывают практические паттерны. Свыше трёх — скорее всего логические упражнения.

При превышении бюджета возврат Unproven, ошибка компиляции + позиция предиката + потреблённый бюджет. Никакой деградации, никаких проверок времени выполнения, никакого silent pass.

Почему это практически работает: в инженерной практике 95% практических предикатов — линейная арифметика — x > 0, arr.len > 0, 0 <= idx < arr.len — всё в разрешимом фрагменте, SMT-решатель возвращается за миллисекунды. Для редких сложных предикатов, превышающих бюджет, программист пишет доказательственную функцию.

Зависимые типы перед вызовом SMT проходят предварительную редукцию: factorial(5) напрямую вычисляется во время компиляции в 120, append([1,2], [3]) напрямую вычисляется в [1,2,3]. Эти детерминированные вычисления значений не потребляют бюджет SMT.

Программисту не нужно знать о существовании SMT. Модель мышления: компилятор может доказать — проходит, не может — ошибка — если компилятор не может, можешь написать функцию и доказать ему.

9. Комбинирование компиляторных предикатов

Компиляторный предикат — это функция, возвращающая Type, комбинирование естественно через функциональную композицию:

SortedNonEmpty: (T: Ord, arr: Array(T)) -> Type = {
    Sorted(T, arr) && NonEmpty(arr)
}

10. Примеры кода

9.1 Безопасное деление

Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b

result = divide(10, 2)   # ✅ компилятор верифицирует Positive(2) = { 2 > 0 } → True
// result = divide(10, 0)  # ❌ компилятор верифицирует Positive(0) = { 0 > 0 } → False

9.2 Безопасность обращения к массиву

InBounds: (idx: Int, arr: Array(T)) -> Type = { 0 <= idx && idx < arr.len }

get: (arr: Array(T), idx: InBounds(idx, arr)) -> T = arr.data[idx]

arr = Array(Int)(1, 2, 3)
x = get(arr, 1)   # ✅ компилятор верифицирует InBounds(1, arr) = { 0 <= 1 && 1 < 3 } → True
// y = get(arr, 5)  # ❌ компилятор верифицирует InBounds(5, arr) = { 0 <= 5 && 5 < 3 } → False

9.3 Корректность сортировки

Sorted: (T: Ord, arr: Array(T)) -> Type = {
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

sort: (T: Ord) -> ((arr: Array(T))) -> (result: Sorted(T, result)) = {
    result = arr.clone()
    // ... реализация алгоритма сортировки ...
    return result
}

9.4 Циклы: генерация VC компилятором

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0
    mut i: UpTo(arr.len) = 0
    while i < arr.len {
        s += arr[i]
        i += 1
    }
    return s
}

11. Конвейер диспетчеризации dispatch: унифицированная диспетчеризация времени компиляции и выполнения

assert и Assert — две стороны одного примитива уточнённого типа. Конвейер диспетчеризации dispatch автоматически решает идти ли по пути компиляторного доказательства или проверки времени выполнения в зависимости от свободных переменных предиката — доступны ли они во время компиляции:

Критерий	Режим	Поведение
Все свободные переменные известны во время компиляции (параметры обобщённого типа, константы времени компиляции)	CompileTime	Вход в конвейер доказательств: Proved → стирание, Disproved → ошибка компиляции, Unknown → требуется доказательство
Существуют свободные переменные времени выполнения (параметры функций, внешний ввод, mut-переменные)	Runtime	Вставка проверки времени выполнения, инъекция уточнённого факта в потоково-чувствительное множество предположений Γ

Ключевой момент: «не может определить» ≠ «опровергнуто». В режиме CompileTime Unknown требует доказательства (без тихого понижения), в режиме Runtime высказывание во время компиляции вообще не имеет истинностного значения — как бы ни был силён провайдер, он не сможет написать тавтологию для «пользователь мог ввести отрицательное число», проверка времени выполнения — единственный sound выбор. Это не слабость провайдера, а теоретическая неизбежность.

12. Потоково-чувствительное множество предположений Γ: распространение наисильнейшего постусловия

Компилятор поддерживает потоково-чувствительное (flow-sensitive) множество предположений Γ, отслеживающее высказывания, известные как истинные в каждой точке потока управления.

SP (наисильнейшее постусловие) распространение:

assert(x > 0)       // Γ = {x > 0}
y = x + 1           // Γ = {x > 0, y > 1}  ← SP распространение

Kill set для mut-переменных: после переприсваивания mut-переменной все предположения, затрагивающие эту переменную, удаляются из Γ:

assert(x > 0)       // Γ = {x > 0}
mut x = x - 5       // Γ = {}  ← x > 0 убито

Это жёсткое требование soundness — значение переменной изменилось, старые предположения недействительны.

Слияние веток: при слиянии IF/ELSE или match-веток Γ берёт пересечение предположений веток. Только высказывания, истинные на всех путях, выходят из ветки.

13. Уточнение модели стирания: стирание witness ≠ стирание check

Утверждение RFC-027 о том, что «уточнённые типы во время выполнения полностью стираются», относится к proof witness (доказательским токенам) — верифицированные во время компиляции доказательские объекты не генерируют кода времени выполнения. Но runtime check, вставленный dispatch в режиме Runtime, сохраняется — это Bool-проверка на уровне значений, не witness на уровне типов.

Резюме: witness стирается, check сохраняется. Две вещи не конфликтуют, исходное утверждение RFC-027 остаётся в силе.

Детальное проектирование

Синтаксические изменения

Ранее (RFC-022)	После (этот RFC)
//! requires: NonEmpty(n) = n > 0	Компиляторный предикаат как тип параметра (b: Positive(b))
//! ensures: ExistsMax(result, arr)	Тип возврата с параметром возвращаемого значения -> (result: IsMax(T, arr, result))
/*! invariant: ... !*/	Типовые аннотации с компиляторными предикатами на переменных — инварианты Флойда-Хоара
//! decreases: n	Полностью автоматический вывод меры функций компилятором
Спецификации — комментарии	Спецификации — система типов

Синтаксис

Для компиляторных предикатов нет новых ключевых слов. {} — пространство доказательств, полностью согласовано с существующим синтаксисом определения типов. Компиляторный предикат — это функция, возвращающая Type — name: (params) -> Type = { утверждения }. При использовании — просто вызов функции — Positive(b), IsMax(T, arr, result).

# Компиляторный предикат = функция, возвращающая Type, {} внутри — утверждения, верифицируемые компилятором
# Используется существующий синтаксис функций/типов, новые BNF-правила не нужны
predicate ::= identifier ':' params '->' 'Type' '=' '{' assertions '}'

Новая синтаксическая концепция: параметр возвращаемого значения — в -> (name: Type) name — это параметр возвращаемого значения.

Параметр возвращаемого значения — это единственная синтаксическая концепция, которую YaoXiang вводит поверх существующего синтаксиса функций. Его семантика:

• Значение name предоставляется оператором return
• name существует только в сигнатуре типа, только предикат постусловия ссылается на него (как -> (result: IsMax(T, arr, result)))
• name не входит в область видимости тела функции, не появляется у вызывающей стороны
• Параметр возвращаемого значения опционален — без постусловия сигнатура полностью совпадает с обычной функцией (-> Int), никакой дополнительной нагрузки

Причина введения: постусловию нужно ссылаться на «значение, которое функция вернёт». Без параметра возвращаемого значения компилятор мог бы использовать только специальные правила (неявные переменные вроде $result или __retval__), чтобы позволить предикату ссылаться на возвращаемое значение. Параметр возвращаемого значения делает такую ссылку явной — это просто параметр, только значение предоставляется return, а не вызывающей стороной.

Доказательственная функция — это не новая концепция — это просто функция YaoXiang, тип возврата которой равен доказываемому высказыванию. Когда компилятор возвращает Unproven, программист предоставляет доказательственную функцию, проверщик типов верифицирует её тем же способом, что и тип возврата любой другой функции. Никакого нового синтаксиса, новых ключевых слов, новых правил.

Влияние на систему типов

• Типовые вселенные: компиляторные предикаты находятся на уровне Type₂ — функции, принимающие значения и возвращающие Type, на том же уровне, что и конструкторы типов
• Взаимодействие с обобщениями: компиляторные предикаты могут иметь обобщённые параметры, например NonEmpty: (T: Type) -> (arr: Array(T)) -> Type
• Взаимодействие с владением: выражения в компиляторных предикатах подчиняются правилам владения, могут только читать, не писать
• Вывод типов: параметры компиляторных предикатов участвуют в HM-выводе типов

Представление во время выполнения

Компиляторные предикаты во время выполнения обрабатываются согласно результату dispatch-диспетчеризации:

• Режим CompileTime (все свободные переменные известны во время компиляции): после подтверждения доказательства witness (доказательский токен) полностью стирается. Positive: (x: Int) -> Type = { x > 0 } — параметр b: Positive(5) во время выполнения представляется просто как Int. Уточнённое условие { 5 > 0 } уже проверено и стёрто.
• Режим Runtime (существуют свободные переменные времени выполнения): сохраняется runtime check — Bool-проверка на уровне значений, инъекция в потоково-чувствительное множество предположений Γ. Подробности см. в §11 конвейер dispatch и §13 уточнение модели стирания.

Размещение компиляторного предиката в типовой позиции (как f(x: Positive(x))) не создаёт обёрточный тип и не выделяет дополнительную память. Но когда x происходит из пользовательского ввода, вставляется Bool-проверка времени выполнения.

Ограничение взаимодействия с ref: компиляторные предикаты могут ссылаться только на неизменяемые заимствования или значения с переданным владением. Попытка использовать изменяемое заимствование в компиляторном предикате — компилятор не может гарантировать во время компиляции, что результат верификации останется верным во время выполнения — такое использование вызывает ошибку компиляции.

Изменения в компиляторе

1. Парсер: компиляторные предикаты используют стандартный синтаксис функций, дополнительных правил парсинга не требуется
2. Конвейер доказательств времени компиляции: унифицированный интерфейс возврата Proved/Disproved/Unproven, автоматический выбор стратегии
3. Модуль SMT-ускорения: слой трансляции в SMT-LIB 2.6, бэкенд по умолчанию Z3, альтернатива CVC5
4. Ядро проверщика типов: реализация правил вывода — структурная эквивалентность, βδι-редукция, введение/устранение универсальных кванторов. Это единственный корень доверия, SMT и доказательства программиста проходят через него
5. Генерация условий верификации: WP/SP-исчисление + обязательства по доказательству инвариантов циклов
6. Отчёт об ошибках: форматирование контрпримеров + отчёт о недоказанных высказываниях + привязка к позиции исходного кода

Обратная совместимость

• ✅ Код, не использующий компиляторные предикаты, полностью неизменен
• ✅ Компиляторные предикаты в режиме CompileTime имеют нулевые накладные расходы времени выполнения, в режиме Runtime сохраняют только необходимые Bool-проверки
• ⚠️ Синтаксис //! из RFC-022 более не поддерживается — но 022 никогда не был реализован, миграционная нагрузка отсутствует

Компромиссы

Преимущества

• Полная реализация изоморфизма Карри-Ховарда: тип — высказывание, программа — доказательство, name: Proposition = Proof
• Единство: компиляторные предикаты используют полностью идентичный синтаксис с обычными функциями, без концептуального раскола
• Прозрачность SMT: программисту не нужно знать о существовании SMT, модель мышления согласована с проверкой типов
• Постепенное принятие: можно начать с одного компиляторного предиката и постепенно расширять покрытие
• Минимальные накладные расходы времени выполнения: режим CompileTime имеет нулевые накладные расходы, режим Runtime сохраняет только необходимые Bool-проверки

Недостатки

• Время компиляции: SMT-решение увеличивает время компиляции, но жёсткие бюджетные ограничения гарантируют контролируемый верхний предел
• Границы автоматического доказательства: сложные предикаты за пределами логики первого порядка с линейной арифметикой могут требовать от программиста написания доказательственных функций. Это не недостаток языка — это неизбежный вывод из проблемы остановки. Компилятор честно сообщает Unproven вместо ложного True/False
• Кривая обучения: написание эффективных компиляторных предикатов и доказательственных функций требует понимания базовой интуиции изоморфизма Карри-Ховарда
• Сложность реализации: унификация компиляторного конвейера доказательств требует тщательного проектирования

Смягчение рисков

• Жёсткие бюджетные ограничения SMT-решения (шаги 10,000 / время 100ms / глубина инстанцирования 3), при превышении бюджета возврат Unproven
• Предварительная редукция зависимых типов: детерминированные вычисления значений выполняются первыми, SMT обрабатывает только недетерминированную часть
• Unproven — не тупик: программист может написать доказательственную функцию, проверщик типов верифицирует — то же самое, что и верификация типа возврата любой функции
• Инкрементальная верификация: верифицируются только изменённые модули
• Чёткие сообщения об ошибках +展示 контрпримеров + отчёт о потреблении бюджета + недоказанные высказывания + suggestions (если компилятор может предложить)

Альтернативные варианты

Вариант	Почему не выбран
RFC-022: спецификации в виде //! комментариев	Спецификации и типы разделены, нарушение изоморфизма Карри-Ховарда
Отдельные файлы спецификаций (как CVL)	Спецификации отделены от кода, увеличение стоимости сопровождения
Только проверки времени выполнения	Невозможность статической гарантии корректности
Внешние помощники доказательства (как Coq)	Разрыв с компилятором, требуется独立ный язык доказательств и独立ная граница доверия. Выбор YaoXiang: доказательство — код YaoXiang, проверщик типов — единственный корень доверия
本方案: компиляторные предикаты как объекты первого класса	✅

Стратегия реализации

Разделение на фазы

Фаза	Содержание
Фаза 1	Ядро компилятора: структурная эквивалентность + βδι-редукция + введение/устранление универсальных кванторов. Поддержка простых арифметических предикатов (x > 0, arr.len > 0)
Фаза 2	Слой трансляции SMT-LIB + интеграция Z3/CVC5. Конвейер возвращает Proved/Disproved/Unproven. При Unproven поддержка написания программистом доказательственных функций
Фаза 3	Генерация VC для инвариантов циклов + проверка завершимости (линейная ранк-функция + подсчёт нарушений + ограниченный паттерн + контроль комбинаторного взрыва)
Фаза 4	Инкрементальная верификация + кэширование + поддержка IDE

Зависимости

• RFC-010: Унифицированный синтаксис типов — компиляторные предикаты основаны на name: type = value
• RFC-011: Система обобщённых типов — компиляторные предикаты могут иметь обобщённые параметры
• RFC-009: Модель владения — выражения в компиляторных предикатах подчиняются правилам владения

Открытые вопросы

• [x] Выбор SMT-решателя: по умолчанию Z3 (лицензия MIT, наиболее широко верифицирован). CVC5 как SMT-LIB-совместимая альтернатива, переключение через флаг компилятора. Компилятор внутренне транслирует в стандартный формат SMT-LIB 2.6 — SMT-LIB и есть слой абстракции, никаких自定义ных интерфейсов通用ного решателя.
• [x] Конкретные数值 бюджета решения: шаги 10,000 / время 100ms / глубина инстанцирования кванторов 3. Фиксировано внутри компилятора, без ручек. Если на практике окажется недостаточно (реальный use case, не «пользователь ошибся»), скорректировать.
• [x] Диапазон поддержки кванторов: на уровне языка нет ограничений на порядок кванторов. Компиляторные предикаты принимают параметры типа Type — Type включает функциональные типы — поэтому кванторы высших порядков являются естественным следствием системы типов, не требуют特殊ного синтаксиса. SMT-решатель может автоматически判定 кванторы первого порядка (forall/exists, поддержка чередующихся вложений, ограничено бюджетной глубиной 3). Кванторы высших порядков: SMT возвращает Unproven, компилятор предлагает «этот предикат выходит за рамки автоматического доказательства, предоставьте доказательственную функцию». Программист пишет функцию YaoXiang, тип возврата которой равен этому высказыванию — проверщик типов верифицирует. Никакого внешнего экспорта, никакого AI, никакого интерактивного режима доказательства. Всё — код YaoXiang, всё верифицируется проверщиком типов.
• [x] Форматирование контрпримеров: имена переменных исходного кода напрямую используются как SMT-переменные (плюс префикс модуля во избежание конфликтов). При возврате модели Z3 обратный поиск по имени переменной. Формат вывода: имя переменной = конкретное значение + позиция в исходном коде + позиция определения предиката. Никаких сложных слоёв маппинга.
• [x] Взаимодействие компиляторных предикатов с ref умными указателями? → Решено: компиляторные предикаты допускают только неизменяемые заимствования или значения с переданным владением. Значения с изменяемым заимствованием не могут появляться в компиляторных предикатах.
• [x] Расширение меры подсчёта нарушений предиката на дальние операции? → Не расширять. Текущее покрытие (соседние обмены, соседние перемещения) дополняется стратегией 1 (линейная ранк-функция) — внешнее сжатие интервала в быстрой сортировке покрывается стратегией 1, пирамидальная сортировка покрывается стратегией 1 (паттерн индексов массива). Циклы, завершимость которых не может быть доказана ни одной из четырёх стратегий, компилятор выдаёт ошибку — это философия жёсткой безопасности, не недостаток. Если в будущем появятся реальные сценарии (не академические построения) алгоритмов, которые не покрываются ни одной стратегией, пересмотреть.
• [x] Комбинаторный взрыв перечисления линейных ранк-функций: верхний предел перечисления кандидатов — 3 переменных с границами. ≤3 — перечисление всех линейных комбинаций и SMT-верификация по одной. >3 — только попытка однопеременных мер (v_i, u_i - v_i), при неудаче прямая ошибка компиляции — подсказка программисту «в цикле >3 переменных с границами, компилятор не может автоматически синтезировать многопеременную меру». Это не инженерный компромисс — это вынуждение программиста писать более простые циклы.

Ссылки

• RFC-010: Унифицированный синтаксис типов
• RFC-011: Проектирование системы обобщённых типов
• RFC-009: Модель владения
• Howard, W. A. (1969). The Formulae-as-Types Notion of Construction.
• Swamy, N. et al. (2016). Dependent Types and Multi-Monadic Effects in F*. POPL 2016.
• Vazou, N. et al. (2014). Refinement Types for Haskell. ICFP 2014.
• Leino, K. R. M. (2010). Dafny: An Automatic Program Verifier for Functional Correctness. LPAR 2010.
• De Moura, L. & Bjørner, N. (2008). Z3: An Efficient SMT Solver. TACAS 2008.

---

Жизненный цикл и судьба

┌─────────────┐
│   Черновик  │  ← создан автором
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  На ревью   │  ← текущий статус: обсуждение сообществом
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│  Принято    │    │  Отклонено  │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/  │    │  rejected/  │
│ (финальный │    │ (оставлен   │
│  дизайн)   │    │  на месте)  │
└─────────────┘    └─────────────┘