IDNA MODULE
===========
Standard: UTS #46 (Unicode IDNA Compatibility Processing)
RFC 3492 (Punycode), RFC 5892 (IDNA), RFC 5893 (Bidi for IDNA)
Files: src/lingenic_text-idna_spec.ads (ghost specification)
src/lingenic_text-idna.ads (public API)
src/lingenic_text-idna.adb (implementation)
PURPOSE
-------
The IDNA module converts domain names between Unicode and ASCII-
Compatible Encoding (ACE) per UTS #46 with nontransitional handling.
This is the standard for Internationalized Domain Names in Applications.
GHOST SPECIFICATION (IDNA_Spec)
-------------------------------
IDNA Status Values:
type Status_Value is
(ST_Valid, ST_Ignored, ST_Mapped, ST_Deviation, ST_Disallowed);
ST_Valid Codepoint passes through unchanged
ST_Ignored Codepoint is removed during mapping
ST_Mapped Codepoint is replaced by a mapping sequence
ST_Deviation Treated as Valid in nontransitional processing
ST_Disallowed Codepoint is not permitted
Punycode Parameters (RFC 3492, Section 5):
Base = 36
Tmin = 1
Tmax = 26
Skew = 38
Damp = 700
Initial_Bias = 72
Initial_N = 128
Delimiter = 16#2D# (hyphen-minus)
DNS Length Limits:
Max_Domain_Length = 253 Maximum ASCII domain name length
Max_Label_Length = 63 Maximum ASCII label length
Processing Limits:
Max_Domain_CPs = 1024 Maximum codepoints in mapped domain
Max_Label_CPs = 256 Maximum codepoints per label
Max_Labels = 128 Maximum labels per domain
Max_Mapping_CPs = 18 Maximum codepoints in a mapping sequence
IDNA Options:
type IDNA_Options is record
Check_Hyphens : Boolean;
Check_Bidi : Boolean;
Check_Joiners : Boolean;
Use_STD3_Rules : Boolean;
Verify_DNS_Length : Boolean;
end record;
ContextJ Predicates (RFC 5892, Appendix A):
ZWJ_Valid_After_Virama(Prev_CCC)
ZWJ (U+200D) is valid in IDNA only after a character with CCC = Virama
(CCC value 9).
ZWNJ_Valid_After_Virama(Prev_CCC)
ZWNJ (U+200C) same rule.
Is_Left_Or_Dual(JT)
True if Joining_Type is Left_Joining or Dual_Joining.
Used for additional ZWNJ context rules.
INITIALIZATION
--------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean);
Post: if Success then Initialized
Reads from UCD_Dir:
IdnaMappingTable.txt IDNA status and mapping data per codepoint
Builds internal data tables:
Status_Table IDNA status per codepoint (Valid/Ignored/Mapped/etc.)
Map_Index Mapping offset per codepoint (for Mapped/Deviation)
Map_Data Packed mapping sequences (codepoint sequences)
DEPENDENCIES
------------
The IDNA module requires:
Properties.Initialized For Bidi_Class, Joining_Type, General_Category
Normalization.Initialized For NFC normalization
Normalization.Data_All_Terminal For normalization correctness
All three must be established before calling To_ASCII or To_Unicode.
PUBLIC API
----------
Result Type:
type IDNA_Result is
(Success,
Invalid_Input,
Disallowed_Codepoint,
Label_Too_Long,
Domain_Too_Long,
Invalid_Hyphen,
Leading_Combining_Mark,
NFC_Failure,
Bidi_Failure,
ContextJ_Failure,
Punycode_Failure,
Buffer_Overflow,
STD3_Failure,
Too_Many_Labels,
Empty_Label);
To_ASCII:
procedure To_ASCII
(Input : Byte_Array;
Options : IDNA_Options;
Output : in out Byte_Array;
Last : out Natural;
Status : out IDNA_Result);
Pre: Initialized, Properties.Initialized,
Normalization.Initialized, Normalization.Data_All_Terminal
Input'Length >= 1, Output'Length >= 1
Post: if Success then
Last in Output'First..Output'Last
All output bytes < 128 (ASCII)
if Verify_DNS_Length then
output length in 1..253
else
Last = Output'First - 1
Converts a Unicode domain name to ASCII-Compatible Encoding.
Processing Steps (UTS #46, Section 4):
1. MAP
Apply the IDNA mapping table to each codepoint:
- Valid/Deviation: keep as-is
- Ignored: remove
- Mapped: replace with mapping sequence
- Disallowed: fail with Disallowed_Codepoint
2. NORMALIZE
Apply NFC normalization to the mapped string.
3. BREAK
Split the normalized string at U+002E (FULL STOP) into labels.
4. CONVERT
For each label:
a. Check if the label is already ASCII (all bytes < 128)
b. If not, encode the label using Punycode (RFC 3492)
and prepend "xn--"
5. VALIDATE
Apply validity criteria (UTS #46, Section 4.1):
V1: NFC-normalized (guaranteed by step 2)
V2: No U+002D (hyphen) at positions 3-4 (unless "xn--" prefix)
V3: No leading or trailing U+002D
V4: No disallowed codepoints
V5: No leading combining mark (General_Category = Mn or Mc)
V6: Check_Joiners: ZWNJ/ZWJ must satisfy ContextJ rules
V7: Check_Bidi: labels must satisfy RFC 5893 Bidi rules
V8: Each label <= 63 bytes (if Verify_DNS_Length)
V9: Total domain <= 253 bytes (if Verify_DNS_Length)
Bidi Rules (RFC 5893, Section 2):
Rule 1: First character must be L, R, AL, EN, or AN
Rule 2: R/AL label: no L characters
Rule 3: R/AL label: ends with R, AL, EN, or AN
Rule 4: EN and AN cannot both appear in same label
Rule 5: L label: no R, AL characters
Rule 6: L label: ends with L or EN
ContextJ Rules (RFC 5892, Appendix A):
ZWNJ: valid after Virama (CCC=9) or between Left/Dual-joining characters
ZWJ: valid after Virama (CCC=9)
To_Unicode:
procedure To_Unicode
(Input : Byte_Array;
Options : IDNA_Options;
Output : in out Byte_Array;
Last : out Natural;
Status : out IDNA_Result);
Pre: same as To_ASCII
Post: if Success then
Last in Output'First..Output'Last
else
Last = Output'First - 1
Converts a domain name to Unicode.
Input may be ASCII (ACE) or UTF-8. Output is UTF-8.
Processing Steps:
1. Map (same as To_ASCII)
2. Normalize (NFC)
3. Break into labels
4. For each label: if it has "xn--" prefix, Punycode-decode it
5. Validate (same criteria as To_ASCII)
PUNYCODE (RFC 3492)
-------------------
The IDNA module includes a complete Punycode encoder and decoder
implemented in SPARK.
Punycode encodes Unicode strings as ASCII using a generalized variable-
length integer encoding with bias adaptation. The algorithm:
1. Copy all ASCII characters directly
2. For each non-ASCII codepoint in sorted order:
a. Encode the delta from the previous insertion point
b. Adapt the bias for the next encoding
The implementation handles:
- Bias adaptation (Adapt function from RFC 3492 Section 6.1)
- Variable-length integer encoding/decoding
- Overflow detection for all arithmetic
USAGE PATTERN
-------------
-- Convert Unicode domain to ASCII for DNS lookup
IDNA.To_ASCII
(Input => Domain_UTF8,
Options => (Check_Hyphens => True,
Check_Bidi => True,
Check_Joiners => True,
Use_STD3_Rules => True,
Verify_DNS_Length => True),
Output => ASCII_Buffer,
Last => ASCII_Last,
Status => Result);
if Result = IDNA.Success then
-- ASCII_Buffer(ASCII_Buffer'First .. ASCII_Last) is the ACE domain
-- Ready for DNS lookup
else
-- Handle error based on Result value
end if;