fix(ci): complete Ast import removal in verification/mod.rs and cargo fmt across crate (#44)

## Summary

Closes the remaining Rust CI red on `main` after #43 (steamworks 0.12.2
→ 0.13.1):

- **`coverage` job** was still failing with `error: unused import: Ast`
at `src/verification/mod.rs:81`. The fix-up commit `9435baa` removed the
same import from `src/verification/z3_integration.rs` but missed this
second occurrence. Removed.
- **`test` job** was exit-1-ing on `cargo fmt --check`. Ran `cargo fmt
--all` across the crate — 12 files reformatted, no semantic change
(struct-literal expansion + use-ordering).

The `security` job was cancelled by an Actions runner shutdown signal
during the `cargo-outdated` install — looks transient, not code-related,
and should pass on rerun.

## Test plan
- [ ] `cargo fmt --all -- --check` clean.
- [ ] `cargo build --features z3-verify` succeeds.
- [ ] `coverage`, `test`, and `security` Rust CI jobs go green on this
branch.

Author: hyperpolymath

.github/workflows/hypatia-scan.yml

@@ -79,7 +79,7 @@ jobs:
           echo "- Medium: $MEDIUM" >> $GITHUB_STEP_SUMMARY
 
       - name: Upload findings artifact
-        uses: actions/upload-artifact@65c79d7f54e76e4e3c7a8f34db0f4ac8b515c478 # v4
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
           name: hypatia-findings
           path: hypatia-findings.json

benches/proof_of_work_bench.rs

@@ -17,20 +17,50 @@ use proof_of_work::{BoardState, GoalCondition, Level, LogicPiece};
 /// Create a populated board with assumptions, gates, goals, and wires.
 fn populated_board() -> BoardState {
     let pieces = vec![
-        LogicPiece::Assumption { formula: "P".into(), position: (2, 5) },
-        LogicPiece::Assumption { formula: "Q".into(), position: (2, 3) },
-        LogicPiece::Assumption { formula: "R".into(), position: (1, 7) },
-        LogicPiece::Goal { formula: "S".into(), position: (15, 5) },
-        LogicPiece::Goal { formula: "T".into(), position: (15, 10) },
+        LogicPiece::Assumption {
+            formula: "P".into(),
+            position: (2, 5),
+        },
+        LogicPiece::Assumption {
+            formula: "Q".into(),
+            position: (2, 3),
+        },
+        LogicPiece::Assumption {
+            formula: "R".into(),
+            position: (1, 7),
+        },
+        LogicPiece::Goal {
+            formula: "S".into(),
+            position: (15, 5),
+        },
+        LogicPiece::Goal {
+            formula: "T".into(),
+            position: (15, 10),
+        },
         LogicPiece::AndIntro { position: (5, 4) },
         LogicPiece::OrIntro { position: (8, 6) },
         LogicPiece::ImpliesIntro { position: (10, 4) },
         LogicPiece::NotIntro { position: (12, 8) },
-        LogicPiece::Wire { from: (3, 5), to: (5, 4) },
-        LogicPiece::Wire { from: (3, 3), to: (5, 4) },
-        LogicPiece::Wire { from: (6, 4), to: (8, 6) },
-        LogicPiece::Wire { from: (9, 6), to: (10, 4) },
-        LogicPiece::Wire { from: (11, 4), to: (15, 5) },
+        LogicPiece::Wire {
+            from: (3, 5),
+            to: (5, 4),
+        },
+        LogicPiece::Wire {
+            from: (3, 3),
+            to: (5, 4),
+        },
+        LogicPiece::Wire {
+            from: (6, 4),
+            to: (8, 6),
+        },
+        LogicPiece::Wire {
+            from: (9, 6),
+            to: (10, 4),
+        },
+        LogicPiece::Wire {
+            from: (11, 4),
+            to: (15, 5),
+        },
     ];
     BoardState::with_pieces(20, 20, pieces)
 }
