# LOL i18n Service — ABI/FFI/API Triple Documentation

## Overview

The LOL (Language of Languages) i18n service follows the **Hyperpolymath ABI/FFI/API Triple Standard**:

- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs
- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility
- **API** exposed via a **Zig** gateway (REST/gRPC/GraphQL) for idiomatic high-level access

LOL is always called as a service, never embedded. Consumers initialise with
`lol_init()`, perform translation lookups and plural form selection across
1500+ languages, then clean up with `lol_free()`.

> **Note:** V-lang was the previous API layer and was banned estate-wide on 2026-04-10.
> The sidelined V-lang wrappers under `api/v-lol/` and `api/v-gateway/` remain only
> for historical reference. See their respective `MIGRATION.adoc` files for details.

## Architecture

```
┌─────────────────────────────────────────────────┐
│  ABI Definitions (Idris2)                       │
│  src/abi/                                       │
│  - Types.idr           (Result, Handle, enums)  │
│  - Layout.idr          (Memory layout proofs)   │
│  - Locale.idr          (BCP-47 validated locale) │
│  - TranslationKey.idr  (Type-safe key proofs)   │
│  - PluralForm.idr      (CLDR rules + coverage)  │
│  - I18nStore.idr       (Store interface + proofs)│
│  - Foreign.idr         (FFI declarations)       │
└─────────────────┬───────────────────────────────┘
                  │
                  │ generates
                  ▼
┌─────────────────────────────────────────────────┐
│  C Headers (auto-generated)                     │
│  generated/abi/lol.h                            │
│  - lol_result_t, lol_plural_category_t          │
│  - lol_locale_t, lol_translation_result_t       │
│  - lol_language_info_t, lol_plural_rule_t       │
│  - All function prototypes                      │
└─────────────────┬───────────────────────────────┘
                  │
                  │ implemented by
                  ▼
┌─────────────────────────────────────────────────┐
│  FFI Implementation (Zig)                       │
│  ffi/zig/src/                                   │
│  - main.zig    (C ABI exports, service state)   │
│  - locale.zig  (BCP 47 parse, validate, norm)   │
│  - store.zig   (HashMap store, fallback chains) │
│  - plural.zig  (CLDR plural rule engine)        │
│  - ffi.zig     (Module re-exports, FFI index)   │
└─────────────────┬───────────────────────────────┘
                  │
                  │ linked by (-llol)
                  ▼
┌─────────────────────────────────────────────────┐
│  Zig API Gateway (REST/gRPC/GraphQL)            │
│  api/zig-gateway/src/                           │
│  - main.zig      (HTTP gateway, triple endpoints,│
│                   REST 7800 / gRPC 7801 / GQL    │
│                   7802; REST+gRPC+GraphQL         │
│                   handlers; domain I/O)          │
│  - types.zig     (public domain types; replaces  │
│                   v-lol/src/types.v)             │
│  - lol_ffi.zig   (Zig wrapper around liblol;    │
│                   replaces v-lol/src/lol.v +     │
│                   ffi.v)                         │
└─────────────────────────────────────────────────┘
```

## Directory Structure

```
lol/
├── src/
│   └── abi/                         # ABI definitions (Idris2)
│       ├── Types.idr                # Core types with formal proofs
│       ├── Layout.idr               # Memory layout verification
│       ├── Locale.idr               # BCP-47 locale with validation proofs
│       ├── TranslationKey.idr       # Type-safe translation key proofs
│       ├── PluralForm.idr           # CLDR plural rules + coverage proofs
│       ├── I18nStore.idr            # Store interface with lookup proofs
│       └── Foreign.idr              # FFI function declarations
├── ffi/
│   └── zig/                         # FFI implementation (Zig)
│       ├── build.zig                # Build configuration
│       ├── src/
│       │   ├── main.zig             # C ABI exports + service state
│       │   ├── locale.zig           # Locale parse/validate/normalise
│       │   ├── store.zig            # Translation store with fallback
│       │   ├── plural.zig           # CLDR plural rule engine
│       │   └── ffi.zig              # Module re-exports + FFI index
│       └── test/integration_test.zig# Integration tests
├── generated/
│   └── abi/
│       └── lol.h                    # Auto-generated C header
├── api/
│   ├── zig-gateway/                 # Canonical API gateway (REST/gRPC/GraphQL)
│   │   ├── build.zig                # Build configuration (links liblol)
│   │   └── src/
│   │       ├── main.zig             # HTTP gateway: REST/gRPC/GraphQL handlers + domain I/O
│   │       ├── types.zig            # Public domain types (replaces v-lol/src/types.v)
│   │       └── lol_ffi.zig          # Zig liblol wrapper (replaces v-lol/src/lol.v + ffi.v)
│   ├── v-lol/                       # DEPRECATED — see MIGRATION.adoc
│   │   ├── v.mod
│   │   └── src/
│   └── v-gateway/                   # DEPRECATED — see MIGRATION.adoc
│       └── src/
└── ABI-FFI-README.md                # This file
```

