source: src/ASM/AssemblyProofSplit.ma @ 2181

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

Work from the last week on the new formulation of the main lemma for assembler correctness.

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