source: src/ASM/AssemblyProofSplit.ma @ 2108

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

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File size: 53.6 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5lemma set_arg_16_mk_Status_commutation:
6  ∀M: Type[0].
7  ∀cm: M.
8  ∀s: PreStatus M cm.
9  ∀w: Word.
10  ∀d: [[dptr]].
11    set_arg_16 M cm s w d =
12      mk_PreStatus M cm
13        (low_internal_ram … s)
14        (high_internal_ram … s)
15        (external_ram … s)
16        (program_counter … s)
17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
18        (special_function_registers_8052 … s)
19        (p1_latch … s)
20        (p3_latch … s)
21        (clock … s).
22  #M #cm #s #w #d
23  whd in match set_arg_16; normalize nodelta
24  whd in match set_arg_16'; normalize nodelta
25  @(subaddressing_mode_elim … d)
26  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
29
30lemma set_program_counter_mk_Status_commutation:
31  ∀M: Type[0].
32  ∀cm: M.
33  ∀s: PreStatus M cm.
34  ∀w: Word.
35    set_program_counter M cm s w =
36      mk_PreStatus M cm
37        (low_internal_ram … s)
38        (high_internal_ram … s)
39        (external_ram … s)
40        w
41        (special_function_registers_8051 … s)
42        (special_function_registers_8052 … s)
43        (p1_latch … s)
44        (p3_latch … s)
45        (clock … s).
46  //
47qed.
48
49lemma set_clock_mk_Status_commutation:
50  ∀M: Type[0].
51  ∀cm: M.
52  ∀s: PreStatus M cm.
53  ∀c: nat.
54    set_clock M cm s c =
55      mk_PreStatus M cm
56        (low_internal_ram … s)
57        (high_internal_ram … s)
58        (external_ram … s)
59        (program_counter … s)
60        (special_function_registers_8051 … s)
61        (special_function_registers_8052 … s)
62        (p1_latch … s)
63        (p3_latch … s)
64        c.
65  //
66qed.
67
68lemma get_8051_sfr_set_clock:
69  ∀M: Type[0].
70  ∀cm: M.
71  ∀s: PreStatus M cm.
72  ∀sfr: SFR8051.
73  ∀t: Time.
74    get_8051_sfr M cm (set_clock M cm s t) sfr =
75      get_8051_sfr M cm s sfr.
76  #M #cm #s #sfr #t %
77qed.
78
79lemma get_8051_sfr_set_program_counter:
80  ∀M: Type[0].
81  ∀cm: M.
82  ∀s: PreStatus M cm.
83  ∀sfr: SFR8051.
84  ∀pc: Word.
85    get_8051_sfr M cm (set_program_counter M cm s pc) =
86      get_8051_sfr M cm s.
87  #M #cm #s #sfr #pc %
88qed.
89
90lemma special_function_registers_8051_set_arg_16:
91  ∀M, M': Type[0].
92  ∀cm: M.
93  ∀cm': M'.
94  ∀s: PreStatus M cm.
95  ∀s': PreStatus M' cm'.
96  ∀w, w': Word.
97  ∀d, d': [[dptr]].
98   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
99    w = w' →
100      special_function_registers_8051 ?? (set_arg_16 … s w d) =
101        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
102  #M #M' #cm #cm' #s #s' #w #w'
103  @list_addressing_mode_tags_elim_prop try %
104  @list_addressing_mode_tags_elim_prop try %
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    XXX: here
907    >EQppc
908    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
909    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
910    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
911    #fetch_many_assm whd in fetch_many_assm; %{2}
912    change with (execute_1 ?? = ?)
913    @(pose … (execute_1 ? (status_of_pseudo_status …)))
914    #status_after_1 #EQstatus_after_1
915    <(?: ? = status_after_1)
916    [3,6:
917      >EQstatus_after_1 in ⊢ (???%);
918      whd in ⊢ (???%);
919      [1:exists_labelled_instruction id instr_list →
920        <fetch_refl in ⊢ (???%);
921      |2:
922        <fetch_refl in ⊢ (???%);
923      ]
924      whd in ⊢ (???%);
925      @(pair_replace ?????????? p)
926      [1,3:
927        cases daemon
928      |2,4:
929        normalize nodelta
930        whd in match (addr_of_relative ????);
931        cases (¬ eq_bv ???) normalize nodelta
932        >set_clock_mk_Status_commutation
933        whd in ⊢ (???%);
934        change with (add ???) in match (\snd (half_add ???));
935        >set_arg_8_set_program_counter in ⊢ (???%);
936        [2,4,6,8: /2/ ]
937        >program_counter_set_program_counter in ⊢ (???%);
938        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
939        [2,4,6,8:
940          >bitvector_of_nat_sign_extension_equivalence
941          [1,3,5,7:
942            >EQintermediate_pc' %
943          |*:
944            repeat @le_S_S @le_O_n
945          ]
946        ]
947        [1,3: % ]
948      ]
949    |1,4:
950      skip
951    ]
952    [3,4:
953      -status_after_1
954      @(pose … (execute_1 ? (mk_PreStatus …)))
955      #status_after_1 #EQstatus_after_1
956      <(?: ? = status_after_1)
957      [3,6:
958        >EQstatus_after_1 in ⊢ (???%);
959        whd in ⊢ (???%);
960        (* XXX: matita bug with patterns across multiple goals *)
961        [1:
962          <fetch_refl'' in ⊢ (???%);
963        |2:
964          <fetch_refl'' in ⊢ (???%);
965        ]
966        [2: % |1: whd in ⊢ (???%); % ]
967      |1,4:
968        skip
969      ]
970      -status_after_1 whd in ⊢ (??%?);
971      (* XXX: switch to the right hand side *)
972      normalize nodelta >EQs -s >EQticks -ticks
973      cases (¬ eq_bv ???) normalize nodelta
974      whd in ⊢ (??%%);
975    ]
976    (* XXX: finally, prove the equality using sigma commutation *)
977    @split_eq_status try %
978    whd in ⊢ (??%%);
979    cases daemon
980  ]
981  |30: (* CJNE *)
982  (* XXX: work on the right hand side *)
983  cases addr1 -addr1 #addr1 normalize nodelta
984  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
985  (* XXX: switch to the left hand side *)
986  >EQP -P normalize nodelta
987  #sigma_increment_commutation #maps_assm #fetch_many_assm
988
989  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
990  whd in match (expand_relative_jump ????);
991  <EQppc in fetch_many_assm;
992  @pair_elim #result #flags #sub16_refl
993  @pair_elim #upper #lower #vsplit_refl
994  inversion (eq_bv ???) #upper_vsplit_refl normalize nodelta
995  [1,3:
996    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
997    whd in ⊢ (??%?);
998    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
999    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1000    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
1001    @(if_then_else_replace ???????? eq_bv_refl)
1002    [1,3,5,7:
1003      cases daemon
1004    |2,4,6,8:
1005      (* XXX: switch to the right hand side *)
1006      normalize nodelta >EQs -s >EQticks -ticks
1007      whd in ⊢ (??%%);
1008      (* XXX: finally, prove the equality using sigma commutation *)
1009      @split_eq_status try %
1010      [3,7,11,15:
1011        whd in ⊢ (??%?);
1012        [1,3:
1013          cases daemon
1014        |2,4:
1015          cases daemon
1016        ]
1017      ]
1018      cases daemon (* XXX *)
1019    ]
1020  |2,4:
1021    >EQppc
1022    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1023    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1024    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1025    #fetch_many_assm whd in fetch_many_assm; %{2}
1026    change with (execute_1 ?? = ?)
1027    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1028    #status_after_1 #EQstatus_after_1
1029    <(?: ? = status_after_1)
1030    [2,5:
1031      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
1032    |3,6:
1033      >EQstatus_after_1 in ⊢ (???%);
1034      whd in ⊢ (???%);
1035      [1: <fetch_refl in ⊢ (???%);
1036      |2: <fetch_refl in ⊢ (???%);
1037      ]
1038      whd in ⊢ (???%);
1039      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1040      whd in ⊢ (???%);
1041      whd in match (addr_of_relative ????);
1042      change with (add ???) in match (\snd (half_add ???));
1043      >set_clock_set_program_counter in ⊢ (???%);
1044      >program_counter_set_program_counter in ⊢ (???%);
1045      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1046      [2,4,6,8:
1047        >bitvector_of_nat_sign_extension_equivalence
1048        [1,3,5,7:
1049          >EQintermediate_pc' %
1050        |*:
1051          repeat @le_S_S @le_O_n
1052        ]
1053      |1,5:
1054        %
1055      ]
1056    |1,4: skip
1057    ]
1058    [1,2,3,4:
1059      -status_after_1
1060      @(pose … (execute_1 ? (mk_PreStatus …)))
1061      #status_after_1 #EQstatus_after_1
1062      <(?: ? = status_after_1)
1063      [3,6,9,12:
1064        >EQstatus_after_1 in ⊢ (???%);
1065        whd in ⊢ (???%);
1066        (* XXX: matita bug with patterns across multiple goals *)
1067        [1: <fetch_refl'' in ⊢ (???%);
1068        |2: <fetch_refl'' in ⊢ (???%);
1069        |3: <fetch_refl'' in ⊢ (???%);
1070        |4: <fetch_refl'' in ⊢ (???%);
1071        ] %
1072      |1,4,7,10:
1073        skip
1074      ]
1075      -status_after_1 whd in ⊢ (??%?);
1076      (* XXX: switch to the right hand side *)
1077      normalize nodelta >EQs -s >EQticks -ticks
1078      whd in ⊢ (??%%);
1079    ]
1080    (* XXX: finally, prove the equality using sigma commutation *)
1081    @split_eq_status try %
1082    cases daemon
1083  ]
1084  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1085  (* XXX: work on the right hand side *)
1086  >p normalize nodelta
1087  (* XXX: switch to the left hand side *)
1088  -instr_refl >EQP -P normalize nodelta
1089  #sigma_increment_commutation #maps_assm #fetch_many_assm
1090 
1091  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1092  whd in match (expand_relative_jump ????);
1093  <EQppc in fetch_many_assm;
1094  @pair_elim #result #flags #sub16_refl
1095  @pair_elim #upper #lower #vsplit_refl
1096  cases (eq_bv ???) normalize nodelta
1097  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1098    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1099    whd in ⊢ (??%?);
1100    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1101    (* XXX: work on the left hand side *)
1102    @(if_then_else_replace ???????? p) normalize nodelta
1103    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1104      cases daemon
1105    ]
1106    (* XXX: switch to the right hand side *)
1107    normalize nodelta >EQs -s >EQticks -ticks
1108    whd in ⊢ (??%%);
1109    (* XXX: finally, prove the equality using sigma commutation *)
1110    @split_eq_status try %
1111    cases daemon
1112  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1113    >EQppc
1114    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1115    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1116    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1117    #fetch_many_assm whd in fetch_many_assm; %{2}
1118    change with (execute_1 ?? = ?)
1119    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1120    #status_after_1 #EQstatus_after_1
1121    <(?: ? = status_after_1)
1122    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1123      >EQstatus_after_1 in ⊢ (???%);
1124      whd in ⊢ (???%);
1125      [1: <fetch_refl in ⊢ (???%);
1126      |2: <fetch_refl in ⊢ (???%);
1127      |3: <fetch_refl in ⊢ (???%);
1128      |4: <fetch_refl in ⊢ (???%);
1129      |5: <fetch_refl in ⊢ (???%);
1130      |6: <fetch_refl in ⊢ (???%);
1131      |7: <fetch_refl in ⊢ (???%);
1132      |8: <fetch_refl in ⊢ (???%);
1133      |9: <fetch_refl in ⊢ (???%);
1134      |10: <fetch_refl in ⊢ (???%);
1135      |11: <fetch_refl in ⊢ (???%);
1136      |12: <fetch_refl in ⊢ (???%);
1137      |13: <fetch_refl in ⊢ (???%);
1138      |14: <fetch_refl in ⊢ (???%);
1139      ]
1140      whd in ⊢ (???%);
1141      @(if_then_else_replace ???????? p)
1142      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1143        cases daemon
1144      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1145        normalize nodelta
1146        whd in match (addr_of_relative ????);
1147        >set_clock_mk_Status_commutation
1148        [9,10:
1149          (* XXX: demodulation not working in this case *)
1150          >program_counter_set_arg_1 in ⊢ (???%);
1151          >program_counter_set_program_counter in ⊢ (???%);
1152        |*:
1153          /demod/
1154        ]
1155        whd in ⊢ (???%);
1156        change with (add ???) in match (\snd (half_add ???));
1157        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1158        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1159          >bitvector_of_nat_sign_extension_equivalence
1160          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1161            >EQintermediate_pc' %
1162          |*:
1163            repeat @le_S_S @le_O_n
1164          ]
1165        ]
1166        %
1167      ]
1168    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1169      skip
1170    ]
1171    -status_after_1
1172    @(pose … (execute_1 ? (mk_PreStatus …)))
1173    #status_after_1 #EQstatus_after_1
1174    <(?: ? = status_after_1)
1175    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1176      >EQstatus_after_1 in ⊢ (???%);
1177      whd in ⊢ (???%);
1178      (* XXX: matita bug with patterns across multiple goals *)
1179      [1: <fetch_refl'' in ⊢ (???%);
1180      |2: <fetch_refl' in ⊢ (???%);
1181      |3: <fetch_refl'' in ⊢ (???%);
1182      |4: <fetch_refl' in ⊢ (???%);
1183      |5: <fetch_refl'' in ⊢ (???%);
1184      |6: <fetch_refl' in ⊢ (???%);
1185      |7: <fetch_refl'' in ⊢ (???%);
1186      |8: <fetch_refl' in ⊢ (???%);
1187      |9: <fetch_refl'' in ⊢ (???%);
1188      |10: <fetch_refl' in ⊢ (???%);
1189      |11: <fetch_refl'' in ⊢ (???%);
1190      |12: <fetch_refl' in ⊢ (???%);
1191      |13: <fetch_refl'' in ⊢ (???%);
1192      |14: <fetch_refl' in ⊢ (???%);
1193      ]
1194      whd in ⊢ (???%);
1195      [9,10:
1196      |*:
1197        /demod/
1198      ] %
1199    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1200      skip
1201    ]
1202    -status_after_1 whd in ⊢ (??%?);
1203    (* XXX: switch to the right hand side *)
1204    normalize nodelta >EQs -s >EQticks -ticks
1205    whd in ⊢ (??%%);
1206    (* XXX: finally, prove the equality using sigma commutation *)
1207    @split_eq_status try %
1208    [3,11,19,27,36,53,61:
1209      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1210      [5: >program_counter_set_program_counter ]
1211      >EQaddr_of normalize nodelta
1212      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1213      >EQcm %
1214    |7,15,23,31,45,57,65:
1215      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1216      whd in ⊢ (??%?); normalize nodelta
1217      >EQppc in fetch_many_assm; #fetch_many_assm
1218      [5:
1219        >program_counter_set_arg_1 >program_counter_set_program_counter
1220      ]
1221      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1222      <bitvector_of_nat_sign_extension_equivalence
1223      [1,3,5,7,9,11,13:
1224        whd in ⊢ (???%); cases (half_add ???) normalize //
1225      |2,4,6,8,10,12,14:
1226        @assembly1_lt_128
1227        @le_S_S @le_O_n
1228      ]
1229    |*:
1230      cases daemon
1231    ]
1232  ]
1233  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1234  (* XXX: work on the right hand side *)
1235  lapply (subaddressing_modein ???)
1236  <EQaddr normalize nodelta #irrelevant
1237  try (>p normalize nodelta)
1238  try (>p1 normalize nodelta)
1239  (* XXX: switch to the left hand side *)
1240  >EQP -P normalize nodelta
1241  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1242  whd in ⊢ (??%?);
1243  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1244  (* XXX: work on the left hand side *)
1245  [1,2,3,4,5:
1246    generalize in ⊢ (??(???(?%))?);
1247  |6,7,8,9,10,11:
1248    generalize in ⊢ (??(???(?%))?);
1249  |12:
1250    generalize in ⊢ (??(???(?%))?);
1251  ]
1252  <EQaddr normalize nodelta #irrelevant
1253  try @(jmpair_as_replace ?????????? p)
1254  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1255  (* XXX: switch to the right hand side *)
1256  normalize nodelta >EQs -s >EQticks -ticks
1257  whd in ⊢ (??%%);
1258  (* XXX: finally, prove the equality using sigma commutation *)
1259  try @split_eq_status try % whd in ⊢ (??%%);
1260  cases daemon
1261  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1262  (* XXX: work on the right hand side *)
1263  >p normalize nodelta
1264  try (>p1 normalize nodelta)
1265  (* XXX: switch to the left hand side *)
1266  -instr_refl >EQP -P normalize nodelta
1267  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1268  whd in ⊢ (??%?);
1269  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1270  (* XXX: work on the left hand side *)
1271  @(pair_replace ?????????? p)
1272  [1,3,5,7,9,11,13,15,17:
1273    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1274    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1275    cases daemon
1276  |14,16,18:
1277    normalize nodelta
1278    @(pair_replace ?????????? p1)
1279    [1,3,5:
1280      >set_clock_mk_Status_commutation
1281      cases daemon
1282    ]
1283  ]
1284  (* XXX: switch to the right hand side *)
1285  normalize nodelta >EQs -s >EQticks -ticks
1286  whd in ⊢ (??%%);
1287  (* XXX: finally, prove the equality using sigma commutation *)
1288  try @split_eq_status try %
1289  cases daemon
1290  |10,42,43,44,45,49,52,56: (* MUL *)
1291  (* XXX: work on the right hand side *)
1292  (* XXX: switch to the left hand side *)
1293  -instr_refl >EQP -P normalize nodelta
1294  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1295  whd in ⊢ (??%?);
1296  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1297  (* XXX: work on the left hand side *)
1298  (* XXX: switch to the right hand side *)
1299  normalize nodelta >EQs -s >EQticks -ticks
1300  whd in ⊢ (??%%);
1301  (* XXX: finally, prove the equality using sigma commutation *)
1302  cases daemon
1303  |11,12: (* DIV *)
1304  (* XXX: work on the right hand side *)
1305  normalize nodelta in p;
1306  >p normalize nodelta
1307  (* XXX: switch to the left hand side *)
1308  -instr_refl >EQP -P normalize nodelta
1309  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1310  whd in ⊢ (??%?);
1311  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1312  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1313  >(?: pose_assm = 0) normalize nodelta
1314  [2,4:
1315    <p >pose_refl
1316    cases daemon
1317  |1,3:
1318    (* XXX: switch to the right hand side *)
1319    >EQs -s >EQticks -ticks
1320    whd in ⊢ (??%%);
1321    (* XXX: finally, prove the equality using sigma commutation *)
1322    @split_eq_status try %
1323    cases daemon
1324  ]
1325  |13,14,15: (* DA *)
1326  (* XXX: work on the right hand side *)
1327  >p normalize nodelta
1328  >p1 normalize nodelta
1329  try (>p2 normalize nodelta
1330  try (>p3 normalize nodelta
1331  try (>p4 normalize nodelta
1332  try (>p5 normalize nodelta))))
1333  (* XXX: switch to the left hand side *)
1334  -instr_refl >EQP -P normalize nodelta
1335  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1336  whd in ⊢ (??%?);
1337  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1338  (* XXX: work on the left hand side *)
1339  @(pair_replace ?????????? p)
1340  [1,3,5:
1341    /demod/
1342    cases daemon
1343  |2,4,6:
1344    @(if_then_else_replace ???????? p1)
1345    [1,3,5:
1346      cases daemon
1347    |2,4:
1348      normalize nodelta
1349      @(pair_replace ?????????? p2)
1350      [1,3:
1351        cases daemon
1352      |2,4:
1353        normalize nodelta >p3 normalize nodelta
1354        >p4 normalize nodelta try >p5
1355      ]
1356    ]
1357  (* XXX: switch to the right hand side *)
1358  normalize nodelta >EQs -s >EQticks -ticks
1359  whd in ⊢ (??%%);
1360  (* XXX: finally, prove the equality using sigma commutation *)
1361  @split_eq_status try %
1362  cases daemon
1363  ]
1364  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1365  (* XXX: work on the right hand side *)
1366  cases addr #addr' normalize nodelta
1367  [1,3:
1368    cases addr' #addr'' normalize nodelta
1369  ]
1370  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1371  (* XXX: switch to the left hand side *)
1372  -instr_refl >EQP -P normalize nodelta
1373  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1374  whd in ⊢ (??%?);
1375  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1376  (* XXX: work on the left hand side *)
1377  (* XXX: switch to the right hand side *)
1378  normalize nodelta >EQs -s >EQticks -ticks
1379  whd in ⊢ (??%%);
1380  (* XXX: finally, prove the equality using sigma commutation *)
1381  cases daemon
1382  |47: (* MOV *)
1383  (* XXX: work on the right hand side *)
1384  cases addr -addr #addr normalize nodelta
1385  [1:
1386    cases addr #addr normalize nodelta
1387    [1:
1388      cases addr #addr normalize nodelta
1389      [1:
1390        cases addr #addr normalize nodelta
1391        [1:
1392          cases addr #addr normalize nodelta
1393        ]
1394      ]
1395    ]
1396  ]
1397  cases addr #lft #rgt normalize nodelta
1398  (* XXX: switch to the left hand side *)
1399  >EQP -P normalize nodelta
1400  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1401  whd in ⊢ (??%?);
1402  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1403  (* XXX: work on the left hand side *)
1404  (* XXX: switch to the right hand side *)
1405  normalize nodelta >EQs -s >EQticks -ticks
1406  whd in ⊢ (??%%);
1407  (* XXX: finally, prove the equality using sigma commutation *)
1408  cases daemon
1409  ]
1410qed.
1411*)
Note: See TracBrowser for help on using the repository browser.