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_source_recording_facts(
296                            atomic_fact.clone().into(),
297                            known_atomic_fact.to_string(),
298                            Some(known_atomic_fact.clone().into()),
299                            None,
300                            Vec::new(),
301                        )).into());
302                }
303            }
304        }
305
306        Ok((StmtUnknown::new()).into())
307    }
308
309    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params_with_facts_in_environment(
310        environment: &Environment,
311        atomic_fact: &AtomicFact,
312        all_objs_equal_to_arg0: &Vec<String>,
313        all_objs_equal_to_arg1: &Vec<String>,
314    ) -> Result<StmtResult, RuntimeError> {
315        if let Some(known_facts_map) = environment
316            .known_atomic_facts_with_2_args
317            .get(&(atomic_fact.key(), atomic_fact.is_true()))
318        {
319            for obj0 in all_objs_equal_to_arg0.iter() {
320                for obj1 in all_objs_equal_to_arg1.iter() {
321                    if let Some(known_atomic_fact) =
322                        known_facts_map.get(&(obj0.clone(), obj1.clone()))
323                    {
324                        return Ok((FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
325                                atomic_fact.clone().into(),
326                                known_atomic_fact.to_string(),
327                                Some(known_atomic_fact.clone().into()),
328                                None,
329                                Vec::new(),
330                            )).into());
331                    }
332                }
333            }
334        }
335
336        // Order facts are stored under `<` vs `>` etc.; e.g. known `a > 0` must match goal `0 < a`.
337        if let Some(alt) = atomic_fact.transposed_binary_order_equivalent() {
338            if let Some(known_facts_map) = environment
339                .known_atomic_facts_with_2_args
340                .get(&(alt.key(), alt.is_true()))
341            {
342                for obj0 in all_objs_equal_to_arg1.iter() {
343                    for obj1 in all_objs_equal_to_arg0.iter() {
344                        if let Some(known_atomic_fact) =
345                            known_facts_map.get(&(obj0.clone(), obj1.clone()))
346                        {
347                            return Ok((FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
348                                    atomic_fact.clone().into(),
349                                    known_atomic_fact.to_string(),
350                                    Some(known_atomic_fact.clone().into()),
351                                    None,
352                                    Vec::new(),
353                                )).into());
354                        }
355                    }
356                }
357            }
358        }
359
360        Ok((StmtUnknown::new()).into())
361    }
362
363    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params_with_facts_in_environment(
364        environment: &Environment,
365        atomic_fact: &AtomicFact,
366        all_objs_equal_to_each_arg: &Vec<Vec<String>>,
367    ) -> Result<StmtResult, RuntimeError> {
368        if let Some(known_facts) = environment
369            .known_atomic_facts_with_0_or_more_than_2_args
370            .get(&(atomic_fact.key(), atomic_fact.is_true()))
371        {
372            for known_fact in known_facts.iter() {
373                if known_fact.args().len() != atomic_fact.args().len() {
374                    let message = format!(
375                        "known atomic fact {} has different number of args than the given fact {}",
376                        known_fact.to_string(),
377                        atomic_fact.to_string()
378                    );
379                    return Err({
380                        VerifyRuntimeError(RuntimeErrorStruct::new(
381                            Some(Fact::from(atomic_fact.clone()).into_stmt()),
382                            message.clone(),
383                            atomic_fact.line_file(),
384                            Some(
385                                UnknownRuntimeError(RuntimeErrorStruct::new(
386                                    Some(Fact::from(atomic_fact.clone()).into_stmt()),
387                                    message,
388                                    atomic_fact.line_file(),
389                                    None,
390                                    vec![],
391                                ))
392                                .into(),
393                            ),
394                            vec![],
395                        ))
396                        .into()
397                    });
398                }
399                let mut all_args_match = true;
400                for (index, known_arg) in known_fact.args().iter().enumerate() {
401                    let known_arg_string = known_arg.to_string();
402                    if !all_objs_equal_to_each_arg[index].contains(&known_arg_string) {
403                        all_args_match = false;
404                        break;
405                    }
406                }
407                if all_args_match {
408                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
409                            atomic_fact.clone().into(),
410                            known_fact.to_string(),
411                            Some(known_fact.clone().into()),
412                            None,
413                            Vec::new(),
414                        )).into());
415                }
416            }
417        }
418
419        Ok((StmtUnknown::new()).into())
420    }
421
422    pub fn verify_fact(
423        &mut self,
424        fact: &Fact,
425        verify_state: &VerifyState,
426    ) -> Result<StmtResult, RuntimeError> {
427        match fact {
428            Fact::AtomicFact(atomic_fact) => self.verify_atomic_fact(atomic_fact, verify_state),
429            Fact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
430            Fact::ChainFact(chain_fact) => self.verify_chain_fact(chain_fact, verify_state),
431            Fact::ForallFact(forall_fact) => self.verify_forall_fact(forall_fact, verify_state),
432            Fact::ForallFactWithIff(forall_iff) => {
433                self.verify_forall_fact_with_iff(forall_iff, verify_state)
434            }
435            Fact::NotForall(not_forall) => self.verify_not_forall_fact(not_forall, verify_state),
436            Fact::ExistFact(exist_fact) => self.verify_exist_fact(exist_fact, verify_state),
437            Fact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
438        }
439    }
440
441    fn verify_subset_fact_by_membership_forall_definition(
442        &mut self,
443        subset_fact: &SubsetFact,
444        verify_state: &VerifyState,
445    ) -> Result<Option<StmtResult>, RuntimeError> {
446        let bound_param_name = self.generate_random_unused_name();
447        let membership_forall_fact = ForallFact::new(
448            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
449                vec![bound_param_name.clone()],
450                ParamType::Obj(subset_fact.left.clone()),
451            )]),
452            vec![],
453            vec![InFact::new(
454                obj_for_bound_param_in_scope(bound_param_name.clone(), ParamObjType::Forall),
455                subset_fact.right.clone(),
456                subset_fact.line_file.clone(),
457            )
458            .into()],
459            subset_fact.line_file.clone(),
460        )?
461        .into();
462        let verify_forall_result = self.verify_fact(&membership_forall_fact, verify_state)?;
463        if !verify_forall_result.is_true() {
464            return Ok(None);
465        }
466        Ok(Some(
467            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
468                subset_fact.clone().into(),
469                "subset by definition (forall x in left: x in right)".to_string(),
470                Vec::new(),
471            ))
472            .into(),
473        ))
474    }
475
476    fn verify_superset_fact_by_membership_forall_definition(
477        &mut self,
478        superset_fact: &SupersetFact,
479        verify_state: &VerifyState,
480    ) -> Result<Option<StmtResult>, RuntimeError> {
481        let bound_param_name = self.generate_random_unused_name();
482        let membership_forall_fact = ForallFact::new(
483            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
484                vec![bound_param_name.clone()],
485                ParamType::Obj(superset_fact.right.clone()),
486            )]),
487            vec![],
488            vec![InFact::new(
489                obj_for_bound_param_in_scope(bound_param_name.clone(), ParamObjType::Forall),
490                superset_fact.left.clone(),
491                superset_fact.line_file.clone(),
492            )
493            .into()],
494            superset_fact.line_file.clone(),
495        )?
496        .into();
497        let verify_forall_result = self.verify_fact(&membership_forall_fact, verify_state)?;
498        if !verify_forall_result.is_true() {
499            return Ok(None);
500        }
501        Ok(Some(
502            (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
503                superset_fact.clone().into(),
504                "superset by definition (forall x in right: x in left)".to_string(),
505                Vec::new(),
506            ))
507            .into(),
508        ))
509    }
510
511    // Built-in subset/superset/restrict_fn_in definitions first, then user `prop` iff-clauses.
512    fn verify_atomic_fact_using_builtin_or_prop_definition(
513        &mut self,
514        atomic_fact: &AtomicFact,
515        verify_state: &VerifyState,
516    ) -> Result<Option<StmtResult>, RuntimeError> {
517        if let Some(result) =
518            self.verify_builtin_fact_with_their_definition(atomic_fact, verify_state)?
519        {
520            return Ok(Some(result));
521        }
522        if let AtomicFact::NormalAtomicFact(n) = atomic_fact {
523            return self.verify_normal_atomic_fact_using_its_definition(n, verify_state);
524        }
525        Ok(None)
526    }
527
528    fn verify_normal_atomic_fact_using_its_definition(
529        &mut self,
530        normal_atomic_fact: &NormalAtomicFact,
531        verify_state: &VerifyState,
532    ) -> Result<Option<StmtResult>, RuntimeError> {
533        if let Some(_) =
534            self.get_abstract_prop_definition_by_name(&normal_atomic_fact.predicate.to_string())
535        {
536            return Ok(None);
537        }
538
539        let predicate_name = normal_atomic_fact.predicate.to_string();
540
541        let definition = match self.get_prop_definition_by_name(&predicate_name) {
542            Some(definition_reference) => definition_reference.clone(),
543            None => {
544                return Err({
545                    VerifyRuntimeError(RuntimeErrorStruct::new(
546                        Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
547                        format!("prop definition not found for {}", predicate_name),
548                        normal_atomic_fact.line_file.clone(),
549                        None,
550                        vec![],
551                    ))
552                    .into()
553                })
554            }
555        };
556
557        let verify_state_for_definition_clauses = verify_state;
558
559        let args_param_types = match self.verify_args_satisfy_param_def_flat_types(
560            &definition.params_def_with_type,
561            &normal_atomic_fact.body,
562            verify_state_for_definition_clauses,
563            ParamObjType::DefHeader,
564        ) {
565            Ok(x) => x,
566            Err(_) => {
567                return Err({
568                    VerifyRuntimeError(RuntimeErrorStruct::new(
569                        Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
570                        format!("failed to verify parameter types for {}", predicate_name),
571                        normal_atomic_fact.line_file.clone(),
572                        None,
573                        vec![],
574                    ))
575                    .into()
576                })
577            }
578        };
579        if args_param_types.is_unknown() {
580            return Ok(None);
581        }
582
583        if definition.iff_facts.is_empty() {
584            return Ok(None);
585        }
586
587        let param_to_arg_map = definition
588            .params_def_with_type
589            .param_defs_and_args_to_param_to_arg_map(normal_atomic_fact.body.as_slice());
590
591        let mut infer_result = InferResult::new();
592        let mut definition_clause_descriptions: Vec<String> = Vec::new();
593
594        for iff_fact in definition.iff_facts.iter() {
595            let instantiated_iff_fact = self
596                .inst_fact(iff_fact, &param_to_arg_map, ParamObjType::DefHeader, None)
597                .map_err(|e| {
598                    {
599                        RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
600                            Some(Fact::from(normal_atomic_fact.clone()).into_stmt()),
601                            String::new(),
602                            normal_atomic_fact.line_file.clone(),
603                            Some(e),
604                            vec![],
605                        )))
606                    }
607                })?;
608            let iff_clause_verify_result =
609                self.verify_fact(&instantiated_iff_fact, &verify_state_for_definition_clauses)?;
610            if iff_clause_verify_result.is_unknown() {
611                return Ok(None);
612            }
613            match &iff_clause_verify_result {
614                StmtResult::FactualStmtSuccess(factual_success) => {
615                    infer_result.new_infer_result_inside(factual_success.infers.clone());
616                    definition_clause_descriptions.push(factual_success.msg.clone());
617                }
618                StmtResult::NonFactualStmtSuccess(non_factual_success) => {
619                    infer_result.new_infer_result_inside(non_factual_success.infers.clone());
620                }
621                StmtResult::StmtUnknown(_) => return Ok(None),
622            }
623        }
624
625        let verified_by_text = format!(
626            "prop with meaning `{}` (param constraints and definition clauses): {}",
627            predicate_name,
628            definition_clause_descriptions.join("; ")
629        );
630        infer_result.new_fact(&normal_atomic_fact.clone().into());
631        Ok(Some(
632            (FactualStmtSuccess::new_with_verified_by_known_fact_source(
633                normal_atomic_fact.clone().into(),
634                infer_result,
635                verified_by_text,
636                None,
637                Some(normal_atomic_fact.line_file.clone()),
638                Vec::new(),
639            ))
640            .into(),
641        ))
642    }
643
644    fn verify_builtin_fact_with_their_definition(
645        &mut self,
646        fact: &AtomicFact,
647        verify_state: &VerifyState,
648    ) -> Result<Option<StmtResult>, RuntimeError> {
649        match fact {
650            AtomicFact::SubsetFact(subset_fact) => {
651                if let Some(verified_by_subset_definition) = self
652                    .verify_subset_fact_by_membership_forall_definition(subset_fact, verify_state)?
653                {
654                    return Ok(Some(verified_by_subset_definition));
655                }
656                return Ok(None);
657            }
658            AtomicFact::SupersetFact(superset_fact) => {
659                if let Some(verified_by_superset_definition) = self
660                    .verify_superset_fact_by_membership_forall_definition(
661                        superset_fact,
662                        verify_state,
663                    )?
664                {
665                    return Ok(Some(verified_by_superset_definition));
666                }
667                return Ok(None);
668            }
669            AtomicFact::RestrictFact(restrict_fact) => {
670                if let Some(verified_by_restrict_definition) =
671                    self.verify_restrict_fact_using_its_definition(restrict_fact, verify_state)?
672                {
673                    return Ok(Some(verified_by_restrict_definition));
674                }
675                return Ok(None);
676            }
677            _ => {}
678        }
679        Ok(None)
680    }
681
682    // If direct verification failed, try the order-dual with swapped operands (e.g. a >= b via b <= a).
683    fn post_process_non_equational_atomic_fact(
684        &mut self,
685        atomic_fact: &AtomicFact,
686        verify_state: &VerifyState,
687        result: StmtResult,
688    ) -> Result<StmtResult, RuntimeError> {
689        let Some(transposed_fact) = atomic_fact.transposed_binary_order_equivalent() else {
690            return Ok(result);
691        };
692        let transposed_result =
693            self.verify_non_equational_atomic_fact(&transposed_fact, verify_state, false)?;
694        match transposed_result {
695            StmtResult::FactualStmtSuccess(inner_success) => Ok(
696                (FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
697                    atomic_fact.clone().into(),
698                    inner_success.msg,
699                    inner_success.verified_by_fact,
700                    inner_success.verified_by_fact_known_line_file,
701                    inner_success.inside_results,
702                ))
703                .into(),
704            ),
705            other if other.is_true() => Ok(other),
706            _ => Ok(result),
707        }
708    }
709}
litex/verify/verify_non_equational_atomic_fact.rs

litex/verify/
verify_non_equational_atomic_fact.rs
