source: src/ASM/AssemblyProofSplit.ma @ 2212

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

More work on the INC case

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