## Key Types

| Type | Idris2 | C |
|------|--------|---|
| Result codes | `Result` | `lol_result_t` |
| Plural category | `PluralCategory` | `lol_plural_category_t` |
| Locale | `Locale` | `lol_locale_t` |
| Translation | `TranslationResult` | `lol_translation_result_t` |
| Language info | `LanguageInfo` | `lol_language_info_t` |
| Plural rule | `PluralRule` | `lol_plural_rule_t` |

## Formal Proofs (Idris2 ABI)

The Idris2 ABI layer provides the following compile-time guarantees:

1. **Result code round-trip**: `resultFromInt (resultToInt r) = Just r` for all `r`
2. **Plural category round-trip**: `pluralFromInt (pluralToInt p) = Just p` for all `p`
3. **Result code injectivity**: distinct results map to distinct integer codes
4. **Handle non-null**: the `Handle` type cannot wrap a null pointer (enforced by `So`)
5. **Struct alignment**: all C struct layouts are proven to have correctly aligned fields
6. **Plural form count bounds**: `PluralRule.formCount` is proven to be in range 1-6
7. **BCP-47 validation**: `ValidLocale` proves tag structure at construction (Locale.idr)
8. **Translation key validity**: `ValidKey` proves non-empty dot-separated segments (TranslationKey.idr)
9. **Plural coverage**: `eastAsianPluralConstant` proves East Asian always returns Other (PluralForm.idr)
10. **Plural FFI bounds**: `pluralToIntBounded` proves category integers stay in 0-5 range
11. **Store lookup guarantee**: `CorrectStore` interface proves key-exists implies non-empty result (I18nStore.idr)
12. **Fallback chain contract**: `lookupWithFallback` walks chain with locale/key pair, resolves or returns Nothing

No `believe_me`, `assert_total`, or other escape hatches are used.

## Building

### Idris2 ABI

```bash
idris2 --check lol-abi.ipkg   # Type-check all ABI definitions and proofs
idris2 --build lol-abi.ipkg   # Build (optional, ABI is specification-only)
```

### Zig FFI

```bash
cd ffi/zig
zig build              # Builds liblol.so and liblol.a
zig build test         # Runs unit tests
zig build test-integration  # Runs integration tests
```

### Zig API Gateway

```bash
cd api/zig-gateway
zig build
./zig-out/bin/lol-gateway
```

Default base port is 7800. Configure via `LOL_PORT` environment variable.
Corpus data directory defaults to `corpus`; set via `LOL_DATA_DIR`.

## Usage (Zig gateway, HTTP)

The Zig API gateway exposes three endpoint families:

**REST API** (HTTP on port 7800):
```bash
curl http://localhost:7800/api/v1/languages
curl http://localhost:7800/api/v1/corpus/stats
```

**gRPC JSON-compatible** (on port 7801):
```bash
curl -X POST http://localhost:7801/lol.TranslationService/Translate \
  -H "Content-Type: application/json" \
  -d '{"locale":"en-US","key":"app.greeting"}'
```

**GraphQL** (on port 7802, endpoint `/graphql`):
```bash
curl -X POST http://localhost:7802/graphql \
  -H "Content-Type: application/json" \
  -d '{"query":"{ languages { code name } }"}'
```

## License

SPDX-License-Identifier: MPL-2.0

Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
