UCD PARSER MODULE
=================

Standard: UAX #44 Section 4.2
Files:    src/lingenic_text-ucd_format_spec.ads       (ghost specification)
          src/lingenic_text-ucd_parser.ads            (public API)
          src/lingenic_text-ucd_parser.adb            (implementation)
          src/lingenic_text-scx_parser.ads            (Script_Extensions parser)
          src/lingenic_text-scx_parser.adb            (Script_Extensions implementation)
          src/lingenic_text-bidi_brackets_spec.ads     (BidiBrackets ghost spec)
          src/lingenic_text-bidi_brackets_spec.adb     (opaque wrapper bodies)
          src/lingenic_text-bidi_brackets_parser.ads    (BidiBrackets parser API)
          src/lingenic_text-bidi_brackets_parser.adb    (BidiBrackets parser body)
          src/lingenic_text-file_io.ads               (file I/O)
          src/lingenic_text-file_io.adb               (file I/O implementation)


PURPOSE
-------

The UCD parser reads standard-format Unicode Character Database property
files (Scripts.txt, GraphemeBreakProperty.txt, WordBreakProperty.txt,
etc.) from in-memory byte buffers and populates flat lookup tables
indexed by codepoint.

The entire chain from file format to query result is machine-checked.
The parser's postconditions reference the ghost specification in
UCD_Format_Spec, proving that for every codepoint, the parsed table
value corresponds to what the UCD file specifies.


UCD FILE FORMAT (UCD_Format_Spec)
---------------------------------

Package Lingenic_Text.UCD_Format_Spec is Ghost and Pure.  It encodes
the standard UCD property file format as expression functions:

  codepoint_or_range ; property_value # comment

Where codepoint_or_range is XXXX or XXXX..YYYY (4-6 uppercase hex
digits, no prefix).  Lines starting with '#' are comments.  Blank
lines are skipped.  Whitespace around fields is trimmed.

The ghost specification is organized in layers:

Layer 1: Byte classification
  Inherited from the root package: Is_Hex_Digit, Hex_Value,
  Is_Line_End, Is_Field_Space.

Layer 2: Scanning helpers (recursive, with Subprogram_Variant)

  Hex_Digit_Count(Source, Pos)     Count consecutive hex digits at Pos
  Parse_Hex_1..6(Source, Pos)      Parse N-digit hex number at Pos
  Parse_Hex(Source, Pos, Len)      Dispatch to Parse_Hex_N by length
  Next_Line_Start(Source, Pos)     Find position after next LF
  Skip_Spaces(Source, Pos)         Find first non-space on line
  Find_Semicolon(Source, Pos)      Find ';' on current line
  Find_Value_End(Source, Pos)      Find '#', LF, CR, or past end

Layer 3: Data line predicates

  Is_Data_Line(Source, Line_Start)
    True if the line starts with 4-6 hex digits and has a semicolon.

  Is_Range_Line(Source, Line_Start)
    True if the line has XXXX..YYYY format.

  Line_First_CP(Source, Line_Start)
    Extract the first (or only) codepoint.

  Line_Last_CP(Source, Line_Start)
    Extract the range endpoint.

Layer 4: Value field extraction

  Value_Start(Source, Line_Start)  First non-space after ';'
  Value_End(Source, Line_Start)    Position of '#', LF, or end
  Trim_Spaces_End(Source, F, L)    Trim trailing spaces from range

Layer 5: File-level assignment

  Line_Covers_CP(Source, Line_Start, CP)
    True if the data line at Line_Start assigns a value to codepoint CP.

Layer 6: Byte comparison

  Bytes_Equal(Source, A_First, B_First, Len)
    Byte-by-byte equality for matching value strings.

All functions have preconditions requiring Source'First = 1 and
Source'Last < Positive'Last.  All recursive functions have
Subprogram_Variant annotations proving termination.


PARSER (UCD_Parser)
-------------------

