source: src/ASM/AssemblyProofSplit.ma @ 2272

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

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File size: 113.7 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
392axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
393  ∀M, M', sigma,cm,s,addr,v,v'.
394    (∀addr'.
395      ((false:::addr) = addr' →
396        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
397        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
398      ((false:::addr) ≠ addr' →
399        let 〈callM, accM〉 ≝ M in
400        let 〈callM', accM'〉 ≝ M' in
401          accM = accM' ∧
402            assoc_list_lookup … addr' (eq_bv 8) … callM =
403              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
404    insert Byte 7 addr v'
405      (low_internal_ram_of_pseudo_low_internal_ram M'
406      (low_internal_ram pseudo_assembly_program cm s)) =
407    low_internal_ram_of_pseudo_low_internal_ram M
408      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
409
410lemma write_at_stack_pointer_status_of_pseudo_status:
411  ∀M, M'.
412  ∀cm.
413  ∀sigma.
414  ∀policy.
415  ∀s, s'.
416  ∀new_b, new_b'.
417    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
418    status_of_pseudo_status M cm s sigma policy = s' →
419    write_at_stack_pointer ?? s' new_b' =
420    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
421  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
422  #new_b_refl #s_refl <new_b_refl <s_refl
423  whd in match write_at_stack_pointer; normalize nodelta
424  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
425  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
426  [1:
427    @eq_f
428    whd in match get_8051_sfr; normalize nodelta
429    whd in match sfr_8051_index; normalize nodelta
430    whd in match status_of_pseudo_status; normalize nodelta
431    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
432    cases (\snd M) [2: * #address ] normalize nodelta
433    [1,2:
434      cases (vsplit bool ???) #high #low normalize nodelta
435      whd in match sfr_8051_index; normalize nodelta
436      >get_index_v_set_index_miss %
437      #absurd destruct(absurd)
438    |3:
439      %
440    ]
441  |2:
442    @if_then_else_status_of_pseudo_status try %
443    [2:
444      @sym_eq <set_low_internal_ram_status_of_pseudo_status
445      [1:
446        @eq_f2
447        [2:
448          @insert_low_internal_ram_of_pseudo_low_internal_ram'
449    @sym_eq
450    [2:
451      <set_low_internal_ram_status_of_pseudo_status
452      [1:
453        @eq_f2
454        [2:
455          @sym_eq
456          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
457          [2:
458            >new_b_refl
459    ]
460  ]
461qed.
462
463lemma main_lemma_preinstruction:
464  ∀M, M': internal_pseudo_address_map.
465  ∀preamble: preamble.
466  ∀instr_list: list labelled_instruction.
467  ∀cm: pseudo_assembly_program.
468  ∀EQcm: cm = 〈preamble, instr_list〉.
469  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
470  ∀sigma: Word → Word.
471  ∀policy: Word → bool.
472  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
473  ∀ps: PseudoStatus cm.
474  ∀ppc: Word.
475  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
476  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
477  ∀labels: label_map.
478  ∀costs: BitVectorTrie costlabel 16.
479  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
480  ∀newppc: Word.
481  ∀lookup_labels: Identifier → Word.
482  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
483  ∀lookup_datalabels: Identifier → Word.
484  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
485  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
486  ∀instr: preinstruction Identifier.
487  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
488  ∀ticks: nat × nat.
489  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
490  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
491  ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
492  ∀s: PreStatus pseudo_assembly_program cm.
493  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
494  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
495  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
496              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
497                  lookup_datalabels (Instruction instr)))) →
498              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
499                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))
500                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
501                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
502                      status_of_pseudo_status M' cm s sigma policy).
503    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
504  (* XXX: takes about 45 minutes to type check! *)
505  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
506  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
507  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
508  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
509  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
510  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
511  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
512  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
513  [2: * // ]
514  @(
515  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
516  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
517  match instr in preinstruction return λx. x = instr → Σs'.? with
518        [ ADD addr1 addr2 ⇒ λinstr_refl.
519            let s ≝ add_ticks1 s in
520            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
521                                                   (get_arg_8 … s false addr2) false in
522            let cy_flag ≝ get_index' ? O ? flags in
523            let ac_flag ≝ get_index' ? 1 ? flags in
524            let ov_flag ≝ get_index' ? 2 ? flags in
525            let s ≝ set_arg_8 … s ACC_A result in
526              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
527        | ADDC addr1 addr2 ⇒ λinstr_refl.
528            let s ≝ add_ticks1 s in
529            let old_cy_flag ≝ get_cy_flag ?? s in
530            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
531                                                   (get_arg_8 … s false addr2) old_cy_flag in
532            let cy_flag ≝ get_index' ? O ? flags in
533            let ac_flag ≝ get_index' ? 1 ? flags in
534            let ov_flag ≝ get_index' ? 2 ? flags in
535            let s ≝ set_arg_8 … s ACC_A result in
536              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
537        | SUBB addr1 addr2 ⇒ λinstr_refl.
538            let s ≝ add_ticks1 s in
539            let old_cy_flag ≝ get_cy_flag ?? s in
540            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
541                                                   (get_arg_8 … s false addr2) old_cy_flag in
542            let cy_flag ≝ get_index' ? O ? flags in
543            let ac_flag ≝ get_index' ? 1 ? flags in
544            let ov_flag ≝ get_index' ? 2 ? flags in
545            let s ≝ set_arg_8 … s ACC_A result in
546              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
547        | ANL addr ⇒ λinstr_refl.
548          let s ≝ add_ticks1 s in
549          match addr with
550            [ inl l ⇒
551              match l with
552                [ inl l' ⇒
553                  let 〈addr1, addr2〉 ≝ l' in
554                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
555                    set_arg_8 … s addr1 and_val
556                | inr r ⇒
557                  let 〈addr1, addr2〉 ≝ r in
558                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
559                    set_arg_8 … s addr1 and_val
560                ]
561            | inr r ⇒
562              let 〈addr1, addr2〉 ≝ r in
563              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
564               set_flags … s and_val (None ?) (get_ov_flag ?? s)
565            ]
566        | ORL addr ⇒ λinstr_refl.
567          let s ≝ add_ticks1 s in
568          match addr with
569            [ inl l ⇒
570              match l with
571                [ inl l' ⇒
572                  let 〈addr1, addr2〉 ≝ l' in
573                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
574                    set_arg_8 … s addr1 or_val
575                | inr r ⇒
576                  let 〈addr1, addr2〉 ≝ r in
577                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
578                    set_arg_8 … s addr1 or_val
579                ]
580            | inr r ⇒
581              let 〈addr1, addr2〉 ≝ r in
582              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
583               set_flags … s or_val (None ?) (get_ov_flag … s)
584            ]
585        | XRL addr ⇒ λinstr_refl.
586          let s ≝ add_ticks1 s in
587          match addr with
588            [ inl l' ⇒
589              let 〈addr1, addr2〉 ≝ l' in
590              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
591                set_arg_8 … s addr1 xor_val
592            | inr r ⇒
593              let 〈addr1, addr2〉 ≝ r in
594              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
595                set_arg_8 … s addr1 xor_val
596            ]
597        | INC addr ⇒ λinstr_refl.
598            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
599              [ ACC_A ⇒ λacc_a: True. λEQaddr.
600                let s' ≝ add_ticks1 s in
601                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
602                 set_arg_8 … s' ACC_A result
603              | REGISTER r ⇒ λregister: True. λEQaddr.
604                let s' ≝ add_ticks1 s in
605                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
606                 set_arg_8 … s' (REGISTER r) result
607              | DIRECT d ⇒ λdirect: True. λEQaddr.
608                let s' ≝ add_ticks1 s in
609                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
610                 set_arg_8 … s' (DIRECT d) result
611              | INDIRECT i ⇒ λindirect: True. λEQaddr.
612                let s' ≝ add_ticks1 s in
613                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
614                 set_arg_8 … s' (INDIRECT i) result
615              | DPTR ⇒ λdptr: True. λEQaddr.
616                let s' ≝ add_ticks1 s in
617                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
618                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
619                let s ≝ set_8051_sfr … s' SFR_DPL bl in
620                 set_8051_sfr … s' SFR_DPH bu
621              | _ ⇒ λother: False. ⊥
622              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
623        | NOP ⇒ λinstr_refl.
624           let s ≝ add_ticks2 s in
625            s
626        | DEC addr ⇒ λinstr_refl.
627           let s ≝ add_ticks1 s in
628           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
629             set_arg_8 … s addr result
630        | MUL addr1 addr2 ⇒ λinstr_refl.
631           let s ≝ add_ticks1 s in
632           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
633           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
634           let product ≝ acc_a_nat * acc_b_nat in
635           let ov_flag ≝ product ≥ 256 in
636           let low ≝ bitvector_of_nat 8 (product mod 256) in
637           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
638           let s ≝ set_8051_sfr … s SFR_ACC_A low in
639             set_8051_sfr … s SFR_ACC_B high
640        | DIV addr1 addr2 ⇒ λinstr_refl.
641           let s ≝ add_ticks1 s in
642           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
643           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
644             match acc_b_nat with
645               [ O ⇒ set_flags … s false (None Bit) true
646               | S o ⇒
647                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
648                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
649                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
650                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
651                   set_flags … s false (None Bit) false
652               ]
653        | DA addr ⇒ λinstr_refl.
654            let s ≝ add_ticks1 s in
655            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
656              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
657                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
658                let cy_flag ≝ get_index' ? O ? flags in
659                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
660                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
661                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
662                    let new_acc ≝ nu @@ acc_nl' in
663                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
664                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
665                  else
666                    s
667              else
668                s
669        | CLR addr ⇒ λinstr_refl.
670          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
671            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
672              let s ≝ add_ticks1 s in
673               set_arg_8 … s ACC_A (zero 8)
674            | CARRY ⇒ λcarry: True.  λEQaddr.
675              let s ≝ add_ticks1 s in
676               set_arg_1 … s CARRY false
677            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
678              let s ≝ add_ticks1 s in
679               set_arg_1 … s (BIT_ADDR b) false
680            | _ ⇒ λother: False. ⊥
681            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
682        | CPL addr ⇒ λinstr_refl.
683          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
684            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
685                let s ≝ add_ticks1 s in
686                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
687                let new_acc ≝ negation_bv ? old_acc in
688                 set_8051_sfr … s SFR_ACC_A new_acc
689            | CARRY ⇒ λcarry: True. λEQaddr.
690                let s ≝ add_ticks1 s in
691                let old_cy_flag ≝ get_arg_1 … s CARRY true in
692                let new_cy_flag ≝ ¬old_cy_flag in
693                 set_arg_1 … s CARRY new_cy_flag
694            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
695                let s ≝ add_ticks1 s in
696                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
697                let new_bit ≝ ¬old_bit in
698                 set_arg_1 … s (BIT_ADDR b) new_bit
699            | _ ⇒ λother: False. ?
700            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
701        | SETB b ⇒ λinstr_refl.
702            let s ≝ add_ticks1 s in
703            set_arg_1 … s b false
704        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
705            let s ≝ add_ticks1 s in
706            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
707            let new_acc ≝ rotate_left … 1 old_acc in
708              set_8051_sfr … s SFR_ACC_A new_acc
709        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
710            let s ≝ add_ticks1 s in
711            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
712            let new_acc ≝ rotate_right … 1 old_acc in
713              set_8051_sfr … s SFR_ACC_A new_acc
714        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
715            let s ≝ add_ticks1 s in
716            let old_cy_flag ≝ get_cy_flag ?? s in
717            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
718            let new_cy_flag ≝ get_index' ? O ? old_acc in
719            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
720            let s ≝ set_arg_1 … s CARRY new_cy_flag in
721              set_8051_sfr … s SFR_ACC_A new_acc
722        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
723            let s ≝ add_ticks1 s in
724            let old_cy_flag ≝ get_cy_flag ?? s in
725            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
726            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
727            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
728            let s ≝ set_arg_1 … s CARRY new_cy_flag in
729              set_8051_sfr … s SFR_ACC_A new_acc
730        | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *)
731            let s ≝ add_ticks1 s in
732            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
733            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
734            let new_acc ≝ nl @@ nu in
735              set_8051_sfr … s SFR_ACC_A new_acc
736        | PUSH addr ⇒ λinstr_refl.
737            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with
738              [ DIRECT d ⇒ λdirect: True. λEQaddr.
739                let s ≝ add_ticks1 s in
740                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
741                let s ≝ set_8051_sfr … s SFR_SP new_sp in
742                  write_at_stack_pointer … s d
743              | _ ⇒ λother: False. ⊥
744              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
745        | POP addr ⇒ λinstr_refl.
746            let s ≝ add_ticks1 s in
747            let contents ≝ read_at_stack_pointer ?? s in
748            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
749            let s ≝ set_8051_sfr … s SFR_SP new_sp in
750              set_arg_8 … s addr contents
751        | XCH addr1 addr2 ⇒ λinstr_refl.
752            let s ≝ add_ticks1 s in
753            let old_addr ≝ get_arg_8 … s false addr2 in
754            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
755            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
756              set_arg_8 … s addr2 old_acc
757        | XCHD addr1 addr2 ⇒ λinstr_refl.
758            let s ≝ add_ticks1 s in
759            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
760            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
761            let new_acc ≝ acc_nu @@ arg_nl in
762            let new_arg ≝ arg_nu @@ acc_nl in
763            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
764              set_arg_8 … s addr2 new_arg
765        | RET ⇒ λinstr_refl.
766            let s ≝ add_ticks1 s in
767            let high_bits ≝ read_at_stack_pointer ?? s in
768            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
769            let s ≝ set_8051_sfr … s SFR_SP new_sp in
770            let low_bits ≝ read_at_stack_pointer ?? s in
771            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
772            let s ≝ set_8051_sfr … s SFR_SP new_sp in
773            let new_pc ≝ high_bits @@ low_bits in
774              set_program_counter … s new_pc
775        | RETI ⇒ λinstr_refl.
776            let s ≝ add_ticks1 s in
777            let high_bits ≝ read_at_stack_pointer ?? s in
778            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
779            let s ≝ set_8051_sfr … s SFR_SP new_sp in
780            let low_bits ≝ read_at_stack_pointer ?? s in
781            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
782            let s ≝ set_8051_sfr … s SFR_SP new_sp in
783            let new_pc ≝ high_bits @@ low_bits in
784              set_program_counter … s new_pc
785        | MOVX addr ⇒ λinstr_refl.
786          let s ≝ add_ticks1 s in
787          (* DPM: only copies --- doesn't affect I/O *)
788          match addr with
789            [ inl l ⇒
790              let 〈addr1, addr2〉 ≝ l in
791                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
792            | inr r ⇒
793              let 〈addr1, addr2〉 ≝ r in
794                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
795            ]
796        | MOV addr ⇒ λinstr_refl.
797          let s ≝ add_ticks1 s in
798          match addr with
799            [ inl l ⇒
800              match l with
801                [ inl l' ⇒
802                  match l' with
803                    [ inl l'' ⇒
804                      match l'' with
805                        [ inl l''' ⇒
806                          match l''' with
807                            [ inl l'''' ⇒
808                              let 〈addr1, addr2〉 ≝ l'''' in
809                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
810                            | inr r'''' ⇒
811                              let 〈addr1, addr2〉 ≝ r'''' in
812                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
813                            ]
814                        | inr r''' ⇒
815                          let 〈addr1, addr2〉 ≝ r''' in
816                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
817                        ]
818                    | inr r'' ⇒
819                      let 〈addr1, addr2〉 ≝ r'' in
820                       set_arg_16 … s (get_arg_16 … s addr2) addr1
821                    ]
822                | inr r ⇒
823                  let 〈addr1, addr2〉 ≝ r in
824                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
825                ]
826            | inr r ⇒
827              let 〈addr1, addr2〉 ≝ r in
828               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
829            ]
830          | JC addr ⇒ λinstr_refl.
831                  if get_cy_flag ?? s then
832                    let s ≝ add_ticks1 s in
833                      set_program_counter … s (addr_of addr s)
834                  else
835                    let s ≝ add_ticks2 s in
836                      s
837            | JNC addr ⇒ λinstr_refl.
838                  if ¬(get_cy_flag ?? s) then
839                   let s ≝ add_ticks1 s in
840                     set_program_counter … s (addr_of addr s)
841                  else
842                   let s ≝ add_ticks2 s in
843                    s
844            | JB addr1 addr2 ⇒ λinstr_refl.
845                  if get_arg_1 … s addr1 false then
846                   let s ≝ add_ticks1 s in
847                    set_program_counter … s (addr_of addr2 s)
848                  else
849                   let s ≝ add_ticks2 s in
850                    s
851            | JNB addr1 addr2 ⇒ λinstr_refl.
852                  if ¬(get_arg_1 … s addr1 false) then
853                   let s ≝ add_ticks1 s in
854                    set_program_counter … s (addr_of addr2 s)
855                  else
856                   let s ≝ add_ticks2 s in
857                    s
858            | JBC addr1 addr2 ⇒ λinstr_refl.
859                  let s ≝ set_arg_1 … s addr1 false in
860                    if get_arg_1 … s addr1 false then
861                     let s ≝ add_ticks1 s in
862                      set_program_counter … s (addr_of addr2 s)
863                    else
864                     let s ≝ add_ticks2 s in
865                      s
866            | JZ addr ⇒ λinstr_refl.
867                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
868                     let s ≝ add_ticks1 s in
869                      set_program_counter … s (addr_of addr s)
870                    else
871                     let s ≝ add_ticks2 s in
872                      s
873            | JNZ addr ⇒ λinstr_refl.
874                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
875                     let s ≝ add_ticks1 s in
876                      set_program_counter … s (addr_of addr s)
877                    else
878                     let s ≝ add_ticks2 s in
879                      s
880            | CJNE addr1 addr2 ⇒ λinstr_refl.
881                  match addr1 with
882                    [ inl l ⇒
883                        let 〈addr1, addr2'〉 ≝ l in
884                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
885                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
886                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
887                            let s ≝ add_ticks1 s in
888                            let s ≝ set_program_counter … s (addr_of addr2 s) in
889                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
890                          else
891                            let s ≝ add_ticks2 s in
892                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
893                    | inr r' ⇒
894                        let 〈addr1, addr2'〉 ≝ r' in
895                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
896                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
897                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
898                            let s ≝ add_ticks1 s in
899                            let s ≝ set_program_counter … s (addr_of addr2 s) in
900                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
901                          else
902                            let s ≝ add_ticks2 s in
903                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
904                    ]
905            | DJNZ addr1 addr2 ⇒ λinstr_refl.
906              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
907              let s ≝ set_arg_8 … s addr1 result in
908                if ¬(eq_bv ? result (zero 8)) then
909                 let s ≝ add_ticks1 s in
910                  set_program_counter … s (addr_of addr2 s)
911                else
912                 let s ≝ add_ticks2 s in
913                  s
914           ] (refl … instr))
915  try cases other
916  try assumption (*20s*)
917  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
918  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
919  whd in match execute_1_preinstruction; normalize nodelta
920  [(*1,2: (* ADD and ADDC *)
921    (* XXX: work on the right hand side *)
922    (* XXX: switch to the left hand side *)
923    >EQP -P normalize nodelta
924    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
925    whd in maps_assm:(??%%);
926    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
927    [2,4: normalize nodelta #absurd destruct(absurd) ]
928    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
929    [2,4: normalize nodelta #absurd destruct(absurd) ]
930    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
931    whd in ⊢ (??%?);
932    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
933    whd in ⊢ (??%?);
934    normalize nodelta >EQs >EQticks <instr_refl
935    @let_pair_in_status_of_pseudo_status
936    [1,3:
937      @eq_f3
938      [1,2,4,5:
939        @(pose … (set_clock ????)) #status #status_refl
940        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
941        [1,5:
942          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
943          @(subaddressing_mode_elim … addr1) %
944        |3,7:
945          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
946          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
947        |2,6:
948          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
949          @(subaddressing_mode_elim … addr1) %
950        |4,8:
951          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
952          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
953        ]
954      |3:
955        %
956      |6:
957        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
958        @sym_eq @set_clock_status_of_pseudo_status %
959      ]
960    |2,4:
961      #result #flags @sym_eq
962      @set_flags_status_of_pseudo_status try %
963      @sym_eq @set_arg_8_status_of_pseudo_status try %
964      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
965    ]
966  |3: (* SUBB *)
967    (* XXX: work on the right hand side *)
968    (* XXX: switch to the left hand side *)
969    >EQP -P normalize nodelta
970    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
971    whd in maps_assm:(??%%);
972    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
973    [2,4: normalize nodelta #absurd destruct(absurd) ]
974    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
975    [2,4: normalize nodelta #absurd destruct(absurd) ]
976    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
977    whd in ⊢ (??%?);
978    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
979    whd in ⊢ (??%?);
980    @(pair_replace ?????????? p)
981    [1:
982      @eq_f3
983      normalize nodelta >EQs >EQticks <instr_refl
984      [1:
985        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
986        @(get_arg_8_status_of_pseudo_status cm status … M')
987        [1:
988          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
989        |2:
990          >status_refl
991          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
992          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
993        |3:
994          >status_refl
995          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
996          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
997        ]
998      |2:
999        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
1000        @(get_arg_8_status_of_pseudo_status cm status … M')
1001        [1:
1002          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
1003        |2:
1004          >status_refl
1005          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
1006          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
1007        |3:
1008          >status_refl
1009          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1010          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
1011        ]
1012      |3:
1013        @(get_cy_flag_status_of_pseudo_status … M')
1014        @sym_eq @set_clock_status_of_pseudo_status
1015        [1:
1016          @sym_eq @set_program_counter_status_of_pseudo_status %
1017        |2:
1018          %
1019        ]
1020      ]
1021    |2:
1022      normalize nodelta
1023      @(pair_replace ?????????? p)
1024      [1:
1025        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
1026      |2:
1027        @set_flags_status_of_pseudo_status try %
1028        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
1029        [1:
1030          @sym_eq @set_clock_status_of_pseudo_status %
1031        |2:
1032          @I
1033        |3:
1034          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
1035          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
1036        ]
1037      ]
1038    ]
1039  |4: (* INC *)
1040    (* XXX: work on the right hand side *)
1041    (* XXX: switch to the left hand side *)
1042    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
1043    @(subaddressing_mode_elim … addr) normalize nodelta
1044    [1:
1045      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1046      whd in maps_assm:(??%%);
1047      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1048      [2: normalize nodelta #absurd destruct(absurd) ]
1049      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1050      whd in ⊢ (??%?);
1051      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1052      whd in ⊢ (??%?);
1053      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
1054      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
1055      [1:
1056        @eq_f2 try %
1057        @(pose … (set_clock ????)) #status #status_refl
1058        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1059        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
1060      |2:
1061        @set_arg_8_status_of_pseudo_status try %
1062        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
1063      ]
1064    |2:
1065      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1066      whd in maps_assm:(??%%);
1067      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1068      [2: normalize nodelta #absurd destruct(absurd) ]
1069      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1070      whd in ⊢ (??%?);
1071      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1072      whd in ⊢ (??%?);
1073      @let_pair_in_status_of_pseudo_status
1074      [1:
1075        @eq_f2 try %
1076        @(pose … (set_clock ????)) #status #status_refl
1077        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1078        >EQs >EQticks
1079        [1:
1080          @sym_eq @set_clock_status_of_pseudo_status %
1081        |2:
1082          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1083        |3:
1084          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
1085        ]
1086      |2:
1087        #carry #result
1088        @sym_eq @set_arg_8_status_of_pseudo_status try %
1089        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1090      ]
1091    |3:
1092      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1093      whd in maps_assm:(??%%);
1094      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1095      [2: normalize nodelta #absurd destruct(absurd) ]
1096      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1097      whd in ⊢ (??%?);
1098      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1099      whd in ⊢ (??%?);
1100      @let_pair_in_status_of_pseudo_status
1101      [1:
1102        @eq_f2 try %
1103        @(pose … (set_clock ????)) #status #status_refl
1104        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1105        >EQs >EQticks
1106        [1:
1107          @sym_eq @set_clock_status_of_pseudo_status %
1108        |2:
1109          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1110        |3:
1111          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
1112        ]
1113      |2:
1114        #carry #result
1115        @sym_eq @set_arg_8_status_of_pseudo_status try %
1116        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
1117      ]
1118    |4:
1119      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1120      whd in maps_assm:(??%%);
1121      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1122      [2: normalize nodelta #absurd destruct(absurd) ]
1123      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1124      whd in ⊢ (??%?);
1125      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1126      whd in ⊢ (??%?);
1127      @let_pair_in_status_of_pseudo_status
1128      [1:
1129        @eq_f2 try %
1130        @(pose … (set_clock ????)) #status #status_refl
1131        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1132        >EQs >EQticks
1133        [1:
1134          @sym_eq @set_clock_status_of_pseudo_status %
1135        |2:
1136          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1137        |3:
1138          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1139        ]
1140      |2:
1141        #carry #result
1142        @sym_eq @set_arg_8_status_of_pseudo_status try %
1143        [1:
1144          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1145        |2:
1146          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
1147        ]
1148      ]
1149    |5:
1150      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1151      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1152      whd in ⊢ (??%?);
1153      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1154      whd in ⊢ (??%?);
1155      @let_pair_in_status_of_pseudo_status
1156      [1:
1157        @eq_f2 try %
1158        @(pose … (set_clock ????)) #status #status_refl
1159        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
1160        >EQs >EQticks %
1161      |2:
1162        #carry #bl
1163        @sym_eq @let_pair_in_status_of_pseudo_status
1164        [1:
1165          @eq_f3 try %
1166          @(pose … (set_clock ????)) #status #status_refl
1167          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
1168          >EQs >EQticks %
1169        |2:
1170          #carry' #bu
1171          @sym_eq @set_8051_sfr_status_of_pseudo_status %
1172        ]
1173      ]
1174    ]
1175  |5: (* DEC *)
1176    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
1177    @(subaddressing_mode_elim … addr) normalize nodelta
1178    [1:
1179      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1180      whd in maps_assm:(??%%);
1181      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1182      [2: normalize nodelta #absurd destruct(absurd) ]
1183      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1184      whd in ⊢ (??%?);
1185      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1186      whd in ⊢ (??%?);
1187      @let_pair_in_status_of_pseudo_status
1188      [1:
1189        @eq_f3 try %
1190        @(pose … (set_clock ????)) #status #status_refl
1191        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1192        >EQs >EQticks try %
1193        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1194      |2:
1195        #result #flags
1196        @sym_eq @set_arg_8_status_of_pseudo_status try %
1197        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1198      ]
1199    |2:
1200      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1201      whd in maps_assm:(??%%);
1202      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1203      [2: normalize nodelta #absurd destruct(absurd) ]
1204      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1205      whd in ⊢ (??%?);
1206      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1207      whd in ⊢ (??%?);
1208      @let_pair_in_status_of_pseudo_status
1209      [1:
1210        @eq_f3 try %
1211        @(pose … (set_clock ????)) #status #status_refl
1212        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1213        >EQs >EQticks try %
1214        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1215      |2:
1216        #result #flags
1217        @sym_eq @set_arg_8_status_of_pseudo_status try %
1218        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1219      ]
1220    |3:
1221      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1222      whd in maps_assm:(??%%);
1223      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1224      [2: normalize nodelta #absurd destruct(absurd) ]
1225      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1226      whd in ⊢ (??%?);
1227      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1228      whd in ⊢ (??%?);
1229      @let_pair_in_status_of_pseudo_status
1230      [1:
1231        @eq_f3 try %
1232        @(pose … (set_clock ????)) #status #status_refl
1233        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1234        >EQs >EQticks try %
1235        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1236      |2:
1237        #result #flags
1238        @sym_eq @set_arg_8_status_of_pseudo_status try %
1239        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1240      ]
1241    |4:
1242      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1243      whd in maps_assm:(??%%);
1244      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1245      [2: normalize nodelta #absurd destruct(absurd) ]
1246      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1247      whd in ⊢ (??%?);
1248      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1249      whd in ⊢ (??%?);
1250      @let_pair_in_status_of_pseudo_status
1251      [1:
1252        @eq_f3 try %
1253        @(pose … (set_clock ????)) #status #status_refl
1254        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1255        >EQs >EQticks try %
1256        [1:
1257          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1258        |2:
1259          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1260        ]
1261      |2:
1262        #result #flags
1263        @sym_eq @set_arg_8_status_of_pseudo_status try %
1264        [1:
1265          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1266        |2:
1267          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1268        ]
1269      ]
1270    ]
1271  |6: (* MUL *)
1272    (* XXX: work on the right hand side *)
1273    (* XXX: switch to the left hand side *)
1274    >EQP -P normalize nodelta
1275    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1276    whd in maps_assm:(??%%);
1277    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1278    [2: normalize nodelta #absurd destruct(absurd) ]
1279    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1280    [2: normalize nodelta #absurd destruct(absurd) ]
1281    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1282    whd in ⊢ (??%?);
1283    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1284    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1285    [2:
1286      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
1287      @sym_eq
1288      [1:
1289        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1290        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
1291        %
1292      |2:
1293        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
1294      ]
1295    ]
1296    @sym_eq @set_8051_sfr_status_of_pseudo_status
1297    [2:
1298      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
1299      @eq_f @eq_f2 try % @eq_f2 @eq_f
1300      @sym_eq
1301      [1:
1302        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1303        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1304      |2:
1305        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
1306      ]
1307    ]
1308    @sym_eq @set_clock_status_of_pseudo_status
1309    [2:
1310      @eq_f %
1311    ]
1312    @sym_eq @set_program_counter_status_of_pseudo_status %
1313  |7,8: (* DIV *)
1314    (* XXX: work on the right hand side *)
1315    (* XXX: switch to the left hand side *)
1316    >EQP -P normalize nodelta
1317    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1318    whd in maps_assm:(??%%);
1319    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1320    [2,4: normalize nodelta #absurd destruct(absurd) ]
1321    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1322    [2,4: normalize nodelta #absurd destruct(absurd) ]
1323    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1324    whd in ⊢ (??%?);
1325    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1326    whd in ⊢ (??%?); normalize nodelta
1327    @(match_nat_status_of_pseudo_status M' cm sigma policy)
1328    [1,4:
1329      @eq_f
1330      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1331      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1332    |2,5:
1333      @sym_eq @set_flags_status_of_pseudo_status %
1334    |3,6:
1335      #n @sym_eq @set_flags_status_of_pseudo_status try %
1336      @sym_eq @set_8051_sfr_status_of_pseudo_status
1337      [1,3:
1338        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
1339        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
1340        @eq_f @eq_f2 try % @eq_f
1341        @(pose … (set_clock ????)) #status #status_refl
1342        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1343        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1344      |2,4:
1345        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
1346        @(pose … (set_clock ????)) #status #status_refl
1347        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1348        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1349      ]
1350    ]
1351  |9: (* DA *)
1352    (* XXX: work on the right hand side *)
1353    (* XXX: switch to the left hand side *)
1354    >EQP -P normalize nodelta
1355    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1356    whd in maps_assm:(??%%);
1357    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1358    [2: normalize nodelta #absurd destruct(absurd) ]
1359    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1360    whd in ⊢ (??%?);
1361    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1362    whd in ⊢ (??%?); normalize nodelta
1363    @(pair_replace ?????????? p)
1364    [1:
1365      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1366      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1367      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1368    |2:
1369      @(pair_replace ?????????? p)
1370      [1:
1371        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1372      |2:
1373        @(if_then_else_replace ???????? p1) normalize nodelta
1374        [1:
1375          cases (gtb ? 9)
1376          [1:
1377            %
1378          |2:
1379            change with (get_ac_flag ??? = get_ac_flag ???)
1380            @(get_ac_flag_status_of_pseudo_status M')
1381            @sym_eq @set_clock_status_of_pseudo_status
1382            >EQs >EQticks <instr_refl %
1383          ]
1384        |2:
1385          @(if_then_else_replace ???????? p1) normalize nodelta try %
1386          @(pair_replace ?????????? p2)
1387          [1:
1388            @eq_f3 try % normalize nodelta
1389            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1390            whd in ⊢ (??%?);
1391            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1392          |2:
1393            @(pair_replace ?????????? p2) try %
1394            @(pair_replace ?????????? p3) try %
1395            @(pair_replace ?????????? p3) try %
1396            @(if_then_else_replace ???????? p4) try % normalize nodelta
1397            @(if_then_else_replace ???????? p4) try % normalize nodelta
1398            @(pair_replace ?????????? p5) try %
1399            @(pair_replace ?????????? p5) try %
1400            @set_flags_status_of_pseudo_status try %
1401            [1:
1402              @eq_f @(get_ac_flag_status_of_pseudo_status M')
1403              @sym_eq @set_8051_sfr_status_of_pseudo_status
1404              [1:
1405                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1406              |2:
1407                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1408              ]
1409            |2:
1410              @(get_ov_flag_status_of_pseudo_status M')
1411              @sym_eq @set_8051_sfr_status_of_pseudo_status
1412              [1:
1413                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1414              |2:
1415                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1416              ]
1417            |3:
1418              @sym_eq @set_8051_sfr_status_of_pseudo_status
1419              [1:
1420                @sym_eq @set_clock_status_of_pseudo_status
1421                [1:
1422                  >EQs
1423                  @sym_eq @set_program_counter_status_of_pseudo_status %
1424                |2:
1425                  >EQs >EQticks <instr_refl %
1426                ]
1427              |2:
1428                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1429              ]
1430            ]
1431          ]
1432        ]
1433      ]
1434    ]
1435  |10: (* DA *)
1436    (* XXX: work on the right hand side *)
1437    (* XXX: switch to the left hand side *)
1438    >EQP -P normalize nodelta
1439    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1440    whd in maps_assm:(??%%);
1441    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1442    [2: normalize nodelta #absurd destruct(absurd) ]
1443    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1444    whd in ⊢ (??%?);
1445    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1446    whd in ⊢ (??%?); normalize nodelta
1447    @(pair_replace ?????????? p)
1448    [1:
1449      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1450      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1451      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1452    |2:
1453      @(pair_replace ?????????? p)
1454      [1:
1455        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1456      |2:
1457        @(if_then_else_replace ???????? p1) normalize nodelta
1458        [1:
1459          cases (gtb ? 9)
1460          [1:
1461            %
1462          |2:
1463            change with (get_ac_flag ??? = get_ac_flag ???)
1464            @(get_ac_flag_status_of_pseudo_status M')
1465            @sym_eq @set_clock_status_of_pseudo_status
1466            >EQs >EQticks <instr_refl %
1467          ]
1468        |2:
1469          @(if_then_else_replace ???????? p1) normalize nodelta try %
1470          @(pair_replace ?????????? p2)
1471          [1:
1472            @eq_f3 try % normalize nodelta
1473            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1474            whd in ⊢ (??%?);
1475            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1476          |2:
1477            @(pair_replace ?????????? p2) try %
1478            @(pair_replace ?????????? p3) try %
1479            @(pair_replace ?????????? p3) try %
1480            @(if_then_else_replace ???????? p4) try % normalize nodelta
1481            @(if_then_else_replace ???????? p4) try % normalize nodelta
1482            @set_clock_status_of_pseudo_status
1483            [1:
1484              >EQs
1485              @sym_eq @set_program_counter_status_of_pseudo_status %
1486            |2:
1487              >EQs >EQticks <instr_refl %
1488            ]
1489          ]
1490        ]
1491      ]
1492    ]
1493  |11: (* DA *)
1494    (* XXX: work on the right hand side *)
1495    (* XXX: switch to the left hand side *)
1496    >EQP -P normalize nodelta
1497    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1498    whd in maps_assm:(??%%);
1499    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1500    [2: normalize nodelta #absurd destruct(absurd) ]
1501    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1502    whd in ⊢ (??%?);
1503    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1504    whd in ⊢ (??%?); normalize nodelta
1505    @(pair_replace ?????????? p)
1506    [1:
1507      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1508      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1509      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1510    |2:
1511      @(pair_replace ?????????? p)
1512      [1:
1513        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1514      |2:
1515        @(if_then_else_replace ???????? p1) normalize nodelta
1516        [1:
1517          cases (gtb ? 9)
1518          [1:
1519            %
1520          |2:
1521            change with (get_ac_flag ??? = get_ac_flag ???)
1522            @(get_ac_flag_status_of_pseudo_status M')
1523            @sym_eq @set_clock_status_of_pseudo_status
1524            >EQs >EQticks <instr_refl %
1525          ]
1526        |2:
1527          @(if_then_else_replace ???????? p1) normalize nodelta try %
1528          @set_clock_status_of_pseudo_status
1529          [1:
1530            >EQs
1531            @sym_eq @set_program_counter_status_of_pseudo_status %
1532          |2:
1533            >EQs >EQticks <instr_refl %
1534          ]
1535        ]
1536      ]
1537    ]
1538  |*)12: (* JC *)
1539    >EQP -P normalize nodelta
1540    whd in match expand_pseudo_instruction; normalize nodelta
1541    whd in match expand_relative_jump; normalize nodelta
1542    whd in match expand_relative_jump_internal; normalize nodelta
1543    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1544    inversion sj_possible #sj_possible_refl normalize nodelta
1545    [1:
1546      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1547      whd in maps_assm:(??%%);
1548      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1549      whd in ⊢ (??%?); normalize nodelta
1550      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1551      whd in ⊢ (??%?);
1552      @if_then_else_status_of_pseudo_status
1553      >EQs >EQticks <instr_refl normalize nodelta
1554      [1:
1555        @(get_cy_flag_status_of_pseudo_status M') %
1556      |2:
1557        @sym_eq @set_program_counter_status_of_pseudo_status
1558        [1:
1559        |2:
1560          @sym_eq @set_clock_status_of_pseudo_status try %
1561          whd in match ticks_of0; normalize nodelta
1562          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1563          [1:
1564            @eq_f2 try %
1565            >sigma_increment_commutation
1566            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
1567            * #sigma_zero_assm #relevant cases (relevant ppc ?)
1568            [1:
1569              -relevant
1570              [2:
1571                >EQcm assumption
1572              |1:
1573                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
1574                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
1575              ]
1576            |2:
1577            ]
1578          |2:
1579            >sj_possible_refl %
1580          ]
1581        ]
1582      |3:
1583      ]
1584    ]
1585    cases daemon
1586  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
1587    cases daemon
1588  |(*29,30: (* ANL and ORL *)
1589    inversion addr
1590    [1,3:
1591      *
1592      [1,3:
1593        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1594        >EQP -P normalize nodelta
1595        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1596        whd in maps_assm:(??%%);
1597        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1598        [2,4: normalize nodelta #absurd destruct(absurd) ]
1599        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1600        [2,4: normalize nodelta #absurd destruct(absurd) ]
1601        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1602        whd in ⊢ (??%?);
1603        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1604        change with (set_arg_8 ????? = ?)
1605        @set_arg_8_status_of_pseudo_status try %
1606        >EQs >EQticks <instr_refl >addr_refl
1607        [1,4:
1608          @sym_eq @set_clock_status_of_pseudo_status
1609          [1,3:
1610            @sym_eq @set_program_counter_status_of_pseudo_status %
1611          |2,4:
1612            @eq_f2 %
1613          ]
1614        |2,5:
1615          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1616          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
1617        |3,6:
1618          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1619          [1,5:
1620            @(subaddressing_mode_elim … acc_a) %
1621          |4,8:
1622            @eq_f2
1623            @(pose … (set_clock ????)) #status #status_refl
1624            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1625            [1,5:
1626              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1627              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
1628            |3,7:
1629              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1630              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1631            |2,6:
1632              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1633              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
1634            |4,8:
1635              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1636              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1637            ]
1638          |*:
1639            %
1640          ]
1641        ]
1642      |2,4:
1643        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1644        >EQP -P normalize nodelta
1645        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1646        whd in maps_assm:(??%%);
1647        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1648        [2,4: normalize nodelta #absurd destruct(absurd) ]
1649        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1650        [2,4: normalize nodelta #absurd destruct(absurd) ]
1651        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1652        whd in ⊢ (??%?);
1653        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1654        change with (set_arg_8 ????? = ?)
1655        @set_arg_8_status_of_pseudo_status try %
1656        >EQs >EQticks <instr_refl >addr_refl
1657        [1,4:
1658          @sym_eq @set_clock_status_of_pseudo_status
1659          [1,3:
1660            @sym_eq @set_program_counter_status_of_pseudo_status %
1661          |2,4:
1662            @eq_f2 %
1663          ]
1664        |2,5:
1665          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1666          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
1667        |3,6:
1668          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1669          [1,5:
1670            @(subaddressing_mode_elim … direct) #w %
1671          |4,8:
1672            @eq_f2
1673            @(pose … (set_clock ????)) #status #status_refl
1674            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1675            [1,5:
1676              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1677              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
1678            |3,7:
1679              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1680              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1681            |2,6:
1682              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1683              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
1684            |4,8:
1685              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1686              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1687            ]
1688          |*:
1689            %
1690          ]
1691        ]
1692      ]
1693    |2,4:
1694      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
1695      >EQP -P normalize nodelta
1696      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1697      whd in maps_assm:(??%%);
1698      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1699      [2,4: normalize nodelta #absurd destruct(absurd) ]
1700      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1701      [2,4: normalize nodelta #absurd destruct(absurd) ]
1702      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1703      whd in ⊢ (??%?);
1704      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1705      change with (set_flags ?????? = ?)
1706      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
1707      >EQs >EQticks <instr_refl >addr_refl
1708      @sym_eq @set_clock_status_of_pseudo_status %
1709    ]
1710  |31: (* XRL *)
1711    inversion addr
1712    [1:
1713      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1714      >EQP -P normalize nodelta
1715      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1716      whd in maps_assm:(??%%);
1717      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1718      [2: normalize nodelta #absurd destruct(absurd) ]
1719      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1720      [2: normalize nodelta #absurd destruct(absurd) ]
1721      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1722      whd in ⊢ (??%?);
1723      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1724      change with (set_arg_8 ????? = ?)
1725      @set_arg_8_status_of_pseudo_status try %
1726      >EQs >EQticks <instr_refl >addr_refl
1727      [1:
1728        @sym_eq @set_clock_status_of_pseudo_status
1729        [1:
1730          @sym_eq @set_program_counter_status_of_pseudo_status %
1731        |2:
1732          @eq_f2 %
1733        ]
1734      |2:
1735        @(subaddressing_mode_elim … acc_a) @I
1736      |3:
1737        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1738        [1:
1739          @(subaddressing_mode_elim … acc_a) %
1740        |4:
1741          @eq_f2
1742          @(pose … (set_clock ????)) #status #status_refl
1743          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1744          [1:
1745            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1746            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
1747          |3:
1748            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1749            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1750          |2:
1751            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1752            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
1753          |4:
1754            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1755            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1756          ]
1757        |*:
1758          %
1759        ]
1760      ]
1761    |2:
1762      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1763      >EQP -P normalize nodelta
1764      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1765      whd in maps_assm:(??%%);
1766      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1767      [2: normalize nodelta #absurd destruct(absurd) ]
1768      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1769      [2: normalize nodelta #absurd destruct(absurd) ]
1770      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1771      whd in ⊢ (??%?);
1772      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1773      change with (set_arg_8 ????? = ?)
1774      @set_arg_8_status_of_pseudo_status try %
1775      >EQs >EQticks <instr_refl >addr_refl
1776      [1:
1777        @sym_eq @set_clock_status_of_pseudo_status
1778        [1:
1779          @sym_eq @set_program_counter_status_of_pseudo_status %
1780        |2:
1781          @eq_f2 %
1782        ]
1783      |2:
1784        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1785        [1: @(subaddressing_mode_elim … direct) #w % ] %
1786      |3:
1787        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1788        [1:
1789          @(subaddressing_mode_elim … direct) #w %
1790        |4:
1791          @eq_f2
1792          @(pose … (set_clock ????)) #status #status_refl
1793          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1794          [1:
1795            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1796            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
1797          |3:
1798            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1799            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1800          |2:
1801            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1802            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
1803          |4:
1804            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1805            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1806          ]
1807        |*:
1808          %
1809        ]
1810      ]
1811    ]
1812  |32: (* CLR *)
1813    >EQP -P normalize nodelta lapply instr_refl
1814    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1815    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1816    whd in maps_assm:(??%%);
1817    [1,2:
1818      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1819      [2,4: normalize nodelta #absurd destruct(absurd) ]
1820      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1821      whd in ⊢ (??%?);
1822      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1823      [1:
1824        >EQs >EQticks <instr_refl
1825        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1826        @set_arg_1_status_of_pseudo_status try %
1827        [1:
1828          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
1829        |2:
1830          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
1831        ]         
1832      |2:
1833        >EQs >EQticks <instr_refl
1834        change with (set_arg_8 ??? ACC_A ? = ?) try %
1835        @set_arg_8_status_of_pseudo_status try %
1836        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1837      ]
1838    |3:
1839      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1840      whd in ⊢ (??%?);
1841      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1842      >EQs >EQticks <instr_refl
1843      change with (set_arg_1 ??? CARRY ? = ?) try %
1844      @set_arg_1_status_of_pseudo_status %
1845    ]
1846  |33: (* CPL *)
1847    >EQP -P normalize nodelta lapply instr_refl
1848    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1849    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1850    whd in maps_assm:(??%%);
1851    [1,2:
1852      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1853      [2,4: normalize nodelta #absurd destruct(absurd) ]
1854      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1855      whd in ⊢ (??%?);
1856      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1857      [1:
1858        >EQs >EQticks <instr_refl
1859        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1860        @set_arg_1_status_of_pseudo_status
1861        [1:
1862          @eq_f
1863          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1864          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1865          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
1866        |2:
1867          %
1868        |3:
1869          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) %
1870        |4:
1871          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) %
1872        ]       
1873      |2:
1874        >EQs >EQticks <instr_refl
1875        change with (set_8051_sfr ????? = ?)
1876        @set_8051_sfr_status_of_pseudo_status try %
1877        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
1878        normalize nodelta @eq_f
1879        @(pose … (set_clock ????)) #status #status_refl
1880        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1881        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
1882      ]
1883    |3:
1884      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1885      whd in ⊢ (??%?);
1886      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1887      >EQs >EQticks <instr_refl
1888      change with (set_arg_1 ??? CARRY ? = ?) try %
1889      @set_arg_1_status_of_pseudo_status try %
1890      @eq_f
1891      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1892      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
1893    ]
1894  |34,36: (* RL and RR *)
1895    (* XXX: work on the right hand side *)
1896    (* XXX: switch to the left hand side *)
1897    >EQP -P normalize nodelta
1898    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1899    whd in maps_assm:(??%%);
1900    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1901    [2,4: normalize nodelta #absurd destruct(absurd) ]
1902    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1903    whd in ⊢ (??%?);
1904    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1905    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1906    [2,4:
1907      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1908      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1909      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1910      %
1911    ]
1912    @sym_eq @set_clock_status_of_pseudo_status
1913    [2,4:
1914      %
1915    ]
1916    @sym_eq @set_program_counter_status_of_pseudo_status %
1917  |35,37: (* RLC and RRC *)
1918    (* XXX: work on the right hand side *)
1919    (* XXX: switch to the left hand side *)
1920    >EQP -P normalize nodelta
1921    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1922    whd in maps_assm:(??%%);
1923    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1924    [2,4: normalize nodelta #absurd destruct(absurd) ]
1925    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1926    whd in ⊢ (??%?);
1927    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1928    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1929    [2,4:
1930      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1931      @eq_f2
1932      [1,3:
1933        @sym_eq
1934        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1935        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1936      |2,4:
1937        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
1938        @sym_eq @set_clock_status_of_pseudo_status %
1939      ]
1940    |1,3:
1941      @sym_eq @set_arg_1_status_of_pseudo_status try %
1942      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1943      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1944    ]
1945  |38: (* SWAP *)
1946    >EQP -P normalize nodelta
1947    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1948    whd in maps_assm:(??%%);
1949    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1950    [2: normalize nodelta #absurd destruct(absurd) ]
1951    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1952    whd in ⊢ (??%?);
1953    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1954    whd in ⊢ (??%?);
1955    @(pair_replace ?????????? p)
1956    [1:
1957      @eq_f normalize nodelta
1958      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1959      @(get_8051_sfr_status_of_pseudo_status … M' … status)
1960      [1:
1961        >status_refl -status_refl
1962        @sym_eq @set_clock_status_of_pseudo_status
1963        >EQs >EQticks <instr_refl %
1964      |2:
1965        whd in ⊢ (??%?);
1966        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1967      ]
1968    |2:
1969      @(pair_replace ?????????? p) normalize nodelta
1970      [1:
1971        %
1972      |2:
1973        @set_8051_sfr_status_of_pseudo_status
1974        [1:
1975          @sym_eq @set_clock_status_of_pseudo_status
1976          >EQs >EQticks <instr_refl %
1977        |2:
1978          whd in ⊢ (??%?);
1979          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1980        ]
1981      ]     
1982    ]
1983  |39: (* MOV *)
1984    >EQP -P normalize nodelta
1985    inversion addr
1986    [1:
1987      #addr' normalize nodelta
1988      inversion addr'
1989      [1:
1990        #addr'' normalize nodelta
1991        inversion addr''
1992        [1:
1993          #addr''' normalize nodelta
1994          inversion addr'''
1995          [1:
1996            #addr'''' normalize nodelta
1997            inversion addr''''
1998            [1:
1999              normalize nodelta #acc_a_others
2000              cases acc_a_others #acc_a #others
2001              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2002              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2003              whd in maps_assm:(??%%);
2004              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2005              [2: normalize nodelta #absurd destruct(absurd) ]
2006              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2007              [2: normalize nodelta #absurd destruct(absurd) ]
2008              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2009              whd in ⊢ (??%?);
2010              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2011              change with (set_arg_8 ????? = ?)
2012              @set_arg_8_status_of_pseudo_status try %
2013              [1:
2014                @sym_eq @set_clock_status_of_pseudo_status
2015                >EQs >EQticks <instr_refl >addr_refl %
2016              |2:
2017                @(subaddressing_mode_elim … acc_a) @I
2018              |3:
2019                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2020                [1: @(subaddressing_mode_elim … acc_a) % ]
2021                >EQs >EQticks <instr_refl >addr_refl
2022                [1,2:
2023                  %
2024                |3:
2025                  @(pose … (set_clock ????)) #status #status_refl
2026                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
2027                  [1:
2028                    @sym_eq @set_clock_status_of_pseudo_status %
2029                  |2:
2030                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2031                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2032                  |3:
2033                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2034                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2035                  ]
2036                ]
2037              ]
2038            |2:
2039              #others_others' cases others_others' #others #others' normalize nodelta
2040              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2041              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2042              whd in maps_assm:(??%%);
2043              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2044              [2: normalize nodelta #absurd destruct(absurd) ]
2045              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2046              [2: normalize nodelta #absurd destruct(absurd) ]
2047              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2048              whd in ⊢ (??%?);
2049              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2050              change with (set_arg_8 ????? = ?)
2051              @set_arg_8_status_of_pseudo_status try %
2052              >EQs >EQticks <instr_refl >addr_refl try %
2053              [1:
2054                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2055                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2056              |2:
2057                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2058                [1:
2059                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2060                |2,3:
2061                  %
2062                |4:
2063                  @(pose … (set_clock ????)) #status #status_refl
2064                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
2065                  [1:
2066                    @sym_eq @set_clock_status_of_pseudo_status %
2067                  |2:
2068                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
2069                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2070                  |3:
2071                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
2072                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2073                  ]
2074                ]
2075              ]
2076            ]
2077          |2:
2078            #direct_others cases direct_others #direct #others
2079            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2080            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2081            whd in maps_assm:(??%%);
2082            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2083            [2: normalize nodelta #absurd destruct(absurd) ]
2084            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2085            [2: normalize nodelta #absurd destruct(absurd) ]
2086            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2087            whd in ⊢ (??%?);
2088            <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2089            change with (set_arg_8 ????? = ?)
2090            @set_arg_8_status_of_pseudo_status try %
2091            >EQs >EQticks <instr_refl >addr_refl
2092            [1:
2093              @sym_eq @set_clock_status_of_pseudo_status %
2094            |2:
2095              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
2096              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2097            |3:
2098              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
2099              [1:
2100                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2101              |2,3:
2102                %
2103              |4:
2104                @(pose … (set_clock ????)) #status #status_refl
2105                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2106                [1:
2107                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2108                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2109                |2:
2110                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2111                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2112                ]
2113              ]
2114            ]
2115          ]
2116        |2:
2117          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
2118          #addr_refl'' #addr_refl' #addr_refl
2119          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2120          whd in maps_assm:(??%%);
2121          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2122          [2: normalize nodelta #absurd destruct(absurd) ]
2123          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2124          [2: normalize nodelta #absurd destruct(absurd) ]
2125          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2126          whd in ⊢ (??%?);
2127          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2128          change with (set_arg_16 ????? = ?)
2129          @set_arg_16_status_of_pseudo_status try %
2130          >EQs >EQticks <instr_refl >addr_refl
2131          @sym_eq @set_clock_status_of_pseudo_status %
2132        ]
2133      |2:
2134        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
2135        #addr_refl' #addr_refl
2136        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2137        whd in maps_assm:(??%%);
2138        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2139        [2: normalize nodelta #absurd destruct(absurd) ]
2140        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2141        [2: normalize nodelta #absurd destruct(absurd) ]
2142        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2143        whd in ⊢ (??%?);
2144        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2145        change with (set_arg_1 ????? = ?)
2146        @set_arg_1_status_of_pseudo_status
2147        >EQs >EQticks <instr_refl >addr_refl try %
2148        [1:
2149          @sym_eq @(pose … (set_clock ????)) #status #status_refl
2150          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2151          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
2152        |2,3:
2153          @(subaddressing_mode_elim … carry) @I
2154        ]
2155      ]
2156    |2:
2157      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
2158      #addr_refl
2159      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2160      whd in maps_assm:(??%%);
2161      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2162      [2: normalize nodelta #absurd destruct(absurd) ]
2163      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2164      [2: normalize nodelta #absurd destruct(absurd) ]
2165      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2166      whd in ⊢ (??%?);
2167      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2168      change with (set_arg_1 ????? = ?)
2169      @set_arg_1_status_of_pseudo_status
2170      [1:
2171        >EQs >EQticks <instr_refl >addr_refl
2172        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
2173        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2174        @(subaddressing_mode_elim … carry) @I
2175      |2:
2176        >EQs >EQticks <instr_refl >addr_refl %
2177      |3,4:
2178        @(pose … (set_clock ????)) #status #status_refl
2179        [1:
2180          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
2181        |2:
2182          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
2183        ]
2184        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
2185        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
2186        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
2187      ]
2188    ]
2189  |40: (* MOVX *)
2190    >EQP -P normalize nodelta
2191    inversion addr
2192    [1:
2193      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
2194      #addr_refl
2195      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2196      whd in maps_assm:(??%%);
2197      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2198      [2: normalize nodelta #absurd destruct(absurd) ]
2199      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2200      [2: normalize nodelta #absurd destruct(absurd) ]
2201      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2202      whd in ⊢ (??%?);
2203      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2204      change with (set_arg_8 ????? = ?)
2205      @set_arg_8_status_of_pseudo_status try %
2206      >EQs >EQticks <instr_refl >addr_refl
2207      [1:
2208        @sym_eq @set_clock_status_of_pseudo_status %
2209      |2:
2210        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
2211        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2212      |3:
2213        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2214        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
2215        @(pose … (set_clock ????)) #status #status_refl
2216        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2217        [1:
2218          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2219          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2220        |2:
2221          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2222          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2223        ]
2224      ]
2225    |2:
2226      #others_acc_a cases others_acc_a #others #acc_a
2227      #addr_refl
2228      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2229      whd in maps_assm:(??%%);
2230      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2231      [2: normalize nodelta #absurd destruct(absurd) ]
2232      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2233      [2: normalize nodelta #absurd destruct(absurd) ]
2234      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2235      whd in ⊢ (??%?);
2236      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2237      change with (set_arg_8 ????? = ?)
2238      @set_arg_8_status_of_pseudo_status
2239      >EQs >EQticks <instr_refl >addr_refl try %
2240      [1:
2241        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2242        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2243      |2:
2244        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2245        [1:
2246          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2247        |2,3:
2248          %
2249        |4:
2250          @(pose … (set_clock ????)) #status #status_refl
2251          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2252          [1:
2253            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
2254            [1: @(subaddressing_mode_elim … acc_a) % ] %
2255          |2:
2256            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
2257            [1: @(subaddressing_mode_elim … acc_a) % ] %
2258          ]
2259        ]
2260      ]
2261    ]
2262  |41: (* SETB *)
2263    >EQs >EQticks <instr_refl
2264    >EQP -P normalize nodelta
2265    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2266    whd in maps_assm:(??%%);
2267    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2268    [2: normalize nodelta #absurd destruct(absurd) ]
2269    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2270    whd in ⊢ (??%?);
2271    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2272    change with (set_arg_1 ????? = ?)
2273    @set_arg_1_status_of_pseudo_status try %
2274    [1:
2275      @(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)
2276    |2:
2277      @(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)
2278    ]
2279  |*)42: (* PUSH *)
2280    >EQP -P normalize nodelta lapply instr_refl
2281    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
2282    #sigma_increment_commutation
2283    whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
2284    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
2285    whd in ⊢ (??%?);
2286    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2287    whd in ⊢ (??%?);
2288    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
2289    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
2290    [1:
2291      @eq_f2 try %
2292      @(pose … (set_clock ????)) #status #status_refl
2293      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
2294      @sym_eq @set_clock_status_of_pseudo_status
2295      >EQs >EQticks <instr_refl %
2296    |2:
2297      >EQs >EQticks <instr_refl
2298      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
2299    ]
2300  |43: (* POP *)
2301    cases daemon
2302  |44:
2303    >EQP -P normalize nodelta
2304    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2305    whd in maps_assm:(??%%);
2306    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2307    [2: normalize nodelta #absurd destruct(absurd) ]
2308    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2309    [2: normalize nodelta #absurd destruct(absurd) ]
2310    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2311    whd in ⊢ (??%?);
2312    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2313    change with (set_arg_8 ????? = ?)
2314    >EQs >EQticks <instr_refl
2315    @set_arg_8_status_of_pseudo_status try %
2316    [1:
2317      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2318      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
2319      @(pose … (set_clock ????)) #status #status_refl
2320      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2321      [1:
2322        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2323        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2324      |2:
2325        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2326        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2327      ]
2328    |2:
2329      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2330      [1:
2331        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2332      |*:
2333        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2334        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2335        whd in match sfr_8051_index; normalize nodelta
2336        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2337      ]
2338    |3:
2339      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2340      [1:
2341        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2342      |2:
2343        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2344        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2345        whd in match sfr_8051_index; normalize nodelta
2346        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2347      |3:
2348        @(pose … (set_clock ????)) #status #status_refl
2349        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2350        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2351      ]
2352    ]
2353  |45: (* XCHD *)
2354    >EQP -P normalize nodelta
2355    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2356    whd in maps_assm:(??%%);
2357    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2358    [2: normalize nodelta #absurd destruct(absurd) ]
2359    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2360    [2: normalize nodelta #absurd destruct(absurd) ]
2361    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2362    whd in ⊢ (??%?);
2363    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2364    whd in ⊢ (??%?);
2365    @(pair_replace ?????????? p) normalize nodelta
2366    >EQs >EQticks <instr_refl
2367    [1:
2368      @eq_f
2369      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2370      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2371      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2372    |2:
2373      @(pair_replace ?????????? p1) normalize nodelta
2374      >EQs >EQticks <instr_refl
2375      [1:
2376        @eq_f
2377        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2378        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2379        [1:
2380          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2381          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2382        |2:
2383          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2384          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2385        ]
2386      |2:
2387        @(pair_replace ?????????? p) normalize nodelta
2388        >EQs >EQticks <instr_refl
2389        [1:
2390          %
2391        |2:
2392          @(pair_replace ?????????? p1) normalize nodelta
2393          >EQs >EQticks <instr_refl
2394          [1:
2395            %
2396          |2:
2397            @set_arg_8_status_of_pseudo_status try %
2398            [1:
2399              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2400              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2401            |2:
2402              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2403              [1:
2404                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2405              |2:
2406                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2407                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2408                whd in match sfr_8051_index; normalize nodelta
2409                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2410              ]
2411            |3:
2412              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2413              [1:
2414                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2415              |2:
2416                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2417                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2418                whd in match sfr_8051_index; normalize nodelta
2419                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2420              ]
2421            ]
2422          ]
2423        ]
2424      ]
2425    ]
2426  |46: (* RET *)
2427    >EQP -P normalize nodelta
2428    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2429    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2430    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2431    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2432    [2: normalize nodelta #absurd destruct(absurd) ]
2433    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2434    [2: normalize nodelta #absurd destruct(absurd) ]
2435    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2436    whd in ⊢ (??%?);
2437    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2438    whd in ⊢ (??%?);
2439    @(pair_replace ?????????? p) normalize nodelta
2440    >EQs >EQticks <instr_refl
2441    [1:
2442      @eq_f3 try %
2443      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2444      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2445    |2:
2446      @(pair_replace ?????????? p1) normalize nodelta
2447      >EQs >EQticks <instr_refl
2448      [1:
2449        @eq_f3 try %
2450        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2451        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2452        [1:
2453          cases daemon
2454          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2455        |2:
2456          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2457          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2458          whd in match sfr_8051_index; normalize nodelta
2459          >get_index_v_set_index_hit
2460          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2461          cases daemon
2462          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2463        ]
2464      |2:
2465        cases daemon (* XXX *)
2466      ]
2467    ]
2468  |47: (* RETI *)
2469    cases daemon
2470  |48: (* NOP *)
2471    >EQP -P normalize nodelta
2472    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2473    whd in maps_assm:(??%%);
2474    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2475    whd in ⊢ (??%?);
2476    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2477    change with (set_clock ???? = ?)
2478    @set_clock_status_of_pseudo_status %
2479  ]
2480qed.
Note: See TracBrowser for help on using the repository browser.