source: src/ASM/AssemblyProofSplit.ma @ 2023

Last change on this file since 2023 was 2023, checked in by mulligan, 7 years ago

Closed main lemma modulo closing trivial subgoals about commutations and addressing modes being in vectors of addressing modes.

File size: 80.7 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 … [[dptr]] … [[dptr]]) [1: // ]
26  cases (split 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 (split 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 … [[bit_addr; carry]] … [[bit_addr; carry]]) [1: // ]
118  [1:
119    #byte cases (split ????) #nu #nl normalize nodelta
120    cases (split ????) #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 (split ????) //
129  ]
130qed.
131
132lemma get_ov_flag_set_program_counter:
133  ∀M: Type[0].
134  ∀cm: M.
135  ∀s: PreStatus M cm.
136  ∀pc: Word.
137    get_ov_flag M cm (set_program_counter M cm s pc) =
138      get_ov_flag M cm s.
139  #M #cm #s #pc %
140qed.
141
142lemma external_ram_set_program_counter:
143  ∀M: Type[0].
144  ∀cm: M.
145  ∀s: PreStatus M cm.
146  ∀pc: Word.
147    external_ram M cm (set_program_counter M cm s pc) =
148      external_ram M cm s.
149  #M #cm #s #pc %
150qed.
151
152lemma low_internal_ram_set_program_counter:
153  ∀M: Type[0].
154  ∀cm: M.
155  ∀s: PreStatus M cm.
156  ∀pc: Word.
157    low_internal_ram M cm (set_program_counter M cm s pc) =
158      low_internal_ram M cm s.
159  #M #cm #s #pc %
160qed.
161
162lemma high_internal_ram_set_program_counter:
163  ∀M: Type[0].
164  ∀cm: M.
165  ∀s: PreStatus M cm.
166  ∀pc: Word.
167    high_internal_ram M cm (set_program_counter M cm s pc) =
168      high_internal_ram M cm s.
169  #M #cm #s #pc %
170qed.
171
172lemma get_arg_8_set_program_counter:
173  ∀M: Type[0].
174  ∀cm: M.
175  ∀s: PreStatus M cm.
176  ∀flag: bool.
177  ∀addr.
178  ∀pc: Word.
179    get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
180      get_arg_8 M cm s flag addr.
181  #M #cm #s #flag #addr #pc
182  whd in match get_arg_8; normalize nodelta
183  cases addr *
184  try (#addr1 #addr2 #absurd normalize in absurd; cases absurd @I)
185  try (#addr1 #absurd normalize in absurd; cases absurd @I)
186  try (#absurd normalize in absurd; cases absurd @I)
187  try (#addr1 #addr2) try #addr1
188  normalize nodelta try %
189  >external_ram_set_program_counter
190  >program_counter_set_program_counter
191  cases daemon (* XXX: rewrite not working but provable *)
192qed.
193
194lemma external_ram_set_flags:
195  ∀M: Type[0].
196  ∀cm: M.
197  ∀s: PreStatus M cm.
198  ∀opt: option Bit.
199  ∀bit1, bit2: Bit.
200    external_ram M cm (set_flags M cm s bit1 opt bit2) =
201      external_ram M cm s.
202  #M #cm #s #opt #bit1 #bit2 %
203qed.
204
205lemma low_internal_ram_set_flags:
206  ∀M: Type[0].
207  ∀cm: M.
208  ∀s: PreStatus M cm.
209  ∀opt: option Bit.
210  ∀bit1, bit2: Bit.
211    low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
212      low_internal_ram M cm s.
213  #M #cm #s #opt #bit1 #bit2 %
214qed.
215
216lemma high_internal_ram_set_flags:
217  ∀M: Type[0].
218  ∀cm: M.
219  ∀s: PreStatus M cm.
220  ∀opt: option Bit.
221  ∀bit1, bit2: Bit.
222    high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
223      high_internal_ram M cm s.
224  #M #cm #s #opt #bit1 #bit2 %
225qed.
226
227lemma low_internal_ram_set_clock:
228  ∀M: Type[0].
229  ∀cm: M.
230  ∀s: PreStatus M cm.
231  ∀t: Time.
232    low_internal_ram M cm (set_clock M cm s t) =
233      low_internal_ram M cm s.
234  #M #cm #s #t %
235qed.
236
237lemma high_internal_ram_set_clock:
238  ∀M: Type[0].
239  ∀cm: M.
240  ∀s: PreStatus M cm.
241  ∀t: Time.
242    high_internal_ram M cm (set_clock M cm s t) =
243      high_internal_ram M cm s.
244  #M #cm #s #t %
245qed.
246
247lemma external_ram_set_clock:
248  ∀M: Type[0].
249  ∀cm: M.
250  ∀s: PreStatus M cm.
251  ∀t: Time.
252    external_ram M cm (set_clock M cm s t) =
253      external_ram M cm s.
254  #M #cm #s #t %
255qed.
256
257lemma set_8051_sfr_set_program_counter:
258  ∀M: Type[0].
259  ∀cm: M.
260  ∀s: PreStatus M cm.
261  ∀pc: Word.
262  ∀sfr: SFR8051.
263  ∀v: Byte.
264    set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
265      set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
266  #M #cm #s #pc #sfr #v %
267qed.
268
269lemma low_internal_ram_set_8051_sfr:
270  ∀M: Type[0].
271  ∀cm: M.
272  ∀s: PreStatus M cm.
273  ∀sfr: SFR8051.
274  ∀v: Byte.
275    low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
276      low_internal_ram M cm s.
277  #M #cm #s #sfr #v %
278qed.
279
280lemma high_internal_ram_set_8051_sfr:
281  ∀M: Type[0].
282  ∀cm: M.
283  ∀s: PreStatus M cm.
284  ∀sfr: SFR8051.
285  ∀v: Byte.
286    high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
287      high_internal_ram M cm s.
288  #M #cm #s #sfr #v %
289qed.
290
291lemma external_ram_set_8051_sfr:
292  ∀M: Type[0].
293  ∀cm: M.
294  ∀s: PreStatus M cm.
295  ∀sfr: SFR8051.
296  ∀v: Byte.
297    external_ram M cm (set_8051_sfr M cm s sfr v) =
298      external_ram M cm s.
299  #M #cm #s #sfr #v %
300qed.
301
302lemma get_arg_8_set_clock:
303  ∀M: Type[0].
304  ∀cm: M.
305  ∀s: PreStatus M cm.
306  ∀addr.
307  ∀t: Time.
308    get_arg_8 M cm (set_clock M cm s t) addr =
309      get_arg_8 M cm s addr.
310  #M #cm #s #addr #t %
311qed.
312
313lemma set_program_counter_set_program_counter:
314  ∀M: Type[0].
315  ∀cm: M.
316  ∀s: PreStatus M cm.
317  ∀pc: Word.
318  ∀pc': Word.
319    set_program_counter M cm (set_program_counter M cm s pc) pc' =
320      set_program_counter M cm s pc'.
321  #M #cm #s #pc #pc' %
322qed.
323
324lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
325 #P #A #a #abs destruct
326qed.
327
328(*
329lemma pi1_let_commute:
330 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
331 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
332 #A #B #C #P * #a #b * //
333qed.
334
335lemma pi1_let_as_commute:
336 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
337 pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
338  (let 〈x1,y1〉 as H ≝ c in pi1 … t).
339 #A #B #C #P * #a #b * //
340qed.
341
342lemma tech_pi1_let_as_commute:
343 ∀A,B,C,P. ∀f. ∀c,c':A × B.
344 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
345 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
346  c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
347  pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
348   f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
349 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
350qed.
351*)
352
353include alias "arithmetics/nat.ma".
354include alias "basics/logic.ma".
355include alias "ASM/BitVectorTrie.ma".
356
357lemma pair_replace:
358 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
359  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
360 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
361qed.
362
363lemma jmpair_as_replace:
364 ∀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.
365  ∀EQ:c ≃ 〈a,b〉.
366  P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
367  [2:
368    >EQc @EQ
369  |1:
370    #A #B #T #P #a #b
371    #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
372    letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
373    change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
374    @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
375    -EQ cases c in f; normalize //
376  ]
377qed.
378
379lemma if_then_else_replace:
380  ∀T: Type[0].
381  ∀P: T → Prop.
382  ∀t1, t2: T.
383  ∀c, c', c'': bool.
384    c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
385  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
386  assumption
387qed.
388
389lemma fetch_many_singleton:
390  ∀code_memory: BitVectorTrie Byte 16.
391  ∀final_pc, start_pc: Word.
392  ∀i: instruction.
393    fetch_many code_memory final_pc start_pc [i] →
394      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
395  #code_memory #final_pc #start_pc #i * #new_pc
396  #fetch_many_assm whd in fetch_many_assm;
397  cases (eq_bv_eq … fetch_many_assm) assumption
398qed.
399
400lemma refl_to_jmrefl:
401  ∀a: Type[0].
402  ∀l, r: a.
403    l = r → l ≃ r.
404  #a #l #r #refl destruct %
405qed.
406
407include alias "ASM/Vector.ma".
408
409lemma main_lemma_preinstruction:
410  ∀M, M': internal_pseudo_address_map.
411  ∀preamble: preamble.
412  ∀instr_list: list labelled_instruction.
413  ∀cm: pseudo_assembly_program.
414  ∀EQcm: cm = 〈preamble, instr_list〉.
415  ∀sigma: Word → Word.
416  ∀policy: Word → bool.
417  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
418  ∀ps: PseudoStatus cm.
419  ∀ppc: Word.
420  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
421  ∀labels: label_map.
422  ∀costs: BitVectorTrie costlabel 16.
423  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
424  ∀newppc: Word.
425  ∀lookup_labels: Identifier → Word.
426  ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
427  ∀lookup_datalabels: Identifier → Word.
428  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
429  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
430  ∀instr: preinstruction Identifier.
431  ∀ticks: nat × nat.
432  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
433  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
434  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
435  ∀s: PreStatus pseudo_assembly_program cm.
436  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
437  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
438  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
439              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
440                  lookup_datalabels (Instruction instr)))) →
441              next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
442                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))
443                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
444                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
445                      status_of_pseudo_status M' cm s sigma policy).
446    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
447  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
448  #costs #create_label_cost_refl #newppc
449  #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
450  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
451  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
452  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
453  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
454  [2: * // ]
455  @(
456  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
457  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
458  match instr in preinstruction return λx. x = instr → Σs'.? with
459        [ ADD addr1 addr2 ⇒ λinstr_refl.
460            let s ≝ add_ticks1 s in
461            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
462                                                   (get_arg_8 … s false addr2) false in
463            let cy_flag ≝ get_index' ? O  ? flags in
464            let ac_flag ≝ get_index' ? 1 ? flags in
465            let ov_flag ≝ get_index' ? 2 ? flags in
466            let s ≝ set_arg_8 … s ACC_A result in
467              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
468        | ADDC addr1 addr2 ⇒ λinstr_refl.
469            let s ≝ add_ticks1 s in
470            let old_cy_flag ≝ get_cy_flag ?? s in
471            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
472                                                   (get_arg_8 … s false addr2) old_cy_flag 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        | SUBB 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〉 ≝ sub_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        | ANL addr ⇒ λinstr_refl.
489          let s ≝ add_ticks1 s in
490          match addr with
491            [ inl l ⇒
492              match l with
493                [ inl l' ⇒
494                  let 〈addr1, addr2〉 ≝ l' in
495                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
496                    set_arg_8 … s addr1 and_val
497                | inr r ⇒
498                  let 〈addr1, addr2〉 ≝ r in
499                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
500                    set_arg_8 … s addr1 and_val
501                ]
502            | inr r ⇒
503              let 〈addr1, addr2〉 ≝ r in
504              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
505               set_flags … s and_val (None ?) (get_ov_flag ?? s)
506            ]
507        | ORL addr ⇒ λinstr_refl.
508          let s ≝ add_ticks1 s in
509          match addr with
510            [ inl l ⇒
511              match l with
512                [ inl l' ⇒
513                  let 〈addr1, addr2〉 ≝ l' in
514                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
515                    set_arg_8 … s addr1 or_val
516                | inr r ⇒
517                  let 〈addr1, addr2〉 ≝ r in
518                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
519                    set_arg_8 … s addr1 or_val
520                ]
521            | inr r ⇒
522              let 〈addr1, addr2〉 ≝ r in
523              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
524               set_flags … s or_val (None ?) (get_ov_flag … s)
525            ]
526        | XRL addr ⇒ λinstr_refl.
527          let s ≝ add_ticks1 s in
528          match addr with
529            [ inl l' ⇒
530              let 〈addr1, addr2〉 ≝ l' in
531              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
532                set_arg_8 … s addr1 xor_val
533            | inr r ⇒
534              let 〈addr1, addr2〉 ≝ r in
535              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
536                set_arg_8 … s addr1 xor_val
537            ]
538        | INC addr ⇒ λinstr_refl.
539            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
540              [ ACC_A ⇒ λacc_a: True. λEQaddr.
541                let s' ≝ add_ticks1 s in
542                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
543                 set_arg_8 … s' ACC_A result
544              | REGISTER r ⇒ λregister: True. λEQaddr.
545                let s' ≝ add_ticks1 s in
546                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
547                 set_arg_8 … s' (REGISTER r) result
548              | DIRECT d ⇒ λdirect: True. λEQaddr.
549                let s' ≝ add_ticks1 s in
550                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
551                 set_arg_8 … s' (DIRECT d) result
552              | INDIRECT i ⇒ λindirect: True. λEQaddr.
553                let s' ≝ add_ticks1 s in
554                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
555                 set_arg_8 … s' (INDIRECT i) result
556              | DPTR ⇒ λdptr: True. λEQaddr.
557                let s' ≝ add_ticks1 s in
558                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
559                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
560                let s ≝ set_8051_sfr … s' SFR_DPL bl in
561                 set_8051_sfr … s' SFR_DPH bu
562              | _ ⇒ λother: False. ⊥
563              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
564        | NOP ⇒ λinstr_refl.
565           let s ≝ add_ticks2 s in
566            s
567        | DEC addr ⇒ λinstr_refl.
568           let s ≝ add_ticks1 s in
569           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
570             set_arg_8 … s addr result
571        | MUL addr1 addr2 ⇒ λinstr_refl.
572           let s ≝ add_ticks1 s in
573           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
574           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
575           let product ≝ acc_a_nat * acc_b_nat in
576           let ov_flag ≝ product ≥ 256 in
577           let low ≝ bitvector_of_nat 8 (product mod 256) in
578           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
579           let s ≝ set_8051_sfr … s SFR_ACC_A low in
580             set_8051_sfr … s SFR_ACC_B high
581        | DIV 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             match acc_b_nat with
586               [ O ⇒ set_flags … s false (None Bit) true
587               | S o ⇒
588                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
589                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
590                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
591                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
592                   set_flags … s false (None Bit) false
593               ]
594        | DA addr ⇒ λinstr_refl.
595            let s ≝ add_ticks1 s in
596            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
597              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
598                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
599                let cy_flag ≝ get_index' ? O ? flags in
600                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
601                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
602                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
603                    let new_acc ≝ nu @@ acc_nl' in
604                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
605                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
606                  else
607                    s
608              else
609                s
610        | CLR addr ⇒ λinstr_refl.
611          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
612            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
613              let s ≝ add_ticks1 s in
614               set_arg_8 … s ACC_A (zero 8)
615            | CARRY ⇒ λcarry: True.  λEQaddr.
616              let s ≝ add_ticks1 s in
617               set_arg_1 … s CARRY false
618            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
619              let s ≝ add_ticks1 s in
620               set_arg_1 … s (BIT_ADDR b) false
621            | _ ⇒ λother: False. ⊥
622            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
623        | CPL addr ⇒ λinstr_refl.
624          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
625            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
626                let s ≝ add_ticks1 s in
627                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
628                let new_acc ≝ negation_bv ? old_acc in
629                 set_8051_sfr … s SFR_ACC_A new_acc
630            | CARRY ⇒ λcarry: True. λEQaddr.
631                let s ≝ add_ticks1 s in
632                let old_cy_flag ≝ get_arg_1 … s CARRY true in
633                let new_cy_flag ≝ ¬old_cy_flag in
634                 set_arg_1 … s CARRY new_cy_flag
635            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
636                let s ≝ add_ticks1 s in
637                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
638                let new_bit ≝ ¬old_bit in
639                 set_arg_1 … s (BIT_ADDR b) new_bit
640            | _ ⇒ λother: False. ?
641            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
642        | SETB b ⇒ λinstr_refl.
643            let s ≝ add_ticks1 s in
644            set_arg_1 … s b false
645        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
646            let s ≝ add_ticks1 s in
647            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
648            let new_acc ≝ rotate_left … 1 old_acc in
649              set_8051_sfr … s SFR_ACC_A new_acc
650        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
651            let s ≝ add_ticks1 s in
652            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
653            let new_acc ≝ rotate_right … 1 old_acc in
654              set_8051_sfr … s SFR_ACC_A new_acc
655        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
656            let s ≝ add_ticks1 s in
657            let old_cy_flag ≝ get_cy_flag ?? s in
658            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
659            let new_cy_flag ≝ get_index' ? O ? old_acc in
660            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
661            let s ≝ set_arg_1 … s CARRY new_cy_flag in
662              set_8051_sfr … s SFR_ACC_A new_acc
663        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
664            let s ≝ add_ticks1 s in
665            let old_cy_flag ≝ get_cy_flag ?? s in
666            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
667            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
668            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
669            let s ≝ set_arg_1 … s CARRY new_cy_flag in
670              set_8051_sfr … s SFR_ACC_A new_acc
671        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
672            let s ≝ add_ticks1 s in
673            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
674            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
675            let new_acc ≝ nl @@ nu in
676              set_8051_sfr … s SFR_ACC_A new_acc
677        | PUSH addr ⇒ λinstr_refl.
678            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
679              [ DIRECT d ⇒ λdirect: True. λEQaddr.
680                let s ≝ add_ticks1 s in
681                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
682                let s ≝ set_8051_sfr … s SFR_SP new_sp in
683                  write_at_stack_pointer … s d
684              | _ ⇒ λother: False. ⊥
685              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
686        | POP addr ⇒ λinstr_refl.
687            let s ≝ add_ticks1 s in
688            let contents ≝ read_at_stack_pointer ?? s in
689            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
690            let s ≝ set_8051_sfr … s SFR_SP new_sp in
691              set_arg_8 … s addr contents
692        | XCH addr1 addr2 ⇒ λinstr_refl.
693            let s ≝ add_ticks1 s in
694            let old_addr ≝ get_arg_8 … s false addr2 in
695            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
696            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
697              set_arg_8 … s addr2 old_acc
698        | XCHD addr1 addr2 ⇒ λinstr_refl.
699            let s ≝ add_ticks1 s in
700            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
701            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
702            let new_acc ≝ acc_nu @@ arg_nl in
703            let new_arg ≝ arg_nu @@ acc_nl in
704            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
705              set_arg_8 … s addr2 new_arg
706        | RET ⇒ λinstr_refl.
707            let s ≝ add_ticks1 s in
708            let high_bits ≝ read_at_stack_pointer ?? s in
709            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
710            let s ≝ set_8051_sfr … s SFR_SP new_sp in
711            let low_bits ≝ read_at_stack_pointer ?? s in
712            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
713            let s ≝ set_8051_sfr … s SFR_SP new_sp in
714            let new_pc ≝ high_bits @@ low_bits in
715              set_program_counter … s new_pc
716        | RETI ⇒ λ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        | MOVX addr ⇒ λinstr_refl.
727          let s ≝ add_ticks1 s in
728          (* DPM: only copies --- doesn't affect I/O *)
729          match addr with
730            [ inl l ⇒
731              let 〈addr1, addr2〉 ≝ l in
732                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
733            | inr r ⇒
734              let 〈addr1, addr2〉 ≝ r in
735                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
736            ]
737        | MOV addr ⇒ λinstr_refl.
738          let s ≝ add_ticks1 s in
739          match addr with
740            [ inl l ⇒
741              match l with
742                [ inl l' ⇒
743                  match l' with
744                    [ inl l'' ⇒
745                      match l'' with
746                        [ inl l''' ⇒
747                          match l''' with
748                            [ inl l'''' ⇒
749                              let 〈addr1, addr2〉 ≝ l'''' in
750                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
751                            | inr r'''' ⇒
752                              let 〈addr1, addr2〉 ≝ r'''' in
753                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
754                            ]
755                        | inr r''' ⇒
756                          let 〈addr1, addr2〉 ≝ r''' in
757                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
758                        ]
759                    | inr r'' ⇒
760                      let 〈addr1, addr2〉 ≝ r'' in
761                       set_arg_16 … s (get_arg_16 … s addr2) addr1
762                    ]
763                | inr r ⇒
764                  let 〈addr1, addr2〉 ≝ r in
765                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
766                ]
767            | inr r ⇒
768              let 〈addr1, addr2〉 ≝ r in
769               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
770            ]
771          | JC addr ⇒ λinstr_refl.
772                  if get_cy_flag ?? s then
773                    let s ≝ add_ticks1 s in
774                      set_program_counter … s (addr_of addr s)
775                  else
776                    let s ≝ add_ticks2 s in
777                      s
778            | JNC addr ⇒ λinstr_refl.
779                  if ¬(get_cy_flag ?? s) then
780                   let s ≝ add_ticks1 s in
781                     set_program_counter … s (addr_of addr s)
782                  else
783                   let s ≝ add_ticks2 s in
784                    s
785            | JB addr1 addr2 ⇒ λinstr_refl.
786                  if get_arg_1 … s addr1 false then
787                   let s ≝ add_ticks1 s in
788                    set_program_counter … s (addr_of addr2 s)
789                  else
790                   let s ≝ add_ticks2 s in
791                    s
792            | JNB addr1 addr2 ⇒ λinstr_refl.
793                  if ¬(get_arg_1 … s addr1 false) then
794                   let s ≝ add_ticks1 s in
795                    set_program_counter … s (addr_of addr2 s)
796                  else
797                   let s ≝ add_ticks2 s in
798                    s
799            | JBC addr1 addr2 ⇒ λinstr_refl.
800                  let s ≝ set_arg_1 … s addr1 false in
801                    if get_arg_1 … s addr1 false then
802                     let s ≝ add_ticks1 s in
803                      set_program_counter … s (addr_of addr2 s)
804                    else
805                     let s ≝ add_ticks2 s in
806                      s
807            | JZ addr ⇒ λinstr_refl.
808                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
809                     let s ≝ add_ticks1 s in
810                      set_program_counter … s (addr_of addr s)
811                    else
812                     let s ≝ add_ticks2 s in
813                      s
814            | JNZ addr ⇒ λinstr_refl.
815                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
816                     let s ≝ add_ticks1 s in
817                      set_program_counter … s (addr_of addr s)
818                    else
819                     let s ≝ add_ticks2 s in
820                      s
821            | CJNE addr1 addr2 ⇒ λinstr_refl.
822                  match addr1 with
823                    [ inl l ⇒
824                        let 〈addr1, addr2'〉 ≝ l in
825                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
826                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
827                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
828                            let s ≝ add_ticks1 s in
829                            let s ≝ set_program_counter … s (addr_of addr2 s) in
830                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
831                          else
832                            let s ≝ add_ticks2 s in
833                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
834                    | inr r' ⇒
835                        let 〈addr1, addr2'〉 ≝ r' in
836                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
837                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
838                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
839                            let s ≝ add_ticks1 s in
840                            let s ≝ set_program_counter … s (addr_of addr2 s) in
841                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
842                          else
843                            let s ≝ add_ticks2 s in
844                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
845                    ]
846            | DJNZ addr1 addr2 ⇒ λinstr_refl.
847              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
848              let s ≝ set_arg_8 … s addr1 result in
849                if ¬(eq_bv ? result (zero 8)) then
850                 let s ≝ add_ticks1 s in
851                  set_program_counter … s (addr_of addr2 s)
852                else
853                 let s ≝ add_ticks2 s in
854                  s
855           ] (refl … instr))
856  try (cases(other))
857  try assumption (*20s*)
858  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
859  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
860  whd in match execute_1_preinstruction; normalize nodelta
861  [31,32: (* DJNZ *)
862  (* XXX: work on the right hand side *)
863  >p normalize nodelta
864  (* XXX: switch to the left hand side *)
865  -instr_refl >EQP -P normalize nodelta
866  #sigma_increment_commutation #maps_assm #fetch_many_assm
867  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
868  whd in match (expand_relative_jump ????);
869  <EQppc in fetch_many_assm;
870  @pair_elim #result #flags #sub16_refl
871  @pair_elim #upper #lower #split_refl
872  cases (eq_bv ???) normalize nodelta
873  [1,3:
874    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
875    whd in ⊢ (??%?);
876    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
877    (* XXX: work on the left hand side *)
878    @(pair_replace ?????????? p) normalize nodelta
879    [1,3:
880      cases daemon
881    ]
882    (* XXX: switch to the right hand side *)
883    normalize nodelta >EQs -s >EQticks -ticks
884    cases (¬ eq_bv ???) normalize nodelta
885    whd in ⊢ (??%%);
886    (* XXX: finally, prove the equality using sigma commutation *)
887    @split_eq_status try %
888    cases daemon
889  |2,4:
890    >EQppc
891    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
892    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
893    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
894    #fetch_many_assm whd in fetch_many_assm; %{2}
895    change with (execute_1 ?? = ?)
896    @(pose … (execute_1 ? (status_of_pseudo_status …)))
897    #status_after_1 #EQstatus_after_1
898    <(?: ? = status_after_1)
899    [3,6:
900      >EQstatus_after_1 in ⊢ (???%);
901      whd in ⊢ (???%);
902      [1:
903        <fetch_refl in ⊢ (???%);
904      |2:
905        <fetch_refl in ⊢ (???%);
906      ]
907      whd in ⊢ (???%);
908      @(pair_replace ?????????? p)
909      [1,3:
910        cases daemon
911      |2,4:
912        normalize nodelta
913        whd in match (addr_of_relative ????);
914        cases (¬ eq_bv ???) normalize nodelta
915        >set_clock_mk_Status_commutation
916        whd in ⊢ (???%);
917        change with (add ???) in match (\snd (half_add ???));
918        >set_arg_8_set_program_counter in ⊢ (???%);
919        [2,4,6,8: cases daemon ]
920        >program_counter_set_program_counter in ⊢ (???%);
921        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
922        [2,4,6,8:
923          >bitvector_of_nat_sign_extension_equivalence
924          [1,3,5,7:
925            >EQintermediate_pc' %
926          |*:
927            repeat @le_S_S @le_O_n
928          ]
929        ]
930        [1,3: % ]
931      ]
932    |1,4:
933      skip
934    ]
935    [3,4:
936      -status_after_1
937      @(pose … (execute_1 ? (mk_PreStatus …)))
938      #status_after_1 #EQstatus_after_1
939      <(?: ? = status_after_1)
940      [3,6:
941        >EQstatus_after_1 in ⊢ (???%);
942        whd in ⊢ (???%);
943        (* XXX: matita bug with patterns across multiple goals *)
944        [1:
945          <fetch_refl'' in ⊢ (???%);
946        |2:
947          <fetch_refl'' in ⊢ (???%);
948        ]
949        [2: % |1: whd in ⊢ (???%); % ]
950      |1,4:
951        skip
952      ]
953      -status_after_1 whd in ⊢ (??%?);
954      (* XXX: switch to the right hand side *)
955      normalize nodelta >EQs -s >EQticks -ticks
956      cases (¬ eq_bv ???) normalize nodelta
957      whd in ⊢ (??%%);
958    ]
959    (* XXX: finally, prove the equality using sigma commutation *)
960    @split_eq_status try %
961    whd in ⊢ (??%%);
962    cases daemon
963  ]
964  |30: (* CJNE *)
965  (* XXX: work on the right hand side *)
966  cases addr1 -addr1 #addr1 normalize nodelta
967  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
968  (* XXX: switch to the left hand side *)
969  >EQP -P normalize nodelta
970  #sigma_increment_commutation #maps_assm #fetch_many_assm
971
972  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
973  whd in match (expand_relative_jump ????);
974  <EQppc in fetch_many_assm;
975  @pair_elim #result #flags #sub16_refl
976  @pair_elim #upper #lower #split_refl
977  inversion (eq_bv ???) #upper_split_refl normalize nodelta
978  [1,3:
979    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
980    whd in ⊢ (??%?);
981    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
982    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
983    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
984    @(if_then_else_replace ???????? eq_bv_refl)
985    [1,3,5,7:
986      cases daemon
987    |2,4,6,8:
988      (* XXX: switch to the right hand side *)
989      normalize nodelta >EQs -s >EQticks -ticks
990      whd in ⊢ (??%%);
991      (* XXX: finally, prove the equality using sigma commutation *)
992      @split_eq_status try %
993      [3,7,11,15:
994        whd in ⊢ (??%?);
995        [1,3:
996          cases daemon
997        |2,4:
998          cases daemon
999        ]
1000      ]
1001      cases daemon (* XXX *)
1002    ]
1003  |2,4:
1004    >EQppc
1005    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1006    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1007    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1008    #fetch_many_assm whd in fetch_many_assm; %{2}
1009    change with (execute_1 ?? = ?)
1010    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1011    #status_after_1 #EQstatus_after_1
1012    <(?: ? = status_after_1)
1013    [2,5:
1014      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
1015    |3,6:
1016      >EQstatus_after_1 in ⊢ (???%);
1017      whd in ⊢ (???%);
1018      [1: <fetch_refl in ⊢ (???%);
1019      |2: <fetch_refl in ⊢ (???%);
1020      ]
1021      whd in ⊢ (???%);
1022      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
1023      whd in ⊢ (???%);
1024      whd in match (addr_of_relative ????);
1025      change with (add ???) in match (\snd (half_add ???));
1026      >set_clock_set_program_counter in ⊢ (???%);
1027      >program_counter_set_program_counter in ⊢ (???%);
1028      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1029      [2,4,6,8:
1030        >bitvector_of_nat_sign_extension_equivalence
1031        [1,3,5,7:
1032          >EQintermediate_pc' %
1033        |*:
1034          repeat @le_S_S @le_O_n
1035        ]
1036      |1,5:
1037        %
1038      ]
1039    |1,4: skip
1040    ]
1041    [1,2,3,4:
1042      -status_after_1
1043      @(pose … (execute_1 ? (mk_PreStatus …)))
1044      #status_after_1 #EQstatus_after_1
1045      <(?: ? = status_after_1)
1046      [3,6,9,12:
1047        >EQstatus_after_1 in ⊢ (???%);
1048        whd in ⊢ (???%);
1049        (* XXX: matita bug with patterns across multiple goals *)
1050        [1: <fetch_refl'' in ⊢ (???%);
1051        |2: <fetch_refl'' in ⊢ (???%);
1052        |3: <fetch_refl'' in ⊢ (???%);
1053        |4: <fetch_refl'' in ⊢ (???%);
1054        ] %
1055      |1,4,7,10:
1056        skip
1057      ]
1058      -status_after_1 whd in ⊢ (??%?);
1059      (* XXX: switch to the right hand side *)
1060      normalize nodelta >EQs -s >EQticks -ticks
1061      whd in ⊢ (??%%);
1062    ]
1063    (* XXX: finally, prove the equality using sigma commutation *)
1064    @split_eq_status try %
1065    cases daemon
1066  ]
1067  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
1068  (* XXX: work on the right hand side *)
1069  >p normalize nodelta
1070  (* XXX: switch to the left hand side *)
1071  -instr_refl >EQP -P normalize nodelta
1072  #sigma_increment_commutation #maps_assm #fetch_many_assm
1073 
1074  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1075  whd in match (expand_relative_jump ????);
1076  <EQppc in fetch_many_assm;
1077  @pair_elim #result #flags #sub16_refl
1078  @pair_elim #upper #lower #split_refl
1079  cases (eq_bv ???) normalize nodelta
1080  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1081    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
1082    whd in ⊢ (??%?);
1083    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1084    (* XXX: work on the left hand side *)
1085    @(if_then_else_replace ???????? p) normalize nodelta
1086    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1087      cases daemon
1088    ]
1089    (* XXX: switch to the right hand side *)
1090    normalize nodelta >EQs -s >EQticks -ticks
1091    whd in ⊢ (??%%);
1092    (* XXX: finally, prove the equality using sigma commutation *)
1093    @split_eq_status try %
1094    cases daemon
1095  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1096    >EQppc
1097    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
1098    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
1099    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
1100    #fetch_many_assm whd in fetch_many_assm; %{2}
1101    change with (execute_1 ?? = ?)
1102    @(pose … (execute_1 ? (status_of_pseudo_status …)))
1103    #status_after_1 #EQstatus_after_1
1104    <(?: ? = status_after_1)
1105    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1106      >EQstatus_after_1 in ⊢ (???%);
1107      whd in ⊢ (???%);
1108      [1: <fetch_refl in ⊢ (???%);
1109      |2: <fetch_refl in ⊢ (???%);
1110      |3: <fetch_refl in ⊢ (???%);
1111      |4: <fetch_refl in ⊢ (???%);
1112      |5: <fetch_refl in ⊢ (???%);
1113      |6: <fetch_refl in ⊢ (???%);
1114      |7: <fetch_refl in ⊢ (???%);
1115      |8: <fetch_refl in ⊢ (???%);
1116      |9: <fetch_refl in ⊢ (???%);
1117      |10: <fetch_refl in ⊢ (???%);
1118      |11: <fetch_refl in ⊢ (???%);
1119      |12: <fetch_refl in ⊢ (???%);
1120      |13: <fetch_refl in ⊢ (???%);
1121      |14: <fetch_refl in ⊢ (???%);
1122      ]
1123      whd in ⊢ (???%);
1124      @(if_then_else_replace ???????? p)
1125      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1126        cases daemon
1127      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1128        normalize nodelta
1129        whd in match (addr_of_relative ????);
1130        >set_clock_mk_Status_commutation
1131        [9,10:
1132          (* XXX: demodulation not working in this case *)
1133          >program_counter_set_arg_1 in ⊢ (???%);
1134          >program_counter_set_program_counter in ⊢ (???%);
1135        |*:
1136          /demod/
1137        ]
1138        whd in ⊢ (???%);
1139        change with (add ???) in match (\snd (half_add ???));
1140        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
1141        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
1142          >bitvector_of_nat_sign_extension_equivalence
1143          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
1144            >EQintermediate_pc' %
1145          |*:
1146            repeat @le_S_S @le_O_n
1147          ]
1148        ]
1149        %
1150      ]
1151    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1152      skip
1153    ]
1154    -status_after_1
1155    @(pose … (execute_1 ? (mk_PreStatus …)))
1156    #status_after_1 #EQstatus_after_1
1157    <(?: ? = status_after_1)
1158    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
1159      >EQstatus_after_1 in ⊢ (???%);
1160      whd in ⊢ (???%);
1161      (* XXX: matita bug with patterns across multiple goals *)
1162      [1: <fetch_refl'' in ⊢ (???%);
1163      |2: <fetch_refl' in ⊢ (???%);
1164      |3: <fetch_refl'' in ⊢ (???%);
1165      |4: <fetch_refl' in ⊢ (???%);
1166      |5: <fetch_refl'' in ⊢ (???%);
1167      |6: <fetch_refl' in ⊢ (???%);
1168      |7: <fetch_refl'' in ⊢ (???%);
1169      |8: <fetch_refl' in ⊢ (???%);
1170      |9: <fetch_refl'' in ⊢ (???%);
1171      |10: <fetch_refl' in ⊢ (???%);
1172      |11: <fetch_refl'' in ⊢ (???%);
1173      |12: <fetch_refl' in ⊢ (???%);
1174      |13: <fetch_refl'' in ⊢ (???%);
1175      |14: <fetch_refl' in ⊢ (???%);
1176      ]
1177      whd in ⊢ (???%);
1178      [9,10:
1179      |*:
1180        /demod/
1181      ] %
1182    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
1183      skip
1184    ]
1185    -status_after_1 whd in ⊢ (??%?);
1186    (* XXX: switch to the right hand side *)
1187    normalize nodelta >EQs -s >EQticks -ticks
1188    whd in ⊢ (??%%);
1189    (* XXX: finally, prove the equality using sigma commutation *)
1190    @split_eq_status try %
1191    [3,11,19,27,36,53,61:
1192      >program_counter_set_program_counter >set_clock_mk_Status_commutation
1193      [5: >program_counter_set_program_counter ]
1194      >EQaddr_of normalize nodelta
1195      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
1196      >EQcm %
1197    |7,15,23,31,45,57,65:
1198      >set_clock_mk_Status_commutation >program_counter_set_program_counter
1199      whd in ⊢ (??%?); normalize nodelta
1200      >EQppc in fetch_many_assm; #fetch_many_assm
1201      [5:
1202        >program_counter_set_arg_1 >program_counter_set_program_counter
1203      ]
1204      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1205      <bitvector_of_nat_sign_extension_equivalence
1206      [1,3,5,7,9,11,13:
1207        whd in ⊢ (???%); cases (half_add ???) normalize //
1208      |2,4,6,8,10,12,14:
1209        @assembly1_lt_128
1210        @le_S_S @le_O_n
1211      ]
1212    |*:
1213      cases daemon
1214    ]
1215  ]
1216  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1217  (* XXX: work on the right hand side *)
1218  lapply (subaddressing_modein ???)
1219  <EQaddr normalize nodelta #irrelevant
1220  try (>p normalize nodelta)
1221  try (>p1 normalize nodelta)
1222  (* XXX: switch to the left hand side *)
1223  >EQP -P normalize nodelta
1224  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1225  whd in ⊢ (??%?);
1226  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1227  (* XXX: work on the left hand side *)
1228  [1,2,3,4,5:
1229    generalize in ⊢ (??(???(?%))?);
1230  |6,7,8,9,10,11:
1231    generalize in ⊢ (??(???(?%))?);
1232  |12:
1233    generalize in ⊢ (??(???(?%))?);
1234  ]
1235  <EQaddr normalize nodelta #irrelevant
1236  try @(jmpair_as_replace ?????????? p)
1237  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1238  (* XXX: switch to the right hand side *)
1239  normalize nodelta >EQs -s >EQticks -ticks
1240  whd in ⊢ (??%%);
1241  (* XXX: finally, prove the equality using sigma commutation *)
1242  try @split_eq_status try % whd in ⊢ (??%%);
1243  cases daemon
1244  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1245  (* XXX: work on the right hand side *)
1246  >p normalize nodelta
1247  try (>p1 normalize nodelta)
1248  (* XXX: switch to the left hand side *)
1249  -instr_refl >EQP -P normalize nodelta
1250  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1251  whd in ⊢ (??%?);
1252  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1253  (* XXX: work on the left hand side *)
1254  @(pair_replace ?????????? p)
1255  [1,3,5,7,9,11,13,15,17:
1256    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1257    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1258    cases daemon
1259  |14,16,18:
1260    normalize nodelta
1261    @(pair_replace ?????????? p1)
1262    [1,3,5:
1263      >set_clock_mk_Status_commutation
1264      cases daemon
1265    ]
1266  ]
1267  (* XXX: switch to the right hand side *)
1268  normalize nodelta >EQs -s >EQticks -ticks
1269  whd in ⊢ (??%%);
1270  (* XXX: finally, prove the equality using sigma commutation *)
1271  try @split_eq_status try %
1272  cases daemon
1273  |10,42,43,44,45,49,52,56: (* MUL *)
1274  (* XXX: work on the right hand side *)
1275  (* XXX: switch to the left hand side *)
1276  -instr_refl >EQP -P normalize nodelta
1277  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1278  whd in ⊢ (??%?);
1279  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1280  (* XXX: work on the left hand side *)
1281  (* XXX: switch to the right hand side *)
1282  normalize nodelta >EQs -s >EQticks -ticks
1283  whd in ⊢ (??%%);
1284  (* XXX: finally, prove the equality using sigma commutation *)
1285  cases daemon
1286  |11,12: (* DIV *)
1287  (* XXX: work on the right hand side *)
1288  normalize nodelta in p;
1289  >p normalize nodelta
1290  (* XXX: switch to the left hand side *)
1291  -instr_refl >EQP -P normalize nodelta
1292  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1293  whd in ⊢ (??%?);
1294  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1295  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1296  >(?: pose_assm = 0) normalize nodelta
1297  [2,4:
1298    <p >pose_refl
1299    cases daemon
1300  |1,3:
1301    (* XXX: switch to the right hand side *)
1302    >EQs -s >EQticks -ticks
1303    whd in ⊢ (??%%);
1304    (* XXX: finally, prove the equality using sigma commutation *)
1305    @split_eq_status try %
1306    cases daemon
1307  ]
1308  |13,14,15: (* DA *)
1309  (* XXX: work on the right hand side *)
1310  >p normalize nodelta
1311  >p1 normalize nodelta
1312  try (>p2 normalize nodelta
1313  try (>p3 normalize nodelta
1314  try (>p4 normalize nodelta
1315  try (>p5 normalize nodelta))))
1316  (* XXX: switch to the left hand side *)
1317  -instr_refl >EQP -P normalize nodelta
1318  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1319  whd in ⊢ (??%?);
1320  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1321  (* XXX: work on the left hand side *)
1322  @(pair_replace ?????????? p)
1323  [1,3,5:
1324    /demod/
1325    cases daemon
1326  |2,4,6:
1327    @(if_then_else_replace ???????? p1)
1328    [1,3,5:
1329      cases daemon
1330    |2,4:
1331      normalize nodelta
1332      @(pair_replace ?????????? p2)
1333      [1,3:
1334        cases daemon
1335      |2,4:
1336        normalize nodelta >p3 normalize nodelta
1337        >p4 normalize nodelta try >p5
1338      ]
1339    ]
1340  (* XXX: switch to the right hand side *)
1341  normalize nodelta >EQs -s >EQticks -ticks
1342  whd in ⊢ (??%%);
1343  (* XXX: finally, prove the equality using sigma commutation *)
1344  @split_eq_status try %
1345  cases daemon
1346  ]
1347  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1348  (* XXX: work on the right hand side *)
1349  cases addr #addr' normalize nodelta
1350  [1,3:
1351    cases addr' #addr'' normalize nodelta
1352  ]
1353  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1354  (* XXX: switch to the left hand side *)
1355  -instr_refl >EQP -P normalize nodelta
1356  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1357  whd in ⊢ (??%?);
1358  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1359  (* XXX: work on the left hand side *)
1360  (* XXX: switch to the right hand side *)
1361  normalize nodelta >EQs -s >EQticks -ticks
1362  whd in ⊢ (??%%);
1363  (* XXX: finally, prove the equality using sigma commutation *)
1364  cases daemon
1365  |47: (* MOV *)
1366  (* XXX: work on the right hand side *)
1367  cases addr -addr #addr normalize nodelta
1368  [1:
1369    cases addr #addr normalize nodelta
1370    [1:
1371      cases addr #addr normalize nodelta
1372      [1:
1373        cases addr #addr normalize nodelta
1374        [1:
1375          cases addr #addr normalize nodelta
1376        ]
1377      ]
1378    ]
1379  ]
1380  cases addr #lft #rgt normalize nodelta
1381  (* XXX: switch to the left hand side *)
1382  >EQP -P normalize nodelta
1383  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1384  whd in ⊢ (??%?);
1385  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1386  (* XXX: work on the left hand side *)
1387  (* XXX: switch to the right hand side *)
1388  normalize nodelta >EQs -s >EQticks -ticks
1389  whd in ⊢ (??%%);
1390  (* XXX: finally, prove the equality using sigma commutation *)
1391  cases daemon
1392  ]
1393qed.
1394
1395theorem main_thm:
1396  ∀M.
1397  ∀M'.
1398  ∀program: pseudo_assembly_program.
1399  ∀sigma: Word → Word.
1400  ∀policy: Word → bool.
1401  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1402  ∀ps: PseudoStatus program.
1403    next_internal_pseudo_address_map M program ps = Some … M' →
1404      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
1405        status_of_pseudo_status M' …
1406          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
1407  #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
1408  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
1409  @(pose … (program_counter ?? ps)) #ppc #EQppc
1410  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
1411  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
1412  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
1413  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
1414  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
1415  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
1416  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
1417  whd in match execute_1_pseudo_instruction; normalize nodelta
1418  whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
1419  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
1420  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
1421  [1: >fetch_pseudo_refl % ]
1422  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
1423  generalize in match assm1; -assm1 -assm2 -assm3
1424  normalize nodelta
1425  cases pi
1426  [2,3:
1427    #arg
1428    (* XXX: we first work on sigma_increment_commutation *)
1429    #sigma_increment_commutation
1430    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
1431    (* XXX: we work on the maps *)
1432    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
1433    (* XXX: we assume the fetch_many hypothesis *)
1434    #fetch_many_assm
1435    (* XXX: we give the existential *)
1436    %{0}
1437    whd in match (execute_1_pseudo_instruction0 ?????);
1438    (* XXX: work on the left hand side of the equality *)
1439    whd in ⊢ (??%?);
1440    @split_eq_status //
1441    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
1442  |6: (* Mov *)
1443    #arg1 #arg2
1444    (* XXX: we first work on sigma_increment_commutation *)
1445    #sigma_increment_commutation
1446    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
1447    (* XXX: we work on the maps *)
1448    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
1449    (* XXX: we assume the fetch_many hypothesis *)
1450    #fetch_many_assm
1451    (* XXX: we give the existential *)
1452    %{1}
1453    whd in match (execute_1_pseudo_instruction0 ?????);
1454    (* XXX: work on the left hand side of the equality *)
1455    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
1456    (* XXX: execute fetches some more *)
1457    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
1458    whd in fetch_many_assm;
1459    >EQassembled in fetch_many_assm;
1460    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
1461    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
1462    #fetch_many_assm whd in fetch_many_assm;
1463    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1464    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
1465    (* XXX: now we start to work on the mk_PreStatus equality *)
1466    (* XXX: lhs *)
1467    change with (set_arg_16 ????? = ?)
1468    >set_program_counter_mk_Status_commutation
1469    >set_clock_mk_Status_commutation
1470    >set_arg_16_mk_Status_commutation
1471    (* XXX: rhs *)
1472    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
1473    >set_program_counter_mk_Status_commutation
1474    >set_clock_mk_Status_commutation
1475    >set_arg_16_mk_Status_commutation in ⊢ (???%);
1476    (* here we are *)
1477    @split_eq_status //
1478    [1:
1479      assumption
1480    |2:
1481      @special_function_registers_8051_set_arg_16
1482      [2: >EQlookup_datalabels %
1483      |1: //
1484      ]
1485    ]
1486  |1: (* Instruction *) -pi; #instr
1487    @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
1488      … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
1489      EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
1490  |4,5: cases daemon
1491  ]
1492qed.
1493(* 
1494    *
1495    [1,2,3: (* ADD, ADDC, SUBB *)
1496    @list_addressing_mode_tags_elim_prop try % whd
1497    @list_addressing_mode_tags_elim_prop try % whd #arg
1498    (* XXX: we first work on sigma_increment_commutation *)
1499    #sigma_increment_commutation
1500    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
1501    (* XXX: we work on the maps *)
1502    whd in ⊢ (??%? → ?);
1503    try (change with (if ? then ? else ? = ? → ?)
1504         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
1505    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
1506    (* XXX: we assume the fetch_many hypothesis *)
1507    #fetch_many_assm
1508    (* XXX: we give the existential *)
1509    %{1}
1510    whd in match (execute_1_pseudo_instruction0 ?????);
1511    (* XXX: work on the left hand side of the equality *)
1512    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
1513    (* XXX: execute fetches some more *)
1514    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
1515    whd in fetch_many_assm;
1516    >EQassembled in fetch_many_assm;
1517    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1518    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
1519    #fetch_many_assm whd in fetch_many_assm;
1520    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1521    >(eq_instruction_to_eq … eq_instr) -instr
1522    [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
1523      @(pose …
1524        (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
1525      #Pl #EQPl
1526      cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
1527      lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
1528      whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
1529      @pair_elim
1530      >tech_pi1_let_as_commute
1531   
1532   
1533    whd in ⊢ (??%?);
1534    [ @(pose … (execute_1_preinstruction' ???????))
1535      #lhs whd in ⊢ (???% → ?); #EQlhs
1536      @(pose … (execute_1_preinstruction' ???????))
1537      #rhs whd in ⊢ (???% → ?); #EQrhs
1538
1539
1540      CSC: delirium
1541     
1542      >EQlhs -EQlhs >EQrhs -EQrhs
1543      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);
1544     
1545     lapply (refl ? (execute_1_preinstruction' ???????));
1546    [ whd in match (execute_1_preinstruction' ???????);
1547
1548    whd in ⊢ (??%?);
1549    [ whd in ⊢ (??(???%)%);
1550      whd in match (execute_1_preinstruction' ???????);
1551      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);
1552      @pair_elim #result #flags #Heq1
1553    whd in match execute_1_preinstruction'; normalize nodelta
1554    (* XXX: now we start to work on the mk_PreStatus equality *)
1555    whd in ⊢ (??%?);
1556 
1557 
1558 
1559    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2
1560    (* XXX: we take up the hypotheses *)
1561    #sigma_increment_commutation #next_map_assm #fetch_many_assm
1562    (* XXX: we give the existential *)
1563    %{1}
1564    whd in match (execute_1_pseudo_instruction0 ?????);
1565    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
1566    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
1567    (* XXX: fetching of the instruction *)
1568    whd in fetch_many_assm;
1569    >EQassembled in fetch_many_assm;
1570    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1571    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
1572    #fetch_many_assm whd in fetch_many_assm;
1573    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1574    >(eq_instruction_to_eq … eq_instr) -instr
1575    (* XXX: now we start to work on the mk_PreStatus equality *)
1576    whd in ⊢ (??%?);
1577    check execute_1_preinstruction
1578   
1579   
1580     #MAP #H1 #H2 #EQ %[1,3,5:@1]
1581       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1582       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1583       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1584       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1585       >H2b >(eq_instruction_to_eq … H2a)
1586       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1587       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1588       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1589       normalize nodelta; #MAP;
1590       [1: change in ⊢ (? → %) with
1591        ((let 〈result,flags〉 ≝
1592          add_8_with_carry
1593           (get_arg_8 ? ps false ACC_A)
1594           (get_arg_8 ?
1595             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1596             false (DIRECT ARG2))
1597           ? in ?) = ?)
1598        [2,3: %]
1599        change in ⊢ (???% → ?) with
1600         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
1601        >get_arg_8_set_clock
1602       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1603         [2,4: #abs @⊥ normalize in abs; destruct (abs)
1604         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1605       [ change in ⊢ (? → %) with
1606        ((let 〈result,flags〉 ≝
1607          add_8_with_carry
1608           (get_arg_8 ? ps false ACC_A)
1609           (get_arg_8 ?
1610             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1611             false (DIRECT ARG2))
1612           ? in ?) = ?)
1613          >get_arg_8_set_low_internal_ram
1614       
1615        cases (add_8_with_carry ???)
1616         
1617        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1618       #result #flags
1619       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1620
1621
1622  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
1623   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
1624       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
1625         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
1626         @pair_elim' * #instr #newppc' #ticks #EQ4       
1627         * * #H2a #H2b whd in ⊢ (% → ?) #H2
1628         >H2b >(eq_instruction_to_eq … H2a)
1629         #EQ %[@1]
1630         <MAP >(eq_bv_eq … H2) >EQ
1631         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
1632         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
1633         whd in ⊢ (??%?)
1634         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
1635         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1636  |5: (* Call *) #label #MAP
1637      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
1638      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1639       [ (* short *) #abs @⊥ destruct (abs)
1640       |3: (* long *) #H1 #H2 #EQ %[@1]
1641           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1642           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1643           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1644           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1645           >H2b >(eq_instruction_to_eq … H2a)
1646           generalize in match EQ; -EQ;
1647           whd in ⊢ (???% → ??%?);
1648           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
1649           >(eq_bv_eq … H2c)
1650           change with
1651            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
1652                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1653           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
1654           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
1655           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
1656           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
1657           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
1658           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1659           @split_eq_status;
1660            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
1661              >code_memory_write_at_stack_pointer %
1662            | >set_program_counter_set_low_internal_ram
1663              >set_clock_set_low_internal_ram
1664              @low_internal_ram_write_at_stack_pointer
1665               [ >EQ0 @pol | % | %
1666               | @(  … EQ1)
1667               | @(pair_destruct_2 … EQ2)
1668               | >(pair_destruct_1 ????? EQpc)
1669                 >(pair_destruct_2 ????? EQpc)
1670                 @split_elim #x #y #H <H -x y H;
1671                 >(pair_destruct_1 ????? EQppc)
1672                 >(pair_destruct_2 ????? EQppc)
1673                 @split_elim #x #y #H <H -x y H;
1674                 >EQ0 % ]
1675            | >set_low_internal_ram_set_high_internal_ram
1676              >set_program_counter_set_high_internal_ram
1677              >set_clock_set_high_internal_ram
1678              @high_internal_ram_write_at_stack_pointer
1679               [ >EQ0 @pol | % | %
1680               | @(pair_destruct_2 … EQ1)
1681               | @(pair_destruct_2 … EQ2)
1682               | >(pair_destruct_1 ????? EQpc)
1683                 >(pair_destruct_2 ????? EQpc)
1684                 @split_elim #x #y #H <H -x y H;
1685                 >(pair_destruct_1 ????? EQppc)
1686                 >(pair_destruct_2 ????? EQppc)
1687                 @split_elim #x #y #H <H -x y H;
1688                 >EQ0 % ]           
1689            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
1690              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1691              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1692              >external_ram_write_at_stack_pointer %
1693            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
1694              >EQ0 %
1695            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
1696              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1697              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1698              >special_function_registers_8051_write_at_stack_pointer %
1699            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
1700              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1701              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1702              >special_function_registers_8052_write_at_stack_pointer %
1703            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
1704              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1705              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1706              >p1_latch_write_at_stack_pointer %
1707            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
1708              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1709              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1710              >p3_latch_write_at_stack_pointer %
1711            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
1712              >clock_write_at_stack_pointer whd in ⊢ (???%)
1713              >clock_write_at_stack_pointer whd in ⊢ (???%)
1714              >clock_write_at_stack_pointer %]
1715       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1716         @pair_elim' #fst_5_addr #rest_addr #EQ1
1717         @pair_elim' #fst_5_pc #rest_pc #EQ2
1718         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1719         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1720         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1721         change in ⊢ (? →??%?) with (execute_1_0 ??)
1722         @pair_elim' * #instr #newppc' #ticks #EQn
1723          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
1724          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1725          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
1726          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
1727          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
1728          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
1729          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
1730          >get_8051_sfr_set_8051_sfr
1731         
1732          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1733           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
1734           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
1735           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1736           generalize in match (refl … (split bool 4 4 pc_bu))
1737           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1738           generalize in match (refl … (split bool 3 8 rest_addr))
1739           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1740           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1741           generalize in match
1742            (refl …
1743             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
1744             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1745           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
1746           @split_eq_status try %
1747            [ change with (? = sigma ? (address_of_word_labels ps label))
1748              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1749            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1750              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
1751  |4: (* Jmp *) #label #MAP
1752      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
1753      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1754       [3: (* long *) #H1 #H2 #EQ %[@1]
1755           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1756           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1757           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1758           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1759           >H2b >(eq_instruction_to_eq … H2a)
1760           generalize in match EQ; -EQ;
1761           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1762           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1763       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1764           generalize in match
1765            (refl ?
1766             (sub_16_with_carry
1767              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
1768              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
1769              false))
1770           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
1771           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
1772           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
1773           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
1774           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1775           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1776           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1777           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1778           >H2b >(eq_instruction_to_eq … H2a)
1779           generalize in match EQ; -EQ;
1780           whd in ⊢ (???% → ?);
1781           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1782           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
1783           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
1784           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
1785           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
1786           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1787       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1788         generalize in match
1789          (refl …
1790            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
1791         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
1792         generalize in match
1793          (refl …
1794            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
1795         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
1796         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1797         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1798         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1799         change in ⊢ (? →??%?) with (execute_1_0 ??)
1800           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1801           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1802           >H2b >(eq_instruction_to_eq … H2a)
1803           generalize in match EQ; -EQ;
1804           whd in ⊢ (???% → ?);
1805           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1806           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1807           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
1808           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1809           generalize in match (refl … (split bool 4 4 pc_bu))
1810           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1811           generalize in match (refl … (split bool 3 8 rest_addr))
1812           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1813           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1814           generalize in match
1815            (refl …
1816             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
1817             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1818           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
1819           @split_eq_status try %
1820            [ change with (? = sigma ?? (address_of_word_labels ps label))
1821              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1822            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1823              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
1824  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
1825    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
1826       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1827       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1828       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1829       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1830       >H2b >(eq_instruction_to_eq … H2a)
1831       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1832       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1833       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1834       normalize nodelta; #MAP;
1835       [1: change in ⊢ (? → %) with
1836        ((let 〈result,flags〉 ≝
1837          add_8_with_carry
1838           (get_arg_8 ? ps false ACC_A)
1839           (get_arg_8 ?
1840             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1841             false (DIRECT ARG2))
1842           ? in ?) = ?)
1843        [2,3: %]
1844        change in ⊢ (???% → ?) with
1845         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
1846        >get_arg_8_set_clock
1847       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1848         [2,4: #abs @⊥ normalize in abs; destruct (abs)
1849         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1850       [ change in ⊢ (? → %) with
1851        ((let 〈result,flags〉 ≝
1852          add_8_with_carry
1853           (get_arg_8 ? ps false ACC_A)
1854           (get_arg_8 ?
1855             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1856             false (DIRECT ARG2))
1857           ? in ?) = ?)
1858          >get_arg_8_set_low_internal_ram
1859       
1860        cases (add_8_with_carry ???)
1861         
1862        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1863       #result #flags
1864       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1865    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
1866       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1867       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1868       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1869       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1870       >H2b >(eq_instruction_to_eq … H2a)
1871       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1872       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
1873       [1,2,3,4: cases (half_add ???) #carry #result
1874       | cases (half_add ???) #carry #bl normalize nodelta;
1875         cases (full_add ????) #carry' #bu normalize nodelta ]
1876        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
1877        [5: %
1878        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
1879      (set_program_counter pseudo_assembly_program ps newppc)
1880      (\fst  (ticks_of0 〈preamble,instr_list〉
1881                   (program_counter pseudo_assembly_program ps)
1882                   (Instruction (INC Identifier (DIRECT ARG))))
1883       +clock pseudo_assembly_program
1884        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
1885        [2,3: // ]
1886            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
1887            whd in ⊢ (??%%)
1888            cases (split bool 4 4 ARG)
1889            #nu' #nl'
1890            normalize nodelta
1891            cases (split bool 1 3 nu')
1892            #bit_1' #ignore'
1893            normalize nodelta
1894            cases (get_index_v bool 4 nu' ? ?)
1895            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
1896            |
1897            ]
1898cases daemon (* EASY CASES TO BE COMPLETED *)
1899qed.
1900*)
Note: See TracBrowser for help on using the repository browser.