source: src/ASM/AssemblyProofSplit.ma @ 2247

Last change on this file since 2247 was 2247, checked in by mulligan, 8 years ago

Work on the MOV instruction from today and bug fixes in set_arg_1.

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