Synthèse et équivalence
Protéger la forme de calculs importants tout en vérifiant la préservation de leurs résultats.
Reconstruire le calcul lui-même#
La synthèse inductive guidée par contre-exemples, CEGIS, cherche un autre calcul à partir du comportement et de contre-exemples. Dans les régions scalaires pures admissibles, elle construit des expressions dans une autre base booléenne-arithmétique et une autre structure d’évaluation. Le graphe d’expression lui-même peut ainsi changer.
Le contre-exemple guide le candidat suivant#
Le candidat est soumis à la validation de traduction régionale. Si une entrée révèle une divergence, ce témoin est réinjecté dans la synthèse et doit être pris en compte par le candidat suivant. La recherche et la preuve forment une boucle explicite, plutôt qu’une acceptation fondée sur quelques exemples réussis.
Seule une réécriture régionale prouvée est acceptée#
Le validateur distingue PROVED, COUNTEREXAMPLE_FOUND, OUT_OF_SCOPE et UNKNOWN_BUDGET_EXCEEDED. Seul PROVED autorise l’acceptation. L’épuisement du budget ne devient pas un succès ; une région hors du modèle pris en charge ne peut réutiliser une preuve d’un autre périmètre.
Explorez les règles de décision. Ce schéma n’exécute pas de solveur.
R₀(x)R₁(x)Résultats + traps + préconditions
Le candidat est accepté dans le modèle et les préconditions déclarés. Le verdict porte sur cette réécriture, pas sur toute l’application.
Une entrée concrète révèle une différence. Le candidat est rejeté et le témoin alimente la synthèse.
La région ne respecte pas les obligations de pureté, propriété, frame ou frontière. Ce modèle ne permet pas de l’accepter.
Le budget est épuisé sans preuve. Ce résultat indécis n’autorise pas la réécriture et n’est pas mis en cache comme preuve réussie.
La preuve possède un contrat précis#
Le modèle compare les résultats exacts sur 32/64 bits et les traps sous les préconditions d’entrée et obligations de frame déclarées. Largeurs signées, débordement et division par zéro en font partie. Les régressions couvrent les préconditions manquantes, traps divergents et résultats indécis, ainsi que le cache de preuves.
Il s’agit d’une propriété de correction limitée à la région acceptée, pas d’une preuve d’absence de bugs dans toute l’application ou d’impossibilité de rétro-ingénierie. La validation applicative et le modèle de sécurité restent distincts.