Make with Ada: Formal Proof On My Wrist

When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.

At first I wasn't sure if I was going to replace the Pebble OS entirely or only write an application for it. The first option requires to re-write all the drivers (screen, bluetooth, etc) and I would also need a way to program the chip, which to my knowledge requires opening the watch and soldering a debug interface to the chip. Since I’m not ready to crack open a $200 watch just for the sake of hacking I decided to go with the second option, write an app.

Binding the C API to Ada

The Pebble SDK is very well thought out and provides an emulator based on QEMU which is great for testing. In fact I developed and tested the binding with this SDK before I even got the real watch.

The entire API is contained in a single C header (pebble.h). I used GNAT's switch -fdump-ada-spec to generate a first version of the binding, then I reformatted it to split the features in packages and rename the subprograms. For example, the function layer_create became:

package
    
   
; 

The API uses almost exclusively pointers to hidden structures:

typedef
Window * window_create(

Which we can conveniently map in Ada like so:

Overall the binding was relatively easy to create.

Smartwatch app and formal proof

To use this binding I decided to port the formally proven Tetris written in SPARK by Yannick and Tristan.

The game system being the same, this port consists of a new graphical front-end, menus and button handling. The app was quite straightforward to develop, the Pebble API is well designed and quite easy to use.

The formal proof is focused on things that are impossible to test, in our case, the game system. Can you think of a way to test that the code will reject invalid moves on any piece, in any orientation, at any position and for every board state possible (that's trillions or quadrillions of combinations)?

The first thing we get from SPARK analysis is the absence of run-time error. For us it means, for instance, that we are sure not to do invalid access to the game board matrix.

Then we prove high level game properties like:

• Never move the falling piece into an invalid position

• The falling piece will never overlap the pieces already in the board

• All the complete lines are removed

• Whatever the player does, the game will always be in a valid state

This application was released on the Pebble app store under the name of PATRIS, and as of today more than 660 users downloaded it.

I also made a watchface using the blocks to display time digits.

Persistent storage

The last thing I did was to create a higher interface to the persistent storage API, a mechanism to store data and retrieve it after the app is closed.

The C interface is very simple with only a couple of functions. Each data is associated with a uint32_t key, so the app can read, write and test the existence of data for a given key.

int
int
bool

But of course, the Ada type system doesn't like void pointers and to be able to use the persistent storage without having to deal with nasty unchecked conversions (same as C casts) I wrote a generic package that automatically takes care of everything:

generic
   Data_Key : Uint32_T;
   
package
    
   --  Write data associated with the key, return True on success
   
   --  Read data associated with the key, return True on success
   
   --  Return True if there is data associated with the key
   
   --  Erase data associated with the key
end

Using the persistent storage is now as simple as:

      Level : Natural;
      XP    : Natural;
   
   
   Player : My_Data;
begin
   
      Player.XP    := 0;
      Player.Level := 1;
   
    --   Insert complex gameplay here…
   
      Put_Line ("The game could not be saved");
   

Sources

The binding and app source code are available on GitHub.