root/src/ASM/AssemblyProofSplit.ma

Revision 2516, 119.7 KB (checked in by mckinna, 6 months ago)

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