litex/verify/
verify_non_equational_atomic_fact.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_non_equational_atomic_fact(
5        &mut self,
6        atomic_fact: &AtomicFact,
7        verify_state: &VerifyState,
8        post_process: bool,
9    ) -> Result<StmtResult, RuntimeError> {
10        let mut result =
11            self.verify_non_equational_atomic_fact_with_builtin_rules(atomic_fact, verify_state)?;
12        if result.is_true() {
13            return Ok(result);
14        }
15
16        result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(atomic_fact)?;
17        if result.is_true() {
18            return Ok(result);
19        }
20
21        if verify_state.is_round_0() {
22            let verify_state_add_one_round = verify_state.new_state_with_round_increased();
23
24            if let Some(verified_by_definition) =
25                self.verify_atomic_fact_using_builtin_or_prop_definition(atomic_fact, verify_state)?
26            {
27                return Ok(verified_by_definition);
28            }
29
30            result = self
31                .verify_atomic_fact_with_known_forall(atomic_fact, &verify_state_add_one_round)?;
32            if result.is_true() {
33                return Ok(result);
34            }
35        }
36
37        if post_process {
38            result =
39                self.post_process_non_equational_atomic_fact(atomic_fact, verify_state, result)?;
40            if result.is_true() {
41                return Ok(result);
42            }
43        }
44
45        Ok((StmtUnknown::new()).into())
46    }
47
48    pub fn verify_non_equational_atomic_fact_with_known_atomic_facts(
49        &mut self,
50        atomic_fact: &AtomicFact,
51    ) -> Result<StmtResult, RuntimeError> {
52        let result = if atomic_fact.number_of_args() == 1 {
53            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(atomic_fact)?
54        } else if atomic_fact.number_of_args() == 2 {
55            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(atomic_fact)?
56        } else {
57            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
58                atomic_fact,
59            )?
60        };
61
62        if result.is_true() {
63            return Ok(result);
64        }
65
66        Ok(result)
67    }
68
69    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(
70        &mut self,
71        atomic_fact: &AtomicFact,
72    ) -> Result<StmtResult, RuntimeError> {
73        let mut all_objs_equal_to_arg =
74            self.get_all_objs_equal_to_given(&atomic_fact.args()[0].to_string());
75
76        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[0]) {
77            if calculated_obj.to_string() != atomic_fact.args()[0].to_string() {
78                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
79                all_objs_equal_to_arg.extend(equal_tos);
80            }
81        }
82
83        if all_objs_equal_to_arg.is_empty() {
84            all_objs_equal_to_arg.push(atomic_fact.args()[0].to_string());
85        }
86
87        for environment in self.iter_environments_from_top() {
88            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param_with_facts_in_environment(environment, atomic_fact, &all_objs_equal_to_arg)?;
89            if result.is_true() {
90                return Ok(result);
91            }
92        }
93
94        let arg = atomic_fact.args()[0].clone();
95        let arg_resolved = self.resolve_obj(&arg);
96        if arg_resolved.to_string() != arg.to_string() {
97            let rewritten =
98                Self::atomic_fact_with_resolved_unary_operand(atomic_fact, arg_resolved);
99            return self
100                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(&rewritten);
101        }
102
103        Ok((StmtUnknown::new()).into())
104    }
105
106    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(
107        &mut self,
108        atomic_fact: &AtomicFact,
109    ) -> Result<StmtResult, RuntimeError> {
110        let mut all_objs_equal_to_arg0 =
111            self.get_all_objs_equal_to_given(&atomic_fact.args()[0].to_string());
112        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[0]) {
113            if calculated_obj.to_string() != atomic_fact.args()[0].to_string() {
114                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
115                all_objs_equal_to_arg0.extend(equal_tos);
116            }
117        }
118        if all_objs_equal_to_arg0.is_empty() {
119            all_objs_equal_to_arg0.push(atomic_fact.args()[0].to_string());
120        }
121        let mut all_objs_equal_to_arg1 =
122            self.get_all_objs_equal_to_given(&atomic_fact.args()[1].to_string());
123        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[1]) {
124            if calculated_obj.to_string() != atomic_fact.args()[1].to_string() {
125                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
126                all_objs_equal_to_arg1.extend(equal_tos);
127            }
128        }
129        if all_objs_equal_to_arg1.is_empty() {
130            all_objs_equal_to_arg1.push(atomic_fact.args()[1].to_string());
131        }
132
133        for environment in self.iter_environments_from_top() {
134            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params_with_facts_in_environment(environment, atomic_fact, &all_objs_equal_to_arg0, &all_objs_equal_to_arg1)?;
135            if result.is_true() {
136                return Ok(result);
137            }
138        }
139
140        let left = atomic_fact.args()[0].clone();
141        let right = atomic_fact.args()[1].clone();
142        let left_resolved = self.resolve_obj(&left);
143        let right_resolved = self.resolve_obj(&right);
144        if left_resolved.to_string() != left.to_string()
145            || right_resolved.to_string() != right.to_string()
146        {
147            let rewritten = Self::atomic_fact_with_resolved_binary_operands(
148                atomic_fact,
149                left_resolved,
150                right_resolved,
151            );
152            return self
153                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(&rewritten);
154        }
155
156        Ok((StmtUnknown::new()).into())
157    }
158
159    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
160        &mut self,
161        atomic_fact: &AtomicFact,
162    ) -> Result<StmtResult, RuntimeError> {
163        let mut all_objs_equal_to_each_arg: Vec<Vec<String>> = Vec::new();
164        for arg in atomic_fact.args().iter() {
165            let mut all_objs_equal_to_current_arg =
166                self.get_all_objs_equal_to_given(&arg.to_string());
167            if all_objs_equal_to_current_arg.is_empty() {
168                all_objs_equal_to_current_arg.push(arg.to_string());
169            }
170            all_objs_equal_to_each_arg.push(all_objs_equal_to_current_arg);
171        }
172
173        for environment in self.iter_environments_from_top() {
174            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params_with_facts_in_environment(
175                environment,
176                atomic_fact,
177                &all_objs_equal_to_each_arg,
178            )?;
179            if result.is_true() {
180                return Ok(result);
181            }
182        }
183
184        let old_args = atomic_fact.args();
185        let mut new_args: Vec<Obj> = Vec::with_capacity(old_args.len());
186        let mut any_changed = false;
187        for a in old_args.iter() {
188            let r = self.resolve_obj(a);
189            if r.to_string() != a.to_string() {
190                any_changed = true;
191            }
192            new_args.push(r);
193        }
194        if any_changed {
195            let rewritten = Self::atomic_fact_with_resolved_predicate_args(atomic_fact, new_args);
196            return self
197                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
198                    &rewritten,
199                );
200        }
201
202        Ok((StmtUnknown::new()).into())
203    }
204
205    fn atomic_fact_with_resolved_unary_operand(fact: &AtomicFact, x: Obj) -> AtomicFact {
206        let line_file = fact.line_file();
207        match fact {
208            AtomicFact::IsSetFact(_) => IsSetFact::new(x, line_file).into(),
209            AtomicFact::IsNonemptySetFact(_) => IsNonemptySetFact::new(x, line_file).into(),
210            AtomicFact::IsFiniteSetFact(_) => IsFiniteSetFact::new(x, line_file).into(),
211            AtomicFact::IsCartFact(_) => IsCartFact::new(x, line_file).into(),
212            AtomicFact::IsTupleFact(_) => IsTupleFact::new(x, line_file).into(),
213            AtomicFact::NotIsSetFact(_) => NotIsSetFact::new(x, line_file).into(),
214            AtomicFact::NotIsNonemptySetFact(_) => NotIsNonemptySetFact::new(x, line_file).into(),
215            AtomicFact::NotIsFiniteSetFact(_) => NotIsFiniteSetFact::new(x, line_file).into(),
216            AtomicFact::NotIsCartFact(_) => NotIsCartFact::new(x, line_file).into(),
217            AtomicFact::NotIsTupleFact(_) => NotIsTupleFact::new(x, line_file).into(),
218            AtomicFact::NormalAtomicFact(n) => {
219                NormalAtomicFact::new(n.predicate.clone(), vec![x], line_file).into()
220            }
221            AtomicFact::NotNormalAtomicFact(n) => {
222                NotNormalAtomicFact::new(n.predicate.clone(), vec![x], line_file).into()
223            }
224            _ => unreachable!(
225                "atomic_fact_with_resolved_unary_operand: expected a one-argument atomic fact"
226            ),
227        }
228    }
229
230    fn atomic_fact_with_resolved_binary_operands(
231        fact: &AtomicFact,
232        left: Obj,
233        right: Obj,
234    ) -> AtomicFact {
235        let line_file = fact.line_file();
236        match fact {
237            AtomicFact::EqualFact(_) => EqualFact::new(left, right, line_file).into(),
238            AtomicFact::LessFact(_) => LessFact::new(left, right, line_file).into(),
239            AtomicFact::GreaterFact(_) => GreaterFact::new(left, right, line_file).into(),
240            AtomicFact::LessEqualFact(_) => LessEqualFact::new(left, right, line_file).into(),
241            AtomicFact::GreaterEqualFact(_) => GreaterEqualFact::new(left, right, line_file).into(),
242            AtomicFact::InFact(_) => InFact::new(left, right, line_file).into(),
243            AtomicFact::SubsetFact(_) => SubsetFact::new(left, right, line_file).into(),
244            AtomicFact::SupersetFact(_) => SupersetFact::new(left, right, line_file).into(),
245            AtomicFact::NotEqualFact(_) => NotEqualFact::new(left, right, line_file).into(),
246            AtomicFact::NotLessFact(_) => NotLessFact::new(left, right, line_file).into(),
247            AtomicFact::NotGreaterFact(_) => NotGreaterFact::new(left, right, line_file).into(),
248            AtomicFact::NotLessEqualFact(_) => NotLessEqualFact::new(left, right, line_file).into(),
249            AtomicFact::NotGreaterEqualFact(_) => {
250                NotGreaterEqualFact::new(left, right, line_file).into()
251            }
252            AtomicFact::NotInFact(_) => NotInFact::new(left, right, line_file).into(),
253            AtomicFact::NotSubsetFact(_) => NotSubsetFact::new(left, right, line_file).into(),
254            AtomicFact::NotSupersetFact(_) => NotSupersetFact::new(left, right, line_file).into(),
255            AtomicFact::RestrictFact(_) => RestrictFact::new(left, right, line_file).into(),
256            AtomicFact::NotRestrictFact(_) => NotRestrictFact::new(left, right, line_file).into(),
257            AtomicFact::NormalAtomicFact(x) => {
258                NormalAtomicFact::new(x.predicate.clone(), vec![left, right], line_file).into()
259            }
260            AtomicFact::NotNormalAtomicFact(x) => {
261                NotNormalAtomicFact::new(x.predicate.clone(), vec![left, right], line_file).into()
262            }
263            _ => unreachable!(
264                "atomic_fact_with_resolved_binary_operands: expected a two-argument atomic fact"
265            ),
266        }
267    }
268
269    fn atomic_fact_with_resolved_predicate_args(fact: &AtomicFact, args: Vec<Obj>) -> AtomicFact {
270        let line_file = fact.line_file();
271        match fact {
272            AtomicFact::NormalAtomicFact(x) => {
273                NormalAtomicFact::new(x.predicate.clone(), args, line_file).into()
274            }
275            AtomicFact::NotNormalAtomicFact(x) => {
276                NotNormalAtomicFact::new(x.predicate.clone(), args, line_file).into()
277            }
278            _ => unreachable!(
279                "atomic_fact_with_resolved_predicate_args: expected NormalAtomicFact or NotNormalAtomicFact"
280            ),
281        }
282    }
283
284    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param_with_facts_in_environment(
285        environment: &Environment,
286        atomic_fact: &AtomicFact,
287        all_objs_equal_to_arg: &Vec<String>,
288    ) -> Result<StmtResult, RuntimeError> {
289        if let Some(known_facts_map) = environment
290            .known_atomic_facts_with_1_arg
291            .get(&(atomic_fact.key(), atomic_fact.is_true()))
292        {
293            for obj in all_objs_equal_to_arg.iter() {
294                if let Some(known_atomic_fact) = known_facts_map.get(obj) {
295                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
296                        atomic_fact.clone().into(),
297                        VerifiedByResult::Fact(
298                            known_atomic_fact.clone().into(),
299                            known_atomic_fact.to_string(),
300                        ),
301                        Vec::new(),
302                    ))
303                    .into());
304                }
305            }
306        }
307
308        Ok((StmtUnknown::new()).into())
309    }
310
311    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params_with_facts_in_environment(
312        environment: &Environment,
313        atomic_fact: &AtomicFact,
314        all_objs_equal_to_arg0: &Vec<String>,
315        all_objs_equal_to_arg1: &Vec<String>,
316    ) -> Result<StmtResult, RuntimeError> {
317        if let Some(known_facts_map) = environment
318            .known_atomic_facts_with_2_args
319            .get(&(atomic_fact.key(), atomic_fact.is_true()))
320        {
321            for obj0 in all_objs_equal_to_arg0.iter() {
322                for obj1 in all_objs_equal_to_arg1.iter() {
323                    if let Some(known_atomic_fact) =
324                        known_facts_map.get(&(obj0.clone(), obj1.clone()))
325                    {
326                        return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
327                            atomic_fact.clone().into(),
328                            VerifiedByResult::Fact(
329                                known_atomic_fact.clone().into(),
330                                known_atomic_fact.to_string(),
331                            ),
332                            Vec::new(),
333                        ))
334                        .into());
335                    }
336                }
337            }
338        }
339
340        // Order facts are stored under `<` vs `>` etc.; e.g. known `a > 0` must match goal `0 < a`.
341        if let Some(alt) = atomic_fact.transposed_binary_order_equivalent() {
342            if let Some(known_facts_map) = environment
343                .known_atomic_facts_with_2_args
344                .get(&(alt.key(), alt.is_true()))
345            {
346                for obj0 in all_objs_equal_to_arg1.iter() {
347                    for obj1 in all_objs_equal_to_arg0.iter() {
348                        if let Some(known_atomic_fact) =
349                            known_facts_map.get(&(obj0.clone(), obj1.clone()))
350                        {
351                            return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
352                                atomic_fact.clone().into(),
353                                VerifiedByResult::Fact(
354                                    known_atomic_fact.clone().into(),
355                                    known_atomic_fact.to_string(),
356                                ),
357                                Vec::new(),
358                            ))
359                            .into());
360                        }
361                    }
362                }
363            }
364        }
365
366        Ok((StmtUnknown::new()).into())
367    }
368
369    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params_with_facts_in_environment(
370        environment: &Environment,
371        atomic_fact: &AtomicFact,
372        all_objs_equal_to_each_arg: &Vec<Vec<String>>,
373    ) -> Result<StmtResult, RuntimeError> {
374        if let Some(known_facts) = environment
375            .known_atomic_facts_with_0_or_more_than_2_args
376            .get(&(atomic_fact.key(), atomic_fact.is_true()))
377        {
378            for known_fact in known_facts.iter() {
379                if known_fact.args().len() != atomic_fact.args().len() {
380                    let message = format!(
381                        "known atomic fact {} has different number of args than the given fact {}",
382                        known_fact.to_string(),
383                        atomic_fact.to_string()
384                    );
385                    return Err({
386                        VerifyRuntimeError(RuntimeErrorStruct::new(
387                            Some(Fact::from(atomic_fact.clone()).into_stmt()),
388                            message.clone(),
389                            atomic_fact.line_file(),
390                            Some(
391                                UnknownRuntimeError(RuntimeErrorStruct::new(
392                                    Some(Fact::from(atomic_fact.clone()).into_stmt()),
393                                    message,
394                                    atomic_fact.line_file(),
395                                    None,
396                                    vec![],
397                                ))
398                                .into(),
399                            ),
400                            vec![],
401                        ))
402                        .into()
403                    });
404                }
405                let mut all_args_match = true;
406                for (index, known_arg) in known_fact.args().iter().enumerate() {
407                    let known_arg_string = known_arg.to_string();
408                    if !all_objs_equal_to_each_arg[index].contains(&known_arg_string) {
409                        all_args_match = false;
410                        break;
411                    }
412                }
413                if all_args_match {
414                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
415                        atomic_fact.clone().into(),
416                        VerifiedByResult::Fact(known_fact.clone().into(), known_fact.to_string()),
417                        Vec::new(),
418                    ))
419                    .into());
420                }
421            }
422        }
423
424        Ok((StmtUnknown::new()).into())
425    }
426
427    pub fn verify_fact(
428        &mut self,
429        fact: &Fact,
430        verify_state: &VerifyState,
431    ) -> Result<StmtResult, RuntimeError> {
432        match fact {
433            Fact::AtomicFact(atomic_fact) => self.verify_atomic_fact(atomic_fact, verify_state),
434            Fact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
435            Fact::ChainFact(chain_fact) => self.verify_chain_fact(chain_fact, verify_state),
436            Fact::ForallFact(forall_fact) => self.verify_forall_fact(forall_fact, verify_state),
437            Fact::ForallFactWithIff(forall_iff) => {
438                self.verify_forall_fact_with_iff(forall_iff, verify_state)
439            }
440            Fact::NotForall(not_forall) => self.verify_not_forall_fact(not_forall, verify_state),
441            Fact::ExistFact(exist_fact) => self.verify_exist_fact(exist_fact, verify_state),
442            Fact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
443        }
444    }
445
446    fn verify_subset_fact_by_membership_forall_definition(
447        &mut self,
448        subset_fact: &SubsetFact,
449        verify_state: &VerifyState,
450    ) -> Result<Option<StmtResult>, RuntimeError> {
451        let bound_param_name = self.generate_random_unused_name();
452        let membership_forall_fact = ForallFact::new(
453            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
454                vec![bound_param_name.clone()],
455                ParamType::Obj(subset_fact.left.clone()),
456            )]),
457            vec![],
458            vec![InFact::new(
459                obj_for_bound_param_in_scope(bound_param_name.clone(), ParamObjType::Forall),
460                subset_fact.right.clone(),
461                subset_fact.line_file.clone(),
462            )
463            .into()],
464            subset_fact.line_file.clone(),
465        )?
466        .into();
467        let verify_forall_result = self.verify_fact(&membership_forall_fact, verify_state)?;
468        if !verify_forall_result.is_true() {
469            return Ok(None);
470        }
471        Ok(Some(
472            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
473                subset_fact.clone().into(),
474                "subset by definition (forall x in left: x in right)".to_string(),
475                Vec::new(),
476            ))
477            .into(),
478        ))
479    }
480
481    fn verify_superset_fact_by_membership_forall_definition(
482        &mut self,
483        superset_fact: &SupersetFact,
484        verify_state: &VerifyState,
485    ) -> Result<Option<StmtResult>, RuntimeError> {
486        let bound_param_name = self.generate_random_unused_name();
487        let membership_forall_fact = ForallFact::new(
488            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
489                vec![bound_param_name.clone()],
490                ParamType::Obj(superset_fact.right.clone()),
491            )]),
492            vec![],
493            vec![InFact::new(
494                obj_for_bound_param_in_scope(bound_param_name.clone(), ParamObjType::Forall),
495                superset_fact.left.clone(),
496                superset_fact.line_file.clone(),
497            )
498            .into()],
499            superset_fact.line_file.clone(),
500        )?
501        .into();
502        let verify_forall_result = self.verify_fact(&membership_forall_fact, verify_state)?;
503        if !verify_forall_result.is_true() {
504            return Ok(None);
505        }
506        Ok(Some(
507            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
508                superset_fact.clone().into(),
509                "superset by definition (forall x in right: x in left)".to_string(),
510                Vec::new(),
511            ))
512            .into(),
513        ))
514    }
515
516    // Built-in subset/superset/restrict_fn_in definitions first, then user `prop` iff-clauses.
517    fn verify_atomic_fact_using_builtin_or_prop_definition(
518        &mut self,
519        atomic_fact: &AtomicFact,
520        verify_state: &VerifyState,
521    ) -> Result<Option<StmtResult>, RuntimeError> {
522        if let Some(result) =
523            self.verify_builtin_fact_with_their_definition(atomic_fact, verify_state)?
524        {
525            return Ok(Some(result));
526        }
527        if let AtomicFact::NormalAtomicFact(n) = atomic_fact {
528            return self.verify_normal_atomic_fact_using_its_definition(n, verify_state);
529        }
530        Ok(None)
531    }
532
533    fn verify_normal_atomic_fact_using_its_definition(
534        &mut self,
535        normal_atomic_fact: &NormalAtomicFact,
536        verify_state: &VerifyState,
537    ) -> Result<Option<StmtResult>, RuntimeError> {
538        if let Some(_) =
539            self.get_abstract_prop_definition_by_name(&normal_atomic_fact.predicate.to_string())
540        {
541            return Ok(None);
542        }
543
544        let predicate_name = normal_atomic_fact.predicate.to_string();
545
546        let definition = match self.get_prop_definition_by_name(&predicate_name) {
547            Some(definition_reference) => definition_reference.clone(),
548            None => {
549                return Err({
550                    VerifyRuntimeError(RuntimeErrorStruct::new(
551                        Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
552                        format!("prop definition not found for {}", predicate_name),
553                        normal_atomic_fact.line_file.clone(),
554                        None,
555                        vec![],
556                    ))
557                    .into()
558                })
559            }
560        };
561
562        let verify_state_for_definition_clauses = verify_state;
563
564        let args_param_types = match self.verify_args_satisfy_param_def_flat_types(
565            &definition.params_def_with_type,
566            &normal_atomic_fact.body,
567            verify_state_for_definition_clauses,
568            ParamObjType::DefHeader,
569        ) {
570            Ok(x) => x,
571            Err(_) => {
572                return Err({
573                    VerifyRuntimeError(RuntimeErrorStruct::new(
574                        Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
575                        format!("failed to verify parameter types for {}", predicate_name),
576                        normal_atomic_fact.line_file.clone(),
577                        None,
578                        vec![],
579                    ))
580                    .into()
581                })
582            }
583        };
584        if args_param_types.is_unknown() {
585            return Ok(None);
586        }
587
588        if definition.iff_facts.is_empty() {
589            return Ok(None);
590        }
591
592        let param_to_arg_map = definition
593            .params_def_with_type
594            .param_defs_and_args_to_param_to_arg_map(normal_atomic_fact.body.as_slice());
595
596        let mut infer_result = InferResult::new();
597        let mut definition_clause_descriptions: Vec<String> = Vec::new();
598
599        for iff_fact in definition.iff_facts.iter() {
600            let instantiated_iff_fact = self
601                .inst_fact(iff_fact, &param_to_arg_map, ParamObjType::DefHeader, None)
602                .map_err(|e| {
603                    {
604                        RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
605                            Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
606                            String::new(),
607                            normal_atomic_fact.line_file.clone(),
608                            Some(e),
609                            vec![],
610                        )))
611                    }
612                })?;
613            let iff_clause_verify_result =
614                self.verify_fact(&instantiated_iff_fact, &verify_state_for_definition_clauses)?;
615            if iff_clause_verify_result.is_unknown() {
616                return Ok(None);
617            }
618            match &iff_clause_verify_result {
619                StmtResult::FactualStmtSuccess(factual_success) => {
620                    infer_result.new_infer_result_inside(factual_success.infers.clone());
621                    definition_clause_descriptions
622                        .push(factual_success.verification_display_line());
623                }
624                StmtResult::NonFactualStmtSuccess(non_factual_success) => {
625                    infer_result.new_infer_result_inside(non_factual_success.infers.clone());
626                }
627                StmtResult::StmtUnknown(_) => return Ok(None),
628            }
629        }
630
631        let verified_by_text = format!(
632            "prop with meaning `{}` (param constraints and definition clauses): {}",
633            predicate_name,
634            definition_clause_descriptions.join("; ")
635        );
636        infer_result.new_fact(&normal_atomic_fact.clone().into());
637        Ok(Some(
638            (FactualStmtSuccess::new_with_verified_by_known_fact_and_infer(
639                normal_atomic_fact.clone().into(),
640                infer_result,
641                VerifiedByResult::Fact(normal_atomic_fact.clone().into(), verified_by_text),
642                Vec::new(),
643            ))
644            .into(),
645        ))
646    }
647
648    fn verify_builtin_fact_with_their_definition(
649        &mut self,
650        fact: &AtomicFact,
651        verify_state: &VerifyState,
652    ) -> Result<Option<StmtResult>, RuntimeError> {
653        match fact {
654            AtomicFact::SubsetFact(subset_fact) => {
655                if let Some(verified_by_subset_definition) = self
656                    .verify_subset_fact_by_membership_forall_definition(subset_fact, verify_state)?
657                {
658                    return Ok(Some(verified_by_subset_definition));
659                }
660                return Ok(None);
661            }
662            AtomicFact::SupersetFact(superset_fact) => {
663                if let Some(verified_by_superset_definition) = self
664                    .verify_superset_fact_by_membership_forall_definition(
665                        superset_fact,
666                        verify_state,
667                    )?
668                {
669                    return Ok(Some(verified_by_superset_definition));
670                }
671                return Ok(None);
672            }
673            AtomicFact::RestrictFact(restrict_fact) => {
674                if let Some(verified_by_restrict_definition) =
675                    self.verify_restrict_fact_using_its_definition(restrict_fact, verify_state)?
676                {
677                    return Ok(Some(verified_by_restrict_definition));
678                }
679                return Ok(None);
680            }
681            _ => {}
682        }
683        Ok(None)
684    }
685
686    // If direct verification failed, try the order-dual with swapped operands (e.g. a >= b via b <= a).
687    fn post_process_non_equational_atomic_fact(
688        &mut self,
689        atomic_fact: &AtomicFact,
690        verify_state: &VerifyState,
691        result: StmtResult,
692    ) -> Result<StmtResult, RuntimeError> {
693        let Some(transposed_fact) = atomic_fact.transposed_binary_order_equivalent() else {
694            return Ok(result);
695        };
696        let transposed_result =
697            self.verify_non_equational_atomic_fact(&transposed_fact, verify_state, false)?;
698        match transposed_result {
699            StmtResult::FactualStmtSuccess(inner_success) => {
700                let FactualStmtSuccess {
701                    verified_by,
702                    infers: _,
703                    stmt: _,
704                } = inner_success;
705                Ok(FactualStmtSuccess::new_with_verified_by_known_fact(
706                    atomic_fact.clone().into(),
707                    verified_by,
708                    Vec::new(),
709                )
710                .into())
711            }
712            other if other.is_true() => Ok(other),
713            _ => Ok(result),
714        }
715    }
716}
litex/verify/verify_non_equational_atomic_fact.rs

litex/verify/
verify_non_equational_atomic_fact.rs
