litex/verify/
verify_forall_fact_with_iff.rs

1use crate::prelude::*;
2use std::result::Result;
3
4impl Runtime {
5    pub fn verify_forall_fact_with_iff(
6        &mut self,
7        forall_iff: &ForallFactWithIff,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        if let Some(cached_result) =
11            self.verify_fact_from_cache_using_display_string(&forall_iff.clone().into())
12        {
13            return Ok(cached_result);
14        }
15
16        let (forall_then_implies_iff, forall_iff_implies_then) =
17            forall_iff.to_two_forall_facts()?;
18        let verification_steps = [&forall_then_implies_iff, &forall_iff_implies_then];
19        for forall_step in verification_steps {
20            let result = self.verify_forall_fact(forall_step, verify_state)?;
21            if result.is_unknown() {
22                return Ok(result);
23            }
24        }
25
26        Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
27            forall_iff.clone().into(),
28            VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::fact_with_note(
29                forall_iff.clone().into(),
30                Some("forall iff: then=>iff and iff=>then verified".to_string()),
31            )]),
32            Vec::new(),
33        ))
34        .into())
35    }
36}
litex/verify/verify_forall_fact_with_iff.rs

litex/verify/
verify_forall_fact_with_iff.rs
