Skip to content

Commit 2fb28cf

Browse files
hyperpolymathclaude
andcommitted
feat: Add VQL-UT panel — flagship PanLL panel for type-safe queries
The VQL panel is the primary interface for VeriSimDB, ECHIDNA provers, and the 10-level VQL-UT type safety system. Includes: - VqlModel.res: 500+ line state model covering 10 safety levels, linter (30+ rules, 6 categories), formatter (5 presets), query editor, execution engine, schema browser, prover dispatch - VqlEngine.res: 900+ line pure computation engine with full linter implementation, formatter, template system, narrative generation - VqlCmd.res: Tauri FFI bridge for VeriSimDB/ECHIDNA/TypeLL/BoJ - Vql.res: 900+ line component with 7 tabs (Editor, Results, Plan, Schema, Provers, History, Config), safety gauge, diagnostics, evangeliser narratives, keyboard shortcuts - VQL.a2ml: Clade definition with capabilities and endpoint config - Wired into PanelSwitcherModel, PanelRegistry, PanelBus Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent d93fe06 commit 2fb28cf

8 files changed

Lines changed: 3174 additions & 0 deletions

File tree

panel-clades/clades/vql/VQL.a2ml

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// VQL-UT Panel Clade Definition — Attested Markup Language
3+
4+
[clade]
5+
id = "vql"
6+
kind = "service"
7+
version = "1.0.0"
8+
name = "VQL-UT: Type-Safe Query Language"
9+
description = """
10+
The flagship PanLL panel. VQL-UT provides a 10-level progressive type safety
11+
system for querying VeriSimDB's 8-modality octad storage, dispatching across
12+
ECHIDNA's 30 prover backends, and generating formally verified query plans.
13+
14+
Features:
15+
- 10-level type safety ratchet (L0 Unsafe → L10 Linear-Safe)
16+
- Dedicated linter with 30+ rules across 6 categories
17+
- Dedicated formatter with 5 style presets
18+
- Cross-prover federated query dispatch
19+
- VeriSimDB octad-aware schema browser
20+
- Query plan visualization with cost estimation
21+
- TypeLL integration for dependent-type checking
22+
- Proof obligation tracking and discharge
23+
- Evangeliser narratives (celebrate/minimize/improve/safety)
24+
"""
25+
26+
capabilities = [
27+
"VqlQuery",
28+
"VqlLint",
29+
"VqlFormat",
30+
"VqlTypeCheck",
31+
"VqlExplain",
32+
"SchemaIntrospect",
33+
"CrossProverDispatch",
34+
"ProofObligationTrack",
35+
"QueryHistoryManage",
36+
"ResultExport",
37+
]
38+
39+
consumed-by = [
40+
"typell", // TypeLL provides type checking for VQL expressions
41+
"echidna", // ECHIDNA provides cross-prover dispatch
42+
"verisimdb", // VeriSimDB provides octad storage
43+
"databases", // Databases panel shares connection state
44+
"boj", // BoJ routes queries through cartridges
45+
]
46+
47+
consumes = [
48+
"verisimdb", // Query execution target
49+
"echidna", // Prover dispatch
50+
"typell", // Type checking service
51+
]
52+
53+
[endpoints]
54+
verisimdb = "http://localhost:8200"
55+
echidna = "http://localhost:8000"
56+
typell = "http://localhost:7800"
57+
boj = "http://localhost:7700"
58+
59+
[health]
60+
check-interval-ms = 10000
61+
endpoints = [
62+
"http://localhost:8200/api/v1/health",
63+
"http://localhost:8000/api/v1/health",
64+
"http://localhost:7800/api/v1/health",
65+
]
66+
67+
[bus]
68+
subscribes = ["TopicDatabase", "TopicType", "TopicProtocol"]
69+
publishes = ["TopicDatabase", "TopicType"]
70+
71+
[taxonomy]
72+
domain = "data"
73+
group = "Data"
74+
priority = 1
75+
icon = "database-search"

