package FILO.FS.Ext2 is

   type T is private;

   function Is_Mounted (State : T) return Boolean;
   function Is_Open (State : T) return Boolean
   with
      Post => (if Is_Open'Result then Is_Mounted (State));

   procedure Mount
     (State    : in out T;
      Part_Len : in     Partition_Length;
      Success  :    out Boolean)
   with
      Pre => not Is_Mounted (State),
      Post => Success = Is_Mounted (State);

   procedure Open
     (State       : in out T;
      File_Len    :    out File_Length;
      File_Type   :    out FS.File_Type;
      File_Name   : in     String;
      In_Root     : in     Boolean;
      Success     : out    Boolean)
   with
      Pre => Is_Mounted (State),
      Post => (if Success then Is_Open (State) else Is_Mounted (State));

   procedure Close (State : in out T)
   with
      Pre => Is_Open (State),
      Post => Is_Mounted (State);

   procedure Read
     (State    : in out T;
      File_Pos : in out File_Offset;
      Buf      :    out Buffer_Type;
      Len      :    out Natural)
   with
      Relaxed_Initialization => Buf,
      Pre => Is_Open (State) and Buf'Length > 0,
      Post => Is_Open (State) and Buf'Initialized;

private
   type State is (Unmounted, Mounted, File_Opened);

   -- maximum block size is 64KiB (2^16):
   subtype Log_Block_Size is Positive range 10 .. 16;
   subtype Block_Size is Natural range 2 ** Log_Block_Size'First .. 2 ** Log_Block_Size'Last;
   subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1;

   -- Extent physical addresses are 48 bits.
   type FSBlock_Offset is new Block_Offset range 0 .. 2 ** 48 - 1;
   -- Logical block addresses are 32 bits.
   type FSBlock_Logical is new Block_Offset range 0 .. 2 ** 32 - 1;

   -- We use a 64KiB cache which fits at least one ext2 block. If a lower
   -- block size is encountered (likely), we partition the cache into up
   -- to 64 1KiB blocks.
   subtype Block_Cache_Index is Natural range 0 .. 63;
   File_Cache_Level : constant := 0;      -- Use a single cache block each for
   Inode_Cache_Level : constant := 1;     -- file contents, the inode block,
   Group_Cache_Level : constant := 2;     -- the group block.
   Block_Map_Cache_Level : constant := 3; -- Use all other cache blocks for
                                          -- mapping file content blocks.
   type Cache_Label is array (Block_Cache_Index) of FSBlock_Offset;
   subtype Cache_Buffer is Buffer_Type (Max_Block_Index);

   -- Same as the 12 direct + 3 indirect blocks times 4B:
   subtype Inline_Extents_Index is Natural range 0 .. 59;
   subtype Inline_Extents is Buffer_Type (Inline_Extents_Index)
   with
      Object_Size => (Inline_Extents_Index'Last + 1) * 8;

   -- TODO: Could use modular Unsigned_32 if GNATprove wouldn't stumble as much:
   type Inode_0_Index is new Integer_64 range 0 .. Integer_64 (Unsigned_32'Last);
   subtype Inode_Index is Inode_0_Index range 2 .. Inode_0_Index'Last;
   subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
   subtype Group_Desc_Size  is Positive range  32 .. 2 ** 15; -- power-of-2 that fits in 16 bits

   type Inode_Type is (Dir, Regular, Link, Fast_Link);
   type Inode_Length is range 0 .. 2 ** 46;

   type Inode_Map_Cache is record
      Phys     : FSBlock_Offset := 0;
      Logical  : Block_Offset := Block_Offset'Last;
   end record;

   type Inode_Info is record
      I           : Inode_Index := Inode_Index'First;
      Mode        : Inode_Type := Inode_Type'First;
      Size        : Inode_Length := 0;
      Use_Extents : Boolean := False;
      Inline      : Inline_Extents := (others => 16#00#);
      Map_Cache   : Inode_Map_Cache := (others => <>);
   end record;

   type Group_Index is new Inode_0_Index;
   subtype Group_In_Block_Count is Group_Index
      range 1 .. Group_Index (Block_Size'Last / Group_Desc_Size'First);
   type Group_In_Block_Index is new Natural range 0 .. Natural (Group_In_Block_Count'Last - 1);

   subtype Inode_In_Group_Count is Inode_0_Index range 1 .. Inode_0_Index'Last;
   type Inode_In_Group_Index is new Inode_0_Index range 0 .. Inode_In_Group_Count'Last - 1;
   subtype Inode_In_Block_Count is Inode_In_Group_Index
      range 1 .. Inode_In_Group_Index (Block_Size'Last / Inode_Size'First);
   type Inode_In_Block_Index is new Natural range 0 .. Natural (Inode_In_Block_Count'Last - 1);

   type Mount_State is record
      Part_Len             : Partition_Length := 0;
      First_Data_Block     : Unsigned_32 := Unsigned_32'First;
      Block_Size_Bits      : Log_Block_Size := Log_Block_Size'First;
      Block_Size           : Ext2.Block_Size := Ext2.Block_Size'First;
      Inodes_Per_Group     : Inode_In_Group_Count := Inode_In_Group_Count'First;
      Inode_Size           : Ext2.Inode_Size := Ext2.Inode_Size'First;
      Inodes_Per_Block     : Inode_In_Block_Count := Inode_In_Block_Count'First;
      Group_Desc_Size      : Ext2.Group_Desc_Size := Ext2.Group_Desc_Size'First;
      Group_Desc_Per_Block : Group_In_Block_Count := Group_In_Block_Count'First;
      Feature_Extents      : Boolean := False;
      Feature_64Bit        : Boolean := False;
   end record;

   type Block_Cache is record
      Phys     : Cache_Label := (others => 0);
      Buffer   : Cache_Buffer := (others => 16#00#);
   end record;

   type T is record
      Static   : Mount_State  := (others => <>);
      S        : State;
      Inode    : Inode_Info   := (others => <>);
      Cur_Dir  : Inode_Index  := Inode_Index'First;
      Cache    : Block_Cache  := (others => <>);
   end record;

end FILO.FS.Ext2;