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.