source: src/ASM/AssemblyProofSplit.ma @ 2278

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

Half of JC case complete

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