-- 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 ghost specification (UTS #46).
--
-- Expression functions encoding UTS #46 validity criteria, RFC 5892
-- ContextJ rules, RFC 5893 Bidi domain rules, and RFC 3492 Punycode
-- parameters. The solver unfolds these during proof.
-------------------------------------------------------------------------------
with Lingenic_Text.Properties_Spec;
package Lingenic_Text.IDNA_Spec
with SPARK_Mode, Pure
is
---------------------------------------------------------------------------
-- IDNA mapping status values (IdnaMappingTable.txt)
---------------------------------------------------------------------------
ST_Valid : constant := 0;
ST_Ignored : constant := 1;
ST_Mapped : constant := 2;
ST_Deviation : constant := 3;
ST_Disallowed : constant := 4;
subtype Status_Value is Natural range 0 .. 4;
---------------------------------------------------------------------------
-- Punycode parameters (RFC 3492 Section 5)
---------------------------------------------------------------------------
Puny_Base : constant := 36;
Puny_Tmin : constant := 1;
Puny_Tmax : constant := 26;
Puny_Skew : constant := 38;
Puny_Damp : constant := 700;
Puny_Initial_Bias : constant := 72;
Puny_Initial_N : constant := 128;
Puny_Delimiter : constant := 16#2D#; -- hyphen-minus
---------------------------------------------------------------------------
-- DNS length limits
---------------------------------------------------------------------------
Max_Domain_Length : constant := 253; -- excluding root label
Max_Label_Length : constant := 63;
---------------------------------------------------------------------------
-- Processing limits
---------------------------------------------------------------------------
Max_Domain_CPs : constant := 1024; -- generous limit on input CPs
Max_Label_CPs : constant := 256; -- per label before Punycode
Max_Labels : constant := 128; -- per domain
Max_Mapping_CPs : constant := 18; -- max CPs in a single mapping
---------------------------------------------------------------------------
-- IDNA options (input flags, UTS #46 Section 4)
---------------------------------------------------------------------------
type IDNA_Options is record
Check_Hyphens : Boolean;
Check_Bidi : Boolean;
Check_Joiners : Boolean;
Use_STD3_Rules : Boolean;
Verify_DNS_Length : Boolean;
end record;
Default_Options : constant IDNA_Options :=
(Check_Hyphens => True,
Check_Bidi => True,
Check_Joiners => True,
Use_STD3_Rules => True,
Verify_DNS_Length => True);
---------------------------------------------------------------------------
-- Virama detection: CCC = 9
---------------------------------------------------------------------------
Virama_CCC : constant := 9;
---------------------------------------------------------------------------
-- ContextJ predicates (RFC 5892 Appendix A)
---------------------------------------------------------------------------
-- ZWJ (U+200D): valid only after Virama (CCC=9)
function ZWJ_Valid_After_Virama (Prev_CCC : Natural) return Boolean
is (Prev_CCC = Virama_CCC);
-- ZWNJ (U+200C) Context A: valid after Virama
function ZWNJ_Valid_After_Virama (Prev_CCC : Natural) return Boolean
is (Prev_CCC = Virama_CCC);
-- ZWNJ (U+200C) Context B: joining context helpers
-- Pattern: (JT:{L,D})(JT:T)* ZWNJ (JT:T)*(JT:{R,D})
function Is_Left_Or_Dual (JT : Properties_Spec.JT_Value) return Boolean
is (JT = Properties_Spec.JT_L or JT = Properties_Spec.JT_D);
function Is_Right_Or_Dual (JT : Properties_Spec.JT_Value) return Boolean
is (JT = Properties_Spec.JT_R or JT = Properties_Spec.JT_D);
function Is_Transparent (JT : Properties_Spec.JT_Value) return Boolean
is (JT = Properties_Spec.JT_T);
---------------------------------------------------------------------------
-- Bidi domain predicates (RFC 5893 Section 2)
--
-- BC values reference Bidi_Spec constants:
-- BC_L=1, BC_R=2, BC_AL=3, BC_EN=4, BC_ES=5, BC_ET=6, BC_AN=7,
-- BC_CS=8, BC_NSM=9, BC_BN=10, BC_B=11, BC_S=12, BC_WS=13, BC_ON=14
---------------------------------------------------------------------------
-- Condition 1: First character must be L, R, or AL
function Bidi_Rule1_Valid (First_BC : Natural) return Boolean
is (First_BC = 1 or First_BC = 2 or First_BC = 3);
-- RTL label: first char is R or AL
function Is_RTL_Label (First_BC : Natural) return Boolean
is (First_BC = 2 or First_BC = 3);
-- Condition 2: RTL label allowed types: R, AL, AN, EN, ES, CS, ET, ON,
-- BN, NSM
function RTL_Allowed (BC : Natural) return Boolean
is (BC = 2 or BC = 3 or BC = 7 or BC = 4
or BC = 5 or BC = 8 or BC = 6 or BC = 14
or BC = 10 or BC = 9);
-- Condition 3: RTL label end type (before trailing NSMs): R, AL, EN, AN
function RTL_End_Valid (BC : Natural) return Boolean
is (BC = 2 or BC = 3 or BC = 4 or BC = 7);
-- Condition 5: LTR label allowed types: L, EN, ES, CS, ET, ON, BN, NSM
function LTR_Allowed (BC : Natural) return Boolean
is (BC = 1 or BC = 4
or BC = 5 or BC = 8
or BC = 6 or BC = 14
or BC = 10 or BC = 9);
-- Condition 6: LTR label end type (before trailing NSMs): L, EN
function LTR_End_Valid (BC : Natural) return Boolean
is (BC = 1 or BC = 4);
---------------------------------------------------------------------------
-- Validity predicates (UTS #46 Section 4.1)
---------------------------------------------------------------------------
-- Criterion 7 (nontransitional): each CP must be valid or deviation
function Status_Valid_Nontransitional (S : Status_Value) return Boolean
is (S = ST_Valid or S = ST_Deviation);
-- STD3 ASCII check (Criterion 7 addendum): if UseSTD3 and CP is ASCII,
-- must be a-z, 0-9, or hyphen-minus
function STD3_ASCII_Valid (CP : Natural) return Boolean
is (CP in 16#61# .. 16#7A#
or CP in 16#30# .. 16#39#
or CP = 16#2D#);
---------------------------------------------------------------------------
-- DNS structural validity ghost predicates
---------------------------------------------------------------------------
-- All bytes in Buf(First..Last) are ASCII (< 128)
function Ghost_All_ASCII
(Buf : Lingenic_Text.Byte_Array;
First : Positive;
Last : Natural) return Boolean
is (for all I in First .. Last => Buf (I) < 128)
with Ghost,
Pre => (if First <= Last then
First in Buf'Range and Last in Buf'Range);
---------------------------------------------------------------------------
-- Punycode bias adaptation (RFC 3492 Section 6.1)
--
-- Ghost encoding for proof reference. The implementation uses the same
-- formulas; postconditions reference this function.
---------------------------------------------------------------------------
function Adapt_Ghost
(Delta_Val : Natural;
Num_Points : Positive;
First_Time : Boolean) return Natural
is (declare
D1 : constant Natural :=
(if First_Time then Delta_Val / Puny_Damp
else Delta_Val / 2);
D2 : constant Natural := D1 + D1 / Num_Points;
begin
-- The loop in adapt counts iterations; we express the result
-- without unrolling. The prover uses this for type bounds only.
D2)
with Pre => Num_Points >= 1;
end Lingenic_Text.IDNA_Spec;