Lingenic-Text

The first formally verified Unicode text processing library.

Version 1.1.0 · Unicode 17.0 · SPARK/Ada (Ada 2022) · 53 source files · ~30,500 lines

Lingenic-Text implements the Unicode 17.0 standard in SPARK/Ada with machine-checked correctness proofs on every subprogram.

The full library surface is also available as a C static library — 53 functions in include/lingenic_text.h, covering every module from UTF-8 to IDNA.

Unicode text processing has historically been a domain where correctness is assumed on faith: test suites catch some bugs, fuzzing catches some more, and the rest ship. Lingenic-Text takes a different position. The Unicode algorithms are deterministic specifications with well-defined rules — they can be encoded as mathematical functions and the implementation can be proved to match. That is what this library does. The ghost specification is the standard; the prover confirms the code follows it; the conformance tests confirm the specification was transcribed correctly. Two independent evidence chains, no gaps.

Segmentation, normalization, case mapping, collation, the bidirectional algorithm, IDNA, emoji classification — fourteen algorithm modules, each with postconditions verified by GNATprove for all inputs. No heap allocation. No runtime exceptions. Every buffer is bounded, every index is proved in range, every output is specified by a ghost function that encodes the Unicode rules directly.

Key Design Principles

1. Ghost specification first — every algorithm gets a *_spec.ads with pure expression functions the solver unfolds. Ghost code is free (compiled to nothing).
2. Double proof chain — formal proofs verify implementation ≡ ghost spec; conformance tests verify ghost spec ≡ Unicode standard. No gap.
3. Flat O(1) arrays — all property lookups are indexed by codepoint. No trees, no hash tables, deterministic and proved.
4. No heap, no exceptions — all buffers are bounded Byte_Arrays, all paths structurally proved safe. Runtime checks suppressed via -gnatp because GNATprove has already proved them.
5. UCD at runtime — no code generator. Property tables populated from UCD text files at initialization. Drop new files to update Unicode version.
6. SPARK_Mode(Off) boundary — only File_IO touches the outside world; everything else is proved SPARK.

macOS environment setup (replace USERNAME and NNNNNN with your values):

export LIBRARY_PATH="$(xcrun --show-sdk-path)/usr/lib"
export PATH="/Users/USERNAME/.local/share/alire/toolchains/gprbuild_25.0.1_NNNNNN/bin:/Users/USERNAME/.local/share/alire/toolchains/gnat_native_15.1.2_NNNNNN/bin:$PATH"

Modules

Approach

Spec-first, top-down:

1. Ghost functions encode Unicode rules directly from the standard — the specification is the code
2. Postconditions on implementation functions reference the ghost spec
3. GNATprove verifies the postconditions hold — machine-checked, no hand-waving
4. Runtime safety falls out as a side effect of step 3

Ghost code (with Ghost) compiles to nothing. Zero runtime cost, zero code size impact. The proof is the product.

The ghost spec is the rules — GB3_Applies, GB9c_Applies, Is_Grapheme_Break — encoded as expression functions the solver can unfold. For the segmentation modules, recursive ghost functions (Next_GCB_From, Next_WB_From, Next_SB_From, Next_LB_From) simulate the complete algorithm as pure mathematical functions. Postconditions say Next_Pos = Next_GCB_From(Text, Pos) — GNATprove proves the implementation matches the specification for all inputs. For the transform modules (normalization, case mapping), recursive ghost predicates (Ghost_Is_NFD, Ghost_Is_NFC, Ghost_Upper_Total, Ghost_Lower_Total) specify what correct output means, and the prover confirms the implementation satisfies these predicates.

The conformance tests verify the ghost specs themselves encode the correct Unicode rules. Two independent chains of evidence: proofs guarantee the implementation matches the spec, tests guarantee the spec matches the standard.

Architecture

lingenic_text.gpr              GPR project file (verified core)
lingenic_text_c.gpr            GPR project file (C library)
build.adc / gnatprove.adc      Compiler configuration (build / prove)
VERSION                         1.1.0

src/                            53 Ada source files (~30,500 lines)
  lingenic_text.ads               Root: Codepoint, Byte, Byte_Array
  lingenic_text-<module>_spec.ads Ghost: Unicode rules as expression functions
  lingenic_text-<module>.ads/adb  Implementation with proved postconditions
  lingenic_text-text_transform.ads Generic UTF-8 → UTF-8 transform

src-c/                          C binding (validation shim, SPARK_Mode Off)
  lingenic_text_c.ads/.adb        53 exported lt_* functions

include/
  lingenic_text.h                 C header: prototypes + constants

ucd/                            28 Unicode Character Database files
  UnicodeData.txt, Scripts.txt, allkeys.txt, ...

