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            return Ok(
113                FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
114                    forall_fact.clone().into(),
115                    forall_infers,
116                    "forall: then-facts by builtin rules".to_string(),
117                    then_verification_results,
118                )
119                .into(),
120            );
121        }
122
123        infer_result.new_fact(&forall_fact.clone().into());
124        let infer_for_success = std::mem::replace(infer_result, InferResult::new());
125        Ok(
126            (FactualStmtSuccess::new_with_verified_by_known_fact_and_infer(
127                forall_fact.clone().into(),
128                infer_for_success,
129                VerifiedByResult::wrap_bys(vec![VerifiedByResult::Fact(
130                    forall_fact.clone().into(),
131                    String::new(),
132                )]),
133                then_verification_results,
134            ))
135            .into(),
136        )
137    }
138
139    /// Declare params, assume dom facts hold, then verify each then_fact.
140    pub fn verify_forall_fact(
141        &mut self,
142        forall_fact: &ForallFact,
143        verify_state: &VerifyState,
144    ) -> Result<StmtResult, RuntimeError> {
145        if let Some(cached_result) =
146            self.verify_fact_from_cache_using_display_string(&forall_fact.clone().into())
147        {
148            return Ok(cached_result);
149        }
150
151        if !verify_state.is_round_0() {
152            return Ok(StmtResult::StmtUnknown(StmtUnknown::new()).into());
153        }
154
155        self.run_in_local_env(|rt| {
156            let mut infer_result =
157                rt.forall_assume_params_and_dom_in_current_env(forall_fact, verify_state)?;
158            rt.forall_verify_then_facts_in_current_env(
159                forall_fact,
160                verify_state,
161                &mut infer_result,
162                None,
163            )
164        })
165    }
166}
litex/verify/verify_forall_fact.rs

litex/verify/
verify_forall_fact.rs
