Контракты и формальная верификация в Nova

Система контрактов Nova позволяет описать, что функция требует и гарантирует, и проверяет эти утверждения на этапе компиляции через SMT-солвер. Модель — enforce-with-elision (D24 / Plan 140), а не debug-only assert’ы: доказанный контракт элидируется (нулевая цена в runtime, даже в debug); недоказанный — проверяется в runtime И в debug, И в release (fail-fast abort nova_contract_violation, без тихого UB). Снять проверку с недоказанного можно только явно — per-fn #unchecked или build-policy --contracts=off. У opt-out три уровня (Plan 140.3): #unchecked на функции, #unchecked на модуле (перед module X), или build-флаг; плюс Eiffel-style per-kind гранулярность — #unchecked(requires) / #unchecked(ensures) / #unchecked(invariant) (комбинируемо, fn или module) элидируют только перечисленные виды. Без SMT-бэкенда proven-множество пусто → проверяется каждый контракт (safe degrade: медленнее, но не unsafe).

Нарушение контракта — как и провал assert — panic-класса: пойманное consume/supervised-скоупом, оно классифицируется как Panic, а не recoverable Failure (Plan 140.3 / D13). Сообщение requires может интерполировать runtime-значения через ${...} — requires x > 0, "got ${x}" показывает got -5 на провалившемся вызове (сообщение строится только при нарушении, не на успешном пути; Plan 140.3).

