qoi

Verified Scala implementation of QOI using Stainless

A Scala implementation of the Quite OK Image lossless compression algorithm, formally verified using Stainless.

This case study is described in the FMCAD 2022 paper Formally Verified Quite OK Image Format.

The following properties are verified:

• Absence of runtime failure such as out-of-bound array accesses, division by zero, pattern matching, and so on (but not OOM).
• Program termination
• Decoding is the inverse of decoding
  • This property is stated in encoder.scala, lines 43-56

Additionally, one may run the Stainless' GenC pipeline to transpile Scala into C (see below).

Directory structure

• verified contains the verified Scala implementation, along with the necessary proof annotations and lemmas to prove the above-stated properties
• unannotated has the same implementation as verified, except that we removed all annotations.
• genc includes scripts and C files allowing to try out the generated C files from Scala files.
  • make genc triggers a command to run GenC and transpile Scala to C (generating files stainless.c and stainless.h)
  • The script test-genc.sh converts sample images from QOI to PNG and vice-versa (using a modified version of qoiconv.c)
  • The script run-bench.sh executes a modified version of qoibench.c to compare the reference implementation to ours.

Additional resources

• This case study was first mentioned as part of the ASPLOS 2022 Stainless tutorial.
• FMCAD 2022 Paper