RFC-009a: Анализ жизненного цикла токенов — на основе конвейера доказательств Хоара

Родительский RFC: RFC-009: Проект модели владения
Зависимость: RFC-027: Предикаты времени компиляции и унифицированная статическая верификация
Предусловие: RFC-027 должен быть принят. Все механизмы данного RFC (конвейер доказательств, SMT-fallback, сбор путевых условий) зависят от реализации RFC-027.
Настоящий RFC исправляет и заменяет раздел RFC-009 §"Обнаружение конфликтов токенов: потоко-чувствительный анализ живости" (строки 663-684).

Резюме

В строке 684 RFC-009 утверждается, что обнаружение конфликтов токенов "не требует……NLL". Вывод верен, обоснование ошибочно.

Дело не в том, что "т.к. токены — это значения, достаточно линейного отслеживания". Дело в том, что: живость токенов — это логическое утверждение Хоара, а не специальный потоко-чувствительный анализ.

{все конфликтующие токены мертвы} op {WriteToken безопасно получен} — это тот же самый {P} op {Q}, который разделяет конвейер доказательств из RFC-027 с проверкой типов и верификацией предикатов. Никаких новых фреймворков анализа. Один конвейер, множество утверждений.

Мотивация

Путаница в RFC-009

RFC-009 смешивает две проблемы:

Линейное отслеживание (после Move недоступно) — {v не перемещён} use(v) {тип совпадает}. Уже есть в проверщике типов.
Взаимодействие жизненных циклов токенов (дочерний токен жив → родительский токен приостановлен → дочерний токен мёртв → родительский токен возрождается) — {все конфликтующие токены мертвы} write(data) {безопасно}. Требуется анализ живости, а не линейное отслеживание.

Текущее состояние кода

Компонент	Состояние
`BorrowChecker`	Линейное сканирование IR, пассивная реакция на явные инструкции `Borrow`/`Release`
`ControlFlowAnalyzer::analyze_instruction`	Пустая реализация (`control_flow.rs:145-153`)
`liveness_analysis`	Существует, но используется только для вставки Drop, не подключён к конфликтам токенов
Вставка Release	Жёстко закодирована после инструкций Call — чисто лексическая область видимости (`ir_gen.rs:2734-2736`)

Последствия для пользователя:

yaoxiang

data = vec![1, 2, 3]
view = &data              # Создание ReadToken
x = view.total_count      # Последнее использование view
data.push(4)              # ❌ Release(view) ещё не выполнен, ReadToken "жив"

Почему требуется переработка

Предыдущая версия (009a v1) использовала нарратив "DAG вместо NLL", вводя ненужные новые концепции (консервативные правила ветвления, специальная обработка циклов). Основное противоречие не было сформулировано ясно: проверка заимствований — это не отдельная система — она является одним из видов утверждений Хоара.

Основной проект

Всё есть Хоар

Проверка типов:   { x: Int }        x + 1        { result: Int }
Проверка заимств.: { view мёртв }    data.push(4)  { WriteToken успешно получен }
Верификация пред.: { y > 0 }         divide(x, y)  { result: Int }
Обрезка обратной дуги: { i == n }    следующая итерация цикла { cond == false }

Одна и та же форма {P} op {Q}. Компилятор для каждой операции генерирует предусловие P и отправляет его в конвейер доказательств для верификации.

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

Два типа предикатов, один конвейер

	Пользовательские предикаты	Системные предикаты (заимствования)
Генерация утверждений	Программист (аннотации типов)	Компилятор (дерево брендов + правила владения)
Предоставление доказательства	Компилятор + программист	Полностью автоматически компилятором
Если не доказано	Написать функцию-доказательство или рефакторить	Рефакторить код (ворота оставлены, но нужны крайне редко)
Видимость	Видны в сигнатуре	Неявные, не загрязняют сигнатуры типов
Стоимость обучения	Учишь только если хочешь использовать	Нулевая

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

Три режима отказа, один движок верификации. Утверждение типа не доказано → ошибка компиляции (необходимо). Утверждение заимствования не доказано → ошибка компиляции, рефакторинг (необходимо). Пользовательский предикат не доказан → ошибка компиляции, можно написать функцию-доказательство (обходимо). Стратегии отказа различаются, но движок верификации один и тот же — SMT-решатель + правила вывода ядра компилятора. Различие только в том, "кто отвечает за добавление доказательства, когда не получается" — компилятор отказывается писать за программиста доказательства заимствований (стратегия доказательства для заимствований — это структурный анализ + SMT, вмешательство программиста не требуется), но принимает функции-доказательства пользовательских предикатов от программиста. Это не несоответствие конвейера — это разные границы ответственности для разных категорий утверждений.

Это отличается от Rust 'a: 'a — обязательный курс, функция-доказательство — факультативный — подавляющее большинство пользователей никогда не столкнётся с факультативом.

Утверждения заимствований: автоматическая генерация компилятором

