source: src/ASM/AssemblyProofSplit.ma @ 2136

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

No more need for functional extensionality.

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