fix(server): drop the unwraps in apply_tactic; mark the test fixture module

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

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,26 +110,29 @@ 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(),
             }))
         },
 
         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,