Пользователь пишет data.push(4). Компилятор автоматически генерирует утверждение:

WriteToken(data, node) может быть получен
  = forall t в conflicting_tokens(data): t в node мёртв
  = forall t в brand_tree.children(data): forward_reachable(node) ∩ consumers(t) == ∅

Три правила, ноль особых случаев:

Дерево брендов (RFC-009 §2.7) отвечает на вопрос "кто с кем конфликтует": сопоставление префиксов, O(глубина), глубина ≤ 3
Список потребителей (автоматически собирается при построении DAG) отвечает на вопрос "кто последним потребил токен"
Прямая достижимость отвечает на вопрос "может ли потребитель ещё быть выполнен": структурная обрезка + логическая обрезка

Прямая достижимость: обратное обходное исследование от потребителя

Для каждого потребителя C токена T:

Из C запускается обратный BFS по DAG.
Ребро обрезается, если:
  1. Это break (структурная обрезка)
  2. Условие пути ⇒ !loop_cond доказано SMT как истинное (логическая обрезка, конвейер RFC-027)

Распространить по всем необрезанным рёбрам в обратном направлении (включая обратные рёбра, которые переносят живость в предыдущую итерацию).
Пометить все достижимые узлы → unsafe.

Запрос: операция записи в узле W → W ∉ unsafe → безопасно.

Не нужно изобретать "консервативные правила ветвления". Не нужно "консервативного сохранения живости в циклах". Один обратный BFS + два правила обрезки.

Стратегия доказательства: быстрый путь первый, SMT как страховка

Каждая операция записи, требующая токен
  │
  ├→ Быстрый путь: структурный анализ DAG (покрывает 95%+ сценариев)
  │     │
  │     ├→ Сопоставление префиксов в дереве брендов → найти конфликтующие токены (O(глубина))
  │     ├→ Обратный BFS, break обрезает обратные рёбра
  │     └→ Нет проходимых обратных рёбер → непосредственный вердикт Proved / Disproved
  │
  └→ Медленный путь: логическая обрезка SMT (только когда быстрый путь встречает проходимое обратное ребро)
        │
        ├→ Начало обратного ребра имеет условие пути → SMT проверяет path_cond ⇒ !loop_cond
        │     ├→ Proved → логическая обрезка → возврат к быстрому пути
        │     └→ Disproved / Unproven → обратное ребро проходимо → пометить unsafe
        │
        └→ Начало обратного ребра не имеет условия пути → обратное ребро проходимо напрямую

Покрытие быстрого пути: линейный код, if/else, loop + break, while без условий пути. Покрытие медленного пути: тело цикла while, когда условие пути подразумевает выход из цикла. Не покрывается: условия времени выполнения, которые не могут быть статически доказаны → обратное ребро проходимо → unsafe → ошибка компиляции (пользователь рефакторит).

SMT — не главная сила, а страховочная сетка. В отличие от пользовательских предикатов RFC-027: пользовательские предикаты полагаются на SMT как на главную силу; системные предикаты заимствований полагаются на структурный анализ как на главную силу, а SMT дополняет только те угловые случаи, куда структурный анализ не дотягивается.

SMT — это слой точности, а не зависимость soundness. Полностью sound-решение для системных предикатов заимствований обеспечивается быстрым путём (интервалы + обратный BFS + обрезка break); логическая обрезка SMT только определяет «пропускать ли легальные программы с границами циклов». Когда SMT недоступен / тайм-аут / не реализован (RFC-027 impl: in_progress), fallback = обратное ребро проходимо = консервативный отказ, и то, что должно быть отвергнуто, всё равно будет отвергнуто. Консервативность без SMT = любое заимствование+запись в цикле отвергается, на одном уровне с Rust NLL (производственная проверка заимствований в Rust также не использует SMT). Внедрение SMT — это чистый прирост точности, не блокирующий поставку sound-основной линии.

Анализ случаев использования

Линейный код

yaoxiang

data = vec![1, 2, 3]        # Узел 1
view = &data                # Узел 2: потребляет data, производит ReadToken(#1)
x = view.total_count        # Узел 3: потребляет view (= последний потребитель #1)
data.push(4)                # Узел 4: требует WriteToken(data)

Обратный BFS из view.total_count (узел 3) → узел 3 — последний потребитель #1 → узел 4 > узел 3 → узел 4 не в unsafe → ✅

if/else: без специальных правил

yaoxiang

view = &data
if cond {
    use(view)               # then-ветвь потребляет view
} else {
    do_something_else()     # не трогает view
}
data.push(4)                # Последний потребитель view в if → после if нет потребителей → ✅

if/else — это составной узел DAG. Внутреннее потребление приписывается этому узлу. Не объединять состояние ветвей. Не консервативный арбитраж. Есть ли потребитель после — целочисленное сравнение.

