Skip to content

README.md

Latest commit

 

History

History
116 lines (92 loc) · 9.91 KB

README.md

File metadata and controls

116 lines (92 loc) · 9.91 KB
Raw

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/JSON/plaintext/protobuf + value-preserving), 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).
📊 Benchmarks benchmarks/ Scientific-method benchmarking ledgers and artifacts.
🧪 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.
🎨 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.

Documentation reading-order map, part 1 of 2 (getting-started and theory tracks): a top-to-bottom directed graph. The green getting-started spine runs crate README → backend selector → user-guide/backends → algorithms/README (trait layer) → algorithms/implementations (per-backend), which branches to zippers and serialization. Teal 'go deeper' edges cross from the trait layer and per-backend guides into the grey theory track (architecture/abstractions, theory/disk-tries, theory/scdawg). The three edges that continue into the persistence and formal tracks terminate at a 'see part 2' note.

Documentation reading-order map, part 2 of 2 (persistence and formal tracks): a top-to-bottom directed graph continuing from part 1. A 'from part 1' note re-attaches the three cross-track edges into the blue persistence track (architecture/persistence + storage-backends), which fans out to native-u64-and-cx, vocab-trie, persistent-suffix-graphs, the WAL format reference, and eviction. The persistence track finally points into the amber formal-verification track (Rocq theorems, TLA+ models, unsafe-contract inventory).

  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