source: src/ASM/AssemblyProofSplit.ma @ 2276

Last change on this file since 2276 was 2276, checked in by sacerdot, 7 years ago

...

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