From 29c2cd824815161669d4e1f6e70ed62390403805 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 17:45:18 +0000 Subject: [PATCH] fix(server): drop the unwraps in apply_tactic; mark the test fixture module The Hypatia baseline gate fails with three unfiltered findings: * code_safety/unwrap_without_check in src/rust/server/session.rs. The handler checked state.is_none() and then unwrapped four times. Bind the state with let-else instead, take the goal counts from the values in hand, and clear goals through if-let on QED. Behaviour is the same. * code_safety/expect_in_hot_path and code_safety/panic_macro in src/rust/provers/test_fixture.rs. The module is compiled only under #[cfg(all(test, unix))] (provers/mod.rs); a failed fixture setup must fail the test. Hypatia strips only a trailing #[cfg(test)] block in the same file, so it cannot see this. Record that with file-level hypatia: allow directives rather than baseline entries. Checked with Hypatia main's code_safety scan: the three findings are present without this change and absent with it. cargo fmt --check and cargo clippy --lib -D warnings pass; cargo test --lib server passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4 --- src/rust/provers/test_fixture.rs | 2 ++ src/rust/server/session.rs | 15 +++++++++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/rust/provers/test_fixture.rs b/src/rust/provers/test_fixture.rs index c148a3bf..027cfd66 100644 --- a/src/rust/provers/test_fixture.rs +++ b/src/rust/provers/test_fixture.rs @@ -1,4 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 +// hypatia: allow code_safety/expect_in_hot_path -- test-only module, compiled only under #[cfg(all(test, unix))] in provers/mod.rs +// hypatia: allow code_safety/panic_macro -- test-only module; a failed fixture setup must fail the test //! Test-only helper for writing an executable fixture script. //! //! Writing a script and executing it straight away races with every other diff --git a/src/rust/server/session.rs b/src/rust/server/session.rs index 9891e3b6..6ce08d10 100644 --- a/src/rust/server/session.rs +++ b/src/rust/server/session.rs @@ -90,17 +90,17 @@ pub(super) async fn apply_tactic_handler( let mut session = session_arc.lock().await; // Ensure we have a state - if session.state.is_none() { + let Some(proof_state) = session.state.as_ref() else { return Err(AppError::BadRequest( "No proof loaded in session".to_string(), )); - } + }; + let goals_before = proof_state.goals.len(); // Parse tactic (simplified) let tactic = parse_tactic_from_json(&req.tactic)?; // Apply tactic - let proof_state = session.state.as_ref().unwrap(); let result = session .prover .apply_tactic(proof_state, &tactic) @@ -110,13 +110,14 @@ pub(super) async fn apply_tactic_handler( match result { TacticResult::Success(new_state) => { let complete = new_state.is_complete(); + let goals_remaining = new_state.goals.len(); session.state = Some(new_state); session.history.push(req.tactic.clone()); Ok(Json(ApplyTacticResponse { success: true, complete, - goals_remaining: session.state.as_ref().unwrap().goals.len(), + goals_remaining, message: "Tactic applied successfully".to_string(), })) }, @@ -124,12 +125,14 @@ pub(super) async fn apply_tactic_handler( TacticResult::Error(msg) => Ok(Json(ApplyTacticResponse { success: false, complete: false, - goals_remaining: session.state.as_ref().unwrap().goals.len(), + goals_remaining: goals_before, message: msg, })), TacticResult::QED => { - session.state.as_mut().unwrap().goals.clear(); + if let Some(state) = session.state.as_mut() { + state.goals.clear(); + } Ok(Json(ApplyTacticResponse { success: true,