Cross-repo synthesis: vcl-ut + kategoria + echo-types + tropical-resource-typing → VeriSimDB #84

Background

Owner directive 2026-06-01: cross-reference VeriSimDB against four sibling repos that bear on its design — vcl-ut (VCL-total: next-gen interaction language, certified Idris2 + Rust trusted parser + Ed25519 attestation), kategoria (10-level type-safety challenge / teaching surface), echo-types (constructive Agda for proof-relevant structured loss; Pillars A–D complete), tropical-resource-typing (max-plus tropical algebra for worst-case bounds; AFP-grade Isabelle).

This issue surfaces the top concrete hooks each sibling gives VeriSimDB, the five cross-repo opportunities, and the foundation-pack alignment (which of the 8 proof targets from #77 fit which sibling).

Per-sibling top hooks

vcl-ut (VCL-total)

• src/vql/VQLBidir.res + VQLProofObligation.res ← vcl-ut/src/core/Checker.idr + Levels.idr. Sibling provides the dependent SafetyCertificate and 10-level evidence-carrying predicates already mechanized. VeriSimDB's bidirectional checker becomes a thin wrapper over certifiedLevel, replacing the ad-hoc obligation-kind enum with proof-carrying receipts.
• rust-core/verisim-api/src/vql.rs + connectors/clients/elixir/lib/verisim_client/vcl.ex ← vcl-ut/src/interface/attest + recompute-wasm. Switch the /api/v1/vql/execute path to the deterministic wire format (vcl-ut/src/interface/parse/WIRE-FORMAT.adoc) + add the Tier-2 Ed25519 attestation. Every query gains a Refl-pinned conformance receipt the client can verify offline.
• docs/VQL-SPEC.adoc ← vcl-ut/docs/vcl-total-grammar.ebnf (25 KB). Replace VeriSimDB's informal grammar with a re-export of the EBNF that vcl-ut/src/core/Grammar.idr certifies. Single-source-of-truth move.

Maturity: Phase 5 complete; 12 certified Idris2 modules; 49 tests passing; believe_me: 0.

kategoria

• src/vql/VQLTypes.res ← kategoria/routes/alpha-extend/Level0[1-6]_*.idr. Tag each VeriSimDB type-primitive with its kategoria level so the planner can emit per-level certificates rather than a flat "type-safe" boolean.
• rust-core/verisim-planner/src/cost.rs ← Level07_LinearTypes.idr (QTT). Annotate BaseCost per modality with multiplicity (Semantic-ZKP = 1, Vector-HNSW = ω); rewrite sequential/parallel combinators to reject double-consumption of a 1-graded modality at plan time.
• connectors/clients/elixir/lib/verisim_client/octad.ex ← Level09_SessionTypes.idr. Express octad CRDT write protocol as a session type — fixing the lone believe_me in the kategoria file lands both repos.

Maturity: mid-alpha skeleton (Route α only); thesis LaTeX is the real product right now. Best fit as VCL-total per-level conformance test suite, not as a prover engine.

echo-types

• rust-core/verisim-drift/src/calculator.rs (scalar drift_score: f64 at lines 67, 127, 177, 193, 228, 245, 266, 284) ← EchoResidueTaxonomy.agda. Each modality view is a function f_m : Octad → ModalityView_m. Drift between two views = an echo at the disagreement set. Replace the scalar score with a ResidueForm-instance (lower: Echo f y → R y) and pick the residue carrier per drift type — trivial-residue for QualityDrift, identity-residue for ProvenanceDrift, linear-affine-residue for SchemaDrift. "No drift" becomes the theorem "echo is canonically trivial", not a magic 0.0.
• rust-core/verisim-normalizer/src/{conflict.rs, regeneration.rs} ← EchoDecorationStructure.agda + the compositional iso family in Echo.agda. Re-state ConflictPolicy::ModalityPriority(Vec<Modality>) as a DecorationStructure instance. The pentagon coherence + cancel-iso prove commute-with-composition; ≤-join-univ / degrade-compose / degrade-via-join give commutative/associative/idempotent merge as theorems — directly closes the N2 foundation-pack target.
• rust-core/verisim-octad/src/query_octad.rs ← EchoOFSUnivF5Iso.agda + EchoImageFactorization.agda. The octad query "8 modality views → unified result" is the (equivalence, projection) factorization. Image f := Σ B (Echo f) + the factorization triangle f = proj₁ ∘ encode f give query results a residue witness recording which modalities contributed — provenance for free.

Maturity: late-alpha / publication-ready for the internal programme. Pillars A–D complete 2026-05-17; Pillar E paper drafted with [EXPAND] tags. Open headline: Bachmann-Howard rank-mono <ᵇ-+1 joint-bplus.

tropical-resource-typing

• rust-core/verisim-planner/src/cost.rs (CostEstimate::sequential line 89 sums time_ms; CostEstimate::parallel line 100 takes max) ← Tropical.thy + TropicalSessionTypes.lean. The planner is already secretly tropical: parallel = max (tropical add), sequential = + (tropical mul). Make it explicit. Re-state CostEstimate over the tropical semiring (ℕ ∪ {-∞}, max, +); CostEstimate::combine becomes a tropical matrix-power product; the floyd_warshall theorem becomes the planner's correctness theorem. Closes Q1 for free.
• rust-core/verisim-planner/src/profiler.rs ← Tropical_Kleene.thy (Kleene star = max-weight simple path). Slow-query analysis = path through modality DAG with worst-case weight. floyd_warshall over the cost matrix gives certified p99 bounds rather than empirical.
• rust-core/verisim-api/src/rbac.rs + proof-obligation cost layer ← TropicalSessionTypes.lean grading. Speculative parallel proof obligations (e.g., INTEGRITY ‖ PROVENANCE) get bottleneck cost not sum cost.

Maturity: research note + AFP-grade Isabelle (paper outline targets AFP submission). Tropical_Ordinal_Bridge.thy is a forward hook for the echo-types Bachmann-Howard milestone.

Five cross-repo opportunities (ranked)

1. Drift = echo + tropical cost (verisim + echo-types + tropical). Each DriftCalculator::*_drift becomes the echo at a modality-disagreement set with residue carrier picked by drift type; the severity is the tropical cost (worst-case bound) over the residue's collapse path. Single most natural composition the four siblings invite. Closes both D1 (drift-score soundness) and Q1 (planner-cost soundness) under one algebraic structure.

2. Octad merge = DecorationStructure join (verisim + echo-types). N2 (normalizer-merge CRDT laws) becomes the existing EchoDecorationStructure lemmas applied to ConflictPolicy::ModalityPriority. Commutativity / associativity / idempotence by re-export.

3. VCL-total + tropical = session-typed query plan (vcl-ut + tropical + kategoria). VCL-total L8 (Effects) + L10 (Linearity) are in the 10-level grammar; grade each effect with a tropical session type so a VCL EFFECTS { Read, Write } clause carries a Refl-pinned worst-case latency bound through the wire codec.

4. Kategoria 10-levels as VCL-total conformance suite (kategoria + vcl-ut + verisim). kategoria/shared/test-suite/CHALLENGES.adoc already specifies 10 challenge programs — wire each as a VCL-total fragment so the kategoria test-suite doubles as VCL-total's per-level conformance suite.

5. Ordinal track unblocks long-game alignment (echo-types + tropical). When echo-types' Buchholz track reaches Bachmann-Howard, Tropical_Ordinal_Bridge.thy becomes the cross-prover alignment target (Agda BT ↔ Isabelle tropO). Firewalled per echo-types/docs/bridges/tropical-correspondence.md — track, don't pull forward.

Foundation-pack alignment (8 theorems × 4 siblings)

5 of 8 → echo-types, 2 → vcl-ut, 1 → tropical, 0 → kategoria (kategoria's role is teaching/test-bed, not prover).

VQL → VCL rename: scope quantified

• 90 files in verisimdb still reference VQL (*.res, *.rs, *.adoc)
• 11 ReScript modules in src/vql/ named VQL*.res (4,974 LOC): VQLTypes, VQLError, VQLBidir, VQLExplain, VQLTypeChecker, VQLProofObligation, VQLContext, VQLParser_test, VQLSubtyping, VQLCircuit, VQLParser
• Rust touchpoints: verisim-repl/src/vql_fmt.rs, verisim-planner/src/vql_bridge.rs, verisim-api/src/vql.rs, verisim-semantic/src/zkp_bridge.rs, verisim-octad/src/query_octad.rs, fuzz/fuzz_targets/fuzz_vql_parser.rs, SDK clients in connectors/clients/{rust,rescript}/
• Already migrated: connectors/clients/elixir/lib/verisim_client/vcl.ex (lone outpost)
• User-facing route: /api/v1/vql/execute (still old name)
• 0 files reference VclTotal — clean separation from the vcl-ut upstream

Recommended strategy: single PR adding vcl/ modules as pub use re-exports of vql/ so old call-sites compile; follow-up batches switch call-sites. Estate-flavour fanout (similar to standards#288 CodeQL cron sweep), not per-call-site PRs.

Relevant paths

• VeriSimDB: rust-core/verisim-drift/src/calculator.rs, rust-core/verisim-planner/src/{cost.rs,profiler.rs}, rust-core/verisim-normalizer/src/{conflict.rs,regeneration.rs}, rust-core/verisim-octad/src/query_octad.rs, src/vql/{VQLBidir,VQLProofObligation,VQLTypeChecker}.res, connectors/clients/elixir/lib/verisim_client/vcl.ex
• vcl-ut: src/core/{Checker,Levels,Grammar}.idr, src/interface/{parse/WIRE-FORMAT.adoc,attest,recompute-wasm,WireConformance.idr}, docs/{THE-10-LEVELS-EXPLAINED.adoc,vcl-total-grammar.ebnf}
• echo-types: proofs/agda/{EchoResidueTaxonomy,EchoDecorationStructure,EchoNoSectionGeneric,EchoOFSUnivF5Iso,EchoImageFactorization,EchoCanonicalIdentitySuite,EchoChoreo,EchoObservationalEquivalence}.agda, docs/bridges/tropical-correspondence.md
• tropical-resource-typing: Tropical.thy, Tropical_Kleene.thy, Tropical_Matrices_Clean.thy, TropicalSessionTypes.lean, Tropical_Ordinal_Bridge.thy
• kategoria: routes/alpha-extend/Level0[1-9]_*.idr + Level10_CubicalTypes.idr, shared/test-suite/CHALLENGES.adoc