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 проектировал спецификации в форме комментариев //!:

yaoxiang

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)

Дженерики — это частный случай предикатов времени компиляции.

yaoxiang

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 = { утверждения }. Компилятор не различает «утверждения о типах» и «утверждения о значениях» — всё это цели вычисления в конвейере доказательств.

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

yaoxiang

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])
}

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

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

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

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

yaoxiang

# Предусловие: явный вызов предиката времени компиляции в типе параметра
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. Распространение путевых условий: верификация времени компиляции для значений времени выполнения

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

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

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

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

yaoxiang

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) — обе аннотации типов ссылаются на сам параметр. Различие только в сложности аннотации типа, механизм полностью одинаков — после связывания имени тип может зависеть от этого имени.

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

yaoxiang

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(значение)

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

yaoxiang

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 во время компиляции.

yaoxiang

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 and y < 10 → в ветвь помещается x > 0 и y < 10
предусловие функции: при вызове divide(a, b) свидетельство того, что b удовлетворяет Positive, должно приходить либо из текущих гипотез, либо из аннотации уточнённого типа самого аргумента (если b уже аннотирован как Positive, его тип несёт b > 0)
присваивание: при let z = y существующее уточнённое условие на y передаётся z

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

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

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

yaoxiang

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

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

{} ⇒ { y > 0 }

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

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

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

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

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

Этап	Обязанности
Сбор путевых условий	Этап анализа потока управления компилятора, аннотирование множества гипотез для каждого базового блока
Генерация условий верификации	При встрече ограничения типа, требующего верификации, объединение путевых условий + информации о типе аргумента
Вычисление в конвейере	Ядро компилятора → ускорение 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 — программист может вручную написать функцию-доказательство.

yaoxiang

# Утверждение: уточнённое свойство, которое компилятор не может автоматически доказать
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)
    ...
}

Не нужен ИИ, не нужен экспорт в 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]. Компилятор генерирует условие верификации для тела цикла один раз — после того как конвейер доказательств устанавливает индуктивный шаг, все итерации покрываются автоматически.

yaoxiang

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 Отслеживание зависимостей: зависимые типы на мутабельных переменных

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

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

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

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

Срабатывание: когда зависимая переменная x получает значение, компилятор:

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

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

yaoxiang

# Правильный порядок
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. Проверка завершения

