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-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.
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.