litex/execute/by_stmt/
extension_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_by_extension_stmt(
5        &mut self,
6        stmt: &ByExtensionStmt,
7    ) -> Result<StmtResult, RuntimeError> {
8        self.verify_obj_well_defined_and_store_cache(&stmt.left, &VerifyState::new(0, false))
9            .map_err(|well_defined_error| {
10                short_exec_error(
11                    stmt.clone().into(),
12                    format!("by extension: left set `{}` is not well-defined", stmt.left),
13                    Some(well_defined_error),
14                    vec![],
15                )
16            })?;
17        self.verify_obj_well_defined_and_store_cache(&stmt.right, &VerifyState::new(0, false))
18            .map_err(|well_defined_error| {
19                short_exec_error(
20                    stmt.clone().into(),
21                    format!(
22                        "by extension: right set `{}` is not well-defined",
23                        stmt.right
24                    ),
25                    Some(well_defined_error),
26                    vec![],
27                )
28            })?;
29
30        let local_proof_result: Result<(Vec<StmtResult>, Fact, Fact), RuntimeError> = self
31            .run_in_local_env(|rt| {
32                let mut inside_results: Vec<StmtResult> = Vec::new();
33                for proof_stmt in stmt.proof.iter() {
34                    let one_proof_stmt_exec_result =
35                        rt.exec_stmt(proof_stmt).map_err(|stmt_error| {
36                            short_exec_error(
37                                stmt.clone().into(),
38                                format!(
39                                    "by extension: failed to execute proof stmt `{}`",
40                                    proof_stmt
41                                ),
42                                Some(stmt_error),
43                                vec![],
44                            )
45                        })?;
46                    inside_results.push(one_proof_stmt_exec_result);
47                }
48
49                let unused_name = rt.generate_random_unused_name();
50
51                let left_to_right_forall_fact = ForallFact::new(
52                    ParamDefWithType::new(vec![ParamGroupWithParamType::new(
53                        vec![unused_name.clone()],
54                        ParamType::Obj(stmt.left.clone()),
55                    )]),
56                    vec![],
57                    vec![InFact::new(
58                        obj_for_bound_param_in_scope(unused_name.clone(), ParamObjType::Forall),
59                        stmt.right.clone(),
60                        stmt.line_file.clone(),
61                    )
62                    .into()],
63                    stmt.line_file.clone(),
64                )?
65                .into();
66                rt.verify_fact_return_err_if_not_true(
67                    &left_to_right_forall_fact,
68                    &VerifyState::new(0, false),
69                )
70                .map_err(|verify_error| {
71                    short_exec_error(
72                        stmt.clone().into(),
73                        format!(
74                            "by extension: failed to prove left subset right `{}`",
75                            left_to_right_forall_fact
76                        ),
77                        Some(verify_error),
78                        vec![],
79                    )
80                })?;
81
82                let right_to_left_forall_fact = ForallFact::new(
83                    ParamDefWithType::new(vec![ParamGroupWithParamType::new(
84                        vec![unused_name.clone()],
85                        ParamType::Obj(stmt.right.clone()),
86                    )]),
87                    vec![],
88                    vec![InFact::new(
89                        obj_for_bound_param_in_scope(unused_name.clone(), ParamObjType::Forall),
90                        stmt.left.clone(),
91                        stmt.line_file.clone(),
92                    )
93                    .into()],
94                    stmt.line_file.clone(),
95                )?
96                .into();
97                rt.verify_fact_return_err_if_not_true(
98                    &right_to_left_forall_fact,
99                    &VerifyState::new(0, false),
100                )
101                .map_err(|verify_error| {
102                    short_exec_error(
103                        stmt.clone().into(),
104                        format!(
105                            "by extension: failed to prove right subset left `{}`",
106                            right_to_left_forall_fact
107                        ),
108                        Some(verify_error),
109                        vec![],
110                    )
111                })?;
112
113                Ok::<_, RuntimeError>((
114                    inside_results,
115                    left_to_right_forall_fact,
116                    right_to_left_forall_fact,
117                ))
118            });
119        let local_proof_result = local_proof_result?;
120        let (inside_results, _, _) = local_proof_result;
121
122        let left_equal_to_right_atomic_fact = AtomicFact::EqualFact(EqualFact::new(
123            stmt.left.clone(),
124            stmt.right.clone(),
125            stmt.line_file.clone(),
126        ));
127
128        let mut infer_result = InferResult::new();
129        infer_result.new_infer_result_inside(
130            self.store_atomic_fact_without_well_defined_verified_and_infer(
131                left_equal_to_right_atomic_fact,
132            )?,
133        );
134
135        Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, inside_results)).into())
136    }
137}
litex/execute/by_stmt/extension_by_stmt.rs

litex/execute/by_stmt/
extension_by_stmt.rs
