1  use anyhow::{anyhow, bail, Result};
  2  use jsonschema::{JSONSchema, ValidationError};
  3  use serde_json::{json, Value};
  4  use tracing::debug;
  5  
  6  pub struct SchemaValidator {
  7      config_schema: JSONSchema,
  8      module_schema: JSONSchema,
  9  }
 10  
 11  impl std::fmt::Debug for SchemaValidator {
 12      fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
 13          f.debug_struct("SchemaValidator")
 14              .field("config_schema", &"<JSONSchema>")
 15              .field("module_schema", &"<JSONSchema>")
 16              .finish()
 17      }
 18  }
 19  
 20  impl SchemaValidator {
 21      pub fn new() -> Result<Self> {
 22          let config_schema = Self::build_config_schema()?;
 23          let module_schema = Self::build_module_schema()?;
 24  
 25          Ok(Self {
 26              config_schema,
 27              module_schema,
 28          })
 29      }
 30  
 31      /// Validate a root configuration file
 32      pub fn validate(&self, config: &Value) -> Result<()> {
 33          debug!("Validating configuration against schema");
 34  
 35          match self.config_schema.validate(config) {
 36              Ok(_) => {
 37                  debug!("Configuration schema validation passed");
 38                  Ok(())
 39              }
 40              Err(errors) => {
 41                  let error_messages: Vec<String> = errors
 42                      .into_iter()
 43                      .map(|e| format!("{:?} at {}", e.kind, e.instance_path))
 44                      .collect();
 45  
 46                  bail!(
 47                      "Configuration validation failed:\n{}",
 48                      error_messages.join("\n")
 49                  );
 50              }
 51          }
 52      }
 53  
 54      /// Validate a module configuration (partial config)
 55      pub fn validate_module(&self, config: &Value) -> Result<()> {
 56          debug!("Validating module configuration against schema");
 57  
 58          match self.module_schema.validate(config) {
 59              Ok(_) => {
 60                  debug!("Module configuration schema validation passed");
 61                  Ok(())
 62              }
 63              Err(errors) => {
 64                  let error_messages: Vec<String> = errors
 65                      .into_iter()
 66                      .map(|e| format!("{:?} at {}", e.kind, e.instance_path))
 67                      .collect();
 68  
 69                  bail!(
 70                      "Module configuration validation failed:\n{}",
 71                      error_messages.join("\n")
 72                  );
 73              }
 74          }
 75      }
 76  
 77      /// Get detailed validation errors with suggestions
 78      pub fn validate_with_details(&self, config: &Value) -> ValidationResult {
 79          let mut result = ValidationResult {
 80              is_valid: true,
 81              errors: Vec::new(),
 82              warnings: Vec::new(),
 83              suggestions: Vec::new(),
 84          };
 85  
 86          // Validate against schema
 87          if let Err(errors) = self.config_schema.validate(config) {
 88              result.is_valid = false;
 89              for error in errors {
 90                  let location = error.instance_path.to_string();
 91                  let message = format!("{:?}", error.kind);
 92  
 93                  let validation_error = ValidationErrorDetail {
 94                      field: if location.is_empty() {
 95                          "root".to_string()
 96                      } else {
 97                          location.clone()
 98                      },
 99                      message,
100                      location: location.clone(),
101                      expected_value: self.get_expected_value_for_field(&location),
102                      suggestion: self.get_suggestion_for_field(&location, &error),
103                  };
104  
105                  result.errors.push(validation_error);
106              }
107          }
108  
109          // Additional business logic validation
110          self.validate_business_logic(config, &mut result);
111  
112          result
113      }
114  
115      /// Validate business logic beyond schema validation
116      fn validate_business_logic(&self, config: &Value, result: &mut ValidationResult) {
117          // Check verification level vs enabled techniques
118          if let (Some(level), Some(techniques)) = (
119              config
120                  .get("profile")
121                  .and_then(|p| p.get("level"))
122                  .and_then(|l| l.as_str()),
123              config
124                  .get("profile")
125                  .and_then(|p| p.get("enabled_techniques"))
126                  .and_then(|t| t.as_array()),
127          ) {
128              self.validate_level_techniques_consistency(level, techniques, result);
129          }
130  
131          // Check threshold values
132          if let Some(thresholds) = config.get("thresholds") {
133              self.validate_thresholds(thresholds, result);
134          }
135  
136          // Check tool configurations
137          if let Some(tools) = config.get("tools") {
138              self.validate_tool_configs(tools, result);
139          }
140      }
141  
142      fn validate_level_techniques_consistency(
143          &self,
144          level: &str,
145          techniques: &[Value],
146          result: &mut ValidationResult,
147      ) {
148          let techniques_vec: Vec<String> = techniques
149              .iter()
150              .filter_map(|t| t.as_str().map(|s| s.to_string()))
151              .collect();
152  
153          match level {
154              "minimal" => {
155                  if !techniques_vec.contains(&"TypeSafety".to_string()) {
156                      result.errors.push(ValidationErrorDetail {
157                          field: "profile.enabled_techniques".to_string(),
158                          message: "Minimal level must include TypeSafety technique".to_string(),
159                          location: "profile.enabled_techniques".to_string(),
160                          expected_value: Some("TypeSafety".to_string()),
161                          suggestion: Some("Add TypeSafety to enabled_techniques or use a higher verification level".to_string()),
162                      });
163                      result.is_valid = false;
164                  }
165              }
166              "standard" => {
167                  if !techniques_vec.contains(&"PropertyTests".to_string()) {
168                      result.errors.push(ValidationErrorDetail {
169                          field: "profile.enabled_techniques".to_string(),
170                          message: "Standard level must include PropertyTests technique".to_string(),
171                          location: "profile.enabled_techniques".to_string(),
172                          expected_value: Some("PropertyTests".to_string()),
173                          suggestion: Some("Add PropertyTests to enabled_techniques or use a higher verification level".to_string()),
174                      });
175                      result.is_valid = false;
176                  }
177              }
178              "strict" => {
179                  if !techniques_vec.contains(&"SessionTypes".to_string()) {
180                      result.errors.push(ValidationErrorDetail {
181                          field: "profile.enabled_techniques".to_string(),
182                          message: "Strict level must include SessionTypes technique".to_string(),
183                          location: "profile.enabled_techniques".to_string(),
184                          expected_value: Some("SessionTypes".to_string()),
185                          suggestion: Some("Add SessionTypes to enabled_techniques or use the formal verification level".to_string()),
186                      });
187                      result.is_valid = false;
188                  }
189              }
190              "formal" => {
191                  if !techniques_vec.contains(&"FormalSpecs".to_string()) {
192                      result.errors.push(ValidationErrorDetail {
193                          field: "profile.enabled_techniques".to_string(),
194                          message: "Formal level must include FormalSpecs technique".to_string(),
195                          location: "profile.enabled_techniques".to_string(),
196                          expected_value: Some("FormalSpecs".to_string()),
197                          suggestion: Some("Add FormalSpecs to enabled_techniques".to_string()),
198                      });
199                      result.is_valid = false;
200                  }
201              }
202              _ => {
203                  result.errors.push(ValidationErrorDetail {
204                      field: "profile.level".to_string(),
205                      message: format!("Unknown verification level: {}", level),
206                      location: "profile.level".to_string(),
207                      expected_value: Some("minimal, standard, strict, formal".to_string()),
208                      suggestion: Some("Use one of: minimal, standard, strict, formal".to_string()),
209                  });
210                  result.is_valid = false;
211              }
212          }
213      }
214  
215      fn validate_thresholds(&self, thresholds: &Value, result: &mut ValidationResult) {
216          if let Some(max_time) = thresholds
217              .get("max_verification_time")
218              .and_then(|t| t.as_u64())
219          {
220              if max_time == 0 {
221                  result.errors.push(ValidationErrorDetail {
222                      field: "thresholds.max_verification_time".to_string(),
223                      message: "max_verification_time must be > 0".to_string(),
224                      location: "thresholds.max_verification_time".to_string(),
225                      expected_value: Some("positive integer".to_string()),
226                      suggestion: Some(
227                          "Set to at least 60 seconds for basic verification".to_string(),
228                      ),
229                  });
230                  result.is_valid = false;
231              }
232              if max_time > 3600 {
233                  result.warnings.push(ValidationWarning {
234                      field: "thresholds.max_verification_time".to_string(),
235                      message: "max_verification_time is very high (> 1 hour)".to_string(),
236                      location: "thresholds.max_verification_time".to_string(),
237                      suggestion: Some(
238                          "Consider using a shorter timeout for faster feedback".to_string(),
239                      ),
240                  });
241              }
242          }
243  
244          if let Some(max_memory) = thresholds.get("max_memory_usage").and_then(|m| m.as_u64()) {
245              if max_memory == 0 {
246                  result.errors.push(ValidationErrorDetail {
247                      field: "thresholds.max_memory_usage".to_string(),
248                      message: "max_memory_usage must be > 0".to_string(),
249                      location: "thresholds.max_memory_usage".to_string(),
250                      expected_value: Some("positive integer (bytes)".to_string()),
251                      suggestion: Some(
252                          "Set to at least 1073741824 (1GB) for basic verification".to_string(),
253                      ),
254                  });
255                  result.is_valid = false;
256              }
257          }
258      }
259  
260      fn validate_tool_configs(&self, tools: &Value, result: &mut ValidationResult) {
261          if let Some(proptest) = tools.get("proptest") {
262              if let Some(cases) = proptest.get("cases").and_then(|c| c.as_u64()) {
263                  if cases == 0 {
264                      result.errors.push(ValidationErrorDetail {
265                          field: "tools.proptest.cases".to_string(),
266                          message: "proptest.cases must be > 0".to_string(),
267                          location: "tools.proptest.cases".to_string(),
268                          expected_value: Some("positive integer".to_string()),
269                          suggestion: Some(
270                              "Set to at least 100 test cases for reasonable coverage".to_string(),
271                          ),
272                      });
273                      result.is_valid = false;
274                  }
275                  if cases > 100000 {
276                      result.warnings.push(ValidationWarning {
277                          field: "tools.proptest.cases".to_string(),
278                          message: "proptest.cases is very high (>100k)".to_string(),
279                          location: "tools.proptest.cases".to_string(),
280                          suggestion: Some(
281                              "Consider reducing cases for faster test execution".to_string(),
282                          ),
283                      });
284                  }
285              }
286          }
287      }
288  
289      fn get_expected_value_for_field(&self, field: &str) -> Option<String> {
290          match field {
291              "profile.level" => Some("one of: minimal, standard, strict, formal".to_string()),
292              "profile.enforcement" => Some("one of: advisory, warning, error".to_string()),
293              "thresholds.max_verification_time" => Some("positive integer (seconds)".to_string()),
294              "thresholds.max_memory_usage" => Some("positive integer (bytes)".to_string()),
295              "tools.proptest.cases" => Some("positive integer".to_string()),
296              _ => None,
297          }
298      }
299  
300      fn get_suggestion_for_field(&self, field: &str, _error: &ValidationError) -> Option<String> {
301          match field {
302              "profile.level" => Some("Use 'minimal' for basic checks, 'standard' for most projects, 'strict' for critical systems, or 'formal' for safety-critical systems".to_string()),
303              "profile.enforcement" => Some("Use 'advisory' during development, 'warning' for CI, or 'error' for production builds".to_string()),
304              _ => None,
305          }
306      }
307  
308      /// Build the JSON schema for root configuration
309      fn build_config_schema() -> Result<JSONSchema> {
310          let schema = json!({
311              "$schema": "http://json-schema.org/draft-07/schema#",
312              "title": "FerrisProof Configuration",
313              "description": "Configuration for FerrisProof multi-layer verification pipeline",
314              "type": "object",
315              "properties": {
316                  "profile": {
317                      "type": "object",
318                      "properties": {
319                          "level": {
320                              "type": "string",
321                              "enum": ["minimal", "standard", "strict", "formal"],
322                              "description": "Verification level for the project"
323                          },
324                          "enforcement": {
325                              "type": "string",
326                              "enum": ["advisory", "warning", "error"],
327                              "description": "How verification violations should be handled"
328                          },
329                          "enabled_techniques": {
330                              "type": "array",
331                              "items": {
332                                  "type": "string",
333                                  "enum": ["TypeSafety", "PropertyTests", "SessionTypes", "RefinementTypes", "ConcurrencyTesting", "FormalSpecs", "ModelChecking"]
334                              },
335                              "description": "List of verification techniques to enable"
336                          }
337                      },
338                      "required": ["level", "enforcement", "enabled_techniques"]
339                  },
340                  "tools": {
341                      "type": "object",
342                      "properties": {
343                          "tla_plus": {
344                              "$ref": "#/definitions/TlaPlusConfig"
345                          },
346                          "alloy": {
347                              "$ref": "#/definitions/AlloyConfig"
348                          },
349                          "proptest": {
350                              "$ref": "#/definitions/ProptestConfig"
351                          },
352                          "kani": {
353                              "$ref": "#/definitions/KaniConfig"
354                          }
355                      },
356                      "additionalProperties": false
357                  },
358                  "modules": {
359                      "type": "object",
360                      "patternProperties": {
361                          "^.*$": {
362                              "$ref": "#/definitions/ModuleConfig"
363                          }
364                      },
365                      "additionalProperties": false
366                  },
367                  "features": {
368                      "$ref": "#/definitions/FeatureConfig"
369                  },
370                  "thresholds": {
371                      "$ref": "#/definitions/Thresholds"
372                  },
373                  "ci": {
374                      "$ref": "#/definitions/CiConfig"
375                  }
376              },
377              "required": ["profile"],
378              "additionalProperties": false,
379              "definitions": {
380                  "TlaPlusConfig": {
381                      "type": "object",
382                      "properties": {
383                          "tlc_path": {
384                              "type": "string",
385                              "description": "Path to TLC model checker executable"
386                          },
387                          "timeout": {
388                              "type": "integer",
389                              "minimum": 1,
390                              "description": "Timeout in seconds for TLA+ model checking"
391                          },
392                          "workers": {
393                              "type": "integer",
394                              "minimum": 1,
395                              "description": "Number of parallel workers for model checking"
396                          }
397                      },
398                      "additionalProperties": false
399                  },
400                  "AlloyConfig": {
401                      "type": "object",
402                      "properties": {
403                          "analyzer_path": {
404                              "type": "string",
405                              "description": "Path to Alloy Analyzer executable"
406                          },
407                          "scope": {
408                              "type": "integer",
409                              "minimum": 1,
410                              "description": "Scope for Alloy analysis"
411                          }
412                      },
413                      "additionalProperties": false
414                  },
415                  "ProptestConfig": {
416                      "type": "object",
417                      "properties": {
418                          "cases": {
419                              "type": "integer",
420                              "minimum": 1,
421                              "description": "Number of test cases to generate"
422                          },
423                          "max_shrink_iters": {
424                              "type": "integer",
425                              "minimum": 1,
426                              "description": "Maximum iterations for test case shrinking"
427                          }
428                      },
429                      "additionalProperties": false
430                  },
431                  "KaniConfig": {
432                      "type": "object",
433                      "properties": {
434                          "cbmc_path": {
435                              "type": "string",
436                              "description": "Path to CBMC executable"
437                          },
438                          "unwind": {
439                              "type": "integer",
440                              "minimum": 1,
441                              "description": "Unwind depth for Kani verification"
442                          }
443                      },
444                      "additionalProperties": false
445                  },
446                  "ModuleConfig": {
447                      "type": "object",
448                      "properties": {
449                          "level": {
450                              "type": "string",
451                              "enum": ["minimal", "standard", "strict", "formal"]
452                          },
453                          "enforcement": {
454                              "type": "string",
455                              "enum": ["advisory", "warning", "error"]
456                          },
457                          "enabled_techniques": {
458                              "type": "array",
459                              "items": {
460                                  "type": "string"
461                              }
462                          },
463                          "spec_file": {
464                              "type": "string",
465                              "description": "Path to formal specification file"
466                          }
467                      },
468                      "additionalProperties": false
469                  },
470                  "FeatureConfig": {
471                      "type": "object",
472                      "properties": {
473                          "cache_enabled": {
474                              "type": "boolean",
475                              "description": "Enable verification result caching"
476                          },
477                          "parallel_execution": {
478                              "type": "boolean",
479                              "description": "Enable parallel verification execution"
480                          },
481                          "generate_reports": {
482                              "type": "boolean",
483                              "description": "Generate verification reports"
484                          }
485                      },
486                      "required": ["cache_enabled", "parallel_execution", "generate_reports"]
487                  },
488                  "Thresholds": {
489                      "type": "object",
490                      "properties": {
491                          "max_verification_time": {
492                              "type": "integer",
493                              "minimum": 1,
494                              "description": "Maximum verification time in seconds"
495                          },
496                          "max_memory_usage": {
497                              "type": "integer",
498                              "minimum": 1,
499                              "description": "Maximum memory usage in bytes"
500                          },
501                          "cache_ttl": {
502                              "type": "integer",
503                              "minimum": 1,
504                              "description": "Cache time-to-live in seconds"
505                          }
506                      },
507                      "required": ["max_verification_time", "max_memory_usage", "cache_ttl"]
508                  },
509                  "CiConfig": {
510                      "type": "object",
511                      "properties": {
512                          "fail_on_violations": {
513                              "type": "boolean",
514                              "description": "Fail CI builds on verification violations"
515                          },
516                          "generate_artifacts": {
517                              "type": "boolean",
518                              "description": "Generate verification artifacts in CI"
519                          },
520                          "upload_reports": {
521                              "type": "boolean",
522                              "description": "Upload verification reports"
523                          }
524                      },
525                      "required": ["fail_on_violations", "generate_artifacts", "upload_reports"]
526                  }
527              }
528          });
529  
530          JSONSchema::compile(&schema).map_err(|e| anyhow!("Failed to compile config schema: {}", e))
531      }
532  
533      /// Build the JSON schema for module configuration (partial config)
534      fn build_module_schema() -> Result<JSONSchema> {
535          let schema = json!({
536              "$schema": "http://json-schema.org/draft-07/schema#",
537              "title": "FerrisProof Module Configuration",
538              "description": "Partial configuration for specific modules",
539              "type": "object",
540              "properties": {
541                  "profile": {
542                      "type": "object",
543                      "properties": {
544                          "level": {
545                              "type": "string",
546                              "enum": ["minimal", "standard", "strict", "formal"]
547                          },
548                          "enforcement": {
549                              "type": "string",
550                              "enum": ["advisory", "warning", "error"]
551                          },
552                          "enabled_techniques": {
553                              "type": "array",
554                              "items": {
555                                  "type": "string"
556                              }
557                          }
558                      }
559                  },
560                  "modules": {
561                      "type": "object",
562                      "patternProperties": {
563                          "^.*$": {
564                              "$ref": "#/definitions/ModuleConfig"
565                          }
566                      }
567                  }
568              },
569              "additionalProperties": false,
570              "definitions": {
571                  "ModuleConfig": {
572                      "type": "object",
573                      "properties": {
574                          "level": {
575                              "type": "string",
576                              "enum": ["minimal", "standard", "strict", "formal"]
577                          },
578                          "enforcement": {
579                              "type": "string",
580                              "enum": ["advisory", "warning", "error"]
581                          },
582                          "enabled_techniques": {
583                              "type": "array",
584                              "items": {
585                                  "type": "string"
586                              }
587                          },
588                          "spec_file": {
589                              "type": "string"
590                          }
591                      }
592                  }
593              }
594          });
595  
596          JSONSchema::compile(&schema).map_err(|e| anyhow!("Failed to compile module schema: {}", e))
597      }
598  }
599  
600  impl Default for SchemaValidator {
601      fn default() -> Self {
602          Self::new().expect("Failed to create schema validator")
603      }
604  }
605  
606  #[derive(Debug, Clone)]
607  pub struct ValidationResult {
608      pub is_valid: bool,
609      pub errors: Vec<ValidationErrorDetail>,
610      pub warnings: Vec<ValidationWarning>,
611      pub suggestions: Vec<String>,
612  }
613  
614  #[derive(Debug, Clone)]
615  pub struct ValidationErrorDetail {
616      pub field: String,
617      pub message: String,
618      pub location: String,
619      pub expected_value: Option<String>,
620      pub suggestion: Option<String>,
621  }
622  
623  #[derive(Debug, Clone)]
624  pub struct ValidationWarning {
625      pub field: String,
626      pub message: String,
627      pub location: String,
628      pub suggestion: Option<String>,
629  }