src/commands/VqlCmd.res

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,196 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// VQL-UT Commands — Tauri FFI bridge for VQL panel I/O.
3+
//
4+
// All side effects (HTTP calls, file I/O, clipboard) route through here.
5+
// The VQL panel's Engine layer is pure; this module handles the real world.
6+
//
7+
// Endpoints:
8+
// VeriSimDB — http://localhost:8200 (octad query execution)
9+
// ECHIDNA — http://localhost:8000 (cross-prover dispatch)
10+
// TypeLL — http://localhost:7800 (type checking)
11+
// BoJ Server — http://localhost:7700 (cartridge routing)
12+
13+
open VqlModel
14+
15+
// ============================================================
16+
// SECTION 1: Tauri Command Bindings
17+
// ============================================================
18+
19+
/// Generic Tauri invoke binding.
20+
@module("@tauri-apps/api/core")
21+
external invoke: (string, 'a) => promise<string> = "invoke"
22+
23+
/// Invoke with no arguments.
24+
@module("@tauri-apps/api/core")
25+
external invokeNoArgs: string => promise<string> = "invoke"
26+
27+
// ============================================================
28+
// SECTION 2: VeriSimDB Commands
29+
// ============================================================
30+
31+
/// Execute a VQL-UT query against VeriSimDB.
32+
let executeQuery = (
33+
query: string,
34+
target: executionTarget,
35+
level: typeSafetyLevel,
36+
_bojRouting: bool,
37+
): promise<result<string, string>> => {
38+
let endpoint = switch target {
39+
| TargetVeriSimDB => "http://localhost:8200/api/v1/query"
40+
| TargetEchidna => "http://localhost:8000/api/v1/vql"
41+
| TargetBoJ => "http://localhost:7700/echidna-llm/vql"
42+
| TargetTypeLL => "http://localhost:7800/api/v1/vql-ut/check"
43+
| TargetDryRun => "http://localhost:8200/api/v1/explain"
44+
}
45+
let levelInt = VqlEngine.levelToInt(level)
46+
let body = `{"query": ${JSON.stringify(JSON.Encode.string(query))}, "level": ${Int.toString(levelInt)}}`
47+
invoke("http_post", {"url": endpoint, "body": body})
48+
->Promise.then(response => Promise.resolve(Ok(response)))
49+
->Promise.catch(err => {
50+
let msg = switch err {
51+
| Exn.Error(e) => switch Exn.message(e) {
52+
| Some(m) => m
53+
| None => "Unknown error"
54+
}
55+
| _ => "Unknown error"
56+
}
57+
Promise.resolve(Error(msg))
58+
})
59+
}
60+
61+
/// Fetch the VeriSimDB schema (tables, columns, modalities).
62+
let fetchSchema = (): promise<result<string, string>> => {
63+
invoke("http_get", {"url": "http://localhost:8200/api/v1/schema"})
64+
->Promise.then(r => Promise.resolve(Ok(r)))
65+
->Promise.catch(err => {
66+
let msg = switch err {
67+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Schema fetch failed" }
68+
| _ => "Schema fetch failed"
69+
}
70+
Promise.resolve(Error(msg))
71+
})
72+
}
73+
74+
/// Check VeriSimDB connection health.
75+
let checkConnection = (): promise<result<string, string>> => {
76+
invoke("http_get", {"url": "http://localhost:8200/api/v1/health"})
77+
->Promise.then(r => Promise.resolve(Ok(r)))
78+
->Promise.catch(err => {
79+
let msg = switch err {
80+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Connection failed" }
81+
| _ => "Connection failed"
82+
}
83+
Promise.resolve(Error(msg))
84+
})
85+
}
86+
87+
// ============================================================
88+
// SECTION 3: TypeLL Type Checking Commands
89+
// ============================================================
90+
91+
/// Send a VQL-UT query to TypeLL for type checking.
92+
let typeCheckQuery = (query: string, level: typeSafetyLevel): promise<result<string, string>> => {
93+
let levelInt = VqlEngine.levelToInt(level)
94+
let body = `{"query": ${JSON.stringify(JSON.Encode.string(query))}, "level": ${Int.toString(levelInt)}, "mode": "vql-ut"}`
95+
invoke("http_post", {"url": "http://localhost:7800/api/v1/vql-ut/check", "body": body})
96+
->Promise.then(r => Promise.resolve(Ok(r)))
97+
->Promise.catch(err => {
98+
let msg = switch err {
99+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "TypeLL check failed" }
100+
| _ => "TypeLL check failed"
101+
}
102+
Promise.resolve(Error(msg))
103+
})
104+
}
105+
106+
// ============================================================
107+
// SECTION 4: ECHIDNA Cross-Prover Commands
108+
// ============================================================
109+
110+
/// Fetch available prover statuses from ECHIDNA.
111+
let fetchProverStatus = (): promise<result<string, string>> => {
112+
invoke("http_get", {"url": "http://localhost:8000/api/v1/provers"})
113+
->Promise.then(r => Promise.resolve(Ok(r)))
114+
->Promise.catch(err => {
115+
let msg = switch err {
116+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Prover fetch failed" }
117+
| _ => "Prover fetch failed"
118+
}
119+
Promise.resolve(Error(msg))
120+
})
121+
}
122+
123+
/// Get a query execution plan without executing.
124+
let explainQuery = (query: string): promise<result<string, string>> => {
125+
let body = `{"query": ${JSON.stringify(JSON.Encode.string(query))}, "explain": true}`
126+
invoke("http_post", {"url": "http://localhost:8000/api/v1/vql/explain", "body": body})
127+
->Promise.then(r => Promise.resolve(Ok(r)))
128+
->Promise.catch(err => {
129+
let msg = switch err {
130+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Explain failed" }
131+
| _ => "Explain failed"
132+
}
133+
Promise.resolve(Error(msg))
134+
})
135+
}
136+
137+
// ============================================================
138+
// SECTION 5: Export Commands
139+
// ============================================================
140+
141+
/// Export query results to a file.
142+
let exportResults = (data: string, format: string): promise<result<string, string>> => {
143+
invoke("save_file", {"content": data, "format": format, "defaultName": `vql-results.${format}`})
144+
->Promise.then(r => Promise.resolve(Ok(r)))
145+
->Promise.catch(err => {
146+
let msg = switch err {
147+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Export failed" }
148+
| _ => "Export failed"
149+
}
150+
Promise.resolve(Error(msg))
151+
})
152+
}
153+
154+
/// Copy text to clipboard.
155+
let copyToClipboard = (text: string): promise<result<string, string>> => {
156+
invoke("clipboard_write", {"text": text})
157+
->Promise.then(r => Promise.resolve(Ok(r)))
158+
->Promise.catch(err => {
159+
let msg = switch err {
160+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Clipboard failed" }
161+
| _ => "Clipboard failed"
162+
}
163+
Promise.resolve(Error(msg))
164+
})
165+
}
166+
167+
// ============================================================
168+
// SECTION 6: History Persistence
169+
// ============================================================
170+
171+
/// Save query history to local storage.
172+
let saveHistory = (history: array<historyEntry>): promise<result<string, string>> => {
173+
let json = JSON.stringify(Obj.magic(history))
174+
invoke("store_set", {"key": "vql_history", "value": json})
175+
->Promise.then(r => Promise.resolve(Ok(r)))
176+
->Promise.catch(err => {
177+
let msg = switch err {
178+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Save failed" }
179+
| _ => "Save failed"
180+
}
181+
Promise.resolve(Error(msg))
182+
})
183+
}
184+
185+
/// Load query history from local storage.
186+
let loadHistory = (): promise<result<string, string>> => {
187+
invoke("store_get", {"key": "vql_history"})
188+
->Promise.then(r => Promise.resolve(Ok(r)))
189+
->Promise.catch(err => {
190+
let msg = switch err {
191+
| Exn.Error(e) => switch Exn.message(e) { | Some(m) => m | None => "Load failed" }
192+
| _ => "Load failed"
193+
}
194+
Promise.resolve(Error(msg))
195+
})
196+
}

0 commit comments

Comments
 (0)