-- 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
--
-- UCD property file parser implementation.
--
-- Scans the source buffer line by line. For each data line:
-- 1. Extract codepoint or range from field 0
-- 2. Extract value string from field 1
-- 3. Match value against known property value names
-- 4. Populate the table for the covered codepoint(s)
--
-- Comment lines (first non-space is '#') and blank lines are skipped.
--
-- Every runtime helper's postcondition proves equivalence with the
-- corresponding ghost spec function. This chain of equivalences feeds
-- into the main loop's correctness invariant, which connects Table entries
-- to Expected_Value.
-------------------------------------------------------------------------------
package body Lingenic_Text.UCD_Parser
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Internal: Skip whitespace forward on the current line.
-- Returns 0 if no non-space found before line end.
--
-- Ghost equivalence: result = Skip_Spaces (Source, Pos)
---------------------------------------------------------------------------
function Skip_WS
(Source : Byte_Array;
Pos : Positive) return Natural
is
P : Positive := Pos;
begin
loop
if Is_Line_End (Source (P)) then
return 0;
elsif not Is_Field_Space (Source (P)) then
return P;
elsif P = Source'Last then
return 0;
else
P := P + 1;
end if;
pragma Loop_Invariant (P in Pos + 1 .. Source'Last);
pragma Loop_Invariant
(UCD_Format_Spec.Skip_Spaces (Source, Pos) =
UCD_Format_Spec.Skip_Spaces (Source, P));
pragma Loop_Variant (Increases => P);
end loop;
end Skip_WS;
---------------------------------------------------------------------------
-- Internal: Find semicolon on the current line.
-- Returns 0 if not found.
--
-- Ghost equivalence: result = Find_Semicolon (Source, Pos)
---------------------------------------------------------------------------
function Find_Semi
(Source : Byte_Array;
Pos : Positive) return Natural
is
P : Positive := Pos;
begin
loop
if Is_Line_End (Source (P)) then
return 0;
elsif Source (P) = Semicolon_Byte then
return P;
elsif P = Source'Last then
return 0;
else
P := P + 1;
end if;
pragma Loop_Invariant (P in Pos + 1 .. Source'Last);
pragma Loop_Invariant
(UCD_Format_Spec.Find_Semicolon (Source, Pos) =
UCD_Format_Spec.Find_Semicolon (Source, P));
pragma Loop_Variant (Increases => P);
end loop;
end Find_Semi;
---------------------------------------------------------------------------
-- Internal: Parse hex codepoint at Pos. Returns the parsed value and
-- the number of hex digits consumed.
---------------------------------------------------------------------------
procedure Parse_CP
(Source : Byte_Array;
Pos : Positive;
CP : out Natural;
Len : out Natural)
is
P : Positive := Pos;
Val : Natural;
begin
Len := 0;
-- Phase 1: Count consecutive hex digits
loop
exit when P > Source'Last;
exit when not Is_Hex_Digit (Source (P));
if Len >= 6 then
pragma Assert (Pos + Len - 1 <= Source'Last);
exit;
end if;
pragma Assert (P = Pos + Len);
pragma Assert (Is_Hex_Digit (Source (Pos + Len)));
Len := Len + 1;
pragma Assert (Pos + Len - 1 <= Source'Last);
exit when P = Source'Last;
P := P + 1;
pragma Loop_Invariant (Len in 1 .. 6);
pragma Loop_Invariant (P = Pos + Len);
pragma Loop_Invariant (Pos + Len - 1 <= Source'Last);
-- Per-byte hex digit invariants (enumerated, no quantifier)
pragma Loop_Invariant (Is_Hex_Digit (Source (Pos)));
pragma Loop_Invariant
(if Len >= 2 then Is_Hex_Digit (Source (Pos + 1)));
pragma Loop_Invariant
(if Len >= 3 then Is_Hex_Digit (Source (Pos + 2)));
pragma Loop_Invariant
(if Len >= 4 then Is_Hex_Digit (Source (Pos + 3)));
pragma Loop_Invariant
(if Len >= 5 then Is_Hex_Digit (Source (Pos + 4)));
pragma Loop_Invariant
(if Len >= 6 then Is_Hex_Digit (Source (Pos + 5)));
pragma Loop_Variant (Increases => P);
end loop;
-- Phase 2: Compute value from counted digits using direct formula.
-- This matches the ghost Parse_Hex_N functions exactly.
if Len = 4 then
Val := Hex_Value (Source (Pos)) * 4096
+ Hex_Value (Source (Pos + 1)) * 256
+ Hex_Value (Source (Pos + 2)) * 16
+ Hex_Value (Source (Pos + 3));
elsif Len = 5 then
Val := Hex_Value (Source (Pos)) * 65536
+ Hex_Value (Source (Pos + 1)) * 4096
+ Hex_Value (Source (Pos + 2)) * 256
+ Hex_Value (Source (Pos + 3)) * 16
+ Hex_Value (Source (Pos + 4));
elsif Len = 6 then
Val := Hex_Value (Source (Pos)) * 1048576
+ Hex_Value (Source (Pos + 1)) * 65536
+ Hex_Value (Source (Pos + 2)) * 4096
+ Hex_Value (Source (Pos + 3)) * 256
+ Hex_Value (Source (Pos + 4)) * 16
+ Hex_Value (Source (Pos + 5));
else
Val := 0;
end if;
CP := Val;
end Parse_CP;
---------------------------------------------------------------------------
-- Internal: Find the start of the next line (after LF).
-- Returns Source'Last + 1 if at end of buffer.
--
-- Ghost equivalence: result = Next_Line_Start (Source, Pos)
---------------------------------------------------------------------------
function Next_Line
(Source : Byte_Array;
Pos : Positive) return Positive
is
P : Positive := Pos;
begin
loop
if Source (P) = LF_Byte then
if P < Source'Last then
return P + 1;
else
return Source'Last + 1;
end if;
elsif P = Source'Last then
return Source'Last + 1;
else
P := P + 1;
end if;
pragma Loop_Invariant (P in Pos + 1 .. Source'Last);
pragma Loop_Invariant
(UCD_Format_Spec.Next_Line_Start (Source, Pos) =
UCD_Format_Spec.Next_Line_Start (Source, P));
pragma Loop_Variant (Increases => P);
end loop;
end Next_Line;
---------------------------------------------------------------------------
-- Internal: Find end of value field (position of '#', LF, CR, or past
-- end).
--
-- Ghost equivalence: result = Find_Value_End (Source, Pos)
---------------------------------------------------------------------------
function Find_Val_End
(Source : Byte_Array;
Pos : Positive) return Positive
is
P : Positive := Pos;
begin
loop
if Source (P) = Hash_Byte or else Is_Line_End (Source (P)) then
return P;
elsif P = Source'Last then
return Source'Last + 1;
else
P := P + 1;
end if;
pragma Loop_Invariant (P in Pos + 1 .. Source'Last);
pragma Loop_Invariant
(UCD_Format_Spec.Find_Value_End (Source, Pos) =
UCD_Format_Spec.Find_Value_End (Source, P));
pragma Loop_Variant (Increases => P);
end loop;
end Find_Val_End;
---------------------------------------------------------------------------
-- Internal: Trim trailing spaces from a range [First .. Last-1].
-- Returns the new Last (position after last non-space).
--
-- Ghost equivalence: result = Trim_Spaces_End (Source, First, Last)
---------------------------------------------------------------------------
function Trim_Trailing
(Source : Byte_Array;
First : Positive;
Last : Positive) return Positive
is
P : Positive := Last;
begin
loop
exit when P = First;
exit when not Is_Field_Space (Source (P - 1));
P := P - 1;
pragma Loop_Invariant (P in First .. Last);
pragma Loop_Invariant
(UCD_Format_Spec.Trim_Spaces_End (Source, First, Last) =
UCD_Format_Spec.Trim_Spaces_End (Source, First, P));
pragma Loop_Variant (Decreases => P);
end loop;
return P;
end Trim_Trailing;
---------------------------------------------------------------------------
-- Ghost lemma: if all bytes in [A..A+Len-1] equal [B..B+Len-1]
-- pointwise, then Bytes_Equal holds.
---------------------------------------------------------------------------
-- Ghost lemma: extend Bytes_Equal by one byte at the front.
-- If S(A)=S(B) and Bytes_Equal(S, A+1, B+1, Len), then
-- Bytes_Equal(S, A, B, Len+1).
--
-- This follows directly from Bytes_Equal's definition — the solver
-- just needs the assertion chain.
procedure Lemma_Bytes_Equal_Extend
(Source : Byte_Array;
A_First : Positive;
B_First : Positive;
Len : Natural)
with Ghost,
Always_Terminates,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then A_First in Source'Range
and then B_First in Source'Range
and then Source'Last - A_First >= Len
and then Source'Last - B_First >= Len
and then Source (A_First) = Source (B_First)
and then UCD_Format_Spec.Bytes_Equal
(Source, A_First + 1, B_First + 1, Len),
Post => UCD_Format_Spec.Bytes_Equal
(Source, A_First, B_First, Len + 1)
is
begin
null; -- Follows from unfolding Bytes_Equal one level
end Lemma_Bytes_Equal_Extend;
---------------------------------------------------------------------------
-- Ghost lemma: if there exists a position K where bytes differ,
-- then Bytes_Equal is False.
---------------------------------------------------------------------------
procedure Lemma_Not_Bytes_Equal
(Source : Byte_Array;
A_First : Positive;
B_First : Positive;
Len : Positive;
Diff : Natural)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Diff),
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then A_First in Source'Range
and then B_First in Source'Range
and then Source'Last - A_First >= Len - 1
and then Source'Last - B_First >= Len - 1
and then Diff < Len
and then Source (A_First + Diff) /= Source (B_First + Diff),
Post => not UCD_Format_Spec.Bytes_Equal
(Source, A_First, B_First, Len)
is
begin
if Diff = 0 then
-- First byte differs: Bytes_Equal(S, A, B, Len) starts with
-- S(A) = S(B) which is False.
null;
else
-- Diff > 0: first bytes might be equal, but there's a diff deeper.
-- Bytes_Equal(S, A, B, Len) = S(A)=S(B) and Bytes_Equal(S,A+1,B+1,Len-1)
-- We prove the recursive part is False.
Lemma_Not_Bytes_Equal
(Source, A_First + 1, B_First + 1, Len - 1, Diff - 1);
end if;
end Lemma_Not_Bytes_Equal;
---------------------------------------------------------------------------
-- Internal: Match a value field against known names.
-- Returns the matched index, or 0 if no match.
--
-- Ghost equivalence: result = Ghost_Match_Index(Source, Val_First,
-- Val_Last - Val_First, Names, Num_Values, 1)
---------------------------------------------------------------------------
function Match_Value
(Source : Byte_Array;
Val_First : Positive;
Val_Last : Positive; -- position AFTER last char
Names : Value_Name_Array;
Num_Values : Property_Index) return Property_Index
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Val_First in Source'Range
and then Val_Last in Val_First .. Source'Last + 1
and then Num_Values >= 1,
Post => Match_Value'Result in 0 .. Num_Values
and then Match_Value'Result =
Ghost_Match_Index (Source, Val_First,
Val_Last - Val_First,
Names, Num_Values, 1)
is
Val_Len : constant Natural := Val_Last - Val_First;
begin
if Val_Len = 0 then
-- GMI with Val_Len=0: Ghost_Match always False (requires Val_Len>0)
pragma Assert
(Ghost_Match_Index (Source, Val_First, 0,
Names, Num_Values, 1) = 0);
return 0;
end if;
for I in 1 .. Num_Values loop
if Names (I).Last >= Names (I).First
and then Names (I).First in Source'Range
and then Names (I).Last in Source'Range
then
declare
Name_Len : constant Natural :=
Names (I).Last - Names (I).First + 1;
begin
if Name_Len = Val_Len then
-- Compare byte by byte from the END and build
-- Bytes_Equal simultaneously.
--
-- By scanning in reverse, each step either:
-- (a) confirms S(VF+K)=S(NF+K) and extends
-- Bytes_Equal(S, VF+K, NF+K, Name_Len-K), or
-- (b) finds a mismatch, proving not Bytes_Equal.
--
-- This avoids the quantifier shift problem entirely.
declare
NF : constant Positive := Names (I).First;
Match : Boolean := True;
begin
for K in reverse 0 .. Name_Len - 1 loop
if Source (Val_First + K) /= Source (NF + K) then
Match := False;
-- Mismatch at K: prove not Bytes_Equal for whole
Lemma_Not_Bytes_Equal
(Source, Val_First, NF, Name_Len, K);
exit;
end if;
-- S(VF+K) = S(NF+K) confirmed.
-- Extend: from BE_Tail = Bytes_Equal(S,VF+K+1,NF+K+1,
-- Name_Len-K-1) and the byte equality,
-- we get Bytes_Equal(S, VF+K, NF+K, Name_Len-K).
Lemma_Bytes_Equal_Extend
(Source, Val_First + K, NF + K,
Name_Len - K - 1);
pragma Loop_Invariant (Match);
pragma Loop_Invariant
(UCD_Format_Spec.Bytes_Equal
(Source, Val_First + K, NF + K,
Name_Len - K));
pragma Loop_Variant (Decreases => K);
end loop;
if Match then
-- After K=0: Bytes_Equal(S, VF, NF, Name_Len)
pragma Assert
(Ghost_Match
(Source, Val_First, Val_Len, Names, I));
-- Ghost_Match_Index unfolds: GM(I) is True, so
-- GMI(S, VF, VL, Names, NV, I) = I.
pragma Assert
(Ghost_Match_Index
(Source, Val_First, Val_Len,
Names, Num_Values, I) = I);
return I;
end if;
-- Mismatch branch already called Lemma_Not_Bytes_Equal.
end;
end if;
end;
end if;
-- We did NOT return I, so Ghost_Match must be False.
-- Cases: Names conditions fail, or length mismatch, or byte mismatch.
-- For length/Names failures, Ghost_Match's conjuncts are trivially False.
-- For byte mismatch: we need help — skip the assertion for now and
-- let the GMI invariant handle it by unfolding.
-- Key insight: Ghost_Match_Index unfolds to check Ghost_Match(I).
-- If GM(I) is True, GMI returns I. Since we didn't return I,
-- the only way is GM(I) = False. The solver may need help here.
pragma Assert
(not Ghost_Match (Source, Val_First, Val_Len, Names, I));
-- No match at entry I: GMI from 1 = GMI from I+1.
pragma Loop_Invariant
(Ghost_Match_Index (Source, Val_First, Val_Len,
Names, Num_Values, 1) =
(if I < Num_Values
then Ghost_Match_Index (Source, Val_First, Val_Len,
Names, Num_Values, I + 1)
else 0));
end loop;
pragma Assert
(Ghost_Match_Index (Source, Val_First, Val_Len,
Names, Num_Values, 1) = 0);
return 0;
end Match_Value;
---------------------------------------------------------------------------
-- Ghost lemma: one-step transfer of the correctness invariant.
--
-- Given:
-- - The invariant holds at Pos (for all CP, EF(1,CP) decomposes
-- through EF(Pos,CP) and Table(CP))
-- - Table was updated according to what the parser does for the
-- line at Pos (for covering CPs: Table(CP) = matched value;
-- for non-covering CPs: Table(CP) unchanged)
-- - NL = Next_Line_Start(Source, Pos)
--
-- Proves:
-- - The invariant holds at NL
--
-- The body unfolds Expected_Value one level at Pos, which the solver
-- can see because Expected_Value is an expression function.
---------------------------------------------------------------------------
pragma Warnings (Off, "is not referenced");
procedure Lemma_Invariant_Step
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint;
Names : Value_Name_Array;
Num_Values : Property_Index;
Table_CP : Property_Index;
Old_Table_CP : Property_Index)
with Ghost,
Always_Terminates,
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range
and then Num_Values >= 1
and then Table_CP in 0 .. Num_Values
and then Old_Table_CP in 0 .. Num_Values
-- Old invariant at Pos:
and then
Expected_From (Source, 1, CP, Names, Num_Values) =
(if Expected_From (Source, Pos, CP, Names, Num_Values)
/= Default_Index
then Expected_From (Source, Pos, CP, Names, Num_Values)
else Old_Table_CP)
-- Table update: if the line covers CP and matched, Table
-- got the value; otherwise Table is unchanged.
and then
(if UCD_Format_Spec.Is_Data_Line (Source, Pos)
and then UCD_Format_Spec.Line_Covers_CP
(Source, Pos, CP)
then
(declare
LVI : constant Property_Index :=
Line_Value_Index (Source, Pos, Names, Num_Values);
begin
(if LVI > 0 then Table_CP = LVI
else Table_CP = Old_Table_CP))
else
Table_CP = Old_Table_CP),
Post =>
(declare
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Source, Pos);
begin
Expected_From (Source, 1, CP, Names, Num_Values) =
(if Expected_From (Source, NL, CP, Names, Num_Values)
/= Default_Index
then Expected_From (Source, NL, CP, Names, Num_Values)
else Table_CP))
is
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Source, Pos) with Ghost;
begin
-- Unfold Expected_Value(S, Pos, CP, ...) one level.
-- EV(S, Pos, CP, ...) is an expression function; the solver sees
-- its body:
--
-- Case A: Is_Data_Line(S, Pos) and Line_Covers_CP(S, Pos, CP)
-- EV = if Rest /= 0 then Rest
-- elsif Line_Value_Index(S, Pos, ...) > 0
-- then Line_Value_Index(S, Pos, ...)
-- else 0
-- where Rest = EF(S, NL, CP, ...)
--
-- Case B: otherwise
-- EV = EF(S, NL, CP, ...)
--
-- From the old invariant:
-- EF(1, CP) = if EV /= 0 then EV else Old_Table_CP
--
-- We need:
-- EF(1, CP) = if Rest /= 0 then Rest else Table_CP
if UCD_Format_Spec.Is_Data_Line (Source, Pos)
and then UCD_Format_Spec.Line_Covers_CP (Source, Pos, CP)
then
-- Case A: data line covering CP
declare
LVI : constant Property_Index :=
Line_Value_Index (Source, Pos, Names, Num_Values);
Rest : constant Property_Index :=
Expected_From (Source, NL, CP, Names, Num_Values);
EV : constant Property_Index :=
Expected_Value (Source, Pos, CP, Names, Num_Values);
begin
-- EV = if Rest /= 0 then Rest elsif LVI > 0 then LVI else 0
-- From old invariant: EF(1,CP) = if EV /= 0 then EV else OT
--
-- Sub-case A1: Rest /= 0
-- EV = Rest /= 0, so EF(1,CP) = EV = Rest
-- Target: if Rest /= 0 then Rest else T => Rest ✓
--
-- Sub-case A2: Rest = 0, LVI > 0
-- EV = LVI /= 0, so EF(1,CP) = EV = LVI
-- Table_CP = LVI (from precondition)
-- Target: if 0 /= 0 then 0 else LVI => LVI ✓
--
-- Sub-case A3: Rest = 0, LVI = 0
-- EV = 0, so EF(1,CP) = OT
-- Table_CP = OT (from precondition, LVI=0 case)
-- Target: if 0 /= 0 then 0 else OT => OT ✓
-- Help the solver see the unfolding:
pragma Assert (EV =
(if Rest /= Default_Index then Rest
elsif LVI > Default_Index then LVI
else Default_Index));
null;
end;
else
-- Case B: not a data line covering CP
-- EV = EF(S, NL, CP, ...) = Rest
-- From old invariant: EF(1,CP) = if EV /= 0 then EV else OT
-- = if Rest /= 0 then Rest else OT
-- Table_CP = OT (unchanged)
-- Target: if Rest /= 0 then Rest else OT ✓
null;
end if;
end Lemma_Invariant_Step;
pragma Warnings (On, "is not referenced");
---------------------------------------------------------------------------
-- Parse_Property_File
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Ghost lemma: Hex_Digit_Count(Source, Pos) = Len when:
-- (1) there are exactly Len consecutive hex digits at Pos
-- (2) either the next position is past the end OR not a hex digit
--
-- This connects the runtime Parse_CP output (Len) to the ghost
-- Hex_Digit_Count. Proved by induction on Len.
---------------------------------------------------------------------------
procedure Lemma_Hex_Digit_Count
(Source : Byte_Array;
Pos : Positive;
Len : Natural)
is
begin
if Len = 1 then
null;
else
Lemma_Hex_Digit_Count (Source, Pos + 1, Len - 1);
end if;
end Lemma_Hex_Digit_Count;
---------------------------------------------------------------------------
-- Ghost lemma: Hex_Digit_Count(Source, Pos) >= 7 when there are at
-- least 7 consecutive hex digits starting at Pos.
--
-- This is needed for the >6-digit case in range detection: when
-- Parse_CP returns Hex_Len2 = 6 but there's still a hex digit at
-- Pos+6, the real Hex_Digit_Count is > 6, hence not in 4..6.
--
-- Proved by unfolding Hex_Digit_Count 7 times. At each step,
-- Is_Hex_Digit(Source(Pos+K)) is True and Pos+K < Source'Last,
-- so HDC(S, Pos+K) = 1 + HDC(S, Pos+K+1). After 7 steps:
-- HDC(S, Pos) = 7 + HDC(S, Pos+7) >= 7.
---------------------------------------------------------------------------
procedure Lemma_HDC_GT_6
(Source : Byte_Array;
Pos : Positive)
is
-- Unfold from the innermost position outward.
-- HDC(S, Pos+6) >= 1 because Is_Hex_Digit(Source(Pos+6)).
-- HDC(S, Pos+5) = 1 + HDC(S, Pos+6) >= 2.
-- ... and so on until HDC(S, Pos) >= 7.
begin
-- Step 1: HDC(S, Pos+6) >= 1
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 6) >= 1);
-- Step 2: Pos+5 < Source'Last (since Pos+6 <= Source'Last),
-- so HDC(S, Pos+5) = 1 + HDC(S, Pos+6) >= 2
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 5) >= 2);
-- Step 3:
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 4) >= 3);
-- Step 4:
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 3) >= 4);
-- Step 5:
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 2) >= 5);
-- Step 6:
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos + 1) >= 6);
-- Step 7:
pragma Assert
(UCD_Format_Spec.Hex_Digit_Count (Source, Pos) >= 7);
end Lemma_HDC_GT_6;
---------------------------------------------------------------------------
-- Ghost lemma: Find_Value_End skips over field spaces.
--
-- If Skip_Spaces(S, P) = Q > 0, then Find_Value_End(S, P) =
-- Find_Value_End(S, Q).
--
-- Proof: by induction on the distance from P to Q.
-- At each step P, Source(P) is a field space (not #, LF, CR),
-- so Find_Value_End recurses to P+1. Eventually P = Q.
---------------------------------------------------------------------------
procedure Lemma_Find_Value_End_Skip_Spaces
(Source : Byte_Array;
P : Positive;
Q : Positive)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Q - P),
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then P in Source'Range
and then Q in P .. Source'Last
and then UCD_Format_Spec.Skip_Spaces (Source, P) = Q
and then not Is_Field_Space (Source (Q)),
Post => UCD_Format_Spec.Find_Value_End (Source, P) =
UCD_Format_Spec.Find_Value_End (Source, Q)
is
begin
if P = Q then
null; -- Base case: P = Q, trivially equal.
else
-- P < Q. Skip_Spaces(S, P) = Q > P means Source(P) is a field
-- space (not line-end, not non-space).
-- Find_Value_End(S, P): Source(P) is space, not # or line-end,
-- and P /= Source'Last (since Q > P and Q <= Source'Last).
-- So Find_Value_End(S, P) = Find_Value_End(S, P+1).
-- Also Skip_Spaces(S, P+1) = Q (unfolding one step of Skip_Spaces).
-- By induction: Find_Value_End(S, P+1) = Find_Value_End(S, Q).
Lemma_Find_Value_End_Skip_Spaces (Source, P + 1, Q);
end if;
end Lemma_Find_Value_End_Skip_Spaces;
---------------------------------------------------------------------------
-- Ghost lemma: Ghost_Match_Index with Val_Len = 0 always returns 0.
--
-- Ghost_Match requires Val_Len > 0, so it's always False when Val_Len=0.
-- GMI checks Ghost_Match at each entry, finds False, recurses to next.
-- Induction on Num_Values - I.
---------------------------------------------------------------------------
procedure Lemma_GMI_Zero_Len
(Source : Byte_Array;
Val_First : Positive;
Names : Value_Name_Array;
Num_Values : Property_Index;
I : Property_Index)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Increases => I),
Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Num_Values >= 1
and then I >= 1,
Post => Ghost_Match_Index (Source, Val_First, 0,
Names, Num_Values, I) = 0
is
begin
if I > Num_Values then
null; -- Base: I > NV → GMI returns 0
elsif I = Num_Values then
-- GM(S, VF, 0, Names, I) is False (Val_Len=0, GM needs >0).
-- GMI: not GM, I = NV → 0.
null;
else
-- GM(S, VF, 0, Names, I) is False.
-- GMI(S, VF, 0, Names, NV, I) =
-- GMI(S, VF, 0, Names, NV, I+1)
Lemma_GMI_Zero_Len (Source, Val_First, Names, Num_Values, I + 1);
end if;
end Lemma_GMI_Zero_Len;
---------------------------------------------------------------------------
-- Process_Line: Extract codepoint(s) and value from one UCD data line,
-- update Table accordingly.
--
-- This is the core line-processing logic, extracted to give the prover
-- a clean postcondition about what happened to Table.
--
-- Postconditions:
-- 1. Range: all Table entries remain in 0..Num_Values
-- 2. Frame: entries NOT in the modified range are unchanged
-- 3. For entries IN the modified range: set to the matched value
---------------------------------------------------------------------------
procedure Process_Line
(Source : Byte_Array;
Line_Pos : Positive;
Names : Value_Name_Array;
Num_Values : Property_Index;
Table : in out Property_Table;
Success : in out Boolean)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Pos in Source'Range
and then Num_Values >= 1
and then (for all CP in Codepoint =>
Table (CP) in 0 .. Num_Values),
Post => -- Safety: all entries remain in range
(for all CP in Codepoint =>
Table (CP) in 0 .. Num_Values)
-- Ghost-spec correctness: each codepoint's table entry
-- reflects the data line's value (if it covers CP and
-- the value matches), or is unchanged.
and then
(for all CP in Codepoint =>
(declare
LVI : constant Property_Index :=
(if UCD_Format_Spec.Is_Data_Line (Source, Line_Pos)
and then UCD_Format_Spec.Line_Covers_CP
(Source, Line_Pos, CP)
then Line_Value_Index (Source, Line_Pos,
Names, Num_Values)
else 0);
begin
(if LVI > 0 then Table (CP) = LVI
else Table (CP) = Table'Old (CP))))
is
F0 : constant Natural := Skip_WS (Source, Line_Pos);
Semi : Natural;
-- Ghost copy of the initial table for assertions in the body.
-- (Table'Old is only available in postconditions, not in the body.)
Table_At_Entry : constant Property_Table := Table with Ghost;
begin
if F0 = 0 or else not Is_Hex_Digit (Source (F0)) then
-- Not a data line: Skip_Spaces = 0 or first non-space not hex.
-- Is_Data_Line is False, so LVI = 0 for all CP, so Table unchanged.
return;
end if;
Semi := Find_Semi (Source, Line_Pos);
if Semi = 0 then
-- No semicolon: not a data line.
return;
end if;
declare
CP1 : Natural;
Hex_Len : Natural;
begin
Parse_CP (Source, F0, CP1, Hex_Len);
if Hex_Len < 4 or else CP1 > Max_Codepoint
or else (F0 + Hex_Len <= Source'Last
and then Is_Hex_Digit (Source (F0 + Hex_Len)))
then
-- Bad hex field (< 4 digits, > max CP, or > 6 digits).
-- Hex_Digit_Count not in 4..6 so Is_Data_Line is False.
return;
end if;
-- At this point we know:
-- F0 = Skip_Spaces(Source, Line_Pos) > 0
-- Is_Hex_Digit(Source(F0))
-- Hex_Len in 4..6
-- F0 + Hex_Len - 1 <= Source'Last
-- The byte at F0 + Hex_Len is NOT hex (or past end)
-- Semi = Find_Semicolon(Source, Line_Pos) > 0
--
-- We need to establish: Hex_Digit_Count(Source, F0) = Hex_Len
-- so that Is_Data_Line(Source, Line_Pos) is True.
--
-- Use Lemma_Hex_Digit_Count, which needs individual hex digit
-- facts per byte position. Parse_CP gives us these enumerated.
-- === Ghost equivalence chain ===
--
-- Step 1: Hex_Digit_Count(Source, F0) = Hex_Len
Lemma_Hex_Digit_Count (Source, F0, Hex_Len);
-- Step 2: Is_Data_Line(Source, Line_Pos)
pragma Assert (UCD_Format_Spec.Is_Data_Line (Source, Line_Pos));
-- Step 3: CP1 = Line_First_CP(Source, Line_Pos)
-- Line_First_CP unfolds to Parse_Hex(S, F0, HC) where
-- HC = Hex_Digit_Count(S, F0) = Hex_Len.
-- Parse_Hex dispatches to Parse_Hex_N.
-- Parse_CP postcondition gives CP1 = Parse_Hex_N(S, F0).
pragma Assert
(CP1 = UCD_Format_Spec.Line_First_CP (Source, Line_Pos));
declare
Is_Range : Boolean := False;
CP2 : Natural := CP1;
After_Hex : constant Positive := F0 + Hex_Len;
begin
if After_Hex < Source'Last
and then Source (After_Hex) = Dot_Byte
and then Source (After_Hex + 1) = Dot_Byte
then
if After_Hex + 1 < Source'Last then
declare
CP2_Val : Natural;
Hex_Len2 : Natural;
P2 : constant Positive := After_Hex + 2;
begin
Parse_CP (Source, P2, CP2_Val, Hex_Len2);
if Hex_Len2 >= 4
-- Ensure stopping: no further hex digit after field.
and then (Hex_Len2 <= 5
or else P2 + Hex_Len2 > Source'Last
or else not Is_Hex_Digit
(Source (P2 + Hex_Len2)))
then
-- Valid range format (4-6 hex digits).
Is_Range := True;
-- Cap at Max_Codepoint for the loop bound.
-- Line_Covers_CP uses Line_Last_CP which may be
-- > Max_Codepoint, but the Codepoint type is
-- 0..Max_Codepoint so all valid CPs are covered.
CP2 := Natural'Min (CP2_Val, Max_Codepoint);
-- Step 4a: Connect Is_Range to Is_Range_Line
Lemma_Hex_Digit_Count (Source, P2, Hex_Len2);
pragma Assert
(UCD_Format_Spec.Is_Range_Line
(Source, Line_Pos));
-- Step 4b: Line_Last_CP = CP2_Val
pragma Assert
(UCD_Format_Spec.Line_Last_CP (Source, Line_Pos)
= CP2_Val);
else
-- Second hex field invalid (< 4 digits or > 6).
-- Hex_Digit_Count not in 4..6 → not Is_Range_Line.
if Hex_Len2 = 0 then
-- No hex digit at P2.
-- HDC(S, P2) = 0, not in 4..6.
pragma Assert
(not Is_Hex_Digit (Source (P2)));
elsif Hex_Len2 <= 3 then
-- 1-3 hex digits: HDC = Hex_Len2, not in 4..6.
Lemma_Hex_Digit_Count (Source, P2, Hex_Len2);
else
-- Hex_Len2 = 6 (since >= 4, <= 6 from Parse_CP,
-- and condition failed meaning Hex_Len2 > 5
-- i.e. Hex_Len2 = 6) with:
-- P2 + 6 <= Source'Last
-- Is_Hex_Digit(Source(P2 + 6))
-- So there are >= 7 consecutive hex digits.
pragma Assert (Hex_Len2 = 6);
pragma Assert (P2 + Hex_Len2 <= Source'Last);
pragma Assert
(Is_Hex_Digit (Source (P2 + Hex_Len2)));
Lemma_HDC_GT_6 (Source, P2);
end if;
pragma Assert
(not UCD_Format_Spec.Is_Range_Line
(Source, Line_Pos));
end if;
end;
else
-- After_Hex + 1 >= Source'Last: no room for second hex.
-- Source'Last - F0 < HC + 2, falsifying Is_Range_Line.
pragma Assert
(not UCD_Format_Spec.Is_Range_Line
(Source, Line_Pos));
end if;
else
-- No ".." found: Source(F0+HC) /= Dot_Byte or
-- Source(F0+HC+1) /= Dot_Byte or no room.
-- Directly falsifies Is_Range_Line's dot conditions.
pragma Assert
(not UCD_Format_Spec.Is_Range_Line
(Source, Line_Pos));
end if;
if Semi >= Source'Last then
-- Semi >= Source'Last: Value_Start returns 0.
-- Line_Value_Index: VS=0, so returns 0. LVI = 0.
-- Table unchanged → postcondition satisfied.
return;
end if;
declare
VS : constant Natural := Skip_WS (Source, Semi + 1);
begin
if VS = 0 then
-- Empty value field. Line_Value_Index: VS=0, returns 0.
return;
end if;
-- Step 5: VS = Value_Start(Source, Line_Pos)
-- Value_Start = (let Semi := Find_Semicolon(S, LP);
-- if Semi >= Source'Last then 0
-- else Skip_Spaces(S, Semi+1))
-- We have Semi < Source'Last and
-- VS = Skip_WS(S, Semi+1) = Skip_Spaces(S, Semi+1).
pragma Assert
(VS = UCD_Format_Spec.Value_Start (Source, Line_Pos));
declare
VE_Raw : constant Positive :=
Find_Val_End (Source, VS);
VE : constant Positive :=
Trim_Trailing (Source, VS, VE_Raw);
Idx : constant Property_Index :=
Match_Value (Source, VS, VE, Names, Num_Values);
begin
-- Step 6: VE_Raw = Find_Value_End(S, VS).
-- Ghost Value_End(S, LP) = Find_Value_End(S, Semi+1).
-- Bridge: Find_Value_End(S, Semi+1) = Find_Value_End(S, VS)
-- because spaces between Semi+1 and VS are not #/LF/CR.
--
-- VS > 0 from Skip_WS postcondition, which guarantees
-- not Is_Field_Space and not Is_Line_End at Source(VS).
Lemma_Find_Value_End_Skip_Spaces
(Source, Semi + 1, VS);
-- Now: Value_End(S, LP) = VE_Raw
pragma Assert
(UCD_Format_Spec.Value_End (Source, Line_Pos) = VE_Raw);
-- Step 7: Idx = Line_Value_Index
--
-- Line_Value_Index(S, LP, Names, NV) unfolds as:
-- let GSemi := Find_Semicolon(S, LP);
-- let GVS := if GSemi >= S'Last then 0
-- else Skip_Spaces(S, GSemi+1);
-- let GVE := if GSemi >= S'Last then S'Last+1
-- else Find_Value_End(S, GSemi+1);
-- if GVS = 0 or GVE <= GVS then 0
-- else let GTV := Trim_Spaces_End(S, GVS, GVE);
-- if GTV <= GVS then 0
-- else GMI(S, GVS, GTV-GVS, Names, NV, 1)
--
-- Restate key equalities close to the assertion:
pragma Assert
(Semi = UCD_Format_Spec.Find_Semicolon
(Source, Line_Pos));
pragma Assert (Semi < Source'Last);
-- So: GSemi = Semi, and Semi < Source'Last.
-- GVS = Skip_Spaces(S, Semi+1) = VS (from Step 5)
-- GVE = Find_Value_End(S, Semi+1) = VE_Raw (from Step 6)
pragma Assert
(UCD_Format_Spec.Trim_Spaces_End (Source, VS, VE_Raw)
= VE);
-- Now spell out the Line_Value_Index evaluation.
-- After substitution of established equalities:
-- GVS = VS /= 0, and VE_Raw >= VS (Find_Val_End >= VS)
-- LVI = if VS = 0 or else VE_Raw <= VS then 0
-- else if VE <= VS then 0
-- else GMI(S, VS, VE - VS, Names, NV, 1)
-- Case 1: VE_Raw <= VS — LVI = 0.
-- Find_Val_End returns >= VS, so VE_Raw >= VS.
-- If VE_Raw = VS, then Trim_Trailing returns VS, so VE = VS.
-- Then Match_Value with empty range returns 0, so Idx = 0.
-- Case 2: VE_Raw > VS.
-- If VE <= VS: GMI range is empty, Idx = 0.
-- If VE > VS: LVI = GMI(S, VS, VE-VS, ...) = Idx. ✓
--
-- In all cases: LVI = Idx.
--
-- Help the solver by asserting VE_Raw >= VS:
pragma Assert (VE_Raw >= VS);
-- Help: state what Line_Value_Index evaluates to
-- when GVS = VS, GVE = VE_Raw, GTV = VE:
pragma Assert
(Line_Value_Index (Source, Line_Pos, Names, Num_Values) =
(if VS = 0 or else VE_Raw <= VS then 0
elsif VE <= VS then 0
else Ghost_Match_Index
(Source, VS, VE - VS,
Names, Num_Values, 1)));
-- From the proved assertion (line 1008):
-- LVI = if VS=0 or VE_Raw<=VS then 0
-- elsif VE<=VS then 0
-- else GMI(S, VS, VE-VS, Names, NV, 1)
--
-- From Match_Value postcondition:
-- Idx = GMI(S, VS, VE - VS, Names, NV, 1)
--
-- We need: Idx = LVI.
--
-- The tricky case: VE_Raw <= VS or VE <= VS.
-- Then LVI = 0.
-- And VE - VS = 0 (since VE >= VS from Trim post).
-- Idx = GMI(S, VS, 0, Names, NV, 1).
-- Ghost_Match with Val_Len=0 is always False.
-- So GMI returns 0 at every step.
-- Help the solver with this Val_Len=0 case:
if VE = VS then
-- Val_Len = 0. GMI with length 0 always returns 0.
Lemma_GMI_Zero_Len
(Source, VS, Names, Num_Values, 1);
pragma Assert (Idx = 0);
end if;
pragma Assert
(Idx = Line_Value_Index
(Source, Line_Pos, Names, Num_Values));
if Idx = 0 then
Success := False;
return;
end if;
-- Key identity for Is_Range_Line unfolding:
-- After_Hex = F0 + Hex_Digit_Count(S, F0)
pragma Assert
(After_Hex = F0 +
UCD_Format_Spec.Hex_Digit_Count (Source, F0));
if Is_Range then
pragma Assert
(UCD_Format_Spec.Is_Range_Line (Source, Line_Pos));
for CP in CP1 .. CP2 loop
if CP <= Max_Codepoint then
Table (CP) := Idx;
end if;
pragma Loop_Invariant (Idx in 1 .. Num_Values);
pragma Loop_Invariant
(for all C in Codepoint =>
Table (C) in 0 .. Num_Values);
pragma Loop_Invariant
(for all C in Codepoint =>
(if C >= CP1 and then C <= CP
then Table (C) = Idx
else Table (C) = Table'Loop_Entry (C)));
end loop;
-- Reassert range facts for postcondition:
pragma Assert
(UCD_Format_Spec.Is_Range_Line (Source, Line_Pos));
-- CP2 = min(Line_Last_CP, Max_Codepoint).
-- Line_Last_CP >= CP2, so for Codepoint C
-- (0..Max_Codepoint): Line_Covers_CP(C)
-- ↔ C >= CP1 and C <= Line_Last_CP
-- ↔ C >= CP1 and C <= CP2 (since C <= Max_Codepoint
-- and CP2 = min(Line_Last_CP, Max_Codepoint)).
pragma Assert
(UCD_Format_Spec.Line_Last_CP (Source, Line_Pos)
>= CP2);
-- Bridge to postcondition: for range case,
-- Line_Covers_CP(S,LP,C) ↔ (C >= CP1 and C <= CP2).
-- After loop: Table(C) = Idx for covering CPs,
-- Table(C) = Table_At_Entry(C) for others.
pragma Assert
(for all C in Codepoint =>
(declare
LVI : constant Property_Index :=
(if UCD_Format_Spec.Is_Data_Line
(Source, Line_Pos)
and then UCD_Format_Spec.Line_Covers_CP
(Source, Line_Pos, C)
then Line_Value_Index
(Source, Line_Pos,
Names, Num_Values)
else 0);
begin
(if LVI > 0 then Table (C) = LVI
else Table (C) = Table_At_Entry (C))));
else
pragma Assert
(not UCD_Format_Spec.Is_Range_Line
(Source, Line_Pos));
-- Line_Covers_CP(S, LP, C) simplifies to
-- C = Line_First_CP(S, LP) = CP1.
pragma Assert
(for all C in Codepoint =>
(UCD_Format_Spec.Line_Covers_CP
(Source, Line_Pos, C)
= (C = CP1)));
Table (CP1) := Idx;
-- Bridge to postcondition: for single case,
-- Table(CP1) = Idx = LVI, rest unchanged.
pragma Assert
(for all C in Codepoint =>
(declare
LVI : constant Property_Index :=
(if UCD_Format_Spec.Is_Data_Line
(Source, Line_Pos)
and then UCD_Format_Spec.Line_Covers_CP
(Source, Line_Pos, C)
then Line_Value_Index
(Source, Line_Pos,
Names, Num_Values)
else 0);
begin
(if LVI > 0 then Table (C) = LVI
else Table (C) = Table_At_Entry (C))));
end if;
end;
end;
end;
end;
end Process_Line;
---------------------------------------------------------------------------
-- Extract_Value_Names
--
-- Scans Source line by line to discover all unique value names.
-- For each data line, extracts the value field and checks if it's
-- already in Names. If not, appends it.
---------------------------------------------------------------------------
procedure Extract_Value_Names
(Source : Byte_Array;
Names : out Value_Name_Array;
Num_Values : out Property_Index;
Success : out Boolean)
is
Line_Pos : Positive := 1;
Found_Any : Boolean := False;
begin
Names := [others => (First => 1, Last => 0)];
Num_Values := 0;
Success := True;
while Line_Pos <= Source'Last loop
-- Check if this is a data line: first non-space is hex digit
-- and there's a semicolon.
declare
F0 : constant Natural := Skip_WS (Source, Line_Pos);
Semi : Natural;
begin
if F0 > 0 and then Is_Hex_Digit (Source (F0)) then
Semi := Find_Semi (Source, Line_Pos);
if Semi > 0 and then Semi < Source'Last then
-- Extract value field
declare
VS : constant Natural := Skip_WS (Source, Semi + 1);
begin
if VS > 0 then
declare
VE_Raw : constant Positive :=
Find_Val_End (Source, VS);
VE : constant Positive :=
Trim_Trailing (Source, VS, VE_Raw);
Val_Len : constant Natural := VE - VS;
begin
if Val_Len > 0 then
Found_Any := True;
-- Check if this value is already in Names
declare
Is_New : Boolean := True;
begin
for I in 1 .. Num_Values loop
declare
Name_Len : constant Natural :=
Names (I).Last -
Names (I).First + 1;
begin
if Name_Len = Val_Len then
-- Compare byte by byte
declare
NF : constant Positive :=
Names (I).First;
Match : Boolean := True;
begin
for K in 0 .. Val_Len - 1 loop
if Source (VS + K)
/= Source (NF + K)
then
Match := False;
exit;
end if;
pragma Loop_Invariant
(Match);
pragma Loop_Variant
(Increases => K);
end loop;
if Match then
Is_New := False;
exit;
end if;
end;
end if;
end;
-- Safety: all existing entries valid
pragma Loop_Invariant (Is_New);
pragma Loop_Invariant
(Num_Values in 1 .. Max_Value_Names);
pragma Loop_Invariant
(for all J in 1 .. Num_Values =>
Names (J).First in Source'Range
and then
Names (J).Last in Source'Range
and then
Names (J).Last >=
Names (J).First);
pragma Loop_Variant (Increases => I);
end loop;
if Is_New then
if Num_Values = Max_Value_Names then
-- Too many unique values
Success := False;
return;
end if;
Num_Values := Num_Values + 1;
Names (Num_Values) :=
(First => VS,
Last => VE - 1);
end if;
end;
end if;
end;
end if;
end;
end if;
end if;
end;
Line_Pos := Next_Line (Source, Line_Pos);
pragma Loop_Invariant (Line_Pos in 2 .. Source'Last + 1);
pragma Loop_Invariant
(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);
pragma Loop_Variant (Increases => Line_Pos);
end loop;
if not Found_Any then
Success := False;
end if;
end Extract_Value_Names;
---------------------------------------------------------------------------
-- Parse_Property_File
---------------------------------------------------------------------------
procedure Parse_Property_File
(Source : Byte_Array;
Names : Value_Name_Array;
Num_Values : Property_Index;
Table : out Property_Table;
Success : out Boolean)
is
Line_Pos : Positive := 1;
begin
-- Initialize table to default
Table := [others => Default_Index];
Success := True;
while Line_Pos <= Source'Last loop
Process_Line (Source, Line_Pos, Names, Num_Values, Table, Success);
-- Advance to next line
Line_Pos := Next_Line (Source, Line_Pos);
-- Safety invariant: table entries in range
pragma Loop_Invariant (Line_Pos in 2 .. Source'Last + 1);
pragma Loop_Invariant
(for all CP in Codepoint =>
Table (CP) in 0 .. Num_Values);
-- Correctness Part A: if future lines assign CP a value,
-- that value equals what Expected_Value(S, 1, CP, ...) produces.
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_From (Source, Line_Pos, CP, Names, Num_Values)
/= Default_Index
then
Expected_From (Source, 1, CP, Names, Num_Values) =
Expected_From (Source, Line_Pos, CP, Names, Num_Values)));
-- Correctness Part B: if future lines do NOT assign CP a value,
-- then Table(CP) holds the correct Expected_Value(S, 1, CP, ...).
pragma Loop_Invariant
(for all CP in Codepoint =>
(if Expected_From (Source, Line_Pos, CP, Names, Num_Values)
= Default_Index
then
Expected_From (Source, 1, CP, Names, Num_Values) =
Table (CP)));
pragma Loop_Variant (Increases => Line_Pos);
end loop;
end Parse_Property_File;
end Lingenic_Text.UCD_Parser;