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_header = match by_cases_case_label {
70                    None => format!(
71                        "forall: then-fact {}/{} could not be verified (unknown): `{}`",
72                        then_one_based, then_count, then_fact
73                    ),
74                    Some(case_s) => format!(
75                        "by cases: under case `{case_s}`: forall: then-fact {then_one_based}/{then_count} could not be verified (unknown): `{then}`",
76                        case_s = case_s,
77                        then_one_based = then_one_based,
78                        then_count = then_count,
79                        then = then_fact
80                    ),
81                };
82                let detail_lines = vec![detail_header, result.body_string()];
83                return Ok(StmtUnknown::new_with_detail_lines(detail_lines).into());
84            }
85
86            self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
87                then_fact.clone(),
88            )?;
89
90            match &result {
91                StmtResult::FactualStmtSuccess(factual_verification_result) => {
92                    if !factual_verification_result.is_verified_by_builtin_rules_only() {
93                        all_then_facts_are_verified_by_builtin_rules = false;
94                    }
95                    // Do not merge then-fact verification `infers` into `infer_result` (e.g. instantiated
96                    // `min(a,b) <= a` from a known forall). Each then proof is attached as Steps under
97                    // `verified_by` for JSON/CLI.
98                }
99                StmtResult::NonFactualStmtSuccess(non_factual_success) => {
100                    all_then_facts_are_verified_by_builtin_rules = false;
101                    infer_result.new_infer_result_inside(non_factual_success.infers.clone());
102                }
103                StmtResult::StmtUnknown(_) => {
104                    unreachable!("stmt unknown is handled above before this match")
105                }
106            }
107            then_verification_results.push(result);
108        }
109
110        if all_then_facts_are_verified_by_builtin_rules && !forall_fact.then_facts.is_empty() {
111            let forall_infers = InferResult::from_fact(&forall_fact.clone().into());
112            let cite_items: Vec<VerifiedBysEnum> = then_verification_results
113                .into_iter()
114                .flat_map(crate::result::verified_by_items_from_stmt_result)
115                .collect();
116            let verified_by = VerifiedByResult::wrap_bys(cite_items);
117            return Ok(FactualStmtSuccess::new_with_verified_by_builtin_rules(
118                forall_fact.clone().into(),
119                forall_infers,
120                verified_by,
121            )
122            .into());
123        }
124
125        infer_result.new_fact(&forall_fact.clone().into());
126        let infer_for_success = std::mem::replace(infer_result, InferResult::new());
127        Ok(
128            (FactualStmtSuccess::new_with_verified_by_known_fact_and_infer(
129                forall_fact.clone().into(),
130                infer_for_success,
131                VerifiedByResult::wrap_bys(Vec::new()),
132                then_verification_results,
133            ))
134            .into(),
135        )
136    }
137
138    /// Declare params, assume dom facts hold, then verify each then_fact.
139    pub fn verify_forall_fact(
140        &mut self,
141        forall_fact: &ForallFact,
142        verify_state: &VerifyState,
143    ) -> Result<StmtResult, RuntimeError> {
144        if let Some(cached_result) =
145            self.verify_fact_from_cache_using_display_string(&forall_fact.clone().into())
146        {
147            return Ok(cached_result);
148        }
149
150        if !verify_state.is_round_0() {
151            return Ok(StmtResult::StmtUnknown(StmtUnknown::new()).into());
152        }
153
154        self.run_in_local_env(|rt| {
155            let mut infer_result =
156                rt.forall_assume_params_and_dom_in_current_env(forall_fact, verify_state)?;
157            rt.forall_verify_then_facts_in_current_env(
158                forall_fact,
159                verify_state,
160                &mut infer_result,
161                None,
162            )
163        })
164    }
165}
litex/verify/verify_forall_fact.rs

litex/verify/
verify_forall_fact.rs
