TECHNICAL REVIEW: LINGENIC-TEXT
===============================
Project: Lingenic-Text v1.1.0
Scope: Unicode 17.0 text processing library
Language: SPARK/Ada (Ada 2022)
Scale: 53 source files, ~30,500 lines, 14 algorithm modules
Method: Formal verification (GNATprove Level 4), conformance testing
SUMMARY
-------
Lingenic-Text is a formally verified Unicode 17.0 text processing
library. Fourteen algorithm modules -- UTF-8 encoding, text
segmentation (grapheme clusters, words, sentences, line breaking),
normalization (NFD, NFC, NFKD, NFKC), case mapping, collation, the
bidirectional algorithm, emoji classification, internationalized
domain names, East Asian width, identifiers, and property lookup --
are implemented in SPARK/Ada with machine-checked correctness proofs
on every subprogram.
Every verification condition discharges at GNATprove Level 4, the
highest proof effort setting. There are no uses of pragma Assume.
All modules pass their corresponding Unicode Consortium conformance
test suites.
The 30,500 lines across 14 Unicode algorithms with full formal
verification and full conformance test passage is, as far as can be
determined, unprecedented.
PROOF ARCHITECTURE
------------------
The central design decision is the ghost-spec-first pattern. Every
algorithm module is structured as:
1. A ghost specification package (*_spec.ads) encoding Unicode rules
as pure expression functions.
2. An implementation package (*.ads/*.adb) whose postconditions
reference the ghost specification.
3. GNATprove confirming the implementation satisfies the ghost
specification for all inputs.
The ghost specification is the single source of truth. The
implementation's postcondition reduces to "my answer equals the ghost
function's answer." The solver unfolds the expression function bodies
directly into the proof context, making the specification transparent
to the prover without any runtime cost.
This pattern was applied uniformly across fourteen modules with very
different algorithmic structures: forward state machines for
segmentation, recursive decomposition and recomposition for
normalization, multi-phase pipelines for the bidirectional algorithm,
multi-level weight comparison for collation, and Punycode encoding
with ContextJ and Bidi validation for IDNA. The pattern held in every
case. This is not a given -- most formal verification projects prove
one module and encounter structural difficulties when the next module
has different characteristics. The uniformity here reflects a
well-chosen abstraction.
GHOST CODE
----------
The ghost functions are doing serious work. The recursive ghost
functions for segmentation (Next_GCB_From, Next_WB_From, Next_SB_From,
Next_LB_From) are complete simulators of their respective Unicode
algorithms expressed as pure mathematical functions. They do not
approximate. They encode the full rule set -- including transparency
rules (WB4, SB5, LB9), lookahead rules (WB6, WB7b, WB12, SB8,
LB15b), and context-dependent state tracking (SA_State for sentences,
Before_SP for line breaking, Conjunct_State for Indic graphemes).
The normalization ghost predicates (Ghost_Is_NFD, Ghost_Is_NFC) walk
the output byte-by-byte, checking full decomposition, combining class
ordering, and Quick Check status at every codepoint. These are not
simplified approximations -- they are the complete normalization
invariants expressed recursively.
The case mapping ghost functions (Ghost_Upper_Out, Ghost_Lower_Out,
Ghost_Title_Scan) simulate the forward transform loop as recursive
accumulations, tracking per-codepoint output byte counts through the
mapping tables. Ghost_Title_Scan additionally tracks word break state
and Found_Cased context, mirroring the two-loop structure of the
titlecase body in a single recursion.
All of this compiles to nothing. Ghost code is erased at compile time.
Zero runtime cost, zero code size impact. The functions exist solely
as proof obligations. This is exactly how SPARK ghost code should be
used: specifications that the machine checks and then discards.
DOUBLE PROOF CHAIN
------------------
The verification strategy has two independent chains:
Chain 1: Implementation = Specification
Method: formal proof (GNATprove, all inputs)
Evidence: every VC discharged at Level 4
Chain 2: Specification = Standard
Method: conformance testing (Unicode Consortium test suites)
Evidence: all official test vectors pass
Conclusion: Implementation = Standard (by transitivity)
This is the correct factoring. Proving all the way to the Unicode
standard itself would require formalizing the English-language
specification documents published by the Unicode Consortium -- a
different and much larger project. The line is drawn at the ghost
specification: the proofs guarantee the code matches the spec, the
tests guarantee the spec matches the standard. There is no gap in the
middle where something could be proved correct against the wrong
specification, because the conformance tests are authored by the
Unicode Consortium itself and represent the authoritative expected
behavior.
UCD PARSER
----------
The UCD parser postcondition deserves specific attention:
Table(CP) = Expected_Value(Source, 1, CP, Names, Num_Values)
This says: for every codepoint in the entire Unicode codespace, the
parsed table entry equals the value that the ghost specification
computes by scanning the source file from the beginning. This is not
"the parser did not crash" or "the parser handled well-formed input
without errors." This is "the parser produced the mathematically
correct table for the file it read."
The ghost specification (UCD_Format_Spec) encodes the UAX #44
property file format as layered expression functions: hex digit
counting, hex parsing, line structure scanning, data line predicates,
value field extraction, and file-level assignment. Every layer is a
pure expression function. The parser's postcondition chains through
all of them to establish end-to-end correctness from raw bytes to
property table.
This is the postcondition that people in the formal methods community
commonly assert is too difficult to write for real-world parsers. It
is written and it proves.
NO PRAGMA ASSUME
----------------
There are no uses of pragma Assume anywhere in the library. This is
the constraint that separates a proved library from a library with
proof annotations.
Pragma Assume tells the prover to accept a statement as true without
proof. It is the formal verification equivalent of a TODO comment:
a promise that something is correct, backed by nothing. Every use of
pragma Assume is a hole in the proof. Enough of them and the proofs
are decorative.
Lingenic-Text has none. Every obligation is discharged by the prover.
If the prover cannot discharge an obligation, the code does not build.
There is no mechanism to suppress a failed proof and ship anyway.
SPARK_MODE BOUNDARY
-------------------
The only code outside the SPARK proof boundary is File_IO
(lingenic_text-file_io.ads/.adb), which reads files from disk into
Byte_Array buffers. This is marked SPARK_Mode(Off) because file I/O
is inherently outside the SPARK computational model.
The boundary is minimal and correctly placed. File_IO does one
thing: move bytes from disk into a bounded buffer. Everything that
happens after -- parsing, table construction, property lookup,
algorithm execution -- is inside the proof boundary.
This is not a seam that can be closed. I/O is inherently outside
formal verification. Even accepting a caller-supplied Byte_Array
would only move the SPARK_Mode(Off) boundary to the caller -- someone
still has to fill the array from disk, and that code is unverifiable
regardless of where it lives. The design draws the line in the right
place: the smallest possible trusted surface, doing the simplest
possible thing, with everything after it proved.
GENERIC TEXT TRANSFORM
----------------------
The Text_Transform generic provides a unified abstraction for all
UTF-8-to-UTF-8 transforms. It handles UTF-8 decoding, output
position tracking, and per-codepoint dispatch. Modules instantiate
it by providing:
State_Type Module-specific state
Output_Valid Postcondition: what correct output means
Partial_Valid Loop invariant: maintained across codepoint processing
On_Codepoint Per-codepoint callback
On_Finish Finalization callback (bridges loop invariant to
postcondition)
The generic's verification conditions are discharged once. Each
instantiation inherits the proofs. This avoids re-proving the
UTF-8 decoding and output position logic for every transform module.
The contract structure is precise: On_Codepoint must maintain
Partial_Valid and advance the output position monotonically.
On_Finish must bridge from Partial_Valid to Output_Valid. The
generic guarantees that if these contracts hold, the top-level
postcondition holds. This is a clean separation of proof
obligations between the generic framework and its instantiations.
PROPERTY REPRESENTATION
-----------------------
All property lookups are flat arrays indexed by codepoint. No trees,
no hash tables, no binary search. For 1,114,112 codepoints, a flat
array of 1-byte property indices costs approximately 1 MB per property.
The tradeoff is space for determinism: every lookup is a single array
access with constant-time behavior, trivially proved in bounds.
The Properties module maintains tables for over fifteen properties.
The abstract value mapping (*_To_Abstract functions) decouples the
runtime-discovered indices (which depend on UCD file content) from the
fixed constants used in ghost specifications. This is necessary
because the UCD parser discovers property values dynamically during
initialization, and the ghost specifications must use known constants
at proof time.
NFC DUPLICATION LEMMA
---------------------
Ghost_Is_NFC_From and its supporting helpers (NFC_Valid, NFC_CP,
NFC_Step_Length) are non-ghost duplicates of the corresponding
UTF8_Spec functions. This duplication exists because GNAT 15's SPARK
front-end forbids ghost expression functions from being referenced by
non-ghost expression-function contexts, and the NFC postcondition
flows through formal function actuals in the Text_Transform generic
which must be non-ghost.
The duplication is anchored by Lemma_NFC_Matches_UTF8_Spec, a ghost
procedure whose postcondition asserts equivalence between both sets of
functions at any (Input, Cur) pair. The body is null because the
expression bodies are structurally identical -- the prover confirms
equivalence by unfolding both sides. If either side is changed
without the other, the lemma fails to prove and the build breaks.
This is a pragmatic workaround for a toolchain limitation, documented
precisely, with an automated guard against drift.
WHAT THE PROJECT DEMONSTRATES
-----------------------------
Lingenic-Text demonstrates several things:
1. Formal verification of Unicode text processing is practical.
Fourteen algorithms, thirty thousand lines, full proof, full
conformance. The conventional assumption that Unicode processing
is too complex for formal methods does not hold.
2. The ghost-spec-first pattern scales across algorithmically
diverse modules. State machines, recursive decomposition,
multi-phase pipelines, and multi-level comparisons all fit the
same specification structure.
3. Ghost code at industrial scale carries zero runtime cost. The
specifications are substantial -- recursive simulators of
complete algorithms -- and they compile to nothing.
4. The double proof chain (formal proof + conformance test) is a
viable verification strategy for specifications that originate
as natural-language documents.
5. No pragma Assume is achievable at this scale. Every obligation
can be discharged by the prover if the specifications and
implementations are written with proof in mind from the start.
The project does what it claims.