Skip to content

Commit 1c78af9

Browse files
hyperpolymathclaude
andcommitted
feat(verisimdb): Add TypeLL VQL-UT pre-flight check and safety metadata
VQL execute handler now validates queries against TypeLL before execution. VqlExecuteResponse extended with safety_level, query_path, and proof_obligations fields. Non-blocking — proceeds without TypeLL if unreachable. Enables PanLL and ECHIDNA to consume type safety metadata. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 6651558 commit 1c78af9

1 file changed

Lines changed: 148 additions & 1 deletion

File tree

  • verisimdb/rust-core/verisim-api/src

verisimdb/rust-core/verisim-api/src/vql.rs

Lines changed: 148 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,15 @@ pub struct VqlExecuteResponse {
5252
/// Optional message (e.g., for INSERT/DELETE confirmations).
5353
#[serde(skip_serializing_if = "Option::is_none")]
5454
pub message: Option<String>,
55+
/// VQL-UT safety level achieved (0-9), if TypeLL validation was performed.
56+
#[serde(skip_serializing_if = "Option::is_none")]
57+
pub safety_level: Option<u8>,
58+
/// VQL-UT query path used: "VQL (Slipstream)", "VQL-DT", or "VQL-UT".
59+
#[serde(skip_serializing_if = "Option::is_none")]
60+
pub query_path: Option<String>,
61+
/// Proof obligations generated by TypeLL (for ECHIDNA dispatch).
62+
#[serde(skip_serializing_if = "Option::is_none")]
63+
pub proof_obligations: Option<Vec<String>>,
5564
}
5665

5766
/// Execute a VQL query string against the database.
@@ -78,7 +87,11 @@ pub async fn vql_execute_handler(
7887
return Err(ApiError::BadRequest("Empty query after parsing".to_string()));
7988
}
8089

81-
let result = match tokens[0].to_uppercase().as_str() {
90+
// Pre-flight: validate with TypeLL VQL-UT checker if available.
91+
// This is non-blocking — if TypeLL is unreachable, we proceed without it.
92+
let typell_report = validate_with_typell(query).await;
93+
94+
let mut result = match tokens[0].to_uppercase().as_str() {
8295
"SELECT" => execute_select(&state, &tokens, query).await,
8396
"SEARCH" => execute_search(&state, &tokens).await,
8497
"INSERT" => execute_insert(&state, query).await,
@@ -92,9 +105,19 @@ pub async fn vql_execute_handler(
92105
))),
93106
}?;
94107

108+
// Attach TypeLL safety metadata to the response
109+
if let Some((level, path, obligations)) = typell_report {
110+
result.safety_level = Some(level);
111+
result.query_path = Some(path);
112+
if !obligations.is_empty() {
113+
result.proof_obligations = Some(obligations);
114+
}
115+
}
116+
95117
info!(
96118
statement_type = %result.statement_type,
97119
row_count = result.row_count,
120+
safety_level = ?result.safety_level,
98121
"VQL query executed"
99122
);
100123