Уточнение: "не объединять состояние ветвей" относится только к живости заимствований (обратный BFS потребителей бренда). Состояние move (владение переменными) — это отдельный анализ: прямой поток данных по узлам CFG (стиль NLL/Polonius), при слиянии ветвей консервативный meet (любая ветвь Moved → слияние Moved), недостижимые литерально ветви (if false) не участвуют. Два слоя разделены: живость заимствований смотрит на "есть ли будущие потребители", анализ move смотрит на "возможно ли переменная уже перемещена".

if/else с побегом возвращаемого значения

yaoxiang

view = &data
result = if cond {
    view                     # view убегает в result
} else {
    something_else
}
use(result)                  # Косвенное потребление view
data.push(4)                 # view всё ещё имеет потребителей (use(result))
                             # → push в unsafe → ❌ Правильная ошибка

view убегает через возвращаемое значение → use(result) — потребитель view → от push в обратном направлении можно достичь use(result) → unsafe.

Цикл: break обрезает обратное ребро

yaoxiang

view = &data
loop {
    use(view)                # consumer
    if is_last {
        data.push(4)         # Операция записи
        break                # ← Структурная обрезка
    }
}

Обратный BFS из use(view) → обратное ребро → вперёд к data.push(4) → встречает break → обрезано → data.push(4) не в unsafe → ✅

Без break:

yaoxiang

view = &data
loop {
    use(view)
    data.push(4)             # Нет обрезки break → обратное ребро проходимо → следующий use(view) достижим
                             # → push в unsafe → ❌ Правильная ошибка
}

while: логическая обрезка SMT

yaoxiang

view = &data
mut i: UpTo(n) = 0
while i < n {
    use(view)                # consumer
    i += 1
    if i == n {
        data.push(4)         # Условие пути: i == n
    }
}

Обратный BFS из use(view) → обратное ребро → к data.push(4) → проверка условия пути i == n → SMT-запрос: i == n ⇒ !(i < n)? → Proved → логическая обрезка → data.push(4) не в unsafe → ✅

Заметьте, что цель проверки — это условие пути самого узла записи (i == n принадлежит data.push(4) внутри ветви if), а не условие пути узла обратного ребра.

Суть: ID бренда — это и есть `'a`

Не говорим "нам не нужен 'a". Говорим "#42 — это и есть '42".

Rust	YaoXiang	Эквивалентность
`'a`	`#42`	Идентификатор времени жизни на этапе компиляции
`'a: 'b` outlives-ограничение	`#42` — префикс `#42.field_x`	Сравнение строковых префиксов = частичный порядок
Распространение живости NLL (неподвижная точка CFG)	Обратный BFS (DAG)	Оба вычисляют достижимость
Факты Polonius	Логическая обрезка SMT	Оба выводят по условиям пути
Решение системы ограничений в неподвижной точке	Сопоставление префиксов дерева брендов + BFS	Разные кодировки, та же проблема

Мы не изобрели новый анализ. Мы просто опустили 'a с уровня сигнатур типов на уровень доказательств. ID бренда делает в точности то же, что 'a — помечает идентичность заимствования, отслеживает отношение порождения, выносит вердикт о конфликте. Разница только одна: 'a находится в сигнатуре типа, написанной пользователем; #42 находится внутри компилятора.

Это не зазорно. Карри-Ховард говорит: типы — это утверждения, программы — доказательства. 'a не является частью утверждения — это часть стратегии доказательства. Rust записал стратегию доказательства в сигнатуру утверждения. Мы вернули её туда, где ей место.

Что устраняют ограничения языкового дизайна

Источник сложности	Устранён?	Причина
Затенение переменных	✅	Язык запрещает — одно имя всегда ссылается на одно и то же
Заимствования через for-итерации	✅	Каждая итерация — новая привязка — естественная изоляция между итерациями
Аннотации времени жизни `'a`	✅	Путь бренда = `#42.field_x`, выводится компилятором
Именованные времена жизни + распространение ограничений	✅	Сравнение префиксов пути бренда заменяет явные множества ограничений
Решение ограничений графа заимствований (Polonius)	✅	Сопоставление префиксов дерева брендов + запрос потребителей DAG
Распространение живости заимствований в теле цикла	❌	Требует обработки, как в Rust — используем обратный BFS + логическую обрезку
Консервативность условных ветвей	❌	Как в Rust — SMT покрывает доказуемое, остальное консервативно отвергается

Почему DAG осуществим

Три ограничения языкового дизайна YaoXiang делают анализ DAG осуществимым:

Без затенения переменных — одно имя всегда ссылается на одно и то же, не нужно отслеживать через перепривязку
for создаёт новую привязку в каждой итерации — естественная изоляция между итерациями, нет межитерационных заимствований
Структурированная конкуррентность — границы задач ясны, не нужно распространять живость между задачами

Эти ограничения устраняют основные источники сложности итерации неподвижной точки CFG в Rust. Не DAG "более продвинутый", чем CFG — более простой языковой дизайн позволяет более простой анализ.

