diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 40b2420903..30740272b0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -197,7 +197,7 @@ jobs: working-directory: ./source run: | # check cvc5 - cargo run --release -p rust_verify -- -V cvc5 ../examples/assorted_demo.rs + cargo run --release -p rust_verify -- --mcp -V cvc5 ../examples/assorted_demo.rs CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p air CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p rust_verify_test diff --git a/BUILD.md b/BUILD.md index a4f8cc7a03..8022384d4a 100644 --- a/BUILD.md +++ b/BUILD.md @@ -106,7 +106,7 @@ After running the build steps above, you can verify an example file. From the `source` directory, run: ``` -vargo run -p rust_verify --release -- ../examples/vectors.rs +vargo run -p rust_verify --release -- --mcp ../examples/vectors.rs ``` This will make sure that the Verus and `vstd` builds are up-to-date, then run the verifier. @@ -116,13 +116,13 @@ You can also run the verifier directly (skipping the up-to-date check) with: on Linux and macOS: ``` -./target-verus/release/verus ../examples/vectors.rs +./target-verus/release/verus --mcp ../examples/vectors.rs ``` on Windows: ``` -.\target-verus\release\verus.exe ..\examples\vectors.rs +.\target-verus\release\verus.exe --mcp ..\examples\vectors.rs ``` You should see something like the following, indicating that verification was a success: @@ -136,14 +136,14 @@ You can also add the `--compile` flag, which tells Verus to compile the Verus co on Linux and macOS: ``` -./target-verus/release/verus ../examples/doubly_linked_xor.rs --compile +./target-verus/release/verus --mcp ../examples/doubly_linked_xor.rs --compile ./doubly_linked_xor ``` on Windows: ``` -.\target-verus\release\verus.exe ..\examples\doubly_linked_xor.rs --compile +.\target-verus\release\verus.exe --mcp ..\examples\doubly_linked_xor.rs --compile .\doubly_linked_xor.exe ``` diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e1b99bc733..cd0f7ac6a2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -235,7 +235,7 @@ run, from the project root: ``` cd source/vstd -../target-verus/release/verus --crate-type=lib --is-vstd vstd.rs --cfg 'feature="std"' --cfg 'feature="alloc"' +../target-verus/release/verus --mcp --crate-type=lib --is-vstd vstd.rs --cfg 'feature="std"' --cfg 'feature="alloc"' ``` ### Common conventions diff --git a/source/rust_verify/src/main.rs b/source/rust_verify/src/main.rs index 19b1d75473..2df81bd854 100644 --- a/source/rust_verify/src/main.rs +++ b/source/rust_verify/src/main.rs @@ -6,6 +6,28 @@ extern crate rustc_driver; extern crate rustc_log; extern crate rustc_session; +const MCP_REQUIRED_MESSAGE: &str = "rust_verify is only meant to be invoked by the MCP server, not directly from bash; use the `verus` MCP server's tools instead (or pass `--mcp` if you really are the MCP server)"; + +fn consume_mcp_flag(args: impl IntoIterator) -> (bool, Vec) { + let mut mcp = false; + let args = args + .into_iter() + .filter(|arg| { + if arg == "--mcp" { + mcp = true; + false + } else { + true + } + }) + .collect(); + (mcp, args) +} + +fn authorize_mcp(mcp: bool, via_cargo: bool) -> Result<(), &'static str> { + if mcp || via_cargo { Ok(()) } else { Err(MCP_REQUIRED_MESSAGE) } +} + #[cfg(target_family = "windows")] fn os_setup() -> Result<(), Box> { // Configure Windows to kill the child SMT process if the parent is killed @@ -27,10 +49,15 @@ fn os_setup() -> Result<(), Box> { pub fn main() { let mut dep_tracker = rust_verify::cargo_verus_dep_tracker::DepTracker::init(); let via_cargo = dep_tracker.compare_env(rust_verify::cargo_verus::VERUS_DRIVER_VIA_CARGO, "1"); + let (mcp, process_args) = consume_mcp_flag(std::env::args()); + if let Err(message) = authorize_mcp(mcp, via_cargo) { + eprintln!("error: {message}"); + std::process::exit(1); + } // For now, verus_builtin, vstd, etc. must be rebuilt for each via_cargo crate: let via_cargo_rebuild_verus_libs = via_cargo; - let mut internal_args = std::env::args(); + let mut internal_args = process_args.clone().into_iter(); let internal_program = internal_args.next().unwrap(); let (build_test_mode, has_rustc) = if let Some(first_arg) = internal_args.next() { match first_arg.as_str() { @@ -71,7 +98,8 @@ pub fn main() { std::process::exit(1); } - let mut args = if build_test_mode || via_cargo { internal_args } else { std::env::args() }; + let mut args = + if build_test_mode || via_cargo { internal_args } else { process_args.into_iter() }; let program = if build_test_mode || via_cargo { internal_program } else { args.next().unwrap() }; @@ -561,3 +589,41 @@ pub fn main() { } } } + +#[cfg(test)] +mod tests { + use super::{MCP_REQUIRED_MESSAGE, authorize_mcp, consume_mcp_flag}; + + #[test] + fn mcp_flag_is_consumed_before_normal_argument_parsing() { + let (mcp, args) = + consume_mcp_flag(["rust_verify", "input.rs", "--mcp", "--version"].map(str::to_owned)); + + assert!(mcp); + assert_eq!(args, ["rust_verify", "input.rs", "--version"]); + } + + #[test] + fn missing_mcp_flag_is_reported() { + let (mcp, args) = + consume_mcp_flag(["rust_verify", "input.rs", "--version"].map(str::to_owned)); + + assert!(!mcp); + assert_eq!(args, ["rust_verify", "input.rs", "--version"]); + assert_eq!(authorize_mcp(mcp, false), Err(MCP_REQUIRED_MESSAGE)); + } + + #[test] + fn every_mcp_flag_is_removed() { + let (mcp, args) = + consume_mcp_flag(["rust_verify", "--mcp", "input.rs", "--mcp"].map(str::to_owned)); + + assert!(mcp); + assert_eq!(args, ["rust_verify", "input.rs"]); + } + + #[test] + fn cargo_wrapper_invocation_remains_authorized() { + assert_eq!(authorize_mcp(false, true), Ok(())); + } +} diff --git a/source/rust_verify/src/trait_check.rs b/source/rust_verify/src/trait_check.rs index d1efc1badc..db9356a21d 100644 --- a/source/rust_verify/src/trait_check.rs +++ b/source/rust_verify/src/trait_check.rs @@ -269,7 +269,7 @@ pub(crate) fn check_trait_conflicts<'tcx>( if let Some(mut file) = tc_log_file { write!(file, "{}", rust_code).expect("error writing to trait-conflict log file"); } - let rustc_args = [TC_DRIVER_ARG, TCFileLoader::FILENAME, "--error-format=json"]; + let rustc_args = ["--mcp", TC_DRIVER_ARG, TCFileLoader::FILENAME, "--error-format=json"]; let mut child = std::process::Command::new(std::env::current_exe().unwrap()) // avoid warning about jobserver fd diff --git a/source/rust_verify_test/tests/common/mod.rs b/source/rust_verify_test/tests/common/mod.rs index 301269d2df..20be511927 100644 --- a/source/rust_verify_test/tests/common/mod.rs +++ b/source/rust_verify_test/tests/common/mod.rs @@ -287,7 +287,7 @@ pub fn run_verus( #[cfg(target_os = "windows")] std::thread::sleep(std::time::Duration::from_millis(1000)); - let mut verus_args = Vec::new(); + let mut verus_args = vec!["--mcp".to_string()]; let mut no_external_by_default = false; let mut is_core = false; let mut use_internal_test_mode = true; @@ -478,6 +478,7 @@ pub fn run_verus_raw(args: &[&str], dir: &std::path::Path) -> std::process::Outp std::process::Command::new(bin) .current_dir(dir) .env("VERUS_Z3_PATH", z3) + .arg("--mcp") .args(args) .stdout(std::process::Stdio::piped()) .stderr(std::process::Stdio::piped()) diff --git a/source/verus/src/main.rs b/source/verus/src/main.rs index c94d4effda..2476ea6413 100644 --- a/source/verus/src/main.rs +++ b/source/verus/src/main.rs @@ -212,6 +212,11 @@ fn run() -> Result { } else { Command::new(verus_root.join(RUST_VERIFY_FILE_NAME)) }; + if !via_cargo { + // The wrapper consumed the user-facing flag. Forward authorization so + // invoking rust_verify directly cannot bypass the same gate. + cmd.arg("--mcp"); + } let vstd_kind = get_vstd_kind(&args); cmd.env("VSTD_KIND", vstd_kind); diff --git a/source/vstd_build/src/main.rs b/source/vstd_build/src/main.rs index 6b849bf231..947697f25c 100644 --- a/source/vstd_build/src/main.rs +++ b/source/vstd_build/src/main.rs @@ -150,6 +150,7 @@ fn main() { let mut child = std::process::Command::new(cmd); child.env("RUST_MIN_STACK", (10 * 1024 * 1024).to_string()); child.env("VSTD_KIND", "IsVstd"); + child.arg("--mcp"); child.args(&child_args[..]); if verbose {