cli_initialization_property_test.rs
1 use ferris_proof_cli::commands::init; 2 use ferris_proof_core::VerificationLevel; 3 use proptest::prelude::*; 4 use std::fs; 5 use std::sync::Mutex; 6 use tempfile::TempDir; 7 8 // Mutex to serialize tests that change the current working directory 9 static WORKING_DIR_MUTEX: Mutex<()> = Mutex::new(()); 10 11 proptest! { 12 #[test] 13 /// **Feature: ferris-proof, Property 6: CLI verification level initialization** 14 /// **Validates: Requirements 6.1** 15 fn cli_verification_level_initialization( 16 level in prop::sample::select(vec![ 17 VerificationLevel::Minimal, 18 VerificationLevel::Standard, 19 VerificationLevel::Strict, 20 VerificationLevel::Formal, 21 ]) 22 ) { 23 let _guard = WORKING_DIR_MUTEX.lock().unwrap(); 24 25 // Create a temporary directory for the test 26 let temp_dir = TempDir::new().unwrap(); 27 let original_dir = std::env::current_dir().unwrap(); 28 29 // Change to the temporary directory 30 std::env::set_current_dir(temp_dir.path()).unwrap(); 31 32 // Run the init command 33 let rt = tokio::runtime::Runtime::new().unwrap(); 34 let result = rt.block_on(async { 35 init::run(level, false, None).await 36 }); 37 38 // Verify the command succeeded 39 prop_assert!(result.is_ok()); 40 prop_assert_eq!(result.unwrap(), 0); 41 42 // Verify ferrisproof.toml was created while still in temp directory 43 prop_assert!(std::path::Path::new("ferrisproof.toml").exists()); 44 45 // Parse the configuration file 46 let config_content = fs::read_to_string("ferrisproof.toml").unwrap(); 47 let config: ferris_proof_config::Config = toml::from_str(&config_content).unwrap(); 48 49 // Verify the configuration has the correct verification level 50 prop_assert_eq!(config.profile.level, level); 51 52 // Verify the enabled techniques match the verification level 53 let expected_techniques = match level { 54 VerificationLevel::Minimal => vec![ 55 ferris_proof_core::Technique::TypeSafety 56 ], 57 VerificationLevel::Standard => vec![ 58 ferris_proof_core::Technique::TypeSafety, 59 ferris_proof_core::Technique::PropertyTests, 60 ], 61 VerificationLevel::Strict => vec![ 62 ferris_proof_core::Technique::TypeSafety, 63 ferris_proof_core::Technique::PropertyTests, 64 ferris_proof_core::Technique::SessionTypes, 65 ferris_proof_core::Technique::RefinementTypes, 66 ferris_proof_core::Technique::ConcurrencyTesting, 67 ], 68 VerificationLevel::Formal => vec![ 69 ferris_proof_core::Technique::TypeSafety, 70 ferris_proof_core::Technique::PropertyTests, 71 ferris_proof_core::Technique::SessionTypes, 72 ferris_proof_core::Technique::RefinementTypes, 73 ferris_proof_core::Technique::ConcurrencyTesting, 74 ferris_proof_core::Technique::FormalSpecs, 75 ferris_proof_core::Technique::ModelChecking, 76 ], 77 }; 78 79 prop_assert_eq!(config.profile.enabled_techniques, expected_techniques); 80 81 // Verify appropriate directories were created while still in temp directory 82 prop_assert!(std::path::Path::new("specs").exists()); 83 prop_assert!(std::path::Path::new("tests").exists()); 84 85 // Verify level-specific directories 86 match level { 87 VerificationLevel::Minimal => { 88 // No additional directories expected 89 } 90 VerificationLevel::Standard => { 91 prop_assert!(std::path::Path::new("tests/property").exists()); 92 } 93 VerificationLevel::Strict => { 94 prop_assert!(std::path::Path::new("tests/property").exists()); 95 prop_assert!(std::path::Path::new("specs/session-types").exists()); 96 prop_assert!(std::path::Path::new("specs/refinement-types").exists()); 97 } 98 VerificationLevel::Formal => { 99 prop_assert!(std::path::Path::new("tests/property").exists()); 100 prop_assert!(std::path::Path::new("specs/session-types").exists()); 101 prop_assert!(std::path::Path::new("specs/refinement-types").exists()); 102 prop_assert!(std::path::Path::new("specs/formal").exists()); 103 prop_assert!(std::path::Path::new("specs/formal/tla").exists()); 104 prop_assert!(std::path::Path::new("specs/formal/alloy").exists()); 105 } 106 } 107 108 // Restore original directory 109 std::env::set_current_dir(original_dir).unwrap(); 110 } 111 } 112 113 #[cfg(test)] 114 mod unit_tests { 115 use super::*; 116 use tempfile::TempDir; 117 118 #[tokio::test] 119 async fn test_init_creates_config_file() { 120 let _guard = WORKING_DIR_MUTEX.lock().unwrap(); 121 122 let temp_dir = TempDir::new().unwrap(); 123 let temp_path = temp_dir.path().to_path_buf(); 124 let original_dir = std::env::current_dir().unwrap(); 125 126 std::env::set_current_dir(&temp_path).unwrap(); 127 128 let result = init::run(VerificationLevel::Standard, false, None).await; 129 130 // Check that config file was created while still in temp directory 131 assert!(std::path::Path::new("ferrisproof.toml").exists()); 132 133 // Restore directory before checking result to avoid issues with temp dir cleanup 134 std::env::set_current_dir(original_dir).unwrap(); 135 136 // Check result 137 assert!(result.is_ok()); 138 assert_eq!(result.unwrap(), 0); 139 } 140 141 #[tokio::test] 142 async fn test_init_creates_directories() { 143 let _guard = WORKING_DIR_MUTEX.lock().unwrap(); 144 145 let temp_dir = TempDir::new().unwrap(); 146 let temp_path = temp_dir.path().to_path_buf(); 147 let original_dir = std::env::current_dir().unwrap(); 148 149 std::env::set_current_dir(&temp_path).unwrap(); 150 151 let result = init::run(VerificationLevel::Formal, false, None).await; 152 153 // Check that all expected directories exist while still in temp directory 154 assert!(std::path::Path::new("specs").exists()); 155 assert!(std::path::Path::new("tests").exists()); 156 assert!(std::path::Path::new("tests/property").exists()); 157 assert!(std::path::Path::new("specs/formal").exists()); 158 assert!(std::path::Path::new("specs/formal/tla").exists()); 159 assert!(std::path::Path::new("specs/formal/alloy").exists()); 160 161 // Restore directory before checking result to avoid issues with temp dir cleanup 162 std::env::set_current_dir(original_dir).unwrap(); 163 164 // Check result 165 assert!(result.is_ok()); 166 assert_eq!(result.unwrap(), 0); 167 } 168 }