source: src/ASM/AssemblyProofSplit.ma @ 2187

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

Work from today on the big proof.

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