Tooling — компилятор, верификация, диагностика

Решения этой группы определяют, как инструменты Nova работают с программами: какие проверки выполняются на этапе компиляции, какие — в runtime, и как ошибки оформлены для AI-генерации кода.

D24. Стратегия SMT-проверки контрактов

AMEND (Plan 140.2 Part A, 2026-06-13) — @field self-access в контрактах. Прежнее ограничение «контракт не может ссылаться на @field (self-access); передавайте поля явным параметром в #pure fn» — RETRACT. Контракт метода (requires/ensures/invariant) теперь МОЖЕТ ссылаться на поля receiver’а через @field (read-only) и на встроенные #pure-аксессоры @len()/@cap()/ @byte_len()/@is_empty(). SMT-модель: receiver — сущность _self; @f → uninterpreted _field_<name>_<sort>(_self) (та же конвенция, что для obj.field параметра). Полное описание — D256. Прочие @method() (non-accessor / non-pure / mut-receiver) НЕ кодируются — внятная checker-ошибка (не E2401). Запускает [M-140-bounds-as-contract] Part A.

AMEND (Plan 140.4, 2026-06-14) — overflow-чеки. Модель enforce-with-elision теперь покрывает и always-on int-overflow проверки (Plan 33.8 Ф.1.2): Z3- доказанные a OP b в диапазоне i64 → элидируются (always-safe — всегда; contract-based — лишь при enforced requires), недоказанные → checked-форма остаётся (и в release). Полное описание — D272.

Note (Plan 33.1, D96): Атрибуты используют префикс # (не @), см. D96.

Note (Plan 33.3 Ф.9): Атрибут #must_verify переименован в #verify. В старых текстах этого D-блока встречается #must_verify — читать как #verify.

AMEND (Plan 140.3, 2026-06-13) — violation = panic-class + interp-сообщения. (1) nova_contract_violation тегает fail-frame error_kind = NOVA_THROW_PANIC (как nv_panic/assert, D13) → пойманное consume/supervised нарушение классифицируется как Panic, не recoverable Failure (формат сообщения уже унифицирован Plan 140.1). (2) Сообщение requires <e>, "..." может быть interp-строкой "... ${x} ..." (синтаксис Nova interp; значения захватываются lazy на сайте нарушения через nova_contract_violation_dyn) — для requires; ensures/invariant пока статика. [M-140-contract-panic-unwind] + [M-140.1-message-interpolation] (Plan 140.3).

AMEND (Plan 140, 2026-06-12) — release-eval = «enforce-with-elision». Прежняя формулировка «в release недоказанные контракты стираются (zero-cost, как assert/NDEBUG)» — RETRACT. Контракты больше НЕ debug-only. Release-поведение теперь:

• Z3-доказанный контракт (proven_contracts) — элидируется на codegen (zero-cost даже в debug);
• контракт, который SMT не доказал, — runtime-проверка остаётся и в release; нарушение → nova_contract_violation (fail-fast abort), а не silent UB;
• снять проверку с недоказанного контракта можно только явно: per-fn #unchecked или build-policy --contracts=off.

Модель Dafny/Verus + runtime-fallback, ровно как bounds-check в Rust: оптимизатор снимает доказуемые, прочие проверяются всегда. «Always-on» ≠ «always pay» — платишь только за недоказанное. Без --features z3-backend proven пуст → все контракты проверяются в release (safe degrade, медленнее, не unsafe). Старый текст этого D-блока ниже читать сквозь эту правку (см. §«Поведение по уровням сборки» и §«Что отвергнуто» — они переписаны).

AMEND (Plan 140.1, 2026-06-12) — короткий location-first формат violation + опциональное сообщение на контрактах. Касается только диагностики nova_contract_violation (что печатается при runtime- нарушении); семантика проверки/элидирования (Plan 140 выше) не меняется. См. отдельную подсекцию «Формат runtime-violation» ниже. Два изменения:

1. Короткий location-first формат. Прежний многословный contract <kind> failed in : <expr> at <file>:<line> (verbose — слова «contract» и «in <fn>» избыточны, локация в хвосте) RETRACT. Новый:

   <file>:<line>: <kind> failed: <expr>
   

   где <kind> ∈ requires / ensures / invariant. Пример: bank.nv:42: requires failed: amount > 0. Слова <kind> failed: СОХРАНЯЮТСЯ (kind несёт смысл «какой именно контракт»); убраны лишь «contract» и «in <fn>». <file>:<line>: уезжает в начало — терминалы и IDE делают такой префикс кликабельным (jump-to-line).
2. Опциональное пользовательское сообщение. requires/ensures/ invariant принимают необязательный строковый литерал после выражения (requires amount > 0, "amount must be positive"). При нарушении сообщение печатается, выражение — в скобках:

   <file>:<line>: <kind> failed: <msg> (<expr>)
   

   Пример: bank.nv:42: requires failed: amount must be positive (amount > 0). Без сообщения — формат из п.1.

<file>:<line>: ВСЕГДА авто-добавляется в начало — и с сообщением, и без; локацию проставляет codegen из __FILE__/__LINE__ контракт- сайта, пользователь её не включает в свой текст (как и не включает само <expr>). Грамматика (Plan 140.1 Ф.1): (requires|ensures|invariant) <expr> ("," <string-lit>)?; не-строковый- литерал в позиции сообщения → E_CONTRACT_MESSAGE_NOT_STRING. Прецедент сообщения — assert(cond, "msg") (D84), императивный аналог; Plan 140.1 распространяет тот же принцип на декларативные контракты и на assert/debug_assert (см. D13 — тот же location-first формат + file:line для assert).

Что

Контракты в сигнатуре (requires/ensures/invariant) проверяются SMT-движком на этапе компиляции с явным таймаутом и fallback на runtime-проверку. Контракт, который SMT не смог доказать, не блокирует компиляцию по умолчанию — он становится runtime-проверкой и в debug, и в release (Plan 140: enforce-with-elision; прежнее «тихо игнорируется в release» — retract). Доказанный SMT контракт элидируется из codegen (zero-cost). Программист может явно требовать статическое доказательство через #verify — тогда компиляция падает, если SMT не справился; и явно снять runtime-проверку через #unchecked (per-fn) или --contracts=off (build), беря недоказанность под свою ответственность.

Правило

Стратегия SMT

1. SMT-кодировка контрактов из requires/ensures/invariant в стандартный формат (SMT-LIB v2). Конкретный движок — выбор реализации, не дизайна. Дизайн фиксирует класс движка: поддержка теорий LIA (linear integer arithmetic), EUF (equality + uninterpreted functions), arrays базовой функциональности. Этим требованиям удовлетворяют Z3, CVC5, Bitwuzla — выбор делает компилятор-реализация.

2. Таймаут на функцию — рекомендуемый дефолт 2 секунды. Превышение → fallback на runtime-проверку. Программист может увеличить через #verify_timeout(10000) локально или глобально в конфигурации проекта.

3. Поведение по уровням сборки (Plan 140 amend — enforce-with-elision):

   • debug: SMT-проверка + runtime-fallback для непроверенного. Нарушение runtime → panic с указанием контракта и точки.
   • release: SMT-проверка + runtime-fallback для непроверенного (как в debug). Доказанные SMT контракты (proven_contracts) — элидируются на codegen полностью (zero cost). Недоказанные — проверяются в runtime; нарушение → nova_contract_violation (fail-fast abort, не silent), с warning’ом #unverified на этапе сборки. Снять проверку с недоказанного — только явно через #unchecked (per-fn) или --contracts=off (build).
   • Без Z3 (--features z3-backend выключен): proven пуст → все контракты проверяются в release (safe degrade — медленнее, не unsafe).

   Wiring (Plan 140 Ф.3) — пайплайн верификации на build-пути. proven_contracts наполняется внутри types::check_module (env.proven_contracts = report.proven ← verify::verify_module → VerificationPipeline). До Plan 140 Ф.3 этот набор передавался в codegen только на пути nova-codegen compile (compiler-codegen/main.rs set_proven_contracts); на путях nova build, nova-codegen test-build/ test-all и nova bench возвращаемый ModuleEnv отбрасывался, и CEmitter::set_proven_contracts НЕ вызывался → набор proven у эмиттера пуст → доказанные контракты проверялись в runtime наравне с недоказанными (риск R4: пайплайн прогонялся, но proven не доходил до codegen → элизии не было). Ф.3 захватывает ModuleEnv на всех этих путях и вызывает set_proven_contracts(&env.proven_contracts) перед emit_module. Теперь элизия доказанного происходит и в nova build/ nova test --mode release, а не только в nova doc/verify.

   Выбор SMT-бэкенда на build-пути. VerificationPipeline::new() берёт бэкенд из BackendChoice::from_env(); по умолчанию Trivial (linear-arith + tautology/contradiction — доказывает узкий, но реальный класс: requires x >= 0; ensures x + 1 >= 1 элидируется и под Trivial). Полный Z3 включается двумя условиями вместе: бинарь собран cargo build --release --features z3-backend (vcpkg libz3 — см. compiler-codegen/build.rs) и в окружении задан NOVA_SMT_BACKEND=z3 (или NOVA_CROSSCHECK=1). Default-бэкенд намеренно остаётся Trivial даже при скомпилированном Z3 — это сохраняет детерминизм verify-набора тестов Plan 33 и не меняет поведение тех, кто не запросил Z3 явно. Элизия доказанного работает одинаково независимо от того, какой бэкенд наполнил proven (Z3 доказывает строго больше, чем Trivial).

   Perf (Plan 140 Ф.5) — proven-элидирование zero-cost. Микробенч nova_tests/plan140/perf_contract_hot_loop.nv (20M-итерационный hot-loop, вызывает sq_plus(x) => x*x + x с ensures result >= x — VC нелинейный, Z3 доказывает, Trivial — нет), release/clang, best-of-N:

   • --contracts=off (всё элидировано, baseline): 0.191s
   • Z3 enforce (POST result >= x элидирован как proven): 0.197s (≈baseline в пределах шума → zero-cost, как и заявлено)
   • Trivial enforce (POST проверяется каждую итерацию, no-Z3 degrade): 0.214s (≈+12% на contract-saturated loop, где проверка = заметная доля работы)

   Codegen-доказательство элизии (тот же .c): под Z3 эмитится 3 nova_contract_violation (PRE x >= 0 для sq_plus + 2 prelude with_capacity PRE), POST result >= x отсутствует; под Trivial — 4 (тот же набор + POST result >= x); под --contracts=off — 0. PRE (caller-obligation) никогда не входит в report.proven → всегда эмитится. Вывод: платишь только за недоказанное; overhead скейлится с долей runtime- проверки в теле — в реальном коде, где контракт гейтит существенную работу, относительная цена много меньше микробенч-12%. R1 (perf-overhead без Z3) измерен; смягчается --contracts=off / #unchecked / Z3-сборкой.

   RETRACT (Plan 140): прежний текст «недоказанные — игнорируются молча» отменён. Молчаливое стирание недоказанного контракта в release = снятие страховки именно там, где статическая безопасность НЕ подтверждена → silent UB/corruption в самых рискованных местах. Это худший выбор; Plan 140 заменил его на fail-fast.

4. Опт-ин строгости и опт-аут проверок через атрибуты:

   • #verify на функции → если SMT не доказал контракт, компиляция падает. Для критичного кода (медицина, финансы, авионика). (до Plan 33.3 Ф.9 назывался #must_verify)

   • #unverified на функции → отказ от попытки доказательства заранее, всегда runtime-check (чтобы не тратить время компиляции на заведомо непроверяемое). NB (Plan 140): #unverified НЕ снимает проверку — она остаётся в runtime (в т.ч. в release).

   • #unchecked на функции (Plan 140 Ф.2, opt-out) → элидирует даже недоказанные контракт-проверки целиком (zero-cost), беря недоказанность под ответственность разработчика. Для проверенного hot-path, где runtime-стоимость недопустима. Ортогонально #verify/ #unverified: те управляют статическим доказательством, #unchecked — наличием runtime-страховки. Build-аналог — --contracts=off. Реализовано (Plan 140 Ф.2): #unchecked — contract-attr перед fn (parser parse_contract_attrs → ContractAttrs.contracts_unchecked → FnDecl.contracts_unchecked). Codegen элидирует ВСЕ контракт-проверки тела помеченной fn (requires/ensures/invariant/decreases/ assert_static/assume — последние три через per-fn-body флаг contracts_unchecked_fn). Build-policy --contracts=enforce|off (default enforce) на nova build / nova-codegen compile|test-build| test-all: off глобально элидирует все контракт-проверки модуля (CEmitter.set_contracts_off). Per-fixture тест-директива // CONTRACTS off|enforce (D89) переопределяет политику для одного фикстура.

     AMEND (Plan 140.3, 2026-06-14, [M-140-contract-levels]): добавлены module-level opt-out и Eiffel-гранулярность. (a) #unchecked перед module X — элидирует контракт-страховку всего модуля (голое имя, НЕ #unchecked_module: суффикса _module в директивах Nova нет; консистентно с #stable/#no_prelude/#forbid). (b) #unchecked(requires) / #unchecked(ensures) / #unchecked(invariant) (комбинируемо) на fn И module уровне — элидирует ТОЛЬКО перечисленные виды. AST: FnDecl.contracts_unchecked: bool → ContractOptOut{requires,ensures,invariant}; Module.contract_opt_out; ModuleAttrKind::Unchecked. Codegen: per-fn флаг → per-kind гейт contracts_elided_for(kind) = --contracts=off ⊔ module-opt-out(kind) ⊔ fn-opt-out(kind), + invariants_elided_here(); requires/ensures/decreases/ invariant гейтятся НЕЗАВИСИМО. Bad kind → E_UNCHECKED_KIND.

Формат runtime-violation (Plan 140.1)

Когда недоказанный контракт нарушается в runtime (debug или release — enforce-with-elision, см. п.3), nova_contract_violation печатает короткий location-first диагностический текст. Формат — общий с assert/debug_assert (D13): один префикс <file>:<line>: для контрактов и assert’ов, чтобы IDE/терминал одинаково делали его кликабельным.

Без пользовательского сообщения:

<file>:<line>: <kind> failed: <expr>

Примеры:

bank.nv:42: requires failed: amount > 0
bank.nv:50: ensures failed: result >= 0
vec.nv:12: invariant failed: size <= cap

С пользовательским сообщением (requires <expr>, "<msg>"):

<file>:<line>: <kind> failed: <msg> (<expr>)

Пример:

bank.nv:42: requires failed: amount must be positive (amount > 0)

Правила формата:

• <file>:<line>: — всегда первый, авто-проставляется codegen’ом из контракт-сайта (__FILE__/__LINE__). Пользователь его не пишет.
• <kind> failed: сохраняется в обоих вариантах (kind = смысл «какой именно контракт нарушен»).
• <expr> — исходный текст контракт-выражения (как написан в коде). В варианте с сообщением он уходит в скобки после <msg>.
• <msg> — пользовательский строковый литерал; опционален. Без него — формат без скобок (back-compat по содержанию: тот же <kind> failed: <expr>, только короче и с location-first префиксом).

Прежний verbose-формат contract <kind> failed in : <expr> at <file>:<line> (имя функции в тексте, локация в хвосте) — RETRACT (Plan 140.1). Имя функции из текста убрано: <file>:<line> локализует точнее, а имя функции IDE достаёт по строке. Routing нарушения (fiber-fail-frame → test-frame → stderr+abort) — без изменений.

Парс-грамматика сообщения: (requires|ensures|invariant) <expr> ("," <string-lit>)? (Plan 140.1 Ф.1). Не-строковый литерал в позиции сообщения → E_CONTRACT_MESSAGE_NOT_STRING. Интерполяция значений в сообщении ("got {x}") не входит в v1 — отложено ([M-140.1-message-interpolation], нужен capture значений на момент нарушения).

Что поддерживается в v1.0

Целевые классы контрактов:

Plan 33.7 (BitVec): sized-integer типы (u8/u16/u32/u64/i8/i16/i32) кодируются в SMT bit-vector теорию с точной wrap-around семантикой (255u8 + 1u8 == 0u8). Битовые операции &/|/^/<</>> доступны в контрактах. Атрибут #nooverflow на функции добавляет VC на отсутствие переполнения для каждой арифметической операции — недоказуемый VC → compile error. int остаётся unbounded Z3 Int.

Пример: #nooverflow + #verify гарантируют, что сложение u32 не переполнится и postcondition доказан статически:

#nooverflow #verify
fn safe_add_u32(a u32, b u32) -> u32
    requires a <= 1000 as u32
    requires b <= 1000 as u32
    ensures  result == a + b
=> a + b

Требует NOVA_SMT_BACKEND=z3 (bit-vector theory). requires с && на одной строке (requires a <= 1000 as u32 && b <= 1000 as u32) также допустим.

Что НЕ поддерживается (research-уровень, отложено):

• Квантификаторы общего вида (forall x. P(x) ==> Q(x)).
• Индукция по структуре данных.
• Рекурсивные предикаты.
• Нелинейная арифметика над int (sized-int — через BitVec).
• Floating-point reasoning.
• String reasoning сложнее len() и equality.

Контракты с этими конструкциями принимаются грамматикой, но SMT их не доказывает → fallback на runtime или ошибка с #verify.

Контракты со ссылками на handler-state

Открытый вопрос. Контракт может содержать обращение к операции эффекта:

fn transfer(...) Db -> ()
    ensures Db.balance(to) == old(Db.balance(to)) + amount
=> ...

Это требует effect-aware SMT-кодировки: handler-вызов как неинтерпретированная функция с теоремами о её поведении. В v1.0 поддержка частичная — только для эффектов с явным pure_view (чистая проекция состояния handler’а). Полная поддержка — research, отдельный D-пункт после v1.0.

