logicaffeine_compile/codegen_sva/
fol_to_verify.rs

1//! FOL → Bounded Verification IR Translation
2//!
3//! Translates Kripke-lowered LogicExpr to a bounded timestep model.
4//! World variables (w0, w1, ...) become timestep indices.
5//! Temporal accessibility predicates control the unrolling.
6
7use logicaffeine_language::ast::logic::{LogicExpr, QuantifierKind, TemporalOperator, BinaryTemporalOp, Term, ThematicRole};
8use logicaffeine_language::Interner;
9use logicaffeine_language::token::TokenType;
10use super::sva_to_verify::BoundedExpr;
11use super::hw_pipeline::SignalMap;
12use std::collections::{HashMap, HashSet};
13use logicaffeine_base::Symbol;
14
15/// Translator from Kripke-lowered FOL to bounded timestep model.
16pub struct FolTranslator<'a> {
17    interner: &'a Interner,
18    bound: u32,
19    /// Maps world variable symbols to fixed timesteps
20    world_map: HashMap<Symbol, u32>,
21    /// Accumulated signal declarations
22    declarations: HashSet<String>,
23    /// Optional signal map for FOL arg → SVA signal name mapping
24    signal_map: Option<&'a SignalMap>,
25    /// When true, collapse ∀x(P(x) → TruthPred(x)) to just P even without a signal map.
26    /// Used by the consistency checker to ensure contradictory specs produce conflicting variables.
27    collapse_truth_predicates: bool,
28}
29
30impl<'a> FolTranslator<'a> {
31    pub fn new(interner: &'a Interner, bound: u32) -> Self {
32        Self {
33            interner,
34            bound,
35            world_map: HashMap::new(),
36            declarations: HashSet::new(),
37            signal_map: None,
38            collapse_truth_predicates: false,
39        }
40    }
41
42    /// Enable truth predicate collapsing for consistency checking.
43    pub fn set_collapse_truth_predicates(&mut self, collapse: bool) {
44        self.collapse_truth_predicates = collapse;
45    }
46
47    /// Set a signal map for translating FOL argument names to SVA signal names.
48    pub fn set_signal_map(&mut self, map: &'a SignalMap) {
49        self.signal_map = Some(map);
50    }
51
52    /// Try to extract an accessibility predicate pattern from a quantifier body.
53    ///
54    /// For existential: body is `And(Reachable_Temporal(w_source, w_target), actual_body)`
55    /// Returns (source_world_symbol, actual_body, is_strictly_future)
56    fn extract_accessibility_from_existential<'b>(
57        &self,
58        body: &'b LogicExpr<'b>,
59        quantified_var: Symbol,
60    ) -> Option<(Symbol, &'b LogicExpr<'b>, bool)> {
61        if let LogicExpr::BinaryOp { left, op, right } = body {
62            if matches!(op, TokenType::And) {
63                if let LogicExpr::Predicate { name, args, world: None } = *left {
64                    let pred_name = self.interner.resolve(*name);
65                    if pred_name == "Reachable_Temporal" || pred_name == "Accessible_Temporal" {
66                        if args.len() >= 2 {
67                            if let (Term::Variable(source), Term::Variable(target)) = (&args[0], &args[1]) {
68                                if *target == quantified_var {
69                                    let strictly_future = pred_name == "Reachable_Temporal";
70                                    return Some((*source, right, strictly_future));
71                                }
72                            }
73                        }
74                    }
75                }
76            }
77        }
78        None
79    }
80
81    /// Try to extract an accessibility predicate pattern from a universal quantifier body.
82    ///
83    /// For universal: body is `Implies(Accessible_Temporal(w_source, w_target), actual_body)`
84    /// Returns (source_world_symbol, actual_body, predicate_name)
85    fn extract_accessibility_from_universal<'b>(
86        &self,
87        body: &'b LogicExpr<'b>,
88        quantified_var: Symbol,
89    ) -> Option<(Symbol, &'b LogicExpr<'b>, &'a str)> {
90        if let LogicExpr::BinaryOp { left, op, right } = body {
91            if matches!(op, TokenType::If | TokenType::Implies) {
92                if let LogicExpr::Predicate { name, args, world: None } = *left {
93                    let pred_name = self.interner.resolve(*name);
94                    if pred_name == "Accessible_Temporal"
95                        || pred_name == "Reachable_Temporal"
96                        || pred_name == "Next_Temporal"
97                    {
98                        if args.len() >= 2 {
99                            if let (Term::Variable(source), Term::Variable(target)) = (&args[0], &args[1]) {
100                                if *target == quantified_var {
101                                    return Some((*source, right, pred_name));
102                                }
103                            }
104                        }
105                    }
106                }
107            }
108        }
109        None
110    }
111
112    /// Translate a Kripke-lowered LogicExpr to bounded verification IR.
113    pub fn translate(&mut self, expr: &LogicExpr<'_>) -> BoundedExpr {
114        match expr {
115            // Predicates with world arguments → timestamped variables
116            LogicExpr::Predicate { name, args, world } => {
117                let pred_name = self.interner.resolve(*name).to_string();
118
119                // Accessibility predicates — evaluate ordering constraint
120                if pred_name == "Accessible_Temporal"
121                    || pred_name == "Reachable_Temporal"
122                    || pred_name == "Next_Temporal"
123                {
124                    // Extract source and target world timesteps from args
125                    if args.len() >= 2 {
126                        if let (Term::Variable(source), Term::Variable(target)) = (&args[0], &args[1]) {
127                            let source_t = self.world_map.get(source).copied().unwrap_or(0);
128                            let target_t = self.world_map.get(target).copied().unwrap_or(0);
129
130                            return match pred_name.as_str() {
131                                "Accessible_Temporal" => BoundedExpr::Bool(target_t >= source_t),
132                                "Reachable_Temporal" => BoundedExpr::Bool(target_t > source_t),
133                                "Next_Temporal" => BoundedExpr::Bool(target_t == source_t + 1),
134                                _ => BoundedExpr::Bool(true),
135                            };
136                        }
137                    }
138                    // Fallback if args don't match expected structure
139                    return BoundedExpr::Bool(true);
140                }
141
142                // Regular predicate with world → timestamped variable
143                if let Some(w) = world {
144                    let timestep = self.world_map.get(w).copied().unwrap_or(0);
145
146                    // Check if the predicate name itself matches a signal declaration
147                    if let Some(signal_map) = self.signal_map {
148                        if let Some(sva_name) = signal_map.resolve(&pred_name) {
149                            let var_name = format!("{}@{}", sva_name, timestep);
150                            self.declarations.insert(var_name.clone());
151                            return BoundedExpr::Var(var_name);
152                        }
153                    }
154
155                    if args.is_empty() {
156                        let var_name = format!("{}@{}", pred_name, timestep);
157                        self.declarations.insert(var_name.clone());
158                        return BoundedExpr::Var(var_name);
159                    }
160                    // Multi-arg predicate: use first arg as signal name
161                    if let Some(arg) = args.first() {
162                        let arg_name = self.term_to_string(arg);
163
164                        // If signal map has this argument (constant/proper noun),
165                        // use the mapped signal name
166                        if let Some(signal_map) = self.signal_map {
167                            if let Some(sva_name) = signal_map.resolve(&arg_name) {
168                                let var_name = format!("{}@{}", sva_name, timestep);
169                                self.declarations.insert(var_name.clone());
170                                return BoundedExpr::Var(var_name);
171                            }
172                        }
173
174                        let var_name = format!("{}_{}_@{}", pred_name, arg_name, timestep);
175                        self.declarations.insert(var_name.clone());
176                        return BoundedExpr::Var(var_name);
177                    }
178                }
179
180                // Predicate without world → static (non-temporal)
181                let var_name = pred_name;
182                self.declarations.insert(var_name.clone());
183                BoundedExpr::Var(var_name)
184            }
185
186            // Universal quantifier over worlds → conjunction over timesteps
187            LogicExpr::Quantifier { kind: QuantifierKind::Universal, variable, body, .. } => {
188                let var_name = self.interner.resolve(*variable).to_string();
189                if var_name.starts_with('w') {
190                    // Check for accessibility predicate pattern in body
191                    if let Some((source_world, actual_body, pred_kind)) =
192                        self.extract_accessibility_from_universal(body, *variable)
193                    {
194                        let source_t = self.world_map.get(&source_world).copied().unwrap_or(0);
195
196                        // Next_Temporal: exactly one timestep (source + 1)
197                        if pred_kind == "Next_Temporal" {
198                            let next_t = source_t + 1;
199                            self.world_map.insert(*variable, next_t);
200                            let step = self.translate(actual_body);
201                            self.world_map.remove(variable);
202                            return step;
203                        }
204
205                        let (start, end) = match pred_kind {
206                            "Accessible_Temporal" => (source_t, source_t + self.bound),
207                            "Reachable_Temporal" => (source_t + 1, source_t + 1 + self.bound),
208                            _ => (0, self.bound),
209                        };
210
211                        let mut result: Option<BoundedExpr> = None;
212                        for t in start..end {
213                            self.world_map.insert(*variable, t);
214                            let step = self.translate(actual_body);
215                            result = Some(match result {
216                                None => step,
217                                Some(acc) => BoundedExpr::And(Box::new(acc), Box::new(step)),
218                            });
219                        }
220                        self.world_map.remove(variable);
221                        return result.unwrap_or(BoundedExpr::Bool(true));
222                    }
223
224                    // Fallback: generic world quantifier — iterate 0..bound
225                    let mut result: Option<BoundedExpr> = None;
226                    for t in 0..self.bound {
227                        self.world_map.insert(*variable, t);
228                        let step = self.translate(body);
229                        result = Some(match result {
230                            None => step,
231                            Some(acc) => BoundedExpr::And(Box::new(acc), Box::new(step)),
232                        });
233                    }
234                    self.world_map.remove(variable);
235                    result.unwrap_or(BoundedExpr::Bool(true))
236                } else {
237                    // Regular variable quantifier: check for signal collapsing pattern
238                    // ∀x(Restrictor(x,w) → TruthPredicate(x,w)) → just Restrictor@t
239                    // ∀x(Restrictor(x,w) → ¬TruthPredicate(x,w)) → ¬Restrictor@t
240                    if self.signal_map.is_some() || self.collapse_truth_predicates {
241                        if let LogicExpr::BinaryOp { left, right, op } = body {
242                            if matches!(op, TokenType::If | TokenType::Implies) {
243                                if self.is_truth_expr(right) {
244                                    // When collapsing, use just the restrictor predicate name
245                                    // (without variable suffix) for cross-sentence consistency.
246                                    let restrictor = if self.signal_map.is_some() {
247                                        // With signal map: normal translation (uses mapped name)
248                                        self.translate(left)
249                                    } else {
250                                        // Without signal map (consistency mode): use bare predicate name
251                                        self.translate_predicate_bare(left)
252                                    };
253                                    if matches!(right, LogicExpr::UnaryOp { .. }) {
254                                        return BoundedExpr::Not(Box::new(restrictor));
255                                    }
256                                    return restrictor;
257                                }
258                            }
259                        }
260                    }
261                    self.translate(body)
262                }
263            }
264
265            // Existential quantifier over worlds → disjunction over timesteps
266            LogicExpr::Quantifier { kind: QuantifierKind::Existential, variable, body, .. } => {
267                let var_name = self.interner.resolve(*variable).to_string();
268                if var_name.starts_with('w') {
269                    // Check for accessibility predicate pattern in body
270                    if let Some((source_world, actual_body, strictly_future)) =
271                        self.extract_accessibility_from_existential(body, *variable)
272                    {
273                        let source_t = self.world_map.get(&source_world).copied().unwrap_or(0);
274                        let start = if strictly_future { source_t + 1 } else { source_t };
275                        let end = start + self.bound;
276
277                        let mut result: Option<BoundedExpr> = None;
278                        for t in start..end {
279                            self.world_map.insert(*variable, t);
280                            let step = self.translate(actual_body);
281                            result = Some(match result {
282                                None => step,
283                                Some(acc) => BoundedExpr::Or(Box::new(acc), Box::new(step)),
284                            });
285                        }
286                        self.world_map.remove(variable);
287                        return result.unwrap_or(BoundedExpr::Bool(false));
288                    }
289
290                    // Fallback: generic world quantifier — iterate 0..bound
291                    let mut result: Option<BoundedExpr> = None;
292                    for t in 0..self.bound {
293                        self.world_map.insert(*variable, t);
294                        let step = self.translate(body);
295                        result = Some(match result {
296                            None => step,
297                            Some(acc) => BoundedExpr::Or(Box::new(acc), Box::new(step)),
298                        });
299                    }
300                    self.world_map.remove(variable);
301                    result.unwrap_or(BoundedExpr::Bool(false))
302                } else {
303                    self.translate(body)
304                }
305            }
306
307            // Binary connectives
308            LogicExpr::BinaryOp { left, op, right } => {
309                let l = self.translate(left);
310                let r = self.translate(right);
311                match op {
312                    TokenType::And => {
313                        BoundedExpr::And(Box::new(l), Box::new(r))
314                    }
315                    TokenType::Or => {
316                        BoundedExpr::Or(Box::new(l), Box::new(r))
317                    }
318                    TokenType::If
319                    | TokenType::Implies => {
320                        BoundedExpr::Implies(Box::new(l), Box::new(r))
321                    }
322                    _ => {
323                        // Other binary ops: default to And
324                        BoundedExpr::And(Box::new(l), Box::new(r))
325                    }
326                }
327            }
328
329            // Negation
330            LogicExpr::UnaryOp { operand, .. } => {
331                let inner = self.translate(operand);
332                BoundedExpr::Not(Box::new(inner))
333            }
334
335            // LTL temporal operators (if not already Kripke-lowered)
336            LogicExpr::Temporal { operator, body } => {
337                match operator {
338                    TemporalOperator::Always => {
339                        // G(P) → conjunction over all timesteps
340                        let mut result: Option<BoundedExpr> = None;
341                        for _t in 0..self.bound {
342                            // Temporarily set world mapping
343                            let step = self.translate(body);
344                            result = Some(match result {
345                                None => step,
346                                Some(acc) => BoundedExpr::And(Box::new(acc), Box::new(step)),
347                            });
348                        }
349                        result.unwrap_or(BoundedExpr::Bool(true))
350                    }
351                    TemporalOperator::Eventually => {
352                        let mut result: Option<BoundedExpr> = None;
353                        for _t in 0..self.bound {
354                            let step = self.translate(body);
355                            result = Some(match result {
356                                None => step,
357                                Some(acc) => BoundedExpr::Or(Box::new(acc), Box::new(step)),
358                            });
359                        }
360                        result.unwrap_or(BoundedExpr::Bool(false))
361                    }
362                    _ => self.translate(body),
363                }
364            }
365
366            // Binary temporal operators — each has distinct bounded semantics
367            LogicExpr::TemporalBinary { operator, left, right } => {
368                let l = self.translate(left);
369                let r = self.translate(right);
370                match operator {
371                    BinaryTemporalOp::Until => {
372                        self.unroll_until(&l, &r, 0)
373                    }
374                    BinaryTemporalOp::Release => {
375                        self.unroll_release(&l, &r, 0)
376                    }
377                    BinaryTemporalOp::WeakUntil => {
378                        let until = self.unroll_until(&l, &r, 0);
379                        let always = self.unroll_always(&l, 0);
380                        BoundedExpr::Or(Box::new(until), Box::new(always))
381                    }
382                }
383            }
384
385            // Identity/equality
386            LogicExpr::Identity { left, right, .. } => {
387                let l = self.term_to_bounded(left);
388                let r = self.term_to_bounded(right);
389                BoundedExpr::Eq(Box::new(l), Box::new(r))
390            }
391
392            // Neo-Davidsonian event: extract verb + agent as signal name
393            LogicExpr::NeoEvent(data) => {
394                let verb_name = self.interner.resolve(data.verb).to_string();
395                let timestep = data.world
396                    .and_then(|w| self.world_map.get(&w).copied())
397                    .unwrap_or(0);
398
399                // Extract agent from roles for signal naming
400                let agent_name = data.roles.iter()
401                    .find(|(role, _)| matches!(role, ThematicRole::Agent))
402                    .map(|(_, term)| self.term_to_string(term));
403
404                if let Some(ref arg_name) = agent_name {
405                    if let Some(signal_map) = self.signal_map {
406                        if let Some(sva_name) = signal_map.resolve(arg_name) {
407                            let var_name = format!("{}@{}", sva_name, timestep);
408                            self.declarations.insert(var_name.clone());
409                            return BoundedExpr::Var(var_name);
410                        }
411                        if let Some(sva_name) = signal_map.resolve(&verb_name) {
412                            let var_name = format!("{}@{}", sva_name, timestep);
413                            self.declarations.insert(var_name.clone());
414                            return BoundedExpr::Var(var_name);
415                        }
416                    }
417                    let var_name = format!("{}_{}_@{}", verb_name, arg_name, timestep);
418                    self.declarations.insert(var_name.clone());
419                    BoundedExpr::Var(var_name)
420                } else {
421                    if let Some(signal_map) = self.signal_map {
422                        if let Some(sva_name) = signal_map.resolve(&verb_name) {
423                            let var_name = format!("{}@{}", sva_name, timestep);
424                            self.declarations.insert(var_name.clone());
425                            return BoundedExpr::Var(var_name);
426                        }
427                    }
428                    let var_name = format!("{}@{}", verb_name, timestep);
429                    self.declarations.insert(var_name.clone());
430                    BoundedExpr::Var(var_name)
431                }
432            }
433
434            // Modal: unwrap
435            LogicExpr::Modal { operand, .. } => {
436                self.translate(operand)
437            }
438
439            // Catch-all: fail closed (false, not true) for unhandled constructs.
440            // Unsupported constructs must NOT silently become vacuously true.
441            _ => BoundedExpr::Bool(false),
442        }
443    }
444
445    /// Translate a full Kripke-lowered expression as a property (for all timesteps).
446    pub fn translate_property(&mut self, expr: &LogicExpr<'_>) -> super::sva_to_verify::TranslateResult {
447        let expr_result = self.translate(expr);
448        let declarations: Vec<String> = self.declarations.iter().cloned().collect();
449        super::sva_to_verify::TranslateResult {
450            expr: expr_result,
451            declarations,
452        }
453    }
454
455    /// Unroll φ U ψ (Until) to bounded depth.
456    fn unroll_until(&self, phi: &BoundedExpr, psi: &BoundedExpr, depth: u32) -> BoundedExpr {
457        if depth >= self.bound {
458            psi.clone()
459        } else {
460            let rest = self.unroll_until(phi, psi, depth + 1);
461            BoundedExpr::Or(
462                Box::new(psi.clone()),
463                Box::new(BoundedExpr::And(
464                    Box::new(phi.clone()),
465                    Box::new(rest),
466                )),
467            )
468        }
469    }
470
471    /// Unroll φ R ψ (Release) to bounded depth.
472    fn unroll_release(&self, phi: &BoundedExpr, psi: &BoundedExpr, depth: u32) -> BoundedExpr {
473        if depth >= self.bound {
474            psi.clone()
475        } else {
476            let rest = self.unroll_release(phi, psi, depth + 1);
477            BoundedExpr::And(
478                Box::new(psi.clone()),
479                Box::new(BoundedExpr::Or(
480                    Box::new(phi.clone()),
481                    Box::new(rest),
482                )),
483            )
484        }
485    }
486
487    /// Unroll G(φ) (Always) to bounded depth.
488    fn unroll_always(&self, phi: &BoundedExpr, depth: u32) -> BoundedExpr {
489        if depth >= self.bound {
490            phi.clone()
491        } else {
492            let rest = self.unroll_always(phi, depth + 1);
493            BoundedExpr::And(Box::new(phi.clone()), Box::new(rest))
494        }
495    }
496
497    /// Check if a LogicExpr is a truth predicate (hold/have/valid/active)
498    /// or a negation of one. Used for quantifier collapsing:
499    /// ∀x(Signal(x) → TruthPred(x)) → Signal
500    /// ∀x(Signal(x) → ¬TruthPred(x)) → ¬Signal
501    fn is_truth_expr(&self, expr: &LogicExpr<'_>) -> bool {
502        match expr {
503            LogicExpr::Predicate { name, .. } => {
504                let pred_name = self.interner.resolve(*name).to_string();
505                is_truth_predicate(&pred_name)
506            }
507            LogicExpr::NeoEvent(data) => {
508                let verb_name = self.interner.resolve(data.verb).to_string();
509                is_truth_predicate(&verb_name)
510            }
511            LogicExpr::UnaryOp { operand, .. } => self.is_truth_expr(operand),
512            _ => false,
513        }
514    }
515
516    /// Translate a restrictor predicate using just its name (no variable suffix).
517    /// Used in consistency mode to ensure cross-sentence variable consistency.
518    fn translate_predicate_bare(&mut self, expr: &LogicExpr<'_>) -> BoundedExpr {
519        match expr {
520            LogicExpr::Predicate { name, world, .. } => {
521                let pred_name = self.interner.resolve(*name).to_string();
522                let timestep = world
523                    .and_then(|w| self.world_map.get(&w).copied())
524                    .unwrap_or(0);
525                let var_name = format!("{}@{}", pred_name, timestep);
526                self.declarations.insert(var_name.clone());
527                BoundedExpr::Var(var_name)
528            }
529            _ => self.translate(expr),
530        }
531    }
532
533    fn term_to_string(&self, term: &Term<'_>) -> String {
534        match term {
535            Term::Constant(sym) | Term::Variable(sym) => {
536                self.interner.resolve(*sym).to_string()
537            }
538            Term::Function(sym, _) => self.interner.resolve(*sym).to_string(),
539            _ => "unknown".to_string(),
540        }
541    }
542
543    fn term_to_bounded(&self, term: &Term<'_>) -> BoundedExpr {
544        let name = self.term_to_string(term);
545        BoundedExpr::Var(name)
546    }
547}
548
549/// Check if a predicate name is a "truth predicate" — a copula-like verb
550/// that means "the signal is true" in hardware context.
551/// When a signal map is present and the restrictor maps to a signal,
552/// truth predicates should be elided (the signal itself carries the boolean).
553fn is_truth_predicate(name: &str) -> bool {
554    let lower = name.to_lowercase();
555    matches!(lower.as_str(),
556        "hold" | "holds" | "have" | "has" | "had"
557        | "valid" | "active" | "true" | "assert" | "asserted"
558    )
559}
logicaffeine_compile/codegen_sva/fol_to_verify.rs

logicaffeine_compile/codegen_sva/
fol_to_verify.rs
