-- 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
--
-- Unicode normalization (UAX #15).
--
-- Implements NFD, NFC, NFKD, NFKC via decomposition, canonical ordering,
-- and canonical composition. Quick Check and Is_Normalized queries.
--
-- Self-contained module with its own Initialize. Reads UnicodeData.txt
-- (CCC + decomposition mappings) and DerivedNormalizationProps.txt
-- (Quick Check properties + composition exclusions).
--
-- Data tables:
-- CCC_Table — flat array, codepoint → CCC (0..254)
-- Canon_Index/Data — pre-expanded canonical decompositions
-- Compat_Index/Data — pre-expanded compatibility decompositions
-- Comp_Index/Pairs — composition pairs (starter + combining → composite)
-- NFD/NFC/NFKD/NFKC_QC — Quick Check tables
--
-- Hangul syllable decomposition and composition are algorithmic
-- (not stored in tables).
-------------------------------------------------------------------------------
with Lingenic_Text.Normalization_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Normalization
with SPARK_Mode,
Abstract_State => Norm_State,
Initializes => Norm_State
is
use type Normalization_Spec.QC_Value;
---------------------------------------------------------------------------
-- Initialization
---------------------------------------------------------------------------
function Initialized return Boolean
with Global => Norm_State;
---------------------------------------------------------------------------
-- UCD data invariant: decomposition tables contain terminal entries.
--
-- All entries in Canon_Data (canonical) and Compat_Data (compatibility)
-- are fully expanded: they have no further decomposition (Ghost_Decomp_Len
-- returns 0) and are not Hangul syllables. True by construction —
-- Initialize runs Expand_Decompositions which iterates to fixed point.
--
-- Established by Initialize postcondition (trusted, body is SPARK_Mode
-- Off). Used by Flush_Segment to prove Ghost_Is_NFD_From / Ghost_Is_NFC_From.
---------------------------------------------------------------------------
function Data_All_Terminal return Boolean
with Ghost, Global => Norm_State;
procedure Initialize
(UCD_Dir : String;
Success : out Boolean)
with Global => (Output => Norm_State),
Post => (if Success then Initialized and then Data_All_Terminal);
---------------------------------------------------------------------------
-- Normalization status
---------------------------------------------------------------------------
type Norm_Status is (Success, Buffer_Overflow, Invalid_Input);
---------------------------------------------------------------------------
-- Normalize
--
-- Normalize Input (UTF-8) to the given Form, writing UTF-8 result
-- into Output. Last is the index of the last byte written
-- (Output'First - 1 if the result is empty, which cannot happen
-- for valid non-empty input).
--
-- For NFD/NFC: Output'Length >= Input'Length * 3 is always sufficient
-- (Unicode stability guarantee for canonical mappings).
-- For NFKD/NFKC: larger buffer may be needed for strings composed
-- entirely of compatibility characters.
--
-- Returns Buffer_Overflow if Output is too small.
-- Returns Invalid_Input if Input contains invalid UTF-8.
---------------------------------------------------------------------------
procedure Normalize
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form;
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
(if not Normalization_Spec.Is_Compose (Form) then
Ghost_Is_NFD (Output, Output'First, Last))
and then
(if Normalization_Spec.Is_Compose (Form) then
Ghost_Is_NFC (Output, Output'First, Last,
Normalization_Spec.Is_Canonical (Form)))
else
Last = Output'First - 1),
Always_Terminates;
---------------------------------------------------------------------------
-- Quick_Check
--
-- Returns QC_Yes if the input is definitely in the given form,
-- QC_No if it definitely is not, or QC_Maybe if full normalization
-- is needed to determine.
--
-- NFD and NFKD never return QC_Maybe.
---------------------------------------------------------------------------
function Quick_Check
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form)
return Normalization_Spec.QC_Value
with Pre => Initialized
and then Input'Length >= 1
and then Input'Last < Positive'Last;
---------------------------------------------------------------------------
-- Is_Normalized
--
-- Returns True if the input is in the given normalization form.
-- For QC_Maybe results, runs full normalization and compares.
---------------------------------------------------------------------------
function Is_Normalized
(Input : Byte_Array;
Form : Normalization_Spec.Normalization_Form)
return Boolean
with Pre => Initialized
and then Input'Length >= 1
and then Input'Last < Positive'Last;
---------------------------------------------------------------------------
-- Direct property access
---------------------------------------------------------------------------
function Get_CCC (CP : Codepoint) return Normalization_Spec.CCC_Value
with Pre => Initialized,
Global => Norm_State;
function Get_NFC_QC (CP : Codepoint) return Normalization_Spec.QC_Value
with Pre => Initialized,
Global => Norm_State;
function Get_NFKC_QC (CP : Codepoint) return Normalization_Spec.QC_Value
with Pre => Initialized,
Global => Norm_State;
---------------------------------------------------------------------------
-- Ghost functions for Platinum postconditions
--
-- These expose decomposition data as ghost expression functions
-- for use in postconditions and loop invariants.
---------------------------------------------------------------------------
-- Number of codepoints in CP's pre-expanded decomposition.
-- Returns 0 if CP maps to itself (no decomposition).
-- Hangul syllables decompose algorithmically to 2 or 3 jamo.
function Ghost_Decomp_Len
(CP : Codepoint;
Use_Canon : Boolean) return Natural
with Ghost,
Pre => Initialized,
Global => Norm_State;
-- The Idx-th codepoint in CP's decomposition (1-indexed).
function Ghost_Decomp_CP
(CP : Codepoint;
Use_Canon : Boolean;
Idx : Positive) return Codepoint
with Ghost,
Pre => Initialized
and then Ghost_Decomp_Len (CP, Use_Canon) >= 1
and then Idx <= Ghost_Decomp_Len (CP, Use_Canon),
Global => Norm_State;
-- UTF-8 byte count for one input CP's NFD expansion.
-- If CP decomposes: sum of Encoded_Length for each decomposed CP.
-- If CP maps to itself: its own Encoded_Length.
-- Hangul syllables: sum of jamo Encoded_Lengths (always 3 bytes each).
Max_Decomp_Out_Bytes : constant := 400_000;
function Ghost_Decomp_Out_Bytes
(CP : Codepoint;
Use_Canon : Boolean) return Positive
with Ghost,
Pre => Initialized,
Post => Ghost_Decomp_Out_Bytes'Result <= Max_Decomp_Out_Bytes,
Global => Norm_State;
---------------------------------------------------------------------------
-- Ghost UTF-8 decode helpers (same pattern as case_mapping)
---------------------------------------------------------------------------
function Ghost_Step_Length
(Input : Byte_Array;
Cur : Positive) return Positive
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Lead_Length (Input (Cur))
else 1)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
function Ghost_Valid
(Input : Byte_Array;
Cur : Positive) return Boolean
is (UTF8_Spec.Well_Formed_At (Input, Cur))
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
function Ghost_CP
(Input : Byte_Array;
Cur : Positive) return Codepoint
is (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Decoded_At (Input, Cur)
else 0)
with Ghost,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
---------------------------------------------------------------------------
-- Ghost_Is_NFD_From — recursive predicate: output is in NFD form
--
-- Walks Output from Cur to the end (bounded by Bound), checking each
-- codepoint:
-- 1. Valid UTF-8 encoding
-- 2. Fully canonically decomposed: Ghost_Decomp_Len(CP, True) = 0
-- and not a Hangul syllable (which would need decomposition)
-- 3. CCC non-decreasing within non-starter runs
--
-- Last_CCC tracks the CCC of the previous codepoint for ordering checks.
---------------------------------------------------------------------------
function Ghost_Is_NFD_From
(Output : Byte_Array;
Cur : Positive;
Bound : Natural;
Last_CCC : Normalization_Spec.CCC_Value) return Boolean
is (if Cur > Bound then
True
elsif not Ghost_Valid (Output, Cur) then
False
-- Encoding must fit within Bound: reject CPs whose encoded length
-- extends past Bound. Without this check, the frame lemmas cannot
-- transfer the predicate across byte-identical ranges when the
-- final codepoint's tail bytes lie beyond Bound.
elsif Cur + Ghost_Step_Length (Output, Cur) - 1 > Bound then
False
-- Must be fully decomposed (no canonical decomposition)
elsif Ghost_Decomp_Len (Ghost_CP (Output, Cur), True) /= 0 then
False
-- Hangul syllables must not appear (they decompose to jamo)
elsif Normalization_Spec.Is_Hangul_Syllable (Ghost_CP (Output, Cur)) then
False
-- CCC ordering: non-starters must be in non-decreasing CCC order
elsif Get_CCC (Ghost_CP (Output, Cur)) /= 0
and then Last_CCC > Get_CCC (Ghost_CP (Output, Cur))
then
False
-- Last codepoint (fits exactly: Cur + StepLen - 1 = Bound)
elsif Cur + Ghost_Step_Length (Output, Cur) - 1 = Bound then
True
-- Recurse to next codepoint
else
Ghost_Is_NFD_From
(Output,
Cur + Ghost_Step_Length (Output, Cur),
Bound,
Get_CCC (Ghost_CP (Output, Cur))))
with Ghost,
Pre => Initialized
and then Output'Last < Positive'Last
and then Cur >= Output'First
and then Bound <= Output'Last,
Global => Norm_State,
Subprogram_Variant => (Decreases => Bound - Cur + 1);
-- Top-level wrapper: check if Output(First..Last) is in NFD
function Ghost_Is_NFD
(Output : Byte_Array;
First : Positive;
Last : Natural) return Boolean
is (if Last < First then True
else Ghost_Is_NFD_From (Output, First, Last, 0))
with Ghost,
Pre => Initialized
and then Output'Last < Positive'Last
and then First >= Output'First
and then Last <= Output'Last,
Global => Norm_State;
---------------------------------------------------------------------------
-- NFC UTF-8 decode helpers (non-ghost)
--
-- Inlined byte-level UTF-8 decoding, NOT referencing the Ghost package
-- UTF8_Spec. Ghost_Is_NFC_From must be non-ghost because it flows
-- through Normalize_Internal's postcondition which is also non-ghost.
--
-- These helpers are literal duplicates of UTF8_Spec.Lead_Length /
-- Is_Continuation / Well_Formed_At / (lead-length-or-1) / Decoded_At.
-- Equivalence is anchored by Lemma_NFC_Matches_UTF8_Spec (declared
-- below). If either side ever drifts from the other, that lemma
-- fails to prove and the build breaks — which is what we want.
---------------------------------------------------------------------------
function NFC_Lead_Length (B : Byte) return Natural
is (if B <= 16#7F# then 1
elsif B <= 16#C1# then 0
elsif B <= 16#DF# then 2
elsif B <= 16#EF# then 3
elsif B <= 16#F4# then 4
else 0);
function NFC_Is_Cont (B : Byte) return Boolean
is (B in 16#80# .. 16#BF#);
function NFC_Valid
(Input : Byte_Array;
Cur : Positive) return Boolean
is (Cur in Input'Range
and then NFC_Lead_Length (Input (Cur)) >= 1
and then Input'Last - Cur >= NFC_Lead_Length (Input (Cur)) - 1
and then
(case NFC_Lead_Length (Input (Cur)) is
when 1 => Input (Cur) <= 16#7F#,
when 2 => Input (Cur) in 16#C2# .. 16#DF#
and then NFC_Is_Cont (Input (Cur + 1)),
when 3 =>
(Input (Cur) = 16#E0#
and then Input (Cur + 1) in 16#A0# .. 16#BF#
and then NFC_Is_Cont (Input (Cur + 2)))
or else
(Input (Cur) in 16#E1# .. 16#EC#
and then NFC_Is_Cont (Input (Cur + 1))
and then NFC_Is_Cont (Input (Cur + 2)))
or else
(Input (Cur) = 16#ED#
and then Input (Cur + 1) in 16#80# .. 16#9F#
and then NFC_Is_Cont (Input (Cur + 2)))
or else
(Input (Cur) in 16#EE# .. 16#EF#
and then NFC_Is_Cont (Input (Cur + 1))
and then NFC_Is_Cont (Input (Cur + 2))),
when 4 =>
(Input (Cur) = 16#F0#
and then Input (Cur + 1) in 16#90# .. 16#BF#
and then NFC_Is_Cont (Input (Cur + 2))
and then NFC_Is_Cont (Input (Cur + 3)))
or else
(Input (Cur) in 16#F1# .. 16#F3#
and then NFC_Is_Cont (Input (Cur + 1))
and then NFC_Is_Cont (Input (Cur + 2))
and then NFC_Is_Cont (Input (Cur + 3)))
or else
(Input (Cur) = 16#F4#
and then Input (Cur + 1) in 16#80# .. 16#8F#
and then NFC_Is_Cont (Input (Cur + 2))
and then NFC_Is_Cont (Input (Cur + 3))),
when others => False))
with Pre => Input'Last < Positive'Last;
function NFC_Step_Length
(Input : Byte_Array;
Cur : Positive) return Positive
is (if NFC_Valid (Input, Cur)
then NFC_Lead_Length (Input (Cur))
else 1)
with Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
function NFC_CP
(Input : Byte_Array;
Cur : Positive) return Codepoint
is (if not NFC_Valid (Input, Cur) then 0
else
(case NFC_Lead_Length (Input (Cur)) is
when 1 => Codepoint (Input (Cur)),
when 2 => (Input (Cur) - 16#C0#) * 64
+ (Input (Cur + 1) - 16#80#),
when 3 => (Input (Cur) - 16#E0#) * 4096
+ (Input (Cur + 1) - 16#80#) * 64
+ (Input (Cur + 2) - 16#80#),
when 4 => (Input (Cur) - 16#F0#) * 262144
+ (Input (Cur + 1) - 16#80#) * 4096
+ (Input (Cur + 2) - 16#80#) * 64
+ (Input (Cur + 3) - 16#80#),
when others => 0))
with Pre => Input'Last < Positive'Last
and then Cur in Input'Range;
---------------------------------------------------------------------------
-- Ghost lemma: NFC_* helpers match UTF8_Spec.
--
-- The NFC_Lead_Length / NFC_Is_Cont / NFC_Valid / NFC_Step_Length /
-- NFC_CP expression functions above are literal duplicates of the
-- ghost predicates in Lingenic_Text.UTF8_Spec. The duplication exists
-- because Norm_Output_Valid and Norm_Partial_Valid (formal function
-- actuals to the Text_Transform generic) are non-ghost in GNAT 15,
-- and SPARK forbids ghost expression functions from being referenced
-- by non-ghost expression-function contexts.
--
-- This lemma anchors the duplicates to the canonical UTF-8 spec. It
-- proves equivalence at any (Input, Cur) by direct unfolding of both
-- sides; the body is null because the expression bodies are
-- structurally identical. If either side is ever changed without the
-- other, this lemma fails to prove and the build breaks.
---------------------------------------------------------------------------
procedure Lemma_NFC_Matches_UTF8_Spec
(Input : Byte_Array;
Cur : Positive)
with Ghost,
Always_Terminates,
Pre => Input'Last < Positive'Last
and then Cur in Input'Range,
Post => NFC_Lead_Length (Input (Cur))
= UTF8_Spec.Lead_Length (Input (Cur))
and then NFC_Valid (Input, Cur)
= UTF8_Spec.Well_Formed_At (Input, Cur)
and then NFC_Step_Length (Input, Cur)
= (if UTF8_Spec.Well_Formed_At (Input, Cur)
then UTF8_Spec.Lead_Length (Input (Cur))
else 1)
and then (if UTF8_Spec.Well_Formed_At (Input, Cur) then
NFC_CP (Input, Cur)
= UTF8_Spec.Decoded_At (Input, Cur)
else
NFC_CP (Input, Cur) = 0);
---------------------------------------------------------------------------
-- Ghost_Is_NFC_From — recursive predicate: output is in NFC form
--
-- Walks Output from Cur to the end (bounded by Bound), checking each
-- codepoint:
-- 1. Valid UTF-8 encoding
-- 2. Quick Check pass: NFC_QC(CP) /= QC_No (for canonical)
-- or NFKC_QC(CP) /= QC_No (for compatibility)
-- 3. CCC non-decreasing within non-starter runs
--
-- Use_Canon selects NFC (True) vs NFKC (False) Quick Check table.
-- Last_CCC tracks the CCC of the previous codepoint for ordering checks.
--
-- NON-GHOST: referenced by Norm_Output_Valid / Norm_Partial_Valid,
-- which are formal function actuals (cannot be ghost in GNAT 15).
-- Uses NFC_Step_Length / NFC_Valid / NFC_CP (non-ghost equivalents).
---------------------------------------------------------------------------
function Ghost_Is_NFC_From
(Output : Byte_Array;
Cur : Positive;
Bound : Natural;
Last_CCC : Normalization_Spec.CCC_Value;
Use_Canon : Boolean) return Boolean
is (if Cur > Bound then
True
elsif not NFC_Valid (Output, Cur) then
False
-- Encoding must fit within Bound: reject CPs whose encoded length
-- extends past Bound. Without this check, the frame lemmas cannot
-- transfer the predicate across byte-identical ranges when the
-- final codepoint's tail bytes lie beyond Bound.
elsif Cur + NFC_Step_Length (Output, Cur) - 1 > Bound then
False
-- Quick Check: no QC_No characters allowed in composed output
elsif Use_Canon
and then Get_NFC_QC (NFC_CP (Output, Cur))
= Normalization_Spec.QC_No
then
False
elsif not Use_Canon
and then Get_NFKC_QC (NFC_CP (Output, Cur))
= Normalization_Spec.QC_No
then
False
-- CCC ordering: non-starters must be in non-decreasing CCC order
elsif Get_CCC (NFC_CP (Output, Cur)) /= 0
and then Last_CCC > Get_CCC (NFC_CP (Output, Cur))
then
False
-- Last codepoint (fits exactly: Cur + StepLen - 1 = Bound)
elsif Cur + NFC_Step_Length (Output, Cur) - 1 = Bound then
True
-- Recurse to next codepoint
else
Ghost_Is_NFC_From
(Output,
Cur + NFC_Step_Length (Output, Cur),
Bound,
Get_CCC (NFC_CP (Output, Cur)),
Use_Canon))
with Pre => Initialized
and then Output'Last < Positive'Last
and then Cur >= Output'First
and then Bound <= Output'Last,
Global => Norm_State,
Subprogram_Variant => (Decreases => Bound - Cur + 1);
-- Top-level wrapper: check if Output(First..Last) is in NFC/NFKC
function Ghost_Is_NFC
(Output : Byte_Array;
First : Positive;
Last : Natural;
Use_Canon : Boolean) return Boolean
is (if Last < First then True
else Ghost_Is_NFC_From (Output, First, Last, 0, Use_Canon))
with Pre => Initialized
and then Output'Last < Positive'Last
and then First >= Output'First
and then Last <= Output'Last,
Global => Norm_State;
---------------------------------------------------------------------------
-- Ghost_Norm_Out — recursive output byte count for normalization
--
-- Walks Input from Cur, accumulating the total UTF-8 byte count of the
-- decomposed (and for NFC/NFKC, recomposed) output. For NFD/NFKD
-- this is the sum of Ghost_Decomp_Out_Bytes for each input codepoint.
--
-- NFC/NFKC adds composition which changes the byte count — handled
-- separately in Phase 7. For now this covers NFD/NFKD.
---------------------------------------------------------------------------
Max_Norm_Acc : constant := Natural'Last / 2;
function Ghost_Norm_Out
(Input : Byte_Array;
Cur : Positive;
Use_Canon : Boolean;
Acc : Natural) return Natural
is (if Cur not in Input'Range then
Acc
elsif not Ghost_Valid (Input, Cur) then
0 -- Invalid UTF-8: failure sentinel
elsif Acc > Max_Norm_Acc then
0 -- Overflow guard
elsif Cur > Input'Last - Ghost_Step_Length (Input, Cur) + 1 then
Acc + Ghost_Decomp_Out_Bytes (Ghost_CP (Input, Cur), Use_Canon)
else
Ghost_Norm_Out
(Input,
Cur + Ghost_Step_Length (Input, Cur),
Use_Canon,
Acc + Ghost_Decomp_Out_Bytes (Ghost_CP (Input, Cur), Use_Canon)))
with Ghost,
Pre => Initialized
and then Input'Last < Positive'Last
and then Input'Length >= 1
and then Cur > 0,
Global => Norm_State,
Subprogram_Variant => (Decreases => Input'Last - Cur + 1);
-- Top-level wrappers
function Ghost_NFD_Total (Input : Byte_Array) return Natural
is (Ghost_Norm_Out (Input, Input'First, True, 0))
with Ghost,
Pre => Initialized
and then Input'Length >= 1
and then Input'Last < Positive'Last,
Global => Norm_State;
function Ghost_NFKD_Total (Input : Byte_Array) return Natural
is (Ghost_Norm_Out (Input, Input'First, False, 0))
with Ghost,
Pre => Initialized
and then Input'Length >= 1
and then Input'Last < Positive'Last,
Global => Norm_State;
end Lingenic_Text.Normalization;