source: src/ASM/AssemblyProofSplit.ma @ 2204

Last change on this file since 2204 was 2204, checked in by sacerdot, 8 years ago

Shuffling around, suggestions, improvements.

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