libdictenstein documentation

This is the documentation index for libdictenstein — a toolbox of high-performance dictionary data structures (tries, DAWGs, double-array tries, suffix automata, SCDAWGs, and a lock-free durable persistent ARTrie family), unified behind one trait API and backed by machine-checked proofs.

New here? Start with the root README.md for the crate overview and the backend selector, then come back here for depth.

---

Documentation map

The docs are organized along a single axis: theory (paper-grounded math and data-structure foundations) → algorithms (per-backend implementation and usage) → architecture / persistence (cross-cutting systems) → formal verification (the proofs that pin the concurrency and durability claims), with benchmarks, experiments, and design records alongside.

Area	Path	What's there
🧮 Theory	theory/	Data-structure foundations: disk-tries (trie → B-trie → ART → persistent ART → buffer management), SCDAWG (suffix automaton → CDAWG → symmetric compact DAWG), and volatile automata (DAWG minimization, double-array tries, Bloom filters, bit-parallel child scan). Paper-grounded, with proofs.
⚙️ Algorithms	algorithms/	The dictionary-layer trait API and a per-backend deep-dive for each implementation (implementations/). Conceptual guides: zippers (lazy set-algebra), serialization (bincode/protobuf binary persistence + value-preserving bincode), persistent suffix graphs (durable substring indexes), native u64 + CX (u64-sequence profile + compact snapshot), and the vocab trie (term ↔ u64 bijection).
🏗️ Architecture	architecture/	Cross-cutting system design: the core abstractions (CharUnit + KeyEncoding — one code path, three alphabets), the in-memory dictionary architecture (monomorphized cores + the two lock-free strategies), the optimization roadmap, and the persistence family overview.
📖 User guide	user-guide/	Task-oriented usage: getting started, choosing a backend, the in-memory tour, and the cookbook.
💾 Persistence	persistence/	The durable, lock-free ARTrie engine end-to-end. Start at the architecture entry point, then descend: the reusable durable-storage kernel, the families, the lock-free overlay, durability & recovery, the concurrency model, storage backends + WAL format, eviction, group commit, and the proof map.
♻️ Eviction	persistence/eviction.md	The memory-pressure eviction subsystem for the persistent ARTrie (part of the persistence corpus).
🔌 Integration	integration/	Backend integrations (e.g. PathMap).
🔗 Bindings / C ABI	bindings/	The producer contract corpus: the ldict_* C-ABI reference (all 41 functions, status/kind/capability tables, per-backend matrix, verified C example), the resource-producer architecture (vt.dictionary.v1 production, O(1) snapshot capture, node-id leasing, retain ledger), the native collection quick reference, the FFI boundary analysis, and the findings ledger. The machine-readable ABI model is ../bindings/api.json, enforced by ../scripts/check-bindings.py (CI job binding-contract).
📊 Benchmarks	benchmarks/	Scientific-method benchmarking ledgers and artifacts, including the collection traversal and language-binding protocol.
🧪 Experiments	experiments/	Per-optimization experiment ledgers (persistence enhancements, loading, lock-free flip).
📐 Design	design/	Architecture/mechanism design records and the historical campaign ledger.
✅ Formal verification	../formal-verification/	Rocq theorems + TLA⁺ models + the CI-gated unsafe contract inventory.
🔒 Security	security/	Threat model, untrusted-input / DoS analysis, deserialization safety, and the unsafe-contract map.
🛠️ Engineering	engineering/	Testing strategy, benchmarking methodology, and the feature-flag reference.
🚢 Release engineering	releasing.md	Immutable-tag validation, one-registry dispatch, artifact evidence, npm promotion, and failure recovery.
🎨 Diagrams	diagrams/	Diagrams-as-code sources and rendered SVGs; see diagrams/README.md for the rendering pipeline.

---

Suggested reading order

The map below renders the reading paths as a graph: follow an edge from its tail to its head. The green spine is the on-ramp (crate README → trait layer → per-backend guide); from there you branch into the grey theory track, the blue persistence / systems track, and finally the amber formal verification track. It is split across two figures — part 1 covers the getting-started and theory tracks, part 2 the persistence and formal tracks; the three "go deeper" edges that cross between them are drawn as a → see part 2 note in part 1 and re-attached from a ← from part 1 note in part 2.

1. Pick a backend — root README.md selector + user-guide/backends.md.
2. Understand the trait layer — algorithms/README.md.
3. Go deep on your backend — the matching file under algorithms/implementations/, with its theory back-link into theory/.
4. If you need durability — theory/disk-tries/ for the foundations, then persistence/ and architecture/persistence/ for the system.
5. If you need to trust it — ../formal-verification/.

The query half of approximate string matching — a Levenshtein-automaton transducer that walks any of these dictionaries — lives in the companion crate liblevenshtein. libdictenstein contains no fuzzy-matching code itself.

---

Authoring conventions — math in Markdown

Prose math is MathJax; diagram labels use PlantUML-LaTeX (<latex> / <math>). Which delimiters you use is not cosmetic — GitHub corrupts the obvious ones.

This section is the authority on delimiters — the characters that wrap a math span. For which LaTeX goes inside a span and which word names each concept, see the notation & terminology register. In particular, a length bar is \lvert x \rvert (never \mid), and big-O is inline math, never a code span.

Before handing a math span to MathJax, GitHub's Markdown pass runs CommonMark backslash-escape processing over the span's interior. Inside $…$ and $$…$$ that rewrites \_→_, \{→{, \}→}, \;→;, \,→,, \#→#. The damage comes in two flavours, and the silent one is the dangerous one:

• Loud — a bare _ or # reaches MathJax, which aborts with '_' allowed only in math mode.
• Silent — \max\{\,L\,\} renders as \max{,L,}: the set braces disappear and literal commas replace thin-spaces. No error, wrong mathematics.

Only two forms survive GitHub's escape pass verbatim. Use them:

	Write this	Not this
Inline	$`\text{checkpoint\_lsn}`$	$\text{checkpoint\_lsn}$
Display	a ```math fenced block	$$ … $$
Literal $	inline code — `$₁`	\$₁

Two further rules, both established by rendering probes against GitHub's own GFM endpoint (gh api -X POST /markdown):

1. Never let an ASCII letter abut the opening $`. GitHub declines to open inline math there, so InMem$`\Rightarrow`$descend renders as literal text. Write InMem $`\Rightarrow`$ descend. (A digit or ) before the $ is fine.)
2. Keep literal dollars in inline code. Two or more \$ on one line can pair into a spurious math span — and whether they do is not predictable from the source: {\$, b\$} renders as text while \$₁, \$₂ renders as math.

scripts/check-doc-math.py enforces all four rules over every tracked *.md, and runs in the diagrams CI job. Run it before committing docs:

python3 scripts/check-doc-math.py          # every tracked *.md
python3 scripts/check-doc-math.py FILE…    # just these