Детальный проект

Список системных предикатов

Компилятор автоматически генерирует следующие утверждения, отправляя их в конвейер доказательств RFC-027:

Системный предикат	Момент срабатывания	Форма утверждения
`borrow_conflict`	Требуется WriteToken(v)	`forall t ∈ conflicting(v): dead_at(t, node)`
`use_after_move`	Использование переменной v	`¬moved(v)`
`use_after_drop`	Использование переменной v	`¬dropped(v)`
`double_drop`	Drop(v)	`¬dropped(v)`
`mut_violation`	Запись в неизменяемую переменную v	`is_mut(v)`

Существующие BorrowChecker, MoveChecker, DropChecker, MutChecker становятся генераторами утверждений — не исчезают, меняют идентичность. Они генерируют утверждения, конвейер их верифицирует.

Дерево брендов

Механизм брендов из RFC-009 §2.7 формализован как дерево брендов.

Семантика токенов — заморозка первична, не копируемость:

Сущностное различие между &T и &mut T не в том, "можно ли копировать", а в том, "разрешена ли одновременная запись":

ReadToken(T):  Предоставляет разрешение только на чтение, одновременно замораживая исходные данные T —
               любой WriteToken(T) в этот период не может быть получен. Заморозка —
               первичная семантика ReadToken. Dup (копируемость) — следствие заморозки:
               поскольку данные заморожены (мутация невозможна), множественные
               представления только для чтения по природе безопасны.

WriteToken(T): Предоставляет исключительное разрешение на чтение и запись. Поскольку запись существует,
               никакой другой токен (чтение или запись) не может сосуществовать. Не реализует
               Dup (линейный тип) — следствие исключительности.

Причинно-следственная связь:

Существование ReadToken → исходные данные заморожены → множественное чтение безопасно → Dup
                                  ↓
                  WriteToken отвергается (системный предикат borrow_conflict принуждает)

А не:

ReadToken имеет Dup → может быть несколько → заодно проверяем конфликт  ← Инверсия причинности

BrandTree:
  nodes: Map<BrandId, BrandNode>

BrandNode:
  id: BrandId               # "#42", "#42.field_x"
  kind: ReadToken | WriteToken
  source_var: Operand
  parent: Option<BrandId>   # Родительский узел в отношении порождения
  children: Set<BrandId>    # Порождённые дочерние токены
  consumers: Set<NodeId>    # Узлы DAG, потребляющие этот токен
  ref_count: usize          # Число безопасных копий в период заморозки ReadToken

Проверка конфликтов — механизм обеспечения гарантии заморозки:

rust

fn conflicts(a: &BrandId, b: &BrandId) -> bool {
    // Условие конфликта: один источник + хотя бы одна запись + перекрытие путей бренда
    // Это означает:
    //   1. ReadToken против ReadToken → нет конфликта (оба только для чтения, нет мутации)
    //   2. WriteToken против ReadToken → конфликт (запись нарушает гарантию заморозки чтения)
    //   3. WriteToken против WriteToken → конфликт (две записи не могут сосуществовать)
    a.source() == b.source()
        && (a.is_write() || b.is_write())
        && (a.is_prefix_of(b) || b.is_prefix_of(a))
}

O(глубина) сравнение строковых префиксов, глубина ≤ 3. Константный уровень.

Анализ живости обратным BFS

Этот алгоритм вводит измерение "времени создания токена". Живость токена — это интервал[created_at, last_use], а не множество обратной достижимости; операция записи составляет конфликт только внутри интервала живости токена — это покрывает легальный порядок "запись сначала, заимствование потом" (§2.4 семантика: токен параметра освобождается по окончании вызова), избегая ложных срабатываний.

Алгоритм: check_borrow(token, node, dag, brand_tree)

Вход:
  token: WriteToken, который нужно проверить
  node:  Узел DAG, в котором находится операция записи

Выход: Proved | Disproved

Алгоритм:
  # Быстрый путь: обратный BFS
  unsafe = empty_set
  queue = brand_tree.consumers(token)

  while queue не пуста:
    cur = queue.pop()
    unsafe.add(cur)

    for each pred in dag.predecessors(cur):
      # Структурная обрезка: break не проходим
      if pred является break-ребром:
        continue

      # Обратное ребро → проверить, нужен ли SMT-fallback
      if pred является обратным ребром:
        path_cond = условие пути узла записи node   # Цель проверки — условие самого узла записи
        loop_cond = условие цикла
        # Сначала проверить, можно ли обрезать структурно (соответствующий break уже обрезал путь → сюда не дойдёт)
        # Затем проверить условие пути
        if path_cond не пусто:
          result = smt_fallback(path_cond, loop_cond)   # ← Медленный путь
          if result == Proved:
            continue                    # Логическая обрезка
        # Нет условия пути или SMT не доказал → проходим обратное ребро
        # fall through

      if pred ∉ unsafe:
        queue.push(pred)

  # Вердикт (запись сначала, заимствование потом)
  # node < created_at(token) → во время записи токен ещё не существует → Safe
  if node ∈ unsafe и created_at(token) ≤ node:
    return Disproved
  else:
    return Proved


