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

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

Аннотация

Строка 684 RFC-009 утверждает, что обнаружение конфликтов токенов "не требует... NLL". Вывод правильный, аргументация ошибочна.

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

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

Мотивация

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

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

Линейное отслеживание (после перемещения недоступно) — {v не перемещён} use(v) {тип совпадает}. Имеется в типоchecker.
Взаимодействие времени жизни токенов (дочерний токен жив → родительский приостановлен → дочерний умер → родительский возрождён) — {все_конфликтующие_токены_мертвы} 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 in conflicting_tokens(data): t мёртв в node
  ≡ forall t in brand_tree.children(data): forward_reachable(node) ∩ consumers(t) == ∅

Три правила, ноль исключений:

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

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

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

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

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

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

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

Стратегия доказательства: быстрый путь приоритетен, СМТ как fallback

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

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

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

Анализ вариантов использования

Линейный код

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. Внутреннее потребление атрибутируется этому узлу. Без слияния состояний ветвей. Без консервативного голосования. Есть ли потребители дальше — простое сравнение целых.

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)                # Потребитель
    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: СМТ логический разрыв

yaoxiang

view = &data
mut i: UpTo(n) = 0
while i < n {
    use(view)                # Потребитель
    i += 1
    if i == n {
        data.push(4)         # path_condition: i == n
    }
}

Обратный BFS от use(view) → обратное ребро → до data.push(4) → проверка path_condition i == n → СМТ запрос: i == n ⇒ !(i < n)? → Proved → Логический разрыв → data.push(4) не в unsafe → ✅

Суть: Brand ID — это и есть `'a`

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

Rust	YaoXiang	Эквивалентность
`'a`	`#42`	Времяной идентификатор времени жизни
`'a: 'b` ограничение lifespan	`#42` — префикс `#42.field_x`	Сравнение строковых префиксов = частичный порядок
NLL жизнеспособность (неподвижная точка CFG)	Обратный BFS (DAG)	Оба — вычисления достижимости
Факты Polonius	СМТ логический разрыв	Оба — вывод по path_condition
Решение ограничений (неподвижная точка)	Brand tree префикс + BFS	Различные кодировки, одна задача

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

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

Какие сложности устранены языковыми ограничениями

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

Почему 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 {
    // Условие конфликта: общий источник + хотя бы один записывающий + brand path пересекаются
    // Это означает:
    //   1. ReadToken vs ReadToken → Нет конфликта (оба только читают, мутации нет)
    //   2. WriteToken vs ReadToken → Конфликт (запись нарушает гарантию заморозки чтения)
    //   3. WriteToken vs WriteToken → Конфликт (две записи не могут сосуществовать)
    a.source() == b.source()
        && (a.is_write() || b.is_write())
        && (a.is_prefix_of(b) || b.is_prefix_of(a))
}

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

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

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

Вход:
  token: WriteToken для проверки
  node:  Узел DAG, где находится операция записи

Выход: Proved | Disproved

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

  while queue not empty:
    cur = queue.pop()
    unsafe.add(cur)

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

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

      if pred ∉ unsafe:
        queue.push(pred)

  # Решение
  if node ∈ unsafe:
    return Disproved
  else:
    return Proved


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

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

Сбор path_condition

Обеспечивается существующими механизмами RFC-027 §3.2-3.3:

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

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

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

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

Тип запроса	Источник пропозиции	Главная стратегия	Fallback
Типовое равенство	Типоchecker	Структурная эквивалентность	—
Пользовательские предикаты	Аннотации типов программиста	СМТ	Доказательная функция программиста
Конфликт заимствований	Автогенерация компилятором	Структурный анализ DAG (быстрый путь)	СМТ логический разрыв

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

Отношение с существующим кодом

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

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

Момент смерти токена = точка последнего использования (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)                           # Потребитель: последнее использование v2 → v2 умирает → ref_count = 1
    data.push(4)                      # ✅ Безопасно! v2 мёртв, остался только view (ref_count = 1, не конфликт записи)
    # Граница итерации: Правило 3 — не переносить v2 в следующий раунд. В начале следующей итерации v2 recreируется новой привязкой.
}

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

`?` Распространение ошибок и Release, управляемый областями видимости

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

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

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

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

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

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, переделывается на управление областями видимости — без нового прохода компилятора.

Операция	Сложность	Частота триггера
Определение конфликта в дереве брендов	O(1)	При каждом требовании токена
Запрос потребителей DAG	O(1)	При каждом требовании токена
Обратный BFS (быстрый путь)	O(N)	При каждом требовании токена, N = количество узлов в блоке
СМТ логический разрыв (fallback)	~1мс	Крайне редко — только while + path_condition

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

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

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

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

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

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

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

Ошибки уровня сигнатуры: E0623 (несовпадение времени жизни), E0106 (отсутствует спецификатор времени жизни), E0477 (не удовлетворяет требуемому времени жизни). Вокруг 'a. В YaoXiang таких ошибок нет — в сигнатуре нет 'a. Не "невозможно сообщить", а "то, что пользователь не писал, не нужно сообщать".

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

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

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

Пример межфункционального экранирования:

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

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

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

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

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

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

Компромиссы

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

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

Недостатки

Не новое изобретение: Brand ID делает ровно то же, что 'a — сложность решения ограничений внутри компилятора не исчезла, просто кодировка изменилась с "имя переменной + набор ограничений" на "brand path + префиксное сопоставление". Для конечного пользователя разница только в том, что в сигнатуре не пишется 'a.
Полностью новая реализация: дерево брендов существует только как концепция в коде, требуется реализация с нуля. BorrowChecker, ControlFlowAnalyzer заменяются.
Зависимость от СМТ: логический разрыв зависит от Z3 (RFC-027 уже ввёл эту зависимость, не новая). Но проверка заимствований почти не триггерит — только while + path_condition.
Очень редкие паттерны требуют рефакторинга: паттерны, которые компилятор не может автоматически доказать, требуют рефакторинга кода пользователем. В отличие от 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	Сбор path_condition + СМТ логический разрыв (уровень 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 блоков — spawn DAG

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

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

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

Аннотация ​

Мотивация ​

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

Текущее состояние кодовой базы ​

Почему нужен пересмотр ​

Основной дизайн ​

Всё есть Хор ​

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

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

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

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

Анализ вариантов использования ​

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

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

if/else с возвратом значения и экранированием ​

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

while: СМТ логический разрыв ​

Суть: Brand ID — это и есть 'a ​

Какие сложности устранены языковыми ограничениями ​

Почему DAG возможен ​

Детальный дизайн ​

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

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

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

Сбор path_condition ​

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

Отношение с существующим кодом ​

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

? Распространение ошибок и Release, управляемый областями видимости ​

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

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

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

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

Недостатки ​

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

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

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

Ссылки ​

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

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

Аннотация

Мотивация

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

Текущее состояние кодовой базы

Почему нужен пересмотр

Основной дизайн

Всё есть Хор

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

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

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

Стратегия доказательства: быстрый путь приоритетен, СМТ как fallback

Анализ вариантов использования

Линейный код

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

if/else с возвратом значения и экранированием

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

while: СМТ логический разрыв

Суть: Brand ID — это и есть `'a`

Какие сложности устранены языковыми ограничениями

Почему DAG возможен

Детальный дизайн

Каталог системных предикатов

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

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

Сбор path_condition

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

Отношение с существующим кодом

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

`?` Распространение ошибок и Release, управляемый областями видимости

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

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

Компромиссы

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

Недостатки

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

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

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

Ссылки

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