source: src/ASM/AssemblyProofSplit.ma @ 2273

Last change on this file since 2273 was 2273, checked in by sacerdot, 8 years ago
  1. lemmas moved from all files to Test.ma
  2. most of the lemmas in Test.ma repaired. A few are commented out. Several needs to be slightly generalized.
File size: 97.4 KB
Line 
1include "ASM/StatusProofsSplit.ma".
2
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5include alias "ASM/BitVectorTrie.ma".
6
7lemma fetch_many_singleton:
8  ∀code_memory: BitVectorTrie Byte 16.
9  ∀final_pc, start_pc: Word.
10  ∀i: instruction.
11    fetch_many code_memory final_pc start_pc [i] →
12      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
13start_pc.
14  #code_memory #final_pc #start_pc #i * #new_pc
15  #fetch_many_assm whd in fetch_many_assm;
16  cases (eq_bv_eq … fetch_many_assm) assumption
17qed.
18
19include alias "ASM/Vector.ma".
20include "ASM/Test.ma".
21
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 main_lemma_preinstruction:
59  ∀M, M': internal_pseudo_address_map.
60  ∀preamble: preamble.
61  ∀instr_list: list labelled_instruction.
62  ∀cm: pseudo_assembly_program.
63  ∀EQcm: cm = 〈preamble, instr_list〉.
64  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
65  ∀sigma: Word → Word.
66  ∀policy: Word → bool.
67  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
68  ∀ps: PseudoStatus cm.
69  ∀ppc: Word.
70  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
71  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
72  ∀labels: label_map.
73  ∀costs: BitVectorTrie costlabel 16.
74  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
75  ∀newppc: Word.
76  ∀lookup_labels: Identifier → Word.
77  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
78  ∀lookup_datalabels: Identifier → Word.
79  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
80  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
81  ∀instr: preinstruction Identifier.
82  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
83  ∀ticks: nat × nat.
84  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
85  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
86  ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
87  ∀s: PreStatus pseudo_assembly_program cm.
88  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
89  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
90  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
91              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
92                  lookup_datalabels (Instruction instr)))) →
93              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
94                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))
95                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
96                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
97                      status_of_pseudo_status M' cm s sigma policy).
98    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
99  (* XXX: takes about 45 minutes to type check! *)
100  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
101  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
102  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
103  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
104  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
105  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
106  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
107  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
108  [2: * // ]
109  @(
110  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
111  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
112  match instr in preinstruction return λx. x = instr → Σs'.? with
113        [ ADD addr1 addr2 ⇒ λinstr_refl.
114            let s ≝ add_ticks1 s in
115            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
116                                                   (get_arg_8 … s false addr2) false in
117            let cy_flag ≝ get_index' ? O ? flags in
118            let ac_flag ≝ get_index' ? 1 ? flags in
119            let ov_flag ≝ get_index' ? 2 ? flags in
120            let s ≝ set_arg_8 … s ACC_A result in
121              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
122        | ADDC addr1 addr2 ⇒ λinstr_refl.
123            let s ≝ add_ticks1 s in
124            let old_cy_flag ≝ get_cy_flag ?? s in
125            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
126                                                   (get_arg_8 … s false addr2) old_cy_flag in
127            let cy_flag ≝ get_index' ? O ? flags in
128            let ac_flag ≝ get_index' ? 1 ? flags in
129            let ov_flag ≝ get_index' ? 2 ? flags in
130            let s ≝ set_arg_8 … s ACC_A result in
131              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
132        | SUBB addr1 addr2 ⇒ λinstr_refl.
133            let s ≝ add_ticks1 s in
134            let old_cy_flag ≝ get_cy_flag ?? s in
135            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
136                                                   (get_arg_8 … s false addr2) old_cy_flag in
137            let cy_flag ≝ get_index' ? O ? flags in
138            let ac_flag ≝ get_index' ? 1 ? flags in
139            let ov_flag ≝ get_index' ? 2 ? flags in
140            let s ≝ set_arg_8 … s ACC_A result in
141              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
142        | ANL addr ⇒ λinstr_refl.
143          let s ≝ add_ticks1 s in
144          match addr with
145            [ inl l ⇒
146              match l with
147                [ inl l' ⇒
148                  let 〈addr1, addr2〉 ≝ l' in
149                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
150                    set_arg_8 … s addr1 and_val
151                | inr r ⇒
152                  let 〈addr1, addr2〉 ≝ r in
153                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
154                    set_arg_8 … s addr1 and_val
155                ]
156            | inr r ⇒
157              let 〈addr1, addr2〉 ≝ r in
158              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
159               set_flags … s and_val (None ?) (get_ov_flag ?? s)
160            ]
161        | ORL addr ⇒ λinstr_refl.
162          let s ≝ add_ticks1 s in
163          match addr with
164            [ inl l ⇒
165              match l with
166                [ inl l' ⇒
167                  let 〈addr1, addr2〉 ≝ l' in
168                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
169                    set_arg_8 … s addr1 or_val
170                | inr r ⇒
171                  let 〈addr1, addr2〉 ≝ r in
172                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
173                    set_arg_8 … s addr1 or_val
174                ]
175            | inr r ⇒
176              let 〈addr1, addr2〉 ≝ r in
177              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
178               set_flags … s or_val (None ?) (get_ov_flag … s)
179            ]
180        | XRL addr ⇒ λinstr_refl.
181          let s ≝ add_ticks1 s in
182          match addr with
183            [ inl l' ⇒
184              let 〈addr1, addr2〉 ≝ l' in
185              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
186                set_arg_8 … s addr1 xor_val
187            | inr r ⇒
188              let 〈addr1, addr2〉 ≝ r in
189              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
190                set_arg_8 … s addr1 xor_val
191            ]
192        | INC addr ⇒ λinstr_refl.
193            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
194              [ ACC_A ⇒ λacc_a: True. λEQaddr.
195                let s' ≝ add_ticks1 s in
196                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
197                 set_arg_8 … s' ACC_A result
198              | REGISTER r ⇒ λregister: True. λEQaddr.
199                let s' ≝ add_ticks1 s in
200                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
201                 set_arg_8 … s' (REGISTER r) result
202              | DIRECT d ⇒ λdirect: True. λEQaddr.
203                let s' ≝ add_ticks1 s in
204                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
205                 set_arg_8 … s' (DIRECT d) result
206              | INDIRECT i ⇒ λindirect: True. λEQaddr.
207                let s' ≝ add_ticks1 s in
208                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
209                 set_arg_8 … s' (INDIRECT i) result
210              | DPTR ⇒ λdptr: True. λEQaddr.
211                let s' ≝ add_ticks1 s in
212                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
213                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
214                let s ≝ set_8051_sfr … s' SFR_DPL bl in
215                 set_8051_sfr … s' SFR_DPH bu
216              | _ ⇒ λother: False. ⊥
217              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
218        | NOP ⇒ λinstr_refl.
219           let s ≝ add_ticks2 s in
220            s
221        | DEC addr ⇒ λinstr_refl.
222           let s ≝ add_ticks1 s in
223           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
224             set_arg_8 … s addr result
225        | MUL addr1 addr2 ⇒ λinstr_refl.
226           let s ≝ add_ticks1 s in
227           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
228           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
229           let product ≝ acc_a_nat * acc_b_nat in
230           let ov_flag ≝ product ≥ 256 in
231           let low ≝ bitvector_of_nat 8 (product mod 256) in
232           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
233           let s ≝ set_8051_sfr … s SFR_ACC_A low in
234             set_8051_sfr … s SFR_ACC_B high
235        | DIV addr1 addr2 ⇒ λinstr_refl.
236           let s ≝ add_ticks1 s in
237           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
238           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
239             match acc_b_nat with
240               [ O ⇒ set_flags … s false (None Bit) true
241               | S o ⇒
242                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
243                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
244                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
245                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
246                   set_flags … s false (None Bit) false
247               ]
248        | DA addr ⇒ λinstr_refl.
249            let s ≝ add_ticks1 s in
250            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
251              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
252                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
253                let cy_flag ≝ get_index' ? O ? flags in
254                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
255                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
256                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
257                    let new_acc ≝ nu @@ acc_nl' in
258                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
259                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
260                  else
261                    s
262              else
263                s
264        | CLR addr ⇒ λinstr_refl.
265          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
266            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
267              let s ≝ add_ticks1 s in
268               set_arg_8 … s ACC_A (zero 8)
269            | CARRY ⇒ λcarry: True.  λEQaddr.
270              let s ≝ add_ticks1 s in
271               set_arg_1 … s CARRY false
272            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
273              let s ≝ add_ticks1 s in
274               set_arg_1 … s (BIT_ADDR b) false
275            | _ ⇒ λother: False. ⊥
276            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
277        | CPL addr ⇒ λinstr_refl.
278          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
279            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
280                let s ≝ add_ticks1 s in
281                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
282                let new_acc ≝ negation_bv ? old_acc in
283                 set_8051_sfr … s SFR_ACC_A new_acc
284            | CARRY ⇒ λcarry: True. λEQaddr.
285                let s ≝ add_ticks1 s in
286                let old_cy_flag ≝ get_arg_1 … s CARRY true in
287                let new_cy_flag ≝ ¬old_cy_flag in
288                 set_arg_1 … s CARRY new_cy_flag
289            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
290                let s ≝ add_ticks1 s in
291                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
292                let new_bit ≝ ¬old_bit in
293                 set_arg_1 … s (BIT_ADDR b) new_bit
294            | _ ⇒ λother: False. ?
295            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
296        | SETB b ⇒ λinstr_refl.
297            let s ≝ add_ticks1 s in
298            set_arg_1 … s b false
299        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
300            let s ≝ add_ticks1 s in
301            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
302            let new_acc ≝ rotate_left … 1 old_acc in
303              set_8051_sfr … s SFR_ACC_A new_acc
304        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
305            let s ≝ add_ticks1 s in
306            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
307            let new_acc ≝ rotate_right … 1 old_acc in
308              set_8051_sfr … s SFR_ACC_A new_acc
309        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
310            let s ≝ add_ticks1 s in
311            let old_cy_flag ≝ get_cy_flag ?? s in
312            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
313            let new_cy_flag ≝ get_index' ? O ? old_acc in
314            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
315            let s ≝ set_arg_1 … s CARRY new_cy_flag in
316              set_8051_sfr … s SFR_ACC_A new_acc
317        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
318            let s ≝ add_ticks1 s in
319            let old_cy_flag ≝ get_cy_flag ?? s in
320            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
321            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
322            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
323            let s ≝ set_arg_1 … s CARRY new_cy_flag in
324              set_8051_sfr … s SFR_ACC_A new_acc
325        | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *)
326            let s ≝ add_ticks1 s in
327            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
328            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
329            let new_acc ≝ nl @@ nu in
330              set_8051_sfr … s SFR_ACC_A new_acc
331        | PUSH addr ⇒ λinstr_refl.
332            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with
333              [ DIRECT d ⇒ λdirect: True. λEQaddr.
334                let s ≝ add_ticks1 s in
335                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
336                let s ≝ set_8051_sfr … s SFR_SP new_sp in
337                  write_at_stack_pointer … s d
338              | _ ⇒ λother: False. ⊥
339              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
340        | POP addr ⇒ λinstr_refl.
341            let s ≝ add_ticks1 s in
342            let contents ≝ read_at_stack_pointer ?? s in
343            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
344            let s ≝ set_8051_sfr … s SFR_SP new_sp in
345              set_arg_8 … s addr contents
346        | XCH addr1 addr2 ⇒ λinstr_refl.
347            let s ≝ add_ticks1 s in
348            let old_addr ≝ get_arg_8 … s false addr2 in
349            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
350            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
351              set_arg_8 … s addr2 old_acc
352        | XCHD addr1 addr2 ⇒ λinstr_refl.
353            let s ≝ add_ticks1 s in
354            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
355            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
356            let new_acc ≝ acc_nu @@ arg_nl in
357            let new_arg ≝ arg_nu @@ acc_nl in
358            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
359              set_arg_8 … s addr2 new_arg
360        | RET ⇒ λinstr_refl.
361            let s ≝ add_ticks1 s in
362            let high_bits ≝ read_at_stack_pointer ?? s in
363            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
364            let s ≝ set_8051_sfr … s SFR_SP new_sp in
365            let low_bits ≝ read_at_stack_pointer ?? s in
366            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
367            let s ≝ set_8051_sfr … s SFR_SP new_sp in
368            let new_pc ≝ high_bits @@ low_bits in
369              set_program_counter … s new_pc
370        | RETI ⇒ λinstr_refl.
371            let s ≝ add_ticks1 s in
372            let high_bits ≝ read_at_stack_pointer ?? s in
373            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
374            let s ≝ set_8051_sfr … s SFR_SP new_sp in
375            let low_bits ≝ read_at_stack_pointer ?? s in
376            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
377            let s ≝ set_8051_sfr … s SFR_SP new_sp in
378            let new_pc ≝ high_bits @@ low_bits in
379              set_program_counter … s new_pc
380        | MOVX addr ⇒ λinstr_refl.
381          let s ≝ add_ticks1 s in
382          (* DPM: only copies --- doesn't affect I/O *)
383          match addr with
384            [ inl l ⇒
385              let 〈addr1, addr2〉 ≝ l in
386                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
387            | inr r ⇒
388              let 〈addr1, addr2〉 ≝ r in
389                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
390            ]
391        | MOV addr ⇒ λinstr_refl.
392          let s ≝ add_ticks1 s in
393          match addr with
394            [ inl l ⇒
395              match l with
396                [ inl l' ⇒
397                  match l' with
398                    [ inl l'' ⇒
399                      match l'' with
400                        [ inl l''' ⇒
401                          match l''' with
402                            [ inl l'''' ⇒
403                              let 〈addr1, addr2〉 ≝ l'''' in
404                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
405                            | inr r'''' ⇒
406                              let 〈addr1, addr2〉 ≝ r'''' in
407                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
408                            ]
409                        | inr r''' ⇒
410                          let 〈addr1, addr2〉 ≝ r''' in
411                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
412                        ]
413                    | inr r'' ⇒
414                      let 〈addr1, addr2〉 ≝ r'' in
415                       set_arg_16 … s (get_arg_16 … s addr2) addr1
416                    ]
417                | inr r ⇒
418                  let 〈addr1, addr2〉 ≝ r in
419                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
420                ]
421            | inr r ⇒
422              let 〈addr1, addr2〉 ≝ r in
423               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
424            ]
425          | JC addr ⇒ λinstr_refl.
426                  if get_cy_flag ?? s then
427                    let s ≝ add_ticks1 s in
428                      set_program_counter … s (addr_of addr s)
429                  else
430                    let s ≝ add_ticks2 s in
431                      s
432            | JNC addr ⇒ λinstr_refl.
433                  if ¬(get_cy_flag ?? s) then
434                   let s ≝ add_ticks1 s in
435                     set_program_counter … s (addr_of addr s)
436                  else
437                   let s ≝ add_ticks2 s in
438                    s
439            | JB addr1 addr2 ⇒ λinstr_refl.
440                  if get_arg_1 … s addr1 false then
441                   let s ≝ add_ticks1 s in
442                    set_program_counter … s (addr_of addr2 s)
443                  else
444                   let s ≝ add_ticks2 s in
445                    s
446            | JNB addr1 addr2 ⇒ λinstr_refl.
447                  if ¬(get_arg_1 … s addr1 false) then
448                   let s ≝ add_ticks1 s in
449                    set_program_counter … s (addr_of addr2 s)
450                  else
451                   let s ≝ add_ticks2 s in
452                    s
453            | JBC addr1 addr2 ⇒ λinstr_refl.
454                  let s ≝ set_arg_1 … s addr1 false in
455                    if get_arg_1 … s addr1 false then
456                     let s ≝ add_ticks1 s in
457                      set_program_counter … s (addr_of addr2 s)
458                    else
459                     let s ≝ add_ticks2 s in
460                      s
461            | JZ addr ⇒ λinstr_refl.
462                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
463                     let s ≝ add_ticks1 s in
464                      set_program_counter … s (addr_of addr s)
465                    else
466                     let s ≝ add_ticks2 s in
467                      s
468            | JNZ addr ⇒ λinstr_refl.
469                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
470                     let s ≝ add_ticks1 s in
471                      set_program_counter … s (addr_of addr s)
472                    else
473                     let s ≝ add_ticks2 s in
474                      s
475            | CJNE addr1 addr2 ⇒ λinstr_refl.
476                  match addr1 with
477                    [ inl l ⇒
478                        let 〈addr1, addr2'〉 ≝ l in
479                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
480                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
481                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
482                            let s ≝ add_ticks1 s in
483                            let s ≝ set_program_counter … s (addr_of addr2 s) in
484                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
485                          else
486                            let s ≝ add_ticks2 s in
487                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
488                    | inr r' ⇒
489                        let 〈addr1, addr2'〉 ≝ r' in
490                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
491                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
492                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
493                            let s ≝ add_ticks1 s in
494                            let s ≝ set_program_counter … s (addr_of addr2 s) in
495                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
496                          else
497                            let s ≝ add_ticks2 s in
498                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
499                    ]
500            | DJNZ addr1 addr2 ⇒ λinstr_refl.
501              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
502              let s ≝ set_arg_8 … s addr1 result in
503                if ¬(eq_bv ? result (zero 8)) then
504                 let s ≝ add_ticks1 s in
505                  set_program_counter … s (addr_of addr2 s)
506                else
507                 let s ≝ add_ticks2 s in
508                  s
509           ] (refl … instr))
510  try cases other
511  try assumption (*20s*)
512  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
513  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
514  whd in match execute_1_preinstruction; normalize nodelta
515  [(*1,2: (* ADD and ADDC *)
516    (* XXX: work on the right hand side *)
517    (* XXX: switch to the left hand side *)
518    >EQP -P normalize nodelta
519    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
520    whd in maps_assm:(??%%);
521    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
522    [2,4: normalize nodelta #absurd destruct(absurd) ]
523    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
524    [2,4: normalize nodelta #absurd destruct(absurd) ]
525    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
526    whd in ⊢ (??%?);
527    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
528    whd in ⊢ (??%?);
529    normalize nodelta >EQs >EQticks <instr_refl
530    @let_pair_in_status_of_pseudo_status
531    [1,3:
532      @eq_f3
533      [1,2,4,5:
534        @(pose … (set_clock ????)) #status #status_refl
535        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
536        [1,5:
537          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
538          @(subaddressing_mode_elim … addr1) %
539        |3,7:
540          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
541          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
542        |2,6:
543          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
544          @(subaddressing_mode_elim … addr1) %
545        |4,8:
546          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
547          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
548        ]
549      |3:
550        %
551      |6:
552        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
553        @sym_eq @set_clock_status_of_pseudo_status %
554      ]
555    |2,4:
556      #result #flags @sym_eq
557      @set_flags_status_of_pseudo_status try %
558      @sym_eq @set_arg_8_status_of_pseudo_status try %
559      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
560    ]
561  |3: (* SUBB *)
562    (* XXX: work on the right hand side *)
563    (* XXX: switch to the left hand side *)
564    >EQP -P normalize nodelta
565    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
566    whd in maps_assm:(??%%);
567    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
568    [2,4: normalize nodelta #absurd destruct(absurd) ]
569    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
570    [2,4: normalize nodelta #absurd destruct(absurd) ]
571    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
572    whd in ⊢ (??%?);
573    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
574    whd in ⊢ (??%?);
575    @(pair_replace ?????????? p)
576    [1:
577      @eq_f3
578      normalize nodelta >EQs >EQticks <instr_refl
579      [1:
580        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
581        @(get_arg_8_status_of_pseudo_status cm status … M')
582        [1:
583          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
584        |2:
585          >status_refl
586          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
587          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
588        |3:
589          >status_refl
590          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
591          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
592        ]
593      |2:
594        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
595        @(get_arg_8_status_of_pseudo_status cm status … M')
596        [1:
597          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
598        |2:
599          >status_refl
600          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
601          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
602        |3:
603          >status_refl
604          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
605          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
606        ]
607      |3:
608        @(get_cy_flag_status_of_pseudo_status … M')
609        @sym_eq @set_clock_status_of_pseudo_status
610        [1:
611          @sym_eq @set_program_counter_status_of_pseudo_status %
612        |2:
613          %
614        ]
615      ]
616    |2:
617      normalize nodelta
618      @(pair_replace ?????????? p)
619      [1:
620        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
621      |2:
622        @set_flags_status_of_pseudo_status try %
623        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
624        [1:
625          @sym_eq @set_clock_status_of_pseudo_status %
626        |2:
627          @I
628        |3:
629          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
630          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
631        ]
632      ]
633    ]
634  |4: (* INC *)
635    (* XXX: work on the right hand side *)
636    (* XXX: switch to the left hand side *)
637    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
638    @(subaddressing_mode_elim … addr) normalize nodelta
639    [1:
640      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
641      whd in maps_assm:(??%%);
642      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
643      [2: normalize nodelta #absurd destruct(absurd) ]
644      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
645      whd in ⊢ (??%?);
646      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
647      whd in ⊢ (??%?);
648      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
649      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
650      [1:
651        @eq_f2 try %
652        @(pose … (set_clock ????)) #status #status_refl
653        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
654        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
655      |2:
656        @set_arg_8_status_of_pseudo_status try %
657        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
658      ]
659    |2:
660      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
661      whd in maps_assm:(??%%);
662      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
663      [2: normalize nodelta #absurd destruct(absurd) ]
664      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
665      whd in ⊢ (??%?);
666      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
667      whd in ⊢ (??%?);
668      @let_pair_in_status_of_pseudo_status
669      [1:
670        @eq_f2 try %
671        @(pose … (set_clock ????)) #status #status_refl
672        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
673        >EQs >EQticks
674        [1:
675          @sym_eq @set_clock_status_of_pseudo_status %
676        |2:
677          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
678        |3:
679          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
680        ]
681      |2:
682        #carry #result
683        @sym_eq @set_arg_8_status_of_pseudo_status try %
684        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
685      ]
686    |3:
687      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
688      whd in maps_assm:(??%%);
689      inversion (addressing_mode_ok ?????) 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      whd in ⊢ (??%?);
695      @let_pair_in_status_of_pseudo_status
696      [1:
697        @eq_f2 try %
698        @(pose … (set_clock ????)) #status #status_refl
699        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
700        >EQs >EQticks
701        [1:
702          @sym_eq @set_clock_status_of_pseudo_status %
703        |2:
704          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
705        |3:
706          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
707        ]
708      |2:
709        #carry #result
710        @sym_eq @set_arg_8_status_of_pseudo_status try %
711        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
712      ]
713    |4:
714      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
715      whd in maps_assm:(??%%);
716      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
717      [2: normalize nodelta #absurd destruct(absurd) ]
718      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
719      whd in ⊢ (??%?);
720      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
721      whd in ⊢ (??%?);
722      @let_pair_in_status_of_pseudo_status
723      [1:
724        @eq_f2 try %
725        @(pose … (set_clock ????)) #status #status_refl
726        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
727        >EQs >EQticks
728        [1:
729          @sym_eq @set_clock_status_of_pseudo_status %
730        |2:
731          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
732        |3:
733          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
734        ]
735      |2:
736        #carry #result
737        @sym_eq @set_arg_8_status_of_pseudo_status try %
738        [1:
739          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
740        |2:
741          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
742        ]
743      ]
744    |5:
745      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
746      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
747      whd in ⊢ (??%?);
748      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
749      whd in ⊢ (??%?);
750      @let_pair_in_status_of_pseudo_status
751      [1:
752        @eq_f2 try %
753        @(pose … (set_clock ????)) #status #status_refl
754        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
755        >EQs >EQticks %
756      |2:
757        #carry #bl
758        @sym_eq @let_pair_in_status_of_pseudo_status
759        [1:
760          @eq_f3 try %
761          @(pose … (set_clock ????)) #status #status_refl
762          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
763          >EQs >EQticks %
764        |2:
765          #carry' #bu
766          @sym_eq @set_8051_sfr_status_of_pseudo_status %
767        ]
768      ]
769    ]
770  |5: (* DEC *)
771    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
772    @(subaddressing_mode_elim … addr) normalize nodelta
773    [1:
774      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
775      whd in maps_assm:(??%%);
776      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
777      [2: normalize nodelta #absurd destruct(absurd) ]
778      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
779      whd in ⊢ (??%?);
780      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
781      whd in ⊢ (??%?);
782      @let_pair_in_status_of_pseudo_status
783      [1:
784        @eq_f3 try %
785        @(pose … (set_clock ????)) #status #status_refl
786        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
787        >EQs >EQticks try %
788        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
789      |2:
790        #result #flags
791        @sym_eq @set_arg_8_status_of_pseudo_status try %
792        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
793      ]
794    |2:
795      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
796      whd in maps_assm:(??%%);
797      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
798      [2: normalize nodelta #absurd destruct(absurd) ]
799      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
800      whd in ⊢ (??%?);
801      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
802      whd in ⊢ (??%?);
803      @let_pair_in_status_of_pseudo_status
804      [1:
805        @eq_f3 try %
806        @(pose … (set_clock ????)) #status #status_refl
807        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
808        >EQs >EQticks try %
809        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
810      |2:
811        #result #flags
812        @sym_eq @set_arg_8_status_of_pseudo_status try %
813        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
814      ]
815    |3:
816      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
817      whd in maps_assm:(??%%);
818      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
819      [2: normalize nodelta #absurd destruct(absurd) ]
820      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
821      whd in ⊢ (??%?);
822      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
823      whd in ⊢ (??%?);
824      @let_pair_in_status_of_pseudo_status
825      [1:
826        @eq_f3 try %
827        @(pose … (set_clock ????)) #status #status_refl
828        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
829        >EQs >EQticks try %
830        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
831      |2:
832        #result #flags
833        @sym_eq @set_arg_8_status_of_pseudo_status try %
834        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
835      ]
836    |4:
837      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
838      whd in maps_assm:(??%%);
839      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
840      [2: normalize nodelta #absurd destruct(absurd) ]
841      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
842      whd in ⊢ (??%?);
843      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
844      whd in ⊢ (??%?);
845      @let_pair_in_status_of_pseudo_status
846      [1:
847        @eq_f3 try %
848        @(pose … (set_clock ????)) #status #status_refl
849        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
850        >EQs >EQticks try %
851        [1:
852          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
853        |2:
854          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
855        ]
856      |2:
857        #result #flags
858        @sym_eq @set_arg_8_status_of_pseudo_status try %
859        [1:
860          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
861        |2:
862          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
863        ]
864      ]
865    ]
866  |6: (* MUL *)
867    (* XXX: work on the right hand side *)
868    (* XXX: switch to the left hand side *)
869    >EQP -P normalize nodelta
870    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
871    whd in maps_assm:(??%%);
872    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
873    [2: normalize nodelta #absurd destruct(absurd) ]
874    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
875    [2: normalize nodelta #absurd destruct(absurd) ]
876    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
877    whd in ⊢ (??%?);
878    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
879    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
880    [2:
881      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
882      @sym_eq
883      [1:
884        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
885        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
886        %
887      |2:
888        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
889      ]
890    ]
891    @sym_eq @set_8051_sfr_status_of_pseudo_status
892    [2:
893      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
894      @eq_f @eq_f2 try % @eq_f2 @eq_f
895      @sym_eq
896      [1:
897        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
898        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
899      |2:
900        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
901      ]
902    ]
903    @sym_eq @set_clock_status_of_pseudo_status
904    [2:
905      @eq_f %
906    ]
907    @sym_eq @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 (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
915    [2,4: normalize nodelta #absurd destruct(absurd) ]
916    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
917    [2,4: normalize nodelta #absurd destruct(absurd) ]
918    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
919    whd in ⊢ (??%?);
920    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
921    whd in ⊢ (??%?); normalize nodelta
922    @(match_nat_status_of_pseudo_status M' cm sigma policy)
923    [1,4:
924      @eq_f
925      @sym_eq @(pose … (set_clock ????)) #status #status_refl
926      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
927    |2,5:
928      @sym_eq @set_flags_status_of_pseudo_status %
929    |3,6:
930      #n @sym_eq @set_flags_status_of_pseudo_status try %
931      @sym_eq @set_8051_sfr_status_of_pseudo_status
932      [1,3:
933        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
934        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
935        @eq_f @eq_f2 try % @eq_f
936        @(pose … (set_clock ????)) #status #status_refl
937        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
938        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
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 … M' … status) >status_refl -status_refl try %
943        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
944      ]
945    ]
946  |9: (* DA *)
947    (* XXX: work on the right hand side *)
948    (* XXX: switch to the left hand side *)
949    >EQP -P normalize nodelta
950    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
951    whd in maps_assm:(??%%);
952    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
953    [2: normalize nodelta #absurd destruct(absurd) ]
954    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
955    whd in ⊢ (??%?);
956    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
957    whd in ⊢ (??%?); normalize nodelta
958    @(pair_replace ?????????? p)
959    [1:
960      @eq_f normalize nodelta >EQs >EQticks <instr_refl
961      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
962      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
963    |2:
964      @(pair_replace ?????????? p)
965      [1:
966        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
967      |2:
968        @(if_then_else_replace ???????? p1) normalize nodelta
969        [1:
970          cases (gtb ? 9)
971          [1:
972            %
973          |2:
974            change with (get_ac_flag ??? = get_ac_flag ???)
975            @(get_ac_flag_status_of_pseudo_status M')
976            @sym_eq @set_clock_status_of_pseudo_status
977            >EQs >EQticks <instr_refl %
978          ]
979        |2:
980          @(if_then_else_replace ???????? p1) normalize nodelta try %
981          @(pair_replace ?????????? p2)
982          [1:
983            @eq_f3 try % normalize nodelta
984            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
985            whd in ⊢ (??%?);
986            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
987          |2:
988            @(pair_replace ?????????? p2) try %
989            @(pair_replace ?????????? p3) try %
990            @(pair_replace ?????????? p3) try %
991            @(if_then_else_replace ???????? p4) try % normalize nodelta
992            @(if_then_else_replace ???????? p4) try % normalize nodelta
993            @(pair_replace ?????????? p5) try %
994            @(pair_replace ?????????? p5) try %
995            @set_flags_status_of_pseudo_status try %
996            [1:
997              @eq_f @(get_ac_flag_status_of_pseudo_status M')
998              @sym_eq @set_8051_sfr_status_of_pseudo_status
999              [1:
1000                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1001              |2:
1002                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1003              ]
1004            |2:
1005              @(get_ov_flag_status_of_pseudo_status M')
1006              @sym_eq @set_8051_sfr_status_of_pseudo_status
1007              [1:
1008                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1009              |2:
1010                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1011              ]
1012            |3:
1013              @sym_eq @set_8051_sfr_status_of_pseudo_status
1014              [1:
1015                @sym_eq @set_clock_status_of_pseudo_status
1016                [1:
1017                  >EQs
1018                  @sym_eq @set_program_counter_status_of_pseudo_status %
1019                |2:
1020                  >EQs >EQticks <instr_refl %
1021                ]
1022              |2:
1023                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1024              ]
1025            ]
1026          ]
1027        ]
1028      ]
1029    ]
1030  |10: (* DA *)
1031    (* XXX: work on the right hand side *)
1032    (* XXX: switch to the left hand side *)
1033    >EQP -P normalize nodelta
1034    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1035    whd in maps_assm:(??%%);
1036    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1037    [2: normalize nodelta #absurd destruct(absurd) ]
1038    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1039    whd in ⊢ (??%?);
1040    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1041    whd in ⊢ (??%?); normalize nodelta
1042    @(pair_replace ?????????? p)
1043    [1:
1044      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1045      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1046      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1047    |2:
1048      @(pair_replace ?????????? p)
1049      [1:
1050        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1051      |2:
1052        @(if_then_else_replace ???????? p1) normalize nodelta
1053        [1:
1054          cases (gtb ? 9)
1055          [1:
1056            %
1057          |2:
1058            change with (get_ac_flag ??? = get_ac_flag ???)
1059            @(get_ac_flag_status_of_pseudo_status M')
1060            @sym_eq @set_clock_status_of_pseudo_status
1061            >EQs >EQticks <instr_refl %
1062          ]
1063        |2:
1064          @(if_then_else_replace ???????? p1) normalize nodelta try %
1065          @(pair_replace ?????????? p2)
1066          [1:
1067            @eq_f3 try % normalize nodelta
1068            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1069            whd in ⊢ (??%?);
1070            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1071          |2:
1072            @(pair_replace ?????????? p2) try %
1073            @(pair_replace ?????????? p3) try %
1074            @(pair_replace ?????????? p3) try %
1075            @(if_then_else_replace ???????? p4) try % normalize nodelta
1076            @(if_then_else_replace ???????? p4) try % normalize nodelta
1077            @set_clock_status_of_pseudo_status
1078            [1:
1079              >EQs
1080              @sym_eq @set_program_counter_status_of_pseudo_status %
1081            |2:
1082              >EQs >EQticks <instr_refl %
1083            ]
1084          ]
1085        ]
1086      ]
1087    ]
1088  |11: (* DA *)
1089    (* XXX: work on the right hand side *)
1090    (* XXX: switch to the left hand side *)
1091    >EQP -P normalize nodelta
1092    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1093    whd in maps_assm:(??%%);
1094    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1095    [2: normalize nodelta #absurd destruct(absurd) ]
1096    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1097    whd in ⊢ (??%?);
1098    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1099    whd in ⊢ (??%?); normalize nodelta
1100    @(pair_replace ?????????? p)
1101    [1:
1102      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1103      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1104      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1105    |2:
1106      @(pair_replace ?????????? p)
1107      [1:
1108        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1109      |2:
1110        @(if_then_else_replace ???????? p1) normalize nodelta
1111        [1:
1112          cases (gtb ? 9)
1113          [1:
1114            %
1115          |2:
1116            change with (get_ac_flag ??? = get_ac_flag ???)
1117            @(get_ac_flag_status_of_pseudo_status M')
1118            @sym_eq @set_clock_status_of_pseudo_status
1119            >EQs >EQticks <instr_refl %
1120          ]
1121        |2:
1122          @(if_then_else_replace ???????? p1) normalize nodelta try %
1123          @set_clock_status_of_pseudo_status
1124          [1:
1125            >EQs
1126            @sym_eq @set_program_counter_status_of_pseudo_status %
1127          |2:
1128            >EQs >EQticks <instr_refl %
1129          ]
1130        ]
1131      ]
1132    ]
1133  |*)12: (* JC *)
1134    >EQP -P normalize nodelta
1135    whd in match expand_pseudo_instruction; normalize nodelta
1136    whd in match expand_relative_jump; normalize nodelta
1137    whd in match expand_relative_jump_internal; normalize nodelta
1138    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1139    inversion sj_possible #sj_possible_refl normalize nodelta
1140    [1:
1141      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1142      whd in maps_assm:(??%%);
1143      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1144      whd in ⊢ (??%?); normalize nodelta
1145      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1146      whd in ⊢ (??%?);
1147      @if_then_else_status_of_pseudo_status
1148      >EQs >EQticks <instr_refl normalize nodelta
1149      [1:
1150        @(get_cy_flag_status_of_pseudo_status M') %
1151      |2:
1152        @sym_eq @set_program_counter_status_of_pseudo_status
1153        [1:
1154        |2:
1155          @sym_eq @set_clock_status_of_pseudo_status try %
1156          whd in match ticks_of0; normalize nodelta
1157          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1158          [1:
1159            @eq_f2 try %
1160            >sigma_increment_commutation
1161            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
1162            * #sigma_zero_assm #relevant cases (relevant ppc ?)
1163            [1:
1164              -relevant
1165              [2:
1166                >EQcm assumption
1167              |1:
1168                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
1169                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
1170              ]
1171            |2:
1172            ]
1173          |2:
1174            >sj_possible_refl %
1175          ]
1176        ]
1177      |3:
1178      ]
1179    ]
1180    cases daemon
1181  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
1182    cases daemon
1183  |(*29,30: (* ANL and ORL *)
1184    inversion addr
1185    [1,3:
1186      *
1187      [1,3:
1188        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1189        >EQP -P normalize nodelta
1190        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1191        whd in maps_assm:(??%%);
1192        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1193        [2,4: normalize nodelta #absurd destruct(absurd) ]
1194        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1195        [2,4: normalize nodelta #absurd destruct(absurd) ]
1196        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1197        whd in ⊢ (??%?);
1198        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1199        change with (set_arg_8 ????? = ?)
1200        @set_arg_8_status_of_pseudo_status try %
1201        >EQs >EQticks <instr_refl >addr_refl
1202        [1,4:
1203          @sym_eq @set_clock_status_of_pseudo_status
1204          [1,3:
1205            @sym_eq @set_program_counter_status_of_pseudo_status %
1206          |2,4:
1207            @eq_f2 %
1208          ]
1209        |2,5:
1210          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1211          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
1212        |3,6:
1213          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1214          [1,5:
1215            @(subaddressing_mode_elim … acc_a) %
1216          |4,8:
1217            @eq_f2
1218            @(pose … (set_clock ????)) #status #status_refl
1219            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1220            [1,5:
1221              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1222              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
1223            |3,7:
1224              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1225              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1226            |2,6:
1227              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1228              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
1229            |4,8:
1230              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1231              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1232            ]
1233          |*:
1234            %
1235          ]
1236        ]
1237      |2,4:
1238        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1239        >EQP -P normalize nodelta
1240        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1241        whd in maps_assm:(??%%);
1242        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1243        [2,4: normalize nodelta #absurd destruct(absurd) ]
1244        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1245        [2,4: normalize nodelta #absurd destruct(absurd) ]
1246        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1247        whd in ⊢ (??%?);
1248        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1249        change with (set_arg_8 ????? = ?)
1250        @set_arg_8_status_of_pseudo_status try %
1251        >EQs >EQticks <instr_refl >addr_refl
1252        [1,4:
1253          @sym_eq @set_clock_status_of_pseudo_status
1254          [1,3:
1255            @sym_eq @set_program_counter_status_of_pseudo_status %
1256          |2,4:
1257            @eq_f2 %
1258          ]
1259        |2,5:
1260          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1261          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
1262        |3,6:
1263          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1264          [1,5:
1265            @(subaddressing_mode_elim … direct) #w %
1266          |4,8:
1267            @eq_f2
1268            @(pose … (set_clock ????)) #status #status_refl
1269            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1270            [1,5:
1271              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1272              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
1273            |3,7:
1274              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1275              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1276            |2,6:
1277              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1278              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
1279            |4,8:
1280              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1281              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1282            ]
1283          |*:
1284            %
1285          ]
1286        ]
1287      ]
1288    |2,4:
1289      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
1290      >EQP -P normalize nodelta
1291      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1292      whd in maps_assm:(??%%);
1293      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1294      [2,4: normalize nodelta #absurd destruct(absurd) ]
1295      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1296      [2,4: normalize nodelta #absurd destruct(absurd) ]
1297      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1298      whd in ⊢ (??%?);
1299      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1300      change with (set_flags ?????? = ?)
1301      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
1302      >EQs >EQticks <instr_refl >addr_refl
1303      @sym_eq @set_clock_status_of_pseudo_status %
1304    ]
1305  |31: (* XRL *)
1306    inversion addr
1307    [1:
1308      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1309      >EQP -P normalize nodelta
1310      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1311      whd in maps_assm:(??%%);
1312      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1313      [2: normalize nodelta #absurd destruct(absurd) ]
1314      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1315      [2: normalize nodelta #absurd destruct(absurd) ]
1316      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1317      whd in ⊢ (??%?);
1318      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1319      change with (set_arg_8 ????? = ?)
1320      @set_arg_8_status_of_pseudo_status try %
1321      >EQs >EQticks <instr_refl >addr_refl
1322      [1:
1323        @sym_eq @set_clock_status_of_pseudo_status
1324        [1:
1325          @sym_eq @set_program_counter_status_of_pseudo_status %
1326        |2:
1327          @eq_f2 %
1328        ]
1329      |2:
1330        @(subaddressing_mode_elim … acc_a) @I
1331      |3:
1332        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1333        [1:
1334          @(subaddressing_mode_elim … acc_a) %
1335        |4:
1336          @eq_f2
1337          @(pose … (set_clock ????)) #status #status_refl
1338          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1339          [1:
1340            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1341            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
1342          |3:
1343            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1344            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1345          |2:
1346            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1347            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
1348          |4:
1349            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1350            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1351          ]
1352        |*:
1353          %
1354        ]
1355      ]
1356    |2:
1357      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1358      >EQP -P normalize nodelta
1359      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1360      whd in maps_assm:(??%%);
1361      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1362      [2: normalize nodelta #absurd destruct(absurd) ]
1363      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1364      [2: normalize nodelta #absurd destruct(absurd) ]
1365      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1366      whd in ⊢ (??%?);
1367      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1368      change with (set_arg_8 ????? = ?)
1369      @set_arg_8_status_of_pseudo_status try %
1370      >EQs >EQticks <instr_refl >addr_refl
1371      [1:
1372        @sym_eq @set_clock_status_of_pseudo_status
1373        [1:
1374          @sym_eq @set_program_counter_status_of_pseudo_status %
1375        |2:
1376          @eq_f2 %
1377        ]
1378      |2:
1379        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1380        [1: @(subaddressing_mode_elim … direct) #w % ] %
1381      |3:
1382        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1383        [1:
1384          @(subaddressing_mode_elim … direct) #w %
1385        |4:
1386          @eq_f2
1387          @(pose … (set_clock ????)) #status #status_refl
1388          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1389          [1:
1390            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1391            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
1392          |3:
1393            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1394            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1395          |2:
1396            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1397            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
1398          |4:
1399            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1400            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1401          ]
1402        |*:
1403          %
1404        ]
1405      ]
1406    ]
1407  |32: (* CLR *)
1408    >EQP -P normalize nodelta lapply instr_refl
1409    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1410    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1411    whd in maps_assm:(??%%);
1412    [1,2:
1413      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1414      [2,4: normalize nodelta #absurd destruct(absurd) ]
1415      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1416      whd in ⊢ (??%?);
1417      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1418      [1:
1419        >EQs >EQticks <instr_refl
1420        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1421        @set_arg_1_status_of_pseudo_status try %
1422        [1:
1423          @(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) %
1424        |2:
1425          @(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) %
1426        ]         
1427      |2:
1428        >EQs >EQticks <instr_refl
1429        change with (set_arg_8 ??? ACC_A ? = ?) try %
1430        @set_arg_8_status_of_pseudo_status try %
1431        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1432      ]
1433    |3:
1434      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1435      whd in ⊢ (??%?);
1436      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1437      >EQs >EQticks <instr_refl
1438      change with (set_arg_1 ??? CARRY ? = ?) try %
1439      @set_arg_1_status_of_pseudo_status %
1440    ]
1441  |33: (* CPL *)
1442    >EQP -P normalize nodelta lapply instr_refl
1443    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1444    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1445    whd in maps_assm:(??%%);
1446    [1,2:
1447      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1448      [2,4: normalize nodelta #absurd destruct(absurd) ]
1449      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1450      whd in ⊢ (??%?);
1451      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1452      [1:
1453        >EQs >EQticks <instr_refl
1454        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1455        @set_arg_1_status_of_pseudo_status
1456        [1:
1457          @eq_f
1458          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1459          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1460          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
1461        |2:
1462          %
1463        |3:
1464          @(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) %
1465        |4:
1466          @(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) %
1467        ]       
1468      |2:
1469        >EQs >EQticks <instr_refl
1470        change with (set_8051_sfr ????? = ?)
1471        @set_8051_sfr_status_of_pseudo_status try %
1472        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
1473        normalize nodelta @eq_f
1474        @(pose … (set_clock ????)) #status #status_refl
1475        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1476        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
1477      ]
1478    |3:
1479      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1480      whd in ⊢ (??%?);
1481      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1482      >EQs >EQticks <instr_refl
1483      change with (set_arg_1 ??? CARRY ? = ?) try %
1484      @set_arg_1_status_of_pseudo_status try %
1485      @eq_f
1486      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1487      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
1488    ]
1489  |34,36: (* RL and RR *)
1490    (* XXX: work on the right hand side *)
1491    (* XXX: switch to the left hand side *)
1492    >EQP -P normalize nodelta
1493    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1494    whd in maps_assm:(??%%);
1495    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1496    [2,4: normalize nodelta #absurd destruct(absurd) ]
1497    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1498    whd in ⊢ (??%?);
1499    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1500    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1501    [2,4:
1502      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1503      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1504      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1505      %
1506    ]
1507    @sym_eq @set_clock_status_of_pseudo_status
1508    [2,4:
1509      %
1510    ]
1511    @sym_eq @set_program_counter_status_of_pseudo_status %
1512  |35,37: (* RLC and RRC *)
1513    (* XXX: work on the right hand side *)
1514    (* XXX: switch to the left hand side *)
1515    >EQP -P normalize nodelta
1516    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1517    whd in maps_assm:(??%%);
1518    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1519    [2,4: normalize nodelta #absurd destruct(absurd) ]
1520    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1521    whd in ⊢ (??%?);
1522    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1523    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1524    [2,4:
1525      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1526      @eq_f2
1527      [1,3:
1528        @sym_eq
1529        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1530        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1531      |2,4:
1532        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
1533        @sym_eq @set_clock_status_of_pseudo_status %
1534      ]
1535    |1,3:
1536      @sym_eq @set_arg_1_status_of_pseudo_status try %
1537      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1538      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1539    ]
1540  |38: (* SWAP *)
1541    >EQP -P normalize nodelta
1542    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1543    whd in maps_assm:(??%%);
1544    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1545    [2: normalize nodelta #absurd destruct(absurd) ]
1546    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1547    whd in ⊢ (??%?);
1548    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1549    whd in ⊢ (??%?);
1550    @(pair_replace ?????????? p)
1551    [1:
1552      @eq_f normalize nodelta
1553      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1554      @(get_8051_sfr_status_of_pseudo_status … M' … status)
1555      [1:
1556        >status_refl -status_refl
1557        @sym_eq @set_clock_status_of_pseudo_status
1558        >EQs >EQticks <instr_refl %
1559      |2:
1560        whd in ⊢ (??%?);
1561        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1562      ]
1563    |2:
1564      @(pair_replace ?????????? p) normalize nodelta
1565      [1:
1566        %
1567      |2:
1568        @set_8051_sfr_status_of_pseudo_status
1569        [1:
1570          @sym_eq @set_clock_status_of_pseudo_status
1571          >EQs >EQticks <instr_refl %
1572        |2:
1573          whd in ⊢ (??%?);
1574          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1575        ]
1576      ]     
1577    ]
1578  |39: (* MOV *)
1579    >EQP -P normalize nodelta
1580    inversion addr
1581    [1:
1582      #addr' normalize nodelta
1583      inversion addr'
1584      [1:
1585        #addr'' normalize nodelta
1586        inversion addr''
1587        [1:
1588          #addr''' normalize nodelta
1589          inversion addr'''
1590          [1:
1591            #addr'''' normalize nodelta
1592            inversion addr''''
1593            [1:
1594              normalize nodelta #acc_a_others
1595              cases acc_a_others #acc_a #others
1596              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1597              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1598              whd in maps_assm:(??%%);
1599              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1600              [2: normalize nodelta #absurd destruct(absurd) ]
1601              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1602              [2: normalize nodelta #absurd destruct(absurd) ]
1603              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1604              whd in ⊢ (??%?);
1605              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1606              change with (set_arg_8 ????? = ?)
1607              @set_arg_8_status_of_pseudo_status try %
1608              [1:
1609                @sym_eq @set_clock_status_of_pseudo_status
1610                >EQs >EQticks <instr_refl >addr_refl %
1611              |2:
1612                @(subaddressing_mode_elim … acc_a) @I
1613              |3:
1614                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1615                [1: @(subaddressing_mode_elim … acc_a) % ]
1616                >EQs >EQticks <instr_refl >addr_refl
1617                [1,2:
1618                  %
1619                |3:
1620                  @(pose … (set_clock ????)) #status #status_refl
1621                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1622                  [1:
1623                    @sym_eq @set_clock_status_of_pseudo_status %
1624                  |2:
1625                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1626                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1627                  |3:
1628                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1629                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1630                  ]
1631                ]
1632              ]
1633            |2:
1634              #others_others' cases others_others' #others #others' normalize nodelta
1635              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1636              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1637              whd in maps_assm:(??%%);
1638              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1639              [2: normalize nodelta #absurd destruct(absurd) ]
1640              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1641              [2: normalize nodelta #absurd destruct(absurd) ]
1642              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1643              whd in ⊢ (??%?);
1644              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1645              change with (set_arg_8 ????? = ?)
1646              @set_arg_8_status_of_pseudo_status try %
1647              >EQs >EQticks <instr_refl >addr_refl try %
1648              [1:
1649                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
1650                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1651              |2:
1652                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
1653                [1:
1654                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1655                |2,3:
1656                  %
1657                |4:
1658                  @(pose … (set_clock ????)) #status #status_refl
1659                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1660                  [1:
1661                    @sym_eq @set_clock_status_of_pseudo_status %
1662                  |2:
1663                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
1664                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1665                  |3:
1666                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
1667                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1668                  ]
1669                ]
1670              ]
1671            ]
1672          |2:
1673            #direct_others cases direct_others #direct #others
1674            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1675            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1676            whd in maps_assm:(??%%);
1677            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1678            [2: normalize nodelta #absurd destruct(absurd) ]
1679            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1680            [2: 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:
1688              @sym_eq @set_clock_status_of_pseudo_status %
1689            |2:
1690              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1691              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1692            |3:
1693              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1694              [1:
1695                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1696              |2,3:
1697                %
1698              |4:
1699                @(pose … (set_clock ????)) #status #status_refl
1700                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1701                [1:
1702                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1703                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1704                |2:
1705                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1706                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1707                ]
1708              ]
1709            ]
1710          ]
1711        |2:
1712          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
1713          #addr_refl'' #addr_refl' #addr_refl
1714          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1715          whd in maps_assm:(??%%);
1716          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1717          [2: normalize nodelta #absurd destruct(absurd) ]
1718          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1719          [2: normalize nodelta #absurd destruct(absurd) ]
1720          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1721          whd in ⊢ (??%?);
1722          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1723          change with (set_arg_16 ????? = ?)
1724          @set_arg_16_status_of_pseudo_status try %
1725          >EQs >EQticks <instr_refl >addr_refl
1726          @sym_eq @set_clock_status_of_pseudo_status %
1727        ]
1728      |2:
1729        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
1730        #addr_refl' #addr_refl
1731        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1732        whd in maps_assm:(??%%);
1733        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1734        [2: normalize nodelta #absurd destruct(absurd) ]
1735        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1736        [2: normalize nodelta #absurd destruct(absurd) ]
1737        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1738        whd in ⊢ (??%?);
1739        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1740        change with (set_arg_1 ????? = ?)
1741        @set_arg_1_status_of_pseudo_status
1742        >EQs >EQticks <instr_refl >addr_refl try %
1743        [1:
1744          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1745          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1746          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
1747        |2,3:
1748          @(subaddressing_mode_elim … carry) @I
1749        ]
1750      ]
1751    |2:
1752      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
1753      #addr_refl
1754      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1755      whd in maps_assm:(??%%);
1756      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1757      [2: normalize nodelta #absurd destruct(absurd) ]
1758      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1759      [2: normalize nodelta #absurd destruct(absurd) ]
1760      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1761      whd in ⊢ (??%?);
1762      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1763      change with (set_arg_1 ????? = ?)
1764      @set_arg_1_status_of_pseudo_status
1765      [1:
1766        >EQs >EQticks <instr_refl >addr_refl
1767        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1768        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1769        @(subaddressing_mode_elim … carry) @I
1770      |2:
1771        >EQs >EQticks <instr_refl >addr_refl %
1772      |3,4:
1773        @(pose … (set_clock ????)) #status #status_refl
1774        [1:
1775          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
1776        |2:
1777          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
1778        ]
1779        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
1780        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
1781        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
1782      ]
1783    ]
1784  |40: (* MOVX *)
1785    >EQP -P normalize nodelta
1786    inversion addr
1787    [1:
1788      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
1789      #addr_refl
1790      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1791      whd in maps_assm:(??%%);
1792      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1793      [2: normalize nodelta #absurd destruct(absurd) ]
1794      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1795      [2: normalize nodelta #absurd destruct(absurd) ]
1796      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1797      whd in ⊢ (??%?);
1798      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1799      change with (set_arg_8 ????? = ?)
1800      @set_arg_8_status_of_pseudo_status try %
1801      >EQs >EQticks <instr_refl >addr_refl
1802      [1:
1803        @sym_eq @set_clock_status_of_pseudo_status %
1804      |2:
1805        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1806        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1807      |3:
1808        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1809        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
1810        @(pose … (set_clock ????)) #status #status_refl
1811        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1812        [1:
1813          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1814          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1815        |2:
1816          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1817          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1818        ]
1819      ]
1820    |2:
1821      #others_acc_a cases others_acc_a #others #acc_a
1822      #addr_refl
1823      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1824      whd in maps_assm:(??%%);
1825      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1826      [2: normalize nodelta #absurd destruct(absurd) ]
1827      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1828      [2: normalize nodelta #absurd destruct(absurd) ]
1829      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1830      whd in ⊢ (??%?);
1831      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1832      change with (set_arg_8 ????? = ?)
1833      @set_arg_8_status_of_pseudo_status
1834      >EQs >EQticks <instr_refl >addr_refl try %
1835      [1:
1836        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
1837        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1838      |2:
1839        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
1840        [1:
1841          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1842        |2,3:
1843          %
1844        |4:
1845          @(pose … (set_clock ????)) #status #status_refl
1846          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1847          [1:
1848            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
1849            [1: @(subaddressing_mode_elim … acc_a) % ] %
1850          |2:
1851            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
1852            [1: @(subaddressing_mode_elim … acc_a) % ] %
1853          ]
1854        ]
1855      ]
1856    ]
1857  |41: (* SETB *)
1858    >EQs >EQticks <instr_refl
1859    >EQP -P normalize nodelta
1860    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1861    whd in maps_assm:(??%%);
1862    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1863    [2: normalize nodelta #absurd destruct(absurd) ]
1864    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1865    whd in ⊢ (??%?);
1866    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1867    change with (set_arg_1 ????? = ?)
1868    @set_arg_1_status_of_pseudo_status try %
1869    [1:
1870      @(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)
1871    |2:
1872      @(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)
1873    ]
1874  |*)42: (* PUSH *)
1875    >EQP -P normalize nodelta lapply instr_refl
1876    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
1877    #sigma_increment_commutation
1878    whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
1879    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
1880    whd in ⊢ (??%?);
1881    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1882    whd in ⊢ (??%?);
1883    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
1884    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
1885    [1:
1886      @eq_f2 try %
1887      @(pose … (set_clock ????)) #status #status_refl
1888      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
1889      @sym_eq @set_clock_status_of_pseudo_status
1890      >EQs >EQticks <instr_refl %
1891    |2:
1892      >EQs >EQticks <instr_refl
1893      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
1894    ]
1895  |43: (* POP *)
1896    cases daemon
1897  |44:
1898    >EQP -P normalize nodelta
1899    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1900    whd in maps_assm:(??%%);
1901    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1902    [2: normalize nodelta #absurd destruct(absurd) ]
1903    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1904    [2: normalize nodelta #absurd destruct(absurd) ]
1905    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1906    whd in ⊢ (??%?);
1907    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1908    change with (set_arg_8 ????? = ?)
1909    >EQs >EQticks <instr_refl
1910    @set_arg_8_status_of_pseudo_status try %
1911    [1:
1912      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
1913      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
1914      @(pose … (set_clock ????)) #status #status_refl
1915      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1916      [1:
1917        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
1918        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1919      |2:
1920        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1921        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1922      ]
1923    |2:
1924      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1925      [1:
1926        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1927      |*:
1928        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
1929        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
1930        whd in match sfr_8051_index; normalize nodelta
1931        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
1932      ]
1933    |3:
1934      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
1935      [1:
1936        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1937      |2:
1938        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
1939        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
1940        whd in match sfr_8051_index; normalize nodelta
1941        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
1942      |3:
1943        @(pose … (set_clock ????)) #status #status_refl
1944        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1945        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1946      ]
1947    ]
1948  |45: (* XCHD *)
1949    >EQP -P normalize nodelta
1950    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1951    whd in maps_assm:(??%%);
1952    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1953    [2: normalize nodelta #absurd destruct(absurd) ]
1954    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1955    [2: normalize nodelta #absurd destruct(absurd) ]
1956    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1957    whd in ⊢ (??%?);
1958    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1959    whd in ⊢ (??%?);
1960    @(pair_replace ?????????? p) normalize nodelta
1961    >EQs >EQticks <instr_refl
1962    [1:
1963      @eq_f
1964      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1965      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1966      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1967    |2:
1968      @(pair_replace ?????????? p1) normalize nodelta
1969      >EQs >EQticks <instr_refl
1970      [1:
1971        @eq_f
1972        @sym_eq @(pose … (set_clock ????)) #status #status_refl
1973        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1974        [1:
1975          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
1976          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1977        |2:
1978          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1979          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1980        ]
1981      |2:
1982        @(pair_replace ?????????? p) normalize nodelta
1983        >EQs >EQticks <instr_refl
1984        [1:
1985          %
1986        |2:
1987          @(pair_replace ?????????? p1) normalize nodelta
1988          >EQs >EQticks <instr_refl
1989          [1:
1990            %
1991          |2:
1992            @set_arg_8_status_of_pseudo_status try %
1993            [1:
1994              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
1995              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1996            |2:
1997              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1998              [1:
1999                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2000              |2:
2001                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2002                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2003                whd in match sfr_8051_index; normalize nodelta
2004                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2005              ]
2006            |3:
2007              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2008              [1:
2009                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2010              |2:
2011                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2012                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2013                whd in match sfr_8051_index; normalize nodelta
2014                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2015              ]
2016            ]
2017          ]
2018        ]
2019      ]
2020    ]
2021  |46: (* RET *)
2022    >EQP -P normalize nodelta
2023    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2024    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2025    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2026    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2027    [2: normalize nodelta #absurd destruct(absurd) ]
2028    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2029    [2: normalize nodelta #absurd destruct(absurd) ]
2030    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2031    whd in ⊢ (??%?);
2032    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2033    whd in ⊢ (??%?);
2034    @(pair_replace ?????????? p) normalize nodelta
2035    >EQs >EQticks <instr_refl
2036    [1:
2037      @eq_f3 try %
2038      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2039      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2040    |2:
2041      @(pair_replace ?????????? p1) normalize nodelta
2042      >EQs >EQticks <instr_refl
2043      [1:
2044        @eq_f3 try %
2045        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2046        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2047        [1:
2048          cases daemon
2049          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2050        |2:
2051          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2052          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2053          whd in match sfr_8051_index; normalize nodelta
2054          >get_index_v_set_index_hit
2055          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2056          cases daemon
2057          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2058        ]
2059      |2:
2060        cases daemon (* XXX *)
2061      ]
2062    ]
2063  |47: (* RETI *)
2064    cases daemon
2065  |48: (* NOP *)
2066    >EQP -P normalize nodelta
2067    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2068    whd in maps_assm:(??%%);
2069    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2070    whd in ⊢ (??%?);
2071    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2072    change with (set_clock ???? = ?)
2073    @set_clock_status_of_pseudo_status %
2074  ]
2075qed.
Note: See TracBrowser for help on using the repository browser.