logicaffeine_compile/codegen_sva/
verify_to_kernel.rs

1//! Spec Encoding: BoundedExpr → Kernel Term
2//!
3//! Translates hardware verification expressions from the bounded timestep model
4//! into kernel Terms. Under Curry-Howard, these Terms are types — inhabiting
5//! them constitutes a proof that the hardware satisfies the specification.
6//!
7//! This is the bridge between the SVA verification pipeline and the CoIC kernel.
8
9use logicaffeine_kernel::{Term, Literal};
10use super::sva_to_verify::BoundedExpr;
11
12/// Encode a BoundedExpr as a kernel Term.
13///
14/// The encoding follows Curry-Howard:
15/// - Bool(true) → Global("True") (trivially inhabited proposition)
16/// - Bool(false) → Global("False") (uninhabited proposition)
17/// - And(l, r) → App(App(Global("And"), l'), r')
18/// - Or(l, r) → App(App(Global("Or"), l'), r')
19/// - Not(e) → App(Global("Not"), e')
20/// - Implies(l, r) → Pi("_", l', r') (function type = implication)
21/// - Eq(l, r) → App(App(App(Global("Eq"), Hole), l'), r')
22/// - Var("sig@t") → App(Global("sig"), nat_literal(t))
23/// - Int(n) → Lit(Int(n))
24pub fn encode_bounded_expr(expr: &BoundedExpr) -> Term {
25    match expr {
26        BoundedExpr::Bool(true) => Term::Global("True".to_string()),
27        BoundedExpr::Bool(false) => Term::Global("False".to_string()),
28
29        BoundedExpr::Int(n) => Term::Lit(Literal::Int(*n)),
30
31        BoundedExpr::Var(name) => {
32            if let Some(at_pos) = name.find('@') {
33                let sig = &name[..at_pos];
34                let t: i64 = name[at_pos + 1..].parse().unwrap_or(0);
35                // Signal as function of time: sig(t)
36                Term::App(
37                    Box::new(Term::Global(sig.to_string())),
38                    Box::new(Term::Lit(Literal::Int(t))),
39                )
40            } else {
41                Term::Var(name.clone())
42            }
43        }
44
45        BoundedExpr::And(left, right) => {
46            let l = encode_bounded_expr(left);
47            let r = encode_bounded_expr(right);
48            Term::App(
49                Box::new(Term::App(
50                    Box::new(Term::Global("And".to_string())),
51                    Box::new(l),
52                )),
53                Box::new(r),
54            )
55        }
56
57        BoundedExpr::Or(left, right) => {
58            let l = encode_bounded_expr(left);
59            let r = encode_bounded_expr(right);
60            Term::App(
61                Box::new(Term::App(
62                    Box::new(Term::Global("Or".to_string())),
63                    Box::new(l),
64                )),
65                Box::new(r),
66            )
67        }
68
69        BoundedExpr::Not(inner) => {
70            let e = encode_bounded_expr(inner);
71            Term::App(
72                Box::new(Term::Global("Not".to_string())),
73                Box::new(e),
74            )
75        }
76
77        BoundedExpr::Implies(left, right) => {
78            let l = encode_bounded_expr(left);
79            let r = encode_bounded_expr(right);
80            // Under Curry-Howard: implication = function type (Pi)
81            Term::Pi {
82                param: "_".to_string(),
83                param_type: Box::new(l),
84                body_type: Box::new(r),
85            }
86        }
87
88        BoundedExpr::Eq(left, right) => {
89            let l = encode_bounded_expr(left);
90            let r = encode_bounded_expr(right);
91            // Eq _ l r (type inferred via Hole)
92            Term::App(
93                Box::new(Term::App(
94                    Box::new(Term::App(
95                        Box::new(Term::Global("Eq".to_string())),
96                        Box::new(Term::Hole),
97                    )),
98                    Box::new(l),
99                )),
100                Box::new(r),
101            )
102        }
103
104        BoundedExpr::Lt(left, right) => {
105            let l = encode_bounded_expr(left);
106            let r = encode_bounded_expr(right);
107            Term::App(
108                Box::new(Term::App(
109                    Box::new(Term::Global("lt".to_string())),
110                    Box::new(l),
111                )),
112                Box::new(r),
113            )
114        }
115
116        BoundedExpr::Gt(left, right) => {
117            let l = encode_bounded_expr(left);
118            let r = encode_bounded_expr(right);
119            Term::App(
120                Box::new(Term::App(
121                    Box::new(Term::Global("gt".to_string())),
122                    Box::new(l),
123                )),
124                Box::new(r),
125            )
126        }
127
128        BoundedExpr::Lte(left, right) => {
129            let l = encode_bounded_expr(left);
130            let r = encode_bounded_expr(right);
131            Term::App(
132                Box::new(Term::App(
133                    Box::new(Term::Global("le".to_string())),
134                    Box::new(l),
135                )),
136                Box::new(r),
137            )
138        }
139
140        BoundedExpr::Gte(left, right) => {
141            let l = encode_bounded_expr(left);
142            let r = encode_bounded_expr(right);
143            Term::App(
144                Box::new(Term::App(
145                    Box::new(Term::Global("ge".to_string())),
146                    Box::new(l),
147                )),
148                Box::new(r),
149            )
150        }
151
152        BoundedExpr::Unsupported(msg) => {
153            // Unsupported constructs become False — fail closed
154            let _ = msg;
155            Term::Global("False".to_string())
156        }
157
158        // Multi-sorted extensions: encode as appropriate kernel terms
159        BoundedExpr::BitVecConst { value, .. } => Term::Lit(Literal::Int(*value as i64)),
160        BoundedExpr::BitVecVar(name, _) => Term::Var(name.clone()),
161        BoundedExpr::BitVecBinary { op, left, right } => {
162            let l = encode_bounded_expr(left);
163            let r = encode_bounded_expr(right);
164            let op_name = match op {
165                super::sva_to_verify::BitVecBoundedOp::And => "bit_and",
166                super::sva_to_verify::BitVecBoundedOp::Or => "bit_or",
167                super::sva_to_verify::BitVecBoundedOp::Xor => "bit_xor",
168                super::sva_to_verify::BitVecBoundedOp::Add => "bv_add",
169                super::sva_to_verify::BitVecBoundedOp::Sub => "bv_sub",
170                _ => "bv_op",
171            };
172            Term::App(
173                Box::new(Term::App(
174                    Box::new(Term::Global(op_name.to_string())),
175                    Box::new(l),
176                )),
177                Box::new(r),
178            )
179        }
180        BoundedExpr::BitVecExtract { operand, .. } => encode_bounded_expr(operand),
181        BoundedExpr::BitVecConcat(l, r) => {
182            let left = encode_bounded_expr(l);
183            let right = encode_bounded_expr(r);
184            Term::App(
185                Box::new(Term::App(
186                    Box::new(Term::Global("bv_concat".to_string())),
187                    Box::new(left),
188                )),
189                Box::new(right),
190            )
191        }
192        BoundedExpr::ArraySelect { array, index } => {
193            let a = encode_bounded_expr(array);
194            let i = encode_bounded_expr(index);
195            Term::App(
196                Box::new(Term::App(
197                    Box::new(Term::Global("select".to_string())),
198                    Box::new(a),
199                )),
200                Box::new(i),
201            )
202        }
203        BoundedExpr::ArrayStore { array, index, value } => {
204            let a = encode_bounded_expr(array);
205            let i = encode_bounded_expr(index);
206            let v = encode_bounded_expr(value);
207            Term::App(
208                Box::new(Term::App(
209                    Box::new(Term::App(
210                        Box::new(Term::Global("store".to_string())),
211                        Box::new(a),
212                    )),
213                    Box::new(i),
214                )),
215                Box::new(v),
216            )
217        }
218        BoundedExpr::IntBinary { op, left, right } => {
219            let l = encode_bounded_expr(left);
220            let r = encode_bounded_expr(right);
221            let op_name = match op {
222                super::sva_to_verify::ArithBoundedOp::Add => "plus",
223                super::sva_to_verify::ArithBoundedOp::Sub => "minus",
224                super::sva_to_verify::ArithBoundedOp::Mul => "mult",
225                super::sva_to_verify::ArithBoundedOp::Div => "div",
226            };
227            Term::App(
228                Box::new(Term::App(
229                    Box::new(Term::Global(op_name.to_string())),
230                    Box::new(l),
231                )),
232                Box::new(r),
233            )
234        }
235        BoundedExpr::Comparison { op, left, right } => {
236            let l = encode_bounded_expr(left);
237            let r = encode_bounded_expr(right);
238            let op_name = match op {
239                super::sva_to_verify::CmpBoundedOp::Gt => "gt",
240                super::sva_to_verify::CmpBoundedOp::Lt => "lt",
241                super::sva_to_verify::CmpBoundedOp::Gte => "ge",
242                super::sva_to_verify::CmpBoundedOp::Lte => "le",
243            };
244            Term::App(
245                Box::new(Term::App(
246                    Box::new(Term::Global(op_name.to_string())),
247                    Box::new(l),
248                )),
249                Box::new(r),
250            )
251        }
252        BoundedExpr::ForAll { var, body, .. } => {
253            let b = encode_bounded_expr(body);
254            Term::Pi {
255                param: var.clone(),
256                param_type: Box::new(Term::Hole),
257                body_type: Box::new(b),
258            }
259        }
260        BoundedExpr::Exists { var, body, .. } => {
261            let b = encode_bounded_expr(body);
262            Term::App(
263                Box::new(Term::Global("Ex".to_string())),
264                Box::new(Term::Lambda {
265                    param: var.clone(),
266                    param_type: Box::new(Term::Hole),
267                    body: Box::new(b),
268                }),
269            )
270        }
271        BoundedExpr::Apply { name, args } => {
272            // Uninterpreted function: encode as nested application f(a1)(a2)...
273            let mut term = Term::Global(name.clone());
274            for arg in args {
275                term = Term::App(
276                    Box::new(term),
277                    Box::new(encode_bounded_expr(arg)),
278                );
279            }
280            term
281        }
282    }
283}
284
285/// Helper: build a Nat literal (Zero, Succ Zero, Succ (Succ Zero), ...)
286#[allow(dead_code)]
287fn nat_literal(n: usize) -> Term {
288    let mut term = Term::Global("Zero".to_string());
289    for _ in 0..n {
290        term = Term::App(
291            Box::new(Term::Global("Succ".to_string())),
292            Box::new(term),
293        );
294    }
295    term
296}
logicaffeine_compile/codegen_sva/verify_to_kernel.rs

logicaffeine_compile/codegen_sva/
verify_to_kernel.rs
