-- 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 — Normalization body
--
-- Self-contained normalization module. Initialize reads UnicodeData.txt
-- and DerivedNormalizationProps.txt, builds CCC, decomposition,
-- composition, and Quick Check tables.
--
-- Initialize is SPARK_Mode Off: file I/O, string concatenation,
-- UnicodeData.txt 14-field parsing, DerivedNormalizationProps.txt
-- multi-field parsing.
--
-- Expand_Decompositions and Build_Composition_Table are SPARK_Mode On:
-- pure array transformations with proved bounds.
--
-- All runtime procedures (Decompose, Canonical_Order, Compose,
-- Normalize, Quick_Check, Is_Normalized) are SPARK_Mode On.
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.UTF8;
package body Lingenic_Text.Normalization
with SPARK_Mode,
Refined_State => (Norm_State =>
(Is_Init,
CCC_Table,
Canon_Index, Canon_Data, Canon_Used,
Compat_Index, Compat_Data, Compat_Used,
Comp_Index, Comp_Pairs, Comp_Used,
NFD_QC_Table, NFC_QC_Table,
NFKD_QC_Table, NFKC_QC_Table,
Init_UD_Buffer, Init_UD_Length,
Init_DNP_Buffer, Init_DNP_Length,
Init_Raw_Decomps, Init_Raw_CPs,
Init_Num_Raw, Init_Raw_CP_Used,
Init_Excluded, Init_Counts))
is
use Normalization_Spec;
---------------------------------------------------------------------------
-- Constants
---------------------------------------------------------------------------
Max_Decomp_Data : constant := 100_000;
Max_Comp_Pairs : constant := 2_000;
-- Working buffer for codepoints during normalization.
-- Each segment between starters is tiny (max ~30 CPs in practice).
-- 256 is extremely generous.
Max_Work_CPs : constant := 256;
---------------------------------------------------------------------------
-- Data types
---------------------------------------------------------------------------
type CCC_Table_Type is array (0 .. Max_Codepoint) of CCC_Value;
type Decomp_Entry is record
Offset : Natural; -- into Decomp_Data, 0 = no decomposition
Length : Natural; -- number of codepoints, 0 = maps to self
end record;
type Decomp_Index_Type is array (0 .. Max_Codepoint) of Decomp_Entry;
type Decomp_Data_Type is array (1 .. Max_Decomp_Data) of Codepoint;
type Comp_Pair is record
Second : Codepoint;
Result : Codepoint;
end record;
type Comp_Range is record
Start : Natural; -- index into Comp_Pairs, 0 = no compositions
Count : Natural; -- number of pairs for this starter
end record;
type Comp_Index_Type is array (0 .. Max_Codepoint) of Comp_Range;
type Comp_Pairs_Type is array (1 .. Max_Comp_Pairs) of Comp_Pair;
type QC_Binary_Type is array (0 .. Max_Codepoint) of Boolean;
type QC_Ternary_Type is array (0 .. Max_Codepoint) of QC_Value;
-- Work array element is Natural, not Codepoint, because Compose_Buffer
-- uses Max_Codepoint + 1 as a deletion sentinel.
type CP_Work_Array is array (1 .. Max_Work_CPs) of Natural;
type CCC_Work_Array is array (1 .. Max_Work_CPs) of CCC_Value;
---------------------------------------------------------------------------
-- State variables
---------------------------------------------------------------------------
Is_Init : Boolean := False;
CCC_Table : CCC_Table_Type := [others => 0];
Canon_Index : Decomp_Index_Type := [others => (Offset => 0, Length => 0)];
Canon_Data : Decomp_Data_Type := [others => 0];
Canon_Used : Natural := 0;
Compat_Index : Decomp_Index_Type := [others => (Offset => 0, Length => 0)];
Compat_Data : Decomp_Data_Type := [others => 0];
Compat_Used : Natural := 0;
Comp_Index : Comp_Index_Type := [others => (Start => 0, Count => 0)];
Comp_Pairs : Comp_Pairs_Type := [others => (Second => 0, Result => 0)];
Comp_Used : Natural := 0;
NFD_QC_Table : QC_Binary_Type := [others => True];
NFC_QC_Table : QC_Ternary_Type := [others => QC_Yes];
NFKD_QC_Table : QC_Binary_Type := [others => True];
NFKC_QC_Table : QC_Ternary_Type := [others => QC_Yes];
---------------------------------------------------------------------------
-- Init-time temporaries (package-level to avoid stack overflow)
--
-- These are only used during Initialize and could conceptually be local,
-- but they're too large for the default 8 MB stack on macOS:
-- UD_Buffer, DNP_Buffer: 4 MB each (file contents)
-- Init_Excluded: ~1.1 MB (composition exclusion flags)
-- Init_Counts: ~4.5 MB (composition pair counting)
-- Raw_Decomps: ~800 KB (raw decomposition entries)
-- Raw_CPs: ~400 KB (raw decomposition codepoints)
-- Following the Properties module pattern: all at package level.
---------------------------------------------------------------------------
Init_UD_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_UD_Length : File_IO.File_Size := 0;
Init_DNP_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_DNP_Length : File_IO.File_Size := 0;
Max_Raw_Decomps : constant := 50_000;
Max_Raw_CPs : constant := 100_000;
type Raw_Decomp_Entry is record
CP : Codepoint;
Offset : Natural;
Length : Natural;
Is_Canon : Boolean;
end record;
type Raw_Decomp_Array is
array (1 .. Max_Raw_Decomps) of Raw_Decomp_Entry;
type Raw_CP_Array is array (1 .. Max_Raw_CPs) of Codepoint;
Init_Raw_Decomps : Raw_Decomp_Array :=
[others => (CP => 0, Offset => 0, Length => 0, Is_Canon => False)];
Init_Raw_CPs : Raw_CP_Array := [others => 0];
Init_Num_Raw : Natural := 0;
Init_Raw_CP_Used : Natural := 0;
Init_Excluded : QC_Binary_Type := [others => False];
-- Counts array for Build_Composition_Table
type Count_Array is array (0 .. Max_Codepoint) of Natural;
Init_Counts : Count_Array := [others => 0];
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean is (Is_Init);
---------------------------------------------------------------------------
-- Data_All_Terminal — UCD data invariant
--
-- All entries in Canon_Data(1..Canon_Used) and Compat_Data(1..Compat_Used)
-- are terminal: no further decomposition (Canon_Index maps to self) and
-- not Hangul syllables. Also: all entries in the NFC/NFKC composition
-- results have NFC_QC /= QC_No (needed for NFC closing).
---------------------------------------------------------------------------
function Data_All_Terminal return Boolean
is (Canon_Used <= Max_Decomp_Data
and then Compat_Used <= Max_Decomp_Data
-- Canonical decomposition entries are terminal
and then (for all I in 1 .. Canon_Used =>
Canon_Data (I) <= Max_Codepoint
and then Canon_Index (Canon_Data (I)).Length = 0
and then not Is_Hangul_Syllable (Canon_Data (I)))
-- Compatibility decomposition entries are terminal
and then (for all I in 1 .. Compat_Used =>
Compat_Data (I) <= Max_Codepoint
and then Compat_Index (Compat_Data (I)).Length = 0
and then not Is_Hangul_Syllable (Compat_Data (I)))
-- Canonical decomposition entries have NFC_QC /= QC_No
and then (for all I in 1 .. Canon_Used =>
NFC_QC_Table (Canon_Data (I)) /= QC_No)
-- Compatibility decomposition entries have NFKC_QC /= QC_No
and then (for all I in 1 .. Compat_Used =>
NFKC_QC_Table (Compat_Data (I)) /= QC_No)
-- Compatibility entries also have no canonical decomposition
-- (terminal under canonical decomp as well as compat).
and then (for all I in 1 .. Compat_Used =>
Canon_Index (Compat_Data (I)).Length = 0)
-- Valid decomposition offsets point within the Used range.
and then (for all C in Codepoint =>
(if Canon_Index (C).Length > 0
and then Canon_Index (C).Offset >= 1
then Canon_Index (C).Offset <= Canon_Used
and then Canon_Index (C).Length
<= Canon_Used - Canon_Index (C).Offset + 1))
and then (for all C in Codepoint =>
(if Compat_Index (C).Length > 0
and then Compat_Index (C).Offset >= 1
then Compat_Index (C).Offset <= Compat_Used
and then Compat_Index (C).Length
<= Compat_Used - Compat_Index (C).Offset + 1))
-- Offset validity: Length > 0 implies Offset >= 1.
-- A non-empty decomposition always has a valid starting offset.
and then (for all C in Codepoint =>
(if Canon_Index (C).Length > 0
then Canon_Index (C).Offset >= 1))
and then (for all C in Codepoint =>
(if Compat_Index (C).Length > 0
then Compat_Index (C).Offset >= 1))
-- Self-mapping under compat also self-maps under canon:
-- every canonical decomposition is a compatibility decomposition,
-- so no compat decomposition implies no canon decomposition.
and then (for all I in Codepoint =>
(if not Is_Hangul_Syllable (I)
and then Compat_Index (I).Length = 0
then Canon_Index (I).Length = 0))
-- Hangul jamo (L, V, T) have no canonical decomposition.
-- Jamo are the terminal elements of Hangul syllable decomposition.
and then (for all I in LBase .. LBase + LCount - 1 =>
Canon_Index (I).Length = 0)
and then (for all I in VBase .. VBase + VCount - 1 =>
Canon_Index (I).Length = 0)
and then (for all I in TBase .. TBase + TCount - 1 =>
Canon_Index (I).Length = 0)
-- Hangul jamo (L, V, T) have no compatibility decomposition.
and then (for all I in LBase .. LBase + LCount - 1 =>
Compat_Index (I).Length = 0)
and then (for all I in VBase .. VBase + VCount - 1 =>
Compat_Index (I).Length = 0)
and then (for all I in TBase .. TBase + TCount - 1 =>
Compat_Index (I).Length = 0)
-- Hangul L jamo are starters (CCC = 0).
and then (for all I in LBase .. LBase + LCount - 1 =>
CCC_Table (I) = 0)
-- Hangul syllables (precomposed) are starters (CCC = 0).
-- No Hangul syllable carries a combining class — UnicodeData.txt
-- never assigns CCC to U+AC00..U+D7A3, so the default 0 stands.
and then (for all I in SBase .. SBase + SCount - 1 =>
CCC_Table (I) = 0)
-- Composition table results have NFC_QC /= QC_No.
-- Primary composites always have NFC_QC = QC_Yes.
and then Comp_Used <= Max_Comp_Pairs
and then (for all I in 1 .. Comp_Used =>
Comp_Pairs (I).Result <= Max_Codepoint
and then NFC_QC_Table (Comp_Pairs (I).Result) /= QC_No
and then NFKC_QC_Table (Comp_Pairs (I).Result) /= QC_No)
-- Composition index entries point within 1..Comp_Used.
and then (for all C in Codepoint =>
(if Comp_Index (C).Start >= 1
and then Comp_Index (C).Count >= 1
and then Comp_Index (C).Start <= Max_Comp_Pairs
and then Comp_Index (C).Count <= Max_Comp_Pairs
and then Comp_Index (C).Start <=
Max_Comp_Pairs - Comp_Index (C).Count + 1
then Comp_Index (C).Start + Comp_Index (C).Count - 1
<= Comp_Used))
-- Hangul syllables have NFC_QC /= QC_No and NFKC_QC /= QC_No.
-- All Hangul syllables (U+AC00..U+D7A3) are primary composites.
and then (for all I in SBase .. SBase + SCount - 1 =>
NFC_QC_Table (I) /= QC_No
and then NFKC_QC_Table (I) /= QC_No)
-- Self-mapping CPs have NFC_QC /= QC_No.
-- NFC_QC = QC_No implies the CP has a canonical decomposition.
and then (for all I in Codepoint =>
(if Canon_Index (I).Length = 0
and then not Is_Hangul_Syllable (I)
then NFC_QC_Table (I) /= QC_No))
-- Self-mapping CPs under compat have NFKC_QC /= QC_No.
and then (for all I in Codepoint =>
(if Compat_Index (I).Length = 0
and then not Is_Hangul_Syllable (I)
then NFKC_QC_Table (I) /= QC_No)));
---------------------------------------------------------------------------
-- Ghost function bodies
---------------------------------------------------------------------------
-- Expression function body: solver can unfold during proof.
function Ghost_Decomp_Len
(CP : Codepoint;
Use_Canon : Boolean) return Natural
is (if Is_Hangul_Syllable (CP) then
(if (CP - SBase) mod TCount = 0 then 2 else 3)
elsif Use_Canon
and then Canon_Index (CP).Length > 0
and then Canon_Index (CP).Offset >= 1
and then Canon_Index (CP).Length <= Max_Decomp_Data
and then Canon_Index (CP).Offset <=
Max_Decomp_Data - Canon_Index (CP).Length + 1
then Canon_Index (CP).Length
elsif not Use_Canon
and then Compat_Index (CP).Length > 0
and then Compat_Index (CP).Offset >= 1
and then Compat_Index (CP).Length <= Max_Decomp_Data
and then Compat_Index (CP).Offset <=
Max_Decomp_Data - Compat_Index (CP).Length + 1
then Compat_Index (CP).Length
else 0);
function Ghost_Decomp_CP
(CP : Codepoint;
Use_Canon : Boolean;
Idx : Positive) return Codepoint
is
D : Decomp_Entry;
begin
-- Hangul algorithmic decomposition
if Is_Hangul_Syllable (CP) then
declare
SIndex : constant Natural := CP - SBase;
L : constant Codepoint := LBase + SIndex / NCount;
V : constant Codepoint :=
VBase + (SIndex mod NCount) / TCount;
T : constant Codepoint := TBase + SIndex mod TCount;
begin
if Idx = 1 then return L;
elsif Idx = 2 then return V;
else return T;
end if;
end;
end if;
if Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Length <= Max_Decomp_Data
and then D.Offset <= Max_Decomp_Data - D.Length + 1
and then Idx <= D.Length
then
if Use_Canon then
return Canon_Data (D.Offset + Idx - 1);
else
return Compat_Data (D.Offset + Idx - 1);
end if;
else
return CP; -- Shouldn't happen given precondition
end if;
end Ghost_Decomp_CP;
function Ghost_Decomp_Out_Bytes
(CP : Codepoint;
Use_Canon : Boolean) return Positive
is
D : Decomp_Entry;
Total : Natural := 0;
begin
-- Hangul algorithmic decomposition
if Is_Hangul_Syllable (CP) then
-- Jamo L, V, T are all in 0x1100..0x11FF range → 3 bytes each
if (CP - SBase) mod TCount = 0 then
return 6; -- L (3) + V (3)
else
return 9; -- L (3) + V (3) + T (3)
end if;
end if;
if Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Length <= Max_Decomp_Data
and then D.Offset <= Max_Decomp_Data - D.Length + 1
then
for I in D.Offset .. D.Offset + D.Length - 1 loop
pragma Loop_Invariant (Total <= (I - D.Offset) * 4);
if Use_Canon then
Total := Total + UTF8_Spec.Encoded_Length (Canon_Data (I));
else
Total := Total + UTF8_Spec.Encoded_Length (Compat_Data (I));
end if;
end loop;
pragma Assert (Total <= D.Length * 4);
if Total = 0 then
return UTF8_Spec.Encoded_Length (CP);
else
return Total;
end if;
else
return UTF8_Spec.Encoded_Length (CP); -- Maps to self
end if;
end Ghost_Decomp_Out_Bytes;
---------------------------------------------------------------------------
-- Expand_Decompositions (SPARK_Mode On)
--
-- Takes single-step decompositions and expands them to full recursive
-- decompositions. Fixed-point iteration: each pass replaces entries
-- whose decomposition contains CPs that themselves decompose.
-- Terminates when no entry changes (max depth ~3 in Unicode).
---------------------------------------------------------------------------
procedure Expand_Decompositions
(Index : in out Decomp_Index_Type;
Data : in out Decomp_Data_Type;
Used : in out Natural)
with Pre => Used <= Max_Decomp_Data,
Post => Used <= Max_Decomp_Data
is
Changed : Boolean;
New_Used : Natural;
-- Temporary expansion buffer for one entry
Max_Expand : constant := 64;
Tmp : array (1 .. Max_Expand) of Codepoint := [others => 0];
Tmp_Len : Natural;
begin
loop
pragma Loop_Invariant (Used <= Max_Decomp_Data);
Changed := False;
for CP in 0 .. Max_Codepoint loop
pragma Loop_Invariant (Used <= Max_Decomp_Data);
if Index (CP).Length > 0
and then Index (CP).Offset >= 1
and then Index (CP).Length <= Max_Decomp_Data
and then Index (CP).Offset <= Max_Decomp_Data
- Index (CP).Length + 1
and then Index (CP).Offset + Index (CP).Length - 1
<= Used
then
-- Check if any CP in this entry's decomposition
-- itself has a decomposition
declare
Off : constant Positive := Index (CP).Offset;
Len : constant Positive := Index (CP).Length;
Needs_Expand : Boolean := False;
begin
for I in Off .. Off + Len - 1 loop
if Index (Data (I)).Length > 0 then
Needs_Expand := True;
exit;
end if;
end loop;
if Needs_Expand then
-- Build expanded sequence in Tmp
Tmp_Len := 0;
for I in Off .. Off + Len - 1 loop
pragma Loop_Invariant (Tmp_Len <= Max_Expand);
pragma Loop_Invariant (Used <= Max_Decomp_Data);
declare
Sub_CP : constant Codepoint := Data (I);
begin
if Index (Sub_CP).Length > 0
and then Index (Sub_CP).Offset >= 1
and then Index (Sub_CP).Length
<= Max_Decomp_Data
and then Index (Sub_CP).Offset
<= Max_Decomp_Data
- Index (Sub_CP).Length + 1
and then Index (Sub_CP).Offset
+ Index (Sub_CP).Length - 1 <= Used
then
-- Replace with sub-decomposition
declare
SO : constant Positive :=
Index (Sub_CP).Offset;
SL : constant Positive :=
Index (Sub_CP).Length;
begin
for J in SO .. SO + SL - 1 loop
pragma Loop_Invariant
(Tmp_Len <= Max_Expand);
if Tmp_Len < Max_Expand then
Tmp_Len := Tmp_Len + 1;
Tmp (Tmp_Len) := Data (J);
end if;
end loop;
end;
else
-- Keep as-is
if Tmp_Len < Max_Expand then
Tmp_Len := Tmp_Len + 1;
Tmp (Tmp_Len) := Sub_CP;
end if;
end if;
end;
end loop;
-- Write expanded sequence to end of Data
if Tmp_Len > 0
and then Tmp_Len <= Max_Decomp_Data
and then Used <= Max_Decomp_Data - Tmp_Len
then
New_Used := Used;
for I in 1 .. Tmp_Len loop
pragma Loop_Invariant
(New_Used >= Used
and New_Used <= Used + I - 1
and New_Used < Max_Decomp_Data);
New_Used := New_Used + 1;
Data (New_Used) := Tmp (I);
end loop;
Index (CP) :=
(Offset => Used + 1, Length => Tmp_Len);
Used := New_Used;
Changed := True;
end if;
end if;
end;
end if;
end loop;
exit when not Changed;
end loop;
end Expand_Decompositions;
---------------------------------------------------------------------------
-- Build_Composition_Table (SPARK_Mode On)
--
-- Scans canonical decompositions for length-2 entries where the first
-- CP is a starter and the composite is not excluded. Populates
-- Comp_Index (flat, indexed by first/starter) and Comp_Pairs.
---------------------------------------------------------------------------
procedure Build_Composition_Table
(C_Index : Decomp_Index_Type;
C_Data : Decomp_Data_Type;
C_Used : Natural;
CCC_Tab : CCC_Table_Type;
Excluded : QC_Binary_Type; -- True = excluded
CI : out Comp_Index_Type;
CP_Arr : out Comp_Pairs_Type;
CP_Used : out Natural)
with Pre => C_Used <= Max_Decomp_Data
is
-- Uses package-level Init_Counts to avoid stack overflow
Total : Natural := 0;
begin
CI := [others => (Start => 0, Count => 0)];
CP_Arr := [others => (Second => 0, Result => 0)];
CP_Used := 0;
Init_Counts := [others => 0];
-- Count compositions per starter
for Composite in 0 .. Max_Codepoint loop
if C_Index (Composite).Length = 2
and then C_Index (Composite).Offset >= 1
and then C_Index (Composite).Offset <= Max_Decomp_Data - 1
and then C_Index (Composite).Offset + 1 <= C_Used
and then not Excluded (Composite)
and then not Is_Hangul_Syllable (Composite)
then
declare
First : constant Codepoint :=
C_Data (C_Index (Composite).Offset);
begin
if CCC_Tab (First) = 0
and then Init_Counts (First) < Natural'Last
and then Total < Max_Comp_Pairs
then
Init_Counts (First) := Init_Counts (First) + 1;
Total := Total + 1;
end if;
end;
end if;
end loop;
if Total = 0 or Total > Max_Comp_Pairs then
return;
end if;
-- Assign ranges in Comp_Pairs for each starter
declare
Pos : Natural := 1;
begin
for Starter in 0 .. Max_Codepoint loop
pragma Loop_Invariant (Pos >= 1 and Pos <= Max_Comp_Pairs + 1);
if Init_Counts (Starter) > 0
and then Init_Counts (Starter) <= Max_Comp_Pairs
and then Pos <= Max_Comp_Pairs - Init_Counts (Starter) + 1
then
CI (Starter) :=
(Start => Pos, Count => Init_Counts (Starter));
Pos := Pos + Init_Counts (Starter);
end if;
end loop;
end;
-- Fill pairs - use Init_Counts as a "next slot" tracker
-- Reset counts to 0, then use as offset within each starter's range
Init_Counts := [others => 0];
for Composite in 0 .. Max_Codepoint loop
if C_Index (Composite).Length = 2
and then C_Index (Composite).Offset >= 1
and then C_Index (Composite).Offset <= Max_Decomp_Data - 1
and then C_Index (Composite).Offset + 1 <= C_Used
and then not Excluded (Composite)
and then not Is_Hangul_Syllable (Composite)
then
declare
First : constant Codepoint :=
C_Data (C_Index (Composite).Offset);
Second : constant Codepoint :=
C_Data (C_Index (Composite).Offset + 1);
begin
if CCC_Tab (First) = 0
and then CI (First).Start > 0
and then CI (First).Start <= Max_Comp_Pairs
and then Init_Counts (First) < CI (First).Count
and then CI (First).Count <= Max_Comp_Pairs
then
declare
Slot : constant Positive :=
CI (First).Start + Init_Counts (First);
begin
if Slot <= Max_Comp_Pairs then
CP_Arr (Slot) :=
(Second => Second, Result => Composite);
Init_Counts (First) := Init_Counts (First) + 1;
end if;
end;
end if;
end;
end if;
end loop;
CP_Used := Total;
end Build_Composition_Table;
---------------------------------------------------------------------------
-- Lookup_Composition
--
-- Given a starter and a combining character, look up the composite.
-- Returns Max_Codepoint + 1 (outside Codepoint range) if no composition.
---------------------------------------------------------------------------
function Lookup_Composition
(Starter : Codepoint;
Combining : Codepoint) return Natural
with Pre => Initialized and then Data_All_Terminal,
Post => (if Lookup_Composition'Result <= Max_Codepoint then
NFC_QC_Table (Lookup_Composition'Result) /= QC_No
and then NFKC_QC_Table (Lookup_Composition'Result) /= QC_No)
is
R : Comp_Range;
begin
R := Comp_Index (Starter);
if R.Start = 0 or R.Count = 0
or R.Start > Max_Comp_Pairs
or R.Count > Max_Comp_Pairs
or R.Start > Max_Comp_Pairs - R.Count + 1
then
return Max_Codepoint + 1;
end if;
for I in R.Start .. R.Start + R.Count - 1 loop
pragma Loop_Invariant (I <= R.Start + R.Count - 1);
if I <= Max_Comp_Pairs
and then Comp_Pairs (I).Second = Combining
then
-- I <= Comp_Used from Comp_Index data invariant.
pragma Assert (I <= Comp_Used);
return Comp_Pairs (I).Result;
end if;
end loop;
return Max_Codepoint + 1;
end Lookup_Composition;
---------------------------------------------------------------------------
-- Is_NF_Boundary
--
-- Returns True if CP is a normalization boundary: a starter (CCC = 0)
-- that can safely begin a new segment.
--
-- For decomposition forms (NFD/NFKD), every starter is a boundary.
-- For composition forms (NFC/NFKC), a starter with QC_Maybe is NOT
-- a boundary because it could be the second element of a composition
-- pair with the preceding starter.
---------------------------------------------------------------------------
function Is_NF_Boundary
(CP : Codepoint; Do_Compose : Boolean) return Boolean
is (CCC_Table (CP) = 0
and then (not Do_Compose
or else (NFC_QC_Table (CP) /= QC_Maybe
and then NFKC_QC_Table (CP) /= QC_Maybe)));
---------------------------------------------------------------------------
-- Initialize (SPARK_Mode Off)
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
OK : Boolean;
-----------------------------------------------------------------------
-- Parse a decimal integer from a string
-----------------------------------------------------------------------
function Parse_Decimal (S : String) return Natural is
Val : Natural := 0;
begin
for I in S'Range loop
if S (I) in '0' .. '9' then
Val := Val * 10 +
(Character'Pos (S (I)) - Character'Pos ('0'));
end if;
end loop;
return Val;
end Parse_Decimal;
-----------------------------------------------------------------------
-- Parse hex codepoint from a string
-----------------------------------------------------------------------
function Parse_Hex (S : String) return Natural is
Val : Natural := 0;
begin
for I in S'Range loop
Val := Val * 16;
case S (I) is
when '0' .. '9' =>
Val := Val + (Character'Pos (S (I)) - Character'Pos ('0'));
when 'A' .. 'F' =>
Val := Val +
(Character'Pos (S (I)) - Character'Pos ('A') + 10);
when 'a' .. 'f' =>
Val := Val +
(Character'Pos (S (I)) - Character'Pos ('a') + 10);
when others =>
return Val / 16; -- undo last multiply
end case;
end loop;
return Val;
end Parse_Hex;
-----------------------------------------------------------------------
-- Extract field N (0-based) from a semicolon-delimited line.
-- Returns the substring bounds (First .. Last). Last < First if
-- the field is empty or not found.
-----------------------------------------------------------------------
procedure Get_Field
(Line : String;
Field_Num : Natural;
First : out Positive;
Last : out Natural)
is
Pos : Positive := Line'First;
Field : Natural := 0;
F_Start : Positive := Line'First;
begin
First := Line'First;
Last := Line'First - 1;
while Pos <= Line'Last loop
if Line (Pos) = ';' then
if Field = Field_Num then
First := F_Start;
-- Trim trailing spaces
Last := Pos - 1;
while Last >= F_Start
and then (Line (Last) = ' ' or Line (Last) = ASCII.HT)
loop
Last := Last - 1;
end loop;
return;
end if;
Field := Field + 1;
F_Start := Pos + 1;
-- Skip leading spaces
while F_Start <= Line'Last
and then (Line (F_Start) = ' '
or Line (F_Start) = ASCII.HT)
loop
F_Start := F_Start + 1;
end loop;
end if;
Pos := Pos + 1;
end loop;
-- Last field (no trailing semicolon)
if Field = Field_Num then
First := F_Start;
Last := Line'Last;
while Last >= F_Start
and then (Line (Last) = ' ' or Line (Last) = ASCII.HT)
loop
Last := Last - 1;
end loop;
end if;
end Get_Field;
-----------------------------------------------------------------------
-- Parse UnicodeData.txt
--
-- Extracts CCC (field 3) and decomposition mappings (field 5).
-----------------------------------------------------------------------
procedure Parse_UnicodeData is
Pos : Positive := 1;
Line_Start : Positive;
Line_End : Natural;
Range_Start_CP : Natural := 0;
In_Range : Boolean := False;
begin
while Pos <= Init_UD_Length loop
Line_Start := Pos;
-- Find end of line
Line_End := Pos;
while Line_End <= Init_UD_Length
and then Init_UD_Buffer (Line_End) /= LF_Byte
and then Init_UD_Buffer (Line_End) /= CR_Byte
loop
Line_End := Line_End + 1;
end loop;
Line_End := Line_End - 1;
-- Skip blank lines and comments
if Line_End >= Line_Start
and then Init_UD_Buffer (Line_Start) /= Hash_Byte
then
-- Convert to String for parsing
declare
Len : constant Natural := Line_End - Line_Start + 1;
Line : String (1 .. Len);
F0_First, F1_First, F3_First, F5_First : Positive;
F0_Last, F1_Last, F3_Last, F5_Last : Natural;
CP_Val : Natural;
CCC_Val : Natural;
begin
for I in 0 .. Len - 1 loop
Line (I + 1) :=
Character'Val (Init_UD_Buffer (Line_Start + I));
end loop;
-- Field 0: codepoint
Get_Field (Line, 0, F0_First, F0_Last);
if F0_Last >= F0_First then
CP_Val := Parse_Hex (Line (F0_First .. F0_Last));
else
CP_Val := Max_Codepoint + 1;
end if;
if CP_Val <= Max_Codepoint then
-- Check for range lines (field 1 contains
-- "<..., First>" or "<..., Last>")
Get_Field (Line, 1, F1_First, F1_Last);
declare
Name : constant String :=
(if F1_Last >= F1_First
then Line (F1_First .. F1_Last)
else "");
begin
if Name'Length > 7
and then Name (Name'Last - 5 .. Name'Last)
= "First>"
then
In_Range := True;
Range_Start_CP := CP_Val;
elsif Name'Length > 6
and then Name (Name'Last - 4 .. Name'Last)
= "Last>"
then
-- Apply CCC to entire range
-- (CCC is always 0 for ranges, but parse anyway)
Get_Field (Line, 3, F3_First, F3_Last);
if F3_Last >= F3_First then
CCC_Val := Parse_Decimal
(Line (F3_First .. F3_Last));
if CCC_Val <= 254 then
for C in Range_Start_CP .. CP_Val loop
if C <= Max_Codepoint then
CCC_Table (C) := CCC_Val;
end if;
end loop;
end if;
end if;
In_Range := False;
goto Continue;
end if;
end;
if In_Range then
goto Continue;
end if;
-- Field 3: CCC
Get_Field (Line, 3, F3_First, F3_Last);
if F3_Last >= F3_First then
CCC_Val := Parse_Decimal
(Line (F3_First .. F3_Last));
if CCC_Val <= 254 then
CCC_Table (CP_Val) := CCC_Val;
end if;
end if;
-- Field 5: decomposition mapping
Get_Field (Line, 5, F5_First, F5_Last);
if F5_Last >= F5_First then
declare
Field : constant String :=
Line (F5_First .. F5_Last);
Is_Canon : Boolean := True;
Parse_Start : Positive := Field'First;
D_Offset : Natural;
D_Length : Natural := 0;
begin
-- Check for compatibility tag <...>
if Field (Field'First) = '<' then
Is_Canon := False;
-- Skip past '>'
Parse_Start := Field'First;
while Parse_Start <= Field'Last
and then Field (Parse_Start) /= '>'
loop
Parse_Start := Parse_Start + 1;
end loop;
if Parse_Start <= Field'Last then
Parse_Start := Parse_Start + 1;
-- Skip spaces after '>'
while Parse_Start <= Field'Last
and then Field (Parse_Start) = ' '
loop
Parse_Start := Parse_Start + 1;
end loop;
end if;
end if;
-- Parse space-separated hex codepoints
D_Offset := Init_Raw_CP_Used + 1;
declare
P : Positive := Parse_Start;
Hex_Start : Positive;
Decomp_CP : Natural;
begin
while P <= Field'Last loop
-- Skip spaces
while P <= Field'Last
and then Field (P) = ' '
loop
P := P + 1;
end loop;
exit when P > Field'Last;
-- Read hex value
Hex_Start := P;
while P <= Field'Last
and then Field (P) /= ' '
loop
P := P + 1;
end loop;
Decomp_CP := Parse_Hex
(Field (Hex_Start .. P - 1));
if Decomp_CP <= Max_Codepoint
and then Init_Raw_CP_Used < Max_Raw_CPs
then
Init_Raw_CP_Used := Init_Raw_CP_Used + 1;
Init_Raw_CPs (Init_Raw_CP_Used) := Decomp_CP;
D_Length := D_Length + 1;
end if;
end loop;
end;
-- Store raw decomposition entry
if D_Length > 0
and then Init_Num_Raw < Max_Raw_Decomps
then
Init_Num_Raw := Init_Num_Raw + 1;
Init_Raw_Decomps (Init_Num_Raw) :=
(CP => CP_Val,
Offset => D_Offset,
Length => D_Length,
Is_Canon => Is_Canon);
end if;
end;
end if;
end if;
end;
end if;
<<Continue>>
-- Advance past line ending
Pos := Line_End + 1;
if Pos <= Init_UD_Length
and then Init_UD_Buffer (Pos) = CR_Byte
then
Pos := Pos + 1;
end if;
if Pos <= Init_UD_Length
and then Init_UD_Buffer (Pos) = LF_Byte
then
Pos := Pos + 1;
end if;
if Pos <= Line_End + 1 then
Pos := Init_UD_Length + 1;
end if;
end loop;
-- Populate Canon_Index and Compat_Index from raw decompositions
Canon_Used := 0;
Compat_Used := 0;
for I in 1 .. Init_Num_Raw loop
declare
R : Raw_Decomp_Entry renames Init_Raw_Decomps (I);
begin
-- Canonical decomposition
if R.Is_Canon
and then R.Length > 0
and then Canon_Used + R.Length <= Max_Decomp_Data
then
for J in 0 .. R.Length - 1 loop
Canon_Data (Canon_Used + J + 1) :=
Init_Raw_CPs (R.Offset + J);
end loop;
Canon_Index (R.CP) :=
(Offset => Canon_Used + 1, Length => R.Length);
Canon_Used := Canon_Used + R.Length;
end if;
-- All decompositions go into compat
if R.Length > 0
and then Compat_Used + R.Length <= Max_Decomp_Data
then
for J in 0 .. R.Length - 1 loop
Compat_Data (Compat_Used + J + 1) :=
Init_Raw_CPs (R.Offset + J);
end loop;
Compat_Index (R.CP) :=
(Offset => Compat_Used + 1, Length => R.Length);
Compat_Used := Compat_Used + R.Length;
end if;
end;
end loop;
end Parse_UnicodeData;
-----------------------------------------------------------------------
-- Parse DerivedNormalizationProps.txt
--
-- Extracts Full_Composition_Exclusion, NFD_QC, NFC_QC, NFKD_QC,
-- NFKC_QC properties.
-----------------------------------------------------------------------
procedure Parse_DerivedNormProps is
Pos : Positive := 1;
Line_Start : Positive;
Line_End : Natural;
begin
while Pos <= Init_DNP_Length loop
Line_Start := Pos;
-- Find end of line
Line_End := Pos;
while Line_End <= Init_DNP_Length
and then Init_DNP_Buffer (Line_End) /= LF_Byte
and then Init_DNP_Buffer (Line_End) /= CR_Byte
loop
Line_End := Line_End + 1;
end loop;
Line_End := Line_End - 1;
-- Skip blank lines and comments
if Line_End >= Line_Start
and then Init_DNP_Buffer (Line_Start) /= Hash_Byte
then
declare
Len : constant Natural := Line_End - Line_Start + 1;
Line : String (1 .. Len);
begin
for I in 0 .. Len - 1 loop
Line (I + 1) :=
Character'Val (Init_DNP_Buffer (Line_Start + I));
end loop;
-- Parse: "CP..CP ; PropName ; Value" or
-- "CP..CP ; PropName"
declare
Semi1 : Natural := 0;
Semi2 : Natural := 0;
CP_Start_Val : Natural;
CP_End_Val : Natural;
begin
-- Find first semicolon
for I in Line'Range loop
if Line (I) = ';' then
Semi1 := I;
exit;
end if;
end loop;
if Semi1 = 0 then
goto DNP_Continue;
end if;
-- Find second semicolon (if any)
for I in Semi1 + 1 .. Line'Last loop
if Line (I) = ';' then
Semi2 := I;
exit;
end if;
end loop;
-- Parse codepoint or range
declare
CP_Field : constant String :=
Line (Line'First .. Semi1 - 1);
Dot_Pos : Natural := 0;
Trimmed_Last : Natural := CP_Field'Last;
begin
-- Trim trailing spaces
while Trimmed_Last >= CP_Field'First
and then (CP_Field (Trimmed_Last) = ' '
or CP_Field (Trimmed_Last) = ASCII.HT)
loop
Trimmed_Last := Trimmed_Last - 1;
end loop;
-- Find ".."
for I in CP_Field'First .. Trimmed_Last - 1 loop
if CP_Field (I) = '.'
and then I + 1 <= Trimmed_Last
and then CP_Field (I + 1) = '.'
then
Dot_Pos := I;
exit;
end if;
end loop;
if Dot_Pos > 0 then
CP_Start_Val := Parse_Hex
(CP_Field (CP_Field'First .. Dot_Pos - 1));
CP_End_Val := Parse_Hex
(CP_Field (Dot_Pos + 2 .. Trimmed_Last));
else
CP_Start_Val := Parse_Hex
(CP_Field (CP_Field'First .. Trimmed_Last));
CP_End_Val := CP_Start_Val;
end if;
end;
if CP_Start_Val > Max_Codepoint
or CP_End_Val > Max_Codepoint
then
goto DNP_Continue;
end if;
-- Extract property name (between first and second
-- semicolons, or after first semicolon if no second)
declare
Prop_Start : Positive := Semi1 + 1;
Prop_End : Natural;
begin
-- Skip spaces
while Prop_Start <= Line'Last
and then (Line (Prop_Start) = ' '
or Line (Prop_Start) = ASCII.HT)
loop
Prop_Start := Prop_Start + 1;
end loop;
if Semi2 > 0 then
Prop_End := Semi2 - 1;
else
-- Find end (comment or end of line)
Prop_End := Line'Last;
for I in Prop_Start .. Line'Last loop
if Line (I) = '#' then
Prop_End := I - 1;
exit;
end if;
end loop;
end if;
-- Trim trailing spaces from property name
while Prop_End >= Prop_Start
and then (Line (Prop_End) = ' '
or Line (Prop_End) = ASCII.HT)
loop
Prop_End := Prop_End - 1;
end loop;
if Prop_End < Prop_Start then
goto DNP_Continue;
end if;
declare
Prop_Name : constant String :=
Line (Prop_Start .. Prop_End);
-- Extract value (after second semicolon)
Val_N : Boolean := False;
Val_M : Boolean := False;
begin
if Semi2 > 0 then
declare
VS : Positive := Semi2 + 1;
VE : Natural := Line'Last;
begin
while VS <= Line'Last
and then (Line (VS) = ' '
or Line (VS) = ASCII.HT)
loop
VS := VS + 1;
end loop;
for I in VS .. Line'Last loop
if Line (I) = '#'
or Line (I) = ' '
or Line (I) = ASCII.HT
then
VE := I - 1;
exit;
end if;
end loop;
if VE >= VS then
declare
V : constant String :=
Line (VS .. VE);
begin
Val_N := (V = "N");
Val_M := (V = "M");
end;
end if;
end;
end if;
if Prop_Name = "Full_Composition_Exclusion" then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
Init_Excluded (C) := True;
end if;
end loop;
elsif Prop_Name = "NFD_QC" then
if Val_N then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFD_QC_Table (C) := False;
end if;
end loop;
end if;
elsif Prop_Name = "NFC_QC" then
if Val_N then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFC_QC_Table (C) := QC_No;
end if;
end loop;
elsif Val_M then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFC_QC_Table (C) := QC_Maybe;
end if;
end loop;
end if;
elsif Prop_Name = "NFKD_QC" then
if Val_N then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFKD_QC_Table (C) := False;
end if;
end loop;
end if;
elsif Prop_Name = "NFKC_QC" then
if Val_N then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFKC_QC_Table (C) := QC_No;
end if;
end loop;
elsif Val_M then
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
NFKC_QC_Table (C) := QC_Maybe;
end if;
end loop;
end if;
end if;
end;
end;
end;
end;
end if;
<<DNP_Continue>>
-- Advance past line ending
Pos := Line_End + 1;
if Pos <= Init_DNP_Length
and then Init_DNP_Buffer (Pos) = CR_Byte
then
Pos := Pos + 1;
end if;
if Pos <= Init_DNP_Length
and then Init_DNP_Buffer (Pos) = LF_Byte
then
Pos := Pos + 1;
end if;
if Pos <= Line_End + 1 then
Pos := Init_DNP_Length + 1;
end if;
end loop;
end Parse_DerivedNormProps;
begin -- Initialize
-- Reset state
Is_Init := False;
CCC_Table := [others => 0];
Canon_Index := [others => (Offset => 0, Length => 0)];
Canon_Data := [others => 0];
Canon_Used := 0;
Compat_Index := [others => (Offset => 0, Length => 0)];
Compat_Data := [others => 0];
Compat_Used := 0;
Comp_Index := [others => (Start => 0, Count => 0)];
Comp_Pairs := [others => (Second => 0, Result => 0)];
Comp_Used := 0;
NFD_QC_Table := [others => True];
NFC_QC_Table := [others => QC_Yes];
NFKD_QC_Table := [others => True];
NFKC_QC_Table := [others => QC_Yes];
Init_Num_Raw := 0;
Init_Raw_CP_Used := 0;
Init_Excluded := [others => False];
Success := False;
-- 1. Read UnicodeData.txt
File_IO.Read_File
(UCD_Dir & "/UnicodeData.txt",
Init_UD_Buffer, Init_UD_Length, OK);
if not OK or Init_UD_Length = 0 then return; end if;
-- 2. Parse UnicodeData.txt → CCC + raw decompositions
Parse_UnicodeData;
-- 3. Read DerivedNormalizationProps.txt
File_IO.Read_File
(UCD_Dir & "/DerivedNormalizationProps.txt",
Init_DNP_Buffer, Init_DNP_Length, OK);
if not OK or Init_DNP_Length = 0 then return; end if;
-- 4. Parse DerivedNormalizationProps.txt → QC + exclusions
Parse_DerivedNormProps;
-- 5. Build composition table from single-step decompositions
-- (MUST happen BEFORE expansion — composition pairs come from
-- the original 2-element mappings, not the fully expanded ones)
Build_Composition_Table
(Canon_Index, Canon_Data, Canon_Used,
CCC_Table, Init_Excluded,
Comp_Index, Comp_Pairs, Comp_Used);
-- 6. Expand decompositions (SPARK_Mode On procedure)
Expand_Decompositions (Canon_Index, Canon_Data, Canon_Used);
Expand_Decompositions (Compat_Index, Compat_Data, Compat_Used);
Is_Init := True;
Success := True;
end Initialize;
---------------------------------------------------------------------------
-- Ghost_Buf_Enc_Len — sum of UTF-8 encoded lengths for buffer entries
--
-- Ghost_Buf_Enc_Len(Buf, Len) = sum of Encoded_Length(Buf(I)) for I in 1..Len
-- Returns 0 if any entry exceeds Max_Codepoint (error sentinel).
---------------------------------------------------------------------------
function Ghost_Buf_Enc_Len
(Buf : CP_Work_Array;
Len : Natural) return Natural
is (if Len = 0 then 0
elsif Buf (Len) > Max_Codepoint then 0
else Ghost_Buf_Enc_Len (Buf, Len - 1)
+ UTF8_Spec.Encoded_Length (Buf (Len)))
with Ghost,
Pre => Len <= Max_Work_CPs,
Post => Ghost_Buf_Enc_Len'Result <= Len * 4,
Subprogram_Variant => (Decreases => Len);
---------------------------------------------------------------------------
-- Ghost lemma: if two arrays agree on 1..Len, their sums are equal.
---------------------------------------------------------------------------
procedure Lemma_Buf_Enc_Same
(A : CP_Work_Array;
B : CP_Work_Array;
Len : Natural)
with Ghost,
Pre => Len <= Max_Work_CPs
and then (for all K in 1 .. Len => A (K) = B (K)),
Post => Ghost_Buf_Enc_Len (A, Len) = Ghost_Buf_Enc_Len (B, Len),
Subprogram_Variant => (Decreases => Len)
is
begin
if Len > 0 then
Lemma_Buf_Enc_Same (A, B, Len - 1);
end if;
end Lemma_Buf_Enc_Same;
---------------------------------------------------------------------------
-- Ghost lemma: changing one position preserves the sum modulo the
-- difference at that position.
--
-- Ghost_Buf_Enc_Len(New_Buf, Len) + Encoded_Length(Old_Val)
-- = Ghost_Buf_Enc_Len(Old_Buf, Len) + Encoded_Length(New_Val)
---------------------------------------------------------------------------
procedure Lemma_Update_At
(Old_Buf : CP_Work_Array;
New_Buf : CP_Work_Array;
Len : Natural;
P : Positive;
Old_Val : Codepoint;
New_Val : Codepoint)
with Ghost,
Pre => Len <= Max_Work_CPs
and then P in 1 .. Len
and then Old_Buf (P) = Old_Val
and then New_Buf (P) = New_Val
and then (for all K in 1 .. Len =>
Old_Buf (K) <= Max_Codepoint)
and then (for all K in 1 .. Len =>
New_Buf (K) <= Max_Codepoint)
and then (for all K in 1 .. Len =>
(if K /= P then New_Buf (K) = Old_Buf (K))),
Post => Ghost_Buf_Enc_Len (New_Buf, Len)
+ UTF8_Spec.Encoded_Length (Old_Val)
= Ghost_Buf_Enc_Len (Old_Buf, Len)
+ UTF8_Spec.Encoded_Length (New_Val),
Subprogram_Variant => (Decreases => Len)
is
begin
if P < Len then
-- Top elements agree; recurse on prefix
Lemma_Update_At (Old_Buf, New_Buf, Len - 1, P, Old_Val, New_Val);
else
-- P = Len: top elements differ, prefix agrees
Lemma_Buf_Enc_Same (Old_Buf, New_Buf, Len - 1);
end if;
end Lemma_Update_At;
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Lemma_NFD_Frame — ghost lemma: NFD transfers across byte-identical arrays
--
-- If Ghost_Is_NFD_From holds on Old_Out(Start..Bound), and New_Out agrees
-- with Old_Out on all positions Start..Bound, then Ghost_Is_NFD_From also
-- holds on New_Out(Start..Bound).
--
-- Recursive: unfolds Ghost_Is_NFD_From one CP at a time. At each step,
-- the bytes read are within Start..Bound and are thus identical between
-- Old_Out and New_Out, so the predicate evaluates identically.
---------------------------------------------------------------------------
procedure Lemma_NFD_Frame
(Old_Out : Byte_Array;
New_Out : Byte_Array;
Start : Positive;
Bound : Natural;
Last_CCC : Normalization_Spec.CCC_Value)
with Ghost,
Pre => Initialized
and then Old_Out'First = New_Out'First
and then Old_Out'Last = New_Out'Last
and then Old_Out'Last < Positive'Last
and then Start >= Old_Out'First
and then Bound <= Old_Out'Last
and then Ghost_Is_NFD_From (Old_Out, Start, Bound, Last_CCC)
and then (for all J in Start .. Bound =>
New_Out (J) = Old_Out (J)),
Post => Ghost_Is_NFD_From (New_Out, Start, Bound, Last_CCC),
Subprogram_Variant => (Decreases => Bound - Start + 1)
is
begin
if Start > Bound then
-- Base case: Cur > Bound → True.
return;
end if;
-- Start <= Bound. Ghost_Is_NFD_From(Old_Out, Start, Bound, Last_CCC)
-- unfolds: Ghost_Valid(Old_Out, Start) holds, checks pass, etc.
-- Since bytes Start..Bound are identical, Ghost_Valid(New_Out, Start)
-- also holds, and all byte-level checks give the same result.
-- Help the solver see Ghost_Valid transfers.
pragma Assert (Old_Out (Start) = New_Out (Start));
pragma Assert (Ghost_Valid (New_Out, Start));
-- Step to next CP position.
declare
Step : constant Positive := Ghost_Step_Length (Old_Out, Start);
begin
pragma Assert (Ghost_Step_Length (New_Out, Start) = Step);
if Start > Bound - Step + 1 then
-- Last CP in the range: no further recursion.
return;
end if;
-- Recurse for the rest.
Lemma_NFD_Frame
(Old_Out, New_Out, Start + Step, Bound,
Get_CCC (Ghost_CP (Old_Out, Start)));
end;
end Lemma_NFD_Frame;
---------------------------------------------------------------------------
-- Lemma_NFD_Concat — ghost lemma for concatenating two NFD segments
--
-- If Output(Start..Mid) is NFD (with given Last_CCC) and
-- Output(Mid+1..End_Pos) is NFD starting with a starter (CCC = 0),
-- then Output(Start..End_Pos) is NFD (with the same Last_CCC).
--
-- Recursive: unfolds Ghost_Is_NFD_From one step at a time on the
-- prefix. When Start > Mid, the prefix is empty and the result
-- is the suffix (which starts with CCC=0).
--
-- The suffix's first CP has CCC=0, so the CCC ordering check at
-- the join point always passes (non-starter check is against 0).
---------------------------------------------------------------------------
procedure Lemma_NFD_Concat
(Output : Byte_Array;
Start : Positive;
Mid : Natural;
End_Pos : Natural;
Last_CCC : Normalization_Spec.CCC_Value)
with Ghost,
Pre => Initialized
and then Output'Last < Positive'Last
and then Start >= Output'First
and then End_Pos <= Output'Last
and then Mid >= Start - 1
and then Mid < End_Pos
and then Ghost_Is_NFD_From (Output, Start, Mid, Last_CCC)
and then Ghost_Valid (Output, Mid + 1)
and then Get_CCC (Ghost_CP (Output, Mid + 1)) = 0
and then Ghost_Is_NFD_From (Output, Mid + 1, End_Pos, 0),
Post => Ghost_Is_NFD_From (Output, Start, End_Pos, Last_CCC),
Subprogram_Variant => (Decreases => Mid - Start + 2)
is
begin
if Start > Mid then
-- Prefix is empty: Start = Mid + 1.
-- Ghost_Is_NFD_From(Output, Start, End_Pos, Last_CCC) unfolds:
-- Start <= End_Pos (since Mid < End_Pos and Start = Mid + 1).
-- Ghost_Valid at Start ✓ (from Pre: Ghost_Valid(Output, Mid+1)).
-- Ghost_Decomp_Len/Is_Hangul/CCC checks: suffix starts with
-- CCC=0 starter, so CCC check passes regardless of Last_CCC.
-- Then recursion into suffix gives Ghost_Is_NFD_From at next CP
-- with the suffix's CCC as Last_CCC.
-- The solver should unfold this one step and match the suffix Pre.
return;
end if;
-- Unfold one step at Start.
-- Ghost_Is_NFD_From(Output, Start, Mid, Last_CCC) gives us:
-- Ghost_Valid(Output, Start) ✓
-- Ghost_Decomp_Len = 0 ✓
-- not Is_Hangul_Syllable ✓
-- CCC ordering passes ✓
-- And either:
-- (a) Start is the last CP in prefix → base case
-- (b) Ghost_Is_NFD_From(Output, Start+Step, Mid, CCC_of_Start)
declare
Step : constant Positive := Ghost_Step_Length (Output, Start);
CP_CCC : constant CCC_Value :=
Get_CCC (Ghost_CP (Output, Start));
begin
if Start > Mid - Step + 1 then
-- Start is the last CP in the prefix.
-- Start + Step > Mid, and Mid + 1 is the suffix start.
-- Ghost_Is_NFD_From(Output, Start, End_Pos, Last_CCC) unfolds:
-- checks at Start pass, then recurse to Start + Step with
-- Last_CCC = CP_CCC. At Start + Step: if Start + Step = Mid + 1,
-- the suffix predicate applies directly. The suffix starts with
-- CCC=0, so the CCC check (CP_CCC vs CCC=0) passes.
return;
end if;
-- Recursive case: Start + Step <= Mid.
-- From unfolding the prefix predicate at Start:
-- Ghost_Is_NFD_From(Output, Start+Step, Mid, CP_CCC) holds.
-- Recurse with Start' = Start + Step, Last_CCC' = CP_CCC.
Lemma_NFD_Concat
(Output, Start + Step, Mid, End_Pos, CP_CCC);
-- After recursion:
-- Ghost_Is_NFD_From(Output, Start+Step, End_Pos, CP_CCC) holds.
-- One-step unfolding at Start with Last_CCC gives:
-- Ghost_Is_NFD_From(Output, Start, End_Pos, Last_CCC) =
-- checks at Start pass, then
-- Ghost_Is_NFD_From(Output, Start+Step, End_Pos, CP_CCC)
-- which we just established. ✓
end;
end Lemma_NFD_Concat;
---------------------------------------------------------------------------
-- Lemma_NFC_Frame — transfer Ghost_Is_NFC_From across identical ranges
--
-- Same pattern as Lemma_NFD_Frame but for the NFC predicate.
-- Ghost_Is_NFC_From uses NFC_Valid/NFC_CP/NFC_Step_Length (non-ghost
-- UTF-8 decode helpers that produce the same results as the ghost
-- versions when the underlying bytes are identical).
---------------------------------------------------------------------------
procedure Lemma_NFC_Frame
(Old_Out : Byte_Array;
New_Out : Byte_Array;
Start : Positive;
Bound : Natural;
Last_CCC : Normalization_Spec.CCC_Value;
Use_Canon : Boolean)
with Ghost,
Pre => Initialized
and then Old_Out'First = New_Out'First
and then Old_Out'Last = New_Out'Last
and then Old_Out'Last < Positive'Last
and then Start >= Old_Out'First
and then Bound <= Old_Out'Last
and then Ghost_Is_NFC_From (Old_Out, Start, Bound,
Last_CCC, Use_Canon)
and then (for all J in Start .. Bound =>
New_Out (J) = Old_Out (J)),
Post => Ghost_Is_NFC_From (New_Out, Start, Bound,
Last_CCC, Use_Canon),
Subprogram_Variant => (Decreases => Bound - Start + 1)
is
begin
if Start > Bound then
return;
end if;
pragma Assert (Old_Out (Start) = New_Out (Start));
pragma Assert (NFC_Valid (New_Out, Start));
declare
Step : constant Positive := NFC_Step_Length (Old_Out, Start);
begin
pragma Assert (NFC_Step_Length (New_Out, Start) = Step);
if Start > Bound - Step + 1 then
return;
end if;
Lemma_NFC_Frame
(Old_Out, New_Out, Start + Step, Bound,
Get_CCC (NFC_CP (Old_Out, Start)), Use_Canon);
end;
end Lemma_NFC_Frame;
---------------------------------------------------------------------------
-- Lemma_NFC_Concat — concatenate two NFC segments
--
-- Same pattern as Lemma_NFD_Concat but for the NFC predicate.
-- If Output(Start..Mid) is NFC and Output(Mid+1..End_Pos) is NFC
-- with the first CP being a starter (CCC=0), then
-- Output(Start..End_Pos) is NFC.
---------------------------------------------------------------------------
procedure Lemma_NFC_Concat
(Output : Byte_Array;
Start : Positive;
Mid : Natural;
End_Pos : Natural;
Last_CCC : Normalization_Spec.CCC_Value;
Use_Canon : Boolean)
with Ghost,
Pre => Initialized
and then Output'Last < Positive'Last
and then Start >= Output'First
and then End_Pos <= Output'Last
and then Mid >= Start - 1
and then Mid < End_Pos
and then Ghost_Is_NFC_From (Output, Start, Mid,
Last_CCC, Use_Canon)
and then NFC_Valid (Output, Mid + 1)
and then Get_CCC (NFC_CP (Output, Mid + 1)) = 0
and then Ghost_Is_NFC_From (Output, Mid + 1, End_Pos,
0, Use_Canon),
Post => Ghost_Is_NFC_From (Output, Start, End_Pos,
Last_CCC, Use_Canon),
Subprogram_Variant => (Decreases => Mid - Start + 2)
is
begin
if Start > Mid then
return;
end if;
declare
Step : constant Positive := NFC_Step_Length (Output, Start);
CP_CCC : constant CCC_Value :=
Get_CCC (NFC_CP (Output, Start));
begin
if Start > Mid - Step + 1 then
return;
end if;
Lemma_NFC_Concat
(Output, Start + Step, Mid, End_Pos, CP_CCC, Use_Canon);
end;
end Lemma_NFC_Concat;
---------------------------------------------------------------------------
-- Canonical_Order_Buffer
--
-- Applies canonical ordering to a codepoint buffer. Insertion sort
-- by CCC value, with starters (CCC = 0) acting as barriers.
-- Stable sort (only move when CCC is strictly greater).
--
-- Insertion sort has a naturally provable invariant: the first I-1
-- elements are pairwise CCC-ordered. When I reaches Len+1 this
-- gives the postcondition directly.
---------------------------------------------------------------------------
procedure Canonical_Order_Buffer
(Buf : in out CP_Work_Array;
CCC_Arr : in out CCC_Work_Array;
Len : Natural)
with Pre => Initialized
and then Len <= Max_Work_CPs
and then (for all I in 1 .. Len =>
Buf (I) <= Max_Codepoint)
and then (for all I in 1 .. Len =>
CCC_Arr (I) = CCC_Table (Buf (I))),
Post => (for all I in 1 .. Len - 1 =>
(CCC_Arr (I) = 0
or CCC_Arr (I + 1) = 0
or CCC_Arr (I) <= CCC_Arr (I + 1)))
and then
(for all I in 1 .. Len =>
Buf (I) <= Max_Codepoint)
and then
(for all I in 1 .. Len =>
CCC_Arr (I) = CCC_Table (Buf (I)))
and then
Ghost_Buf_Enc_Len (Buf, Len) =
Ghost_Buf_Enc_Len (Buf'Old, Len)
-- Permutation preserves pointwise properties:
-- sort only rearranges entries, so if all original entries
-- satisfy a predicate, all sorted entries do too.
and then
(if (for all J in 1 .. Len =>
Ghost_Decomp_Len (Buf'Old (J), True) = 0)
then (for all I in 1 .. Len =>
Ghost_Decomp_Len (Buf (I), True) = 0))
and then
(if (for all J in 1 .. Len =>
not Is_Hangul_Syllable (Buf'Old (J)))
then (for all I in 1 .. Len =>
not Is_Hangul_Syllable (Buf (I))))
-- Permutation preserves NFC_QC validity.
and then
(if (for all J in 1 .. Len =>
NFC_QC_Table (Buf'Old (J)) /= QC_No)
then (for all I in 1 .. Len =>
NFC_QC_Table (Buf (I)) /= QC_No))
-- Permutation preserves NFKC_QC validity.
and then
(if (for all J in 1 .. Len =>
NFKC_QC_Table (Buf'Old (J)) /= QC_No)
then (for all I in 1 .. Len =>
NFKC_QC_Table (Buf (I)) /= QC_No))
-- First entry CCC=0 preserved: starter stays at position 1
-- because stable bubble sort never swaps past a CCC=0 entry.
and then
(if Len >= 1 and then CCC_Table (Buf'Old (1)) = 0
then CCC_Table (Buf (1)) = 0),
Always_Terminates
is
begin
if Len <= 1 then
return;
end if;
for I in 2 .. Len loop
pragma Loop_Invariant (Initialized);
-- Platinum: positions 1 .. I-1 are pairwise CCC-ordered.
pragma Loop_Invariant
(for all K in 1 .. I - 2 =>
(CCC_Arr (K) = 0
or CCC_Arr (K + 1) = 0
or CCC_Arr (K) <= CCC_Arr (K + 1)));
-- Sum preservation: total encoded length unchanged.
pragma Loop_Invariant
(Ghost_Buf_Enc_Len (Buf, Len) =
Ghost_Buf_Enc_Len (Buf'Loop_Entry, Len));
-- All entries remain valid codepoints.
pragma Loop_Invariant
(for all K in 1 .. Len => Buf (K) <= Max_Codepoint);
-- CCC correspondence: CCC_Arr tracks CCC_Table for all entries.
pragma Loop_Invariant
(for all K in 1 .. Len =>
CCC_Arr (K) = CCC_Table (Buf (K)));
-- Permutation preserves pointwise predicates.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
Ghost_Decomp_Len (Buf'Loop_Entry (K), True) = 0)
then (for all K in 1 .. Len =>
Ghost_Decomp_Len (Buf (K), True) = 0));
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
not Is_Hangul_Syllable (Buf'Loop_Entry (K)))
then (for all K in 1 .. Len =>
not Is_Hangul_Syllable (Buf (K))));
-- Permutation preserves NFC_QC validity.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
NFC_QC_Table (Buf'Loop_Entry (K)) /= QC_No)
then (for all K in 1 .. Len =>
NFC_QC_Table (Buf (K)) /= QC_No));
-- Permutation preserves NFKC_QC validity.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
NFKC_QC_Table (Buf'Loop_Entry (K)) /= QC_No)
then (for all K in 1 .. Len =>
NFKC_QC_Table (Buf (K)) /= QC_No));
-- First entry CCC=0 preserved: starter at pos 1 never moves.
pragma Loop_Invariant
(if CCC_Table (Buf'Loop_Entry (1)) = 0
then CCC_Table (Buf (1)) = 0);
-- Starters (CCC = 0) act as barriers — they never move.
-- The pair (I-1, I) with CCC_Arr(I) = 0 is allowed by the
-- postcondition, so nothing to do.
if CCC_Arr (I) /= 0 then
declare
Key_CP : constant Natural := Buf (I);
Key_CCC : constant CCC_Value := CCC_Arr (I);
J : Positive := I;
-- Ghost: sum before this insertion step.
Sum_Before : constant Natural :=
Ghost_Buf_Enc_Len (Buf, Len) with Ghost;
begin
pragma Assert (Key_CP <= Max_Codepoint);
pragma Assert (Buf (J) <= Max_Codepoint);
-- CCC correspondence for key: Key_CCC = CCC_Table(Key_CP).
pragma Assert (Key_CCC = CCC_Table (Key_CP));
-- Establish sum-tracking property before while loop.
-- J = I and Key_CP = Buf(I) = Buf(J), so:
-- GBEL(Buf, Len) + EL(Key_CP)
-- = Sum_Before + EL(Key_CP)
-- = Sum_Before + EL(Buf(J))
pragma Assert
(Ghost_Buf_Enc_Len (Buf, Len)
+ UTF8_Spec.Encoded_Length (Key_CP)
= Sum_Before
+ UTF8_Spec.Encoded_Length (Buf (J)));
-- Shift elements right while CCC_Arr(J-1) > Key_CCC,
-- stopping at a starter or the array start.
while J > 1
and then CCC_Arr (J - 1) /= 0
and then CCC_Arr (J - 1) > Key_CCC
loop
pragma Loop_Invariant (Initialized);
pragma Loop_Invariant (J in 2 .. I);
-- Frame: CCC positions 1 .. J are untouched.
pragma Loop_Invariant
(for all K in 1 .. J =>
CCC_Arr (K) = CCC_Arr'Loop_Entry (K));
-- Frame: Buf positions 1 .. J are untouched.
pragma Loop_Invariant
(for all K in 1 .. J =>
Buf (K) = Buf'Loop_Entry (K));
-- All entries remain valid codepoints (permutation).
pragma Loop_Invariant
(for all K in 1 .. Len => Buf (K) <= Max_Codepoint);
-- CCC_Arr(J) is non-zero (from frame or Key_CCC).
pragma Loop_Invariant (CCC_Arr (J) /= 0);
-- Shifted suffix J+1 .. I connects to frame.
pragma Loop_Invariant
(if J < I then
CCC_Arr (J + 1) = CCC_Arr'Loop_Entry (J));
-- Shifted suffix J+1 .. I is sorted.
pragma Loop_Invariant
(for all K in J + 1 .. I - 1 =>
CCC_Arr (K) <= CCC_Arr (K + 1));
-- All elements in shifted region have CCC > Key_CCC.
pragma Loop_Invariant
(for all K in J + 1 .. I =>
CCC_Arr (K) > Key_CCC);
-- CCC correspondence: CCC_Arr tracks CCC_Table.
pragma Loop_Invariant
(for all K in 1 .. Len =>
CCC_Arr (K) = CCC_Table (Buf (K)));
-- Sum tracking: Buf(J) is in the frame (original
-- value). The sum "lost" Key_CP at position I and
-- "gained" a duplicate of Buf(J) via shifting.
pragma Loop_Invariant
(Ghost_Buf_Enc_Len (Buf, Len)
+ UTF8_Spec.Encoded_Length (Key_CP)
= Sum_Before
+ UTF8_Spec.Encoded_Length (Buf (J)));
-- Permutation preserves pointwise predicates.
-- Shifting copies existing values; no new values introduced.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
Ghost_Decomp_Len (Buf'Loop_Entry (K), True) = 0)
then (for all K in 1 .. Len =>
Ghost_Decomp_Len (Buf (K), True) = 0));
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
not Is_Hangul_Syllable (Buf'Loop_Entry (K)))
then (for all K in 1 .. Len =>
not Is_Hangul_Syllable (Buf (K))));
-- Permutation preserves NFC_QC validity.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
NFC_QC_Table (Buf'Loop_Entry (K)) /= QC_No)
then (for all K in 1 .. Len =>
NFC_QC_Table (Buf (K)) /= QC_No));
-- Permutation preserves NFKC_QC validity.
pragma Loop_Invariant
(if (for all K in 1 .. Len =>
NFKC_QC_Table (Buf'Loop_Entry (K)) /= QC_No)
then (for all K in 1 .. Len =>
NFKC_QC_Table (Buf (K)) /= QC_No));
-- First entry CCC=0 preserved (pos 1 in frame: 1 <= J).
pragma Loop_Invariant
(if CCC_Table (Buf'Loop_Entry (1)) = 0
then CCC_Table (Buf (1)) = 0);
pragma Loop_Variant (Decreases => J);
-- Snapshot for lemma call.
declare
Buf_Pre : constant CP_Work_Array := Buf with Ghost;
Old_J_Val : constant Natural := Buf (J) with Ghost;
begin
Buf (J) := Buf (J - 1);
CCC_Arr (J) := CCC_Arr (J - 1);
-- Prove the shift preserves sum via Lemma_Update_At.
-- Position J changed from Old_J_Val to Buf(J-1).
-- Buf_Pre and Buf agree everywhere except at J.
pragma Assert (Buf_Pre (J) = Old_J_Val);
pragma Assert (Buf (J) = Buf_Pre (J - 1));
pragma Assert (Old_J_Val <= Max_Codepoint);
pragma Assert (Buf (J) <= Max_Codepoint);
Lemma_Update_At
(Buf_Pre, Buf, Len, J, Old_J_Val, Buf_Pre (J - 1));
-- From the lemma:
-- GBEL(Buf, Len) + EL(Old_J_Val)
-- = GBEL(Buf_Pre, Len) + EL(Buf_Pre(J-1))
--
-- From the invariant (Buf_Pre = Buf at invariant):
-- GBEL(Buf_Pre, Len) + EL(Key_CP)
-- = Sum_Before + EL(Buf_Pre(J))
-- = Sum_Before + EL(Old_J_Val)
--
-- So GBEL(Buf_Pre, Len) = Sum_Before + EL(Old_J_Val) - EL(Key_CP)
-- Subst: GBEL(Buf, Len) + EL(Old_J_Val)
-- = Sum_Before + EL(Old_J_Val) - EL(Key_CP) + EL(Buf_Pre(J-1))
-- => GBEL(Buf, Len)
-- = Sum_Before - EL(Key_CP) + EL(Buf_Pre(J-1))
-- => GBEL(Buf, Len) + EL(Key_CP)
-- = Sum_Before + EL(Buf_Pre(J-1))
-- Buf_Pre(J-1) = Buf(J-1) (unchanged)
-- After J := J-1, new Buf(J) = old Buf(J-1)
pragma Assert
(Ghost_Buf_Enc_Len (Buf, Len)
+ UTF8_Spec.Encoded_Length (Key_CP)
= Sum_Before
+ UTF8_Spec.Encoded_Length (Buf (J - 1)));
end;
-- After the copy: CCC_Arr(J) = CCC_Arr(J-1).
pragma Assert (CCC_Arr (J - 1) = CCC_Arr (J));
if J < I then
pragma Assert (CCC_Arr (J) <= CCC_Arr (J + 1));
end if;
-- The suffix including the new pair is sorted.
pragma Assert
(for all K in J - 1 .. I - 1 =>
CCC_Arr (K) <= CCC_Arr (K + 1));
J := J - 1;
end loop;
-- Sum property holds here: either from while loop
-- invariant (1+ iterations) or pre-loop assertion (0 iters).
pragma Assert
(Ghost_Buf_Enc_Len (Buf, Len)
+ UTF8_Spec.Encoded_Length (Key_CP)
= Sum_Before
+ UTF8_Spec.Encoded_Length (Buf (J)));
-- Insert Key_CP at position J.
-- From the sum property:
-- GBEL(Buf, Len) + EL(Key_CP) = Sum_Before + EL(Buf(J))
-- After writing Key_CP at J, the sum changes by
-- EL(Key_CP) - EL(old Buf(J)).
-- New sum = old sum + EL(Key_CP) - EL(old Buf(J))
-- = Sum_Before + EL(Buf(J)) - EL(Key_CP)
-- + EL(Key_CP) - EL(Buf(J))
-- = Sum_Before.
declare
Buf_Pre2 : constant CP_Work_Array := Buf with Ghost;
Old_J_Val2 : constant Natural := Buf (J) with Ghost;
begin
Buf (J) := Key_CP;
CCC_Arr (J) := Key_CCC;
pragma Assert (Buf_Pre2 (J) = Old_J_Val2);
pragma Assert (Buf (J) = Key_CP);
pragma Assert (Old_J_Val2 <= Max_Codepoint);
pragma Assert (Key_CP <= Max_Codepoint);
Lemma_Update_At
(Buf_Pre2, Buf, Len, J, Old_J_Val2, Key_CP);
-- Lemma gives:
-- GBEL(Buf, Len) + EL(Old_J_Val2)
-- = GBEL(Buf_Pre2, Len) + EL(Key_CP)
--
-- From invariant: GBEL(Buf_Pre2, Len) + EL(Key_CP)
-- = Sum_Before + EL(Old_J_Val2)
-- So: GBEL(Buf_Pre2, Len) = Sum_Before + EL(Old_J_Val2) - EL(Key_CP)
-- Subst: GBEL(Buf, Len) + EL(Old_J_Val2)
-- = Sum_Before + EL(Old_J_Val2) - EL(Key_CP) + EL(Key_CP)
-- = Sum_Before + EL(Old_J_Val2)
-- => GBEL(Buf, Len) = Sum_Before ✓
pragma Assert
(Ghost_Buf_Enc_Len (Buf, Len) = Sum_Before);
-- CCC correspondence: Key_CCC = CCC_Table(Key_CP),
-- and we just set Buf(J) := Key_CP, CCC_Arr(J) := Key_CCC.
-- Other positions unchanged from while loop exit.
pragma Assert
(for all K in 1 .. Len =>
CCC_Arr (K) = CCC_Table (Buf (K)));
end;
end;
end if;
-- After processing element I (either a starter left in place,
-- or a non-starter inserted at its correct position), all
-- pairs 1..I-1 are CCC-ordered.
pragma Assert
(for all K in 1 .. I - 1 =>
(CCC_Arr (K) = 0
or CCC_Arr (K + 1) = 0
or CCC_Arr (K) <= CCC_Arr (K + 1)));
end loop;
end Canonical_Order_Buffer;
---------------------------------------------------------------------------
-- Compose_Buffer
--
-- Applies the Canonical Composition Algorithm to a decomposed,
-- canonically ordered codepoint buffer.
--
-- Marks composed characters with Max_Codepoint + 1 (sentinel),
-- then compacts the buffer.
---------------------------------------------------------------------------
Deleted_Marker : constant := Max_Codepoint + 1;
procedure Compose_Buffer
(Buf : in out CP_Work_Array;
CCC_Arr : in out CCC_Work_Array;
Len : in out Natural;
Use_Canon : Boolean)
with Pre => Initialized
and then Data_All_Terminal
and then Len <= Max_Work_CPs
-- All input CPs are valid codepoints.
and then (for all I in 1 .. Len =>
Buf (I) <= Max_Codepoint)
-- CCC correspondence.
and then (for all I in 1 .. Len =>
CCC_Arr (I) = CCC_Table (Buf (I)))
-- QC validity for all input CPs.
and then (for all I in 1 .. Len =>
(if Use_Canon
then NFC_QC_Table (Buf (I)) /= QC_No
else NFKC_QC_Table (Buf (I)) /= QC_No)),
Post => Len <= Max_Work_CPs
and then Len <= Len'Old
-- All output CPs are valid codepoints.
and then (for all I in 1 .. Len =>
Buf (I) <= Max_Codepoint)
-- CCC correspondence.
and then (for all I in 1 .. Len =>
CCC_Arr (I) = CCC_Table (Buf (I)))
-- QC validity preserved through composition.
and then (for all I in 1 .. Len =>
(if Use_Canon
then NFC_QC_Table (Buf (I)) /= QC_No
else NFKC_QC_Table (Buf (I)) /= QC_No))
-- First-starter preservation: if the input starts with a
-- starter (CCC=0), the output also starts with a starter.
-- Compose_Buffer never deletes entry 1: it only marks
-- later entries (I >= 2) as deleted, or replaces Buf(1)
-- with a composition result whose CCC is forced to 0
-- (Hangul branches set CCC explicitly; table-composition
-- branches gate on CCC_Table(Composite) = 0).
and then (if Len'Old >= 1
and then CCC_Arr'Old (1) = 0
and then Len >= 1
then CCC_Arr (1) = 0
and then CCC_Table (Buf (1)) = 0),
Always_Terminates
is
Starter_Idx : Natural := 0;
Composite : Natural;
begin
if Len <= 1 then
return;
end if;
-- Find first starter
for I in 1 .. Len loop
if CCC_Arr (I) = 0 then
Starter_Idx := I;
exit;
end if;
end loop;
if Starter_Idx = 0 then
return; -- No starters at all
end if;
for I in Starter_Idx + 1 .. Len loop
pragma Loop_Invariant (Starter_Idx >= 1 and Starter_Idx < I);
pragma Loop_Invariant (Len <= Max_Work_CPs);
-- QC validity: all non-deleted entries satisfy NFC/NFKC QC.
pragma Loop_Invariant
(for all K in 1 .. Len =>
(if Buf (K) <= Max_Codepoint then
(if Use_Canon
then NFC_QC_Table (Buf (K)) /= QC_No
else NFKC_QC_Table (Buf (K)) /= QC_No)));
-- CCC correspondence for non-deleted entries.
pragma Loop_Invariant
(for all K in 1 .. Len =>
(if Buf (K) <= Max_Codepoint then
CCC_Arr (K) = CCC_Table (Buf (K))));
-- First-starter preservation through composition.
--
-- If entry 1 was a starter on entry to this loop, it stays
-- a starter:
-- * Buf (1) is never marked Deleted_Marker (only Buf (I)
-- for I >= Starter_Idx + 1 >= 2 is deleted), so position
-- 1 stays a valid CP.
-- * The only writes to CCC_Arr (Starter_Idx) (Hangul L+V,
-- Hangul LV+T, table composition) all yield CCC = 0:
-- Hangul branches assign 0 explicitly; table-composition
-- branches gate on CCC_Table (Composite) = 0.
pragma Loop_Invariant
(if CCC_Arr'Loop_Entry (1) = 0 then
Buf (1) <= Max_Codepoint
and then CCC_Arr (1) = 0
and then CCC_Table (Buf (1)) = 0);
if Buf (I) > Max_Codepoint then
-- Already deleted
null;
elsif Buf (Starter_Idx) > Max_Codepoint then
-- Starter was deleted (shouldn't happen), treat I as new starter
if CCC_Arr (I) = 0 then
Starter_Idx := I;
end if;
elsif CCC_Arr (I) = 0 then
-- I is a starter
-- Check if it composes with the previous starter
-- Only if they're adjacent (no intervening non-deleted chars)
declare
Blocked : Boolean := False;
S_CP : constant Codepoint := Buf (Starter_Idx);
I_CP : constant Codepoint := Buf (I);
begin
-- Check for blocking characters between Starter_Idx and I
for J in Starter_Idx + 1 .. I - 1 loop
if Buf (J) <= Max_Codepoint then
Blocked := True;
exit;
end if;
end loop;
if not Blocked then
-- Try Hangul L + V composition
if Is_Hangul_L (S_CP)
and then Is_Hangul_V (I_CP)
then
declare
LV : constant Natural :=
SBase
+ (S_CP - LBase) * NCount
+ (I_CP - VBase) * TCount;
begin
-- LV is a Hangul syllable → QC ≠ QC_No, CCC = 0.
pragma Assert (LV >= SBase and then LV <= SBase + SCount - 1);
pragma Assert (LV <= Max_Codepoint);
-- From Data_All_Terminal: every Hangul syllable
-- has CCC = 0 and NFC_QC /= QC_No. Spell out
-- the instance the loop invariant needs at K =
-- Starter_Idx after the write below.
pragma Assert (CCC_Table (LV) = 0);
pragma Assert (NFC_QC_Table (LV) /= QC_No);
pragma Assert (NFKC_QC_Table (LV) /= QC_No);
Buf (Starter_Idx) := LV;
CCC_Arr (Starter_Idx) := 0;
Buf (I) := Deleted_Marker;
end;
goto Next;
end if;
-- Try Hangul LV + T composition
if Is_Hangul_LV (S_CP)
and then Is_Hangul_T (I_CP)
then
declare
LVT : constant Natural := S_CP + (I_CP - TBase);
begin
-- LVT is a Hangul syllable → QC ≠ QC_No, CCC = 0.
pragma Assert (LVT >= SBase and then LVT <= SBase + SCount - 1);
pragma Assert (LVT <= Max_Codepoint);
-- From Data_All_Terminal: every Hangul syllable
-- has CCC = 0 and NFC_QC /= QC_No.
pragma Assert (CCC_Table (LVT) = 0);
pragma Assert (NFC_QC_Table (LVT) /= QC_No);
pragma Assert (NFKC_QC_Table (LVT) /= QC_No);
Buf (Starter_Idx) := LVT;
CCC_Arr (Starter_Idx) := 0;
Buf (I) := Deleted_Marker;
end;
goto Next;
end if;
-- Try table composition.
-- Gate on CCC = 0: only commit a composition when
-- the result is itself a starter. This preserves
-- the first-starter property of the buffer (a
-- property carried in Compose_Buffer's Post and
-- consumed downstream by Flush_Segment). Per
-- Unicode, primary composites are always starters,
-- so this gate is a defensive no-op for conforming
-- data.
Composite :=
Lookup_Composition (S_CP, I_CP);
if Composite <= Max_Codepoint
and then CCC_Table (Composite) = 0
then
-- Lookup_Composition postcondition: QC ≠ QC_No.
Buf (Starter_Idx) := Composite;
CCC_Arr (Starter_Idx) :=
CCC_Table (Composite);
Buf (I) := Deleted_Marker;
goto Next;
end if;
end if;
-- No composition — this becomes the new starter
Starter_Idx := I;
end;
else
-- I is a non-starter (CCC > 0) — Buf(I) <= Max_Codepoint
-- Check if it's blocked from the last starter
declare
Blocked : Boolean := False;
I_CCC : constant CCC_Value := CCC_Arr (I);
S_CP : constant Codepoint := Buf (Starter_Idx);
I_CP : constant Codepoint := Buf (I);
begin
for J in Starter_Idx + 1 .. I - 1 loop
if Buf (J) <= Max_Codepoint
and then CCC_Arr (J) >= I_CCC
then
Blocked := True;
exit;
end if;
end loop;
if not Blocked then
-- Same CCC = 0 gate as the starter+starter branch:
-- guarantees first-starter preservation in Post.
Composite :=
Lookup_Composition (S_CP, I_CP);
if Composite <= Max_Codepoint
and then CCC_Table (Composite) = 0
then
Buf (Starter_Idx) := Composite;
CCC_Arr (Starter_Idx) :=
CCC_Table (Composite);
Buf (I) := Deleted_Marker;
end if;
end if;
end;
end if;
<<Next>>
null;
end loop;
-- Compact: remove deleted entries.
-- Source entries at I..Len are untouched by this loop (Write_Idx < I
-- always holds, so writes at Write_Idx never overwrite source I).
-- Their CCC/QC properties from the composition loop above must be
-- preserved as a loop invariant so that copies to Write_Idx
-- re-establish the destination invariant.
declare
Write_Idx : Natural := 0;
begin
for I in 1 .. Len loop
pragma Loop_Invariant (Write_Idx < I);
pragma Loop_Invariant (Write_Idx <= Max_Work_CPs);
-- Source range I..Len is untouched: properties carry over
-- from the composition loop's exit state.
pragma Loop_Invariant
(for all K in I .. Len =>
(if Buf (K) <= Max_Codepoint then
(if Use_Canon
then NFC_QC_Table (Buf (K)) /= QC_No
else NFKC_QC_Table (Buf (K)) /= QC_No)
and then CCC_Arr (K) = CCC_Table (Buf (K))));
-- All compacted entries so far are valid and satisfy QC.
pragma Loop_Invariant
(for all K in 1 .. Write_Idx =>
Buf (K) <= Max_Codepoint
and then (if Use_Canon
then NFC_QC_Table (Buf (K)) /= QC_No
else NFKC_QC_Table (Buf (K)) /= QC_No)
and then CCC_Arr (K) = CCC_Table (Buf (K)));
-- First-starter preservation: if the post-composition state
-- has a starter at position 1, compaction never overwrites
-- it. At I=1 the body's self-write sets Write_Idx := 1, so
-- for all subsequent iterations Write_Idx >= 1 and writes go
-- to positions >= 2.
pragma Loop_Invariant
(if Buf'Loop_Entry (1) <= Max_Codepoint
and then CCC_Arr'Loop_Entry (1) = 0
then
(if I = 1
then Buf (1) = Buf'Loop_Entry (1)
and then CCC_Arr (1) = 0)
and then (if I > 1
then Write_Idx >= 1
and then Buf (1) = Buf'Loop_Entry (1)
and then CCC_Arr (1) = 0));
if Buf (I) <= Max_Codepoint then
Write_Idx := Write_Idx + 1;
Buf (Write_Idx) := Buf (I);
CCC_Arr (Write_Idx) := CCC_Arr (I);
end if;
end loop;
Len := Write_Idx;
end;
end Compose_Buffer;
---------------------------------------------------------------------------
-- Normalization — segment-based processing
--
-- The work buffer holds one segment at a time. Segments between
-- normalization boundaries are small (max ~30 CPs in Unicode), so the
-- 256-entry buffer never overflows for valid Unicode input.
--
-- Buffer_Overflow from Normalize means the OUTPUT buffer is too small.
---------------------------------------------------------------------------
subtype Seg_Length is Natural range 0 .. Max_Work_CPs;
type Norm_Process_State is record
CP_Buf : CP_Work_Array;
CCC_Buf : CCC_Work_Array;
Seg_Len : Seg_Length;
Do_Compose : Boolean;
Use_Canon : Boolean;
end record;
-- Flush the segment in St.CP_Buf(1..St.Seg_Len) to Output.
-- Canonical order, compose (if NFC/NFKC), encode to UTF-8.
-- Resets St.Seg_Len to 0.
procedure Flush_Segment
(St : in out Norm_Process_State;
Output : in out Byte_Array;
Pos : in out Natural;
OK : in out Boolean)
with Pre => Initialized
and then Data_All_Terminal
and then Output'Last < Positive'Last
and then Pos >= Output'First
and then Pos <= Output'Last + 1
and then OK
-- NFD readiness: all buffer entries are terminal CPs
and then (if not St.Do_Compose then
(for all I in 1 .. St.Seg_Len =>
St.CP_Buf (I) <= Max_Codepoint
and then Ghost_Decomp_Len (St.CP_Buf (I), True) = 0
and then not Is_Hangul_Syllable (St.CP_Buf (I))))
-- First buffer entry is a starter (for concat at boundary).
-- Only required when the segment will be concatenated with
-- prior output. The very first segment (no prior output)
-- may start with a non-starter.
and then (if not St.Do_Compose and then St.Seg_Len >= 1
and then Pos > Output'First
then CCC_Table (St.CP_Buf (1)) = 0)
-- NFD accumulator: all output so far is in NFD form.
-- Passed from caller's loop invariant.
and then (if not St.Do_Compose and then Pos > Output'First
then Ghost_Is_NFD (Output, Output'First, Pos - 1))
-- NFC path: buffer entries have NFC/NFKC QC ≠ QC_No.
-- Terminal decomposition CPs satisfy this by Data_All_Terminal.
and then (if St.Do_Compose then
(for all I in 1 .. St.Seg_Len =>
St.CP_Buf (I) <= Max_Codepoint
and then (if St.Use_Canon
then NFC_QC_Table (St.CP_Buf (I)) /= QC_No
else NFKC_QC_Table (St.CP_Buf (I)) /= QC_No)))
-- NFC first-starter: same as NFD case. When the segment will
-- be concatenated with prior output, position 1 must be a
-- starter so the boundary CCC=0 is preserved across
-- composition (used by Ghost_NFC_Reverse to derive that the
-- segment-start CP in the encoded output is a starter).
and then (if St.Do_Compose and then St.Seg_Len >= 1
and then Pos > Output'First
then CCC_Table (St.CP_Buf (1)) = 0)
-- NFC accumulator: all output so far is in NFC form.
-- Passed from caller's loop invariant.
and then (if St.Do_Compose and then Pos > Output'First
then Ghost_Is_NFC (Output, Output'First, Pos - 1,
St.Use_Canon)),
Post => St.Seg_Len = 0
and then St.Do_Compose = St.Do_Compose'Old
and then St.Use_Canon = St.Use_Canon'Old
and then Pos >= Pos'Old
and then Pos <= Output'Last + 1
and then (if OK and then not St.Do_Compose'Old then
Pos - Pos'Old =
Ghost_Buf_Enc_Len
(St'Old.CP_Buf, St'Old.Seg_Len))
-- NFD content: encoded output is in NFD form
and then (if OK and then not St.Do_Compose'Old
and then Pos > Pos'Old
then Ghost_Is_NFD_From
(Output, Pos'Old, Pos - 1, 0))
-- NFD accumulator: full output is in NFD form.
-- Combines pre-existing NFD prefix with new segment.
and then (if OK and then not St.Do_Compose'Old
and then Pos > Output'First
then Ghost_Is_NFD (Output, Output'First, Pos - 1))
-- NFC content: encoded output is in NFC form
and then (if OK and then St.Do_Compose'Old
and then Pos > Pos'Old
then Ghost_Is_NFC_From
(Output, Pos'Old, Pos - 1, 0,
St'Old.Use_Canon))
-- NFC accumulator: full output is in NFC form.
-- Combines pre-existing NFC prefix with new segment.
and then (if OK and then St.Do_Compose'Old
and then Pos > Output'First
then Ghost_Is_NFC (Output, Output'First, Pos - 1,
St'Old.Use_Canon))
-- Output frame: bytes before Pos'Old unchanged
and then (for all J in Output'Range =>
(if J < Pos'Old then
Output (J) = Output'Old (J))),
Always_Terminates
is
Enc_Len : Positive;
-- Ghost: original buffer sum and starting position for
-- byte-count tracking in NFD path.
Orig_Sum : Natural with Ghost;
Pos_Start : Natural with Ghost;
-- Ghost: trace of output positions for two-phase NFD proof.
-- Trace(I) = output position where CP_Buf(I) was encoded.
type Trace_Array is array (1 .. Max_Work_CPs) of Natural;
Trace : Trace_Array := [others => 0] with Ghost;
Old_Seg_Len : Seg_Length with Ghost;
begin
if St.Seg_Len = 0 then
return;
end if;
-- Fill CCC buffer and validate entries.
-- All entries should be valid codepoints (from decomposition).
-- The loop invariant tracks validity for the prover.
for I in 1 .. St.Seg_Len loop
pragma Loop_Invariant
(for all K in 1 .. I - 1 => St.CP_Buf (K) <= Max_Codepoint);
pragma Loop_Invariant
(for all K in 1 .. I - 1 =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K)));
if St.CP_Buf (I) > Max_Codepoint then
-- Defensive: should never happen in practice.
St.Seg_Len := 0;
OK := False;
return;
end if;
St.CCC_Buf (I) := CCC_Table (St.CP_Buf (I));
end loop;
-- Capture original buffer sum before sort.
Orig_Sum := Ghost_Buf_Enc_Len (St.CP_Buf, St.Seg_Len);
Pos_Start := Pos;
-- Canonical ordering (preserves Ghost_Buf_Enc_Len)
Canonical_Order_Buffer (St.CP_Buf, St.CCC_Buf, St.Seg_Len);
-- Sum preserved after sort.
pragma Assert
(Ghost_Buf_Enc_Len (St.CP_Buf, St.Seg_Len) = Orig_Sum);
-- Compose (NFC / NFKC only)
if St.Do_Compose then
Compose_Buffer (St.CP_Buf, St.CCC_Buf, St.Seg_Len, St.Use_Canon);
-- Re-establish canonical ordering after composition: composition
-- may leave non-starters out of CCC order (e.g., after a starter
-- swallows a leading non-starter into a composite, the remaining
-- non-starters keep their original positions but lose the
-- pre-composition ordering invariant). Canonical_Order_Buffer's
-- Post unconditionally re-establishes ordering and preserves
-- CCC correspondence + first-starter property.
Canonical_Order_Buffer (St.CP_Buf, St.CCC_Buf, St.Seg_Len);
end if;
-- Capture segment length before encoding (for reverse loop).
Old_Seg_Len := St.Seg_Len;
-- Ghost copy of Output before encoding, for NFD frame transfer.
-- After encoding, Lemma_NFD_Frame proves the prefix NFD transfers
-- from Output_Entry to the modified Output.
declare
Output_Entry : constant Byte_Array (Output'Range) := Output with Ghost;
begin
-- Trace(1) = Pos_Start — set before the loop so it persists.
Trace (1) := Pos;
-- Phase 1: Encode to UTF-8, recording ghost trace positions.
for I in 1 .. St.Seg_Len loop
pragma Loop_Invariant (Pos >= Pos_Start);
pragma Loop_Invariant (Pos >= Output'First);
pragma Loop_Invariant (Pos <= Output'Last + 1);
pragma Loop_Invariant (OK);
pragma Loop_Invariant (Old_Seg_Len = St.Seg_Len);
-- Byte count: bytes written so far = sum of first I-1 entries.
-- Only valid for NFD path (not compose).
pragma Loop_Invariant
(if not St.Do_Compose then
Pos - Pos_Start =
Ghost_Buf_Enc_Len (St.CP_Buf, I - 1));
-- Entries remain valid after sort (sort postcondition).
pragma Loop_Invariant
(if not St.Do_Compose then
(for all K in 1 .. St.Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint));
-- CCC correspondence survives sort.
pragma Loop_Invariant
(if not St.Do_Compose then
(for all K in 1 .. St.Seg_Len =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K))));
-- Ghost trace: Trace(K) records position where CP K was encoded.
-- The encoding occupies Encoded_Length bytes starting at
-- Trace(K), and the end of the encoding is at or before Pos.
-- Encoded_At is a per-byte predicate preserved by the frame
-- condition from Encode (bytes < Pos are unchanged).
pragma Loop_Invariant
(if not St.Do_Compose and then I >= 2 then
(for all K in 1 .. I - 1 =>
Trace (K) >= Pos_Start
and then Trace (K) in Output'Range
and then St.CP_Buf (K) <= Max_Codepoint
and then Is_Scalar_Value (St.CP_Buf (K))
and then Trace (K) + UTF8_Spec.Encoded_Length
(St.CP_Buf (K)) <= Pos
and then UTF8_Spec.Encoded_At
(Output, Trace (K), St.CP_Buf (K))
-- Step: consecutive entries separated by EL.
and then (if K >= 2 then
Trace (K) = Trace (K - 1) +
UTF8_Spec.Encoded_Length
(St.CP_Buf (K - 1)))));
-- Trace(1) = Pos_Start: first entry starts at the beginning.
pragma Loop_Invariant
(if not St.Do_Compose and then I >= 2 then
Trace (1) = Pos_Start);
-- Track: Pos = Trace(I-1) + EL(I-1) for previous entry.
pragma Loop_Invariant
(if not St.Do_Compose and then I >= 2 then
Pos = Trace (I - 1) +
UTF8_Spec.Encoded_Length (St.CP_Buf (I - 1)));
-- NFC PATH: post-Compose buffer state survives the loop.
-- Compose_Buffer's postcondition guarantees CP bounds, CCC
-- correspondence, and NFC_QC validity for all 1..Seg_Len.
pragma Loop_Invariant
(if St.Do_Compose then
(for all K in 1 .. St.Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint));
pragma Loop_Invariant
(if St.Do_Compose then
(for all K in 1 .. St.Seg_Len =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K))));
pragma Loop_Invariant
(if St.Do_Compose then
(for all K in 1 .. St.Seg_Len =>
(if St.Use_Canon
then NFC_QC_Table (St.CP_Buf (K)) /= QC_No
else NFKC_QC_Table (St.CP_Buf (K)) /= QC_No)));
-- NFC PATH: at start of iteration I, Pos relationship.
-- When I=1, Pos = Pos_Start (no encoding done yet).
-- When I>=2, Pos = Trace(I-1) + Encoded_Length(CP_Buf(I-1)).
pragma Loop_Invariant
(if St.Do_Compose and then I = 1 then
Pos = Pos_Start);
pragma Loop_Invariant
(if St.Do_Compose and then I >= 2 then
Pos = Trace (I - 1) +
UTF8_Spec.Encoded_Length (St.CP_Buf (I - 1)));
-- NFC PATH: trace properties (analogous to NFD path).
pragma Loop_Invariant
(if St.Do_Compose and then I >= 2 then
(for all K in 1 .. I - 1 =>
Trace (K) >= Pos_Start
and then Trace (K) in Output'Range
and then St.CP_Buf (K) <= Max_Codepoint
and then Is_Scalar_Value (St.CP_Buf (K))
and then Trace (K) + UTF8_Spec.Encoded_Length
(St.CP_Buf (K)) <= Pos
and then UTF8_Spec.Encoded_At
(Output, Trace (K), St.CP_Buf (K))
and then (if K >= 2 then
Trace (K) = Trace (K - 1) +
UTF8_Spec.Encoded_Length
(St.CP_Buf (K - 1)))));
pragma Loop_Invariant
(if St.Do_Compose then
Trace (1) = Pos_Start);
-- Output frame: bytes before Pos_Start unchanged (vs entry).
pragma Loop_Invariant
(for all J in Output'Range =>
(if J < Pos_Start then
Output (J) = Output_Entry (J)));
-- Record ghost trace position before encoding.
Trace (I) := Pos;
declare
Val : constant Natural := St.CP_Buf (I);
begin
if Val > Max_Codepoint then
St.Seg_Len := 0;
OK := False;
return;
end if;
declare
C : constant Codepoint := Val;
begin
if not Is_Scalar_Value (C) then
St.Seg_Len := 0;
OK := False;
return;
end if;
Enc_Len := (if C <= 16#7F# then 1
elsif C <= 16#7FF# then 2
elsif C <= 16#FFFF# then 3
else 4);
if Pos > Output'Last
or else Output'Last - Pos < Enc_Len - 1
then
St.Seg_Len := 0;
OK := False;
return;
end if;
UTF8.Encode (C, Output, Pos, Enc_Len);
Pos := Pos + Enc_Len;
-- After encoding entry I:
-- Pos - Pos_Start = Ghost_Buf_Enc_Len(Buf, I)
-- Because GBEL(Buf, I) = GBEL(Buf, I-1) + EL(Buf(I))
-- and Pos increased by EL(C) = EL(Buf(I)).
end;
end;
end loop;
-- Trace(1) = Pos_Start: from pre-loop assignment + Phase 1 preserves it.
pragma Assert
(if not St.Do_Compose and then Pos > Pos_Start
then Trace (1) = Pos_Start);
-- Post-Phase 1 summary: Encoded_At for all entries.
-- Extracting from the Phase 1 loop invariant while still available.
pragma Assert
(if not St.Do_Compose and then Old_Seg_Len >= 1 then
(for all K in 1 .. Old_Seg_Len =>
Trace (K) >= Pos_Start
and then Trace (K) in Output'Range
and then St.CP_Buf (K) <= Max_Codepoint
and then Is_Scalar_Value (St.CP_Buf (K))
and then UTF8_Spec.Encoded_At
(Output, Trace (K), St.CP_Buf (K))));
-- Post-Phase 1 summary for NFC path: Encoded_At + post-Compose facts.
pragma Assert
(if St.Do_Compose and then Old_Seg_Len >= 1 then
(for all K in 1 .. Old_Seg_Len =>
Trace (K) >= Pos_Start
and then Trace (K) in Output'Range
and then St.CP_Buf (K) <= Max_Codepoint
and then Is_Scalar_Value (St.CP_Buf (K))
and then UTF8_Spec.Encoded_At
(Output, Trace (K), St.CP_Buf (K))));
pragma Assert
(if St.Do_Compose and then Old_Seg_Len >= 1 then
(for all K in 1 .. Old_Seg_Len =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K))
and then (if St.Use_Canon
then NFC_QC_Table (St.CP_Buf (K)) /= QC_No
else NFKC_QC_Table (St.CP_Buf (K)) /= QC_No)));
pragma Assert
(if St.Do_Compose and then Old_Seg_Len >= 2 then
(for all K in 1 .. Old_Seg_Len - 1 =>
Trace (K + 1) = Trace (K) +
UTF8_Spec.Encoded_Length (St.CP_Buf (K))));
pragma Assert
(if St.Do_Compose then Trace (1) = Pos_Start);
-- Phase 1b + Phase 2: Ghost verification and NFD reverse unfolding.
-- First: derive Well_Formed_At / Decoded_At from Encoded_At.
-- Then: reverse-unfold Ghost_Is_NFD_From one CP per iteration.
-- Combined into a single ghost procedure so the verification
-- loop's conclusions are visible to the reverse loop.
declare
procedure Ghost_NFD_Reverse with Ghost is
begin
if not (not St.Do_Compose
and then Pos > Pos_Start
and then Old_Seg_Len >= 1) then
return;
end if;
-- Phase 1b: derive Well_Formed_At/Decoded_At from Encoded_At.
-- The Phase 1 loop carries Encoded_At per trace position.
-- This loop unfolds the byte-level connection one K at a time
-- (non-quantified context: the solver matches Enc_* to WF*).
for K in 1 .. Old_Seg_Len loop
pragma Loop_Invariant
(for all J in 1 .. K - 1 =>
Ghost_Valid (Output, Trace (J))
and then Ghost_CP (Output, Trace (J)) = St.CP_Buf (J));
-- Per-K: Encoded_At is known from Phase 1 invariant.
-- Unfold to conclude Well_Formed_At and Decoded_At.
pragma Assert (Trace (K) in Output'Range);
pragma Assert (St.CP_Buf (K) <= Max_Codepoint);
pragma Assert (Is_Scalar_Value (St.CP_Buf (K)));
pragma Assert
(UTF8_Spec.Encoded_At (Output, Trace (K), St.CP_Buf (K)));
pragma Assert
(UTF8_Spec.Well_Formed_At (Output, Trace (K)));
-- Round-trip: Decoded_At(Output, P) = CP.
-- Must match on encoding length to help the solver
-- pick the right Decode_N case.
declare
P : constant Positive := Trace (K);
CV : constant Codepoint := St.CP_Buf (K);
EL : constant Positive :=
UTF8_Spec.Encoded_Length (CV);
begin
pragma Assert (EL = UTF8_Spec.Lead_Length (Output (P)));
pragma Assert
(UTF8_Spec.Decoded_At (Output, P) = CV);
-- Ghost_Step_Length = Lead_Length when Well_Formed_At.
pragma Assert
(Ghost_Step_Length (Output, P) = EL);
end;
end loop;
-- Now collect into Ghost_Valid/Ghost_CP form.
pragma Assert
(for all K in 1 .. Old_Seg_Len =>
Ghost_Valid (Output, Trace (K))
and then Ghost_CP (Output, Trace (K)) = St.CP_Buf (K));
-- Trace step in Ghost_Step_Length form.
-- Trace(K+1) = Trace(K) + Ghost_Step_Length(Output, Trace(K)).
pragma Assert
(for all K in 1 .. Old_Seg_Len - 1 =>
Trace (K + 1) = Trace (K) +
Ghost_Step_Length (Output, Trace (K)));
-- Phase 2: reverse unfolding for Ghost_Is_NFD_From.
for I in reverse 1 .. Old_Seg_Len loop
pragma Loop_Invariant (Old_Seg_Len = St.Seg_Len);
pragma Loop_Invariant (Pos > Pos_Start);
pragma Loop_Invariant (Pos <= Output'Last + 1);
-- Core invariant: NFD holds from Trace(I+1) onward
-- (with Last_CCC from entry I). Trivially true for
-- I = Old_Seg_Len (suffix is empty or single-CP).
pragma Loop_Invariant
(if I < Old_Seg_Len then
Ghost_Is_NFD_From
(Output, Trace (I + 1), Pos - 1,
Get_CCC (St.CP_Buf (I))));
-- All trace/buffer properties survive the reverse loop.
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
Trace (K) >= Pos_Start
and then Trace (K) < Pos
and then Trace (K) in Output'Range);
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
Ghost_Valid (Output, Trace (K))
and then Ghost_CP (Output, Trace (K))
= St.CP_Buf (K));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint
and then Ghost_Decomp_Len (St.CP_Buf (K), True) = 0
and then not Is_Hangul_Syllable (St.CP_Buf (K)));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K)));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len - 1 =>
(St.CCC_Buf (K) = 0
or St.CCC_Buf (K + 1) = 0
or St.CCC_Buf (K) <= St.CCC_Buf (K + 1)));
-- Trace step: consecutive entries separated by Ghost_Step_Length.
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len - 1 =>
Trace (K + 1) = Trace (K) +
Ghost_Step_Length (Output, Trace (K)));
-- One-step unfolding: Ghost_Is_NFD_From at Trace(I).
-- NFD definition checks at Trace(I):
pragma Assert (Ghost_Valid (Output, Trace (I)));
pragma Assert (Ghost_CP (Output, Trace (I)) = St.CP_Buf (I));
pragma Assert (Ghost_Decomp_Len (St.CP_Buf (I), True) = 0);
pragma Assert
(not Is_Hangul_Syllable (Ghost_CP (Output, Trace (I))));
-- CCC ordering: either I=1 (Last_CCC=0) or canonical sort.
if I > 1 then
pragma Assert
(St.CCC_Buf (I - 1) = 0
or St.CCC_Buf (I) = 0
or St.CCC_Buf (I - 1) <= St.CCC_Buf (I));
pragma Assert
(Get_CCC (St.CP_Buf (I)) = 0
or Get_CCC (St.CP_Buf (I - 1))
<= Get_CCC (St.CP_Buf (I)));
end if;
-- Recursive step connection: Trace(I) + Step = Trace(I+1) or Pos.
declare
Step : constant Positive :=
Ghost_Step_Length (Output, Trace (I));
Next_Pos : constant Positive := Trace (I) + Step;
begin
if I < Old_Seg_Len then
-- Not last: Trace(I+1) = Trace(I) + Step.
pragma Assert (Trace (I + 1) = Next_Pos);
-- Recursive target matches loop invariant.
pragma Assert
(Ghost_Is_NFD_From
(Output, Next_Pos, Pos - 1,
Get_CCC (St.CP_Buf (I))));
else
-- Last entry: Next_Pos = Pos, so
-- Ghost_Is_NFD_From(Output, Pos, Pos-1, ...) = True
-- because Pos > Pos - 1 (base case).
pragma Assert (Next_Pos <= Pos);
pragma Assert
(Ghost_Is_NFD_From
(Output, Next_Pos, Pos - 1,
Get_CCC (St.CP_Buf (I))));
end if;
-- Full unfolding: Ghost_Is_NFD_From at Trace(I).
pragma Assert
(Ghost_Is_NFD_From
(Output, Trace (I), Pos - 1,
(if I = 1 then 0
else Get_CCC (St.CP_Buf (I - 1)))));
end;
end loop;
-- After full reverse: NFD from Trace(1) = Pos_Start.
pragma Assert (Trace (1) = Pos_Start);
pragma Assert
(Ghost_Is_NFD_From (Output, Pos_Start, Pos - 1, 0));
-- First CP is a starter (only when prior output exists):
-- from encoding Trace(1) = Pos_Start,
-- Ghost_CP(Output, Pos_Start) = CP_Buf(1), and the
-- first-is-starter precondition gives CCC_Table(CP_Buf(1))=0.
if Pos_Start > Output'First then
pragma Assert (Ghost_Valid (Output, Pos_Start));
pragma Assert
(Ghost_CP (Output, Pos_Start) = St.CP_Buf (1));
pragma Assert
(Get_CCC (Ghost_CP (Output, Pos_Start)) = 0);
end if;
end Ghost_NFD_Reverse;
begin
if not St.Do_Compose then
Ghost_NFD_Reverse;
end if;
end;
-- NFC reverse unfolding: same two-phase pattern as NFD but for
-- Ghost_Is_NFC_From. Uses NFC_Valid/NFC_CP/NFC_Step_Length.
-- Checks NFC_QC(CP) /= QC_No instead of Ghost_Decomp_Len = 0.
--
-- The buffer entries at this point are POST-composition, so they
-- include Hangul syllable compositions and table compositions.
-- Compose_Buffer's postcondition guarantees NFC_QC validity.
declare
procedure Ghost_NFC_Reverse with Ghost is
begin
if not (St.Do_Compose
and then Pos > Pos_Start
and then Old_Seg_Len >= 1) then
return;
end if;
-- Phase 1b-NFC: derive NFC_Valid/NFC_CP from Encoded_At.
for K in 1 .. Old_Seg_Len loop
pragma Loop_Invariant
(for all J in 1 .. K - 1 =>
NFC_Valid (Output, Trace (J))
and then NFC_CP (Output, Trace (J)) = St.CP_Buf (J));
pragma Assert (Trace (K) in Output'Range);
pragma Assert (St.CP_Buf (K) <= Max_Codepoint);
pragma Assert (Is_Scalar_Value (St.CP_Buf (K)));
pragma Assert
(UTF8_Spec.Encoded_At (Output, Trace (K), St.CP_Buf (K)));
pragma Assert
(UTF8_Spec.Well_Formed_At (Output, Trace (K)));
declare
P : constant Positive := Trace (K);
CV : constant Codepoint := St.CP_Buf (K);
EL : constant Positive :=
UTF8_Spec.Encoded_Length (CV);
begin
pragma Assert (EL = UTF8_Spec.Lead_Length (Output (P)));
-- Round-trip: Decoded_At(Output, P) = CV.
-- Explicit case-split on the encoding length helps the
-- prover match the Encoded_At case (Enc_N bytes at P)
-- to the Decoded_At case (Decode_N at P). In the NFD
-- path the analogous assertion proves without the
-- case-split, but the NFC ghost context loses some
-- heuristic chain; the case-split restores the
-- byte-level connection.
pragma Assert (EL in 1 .. 4);
case EL is
when 1 =>
pragma Assert
(Output (P) = UTF8_Spec.Enc_1_B0 (CV));
pragma Assert
(UTF8_Spec.Decode_1 (Output (P)) = CV);
when 2 =>
pragma Assert
(Output (P) = UTF8_Spec.Enc_2_B0 (CV));
pragma Assert
(Output (P + 1) = UTF8_Spec.Enc_2_B1 (CV));
pragma Assert
(UTF8_Spec.Decode_2
(Output (P), Output (P + 1)) = CV);
when 3 =>
pragma Assert
(Output (P) = UTF8_Spec.Enc_3_B0 (CV));
pragma Assert
(Output (P + 1) = UTF8_Spec.Enc_3_B1 (CV));
pragma Assert
(Output (P + 2) = UTF8_Spec.Enc_3_B2 (CV));
pragma Assert
(UTF8_Spec.Decode_3
(Output (P), Output (P + 1),
Output (P + 2)) = CV);
when 4 =>
pragma Assert
(Output (P) = UTF8_Spec.Enc_4_B0 (CV));
pragma Assert
(Output (P + 1) = UTF8_Spec.Enc_4_B1 (CV));
pragma Assert
(Output (P + 2) = UTF8_Spec.Enc_4_B2 (CV));
pragma Assert
(Output (P + 3) = UTF8_Spec.Enc_4_B3 (CV));
pragma Assert
(UTF8_Spec.Decode_4
(Output (P), Output (P + 1),
Output (P + 2), Output (P + 3)) = CV);
when others =>
pragma Assert (False);
end case;
pragma Assert
(UTF8_Spec.Decoded_At (Output, P) = CV);
-- NFC_Valid and NFC_CP follow from byte-level encoding.
pragma Assert (NFC_Valid (Output, P));
pragma Assert (NFC_CP (Output, P) = CV);
pragma Assert
(NFC_Step_Length (Output, P) = EL);
end;
end loop;
pragma Assert
(for all K in 1 .. Old_Seg_Len =>
NFC_Valid (Output, Trace (K))
and then NFC_CP (Output, Trace (K)) = St.CP_Buf (K));
-- Trace step in NFC_Step_Length form.
pragma Assert
(for all K in 1 .. Old_Seg_Len - 1 =>
Trace (K + 1) = Trace (K) +
NFC_Step_Length (Output, Trace (K)));
-- Phase 2-NFC: reverse unfolding for Ghost_Is_NFC_From.
for I in reverse 1 .. Old_Seg_Len loop
pragma Loop_Invariant (Old_Seg_Len = St.Seg_Len);
pragma Loop_Invariant (Pos > Pos_Start);
pragma Loop_Invariant (Pos <= Output'Last + 1);
pragma Loop_Invariant
(if I < Old_Seg_Len then
Ghost_Is_NFC_From
(Output, Trace (I + 1), Pos - 1,
Get_CCC (St.CP_Buf (I)), St.Use_Canon));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
Trace (K) >= Pos_Start
and then Trace (K) < Pos
and then Trace (K) in Output'Range);
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
NFC_Valid (Output, Trace (K))
and then NFC_CP (Output, Trace (K)) = St.CP_Buf (K));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint
and then (if St.Use_Canon then
NFC_QC_Table (St.CP_Buf (K)) /= QC_No
else
NFKC_QC_Table (St.CP_Buf (K)) /= QC_No));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len =>
St.CCC_Buf (K) = CCC_Table (St.CP_Buf (K)));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len - 1 =>
(St.CCC_Buf (K) = 0
or St.CCC_Buf (K + 1) = 0
or St.CCC_Buf (K) <= St.CCC_Buf (K + 1)));
pragma Loop_Invariant
(for all K in 1 .. Old_Seg_Len - 1 =>
Trace (K + 1) = Trace (K) +
NFC_Step_Length (Output, Trace (K)));
-- One-step unfolding at Trace(I).
pragma Assert (NFC_Valid (Output, Trace (I)));
pragma Assert (NFC_CP (Output, Trace (I)) = St.CP_Buf (I));
-- QC check: NFC_QC ≠ QC_No (from Compose_Buffer post).
if St.Use_Canon then
pragma Assert
(Get_NFC_QC (NFC_CP (Output, Trace (I))) /= QC_No);
else
pragma Assert
(Get_NFKC_QC (NFC_CP (Output, Trace (I))) /= QC_No);
end if;
-- CCC ordering.
if I > 1 then
pragma Assert
(St.CCC_Buf (I - 1) = 0
or St.CCC_Buf (I) = 0
or St.CCC_Buf (I - 1) <= St.CCC_Buf (I));
pragma Assert
(Get_CCC (St.CP_Buf (I)) = 0
or Get_CCC (St.CP_Buf (I - 1))
<= Get_CCC (St.CP_Buf (I)));
end if;
-- Recursive step.
declare
Step : constant Positive :=
NFC_Step_Length (Output, Trace (I));
Next_Pos : constant Positive := Trace (I) + Step;
begin
if I < Old_Seg_Len then
pragma Assert (Trace (I + 1) = Next_Pos);
pragma Assert
(Ghost_Is_NFC_From
(Output, Next_Pos, Pos - 1,
Get_CCC (St.CP_Buf (I)), St.Use_Canon));
else
pragma Assert (Next_Pos <= Pos);
pragma Assert
(Ghost_Is_NFC_From
(Output, Next_Pos, Pos - 1,
Get_CCC (St.CP_Buf (I)), St.Use_Canon));
end if;
pragma Assert
(Ghost_Is_NFC_From
(Output, Trace (I), Pos - 1,
(if I = 1 then 0
else Get_CCC (St.CP_Buf (I - 1))),
St.Use_Canon));
end;
end loop;
-- After full reverse: NFC from Trace(1) = Pos_Start.
pragma Assert (Trace (1) = Pos_Start);
pragma Assert
(Ghost_Is_NFC_From (Output, Pos_Start, Pos - 1, 0,
St.Use_Canon));
-- First CP is a starter (only when prior output exists).
if Pos_Start > Output'First then
pragma Assert (NFC_Valid (Output, Pos_Start));
pragma Assert
(NFC_CP (Output, Pos_Start) = St.CP_Buf (1));
pragma Assert
(Get_CCC (NFC_CP (Output, Pos_Start)) = 0);
end if;
end Ghost_NFC_Reverse;
begin
if St.Do_Compose then
Ghost_NFC_Reverse;
end if;
end;
-- NFC accumulator: concatenate pre-existing NFC prefix with new segment.
declare
procedure Ghost_NFC_Accum with
Ghost,
Pre => Initialized
and then OK
and then St.Do_Compose
and then Output'Last < Positive'Last
and then Pos >= Pos_Start
and then Pos_Start >= Output'First
and then Pos <= Output'Last + 1
and then Output_Entry'First = Output'First
and then Output_Entry'Last = Output'Last
-- Prefix NFC in saved copy
and then (if Pos_Start > Output'First
then Ghost_Is_NFC_From
(Output_Entry, Output'First,
Pos_Start - 1, 0, St.Use_Canon))
-- Frame: prefix bytes unchanged
and then (for all J in Output'First .. Pos_Start - 1 =>
Output (J) = Output_Entry (J))
-- New segment NFC
and then (if Pos > Pos_Start
then Ghost_Is_NFC_From
(Output, Pos_Start, Pos - 1, 0,
St.Use_Canon))
-- Starter at segment start (needed for concat)
and then (if Pos > Pos_Start
and then Pos_Start > Output'First
then NFC_Valid (Output, Pos_Start)
and then Get_CCC
(NFC_CP (Output, Pos_Start)) = 0),
Post => (if Pos > Output'First
then Ghost_Is_NFC (Output, Output'First, Pos - 1,
St.Use_Canon));
procedure Ghost_NFC_Accum is
begin
if Pos = Pos_Start then
-- No new bytes encoded — prefix unchanged.
if Pos_Start > Output'First then
Lemma_NFC_Frame
(Output_Entry, Output, Output'First,
Pos_Start - 1, 0, St.Use_Canon);
end if;
elsif Pos_Start = Output'First then
-- First segment — no prefix, segment is the full output.
null;
else
-- Both prefix and segment present — frame + concat.
Lemma_NFC_Frame
(Output_Entry, Output, Output'First, Pos_Start - 1,
0, St.Use_Canon);
Lemma_NFC_Concat
(Output, Output'First, Pos_Start - 1, Pos - 1,
0, St.Use_Canon);
end if;
end Ghost_NFC_Accum;
begin
if St.Do_Compose then
Ghost_NFC_Accum;
end if;
end;
-- NFD accumulator: concatenate pre-existing NFD prefix with new segment.
-- Ghost_NFD_Reverse established Ghost_Is_NFD_From(Output, Pos_Start, Pos-1, 0).
-- The Pre gives Ghost_Is_NFD(Output_Entry, Output'First, Pos_Start-1) since
-- Output_Entry captures the Output array at entry (before encoding).
-- Lemma_NFD_Frame transfers the predicate from Output_Entry to Output.
-- Concat gives Ghost_Is_NFD(Output, Output'First, Pos-1).
declare
procedure Ghost_NFD_Accum with
Ghost,
Pre => Initialized
and then OK
and then not St.Do_Compose
and then Output'Last < Positive'Last
and then Pos >= Pos_Start
and then Pos_Start >= Output'First
and then Pos <= Output'Last + 1
and then Output_Entry'First = Output'First
and then Output_Entry'Last = Output'Last
-- Prefix NFD in saved copy
and then (if Pos_Start > Output'First
then Ghost_Is_NFD_From
(Output_Entry, Output'First,
Pos_Start - 1, 0))
-- Frame: prefix bytes unchanged
and then (for all J in Output'First .. Pos_Start - 1 =>
Output (J) = Output_Entry (J))
-- New segment NFD
and then (if Pos > Pos_Start
then Ghost_Is_NFD_From
(Output, Pos_Start, Pos - 1, 0))
-- Starter at segment start (needed for concat)
and then (if Pos > Pos_Start
and then Pos_Start > Output'First
then Ghost_Valid (Output, Pos_Start)
and then Get_CCC
(Ghost_CP (Output, Pos_Start)) = 0),
Post => (if Pos > Output'First
then Ghost_Is_NFD (Output, Output'First, Pos - 1));
procedure Ghost_NFD_Accum is
begin
if Pos = Pos_Start then
-- No new bytes encoded — prefix unchanged.
if Pos_Start > Output'First then
Lemma_NFD_Frame
(Output_Entry, Output, Output'First,
Pos_Start - 1, 0);
end if;
elsif Pos_Start = Output'First then
-- First segment — no prefix, segment is the full output.
null;
else
-- Both prefix and segment present — frame + concat.
Lemma_NFD_Frame
(Output_Entry, Output, Output'First, Pos_Start - 1, 0);
Lemma_NFD_Concat
(Output, Output'First, Pos_Start - 1, Pos - 1, 0);
end if;
end Ghost_NFD_Accum;
begin
if not St.Do_Compose then
Ghost_NFD_Accum;
end if;
end;
end; -- declare Output_Entry
-- After encoding all entries:
-- Pos - Pos_Start = Ghost_Buf_Enc_Len(Buf, Seg_Len) = Orig_Sum
St.Seg_Len := 0;
end Flush_Segment;
---------------------------------------------------------------------------
-- Normalize_Decomp / Normalize_Compose — Platinum ghost proofs
--
-- Both procedures inline the UTF-8 decode loop and decompose-into-buffer
-- step so that ghost invariants can track properties across output.
-- Separate procedures ensure Do_Compose is a literal (not a parameter),
-- which the prover needs for the recursive ghost predicates.
--
-- Ghost invariants:
-- Normalize_Decomp: Ghost_Is_NFD(Output, First, Out_Pos - 1)
-- Normalize_Compose: Ghost_Is_NFC(Output, First, Out_Pos - 1, Use_Canon)
---------------------------------------------------------------------------
procedure Normalize_Decomp
(Input : Byte_Array;
Use_Canon : Boolean;
Output : in out Byte_Array;
Last : out Natural;
Status : out Norm_Status)
with Pre => Initialized
and then Data_All_Terminal
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Norm_Acc,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Ghost_Is_NFD (Output, Output'First, Last)
else
Last = Output'First - 1),
Always_Terminates
is
Pos : Positive := Input'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
Out_Pos : Natural := Output'First;
OK : Boolean := True;
St : Norm_Process_State :=
(CP_Buf => [others => 0],
CCC_Buf => [others => 0],
Seg_Len => 0,
Do_Compose => False,
Use_Canon => Use_Canon);
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (OK);
pragma Loop_Invariant (not St.Do_Compose);
pragma Loop_Invariant (St.Use_Canon = Use_Canon);
-- NFD readiness: all buffer entries are terminal.
pragma Loop_Invariant
(for all I in 1 .. St.Seg_Len =>
St.CP_Buf (I) <= Max_Codepoint
and then Ghost_Decomp_Len (St.CP_Buf (I), True) = 0
and then not Is_Hangul_Syllable (St.CP_Buf (I)));
-- Data invariant available.
pragma Loop_Invariant (Data_All_Terminal);
-- Buffer is non-empty once output has been produced.
-- Each iteration: flush sets Seg_Len=0, then decomposition adds
-- at least 1 entry. So at the top of each subsequent iteration,
-- Seg_Len >= 1. When Out_Pos = Output'First (no output yet),
-- Seg_Len can be 0 (first iteration).
pragma Loop_Invariant
(if Out_Pos > Output'First then St.Seg_Len >= 1);
-- First buffer entry is a starter (when there's prior output).
pragma Loop_Invariant
(if Out_Pos > Output'First
then CCC_Table (St.CP_Buf (1)) = 0);
-- NFD invariant: all flushed output so far is in NFD form.
pragma Loop_Invariant
(if Out_Pos > Output'First then
Ghost_Is_NFD (Output, Output'First, Out_Pos - 1));
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
-- Boundary detection + flush (inlined from Norm_On_Codepoint)
-- Ghost: capture the CCC of the first decomposition entry
-- from the boundary check so the fact survives into the
-- decomposition section below.
declare
First_Decomp_CCC : CCC_Value := 0 with Ghost;
Seg_Before : constant Natural := St.Seg_Len with Ghost;
begin
if St.Seg_Len > 0
and then Is_NF_Boundary (CP, St.Do_Compose)
then
pragma Assert (CCC_Table (CP) = 0);
declare
D : Decomp_Entry;
First_CP : Codepoint;
Is_Boundary : Boolean := True;
begin
if St.Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Offset <= Max_Decomp_Data
then
if St.Use_Canon then
First_CP := Canon_Data (D.Offset);
else
First_CP := Compat_Data (D.Offset);
end if;
First_Decomp_CCC := CCC_Table (First_CP);
if CCC_Table (First_CP) /= 0 then
Is_Boundary := False;
end if;
end if;
if Is_Boundary then
-- Ghost: Is_Boundary true means the first decomp CP
-- (if any) has CCC=0, or the CP has no decomposition
-- (self-maps, CCC=0 from Is_NF_Boundary).
pragma Assert (First_Decomp_CCC = 0);
-- Flush_Segment handles the NFD concat internally:
-- its Pre takes Ghost_Is_NFD on the prefix, and its
-- Post gives Ghost_Is_NFD on the full output.
Flush_Segment (St, Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
end if;
end;
end if;
-- After boundary: if a flush happened (Seg_Before > 0,
-- St.Seg_Len = 0), the boundary check verified that the
-- first decomposition entry has CCC=0. Also CCC_Table(CP)=0
-- from Is_NF_Boundary.
pragma Assert
(if St.Seg_Len = 0 and then Seg_Before > 0
then First_Decomp_CCC = 0 and then CCC_Table (CP) = 0);
-- Decompose this CP into the work buffer (inlined from Norm_On_Codepoint)
if Is_Hangul_Syllable (CP) then
declare
SIndex : constant Natural := CP - SBase;
L : constant Codepoint := LBase + SIndex / NCount;
V : constant Codepoint :=
VBase + (SIndex mod NCount) / TCount;
T : constant Codepoint := TBase + SIndex mod TCount;
begin
if St.Seg_Len + 2 > Max_Work_CPs
or (T /= TBase
and then St.Seg_Len + 3 > Max_Work_CPs)
then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := L;
-- L jamo: not a syllable, no canonical decomp, CCC=0.
pragma Assert (not Is_Hangul_Syllable (L));
pragma Assert (Canon_Index (L).Length = 0);
pragma Assert (Ghost_Decomp_Len (L, True) = 0);
pragma Assert (CCC_Table (L) = 0);
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := V;
-- V jamo: not a syllable, no canonical decomp.
pragma Assert (not Is_Hangul_Syllable (V));
pragma Assert (Canon_Index (V).Length = 0);
pragma Assert (Ghost_Decomp_Len (V, True) = 0);
if T /= TBase then
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := T;
-- T jamo: not a syllable, no canonical decomp.
pragma Assert (not Is_Hangul_Syllable (T));
pragma Assert (Canon_Index (T).Length = 0);
pragma Assert (Ghost_Decomp_Len (T, True) = 0);
end if;
end;
else
declare
D : Decomp_Entry;
begin
if St.Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Length <= Max_Decomp_Data
and then D.Offset <= Max_Decomp_Data - D.Length + 1
then
if St.Seg_Len + D.Length > Max_Work_CPs then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- First-CP-starter: when Seg_Len=0, the first entry
-- will have CCC=0. First_Decomp_CCC captured the CCC
-- of Canon/Compat_Data(Canon/Compat_Index(CP).Offset)
-- from the boundary check. D here = Canon/Compat_Index(CP)
-- (same CP, same table), so D.Offset is the same, and
-- First_Decomp_CCC = CCC_Table(Canon/Compat_Data(D.Offset)).
if Out_Pos > Output'First and then St.Seg_Len = 0 then
-- Seg_Len = 0 with prior output means a flush happened,
-- so Seg_Before > 0 and First_Decomp_CCC = 0.
pragma Assert (Seg_Before > 0);
pragma Assert (First_Decomp_CCC = 0);
if St.Use_Canon then
-- D = Canon_Index(CP), same as boundary's D.
-- First_Decomp_CCC = CCC_Table(Canon_Data(D.Offset)).
pragma Assert (First_Decomp_CCC =
CCC_Table (Canon_Data (D.Offset)));
pragma Assert (CCC_Table (Canon_Data (D.Offset)) = 0);
else
pragma Assert (First_Decomp_CCC =
CCC_Table (Compat_Data (D.Offset)));
pragma Assert (CCC_Table (Compat_Data (D.Offset)) = 0);
end if;
end if;
declare
Seg_Pre_Loop : constant Natural :=
St.Seg_Len with Ghost;
begin
for I in D.Offset .. D.Offset + D.Length - 1 loop
pragma Loop_Invariant
(St.Seg_Len + (D.Offset + D.Length - 1 - I)
< Max_Work_CPs);
-- Track Seg_Len = Seg_Pre_Loop + (I - D.Offset).
pragma Loop_Invariant
(St.Seg_Len = Seg_Pre_Loop + (I - D.Offset));
-- NFD readiness: all previously added entries are
-- terminal (from Data_All_Terminal + expression
-- function unfolding).
pragma Loop_Invariant
(for all K in 1 .. St.Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint
and then Ghost_Decomp_Len (St.CP_Buf (K), True) = 0
and then not Is_Hangul_Syllable (St.CP_Buf (K)));
-- First-CP-starter invariant survives inner loop.
pragma Loop_Invariant
(if Out_Pos > Output'First and then St.Seg_Len >= 1
then CCC_Table (St.CP_Buf (1)) = 0);
St.Seg_Len := St.Seg_Len + 1;
if St.Use_Canon then
St.CP_Buf (St.Seg_Len) := Canon_Data (I);
-- Canon_Data entry is terminal (Data_All_Terminal).
pragma Assert (Canon_Data (I) <= Max_Codepoint);
pragma Assert
(Canon_Index (Canon_Data (I)).Length = 0);
pragma Assert (not Is_Hangul_Syllable (Canon_Data (I)));
pragma Assert
(Ghost_Decomp_Len (Canon_Data (I), True) = 0);
-- First entry is a starter: when Seg_Len just became 1.
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (I = D.Offset);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
else
St.CP_Buf (St.Seg_Len) := Compat_Data (I);
-- Compat_Data entry is terminal (Data_All_Terminal).
pragma Assert (Compat_Data (I) <= Max_Codepoint);
pragma Assert
(Canon_Index (Compat_Data (I)).Length = 0);
pragma Assert
(not Is_Hangul_Syllable (Compat_Data (I)));
pragma Assert
(Ghost_Decomp_Len (Compat_Data (I), True) = 0);
-- First entry is a starter: when Seg_Len just became 1.
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (I = D.Offset);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
end if;
end loop;
end;
else
-- Self-mapping CP: no decomposition, not a Hangul syllable
-- (Hangul path handled above).
if St.Seg_Len = Max_Work_CPs then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- CP is not a Hangul syllable (handled by outer if).
pragma Assert (not Is_Hangul_Syllable (CP));
-- In the else branch: D does not encode a valid decomp.
-- For Use_Canon=True: D = Canon_Index(CP), and failing the
-- if means Canon_Index(CP).Length = 0 (or offset invalid).
-- For Use_Canon=False: D = Compat_Index(CP). We need to
-- show Canon_Index(CP).Length = 0. Two sub-cases:
-- (a) D.Length = 0 → Compat_Index(CP).Length = 0 →
-- Data_All_Terminal gives Canon_Index(CP).Length = 0.
-- (b) D conditions fail but D.Length > 0 → impossible in
-- correct UCD data (covered by Initialize).
if St.Use_Canon then
pragma Assert (Canon_Index (CP).Length = 0
or else Canon_Index (CP).Offset < 1
or else Canon_Index (CP).Length
> Max_Decomp_Data
or else Canon_Index (CP).Offset
> Max_Decomp_Data
- Canon_Index (CP).Length + 1);
else
-- D = Compat_Index(CP), falling through means no valid
-- compat decomposition.
-- Data_All_Terminal: Length > 0 → Offset >= 1.
-- Data_All_Terminal: Length > 0 ∧ Offset >= 1 →
-- valid range (within Compat_Used ≤ Max_Decomp_Data).
-- So if Length > 0, all four decomp conditions are met,
-- contradicting the else branch. Therefore Length = 0.
if Compat_Index (CP).Length > 0 then
-- Length > 0 → Offset >= 1 (Data_All_Terminal).
pragma Assert (Compat_Index (CP).Offset >= 1);
-- Data_All_Terminal: valid range within Compat_Used.
pragma Assert
(Compat_Index (CP).Offset <= Compat_Used);
pragma Assert
(Compat_Index (CP).Length <=
Compat_Used - Compat_Index (CP).Offset + 1);
-- Compat_Used ≤ Max_Decomp_Data.
pragma Assert
(Compat_Index (CP).Length <= Max_Decomp_Data);
pragma Assert
(Compat_Index (CP).Offset <=
Max_Decomp_Data - Compat_Index (CP).Length + 1);
-- All decomp conditions met → contradiction.
pragma Assert (False);
end if;
pragma Assert (Compat_Index (CP).Length = 0);
-- Canon_Index(CP).Length = 0 by Data_All_Terminal.
pragma Assert (Canon_Index (CP).Length = 0);
end if;
pragma Assert (Ghost_Decomp_Len (CP, True) = 0);
-- Self-mapping CP as first entry: Is_NF_Boundary(CP)
-- includes CCC_Table(CP) = 0. When Seg_Len = 0 and
-- Out_Pos > Output'First, a flush just happened, so
-- the boundary check entered and Is_NF_Boundary held.
-- For Seg_Len = 0 and Out_Pos = Output'First (first
-- iteration), the invariant condition is vacuously true.
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := CP;
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (CCC_Table (CP) = 0);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
end if;
end;
end if;
end; -- declare First_Entry_Starter / Seg_Before
-- Advance past decoded UTF-8 sequence
if Pos > Input'Last - Len + 1 then
Pos := Input'Last + 1;
else
Pos := Pos + Len;
end if;
end loop;
-- Flush remaining segment
if St.Seg_Len > 0 then
-- Flush_Segment handles NFD concat internally.
pragma Warnings
(GNATprove, Off,
"""St"" is set by ""Flush_Segment"" but not used after the call",
Reason => "Final flush; the emptied segment state is not needed");
Flush_Segment (St, Output, Out_Pos, OK);
pragma Warnings
(GNATprove, On,
"""St"" is set by ""Flush_Segment"" but not used after the call");
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
end if;
if Out_Pos = Output'First then
-- No output produced
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Normalize_Decomp;
---------------------------------------------------------------------------
-- Normalize_Compose — inline NFC/NFKC with Platinum ghost proof
--
-- Same structure as Normalize_Decomp but with Do_Compose => True.
-- Ghost invariant tracks Ghost_Is_NFC across the output.
---------------------------------------------------------------------------
procedure Normalize_Compose
(Input : Byte_Array;
Use_Canon : Boolean;
Output : in out Byte_Array;
Last : out Natural;
Status : out Norm_Status)
with Pre => Initialized
and then Data_All_Terminal
and then Input'Length >= 1
and then Output'Length >= 1
and then Input'Last < Positive'Last
and then Output'Last < Positive'Last
and then Output'Length <= Max_Norm_Acc,
Post => (if Status = Success then
Last in Output'First .. Output'Last
and then Ghost_Is_NFC (Output, Output'First, Last,
Use_Canon)
else
Last = Output'First - 1),
Always_Terminates
is
Pos : Positive := Input'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
Out_Pos : Natural := Output'First;
OK : Boolean := True;
St : Norm_Process_State :=
(CP_Buf => [others => 0],
CCC_Buf => [others => 0],
Seg_Len => 0,
Do_Compose => True,
Use_Canon => Use_Canon);
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant (OK);
pragma Loop_Invariant (St.Do_Compose);
pragma Loop_Invariant (St.Use_Canon = Use_Canon);
-- NFC readiness: all buffer entries have QC ≠ QC_No.
pragma Loop_Invariant
(for all I in 1 .. St.Seg_Len =>
St.CP_Buf (I) <= Max_Codepoint
and then (if Use_Canon
then NFC_QC_Table (St.CP_Buf (I)) /= QC_No
else NFKC_QC_Table (St.CP_Buf (I)) /= QC_No));
-- Data invariant available.
pragma Loop_Invariant (Data_All_Terminal);
-- Buffer is non-empty once output has been produced.
-- Each iteration: flush sets Seg_Len=0, then decomposition adds
-- at least 1 entry. So at the top of each subsequent iteration,
-- Seg_Len >= 1. When Out_Pos = Output'First (no output yet),
-- Seg_Len can be 0 (first iteration).
pragma Loop_Invariant
(if Out_Pos > Output'First then St.Seg_Len >= 1);
-- First buffer entry is a starter (when there's prior output).
-- Required by Flush_Segment's NFC first-starter Pre.
pragma Loop_Invariant
(if Out_Pos > Output'First
then CCC_Table (St.CP_Buf (1)) = 0);
-- NFC invariant: all flushed output so far passes NFC Quick Check.
pragma Loop_Invariant
(if Out_Pos > Output'First then
Ghost_Is_NFC (Output, Output'First, Out_Pos - 1,
Use_Canon));
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
Status := Invalid_Input;
Last := Output'First - 1;
return;
end if;
-- Boundary detection + flush (same as Normalize_Decomp).
-- Ghost: capture the CCC of the first decomposition entry from
-- the boundary check so the fact survives into the decomposition
-- section below (used to re-establish the first-starter invariant
-- after Flush_Segment resets Seg_Len to 0).
declare
First_Decomp_CCC : CCC_Value := 0 with Ghost;
Seg_Before : constant Natural := St.Seg_Len with Ghost;
begin
if St.Seg_Len > 0
and then Is_NF_Boundary (CP, St.Do_Compose)
then
pragma Assert (CCC_Table (CP) = 0);
declare
D : Decomp_Entry;
First_CP : Codepoint;
Is_Boundary : Boolean := True;
begin
if St.Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Offset <= Max_Decomp_Data
then
if St.Use_Canon then
First_CP := Canon_Data (D.Offset);
else
First_CP := Compat_Data (D.Offset);
end if;
First_Decomp_CCC := CCC_Table (First_CP);
if CCC_Table (First_CP) /= 0 then
Is_Boundary := False;
end if;
end if;
if Is_Boundary then
Flush_Segment (St, Output, Out_Pos, OK);
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
end if;
end;
end if;
-- After boundary: if a flush happened (Seg_Before > 0,
-- St.Seg_Len = 0), the boundary check verified that the first
-- decomposition entry has CCC=0. Also CCC_Table(CP)=0 from
-- Is_NF_Boundary.
pragma Assert
(if St.Seg_Len = 0 and then Seg_Before > 0
then First_Decomp_CCC = 0 and then CCC_Table (CP) = 0);
-- Decompose this CP into the work buffer
if Is_Hangul_Syllable (CP) then
declare
SIndex : constant Natural := CP - SBase;
L : constant Codepoint := LBase + SIndex / NCount;
V : constant Codepoint :=
VBase + (SIndex mod NCount) / TCount;
T : constant Codepoint := TBase + SIndex mod TCount;
begin
if St.Seg_Len + 2 > Max_Work_CPs
or (T /= TBase
and then St.Seg_Len + 3 > Max_Work_CPs)
then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := L;
-- L jamo: no canon/compat decomp, not Hangul syllable
-- → NFC_QC ≠ QC_No and NFKC_QC ≠ QC_No
-- (from Data_All_Terminal self-mapping invariants).
pragma Assert (not Is_Hangul_Syllable (L));
pragma Assert (Canon_Index (L).Length = 0);
pragma Assert (Compat_Index (L).Length = 0);
pragma Assert (NFC_QC_Table (L) /= QC_No);
pragma Assert (NFKC_QC_Table (L) /= QC_No);
-- L jamo is a starter (CCC=0 by Data_All_Terminal,
-- Hangul L-jamo invariant). When this addition just
-- brought Seg_Len to 1 with prior output, CP_Buf(1) = L
-- is a starter — restoring the loop's first-starter
-- invariant after a flush.
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (CCC_Table (L) = 0);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := V;
-- V jamo: no canon/compat decomp, not Hangul syllable.
pragma Assert (not Is_Hangul_Syllable (V));
pragma Assert (Canon_Index (V).Length = 0);
pragma Assert (Compat_Index (V).Length = 0);
pragma Assert (NFC_QC_Table (V) /= QC_No);
pragma Assert (NFKC_QC_Table (V) /= QC_No);
if T /= TBase then
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := T;
-- T jamo: no canon/compat decomp, not Hangul syllable.
pragma Assert (not Is_Hangul_Syllable (T));
pragma Assert (Canon_Index (T).Length = 0);
pragma Assert (Compat_Index (T).Length = 0);
pragma Assert (NFC_QC_Table (T) /= QC_No);
pragma Assert (NFKC_QC_Table (T) /= QC_No);
end if;
end;
else
declare
D : Decomp_Entry;
begin
if St.Use_Canon then
D := Canon_Index (CP);
else
D := Compat_Index (CP);
end if;
if D.Length > 0
and then D.Offset >= 1
and then D.Length <= Max_Decomp_Data
and then D.Offset <= Max_Decomp_Data - D.Length + 1
then
if St.Seg_Len + D.Length > Max_Work_CPs then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- First-CP-starter: when Seg_Len=0, the first entry
-- added below will have CCC=0. First_Decomp_CCC
-- captured CCC_Table(Canon/Compat_Data(D.Offset))
-- during the boundary check. D here = same Canon/
-- Compat_Index(CP), so D.Offset matches and
-- First_Decomp_CCC = CCC_Table of the first decomp CP.
if Out_Pos > Output'First and then St.Seg_Len = 0 then
pragma Assert (Seg_Before > 0);
pragma Assert (First_Decomp_CCC = 0);
if St.Use_Canon then
pragma Assert (First_Decomp_CCC =
CCC_Table (Canon_Data (D.Offset)));
pragma Assert (CCC_Table (Canon_Data (D.Offset)) = 0);
else
pragma Assert (First_Decomp_CCC =
CCC_Table (Compat_Data (D.Offset)));
pragma Assert (CCC_Table (Compat_Data (D.Offset)) = 0);
end if;
end if;
declare
Seg_Pre_Loop : constant Natural :=
St.Seg_Len with Ghost;
begin
for I in D.Offset .. D.Offset + D.Length - 1 loop
pragma Loop_Invariant
(St.Seg_Len + (D.Offset + D.Length - 1 - I)
< Max_Work_CPs);
-- Track Seg_Len = Seg_Pre_Loop + (I - D.Offset).
pragma Loop_Invariant
(St.Seg_Len = Seg_Pre_Loop + (I - D.Offset));
-- NFC readiness: all previously added entries have
-- QC ≠ QC_No (from Data_All_Terminal).
pragma Loop_Invariant
(for all K in 1 .. St.Seg_Len =>
St.CP_Buf (K) <= Max_Codepoint
and then (if Use_Canon
then NFC_QC_Table (St.CP_Buf (K)) /= QC_No
else NFKC_QC_Table (St.CP_Buf (K)) /= QC_No));
-- First-CP-starter invariant survives inner loop.
pragma Loop_Invariant
(if Out_Pos > Output'First and then St.Seg_Len >= 1
then CCC_Table (St.CP_Buf (1)) = 0);
St.Seg_Len := St.Seg_Len + 1;
if St.Use_Canon then
St.CP_Buf (St.Seg_Len) := Canon_Data (I);
-- Canon_Data entry has NFC_QC ≠ QC_No
-- (Data_All_Terminal, line 184).
pragma Assert (Canon_Data (I) <= Max_Codepoint);
pragma Assert (NFC_QC_Table (Canon_Data (I)) /= QC_No);
-- First entry is a starter when Seg_Len just
-- became 1 (first iteration of inner loop with
-- Seg_Pre_Loop = 0).
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (I = D.Offset);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
else
St.CP_Buf (St.Seg_Len) := Compat_Data (I);
-- Compat_Data entry has NFKC_QC ≠ QC_No
-- (Data_All_Terminal, line 187).
pragma Assert (Compat_Data (I) <= Max_Codepoint);
pragma Assert (NFKC_QC_Table (Compat_Data (I)) /= QC_No);
-- First entry is a starter when Seg_Len just
-- became 1.
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (I = D.Offset);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
end if;
end loop;
end;
else
if St.Seg_Len = Max_Work_CPs then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
-- Self-mapping CP: not a Hangul syllable
-- (Hangul path handled by outer if).
pragma Assert (not Is_Hangul_Syllable (CP));
-- Self-mapping: Canon_Index(CP).Length = 0 or
-- Compat_Index(CP).Length = 0 (else branch condition).
-- Data_All_Terminal → NFC/NFKC QC ≠ QC_No.
if St.Use_Canon then
pragma Assert (Canon_Index (CP).Length = 0
or else Canon_Index (CP).Offset < 1
or else Canon_Index (CP).Length
> Max_Decomp_Data
or else Canon_Index (CP).Offset
> Max_Decomp_Data
- Canon_Index (CP).Length + 1);
else
-- Compat path: if Compat_Index(CP).Length > 0 then
-- all decomp conditions are met (Data_All_Terminal),
-- contradicting the else branch. So Length = 0.
if Compat_Index (CP).Length > 0 then
pragma Assert (Compat_Index (CP).Offset >= 1);
pragma Assert
(Compat_Index (CP).Offset <= Compat_Used);
pragma Assert
(Compat_Index (CP).Length <=
Compat_Used - Compat_Index (CP).Offset + 1);
pragma Assert
(Compat_Index (CP).Length <= Max_Decomp_Data);
pragma Assert
(Compat_Index (CP).Offset <=
Max_Decomp_Data - Compat_Index (CP).Length + 1);
pragma Assert (False);
end if;
pragma Assert (Compat_Index (CP).Length = 0);
pragma Assert (Canon_Index (CP).Length = 0);
end if;
-- Now NFC/NFKC QC follows from Data_All_Terminal
-- self-mapping invariants.
-- Canon path: Canon_Index(CP).Length=0 → NFC_QC ≠ QC_No.
-- Compat path: Compat_Index(CP).Length=0 → NFKC_QC ≠ QC_No.
if St.Use_Canon then
pragma Assert (NFC_QC_Table (CP) /= QC_No);
else
pragma Assert (NFKC_QC_Table (CP) /= QC_No);
end if;
-- Self-mapping CP as first entry: Is_NF_Boundary(CP)
-- includes CCC_Table(CP) = 0. When Seg_Len = 0 and
-- Out_Pos > Output'First, a flush just happened, so
-- Seg_Before > 0 → CCC_Table(CP) = 0 from the
-- post-boundary assertion above.
St.Seg_Len := St.Seg_Len + 1;
St.CP_Buf (St.Seg_Len) := CP;
if St.Seg_Len = 1 and then Out_Pos > Output'First then
pragma Assert (CCC_Table (CP) = 0);
pragma Assert (CCC_Table (St.CP_Buf (1)) = 0);
end if;
end if;
end;
end if;
end; -- declare First_Decomp_CCC / Seg_Before
-- Advance past decoded UTF-8 sequence
if Pos > Input'Last - Len + 1 then
Pos := Input'Last + 1;
else
Pos := Pos + Len;
end if;
end loop;
-- Flush remaining segment
if St.Seg_Len > 0 then
pragma Warnings
(GNATprove, Off,
"""St"" is set by ""Flush_Segment"" but not used after the call",
Reason => "Final flush; the emptied segment state is not needed");
Flush_Segment (St, Output, Out_Pos, OK);
pragma Warnings
(GNATprove, On,
"""St"" is set by ""Flush_Segment"" but not used after the call");
if not OK then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
end if;
if Out_Pos = Output'First then
-- No output produced
Status := Buffer_Overflow;
Last := Output'First - 1;
else
Last := Out_Pos - 1;
Status := Success;
end if;
end Normalize_Compose;
procedure Normalize
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form;
Output : in out Byte_Array;
Last : out Natural;
Status : out Norm_Status)
is
begin
if not Is_Compose (Form) then
-- NFD / NFKD: Platinum postcondition via Ghost_Is_NFD
Normalize_Decomp (Input, Is_Canonical (Form), Output, Last, Status);
else
-- NFC / NFKC: Platinum postcondition via Ghost_Is_NFC
Normalize_Compose (Input, Is_Canonical (Form), Output, Last, Status);
end if;
end Normalize;
---------------------------------------------------------------------------
-- Quick_Check
---------------------------------------------------------------------------
function Quick_Check
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form)
return Normalization_Spec.QC_Value
is
Pos : Positive := Input'First;
CP : Codepoint;
Len : Positive;
Valid : Boolean;
Last_CCC : CCC_Value := 0;
Result : QC_Value := QC_Yes;
CCC_Val : CCC_Value;
begin
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Len, Valid);
if not Valid then
return QC_No;
end if;
CCC_Val := CCC_Table (CP);
-- Check canonical ordering
if CCC_Val /= 0 and then CCC_Val < Last_CCC then
return QC_No;
end if;
Last_CCC := CCC_Val;
-- Check form-specific QC
case Form is
when NFD =>
if not NFD_QC_Table (CP) then
return QC_No;
end if;
when NFC =>
declare
QC : constant QC_Value := NFC_QC_Table (CP);
begin
if QC = QC_No then
return QC_No;
elsif QC = QC_Maybe then
Result := QC_Maybe;
end if;
end;
when NFKD =>
if not NFKD_QC_Table (CP) then
return QC_No;
end if;
when NFKC =>
declare
QC : constant QC_Value := NFKC_QC_Table (CP);
begin
if QC = QC_No then
return QC_No;
elsif QC = QC_Maybe then
Result := QC_Maybe;
end if;
end;
end case;
-- Advance (Len >= 1, so Pos strictly increases)
if Pos > Input'Last - Len + 1 then
exit;
else
Pos := Pos + Len;
end if;
end loop;
return Result;
end Quick_Check;
---------------------------------------------------------------------------
-- Is_Normalized
--
-- SPARK_Mode Off because it allocates a variable-length local array
-- (not supported in SPARK) for the QC_Maybe comparison buffer.
-- The actual normalization logic (Normalize, Quick_Check) is fully
-- proved. Is_Normalized is a thin convenience wrapper verified by
-- the conformance test suite.
---------------------------------------------------------------------------
function Is_Normalized
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form)
return Boolean
with SPARK_Mode => Off
is
QC : constant QC_Value := Quick_Check (Input, Form);
begin
if QC = QC_Yes then
return True;
elsif QC = QC_No then
return False;
end if;
-- QC_Maybe: run full normalization and compare.
-- For NFC/NFKC QC_Maybe, composition can only shrink or preserve
-- the byte length, so Input'Length is a safe output size.
-- Variable-length local array — sized to Input'Length.
declare
Tmp : Byte_Array (1 .. Input'Length) := [others => 0];
Last : Natural;
Status : Norm_Status;
begin
Normalize (Input, Form, Tmp, Last, Status);
if Status /= Success then
return False;
end if;
-- Compare byte-by-byte
if Last /= Input'Length then
return False;
end if;
for I in 1 .. Last loop
if Tmp (I) /= Input (Input'First + I - 1) then
return False;
end if;
end loop;
return True;
end;
end Is_Normalized;
---------------------------------------------------------------------------
-- Get_CCC
---------------------------------------------------------------------------
function Get_CCC (CP : Codepoint) return Normalization_Spec.CCC_Value
is (CCC_Table (CP));
function Get_NFC_QC (CP : Codepoint) return Normalization_Spec.QC_Value
is (NFC_QC_Table (CP));
function Get_NFKC_QC (CP : Codepoint) return Normalization_Spec.QC_Value
is (NFKC_QC_Table (CP));
---------------------------------------------------------------------------
-- Lemma body: NFC_* helpers match UTF8_Spec.
--
-- Null body — the NFC_Lead_Length / NFC_Is_Cont / NFC_Valid /
-- NFC_Step_Length / NFC_CP expression functions in the spec are
-- structurally identical to UTF8_Spec.Lead_Length / Is_Continuation /
-- Well_Formed_At / (lead-length-or-1) / Decoded_At, so GNATprove
-- discharges the postcondition by direct unfolding.
---------------------------------------------------------------------------
procedure Lemma_NFC_Matches_UTF8_Spec
(Input : Byte_Array;
Cur : Positive)
is null;
end Lingenic_Text.Normalization;