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

Система контрактов Nova позволяет описать, что функция требует и гарантирует, и проверяет эти утверждения на этапе компиляции через SMT-солвер. Доказанные контракты стираются в release-сборке — нулевая цена в runtime. Недоказанные откатываются до runtime-assert'а в debug.

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

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-запрос и спрашивает солвер. Если солвер доказал контракты — они стираются в release. Если нет — warning W2402 + runtime fallback в debug.

#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-верификации. Контракты остаются как runtime-assert'ы в debug; в release пропускаются. Используйте для контрактов, которые солвер не может обработать (нелинейная арифметика, строки и т.д.).

#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 {
    let 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-солверу. Разбивает сложный контракт на маленькие, независимо проверяемые факты. В debug — runtime check; в release — стирается после доказательства.

#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 {
    let 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
{
    let mut sum = 0
    let 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
{
    let 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.

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

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-бэкенда

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

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

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

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

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)
• 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)