tests/                          13 conformance test programs
  test_graphemes.adb, test_normalization.adb, ...
  c/smoke_test.c                 C API smoke test (106 checks)

scripts/
  fetch-ucd.sh                   Download UCD files from unicode.org

docs/                           21 documentation files
  OVERVIEW.txt, ARCHITECTURE.txt, API_REFERENCE.txt, C_API_GUIDE.txt, ...

Every Unicode algorithm follows the same structure:

lingenic_text-<module>_spec.ads   -- Ghost: Unicode rules as expression functions
lingenic_text-<module>.ads/.adb   -- Implementation with postconditions referencing spec

All modules that transform UTF-8 input into UTF-8 output (normalization, case mapping) instantiate the generic Text_Transform procedure. The generic handles UTF-8 decoding, output position tracking, and per-codepoint dispatch. Modules provide State_Type, On_Codepoint, and On_Finish callbacks with formal contracts guaranteeing output position monotonicity and bounds safety.

Property data comes from Unicode Character Database files read at initialization and parsed by a proved SPARK parser. The entire chain from file format to query result is machine-checked:

UCD files (unicode.org, in ucd/ directory)
  → File_IO.Read_File (only SPARK_Mode Off code in the library)
    → Byte_Array in memory
      → Extract_Value_Names (proved, discovers property values)
      → Parse_Property_File (proved, postcondition: ∀CP. Table(CP) = Expected_Value(Source, 1, CP, ...))
        → flat lookup tables indexed by codepoint (O(1) access)

No code generator. No generated source files. New Unicode version = drop new UCD files in the ucd/ directory.

Building

Requires GNAT 15+, GPRBuild 25+, and GNATprove 15+ (Ada 2022). UCD files in ucd/.

# Fetch UCD files
scripts/fetch-ucd.sh

# Build the static library
gprbuild -P lingenic_text.gpr

# Run formal verification (all VCs, Level 4, 60s timeout)
gnatprove -P lingenic_text.gpr -XMODE=prove -j0

# Build and run a conformance test
gprbuild -P tests/test_graphemes.gpr
./tests/obj/test_graphemes

The library produces a static archive at lib/lingenic_text.a. Runtime checks are suppressed (-gnatp) because GNATprove has already proved their absence. Assertions are set to Ignore in build mode (build.adc) and Check in prove mode (gnatprove.adc).

C Library

The full library surface is also available as a C static library — 53 functions in include/lingenic_text.h, covering every module from UTF-8 to IDNA. The binding is a thin validation shim over the proved core: every C entry point checks its arguments against the precondition of the proved subprogram it calls and returns LT_ERR on violation, so the core's machine-checked postconditions apply to every successful call.

# Build the C library (produces lib-c/liblingenic_text_c.a)
gprbuild -P lingenic_text_c.gpr -p -j0

# Use it
cc your_program.c -Iinclude -Llib-c -llingenic_text_c -lgnat

lingenic_text_cinit();               /* Ada elaboration, once      */
lt_init("ucd");                      /* load UCD data tables       */
lt_normalize(LT_NFC, in, in_len, out, sizeof out, &out_len);

See src-c/README.md for build and linking details (including the macOS static-runtime note) and docs/C_API_GUIDE.txt for the complete function-by-function guide. The C API smoke test (tests/c/smoke_test.c, 106 checks) exercises every module through the binding.

Initialization

Modules with runtime data tables require initialization before use:

Properties.Initialize ("ucd", Success);        --  1. Reads 12+ UCD files
Emoji.Initialize ("ucd", Emoji_OK);             --  2. Independent, reads emoji-data.txt
Normalization.Initialize ("ucd", Norm_OK);       --  3. Reads UnicodeData.txt + derived
Case_Mapping.Initialize ("ucd", Case_OK);        --  4. Requires Properties
Collation.Initialize ("ucd", Coll_OK);           --  5. Requires Normalization
Bidi.Initialize ("ucd", Bidi_OK);                --  6. Requires Properties
IDNA.Initialize ("ucd", IDNA_OK);                --  7. Requires Properties + Normalization

Segmentation modules (Graphemes, Words, Sentences, Line_Break), EAW, and Identifiers require Properties.Initialized but have no Initialize of their own.

Conformance Tests

Each module is validated against official Unicode 17.0 test files:

Constraints

• No pragma Assume — only real proofs
• No algorithm changes to satisfy the prover — if the spec says it, implement it exactly
• Flat array indexed lookup for all property tables — O(1), no trees, no hash tables
• UCD files are read from disk at initialization — drop new files from unicode.org to update
• Every Unicode conformance test suite must pass
• All ghost code erased at compile time — zero runtime cost

Documentation

Comprehensive documentation is available in docs/: