Documentation Index

Complete documentation for liblevenshtein-rust v4.0.0-rc.4 — Levenshtein and related (phonetic, time-series) automata for error-tolerant search over strings and byte arrays, with several trie/DAWG dictionaries, fuzzy maps, and fuzzy caches.

Last Updated: 2026-08-24 · Version: 4.0.0-rc.4

---

How this documentation is organized

The set is grouped into nine sections, from first-contact tutorials through deep theory, formal proofs, and the project's scientific research record. The main README is the canonical, quality-reference overview; this index maps everything else.

Document conventions

• Math is written as MathJax LaTeX, never as Unicode literals. Inline math is a backtick code span whose content is dollar-delimited — `$\mathcal{O}(\lvert W\rvert)$` renders as $\mathcal{O}(\lvert W\rvert)$ — and display math is a fenced block whose info-string is math. We never use bare dollar-delimited math (dollars without the enclosing backticks): GitHub's CommonMark pass strips backslash escapes before MathJax parses them. Cardinality and absolute-value bars are \lvert … \rvert; a literal ASCII | is reserved for Markdown table delimiters and code. Genuine algorithm listings stay as fenced pseudocode (literate form); only standalone formulae, recurrences, and inference rules become math blocks.
• Diagrams live under diagrams/ as text source + a committed SVG, fully coloured per a shared legend; docs embed the SVG.
• Citations link to DOIs where one exists.

Living vs. Historical — the rule that bounds edits

A document is LIVING if it describes the current behaviour, API, theory, or architecture of liblevenshtein v4.0.0-rc.4 — something you would consult to use or extend the library today. A document is HISTORICAL if it is a dated record of how we got here: a scientific ledger, hypothesis log, experiment record, phase/session/completion report, or benchmark dump. Per the project's append-only scientific-method practice, HISTORICAL documents are never rewritten or "cleaned up" — only indexed and cross-linked. When in doubt, a doc whose path carries a date, phase, hypothesis, or session name is HISTORICAL.

---

1 · Getting Started

