/home/noah/src/ruchy/src/proving/refinement.rs

Source
//! Refinement type system for property verification

use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use std::fmt;

use super::smt::{SmtSolver, SmtBackend, SmtResult};

/// Refinement type
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct RefinementType {
    /// Base type
    pub base: BaseType,
    
    /// Refinement predicate
    pub predicate: Option<Predicate>,
    
    /// Type parameters
    pub params: Vec<String>,
}

/// Base types
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum BaseType {
    Int,
    Bool,
    String,
    Float,
    Array(Box<BaseType>),
    Tuple(Vec<BaseType>),
    Function(Vec<BaseType>, Box<BaseType>),
    Custom(String),
}

/// Refinement predicate
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Predicate {
    /// Variable binding
    pub var: String,
    
    /// Predicate expression
    pub expr: String,
}

impl RefinementType {
    /// Create integer with bounds
    pub fn bounded_int(min: i64, max: i64) -> Self {
        Self {
            base: BaseType::Int,
            predicate: Some(Predicate {
                var: "x".to_string(),
                expr: format!("(and (>= x {min}) (<= x {max}))"),
            }),
            params: Vec::new(),
        }
    }
    
    /// Create positive integer
    pub fn positive_int() -> Self {
        Self {
            base: BaseType::Int,
            predicate: Some(Predicate {
                var: "x".to_string(),
                expr: "(> x 0)".to_string(),
            }),
            params: Vec::new(),
        }
    }
    
    /// Create non-empty array
    pub fn non_empty_array(elem_type: BaseType) -> Self {
        Self {
            base: BaseType::Array(Box::new(elem_type)),
            predicate: Some(Predicate {
                var: "a".to_string(),
                expr: "(> (len a) 0)".to_string(),
            }),
            params: Vec::new(),
        }
    }
    
    /// Create sorted array
    pub fn sorted_array() -> Self {
        Self {
            base: BaseType::Array(Box::new(BaseType::Int)),
            predicate: Some(Predicate {
                var: "a".to_string(),
                expr: "(sorted a)".to_string(),
            }),
            params: Vec::new(),
        }
    }
}

impl fmt::Display for RefinementType {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        if let Some(pred) = &self.predicate {
            write!(f, "{} where {}", self.base, pred.expr)
        } else {
            write!(f, "{}", self.base)
        }
    }
}

impl fmt::Display for BaseType {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Int => write!(f, "Int"),
            Self::Bool => write!(f, "Bool"),
            Self::String => write!(f, "String"),
            Self::Float => write!(f, "Float"),
            Self::Array(t) => write!(f, "[{t}]"),
            Self::Tuple(ts) => {
                write!(f, "(")?;
                for (i, t) in ts.iter().enumerate() {
                    if i > 0 { write!(f, ", ")?; }
                    write!(f, "{t}")?;
                }
                write!(f, ")")
            }
            Self::Function(params, ret) => {
                write!(f, "(")?0;
                for (i, p) in params.iter()1.enumerate1() {
                    if i > 0 { write!1(f1, ", "1)?0; }1
                    write!(f, "{p}")?0;
                }
                write!(f, ") -> {ret}")
            }
            Self::Custom(name) => write!(f, "{name}"),
        }
    }
}

/// Type refinement
#[derive(Debug, Clone)]
pub struct TypeRefinement {
    /// Input type
    pub input: RefinementType,
    
    /// Output type
    pub output: RefinementType,
    
    /// Preconditions
    pub preconditions: Vec<String>,
    
    /// Postconditions
    pub postconditions: Vec<String>,
    
    /// Invariants
    pub invariants: Vec<String>,
}

impl TypeRefinement {
    /// Create new refinement
    pub fn new(input: RefinementType, output: RefinementType) -> Self {
        Self {
            input,
            output,
            preconditions: Vec::new(),
            postconditions: Vec::new(),
            invariants: Vec::new(),
        }
    }
    
    /// Add precondition
    pub fn add_precondition(&mut self, pred: &str) {
        self.preconditions.push(pred.to_string());
    }
    
    /// Add postcondition
    pub fn add_postcondition(&mut self, pred: &str) {
        self.postconditions.push(pred.to_string());
    }
    
    /// Add invariant
    pub fn add_invariant(&mut self, inv: &str) {
        self.invariants.push(inv.to_string());
    }
}

