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,