• Main README — overview, installation, quick start, the full feature tour.
• User Guide → Getting Started — first dictionary and query.
• CHANGELOG — version history (current: 0.10.0).
• Examples & Tutorials — the numbered tutorial series (01 … 08) and a map to the runnable examples/*.rs.

2 · Concepts & Theory

• Lazy vs. Eager Automata — the central idea: a query lazily simulates a parameterized Levenshtein automaton, it is not a precompiled universal DFA.
• Levenshtein-automata theory — the Schulz–Mihov method, glossary, and code-to-paper mapping (theory home; also cross-linked from the glossary).
• Algorithm layer 02 — Levenshtein automata — the position/subsumption model, with diagrams.
• Edit-distance classification — the alignment/script boundary, four implementation classes, metricity-versus-pruning distinction, and placement checklist for future measures.
• Snapshot semantics — the cursor laws S1-S6 as display math, the $\mathcal{O}(1)$-capture argument from path-copied revisions, the partial-persistence classification (Driscoll; Okasaki), and the law ↔ formal-model ↔ test correspondence table.
• Theory — disk-trie and SCDAWG theory pointers (backend internals now live in libdictenstein).
• Specialized theory: universal automata · weighted automata · bimachines.

3 · Architecture

• Architecture Overview — the inter-crate view: liblevenshtein ↔ libdictenstein ↔ optional duallity (WFST) ↔ the .llev/.llre DSL layer.
• Language-bindings architecture — the three-layer binding decision (versioned C resource ABI + generated constants + hand-written facades), the shared VtResource boundary, snapshot/marshalling contracts, tiers, distribution, and platform policy.
• Binding documentation hub — the corpus map and reading order: the llev_* C-ABI reference (all 35 functions, status sets, the lease protocol, a compile-checked C consumer), the resource consumer (intake, CallGate, fault channel, arenas), the WASM/JS topology (umbrella runtime, identity guard, WASI preopens), and the machine-readable governance (bindings/api.json, conformance fixtures, ABI_INVARIANTS.tsv).
• Family ABI canon (hosted with the interop crate): portal · ABI reference · evolution policy · security model.
• Developer Guide → Architecture — the intra-crate module design and traits.
• Design specifications — feature-level designs, including Class-A presets, the ordered cost monoid, language products, dynamic DAWG, suffix automaton, contextual completion, protobuf serialization, and grammar correction.
• Algorithm Reference layers 01–09 — the layered architecture, bottom-up.
• Diagrams: crate boundary · component stack · C4 context / container · feature-flag DAG · module dependencies.

4 · User Guide

• User Guide — getting-started, algorithms, backends, serialization, features, code completion, thread safety, prefix zipper.
• Guides — articulatory distance, compositional phonetic + Levenshtein, phonetic-rules developer guide, hierarchical scope completion, restricted substitutions, grammar correction.
• Phonetic extraction — Soundex, Metaphone, NYSIIS, Caverphone, Cologne, Daitch–Mokotoff, Beider–Morse.
• DSL grammar reference — the .llev, .llre, and regex EBNF grammars with prose.
• LLRE reference.

5 · Developer Guide

• Developer Guide — building, contributing, performance, publishing.
• Migration to the split CLI — the v0.10 package and API boundary.
• Security & threat model — untrusted-input surfaces (FFI/WASM boundaries, serialization, .llre parsing).
• Binding trust model — the family trust model instantiated for the resource consumer: boundary() containment, the bounded error channel, the decoded status wire, lease refusal as use-after-free prevention, and duty status per hostile-input class.
• Releasing language bindings — the publish-order DAG, registry coordinates and credentials, pin-coherence preconditions, and pre-publication gates.
• Release evidence ledgers — immutable source commits, workflow runs, registry digests, public-byte smokes, incidents, and recovery decisions; start with the 4.0.0-rc.4 ledger.
• Resource-exhaustion controls — automaton state ceilings, edit budgets, elastic-DP guards, and deployment policy.
• Automaton-variant security — continuation-tag integrity, subsumption soundness, selector stability, and extension review controls.
• Migration — terminology and version-migration notes (including the libdictenstein extraction).
• Development logs — phase/session implementation logs (historical).

6 · Algorithm Reference

• Algorithm Reference — the documentation index, layers 01 dictionary through 09 value storage, the 10 affine-gap automaton, 13 language products, and the 14 exact generalized-operation grid.

7 · Formal Verification

• Verification — the formal-proof artifacts. FORMAL_VERIFICATION_MANIFEST.tsv is the declared source of truth for trusted/partial/legacy status; see INDEX and README_FORMAL_GATES. The trusted CostMonoid island combines Rocq, Verus, cross-solver SMT, and property tests; the tree also holds the remaining Rocq and TLA+ models.
• Formal-verification writeups — the parallel markdown proof exposition and findings (defers to the manifest for canonical status).

8 · Research & Scientific Ledgers — historical, append-only (indexed, not edited)

The project keeps an append-only scientific record. These are preserved as written; they are indexed and cross-linked but never rewritten.

• Research — per-topic investigations: levenshtein-automata, universal-levenshtein, weighted-levenshtein-automata, wallbreaker, artrie, simd-optimization, comparative-analysis, bimachines, eviction-wrapper, grammar-correction, phonetic-corrections, batch-processing.
• Scientific ledgers — the canonical ledger home (automata/WFST evaluation, MSM automata evaluation).
• Optimization journals and optimization results — hypothesis ledgers (H1/H2…), per-topic experiment logs.
• Universal · Generalized — phase records for the universal & generalized automaton work.
• MeTTaIL — semantic type-checking for MeTTa (a large self-contained subtree: theoretical foundations, correction-WFST, simplification, implementation, ecosystem).
• Time-series analysis · Integration (MORK, PathMap) · Benchmarks · Analysis · Bug reports · Completion reports · Implementation status · Archive.

9 · Diagrams

• Diagram suite & style guide — fully coloured diagrams (text source + committed SVG) built with PlantUML, Graphviz, D2, Structurizr, Pikchr, and Asymptote, with a shared colour legend and a reproducible render pipeline.

---

Glossary

• Technical Glossary — implementation, performance, and user-facing terms.
• Levenshtein-automata theory glossary — Position, Subsumption, Characteristic Vector, and other theoretical terms.

---

Navigation: ← Main README · User Guide · Developer Guide · Algorithm Reference · Diagrams