Skip to main content

litex/execute/by_stmt/
by_fn_and_by_fn_set.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3
4impl Runtime {
5    fn build_fn_characterization_facts(
6        &mut self,
7        function: &Obj,
8        fn_body: &FnSetBody,
9        line_file: &LineFile,
10        stmt_exec: &Stmt,
11        context: &str,
12    ) -> Result<(Fact, Fact, Fact, Fact), RuntimeError> {
13        let param_names = ParamGroupWithSet::collect_param_names(&fn_body.params_def_with_set);
14        if param_names.is_empty() {
15            return Err(short_exec_error(
16                stmt_exec.clone(),
17                format!("{}: fn set has no parameters", context),
18                None,
19                vec![],
20            ));
21        }
22
23        let mut generated_forall_names = self
24            .generate_random_unused_names(param_names.len() + 2)
25            .into_iter();
26        let forall_element_name = generated_forall_names.next().unwrap();
27        let forall_z_name = generated_forall_names.next().unwrap();
28        let generated_forall_param_names: Vec<String> = generated_forall_names.collect();
29        let mut original_param_to_forall_obj: HashMap<String, Obj> =
30            HashMap::with_capacity(param_names.len());
31        let mut forall_param_defs_with_type: Vec<ParamGroupWithParamType> =
32            Vec::with_capacity(fn_body.params_def_with_set.len());
33        let mut flat_index: usize = 0;
34        for param_def_with_set in fn_body.params_def_with_set.iter() {
35            let next_flat_index = flat_index + param_def_with_set.params.len();
36            let generated_names_for_current_group =
37                generated_forall_param_names[flat_index..next_flat_index].to_vec();
38            let instantiated_type = ParamType::Obj(
39                self.inst_obj(
40                    param_def_with_set.set_obj(),
41                    &original_param_to_forall_obj,
42                    ParamObjType::FnSet,
43                )
44                .map_err(|inst_error| {
45                    short_exec_error(
46                        stmt_exec.clone(),
47                        format!("{}: failed to instantiate generated parameter set", context),
48                        Some(inst_error),
49                        vec![],
50                    )
51                })?,
52            );
53            forall_param_defs_with_type.push(ParamGroupWithParamType::new(
54                generated_names_for_current_group.clone(),
55                instantiated_type,
56            ));
57            for (original_name, generated_name) in param_def_with_set
58                .params
59                .iter()
60                .zip(generated_names_for_current_group.iter())
61            {
62                original_param_to_forall_obj.insert(
63                    original_name.clone(),
64                    obj_for_bound_param_in_scope(generated_name.clone(), ParamObjType::FnSet),
65                );
66            }
67            flat_index = next_flat_index;
68        }
69        // Exist body binds the same generated names as `Exist` params (~3), not FnSet (~5).
70        let original_param_to_exist_inner: HashMap<String, Obj> = original_param_to_forall_obj
71            .iter()
72            .filter_map(|(orig, obj)| {
73                if let Obj::Atom(AtomObj::FnSet(p)) = obj {
74                    Some((
75                        orig.clone(),
76                        obj_for_bound_param_in_scope(p.name.clone(), ParamObjType::Exist),
77                    ))
78                } else {
79                    None
80                }
81            })
82            .collect();
83        let forall_ret_set = self
84            .inst_obj(
85                fn_body.ret_set.as_ref(),
86                &original_param_to_forall_obj,
87                ParamObjType::FnSet,
88            )
89            .map_err(|inst_error| {
90                short_exec_error(
91                    stmt_exec.clone(),
92                    format!("{}: failed to instantiate generated return set", context),
93                    Some(inst_error),
94                    vec![],
95                )
96            })?;
97        let forall_args_exist: Vec<Obj> = param_names
98            .iter()
99            .map(|param_name| {
100                original_param_to_exist_inner
101                    .get(param_name)
102                    .unwrap()
103                    .clone()
104            })
105            .collect();
106        let forall_element_obj: Obj =
107            obj_for_bound_param_in_scope(forall_element_name.clone(), ParamObjType::Forall);
108        let mut forall_element_cart_factors: Vec<Obj> = Vec::with_capacity(param_names.len() + 1);
109        for param_def_with_type in forall_param_defs_with_type.iter() {
110            match &param_def_with_type.param_type {
111                ParamType::Obj(obj) => {
112                    for _ in param_def_with_type.params.iter() {
113                        forall_element_cart_factors.push(obj.clone());
114                    }
115                }
116                _ => unreachable!(),
117            }
118        }
119        forall_element_cart_factors.push(forall_ret_set.clone());
120        let forall_element_cart_set = Cart::new(forall_element_cart_factors).into();
121        let forall_shape = ForallFact::new(
122            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
123                vec![forall_element_name.clone()],
124                ParamType::Obj(function.clone()),
125            )]),
126            vec![],
127            vec![
128                InFact::new(
129                    forall_element_obj.clone(),
130                    forall_element_cart_set,
131                    line_file.clone(),
132                )
133                .into(),
134                EqualFact::new(
135                    TupleDim::new(forall_element_obj.clone()).into(),
136                    Number::new((param_names.len() + 1).to_string()).into(),
137                    line_file.clone(),
138                )
139                .into(),
140            ],
141            line_file.clone(),
142        )?
143        .into();
144        let forall_z_obj = obj_for_bound_param_in_scope(forall_z_name.clone(), ParamObjType::Exist);
145        let mut tuple_in_fn = forall_args_exist;
146        tuple_in_fn.push(forall_z_obj);
147        let tuple_in_fn = Tuple::new(tuple_in_fn).into();
148        let forall_in = ForallFact::new(
149            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
150                vec![forall_element_name],
151                ParamType::Obj(function.clone()),
152            )]),
153            vec![],
154            vec![ExistFactEnum::ExistFact(ExistFactBody::new(
155                ParamDefWithType::new({
156                    let mut exist_param_defs = forall_param_defs_with_type;
157                    exist_param_defs.push(ParamGroupWithParamType::new(
158                        vec![forall_z_name],
159                        ParamType::Obj(forall_ret_set),
160                    ));
161                    exist_param_defs
162                }),
163                {
164                    let mut facts: Vec<ExistBodyFact> =
165                        Vec::with_capacity(fn_body.dom_facts.len() + 1);
166                    for dom_fact in fn_body.dom_facts.iter() {
167                        facts.push(
168                            self.inst_or_and_chain_atomic_fact(
169                                dom_fact,
170                                &original_param_to_exist_inner,
171                                ParamObjType::FnSet,
172                                None,
173                            )
174                            .map_err(|inst_error| {
175                                short_exec_error(
176                                    stmt_exec.clone(),
177                                    format!(
178                                        "{}: failed to instantiate generated domain fact",
179                                        context
180                                    ),
181                                    Some(inst_error),
182                                    vec![],
183                                )
184                            })?
185                            .into(),
186                        );
187                    }
188                    facts.push(
189                        EqualFact::new(forall_element_obj, tuple_in_fn, line_file.clone()).into(),
190                    );
191                    facts
192                },
193                line_file.clone(),
194            )?)
195            .into()],
196            line_file.clone(),
197        )?
198        .into();
199
200        let mut generated_exist_names = self
201            .generate_random_unused_names(param_names.len() + 2)
202            .into_iter();
203        let exist_element_name = generated_exist_names.next().unwrap();
204        let exist_z_name = generated_exist_names.next().unwrap();
205        let generated_exist_param_names: Vec<String> = generated_exist_names.collect();
206        let mut original_param_to_exist_obj: HashMap<String, Obj> =
207            HashMap::with_capacity(param_names.len());
208        let mut exist_param_defs_with_type: Vec<ParamGroupWithParamType> =
209            Vec::with_capacity(fn_body.params_def_with_set.len());
210        let mut exist_flat_index: usize = 0;
211        for param_def_with_set in fn_body.params_def_with_set.iter() {
212            let next_flat_index = exist_flat_index + param_def_with_set.params.len();
213            let generated_names_for_current_group =
214                generated_exist_param_names[exist_flat_index..next_flat_index].to_vec();
215            let instantiated_type = ParamType::Obj(
216                self.inst_obj(
217                    param_def_with_set.set_obj(),
218                    &original_param_to_exist_obj,
219                    ParamObjType::FnSet,
220                )
221                .map_err(|inst_error| {
222                    short_exec_error(
223                        stmt_exec.clone(),
224                        format!("{}: failed to instantiate witness parameter set", context),
225                        Some(inst_error),
226                        vec![],
227                    )
228                })?,
229            );
230            exist_param_defs_with_type.push(ParamGroupWithParamType::new(
231                generated_names_for_current_group.clone(),
232                instantiated_type,
233            ));
234            for (original_name, generated_name) in param_def_with_set
235                .params
236                .iter()
237                .zip(generated_names_for_current_group.iter())
238            {
239                original_param_to_exist_obj.insert(
240                    original_name.clone(),
241                    obj_for_bound_param_in_scope(generated_name.clone(), ParamObjType::FnSet),
242                );
243            }
244            exist_flat_index = next_flat_index;
245        }
246        // Outer `forall_exist` quantifies fn parameters as Forall (~1), not FnSet (~5).
247        let original_param_to_forall_witness: HashMap<String, Obj> = original_param_to_exist_obj
248            .iter()
249            .filter_map(|(orig, obj)| {
250                if let Obj::Atom(AtomObj::FnSet(p)) = obj {
251                    Some((
252                        orig.clone(),
253                        obj_for_bound_param_in_scope(p.name.clone(), ParamObjType::Forall),
254                    ))
255                } else {
256                    None
257                }
258            })
259            .collect();
260        let exist_ret_set = self
261            .inst_obj(
262                fn_body.ret_set.as_ref(),
263                &original_param_to_exist_obj,
264                ParamObjType::FnSet,
265            )
266            .map_err(|inst_error| {
267                short_exec_error(
268                    stmt_exec.clone(),
269                    format!("{}: failed to instantiate witness return set", context),
270                    Some(inst_error),
271                    vec![],
272                )
273            })?;
274        let exist_args_for_pair: Vec<Obj> = param_names
275            .iter()
276            .map(|param_name| {
277                original_param_to_forall_witness
278                    .get(param_name)
279                    .unwrap()
280                    .clone()
281            })
282            .collect();
283        let exist_element_obj =
284            obj_for_bound_param_in_scope(exist_element_name.clone(), ParamObjType::Exist);
285        let exist_z_obj = obj_for_bound_param_in_scope(exist_z_name.clone(), ParamObjType::Exist);
286        let mut exist_tuple = exist_args_for_pair;
287        exist_tuple.push(exist_z_obj);
288        let exist_tuple = Tuple::new(exist_tuple).into();
289        let exist_fact = ExistFactEnum::ExistFact(ExistFactBody::new(
290            ParamDefWithType::new(vec![
291                ParamGroupWithParamType::new(
292                    vec![exist_element_name],
293                    ParamType::Obj(function.clone()),
294                ),
295                ParamGroupWithParamType::new(vec![exist_z_name], ParamType::Obj(exist_ret_set)),
296            ]),
297            vec![EqualFact::new(exist_element_obj, exist_tuple, line_file.clone()).into()],
298            line_file.clone(),
299        )?);
300        let forall_exist = ForallFact::new(
301            ParamDefWithType::new(exist_param_defs_with_type),
302            {
303                let mut dom_facts: Vec<Fact> = Vec::with_capacity(fn_body.dom_facts.len());
304                for dom_fact in fn_body.dom_facts.iter() {
305                    dom_facts.push(
306                        self.inst_or_and_chain_atomic_fact(
307                            dom_fact,
308                            &original_param_to_forall_witness,
309                            ParamObjType::FnSet,
310                            None,
311                        )
312                        .map_err(|inst_error| {
313                            short_exec_error(
314                                stmt_exec.clone(),
315                                format!("{}: failed to instantiate witness domain fact", context),
316                                Some(inst_error),
317                                vec![],
318                            )
319                        })?
320                        .into(),
321                    );
322                }
323                dom_facts
324            },
325            vec![exist_fact.into()],
326            line_file.clone(),
327        )?
328        .into();
329
330        let unique_names = self.generate_random_unused_names(2);
331        let unique_x1_name = unique_names[0].clone();
332        let unique_x2_name = unique_names[1].clone();
333        let unique_x1_obj: Obj =
334            obj_for_bound_param_in_scope(unique_x1_name.clone(), ParamObjType::Forall);
335        let unique_x2_obj: Obj =
336            obj_for_bound_param_in_scope(unique_x2_name.clone(), ParamObjType::Forall);
337        let mut unique_element_cart_factors: Vec<Obj> = Vec::with_capacity(param_names.len() + 1);
338        for param_def_with_set in fn_body.params_def_with_set.iter() {
339            for _ in param_def_with_set.params.iter() {
340                unique_element_cart_factors.push(param_def_with_set.set_obj().clone());
341            }
342        }
343        unique_element_cart_factors.push(fn_body.ret_set.as_ref().clone());
344        let unique_element_cart_set: Obj = Cart::new(unique_element_cart_factors).into();
345        let mut unique_dom_facts: Vec<Fact> = Vec::with_capacity(param_names.len() + 2);
346        unique_dom_facts.push(
347            InFact::new(
348                unique_x1_obj.clone(),
349                unique_element_cart_set.clone(),
350                line_file.clone(),
351            )
352            .into(),
353        );
354        unique_dom_facts.push(
355            InFact::new(
356                unique_x2_obj.clone(),
357                unique_element_cart_set.clone(),
358                line_file.clone(),
359            )
360            .into(),
361        );
362        for index in 1..=param_names.len() {
363            unique_dom_facts.push(
364                EqualFact::new(
365                    ObjAtIndex::new(unique_x1_obj.clone(), Number::new(index.to_string()).into())
366                        .into(),
367                    ObjAtIndex::new(unique_x2_obj.clone(), Number::new(index.to_string()).into())
368                        .into(),
369                    line_file.clone(),
370                )
371                .into(),
372            );
373        }
374        let forall_unique = ForallFact::new(
375            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
376                vec![unique_x1_name, unique_x2_name],
377                ParamType::Obj(function.clone()),
378            )]),
379            unique_dom_facts,
380            vec![EqualFact::new(unique_x1_obj, unique_x2_obj, line_file.clone()).into()],
381            line_file.clone(),
382        )?
383        .into();
384
385        Ok((forall_shape, forall_in, forall_exist, forall_unique))
386    }
387
388    // `by fn as set` stores the characterization facts in the main environment.
389    fn exec_by_fn_stmt_verify_process(&mut self) -> Result<(), RuntimeError> {
390        Ok(())
391    }
392
393    fn exec_by_fn_stmt_store_process(
394        &mut self,
395        stmt_exec: &Stmt,
396        forall_shape: Fact,
397        forall_in: Fact,
398        forall_exist: Fact,
399        forall_unique: Fact,
400    ) -> Result<InferResult, RuntimeError> {
401        // `store_fact...` on forall facts already feeds the stored fact back through `infer`,
402        // so avoid pre-recording the same fact here or JSON `infer_facts` will show duplicates.
403        let mut infer_result = InferResult::new();
404        let infer_shape = self
405            .verify_well_defined_and_store_and_infer_with_default_verify_state(forall_shape)
406            .map_err(|store_fact_error| {
407                short_exec_error(
408                    stmt_exec.clone(),
409                    "by fn as set: failed to store cart/tuple shape characterization fact"
410                        .to_string(),
411                    Some(store_fact_error),
412                    vec![],
413                )
414            })?;
415        infer_result.new_infer_result_inside(infer_shape);
416        let infer_in = self
417            .verify_well_defined_and_store_and_infer_with_default_verify_state(forall_in)
418            .map_err(|store_fact_error| {
419                short_exec_error(
420                    stmt_exec.clone(),
421                    "by fn as set: failed to store graph-element characterization fact".to_string(),
422                    Some(store_fact_error),
423                    vec![],
424                )
425            })?;
426        infer_result.new_infer_result_inside(infer_in);
427
428        let infer_exist = self
429            .verify_well_defined_and_store_and_infer_with_default_verify_state(forall_exist)
430            .map_err(|store_fact_error| {
431                short_exec_error(
432                    stmt_exec.clone(),
433                    "by fn as set: failed to store element characterization fact".to_string(),
434                    Some(store_fact_error),
435                    vec![],
436                )
437            })?;
438        infer_result.new_infer_result_inside(infer_exist);
439
440        let infer_unique = self
441            .store_fact_without_forall_coverage_check_and_infer(forall_unique)
442            .map_err(|store_fact_error| {
443                short_exec_error(
444                    stmt_exec.clone(),
445                    "by fn as set: failed to store uniqueness characterization fact".to_string(),
446                    Some(store_fact_error),
447                    vec![],
448                )
449            })?;
450        infer_result.new_infer_result_inside(infer_unique);
451
452        Ok(infer_result)
453    }
454
455    pub fn exec_by_fn_stmt(&mut self, stmt: &ByFnAsSetStmt) -> Result<StmtResult, RuntimeError> {
456        let stmt_exec: Stmt = stmt.clone().into();
457
458        let fn_set = match self.get_cloned_object_in_fn_set(&stmt.function) {
459            Some(fs) => fs,
460            None => {
461                return Err(short_exec_error(
462                    stmt_exec,
463                    format!(
464                        "by fn as set: `{}` is not known to belong to a fn set",
465                        stmt.function
466                    ),
467                    None,
468                    vec![],
469                ));
470            }
471        };
472
473        let (forall_shape, forall_in, forall_exist, forall_unique) = self
474            .build_fn_characterization_facts(
475                &stmt.function,
476                &fn_set,
477                &stmt.line_file,
478                &stmt_exec,
479                "by fn as set",
480            )?;
481
482        self.run_in_local_env(|rt| rt.exec_by_fn_stmt_verify_process())?;
483
484        let infer_result = self.exec_by_fn_stmt_store_process(
485            &stmt_exec,
486            forall_shape,
487            forall_in,
488            forall_exist,
489            forall_unique,
490        )?;
491
492        Ok((NonFactualStmtSuccess::new(stmt_exec, infer_result, vec![])).into())
493    }
494
495    fn exec_by_fn_set_stmt_verify_process(
496        &mut self,
497        stmt_exec: &Stmt,
498        forall_shape: &Fact,
499        forall_in: &Fact,
500        forall_exist: &Fact,
501        forall_unique: &Fact,
502    ) -> Result<Vec<StmtResult>, RuntimeError> {
503        let verify_state = VerifyState::new(0, false);
504        let verify_shape_fact = self
505            .verify_fact_return_err_if_not_true(forall_shape, &verify_state)
506            .map_err(|verify_error| {
507                short_exec_error(
508                    stmt_exec.clone(),
509                    format!(
510                        "by fn set as set: failed to prove cart/tuple shape characterization `{}`",
511                        forall_shape
512                    ),
513                    Some(verify_error),
514                    vec![],
515                )
516            })?;
517        let verify_random_param_fact = self
518            .verify_fact_return_err_if_not_true(forall_in, &verify_state)
519            .map_err(|verify_error| {
520                short_exec_error(
521                    stmt_exec.clone(),
522                    format!(
523                        "by fn set as set: failed to prove graph-element characterization `{}`",
524                        forall_in
525                    ),
526                    Some(verify_error),
527                    vec![],
528                )
529            })?;
530        let verify_param_to_element_fact = self
531            .verify_fact_return_err_if_not_true(forall_exist, &verify_state)
532            .map_err(|verify_error| {
533                short_exec_error(
534                    stmt_exec.clone(),
535                    format!(
536                        "by fn set as set: failed to prove graph-coverage characterization `{}`",
537                        forall_exist
538                    ),
539                    Some(verify_error),
540                    vec![],
541                )
542            })?;
543        let verify_uniqueness_fact = self
544            .verify_fact_return_err_if_not_true(forall_unique, &verify_state)
545            .map_err(|verify_error| {
546                short_exec_error(
547                    stmt_exec.clone(),
548                    format!(
549                        "by fn set as set: failed to prove graph-uniqueness characterization `{}`",
550                        forall_unique
551                    ),
552                    Some(verify_error),
553                    vec![],
554                )
555            })?;
556
557        Ok(vec![
558            verify_shape_fact,
559            verify_random_param_fact,
560            verify_param_to_element_fact,
561            verify_uniqueness_fact,
562        ])
563    }
564
565    fn exec_by_fn_set_stmt_store_process(
566        &mut self,
567        stmt: &ByFnSetAsSetStmt,
568        stmt_exec: &Stmt,
569    ) -> Result<InferResult, RuntimeError> {
570        let membership_fact = InFact::new(
571            stmt.func.clone(),
572            stmt.fn_set.clone().into(),
573            stmt.line_file.clone(),
574        )
575        .into();
576        self.store_atomic_fact_without_well_defined_verified_and_infer(membership_fact)
577            .map_err(|store_fact_error| {
578                short_exec_error(
579                    stmt_exec.clone(),
580                    "by fn set as set: failed to store membership fact".to_string(),
581                    Some(store_fact_error),
582                    vec![],
583                )
584            })
585    }
586
587    pub fn exec_by_fn_set_stmt(
588        &mut self,
589        stmt: &ByFnSetAsSetStmt,
590    ) -> Result<StmtResult, RuntimeError> {
591        let stmt_exec: Stmt = stmt.clone().into();
592        let (forall_shape, forall_in, forall_exist, forall_unique) = self
593            .build_fn_characterization_facts(
594                &stmt.func,
595                &stmt.fn_set.body,
596                &stmt.line_file,
597                &stmt_exec,
598                "by fn set as set",
599            )?;
600
601        let verify_inside_results = self.run_in_local_env(|rt| {
602            rt.exec_by_fn_set_stmt_verify_process(
603                &stmt_exec,
604                &forall_shape,
605                &forall_in,
606                &forall_exist,
607                &forall_unique,
608            )
609        })?;
610
611        let infer_result = self.exec_by_fn_set_stmt_store_process(stmt, &stmt_exec)?;
612
613        Ok((NonFactualStmtSuccess::new(stmt_exec, infer_result, verify_inside_results)).into())
614    }
615}