/home/noah/src/ruchy/src/bin/handlers/handlers_modules/prove_helpers.rs

Source
//! Helper functions for prove command
//! Extracted to maintain ≤10 complexity per function

use anyhow::{Context, Result};
use ruchy::proving::{InteractiveProver, ProverSession, SmtBackend};
use std::fs;

/// Parse SMT backend from string
pub fn parse_smt_backend(backend: &str, verbose: bool) -> SmtBackend {
    match backend.to_lowercase().as_str() {
        "z3" => SmtBackend::Z3,
        "cvc5" => SmtBackend::CVC5,
        "yices2" => SmtBackend::Yices2,
        _ => {
            if verbose {
                eprintln!("Warning: Unknown backend '{}', defaulting to Z3", backend);
            }
            SmtBackend::Z3
        }
    }
}

/// Configure prover with settings
pub fn configure_prover(
    prover: &mut InteractiveProver,
    timeout: u64,
    ml_suggestions: bool,
    verbose: bool,
) {
    prover.set_timeout(timeout);
    prover.set_ml_suggestions(ml_suggestions);
    
    if verbose {
        println!("⚙️  Configuration:");
        println!("  Timeout: {}ms", timeout);
        println!("  ML Suggestions: {}", ml_suggestions);
    }
}

/// Load and parse file for proof checking
pub fn load_proof_file(file_path: &std::path::Path, verbose: bool) -> Result<ruchy::frontend::ast::Expr> {
    use ruchy::Parser as RuchyParser;
    
    if verbose {
        println!("📂 Loading file: {}", file_path.display());
    }
    
    let source = fs::read_to_string(file_path)
        .with_context(|| format!("Failed to read file: {}", file_path.display()))?;
    
    let mut parser = RuchyParser::new(&source);
    let ast = parser.parse()
        .with_context(|| format!("Failed to parse file: {}", file_path.display()))?;
    
    if verbose {
        println!("📋 Extracted proof goals from source");
    }
    
    Ok(ast)
}

/// Load proof script from file
pub fn load_proof_script(
    prover: &mut InteractiveProver,
    script_path: &std::path::Path,
    verbose: bool,
) -> Result<()> {
    if verbose {
        println!("📜 Loading proof script: {}", script_path.display());
    }
    
    let script_content = fs::read_to_string(script_path)
        .with_context(|| format!("Failed to read script: {}", script_path.display()))?;
    
    prover.load_script(&script_content)?;
    Ok(())
}

/// Print interactive prover help
pub fn print_prover_help() {
    println!("\nInteractive Prover Commands:");
    println!("  help          - Show this help message");
    println!("  quit/exit     - Exit the prover");
    println!("  goals         - Show current proof goals");
    println!("  tactics       - List available tactics");
    println!("  goal <stmt>   - Add a new proof goal");
    println!("  apply <tactic> - Apply a tactic to current goal");
    println!("\nTactics:");
    println!("  intro         - Introduce hypothesis from implication");
    println!("  split         - Split conjunction into subgoals");
    println!("  induction     - Proof by induction");
    println!("  contradiction - Proof by contradiction");
    println!("  reflexivity   - Prove equality by reflexivity");
    println!("  simplify      - Simplify expression");
    println!("  assumption    - Prove using an assumption");
    println!("\nExamples:");
    println!("  goal x > 0 -> x + 1 > 1");
    println!("  apply intro");
    println!("  apply simplify\n");
}

/// Handle single prover command
pub fn handle_prover_command(
    input: &str,
    prover: &mut InteractiveProver,
    session: &mut ProverSession,
    verbose: bool,
) -> Result<bool> {
    match input {
        "quit" | "exit" => {
            println!("Goodbye!");
            Ok(true) // Signal to exit
        }
        "help" => {
            print_prover_help();
            Ok(false)
        }
        "goals" => {
            print_current_goals(session);
            Ok(false)
        }
        "tactics" => {
            print_available_tactics(prover);
            Ok(false)
        }
        cmd if cmd.starts_with("apply ") => {
            apply_tactic(cmd, prover, session)?;
            Ok(false)
        }
        cmd if cmd.starts_with("goal ") => {
            add_goal(cmd, session);
            Ok(false)
        }
        _ => {
            process_general_input(input, prover, session, verbose)?;
            Ok(false)
        }
    }
}

