source: src/ASM/AssemblyProofSplit.ma @ 2258

Last change on this file since 2258 was 2258, checked in by sacerdot, 7 years ago
  1. lemma generalized
  2. automation replaced with expansion to make everything faster
File size: 136.0 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; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
126    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
127    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
128    map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1.
129  #M' #cm #status #status' #sigma #addr1 #sfr_refl
130  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
131  [1,4: #_ @I ] #w
132  whd in ⊢ (??%? → %);
133  inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
134  [1,3:
135    #absurd destruct(absurd)
136  |2,4:
137    #_
138    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
139    <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption
140  ]
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; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
224    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
225    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
226    b = b' →
227    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
228      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
229  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
230  @(subaddressing_mode_elim … addr1)
231  [1:
232    whd in ⊢ (??%? → ??%?); cases (\snd M')
233    [1:
234      normalize nodelta #_ %
235    |2:
236      * #address normalize nodelta #absurd destruct(absurd)
237    ]
238  |2,4:
239    #w whd in ⊢ (??%? → ??%?);
240    inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
241    [1,3:
242      #absurd destruct(absurd)
243    |2:
244      #_
245      <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
246      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
247      normalize nodelta %
248    |4:
249      #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm)
250      -assoc_list_exists_assm #assoc_list_exists_assm
251      <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
252      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)
253      normalize nodelta %
254    ]
255  |3:
256    #w whd in ⊢ (??%? → ??%?);
257    @eq_bv_elim #eq_bv_refl normalize nodelta
258    [1:
259      #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)
260      #assoc_list_exists_refl #eq_accumulator_refl
261      >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b)
262      whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl)
263      %
264    |2:
265      #assoc_list_exists_assm
266      @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
267      cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl
268      <head_head' inversion bit #bit_refl normalize nodelta
269      >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl;
270      [1:
271        @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption
272      |2:
273        @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map
274        <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)
275      ]
276    ]
277  |5,6,7,8:
278    #w try #w' %
279  ]
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          @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
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          @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
946        |3:
947          >status_refl
948          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
949          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
960        |3:
961          >status_refl
962          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
963          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1986                  |3:
1987                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1988                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2024                  |3:
2025                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
2026                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
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 try %
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      [1:
2124        >EQs >EQticks <instr_refl >addr_refl
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        >EQs >EQticks <instr_refl >addr_refl %
2130      |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *)
2131        @(pose … (set_clock ????)) #status #status_refl
2132        [1:
2133          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
2134        |2:
2135          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
2136        ]
2137        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
2138        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
2139        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
2140      ]
2141    ]
2142  |44: (* MOVX *)
2143    >EQP -P normalize nodelta
2144    inversion addr
2145    [1:
2146      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
2147      #addr_refl
2148      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2149      whd in maps_assm:(??%%);
2150      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2151      [2: normalize nodelta #absurd destruct(absurd) ]
2152      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2153      [2: normalize nodelta #absurd destruct(absurd) ]
2154      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2155      whd in ⊢ (??%?);
2156      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2157      change with (set_arg_8 ????? = ?)
2158      @set_arg_8_status_of_pseudo_status try %
2159      >EQs >EQticks <instr_refl >addr_refl
2160      [1:
2161        @sym_eq @set_clock_status_of_pseudo_status %
2162      |2:
2163        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
2164        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
2165      |3:
2166        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2167        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
2168        @(pose … (set_clock ????)) #status #status_refl
2169        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2170        [1:
2171          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2172          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
2173        |2:
2174          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2175          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
2176        ]
2177      ]
2178    |2:
2179      #others_acc_a cases others_acc_a #others #acc_a
2180      #addr_refl
2181      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2182      whd in maps_assm:(??%%);
2183      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2184      [2: normalize nodelta #absurd destruct(absurd) ]
2185      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2186      [2: normalize nodelta #absurd destruct(absurd) ]
2187      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2188      whd in ⊢ (??%?);
2189      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2190      change with (set_arg_8 ????? = ?)
2191      @set_arg_8_status_of_pseudo_status
2192      >EQs >EQticks <instr_refl >addr_refl try %
2193      [1:
2194        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2195        [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
2196      |2:
2197        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2198        [1:
2199          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
2200        |2,3:
2201          %
2202        |4:
2203          @(pose … (set_clock ????)) #status #status_refl
2204          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2205          [1:
2206            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
2207            [1: @(subaddressing_mode_elim … acc_a) % ] %
2208          |2:
2209            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
2210            [1: @(subaddressing_mode_elim … acc_a) % ] %
2211          ]
2212        ]
2213      ]
2214    ]
2215  |*)45: (* SETB *)
2216    >EQs >EQticks <instr_refl
2217    >EQP -P normalize nodelta
2218    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2219    whd in maps_assm:(??%%);
2220    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2221    [2: normalize nodelta #absurd destruct(absurd) ]
2222    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2223    whd in ⊢ (??%?);
2224    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2225    change with (set_arg_1 ????? = ?)
2226    @set_arg_1_status_of_pseudo_status try %
2227    [1:
2228      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
2229    |2:
2230      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
2231    ]
2232  |46: (* PUSH *)
2233    >EQP -P normalize nodelta
2234    #sigma_increment_commutation whd in ⊢ (??%% → ?);
2235    inversion M #callM #accM #callM_accM_refl normalize nodelta
2236    @(subaddressing_mode_elim … addr) #w normalize nodelta
2237    @Some_Some_elim #Mrefl destruct(Mrefl)
2238    cases daemon (* XXX *)
2239  |47: (* POP *)
2240  |48: (* XCH *)
2241    >EQP -P normalize nodelta
2242    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2243    whd in maps_assm:(??%%);
2244    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2245    [2: normalize nodelta #absurd destruct(absurd) ]
2246    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2247    [2: normalize nodelta #absurd destruct(absurd) ]
2248    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2249    whd in ⊢ (??%?);
2250    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2251    change with (set_arg_8 ????? = ?)
2252    >EQs >EQticks <instr_refl
2253    @set_arg_8_status_of_pseudo_status try %
2254    [1:
2255      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2256      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
2257      @(pose … (set_clock ????)) #status #status_refl
2258      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2259      [1:
2260        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2261        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
2262      |2:
2263        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2264        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
2265      ]
2266    |2:
2267      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2268      [1:
2269        @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
2270      |*:
2271        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2272        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2273        whd in match sfr_8051_index; normalize nodelta
2274        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2275      ]
2276    |3:
2277      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2278      [1:
2279        @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
2280      |2:
2281        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2282        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2283        whd in match sfr_8051_index; normalize nodelta
2284        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2285      |3:
2286        @(pose … (set_clock ????)) #status #status_refl
2287        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2288        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2289      ]
2290    ]
2291  |49: (* XCHD *)
2292    >EQP -P normalize nodelta
2293    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2294    whd in maps_assm:(??%%);
2295    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2296    [2: normalize nodelta #absurd destruct(absurd) ]
2297    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2298    [2: normalize nodelta #absurd destruct(absurd) ]
2299    normalize nodelta @Some_Some_elim #Mrefl 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_f
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 try %
2309      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2310    |2:
2311      @(pair_replace ?????????? p1) normalize nodelta
2312      >EQs >EQticks <instr_refl
2313      [1:
2314        @eq_f
2315        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2316        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2317        [1:
2318          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2319          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
2320        |2:
2321          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2322          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
2323        ]
2324      |2:
2325        @(pair_replace ?????????? p) normalize nodelta
2326        >EQs >EQticks <instr_refl
2327        [1:
2328          %
2329        |2:
2330          @(pair_replace ?????????? p1) normalize nodelta
2331          >EQs >EQticks <instr_refl
2332          [1:
2333            %
2334          |2:
2335            @set_arg_8_status_of_pseudo_status try %
2336            [1:
2337              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2338              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2339            |2:
2340              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2341              [1:
2342                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
2343              |2:
2344                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2345                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2346                whd in match sfr_8051_index; normalize nodelta
2347                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2348              ]
2349            |3:
2350              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2351              [1:
2352                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
2353              |2:
2354                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2355                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2356                whd in match sfr_8051_index; normalize nodelta
2357                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2358              ]
2359            ]
2360          ]
2361        ]
2362      ]
2363    ]
2364  |50: (* RET *)
2365    >EQP -P normalize nodelta
2366    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2367    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2368    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2369    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2370    [2: normalize nodelta #absurd destruct(absurd) ]
2371    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2372    [2: normalize nodelta #absurd destruct(absurd) ]
2373    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2374    whd in ⊢ (??%?);
2375    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2376    whd in ⊢ (??%?);
2377    @(pair_replace ?????????? p) normalize nodelta
2378    >EQs >EQticks <instr_refl
2379    [1:
2380      @eq_f3 try %
2381      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2382      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2383    |2:
2384      @(pair_replace ?????????? p1) normalize nodelta
2385      >EQs >EQticks <instr_refl
2386      [1:
2387        @eq_f3 try %
2388        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2389        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2390        [1:
2391          cases daemon
2392          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2393        |2:
2394          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2395          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2396          whd in match sfr_8051_index; normalize nodelta
2397          >get_index_v_set_index_hit
2398          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2399          cases daemon
2400          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2401        ]
2402      |2:
2403        cases daemon (* XXX *)
2404      ]
2405    ]
2406  |51: (* RETI *)
2407  |52: (* NOP *)
2408    >EQP -P normalize nodelta
2409    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2410    whd in maps_assm:(??%%);
2411    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2412    whd in ⊢ (??%?);
2413    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2414    change with (set_clock ???? = ?)
2415    @set_clock_status_of_pseudo_status %
2416  ]
2417cases daemon
2418qed.
2419
2420(*
2421  (* XXX: work on the left hand side *)
2422  (* XXX: switch to the right hand side *)
2423  normalize nodelta >EQs -s >EQticks -ticks
2424  whd in ⊢ (??%%);
2425  (* XXX: finally, prove the equality using sigma commutation *)
2426  cases daemon
2427  |11,12: (* DIV *)
2428  (* XXX: work on the right hand side *)
2429  normalize nodelta in p;
2430  >p normalize nodelta
2431  (* XXX: switch to the left hand side *)
2432  -instr_refl >EQP -P normalize nodelta
2433  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2434  whd in ⊢ (??%?);
2435  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2436  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
2437  >(?: pose_assm = 0) normalize nodelta
2438  [2,4:
2439    <p >pose_refl
2440    cases daemon
2441  |1,3:
2442    (* XXX: switch to the right hand side *)
2443    >EQs -s >EQticks -ticks
2444    whd in ⊢ (??%%);
2445    (* XXX: finally, prove the equality using sigma commutation *)
2446    @split_eq_status try %
2447    cases daemon
2448  ]
2449  |13,14,15: (* DA *)
2450  (* XXX: work on the right hand side *)
2451  >p normalize nodelta
2452  >p1 normalize nodelta
2453  try (>p2 normalize nodelta
2454  try (>p3 normalize nodelta
2455  try (>p4 normalize nodelta
2456  try (>p5 normalize nodelta))))
2457  (* XXX: switch to the left hand side *)
2458  -instr_refl >EQP -P normalize nodelta
2459  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2460  whd in ⊢ (??%?);
2461  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2462  (* XXX: work on the left hand side *)
2463  @(pair_replace ?????????? p)
2464  [1,3,5:
2465    /demod/
2466    cases daemon
2467  |2,4,6:
2468    @(if_then_else_replace ???????? p1)
2469    [1,3,5:
2470      cases daemon
2471    |2,4:
2472      normalize nodelta
2473      @(pair_replace ?????????? p2)
2474      [1,3:
2475        cases daemon
2476      |2,4:
2477        normalize nodelta >p3 normalize nodelta
2478        >p4 normalize nodelta try >p5
2479      ]
2480    ]
2481  (* XXX: switch to the right hand side *)
2482  normalize nodelta >EQs -s >EQticks -ticks
2483  whd in ⊢ (??%%);
2484  (* XXX: finally, prove the equality using sigma commutation *)
2485  @split_eq_status try %
2486  cases daemon
2487  ]
2488  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
2489  (* XXX: work on the right hand side *)
2490  cases addr #addr' normalize nodelta
2491  [1,3:
2492    cases addr' #addr'' normalize nodelta
2493  ]
2494  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
2495  (* XXX: switch to the left hand side *)
2496  -instr_refl >EQP -P normalize nodelta
2497  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2498  whd in ⊢ (??%?);
2499  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2500  (* XXX: work on the left hand side *)
2501  (* XXX: switch to the right hand side *)
2502  normalize nodelta >EQs -s >EQticks -ticks
2503  whd in ⊢ (??%%);
2504  (* XXX: finally, prove the equality using sigma commutation *)
2505  cases daemon
2506  |47: (* MOV *)
2507  (* XXX: work on the right hand side *)
2508  cases addr -addr #addr normalize nodelta
2509  [1:
2510    cases addr #addr normalize nodelta
2511    [1:
2512      cases addr #addr normalize nodelta
2513      [1:
2514        cases addr #addr normalize nodelta
2515        [1:
2516          cases addr #addr normalize nodelta
2517        ]
2518      ]
2519    ]
2520  ]
2521  cases addr #lft #rgt normalize nodelta
2522  (* XXX: switch to the left hand side *)
2523  >EQP -P normalize nodelta
2524  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2525  whd in ⊢ (??%?);
2526  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2527  (* XXX: work on the left hand side *)
2528  (* XXX: switch to the right hand side *)
2529  normalize nodelta >EQs -s >EQticks -ticks
2530  whd in ⊢ (??%%);
2531  (* XXX: finally, prove the equality using sigma commutation *)
2532  cases daemon
2533  ]
2534*)
2535
2536
2537(*  [31,32: (* DJNZ *)
2538  (* XXX: work on the right hand side *)
2539  >p normalize nodelta >p1 normalize nodelta
2540  (* XXX: switch to the left hand side *)
2541  >EQP -P normalize nodelta
2542  #sigma_increment_commutation #maps_assm #fetch_many_assm
2543  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2544  <EQppc in fetch_many_assm;
2545  whd in match (short_jump_cond ??);
2546  @pair_elim #sj_possible #disp
2547  @pair_elim #result #flags #sub16_refl
2548  @pair_elim #upper #lower #vsplit_refl
2549  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2550  #sj_possible_pair destruct(sj_possible_pair)
2551  >p1 normalize nodelta
2552  [1,3:
2553    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2554    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2555    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2556    whd in ⊢ (??%?);
2557    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2558    lapply maps_assm whd in ⊢ (??%? → ?);
2559    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
2560    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
2561    (* XXX: work on the left hand side *)
2562    @(pair_replace ?????????? p) normalize nodelta
2563    [1,3:
2564      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
2565      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2566      >(get_arg_8_set_program_counter … true addr1)
2567      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2568      @get_arg_8_pseudo_addressing_mode_ok assumption
2569    |2,4:
2570      >p1 normalize nodelta >EQs
2571      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
2572      >set_program_counter_status_of_pseudo_status
2573       whd in ⊢ (??%%);
2574      @split_eq_status
2575      [1,10:
2576        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2577        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2578        >low_internal_ram_set_program_counter
2579        [1:
2580          >low_internal_ram_set_program_counter
2581          (* XXX: ??? *)
2582        |2:
2583          >low_internal_ram_set_clock
2584          (* XXX: ??? *)
2585        ]
2586      |2,11:
2587        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2588        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2589        >high_internal_ram_set_program_counter
2590        [1:
2591          >high_internal_ram_set_program_counter
2592          (* XXX: ??? *)
2593        |2:
2594          >high_internal_ram_set_clock
2595          (* XXX: ??? *)
2596        ]
2597      |3,12:
2598        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
2599        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2600        >(external_ram_set_arg_8 ??? addr1)
2601        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2602      |4,13:
2603        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
2604        [1:
2605          >program_counter_set_program_counter
2606          >set_arg_8_set_program_counter
2607          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2608          >set_clock_set_program_counter >program_counter_set_program_counter
2609          change with (add ??? = ?)
2610          (* XXX: ??? *)
2611        |2:
2612          >set_arg_8_set_program_counter
2613          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2614          >program_counter_set_program_counter
2615          >set_arg_8_set_program_counter
2616          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2617          >set_clock_set_program_counter >program_counter_set_program_counter
2618          >sigma_increment_commutation <EQppc
2619          whd in match (assembly_1_pseudoinstruction ??????);
2620          whd in match (expand_pseudo_instruction ??????);
2621          (* XXX: ??? *)
2622        ]
2623      |5,14:
2624        whd in match (special_function_registers_8051 ???);
2625        [1:
2626          >special_function_registers_8051_set_program_counter
2627          >special_function_registers_8051_set_clock
2628          >set_arg_8_set_program_counter in ⊢ (???%);
2629          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2630          >special_function_registers_8051_set_program_counter
2631          >set_arg_8_set_program_counter
2632          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2633          >special_function_registers_8051_set_program_counter
2634          @special_function_registers_8051_set_arg_8 assumption
2635        |2:
2636          >special_function_registers_8051_set_clock
2637          >set_arg_8_set_program_counter
2638          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2639          >set_arg_8_set_program_counter
2640          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2641          >special_function_registers_8051_set_program_counter
2642          >special_function_registers_8051_set_program_counter
2643          @special_function_registers_8051_set_arg_8 assumption
2644        ]
2645      |6,15:
2646        whd in match (special_function_registers_8052 ???);
2647        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
2648        [1:
2649          >set_arg_8_set_program_counter
2650          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2651          >set_arg_8_set_program_counter
2652          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2653          >special_function_registers_8052_set_program_counter
2654          >special_function_registers_8052_set_program_counter
2655          @special_function_registers_8052_set_arg_8 assumption
2656        |2:
2657          whd in ⊢ (??%%);
2658          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
2659        ]
2660        (* XXX: we need special_function_registers_8052_set_arg_8 *)
2661      |7,16:
2662        whd in match (p1_latch ???);
2663        whd in match (p1_latch ???) in ⊢ (???%);
2664        (* XXX: we need p1_latch_8052_set_arg_8 *)
2665      |8,17:
2666        whd in match (p3_latch ???);
2667        whd in match (p3_latch ???) in ⊢ (???%);
2668        (* XXX: we need p3_latch_8052_set_arg_8 *)
2669      |9:
2670        >clock_set_clock
2671        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
2672        >EQticks <instr_refl @eq_f2
2673        [1:
2674          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
2675        |2:
2676          (* XXX: we need clock_set_arg_8 *)
2677        ]
2678      |18:
2679      ]
2680    ]
2681    (* XXX: switch to the right hand side *)
2682    normalize nodelta >EQs -s >EQticks -ticks
2683    cases (¬ eq_bv ???) normalize nodelta
2684    whd in ⊢ (??%%);
2685    (* XXX: finally, prove the equality using sigma commutation *)
2686    @split_eq_status try %
2687    [1,2,3,19,20,21,28,29,30:
2688      cases daemon (* XXX: axioms as above *)
2689    |4,13,22,31:
2690    |5,14,23,32:
2691    |6,15,24,33:
2692    |7,16,25,34:
2693    |8,17,26,35:
2694      whd in ⊢ (??%%);maps_assm
2695     
2696    |9,18,27,36:
2697      whd in ⊢ (??%%);
2698      whd in match (ticks_of_instruction ?); <instr_refl
2699      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
2700    ]
2701  |2,4:
2702    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2703    [2, 4:
2704      cases daemon (* XXX: !!! *)
2705    ]
2706    normalize nodelta >EQppc
2707    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2708    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2709    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2710    #fetch_many_assm whd in fetch_many_assm; %{2}
2711    change with (execute_1 ?? = ?)
2712    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2713    #status_after_1 #EQstatus_after_1
2714    <(?: ? = status_after_1)
2715    [3,6:
2716      >EQstatus_after_1 in ⊢ (???%);
2717      whd in ⊢ (???%);
2718      [1:
2719        <fetch_refl in ⊢ (???%);
2720      |2:
2721        <fetch_refl in ⊢ (???%);
2722      ]
2723      whd in ⊢ (???%);
2724      @(pair_replace ?????????? p)
2725      [1,3:
2726        cases daemon
2727      |2,4:
2728        normalize nodelta
2729        whd in match (addr_of_relative ????);
2730        cases (¬ eq_bv ???) normalize nodelta
2731        >set_clock_mk_Status_commutation
2732        whd in ⊢ (???%);
2733        change with (add ???) in match (\snd (half_add ???));
2734        >set_arg_8_set_program_counter in ⊢ (???%);
2735        [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2736        >program_counter_set_program_counter in ⊢ (???%);
2737        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2738        [2,4,6,8:
2739          >bitvector_of_nat_sign_extension_equivalence
2740          [1,3,5,7:
2741            >EQintermediate_pc' %
2742          |*:
2743            repeat @le_S_S @le_O_n
2744          ]
2745        ]
2746        [1,3: % ]
2747      ]
2748    |1,4:
2749      skip
2750    ]
2751    [3,4:
2752      -status_after_1
2753      @(pose … (execute_1 ? (mk_PreStatus …)))
2754      #status_after_1 #EQstatus_after_1
2755      <(?: ? = status_after_1)
2756      [3,6:
2757        >EQstatus_after_1 in ⊢ (???%);
2758        whd in ⊢ (???%);
2759        (* XXX: matita bug with patterns across multiple goals *)
2760        [1:
2761          <fetch_refl'' in ⊢ (???%);
2762        |2:
2763          <fetch_refl'' in ⊢ (???%);
2764        ]
2765        [2: % |1: whd in ⊢ (???%); % ]
2766      |1,4:
2767        skip
2768      ]
2769      -status_after_1 whd in ⊢ (??%?);
2770      (* XXX: switch to the right hand side *)
2771      normalize nodelta >EQs -s >EQticks -ticks
2772      normalize nodelta whd in ⊢ (??%%);
2773    ]
2774    (* XXX: finally, prove the equality using sigma commutation *)
2775    @split_eq_status try %
2776    whd in ⊢ (??%%);
2777    cases daemon
2778  ]
2779  |30: (* CJNE *)
2780  (* XXX: work on the right hand side *)
2781  cases addr1 -addr1 #addr1 normalize nodelta
2782  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
2783  (* XXX: switch to the left hand side *)
2784  >EQP -P normalize nodelta
2785  #sigma_increment_commutation #maps_assm #fetch_many_assm
2786
2787  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2788  <EQppc in fetch_many_assm;
2789  whd in match (short_jump_cond ??);
2790  @pair_elim #sj_possible #disp
2791  @pair_elim #result #flags #sub16_refl
2792  @pair_elim #upper #lower #vsplit_refl
2793  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2794  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2795  [1,3:
2796    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2797    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2798    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2799    whd in ⊢ (??%?);
2800    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2801    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2802    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
2803    @(if_then_else_replace ???????? eq_bv_refl)
2804    [1,3,5,7:
2805      cases daemon
2806    |2,4,6,8:
2807      (* XXX: switch to the right hand side *)
2808      normalize nodelta >EQs -s >EQticks -ticks
2809      whd in ⊢ (??%%);
2810      (* XXX: finally, prove the equality using sigma commutation *)
2811      @split_eq_status try %
2812      [3,7,11,15:
2813        whd in ⊢ (??%?);
2814        [1,3:
2815          cases daemon
2816        |2,4:
2817          cases daemon
2818        ]
2819      ]
2820      cases daemon (* XXX *)
2821    ]
2822  |2,4:
2823    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2824    [2, 4:
2825      cases daemon (* XXX: !!! *)
2826    ]
2827    normalize nodelta >EQppc
2828    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2829    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2830    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2831    #fetch_many_assm whd in fetch_many_assm; %{2}
2832    change with (execute_1 ?? = ?)
2833    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2834    #status_after_1 #EQstatus_after_1
2835    <(?: ? = status_after_1)
2836    [2,5:
2837      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
2838    |3,6:
2839      >EQstatus_after_1 in ⊢ (???%);
2840      whd in ⊢ (???%);
2841      [1: <fetch_refl in ⊢ (???%);
2842      |2: <fetch_refl in ⊢ (???%);
2843      ]
2844      whd in ⊢ (???%);
2845      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2846      whd in ⊢ (???%);
2847      whd in match (addr_of_relative ????);
2848      change with (add ???) in match (\snd (half_add ???));
2849      >set_clock_set_program_counter in ⊢ (???%);
2850      >program_counter_set_program_counter in ⊢ (???%);
2851      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2852      [2,4,6,8:
2853        >bitvector_of_nat_sign_extension_equivalence
2854        [1,3,5,7:
2855          >EQintermediate_pc' %
2856        |*:
2857          repeat @le_S_S @le_O_n
2858        ]
2859      |1,5:
2860        %
2861      ]
2862    |1,4: skip
2863    ]
2864    [1,2,3,4:
2865      -status_after_1
2866      @(pose … (execute_1 ? (mk_PreStatus …)))
2867      #status_after_1 #EQstatus_after_1
2868      <(?: ? = status_after_1)
2869      [3,6,9,12:
2870        >EQstatus_after_1 in ⊢ (???%);
2871        whd in ⊢ (???%);
2872        (* XXX: matita bug with patterns across multiple goals *)
2873        [1: <fetch_refl'' in ⊢ (???%);
2874        |2: <fetch_refl'' in ⊢ (???%);
2875        |3: <fetch_refl'' in ⊢ (???%);
2876        |4: <fetch_refl'' in ⊢ (???%);
2877        ] %
2878      |1,4,7,10:
2879        skip
2880      ]
2881      -status_after_1 whd in ⊢ (??%?);
2882      (* XXX: switch to the right hand side *)
2883      normalize nodelta >EQs -s >EQticks -ticks
2884      whd in ⊢ (??%%);
2885    ]
2886    (* XXX: finally, prove the equality using sigma commutation *)
2887    @split_eq_status try %
2888    cases daemon
2889  ]
2890  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
2891  (* XXX: work on the right hand side *)
2892  >p normalize nodelta
2893  (* XXX: switch to the left hand side *)
2894  >EQP -P normalize nodelta
2895  #sigma_increment_commutation #maps_assm #fetch_many_assm
2896 
2897  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2898  <EQppc in fetch_many_assm;
2899  whd in match (short_jump_cond ??);
2900  @pair_elim #sj_possible #disp
2901  @pair_elim #result #flags #sub16_refl
2902  @pair_elim #upper #lower #vsplit_refl
2903  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2904  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2905  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2906    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2907    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2908    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2909    whd in ⊢ (??%?);
2910    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2911    (* XXX: work on the left hand side *)
2912    @(if_then_else_replace ???????? p) normalize nodelta
2913    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2914      cases daemon
2915    ]
2916    (* XXX: switch to the right hand side *)
2917    normalize nodelta >EQs -s >EQticks -ticks
2918    whd in ⊢ (??%%);
2919    (* XXX: finally, prove the equality using sigma commutation *)
2920    @split_eq_status try %
2921    cases daemon
2922  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2923    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2924    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2925      cases daemon (* XXX: !!! *)
2926    ]
2927    normalize nodelta >EQppc
2928    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2929    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2930    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2931    #fetch_many_assm whd in fetch_many_assm; %{2}
2932    change with (execute_1 ?? = ?)
2933    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2934    #status_after_1 #EQstatus_after_1
2935    <(?: ? = status_after_1)
2936    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2937      >EQstatus_after_1 in ⊢ (???%);
2938      whd in ⊢ (???%);
2939      [1: <fetch_refl in ⊢ (???%);
2940      |2: <fetch_refl in ⊢ (???%);
2941      |3: <fetch_refl in ⊢ (???%);
2942      |4: <fetch_refl in ⊢ (???%);
2943      |5: <fetch_refl in ⊢ (???%);
2944      |6: <fetch_refl in ⊢ (???%);
2945      |7: <fetch_refl in ⊢ (???%);
2946      |8: <fetch_refl in ⊢ (???%);
2947      |9: <fetch_refl in ⊢ (???%);
2948      |10: <fetch_refl in ⊢ (???%);
2949      |11: <fetch_refl in ⊢ (???%);
2950      |12: <fetch_refl in ⊢ (???%);
2951      |13: <fetch_refl in ⊢ (???%);
2952      |14: <fetch_refl in ⊢ (???%);
2953      ]
2954      whd in ⊢ (???%);
2955      @(if_then_else_replace ???????? p)
2956      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2957        cases daemon
2958      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2959        normalize nodelta
2960        whd in match (addr_of_relative ????);
2961        >set_clock_mk_Status_commutation
2962        [9,10:
2963          (* XXX: demodulation not working in this case *)
2964          >program_counter_set_arg_1 in ⊢ (???%);
2965          >program_counter_set_program_counter in ⊢ (???%);
2966        |*:
2967          /demod/
2968        ]
2969        whd in ⊢ (???%);
2970        change with (add ???) in match (\snd (half_add ???));
2971        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2972        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2973          >bitvector_of_nat_sign_extension_equivalence
2974          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2975            >EQintermediate_pc' %
2976          |*:
2977            repeat @le_S_S @le_O_n
2978          ]
2979        ]
2980        %
2981      ]
2982    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
2983      skip
2984    ]
2985    -status_after_1
2986    @(pose … (execute_1 ? (mk_PreStatus …)))
2987    #status_after_1 #EQstatus_after_1
2988    <(?: ? = status_after_1)
2989    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2990      >EQstatus_after_1 in ⊢ (???%);
2991      whd in ⊢ (???%);
2992      (* XXX: matita bug with patterns across multiple goals *)
2993      [1: <fetch_refl'' in ⊢ (???%);
2994      |2: <fetch_refl' in ⊢ (???%);
2995      |3: <fetch_refl'' in ⊢ (???%);
2996      |4: <fetch_refl' in ⊢ (???%);
2997      |5: <fetch_refl'' in ⊢ (???%);
2998      |6: <fetch_refl' in ⊢ (???%);
2999      |7: <fetch_refl'' in ⊢ (???%);
3000      |8: <fetch_refl' in ⊢ (???%);
3001      |9: <fetch_refl'' in ⊢ (???%);
3002      |10: <fetch_refl' in ⊢ (???%);
3003      |11: <fetch_refl'' in ⊢ (???%);
3004      |12: <fetch_refl' in ⊢ (???%);
3005      |13: <fetch_refl'' in ⊢ (???%);
3006      |14: <fetch_refl' in ⊢ (???%);
3007      ]
3008      whd in ⊢ (???%);
3009      [9,10:
3010      |*:
3011        /demod/
3012      ] %
3013    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
3014      skip
3015    ]
3016    -status_after_1 whd in ⊢ (??%?);
3017    (* XXX: switch to the right hand side *)
3018    normalize nodelta >EQs -s >EQticks -ticks
3019    whd in ⊢ (??%%);
3020    (* XXX: finally, prove the equality using sigma commutation *)
3021    @split_eq_status try %
3022    [3,11,19,27,36,53,61:
3023      >program_counter_set_program_counter >set_clock_mk_Status_commutation
3024      [5: >program_counter_set_program_counter ]
3025      >EQaddr_of normalize nodelta
3026      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
3027      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
3028      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
3029      >create_label_cost_refl normalize nodelta #relevant @relevant
3030      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
3031      try assumption whd in match instruction_has_label; normalize nodelta
3032      <instr_refl normalize nodelta %
3033    |7,15,23,31,45,57,65:
3034      >set_clock_mk_Status_commutation >program_counter_set_program_counter
3035      whd in ⊢ (??%?); normalize nodelta
3036      >EQppc in fetch_many_assm; #fetch_many_assm
3037      [5:
3038        >program_counter_set_arg_1 >program_counter_set_program_counter
3039      ]
3040      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
3041      <bitvector_of_nat_sign_extension_equivalence
3042      [1,3,5,7,9,11,13:
3043        whd in ⊢ (???%); cases (half_add ???) normalize //
3044      |2,4,6,8,10,12,14:
3045        @assembly1_lt_128
3046        @le_S_S @le_O_n
3047      ]
3048    |*:
3049      cases daemon
3050    ]
3051  ]
3052  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
3053  (* XXX: work on the right hand side *)
3054  lapply (subaddressing_modein ???)
3055  <EQaddr normalize nodelta #irrelevant
3056  try (>p normalize nodelta)
3057  try (>p1 normalize nodelta)
3058  (* XXX: switch to the left hand side *)
3059  >EQP -P normalize nodelta
3060  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3061  whd in ⊢ (??%?);
3062  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
3063  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3064  (* XXX: work on the left hand side *)
3065  [1,2,3,4,5:
3066    generalize in ⊢ (??(???(?%))?);
3067  |6,7,8,9,10,11:
3068    generalize in ⊢ (??(???(?%))?);
3069  |12:
3070    generalize in ⊢ (??(???(?%))?);
3071  ]
3072  <EQaddr normalize nodelta #irrelevant
3073  try @(jmpair_as_replace ?????????? p)
3074  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
3075  (* XXX: switch to the right hand side *)
3076  normalize nodelta >EQs -s >EQticks -ticks
3077  whd in ⊢ (??%%);
3078  (* XXX: finally, prove the equality using sigma commutation *)
3079  try @split_eq_status try % whd in ⊢ (??%%);
3080  cases daemon
3081  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
3082  (* XXX: work on the right hand side *)
3083  >p normalize nodelta
3084  try (>p1 normalize nodelta)
3085  (* XXX: switch to the left hand side *)
3086  -instr_refl >EQP -P normalize nodelta
3087  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3088  whd in ⊢ (??%?);
3089  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3090  (* XXX: work on the left hand side *)
3091  @(pair_replace ?????????? p)
3092  [1,3,5,7,9,11,13,15,17:
3093    >set_clock_set_program_counter >set_clock_mk_Status_commutation
3094    >set_program_counter_mk_Status_commutation >clock_set_program_counter
3095    cases daemon
3096  |14,16,18:
3097    normalize nodelta
3098    @(pair_replace ?????????? p1)
3099    [1,3,5:
3100      >set_clock_mk_Status_commutation
3101      cases daemon
3102    ]
3103  ]
3104  (* XXX: switch to the right hand side *)
3105  normalize nodelta >EQs -s >EQticks -ticks
3106  whd in ⊢ (??%%);
3107  (* XXX: finally, prove the equality using sigma commutation *)
3108  try @split_eq_status try %
3109  cases daemon *)
Note: See TracBrowser for help on using the repository browser.