Types:

  subtype Property_Index is Natural range 0 .. 255;
  type Property_Table is array (Codepoint) of Property_Index;
  type Value_Name is record First : Positive; Last : Natural; end record;
  type Value_Name_Array is array (1 .. 255) of Value_Name;

  Property_Index 0 = default/unassigned.
  Indices 1..255 are named values discovered from the file.
  Value_Name entries point to byte ranges within the source buffer.

Ghost Correctness Specification:

  Ghost_Match(Source, Val_First, Val_Len, Names, I)
    Does the value field match Names(I)?

  Ghost_Match_Index(Source, Val_First, Val_Len, Names, Num_Values, I)
    Search Names(1..Num_Values) for a match; return first match or 0.
    Recursive, increasing I.

  Line_Value_Index(Source, Line_Start, Names, Num_Values)
    What index does a data line's value field match?
    Composes field extraction + trimming + matching.

  Expected_Value(Source, Pos, CP, Names, Num_Values)
    What should Table(CP) be after processing all lines from Pos forward?
    Recursive over lines.  Later lines take precedence (last-writer-wins).
    Returns 0 (default) if no line assigns CP.

  Expected_From(Source, Pos, CP, Names, Num_Values)
    Boundary-safe wrapper for Expected_Value.

Public Procedures:

  procedure Parse_Property_File
    (Source     : Byte_Array;
     Names      : Value_Name_Array;
     Num_Values : Property_Index;
     Table      : out Property_Table;
     Success    : out Boolean);

    Pre:  Source'First = 1, Source'Last < Positive'Last,
          Source'Length > 0, Num_Values >= 1
    Post: Safety:    for all CP => Table(CP) in 0..Num_Values
          Correctness: for all CP =>
            Table(CP) = Expected_Value(Source, 1, CP, Names, Num_Values)

    The correctness postcondition proves that every codepoint's property
    value matches the recursive ghost specification -- which in turn
    encodes the UCD file format rules.

  procedure Extract_Value_Names
    (Source     : Byte_Array;
     Names      : out Value_Name_Array;
     Num_Values : out Property_Index;
     Success    : out Boolean);

    Scans Source line by line, discovers unique property value names.
    Post: Every name entry points to valid bytes in Source.
    Transitively validated: if any value is missing, Parse_Property_File
    will fail for lines using that value.

Runtime Line-Scanning Helpers:

  The parser exposes proved-equivalent runtime functions for use by
  other parsers (e.g., Scx_Parser):

    Skip_WS(Source, Pos)        = UCD_Format_Spec.Skip_Spaces
    Find_Semi(Source, Pos)      = UCD_Format_Spec.Find_Semicolon
    Parse_CP(Source, Pos, CP, Len)  Parse 4-6 hex codepoint
    Next_Line(Source, Pos)      = UCD_Format_Spec.Next_Line_Start
    Find_Val_End(Source, Pos)   = UCD_Format_Spec.Find_Value_End
    Trim_Trailing(Source, F, L) = UCD_Format_Spec.Trim_Spaces_End

  Each has a postcondition proving equivalence to the corresponding
  ghost function.

Ghost Lemmas:

  Lemma_Hex_Digit_Count(Source, Pos, Len)
    Links Parse_CP output to the ghost Hex_Digit_Count function.
    If Parse_CP reports Len hex digits at Pos, then
    Hex_Digit_Count(Source, Pos) = Len.

  Lemma_HDC_GT_6(Source, Pos)
    If 7+ consecutive hex digits at Pos, then Hex_Digit_Count >= 7.
    Used to reject oversized codepoints in range detection.


SCRIPT_EXTENSIONS PARSER (Scx_Parser)
--------------------------------------

ScriptExtensions.txt has a different value field format: space-separated
script abbreviations rather than a single value.  Scx_Parser handles
this with pool interning.

Types:

  type Script_Set is record
    Count : Natural range 0 .. 255;
    Items : array (1 .. 255) of Property_Index;
  end record;

  subtype Scx_Pool_Id is Natural range 0 .. 512;
  type Scx_Pool_Array is array (1 .. 512) of Script_Set;
  type Scx_Table_Array is array (Codepoint) of Scx_Pool_Id;

  Pool_Id 0 = sentinel (CP not covered by ScriptExtensions.txt).

