n版システムを構築した。同じクリティカルな関数を3つの独立した実装で用意し、多数決で結果を選ぶvoterを置き、単一障害点を凌駕したという満足感に浸っている。

だが、あなたは関数が等価であることを証明していない。コンパイルが通ることを証明したにすぎない。

なぜ等価性がn-version programmingの隠れた基盤なのか

n-version programmingとは、1つの実装にバグがあっても他の実装にはおそらくないだろう、という発想である。したがってvoterが外れ値を破棄できる。この前提が成り立つのは、出力が比較可能である場合に限られる。

関数Aがfloatを返し、関数Bがstringを返せば、voterは判断の根拠を失う。しかし型が一致していても、意味上の差異が致命的になる。1つは昇順にソートし、もう1つは降順にソートしている。1つはhalf upで丸め、もう1つは偶数への丸め（banker’s rounding）をしている。voterは3つの異なる答えを目にし、原理的にどれを選べばよいかわからない。

n-version programmingに関する文献には、独立に書かれたプログラムが相関した形で失敗するという研究が多数ある。プログラマは同じミスを犯す。同じ曖昧な仕様を誤読する。仕様が「このリストをソートせよ」で、1人がquicksort、もう1人がmergesortを実装したとして、等価だと思うかもしれない。安定性について問われるまでは、そうだ。あるいは入力にNaNが含まれるまでは。

ほとんどのチームは等価性検査を飛ばす。余分な作業のように感じるからだ。だが、それは余分な作業ではない。システム全体に意味を与える作業なのだ。

なぜテストスイートが虚栄心を与えているのか

ユニットテストを書く。両方の関数が通過する。勝利を宣言する。

これはカテゴリーミスだ。テストはバグの存在を証明できるが、その不在は証明できない。無限の入力空間がある場合、あるいは有限だとしても十分に大きい場合、テストカバレッジは丸め誤差に過ぎない。2つの関数は、あなたが思いついたすべてのケースで一致し、深夜3時の本番環境で意味を持つ1つのケースで分岐するかもしれない。

2つのJSONパーサーを扱ったプロジェクトで、私は身をもって学んだ。1つはPythonの組み込み json.loads を使い、もう1つはパフォーマンスのために手作りのパーサーだった。テストスイートには50ケースあった。両方通過した。本番では、顧客が重複キーを持つJSONオブジェクトを送信した。Pythonのパーサーは最後の値を保持した。手作りのパーサーは最初の値を保持した。voterは2つの異なるオブジェクトを目にし、パニックになった。

property-based testingは、もう少し近づく。入力を手で選ぶのではなく、両方の関数が満たすべき性質を記述し、ジェネレーターに反例を探させる。以下はPythonのHypothesisライブラリを使った実例だ：

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 を返す。Pythonの組み込み round(2.5) は 2 を返す。banker’s roundingを使い、最も近い偶数へ丸めるからだ。両方の関数は、ある基準では「正しい」。だが等価ではない。

property-based testingは等価性を証明しない。ユニットテストが見逃したエッジケースを見つける。それは価値があるが、それでも偽証であり、検証ではない。

SMT solverがいかにして実際に等価性を証明できるのか

証明が欲しければ、テストの快適ゾーンを離れ、SMT solverの世界に入る必要がある。考え方は単純だ。両方の関数を論理式として符号化し、それらが異なる入力が存在するかどうかをsolverに問う。

有界ドメインでは、これは機械的である。以下はZ3を使って、2つの整数 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が推論している理論内で有界されている。

より複雑な関数に対してもこれができる。コツは、関数を論理式として表現することだ。forループはアンロールする。配列にはZ3の配列理論を使う。浮動小数点にはZ3のFP理論を使い、複雑な式でsolverがタイムアウトする可能性を受け入れる。

「機械的」と「簡単」の間のギャップが、ほとんどのチームが行き詰まる場所だ。Pythonの関数をZ3の言語に翻訳するには、両方を理解する必要がある。だが一度翻訳ができれば、solverが難しい仕事を引き受ける。

誰も公表したがらないトレードオフ表

すべての可能な入力、あらゆるIEEE 754のエッジケースを含めて等価性を証明する完全な形式的検証は、可能だ。暗号プリミティブや航空電子システムのために人々はそれを行う。数週間から数ヶ月の専門家の時間を要し、CoqやIsabelleのようなツールが必要だ。

property-based testingは数分でコストがかかり、実際のバグを捕まえるが、保証は何も与えない。

SMT solverによる有界検証は、その中間に位置する。明確に定義された範囲について保証を与える。その範囲は、本番入力の99.9%をカバーするかもしれない。それが十分かどうかは、失敗のコストがどれだけ大きいかに依存する。

タダのランチはない。リスク許容度とチームの専門知識に合ったツールを選べ。

諦めるべき時を知るvoter

ほとんどのn-versionシステムは、単純な多数決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が特定の入力クラスで持続的な不一致を検出したとき、それはシグナルだ。等価性の仮定が間違っているか、あるいは1つの実装にバグがあるかのどちらかだ。いずれにせよ、知る価値がある。

voterは勝者を選ぶためだけにあるのではない。等価性に関するあなたの仮定が間違っていた時に教えてくれるためにあるのだ。

次に実際にやるべきこと

property-based testingから始めよ。安価だ。バグを見つける。そして、あなたのドメインにおいて「等価性」が何を意味するかを明確にすることを強制する。ビットレベルで同一の出力か？あるイプシロン内の出力か？同じ事後条件を満たす出力か？

等価性を正確に定義できたら、ドメインが有限でステークスが高い場合は有界検証へ移れ。Z3、CBMC、あるいは類似のツールを使い、有界な範囲で機械的な証明を得よ。

完全な形式的検証は、バグが文字通り人を殺す部分にだけ留めよ。それ以外のすべてについては、証明の限界を知り、本番環境で不一致を監視せよ。最良のn-versionシステムとは、自分が何を知らないかを自覚しているシステムである。