source: src/ASM/AssemblyProofSplit.ma @ 2139

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

Changes to get the main lemma compiling again. Changes pushed into
the first half of the proof of the main theorem, too.

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  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
406  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
407  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
408  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
409  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
410  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
411  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
412  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
413  [2: * // ]
414  @(
415  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
416  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
417  match instr in preinstruction return λx. x = instr → Σs'.? with
418        [ ADD addr1 addr2 ⇒ λinstr_refl.
419            let s ≝ add_ticks1 s in
420            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
421                                                   (get_arg_8 … s false addr2) false in
422            let cy_flag ≝ get_index' ? O  ? flags in
423            let ac_flag ≝ get_index' ? 1 ? flags in
424            let ov_flag ≝ get_index' ? 2 ? flags in
425            let s ≝ set_arg_8 … s ACC_A result in
426              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
427        | ADDC addr1 addr2 ⇒ λinstr_refl.
428            let s ≝ add_ticks1 s in
429            let old_cy_flag ≝ get_cy_flag ?? s in
430            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
431                                                   (get_arg_8 … s false addr2) old_cy_flag in
432            let cy_flag ≝ get_index' ? O ? flags in
433            let ac_flag ≝ get_index' ? 1 ? flags in
434            let ov_flag ≝ get_index' ? 2 ? flags in
435            let s ≝ set_arg_8 … s ACC_A result in
436              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
437        | SUBB addr1 addr2 ⇒ λinstr_refl.
438            let s ≝ add_ticks1 s in
439            let old_cy_flag ≝ get_cy_flag ?? s in
440            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
441                                                   (get_arg_8 … s false addr2) old_cy_flag in
442            let cy_flag ≝ get_index' ? O ? flags in
443            let ac_flag ≝ get_index' ? 1 ? flags in
444            let ov_flag ≝ get_index' ? 2 ? flags in
445            let s ≝ set_arg_8 … s ACC_A result in
446              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
447        | ANL addr ⇒ λinstr_refl.
448          let s ≝ add_ticks1 s in
449          match addr with
450            [ inl l ⇒
451              match l with
452                [ inl l' ⇒
453                  let 〈addr1, addr2〉 ≝ l' in
454                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
455                    set_arg_8 … s addr1 and_val
456                | inr r ⇒
457                  let 〈addr1, addr2〉 ≝ r in
458                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
459                    set_arg_8 … s addr1 and_val
460                ]
461            | inr r ⇒
462              let 〈addr1, addr2〉 ≝ r in
463              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
464               set_flags … s and_val (None ?) (get_ov_flag ?? s)
465            ]
466        | ORL addr ⇒ λinstr_refl.
467          let s ≝ add_ticks1 s in
468          match addr with
469            [ inl l ⇒
470              match l with
471                [ inl l' ⇒
472                  let 〈addr1, addr2〉 ≝ l' in
473                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
474                    set_arg_8 … s addr1 or_val
475                | inr r ⇒
476                  let 〈addr1, addr2〉 ≝ r in
477                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
478                    set_arg_8 … s addr1 or_val
479                ]
480            | inr r ⇒
481              let 〈addr1, addr2〉 ≝ r in
482              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
483               set_flags … s or_val (None ?) (get_ov_flag … s)
484            ]
485        | XRL addr ⇒ λinstr_refl.
486          let s ≝ add_ticks1 s in
487          match addr with
488            [ inl l' ⇒
489              let 〈addr1, addr2〉 ≝ l' in
490              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
491                set_arg_8 … s addr1 xor_val
492            | inr r ⇒
493              let 〈addr1, addr2〉 ≝ r in
494              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
495                set_arg_8 … s addr1 xor_val
496            ]
497        | INC addr ⇒ λinstr_refl.
498            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
499              [ ACC_A ⇒ λacc_a: True. λEQaddr.
500                let s' ≝ add_ticks1 s in
501                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
502                 set_arg_8 … s' ACC_A result
503              | REGISTER r ⇒ λregister: True. λEQaddr.
504                let s' ≝ add_ticks1 s in
505                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
506                 set_arg_8 … s' (REGISTER r) result
507              | DIRECT d ⇒ λdirect: True. λEQaddr.
508                let s' ≝ add_ticks1 s in
509                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
510                 set_arg_8 … s' (DIRECT d) result
511              | INDIRECT i ⇒ λindirect: True. λEQaddr.
512                let s' ≝ add_ticks1 s in
513                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
514                 set_arg_8 … s' (INDIRECT i) result
515              | DPTR ⇒ λdptr: True. λEQaddr.
516                let s' ≝ add_ticks1 s in
517                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
518                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
519                let s ≝ set_8051_sfr … s' SFR_DPL bl in
520                 set_8051_sfr … s' SFR_DPH bu
521              | _ ⇒ λother: False. ⊥
522              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
523        | NOP ⇒ λinstr_refl.
524           let s ≝ add_ticks2 s in
525            s
526        | DEC addr ⇒ λinstr_refl.
527           let s ≝ add_ticks1 s in
528           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
529             set_arg_8 … s addr result
530        | MUL addr1 addr2 ⇒ λinstr_refl.
531           let s ≝ add_ticks1 s in
532           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
533           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
534           let product ≝ acc_a_nat * acc_b_nat in
535           let ov_flag ≝ product ≥ 256 in
536           let low ≝ bitvector_of_nat 8 (product mod 256) in
537           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
538           let s ≝ set_8051_sfr … s SFR_ACC_A low in
539             set_8051_sfr … s SFR_ACC_B high
540        | DIV addr1 addr2 ⇒ λinstr_refl.
541           let s ≝ add_ticks1 s in
542           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
543           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
544             match acc_b_nat with
545               [ O ⇒ set_flags … s false (None Bit) true
546               | S o ⇒
547                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
548                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
549                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
550                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
551                   set_flags … s false (None Bit) false
552               ]
553        | DA addr ⇒ λinstr_refl.
554            let s ≝ add_ticks1 s in
555            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
556              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
557                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
558                let cy_flag ≝ get_index' ? O ? flags in
559                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
560                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
561                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
562                    let new_acc ≝ nu @@ acc_nl' in
563                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
564                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
565                  else
566                    s
567              else
568                s
569        | CLR addr ⇒ λinstr_refl.
570          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
571            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
572              let s ≝ add_ticks1 s in
573               set_arg_8 … s ACC_A (zero 8)
574            | CARRY ⇒ λcarry: True.  λEQaddr.
575              let s ≝ add_ticks1 s in
576               set_arg_1 … s CARRY false
577            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
578              let s ≝ add_ticks1 s in
579               set_arg_1 … s (BIT_ADDR b) false
580            | _ ⇒ λother: False. ⊥
581            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
582        | CPL addr ⇒ λinstr_refl.
583          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
584            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
585                let s ≝ add_ticks1 s in
586                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
587                let new_acc ≝ negation_bv ? old_acc in
588                 set_8051_sfr … s SFR_ACC_A new_acc
589            | CARRY ⇒ λcarry: True. λEQaddr.
590                let s ≝ add_ticks1 s in
591                let old_cy_flag ≝ get_arg_1 … s CARRY true in
592                let new_cy_flag ≝ ¬old_cy_flag in
593                 set_arg_1 … s CARRY new_cy_flag
594            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
595                let s ≝ add_ticks1 s in
596                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
597                let new_bit ≝ ¬old_bit in
598                 set_arg_1 … s (BIT_ADDR b) new_bit
599            | _ ⇒ λother: False. ?
600            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
601        | SETB b ⇒ λinstr_refl.
602            let s ≝ add_ticks1 s in
603            set_arg_1 … s b false
604        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
605            let s ≝ add_ticks1 s in
606            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
607            let new_acc ≝ rotate_left … 1 old_acc in
608              set_8051_sfr … s SFR_ACC_A new_acc
609        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
610            let s ≝ add_ticks1 s in
611            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
612            let new_acc ≝ rotate_right … 1 old_acc in
613              set_8051_sfr … s SFR_ACC_A new_acc
614        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
615            let s ≝ add_ticks1 s in
616            let old_cy_flag ≝ get_cy_flag ?? s in
617            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
618            let new_cy_flag ≝ get_index' ? O ? old_acc in
619            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
620            let s ≝ set_arg_1 … s CARRY new_cy_flag in
621              set_8051_sfr … s SFR_ACC_A new_acc
622        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
623            let s ≝ add_ticks1 s in
624            let old_cy_flag ≝ get_cy_flag ?? s in
625            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
626            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
627            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
628            let s ≝ set_arg_1 … s CARRY new_cy_flag in
629              set_8051_sfr … s SFR_ACC_A new_acc
630        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
631            let s ≝ add_ticks1 s in
632            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
633            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
634            let new_acc ≝ nl @@ nu in
635              set_8051_sfr … s SFR_ACC_A new_acc
636        | PUSH addr ⇒ λinstr_refl.
637            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
638              [ DIRECT d ⇒ λdirect: True. λEQaddr.
639                let s ≝ add_ticks1 s in
640                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
641                let s ≝ set_8051_sfr … s SFR_SP new_sp in
642                  write_at_stack_pointer … s d
643              | _ ⇒ λother: False. ⊥
644              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
645        | POP addr ⇒ λinstr_refl.
646            let s ≝ add_ticks1 s in
647            let contents ≝ read_at_stack_pointer ?? s in
648            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
649            let s ≝ set_8051_sfr … s SFR_SP new_sp in
650              set_arg_8 … s addr contents
651        | XCH addr1 addr2 ⇒ λinstr_refl.
652            let s ≝ add_ticks1 s in
653            let old_addr ≝ get_arg_8 … s false addr2 in
654            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
655            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
656              set_arg_8 … s addr2 old_acc
657        | XCHD addr1 addr2 ⇒ λinstr_refl.
658            let s ≝ add_ticks1 s in
659            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
660            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
661            let new_acc ≝ acc_nu @@ arg_nl in
662            let new_arg ≝ arg_nu @@ acc_nl in
663            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
664              set_arg_8 … s addr2 new_arg
665        | RET ⇒ λinstr_refl.
666            let s ≝ add_ticks1 s in
667            let high_bits ≝ read_at_stack_pointer ?? s in
668            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
669            let s ≝ set_8051_sfr … s SFR_SP new_sp in
670            let low_bits ≝ read_at_stack_pointer ?? s in
671            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
672            let s ≝ set_8051_sfr … s SFR_SP new_sp in
673            let new_pc ≝ high_bits @@ low_bits in
674              set_program_counter … s new_pc
675        | RETI ⇒ λinstr_refl.
676            let s ≝ add_ticks1 s in
677            let high_bits ≝ read_at_stack_pointer ?? s in
678            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
679            let s ≝ set_8051_sfr … s SFR_SP new_sp in
680            let low_bits ≝ read_at_stack_pointer ?? s in
681            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
682            let s ≝ set_8051_sfr … s SFR_SP new_sp in
683            let new_pc ≝ high_bits @@ low_bits in
684              set_program_counter … s new_pc
685        | MOVX addr ⇒ λinstr_refl.
686          let s ≝ add_ticks1 s in
687          (* DPM: only copies --- doesn't affect I/O *)
688          match addr with
689            [ inl l ⇒
690              let 〈addr1, addr2〉 ≝ l in
691                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
692            | inr r ⇒
693              let 〈addr1, addr2〉 ≝ r in
694                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
695            ]
696        | MOV addr ⇒ λinstr_refl.
697          let s ≝ add_ticks1 s in
698          match addr with
699            [ inl l ⇒
700              match l with
701                [ inl l' ⇒
702                  match l' with
703                    [ inl l'' ⇒
704                      match l'' with
705                        [ inl l''' ⇒
706                          match l''' with
707                            [ inl l'''' ⇒
708                              let 〈addr1, addr2〉 ≝ l'''' in
709                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
710                            | inr r'''' ⇒
711                              let 〈addr1, addr2〉 ≝ r'''' in
712                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
713                            ]
714                        | inr r''' ⇒
715                          let 〈addr1, addr2〉 ≝ r''' in
716                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
717                        ]
718                    | inr r'' ⇒
719                      let 〈addr1, addr2〉 ≝ r'' in
720                       set_arg_16 … s (get_arg_16 … s addr2) addr1
721                    ]
722                | inr r ⇒
723                  let 〈addr1, addr2〉 ≝ r in
724                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
725                ]
726            | inr r ⇒
727              let 〈addr1, addr2〉 ≝ r in
728               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
729            ]
730          | JC addr ⇒ λinstr_refl.
731                  if get_cy_flag ?? s then
732                    let s ≝ add_ticks1 s in
733                      set_program_counter … s (addr_of addr s)
734                  else
735                    let s ≝ add_ticks2 s in
736                      s
737            | JNC addr ⇒ λinstr_refl.
738                  if ¬(get_cy_flag ?? s) then
739                   let s ≝ add_ticks1 s in
740                     set_program_counter … s (addr_of addr s)
741                  else
742                   let s ≝ add_ticks2 s in
743                    s
744            | JB addr1 addr2 ⇒ λinstr_refl.
745                  if get_arg_1 … s addr1 false then
746                   let s ≝ add_ticks1 s in
747                    set_program_counter … s (addr_of addr2 s)
748                  else
749                   let s ≝ add_ticks2 s in
750                    s
751            | JNB addr1 addr2 ⇒ λinstr_refl.
752                  if ¬(get_arg_1 … s addr1 false) then
753                   let s ≝ add_ticks1 s in
754                    set_program_counter … s (addr_of addr2 s)
755                  else
756                   let s ≝ add_ticks2 s in
757                    s
758            | JBC addr1 addr2 ⇒ λinstr_refl.
759                  let s ≝ set_arg_1 … s addr1 false in
760                    if get_arg_1 … s addr1 false then
761                     let s ≝ add_ticks1 s in
762                      set_program_counter … s (addr_of addr2 s)
763                    else
764                     let s ≝ add_ticks2 s in
765                      s
766            | JZ addr ⇒ λinstr_refl.
767                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
768                     let s ≝ add_ticks1 s in
769                      set_program_counter … s (addr_of addr s)
770                    else
771                     let s ≝ add_ticks2 s in
772                      s
773            | JNZ addr ⇒ λinstr_refl.
774                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
775                     let s ≝ add_ticks1 s in
776                      set_program_counter … s (addr_of addr s)
777                    else
778                     let s ≝ add_ticks2 s in
779                      s
780            | CJNE addr1 addr2 ⇒ λinstr_refl.
781                  match addr1 with
782                    [ inl l ⇒
783                        let 〈addr1, addr2'〉 ≝ l in
784                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
785                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
786                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
787                            let s ≝ add_ticks1 s in
788                            let s ≝ set_program_counter … s (addr_of addr2 s) in
789                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
790                          else
791                            let s ≝ add_ticks2 s in
792                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
793                    | inr r' ⇒
794                        let 〈addr1, addr2'〉 ≝ r' in
795                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
796                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
797                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
798                            let s ≝ add_ticks1 s in
799                            let s ≝ set_program_counter … s (addr_of addr2 s) in
800                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
801                          else
802                            let s ≝ add_ticks2 s in
803                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
804                    ]
805            | DJNZ addr1 addr2 ⇒ λinstr_refl.
806              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
807              let s ≝ set_arg_8 … s addr1 result in
808                if ¬(eq_bv ? result (zero 8)) then
809                 let s ≝ add_ticks1 s in
810                  set_program_counter … s (addr_of addr2 s)
811                else
812                 let s ≝ add_ticks2 s in
813                  s
814           ] (refl … instr))
815  try (cases(other))
816  try assumption (*20s*)
817  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
818  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
819  whd in match execute_1_preinstruction; normalize nodelta
820  [31,32: (* DJNZ *)
821  (* XXX: work on the right hand side *)
822  >p normalize nodelta >p1 normalize nodelta
823  (* XXX: switch to the left hand side *)
824  -instr_refl >EQP -P normalize nodelta
825  #sigma_increment_commutation #maps_assm #fetch_many_assm
826  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
827  <EQppc in fetch_many_assm;
828  whd in match (short_jump_cond ??);
829  @pair_elim #sj_possible #disp
830  @pair_elim #result #flags #sub16_refl
831  @pair_elim #upper #lower #vsplit_refl
832  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
833  #sj_possible_pair destruct(sj_possible_pair)
834  >p1 normalize nodelta
835  [1,3:
836    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
837    whd in ⊢ (??%?);
838    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
839    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
840    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
841    (* XXX: work on the left hand side *)
842    @(pair_replace ?????????? p) normalize nodelta
843    [1,3:
844      >get_arg_8_set_program_counter
845      cases daemon
846    ]
847    (* XXX: switch to the right hand side *)
848    normalize nodelta >EQs -s >EQticks -ticks
849    cases (¬ eq_bv ???) normalize nodelta
850    whd in ⊢ (??%%);
851    (* XXX: finally, prove the equality using sigma commutation *)
852    @split_eq_status try %
853    cases daemon
854  |2,4:
855    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
856    [2, 4:
857      cases daemon (* XXX: !!! *)
858    ]
859    normalize nodelta >EQppc
860    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
861    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
862    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
863    #fetch_many_assm whd in fetch_many_assm; %{2}
864    change with (execute_1 ?? = ?)
865    @(pose … (execute_1 ? (status_of_pseudo_status …)))
866    #status_after_1 #EQstatus_after_1
867    <(?: ? = status_after_1)
868    [3,6:
869      >EQstatus_after_1 in ⊢ (???%);
870      whd in ⊢ (???%);
871      [1:
872        <fetch_refl in ⊢ (???%);
873      |2:
874        <fetch_refl in ⊢ (???%);
875      ]
876      whd in ⊢ (???%);
877      @(pair_replace ?????????? p)
878      [1,3:
879        cases daemon
880      |2,4:
881        normalize nodelta
882        whd in match (addr_of_relative ????);
883        cases (¬ eq_bv ???) normalize nodelta
884        >set_clock_mk_Status_commutation
885        whd in ⊢ (???%);
886        change with (add ???) in match (\snd (half_add ???));
887        >set_arg_8_set_program_counter in ⊢ (???%);
888        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
889        >program_counter_set_program_counter in ⊢ (???%);
890        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
891        [2,4,6,8:
892          >bitvector_of_nat_sign_extension_equivalence
893          [1,3,5,7:
894            >EQintermediate_pc' %
895          |*:
896            repeat @le_S_S @le_O_n
897          ]
898        ]
899        [1,3: % ]
900      ]
901    |1,4:
902      skip
903    ]
904    [3,4:
905      -status_after_1
906      @(pose … (execute_1 ? (mk_PreStatus …)))
907      #status_after_1 #EQstatus_after_1
908      <(?: ? = status_after_1)
909      [3,6:
910        >EQstatus_after_1 in ⊢ (???%);
911        whd in ⊢ (???%);
912        (* XXX: matita bug with patterns across multiple goals *)
913        [1:
914          <fetch_refl'' in ⊢ (???%);
915        |2:
916          <fetch_refl'' in ⊢ (???%);
917        ]
918        [2: % |1: whd in ⊢ (???%); % ]
919      |1,4:
920        skip
921      ]
922      -status_after_1 whd in ⊢ (??%?);
923      (* XXX: switch to the right hand side *)
924      normalize nodelta >EQs -s >EQticks -ticks
925      normalize nodelta whd in ⊢ (??%%);
926    ]
927    (* XXX: finally, prove the equality using sigma commutation *)
928    @split_eq_status try %
929    whd in ⊢ (??%%);
930    cases daemon
931  ]
932  |30: (* CJNE *)
933  (* XXX: work on the right hand side *)
934  cases addr1 -addr1 #addr1 normalize nodelta
935  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
936  (* XXX: switch to the left hand side *)
937  >EQP -P normalize nodelta
938  #sigma_increment_commutation #maps_assm #fetch_many_assm
939
940  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
941  <EQppc in fetch_many_assm;
942  whd in match (short_jump_cond ??);
943  @pair_elim #sj_possible #disp
944  @pair_elim #result #flags #sub16_refl
945  @pair_elim #upper #lower #vsplit_refl
946  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
947  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
948  [1,3:
949    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
950    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
951    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
952    whd in ⊢ (??%?);
953    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
954    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
955    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
956    @(if_then_else_replace ???????? eq_bv_refl)
957    [1,3,5,7:
958      cases daemon
959    |2,4,6,8:
960      (* XXX: switch to the right hand side *)
961      normalize nodelta >EQs -s >EQticks -ticks
962      whd in ⊢ (??%%);
963      (* XXX: finally, prove the equality using sigma commutation *)
964      @split_eq_status try %
965      [3,7,11,15:
966        whd in ⊢ (??%?);
967        [1,3:
968          cases daemon
969        |2,4:
970          cases daemon
971        ]
972      ]
973      cases daemon (* XXX *)
974    ]
975  |2,4:
976    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
977    [2, 4:
978      cases daemon (* XXX: !!! *)
979    ]
980    normalize nodelta >EQppc
981    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
982    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
983    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
984    #fetch_many_assm whd in fetch_many_assm; %{2}
985    change with (execute_1 ?? = ?)
986    @(pose … (execute_1 ? (status_of_pseudo_status …)))
987    #status_after_1 #EQstatus_after_1
988    <(?: ? = status_after_1)
989    [2,5:
990      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
991    |3,6:
992      >EQstatus_after_1 in ⊢ (???%);
993      whd in ⊢ (???%);
994      [1: <fetch_refl in ⊢ (???%);
995      |2: <fetch_refl in ⊢ (???%);
996      ]
997      whd in ⊢ (???%);
998      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
999      whd in ⊢ (???%);
1000      whd in match (addr_of_relative ????);
1001      change with (add ???) in match (\snd (half_add ???));
1002      >set_clock_set_program_counter in ⊢ (???%);
1003      >program_counter_set_program_counter in ⊢ (???%);
1004      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1005      [2,4,6,8:
1006        >bitvector_of_nat_sign_extension_equivalence
1007        [1,3,5,7:
1008          >EQintermediate_pc' %
1009        |*:
1010          repeat @le_S_S @le_O_n
1011        ]
1012      |1,5:
1013        %
1014      ]
1015    |1,4: skip
1016    ]
1017    [1,2,3,4:
1018      -status_after_1
1019      @(pose … (execute_1 ? (mk_PreStatus …)))
1020      #status_after_1 #EQstatus_after_1
1021      <(?: ? = status_after_1)
1022      [3,6,9,12:
1023        >EQstatus_after_1 in ⊢ (???%);
1024        whd in ⊢ (???%);
1025        (* XXX: matita bug with patterns across multiple goals *)
1026        [1: <fetch_refl'' in ⊢ (???%);
1027        |2: <fetch_refl'' in ⊢ (???%);
1028        |3: <fetch_refl'' in ⊢ (???%);
1029        |4: <fetch_refl'' in ⊢ (???%);
1030        ] %
1031      |1,4,7,10:
1032        skip
1033      ]
1034      -status_after_1 whd in ⊢ (??%?);
1035      (* XXX: switch to the right hand side *)
1036      normalize nodelta >EQs -s >EQticks -ticks
1037      whd in ⊢ (??%%);
1038    ]
1039    (* XXX: finally, prove the equality using sigma commutation *)
1040    @split_eq_status try %
1041    cases daemon
1042  ]
1043  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1044  (* XXX: work on the right hand side *)
1045  >p normalize nodelta
1046  (* XXX: switch to the left hand side *)
1047  >EQP -P normalize nodelta
1048  #sigma_increment_commutation #maps_assm #fetch_many_assm
1049 
1050  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1051  <EQppc in fetch_many_assm;
1052  whd in match (short_jump_cond ??);
1053  @pair_elim #sj_possible #disp
1054  @pair_elim #result #flags #sub16_refl
1055  @pair_elim #upper #lower #vsplit_refl
1056  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
1057  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
1058  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1059    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1060    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
1061    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
1062    whd in ⊢ (??%?);
1063    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1064    (* XXX: work on the left hand side *)
1065    @(if_then_else_replace ???????? p) normalize nodelta
1066    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1067      cases daemon
1068    ]
1069    (* XXX: switch to the right hand side *)
1070    normalize nodelta >EQs -s >EQticks -ticks
1071    whd in ⊢ (??%%);
1072    (* XXX: finally, prove the equality using sigma commutation *)
1073    @split_eq_status try %
1074    cases daemon
1075  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1076    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
1077    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1078      cases daemon (* XXX: !!! *)
1079    ]
1080    normalize nodelta >EQppc
1081    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1082    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1083    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1084    #fetch_many_assm whd in fetch_many_assm; %{2}
1085    change with (execute_1 ?? = ?)
1086    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1087    #status_after_1 #EQstatus_after_1
1088    <(?: ? = status_after_1)
1089    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1090      >EQstatus_after_1 in ⊢ (???%);
1091      whd in ⊢ (???%);
1092      [1: <fetch_refl in ⊢ (???%);
1093      |2: <fetch_refl in ⊢ (???%);
1094      |3: <fetch_refl in ⊢ (???%);
1095      |4: <fetch_refl in ⊢ (???%);
1096      |5: <fetch_refl in ⊢ (???%);
1097      |6: <fetch_refl in ⊢ (???%);
1098      |7: <fetch_refl in ⊢ (???%);
1099      |8: <fetch_refl in ⊢ (???%);
1100      |9: <fetch_refl in ⊢ (???%);
1101      |10: <fetch_refl in ⊢ (???%);
1102      |11: <fetch_refl in ⊢ (???%);
1103      |12: <fetch_refl in ⊢ (???%);
1104      |13: <fetch_refl in ⊢ (???%);
1105      |14: <fetch_refl in ⊢ (???%);
1106      ]
1107      whd in ⊢ (???%);
1108      @(if_then_else_replace ???????? p)
1109      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1110        cases daemon
1111      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1112        normalize nodelta
1113        whd in match (addr_of_relative ????);
1114        >set_clock_mk_Status_commutation
1115        [9,10:
1116          (* XXX: demodulation not working in this case *)
1117          >program_counter_set_arg_1 in ⊢ (???%);
1118          >program_counter_set_program_counter in ⊢ (???%);
1119        |*:
1120          /demod/
1121        ]
1122        whd in ⊢ (???%);
1123        change with (add ???) in match (\snd (half_add ???));
1124        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1125        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1126          >bitvector_of_nat_sign_extension_equivalence
1127          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1128            >EQintermediate_pc' %
1129          |*:
1130            repeat @le_S_S @le_O_n
1131          ]
1132        ]
1133        %
1134      ]
1135    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1136      skip
1137    ]
1138    -status_after_1
1139    @(pose … (execute_1 ? (mk_PreStatus …)))
1140    #status_after_1 #EQstatus_after_1
1141    <(?: ? = status_after_1)
1142    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1143      >EQstatus_after_1 in ⊢ (???%);
1144      whd in ⊢ (???%);
1145      (* XXX: matita bug with patterns across multiple goals *)
1146      [1: <fetch_refl'' in ⊢ (???%);
1147      |2: <fetch_refl' in ⊢ (???%);
1148      |3: <fetch_refl'' in ⊢ (???%);
1149      |4: <fetch_refl' in ⊢ (???%);
1150      |5: <fetch_refl'' in ⊢ (???%);
1151      |6: <fetch_refl' in ⊢ (???%);
1152      |7: <fetch_refl'' in ⊢ (???%);
1153      |8: <fetch_refl' in ⊢ (???%);
1154      |9: <fetch_refl'' in ⊢ (???%);
1155      |10: <fetch_refl' in ⊢ (???%);
1156      |11: <fetch_refl'' in ⊢ (???%);
1157      |12: <fetch_refl' in ⊢ (???%);
1158      |13: <fetch_refl'' in ⊢ (???%);
1159      |14: <fetch_refl' in ⊢ (???%);
1160      ]
1161      whd in ⊢ (???%);
1162      [9,10:
1163      |*:
1164        /demod/
1165      ] %
1166    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1167      skip
1168    ]
1169    -status_after_1 whd in ⊢ (??%?);
1170    (* XXX: switch to the right hand side *)
1171    normalize nodelta >EQs -s >EQticks -ticks
1172    whd in ⊢ (??%%);
1173    (* XXX: finally, prove the equality using sigma commutation *)
1174    @split_eq_status try %
1175    [3,11,19,27,36,53,61:
1176      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1177      [5: >program_counter_set_program_counter ]
1178      >EQaddr_of normalize nodelta
1179      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1180      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
1181      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
1182      >create_label_cost_refl normalize nodelta #relevant @relevant
1183      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
1184      try assumption whd in match instruction_has_label; normalize nodelta
1185      <instr_refl normalize nodelta %
1186    |7,15,23,31,45,57,65:
1187      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1188      whd in ⊢ (??%?); normalize nodelta
1189      >EQppc in fetch_many_assm; #fetch_many_assm
1190      [5:
1191        >program_counter_set_arg_1 >program_counter_set_program_counter
1192      ]
1193      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1194      <bitvector_of_nat_sign_extension_equivalence
1195      [1,3,5,7,9,11,13:
1196        whd in ⊢ (???%); cases (half_add ???) normalize //
1197      |2,4,6,8,10,12,14:
1198        @assembly1_lt_128
1199        @le_S_S @le_O_n
1200      ]
1201    |*:
1202      cases daemon
1203    ]
1204  ]
1205  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1206  (* XXX: work on the right hand side *)
1207  lapply (subaddressing_modein ???)
1208  <EQaddr normalize nodelta #irrelevant
1209  try (>p normalize nodelta)
1210  try (>p1 normalize nodelta)
1211  (* XXX: switch to the left hand side *)
1212  >EQP -P normalize nodelta
1213  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1214  whd in ⊢ (??%?);
1215  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1216  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1217  (* XXX: work on the left hand side *)
1218  [1,2,3,4,5:
1219    generalize in ⊢ (??(???(?%))?);
1220  |6,7,8,9,10,11:
1221    generalize in ⊢ (??(???(?%))?);
1222  |12:
1223    generalize in ⊢ (??(???(?%))?);
1224  ]
1225  <EQaddr normalize nodelta #irrelevant
1226  try @(jmpair_as_replace ?????????? p)
1227  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1228  (* XXX: switch to the right hand side *)
1229  normalize nodelta >EQs -s >EQticks -ticks
1230  whd in ⊢ (??%%);
1231  (* XXX: finally, prove the equality using sigma commutation *)
1232  try @split_eq_status try % whd in ⊢ (??%%);
1233  cases daemon
1234  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1235  (* XXX: work on the right hand side *)
1236  >p normalize nodelta
1237  try (>p1 normalize nodelta)
1238  (* XXX: switch to the left hand side *)
1239  -instr_refl >EQP -P normalize nodelta
1240  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1241  whd in ⊢ (??%?);
1242  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1243  (* XXX: work on the left hand side *)
1244  @(pair_replace ?????????? p)
1245  [1,3,5,7,9,11,13,15,17:
1246    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1247    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1248    cases daemon
1249  |14,16,18:
1250    normalize nodelta
1251    @(pair_replace ?????????? p1)
1252    [1,3,5:
1253      >set_clock_mk_Status_commutation
1254      cases daemon
1255    ]
1256  ]
1257  (* XXX: switch to the right hand side *)
1258  normalize nodelta >EQs -s >EQticks -ticks
1259  whd in ⊢ (??%%);
1260  (* XXX: finally, prove the equality using sigma commutation *)
1261  try @split_eq_status try %
1262  cases daemon
1263  |10,42,43,44,45,49,52,56: (* MUL *)
1264  (* XXX: work on the right hand side *)
1265  (* XXX: switch to the left hand side *)
1266  -instr_refl >EQP -P normalize nodelta
1267  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1268  whd in ⊢ (??%?);
1269  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1270  (* XXX: work on the left hand side *)
1271  (* XXX: switch to the right hand side *)
1272  normalize nodelta >EQs -s >EQticks -ticks
1273  whd in ⊢ (??%%);
1274  (* XXX: finally, prove the equality using sigma commutation *)
1275  cases daemon
1276  |11,12: (* DIV *)
1277  (* XXX: work on the right hand side *)
1278  normalize nodelta in p;
1279  >p normalize nodelta
1280  (* XXX: switch to the left hand side *)
1281  -instr_refl >EQP -P normalize nodelta
1282  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1283  whd in ⊢ (??%?);
1284  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1285  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1286  >(?: pose_assm = 0) normalize nodelta
1287  [2,4:
1288    <p >pose_refl
1289    cases daemon
1290  |1,3:
1291    (* XXX: switch to the right hand side *)
1292    >EQs -s >EQticks -ticks
1293    whd in ⊢ (??%%);
1294    (* XXX: finally, prove the equality using sigma commutation *)
1295    @split_eq_status try %
1296    cases daemon
1297  ]
1298  |13,14,15: (* DA *)
1299  (* XXX: work on the right hand side *)
1300  >p normalize nodelta
1301  >p1 normalize nodelta
1302  try (>p2 normalize nodelta
1303  try (>p3 normalize nodelta
1304  try (>p4 normalize nodelta
1305  try (>p5 normalize nodelta))))
1306  (* XXX: switch to the left hand side *)
1307  -instr_refl >EQP -P normalize nodelta
1308  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1309  whd in ⊢ (??%?);
1310  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1311  (* XXX: work on the left hand side *)
1312  @(pair_replace ?????????? p)
1313  [1,3,5:
1314    /demod/
1315    cases daemon
1316  |2,4,6:
1317    @(if_then_else_replace ???????? p1)
1318    [1,3,5:
1319      cases daemon
1320    |2,4:
1321      normalize nodelta
1322      @(pair_replace ?????????? p2)
1323      [1,3:
1324        cases daemon
1325      |2,4:
1326        normalize nodelta >p3 normalize nodelta
1327        >p4 normalize nodelta try >p5
1328      ]
1329    ]
1330  (* XXX: switch to the right hand side *)
1331  normalize nodelta >EQs -s >EQticks -ticks
1332  whd in ⊢ (??%%);
1333  (* XXX: finally, prove the equality using sigma commutation *)
1334  @split_eq_status try %
1335  cases daemon
1336  ]
1337  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1338  (* XXX: work on the right hand side *)
1339  cases addr #addr' normalize nodelta
1340  [1,3:
1341    cases addr' #addr'' normalize nodelta
1342  ]
1343  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1344  (* XXX: switch to the left hand side *)
1345  -instr_refl >EQP -P normalize nodelta
1346  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1347  whd in ⊢ (??%?);
1348  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1349  (* XXX: work on the left hand side *)
1350  (* XXX: switch to the right hand side *)
1351  normalize nodelta >EQs -s >EQticks -ticks
1352  whd in ⊢ (??%%);
1353  (* XXX: finally, prove the equality using sigma commutation *)
1354  cases daemon
1355  |47: (* MOV *)
1356  (* XXX: work on the right hand side *)
1357  cases addr -addr #addr normalize nodelta
1358  [1:
1359    cases addr #addr normalize nodelta
1360    [1:
1361      cases addr #addr normalize nodelta
1362      [1:
1363        cases addr #addr normalize nodelta
1364        [1:
1365          cases addr #addr normalize nodelta
1366        ]
1367      ]
1368    ]
1369  ]
1370  cases addr #lft #rgt normalize nodelta
1371  (* XXX: switch to the left hand side *)
1372  >EQP -P normalize nodelta
1373  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1374  whd in ⊢ (??%?);
1375  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1376  (* XXX: work on the left hand side *)
1377  (* XXX: switch to the right hand side *)
1378  normalize nodelta >EQs -s >EQticks -ticks
1379  whd in ⊢ (??%%);
1380  (* XXX: finally, prove the equality using sigma commutation *)
1381  cases daemon
1382  ]
1383qed.
Note: See TracBrowser for help on using the repository browser.