source: src/ASM/AssemblyProofSplit.ma @ 2121

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

More functions moved to the places they belong to

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