1  use ferris_proof_core::plugins::{PluginManager, ValidationStatus, VerificationPlugin};
  2  use ferris_proof_plugins::sandbox::{NetworkPolicy, ResourceLimits};
  3  use ferris_proof_plugins::{ProptestPlugin, SandboxedExecutor, TlaPlusPlugin};
  4  use serde_json::json;
  5  use std::collections::HashMap;
  6  use std::time::Duration;
  7  
  8  #[cfg(test)]
  9  mod plugin_system_tests {
 10      use super::*;
 11  
 12      #[test]
 13      /// Test plugin loading and version compatibility
 14      /// Validates: Requirements 9.11, 9.16
 15      fn test_plugin_loading_and_version_compatibility() {
 16          let mut plugin_manager = PluginManager::new();
 17  
 18          // Test loading TLA+ plugin
 19          let tla_plugin = Box::new(TlaPlusPlugin::new());
 20          let plugin_name = tla_plugin.name().to_string();
 21          let plugin_version = tla_plugin.version().to_string();
 22  
 23          // Plugin should load successfully
 24          let load_result = plugin_manager.register_plugin(tla_plugin);
 25          assert!(load_result.is_ok(), "TLA+ plugin should load successfully");
 26  
 27          // Check that plugin is registered
 28          let plugin_metadata = plugin_manager.plugin_metadata(&plugin_name);
 29          assert!(
 30              plugin_metadata.is_some(),
 31              "Plugin metadata should be available"
 32          );
 33  
 34          let metadata = plugin_metadata.unwrap();
 35          assert_eq!(metadata.name, plugin_name);
 36          assert_eq!(metadata.version, plugin_version);
 37  
 38          // Test loading Proptest plugin
 39          let proptest_plugin = Box::new(ProptestPlugin::new());
 40          let proptest_name = proptest_plugin.name().to_string();
 41  
 42          let load_result = plugin_manager.register_plugin(proptest_plugin);
 43          assert!(
 44              load_result.is_ok(),
 45              "Proptest plugin should load successfully"
 46          );
 47  
 48          // Verify both plugins are listed
 49          let all_plugins = plugin_manager.list_plugins();
 50          assert!(
 51              all_plugins.len() >= 2,
 52              "Should have at least 2 plugins registered"
 53          );
 54  
 55          let plugin_names: Vec<String> = all_plugins.iter().map(|p| p.name.clone()).collect();
 56          assert!(
 57              plugin_names.contains(&plugin_name),
 58              "TLA+ plugin should be in list"
 59          );
 60          assert!(
 61              plugin_names.contains(&proptest_name),
 62              "Proptest plugin should be in list"
 63          );
 64      }
 65  
 66      #[test]
 67      /// Test tool discovery and availability checking
 68      /// Validates: Requirements 9.11, 9.16
 69      fn test_tool_discovery_and_availability() {
 70          let mut plugin_manager = PluginManager::new();
 71  
 72          // Register plugins
 73          let tla_plugin = Box::new(TlaPlusPlugin::new());
 74          let proptest_plugin = Box::new(ProptestPlugin::new());
 75  
 76          plugin_manager
 77              .register_plugin(tla_plugin)
 78              .expect("TLA+ plugin should register");
 79          plugin_manager
 80              .register_plugin(proptest_plugin)
 81              .expect("Proptest plugin should register");
 82  
 83          // Validate tools
 84          let validation_results = plugin_manager
 85              .validate_tools()
 86              .expect("Tool validation should succeed");
 87  
 88          assert!(
 89              !validation_results.is_empty(),
 90              "Should have validation results"
 91          );
 92  
 93          for result in &validation_results {
 94              // Each plugin should have a validation result
 95              assert!(
 96                  !result.plugin_name.is_empty(),
 97                  "Plugin name should not be empty"
 98              );
 99  
100              match result.status {
101                  ValidationStatus::Valid => {
102                      assert!(
103                          result.tool_info.is_some(),
104                          "Valid tools should have tool info"
105                      );
106                      let tool_info = result.tool_info.as_ref().unwrap();
107                      assert!(
108                          tool_info.available,
109                          "Valid tools should be marked as available"
110                      );
111                      assert!(
112                          !tool_info.capabilities.is_empty(),
113                          "Valid tools should have capabilities"
114                      );
115                  }
116                  ValidationStatus::Unavailable => {
117                      // Tool not available - this is acceptable in test environments
118                      assert!(
119                          !result.issues.is_empty(),
120                          "Unavailable tools should have issues listed"
121                      );
122                  }
123                  ValidationStatus::VersionIncompatible => {
124                      // Version incompatible - should have tool info but marked as incompatible
125                      assert!(
126                          !result.issues.is_empty(),
127                          "Incompatible tools should have issues listed"
128                      );
129                  }
130                  ValidationStatus::Error => {
131                      // Error occurred during validation
132                      assert!(
133                          !result.issues.is_empty(),
134                          "Error status should have issues listed"
135                      );
136                  }
137              }
138          }
139      }
140  
141      #[test]
142      /// Test plugin metadata and capabilities
143      /// Validates: Requirements 9.15
144      fn test_plugin_metadata_and_capabilities() {
145          let tla_plugin = TlaPlusPlugin::new();
146          let proptest_plugin = ProptestPlugin::new();
147  
148          // Test TLA+ plugin metadata
149          let tla_metadata = tla_plugin.metadata();
150          assert_eq!(tla_metadata.name, "tla-plus");
151          assert!(!tla_metadata.version.is_empty());
152          assert!(!tla_metadata.description.is_empty());
153          assert!(!tla_metadata.techniques.is_empty());
154          assert!(tla_metadata
155              .techniques
156              .contains(&ferris_proof_core::types::Technique::FormalSpecs));
157          assert!(tla_metadata
158              .techniques
159              .contains(&ferris_proof_core::types::Technique::ModelChecking));
160  
161          // Test Proptest plugin metadata
162          let proptest_metadata = proptest_plugin.metadata();
163          assert_eq!(proptest_metadata.name, "proptest");
164          assert!(!proptest_metadata.version.is_empty());
165          assert!(!proptest_metadata.description.is_empty());
166          assert!(!proptest_metadata.techniques.is_empty());
167          assert!(proptest_metadata
168              .techniques
169              .contains(&ferris_proof_core::types::Technique::PropertyTests));
170  
171          // Test supported techniques
172          let tla_techniques = tla_plugin.supported_techniques();
173          assert!(!tla_techniques.is_empty());
174  
175          let proptest_techniques = proptest_plugin.supported_techniques();
176          assert!(!proptest_techniques.is_empty());
177  
178          // Test version ranges
179          let tla_versions = tla_plugin.supported_versions();
180          assert!(
181              tla_versions.min.is_some()
182                  || tla_versions.max.is_some()
183                  || tla_versions.requires_exact.is_some()
184          );
185  
186          let proptest_versions = proptest_plugin.supported_versions();
187          assert!(
188              proptest_versions.min.is_some()
189                  || proptest_versions.max.is_some()
190                  || proptest_versions.requires_exact.is_some()
191          );
192      }
193  
194      #[test]
195      /// Test plugin initialization and cleanup
196      /// Validates: Requirements 9.15
197      fn test_plugin_initialization_and_cleanup() {
198          let mut tla_plugin = TlaPlusPlugin::new();
199          let mut proptest_plugin = ProptestPlugin::new();
200  
201          // Test initialization with empty config
202          let empty_config = json!({});
203  
204          // TLA+ plugin initialization might fail if TLC is not available, which is acceptable
205          let _tla_init_result = tla_plugin.initialize(&empty_config);
206          // Don't assert success since TLC might not be installed
207  
208          // Proptest plugin initialization might fail if Rust toolchain is not available
209          let _proptest_init_result = proptest_plugin.initialize(&empty_config);
210          // Don't assert success since Rust might not be installed
211  
212          // Test initialization with specific config
213          let tla_config = json!({
214              "tla_plus": {
215                  "tlc_path": "/usr/local/bin/tlc"
216              }
217          });
218  
219          let proptest_config = json!({
220              "proptest": {
221                  "path": "cargo"
222              }
223          });
224  
225          // These might fail if tools are not available, which is acceptable in tests
226          let _ = tla_plugin.initialize(&tla_config);
227          let _ = proptest_plugin.initialize(&proptest_config);
228  
229          // Test cleanup - should always succeed
230          let tla_cleanup = tla_plugin.cleanup();
231          assert!(tla_cleanup.is_ok(), "TLA+ plugin cleanup should succeed");
232  
233          let proptest_cleanup = proptest_plugin.cleanup();
234          assert!(
235              proptest_cleanup.is_ok(),
236              "Proptest plugin cleanup should succeed"
237          );
238      }
239  
240      #[tokio::test]
241      /// Test sandboxed execution with resource limits
242      /// Validates: Requirements 12.4
243      async fn test_sandboxed_execution_with_resource_limits() {
244          let executor = SandboxedExecutor::new()
245              .with_network_policy(NetworkPolicy::Denied)
246              .with_limits(ResourceLimits {
247                  max_memory: 50 * 1024 * 1024, // 50MB
248                  max_cpu_time: 5,              // 5 seconds
249                  max_file_descriptors: 32,
250                  max_processes: 2,
251                  max_file_size: 1024, // 1KB
252              })
253              .with_timeout(Duration::from_secs(3));
254  
255          // Test executing a simple command
256          let result = executor
257              .execute("echo", &["Hello, World!"], HashMap::new(), None)
258              .await;
259  
260          match result {
261              Ok(output) => {
262                  assert_eq!(output.exit_code, 0, "Echo command should succeed");
263                  assert!(
264                      output.stdout.contains("Hello, World!"),
265                      "Output should contain expected text"
266                  );
267                  assert!(!output.timeout_occurred, "Command should not timeout");
268              }
269              Err(e) => {
270                  // Command might not be available in test environment
271                  let error_msg = e.to_string();
272                  assert!(
273                      error_msg.contains("not found")
274                          || error_msg.contains("No such file")
275                          || error_msg.contains("Failed to spawn process"),
276                      "Error should be due to command not found, got: {}",
277                      error_msg
278                  );
279              }
280          }
281      }
282  
283      #[tokio::test]
284      /// Test sandboxed execution timeout handling
285      /// Validates: Requirements 12.4
286      async fn test_sandboxed_execution_timeout_handling() {
287          let executor = SandboxedExecutor::new()
288              .with_network_policy(NetworkPolicy::Denied)
289              .with_limits(ResourceLimits::default())
290              .with_timeout(Duration::from_millis(100)); // Very short timeout
291  
292          // Test with a command that should timeout (sleep)
293          let result = executor
294              .execute(
295                  "sleep",
296                  &["5"], // Sleep for 5 seconds, but timeout is 100ms
297                  HashMap::new(),
298                  None,
299              )
300              .await;
301  
302          match result {
303              Ok(output) => {
304                  // If sleep command is available, it should timeout
305                  if output.timeout_occurred {
306                      assert_ne!(
307                          output.exit_code, 0,
308                          "Timed out command should have non-zero exit code"
309                      );
310                      assert!(
311                          output.stderr.contains("timeout"),
312                          "Error should mention timeout"
313                      );
314                  } else {
315                      // Command might have completed very quickly or failed to start
316                      // This is acceptable in test environments
317                  }
318              }
319              Err(e) => {
320                  // Command might not be available in test environment
321                  let error_msg = e.to_string();
322                  assert!(
323                      error_msg.contains("not found")
324                          || error_msg.contains("No such file")
325                          || error_msg.contains("Failed to spawn process"),
326                      "Error should be due to command not found, got: {}",
327                      error_msg
328                  );
329              }
330          }
331      }
332  
333      #[test]
334      /// Test plugin manager with multiple plugins
335      /// Validates: Requirements 9.11, 9.15, 9.16
336      fn test_plugin_manager_multiple_plugins() {
337          let mut plugin_manager = PluginManager::new();
338  
339          // Register multiple plugins
340          let tla_plugin = Box::new(TlaPlusPlugin::new());
341          let proptest_plugin = Box::new(ProptestPlugin::new());
342  
343          plugin_manager
344              .register_plugin(tla_plugin)
345              .expect("TLA+ plugin should register");
346          plugin_manager
347              .register_plugin(proptest_plugin)
348              .expect("Proptest plugin should register");
349  
350          // Test getting plugins for specific techniques
351          let formal_plugins =
352              plugin_manager.plugins_for_technique(&ferris_proof_core::types::Technique::FormalSpecs);
353          assert!(
354              !formal_plugins.is_empty(),
355              "Should have plugins for formal specs"
356          );
357  
358          let property_plugins = plugin_manager
359              .plugins_for_technique(&ferris_proof_core::types::Technique::PropertyTests);
360          assert!(
361              !property_plugins.is_empty(),
362              "Should have plugins for property tests"
363          );
364  
365          // Test plugin initialization
366          let config = json!({
367              "tla-plus": {
368                  "tlc_path": "/usr/local/bin/tlc"
369              },
370              "proptest": {
371                  "path": "cargo"
372              }
373          });
374  
375          let init_result = plugin_manager.initialize_plugins(&config);
376          assert!(init_result.is_ok(), "Plugin initialization should succeed");
377  
378          // Test plugin cleanup
379          let cleanup_result = plugin_manager.cleanup_plugins();
380          assert!(cleanup_result.is_ok(), "Plugin cleanup should succeed");
381      }
382  
383      #[test]
384      /// Test resource limits configuration
385      /// Validates: Requirements 12.4
386      fn test_resource_limits_configuration() {
387          let limits = ResourceLimits {
388              max_memory: 100 * 1024 * 1024, // 100MB
389              max_cpu_time: 30,              // 30 seconds
390              max_file_descriptors: 64,
391              max_processes: 5,
392              max_file_size: 10 * 1024 * 1024, // 10MB
393          };
394  
395          let _executor = SandboxedExecutor::new().with_limits(limits.clone());
396  
397          // Verify limits are set correctly
398          // Note: We can't directly access private fields, but we can test behavior
399          // Resource limits should be configurable
400  
401          // Test default limits
402          let default_limits = ResourceLimits::default();
403          assert!(
404              default_limits.max_memory > 0,
405              "Default memory limit should be positive"
406          );
407          assert!(
408              default_limits.max_cpu_time > 0,
409              "Default CPU time limit should be positive"
410          );
411          assert!(
412              default_limits.max_file_descriptors > 0,
413              "Default file descriptor limit should be positive"
414          );
415          assert!(
416              default_limits.max_processes > 0,
417              "Default process limit should be positive"
418          );
419          assert!(
420              default_limits.max_file_size > 0,
421              "Default file size limit should be positive"
422          );
423      }
424  
425      #[test]
426      /// Test network policy configuration
427      /// Validates: Requirements 12.1
428      fn test_network_policy_configuration() {
429          // Test denied policy
430          let _denied_executor = SandboxedExecutor::new().with_network_policy(NetworkPolicy::Denied);
431  
432          // Test allowlist policy
433          let allowed_hosts = vec!["example.com".to_string(), "trusted.org".to_string()];
434          let _allowlist_executor = SandboxedExecutor::new()
435              .with_network_policy(NetworkPolicy::AllowList(allowed_hosts.clone()));
436  
437          // Test unrestricted policy with consent
438          let _unrestricted_executor = SandboxedExecutor::new()
439              .with_network_policy(NetworkPolicy::Unrestricted { user_consent: true });
440  
441          // Test unrestricted policy without consent
442          let _no_consent_executor =
443              SandboxedExecutor::new().with_network_policy(NetworkPolicy::Unrestricted {
444                  user_consent: false,
445              });
446  
447          // Verify policies can be configured
448          // Network policies should be configurable
449  
450          // Test policy equality
451          let policy1 = NetworkPolicy::Denied;
452          let policy2 = NetworkPolicy::Denied;
453          assert_eq!(policy1, policy2, "Denied policies should be equal");
454  
455          let policy3 = NetworkPolicy::AllowList(vec!["test.com".to_string()]);
456          let policy4 = NetworkPolicy::AllowList(vec!["test.com".to_string()]);
457          assert_eq!(
458              policy3, policy4,
459              "Identical allowlist policies should be equal"
460          );
461  
462          let policy5 = NetworkPolicy::Unrestricted { user_consent: true };
463          let policy6 = NetworkPolicy::Unrestricted { user_consent: true };
464          assert_eq!(
465              policy5, policy6,
466              "Identical unrestricted policies should be equal"
467          );
468      }
469  }