source: src/ASM/AssemblyProof.ma @ 991

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

loads of axioms related to equality on instructions closed

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