litex/verify/
verify_exist_fact.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3use std::result::Result;
4
5impl Runtime {
6    pub fn verify_exist_fact(
7        &mut self,
8        exist_fact: &ExistFactEnum,
9        verify_state: &VerifyState,
10    ) -> Result<StmtResult, RuntimeError> {
11        if let Some(cached_result) =
12            self.verify_fact_from_cache_using_display_string(&exist_fact.clone().into())
13        {
14            return Ok(cached_result);
15        }
16
17        if !verify_state.well_defined_already_verified {
18            if let Err(e) = self.verify_exist_fact_well_defined(exist_fact, verify_state) {
19                return Err({
20                    VerifyRuntimeError(RuntimeErrorStruct::new(
21                        Some(Fact::from(exist_fact.clone()).into_stmt()),
22                        String::new(),
23                        exist_fact.line_file(),
24                        Some(e),
25                        vec![],
26                    ))
27                    .into()
28                });
29            }
30        }
31
32        let result = self.verify_exist_fact_with_known_exist_fact(exist_fact, exist_fact)?;
33        if result.is_true() {
34            return Ok(result);
35        }
36
37        if verify_state.is_round_0() {
38            let result = self.verify_exist_fact_with_known_forall(exist_fact, verify_state)?;
39            if result.is_true() {
40                return Ok(result);
41            }
42
43            if exist_fact.is_exist_unique() {
44                if let Some(proved) = self.try_verify_exist_unique_by_exist_and_uniqueness_forall(
45                    exist_fact,
46                    verify_state,
47                )? {
48                    return Ok(proved);
49                }
50            }
51        }
52
53        Ok((StmtUnknown::new()).into())
54    }
55
56    pub(crate) fn build_exist_unique_uniqueness_forall_fact(
57        &self,
58        exist_fact: &ExistFactEnum,
59    ) -> Result<ForallFact, RuntimeError> {
60        let lf = exist_fact.line_file();
61        let flat_orig = exist_fact.params_def_with_type().collect_param_names();
62        let n = flat_orig.len();
63        let flat_a: Vec<String> = flat_orig.iter().map(|name| format!("{}1", name)).collect();
64        let flat_b: Vec<String> = flat_orig.iter().map(|name| format!("{}2", name)).collect();
65
66        let mut map_running_a: HashMap<String, Obj> = HashMap::new();
67        let mut map_running_b: HashMap<String, Obj> = HashMap::new();
68        let mut forall_groups: Vec<ParamGroupWithParamType> = Vec::new();
69        for group in exist_fact.params_def_with_type().groups.iter() {
70            let chunk_a: Vec<String> = group
71                .params
72                .iter()
73                .map(|name| format!("{}1", name))
74                .collect();
75            for (orig, nm) in group.params.iter().zip(chunk_a.iter()) {
76                map_running_a.insert(
77                    orig.clone(),
78                    obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
79                );
80            }
81            let pt_a =
82                self.inst_param_type(&group.param_type, &map_running_a, ParamObjType::Forall)?;
83            forall_groups.push(ParamGroupWithParamType::new(chunk_a, pt_a));
84        }
85        for group in exist_fact.params_def_with_type().groups.iter() {
86            let chunk_b: Vec<String> = group
87                .params
88                .iter()
89                .map(|name| format!("{}2", name))
90                .collect();
91            for (orig, nm) in group.params.iter().zip(chunk_b.iter()) {
92                map_running_b.insert(
93                    orig.clone(),
94                    obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
95                );
96            }
97            let pt_b =
98                self.inst_param_type(&group.param_type, &map_running_b, ParamObjType::Forall)?;
99            forall_groups.push(ParamGroupWithParamType::new(chunk_b, pt_b));
100        }
101
102        let map_a: HashMap<String, Obj> = flat_orig
103            .iter()
104            .cloned()
105            .zip(
106                flat_a
107                    .iter()
108                    .cloned()
109                    .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
110            )
111            .collect();
112        let map_b: HashMap<String, Obj> = flat_orig
113            .iter()
114            .cloned()
115            .zip(
116                flat_b
117                    .iter()
118                    .cloned()
119                    .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
120            )
121            .collect();
122
123        // Witness parameters in `exist_fact.facts` are [`ExistFreeParamObj`]; only `inst_*` with
124        // [`ParamObjType::Exist`] substitutes them from `map_a` / `map_b` into the forall copies.
125        let mut dom_facts: Vec<Fact> = Vec::new();
126        for inner in exist_fact.facts().iter() {
127            let f_a = self.inst_exist_body_fact(inner, &map_a, ParamObjType::Exist, None)?;
128            dom_facts.push(f_a.to_fact());
129        }
130        for inner in exist_fact.facts().iter() {
131            let f_b = self.inst_exist_body_fact(inner, &map_b, ParamObjType::Exist, None)?;
132            dom_facts.push(f_b.to_fact());
133        }
134
135        let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
136        if n == 1 {
137            let eq = EqualFact::new(
138                obj_for_bound_param_in_scope(flat_a[0].clone(), ParamObjType::Forall),
139                obj_for_bound_param_in_scope(flat_b[0].clone(), ParamObjType::Forall),
140                lf.clone(),
141            );
142            then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
143        } else {
144            let left_tuple: Obj = Tuple::new(
145                flat_a
146                    .iter()
147                    .cloned()
148                    .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
149                    .collect::<Vec<Obj>>(),
150            )
151            .into();
152            let right_tuple: Obj = Tuple::new(
153                flat_b
154                    .iter()
155                    .cloned()
156                    .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
157                    .collect::<Vec<Obj>>(),
158            )
159            .into();
160            let eq = EqualFact::new(left_tuple, right_tuple, lf.clone());
161            then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
162        }
163
164        let forall_fact = ForallFact::new(
165            ParamDefWithType::new(forall_groups),
166            dom_facts,
167            then_facts,
168            lf,
169        )?;
170
171        let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
172        for group in forall_fact.params_def_with_type.groups.iter() {
173            for param in group.params.iter() {
174                param_to_arg_map
175                    .insert(param.clone(), ForallFreeParamObj::new(param.clone()).into());
176            }
177        }
178
179        let forall_fact = self.inst_fact(
180            &forall_fact.into(),
181            &param_to_arg_map,
182            ParamObjType::Forall,
183            None,
184        )?;
185
186        match forall_fact {
187            Fact::ForallFact(x) => Ok(x.clone()),
188            _ => {
189                unreachable!();
190            }
191        }
192    }
193
194    fn try_verify_exist_unique_by_exist_and_uniqueness_forall(
195        &mut self,
196        exist_fact: &ExistFactEnum,
197        verify_state: &VerifyState,
198    ) -> Result<Option<StmtResult>, RuntimeError> {
199        if exist_fact.params_def_with_type().number_of_params() == 0 {
200            return Ok(None);
201        }
202        let plain = ExistFactEnum::ExistFact(ExistFactBody::new(
203            exist_fact.params_def_with_type().clone(),
204            exist_fact.facts().clone(),
205            exist_fact.line_file(),
206        )?);
207        let wd_ok = verify_state.make_state_with_req_ok_set_to_true();
208        let plain_res = self.verify_exist_fact(&plain, &wd_ok)?;
209        if !plain_res.is_true() {
210            return Ok(None);
211        }
212
213        let uniqueness_forall = self.build_exist_unique_uniqueness_forall_fact(exist_fact)?;
214
215        let uniqueness_fact: Fact = uniqueness_forall.clone().into();
216        let uniq_res = self.verify_fact(&uniqueness_fact, &wd_ok)?;
217        if !uniq_res.is_true() {
218            return Ok(None);
219        }
220
221        let mut infers = InferResult::new();
222        infers.new_fact(&exist_fact.clone().into());
223        infers.new_infer_result_inside(stmt_result_infers(&plain_res));
224        infers.new_infer_result_inside(stmt_result_infers(&uniq_res));
225        infers.new_fact(&uniqueness_fact);
226
227        let out = FactualStmtSuccess::new_with_verified_by_known_fact_source(
228            exist_fact.clone().into(),
229            infers,
230            "exist!: witness exist and uniqueness forall verified".to_string(),
231            Some(uniqueness_fact),
232            None,
233            vec![],
234        );
235        Ok(Some(out.into()))
236    }
237
238    pub fn verify_exist_fact_with_known_exist_fact(
239        &mut self,
240        exist_fact: &ExistFactEnum,
241        known_exist_fact: &ExistFactEnum,
242    ) -> Result<StmtResult, RuntimeError> {
243        for environment in self.iter_environments_from_top() {
244            let result = Self::verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
245                self,
246                environment,
247                exist_fact,
248                known_exist_fact,
249            )?;
250            if result.is_true() {
251                return Ok(result);
252            }
253        }
254
255        Ok((StmtUnknown::new()).into())
256    }
257
258    pub fn verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
259        runtime: &Runtime,
260        environment: &Environment,
261        exist_fact: &ExistFactEnum,
262        known_exist_fact: &ExistFactEnum,
263    ) -> Result<StmtResult, RuntimeError> {
264        let goal_keys = Self::known_exist_lookup_keys(known_exist_fact);
265        let target_body_string = Self::exist_fact_normalized_body_string(runtime, exist_fact)
266            .map_err(|e| {
267                RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
268                    Some(Fact::from(exist_fact.clone()).into_stmt()),
269                    String::new(),
270                    exist_fact.line_file(),
271                    Some(e),
272                    vec![],
273                )))
274            })?;
275        for key in goal_keys.iter() {
276            let Some(known_exist_facts) = environment.known_exist_facts.get(key) else {
277                continue;
278            };
279            for known_fact in known_exist_facts.iter() {
280                if !known_fact.can_be_used_to_verify_goal(exist_fact) {
281                    continue;
282                }
283                let known_body_string =
284                    Self::exist_fact_normalized_body_string(runtime, known_fact).map_err(|e| {
285                        RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
286                            Some(Fact::from(exist_fact.clone()).into_stmt()),
287                            String::new(),
288                            exist_fact.line_file(),
289                            Some(e),
290                            vec![],
291                        )))
292                    })?;
293                if target_body_string == known_body_string {
294                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
295                        exist_fact.clone().into(),
296                        known_fact.to_string(),
297                        Some(known_fact.clone().into()),
298                        None,
299                        Vec::new(),
300                    ))
301                    .into());
302                }
303            }
304        }
305
306        Ok((StmtUnknown::new()).into())
307    }
308
309    fn known_exist_lookup_keys(goal: &ExistFactEnum) -> Vec<String> {
310        let mut keys = vec![goal.key()];
311        if let ExistFactEnum::ExistFact(body) = goal {
312            keys.push(ExistFactEnum::ExistUniqueFact(body.clone()).key());
313        }
314        keys.sort();
315        keys.dedup();
316        keys
317    }
318
319    fn exist_fact_normalized_body_string(
320        runtime: &Runtime,
321        exist_fact: &ExistFactEnum,
322    ) -> Result<String, RuntimeError> {
323        let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
324        let mut normalized_params: Vec<ParamGroupWithParamType> = Vec::new();
325        let mut param_index: usize = 0;
326
327        for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
328            let mut new_param_names: Vec<String> = Vec::new();
329            for original_name in param_def_with_type.params.iter() {
330                let normalized_name = format!("#{}", param_index);
331                param_index += 1;
332
333                param_to_arg_map.insert(
334                    original_name.clone(),
335                    obj_for_bound_param_in_scope(normalized_name.clone(), ParamObjType::Exist),
336                );
337                new_param_names.push(normalized_name);
338            }
339
340            let instantiated_param_type = runtime.inst_param_type(
341                &param_def_with_type.param_type,
342                &param_to_arg_map,
343                ParamObjType::Exist,
344            )?;
345            normalized_params.push(ParamGroupWithParamType::new(
346                new_param_names,
347                instantiated_param_type,
348            ));
349        }
350
351        let instantiated_exist_fact =
352            runtime.inst_exist_fact(exist_fact, &param_to_arg_map, ParamObjType::Exist, None)?;
353
354        let mut fact_strings: Vec<String> = Vec::new();
355        for fact in instantiated_exist_fact.facts().iter() {
356            let fact_as_fact = fact.from_ref_to_cloned_fact();
357            fact_strings.push(fact_as_fact.to_string());
358        }
359
360        let mut params_string_parts: Vec<String> = Vec::new();
361        for param_def_with_type in normalized_params.iter() {
362            params_string_parts.push(format!(
363                "{} {}",
364                param_def_with_type.params.join(","),
365                param_def_with_type.param_type
366            ));
367        }
368        let params_string = params_string_parts.join("; ");
369        let facts_string = fact_strings.join("; ");
370        Ok(format!("{} || {}", params_string, facts_string))
371    }
372}
373
374fn stmt_result_infers(result: &StmtResult) -> InferResult {
375    match result {
376        StmtResult::FactualStmtSuccess(x) => x.infers.clone(),
377        StmtResult::NonFactualStmtSuccess(x) => x.infers.clone(),
378        StmtResult::StmtUnknown(_) => InferResult::new(),
379    }
380}
litex/verify/verify_exist_fact.rs

litex/verify/
verify_exist_fact.rs
