litex/execute/by_stmt/
induc_by_stmt.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3
4impl Runtime {
5    pub fn exec_by_induc_stmt(&mut self, stmt: &ByInducStmt) -> Result<StmtResult, RuntimeError> {
6        let body_exec_result: Result<StmtResult, RuntimeError> = self.run_in_local_env(|rt| {
7            if stmt.strong {
8                rt.exec_strong_induc_stmt_assume_proof_context(stmt)?;
9            } else {
10                rt.exec_by_induc_stmt_assume_proof_context(stmt)?;
11            }
12            let mut infer_result = InferResult::new();
13            let mut inside_results: Vec<StmtResult> = Vec::new();
14            for proof_stmt in stmt.proof.iter() {
15                inside_results.push(rt.exec_stmt(proof_stmt)?);
16            }
17            for fact in stmt.to_prove.iter() {
18                let one_fact_infer_result = if stmt.strong {
19                    rt.exec_strong_induc_stmt_for_one_fact(stmt, fact)?
20                } else {
21                    rt.exec_by_induc_stmt_for_one_fact(stmt, fact)?
22                };
23                infer_result.new_infer_result_inside(one_fact_infer_result);
24            }
25            Ok(
26                NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, inside_results)
27                    .into(),
28            )
29        });
30
31        let non_err_after_body: StmtResult = match body_exec_result {
32            Ok(non_err_stmt_exec_result) => non_err_stmt_exec_result,
33            Err(runtime_error) => return Err(runtime_error),
34        };
35
36        let store_err_msg = if stmt.strong {
37            "strong_induc: failed to build concluding forall fact"
38        } else {
39            "by induc: failed to build concluding forall fact"
40        };
41        let corresponding_forall_fact =
42            self.by_induc_stmt_stored_forall_fact(stmt)
43                .map_err(|runtime_error| {
44                    short_exec_error(
45                        stmt.clone().into(),
46                        store_err_msg.to_string(),
47                        Some(runtime_error),
48                        vec![],
49                    )
50                })?;
51        let infer_after_store = self
52            .verify_well_defined_and_store_and_infer_with_default_verify_state(
53                corresponding_forall_fact,
54            )?;
55
56        Ok(non_err_after_body.with_infers(infer_after_store))
57    }
58}
59
60impl Runtime {
61    /// Inner bound variable name for `forall y` in strong induction; avoids clashing with the outer parameter.
62    fn strong_induc_inner_param_name(outer: &str) -> String {
63        if outer == "y" {
64            "y_inner".to_string()
65        } else {
66            "y".to_string()
67        }
68    }
69
70    /// Induction hypothesis for strong induc: `forall y, m <= y <= n =>: P(y)` in the case proof environment (`n` is [Induc]).
71    fn strong_induc_ih_forall_fact(
72        &self,
73        stmt: &ByInducStmt,
74        fact: &ExistOrAndChainAtomicFact,
75    ) -> Result<Fact, RuntimeError> {
76        let lf = stmt.line_file.clone();
77        let inner = Self::strong_induc_inner_param_name(&stmt.param);
78        let y_obj = obj_for_bound_param_in_scope(inner.clone(), ParamObjType::Forall);
79        let n_induc = obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Induc);
80        // `to_prove` uses the outer param name (e.g. `n` in `$p(n)`); substitute it with the inner `y` object.
81        let y_map = HashMap::from([(stmt.param.clone(), y_obj.clone())]);
82        let p_y =
83            self.inst_exist_or_and_chain_atomic_fact(fact, &y_map, ParamObjType::Forall, None)?;
84        Ok(ForallFact::new(
85            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
86                vec![inner],
87                ParamType::Obj(StandardSet::Z.into()),
88            )]),
89            vec![
90                GreaterEqualFact::new(y_obj.clone(), stmt.induc_from.clone(), lf.clone()).into(),
91                LessEqualFact::new(y_obj, n_induc, lf.clone()).into(),
92            ],
93            vec![p_y],
94            lf,
95        )?
96        .into())
97    }
98
99    /// Step obligation for strong induc: `forall n, n >= m, (forall y, m<=y<=n =>: P(y)) =>: P(n+1)`.
100    fn strong_induc_step_forall_fact(
101        &self,
102        stmt: &ByInducStmt,
103        fact: &ExistOrAndChainAtomicFact,
104    ) -> Result<Fact, RuntimeError> {
105        let lf = stmt.line_file.clone();
106        let inner = Self::strong_induc_inner_param_name(&stmt.param);
107        let n_forall = obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Forall);
108        let y_obj = obj_for_bound_param_in_scope(inner.clone(), ParamObjType::Forall);
109        // Same as IH: map outer param name in `$p(n)` to the inner `y` binding.
110        let y_map = HashMap::from([(stmt.param.clone(), y_obj.clone())]);
111        let p_y =
112            self.inst_exist_or_and_chain_atomic_fact(fact, &y_map, ParamObjType::Forall, None)?;
113        let inner_forall: Fact = ForallFact::new(
114            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
115                vec![inner],
116                ParamType::Obj(StandardSet::Z.into()),
117            )]),
118            vec![
119                GreaterEqualFact::new(y_obj.clone(), stmt.induc_from.clone(), lf.clone()).into(),
120                LessEqualFact::new(y_obj, n_forall.clone(), lf.clone()).into(),
121            ],
122            vec![p_y],
123            lf.clone(),
124        )?
125        .into();
126
127        let param_plus_one_obj =
128            Add::new(n_forall.clone(), Number::new("1".to_string()).into()).into();
129        let mut n_to_n1: HashMap<String, Obj> = HashMap::new();
130        n_to_n1.insert(stmt.param.clone(), param_plus_one_obj);
131        let p_n1 =
132            self.inst_exist_or_and_chain_atomic_fact(fact, &n_to_n1, ParamObjType::Forall, None)?;
133
134        Ok(ForallFact::new(
135            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
136                vec![stmt.param.clone()],
137                ParamType::Obj(StandardSet::Z.into()),
138            )]),
139            vec![
140                GreaterEqualFact::new(n_forall, stmt.induc_from.clone(), lf.clone()).into(),
141                inner_forall,
142            ],
143            vec![p_n1],
144            lf,
145        )?
146        .into())
147    }
148
149    fn exec_strong_induc_stmt_assume_proof_context(
150        &mut self,
151        stmt: &ByInducStmt,
152    ) -> Result<(), RuntimeError> {
153        let params_def = ParamDefWithType::new(vec![ParamGroupWithParamType::new(
154            vec![stmt.param.clone()],
155            ParamType::Obj(StandardSet::Z.into()),
156        )]);
157        self.define_params_with_type(&params_def, false, ParamObjType::Induc)
158            .map_err(|e| {
159                short_exec_error(
160                    stmt.clone().into(),
161                    "strong_induc: failed to declare induction parameter in proof".to_string(),
162                    Some(e),
163                    vec![],
164                )
165            })?;
166
167        let dom_ge: Fact = GreaterEqualFact::new(
168            obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Induc),
169            stmt.induc_from.clone(),
170            stmt.line_file.clone(),
171        )
172        .into();
173        self.verify_well_defined_and_store_and_infer_with_default_verify_state(dom_ge)
174            .map_err(|e| {
175                short_exec_error(
176                    stmt.clone().into(),
177                    "strong_induc: failed to assume domain (param >= induction start) in proof"
178                        .to_string(),
179                    Some(e),
180                    vec![],
181                )
182            })?;
183
184        for fact in stmt.to_prove.iter() {
185            let ih = self.strong_induc_ih_forall_fact(stmt, fact)?;
186            self.verify_well_defined_and_store_and_infer_with_default_verify_state(ih)
187                .map_err(|e| {
188                    short_exec_error(
189                        stmt.clone().into(),
190                        "strong_induc: failed to assume strong induction hypothesis in proof"
191                            .to_string(),
192                        Some(e),
193                        vec![],
194                    )
195                })?;
196        }
197        Ok(())
198    }
199
200    fn exec_strong_induc_stmt_for_one_fact(
201        &mut self,
202        stmt: &ByInducStmt,
203        fact: &ExistOrAndChainAtomicFact,
204    ) -> Result<InferResult, RuntimeError> {
205        let mut infer_result = InferResult::new();
206
207        let mut base_case_param_to_arg_map: HashMap<String, Obj> = HashMap::new();
208        base_case_param_to_arg_map.insert(stmt.param.clone(), stmt.induc_from.clone());
209        let base_case_fact = self
210            .inst_exist_or_and_chain_atomic_fact(
211                fact,
212                &base_case_param_to_arg_map,
213                ParamObjType::Induc,
214                None,
215            )?
216            .to_fact();
217        self.verify_fact_return_err_if_not_true(&base_case_fact, &VerifyState::new(0, false))
218            .map_err(|verify_error| {
219                short_exec_error(
220                    stmt.clone().into(),
221                    format!("strong_induc: base case is not proved `{}`", base_case_fact),
222                    Some(verify_error),
223                    vec![],
224                )
225            })?;
226
227        let induc_from_in_z_fact = InFact::new(
228            stmt.induc_from.clone(),
229            StandardSet::Z.into(),
230            stmt.line_file.clone(),
231        )
232        .into();
233        let verify_induc_from_in_z_result = self
234            .verify_atomic_fact(&induc_from_in_z_fact, &VerifyState::new(0, false))
235            .map_err(|verify_error| {
236                short_exec_error(
237                    stmt.clone().into(),
238                    format!("strong_induc: failed to verify `{}`", induc_from_in_z_fact),
239                    Some(verify_error),
240                    vec![],
241                )
242            })?;
243        if verify_induc_from_in_z_result.is_unknown() {
244            return Err(short_exec_error(
245                stmt.clone().into(),
246                format!("strong_induc: failed to verify `{}`", induc_from_in_z_fact),
247                None,
248                vec![],
249            ));
250        }
251
252        let corresponding_forall_fact = self.strong_induc_step_forall_fact(stmt, fact)?;
253
254        self.verify_fact_return_err_if_not_true(
255            &corresponding_forall_fact,
256            &VerifyState::new(0, false),
257        )
258        .map_err(|well_defined_error| {
259            short_exec_error(
260                stmt.clone().into(),
261                format!(
262                    "strong_induc: generated step forall is not well-defined `{}`",
263                    corresponding_forall_fact
264                ),
265                Some(well_defined_error),
266                vec![],
267            )
268        })?;
269
270        infer_result.new_fact(&corresponding_forall_fact);
271        Ok(infer_result)
272    }
273
274    /// `x $in Z`, `x >= induc_from`, and each `to_prove` instantiated at `x` (induction hypothesis)
275    /// for the step — same assumptions the checker uses when verifying the generated step `forall`.
276    fn exec_by_induc_stmt_assume_proof_context(
277        &mut self,
278        stmt: &ByInducStmt,
279    ) -> Result<(), RuntimeError> {
280        let params_def = ParamDefWithType::new(vec![ParamGroupWithParamType::new(
281            vec![stmt.param.clone()],
282            ParamType::Obj(StandardSet::Z.into()),
283        )]);
284        self.define_params_with_type(&params_def, false, ParamObjType::Induc)
285            .map_err(|e| {
286                short_exec_error(
287                    stmt.clone().into(),
288                    "by induc: failed to declare induction parameter in proof".to_string(),
289                    Some(e),
290                    vec![],
291                )
292            })?;
293
294        let dom_ge: Fact = GreaterEqualFact::new(
295            obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Induc),
296            stmt.induc_from.clone(),
297            stmt.line_file.clone(),
298        )
299        .into();
300        self.verify_well_defined_and_store_and_infer_with_default_verify_state(dom_ge)
301            .map_err(|e| {
302                short_exec_error(
303                    stmt.clone().into(),
304                    "by induc: failed to assume domain (param >= induction start) in proof"
305                        .to_string(),
306                    Some(e),
307                    vec![],
308                )
309            })?;
310
311        let induc_param_obj = obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Induc);
312        let induc_map: HashMap<String, Obj> =
313            HashMap::from([(stmt.param.clone(), induc_param_obj)]);
314        for fact in stmt.to_prove.iter() {
315            let inst = self
316                .inst_exist_or_and_chain_atomic_fact(fact, &induc_map, ParamObjType::Induc, None)?
317                .to_fact();
318            self.verify_well_defined_and_store_and_infer_with_default_verify_state(inst)
319                .map_err(|e| {
320                    short_exec_error(
321                        stmt.clone().into(),
322                        "by induc: failed to assume induction hypothesis in proof".to_string(),
323                        Some(e),
324                        vec![],
325                    )
326                })?;
327        }
328        Ok(())
329    }
330
331    fn induc_stmt_forall_param_map(param: &str) -> HashMap<String, Obj> {
332        let mut m = HashMap::with_capacity(1);
333        m.insert(
334            param.to_string(),
335            obj_for_bound_param_in_scope(param.to_string(), ParamObjType::Forall),
336        );
337        m
338    }
339
340    fn by_induc_stmt_stored_forall_fact(&self, stmt: &ByInducStmt) -> Result<Fact, RuntimeError> {
341        let forall_map = Self::induc_stmt_forall_param_map(&stmt.param);
342        let mut then_facts: Vec<ExistOrAndChainAtomicFact> =
343            Vec::with_capacity(stmt.to_prove.len());
344        for fact in stmt.to_prove.iter() {
345            then_facts.push(self.inst_exist_or_and_chain_atomic_fact(
346                fact,
347                &forall_map,
348                ParamObjType::Forall,
349                None,
350            )?);
351        }
352        Ok(ForallFact::new(
353            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
354                vec![stmt.param.clone()],
355                ParamType::Obj(StandardSet::Z.into()),
356            )]),
357            vec![GreaterEqualFact::new(
358                obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Forall),
359                stmt.induc_from.clone(),
360                stmt.line_file.clone(),
361            )
362            .into()],
363            then_facts,
364            stmt.line_file.clone(),
365        )?
366        .into())
367    }
368
369    fn exec_by_induc_stmt_for_one_fact(
370        &mut self,
371        stmt: &ByInducStmt,
372        fact: &ExistOrAndChainAtomicFact,
373    ) -> Result<InferResult, RuntimeError> {
374        let mut infer_result = InferResult::new();
375
376        let mut base_case_param_to_arg_map: HashMap<String, Obj> = HashMap::new();
377        base_case_param_to_arg_map.insert(stmt.param.clone(), stmt.induc_from.clone());
378        let base_case_fact = self
379            .inst_exist_or_and_chain_atomic_fact(
380                fact,
381                &base_case_param_to_arg_map,
382                ParamObjType::Induc,
383                None,
384            )?
385            .to_fact();
386        self.verify_fact_return_err_if_not_true(&base_case_fact, &VerifyState::new(0, false))
387            .map_err(|verify_error| {
388                short_exec_error(
389                    stmt.clone().into(),
390                    format!("by induc: base case is not proved `{}`", base_case_fact),
391                    Some(verify_error),
392                    vec![],
393                )
394            })?;
395
396        let induc_from_in_z_fact = InFact::new(
397            stmt.induc_from.clone(),
398            StandardSet::Z.into(),
399            stmt.line_file.clone(),
400        )
401        .into();
402        let verify_induc_from_in_z_result = self
403            .verify_atomic_fact(&induc_from_in_z_fact, &VerifyState::new(0, false))
404            .map_err(|verify_error| {
405                short_exec_error(
406                    stmt.clone().into(),
407                    format!("by induc: failed to verify `{}`", induc_from_in_z_fact),
408                    Some(verify_error),
409                    vec![],
410                )
411            })?;
412        if verify_induc_from_in_z_result.is_unknown() {
413            return Err(short_exec_error(
414                stmt.clone().into(),
415                format!("by induc: failed to verify `{}`", induc_from_in_z_fact),
416                None,
417                vec![],
418            ));
419        }
420
421        let forall_bound_param =
422            obj_for_bound_param_in_scope(stmt.param.clone(), ParamObjType::Forall);
423        let forall_map = Self::induc_stmt_forall_param_map(&stmt.param);
424        let dom_p_fact = self.inst_exist_or_and_chain_atomic_fact(
425            fact,
426            &forall_map,
427            ParamObjType::Forall,
428            None,
429        )?;
430        let param_plus_one_obj = Add::new(
431            forall_bound_param.clone(),
432            Number::new("1".to_string()).into(),
433        )
434        .into();
435        let mut induction_step_param_to_obj_map: HashMap<String, Obj> = HashMap::new();
436        induction_step_param_to_obj_map.insert(stmt.param.clone(), param_plus_one_obj);
437        let next_fact_of_induction_step = self.inst_exist_or_and_chain_atomic_fact(
438            fact,
439            &induction_step_param_to_obj_map,
440            ParamObjType::Forall,
441            None,
442        )?;
443
444        let corresponding_forall_fact = ForallFact::new(
445            ParamDefWithType::new(vec![ParamGroupWithParamType::new(
446                vec![stmt.param.clone()],
447                ParamType::Obj(StandardSet::Z.into()),
448            )]),
449            vec![
450                GreaterEqualFact::new(
451                    forall_bound_param,
452                    stmt.induc_from.clone(),
453                    stmt.line_file.clone(),
454                )
455                .into(),
456                dom_p_fact.to_fact(),
457            ],
458            vec![next_fact_of_induction_step],
459            stmt.line_file.clone(),
460        )?
461        .into();
462
463        self.verify_fact_return_err_if_not_true(
464            &corresponding_forall_fact,
465            &VerifyState::new(0, false),
466        )
467        .map_err(|well_defined_error| {
468            short_exec_error(
469                stmt.clone().into(),
470                format!(
471                    "by induc: generated step forall is not well-defined `{}`",
472                    corresponding_forall_fact
473                ),
474                Some(well_defined_error),
475                vec![],
476            )
477        })?;
478
479        infer_result.new_fact(&corresponding_forall_fact);
480        Ok(infer_result)
481    }
482}
litex/execute/by_stmt/induc_by_stmt.rs

litex/execute/by_stmt/
induc_by_stmt.rs
