litex/verify/
verify_and_chain_fact.rs

1use crate::prelude::*;
2use std::result::Result;
3
4impl Runtime {
5    pub fn verify_and_fact(
6        &mut self,
7        and_fact: &AndFact,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        if let Some(cached_result) =
11            self.verify_fact_from_cache_using_display_string(&and_fact.clone().into())
12        {
13            return Ok(cached_result);
14        }
15
16        if !verify_state.well_defined_already_verified {
17            if let Err(e) = self.verify_and_fact_well_defined(and_fact, verify_state) {
18                return Err(RuntimeError::from(VerifyRuntimeError(
19                    RuntimeErrorStruct::new(
20                        Some(Fact::from(and_fact.clone()).into_stmt()),
21                        String::new(),
22                        and_fact.line_file(),
23                        Some(e),
24                        vec![],
25                    ),
26                )));
27            }
28        }
29
30        let verify_state_for_children = verify_state.make_state_with_req_ok_set_to_true();
31
32        let mut child_results: Vec<StmtResult> = Vec::with_capacity(and_fact.facts.len());
33        for fact in &and_fact.facts {
34            let result = self.verify_atomic_fact(fact, &verify_state_for_children)?;
35            if result.is_unknown() {
36                return Ok(result);
37            }
38            child_results.push(result);
39        }
40        Ok(
41            (FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
42                and_fact.clone().into(),
43                "and: each conjunct verified in order".to_string(),
44                None,
45                Some(and_fact.line_file()),
46                child_results,
47            ))
48            .into(),
49        )
50    }
51
52    pub fn verify_chain_fact(
53        &mut self,
54        chain_fact: &ChainFact,
55        verify_state: &VerifyState,
56    ) -> Result<StmtResult, RuntimeError> {
57        if let Some(cached_result) =
58            self.verify_fact_from_cache_using_display_string(&chain_fact.clone().into())
59        {
60            return Ok(cached_result);
61        }
62
63        if !verify_state.well_defined_already_verified {
64            if let Err(e) = self.verify_chain_fact_well_defined(chain_fact, verify_state) {
65                return Err(RuntimeError::from(VerifyRuntimeError(
66                    RuntimeErrorStruct::new(
67                        Some(Fact::from(chain_fact.clone()).into_stmt()),
68                        String::new(),
69                        chain_fact.line_file(),
70                        Some(e),
71                        vec![],
72                    ),
73                )));
74            }
75        }
76
77        let verify_state_for_children = verify_state.make_state_with_req_ok_set_to_true();
78
79        let facts = chain_fact.facts().map_err(|e| {
80            RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
81                Some(Fact::ChainFact(chain_fact.clone()).into_stmt()),
82                String::new(),
83                chain_fact.line_file(),
84                Some(e),
85                vec![],
86            )))
87        })?;
88        let mut child_results: Vec<StmtResult> = Vec::with_capacity(facts.len());
89        for fact in &facts {
90            let result = self.verify_atomic_fact(fact, &verify_state_for_children)?;
91            if result.is_unknown() {
92                return Ok((StmtUnknown::new_with_detail(format!(
93                    "unverified chain step: {}",
94                    fact
95                )))
96                .into());
97            }
98
99            child_results.push(result);
100        }
101        Ok(
102            (FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
103                chain_fact.clone().into(),
104                "chain: each step verified in order".to_string(),
105                None,
106                Some(chain_fact.line_file()),
107                child_results,
108            ))
109            .into(),
110        )
111    }
112}
litex/verify/verify_and_chain_fact.rs

litex/verify/
verify_and_chain_fact.rs
