1  use ferris_proof_cli::commands::init;
  2  use ferris_proof_core::models::config::VerificationLevel;
  3  use proptest::prelude::*;
  4  use std::fs;
  5  use std::path::PathBuf;
  6  use tempfile::{tempdir, TempDir};
  7  use tokio::sync::Mutex;
  8  
  9  lazy_static::lazy_static! {
 10      // Use a tokio Mutex to make it async-aware
 11      static ref WORKING_DIR_MUTEX: Mutex<()> = Mutex::new(());
 12  }
 13  
 14  /// Represents the outcome of an `init` command execution for property testing.
 15  #[derive(Debug, Clone)]
 16  struct InitCommandOutcome {
 17      level: VerificationLevel,
 18      created_config: bool,
 19      created_specs_dir: bool,
 20      created_tests_dir: bool,
 21      config_content_valid: bool,
 22      temp_dir: Option<PathBuf>, // Keep track of the temp dir path for cleanup
 23  }
 24  
 25  /// Strategy to generate different verification levels for testing.
 26  fn verification_level_strategy() -> impl Strategy<Value = VerificationLevel> {
 27      prop_oneof![
 28          Just(VerificationLevel::Minimal),
 29          Just(VerificationLevel::Standard),
 30          Just(VerificationLevel::Strict),
 31          Just(VerificationLevel::Formal),
 32      ]
 33  }
 34  
 35  /// Runs the `init` command in a temporary directory and captures the outcome.
 36  async fn run_init_and_capture_outcome(level: VerificationLevel) -> (InitCommandOutcome, TempDir) {
 37      let dir = tempdir().unwrap();
 38      let project_path = dir.path().to_path_buf();
 39  
 40      // Set current directory for the test
 41      std::env::set_current_dir(&project_path).unwrap();
 42  
 43      let result = init::run(level.clone(), false, None).await;
 44      assert!(result.is_ok());
 45  
 46      let config_path = project_path.join("ferrisproof.toml");
 47      let created_config = config_path.exists();
 48      let created_specs_dir = project_path.join("specs").is_dir();
 49      let created_tests_dir = project_path.join("tests").is_dir();
 50  
 51      let config_content_valid = if created_config {
 52          let content = fs::read_to_string(&config_path).unwrap();
 53          content.contains(&format!("level = \"{}\"", level.to_string().to_lowercase()))
 54      } else {
 55          false
 56      };
 57  
 58      (
 59          InitCommandOutcome {
 60              level,
 61              created_config,
 62              created_specs_dir,
 63              created_tests_dir,
 64              config_content_valid,
 65              temp_dir: Some(project_path),
 66          },
 67          dir, // Return the TempDir to keep it in scope
 68      )
 69  }
 70  
 71  proptest! {
 72      #![proptest_config(ProptestConfig::with_cases(10))]
 73  
 74      /// Property: The `init` command should always create the configuration file and standard directories.
 75      #[test]
 76      fn prop_init_creates_required_files(level in verification_level_strategy()) {
 77          tokio::runtime::Runtime::new().unwrap().block_on(async {
 78              // Lock the async mutex
 79              let _guard = WORKING_DIR_MUTEX.lock().await;
 80  
 81              let (outcome, _dir) = run_init_and_capture_outcome(level).await;
 82  
 83              prop_assert!(outcome.created_config, "ferrisproof.toml should be created");
 84              prop_assert!(outcome.created_specs_dir, "specs directory should be created");
 85              prop_assert!(outcome.created_tests_dir, "tests directory should be created");
 86              prop_assert!(outcome.config_content_valid, "ferrisproof.toml should have the correct level");
 87          });
 88      }
 89  
 90      /// Property: The generated `ferrisproof.toml` should always contain the correct verification level.
 91      #[test]
 92      fn prop_init_config_contains_correct_level(level in verification_level_strategy()) {
 93          tokio::runtime::Runtime::new().unwrap().block_on(async {
 94              // Lock the async mutex
 95              let _guard = WORKING_DIR_MUTEX.lock().await;
 96  
 97              let (outcome, _dir) = run_init_and_capture_outcome(level).await;
 98  
 99              prop_assert!(outcome.config_content_valid, "Generated config must contain the correct verification level");
100          });
101      }
102  }
103  
104  #[tokio::test]
105  async fn test_init_standard_level() {
106      // Lock the async mutex
107      let _guard = WORKING_DIR_MUTEX.lock().await;
108      let dir = tempdir().unwrap();
109      std::env::set_current_dir(dir.path()).unwrap();
110  
111      let result = init::run(VerificationLevel::Standard, false, None).await;
112      assert!(result.is_ok());
113  
114      let config_path = dir.path().join("ferrisproof.toml");
115      assert!(config_path.exists());
116  
117      let content = fs::read_to_string(config_path).unwrap();
118      assert!(content.contains("level = \"standard\""));
119      assert!(content.contains("cache_enabled = true"));
120  
121      dir.close().unwrap();
122  }
123  
124  #[tokio::test]
125  async fn test_init_formal_level() {
126      // Lock the async mutex
127      let _guard = WORKING_DIR_MUTEX.lock().await;
128      let dir = tempdir().unwrap();
129      std::env::set_current_dir(dir.path()).unwrap();
130  
131      let result = init::run(VerificationLevel::Formal, false, None).await;
132      assert!(result.is_ok());
133  
134      let config_path = dir.path().join("ferrisproof.toml");
135      assert!(config_path.exists());
136  
137      let content = fs::read_to_string(config_path).unwrap();
138      assert!(content.contains("level = \"formal\""));
139      assert!(content.contains("[[profile.enabled_techniques]]"));
140  
141      dir.close().unwrap();
142  }