ARCHITECTURE
============
This document describes the architecture, design patterns, and layering
of Lingenic-Text.
PACKAGE HIERARCHY
-----------------
Everything lives under the root package Lingenic_Text. Child packages
are named Lingenic_Text.<Module> with an optional _Spec suffix for
ghost specifications.
Lingenic_Text Root: core types and constants
.UTF8_Spec Ghost: RFC 3629 encoding rules
.UTF8 Implementation: Encode, Decode
.UCD_Format_Spec Ghost: UCD file format rules (UAX #44)
.UCD_Parser Proved UCD property file parser
.Scx_Parser Proved Script_Extensions parser
.File_IO Disk I/O (only SPARK_Mode Off code)
.Properties_Spec Ghost: Joining_Type values
.Properties O(1) property lookup tables
.Graphemes_Spec Ghost: GB rules 3-999
.Graphemes Grapheme cluster segmentation
.Words_Spec Ghost: WB rules 3-999
.Words Word segmentation
.Sentences_Spec Ghost: SB rules 3-999
.Sentences Sentence segmentation
.Line_Break_Spec Ghost: LB rules 1-30b
.Line_Break Line break detection
.Normalization_Spec Ghost: CCC, QC, Hangul constants
.Normalization NFD, NFC, NFKD, NFKC, Quick Check
.Case_Mapping_Spec Ghost: sigma constants, Final_Sigma
.Case_Mapping Uppercase, Lowercase, Titlecase, Casefold
.Collation_Spec Ghost: weight types, implicit ranges
.Collation DUCET Compare, Sort_Key
.Bidi_Spec Ghost: Bidi_Class values, embedding types
.Bidi Resolve_Levels, Reorder, Needs_Mirror
.EAW_Spec Ghost: East_Asian_Width values, Cell_Width
.EAW Display_Width
.Emoji_Spec Ghost: sequence types, structural codepoints
.Emoji Boolean properties, Classify_Sequence
.Identifiers XID_Start, XID_Continue
.IDNA_Spec Ghost: Punycode params, IDNA status types
.IDNA To_ASCII, To_Unicode
.Text_Transform Generic UTF-8 -> UTF-8 transform procedure
THE FOUR LAYERS
---------------
Layer 1: Foundation
The root package defines core types used everywhere:
subtype Codepoint is Natural range 0 .. 16#10_FFFF#;
subtype Byte is Natural range 0 .. 255;
type Byte_Array is array (Positive range <>) of Byte;
Plus surrogate range constants, scalar value predicates, and ASCII byte
constants for UCD file parsing.
UTF8_Spec encodes RFC 3629 as pure ghost expression functions. UTF8
implements Decode and Encode with postconditions referencing the ghost
spec. The UTF-8 layer is the only path from raw bytes to codepoints.
Layer 2: UCD Infrastructure
UCD_Format_Spec encodes the UAX #44 Section 4.2 property file format
as ghost expression functions: hex parsing, line structure, field
extraction, byte comparison. All erased at compile time.
UCD_Parser is the proved parser. It reads any standard-format UCD file
and populates a flat Property_Table (array[Codepoint] of Property_Index).
The postcondition proves:
for all CP in Codepoint =>
Table(CP) = Expected_Value(Source, 1, CP, Names, Num_Values)
This means every codepoint's property index matches what the UCD file
specifies, as defined by the recursive ghost function Expected_Value.
File_IO is the only SPARK_Mode(Off) code. It reads files from disk
into bounded Byte_Array buffers (max 4 MB per file). Trust boundary:
same as the compiler. Once bytes are in memory, everything is proved.
Layer 3: Properties
The Properties module reads 12+ UCD files at initialization and
populates O(1) flat arrays indexed by codepoint. Every property
lookup is a single array access -- no trees, no hash tables, fully
deterministic and proved.
Properties exposed: Script, Script_Extensions, GBP, WBP, SBP, LBP,
EAW, Bidi_Class, General_Category, Joining_Type, Extended_Pictographic,
XID_Start, XID_Continue, Bidi_Mirrored, InCB.
The Emoji module independently loads 5 boolean emoji properties.
Layer 4: Algorithms
Every algorithm module sits on top of Layers 1-3 and follows one of
two patterns:
a) Segmentation pattern (Graphemes, Words, Sentences, Line_Break):
- Ghost _Spec encodes individual rules as expression functions
- Ghost recursive function simulates the complete algorithm
- Implementation is a forward state machine
- Postcondition: implementation output = ghost recursive function
b) Transform pattern (Normalization, Case_Mapping):
- Ghost specification defines what correct output means
- Implementation instantiates the generic Text_Transform procedure
- Text_Transform handles UTF-8 decode, output tracking, dispatch
- Module provides On_Codepoint callback with loop-invariant contract
- Postcondition: output satisfies the ghost correctness predicate
INITIALIZATION ORDER
--------------------
Modules with runtime data tables require initialization by calling their
Initialize procedure with the UCD directory path. The dependency order:
1. Properties.Initialize(UCD_Dir) -- reads 12+ UCD files
2. Emoji.Initialize(UCD_Dir) -- independent, reads emoji-data.txt
3. Normalization.Initialize(UCD_Dir) -- reads UnicodeData.txt + derived
4. Case_Mapping.Initialize(UCD_Dir) -- requires Properties
5. Collation.Initialize(UCD_Dir) -- requires Normalization
6. Bidi.Initialize(UCD_Dir) -- requires Properties
7. IDNA.Initialize(UCD_Dir) -- requires Properties + Normalization
Segmentation modules (Graphemes, Words, Sentences, Line_Break) require
Properties to be initialized but have no Initialize of their own -- they
use Properties directly at call time.
The EAW and Identifiers modules are thin wrappers around Properties
lookups and require only Properties.Initialized.
THE GHOST SPECIFICATION PATTERN
-------------------------------
Every algorithm has a ghost specification. The pattern:
1. Spec file (*_spec.ads) with SPARK_Mode, Ghost, Pure:
- Named constants for abstract property values
- Expression functions encoding individual rules
- Composite decision function combining rules in priority order
2. Implementation file (*.ads):
- State record capturing the minimum context for the state machine
- Ghost helper functions (Ghost_CP, Ghost_GBP, Ghost_Break, etc.)
that mirror the runtime decode + property lookup as expression
functions the solver can unfold
- Recursive ghost function simulating the complete algorithm
- Public procedure with postcondition referencing the ghost function
3. Body file (*.adb):
- Forward state machine implementing the algorithm
- Loop invariants connecting the loop state to the ghost function
- The prover verifies the loop body's state transitions match the
ghost function's recursive steps
Ghost code is free. All functions and predicates marked Ghost or in
Ghost packages are erased completely at compile time. Zero runtime cost,
zero code size impact. The proof is the product.
THE GENERIC TEXT_TRANSFORM
--------------------------
Modules that transform UTF-8 input into UTF-8 output share a common
structure via the generic procedure Text_Transform.
Generic parameters:
State_Type Module-specific state record
Output_Valid Final postcondition: what "correct output" means
Partial_Valid Loop invariant: maintained across On_Codepoint calls
On_Codepoint Per-codepoint callback:
Pre: Partial_Valid holds
Post: Pos >= Pos'Old, Pos <= Output'Last + 1,
Partial_Valid still holds (if OK)
On_Finish End-of-input finalization:
Pre: Partial_Valid holds
Post: Output_Valid holds (if OK)
The generic handles:
- UTF-8 decoding of input bytes into codepoints
- Output buffer position tracking
- Per-codepoint dispatch
- The bridge from loop invariant to postcondition via On_Finish
Instantiated by Normalization (for NFD/NFC/NFKD/NFKC) and Case_Mapping
(for Uppercase/Lowercase/Casefold).
DATA REPRESENTATION
-------------------
Property tables: Flat arrays indexed by codepoint.
type Property_Table is array (Codepoint) of Property_Index;
Property_Index is 0..255. Index 0 is the default/unassigned value.
Indices 1..255 are named property values discovered by
Extract_Value_Names during initialization.
For boolean properties (ExtPict, XID_Start, XID_Continue, Bidi_Mirrored,
Is_Cased, Is_Case_Ignorable, emoji properties), flat Boolean arrays
indexed by codepoint.
Script_Extensions: Pool-interned script sets.
type Script_Set is record
Count : Natural range 0 .. 255;
Items : array (1 .. 255) of Property_Index;
end record;
type Scx_Table_Array is array (Codepoint) of Scx_Pool_Id;
Codepoints sharing the same script-extension set point to the same
pool entry. ~300 distinct sets for 1.1M codepoints.
Case mappings: Index/Data tables.
Per-codepoint: index into a data array containing 1-3 mapped codepoints.
Self-mapping codepoints have index 0 (identity mapping, no data entry).
Normalization: Pre-expanded decomposition tables.
Decompositions are expanded to fixed point at initialization time.
No recursive decomposition at runtime. Composition pairs stored as
(starter, combining) -> composite lookup.
Collation: CE_Index/CE_Data with contraction tables.
Per-codepoint index into collation element data. Contraction starters
have a Boolean flag; contraction matching uses Starter_Index/Entries.
Implicit weights computed algorithmically for CJK and other ranges.
SPARK_MODE BOUNDARIES
---------------------
The entire library is SPARK_Mode(On) except:
- File_IO.Read_File: reads bytes from disk into a Byte_Array buffer.
This is the trust boundary. Once bytes are in memory, all processing
is proved SPARK.
- Initialize procedure bodies: these call File_IO.Read_File and then
the proved parsers. The bodies are SPARK_Mode(Off) because they
must call the non-SPARK File_IO, but the postconditions on the
Initialize procedures are proved.
- build.adc: pragma Assertion_Policy(Ignore) -- assertions are proved
by GNATprove, not checked at runtime. Runtime checks suppressed via
-gnatp because the prover has already discharged them.
DOUBLE PROOF CHAIN
------------------
Correctness rests on two independent evidence chains:
1. Formal proofs: GNATprove verifies that the implementation matches
the ghost specification for all inputs. If the implementation
deviates from the spec, the proof fails and the code does not build.
2. Conformance tests: Official Unicode test suites (GraphemeBreakTest.txt,
NormalizationTest.txt, BidiCharacterTest.txt, etc.) verify that the
ghost specification encodes the correct Unicode rules. If the spec
is wrong, the tests fail.
Together: implementation = specification (by proof), specification =
standard (by test). No gap.