source: src/ASM/AssemblyProof.ma @ 1616

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

Partially ported to new Matita syntax.
Because of some changes in Fetch.ma, it no longer compiles.

File size: 88.7 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
7  λP.
8    P true ∧ P false.
9 
10let rec bitvector_elim_prop_internal
11  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
12  match m return λm. m ≤ n → BitVector (n - m) → Prop with
13  [ O    ⇒ λprf1. λprefix. P ?
14  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
15  ].
16  [ applyS prefix
17  | letin res ≝ (bit ::: prefix)
18    < (minus_S_S ? ?)
19    > (minus_Sn_m ? ?)
20  [ @ res
21  | @ prf2
22  ]
23  | /2/
24  ].
25qed.
26
27definition bitvector_elim_prop ≝
28  λn: nat.
29  λP: BitVector n → Prop.
30    bitvector_elim_prop_internal n P n ? ?.
31  [ @ (le_n ?)
32  | < (minus_n_n ?)
33    @ [[ ]]
34  ]
35qed.
36
37lemma bool_eq_internal_eq:
38  ∀b, c.
39    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
40  #b #c
41  cases b
42  [ normalize //
43  | normalize
44    cases c
45    [ normalize //
46    | normalize //
47    ]
48  ]
49qed.
50
51definition bit_elim: ∀P: bool → bool. bool ≝
52  λP.
53    P true ∧ P false.
54
55let rec bitvector_elim_internal
56  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
57  match m return λm. m ≤ n → BitVector (n - m) → bool with
58  [ O    ⇒ λprf1. λprefix. P ?
59  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
60  ].
61  [ applyS prefix
62  | letin res ≝ (bit ::: prefix)
63    < (minus_S_S ? ?)
64    > (minus_Sn_m ? ?)
65    [ @ res
66    | @ prf2
67    ]
68  | /2/
69  ].
70qed.
71
72definition bitvector_elim ≝
73  λn: nat.
74  λP: BitVector n → bool.
75    bitvector_elim_internal n P n ? ?.
76  [ @ (le_n ?)
77  | < (minus_n_n ?)
78    @ [[ ]]
79  ]
80qed.
81
82lemma super_rewrite2:
83 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
84  ∀P: ∀m. Vector A m → Prop.
85   n=m → v1 ≃ v2 → P n v1 → P m v2.
86 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
87qed.
88
89lemma vector_cons_append:
90  ∀A: Type[0].
91  ∀n: nat.
92  ∀e: A.
93  ∀v: Vector A n.
94    e ::: v = [[ e ]] @@ v.
95  # A # N # E # V
96  elim V
97  [ normalize %
98  | # NN # AA # VV # IH
99    normalize
100    %
101qed.
102
103lemma vector_cons_append2:
104  ∀A: Type[0].
105  ∀n, m: nat.
106  ∀v: Vector A n.
107  ∀q: Vector A m.
108  ∀hd: A.
109    hd:::(v@@q) = (hd:::v)@@q.
110  #A #n #m #v #q
111  elim v
112  [ #hd %
113  | #n' #hd' #tl' #ih #hd' <ih %
114  ]
115qed.
116
117lemma jmeq_cons_vector_monotone:
118  ∀A: Type[0].
119  ∀m, n: nat.
120  ∀v: Vector A m.
121  ∀q: Vector A n.
122  ∀prf: m = n.
123  ∀hd: A.
124    v ≃ q → hd:::v ≃ hd:::q.
125  #A #m #n #v #q #prf #hd #E
126  @(super_rewrite2 A … E)
127  [ assumption | % ]
128qed.
129
130lemma vector_associative_append:
131  ∀A: Type[0].
132  ∀n, m, o:  nat.
133  ∀v: Vector A n.
134  ∀q: Vector A m.
135  ∀r: Vector A o.
136    ((v @@ q) @@ r)
137    ≃
138    (v @@ (q @@ r)).
139  #A #n #m #o #v #q #r
140  elim v
141  [ %
142  | #n' #hd #tl #ih
143    <(vector_cons_append2 A … hd)
144    @jmeq_cons_vector_monotone
145    //
146  ]
147qed.
148
149lemma mem_middle_vector:
150  ∀A: Type[0].
151  ∀m, o: nat.
152  ∀eq: A → A → bool.
153  ∀reflex: ∀a. eq a a = true.
154  ∀p: Vector A m.
155  ∀a: A.
156  ∀r: Vector A o.
157    mem A eq ? (p@@(a:::r)) a = true.
158  # A # M # O # EQ # REFLEX # P # A
159  elim P
160  [ normalize
161    > (REFLEX A)
162    normalize
163    # H
164    %
165  | # NN # AA # PP # IH
166    normalize
167    cases (EQ A AA) //
168     @ IH
169  ]
170qed.
171
172lemma mem_monotonic_wrt_append:
173  ∀A: Type[0].
174  ∀m, o: nat.
175  ∀eq: A → A → bool.
176  ∀reflex: ∀a. eq a a = true.
177  ∀p: Vector A m.
178  ∀a: A.
179  ∀r: Vector A o.
180    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
181  # A # M # O # EQ # REFLEX # P # A
182  elim P
183  [ #R #H @H
184  | #NN #AA # PP # IH #R #H
185    normalize
186    cases (EQ A AA)
187    [ normalize %
188    | @ IH @ H
189    ]
190  ]
191qed.
192
193lemma subvector_multiple_append:
194  ∀A: Type[0].
195  ∀o, n: nat.
196  ∀eq: A → A → bool.
197  ∀refl: ∀a. eq a a = true.
198  ∀h: Vector A o.
199  ∀v: Vector A n.
200  ∀m: nat.
201  ∀q: Vector A m.
202    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
203  # A # O # N # EQ # REFLEX # H # V
204  elim V
205  [ normalize
206    # M # V %
207  | # NN # AA # VV # IH # MM # QQ
208    change with (bool_to_Prop (andb ??))
209    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
210    [
211    | # HH > HH
212      > (vector_cons_append ? ? AA VV)
213      change with (bool_to_Prop (subvector_with ??????))
214      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
215        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
216        ?
217        (vector_associative_append A ? ? ? QQ [[AA]] VV))
218      [ >associative_plus //
219      | @IH ]
220    ]
221    @(mem_monotonic_wrt_append)
222    [ @ REFLEX
223    | @(mem_monotonic_wrt_append)
224      [ @ REFLEX
225      | normalize
226        > REFLEX
227        normalize
228        %
229      ]
230    ]
231qed.
232
233lemma vector_cons_empty:
234  ∀A: Type[0].
235  ∀n: nat.
236  ∀v: Vector A n.
237    [[ ]] @@ v = v.
238  # A # N # V
239  elim V
240  [ normalize %
241  | # NN # HH # VV #H %
242  ]
243qed.
244
245corollary subvector_hd_tl:
246  ∀A: Type[0].
247  ∀o: nat.
248  ∀eq: A → A → bool.
249  ∀refl: ∀a. eq a a = true.
250  ∀h: A.
251  ∀v: Vector A o.
252    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
253  # A # O # EQ # REFLEX # H # V
254  > (vector_cons_append A ? H V)
255  < (vector_cons_empty A ? ([[H]] @@ V))
256  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
257qed.
258
259lemma eq_a_reflexive:
260  ∀a. eq_a a a = true.
261  # A
262  cases A
263  %
264qed.
265
266lemma is_in_monotonic_wrt_append:
267  ∀m, n: nat.
268  ∀p: Vector addressing_mode_tag m.
269  ∀q: Vector addressing_mode_tag n.
270  ∀to_search: addressing_mode.
271    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
272  # M # N # P # Q # TO_SEARCH
273  # H
274  elim Q
275  [ normalize
276    @ H
277  | # NN # PP # QQ # IH
278    normalize
279    cases (is_a PP TO_SEARCH)
280    [ normalize
281      %
282    | normalize
283      normalize in IH;
284      @ IH
285    ]
286  ]
287qed.
288
289corollary is_in_hd_tl:
290  ∀to_search: addressing_mode.
291  ∀hd: addressing_mode_tag.
292  ∀n: nat.
293  ∀v: Vector addressing_mode_tag n.
294    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
295  # TO_SEARCH # HD # N # V
296  elim V
297  [ # H
298    normalize in H;
299    cases H
300  | # NN # HHD # VV # IH # HH
301    > vector_cons_append
302    > (vector_cons_append ? ? HHD VV)
303    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
304    @ HH
305  ]
306qed.
307 
308let rec list_addressing_mode_tags_elim
309  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
310  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
311   (l → bool) → bool ] with
312  [ VEmpty      ⇒  true 
313  | VCons len hd tl ⇒ λP.
314    let process_hd ≝
315      match hd return λhd. ∀P: hd:::tl → bool. bool with
316      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
317      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
318      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
319      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
320      | acc_a ⇒ λP.P ACC_A
321      | acc_b ⇒ λP.P ACC_B
322      | dptr ⇒ λP.P DPTR
323      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
324      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
325      | acc_dptr ⇒ λP.P ACC_DPTR
326      | acc_pc ⇒ λP.P ACC_PC
327      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
328      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
329      | carry ⇒ λP.P CARRY
330      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
331      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
332      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
333      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
334      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
335      ]
336    in
337      andb (process_hd P)
338       (match len return λx. x = len → bool with
339         [ O ⇒ λprf. true
340         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
341  ].
342  try %
343  [ 2: cases (sym_eq ??? prf); @tl
344  | generalize in match H; generalize in match tl; cases prf;
345    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
346    #tl
347    normalize in ⊢ (∀_: %. ?);
348    # H
349    whd
350    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
351    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
352qed.
353
354definition product_elim ≝
355  λm, n: nat.
356  λv: Vector addressing_mode_tag (S m).
357  λq: Vector addressing_mode_tag (S n).
358  λP: (v × q) → bool.
359    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
360
361definition union_elim ≝
362  λA, B: Type[0].
363  λelimA: (A → bool) → bool.
364  λelimB: (B → bool) → bool.
365  λelimU: A ⊎ B → bool.
366    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
367
368(*                           
369definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
370  λP.
371    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
372    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
373    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
374    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
375    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
376    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
377    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
378    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
379    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
380    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
381    P (DA ? ACC_A) ∧
382    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
383    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
384    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
385    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
386    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
387    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
388    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
389    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
390    P (RL ? ACC_A) ∧
391    P (RLC ? ACC_A) ∧
392    P (RR ? ACC_A) ∧
393    P (RRC ? ACC_A) ∧
394    P (SWAP ? ACC_A) ∧
395    P (RET ?) ∧
396    P (RETI ?) ∧
397    P (NOP ?) ∧
398    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
399    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
400    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
401    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
402    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
403                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
404                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
405    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
406    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
407                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
408                   (λd. P (XRL ? d)) ∧
409    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
410                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
411                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
412                   (λd. P (ANL ? d)) ∧
413    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
414                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
415                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
416                   (λd. P (ORL ? d)) ∧
417    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
418                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
419                   (λd. P (MOVX ? d)) ∧
420    union_elim ? ? (
421      union_elim ? ? (
422        union_elim ? ? (
423          union_elim ? ? (
424            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
425                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
426                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
427                            (product_elim ? ? [[dptr]] [[data16]]))
428                            (product_elim ? ? [[carry]] [[bit_addr]]))
429                            (product_elim ? ? [[bit_addr]] [[carry]])
430                            (λd. P (MOV ? d)).
431  %
432qed.
433 
434definition instruction_elim: ∀P: instruction → bool. bool ≝
435  λP. (*
436    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
437    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
438    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
439    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
440    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
441    P (JMP INDIRECT_DPTR) ∧
442    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
443    preinstruction_elim (λp. P (RealInstruction p)). *)
444  %
445qed.
446
447
448axiom instruction_elim_complete:
449 ∀P. instruction_elim P = true → ∀i. P i = true.
450*)
451(*definition eq_instruction ≝
452  λi, j: instruction.
453    true.*)
454
455definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
456  λa, b: addressing_mode.
457  match a with
458  [ DIRECT d ⇒
459    match b with
460    [ DIRECT e ⇒ eq_bv ? d e
461    | _ ⇒ false
462    ]
463  | INDIRECT b' ⇒
464    match b with
465    [ INDIRECT e ⇒ eq_b b' e
466    | _ ⇒ false
467    ]
468  | EXT_INDIRECT b' ⇒
469    match b with
470    [ EXT_INDIRECT e ⇒ eq_b b' e
471    | _ ⇒ false
472    ]
473  | REGISTER bv ⇒
474    match b with
475    [ REGISTER bv' ⇒ eq_bv ? bv bv'
476    | _ ⇒ false
477    ]
478  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
479  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
480  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
481  | DATA b' ⇒
482    match b with
483    [ DATA e ⇒ eq_bv ? b' e
484    | _ ⇒ false
485    ]
486  | DATA16 w ⇒
487    match b with
488    [ DATA16 e ⇒ eq_bv ? w e
489    | _ ⇒ false
490    ]
491  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
492  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
493  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
494  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
495  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
496  | BIT_ADDR b' ⇒
497    match b with
498    [ BIT_ADDR e ⇒ eq_bv ? b' e
499    | _ ⇒ false
500    ]
501  | N_BIT_ADDR b' ⇒
502    match b with
503    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
504    | _ ⇒ false
505    ]
506  | RELATIVE n ⇒
507    match b with
508    [ RELATIVE e ⇒ eq_bv ? n e
509    | _ ⇒ false
510    ]
511  | ADDR11 w ⇒
512    match b with
513    [ ADDR11 e ⇒ eq_bv ? w e
514    | _ ⇒ false
515    ]
516  | ADDR16 w ⇒
517    match b with
518    [ ADDR16 e ⇒ eq_bv ? w e
519    | _ ⇒ false
520    ]
521  ].
522
523lemma eq_bv_refl:
524  ∀n, b.
525    eq_bv n b b = true.
526  #n #b cases b //
527qed.
528
529lemma eq_b_refl:
530  ∀b.
531    eq_b b b = true.
532  #b cases b //
533qed.
534
535lemma eq_addressing_mode_refl:
536  ∀a. eq_addressing_mode a a = true.
537  #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl
538  try normalize %
539qed.
540 
541definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
542  λlt, rt, leq, req, left, right.
543    match left with
544    [ inl l ⇒
545      match right with
546      [ inl l' ⇒ leq l l'
547      | _ ⇒ false
548      ]
549    | inr r ⇒
550      match right with
551      [ inr r' ⇒ req r r'
552      | _ ⇒ false
553      ]
554    ].
555
556definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
557  λlt, rt, leq, req, left, right.
558    let 〈l, r〉 ≝ left in
559    let 〈l', r'〉 ≝ right in
560      leq l l' ∧ req r r'.
561
562definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
563  λi, j.
564  match i with
565  [ ADD arg1 arg2 ⇒
566    match j with
567    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
568    | _ ⇒ false
569    ]
570  | ADDC arg1 arg2 ⇒
571    match j with
572    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
573    | _ ⇒ false
574    ]
575  | SUBB arg1 arg2 ⇒
576    match j with
577    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
578    | _ ⇒ false
579    ]
580  | INC arg ⇒
581    match j with
582    [ INC arg' ⇒ eq_addressing_mode arg arg'
583    | _ ⇒ false
584    ]
585  | DEC arg ⇒
586    match j with
587    [ DEC arg' ⇒ eq_addressing_mode arg arg'
588    | _ ⇒ false
589    ]
590  | MUL arg1 arg2 ⇒
591    match j with
592    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
593    | _ ⇒ false
594    ]
595  | DIV arg1 arg2 ⇒
596    match j with
597    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
598    | _ ⇒ false
599    ]
600  | DA arg ⇒
601    match j with
602    [ DA arg' ⇒ eq_addressing_mode arg arg'
603    | _ ⇒ false
604    ]
605  | JC arg ⇒
606    match j with
607    [ JC arg' ⇒ eq_addressing_mode arg arg'
608    | _ ⇒ false
609    ]
610  | JNC arg ⇒
611    match j with
612    [ JNC arg' ⇒ eq_addressing_mode arg arg'
613    | _ ⇒ false
614    ]
615  | JB arg1 arg2 ⇒
616    match j with
617    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
618    | _ ⇒ false
619    ]
620  | JNB arg1 arg2 ⇒
621    match j with
622    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
623    | _ ⇒ false
624    ]
625  | JBC arg1 arg2 ⇒
626    match j with
627    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
628    | _ ⇒ false
629    ]
630  | JZ arg ⇒
631    match j with
632    [ JZ arg' ⇒ eq_addressing_mode arg arg'
633    | _ ⇒ false
634    ]
635  | JNZ arg ⇒
636    match j with
637    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
638    | _ ⇒ false
639    ]
640  | CJNE arg1 arg2 ⇒
641    match j with
642    [ CJNE arg1' arg2' ⇒
643      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
644      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
645      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
646        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
647    | _ ⇒ false
648    ]
649  | DJNZ arg1 arg2 ⇒
650    match j with
651    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
652    | _ ⇒ false
653    ]
654  | CLR arg ⇒
655    match j with
656    [ CLR arg' ⇒ eq_addressing_mode arg arg'
657    | _ ⇒ false
658    ]
659  | CPL arg ⇒
660    match j with
661    [ CPL arg' ⇒ eq_addressing_mode arg arg'
662    | _ ⇒ false
663    ]
664  | RL arg ⇒
665    match j with
666    [ RL arg' ⇒ eq_addressing_mode arg arg'
667    | _ ⇒ false
668    ]
669  | RLC arg ⇒
670    match j with
671    [ RLC arg' ⇒ eq_addressing_mode arg arg'
672    | _ ⇒ false
673    ]
674  | RR arg ⇒
675    match j with
676    [ RR arg' ⇒ eq_addressing_mode arg arg'
677    | _ ⇒ false
678    ]
679  | RRC arg ⇒
680    match j with
681    [ RRC arg' ⇒ eq_addressing_mode arg arg'
682    | _ ⇒ false
683    ]
684  | SWAP arg ⇒
685    match j with
686    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
687    | _ ⇒ false
688    ]
689  | SETB arg ⇒
690    match j with
691    [ SETB arg' ⇒ eq_addressing_mode arg arg'
692    | _ ⇒ false
693    ]
694  | PUSH arg ⇒
695    match j with
696    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
697    | _ ⇒ false
698    ]
699  | POP arg ⇒
700    match j with
701    [ POP arg' ⇒ eq_addressing_mode arg arg'
702    | _ ⇒ false
703    ]
704  | XCH arg1 arg2 ⇒
705    match j with
706    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
707    | _ ⇒ false
708    ]
709  | XCHD arg1 arg2 ⇒
710    match j with
711    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
712    | _ ⇒ false
713    ]
714  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
715  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
716  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
717  | MOVX arg ⇒
718    match j with
719    [ MOVX arg' ⇒
720      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
721      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
722      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
723        sum_eq arg arg'
724    | _ ⇒ false
725    ]
726  | XRL arg ⇒
727    match j with
728    [ XRL arg' ⇒
729      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
730      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
731      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
732        sum_eq arg arg'
733    | _ ⇒ false
734    ]
735  | ORL arg ⇒
736    match j with
737    [ ORL arg' ⇒
738      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
739      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
740      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
741      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
742      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
743        sum_eq arg arg'
744    | _ ⇒ false
745    ]
746  | ANL arg ⇒
747    match j with
748    [ ANL arg' ⇒
749      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
750      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
751      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
752      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
753      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
754        sum_eq arg arg'
755    | _ ⇒ false
756    ]
757  | MOV arg ⇒
758    match j with
759    [ MOV arg' ⇒
760      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
761      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
762      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
763      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
764      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
765      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
766      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
767      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
768      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
769      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
770      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
771        sum_eq_5 arg arg'
772    | _ ⇒ false
773    ]
774  ].
775
776lemma eq_sum_refl:
777  ∀A, B: Type[0].
778  ∀leq, req.
779  ∀s.
780  ∀leq_refl: (∀t. leq t t = true).
781  ∀req_refl: (∀u. req u u = true).
782    eq_sum A B leq req s s = true.
783  #A #B #leq #req #s #leq_refl #req_refl
784  cases s whd in ⊢ (? → ??%?); //
785qed.
786
787lemma eq_prod_refl:
788  ∀A, B: Type[0].
789  ∀leq, req.
790  ∀s.
791  ∀leq_refl: (∀t. leq t t = true).
792  ∀req_refl: (∀u. req u u = true).
793    eq_prod A B leq req s s = true.
794  #A #B #leq #req #s #leq_refl #req_refl
795  cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl
796qed.
797
798lemma eq_preinstruction_refl:
799  ∀i.
800    eq_preinstruction i i = true.
801  #i cases i try #arg1 try #arg2
802  try @eq_addressing_mode_refl
803  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
804    whd in ⊢ (??%?);
805    try %
806    >eq_addressing_mode_refl
807    >eq_addressing_mode_refl %
808  |13,15:
809    whd in ⊢ (??%?);
810    cases arg1
811    [*:
812      #arg1_left normalize nodelta
813      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
814    ]
815  |11,12:
816    whd in ⊢ (??%?);
817    cases arg1
818    [1:
819      #arg1_left normalize nodelta
820      >(eq_sum_refl …)
821      [1: % | 2,3: #arg @eq_prod_refl ]
822      @eq_addressing_mode_refl
823    |2:
824      #arg1_left normalize nodelta
825      @eq_prod_refl [*: @eq_addressing_mode_refl ]
826    |3:
827      #arg1_left normalize nodelta
828      >(eq_sum_refl …) [1: %
829      |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
830    |4:
831      #arg1_left normalize nodelta
832      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
833    ]
834  |14:
835    whd in ⊢ (??%?);
836    cases arg1
837    [ #arg1_left normalize nodelta
838      @eq_sum_refl
839      [1: #arg @eq_sum_refl
840        [1: #arg @eq_sum_refl
841          [1: #arg @eq_sum_refl
842            [1: #arg @eq_prod_refl
843              [*: @eq_addressing_mode_refl ]
844            |2: #arg @eq_prod_refl
845              [*: #arg @eq_addressing_mode_refl ]
846            ]
847          |2: #arg @eq_prod_refl
848            [*: #arg @eq_addressing_mode_refl ]
849          ]
850        |2: #arg @eq_prod_refl
851          [*: #arg @eq_addressing_mode_refl ]
852        ]
853      |2: #arg @eq_prod_refl
854        [*: #arg @eq_addressing_mode_refl ]
855      ]
856    |2: #arg1_right normalize nodelta
857        @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
858    ]
859  |*:
860    whd in ⊢ (??%?);
861    cases arg1
862    [*: #arg1 >eq_sum_refl
863      [1,4: normalize @eq_addressing_mode_refl
864      |2,3,5,6: #arg @eq_prod_refl
865        [*: #arg @eq_addressing_mode_refl ]
866      ]
867    ]
868  ]
869qed.
870
871definition eq_instruction: instruction → instruction → bool ≝
872  λi, j.
873  match i with
874  [ ACALL arg ⇒
875    match j with
876    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
877    | _ ⇒ false
878    ]
879  | LCALL arg ⇒
880    match j with
881    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
882    | _ ⇒ false
883    ]
884  | AJMP arg ⇒
885    match j with
886    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
887    | _ ⇒ false
888    ]
889  | LJMP arg ⇒
890    match j with
891    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
892    | _ ⇒ false
893    ]
894  | SJMP arg ⇒
895    match j with
896    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
897    | _ ⇒ false
898    ]
899  | JMP arg ⇒
900    match j with
901    [ JMP arg' ⇒ eq_addressing_mode arg arg'
902    | _ ⇒ false
903    ]
904  | MOVC arg1 arg2 ⇒
905    match j with
906    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
907    | _ ⇒ false
908    ]
909  | RealInstruction instr ⇒
910    match j with
911    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
912    | _ ⇒ false
913    ]
914  ].
915 
916lemma eq_instruction_refl:
917  ∀i. eq_instruction i i = true.
918  #i cases i
919  [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
920  |7: #arg1 #arg2
921      whd in ⊢ (??%?);
922      >eq_addressing_mode_refl
923      >eq_addressing_mode_refl
924      %
925  |8: #arg @eq_preinstruction_refl
926  ]
927qed.
928
929let rec vect_member
930  (A: Type[0]) (n: nat) (eq: A → A → bool)
931  (v: Vector A n) (a: A) on v: bool ≝
932  match v with
933  [ VEmpty          ⇒ false
934  | VCons len hd tl ⇒
935    eq hd a ∨ (vect_member A ? eq tl a)
936  ].
937
938let rec list_addressing_mode_tags_elim_prop
939  (n: nat)
940  (l: Vector addressing_mode_tag (S n))
941  on l:
942  ∀P: l → Prop.
943  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
944  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
945  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
946  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
947  ∀x: l. P x ≝
948  match l return
949    λy.
950      match y with
951      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
952      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
953               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
954               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
955               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
956               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
957               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
958               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
959               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
960               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
961               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
962               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
963               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
964               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
965               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
966               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
967               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
968               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
969               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
970               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
971               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
972               ∀x:l. P x
973      ] with
974  [ VEmpty          ⇒ λAbsurd. ⊥
975  | VCons len hd tl ⇒ λProof. ?
976  ] (refl ? (S n)). cases daemon. qed. (*
977  [ destruct(Absurd)
978  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
979    # A8 # A9 # A10 # A11 # A12 # A13 # A14
980    # A15 # A16 # A17 # A18 # A19 # X
981    cases X
982    # SUB cases daemon ] qed.
983    cases SUB
984    [ # BYTE
985    normalize
986  ].
987 
988 
989(*    let prepare_hd ≝
990      match hd with
991      [ direct ⇒ λdirect_prf. ?
992      | indirect ⇒ λindirect_prf. ?
993      | ext_indirect ⇒ λext_indirect_prf. ?
994      | registr ⇒ λregistr_prf. ?
995      | acc_a ⇒ λacc_a_prf. ?
996      | acc_b ⇒ λacc_b_prf. ?
997      | dptr ⇒ λdptr_prf. ?
998      | data ⇒ λdata_prf. ?
999      | data16 ⇒ λdata16_prf. ?
1000      | acc_dptr ⇒ λacc_dptr_prf. ?
1001      | acc_pc ⇒ λacc_pc_prf. ?
1002      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
1003      | indirect_dptr ⇒ λindirect_prf. ?
1004      | carry ⇒ λcarry_prf. ?
1005      | bit_addr ⇒ λbit_addr_prf. ?
1006      | n_bit_addr ⇒ λn_bit_addr_prf. ?
1007      | relative ⇒ λrelative_prf. ?
1008      | addr11 ⇒ λaddr11_prf. ?
1009      | addr16 ⇒ λaddr16_prf. ?
1010      ]
1011    in ? *)
1012  ].
1013  [ 1: destruct(absd)
1014  | 2: # A1 # A2 # A3 # A4 # A5 # A6
1015       # A7 # A8 # A9 # A10 # A11 # A12
1016       # A13 # A14 # A15 # A16 # A17 # A18
1017       # A19 *
1018  ].
1019
1020
1021  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
1022   (l → bool) → bool ] with
1023  [ VEmpty      ⇒  true 
1024  | VCons len hd tl ⇒ λP.
1025    let process_hd ≝
1026      match hd return λhd. ∀P: hd:::tl → bool. bool with
1027      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
1028      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
1029      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
1030      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
1031      | acc_a ⇒ λP.P ACC_A
1032      | acc_b ⇒ λP.P ACC_B
1033      | dptr ⇒ λP.P DPTR
1034      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
1035      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
1036      | acc_dptr ⇒ λP.P ACC_DPTR
1037      | acc_pc ⇒ λP.P ACC_PC
1038      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
1039      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
1040      | carry ⇒ λP.P CARRY
1041      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
1042      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
1043      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
1044      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
1045      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
1046      ]
1047    in
1048      andb (process_hd P)
1049       (match len return λx. x = len → bool with
1050         [ O ⇒ λprf. true
1051         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
1052  ].
1053  try %
1054  [ 2: cases (sym_eq ??? prf); @tl
1055  | generalize in match H; generalize in match tl; cases prf;
1056    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
1057    #tl
1058    normalize in ⊢ (∀_: %. ?)
1059    # H
1060    whd
1061    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1062    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
1063qed.
1064*)
1065
1066definition load_code_memory_aux ≝
1067 fold_left_i_aux … (
1068   λi, mem, v.
1069     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
1070
1071lemma split_zero:
1072  ∀A,m.
1073  ∀v: Vector A m.
1074    〈[[]], v〉 = split A 0 m v.
1075  #A #m #v
1076  elim v
1077  [ %
1078  | #n #hd #tl #ih
1079    normalize in ⊢ (???%); %
1080  ]
1081qed.
1082
1083lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
1084 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
1085 #n #hd #tl #abs @⊥ destruct (abs)
1086qed.
1087
1088lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
1089 ∃hd.∃tl.v ≃ VCons A n hd tl.
1090 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
1091 [ #abs @⊥ destruct (abs)
1092 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
1093qed.
1094
1095lemma vector_append_zero:
1096  ∀A,m.
1097  ∀v: Vector A m.
1098  ∀q: Vector A 0.
1099    v = q@@v.
1100  #A #m #v #q
1101  >(Vector_O A q) %
1102qed.
1103
1104lemma prod_eq_left:
1105  ∀A: Type[0].
1106  ∀p, q, r: A.
1107    p = q → 〈p, r〉 = 〈q, r〉.
1108  #A #p #q #r #hyp
1109  >hyp %
1110qed.
1111
1112lemma prod_eq_right:
1113  ∀A: Type[0].
1114  ∀p, q, r: A.
1115    p = q → 〈r, p〉 = 〈r, q〉.
1116  #A #p #q #r #hyp
1117  >hyp %
1118qed.
1119
1120corollary prod_vector_zero_eq_left:
1121  ∀A, n.
1122  ∀q: Vector A O.
1123  ∀r: Vector A n.
1124    〈q, r〉 = 〈[[ ]], r〉.
1125  #A #n #q #r
1126  generalize in match (Vector_O A q …);
1127  #hyp
1128  >hyp in ⊢ (??%?);
1129  %
1130qed.
1131
1132axiom split_succ:
1133  ∀A, m, n.
1134  ∀l: Vector A m.
1135  ∀r: Vector A n.
1136  ∀v: Vector A (m + n).
1137  ∀hd: A.
1138    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
1139(*
1140  #A #m
1141  elim m
1142  [ #n #l #r #v #hd #equal #hyp
1143    normalize >(Vector_O A l) >equal
1144    >(Vector_O A l) %
1145  | #n' #ih #n #l #r #v #hd
1146    #equal #hyp
1147    cases(Vector_Sn A n' l)
1148    #hd' #exists
1149    cases exists #tl #jmeq
1150    >jmeq *)
1151
1152lemma split_prod:
1153  ∀A,m,n.
1154  ∀p: Vector A (m + n).
1155  ∀v: Vector A m.
1156  ∀q: Vector A n.
1157    p = v@@q → 〈v, q〉 = split A m n p.
1158  #A #m
1159  elim m
1160  [ #n #p #v #q #hyp
1161    >hyp <(vector_append_zero A n q v)
1162    >(prod_vector_zero_eq_left A …)
1163    @split_zero
1164  | #r #ih #n #p #v #q #hyp
1165    >hyp
1166    cases (Vector_Sn A r v)
1167    #hd #exists
1168    cases exists
1169    #tl #jmeq >jmeq
1170    @split_succ [1: % |2: @ih % ]
1171  ]
1172qed.
1173
1174(*
1175lemma split_prod_exists:
1176  ∀A, m, n.
1177  ∀p: Vector A (m + n).
1178  ∃v: Vector A m.
1179  ∃q: Vector A n.
1180    〈v, q〉 = split A m n p.
1181  #A #m #n #p
1182  elim m
1183  @ex_intro
1184  [1:
1185  |2: @ex_intro
1186      [1:
1187      |2:
1188      ]
1189  ]
1190*)
1191
1192axiom split_elim:
1193 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
1194  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
1195(*  #A #l #m #v #P #hyp
1196  normalize
1197  <(split_prod A l m v ? ? ?)
1198*)
1199
1200example half_add_SO:
1201 ∀pc.
1202 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
1203 cases daemon.
1204qed.
1205
1206(*
1207axiom not_eqvb_S:
1208 ∀pc.
1209 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
1210
1211axiom not_eqvb_SS:
1212 ∀pc.
1213 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
1214 
1215axiom bitvector_elim_complete:
1216 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
1217
1218lemma bitvector_elim_complete':
1219 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
1220 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
1221 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
1222qed.
1223*)
1224
1225(*
1226lemma andb_elim':
1227 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
1228 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
1229qed.
1230*)
1231
1232let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
1233                       (encoding: list Byte) on encoding: Prop ≝
1234  match encoding with
1235  [ nil ⇒ final_pc = pc
1236  | cons hd tl ⇒
1237    let 〈new_pc, byte〉 ≝ next code_memory pc in
1238      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
1239  ].
1240
1241lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
1242 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
1243  let intermediate_pc ≝ pc + length … l1 in
1244   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
1245    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
1246 #code_memory #final_pc #l1 elim l1
1247  [ #pc #l2 whd in ⊢ (????% → ?); #H <plus_n_O whd whd in ⊢ (?%?); /2/
1248  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
1249    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
1250qed.
1251
1252axiom bitvector_3_elim_prop:
1253 ∀P: BitVector 3 → Prop.
1254  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
1255  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
1256  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
1257
1258definition ticks_of_instruction ≝
1259 λi.
1260  let trivial_code_memory ≝ assembly1 i in
1261  let trivial_status ≝ load_code_memory trivial_code_memory in
1262   \snd (fetch trivial_status (zero ?)).
1263
1264lemma fetch_assembly:
1265  ∀pc,i,code_memory,assembled.
1266    assembled = assembly1 i →
1267      let len ≝ length … assembled in
1268      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1269      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
1270      let 〈instr_pc, ticks〉 ≝ fetched in
1271      let 〈instr,pc'〉 ≝ instr_pc in
1272       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
1273 #pc #i #code_memory #assembled cases i [8: *]
1274 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
1275 [47,48,49:
1276 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
1277  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
1278   59,60,63,64,65,66,67: #ARG]]
1279 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
1280  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
1281  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
1282   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
1283   68,69,70,71: #ARG2]]
1284 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
1285 normalize in ⊢ (???% → ?);
1286 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
1287  normalize in ⊢ (???% → ?);]
1288 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
1289 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
1290 [ whd in match fetch; normalize nodelta <H1 (*XXX
1291   
1292 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
1293 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
1294 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
1295  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
1296  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
1297 whd >eq_instruction_refl >H4 @eq_bv_refl*)
1298qed.
1299
1300let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
1301 match expected with
1302  [ nil ⇒ eq_bv … pc final_pc = true
1303  | cons i tl ⇒
1304     let fetched ≝ fetch code_memory pc in
1305     let 〈instr_pc, ticks〉 ≝ fetched in
1306     let 〈instr,pc'〉 ≝ instr_pc in
1307      eq_instruction instr i = true ∧
1308      ticks = (ticks_of_instruction i) ∧
1309      fetch_many code_memory final_pc pc' tl].
1310
1311lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
1312 #A #a #b #EQ destruct //
1313qed.
1314
1315axiom eq_instruction_to_eq:
1316  ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
1317               
1318lemma fetch_assembly_pseudo':
1319 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
1320  ∀pi,code_memory,len,assembled,instructions,pc.
1321   let expansion ≝ pol ppc in
1322   Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
1323    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction_safe program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
1324     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
1325      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
1326 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
1327 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
1328 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
1329 >EQ2a >EQ2b -EQ2a EQ2b;
1330  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
1331  generalize in match pc elim instructions
1332  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
1333  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
1334    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
1335    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
1336    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
1337    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
1338    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
1339qed.
1340
1341axiom bitvector_of_nat_nat_of_bitvector:
1342  ∀n,v.
1343    bitvector_of_nat n (nat_of_bitvector n v) = v.
1344
1345(* CSC: soo long next one; can we merge with previous one now? *)
1346lemma fetch_assembly_pseudo:
1347 ∀program.∀pol:policy program.∀ppc.
1348  ∀code_memory.
1349   let lookup_labels ≝ ? in
1350   let lookup_datalabels ≝ ? in
1351   let pc ≝ ? in
1352   let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
1353   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in
1354   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
1355     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
1356      fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
1357 #program #pol #ppc #code_memory
1358 letin lookup_labels ≝ (λx:Identifier
1359    .sigma program pol (address_of_word_labels_code_mem (\snd  program) x))
1360 letin lookup_datalabels ≝
1361  (λx:BitVector 16
1362    .lookup Identifier 16 x (construct_datalabels (\fst  program)) (zero 16))
1363 letin pc ≝ (sigma program pol ppc)
1364 letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
1365 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …))
1366 @pair_elim' #len #assembled #EQ1 #H
1367 generalize in match
1368  (fetch_assembly_pseudo' program pol ppc lookup_labels lookup_datalabels pi
1369  code_memory len assembled instructions (nat_of_bitvector ? pc) ???) in ⊢ ?;
1370 [ >bitvector_of_nat_nat_of_bitvector //
1371 | >bitvector_of_nat_nat_of_bitvector normalize nodelta >(sig2 ?? (expand_pseudo_instruction …)) %
1372 | >bitvector_of_nat_nat_of_bitvector <EQ1 @assembly_1_pseudoinstruction_ok1
1373 | //]
1374qed.
1375
1376(* This is a trivial consequence of fetch_assembly + the proof that the
1377   function that load the code in memory is correct. The latter is based
1378   on missing properties from the standard library on the BitVectorTrie
1379   data structrure. *)
1380axiom assembly_ok:
1381 ∀program,pol,assembled,costs'.
1382  let 〈labels,costs〉 ≝ build_maps program pol in
1383  〈assembled,costs'〉 = assembly program pol →
1384  costs = costs' ∧
1385  let code_memory ≝ load_code_memory assembled in
1386  let preamble ≝ \fst program in
1387  let datalabels ≝ construct_datalabels preamble in
1388  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1389  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1390  ∀ppc.
1391  let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
1392   ∀len,assembledi.
1393     〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) →
1394      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
1395       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
1396
1397lemma fetch_assembly_pseudo2:
1398 ∀program,pol,ppc.
1399(*  let 〈labels,costs〉 ≝ build_maps program pol in *)
1400  let assembled ≝ \fst (assembly program pol) in
1401  let code_memory ≝ load_code_memory assembled in
1402  let data_labels ≝ construct_datalabels (\fst program) in
1403  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
1404  let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1405  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1406  let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
1407   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
1408 * #preamble #instr_list #pol #ppc
1409 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol))
1410 letin code_memory ≝ (load_code_memory assembled)
1411 letin data_labels ≝ (construct_datalabels preamble)
1412 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
1413 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1414 @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
1415 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
1416 @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
1417 #H cases (H (refl \ldots)) -H; #EQ3
1418 generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
1419 cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
1420 #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
1421 generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
1422 >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
1423 >H2 #K @K
1424qed.
1425
1426(* OLD?
1427definition assembly_specification:
1428  ∀assembly_program: pseudo_assembly_program.
1429  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1430  λpseudo_assembly_program.
1431  λcode_mem.
1432    ∀pc: Word.
1433      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1434      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1435      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1436      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1437      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1438       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1439      match pre_assembled with
1440       [ None ⇒ True
1441       | Some pc_code ⇒
1442          let 〈new_pc,code〉 ≝ pc_code in
1443           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1444
1445axiom assembly_meets_specification:
1446  ∀pseudo_assembly_program.
1447    match assembly pseudo_assembly_program with
1448    [ None ⇒ True
1449    | Some code_mem_cost ⇒
1450      let 〈code_mem, cost〉 ≝ code_mem_cost in
1451        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1452    ].
1453(*
1454  # PROGRAM
1455  [ cases PROGRAM
1456    # PREAMBLE
1457    # INSTR_LIST
1458    elim INSTR_LIST
1459    [ whd
1460      whd in ⊢ (∀_. %)
1461      # PC
1462      whd
1463    | # INSTR
1464      # INSTR_LIST_TL
1465      # H
1466      whd
1467      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1468    ]
1469  | cases not_implemented
1470  ] *)
1471*)
1472
1473definition internal_pseudo_address_map ≝ list (BitVector 8).
1474
1475axiom low_internal_ram_of_pseudo_low_internal_ram:
1476 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1477
1478axiom high_internal_ram_of_pseudo_high_internal_ram:
1479 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1480
1481axiom low_internal_ram_of_pseudo_internal_ram_hit:
1482 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
1483  member ? (eq_bv 8) (false:::addr) M = true →
1484   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1485   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1486   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1487   let bl ≝ lookup ? 7 addr ram (zero 8) in
1488   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1489    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
1490
1491(* changed from add to sub *)
1492axiom low_internal_ram_of_pseudo_internal_ram_miss:
1493 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
1494  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1495  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1496  let carr ≝ get_index_v ? ? flags 1 ? in
1497  carr = false →
1498  member ? (eq_bv 8) (false:::Saddr) M = false →
1499   member ? (eq_bv 8) (false:::addr) M = false →
1500    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1501  //
1502qed.
1503
1504definition addressing_mode_ok ≝
1505 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
1506  λaddr:addressing_mode.
1507   match addr with
1508    [ DIRECT d ⇒
1509       ¬(member ? (eq_bv 8) d M) ∧
1510       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1511    | INDIRECT i ⇒
1512       let d ≝ get_register ? s [[false;false;i]] in
1513       ¬(member ? (eq_bv 8) d M) ∧
1514       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1515    | EXT_INDIRECT _ ⇒ true
1516    | REGISTER _ ⇒ true
1517    | ACC_A ⇒ true
1518    | ACC_B ⇒ true
1519    | DPTR ⇒ true
1520    | DATA _ ⇒ true
1521    | DATA16 _ ⇒ true
1522    | ACC_DPTR ⇒ true
1523    | ACC_PC ⇒ true
1524    | EXT_INDIRECT_DPTR ⇒ true
1525    | INDIRECT_DPTR ⇒ true
1526    | CARRY ⇒ true
1527    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1528    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1529    | RELATIVE _ ⇒ true
1530    | ADDR11 _ ⇒ true
1531    | ADDR16 _ ⇒ true ].
1532   
1533definition next_internal_pseudo_address_map0 ≝
1534  λT.
1535  λfetched.
1536  λM: internal_pseudo_address_map.
1537  λs: PreStatus T.
1538   match fetched with
1539    [ Comment _ ⇒ Some ? M
1540    | Cost _ ⇒ Some … M
1541    | Jmp _ ⇒ Some … M
1542    | Call _ ⇒
1543       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1544    | Mov _ _ ⇒ Some … M
1545    | Instruction instr ⇒
1546       match instr with
1547        [ ADD addr1 addr2 ⇒
1548           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1549            Some ? M
1550           else
1551            None ?
1552        | ADDC addr1 addr2 ⇒
1553           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1554            Some ? M
1555           else
1556            None ?
1557        | SUBB addr1 addr2 ⇒
1558           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1559            Some ? M
1560           else
1561            None ?       
1562        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1563 
1564
1565definition next_internal_pseudo_address_map ≝
1566 λM:internal_pseudo_address_map.
1567  λs:PseudoStatus.
1568    next_internal_pseudo_address_map0 ?
1569     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1570   
1571definition status_of_pseudo_status:
1572 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝
1573 λM,ps,pol.
1574  let pap ≝ code_memory … ps in
1575  let p ≝ assembly pap pol in
1576  let cm ≝ load_code_memory (\fst p) in
1577  let pc ≝ sigma pap pol (program_counter ? ps) in
1578  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1579  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1580     mk_PreStatus (BitVectorTrie Byte 16)
1581      cm
1582      lir
1583      hir
1584      (external_ram … ps)
1585      pc
1586      (special_function_registers_8051 … ps)
1587      (special_function_registers_8052 … ps)
1588      (p1_latch … ps)
1589      (p3_latch … ps)
1590      (clock … ps).
1591
1592(*
1593definition write_at_stack_pointer':
1594 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1595  λM: Type[0].
1596  λs: PreStatus M.
1597  λv: Byte.
1598    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1599    let bit_zero ≝ get_index_v… nu O ? in
1600    let bit_1 ≝ get_index_v… nu 1 ? in
1601    let bit_2 ≝ get_index_v… nu 2 ? in
1602    let bit_3 ≝ get_index_v… nu 3 ? in
1603      if bit_zero then
1604        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1605                              v (low_internal_ram ? s) in
1606          set_low_internal_ram ? s memory
1607      else
1608        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1609                              v (high_internal_ram ? s) in
1610          set_high_internal_ram ? s memory.
1611  [ cases l0 %
1612  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1613qed.
1614
1615definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1616 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1617
1618  λticks_of.
1619  λs.
1620  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1621  let ticks ≝ ticks_of (program_counter ? s) in
1622  let s ≝ set_clock ? s (clock ? s + ticks) in
1623  let s ≝ set_program_counter ? s pc in
1624    match instr with
1625    [ Instruction instr ⇒
1626       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1627    | Comment cmt ⇒ s
1628    | Cost cst ⇒ s
1629    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1630    | Call call ⇒
1631      let a ≝ address_of_word_labels s call in
1632      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1633      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1634      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1635      let s ≝ write_at_stack_pointer' ? s pc_bl in
1636      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1637      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1638      let s ≝ write_at_stack_pointer' ? s pc_bu in
1639        set_program_counter ? s a
1640    | Mov dptr ident ⇒
1641       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1642    ].
1643 [
1644 |2,3,4: %
1645 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1646 |
1647 | %
1648 ]
1649 cases not_implemented
1650qed.
1651*)
1652
1653axiom execute_1_pseudo_instruction_preserves_code_memory:
1654 ∀ticks_of,ps.
1655  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1656
1657(*
1658lemma execute_code_memory_unchanged:
1659 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1660 #ticks #ps whd in ⊢ (??? (??%))
1661 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1662  (program_counter pseudo_assembly_program ps)) #instr #pc
1663 whd in ⊢ (??? (??%)) cases instr
1664  [ #pre cases pre
1665     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1666       cases (split ????) #z1 #z2 %
1667     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1668       cases (split ????) #z1 #z2 %
1669     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1670       cases (split ????) #z1 #z2 %
1671     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1672       [ #x1 whd in ⊢ (??? (??%))
1673     | *: cases not_implemented
1674     ]
1675  | #comment %
1676  | #cost %
1677  | #label %
1678  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1679    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1680    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1681    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1682    (* CSC: ??? *)
1683  | #dptr #label (* CSC: ??? *)
1684  ]
1685  cases not_implemented
1686qed.
1687*)
1688
1689(* DEAD CODE?
1690lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1691 ∀M:internal_pseudo_address_map.
1692 ∀ps,ps': PseudoStatus.
1693 ∀pol.
1694  ∀prf:code_memory … ps = code_memory … ps'.
1695   let pol' ≝ ? in
1696   match status_of_pseudo_status M ps pol with
1697    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1698    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1699    ].
1700 [2: <prf @pol]
1701 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1702 generalize in match (refl … (assembly (code_memory … ps) pol))
1703 cases (assembly ??) in ⊢ (???% → %)
1704  [ #K whd whd in ⊢ (??%?) <H >K %
1705  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1706qed.
1707*)
1708
1709definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
1710  λprogram: pseudo_assembly_program.λpol.
1711  λppc: Word.
1712  λfetched.
1713    match fetched with
1714    [ Instruction instr ⇒
1715      match instr with
1716      [ JC lbl ⇒
1717        match pol ppc with
1718        [ short_jump ⇒ 〈2, 2〉
1719        | medium_jump ⇒ ?
1720        | long_jump ⇒ 〈4, 4〉
1721        ]
1722      | JNC lbl ⇒
1723        match pol ppc with
1724        [ short_jump ⇒ 〈2, 2〉
1725        | medium_jump ⇒ ?
1726        | long_jump ⇒ 〈4, 4〉
1727        ]
1728      | JB bit lbl ⇒
1729        match pol ppc with
1730        [ short_jump ⇒ 〈2, 2〉
1731        | medium_jump ⇒ ?
1732        | long_jump ⇒ 〈4, 4〉
1733        ]
1734      | JNB bit lbl ⇒
1735        match pol ppc with
1736        [ short_jump ⇒ 〈2, 2〉
1737        | medium_jump ⇒ ?
1738        | long_jump ⇒ 〈4, 4〉
1739        ]
1740      | JBC bit lbl ⇒
1741        match pol ppc with
1742        [ short_jump ⇒ 〈2, 2〉
1743        | medium_jump ⇒ ?
1744        | long_jump ⇒ 〈4, 4〉
1745        ]
1746      | JZ lbl ⇒
1747        match pol ppc with
1748        [ short_jump ⇒ 〈2, 2〉
1749        | medium_jump ⇒ ?
1750        | long_jump ⇒ 〈4, 4〉
1751        ]
1752      | JNZ lbl ⇒
1753        match pol ppc with
1754        [ short_jump ⇒ 〈2, 2〉
1755        | medium_jump ⇒ ?
1756        | long_jump ⇒ 〈4, 4〉
1757        ]
1758      | CJNE arg lbl ⇒
1759        match pol ppc with
1760        [ short_jump ⇒ 〈2, 2〉
1761        | medium_jump ⇒ ?
1762        | long_jump ⇒ 〈4, 4〉
1763        ]
1764      | DJNZ arg lbl ⇒
1765        match pol ppc with
1766        [ short_jump ⇒ 〈2, 2〉
1767        | medium_jump ⇒ ?
1768        | long_jump ⇒ 〈4, 4〉
1769        ]
1770      | ADD arg1 arg2 ⇒
1771        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1772         〈ticks, ticks〉
1773      | ADDC arg1 arg2 ⇒
1774        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1775         〈ticks, ticks〉
1776      | SUBB arg1 arg2 ⇒
1777        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1778         〈ticks, ticks〉
1779      | INC arg ⇒
1780        let ticks ≝ ticks_of_instruction (INC ? arg) in
1781         〈ticks, ticks〉
1782      | DEC arg ⇒
1783        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1784         〈ticks, ticks〉
1785      | MUL arg1 arg2 ⇒
1786        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1787         〈ticks, ticks〉
1788      | DIV arg1 arg2 ⇒
1789        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1790         〈ticks, ticks〉
1791      | DA arg ⇒
1792        let ticks ≝ ticks_of_instruction (DA ? arg) in
1793         〈ticks, ticks〉
1794      | ANL arg ⇒
1795        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1796         〈ticks, ticks〉
1797      | ORL arg ⇒
1798        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1799         〈ticks, ticks〉
1800      | XRL arg ⇒
1801        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1802         〈ticks, ticks〉
1803      | CLR arg ⇒
1804        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1805         〈ticks, ticks〉
1806      | CPL arg ⇒
1807        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1808         〈ticks, ticks〉
1809      | RL arg ⇒
1810        let ticks ≝ ticks_of_instruction (RL ? arg) in
1811         〈ticks, ticks〉
1812      | RLC arg ⇒
1813        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1814         〈ticks, ticks〉
1815      | RR arg ⇒
1816        let ticks ≝ ticks_of_instruction (RR ? arg) in
1817         〈ticks, ticks〉
1818      | RRC arg ⇒
1819        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1820         〈ticks, ticks〉
1821      | SWAP arg ⇒
1822        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1823         〈ticks, ticks〉
1824      | MOV arg ⇒
1825        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1826         〈ticks, ticks〉
1827      | MOVX arg ⇒
1828        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1829         〈ticks, ticks〉
1830      | SETB arg ⇒
1831        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1832         〈ticks, ticks〉
1833      | PUSH arg ⇒
1834        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1835         〈ticks, ticks〉
1836      | POP arg ⇒
1837        let ticks ≝ ticks_of_instruction (POP ? arg) in
1838         〈ticks, ticks〉
1839      | XCH arg1 arg2 ⇒
1840        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1841         〈ticks, ticks〉
1842      | XCHD arg1 arg2 ⇒
1843        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1844         〈ticks, ticks〉
1845      | RET ⇒
1846        let ticks ≝ ticks_of_instruction (RET ?) in
1847         〈ticks, ticks〉
1848      | RETI ⇒
1849        let ticks ≝ ticks_of_instruction (RETI ?) in
1850         〈ticks, ticks〉
1851      | NOP ⇒
1852        let ticks ≝ ticks_of_instruction (NOP ?) in
1853         〈ticks, ticks〉
1854      ]
1855    | Comment comment ⇒ 〈0, 0〉
1856    | Cost cost ⇒ 〈0, 0〉
1857    | Jmp jmp ⇒ 〈2, 2〉
1858    | Call call ⇒ 〈2, 2〉
1859    | Mov dptr tgt ⇒ 〈2, 2〉
1860    ].
1861  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1862qed.
1863
1864definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
1865  λprogram: pseudo_assembly_program.λpol.
1866  λppc: Word.
1867    let 〈preamble, pseudo〉 ≝ program in
1868    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1869     ticks_of0 program pol ppc fetched.
1870
1871lemma eq_rect_Type1_r:
1872  ∀A: Type[1].
1873  ∀a:A.
1874  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1875  #A #a #P #H #x #p
1876  generalize in match H
1877  generalize in match P
1878  cases p
1879  //
1880qed.
1881
1882axiom split_append:
1883  ∀A: Type[0].
1884  ∀m, n: nat.
1885  ∀v, v': Vector A m.
1886  ∀q, q': Vector A n.
1887    let 〈v', q'〉 ≝ split A m n (v@@q) in
1888      v = v' ∧ q = q'.
1889
1890axiom split_vector_singleton:
1891  ∀A: Type[0].
1892  ∀n: nat.
1893  ∀v: Vector A (S n).
1894  ∀rest: Vector A n.
1895  ∀s: Vector A 1.
1896  ∀prf.
1897    v = s @@ rest →
1898    ((get_index_v A ? v 0 prf) ::: rest) = v.
1899
1900example sub_minus_one_seven_eight:
1901  ∀v: BitVector 7.
1902  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1903  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1904 cases daemon.
1905qed.
1906
1907(*
1908lemma blah:
1909  ∀m: internal_pseudo_address_map.
1910  ∀s: PseudoStatus.
1911  ∀arg: Byte.
1912  ∀b: bool.
1913    addressing_mode_ok m s (DIRECT arg) = true →
1914      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1915      get_arg_8 ? s b (DIRECT arg).
1916  [2, 3: normalize % ]
1917  #m #s #arg #b #hyp
1918  whd in ⊢ (??%%)
1919  @split_elim''
1920  #nu' #nl' #arg_nu_nl_eq
1921  normalize nodelta
1922  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1923  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1924  #get_index_v_eq
1925  normalize nodelta
1926  [2:
1927    normalize nodelta
1928    @split_elim''
1929    #bit_one' #three_bits' #bit_one_three_bit_eq
1930    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1931    normalize nodelta
1932    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1933    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1934    #Saddr #carr' #Saddr_carr_eq
1935    normalize nodelta
1936    #carr_hyp'
1937    @carr_hyp'
1938    [1:
1939    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1940        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1941        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1942        #member_eq
1943        normalize nodelta
1944        [2: #destr destruct(destr)
1945        |1: -carr_hyp';
1946            >arg_nu_nl_eq
1947            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1948            [1: >get_index_v_eq in ⊢ (??%? → ?)
1949            |2: @le_S @le_S @le_S @le_n
1950            ]
1951            cases (member (BitVector 8) ? (\fst ?) ?)
1952            [1: #destr normalize in destr; destruct(destr)
1953            |2:
1954            ]
1955        ]
1956    |3: >get_index_v_eq in ⊢ (??%?)
1957        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1958        >(split_vector_singleton … bit_one_three_bit_eq)
1959        <arg_nu_nl_eq
1960        whd in hyp:(??%?)
1961        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1962        normalize nodelta [*: #ignore @sym_eq ]
1963    ]
1964  |
1965  ].
1966*)
1967(*
1968map_address0 ... (DIRECT arg) = Some .. →
1969  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1970  get_arg_8 (internal_ram ...) (DIRECT arg)
1971
1972((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1973                     then Some internal_pseudo_address_map M 
1974                     else None internal_pseudo_address_map )
1975                    =Some internal_pseudo_address_map M')
1976*)
1977
1978axiom low_internal_ram_write_at_stack_pointer:
1979 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1980  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
1981  low_internal_ram ? s2 = low_internal_ram T2 s3 →
1982  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
1983  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
1984  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
1985   low_internal_ram T1
1986     (write_at_stack_pointer ?
1987       (set_8051_sfr ?
1988         (write_at_stack_pointer ?
1989           (set_8051_sfr ?
1990             (set_low_internal_ram ? s1
1991               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
1992             SFR_SP sp1)
1993          bl)
1994        SFR_SP sp2)
1995      bu)
1996   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1997      (low_internal_ram ?
1998       (write_at_stack_pointer ?
1999         (set_8051_sfr ?
2000           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2001          SFR_SP sp2)
2002        pbu)).
2003
2004axiom high_internal_ram_write_at_stack_pointer:
2005 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2006  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2007  high_internal_ram ? s2 = high_internal_ram T2 s3 →
2008  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2009  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2010  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
2011   high_internal_ram T1
2012     (write_at_stack_pointer ?
2013       (set_8051_sfr ?
2014         (write_at_stack_pointer ?
2015           (set_8051_sfr ?
2016             (set_high_internal_ram ? s1
2017               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
2018             SFR_SP sp1)
2019          bl)
2020        SFR_SP sp2)
2021      bu)
2022   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2023      (high_internal_ram ?
2024       (write_at_stack_pointer ?
2025         (set_8051_sfr ?
2026           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2027          SFR_SP sp2)
2028        pbu)).
2029
2030lemma Some_Some_elim:
2031 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
2032 #T #x #y #P #H #K @H @option_destruct_Some //
2033qed.
2034
2035theorem main_thm:
2036 ∀M,M',ps,pol.
2037  next_internal_pseudo_address_map M ps = Some … M' →
2038   ∃n.
2039      execute n (status_of_pseudo_status M ps pol)
2040    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
2041 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
2042 #M #M' #ps #pol #SAFE
2043 cut
2044  (∀ps'.
2045    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
2046    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
2047 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
2048 #ps' #EQ
2049 whd in ⊢ (??(λ_.??(??%)?))
2050 change with
2051  (∃n.
2052    execute n
2053     (set_low_internal_ram ?
2054       (set_high_internal_ram ?
2055         (set_program_counter ?
2056           (set_code_memory ?? ps (load_code_memory ?))
2057          (sigma ? pol (program_counter ? ps)))
2058        (high_internal_ram_of_pseudo_high_internal_ram M ?))
2059      (low_internal_ram_of_pseudo_low_internal_ram M ?))
2060   = set_low_internal_ram ?
2061      (set_high_internal_ram ?
2062        (set_program_counter ?
2063          (set_code_memory ?? ? (load_code_memory ?))
2064         (sigma ???)) ?) ?)
2065 >EQ whd in match eq_rect_Type0_r normalize nodelta
2066 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
2067 generalize in match EQ -EQ;
2068 generalize in match (refl … (code_memory pseudo_assembly_program ps))
2069 generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
2070 * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
2071 (* Dependent types madness ends here *)
2072 letin ppc ≝ (program_counter … ps)
2073 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
2074 letin assembled ≝ (\fst (assembly ? pol))
2075 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
2076 letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
2077 @pair_elim' #pi #newppc #EQ2
2078 letin instructions ≝
2079  (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
2080    (sigma ? pol ppc) (refl …) (refl …) (refl …))
2081 change with (fetch_many ???? → ?) #H1
2082 change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
2083 change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
2084 >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
2085 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
2086 generalize in match H1; -H1; generalize in match instructions -instructions
2087 * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi
2088 whd in match ticks_of normalize nodelta <EQ1 >EQ2
2089 cases pi in SAFE
2090  [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?)
2091   @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
2092   whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
2093   #H2 #EQ %[1,3:@0]
2094   <MAP >(eq_bv_eq … H2) >EQ %
2095  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
2096   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
2097       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
2098         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
2099         @pair_elim' * #instr #newppc' #ticks #EQ4       
2100         * * #H2a #H2b whd in ⊢ (% → ?) #H2
2101         >H2b >(eq_instruction_to_eq … H2a)
2102         #EQ %[@1]
2103         <MAP >(eq_bv_eq … H2) >EQ
2104         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
2105         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
2106         whd in ⊢ (??%?)
2107         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
2108         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2109  |6: (* Mov *) #arg1 #arg2
2110       #H1 #H2 #EQ %[@1]
2111       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2112       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2113       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2114       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2115       >H2b >(eq_instruction_to_eq … H2a)
2116       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2117       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2118       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2119       normalize nodelta;
2120       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2121       #result #flags
2122       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2123  |5: (* Call *) #label #MAP
2124      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
2125      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2126       [ (* short *) #abs @⊥ destruct (abs)
2127       |3: (* long *) #H1 #H2 #EQ %[@1]
2128           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2129           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2130           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2131           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2132           >H2b >(eq_instruction_to_eq … H2a)
2133           generalize in match EQ; -EQ;
2134           whd in ⊢ (???% → ??%?);
2135           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;
2136           >(eq_bv_eq … H2c)
2137           change with
2138            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
2139                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2140           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
2141           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;
2142           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
2143           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
2144           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
2145           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2146           @split_eq_status;
2147            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
2148              >code_memory_write_at_stack_pointer %
2149            | >set_program_counter_set_low_internal_ram
2150              >set_clock_set_low_internal_ram
2151              @low_internal_ram_write_at_stack_pointer
2152               [ >EQ0 @pol | % | %
2153               | @(pair_destruct_2 … EQ1)
2154               | @(pair_destruct_2 … EQ2)
2155               | >(pair_destruct_1 ????? EQpc)
2156                 >(pair_destruct_2 ????? EQpc)
2157                 @split_elim #x #y #H <H -x y H;
2158                 >(pair_destruct_1 ????? EQppc)
2159                 >(pair_destruct_2 ????? EQppc)
2160                 @split_elim #x #y #H <H -x y H;
2161                 >EQ0 % ]
2162            | >set_low_internal_ram_set_high_internal_ram
2163              >set_program_counter_set_high_internal_ram
2164              >set_clock_set_high_internal_ram
2165              @high_internal_ram_write_at_stack_pointer
2166               [ >EQ0 @pol | % | %
2167               | @(pair_destruct_2 … EQ1)
2168               | @(pair_destruct_2 … EQ2)
2169               | >(pair_destruct_1 ????? EQpc)
2170                 >(pair_destruct_2 ????? EQpc)
2171                 @split_elim #x #y #H <H -x y H;
2172                 >(pair_destruct_1 ????? EQppc)
2173                 >(pair_destruct_2 ????? EQppc)
2174                 @split_elim #x #y #H <H -x y H;
2175                 >EQ0 % ]           
2176            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
2177              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2178              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2179              >external_ram_write_at_stack_pointer %
2180            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
2181              >EQ0 %
2182            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
2183              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2184              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2185              >special_function_registers_8051_write_at_stack_pointer %
2186            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
2187              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2188              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2189              >special_function_registers_8052_write_at_stack_pointer %
2190            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
2191              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2192              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2193              >p1_latch_write_at_stack_pointer %
2194            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
2195              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2196              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2197              >p3_latch_write_at_stack_pointer %
2198            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
2199              >clock_write_at_stack_pointer whd in ⊢ (???%)
2200              >clock_write_at_stack_pointer whd in ⊢ (???%)
2201              >clock_write_at_stack_pointer %]
2202       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2203         @pair_elim' #fst_5_addr #rest_addr #EQ1
2204         @pair_elim' #fst_5_pc #rest_pc #EQ2
2205         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2206         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2207         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2208         change in ⊢ (? →??%?) with (execute_1_0 ??)
2209         @pair_elim' * #instr #newppc' #ticks #EQn
2210          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
2211          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2212          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
2213          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
2214          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
2215          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
2216          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
2217          >get_8051_sfr_set_8051_sfr
2218         
2219          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2220           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2221           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2222           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2223           generalize in match (refl … (split bool 4 4 pc_bu))
2224           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2225           generalize in match (refl … (split bool 3 8 rest_addr))
2226           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2227           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2228           generalize in match
2229            (refl …
2230             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2231             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2232           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2233           @split_eq_status try %
2234            [ change with (? = sigma ? (address_of_word_labels ps label))
2235              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2236            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2237              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
2238  |4: (* Jmp *) #label #MAP
2239      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
2240      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
2241       [3: (* long *) #H1 #H2 #EQ %[@1]
2242           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2243           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2244           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2245           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2246           >H2b >(eq_instruction_to_eq … H2a)
2247           generalize in match EQ; -EQ;
2248           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2249           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2250       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2251           generalize in match
2252            (refl ?
2253             (sub_16_with_carry
2254              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
2255              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
2256              false))
2257           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2258           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2259           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2260           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2261           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2262           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2263           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2264           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2265           >H2b >(eq_instruction_to_eq … H2a)
2266           generalize in match EQ; -EQ;
2267           whd in ⊢ (???% → ?);
2268           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2269           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
2270           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
2271           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2272           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
2273           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2274       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2275         generalize in match
2276          (refl …
2277            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
2278         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2279         generalize in match
2280          (refl …
2281            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
2282         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2283         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2284         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2285         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2286         change in ⊢ (? →??%?) with (execute_1_0 ??)
2287           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2288           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2289           >H2b >(eq_instruction_to_eq … H2a)
2290           generalize in match EQ; -EQ;
2291           whd in ⊢ (???% → ?);
2292           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2293           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2294           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
2295           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2296           generalize in match (refl … (split bool 4 4 pc_bu))
2297           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2298           generalize in match (refl … (split bool 3 8 rest_addr))
2299           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2300           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2301           generalize in match
2302            (refl …
2303             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
2304             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2305           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
2306           @split_eq_status try %
2307            [ change with (? = sigma ?? (address_of_word_labels ps label))
2308              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2309            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2310              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2311  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
2312    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2313       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2314       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2315       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2316       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2317       >H2b >(eq_instruction_to_eq … H2a)
2318       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2319       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2320       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2321       normalize nodelta; #MAP;
2322       [1: change in ⊢ (? → %) with
2323        ((let 〈result,flags〉 ≝
2324          add_8_with_carry
2325           (get_arg_8 ? ps false ACC_A)
2326           (get_arg_8 ?
2327             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2328             false (DIRECT ARG2))
2329           ? in ?) = ?)
2330        [2,3: %]
2331        change in ⊢ (???% → ?) with
2332         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
2333        >get_arg_8_set_clock
2334       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
2335         [2,4: #abs @⊥ normalize in abs; destruct (abs)
2336         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
2337       [ change in ⊢ (? → %) with
2338        ((let 〈result,flags〉 ≝
2339          add_8_with_carry
2340           (get_arg_8 ? ps false ACC_A)
2341           (get_arg_8 ?
2342             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2343             false (DIRECT ARG2))
2344           ? in ?) = ?)
2345          >get_arg_8_set_low_internal_ram
2346       
2347        cases (add_8_with_carry ???)
2348         
2349        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2350       #result #flags
2351       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2352    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2353       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2354       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2355       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2356       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2357       >H2b >(eq_instruction_to_eq … H2a)
2358       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2359       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2360       [1,2,3,4: cases (half_add ???) #carry #result
2361       | cases (half_add ???) #carry #bl normalize nodelta;
2362         cases (full_add ????) #carry' #bu normalize nodelta ]
2363        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
2364        [5: %
2365        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2366      (set_program_counter pseudo_assembly_program ps newppc)
2367      (\fst  (ticks_of0 〈preamble,instr_list〉
2368                   (program_counter pseudo_assembly_program ps)
2369                   (Instruction (INC Identifier (DIRECT ARG))))
2370       +clock pseudo_assembly_program
2371        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2372        [2,3: // ]
2373            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2374            whd in ⊢ (??%%)
2375            cases (split bool 4 4 ARG)
2376            #nu' #nl'
2377            normalize nodelta
2378            cases (split bool 1 3 nu')
2379            #bit_1' #ignore'
2380            normalize nodelta
2381            cases (get_index_v bool 4 nu' ? ?)
2382            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2383            |
2384            ]
2385cases daemon (* EASY CASES TO BE COMPLETED *)
2386qed.
Note: See TracBrowser for help on using the repository browser.