Restructuring for better proof properties about gneiss

[jklmnn]

After a discussion separate pre and post conditions for callbacks are not feasible. The checks should happen in the application. This is both due to the fact that the platform code does not provide a full data flow in SPARK so that the callbacks are often called from C or outside SPARK mode which makes it possible to prove anything via preconditions. Also as the platform code is not proven and therefore it should not provide preconditions as they cannot be proven to be met.

[jklmnn]

Also the generic contract function doesn't seem fully feasible as the preconditions also can hardly be established in the platform. Also the danger of an unsound proof is higher since the platform code is not fully proven.

[jklmnn]

I think I found out why we could not prove those properties without a check in the callback. The session specific callbacks all provide a session identifier that tells who was the caller. What we tried to do is to prove somehow that the caller is always the only session object we have in our component package. But this is simply not possible since there could be some other session object that has been initialized with the same instance of the generic. So checking if the session was initialized was merely a proxy to the check if this has been called by our session (one that also only works if there is only one session). So instead of checking the initialization we should check if the caller is indeed our session and then we should be able to proof that all the properties of our session apply by annotating the identifier of our session with the same properties.
Example:

type Client_Session is limited private;
type Client_Instance is private;
Invalid_Instance : constant Client_Instance;

function Initialized (C : Client_Session) return Boolean;
function Initialized (C : Client_Instance) return Boolean with Ghost;

function Instance (C : Client_Session) return Client_Instance with
   Contract_Cases => (Initialized (C) => Instance'Result /= Invalid_Instance,
                      not Initialized (C) => Instance'Result = Invalid_Instance);

Note that for this to work properly that Instance must be callable on non initialized objects since we can only derive the instance from the object and not the other way round. If Instance would require the session to be initialized we would have to do the check twice.
In a callback we then could do the following:

Session : Client_Session := Create;

procedure Callback (I : Client_Instance)
is
begin
   if Instance (Session) = I then
      pragma Assert (Initialized (Session));
   end if;
end Callback;

What we can do here is to set a precondition to Callback that I is not invalid and then we can implicitly prove that Session is initialized if I is its identifier. But we still have to do the check that we use the correct session because the platform only enforces that whoever called this procedure is initialize but not that the known session has been calling it.

[jklmnn]

For Linux and Genode the thin binding should get post conditions that are executed. As this requires runtime support the exceptions should be added manually.

[jklmnn]

When using a global variable in a callback it can happen that a aliasing check fails if the callback is called from another procedure that takes the same global as an in out argument. In this case the global contract of the callback must denote the global variable as input and then the check can be marked as false positive. Unfortunately this also depends on the platform implementation and when callbacks are called (especially from where they're called).
Currently as far as I can tell all platforms call the same callbacks from the same procedure/function. It might be useful to add a comment to each procedure that calls a callback which one it calls and make this a rule that all platforms must follow.
This does not apply to callback functions as they do not alter global state at any time and can therefore be called always.

[jklmnn]

Fixed by #87.