Database-theory + practice gap analysis (22 areas, 5 theory frontiers)

[hyperpolymath]

Background

Audit on 2026-06-01 mapping what VeriSimDB has, what it lacks vs DB theory + current practice, and where the octad gives it unique opportunities. Owner directive: identify functionality missing or extensible from DB theory or its bridges, then drive it.

22 area assessment

1. Transactions / concurrency — MVCC + optimistic OCC labelled as Serializable; no real SSI, no Calvin-style cross-peer commit. CRIT / XL.
2. Indexing — HNSW + tantivy + Oxigraph + redb + r-tree feature; no PQ/IVF/RaBitQ, no BRIN on temporal, no S2/H3 spatial cells, no composite cross-modal indexes. HIGH / L.
3. Query execution — Volcano-style iterator, no vectorised execution, no SIMD, no Cascades. HIGH / L.
4. Recovery — WAL with CRC + replay; no ARIES (no LSN), no group commit, no PITR. HIGH / L.
5. Replication — KRaft for metadata only; no data-plane replication; leaderless read-fanout federation only. HIGH / XL.
6. CAP / PACELC — implicit CP-metadata / AP-data; no per-query consistency knob. MED / M.
7. CRDTs — normalizer is heuristic; octad merge NOT verified commutative/associative/idempotent. HIGH (theory) / XL — see frontiers below.
8. Schema evolution — no online migration, no projection narrowing, no cross-modality propagation. MED / L.
9. Streaming / CDC — absent. EmptySubscription in GraphQL; no NATS/Kafka emit; no materialized views. HIGH / L.
10. Temporal — single time axis; NOT bitemporal; no Allen interval algebra. HIGH / M.
11. Provenance — hash-chain; NOT PROV-aligned; no why/where/how-provenance distinction. HIGH / L.
12. Spatial — Point/LineString/Polygon/MultiPoint/MultiPolygon; no MultiLineString, no GeometryCollection; r-tree feature-flagged; no ST_* functions in VQL. MED / L.
13. Semantic — Oxigraph SPARQL; no RDFS/OWL reasoning, no SHACL, no named-graph in VQL. HIGH / L.
14. Vector — HNSW only; no PQ/OPQ/RaBitQ/IVF; no multi-vector/ColBERT. HIGH / M.
15. Graph — Oxigraph RDF; not property-graph-native; no Cypher/Gremlin/GQL; no graph algos. MED / L.
16. Document — tantivy FT; no JSONPath/JMESPath/mongo operators. MED / M.
17. Tensor — ndarray; dense only; no SVD/CP/Tucker as queries. MED / L.
18. Adaptive / auto-tuning — AdaptiveTuner exists; no workload-aware index selection; selectivity = 0.2 hardcoded; no learned indexes. HIGH / M.
19. Security beyond ZKP — no RBAC, no row-level security, no column encryption, no KMS. CRIT / L.
20. Observability — telemetry module exists; drift histogram is global not per-modality-pair; no lock-contention metrics. MED / S.
21. Federation extensions — HTTP fanout + median-trust Byzantine; no SWIM, no Merkle anti-entropy, no BFT (HotStuff). MED / L.
22. Bridges & theory frontiers — no chase algorithm, no cross-modal FDs, no formal multi-modal-join cost model. HIGH (theory) / XL.

Theory-frontier opportunities (unique to this system)

1. Cross-modal composite indexes as algebraic structures — a B+-tree keyed by (vector_centroid, geohash, semantic_lub_type) accelerates octad-shaped queries no current DB indexes. Define over a product space of modality projections with a cost model. Publishable as 'Octad Indexes'.

2. The octad-CRDT class — formalise the cross-product of per-modality join-semilattices as a single CRDT with derived properties. Drift = delta-distance in this lattice. Convergence theorem. Counterpart to Shapiro et al. (2011).

3. Why-provenance for cross-modal queries — lift Buneman/Tan why-provenance to results spanning 8 modalities (drift function as a trust modifier on each witness). Each result row carries (modality_witness_set, drift_score). Coupled to verisim-provenance + ZKP for verifiable why-provenance.

4. Chase-based normalization with proven termination — reformulate verisim-normalizer as a typed chase (oblivious / core / parallel) over the 8-modality schema. Fixed cardinality (8) makes termination provable.

5. Multi-modal join problem with cost model — the join across modalities ('find octads where document text describes the spatial region of the vector cluster') has no published cost model. Define the octad-join algebra.

Five fastest wins

