Vous avez construit un système N-version. Trois implémentations indépendantes de la même fonction critique, un votant qui choisit le résultat majoritaire, et une agréable sensation d’avoir déjoué les points de défaillance uniques.

Vous n’avez pas prouvé que les fonctions sont équivalentes. Vous avez seulement prouvé qu’elles compilent.

Pourquoi l’équivalence est le fondement caché de la programmation N-version

La programmation N-version repose sur l’idée que si une implémentation contient un bug, les autres n’en auront probablement pas, donc un votant peut écarter les valeurs aberrantes. Cela suppose que les sorties sont comparables.

Si la fonction A renvoie un float et la fonction B renvoie une string, le votant n’a aucun pied sur lequel se tenir. Mais même avec des types correspondants, des différences sémantiques vous tuent. L’une trie par ordre croissant, l’autre par ordre décroissant. L’une arrondit à la demi supérieure, l’autre arrondit à la demi paire. Le votant voit trois réponses différentes et n’a aucun moyen fondé pour choisir.

La littérature sur la programmation N-version regorge d’études montrant que des programmes écrits indépendamment échouent souvent de manière corrélée. Les programmeurs font les mêmes erreurs. Ils lisent de travers les mêmes spécifications ambiguës. Si votre spécification est « trier cette liste », et qu’un programmeur implémente un quicksort tandis qu’un autre implémente un mergesort, vous pourriez supposer qu’ils sont équivalents. Ils le sont, jusqu’à ce que vous posiez la question de la stabilité. Ou jusqu’à ce que l’entrée contienne un NaN.

La plupart des équipes passent la vérification d’équivalence parce que ça ressemble à du travail supplémentaire. Ce n’en est pas. C’est le travail qui rend le reste du système significatif.

Pourquoi votre suite de tests vous donne une fausse confiance

Vous écrivez des tests unitaires. Les deux fonctions passent. Vous déclarez victoire.

C’est une erreur de catégorie. Les tests peuvent prouver la présence de bugs, jamais leur absence. Avec des espaces d’entrée infinis, ou même juste des grands espaces finis, votre couverture de test est une erreur d’arrondi. Deux fonctions peuvent être d’accord sur chaque cas auquel vous avez pensé et diverger sur celui qui compte à 3h du matin en production.

J’ai appris cela à mes dépens sur un projet avec deux parsers JSON. L’un utilisait le json.loads intégré de Python, l’autre utilisait un parser fait maison pour des raisons de performance. Notre suite de tests avait cinquante cas. Les deux passaient. En production, un client a envoyé un objet JSON avec une clé dupliquée. Le parser de Python gardait la dernière valeur. Notre parser fait maison gardait la première. Le votant a vu deux objets différents et a paniqué.

Le property-based testing s’en rapproche davantage. Au lieu de choisir des entrées à la main, vous décrivez les propriétés que les deux fonctions doivent satisfaire et vous laissez un générateur chasser les contre-exemples. Voici un vrai exemple utilisant la bibliothèque Hypothesis de 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()

Exécutez ceci et Hypothesis trouvera rapidement un contre-exemple. round_half_up(2.5) renvoie 3. Le round(2.5) intégré de Python renvoie 2 car il utilise l’arrondi du banquier, qui arrondit au nombre pair le plus proche. Les deux fonctions sont « correctes » selon un certain standard. Elles ne sont pas équivalentes.

Le property-based testing ne prouvera pas l’équivalence. Il trouvera les cas limites que vos tests unitaires ont manqués. C’est précieux, mais c’est toujours de la falsification, pas de la vérification.

Comment les solveurs SMT peuvent réellement prouver l’équivalence

Si vous voulez une preuve, vous devez quitter la zone de confort des tests et entrer dans le monde des solveurs SMT. L’idée est simple. Encodez les deux fonctions comme des formules logiques et demandez au solveur si une entrée existe où elles diffèrent.

Pour des domaines bornés, c’est mécanique. Voici un exemple utilisant Z3 pour prouver que deux implémentations de max sur des entiers sont équivalentes :

from z3 import Int, Solver, If, Abs

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

# Implémentation max standard
max_standard = If(x > y, x, y)

# Max algébrique : (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 renvoie unsat, ce qui signifie qu’aucun contre-exemple n’existe. Les fonctions sont équivalentes pour tous les entiers dans le modèle de Z3. C’est une vraie preuve, bornée à la théorie dans laquelle Z3 raisonne.

Vous pouvez faire cela pour des fonctions plus complexes aussi. L’astuce est d’exprimer vos fonctions comme des formules logiques. Pour les boucles, vous les déroulez. Pour les tableaux, vous utilisez la théorie des tableaux de Z3. Pour les flottants, vous utilisez la théorie FP de Z3 et acceptez que le solveur puisse dépasser le temps imparti sur des expressions complexes.

L’écart entre « mécanique » et « facile » est là où la plupart des équipes se bloquent. Traduire une fonction Python dans le langage de Z3 nécessite de comprendre les deux. Mais une fois que vous avez la traduction, le solveur fait le gros du travail.

Le tableau de compromis que personne ne veut publier

La vérification formelle complète, prouver l’équivalence pour toutes les entrées possibles incluant chaque cas limite IEEE 754, est possible. Des gens le font pour des primitives cryptographiques et des systèmes avioniques. Cela coûte des semaines ou des mois de temps d’expert et nécessite des outils comme Coq ou Isabelle.

Le property-based testing coûte quelques minutes et attrape des bugs réels, mais n’offre aucune garantie.

La vérification bornée avec des solveurs SMT se situe au milieu. Elle vous donne une garantie pour une portée bien définie. Cette portée pourrait couvrir 99,9% de vos entrées de production. Que cela soit suffisamment bon dépend de ce que coûte une défaillance.

Il n’y a pas de déjeuner gratuit. Choisissez l’outil qui correspond à votre tolérance au risque et à l’expertise de votre équipe.

Un votant qui sait quand abandonner

La plupart des systèmes N-version implémentent un votant majoritaire naïf : renvoyer le résultat le plus commun, ou échouer s’il n’y a pas de majorité. Un meilleur votant connaît ses propres limites.

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

Quand le votant voit un désaccord persistant sur des classes d’entrée spécifiques, c’est un signal. Soit votre hypothèse d’équivalence est fausse, soit vous avez trouvé un bug dans une implémentation. Les deux valent la peine d’être connus.

Le votant n’est pas seulement là pour choisir les gagnants. Il est là pour vous dire quand vos hypothèses sur l’équivalence étaient fausses.

Que faire concrètement ensuite

Commencez par le property-based testing. C’est bon marché, ça trouve des bugs, et ça vous force à articuler ce que signifie « équivalence » pour votre domaine. Est-ce des sorties identiques bit à bit ? Des sorties dans un certain epsilon ? Des sorties qui satisfont la même postcondition ?

Une fois que vous avez défini l’équivalence de manière précise, passez à la vérification bornée si le domaine est fini et que les enjeux sont élevés. Utilisez Z3, CBMC, ou un outil similaire pour obtenir une preuve mécanique pour votre portée bornée.

Réservez la vérification formelle complète pour les parties où un bug tue littéralement des gens. Pour tout le reste, connaissez les limites de votre preuve et surveillez les désaccords en production. Le meilleur système N-version est celui qui sait ce qu’il ne sait pas.