Proof platform

[jklmnn]

To prove applications a dedicated proof platform should be designed. This platform does not allow to compile complete applications but only objects sufficient to run gnatprove. It should be designed to incorporate all properties and behaviours any platform should implement while providing all info to SPARK.
It also should be easy to use from Linux without any further dependencies.

Currently all platforms have drawbacks. Genode does aliasing in C++ which is not checked in SPARK. While that aliasing is intended its absence cannot be proven from SPARK as it is hidden in C++.
Linux does not implement all session types making it not possible to prove Block Server on Linux.
Muen, while being complete in sessions and proof requires a rather complex setup to prove.