|
1 | 1 | // SPDX-License-Identifier: PMPL-1.0-or-later |
2 | 2 | // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell |
3 | 3 |
|
4 | | -//! Bridge from VQL-dt++ query types to TypeLL's unified types. |
| 4 | +//! Bridge from VQL-UT query types to TypeLL's unified types. |
5 | 5 | //! |
6 | | -//! ## VQL Extension → TypeLL Mapping |
| 6 | +//! Maps VQL-UT's 10-level type safety hierarchy into TypeLL concepts. |
| 7 | +//! Legacy VQL-dt++ extensions are preserved and mapped to their |
| 8 | +//! corresponding VQL-UT levels: |
7 | 9 | //! |
8 | | -//! | VQL Extension | TypeLL Concept | |
9 | | -//! |---------------------------|------------------------------------------| |
10 | | -//! | `CONSUME AFTER N USE` | `UsageQuantifier::Bounded(n)` | |
11 | | -//! | `WITH SESSION ReadOnly` | `SessionType::Recv` chain | |
12 | | -//! | `EFFECTS { Read, Write }` | `Effect::Named("Read")` etc. | |
13 | | -//! | `IN TRANSACTION Active` | `Type::Named("TxState:Active", [])` | |
14 | | -//! | `PROOF ATTACHED thm` | Refinement predicate | |
15 | | -//! | `USAGE LIMIT n` | `UsageQuantifier::Bounded(n)` | |
| 10 | +//! | VQL-UT Level | VQL-dt++ Extension | TypeLL Concept | |
| 11 | +//! |--------------|-----------------------------|-----------------------------------| |
| 12 | +//! | 5 | `PROOF ATTACHED thm` | Refinement predicate | |
| 13 | +//! | 8 | `EFFECTS { Read, Write }` | `Effect::Named("Read")` etc. | |
| 14 | +//! | 9 | `WITH SESSION ReadOnly` | `SessionType::Recv` chain | |
| 15 | +//! | 9 | `IN TRANSACTION Active` | `Type::Named("TxState:Active")` | |
| 16 | +//! | 10 | `CONSUME AFTER N USE` | `UsageQuantifier::Bounded(n)` | |
| 17 | +//! | 10 | `USAGE LIMIT n` | `UsageQuantifier::Bounded(n)` | |
16 | 18 |
|
17 | 19 | use serde::{Deserialize, Serialize}; |
18 | 20 | use typell_core::types::{ |
19 | 21 | Effect, Predicate, SessionType, Type, TypeDiscipline, |
20 | 22 | UnifiedType, UsageQuantifier, |
21 | 23 | }; |
22 | 24 |
|
| 25 | +use crate::levels::{SafetyLevel, SafetyReport, LevelCheck, QueryPath}; |
| 26 | + |
23 | 27 | /// VQL modality (one of the 8 query modalities). |
24 | 28 | #[derive(Debug, Clone, Serialize, Deserialize)] |
25 | 29 | pub enum VqlModality { |
@@ -233,6 +237,120 @@ fn modality_name(m: &VqlModality) -> &str { |
233 | 237 | } |
234 | 238 | } |
235 | 239 |
|
| 240 | +/// Determine the VQL-UT safety level achieved by a query. |
| 241 | +/// |
| 242 | +/// Checks each level in order and stops at the first failure. |
| 243 | +/// Returns a safety report with per-level diagnostics. |
| 244 | +pub fn determine_safety_level(vql: &VqlQueryType) -> SafetyReport { |
| 245 | + let mut checks = Vec::new(); |
| 246 | + let mut max_level = SafetyLevel::ParseTime; |
| 247 | + |
| 248 | + // Level 1: Parse-time safety — if we have a VqlQueryType, parsing succeeded. |
| 249 | + checks.push(LevelCheck { |
| 250 | + level: SafetyLevel::ParseTime, |
| 251 | + passed: true, |
| 252 | + diagnostic: String::new(), |
| 253 | + }); |
| 254 | + |
| 255 | + // Level 2: Schema-binding — result fields must be non-empty (schema resolved). |
| 256 | + let l2_pass = !vql.result_fields.is_empty(); |
| 257 | + checks.push(LevelCheck { |
| 258 | + level: SafetyLevel::SchemaBinding, |
| 259 | + passed: l2_pass, |
| 260 | + diagnostic: if l2_pass { String::new() } else { "No result fields bound to schema".to_string() }, |
| 261 | + }); |
| 262 | + if l2_pass { max_level = SafetyLevel::SchemaBinding; } |
| 263 | + |
| 264 | + // Level 3: Type-compatible operations — modalities are valid enum variants. |
| 265 | + let l3_pass = !vql.modalities.is_empty(); |
| 266 | + checks.push(LevelCheck { |
| 267 | + level: SafetyLevel::TypeCompatible, |
| 268 | + passed: l3_pass, |
| 269 | + diagnostic: if l3_pass { String::new() } else { "No modalities specified".to_string() }, |
| 270 | + }); |
| 271 | + if l2_pass && l3_pass { max_level = SafetyLevel::TypeCompatible; } |
| 272 | + |
| 273 | + // Level 4: Null-safety — all fields are typed (no raw strings without schema). |
| 274 | + // At this stage we treat schema-bound fields as null-safe. |
| 275 | + let l4_pass = l2_pass && l3_pass; |
| 276 | + checks.push(LevelCheck { |
| 277 | + level: SafetyLevel::NullSafe, |
| 278 | + passed: l4_pass, |
| 279 | + diagnostic: if l4_pass { String::new() } else { "Schema binding required for null-safety".to_string() }, |
| 280 | + }); |
| 281 | + if l4_pass { max_level = SafetyLevel::NullSafe; } |
| 282 | + |
| 283 | + // Level 5: Injection-proof — proof attachment provides refinement predicates. |
| 284 | + let l5_pass = l4_pass && vql.extensions.proof_attached.is_some(); |
| 285 | + checks.push(LevelCheck { |
| 286 | + level: SafetyLevel::InjectionProof, |
| 287 | + passed: l5_pass, |
| 288 | + diagnostic: if l5_pass { String::new() } else { "PROOF ATTACHED clause required for injection-proof safety".to_string() }, |
| 289 | + }); |
| 290 | + if l5_pass { max_level = SafetyLevel::InjectionProof; } |
| 291 | + |
| 292 | + // Level 6: Result-type safety — always passes if schema-bound (type is inferred). |
| 293 | + let l6_pass = l4_pass; |
| 294 | + checks.push(LevelCheck { |
| 295 | + level: SafetyLevel::ResultType, |
| 296 | + passed: l6_pass, |
| 297 | + diagnostic: if l6_pass { String::new() } else { "Result type cannot be inferred".to_string() }, |
| 298 | + }); |
| 299 | + if l5_pass && l6_pass { max_level = SafetyLevel::ResultType; } |
| 300 | + |
| 301 | + // Level 7: Cardinality safety — usage limit provides bounded quantifiers. |
| 302 | + let l7_pass = l6_pass && vql.extensions.usage_limit.is_some(); |
| 303 | + checks.push(LevelCheck { |
| 304 | + level: SafetyLevel::Cardinality, |
| 305 | + passed: l7_pass, |
| 306 | + diagnostic: if l7_pass { String::new() } else { "USAGE LIMIT clause required for cardinality safety".to_string() }, |
| 307 | + }); |
| 308 | + if l5_pass && l7_pass { max_level = SafetyLevel::Cardinality; } |
| 309 | + |
| 310 | + // Level 8: Effect-tracking — effects clause required. |
| 311 | + let l8_pass = l7_pass && vql.extensions.effects.as_ref().map_or(false, |e| !e.is_empty()); |
| 312 | + checks.push(LevelCheck { |
| 313 | + level: SafetyLevel::EffectTracking, |
| 314 | + passed: l8_pass, |
| 315 | + diagnostic: if l8_pass { String::new() } else { "EFFECTS clause required for effect-tracking safety".to_string() }, |
| 316 | + }); |
| 317 | + if l8_pass { max_level = SafetyLevel::EffectTracking; } |
| 318 | + |
| 319 | + // Level 9: Temporal safety — session protocol or transaction state required. |
| 320 | + let l9_pass = l8_pass && (vql.extensions.session_protocol.is_some() |
| 321 | + || vql.extensions.transaction_state.is_some()); |
| 322 | + checks.push(LevelCheck { |
| 323 | + level: SafetyLevel::Temporal, |
| 324 | + passed: l9_pass, |
| 325 | + diagnostic: if l9_pass { String::new() } else { "WITH SESSION or IN TRANSACTION clause required for temporal safety".to_string() }, |
| 326 | + }); |
| 327 | + if l9_pass { max_level = SafetyLevel::Temporal; } |
| 328 | + |
| 329 | + // Level 10: Linearity safety — consume_after or usage_limit with linear discipline. |
| 330 | + let l10_pass = l9_pass && vql.extensions.consume_after.is_some(); |
| 331 | + checks.push(LevelCheck { |
| 332 | + level: SafetyLevel::Linearity, |
| 333 | + passed: l10_pass, |
| 334 | + diagnostic: if l10_pass { String::new() } else { "CONSUME AFTER clause required for linearity safety".to_string() }, |
| 335 | + }); |
| 336 | + if l10_pass { max_level = SafetyLevel::Linearity; } |
| 337 | + |
| 338 | + // Determine query path based on max level. |
| 339 | + let query_path = if max_level.as_u8() >= 7 { |
| 340 | + QueryPath::Ut |
| 341 | + } else if max_level.as_u8() >= 2 { |
| 342 | + QueryPath::Dt |
| 343 | + } else { |
| 344 | + QueryPath::Slipstream |
| 345 | + }; |
| 346 | + |
| 347 | + SafetyReport { |
| 348 | + max_level, |
| 349 | + checks, |
| 350 | + query_path, |
| 351 | + } |
| 352 | +} |
| 353 | + |
236 | 354 | // ============================================================================ |
237 | 355 | // Tests |
238 | 356 | // ============================================================================ |
@@ -313,4 +431,55 @@ mod tests { |
313 | 431 | let session = session_protocol_to_session(&VqlSessionProtocol::Stream); |
314 | 432 | assert!(matches!(session, SessionType::Rec(_, _))); |
315 | 433 | } |
| 434 | + |
| 435 | + #[test] |
| 436 | + fn test_safety_level_basic_query() { |
| 437 | + let vql = VqlQueryType { |
| 438 | + modalities: vec![VqlModality::Graph], |
| 439 | + result_fields: vec!["name".to_string()], |
| 440 | + extensions: VqlExtensions::default(), |
| 441 | + }; |
| 442 | + let report = determine_safety_level(&vql); |
| 443 | + assert_eq!(report.max_level, SafetyLevel::NullSafe); |
| 444 | + assert_eq!(report.query_path, QueryPath::Dt); |
| 445 | + } |
| 446 | + |
| 447 | + #[test] |
| 448 | + fn test_safety_level_full_ut() { |
| 449 | + let vql = VqlQueryType { |
| 450 | + modalities: vec![VqlModality::Graph], |
| 451 | + result_fields: vec!["name".to_string()], |
| 452 | + extensions: VqlExtensions { |
| 453 | + consume_after: Some(3), |
| 454 | + session_protocol: Some(VqlSessionProtocol::ReadOnly), |
| 455 | + effects: Some(vec![VqlEffectLabel::Read]), |
| 456 | + transaction_state: None, |
| 457 | + proof_attached: Some("integrity".to_string()), |
| 458 | + usage_limit: Some(10), |
| 459 | + }, |
| 460 | + }; |
| 461 | + let report = determine_safety_level(&vql); |
| 462 | + assert_eq!(report.max_level, SafetyLevel::Linearity); |
| 463 | + assert_eq!(report.query_path, QueryPath::Ut); |
| 464 | + assert_eq!(report.checks.len(), 10); |
| 465 | + assert!(report.checks.iter().all(|c| c.passed)); |
| 466 | + } |
| 467 | + |
| 468 | + #[test] |
| 469 | + fn test_safety_level_partial_ut() { |
| 470 | + let vql = VqlQueryType { |
| 471 | + modalities: vec![VqlModality::Document], |
| 472 | + result_fields: vec!["content".to_string()], |
| 473 | + extensions: VqlExtensions { |
| 474 | + effects: Some(vec![VqlEffectLabel::Read, VqlEffectLabel::Write]), |
| 475 | + proof_attached: Some("access_control".to_string()), |
| 476 | + usage_limit: Some(5), |
| 477 | + ..Default::default() |
| 478 | + }, |
| 479 | + }; |
| 480 | + let report = determine_safety_level(&vql); |
| 481 | + // Has effects + proof + usage_limit but no session/consume_after |
| 482 | + assert_eq!(report.max_level, SafetyLevel::EffectTracking); |
| 483 | + assert_eq!(report.query_path, QueryPath::Ut); |
| 484 | + } |
316 | 485 | } |
0 commit comments