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

litex/execute/by_stmt/
by_fn_and_by_fn_set.rs