1. Bitemporal Version — add valid_from/valid_to to verisim-temporal. SQL:2011 alignment. Hours of work, decades of literature.
2. PROOF SHACL(...) — plug into existing VQL-DT proof type framework. One row in vql_type_checker.ex.
3. WAL-tailing CDC — verisim-cdc crate, ~300 LoC; emits change events from existing WAL segments.
4. Drift histogram tensor — replace global histogram with Hist[m_i × m_j] (28 cells). One file change. Operationally transformative.
5. VQL WITH CONSISTENCY clause — grammar mirrors existing WITH DRIFT. ~50 lines.

Five biggest pieces missing

1. Data-plane replication — every modality store is single-instance. Deployment-blocker.
2. Cross-peer write coordination — read fanout only; no 2PC/Calvin/Paxos commit.
3. Authentication / RBAC — ROADMAP §3.1, §3.2 are CRIT and unimplemented.
4. CDC + streaming subscriptions — GraphQL ships EmptySubscription. The estate uses NATS as a primitive; this absence is glaring.
5. Vector quantisation + multi-vector — stuck at 2020-era ANN; competitors all ship PQ + ColBERT-style.

[hyperpolymath]

Terminology correction (2026-06-01): every occurrence of "VQL" in this issue refers to what is now canonically called VCL (VeriSim Consonance Language). The rename happened 2026-04-05 — see hyperpolymath/vcl-ut README ("Its former name used the letter sequence 'V-Q-L-hyphen-U-T'... The canonical name is now VCL-total"). The verisim repo's own files are still file-named VQL* (e.g. src/vql/VQL*.res, vql-bridge/, docs/VQL-SPEC.adoc); that rename is incomplete in-repo and is itself a separable cleanup task — 90 files reference VQL; 11 ReScript files in src/vql/ (4974 LOC); the lone migrated outpost is connectors/clients/elixir/lib/verisim_client/vcl.ex. Where this issue mentions "VQL semantics theorems" or "VQL grammar", read as "VCL semantics"/"VCL grammar"; the VCL-total variant (next-gen, type-safe, certified Idris2 + Rust trusted parser + Ed25519 attestation) lives separately at hyperpolymath/vcl-ut and would replace the verisim-internal VCL surface as the upstream source-of-truth.

[hyperpolymath]

Status 2026-07-21 — untouched, plus two corrections and a sequencing note

Nothing in #185 addresses this issue; it is scoped to CI and the #47 residual. Recording what I verified while working nearby, so the 22-area table stays trustworthy.

Corrections to the area assessment

Area 20, Observability. The drift histogram point stands, but note the "five fastest wins" item 4 (Hist[m_i × m_j], 28 cells) is described as "one file change" — worth re-checking against the current verisim-drift layout before estimating, as the crate has moved since.

Area 11 / 21 — federation. Adjacent to this issue, #80 recorded the federation adapters as "5 silent failures". That is now inaccurate: the adapters match several response shapes and log a warning with a shape summary on an unrecognised one, and resolver.ex:312 already handles per-peer {:error, reason}. The residual is exactly the gap this issue frames better than #80 does — partial failure is not surfaced to the API caller, so a client cannot distinguish "peer had no data" from "peer's reply was unparseable". That belongs here under area 21, not in the seam-walk issue.

The Q1 opportunity is still genuinely open

Verified today: all 9 Coq modules compile under coqc 8.20.1 and just -f formal/Justfile check-assumptions passes (exit 0), but optimize_is_permutation remains an Axiom at formal/Planner.v:63 and formal/PlannerSemantic.v:94, applied at five call sites. So the planner-cost soundness target is undischarged, and the observation in #84 — that CostEstimate::sequential sums while ::parallel takes max, i.e. the planner is already secretly tropical — remains the cheapest available route to it.

Sequencing note on the "five fastest wins"

Four of the five are independent of the #86 A/B ruling and can start immediately: bitemporal Version<T>, PROOF SHACL(...), WAL-tailing CDC, and the drift histogram tensor. Only work that crosses the BEAM boundary should wait.

Of those, bitemporal Version<T> has a new prerequisite worth knowing about. #185 fixes an O(N²) bug in verisim-temporal: append() derived the next version number via versions.keys().last() on a BTreeMap — an O(n) walk on every single write. Five sites across lib.rs and persistent.rs had the same mistake. Anyone adding valid_from/valid_to should build on top of that fix rather than the pre-#185 code, and should be alert to the same .last()-on-a-BTreeMap pattern when adding the second time axis.