@@ -103,6 +126,91 @@ pub async fn vql_execute_handler(
103126

104127
/// Tokenize a VQL query into whitespace-separated tokens, respecting
105128
/// quoted strings (single and double quotes).
129+
/// Validate a VQL query against TypeLL's VQL-UT 10-level type checker.
130+
///
131+
/// Calls the TypeLL server (default: localhost:7800) to verify the query's
132+
/// type safety level. Returns (safety_level, query_path, proof_obligations)
133+
/// if TypeLL is reachable, or None if it's unavailable.
134+
///
135+
/// This is a non-blocking, best-effort validation — query execution proceeds
136+
/// regardless. The safety metadata is attached to the response for downstream
137+
/// consumers (PanLL, ECHIDNA) to act on.
138+
async fn validate_with_typell(query: &str) -> Option<(u8, String, Vec<String>)> {
139+
let typell_url = std::env::var("TYPELL_URL")
140+
.unwrap_or_else(|_| "http://localhost:7800".to_string());
141+
142+
let check_body = serde_json::json!({
143+
"expression": query,
144+
"context": "{\"language\":\"vql\",\"dialect\":\"vql-ut\",\"features\":[\"dependent\",\"linear\",\"proof-carrying\"]}"
145+
});
146+
147+
let client = reqwest::Client::builder()
148+
.timeout(std::time::Duration::from_secs(3))
149+
.build()
150+
.ok()?;
151+
152+
let resp = client
153+
.post(format!("{}/api/v1/check", typell_url))
154+
.json(&check_body)
155+
.send()
156+
.await
157+
.ok()?;
158+
159+
if !resp.status().is_success() {
160+
return None;
161+
}
162+
163+
let body: serde_json::Value = resp.json().await.ok()?;
164+
165+
// Extract VQL-UT level from features (e.g., "vql-ut-l4")
166+
let level = body
167+
.get("features")
168+
.and_then(|f| f.as_array())
169+
.and_then(|arr| {
170+
arr.iter().find_map(|v| {
171+
let s = v.as_str()?;
172+
if let Some(stripped) = s.strip_prefix("vql-ut-l") {
173+
stripped.parse::<u8>().ok()
174+
} else {
175+
None
176+
}
177+
})
178+
})
179+
.unwrap_or(0);
180+
181+
// Extract query path from features (e.g., "path:VQL-UT")
182+
let path = body
183+
.get("features")
184+
.and_then(|f| f.as_array())
185+
.and_then(|arr| {
186+
arr.iter().find_map(|v| {
187+
let s = v.as_str()?;
188+
s.strip_prefix("path:").map(|p| p.to_string())
189+
})
190+
})
191+
.unwrap_or_else(|| "VQL (Slipstream)".to_string());
192+
193+
// Extract proof obligations
194+
let obligations: Vec<String> = body
195+
.get("proof_obligations")
196+
.and_then(|p| p.as_array())
197+
.map(|arr| {
198+
arr.iter()
199+
.filter_map(|v| v.as_str().map(|s| s.to_string()))
200+
.collect()
201+
})
202+
.unwrap_or_default();
203+
204+
info!(
205+
safety_level = level,
206+
query_path = %path,
207+
obligations = obligations.len(),
208+
"TypeLL VQL-UT pre-flight check complete"
209+
);
210+
211+
Some((level, path, obligations))
212+
}
213+
106214
fn tokenize(input: &str) -> Vec<String> {
107215
let mut tokens = Vec::new();
108216
let mut current = String::new();
@@ -198,6 +306,9 @@ async fn execute_select(
198306
data: serde_json::to_value(vec![response])
199307
.map_err(|e| ApiError::Serialization(e.to_string()))?,
200308
message: None,
309+
safety_level: None,
310+
query_path: None,
311+
proof_obligations: None,
201312
})
202313
} else {
203314
// List octads
@@ -217,6 +328,9 @@ async fn execute_select(
217328
data: serde_json::to_value(responses)
218329
.map_err(|e| ApiError::Serialization(e.to_string()))?,
219330
message: None,
331+
safety_level: None,
332+
query_path: None,
333+
proof_obligations: None,
220334
})
221335
}
222336
}
@@ -291,6 +405,9 @@ async fn execute_search(
291405
row_count: count,
292406
data: json!(results),
293407
message: None,
408+
safety_level: None,
409+
query_path: None,
410+
proof_obligations: None,
294411
})
295412
}
296413
"VECTOR" => {
@@ -333,6 +450,9 @@ async fn execute_search(
333450
row_count: count,
334451
data: json!(results),
335452
message: None,
453+
safety_level: None,
454+
query_path: None,
455+
proof_obligations: None,
336456
})
337457
}
338458
"RELATED" => {
@@ -367,6 +487,9 @@ async fn execute_search(
367487
data: serde_json::to_value(responses)
368488
.map_err(|e| ApiError::Serialization(e.to_string()))?,
369489
message: None,
490+
safety_level: None,
491+
query_path: None,
492+
proof_obligations: None,
370493
})
371494
}
372495
other => Err(ApiError::BadRequest(format!(
@@ -449,6 +572,9 @@ async fn execute_insert(
449572
data: serde_json::to_value(vec![&response])
450573
.map_err(|e| ApiError::Serialization(e.to_string()))?,
451574
message: Some(format!("Inserted octad '{}'", response.id)),
575+
safety_level: None,
576+
query_path: None,
577+
proof_obligations: None,
452578
})
453579
}
454580

@@ -516,6 +642,9 @@ async fn execute_delete(
516642
row_count: 1,
517643
data: json!(null),
518644
message: Some(format!("Deleted octad '{}'", id)),
645+
safety_level: None,
646+
query_path: None,
647+
proof_obligations: None,
519648
})
520649
}
521650

@@ -571,6 +700,9 @@ async fn execute_show(
571700
"degraded_reason": reason,
572701
}),
573702
message: None,
703+
safety_level: None,
704+
query_path: None,
705+
proof_obligations: None,
574706
})
575707
}
576708
"DRIFT" => {
@@ -599,6 +731,9 @@ async fn execute_show(
599731
row_count: count,
600732
data: json!(results),
601733
message: None,
734+
safety_level: None,
735+
query_path: None,
736+
proof_obligations: None,
602737
})
603738
}
604739
"NORMALIZER" => {
@@ -610,6 +745,9 @@ async fn execute_show(
610745
data: serde_json::to_value(status)
611746
.map_err(|e| ApiError::Serialization(e.to_string()))?,
612747
message: None,
748+
safety_level: None,
749+
query_path: None,
750+
proof_obligations: None,
613751
})
614752
}
615753
"OCTADS" => {
@@ -630,6 +768,9 @@ async fn execute_show(
630768
data: serde_json::to_value(responses)
631769
.map_err(|e| ApiError::Serialization(e.to_string()))?,
632770
message: None,
771+
safety_level: None,
772+
query_path: None,
773+
proof_obligations: None,
633774
})
634775
}
635776
other => Err(ApiError::BadRequest(format!(
@@ -666,6 +807,9 @@ async fn execute_count(
666807
row_count: 1,
667808
data: json!({ "count": count }),
668809
message: None,
810+
safety_level: None,
811+
query_path: None,
812+
proof_obligations: None,
669813
})
670814
}
671815

@@ -771,6 +915,9 @@ async fn execute_explain(
771915
"plan": plan,
772916
}),
773917
message: None,
918+
safety_level: None,
919+
query_path: None,
920+
proof_obligations: None,
774921
})
775922
}
776923

0 commit comments

Comments
 (0)