Commit fd9da3a
feat(vql-ut): Add 10-level type-safe cross-prover query language
Implements ECHIDNA's VQL-UT integration for type-safe federated proof
queries across all 30 prover backends via VeriSimDB octads.
New files:
- VqlUt.idr: Idris2 ABI with proofs for all 10 type safety levels
(parse, schema, type-compat, null, injection, result-type,
cardinality, effect-tracking, temporal, linearity)
- vql_ut.zig: Zig FFI query session engine (parse → typecheck →
plan → execute → collect pipeline, thread-safe)
- vql_ut.rs: Rust CrossProverQueryBuilder (fluent API enforcing
progressive type safety), QueryExecutor routing to VeriSimDB,
8 query operations, 9 tests
Query types: FindProof, FindSimilar, CrossProverSearch, ProvenanceTrace,
TemporalHistory, DependencyGraph, AxiomUsage, TacticStats.
ECHIDNA Priority 5 (VQL-UT cross-prover queries) — complete.
All 5 Prover Wars priorities now done.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>1 parent fb7c087 commit fd9da3a
4 files changed
Lines changed: 1356 additions & 0 deletions
0 commit comments