litex/execute/
exec_have_fn_by_forall_exist_unique.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3
4use super::exec_have_fn_equal_shared::build_function_obj_with_param_names;
5
6struct HaveFnByForallExistUniqueShape {
7    fn_set_clause: FnSetClause,
8    witness_name: String,
9    exist_body_facts: Vec<ExistBodyFact>,
10}
11
12impl Runtime {
13    pub fn exec_have_fn_by_forall_exist_unique_stmt(
14        &mut self,
15        stmt: &HaveFnByForallExistUniqueStmt,
16    ) -> Result<StmtResult, RuntimeError> {
17        let shape = self.have_fn_by_forall_exist_unique_shape(stmt)?;
18        let forall_fact: Fact = stmt.forall.clone().into();
19        self.verify_fact_return_err_if_not_true(&forall_fact, &VerifyState::new(0, false))
20            .map_err(|e| exec_stmt_error_with_stmt_and_cause(stmt.clone().into(), e))?;
21
22        let infer_result = self.exec_have_fn_by_forall_exist_unique_store_process(stmt, shape)?;
23
24        Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
25    }
26
27    fn exec_have_fn_by_forall_exist_unique_store_process(
28        &mut self,
29        stmt: &HaveFnByForallExistUniqueStmt,
30        shape: HaveFnByForallExistUniqueShape,
31    ) -> Result<InferResult, RuntimeError> {
32        let mut infer_result = InferResult::new();
33        let fn_set = self
34            .fn_set_from_fn_set_clause(&shape.fn_set_clause)
35            .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
36
37        self.store_free_param_or_identifier_name(&stmt.fn_name, ParamObjType::Identifier)
38            .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
39
40        let bind_infer = self
41            .define_parameter_by_binding_param_type(
42                &stmt.fn_name,
43                &ParamType::Obj(fn_set.clone().into()),
44                ParamObjType::Identifier,
45            )
46            .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
47        let bind_fact: Fact = InFact::new(
48            Identifier::new(stmt.fn_name.clone()).into(),
49            fn_set.clone().into(),
50            stmt.line_file.clone(),
51        )
52        .into();
53        Self::merge_have_fn_by_forall_exist_unique_infer(&mut infer_result, bind_infer, &bind_fact);
54
55        let property_forall = self.have_fn_by_forall_exist_unique_property_forall(stmt, &shape)?;
56        let property_fact = self
57            .inst_have_fn_forall_fact_for_store(property_forall)
58            .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
59        let property_infer = self
60            .verify_well_defined_and_store_and_infer_with_default_verify_state(
61                property_fact.clone(),
62            )
63            .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
64        Self::merge_have_fn_by_forall_exist_unique_infer(
65            &mut infer_result,
66            property_infer,
67            &property_fact,
68        );
69
70        Ok(infer_result)
71    }
72
73    fn have_fn_by_forall_exist_unique_shape(
74        &self,
75        stmt: &HaveFnByForallExistUniqueStmt,
76    ) -> Result<HaveFnByForallExistUniqueShape, RuntimeError> {
77        // Preconditions: the source forall must already be true; every forall parameter type must
78        // be an Obj; the forall must have exactly one then fact; that then fact must be an exist!;
79        // and the exist! must bind exactly one Obj-typed witness. Effect: define f as a set-theoretic
80        // function and store that f satisfies the witness body for each input.
81        let params_def_with_set = Self::param_groups_with_set_from_obj_param_defs(
82            stmt,
83            &stmt.forall.params_def_with_type,
84        )?;
85        if stmt.forall.then_facts.len() != 1 {
86            return Err(Self::have_fn_by_forall_exist_unique_msg(
87                stmt,
88                "forall must have exactly one then fact".to_string(),
89            ));
90        }
91
92        let exist_body = match &stmt.forall.then_facts[0] {
93            ExistOrAndChainAtomicFact::ExistFact(ExistFactEnum::ExistUniqueFact(body)) => body,
94            _ => {
95                return Err(Self::have_fn_by_forall_exist_unique_msg(
96                    stmt,
97                    "the only then fact must be an exist! fact".to_string(),
98                ));
99            }
100        };
101
102        if exist_body.params_def_with_type.number_of_params() != 1 {
103            return Err(Self::have_fn_by_forall_exist_unique_msg(
104                stmt,
105                "exist! must bind exactly one witness".to_string(),
106            ));
107        }
108
109        let mut witness_name = String::new();
110        let mut ret_set: Option<Obj> = None;
111        for group in exist_body.params_def_with_type.groups.iter() {
112            match &group.param_type {
113                ParamType::Obj(obj) => {
114                    if !group.params.is_empty() {
115                        witness_name = group.params[0].clone();
116                        ret_set = Some(obj.clone());
117                    }
118                }
119                _ => {
120                    return Err(Self::have_fn_by_forall_exist_unique_msg(
121                        stmt,
122                        "exist! witness type must be Obj".to_string(),
123                    ));
124                }
125            }
126        }
127
128        let ret_set = match ret_set {
129            Some(obj) => obj,
130            None => {
131                return Err(Self::have_fn_by_forall_exist_unique_msg(
132                    stmt,
133                    "exist! must bind exactly one witness".to_string(),
134                ));
135            }
136        };
137
138        let mut dom_facts = Vec::with_capacity(stmt.forall.dom_facts.len());
139        for dom_fact in stmt.forall.dom_facts.iter() {
140            dom_facts.push(Self::fn_set_dom_fact_from_fact(stmt, dom_fact)?);
141        }
142
143        for body_fact in exist_body.facts.iter() {
144            if matches!(body_fact, ExistBodyFact::InlineForall(_)) {
145                return Err(Self::have_fn_by_forall_exist_unique_msg(
146                    stmt,
147                    "exist! body cannot contain inline forall when defining a function".to_string(),
148                ));
149            }
150        }
151
152        Ok(HaveFnByForallExistUniqueShape {
153            fn_set_clause: FnSetClause::new(params_def_with_set, dom_facts, ret_set),
154            witness_name,
155            exist_body_facts: exist_body.facts.clone(),
156        })
157    }
158
159    fn have_fn_by_forall_exist_unique_property_forall(
160        &self,
161        stmt: &HaveFnByForallExistUniqueStmt,
162        shape: &HaveFnByForallExistUniqueShape,
163    ) -> Result<ForallFact, RuntimeError> {
164        let forall_param_names = stmt.forall.params_def_with_type.collect_param_names();
165        let function_obj = build_function_obj_with_param_names(&stmt.fn_name, &forall_param_names);
166        let mut witness_map = HashMap::new();
167        witness_map.insert(shape.witness_name.clone(), function_obj);
168
169        let mut then_facts = Vec::with_capacity(shape.exist_body_facts.len());
170        for body_fact in shape.exist_body_facts.iter() {
171            let inst_body_fact = self
172                .inst_exist_body_fact(
173                    body_fact,
174                    &witness_map,
175                    ParamObjType::Exist,
176                    Some(&stmt.line_file),
177                )
178                .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))?;
179            then_facts.push(Self::then_fact_from_exist_body_fact(stmt, inst_body_fact)?);
180        }
181
182        ForallFact::new(
183            stmt.forall.params_def_with_type.clone(),
184            stmt.forall.dom_facts.clone(),
185            then_facts,
186            stmt.line_file.clone(),
187        )
188        .map_err(|e| Self::have_fn_by_forall_exist_unique_err(stmt, e))
189    }
190
191    fn param_groups_with_set_from_obj_param_defs(
192        stmt: &HaveFnByForallExistUniqueStmt,
193        param_defs: &ParamDefWithType,
194    ) -> Result<Vec<ParamGroupWithSet>, RuntimeError> {
195        let mut result = Vec::with_capacity(param_defs.groups.len());
196        for group in param_defs.groups.iter() {
197            match &group.param_type {
198                ParamType::Obj(obj) => {
199                    result.push(ParamGroupWithSet::new(group.params.clone(), obj.clone()));
200                }
201                _ => {
202                    return Err(Self::have_fn_by_forall_exist_unique_msg(
203                        stmt,
204                        "forall parameter types must all be Obj".to_string(),
205                    ));
206                }
207            }
208        }
209        Ok(result)
210    }
211
212    fn fn_set_dom_fact_from_fact(
213        stmt: &HaveFnByForallExistUniqueStmt,
214        fact: &Fact,
215    ) -> Result<OrAndChainAtomicFact, RuntimeError> {
216        match fact {
217            Fact::AtomicFact(a) => Ok(OrAndChainAtomicFact::AtomicFact(a.clone())),
218            Fact::AndFact(a) => Ok(OrAndChainAtomicFact::AndFact(a.clone())),
219            Fact::ChainFact(c) => Ok(OrAndChainAtomicFact::ChainFact(c.clone())),
220            Fact::OrFact(o) => Ok(OrAndChainAtomicFact::OrFact(o.clone())),
221            _ => Err(Self::have_fn_by_forall_exist_unique_msg(
222                stmt,
223                "forall domain facts must be usable as fn domain facts".to_string(),
224            )),
225        }
226    }
227
228    fn then_fact_from_exist_body_fact(
229        stmt: &HaveFnByForallExistUniqueStmt,
230        fact: ExistBodyFact,
231    ) -> Result<ExistOrAndChainAtomicFact, RuntimeError> {
232        match fact {
233            ExistBodyFact::AtomicFact(a) => Ok(ExistOrAndChainAtomicFact::AtomicFact(a)),
234            ExistBodyFact::AndFact(a) => Ok(ExistOrAndChainAtomicFact::AndFact(a)),
235            ExistBodyFact::ChainFact(c) => Ok(ExistOrAndChainAtomicFact::ChainFact(c)),
236            ExistBodyFact::OrFact(o) => Ok(ExistOrAndChainAtomicFact::OrFact(o)),
237            ExistBodyFact::InlineForall(_) => Err(Self::have_fn_by_forall_exist_unique_msg(
238                stmt,
239                "exist! body cannot contain inline forall when defining a function".to_string(),
240            )),
241        }
242    }
243
244    fn merge_have_fn_by_forall_exist_unique_infer(
245        infer_result: &mut InferResult,
246        store_infer: InferResult,
247        fallback_fact: &Fact,
248    ) {
249        let empty = store_infer.is_empty();
250        infer_result.new_infer_result_inside(store_infer);
251        if empty {
252            infer_result.new_fact(fallback_fact);
253        }
254    }
255
256    fn have_fn_by_forall_exist_unique_msg(
257        stmt: &HaveFnByForallExistUniqueStmt,
258        msg: String,
259    ) -> RuntimeError {
260        short_exec_error(
261            stmt.clone().into(),
262            format!("have_fn_by_forall_exist_unique: {}", msg),
263            None,
264            vec![],
265        )
266    }
267
268    fn have_fn_by_forall_exist_unique_err(
269        stmt: &HaveFnByForallExistUniqueStmt,
270        cause: RuntimeError,
271    ) -> RuntimeError {
272        short_exec_error(
273            stmt.clone().into(),
274            "have_fn_by_forall_exist_unique failed".to_string(),
275            Some(cause),
276            vec![],
277        )
278    }
279}
litex/execute/exec_have_fn_by_forall_exist_unique.rs

litex/execute/
exec_have_fn_by_forall_exist_unique.rs
