Трохи балачок про assert-и: еволюція підходів від C до залежних типів

Які бувають assert-и

function Find_Max (A : My_Array_Type) return Integer with
  Pre  => A'Length > 0,
  Post => (for all J in A'Range => Find_Max'Result >= A(J)) and
          (for some J in A'Range => Find_Max'Result = A(J));

class sorted_pair
feature
  first, second: integer

  set(a, b: integer)
    local
      temp: integer
    do
      first := a
      second := b
      -- тут інваріант може бути порушено!
      if first > second then
        temp := first
        first := second
        second := temp
      end
    end

invariant
  first <= second
end

З поведінкою assert-ів під час розробки все більш-менш зрозуміло. Їхня головна мета полягає в допомозі нам, розробникам. Коли твердження хибне, програма має негайно зупинитися і надати максимум інформації (файл, рядок, умова, стек), щоб розробник швидко зрозумів, що пішло не так. Це вірний помічник, який б’є на сполох при перших ознаках проблеми.

Але що робити, коли код потрапляє у прод? Коли «ситуація, якої ніколи не мало статися» раптом трапляється на бойовому сервері? Ось тут і з’являється вибір. Подивимося, які основні варіанти існують.

Найперший і, мабуть, найпростіший підхід полягає в тому, щоб у релізній версії коду просто вимикати всі перевірки. Багато мов програмування, як от C++, роблять це за замовчуванням. Логіка тут проста: assert-и потрібні для розробки, а в продакшені вони лише сповільнюють роботу. Колись, за часів динозаврів та повільних процесорів, це був вагомий аргумент. Сьогодні ж це вже звучить не так переконливо.

Що відбувається, коли такий assert спрацював би, але його немає? Програма опиняється в стані, на який вона не була розрахована. Це дуже слизька доріжка, що веде прямісінько до горезвісного «Undefined Behavior» (UB). Програма може мовчки видавати неправильні результати, пошкодити дані або впасти значно пізніше, коли знайти причину буде майже неможливо.

Але чи завжди це погано? Іноді дивна поведінка краща за падіння. Уявіть собі комп’ютерну гру. Нехай буде стара добра Jagged Alliance 2. Там характеристики персонажів були в діапазоні від 0 до 100. Але через різні бонуси та модифікатори непомітність бійця могла перевищити 127. Це призводило до переповнення char, і наш ніндзя раптом ставав помітніше за стадо буйволів. Це смішно, це баг, але це краще, ніж якби гра просто вилетіла наприкінці довгої битви, яку ви не зберегли. Інколи краще глюк на екрані, ніж повна зупинка програми. Користувач може не помітити дивну поведінку, але креш помітять усі. До того ж наш світ без глітчей та спідранів був би трошечки сумнішим.

Повною протилежністю ігноруванню буде нещадне падіння програми як тільки так відразу. Це своєрідна філософія, яку активно сповідує Rust. Тут логіка така: якщо ми дійшли до стану, який неможливий за нашими припущеннями, це означає, що програма знаходиться в некоректному стані. Продовження роботи в такому стані може призвести до непередбачуваних наслідків, тобто того самого «Undefined Behavior». Краще вже впасти відразу, ніж потім ламати голову над причинами дивних помилок.

Саме це і сталося 19 листопада 2024 року з Cloudflare. Assert спрацював, демон впав, а з ним і 2+ мільйони сайтів. Технічно все правильно: система виявила невалідний стан і зупинилася замість того, щоб ризикувати. Але для кінцевого користувача це нагадує сумний анекдот: «Чи потів хворий перед смертю?». З точки зору користувача результат той самий: програма не працює.

Між двома крайнощами — ігноруванням і падінням — існує ціла низка проміжних варіантів. Замість класичного assert, який або зникає, або все валить, ми можемо «підкласти» під помилкову ситуацію якусь іншу логіку. Часто, ще з часів Delphi, це реалізується через механізм винятків (exceptions). Інколи можна побачити й кастомні макроси на кшталт ASSERT_WITH_CODE, що виконують певний код при спрацьовуванні. По суті це можна розглядати як визнання того, що assert-и на проді є небажаними, і будь-яку потенційну помилку краще обробляти явно.

