LINGENIC-TEXT
=============
The First Formally Verified Unicode Text Processing Library

Version:  1.2.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.2.0)
  CHANGELOG.md               Version history

  src/                       57 Ada source files (~32,200 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.