litex/verify/
verify_forall_fact.rs

1use crate::prelude::*;
2use std::result::Result;
3
4impl Runtime {
5    /// Assume `forall` parameters and dom facts in the current environment (no extra `push_env`).
6    /// Used by [`Self::verify_forall_fact`] and by `by cases` in the same `run_in_local_env` as the
7    /// case branch.
8    pub(crate) fn forall_assume_params_and_dom_in_current_env(
9        &mut self,
10        forall_fact: &ForallFact,
11        verify_state: &VerifyState,
12    ) -> Result<InferResult, RuntimeError> {
13        if let Err(e) = self.define_params_with_type(
14            &forall_fact.params_def_with_type,
15            false,
16            ParamObjType::Forall,
17        ) {
18            return Err(WellDefinedRuntimeError(RuntimeErrorStruct::new(
19                None,
20                "failed to define parameters in forall fact".to_string(),
21                forall_fact.line_file.clone(),
22                Some(e),
23                vec![],
24            ))
25            .into());
26        }
27
28        for dom_fact in forall_fact.dom_facts.iter() {
29            self.verify_well_defined_and_store_and_infer(dom_fact.clone(), verify_state)
30                .map_err(|e| {
31                    let message = "failed to assume dom fact in forall".to_string();
32                    RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
33                        Some(Fact::from(forall_fact.clone()).into_stmt()),
34                        message.clone(),
35                        forall_fact.line_file.clone(),
36                        Some(RuntimeError::from(UnknownRuntimeError(
37                            RuntimeErrorStruct::new(
38                                Some(Fact::from(forall_fact.clone()).into_stmt()),
39                                message,
40                                forall_fact.line_file.clone(),
41                                Some(e),
42                                vec![],
43                            ),
44                        ))),
45                        vec![],
46                    )))
47                })?;
48        }
49        Ok(InferResult::new())
50    }
51
52    /// Verify and store each `then` clause of `forall_fact` in the current environment.
53    /// `by_cases_case_label`: when set, unknown `then` messages include the active `by cases` case.
54    pub(crate) fn forall_verify_then_facts_in_current_env(
55        &mut self,
56        forall_fact: &ForallFact,
57        verify_state: &VerifyState,
58        infer_result: &mut InferResult,
59        by_cases_case_label: Option<&str>,
60    ) -> Result<StmtResult, RuntimeError> {
61        let mut all_then_facts_are_verified_by_builtin_rules = true;
62        let mut then_verification_results: Vec<StmtResult> = Vec::new();
63
64        let then_count = forall_fact.then_facts.len();
65        for (then_index, then_fact) in forall_fact.then_facts.iter().enumerate() {
66            let result = self.verify_exist_or_and_chain_atomic_fact(then_fact, verify_state)?;
67            if result.is_unknown() {
68                let then_one_based = then_index + 1;
69                let detail = match by_cases_case_label {
70                    None => format!(
71                        "forall: then-fact {}/{} could not be verified (unknown): `{}`\n{}",
72                        then_one_based,
73                        then_count,
74                        then_fact,
75                        result.body_string()
76                    ),
77                    Some(case_s) => format!(
78                        "by cases: under case `{case_s}`: forall: then-fact {then_one_based}/{then_count} could not be verified (unknown): `{then}`\n{body}",
79                        case_s = case_s,
80                        then_one_based = then_one_based,
81                        then_count = then_count,
82                        then = then_fact,
83                        body = result.body_string()
84                    ),
85                };
86                return Ok(StmtUnknown::new_with_detail(detail).into());
87            }
88
89            self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
90                then_fact.clone(),
91            )?;
92
93            match &result {
94                StmtResult::FactualStmtSuccess(factual_verification_result) => {
95                    if !factual_verification_result.is_verified_by_builtin_rules_only() {
96                        all_then_facts_are_verified_by_builtin_rules = false;
97                    }
98                    // Do not merge then-fact verification `infers` into `infer_result` (e.g. instantiated
99                    // `min(a,b) <= a` from a known forall). Each then proof is listed in
100                    // `FactualStmtSuccess::inside_results` for JSON/CLI.
101                }
102                StmtResult::NonFactualStmtSuccess(non_factual_success) => {
103                    all_then_facts_are_verified_by_builtin_rules = false;
104                    infer_result.new_infer_result_inside(non_factual_success.infers.clone());
105                }
106                StmtResult::StmtUnknown(_) => {
107                    unreachable!("stmt unknown is handled above before this match")
108                }
109            }
110            then_verification_results.push(result);
111        }
112
113        if all_then_facts_are_verified_by_builtin_rules && !forall_fact.then_facts.is_empty() {
114            let forall_infers = InferResult::from_fact(&forall_fact.clone().into());
115            return Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules(
116                forall_fact.clone().into(),
117                forall_infers,
118                "forall: then-facts by builtin rules".to_string(),
119                then_verification_results,
120            ))
121            .into());
122        }
123
124        infer_result.new_fact(&forall_fact.clone().into());
125        let infer_for_success = std::mem::replace(infer_result, InferResult::new());
126        Ok((FactualStmtSuccess::new_with_verified_by_known_fact_source(
127            forall_fact.clone().into(),
128            infer_for_success,
129            "".to_string(),
130            None,
131            Some(forall_fact.line_file.clone()),
132            then_verification_results,
133        ))
134        .into())
135    }
136
137    /// Declare params, assume dom facts hold, then verify each then_fact.
138    pub fn verify_forall_fact(
139        &mut self,
140        forall_fact: &ForallFact,
141        verify_state: &VerifyState,
142    ) -> Result<StmtResult, RuntimeError> {
143        if let Some(cached_result) =
144            self.verify_fact_from_cache_using_display_string(&forall_fact.clone().into())
145        {
146            return Ok(cached_result);
147        }
148
149        if !verify_state.is_round_0() {
150            return Ok(StmtResult::StmtUnknown(StmtUnknown::new()).into());
151        }
152
153        self.run_in_local_env(|rt| {
154            let mut infer_result =
155                rt.forall_assume_params_and_dom_in_current_env(forall_fact, verify_state)?;
156            rt.forall_verify_then_facts_in_current_env(
157                forall_fact,
158                verify_state,
159                &mut infer_result,
160                None,
161            )
162        })
163    }
164}
litex/verify/verify_forall_fact.rs

litex/verify/
verify_forall_fact.rs