На перший погляд це може здатися ідеальною «золотою серединою». Програма не падає, а продовжує роботу, намагаючись коректно відреагувати на несподівану ситуацію. Проте тут криються свої підводні камені. Нам доводиться писати обробники помилок для ситуацій, які, за нашими припущеннями, ніколи не мають виникнути. Такий код часто буває важко протестувати. Щоб досягти 100% покриття тестами, доводиться вигадувати складні «моки» на assert-и або йти на інші хитрощі. Іноді при помилці потрібно нетривіально відкотити всі зміни, що вже були зроблені.

І найгірше — психологічний момент. Коли ти пишеш обробник для assert-а, у тебе є чітке відчуття, що займаєшся марною справою, адже ти обробляєш ситуацію, якої, за всією логікою, взагалі не може бути. Це може трохи демотивувати.

Зазвичай у таких сценаріях ми зазвичай якось логуємо випадок, «прокидаємо» помилку нагору по стеку, щоб її обробив вищий рівень програми. Але буває й так, що помилка просто не вписується в бізнес-логіку. Наприклад, при авторизації користувача нам потрібна бінарна відповідь: «дозволено» або «не дозволено». Будь-яка відповідь при помилці буде поганою. Якщо ми відповімо «ні», для користувача це виглядає як непрацююча система. Якщо ми відповімо «так», то це ще гірше: система не працює з точки зору безпеки.

Здається, ми перебрали основні варіанти поведінки: ігнорувати, падати або намагатися обробити помилку. Лишилося обрати, що буде краще працювати в конкретному випадку, залежно від конкретної задачі та філософії проєкту, та змиритися з компромісами. Але існує ще один, зовсім інший шлях: можна довести, що assert ніколи не спрацює!

Цей підхід звучить як щось із наукової фантастики, але він цілком реальний. Ідея полягає в тому, щоб не думати, що станеться, коли assert спрацює, а математично довести, що він не спрацює ніколи. В такому разі перевірка під час виконання стає зайвою, адже ми маємо залізну гарантію її істинності.

Це, так би мовити, святий Грааль надійності. Щобільше, тут є навіть кілька способів досягти цієї мети, які активно використовуються в критичних системах.

Один зі способів це делегування роботи спеціальним інструментам, які називаються SMT-солверами (Satisfiability Modulo Theories). Якщо простими словами, то це така розумна програма, яка вміє автоматично доводити або спростовувати математичні твердження. Яскравий приклад реалізації цього підходу — мова Ada разом з інструментом SPARK.

Пам’ятаєте приклад коду на Ada з pre- та post-умовами для функції Find_Max? SPARK працює так: він «згодовує» SMT-солверу всі pre-умови вашої функції як початкові факти. Потім він аналізує код рядок за рядком, додаючи нові факти. Наприклад, якщо у вас є факт, що X > 5, а в коді написано Y := X + 1, то солвер робить висновок, що Y > 6. Коли SPARK зустрічає assert(Y > 0), він намагається довести його істинність на основі вже відомих фактів. Якщо йому це вдається, перевірка вважається математично доведеною, тож її можна сміливо викинути з рантайму.

Звучить круто, правда? Але є нюанси. По-перше, SMT-солвер не всесильний. Існує цілий клас задач, які він не може довести автоматично. По-друге, щоб допомогти солверу, програмісту часто доводиться додавати проміжні assert-и, які підказують правильний хід думок. SMT-солвер не впорався? Додамо ще assert. Ще раз не впорався? Ще assert. Ще раз? Треба думати...

Це вимагає від розробника не тільки навичок програмування, а й специфічного математичного мислення та розуміння того, як працює солвер під капотом, та якого факту йому не вистачає для повного доказу. Тож це досить потужний інструмент, але складний. Точно не чарівна паличка.

Якщо SMT-солвери це складно, то тримайтеся, бо ми переходимо до важкої артилерії. Це мови програмування із залежними типами, такі як Idris, Agda або Coq. Вони інтегрують математичні докази безпосередньо в систему типів.

У звичайній мові ми можемо написати тип «масив цілих чисел». У мові з залежними типами можна написати «масив з рівно 10 цілих чисел». В C++ теж так можна! Але йдемо далі, «масив довжиною N», де N це змінна або параметр функції. Або навіть «відсортований масив цілих чисел».

Тип стає математичним твердженням, це всім відомий ізоморфізм Карі-Говарда. Програма містить докази цих тверджень. Якщо компілятор прийняв код, значить, доказ коректний.

Звісно, є «невеличкий» нюанс: цей доказ доведеться побудувати власноруч. Якщо SMT-солвер робить докази автоматично: ви пишете код, він намагається довести, то тут усе навпаки: ви маєте побудувати доказ власноруч. Компілятор лише перевіряє, чи доказ коректний.

