source: src/ASM/AssemblyProofSplit.ma @ 2129

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

Large changes from today trying to complete the main theorem. Again :(

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