litex/execute/
exec_have_fn_by_induc.rs

1use crate::prelude::*;
2use crate::stmt::definition_stmt::induc_obj_plus_offset;
3
4impl Runtime {
5    pub fn exec_have_fn_by_induc(
6        &mut self,
7        stmt: &HaveFnByInducStmt,
8    ) -> Result<StmtResult, RuntimeError> {
9        self.run_in_local_env(|rt| rt.exec_have_fn_by_induc_verify_process(stmt))?;
10
11        let infer_result = self.exec_have_fn_by_induc_store_process(stmt)?;
12
13        Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
14    }
15
16    fn exec_have_fn_by_induc_verify_process(
17        &mut self,
18        stmt: &HaveFnByInducStmt,
19    ) -> Result<(), RuntimeError> {
20        for special_case_equal_to in stmt.special_cases_equal_tos.iter() {
21            self.verify_obj_well_defined_and_store_cache(
22                special_case_equal_to,
23                &VerifyState::new(0, false),
24            )?;
25        }
26
27        self.run_in_local_env(|rt| rt.exec_have_fn_by_induc_verify_last_case(stmt))?;
28
29        Ok(())
30    }
31
32    fn have_fn_by_induc_err(stmt: &HaveFnByInducStmt, cause: RuntimeError) -> RuntimeError {
33        RuntimeError::ExecStmtError({
34            let st: Stmt = stmt.clone().into();
35            let lf = st.line_file();
36            RuntimeErrorStruct::new(Some(st), String::new(), lf, Some(cause), vec![])
37        })
38    }
39
40    // have fn by induc from 0: f(x Z: x >= 0) R: case 0: … case 1: …
41    // Registers stmt.name in a new FnSet whose domain matches special-case indices.
42    fn have_fn_by_induc_verify_last_case_register_fn(
43        &mut self,
44        stmt: &HaveFnByInducStmt,
45        param_name: &str,
46    ) -> Result<(), RuntimeError> {
47        self.store_free_param_or_identifier_name(&stmt.name, ParamObjType::Identifier)?;
48
49        let random_param = self.generate_random_unused_name();
50
51        let induc_outer_param =
52            obj_for_bound_param_in_scope(param_name.to_string(), ParamObjType::Induc);
53        let param_minus_n: Obj = Sub::new(
54            induc_outer_param.clone(),
55            stmt.special_cases_equal_tos.len().into(),
56        )
57        .into();
58
59        let dom_facts: Vec<OrAndChainAtomicFact> = vec![
60            GreaterEqualFact::new(
61                obj_for_bound_param_in_scope(random_param.clone(), ParamObjType::FnSet),
62                param_minus_n,
63                stmt.line_file.clone(),
64            )
65            .into(),
66            LessFact::new(
67                obj_for_bound_param_in_scope(random_param.clone(), ParamObjType::FnSet),
68                induc_outer_param,
69                stmt.line_file.clone(),
70            )
71            .into(),
72        ];
73
74        let fn_set = self.new_fn_set(
75            vec![ParamGroupWithSet::new(
76                vec![random_param.clone()],
77                StandardSet::Z.into(),
78            )],
79            dom_facts,
80            stmt.ret_set.clone(),
81        )?;
82
83        let function_in_function_set_fact: Fact = InFact::new(
84            Identifier::new(stmt.name.clone()).into(),
85            fn_set.into(),
86            stmt.line_file.clone(),
87        )
88        .into();
89
90        self.verify_well_defined_and_store_and_infer_with_default_verify_state(
91            function_in_function_set_fact,
92        )
93        .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
94
95        Ok(())
96    }
97
98    fn have_fn_by_induc_verify_one_equal_to_well_defined(
99        &mut self,
100        stmt: &HaveFnByInducStmt,
101        equal_to: &Obj,
102        verify_state: &VerifyState,
103    ) -> Result<(), RuntimeError> {
104        self.verify_obj_well_defined_and_store_cache(equal_to, verify_state)
105            .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
106
107        let equal_to_in_ret_set_atomic_fact: AtomicFact = InFact::new(
108            equal_to.clone(),
109            stmt.ret_set.clone(),
110            stmt.line_file.clone(),
111        )
112        .into();
113        let verify_result = self
114            .verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, verify_state)
115            .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
116        if verify_result.is_unknown() {
117            return Err(short_exec_error(
118                stmt.clone().into(),
119                format!(
120                    "have_fn_by_induc: {} is not in return set {}",
121                    equal_to, stmt.ret_set
122                ),
123                None,
124                vec![],
125            ));
126        }
127        Ok(())
128    }
129
130    // have fn by induc from 0: f(x Z: x >= 0) R:
131    // case 0: 1
132    // case 1: 2
133    // case >= 2:
134    //      case x % 2 = 0: f(x - 1)
135    //      case x % 2 = 2: f(x - 1) + f(x - 2)
136    fn exec_have_fn_by_induc_verify_last_case(
137        &mut self,
138        stmt: &HaveFnByInducStmt,
139    ) -> Result<(), RuntimeError> {
140        let verify_state = VerifyState::new(0, false);
141        let n = stmt.special_cases_equal_tos.len();
142        let line_file = stmt.line_file.clone();
143
144        let param_name_str = stmt.param.clone();
145
146        let left_id: Obj =
147            obj_for_bound_param_in_scope(param_name_str.clone(), ParamObjType::Induc);
148
149        self.store_free_param_or_identifier_name(&param_name_str, ParamObjType::Induc)?;
150
151        self.define_parameter_by_binding_param_type(
152            &param_name_str,
153            &ParamType::Obj(StandardSet::Z.into()),
154            ParamObjType::Induc,
155        )?;
156
157        let param_larger_than_induc_plus_offset: AndChainAtomicFact = GreaterEqualFact::new(
158            left_id,
159            induc_obj_plus_offset(&stmt.induc_from, n),
160            line_file.clone(),
161        )
162        .into();
163
164        self.verify_well_defined_and_store_and_infer_with_default_verify_state(
165            param_larger_than_induc_plus_offset.into(),
166        )
167        .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
168
169        // Induction step needs f(x-1)..f(x-n); cache alone skips fn membership, so store FnObj and in ret_set.
170        for i in 1..=n {
171            let arg: Obj = Sub::new(
172                obj_for_bound_param_in_scope(param_name_str.clone(), ParamObjType::Induc),
173                i.into(),
174            )
175            .into();
176            let fn_obj: Obj = FnObj::new(
177                FnObjHead::Identifier(Identifier::new(stmt.name.clone())),
178                vec![vec![Box::new(arg.clone())]],
179            )
180            .into();
181            self.store_well_defined_obj_cache(&fn_obj);
182            let fn_in_ret: Fact =
183                InFact::new(fn_obj, stmt.ret_set.clone(), line_file.clone()).into();
184            self.verify_well_defined_and_store_and_infer_with_default_verify_state(fn_in_ret)
185                .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
186        }
187
188        self.have_fn_by_induc_verify_last_case_register_fn(stmt, &param_name_str)?;
189
190        match &stmt.last_case {
191            HaveFnByInducLastCase::EqualTo(eq) => {
192                self.have_fn_by_induc_verify_one_equal_to_well_defined(stmt, eq, &verify_state)?;
193            }
194            HaveFnByInducLastCase::NestedCases(last_pairs) if !last_pairs.is_empty() => {
195                let coverage_cases: Vec<AndChainAtomicFact> =
196                    last_pairs.iter().map(|c| c.case_fact.clone()).collect();
197                let coverage: Fact = OrFact::new(coverage_cases, line_file.clone()).into();
198                self.verify_fact_return_err_if_not_true(&coverage, &verify_state)
199                    .map_err(|e| {
200                        short_exec_error(
201                            stmt.clone().into(),
202                            "have_fn_by_induc: nested last cases do not cover all situations"
203                                .to_string(),
204                            Some(e),
205                            vec![],
206                        )
207                    })?;
208
209                for nested in last_pairs.iter() {
210                    self.run_in_local_env(|rt| {
211                        rt.verify_well_defined_and_store_and_infer_with_default_verify_state(
212                            nested.case_fact.clone().into(),
213                        )
214                        .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
215                        rt.have_fn_by_induc_verify_one_equal_to_well_defined(
216                            stmt,
217                            &nested.equal_to,
218                            &verify_state,
219                        )
220                    })?;
221                }
222            }
223            HaveFnByInducLastCase::NestedCases(_) => {
224                return Err(short_exec_error(
225                    stmt.clone().into(),
226                    "have_fn_by_induc: nested last case list must not be empty".to_string(),
227                    None,
228                    vec![],
229                ));
230            }
231        }
232
233        Ok(())
234    }
235
236    // When store_*_and_infer yields an empty chain, record the stored fact for infer_facts display.
237    fn merge_store_infer_with_fallback_fact(
238        infer_result: &mut InferResult,
239        store_infer: InferResult,
240        fallback_fact: &Fact,
241    ) {
242        let empty = store_infer.is_empty();
243        infer_result.new_infer_result_inside(store_infer);
244        if empty {
245            infer_result.new_fact(fallback_fact);
246        }
247    }
248
249    fn exec_have_fn_by_induc_store_process(
250        &mut self,
251        stmt: &HaveFnByInducStmt,
252    ) -> Result<InferResult, RuntimeError> {
253        // stmt.induc_from 得是 Z
254        let in_fact: AtomicFact = InFact::new(
255            stmt.induc_from.clone(),
256            StandardSet::Z.into(),
257            stmt.line_file.clone(),
258        )
259        .into();
260        let verify_result = self
261            .verify_atomic_fact(&in_fact, &VerifyState::new(0, false))
262            .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
263        if verify_result.is_unknown() {
264            return Err(short_exec_error(
265                stmt.clone().into(),
266                "have_fn_by_induc: induc_from is not in Z".to_string(),
267                None,
268                vec![],
269            ));
270        }
271
272        let mut infer_result = InferResult::new();
273        let fs = self.fn_set_from_fn_set_clause(&stmt.fn_user_fn_set_clause())?;
274
275        // Same order as `define_params_with_type`: declare the name before storing the typing fact,
276        // otherwise `verify_fact_well_defined` rejects `f $in ...` with "identifier not defined".
277        self.store_free_param_or_identifier_name(&stmt.name, ParamObjType::Identifier)?;
278
279        let bind_infer = self.define_parameter_by_binding_param_type(
280            &stmt.name,
281            &ParamType::Obj(fs.clone().into()),
282            ParamObjType::Identifier,
283        )?;
284        let bind_fact: Fact = InFact::new(
285            Identifier::new(stmt.name.clone()).into(),
286            fs.clone().into(),
287            stmt.line_file.clone(),
288        )
289        .into();
290        Self::merge_store_infer_with_fallback_fact(&mut infer_result, bind_infer, &bind_fact);
291
292        // Special cases: stmt.name(induc_from + i) = equal_to[i]
293        for i in 0..stmt.special_cases_equal_tos.len() {
294            let raw_arg = if i == 0 {
295                stmt.induc_from.clone()
296            } else {
297                Add::new(stmt.induc_from.clone(), i.into()).into()
298            };
299            // Fold numeric adds so we store f(1) not f(0 + 1)
300            let arg = raw_arg.replace_with_numeric_result_if_can_be_calculated().0;
301
302            let equal_to = &stmt.special_cases_equal_tos[i];
303
304            let fn_obj: Obj = FnObj::new(
305                FnObjHead::Identifier(Identifier::new(stmt.name.clone())),
306                vec![vec![Box::new(arg.clone())]],
307            )
308            .into();
309
310            let equal_fact: Fact =
311                EqualFact::new(fn_obj.clone(), equal_to.clone(), stmt.line_file.clone()).into();
312
313            let result = self
314                .verify_well_defined_and_store_and_infer_with_default_verify_state(
315                    equal_fact.clone(),
316                )
317                .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
318
319            Self::merge_store_infer_with_fallback_fact(&mut infer_result, result, &equal_fact);
320        }
321
322        match &stmt.last_case {
323            HaveFnByInducLastCase::EqualTo(eq) => {
324                let param_name = stmt.param.clone();
325                let param_def = vec![ParamGroupWithParamType::new(
326                    vec![param_name.clone()],
327                    ParamType::Obj(StandardSet::Z.into()),
328                )];
329
330                let mut dom: Vec<Fact> = stmt.forall_fn_base_dom_exist_or_facts();
331
332                let induc_plus_n =
333                    induc_obj_plus_offset(&stmt.induc_from, stmt.special_cases_equal_tos.len())
334                        .replace_with_numeric_result_if_can_be_calculated()
335                        .0;
336                dom.push(
337                    GreaterEqualFact::new(
338                        obj_for_bound_param_in_scope(param_name.clone(), ParamObjType::Forall),
339                        induc_plus_n,
340                        stmt.line_file.clone(),
341                    )
342                    .into(),
343                );
344
345                let forall_fact_raw = ForallFact::new(
346                    ParamDefWithType::new(param_def),
347                    dom,
348                    vec![EqualFact::new(
349                        FnObj::new(
350                            FnObjHead::Identifier(Identifier::new(stmt.name.clone())),
351                            vec![vec![Box::new(obj_for_bound_param_in_scope(
352                                param_name.clone(),
353                                ParamObjType::Forall,
354                            ))]],
355                        )
356                        .into(),
357                        eq.clone(),
358                        stmt.line_file.clone(),
359                    )
360                    .into()],
361                    stmt.line_file.clone(),
362                )?;
363
364                let forall_fact = self
365                    .inst_have_fn_forall_fact_for_store(forall_fact_raw)
366                    .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
367
368                let result = self
369                    .verify_well_defined_and_store_and_infer_with_default_verify_state(
370                        forall_fact.clone(),
371                    )
372                    .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
373                Self::merge_store_infer_with_fallback_fact(&mut infer_result, result, &forall_fact);
374            }
375            HaveFnByInducLastCase::NestedCases(last_pairs) => {
376                for nested in last_pairs.iter() {
377                    let param_name = stmt.param.clone();
378                    let param_def = vec![ParamGroupWithParamType::new(
379                        vec![param_name.clone()],
380                        ParamType::Obj(StandardSet::Z.into()),
381                    )];
382                    let eq = nested.equal_to.clone();
383
384                    let mut dom: Vec<Fact> = stmt.forall_fn_base_dom_exist_or_facts();
385
386                    let induc_plus_n =
387                        induc_obj_plus_offset(&stmt.induc_from, stmt.special_cases_equal_tos.len())
388                            .replace_with_numeric_result_if_can_be_calculated()
389                            .0;
390                    dom.push(
391                        GreaterEqualFact::new(
392                            obj_for_bound_param_in_scope(param_name.clone(), ParamObjType::Forall),
393                            induc_plus_n,
394                            stmt.line_file.clone(),
395                        )
396                        .into(),
397                    );
398
399                    let c: AndChainAtomicFact = nested.case_fact.clone();
400                    dom.push(c.into());
401
402                    let forall_fact_raw = ForallFact::new(
403                        ParamDefWithType::new(param_def),
404                        dom,
405                        vec![EqualFact::new(
406                            FnObj::new(
407                                FnObjHead::Identifier(Identifier::new(stmt.name.clone())),
408                                vec![vec![Box::new(obj_for_bound_param_in_scope(
409                                    param_name.clone(),
410                                    ParamObjType::Forall,
411                                ))]],
412                            )
413                            .into(),
414                            eq.clone(),
415                            stmt.line_file.clone(),
416                        )
417                        .into()],
418                        stmt.line_file.clone(),
419                    )?;
420
421                    let forall_fact = self
422                        .inst_have_fn_forall_fact_for_store(forall_fact_raw)
423                        .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
424
425                    let result = self
426                        .verify_well_defined_and_store_and_infer_with_default_verify_state(
427                            forall_fact.clone(),
428                        )
429                        .map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
430                    Self::merge_store_infer_with_fallback_fact(
431                        &mut infer_result,
432                        result,
433                        &forall_fact,
434                    );
435                }
436            }
437        }
438
439        Ok(infer_result)
440    }
441
442    pub fn exec_have_fn_by_induc_stmt(
443        &mut self,
444        stmt: &HaveFnByInducStmt,
445    ) -> Result<StmtResult, RuntimeError> {
446        self.exec_have_fn_by_induc(stmt)
447    }
448}
litex/execute/exec_have_fn_by_induc.rs

litex/execute/
exec_have_fn_by_induc.rs