І це, м’яко кажучи, непросто. Це вимагає від програміста бути не просто інженером, а ще й трішки математиком. А це, погодьтеся, досить рідкісний і високооплачуваний скіл.

Якщо ви заінтриговані, як це може виглядати в коді, читайте наступний розділ. Якщо ні — мотайте до висновків про Cloudflare, там все зібрано докупи.

Давайте подивимося на невеличкий приклад мовою Agda. Припустимо, ми хочемо написати функцію, яка бере два непорожні масиви (вектори в C++ або списки в Python), з’єднує їх і повертає другий елемент результату.

-- Takes two non-empty vectors and returns the second element of their concatenation
second : {A : Set} {n m : ℕ} → 𝕍 A (suc n) → 𝕍 A (suc m) → A
second {A} {n} {m} vec1 vec2 =
  let one = suc zero
      concatenated : 𝕍 A (suc n + suc m)
      concatenated = vec1 ++ vec2
      -- Proof that index 1 is in bounds
      index-proof : one < suc n + suc m
      index-proof = 1<suc-n+suc-m
  in nth concatenated one index-proof

Що ми бачимо? Функція second приймає аж п’ять аргументів. Перші три — {A : Set} {n m : ℕ} — записані у фігурних дужках. Це неявні аргументи, такі собі параметри за замовчуванням. Тільки на відміну від більшості мов програмування, їх значення не задає програміст, а виводить компілятор.

A — це аргумент типу Set, який містить типи. Для педантів поясню, що Set містить типи першого порядку, бо тип усіх типів призводить до парадоксу Расела. Тобто A задає тип елементів масиву (чи то числа, чи рядки, чи щось інше).

n та m — це натуральні числа, довжини масивів, точніше, довжина мінус один, бо реальна довжина suc n та suc m.

А далі — це два аргументи, які нам треба задавати явно. Перший — 𝕍 A (suc n) — масив довжини n + 1. Другий — 𝕍 A (suc m) — масив довжини m + 1. Тут suc це наступне натуральне число. Оскільки n та m — це натуральні числа (можуть бути нулем), то довжини масивів щонайменше 1. А значить обидва масиви не можуть бути порожніми, бо мінімальна довжина завжди 1. Компілятор не дозволить передати порожній масив — це буде помилка типу.

Коли ви викликаєте second vec1 vec2, компілятор дивиться на типи vec1 та vec2 і сам розуміє: Ага, A — це тип Int (вбудований тип для цілих, не плутайте з ℕ — математичним типом натуральних чисел, які існують на етапі компіляції), n = 5, m = 3. Схоже на generics у Java або templates у C++, тільки набагато потужніше.

Тіло функції second це дві дії: конкатенація масивів (нічого перевіряти, завжди можемо виконати) та отримання другого елемента, який має індекс 1. Для цього ми викликаємо функцію nth, і тут найцікавіше:

nth : {A : Set} {n : ℕ} → 𝕍 A n → (i : ℕ) → i < n → A
nth []       i       ()
nth (x ∷ xs) zero    (z<s)     = x
nth (x ∷ xs) (suc i) (s<s i<n) = nth xs i i<n

Ще раз, подумаймо про індекси. Щоб взяти другий елемент, нам треба передати доказ, що довжина масиву більше одиниці. Перший масив має довжину n+1, другий — m+1, конкатенація має довжину n+m+2. Інтуїтивно очевидно, що довжина масиву concatenated більше одиниці. Але... Agda потребує формальний доказ цього факту! Ми приведемо тут його, щоб трошечки залякати читача:

subst : {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

+-suc : (n m : ℕ) → n + suc m ≡ suc (n + m)
+-suc zero    m = refl
+-suc (suc n) m = subst (λ k → suc n + suc m ≡ suc k) (+-suc n m) refl

1<suc-n+suc-m : {n m : ℕ} → suc zero < suc n + suc m
1<suc-n+suc-m {n} {m} = s<s (subst (λ k → zero < k) (sym (+-suc n m)) z<s)

В нашу задачу не входить розбирати покроково, як саме побудовано ці докази, бо це окрема велика тема. Головне: якщо доказ неправильний — код не скомпілюється. Якщо доказ правильний, то функції nth та second гарантовано не можуть впасти з помилкою «індекс за межами масиву». Система типів мови виключає цю помилку.

Підсумки: повертаємося до Cloudflare