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((FactualStmtSuccess::new_with_verified_by_known_fact(
41            and_fact.clone().into(),
42            VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::fact_with_note(
43                and_fact.clone().into(),
44                Some("and: each conjunct verified in order".to_string()),
45            )]),
46            child_results,
47        ))
48        .into())
49    }
50
51    pub fn verify_chain_fact(
52        &mut self,
53        chain_fact: &ChainFact,
54        verify_state: &VerifyState,
55    ) -> Result<StmtResult, RuntimeError> {
56        if let Some(cached_result) =
57            self.verify_fact_from_cache_using_display_string(&chain_fact.clone().into())
58        {
59            return Ok(cached_result);
60        }
61
62        if !verify_state.well_defined_already_verified {
63            if let Err(e) = self.verify_chain_fact_well_defined(chain_fact, verify_state) {
64                return Err(RuntimeError::from(VerifyRuntimeError(
65                    RuntimeErrorStruct::new(
66                        Some(Fact::from(chain_fact.clone()).into_stmt()),
67                        String::new(),
68                        chain_fact.line_file(),
69                        Some(e),
70                        vec![],
71                    ),
72                )));
73            }
74        }
75
76        let verify_state_for_children = verify_state.make_state_with_req_ok_set_to_true();
77
78        let facts = chain_fact.facts().map_err(|e| {
79            RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
80                Some(Fact::ChainFact(chain_fact.clone()).into_stmt()),
81                String::new(),
82                chain_fact.line_file(),
83                Some(e),
84                vec![],
85            )))
86        })?;
87        let mut child_results: Vec<StmtResult> = Vec::with_capacity(facts.len());
88        for fact in &facts {
89            let result = self.verify_atomic_fact(fact, &verify_state_for_children)?;
90            if result.is_unknown() {
91                return Ok((StmtUnknown::new_with_detail(format!(
92                    "unverified chain step: {}",
93                    fact
94                )))
95                .into());
96            }
97
98            child_results.push(result);
99        }
100        Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
101            chain_fact.clone().into(),
102            VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::fact_with_note(
103                chain_fact.clone().into(),
104                Some("chain: each step verified in order".to_string()),
105            )]),
106            child_results,
107        ))
108        .into())
109    }
110}
litex/verify/verify_and_chain_fact.rs

litex/verify/
verify_and_chain_fact.rs
