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::Fact(
231 uniqueness_fact.clone(),
232 "exist!: witness exist and uniqueness forall verified".to_string(),
233 ),
234 vec![],
235 );
236 Ok(Some(out.into()))
237 }
238
239 pub fn verify_exist_fact_with_known_exist_fact(
240 &mut self,
241 exist_fact: &ExistFactEnum,
242 known_exist_fact: &ExistFactEnum,
243 ) -> Result<StmtResult, RuntimeError> {
244 for environment in self.iter_environments_from_top() {
245 let result = Self::verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
246 self,
247 environment,
248 exist_fact,
249 known_exist_fact,
250 )?;
251 if result.is_true() {
252 return Ok(result);
253 }
254 }
255
256 Ok((StmtUnknown::new()).into())
257 }
258
259 pub fn verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
260 runtime: &Runtime,
261 environment: &Environment,
262 exist_fact: &ExistFactEnum,
263 known_exist_fact: &ExistFactEnum,
264 ) -> Result<StmtResult, RuntimeError> {
265 let goal_keys = Self::known_exist_lookup_keys(known_exist_fact);
266 let target_body_string = Self::exist_fact_normalized_body_string(runtime, exist_fact)
267 .map_err(|e| {
268 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
269 Some(Fact::from(exist_fact.clone()).into_stmt()),
270 String::new(),
271 exist_fact.line_file(),
272 Some(e),
273 vec![],
274 )))
275 })?;
276 for key in goal_keys.iter() {
277 let Some(known_exist_facts) = environment.known_exist_facts.get(key) else {
278 continue;
279 };
280 for known_fact in known_exist_facts.iter() {
281 if !known_fact.can_be_used_to_verify_goal(exist_fact) {
282 continue;
283 }
284 let known_body_string =
285 Self::exist_fact_normalized_body_string(runtime, known_fact).map_err(|e| {
286 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
287 Some(Fact::from(exist_fact.clone()).into_stmt()),
288 String::new(),
289 exist_fact.line_file(),
290 Some(e),
291 vec![],
292 )))
293 })?;
294 if target_body_string == known_body_string {
295 return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
296 exist_fact.clone().into(),
297 VerifiedByResult::Fact(known_fact.clone().into(), known_fact.to_string()),
298 Vec::new(),
299 ))
300 .into());
301 }
302 }
303 }
304
305 Ok((StmtUnknown::new()).into())
306 }
307
308 fn known_exist_lookup_keys(goal: &ExistFactEnum) -> Vec<String> {
309 let mut keys = vec![goal.key()];
310 if let ExistFactEnum::ExistFact(body) = goal {
311 keys.push(ExistFactEnum::ExistUniqueFact(body.clone()).key());
312 }
313 keys.sort();
314 keys.dedup();
315 keys
316 }
317
318 fn exist_fact_normalized_body_string(
319 runtime: &Runtime,
320 exist_fact: &ExistFactEnum,
321 ) -> Result<String, RuntimeError> {
322 let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
323 let mut normalized_params: Vec<ParamGroupWithParamType> = Vec::new();
324 let mut param_index: usize = 0;
325
326 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
327 let mut new_param_names: Vec<String> = Vec::new();
328 for original_name in param_def_with_type.params.iter() {
329 let normalized_name = format!("#{}", param_index);
330 param_index += 1;
331
332 param_to_arg_map.insert(
333 original_name.clone(),
334 obj_for_bound_param_in_scope(normalized_name.clone(), ParamObjType::Exist),
335 );
336 new_param_names.push(normalized_name);
337 }
338
339 let instantiated_param_type = runtime.inst_param_type(
340 ¶m_def_with_type.param_type,
341 ¶m_to_arg_map,
342 ParamObjType::Exist,
343 )?;
344 normalized_params.push(ParamGroupWithParamType::new(
345 new_param_names,
346 instantiated_param_type,
347 ));
348 }
349
350 let instantiated_exist_fact =
351 runtime.inst_exist_fact(exist_fact, ¶m_to_arg_map, ParamObjType::Exist, None)?;
352
353 let mut fact_strings: Vec<String> = Vec::new();
354 for fact in instantiated_exist_fact.facts().iter() {
355 let fact_as_fact = fact.from_ref_to_cloned_fact();
356 fact_strings.push(fact_as_fact.to_string());
357 }
358
359 let mut params_string_parts: Vec<String> = Vec::new();
360 for param_def_with_type in normalized_params.iter() {
361 params_string_parts.push(format!(
362 "{} {}",
363 param_def_with_type.params.join(","),
364 param_def_with_type.param_type
365 ));
366 }
367 let params_string = params_string_parts.join("; ");
368 let facts_string = fact_strings.join("; ");
369 Ok(format!("{} || {}", params_string, facts_string))
370 }
371}
372
373fn stmt_result_infers(result: &StmtResult) -> InferResult {
374 match result {
375 StmtResult::FactualStmtSuccess(x) => x.infers.clone(),
376 StmtResult::NonFactualStmtSuccess(x) => x.infers.clone(),
377 StmtResult::StmtUnknown(_) => InferResult::new(),
378 }
379}