source: src/ASM/AssemblyProofSplit.ma @ 2140

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

Done the hardest cases in the main theorem. Just got a few daemons to close...

File size: 53.5 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5lemma set_arg_16_mk_Status_commutation:
6  ∀M: Type[0].
7  ∀cm: M.
8  ∀s: PreStatus M cm.
9  ∀w: Word.
10  ∀d: [[dptr]].
11    set_arg_16 M cm s w d =
12      mk_PreStatus M cm
13        (low_internal_ram … s)
14        (high_internal_ram … s)
15        (external_ram … s)
16        (program_counter … s)
17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
18        (special_function_registers_8052 … s)
19        (p1_latch … s)
20        (p3_latch … s)
21        (clock … s).
22  #M #cm #s #w #d
23  whd in match set_arg_16; normalize nodelta
24  whd in match set_arg_16'; normalize nodelta
25  @(subaddressing_mode_elim … d)
26  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
29
30lemma set_program_counter_mk_Status_commutation:
31  ∀M: Type[0].
32  ∀cm: M.
33  ∀s: PreStatus M cm.
34  ∀w: Word.
35    set_program_counter M cm s w =
36      mk_PreStatus M cm
37        (low_internal_ram … s)
38        (high_internal_ram … s)
39        (external_ram … s)
40        w
41        (special_function_registers_8051 … s)
42        (special_function_registers_8052 … s)
43        (p1_latch … s)
44        (p3_latch … s)
45        (clock … s).
46  //
47qed.
48
49lemma set_clock_mk_Status_commutation:
50  ∀M: Type[0].
51  ∀cm: M.
52  ∀s: PreStatus M cm.
53  ∀c: nat.
54    set_clock M cm s c =
55      mk_PreStatus M cm
56        (low_internal_ram … s)
57        (high_internal_ram … s)
58        (external_ram … s)
59        (program_counter … s)
60        (special_function_registers_8051 … s)
61        (special_function_registers_8052 … s)
62        (p1_latch … s)
63        (p3_latch … s)
64        c.
65  //
66qed.
67
68lemma get_8051_sfr_set_clock:
69  ∀M: Type[0].
70  ∀cm: M.
71  ∀s: PreStatus M cm.
72  ∀sfr: SFR8051.
73  ∀t: Time.
74    get_8051_sfr M cm (set_clock M cm s t) sfr =
75      get_8051_sfr M cm s sfr.
76  #M #cm #s #sfr #t %
77qed.
78
79lemma get_8051_sfr_set_program_counter:
80  ∀M: Type[0].
81  ∀cm: M.
82  ∀s: PreStatus M cm.
83  ∀sfr: SFR8051.
84  ∀pc: Word.
85    get_8051_sfr M cm (set_program_counter M cm s pc) =
86      get_8051_sfr M cm s.
87  #M #cm #s #sfr #pc %
88qed.
89
90lemma special_function_registers_8051_set_arg_16:
91  ∀M, M': Type[0].
92  ∀cm: M.
93  ∀cm': M'.
94  ∀s: PreStatus M cm.
95  ∀s': PreStatus M' cm'.
96  ∀w, w': Word.
97  ∀d, d': [[dptr]].
98   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
99    w = w' →
100      special_function_registers_8051 ?? (set_arg_16 … s w d) =
101        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
102  #M #M' #cm #cm' #s #s' #w #w'
103  #d @(subaddressing_mode_elim … d)
104  #d' @(subaddressing_mode_elim … d')
105  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
106qed.
107
108lemma program_counter_set_arg_1:
109  ∀M: Type[0].
110  ∀cm: M.
111  ∀s: PreStatus M cm.
112  ∀addr: [[bit_addr; carry]].
113  ∀b: Bit.
114    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
115  #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
116  #addr #b
117  @(subaddressing_mode_elim … addr)
118  [1:
119    #byte cases (vsplit ????) #nu #nl normalize nodelta
120    cases (vsplit ????) #ignore #three_bits normalize nodelta
121    cases (get_index_v bool ????) normalize nodelta
122    [1:
123      @program_counter_set_bit_addressable_sfr
124    |2:
125      @program_counter_set_low_internal_ram
126    ]
127  |2:
128    cases (vsplit ????) //
129  ]
130qed.
131
132lemma get_ov_flag_set_program_counter:
133  ∀M: Type[0].
134  ∀cm: M.
135  ∀s: PreStatus M cm.
136  ∀pc: Word.
137    get_ov_flag M cm (set_program_counter M cm s pc) =
138      get_ov_flag M cm s.
139  #M #cm #s #pc %
140qed.
141
142lemma external_ram_set_program_counter:
143  ∀M: Type[0].
144  ∀cm: M.
145  ∀s: PreStatus M cm.
146  ∀pc: Word.
147    external_ram M cm (set_program_counter M cm s pc) =
148      external_ram M cm s.
149  #M #cm #s #pc %
150qed.
151
152lemma low_internal_ram_set_program_counter:
153  ∀M: Type[0].
154  ∀cm: M.
155  ∀s: PreStatus M cm.
156  ∀pc: Word.
157    low_internal_ram M cm (set_program_counter M cm s pc) =
158      low_internal_ram M cm s.
159  #M #cm #s #pc %
160qed.
161
162lemma high_internal_ram_set_program_counter:
163  ∀M: Type[0].
164  ∀cm: M.
165  ∀s: PreStatus M cm.
166  ∀pc: Word.
167    high_internal_ram M cm (set_program_counter M cm s pc) =
168      high_internal_ram M cm s.
169  #M #cm #s #pc %
170qed.
171
172lemma get_arg_8_set_program_counter:
173  ∀M: Type[0].
174  ∀cm: M.
175  ∀s: PreStatus M cm.
176  ∀flag: bool.
177  ∀addr.
178  ∀pc: Word.
179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
180      get_arg_8 M cm s flag addr.
181  #M #cm #s #flag #addr #pc
182  whd in match get_arg_8; normalize nodelta
183  cases addr *
184  try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I)
185  try (#addr1 #absurd normalize in absurd; cases absurd @I)
186  try (#absurd normalize in absurd; cases absurd @I)
187  try (#addr1 #addr2) try #addr1
188  normalize nodelta try %
189  cases daemon (* XXX: rewrite not working but provable *)
190qed.
191
192lemma external_ram_set_flags:
193  ∀M: Type[0].
194  ∀cm: M.
195  ∀s: PreStatus M cm.
196  ∀opt: option Bit.
197  ∀bit1, bit2: Bit.
198    external_ram M cm (set_flags M cm s bit1 opt bit2) =
199      external_ram M cm s.
200  #M #cm #s #opt #bit1 #bit2 %
201qed.
202
203lemma low_internal_ram_set_flags:
204  ∀M: Type[0].
205  ∀cm: M.
206  ∀s: PreStatus M cm.
207  ∀opt: option Bit.
208  ∀bit1, bit2: Bit.
209    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
210      low_internal_ram M cm s.
211  #M #cm #s #opt #bit1 #bit2 %
212qed.
213
214lemma high_internal_ram_set_flags:
215  ∀M: Type[0].
216  ∀cm: M.
217  ∀s: PreStatus M cm.
218  ∀opt: option Bit.
219  ∀bit1, bit2: Bit.
220    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
221      high_internal_ram M cm s.
222  #M #cm #s #opt #bit1 #bit2 %
223qed.
224
225lemma low_internal_ram_set_clock:
226  ∀M: Type[0].
227  ∀cm: M.
228  ∀s: PreStatus M cm.
229  ∀t: Time.
230    low_internal_ram M cm (set_clock M cm s t) =
231      low_internal_ram M cm s.
232  #M #cm #s #t %
233qed.
234
235lemma high_internal_ram_set_clock:
236  ∀M: Type[0].
237  ∀cm: M.
238  ∀s: PreStatus M cm.
239  ∀t: Time.
240    high_internal_ram M cm (set_clock M cm s t) =
241      high_internal_ram M cm s.
242  #M #cm #s #t %
243qed.
244
245lemma external_ram_set_clock:
246  ∀M: Type[0].
247  ∀cm: M.
248  ∀s: PreStatus M cm.
249  ∀t: Time.
250    external_ram M cm (set_clock M cm s t) =
251      external_ram M cm s.
252  #M #cm #s #t %
253qed.
254
255lemma set_8051_sfr_set_program_counter:
256  ∀M: Type[0].
257  ∀cm: M.
258  ∀s: PreStatus M cm.
259  ∀pc: Word.
260  ∀sfr: SFR8051.
261  ∀v: Byte.
262    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
263      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
264  #M #cm #s #pc #sfr #v %
265qed.
266
267lemma low_internal_ram_set_8051_sfr:
268  ∀M: Type[0].
269  ∀cm: M.
270  ∀s: PreStatus M cm.
271  ∀sfr: SFR8051.
272  ∀v: Byte.
273    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
274      low_internal_ram M cm s.
275  #M #cm #s #sfr #v %
276qed.
277
278lemma high_internal_ram_set_8051_sfr:
279  ∀M: Type[0].
280  ∀cm: M.
281  ∀s: PreStatus M cm.
282  ∀sfr: SFR8051.
283  ∀v: Byte.
284    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
285      high_internal_ram M cm s.
286  #M #cm #s #sfr #v %
287qed.
288
289lemma external_ram_set_8051_sfr:
290  ∀M: Type[0].
291  ∀cm: M.
292  ∀s: PreStatus M cm.
293  ∀sfr: SFR8051.
294  ∀v: Byte.
295    external_ram M cm (set_8051_sfr M cm s sfr v) =
296      external_ram M cm s.
297  #M #cm #s #sfr #v %
298qed.
299
300lemma get_arg_8_set_clock:
301  ∀M: Type[0].
302  ∀cm: M.
303  ∀s: PreStatus M cm.
304  ∀addr.
305  ∀t: Time.
306    get_arg_8 M cm (set_clock M cm s t) addr =
307      get_arg_8 M cm s addr.
308  #M #cm #s #addr #t %
309qed.
310
311lemma set_program_counter_set_program_counter:
312  ∀M: Type[0].
313  ∀cm: M.
314  ∀s: PreStatus M cm.
315  ∀pc: Word.
316  ∀pc': Word.
317    set_program_counter M cm (set_program_counter M cm s pc) pc' =
318      set_program_counter M cm s pc'.
319  #M #cm #s #pc #pc' %
320qed.
321
322(*
323lemma pi1_let_commute:
324 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
325 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
326 #A #B #C #P * #a #b * //
327qed.
328
329lemma pi1_let_as_commute:
330 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
331 pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
332  (let 〈x1,y1〉 as H ≝ c in pi1 … t).
333 #A #B #C #P * #a #b * //
334qed.
335
336lemma tech_pi1_let_as_commute:
337 ∀A,B,C,P. ∀f. ∀c,c':A × B.
338 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
339 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
340  c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
341  pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
342   f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
343 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
344qed.
345*)
346
347include alias "arithmetics/nat.ma".
348include alias "basics/logic.ma".
349include alias "ASM/BitVectorTrie.ma".
350
351lemma fetch_many_singleton:
352  ∀code_memory: BitVectorTrie Byte 16.
353  ∀final_pc, start_pc: Word.
354  ∀i: instruction.
355    fetch_many code_memory final_pc start_pc [i] →
356      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
357  #code_memory #final_pc #start_pc #i * #new_pc
358  #fetch_many_assm whd in fetch_many_assm;
359  cases (eq_bv_eq … fetch_many_assm) assumption
360qed.
361
362include alias "ASM/Vector.ma".
363
364lemma main_lemma_preinstruction:
365  ∀M, M': internal_pseudo_address_map.
366  ∀preamble: preamble.
367  ∀instr_list: list labelled_instruction.
368  ∀cm: pseudo_assembly_program.
369  ∀EQcm: cm = 〈preamble, instr_list〉.
370  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
371  ∀sigma: Word → Word.
372  ∀policy: Word → bool.
373  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
374  ∀ps: PseudoStatus cm.
375  ∀ppc: Word.
376  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
377  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
378  ∀labels: label_map.
379  ∀costs: BitVectorTrie costlabel 16.
380  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
381  ∀newppc: Word.
382  ∀lookup_labels: Identifier → Word.
383  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
384  ∀lookup_datalabels: Identifier → Word.
385  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
386  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
387  ∀instr: preinstruction Identifier.
388  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
389  ∀ticks: nat × nat.
390  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
391  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
392  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
393  ∀s: PreStatus pseudo_assembly_program cm.
394  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
395  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
396  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
397              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
398                  lookup_datalabels (Instruction instr)))) →
399              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
400                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))
401                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
402                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
403                      status_of_pseudo_status M' cm s sigma policy).
404    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
405  (* XXX: takes about 45 minutes to type check! *)
406  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
407  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
408  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
409  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
410  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
411  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
412  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
413  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
414  [2: * // ]
415  @(
416  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
417  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
418  match instr in preinstruction return λx. x = instr → Σs'.? with
419        [ ADD addr1 addr2 ⇒ λinstr_refl.
420            let s ≝ add_ticks1 s in
421            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
422                                                   (get_arg_8 … s false addr2) false in
423            let cy_flag ≝ get_index' ? O  ? flags in
424            let ac_flag ≝ get_index' ? 1 ? flags in
425            let ov_flag ≝ get_index' ? 2 ? flags in
426            let s ≝ set_arg_8 … s ACC_A result in
427              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
428        | ADDC addr1 addr2 ⇒ λinstr_refl.
429            let s ≝ add_ticks1 s in
430            let old_cy_flag ≝ get_cy_flag ?? s in
431            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
432                                                   (get_arg_8 … s false addr2) old_cy_flag in
433            let cy_flag ≝ get_index' ? O ? flags in
434            let ac_flag ≝ get_index' ? 1 ? flags in
435            let ov_flag ≝ get_index' ? 2 ? flags in
436            let s ≝ set_arg_8 … s ACC_A result in
437              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
438        | SUBB addr1 addr2 ⇒ λinstr_refl.
439            let s ≝ add_ticks1 s in
440            let old_cy_flag ≝ get_cy_flag ?? s in
441            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
442                                                   (get_arg_8 … s false addr2) old_cy_flag in
443            let cy_flag ≝ get_index' ? O ? flags in
444            let ac_flag ≝ get_index' ? 1 ? flags in
445            let ov_flag ≝ get_index' ? 2 ? flags in
446            let s ≝ set_arg_8 … s ACC_A result in
447              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
448        | ANL addr ⇒ λinstr_refl.
449          let s ≝ add_ticks1 s in
450          match addr with
451            [ inl l ⇒
452              match l with
453                [ inl l' ⇒
454                  let 〈addr1, addr2〉 ≝ l' in
455                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
456                    set_arg_8 … s addr1 and_val
457                | inr r ⇒
458                  let 〈addr1, addr2〉 ≝ r in
459                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
460                    set_arg_8 … s addr1 and_val
461                ]
462            | inr r ⇒
463              let 〈addr1, addr2〉 ≝ r in
464              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
465               set_flags … s and_val (None ?) (get_ov_flag ?? s)
466            ]
467        | ORL addr ⇒ λinstr_refl.
468          let s ≝ add_ticks1 s in
469          match addr with
470            [ inl l ⇒
471              match l with
472                [ inl l' ⇒
473                  let 〈addr1, addr2〉 ≝ l' in
474                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
475                    set_arg_8 … s addr1 or_val
476                | inr r ⇒
477                  let 〈addr1, addr2〉 ≝ r in
478                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
479                    set_arg_8 … s addr1 or_val
480                ]
481            | inr r ⇒
482              let 〈addr1, addr2〉 ≝ r in
483              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
484               set_flags … s or_val (None ?) (get_ov_flag … s)
485            ]
486        | XRL addr ⇒ λinstr_refl.
487          let s ≝ add_ticks1 s in
488          match addr with
489            [ inl l' ⇒
490              let 〈addr1, addr2〉 ≝ l' in
491              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
492                set_arg_8 … s addr1 xor_val
493            | inr r ⇒
494              let 〈addr1, addr2〉 ≝ r in
495              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
496                set_arg_8 … s addr1 xor_val
497            ]
498        | INC addr ⇒ λinstr_refl.
499            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
500              [ ACC_A ⇒ λacc_a: True. λEQaddr.
501                let s' ≝ add_ticks1 s in
502                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
503                 set_arg_8 … s' ACC_A result
504              | REGISTER r ⇒ λregister: True. λEQaddr.
505                let s' ≝ add_ticks1 s in
506                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
507                 set_arg_8 … s' (REGISTER r) result
508              | DIRECT d ⇒ λdirect: True. λEQaddr.
509                let s' ≝ add_ticks1 s in
510                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
511                 set_arg_8 … s' (DIRECT d) result
512              | INDIRECT i ⇒ λindirect: True. λEQaddr.
513                let s' ≝ add_ticks1 s in
514                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
515                 set_arg_8 … s' (INDIRECT i) result
516              | DPTR ⇒ λdptr: True. λEQaddr.
517                let s' ≝ add_ticks1 s in
518                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
519                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
520                let s ≝ set_8051_sfr … s' SFR_DPL bl in
521                 set_8051_sfr … s' SFR_DPH bu
522              | _ ⇒ λother: False. ⊥
523              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
524        | NOP ⇒ λinstr_refl.
525           let s ≝ add_ticks2 s in
526            s
527        | DEC addr ⇒ λinstr_refl.
528           let s ≝ add_ticks1 s in
529           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
530             set_arg_8 … s addr result
531        | MUL addr1 addr2 ⇒ λinstr_refl.
532           let s ≝ add_ticks1 s in
533           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
534           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
535           let product ≝ acc_a_nat * acc_b_nat in
536           let ov_flag ≝ product ≥ 256 in
537           let low ≝ bitvector_of_nat 8 (product mod 256) in
538           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
539           let s ≝ set_8051_sfr … s SFR_ACC_A low in
540             set_8051_sfr … s SFR_ACC_B high
541        | DIV addr1 addr2 ⇒ λinstr_refl.
542           let s ≝ add_ticks1 s in
543           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
544           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
545             match acc_b_nat with
546               [ O ⇒ set_flags … s false (None Bit) true
547               | S o ⇒
548                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
549                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
550                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
551                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
552                   set_flags … s false (None Bit) false
553               ]
554        | DA addr ⇒ λinstr_refl.
555            let s ≝ add_ticks1 s in
556            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
557              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
558                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
559                let cy_flag ≝ get_index' ? O ? flags in
560                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
561                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
562                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
563                    let new_acc ≝ nu @@ acc_nl' in
564                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
565                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
566                  else
567                    s
568              else
569                s
570        | CLR addr ⇒ λinstr_refl.
571          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
572            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
573              let s ≝ add_ticks1 s in
574               set_arg_8 … s ACC_A (zero 8)
575            | CARRY ⇒ λcarry: True.  λEQaddr.
576              let s ≝ add_ticks1 s in
577               set_arg_1 … s CARRY false
578            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
579              let s ≝ add_ticks1 s in
580               set_arg_1 … s (BIT_ADDR b) false
581            | _ ⇒ λother: False. ⊥
582            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
583        | CPL addr ⇒ λinstr_refl.
584          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
585            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
586                let s ≝ add_ticks1 s in
587                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
588                let new_acc ≝ negation_bv ? old_acc in
589                 set_8051_sfr … s SFR_ACC_A new_acc
590            | CARRY ⇒ λcarry: True. λEQaddr.
591                let s ≝ add_ticks1 s in
592                let old_cy_flag ≝ get_arg_1 … s CARRY true in
593                let new_cy_flag ≝ ¬old_cy_flag in
594                 set_arg_1 … s CARRY new_cy_flag
595            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
596                let s ≝ add_ticks1 s in
597                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
598                let new_bit ≝ ¬old_bit in
599                 set_arg_1 … s (BIT_ADDR b) new_bit
600            | _ ⇒ λother: False. ?
601            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
602        | SETB b ⇒ λinstr_refl.
603            let s ≝ add_ticks1 s in
604            set_arg_1 … s b false
605        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
606            let s ≝ add_ticks1 s in
607            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
608            let new_acc ≝ rotate_left … 1 old_acc in
609              set_8051_sfr … s SFR_ACC_A new_acc
610        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
611            let s ≝ add_ticks1 s in
612            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
613            let new_acc ≝ rotate_right … 1 old_acc in
614              set_8051_sfr … s SFR_ACC_A new_acc
615        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
616            let s ≝ add_ticks1 s in
617            let old_cy_flag ≝ get_cy_flag ?? s in
618            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
619            let new_cy_flag ≝ get_index' ? O ? old_acc in
620            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
621            let s ≝ set_arg_1 … s CARRY new_cy_flag in
622              set_8051_sfr … s SFR_ACC_A new_acc
623        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
624            let s ≝ add_ticks1 s in
625            let old_cy_flag ≝ get_cy_flag ?? s in
626            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
627            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
628            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
629            let s ≝ set_arg_1 … s CARRY new_cy_flag in
630              set_8051_sfr … s SFR_ACC_A new_acc
631        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
632            let s ≝ add_ticks1 s in
633            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
634            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
635            let new_acc ≝ nl @@ nu in
636              set_8051_sfr … s SFR_ACC_A new_acc
637        | PUSH addr ⇒ λinstr_refl.
638            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
639              [ DIRECT d ⇒ λdirect: True. λEQaddr.
640                let s ≝ add_ticks1 s in
641                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
642                let s ≝ set_8051_sfr … s SFR_SP new_sp in
643                  write_at_stack_pointer … s d
644              | _ ⇒ λother: False. ⊥
645              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
646        | POP addr ⇒ λinstr_refl.
647            let s ≝ add_ticks1 s in
648            let contents ≝ read_at_stack_pointer ?? s in
649            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
650            let s ≝ set_8051_sfr … s SFR_SP new_sp in
651              set_arg_8 … s addr contents
652        | XCH addr1 addr2 ⇒ λinstr_refl.
653            let s ≝ add_ticks1 s in
654            let old_addr ≝ get_arg_8 … s false addr2 in
655            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
656            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
657              set_arg_8 … s addr2 old_acc
658        | XCHD addr1 addr2 ⇒ λinstr_refl.
659            let s ≝ add_ticks1 s in
660            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
661            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
662            let new_acc ≝ acc_nu @@ arg_nl in
663            let new_arg ≝ arg_nu @@ acc_nl in
664            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
665              set_arg_8 … s addr2 new_arg
666        | RET ⇒ λinstr_refl.
667            let s ≝ add_ticks1 s in
668            let high_bits ≝ read_at_stack_pointer ?? s in
669            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
670            let s ≝ set_8051_sfr … s SFR_SP new_sp in
671            let low_bits ≝ read_at_stack_pointer ?? s in
672            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
673            let s ≝ set_8051_sfr … s SFR_SP new_sp in
674            let new_pc ≝ high_bits @@ low_bits in
675              set_program_counter … s new_pc
676        | RETI ⇒ λinstr_refl.
677            let s ≝ add_ticks1 s in
678            let high_bits ≝ read_at_stack_pointer ?? s in
679            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
680            let s ≝ set_8051_sfr … s SFR_SP new_sp in
681            let low_bits ≝ read_at_stack_pointer ?? s in
682            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
683            let s ≝ set_8051_sfr … s SFR_SP new_sp in
684            let new_pc ≝ high_bits @@ low_bits in
685              set_program_counter … s new_pc
686        | MOVX addr ⇒ λinstr_refl.
687          let s ≝ add_ticks1 s in
688          (* DPM: only copies --- doesn't affect I/O *)
689          match addr with
690            [ inl l ⇒
691              let 〈addr1, addr2〉 ≝ l in
692                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
693            | inr r ⇒
694              let 〈addr1, addr2〉 ≝ r in
695                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
696            ]
697        | MOV addr ⇒ λinstr_refl.
698          let s ≝ add_ticks1 s in
699          match addr with
700            [ inl l ⇒
701              match l with
702                [ inl l' ⇒
703                  match l' with
704                    [ inl l'' ⇒
705                      match l'' with
706                        [ inl l''' ⇒
707                          match l''' with
708                            [ inl l'''' ⇒
709                              let 〈addr1, addr2〉 ≝ l'''' in
710                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
711                            | inr r'''' ⇒
712                              let 〈addr1, addr2〉 ≝ r'''' in
713                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
714                            ]
715                        | inr r''' ⇒
716                          let 〈addr1, addr2〉 ≝ r''' in
717                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
718                        ]
719                    | inr r'' ⇒
720                      let 〈addr1, addr2〉 ≝ r'' in
721                       set_arg_16 … s (get_arg_16 … s addr2) addr1
722                    ]
723                | inr r ⇒
724                  let 〈addr1, addr2〉 ≝ r in
725                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
726                ]
727            | inr r ⇒
728              let 〈addr1, addr2〉 ≝ r in
729               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
730            ]
731          | JC addr ⇒ λinstr_refl.
732                  if get_cy_flag ?? s then
733                    let s ≝ add_ticks1 s in
734                      set_program_counter … s (addr_of addr s)
735                  else
736                    let s ≝ add_ticks2 s in
737                      s
738            | JNC addr ⇒ λinstr_refl.
739                  if ¬(get_cy_flag ?? s) then
740                   let s ≝ add_ticks1 s in
741                     set_program_counter … s (addr_of addr s)
742                  else
743                   let s ≝ add_ticks2 s in
744                    s
745            | JB addr1 addr2 ⇒ λinstr_refl.
746                  if get_arg_1 … s addr1 false then
747                   let s ≝ add_ticks1 s in
748                    set_program_counter … s (addr_of addr2 s)
749                  else
750                   let s ≝ add_ticks2 s in
751                    s
752            | JNB addr1 addr2 ⇒ λinstr_refl.
753                  if ¬(get_arg_1 … s addr1 false) then
754                   let s ≝ add_ticks1 s in
755                    set_program_counter … s (addr_of addr2 s)
756                  else
757                   let s ≝ add_ticks2 s in
758                    s
759            | JBC addr1 addr2 ⇒ λinstr_refl.
760                  let s ≝ set_arg_1 … s addr1 false in
761                    if get_arg_1 … s addr1 false then
762                     let s ≝ add_ticks1 s in
763                      set_program_counter … s (addr_of addr2 s)
764                    else
765                     let s ≝ add_ticks2 s in
766                      s
767            | JZ addr ⇒ λinstr_refl.
768                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
769                     let s ≝ add_ticks1 s in
770                      set_program_counter … s (addr_of addr s)
771                    else
772                     let s ≝ add_ticks2 s in
773                      s
774            | JNZ addr ⇒ λinstr_refl.
775                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
776                     let s ≝ add_ticks1 s in
777                      set_program_counter … s (addr_of addr s)
778                    else
779                     let s ≝ add_ticks2 s in
780                      s
781            | CJNE addr1 addr2 ⇒ λinstr_refl.
782                  match addr1 with
783                    [ inl l ⇒
784                        let 〈addr1, addr2'〉 ≝ l in
785                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
786                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
787                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
788                            let s ≝ add_ticks1 s in
789                            let s ≝ set_program_counter … s (addr_of addr2 s) in
790                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
791                          else
792                            let s ≝ add_ticks2 s in
793                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
794                    | inr r' ⇒
795                        let 〈addr1, addr2'〉 ≝ r' in
796                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
797                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
798                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
799                            let s ≝ add_ticks1 s in
800                            let s ≝ set_program_counter … s (addr_of addr2 s) in
801                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
802                          else
803                            let s ≝ add_ticks2 s in
804                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
805                    ]
806            | DJNZ addr1 addr2 ⇒ λinstr_refl.
807              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
808              let s ≝ set_arg_8 … s addr1 result in
809                if ¬(eq_bv ? result (zero 8)) then
810                 let s ≝ add_ticks1 s in
811                  set_program_counter … s (addr_of addr2 s)
812                else
813                 let s ≝ add_ticks2 s in
814                  s
815           ] (refl … instr))
816  try (cases(other))
817  try assumption (*20s*)
818  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
819  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
820  whd in match execute_1_preinstruction; normalize nodelta
821  [31,32: (* DJNZ *)
822  (* XXX: work on the right hand side *)
823  >p normalize nodelta >p1 normalize nodelta
824  (* XXX: switch to the left hand side *)
825  -instr_refl >EQP -P normalize nodelta
826  #sigma_increment_commutation #maps_assm #fetch_many_assm
827  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
828  <EQppc in fetch_many_assm;
829  whd in match (short_jump_cond ??);
830  @pair_elim #sj_possible #disp
831  @pair_elim #result #flags #sub16_refl
832  @pair_elim #upper #lower #vsplit_refl
833  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
834  #sj_possible_pair destruct(sj_possible_pair)
835  >p1 normalize nodelta
836  [1,3:
837    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
838    whd in ⊢ (??%?);
839    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
840    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
841    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
842    (* XXX: work on the left hand side *)
843    @(pair_replace ?????????? p) normalize nodelta
844    [1,3:
845      >get_arg_8_set_program_counter
846      cases daemon
847    ]
848    (* XXX: switch to the right hand side *)
849    normalize nodelta >EQs -s >EQticks -ticks
850    cases (¬ eq_bv ???) normalize nodelta
851    whd in ⊢ (??%%);
852    (* XXX: finally, prove the equality using sigma commutation *)
853    @split_eq_status try %
854    cases daemon
855  |2,4:
856    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
857    [2, 4:
858      cases daemon (* XXX: !!! *)
859    ]
860    normalize nodelta >EQppc
861    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
862    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
863    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
864    #fetch_many_assm whd in fetch_many_assm; %{2}
865    change with (execute_1 ?? = ?)
866    @(pose … (execute_1 ? (status_of_pseudo_status …)))
867    #status_after_1 #EQstatus_after_1
868    <(?: ? = status_after_1)
869    [3,6:
870      >EQstatus_after_1 in ⊢ (???%);
871      whd in ⊢ (???%);
872      [1:
873        <fetch_refl in ⊢ (???%);
874      |2:
875        <fetch_refl in ⊢ (???%);
876      ]
877      whd in ⊢ (???%);
878      @(pair_replace ?????????? p)
879      [1,3:
880        cases daemon
881      |2,4:
882        normalize nodelta
883        whd in match (addr_of_relative ????);
884        cases (¬ eq_bv ???) normalize nodelta
885        >set_clock_mk_Status_commutation
886        whd in ⊢ (???%);
887        change with (add ???) in match (\snd (half_add ???));
888        >set_arg_8_set_program_counter in ⊢ (???%);
889        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
890        >program_counter_set_program_counter in ⊢ (???%);
891        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
892        [2,4,6,8:
893          >bitvector_of_nat_sign_extension_equivalence
894          [1,3,5,7:
895            >EQintermediate_pc' %
896          |*:
897            repeat @le_S_S @le_O_n
898          ]
899        ]
900        [1,3: % ]
901      ]
902    |1,4:
903      skip
904    ]
905    [3,4:
906      -status_after_1
907      @(pose … (execute_1 ? (mk_PreStatus …)))
908      #status_after_1 #EQstatus_after_1
909      <(?: ? = status_after_1)
910      [3,6:
911        >EQstatus_after_1 in ⊢ (???%);
912        whd in ⊢ (???%);
913        (* XXX: matita bug with patterns across multiple goals *)
914        [1:
915          <fetch_refl'' in ⊢ (???%);
916        |2:
917          <fetch_refl'' in ⊢ (???%);
918        ]
919        [2: % |1: whd in ⊢ (???%); % ]
920      |1,4:
921        skip
922      ]
923      -status_after_1 whd in ⊢ (??%?);
924      (* XXX: switch to the right hand side *)
925      normalize nodelta >EQs -s >EQticks -ticks
926      normalize nodelta whd in ⊢ (??%%);
927    ]
928    (* XXX: finally, prove the equality using sigma commutation *)
929    @split_eq_status try %
930    whd in ⊢ (??%%);
931    cases daemon
932  ]
933  |30: (* CJNE *)
934  (* XXX: work on the right hand side *)
935  cases addr1 -addr1 #addr1 normalize nodelta
936  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
937  (* XXX: switch to the left hand side *)
938  >EQP -P normalize nodelta
939  #sigma_increment_commutation #maps_assm #fetch_many_assm
940
941  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
942  <EQppc in fetch_many_assm;
943  whd in match (short_jump_cond ??);
944  @pair_elim #sj_possible #disp
945  @pair_elim #result #flags #sub16_refl
946  @pair_elim #upper #lower #vsplit_refl
947  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
948  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
949  [1,3:
950    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
951    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
952    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
953    whd in ⊢ (??%?);
954    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
955    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
956    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
957    @(if_then_else_replace ???????? eq_bv_refl)
958    [1,3,5,7:
959      cases daemon
960    |2,4,6,8:
961      (* XXX: switch to the right hand side *)
962      normalize nodelta >EQs -s >EQticks -ticks
963      whd in ⊢ (??%%);
964      (* XXX: finally, prove the equality using sigma commutation *)
965      @split_eq_status try %
966      [3,7,11,15:
967        whd in ⊢ (??%?);
968        [1,3:
969          cases daemon
970        |2,4:
971          cases daemon
972        ]
973      ]
974      cases daemon (* XXX *)
975    ]
976  |2,4:
977    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
978    [2, 4:
979      cases daemon (* XXX: !!! *)
980    ]
981    normalize nodelta >EQppc
982    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
983    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
984    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
985    #fetch_many_assm whd in fetch_many_assm; %{2}
986    change with (execute_1 ?? = ?)
987    @(pose … (execute_1 ? (status_of_pseudo_status …)))
988    #status_after_1 #EQstatus_after_1
989    <(?: ? = status_after_1)
990    [2,5:
991      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
992    |3,6:
993      >EQstatus_after_1 in ⊢ (???%);
994      whd in ⊢ (???%);
995      [1: <fetch_refl in ⊢ (???%);
996      |2: <fetch_refl in ⊢ (???%);
997      ]
998      whd in ⊢ (???%);
999      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1000      whd in ⊢ (???%);
1001      whd in match (addr_of_relative ????);
1002      change with (add ???) in match (\snd (half_add ???));
1003      >set_clock_set_program_counter in ⊢ (???%);
1004      >program_counter_set_program_counter in ⊢ (???%);
1005      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1006      [2,4,6,8:
1007        >bitvector_of_nat_sign_extension_equivalence
1008        [1,3,5,7:
1009          >EQintermediate_pc' %
1010        |*:
1011          repeat @le_S_S @le_O_n
1012        ]
1013      |1,5:
1014        %
1015      ]
1016    |1,4: skip
1017    ]
1018    [1,2,3,4:
1019      -status_after_1
1020      @(pose … (execute_1 ? (mk_PreStatus …)))
1021      #status_after_1 #EQstatus_after_1
1022      <(?: ? = status_after_1)
1023      [3,6,9,12:
1024        >EQstatus_after_1 in ⊢ (???%);
1025        whd in ⊢ (???%);
1026        (* XXX: matita bug with patterns across multiple goals *)
1027        [1: <fetch_refl'' in ⊢ (???%);
1028        |2: <fetch_refl'' in ⊢ (???%);
1029        |3: <fetch_refl'' in ⊢ (???%);
1030        |4: <fetch_refl'' in ⊢ (???%);
1031        ] %
1032      |1,4,7,10:
1033        skip
1034      ]
1035      -status_after_1 whd in ⊢ (??%?);
1036      (* XXX: switch to the right hand side *)
1037      normalize nodelta >EQs -s >EQticks -ticks
1038      whd in ⊢ (??%%);
1039    ]
1040    (* XXX: finally, prove the equality using sigma commutation *)
1041    @split_eq_status try %
1042    cases daemon
1043  ]
1044  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1045  (* XXX: work on the right hand side *)
1046  >p normalize nodelta
1047  (* XXX: switch to the left hand side *)
1048  >EQP -P normalize nodelta
1049  #sigma_increment_commutation #maps_assm #fetch_many_assm
1050 
1051  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1052  <EQppc in fetch_many_assm;
1053  whd in match (short_jump_cond ??);
1054  @pair_elim #sj_possible #disp
1055  @pair_elim #result #flags #sub16_refl
1056  @pair_elim #upper #lower #vsplit_refl
1057  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1058  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1059  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1060    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1061    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1062    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1063    whd in ⊢ (??%?);
1064    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1065    (* XXX: work on the left hand side *)
1066    @(if_then_else_replace ???????? p) normalize nodelta
1067    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1068      cases daemon
1069    ]
1070    (* XXX: switch to the right hand side *)
1071    normalize nodelta >EQs -s >EQticks -ticks
1072    whd in ⊢ (??%%);
1073    (* XXX: finally, prove the equality using sigma commutation *)
1074    @split_eq_status try %
1075    cases daemon
1076  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1077    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1078    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1079      cases daemon (* XXX: !!! *)
1080    ]
1081    normalize nodelta >EQppc
1082    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1083    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1084    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1085    #fetch_many_assm whd in fetch_many_assm; %{2}
1086    change with (execute_1 ?? = ?)
1087    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1088    #status_after_1 #EQstatus_after_1
1089    <(?: ? = status_after_1)
1090    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1091      >EQstatus_after_1 in ⊢ (???%);
1092      whd in ⊢ (???%);
1093      [1: <fetch_refl in ⊢ (???%);
1094      |2: <fetch_refl in ⊢ (???%);
1095      |3: <fetch_refl in ⊢ (???%);
1096      |4: <fetch_refl in ⊢ (???%);
1097      |5: <fetch_refl in ⊢ (???%);
1098      |6: <fetch_refl in ⊢ (???%);
1099      |7: <fetch_refl in ⊢ (???%);
1100      |8: <fetch_refl in ⊢ (???%);
1101      |9: <fetch_refl in ⊢ (???%);
1102      |10: <fetch_refl in ⊢ (???%);
1103      |11: <fetch_refl in ⊢ (???%);
1104      |12: <fetch_refl in ⊢ (???%);
1105      |13: <fetch_refl in ⊢ (???%);
1106      |14: <fetch_refl in ⊢ (???%);
1107      ]
1108      whd in ⊢ (???%);
1109      @(if_then_else_replace ???????? p)
1110      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1111        cases daemon
1112      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1113        normalize nodelta
1114        whd in match (addr_of_relative ????);
1115        >set_clock_mk_Status_commutation
1116        [9,10:
1117          (* XXX: demodulation not working in this case *)
1118          >program_counter_set_arg_1 in ⊢ (???%);
1119          >program_counter_set_program_counter in ⊢ (???%);
1120        |*:
1121          /demod/
1122        ]
1123        whd in ⊢ (???%);
1124        change with (add ???) in match (\snd (half_add ???));
1125        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1126        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1127          >bitvector_of_nat_sign_extension_equivalence
1128          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1129            >EQintermediate_pc' %
1130          |*:
1131            repeat @le_S_S @le_O_n
1132          ]
1133        ]
1134        %
1135      ]
1136    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1137      skip
1138    ]
1139    -status_after_1
1140    @(pose … (execute_1 ? (mk_PreStatus …)))
1141    #status_after_1 #EQstatus_after_1
1142    <(?: ? = status_after_1)
1143    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1144      >EQstatus_after_1 in ⊢ (???%);
1145      whd in ⊢ (???%);
1146      (* XXX: matita bug with patterns across multiple goals *)
1147      [1: <fetch_refl'' in ⊢ (???%);
1148      |2: <fetch_refl' in ⊢ (???%);
1149      |3: <fetch_refl'' in ⊢ (???%);
1150      |4: <fetch_refl' in ⊢ (???%);
1151      |5: <fetch_refl'' in ⊢ (???%);
1152      |6: <fetch_refl' in ⊢ (???%);
1153      |7: <fetch_refl'' in ⊢ (???%);
1154      |8: <fetch_refl' in ⊢ (???%);
1155      |9: <fetch_refl'' in ⊢ (???%);
1156      |10: <fetch_refl' in ⊢ (???%);
1157      |11: <fetch_refl'' in ⊢ (???%);
1158      |12: <fetch_refl' in ⊢ (???%);
1159      |13: <fetch_refl'' in ⊢ (???%);
1160      |14: <fetch_refl' in ⊢ (???%);
1161      ]
1162      whd in ⊢ (???%);
1163      [9,10:
1164      |*:
1165        /demod/
1166      ] %
1167    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1168      skip
1169    ]
1170    -status_after_1 whd in ⊢ (??%?);
1171    (* XXX: switch to the right hand side *)
1172    normalize nodelta >EQs -s >EQticks -ticks
1173    whd in ⊢ (??%%);
1174    (* XXX: finally, prove the equality using sigma commutation *)
1175    @split_eq_status try %
1176    [3,11,19,27,36,53,61:
1177      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1178      [5: >program_counter_set_program_counter ]
1179      >EQaddr_of normalize nodelta
1180      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1181      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
1182      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
1183      >create_label_cost_refl normalize nodelta #relevant @relevant
1184      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
1185      try assumption whd in match instruction_has_label; normalize nodelta
1186      <instr_refl normalize nodelta %
1187    |7,15,23,31,45,57,65:
1188      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1189      whd in ⊢ (??%?); normalize nodelta
1190      >EQppc in fetch_many_assm; #fetch_many_assm
1191      [5:
1192        >program_counter_set_arg_1 >program_counter_set_program_counter
1193      ]
1194      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1195      <bitvector_of_nat_sign_extension_equivalence
1196      [1,3,5,7,9,11,13:
1197        whd in ⊢ (???%); cases (half_add ???) normalize //
1198      |2,4,6,8,10,12,14:
1199        @assembly1_lt_128
1200        @le_S_S @le_O_n
1201      ]
1202    |*:
1203      cases daemon
1204    ]
1205  ]
1206  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1207  (* XXX: work on the right hand side *)
1208  lapply (subaddressing_modein ???)
1209  <EQaddr normalize nodelta #irrelevant
1210  try (>p normalize nodelta)
1211  try (>p1 normalize nodelta)
1212  (* XXX: switch to the left hand side *)
1213  >EQP -P normalize nodelta
1214  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1215  whd in ⊢ (??%?);
1216  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1217  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1218  (* XXX: work on the left hand side *)
1219  [1,2,3,4,5:
1220    generalize in ⊢ (??(???(?%))?);
1221  |6,7,8,9,10,11:
1222    generalize in ⊢ (??(???(?%))?);
1223  |12:
1224    generalize in ⊢ (??(???(?%))?);
1225  ]
1226  <EQaddr normalize nodelta #irrelevant
1227  try @(jmpair_as_replace ?????????? p)
1228  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1229  (* XXX: switch to the right hand side *)
1230  normalize nodelta >EQs -s >EQticks -ticks
1231  whd in ⊢ (??%%);
1232  (* XXX: finally, prove the equality using sigma commutation *)
1233  try @split_eq_status try % whd in ⊢ (??%%);
1234  cases daemon
1235  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1236  (* XXX: work on the right hand side *)
1237  >p normalize nodelta
1238  try (>p1 normalize nodelta)
1239  (* XXX: switch to the left hand side *)
1240  -instr_refl >EQP -P normalize nodelta
1241  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1242  whd in ⊢ (??%?);
1243  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1244  (* XXX: work on the left hand side *)
1245  @(pair_replace ?????????? p)
1246  [1,3,5,7,9,11,13,15,17:
1247    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1248    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1249    cases daemon
1250  |14,16,18:
1251    normalize nodelta
1252    @(pair_replace ?????????? p1)
1253    [1,3,5:
1254      >set_clock_mk_Status_commutation
1255      cases daemon
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  try @split_eq_status try %
1263  cases daemon
1264  |10,42,43,44,45,49,52,56: (* MUL *)
1265  (* XXX: work on the right hand side *)
1266  (* XXX: switch to the left hand side *)
1267  -instr_refl >EQP -P normalize nodelta
1268  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1269  whd in ⊢ (??%?);
1270  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1271  (* XXX: work on the left hand side *)
1272  (* XXX: switch to the right hand side *)
1273  normalize nodelta >EQs -s >EQticks -ticks
1274  whd in ⊢ (??%%);
1275  (* XXX: finally, prove the equality using sigma commutation *)
1276  cases daemon
1277  |11,12: (* DIV *)
1278  (* XXX: work on the right hand side *)
1279  normalize nodelta in p;
1280  >p normalize nodelta
1281  (* XXX: switch to the left hand side *)
1282  -instr_refl >EQP -P normalize nodelta
1283  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1284  whd in ⊢ (??%?);
1285  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1286  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1287  >(?: pose_assm = 0) normalize nodelta
1288  [2,4:
1289    <p >pose_refl
1290    cases daemon
1291  |1,3:
1292    (* XXX: switch to the right hand side *)
1293    >EQs -s >EQticks -ticks
1294    whd in ⊢ (??%%);
1295    (* XXX: finally, prove the equality using sigma commutation *)
1296    @split_eq_status try %
1297    cases daemon
1298  ]
1299  |13,14,15: (* DA *)
1300  (* XXX: work on the right hand side *)
1301  >p normalize nodelta
1302  >p1 normalize nodelta
1303  try (>p2 normalize nodelta
1304  try (>p3 normalize nodelta
1305  try (>p4 normalize nodelta
1306  try (>p5 normalize nodelta))))
1307  (* XXX: switch to the left hand side *)
1308  -instr_refl >EQP -P normalize nodelta
1309  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1310  whd in ⊢ (??%?);
1311  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1312  (* XXX: work on the left hand side *)
1313  @(pair_replace ?????????? p)
1314  [1,3,5:
1315    /demod/
1316    cases daemon
1317  |2,4,6:
1318    @(if_then_else_replace ???????? p1)
1319    [1,3,5:
1320      cases daemon
1321    |2,4:
1322      normalize nodelta
1323      @(pair_replace ?????????? p2)
1324      [1,3:
1325        cases daemon
1326      |2,4:
1327        normalize nodelta >p3 normalize nodelta
1328        >p4 normalize nodelta try >p5
1329      ]
1330    ]
1331  (* XXX: switch to the right hand side *)
1332  normalize nodelta >EQs -s >EQticks -ticks
1333  whd in ⊢ (??%%);
1334  (* XXX: finally, prove the equality using sigma commutation *)
1335  @split_eq_status try %
1336  cases daemon
1337  ]
1338  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1339  (* XXX: work on the right hand side *)
1340  cases addr #addr' normalize nodelta
1341  [1,3:
1342    cases addr' #addr'' normalize nodelta
1343  ]
1344  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1345  (* XXX: switch to the left hand side *)
1346  -instr_refl >EQP -P normalize nodelta
1347  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1348  whd in ⊢ (??%?);
1349  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1350  (* XXX: work on the left hand side *)
1351  (* XXX: switch to the right hand side *)
1352  normalize nodelta >EQs -s >EQticks -ticks
1353  whd in ⊢ (??%%);
1354  (* XXX: finally, prove the equality using sigma commutation *)
1355  cases daemon
1356  |47: (* MOV *)
1357  (* XXX: work on the right hand side *)
1358  cases addr -addr #addr normalize nodelta
1359  [1:
1360    cases addr #addr normalize nodelta
1361    [1:
1362      cases addr #addr normalize nodelta
1363      [1:
1364        cases addr #addr normalize nodelta
1365        [1:
1366          cases addr #addr normalize nodelta
1367        ]
1368      ]
1369    ]
1370  ]
1371  cases addr #lft #rgt normalize nodelta
1372  (* XXX: switch to the left hand side *)
1373  >EQP -P normalize nodelta
1374  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1375  whd in ⊢ (??%?);
1376  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1377  (* XXX: work on the left hand side *)
1378  (* XXX: switch to the right hand side *)
1379  normalize nodelta >EQs -s >EQticks -ticks
1380  whd in ⊢ (??%%);
1381  (* XXX: finally, prove the equality using sigma commutation *)
1382  cases daemon
1383  ]
1384qed.
Note: See TracBrowser for help on using the repository browser.