A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression designed to have a very simple implementation (about 300 lines of C).

Shortly, a few alternative implementations popped up here and there, and in this kind of situation we are eager to show what Ada/SPARK can bring to the table.

So we started by writing a translation from the C implementation to Ada. The code was already quite different thanks to Ada features such as nested subprograms or range tests. We also used representations clauses to easily read/write QOI “chunks” and avoid bit shifts and masks that can be difficult to understand:

The next step was to use SPARK to prove the absence of run-time error. With this algorithm that mostly translates data from one buffer to another, the main benefit is to guarantee that the code does not have out-of-bounds access when encoding the image.

Like in the C implementation, we decided to leave the responsibility of allocating the output buffer to the caller, and to provide a function to compute the worst case output size. This worst case output size is one of the preconditions for the Encode subprogram. With SPARK, users can therefore prove that images will always be successfully encoded.

Passing the proof required adding pre- and post-conditions to specify what each function expects and guarantees, and loop invariants in the main loop to help the prover analyze the behavior of the loop. The main encoding loop is iterating over every pixel of the image, and some iterations will "push" more data to the output buffer than others. But we don't overflow because that means we did not push anything during the previous iteration.

SPARK is also quite picky about initialization, so by default it requires that the output buffer is fully initialized on return. That’s not so convenient here, as the encoded data size will most of the time be smaller than the worst case buffer size provided by the caller. To have more flexibility, we added the aspect Relaxed_Initialization on the output buffer to specify that it may not be fully initialized, and we specify in the postcondition which part of the array is initialized, and thus can be read by the user after the procedure call.

A possible next step for the user interface would be to add contracts on Encode and Decode that would enable the user to prove the preconditions of one with the postconditions of the other, which is likely to happen in practice.

This SPARK QOI encoder/decoder code is hosted on GitHub and available in the Alire ecosystem in the “qoi” crate. You can get it with:

And if you go into the tests directory you can build a simple PNG/QOI converter:

To use the library in your own projects, simply run

The code is compatible with ZFP run-times, so you can use it in embedded projects.