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

    Line
    Count
    Source
    1
    //! Refinement type system for property verification
    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
    /// Refinement type
    11
    #[derive(Debug, Clone, Serialize, Deserialize)]
    12
    pub struct RefinementType {
    13
        /// Base type
    14
        pub base: BaseType,
    15
    16
        /// Refinement predicate
    17
        pub predicate: Option<Predicate>,
    18
    19
        /// Type parameters
    20
        pub params: Vec<String>,
    21
    }
    22
    23
    /// Base types
    24
    #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
    25
    pub enum BaseType {
    26
        Int,
    27
        Bool,
    28
        String,
    29
        Float,
    30
        Array(Box<BaseType>),
    31
        Tuple(Vec<BaseType>),
    32
        Function(Vec<BaseType>, Box<BaseType>),
    33
        Custom(String),
    34
    }
    35
    36
    /// Refinement predicate
    37
    #[derive(Debug, Clone, Serialize, Deserialize)]
    38
    pub struct Predicate {
    39
        /// Variable binding
    40
        pub var: String,
    41
    42
        /// Predicate expression
    43
        pub expr: String,
    44
    }
    45
    46
    impl RefinementType {
    47
        /// Create integer with bounds
    48
    0
        pub fn bounded_int(min: i64, max: i64) -> Self {
    49
    0
            Self {
    50
    0
                base: BaseType::Int,
    51
    0
                predicate: Some(Predicate {
    52
    0
                    var: "x".to_string(),
    53
    0
                    expr: format!("(and (>= x {min}) (<= x {max}))"),
    54
    0
                }),
    55
    0
                params: Vec::new(),
    56
    0
            }
    57
    0
        }
    58
    59
        /// Create positive integer
    60
    0
        pub fn positive_int() -> Self {
    61
    0
            Self {
    62
    0
                base: BaseType::Int,
    63
    0
                predicate: Some(Predicate {
    64
    0
                    var: "x".to_string(),
    65
    0
                    expr: "(> x 0)".to_string(),
    66
    0
                }),
    67
    0
                params: Vec::new(),
    68
    0
            }
    69
    0
        }
    70
    71
        /// Create non-empty array
    72
    0
        pub fn non_empty_array(elem_type: BaseType) -> Self {
    73
    0
            Self {
    74
    0
                base: BaseType::Array(Box::new(elem_type)),
    75
    0
                predicate: Some(Predicate {
    76
    0
                    var: "a".to_string(),
    77
    0
                    expr: "(> (len a) 0)".to_string(),
    78
    0
                }),
    79
    0
                params: Vec::new(),
    80
    0
            }
    81
    0
        }
    82
    83
        /// Create sorted array
    84
    0
        pub fn sorted_array() -> Self {
    85
    0
            Self {
    86
    0
                base: BaseType::Array(Box::new(BaseType::Int)),
    87
    0
                predicate: Some(Predicate {
    88
    0
                    var: "a".to_string(),
    89
    0
                    expr: "(sorted a)".to_string(),
    90
    0
                }),
    91
    0
                params: Vec::new(),
    92
    0
            }
    93
    0
        }
    94
    }
    95
    96
    impl fmt::Display for RefinementType {
    97
    0
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
    98
    0
            if let Some(pred) = &self.predicate {
    99
    0
                write!(f, "{} where {}", self.base, pred.expr)
    100
            } else {
    101
    0
                write!(f, "{}", self.base)
    102
            }
    103
    0
        }
    104
    }
    105
    106
    impl fmt::Display for BaseType {
    107
    0
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
    108
    0
            match self {
    109
    0
                Self::Int => write!(f, "Int"),
    110
    0
                Self::Bool => write!(f, "Bool"),
    111
    0
                Self::String => write!(f, "String"),
    112
    0
                Self::Float => write!(f, "Float"),
    113
    0
                Self::Array(t) => write!(f, "[{t}]"),
    114
    0
                Self::Tuple(ts) => {
    115
    0
                    write!(f, "(")?;
    116
    0
                    for (i, t) in ts.iter().enumerate() {
    117
    0
                        if i > 0 { write!(f, ", ")?; }
    118
    0
                        write!(f, "{t}")?;
    119
                    }
    120
    0
                    write!(f, ")")
    121
                }
    122
    0
                Self::Function(params, ret) => {
    123
    0
                    write!(f, "(")?;
    124
    0
                    for (i, p) in params.iter().enumerate() {
    125
    0
                        if i > 0 { write!(f, ", ")?; }
    126
    0
                        write!(f, "{p}")?;
    127
                    }
    128
    0
                    write!(f, ") -> {ret}")
    129
                }
    130
    0
                Self::Custom(name) => write!(f, "{name}"),
    131
            }
    132
    0
        }
    133
    }
    134
    135
    /// Type refinement
    136
    #[derive(Debug, Clone)]
    137
    pub struct TypeRefinement {
    138
        /// Input type
    139
        pub input: RefinementType,
    140
    141
        /// Output type
    142
        pub output: RefinementType,
    143
    144
        /// Preconditions
    145
        pub preconditions: Vec<String>,
    146
    147
        /// Postconditions
    148
        pub postconditions: Vec<String>,
    149
    150
        /// Invariants
    151
        pub invariants: Vec<String>,
    152
    }
    153
    154
    impl TypeRefinement {
    155
        /// Create new refinement
    156
    0
        pub fn new(input: RefinementType, output: RefinementType) -> Self {
    157
    0
            Self {
    158
    0
                input,
    159
    0
                output,
    160
    0
                preconditions: Vec::new(),
    161
    0
                postconditions: Vec::new(),
    162
    0
                invariants: Vec::new(),
    163
    0
            }
    164
    0
        }
    165
    166
        /// Add precondition
    167
    0
        pub fn add_precondition(&mut self, pred: &str) {
    168
    0
            self.preconditions.push(pred.to_string());
    169
    0
        }
    170
    171
        /// Add postcondition
    172
    0
        pub fn add_postcondition(&mut self, pred: &str) {
    173
    0
            self.postconditions.push(pred.to_string());
    174
    0
        }
    175
    176
        /// Add invariant
    177
    0
        pub fn add_invariant(&mut self, inv: &str) {
    178
    0
            self.invariants.push(inv.to_string());
    179
    0
        }
    180
    }
    181
    182
    /// Refinement type checker
    183
    pub struct RefinementChecker {
    184
        /// SMT backend
    185
        backend: SmtBackend,
    186
    187
        /// Type environment
    188
        env: HashMap<String, RefinementType>,
    189
    190
        /// Function signatures
    191
        signatures: HashMap<String, TypeRefinement>,
    192
    }
    193
    194
    impl RefinementChecker {
    195
        /// Create new checker
    196
    0
        pub fn new() -> Self {
    197
    0
            Self {
    198
    0
                backend: SmtBackend::Z3,
    199
    0
                env: HashMap::new(),
    200
    0
                signatures: HashMap::new(),
    201
    0
            }
    202
    0
        }
    203
    204
        /// Set SMT backend
    205
    0
        pub fn set_backend(&mut self, backend: SmtBackend) {
    206
    0
            self.backend = backend;
    207
    0
        }
    208
    209
        /// Declare variable
    210
    0
        pub fn declare_var(&mut self, name: &str, ty: RefinementType) {
    211
    0
            self.env.insert(name.to_string(), ty);
    212
    0
        }
    213
    214
        /// Declare function
    215
    0
        pub fn declare_function(&mut self, name: &str, refinement: TypeRefinement) {
    216
    0
            self.signatures.insert(name.to_string(), refinement);
    217
    0
        }
    218
    219
        /// Check subtyping
    220
    0
        pub fn is_subtype(&self, sub_type: &RefinementType, super_type: &RefinementType) -> Result<bool> {
    221
    0
            if sub_type.base != super_type.base {
    222
    0
                return Ok(false);
    223
    0
            }
    224
    225
    0
            match (&sub_type.predicate, &super_type.predicate) {
    226
    0
                (Some(sub_pred), Some(super_pred)) => {
    227
    0
                    self.check_implication(&sub_pred.expr, &super_pred.expr)
    228
                }
    229
    0
                (Some(_), None) => Ok(true),
    230
    0
                (None, Some(_)) => Ok(false),
    231
    0
                (None, None) => Ok(true),
    232
            }
    233
    0
        }
    234
    235
        /// Check implication using SMT
    236
    0
        fn check_implication(&self, antecedent: &str, consequent: &str) -> Result<bool> {
    237
    0
            let mut solver = SmtSolver::new(self.backend);
    238
    239
    0
            solver.assert(antecedent);
    240
    0
            solver.assert(&format!("(not {consequent})"));
    241
    242
    0
            match solver.check_sat()? {
    243
    0
                SmtResult::Unsat => Ok(true),
    244
    0
                _ => Ok(false),
    245
            }
    246
    0
        }
    247
    248
        /// Verify function refinement
    249
    0
        pub fn verify_function(&self, name: &str, body: &str) -> Result<VerificationResult> {
    250
    0
            let refinement = self.signatures.get(name)
    251
    0
                .ok_or_else(|| anyhow::anyhow!("Unknown function: {}", name))?;
    252
    253
    0
            let mut solver = SmtSolver::new(self.backend);
    254
    255
    0
            for pre in &refinement.preconditions {
    256
    0
                solver.assert(pre);
    257
    0
            }
    258
    259
    0
            solver.assert(body);
    260
    261
    0
            for post in &refinement.postconditions {
    262
    0
                solver.assert(&format!("(not {post})"));
    263
    0
            }
    264
    265
    0
            match solver.check_sat()? {
    266
    0
                SmtResult::Unsat => Ok(VerificationResult::Valid),
    267
    0
                SmtResult::Sat => Ok(VerificationResult::Invalid("Postcondition violation".to_string())),
    268
    0
                _ => Ok(VerificationResult::Unknown),
    269
            }
    270
    0
        }
    271
    272
        /// Check invariant preservation
    273
    0
        pub fn check_invariant(&self, invariant: &str, body: &str) -> Result<bool> {
    274
    0
            let mut solver = SmtSolver::new(self.backend);
    275
    276
    0
            solver.assert(invariant);
    277
    278
    0
            solver.assert(body);
    279
    280
    0
            solver.assert(&format!("(not {invariant})"));
    281
    282
    0
            match solver.check_sat()? {
    283
    0
                SmtResult::Unsat => Ok(true),
    284
    0
                _ => Ok(false),
    285
            }
    286
    0
        }
    287
    }
    288
    289
    impl Default for RefinementChecker {
    290
    0
        fn default() -> Self {
    291
    0
            Self::new()
    292
    0
        }
    293
    }
    294
    295
    /// Verification result
    296
    #[derive(Debug, Clone, Serialize, Deserialize)]
    297
    pub enum VerificationResult {
    298
        Valid,
    299
        Invalid(String),
    300
        Unknown,
    301
    }
    302
    303
    impl VerificationResult {
    304
        /// Check if valid
    305
    0
        pub fn is_valid(&self) -> bool {
    306
    0
            matches!(self, Self::Valid)
    307
    0
        }
    308
    309
        /// Get error message
    310
    0
        pub fn error(&self) -> Option<&str> {
    311
    0
            match self {
    312
    0
                Self::Invalid(msg) => Some(msg),
    313
    0
                _ => None,
    314
            }
    315
    0
        }
    316
    }
    317
    318
    /// Liquid type inference
    319
    pub struct LiquidTypeInference {
    320
        checker: RefinementChecker,
    321
        constraints: Vec<String>,
    322
    }
    323
    324
    impl LiquidTypeInference {
    325
        /// Create new inference engine
    326
    0
        pub fn new() -> Self {
    327
    0
            Self {
    328
    0
                checker: RefinementChecker::new(),
    329
    0
                constraints: Vec::new(),
    330
    0
            }
    331
    0
        }
    332
    333
        /// Infer refinement type
    334
    0
        pub fn infer(&mut self, expr: &str) -> Result<RefinementType> {
    335
    0
            match expr {
    336
    0
                s if s.parse::<i64>().is_ok() => {
    337
    0
                    let n = s.parse::<i64>().unwrap();
    338
    0
                    Ok(RefinementType {
    339
    0
                        base: BaseType::Int,
    340
    0
                        predicate: Some(Predicate {
    341
    0
                            var: "x".to_string(),
    342
    0
                            expr: format!("(= x {n})"),
    343
    0
                        }),
    344
    0
                        params: Vec::new(),
    345
    0
                    })
    346
                }
    347
    0
                "true" | "false" => Ok(RefinementType {
    348
    0
                    base: BaseType::Bool,
    349
    0
                    predicate: None,
    350
    0
                    params: Vec::new(),
    351
    0
                }),
    352
    0
                _ => Ok(RefinementType {
    353
    0
                    base: BaseType::Custom("Unknown".to_string()),
    354
    0
                    predicate: None,
    355
    0
                    params: Vec::new(),
    356
    0
                }),
    357
            }
    358
    0
        }
    359
    360
        /// Add constraint
    361
    0
        pub fn add_constraint(&mut self, constraint: &str) {
    362
    0
            self.constraints.push(constraint.to_string());
    363
    0
        }
    364
    365
        /// Solve constraints
    366
    0
        pub fn solve(&self) -> Result<bool> {
    367
    0
            let mut solver = SmtSolver::new(self.checker.backend);
    368
    369
    0
            for constraint in &self.constraints {
    370
    0
                solver.assert(constraint);
    371
    0
            }
    372
    373
    0
            match solver.check_sat()? {
    374
    0
                SmtResult::Sat => Ok(true),
    375
    0
                _ => Ok(false),
    376
            }
    377
    0
        }
    378
    }
    379
    380
    impl Default for LiquidTypeInference {
    381
    0
        fn default() -> Self {
    382
    0
            Self::new()
    383
    0
        }
    384
    }
    385
    386
    #[cfg(test)]
    387
    mod tests {
    388
        use super::*;
    389
    390
        #[test]
    391
        fn test_refinement_type_display() {
    392
            let ty = RefinementType::positive_int();
    393
            assert_eq!(ty.to_string(), "Int where (> x 0)");
    394
    395
            let bounded = RefinementType::bounded_int(0, 100);
    396
            assert_eq!(bounded.to_string(), "Int where (and (>= x 0) (<= x 100))");
    397
        }
    398
    399
        #[test]
    400
        fn test_base_type_display() {
    401
            assert_eq!(BaseType::Int.to_string(), "Int");
    402
            assert_eq!(BaseType::Array(Box::new(BaseType::Int)).to_string(), "[Int]");
    403
    404
            let func = BaseType::Function(
    405
                vec![BaseType::Int, BaseType::Bool],
    406
                Box::new(BaseType::String)
    407
            );
    408
            assert_eq!(func.to_string(), "(Int, Bool) -> String");
    409
        }
    410
    }