Область применения: уточнённые типы. Завершаемость — не независимый переключатель, а часть режима верификации: как только тип уточнён (`Refined { base, constraint }), вычисление, аннотированное этим типом, входит в режим верификации, и в этом режиме требуется завершаемость; неуточнённые обычные типы не входят в режим верификации и не порождают обязательств завершения.

Отсюда два следствия:

Циклы: голый while не входит в режим верификации; когда переменная меры имеет уточнённую аннотацию (например, i: UpTo(n)), она входит в режим верификации и должна доказывать завершение.
Рекурсия: когда сигнатура функции уточнена (уточнение параметра или возвращаемый тип содержит уточнение), она входит в режим верификации и должна доказывать строгое убывание меры в каждой точке рекурсивного вызова.

В режиме верификации приоритет у автоматического подхода: компилятор сначала автоматически исследует меры, доказуемые проходят; если не найдено и мера не дана явно — ошибка компиляции. Нет лазейки в виде синтаксиса аннотаций — мера и утверждение завершения пишутся в позиции типа, без введения нового синтаксиса типа decreases. Формы меры и явного фолбэка см. в §6.9.

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

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

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

Компилятор пробует четыре стратегии синтеза меры в порядке приоритета, останавливаясь на первой подходящей. Четыре стратегии — это ограниченная последовательность шаблонов исследования меры, вход — уточнённые ограничения (стратегии 1–4 стартуют с «переменных ограниченного типа»), а не «код, вычисляемый во время компиляции»; они и явная мера из §6.9 — это автоматическая и ручная стороны одной и той же вещи.

Исследование меры — это поиск, а не вывод. Поиск только перечисляет шаблоны (линейный ранг, счётчик нарушений, ограниченные паттерны, мультипликативное сжатие), не гарантирует существования решения — общий вывод меры в общем случае неразрешим (сводится к проблеме остановки). Поэтому случаи вне шаблонов должны допускать явное указание меры программистом (§6.9), иначе ошибка компиляции.

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, а также бинарный поиск со сжатием интервала:

yaoxiang

# Бинарный поиск: 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: счётчик нарушений предиката — автоматическое извлечение меры из целевого типа 【Экспериментальная стратегия】

⚠️ Текущий статус: экспериментальная стратегия, на этапе 3 реализации будет решено по фактической реализуемости, включать ли её. Эта стратегия эффективна для операций соседнего обмена (сортировка пузырьком, сортировка вставками), но не может автоматически доказать несмежные операции (partition быстрой сортировки, sift-down пирамидальной сортировки). Границы покрытия см. в таблице ниже. Если на этапе 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 (несоседние операции, древовидные операции) остаётся открытой проблемой.

yaoxiang

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.

yaoxiang

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

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

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

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

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

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

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

yaoxiang

gcd: (a: Int, b: NonNegative(b)) -> Int = {
    if b == 0 { return a }
    return gcd(b, a % b)  // Компилятор исследует: мера (b, a % b) с подходящим порядком убывает → завершение
}

Убывание формальных параметров — сильнейший автоматический путь (структурная рекурсия). Если не найдено, программист явно указывает меру в позиции типа (§6.9).

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

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

Этот цикл не может быть автоматически доказан как завершающийся. Переменная цикла зависит от неанализируемой функции f. Пожалуйста, используйте итеративный паттерн, который может быть проанализирован компилятором, или привяжите имя к этому циклу и предоставьте меру в позиции типа (§6.9).

Это не провал компилятора. Код, который не может быть статически доказан как безопасный, не проходит компиляцию. Даже при явной мере она должна быть признана SMT истинной, чтобы пройти — неправильно написанная мера будет отклонена контрпримером, человек может не суметь доказать, но не может доказать неверно.

6.9 Явная мера: `Terminates`

Когда автоматическое исследование не находит меру, программист записывает меру в позиции типа — тем же механизмом, что и Positive(b), IsMax(T, arr, result) (применение предиката), без нового синтаксиса:

yaoxiang

// Мера: обычная функция, тестируемая, переиспользуемая, не участвует в рантайме
gcd_measure: (a: Int, b: Int) -> Int = { b }

// Компонент завершения живёт в типе самой функции
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

// Цикл: имя привязки — это якорь, мера получает значения в своей области видимости
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

Обоснование для цикла: Terminates(m) уточняет тип значения хвостового выражения тела цикла, якорь предоставляется именем привязки acc — благодаря этому цикл может быть обозначен, и нет «слепого пятна невозможности обозначения анонимной конструкции».

Terminates — это встроенный предикат, принадлежащий к тем же базовым примитивам, что и Int, Never. Это единственный предикат, чей функционал пишется компилятором — его утверждение («мера строго убывает в каждой точке рекурсивного вызова / на каждом обратном ребре цикла») живёт в вычислительной структуре, и пользовательский предикат не может сослаться на тело функции или тело цикла, поэтому не может быть выражен через синтаксис определения предикатов из раздела «Синтаксис». Встроенная поверхность сходится к этому единственному имени.

Арности. Terminates(FnType, m) и Terminates(m) — это два арности одного и того же предиката, а не два разных конструктора:

Форма	Якорь	Назначение
`Terminates(m)`	Имя текущей привязки	Саморекурсивные функции, циклы — форма по умолчанию
`Terminates(FnType, m)`	Явный тип функции	Взаимная рекурсия и другие сценарии без уникального якоря

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

Мера не ограничивает возвращаемый тип. Мера может быть выражением любого типа (не обязательно натуральным числом); «строгое убывание» на ней задаётся имеющимся подходящим порядком на этом типе. Является ли мера обоснованной (например, при возврате Int является ли она >= 0) — это отдельное обязательство, передаваемое наряду с обязательством убывания в уточняющий вывод или SMT; если оба не выводятся, диагностика не отвергает напрямую, а предлагает направление проверки (обоснована ли нижняя граница меры, действительно ли рекурсивные аргументы движутся в эту сторону).

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

Механизмы генерации обязательств, конвейер верификации, направления диагностики, разделение меры взаимной рекурсии (SCC) и т.д. см. в RFC-027a: Явные меры проверки завершения.

8. Решатель SMT: модуль ускорения проверки типов

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

Модель доверия: проверка типов — единственный корень доверия. Решатель SMT — модуль ускорения — он помогает найти доказательство, но SMT не является отдельным доверенным рубежом. Компилятор доверяет результату unsat от Z3 (в соответствии с подходом 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% практических предикатов.
Время	100 мс	Один предикат дольше 100 мс = пользователь пишет программу времени компиляции, а не аннотацию типа. 100 мс × 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, и композиция реализуется естественно через композицию функций:

yaoxiang

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

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

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

yaoxiang

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 Безопасность доступа к массиву

yaoxiang

InBounds: (idx: Int, arr: Array(T)) -> Type = { 0 <= idx and 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 and 1 < 3 } → True
# y = get(arr, 5)  # ❌ Компилятор верифицирует InBounds(5, arr) = { 0 <= 5 and 5 < 3 } → False

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

yaoxiang

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 компилятором

yaoxiang

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 у утверждения в компайл-тайме вообще нет истинности — никакой prover не напишет тавтологию для «пользователь мог ввести отрицательное число», рантайм-проверка — единственный sound-выбор. Это не слабость prover-а, это теоретическая неизбежность.

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

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

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

yaoxiang

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

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

yaoxiang

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

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

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

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

Утверждение RFC-027 «уточнённые типы полностью стираются в рантайме» относится к proof witness (токену доказательства) — терм доказательства, верифицированный в компайл-тайме, не порождает рантайм-кода. Но рантайм-check, вставленный диспетчеризацией в режиме 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`	Мера записывается в позиции уточнённого типа (`Terminates`); компилятор сначала пытается автоматическое исследование, требует явную только при провале
Спецификация — это аннотация	Спецификация — это система типов

Синтаксис

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

bnf

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

Аргументы применения предиката должны быть формой констант времени компиляции — литералы, переменные (связанные по имени), применения типов (рекурсивное извлечение) или обозначаемые ссылки на функции времени компиляции (имя функции). Непреобразуемость аргумента в константное выражение — ошибка E1092, несовпадение числа аргументов с числом формальных параметров — ошибка E1093. Аргументы связываются позиционно со списком формальных параметров, арность предиката определяется объявлением — Positive(x) унарный, IsMax(T, arr, result) тернарный, Terminates(m) и Terminates(FnType, m) унарный и бинарный — уточняющие ограничения никогда не отбрасываются молча (ранее непреобразуемые аргументы приводили к беззвучному исчезновению ограничений, и связывание, нарушающее ограничение, проходило молча).

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

Формальный параметр возврата — это единственная синтаксическая концепция, вводимая YaoXiang в существующий синтаксис функций. Её семантика:

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

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

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

Граница между ними. Область корректности (Unproven предиката) восполняется доказательством в теле: пишется функция, чей возвращаемый тип — доказываемое утверждение. Область завершения (§6.9) восполняется явной мерой в позиции типа: пишется Terminates(мера) как тип привязки или сигнатуры функции. Первое — «для недоказуемого утверждения пишется доказательство», второе — «для неисследимой меры даётся явное объявление» — механизм один (применение уточнённого типа), точка приложения разная. Области завершения не нужно писать функцию _proof.

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

Вселенная типов: предикаты времени компиляции находятся на уровне 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 (есть свободные переменные из рантайма): сохраняется рантайм-check — проверка Bool на уровне значений, инъекция в потокочувствительное множество гипотез Γ. Подробности см. в §11 конвейер диспетчеризации и §13 уточнение модели стирания.

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

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

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

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

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

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

Компромиссы

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

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

Недостатки

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

Снижение рисков

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

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

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

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

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

Фаза	Содержание
Фаза 1	Ядро компилятора: структурная эквивалентность + βδι-редукция + введение/элиминация кванторов всеобщности. Поддержка простых арифметических предикатов (`x > 0`, `arr.len > 0`)
Фаза 2	Слой трансляции в SMT-LIB + интеграция Z3/CVC5. Конвейер возвращает Proved/Disproved/Unproven. При Unproven поддержка функций-доказательств от программиста
Фаза 3	Генерация VC для инвариантов цикла + проверка завершения (четыре стратегии исследования меры + явная мера `Terminates`, §6, §6.9)
Фаза 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 / время 100 мс / глубина инстанцирования кванторов 3. Жёстко зашито в компиляторе, без ручек. В практическом использовании, если есть реальные случаи, доказывающие недостаточность (не «пользователь ошибся»), значения корректируются.
[x] Область поддержки кванторов: на уровне языка порядок кванторов не ограничен. Предикат времени компиляции принимает параметры Type — Type включает функциональные типы — поэтому кванторы высшего порядка — естественное следствие системы типов, специальный синтаксис не нужен. Решатель SMT может автоматически разрешать кванторы первого порядка (forall/exists, поддерживается чередующееся вложение, ограничено бюджетом глубины 3). Кванторы высшего порядка: SMT возвращает Unproven, компилятор подсказывает «этот предикат за пределами автоматического доказательства, предоставьте функцию-доказательство». Программист пишет функцию, чей возвращаемый тип равен утверждению — проверка типов верифицирует эту функцию. Не нужен внешний экспорт, не нужен ИИ, не нужен интерактивный режим доказательства. Всё — код YaoXiang, всё верифицируется проверкой типов.
[x] Форматирование контрпримеров: имена переменных исходного кода используются непосредственно как имена переменных SMT (с префиксом модуля для предотвращения коллизий). При возврате модели Z3 выполняется обратный поиск по именам переменных. Формат вывода: имя переменной = конкретное значение + позиция в исходном коде + позиция определения предиката. Сложный слой отображения не делается.
[x] ~~Взаимодействие предикатов времени компиляции со смарт-указателем ref?~~ → Решено: предикаты времени компиляции допускают только неизменяемые заимствования или значения с переданным владением. Значения с мутабельным заимствованием не могут появляться в предикатах времени компиляции.
[x] Расширение счётчика нарушений forall на несмежные операции? → Не расширяется. Текущая область покрытия (соседний обмен, соседний сдвиг) дополняется стратегией 1 (линейная ранговая функция) — сжатие внешнего интервала быстрой сортировки покрывается стратегией 1, пирамидальная сортировка покрывается стратегией 1 (паттерн индексов массива). Циклы, завершаемость которых не доказуема ни одной стратегией, компилятор отвергает напрямую — это философия жёсткой безопасности, не дефект. Если в будущем появятся реальные сценарии (не академические конструкции), которые не покрываются всеми четырьмя стратегиями, обсуждение возобновляется. → Обсуждение возобновлено (2026-09-14, #318): неструктурная рекурсия (такая как gcd без прямого убывания, взаимная рекурсия, рекурсия слияния-разделения) — это именно реальные сценарии, предвиденные этим пунктом — шаблонная последовательность исследования меры не может автоматически справиться с ними, и их невозможно переписать в анализируемые итеративные паттерны без потери читаемости. Заключение: философия жёсткой безопасности не меняется (неправильно написанная мера по-прежнему отклоняется SMT-контрпримером, человек может не суметь доказать, но не может доказать неверно), но «отказ при провале исследования» смягчается до «при провале исследования программист может явно указать меру в позиции типа» — см. §6.9.
[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/  │
│ (официальный проект) │  (остаётся на месте) │
└─────────────┘    └─────────────┘

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

Резюме ​

Мотивация ​

Почему RFC-022 устарел? ​

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

Правильная ментальная модель ​

Предложение ​

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

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

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

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

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

3.3 Стек гипотез ​

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

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

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

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

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

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

5. Единство трёх слоёв функций ​

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

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

7. Проверка завершения ​

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

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

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

6.4 Стратегия 3: паттерн ограниченного возрастания/убывания ​

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

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

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

6.8 Жёсткая граница ​

6.9 Явная мера: Terminates ​

8. Решатель SMT: модуль ускорения проверки типов ​

9. Композиция предикатов времени компиляции ​

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

9.1 Безопасность деления ​

9.2 Безопасность доступа к массиву ​

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

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

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

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

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

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

Изменения синтаксиса ​

Синтаксис ​

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

Представление в рантайме ​

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

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

Компромиссы ​

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

Недостатки ​

Снижение рисков ​

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

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

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

Зависимости ​

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

Ссылки ​

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

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

Резюме

Мотивация

Почему RFC-022 устарел?

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

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

Предложение

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

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

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

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

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

3.3 Стек гипотез

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

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

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

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

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

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

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

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

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

7. Проверка завершения

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

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

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

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

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

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

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

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

6.9 Явная мера: `Terminates`

8. Решатель SMT: модуль ускорения проверки типов

9. Композиция предикатов времени компиляции

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

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

9.2 Безопасность доступа к массиву

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

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

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

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

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

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

Изменения синтаксиса

Синтаксис

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

Представление в рантайме

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

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

Компромиссы

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

Недостатки

Снижение рисков

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

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

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

Зависимости

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

Ссылки

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