source: src/ASM/AssemblyProofSplit.ma @ 2183

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

More progress on main lemma proof.

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