diff --git a/src/fs-filo-ext2.ads b/src/fs-filo-ext2.ads
index d19a00f..d8cc7e9 100644
--- a/src/fs-filo-ext2.ads
+++ b/src/fs-filo-ext2.ads
@@ -1,21 +1,49 @@
 package FS.FILO.Ext2 is
 
-   Sane_And_Mounted : Boolean with Ghost; -- TODO: track what FS type is mounted in FS.FILO
+   type T is private;
 
-   procedure Mount (Success : out Boolean)
+   function Is_Mounted (State : T) return Boolean;
+   function Is_Open (State : T) return Boolean
    with
-      Post => (if Success then Sane_And_Mounted);
+      Post => (if Is_Open'Result then Is_Mounted (State));
 
-   procedure Open (File_Path : String; Success : out Boolean)
+   procedure Mount
+     (State    : in out T;
+      Part_Len : in     Partition_Length;
+      Success  :    out Boolean)
    with
-      Pre => Sane_And_Mounted;
-   procedure Close
-   with
-      Convention => C,
-      Pre => Sane_And_Mounted;
+      Pre => not Is_Mounted (State),
+      Post => Success = Is_Mounted (State);
 
-   procedure Read (Buf : out Buffer_Type; Len : out Natural)
+   procedure Open
+     (State       : in out T;
+      File_Len    :    out File_Length;
+      File_Path   : in     String;
+      Success     : out    Boolean)
    with
-      Pre => Sane_And_Mounted;
+      Pre => Is_Mounted (State) and not Is_Open (State),
+      Post => Success = Is_Open (State);
+
+   procedure Close (State : in out T)
+   with
+      Pre => Is_Open (State),
+      Post => Is_Mounted (State);
+
+   procedure Read
+     (State    : in out T;
+      File_Len : in     File_Length;
+      File_Pos : in out File_Offset;
+      Buf      :    out Buffer_Type;
+      Len      :    out Natural)
+   with
+      Pre => Is_Open (State),
+      Post => Is_Open (State);
+
+private
+   type State is (Unmounted, Mounted, File_Opened);
+
+   type T is record
+      S : State;
+   end record;
 
 end FS.FILO.Ext2;