1 | include "ASM/StatusProofsSplit.ma". |
---|
2 | |
---|
3 | include alias "arithmetics/nat.ma". |
---|
4 | include alias "basics/logic.ma". |
---|
5 | include alias "ASM/BitVectorTrie.ma". |
---|
6 | |
---|
7 | lemma fetch_many_singleton: |
---|
8 | ∀code_memory: BitVectorTrie Byte 16. |
---|
9 | ∀final_pc, start_pc: Word. |
---|
10 | ∀i: instruction. |
---|
11 | fetch_many code_memory final_pc start_pc [i] → |
---|
12 | 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory |
---|
13 | start_pc. |
---|
14 | #code_memory #final_pc #start_pc #i * #new_pc |
---|
15 | #fetch_many_assm whd in fetch_many_assm; |
---|
16 | cases (eq_bv_eq … fetch_many_assm) assumption |
---|
17 | qed. |
---|
18 | |
---|
19 | include alias "ASM/Vector.ma". |
---|
20 | include "ASM/Test.ma". |
---|
21 | |
---|
22 | lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map: |
---|
23 | ∀M, cm, ps, sigma, x. |
---|
24 | ∀addr1: [[acc_a]]. |
---|
25 | addressing_mode_ok pseudo_assembly_program M cm ps addr1=true → |
---|
26 | map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x. |
---|
27 | #M #cm #ps #sigma #x #addr1 |
---|
28 | @(subaddressing_mode_elim … addr1) |
---|
29 | whd in ⊢ (??%? → ??%?); |
---|
30 | cases (\snd M) |
---|
31 | [1: |
---|
32 | // |
---|
33 | |2: |
---|
34 | #upper_lower #address normalize nodelta #absurd |
---|
35 | destruct(absurd) |
---|
36 | ] |
---|
37 | qed. |
---|
38 | |
---|
39 | lemma addressing_mode_ok_to_snd_M_data: |
---|
40 | ∀M, cm, ps. |
---|
41 | ∀addr: [[acc_a]]. |
---|
42 | addressing_mode_ok pseudo_assembly_program M cm ps addr = true → |
---|
43 | \snd M = data. |
---|
44 | #M #addr #ps #addr |
---|
45 | @(subaddressing_mode_elim … addr) |
---|
46 | whd in ⊢ (??%? → ?); |
---|
47 | cases (\snd M) normalize nodelta |
---|
48 | [2: |
---|
49 | * #address #absurd destruct(absurd) |
---|
50 | ] |
---|
51 | #_ % |
---|
52 | qed. |
---|
53 | |
---|
54 | lemma assoc_list_exists_true_to_assoc_list_lookup_Some: |
---|
55 | ∀A, B: Type[0]. |
---|
56 | ∀e: A. |
---|
57 | ∀the_list: list (A × B). |
---|
58 | ∀eq_f: A → A → bool. |
---|
59 | assoc_list_exists A B e eq_f the_list = true → |
---|
60 | ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'. |
---|
61 | #A #B #e #the_list #eq_f elim the_list |
---|
62 | [1: |
---|
63 | whd in ⊢ (??%? → ?); #absurd destruct(absurd) |
---|
64 | |2: |
---|
65 | #hd #tl #inductive_hypothesis |
---|
66 | whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????); |
---|
67 | cases (eq_f (\fst hd) e) normalize nodelta |
---|
68 | [1: |
---|
69 | #_ %{(\snd hd)} % |
---|
70 | |2: |
---|
71 | @inductive_hypothesis |
---|
72 | ] |
---|
73 | ] |
---|
74 | qed. |
---|
75 | |
---|
76 | lemma assoc_list_exists_false_to_assoc_list_lookup_None: |
---|
77 | ∀A, B: Type[0]. |
---|
78 | ∀e, e': A. |
---|
79 | ∀the_list, the_list': list (A × B). |
---|
80 | ∀eq_f: A → A → bool. |
---|
81 | e = e' → |
---|
82 | the_list = the_list' → |
---|
83 | assoc_list_exists A B e eq_f the_list = false → |
---|
84 | assoc_list_lookup A B e' eq_f the_list' = None …. |
---|
85 | #A #B #e #e' #the_list elim the_list |
---|
86 | [1: |
---|
87 | #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ % |
---|
88 | |2: |
---|
89 | #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl |
---|
90 | whd in ⊢ (??%? → ??%?); <e_refl |
---|
91 | cases (eq_f (\fst hd) e) normalize nodelta |
---|
92 | [1: |
---|
93 | #absurd destruct(absurd) |
---|
94 | |2: |
---|
95 | >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption |
---|
96 | ] |
---|
97 | ] |
---|
98 | qed. |
---|
99 | |
---|
100 | lemma sfr_psw_eq_to_bit_address_of_register_eq: |
---|
101 | ∀A: Type[0]. |
---|
102 | ∀code_memory: A. |
---|
103 | ∀status, status', register_address. |
---|
104 | get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → |
---|
105 | bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address. |
---|
106 | #A #code_memory #status #status' #register_address #sfr_psw_refl |
---|
107 | whd in match bit_address_of_register; normalize nodelta |
---|
108 | <sfr_psw_refl % |
---|
109 | qed. |
---|
110 | |
---|
111 | lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq: |
---|
112 | ∀A: Type[0]. |
---|
113 | ∀code_memory: A. |
---|
114 | ∀status, status', register_address. |
---|
115 | get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → |
---|
116 | low_internal_ram A code_memory status = low_internal_ram A code_memory status' → |
---|
117 | get_register A code_memory status register_address = get_register A code_memory status' register_address. |
---|
118 | #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl |
---|
119 | whd in match get_register; normalize nodelta <low_internal_ram_refl |
---|
120 | >(sfr_psw_eq_to_bit_address_of_register_eq … status status') // |
---|
121 | qed. |
---|
122 | |
---|
123 | lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: |
---|
124 | ∀M', cm, status, status', sigma. |
---|
125 | ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) |
---|
126 | get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → |
---|
127 | addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → |
---|
128 | map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1. |
---|
129 | #M' #cm #status #status' #sigma #addr1 #sfr_refl |
---|
130 | @(subaddressing_mode_elim … addr1) try (#w #_ @I) |
---|
131 | [1,4: #_ @I ] #w |
---|
132 | whd in ⊢ (??%? → %); |
---|
133 | inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta |
---|
134 | [1,3: |
---|
135 | #absurd destruct(absurd) |
---|
136 | |2,4: |
---|
137 | #_ |
---|
138 | @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) |
---|
139 | <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption |
---|
140 | ] |
---|
141 | qed. |
---|
142 | |
---|
143 | lemma not_b_c_to_b_not_c: |
---|
144 | ∀b, c: bool. |
---|
145 | (¬b) = c → b = (¬c). |
---|
146 | // |
---|
147 | qed. |
---|
148 | (* XXX: move above elsewhere *) |
---|
149 | |
---|
150 | lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map: |
---|
151 | ∀M. |
---|
152 | ∀sigma. |
---|
153 | ∀sfr8051. |
---|
154 | ∀b. |
---|
155 | sfr8051 ≠ SFR_ACC_A → |
---|
156 | map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b. |
---|
157 | #M #sigma * #b |
---|
158 | [18: |
---|
159 | #relevant cases (absurd … (refl ??) relevant) |
---|
160 | ] |
---|
161 | #_ % |
---|
162 | qed. |
---|
163 | |
---|
164 | lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map: |
---|
165 | ∀M. |
---|
166 | ∀sigma: Word → Word. |
---|
167 | ∀w: BitVector 8. |
---|
168 | ∀b. |
---|
169 | w ≠ bitvector_of_nat … 224 → |
---|
170 | map_address_Byte_using_internal_pseudo_address_map M sigma w b = b. |
---|
171 | #M #sigma #w #b #w_neq_assm |
---|
172 | whd in ⊢ (??%?); inversion (sfr_of_Byte ?) |
---|
173 | [1: |
---|
174 | #sfr_of_Byte_refl % |
---|
175 | |2: |
---|
176 | * #sfr8051 #sfr_of_Byte_refl normalize nodelta try % |
---|
177 | @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map % |
---|
178 | #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl |
---|
179 | @(absurd ?? w_neq_assm) |
---|
180 | lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma |
---|
181 | whd in match sfr_of_Byte; normalize nodelta |
---|
182 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
183 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
184 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
185 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
186 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
187 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
188 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
189 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
190 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
191 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
192 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
193 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
194 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
195 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
196 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
197 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
198 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
199 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
200 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
201 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
202 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
203 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
204 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
205 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
206 | @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ] |
---|
207 | cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] |
---|
208 | #absurd destruct(absurd) |
---|
209 | qed. |
---|
210 | |
---|
211 | lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map: |
---|
212 | ∀M, sigma, w, b. |
---|
213 | assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst M) = false → |
---|
214 | map_internal_ram_address_using_pseudo_address_map M sigma w b = b. |
---|
215 | #M #sigma #w #b #assoc_list_exists_assm |
---|
216 | whd in ⊢ (??%?); |
---|
217 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) % |
---|
218 | qed. |
---|
219 | |
---|
220 | lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2: |
---|
221 | ∀M', cm. |
---|
222 | ∀sigma, status, status', b, b'. |
---|
223 | ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) |
---|
224 | get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → |
---|
225 | low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' → |
---|
226 | b = b' → |
---|
227 | addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → |
---|
228 | map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'. |
---|
229 | #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl |
---|
230 | @(subaddressing_mode_elim … addr1) |
---|
231 | [1: |
---|
232 | whd in ⊢ (??%? → ??%?); cases (\snd M') |
---|
233 | [1: |
---|
234 | normalize nodelta #_ % |
---|
235 | |2: |
---|
236 | * #address normalize nodelta #absurd destruct(absurd) |
---|
237 | ] |
---|
238 | |2,4: |
---|
239 | #w whd in ⊢ (??%? → ??%?); |
---|
240 | inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta |
---|
241 | [1,3: |
---|
242 | #absurd destruct(absurd) |
---|
243 | |2: |
---|
244 | #_ |
---|
245 | <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl) |
---|
246 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) |
---|
247 | normalize nodelta % |
---|
248 | |4: |
---|
249 | #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm) |
---|
250 | -assoc_list_exists_assm #assoc_list_exists_assm |
---|
251 | <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl) |
---|
252 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) |
---|
253 | normalize nodelta % |
---|
254 | ] |
---|
255 | |3: |
---|
256 | #w whd in ⊢ (??%? → ??%?); |
---|
257 | @eq_bv_elim #eq_bv_refl normalize nodelta |
---|
258 | [1: |
---|
259 | #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm) |
---|
260 | #assoc_list_exists_refl #eq_accumulator_refl |
---|
261 | >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b) |
---|
262 | whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl) |
---|
263 | % |
---|
264 | |2: |
---|
265 | #assoc_list_exists_assm |
---|
266 | @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta |
---|
267 | cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl |
---|
268 | <head_head' inversion bit #bit_refl normalize nodelta |
---|
269 | >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl; |
---|
270 | [1: |
---|
271 | @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption |
---|
272 | |2: |
---|
273 | @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map |
---|
274 | <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm) |
---|
275 | ] |
---|
276 | ] |
---|
277 | |5,6,7,8: |
---|
278 | #w try #w' % |
---|
279 | ] |
---|
280 | qed. |
---|
281 | |
---|
282 | lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get: |
---|
283 | ∀M: internal_pseudo_address_map. |
---|
284 | ∀cm: pseudo_assembly_program. |
---|
285 | ∀s: PreStatus pseudo_assembly_program cm. |
---|
286 | ∀sigma: Word → Word. |
---|
287 | ∀addr: [[bit_addr]]. (* XXX: expand as needed *) |
---|
288 | ∀f: bool. |
---|
289 | addressing_mode_ok pseudo_assembly_program M cm s addr = true → |
---|
290 | map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f. |
---|
291 | #M #cm #s #sigma #addr #f |
---|
292 | @(subaddressing_mode_elim … addr) #w |
---|
293 | whd in ⊢ (??%? → %); |
---|
294 | @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta |
---|
295 | cases (head' bool ??) normalize nodelta |
---|
296 | [1: |
---|
297 | #eq_accumulator_assm whd in ⊢ (??%?); |
---|
298 | cases (sfr_of_Byte ?) try % |
---|
299 | * * normalize nodelta try % |
---|
300 | whd in ⊢ (??%?); |
---|
301 | >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % |
---|
302 | |2: |
---|
303 | #assoc_list_exists_assm whd in ⊢ (??%?); |
---|
304 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) (not_b_c_to_b_not_c … assoc_list_exists_assm)) % |
---|
305 | ] |
---|
306 | qed. |
---|
307 | |
---|
308 | lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1: |
---|
309 | ∀M: internal_pseudo_address_map. |
---|
310 | ∀cm: pseudo_assembly_program. |
---|
311 | ∀s, s': PreStatus pseudo_assembly_program cm. |
---|
312 | ∀sigma: Word → Word. |
---|
313 | ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) |
---|
314 | ∀f: bool. |
---|
315 | s = s' → |
---|
316 | addressing_mode_ok pseudo_assembly_program M cm s addr = true → |
---|
317 | map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f. |
---|
318 | #M #cm #s #s' #sigma #addr #f #s_refl <s_refl |
---|
319 | @(subaddressing_mode_elim … addr) [1: #w ] |
---|
320 | whd in ⊢ (??%? → %); [2: #_ @I ] |
---|
321 | inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta |
---|
322 | cases (head' bool ??) normalize nodelta |
---|
323 | [1: |
---|
324 | #eq_accumulator_assm whd in ⊢ (??%?); |
---|
325 | cases (sfr_of_Byte ?) try % * * try % normalize nodelta |
---|
326 | whd in ⊢ (??%?); |
---|
327 | >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % |
---|
328 | |2: |
---|
329 | #assoc_list_exists_assm whd in ⊢ (??%?); |
---|
330 | lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm |
---|
331 | whd in assoc_list_exists_assm:(???%); |
---|
332 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % |
---|
333 | ] |
---|
334 | qed. |
---|
335 | |
---|
336 | lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2: |
---|
337 | ∀M: internal_pseudo_address_map. |
---|
338 | ∀cm: pseudo_assembly_program. |
---|
339 | ∀s, s': PreStatus pseudo_assembly_program cm. |
---|
340 | ∀sigma: Word → Word. |
---|
341 | ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) |
---|
342 | ∀f: bool. |
---|
343 | s = s' → |
---|
344 | addressing_mode_ok pseudo_assembly_program M cm s addr = true → |
---|
345 | map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f. |
---|
346 | #M #cm #s #s' #sigma #addr #f #s_refl <s_refl |
---|
347 | @(subaddressing_mode_elim … addr) [1: #w ] |
---|
348 | whd in ⊢ (??%? → %); [2: #_ @I ] |
---|
349 | inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta |
---|
350 | cases (head' bool ??) normalize nodelta |
---|
351 | [1: |
---|
352 | #eq_accumulator_assm whd in ⊢ (??%?); |
---|
353 | cases (sfr_of_Byte ?) try % * * try % normalize nodelta |
---|
354 | whd in ⊢ (??%?); |
---|
355 | >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % |
---|
356 | |2: |
---|
357 | #assoc_list_exists_assm whd in ⊢ (??%?); |
---|
358 | lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm |
---|
359 | whd in assoc_list_exists_assm:(???%); |
---|
360 | >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % |
---|
361 | ] |
---|
362 | qed. |
---|
363 | |
---|
364 | lemma match_nat_replace: |
---|
365 | ∀l, o, p, r, o', p': nat. |
---|
366 | l ≃ r → |
---|
367 | o ≃ o' → |
---|
368 | p ≃ p' → |
---|
369 | match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ]. |
---|
370 | #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl % |
---|
371 | qed. |
---|
372 | |
---|
373 | lemma conjunction_split: |
---|
374 | ∀l, l', r, r': bool. |
---|
375 | l = l' → r = r' → (l ∧ r) = (l' ∧ r'). |
---|
376 | #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl % |
---|
377 | qed. |
---|
378 | |
---|
379 | lemma match_nat_status_of_pseudo_status: |
---|
380 | ∀M, cm, sigma, policy, s, s', s'', s'''. |
---|
381 | ∀n, n': nat. |
---|
382 | n = n' → |
---|
383 | status_of_pseudo_status M cm s' sigma policy = s → |
---|
384 | (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) → |
---|
385 | match n with [ O ⇒ s | S n' ⇒ s'' n' ] = |
---|
386 | status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy. |
---|
387 | #M #cm #sigma #policy #s #s' #s'' #s''' #n #n' |
---|
388 | #n_refl #s_refl #s_refl' <n_refl <s_refl |
---|
389 | cases n normalize nodelta try % #n' <(s_refl' n') % |
---|
390 | qed. |
---|
391 | |
---|
392 | lemma get_index_v_set_index_hit: |
---|
393 | ∀A: Type[0]. |
---|
394 | ∀n: nat. |
---|
395 | ∀v: Vector A n. |
---|
396 | ∀i: nat. |
---|
397 | ∀e: A. |
---|
398 | ∀i_lt_n_proof: i < n. |
---|
399 | ∀i_lt_n_proof': i < n. |
---|
400 | get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e. |
---|
401 | #A #n #v elim v |
---|
402 | [1: |
---|
403 | #i #e #i_lt_n_proof |
---|
404 | cases (lt_to_not_zero … i_lt_n_proof) |
---|
405 | |2: |
---|
406 | #n' #hd #tl #inductive_hypothesis #i #e |
---|
407 | cases i |
---|
408 | [1: |
---|
409 | #i_lt_n_proof #i_lt_n_proof' % |
---|
410 | |2: |
---|
411 | #i' #i_lt_n_proof' #i_lt_n_proof'' |
---|
412 | whd in ⊢ (??%?); @inductive_hypothesis |
---|
413 | ] |
---|
414 | ] |
---|
415 | qed. |
---|
416 | |
---|
417 | (* |
---|
418 | lemma write_at_stack_pointer_status_of_pseudo_status: |
---|
419 | ∀M, M'. |
---|
420 | ∀cm. |
---|
421 | ∀sigma. |
---|
422 | ∀policy. |
---|
423 | ∀s, s'. |
---|
424 | ∀new_b, new_b'. |
---|
425 | M = M' → |
---|
426 | map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' → |
---|
427 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
428 | write_at_stack_pointer ?? s' new_b' = |
---|
429 | status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy. |
---|
430 | #M #M' #cm #sigma #policy #s #s' #new_b #new_b' |
---|
431 | #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl |
---|
432 | whd in match write_at_stack_pointer; normalize nodelta |
---|
433 | @pair_elim #nu #nl #nu_nl_refl normalize nodelta |
---|
434 | @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl)) |
---|
435 | [1: |
---|
436 | @eq_f |
---|
437 | whd in match get_8051_sfr; normalize nodelta |
---|
438 | whd in match sfr_8051_index; normalize nodelta |
---|
439 | whd in match status_of_pseudo_status; normalize nodelta |
---|
440 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
441 | cases (\snd M) [2: * #address ] normalize nodelta |
---|
442 | [1,2: |
---|
443 | cases (vsplit bool ???) #high #low normalize nodelta |
---|
444 | whd in match sfr_8051_index; normalize nodelta |
---|
445 | >get_index_v_set_index_miss % |
---|
446 | #absurd destruct(absurd) |
---|
447 | |3: |
---|
448 | % |
---|
449 | ] |
---|
450 | |2: |
---|
451 | cases (get_index_v bool ????) normalize nodelta |
---|
452 | whd in match status_of_pseudo_status; normalize nodelta |
---|
453 | whd in match set_low_internal_ram; normalize nodelta |
---|
454 | @split_eq_status try % |
---|
455 | [1: |
---|
456 | @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
457 | |2: |
---|
458 | @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma) |
---|
459 | ] |
---|
460 | *) |
---|
461 | |
---|
462 | lemma main_lemma_preinstruction: |
---|
463 | ∀M, M': internal_pseudo_address_map. |
---|
464 | ∀preamble: preamble. |
---|
465 | ∀instr_list: list labelled_instruction. |
---|
466 | ∀cm: pseudo_assembly_program. |
---|
467 | ∀EQcm: cm = 〈preamble, instr_list〉. |
---|
468 | ∀is_well_labelled_witness: is_well_labelled_p instr_list. |
---|
469 | ∀sigma: Word → Word. |
---|
470 | ∀policy: Word → bool. |
---|
471 | ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. |
---|
472 | ∀ps: PseudoStatus cm. |
---|
473 | ∀ppc: Word. |
---|
474 | ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|. |
---|
475 | ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. |
---|
476 | ∀labels: label_map. |
---|
477 | ∀costs: BitVectorTrie costlabel 16. |
---|
478 | ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. |
---|
479 | ∀newppc: Word. |
---|
480 | ∀lookup_labels: Identifier → Word. |
---|
481 | ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)). |
---|
482 | ∀lookup_datalabels: Identifier → Word. |
---|
483 | ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). |
---|
484 | ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). |
---|
485 | ∀instr: preinstruction Identifier. |
---|
486 | ∀fetch_pseudo_refl: \fst (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr. |
---|
487 | ∀ticks: nat × nat. |
---|
488 | ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr). |
---|
489 | ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. |
---|
490 | ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)). |
---|
491 | ∀s: PreStatus pseudo_assembly_program cm. |
---|
492 | ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). |
---|
493 | ∀P: preinstruction Identifier → PseudoStatus cm → Prop. |
---|
494 | ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) |
---|
495 | (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc |
---|
496 | lookup_datalabels (Instruction instr)))) → |
---|
497 | next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' → |
---|
498 | fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) |
---|
499 | (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → |
---|
500 | ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = |
---|
501 | status_of_pseudo_status M' cm s sigma policy). |
---|
502 | P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). |
---|
503 | (* XXX: takes about 45 minutes to type check! *) |
---|
504 | #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy |
---|
505 | #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels |
---|
506 | #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels |
---|
507 | #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl |
---|
508 | #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP |
---|
509 | (*#sigma_increment_commutation #maps_assm #fetch_many_assm *) |
---|
510 | letin a ≝ Identifier letin m ≝ pseudo_assembly_program |
---|
511 | cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s)) |
---|
512 | [2: * // ] |
---|
513 | @( |
---|
514 | let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in |
---|
515 | let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in |
---|
516 | match instr in preinstruction return λx. x = instr → Σs'.? with |
---|
517 | [ ADD addr1 addr2 ⇒ λinstr_refl. |
---|
518 | let s ≝ add_ticks1 s in |
---|
519 | let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) |
---|
520 | (get_arg_8 … s false addr2) false in |
---|
521 | let cy_flag ≝ get_index' ? O ? flags in |
---|
522 | let ac_flag ≝ get_index' ? 1 ? flags in |
---|
523 | let ov_flag ≝ get_index' ? 2 ? flags in |
---|
524 | let s ≝ set_arg_8 … s ACC_A result in |
---|
525 | set_flags … s cy_flag (Some Bit ac_flag) ov_flag |
---|
526 | | ADDC addr1 addr2 ⇒ λinstr_refl. |
---|
527 | let s ≝ add_ticks1 s in |
---|
528 | let old_cy_flag ≝ get_cy_flag ?? s in |
---|
529 | let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) |
---|
530 | (get_arg_8 … s false addr2) old_cy_flag in |
---|
531 | let cy_flag ≝ get_index' ? O ? flags in |
---|
532 | let ac_flag ≝ get_index' ? 1 ? flags in |
---|
533 | let ov_flag ≝ get_index' ? 2 ? flags in |
---|
534 | let s ≝ set_arg_8 … s ACC_A result in |
---|
535 | set_flags … s cy_flag (Some Bit ac_flag) ov_flag |
---|
536 | | SUBB addr1 addr2 ⇒ λinstr_refl. |
---|
537 | let s ≝ add_ticks1 s in |
---|
538 | let old_cy_flag ≝ get_cy_flag ?? s in |
---|
539 | let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) |
---|
540 | (get_arg_8 … s false addr2) old_cy_flag in |
---|
541 | let cy_flag ≝ get_index' ? O ? flags in |
---|
542 | let ac_flag ≝ get_index' ? 1 ? flags in |
---|
543 | let ov_flag ≝ get_index' ? 2 ? flags in |
---|
544 | let s ≝ set_arg_8 … s ACC_A result in |
---|
545 | set_flags … s cy_flag (Some Bit ac_flag) ov_flag |
---|
546 | | ANL addr ⇒ λinstr_refl. |
---|
547 | let s ≝ add_ticks1 s in |
---|
548 | match addr with |
---|
549 | [ inl l ⇒ |
---|
550 | match l with |
---|
551 | [ inl l' ⇒ |
---|
552 | let 〈addr1, addr2〉 ≝ l' in |
---|
553 | let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
554 | set_arg_8 … s addr1 and_val |
---|
555 | | inr r ⇒ |
---|
556 | let 〈addr1, addr2〉 ≝ r in |
---|
557 | let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
558 | set_arg_8 … s addr1 and_val |
---|
559 | ] |
---|
560 | | inr r ⇒ |
---|
561 | let 〈addr1, addr2〉 ≝ r in |
---|
562 | let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in |
---|
563 | set_flags … s and_val (None ?) (get_ov_flag ?? s) |
---|
564 | ] |
---|
565 | | ORL addr ⇒ λinstr_refl. |
---|
566 | let s ≝ add_ticks1 s in |
---|
567 | match addr with |
---|
568 | [ inl l ⇒ |
---|
569 | match l with |
---|
570 | [ inl l' ⇒ |
---|
571 | let 〈addr1, addr2〉 ≝ l' in |
---|
572 | let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
573 | set_arg_8 … s addr1 or_val |
---|
574 | | inr r ⇒ |
---|
575 | let 〈addr1, addr2〉 ≝ r in |
---|
576 | let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
577 | set_arg_8 … s addr1 or_val |
---|
578 | ] |
---|
579 | | inr r ⇒ |
---|
580 | let 〈addr1, addr2〉 ≝ r in |
---|
581 | let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in |
---|
582 | set_flags … s or_val (None ?) (get_ov_flag … s) |
---|
583 | ] |
---|
584 | | XRL addr ⇒ λinstr_refl. |
---|
585 | let s ≝ add_ticks1 s in |
---|
586 | match addr with |
---|
587 | [ inl l' ⇒ |
---|
588 | let 〈addr1, addr2〉 ≝ l' in |
---|
589 | let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
590 | set_arg_8 … s addr1 xor_val |
---|
591 | | inr r ⇒ |
---|
592 | let 〈addr1, addr2〉 ≝ r in |
---|
593 | let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in |
---|
594 | set_arg_8 … s addr1 xor_val |
---|
595 | ] |
---|
596 | | INC addr ⇒ λinstr_refl. |
---|
597 | match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with |
---|
598 | [ ACC_A ⇒ λacc_a: True. λEQaddr. |
---|
599 | let s' ≝ add_ticks1 s in |
---|
600 | let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in |
---|
601 | set_arg_8 … s' ACC_A result |
---|
602 | | REGISTER r ⇒ λregister: True. λEQaddr. |
---|
603 | let s' ≝ add_ticks1 s in |
---|
604 | let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in |
---|
605 | set_arg_8 … s' (REGISTER r) result |
---|
606 | | DIRECT d ⇒ λdirect: True. λEQaddr. |
---|
607 | let s' ≝ add_ticks1 s in |
---|
608 | let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in |
---|
609 | set_arg_8 … s' (DIRECT d) result |
---|
610 | | INDIRECT i ⇒ λindirect: True. λEQaddr. |
---|
611 | let s' ≝ add_ticks1 s in |
---|
612 | let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in |
---|
613 | set_arg_8 … s' (INDIRECT i) result |
---|
614 | | DPTR ⇒ λdptr: True. λEQaddr. |
---|
615 | let s' ≝ add_ticks1 s in |
---|
616 | let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in |
---|
617 | let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in |
---|
618 | let s ≝ set_8051_sfr … s' SFR_DPL bl in |
---|
619 | set_8051_sfr … s' SFR_DPH bu |
---|
620 | | _ ⇒ λother: False. ⊥ |
---|
621 | ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) |
---|
622 | | NOP ⇒ λinstr_refl. |
---|
623 | let s ≝ add_ticks2 s in |
---|
624 | s |
---|
625 | | DEC addr ⇒ λinstr_refl. |
---|
626 | let s ≝ add_ticks1 s in |
---|
627 | let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in |
---|
628 | set_arg_8 … s addr result |
---|
629 | | MUL addr1 addr2 ⇒ λinstr_refl. |
---|
630 | let s ≝ add_ticks1 s in |
---|
631 | let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in |
---|
632 | let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in |
---|
633 | let product ≝ acc_a_nat * acc_b_nat in |
---|
634 | let ov_flag ≝ product ≥ 256 in |
---|
635 | let low ≝ bitvector_of_nat 8 (product mod 256) in |
---|
636 | let high ≝ bitvector_of_nat 8 (product ÷ 256) in |
---|
637 | let s ≝ set_8051_sfr … s SFR_ACC_A low in |
---|
638 | set_8051_sfr … s SFR_ACC_B high |
---|
639 | | DIV addr1 addr2 ⇒ λinstr_refl. |
---|
640 | let s ≝ add_ticks1 s in |
---|
641 | let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in |
---|
642 | let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in |
---|
643 | match acc_b_nat with |
---|
644 | [ O ⇒ set_flags … s false (None Bit) true |
---|
645 | | S o ⇒ |
---|
646 | let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in |
---|
647 | let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in |
---|
648 | let s ≝ set_8051_sfr … s SFR_ACC_A q in |
---|
649 | let s ≝ set_8051_sfr … s SFR_ACC_B r in |
---|
650 | set_flags … s false (None Bit) false |
---|
651 | ] |
---|
652 | | DA addr ⇒ λinstr_refl. |
---|
653 | let s ≝ add_ticks1 s in |
---|
654 | let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in |
---|
655 | if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then |
---|
656 | let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in |
---|
657 | let cy_flag ≝ get_index' ? O ? flags in |
---|
658 | let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in |
---|
659 | if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then |
---|
660 | let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in |
---|
661 | let new_acc ≝ nu @@ acc_nl' in |
---|
662 | let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in |
---|
663 | set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) |
---|
664 | else |
---|
665 | s |
---|
666 | else |
---|
667 | s |
---|
668 | | CLR addr ⇒ λinstr_refl. |
---|
669 | match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with |
---|
670 | [ ACC_A ⇒ λacc_a: True. λEQaddr. |
---|
671 | let s ≝ add_ticks1 s in |
---|
672 | set_arg_8 … s ACC_A (zero 8) |
---|
673 | | CARRY ⇒ λcarry: True. λEQaddr. |
---|
674 | let s ≝ add_ticks1 s in |
---|
675 | set_arg_1 … s CARRY false |
---|
676 | | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. |
---|
677 | let s ≝ add_ticks1 s in |
---|
678 | set_arg_1 … s (BIT_ADDR b) false |
---|
679 | | _ ⇒ λother: False. ⊥ |
---|
680 | ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) |
---|
681 | | CPL addr ⇒ λinstr_refl. |
---|
682 | match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with |
---|
683 | [ ACC_A ⇒ λacc_a: True. λEQaddr. |
---|
684 | let s ≝ add_ticks1 s in |
---|
685 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
686 | let new_acc ≝ negation_bv ? old_acc in |
---|
687 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
688 | | CARRY ⇒ λcarry: True. λEQaddr. |
---|
689 | let s ≝ add_ticks1 s in |
---|
690 | let old_cy_flag ≝ get_arg_1 … s CARRY true in |
---|
691 | let new_cy_flag ≝ ¬old_cy_flag in |
---|
692 | set_arg_1 … s CARRY new_cy_flag |
---|
693 | | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. |
---|
694 | let s ≝ add_ticks1 s in |
---|
695 | let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in |
---|
696 | let new_bit ≝ ¬old_bit in |
---|
697 | set_arg_1 … s (BIT_ADDR b) new_bit |
---|
698 | | _ ⇒ λother: False. ? |
---|
699 | ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) |
---|
700 | | SETB b ⇒ λinstr_refl. |
---|
701 | let s ≝ add_ticks1 s in |
---|
702 | set_arg_1 … s b false |
---|
703 | | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) |
---|
704 | let s ≝ add_ticks1 s in |
---|
705 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
706 | let new_acc ≝ rotate_left … 1 old_acc in |
---|
707 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
708 | | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) |
---|
709 | let s ≝ add_ticks1 s in |
---|
710 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
711 | let new_acc ≝ rotate_right … 1 old_acc in |
---|
712 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
713 | | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) |
---|
714 | let s ≝ add_ticks1 s in |
---|
715 | let old_cy_flag ≝ get_cy_flag ?? s in |
---|
716 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
717 | let new_cy_flag ≝ get_index' ? O ? old_acc in |
---|
718 | let new_acc ≝ shift_left … 1 old_acc old_cy_flag in |
---|
719 | let s ≝ set_arg_1 … s CARRY new_cy_flag in |
---|
720 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
721 | | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) |
---|
722 | let s ≝ add_ticks1 s in |
---|
723 | let old_cy_flag ≝ get_cy_flag ?? s in |
---|
724 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
725 | let new_cy_flag ≝ get_index' ? 7 ? old_acc in |
---|
726 | let new_acc ≝ shift_right … 1 old_acc old_cy_flag in |
---|
727 | let s ≝ set_arg_1 … s CARRY new_cy_flag in |
---|
728 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
729 | | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *) |
---|
730 | let s ≝ add_ticks1 s in |
---|
731 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
732 | let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in |
---|
733 | let new_acc ≝ nl @@ nu in |
---|
734 | set_8051_sfr … s SFR_ACC_A new_acc |
---|
735 | | PUSH addr ⇒ λinstr_refl. |
---|
736 | match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with |
---|
737 | [ DIRECT d ⇒ λdirect: True. λEQaddr. |
---|
738 | let s ≝ add_ticks1 s in |
---|
739 | let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in |
---|
740 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
741 | write_at_stack_pointer … s d |
---|
742 | | _ ⇒ λother: False. ⊥ |
---|
743 | ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) |
---|
744 | | POP addr ⇒ λinstr_refl. |
---|
745 | let s ≝ add_ticks1 s in |
---|
746 | let contents ≝ read_at_stack_pointer ?? s in |
---|
747 | let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in |
---|
748 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
749 | set_arg_8 … s addr contents |
---|
750 | | XCH addr1 addr2 ⇒ λinstr_refl. |
---|
751 | let s ≝ add_ticks1 s in |
---|
752 | let old_addr ≝ get_arg_8 … s false addr2 in |
---|
753 | let old_acc ≝ get_8051_sfr … s SFR_ACC_A in |
---|
754 | let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in |
---|
755 | set_arg_8 … s addr2 old_acc |
---|
756 | | XCHD addr1 addr2 ⇒ λinstr_refl. |
---|
757 | let s ≝ add_ticks1 s in |
---|
758 | let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in |
---|
759 | let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in |
---|
760 | let new_acc ≝ acc_nu @@ arg_nl in |
---|
761 | let new_arg ≝ arg_nu @@ acc_nl in |
---|
762 | let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in |
---|
763 | set_arg_8 … s addr2 new_arg |
---|
764 | | RET ⇒ λinstr_refl. |
---|
765 | let s ≝ add_ticks1 s in |
---|
766 | let high_bits ≝ read_at_stack_pointer ?? s in |
---|
767 | let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in |
---|
768 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
769 | let low_bits ≝ read_at_stack_pointer ?? s in |
---|
770 | let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in |
---|
771 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
772 | let new_pc ≝ high_bits @@ low_bits in |
---|
773 | set_program_counter … s new_pc |
---|
774 | | RETI ⇒ λinstr_refl. |
---|
775 | let s ≝ add_ticks1 s in |
---|
776 | let high_bits ≝ read_at_stack_pointer ?? s in |
---|
777 | let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in |
---|
778 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
779 | let low_bits ≝ read_at_stack_pointer ?? s in |
---|
780 | let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in |
---|
781 | let s ≝ set_8051_sfr … s SFR_SP new_sp in |
---|
782 | let new_pc ≝ high_bits @@ low_bits in |
---|
783 | set_program_counter … s new_pc |
---|
784 | | MOVX addr ⇒ λinstr_refl. |
---|
785 | let s ≝ add_ticks1 s in |
---|
786 | (* DPM: only copies --- doesn't affect I/O *) |
---|
787 | match addr with |
---|
788 | [ inl l ⇒ |
---|
789 | let 〈addr1, addr2〉 ≝ l in |
---|
790 | set_arg_8 … s addr1 (get_arg_8 … s false addr2) |
---|
791 | | inr r ⇒ |
---|
792 | let 〈addr1, addr2〉 ≝ r in |
---|
793 | set_arg_8 … s addr1 (get_arg_8 … s false addr2) |
---|
794 | ] |
---|
795 | | MOV addr ⇒ λinstr_refl. |
---|
796 | let s ≝ add_ticks1 s in |
---|
797 | match addr with |
---|
798 | [ inl l ⇒ |
---|
799 | match l with |
---|
800 | [ inl l' ⇒ |
---|
801 | match l' with |
---|
802 | [ inl l'' ⇒ |
---|
803 | match l'' with |
---|
804 | [ inl l''' ⇒ |
---|
805 | match l''' with |
---|
806 | [ inl l'''' ⇒ |
---|
807 | let 〈addr1, addr2〉 ≝ l'''' in |
---|
808 | set_arg_8 … s addr1 (get_arg_8 … s false addr2) |
---|
809 | | inr r'''' ⇒ |
---|
810 | let 〈addr1, addr2〉 ≝ r'''' in |
---|
811 | set_arg_8 … s addr1 (get_arg_8 … s false addr2) |
---|
812 | ] |
---|
813 | | inr r''' ⇒ |
---|
814 | let 〈addr1, addr2〉 ≝ r''' in |
---|
815 | set_arg_8 … s addr1 (get_arg_8 … s false addr2) |
---|
816 | ] |
---|
817 | | inr r'' ⇒ |
---|
818 | let 〈addr1, addr2〉 ≝ r'' in |
---|
819 | set_arg_16 … s (get_arg_16 … s addr2) addr1 |
---|
820 | ] |
---|
821 | | inr r ⇒ |
---|
822 | let 〈addr1, addr2〉 ≝ r in |
---|
823 | set_arg_1 … s addr1 (get_arg_1 … s addr2 false) |
---|
824 | ] |
---|
825 | | inr r ⇒ |
---|
826 | let 〈addr1, addr2〉 ≝ r in |
---|
827 | set_arg_1 … s addr1 (get_arg_1 … s addr2 false) |
---|
828 | ] |
---|
829 | | JC addr ⇒ λinstr_refl. |
---|
830 | if get_cy_flag ?? s then |
---|
831 | let s ≝ add_ticks1 s in |
---|
832 | set_program_counter … s (addr_of addr s) |
---|
833 | else |
---|
834 | let s ≝ add_ticks2 s in |
---|
835 | s |
---|
836 | | JNC addr ⇒ λinstr_refl. |
---|
837 | if ¬(get_cy_flag ?? s) then |
---|
838 | let s ≝ add_ticks1 s in |
---|
839 | set_program_counter … s (addr_of addr s) |
---|
840 | else |
---|
841 | let s ≝ add_ticks2 s in |
---|
842 | s |
---|
843 | | JB addr1 addr2 ⇒ λinstr_refl. |
---|
844 | if get_arg_1 … s addr1 false then |
---|
845 | let s ≝ add_ticks1 s in |
---|
846 | set_program_counter … s (addr_of addr2 s) |
---|
847 | else |
---|
848 | let s ≝ add_ticks2 s in |
---|
849 | s |
---|
850 | | JNB addr1 addr2 ⇒ λinstr_refl. |
---|
851 | if ¬(get_arg_1 … s addr1 false) then |
---|
852 | let s ≝ add_ticks1 s in |
---|
853 | set_program_counter … s (addr_of addr2 s) |
---|
854 | else |
---|
855 | let s ≝ add_ticks2 s in |
---|
856 | s |
---|
857 | | JBC addr1 addr2 ⇒ λinstr_refl. |
---|
858 | let s ≝ set_arg_1 … s addr1 false in |
---|
859 | if get_arg_1 … s addr1 false then |
---|
860 | let s ≝ add_ticks1 s in |
---|
861 | set_program_counter … s (addr_of addr2 s) |
---|
862 | else |
---|
863 | let s ≝ add_ticks2 s in |
---|
864 | s |
---|
865 | | JZ addr ⇒ λinstr_refl. |
---|
866 | if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then |
---|
867 | let s ≝ add_ticks1 s in |
---|
868 | set_program_counter … s (addr_of addr s) |
---|
869 | else |
---|
870 | let s ≝ add_ticks2 s in |
---|
871 | s |
---|
872 | | JNZ addr ⇒ λinstr_refl. |
---|
873 | if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then |
---|
874 | let s ≝ add_ticks1 s in |
---|
875 | set_program_counter … s (addr_of addr s) |
---|
876 | else |
---|
877 | let s ≝ add_ticks2 s in |
---|
878 | s |
---|
879 | | CJNE addr1 addr2 ⇒ λinstr_refl. |
---|
880 | match addr1 with |
---|
881 | [ inl l ⇒ |
---|
882 | let 〈addr1, addr2'〉 ≝ l in |
---|
883 | let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) |
---|
884 | (nat_of_bitvector ? (get_arg_8 … s false addr2')) in |
---|
885 | if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then |
---|
886 | let s ≝ add_ticks1 s in |
---|
887 | let s ≝ set_program_counter … s (addr_of addr2 s) in |
---|
888 | set_flags … s new_cy (None ?) (get_ov_flag ?? s) |
---|
889 | else |
---|
890 | let s ≝ add_ticks2 s in |
---|
891 | set_flags … s new_cy (None ?) (get_ov_flag ?? s) |
---|
892 | | inr r' ⇒ |
---|
893 | let 〈addr1, addr2'〉 ≝ r' in |
---|
894 | let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) |
---|
895 | (nat_of_bitvector ? (get_arg_8 … s false addr2')) in |
---|
896 | if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then |
---|
897 | let s ≝ add_ticks1 s in |
---|
898 | let s ≝ set_program_counter … s (addr_of addr2 s) in |
---|
899 | set_flags … s new_cy (None ?) (get_ov_flag ?? s) |
---|
900 | else |
---|
901 | let s ≝ add_ticks2 s in |
---|
902 | set_flags … s new_cy (None ?) (get_ov_flag ?? s) |
---|
903 | ] |
---|
904 | | DJNZ addr1 addr2 ⇒ λinstr_refl. |
---|
905 | let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in |
---|
906 | let s ≝ set_arg_8 … s addr1 result in |
---|
907 | if ¬(eq_bv ? result (zero 8)) then |
---|
908 | let s ≝ add_ticks1 s in |
---|
909 | set_program_counter … s (addr_of addr2 s) |
---|
910 | else |
---|
911 | let s ≝ add_ticks2 s in |
---|
912 | s |
---|
913 | ] (refl … instr)) |
---|
914 | try cases other |
---|
915 | try assumption (*20s*) |
---|
916 | try (% @False) (*6s*) (* Bug exploited here to implement solve :-*) |
---|
917 | try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) |
---|
918 | whd in match execute_1_preinstruction; normalize nodelta |
---|
919 | [(*1,2: (* ADD and ADDC *) |
---|
920 | (* XXX: work on the right hand side *) |
---|
921 | (* XXX: switch to the left hand side *) |
---|
922 | >EQP -P normalize nodelta |
---|
923 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
924 | whd in maps_assm:(??%%); |
---|
925 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
926 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
927 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
928 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
929 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
930 | whd in ⊢ (??%?); |
---|
931 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
932 | whd in ⊢ (??%?); |
---|
933 | normalize nodelta >EQs >EQticks <instr_refl |
---|
934 | @let_pair_in_status_of_pseudo_status |
---|
935 | [1,3: |
---|
936 | @eq_f3 |
---|
937 | [1,2,4,5: |
---|
938 | @(pose … (set_clock ????)) #status #status_refl |
---|
939 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
940 | [1,5: |
---|
941 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try % |
---|
942 | @(subaddressing_mode_elim … addr1) % |
---|
943 | |3,7: |
---|
944 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % |
---|
945 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
946 | |2,6: |
---|
947 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try % |
---|
948 | @(subaddressing_mode_elim … addr1) % |
---|
949 | |4,8: |
---|
950 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try % |
---|
951 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
952 | ] |
---|
953 | |3: |
---|
954 | % |
---|
955 | |6: |
---|
956 | @sym_eq @(get_cy_flag_status_of_pseudo_status M') |
---|
957 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
958 | ] |
---|
959 | |2,4: |
---|
960 | #result #flags @sym_eq |
---|
961 | @set_flags_status_of_pseudo_status try % |
---|
962 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
963 | @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) |
---|
964 | ] |
---|
965 | |3: (* SUBB *) |
---|
966 | (* XXX: work on the right hand side *) |
---|
967 | (* XXX: switch to the left hand side *) |
---|
968 | >EQP -P normalize nodelta |
---|
969 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
970 | whd in maps_assm:(??%%); |
---|
971 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
972 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
973 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
974 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
975 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
976 | whd in ⊢ (??%?); |
---|
977 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
978 | whd in ⊢ (??%?); |
---|
979 | @(pair_replace ?????????? p) |
---|
980 | [1: |
---|
981 | @eq_f3 |
---|
982 | normalize nodelta >EQs >EQticks <instr_refl |
---|
983 | [1: |
---|
984 | @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl |
---|
985 | @(get_arg_8_status_of_pseudo_status cm status … M') |
---|
986 | [1: |
---|
987 | >status_refl @sym_eq @set_clock_status_of_pseudo_status % |
---|
988 | |2: |
---|
989 | >status_refl |
---|
990 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) |
---|
991 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
992 | |3: |
---|
993 | >status_refl |
---|
994 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) |
---|
995 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
996 | ] |
---|
997 | |2: |
---|
998 | @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl |
---|
999 | @(get_arg_8_status_of_pseudo_status cm status … M') |
---|
1000 | [1: |
---|
1001 | >status_refl @sym_eq @set_clock_status_of_pseudo_status % |
---|
1002 | |2: |
---|
1003 | >status_refl |
---|
1004 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) |
---|
1005 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1006 | |3: |
---|
1007 | >status_refl |
---|
1008 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) |
---|
1009 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1010 | ] |
---|
1011 | |3: |
---|
1012 | @(get_cy_flag_status_of_pseudo_status … M') |
---|
1013 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1014 | [1: |
---|
1015 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1016 | |2: |
---|
1017 | % |
---|
1018 | ] |
---|
1019 | ] |
---|
1020 | |2: |
---|
1021 | normalize nodelta |
---|
1022 | @(pair_replace ?????????? p) |
---|
1023 | [1: |
---|
1024 | @eq_f3 normalize nodelta >EQs >EQticks <instr_refl % |
---|
1025 | |2: |
---|
1026 | @set_flags_status_of_pseudo_status try % |
---|
1027 | @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …)) |
---|
1028 | [1: |
---|
1029 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1030 | |2: |
---|
1031 | @I |
---|
1032 | |3: |
---|
1033 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) |
---|
1034 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try % |
---|
1035 | <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) % |
---|
1036 | ] |
---|
1037 | ] |
---|
1038 | ] |
---|
1039 | |4: (* INC *) |
---|
1040 | (* XXX: work on the right hand side *) |
---|
1041 | (* XXX: switch to the left hand side *) |
---|
1042 | >EQs >EQticks <instr_refl >EQP -P normalize nodelta |
---|
1043 | @(subaddressing_mode_elim … addr) normalize nodelta |
---|
1044 | [1: |
---|
1045 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1046 | whd in maps_assm:(??%%); |
---|
1047 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1048 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1049 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1050 | whd in ⊢ (??%?); |
---|
1051 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1052 | whd in ⊢ (??%?); |
---|
1053 | inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta |
---|
1054 | @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl)) |
---|
1055 | [1: |
---|
1056 | @eq_f2 try % |
---|
1057 | @(pose … (set_clock ????)) #status #status_refl |
---|
1058 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1059 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % |
---|
1060 | |2: |
---|
1061 | @set_arg_8_status_of_pseudo_status try % |
---|
1062 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try % |
---|
1063 | ] |
---|
1064 | |2: |
---|
1065 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1066 | whd in maps_assm:(??%%); |
---|
1067 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1068 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1069 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1070 | whd in ⊢ (??%?); |
---|
1071 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1072 | whd in ⊢ (??%?); |
---|
1073 | @let_pair_in_status_of_pseudo_status |
---|
1074 | [1: |
---|
1075 | @eq_f2 try % |
---|
1076 | @(pose … (set_clock ????)) #status #status_refl |
---|
1077 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1078 | >EQs >EQticks |
---|
1079 | [1: |
---|
1080 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1081 | |2: |
---|
1082 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % |
---|
1083 | |3: |
---|
1084 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) % |
---|
1085 | ] |
---|
1086 | |2: |
---|
1087 | #carry #result |
---|
1088 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1089 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % |
---|
1090 | ] |
---|
1091 | |3: |
---|
1092 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1093 | whd in maps_assm:(??%%); |
---|
1094 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1095 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1096 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1097 | whd in ⊢ (??%?); |
---|
1098 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1099 | whd in ⊢ (??%?); |
---|
1100 | @let_pair_in_status_of_pseudo_status |
---|
1101 | [1: |
---|
1102 | @eq_f2 try % |
---|
1103 | @(pose … (set_clock ????)) #status #status_refl |
---|
1104 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1105 | >EQs >EQticks |
---|
1106 | [1: |
---|
1107 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1108 | |2: |
---|
1109 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % |
---|
1110 | |3: |
---|
1111 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) % |
---|
1112 | ] |
---|
1113 | |2: |
---|
1114 | #carry #result |
---|
1115 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1116 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % |
---|
1117 | ] |
---|
1118 | |4: |
---|
1119 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1120 | whd in maps_assm:(??%%); |
---|
1121 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1122 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1123 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1124 | whd in ⊢ (??%?); |
---|
1125 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1126 | whd in ⊢ (??%?); |
---|
1127 | @let_pair_in_status_of_pseudo_status |
---|
1128 | [1: |
---|
1129 | @eq_f2 try % |
---|
1130 | @(pose … (set_clock ????)) #status #status_refl |
---|
1131 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1132 | >EQs >EQticks |
---|
1133 | [1: |
---|
1134 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1135 | |2: |
---|
1136 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1137 | |3: |
---|
1138 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1139 | ] |
---|
1140 | |2: |
---|
1141 | #carry #result |
---|
1142 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1143 | [1: |
---|
1144 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1145 | |2: |
---|
1146 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1147 | ] |
---|
1148 | ] |
---|
1149 | |5: |
---|
1150 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1151 | whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1152 | whd in ⊢ (??%?); |
---|
1153 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1154 | whd in ⊢ (??%?); |
---|
1155 | @let_pair_in_status_of_pseudo_status |
---|
1156 | [1: |
---|
1157 | @eq_f2 try % |
---|
1158 | @(pose … (set_clock ????)) #status #status_refl |
---|
1159 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl |
---|
1160 | >EQs >EQticks % |
---|
1161 | |2: |
---|
1162 | #carry #bl |
---|
1163 | @sym_eq @let_pair_in_status_of_pseudo_status |
---|
1164 | [1: |
---|
1165 | @eq_f3 try % |
---|
1166 | @(pose … (set_clock ????)) #status #status_refl |
---|
1167 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl |
---|
1168 | >EQs >EQticks % |
---|
1169 | |2: |
---|
1170 | #carry' #bu |
---|
1171 | @sym_eq @set_8051_sfr_status_of_pseudo_status % |
---|
1172 | ] |
---|
1173 | ] |
---|
1174 | ] |
---|
1175 | |5: (* DEC *) |
---|
1176 | >EQs >EQticks <instr_refl >EQP -P normalize nodelta |
---|
1177 | @(subaddressing_mode_elim … addr) normalize nodelta |
---|
1178 | [1: |
---|
1179 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1180 | whd in maps_assm:(??%%); |
---|
1181 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1182 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1183 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1184 | whd in ⊢ (??%?); |
---|
1185 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1186 | whd in ⊢ (??%?); |
---|
1187 | @let_pair_in_status_of_pseudo_status |
---|
1188 | [1: |
---|
1189 | @eq_f3 try % |
---|
1190 | @(pose … (set_clock ????)) #status #status_refl |
---|
1191 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1192 | >EQs >EQticks try % |
---|
1193 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % |
---|
1194 | |2: |
---|
1195 | #result #flags |
---|
1196 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1197 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % |
---|
1198 | ] |
---|
1199 | |2: |
---|
1200 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1201 | whd in maps_assm:(??%%); |
---|
1202 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1203 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1204 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1205 | whd in ⊢ (??%?); |
---|
1206 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1207 | whd in ⊢ (??%?); |
---|
1208 | @let_pair_in_status_of_pseudo_status |
---|
1209 | [1: |
---|
1210 | @eq_f3 try % |
---|
1211 | @(pose … (set_clock ????)) #status #status_refl |
---|
1212 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1213 | >EQs >EQticks try % |
---|
1214 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % |
---|
1215 | |2: |
---|
1216 | #result #flags |
---|
1217 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1218 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) % |
---|
1219 | ] |
---|
1220 | |3: |
---|
1221 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1222 | whd in maps_assm:(??%%); |
---|
1223 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1224 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1225 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1226 | whd in ⊢ (??%?); |
---|
1227 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1228 | whd in ⊢ (??%?); |
---|
1229 | @let_pair_in_status_of_pseudo_status |
---|
1230 | [1: |
---|
1231 | @eq_f3 try % |
---|
1232 | @(pose … (set_clock ????)) #status #status_refl |
---|
1233 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1234 | >EQs >EQticks try % |
---|
1235 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % |
---|
1236 | |2: |
---|
1237 | #result #flags |
---|
1238 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1239 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) % |
---|
1240 | ] |
---|
1241 | |4: |
---|
1242 | #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1243 | whd in maps_assm:(??%%); |
---|
1244 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1245 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1246 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1247 | whd in ⊢ (??%?); |
---|
1248 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1249 | whd in ⊢ (??%?); |
---|
1250 | @let_pair_in_status_of_pseudo_status |
---|
1251 | [1: |
---|
1252 | @eq_f3 try % |
---|
1253 | @(pose … (set_clock ????)) #status #status_refl |
---|
1254 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1255 | >EQs >EQticks try % |
---|
1256 | [1: |
---|
1257 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1258 | |2: |
---|
1259 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1260 | ] |
---|
1261 | |2: |
---|
1262 | #result #flags |
---|
1263 | @sym_eq @set_arg_8_status_of_pseudo_status try % |
---|
1264 | [1: |
---|
1265 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1266 | |2: |
---|
1267 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) % |
---|
1268 | ] |
---|
1269 | ] |
---|
1270 | ] |
---|
1271 | |6: (* MUL *) |
---|
1272 | (* XXX: work on the right hand side *) |
---|
1273 | (* XXX: switch to the left hand side *) |
---|
1274 | >EQP -P normalize nodelta |
---|
1275 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1276 | whd in maps_assm:(??%%); |
---|
1277 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1278 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1279 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1280 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1281 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1282 | whd in ⊢ (??%?); |
---|
1283 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
1284 | change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status |
---|
1285 | [2: |
---|
1286 | whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f |
---|
1287 | @sym_eq |
---|
1288 | [1: |
---|
1289 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1290 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) |
---|
1291 | % |
---|
1292 | |2: |
---|
1293 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) % |
---|
1294 | ] |
---|
1295 | ] |
---|
1296 | @sym_eq @set_8051_sfr_status_of_pseudo_status |
---|
1297 | [2: |
---|
1298 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) |
---|
1299 | @eq_f @eq_f2 try % @eq_f2 @eq_f |
---|
1300 | @sym_eq |
---|
1301 | [1: |
---|
1302 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1303 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1304 | |2: |
---|
1305 | @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) % |
---|
1306 | ] |
---|
1307 | ] |
---|
1308 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1309 | [2: |
---|
1310 | @eq_f % |
---|
1311 | ] |
---|
1312 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1313 | |7,8: (* DIV *) |
---|
1314 | (* XXX: work on the right hand side *) |
---|
1315 | (* XXX: switch to the left hand side *) |
---|
1316 | >EQP -P normalize nodelta |
---|
1317 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1318 | whd in maps_assm:(??%%); |
---|
1319 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1320 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1321 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1322 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1323 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1324 | whd in ⊢ (??%?); |
---|
1325 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
1326 | whd in ⊢ (??%?); normalize nodelta |
---|
1327 | @(match_nat_status_of_pseudo_status M' cm sigma policy) |
---|
1328 | [1,4: |
---|
1329 | @eq_f |
---|
1330 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
1331 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
1332 | |2,5: |
---|
1333 | @sym_eq @set_flags_status_of_pseudo_status % |
---|
1334 | |3,6: |
---|
1335 | #n @sym_eq @set_flags_status_of_pseudo_status try % |
---|
1336 | @sym_eq @set_8051_sfr_status_of_pseudo_status |
---|
1337 | [1,3: |
---|
1338 | @sym_eq @set_8051_sfr_status_of_pseudo_status try % |
---|
1339 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta |
---|
1340 | @eq_f @eq_f2 try % @eq_f |
---|
1341 | @(pose … (set_clock ????)) #status #status_refl |
---|
1342 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
1343 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1344 | |2,4: |
---|
1345 | whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f |
---|
1346 | @(pose … (set_clock ????)) #status #status_refl |
---|
1347 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
1348 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1349 | ] |
---|
1350 | ] |
---|
1351 | |9: (* DA *) |
---|
1352 | (* XXX: work on the right hand side *) |
---|
1353 | (* XXX: switch to the left hand side *) |
---|
1354 | >EQP -P normalize nodelta |
---|
1355 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1356 | whd in maps_assm:(??%%); |
---|
1357 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1358 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1359 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1360 | whd in ⊢ (??%?); |
---|
1361 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1362 | whd in ⊢ (??%?); normalize nodelta |
---|
1363 | @(pair_replace ?????????? p) |
---|
1364 | [1: |
---|
1365 | @eq_f normalize nodelta >EQs >EQticks <instr_refl |
---|
1366 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1367 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1368 | |2: |
---|
1369 | @(pair_replace ?????????? p) |
---|
1370 | [1: |
---|
1371 | @eq_f normalize nodelta >EQs >EQticks <instr_refl % |
---|
1372 | |2: |
---|
1373 | @(if_then_else_replace ???????? p1) normalize nodelta |
---|
1374 | [1: |
---|
1375 | cases (gtb ? 9) |
---|
1376 | [1: |
---|
1377 | % |
---|
1378 | |2: |
---|
1379 | change with (get_ac_flag ??? = get_ac_flag ???) |
---|
1380 | @(get_ac_flag_status_of_pseudo_status M') |
---|
1381 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1382 | >EQs >EQticks <instr_refl % |
---|
1383 | ] |
---|
1384 | |2: |
---|
1385 | @(if_then_else_replace ???????? p1) normalize nodelta try % |
---|
1386 | @(pair_replace ?????????? p2) |
---|
1387 | [1: |
---|
1388 | @eq_f3 try % normalize nodelta |
---|
1389 | @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) |
---|
1390 | whd in ⊢ (??%?); |
---|
1391 | >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1392 | |2: |
---|
1393 | @(pair_replace ?????????? p2) try % |
---|
1394 | @(pair_replace ?????????? p3) try % |
---|
1395 | @(pair_replace ?????????? p3) try % |
---|
1396 | @(if_then_else_replace ???????? p4) try % normalize nodelta |
---|
1397 | @(if_then_else_replace ???????? p4) try % normalize nodelta |
---|
1398 | @(pair_replace ?????????? p5) try % |
---|
1399 | @(pair_replace ?????????? p5) try % |
---|
1400 | @set_flags_status_of_pseudo_status try % |
---|
1401 | [1: |
---|
1402 | @eq_f @(get_ac_flag_status_of_pseudo_status M') |
---|
1403 | @sym_eq @set_8051_sfr_status_of_pseudo_status |
---|
1404 | [1: |
---|
1405 | @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % |
---|
1406 | |2: |
---|
1407 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1408 | ] |
---|
1409 | |2: |
---|
1410 | @(get_ov_flag_status_of_pseudo_status M') |
---|
1411 | @sym_eq @set_8051_sfr_status_of_pseudo_status |
---|
1412 | [1: |
---|
1413 | @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % |
---|
1414 | |2: |
---|
1415 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1416 | ] |
---|
1417 | |3: |
---|
1418 | @sym_eq @set_8051_sfr_status_of_pseudo_status |
---|
1419 | [1: |
---|
1420 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1421 | [1: |
---|
1422 | >EQs |
---|
1423 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1424 | |2: |
---|
1425 | >EQs >EQticks <instr_refl % |
---|
1426 | ] |
---|
1427 | |2: |
---|
1428 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1429 | ] |
---|
1430 | ] |
---|
1431 | ] |
---|
1432 | ] |
---|
1433 | ] |
---|
1434 | ] |
---|
1435 | |10: (* DA *) |
---|
1436 | (* XXX: work on the right hand side *) |
---|
1437 | (* XXX: switch to the left hand side *) |
---|
1438 | >EQP -P normalize nodelta |
---|
1439 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1440 | whd in maps_assm:(??%%); |
---|
1441 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1442 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1443 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1444 | whd in ⊢ (??%?); |
---|
1445 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1446 | whd in ⊢ (??%?); normalize nodelta |
---|
1447 | @(pair_replace ?????????? p) |
---|
1448 | [1: |
---|
1449 | @eq_f normalize nodelta >EQs >EQticks <instr_refl |
---|
1450 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1451 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1452 | |2: |
---|
1453 | @(pair_replace ?????????? p) |
---|
1454 | [1: |
---|
1455 | @eq_f normalize nodelta >EQs >EQticks <instr_refl % |
---|
1456 | |2: |
---|
1457 | @(if_then_else_replace ???????? p1) normalize nodelta |
---|
1458 | [1: |
---|
1459 | cases (gtb ? 9) |
---|
1460 | [1: |
---|
1461 | % |
---|
1462 | |2: |
---|
1463 | change with (get_ac_flag ??? = get_ac_flag ???) |
---|
1464 | @(get_ac_flag_status_of_pseudo_status M') |
---|
1465 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1466 | >EQs >EQticks <instr_refl % |
---|
1467 | ] |
---|
1468 | |2: |
---|
1469 | @(if_then_else_replace ???????? p1) normalize nodelta try % |
---|
1470 | @(pair_replace ?????????? p2) |
---|
1471 | [1: |
---|
1472 | @eq_f3 try % normalize nodelta |
---|
1473 | @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) |
---|
1474 | whd in ⊢ (??%?); |
---|
1475 | >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1476 | |2: |
---|
1477 | @(pair_replace ?????????? p2) try % |
---|
1478 | @(pair_replace ?????????? p3) try % |
---|
1479 | @(pair_replace ?????????? p3) try % |
---|
1480 | @(if_then_else_replace ???????? p4) try % normalize nodelta |
---|
1481 | @(if_then_else_replace ???????? p4) try % normalize nodelta |
---|
1482 | @set_clock_status_of_pseudo_status |
---|
1483 | [1: |
---|
1484 | >EQs |
---|
1485 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1486 | |2: |
---|
1487 | >EQs >EQticks <instr_refl % |
---|
1488 | ] |
---|
1489 | ] |
---|
1490 | ] |
---|
1491 | ] |
---|
1492 | ] |
---|
1493 | |11: (* DA *) |
---|
1494 | (* XXX: work on the right hand side *) |
---|
1495 | (* XXX: switch to the left hand side *) |
---|
1496 | >EQP -P normalize nodelta |
---|
1497 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1498 | whd in maps_assm:(??%%); |
---|
1499 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1500 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1501 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1502 | whd in ⊢ (??%?); |
---|
1503 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1504 | whd in ⊢ (??%?); normalize nodelta |
---|
1505 | @(pair_replace ?????????? p) |
---|
1506 | [1: |
---|
1507 | @eq_f normalize nodelta >EQs >EQticks <instr_refl |
---|
1508 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1509 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1510 | |2: |
---|
1511 | @(pair_replace ?????????? p) |
---|
1512 | [1: |
---|
1513 | @eq_f normalize nodelta >EQs >EQticks <instr_refl % |
---|
1514 | |2: |
---|
1515 | @(if_then_else_replace ???????? p1) normalize nodelta |
---|
1516 | [1: |
---|
1517 | cases (gtb ? 9) |
---|
1518 | [1: |
---|
1519 | % |
---|
1520 | |2: |
---|
1521 | change with (get_ac_flag ??? = get_ac_flag ???) |
---|
1522 | @(get_ac_flag_status_of_pseudo_status M') |
---|
1523 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1524 | >EQs >EQticks <instr_refl % |
---|
1525 | ] |
---|
1526 | |2: |
---|
1527 | @(if_then_else_replace ???????? p1) normalize nodelta try % |
---|
1528 | @set_clock_status_of_pseudo_status |
---|
1529 | [1: |
---|
1530 | >EQs |
---|
1531 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1532 | |2: |
---|
1533 | >EQs >EQticks <instr_refl % |
---|
1534 | ] |
---|
1535 | ] |
---|
1536 | ] |
---|
1537 | ] |
---|
1538 | |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *) |
---|
1539 | cases daemon |
---|
1540 | |29,30: (* ANL and ORL *) |
---|
1541 | inversion addr |
---|
1542 | [1,3: |
---|
1543 | * |
---|
1544 | [1,3: |
---|
1545 | #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl |
---|
1546 | >EQP -P normalize nodelta |
---|
1547 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1548 | whd in maps_assm:(??%%); |
---|
1549 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1550 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1551 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1552 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1553 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1554 | whd in ⊢ (??%?); |
---|
1555 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1556 | change with (set_arg_8 ????? = ?) |
---|
1557 | @set_arg_8_status_of_pseudo_status try % |
---|
1558 | >EQs >EQticks <instr_refl >addr_refl |
---|
1559 | [1,4: |
---|
1560 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1561 | [1,3: |
---|
1562 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1563 | |2,4: |
---|
1564 | @eq_f2 % |
---|
1565 | ] |
---|
1566 | |2,5: |
---|
1567 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) |
---|
1568 | [1,3: @(subaddressing_mode_elim … acc_a) % ] % |
---|
1569 | |3,6: |
---|
1570 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
1571 | [1,5: |
---|
1572 | @(subaddressing_mode_elim … acc_a) % |
---|
1573 | |4,8: |
---|
1574 | @eq_f2 |
---|
1575 | @(pose … (set_clock ????)) #status #status_refl |
---|
1576 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1577 | [1,5: |
---|
1578 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
1579 | [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ] |
---|
1580 | |3,7: |
---|
1581 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
1582 | [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1583 | |2,6: |
---|
1584 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) |
---|
1585 | [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ] |
---|
1586 | |4,8: |
---|
1587 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
1588 | [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1589 | ] |
---|
1590 | |*: |
---|
1591 | % |
---|
1592 | ] |
---|
1593 | ] |
---|
1594 | |2,4: |
---|
1595 | #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl |
---|
1596 | >EQP -P normalize nodelta |
---|
1597 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1598 | whd in maps_assm:(??%%); |
---|
1599 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1600 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1601 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1602 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1603 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1604 | whd in ⊢ (??%?); |
---|
1605 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1606 | change with (set_arg_8 ????? = ?) |
---|
1607 | @set_arg_8_status_of_pseudo_status try % |
---|
1608 | >EQs >EQticks <instr_refl >addr_refl |
---|
1609 | [1,4: |
---|
1610 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1611 | [1,3: |
---|
1612 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1613 | |2,4: |
---|
1614 | @eq_f2 % |
---|
1615 | ] |
---|
1616 | |2,5: |
---|
1617 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) |
---|
1618 | [1,3: @(subaddressing_mode_elim … direct) #w % ] % |
---|
1619 | |3,6: |
---|
1620 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) |
---|
1621 | [1,5: |
---|
1622 | @(subaddressing_mode_elim … direct) #w % |
---|
1623 | |4,8: |
---|
1624 | @eq_f2 |
---|
1625 | @(pose … (set_clock ????)) #status #status_refl |
---|
1626 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1627 | [1,5: |
---|
1628 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) |
---|
1629 | [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ] |
---|
1630 | |3,7: |
---|
1631 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
1632 | [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1633 | |2,6: |
---|
1634 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) |
---|
1635 | [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ] |
---|
1636 | |4,8: |
---|
1637 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
1638 | [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1639 | ] |
---|
1640 | |*: |
---|
1641 | % |
---|
1642 | ] |
---|
1643 | ] |
---|
1644 | ] |
---|
1645 | |2,4: |
---|
1646 | #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl |
---|
1647 | >EQP -P normalize nodelta |
---|
1648 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1649 | whd in maps_assm:(??%%); |
---|
1650 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1651 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1652 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1653 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1654 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1655 | whd in ⊢ (??%?); |
---|
1656 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1657 | change with (set_flags ?????? = ?) |
---|
1658 | [1,4: @set_flags_status_of_pseudo_status try % |*: skip ] |
---|
1659 | >EQs >EQticks <instr_refl >addr_refl |
---|
1660 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1661 | ] |
---|
1662 | |31: (* XRL *) |
---|
1663 | inversion addr |
---|
1664 | [1: |
---|
1665 | #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl |
---|
1666 | >EQP -P normalize nodelta |
---|
1667 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1668 | whd in maps_assm:(??%%); |
---|
1669 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1670 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1671 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1672 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1673 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1674 | whd in ⊢ (??%?); |
---|
1675 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1676 | change with (set_arg_8 ????? = ?) |
---|
1677 | @set_arg_8_status_of_pseudo_status try % |
---|
1678 | >EQs >EQticks <instr_refl >addr_refl |
---|
1679 | [1: |
---|
1680 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1681 | [1: |
---|
1682 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1683 | |2: |
---|
1684 | @eq_f2 % |
---|
1685 | ] |
---|
1686 | |2: |
---|
1687 | @(subaddressing_mode_elim … acc_a) @I |
---|
1688 | |3: |
---|
1689 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
1690 | [1: |
---|
1691 | @(subaddressing_mode_elim … acc_a) % |
---|
1692 | |4: |
---|
1693 | @eq_f2 |
---|
1694 | @(pose … (set_clock ????)) #status #status_refl |
---|
1695 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1696 | [1: |
---|
1697 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
1698 | [1: @(subaddressing_mode_elim … acc_a) % |*: % ] |
---|
1699 | |3: |
---|
1700 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
1701 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1702 | |2: |
---|
1703 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) |
---|
1704 | [1: @(subaddressing_mode_elim … acc_a) % |2: % ] |
---|
1705 | |4: |
---|
1706 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
1707 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1708 | ] |
---|
1709 | |*: |
---|
1710 | % |
---|
1711 | ] |
---|
1712 | ] |
---|
1713 | |2: |
---|
1714 | #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl |
---|
1715 | >EQP -P normalize nodelta |
---|
1716 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1717 | whd in maps_assm:(??%%); |
---|
1718 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1719 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1720 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1721 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1722 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1723 | whd in ⊢ (??%?); |
---|
1724 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1725 | change with (set_arg_8 ????? = ?) |
---|
1726 | @set_arg_8_status_of_pseudo_status try % |
---|
1727 | >EQs >EQticks <instr_refl >addr_refl |
---|
1728 | [1: |
---|
1729 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1730 | [1: |
---|
1731 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1732 | |2: |
---|
1733 | @eq_f2 % |
---|
1734 | ] |
---|
1735 | |2: |
---|
1736 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) |
---|
1737 | [1: @(subaddressing_mode_elim … direct) #w % ] % |
---|
1738 | |3: |
---|
1739 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) |
---|
1740 | [1: |
---|
1741 | @(subaddressing_mode_elim … direct) #w % |
---|
1742 | |4: |
---|
1743 | @eq_f2 |
---|
1744 | @(pose … (set_clock ????)) #status #status_refl |
---|
1745 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1746 | [1: |
---|
1747 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) |
---|
1748 | [1: @(subaddressing_mode_elim … direct) #w % |*: % ] |
---|
1749 | |3: |
---|
1750 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
1751 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1752 | |2: |
---|
1753 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) |
---|
1754 | [1: @(subaddressing_mode_elim … direct) #w % |2: % ] |
---|
1755 | |4: |
---|
1756 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
1757 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1758 | ] |
---|
1759 | |*: |
---|
1760 | % |
---|
1761 | ] |
---|
1762 | ] |
---|
1763 | ] |
---|
1764 | |32: (* CLR *) |
---|
1765 | >EQP -P normalize nodelta lapply instr_refl |
---|
1766 | @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta |
---|
1767 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1768 | whd in maps_assm:(??%%); |
---|
1769 | [1,2: |
---|
1770 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1771 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1772 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1773 | whd in ⊢ (??%?); |
---|
1774 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1775 | [1: |
---|
1776 | >EQs >EQticks <instr_refl |
---|
1777 | change with (set_arg_1 ??? (BIT_ADDR w) ? = ?) |
---|
1778 | @set_arg_1_status_of_pseudo_status try % |
---|
1779 | [1: |
---|
1780 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) % |
---|
1781 | |2: |
---|
1782 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) % |
---|
1783 | ] |
---|
1784 | |2: |
---|
1785 | >EQs >EQticks <instr_refl |
---|
1786 | change with (set_arg_8 ??? ACC_A ? = ?) try % |
---|
1787 | @set_arg_8_status_of_pseudo_status try % |
---|
1788 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % |
---|
1789 | ] |
---|
1790 | |3: |
---|
1791 | lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1792 | whd in ⊢ (??%?); |
---|
1793 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1794 | >EQs >EQticks <instr_refl |
---|
1795 | change with (set_arg_1 ??? CARRY ? = ?) try % |
---|
1796 | @set_arg_1_status_of_pseudo_status % |
---|
1797 | ] |
---|
1798 | |33: (* CPL *) |
---|
1799 | >EQP -P normalize nodelta lapply instr_refl |
---|
1800 | @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta |
---|
1801 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1802 | whd in maps_assm:(??%%); |
---|
1803 | [1,2: |
---|
1804 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1805 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1806 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1807 | whd in ⊢ (??%?); |
---|
1808 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1809 | [1: |
---|
1810 | >EQs >EQticks <instr_refl |
---|
1811 | change with (set_arg_1 ??? (BIT_ADDR w) ? = ?) |
---|
1812 | @set_arg_1_status_of_pseudo_status |
---|
1813 | [1: |
---|
1814 | @eq_f |
---|
1815 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
1816 | @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
1817 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) % |
---|
1818 | |2: |
---|
1819 | % |
---|
1820 | |3: |
---|
1821 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) % |
---|
1822 | |4: |
---|
1823 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) % |
---|
1824 | ] |
---|
1825 | |2: |
---|
1826 | >EQs >EQticks <instr_refl |
---|
1827 | change with (set_8051_sfr ????? = ?) |
---|
1828 | @set_8051_sfr_status_of_pseudo_status try % |
---|
1829 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try % |
---|
1830 | normalize nodelta @eq_f |
---|
1831 | @(pose … (set_clock ????)) #status #status_refl |
---|
1832 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
1833 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) % |
---|
1834 | ] |
---|
1835 | |3: |
---|
1836 | lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1837 | whd in ⊢ (??%?); |
---|
1838 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1839 | >EQs >EQticks <instr_refl |
---|
1840 | change with (set_arg_1 ??? CARRY ? = ?) try % |
---|
1841 | @set_arg_1_status_of_pseudo_status try % |
---|
1842 | @eq_f |
---|
1843 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
1844 | @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl % |
---|
1845 | ] |
---|
1846 | |34,36: (* RL and RR *) |
---|
1847 | (* XXX: work on the right hand side *) |
---|
1848 | (* XXX: switch to the left hand side *) |
---|
1849 | >EQP -P normalize nodelta |
---|
1850 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1851 | whd in maps_assm:(??%%); |
---|
1852 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm |
---|
1853 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1854 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1855 | whd in ⊢ (??%?); |
---|
1856 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
1857 | change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status |
---|
1858 | [2,4: |
---|
1859 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) |
---|
1860 | @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1861 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) |
---|
1862 | % |
---|
1863 | ] |
---|
1864 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1865 | [2,4: |
---|
1866 | % |
---|
1867 | ] |
---|
1868 | @sym_eq @set_program_counter_status_of_pseudo_status % |
---|
1869 | |35,37: (* RLC and RRC *) |
---|
1870 | (* XXX: work on the right hand side *) |
---|
1871 | (* XXX: switch to the left hand side *) |
---|
1872 | >EQP -P normalize nodelta |
---|
1873 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1874 | whd in maps_assm:(??%%); |
---|
1875 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm |
---|
1876 | [2,4: normalize nodelta #absurd destruct(absurd) ] |
---|
1877 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1878 | whd in ⊢ (??%?); |
---|
1879 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
1880 | change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status |
---|
1881 | [2,4: |
---|
1882 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) |
---|
1883 | @eq_f2 |
---|
1884 | [1,3: |
---|
1885 | @sym_eq |
---|
1886 | @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1887 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % |
---|
1888 | |2,4: |
---|
1889 | @sym_eq @(get_cy_flag_status_of_pseudo_status … M') |
---|
1890 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1891 | ] |
---|
1892 | |1,3: |
---|
1893 | @sym_eq @set_arg_1_status_of_pseudo_status try % |
---|
1894 | @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) |
---|
1895 | >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % |
---|
1896 | ] |
---|
1897 | |38: (* SWAP *) |
---|
1898 | >EQP -P normalize nodelta |
---|
1899 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1900 | whd in maps_assm:(??%%); |
---|
1901 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1902 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1903 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1904 | whd in ⊢ (??%?); |
---|
1905 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1906 | whd in ⊢ (??%?); |
---|
1907 | @(pair_replace ?????????? p) |
---|
1908 | [1: |
---|
1909 | @eq_f normalize nodelta |
---|
1910 | @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq |
---|
1911 | @(get_8051_sfr_status_of_pseudo_status … M' … status) |
---|
1912 | [1: |
---|
1913 | >status_refl -status_refl |
---|
1914 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1915 | >EQs >EQticks <instr_refl % |
---|
1916 | |2: |
---|
1917 | whd in ⊢ (??%?); |
---|
1918 | >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1919 | ] |
---|
1920 | |2: |
---|
1921 | @(pair_replace ?????????? p) normalize nodelta |
---|
1922 | [1: |
---|
1923 | % |
---|
1924 | |2: |
---|
1925 | @set_8051_sfr_status_of_pseudo_status |
---|
1926 | [1: |
---|
1927 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1928 | >EQs >EQticks <instr_refl % |
---|
1929 | |2: |
---|
1930 | whd in ⊢ (??%?); |
---|
1931 | >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
1932 | ] |
---|
1933 | ] |
---|
1934 | ] |
---|
1935 | |39: (* MOV *) |
---|
1936 | >EQP -P normalize nodelta |
---|
1937 | inversion addr |
---|
1938 | [1: |
---|
1939 | #addr' normalize nodelta |
---|
1940 | inversion addr' |
---|
1941 | [1: |
---|
1942 | #addr'' normalize nodelta |
---|
1943 | inversion addr'' |
---|
1944 | [1: |
---|
1945 | #addr''' normalize nodelta |
---|
1946 | inversion addr''' |
---|
1947 | [1: |
---|
1948 | #addr'''' normalize nodelta |
---|
1949 | inversion addr'''' |
---|
1950 | [1: |
---|
1951 | normalize nodelta #acc_a_others |
---|
1952 | cases acc_a_others #acc_a #others |
---|
1953 | #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl |
---|
1954 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1955 | whd in maps_assm:(??%%); |
---|
1956 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1957 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1958 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1959 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1960 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
1961 | whd in ⊢ (??%?); |
---|
1962 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
1963 | change with (set_arg_8 ????? = ?) |
---|
1964 | @set_arg_8_status_of_pseudo_status try % |
---|
1965 | [1: |
---|
1966 | @sym_eq @set_clock_status_of_pseudo_status |
---|
1967 | >EQs >EQticks <instr_refl >addr_refl % |
---|
1968 | |2: |
---|
1969 | @(subaddressing_mode_elim … acc_a) @I |
---|
1970 | |3: |
---|
1971 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
1972 | [1: @(subaddressing_mode_elim … acc_a) % ] |
---|
1973 | >EQs >EQticks <instr_refl >addr_refl |
---|
1974 | [1,2: |
---|
1975 | % |
---|
1976 | |3: |
---|
1977 | @(pose … (set_clock ????)) #status #status_refl |
---|
1978 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
1979 | [1: |
---|
1980 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
1981 | |2: |
---|
1982 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
1983 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1984 | |3: |
---|
1985 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
1986 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
1987 | ] |
---|
1988 | ] |
---|
1989 | ] |
---|
1990 | |2: |
---|
1991 | #others_others' cases others_others' #others #others' normalize nodelta |
---|
1992 | #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl |
---|
1993 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
1994 | whd in maps_assm:(??%%); |
---|
1995 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
1996 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1997 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
1998 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
1999 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2000 | whd in ⊢ (??%?); |
---|
2001 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2002 | change with (set_arg_8 ????? = ?) |
---|
2003 | @set_arg_8_status_of_pseudo_status try % |
---|
2004 | >EQs >EQticks <instr_refl >addr_refl try % |
---|
2005 | [1: |
---|
2006 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1) |
---|
2007 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2008 | |2: |
---|
2009 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) |
---|
2010 | [1: |
---|
2011 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2012 | |2,3: |
---|
2013 | % |
---|
2014 | |4: |
---|
2015 | @(pose … (set_clock ????)) #status #status_refl |
---|
2016 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl |
---|
2017 | [1: |
---|
2018 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
2019 | |2: |
---|
2020 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2) |
---|
2021 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2022 | |3: |
---|
2023 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2) |
---|
2024 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2025 | ] |
---|
2026 | ] |
---|
2027 | ] |
---|
2028 | ] |
---|
2029 | |2: |
---|
2030 | #direct_others cases direct_others #direct #others |
---|
2031 | #addr_refl''' #addr_refl'' #addr_refl' #addr_refl |
---|
2032 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2033 | whd in maps_assm:(??%%); |
---|
2034 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2035 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2036 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2037 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2038 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2039 | whd in ⊢ (??%?); |
---|
2040 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2041 | change with (set_arg_8 ????? = ?) |
---|
2042 | @set_arg_8_status_of_pseudo_status try % |
---|
2043 | >EQs >EQticks <instr_refl >addr_refl |
---|
2044 | [1: |
---|
2045 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
2046 | |2: |
---|
2047 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) |
---|
2048 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2049 | |3: |
---|
2050 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) |
---|
2051 | [1: |
---|
2052 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2053 | |2,3: |
---|
2054 | % |
---|
2055 | |4: |
---|
2056 | @(pose … (set_clock ????)) #status #status_refl |
---|
2057 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2058 | [1: |
---|
2059 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
2060 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2061 | |2: |
---|
2062 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
2063 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2064 | ] |
---|
2065 | ] |
---|
2066 | ] |
---|
2067 | ] |
---|
2068 | |2: |
---|
2069 | #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta |
---|
2070 | #addr_refl'' #addr_refl' #addr_refl |
---|
2071 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2072 | whd in maps_assm:(??%%); |
---|
2073 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2074 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2075 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2076 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2077 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2078 | whd in ⊢ (??%?); |
---|
2079 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2080 | change with (set_arg_16 ????? = ?) |
---|
2081 | @set_arg_16_status_of_pseudo_status try % |
---|
2082 | >EQs >EQticks <instr_refl >addr_refl |
---|
2083 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
2084 | ] |
---|
2085 | |2: |
---|
2086 | #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta |
---|
2087 | #addr_refl' #addr_refl |
---|
2088 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2089 | whd in maps_assm:(??%%); |
---|
2090 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2091 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2092 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2093 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2094 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2095 | whd in ⊢ (??%?); |
---|
2096 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2097 | change with (set_arg_1 ????? = ?) |
---|
2098 | @set_arg_1_status_of_pseudo_status |
---|
2099 | >EQs >EQticks <instr_refl >addr_refl try % |
---|
2100 | [1: |
---|
2101 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
2102 | @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2103 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2) |
---|
2104 | |2,3: |
---|
2105 | @(subaddressing_mode_elim … carry) @I |
---|
2106 | ] |
---|
2107 | ] |
---|
2108 | |2: |
---|
2109 | #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta |
---|
2110 | #addr_refl |
---|
2111 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2112 | whd in maps_assm:(??%%); |
---|
2113 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2114 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2115 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2116 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2117 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2118 | whd in ⊢ (??%?); |
---|
2119 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2120 | change with (set_arg_1 ????? = ?) |
---|
2121 | @set_arg_1_status_of_pseudo_status |
---|
2122 | [1: |
---|
2123 | >EQs >EQticks <instr_refl >addr_refl |
---|
2124 | @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq |
---|
2125 | @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2126 | @(subaddressing_mode_elim … carry) @I |
---|
2127 | |2: |
---|
2128 | >EQs >EQticks <instr_refl >addr_refl % |
---|
2129 | |3,4: |
---|
2130 | @(pose … (set_clock ????)) #status #status_refl |
---|
2131 | [1: |
---|
2132 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try % |
---|
2133 | |2: |
---|
2134 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try % |
---|
2135 | ] |
---|
2136 | >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl |
---|
2137 | lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?); |
---|
2138 | @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption |
---|
2139 | ] |
---|
2140 | ] |
---|
2141 | |40: (* MOVX *) |
---|
2142 | >EQP -P normalize nodelta |
---|
2143 | inversion addr |
---|
2144 | [1: |
---|
2145 | #acc_a_others cases acc_a_others #acc_a #others normalize nodelta |
---|
2146 | #addr_refl |
---|
2147 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2148 | whd in maps_assm:(??%%); |
---|
2149 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2150 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2151 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2152 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2153 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2154 | whd in ⊢ (??%?); |
---|
2155 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2156 | change with (set_arg_8 ????? = ?) |
---|
2157 | @set_arg_8_status_of_pseudo_status try % |
---|
2158 | >EQs >EQticks <instr_refl >addr_refl |
---|
2159 | [1: |
---|
2160 | @sym_eq @set_clock_status_of_pseudo_status % |
---|
2161 | |2: |
---|
2162 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) |
---|
2163 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2164 | |3: |
---|
2165 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) |
---|
2166 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try % |
---|
2167 | @(pose … (set_clock ????)) #status #status_refl |
---|
2168 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2169 | [1: |
---|
2170 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) |
---|
2171 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2172 | |2: |
---|
2173 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) |
---|
2174 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2175 | ] |
---|
2176 | ] |
---|
2177 | |2: |
---|
2178 | #others_acc_a cases others_acc_a #others #acc_a |
---|
2179 | #addr_refl |
---|
2180 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2181 | whd in maps_assm:(??%%); |
---|
2182 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2183 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2184 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2185 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2186 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2187 | whd in ⊢ (??%?); |
---|
2188 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2189 | change with (set_arg_8 ????? = ?) |
---|
2190 | @set_arg_8_status_of_pseudo_status |
---|
2191 | >EQs >EQticks <instr_refl >addr_refl try % |
---|
2192 | [1: |
---|
2193 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1) |
---|
2194 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2195 | |2: |
---|
2196 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) |
---|
2197 | [1: |
---|
2198 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2199 | |2,3: |
---|
2200 | % |
---|
2201 | |4: |
---|
2202 | @(pose … (set_clock ????)) #status #status_refl |
---|
2203 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2204 | [1: |
---|
2205 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2) |
---|
2206 | [1: @(subaddressing_mode_elim … acc_a) % ] % |
---|
2207 | |2: |
---|
2208 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2) |
---|
2209 | [1: @(subaddressing_mode_elim … acc_a) % ] % |
---|
2210 | ] |
---|
2211 | ] |
---|
2212 | ] |
---|
2213 | ] |
---|
2214 | |41: (* SETB *) |
---|
2215 | >EQs >EQticks <instr_refl |
---|
2216 | >EQP -P normalize nodelta |
---|
2217 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2218 | whd in maps_assm:(??%%); |
---|
2219 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2220 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2221 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2222 | whd in ⊢ (??%?); |
---|
2223 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2224 | change with (set_arg_1 ????? = ?) |
---|
2225 | @set_arg_1_status_of_pseudo_status try % |
---|
2226 | [1: |
---|
2227 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) |
---|
2228 | |2: |
---|
2229 | @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) |
---|
2230 | ] |
---|
2231 | |42: (* PUSH *) |
---|
2232 | >EQP -P normalize nodelta lapply instr_refl |
---|
2233 | @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta |
---|
2234 | #sigma_increment_commutation |
---|
2235 | whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta |
---|
2236 | @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1} |
---|
2237 | whd in ⊢ (??%?); |
---|
2238 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2239 | whd in ⊢ (??%?); |
---|
2240 | @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta |
---|
2241 | @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl)) |
---|
2242 | [1: |
---|
2243 | @eq_f2 try % |
---|
2244 | @(pose … (set_clock ????)) #status #status_refl |
---|
2245 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try % |
---|
2246 | @sym_eq @set_clock_status_of_pseudo_status |
---|
2247 | >EQs >EQticks <instr_refl % |
---|
2248 | |2: |
---|
2249 | >EQs >EQticks <instr_refl |
---|
2250 | cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *) |
---|
2251 | ] |
---|
2252 | |*)43: (* POP *) |
---|
2253 | |44: |
---|
2254 | >EQP -P normalize nodelta |
---|
2255 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2256 | whd in maps_assm:(??%%); |
---|
2257 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2258 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2259 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2260 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2261 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2262 | whd in ⊢ (??%?); |
---|
2263 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2264 | change with (set_arg_8 ????? = ?) |
---|
2265 | >EQs >EQticks <instr_refl |
---|
2266 | @set_arg_8_status_of_pseudo_status try % |
---|
2267 | [1: |
---|
2268 | @sym_eq @set_8051_sfr_status_of_pseudo_status try % |
---|
2269 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta |
---|
2270 | @(pose … (set_clock ????)) #status #status_refl |
---|
2271 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2272 | [1: |
---|
2273 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) |
---|
2274 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ] |
---|
2275 | |2: |
---|
2276 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) |
---|
2277 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ] |
---|
2278 | ] |
---|
2279 | |2: |
---|
2280 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) |
---|
2281 | [1: |
---|
2282 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2283 | |*: |
---|
2284 | whd in match get_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2285 | whd in match set_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2286 | whd in match sfr_8051_index; normalize nodelta |
---|
2287 | >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % |
---|
2288 | ] |
---|
2289 | |3: |
---|
2290 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % |
---|
2291 | [1: |
---|
2292 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2293 | |2: |
---|
2294 | whd in match get_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2295 | whd in match set_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2296 | whd in match sfr_8051_index; normalize nodelta |
---|
2297 | >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % |
---|
2298 | |3: |
---|
2299 | @(pose … (set_clock ????)) #status #status_refl |
---|
2300 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
2301 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
2302 | ] |
---|
2303 | ] |
---|
2304 | |45: (* XCHD *) |
---|
2305 | >EQP -P normalize nodelta |
---|
2306 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2307 | whd in maps_assm:(??%%); |
---|
2308 | inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 |
---|
2309 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2310 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 |
---|
2311 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2312 | normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2313 | whd in ⊢ (??%?); |
---|
2314 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2315 | whd in ⊢ (??%?); |
---|
2316 | @(pair_replace ?????????? p) normalize nodelta |
---|
2317 | >EQs >EQticks <instr_refl |
---|
2318 | [1: |
---|
2319 | @eq_f |
---|
2320 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
2321 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % |
---|
2322 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
2323 | |2: |
---|
2324 | @(pair_replace ?????????? p1) normalize nodelta |
---|
2325 | >EQs >EQticks <instr_refl |
---|
2326 | [1: |
---|
2327 | @eq_f |
---|
2328 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
2329 | @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % |
---|
2330 | [1: |
---|
2331 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) |
---|
2332 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ] |
---|
2333 | |2: |
---|
2334 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) |
---|
2335 | [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ] |
---|
2336 | ] |
---|
2337 | |2: |
---|
2338 | @(pair_replace ?????????? p) normalize nodelta |
---|
2339 | >EQs >EQticks <instr_refl |
---|
2340 | [1: |
---|
2341 | % |
---|
2342 | |2: |
---|
2343 | @(pair_replace ?????????? p1) normalize nodelta |
---|
2344 | >EQs >EQticks <instr_refl |
---|
2345 | [1: |
---|
2346 | % |
---|
2347 | |2: |
---|
2348 | @set_arg_8_status_of_pseudo_status try % |
---|
2349 | [1: |
---|
2350 | @sym_eq @set_8051_sfr_status_of_pseudo_status try % |
---|
2351 | whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) % |
---|
2352 | |2: |
---|
2353 | @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) |
---|
2354 | [1: |
---|
2355 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2356 | |2: |
---|
2357 | whd in match get_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2358 | whd in match set_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2359 | whd in match sfr_8051_index; normalize nodelta |
---|
2360 | >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % |
---|
2361 | ] |
---|
2362 | |3: |
---|
2363 | @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % |
---|
2364 | [1: |
---|
2365 | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |
---|
2366 | |2: |
---|
2367 | whd in match get_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2368 | whd in match set_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2369 | whd in match sfr_8051_index; normalize nodelta |
---|
2370 | >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] % |
---|
2371 | ] |
---|
2372 | ] |
---|
2373 | ] |
---|
2374 | ] |
---|
2375 | ] |
---|
2376 | ] |
---|
2377 | |46: (* RET *) |
---|
2378 | >EQP -P normalize nodelta |
---|
2379 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2380 | whd in maps_assm:(??%%); normalize nodelta in maps_assm; |
---|
2381 | lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta |
---|
2382 | inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1 |
---|
2383 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2384 | inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2 |
---|
2385 | [2: normalize nodelta #absurd destruct(absurd) ] |
---|
2386 | normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl) |
---|
2387 | whd in ⊢ (??%?); |
---|
2388 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm |
---|
2389 | whd in ⊢ (??%?); |
---|
2390 | @(pair_replace ?????????? p) normalize nodelta |
---|
2391 | >EQs >EQticks <instr_refl |
---|
2392 | [1: |
---|
2393 | @eq_f3 try % |
---|
2394 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
2395 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl % |
---|
2396 | |2: |
---|
2397 | @(pair_replace ?????????? p1) normalize nodelta |
---|
2398 | >EQs >EQticks <instr_refl |
---|
2399 | [1: |
---|
2400 | @eq_f3 try % |
---|
2401 | @sym_eq @(pose … (set_clock ????)) #status #status_refl |
---|
2402 | @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl |
---|
2403 | [1: |
---|
2404 | cases daemon |
---|
2405 | (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) |
---|
2406 | |2: |
---|
2407 | whd in match get_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2408 | whd in match set_8051_sfr in ⊢ (???%); normalize nodelta |
---|
2409 | whd in match sfr_8051_index; normalize nodelta |
---|
2410 | >get_index_v_set_index_hit |
---|
2411 | change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp) |
---|
2412 | cases daemon |
---|
2413 | (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) |
---|
2414 | ] |
---|
2415 | |2: |
---|
2416 | cases daemon (* XXX *) |
---|
2417 | ] |
---|
2418 | ] |
---|
2419 | |47: (* POP *) |
---|
2420 | |48: (* XCH *) |
---|
2421 | |49: (* XCHD *) |
---|
2422 | |50: (* RET *) |
---|
2423 | |51: (* RETI *) |
---|
2424 | |52: (* NOP *) |
---|
2425 | >EQP -P normalize nodelta |
---|
2426 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2427 | whd in maps_assm:(??%%); |
---|
2428 | lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl) |
---|
2429 | whd in ⊢ (??%?); |
---|
2430 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl |
---|
2431 | change with (set_clock ???? = ?) |
---|
2432 | @set_clock_status_of_pseudo_status % |
---|
2433 | ] |
---|
2434 | cases daemon |
---|
2435 | qed. |
---|
2436 | |
---|
2437 | (* |
---|
2438 | (* XXX: work on the left hand side *) |
---|
2439 | (* XXX: switch to the right hand side *) |
---|
2440 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2441 | whd in ⊢ (??%%); |
---|
2442 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2443 | cases daemon |
---|
2444 | |11,12: (* DIV *) |
---|
2445 | (* XXX: work on the right hand side *) |
---|
2446 | normalize nodelta in p; |
---|
2447 | >p normalize nodelta |
---|
2448 | (* XXX: switch to the left hand side *) |
---|
2449 | -instr_refl >EQP -P normalize nodelta |
---|
2450 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2451 | whd in ⊢ (??%?); |
---|
2452 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2453 | @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl |
---|
2454 | >(?: pose_assm = 0) normalize nodelta |
---|
2455 | [2,4: |
---|
2456 | <p >pose_refl |
---|
2457 | cases daemon |
---|
2458 | |1,3: |
---|
2459 | (* XXX: switch to the right hand side *) |
---|
2460 | >EQs -s >EQticks -ticks |
---|
2461 | whd in ⊢ (??%%); |
---|
2462 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2463 | @split_eq_status try % |
---|
2464 | cases daemon |
---|
2465 | ] |
---|
2466 | |13,14,15: (* DA *) |
---|
2467 | (* XXX: work on the right hand side *) |
---|
2468 | >p normalize nodelta |
---|
2469 | >p1 normalize nodelta |
---|
2470 | try (>p2 normalize nodelta |
---|
2471 | try (>p3 normalize nodelta |
---|
2472 | try (>p4 normalize nodelta |
---|
2473 | try (>p5 normalize nodelta)))) |
---|
2474 | (* XXX: switch to the left hand side *) |
---|
2475 | -instr_refl >EQP -P normalize nodelta |
---|
2476 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2477 | whd in ⊢ (??%?); |
---|
2478 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2479 | (* XXX: work on the left hand side *) |
---|
2480 | @(pair_replace ?????????? p) |
---|
2481 | [1,3,5: |
---|
2482 | /demod/ |
---|
2483 | cases daemon |
---|
2484 | |2,4,6: |
---|
2485 | @(if_then_else_replace ???????? p1) |
---|
2486 | [1,3,5: |
---|
2487 | cases daemon |
---|
2488 | |2,4: |
---|
2489 | normalize nodelta |
---|
2490 | @(pair_replace ?????????? p2) |
---|
2491 | [1,3: |
---|
2492 | cases daemon |
---|
2493 | |2,4: |
---|
2494 | normalize nodelta >p3 normalize nodelta |
---|
2495 | >p4 normalize nodelta try >p5 |
---|
2496 | ] |
---|
2497 | ] |
---|
2498 | (* XXX: switch to the right hand side *) |
---|
2499 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2500 | whd in ⊢ (??%%); |
---|
2501 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2502 | @split_eq_status try % |
---|
2503 | cases daemon |
---|
2504 | ] |
---|
2505 | |33,34,35,48: (* ANL, ORL, XRL, MOVX *) |
---|
2506 | (* XXX: work on the right hand side *) |
---|
2507 | cases addr #addr' normalize nodelta |
---|
2508 | [1,3: |
---|
2509 | cases addr' #addr'' normalize nodelta |
---|
2510 | ] |
---|
2511 | @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta |
---|
2512 | (* XXX: switch to the left hand side *) |
---|
2513 | -instr_refl >EQP -P normalize nodelta |
---|
2514 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2515 | whd in ⊢ (??%?); |
---|
2516 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2517 | (* XXX: work on the left hand side *) |
---|
2518 | (* XXX: switch to the right hand side *) |
---|
2519 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2520 | whd in ⊢ (??%%); |
---|
2521 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2522 | cases daemon |
---|
2523 | |47: (* MOV *) |
---|
2524 | (* XXX: work on the right hand side *) |
---|
2525 | cases addr -addr #addr normalize nodelta |
---|
2526 | [1: |
---|
2527 | cases addr #addr normalize nodelta |
---|
2528 | [1: |
---|
2529 | cases addr #addr normalize nodelta |
---|
2530 | [1: |
---|
2531 | cases addr #addr normalize nodelta |
---|
2532 | [1: |
---|
2533 | cases addr #addr normalize nodelta |
---|
2534 | ] |
---|
2535 | ] |
---|
2536 | ] |
---|
2537 | ] |
---|
2538 | cases addr #lft #rgt normalize nodelta |
---|
2539 | (* XXX: switch to the left hand side *) |
---|
2540 | >EQP -P normalize nodelta |
---|
2541 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
2542 | whd in ⊢ (??%?); |
---|
2543 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2544 | (* XXX: work on the left hand side *) |
---|
2545 | (* XXX: switch to the right hand side *) |
---|
2546 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2547 | whd in ⊢ (??%%); |
---|
2548 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2549 | cases daemon |
---|
2550 | ] |
---|
2551 | *) |
---|
2552 | |
---|
2553 | |
---|
2554 | (* [31,32: (* DJNZ *) |
---|
2555 | (* XXX: work on the right hand side *) |
---|
2556 | >p normalize nodelta >p1 normalize nodelta |
---|
2557 | (* XXX: switch to the left hand side *) |
---|
2558 | >EQP -P normalize nodelta |
---|
2559 | #sigma_increment_commutation #maps_assm #fetch_many_assm |
---|
2560 | whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; |
---|
2561 | <EQppc in fetch_many_assm; |
---|
2562 | whd in match (short_jump_cond ??); |
---|
2563 | @pair_elim #sj_possible #disp |
---|
2564 | @pair_elim #result #flags #sub16_refl |
---|
2565 | @pair_elim #upper #lower #vsplit_refl |
---|
2566 | inversion (get_index' bool ???) #get_index_refl' normalize nodelta |
---|
2567 | #sj_possible_pair destruct(sj_possible_pair) |
---|
2568 | >p1 normalize nodelta |
---|
2569 | [1,3: |
---|
2570 | >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} |
---|
2571 | >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; |
---|
2572 | normalize nodelta in ⊢ (% → ?); #fetch_many_assm |
---|
2573 | whd in ⊢ (??%?); |
---|
2574 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2575 | lapply maps_assm whd in ⊢ (??%? → ?); |
---|
2576 | inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta |
---|
2577 | [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M' |
---|
2578 | (* XXX: work on the left hand side *) |
---|
2579 | @(pair_replace ?????????? p) normalize nodelta |
---|
2580 | [1,3: |
---|
2581 | >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) |
---|
2582 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] |
---|
2583 | >(get_arg_8_set_program_counter … true addr1) |
---|
2584 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] |
---|
2585 | @get_arg_8_pseudo_addressing_mode_ok assumption |
---|
2586 | |2,4: |
---|
2587 | >p1 normalize nodelta >EQs |
---|
2588 | alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)". |
---|
2589 | >set_program_counter_status_of_pseudo_status |
---|
2590 | whd in ⊢ (??%%); |
---|
2591 | @split_eq_status |
---|
2592 | [1,10: |
---|
2593 | whd in ⊢ (??%%); >set_arg_8_set_program_counter |
---|
2594 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] |
---|
2595 | >low_internal_ram_set_program_counter |
---|
2596 | [1: |
---|
2597 | >low_internal_ram_set_program_counter |
---|
2598 | (* XXX: ??? *) |
---|
2599 | |2: |
---|
2600 | >low_internal_ram_set_clock |
---|
2601 | (* XXX: ??? *) |
---|
2602 | ] |
---|
2603 | |2,11: |
---|
2604 | whd in ⊢ (??%%); >set_arg_8_set_program_counter |
---|
2605 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] |
---|
2606 | >high_internal_ram_set_program_counter |
---|
2607 | [1: |
---|
2608 | >high_internal_ram_set_program_counter |
---|
2609 | (* XXX: ??? *) |
---|
2610 | |2: |
---|
2611 | >high_internal_ram_set_clock |
---|
2612 | (* XXX: ??? *) |
---|
2613 | ] |
---|
2614 | |3,12: |
---|
2615 | whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); |
---|
2616 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] |
---|
2617 | >(external_ram_set_arg_8 ??? addr1) |
---|
2618 | [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % |
---|
2619 | |4,13: |
---|
2620 | whd in ⊢ (??%%); >EQaddr_of normalize nodelta |
---|
2621 | [1: |
---|
2622 | >program_counter_set_program_counter |
---|
2623 | >set_arg_8_set_program_counter |
---|
2624 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] |
---|
2625 | >set_clock_set_program_counter >program_counter_set_program_counter |
---|
2626 | change with (add ??? = ?) |
---|
2627 | (* XXX: ??? *) |
---|
2628 | |2: |
---|
2629 | >set_arg_8_set_program_counter |
---|
2630 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] |
---|
2631 | >program_counter_set_program_counter |
---|
2632 | >set_arg_8_set_program_counter |
---|
2633 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2634 | >set_clock_set_program_counter >program_counter_set_program_counter |
---|
2635 | >sigma_increment_commutation <EQppc |
---|
2636 | whd in match (assembly_1_pseudoinstruction ??????); |
---|
2637 | whd in match (expand_pseudo_instruction ??????); |
---|
2638 | (* XXX: ??? *) |
---|
2639 | ] |
---|
2640 | |5,14: |
---|
2641 | whd in match (special_function_registers_8051 ???); |
---|
2642 | [1: |
---|
2643 | >special_function_registers_8051_set_program_counter |
---|
2644 | >special_function_registers_8051_set_clock |
---|
2645 | >set_arg_8_set_program_counter in ⊢ (???%); |
---|
2646 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2647 | >special_function_registers_8051_set_program_counter |
---|
2648 | >set_arg_8_set_program_counter |
---|
2649 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2650 | >special_function_registers_8051_set_program_counter |
---|
2651 | @special_function_registers_8051_set_arg_8 assumption |
---|
2652 | |2: |
---|
2653 | >special_function_registers_8051_set_clock |
---|
2654 | >set_arg_8_set_program_counter |
---|
2655 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2656 | >set_arg_8_set_program_counter |
---|
2657 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2658 | >special_function_registers_8051_set_program_counter |
---|
2659 | >special_function_registers_8051_set_program_counter |
---|
2660 | @special_function_registers_8051_set_arg_8 assumption |
---|
2661 | ] |
---|
2662 | |6,15: |
---|
2663 | whd in match (special_function_registers_8052 ???); |
---|
2664 | whd in match (special_function_registers_8052 ???) in ⊢ (???%); |
---|
2665 | [1: |
---|
2666 | >set_arg_8_set_program_counter |
---|
2667 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2668 | >set_arg_8_set_program_counter |
---|
2669 | [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2670 | >special_function_registers_8052_set_program_counter |
---|
2671 | >special_function_registers_8052_set_program_counter |
---|
2672 | @special_function_registers_8052_set_arg_8 assumption |
---|
2673 | |2: |
---|
2674 | whd in ⊢ (??%%); |
---|
2675 | >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption |
---|
2676 | ] |
---|
2677 | (* XXX: we need special_function_registers_8052_set_arg_8 *) |
---|
2678 | |7,16: |
---|
2679 | whd in match (p1_latch ???); |
---|
2680 | whd in match (p1_latch ???) in ⊢ (???%); |
---|
2681 | (* XXX: we need p1_latch_8052_set_arg_8 *) |
---|
2682 | |8,17: |
---|
2683 | whd in match (p3_latch ???); |
---|
2684 | whd in match (p3_latch ???) in ⊢ (???%); |
---|
2685 | (* XXX: we need p3_latch_8052_set_arg_8 *) |
---|
2686 | |9: |
---|
2687 | >clock_set_clock |
---|
2688 | >clock_set_program_counter in ⊢ (???%); >clock_set_clock |
---|
2689 | >EQticks <instr_refl @eq_f2 |
---|
2690 | [1: |
---|
2691 | whd in ⊢ (??%%); whd in match (ticks_of0 ??????); |
---|
2692 | |2: |
---|
2693 | (* XXX: we need clock_set_arg_8 *) |
---|
2694 | ] |
---|
2695 | |18: |
---|
2696 | ] |
---|
2697 | ] |
---|
2698 | (* XXX: switch to the right hand side *) |
---|
2699 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2700 | cases (¬ eq_bv ???) normalize nodelta |
---|
2701 | whd in ⊢ (??%%); |
---|
2702 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2703 | @split_eq_status try % |
---|
2704 | [1,2,3,19,20,21,28,29,30: |
---|
2705 | cases daemon (* XXX: axioms as above *) |
---|
2706 | |4,13,22,31: |
---|
2707 | |5,14,23,32: |
---|
2708 | |6,15,24,33: |
---|
2709 | |7,16,25,34: |
---|
2710 | |8,17,26,35: |
---|
2711 | whd in ⊢ (??%%);maps_assm |
---|
2712 | |
---|
2713 | |9,18,27,36: |
---|
2714 | whd in ⊢ (??%%); |
---|
2715 | whd in match (ticks_of_instruction ?); <instr_refl |
---|
2716 | cases daemon (* XXX: daemon in ticks_of0 stopping progression *) |
---|
2717 | ] |
---|
2718 | |2,4: |
---|
2719 | >(? : eq_v bool 9 eq_b upper (zero 9) = false) |
---|
2720 | [2, 4: |
---|
2721 | cases daemon (* XXX: !!! *) |
---|
2722 | ] |
---|
2723 | normalize nodelta >EQppc |
---|
2724 | * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl |
---|
2725 | * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' |
---|
2726 | * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' |
---|
2727 | #fetch_many_assm whd in fetch_many_assm; %{2} |
---|
2728 | change with (execute_1 ?? = ?) |
---|
2729 | @(pose … (execute_1 ? (status_of_pseudo_status …))) |
---|
2730 | #status_after_1 #EQstatus_after_1 |
---|
2731 | <(?: ? = status_after_1) |
---|
2732 | [3,6: |
---|
2733 | >EQstatus_after_1 in ⊢ (???%); |
---|
2734 | whd in ⊢ (???%); |
---|
2735 | [1: |
---|
2736 | <fetch_refl in ⊢ (???%); |
---|
2737 | |2: |
---|
2738 | <fetch_refl in ⊢ (???%); |
---|
2739 | ] |
---|
2740 | whd in ⊢ (???%); |
---|
2741 | @(pair_replace ?????????? p) |
---|
2742 | [1,3: |
---|
2743 | cases daemon |
---|
2744 | |2,4: |
---|
2745 | normalize nodelta |
---|
2746 | whd in match (addr_of_relative ????); |
---|
2747 | cases (¬ eq_bv ???) normalize nodelta |
---|
2748 | >set_clock_mk_Status_commutation |
---|
2749 | whd in ⊢ (???%); |
---|
2750 | change with (add ???) in match (\snd (half_add ???)); |
---|
2751 | >set_arg_8_set_program_counter in ⊢ (???%); |
---|
2752 | [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] |
---|
2753 | >program_counter_set_program_counter in ⊢ (???%); |
---|
2754 | >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') |
---|
2755 | [2,4,6,8: |
---|
2756 | >bitvector_of_nat_sign_extension_equivalence |
---|
2757 | [1,3,5,7: |
---|
2758 | >EQintermediate_pc' % |
---|
2759 | |*: |
---|
2760 | repeat @le_S_S @le_O_n |
---|
2761 | ] |
---|
2762 | ] |
---|
2763 | [1,3: % ] |
---|
2764 | ] |
---|
2765 | |1,4: |
---|
2766 | skip |
---|
2767 | ] |
---|
2768 | [3,4: |
---|
2769 | -status_after_1 |
---|
2770 | @(pose … (execute_1 ? (mk_PreStatus …))) |
---|
2771 | #status_after_1 #EQstatus_after_1 |
---|
2772 | <(?: ? = status_after_1) |
---|
2773 | [3,6: |
---|
2774 | >EQstatus_after_1 in ⊢ (???%); |
---|
2775 | whd in ⊢ (???%); |
---|
2776 | (* XXX: matita bug with patterns across multiple goals *) |
---|
2777 | [1: |
---|
2778 | <fetch_refl'' in ⊢ (???%); |
---|
2779 | |2: |
---|
2780 | <fetch_refl'' in ⊢ (???%); |
---|
2781 | ] |
---|
2782 | [2: % |1: whd in ⊢ (???%); % ] |
---|
2783 | |1,4: |
---|
2784 | skip |
---|
2785 | ] |
---|
2786 | -status_after_1 whd in ⊢ (??%?); |
---|
2787 | (* XXX: switch to the right hand side *) |
---|
2788 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2789 | normalize nodelta whd in ⊢ (??%%); |
---|
2790 | ] |
---|
2791 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2792 | @split_eq_status try % |
---|
2793 | whd in ⊢ (??%%); |
---|
2794 | cases daemon |
---|
2795 | ] |
---|
2796 | |30: (* CJNE *) |
---|
2797 | (* XXX: work on the right hand side *) |
---|
2798 | cases addr1 -addr1 #addr1 normalize nodelta |
---|
2799 | cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta |
---|
2800 | (* XXX: switch to the left hand side *) |
---|
2801 | >EQP -P normalize nodelta |
---|
2802 | #sigma_increment_commutation #maps_assm #fetch_many_assm |
---|
2803 | |
---|
2804 | whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; |
---|
2805 | <EQppc in fetch_many_assm; |
---|
2806 | whd in match (short_jump_cond ??); |
---|
2807 | @pair_elim #sj_possible #disp |
---|
2808 | @pair_elim #result #flags #sub16_refl |
---|
2809 | @pair_elim #upper #lower #vsplit_refl |
---|
2810 | inversion (get_index' bool ???) #get_index_refl' normalize nodelta |
---|
2811 | #sj_possible_pair destruct(sj_possible_pair) normalize nodelta |
---|
2812 | [1,3: |
---|
2813 | >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} |
---|
2814 | >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; |
---|
2815 | normalize nodelta in ⊢ (% → ?); #fetch_many_assm |
---|
2816 | whd in ⊢ (??%?); |
---|
2817 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2818 | inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta |
---|
2819 | lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl |
---|
2820 | @(if_then_else_replace ???????? eq_bv_refl) |
---|
2821 | [1,3,5,7: |
---|
2822 | cases daemon |
---|
2823 | |2,4,6,8: |
---|
2824 | (* XXX: switch to the right hand side *) |
---|
2825 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2826 | whd in ⊢ (??%%); |
---|
2827 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2828 | @split_eq_status try % |
---|
2829 | [3,7,11,15: |
---|
2830 | whd in ⊢ (??%?); |
---|
2831 | [1,3: |
---|
2832 | cases daemon |
---|
2833 | |2,4: |
---|
2834 | cases daemon |
---|
2835 | ] |
---|
2836 | ] |
---|
2837 | cases daemon (* XXX *) |
---|
2838 | ] |
---|
2839 | |2,4: |
---|
2840 | >(? : eq_v bool 9 eq_b upper (zero 9) = false) |
---|
2841 | [2, 4: |
---|
2842 | cases daemon (* XXX: !!! *) |
---|
2843 | ] |
---|
2844 | normalize nodelta >EQppc |
---|
2845 | * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl |
---|
2846 | * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' |
---|
2847 | * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' |
---|
2848 | #fetch_many_assm whd in fetch_many_assm; %{2} |
---|
2849 | change with (execute_1 ?? = ?) |
---|
2850 | @(pose … (execute_1 ? (status_of_pseudo_status …))) |
---|
2851 | #status_after_1 #EQstatus_after_1 |
---|
2852 | <(?: ? = status_after_1) |
---|
2853 | [2,5: |
---|
2854 | inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta |
---|
2855 | |3,6: |
---|
2856 | >EQstatus_after_1 in ⊢ (???%); |
---|
2857 | whd in ⊢ (???%); |
---|
2858 | [1: <fetch_refl in ⊢ (???%); |
---|
2859 | |2: <fetch_refl in ⊢ (???%); |
---|
2860 | ] |
---|
2861 | whd in ⊢ (???%); |
---|
2862 | inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta |
---|
2863 | whd in ⊢ (???%); |
---|
2864 | whd in match (addr_of_relative ????); |
---|
2865 | change with (add ???) in match (\snd (half_add ???)); |
---|
2866 | >set_clock_set_program_counter in ⊢ (???%); |
---|
2867 | >program_counter_set_program_counter in ⊢ (???%); |
---|
2868 | >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') |
---|
2869 | [2,4,6,8: |
---|
2870 | >bitvector_of_nat_sign_extension_equivalence |
---|
2871 | [1,3,5,7: |
---|
2872 | >EQintermediate_pc' % |
---|
2873 | |*: |
---|
2874 | repeat @le_S_S @le_O_n |
---|
2875 | ] |
---|
2876 | |1,5: |
---|
2877 | % |
---|
2878 | ] |
---|
2879 | |1,4: skip |
---|
2880 | ] |
---|
2881 | [1,2,3,4: |
---|
2882 | -status_after_1 |
---|
2883 | @(pose … (execute_1 ? (mk_PreStatus …))) |
---|
2884 | #status_after_1 #EQstatus_after_1 |
---|
2885 | <(?: ? = status_after_1) |
---|
2886 | [3,6,9,12: |
---|
2887 | >EQstatus_after_1 in ⊢ (???%); |
---|
2888 | whd in ⊢ (???%); |
---|
2889 | (* XXX: matita bug with patterns across multiple goals *) |
---|
2890 | [1: <fetch_refl'' in ⊢ (???%); |
---|
2891 | |2: <fetch_refl'' in ⊢ (???%); |
---|
2892 | |3: <fetch_refl'' in ⊢ (???%); |
---|
2893 | |4: <fetch_refl'' in ⊢ (???%); |
---|
2894 | ] % |
---|
2895 | |1,4,7,10: |
---|
2896 | skip |
---|
2897 | ] |
---|
2898 | -status_after_1 whd in ⊢ (??%?); |
---|
2899 | (* XXX: switch to the right hand side *) |
---|
2900 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2901 | whd in ⊢ (??%%); |
---|
2902 | ] |
---|
2903 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2904 | @split_eq_status try % |
---|
2905 | cases daemon |
---|
2906 | ] |
---|
2907 | |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *) |
---|
2908 | (* XXX: work on the right hand side *) |
---|
2909 | >p normalize nodelta |
---|
2910 | (* XXX: switch to the left hand side *) |
---|
2911 | >EQP -P normalize nodelta |
---|
2912 | #sigma_increment_commutation #maps_assm #fetch_many_assm |
---|
2913 | |
---|
2914 | whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; |
---|
2915 | <EQppc in fetch_many_assm; |
---|
2916 | whd in match (short_jump_cond ??); |
---|
2917 | @pair_elim #sj_possible #disp |
---|
2918 | @pair_elim #result #flags #sub16_refl |
---|
2919 | @pair_elim #upper #lower #vsplit_refl |
---|
2920 | inversion (get_index' bool ???) #get_index_refl' normalize nodelta |
---|
2921 | #sj_possible_pair destruct(sj_possible_pair) normalize nodelta |
---|
2922 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27: |
---|
2923 | >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} |
---|
2924 | >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; |
---|
2925 | normalize nodelta in ⊢ (% → ?); #fetch_many_assm |
---|
2926 | whd in ⊢ (??%?); |
---|
2927 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
2928 | (* XXX: work on the left hand side *) |
---|
2929 | @(if_then_else_replace ???????? p) normalize nodelta |
---|
2930 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27: |
---|
2931 | cases daemon |
---|
2932 | ] |
---|
2933 | (* XXX: switch to the right hand side *) |
---|
2934 | normalize nodelta >EQs -s >EQticks -ticks |
---|
2935 | whd in ⊢ (??%%); |
---|
2936 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
2937 | @split_eq_status try % |
---|
2938 | cases daemon |
---|
2939 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28: |
---|
2940 | >(? : eq_v bool 9 eq_b upper (zero 9) = false) |
---|
2941 | [2,4,6,8,10,12,14,16,18,20,22,24,26,28: |
---|
2942 | cases daemon (* XXX: !!! *) |
---|
2943 | ] |
---|
2944 | normalize nodelta >EQppc |
---|
2945 | * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl |
---|
2946 | * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' |
---|
2947 | * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl'' |
---|
2948 | #fetch_many_assm whd in fetch_many_assm; %{2} |
---|
2949 | change with (execute_1 ?? = ?) |
---|
2950 | @(pose … (execute_1 ? (status_of_pseudo_status …))) |
---|
2951 | #status_after_1 #EQstatus_after_1 |
---|
2952 | <(?: ? = status_after_1) |
---|
2953 | [3,6,9,12,15,18,21,24,27,30,33,36,39,42: |
---|
2954 | >EQstatus_after_1 in ⊢ (???%); |
---|
2955 | whd in ⊢ (???%); |
---|
2956 | [1: <fetch_refl in ⊢ (???%); |
---|
2957 | |2: <fetch_refl in ⊢ (???%); |
---|
2958 | |3: <fetch_refl in ⊢ (???%); |
---|
2959 | |4: <fetch_refl in ⊢ (???%); |
---|
2960 | |5: <fetch_refl in ⊢ (???%); |
---|
2961 | |6: <fetch_refl in ⊢ (???%); |
---|
2962 | |7: <fetch_refl in ⊢ (???%); |
---|
2963 | |8: <fetch_refl in ⊢ (???%); |
---|
2964 | |9: <fetch_refl in ⊢ (???%); |
---|
2965 | |10: <fetch_refl in ⊢ (???%); |
---|
2966 | |11: <fetch_refl in ⊢ (???%); |
---|
2967 | |12: <fetch_refl in ⊢ (???%); |
---|
2968 | |13: <fetch_refl in ⊢ (???%); |
---|
2969 | |14: <fetch_refl in ⊢ (???%); |
---|
2970 | ] |
---|
2971 | whd in ⊢ (???%); |
---|
2972 | @(if_then_else_replace ???????? p) |
---|
2973 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27: |
---|
2974 | cases daemon |
---|
2975 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28: |
---|
2976 | normalize nodelta |
---|
2977 | whd in match (addr_of_relative ????); |
---|
2978 | >set_clock_mk_Status_commutation |
---|
2979 | [9,10: |
---|
2980 | (* XXX: demodulation not working in this case *) |
---|
2981 | >program_counter_set_arg_1 in ⊢ (???%); |
---|
2982 | >program_counter_set_program_counter in ⊢ (???%); |
---|
2983 | |*: |
---|
2984 | /demod/ |
---|
2985 | ] |
---|
2986 | whd in ⊢ (???%); |
---|
2987 | change with (add ???) in match (\snd (half_add ???)); |
---|
2988 | >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') |
---|
2989 | [2,4,6,8,10,12,14,16,18,20,22,24,26,28: |
---|
2990 | >bitvector_of_nat_sign_extension_equivalence |
---|
2991 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27: |
---|
2992 | >EQintermediate_pc' % |
---|
2993 | |*: |
---|
2994 | repeat @le_S_S @le_O_n |
---|
2995 | ] |
---|
2996 | ] |
---|
2997 | % |
---|
2998 | ] |
---|
2999 | |1,4,7,10,13,16,19,22,25,28,31,34,37,40: |
---|
3000 | skip |
---|
3001 | ] |
---|
3002 | -status_after_1 |
---|
3003 | @(pose … (execute_1 ? (mk_PreStatus …))) |
---|
3004 | #status_after_1 #EQstatus_after_1 |
---|
3005 | <(?: ? = status_after_1) |
---|
3006 | [3,6,9,12,15,18,21,24,27,30,33,36,39,42: |
---|
3007 | >EQstatus_after_1 in ⊢ (???%); |
---|
3008 | whd in ⊢ (???%); |
---|
3009 | (* XXX: matita bug with patterns across multiple goals *) |
---|
3010 | [1: <fetch_refl'' in ⊢ (???%); |
---|
3011 | |2: <fetch_refl' in ⊢ (???%); |
---|
3012 | |3: <fetch_refl'' in ⊢ (???%); |
---|
3013 | |4: <fetch_refl' in ⊢ (???%); |
---|
3014 | |5: <fetch_refl'' in ⊢ (???%); |
---|
3015 | |6: <fetch_refl' in ⊢ (???%); |
---|
3016 | |7: <fetch_refl'' in ⊢ (???%); |
---|
3017 | |8: <fetch_refl' in ⊢ (???%); |
---|
3018 | |9: <fetch_refl'' in ⊢ (???%); |
---|
3019 | |10: <fetch_refl' in ⊢ (???%); |
---|
3020 | |11: <fetch_refl'' in ⊢ (???%); |
---|
3021 | |12: <fetch_refl' in ⊢ (???%); |
---|
3022 | |13: <fetch_refl'' in ⊢ (???%); |
---|
3023 | |14: <fetch_refl' in ⊢ (???%); |
---|
3024 | ] |
---|
3025 | whd in ⊢ (???%); |
---|
3026 | [9,10: |
---|
3027 | |*: |
---|
3028 | /demod/ |
---|
3029 | ] % |
---|
3030 | |1,4,7,10,13,16,19,22,25,28,31,34,37,40: |
---|
3031 | skip |
---|
3032 | ] |
---|
3033 | -status_after_1 whd in ⊢ (??%?); |
---|
3034 | (* XXX: switch to the right hand side *) |
---|
3035 | normalize nodelta >EQs -s >EQticks -ticks |
---|
3036 | whd in ⊢ (??%%); |
---|
3037 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
3038 | @split_eq_status try % |
---|
3039 | [3,11,19,27,36,53,61: |
---|
3040 | >program_counter_set_program_counter >set_clock_mk_Status_commutation |
---|
3041 | [5: >program_counter_set_program_counter ] |
---|
3042 | >EQaddr_of normalize nodelta |
---|
3043 | whd in ⊢ (??%?); >EQlookup_labels normalize nodelta |
---|
3044 | >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); |
---|
3045 | @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉) |
---|
3046 | >create_label_cost_refl normalize nodelta #relevant @relevant |
---|
3047 | whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr)) |
---|
3048 | try assumption whd in match instruction_has_label; normalize nodelta |
---|
3049 | <instr_refl normalize nodelta % |
---|
3050 | |7,15,23,31,45,57,65: |
---|
3051 | >set_clock_mk_Status_commutation >program_counter_set_program_counter |
---|
3052 | whd in ⊢ (??%?); normalize nodelta |
---|
3053 | >EQppc in fetch_many_assm; #fetch_many_assm |
---|
3054 | [5: |
---|
3055 | >program_counter_set_arg_1 >program_counter_set_program_counter |
---|
3056 | ] |
---|
3057 | <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc'' |
---|
3058 | <bitvector_of_nat_sign_extension_equivalence |
---|
3059 | [1,3,5,7,9,11,13: |
---|
3060 | whd in ⊢ (???%); cases (half_add ???) normalize // |
---|
3061 | |2,4,6,8,10,12,14: |
---|
3062 | @assembly1_lt_128 |
---|
3063 | @le_S_S @le_O_n |
---|
3064 | ] |
---|
3065 | |*: |
---|
3066 | cases daemon |
---|
3067 | ] |
---|
3068 | ] |
---|
3069 | |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *) |
---|
3070 | (* XXX: work on the right hand side *) |
---|
3071 | lapply (subaddressing_modein ???) |
---|
3072 | <EQaddr normalize nodelta #irrelevant |
---|
3073 | try (>p normalize nodelta) |
---|
3074 | try (>p1 normalize nodelta) |
---|
3075 | (* XXX: switch to the left hand side *) |
---|
3076 | >EQP -P normalize nodelta |
---|
3077 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
3078 | whd in ⊢ (??%?); |
---|
3079 | whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; |
---|
3080 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
3081 | (* XXX: work on the left hand side *) |
---|
3082 | [1,2,3,4,5: |
---|
3083 | generalize in ⊢ (??(???(?%))?); |
---|
3084 | |6,7,8,9,10,11: |
---|
3085 | generalize in ⊢ (??(???(?%))?); |
---|
3086 | |12: |
---|
3087 | generalize in ⊢ (??(???(?%))?); |
---|
3088 | ] |
---|
3089 | <EQaddr normalize nodelta #irrelevant |
---|
3090 | try @(jmpair_as_replace ?????????? p) |
---|
3091 | [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ] |
---|
3092 | (* XXX: switch to the right hand side *) |
---|
3093 | normalize nodelta >EQs -s >EQticks -ticks |
---|
3094 | whd in ⊢ (??%%); |
---|
3095 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
3096 | try @split_eq_status try % whd in ⊢ (??%%); |
---|
3097 | cases daemon |
---|
3098 | |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) |
---|
3099 | (* XXX: work on the right hand side *) |
---|
3100 | >p normalize nodelta |
---|
3101 | try (>p1 normalize nodelta) |
---|
3102 | (* XXX: switch to the left hand side *) |
---|
3103 | -instr_refl >EQP -P normalize nodelta |
---|
3104 | #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} |
---|
3105 | whd in ⊢ (??%?); |
---|
3106 | <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); |
---|
3107 | (* XXX: work on the left hand side *) |
---|
3108 | @(pair_replace ?????????? p) |
---|
3109 | [1,3,5,7,9,11,13,15,17: |
---|
3110 | >set_clock_set_program_counter >set_clock_mk_Status_commutation |
---|
3111 | >set_program_counter_mk_Status_commutation >clock_set_program_counter |
---|
3112 | cases daemon |
---|
3113 | |14,16,18: |
---|
3114 | normalize nodelta |
---|
3115 | @(pair_replace ?????????? p1) |
---|
3116 | [1,3,5: |
---|
3117 | >set_clock_mk_Status_commutation |
---|
3118 | cases daemon |
---|
3119 | ] |
---|
3120 | ] |
---|
3121 | (* XXX: switch to the right hand side *) |
---|
3122 | normalize nodelta >EQs -s >EQticks -ticks |
---|
3123 | whd in ⊢ (??%%); |
---|
3124 | (* XXX: finally, prove the equality using sigma commutation *) |
---|
3125 | try @split_eq_status try % |
---|
3126 | cases daemon *) |
---|