LIVE PROOF · PYTHON TO C

Translated to C. Proven, not tested.

A fixed-point filter step, the kind of signal-processing prototype teams port to a chip. Written in Python, translated to embedded C, then checked by a solver on every input the function can receive.

PYTHON · THE 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 · THE TRANSLATION

#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;
}

WHAT WAS PROVEN

Same result, on every input. Not on a sample.

For every 16-bit value of prev and x, and every alpha from 0 to 32,768, the C returns exactly what the Python returns. The solver does not try inputs one by one: it shows that no input exists where the two differ.

140,741,783,322,624

input combinations covered

0 of 15

checks failed, overflow and conversion included

1.3 s

to prove it, on a laptop

THE COMMAND AND ITS OUTPUT · CBMC 6.10.0 WITH Z3

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

THE BUG A TEST WOULD MISS

The most natural translation is wrong by one.

Write the division the obvious way in C, acc / 32768, and it looks right. But C rounds toward zero, and Python rounds toward minus infinity. The solver finds an input where they part:

Python returns −4752

the naive C returns −4751

prev = −12,565, x = 8,715, alpha = 12,032. One step off, only on some negative values: the kind of difference that passes a test suite and shows up later as a wrong figure. A second planted fault, alpha off by one, was caught the same way.

A SECOND, INDEPENDENT CHECK

The proof compares the C to a reference we transcribed from the Python. To catch a mistake in that transcription, the real Python and the compiled C also ran side by side on 100,000 inputs, edge values included: 0 differences.

WHAT THIS DOES NOT SHOW

One short function, with no loop. Larger programs are the work ahead, not something this page proves.
The proof's reference is a hand transcription of the Python semantics; the 100,000-input run is what checks it, and a sample is not a proof.
This C is not yet MISRA-clean: a separate run found deviations to fix before it would ship to a regulated device.

RE-RUN IT WITHOUT US

Four files. One command. Your machine.

01Download the four files below.
02Prove the translation: cbmc harness.c ema.c --signed-overflow-check --conversion-check --z3
03Build the C (cc -O2 -shared -o libema.dylib ema.c on macOS; add -fPIC and name it libema.so on Linux), then run python3 check.py.

THE FILES

SEND US A PROGRAM