source: src/ASM/AssemblyProofSplit.ma @ 2207

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

Improvements and corrections to the main lemma proof in AssemblyProofSplit?.ma.

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