Почему

AI-first связь

Когда SMT не справился, ошибка компилятора имеет структурированный формат:

warning C0341: contract not verified statically
   in function `withdraw` at src/account.nv:34
   ┌─ src/account.nv:34:5
   │
   34 │     ensures acc.balance == old(acc.balance) - amount
   │             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this contract was not proven

   reason: SMT solver returned 'unknown' after 2.0s
   missing facts:
     - relation between `acc.balance` and arithmetic operations on `money`

   fallback: runtime check inserted in debug build

   suggestions:
     1. add intermediate `assert` to break the proof into steps
     2. use `#verify` if static proof is required
     3. simplify the contract if possible

Это обучающий сигнал для LLM. Модель получает не «что-то не так», а конкретный класс проблемы и три предложения. Это и есть AI-first компилятор.

Прецеденты

• Dafny — SMT-проверка через Z3, fallback на runtime.
• F* — статическое доказательство, без fallback (более строго).
• Why3 — оркестрация нескольких SMT-движков.
• Spec# (Microsoft Research) — пилот для C#, заглох, но идеи переехали в Code Contracts.

Nova берёт прагматичный путь Dafny (статика + runtime fallback), не максималистский путь F* (всё статически).

Что отвергнуто

• «Всегда статическая проверка, без runtime-fallback» — сделало бы контракты обязательно тотальными, половину прикладного кода невозможно было бы аннотировать.
• «Стирать недоказанные контракты в release» (legacy, RETRACT Plan 140) — прежняя модель assert/NDEBUG: в release недоказанное молча выключалось ради zero-cost. Отвергнуто Plan 140: это снимало страховку именно в недоказанных (= рискованных) местах → silent UB/corruption. Заменено на enforce-with-elision (доказанное элидируется, недоказанное проверяется и в release, abort на violation). Zero-cost достигается элидированием доказанного, а не стиранием всего.
• «Только runtime-проверка, без статического элидирования» — теряется ценность контрактов: каждый, даже доказуемый, контракт платит runtime-цену. Превращает контракты в обычные assert. Plan 140 элидирует Z3-доказанные → платишь только за недоказанное.
• Фиксация конкретного SMT-движка в дизайне. Дизайн — про семантику, не про имя движка. Имя — выбор реализации, как fiber-runtime в 06-concurrency.md → D14 (там не сказано «Tokio», сказано «fiber-based scheduler»).

Связь

• 01-philosophy.md → D10 — видимость в типах, проверяемость по фрагменту, AI-first как обоснование.
• 04-effects.md — handler-state в контрактах требует effect-aware SMT.
• 05-memory.md → D6 — параллель: «дизайн фиксирует класс, имя движка — выбор реализации».
• 08-runtime.md → D13 — отношение Panic и contract-violations: нарушение контракта в runtime — это panic (см. Q-block ниже / open-questions Q34 — abort-vs-panic-unwind в release).
• 08-runtime.md → D81 — три уровня safety: assert(cond) (always runtime) < debug_assert(cond) (debug-only) < requires/ensures (D24, compile-time где возможно). Контракты — «zero-cost когда SMT доказал» (Plan 140: доказанное элидируется, недоказанное проверяется и в release — НЕ debug-only); assert’ы — escape hatch для ситуаций где SMT недоступен.
• Plan 140 / D24 amend — release-eval = enforce-with-elision (proven-elided, unproven-checked). Открытые под-вопросы политики (default build-policy, abort-vs-panic, гранулярность opt-out) — open-questions.md → Q34.

Цена

1. Реализация требует SMT-интеграции. Нетривиально, но не research — Dafny / F* / Why3 показали, что это работает.
2. Таймаут зависит от структуры контракта. Программист иногда удивится: «почему не доказывается?». Структурированная ошибка должна объяснять.
3. Effect-aware SMT — частичная поддержка в v1.0, полная — после. Контракты с handler-state — known limitation, не проблема.

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

• Effect-aware SMT — полная поддержка контрактов с обращениями к handler-state.
• Структура pure_view для эффектов — какие части handler-state программист объявляет «чистыми проекциями».
• #must_verify на уровне модуля — глобальный strict mode для критичных компонентов.
• Политика enforce-in-release (Plan 140) — default build-policy (enforce vs off), поведение violation в release (abort vs panic-unwind), гранулярность opt-out (per-fn / per-module / build): open-questions.md → Q34.

D89. Test-tooling конвенции — EXPECT_* маркеры для negative-тестов

Что

Стандартизированный набор comment-маркеров в .nv-файлах для тестов, которые должны не сработать ожидаемым образом — от compile error до runtime panic / specific exit code / stdout pattern. Маркеры интерпретируются test-runner’ом, не парсером Nova: для самого языка это обычные комментарии.

Цель — унифицировать test-tooling-конвенцию. Любой Nova-conformant test-runner (текущий run_tests.ps1, будущий nova test, CI- интеграции, third-party fuzzer’ы) обязан реализовать стандартные маркеры. Это снимает вопрос «каждый разработчик придумывает своё» и делает тесты переносимыми между runner’ами.

Правило

Стандартные маркеры (4 штуки)

Маркер располагается в первых 30 строках файла, в строке- комментарии, формат:

// EXPECT_<TYPE> <argument>

Один маркер на файл. Если в файле несколько маркеров — runner берёт первый найденный.

Семантика логики:

• При наличии маркера логика test-runner’а переворачивается: обычное «codegen succeeded → pass» становится «codegen failed ожидаемым образом → pass».
• При несоответствии (codegen не упал когда ждали error, или упал не с тем pattern, или exe вернул не тот exit code, или нужный поток не содержит pattern) — test fails.
• Файл с EXPECT_COMPILE_ERROR не компилируется в exe и не запускается (предполагается невалидный код).
• Файл с EXPECT_RUNTIME_PANIC / EXPECT_EXIT_CODE / EXPECT_STDOUT / EXPECT_STDERR компилируется и запускается, runner смотрит на runtime-результат.
• stdout и stderr — разные потоки. EXPECT_STDOUT pattern сматчит pattern только если он в stdout; EXPECT_STDERR pattern — только если в stderr. Для проверки combined-вывода (любой поток) используйте EXPECT_RUNTIME_PANIC (для panic’ов, которые идут в stderr).

Pattern-matching

• Substring, не regex. Должен присутствовать в выводе компилятора (для EXPECT_COMPILE_ERROR) или в panic-сообщении / stdout (для runtime-маркеров).
• Case-sensitive. Программист пишет точный кусок ожидаемого сообщения.
• Multi-line patterns не поддерживаются — runner склеивает вывод в одну строку через пробел перед matching.

Исключающее поведение

Маркеры взаимоисключающие — один файл = один маркер. Если автор хочет проверить несколько error-условий — отдельные файлы для каждого (один файл на один аспект).

Это ограничение сознательное:

• Простой mental model для авторов тестов.
• Простой код test-runner’а (одна вилка на файл).
• Force’ит разделение тестов по сценариям, что улучшает читаемость и точность диагностики падений.

Альтернатива (multi-marker через EXPECT_*_LINE N: pattern) — сложнее, отвергнута для bootstrap’а.

Примеры

EXPECT_COMPILE_ERROR:

// EXPECT_COMPILE_ERROR duplicate definition

module nova_tests.negative_capability.overload_dup

fn process(n int) -> str { "first" }
fn process(n int) -> str { "second" }    // duplicate sig

EXPECT_RUNTIME_PANIC:

// EXPECT_RUNTIME_PANIC array bounds

module nova_tests.runtime_panic.array_bounds

fn main() Io -> () {
    ro xs = [1, 2, 3]
    ro _ = xs[10]                       // out-of-bounds
}

EXPECT_EXIT_CODE:

// EXPECT_EXIT_CODE 42

module nova_tests.runtime_panic.exit_code

fn main() Io -> () {
    exit(42, "intentional")
}

EXPECT_STDOUT:

// EXPECT_STDOUT hello world

module nova_tests.runtime.golden_hello

fn main() Io -> () {
    println("hello world")
}

Compliance

Test-runner называется Nova-conformant ⇔ реализует все 4 стандартных маркера согласно спецификации выше.

Custom-runner может расширять набор маркеров своими (например EXPECT_LINT_WARNING, EXPECT_MEMORY_LEAK), но не должен:

• Игнорировать стандартные маркеры (молча выполнять файл с EXPECT_COMPILE_ERROR как обычный тест).
• Изменять семантику стандартных маркеров (например делать EXPECT_COMPILE_ERROR case-insensitive).
• Использовать имена EXPECT_* для своих расширений (зарезервировано).

Почему

Зачем стандартизировать

Без D89 каждый test-runner придумывает свой механизм:

• run_tests.ps1 — comment-маркер EXPECT_COMPILE_ERROR.
• Гипотетический nova test — мог бы выбрать атрибут @expect_error.
• CI-скрипт — мог бы держать список «ожидаемо падающих» файлов в YAML.

Это привело бы к fragmentation: тесты, написанные для одного runner’а, не работают в другом. Авторам тестов пришлось бы дублировать маркеры или писать «multi-runner adapter». Это анти-паттерн — test-конвенции должны быть переносимыми.

D89 фиксирует минимальный общий набор. Расширения возможны, но ядро универсально.

Почему comment-маркер, а не часть языка