smt_fallback(path_cond, loop_cond):
  # Вызывается только при обратном ребре + наличии условия пути
  # Использует конвейер доказательств RFC-027, разделяя тот же SMT-решатель и бюджет
  return smt.prove(path_cond ⇒ !loop_cond)
  # Proved → логическая обрезка
  # Disproved / Unproven → не обрезаем, обратное ребро проходимо (консервативный отказ)
  # SMT недоступен/тайм-аут/не реализован = ветвь Disproved —
  # SMT влияет только на точность (пропускаются ли легальные программы), не на soundness (то, что должно быть отвергнуто, будет отвергнуто);
  # консервативность без SMT = любое заимствование+запись в цикле отвергается, на одном уровне с Rust NLL.

BrandNode получает дополнительное поле:

BrandNode:
  ...
  created_at: NodeId         # Узел создания токена (левый конец интервала заимствования)

O(N), где число вызовов SMT = число обратных рёбер × доля обратных рёбер с условиями пути. В реальном коде вызовы SMT крайне редки — только в теле цикла while при наличии переменных с уточнёнными типами в условиях пути.

Сбор условий пути

Предоставляется существующими механизмами RFC-027 §3.2-3.3:

if-guard: if y > 0 → в true-ветвь помещается y > 0
match-паттерн: if let Some(v) = opt → в ветвь помещается opt == Some(v)
Присваивание: i += 1, компилятор поддерживает информацию о диапазонах значений
while cond: в тело цикла помещается cond == true

Каждый узел DAG несёт множество условий пути. При обратном BFS по обратному ребру берётся условие пути начала обратного ребра, SMT проверяет, исключает ли оно условие входа в следующую итерацию.

Правила распространения условий пути:

Условие пути прикрепляется к самому узлу записи: операция записи W внутри ветви несёт условие своей ветви (if i == n { W } → path_cond(W) = i == n). При прохождении обратного ребра через обратный BFS SMT проверяет path_cond(W) ⇒ !loop_cond (путь, ведущий к W, неизбежно выходит из цикла → потребитель следующей итерации недостижим → обрезка), а не условие пути узла обратного ребра.
Консервативная очистка при join: точка слияния if/else не несёт условий пути из ветвей (дизъюнкция условий ветвей обычно неразрешима, очищается напрямую). У операции записи после точки слияния path_cond пуст → обратное ребро проходимо.
Семантизация условий пути: path_cond — это ConstExpr (семантика из RFC-027 §3.2), а не исходный текст; smt_cut переводит его в SMT-ограничения и решает.
Нет условия пути → обратное ребро проходимо напрямую (unsafe), SMT не вызывается.

Интерфейс с RFC-027

Системные предикаты заимствований и пользовательские предикаты разделяют один конвейер доказательств — различие в основной стратегии доказательства:

Тип запроса	Источник утверждения	Основная стратегия	Fallback
Равенство типов	Проверщик типов	Структурная эквивалентность	—
Пользовательский предикат	Аннотация типов программиста	SMT	Функция-доказательство программиста
Конфликт заимствований	Автоматически генерируется компилятором	Структурный анализ DAG (быстрый путь)	Логическая обрезка SMT

Роль SMT-решателя в проверке заимствований: не главная сила, а страховочная сетка. Вызывается только тогда, когда обратное ребро while требует логической обрезки. Подавляющее большинство проверок заимствований завершается на быстром пути — O(N) обратный BFS, нулевые накладные расходы SMT.

Связь с существующим кодом

Существующий компонент	Обработка
`BorrowChecker`	Становится `BorrowPredicateEmitter` — генерирует утверждения Хоара для заимствований
`MoveChecker`	Становится `MovePredicateEmitter` — генерирует утверждения `¬moved(v)`
`DropChecker`	То же самое — генерирует утверждения, связанные с Drop
`MutChecker`	То же самое — генерирует утверждения `is_mut(v)`
`ControlFlowAnalyzer`	Больше не нужен — конвейер обрабатывает унифицированно
`liveness_analysis`	Сохраняется — вставка Drop по-прежнему нуждается в информации о живости переменных
Жёстко закодированный Release в `ir_gen.rs`	Удаляется — позиция Release определяется анализом потребителей DAG

NLL и границы итераций

