Вы построили n-версионную систему. Три независимые реализации одной и той же критической функции, voter, который выбирает результат большинства, и приятное ощущение, что вы перехитрили единые точки отказа.

Вы не доказали, что функции эквивалентны. Вы доказали только то, что они компилируются.

Почему эквивалентность — скрытый фундамент n-версионного программирования

N-версионное программирование — это идея о том, что если в одной реализации есть баг, то в остальных, скорее всего, его нет, поэтому voter может отбросить выбросы. Это предполагает, что выходы сравнимы.

Если функция A возвращает float, а функция B возвращает string, у voter нет никакой почвы под ногами. Но даже при совпадающих типах семантические различия убивают вас. Одна сортирует по возрастанию, другая — по убыванию. Одна округляет половину вверх, другая — до ближайшего чётного. Voter видит три разных ответа и не имеет принципиального способа выбрать.

В литературе по n-версионному программированию полно исследований, показывающих, что независимо написанные программы часто падают коррелированным образом. Программисты совершают одни и те же ошибки. Они неправильно понимают одни и те же двусмысленные спецификации. Если ваша спецификация звучит как «отсортируй этот список», и один программист реализует quicksort, а другой — mergesort, вы можете предположить, что они эквивалентны. Они эквивалентны, пока вы не спросите про stability. Или пока входные данные не содержат NaN.

Большинство команд пропускают проверку эквивалентности, потому что это кажется лишней работой. Это не так. Это работа, которая придаёт смысл всей остальной системе.

Почему ваш набор тестов даёт вам ложную уверенность

Вы пишете unit-тесты. Обе функции проходят. Вы объявляете победу.

Это категориальная ошибка. Тесты могут доказать наличие багов, но никогда — их отсутствие. При бесконечных пространствах входных данных, или даже просто при больших конечных, ваше покрытие тестами — это погрешность округления. Две функции могут согласовываться в каждом случае, который вы придумали, и расходиться в том, который имеет значение в продакшене в три часа ночи.

Я усвоил это на собственном горьком опыте в проекте с двумя JSON-парсерами. Один использовал встроенный json.loads Python, другой — самописный парсер ради производительности. У нашего набора тестов было пятьдесят кейсов. Оба прошли. В продакшене клиент прислал JSON-объект с дублирующимся ключом. Парсер Python оставил последнее значение. Наш самописный парсер оставил первое. Voter увидел два разных объекта и запаниковал.

Property-based testing подходит ближе. Вместо ручного подбора входных данных вы описываете свойства, которым должны удовлетворять обе функции, и позволяете генератору искать контрпримеры. Вот реальный пример с использованием библиотеки Hypothesis для Python:

from hypothesis import given, strategies as st
import math

def round_half_up(n):
    return math.floor(n + 0.5)

@given(st.floats(allow_nan=False, allow_infinity=False))
def test_rounding_equivalence(n):
    assert round_half_up(n) == round(n)

if __name__ == "__main__":
    test_rounding_equivalence()

Запустите это, и Hypothesis быстро найдёт контрпример. round_half_up(2.5) возвращает 3. Встроенный round(2.5) Python возвращает 2, потому что использует banker’s rounding, который округляет до ближайшего чётного числа. Обе функции «корректны» по некоторому стандарту. Они не эквивалентны.

Property-based testing не докажет эквивалентность. Он найдёт краевые случаи, которые пропустили ваши unit-тесты. Это ценно, но это всё ещё фальсификация, а не верификация.

Как SMT-солверы могут реально доказать эквивалентность

Если вы хотите доказательства, вам нужно покинуть зону комфорта тестирования и войти в мир SMT-солверов. Идея проста. Закодируйте обе функции как логические формулы и спросите солвер, существует ли вход, на котором они различаются.

Для ограниченных доменов это механический процесс. Вот пример с использованием Z3 для доказательства эквивалентности двух реализаций max для целых чисел:

from z3 import Int, Solver, If, Abs

x = Int('x')
y = Int('y')

# Standard max implementation
max_standard = If(x > y, x, y)

# Algebraic max: (x + y + abs(x - y)) / 2
max_algebraic = (x + y + Abs(x - y)) / 2

solver = Solver()
solver.add(max_standard != max_algebraic)
result = solver.check()
print(result)  # unsat

Z3 возвращает unsat, то есть контрпримера не существует. Функции эквивалентны для всех целых чисел в модели Z3. Это настоящее доказательство, ограниченное теорией, в рамках которой рассуждает Z3.

Это можно сделать и для более сложных функций. Хитрость в том, чтобы выразить ваши функции как логические формулы. Для циклов вы их разворачиваете. Для массивов используете теорию массивов Z3. Для floating point — FP-теорию Z3 и принимаете тот факт, что солвер может зависнуть на сложных выражениях.

Пропасть между «механическим» и «лёгким» — это то место, где застревают большинство команд. Перевод функции Python в язык Z3 требует понимания обоих. Но как только перевод готов, солвер делает всю тяжёлую работу.

Таблица компромиссов, которую никто не хочет публиковать

Полная формальная верификация, доказывающая эквивалентность для всех возможных входов, включая каждый краевой случай IEEE 754, возможна. Люди делают это для криптографических примитивов и авионических систем. Это стоит недель или месяцев работы экспертов и требует инструментов вроде Coq или Isabelle.

Property-based testing стоит минут и ловит реальные баги, но не даёт гарантий.

Ограниченная верификация с помощью SMT-солверов находится посередине. Она даёт гарантию для чётко определённой области. Эта область может покрывать 99.9% ваших продакшен-входов. Достаточно ли этого — зависит от того, чего стоит отказ.

Бесплатных обедов не бывает. Выбирайте инструмент, который соответствует вашей толерантности к риску и экспертизе команды.

Voter, который знает, когда сдаться

Большинство n-версионных систем реализуют наивный majority voter: вернуть наиболее частый результат или упасть, если большинства нет. Более умный voter знает о собственном невежестве.

from collections import Counter

def naive_voter(results):
    if not results:
        raise ValueError("No results to vote on")
    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner
    raise ValueError("No majority found")

def informed_voter(results, input_sample=None):
    if not results:
        raise ValueError("No results to vote on")

    distinct = set(results)
    if len(distinct) == 1:
        return results[0]

    # Log disagreement for later analysis
    if input_sample is not None:
        print(f"Disagreement on input {input_sample}: {distinct}")

    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner

    raise ValueError("No majority found")

Когда voter видит постоянное несогласие на определённых классах входных данных, это сигнал. Либо ваше предположение об эквивалентности неверно, либо вы нашли баг в одной из реализаций. Оба варианта стоит знать.

Voter нужен не только для того, чтобы выбирать победителей. Он нужен для того, чтобы сообщать вам, когда ваши предположения об эквивалентности были неверны.

Что реально делать дальше

Начните с property-based testing. Это дёшево, это находит баги, и это заставляет вас сформулировать, что означает «эквивалентность» в вашей предметной области. Это побитово идентичные выходы? Выходы в пределах какого-то epsilon? Выходы, удовлетворяющие одному и тому же постусловию?

Как только вы точно определили эквивалентность, переходите к ограниченной верификации, если домен конечен и ставки высоки. Используйте Z3, CBMC или похожий инструмент, чтобы получить механическое доказательство для вашей ограниченной области.

Резервируйте полную формальную верификацию для тех частей, где баг буквально убивает людей. Для всего остального знайте пределы вашего доказательства и отслеживайте расхождения в продакшене. Лучшая n-версионная система — та, которая знает, чего она не знает.