fix muen block server test proof

ref #80

Author: jklmnn

src/block/muen/componolit-gneiss-block.adb

@@ -75,6 +75,6 @@ is
       (True); --  TODO: Range check for Session_Id
 
    function Identifier (S : Server_Session) return Session_Id is
-      (Session_Id'Val (Standard.Interfaces.Unsigned_32'Pos (S.Tag) + Session_Id'Pos (Session_Id'Last)));
+      (Session_Id'Val (Standard.Interfaces.Unsigned_32'Pos (S.Tag) + Session_Id'Pos (Session_Id'First)));
 
 end Componolit.Gneiss.Block;

src/block/server/muen/componolit-gneiss-block-dispatcher.adb

@@ -26,9 +26,14 @@ is
       (Serv.Event'Address) with
       SPARK_Mode => Off;
 
-   function Session_Address (D : Dispatcher_Session) return System.Address is
-      (D'Address) with
-      SPARK_Mode => Off;
+   function Session_Address (D : Dispatcher_Session) return System.Address;
+
+   function Session_Address (D : Dispatcher_Session) return System.Address with
+      SPARK_Mode => Off
+   is
+   begin
+      return D'Address;
+   end Session_Address;
 
    procedure Initialize (D   : in out Dispatcher_Session;
                          Cap :        Componolit.Gneiss.Types.Capability;
@@ -44,7 +49,7 @@ is
                                                    Block_Dispatch_Event => System.Null_Address,
                                                    Tag                  => Standard.Interfaces.Unsigned_32'Val
                                                                               (Session_Id'Pos (Tag)
-                                                                               - Session_Id'Pos (Session_Id'Last)),
+                                                                               - Session_Id'Pos (Session_Id'First)),
                                                    Session              => Session_Address (D));
             exit;
          end if;