/// Refinement type checker
pub struct RefinementChecker {
    /// SMT backend
    backend: SmtBackend,
    
    /// Type environment
    env: HashMap<String, RefinementType>,
    
    /// Function signatures
    signatures: HashMap<String, TypeRefinement>,
}

impl RefinementChecker {
    /// Create new checker
    pub fn new() -> Self {
        Self {
            backend: SmtBackend::Z3,
            env: HashMap::new(),
            signatures: HashMap::new(),
        }
    }
    
    /// Set SMT backend
    pub fn set_backend(&mut self, backend: SmtBackend) {
        self.backend = backend;
    }
    
    /// Declare variable
    pub fn declare_var(&mut self, name: &str, ty: RefinementType) {
        self.env.insert(name.to_string(), ty);
    }
    
    /// Declare function
    pub fn declare_function(&mut self, name: &str, refinement: TypeRefinement) {
        self.signatures.insert(name.to_string(), refinement);
    }
    
    /// Check subtyping
    pub fn is_subtype(&self, sub_type: &RefinementType, super_type: &RefinementType) -> Result<bool> {
        if sub_type.base != super_type.base {
            return Ok(false);
        }
        
        match (&sub_type.predicate, &super_type.predicate) {
            (Some(sub_pred), Some(super_pred)) => {
                self.check_implication(&sub_pred.expr, &super_pred.expr)
            }
            (Some(_), None) => Ok(true),
            (None, Some(_)) => Ok(false),
            (None, None) => Ok(true),
        }
    }
    
    /// Check implication using SMT
    fn check_implication(&self, antecedent: &str, consequent: &str) -> Result<bool> {
        let mut solver = SmtSolver::new(self.backend);
        
        solver.assert(antecedent);
        solver.assert(&format!("(not {consequent})"));
        
        match solver.check_sat()? {
            SmtResult::Unsat => Ok(true),
            _ => Ok(false),
        }
    }
    
    /// Verify function refinement
    pub fn verify_function(&self, name: &str, body: &str) -> Result<VerificationResult> {
        let refinement = self.signatures.get(name)
            .ok_or_else(|| anyhow::anyhow!("Unknown function: {}", name))?;
        
        let mut solver = SmtSolver::new(self.backend);
        
        for pre in &refinement.preconditions {
            solver.assert(pre);
        }
        
        solver.assert(body);
        
        for post in &refinement.postconditions {
            solver.assert(&format!("(not {post})"));
        }
        
        match solver.check_sat()? {
            SmtResult::Unsat => Ok(VerificationResult::Valid),
            SmtResult::Sat => Ok(VerificationResult::Invalid("Postcondition violation".to_string())),
            _ => Ok(VerificationResult::Unknown),
        }
    }
    
    /// Check invariant preservation
    pub fn check_invariant(&self, invariant: &str, body: &str) -> Result<bool> {
        let mut solver = SmtSolver::new(self.backend);
        
        solver.assert(invariant);
        
        solver.assert(body);
        
        solver.assert(&format!("(not {invariant})"));
        
        match solver.check_sat()? {
            SmtResult::Unsat => Ok(true),
            _ => Ok(false),
        }
    }
}

impl Default for RefinementChecker {
    fn default() -> Self {
        Self::new()
    }
}

/// Verification result
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum VerificationResult {
    Valid,
    Invalid(String),
    Unknown,
}

impl VerificationResult {
    /// Check if valid
    pub fn is_valid(&self) -> bool {
        matches!(self, Self::Valid)
    }
    
    /// Get error message
    pub fn error(&self) -> Option<&str> {
        match self {
            Self::Invalid(msg) => Some(msg),
            _ => None,
        }
    }
}

/// Liquid type inference
pub struct LiquidTypeInference {
    checker: RefinementChecker,
    constraints: Vec<String>,
}

impl LiquidTypeInference {
    /// Create new inference engine
    pub fn new() -> Self {
        Self {
            checker: RefinementChecker::new(),
            constraints: Vec::new(),
        }
    }
    
    /// Infer refinement type
    pub fn infer(&mut self, expr: &str) -> Result<RefinementType> {
        match expr {
            s if s.parse::<i64>().is_ok() => {
                let n = s.parse::<i64>().unwrap();
                Ok(RefinementType {
                    base: BaseType::Int,
                    predicate: Some(Predicate {
                        var: "x".to_string(),
                        expr: format!("(= x {n})"),
                    }),
                    params: Vec::new(),
                })
            }
            "true" | "false" => Ok(RefinementType {
                base: BaseType::Bool,
                predicate: None,
                params: Vec::new(),
            }),
            _ => Ok(RefinementType {
                base: BaseType::Custom("Unknown".to_string()),
                predicate: None,
                params: Vec::new(),
            }),
        }
    }
    
