Lingenic-Text C Library

C bindings for Lingenic-Text, the formally verified Unicode 17.0 text processing library. The full library surface — UTF-8, segmentation, normalization, case mapping, collation, the bidirectional algorithm, East Asian width, emoji, identifiers, IDNA, and property lookup — is exported as 53 plain C functions in a single static library.

Design

The binding is a thin validation shim over the proved SPARK/Ada core:

• The core is proved. Every subprogram in src/ carries GNATprove-verified contracts: 9,214 verification conditions, 0 unproved, no pragma Assume. Runtime checks in the core are suppressed (-gnatp) because the prover has established their absence.
• The shim validates. Every C entry point checks its arguments against the precondition of the proved subprogram it calls — null pointers, zero lengths, out-of-range positions, uninitialized modules. Violations return LT_ERR (−1) instead of invoking the core. The shim itself is compiled with runtime checks and a catch-all exception handler, so no Ada exception can propagate into C.

This means the proof guarantees of the core hold for every call that crosses the C boundary: if the shim accepts your arguments, the core's preconditions are satisfied, and its postconditions — proved for all inputs — apply to the result.

Why a Binding, Not a Port

The C API is deliberately a binding to the verified Ada objects — not a translation of the library into C source. This is what preserves the guarantee.

GNATprove verifies the SPARK source against SPARK semantics, and GNAT compiles that same source directly into the archive you link. The chain is: proved source → compiler → shipped object code. C callers execute exactly the code that was verified.

A C translation — whether generated by a tool or written by hand — would insert unverified steps into that chain:

• A translator would become part of the trusted computing base. No open-source Ada→C path exists (FSF GNAT has no C backend), and any translator is itself unverified.
• A second compilation would reinterpret the code under C semantics. Ada and C differ on overflow, aliasing, and object lifetime; the proofs discharged the core's runtime checks against Ada semantics, which is what makes -gnatp sound. After translation, that argument has a gap.
• A hand-written port would discard the proofs entirely and be just another unverified C Unicode library.

Distribution concerns have better answers that stay on the verified path: consumers of prebuilt archives need only a C compiler, this header, liblingenic_text_c.a, and the GNAT runtime — no Ada toolchain and no Ada knowledge.

Artifacts

Building

Requires GNAT 15+ and GPRBuild 25+. On macOS, set up the environment first:

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

Then build:

gprbuild -P lingenic_text_c.gpr -p -j0

This produces lib-c/liblingenic_text_c.a. Because the project is a standalone library, gprbuild generates two elaboration entry points for C callers: lingenic_text_cinit (run Ada elaboration, call once before anything else) and lingenic_text_cfinal (optional finalization at shutdown).

Linking

Link the static library plus the GNAT runtime:

cc your_program.c -Iinclude -Llib-c -llingenic_text_c -lgnat

macOS note: -lgnat resolves to libgnat-15.dylib, which is built with @rpath install names and will fail to load at runtime unless you configure rpaths. The simplest fix is to link the static GNAT runtime archive directly by path:

ADALIB="$HOME/.local/share/alire/toolchains/gnat_native_15.1.2_60748c54/lib/gcc/aarch64-apple-darwin23.6.0/15.0.1/adalib"
cc your_program.c -Iinclude -Llib-c -llingenic_text_c "$ADALIB/libgnat.a"

Quick Start

#include <lingenic_text.h>
#include <stdio.h>
#include <string.h>

int main(void)
{
    lingenic_text_cinit();                 /* Ada elaboration, once */

    if (lt_init("ucd") != 0) {             /* load UCD data tables  */
        fprintf(stderr, "UCD load failed\n");
        return 1;
    }

    /* NFC-normalize "e" + combining acute -> U+00E9 */
    const uint8_t in[] = { 'e', 0xCC, 0x81 };
    uint8_t out[16];
    size_t  out_len;
    if (lt_normalize(LT_NFC, in, sizeof in, out, sizeof out, &out_len) == 0)
        printf("NFC: %zu bytes\n", out_len);    /* 2 bytes: C3 A9 */

    /* Collate two strings (UTS #10, shifted weighting) */
    int cmp;
    lt_collate((const uint8_t *)"apple", 5,
               (const uint8_t *)"Apple", 5,
               LT_COLLATE_SHIFTED, &cmp);
    printf("apple %s Apple\n", cmp < 0 ? "<" : cmp > 0 ? ">" : "=");

    /* Iterate grapheme cluster boundaries */
    const uint8_t *text = (const uint8_t *)"héllo";
    size_t len = strlen((const char *)text);
    for (size_t pos = 0, next; pos < len; pos = next)
        if (lt_next_grapheme_break(text, len, pos, &next) != 0)
            break;

    lingenic_text_cfinal();
    return 0;
}

lt_init takes the path of the Unicode Character Database directory (the one holding UnicodeData.txt, allkeys.txt, ...). It returns 0 on success or the number of the stage that failed: 1 = properties, 2 = normalization, 3 = emoji, 4 = idna, 5 = bidi, 6 = case mapping, 7 = collation.

Conventions

• Buffers are UTF-8. All text parameters are const uint8_t * + size_t byte length. Nothing is NUL-terminated (except the char * outputs of lt_script_name / lt_general_category_name and the char * input of lt_init).
• Offsets are 0-based byte offsets, C-style. (The Ada core is 1-based; the shim translates.)
• Errors are return codes. LT_ERR (−1) always means invalid arguments or a required module not initialized. Transform functions additionally return 1 = output buffer too small and 2 = invalid UTF-8 input — retry with a larger buffer or fix the input, respectively.
• The caller owns all memory. The library never allocates on behalf of the caller and never retains pointers past the call; every function copies in and copies out.
• Threading. Initialization (lingenic_text_cinit, lt_init) must complete before any other call and must not run concurrently. After initialization all lt_* functions only read the loaded tables and use local state, so they may be called from multiple threads concurrently.

Testing

The smoke test exercises every module through the C API (106 checks). Run it from the repository root so the ucd path resolves:

cc tests/c/smoke_test.c -Iinclude -Llib-c -llingenic_text_c \
   "$ADALIB/libgnat.a" -o tests/c/smoke_test
./tests/c/smoke_test ucd

Expected output ends with 106 checks, 0 failures.

Documentation

The complete function-by-function reference is in docs/C_API_GUIDE.txt. The underlying Ada contracts — the actual proved specifications — are in docs/API_REFERENCE.txt.