Альтернатива — сделать маркер first-class директивой языка (как TypeScript // @ts-expect-error). Это отвергнуто для Nova:

• Test-маркеры — edge-case фича (используется в ~5% файлов). Загрязнять core-language ради 5% — over-engineering.
• Парсер Nova не должен знать про testing — это violation separation of concerns.
• TypeScript-precedent специфичен: TS-комментарий-директива нужна и в production-коде (suppression of compile errors), не только в тестах. У Nova такой потребности нет — есть forbid/realtime блоки для сознательных suppressions.

Comment-маркер — простой и достаточный паттерн для test-only конвенции. Прецеденты:

• Rust compiletest: //~ ERROR pattern.
• Swift test-toolkit: // expected-error {{pattern}}.
• Go errorcheck: // ERROR pattern.

Почему 5 маркеров, не больше

Минимум, покрывающий 95% test-сценариев:

• Compile-time errors → EXPECT_COMPILE_ERROR.
• Runtime panics (D13) → EXPECT_RUNTIME_PANIC.
• Process-exit codes (D13 exit) → EXPECT_EXIT_CODE.
• Output-content tests stdout → EXPECT_STDOUT.
• Output-content tests stderr → EXPECT_STDERR.

stdout/stderr — два независимых маркера, потому что POSIX-конвенция разделяет потоки: stdout — для data, stderr — для diagnostics. Тесты должны различать. Combined-проверка (без разделения) не нужна — для panic’ов есть специализированный EXPECT_RUNTIME_PANIC.

Что может быть добавлено позже, при появлении use-cases:

• EXPECT_NO_STDERR — exe не должен ничего писать в stderr (нет warning’ов).
• EXPECT_LINT_WARNING pattern — lint без error.
• EXPECT_TIMEOUT_MS N — exe должен не превысить N мс.
• EXPECT_NO_OUTPUT — exe не должен ничего выводить.

Эти расширения добавляются отдельным D-блоком при необходимости, не предзагружают spec лишним.

Что отвергнуто

• Уровень 3 — атрибут языка (@expect_error("pattern")). Test-only фича не оправдывает изменения парсера / type-checker’а. См. «Почему comment-маркер».
• Эталонный .stderr-файл рядом с .nv (Rust trybuild-style). Больше ceremony, не нужен для substring-match.
• Multi-marker в одном файле через EXPECT_*_LINE N: pattern. Усложняет mental model и реализацию runner’а; разделение по файлам — лучше для читаемости и точности диагностики.
• Regex-pattern вместо substring. Substring проще писать и читать, не требует escape метасимволов в типичных сообщениях.
• YAML / TOML manifest со списком expected-failures (как у некоторых CI-систем). Маркер в самом файле — локально, виден автору при чтении кода.

Связь

• 08-runtime.md → D13 — panic / exit семантика, на которой строится EXPECT_RUNTIME_PANIC / EXPECT_EXIT_CODE.
• D24 — другой test-related D-блок (SMT-проверка контрактов); D89 — общий тестовый tooling.
• docs/test-conventions.md — практический guide для авторов тестов (как писать каждый тип маркера, типичные паттерны).
• run_tests.ps1 — Windows wrapper над nova-codegen test-all. Был заведён в Plan 16 Ф.7 для capability-enforcement, расширен до полного набора D89-маркеров. После Plan 24 — thin shim.
• run_tests.sh — Linux/macOS wrapper над тем же test-all.
• compiler-codegen/src/test_runner.rs — каноническая реализация D89 парсера и pipeline’а (codegen + cc + run + check). Production-grade hardening — Plan 26: per-test timeout (--timeout), parallel execution (--jobs), structured output (--format json|tap|text), --rerun-failed, per-test isolation, UTF-8 codepage force.

Bootstrap-status

• ✅ EXPECT_COMPILE_ERROR — реализовано в run_tests.ps1 (Plan 16 Ф.7). Используется 8 negative-тестов в nova_tests/negative_capability/.
• ✅ EXPECT_RUNTIME_PANIC — реализовано (2026-05-10).
• ✅ EXPECT_EXIT_CODE — реализовано (2026-05-10).
• ✅ EXPECT_STDOUT — реализовано (2026-05-10). Только stdout (после split’а stdout/stderr).
• ✅ EXPECT_STDERR — реализовано (2026-05-10). Только stderr.

Future runner’ы (nova test CLI, cargo test для interp-mode, CI-плагины) должны переиспользовать эту конвенцию. Реализацию для других OS / toolchain’ов писать с теми же маркерами.

Цена

1. Нужно поддерживать в каждом runner’е. Если появится nova test на Nova самом — реализовать 5 маркеров обязательно. Не сложно (substring-match + condition negation), но обязательно.
2. Маркер — plain comment, парсер про него не знает. Если автор опечатался (EXPECT_COMPILE_EROR без R) — runner проигнорирует, тест выполнится как обычный (и упадёт на compile-error неожиданно). Mitigation: linter может предупреждать о похожих на маркер опечатках в первых 30 строках.
3. Расширения требуют D-блока. Custom-маркеры в одном проекте — допустимы, но если хочется чтобы маркер стал стандартным (доступным в любом runner’е) — нужен D-блок-расширение.

D95. CLI path конвенции — nova check <path> / nova test <path>

Что

CLI subcommand’ы nova check и nova test принимают позиционный polymorphic path argument (file-or-directory). Без --recursive флага — directory всегда рекурсивно. Без --tests-dir, --check-recursive и подобных — путь позиционный.

Прецеденты: cargo check <path> (deprecated в cargo, но pattern в Rust ecosystem standard), go vet ./..., clippy <path>, eslint <path>, prettier <path>, ruff check <path>, black <path>.

Правило

Signature

nova check [<path>...]              # 0+ positional paths
nova test  [<path>]                 # 0..1 positional path

nova check:

• 0 paths → walk parents до nova.toml (workspace root), recurse.
• 1+ paths → каждый is_file → single check; is_dir → recurse.
• Multi-path: nova check std/ examples/ — оба обрабатываются.

nova test:

• 0 paths → default <repo>/nova_tests/.
• 1 path: is_file → single test (filter through display name); is_dir → use as tests directory.
• Multi-path не поддерживается в MVP (test_runner ограничение).

Семантика

1. file vs dir дискриминация через path.is_file() / path.is_dir(), не через флаги.
2. Recurse default для directory — без --recursive флага (clippy/eslint convention).
3. .nv extension required для file argument. Wrong extension → error.
4. Non-existent path → error.
5. std/runtime/ hard-skip (auto-gen из registry, D89).
6. Implicit skip directories: target/, node_modules/, vendor/, .git/, .hg/, .svn/, любые _* и .* directories.

Что НЕ поддерживается в MVP

(Расширения через sub-plans, см. Plan 36: sub-plans 36.A-E.)

• Glob patterns (*.nv, **) — shell expansion достаточен.
• ./... go-style suffix — slash-style (std/) проще и proven.
• Multi-path для nova test — однопутевая семантика в MVP.
• --recursive / --tests-dir / подобные флаги — запрещены (clean break, не deprecation).
• compile_commands.json-style output — отдельный план.
• Glob/regex для filter — --filter остаётся substring match.

Запрещённые флаги

Следующие флаги не должны существовать в nova check / nova test (R1-R3 plan-36, clean-break policy):

Почему

AI-first связь

LLM генерирует CLI invocations в скриптах / документации. Polymorphic path arg = меньше surface для ошибок. Когда есть --tests-dir, LLM может сгенерировать nova test --tests-dir foo где nova test foo работает. Одна форма — одна семантика.

Прецеденты

Nova следует clippy / eslint / ruff / black school: positional path, file-or-dir, recurse-by-default.

Exit codes

Реализовано полностью (commit 62c04378fa, Plan 36 R7).

Что отвергнуто

• nova check --recursive <dir> — дублирует is_dir() дискриминацию. Каждый currentmainstream linter работает без этого флага.
• --tests-dir <dir> deprecation cycle — bootstrap не в проде, clean break лучше (см. feedback_revolutionary_changes память). Удаление флага → error: unexpected argument '--tests-dir' found.
• Glob patterns в CLI (nova check **/*.nv) — shell expansion делает это лучше. Не нужно реализовывать parser glob’ов.
• Cargo-style -p <package> selection — у Nova workspace concept не сформирован (4 nested nova.toml в repo, см. AD6 Plan 36). Path-based proще.
• ./... go-style suffix — лишний синтаксис. nova check std/ более интуитивно чем nova check std/....

Связь

• 01-philosophy.md → D10 — AI-first как driver для simplicity.
• D89 — test-tooling конвенции (EXPECT_* markers).
• Plan 36 — полная спецификация R1-R30 + AD1-AD12, MVP = Ф.0+Ф.1, sub-plans 36.A-E для остального.
• 08-runtime.md → D13 — panic semantics (relates to exit code 101).

Цена

1. Несовместимость со старым --tests-dir. Кто-то у себя имел nova test --tests-dir foo в скрипте → нужно nova test foo. Bootstrap не в проде → приемлемо.
2. Path не path-pattern. Если нужно «все файлы кроме одного» — нужны --no-exclude flags (sub-plan 36.A). MVP shell-expansion достаточен.
3. MVP — exit 0/1 only. Quintuplet (0/1/2/3/101) отложен. Скрипты которые отличают usage-error от diagnostic пока полагаются на stderr message parsing — fragile.

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

• Multi-path для nova test — нужен только если test_runner поддержит multi-tests-dir. Сейчас нет use-case.
• - (stdin) input для editor integration — отдельный план (LSP / formatter).
• --list mode (show files без checking) — useful для отладки implicit-excludes; sub-plan 36.D.

D96. Синтаксис атрибутов — #name без квадратных скобок

Что

Function/type/module-level атрибуты в Nova используют префикс # (а не @), без обязательных квадратных скобок (как в Rust #[name]).

#realtime
#pure
#must_verify
fn must_pure(x int) -> int
    requires x > 0
    ensures result > 0
=> x + 1

Атрибуты с аргументами — через круглые скобки (как Java/Kotlin/Python/Scala):

#verify_timeout(5000)
#allow_transit(Db, Log)
#derive(Json, FromRow)
fn process_order(o Order) -> Receipt => ...

Правило

Грамматика

Attribute := '#' Ident ( '(' ArgList ')' )?
ArgList   := Expr (',' Expr)*

• Простой маркер: #pure.
• С аргументами: #verify_timeout(5000).
• Несколько атрибутов — на отдельных строках перед declaration.

Position

Атрибуты разрешены только перед declarations (fn / type / module).

НЕ разрешены:

• Перед let / const внутри тела функции.
• Перед expressions внутри тела.
• Inner-attributes (#![...] в Rust) — не вводим; для module-level директив есть keyword’ы (module, import).

Префикс # (не @)

Префикс @ уже занят в Nova для другого: receiver/self-доступ в методах (D35):

Использование одного @ для receiver-access И для attributes даёт dual-use символа, что создаёт когнитивную нагрузку и потенциал для ошибок LLM при генерации кода. Префикс # — свободен, не использовался в Nova (комментарии только //).

Почему

AI-first связь

Один символ = одна семантика. LLM, читая @something, не должен гадать «attribute или self-access». # для attributes, @ для self — прозрачное разделение.

Прецеденты

Большинство mainstream языков используют префикс без обязательных скобок — скобки появляются только когда есть аргументы. Rust с #[...] — исключение, обусловленное необходимостью inner attributes #![...], proc-macros (token tree forwarding) и атрибутов на expressions. У Nova ни одной из этих причин нет.

Почему не #[name] (Rust-стиль)

Скобки #[...] в Rust обоснованы тремя историческими факторами, которые не применимы к Nova:

1. Proc-macros с произвольным token tree. #[serde(rename = "x")] передаётся в proc-macro как сырой token stream. Nova не имеет proc-macros (см. revolutionary.md: «no macro AST-rewriting»); комптайм-метапрограммирование делается через typed comptime, не через rewriting.

2. Inner attributes #![...] для модуля / crate-level директив. У Nova module declared через keyword module a.b.c, никаких inner attributes не нужно.

3. Атрибуты на expressions (vec![#[cfg(unix)] 1, 2, 3]). У Nova атрибуты только на declarations — это явное design-ограничение.

С круглыми скобками для arguments (#name(args)) парсер однозначно разрешает в declaration-position. Это работает в Java/Kotlin/Python/Scala уже десятилетиями.

Что отвергнуто

• @name для attributes — конфликт с receiver-prefix @field. Dual-use символа = плохо для AI-first языка.
• #[name] (Rust-стиль) — скобки избыточны без proc-macros, inner attributes или атрибутов на expressions. Карго-культ к Rust без понимания причин.
• Keyword-форма (pure fn) — ломает существующий синтаксис (D64 @realtime; breaking change для каждого атрибута); композиция must_verify pure fn читается странно (два keyword’а подряд).
• name fn (modifier-keyword без префикса) — конфликт с обычными идентификаторами; нужны reserved words для каждого атрибута.

Цена

1. Миграция @realtime → #realtime (Plan 16 уже использовал @realtime). На момент D96 — 5 .nv-файлов в repo. Breaking change, но Nova не в production (см. feedback_revolutionary_changes).
2. Документация: все примеры в spec/, docs/, README обновляются.
3. Будущее расширение: если когда-либо понадобятся proc-macros или inner attributes — добавляется через отдельный D-decision (например ##name для inner) без breaking change для #name outer.

Связь

• D24 — #must_verify, #unverified, #verify_timeout(N), #pure атрибуты для контрактов.
• D64 — #realtime / #realtime nogc атрибут.
• D62 — #allow_transit(Effects...) атрибут для transit-effect warning suppression.
• revolutionary.md — «no macro AST-rewriting» как philosophy reason против Rust-style #[...] token tree.

Используется в

• Plan 16 Ф.5 — #realtime / #realtime nogc.
• Plan 33.1 — #must_verify, #unverified, #verify_timeout(N), #pure.
• Plan 33.3 — #verify_handler, #trusted, #must_verify_module.

D105. Doc-атрибуты

Status: active (spec). Реализация — Plan 45 Ф.3.

Опирается на: D96 (синтаксис атрибутов #name), D101 (module-attr #doc "...").

Namespace: #doc(...) делит префикс с D101 #doc "string", но эти две формы синтаксически различны (string literal vs. parenthesised key-value list) и не коллидируют. См. подсекцию «Namespace» ниже.

Что

Фиксированный набор атрибутов, декорирующих items документационной метаинформацией. Tooling (nova doc, type-checker lint’ы) читает их; runtime — игнорирует.

Каталог для Plan 45 MVP:

Синтаксис

Все doc-атрибуты используют форму D96 #name(...). Голые #stable, #unstable, #experimental, #hide_doc валидны без аргументов; их key-value форма принимает перечисленные параметры.

#deprecated(since = "0.4.0", note = "use [open_buffered] instead")
fn open(path str) Net -> File => ...

#stable(since = "1.0.0")
type Connection { ... }

#unstable(feature = "channel_select")
fn select_or_default[T](chs []ChanReader[T]) -> T = ...

#hide_doc
fn internal_helper() -> int => 42

#doc_alias("malloc", "alloc")
fn allocate(n int) -> []u8 = ...

#doc(inline)
export import std.collections.range.{Range}

#doc(summary = "Compute SHA-256 hash of the input bytes.")
fn sha256(data []u8) -> [32]u8 = ...

Семантика

#deprecated

• Обязательные параметры: since (string, версия Nova/пакета, вводящая deprecation) и note (string с migration guidance).
• Опциональный: until (string, версия планируемого удаления). При присутствии — включает CI-gate --deny-overdue-deprecations в nova doc --check.
• Эффект:
  • nova check / nova test / nova build эмитят warning deprecated на каждом use-сайте (file:line + note).
  • nova doc рендерит deprecation-баннер и включает since, until, note в JSON output.
• Поле note ДОЛЖНО содержать intra-doc link на замену (note = "use [foo.bar] instead"); lint deprecated-without-link warning’ит при отсутствии.

#since(version)

• Записывает версию появления item’а.
• Используется filter’ом --since <version> (Plan 45 Ф.12) для changelog-генерации.
• Diagnostics не производит; чисто информационный.

#stable / #unstable / #experimental (stability tiers)

Три mutually-exclusive tier’а. Item может нести не более одного.

• #stable(since = "...") — committed API. since рекомендован; default unknown.
• #unstable(feature = "name") — opt-in через feature-флаг на этапе билда (Plan 42.12 #cfg(feature = "name")-precedent). Use-сайт вне #cfg(feature = "name")-скоупа — hard error.
• #experimental(note = "...") — proof-of-concept. Use-сайты эмитят warning. note ДОЛЖЕН описывать, что может измениться.

Propagation: module-level stability tier пропагируется на items модуля без явного tier’а (через pass propagate_stability; Plan 45 §3). Item’ы с явным tier override.

#hide_doc

• Item реально exported (виден import-consumer’ам), но не рендерится через nova doc.
• Use case: items, оставшиеся exported для backward compat, которые не должны промоутиться в новой документации; internal helpers, открытые для testing.
• Runtime-эффекта нет; только nova doc collector пропускает item.

#doc_alias("name", "name", ...)

• Альтернативные имена для search index’ов.
• Пример: #doc_alias("malloc") на fn allocate — поиск “malloc” найдёт allocate.
• Каждый alias — string literal; никаких трансформаций.
• Plan 45 MVP: aliases появляются в JSON output; consumption в HTML search index — Plan 45.A.

#doc(inline) / #doc(no_inline)

• Контролирует рендеринг re-export’ов.
• #doc(inline) (default для same-package re-export’ов): re-exported item рендерится у re-export-сайта с теми же docs, что и оригинал.
• #doc(no_inline) (default для cross-package re-export’ов): короткий стаб «re-export of path.to.original» с link’ом.

#doc(summary = "...")

• Override automatic first-sentence summary extraction.
• Plain string; markdown — только inline-code (через backtick) и intra-doc links.
• Используется, когда первое предложение doc-body — не лучший summary (например, начинается с setup-clause).

#doc(section = "Name")

• Помещает item в custom section module rendering.
• Default-секции (Functions, Types, Constants, …) узнаются; этот атрибут создаёт sub-section под соответствующим kind-heading.
• Plan 45 MVP: распознаётся parser’ом, игнорируется в рендеринге (item помещается в default-секцию). Полный рендеринг — Plan 45.A.

#doc(test_handlers = "path.to.handlers")

• Module-level или item-level.
• При присутствии все doc-test’ы в scope’е автоматически оборачиваются в with handler from <path> { ... }. Path резолвится как import.
• Снимает необходимость в hidden setup-line’ах в каждом doc-test’е.
• Cross-ref с D106 для doc-test-семантики.

Namespace

Префикс #doc делится с формой D101 #doc "string-literal". Различаются по первому токену после doc:

• #doc "..." (string literal) — D101 module-doc-атрибут.
• #doc(...) (parenthesised key-value list) — D105 типизированный атрибут.
• #doc_alias(...) (underscore в имени) — D105 catalog-member.
• #doc_* зарезервировано для будущих D105-атрибутов (например, #doc_section).

Parser дисамбигуирует lookahead’ом за токен после идентификатора doc:

• STRING_LIT → D101.
• LPAREN → D105.
• _<ident> → D105 named member.
• что-либо иное → syntax error.

Почему

1. Каталог (не free-form tag soup) — Go, Rust и TypeScript doc-tooling’и все страдали от drift’а конвенций (@param vs @parameter vs ничего в TSDoc; Deprecated: proza vs #[deprecated]-атрибут в Go vs Rust). Фиксация маленького именованного каталога на уровне языка — предотвращает это. Добавление новых атрибутов требует новой D-decision.
2. Типизированные параметры — #deprecated(since, note, until) имеет структурированные fields, доступные в JSON output. LLM- consumer’ы могут читать since numerically; «Deprecated: use foo instead.» в free-form комментарии — opaque.
3. #hide_doc opt-out, не opt-in — Rust’овский #[doc(hidden)] opt-out, mirror’ит pub-by-default. Nova private-by-default (D5), поэтому export opt-in. Прятать export из doc — отдельный opt-out — это соответствует ментальной модели private-by-default.
4. Поле until для #deprecated — ни у Rust, ни у Go нет. А «we’re removing this in 1.0» — реальная lifecycle-стадия. С until nova doc --deny-overdue-deprecations становится CI- gate’ом против забывчивости удалить.

Что отвергнуто

• JSDoc-style теги @param / @returns — у Nova типизированные параметры и return-типы в сигнатуре; документировать их повторно prose’й — duplication и drift. Style guide (Plan 45 §11.5) рекомендует inline-упоминание в description.
• #[doc = "raw text"] alternative form (Rust precedent) — форма /// достаточна; raw text в атрибутах нужен генераторам кода (макросам), которых в Nova нет. Пересмотреть, если появится metaprogramming.
• Multi-tier стабильность сверх трёх (у Rust много flavour’ов unstable) — три tier’а (stable/unstable/experimental) покрывают use-кейсы без сложности.
• User-defined doc-атрибуты — открывает каталог для произвольных тегов, фрагментируя convention. Каталог растёт только через D-decisions.

Связь

• D96 — основание #name(...) синтаксиса.
• D101 — module-attr #doc "..."; namespace сосуществует.
• D104 — лексер //////! doc-comment recognition.
• D106 — #doc(test_handlers) referenced.
• Plan 45 Ф.3 реализация, §11.5 style guide.

D106. Семантика doc-test’ов

Status: active (spec). Реализация — Plan 45 Ф.7.

Reuses: D89 (EXPECT-markers); Plan 24 (test_runner). Doc-test’ы компилируются и запускаются через тот же pipeline, что и *_test.nv-файлы.

Что

Code-блок внутри doc-comment’а является doc-test’ом, если:

• Огорожен triple-backtick (```).
• Имеет language tag nova либо вообще без language tag (default).

/// Возвращает true, если `x` чётно.
///
/// # Examples
///
/// (triple-backtick fenced block здесь — code внутри)
/// assert(is_even(2))
/// assert(!is_even(3))
fn is_even(x int) -> bool => x % 2 == 0

Выше — один doc-test. Test runner извлекает его, компилирует как самодостаточный модуль и запускает assert’ы.

Code-block модификаторы

Language tag может сопровождаться нолём или больше comma-separated модификаторов, написанных сразу после language tag в строке fence-opener’а.

Каталог (MVP):

Множественные модификаторы комбинируются там, где имеет смысл (no_run,must_verify означает «verify but do not execute»). Конфликтующие комбинации (compile_fail,should_panic) — configuration error.

Hidden lines

Doc-test строка, начинающаяся с # (хеш + пробел) — скрыта в рендеренном output’е, но компилируется и выполняется как часть test’а. Используется для setup’а, который засорил бы примеры (import’ы, helper-определения и т.п.).

Privacy

Doc-test’ы имеют module-private access к item’у, который документируют. Doc-test на export fn foo (в std.collections.range) может вызывать non-exported helpers внутри std.collections.range. Это соответствует поведению rustdoc и отражает принцип: примеры демонстрируют использование item’а с same-module-перспективы.

Cross-module doc-test’ы на re-export’ах сохраняют privacy-scope оригинального модуля (того, где item определён), а не re-exporter’а.

Setup через #doc(test_handlers)

D105 определяет атрибут #doc(test_handlers = "path"). При применении к модулю или item’у все doc-test’ы в scope’е неявно оборачиваются:

with handler from path.to.handlers {
    ... тело doc-test'а ...
}

Снимает boilerplate для типичных setup’ов (test-handler stack’и, mock filesystems и пр.).

Peer-файл folder-модуля с именем _doctest_setup.nv (Plan 42 folder-module convention) также неявно импортируется в doc-test- scope, если присутствует. Оба механизма аддитивны.

Модель компиляции

Каждый doc-test компилируется как synthetic module:

module __nova_doc_test_<hash>

import <enclosing-module>.*

test "<item-name> example <index>" {
    <hidden-lines + visible-lines>
}

• Hash — детерминированная функция от (item-path, doc-test-index).
• Имя теста — <item-name> example <N> (1-indexed).
• Import’ы из enclosing-модуля — wildcard-style (peers видимы).

Компиляция переиспользует стандартный pipeline (parser → type-checker → codegen / interp). Сбои маршрутизируются как обычные test-failures.

Выполнение

Doc-test’ы выполняются через тот же test_runner, что и обычные тесты (Plan 24). Parallelism (--jobs N), output format и exit codes идентичны.

nova doc --check запускает doc-test’ы по дефолту; --no-doc-tests отключает. nova test не запускает doc-test’ы по дефолту (doc-test’ы принадлежат nova doc); nova test --doc-tests opt-in.

Exit codes по D95:

• 0 — все doc-test’ы прошли.
• 1 — хотя бы один failed.
• 2 — usage error.
• 101 — internal panic.

Интеграция с EXPECT-markers

Модификаторы compile_fail и should_panic — syntactic sugar, транслирующийся в D89 EXPECT-markers, вставленные в синтетический test-файл:

Reuse’ит существующую test_runner инфраструктуру; никакой новой failure-mode-механики не нужно.

Почему

1. Doc-test’ы соседствуют с документируемыми item’ами — Go’шные Example*-функции в *_test.go (golang/go #16851) дрейфят от документируемого item’а. Inline doc-test’ы co-located с тем, что документируют; при rename item’а соседние тесты в том же файле движутся вместе.
2. compile_fail / should_panic first-class — rustdoc precedent. Документирование «это должно failиться» ценно; tooling-проверка — убирает целый класс stale-example багов.
3. must_verify — Nova-unique — leverages Plan 33 SMT verification. Doc-comment может демонстрировать, что функция удовлетворяет контрактам под всеми входами, не только под одним примером.
4. Hidden setup через # — приемлемый компромисс: слишком verbose показывать каждый import; #doc(test_handlers) и _doctest_setup.nv покрывают типичные кейсы без per-test boilerplate’а.

Что отвергнуто

• Markdown-link-style ссылки на внешние example-файлы — doc-test в examples/foo.nv добавляет indirection, теряет co-location. Inline — каноническая форма.
• Модификатор run_only_if_feature("name") — дублирует #cfg(feature = ...) (Plan 42.12). Если документируемый item feature-gated, тест наследует gate.
• Модификатор expected_output = "..." для stdout-сравнения — assert’ы внутри теста более гибкие. Если нужно stdout-matching — D89 EXPECT_STDOUT через hidden line.
• Doc-test isolation-контейнеры (process-per-test) — overhead слишком высокий; test_runner уже изолирует state per-test через fresh module-instance.

Связь

• D24 — модификатор must_verify завязан на SMT verification.
• D89 — EXPECT-markers reused.
• D95 — CLI exit codes.
• D104 — fenced code-блоки внутри doc-comment’ов.
• D105 — #doc(test_handlers).
• Plan 24 — test_runner reuse.
• Plan 33 — контракты для must_verify.
• Plan 42 — _doctest_setup.nv folder-module peer.
• Plan 45 Ф.7 реализация.

D107. JSON output schema v1

Status: active (spec). Реализация — Plan 45 Ф.9.

Заметка о состоянии stability: v1 поставляется маркированный как mvp-stable — только additive minor changes, никаких breaking. После ≥ 1 milestone’а реального использования (Plan 45.B stdlib doc-pass + ≥ 3 внешних AI-consumer’ов) stability промоутится к stable. Promotion — отдельная spec-ревизия этой D-decision.

Что

nova doc --format json производит JSON-документ, описывающий public API surface модуля (или workspace’а). Документ соответствует versioned-схеме (format_version: u32); consumer’ы ОБЯЗАНЫ проверять версию перед парсингом.

Схема embedded в бинарь компилятора как JSON Schema 2020-12 и эмитится через nova doc --json-schema.

Top-level shape

{
  "format_version": 1,
  "nova_version": "0.1.0",
  "generated_at": "2026-05-15T12:34:56Z",
  "source_root": "/path/to/repo",
  "modules": [ ... Module ... ],
  "items": [ ... Item ... ],
  "links": [ ... Link ... ],
  "doc_tests": [ ... DocTest ... ]
}

Обязательные top-level-поля:

• format_version (u32) — major-версия схемы. Consumer’ы ОБЯЗАНЫ fail-loudly при нераспознанной версии.
• nova_version (string, semver) — версия компилятора, эмитившего документ. Информационно; не stability-контракт.
• generated_at (string, RFC 3339 UTC) — emission timestamp. Может быть elided в reproducible-build mode (SOURCE_DATE_EPOCH).
• modules (array<Module>) — каждый документированный модуль (entry + transitive imports при --workspace).
• items (array<Item>) — flat-список всех items; поле module_path дисамбигуирует ownership.
• links (array<Link>) — резолвенные intra-doc links от items в этом документе.
• doc_tests (array<DocTest>) — извлечённые (и опционально выполненные) doc-test’ы со статусами.

Опциональные top-level-поля:

• source_root (string, абсолютный путь) — корень репозитория. Опускается, когда source-paths анонимизированы (флаг --anonymize-paths — будущий).

Форма Module

{
  "path": "std.collections.range",
  "name": "range",
  "kind": "folder",
  "peers": ["range.nv", "range_test.nv"],
  "summary": "Inclusive/exclusive integer ranges.",
  "description": "Markdown text...",
  "stability": { "tier": "stable", "since": "1.0.0" },
  "deprecation": null,
  "doc_attrs": [ ],
  "source": { "file_id": 12, "line": 1 }
}

• path — dotted module path.
• name — последний segment path.
• kind — folder для folder-модулей, file для single-file.
• peers — relative paths к peer-файлам (только для folder); пустой для file.
• summary — первое предложение, извлечённое из //! doc и #doc module-attr.
• description — полное markdown-тело.
• stability — { tier: "stable" | "unstable" | "experimental", since: "..."?, feature: "..."?, note: "..."? } или null для неизвестного tier’а.
• deprecation — { since, note, until? } или null.
• doc_attrs — прочие doc-атрибуты (по D105), не имеющие structured top-level-поля.
• source — { file_id, line } для «View Source»-links.

Форма Item

Item’ы — tagged unions. Все items делят общий header:

{
  "id": "std.collections.range::Range",
  "module_path": "std.collections.range",
  "name": "Range",
  "kind": "fn",
  "summary": "...",
  "description": "...",
  "sections": { "examples": "...", "errors": "..." },
  "stability": { "tier": "stable" },
  "deprecation": null,
  "doc_attrs": [ ],
  "source": { "file_id": 12, "line": 42 },
  "signature": { }
}

id — стабильный идентификатор: <module_path>::<name> для free items; <module_path>::<TypeName>.<method> для методов. ID’ы — канонический link target.

Объект sections содержит распарсенные стандартизованные секции (# Examples, # Errors и пр.) как markdown-строки, ключеванные lowercase-именем секции.

Kind-specific:

• kind: "fn" — signature (params, return type, effect-row, raises, generics, contracts).
• kind: "type" — definition (Record | Sum | Alias | Protocol | Effect) с fields / variants и т.п.
• kind: "const" — type, value (рендерится как Nova source).
• kind: "effect" — массив methods (effect-op signatures), axioms (Plan 33.3 D24 axiom-clauses).
• kind: "handler" — effect (резолвенный id), флаг is_default.
• kind: "protocol" — methods (signatures обязательных методов), implementors (резолвенные item-id’ы).

Форма Signature (для fn-items)

{
  "params": [
    { "name": "x", "type": "int", "default": null },
    { "name": "port", "type": "int", "default": "8080", "keyword_only": true }
  ],
  "return_type": "int",
  "effects": ["Net", "Db"],
  "raises": ["NotFound", "Timeout"],
  "generics": [
    { "name": "T", "bound": "Hash", "default": null }
  ],
  "receiver": null,
  "contracts": {
    "requires": ["x > 0"],
    "ensures": ["result >= x"],
    "verify_status": "PROVEN"
  }
}

• Поля type — рендерятся как Nova source (строки), не как структурные AST. Это намеренно: consumer’ы, которым нужна структура, могут парсить тем же parser’ом. Рендеринг строк сохраняет JSON output портабельным и человекочитаемым.
• keyword_only: true ставится, когда параметр имеет default по D102.
• Список effects — effect-row (set-typed, упорядочено алфавитно для детерминизма).
• raises — union вариантов Fail[X] из effect-row.
• receiver ненулевой для instance/static-методов: { "type": "Box", "kind": "instance", "mutable": false }.
• contracts.verify_status — одно из PROVEN | UNVERIFIED | TIMEOUT | TRUSTED.

Форма Link

{
  "from": "std.collections.range::Range.map",
  "to": "std.collections.iter::Iter.map",
  "kind": "fn",
  "resolved": true,
  "source_span": { "file_id": 12, "line": 45, "col": 10 }
}

Запись каждого intra-doc link’а, обнаруженного в этом документе. При resolved: false link-target был unresolvable (broken link).

Форма DocTest

{
  "id": "std.collections.range::Range.map::doc_0",
  "item_id": "std.collections.range::Range.map",
  "lang": "nova",
  "modifiers": ["no_run"],
  "code": "...",
  "code_visible": "...",
  "source_span": { "file_id": 12, "line": 67 },
  "status": "passed",
  "duration_ms": 12,
  "failure": null
}

• id — детерминированный: <item_id>::doc_<index> (0-indexed).
• code — полный код, включая hidden setup-lines.
• code_visible — код без hidden-lines (для HTML/Markdown rendering).
• status — одно из passed | failed | skipped | not_run.
• failure — null при успехе; иначе { kind, message }, где kind ∈ compile_error | runtime_panic | verification_failure.
• status: "not_run" — был передан --no-doc-tests; только извлечён, не выполнялся.

Детерминированный output

Producer’ы ОБЯЗАНЫ эмитить JSON детерминированно:

• Object-keys отсортированы алфавитно.
• Arrays в стабильном порядке: modules и items по path/id; links по from затем to; doc_tests по id.
• Поле generated_at опускается, когда в env установлен SOURCE_DATE_EPOCH.

Тесты в Plan 45 Ф.19 проверяют byte-identical output между двумя последовательными прогонами.

Правила стабильности

Полную versioning-политику см. в Plan 45 §6. Кратко:

• Additive minor changes (не bump’ят format_version):
  • Новые опциональные top-level или вложенные поля.
  • Новые enum-варианты в полях, документированных как «extensible».
  • Новые kind-specific Item-fields (consumer’ы default-skip’ают).
• Breaking changes (format_version инкрементится):
  • Удалить или переименовать поле.
  • Сменить тип или семантику поля.
  • Сузить enum (удалить вариант).

format_version=N и format_version=N+1 поддерживаются параллельно ≥ 1 stable-релиз компилятора. Consumer’ы поощряются fail-loudly на непознанной major-версии.

nova-doc-types consumer-крейт

Отдельный Rust-крейт nova-doc-types предоставляет типизированные bindings к схеме:

// nova-doc-types = "1.x" — версия-locked с format_version=1.
use nova_doc_types::{Document, Item, ItemKind};

let doc: Document = serde_json::from_str(&json_input)?;

Mirror’ит rustdoc’овский rustdoc-types-крейт. Versioning параллельный format_version: major-bump’ы lock-step.

Embedded JSON Schema

nova doc --json-schema эмитит схему как JSON-документ, соответствующий JSON Schema 2020-12. Это включает:

• Offline-валидацию в CI-gate’ах.
• IDE auto-completion в редакторах, потребляющих JSON Schema.
• LLM tool-use prompt context.

Схема embedded в бинаре компилятора (include_str!). Версии схемы immutable per format_version; бинарь несёт ровно одну (текущий major).

Почему

1. Stable JSON как first-class output — у godoc’а нет, rustdoc’е только unstable-nightly, TypeDoc — unstable. Nova поставляет stable-схему на stable-сборке с MVP-day-one. AI/LSP-consumer’ы могут полагаться.
2. format_version integer, не semver-string — проверки проще (>= 1 && <= 1 per consumer), parser проще. SemVer-семантика запечена в additive-minor / breaking-major правило выше без exposure version-string complexity.
3. String-рендеренные типы vs структурные AST — exposure полного структурного AST в JSON связал бы consumer’ов с internal Nova type representations. Рендеринг строк портабельный (любой consumer прочитает) и стабильный (parser-changes не ломают JSON shape, только содержимое рендеренных strings меняется в step с языком).
4. Sorted, deterministic output — нужен для --diff (Plan 45.A) и reproducible builds. Без него doc-as-CI-gate производит ложные diff’ы.
5. Embedded schema — offline-валидация без сети. CI-gate’ы могут крутиться на air-gapped-builder’ах.

Что отвергнуто

• Per-module JSON-файлы (один файл на модуль) — Plan 45 эмитит единый документ по дефолту. Per-module-файлы создают discovery-проблемы (надо листать директории, нет глобальных cross-references). Будущее расширение может добавить --split-by-module для очень больших workspace’ов.
• GraphQL endpoint вместо JSON-файла — server-overhead для CLI- инструмента. JSON-документ — consumer-agnostic.
• Protocol Buffers / MessagePack — JSON — lowest common denominator для AI/LSP/CI tooling. Бинарные форматы — позже, если докажут нужду; JSON — канонический контракт.
• Embedded полный source — раздувает output и дублирует работу. Consumer-сайд может резолвить source.file_id, если у него есть доступ к source.

Связь

• D89 — EXPECT-markers транслируются в DocTest.failure.kind.
• D95 — CLI-конвенции для nova doc --format json.
• D104 — источник doc-content.
• D105 — поля attribute-metadata.
• D106 — источник формы DocTest.
• Plan 45 §6, §6.5 — versioning policy; Ф.9 реализация.

D111. assume / assert_static / #trusted external

Статус: Принято (Plan 33.2 Ф.8 + Plan 33.3 Ф.9/Ф.13, реализовано)

Решение

Три escape-hatch механизма для управления верификацией:

assert_static <bool>

Промежуточный шаг доказательства: разбивает сложный контракт на части. SMT видит assert_static как дополнительный fact в текущей точке. В release стирается (verified по SMT); в debug — runtime assert.

fn transfer(from int, to int, amount money) Db -> ()
    requires amount > 0
    ensures Db.balance(to) == old(Db.balance(to)) + amount
{
    assert_static Db.balance(from) >= amount   // промежуточный факт
    Db.setBalance(from, Db.balance(from) - amount)
    Db.setBalance(to,   Db.balance(to)   + amount)
}

assume <bool>

Escape-hatch для знаний о FFI / внешних инвариантах. SMT получает (assert <expr>) без proof. Вне функции, помеченной #trusted, — warning категории trust-introduced.

#trusted
fn call_ffi() -> int {
    ro result = extern_fn()
    assume result >= 0   // знаем по документации FFI
    result
}

#trusted external fn

external fn с контрактами требует #trusted. Контракты регистрируются как axioms — caller получает ensures как предположение без proof.

#trusted
external fn libc_strlen(s str) -> int
    requires s.is_valid_cstring()
    ensures result >= 0

Обоснование

Полностью pure SMT-proof недостижим для кода с FFI, внешними библиотеками и непроверяемыми OS-инвариантами. Escape-хатчи сохраняют expressiveness при сознательном принятии риска. Паттерн из Dafny (assume, {:axiom}), F* (assume_val).

Реализация

• compiler-codegen/src/ast/mod.rs — ExprKind::AssertStatic, ExprKind::Assume.
• compiler-codegen/src/parser/mod.rs — парсинг assert_static, assume.
• compiler-codegen/src/types/mod.rs — #trusted attribute на fn-decl; warning для assume вне #trusted.
• compiler-codegen/src/verify/encode.rs — assert_static → SMT fact; assume → (assert ...).
• compiler-codegen/src/codegen/emit_c.rs — assume → стирается в release; debug → runtime-if с NOVA_ASSUME violation.

D112. Bounded quantifiers (forall/exists по коллекции)

Статус: Принято (Plan 33.3 Ф.10, реализовано в AST и SMT-encoder)

Решение

Nova поддерживает bounded quantifiers — только по конкретным коллекциям или диапазонам. Unbounded quantifiers (forall x : T : P(x)) запрещены (compile error).

requires forall i in 0..xs.len() : xs[i] >= 0
ensures  exists i in indices : result == xs[i]
invariant forall i in 0..k : processed[i] == true

Синтаксис:

forall <ident> in <expr> : <bool>
exists <ident> in <expr> : <bool>

expr после in — Iter[T] (array, range, set, map); body — bool, #pure (без side effects).

SMT encoding:

• Конкретный размер → конъюнкция/дизъюнкция P(xs[0]) ∧ P(xs[1]) ∧ ....
• Символьный размер → Z3_mk_forall_const с :pattern ((select xs i)).

Unbounded форма вызывает ошибку компиляции:

error: unbounded quantifier not supported
  use `forall x in collection : P(x)` (bounded form)

Обоснование

Unbounded quantifiers в SMT практически всегда требуют ручного trigger annotation и часто зависают. Bounded форма даёт детерминированный trigger через select-pattern и покрывает 95% реальных программных инвариантов. Паттерн из Dafny, Verus.

Реализация

• compiler-codegen/src/ast/mod.rs — ExprKind::Forall { var, iter, body }, ExprKind::Exists { ... }.
• compiler-codegen/src/parser/mod.rs — парсинг forall/exists; reject unbounded form.
• compiler-codegen/src/types/mod.rs — type-check: iter → Iter[T], body → bool, #pure.
• compiler-codegen/src/verify/encode.rs — конъюнкция (concrete) или forall с pattern (symbolic).

D113. #must_verify_module — strict mode на модуле

Статус: Запланировано (Plan 33.3 Ф.13, Plan 33.4 V2)

Решение

Атрибут #must_verify_module на модуле переводит все функции внутри в режим #must_verify — любой unprovable контракт становится compile error (не fallback на runtime).

#must_verify_module
module banking.core {
    fn transfer(from int, to int, amount money) Db -> ()
        requires amount > 0
        ensures  Db.balance(to) == old(Db.balance(to)) + amount
    => ...
}

Целевой use-case: критичные компоненты (финансы, медицина, авионика) где runtime-fallback неприемлем. Паритет с Dafny :verify true на модуле.

Функция внутри #must_verify_module может явно opt-out через #unverified (задокументированное исключение).

Обоснование

#must_verify на каждой функции — verbose. Module-level атрибут выражает намерение «этот модуль формально верифицирован» одной строкой. Позволяет CI-gate отделить critical-core от ordinary code.

Реализация (V2)

• compiler-codegen/src/ast/mod.rs — флаг must_verify_module в ModuleDecl.
• compiler-codegen/src/types/mod.rs — при type-check fn в таком модуле: применять semantics #must_verify ко всем fn без явного #unverified.

D114. SMT cache + parallel verification

Статус: Запланировано (Plan 33.3 Ф.12, V2)

Решение

Incremental SMT cache

target/contracts-cache/<hash>.json хранит результат верификации каждой функции:

{
  "fn_id":          "module/path::fn_name",
  "input_hash":     "sha256:<AST + deps + contracts>",
  "smt_query_hash": "sha256:<encoded SMT>",
  "result":         "proven",
  "solver":         "z3-4.13.0",
  "duration_ms":    142
}

Pipeline: compute input_hash → lookup → cache hit → skip SMT call. Инвалидация по изменению любой transitive contract-dependency (Salsa-style).

Parallel verification

verify/worker.rs через rayon::ThreadPool с N = num_cpus workers. Каждая verify_fn — independent job со своей SMT-context (Z3 thread-safe: Z3_global_param_set("parallel.enable", "true")). Финальный diagnostics-merge в главном потоке.

Acceptance targets:

• Incremental rebuild без изменений на 100-fn corpus — < 2 сек.
• Parallel speedup >= 6× на 8 cores.
• Release binary identical для proven fn (zero-cost erasure).

Обоснование

Верификация контрактов линейно растёт с размером кодовой базы. Без кэша и параллелизма time-to-compile с включёнными контрактами становится непрактичным уже при 500+ функциях. Паттерн из Dafny incremental / Verus parallel.

Реализация (V2 plan)

• compiler-codegen/src/verify/worker.rs — rayon ThreadPool.
• compiler-codegen/src/verify/pipeline.rs — cache lookup/save.
• target/contracts-cache/ — директория с JSON-артефактами.

D116. Z3 backend через собственные FFI-биндинги

Статус: Принято (Plan 33.3 Ф.9, реализовано 2026-05-14)

Решение

Nova линкует Z3 напрямую через собственные FFI-биндинги (z3_ffi.rs) без зависимости от crate-экосистемы (z3-sys, z3 crate).

Биндинги декларируют только те функции Z3 C API, которые реально используются в Z3Backend — менее 30 функций. Выбор конкретной версии Z3 полностью под контролем Nova.

Backend реализует trait SolverBackend и выбирается через pipeline-selector: --smt-backend=z3 (default) или env var NOVA_SMT_BACKEND=z3.

Обоснование

Crate z3-sys / z3 — внешние зависимости с независимым release cycle. Историческая практика в Nova: не патчить и не полагаться на сторонние аблокации критичных подсистем (ср. политику с minicoro, Boehm GC). Собственные биндинги дают:

• Полный контроль над версией Z3.
• Минимальный API surface (менее 30 функций vs тысячи в полном z3-sys).
• Возможность свитч Z3 -> CVC5 без смены интерфейса.

Реализация

• compiler-codegen/src/verify/backend/z3_ffi.rs — FFI-объявления (~25 функций Z3 C API).
• compiler-codegen/src/verify/backend/z3.rs — Z3Backend struct, реализация SolverBackend.
• compiler-codegen/src/verify/backend/mod.rs — SolverBackend trait, factory/selector по env/flag.
• compiler-codegen/build.rs — feature z3-backend; link Z3 shared lib.

Cross-check Z3 ↔ CVC5 (Plan 33.14)

Вторая, полностью независимая от FFI, линия проверки VC. CVC5 подключён не через FFI, а через текстовый SMT-LIB v2 и подпроцесс — это намеренно: текстовый путь не разделяет код с Z3-FFI-трансляцией и служит вторым независимым кодировщиком (поймал бы баги кодирования вроде Plan 33.8 Ф.6.2 даже без второго решателя).

• compiler-codegen/src/verify/smtlib.rs — SmtLibEmitter: SmtTerm → текст SMT-LIB v2. Точное зеркало Z3Backend-трансляции по набору операторов; при любой неуверенности — EmitError, а не приблизительный вывод (иначе cross-check давал бы ложные disagreement’ы).
• compiler-codegen/src/verify/backend/cvc5.rs — Cvc5Backend: SmtBackend через подпроцесс cvc5. Бинарник нет → Unknown (graceful skip), не паника.
• compiler-codegen/src/verify/crosscheck.rs — CrossCheckBackend: прогоняет каждую VC через Z3 И CVC5; definite-disagreement (Proven vs Disproved) → compile-error [E2412]. Включается NOVA_CROSSCHECK=1 (CI-only режим).

Gate срабатывает только на definite-disagreement; любой Unknown / timeout с любой стороны — норма. CI-job — contracts-crosscheck.

D121. Benchmark DSL — bench "..." { measure { ... } }

Что

Top-level bench "name" { setup; measure { measured_body } teardown } construct + namespace bench.* (bench.opaque, bench.iterations, bench.reset_timer, bench.bytes, bench.elements, bench.allocs, bench.now_ns). Compiled в bench main entry только при nova bench invocation; в nova test/nova build bench-items игнорируются.

Правило

Синтаксис идентичен top-level test-declaration (D89), но keyword’ы bench и measure — контекстуальные (parses как item только когда за bench идёт string-literal; measure парсится как block-start только внутри bench-body). Это позволяет identifier’ам bench (например namespace bench.opaque) и measure существовать без коллизий.

module bench.my_module

bench "name of this benchmark" {
    // Setup — НЕ measured, выполняется один раз.
    mut m = HashMap[int, int].new()
    ro n = 1000

    // Measured block — adaptive sampling (Criterion-style).
    measure {
        mut i = 0
        while i < n {
            m.insert(i, i)
            i = i + 1
        }
        bench.elements(n)
    }

    // Teardown (optional).
}

Body grammar:

bench_decl := "bench" string_lit "{" bench_body "}"
bench_body := stmt* measure_block stmt*
measure_block := "measure" "{" block_body "}"

Body должен содержать ровно один measure { ... } блок. Statements ДО measure — setup (1×, не measured); statements ПОСЛЕ — teardown (1×, не measured); measure-body — adaptively sampled.

bench.* namespace functions (declared в std/bench.nv, dispatched hardcoded в emit_c.rs):

Adaptive sampling protocol

Codegen эмитит для каждого bench-declaration entry point, который:

1. Warmup (default 500ms via env NOVA_BENCH_WARMUP_NS): крутит measure до warmup-budget elapsed.
2. Calibration: single measure, compute iters_per_sample = max(1, target_ns / single_ns). Target default 1ms.
3. Sampling: 100 batches of iters_per_sample × measure, recording per-iter wall-clock per batch. Stop early если total > time_budget_ns (default 10s).
4. Emit JSONL на stdout: __BENCH_RESULT__ {...} с raw samples + throughput + alloc delta.

CLI (nova bench run) parses JSONL, runs statistical analysis (median, MAD, mean, stddev, p25/p75, IQR, Tukey outliers, bootstrap 95% CI, slope+R²), и emits human/JSON/CSV/MD output.

Phase G/H additions (2026-05-17)

JSON v1 schema additions (backward-compatible):

• stats.drift_slope_ns_per_sample + stats.drift_r_squared (Plan 57.G.1) — regression slope of (sample_index, raw_ns); detects cache warmup leak / thermal drift. Non-Criterion semantic — adapted к our fixed iters_per_sample sampling strategy.
• custom_metrics[] (Plan 57.G.5) — aggregated bench.metric samples per (name, unit) с count/min/max/sum/median.
• per_group_geomeans[] в nova bench diff --format json output (Plan 57.H.1) — benchstat-style per-group breakdown derived from first ’/‘-segment of bench name.

CLI additions:

• nova bench run ... --histogram (Plan 57.G.4) — Unicode block-char histogram per bench after table (M=median + [ ] Tukey fences).
• nova bench hyperfine "name=binary args..." [...] --warmup N --samples K (Plan 57.H.2) — cross-binary wall-clock timing; output совместим с bench diff.
• nova bench callgrind <binary> [args] [--cache-sim] [--out FILE.json] + nova bench callgrind-check (Plan 57.H.3) — deterministic CPU instructions count через valgrind subprocess (Linux + macOS; cross-platform fallback к Linux-only perf_event_open).

Error message decoder (Plan 57.G.3): perf_event_open failures (cpu_instr + membw paths) map к actionable hints (EPERM/EACCES → sudo sysctl -w kernel.perf_event_paranoid=1; EMFILE → ulimit -n; ENOSYS → kernel CONFIG_PERF_EVENTS missing).

Почему

• Criterion (Rust) / testing.B + benchstat (Go) / tinybench (TS) — все эти решения внешние библиотеки, не часть языка. Nova делает встроенным — exposed surface минимален, edge cases (init/teardown leaks, sample noise, alloc counting) обрабатываются один раз в runtime.
• Effect-row aware: компилятор знает по сигнатуре pure-fn → может гарантировать детерминизм measure-блока. Уникально для Nova.
• gc.alloc_count() встроен (Plan 32) — alloc tracking бесплатен.

Что отвергнуто

• #bench attribute на fn (Criterion-style) — отложено в Plan 57.B (для parameterized sweeps). Top-level bench syntax — consistent c test (D89), привычно.
• group/case sub-benches — отложено в Plan 57.A (требует больше parser changes).
• bench как hard keyword — ломает existing identifier’ы (module bench.X, namespace bench.opaque). Решено через contextual lexing (как apply в Plan 33.5).
• Statistical analysis в runtime (C) — perf overhead, complexity. Делается в CLI (Rust): bench-bin emits raw samples JSONL, CLI агрегирует.

Связь

• D89 (test tooling) — bench parallel/sibling.
• Plan 32 (gc.* introspection) — alloc tracking bridge.
• Plan 22 (libuv integration) — uv_hrtime() для measurement primitive.
• Plan 57 (полный 10-layer design + MVP / 57.A / 57.B phasing).
• docs/perf-conventions.md — pragmatic guide.

D127. Stability-tier enforcement scope (Plan 71)

Что

#stable / #unstable / #experimental (определены в D105) не требуются на каждом exported item. Lint public-missing-stability (Plan 45 §11.5 №7) имеет следующий scope:

1. По умолчанию — severity = warning. CI не блокируется.
2. enforce-stability = true в nova.toml [lib] — severity = error. Opt-in для пакетов, обязующихся документировать stability публичного API (stdlib, library crates с обратной совместимостью).
3. Fixture/example exemption — независимо от flag, файлы под путями nova_tests/**, tests/**, examples/**, bench/** (relative to manifest root) skip’ают правило полностью. Эти контексты — не “stable API surface”.

Manifest формат

# nova.toml
[lib]
src = "."
enforce-stability = true   # optional, default false

Boolean. Любое не-true значение трактуется как false (forward-compat для будущих enum’ов severity’ей, если потребуются).

Почему

1. Industry baseline — Rust stdlib единственный enforces stability строго (#![feature(staged_api)]), и только для stdlib, не для user crates. Swift, Kotlin, Go, Python, OCaml, Haskell — convention-based без enforcement. Nova консервативно расширяет: default warning (учит conventions), opt-in error (для production library crates).
2. Test fixtures — не public API. Требовать stability annotation’ов с nova_tests/doc/fixtures/**/*.nv методологически неверно: fixtures существуют как тестовые данные для doc-collector’а, не как stable API surface.
3. CI не должен падать на новых fixture’ах. До Plan 71 каждое добавление test fixture без #stable ломало nova-doc CI workflow. Auto-exempt path-prefix логика устраняет этот mode-failure.
4. Stdlib opt-in. std/nova.toml приобретает enforce-stability = true — stdlib обязан декларировать stability каждого export’а, как user-facing API. User-application’ы не обязаны.

Что отвергнуто

• Per-file #allow(public-missing-stability) — отложено в Plan 71.A (требует расширения lint-attr infrastructure). Path-prefix exemption покрывает 95% legitimate use cases.
• Manifest-config fixture_dirs = ["custom/path"] — отложено V2. Hardcoded prefix список (nova_tests/, tests/, examples/, bench/) — стандартная convention, override редко необходим.
• Default = error (strict-by-default) — выбрано против. Учить conventions warning’ами лучше, чем блокировать CI у каждого нового contributor’а.
• --strict-stability CLI flag — overlap с manifest-level setting; manifest — единый source of truth. CLI override может быть добавлен в Plan 71.A если возникнет user-запрос.

Связь

• D105 — определение #stable / #unstable / #experimental атрибутов.
• Plan 45 Ф.23.12 §11.5 №7 — определение lint public-missing-stability.
• Plan 71 — implementation.
• docs/idioms/stability-tiers.md — pragmatic guide.

D165. Consume-types migration policy — nova consume-migrate + editions

Plan 100.7. Принято 2026-05-23 (proposed). Migration playbook для type-level consume (D133-D164). Integrates с D366 edition versioning.

Что

nova consume-migrate <path> CLI subcommand для assisted migration existing stdlib-типов на consume-семантику. Edition-versioning preserves backward-compat.

CLI subcommand

$ nova consume-migrate std/io/file.nv

Analyzing std/io/file.nv...
Suggestions:
  Line 5: type File { ... }
    → Suggestion: type File consume { ... }
    Reason: file_open returns File, file_close consumes; resource type.

  Line 12: fn File @close() -> Result[(), IoErr]
    → Suggestion: fn File consume @close() -> Result[(), IoErr]
    Reason: close is consume-method (terminal).

Apply (y/n/manual)?

Modes: --dry-run / --apply / --interactive.

Edition-versioning (D366 integration)

[package]
edition = "2026"                                # pre-consume era; legacy API
# vs
edition = "2027"                                # post-consume; migrated API

std/prelude/<edition>.nv resolver (Plan 62.F.bis D366) picks correct stdlib version per package edition.

Deprecation cycle

// Edition 2027 (new):
external consume fn nova_file_open(path str) -> File
fn File consume @close() -> Result[(), IoErr]

// Legacy shim для edition 2026:
#[deprecated_since("2027.1", replacement = "use `consume f = File.open()` + defer close")]
fn File.open_legacy(path str) -> File

Pilot migration scope (4 типа)

Plan 100.7 — полная migration 4 high-priority типов: File / Mutex / TcpSocket / Transaction (mock). Каждый — 5 probes (open-use-close / parallel / error / cancel / cross-fiber).

Сравнение

Связь

• D133 — type-level consume.
• D366, D125 — edition versioning ✅.
• D164 — cross-package contracts.
• Plan 18 — real stdlib (after pilots).
• Plan 28, Plan 36 — CLI infra.

D166. Consume-types developer experience — performance, IDE, docs

Plan 100.8. Принято 2026-05-23 (proposed). Cross-cutting нормы: compile-time budget + LSP API + diagnostic format spec.

Что

Production-grade developer experience для consume-types (Plan 100 family):

1. Compile-time performance budget — check_consume pass overhead < 5% от total nova check time.
2. LSP quick fixes для всех 12 Plan 100 error codes.
3. Hover info с consume status + coverage analysis.
4. nova doc integration — [consume] badges, Resource lifecycle.
5. nova consume-analyze CLI — standalone diagnostic.
6. Structured diagnostic format spec — error-code + ranges + suggestions + notes; JSON-консьюмabel.

Compile-time performance budget

Verification — Plan 57 bench framework (D121).

LSP quick fixes (12 error codes)

Machine-applicable edits через D102 suggestion format.

Hover info format

consume tx: Transaction
  Status: Live (consume obligation pending)
  Type defined in: a/types.nv:5 (package 'a' v1.0)
  Consume methods:
    .commit() -> Result[(), CommitErr]
    .rollback() -> Result[(), RollbackErr]
  Coverage:
    Line 7: `errdefer { tx.rollback() }` covers error-path
    Success path: NOT COVERED (suggest okdefer or explicit commit)

Diagnostic format spec

error[D133-not-consumed]: consume value not consumed before scope exit
   ╭─[file.nv:8:5]
 5 │     consume tx = begin()
   │     ━━━━━━━━━━━━━━━━━━━━ consume binding declared here
 8 │ }
   │ ━ scope exit; tx still Live
   ╰─
   note: type `Transaction` declared `consume` at types.nv:3
   help: consume via:
         .commit() -> Result[(), CommitErr]   (success path)
         .rollback() -> Result[(), RollbackErr] (cleanup)
   suggestion (machine-applicable):
         + errdefer { tx.rollback() }
         + tx.commit()?

JSON variant — D107 schema extension.

nova doc integration (D104-D107)

• Type-decl badge: [consume] next to type name.
• Methods: [consume] annotation на consume-methods.
• Section “Resource lifecycle” — open/use/close pattern.
• Links to docs/idiom/<type>-resource.md.

Сравнение

Связь

• D102 — structured suggestion format.
• D104, D105, D107 — doc-comments + JSON schema.
• D121 — bench DSL (Plan 57).
• D133-D165 — Plan 100 family error codes.
• Plan 28, Plan 36 — nova-cli infra.

D256. @field / @method() self-access в контрактах

Status: active (spec). Реализация — Plan 140.2 Part A (2026-06-13). Amends D24. Пререквизит для D257 (Vec @index bounds как элидируемый контракт, Part B).

Что

Контракт метода (requires / ensures, а также type-invariant) может ссылаться на состояние receiver’а:

• @field — чтение поля receiver’а (read-only). Пример: fn Vec[T] @index(i int) -> T requires 0 <= i && i < @len.
• Встроенные #pure-аксессоры @len() / @cap() / @byte_len() / @is_empty() — zero-arg size-аксессоры (D117 call-syntax). Кодируются идентично соответствующему @field (@len() ≡ @len).

Прочие @method() (non-accessor, non-#pure, либо с mut/consume-receiver) в контракте НЕ поддерживаются — checker даёт внятную ошибку (не обобщённый E2401-encoder-reject), указывая на конкретный @method().

Почему

До Plan 140.2 SMT-encoder отвергал ExprKind::SelfAccess (@) с E2401 («@field в контракте не поддерживается»). Это делало невыразимыми любые контракты метода о собственном состоянии (requires @len > 0, ensures result <= @cap, …) и, в частности, блокировало bounds-as-contract для Vec @index (нельзя написать requires 0 <= i && i < @len). Обходной путь «вынести поле в явный параметр #pure fn» громоздкий и не работает для magic-методов (@index), где сигнатуру задаёт язык.

SMT-модель

• Bare @ (receiver) кодируется как стабильная SMT-переменная _self.
• @field (Member{obj: SelfAccess, name}) → _field_<name>_<sort>(_self) — та же uninterpreted-function конвенция, что для obj.field параметра. Один и тот же _self на все @field метода ⇒ верная конгруэнтность (@len в requires и @len в ensures — один и тот же терм).
• @len() / @cap() / @byte_len() zero-arg → _field_<name>_int(_self) с автоматической аксиомой >= 0 (size-аксессор неотрицателен).
• _self авто-объявляется бэкендом как Int-сущность; sort поля выводится эвристикой имени (is_*/*? → Bool, иначе Int) — как для obj.field.

Call-site instantiation (Part A.2 / Part B)

Для элизии доказуемого доступа: на call-сайте (v[idx], маршрутизируемом через контракт @index) _self подставляется фактическим receiver’ом (_self ↦ v), i ↦ idx. Тогда контракт callee 0 <= i && i < @len становится goal’ом 0 <= idx && idx < _field_len_int(v), который Z3 доказывает под loop-инвариантом for i in 0..v.len(). MVP — индекс есть loop-var с явной границей v.len()/@len (см. Plan 140.2 Part B).

Границы (V1)

• Только чтение @field; запись @field в контракте невозможна синтаксически (контракт — выражение, не statement). mut @field-вектор — только через mut/consume-receiver @method(), который отклонён.
• Общие #pure @method() (не из списка аксессоров) — не инлайнятся в SMT (V1); followup при необходимости (inline #pure method body как для свободных #pure fn).

Диагностика контракт-нарушения (follow-up 2026-06-13)

Раз Part A впервые разрешил @-аксессоры в контрактах, runtime-сообщение о нарушении (<file>:<line>: requires failed: <src>) обязано рендерить их читаемо. Codegen-рендерер expr_to_display (emit_c) до этого имел catch-all _ => "assert" и не покрывал Member/SelfAccess/Index → requires 0 <= i && i < @len печаталось как … i < assert. Баг был невидим существующим тестам: при наличии custom-message маркер матчил только её, а garbled <src> живёт в скобках (failed: msg (<src>)). Исправлено: добавлены армы для Member (@field/obj.field), SelfAccess (@), Index, char/float-литералов, Path, as/is, turbofish; дефолт "assert" → честный "<expr>". Семантика проверки не менялась (только текст сообщения). Маркер [M-140.2-contract-exprdisplay-selfaccess] (backlog) — CLOSED.

• Type-invariant уже использует bare-ident поля (invariant balance >= 0), а не @field; D256 не меняет этот путь.

Связь

• D24 — стратегия SMT-проверки (amended: @field теперь разрешён).
• [D117] — size-accessor uniformity (@len() ≡ @len).
• D257 — Vec @index bounds как элидируемый контракт (Part B; первый потребитель D256).
• [M-140-bounds-as-contract] — маркер, закрываемый Plan 140.2.

D257. Vec @index bounds как элидируемый контракт

Status: active (spec). Реализация — Plan 140.2 Part B (2026-06-13). Зависит от D256 (@field в контрактах) + D24/Plan 140 (enforce-with-elision) + D248 (&&-форма).

Примечание: это бывший преждевременный D249, отозванный до того, как Part A (D256) разблокировал @field в контрактах; теперь внесён под номером D257 (D249–D255 — за Plan 152).

Что

Vec[T] @index(i int) -> T и Vec[T] mut @index(i int, val T) несут контракт requires 0 <= i && i < @len (вместо прежнего ручного if i < 0 || i >= @len { panic(...) }). Bounds-проверка становится элидируемым контрактом по модели D24/Plan 140:

• индекс, доказанный SMT in-bounds (напр. for i in 0..v.len()), — проверка элидируется (zero-cost);
• недоказанный индекс — runtime-проверка остаётся и в debug, и в release; OOB → fail-fast abort (не silent UB).

@get(i) / @first() / @last() (возвращают Option[T]) — без контракта: None на OOB остаётся их штатной семантикой (это и есть безопасный безконтрактный путь для «может не быть элемента»).

Codegen (context-sensitive)

v[i] имеет три контекстно-зависимых пути; все сохраняют inline-эмиссию (маршрутизация через value-возвращающий метод сломала бы lvalue-контексты):

• rvalue v[i] (чтение) — lvalue-safe bounds-checked stmt-expr (*({ …; &data[i]; })) (та же форма, что NovaArray), чтобы v[i].field = x, &v[i], v[i].mut_method() оставались корректными;
• write v[i] = val — inline statement-block;
• bounds-check в обоих путях элидируется на доказанных index-сайтах (per-site proven-множество от верификатора), иначе always-on.

Прямой вызов v.index(i) (редкий) попадает в mono’d-тело @index. NB (Plan 140 gap): contract-enforcement requires пока НЕ эмитится для generic-type mono’d методов, поэтому тело @index/mut @index сохраняет явный runtime-guard if i<0 || i>=@len { panic("Vec: index out of bounds") } (он и ловит OOB прямого вызова — message «Vec: index out of bounds», не contract-violation). Когда generic-mono enforcement починят, guard станет избыточным (его уберут — requires будет enforce’иться). Inline v[i] через это тело не диспатчится и безопасен своей (элидируемой) проверкой.

Условие доказуемости элизии (verifier) + soundness

Верификатор (prove_vec_index_sites, гейт non-trivial backend) доказывает 0 <= idx && idx < v.len() для каждого v[idx]-сайта (read И write-back v[i]=val) под loop-bound for i in lo..v.len(); доказанные сайты — в proven-множестве для codegen-элизии.

Frame-условие (обязательно для soundness): длина v должна быть инвариантна в теле цикла. Z3 моделирует _field_len_int(v) как фиксированное, а Nova переоценивает 0..v.len() каждую итерацию — поэтому мутация длины ДО доступа сломала бы i < v.len()@access. Frame-check (*_len_safe) допускает v лишь как: v[i]-read, v[i]=val in-place-write (mut @index СОХРАНЯЕТ длину) и аксессоры v.len()/cap()/byte_len()/is_empty(); length-changing методы (push/pop/insert/remove/…), &v, передача v в вызов, реассайн v и любое bare-v → НЕ len-safe → сайт не элидируется (консервативно safe). Bound берётся из loop-bound, fn-level frame-safety (vec len-инвариантен над всем телом → v[0..v.len()] вне цикла) или fn-requires.

Покрытие: скалярный v[i] (read + write-back v[i]=val); slice v[a..b] (0<=a && a<=b && b<=v.len(), inline-проверка элидируется); cross-fn — v[i] внутри fn helper(v,i) requires 0<=i && i<v.len() (bound из requires, см. ниже).

Два proven-множества (soundness под --contracts=off):

• always-safe — bound доказан из LOOP/CODE (без requires): loop-bound, fn-frame-safety, slice-константы. Элидируется ВСЕГДА.
• contract-based — bound доказан ТОЛЬКО с учётом fn-requires (cross-fn). Codegen элидит только при включённых контрактах: под --contracts=off / #unchecked сам requires не enforced (проверка на входе fn стёрта), поэтому inline bounds-check ДОЛЖНА остаться (иначе OOB-UB). Verifier различает их двойным доказательством (без requires → always; с requires \ без → contract).

Эволюция: B.4 MVP — read-only циклы; followup — write-back, slice, cross-fn ([M-140.2-elision-writeback]).

Почему контракт, а не codegen-only range-анализ

Bounds как декларативный контракт на @index: (1) единый источник истины (precondition в сигнатуре, не разбросанные codegen-паники), (2) верификатор/инструменты могут о нём рассуждать, (3) элизия — следствие доказательства контракта на call-сайте (D256 call-site instantiation), а не отдельная codegen-эвристика. Sibling [M-opt-elide-proven-overflow-checks] (чистая codegen-range элизия overflow-чеков) — альтернативный не-контрактный путь, не пересекается.

Связь

• D256 — @field в контрактах (пререквизит: без него requires … @len = E2401).
• D24 / Plan 140 — enforce-with-elision.
• D248 / Plan 150 — &&-форма (вакуумная 0 <= i < @len — compile-error).
• [D238] / [D240] — @index / MutIndex magic (v[i] / v[i] = val).
• [M-140-bounds-as-contract] — маркер, закрываемый этим блоком.

D272. Элизия доказуемо-безопасных int-overflow проверок

Plan 140.4 ([M-opt-elide-proven-overflow-checks]); реализует отложенную «Ф.1.3 overflow-VC оптимизация» из Plan 33.8. Sibling к D257 (тот — bounds-чеки; этот — overflow-чеки), та же модель enforce-with-elision D24.

Проблема

Plan 33.8 Ф.1.2 (04-effects.md: int overflow = panic, D13) эмитит always-on checked-форму для каждого безграничного int +/-/*: nova_int_checked_{add,sub,mul} → __builtin_*_overflow → nv_panic. Это soundness-guard (нет silent wrap/UB), но в горячих циклах большинство чеков доказуемо лишние (for i in 0..N { … i + j … } не переполнит i64).

Решение

int моделируется безграничным Z3-Int (overflow-концепции у него нет), поэтому доказательство — range-fit: для a OP b доказать INT64_MIN <= (a OP b) <= INT64_MAX под доступными фактами (литералы, requires, loop-bounds for i in lo..hi, nat >= 0). Runtime-чек паникует ⇔ истинный математический результат выходит за i64 → доказательство in-range = условие элизии. Операнды НЕ ограничиваются искусственно → цель доказуема лишь при реальных фактах → sound by construction. * нелинеен → Z3 часто Unknown → консервативно оставляем чек (никогда не элидируем без пруфа).

Два proven-множества (граница soundness — как D257)

int-overflow panic — реальный safety-guard: никогда не элидируется одним лишь #unchecked — ТОЛЬКО пруфом (always-safe множество контракт-независимо и потому элидируется даже под #unchecked; contract-based — нет). Реализация: verify prove_int_overflow_sites (двухпроходный, зеркало prove_vec_index_sites, non-trivial backend gate); codegen overflow_site_elided(span) гейтит две binary-эмиссии (emit_expr + emit_expr_with_target_type).

Scope (V1)

Binary-выражения int +/-/*. Compound-assign (x += y) отложен — аккумуляторы безграничны (редко доказуемо), отдельный AST-путь → [M-140.4-compound-assign-overflow-elision]. Sized-типы (wrap, Plan 33.7) и //%/унарный - (нет checked-хелпера) — вне scope.

Связь

• D24 / Plan 140 — enforce-with-elision (та же модель).
• D257 / Plan 140.2 — bounds-элизия (sibling-механика).
• 04-effects.md / D13 / Plan 33.8 — int overflow = panic (что элидируем).
• [M-opt-elide-proven-overflow-checks] — маркер, закрываемый этим блоком.

D376. Test-discovery skip/route-конвенции — fixtures/, OS-суффикс, _slow.nv (ex-D277, renumber 2026-07-03)

Plan 156 ([M-test-runner-large-test-lane]) — нормирует все discovery-конвенции test-runner’а (compiler-codegen/src/test_runner.rs), которые ранее были зафиксированы только кодом, и вводит slow-lane. Sibling к D89 (тот — per-file content-маркеры EXPECT_*; этот — per-path/per-name discovery-конвенции, решаемые до чтения файла). Cross-ref: D100 (_module.nv peer-config), D99 (OS-суффикс семейство), docs/plans/156-test-runner-slow-lane.md.

Что

nova test (test-discovery walker walk_nv / walk_nv_filtered) не каждый .nv-файл и не каждый каталог в nova_tests/ трактует как runnable test. Часть путей — вспомогательные (input-данные, peer-конфиг), часть — гейтится (OS, slow-lane). Эти решения принимаются на этапе discovery (по имени dirent’а, до чтения содержимого файла) — в отличие от D89 EXPECT-маркеров, которые видны лишь после чтения первых 30 строк. Нормируются здесь единым перечнем, чтобы любой Nova-conformant runner реализовал ту же конвенцию.

Правило

Скип каталогов (вспомогательные входные данные, не тесты)

Каталог-fixture содержит input-данные (nova doc ingestion-сэмплы, intermediate doc-pipeline-файлы): часто без main/test "...", не должен компилироваться как standalone test. Доступ — explicit nova check <path> (path-based, не через discovery) или integration-tests. Реализация — is_fixture_dir(dir).

Per-file суффиксы (skip / route)

Суффикс — snake_case-хвост file_stem (без .nv). - нельзя (это идентификатор).

Канонический порядок снятия суффиксов

Суффиксы комбинируются; чтобы комбинация резолвилась корректно, они снимаются в фиксированном порядке (важно: _slow снимается ДО OS-проверки, иначе OS-гейт на foo_windows_slow.nv увидел бы …_slow-хвост и не распознал OS):

1. _module → whole-file skip (раньше всего; файл вообще не тест).
2. _slow → lane-routing (Exclude/Include/Only); затем суффикс отрезается.
3. _test → отрезать (наименование).
4. OS-суффикс → проверить на остатке (core_stem); не-матч → skip.

Канонический порядок суффиксов в имени: <core>[_<os>][_test][_slow].nv. Примеры валидных комбинаций:

• foo_windows_test.nv — OS-гейт (_windows) + наименование (_test).
• collation_conformance_slow.nv — slow-lane (большой conformance-корпус).
• foo_windows_slow.nv — гейтится и по OS (_windows), и по slow-lane.

Флаги slow-lane (Plan 156)

• default (nova test без флагов): *_slow.nv skip (инверсия Go -short, аналог Rust #[ignore]) — дефолт-регресс быстрый.
• --include-slow: обычные тесты И *_slow.nv (merge-gate / nightly).
• --slow-only: только *_slow.nv (выделенная CI-job, доказательство G0 «без упрощений», out-of-band).
• Композиция с --filter/--skip/--include-stdlib ортогональна: lane решается на discovery, эти фильтры — после.

Хранение полных корпусов (rev-3, 2026-06-15)

Большие conformance-корпуса (*_conformance_slow.nv: collation 227800 пар ≈ 15.5 MB, normalization 19965 ≈ 5 MB, …) НЕ коммитятся в репозиторий — они регенерируются on-demand детерминированным генератором (nova-codegen unicode --emit-conformance --conformance-full --ucd-dir <UCD>) из pinned UCD в gitignored-кэш (nova_tests/**/*_conformance_slow.nv), затем гоняются nova test --slow-only. Коммитится только fast-сэмпл *_conformance.nv (~1500 case’ов). Пустой кэш → --slow-only находит 0 тестов = skip-never-fail (не ошибка; offline/без-UCD прогон зелёный). Обоснование (модель Go -long/CPython open_urlresource; cross-eco research docs/research/10-unicode-test-data-storage.md): у Nova есть байт-идентичный генератор, поэтому коммит ~23 MB регенерируемого build-output не даёт ничего сверх него, но навсегда утяжеляет историю. git-lfs / submodule / отдельная тест-репа отвергнуты для этого профиля. Полнота (G0 «без упрощений») доказывается slow-gate-прогоном (CI merge/nightly), а не наличием файлов в git.

Деферрал

• [M-156-slow-subtree-dir] — каталог slow/ + сентинел _slow.toml (зеркало fixtures/+_fixture.toml) для случая «медленный folder-module из ≥2 peers, которые нельзя запускать поодиночке». Сейчас такого теста нет (все медленные тесты — по одному сгенерированному файлу) → YAGNI. Добавляется аддитивно, не ломая suffix-механизм, когда появится первый медленный folder-module.

Связь

• D89 — sibling: per-file content-маркеры (после чтения); D376 — per-path/per-name discovery (до чтения).
• D99 — OS-суффикс семейство (_windows/_linux/_macos/_unix/_posix), единый source of truth.
• D100 — _module.nv peer-config.
• docs/plans/156-test-runner-slow-lane.md — реализация slow-lane (is_slow_file_stem, SlowLane, walk_nv_filtered).
• docs/test-conventions.md — практический guide.
• compiler-codegen/src/test_runner.rs — каноническая реализация (is_fixture_dir, is_slow_file_stem, walk_nv_filtered, SlowLane).
• [M-test-runner-large-test-lane] — маркер slow-lane; [M-156-slow-subtree-dir] — отложенный folder-module-вариант.

D298. Test-suite time budget

Plan 169.1 (2026-06-17). Фиксирует численный бюджет дефолтного nova test и пороги переноса тестов в slow-lane.

Бюджет

Эмпирический baseline (2026-06-17, 260 тестов, clang, 8 jobs): медиана 36.7s, p90 47.5s на тест (compile-dominated: 96% времени — компиляция через clang).

Порог кандидата на _slow.nv

Compile time не является критерием: floor на Windows/clang составляет ~15-35 с на любой тест (nova_rt.h + GC headers компилируются каждый раз). compile_ms одинаков у basics/literals и тяжёлого concurrency-теста — отличить по нему невозможно.

Программист решает по характеру теста (как #[ignore] в Rust, -short в Go):

• intentional sleep, stress-loop, bench — переносить в _slow
• функциональный тест, медленный только из-за compile time — оставить в дефолте

Агент применяет алгоритм по --results-file:

1. elapsed_ms ≥ 60 000 → _slow.nv
2. Имя содержит stress, bench, perf → _slow.nv
3. Иначе → оставить в дефолте

Актуальный профиль: docs/research/12-test-suite-profile-2026.md.

Fast-variant конвенция

Когда тест медленен только из-за большого параметра N:

1. Переименовать оригинал → <name>_slow.nv (обновить строку module на …_slow).
2. Создать <name>.nv с уменьшенными параметрами (итерации ≤ 500, sleep ≤ 100ms, concurrent fibers ≤ 100).
3. Добавить комментарий в начало: // Fast variant. Full test: <name>_slow.nv

Поля timing в results-file (Plan 169.1 Ф.1)

nova test --results-file out.json сохраняет на каждый тест:

• elapsed_ms — суммарное (compile + run)
• compile_ms — время codegen → C → clang/cl.exe
• run_ms — время выполнения скомпилированного бинаря

Folder-module test layout (Plan 169.1 Ф.8, 2026-06-17)

Все .nv-файлы в одной директории nova_tests/<dir>/ объявляют одинаковый module nova_tests.<dir> и образуют один compile unit (один вызов clang). Это folder-module peer layout — reduce compile units пропорционально числу файлов в папке.

Обязательные требования к новым тестам:

Конфликты имён в folder-module (одна fn foo в двух файлах) — ошибка; устраняются переименованием (fn <file>_foo) или разделением в отдельный standalone-файл.

Ссылки: D376 (discovery-конвенции _slow.nv); Plan 156; Plan 169.1.

D278. Editor syntax-highlighting keyword set MUST track the lexer

Plan 104.9 (2026-06-14).

Контекст

Подсветка .nv живёт в нескольких независимых артефактах (VSCode TextMate-grammar, vim syntax, Zed/Helix/Neovim tree-sitter queries, кастомный хайлайтер сайта). Каждый держит собственную копию списка ключевых слов. Без принудительной связи они дрейфуют: к Plan 104.9 хайлайтеры подсвечивали изъятые let/readonly/safe/handler, несуществующие race/with_timeout/cancel_scope/region, логические and/or/not (которых в Nova нет — есть &&/||/!), и НЕ подсвечивали актуальные unsafe/priv/pub/blocking/errdefer/okdefer/lemma.

Решение

1. Единственный источник истины для множества ключевых слов Nova — compiler-codegen/src/lexer/mod.rs, функция lex_ident_or_keyword. Лексема → Kw*-токен ⇔ это ключевое слово. Никакой другой документ/файл не является авторитетным; все хайлайтеры — производные.

2. Три класса лексем (хайлайтеры обязаны различать):

   • ACTIVE — лексер даёт Kw*-токен и слово валидно → подсвечивать как keyword.
   • RETIRED — лексер даёт Kw*-токен ТОЛЬКО для точной диагностики удаления (let→E_KW_REMOVED_LET, readonly→E_KW_REMOVED_READONLY, safe→E_SAFE_RETIRED); слово невалидно → НЕ подсвечивать как keyword.
   • НЕ keyword — лексер даёт Ident (handler после D142; and/or/not; race/with_timeout/cancel_scope/region) → НЕ подсвечивать как keyword.

3. Контекстные не-лексер keyword’ы (requires/ensures/invariant/old — contract-clauses; распознаются парсером позиционно) допускается подсвечивать для читаемости. apply/bench/measure/null намеренно НЕ подсвечиваются: лексер держит их идентификаторами во избежание поломки пользовательских имён.

4. Conformance-тест обязателен (compiler-codegen/tests/syntax_highlight_conformance.rs): лексит каждое слово через живой lex() (anchor к компилятору) и проверяет каждый in-repo хайлайтер на отсутствие фантомов + полноту (для regex-хайлайтеров). Артефакт из отдельного репо (сайт) имеет собственный guard (www/site/scripts/check-highlight-keywords.mjs).

5. tree-sitter-хайлайтеры (Zed/Helix/Neovim) ограничены токенами внешней грамматики github.com/nv-lang/tree-sitter-nova. Когда грамматика отстаёт — недостающие keyword’ы документируются inline + в backlog ([M-treesitter-grammar-keyword-bump]), НЕ замалчиваются.

Связь

• editors/README.md — раздел «Source-of-truth для keyword’ов»
  • чеклист «обновить при добавлении keyword’а».
• Q38 — открытый вопрос: генерировать keyword-списки ИЗ лексера (единый источник, без дублирования) vs ручная поддержка + conformance-тест.
• docs/plans/104.9-syntax-highlight-keyword-sync.md.

D283. Reachability-based codegen DCE — эмиссия только достижимого (вариант A, Zig-модель)

Plan 159 ([M-reachability-codegen-dce], 2026-06-15). Codegen-policy: что попадает в сгенерённый C. Родственно codegen-элизии D272 / D257, но здесь — decl-level (целые функции/таблицы/методы выкидываются из эмиссии), а не per-site проверка внутри тела. Cross-ref D371 (const-shadow gate should_skip_const — смежный const-эмиссионный путь), docs/plans/159-reachability-codegen.md, research docs/research/11-stdlib-method-resolution-reachability.md.

Что

Codegen эмитит в C только объявления (free fns, module-level const, ro lazy-static globals, методы), достижимые от корней программы. Это вариант A (модель Zig: «компилируется лишь достижимое от entrypoint»), а НЕ прекомпиляция + линкерный dead-strip (вариант B = Rust/Go, отложен под скорость сборки). До Plan 159 codegen не делал анализа достижимости и эмитил всё объявленное/импортированное (замер: import std.unicode.{is_alphabetic} + вызов только is_alphabetic → C 10606 строк с collate/normalize/words/sentences/graphemes/case).

Правило

1. Roots — main (executable). У Nova нет C-ABI-экспорта, поэтому в executable export/pub-free-fns НЕ являются roots и режутся, если недостижимы от main. FFI-entry = только is_external (тело External) — такие функции вне DCE.
2. «нет main ⇒ держим всё» (БИБЛИОТЕЧНЫЙ режим). Без main (library / negative EXPECT_CC_ERROR-фикстура) DCE выключен — эмитится весь публичный API. Это и отличает executable (срез) от library (полнота API).
3. Reachable-set — worklist от roots по прямым ссылкам (вызов/взятие адреса/чтение const/ro-таблицы/конструктор типа). const и ro-globals (гигантские *_DATA-таблицы) держатся только если их читает достижимая функция/const.
4. Непрямые ссылки (критично для корректности): protocol dynamic-dispatch, замыкания/fn-указатели, @-методы, for/parallel-for iteration, операторы (==/+/[k]), string-interpolation desugar, а также интерполяция в сообщениях контрактов (requires/ensures/invariant <e>, "...${f}..." — Contract.message_expr, десугарится на сайте нарушения) — все засеиваются как достижимые-по-имени (codegen-injected селекторы видны сборщику имён). Сборщик collect_used_names обязан обходить эти позиции: Item::Fn контракты И Item::Type инварианты включают message_expr (иначе method-DCE срежет int→str- конвертер → nova_str ← int CC-FAIL; найдено полным регрессом Plan 159).
5. Method-level DCE — метод T.m эмитится ⇔ достижимо значение типа T И селектор m вызван по имени (прямой/protocol). Монотонный fixpoint. Coarse-by-name: name-collision over-keep’ит (никогда не over-prune’ит).
6. Дженерики — mono-on-use: эмитится только инстанцированная комбинация типов.
7. Kill-switch NOVA_REACH_DCE (читается один раз): unset / != "0" ⇒ DCE ON (default); "0" ⇒ байт-идентичное старое поведение (escape hatch для диагностики over-prune-подозрений).

Почему

G0 — консервативная корректность (release-инвариант): НИКОГДА не отрезать достижимое. Лучше лишнее оставить (over-keep), чем уронить runtime «undefined symbol». Под этим инвариантом name-collision и любая неопределённость разрешаются в пользу сохранения. Окупается на каждой компиляции (время cc + размер бинаря), снимает opt-in-стоимость Unicode-таблиц, ломает цикл prelude↔std.unicode и открывает no-import char-методы (DCE срезает неиспользуемые таблицы → no-import стоит ноль). Прецеденты: Zig Sema/AIR (lazy per referenced decl), rustc monomorphization collector (обход от roots).

Что отвергнуто

• Вариант B (прекомпил std в .o/.a-кэш + cc --gc-sections) — отложен под скорость сборки (не корректность): нужен стабильный C-ABI std + кэш-инвалидация + кросс-toolchain --gc-sections (болело в Plan 82 на MSVC/clang/gcc). Не пререквизит для корректных opt-in/no-import char-методов.
• export как root в executable — отвергнуто: у Nova нет C-ABI-экспорта, держать публичные fns в .exe бессмысленно (они недостижимы от main).
• Полная lazy-module-resolution (ленивый резолв/тайп-чек тел модулей при первой ссылке) для Ф.4 — заменена менее инвазивным Option A (инъекция import std.unicode в entry-модуль при детекте char-method-call). Полная ленивость отложена ([M-159-lazy-module-resolution], P3).

Реализация

compiler-codegen/src/codegen/emit_c.rs: reach_dce_enabled() (OnceLock-kill-switch); compute_dead_decls(module) → DeadDecls{dead_fns, dead_consts, dead_method_keys} (обобщает прежний compute_dead_free_fns); гейты на emit_const_decl-loop, emit_lazy_const-loop, fn fwd-decl + body loops. compiler-codegen/src/lints.rs: collect_used_names/collect_expr — сбор bare-ident + Member-селекторов + засев desugar-селекторов + @method:-тег (Ф.4). Все гейты no-op при DCE off / library mode.

Связь

• docs/plans/159-reachability-codegen.md — план + замеры + критерии A1-A5/G0.
• docs/research/11-stdlib-method-resolution-reachability.md — кросс-языковой research (import ⊥ unused-elimination; вариант A vs B).
• D371 — const-shadow gate (should_skip_const), смежный const-эмиссионный путь.
• [M-reachability-codegen-dce] (Ф.1 core ✅ DONE), [M-159-method-pruning] (P3, coarse-by-name per-kind аудит), [M-159-lazy-module-resolution] (P3), [M-152.3b-char-methods-no-import] (✅ CLOSED через Ф.4).

D296. CodeAction machine-applicable contract (Plan 104.5)

Added 2026-06-16, Plan 104.5. Extends D102 (Suggestion API) — defines the LSP layer contract for quick-fixes.

§1 Error code extraction

Nova diagnostic messages embed a machine-readable error code as a [E_CODE] prefix:

[E_LOCAL_NOT_MUT] binding `x` is not marked `mut` — call chain requires mutation

The LSP adapter (diagnostic_mapping::to_lsp) extracts this prefix and sets:

Diagnostic.code = Some(NumberOrString::String("E_LOCAL_NOT_MUT"))

This enables:

1. Editor lightbulb filtering (only show bulb when code matches a known fix).
2. textDocument/codeAction dispatch via exact code-string match.

Extraction rule: message starts with [E_<UPPERCASE_ALPHANUMERIC_UNDERSCORE>]. Non-matching prefixes (e.g., [NOTE]) produce code = None.

§2 CodeAction kinds

§3 Performance budget

• textDocument/codeAction handler ≤ 100ms total.
• Per-fix computation: O(n) source-scan on the diagnostic line only. No re-compilation.
• compute_code_actions is called synchronously (no spawn_blocking) — all fixes are text-only.

§4 V1 coverage (≥25 fixes)

104.5.2 — Plan 101 (8 fixes): E_UNDECLARED_TYPEVAR_IN_RECEIVER, E_BARE_TYPEVAR_NEEDS_PREFIX, E_DUPLICATE_GENERIC_DECL, E_PREFIX_SHADOWS_NAMED_TYPE, E_UNUSED_PREFIX_TYPEVAR, E_BOUND_UNKNOWN, E_BOUND_NOT_PROTOCOL, E_PROTOCOL_EMBED_UNKNOWN.

104.5.3 — Plan 100 (7 fixes): E_CONSUME_KEYWORD_MISSING, E_LOCAL_NOT_MUT, E_PARAM_NOT_MUT, E_ADDR_OF_REMOVED (Plan 118.6 rename from E_ADDR_OF_MUT_REQUIRES_MUT_BINDING), E_REDUNDANT_POINTER_RO, E_REDUNDANT_TYPE_MODIFIER, E_REDUNDANT_IMPORT_ALIAS.

104.5.4 — General (7 fixes): E_PROTOCOL_EMBED_NOT_PROTOCOL, E_PROTOCOL_EMBED_CYCLE, E_PROTOCOL_EMBED_DUPLICATE, E_PROTOCOL_EMBED_NOT_NAMED, E_EXTENSION_METHOD_NEEDS_IMPORT, E_KW_REMOVED_LET, E_KW_REMOVED_READONLY.

104.5.5 — Auto-import (3 fixes): E_TYPE_UNKNOWN (known stdlib types), E_BOUND_UNKNOWN (stdlib protocols), E_AUTO_DERIVE_UNKNOWN_PROTOCOL (Levenshtein suggestion).

104.5.6 — Protocol impl fixes (7 fixes, added 2026-06-17): E_METHOD_REDEFINITION, E_IMPL_UNKNOWN_PROTOCOL (suggest import for known stdlib protocols), E_IMPL_NOT_A_PROTOCOL_METHOD, E_IMPL_SIGNATURE_MISMATCH, E_PRIMITIVE_NO_PROTOCOL_METHOD, E_BLANKET_CONFLICT, E_DUPLICATE_PROTOCOL_IMPL.

104.5.7 — Field/type fixes (2 fixes, added 2026-06-17): E_FIELD_MODULE_PRIVATE (guidance note), E_TYPE_NAME_TOO_SHORT (guidance note).

104.5.8 — String operation fixes (2 fixes, added 2026-06-17): E_STR_NO_LEN (MachineApplicable: replace .len → .byte_len()), E_STR_NO_INT_INDEX (guidance note).

Plan 172.5 — In-out ref-параметры (D326, added 2026-07-06): E_REF_ALIAS_OVERLAP (headline: два mut ref-аргумента одного вызова с пересекающимися местами, R9), E_REF_NOT_A_TYPE (ref в тип-позиции — parse, R1), E_REF_MODE_REQUIRES_RO_OR_MUT (голый ref без ro/mut в параметре — parse, R2), E_REF_MARKER_REQUIRED (пропущен call-site ref на mut ref-параметре, R4), E_REF_MARKER_NOT_ALLOWED (ref-маркер на не-mut ref-параметре, R4), E_REF_ARG_NOT_ADDRESSABLE (ref на rvalue / индекс-в-цепочке, R4), E_REF_ARG_NOT_MUT (mut ref borrow ro-места, R2), E_REF_ESCAPE_CAPTURE (захват mut ref-параметра closure/spawn/…, R10), E_CONSUME_RECEIVER_RETURNS_AT (реюз: consume @ -> @ — parse, R6).

104.5.9 — Comparison chain fixes (2 fixes, added 2026-06-17): E_CMP_CHAIN_UNSUPPORTED (guidance note — use &&), E_RELATIONAL_OPERAND_NOT_ORDERED (suggest import Ordered protocol).

104.5.10 — FFI C-ABI diagnostics (3 codes, added 2026-07-04, Plan 174.6 M1): These codes are emitted by the Plan 174.6 M1 checker (check_ffi_c_abi_signatures

• the *extern "C" fn coercion gate). Their message-text is normative (fixed in Plan 174.6 §4; the M0 error-index debt in 08-runtime.md D353 is discharged here). Registered as guidance-note quick-fixes (HasPlaceholders, edit = null) — the fix directs the author to convert at the FFI boundary; no single machine-applicable rewrite exists.

• E_FFI_NON_C_ABI_TYPE — a parameter/return/field of an extern "C" fn (or of a *extern "C" fn fn-pointer signature) is not C-ABI-compatible (D282 rule 2). Message: type `%T` in `extern "C" fn` is not C-ABI-compatible; allowed: scalar, raw-ptr, `str`, `Option[*T]`, `*extern "C" fn(...)`, value-record/tuple with all-C-ABI fields + fix-it (convert at the boundary).
• E_CALLBACK_THROWS_OVER_C_ABI — coercing a fn that declares Fail (or, per D353 clause 3, ANY effect) into a C-ABI fn-pointer: C invokes the callback with no Nova handler-frame on the stack. Guidance: catch/handle inside the fn, return a sentinel.
• E_CLOSURE_HAS_ENV — coercing an environment-capturing closure (or a bound method value) into a captureless C-ABI fn-pointer. Guidance: extract to a top-level free fn.

104.5.11 — Record-binding destructure diagnostics (2 codes, added 2026-07-07, D411): Emitted by the [M-d411-record-binding-destructuring] checker work (types/mod.rs). Registered as guidance-note quick-fixes (HasPlaceholders, edit = null) — both diagnoses already embed the concrete fix text in a note:, but the exact insertion span depends on formatting choices left to the author.

• E_REFUTABLE_BINDING — a ro/mut binding pattern is refutable (sum-variant record, literal, variant, |-alternation, or array-length pattern; Plan 53 check, D411 adds the code-tag). Guidance: use if let / match instead of a plain ro/mut binding.
• E_RECORD_PATTERN_NEEDS_REST — a record-pattern binding lists fewer fields than the type declares without a trailing .. (D411 ..-partial rule; ro/mut bindings only, not match-arms/for-loops). Guidance: add .., or list every field.

Total: 44 fixes (initial ≥25 met; extended to 44 across all nova-lsp language-sync work plus the Plan 174.6 M1 FFI C-ABI diagnostics and the D411 record-binding diagnostics).

Note on E_STR_NO_LEN fix applicability: The fix_str_no_len handler scans the diagnostic range for the pattern .len and replaces it with .byte_len(). This is MachineApplicable (is_preferred = true) because byte_len() is the direct equivalent for ASCII strings, and the overwhelming majority of .len usages intend byte-length. For Unicode-aware char-count, the compiler diagnostic message directs the user to as_chars().count() (O(n)) — the fix does not attempt this substitution.

§5 Suggestion vs CodeAction relationship

Diagnostic.suggestion (compiler-codegen D102 Suggestion struct) carries machine-applicable edits at the compiler level. In LSP:

• suggestion.span + replacement → converted to TextEdit { range, new_text }.
• suggestion.applicability → CodeAction.is_preferred.

V1: most fixes recompute the edit from the diagnostic range (no compiler Suggestion field used). V2: wire Diagnostic.suggestion → CodeAction edit directly for full accuracy.

§6 Deferred (V2)

• [M-104.5-suggestion-field-wiring] — use Diagnostic.suggestion.span for edit range instead of re-scanning source text.
• [M-104.5-multi-edit-rename] — rename fixes (E_PREFIX_SHADOWS_NAMED_TYPE) should update all usages in scope, not just the declaration.
• [M-104.5-organize-imports] — sort+deduplicate import list.

D297. LSP Rename Atomicity Contract (Plan 104.6, 2026-06-16)

Status: ✅ IMPLEMENTED — nova-lsp Plan 104.6 (branch plan-104-6). Note: Plan 104.6 initially labelled this D296, but D296 was taken by Plan 104.5 CodeAction spec. Renumbered D297 at merge.

Контекст

LSP textDocument/rename — cross-file операция с высоким риском введения ошибок. Простая замена текста может: (a) привести к конфликту имён, (b) сломать импорты, (c) переименовать перегруженные методы от чужих типов.

Решение — Atomic Rename Contract

Rename в nova-lsp выполняется в три атомарных фазы:

Фаза 1 — Prepare (textDocument/prepareRename):

• Cursor position → identifier validation.
• Допустимые цели: только идентификаторы (не ключевые слова, не строковые литералы, не комментарии, не пробелы).
• Возвращает PrepareRenameResponse::RangeWithPlaceholder { range, placeholder }.
• Ошибка InvalidParams (-32602) при недопустимой позиции.

Фаза 2 — Collect (textDocument/rename, step 1):

• Regex-like word-boundary scan всех open documents + workspace files на диске.
• Обновляет doc-comment [[old_name]] ссылки → [[new_name]].
• Строит WorkspaceEdit.documentChanges (массив TextDocumentEdit) — formат с OptionalVersionedTextDocumentIdentifier для version tracking.
• НЕ изменяет файлы сразу — только строит план правок.

Фаза 3 — Atomic Check (textDocument/rename, step 2):

• Применяет правки к in-memory копиям каждого изменённого файла.
• Запускает check_source_inner (parse + type-check) на каждой копии.
• Если хотя бы один файл не проходит check → вся rename операция отклоняется с ResponseError { code: -32803, message: "rename rejected: post-rename type errors in <uri>: <diags>" }.
• Это предотвращает введение E_UNDECLARED, name-collision errors и других регрессий.

Scoping rules (V1)

• Generic params [T] — scope guard через word-boundary match в пределах файла. Full per-position symbol resolution (точная scope границa) — V2.
• Receiver methods — word-boundary match обновляет все вхождения в файле. Точное ограничение по типу receiver — V2 (требует API типчекера).

New name validation

Новое имя new_name должно быть валидным идентификатором Nova:

• Не пустое.
• Начинается с буквы или _ (не с цифры).
• Состоит только из is_alphanumeric() || '_'.
• Не является зарезервированным ключевым словом Nova.

WorkspaceEdit format

Используется documentChanges: DocumentChanges::Edits(Vec<TextDocumentEdit>) — версионированный формат, совместимый с workspace.workspaceEdit.documentChanges client capability. Не используется устаревший changes: HashMap<Url, Vec<TextEdit>>.

Связь

• nova-lsp/src/rename.rs — реализация.
• nova-lsp/src/server.rs — prepare_rename + rename handlers.
• Plan 104.6 sub-plan file: docs/plans/104.6-rename-format.md.

D303. LSP hover inside fn/test bodies — items_start pattern

NEW (Plan 104.2 Ф.7, 2026-06-17)

Проблема

LSP hover не работал внутри тел функций и тестов: наведение на assert, println, вызовы prelude-функций — всегда возвращало None.

Корневая причина — semantics of resolve_imports_inline: функция prepend-ает импортированные элементы в module.items, а не appended. Из-за этого оригинальные элементы файла смещаются: если файл объявлял N items, после inline-импортов они начинаются с индекса items_start = total_after - N. Старый код использовал .take(original_len) при поиске — он захватывал только импортированные элементы (с чужими file-spans), а не элементы исходного файла.

Решение: items_start pattern

items_before_inline = module.items.len()       // до inlining
resolve_imports_for_hover(path, &mut module)   // prepend-ает импорты
items_start = module.items.len() - items_before_inline  // сколько prepended

Три правила:

1. Span-match (поиск по позиции курсора в file-spans): обходить только module.items[items_start..] (оригинальные элементы файла). Иначе импортированные элементы со span’ами из чужих файлов ложно матчат курсор.

2. Body-walk (поиск идентификатора внутри тела fn/test): тоже начинать с items_start — чужие тела не принадлежат текущему файлу.

3. Name-lookup (поиск декларации по имени после body-walk нашёл идентификатор): обходить все module.items — prelude-функция может быть в prepend-зоне (индексы 0..items_start), и её нужно найти.

resolve_symbol_at_with_limit API

pub fn resolve_symbol_at_with_limit(
    module: &Module,
    byte_offset: usize,
    items_start: usize,   // skip count: how many prepended import items to skip
) -> Option<SymbolInfo>;

• Span-match: module.items.iter().skip(items_start)
• Body-walk: find_ident_in_bodies_from(module, byte_offset, items_start) — .skip(items_start)
• Name-lookup: lookup_decl_by_name(module, &name) — iterates all items

Для hover без URI (unit-тесты без реального файла) передаётся items_start=0 через resolve_symbol_at(module, byte_offset) — resolve_imports_for_hover не вызывается.

Защита от паники

resolve_imports_for_hover оборачивает вызов в std::panic::catch_unwind — import resolution может паниковать при malformed файлах. Паника не должна крашить LSP-сервер.

Plan 104.2 дополнения (2026-06-17)

Два улучшения, реализованных поверх items_start-паттерна:

A. Приоритет body-walk над fn-signature hover

resolve_item для Item::Fn теперь возвращает None, когда курсор находится внутри тела функции (не на сигнатуре). Это позволяет body-walk сработать первым и найти фактический callee или символ под курсором, вместо того чтобы возвращать сигнатуру объемлющей функции.

До этого исправления hover на вызове foo() внутри тела fn bar() возвращал тип bar (объемлющую функцию), а не foo.

B. Тип локальной переменной из body-walk

Body-walk обнаруживает курсор на локальном биндинге (ro x int = … / mut y str) и возвращает SymbolInfo::LocalVar с явной аннотацией типа из LetDecl.ty.

Алгоритм: при сканировании Stmt::Let body-walk проверяет, попадает ли span имени биндинга под курсор; если да — возвращает SymbolInfo::LocalVar { name, ty_text, .. } с текстом типа из LetDecl.ty (если аннотация есть).

Закрывает [M-104.2-body-walk-local-var-type].

C. Инференция типа локальной переменной без аннотации (Variant B, 2026-06-18)

Если у LetDecl нет явной аннотации (ld.ty = None), LSP вызывает infer_rhs_type(rhs, env) используя ModuleEnv, полученный из nova_codegen::types::check_module в hover.rs.

Поддерживаемые случаи:

• ro x = 5 → int (IntLit)
• ro x = 3.14 → float (FloatLit)
• ro x = true → bool (BoolLit)
• ro x = "hello" → str (StrLit)
• ro x = 'a' → char (CharLit)
• ro x = 0..=5 → Range (ExprKind::Range)
• ro x = foo() → return type из ModuleEnv.fns["foo"] (первый overload)
• ro x = val as T → T
• ro x = [1, 2, 3] → []int

Вариант A (полная точность): расширить ModuleEnv полем expr_types: HashMap<Span, Ty> — followup Plan 104.3+.

Закрывает [M-104.2-local-var-type-inference].

Связь

• nova-lsp/src/hover.rs — compute_hover, resolve_imports_for_hover
• nova-lsp/src/symbol.rs — resolve_symbol_at_with_limit, find_ident_in_bodies_from, lookup_decl_by_name, infer_rhs_type
• nova_tests/plan104_9/pos_hover_prelude_calls_in_test.nv — fixture
• nova_tests/plan104_9/pos_hover_prelude_calls_in_fn.nv — fixture
• Plan 104.2 Ф.7 sub-plan file: docs/plans/104.2-hover-goto-sigp.md

D304 — Test Category Selectors: TestSelection + --positive/--compile-error/--panic/--timeout/--exit/--slow/--full (Plan 169.1.1, 2026-06-19)

Проблема. CLI nova test имел только --include-slow/--slow-only (D277). Нет способа запустить только compile-error тесты, только panic-тесты, или их комбинацию. GitHub CI не запускал полный регресс (только contracts-z3 + nova-doc) — поломки копились незаметно (Plan 169.2: десятки битых модулей).

Решение. Аддитивная двух-осевая модель категорий:

• Ось типа (по EXPECT_* маркеру заголовка; positive = нет маркера): Positive · CompileError · Panic · Timeout · Exit.
• Ось скорости (суффикс *_slow.nv): fast · slow.

Новые CLI-флаги (аддитивные, несколько = OR):

--include-slow (D376) сохранён как backward-compat алиас для --slow. --slow-only deprecated (hidden), эквивалентен --full для legacy.

Реализация.

• TestType enum (Positive/CompileError/Panic/Timeout/Exit) в test_runner.rs.
• TestSelection { types: HashSet<TestType>, include_slow: bool } заменяет SlowLane в TestAllOpts.
• detect_test_type(path) — читает первые 30 строк файла, возвращает TestType по первому EXPECT_* маркеру. Нулевой overhead для positive-тестов когда маркер не найден в первых строках.
• walk_nv_selected(root, out, &TestSelection) — заменяет walk_nv_filtered в run_all. Фильтр по маркеру, не по папке — ловит compile-error и panic тесты вне neg/.

CI. .github/workflows/nova-test-regression.yml:

• PR/push: nova test nova_tests + nova test std (positive-fast, 60 мин).
• Nightly 03:00 UTC: nova test --full nova_tests + artifact upload (360 мин).

Связь. D376 (slow-lane), D298 (time budget), Plan 169.1.1.

D378 — LSP source provenance via peer_files (file_id → path); Plan 104.10 Ф.0

NEW (Plan 104.10 Ф.0, 2026-07-04). Нумерация: план назвал блок «D304», но D304 занят Test Category Selectors (см. выше); свободные номера — D378-D380 (D305/D306 остаются свободны).

Проблема

nova-lsp резолвил символы в рамках одного файла: hover/goto использовали nova_codegen::parser::parse(src) (single-string), присваивающий всем спанам входного файла MAIN_FILE_ID = 0. После resolve_imports_inline инлайненные items парсятся с distinct file_id, но nova-lsp нигде не строил SourceMap → не мог отобразить file_id → path. Cross-file goto-definition/hover были невозможны (всегда возвращали текущий URI).

Решение: реконструкция из module.peer_files (без рефактора компилятора)

resolve_imports_inline уже заполняет module.peer_files: Vec<PeerFile> (каждый несёт (file_id, path)). nova-lsp строит file_map: HashMap<FileId, PathBuf> обходом реальных peer_files — НЕ текстовым поиском объявлений по имени. Компилятор менять не потребовалось.

// nova-lsp/src/provenance.rs
pub struct ResolvedModule { pub module: Module, pub items_start: usize,
                            pub file_map: HashMap<FileId, PathBuf>, pub env: Option<ModuleEnv> }
pub fn resolve_module_for(path: &Path, src: &str) -> ResolvedModule;
pub fn span_to_location(span: Span, file_map: &HashMap<FileId, PathBuf>, fallback_uri: &Url) -> Location;

• span_to_location: span.file_id в file_map → Url::from_file_path(target) + UTF-16 range из исходника цели (открытый буфер, иначе диск); неизвестный file_id → fallback_uri, без паники.

Entry-duality инвариант (закрывает Q-104-5)

parse(src) ставит entry-спанам file_id = MAIN_FILE_ID (0), а peer_files для entry — N ≠ 0. Решение: file_map.entry(MAIN_FILE_ID).or_insert(entry_path) → entry всегда резолвится, даже когда resolve_imports_inline вернул Err/паникнул и peer_files пуст (degraded-CU).

Entry-item isolation: provenance вместо items_start (Ф.4 correctness fix)

items_start-слайс (D303) для отделения entry-items от инлайненных imports некорректен для folder-module peers (merged peer-item может отсортироваться ПОСЛЕ item entry → item выпадает из скана). Ф.4 заменил слайс на provenance-предикат item_belongs_to_entry (span.file_id == MAIN_FILE_ID), byte-collision-proof; items_start сохранён для API-стабильности (let _).

Почему Rust-тесты, а не spec_tests/.nv

D378 — LSP-internal (provenance-слой nova-lsp), не наблюдается через nova test (не меняет codegen). Гейт — Rust unit/integration в nova-lsp/ (компилятор-как-библиотека, lsp-conventions §3).

Связь

• nova-lsp/src/provenance.rs, nova-lsp/src/symbol.rs (item_belongs_to_entry)
• Plan 35 Ф.0 (Span.file_id + SourceMap); D303 (items_start pattern, заменён provenance-предикатом)
• Потребители: Ф.3 goto, Ф.4 hover, Ф.7 rename, Ф.19 typeDefinition

D379 — ModuleEnv.expr_types: opt-in per-expression type map для IDE; Plan 104.10 Ф.2

NEW (Plan 104.10 Ф.2, 2026-07-04).

Проблема

Type-checker вычислял типы выражений при обходе, но выбрасывал их: ModuleEnv хранил только top-level (types/fns/consts). IDE не могло узнать тип произвольного выражения (r.start, foo().bar, receiver в x.method()) → type-driven completion/member-hover/signature-dispatch/ inlay/semantic-tokens были невозможны.

Решение: карта Span → TypeRef, opt-in (zero-overhead для обычной компиляции)

// compiler-codegen/src/types/mod.rs — ModuleEnv
pub expr_types: HashMap<Span, TypeRef>,   // заполняется ТОЛЬКО при record_expr_types = true

• Тип значения — TypeRef (не отдельный enum Ty — его в модуле нет; TypeRef — то, что реально возвращает infer_expr_type, богат: path + generics; рендер format_type_ref).
• Opt-in флаг record_expr_types в TypeCheckCtx. check_module → false (zero-overhead, доказан тестом: карта пуста). check_module_with_expr_types → true. Критично: НЕ замедляет nova check/build/test.
• Точки записи (POST-ORDER над infer_expr, чтобы канал resolved_types_buf из Plan 172.1 был заполнен): литералы, Ident, Member (тип объекта И результата — для Ф.6), Index, Call-return, Binary, Range, As, Tuple/Array/Record lit.
• Границы: синтетические/zero-width спаны (start >= end) НЕ пишутся; невыводимое (generic type-param T) НЕ пишется. Semantics: отсутствие в карте = «тип неизвестен» → IDE graceful.

Дизайн: переиспользование, не дублирование

НЕ построен отдельный expr-type walker — переиспользована существующая инференция чекера (infer_expr_type + resolved_types_buf). Production-подход: не текстовая эвристика, не дублирование. Остаток непокрытого (bounded, graceful) — [M-104.10-expr-types-coverage] (generic instance method-chain returns; non-primitive TupleLit; generic-instance RecordLit) — P3.

Lenient IDE variant (Ф.5)

check_module_with_expr_types_ide — возвращает ModuleEnv (с expr_types) даже при type-ошибках (обычный check_module вернул бы Err). Нужно для completion/hover на полу-написанном буфере (IDE запрашивает тип, пока код ещё не компилируется). Пара к repair_completion_buffer (LSP чинит висячую . + баланс скобок).

Почему Rust-тесты, а не spec_tests/.nv

D379 — opt-in compiler API (off by default, zero-overhead, не меняет codegen → не наблюдается через nova test). Гейт — Rust unit в compiler-codegen/types (9 тестов: pos/neg/edge + zero-overhead).

Связь

• compiler-codegen/src/types/mod.rs (check_module_with_expr_types, _ide)
• nova-lsp/src/stdlib_index.rs (Ф.5 — stdlib методы/модули из search-path, не хардкод)
• D303 §C — Variant B (hover local-var inference); D379 = Variant A, надмножество
• Потребители: Ф.5 completion, Ф.6 member-hover, Ф.8 sig-dispatch, Ф.9 inlay, Ф.10 semantic-tokens, Ф.19 typeDef

D380 — LSP V2 capability surface + diagnostic-parity contract; Plan 104.10

NEW (Plan 104.10, 2026-07-04). Итоговая capability-поверхность nova-lsp V2 (паритет с 7 LSP-пирами: rust-analyzer/gopls/tsserver/kotlin-lsp/jdtls/zls/sourcekit).

Diagnostic-parity контракт (Ф.0.5) — 🏆 differentiator

LSP diagnostic-вход сведён к тому же пайплайну, что nova check (cmd_check): number_exprs + collect_all_signatures + check_module_with_sig_table (Plan 162.2 подавляет false-positive на транзитивно-импортированных символах). Гарантия: LSP-диагностики ≡ nova check (byte-parity набора кодов/спанов) — ни один из 7 пиров не даёт формальной LSP↔CLI-parity. Закрывает Q-104-4. Degraded-CU (unsaved buffer / вне-repo / Err резолва): fallback-скан peers по module-имени → 0 ложных red на prelude/peer-символах. Import-ошибки surface (не swallowed). Числовые [Ennnn] коды → code-action dispatch работает.

Capability-поверхность (advertised в ServerCapabilities)

Governance

• no-hardcode (lsp-conventions §1/§2): методы/типы/пакеты/протоколы — из резолва компилятора (expr_types, StdlibIndex search-path, builtin_protocol_names), НЕ хардкод-таблицы (удалены Ф.5).
• degraded-mode (§2.2): completion/hover graceful на неполном буфере (lenient env + repair-buffer).
• Тесты — Rust (nova-lsp/compiler-codegen), т.к. LSP-поведение не наблюдается через nova test (см. D378/D379 «почему Rust-тесты»). Scope-out’ы (call/type-hierarchy, persistent-index, …) — явные [M-104.10-*] маркеры, не молча.

Связь

• nova-lsp/src/* (все хендлеры + capabilities в server.rs)
• D378 (provenance), D379 (expr_types), D296 (rename atomicity), D303 (hover items_start)
• Plan 104.10, lsp-conventions.md