Ghost Membership Predicates:

  Set_Has_From(S, Idx, From)  Recursive membership test from position From
  Set_Has(S, Idx)             Top-level membership test (opaque to solver)
  Pool_Has(Pool, End, P, Script_Idx)  Does pool entry P contain script?

Public Procedure:

  procedure Parse_ScriptExtensions
    (Scx_Src, Script_Src : Byte_Array;
     Script_Names : Value_Name_Array;
     Script_Count : Property_Index;
     Pool : out Scx_Pool_Array;
     Pool_End : out Scx_Pool_Id;
     Table : out Scx_Table_Array);

  ~300 distinct script-sets are interned in the pool for 1.1M codepoints.


BIDI BRACKETS PARSER (Bidi_Brackets_Parser)
--------------------------------------------

BidiBrackets.txt has a different format from standard UCD property files:
two codepoint fields and a bracket type ('o' or 'c'), no ranges.

  HHHH; HHHH; o/c # comment

Ghost Specification (Bidi_Brackets_Spec):

  Reuses UCD_Format_Spec lower layers (hex scanning, line scanning,
  Is_Data_Line, Line_First_CP) and adds BidiBrackets-specific layers:

  Field1_Start(Source, Line_Start)        Start of paired-CP field
  Field1_Hex_Count(Source, Line_Start)    Hex digit count in field 1
  Find_Second_Semi(Source, Line_Start)    Position of second semicolon
  Type_Field_Pos(Source, Line_Start)      Position of 'o'/'c' byte
  Is_Bracket_Data_Line(Source, LS)        Valid bracket data line
  Line_Paired_CP(Source, Line_Start)      Paired codepoint value
  Line_Bracket_Type(Source, Line_Start)   Type byte ('o' or 'c')
  Is_Open_Line / Is_Close_Line           Open/close classification

  Expected-output recursive functions (one per table):
    Expected_Open_Mapping(Source, Pos, CP)     Open table value
    Expected_Close_Mapping(Source, Pos, CP)    Close table value
    Expected_Is_Open(Source, Pos, CP)          Open flag
    Expected_Is_Close(Source, Pos, CP)         Close flag

  Opaque wrappers (Expected_*_From): prevent cascading recursive
  auto-inlining in loop invariant VCs.

Public Procedure:

  procedure Parse_Brackets_File
    (Source       : Byte_Array;
     Open_Table   : out Bracket_Table;
     Close_Table  : out Bracket_Table;
     Open_Flags   : out Bracket_Flag_Table;
     Close_Flags  : out Bracket_Flag_Table;
     Lines_Parsed : out Natural;
     Success      : out Boolean);

    Pre:  Source'First = 1, Source'Last < Positive'Last, Source'Length > 0
    Post: Safety:      for all CP => Open_Table(CP) and Close_Table(CP)
                                     are valid codepoints
          Correctness: for all CP =>
            Open_Table(CP) = Expected_Open_From(Source, 1, CP)
            Close_Table(CP) = Expected_Close_From(Source, 1, CP)
            Open_Flags(CP) = Expected_Is_Open_From(Source, 1, CP)
            Close_Flags(CP) = Expected_Is_Close_From(Source, 1, CP)
          Truncation:  if Success then Lines_Parsed >= 120

  The postcondition proves that every codepoint's bracket table entries
  match the recursive ghost specification -- the same Platinum-level
  guarantee as the UCD property parser.


FILE I/O (File_IO)
------------------

  procedure Read_File
    (Name    : String;
     Buffer  : out Byte_Array;
     Length  : out Natural;
     Success : out Boolean);

  Maximum file size: 4 MB per file.
  SPARK_Mode(Off) -- this is the only non-SPARK code in the library.
  Trust boundary: same as the compiler.  Once bytes are in memory,
  everything is proved.