Живость токена — это интервал [created_at, last_use], а не множество обратной достижимости. created_at = узел создания токена; last_use = максимальный узел потребления из анализа потребителей. Необходимое и достаточное условие конфликта между записью W и токеном T: conflicts(T, W) ∧ created_at(T) ≤ node(W) ∧ node(W) может прямо достичь last_use(T) (определяется обратным BFS). Легальный порядок "запись сначала, заимствование потом" (§2.4: токен параметра освобождается по окончании вызова) напрямую исключается условием created_at(T) ≤ node(W), без каких-либо специальных правил. Эта модель делает утверждение §Достоинства 5 "алгоритм не консервативен" верным при любом порядке.

Момент смерти токена = точка последнего использования (NLL), а не конец лексической области видимости.

Это естественное следствие анализа потребителей: позиции потребителей определяют последнее использование токена. use(v) — потребитель v → v умирает сразу после use(v). Не нужны дополнительные {} или drop() для досрочного завершения жизненного цикла токена.

Граница итерации цикла — это линия смерти копий токена. Три правила:

Правило 1: Переменные, объявленные внутри цикла, автоматически умирают в конце каждой итерации.
        for каждая итерация — новая привязка (гарантия дизайна языка), loop — то же самое.

Правило 2: ref_count дерева брендов на заголовке цикла учитывает только копии, созданные снаружи цикла.
        Новые копии, созданные Dup внутри цикла, обнуляются по ref_count на границе итерации.

Правило 3: При прохождении обратного ребра через обратный BFS не переносится информация о живости текущей итерации.
        Переносится только ref_count на заголовке цикла (т.е.: копии снаружи цикла).

Пример:

yaoxiang

view = &data                          # Заголовок цикла: ref_count = 1, consumer = use(view)
loop {
    v2: &Point = view                 # Dup внутри цикла → ref_count = 2
    use(v2)                           # consumer: последнее использование v2 → v2 умирает → ref_count = 1
    data.push(4)                      # ✅ Безопасно! v2 мёртв, остался только view (ref_count = 1, без конфликта записи)
    # Граница итерации: правило 3 — v2 не переносится в следующую итерацию. В начале следующей итерации v2 пересоздаётся новой привязкой.
}

Этот проект не требует дополнительных правил "консервативного сохранения живости в цикле". Обратный BFS запускается из потребителя, потребитель находится в теле цикла → живость ограничена текущей итерацией → обратное ребро не проходимо. Полностью согласуется с примером цикла из §Анализ случаев использования RFC-009a.

`?`-распространение ошибок и область видимости как источник Release

? — это досрочный возврат — помимо нормального выхода из области видимости существует дополнительный путь выхода. Токены должны быть освобождены на этом пути, неправильный порядок освобождения — UB.

Инструкция Release генерируется анализом областей видимости, а не жёстко закодирована после Call.

Компилятор поддерживает список точек выхода для каждой области видимости:

} (нормальное завершение области видимости)
? (распространение ошибки, досрочный return)
Явный return

В каждой точке выхода, в обратном порядке объявления (LIFO), вставляются инструкции Release для всех живых токенов в этой области видимости. Отношения родитель-потомок в дереве брендов автоматически обрабатывают каскадное освобождение порождённых токенов:

yaoxiang

Point.get_x: (self: &Point) -> (&Float, &Point) = {
    return (&self.x, self)    # Возврат дочернего токена &Float + родительского токена &Point
}

fn use_case(p: Point) -> Result<(), Error> = {
    (x_ref, p_ref) = p.get_x()?   # Если ? распространяет:
    # Дерево брендов знает, что x_ref — порождение p_ref (#42.field_x — префикс #42)
    # Порядок освобождения: x_ref (потомок) → p_ref (родитель) → LIFO выполняется автоматически
    p.modify()                     # WriteToken — все ReadToken уже освобождены
    Ok(())
}

Расположение реализации: остаётся в ir_gen.rs, становится управляемым областью видимости — без введения нового прохода компилятора.

Сложность в таблице выше — это проектные оценки, не измеренные; "~1ms" и "крайне редко" следует рассматривать как порядок ожиданий, а не измеренных значений; после реализации они будут откалиброваны по наблюдаемым данным.

Условия срабатывания SMT-fallback крайне строгие: одновременно выполняются (1) цикл while (2) в теле цикла есть операция записи (3) после операции записи есть условие пути, по которому можно судить о завершении цикла (4) компилятору нужно полагаться на это условие для обрезки обратного ребра. В реальном коде доля значительно ниже 1%. Остальные проверки заимствований все завершаются на быстром пути.

Связь с пользовательскими предикатами RFC-027: пользовательские предикаты полагаются на SMT как на главную силу, системные предикаты заимствований полагаются на структурный анализ как на главную силу. Оба разделяют один и тот же SMT-решатель и верхний предел бюджета (RFC-027 §8), но системные предикаты заимствований почти не потребляют бюджет SMT.

Линейный код → нет обратных рёбер → слой 1 O(N) моментально. Цикл + условие пути → вызов SMT, линейная арифметика на уровне миллисекунд (бюджет RFC-027 100ms). Результат одного BFS может быть кэширован для повторного использования при нескольких запросах к тому же токену.