@@ -43,17 +73,28 @@ fn verifiable_level() -> Level {
         description: "P AND Q implies R".into(),
         theorem: "(assert (=> (and P Q) R))".into(),
         initial_state: BoardState::new(10, 10),
-        goal_state: GoalCondition::ProveFormula { formula: "R".into() },
+        goal_state: GoalCondition::ProveFormula {
+            formula: "R".into(),
+        },
     }
 }
 
 /// Pieces that form a valid proof for the verifiable level (AND gate adjacent to
 /// both assumptions and the goal).
 fn valid_proof_pieces() -> Vec<LogicPiece> {
     vec![
-        LogicPiece::Assumption { formula: "P".into(), position: (2, 5) },
-        LogicPiece::Assumption { formula: "Q".into(), position: (2, 3) },
-        LogicPiece::Goal { formula: "R".into(), position: (5, 4) },
+        LogicPiece::Assumption {
+            formula: "P".into(),
+            position: (2, 5),
+        },
+        LogicPiece::Assumption {
+            formula: "Q".into(),
+            position: (2, 3),
+        },
+        LogicPiece::Goal {
+            formula: "R".into(),
+            position: (5, 4),
+        },
         LogicPiece::AndIntro { position: (3, 4) },
     ]
 }
@@ -154,10 +195,19 @@ fn bench_validate_board(c: &mut Criterion) {
 fn bench_validate_piece_placement(c: &mut Criterion) {
     let board = populated_board();
     let pieces = [
-        LogicPiece::Assumption { formula: "X".into(), position: (0, 0) },
-        LogicPiece::Wire { from: (3, 3), to: (7, 7) },
+        LogicPiece::Assumption {
+            formula: "X".into(),
+            position: (0, 0),
+        },
+        LogicPiece::Wire {
+            from: (3, 3),
+            to: (7, 7),
+        },
         LogicPiece::AndIntro { position: (99, 99) }, // out of bounds
-        LogicPiece::Goal { formula: "".into(), position: (4, 4) }, // empty formula
+        LogicPiece::Goal {
+            formula: "".into(),
+            position: (4, 4),
+        }, // empty formula
     ];
 
     c.bench_function("validate_piece_placement_4_pieces", |b| {
@@ -178,9 +228,7 @@ fn bench_is_ready_for_verification(c: &mut Criterion) {
     let board = populated_board();
 
     c.bench_function("is_ready_for_verification", |b| {
-        b.iter(|| {
-            black_box(validation::is_ready_for_verification(&board))
-        });
+        b.iter(|| black_box(validation::is_ready_for_verification(&board)));
     });
 }
 
@@ -253,9 +301,18 @@ fn bench_verify_level_solution(c: &mut Criterion) {
 fn bench_verify_level_solution_invalid(c: &mut Criterion) {
     let level = verifiable_level();
     let pieces = vec![
-        LogicPiece::Assumption { formula: "P".into(), position: (0, 0) },
-        LogicPiece::Assumption { formula: "Q".into(), position: (0, 19) },
-        LogicPiece::Goal { formula: "R".into(), position: (19, 19) },
+        LogicPiece::Assumption {
+            formula: "P".into(),
+            position: (0, 0),
+        },
+        LogicPiece::Assumption {
+            formula: "Q".into(),
+            position: (0, 19),
+        },
+        LogicPiece::Goal {
+            formula: "R".into(),
+            position: (19, 19),
+        },
         LogicPiece::AndIntro { position: (10, 10) }, // too far from everything
     ];
 
@@ -272,11 +329,20 @@ fn bench_verify_level_solution_invalid(c: &mut Criterion) {
 /// Benchmark serialization of a LogicPiece to SMT format.
 fn bench_piece_to_smt(c: &mut Criterion) {
     let pieces = [
-        LogicPiece::Assumption { formula: "P".into(), position: (2, 5) },
-        LogicPiece::Goal { formula: "Q".into(), position: (8, 4) },
+        LogicPiece::Assumption {
+            formula: "P".into(),
+            position: (2, 5),
+        },
+        LogicPiece::Goal {
+            formula: "Q".into(),
+            position: (8, 4),
+        },
         LogicPiece::AndIntro { position: (5, 5) },
         LogicPiece::ImpliesIntro { position: (3, 3) },
-        LogicPiece::ForallIntro { position: (1, 1), variable: "x".into() },
+        LogicPiece::ForallIntro {
+            position: (1, 1),
+            variable: "x".into(),
+        },
     ];
 
     c.bench_function("piece_to_smt_5_pieces", |b| {

src/editor/ui.rs

@@ -4,7 +4,9 @@
 use bevy::prelude::*;
 use bevy_egui::{egui, EguiContexts};
 
-use super::{EditorEntity, EditorPieceType, EditorState, EditorTool, SaveLevelEvent, TestLevelEvent};
+use super::{
+    EditorEntity, EditorPieceType, EditorState, EditorTool, SaveLevelEvent, TestLevelEvent,
+};
 use crate::game::{GoalCondition, LogicPiece};
 use crate::levels::LevelPackManager;
 use crate::states::GameState;
@@ -124,10 +126,7 @@ pub fn editor_ui_system(
 
             for piece_type in piece_types {
                 let selected = editor.selected_piece == Some(piece_type);
-                if ui
-                    .selectable_label(selected, piece_type.name())
-                    .clicked()
-                {
+                if ui.selectable_label(selected, piece_type.name()).clicked() {
                     editor.selected_piece = Some(piece_type);
                     editor.tool = EditorTool::Place;
                 }
@@ -173,10 +172,7 @@ pub fn editor_ui_system(
             ui.separator();
 
             ui.label("Name:");
-            if ui
-                .text_edit_singleline(&mut editor.level.name)
-                .changed()
-            {
+            if ui.text_edit_singleline(&mut editor.level.name).changed() {
                 editor.dirty = true;
             }
 
@@ -191,10 +187,7 @@ pub fn editor_ui_system(
 
             ui.add_space(5.0);
             ui.label("Theorem (SMT-LIB2):");
-            if ui
-                .text_edit_singleline(&mut editor.level.theorem)
-                .changed()
-            {
+            if ui.text_edit_singleline(&mut editor.level.theorem).changed() {
                 editor.dirty = true;
             }
 
@@ -207,14 +200,20 @@ pub fn editor_ui_system(
 
             ui.horizontal(|ui| {
                 ui.label("Width:");
-                if ui.add(egui::DragValue::new(&mut width).range(3..=20)).changed() {
+                if ui
+                    .add(egui::DragValue::new(&mut width).range(3..=20))
+                    .changed()
+                {
                     editor.set_grid_size(width as u32, height as u32);
                 }
             });
 
             ui.horizontal(|ui| {
                 ui.label("Height:");
-                if ui.add(egui::DragValue::new(&mut height).range(3..=20)).changed() {
+                if ui
+                    .add(egui::DragValue::new(&mut height).range(3..=20))
+                    .changed()
+                {
                     editor.set_grid_size(width as u32, height as u32);
                 }
             });
@@ -396,10 +395,7 @@ pub fn editor_input_system(
 }
 
 /// Spawn editor grid visualization
-pub fn spawn_editor_grid(
-    mut commands: Commands,
-    editor: Res<EditorState>,
-) {
+pub fn spawn_editor_grid(mut commands: Commands, editor: Res<EditorState>) {
     let half_width = editor.grid_width as f32 / 2.0;
     let half_height = editor.grid_height as f32 / 2.0;
 

src/game/validation.rs

@@ -10,11 +10,20 @@ use super::{BoardState, GoalCondition, Level, LogicPiece};
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum ValidationError {
     /// Piece is placed outside board boundaries.
-    OutOfBounds { x: u32, y: u32, max_x: u32, max_y: u32 },
+    OutOfBounds {
+        x: u32,
+        y: u32,
+        max_x: u32,
+        max_y: u32,
+    },
     /// Two pieces occupy the same position.
     OverlappingPieces { position: (u32, u32) },
     /// Wire endpoints are invalid.
-    InvalidWire { from: (u32, u32), to: (u32, u32), reason: String },
+    InvalidWire {
+        from: (u32, u32),
+        to: (u32, u32),
+        reason: String,
+    },
     /// No goals defined on the board.
     NoGoals,
     /// No assumptions defined on the board.
@@ -62,7 +71,10 @@ impl ValidationResult {
 }
 
 /// Validate a piece placement on the board.
-pub fn validate_piece_placement(board: &BoardState, piece: &LogicPiece) -> Result<(), ValidationError> {
+pub fn validate_piece_placement(
+    board: &BoardState,
+    piece: &LogicPiece,
+) -> Result<(), ValidationError> {
     let (x, y) = piece.position();
 
     // Check bounds
@@ -118,7 +130,11 @@ pub fn validate_piece_placement(board: &BoardState, piece: &LogicPiece) -> Resul
                 });
             }
             // Basic formula validation: must start with alphanumeric or parenthesis
-            if !formula.chars().next().map_or(false, |c| c.is_alphanumeric() || c == '(') {
+            if !formula
+                .chars()
+                .next()
+                .map_or(false, |c| c.is_alphanumeric() || c == '(')
+            {
                 return Err(ValidationError::InvalidFormula {
                     formula: formula.clone(),
                     reason: "Formula must start with identifier or parenthesis".to_string(),
@@ -161,8 +177,14 @@ pub fn validate_board(board: &BoardState) -> ValidationResult {
     }
 
     // Check for at least one assumption and one goal
-    let has_assumptions = board.pieces.iter().any(|p| matches!(p, LogicPiece::Assumption { .. }));
-    let has_goals = board.pieces.iter().any(|p| matches!(p, LogicPiece::Goal { .. }));
+    let has_assumptions = board
+        .pieces
+        .iter()
+        .any(|p| matches!(p, LogicPiece::Assumption { .. }));
+    let has_goals = board
+        .pieces
+        .iter()
+        .any(|p| matches!(p, LogicPiece::Goal { .. }));
 
     if !has_assumptions {
         errors.push(ValidationError::NoAssumptions);
@@ -221,7 +243,10 @@ pub fn validate_level(level: &Level) -> ValidationResult {
     match &level.goal_state {
         GoalCondition::ConnectNodes { start, end } => {
             if start.0 >= level.initial_state.width || start.1 >= level.initial_state.height {
-                warnings.push(format!("Goal start node {:?} is outside board bounds", start));
+                warnings.push(format!(
+                    "Goal start node {:?} is outside board bounds",
+                    start
+                ));
             }
             if end.0 >= level.initial_state.width || end.1 >= level.initial_state.height {
                 warnings.push(format!("Goal end node {:?} is outside board bounds", end));
@@ -296,11 +321,16 @@ mod tests {
     #[test]
     fn test_out_of_bounds() {
         let mut board = make_test_board();
-        board.pieces.push(LogicPiece::OrIntro { position: (15, 15) });
+        board
+            .pieces
+            .push(LogicPiece::OrIntro { position: (15, 15) });
 
         let result = validate_board(&board);
         assert!(!result.is_valid);
-        assert!(result.errors.iter().any(|e| matches!(e, ValidationError::OutOfBounds { .. })));
+        assert!(result
+            .errors
+            .iter()
+            .any(|e| matches!(e, ValidationError::OutOfBounds { .. })));
     }
 
     #[test]
@@ -310,7 +340,10 @@ mod tests {
 
         let result = validate_board(&board);
         assert!(!result.is_valid);
-        assert!(result.errors.iter().any(|e| matches!(e, ValidationError::OverlappingPieces { .. })));
+        assert!(result
+            .errors
+            .iter()
+            .any(|e| matches!(e, ValidationError::OverlappingPieces { .. })));
     }
 
     #[test]
@@ -326,7 +359,10 @@ mod tests {
 
         let result = validate_board(&board);
         assert!(!result.is_valid);
-        assert!(result.errors.iter().any(|e| matches!(e, ValidationError::NoAssumptions)));
+        assert!(result
+            .errors
+            .iter()
+            .any(|e| matches!(e, ValidationError::NoAssumptions)));
     }
 
     #[test]