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;About 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.