litex/verify/verify_builtin_rules/
equality_dispatch.rs1use crate::prelude::*;
2use crate::verify::verify_equality_by_builtin_rules::{
3 factual_equal_success_by_builtin_reason, verify_equality_by_they_are_the_same,
4};
5
6impl Runtime {
7 pub fn verify_equality_by_builtin_rules(
8 &mut self,
9 left: &Obj,
10 right: &Obj,
11 line_file: LineFile,
12 verify_state: &VerifyState,
13 ) -> Result<StmtResult, RuntimeError> {
14 if verify_equality_by_they_are_the_same(left, right) {
15 return Ok(factual_equal_success_by_builtin_reason(
16 left,
17 right,
18 line_file,
19 "they are the same",
20 )
21 .into());
22 }
23
24 if let Obj::ObjAsStructInstanceWithFieldAccess(field_access) = left {
25 let projected = self.struct_field_access_projection(field_access)?;
26 let projected_result = self.verify_equality_by_builtin_rules(
27 &projected,
28 right,
29 line_file.clone(),
30 verify_state,
31 )?;
32 if projected_result.is_true() {
33 return Ok(
34 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
35 EqualFact::new(left.clone(), right.clone(), line_file).into(),
36 "struct field access is the corresponding tuple projection".to_string(),
37 vec![projected_result],
38 )
39 .into(),
40 );
41 }
42 }
43 if let Obj::ObjAsStructInstanceWithFieldAccess(field_access) = right {
44 let projected = self.struct_field_access_projection(field_access)?;
45 let projected_result = self.verify_equality_by_builtin_rules(
46 left,
47 &projected,
48 line_file.clone(),
49 verify_state,
50 )?;
51 if projected_result.is_true() {
52 return Ok(
53 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
54 EqualFact::new(left.clone(), right.clone(), line_file).into(),
55 "struct field access is the corresponding tuple projection".to_string(),
56 vec![projected_result],
57 )
58 .into(),
59 );
60 }
61 }
62
63 if let Some(done) = self.try_verify_objs_equal_by_expanding_family(
64 left,
65 right,
66 line_file.clone(),
67 verify_state,
68 )? {
69 return Ok(done);
70 }
71
72 if let Some(done) =
73 self.try_verify_abs_equalities(left, right, line_file.clone(), verify_state)?
74 {
75 return Ok(done);
76 }
77
78 if let Some(done) = self.try_verify_zero_equals_subtraction_implies_equal_operands(
79 left,
80 right,
81 line_file.clone(),
82 verify_state,
83 )? {
84 return Ok(done);
85 }
86
87 if let Some(done) = self.try_verify_zero_equals_pow_from_base_zero(
88 left,
89 right,
90 line_file.clone(),
91 verify_state,
92 )? {
93 return Ok(done);
94 }
95
96 if let Some(done) =
97 self.try_verify_pow_one_identity(left, right, line_file.clone(), verify_state)?
98 {
99 return Ok(done);
100 }
101
102 if let Some(done) = self.try_verify_power_addition_exponent_rule(
103 left,
104 right,
105 line_file.clone(),
106 verify_state,
107 )? {
108 return Ok(done);
109 }
110
111 if let Some(done) = self.try_verify_same_algebra_context_by_equal_args(
112 left,
113 right,
114 line_file.clone(),
115 verify_state,
116 )? {
117 return Ok(done);
118 }
119
120 if let Some(done) =
121 self.try_verify_log_identity_equalities(left, right, line_file.clone(), verify_state)?
122 {
123 return Ok(done);
124 }
125
126 if let Some(done) =
127 self.try_verify_log_algebra_identities(left, right, line_file.clone(), verify_state)?
128 {
129 return Ok(done);
130 }
131
132 if let Some(done) =
133 self.try_verify_log_equals_by_pow_inverse(left, right, line_file.clone(), verify_state)?
134 {
135 return Ok(done);
136 }
137
138 if let Some(done) =
139 self.try_verify_sum_additivity(left, right, line_file.clone(), verify_state)?
140 {
141 return Ok(done);
142 }
143
144 if let Some(done) =
145 self.try_verify_sum_merge_adjacent_ranges(left, right, line_file.clone(), verify_state)?
146 {
147 return Ok(done);
148 }
149
150 if let Some(done) =
151 self.try_verify_sum_split_last_term(left, right, line_file.clone(), verify_state)?
152 {
153 return Ok(done);
154 }
155
156 if let Some(done) =
157 self.try_verify_product_split_last_term(left, right, line_file.clone(), verify_state)?
158 {
159 return Ok(done);
160 }
161
162 if let Some(done) = self.try_verify_sum_partition_adjacent_ranges(
163 left,
164 right,
165 line_file.clone(),
166 verify_state,
167 )? {
168 return Ok(done);
169 }
170
171 if let Some(done) = self.try_verify_product_partition_adjacent_ranges(
172 left,
173 right,
174 line_file.clone(),
175 verify_state,
176 )? {
177 return Ok(done);
178 }
179
180 if let Some(done) =
181 self.try_verify_sum_reindex_shift(left, right, line_file.clone(), verify_state)?
182 {
183 return Ok(done);
184 }
185
186 if let Some(done) =
187 self.try_verify_sum_constant_summand(left, right, line_file.clone(), verify_state)?
188 {
189 return Ok(done);
190 }
191
192 if let Some(done) = self.try_verify_mod_nested_same_modulus_absorption(
193 left,
194 right,
195 line_file.clone(),
196 verify_state,
197 )? {
198 return Ok(done);
199 }
200
201 if let Some(done) = self.try_verify_zero_mod_equals_zero(left, right, line_file.clone())? {
202 return Ok(done);
203 }
204
205 if let Some(done) = self.try_verify_mod_one_equals_zero(left, right, line_file.clone())? {
206 return Ok(done);
207 }
208
209 if let Some(done) = self.try_verify_mod_peel_nested_same_modulus(
210 left,
211 right,
212 line_file.clone(),
213 verify_state,
214 )? {
215 return Ok(done);
216 }
217
218 if let Some(done) = self.try_verify_mod_congruence_from_inner_binary(
219 left,
220 right,
221 line_file.clone(),
222 verify_state,
223 )? {
224 return Ok(done);
225 }
226
227 let (result, calculated_left, calculated_right) = self
228 .verify_equality_by_they_are_the_same_and_calculation(
229 left,
230 right,
231 line_file.clone(),
232 verify_state,
233 )?;
234 if result.is_true() {
235 return Ok(result);
236 }
237
238 if objs_equal_by_rational_expression_evaluation(&left, &right) {
239 return Ok(
240 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
241 EqualFact::new(left.clone(), right.clone(), line_file).into(),
242 "calculation and rational expression simplification".to_string(),
243 Vec::new(),
244 ))
245 .into(),
246 );
247 }
248
249 if objs_equal_by_rational_expression_evaluation(&calculated_left, &calculated_right) {
250 return Ok(
251 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
252 EqualFact::new(left.clone(), right.clone(), line_file).into(),
253 "calculation and rational expression simplification".to_string(),
254 Vec::new(),
255 ))
256 .into(),
257 );
258 }
259
260 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
261 left,
262 right,
263 left,
264 right,
265 line_file.clone(),
266 verify_state,
267 )? {
268 return Ok(done);
269 }
270 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
271 left,
272 right,
273 right,
274 left,
275 line_file.clone(),
276 verify_state,
277 )? {
278 return Ok(done);
279 }
280
281 if let (Obj::FnSet(left_fn_set), Obj::FnSet(right_fn_set)) = (left, right) {
282 return self.verify_fn_set_with_params_equality_by_builtin_rules(
283 left_fn_set,
284 right_fn_set,
285 line_file,
286 verify_state,
287 );
288 }
289
290 if let (Obj::AnonymousFn(l), Obj::AnonymousFn(r)) = (left, right) {
291 if l.to_string() == r.to_string() {
292 return Ok(
293 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
294 EqualFact::new(left.clone(), right.clone(), line_file).into(),
295 "anonymous fn: identical surface syntax (params, dom, ret, body)"
296 .to_string(),
297 Vec::new(),
298 ))
299 .into(),
300 );
301 }
302 }
303
304 Ok((StmtUnknown::new()).into())
305 }
306}