Spec: D24 (SMT-стратегия) · D111 (assume / assert_static / #trusted) · D112 (bounded quantifiers) · D116 (Z3 backend).

Quickstart

// Простое precondition + postcondition.
#verify
fn withdraw(balance int, amount int) -> int
    requires amount > 0 && amount <= balance
    ensures  result == balance - amount
    ensures  result >= 0
{
    balance - amount
}

test "contracts quickstart: withdraw" {
    assert(withdraw(100, 30) == 70)
    assert(withdraw(50, 50)  == 0)
}

// REQUIRES_SMT_BACKEND z3

// Opaque helper + reveal в caller'е — Z3 доказывает более сильный контракт.
#opaque #pure
fn double(x int) -> int
    requires x >= 0
    ensures  result >= 0
=> x * 2

#verify
fn caller_with_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2
{
    reveal double
    double(n)
}

test "contracts quickstart: opaque + reveal" {
    assert(double(5) == 10)
    assert(caller_with_reveal(7) == 14)
}

Клаузулы контракта

Клаузулы контракта располагаются между списком параметров и { телом (или => expression-body). Несколько клаузул одного вида разрешены и соединяются конъюнкцией.

requires

Предусловие. SMT-солвер предполагает его выполнение при верификации тела. Caller обязан его соблюсти.

#verify
fn safe_div(a int, b int) -> int
    requires b != 0
    ensures  result * b == a - (a % b)
{
    a / b
}

Несколько requires-клаузул эквивалентны одной конъюнкции:

#verify
fn clamp(x int, lo int, hi int) -> int
    requires lo <= hi
    ensures  result >= lo && result <= hi
{
    if x < lo { lo } else if x > hi { hi } else { x }
}

Диапазон: используйте &&, а не цепочку

Чтобы ограничить значение полуинтервалом, пишите каноническую конъюнкцию lo <= i && i < hi — НЕ lo <= i < hi:

fn at(buf []int, i int) -> int
    requires 0 <= i && i < buf.len     // ✓ настоящая проверка границ
=> buf[i]

Цепочка сравнений 0 <= i < hi — ошибка компиляции (E_CMP_CHAIN_UNSUPPORTED): иначе бы парсилось как (0 <= i) < hi = bool < hi (вакуумно-истинно — проверка границ молча превращается в no-op). Nova отвергает цепочку (и bool/unit-операнды < <= > >=, E_RELATIONAL_OPERAND_NOT_ORDERED) на этапе parse/check; пишите через && (Plan 150 / D248).

Self-access (@field, @len()) в контрактах метода

Контракт метода может ссылаться на состояние receiver’а: читать поле через @field или встроенный size-аксессор @len() / @cap() / @byte_len() / @is_empty() (call-форма взаимозаменяема с полем: @len() ≡ @len):

fn Vec[T] @index(i int) -> T
    requires 0 <= i && i < @len     // ✓ ссылается на длину receiver'а
{
    unsafe { @data[i] }
}

SMT-солвер моделирует receiver как сущность _self; каждый @field становится uninterpreted _field_<name>(_self), поэтому @len в requires и @len в ensures — один и тот же терм (согласованное рассуждение). Разрешено только чтение — контракт это выражение, записать поле в нём негде.

Когда такой контракт недоказан и срабатывает в runtime, сообщение о нарушении рендерит self-access читаемо — requires failed: 0 <= i && i < @len — называя реальное поле, а не плейсхолдер (Plan 140.2 / D256 §Диагностика).

Вызов non-accessor @method() (или non-#pure / mut-receiver метода) в контракте — внятная ошибка компиляции: SMT-encoder не моделирует произвольные тела методов. Ссылайтесь на поле напрямую или вынесите логику в #pure fn (Plan 140.2 / D256).

Границы как элидируемый контракт (Vec @index)

Vec[T] @index/mut @index несут requires 0 <= i && i < @len, поэтому выход v[i] за границы — нарушение контракта. Границы становятся элидируемым контрактом (D257) по той же модели enforce-with-elision, что и любой контракт:

• доказуемо in-bounds доступ компилируется без runtime-проверки (zero-cost);
• недоказанный доступ сохраняет проверку и аварийно падает на OOB (в debug и release) — без тихого UB.

Верификатор доказывает доступ in-bounds, когда индекс ограничен, например:

for i in 0 .. v.len() {
    sum = sum + v[i]          // доказано: i ∈ [0, v.len()) → проверка элидируется
    v[i] = v[i] * 2           // write-back тоже элидируется (in-place сохраняет длину)
}
ro s = v[0 .. v.len()]        // slice v[a..b]: доказано 0<=a && a<=b && b<=v.len()

fn at(v Vec[int], i int) -> int
    requires 0 <= i && i < v.len()
=> v[i]                       // cross-fn: граница берётся из `requires`

Элизия требует SMT-бэкенда (NOVA_SMT_BACKEND=z3); без него проверяется каждый доступ (safe degrade). Также нужна инвариантность длины вектора в области видимости — length-changing вызов (push/pop/…) на том же векторе сохраняет проверку (soundness). Для доступа, доказанного только через requires, проверка сохраняется под --contracts=off / #unchecked (там requires уже не enforced). @get/@first/@last возвращают Option и дают None на OOB — у них нет контракта границ.

ensures и result

Постусловие. result ссылается на возвращаемое значение функции. Несколько ensures-клаузул проверяются независимо.

#verify
fn abs_val(x int) -> int
    ensures result >= 0
    ensures result == x || result == -x
{
    if x >= 0 { x } else { -x }
}

old(...) в ensures

old(expr) захватывает значение выражения в точке входа в функцию, до выполнения тела. Полезно для контрактов с мутацией.

#verify
fn increment(mut n int) -> int
    ensures result == old(n) + 1
{
    n = n + 1
    n
}

decreases

Доказывает терминацию рекурсивных функций. Выражение должно строго убывать при каждом рекурсивном вызове. SMT-солвер проверяет это как well-foundedness obligation.

fn factorial(n int) -> int
    requires n >= 0
    decreases n
=> if n == 0 { 1 } else { n * factorial(n - 1) }

fn fib(n int) -> int
    requires n >= 0
    decreases n
=> if n < 2 { n } else { fib(n - 1) + fib(n - 2) }

Атрибуты верификации

#verify

Помечает функцию для SMT-верификации. Компилятор кодирует тело и все контракты как SMT-запрос и спрашивает солвер. Доказанные контракты элидируются (zero-cost, и в debug, и в release). Недоказанные — проверяются в runtime И в debug, И в release (enforce-with-elision; для #verify недоказуемость это compile-error, см. ниже).

#verify
fn sum_nonneg(a int, b int) -> int
    requires a >= 0
    requires b >= 0
    ensures  result >= 0
{
    a + b
}

#pure

Помечает функцию как чистую — без side effects, без эффектов в effect-row. Чистые функции можно свободно вызывать внутри контрактных выражений (requires/ensures/invariant), где вызовы с эффектами запрещены.

#pure
fn is_positive(x int) -> bool => x > 0

#verify
fn safe_log(x int) -> int
    requires is_positive(x)    // вызов #pure в контракте разрешён
    ensures  result >= 0
{
    x - 1
}

#unverified

Отказ от SMT-верификации (не от enforcement). Контракты недоказаны, поэтому проверяются в runtime И в debug, И в release (enforce-with-elision — ничего не элидируется). Используйте для контрактов, которые солвер не может обработать (нелинейная арифметика, строки и т.д.). Чтобы снять и runtime- проверку — #unchecked / --contracts=off.

#unverified
fn safe_double(x int) -> int
    requires x > 0
    ensures  result == x * 2
=> x * 2

#must_verify

Противоположность #unverified. Если SMT-солвер не может доказать контракт за отведённый таймаут — компиляция падает с ошибкой (без runtime fallback). Используйте для критичного кода.

#must_verify
fn transfer_total(from_bal int, to_bal int, amount int) -> int
    requires amount > 0 && amount <= from_bal
    ensures  result == from_bal + to_bal
{
    (from_bal - amount) + (to_bal + amount)
}

#trusted

Используется в двух контекстах:

1. with #trusted на binding handler’а — пропускает верификацию аксиом для этого handler’а, принимает контракты как аксиомы на доверии:

with #trusted Log = handler Log {
    Write(msg) { if msg > 0 { buf = msg } else { buf = 0 } }
    last() => buf
} { ... }

2. #trusted на функции с assume — подавляет предупреждение trust-introduced:

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

Композиция #pure-функций

#pure-функции свободно компонуются в контрактных выражениях. Позволяет создавать переиспользуемые предикаты:

#pure
fn in_range(x int, lo int, hi int) -> bool => x >= lo && x <= hi

#verify
fn clamp_tight(x int) -> int
    ensures in_range(result, 0, 100)
{
    if x < 0 { 0 } else if x > 100 { 100 } else { x }
}

Non-pure функция в контракте — ошибка компиляции:

error: effectful function call in contract expression
  contracts require #pure or side-effect-free expressions

Вспомогательные шаги доказательства

assert_static

Вставляет промежуточный шаг доказательства, видимый SMT-солверу. Разбивает сложный контракт на маленькие, независимо проверяемые факты. Доказано → элидируется (zero-cost, и в debug, и в release); недоказано → runtime-проверка остаётся в debug И в release (enforce-with-elision).

#verify
fn transfer(from int, to int, amount int) -> int
    requires amount > 0 && amount <= from
    ensures  result == from + to
{
    assert_static from - amount >= 0    // промежуточный факт
    (from - amount) + (to + amount)
}

assume

Инжектирует факт в SMT-контекст без доказательства. Используйте для постусловий FFI или OS-инвариантов, которые солвер не видит. Генерирует предупреждение trust-introduced вне #trusted-функции.

#trusted
fn read_positive_from_device() -> int {
    ro v = device_read()
    assume v >= 0    // задокументированная аппаратная гарантия
    v
}

calc { ... }

Структурированная цепочка равенств (или неравенств), направляющая SMT-солвер по шагам. Каждый шаг == expr; утверждает равенство с предыдущей строкой. Солвер проверяет каждый шаг независимо.

#verify
fn double_is_double(x int) -> int
    ensures result == x * 2
{
    calc {
        x * 2;
        == x * 2;
    }
    x * 2
}

Более сложные цепочки могут включать алгебраические тождества:

#verify
fn add_assoc_proof(a int, b int, c int) -> bool
    ensures result == true
{
    calc {
        (a + b) + c;
        == a + (b + c);    // ассоциативность — Z3 доказывает каждый шаг
    }
    true
}

Loop invariants

Клаузула invariant внутри тела цикла утверждает условие, которое выполняется при каждом входе в итерацию. SMT-солвер проверяет:

1. Инвариант выполняется перед циклом (инициализация).
2. Если инвариант выполняется в начале итерации и условие цикла выполняется, то инвариант выполняется в конце тела (индуктивный шаг).

// REQUIRES_SMT_BACKEND z3

#verify
fn sum_nonneg_array(n int) -> int
    requires n >= 0
    ensures  result >= 0
{
    mut sum = 0
    mut i = 0
    while i < n {
        invariant sum >= 0
        invariant i >= 0
        sum = sum + i
        i = i + 1
    }
    sum
}

Клаузула decreases также может использоваться в цикле для доказательства терминации:

#verify
fn countdown(n int) -> int
    requires n >= 0
    ensures  result == 0
{
    mut k = n
    while k > 0 {
        invariant k >= 0
        decreases k
        k = k - 1
    }
    k
}

Леммы и apply

Лемма — #verify-функция, назначение которой — установить математический факт: она существует ради своего доказательства, а не runtime-значения. Обычно возвращает bool с ensures result == true.

// REQUIRES_SMT_BACKEND z3

#verify
lemma add_comm(a int, b int) -> bool
    ensures result == true
{
    a + b == b + a
}

Оператор apply инжектирует постусловие леммы как факт в текущий SMT-контекст. Позволяет выстраивать цепочки результатов лемм:

#verify
fn use_commutativity(a int, b int) -> int
    requires a >= 0 && b >= 0
    ensures  result == b + a
{
    apply add_comm(a, b)    // инжектирует: a + b == b + a
    a + b
}

Правила:

• apply работает только внутри #verify-функций.
• Лемма должна быть уже доказана (т.е. #verify и её контракты проверены без ошибки).
• Дублирующий apply одной и той же леммы в той же области — warning W2402.

Opaque-функции и reveal

#opaque

#opaque на #pure-функции скрывает её тело от SMT-солвера. Солвер трактует её как неинтерпретированную функцию (UF): знает requires/ensures-контракты, но не реализацию.

Это предотвращает расходимость matching-loop’а в рекурсивных функциях и даёт контроль над тем, какие caller’ы получают доступ к body-level proof:

// REQUIRES_SMT_BACKEND z3

#opaque #pure
fn double(x int) -> int
    requires x >= 0
    ensures  result >= 0
=> x * 2

Без reveal caller может использовать только задекларированный ensures (result ≥ 0), но не то, что result == x * 2:

// EXPECT_COMPILE_ERROR contract violation

#verify
fn caller_no_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2    // Z3 не может доказать — тело скрыто
{
    double(n)
}

reveal fn_name

reveal fn_name инжектирует body-аксиому #opaque-функции в текущую SMT-область. После reveal солвер может использовать полное тело для доказательств в этой функции:

// REQUIRES_SMT_BACKEND z3

#verify
fn caller_with_reveal(n int) -> int
    requires n >= 0
    ensures  result == n * 2
{
    reveal double       // инжектируется body-аксиома: double(x) == x * 2
    double(n)
}

Область действия: reveal локален для функции. Другие caller’ы не затрагиваются.

Предупреждения:

• W2402 — reveal в не-#verify-функции (нет SMT-контекста).
• W2402 — дублирующий reveal для одного имени в той же области.
• W2403 — reveal для функции, которая не является #opaque.

#fuel(n)

#fuel(n) на #opaque #pure-рекурсивной функции включает N уровней разворачивания в SMT-области после reveal. Без fuel opaque body axiom — нерекурсивная. С #fuel(2) солвер получает два уровня разворачивания — достаточно для доказательства свойств маленьких конкретных входов:

// REQUIRES_SMT_BACKEND z3

#opaque #pure #fuel(2)
fn count_down(n int) -> int
    requires n >= 0
    ensures  result >= 0
=>
    if n == 0 { 0 } else { 1 + count_down(n - 1) }

#verify
fn prove_base_case() -> int
    ensures result == 0
{
    reveal count_down
    count_down(0)      // fuel разворачивает: count_down(0) == 0
}

#verify
fn prove_one_step() -> int
    ensures result == 1
{
    reveal count_down
    count_down(1)      // fuel разворачивает: 1 + count_down(0) == 1
}

Fuel chain создаёт N промежуточных UF и связывает их аксиомами по примеру подхода Dafny.

Bounded quantifiers

Nova поддерживает bounded quantifiers — forall/exists по конкретным коллекциям или индексным диапазонам. Unbounded universal quantifiers — ошибка компиляции.

// REQUIRES_SMT_BACKEND z3

#verify
fn all_nonneg_sum(a int, b int, c int) -> bool
    requires a >= 0 && b >= 0 && c >= 0
    ensures  result == true
{
    a + b + c >= 0
}

Синтаксис bounded quantifiers в контрактах:

// forall — универсальный
requires forall i in 0..xs.len() : xs[i] >= 0

// exists — экзистенциальный
ensures  exists i in 0..result.len() : result[i] == target

Коллекция после in должна быть итерируемой ([]T, range, set, map). Тело должно быть bool и #pure.

Битовые векторы и переполнение

Sized-integer типы — u8, u16, u32, u64, i8, i16, i32 — кодируются в SMT-теорию битовых векторов вместо unbounded-целых. Это даёт точную машинную семантику: арифметика переполняется по модулю (дополнительный код), битовые операции рассуждаются точно.

// REQUIRES_SMT_BACKEND z3

#verify
fn low_byte(x u32) -> u32
    ensures result <= 255 as u32
=> x & 255 as u32

Тип int остаётся unbounded математическим целым — это не битовый вектор. Используйте int для general-purpose арифметики; sized-типы — для low-level, packed, crypto или FFI-кода, где важна разрядность.

Переполнение int — это паника. Знаковая int-арифметика (+, -, *), выходящая за 64-битный диапазон, паникует в рантайме — она никогда не переполняется молча. Именно это делает верификацию int-контрактов sound: верификатор рассуждает об int как о безграничном математическом целом, и доказанный ensures result == a + b выполняется для каждого значения, которое функция реально возвращает — потому что при переполнении a + b функция паникует, а не возвращает ошибочный (обёрнутый) результат. Sized-типы вместо паники переполняются по модулю (см. выше); для них применяйте #nooverflow, когда wrap-around недопустим.

Доказуемо-безопасные overflow-чеки элидируются. Каждый int +/-/* компилируется в always-on overflow-чек (nova_int_checked_*). Когда Z3-backend доказывает, что результат остаётся в 64-битном диапазоне — из loop-bounds, литералов или requires — чек убирается (zero-cost), ровно как элидируемый bounds-чек (D272, та же модель enforce-with-elision). Loop-ограниченный i + j или requires- ограниченный a + b эмитят обычный C-оператор; недоказанная операция оставляет чек (в debug и release). Элизия только пруфом — никогда одним лишь #unchecked: чек, доказанный только через requires, остаётся под --contracts=off / #unchecked(requires). Нужен NOVA_SMT_BACKEND=z3; без него проверяется всё. * нелинеен — Z3 может оставить чек.

Битовые операторы &, |, ^, <<, >> доступны в контрактах для sized-integer операндов (на int они по-прежнему не поддерживаются).

Знаковость. Беззнаковые типы (u8/u16/u32/u64) и знаковые (i8/i16/i32) различаются в сравнении, делении, остатке и сдвиге вправо. Верификатор выбирает правильный оператор по типу параметра: сравнения i32 знаковые (-1 < 0 истинно), сравнения u32 беззнаковые (0xFFFFFFFF > 0). Знаковое деление округляет к нулю; >> для знакового значения — арифметический сдвиг.

Касты между sized-типами. x as u32 переразрядивает битовый вектор: более широкая цель zero-extend’ит беззнаковый источник и sign-extend’ит знаковый; более узкая — отбрасывает старшие биты. Например (b as u32) где b : u8 всегда <= 255, а (x as u8) оставляет только младший байт.

#nooverflow

По умолчанию арифметика sized-целых переполняется молча. Атрибут #nooverflow заставляет верификатор генерировать дополнительное proof-обязательство для каждого +, -, * в теле функции: операция не должна переполнять тип. Недоказуемое обязательство — ошибка компиляции.

// REQUIRES_SMT_BACKEND z3

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

Здесь предусловие ограничивает a и b, так что их сумма не превысит 2^32 - 1 — обязательство переполнения доказано. Без ограничивающего requires a + b могло бы переполниться и #nooverflow отвергнет функцию на этапе компиляции.

#nooverflow требует SMT-бэкенд с поддержкой битовых векторов (REQUIRES_SMT_BACKEND z3); тривиальный бэкенд сообщает теорию битовых векторов как неподдерживаемую.

Доверенные внешние функции

external fn с контрактами требует #trusted. Контракты регистрируются как аксиомы — caller’ы получают ensures как предположения без доказательства. Компилятор не верифицирует тело (Nova-тела нет).

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

#verify
fn use_strlen(s str) -> int
    requires s.is_valid_cstring()
    ensures  result >= 0
{
    libc_strlen(s)    // ensures из #trusted-аксиомы инжектируется
}

Выбор SMT-бэкенда

Nova имеет два бэкенда верификации:

Тесты, требующие Z3, используют маркер // REQUIRES_SMT_BACKEND z3 — test runner пропускает их при отсутствии Z3.

Таймаут на функцию: по умолчанию 2 секунды. Переопределить локально:

#verify_timeout(10000)
#verify
fn complex_proof(x int) -> int
    ...

Cross-check верификация (Z3 ↔ CVC5)

Cross-check — это CI-only защитная сеть для soundness: каждая verification condition прогоняется через два независимых пути решателя, и при расхождении их определённых ответов сборка падает. Это вторая линия защиты после soundness-regression-suite (Plan 33.8 Ф.7): regression-suite ловит известные классы багов, cross-check — неизвестные.

Два пути намеренно независимы:

• Z3 — через FFI-backend.
• CVC5 — через текстовый SMT-LIB v2 скрипт, скармливаемый бинарнику cvc5 подпроцессом.

Текстовый путь не разделяет код с Z3-FFI-трансляцией, поэтому он ещё и второй независимый кодировщик. Баг кодирования, молча терявший формулу на стороне Z3 (класс багов из Plan 33.8 Ф.6.2), был бы пойман здесь даже без второго решателя.

Как запустить

# Соберите с Z3-backend, поставьте cvc5 в PATH (либо укажите NOVA_CVC5
# на бинарник), затем:
NOVA_CROSSCHECK=1 nova test . --filter contracts

NOVA_CROSSCHECK=1 имеет приоритет над NOVA_SMT_BACKEND. Обычная компиляция (nova build / nova check) не затрагивается — она использует один решатель, время компиляции разработчика не растёт.

Если cvc5 не найден, прогон gracefully вырождается в «только Z3» с warning’ом — cross-check просто не происходит, сборка не ломается.

Что считается расхождением

Gate срабатывает только на definite-расхождении: один путь сказал Proven (unsat), другой — Disproved (sat). Любой Unknown / timeout с любой стороны — норма (у решателей разные перф-профили), не ошибка.

Расхождение сообщается как ошибка компиляции E2412 с функцией, VC, обоими вердиктами, контрпримером и SMT-LIB-скриптом для ручного воспроизведения. Это soundness-критично: один из путей дал неверный ответ, значит верификатор мог объявить ложный Proven.

CI-gate

Workflow contracts-crosscheck прогоняет весь корпус контрактов под NOVA_CROSSCHECK=1 и требует 0 расхождений для merge. NOVA_CROSSCHECK_LOG=<файл> заставляет каждое расхождение дописывать строку в этот файл (корпус компилируется процесс-на-файл, поэтому файл — точка межпроцессной агрегации, которую проверяет gate).

Грамматика контрактов

contract-clause  = requires-clause
                 | ensures-clause
                 | decreases-clause

requires-clause  = 'requires' bool-expr
ensures-clause   = 'ensures'  bool-expr
decreases-clause = 'decreases' expr

fn-contracts     = contract-clause*

loop-invariant   = 'invariant' bool-expr
loop-decreases   = 'decreases' expr

calc-block       = 'calc' '{' calc-step+ '}'
calc-step        = expr ';'
               | ('==' | '<=' | '>=' | '<' | '>') expr ';'

reveal-stmt      = 'reveal' ident
apply-stmt       = 'apply' ident '(' expr-list ')'
assert-static    = 'assert_static' bool-expr
assume-stmt      = 'assume' bool-expr

quantifier-expr  = 'forall' ident 'in' expr ':' bool-expr
                 | 'exists' ident 'in' expr ':' bool-expr

old-expr         = 'old' '(' expr ')'
result-ref       = 'result'                  // только в ensures

Сводка атрибутов:

Справочник ошибок

Bootstrap-ограничения

Связанные документы

• spec/decisions/09-tooling.md — D24 / D89 / D111 / D112 / D113 / D114 / D116 (контракты, SMT, test tooling)
• spec/decisions/04-effects.md — D120 (#pure views + axioms), D115 (axiom binders)
• docs/plans/33.9-opaque-reveal-fuel.md — реализация #opaque / reveal / #fuel(n) (Plan 33.9)
• docs/plans/33.14-z3-cvc5-crosscheck.md — реализация Z3 ↔ CVC5 cross-check (Plan 33.14)
• nova_tests/contracts/ — ~280 тестов верификации контрактов
• nova_tests/doc/f23_contracts_positive.nv — базовый doc-пример контрактов
• nova_tests/doc/f24_infer_contracts_positive.nv — doc-пример инферированных контрактов
• nova_tests/doc/f25_mutation_contracts_positive.nv — doc-пример контрактов с мутацией
• nova_tests/expected_runtime/ — тесты нарушений контракта в runtime (contracts_*.nv)