source: src/ASM/AssemblyProofSplit.ma @ 2209

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

Closed major daemons in the supporting lemmas of the main lemma.

File size: 94.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 → Σs': PreStatus m cm. ? 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      cases daemon (* XXX: todo *)
822    ]
823  |4,5,6,7,8,9: (* INC and DEC *)
824    cases daemon
825  |42,44: (* RL and RR *)
826    (* XXX: work on the right hand side *)
827    (* XXX: switch to the left hand side *)
828    >EQP -P normalize nodelta
829    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
830    whd in maps_assm:(??%%);
831    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
832    [2,4: normalize nodelta #absurd destruct(absurd) ]
833    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
834    whd in ⊢ (??%?);
835    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
836    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
837    [2,4:
838      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
839      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
840      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
841      %
842    ]
843    @sym_eq @set_clock_status_of_pseudo_status
844    [2,4:
845      %
846    ]
847    @sym_eq @set_program_counter_status_of_pseudo_status %
848  |43,45: (* RLC and RRC *)
849    (* XXX: work on the right hand side *)
850    (* XXX: switch to the left hand side *)
851    >EQP -P normalize nodelta
852    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
853    whd in maps_assm:(??%%);
854    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
855    [2,4: normalize nodelta #absurd destruct(absurd) ]
856    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
857    whd in ⊢ (??%?);
858    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
859    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
860    [2,4:
861      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
862      @eq_f2
863      [1,3:
864        @sym_eq
865        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
866        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
867      |2,4:
868        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
869        @sym_eq @set_clock_status_of_pseudo_status %
870      ]
871    |1,3:
872      @sym_eq @set_arg_1_status_of_pseudo_status try %
873      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
874      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
875    ]
876  |1,2: (* ADD and ADDC *)
877    (* XXX: work on the right hand side *)
878    (* XXX: switch to the left hand side *)
879    >EQP -P normalize nodelta
880    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
881    whd in maps_assm:(??%%);
882    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
883    [2,4: normalize nodelta #absurd destruct(absurd) ]
884    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
885    [2,4: normalize nodelta #absurd destruct(absurd) ]
886    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
887    whd in ⊢ (??%?);
888    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
889    whd in ⊢ (??%?);
890    normalize nodelta >EQs >EQticks <instr_refl
891    @let_pair_in_status_of_pseudo_status
892    [1,3:
893      @eq_f3
894      [1,2,4,5:
895        @(pose … (set_clock ????)) #status #status_refl
896        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
897        [1,5:
898          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
899          @(subaddressing_mode_elim … addr1) %
900        |3,7:
901          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
902          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
903        |2,6:
904          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
905          @(subaddressing_mode_elim … addr1) %
906        |4,8:
907          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
908          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
909        ]
910      |3: %
911      |6:
912        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
913        @sym_eq @set_clock_status_of_pseudo_status %
914      ]
915    |2,4:
916      #result #flags @sym_eq
917      @set_flags_status_of_pseudo_status try %
918      @sym_eq @set_arg_8_status_of_pseudo_status try %
919      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
920    ]
921  |3: (* SUB *)
922    (* XXX: work on the right hand side *)
923    (* XXX: switch to the left hand side *)
924    >EQP -P normalize nodelta
925    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
926    whd in maps_assm:(??%%);
927    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
928    [2,4: normalize nodelta #absurd destruct(absurd) ]
929    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
930    [2,4: normalize nodelta #absurd destruct(absurd) ]
931    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
932    whd in ⊢ (??%?);
933    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
934    whd in ⊢ (??%?);
935    @(pair_replace ?????????? p)
936    [1:
937      @eq_f3
938      normalize nodelta >EQs >EQticks <instr_refl
939      [1:
940        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
941        @(get_arg_8_status_of_pseudo_status cm status … M')
942        [1:
943          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
944        |2:
945          >status_refl
946          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1)
947          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
948          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
949          @(subaddressing_mode_elim … addr1)
950        |3:
951          >status_refl
952          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1)
953          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
954          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
955          @(subaddressing_mode_elim … addr1)
956        ]
957      |2:
958        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
959        @(get_arg_8_status_of_pseudo_status cm status … M')
960        [1:
961          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
962        |2:
963          >status_refl
964          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2)
965          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
966          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
967          cases daemon (* XXX: ??? *)
968        |3:
969          >status_refl
970          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2)
971          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
972          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
973          cases daemon (* XXX: ??? *)
974        ]
975      |3:
976        @(get_cy_flag_status_of_pseudo_status … M')
977        @sym_eq @set_clock_status_of_pseudo_status
978        [1:
979          @sym_eq @set_program_counter_status_of_pseudo_status %
980        |2:
981          %
982        ]
983      ]
984    |2:
985      normalize nodelta
986      @(pair_replace ?????????? p)
987      [1:
988        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
989      |2:
990        @set_flags_status_of_pseudo_status try %
991        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
992        [1:
993          @sym_eq @set_clock_status_of_pseudo_status %
994        |2:
995          @I
996        |3:
997          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A)
998          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
999          whd in ⊢ (??%?);
1000          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1001        ]
1002      ]
1003    ]
1004  |10: (* MUL *)
1005    (* XXX: work on the right hand side *)
1006    (* XXX: switch to the left hand side *)
1007    >EQP -P normalize nodelta
1008    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1009    whd in maps_assm:(??%%);
1010    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1011    [2: normalize nodelta #absurd destruct(absurd) ]
1012    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1013    [2: normalize nodelta #absurd destruct(absurd) ]
1014    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1015    whd in ⊢ (??%?);
1016    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1017    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1018    [2:
1019      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
1020      @sym_eq
1021      [1:
1022        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1023        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
1024        %
1025      |2:
1026        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
1027      ]
1028    ]
1029    @sym_eq @set_8051_sfr_status_of_pseudo_status
1030    [2:
1031      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
1032      @eq_f @eq_f2 try % @eq_f2 @eq_f
1033      @sym_eq
1034      [1:
1035        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1036        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1037      |2:
1038        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
1039      ]
1040    ]
1041    @sym_eq @set_clock_status_of_pseudo_status
1042    [2:
1043      @eq_f %
1044    ]
1045    @sym_eq @set_program_counter_status_of_pseudo_status %
1046  |11,12: (* DIV *)
1047    (* XXX: work on the right hand side *)
1048    (* XXX: switch to the left hand side *)
1049    >EQP -P normalize nodelta
1050    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1051    whd in maps_assm:(??%%);
1052    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1053    [2,4: normalize nodelta #absurd destruct(absurd) ]
1054    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1055    [2,4: normalize nodelta #absurd destruct(absurd) ]
1056    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1057    whd in ⊢ (??%?);
1058    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1059    whd in ⊢ (??%?); normalize nodelta
1060    cases daemon (* XXX: need match_nat_replace but is not working! *)
1061  |13: (* DA *)
1062    (* XXX: work on the right hand side *)
1063    (* XXX: switch to the left hand side *)
1064    >EQP -P normalize nodelta
1065    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1066    whd in maps_assm:(??%%);
1067    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1068    [2: normalize nodelta #absurd destruct(absurd) ]
1069    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1070    whd in ⊢ (??%?);
1071    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1072    whd in ⊢ (??%?); normalize nodelta
1073    @(pair_replace ?????????? p)
1074    [1:
1075      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1076      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1077      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1078    |2:
1079      @(pair_replace ?????????? p)
1080      [1:
1081        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1082      |2:
1083        @(if_then_else_replace ???????? p1) normalize nodelta
1084        [1:
1085          cases (gtb ? 9)
1086          [1:
1087            %
1088          |2:
1089            change with (get_ac_flag ??? = get_ac_flag ???)
1090            @(get_ac_flag_status_of_pseudo_status M')
1091            @sym_eq @set_clock_status_of_pseudo_status
1092            >EQs >EQticks <instr_refl %
1093          ]
1094        |2:
1095          @(if_then_else_replace ???????? p1) normalize nodelta try %
1096          @(pair_replace ?????????? p2)
1097          [1:
1098            @eq_f3 try % normalize nodelta
1099            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1100            whd in ⊢ (??%?);
1101            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1102          |2:
1103            @(pair_replace ?????????? p2) try %
1104            @(pair_replace ?????????? p3) try %
1105            @(pair_replace ?????????? p3) try %
1106            @(if_then_else_replace ???????? p4) try % normalize nodelta
1107            @(if_then_else_replace ???????? p4) try % normalize nodelta
1108            @(pair_replace ?????????? p5) try %
1109            @(pair_replace ?????????? p5) try %
1110            @set_flags_status_of_pseudo_status try %
1111            [1:
1112              @eq_f @(get_ac_flag_status_of_pseudo_status M')
1113              @sym_eq @set_8051_sfr_status_of_pseudo_status
1114              [1:
1115                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1116              |2:
1117                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1118              ]
1119            |2:
1120              @(get_ov_flag_status_of_pseudo_status M')
1121              @sym_eq @set_8051_sfr_status_of_pseudo_status
1122              [1:
1123                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1124              |2:
1125                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1126              ]
1127            |3:
1128              @sym_eq @set_8051_sfr_status_of_pseudo_status
1129              [1:
1130                @sym_eq @set_clock_status_of_pseudo_status
1131                [1:
1132                  >EQs
1133                  @sym_eq @set_program_counter_status_of_pseudo_status %
1134                |2:
1135                  >EQs >EQticks <instr_refl %
1136                ]
1137              |2:
1138                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1139              ]
1140            ]
1141          ]
1142        ]
1143      ]
1144    ]
1145  |14: (* DA *)
1146    (* XXX: work on the right hand side *)
1147    (* XXX: switch to the left hand side *)
1148    >EQP -P normalize nodelta
1149    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1150    whd in maps_assm:(??%%);
1151    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1152    [2: normalize nodelta #absurd destruct(absurd) ]
1153    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1154    whd in ⊢ (??%?);
1155    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1156    whd in ⊢ (??%?); normalize nodelta
1157    @(pair_replace ?????????? p)
1158    [1:
1159      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1160      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1161      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1162    |2:
1163      @(pair_replace ?????????? p)
1164      [1:
1165        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1166      |2:
1167        @(if_then_else_replace ???????? p1) normalize nodelta
1168        [1:
1169          cases (gtb ? 9)
1170          [1:
1171            %
1172          |2:
1173            change with (get_ac_flag ??? = get_ac_flag ???)
1174            @(get_ac_flag_status_of_pseudo_status M')
1175            @sym_eq @set_clock_status_of_pseudo_status
1176            >EQs >EQticks <instr_refl %
1177          ]
1178        |2:
1179          @(if_then_else_replace ???????? p1) normalize nodelta try %
1180          @(pair_replace ?????????? p2)
1181          [1:
1182            @eq_f3 try % normalize nodelta
1183            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1184            whd in ⊢ (??%?);
1185            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1186          |2:
1187            @(pair_replace ?????????? p2) try %
1188            @(pair_replace ?????????? p3) try %
1189            @(pair_replace ?????????? p3) try %
1190            @(if_then_else_replace ???????? p4) try % normalize nodelta
1191            @(if_then_else_replace ???????? p4) try % normalize nodelta
1192            @set_clock_status_of_pseudo_status
1193            [1:
1194              >EQs
1195              @sym_eq @set_program_counter_status_of_pseudo_status %
1196            |2:
1197              >EQs >EQticks <instr_refl %
1198            ]
1199          ]
1200        ]
1201      ]
1202    ]
1203  |15: (* DA *)
1204    (* XXX: work on the right hand side *)
1205    (* XXX: switch to the left hand side *)
1206    >EQP -P normalize nodelta
1207    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1208    whd in maps_assm:(??%%);
1209    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1210    [2: normalize nodelta #absurd destruct(absurd) ]
1211    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1212    whd in ⊢ (??%?);
1213    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1214    whd in ⊢ (??%?); normalize nodelta
1215    @(pair_replace ?????????? p)
1216    [1:
1217      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1218      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1219      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1220    |2:
1221      @(pair_replace ?????????? p)
1222      [1:
1223        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1224      |2:
1225        @(if_then_else_replace ???????? p1) normalize nodelta
1226        [1:
1227          cases (gtb ? 9)
1228          [1:
1229            %
1230          |2:
1231            change with (get_ac_flag ??? = get_ac_flag ???)
1232            @(get_ac_flag_status_of_pseudo_status M')
1233            @sym_eq @set_clock_status_of_pseudo_status
1234            >EQs >EQticks <instr_refl %
1235          ]
1236        |2:
1237          @(if_then_else_replace ???????? p1) normalize nodelta try %
1238          @set_clock_status_of_pseudo_status
1239          [1:
1240            >EQs
1241            @sym_eq @set_program_counter_status_of_pseudo_status %
1242          |2:
1243            >EQs >EQticks <instr_refl %
1244          ]
1245        ]
1246      ]
1247    ]
1248  |36: (* CLR *)
1249    >EQP -P normalize nodelta
1250    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1251    whd in maps_assm:(??%%);
1252    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1253    [2: normalize nodelta #absurd destruct(absurd) ]
1254    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1255    whd in ⊢ (??%?);
1256    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1257    whd in ⊢ (??%?); normalize nodelta
1258    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1259    normalize nodelta #subaddressing_modein_witness
1260    @set_arg_8_status_of_pseudo_status try %
1261    [1:
1262      @sym_eq @set_clock_status_of_pseudo_status
1263      >EQs >EQticks <instr_refl %
1264    |2:
1265      whd in ⊢ (??%?);
1266      >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
1267      [2: <EQaddr % ] %
1268    ]
1269  |37: (* CLR *)
1270    >EQP -P normalize nodelta
1271    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1272    whd in maps_assm:(??%%);
1273    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1274    [2: normalize nodelta #absurd destruct(absurd) ]
1275    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1276    whd in ⊢ (??%?);
1277    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1278    whd in ⊢ (??%?); normalize nodelta
1279    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1280    normalize nodelta #subaddressing_modein_witness
1281    @set_arg_1_status_of_pseudo_status try %
1282    @sym_eq @set_clock_status_of_pseudo_status
1283    >EQs >EQticks <instr_refl %
1284  |38: (* CLR *)
1285    >EQP -P normalize nodelta
1286    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1287    whd in maps_assm:(??%%);
1288    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1289    [2: normalize nodelta #absurd destruct(absurd) ]
1290    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1291    whd in ⊢ (??%?);
1292    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1293    whd in ⊢ (??%?); normalize nodelta
1294    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1295    normalize nodelta #subaddressing_modein_witness
1296    @set_arg_1_status_of_pseudo_status try %
1297    [1:
1298      @sym_eq @set_clock_status_of_pseudo_status
1299      >EQs >EQticks <instr_refl %
1300    |*:
1301      (* XXX: ??? *)
1302      cases daemon
1303    ]
1304  |39: (* CPL *)
1305    >EQP -P normalize nodelta
1306    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1307    whd in maps_assm:(??%%);
1308    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1309    [2: normalize nodelta #absurd destruct(absurd) ]
1310    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1311    whd in ⊢ (??%?);
1312    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1313    whd in ⊢ (??%?); normalize nodelta
1314    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1315    normalize nodelta #subaddressing_modein_witness
1316    @set_8051_sfr_status_of_pseudo_status
1317    [1:
1318      @sym_eq @set_clock_status_of_pseudo_status
1319      >EQs >EQticks <instr_refl %
1320    |2:
1321      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
1322      [2: <EQaddr % ] normalize nodelta @eq_f
1323      @(pose … (set_clock ????)) #status #status_refl
1324      @sym_eq @(get_8051_sfr_status_of_pseudo_status M' … status) >status_refl
1325      >EQs >EQticks <instr_refl try %
1326      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addr addressing_mode_ok_assm_1)
1327      [2: <EQaddr % ] %
1328    ]
1329  |40: (* CPL *)
1330    >EQP -P normalize nodelta
1331    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1332    whd in maps_assm:(??%%);
1333    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1334    [2: normalize nodelta #absurd destruct(absurd) ]
1335    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1336    whd in ⊢ (??%?);
1337    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1338    whd in ⊢ (??%?); normalize nodelta
1339    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1340    normalize nodelta #subaddressing_modein_witness
1341    @set_arg_1_status_of_pseudo_status try %
1342    [1:
1343      @eq_f @(get_arg_1_status_of_pseudo_status … M') try %
1344      @sym_eq @set_clock_status_of_pseudo_status
1345      >EQs >EQticks <instr_refl <EQaddr %
1346    |2:
1347      @sym_eq @set_clock_status_of_pseudo_status
1348      >EQs >EQticks <instr_refl <EQaddr %
1349    ]
1350  |41: (* CPL *)
1351    >EQP -P normalize nodelta
1352    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1353    whd in maps_assm:(??%%);
1354    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1355    [2: normalize nodelta #absurd destruct(absurd) ]
1356    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1357    whd in ⊢ (??%?);
1358    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1359    whd in ⊢ (??%?); normalize nodelta
1360    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
1361    normalize nodelta #subaddressing_modein_witness
1362    @set_arg_1_status_of_pseudo_status
1363    [1:
1364      @eq_f
1365      @(pose … (set_clock ????)) #status #status_refl
1366      @(get_arg_1_status_of_pseudo_status … M' … status) try % >status_refl
1367      >EQs >EQticks <instr_refl <EQaddr
1368      [1:
1369        @sym_eq @set_clock_status_of_pseudo_status %
1370      |2:
1371        (* XXX: ??? *)
1372        cases daemon
1373      ]
1374    |2:
1375      @sym_eq @set_clock_status_of_pseudo_status
1376      >EQs >EQticks <instr_refl <EQaddr %
1377    |*:
1378      (* XXX: same as above, provable but tedious *)
1379      cases daemon
1380    ]
1381  |33: (* (* ANL *)
1382    (* XXX: work on the right hand side *)
1383    (* XXX: switch to the left hand side *)
1384    >EQP -P normalize nodelta lapply instr_refl
1385    inversion addr
1386    [1:
1387      #addr' #addr_refl'
1388      inversion addr'
1389      #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
1390      whd in ⊢ (??%? → ?); normalize nodelta cases addr
1391      [1:
1392        #acc_a #others normalize nodelta
1393        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
1394        [2: normalize nodelta #absurd destruct(absurd) ]
1395        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1396        [2: normalize nodelta #absurd destruct(absurd) ]
1397        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1398        whd in ⊢ (??%?);
1399        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1400        whd in ⊢ (??%?); normalize nodelta
1401        inversion addr #addr1 #addr2
1402        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a)
1403        @(subaddressing_mode_elim … addr2)
1404        @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try %
1405        [1:
1406          @sym_eq @set_clock_status_of_pseudo_status
1407          >EQs >EQticks <addr_refl <instr_refl
1408          [1:
1409            @sym_eq @set_program_counter_status_of_pseudo_status %
1410          |2:
1411            @eq_f2
1412            [1:
1413              >addr_refl @(subaddressing_mode_elim … addr1) %
1414            |2:
1415              @(clock_status_of_pseudo_status M')
1416              @sym_eq @set_program_counter_status_of_pseudo_status %
1417            ]
1418          ]
1419        |2:
1420          cases daemon (* XXX: matita dies here *)
1421        ]
1422      |2:
1423        #direct #others
1424        @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta
1425        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
1426        [2: normalize nodelta #absurd destruct(absurd) ]
1427        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1428        [2: normalize nodelta #absurd destruct(absurd) ]
1429        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1430        whd in ⊢ (??%?);
1431        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1432        whd in ⊢ (??%?); normalize nodelta
1433        inversion addr #addr1 #addr2
1434        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2)
1435        [1: #w |2: #w1 #w2 ] #addr_refl normalize nodelta
1436        @set_arg_8_status_of_pseudo_status
1437      ]
1438    |2:
1439      -addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
1440      whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta
1441      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
1442      [2: normalize nodelta #absurd destruct(absurd) ]
1443      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1444      [2: normalize nodelta #absurd destruct(absurd) ]
1445      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1446      whd in ⊢ (??%?);
1447      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1448      whd in ⊢ (??%?); normalize nodelta
1449      inversion addr #addr1 #addr2 #addr_refl normalize nodelta
1450      @set_flags_status_of_pseudo_status try %
1451      [1:
1452        @conjunction_split
1453        [1:
1454          @(get_cy_flag_status_of_pseudo_status M')
1455          @sym_eq @set_clock_status_of_pseudo_status
1456          >EQs >EQticks <addr_refl <instr_refl %
1457        |2:
1458          >EQs >EQticks <addr_refl <instr_refl normalize nodelta
1459          (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *)
1460          cases daemon
1461        ]
1462      |2:
1463        @(get_ov_flag_status_of_pseudo_status M')
1464        @sym_eq @set_clock_status_of_pseudo_status
1465        >EQs >EQticks <instr_refl <addr_refl %
1466      |3:
1467        @sym_eq @set_clock_status_of_pseudo_status
1468        >EQs >EQticks <instr_refl <addr_refl %
1469      ]
1470    ]
1471    whd in maps_assm:(??%%);
1472    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1473    [2: normalize nodelta #absurd destruct(absurd) ]
1474    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1475    whd in ⊢ (??%?);
1476    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1477    whd in ⊢ (??%?); normalize nodelta *)
1478  |16: (* JC *)
1479    (* XXX: work on the right hand side *)
1480    (* XXX: switch to the left hand side *)
1481    >EQP -P normalize nodelta
1482    #sigma_increment_commutation #maps_assm
1483    whd in match expand_pseudo_instruction; normalize nodelta
1484    whd in match expand_relative_jump; normalize nodelta
1485    whd in match expand_relative_jump_internal; normalize nodelta
1486    @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta
1487    inversion sj_possible #sj_possible_refl
1488    [1:
1489      #fetch_many_assm %{1}
1490      whd in maps_assm:(??%%);
1491      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1492      whd in ⊢ (??%?); normalize nodelta
1493      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1494      whd in ⊢ (??%?); normalize nodelta
1495      @(if_then_else_replace ???????? p) normalize nodelta
1496      [1:
1497        >EQs @(get_cy_flag_status_of_pseudo_status M')
1498        @sym_eq @set_program_counter_status_of_pseudo_status %
1499      |2:
1500        @(if_then_else_replace ???????? p) normalize nodelta try %
1501        >EQs >EQticks <instr_refl
1502        @set_program_counter_status_of_pseudo_status
1503        [1:
1504          >EQaddr_of normalize nodelta
1505          whd in match addr_of_relative; normalize nodelta
1506          whd in match (program_counter ???);
1507          check address_of_word_labels_code_mem_Some_hit
1508          >EQlookup_labels
1509         
1510          >sigma_increment_commutation
1511          whd in match assembly_1_pseudoinstruction; normalize nodelta
1512          whd in match expand_pseudo_instruction; normalize nodelta
1513          whd in match expand_relative_jump; normalize nodelta
1514          whd in match expand_relative_jump_internal; normalize nodelta
1515          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1516          [1:
1517            >EQppc %
1518          |2:
1519            >sj_possible_refl normalize nodelta normalize in match (length ??);
1520            lapply sigma_increment_commutation
1521            whd in match assembly_1_pseudoinstruction; normalize nodelta
1522            whd in match (length ??); normalize nodelta
1523            cases daemon
1524            (* XXX: missing invariant? *)
1525          ]
1526        |2:
1527          @sym_eq @set_clock_status_of_pseudo_status try %
1528          @eq_f2 try % whd in ⊢ (??%%);
1529          whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation
1530          whd in match assembly_1_pseudoinstruction; normalize nodelta
1531          whd in match expand_pseudo_instruction; normalize nodelta
1532          whd in match expand_relative_jump; normalize nodelta
1533          whd in match expand_relative_jump_internal; normalize nodelta
1534          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1535          [1:
1536            @eq_f2 try % >EQppc %
1537          |2:
1538            @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1539            [1:
1540              @eq_f2 try % (* XXX: finish, use Jaap's invariant *)
1541              cases daemon
1542            |2:
1543              #_ >sj_possible_refl %
1544            ]
1545          ]
1546        ]
1547      ]
1548    |2:
1549      normalize nodelta >EQppc
1550      * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1551      * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1552      * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1553      #fetch_many_assm whd in fetch_many_assm; %{2}
1554      change with (execute_1 ?? = ?)
1555      @(pose … (execute_1 ? (status_of_pseudo_status …)))
1556      #status_after_1 #EQstatus_after_1
1557      cases daemon (* XXX: ??? *)
1558    ]
1559  ]
1560qed.
1561
1562(*
1563  (* XXX: work on the left hand side *)
1564  (* XXX: switch to the right hand side *)
1565  normalize nodelta >EQs -s >EQticks -ticks
1566  whd in ⊢ (??%%);
1567  (* XXX: finally, prove the equality using sigma commutation *)
1568  cases daemon
1569  |11,12: (* DIV *)
1570  (* XXX: work on the right hand side *)
1571  normalize nodelta in p;
1572  >p normalize nodelta
1573  (* XXX: switch to the left hand side *)
1574  -instr_refl >EQP -P normalize nodelta
1575  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1576  whd in ⊢ (??%?);
1577  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1578  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1579  >(?: pose_assm = 0) normalize nodelta
1580  [2,4:
1581    <p >pose_refl
1582    cases daemon
1583  |1,3:
1584    (* XXX: switch to the right hand side *)
1585    >EQs -s >EQticks -ticks
1586    whd in ⊢ (??%%);
1587    (* XXX: finally, prove the equality using sigma commutation *)
1588    @split_eq_status try %
1589    cases daemon
1590  ]
1591  |13,14,15: (* DA *)
1592  (* XXX: work on the right hand side *)
1593  >p normalize nodelta
1594  >p1 normalize nodelta
1595  try (>p2 normalize nodelta
1596  try (>p3 normalize nodelta
1597  try (>p4 normalize nodelta
1598  try (>p5 normalize nodelta))))
1599  (* XXX: switch to the left hand side *)
1600  -instr_refl >EQP -P normalize nodelta
1601  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1602  whd in ⊢ (??%?);
1603  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1604  (* XXX: work on the left hand side *)
1605  @(pair_replace ?????????? p)
1606  [1,3,5:
1607    /demod/
1608    cases daemon
1609  |2,4,6:
1610    @(if_then_else_replace ???????? p1)
1611    [1,3,5:
1612      cases daemon
1613    |2,4:
1614      normalize nodelta
1615      @(pair_replace ?????????? p2)
1616      [1,3:
1617        cases daemon
1618      |2,4:
1619        normalize nodelta >p3 normalize nodelta
1620        >p4 normalize nodelta try >p5
1621      ]
1622    ]
1623  (* XXX: switch to the right hand side *)
1624  normalize nodelta >EQs -s >EQticks -ticks
1625  whd in ⊢ (??%%);
1626  (* XXX: finally, prove the equality using sigma commutation *)
1627  @split_eq_status try %
1628  cases daemon
1629  ]
1630  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1631  (* XXX: work on the right hand side *)
1632  cases addr #addr' normalize nodelta
1633  [1,3:
1634    cases addr' #addr'' normalize nodelta
1635  ]
1636  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1637  (* XXX: switch to the left hand side *)
1638  -instr_refl >EQP -P normalize nodelta
1639  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1640  whd in ⊢ (??%?);
1641  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1642  (* XXX: work on the left hand side *)
1643  (* XXX: switch to the right hand side *)
1644  normalize nodelta >EQs -s >EQticks -ticks
1645  whd in ⊢ (??%%);
1646  (* XXX: finally, prove the equality using sigma commutation *)
1647  cases daemon
1648  |47: (* MOV *)
1649  (* XXX: work on the right hand side *)
1650  cases addr -addr #addr normalize nodelta
1651  [1:
1652    cases addr #addr normalize nodelta
1653    [1:
1654      cases addr #addr normalize nodelta
1655      [1:
1656        cases addr #addr normalize nodelta
1657        [1:
1658          cases addr #addr normalize nodelta
1659        ]
1660      ]
1661    ]
1662  ]
1663  cases addr #lft #rgt normalize nodelta
1664  (* XXX: switch to the left hand side *)
1665  >EQP -P normalize nodelta
1666  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1667  whd in ⊢ (??%?);
1668  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1669  (* XXX: work on the left hand side *)
1670  (* XXX: switch to the right hand side *)
1671  normalize nodelta >EQs -s >EQticks -ticks
1672  whd in ⊢ (??%%);
1673  (* XXX: finally, prove the equality using sigma commutation *)
1674  cases daemon
1675  ]
1676*)
1677
1678
1679(*  [31,32: (* DJNZ *)
1680  (* XXX: work on the right hand side *)
1681  >p normalize nodelta >p1 normalize nodelta
1682  (* XXX: switch to the left hand side *)
1683  >EQP -P normalize nodelta
1684  #sigma_increment_commutation #maps_assm #fetch_many_assm
1685  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1686  <EQppc in fetch_many_assm;
1687  whd in match (short_jump_cond ??);
1688  @pair_elim #sj_possible #disp
1689  @pair_elim #result #flags #sub16_refl
1690  @pair_elim #upper #lower #vsplit_refl
1691  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1692  #sj_possible_pair destruct(sj_possible_pair)
1693  >p1 normalize nodelta
1694  [1,3:
1695    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1696    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1697    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1698    whd in ⊢ (??%?);
1699    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1700    lapply maps_assm whd in ⊢ (??%? → ?);
1701    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
1702    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
1703    (* XXX: work on the left hand side *)
1704    @(pair_replace ?????????? p) normalize nodelta
1705    [1,3:
1706      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
1707      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1708      >(get_arg_8_set_program_counter … true addr1)
1709      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1710      @get_arg_8_pseudo_addressing_mode_ok assumption
1711    |2,4:
1712      >p1 normalize nodelta >EQs
1713      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
1714      >set_program_counter_status_of_pseudo_status
1715       whd in ⊢ (??%%);
1716      @split_eq_status
1717      [1,10:
1718        whd in ⊢ (??%%); >set_arg_8_set_program_counter
1719        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1720        >low_internal_ram_set_program_counter
1721        [1:
1722          >low_internal_ram_set_program_counter
1723          (* XXX: ??? *)
1724        |2:
1725          >low_internal_ram_set_clock
1726          (* XXX: ??? *)
1727        ]
1728      |2,11:
1729        whd in ⊢ (??%%); >set_arg_8_set_program_counter
1730        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1731        >high_internal_ram_set_program_counter
1732        [1:
1733          >high_internal_ram_set_program_counter
1734          (* XXX: ??? *)
1735        |2:
1736          >high_internal_ram_set_clock
1737          (* XXX: ??? *)
1738        ]
1739      |3,12:
1740        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
1741        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1742        >(external_ram_set_arg_8 ??? addr1)
1743        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
1744      |4,13:
1745        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
1746        [1:
1747          >program_counter_set_program_counter
1748          >set_arg_8_set_program_counter
1749          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1750          >set_clock_set_program_counter >program_counter_set_program_counter
1751          change with (add ??? = ?)
1752          (* XXX: ??? *)
1753        |2:
1754          >set_arg_8_set_program_counter
1755          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1756          >program_counter_set_program_counter
1757          >set_arg_8_set_program_counter
1758          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1759          >set_clock_set_program_counter >program_counter_set_program_counter
1760          >sigma_increment_commutation <EQppc
1761          whd in match (assembly_1_pseudoinstruction ??????);
1762          whd in match (expand_pseudo_instruction ??????);
1763          (* XXX: ??? *)
1764        ]
1765      |5,14:
1766        whd in match (special_function_registers_8051 ???);
1767        [1:
1768          >special_function_registers_8051_set_program_counter
1769          >special_function_registers_8051_set_clock
1770          >set_arg_8_set_program_counter in ⊢ (???%);
1771          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1772          >special_function_registers_8051_set_program_counter
1773          >set_arg_8_set_program_counter
1774          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1775          >special_function_registers_8051_set_program_counter
1776          @special_function_registers_8051_set_arg_8 assumption
1777        |2:
1778          >special_function_registers_8051_set_clock
1779          >set_arg_8_set_program_counter
1780          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1781          >set_arg_8_set_program_counter
1782          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1783          >special_function_registers_8051_set_program_counter
1784          >special_function_registers_8051_set_program_counter
1785          @special_function_registers_8051_set_arg_8 assumption
1786        ]
1787      |6,15:
1788        whd in match (special_function_registers_8052 ???);
1789        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
1790        [1:
1791          >set_arg_8_set_program_counter
1792          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1793          >set_arg_8_set_program_counter
1794          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1795          >special_function_registers_8052_set_program_counter
1796          >special_function_registers_8052_set_program_counter
1797          @special_function_registers_8052_set_arg_8 assumption
1798        |2:
1799          whd in ⊢ (??%%);
1800          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
1801        ]
1802        (* XXX: we need special_function_registers_8052_set_arg_8 *)
1803      |7,16:
1804        whd in match (p1_latch ???);
1805        whd in match (p1_latch ???) in ⊢ (???%);
1806        (* XXX: we need p1_latch_8052_set_arg_8 *)
1807      |8,17:
1808        whd in match (p3_latch ???);
1809        whd in match (p3_latch ???) in ⊢ (???%);
1810        (* XXX: we need p3_latch_8052_set_arg_8 *)
1811      |9:
1812        >clock_set_clock
1813        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
1814        >EQticks <instr_refl @eq_f2
1815        [1:
1816          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
1817        |2:
1818          (* XXX: we need clock_set_arg_8 *)
1819        ]
1820      |18:
1821      ]
1822    ]
1823    (* XXX: switch to the right hand side *)
1824    normalize nodelta >EQs -s >EQticks -ticks
1825    cases (¬ eq_bv ???) normalize nodelta
1826    whd in ⊢ (??%%);
1827    (* XXX: finally, prove the equality using sigma commutation *)
1828    @split_eq_status try %
1829    [1,2,3,19,20,21,28,29,30:
1830      cases daemon (* XXX: axioms as above *)
1831    |4,13,22,31:
1832    |5,14,23,32:
1833    |6,15,24,33:
1834    |7,16,25,34:
1835    |8,17,26,35:
1836      whd in ⊢ (??%%);maps_assm
1837     
1838    |9,18,27,36:
1839      whd in ⊢ (??%%);
1840      whd in match (ticks_of_instruction ?); <instr_refl
1841      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
1842    ]
1843  |2,4:
1844    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1845    [2, 4:
1846      cases daemon (* XXX: !!! *)
1847    ]
1848    normalize nodelta >EQppc
1849    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1850    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1851    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1852    #fetch_many_assm whd in fetch_many_assm; %{2}
1853    change with (execute_1 ?? = ?)
1854    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1855    #status_after_1 #EQstatus_after_1
1856    <(?: ? = status_after_1)
1857    [3,6:
1858      >EQstatus_after_1 in ⊢ (???%);
1859      whd in ⊢ (???%);
1860      [1:
1861        <fetch_refl in ⊢ (???%);
1862      |2:
1863        <fetch_refl in ⊢ (???%);
1864      ]
1865      whd in ⊢ (???%);
1866      @(pair_replace ?????????? p)
1867      [1,3:
1868        cases daemon
1869      |2,4:
1870        normalize nodelta
1871        whd in match (addr_of_relative ????);
1872        cases (¬ eq_bv ???) normalize nodelta
1873        >set_clock_mk_Status_commutation
1874        whd in ⊢ (???%);
1875        change with (add ???) in match (\snd (half_add ???));
1876        >set_arg_8_set_program_counter in ⊢ (???%);
1877        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
1878        >program_counter_set_program_counter in ⊢ (???%);
1879        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1880        [2,4,6,8:
1881          >bitvector_of_nat_sign_extension_equivalence
1882          [1,3,5,7:
1883            >EQintermediate_pc' %
1884          |*:
1885            repeat @le_S_S @le_O_n
1886          ]
1887        ]
1888        [1,3: % ]
1889      ]
1890    |1,4:
1891      skip
1892    ]
1893    [3,4:
1894      -status_after_1
1895      @(pose … (execute_1 ? (mk_PreStatus …)))
1896      #status_after_1 #EQstatus_after_1
1897      <(?: ? = status_after_1)
1898      [3,6:
1899        >EQstatus_after_1 in ⊢ (???%);
1900        whd in ⊢ (???%);
1901        (* XXX: matita bug with patterns across multiple goals *)
1902        [1:
1903          <fetch_refl'' in ⊢ (???%);
1904        |2:
1905          <fetch_refl'' in ⊢ (???%);
1906        ]
1907        [2: % |1: whd in ⊢ (???%); % ]
1908      |1,4:
1909        skip
1910      ]
1911      -status_after_1 whd in ⊢ (??%?);
1912      (* XXX: switch to the right hand side *)
1913      normalize nodelta >EQs -s >EQticks -ticks
1914      normalize nodelta whd in ⊢ (??%%);
1915    ]
1916    (* XXX: finally, prove the equality using sigma commutation *)
1917    @split_eq_status try %
1918    whd in ⊢ (??%%);
1919    cases daemon
1920  ]
1921  |30: (* CJNE *)
1922  (* XXX: work on the right hand side *)
1923  cases addr1 -addr1 #addr1 normalize nodelta
1924  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
1925  (* XXX: switch to the left hand side *)
1926  >EQP -P normalize nodelta
1927  #sigma_increment_commutation #maps_assm #fetch_many_assm
1928
1929  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1930  <EQppc in fetch_many_assm;
1931  whd in match (short_jump_cond ??);
1932  @pair_elim #sj_possible #disp
1933  @pair_elim #result #flags #sub16_refl
1934  @pair_elim #upper #lower #vsplit_refl
1935  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1936  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1937  [1,3:
1938    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1939    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1940    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1941    whd in ⊢ (??%?);
1942    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1943    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1944    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
1945    @(if_then_else_replace ???????? eq_bv_refl)
1946    [1,3,5,7:
1947      cases daemon
1948    |2,4,6,8:
1949      (* XXX: switch to the right hand side *)
1950      normalize nodelta >EQs -s >EQticks -ticks
1951      whd in ⊢ (??%%);
1952      (* XXX: finally, prove the equality using sigma commutation *)
1953      @split_eq_status try %
1954      [3,7,11,15:
1955        whd in ⊢ (??%?);
1956        [1,3:
1957          cases daemon
1958        |2,4:
1959          cases daemon
1960        ]
1961      ]
1962      cases daemon (* XXX *)
1963    ]
1964  |2,4:
1965    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1966    [2, 4:
1967      cases daemon (* XXX: !!! *)
1968    ]
1969    normalize nodelta >EQppc
1970    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1971    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1972    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1973    #fetch_many_assm whd in fetch_many_assm; %{2}
1974    change with (execute_1 ?? = ?)
1975    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1976    #status_after_1 #EQstatus_after_1
1977    <(?: ? = status_after_1)
1978    [2,5:
1979      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
1980    |3,6:
1981      >EQstatus_after_1 in ⊢ (???%);
1982      whd in ⊢ (???%);
1983      [1: <fetch_refl in ⊢ (???%);
1984      |2: <fetch_refl in ⊢ (???%);
1985      ]
1986      whd in ⊢ (???%);
1987      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1988      whd in ⊢ (???%);
1989      whd in match (addr_of_relative ????);
1990      change with (add ???) in match (\snd (half_add ???));
1991      >set_clock_set_program_counter in ⊢ (???%);
1992      >program_counter_set_program_counter in ⊢ (???%);
1993      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1994      [2,4,6,8:
1995        >bitvector_of_nat_sign_extension_equivalence
1996        [1,3,5,7:
1997          >EQintermediate_pc' %
1998        |*:
1999          repeat @le_S_S @le_O_n
2000        ]
2001      |1,5:
2002        %
2003      ]
2004    |1,4: skip
2005    ]
2006    [1,2,3,4:
2007      -status_after_1
2008      @(pose … (execute_1 ? (mk_PreStatus …)))
2009      #status_after_1 #EQstatus_after_1
2010      <(?: ? = status_after_1)
2011      [3,6,9,12:
2012        >EQstatus_after_1 in ⊢ (???%);
2013        whd in ⊢ (???%);
2014        (* XXX: matita bug with patterns across multiple goals *)
2015        [1: <fetch_refl'' in ⊢ (???%);
2016        |2: <fetch_refl'' in ⊢ (???%);
2017        |3: <fetch_refl'' in ⊢ (???%);
2018        |4: <fetch_refl'' in ⊢ (???%);
2019        ] %
2020      |1,4,7,10:
2021        skip
2022      ]
2023      -status_after_1 whd in ⊢ (??%?);
2024      (* XXX: switch to the right hand side *)
2025      normalize nodelta >EQs -s >EQticks -ticks
2026      whd in ⊢ (??%%);
2027    ]
2028    (* XXX: finally, prove the equality using sigma commutation *)
2029    @split_eq_status try %
2030    cases daemon
2031  ]
2032  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
2033  (* XXX: work on the right hand side *)
2034  >p normalize nodelta
2035  (* XXX: switch to the left hand side *)
2036  >EQP -P normalize nodelta
2037  #sigma_increment_commutation #maps_assm #fetch_many_assm
2038 
2039  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2040  <EQppc in fetch_many_assm;
2041  whd in match (short_jump_cond ??);
2042  @pair_elim #sj_possible #disp
2043  @pair_elim #result #flags #sub16_refl
2044  @pair_elim #upper #lower #vsplit_refl
2045  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2046  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2047  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2048    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2049    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2050    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2051    whd in ⊢ (??%?);
2052    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2053    (* XXX: work on the left hand side *)
2054    @(if_then_else_replace ???????? p) normalize nodelta
2055    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2056      cases daemon
2057    ]
2058    (* XXX: switch to the right hand side *)
2059    normalize nodelta >EQs -s >EQticks -ticks
2060    whd in ⊢ (??%%);
2061    (* XXX: finally, prove the equality using sigma commutation *)
2062    @split_eq_status try %
2063    cases daemon
2064  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2065    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2066    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2067      cases daemon (* XXX: !!! *)
2068    ]
2069    normalize nodelta >EQppc
2070    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2071    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2072    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2073    #fetch_many_assm whd in fetch_many_assm; %{2}
2074    change with (execute_1 ?? = ?)
2075    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2076    #status_after_1 #EQstatus_after_1
2077    <(?: ? = status_after_1)
2078    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2079      >EQstatus_after_1 in ⊢ (???%);
2080      whd in ⊢ (???%);
2081      [1: <fetch_refl in ⊢ (???%);
2082      |2: <fetch_refl in ⊢ (???%);
2083      |3: <fetch_refl in ⊢ (???%);
2084      |4: <fetch_refl in ⊢ (???%);
2085      |5: <fetch_refl in ⊢ (???%);
2086      |6: <fetch_refl in ⊢ (???%);
2087      |7: <fetch_refl in ⊢ (???%);
2088      |8: <fetch_refl in ⊢ (???%);
2089      |9: <fetch_refl in ⊢ (???%);
2090      |10: <fetch_refl in ⊢ (???%);
2091      |11: <fetch_refl in ⊢ (???%);
2092      |12: <fetch_refl in ⊢ (???%);
2093      |13: <fetch_refl in ⊢ (???%);
2094      |14: <fetch_refl in ⊢ (???%);
2095      ]
2096      whd in ⊢ (???%);
2097      @(if_then_else_replace ???????? p)
2098      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2099        cases daemon
2100      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2101        normalize nodelta
2102        whd in match (addr_of_relative ????);
2103        >set_clock_mk_Status_commutation
2104        [9,10:
2105          (* XXX: demodulation not working in this case *)
2106          >program_counter_set_arg_1 in ⊢ (???%);
2107          >program_counter_set_program_counter in ⊢ (???%);
2108        |*:
2109          /demod/
2110        ]
2111        whd in ⊢ (???%);
2112        change with (add ???) in match (\snd (half_add ???));
2113        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2114        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2115          >bitvector_of_nat_sign_extension_equivalence
2116          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2117            >EQintermediate_pc' %
2118          |*:
2119            repeat @le_S_S @le_O_n
2120          ]
2121        ]
2122        %
2123      ]
2124    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
2125      skip
2126    ]
2127    -status_after_1
2128    @(pose … (execute_1 ? (mk_PreStatus …)))
2129    #status_after_1 #EQstatus_after_1
2130    <(?: ? = status_after_1)
2131    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2132      >EQstatus_after_1 in ⊢ (???%);
2133      whd in ⊢ (???%);
2134      (* XXX: matita bug with patterns across multiple goals *)
2135      [1: <fetch_refl'' in ⊢ (???%);
2136      |2: <fetch_refl' in ⊢ (???%);
2137      |3: <fetch_refl'' in ⊢ (???%);
2138      |4: <fetch_refl' in ⊢ (???%);
2139      |5: <fetch_refl'' in ⊢ (???%);
2140      |6: <fetch_refl' in ⊢ (???%);
2141      |7: <fetch_refl'' in ⊢ (???%);
2142      |8: <fetch_refl' in ⊢ (???%);
2143      |9: <fetch_refl'' in ⊢ (???%);
2144      |10: <fetch_refl' in ⊢ (???%);
2145      |11: <fetch_refl'' in ⊢ (???%);
2146      |12: <fetch_refl' in ⊢ (???%);
2147      |13: <fetch_refl'' in ⊢ (???%);
2148      |14: <fetch_refl' in ⊢ (???%);
2149      ]
2150      whd in ⊢ (???%);
2151      [9,10:
2152      |*:
2153        /demod/
2154      ] %
2155    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
2156      skip
2157    ]
2158    -status_after_1 whd in ⊢ (??%?);
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,11,19,27,36,53,61:
2165      >program_counter_set_program_counter >set_clock_mk_Status_commutation
2166      [5: >program_counter_set_program_counter ]
2167      >EQaddr_of normalize nodelta
2168      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
2169      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
2170      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
2171      >create_label_cost_refl normalize nodelta #relevant @relevant
2172      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
2173      try assumption whd in match instruction_has_label; normalize nodelta
2174      <instr_refl normalize nodelta %
2175    |7,15,23,31,45,57,65:
2176      >set_clock_mk_Status_commutation >program_counter_set_program_counter
2177      whd in ⊢ (??%?); normalize nodelta
2178      >EQppc in fetch_many_assm; #fetch_many_assm
2179      [5:
2180        >program_counter_set_arg_1 >program_counter_set_program_counter
2181      ]
2182      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
2183      <bitvector_of_nat_sign_extension_equivalence
2184      [1,3,5,7,9,11,13:
2185        whd in ⊢ (???%); cases (half_add ???) normalize //
2186      |2,4,6,8,10,12,14:
2187        @assembly1_lt_128
2188        @le_S_S @le_O_n
2189      ]
2190    |*:
2191      cases daemon
2192    ]
2193  ]
2194  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
2195  (* XXX: work on the right hand side *)
2196  lapply (subaddressing_modein ???)
2197  <EQaddr normalize nodelta #irrelevant
2198  try (>p normalize nodelta)
2199  try (>p1 normalize nodelta)
2200  (* XXX: switch to the left hand side *)
2201  >EQP -P normalize nodelta
2202  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2203  whd in ⊢ (??%?);
2204  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2205  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2206  (* XXX: work on the left hand side *)
2207  [1,2,3,4,5:
2208    generalize in ⊢ (??(???(?%))?);
2209  |6,7,8,9,10,11:
2210    generalize in ⊢ (??(???(?%))?);
2211  |12:
2212    generalize in ⊢ (??(???(?%))?);
2213  ]
2214  <EQaddr normalize nodelta #irrelevant
2215  try @(jmpair_as_replace ?????????? p)
2216  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
2217  (* XXX: switch to the right hand side *)
2218  normalize nodelta >EQs -s >EQticks -ticks
2219  whd in ⊢ (??%%);
2220  (* XXX: finally, prove the equality using sigma commutation *)
2221  try @split_eq_status try % whd in ⊢ (??%%);
2222  cases daemon
2223  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
2224  (* XXX: work on the right hand side *)
2225  >p normalize nodelta
2226  try (>p1 normalize nodelta)
2227  (* XXX: switch to the left hand side *)
2228  -instr_refl >EQP -P normalize nodelta
2229  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2230  whd in ⊢ (??%?);
2231  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2232  (* XXX: work on the left hand side *)
2233  @(pair_replace ?????????? p)
2234  [1,3,5,7,9,11,13,15,17:
2235    >set_clock_set_program_counter >set_clock_mk_Status_commutation
2236    >set_program_counter_mk_Status_commutation >clock_set_program_counter
2237    cases daemon
2238  |14,16,18:
2239    normalize nodelta
2240    @(pair_replace ?????????? p1)
2241    [1,3,5:
2242      >set_clock_mk_Status_commutation
2243      cases daemon
2244    ]
2245  ]
2246  (* XXX: switch to the right hand side *)
2247  normalize nodelta >EQs -s >EQticks -ticks
2248  whd in ⊢ (??%%);
2249  (* XXX: finally, prove the equality using sigma commutation *)
2250  try @split_eq_status try %
2251  cases daemon *)
Note: See TracBrowser for help on using the repository browser.