Дизайн сообщений об ошибках

Основной принцип: в сообщениях об ошибках появляются только символы, написанные пользователем.

Ошибки Rust, связанные с заимствованиями, делятся на две категории:

Ошибки на уровне переменных: E0597 (живёт недостаточно долго), E0502 (изменяемое+неизменяемое одновременное заимствование), E0499 (множественные изменяемые заимствования). Rust уже является эталоном — имя переменной + номер строки, без 'a. YaoXiang имеет ту же точность. Вся информация в дереве брендов: точка создания токена, позиции потребителей, точка запроса.

Ошибки на уровне сигнатур: E0623 (lifetime mismatch), E0106 (missing lifetime specifier), E0477 (не выполнено required lifetime). Вращаются вокруг 'a. YaoXiang не имеет таких ошибок — в сигнатуре нет 'a. Не "нельзя сообщить", а о том, о чём пользователь не писал, не сообщается.

Пример конфликта внутри функции:

ошибка: `data` заморожен, невозможно получить изменяемое разрешение
 --> src/main.yx:5:9
2 |     view = &data
  |            ----- `data` заморожен (токен только-для-чтения создан здесь)
4 |         use(view)
  |             ---- `view` всё ещё используется здесь, заморозка не снята
5 |         data.push(4)
  |         ^^^^ здесь требуется изменяемое разрешение

(Та же точность, что у Rust E0499 — имя переменной + номер строки, без ID бренда.)

Пример межфункционального побега:

ошибка: один из источников данных, удерживаемых `num` (строка 4), — это `default_str` (строка 3),
но `default_str` становится недействительным в строке 6, а `num` всё ещё используется в строке 5.

рассмотрите: переместите объявление `default_str` в вызывающую функцию, или используйте `ref default_str` для совместного удержания.

(Та же точность, что у Rust E0597. Сводка бренда знает, что у num есть два пути источника — уже есть в компиляторе, формулировка ошибки может использоваться.)

Исправления к основному тексту RFC-009

Раздел RFC-009 §"Обнаружение конфликтов токенов: потоко-чувствительный анализ живости" обновлён:

Удалено "то, что не нужно:……NLL" — не потому что вывод неверен, а потому что обоснование неверно ("т.к. токены — это значения, достаточно линейного отслеживания")
Переходный план слой 1/слой 2 сохранён, полный план указывает на этот RFC
Уточнено: ID бренда (#42) — это и есть 'a — информация полностью та же, кодировка другая. Не изобретён новый анализ — время жизни перенесено с уровня типов на уровень доказательств

Компромиссы

Достоинства

Сигнатуры типов не содержат времён жизни: #42 — это и есть '42 — та же информация, закодированная в дереве брендов, не выставленная в сигнатуре типа. Этот пункт неопровержим: посчитайте, сколько параметров 'a требуется в Rust для обобщённого типа с 3 параметрами-ссылками, и сколько в YaoXiang. Ответ: 3 против 0.
Концептуальное единство: проверка заимствований и пользовательские предикаты разделяют один конвейер доказательств — {P} op {Q}, конвейер верифицирует P. Карри-Ховард согласовано.
Ноль новых фреймворков анализа: не вводится новый фреймворк анализа. Пользователь не воспринимает существование "проверщика заимствований" — как пользователь не воспринимает деталей реализации "проверщика типов".
Сообщения об ошибках содержат только символы, написанные пользователем: исчезает целое измерение категорий ошибок (E0623, E0106, E0477 — все вращаются вокруг 'a). Ошибки на уровне переменных — на одном уровне точности с Rust.
Алгоритм не консервативен: обратный BFS + обрезка break + логическая обрезка SMT. Не нужно "консервативного сохранения живости в цикле". Не нужно "консервативного слияния ветвей".

Недостатки

Не новое изобретение: ID бренда делает в точности то же, что 'a — сложность решения ограничений внутри компилятора не исчезла, только способ кодирования изменился с "имя переменной + множество ограничений" на "путь бренда + сопоставление префиксов". Для конечного пользователя различие только в том, что в сигнатуре не пишется 'a.
Полностью новая реализация: дерево брендов в коде существует только как концепция, требует реализации с нуля. BorrowChecker, ControlFlowAnalyzer заменяются.
Зависимость от SMT: логическая обрезка зависит от Z3 (уже введён в RFC-027, новых зависимостей нет). Но проверка заимствований почти не срабатывает — только при while + условии пути.
Крайне редкие шаблоны требуют рефакторинга: межветвевые заимствования, которые компилятор не может автоматически доказать, требуют от пользователя рефакторинга кода. Отличается от резервного варианта Rust с 'a: в Rust есть 'a как инструмент (аннотация — и проходит); резервный вариант YaoXiang (функция-доказательство) не входит в MVP.

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

Альтернатива	Почему не выбрана
Реализовать полный Rust NLL	Ограничения дизайна YaoXiang (без затенения, for — новая привязка) уже устранили основные источники сложности NLL, неподвижная точка CFG не нужна
Сохранить текущее (жёстко закодированный Release)	Недостаточно — пользователь должен вручную управлять областью видимости токенов
Анализ только в spawn-блоках	Недостаточно — использование токенов в не-spawn коде — большинство
GC вместо проверки заимствований	Нарушает принципы дизайна языка — в YaoXiang нет GC

Этапы реализации

Этап	Содержание	Зависимости
Phase 1	Реализация структуры данных дерева брендов	—
Phase 2	Генераторы системных предикатов (Borrow/Move/Drop/Mut → утверждения)	Phase 1
Phase 3	Анализ живости обратным BFS + подключение к конвейеру (слой 1)	Phase 2
Phase 4	Сбор условий пути + логическая обрезка SMT (слой 2)	Phase 3 + RFC-027 Phase 2
Phase 5	Инструкции Release переведены на управление от потребителей DAG	Phase 3
Phase 6	Удаление ControlFlowAnalyzer, рефакторинг BorrowChecker	Phase 4

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

[x] Семантика ref_count дерева брендов при развёртке цикла между итерациями — через NLL: токен умирает после последнего использования. Копии, привязанные внутри цикла, умирают на границе итерации, обратный BFS не переносит живость между итерациями. См. §NLL и границы итераций.
[x] Порядок освобождения токенов на пути распространения ошибки ? — Release управляется анализом областей видимости (остаётся в ir_gen.rs). В каждой точке выхода области видимости (}, ?, явный return) живые токены освобождаются в порядке LIFO. Отношения родитель-потомок в дереве брендов автоматически обрабатывают каскадное освобождение. См. §?-распространение ошибок и область видимости как источник Release.
[ ] Синтаксис функции-доказательства (далёкая перспектива, не MVP — не блокирует ни одну фазу)

Ссылки

RFC-009: Проект модели владения — Родительский RFC
RFC-027: Предикаты времени компиляции и унифицированная статическая верификация — Конвейер доказательств
RFC-010: Унифицированный синтаксис типов — Семантика {}
RFC-024: Модель конкуррентности на основе spawn-блоков — DAG spawn

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

Состояние	Расположение	Описание
Принято	`docs/design/rfc/accepted/`	Становится официальным проектным документом

RFC-009a: Анализ жизненного цикла токенов — на основе конвейера доказательств Хоара ​

Резюме ​

Мотивация ​

Путаница в RFC-009 ​

Текущее состояние кода ​

Почему требуется переработка ​

Основной проект ​

Всё есть Хоар ​

Два типа предикатов, один конвейер ​

Утверждения заимствований: автоматическая генерация компилятором ​

Прямая достижимость: обратное обходное исследование от потребителя ​

Стратегия доказательства: быстрый путь первый, SMT как страховка ​

Анализ случаев использования ​

Линейный код ​

if/else: без специальных правил ​

if/else с побегом возвращаемого значения ​

Цикл: break обрезает обратное ребро ​

while: логическая обрезка SMT ​

Суть: ID бренда — это и есть 'a ​

Что устраняют ограничения языкового дизайна ​

Почему DAG осуществим ​

Детальный проект ​

Список системных предикатов ​

Дерево брендов ​

Анализ живости обратным BFS ​

Сбор условий пути ​

Интерфейс с RFC-027 ​

Связь с существующим кодом ​

NLL и границы итераций ​

?-распространение ошибок и область видимости как источник Release ​

Дизайн сообщений об ошибках ​

Исправления к основному тексту RFC-009 ​

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

Достоинства ​

Недостатки ​

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

Этапы реализации ​

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

Ссылки ​

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

RFC-009a: Анализ жизненного цикла токенов — на основе конвейера доказательств Хоара

Резюме

Мотивация

Путаница в RFC-009

Текущее состояние кода

Почему требуется переработка

Основной проект

Всё есть Хоар

Два типа предикатов, один конвейер

Утверждения заимствований: автоматическая генерация компилятором

Прямая достижимость: обратное обходное исследование от потребителя

Стратегия доказательства: быстрый путь первый, SMT как страховка

Анализ случаев использования

Линейный код

if/else: без специальных правил

if/else с побегом возвращаемого значения

Цикл: break обрезает обратное ребро

while: логическая обрезка SMT

Суть: ID бренда — это и есть `'a`

Что устраняют ограничения языкового дизайна

Почему DAG осуществим

Детальный проект

Список системных предикатов

Дерево брендов

Анализ живости обратным BFS

Сбор условий пути

Интерфейс с RFC-027

Связь с существующим кодом

NLL и границы итераций

`?`-распространение ошибок и область видимости как источник Release

Дизайн сообщений об ошибках

Исправления к основному тексту RFC-009

Компромиссы

Достоинства

Недостатки

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

Этапы реализации

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

Ссылки

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