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