lingenic_text-idna

--  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
--
--  Internationalized Domain Names (UTS #46).
--
--  Implements IDNA compatibility processing with nontransitional handling:
--    To_ASCII   — convert a domain name to ASCII-Compatible Encoding (ACE)
--    To_Unicode — convert a domain name to Unicode
--
--  Self-contained module with its own Initialize.  Reads IdnaMappingTable.txt
--  at init time for IDNA status and mapping data.  Requires Properties
--  (for Bidi_Class, Joining_Type, General_Category) and Normalization
--  (for NFC, CCC) to be initialized first.
--
--  Processing steps (UTS #46 Section 4):
--    1. Map      — apply IDNA mapping table
--    2. Normalize — NFC normalization
--    3. Break    — split at U+002E (FULL STOP)
--    4. Convert/Validate — Punycode + validity criteria
--
--  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.
--
--  Data tables:
--    Status_Table  — IDNA status per codepoint
--    Map_Index     — mapping offset per codepoint
--    Map_Data      — packed mapping sequences
-------------------------------------------------------------------------------

with Lingenic_Text.IDNA_Spec;
with Lingenic_Text.Properties;
with Lingenic_Text.Normalization;

package Lingenic_Text.IDNA
   with SPARK_Mode,
        Abstract_State => IDNA_State,
        Initializes    => IDNA_State
is

   use IDNA_Spec;

   ---------------------------------------------------------------------------
   --  Initialization
   ---------------------------------------------------------------------------

   function Initialized return Boolean
     with Global => IDNA_State;

   procedure Initialize
     (UCD_Dir : String;
      Success : out Boolean)
   with Global => (Output => IDNA_State),
        Post   => (if Success then Initialized);

   ---------------------------------------------------------------------------
   --  Result status
   ---------------------------------------------------------------------------

   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
   --
   --  Convert a Unicode domain name to its ASCII-Compatible Encoding.
   --  Input is UTF-8.  Output is ASCII (with Punycode-encoded labels).
   --
   --  On success:
   --    Output(Output'First..Last) contains the ACE domain name
   --  On failure:
   --    Last = Output'First - 1
   ---------------------------------------------------------------------------

   procedure To_ASCII
     (Input   : Byte_Array;
      Options : IDNA_Options;
      Output  : in out Byte_Array;
      Last    : out Natural;
      Status  : out IDNA_Result)
   with Pre  => Initialized
                and then Properties.Initialized
                and then Normalization.Initialized
                and then Normalization.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,
        Post => (if Status = Success then
                    Last in Output'First .. Output'Last
                    and then (for all I in Output'First .. Last =>
                                Output (I) < 128)
                    --  Platinum: DNS length structural validity
                    and then (if Options.Verify_DNS_Length then
                                Last - Output'First + 1 >= 1
                                and then
                                Last - Output'First + 1 <= Max_Domain_Length)
                 else
                    Last = Output'First - 1),
        Global => (Input => (IDNA_State,
                             Properties.Property_State,
                             Normalization.Norm_State));

   ---------------------------------------------------------------------------
   --  To_Unicode
   --
   --  Convert a domain name to Unicode.
   --  Input may be ASCII (ACE) or UTF-8.  Output is UTF-8.
   --
   --  On success:
   --    Output(Output'First..Last) contains the Unicode domain name
   --  On failure:
   --    Last = Output'First - 1
   ---------------------------------------------------------------------------

   procedure To_Unicode
     (Input   : Byte_Array;
      Options : IDNA_Options;
      Output  : in out Byte_Array;
      Last    : out Natural;
      Status  : out IDNA_Result)
   with Pre  => Initialized
                and then Properties.Initialized
                and then Normalization.Initialized
                and then Normalization.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,
        Post => (if Status = Success then
                    Last in Output'First .. Output'Last
                 else
                    Last = Output'First - 1),
        Global => (Input => (IDNA_State,
                             Properties.Property_State,
                             Normalization.Norm_State));

end Lingenic_Text.IDNA;