• API_REFERENCE ⤓ .txt 2026-05-17T174625.000 000000000157096
  Complete public API for Lingenic-Text, organized by module. All types and subprograms are listed with their contracts.
• ARCHITECTURE ⤓ .txt 2026-05-17T173427.000 000000000091680
  Everything lives under the root package Lingenic_Text. Child packages are named Lingenic_Text.<Module> with an optional _Spec suffix for ghost specifications.
• BIDI ⤓ .txt 2026-07-15T070903.000 000000000079088
  Standard: UAX #9 (Unicode Bidirectional Algorithm) Files: src/lingenic_text-bidi_spec.ads (ghost specification) src/lingenic_text-bidi.ads (public API) src/lingenic_text-bidi.adb (implementation) src/lingenic_text-bidi_brackets_spec.ads (BidiBrackets ghost spec) src/lingenic_text-bidi_brackets_spec.adb (opaque wrapper bodies) src/lingenic_text-bidi_brackets_parser.ads (proved parser API) src/lingenic_text-bidi_brackets_parser.adb (proved parser body)
• BUILDING ⤓ .txt 2026-05-17T173427.000 000000000048888
  GNAT 15.1.2 or later Ada 2022 compiler GPRBuild 25.0.1 or later Project-based build system GNATprove 15.1.0 or later SPARK formal verifier
• C_API_GUIDE ⤓ .txt 2026-07-15T071046.000 000000000187552
  Header: include/lingenic_text.h Library: lib-c/liblingenic_text_c.a (build: gprbuild -P lingenic_text_c.gpr) Test: tests/c/smoke_test.c (106 checks, all modules)
• CASE_MAPPING ⤓ .txt 2026-05-17T174005.000 000000000054376
  Standard: Unicode Standard, Section 3.13 Files: src/lingenic_text-case_mapping_spec.ads (ghost specification) src/lingenic_text-case_mapping.ads (public API) src/lingenic_text-case_mapping.adb (implementation)
• COLLATION ⤓ .txt 2026-05-17T174006.000 000000000047144
  Standard: UTS #10 (Unicode Collation Algorithm) Files: src/lingenic_text-collation_spec.ads (ghost specification) src/lingenic_text-collation.ads (public API) src/lingenic_text-collation.adb (implementation)
• EAW_AND_IDENTIFIERS ⤓ .txt 2026-05-17T174255.000 000000000031752
  Standard: UAX #11 (East Asian Width) Files: src/lingenic_text-eaw_spec.ads (ghost specification) src/lingenic_text-eaw.ads (public API) src/lingenic_text-eaw.adb (implementation)
• EMOJI ⤓ .txt 2026-05-17T174254.000 000000000049448
  Standard: UTS #51 (Unicode Emoji) Files: src/lingenic_text-emoji_spec.ads (ghost specification) src/lingenic_text-emoji.ads (public API) src/lingenic_text-emoji.adb (implementation)
• IDNA ⤓ .txt 2026-05-17T174255.000 000000000061440
  Standard: UTS #46 (Unicode IDNA Compatibility Processing) RFC 3492 (Punycode), RFC 5892 (IDNA), RFC 5893 (Bidi for IDNA) Files: src/lingenic_text-idna_spec.ads (ghost specification) src/lingenic_text-idna.ads (public API) src/lingenic_text-idna.adb (implementation)
• NORMALIZATION ⤓ .txt 2026-05-17T174005.000 000000000063320
  Standard: UAX #15 (Unicode Normalization Forms) Files: src/lingenic_text-normalization_spec.ads (ghost specification) src/lingenic_text-normalization.ads (public API) src/lingenic_text-normalization.adb (implementation)
• OVERVIEW ⤓ .txt 2026-07-15T070809.000 000000000036688
  Version: 1.2.0 Standard: Unicode 17.0 Language: SPARK/Ada (Ada 2022)
• PROPERTIES ⤓ .txt 2026-05-17T173646.000 000000000044880
  Standard: UAX #44 (Unicode Character Database) Files: src/lingenic_text-properties_spec.ads (ghost: Joining_Type values) src/lingenic_text-properties.ads (public API) src/lingenic_text-properties.adb (implementation)
• SEGMENTATION ⤓ .txt 2026-05-17T174005.000 000000000076104
  Ghost _Spec encodes individual rules as expression functions 2. Ghost recursive function simulates the complete algorithm 3. Implementation is a forward state machine 4. Postcondition: implementation output = ghost recursive function
• TECHNICAL_REVIEW ⤓ .txt 2026-07-15T071056.000 000000000096960
  Project: Lingenic-Text v1.2.0 Scope: Unicode 17.0 text processing library Language: SPARK/Ada (Ada 2022) Scale: 57 source files, ~32,200 lines, 14 algorithm modules Method: Formal verification (GNATprove Level 4), conformance testing
• TESTING ⤓ .txt 2026-05-17T174446.000 000000000055744
  Conformance tests form the second chain in the double proof chain. While formal proofs verify that the implementation matches the ghost specification, conformance tests verify that the ghost specification correctly encodes the Unicode standard.
• UCD_PARSER ⤓ .txt 2026-07-15T053912.000 000000000087952
  Standard: UAX #44 Section 4.2 Files: src/lingenic_text-ucd_format_spec.ads (ghost specification) src/lingenic_text-ucd_parser.ads (public API) src/lingenic_text-ucd_parser.adb (implementation) src/lingenic_text-scx_parser.ads (Script_Extensions parser) src/lingenic_text-scx_parser.adb (Script_Extensions implementation) src/lingenic_text-bidi_brackets_spec.ads (BidiBrackets ghost spec) src/lingenic_text-bidi_brackets_spec.adb (opaque wrapper bodies) src/lingenic_text-bidi_brackets_parser.ads (BidiBrackets parser API) src/lingenic_text-bidi_brackets_parser.adb (BidiBrackets parser body) src/lingenic_text-file_io.ads (file I/O) src/lingenic_text-file_io.adb (file I/O implementation)
• UTF8 ⤓ .txt 2026-05-17T173645.000 000000000052048
  Standard: RFC 3629 Files: src/lingenic_text-utf8_spec.ads (ghost specification) src/lingenic_text-utf8.ads (public API) src/lingenic_text-utf8.adb (implementation)
• VERIFICATION ⤓ .txt 2026-07-15T070845.000 000000000111064
  GNATprove is the SPARK formal verification tool. It uses the Why3 intermediate verification framework and calls SMT solvers (CVC5, Z3, Alt-Ergo) to discharge verification conditions.