litex/verify/
verify_non_equational_atomic_fact.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_non_equational_atomic_fact(
5        &mut self,
6        atomic_fact: &AtomicFact,
7        verify_state: &VerifyState,
8        post_process: bool,
9    ) -> Result<StmtResult, RuntimeError> {
10        let mut result =
11            self.verify_non_equational_atomic_fact_with_builtin_rules(atomic_fact, verify_state)?;
12        if result.is_true() {
13            return Ok(result);
14        }
15
16        result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(atomic_fact)?;
17        if result.is_true() {
18            return Ok(result);
19        }
20
21        if verify_state.is_round_0() {
22            let verify_state_add_one_round = verify_state.new_state_with_round_increased();
23
24            if let Some(verified_by_definition) =
25                self.verify_atomic_fact_using_builtin_or_prop_definition(atomic_fact, verify_state)?
26            {
27                return Ok(verified_by_definition);
28            }
29
30            result = self
31                .verify_atomic_fact_with_known_forall(atomic_fact, &verify_state_add_one_round)?;
32            if result.is_true() {
33                return Ok(result);
34            }
35        }
36
37        if post_process {
38            result =
39                self.post_process_non_equational_atomic_fact(atomic_fact, verify_state, result)?;
40            if result.is_true() {
41                return Ok(result);
42            }
43        }
44
45        Ok((StmtUnknown::new()).into())
46    }
47
48    pub fn verify_fact(
49        &mut self,
50        fact: &Fact,
51        verify_state: &VerifyState,
52    ) -> Result<StmtResult, RuntimeError> {
53        match fact {
54            Fact::AtomicFact(atomic_fact) => self.verify_atomic_fact(atomic_fact, verify_state),
55            Fact::AndFact(and_fact) => self.verify_and_fact(and_fact, verify_state),
56            Fact::ChainFact(chain_fact) => self.verify_chain_fact(chain_fact, verify_state),
57            Fact::ForallFact(forall_fact) => self.verify_forall_fact(forall_fact, verify_state),
58            Fact::ForallFactWithIff(forall_iff) => {
59                self.verify_forall_fact_with_iff(forall_iff, verify_state)
60            }
61            Fact::NotForall(not_forall) => self.verify_not_forall_fact(not_forall, verify_state),
62            Fact::ExistFact(exist_fact) => self.verify_exist_fact(exist_fact, verify_state),
63            Fact::OrFact(or_fact) => self.verify_or_fact(or_fact, verify_state),
64        }
65    }
66
67    // If direct verification failed, try the order-dual (e.g. a >= b via b <= a), then commutative props.
68    fn post_process_non_equational_atomic_fact(
69        &mut self,
70        atomic_fact: &AtomicFact,
71        verify_state: &VerifyState,
72        result: StmtResult,
73    ) -> Result<StmtResult, RuntimeError> {
74        let result = self.builtin_post_process_non_equational_atomic_fact(
75            atomic_fact,
76            verify_state,
77            result,
78        )?;
79        if result.is_true() {
80            return Ok(result);
81        }
82        self.use_known_commutative_prop(atomic_fact, verify_state, result)
83    }
84
85    fn builtin_post_process_non_equational_atomic_fact(
86        &mut self,
87        atomic_fact: &AtomicFact,
88        verify_state: &VerifyState,
89        result: StmtResult,
90    ) -> Result<StmtResult, RuntimeError> {
91        let Some(transposed_fact) = atomic_fact.transposed_binary_order_equivalent() else {
92            return Ok(result);
93        };
94        let transposed_result =
95            self.verify_non_equational_atomic_fact(&transposed_fact, verify_state, false)?;
96        Self::wrap_post_process_alternate_fact_result(atomic_fact, transposed_result, result)
97    }
98
99    fn use_known_commutative_prop(
100        &mut self,
101        atomic_fact: &AtomicFact,
102        verify_state: &VerifyState,
103        result: StmtResult,
104    ) -> Result<StmtResult, RuntimeError> {
105        let AtomicFact::NormalAtomicFact(f) = atomic_fact else {
106            return Ok(result);
107        };
108        if f.body.len() < 2 {
109            return Ok(result);
110        }
111        let prop_name = f.predicate.to_string();
112
113        let mut permutations: Vec<Vec<usize>> = Vec::new();
114        for env in self.iter_environments_from_top() {
115            if let Some(perms) = env.known_commutative_props.get(&prop_name) {
116                for g in perms {
117                    if g.len() == f.body.len() {
118                        permutations.push(g.clone());
119                    }
120                }
121            }
122        }
123
124        for gather in permutations {
125            let Some(alt) = atomic_fact.commutative_reordered_args(&gather) else {
126                continue;
127            };
128            let alt_result = self.verify_non_equational_atomic_fact(&alt, verify_state, false)?;
129            if alt_result.is_true() {
130                return Self::wrap_post_process_alternate_fact_result(
131                    atomic_fact,
132                    alt_result,
133                    result,
134                );
135            }
136        }
137
138        Ok(result)
139    }
140
141    fn wrap_post_process_alternate_fact_result(
142        original: &AtomicFact,
143        alternate_result: StmtResult,
144        fallback: StmtResult,
145    ) -> Result<StmtResult, RuntimeError> {
146        match alternate_result {
147            StmtResult::FactualStmtSuccess(inner_success) => {
148                let FactualStmtSuccess {
149                    verified_by,
150                    infers: _,
151                    stmt: _,
152                } = inner_success;
153                Ok(FactualStmtSuccess::new_with_verified_by_known_fact(
154                    original.clone().into(),
155                    verified_by,
156                    Vec::new(),
157                )
158                .into())
159            }
160            other if other.is_true() => Ok(other),
161            _ => Ok(fallback),
162        }
163    }
164}
litex/verify/verify_non_equational_atomic_fact.rs

litex/verify/
verify_non_equational_atomic_fact.rs