    /// Add constraint
    pub fn add_constraint(&mut self, constraint: &str) {
        self.constraints.push(constraint.to_string());
    }
    
    /// Solve constraints
    pub fn solve(&self) -> Result<bool> {
        let mut solver = SmtSolver::new(self.checker.backend);
        
        for constraint in &self.constraints {
            solver.assert(constraint);
        }
        
        match solver.check_sat()? {
            SmtResult::Sat => Ok(true),
            _ => Ok(false),
        }
    }
}

impl Default for LiquidTypeInference {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    
    #[test]
    fn test_refinement_type_display() {
        let ty = RefinementType::positive_int();
        assert_eq!(ty.to_string(), "Int where (> x 0)");
        
        let bounded = RefinementType::bounded_int(0, 100);
        assert_eq!(bounded.to_string(), "Int where (and (>= x 0) (<= x 100))");
    }
    
    #[test]
    fn test_base_type_display() {
        assert_eq!(BaseType::Int.to_string(), "Int");
        assert_eq!(BaseType::Array(Box::new(BaseType::Int)).to_string(), "[Int]");
        
        let func = BaseType::Function(
            vec![BaseType::Int, BaseType::Bool],
            Box::new(BaseType::String)
        );
        assert_eq!(func.to_string(), "(Int, Bool) -> String");
    }
}

Coverage Report

Created: 2025-09-05 15:26

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	1	pub fn bounded_int(min: i64, max: i64) -> Self {
49	1	Self {
50	1	base: BaseType::Int,
51	1	predicate: Some(Predicate {
52	1	var: "x".to_string(),
53	1	expr: format!("(and (>= x {min}) (<= x {max}))"),
54	1	}),
55	1	params: Vec::new(),
56	1	}
57	1	}
58
59		/// Create positive integer
60	1	pub fn positive_int() -> Self {
61	1	Self {
62	1	base: BaseType::Int,
63	1	predicate: Some(Predicate {
64	1	var: "x".to_string(),
65	1	expr: "(> x 0)".to_string(),
66	1	}),
67	1	params: Vec::new(),
68	1	}
69	1	}
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	2	fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
98	2	if let Some(pred) = &self.predicate {
99	2	write!(f, "{} where {}", self.base, pred.expr)
100		} else {
101	0	write!(f, "{}", self.base)
102		}
103	2	}
104		}
105
106		impl fmt::Display for BaseType {
107	9	fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
108	9	match self {
109	5	Self::Int => write!(f, "Int"),
110	1	Self::Bool => write!(f, "Bool"),
111	1	Self::String => write!(f, "String"),
112	0	Self::Float => write!(f, "Float"),
113	1	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	1	Self::Function(params, ret) => {
123	1	write!(f, "(") ?0 ;
124	2	for (i, p) in params.iter()1 . enumerate1 () {
125	2	if i > 0 { write!1 ( f1 , ", "1 ) ?0 ; }1
126	2	write!(f, "{p}") ?0 ;
127		}
128	1	write!(f, ") -> {ret}")
129		}
130	0	Self::Custom(name) => write!(f, "{name}"),
131		}
132	9	}
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	1	fn test_refinement_type_display() {
392	1	let ty = RefinementType::positive_int();
393	1	assert_eq!(ty.to_string(), "Int where (> x 0)");
394
395	1	let bounded = RefinementType::bounded_int(0, 100);
396	1	assert_eq!(bounded.to_string(), "Int where (and (>= x 0) (<= x 100))");
397	1	}
398
399		#[test]
400	1	fn test_base_type_display() {
401	1	assert_eq!(BaseType::Int.to_string(), "Int");
402	1	assert_eq!(BaseType::Array(Box::new(BaseType::Int)).to_string(), "[Int]");
403
404	1	let func = BaseType::Function(
405	1	vec![BaseType::Int, BaseType::Bool],
406	1	Box::new(BaseType::String)
407	1	);
408	1	assert_eq!(func.to_string(), "(Int, Bool) -> String");
409	1	}
410		}