/// Print current proof goals
fn print_current_goals(session: &ProverSession) {
    let goals = session.get_goals();
    if goals.is_empty() {
        println!("No active goals");
    } else {
        for (i, goal) in goals.iter().enumerate() {
            println!("Goal {}: {}", i + 1, goal.statement);
        }
    }
}

/// Print available tactics
fn print_available_tactics(prover: &InteractiveProver) {
    let tactics = prover.get_available_tactics();
    println!("Available tactics:");
    for tactic in tactics {
        println!("  {} - {}", tactic.name(), tactic.description());
    }
}

/// Apply a tactic to current goal
fn apply_tactic(
    cmd: &str,
    prover: &mut InteractiveProver,
    session: &mut ProverSession,
) -> Result<()> {
    let tactic_name = &cmd[6..];
    match prover.apply_tactic(session, tactic_name, &[]) {
        Ok(result) => {
            println!("Result: {:?}", result);
            Ok(())
        }
        Err(e) => {
            eprintln!("Error: {}", e);
            Err(e)
        }
    }
}

/// Add a new goal to session
fn add_goal(cmd: &str, session: &mut ProverSession) {
    let goal_stmt = &cmd[5..];
    session.add_goal(goal_stmt.to_string());
    println!("Added goal: {}", goal_stmt);
}

/// Process general input
fn process_general_input(
    input: &str,
    prover: &mut InteractiveProver,
    session: &mut ProverSession,
    verbose: bool,
) -> Result<()> {
    match prover.process_input(session, input) {
        Ok(result) => {
            if verbose {
                println!("Processed: {:?}", result);
            }
            Ok(())
        }
        Err(e) => {
            eprintln!("Error: {}", e);
            Err(e)
        }
    }
}

/// Show current prover state with ML suggestions
pub fn show_prover_state(
    session: &ProverSession,
    prover: &mut InteractiveProver,
    ml_suggestions: bool,
) {
    if session.is_complete() {
        println!("✅ All goals proved!");
    } else if let Some(current_goal) = session.current_goal() {
        println!("\nCurrent goal: {}", current_goal.statement);
        
        if ml_suggestions {
            show_ml_suggestions(prover, current_goal);
        }
    }
}

/// Show ML-powered tactic suggestions
fn show_ml_suggestions(prover: &mut InteractiveProver, goal: &ruchy::proving::ProofGoal) {
    if let Ok(suggestions) = prover.suggest_tactics(goal) {
        if !suggestions.is_empty() {
            println!("\nSuggested tactics:");
            for (i, sugg) in suggestions.iter().take(3).enumerate() {
                println!("  {}. {} (confidence: {:.2})", 
                    i + 1, sugg.tactic_name, sugg.confidence);
            }
        }
    }
}

/// Export proof to file
pub fn export_proof(
    session: &ProverSession,
    export_path: &std::path::Path,
    format: &str,
    verbose: bool,
) -> Result<()> {
    if verbose {
        println!("📝 Exporting proof to: {}", export_path.display());
    }
    
    let proof_content = match format {
        "json" => serde_json::to_string_pretty(session)?,
        "coq" => session.to_coq_proof(),
        "lean" => session.to_lean_proof(),
        _ => session.to_text_proof(),
    };
    
    fs::write(export_path, proof_content)
        .with_context(|| format!("Failed to write proof: {}", export_path.display()))?;
    
    println!("✅ Proof exported successfully");
    Ok(())
}

