source: src/ASM/AssemblyProofSplit.ma @ 2020

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

CJNE case complete, DJNZ case almost complete

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