## 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/proving/counterexample.rs

    Line
    Count
    Source
    1
    //! Counterexample generation for failed proofs
    2
    3
    use anyhow::Result;
    4
    use serde::{Deserialize, Serialize};
    5
    use std::collections::HashMap;
    6
    use std::fmt;
    7
    8
    use super::smt::{SmtSolver, SmtBackend, SmtResult};
    9
    10
    /// Counterexample
    11
    #[derive(Debug, Clone, Serialize, Deserialize)]
    12
    pub struct Counterexample {
    13
        /// Variable assignments
    14
        pub assignments: HashMap<String, Value>,
    15
    16
        /// Execution trace
    17
        pub trace: Vec<TraceStep>,
    18
    19
        /// Failed assertion
    20
        pub failed_assertion: String,
    21
    22
        /// Explanation
    23
        pub explanation: Option<String>,
    24
    }
    25
    26
    /// Value in counterexample
    27
    #[derive(Debug, Clone, Serialize, Deserialize)]
    28
    pub enum Value {
    29
        Int(i64),
    30
        Bool(bool),
    31
        String(String),
    32
        Float(f64),
    33
        Array(Vec<Value>),
    34
        Tuple(Vec<Value>),
    35
        Null,
    36
    }
    37
    38
    impl fmt::Display for Value {
    39
    0
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
    40
    0
            match self {
    41
    0
                Self::Int(n) => write!(f, "{n}"),
    42
    0
                Self::Bool(b) => write!(f, "{b}"),
    43
    0
                Self::String(s) => write!(f, "\"{s}\""),
    44
    0
                Self::Float(x) => write!(f, "{x}"),
    45
    0
                Self::Array(vs) => {
    46
    0
                    write!(f, "[")?;
    47
    0
                    for (i, v) in vs.iter().enumerate() {
    48
    0
                        if i > 0 { write!(f, ", ")?; }
    49
    0
                        write!(f, "{v}")?;
    50
                    }
    51
    0
                    write!(f, "]")
    52
                }
    53
    0
                Self::Tuple(vs) => {
    54
    0
                    write!(f, "(")?;
    55
    0
                    for (i, v) in vs.iter().enumerate() {
    56
    0
                        if i > 0 { write!(f, ", ")?; }
    57
    0
                        write!(f, "{v}")?;
    58
                    }
    59
    0
                    write!(f, ")")
    60
                }
    61
    0
                Self::Null => write!(f, "null"),
    62
            }
    63
    0
        }
    64
    }
    65
    66
    /// Trace step
    67
    #[derive(Debug, Clone, Serialize, Deserialize)]
    68
    pub struct TraceStep {
    69
        /// Step number
    70
        pub step: usize,
    71
    72
        /// Location in code
    73
        pub location: String,
    74
    75
        /// Operation performed
    76
        pub operation: String,
    77
    78
        /// State after operation
    79
        pub state: HashMap<String, Value>,
    80
    }
    81
    82
    impl Counterexample {
    83
        /// Create new counterexample
    84
    0
        pub fn new(failed_assertion: &str) -> Self {
    85
    0
            Self {
    86
    0
                assignments: HashMap::new(),
    87
    0
                trace: Vec::new(),
    88
    0
                failed_assertion: failed_assertion.to_string(),
    89
    0
                explanation: None,
    90
    0
            }
    91
    0
        }
    92
    93
        /// Add assignment
    94
    0
        pub fn add_assignment(&mut self, var: &str, value: Value) {
    95
    0
            self.assignments.insert(var.to_string(), value);
    96
    0
        }
    97
    98
        /// Add trace step
    99
    0
        pub fn add_trace_step(&mut self, step: TraceStep) {
    100
    0
            self.trace.push(step);
    101
    0
        }
    102
    103
        /// Set explanation
    104
    0
        pub fn set_explanation(&mut self, explanation: &str) {
    105
    0
            self.explanation = Some(explanation.to_string());
    106
    0
        }
    107
    108
        /// Format as readable report
    109
    0
        pub fn format_report(&self) -> String {
    110
    0
            let mut report = String::new();
    111
    112
    0
            report.push_str("=== Counterexample Found ===\n\n");
    113
    114
    0
            report.push_str("Failed Assertion:\n");
    115
    0
            report.push_str(&format!("  {}\n\n", self.failed_assertion));
    116
    117
    0
            if !self.assignments.is_empty() {
    118
    0
                report.push_str("Variable Assignments:\n");
    119
    0
                for (var, val) in &self.assignments {
    120
    0
                    report.push_str(&format!("  {var} = {val}\n"));
    121
    0
                }
    122
    0
                report.push('\n');
    123
    0
            }
    124
    125
    0
            if !self.trace.is_empty() {
    126
    0
                report.push_str("Execution Trace:\n");
    127
    0
                for step in &self.trace {
    128
    0
                    report.push_str(&format!("  Step {}: {} at {}\n",
    129
    0
                        step.step, step.operation, step.location));
    130
    0
                    if !step.state.is_empty() {
    131
    0
                        for (var, val) in &step.state {
    132
    0
                            report.push_str(&format!("    {var} = {val}\n"));
    133
    0
                        }
    134
    0
                    }
    135
                }
    136
    0
                report.push('\n');
    137
    0
            }
    138
    139
    0
            if let Some(explanation) = &self.explanation {
    140
    0
                report.push_str("Explanation:\n");
    141
    0
                report.push_str(&format!("  {explanation}\n"));
    142
    0
            }
    143
    144
    0
            report
    145
    0
        }
    146
    }
    147
    148
    /// Test case for property-based testing
    149
    #[derive(Debug, Clone, Serialize, Deserialize)]
    150
    pub struct TestCase {
    151
        /// Input values
    152
        pub inputs: HashMap<String, Value>,
    153
    154
        /// Expected output
    155
        pub expected: Option<Value>,
    156
    157
        /// Property to test
    158
        pub property: String,
    159
    }
    160
    161
    impl TestCase {
    162
        /// Create new test case
    163
    0
        pub fn new(property: &str) -> Self {
    164
    0
            Self {
    165
    0
                inputs: HashMap::new(),
    166
    0
                expected: None,
    167
    0
                property: property.to_string(),
    168
    0
            }
    169
    0
        }
    170
    171
        /// Add input
    172
    0
        pub fn add_input(&mut self, name: &str, value: Value) {
    173
    0
            self.inputs.insert(name.to_string(), value);
    174
    0
        }
    175
    176
        /// Set expected output
    177
    0
        pub fn set_expected(&mut self, value: Value) {
    178
    0
            self.expected = Some(value);
    179
    0
        }
    180
    181
        /// Generate Ruchy test code
    182
    0
        pub fn to_ruchy_test(&self, test_name: &str) -> String {
    183
    0
            let mut code = String::new();
    184
    185
    0
            code.push_str(&format!("#[test]\nfn {test_name}() {{\n"));
    186
    187
    0
            for (name, value) in &self.inputs {
    188
    0
                code.push_str(&format!("    let {} = {};\n", name,
    189
    0
                    self.value_to_ruchy(value)));
    190
    0
            }
    191
    192
    0
            code.push_str(&format!("    assert!({});\n", self.property));
    193
    194
    0
            if let Some(expected) = &self.expected {
    195
    0
                code.push_str(&format!("    assert_eq!(result, {});\n",
    196
    0
                    self.value_to_ruchy(expected)));
    197
    0
            }
    198
    199
    0
            code.push_str("}\n");
    200
    201
    0
            code
    202
    0
        }
    203
    204
        /// Convert value to Ruchy syntax
    205
    0
        fn value_to_ruchy(&self, value: &Value) -> String {
    206
    0
            match value {
    207
    0
                Value::Int(n) => n.to_string(),
    208
    0
                Value::Bool(b) => b.to_string(),
    209
    0
                Value::String(s) => format!("\"{s}\""),
    210
    0
                Value::Float(x) => format!("{x:.6}"),
    211
    0
                Value::Array(vs) => {
    212
    0
                    let items: Vec<String> = vs.iter()
    213
    0
                        .map(|v| self.value_to_ruchy(v))
    214
    0
                        .collect();
    215
    0
                    format!("[{}]", items.join(", "))
    216
                }
    217
    0
                Value::Tuple(vs) => {
    218
    0
                    let items: Vec<String> = vs.iter()
    219
    0
                        .map(|v| self.value_to_ruchy(v))
    220
    0
                        .collect();
    221
    0
                    format!("({})", items.join(", "))
    222
                }
    223
    0
                Value::Null => "None".to_string(),
    224
            }
    225
    0
        }
    226
    }
    227
    228
    /// Counterexample generator
    229
    pub struct CounterexampleGenerator {
    230
        backend: SmtBackend,
    231
        max_iterations: usize,
    232
        shrinking: bool,
    233
    }
    234
    235
    impl CounterexampleGenerator {
    236
        /// Create new generator
    237
    0
        pub fn new() -> Self {
    238
    0
            Self {
    239
    0
                backend: SmtBackend::Z3,
    240
    0
                max_iterations: 100,
    241
    0
                shrinking: true,
    242
    0
            }
    243
    0
        }
    244
    245
        /// Set SMT backend
    246
    0
        pub fn set_backend(&mut self, backend: SmtBackend) {
    247
    0
            self.backend = backend;
    248
    0
        }
    249
    250
        /// Enable/disable shrinking
    251
    0
        pub fn set_shrinking(&mut self, enabled: bool) {
    252
    0
            self.shrinking = enabled;
    253
    0
        }
    254
    255
        /// Generate counterexample for property
    256
    0
        pub fn generate(&self, property: &str, vars: &[(String, String)]) -> Result<Option<Counterexample>> {
    257
    0
            let mut solver = SmtSolver::new(self.backend);
    258
    259
    0
            for (name, sort) in vars {
    260
    0
                solver.declare_var(name, sort);
    261
    0
            }
    262
    263
    0
            solver.assert(&format!("(not {property})"));
    264
    265
    0
            match solver.check_sat()? {
    266
                SmtResult::Sat => {
    267
    0
                    let model = solver.get_model()?;
    268
    0
                    Ok(Some(self.build_counterexample(property, model)))
    269
                }
    270
    0
                _ => Ok(None),
    271
            }
    272
    0
        }
    273
    274
        /// Build counterexample from model
    275
    0
        fn build_counterexample(&self, property: &str, model: Option<HashMap<String, String>>) -> Counterexample {
    276
    0
            let mut cex = Counterexample::new(property);
    277
    278
    0
            if let Some(assignments) = model {
    279
    0
                for (var, val) in assignments {
    280
    0
                    cex.add_assignment(&var, self.parse_value(&val));
    281
    0
                }
    282
    0
            }
    283
    284
    0
            if self.shrinking {
    285
    0
                self.shrink_counterexample(&mut cex);
    286
    0
            }
    287
    288
    0
            cex
    289
    0
        }
    290
    291
        /// Parse SMT value
    292
    0
        fn parse_value(&self, smt_value: &str) -> Value {
    293
    0
            if let Ok(n) = smt_value.parse::<i64>() {
    294
    0
                Value::Int(n)
    295
    0
            } else if smt_value == "true" {
    296
    0
                Value::Bool(true)
    297
    0
            } else if smt_value == "false" {
    298
    0
                Value::Bool(false)
    299
    0
            } else if let Ok(x) = smt_value.parse::<f64>() {
    300
    0
                Value::Float(x)
    301
            } else {
    302
    0
                Value::String(smt_value.to_string())
    303
            }
    304
    0
        }
    305
    306
        /// Shrink counterexample to minimal form
    307
    0
        fn shrink_counterexample(&self, cex: &mut Counterexample) {
    308
    0
            let mut changed = true;
    309
    0
            let mut iterations = 0;
    310
    311
    0
            while changed && iterations < self.max_iterations {
    312
    0
                changed = false;
    313
    0
                iterations += 1;
    314
    315
    0
                for (var, value) in cex.assignments.clone() {
    316
    0
                    if let Some(shrunk) = self.try_shrink_value(&value) {
    317
    0
                        cex.assignments.insert(var, shrunk);
    318
    0
                        changed = true;
    319
    0
                    }
    320
                }
    321
            }
    322
    0
        }
    323
    324
        /// Try to shrink a value
    325
    0
        fn try_shrink_value(&self, value: &Value) -> Option<Value> {
    326
    0
            match value {
    327
    0
                Value::Int(n) if *n > 0 => Some(Value::Int(n / 2)),
    328
    0
                Value::Array(vs) if !vs.is_empty() => {
    329
    0
                    let mut shrunk = vs.clone();
    330
    0
                    shrunk.pop();
    331
    0
                    Some(Value::Array(shrunk))
    332
                }
    333
    0
                Value::String(s) if s.len() > 1 => {
    334
    0
                    Some(Value::String(s[..s.len()-1].to_string()))
    335
                }
    336
    0
                _ => None,
    337
            }
    338
    0
        }
    339
    340
        /// Generate multiple test cases
    341
    0
        pub fn generate_test_suite(&self, property: &str, vars: &[(String, String)], count: usize) -> Result<Vec<TestCase>> {
    342
    0
            let mut test_cases: Vec<TestCase> = Vec::new();
    343
    344
    0
            for i in 0..count {
    345
    0
                let mut solver = SmtSolver::new(self.backend);
    346
    347
    0
                for (name, sort) in vars {
    348
    0
                    solver.declare_var(name, sort);
    349
    0
                }
    350
    351
    0
                for prev_case in &test_cases {
    352
    0
                    for (var, val) in &prev_case.inputs {
    353
    0
                        solver.assert(&format!("(not (= {} {}))", var,
    354
    0
                            self.value_to_smt(val)));
    355
    0
                    }
    356
                }
    357
    358
    0
                solver.assert(&format!("(not {property})"));
    359
    360
    0
                match solver.check_sat()? {
    361
                    SmtResult::Sat => {
    362
    0
                        if let Some(model) = solver.get_model()? {
    363
    0
                            let mut test_case = TestCase::new(property);
    364
    0
                            for (var, val) in model {
    365
    0
                                test_case.add_input(&var, self.parse_value(&val));
    366
    0
                            }
    367
    0
                            test_cases.push(test_case);
    368
    0
                        }
    369
                    }
    370
    0
                    _ => break,
    371
                }
    372
    373
    0
                if i >= count {
    374
    0
                    break;
    375
    0
                }
    376
            }
    377
    378
    0
            Ok(test_cases)
    379
    0
        }
    380
    381
        /// Convert value to SMT syntax
    382
    0
        fn value_to_smt(&self, value: &Value) -> String {
    383
    0
            match value {
    384
    0
                Value::Int(n) => n.to_string(),
    385
    0
                Value::Bool(b) => b.to_string(),
    386
    0
                Value::String(s) => format!("\"{s}\""),
    387
    0
                Value::Float(x) => format!("{x:.6}"),
    388
    0
                _ => "null".to_string(),
    389
            }
    390
    0
        }
    391
    }
    392
    393
    impl Default for CounterexampleGenerator {
    394
    0
        fn default() -> Self {
    395
    0
            Self::new()
    396
    0
        }
    397
    }
    398
    399
    /// Symbolic execution engine
    400
    pub struct SymbolicExecutor {
    401
        generator: CounterexampleGenerator,
    402
        path_conditions: Vec<String>,
    403
        symbolic_state: HashMap<String, String>,
    404
    }
    405
    406
    impl SymbolicExecutor {
    407
        /// Create new symbolic executor
    408
    0
        pub fn new() -> Self {
    409
    0
            Self {
    410
    0
                generator: CounterexampleGenerator::new(),
    411
    0
                path_conditions: Vec::new(),
    412
    0
                symbolic_state: HashMap::new(),
    413
    0
            }
    414
    0
        }
    415
    416
        /// Add path condition
    417
    0
        pub fn add_condition(&mut self, condition: &str) {
    418
    0
            self.path_conditions.push(condition.to_string());
    419
    0
        }
    420
    421
        /// Set symbolic variable
    422
    0
        pub fn set_symbolic(&mut self, var: &str, symbolic: &str) {
    423
    0
            self.symbolic_state.insert(var.to_string(), symbolic.to_string());
    424
    0
        }
    425
    426
        /// Find path to error
    427
    0
        pub fn find_error_path(&self, error_condition: &str) -> Result<Option<Counterexample>> {
    428
    0
            let mut solver = SmtSolver::new(self.generator.backend);
    429
    430
    0
            for var in self.symbolic_state.keys() {
    431
    0
                solver.declare_var(var, "Int");
    432
    0
            }
    433
    434
    0
            for condition in &self.path_conditions {
    435
    0
                solver.assert(condition);
    436
    0
            }
    437
    438
    0
            solver.assert(error_condition);
    439
    440
    0
            match solver.check_sat()? {
    441
                SmtResult::Sat => {
    442
    0
                    let model = solver.get_model()?;
    443
    0
                    Ok(Some(self.generator.build_counterexample(error_condition, model)))
    444
                }
    445
    0
                _ => Ok(None),
    446
            }
    447
    0
        }
    448
    }
    449
    450
    impl Default for SymbolicExecutor {
    451
    0
        fn default() -> Self {
    452
    0
            Self::new()
    453
    0
        }
    454
    }
    455
    456
    #[cfg(test)]
    457
    mod tests {
    458
        use super::*;
    459
    460
        #[test]
    461
        fn test_counterexample_report() {
    462
            let mut cex = Counterexample::new("x > 10");
    463
            cex.add_assignment("x", Value::Int(5));
    464
            cex.set_explanation("x = 5 does not satisfy x > 10");
    465
    466
            let report = cex.format_report();
    467
            assert!(report.contains("x > 10"));
    468
            assert!(report.contains("x = 5"));
    469
        }
    470
    471
        #[test]
    472
        fn test_test_case_generation() {
    473
            let mut test = TestCase::new("x > 0");
    474
            test.add_input("x", Value::Int(42));
    475
            test.set_expected(Value::Bool(true));
    476
    477
            let code = test.to_ruchy_test("test_positive");
    478
            assert!(code.contains("let x = 42"));
    479
            assert!(code.contains("assert!(x > 0)"));
    480
        }
    481
    }