lingenic_text-file_io

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

-------------------------------------------------------------------------------
--  Lingenic-Text
--  Formally Verified Unicode Text Processing Library
--
--  File I/O: reads UCD text files from disk into Byte_Array buffers.
--
--  This is the ONLY SPARK_Mode(Off) code in the library.  The body uses
--  Ada.Streams.Stream_IO to read bytes.  Same trust level as the compiler —
--  it just moves bytes from disk to memory.  Everything downstream (parser,
--  name extraction, property lookup) is fully proved SPARK.
-------------------------------------------------------------------------------

package Lingenic_Text.File_IO
   with SPARK_Mode
is

   Max_File_Size : constant := 4_000_000;  --  4 MB, plenty for any UCD file

   subtype File_Size is Natural range 0 .. Max_File_Size;

   subtype File_Byte_Array is Byte_Array (1 .. Max_File_Size);

   ---------------------------------------------------------------------------
   --  Read an entire file into Buffer (1 .. Length).
   --
   --  Success is True when the file was read successfully.
   --  Success is False if the file does not exist, cannot be opened,
   --  or exceeds Max_File_Size bytes.
   --
   --  On failure, Length is 0 and Buffer contents are unspecified.
   ---------------------------------------------------------------------------

   procedure Read_File
     (Name    : String;
      Buffer  : out File_Byte_Array;
      Length  : out File_Size;
      Success : out Boolean)
   with Post => (if not Success then Length = 0);

end Lingenic_Text.File_IO;