/// Verify proofs extracted from AST
pub fn verify_proofs_from_ast(
    ast: &ruchy::frontend::ast::Expr, 
    file_path: &std::path::Path, 
    format: &str,
    counterexample: bool, 
    verbose: bool
) -> Result<()> {
    use ruchy::proving::{extract_assertions_from_ast, verify_assertions_batch};
    
    let assertions = extract_assertions_from_ast(ast);
    
    if assertions.is_empty() {
        handle_no_assertions(file_path, format, verbose)?;
        return Ok(());
    }
    
    if verbose {
        print_assertions(&assertions);
    }
    
    let results = verify_assertions_batch(&assertions, counterexample);
    
    output_verification_results(&results, file_path, format, verbose)?;
    
    check_verification_failures(&results);
    Ok(())
}

/// Handle case when no assertions found
fn handle_no_assertions(
    file_path: &std::path::Path,
    format: &str,
    verbose: bool,
) -> Result<()> {
    if verbose {
        println!("No assertions found in {}", file_path.display());
    }
    
    if format == "json" {
        let json_result = serde_json::json!({
            "file": file_path.display().to_string(),
            "status": "no_proofs",
            "total": 0,
            "passed": 0,
            "failed": 0,
            "proofs": []
        });
        println!("{}", serde_json::to_string_pretty(&json_result)?);
    } else {
        println!("✅ No proofs found (file valid)");
    }
    
    Ok(())
}

/// Print discovered assertions
fn print_assertions(assertions: &[String]) {
    println!("Found {} assertions to verify", assertions.len());
    for (i, assertion) in assertions.iter().enumerate() {
        println!("  {}: {}", i + 1, assertion);
    }
}

/// Output verification results in requested format
fn output_verification_results(
    results: &[ruchy::proving::ProofVerificationResult],
    file_path: &std::path::Path,
    format: &str,
    verbose: bool,
) -> Result<()> {
    let total = results.len();
    let passed = results.iter().filter(|r| r.is_verified).count();
    let failed = total - passed;
    
    if format == "json" {
        output_json_results(results, file_path, total, passed, failed)?;
    } else {
        output_text_results(results, total, passed, failed, verbose);
    }
    
    Ok(())
}

/// Output results in JSON format
fn output_json_results(
    results: &[ruchy::proving::ProofVerificationResult],
    file_path: &std::path::Path,
    total: usize,
    passed: usize,
    failed: usize,
) -> Result<()> {
    let json_result = serde_json::json!({
        "file": file_path.display().to_string(),
        "status": if failed == 0 { "verified" } else { "failed" },
        "total": total,
        "passed": passed,
        "failed": failed,
        "proofs": results
    });
    println!("{}", serde_json::to_string_pretty(&json_result)?);
    Ok(())
}

/// Output results in text format
fn output_text_results(
    results: &[ruchy::proving::ProofVerificationResult],
    total: usize,
    _passed: usize,
    failed: usize,
    verbose: bool,
) {
    if failed == 0 {
        println!("✅ All {} proofs verified successfully", total);
        if verbose {
            for (i, result) in results.iter().enumerate() {
                println!("  ✅ Proof {}: {} ({:.1}ms)", 
                    i + 1, result.assertion, result.verification_time_ms);
            }
        }
    } else {
        print_failed_proofs(results, total, failed);
        if verbose {
            print_passed_proofs(results);
        }
    }
}

/// Print failed proofs
fn print_failed_proofs(
    results: &[ruchy::proving::ProofVerificationResult],
    total: usize,
    failed: usize,
) {
    println!("❌ {} of {} proofs failed verification", failed, total);
    for (i, result) in results.iter().enumerate() {
        if !result.is_verified {
            println!("  ❌ Proof {}: {}", i + 1, result.assertion);
            if let Some(ref counterex) = result.counterexample {
                println!("     Counterexample: {}", counterex);
            }
            if let Some(ref error) = result.error {
                println!("     Error: {}", error);
            }
        }
    }
}

