AdaCore Blog

Make with Ada: Formal proof on my wrist

Make with Ada: Formal proof on my wrist

by Fabien Chouteau

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 Pebble.Ui.Layers is 
   function Create (Frame : Grect) return Layer; -- pebble.h:3790
   pragma Import (C, Create, "layer_create"); 
end Pebble.Ui.Layers;

The API uses almost exclusively pointers to hidden structures:

typedef struct Window Window;

Window * window_create(void);

which we can conveniently map in Ada like so:

type Window is private;

   function Create return Window;
   pragma Import (C, Create, "window_create"); 

private

   type Window is new System.Address;

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 (redirected now to rebble.io as Pebble ceased operations), 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 persist_read_data(const uint32_t key, void * buffer, const size_t buffer_size);
int persist_write_data(const uint32_t key, const void * data, const size_t size);
bool persist_exists(const uint32_t key);

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;
   type Data_Type is private;

package Pebble.Generic_Persistent_Storage is
    function Write (Data : Data_Type) return Boolean;
   --  Write data associated with the key, return True on success

   function Read (Data : out Data_Type) return Boolean;
   --  Read data associated with the key, return True on success

   function Exists return Boolean;
   --  Return True if there is data associated with the key

   procedure Erase;
   --  Erase data associated with the key
end Pebble.Generic_Persistent_Storage;

Using the persistent storage is now as simple as:

type My_Data is record
      Level : Natural;
      XP    : Natural;
   end record;

   package My_Data_Storage is new Pebble.Generic_Persistent_Storage (1, My_Data);

   Player : My_Data;
begin

   if not My_Data_Storage.Read (Player) then
      Player.XP    := 0;
      Player.Level := 1;
   end if;

    --   Insert complex gameplay here…

   if not My_Data_Storage.Write (Player) then
      Put_Line ("The game could not be saved");
   end if;

Sources

The binding and app source code are available on GitHub.


Posted in #SPARK2014     #Smartwatch    #Makers   

About Fabien Chouteau

Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.