-- Copyright © 2026 Lingenic LLC. All rights reserved.
-- Licensed under the Lingenic Source-Available License v2.3.
-- Production use requires a separate license from Licensor.
-- See LICENSE.md and COPYRIGHT in the project root.
--
-------------------------------------------------------------------------------
-- Lingenic-Text
-- Formally Verified Unicode Text Processing Library
--
-- IDNA implementation body (UTS #46).
--
-- Self-contained module for Internationalized Domain Names. Initialize
-- reads IdnaMappingTable.txt and builds status and mapping tables.
--
-- Initialize is SPARK_Mode Off: file I/O, string operations.
-- Processing procedures (To_ASCII, To_Unicode) are SPARK_Mode On where
-- possible, with careful bounds checking and explicit loop variants.
--
-- Punycode encode/decode per RFC 3492.
-- Validity criteria 1-9 per UTS #46 Section 4.1.
-- ContextJ rules per RFC 5892 Appendix A.
-- Bidi rules per RFC 5893 Section 2.
-------------------------------------------------------------------------------
with Lingenic_Text.File_IO;
with Lingenic_Text.UTF8;
with Lingenic_Text.Bidi_Spec;
with Lingenic_Text.Normalization_Spec;
with Lingenic_Text.Properties_Spec;
package body Lingenic_Text.IDNA
with SPARK_Mode,
Refined_State => (IDNA_State =>
(Is_Init,
Status_Table,
Map_Index,
Map_Data,
Map_Data_Len,
Init_Buffer,
Init_Length))
is
use Properties_Spec;
use Normalization_Spec;
---------------------------------------------------------------------------
-- Constants
---------------------------------------------------------------------------
Max_Map_Data : constant := 65536;
Max_Work_CPs : constant := 2048;
Max_Work_Bytes : constant := 8192;
Hyphen_CP : constant Codepoint := 16#2D#;
Dot_CP : constant Codepoint := 16#2E#;
Dot_Byte : constant Byte := 16#2E#;
-- Punycode ASCII encoding characters
Puny_A_Lower : constant Byte := 16#61#;
Puny_Z_Lower : constant Byte := 16#7A#;
Puny_A_Upper : constant Byte := 16#41#;
Puny_Z_Upper : constant Byte := 16#5A#;
Puny_Zero : constant Byte := 16#30#;
Puny_Nine : constant Byte := 16#39#;
---------------------------------------------------------------------------
-- Data types
---------------------------------------------------------------------------
type Status_Table_Type is array (0 .. Max_Codepoint) of Status_Value;
type Map_Index_Type is array (0 .. Max_Codepoint) of Natural;
type Map_Data_Type is array (0 .. Max_Map_Data - 1) of Natural;
type CP_Work_Array is array (1 .. Max_Work_CPs) of Codepoint;
subtype CP_Work_Length is Natural range 0 .. Max_Work_CPs;
type Label_Boundary is record
Start_Idx : Positive;
End_Idx : Natural;
end record;
type Label_Array is array (1 .. Max_Labels) of Label_Boundary;
subtype Label_Count is Natural range 0 .. Max_Labels;
---------------------------------------------------------------------------
-- State variables
---------------------------------------------------------------------------
Is_Init : Boolean := False;
Status_Table : Status_Table_Type := [others => ST_Disallowed];
Map_Index : Map_Index_Type := [others => 0];
Map_Data : Map_Data_Type := [others => 0];
Map_Data_Len : Natural := 1; -- 0 = "no mapping" sentinel
Init_Buffer : File_IO.File_Byte_Array := [others => 0];
Init_Length : File_IO.File_Size := 0;
---------------------------------------------------------------------------
-- Initialized
---------------------------------------------------------------------------
function Initialized return Boolean is (Is_Init);
---------------------------------------------------------------------------
-- Initialize (SPARK_Mode Off)
---------------------------------------------------------------------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with SPARK_Mode => Off
is
OK : Boolean;
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;
end case;
end loop;
return Val;
end Parse_Hex;
function Skip_Spaces (S : String; From : Positive) return Positive is
P : Positive := From;
begin
while P <= S'Last
and then (S (P) = ' ' or S (P) = ASCII.HT)
loop
P := P + 1;
end loop;
return P;
end Skip_Spaces;
function Trim_Right (S : String) return String is
Last : Natural := S'Last;
begin
while Last >= S'First
and then (S (Last) = ' ' or S (Last) = ASCII.HT)
loop
Last := Last - 1;
end loop;
return S (S'First .. Last);
end Trim_Right;
procedure Parse_Line (Line : String) is
-- Find the effective line (strip comment)
Eff_Last : Natural := Line'Last;
Semi1 : Natural := 0;
Semi2 : Natural := 0;
Semi3 : Natural := 0;
begin
-- Strip trailing comment
for I in Line'Range loop
if Line (I) = '#' then
Eff_Last := I - 1;
exit;
end if;
end loop;
if Eff_Last < Line'First then
return;
end if;
-- Find semicolons
for I in Line'First .. Eff_Last loop
if Line (I) = ';' then
if Semi1 = 0 then
Semi1 := I;
elsif Semi2 = 0 then
Semi2 := I;
elsif Semi3 = 0 then
Semi3 := I;
end if;
end if;
end loop;
if Semi1 = 0 then
return;
end if;
-- Parse codepoint field
declare
CP_Str : constant String :=
Trim_Right (Line (Line'First .. Semi1 - 1));
Dot_Pos : Natural := 0;
CP_First : Positive;
CP_Last : Natural;
CP_Start_Val : Natural;
CP_End_Val : Natural;
begin
if CP_Str'Length = 0 then
return;
end if;
-- Trim leading spaces
CP_First := CP_Str'First;
CP_Last := CP_Str'Last;
while CP_First <= CP_Last
and then (CP_Str (CP_First) = ' '
or CP_Str (CP_First) = ASCII.HT)
loop
CP_First := CP_First + 1;
end loop;
if CP_First > CP_Last then
return;
end if;
-- Find ".."
for I in CP_First .. CP_Last - 1 loop
if CP_Str (I) = '.'
and then I + 1 <= CP_Last
and then CP_Str (I + 1) = '.'
then
Dot_Pos := I;
exit;
end if;
end loop;
if Dot_Pos > 0 then
CP_Start_Val := Parse_Hex (CP_Str (CP_First .. Dot_Pos - 1));
CP_End_Val := Parse_Hex (CP_Str (Dot_Pos + 2 .. CP_Last));
else
CP_Start_Val := Parse_Hex (CP_Str (CP_First .. CP_Last));
CP_End_Val := CP_Start_Val;
end if;
if CP_Start_Val > Max_Codepoint
or CP_End_Val > Max_Codepoint
then
return;
end if;
-- Parse status field
declare
Status_Str : constant String :=
Trim_Right (Line (Skip_Spaces (Line, Semi1 + 1) ..
(if Semi2 > 0 then Semi2 - 1 else Eff_Last)));
S : Status_Value := ST_Disallowed;
Has_Mapping : Boolean := False;
begin
if Status_Str = "valid" then
S := ST_Valid;
elsif Status_Str = "mapped" then
S := ST_Mapped;
Has_Mapping := True;
elsif Status_Str = "deviation" then
S := ST_Deviation;
Has_Mapping := True;
elsif Status_Str = "ignored" then
S := ST_Ignored;
elsif Status_Str = "disallowed" then
S := ST_Disallowed;
elsif Status_Str = "disallowed_STD3_valid" then
S := ST_Disallowed;
elsif Status_Str = "disallowed_STD3_mapped" then
S := ST_Disallowed;
end if;
-- Parse mapping if present
if Has_Mapping and Semi2 > 0 then
declare
Map_Str : constant String :=
Trim_Right (Line (Skip_Spaces (Line, Semi2 + 1) ..
(if Semi3 > 0 then Semi3 - 1 else Eff_Last)));
Map_Off : constant Natural := Map_Data_Len;
Map_Len : Natural := 0;
P : Positive := Map_Str'First;
begin
if Map_Str'Length > 0 then
-- Reserve slot for length
Map_Data_Len := Map_Data_Len + 1;
while P <= Map_Str'Last loop
-- Skip spaces
while P <= Map_Str'Last
and then (Map_Str (P) = ' '
or Map_Str (P) = ASCII.HT)
loop
P := P + 1;
end loop;
exit when P > Map_Str'Last;
-- Read hex
declare
Hex_Start : constant Positive := P;
Map_CP : Natural;
begin
while P <= Map_Str'Last
and then Map_Str (P) /= ' '
and then Map_Str (P) /= ASCII.HT
loop
P := P + 1;
end loop;
Map_CP := Parse_Hex
(Map_Str (Hex_Start .. P - 1));
if Map_CP <= Max_Codepoint
and then Map_Data_Len + 1 < Max_Map_Data
then
Map_Data (Map_Data_Len) := Map_CP;
Map_Data_Len := Map_Data_Len + 1;
Map_Len := Map_Len + 1;
end if;
end;
end loop;
-- Write length into reserved slot
if Map_Len > 0 then
Map_Data (Map_Off) := Map_Len;
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
Map_Index (C) := Map_Off;
end if;
end loop;
else
-- Empty mapping: undo the length reservation
Map_Data_Len := Map_Off;
end if;
end if;
end;
end if;
-- Set status for all CPs in range
for C in CP_Start_Val .. CP_End_Val loop
if C <= Max_Codepoint then
Status_Table (C) := S;
end if;
end loop;
end;
end;
end Parse_Line;
procedure Parse_IDNA_Table is
Pos : Positive := 1;
Line_End : Natural;
begin
while Pos <= Init_Length loop
-- Find end of line
Line_End := Pos;
while Line_End <= Init_Length
and then Init_Buffer (Line_End) /= LF_Byte
and then Init_Buffer (Line_End) /= CR_Byte
loop
Line_End := Line_End + 1;
end loop;
Line_End := Line_End - 1;
-- Process non-blank, non-comment lines
if Line_End >= Pos
and then Init_Buffer (Pos) /= Hash_Byte
then
declare
Len : constant Natural := Line_End - Pos + 1;
Line : String (1 .. Len);
begin
for I in 0 .. Len - 1 loop
Line (I + 1) :=
Character'Val (Init_Buffer (Pos + I));
end loop;
Parse_Line (Line);
end;
end if;
-- Advance past line ending
Pos := Line_End + 2;
if Pos <= Init_Length + 1
and then Pos > 1
and then Pos - 1 <= Init_Length
and then Init_Buffer (Pos - 1) = CR_Byte
and then Pos <= Init_Length
and then Init_Buffer (Pos) = LF_Byte
then
Pos := Pos + 1;
end if;
end loop;
end Parse_IDNA_Table;
begin
Is_Init := False;
Status_Table := [others => ST_Disallowed];
Map_Index := [others => 0];
Map_Data := [others => 0];
Map_Data_Len := 1; -- Reserve index 0 as "no mapping" sentinel
Success := False;
File_IO.Read_File
(UCD_Dir & "/IdnaMappingTable.txt",
Init_Buffer, Init_Length, OK);
if not OK or Init_Length = 0 then
return;
end if;
Parse_IDNA_Table;
Is_Init := True;
Success := True;
end Initialize;
---------------------------------------------------------------------------
-- Punycode helper functions
---------------------------------------------------------------------------
function Digit_To_Char (D : Natural) return Byte
with Pre => D < Puny_Base,
Post => Digit_To_Char'Result < 128
and then
((Digit_To_Char'Result in Puny_A_Lower .. Puny_Z_Lower)
or else
(Digit_To_Char'Result in Puny_Zero .. Puny_Nine))
is
begin
if D < 26 then
return Puny_A_Lower + D;
else
return Puny_Zero + (D - 26);
end if;
end Digit_To_Char;
function Char_To_Digit (C : Byte) return Natural is
begin
if C in Puny_A_Lower .. Puny_Z_Lower then
return C - Puny_A_Lower;
elsif C in Puny_A_Upper .. Puny_Z_Upper then
return C - Puny_A_Upper;
elsif C in Puny_Zero .. Puny_Nine then
return C - Puny_Zero + 26;
else
return Puny_Base;
end if;
end Char_To_Digit;
-- Adapt bias per RFC 3492 Section 6.1.
--
-- The while loop divides D by (Base - Tmin) = 35 each iteration,
-- so D strictly decreases. Starting from D <= Natural'Last, at
-- most 6 iterations can occur before D drops to <= 455.
-- K <= 6 * 36 = 216. Return value <= 216 + 33 = 249.
function Adapt
(Delta_Val : Natural;
Num_Points : Positive;
First_Time : Boolean) return Natural
with Post => Adapt'Result <= 683
is
Threshold_Val : constant Natural :=
((Puny_Base - Puny_Tmin) * Puny_Tmax) / 2; -- 455
Divisor : constant Positive := Puny_Base - Puny_Tmin; -- 35
D : Natural;
K : Natural := 0;
begin
if First_Time then
D := Delta_Val / Puny_Damp;
else
D := Delta_Val / 2;
end if;
D := D + D / Num_Points;
-- Unrolled adaptation loop. Each iteration divides D by 35 and
-- adds 36 to K. At most 6 real iterations needed (Natural'Last/35^6
-- = 33 < 456), but we spell out 7 for safety. After the last
-- iteration that runs, D <= Threshold_Val is guaranteed.
--
-- We track D's upper bound after each step to guide the prover.
-- D starts at most Natural'Last (2_147_483_647).
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
-- D <= max(455, 2_147_483_647 / 35) = 61_356_675
pragma Assert (D <= 61_356_675);
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
-- D <= max(455, 61_356_675 / 35) = 1_753_047
pragma Assert (D <= 1_753_047);
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
-- D <= max(455, 1_753_047 / 35) = 50_087
pragma Assert (D <= 50_087);
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
-- D <= max(455, 50_087 / 35) = 1431
pragma Assert (D <= 1431);
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
-- D <= max(455, 1431 / 35) = 455 (since 1431/35 = 40 < 455)
pragma Assert (D <= Threshold_Val);
-- After 5 steps D is guaranteed <= Threshold_Val.
-- Steps 6-7 are no-ops but included for completeness.
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
if D > Threshold_Val then
D := D / Divisor;
K := K + Puny_Base;
end if;
pragma Assert (D <= Threshold_Val);
pragma Assert (K <= 7 * Puny_Base);
-- D <= 455, K <= 252
-- Numer = 36 * D <= 16380. Denom = D + 38 >= 38.
-- Numer / Denom <= 16380 / 38 = 431. K + 431 <= 683.
declare
subtype Bounded_D is Natural range 0 .. Threshold_Val;
subtype Bounded_K is Natural range 0 .. 7 * Puny_Base;
BD : constant Bounded_D := D;
BK : constant Bounded_K := K;
Numer : constant Natural := BD * 36;
Denom : constant Positive := BD + Puny_Skew;
Ratio : constant Natural := Numer / Denom;
begin
return BK + Ratio;
end;
end Adapt;
function Threshold (K, Bias : Natural) return Natural
with Post => Threshold'Result in Puny_Tmin .. Puny_Tmax
is
begin
-- Rearranged to avoid Bias + Puny_Tmin/Tmax overflow.
-- K <= Bias + Tmin ⟺ K - Tmin <= Bias (when K >= Tmin)
-- K >= Bias + Tmax ⟺ K - Tmax >= Bias (when K >= Tmax)
if K <= Puny_Tmin or else K - Puny_Tmin <= Bias then
return Puny_Tmin;
elsif K >= Puny_Tmax and then K - Puny_Tmax >= Bias then
return Puny_Tmax;
else
return K - Bias;
end if;
end Threshold;
---------------------------------------------------------------------------
-- Punycode_Decode
---------------------------------------------------------------------------
procedure Punycode_Decode
(Input : Byte_Array;
Output : out CP_Work_Array;
Out_Len : out CP_Work_Length;
Success : out Boolean)
is
N : Natural := Puny_Initial_N;
I : Natural := 0;
Bias : Natural := Puny_Initial_Bias;
Basic_End : Natural := 0;
In_Pos : Positive;
begin
Output := [others => 0];
Out_Len := 0;
Success := False;
if Input'Length = 0 then
Success := True;
return;
end if;
-- Find last delimiter (hyphen)
for J in reverse Input'Range loop
if Input (J) = 16#2D# then
Basic_End := J;
exit;
end if;
end loop;
-- Copy basic code points (before last hyphen)
if Basic_End > 0 and Basic_End >= Input'First then
for J in Input'First .. Basic_End - 1 loop
if Out_Len = Max_Work_CPs then
return;
end if;
if Input (J) >= 128 then
return;
end if;
Out_Len := Out_Len + 1;
Output (Out_Len) := Input (J);
end loop;
In_Pos := Basic_End + 1;
else
In_Pos := Input'First;
end if;
-- Decode extended code points
while In_Pos <= Input'Last loop
pragma Loop_Invariant (N <= Max_Codepoint);
pragma Loop_Variant (Increases => Out_Len);
declare
Old_I : constant Natural := I;
W : Natural := 1;
K : Natural := Puny_Base;
Digit : Natural;
T : Natural;
begin
loop
pragma Loop_Invariant (W >= 1);
pragma Loop_Variant (Increases => In_Pos);
if In_Pos > Input'Last then
return;
end if;
Digit := Char_To_Digit (Input (In_Pos));
pragma Assert (In_Pos <= Input'Last);
In_Pos := In_Pos + 1;
if Digit >= Puny_Base then
return;
end if;
if Digit > (Natural'Last - I) / W then
return;
end if;
I := I + Digit * W;
T := Threshold (K, Bias);
exit when Digit < T;
if W > Natural'Last / (Puny_Base - T) then
return;
end if;
W := W * (Puny_Base - T);
if K > Natural'Last - Puny_Base then
return;
end if;
K := K + Puny_Base;
end loop;
if Out_Len = Max_Work_CPs then
return;
end if;
Out_Len := Out_Len + 1;
if I < Old_I then
-- Overflow occurred in I accumulation
return;
end if;
pragma Assert (Out_Len >= 1);
Bias := Adapt (I - Old_I, Out_Len, Old_I = 0);
if I / Out_Len > Natural'Last - N then
return;
end if;
N := N + I / Out_Len;
I := I mod Out_Len;
if N > Max_Codepoint then
return;
end if;
-- I = I mod Out_Len, so I in 0 .. Out_Len-1.
-- Out_Len <= Max_Work_CPs, so I+1 in 1 .. Max_Work_CPs.
pragma Assert (I <= Out_Len - 1);
pragma Assert (I + 1 <= Out_Len);
pragma Assert (N <= Max_Codepoint);
-- Insert N at position I+1, shifting elements right
if Out_Len > 1 then
for J in reverse I + 2 .. Out_Len loop
Output (J) := Output (J - 1);
end loop;
end if;
pragma Assert (N in Codepoint);
Output (I + 1) := N;
I := I + 1;
end;
end loop;
Success := True;
end Punycode_Decode;
---------------------------------------------------------------------------
-- Ghost: Punycode characterization helpers
--
-- RFC 3492 section 6.3 "Encoding procedure":
-- let b = the number of basic code points in the input
-- copy them to the output in order, followed by a delimiter if b > 0
--
-- Ghost_Basic_Count counts the ASCII (< 128) code points in the prefix
-- Input (1 .. Len). The Punycode encoder copies these verbatim at the
-- start of the output, then emits a hyphen delimiter (16#2D#) if any
-- were copied. The postcondition of Punycode_Encode asserts that on
-- success the output is at least this long (plus one for the delimiter
-- when the count is non-zero).
---------------------------------------------------------------------------
function Ghost_Basic_Count
(Input : CP_Work_Array;
Len : CP_Work_Length) return Natural
is (if Len = 0 then 0
elsif Input (Len) < 128 then Ghost_Basic_Count (Input, Len - 1) + 1
else Ghost_Basic_Count (Input, Len - 1))
with Ghost,
Post => Ghost_Basic_Count'Result <= Len,
Subprogram_Variant => (Decreases => Len);
-- Ghost_Basic_Position (Input, Len, K) returns the position I in
-- 1 .. Len such that Input (I) is the K-th basic (ASCII) code point
-- in the prefix Input (1 .. Len). Precondition guarantees K is in
-- range [1 .. Ghost_Basic_Count (Input, Len)], so the search always
-- succeeds. The encoder copies basic code points in order, so the
-- K-th byte of the output's basic prefix equals Input at this position.
function Ghost_Basic_Position
(Input : CP_Work_Array;
Len : Positive;
K : Positive) return Positive
is (if Input (Len) < 128
and then K = Ghost_Basic_Count (Input, Len)
then Len
else Ghost_Basic_Position (Input, Len - 1, K))
with Ghost,
Pre => Len <= Max_Work_CPs
and then K <= Ghost_Basic_Count (Input, Len),
Post => Ghost_Basic_Position'Result in 1 .. Len
and then Input (Ghost_Basic_Position'Result) < 128,
Subprogram_Variant => (Decreases => Len);
---------------------------------------------------------------------------
-- Punycode_Encode
---------------------------------------------------------------------------
procedure Punycode_Encode
(Input : CP_Work_Array;
In_Len : CP_Work_Length;
Output : out Byte_Array;
Out_Len : out Natural;
Success : out Boolean)
with Pre => Output'Length >= 1
and Output'Last < Natural'Last,
Post => Out_Len <= Output'Length
and then (if Success then
(for all I in Output'Range =>
(if I - Output'First < Out_Len then
Output (I) < 128))
and then
(if In_Len = 0 then Out_Len = 0)
and then
Out_Len >= Ghost_Basic_Count (Input, In_Len)
and then
(if Ghost_Basic_Count (Input, In_Len) > 0 then
Out_Len >=
Ghost_Basic_Count (Input, In_Len) + 1
and then
Output (Output'First
+ Ghost_Basic_Count
(Input, In_Len))
= 16#2D#)
and then
(if In_Len >= 1 then
(for all K in
1 .. Ghost_Basic_Count (Input, In_Len) =>
Output (Output'First + K - 1)
= Input (Ghost_Basic_Position
(Input, In_Len, K))))
and then
-- Length lower bound:
-- every extended (non-basic) codepoint
-- contributes at least one emitted byte,
-- so the encoded output is at least as
-- long as In_Len plus a delimiter byte
-- when any basic codepoints were copied.
-- Covers all-basic (equality), all-extended,
-- and the mixed case uniformly.
(if In_Len >= 1 then
Out_Len >= In_Len +
(if Ghost_Basic_Count
(Input, In_Len) > 0
then 1 else 0)))
is
N : Natural := Puny_Initial_N;
Delt : Natural := 0;
Bias : Natural := Puny_Initial_Bias;
H : Natural;
B : Natural := 0;
begin
Output := [others => 0];
Out_Len := 0;
Success := False;
if In_Len = 0 then
Success := True;
return;
end if;
-- Copy basic code points
for I in 1 .. In_Len loop
pragma Loop_Invariant (B <= I - 1);
pragma Loop_Invariant (Out_Len <= I - 1);
pragma Loop_Invariant (Out_Len = B);
pragma Loop_Invariant (B = Ghost_Basic_Count (Input, I - 1));
pragma Loop_Invariant (Out_Len <= Output'Length);
pragma Loop_Invariant
(for all J in Output'Range =>
(if J - Output'First < Out_Len then Output (J) < 128));
pragma Loop_Invariant
(if I >= 2 then
(for all K in 1 .. B =>
Output (Output'First + K - 1)
= Input (Ghost_Basic_Position (Input, I - 1, K))));
if Input (I) < 128 then
if Out_Len >= Output'Length then
return;
end if;
Out_Len := Out_Len + 1;
Output (Output'First + Out_Len - 1) := Input (I);
B := B + 1;
end if;
end loop;
-- After copy loop: B counts all basic CPs in Input (1 .. In_Len)
pragma Assert (B = Ghost_Basic_Count (Input, In_Len));
pragma Assert (Out_Len = B);
pragma Assert
(if In_Len >= 1 then
(for all K in 1 .. B =>
Output (Output'First + K - 1)
= Input (Ghost_Basic_Position (Input, In_Len, K))));
H := B;
-- Add delimiter if there were basic code points
if B > 0 then
if Out_Len >= Output'Length then
return;
end if;
Out_Len := Out_Len + 1;
Output (Output'First + Out_Len - 1) := 16#2D#;
pragma Assert (Out_Len = B + 1);
pragma Assert (Output (Output'First + B) = 16#2D#);
end if;
-- Main encoding loop
while H < In_Len loop
pragma Loop_Variant (Increases => N);
pragma Loop_Invariant (Out_Len <= Output'Length);
pragma Loop_Invariant (B = Ghost_Basic_Count (Input, In_Len));
pragma Loop_Invariant (Out_Len >= B);
pragma Loop_Invariant (if B > 0 then Out_Len >= B + 1);
pragma Loop_Invariant
(if B > 0 then Output (Output'First + B) = 16#2D#);
pragma Loop_Invariant
(if In_Len >= 1 then
(for all K in 1 .. B =>
Output (Output'First + K - 1)
= Input (Ghost_Basic_Position (Input, In_Len, K))));
pragma Loop_Invariant
(for all J in Output'Range =>
(if J - Output'First < Out_Len then Output (J) < 128));
-- Progress: H grows by at least one per emitted delta.
pragma Loop_Invariant (H >= B);
pragma Loop_Invariant
(Out_Len >= H + (if B > 0 then 1 else 0));
declare
M : Natural := Natural'Last;
begin
-- Find minimum codepoint >= N
for I in 1 .. In_Len loop
if Input (I) >= N and Input (I) < M then
M := Input (I);
end if;
end loop;
if M < N then
-- No CP >= N found; should not happen in valid input
return;
end if;
if M - N > (Natural'Last - Delt) / (H + 1) then
return;
end if;
Delt := Delt + (M - N) * (H + 1);
N := M;
for I in 1 .. In_Len loop
pragma Loop_Invariant (Out_Len <= Output'Length);
pragma Loop_Invariant (B = Ghost_Basic_Count (Input, In_Len));
pragma Loop_Invariant (Out_Len >= B);
pragma Loop_Invariant (if B > 0 then Out_Len >= B + 1);
pragma Loop_Invariant
(if B > 0 then Output (Output'First + B) = 16#2D#);
pragma Loop_Invariant
(if In_Len >= 1 then
(for all KK in 1 .. B =>
Output (Output'First + KK - 1)
= Input (Ghost_Basic_Position (Input, In_Len, KK))));
pragma Loop_Invariant
(for all J in Output'Range =>
(if J - Output'First < Out_Len then Output (J) < 128));
pragma Loop_Invariant (H >= B);
pragma Loop_Invariant
(Out_Len >= H + (if B > 0 then 1 else 0));
if Input (I) < N then
if Delt = Natural'Last then
return;
end if;
Delt := Delt + 1;
elsif Input (I) = N then
-- Encode Delt as variable-length integer
declare
Q : Natural := Delt;
K : Natural := Puny_Base;
T : Natural;
begin
loop
pragma Loop_Variant (Decreases => Q);
pragma Loop_Invariant (Out_Len <= Output'Length);
pragma Loop_Invariant
(B = Ghost_Basic_Count (Input, In_Len));
pragma Loop_Invariant (Out_Len >= B);
pragma Loop_Invariant
(if B > 0 then Out_Len >= B + 1);
pragma Loop_Invariant
(if B > 0 then
Output (Output'First + B) = 16#2D#);
pragma Loop_Invariant
(if In_Len >= 1 then
(for all KK in 1 .. B =>
Output (Output'First + KK - 1)
= Input (Ghost_Basic_Position
(Input, In_Len, KK))));
pragma Loop_Invariant
(for all J in Output'Range =>
(if J - Output'First < Out_Len then
Output (J) < 128));
pragma Loop_Invariant (H >= B);
pragma Loop_Invariant
(Out_Len >= H + (if B > 0 then 1 else 0));
if Out_Len >= Output'Length then
return;
end if;
T := Threshold (K, Bias);
if Q < T then
Out_Len := Out_Len + 1;
Output (Output'First + Out_Len - 1) :=
Digit_To_Char (Q);
exit;
end if;
Out_Len := Out_Len + 1;
Output (Output'First + Out_Len - 1) :=
Digit_To_Char (T + (Q - T) mod (Puny_Base - T));
Q := (Q - T) / (Puny_Base - T);
if K > Natural'Last - Puny_Base then
return;
end if;
K := K + Puny_Base;
end loop;
end;
if H = Natural'Last then
return;
end if;
Bias := Adapt (Delt, H + 1, H = B);
Delt := 0;
H := H + 1;
end if;
end loop;
if Delt = Natural'Last then
return;
end if;
Delt := Delt + 1;
if N = Natural'Last then
return;
end if;
N := N + 1;
end;
end loop;
Success := True;
end Punycode_Encode;
---------------------------------------------------------------------------
-- ContextJ validation helpers
---------------------------------------------------------------------------
function ZWNJ_Context_Valid
(CPs : CP_Work_Array;
Len : CP_Work_Length;
Pos : Positive) return Boolean
with Global => (Input => (Properties.Property_State,
Normalization.Norm_State)),
Pre => Properties.Initialized
and then Normalization.Initialized
and then Pos <= Len
and then Len <= Max_Work_CPs
is
JT : JT_Value;
begin
if Pos = 1 then
return False;
end if;
-- Pos >= 2 and Pos <= Len <= Max_Work_CPs
pragma Assert (Pos >= 2 and Pos <= Max_Work_CPs);
-- Rule A: Preceding CP has CCC=9 (Virama)
if Normalization.Get_CCC (CPs (Pos - 1)) = Virama_CCC then
pragma Assert
(ZWNJ_Valid_After_Virama (Normalization.Get_CCC (CPs (Pos - 1))));
return True;
end if;
-- Rule B: Cursive joining context
-- (JT:{L,D})(JT:T)* ZWNJ (JT:T)*(JT:{R,D})
-- Search backward past JT=T for JT in {L, D}
declare
Found_Left : Boolean := False;
J : Natural := Pos - 1;
begin
while J >= 1 loop
pragma Loop_Invariant (J <= Max_Work_CPs);
pragma Loop_Variant (Decreases => J);
JT := Properties.Get_JT (CPs (J));
if Is_Transparent (JT) then
if J = 1 then
exit;
end if;
J := J - 1;
elsif Is_Left_Or_Dual (JT) then
Found_Left := True;
exit;
else
exit;
end if;
end loop;
if not Found_Left then
return False;
end if;
end;
-- Search forward past JT=T for JT in {R, D}
declare
J : Natural := Pos + 1;
begin
while J <= Len loop
pragma Loop_Invariant (J >= 1 and J <= Max_Work_CPs);
pragma Loop_Variant (Increases => J);
JT := Properties.Get_JT (CPs (J));
if Is_Transparent (JT) then
J := J + 1;
elsif Is_Right_Or_Dual (JT) then
return True;
else
return False;
end if;
end loop;
return False;
end;
end ZWNJ_Context_Valid;
function ZWJ_Context_Valid
(CPs : CP_Work_Array;
Len : CP_Work_Length;
Pos : Positive) return Boolean
with Global => (Input => Normalization.Norm_State),
Pre => Normalization.Initialized
and then Pos <= Len
and then Len <= Max_Work_CPs
is
pragma Unreferenced (Len);
begin
if Pos = 1 then
return False;
end if;
-- Ghost assertion: ZWJ validity matches spec predicate
pragma Assert
(ZWJ_Valid_After_Virama (Normalization.Get_CCC (CPs (Pos - 1)))
= (Normalization.Get_CCC (CPs (Pos - 1)) = Virama_CCC));
return Normalization.Get_CCC (CPs (Pos - 1)) = Virama_CCC;
end ZWJ_Context_Valid;
---------------------------------------------------------------------------
-- Bidi validation (RFC 5893)
---------------------------------------------------------------------------
function Bidi_Label_Valid
(CPs : CP_Work_Array;
Len : CP_Work_Length) return Boolean
with Global => (Input => Properties.Property_State),
Pre => Properties.Initialized
and then Len <= Max_Work_CPs,
Post => (if Bidi_Label_Valid'Result and Len >= 1 then
-- Platinum: Rule 1 — first char is L, R, or AL
Bidi_Rule1_Valid (Properties.Get_BC (CPs (1)))
-- Platinum: Rule 2/5 — all CPs have allowed BC
and then
(if Is_RTL_Label (Properties.Get_BC (CPs (1))) then
(for all I in 1 .. Len =>
RTL_Allowed (Properties.Get_BC (CPs (I))))
else
(for all I in 1 .. Len =>
LTR_Allowed (Properties.Get_BC (CPs (I)))))
-- Platinum: Rule 4 — RTL: not both EN and AN
and then
(if Is_RTL_Label (Properties.Get_BC (CPs (1))) then
not ((for some I in 1 .. Len =>
Properties.Get_BC (CPs (I)) =
Bidi_Spec.BC_EN)
and
(for some I in 1 .. Len =>
Properties.Get_BC (CPs (I)) =
Bidi_Spec.BC_AN))))
is
use Bidi_Spec;
First_BC : BC_Value;
RTL_Label : Boolean;
BC : BC_Value;
Has_EN : Boolean := False;
Has_AN : Boolean := False;
Last_Non_NSM : BC_Value := BC_Default;
begin
if Len = 0 then
return True;
end if;
First_BC := Properties.Get_BC (CPs (1));
-- Rule 1: First character must be L, R, or AL
if not Bidi_Rule1_Valid (First_BC) then
return False;
end if;
pragma Assert (Bidi_Rule1_Valid (First_BC));
RTL_Label := Is_RTL_Label (First_BC);
for I in 1 .. Len loop
-- Platinum: track that all checked CPs have allowed BC
pragma Loop_Invariant
(if RTL_Label then
(for all J in 1 .. I - 1 =>
RTL_Allowed (Properties.Get_BC (CPs (J))))
else
(for all J in 1 .. I - 1 =>
LTR_Allowed (Properties.Get_BC (CPs (J)))));
-- Platinum: Has_EN/Has_AN tracking (RTL labels only)
pragma Loop_Invariant
(if RTL_Label and Has_EN then
(for some J in 1 .. I - 1 =>
Properties.Get_BC (CPs (J)) = BC_EN));
pragma Loop_Invariant
(if RTL_Label and Has_AN then
(for some J in 1 .. I - 1 =>
Properties.Get_BC (CPs (J)) = BC_AN));
pragma Loop_Invariant
(if RTL_Label and not Has_EN then
(for all J in 1 .. I - 1 =>
Properties.Get_BC (CPs (J)) /= BC_EN));
pragma Loop_Invariant
(if RTL_Label and not Has_AN then
(for all J in 1 .. I - 1 =>
Properties.Get_BC (CPs (J)) /= BC_AN));
BC := Properties.Get_BC (CPs (I));
if RTL_Label then
-- Rule 2: RTL allowed types only
if not RTL_Allowed (BC) then
return False;
end if;
if BC = BC_EN then
Has_EN := True;
elsif BC = BC_AN then
Has_AN := True;
end if;
else
-- Rule 5: LTR allowed types only
if not LTR_Allowed (BC) then
return False;
end if;
end if;
if BC /= BC_NSM then
Last_Non_NSM := BC;
end if;
end loop;
-- Rule 3/6: End character check
if RTL_Label then
if not RTL_End_Valid (Last_Non_NSM) then
return False;
end if;
-- Rule 4: Cannot have both EN and AN
if Has_EN and Has_AN then
return False;
end if;
else
if not LTR_End_Valid (Last_Non_NSM) then
return False;
end if;
end if;
-- Platinum: connect locals to postcondition
pragma Assert (First_BC = Properties.Get_BC (CPs (1)));
pragma Assert (RTL_Label = Is_RTL_Label (First_BC));
pragma Assert (Bidi_Rule1_Valid (First_BC));
return True;
end Bidi_Label_Valid;
---------------------------------------------------------------------------
-- Domain-level Bidi detection: check if any CP in the domain has
-- BC in {R, AL, AN}. If so, the domain is Bidi and all labels must
-- satisfy RFC 5893 rules.
---------------------------------------------------------------------------
function CPs_Has_RTL
(CPs : CP_Work_Array;
Len : CP_Work_Length) return Boolean
with Global => (Input => Properties.Property_State),
Pre => Properties.Initialized
and then Len <= Max_Work_CPs
is
use Bidi_Spec;
BC : BC_Value;
begin
for I in 1 .. Len loop
BC := Properties.Get_BC (CPs (I));
if BC = BC_R or BC = BC_AL or BC = BC_AN then
return True;
end if;
end loop;
return False;
end CPs_Has_RTL;
-- Determine if the domain is a Bidi domain. Checks all labels including
-- decoded ACE labels. A domain is Bidi if any codepoint has BC in
-- {R, AL, AN} per UTS #46 Section 4.1 / RFC 5893.
function Domain_Is_Bidi_Check
(NFC_CPs : CP_Work_Array;
NFC_Len : CP_Work_Length;
Labels : Label_Array;
Num_Labels : Label_Count) return Boolean
with Global => (Input => Properties.Property_State),
Pre => Properties.Initialized
and then NFC_Len <= Max_Work_CPs
is
begin
-- First check all NFC codepoints (covers non-ACE labels and dots)
if CPs_Has_RTL (NFC_CPs, NFC_Len) then
return True;
end if;
-- Also check decoded ACE labels (NFC_CPs has ASCII for ACE labels,
-- but decoded form may contain RTL characters)
for L in 1 .. Num_Labels loop
if Labels (L).End_Idx >= Labels (L).Start_Idx
and then Labels (L).Start_Idx <= Max_Work_CPs - 3
and then Labels (L).End_Idx <= Max_Work_CPs
then
declare
Label_Len : constant Natural :=
Labels (L).End_Idx - Labels (L).Start_Idx + 1;
S : constant Natural := Labels (L).Start_Idx;
begin
if Label_Len >= 4
and then (NFC_CPs (S) = 16#78# or NFC_CPs (S) = 16#58#)
and then (NFC_CPs (S + 1) = 16#6E#
or NFC_CPs (S + 1) = 16#4E#)
and then NFC_CPs (S + 2) = Hyphen_CP
and then NFC_CPs (S + 3) = Hyphen_CP
then
-- ACE label: try to decode and check for RTL
declare
Puny_In_Len : constant Natural := Label_Len - 4;
Puny_In : Byte_Array
(1 .. Natural'Max (Puny_In_Len, 1)) := [others => 0];
Decoded : CP_Work_Array;
Dec_Len : CP_Work_Length;
Puny_OK : Boolean;
begin
for I in S + 4 .. Labels (L).End_Idx loop
if I - S - 3 >= 1
and then I - S - 3 <= Puny_In'Last
and then NFC_CPs (I) <= 255
then
Puny_In (I - S - 3) := NFC_CPs (I);
end if;
end loop;
Punycode_Decode
(Puny_In (1 .. Puny_In_Len),
Decoded, Dec_Len, Puny_OK);
if Puny_OK and then CPs_Has_RTL (Decoded, Dec_Len) then
return True;
end if;
end;
end if;
end;
end if;
end loop;
return False;
end Domain_Is_Bidi_Check;
---------------------------------------------------------------------------
-- Label validation (UTS #46 Section 4.1)
---------------------------------------------------------------------------
-- Ghost_Is_Leading_CM (CP) captures criterion 6 of UTS #46 §4.1:
-- CP is a "leading combining mark", i.e. its General_Category value's
-- name begins with 'M' (Mc, Me, Mn). Labels whose first codepoint
-- satisfies this predicate must be rejected.
function Ghost_Is_Leading_CM (CP : Codepoint) return Boolean
is (Properties.Get_GC (CP) in 1 .. Properties.GC_Name_Count
and then Properties.GC_Name (Properties.Get_GC (CP))'Length >= 1
and then Properties.GC_Name (Properties.Get_GC (CP))
(Properties.GC_Name (Properties.Get_GC (CP))'First) = 'M')
with Ghost,
Global => Properties.Property_State,
Pre => Properties.Initialized;
procedure Validate_Label
(CPs : CP_Work_Array;
Len : CP_Work_Length;
Options : IDNA_Options;
Domain_Is_Bidi : Boolean;
Status : out IDNA_Result;
Valid : out Boolean)
with Global => (Input => (Status_Table,
Properties.Property_State,
Normalization.Norm_State)),
Pre => Properties.Initialized
and then Normalization.Initialized,
Post => (if Status = Success then Valid)
and then
(if Valid then
Len >= 1
-- Criterion 5: no U+002E (full stop) in label
and then (for all I in 1 .. Len => CPs (I) /= Dot_CP)
-- Criterion 2: no hyphen in both positions 3 and 4
and then (if Options.Check_Hyphens and Len >= 4 then
not (CPs (3) = Hyphen_CP
and CPs (4) = Hyphen_CP))
-- Criterion 3: no leading/trailing hyphen
and then (if Options.Check_Hyphens then
CPs (1) /= Hyphen_CP
and then CPs (Len) /= Hyphen_CP)
-- Criterion 6: no leading combining mark
and then not Ghost_Is_Leading_CM (CPs (1))
-- Criterion 7: each CP has valid/deviation status
and then (for all I in 1 .. Len =>
Status_Valid_Nontransitional
(Status_Table (CPs (I))))
-- Criterion 7 STD3 addendum: ASCII CPs pass STD3
and then (if Options.Use_STD3_Rules then
(for all I in 1 .. Len =>
(if CPs (I) < 128 then
STD3_ASCII_Valid (CPs (I)))))
-- Criterion 8: ContextJ (ZWNJ / ZWJ rules)
and then (if Options.Check_Joiners then
(for all I in 1 .. Len =>
(if CPs (I) = 16#200C# then
ZWNJ_Context_Valid (CPs, Len, I))
and then
(if CPs (I) = 16#200D# then
ZWJ_Context_Valid (CPs, Len, I))))
-- Criterion 9: Bidi rule when the domain is Bidi
and then (if Options.Check_Bidi and Domain_Is_Bidi then
Bidi_Label_Valid (CPs, Len)))
is
S : Status_Value;
begin
Status := Success;
Valid := False;
if Len = 0 then
Status := Empty_Label;
return;
end if;
-- Criterion 2: No hyphen in positions 3 and 4 (if CheckHyphens)
if Options.Check_Hyphens and Len >= 4 then
if CPs (3) = Hyphen_CP and CPs (4) = Hyphen_CP then
Status := Invalid_Hyphen;
return;
end if;
end if;
-- Criterion 3: No leading/trailing hyphen (if CheckHyphens)
if Options.Check_Hyphens then
if CPs (1) = Hyphen_CP or CPs (Len) = Hyphen_CP then
Status := Invalid_Hyphen;
return;
end if;
end if;
-- Criterion 5: No U+002E (FULL STOP) in label
for I in 1 .. Len loop
pragma Loop_Invariant
(for all J in 1 .. I - 1 => CPs (J) /= Dot_CP);
if CPs (I) = Dot_CP then
Status := Invalid_Input;
return;
end if;
end loop;
-- Criterion 6: No leading combining mark (GC starts with M)
declare
GC_Idx : constant Natural := Properties.Get_GC (CPs (1));
begin
if GC_Idx >= 1 and GC_Idx <= Properties.GC_Name_Count then
declare
GC_Name : constant String := Properties.GC_Name (GC_Idx);
begin
if GC_Name'Length >= 1
and then GC_Name (GC_Name'First) = 'M'
then
Status := Leading_Combining_Mark;
return;
end if;
end;
end if;
end;
-- Criterion 7: Each CP status is valid or deviation (nontransitional)
for I in 1 .. Len loop
pragma Loop_Invariant
(for all J in 1 .. I - 1 =>
Status_Valid_Nontransitional (Status_Table (CPs (J))));
pragma Loop_Invariant
(if Options.Use_STD3_Rules then
(for all J in 1 .. I - 1 =>
(if CPs (J) < 128 then STD3_ASCII_Valid (CPs (J)))));
S := Status_Table (CPs (I));
if not Status_Valid_Nontransitional (S) then
Status := Disallowed_Codepoint;
return;
end if;
-- STD3 check for ASCII
if Options.Use_STD3_Rules and CPs (I) < 128 then
if not STD3_ASCII_Valid (CPs (I)) then
Status := STD3_Failure;
return;
end if;
end if;
end loop;
-- Criterion 8: ContextJ rules (if CheckJoiners)
if Options.Check_Joiners then
for I in 1 .. Len loop
pragma Loop_Invariant
(for all J in 1 .. I - 1 =>
(if CPs (J) = 16#200C# then
ZWNJ_Context_Valid (CPs, Len, J))
and then
(if CPs (J) = 16#200D# then
ZWJ_Context_Valid (CPs, Len, J)));
if CPs (I) = 16#200C# then
if not ZWNJ_Context_Valid (CPs, Len, I) then
Status := ContextJ_Failure;
return;
end if;
elsif CPs (I) = 16#200D# then
if not ZWJ_Context_Valid (CPs, Len, I) then
Status := ContextJ_Failure;
return;
end if;
end if;
end loop;
end if;
-- Criterion 9: Bidi rules (if CheckBidi and domain is Bidi)
-- A domain is Bidi if ANY label has R/AL/AN characters.
-- When the domain is Bidi, ALL labels must satisfy RFC 5893 rules.
if Options.Check_Bidi and Domain_Is_Bidi then
if not Bidi_Label_Valid (CPs, Len) then
Status := Bidi_Failure;
return;
end if;
end if;
Valid := True;
end Validate_Label;
---------------------------------------------------------------------------
-- Shared processing: decode, map, normalize, split
---------------------------------------------------------------------------
procedure Decode_UTF8_To_CPs
(Input : Byte_Array;
CPs : out CP_Work_Array;
CP_Len : out CP_Work_Length;
Status : out IDNA_Result)
is
Pos : Positive := Input'First;
CP : Codepoint;
Enc_Len : Positive;
Valid : Boolean;
begin
CPs := [others => 0];
CP_Len := 0;
Status := Success;
while Pos <= Input'Last loop
pragma Loop_Invariant (Pos >= Input'First);
pragma Loop_Invariant (Pos <= Input'Last);
pragma Loop_Variant (Increases => Pos);
UTF8.Decode (Input, Pos, CP, Enc_Len, Valid);
if not Valid then
Status := Invalid_Input;
return;
end if;
if CP_Len = Max_Work_CPs then
Status := Buffer_Overflow;
return;
end if;
CP_Len := CP_Len + 1;
CPs (CP_Len) := CP;
if Pos > Input'Last - Enc_Len + 1 then
exit;
end if;
Pos := Pos + Enc_Len;
end loop;
end Decode_UTF8_To_CPs;
procedure Apply_Mapping
(Input : CP_Work_Array;
In_Len : CP_Work_Length;
Output : out CP_Work_Array;
Out_Len : out CP_Work_Length;
Status : out IDNA_Result)
is
S : Status_Value;
M_Off : Natural;
M_Len : Natural;
begin
Output := [others => 0];
Out_Len := 0;
Status := Success;
for I in 1 .. In_Len loop
S := Status_Table (Input (I));
case S is
when ST_Valid | ST_Deviation =>
-- Keep as-is (nontransitional)
pragma Assert (Status_Valid_Nontransitional (S));
if Out_Len = Max_Work_CPs then
Status := Buffer_Overflow;
return;
end if;
Out_Len := Out_Len + 1;
Output (Out_Len) := Input (I);
when ST_Mapped =>
M_Off := Map_Index (Input (I));
if M_Off > 0 and M_Off < Max_Map_Data then
M_Len := Map_Data (M_Off);
if M_Len > 0 and M_Len <= Max_Mapping_CPs then
for J in 1 .. M_Len loop
if Out_Len = Max_Work_CPs then
Status := Buffer_Overflow;
return;
end if;
if M_Off + J < Max_Map_Data then
declare
MV : constant Natural := Map_Data (M_Off + J);
begin
if MV <= Max_Codepoint then
Out_Len := Out_Len + 1;
Output (Out_Len) := MV;
else
Status := Invalid_Input;
return;
end if;
end;
end if;
end loop;
end if;
end if;
when ST_Ignored =>
null;
when ST_Disallowed =>
Status := Disallowed_Codepoint;
return;
end case;
end loop;
end Apply_Mapping;
procedure CPs_To_UTF8
(CPs : CP_Work_Array;
CP_Len : CP_Work_Length;
Output : out Byte_Array;
Last : out Natural;
Status : out IDNA_Result)
is
Pos : Positive := Output'First;
Enc_Len : Positive;
begin
Output := [others => 0];
Last := Output'First - 1;
Status := Success;
for I in 1 .. CP_Len loop
pragma Loop_Invariant (Pos >= Output'First);
pragma Loop_Invariant (Pos <= Output'Last + 1);
if not Is_Scalar_Value (CPs (I)) then
Status := Invalid_Input;
return;
end if;
declare
Needed : constant Positive :=
(if CPs (I) <= 16#7F# then 1
elsif CPs (I) <= 16#7FF# then 2
elsif CPs (I) <= 16#FFFF# then 3
else 4);
Remaining : constant Natural := Output'Last - Pos + 1;
begin
if Needed > Remaining then
Status := Buffer_Overflow;
return;
end if;
UTF8.Encode (CPs (I), Output, Pos, Enc_Len);
Pos := Pos + Enc_Len;
end;
end loop;
Last := Pos - 1;
end CPs_To_UTF8;
---------------------------------------------------------------------------
-- NFC check for decoded labels (V1: decoded ACE labels must be in NFC)
---------------------------------------------------------------------------
function Is_NFC
(CPs : CP_Work_Array;
Len : CP_Work_Length) return Boolean
with Global => (Input => Normalization.Norm_State),
Pre => Normalization.Initialized
and then Normalization.Data_All_Terminal
is
use type Normalization.Norm_Status;
UTF8_Buf : Byte_Array (1 .. Max_Work_Bytes);
NFC_Buf : Byte_Array (1 .. Max_Work_Bytes) := [others => 0];
UTF8_Last : Natural;
NFC_Last : Natural;
Norm_Status : Normalization.Norm_Status;
UTF8_Status : IDNA_Result;
NFC_CPs : CP_Work_Array;
NFC_Len : CP_Work_Length;
Dec_Status : IDNA_Result;
begin
if Len = 0 then
return True;
end if;
CPs_To_UTF8 (CPs, Len, UTF8_Buf, UTF8_Last, UTF8_Status);
if UTF8_Status /= Success or UTF8_Last < UTF8_Buf'First then
return False;
end if;
Normalization.Normalize
(UTF8_Buf (UTF8_Buf'First .. UTF8_Last), NFC,
NFC_Buf, NFC_Last, Norm_Status);
if Norm_Status /= Normalization.Success then
return False;
end if;
Decode_UTF8_To_CPs
(NFC_Buf (NFC_Buf'First .. NFC_Last), NFC_CPs, NFC_Len, Dec_Status);
if Dec_Status /= Success then
return False;
end if;
if NFC_Len /= Len then
return False;
end if;
for I in 1 .. Len loop
if NFC_CPs (I) /= CPs (I) then
return False;
end if;
end loop;
return True;
end Is_NFC;
---------------------------------------------------------------------------
-- Punycode round-trip check (P4: encode(decode(input)) must equal input)
---------------------------------------------------------------------------
function Punycode_Round_Trip_OK
(Original_ACE : Byte_Array;
Decoded_CPs : CP_Work_Array;
Decoded_Len : CP_Work_Length) return Boolean
is
-- Buffer large enough for any valid Punycode encoding
Re_Encoded : Byte_Array (1 .. Max_Work_Bytes);
Re_Len : Natural;
Re_OK : Boolean;
begin
Punycode_Encode (Decoded_CPs, Decoded_Len, Re_Encoded, Re_Len, Re_OK);
if not Re_OK then
return False;
end if;
if Re_Len /= Original_ACE'Length then
return False;
end if;
-- Re_Len <= Re_Encoded'Length = Max_Work_Bytes (bounded by Punycode_Encode)
if Re_Len > Re_Encoded'Length or Re_Len > Original_ACE'Length then
return False;
end if;
-- Case-insensitive comparison (Punycode is case-insensitive)
for I in 0 .. Re_Len - 1 loop
pragma Loop_Invariant (Re_Encoded'First + I <= Re_Encoded'Last);
pragma Loop_Invariant (Original_ACE'First + I <= Original_ACE'Last);
declare
A : Byte := Original_ACE (Original_ACE'First + I);
B : Byte := Re_Encoded (Re_Encoded'First + I);
begin
if A in Puny_A_Upper .. Puny_Z_Upper then
A := A + 32;
end if;
if B in Puny_A_Upper .. Puny_Z_Upper then
B := B + 32;
end if;
if A /= B then
return False;
end if;
end;
end loop;
return True;
end Punycode_Round_Trip_OK;
procedure Normalize_NFC
(Mapped : CP_Work_Array;
Map_Len : CP_Work_Length;
NFC_CPs : out CP_Work_Array;
NFC_Len : out CP_Work_Length;
Status : out IDNA_Result)
with Global => (Input => Normalization.Norm_State),
Pre => Normalization.Initialized
and then Normalization.Data_All_Terminal
is
use type Normalization.Norm_Status;
Norm_In : Byte_Array (1 .. Max_Work_Bytes);
Norm_Out : Byte_Array (1 .. Max_Work_Bytes) := [others => 0];
UTF8_Last : Natural;
Norm_Last : Natural;
Norm_Status : Normalization.Norm_Status;
UTF8_Status : IDNA_Result;
begin
NFC_CPs := [others => 0];
NFC_Len := 0;
if Map_Len = 0 then
Status := Invalid_Input;
return;
end if;
-- Encode mapped CPs to UTF-8
CPs_To_UTF8 (Mapped, Map_Len, Norm_In, UTF8_Last, UTF8_Status);
if UTF8_Status /= Success then
Status := UTF8_Status;
return;
end if;
if UTF8_Last < Norm_In'First then
Status := Invalid_Input;
return;
end if;
-- NFC normalize
Normalization.Normalize
(Norm_In (Norm_In'First .. UTF8_Last), NFC,
Norm_Out, Norm_Last, Norm_Status);
if Norm_Status /= Normalization.Success then
Status := NFC_Failure;
return;
end if;
-- Decode NFC result back to codepoints
Decode_UTF8_To_CPs
(Norm_Out (Norm_Out'First .. Norm_Last), NFC_CPs, NFC_Len, Status);
if Status /= Success then
Status := NFC_Failure;
end if;
end Normalize_NFC;
function Is_Dot_Or_Variant (CP : Codepoint) return Boolean is
begin
return CP = 16#002E# -- FULL STOP
or CP = 16#3002# -- IDEOGRAPHIC FULL STOP
or CP = 16#FF0E# -- FULLWIDTH FULL STOP
or CP = 16#FF61#; -- HALFWIDTH IDEOGRAPHIC FULL STOP
end Is_Dot_Or_Variant;
procedure Split_Labels
(CPs : CP_Work_Array;
CP_Len : CP_Work_Length;
Labels : out Label_Array;
Num_Labels : out Label_Count;
Has_Trailing_Dot : out Boolean;
Status : out IDNA_Result)
is
Label_Start : Positive := 1;
begin
Labels := [others => (Start_Idx => 1, End_Idx => 0)];
Num_Labels := 0;
Has_Trailing_Dot := False;
Status := Success;
for I in 1 .. CP_Len loop
if CPs (I) = Dot_CP then
if Num_Labels = Max_Labels then
Status := Too_Many_Labels;
return;
end if;
Num_Labels := Num_Labels + 1;
Labels (Num_Labels) :=
(Start_Idx => Label_Start, End_Idx => I - 1);
Label_Start := I + 1;
end if;
end loop;
-- Check for trailing dot (root label)
if CP_Len >= 1 and then CPs (CP_Len) = Dot_CP then
Has_Trailing_Dot := True;
-- All labels already added above; no final non-dot label to add
return;
end if;
-- Add final label (when no trailing dot)
if Label_Start <= CP_Len or Num_Labels = 0 then
if Num_Labels = Max_Labels then
Status := Too_Many_Labels;
return;
end if;
Num_Labels := Num_Labels + 1;
Labels (Num_Labels) :=
(Start_Idx => Label_Start,
End_Idx => (if Label_Start <= CP_Len
then CP_Len else Label_Start - 1));
end if;
end Split_Labels;
-- Split labels on dots AND dot variants (for pre-mapping CPs)
procedure Split_Labels_Pre_Map
(CPs : CP_Work_Array;
CP_Len : CP_Work_Length;
Labels : out Label_Array;
Num_Labels : out Label_Count)
is
Label_Start : Positive := 1;
begin
Labels := [others => (Start_Idx => 1, End_Idx => 0)];
Num_Labels := 0;
for I in 1 .. CP_Len loop
if Is_Dot_Or_Variant (CPs (I)) then
if Num_Labels = Max_Labels then
return;
end if;
Num_Labels := Num_Labels + 1;
Labels (Num_Labels) :=
(Start_Idx => Label_Start, End_Idx => I - 1);
Label_Start := I + 1;
end if;
end loop;
-- Trailing dot: don't add final label
if CP_Len >= 1 and then Is_Dot_Or_Variant (CPs (CP_Len)) then
return;
end if;
-- Add final label
if Label_Start <= CP_Len or Num_Labels = 0 then
if Num_Labels = Max_Labels then
return;
end if;
Num_Labels := Num_Labels + 1;
Labels (Num_Labels) :=
(Start_Idx => Label_Start,
End_Idx => (if Label_Start <= CP_Len
then CP_Len else Label_Start - 1));
end if;
end Split_Labels_Pre_Map;
procedure Extract_Label_CPs
(NFC_CPs : CP_Work_Array;
Start_I : Positive;
End_I : Natural;
Label_CPs : out CP_Work_Array;
Label_Len : out CP_Work_Length;
Is_ASCII : out Boolean;
Status : out IDNA_Result)
with Post => (if Is_ASCII then
(for all I in 1 .. Label_Len => Label_CPs (I) < 128))
is
begin
Label_CPs := [others => 0];
Label_Len := 0;
Is_ASCII := True;
Status := Success;
if End_I >= Start_I and then End_I <= Max_Work_CPs then
for I in Start_I .. End_I loop
pragma Loop_Invariant (Label_Len <= Max_Label_CPs);
pragma Loop_Invariant (I <= Max_Work_CPs);
pragma Loop_Invariant
(if Is_ASCII then
(for all J in 1 .. Label_Len => Label_CPs (J) < 128));
if Label_Len = Max_Label_CPs then
Status := Label_Too_Long;
return;
end if;
Label_Len := Label_Len + 1;
Label_CPs (Label_Len) := NFC_CPs (I);
if NFC_CPs (I) >= 128 then
Is_ASCII := False;
end if;
end loop;
end if;
end Extract_Label_CPs;
function Is_ACE_Label
(CPs : CP_Work_Array;
Len : CP_Work_Length) return Boolean
is
begin
return Len >= 4
and then (CPs (1) = 16#78# or CPs (1) = 16#58#) -- x/X
and then (CPs (2) = 16#6E# or CPs (2) = 16#4E#) -- n/N
and then CPs (3) = Hyphen_CP
and then CPs (4) = Hyphen_CP;
end Is_ACE_Label;
---------------------------------------------------------------------------
-- To_ASCII
---------------------------------------------------------------------------
procedure To_ASCII
(Input : Byte_Array;
Options : IDNA_Options;
Output : in out Byte_Array;
Last : out Natural;
Status : out IDNA_Result)
is
CPs : CP_Work_Array;
CP_Len : CP_Work_Length;
Mapped : CP_Work_Array;
Map_Len : CP_Work_Length;
NFC_CPs : CP_Work_Array;
NFC_Len : CP_Work_Length;
Labels : Label_Array;
Num_Labels : Label_Count;
-- Original (pre-mapping) labels for P4 round-trip check
Orig_Labels : Label_Array;
Orig_Num_Labels : Label_Count;
Trailing_Dot : Boolean;
Out_Pos : Natural;
Step_Status : IDNA_Result;
begin
Last := Output'First - 1;
-- Step 1: Decode UTF-8 to codepoints
Decode_UTF8_To_CPs (Input, CPs, CP_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Split original (pre-mapping) CPs for P4 round-trip check.
-- Uses dots AND dot variants since mapping hasn't happened yet.
Split_Labels_Pre_Map (CPs, CP_Len, Orig_Labels, Orig_Num_Labels);
-- Step 2: Apply IDNA mapping
Apply_Mapping (CPs, CP_Len, Mapped, Map_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 3: NFC normalize
Normalize_NFC (Mapped, Map_Len, NFC_CPs, NFC_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 4: Split into labels
Split_Labels (NFC_CPs, NFC_Len, Labels, Num_Labels,
Trailing_Dot, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 4b: Determine if domain is Bidi (checks all labels including
-- decoded ACE labels for BC in {R, AL, AN})
declare
Bidi_Domain : constant Boolean :=
Domain_Is_Bidi_Check (NFC_CPs, NFC_Len, Labels, Num_Labels);
begin
-- Step 5: Process each label
Out_Pos := Output'First;
for L in 1 .. Num_Labels loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
pragma Loop_Invariant
(for all J in Output'First .. Out_Pos - 1 => Output (J) < 128);
declare
Label_CPs : CP_Work_Array;
Label_Len : CP_Work_Length;
Is_ASCII : Boolean;
Label_Status : IDNA_Result;
Puny_Out : Byte_Array (1 .. Max_Label_Length);
Puny_Len : Natural;
Puny_OK : Boolean;
Ext_Status : IDNA_Result;
-- Check if original (pre-mapping) label was already ACE
Orig_Is_ACE : Boolean := False;
begin
Extract_Label_CPs
(NFC_CPs, Labels (L).Start_Idx, Labels (L).End_Idx,
Label_CPs, Label_Len, Is_ASCII, Ext_Status);
if Ext_Status /= Success then
Status := Ext_Status;
return;
end if;
-- Check if the ORIGINAL label was ACE (before mapping).
-- Only original ACE labels get V1/P4 checks.
if L <= Orig_Num_Labels then
declare
OS : constant Natural := Orig_Labels (L).Start_Idx;
OE : constant Natural := Orig_Labels (L).End_Idx;
OLen : constant Natural :=
(if OE >= OS then OE - OS + 1 else 0);
begin
Orig_Is_ACE := OLen >= 4
and then OS + 3 <= Max_Work_CPs
and then OE <= Max_Work_CPs
and then (CPs (OS) = 16#78# or CPs (OS) = 16#58#)
and then (CPs (OS + 1) = 16#6E#
or CPs (OS + 1) = 16#4E#)
and then CPs (OS + 2) = Hyphen_CP
and then CPs (OS + 3) = Hyphen_CP;
end;
end if;
if Is_ACE_Label (Label_CPs, Label_Len) then
-- ACE label (xn--...): decode Punycode, validate decoded form,
-- then output the original ACE form.
declare
Puny_In_Len : constant Natural :=
(if Label_Len >= 4 then Label_Len - 4 else 0);
Puny_In : Byte_Array (1 .. Natural'Max (Puny_In_Len, 1))
:= [others => 0];
Decoded : CP_Work_Array;
Dec_Len : CP_Work_Length;
Dec_Valid : Boolean;
begin
for I in 5 .. Label_Len loop
if Label_CPs (I) > 255 then
Status := Punycode_Failure;
return;
end if;
Puny_In (I - 4) := Label_CPs (I);
end loop;
Punycode_Decode
(Puny_In (1 .. Puny_In_Len), Decoded, Dec_Len, Puny_OK);
if not Puny_OK then
Status := Punycode_Failure;
return;
end if;
-- UTS #46 §4 Step 4.3: decoded label must be non-empty
-- and must contain at least one non-ASCII code point.
if Orig_Is_ACE then
declare
Has_Non_ASCII : Boolean := False;
begin
for I in 1 .. Dec_Len loop
if Decoded (I) >= 128 then
Has_Non_ASCII := True;
exit;
end if;
end loop;
if Dec_Len = 0 or not Has_Non_ASCII then
Status := Punycode_Failure;
Last := Output'First - 1;
return;
end if;
end;
end if;
-- V1: Decoded form must be in NFC (only for original ACE)
if Orig_Is_ACE and then not Is_NFC (Decoded, Dec_Len) then
Status := NFC_Failure;
Last := Output'First - 1;
return;
end if;
-- P4: Round-trip check using ORIGINAL (pre-mapping) Punycode.
-- Only applies to labels that were ACE before mapping.
if Orig_Is_ACE and then L <= Orig_Num_Labels then
declare
OS : constant Natural := Orig_Labels (L).Start_Idx;
OE : constant Natural := Orig_Labels (L).End_Idx;
Orig_Puny_Len : constant Natural :=
(if OE >= OS + 4 then OE - OS - 3 else 0);
Orig_Puny_In : Byte_Array
(1 .. Natural'Max (Orig_Puny_Len, 1))
:= [others => 0];
begin
for I in OS + 4 .. OE loop
if I - OS - 3 <= Orig_Puny_In'Last
and then CPs (I) <= 255
then
Orig_Puny_In (I - OS - 3) := CPs (I);
end if;
end loop;
if Orig_Puny_Len > 0 and then
not Punycode_Round_Trip_OK
(Orig_Puny_In (1 .. Orig_Puny_Len),
Decoded, Dec_Len)
then
Status := Punycode_Failure;
Last := Output'First - 1;
return;
end if;
end;
end if;
-- Validate decoded form
Validate_Label
(Decoded, Dec_Len, Options, Bidi_Domain,
Label_Status, Dec_Valid);
if not Dec_Valid then
Status := Label_Status;
return;
end if;
-- Output original ACE label bytes
if Label_Len > Max_Label_Length then
Status := Label_Too_Long;
return;
end if;
if Out_Pos > Output'Last
or else Label_Len > Output'Last - Out_Pos + 1
then
Status := Buffer_Overflow;
return;
end if;
for I in 1 .. Label_Len loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last);
pragma Loop_Invariant
(Label_Len - I + 1 <= Output'Last - Out_Pos + 1);
pragma Loop_Invariant
(for all J in Output'First .. Out_Pos - 1 =>
Output (J) < 128);
-- ACE labels are defined as "xn--" followed by
-- Punycode-encoded ASCII characters. Any byte >= 128
-- here is a malformed ACE label.
if Label_CPs (I) >= 128 then
Status := Invalid_Input;
return;
end if;
Output (Out_Pos) := Label_CPs (I);
Out_Pos := Out_Pos + 1;
end loop;
end;
else
-- Non-ACE label: validate, then Punycode encode if non-ASCII
declare
Label_Valid : Boolean;
begin
Validate_Label
(Label_CPs, Label_Len, Options, Bidi_Domain,
Label_Status, Label_Valid);
if not Label_Valid then
Status := Label_Status;
return;
end if;
end;
if not Is_ASCII then
-- Punycode encode
Punycode_Encode (Label_CPs, Label_Len, Puny_Out, Puny_Len,
Puny_OK);
if not Puny_OK then
Status := Punycode_Failure;
return;
end if;
-- Check label length (xn-- prefix + punycode)
if Puny_Len > Max_Label_Length - 4 then
Status := Label_Too_Long;
return;
end if;
-- Check output buffer space: need 4 + Puny_Len bytes
if Out_Pos > Output'Last
or else 4 > Output'Last - Out_Pos + 1
or else Puny_Len > Output'Last - Out_Pos + 1 - 4
then
Status := Buffer_Overflow;
return;
end if;
Output (Out_Pos) := 16#78#; -- 'x'
Output (Out_Pos + 1) := 16#6E#; -- 'n'
Output (Out_Pos + 2) := 16#2D#; -- '-'
Output (Out_Pos + 3) := 16#2D#; -- '-'
Out_Pos := Out_Pos + 4;
-- Punycode_Encode's Post guarantees every byte of its
-- output range is < 128 on success.
pragma Assert
(for all K in 1 .. Puny_Len => Puny_Out (K) < 128);
for I in 1 .. Puny_Len loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last);
pragma Loop_Invariant
(Puny_Len - I + 1 <= Output'Last - Out_Pos + 1);
pragma Loop_Invariant
(for all J in Output'First .. Out_Pos - 1 =>
Output (J) < 128);
Output (Out_Pos) := Puny_Out (I);
Out_Pos := Out_Pos + 1;
end loop;
else
-- ASCII label: just copy
if Label_Len > Max_Label_Length then
Status := Label_Too_Long;
return;
end if;
if Out_Pos > Output'Last
or else Label_Len > Output'Last - Out_Pos + 1
then
Status := Buffer_Overflow;
return;
end if;
-- ASCII branch: Extract_Label_CPs' postcondition gives us
-- that all Label_CPs (1 .. Label_Len) are < 128 when
-- Is_ASCII holds.
for I in 1 .. Label_Len loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last);
pragma Loop_Invariant
(Label_Len - I + 1 <= Output'Last - Out_Pos + 1);
pragma Loop_Invariant
(for all J in Output'First .. Out_Pos - 1 =>
Output (J) < 128);
if Label_CPs (I) > 255 then
Status := Invalid_Input;
return;
end if;
Output (Out_Pos) := Label_CPs (I);
Out_Pos := Out_Pos + 1;
end loop;
end if;
end if;
-- Add dot separator (except after last label)
if L < Num_Labels then
if Out_Pos > Output'Last then
Status := Buffer_Overflow;
return;
end if;
Output (Out_Pos) := Dot_Byte;
Out_Pos := Out_Pos + 1;
end if;
end;
end loop;
end; -- Bidi_Domain declare block
-- Add trailing dot if present in input
if Trailing_Dot then
if Out_Pos > Output'Last then
Status := Buffer_Overflow;
return;
end if;
Output (Out_Pos) := Dot_Byte;
Out_Pos := Out_Pos + 1;
end if;
-- Verify DNS length limits (UTS #46 Section 4.2 Step 4)
if Options.Verify_DNS_Length then
-- Trailing dot = empty root label, which is disallowed
if Trailing_Dot then
Status := Domain_Too_Long;
Last := Output'First - 1;
return;
end if;
if Out_Pos < Output'First then
Status := Buffer_Overflow;
Last := Output'First - 1;
return;
end if;
declare
Total_Len : constant Natural := Out_Pos - Output'First;
-- Check individual label lengths (1..63 bytes each)
Label_Start_Pos : Natural := Output'First;
begin
-- Domain total must be 1..253
if Total_Len = 0 or Total_Len > Max_Domain_Length then
Status := Domain_Too_Long;
Last := Output'First - 1;
return;
end if;
-- Total_Len >= 1 means Out_Pos >= Output'First + 1
pragma Assert (Out_Pos >= Output'First + 1);
-- Check each label is 1..63 bytes
for I in Output'First .. Out_Pos - 1 loop
pragma Loop_Invariant (Label_Start_Pos >= Output'First);
pragma Loop_Invariant (Label_Start_Pos <= I);
if Output (I) = Dot_Byte then
declare
Lbl_Len : constant Natural := I - Label_Start_Pos;
begin
if Lbl_Len = 0 or Lbl_Len > Max_Label_Length then
Status := Label_Too_Long;
Last := Output'First - 1;
return;
end if;
end;
Label_Start_Pos := I + 1;
end if;
end loop;
-- Check last label (after final dot or if no dots)
pragma Assert (Label_Start_Pos <= Out_Pos);
declare
Last_Lbl_Len : constant Natural := Out_Pos - Label_Start_Pos;
begin
if Last_Lbl_Len = 0 or Last_Lbl_Len > Max_Label_Length then
Status := Label_Too_Long;
Last := Output'First - 1;
return;
end if;
end;
-- Platinum: DNS length verified — connect to postcondition
pragma Assert (Out_Pos - Output'First >= 1);
pragma Assert (Out_Pos - Output'First <= Max_Domain_Length);
end;
end if;
if Out_Pos > Output'First
and then Out_Pos <= Output'Last + 1
then
Last := Out_Pos - 1;
-- Platinum: when Verify_DNS_Length, connect Total_Len to Last
pragma Assert
(if Options.Verify_DNS_Length then
Last - Output'First + 1 >= 1
and then Last - Output'First + 1 <= Max_Domain_Length);
Status := Success;
else
Last := Output'First - 1;
Status := Buffer_Overflow;
end if;
end To_ASCII;
---------------------------------------------------------------------------
-- To_Unicode
---------------------------------------------------------------------------
procedure To_Unicode
(Input : Byte_Array;
Options : IDNA_Options;
Output : in out Byte_Array;
Last : out Natural;
Status : out IDNA_Result)
is
CPs : CP_Work_Array;
CP_Len : CP_Work_Length;
Mapped : CP_Work_Array;
Map_Len : CP_Work_Length;
NFC_CPs : CP_Work_Array;
NFC_Len : CP_Work_Length;
Labels : Label_Array;
Num_Labels : Label_Count;
-- Original (pre-mapping) labels for P4 round-trip check
Orig_Labels : Label_Array;
Orig_Num_Labels : Label_Count;
Trailing_Dot : Boolean;
Out_Pos : Natural;
Enc_Len : Positive;
Step_Status : IDNA_Result;
begin
Last := Output'First - 1;
-- Step 1: Decode UTF-8 to codepoints
Decode_UTF8_To_CPs (Input, CPs, CP_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Split original (pre-mapping) CPs for P4 round-trip check.
Split_Labels_Pre_Map (CPs, CP_Len, Orig_Labels, Orig_Num_Labels);
-- Step 2: Apply IDNA mapping
Apply_Mapping (CPs, CP_Len, Mapped, Map_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 3: NFC normalize
Normalize_NFC (Mapped, Map_Len, NFC_CPs, NFC_Len, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 4: Split into labels
Split_Labels (NFC_CPs, NFC_Len, Labels, Num_Labels,
Trailing_Dot, Step_Status);
if Step_Status /= Success then
Status := Step_Status;
return;
end if;
-- Step 4b: Determine if domain is Bidi (checks all labels including
-- decoded ACE labels for BC in {R, AL, AN})
declare
Bidi_Domain : constant Boolean :=
Domain_Is_Bidi_Check (NFC_CPs, NFC_Len, Labels, Num_Labels);
begin
-- Step 5: Process each label
Out_Pos := Output'First;
for L in 1 .. Num_Labels loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
declare
Label_CPs : CP_Work_Array;
Label_Len : CP_Work_Length;
Unused_Is_ASCII : Boolean;
Label_Status : IDNA_Result;
Ext_Status : IDNA_Result;
-- Check if original (pre-mapping) label was already ACE
Orig_Is_ACE : Boolean := False;
begin
Extract_Label_CPs
(NFC_CPs, Labels (L).Start_Idx, Labels (L).End_Idx,
Label_CPs, Label_Len, Unused_Is_ASCII, Ext_Status);
if Ext_Status /= Success then
Status := Ext_Status;
return;
end if;
-- Check if the ORIGINAL label was ACE (before mapping)
if L <= Orig_Num_Labels then
declare
OS : constant Natural := Orig_Labels (L).Start_Idx;
OE : constant Natural := Orig_Labels (L).End_Idx;
OLen : constant Natural :=
(if OE >= OS then OE - OS + 1 else 0);
begin
Orig_Is_ACE := OLen >= 4
and then OS + 3 <= Max_Work_CPs
and then OE <= Max_Work_CPs
and then (CPs (OS) = 16#78# or CPs (OS) = 16#58#)
and then (CPs (OS + 1) = 16#6E#
or CPs (OS + 1) = 16#4E#)
and then CPs (OS + 2) = Hyphen_CP
and then CPs (OS + 3) = Hyphen_CP;
end;
end if;
if Is_ACE_Label (Label_CPs, Label_Len) then
-- Decode Punycode (skip "xn--" prefix)
declare
Puny_In_Len : constant Natural :=
(if Label_Len >= 4 then Label_Len - 4 else 0);
Puny_In : Byte_Array (1 .. Natural'Max (Puny_In_Len, 1))
:= [others => 0];
Decoded : CP_Work_Array;
Dec_Len : CP_Work_Length;
Puny_OK : Boolean;
begin
for I in 5 .. Label_Len loop
if Label_CPs (I) > 255 then
Status := Punycode_Failure;
return;
end if;
Puny_In (I - 4) := Label_CPs (I);
end loop;
Punycode_Decode
(Puny_In (1 .. Puny_In_Len), Decoded, Dec_Len, Puny_OK);
if not Puny_OK then
Status := Punycode_Failure;
return;
end if;
-- UTS #46 §4 Step 4.3: decoded label must be non-empty
-- and must contain at least one non-ASCII code point.
if Orig_Is_ACE then
declare
Has_Non_ASCII : Boolean := False;
begin
for I in 1 .. Dec_Len loop
if Decoded (I) >= 128 then
Has_Non_ASCII := True;
exit;
end if;
end loop;
if Dec_Len = 0 or not Has_Non_ASCII then
Status := Punycode_Failure;
Last := Output'First - 1;
return;
end if;
end;
end if;
-- V1: Decoded form must be in NFC (only for original ACE)
if Orig_Is_ACE and then not Is_NFC (Decoded, Dec_Len) then
Status := NFC_Failure;
Last := Output'First - 1;
return;
end if;
-- P4: Round-trip check using ORIGINAL (pre-mapping) Punycode.
-- Only applies to labels that were ACE before mapping.
if Orig_Is_ACE and then L <= Orig_Num_Labels then
declare
OS : constant Natural := Orig_Labels (L).Start_Idx;
OE : constant Natural := Orig_Labels (L).End_Idx;
Orig_Puny_Len : constant Natural :=
(if OE >= OS + 4 then OE - OS - 3 else 0);
Orig_Puny_In : Byte_Array
(1 .. Natural'Max (Orig_Puny_Len, 1))
:= [others => 0];
begin
for I in OS + 4 .. OE loop
if I - OS - 3 <= Orig_Puny_In'Last
and then CPs (I) <= 255
then
Orig_Puny_In (I - OS - 3) := CPs (I);
end if;
end loop;
if Orig_Puny_Len > 0 and then
not Punycode_Round_Trip_OK
(Orig_Puny_In (1 .. Orig_Puny_Len),
Decoded, Dec_Len)
then
Status := Punycode_Failure;
Last := Output'First - 1;
return;
end if;
end;
end if;
-- Validate decoded label
declare
Dec_Valid : Boolean;
begin
Validate_Label
(Decoded, Dec_Len, Options, Bidi_Domain,
Label_Status, Dec_Valid);
if not Dec_Valid then
Status := Label_Status;
return;
end if;
end;
-- Output decoded Unicode as UTF-8
for I in 1 .. Dec_Len loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
if not Is_Scalar_Value (Decoded (I)) then
Status := Invalid_Input;
return;
end if;
declare
Needed : constant Positive :=
(if Decoded (I) <= 16#7F# then 1
elsif Decoded (I) <= 16#7FF# then 2
elsif Decoded (I) <= 16#FFFF# then 3
else 4);
begin
if Out_Pos > Output'Last
or else Needed > Output'Last - Out_Pos + 1
then
Status := Buffer_Overflow;
return;
end if;
UTF8.Encode (Decoded (I), Output, Out_Pos, Enc_Len);
Out_Pos := Out_Pos + Enc_Len;
end;
end loop;
end;
else
-- Non-ACE label: validate and output as UTF-8
declare
Lbl_Valid : Boolean;
begin
Validate_Label
(Label_CPs, Label_Len, Options, Bidi_Domain,
Label_Status, Lbl_Valid);
if not Lbl_Valid then
Status := Label_Status;
return;
end if;
end;
for I in 1 .. Label_Len loop
pragma Loop_Invariant (Out_Pos >= Output'First);
pragma Loop_Invariant (Out_Pos <= Output'Last + 1);
if not Is_Scalar_Value (Label_CPs (I)) then
Status := Invalid_Input;
return;
end if;
declare
Needed : constant Positive :=
(if Label_CPs (I) <= 16#7F# then 1
elsif Label_CPs (I) <= 16#7FF# then 2
elsif Label_CPs (I) <= 16#FFFF# then 3
else 4);
begin
if Out_Pos > Output'Last
or else Needed > Output'Last - Out_Pos + 1
then
Status := Buffer_Overflow;
return;
end if;
UTF8.Encode (Label_CPs (I), Output, Out_Pos, Enc_Len);
Out_Pos := Out_Pos + Enc_Len;
end;
end loop;
end if;
-- Add dot separator (except after last label)
if L < Num_Labels then
if Out_Pos > Output'Last then
Status := Buffer_Overflow;
return;
end if;
Output (Out_Pos) := Dot_Byte;
Out_Pos := Out_Pos + 1;
end if;
end;
end loop;
end; -- Bidi_Domain declare block
-- Add trailing dot if present in input
if Trailing_Dot then
if Out_Pos > Output'Last then
Status := Buffer_Overflow;
return;
end if;
Output (Out_Pos) := Dot_Byte;
Out_Pos := Out_Pos + 1;
end if;
if Out_Pos > Output'First
and then Out_Pos <= Output'Last + 1
then
Last := Out_Pos - 1;
Status := Success;
else
Last := Output'First - 1;
Status := Buffer_Overflow;
end if;
end To_Unicode;
end Lingenic_Text.IDNA;