/// Print passed proofs
fn print_passed_proofs(results: &[ruchy::proving::ProofVerificationResult]) {
    println!("\nPassed proofs:");
    for (i, result) in results.iter().enumerate() {
        if result.is_verified {
            println!("  ✅ Proof {}: {} ({:.1}ms)", 
                i + 1, result.assertion, result.verification_time_ms);
        }
    }
}

/// Check if any verifications failed and exit accordingly
fn check_verification_failures(results: &[ruchy::proving::ProofVerificationResult]) {
    let failed = results.iter().filter(|r| !r.is_verified).count();
    if failed > 0 {
        std::process::exit(1);
    }
}

Coverage Report

Created: 2025-09-08 21:26

Line	Count	Source
1		//! Helper functions for prove command
2		//! Extracted to maintain ≤10 complexity per function
3
4		use anyhow::{Context, Result};
5		use ruchy::proving::{InteractiveProver, ProverSession, SmtBackend};
6		use std::fs;
7
8		/// Parse SMT backend from string
9	0	pub fn parse_smt_backend(backend: &str, verbose: bool) -> SmtBackend {
10	0	match backend.to_lowercase().as_str() {
11	0	"z3" => SmtBackend::Z3,
12	0	"cvc5" => SmtBackend::CVC5,
13	0	"yices2" => SmtBackend::Yices2,
14		_ => {
15	0	if verbose {
16	0	eprintln!("Warning: Unknown backend '{}', defaulting to Z3", backend);
17	0	}
18	0	SmtBackend::Z3
19		}
20		}
21	0	}
22
23		/// Configure prover with settings
24	0	pub fn configure_prover(
25	0	prover: &mut InteractiveProver,
26	0	timeout: u64,
27	0	ml_suggestions: bool,
28	0	verbose: bool,
29	0	) {
30	0	prover.set_timeout(timeout);
31	0	prover.set_ml_suggestions(ml_suggestions);
32
33	0	if verbose {
34	0	println!("⚙️ Configuration:");
35	0	println!(" Timeout: {}ms", timeout);
36	0	println!(" ML Suggestions: {}", ml_suggestions);
37	0	}
38	0	}
39
40		/// Load and parse file for proof checking
41	0	pub fn load_proof_file(file_path: &std::path::Path, verbose: bool) -> Result<ruchy::frontend::ast::Expr> {
42		use ruchy::Parser as RuchyParser;
43
44	0	if verbose {
45	0	println!("📂 Loading file: {}", file_path.display());
46	0	}
47
48	0	let source = fs::read_to_string(file_path)
49	0	.with_context(\|\| format!("Failed to read file: {}", file_path.display()))?;
50
51	0	let mut parser = RuchyParser::new(&source);
52	0	let ast = parser.parse()
53	0	.with_context(\|\| format!("Failed to parse file: {}", file_path.display()))?;
54
55	0	if verbose {
56	0	println!("📋 Extracted proof goals from source");
57	0	}
58
59	0	Ok(ast)
60	0	}
61
62		/// Load proof script from file
63	0	pub fn load_proof_script(
64	0	prover: &mut InteractiveProver,
65	0	script_path: &std::path::Path,
66	0	verbose: bool,
67	0	) -> Result<()> {
68	0	if verbose {
69	0	println!("📜 Loading proof script: {}", script_path.display());
70	0	}
71
72	0	let script_content = fs::read_to_string(script_path)
73	0	.with_context(\|\| format!("Failed to read script: {}", script_path.display()))?;
74
75	0	prover.load_script(&script_content)?;
76	0	Ok(())
77	0	}
78
79		/// Print interactive prover help
80	0	pub fn print_prover_help() {
81	0	println!("\nInteractive Prover Commands:");
82	0	println!(" help - Show this help message");
83	0	println!(" quit/exit - Exit the prover");
84	0	println!(" goals - Show current proof goals");
85	0	println!(" tactics - List available tactics");
86	0	println!(" goal <stmt> - Add a new proof goal");
87	0	println!(" apply <tactic> - Apply a tactic to current goal");
88	0	println!("\nTactics:");
89	0	println!(" intro - Introduce hypothesis from implication");
90	0	println!(" split - Split conjunction into subgoals");
91	0	println!(" induction - Proof by induction");
92	0	println!(" contradiction - Proof by contradiction");
93	0	println!(" reflexivity - Prove equality by reflexivity");
94	0	println!(" simplify - Simplify expression");
95	0	println!(" assumption - Prove using an assumption");
96	0	println!("\nExamples:");
97	0	println!(" goal x > 0 -> x + 1 > 1");
98	0	println!(" apply intro");
99	0	println!(" apply simplify\n");
100	0	}
101
102		/// Handle single prover command
103	0	pub fn handle_prover_command(
104	0	input: &str,
105	0	prover: &mut InteractiveProver,
106	0	session: &mut ProverSession,
107	0	verbose: bool,
108	0	) -> Result<bool> {
109	0	match input {
110	0	"quit" \| "exit" => {
111	0	println!("Goodbye!");
112	0	Ok(true) // Signal to exit
113		}
114	0	"help" => {
115	0	print_prover_help();
116	0	Ok(false)
117		}
118	0	"goals" => {
119	0	print_current_goals(session);
120	0	Ok(false)
121		}
122	0	"tactics" => {
123	0	print_available_tactics(prover);
124	0	Ok(false)
125		}
126	0	cmd if cmd.starts_with("apply ") => {
127	0	apply_tactic(cmd, prover, session)?;
128	0	Ok(false)
129		}
130	0	cmd if cmd.starts_with("goal ") => {
131	0	add_goal(cmd, session);
132	0	Ok(false)
133		}
134		_ => {
135	0	process_general_input(input, prover, session, verbose)?;
136	0	Ok(false)
137		}
138		}
139	0	}
140
141		/// Print current proof goals
142	0	fn print_current_goals(session: &ProverSession) {
143	0	let goals = session.get_goals();
144	0	if goals.is_empty() {
145	0	println!("No active goals");
146	0	} else {
147	0	for (i, goal) in goals.iter().enumerate() {
148	0	println!("Goal {}: {}", i + 1, goal.statement);
149	0	}
150		}
151	0	}
152
153		/// Print available tactics
154	0	fn print_available_tactics(prover: &InteractiveProver) {
155	0	let tactics = prover.get_available_tactics();
156	0	println!("Available tactics:");
157	0	for tactic in tactics {
158	0	println!(" {} - {}", tactic.name(), tactic.description());
159	0	}
160	0	}
161
162		/// Apply a tactic to current goal
163	0	fn apply_tactic(
164	0	cmd: &str,
165	0	prover: &mut InteractiveProver,
166	0	session: &mut ProverSession,
167	0	) -> Result<()> {
168	0	let tactic_name = &cmd[6..];
169	0	match prover.apply_tactic(session, tactic_name, &[]) {
170	0	Ok(result) => {
171	0	println!("Result: {:?}", result);
172	0	Ok(())
173		}
174	0	Err(e) => {
175	0	eprintln!("Error: {}", e);
176	0	Err(e)
177		}
178		}
179	0	}
180
181		/// Add a new goal to session
182	0	fn add_goal(cmd: &str, session: &mut ProverSession) {
183	0	let goal_stmt = &cmd[5..];
184	0	session.add_goal(goal_stmt.to_string());
185	0	println!("Added goal: {}", goal_stmt);
186	0	}
187
188		/// Process general input
189	0	fn process_general_input(
190	0	input: &str,
191	0	prover: &mut InteractiveProver,
192	0	session: &mut ProverSession,
193	0	verbose: bool,
194	0	) -> Result<()> {
195	0	match prover.process_input(session, input) {
196	0	Ok(result) => {
197	0	if verbose {
198	0	println!("Processed: {:?}", result);
199	0	}
200	0	Ok(())
201		}
202	0	Err(e) => {
203	0	eprintln!("Error: {}", e);
204	0	Err(e)
205		}
206		}
207	0	}
208
209		/// Show current prover state with ML suggestions
210	0	pub fn show_prover_state(
211	0	session: &ProverSession,
212	0	prover: &mut InteractiveProver,
213	0	ml_suggestions: bool,
214	0	) {
215	0	if session.is_complete() {
216	0	println!("✅ All goals proved!");
217	0	} else if let Some(current_goal) = session.current_goal() {
218	0	println!("\nCurrent goal: {}", current_goal.statement);
219
220	0	if ml_suggestions {
221	0	show_ml_suggestions(prover, current_goal);
222	0	}
223	0	}
224	0	}
225
226		/// Show ML-powered tactic suggestions
227	0	fn show_ml_suggestions(prover: &mut InteractiveProver, goal: &ruchy::proving::ProofGoal) {
228	0	if let Ok(suggestions) = prover.suggest_tactics(goal) {
229	0	if !suggestions.is_empty() {
230	0	println!("\nSuggested tactics:");
231	0	for (i, sugg) in suggestions.iter().take(3).enumerate() {
232	0	println!(" {}. {} (confidence: {:.2})",
233	0	i + 1, sugg.tactic_name, sugg.confidence);
234	0	}
235	0	}
236	0	}
237	0	}
238
239		/// Export proof to file
240	0	pub fn export_proof(
241	0	session: &ProverSession,
242	0	export_path: &std::path::Path,
243	0	format: &str,
244	0	verbose: bool,
245	0	) -> Result<()> {
246	0	if verbose {
247	0	println!("📝 Exporting proof to: {}", export_path.display());
248	0	}
249
250	0	let proof_content = match format {
251	0	"json" => serde_json::to_string_pretty(session)?,
252	0	"coq" => session.to_coq_proof(),
253	0	"lean" => session.to_lean_proof(),
254	0	_ => session.to_text_proof(),
255		};
256
257	0	fs::write(export_path, proof_content)
258	0	.with_context(\|\| format!("Failed to write proof: {}", export_path.display()))?;
259
260	0	println!("✅ Proof exported successfully");
261	0	Ok(())
262	0	}
263
264		/// Verify proofs extracted from AST
265	0	pub fn verify_proofs_from_ast(
266	0	ast: &ruchy::frontend::ast::Expr,
267	0	file_path: &std::path::Path,
268	0	format: &str,
269	0	counterexample: bool,
270	0	verbose: bool
271	0	) -> Result<()> {
272		use ruchy::proving::{extract_assertions_from_ast, verify_assertions_batch};
273
274	0	let assertions = extract_assertions_from_ast(ast);
275
276	0	if assertions.is_empty() {
277	0	handle_no_assertions(file_path, format, verbose)?;
278	0	return Ok(());
279	0	}
280
281	0	if verbose {
282	0	print_assertions(&assertions);
283	0	}
284
285	0	let results = verify_assertions_batch(&assertions, counterexample);
286
287	0	output_verification_results(&results, file_path, format, verbose)?;
288
289	0	check_verification_failures(&results);
290	0	Ok(())
291	0	}
292
293		/// Handle case when no assertions found
294	0	fn handle_no_assertions(
295	0	file_path: &std::path::Path,
296	0	format: &str,
297	0	verbose: bool,
298	0	) -> Result<()> {
299	0	if verbose {
300	0	println!("No assertions found in {}", file_path.display());
301	0	}
302
303	0	if format == "json" {
304	0	let json_result = serde_json::json!({
305	0	"file": file_path.display().to_string(),
306	0	"status": "no_proofs",
307	0	"total": 0,
308	0	"passed": 0,
309	0	"failed": 0,
310	0	"proofs": []
311		});
312	0	println!("{}", serde_json::to_string_pretty(&json_result)?);
313	0	} else {
314	0	println!("✅ No proofs found (file valid)");
315	0	}
316
317	0	Ok(())
318	0	}
319
320		/// Print discovered assertions
321	0	fn print_assertions(assertions: &[String]) {
322	0	println!("Found {} assertions to verify", assertions.len());
323	0	for (i, assertion) in assertions.iter().enumerate() {
324	0	println!(" {}: {}", i + 1, assertion);
325	0	}
326	0	}
327
328		/// Output verification results in requested format
329	0	fn output_verification_results(
330	0	results: &[ruchy::proving::ProofVerificationResult],
331	0	file_path: &std::path::Path,
332	0	format: &str,
333	0	verbose: bool,
334	0	) -> Result<()> {
335	0	let total = results.len();
336	0	let passed = results.iter().filter(\|r\| r.is_verified).count();
337	0	let failed = total - passed;
338
339	0	if format == "json" {
340	0	output_json_results(results, file_path, total, passed, failed)?;
341	0	} else {
342	0	output_text_results(results, total, passed, failed, verbose);
343	0	}
344
345	0	Ok(())
346	0	}
347
348		/// Output results in JSON format
349	0	fn output_json_results(
350	0	results: &[ruchy::proving::ProofVerificationResult],
351	0	file_path: &std::path::Path,
352	0	total: usize,
353	0	passed: usize,
354	0	failed: usize,
355	0	) -> Result<()> {
356	0	let json_result = serde_json::json!({
357	0	"file": file_path.display().to_string(),
358	0	"status": if failed == 0 { "verified" } else { "failed" },
359	0	"total": total,
360	0	"passed": passed,
361	0	"failed": failed,
362	0	"proofs": results
363		});
364	0	println!("{}", serde_json::to_string_pretty(&json_result)?);
365	0	Ok(())
366	0	}
367
368		/// Output results in text format
369	0	fn output_text_results(
370	0	results: &[ruchy::proving::ProofVerificationResult],
371	0	total: usize,
372	0	_passed: usize,
373	0	failed: usize,
374	0	verbose: bool,
375	0	) {
376	0	if failed == 0 {
377	0	println!("✅ All {} proofs verified successfully", total);
378	0	if verbose {
379	0	for (i, result) in results.iter().enumerate() {
380	0	println!(" ✅ Proof {}: {} ({:.1}ms)",
381	0	i + 1, result.assertion, result.verification_time_ms);
382	0	}
383	0	}
384		} else {
385	0	print_failed_proofs(results, total, failed);
386	0	if verbose {
387	0	print_passed_proofs(results);
388	0	}
389		}
390	0	}
391
392		/// Print failed proofs
393	0	fn print_failed_proofs(
394	0	results: &[ruchy::proving::ProofVerificationResult],
395	0	total: usize,
396	0	failed: usize,
397	0	) {
398	0	println!("❌ {} of {} proofs failed verification", failed, total);
399	0	for (i, result) in results.iter().enumerate() {
400	0	if !result.is_verified {
401	0	println!(" ❌ Proof {}: {}", i + 1, result.assertion);
402	0	if let Some(ref counterex) = result.counterexample {
403	0	println!(" Counterexample: {}", counterex);
404	0	}
405	0	if let Some(ref error) = result.error {
406	0	println!(" Error: {}", error);
407	0	}
408	0	}
409		}
410	0	}
411
412		/// Print passed proofs
413	0	fn print_passed_proofs(results: &[ruchy::proving::ProofVerificationResult]) {
414	0	println!("\nPassed proofs:");
415	0	for (i, result) in results.iter().enumerate() {
416	0	if result.is_verified {
417	0	println!(" ✅ Proof {}: {} ({:.1}ms)",
418	0	i + 1, result.assertion, result.verification_time_ms);
419	0	}
420		}
421	0	}
422
423		/// Check if any verifications failed and exit accordingly
424	0	fn check_verification_failures(results: &[ruchy::proving::ProofVerificationResult]) {
425	0	let failed = results.iter().filter(\|r\| !r.is_verified).count();
426	0	if failed > 0 {
427	0	std::process::exit(1);
428	0	}
429	0	}