litex/verify/
verify_exist_fact_with_known_forall.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3use std::rc::Rc;
4use std::result::Result;
5
6// Same ∀-instantiation strategy as `verify_atomic_fact_with_known_forall`, plus exist-internal params.
7
8impl Runtime {
9    pub fn verify_exist_fact_with_known_forall(
10        &mut self,
11        exist_fact: &ExistFactEnum,
12        verify_state: &VerifyState,
13    ) -> Result<StmtResult, RuntimeError> {
14        if let Some(fact_verified) =
15            self.try_verify_exist_fact_with_known_forall_facts_in_envs(exist_fact, verify_state)?
16        {
17            return Ok((fact_verified).into());
18        }
19        Ok((StmtUnknown::new()).into())
20    }
21
22    fn get_matched_exist_fact_in_known_forall_fact_in_envs(
23        &mut self,
24        iterate_from_env_index: usize,
25        iterate_from_known_forall_fact_index: usize,
26        given_exist_fact: &ExistFactEnum,
27    ) -> Result<
28        (
29            (usize, usize),
30            Option<HashMap<String, Obj>>,
31            Option<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>,
32        ),
33        RuntimeError,
34    > {
35        let lookup_keys = known_exist_lookup_keys_for_forall_bucket(given_exist_fact);
36
37        let envs_count = self.environment_stack.len();
38        for i in iterate_from_env_index..envs_count {
39            let env = &self.environment_stack[envs_count - 1 - i];
40            let mut merged_bucket: Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)> =
41                Vec::new();
42            for lk in lookup_keys.iter() {
43                if let Some(known_forall_facts_in_env) =
44                    env.known_exist_facts_in_forall_facts.get(lk.as_str())
45                {
46                    merged_bucket.extend(known_forall_facts_in_env.iter().cloned());
47                }
48            }
49            merged_bucket.sort_by(|a, b| a.0.to_string().cmp(&b.0.to_string()));
50            merged_bucket.dedup_by(|a, b| a.0.to_string() == b.0.to_string());
51            if !merged_bucket.is_empty() {
52                let known_forall_facts_count = merged_bucket.len();
53                for j in iterate_from_known_forall_fact_index..known_forall_facts_count {
54                    let entry_idx = known_forall_facts_count - 1 - j;
55                    let (fact_args_in_known_forall, given_fact_args, current_known_forall) = {
56                        let current_known_forall = &merged_bucket[entry_idx];
57                        (
58                            current_known_forall.0.get_args_from_fact(),
59                            given_exist_fact.get_args_from_fact(),
60                            current_known_forall.clone(),
61                        )
62                    };
63                    let match_result = self
64                        .match_args_in_fact_in_known_forall_fact_with_given_args(
65                            &fact_args_in_known_forall,
66                            &given_fact_args,
67                        )?;
68                    if let Some(arg_map) = match_result {
69                        let exist_in_forall = &current_known_forall.0;
70                        if !exist_in_forall.can_be_used_to_verify_goal(given_exist_fact) {
71                            continue;
72                        }
73                        return Ok(((i, j), Some(arg_map), Some(current_known_forall)));
74                    }
75                }
76            }
77        }
78
79        Ok(((0, 0), None, None))
80    }
81
82    fn try_verify_exist_fact_with_known_forall_facts_in_envs(
83        &mut self,
84        exist_fact: &ExistFactEnum,
85        verify_state: &VerifyState,
86    ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
87        let mut iterate_from_env_index = 0;
88        let mut iterate_from_known_forall_fact_index = 0;
89
90        loop {
91            let result = self.get_matched_exist_fact_in_known_forall_fact_in_envs(
92                iterate_from_env_index,
93                iterate_from_known_forall_fact_index,
94                exist_fact,
95            )?;
96            let ((i, j), arg_map_opt, known_forall_opt) = result;
97            match (arg_map_opt, known_forall_opt) {
98                (Some(arg_map), Some((exist_fact_in_known_forall, forall_rc))) => {
99                    if let Some(fact_verified) = self
100                        .verify_exist_fact_args_satisfy_forall_requirements(
101                            &exist_fact_in_known_forall,
102                            &forall_rc,
103                            arg_map,
104                            exist_fact,
105                            verify_state,
106                        )?
107                    {
108                        return Ok(Some(fact_verified));
109                    }
110                    iterate_from_env_index = i;
111                    iterate_from_known_forall_fact_index = j + 1;
112                }
113                _ => return Ok(None),
114            }
115        }
116    }
117
118    fn verify_exist_fact_args_satisfy_forall_requirements(
119        &mut self,
120        exist_fact_in_known_forall: &ExistFactEnum,
121        known_forall: &Rc<KnownForallFactParamsAndDom>,
122        arg_map: HashMap<String, Obj>,
123        given_exist_fact: &ExistFactEnum,
124        verify_state: &VerifyState,
125    ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
126        if !exist_fact_in_known_forall.can_be_used_to_verify_goal(given_exist_fact) {
127            return Ok(None);
128        }
129        // exist param matches exist param
130        let given_exist_param_names = given_exist_fact
131            .params_def_with_type()
132            .collect_param_names();
133
134        let known_exist_param_names = exist_fact_in_known_forall
135            .params_def_with_type()
136            .collect_param_names();
137        if !known_exist_param_names
138            .iter()
139            .all(|param_name| arg_map.contains_key(param_name))
140        {
141            return Ok(None);
142        }
143
144        if given_exist_param_names.len() != known_exist_param_names.len() {
145            return Ok(None);
146        }
147
148        let mut known_exist_params_to_given_exist_params_map: Vec<Obj> = Vec::new();
149        for (known_param_name, given_param_name) in known_exist_param_names
150            .iter()
151            .zip(given_exist_param_names.iter())
152        {
153            let obj = match arg_map.get(known_param_name) {
154                Some(v) => {
155                    if !Self::obj_matches_exist_forall_binding_name(v, given_param_name) {
156                        return Ok(None);
157                    }
158                    v
159                }
160                None => return Ok(None),
161            };
162            known_exist_params_to_given_exist_params_map.push(obj.clone());
163        }
164
165        // given exist param can only match known exist param, it can not match other params
166        for (key, obj) in arg_map.iter() {
167            if let Some(spine) = Self::obj_binding_spine_name_for_arg_map(obj) {
168                if given_exist_param_names.iter().any(|n| n == spine) {
169                    if !known_exist_param_names.contains(key) {
170                        return Ok(None);
171                    }
172                }
173            }
174        }
175
176        // arg that matches forall params
177        let param_names = known_forall.params_def.collect_param_names();
178
179        if !param_names
180            .iter()
181            .all(|param_name| arg_map.contains_key(param_name))
182        {
183            return Ok(None);
184        }
185
186        let mut args_for_params: Vec<Obj> = Vec::new();
187
188        for param_name in param_names.iter() {
189            let obj = match arg_map.get(param_name) {
190                Some(v) => v,
191                None => return Ok(None),
192            };
193
194            args_for_params.push(obj.clone());
195        }
196
197        let args_param_types = self
198            .verify_args_satisfy_param_def_flat_types(
199                &known_forall.params_def,
200                &args_for_params,
201                verify_state,
202                ParamObjType::Forall,
203            )
204            .map_err(|e| {
205                {
206                    RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
207                        Some(Fact::from(given_exist_fact.clone()).into_stmt()),
208                        String::new(),
209                        given_exist_fact.line_file(),
210                        Some(e),
211                        vec![],
212                    )))
213                }
214            })?;
215        if args_param_types.is_unknown() {
216            return Ok(None);
217        }
218
219        let param_to_arg_map = match known_forall
220            .params_def
221            .param_def_params_to_arg_map(&arg_map)
222        {
223            Some(m) => m,
224            None => return Ok(None),
225        };
226
227        for dom_fact in known_forall.dom.iter() {
228            let instantiated_dom_fact = self
229                .inst_fact(dom_fact, &param_to_arg_map, ParamObjType::Forall, None)
230                .map_err(|e| {
231                    {
232                        RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
233                            Some(Fact::from(given_exist_fact.clone()).into_stmt()),
234                            String::new(),
235                            given_exist_fact.line_file(),
236                            Some(e),
237                            vec![],
238                        )))
239                    }
240                })?;
241            let result = self
242                .verify_fact(&instantiated_dom_fact, verify_state)
243                .map_err(|e| {
244                    {
245                        RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
246                            Some(Fact::from(given_exist_fact.clone()).into_stmt()),
247                            String::new(),
248                            given_exist_fact.line_file(),
249                            Some(e),
250                            vec![],
251                        )))
252                    }
253                })?;
254            if result.is_unknown() {
255                return Ok(None);
256            }
257        }
258
259        let verified_by_known_forall_fact = ForallFact::new(
260            known_forall.params_def.clone(),
261            known_forall.dom.clone(),
262            vec![exist_fact_in_known_forall.clone().into()],
263            known_forall.line_file.clone(),
264        )?;
265        let fact_verified = FactualStmtSuccess::new_with_verified_by_known_fact(
266            given_exist_fact.clone().into(),
267            VerifiedByResult::Fact(
268                verified_by_known_forall_fact.clone().into(),
269                verified_by_known_forall_fact.to_string(),
270            ),
271            Vec::new(),
272        );
273        Ok(Some(fact_verified))
274    }
275
276    fn obj_binding_spine_name_for_arg_map(obj: &Obj) -> Option<&str> {
277        match obj {
278            Obj::Atom(AtomObj::Exist(p)) => Some(p.name.as_str()),
279            Obj::Atom(AtomObj::Forall(p)) => Some(p.name.as_str()),
280            Obj::Atom(AtomObj::FnSet(p)) => Some(p.name.as_str()),
281            Obj::Atom(AtomObj::Def(p)) => Some(p.name.as_str()),
282            Obj::Atom(AtomObj::SetBuilder(p)) => Some(p.name.as_str()),
283            Obj::Atom(AtomObj::Induc(p)) => Some(p.name.as_str()),
284            Obj::Atom(AtomObj::DefAlgo(p)) => Some(p.name.as_str()),
285            _ => None,
286        }
287    }
288
289    fn obj_matches_exist_forall_binding_name(obj: &Obj, name: &str) -> bool {
290        match obj {
291            Obj::Atom(AtomObj::Exist(p)) => p.name == name,
292            Obj::Atom(AtomObj::Forall(p)) => p.name == name,
293            Obj::Atom(AtomObj::FnSet(p)) => p.name == name,
294            Obj::Atom(AtomObj::Def(p)) => p.name == name,
295            Obj::Atom(AtomObj::SetBuilder(p)) => p.name == name,
296            Obj::Atom(AtomObj::Induc(p)) => p.name == name,
297            Obj::Atom(AtomObj::DefAlgo(p)) => p.name == name,
298            _ => obj.to_string() == name,
299        }
300    }
301}
302
303fn known_exist_lookup_keys_for_forall_bucket(goal: &ExistFactEnum) -> Vec<String> {
304    let mut keys = vec![goal.alpha_normalized_key(), goal.key()];
305    if let ExistFactEnum::ExistFact(body) = goal {
306        let unique = ExistFactEnum::ExistUniqueFact(body.clone());
307        keys.push(unique.alpha_normalized_key());
308        keys.push(unique.key());
309    }
310    keys.sort();
311    keys.dedup();
312    keys
313}
litex/verify/verify_exist_fact_with_known_forall.rs

litex/verify/
verify_exist_fact_with_known_forall.rs
