NORMALIZATION MODULE
====================
Standard: UAX #15 (Unicode Normalization Forms)
Files: src/lingenic_text-normalization_spec.ads (ghost specification)
src/lingenic_text-normalization.ads (public API)
src/lingenic_text-normalization.adb (implementation)
PURPOSE
-------
The Normalization module implements the four Unicode normalization forms:
NFD Canonical Decomposition
NFC Canonical Decomposition followed by Canonical Composition
NFKD Compatibility Decomposition
NFKC Compatibility Decomposition followed by Canonical Composition
Plus Quick Check and Is_Normalized queries.
Normalization is required by several higher-level algorithms (Collation
uses NFD internally; IDNA uses NFC) and is available as a standalone
transform.
GHOST SPECIFICATION (Normalization_Spec)
----------------------------------------
Package Lingenic_Text.Normalization_Spec is Pure.
Types:
subtype CCC_Value is Natural range 0 .. 254;
Canonical Combining Class. 0 = starter, non-zero = non-starter.
type QC_Value is (QC_Yes, QC_No, QC_Maybe);
Quick Check result.
type Normalization_Form is (NFD, NFC, NFKD, NFKC);
Predicates:
Is_Starter(CCC) CCC = 0
Is_Canonical(Form) Form = NFD or Form = NFC
Is_Compose(Form) Form = NFC or Form = NFKC
CCC_Ordered(A, B) A <= B (canonical ordering)
Hangul Constants (Unicode Standard, Section 3.12):
SBase = 16#AC00#
LBase = 16#1100#
VBase = 16#1161#
TBase = 16#11A7#
LCount = 19, VCount = 21, TCount = 28
NCount = 588 (VCount * TCount)
SCount = 11172 (LCount * NCount)
Hangul Predicates:
Is_Hangul_Syllable(CP) CP in SBase..SBase+SCount-1
Is_Hangul_LV(CP) LV syllable (no trailing consonant)
Is_Hangul_L(CP) Leading consonant jamo
Is_Hangul_V(CP) Vowel jamo
Is_Hangul_T(CP) Trailing consonant jamo
INITIALIZATION
--------------
procedure Initialize
(UCD_Dir : String;
Success : out Boolean);
Post: if Success then Initialized and Data_All_Terminal
Reads from UCD_Dir:
UnicodeData.txt CCC values (field 3)
Decomposition mappings (field 5)
DerivedNormalizationProps.txt Quick Check tables (NFD_QC, NFC_QC,
NFKD_QC, NFKC_QC)
Composition exclusions
Builds internal data tables:
CCC_Table Flat array: codepoint -> CCC_Value (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_QC/NFC_QC/... Quick Check tables per normalization form
Data_All_Terminal is a ghost predicate asserting that all decomposition
table entries are fully expanded (no further decomposition possible, no
Hangul syllables in the data). True by construction: Initialize runs
Expand_Decompositions which iterates decomposition tables to fixed point.
PUBLIC API
----------
Normalize:
procedure Normalize
(Input : Byte_Array;
Form : Normalization_Form;
Output : in out Byte_Array;
Last : out Natural;
Status : out Norm_Status);
Pre: Initialized, Data_All_Terminal
Input'Length >= 1, Output'Length >= 1
Input'Last < Positive'Last, Output'Last < Positive'Last
Output'Length <= Max_Norm_Acc
Post: if Status = Success then
Last in Output'First..Output'Last
if decompose form (NFD/NFKD):
Ghost_Is_NFD(Output, Output'First, Last)
if compose form (NFC/NFKC):
Ghost_Is_NFC(Output, Output'First, Last, Is_Canonical(Form))
else
Last = Output'First - 1
Status values:
Success Normalization completed
Buffer_Overflow Output buffer too small
Invalid_Input Input contains invalid UTF-8
Buffer sizing:
For NFD/NFC (canonical): Output'Length >= Input'Length * 3 is
always sufficient (Unicode stability guarantee).
For NFKD/NFKC: larger buffer may be needed for strings composed
entirely of compatibility characters.
Quick_Check:
function Quick_Check
(Input : Byte_Array;
Form : Normalization_Form)
return QC_Value;
Returns QC_Yes if the input is definitely in the given form,
QC_No if it definitely is not, QC_Maybe if full normalization
is needed to determine. NFD and NFKD never return QC_Maybe.
Is_Normalized:
function Is_Normalized
(Input : Byte_Array;
Form : Normalization_Form)
return Boolean;
Returns True if the input is in the given form.
For QC_Maybe results, runs full normalization and compares.
Direct Property Access:
Get_CCC(CP) -> CCC_Value Canonical Combining Class
Get_NFC_QC(CP) -> QC_Value NFC Quick Check for single codepoint
Get_NFKC_QC(CP) -> QC_Value NFKC Quick Check for single codepoint
GHOST CORRECTNESS PREDICATES
-----------------------------
Ghost_Is_NFD(Output, First, Last):
Recursive predicate checking that Output(First..Last) is in NFD:
1. Every position contains valid UTF-8
2. Every codepoint is fully canonically decomposed
(Ghost_Decomp_Len(CP, True) = 0)
3. No Hangul syllables appear (they would need decomposition)
4. CCC values are non-decreasing within non-starter runs
Ghost_Is_NFC(Output, First, Last, Use_Canon):
Recursive predicate checking that Output(First..Last) is in NFC/NFKC:
1. Every position contains valid UTF-8
2. No codepoint has Quick Check = QC_No
(NFC_QC for canonical, NFKC_QC for compatibility)
3. CCC values are non-decreasing within non-starter runs
Ghost Decomposition Functions:
Ghost_Decomp_Len(CP, Use_Canon)
Number of codepoints in CP's pre-expanded decomposition.
Returns 0 if CP maps to itself.
Ghost_Decomp_CP(CP, Use_Canon, Idx)
The Idx-th codepoint in CP's decomposition (1-indexed).
Ghost_Decomp_Out_Bytes(CP, Use_Canon)
UTF-8 byte count for CP's NFD expansion.
NFC HELPERS AND THE DUPLICATION LEMMA
--------------------------------------
Ghost_Is_NFC_From uses non-ghost NFC_* helper functions (NFC_Valid,
NFC_Step_Length, NFC_CP) that are literal duplicates of the UTF8_Spec
ghost functions. This duplication exists because formal function actuals
to the Text_Transform generic cannot be ghost in GNAT 15.
The equivalence is anchored by:
procedure Lemma_NFC_Matches_UTF8_Spec(Input, Cur)
Post: NFC_Lead_Length = UTF8_Spec.Lead_Length
NFC_Valid = UTF8_Spec.Well_Formed_At
NFC_Step_Length matches
NFC_CP matches Decoded_At
The body is null (structural identity). If either side ever drifts
from the other, this lemma fails to prove and the build breaks.
ALGORITHM OVERVIEW
------------------
NFD/NFKD:
1. Decode input codepoint
2. Decompose (canonical or compatibility) using pre-expanded tables
3. For Hangul syllables, decompose algorithmically to jamo
4. Accumulate decomposed codepoints in a segment buffer
5. At each starter, flush the segment: sort non-starters by CCC,
encode to output
6. Ghost_Is_NFD_From is maintained as the loop invariant
NFC/NFKC:
1. Perform NFD/NFKD (steps 1-5 above)
2. During flush, apply canonical composition:
- Find leftmost starter
- Try composing with each non-starter (if CCC allows)
- Composition pairs looked up in Comp_Index/Pairs table
- Hangul L+V -> LV, LV+T -> LVT composed algorithmically
3. Ghost_Is_NFC_From is maintained as the loop invariant
The implementation instantiates the generic Text_Transform procedure
with normalization-specific On_Codepoint and On_Finish callbacks.
CONSTANTS
---------
Max_Decomp_Out_Bytes = 400_000 Max ghost decomposition byte count
Max_Norm_Acc = Natural'Last / 2 Max output accumulator value