-- 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
--
-- Proved UCD property file parser.
--
-- Reads a standard-format UCD property file (Scripts.txt,
-- GraphemeBreakProperty.txt, etc.) from an in-memory Byte_Array and
-- populates a flat lookup table indexed by codepoint.
--
-- The parser's postconditions reference the ghost spec in
-- Lingenic_Text.UCD_Format_Spec, establishing that for every codepoint
-- the parsed table value corresponds to what the UCD file specifies.
--
-- Property values are represented as (start, end) byte positions into
-- the source buffer. Higher-level code maps these to typed indices.
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Format_Spec;
package Lingenic_Text.UCD_Parser
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- Property value index: 0 = default/unassigned, 1..Max = named values
---------------------------------------------------------------------------
subtype Property_Index is Natural range 0 .. 255;
Default_Index : constant Property_Index := 0;
---------------------------------------------------------------------------
-- Property table: flat array indexed by codepoint
---------------------------------------------------------------------------
type Property_Table is array (Codepoint) of Property_Index;
---------------------------------------------------------------------------
-- Value name table: maps Property_Index to (first, last) byte positions
-- in the source buffer. The parser matches value strings from data lines
-- against these names to determine the index.
--
-- Entry 0 is the default value (not matched against data lines).
-- Entries 1..Num_Values are the known property value names.
---------------------------------------------------------------------------
type Value_Name is record
First : Positive;
Last : Natural; -- 0 means unused entry
end record;
Max_Value_Names : constant := 255;
type Value_Name_Array is array (Property_Index range 1 .. Max_Value_Names)
of Value_Name;
---------------------------------------------------------------------------
-- Ghost correctness specification
--
-- These ghost functions define what the parser's output SHOULD be.
-- The parser's postcondition proves it matches this specification.
--
-- Ghost_Match: does a value byte range [VF..VF+VLen-1] match Names(I)?
-- Ghost_Match_Index: which Names entry matches? (0 if none)
-- Line_Value_Index: what index does a data line's value field match?
-- Expected_Value: recursive over lines — what should Table(CP) be?
---------------------------------------------------------------------------
-- Does the value field [Val_First .. Val_First + Val_Len - 1] match
-- the name at Names(I)?
function Ghost_Match
(Source : Byte_Array;
Val_First : Positive;
Val_Len : Natural;
Names : Value_Name_Array;
I : Property_Index) return Boolean
is (I >= 1
and then Names (I).Last >= Names (I).First
and then Names (I).First in Source'Range
and then Names (I).Last in Source'Range
and then Names (I).Last - Names (I).First + 1 = Val_Len
and then Val_Len > 0
and then UCD_Format_Spec.Bytes_Equal
(Source, Val_First, Names (I).First, Val_Len))
with Ghost,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then I in 1 .. Max_Value_Names
and then (if Val_Len > 0 then
Val_First in Source'Range
and then Source'Last - Val_First >= Val_Len - 1);
-- Search Names(1..Num_Values) for a match against the value field.
-- Returns the first matching index, or 0 if none.
-- Recursive: checks entry I, then recurses on I+1.
function Ghost_Match_Index
(Source : Byte_Array;
Val_First : Positive;
Val_Len : Natural;
Names : Value_Name_Array;
Num_Values : Property_Index;
I : Property_Index) return Property_Index
is (if I > Num_Values then 0
elsif Ghost_Match (Source, Val_First, Val_Len, Names, I) then I
elsif I = Num_Values then 0
else Ghost_Match_Index (Source, Val_First, Val_Len,
Names, Num_Values, I + 1))
with Ghost,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Num_Values >= 1
and then I >= 1
and then (if Val_Len > 0 then
Val_First in Source'Range
and then Source'Last - Val_First >= Val_Len - 1),
Subprogram_Variant => (Increases => I),
Post => Ghost_Match_Index'Result in 0 .. Num_Values;
-- What index does the data line at Line_Start match?
-- Composes value field extraction (with trailing-space trimming) with
-- ghost matching. Returns 0 if the value field is empty or doesn't
-- match any name.
function Line_Value_Index
(Source : Byte_Array;
Line_Start : Positive;
Names : Value_Name_Array;
Num_Values : Property_Index) return Property_Index
is (declare
VS : constant Natural :=
UCD_Format_Spec.Value_Start (Source, Line_Start);
VE : constant Positive :=
UCD_Format_Spec.Value_End (Source, Line_Start);
begin
(if VS = 0 or else VE <= VS then 0
else
(declare
TV : constant Positive :=
UCD_Format_Spec.Trim_Spaces_End (Source, VS, VE);
begin
(if TV <= VS then 0
else Ghost_Match_Index (Source, VS, TV - VS,
Names, Num_Values, 1)))))
with Ghost,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then UCD_Format_Spec.Is_Data_Line (Source, Line_Start)
and then Num_Values >= 1,
Post => Line_Value_Index'Result in 0 .. Num_Values;
-- What value should Table(CP) contain after processing all lines
-- from position Pos forward?
--
-- Semantics: process lines in order. If a data line covers CP and
-- its value matches a Names entry (index I > 0), set Table(CP) = I.
-- Later assignments overwrite earlier ones. If no line assigns CP,
-- the result is Default_Index (0).
--
-- This recurses forward through lines. Later lines take precedence:
-- we check the recursive result first, and only use the current line's
-- match if no later line overwrites it.
function Expected_Value
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
Names : Value_Name_Array;
Num_Values : Property_Index) return Property_Index
is (if Pos > Source'Last then Default_Index
elsif UCD_Format_Spec.Is_Data_Line (Source, Pos)
and then UCD_Format_Spec.Line_Covers_CP (Source, Pos, CP)
then
(declare
I : constant Property_Index :=
Line_Value_Index (Source, Pos, Names, Num_Values);
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Source, Pos);
Rest : constant Property_Index :=
(if NL > Source'Last then Default_Index
else Expected_Value (Source, NL, CP, Names, Num_Values));
begin
(if Rest /= Default_Index then Rest
elsif I > 0 then I
else Default_Index))
else
(declare
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Source, Pos);
begin
(if NL > Source'Last then Default_Index
else Expected_Value (Source, NL, CP, Names, Num_Values))))
with Ghost,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then Num_Values >= 1,
Subprogram_Variant =>
(Decreases => Source'Last - Pos),
Post => Expected_Value'Result in 0 .. Num_Values;
-- Boundary-safe wrapper: what should Table(CP) be for lines from Pos
-- forward? Returns Default_Index when Pos > Source'Last (no more lines).
function Expected_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
Names : Value_Name_Array;
Num_Values : Property_Index) return Property_Index
is (if Pos > Source'Last then Default_Index
else Expected_Value (Source, Pos, CP, Names, Num_Values))
with Ghost,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Num_Values >= 1,
Post => Expected_From'Result in 0 .. Num_Values;
---------------------------------------------------------------------------
-- Runtime line-scanning helpers
--
-- These runtime functions mirror UCD_Format_Spec ghost functions with
-- proved equivalence postconditions. They are exposed publicly so
-- other modules (e.g. Scx_Parser) can consume them without re-proving
-- the basic UCD line format.
---------------------------------------------------------------------------
-- Skip field-spaces forward on the current line. Returns the position
-- of the first non-space byte, or 0 if only spaces precede a line-end
-- or end-of-source.
--
-- Proved equivalent to UCD_Format_Spec.Skip_Spaces.
function Skip_WS
(Source : Byte_Array;
Pos : Positive) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => (if Skip_WS'Result > 0 then
Skip_WS'Result in Pos .. Source'Last
and then not Is_Field_Space (Source (Skip_WS'Result))
and then not Is_Line_End (Source (Skip_WS'Result)))
and then Skip_WS'Result =
UCD_Format_Spec.Skip_Spaces (Source, Pos);
-- Find the first semicolon on the current line, or 0 if none before
-- line-end.
--
-- Proved equivalent to UCD_Format_Spec.Find_Semicolon.
function Find_Semi
(Source : Byte_Array;
Pos : Positive) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => (if Find_Semi'Result > 0 then
Find_Semi'Result in Pos .. Source'Last
and then Source (Find_Semi'Result) = Semicolon_Byte)
and then Find_Semi'Result =
UCD_Format_Spec.Find_Semicolon (Source, Pos);
-- Parse a 4..6 digit hex codepoint at Pos. Returns the parsed value
-- (CP) and the number of hex digits consumed (Len). Len = 0 means
-- the first byte is not a hex digit.
--
-- Proved equivalent to UCD_Format_Spec.Parse_Hex_4/5/6 (per Len).
procedure Parse_CP
(Source : Byte_Array;
Pos : Positive;
CP : out Natural;
Len : out Natural)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => Len <= 6
and then (if Len >= 4 then
Pos + Len - 1 <= Source'Last)
and then (if Len = 0 then
not Is_Hex_Digit (Source (Pos)))
and then (if Len >= 1 then
Is_Hex_Digit (Source (Pos)))
and then (if Len >= 2 then
Pos + 1 <= Source'Last
and then Is_Hex_Digit (Source (Pos + 1)))
and then (if Len >= 3 then
Pos + 2 <= Source'Last
and then Is_Hex_Digit (Source (Pos + 2)))
and then (if Len >= 4 then
Is_Hex_Digit (Source (Pos + 3)))
and then (if Len >= 5 then
Pos + 4 <= Source'Last
and then Is_Hex_Digit (Source (Pos + 4)))
and then (if Len >= 6 then
Pos + 5 <= Source'Last
and then Is_Hex_Digit (Source (Pos + 5)))
and then (if Len >= 1 and then Len <= 5
and then Pos + Len <= Source'Last
then not Is_Hex_Digit (Source (Pos + Len)))
and then (if Len = 4 then
CP = UCD_Format_Spec.Parse_Hex_4 (Source, Pos))
and then (if Len = 5 then
CP = UCD_Format_Spec.Parse_Hex_5 (Source, Pos))
and then (if Len = 6 then
CP = UCD_Format_Spec.Parse_Hex_6 (Source, Pos));
-- Find the start of the next line (position after LF), or Source'Last+1
-- if at end-of-source.
--
-- Proved equivalent to UCD_Format_Spec.Next_Line_Start.
function Next_Line
(Source : Byte_Array;
Pos : Positive) return Positive
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => Next_Line'Result > Pos
and then Next_Line'Result <= Source'Last + 1
and then Next_Line'Result =
UCD_Format_Spec.Next_Line_Start (Source, Pos);
-- Find the end of the value field (position of '#', LF, CR, or
-- Source'Last + 1 if none).
--
-- Proved equivalent to UCD_Format_Spec.Find_Value_End.
function Find_Val_End
(Source : Byte_Array;
Pos : Positive) return Positive
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => Find_Val_End'Result in Pos .. Source'Last + 1
and then Find_Val_End'Result =
UCD_Format_Spec.Find_Value_End (Source, Pos);
-- Trim trailing spaces from a byte range [First .. Last-1]. Returns
-- the new Last (position after the last non-space byte).
--
-- Proved equivalent to UCD_Format_Spec.Trim_Spaces_End.
function Trim_Trailing
(Source : Byte_Array;
First : Positive;
Last : Positive) return Positive
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then First in Source'Range
and then Last in First .. Source'Last + 1,
Post => Trim_Trailing'Result in First .. Last
and then Trim_Trailing'Result =
UCD_Format_Spec.Trim_Spaces_End (Source, First, Last);
---------------------------------------------------------------------------
-- Ghost lemmas linking runtime Parse_CP output to the ghost
-- Hex_Digit_Count function. Exposed so other parsers (e.g. Scx_Parser)
-- can establish Is_Data_Line after calling Parse_CP.
---------------------------------------------------------------------------
-- If Parse_CP reports Len hex digits at Pos (with the byte at Pos+Len
-- either past end or not a hex digit), then the ghost Hex_Digit_Count
-- equals Len. Proved by induction on Len.
procedure Lemma_Hex_Digit_Count
(Source : Byte_Array;
Pos : Positive;
Len : Natural)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Len),
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then Len in 1 .. 6
and then Source'Last - Pos >= Len - 1
and then Is_Hex_Digit (Source (Pos))
and then (if Len >= 2 then
Is_Hex_Digit (Source (Pos + 1)))
and then (if Len >= 3 then
Is_Hex_Digit (Source (Pos + 2)))
and then (if Len >= 4 then
Is_Hex_Digit (Source (Pos + 3)))
and then (if Len >= 5 then
Is_Hex_Digit (Source (Pos + 4)))
and then (if Len >= 6 then
Is_Hex_Digit (Source (Pos + 5)))
and then (Pos + Len > Source'Last
or else not Is_Hex_Digit (Source (Pos + Len))),
Post => UCD_Format_Spec.Hex_Digit_Count (Source, Pos) = Len;
-- If there are at least 7 consecutive hex digits at Pos, then
-- Hex_Digit_Count >= 7 (hence not in 4..6 — used to reject
-- oversized codepoints in range detection).
procedure Lemma_HDC_GT_6
(Source : Byte_Array;
Pos : Positive)
with Ghost,
Always_Terminates,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then Source'Last - Pos >= 6
and then Is_Hex_Digit (Source (Pos))
and then Is_Hex_Digit (Source (Pos + 1))
and then Is_Hex_Digit (Source (Pos + 2))
and then Is_Hex_Digit (Source (Pos + 3))
and then Is_Hex_Digit (Source (Pos + 4))
and then Is_Hex_Digit (Source (Pos + 5))
and then Is_Hex_Digit (Source (Pos + 6)),
Post => UCD_Format_Spec.Hex_Digit_Count (Source, Pos) >= 7;
---------------------------------------------------------------------------
-- Parse a standard UCD property file.
--
-- Source: The embedded UCD file as a Byte_Array (Source'First = 1).
-- Names: Known property value names as byte ranges into Source.
-- Num_Values: Number of valid entries in Names (1 .. Num_Values).
-- Table: Output: flat property lookup table.
-- Success: True if all data lines matched a known value name.
--
-- The parser scans Source line by line:
-- - Comment lines (first non-space is '#') and blank lines are skipped
-- - Data lines: extract codepoint/range and value field, match value
-- against Names entries, populate Table for the covered codepoints
-- - If a value doesn't match any name, Success is set to False
--
-- On entry, all Table entries are Default_Index (0).
-- After parsing, each codepoint's entry is either:
-- - Default_Index (0) if no data line covers it, or
-- - The matched Property_Index for the value from the data line
---------------------------------------------------------------------------
procedure Parse_Property_File
(Source : Byte_Array;
Names : Value_Name_Array;
Num_Values : Property_Index;
Table : out Property_Table;
Success : out Boolean)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Source'Length > 0
and then Num_Values >= 1,
Post => -- Safety: every table entry is in range
(for all CP in Codepoint =>
Table (CP) in 0 .. Num_Values)
-- Correctness: every table entry matches the specification
and then
(for all CP in Codepoint =>
Table (CP) = Expected_Value
(Source, 1, CP, Names, Num_Values));
---------------------------------------------------------------------------
-- Extract unique value names from a UCD property file.
--
-- Scans Source line by line. For each data line, extracts the value
-- field (after the semicolon, trimmed). If the value hasn't been seen
-- before, appends it to Names.
--
-- Output:
-- Names (1 .. Num_Values): each entry's First/Last point to the value
-- string's byte range in Source.
-- Num_Values: number of unique values found.
-- Success: False if more than Max_Value_Names unique values found,
-- or if no data lines found.
--
-- This procedure does not require a ghost correctness spec. Its output
-- is validated transitively: if any value in the file is missing from
-- Names, Parse_Property_File will set its Success to False for that line.
---------------------------------------------------------------------------
procedure Extract_Value_Names
(Source : Byte_Array;
Names : out Value_Name_Array;
Num_Values : out Property_Index;
Success : out Boolean)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Source'Length > 0,
Post => -- Every name entry points to valid bytes in Source
(for all I in 1 .. Num_Values =>
Names (I).First in Source'Range
and then Names (I).Last in Source'Range
and then Names (I).Last >= Names (I).First);
end Lingenic_Text.UCD_Parser;