litex/execute/
exec_witness_stmt.rs1use crate::prelude::*;
2
3impl Runtime {
4 pub fn exec_witness_exist_fact(
5 &mut self,
6 stmt: &WitnessExistFact,
7 ) -> Result<StmtResult, RuntimeError> {
8 let witness_stmt = stmt.clone().into();
9
10 let inside_results_when_verify = self.run_in_local_env(|rt| {
11 let witness_stmt = stmt.clone().into();
12 let verify_state_for_well_defined = VerifyState::new(0, false);
13
14 let expected_param_count = stmt
15 .exist_fact_in_witness
16 .params_def_with_type()
17 .number_of_params();
18 if expected_param_count != stmt.equal_tos.len() {
19 return Err(short_exec_error(
20 witness_stmt,
21 "witness exist fact: parameter count mismatch",
22 None,
23 vec![],
24 ));
25 }
26
27 if let Err(well_defined_error) = rt.verify_exist_fact_well_defined(
28 &stmt.exist_fact_in_witness,
29 &verify_state_for_well_defined,
30 ) {
31 return Err(short_exec_error(
32 witness_stmt,
33 "witness exist fact: exist fact well-defined failed",
34 Some(well_defined_error),
35 vec![],
36 ));
37 }
38
39 for equal_to_obj in stmt.equal_tos.iter() {
40 if let Err(well_defined_error) = rt.verify_obj_well_defined_and_store_cache(
41 equal_to_obj,
42 &verify_state_for_well_defined,
43 ) {
44 return Err(short_exec_error(
45 witness_stmt,
46 "witness exist fact: equal_to well-defined failed",
47 Some(well_defined_error),
48 vec![],
49 ));
50 }
51 }
52
53 let have_obj_equal_stmt = HaveObjEqualStmt::new(
54 stmt.exist_fact_in_witness.params_def_with_type().clone(),
55 stmt.equal_tos.clone(),
56 stmt.line_file.clone(),
57 );
58
59 match rt.exec_have_obj_equal_stmt(&have_obj_equal_stmt) {
60 Ok(_binding_result) => {}
61 Err(exec_stmt_error) => {
62 return Err(exec_stmt_error);
63 }
64 }
65
66 for proof_stmt in stmt.proof.iter() {
67 if let Err(proof_exec_error) = rt.exec_stmt(proof_stmt) {
68 return Err(short_exec_error(
69 witness_stmt.clone(),
70 proof_stmt.to_string(),
71 Some(proof_exec_error),
72 vec![],
73 ));
74 }
75 }
76
77 let param_to_obj_map = stmt
78 .exist_fact_in_witness
79 .params_def_with_type()
80 .param_defs_and_args_to_param_to_arg_map(stmt.equal_tos.as_slice());
81 let instantiated_exist_fact = rt.inst_exist_fact(
82 &stmt.exist_fact_in_witness,
83 ¶m_to_obj_map,
84 ParamObjType::Exist,
85 None,
86 )?;
87
88 let verify_state_for_proof_check = VerifyState::new(0, false);
89 for internal_fact_template in instantiated_exist_fact.facts().iter() {
90 let internal_fact = internal_fact_template.clone().to_fact();
91 let verification_result = rt.verify_fact_return_err_if_not_true(
92 &internal_fact,
93 &verify_state_for_proof_check,
94 );
95 if let Err(verify_error) = verification_result {
96 return Err(verify_error);
97 }
98 }
99
100 Ok(())
101 });
102
103 if let Err(e) = inside_results_when_verify {
104 return Err(e);
105 }
106
107 let store_result = self.verify_well_defined_and_store_and_infer_with_default_verify_state(
109 stmt.exist_fact_in_witness.clone().into(),
110 );
111 match store_result {
112 Ok(infer_result) => {
113 Ok((NonFactualStmtSuccess::new(witness_stmt, infer_result, vec![])).into())
114 }
115 Err(store_error) => Err(short_exec_error(
116 witness_stmt,
117 "witness exist fact: failed to store exist fact",
118 Some(store_error),
119 vec![],
120 )),
121 }
122 }
123
124 pub fn exec_witness_nonempty_set(
125 &mut self,
126 stmt: &WitnessNonemptySet,
127 ) -> Result<StmtResult, RuntimeError> {
128 let witness_stmt = stmt.clone().into();
129
130 let inside_results_when_verify = self.run_in_local_env(|rt| {
131 let witness_stmt = stmt.clone().into();
132
133 let verify_state_for_well_defined = VerifyState::new(0, false);
134
135 if let Err(well_defined_error) = rt
136 .verify_obj_well_defined_and_store_cache(&stmt.obj, &verify_state_for_well_defined)
137 {
138 return Err(short_exec_error(
139 witness_stmt,
140 "witness nonempty set: obj well-defined failed",
141 Some(well_defined_error),
142 vec![],
143 ));
144 }
145
146 if let Err(well_defined_error) = rt
147 .verify_obj_well_defined_and_store_cache(&stmt.set, &verify_state_for_well_defined)
148 {
149 return Err(short_exec_error(
150 witness_stmt.clone(),
151 "witness nonempty set: set well-defined failed",
152 Some(well_defined_error),
153 vec![],
154 ));
155 }
156
157 for proof_stmt in stmt.proof.iter() {
158 if let Err(proof_exec_error) = rt.exec_stmt(proof_stmt) {
159 return Err(short_exec_error(
160 witness_stmt.clone(),
161 proof_stmt.to_string(),
162 Some(proof_exec_error),
163 vec![],
164 ));
165 }
166 }
167
168 let verify_state_for_proof_check = VerifyState::new(0, false);
169 if let Obj::FnSet(fn_set) = &stmt.set {
170 let ret_nonempty_fact = IsNonemptySetFact::new(
171 fn_set.body.ret_set.as_ref().clone(),
172 stmt.line_file.clone(),
173 )
174 .into();
175 let ret_check = rt.verify_non_equational_atomic_fact_with_builtin_rules(
176 &ret_nonempty_fact,
177 &verify_state_for_proof_check,
178 )?;
179 if ret_check.is_true() {
180 return Ok(());
181 }
182 }
183
184 let membership_fact =
185 InFact::new(stmt.obj.clone(), stmt.set.clone(), stmt.line_file.clone()).into();
186 rt.verify_fact_return_err_if_not_true(&membership_fact, &verify_state_for_proof_check)?;
187
188 Ok(())
189 });
190
191 if let Err(e) = inside_results_when_verify {
192 return Err(e);
193 }
194
195 let store_result = self.verify_well_defined_and_store_and_infer_with_default_verify_state(
197 IsNonemptySetFact::new(stmt.set.clone(), stmt.line_file.clone()).into(),
198 );
199 match store_result {
200 Ok(infer_result) => {
201 Ok((NonFactualStmtSuccess::new(witness_stmt, infer_result, vec![])).into())
202 }
203 Err(store_error) => Err(short_exec_error(
204 witness_stmt,
205 "witness nonempty set: failed to store nonempty set fact",
206 Some(store_error),
207 vec![],
208 )),
209 }
210 }
211}