LINGENIC-TEXT
=============
The First Formally Verified Unicode Text Processing Library
Version: 1.1.0
Standard: Unicode 17.0
Language: SPARK/Ada (Ada 2022)
WHAT IT IS
----------
Lingenic-Text implements the Unicode 17.0 standard in SPARK/Ada with
machine-checked correctness proofs on every subprogram. Fourteen
algorithm modules:
- UTF-8 encoding and decoding (RFC 3629)
- Text segmentation: grapheme clusters, words, sentences (UAX #29)
- Line breaking (UAX #14)
- Normalization: NFD, NFC, NFKD, NFKC, Quick Check (UAX #15)
- Case mapping: uppercase, lowercase, titlecase, casefold (Unicode S3.13)
- Collation: DUCET Compare and Sort_Key (UTS #10)
- Bidirectional Algorithm: full P2-L4 (UAX #9)
- East Asian Width: display width in cells (UAX #11)
- Emoji: 5 boolean properties, 8-type sequence classification (UTS #51)
- Identifiers: XID_Start, XID_Continue (UAX #31)
- IDNA: To_ASCII, To_Unicode with Punycode (UTS #46)
- Properties: O(1) lookup for 15+ properties across all codepoints
Each module has 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.
WHY IT EXISTS
-------------
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.
WHAT FORMAL VERIFICATION MEANS HERE
------------------------------------
Every subprogram in Lingenic-Text carries contracts:
- Preconditions state what the caller must guarantee
- Postconditions state what the subprogram guarantees in return
- Loop invariants maintain correctness through iteration
GNATprove (the SPARK prover) discharges every verification condition at
Level 4, the highest setting. This means:
- Every array index is proved in range
- Every arithmetic operation is proved free of overflow
- Every output matches its ghost specification
- Every loop terminates (Subprogram_Variant annotations)
No pragma Assume is used. No proofs are hand-waved. If a verification
condition does not discharge, the code does not build.
CONSTRAINTS
-----------
- No pragma Assume -- only real proofs
- No algorithm changes to satisfy the prover -- 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 to a new Unicode version
- Every Unicode conformance test suite must pass
PROJECT LAYOUT
--------------
lingenic_text.gpr GPR project file
build.adc Build-mode compiler pragmas
gnatprove.adc Prove-mode compiler pragmas
VERSION Version string (1.1.0)
src/ 55 Ada source files (~27,500 lines)
lingenic_text.ads Root package: core types
lingenic_text-*.ads Specification files
lingenic_text-*.adb Implementation files
ucd/ 29 Unicode Character Database files
UnicodeData.txt Core character data
Scripts.txt Script property
allkeys.txt DUCET (collation)
...and 26 more
tests/ 12+ conformance test programs
test_graphemes.adb GraphemeBreakTest.txt
test_normalization.adb NormalizationTest.txt
...and more
scripts/ Build and maintenance scripts
fetch-ucd.sh Download UCD files from unicode.org
lib/ Compiled static library
obj/ Object files
docs/ This documentation
TOOLCHAIN REQUIREMENTS
----------------------
GNAT 15.1.2 or later (Ada 2022 compiler)
GPRBuild 25.0.1 or later (Build system)
GNATprove 15.1.0 or later (Formal verification)
See BUILDING.txt for installation and usage instructions.