EN

PREUVE EN DIRECT · PYTHON VERS C

Traduit en C. Prouvé, pas testé.

Une étape de filtre en virgule fixe, le genre de prototype de traitement du signal qu’on porte vers une puce. Écrit en Python, traduit en C embarqué, puis vérifié par un solveur sur toutes les entrées que la fonction peut recevoir.

PYTHON · L’ORIGINAL

def ema_step(prev, x, alpha_q15):
    acc = prev * (32768 - alpha_q15) + x * alpha_q15
    y = acc >> 15          # Python: a shift is a division by 2**15 rounded toward minus infinity
    return max(-32768, min(32767, y))

C · LA TRADUCTION

#include <stdint.h>
/* Embedded C translation of ema.py */
int16_t ema_step(int16_t prev, int16_t x, uint16_t alpha_q15) {
    int32_t acc = (int32_t)prev * (32768 - (int32_t)alpha_q15) + (int32_t)x * (int32_t)alpha_q15;
    int32_t y = acc >> 15;
    if (y > 32767) y = 32767;
    if (y < -32768) y = -32768;
    return (int16_t)y;
}

CE QUI EST PROUVÉ

Le même résultat, sur toutes les entrées. Pas sur un échantillon.

Pour toutes les valeurs 16 bits de prev et de x, et tout alpha de 0 à 32 768, le C rend exactement ce que rend le Python. Le solveur n’essaie pas les entrées une à une : il montre qu’aucune entrée ne les fait diverger.

140 741 783 322 624

combinaisons d’entrées couvertes

0 sur 15

vérifications en échec, débordements et conversions compris

1,3 s

pour le prouver, sur un portable

LA COMMANDE ET SA SORTIE · CBMC 6.10.0 AVEC Z3

$ cbmc harness.c ema.c --signed-overflow-check --conversion-check --z3
...
** Results:
** 0 of 15 failed (1 iterations)
VERIFICATION SUCCESSFUL

L’ERREUR QU’UN TEST RATERAIT

La traduction la plus naturelle se trompe d’un point.

Écrivez la division de la façon évidente en C, acc / 32768, et elle a l’air juste. Mais le C arrondit vers zéro, et Python vers moins l’infini. Le solveur trouve une entrée où ils se séparent :

Python rend −4752

le C naïf rend −4751

prev = −12 565, x = 8 715, alpha = 12 032. Un point d’écart, seulement sur certaines valeurs négatives : le genre de différence qui passe une suite de tests et revient plus tard sous forme de chiffre faux. Une seconde faute plantée, alpha décalé d’un, a été attrapée de la même façon.

UNE SECONDE VÉRIFICATION, INDÉPENDANTE

La preuve compare le C à une référence que nous avons transcrite depuis le Python. Pour attraper une erreur dans cette transcription, le vrai Python et le C compilé ont aussi tourné côte à côte sur 100 000 entrées, valeurs limites comprises : 0 différence.

CE QUE CETTE PAGE NE MONTRE PAS

  • Une seule fonction courte, sans boucle. Les programmes plus grands sont le travail à venir, pas ce que cette page prouve.
  • La référence de la preuve est une transcription à la main de la sémantique Python ; c’est l’exécution sur 100 000 entrées qui la contrôle, et un échantillon n’est pas une preuve.
  • Ce C n’est pas encore conforme MISRA : une passe séparée a trouvé des écarts à corriger avant qu’il parte dans un appareil réglementé.

REFAITES-LE SANS NOUS

Quatre fichiers. Une commande. Votre machine.

  1. 01Téléchargez les quatre fichiers ci-dessous.
  2. 02Prouvez la traduction : cbmc harness.c ema.c --signed-overflow-check --conversion-check --z3
  3. 03Compilez le C (cc -O2 -shared -o libema.dylib ema.c sur macOS ; ajoutez -fPIC et nommez-le libema.so sur Linux), puis lancez python3 check.py.

LES FICHIERS

ENVOYEZ-NOUS UN PROGRAMME