1use crate::prelude::*;
2use std::collections::HashMap;
3use std::result::Result;
4
5impl Runtime {
6 pub fn verify_exist_fact(
7 &mut self,
8 exist_fact: &ExistFactEnum,
9 verify_state: &VerifyState,
10 ) -> Result<StmtResult, RuntimeError> {
11 if let Some(cached_result) =
12 self.verify_fact_from_cache_using_display_string(&exist_fact.clone().into())
13 {
14 return Ok(cached_result);
15 }
16
17 if !verify_state.well_defined_already_verified {
18 if let Err(e) = self.verify_exist_fact_well_defined(exist_fact, verify_state) {
19 return Err({
20 VerifyRuntimeError(RuntimeErrorStruct::new(
21 Some(Fact::from(exist_fact.clone()).into_stmt()),
22 String::new(),
23 exist_fact.line_file(),
24 Some(e),
25 vec![],
26 ))
27 .into()
28 });
29 }
30 }
31
32 let result = self.verify_exist_fact_with_known_exist_fact(exist_fact, exist_fact)?;
33 if result.is_true() {
34 return Ok(result);
35 }
36
37 if verify_state.is_round_0() {
38 let result = self.verify_exist_fact_with_known_forall(exist_fact, verify_state)?;
39 if result.is_true() {
40 return Ok(result);
41 }
42
43 if exist_fact.is_exist_unique() {
44 if let Some(proved) = self.try_verify_exist_unique_by_exist_and_uniqueness_forall(
45 exist_fact,
46 verify_state,
47 )? {
48 return Ok(proved);
49 }
50 }
51 }
52
53 Ok((StmtUnknown::new()).into())
54 }
55
56 pub(crate) fn build_exist_unique_uniqueness_forall_fact(
57 &self,
58 exist_fact: &ExistFactEnum,
59 ) -> Result<ForallFact, RuntimeError> {
60 let lf = exist_fact.line_file();
61 let flat_orig = exist_fact.params_def_with_type().collect_param_names();
62 let n = flat_orig.len();
63 let flat_a: Vec<String> = flat_orig.iter().map(|name| format!("{}1", name)).collect();
64 let flat_b: Vec<String> = flat_orig.iter().map(|name| format!("{}2", name)).collect();
65
66 let mut map_running_a: HashMap<String, Obj> = HashMap::new();
67 let mut map_running_b: HashMap<String, Obj> = HashMap::new();
68 let mut forall_groups: Vec<ParamGroupWithParamType> = Vec::new();
69 for group in exist_fact.params_def_with_type().groups.iter() {
70 let chunk_a: Vec<String> = group
71 .params
72 .iter()
73 .map(|name| format!("{}1", name))
74 .collect();
75 for (orig, nm) in group.params.iter().zip(chunk_a.iter()) {
76 map_running_a.insert(
77 orig.clone(),
78 obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
79 );
80 }
81 let pt_a =
82 self.inst_param_type(&group.param_type, &map_running_a, ParamObjType::Forall)?;
83 forall_groups.push(ParamGroupWithParamType::new(chunk_a, pt_a));
84 }
85 for group in exist_fact.params_def_with_type().groups.iter() {
86 let chunk_b: Vec<String> = group
87 .params
88 .iter()
89 .map(|name| format!("{}2", name))
90 .collect();
91 for (orig, nm) in group.params.iter().zip(chunk_b.iter()) {
92 map_running_b.insert(
93 orig.clone(),
94 obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
95 );
96 }
97 let pt_b =
98 self.inst_param_type(&group.param_type, &map_running_b, ParamObjType::Forall)?;
99 forall_groups.push(ParamGroupWithParamType::new(chunk_b, pt_b));
100 }
101
102 let map_a: HashMap<String, Obj> = flat_orig
103 .iter()
104 .cloned()
105 .zip(
106 flat_a
107 .iter()
108 .cloned()
109 .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
110 )
111 .collect();
112 let map_b: HashMap<String, Obj> = flat_orig
113 .iter()
114 .cloned()
115 .zip(
116 flat_b
117 .iter()
118 .cloned()
119 .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
120 )
121 .collect();
122
123 let mut dom_facts: Vec<Fact> = Vec::new();
126 for inner in exist_fact.facts().iter() {
127 let f_a = self.inst_exist_body_fact(inner, &map_a, ParamObjType::Exist, None)?;
128 dom_facts.push(f_a.to_fact());
129 }
130 for inner in exist_fact.facts().iter() {
131 let f_b = self.inst_exist_body_fact(inner, &map_b, ParamObjType::Exist, None)?;
132 dom_facts.push(f_b.to_fact());
133 }
134
135 let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
136 if n == 1 {
137 let eq = EqualFact::new(
138 obj_for_bound_param_in_scope(flat_a[0].clone(), ParamObjType::Forall),
139 obj_for_bound_param_in_scope(flat_b[0].clone(), ParamObjType::Forall),
140 lf.clone(),
141 );
142 then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
143 } else {
144 let left_tuple: Obj = Tuple::new(
145 flat_a
146 .iter()
147 .cloned()
148 .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
149 .collect::<Vec<Obj>>(),
150 )
151 .into();
152 let right_tuple: Obj = Tuple::new(
153 flat_b
154 .iter()
155 .cloned()
156 .map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
157 .collect::<Vec<Obj>>(),
158 )
159 .into();
160 let eq = EqualFact::new(left_tuple, right_tuple, lf.clone());
161 then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
162 }
163
164 let forall_fact = ForallFact::new(
165 ParamDefWithType::new(forall_groups),
166 dom_facts,
167 then_facts,
168 lf,
169 )?;
170
171 let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
172 for group in forall_fact.params_def_with_type.groups.iter() {
173 for param in group.params.iter() {
174 param_to_arg_map
175 .insert(param.clone(), ForallFreeParamObj::new(param.clone()).into());
176 }
177 }
178
179 let forall_fact = self.inst_fact(
180 &forall_fact.into(),
181 ¶m_to_arg_map,
182 ParamObjType::Forall,
183 None,
184 )?;
185
186 match forall_fact {
187 Fact::ForallFact(x) => Ok(x.clone()),
188 _ => {
189 unreachable!();
190 }
191 }
192 }
193
194 fn try_verify_exist_unique_by_exist_and_uniqueness_forall(
195 &mut self,
196 exist_fact: &ExistFactEnum,
197 verify_state: &VerifyState,
198 ) -> Result<Option<StmtResult>, RuntimeError> {
199 if exist_fact.params_def_with_type().number_of_params() == 0 {
200 return Ok(None);
201 }
202 let plain = ExistFactEnum::ExistFact(ExistFactBody::new(
203 exist_fact.params_def_with_type().clone(),
204 exist_fact.facts().clone(),
205 exist_fact.line_file(),
206 )?);
207 let wd_ok = verify_state.make_state_with_req_ok_set_to_true();
208 let plain_res = self.verify_exist_fact(&plain, &wd_ok)?;
209 if !plain_res.is_true() {
210 return Ok(None);
211 }
212
213 let uniqueness_forall = self.build_exist_unique_uniqueness_forall_fact(exist_fact)?;
214
215 let uniqueness_fact: Fact = uniqueness_forall.clone().into();
216 let uniq_res = self.verify_fact(&uniqueness_fact, &wd_ok)?;
217 if !uniq_res.is_true() {
218 return Ok(None);
219 }
220
221 let mut infers = InferResult::new();
222 infers.new_fact(&exist_fact.clone().into());
223 infers.new_infer_result_inside(stmt_result_infers(&plain_res));
224 infers.new_infer_result_inside(stmt_result_infers(&uniq_res));
225 infers.new_fact(&uniqueness_fact);
226
227 let out = FactualStmtSuccess::new_with_verified_by_known_fact_and_infer(
228 exist_fact.clone().into(),
229 infers,
230 VerifiedByResult::cited_fact(
231 exist_fact.clone().into(),
232 uniqueness_fact.clone(),
233 Some("exist!: witness exist and uniqueness forall verified".to_string()),
234 ),
235 vec![],
236 );
237 Ok(Some(out.into()))
238 }
239
240 pub fn verify_exist_fact_with_known_exist_fact(
241 &mut self,
242 exist_fact: &ExistFactEnum,
243 known_exist_fact: &ExistFactEnum,
244 ) -> Result<StmtResult, RuntimeError> {
245 for environment in self.iter_environments_from_top() {
246 let result = Self::verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
247 self,
248 environment,
249 exist_fact,
250 known_exist_fact,
251 )?;
252 if result.is_true() {
253 return Ok(result);
254 }
255 }
256
257 Ok((StmtUnknown::new()).into())
258 }
259
260 pub fn verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
261 runtime: &Runtime,
262 environment: &Environment,
263 exist_fact: &ExistFactEnum,
264 known_exist_fact: &ExistFactEnum,
265 ) -> Result<StmtResult, RuntimeError> {
266 let goal_keys = Self::known_exist_lookup_keys(known_exist_fact);
267 let target_body_string = Self::exist_fact_normalized_body_string(runtime, exist_fact)
268 .map_err(|e| {
269 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
270 Some(Fact::from(exist_fact.clone()).into_stmt()),
271 String::new(),
272 exist_fact.line_file(),
273 Some(e),
274 vec![],
275 )))
276 })?;
277 for key in goal_keys.iter() {
278 let Some(known_exist_facts) = environment.known_exist_facts.get(key) else {
279 continue;
280 };
281 for known_fact in known_exist_facts.iter() {
282 if !known_fact.can_be_used_to_verify_goal(exist_fact) {
283 continue;
284 }
285 let known_body_string =
286 Self::exist_fact_normalized_body_string(runtime, known_fact).map_err(|e| {
287 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
288 Some(Fact::from(exist_fact.clone()).into_stmt()),
289 String::new(),
290 exist_fact.line_file(),
291 Some(e),
292 vec![],
293 )))
294 })?;
295 if target_body_string == known_body_string {
296 return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
297 exist_fact.clone().into(),
298 VerifiedByResult::cited_fact(
299 exist_fact.clone().into(),
300 known_fact.clone().into(),
301 None,
302 ),
303 Vec::new(),
304 ))
305 .into());
306 }
307 }
308 }
309
310 Ok((StmtUnknown::new()).into())
311 }
312
313 fn known_exist_lookup_keys(goal: &ExistFactEnum) -> Vec<String> {
314 let mut keys = vec![goal.key()];
315 if let ExistFactEnum::ExistFact(body) = goal {
316 keys.push(ExistFactEnum::ExistUniqueFact(body.clone()).key());
317 }
318 keys.sort();
319 keys.dedup();
320 keys
321 }
322
323 fn exist_fact_normalized_body_string(
324 runtime: &Runtime,
325 exist_fact: &ExistFactEnum,
326 ) -> Result<String, RuntimeError> {
327 let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
328 let mut normalized_params: Vec<ParamGroupWithParamType> = Vec::new();
329 let mut param_index: usize = 0;
330
331 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
332 let mut new_param_names: Vec<String> = Vec::new();
333 for original_name in param_def_with_type.params.iter() {
334 let normalized_name = format!("#{}", param_index);
335 param_index += 1;
336
337 param_to_arg_map.insert(
338 original_name.clone(),
339 obj_for_bound_param_in_scope(normalized_name.clone(), ParamObjType::Exist),
340 );
341 new_param_names.push(normalized_name);
342 }
343
344 let instantiated_param_type = runtime.inst_param_type(
345 ¶m_def_with_type.param_type,
346 ¶m_to_arg_map,
347 ParamObjType::Exist,
348 )?;
349 normalized_params.push(ParamGroupWithParamType::new(
350 new_param_names,
351 instantiated_param_type,
352 ));
353 }
354
355 let instantiated_exist_fact =
356 runtime.inst_exist_fact(exist_fact, ¶m_to_arg_map, ParamObjType::Exist, None)?;
357
358 let mut fact_strings: Vec<String> = Vec::new();
359 for fact in instantiated_exist_fact.facts().iter() {
360 let fact_as_fact = fact.from_ref_to_cloned_fact();
361 fact_strings.push(fact_as_fact.to_string());
362 }
363
364 let mut params_string_parts: Vec<String> = Vec::new();
365 for param_def_with_type in normalized_params.iter() {
366 params_string_parts.push(format!(
367 "{} {}",
368 param_def_with_type.params.join(","),
369 param_def_with_type.param_type
370 ));
371 }
372 let params_string = params_string_parts.join("; ");
373 let facts_string = fact_strings.join("; ");
374 Ok(format!("{} || {}", params_string, facts_string))
375 }
376}
377
378fn stmt_result_infers(result: &StmtResult) -> InferResult {
379 match result {
380 StmtResult::FactualStmtSuccess(x) => x.infers.clone(),
381 StmtResult::NonFactualStmtSuccess(x) => x.infers.clone(),
382 StmtResult::StmtUnknown(_) => InferResult::new(),
383 }
384}