source: src/ASM/AssemblyProofSplit.ma @ 2114

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

Proof repaired

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