source: src/ASM/AssemblyProofSplit.ma @ 2200

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

Work from today.

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