## Coverage Report

#### Created: 2025-09-08 21:26

next uncovered line (L), next uncovered region (R), next uncovered branch (B)

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

    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
    }