source: src/ASM/AssemblyProofSplit.ma @ 2122

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

More stuff moved around in proper places

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