source: src/ASM/AssemblyProof.ma @ 988

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

Proof restored.

File size: 82.5 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.*)
417axiom eq_instruction: instruction → instruction → bool.
418axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
419
420let rec vect_member
421  (A: Type[0]) (n: nat) (eq: A → A → bool)
422  (v: Vector A n) (a: A) on v: bool ≝
423  match v with
424  [ VEmpty          ⇒ false
425  | VCons len hd tl ⇒
426    eq hd a ∨ (vect_member A ? eq tl a)
427  ].
428
429let rec list_addressing_mode_tags_elim_prop
430  (n: nat)
431  (l: Vector addressing_mode_tag (S n))
432  on l:
433  ∀P: l → Prop.
434  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
435  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
436  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
437  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
438  ∀x: l. P x ≝
439  match l return
440    λy.
441      match y with
442      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
443      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
444               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
445               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
446               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
447               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
448               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
449               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
450               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
451               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
452               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
453               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
454               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
455               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
456               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
457               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
458               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
459               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
460               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
461               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
462               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
463               ∀x:l. P x
464      ] with
465  [ VEmpty          ⇒ λAbsurd. ⊥
466  | VCons len hd tl ⇒ λProof. ?
467  ] (refl ? (S n)). cases daemon. qed. (*
468  [ destruct(Absurd)
469  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
470    # A8 # A9 # A10 # A11 # A12 # A13 # A14
471    # A15 # A16 # A17 # A18 # A19 # X
472    cases X
473    # SUB cases daemon ] qed.
474    cases SUB
475    [ # BYTE
476    normalize
477  ].
478 
479 
480(*    let prepare_hd ≝
481      match hd with
482      [ direct ⇒ λdirect_prf. ?
483      | indirect ⇒ λindirect_prf. ?
484      | ext_indirect ⇒ λext_indirect_prf. ?
485      | registr ⇒ λregistr_prf. ?
486      | acc_a ⇒ λacc_a_prf. ?
487      | acc_b ⇒ λacc_b_prf. ?
488      | dptr ⇒ λdptr_prf. ?
489      | data ⇒ λdata_prf. ?
490      | data16 ⇒ λdata16_prf. ?
491      | acc_dptr ⇒ λacc_dptr_prf. ?
492      | acc_pc ⇒ λacc_pc_prf. ?
493      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
494      | indirect_dptr ⇒ λindirect_prf. ?
495      | carry ⇒ λcarry_prf. ?
496      | bit_addr ⇒ λbit_addr_prf. ?
497      | n_bit_addr ⇒ λn_bit_addr_prf. ?
498      | relative ⇒ λrelative_prf. ?
499      | addr11 ⇒ λaddr11_prf. ?
500      | addr16 ⇒ λaddr16_prf. ?
501      ]
502    in ? *)
503  ].
504  [ 1: destruct(absd)
505  | 2: # A1 # A2 # A3 # A4 # A5 # A6
506       # A7 # A8 # A9 # A10 # A11 # A12
507       # A13 # A14 # A15 # A16 # A17 # A18
508       # A19 *
509  ].
510
511
512  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
513   (l → bool) → bool ] with
514  [ VEmpty      ⇒  true 
515  | VCons len hd tl ⇒ λP.
516    let process_hd ≝
517      match hd return λhd. ∀P: hd:::tl → bool. bool with
518      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
519      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
520      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
521      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
522      | acc_a ⇒ λP.P ACC_A
523      | acc_b ⇒ λP.P ACC_B
524      | dptr ⇒ λP.P DPTR
525      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
526      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
527      | acc_dptr ⇒ λP.P ACC_DPTR
528      | acc_pc ⇒ λP.P ACC_PC
529      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
530      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
531      | carry ⇒ λP.P CARRY
532      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
533      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
534      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
535      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
536      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
537      ]
538    in
539      andb (process_hd P)
540       (match len return λx. x = len → bool with
541         [ O ⇒ λprf. true
542         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
543  ].
544  try %
545  [ 2: cases (sym_eq ??? prf); @tl
546  | generalize in match H; generalize in match tl; cases prf;
547    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
548    #tl
549    normalize in ⊢ (∀_: %. ?)
550    # H
551    whd
552    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
553    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
554qed.
555*)
556
557definition load_code_memory_aux ≝
558 fold_left_i_aux … (
559   λi, mem, v.
560     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
561
562axiom split_elim:
563 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
564  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
565
566example half_add_SO:
567 ∀pc.
568 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
569 cases daemon.
570qed.
571
572(*
573axiom not_eqvb_S:
574 ∀pc.
575 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
576
577axiom not_eqvb_SS:
578 ∀pc.
579 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
580 
581axiom bitvector_elim_complete:
582 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
583
584lemma bitvector_elim_complete':
585 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
586 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
587 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
588qed.
589*)
590
591(*
592lemma andb_elim':
593 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
594 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
595qed.
596*)
597
598let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
599                       (encoding: list Byte) on encoding: Prop ≝
600  match encoding with
601  [ nil ⇒ final_pc = pc
602  | cons hd tl ⇒
603    let 〈new_pc, byte〉 ≝ next code_memory pc in
604      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
605  ].
606
607lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
608 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
609  let intermediate_pc ≝ pc + length … l1 in
610   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
611    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
612 #code_memory #final_pc #l1 elim l1
613  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
614  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
615    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
616qed.
617
618axiom bitvector_3_elim_prop:
619 ∀P: BitVector 3 → Prop.
620  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
621  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
622  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
623
624definition ticks_of_instruction ≝
625 λi.
626  let trivial_code_memory ≝ assembly1 i in
627  let trivial_status ≝ load_code_memory trivial_code_memory in
628   \snd (fetch trivial_status (zero ?)).
629
630axiom fetch_assembly:
631  ∀pc,i,code_memory,assembled.
632    assembled = assembly1 i →
633      let len ≝ length … assembled in
634      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
635      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
636      let 〈instr_pc, ticks〉 ≝ fetched in
637      let 〈instr,pc'〉 ≝ instr_pc in
638       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
639(* #pc #i #code_memory #assembled cases i [8: *]
640 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
641 [47,48,49:
642 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
643  [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,
644   59,60,63,64,65,66,67: #ARG]]
645 [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,
646  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
647  [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,
648   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,
649   68,69,70,71: #ARG2]]
650 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
651 normalize in ⊢ (???% → ?)
652 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
653  normalize in ⊢ (???% → ?)]
654 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
655 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
656 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
657 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
658 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
659 [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,
660  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,
661  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
662 whd >eq_instruction_refl >H4 @eq_bv_refl
663qed. *)
664
665let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
666 match expected with
667  [ nil ⇒ eq_bv … pc final_pc = true
668  | cons i tl ⇒
669     let fetched ≝ fetch code_memory pc in
670     let 〈instr_pc, ticks〉 ≝ fetched in
671     let 〈instr,pc'〉 ≝ instr_pc in
672      eq_instruction instr i = true ∧
673      ticks = (ticks_of_instruction i) ∧
674      fetch_many code_memory final_pc pc' tl].
675
676lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
677 #A #a #b #EQ destruct //
678qed.
679
680axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
681
682lemma fetch_assembly_pseudo:
683 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
684  ∀pi,code_memory,len,assembled,instructions,pc.
685   let expansion ≝ pol ppc in
686   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
687    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
688     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
689      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
690 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
691 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
692 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
693 >EQ2a >EQ2b -EQ2a EQ2b;
694  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
695  generalize in match pc elim instructions
696  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
697  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
698    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
699    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
700    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
701    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
702    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
703qed.
704
705(*
706lemma rev_preserves_length:
707 ∀A.∀l. length … (rev A l) = length … l.
708  #A #l elim l
709   [ %
710   | #hd #tl #IH normalize >length_append normalize /2/ ]
711qed.
712
713lemma rev_append:
714 ∀A.∀l1,l2.
715  rev A (l1@l2) = rev A l2 @ rev A l1.
716 #A #l1 elim l1 normalize //
717qed.
718 
719lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
720 #A #l elim l
721  [ //
722  | #hd #tl #IH normalize >rev_append normalize // ]
723qed.
724
725lemma split_len_Sn:
726 ∀A:Type[0].∀l:list A.∀len.
727  length … l = S len →
728   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
729 #A #l elim l
730  [ normalize #len #abs destruct
731  | #hd #tl #IH #len
732    generalize in match (rev_rev … tl)
733    cases (rev A tl) in ⊢ (??%? → ?)
734     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
735     | #a #l' #H <H normalize #EQ
736      %[@(hd::rev … l')] %[@a] % //
737      >length_append in EQ #EQ normalize in EQ; normalize;
738      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
739qed.
740
741lemma list_elim_rev:
742 ∀A:Type[0].∀P:list A → Type[0].
743  P [ ] → (∀l,a. P l → P (l@[a])) →
744   ∀l. P l.
745 #A #P #H1 #H2 #l
746 generalize in match (refl … (length … l))
747 generalize in ⊢ (???% → ?) #n generalize in match l
748 elim n
749  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
750  | #m #IH #L #EQ
751    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
752qed.
753
754axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
755axiom prefix_of_append:
756 ∀A:Type[0].∀l,l1,l2:list A.
757  is_prefix … l l1 → is_prefix … l (l1@l2).
758axiom prefix_reflexive: ∀A,l. is_prefix A l l.
759axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
760
761record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
762
763definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
764 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
765
766definition app ≝
767 λA:Type[0].λl1:Propify (list A).λl2:list A.
768  match l1 with
769   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
770
771lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
772 #A * /3/
773qed.
774
775lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
776 #A * #l1 normalize //
777qed.
778*)
779
780axiom assembly_ok:
781 ∀program,pol,assembled.
782  let 〈labels,costs〉 ≝ build_maps program pol in
783  Some … 〈assembled,costs〉 = assembly program pol →
784  let code_memory ≝ load_code_memory assembled in
785  let preamble ≝ \fst program in
786  let datalabels ≝ construct_datalabels preamble in
787  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
788  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
789   ∀ppc,len,assembledi.
790    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
791     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
792      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
793       sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
794
795axiom bitvector_of_nat_nat_of_bitvector:
796  ∀n,v.
797    bitvector_of_nat n (nat_of_bitvector n v) = v.
798
799axiom assembly_ok_to_expand_pseudo_instruction_ok:
800 ∀program,pol,assembled,costs.
801  Some … 〈assembled,costs〉 = assembly program pol →
802   ∀ppc.
803    let code_memory ≝ load_code_memory assembled in
804    let preamble ≝ \fst program in   
805    let data_labels ≝ construct_datalabels preamble in
806    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
807    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
808    let expansion ≝ pol ppc in
809    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
810     ∃instructions.
811      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
812
813axiom pair_elim':
814  ∀A,B,C: Type[0].
815  ∀T: A → B → C.
816  ∀p.
817  ∀P: A×B → C → Prop.
818    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
819      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
820
821axiom pair_elim'':
822  ∀A,B,C,C': Type[0].
823  ∀T: A → B → C.
824  ∀T': A → B → C'.
825  ∀p.
826  ∀P: A×B → C → C' → Prop.
827    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
828      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
829
830axiom split_elim':
831  ∀A: Type[0].
832  ∀B: Type[1].
833  ∀l, m, v.
834  ∀T: Vector A l → Vector A m → B.
835  ∀P: B → Prop.
836    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
837      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
838
839axiom split_elim'':
840  ∀A: Type[0].
841  ∀B,B': Type[1].
842  ∀l, m, v.
843  ∀T: Vector A l → Vector A m → B.
844  ∀T': Vector A l → Vector A m → B'.
845  ∀P: B → B' → Prop.
846    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
847      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
848        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
849
850lemma fetch_assembly_pseudo2:
851 ∀program,pol,assembled.
852  let 〈labels,costs〉 ≝ build_maps program pol in
853  Some … 〈assembled,costs〉 = assembly program pol →
854   ∀ppc.
855    let code_memory ≝ load_code_memory assembled in
856    let preamble ≝ \fst program in
857    let data_labels ≝ construct_datalabels preamble in
858    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
859    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
860    let expansion ≝ pol ppc in
861    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
862     ∃instructions.
863      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
864       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
865 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
867 letin code_memory ≝ (load_code_memory assembled)
868 letin preamble ≝ (\fst program)
869 letin data_labels ≝ (construct_datalabels preamble)
870 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
871 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
872 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
874 generalize in match (fetch_assembly_pseudo program pol ppc
875  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
876  (load_code_memory assembled));
877 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
878 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
879 normalize nodelta in EXPAND; (* HERE *)
880 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
881 >bitvector_of_nat_nat_of_bitvector in H1; #H1
882 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
883 #H1 #H2
884 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
885 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
886  [ #K3 % [2: % [% | @K3]] | @K1 ]
887qed.
888
889(* OLD?
890definition assembly_specification:
891  ∀assembly_program: pseudo_assembly_program.
892  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
893  λpseudo_assembly_program.
894  λcode_mem.
895    ∀pc: Word.
896      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
897      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
898      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
899      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
900      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
901       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
902      match pre_assembled with
903       [ None ⇒ True
904       | Some pc_code ⇒
905          let 〈new_pc,code〉 ≝ pc_code in
906           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
907
908axiom assembly_meets_specification:
909  ∀pseudo_assembly_program.
910    match assembly pseudo_assembly_program with
911    [ None ⇒ True
912    | Some code_mem_cost ⇒
913      let 〈code_mem, cost〉 ≝ code_mem_cost in
914        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
915    ].
916(*
917  # PROGRAM
918  [ cases PROGRAM
919    # PREAMBLE
920    # INSTR_LIST
921    elim INSTR_LIST
922    [ whd
923      whd in ⊢ (∀_. %)
924      # PC
925      whd
926    | # INSTR
927      # INSTR_LIST_TL
928      # H
929      whd
930      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
931    ]
932  | cases not_implemented
933  ] *)
934*)
935
936definition internal_pseudo_address_map ≝ list (BitVector 8).
937
938axiom low_internal_ram_of_pseudo_low_internal_ram:
939 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
940
941axiom high_internal_ram_of_pseudo_high_internal_ram:
942 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
943
944axiom low_internal_ram_of_pseudo_internal_ram_hit:
945 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
946  member ? (eq_bv 8) (false:::addr) M = true →
947   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
948   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
949   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
950   let bl ≝ lookup ? 7 addr ram (zero 8) in
951   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
952    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
953
954(* changed from add to sub *)
955axiom low_internal_ram_of_pseudo_internal_ram_miss:
956 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
957  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
958  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
959  let carr ≝ get_index_v ? ? flags 1 ? in
960  carr = false →
961  member ? (eq_bv 8) (false:::Saddr) M = false →
962   member ? (eq_bv 8) (false:::addr) M = false →
963    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
964  //
965qed.
966
967definition addressing_mode_ok ≝
968 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
969  λaddr:addressing_mode.
970   match addr with
971    [ DIRECT d ⇒
972       ¬(member ? (eq_bv 8) d M) ∧
973       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
974    | INDIRECT i ⇒
975       let d ≝ get_register ? s [[false;false;i]] in
976       ¬(member ? (eq_bv 8) d M) ∧
977       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
978    | EXT_INDIRECT _ ⇒ true
979    | REGISTER _ ⇒ true
980    | ACC_A ⇒ true
981    | ACC_B ⇒ true
982    | DPTR ⇒ true
983    | DATA _ ⇒ true
984    | DATA16 _ ⇒ true
985    | ACC_DPTR ⇒ true
986    | ACC_PC ⇒ true
987    | EXT_INDIRECT_DPTR ⇒ true
988    | INDIRECT_DPTR ⇒ true
989    | CARRY ⇒ true
990    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
991    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
992    | RELATIVE _ ⇒ true
993    | ADDR11 _ ⇒ true
994    | ADDR16 _ ⇒ true ].
995   
996definition next_internal_pseudo_address_map0 ≝
997  λT.
998  λfetched.
999  λM: internal_pseudo_address_map.
1000  λs: PreStatus T.
1001   match fetched with
1002    [ Comment _ ⇒ Some ? M
1003    | Cost _ ⇒ Some … M
1004    | Jmp _ ⇒ Some … M
1005    | Call _ ⇒
1006       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1007    | Mov _ _ ⇒ Some … M
1008    | Instruction instr ⇒
1009       match instr with
1010        [ ADD addr1 addr2 ⇒
1011           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1012            Some ? M
1013           else
1014            None ?
1015        | ADDC addr1 addr2 ⇒
1016           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1017            Some ? M
1018           else
1019            None ?
1020        | SUBB addr1 addr2 ⇒
1021           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1022            Some ? M
1023           else
1024            None ?       
1025        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1026 
1027
1028definition next_internal_pseudo_address_map ≝
1029 λM:internal_pseudo_address_map.
1030  λs:PseudoStatus.
1031    next_internal_pseudo_address_map0 ?
1032     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1033   
1034definition status_of_pseudo_status:
1035 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
1036 λM,ps,pol.
1037  let pap ≝ code_memory … ps in
1038   match assembly pap pol with
1039    [ None ⇒ None …
1040    | Some p ⇒
1041       let cm ≝ load_code_memory (\fst p) in
1042       let pc ≝ sigma pap pol (program_counter ? ps) in
1043       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1044       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1045        Some …
1046         (mk_PreStatus (BitVectorTrie Byte 16)
1047           cm
1048           lir
1049           hir
1050           (external_ram … ps)
1051           pc
1052           (special_function_registers_8051 … ps)
1053           (special_function_registers_8052 … ps)
1054           (p1_latch … ps)
1055           (p3_latch … ps)
1056           (clock … ps)) ].
1057
1058(*
1059definition write_at_stack_pointer':
1060 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1061  λM: Type[0].
1062  λs: PreStatus M.
1063  λv: Byte.
1064    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1065    let bit_zero ≝ get_index_v… nu O ? in
1066    let bit_1 ≝ get_index_v… nu 1 ? in
1067    let bit_2 ≝ get_index_v… nu 2 ? in
1068    let bit_3 ≝ get_index_v… nu 3 ? in
1069      if bit_zero then
1070        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1071                              v (low_internal_ram ? s) in
1072          set_low_internal_ram ? s memory
1073      else
1074        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1075                              v (high_internal_ram ? s) in
1076          set_high_internal_ram ? s memory.
1077  [ cases l0 %
1078  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1079qed.
1080
1081definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1082 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1083
1084  λticks_of.
1085  λs.
1086  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1087  let ticks ≝ ticks_of (program_counter ? s) in
1088  let s ≝ set_clock ? s (clock ? s + ticks) in
1089  let s ≝ set_program_counter ? s pc in
1090    match instr with
1091    [ Instruction instr ⇒
1092       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1093    | Comment cmt ⇒ s
1094    | Cost cst ⇒ s
1095    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1096    | Call call ⇒
1097      let a ≝ address_of_word_labels s call in
1098      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1099      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1100      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1101      let s ≝ write_at_stack_pointer' ? s pc_bl in
1102      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1103      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1104      let s ≝ write_at_stack_pointer' ? s pc_bu in
1105        set_program_counter ? s a
1106    | Mov dptr ident ⇒
1107       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1108    ].
1109 [
1110 |2,3,4: %
1111 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1112 |
1113 | %
1114 ]
1115 cases not_implemented
1116qed.
1117*)
1118
1119axiom execute_1_pseudo_instruction_preserves_code_memory:
1120 ∀ticks_of,ps.
1121  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1122
1123(*
1124lemma execute_code_memory_unchanged:
1125 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1126 #ticks #ps whd in ⊢ (??? (??%))
1127 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1128  (program_counter pseudo_assembly_program ps)) #instr #pc
1129 whd in ⊢ (??? (??%)) cases instr
1130  [ #pre cases pre
1131     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1132       cases (split ????) #z1 #z2 %
1133     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1134       cases (split ????) #z1 #z2 %
1135     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1136       cases (split ????) #z1 #z2 %
1137     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1138       [ #x1 whd in ⊢ (??? (??%))
1139     | *: cases not_implemented
1140     ]
1141  | #comment %
1142  | #cost %
1143  | #label %
1144  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1145    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1146    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1147    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1148    (* CSC: ??? *)
1149  | #dptr #label (* CSC: ??? *)
1150  ]
1151  cases not_implemented
1152qed.
1153*)
1154
1155lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1156 ∀M:internal_pseudo_address_map.
1157 ∀ps,ps': PseudoStatus.
1158 ∀pol.
1159  ∀prf:code_memory … ps = code_memory … ps'.
1160   let pol' ≝ ? in
1161   match status_of_pseudo_status M ps pol with
1162    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1163    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1164    ].
1165 [2: <prf @pol]
1166 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1167 generalize in match (refl … (assembly (code_memory … ps) pol))
1168 cases (assembly ??) in ⊢ (???% → %)
1169  [ #K whd whd in ⊢ (??%?) <H >K %
1170  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1171qed.
1172
1173definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
1174  λprogram: pseudo_assembly_program.λpol.
1175  λppc: Word.
1176  λfetched.
1177    match fetched with
1178    [ Instruction instr ⇒
1179      match instr with
1180      [ JC lbl ⇒
1181        match pol ppc with
1182        [ short_jump ⇒ 〈2, 2〉
1183        | medium_jump ⇒ ?
1184        | long_jump ⇒ 〈4, 4〉
1185        ]
1186      | JNC lbl ⇒
1187        match pol ppc with
1188        [ short_jump ⇒ 〈2, 2〉
1189        | medium_jump ⇒ ?
1190        | long_jump ⇒ 〈4, 4〉
1191        ]
1192      | JB bit lbl ⇒
1193        match pol ppc with
1194        [ short_jump ⇒ 〈2, 2〉
1195        | medium_jump ⇒ ?
1196        | long_jump ⇒ 〈4, 4〉
1197        ]
1198      | JNB bit lbl ⇒
1199        match pol ppc with
1200        [ short_jump ⇒ 〈2, 2〉
1201        | medium_jump ⇒ ?
1202        | long_jump ⇒ 〈4, 4〉
1203        ]
1204      | JBC bit lbl ⇒
1205        match pol ppc with
1206        [ short_jump ⇒ 〈2, 2〉
1207        | medium_jump ⇒ ?
1208        | long_jump ⇒ 〈4, 4〉
1209        ]
1210      | JZ lbl ⇒
1211        match pol ppc with
1212        [ short_jump ⇒ 〈2, 2〉
1213        | medium_jump ⇒ ?
1214        | long_jump ⇒ 〈4, 4〉
1215        ]
1216      | JNZ lbl ⇒
1217        match pol ppc with
1218        [ short_jump ⇒ 〈2, 2〉
1219        | medium_jump ⇒ ?
1220        | long_jump ⇒ 〈4, 4〉
1221        ]
1222      | CJNE arg lbl ⇒
1223        match pol ppc with
1224        [ short_jump ⇒ 〈2, 2〉
1225        | medium_jump ⇒ ?
1226        | long_jump ⇒ 〈4, 4〉
1227        ]
1228      | DJNZ arg lbl ⇒
1229        match pol ppc with
1230        [ short_jump ⇒ 〈2, 2〉
1231        | medium_jump ⇒ ?
1232        | long_jump ⇒ 〈4, 4〉
1233        ]
1234      | ADD arg1 arg2 ⇒
1235        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1236         〈ticks, ticks〉
1237      | ADDC arg1 arg2 ⇒
1238        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1239         〈ticks, ticks〉
1240      | SUBB arg1 arg2 ⇒
1241        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1242         〈ticks, ticks〉
1243      | INC arg ⇒
1244        let ticks ≝ ticks_of_instruction (INC ? arg) in
1245         〈ticks, ticks〉
1246      | DEC arg ⇒
1247        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1248         〈ticks, ticks〉
1249      | MUL arg1 arg2 ⇒
1250        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1251         〈ticks, ticks〉
1252      | DIV arg1 arg2 ⇒
1253        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1254         〈ticks, ticks〉
1255      | DA arg ⇒
1256        let ticks ≝ ticks_of_instruction (DA ? arg) in
1257         〈ticks, ticks〉
1258      | ANL arg ⇒
1259        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1260         〈ticks, ticks〉
1261      | ORL arg ⇒
1262        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1263         〈ticks, ticks〉
1264      | XRL arg ⇒
1265        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1266         〈ticks, ticks〉
1267      | CLR arg ⇒
1268        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1269         〈ticks, ticks〉
1270      | CPL arg ⇒
1271        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1272         〈ticks, ticks〉
1273      | RL arg ⇒
1274        let ticks ≝ ticks_of_instruction (RL ? arg) in
1275         〈ticks, ticks〉
1276      | RLC arg ⇒
1277        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1278         〈ticks, ticks〉
1279      | RR arg ⇒
1280        let ticks ≝ ticks_of_instruction (RR ? arg) in
1281         〈ticks, ticks〉
1282      | RRC arg ⇒
1283        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1284         〈ticks, ticks〉
1285      | SWAP arg ⇒
1286        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1287         〈ticks, ticks〉
1288      | MOV arg ⇒
1289        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1290         〈ticks, ticks〉
1291      | MOVX arg ⇒
1292        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1293         〈ticks, ticks〉
1294      | SETB arg ⇒
1295        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1296         〈ticks, ticks〉
1297      | PUSH arg ⇒
1298        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1299         〈ticks, ticks〉
1300      | POP arg ⇒
1301        let ticks ≝ ticks_of_instruction (POP ? arg) in
1302         〈ticks, ticks〉
1303      | XCH arg1 arg2 ⇒
1304        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1305         〈ticks, ticks〉
1306      | XCHD arg1 arg2 ⇒
1307        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1308         〈ticks, ticks〉
1309      | RET ⇒
1310        let ticks ≝ ticks_of_instruction (RET ?) in
1311         〈ticks, ticks〉
1312      | RETI ⇒
1313        let ticks ≝ ticks_of_instruction (RETI ?) in
1314         〈ticks, ticks〉
1315      | NOP ⇒
1316        let ticks ≝ ticks_of_instruction (NOP ?) in
1317         〈ticks, ticks〉
1318      ]
1319    | Comment comment ⇒ 〈0, 0〉
1320    | Cost cost ⇒ 〈0, 0〉
1321    | Jmp jmp ⇒ 〈2, 2〉
1322    | Call call ⇒ 〈2, 2〉
1323    | Mov dptr tgt ⇒ 〈2, 2〉
1324    ].
1325  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1326qed.
1327
1328definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
1329  λprogram: pseudo_assembly_program.λpol.
1330  λppc: Word.
1331    let 〈preamble, pseudo〉 ≝ program in
1332    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1333     ticks_of0 program pol ppc fetched.
1334
1335lemma get_register_set_program_counter:
1336 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1337 #T #s #pc %
1338qed.
1339
1340lemma get_8051_sfr_set_program_counter:
1341 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1342 #T #s #pc %
1343qed.
1344
1345lemma get_bit_addressable_sfr_set_program_counter:
1346 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1347 #T #s #pc %
1348qed.
1349
1350lemma low_internal_ram_set_program_counter:
1351 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1352 #T #s #pc %
1353qed.
1354
1355lemma get_arg_8_set_program_counter:
1356 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
1357  ∀T,s,pc,b.∀arg:l.
1358   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
1359 [2,3: cases arg; *; normalize //]
1360 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
1361qed.
1362
1363lemma set_bit_addressable_sfr_set_code_memory:
1364  ∀T, U: Type[0].
1365  ∀ps: PreStatus ?.
1366  ∀code_mem.
1367  ∀x.
1368  ∀val.
1369  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
1370  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
1371  #T #U #ps #code_mem #x #val
1372  whd in ⊢ (??%?)
1373  whd in ⊢ (???(???%?))
1374  cases (eqb ? 128) [ normalize nodelta cases not_implemented
1375  | normalize nodelta
1376  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1377  | normalize nodelta
1378  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1379  | normalize nodelta
1380  cases (eqb ? 176) [ normalize nodelta %
1381  | normalize nodelta
1382  cases (eqb ? 153) [ normalize nodelta %
1383  | normalize nodelta
1384  cases (eqb ? 138) [ normalize nodelta %
1385  | normalize nodelta
1386  cases (eqb ? 139) [ normalize nodelta %
1387  | normalize nodelta
1388  cases (eqb ? 140) [ normalize nodelta %
1389  | normalize nodelta
1390  cases (eqb ? 141) [ normalize nodelta %
1391  | normalize nodelta
1392  cases (eqb ? 200) [ normalize nodelta %
1393  | normalize nodelta
1394  cases (eqb ? 202) [ normalize nodelta %
1395  | normalize nodelta
1396  cases (eqb ? 203) [ normalize nodelta %
1397  | normalize nodelta
1398  cases (eqb ? 204) [ normalize nodelta %
1399  | normalize nodelta
1400  cases (eqb ? 205) [ normalize nodelta %
1401  | normalize nodelta
1402  cases (eqb ? 135) [ normalize nodelta %
1403  | normalize nodelta
1404  cases (eqb ? 136) [ normalize nodelta %
1405  | normalize nodelta
1406  cases (eqb ? 137) [ normalize nodelta %
1407  | normalize nodelta
1408  cases (eqb ? 152) [ normalize nodelta %
1409  | normalize nodelta
1410  cases (eqb ? 168) [ normalize nodelta %
1411  | normalize nodelta
1412  cases (eqb ? 184) [ normalize nodelta %
1413  | normalize nodelta
1414  cases (eqb ? 129) [ normalize nodelta %
1415  | normalize nodelta
1416  cases (eqb ? 130) [ normalize nodelta %
1417  | normalize nodelta
1418  cases (eqb ? 131) [ normalize nodelta %
1419  | normalize nodelta
1420  cases (eqb ? 208) [ normalize nodelta %
1421  | normalize nodelta
1422  cases (eqb ? 224) [ normalize nodelta %
1423  | normalize nodelta
1424  cases (eqb ? 240) [ normalize nodelta %
1425  | normalize nodelta
1426    cases not_implemented
1427  ]]]]]]]]]]]]]]]]]]]]]]]]]]
1428qed.
1429
1430lemma set_arg_8_set_code_memory:
1431  ∀n:nat.
1432  ∀l:Vector addressing_mode_tag (S n).
1433    ¬(is_in ? l ACC_PC) →
1434    ∀T: Type[0].
1435    ∀U: Type[0].
1436    ∀ps: PreStatus ?.
1437    ∀code_mem.
1438    ∀val.
1439    ∀b: l.
1440  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
1441  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
1442  [2,3: cases b; *; normalize //]
1443  #n #l #prf #T #U #ps #code_mem #val * *;
1444  [*:
1445    [1,2,3,4,8,9,15,16,17,18,19: #x]
1446    try #y whd in ⊢ (??(%)?)
1447    whd in ⊢ (???(???(%)?))
1448    [1,2:
1449      cases (split bool 4 4 ?)
1450      #nu' #nl'
1451      normalize nodelta
1452      cases (split bool 1 3 nu')
1453      #bit1' #ignore'
1454      normalize nodelta
1455      cases (get_index_v bool 4 nu' 0 ?)
1456      [1,2,3,4:
1457        normalize nodelta
1458        try %
1459        try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
1460        try (normalize in ⊢ (???(???%?)))
1461      ]
1462    |3,4: %
1463    |*:
1464       try normalize nodelta
1465       normalize cases (not_implemented)
1466    ]
1467 ]
1468 
1469
1470qed.
1471
1472axiom set_arg_8_set_program_counter:
1473  ∀n:nat.
1474  ∀l:Vector addressing_mode_tag (S n).
1475    ¬(is_in ? l ACC_PC) →
1476    ∀T: Type[0].
1477    ∀ps: PreStatus ?.
1478    ∀pc.
1479    ∀val.
1480    ∀b: l.
1481  set_arg_8 ? (set_program_counter T ps pc) b val =
1482  set_program_counter T (set_arg_8 ? ps b val) pc.
1483  [1,2: cases b; *; normalize //]
1484qed.
1485 
1486
1487lemma get_arg_8_set_code_memory:
1488 ∀T1,T2,s,code_mem,b,arg.
1489   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
1490 #T1 #T2 #s #code_mem #b #arg %
1491qed.
1492
1493lemma set_code_memory_set_flags:
1494 ∀T1,T2,s,f1,f2,f3,code_mem.
1495  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
1496   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
1497 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
1498qed.
1499
1500lemma set_program_counter_set_flags:
1501 ∀T1,s,f1,f2,f3,pc.
1502  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
1503   set_flags … (set_program_counter … s pc) f1 f2 f3.
1504 #T1 #s #f1 #f2 #f3 #pc  %
1505qed.
1506
1507lemma program_counter_set_flags:
1508 ∀T1,s,f1,f2,f3.
1509  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
1510 #T1 #s #f1 #f2 #f3 %
1511qed.
1512
1513lemma special_function_registers_8051_write_at_stack_pointer:
1514 ∀T,s,x.
1515    special_function_registers_8051 T (write_at_stack_pointer T s x)
1516  = special_function_registers_8051 T s.
1517 #T #s #x whd in ⊢ (??(??%)?)
1518 cases (split ????) #nu #nl normalize nodelta;
1519 cases (get_index_v bool ????) %
1520qed.
1521
1522lemma get_8051_sfr_write_at_stack_pointer:
1523 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
1524 #T #s #x #y whd in ⊢ (??%%) //
1525qed.
1526
1527lemma code_memory_write_at_stack_pointer:
1528 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
1529 #T #s #x whd in ⊢ (??(??%)?)
1530 cases (split ????) #nu #nl normalize nodelta;
1531 cases (get_index_v bool ????) %
1532qed.
1533
1534axiom low_internal_ram_write_at_stack_pointer:
1535 ∀T1,T2,M,s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1536  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
1537  low_internal_ram ? s2 = low_internal_ram T2 s3 →
1538  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
1539  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
1540  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
1541   low_internal_ram T1
1542     (write_at_stack_pointer ?
1543       (set_8051_sfr ?
1544         (write_at_stack_pointer ?
1545           (set_8051_sfr ?
1546             (set_low_internal_ram ? s1
1547               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
1548             SFR_SP sp1)
1549          bl)
1550        SFR_SP sp2)
1551      bu)
1552   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1553      (low_internal_ram ?
1554       (write_at_stack_pointer ?
1555         (set_8051_sfr ?
1556           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
1557          SFR_SP sp2)
1558        pbu)).
1559       
1560axiom high_internal_ram_write_at_stack_pointer:
1561 ∀T1,T2,M,s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1562  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
1563  high_internal_ram ? s2 = high_internal_ram T2 s3 →
1564  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
1565  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
1566  bu@@bl = sigma (code_memory … s2) pol (pbu@@pbl) →
1567   high_internal_ram T1
1568     (write_at_stack_pointer ?
1569       (set_8051_sfr ?
1570         (write_at_stack_pointer ?
1571           (set_8051_sfr ?
1572             (set_high_internal_ram ? s1
1573               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
1574             SFR_SP sp1)
1575          bl)
1576        SFR_SP sp2)
1577      bu)
1578   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1579      (high_internal_ram ?
1580       (write_at_stack_pointer ?
1581         (set_8051_sfr ?
1582           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
1583          SFR_SP sp2)
1584        pbu)).
1585
1586lemma set_program_counter_set_low_internal_ram:
1587 ∀T,s,x,y.
1588  set_program_counter T (set_low_internal_ram … s x) y =
1589   set_low_internal_ram … (set_program_counter … s y) x.
1590 //
1591qed.
1592
1593lemma set_clock_set_low_internal_ram:
1594 ∀T,s,x,y.
1595  set_clock T (set_low_internal_ram … s x) y =
1596   set_low_internal_ram … (set_clock … s y) x.
1597 //
1598qed.
1599
1600lemma set_program_counter_set_high_internal_ram:
1601 ∀T,s,x,y.
1602  set_program_counter T (set_high_internal_ram … s x) y =
1603   set_high_internal_ram … (set_program_counter … s y) x.
1604 //
1605qed.
1606
1607lemma set_clock_set_high_internal_ram:
1608 ∀T,s,x,y.
1609  set_clock T (set_high_internal_ram … s x) y =
1610   set_high_internal_ram … (set_clock … s y) x.
1611 //
1612qed.
1613
1614lemma set_low_internal_ram_set_high_internal_ram:
1615 ∀T,s,x,y.
1616  set_low_internal_ram T (set_high_internal_ram … s x) y =
1617   set_high_internal_ram … (set_low_internal_ram … s y) x.
1618 //
1619qed.
1620
1621lemma external_ram_write_at_stack_pointer:
1622 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
1623 #T #s #x whd in ⊢ (??(??%)?)
1624 cases (split ????) #nu #nl normalize nodelta;
1625 cases (get_index_v bool ????) %
1626qed.
1627
1628lemma special_function_registers_8052_write_at_stack_pointer:
1629 ∀T,s,x.
1630    special_function_registers_8052 T (write_at_stack_pointer T s x)
1631  = special_function_registers_8052 T s.
1632 #T #s #x whd in ⊢ (??(??%)?)
1633 cases (split ????) #nu #nl normalize nodelta;
1634 cases (get_index_v bool ????) %
1635qed.
1636
1637lemma p1_latch_write_at_stack_pointer:
1638 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
1639 #T #s #x whd in ⊢ (??(??%)?)
1640 cases (split ????) #nu #nl normalize nodelta;
1641 cases (get_index_v bool ????) %
1642qed.
1643
1644lemma p3_latch_write_at_stack_pointer:
1645 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
1646 #T #s #x whd in ⊢ (??(??%)?)
1647 cases (split ????) #nu #nl normalize nodelta;
1648 cases (get_index_v bool ????) %
1649qed.
1650
1651lemma clock_write_at_stack_pointer:
1652 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
1653 #T #s #x whd in ⊢ (??(??%)?)
1654 cases (split ????) #nu #nl normalize nodelta;
1655 cases (get_index_v bool ????) %
1656qed.
1657
1658axiom get_index_v_set_index:
1659 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
1660
1661lemma get_8051_sfr_set_8051_sfr:
1662 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
1663 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
1664 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
1665qed.
1666
1667lemma program_counter_set_8051_sfr:
1668 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
1669 //
1670qed.
1671
1672lemma eq_rect_Type1_r:
1673  ∀A: Type[1].
1674  ∀a:A.
1675  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1676  #A #a #P #H #x #p
1677  generalize in match H
1678  generalize in match P
1679  cases p
1680  //
1681qed.
1682
1683lemma split_eq_status:
1684 ∀T.
1685 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
1686 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
1687  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
1688   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
1689   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
1690 //
1691qed.
1692
1693axiom split_append:
1694  ∀A: Type[0].
1695  ∀m, n: nat.
1696  ∀v, v': Vector A m.
1697  ∀q, q': Vector A n.
1698    let 〈v', q'〉 ≝ split A m n (v@@q) in
1699      v = v' ∧ q = q'.
1700
1701axiom split_vector_singleton:
1702  ∀A: Type[0].
1703  ∀n: nat.
1704  ∀v: Vector A (S n).
1705  ∀rest: Vector A n.
1706  ∀s: Vector A 1.
1707  ∀prf.
1708    v = s @@ rest →
1709    ((get_index_v A ? v 0 prf) ::: rest) = v.
1710
1711example sub_minus_one_seven_eight:
1712  ∀v: BitVector 7.
1713  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1714  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1715 cases daemon.
1716qed.
1717
1718lemma pair_destruct_1:
1719 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
1720 #A #B #a #b *; /2/
1721qed.
1722
1723lemma pair_destruct_2:
1724 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
1725 #A #B #a #b *; /2/
1726qed.
1727
1728(*
1729lemma blah:
1730  ∀m: internal_pseudo_address_map.
1731  ∀s: PseudoStatus.
1732  ∀arg: Byte.
1733  ∀b: bool.
1734    addressing_mode_ok m s (DIRECT arg) = true →
1735      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1736      get_arg_8 ? s b (DIRECT arg).
1737  [2, 3: normalize % ]
1738  #m #s #arg #b #hyp
1739  whd in ⊢ (??%%)
1740  @split_elim''
1741  #nu' #nl' #arg_nu_nl_eq
1742  normalize nodelta
1743  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1744  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1745  #get_index_v_eq
1746  normalize nodelta
1747  [2:
1748    normalize nodelta
1749    @split_elim''
1750    #bit_one' #three_bits' #bit_one_three_bit_eq
1751    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1752    normalize nodelta
1753    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1754    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1755    #Saddr #carr' #Saddr_carr_eq
1756    normalize nodelta
1757    #carr_hyp'
1758    @carr_hyp'
1759    [1:
1760    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1761        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1762        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1763        #member_eq
1764        normalize nodelta
1765        [2: #destr destruct(destr)
1766        |1: -carr_hyp';
1767            >arg_nu_nl_eq
1768            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1769            [1: >get_index_v_eq in ⊢ (??%? → ?)
1770            |2: @le_S @le_S @le_S @le_n
1771            ]
1772            cases (member (BitVector 8) ? (\fst ?) ?)
1773            [1: #destr normalize in destr; destruct(destr)
1774            |2:
1775            ]
1776        ]
1777    |3: >get_index_v_eq in ⊢ (??%?)
1778        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1779        >(split_vector_singleton … bit_one_three_bit_eq)
1780        <arg_nu_nl_eq
1781        whd in hyp:(??%?)
1782        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1783        normalize nodelta [*: #ignore @sym_eq ]
1784    ]
1785  |
1786  ].
1787*)
1788(*
1789map_address0 ... (DIRECT arg) = Some .. →
1790  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1791  get_arg_8 (internal_ram ...) (DIRECT arg)
1792
1793((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1794                     then Some internal_pseudo_address_map M 
1795                     else None internal_pseudo_address_map )
1796                    =Some internal_pseudo_address_map M')
1797*)
1798
1799lemma main_thm:
1800 ∀M,M',ps,s,s'',pol.
1801  next_internal_pseudo_address_map M ps = Some … M' →
1802  status_of_pseudo_status M ps pol = Some … s →
1803  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = Some … s'' →
1804   ∃n. execute n s = s''.
1805 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
1806 #M #M' #ps #s #s'' #pol
1807 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol)
1808 whd in ⊢ (? → ? → ??%? → ??%? → ?)
1809 >execute_1_pseudo_instruction_preserves_code_memory
1810 generalize in match (refl … (assembly (code_memory … ps) pol))
1811 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
1812 cases (build_maps (code_memory … ps) pol)
1813 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
1814 generalize in match pol; -pol;
1815 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%]
1816 #EQ0 #pol normalize nodelta;
1817 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
1818  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
1819 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
1820 #H generalize in match (H ? (refl …)) -H; #H;
1821 #MAP
1822 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
1823 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
1824 change with
1825  (∃n.
1826    execute n
1827     (set_low_internal_ram ?
1828       (set_high_internal_ram ?
1829         (set_program_counter ?
1830           (set_code_memory ?? ps (load_code_memory assembled))
1831          (sigma 〈preamble,instr_list〉 pol (program_counter ? ps)))
1832        (high_internal_ram_of_pseudo_high_internal_ram M ?))
1833      (low_internal_ram_of_pseudo_low_internal_ram M ?))
1834   = set_low_internal_ram ?
1835      (set_high_internal_ram ?
1836        (set_program_counter ?
1837          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
1838         (sigma ???))
1839       ?)
1840     ?)
1841 whd in match (\snd 〈preamble,instr_list〉) in H;
1842 whd in match (\fst 〈preamble,instr_list〉) in H;
1843 whd in match (\snd 〈final_pc,assembled〉) in H;
1844 whd in match (\snd 〈preamble,instr_list〉) in MAP;
1845 -s s'' labels costs final_ppc final_pc;
1846 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps)
1847 (* NICE STATEMENT HERE *)
1848 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
1849 #K <K generalize in match K; -K;
1850 (* STATEMENT WITH EQUALITY HERE *)
1851 whd in ⊢ (???(?%?) → ?)
1852 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
1853 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
1854 #pi #newppc normalize nodelta; #MAP * #instructions *;
1855 cases pi in MAP; normalize nodelta;
1856  [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
1857    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
1858    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1859    #H2 >(eq_bv_eq … H2) >EQ %
1860(*  |6: (* Mov *) #arg1 #arg2
1861       #H1 #H2 #EQ %[@1]
1862       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1863       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1864       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1865       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1866       >H2b >(eq_instruction_to_eq … H2a)
1867       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1868       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
1869       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1870       normalize nodelta;
1871       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1872       #result #flags
1873       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
1874  |5: (* Call *) #label #MAP
1875      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
1876      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1877       [ (* short *) #abs @⊥ destruct (abs)
1878       |3: (* long *) #H1 #H2 #EQ %[@1]
1879           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1880           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1881           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1882           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1883           >H2b >(eq_instruction_to_eq … H2a)
1884           generalize in match EQ; -EQ;
1885           whd in ⊢ (???% → ??%?);
1886           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;
1887           >(eq_bv_eq … H2c)
1888           change with
1889            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
1890                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1891           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
1892           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;
1893           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
1894           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
1895           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
1896           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1897           @split_eq_status;
1898            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
1899              >code_memory_write_at_stack_pointer %
1900            | >set_program_counter_set_low_internal_ram
1901              >set_clock_set_low_internal_ram
1902              @low_internal_ram_write_at_stack_pointer
1903               [ >EQ0 @pol | % | %
1904               | @(pair_destruct_2 … EQ1)
1905               | @(pair_destruct_2 … EQ2)
1906               | >(pair_destruct_1 ????? EQpc)
1907                 >(pair_destruct_2 ????? EQpc)
1908                 @split_elim #x #y #H <H -x y H;
1909                 >(pair_destruct_1 ????? EQppc)
1910                 >(pair_destruct_2 ????? EQppc)
1911                 @split_elim #x #y #H <H -x y H;
1912                 >EQ0 % ]
1913            | >set_low_internal_ram_set_high_internal_ram
1914              >set_program_counter_set_high_internal_ram
1915              >set_clock_set_high_internal_ram
1916              @high_internal_ram_write_at_stack_pointer
1917               [ >EQ0 @pol | % | %
1918               | @(pair_destruct_2 … EQ1)
1919               | @(pair_destruct_2 … EQ2)
1920               | >(pair_destruct_1 ????? EQpc)
1921                 >(pair_destruct_2 ????? EQpc)
1922                 @split_elim #x #y #H <H -x y H;
1923                 >(pair_destruct_1 ????? EQppc)
1924                 >(pair_destruct_2 ????? EQppc)
1925                 @split_elim #x #y #H <H -x y H;
1926                 >EQ0 % ]           
1927            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
1928              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1929              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1930              >external_ram_write_at_stack_pointer %
1931            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
1932              >EQ0 %
1933            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
1934              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1935              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1936              >special_function_registers_8051_write_at_stack_pointer %
1937            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
1938              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1939              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1940              >special_function_registers_8052_write_at_stack_pointer %
1941            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
1942              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1943              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1944              >p1_latch_write_at_stack_pointer %
1945            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
1946              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1947              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1948              >p3_latch_write_at_stack_pointer %
1949            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
1950              >clock_write_at_stack_pointer whd in ⊢ (???%)
1951              >clock_write_at_stack_pointer whd in ⊢ (???%)
1952              >clock_write_at_stack_pointer %]
1953       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1954         @pair_elim' #fst_5_addr #rest_addr #EQ1
1955         @pair_elim' #fst_5_pc #rest_pc #EQ2
1956         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1957         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1958         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1959         change in ⊢ (? →??%?) with (execute_1_0 ??)
1960         @pair_elim' * #instr #newppc' #ticks #EQn
1961          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
1962          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1963          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
1964          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
1965          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
1966          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
1967          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
1968          >get_8051_sfr_set_8051_sfr
1969         
1970          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1971           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
1972           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
1973           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1974           generalize in match (refl … (split bool 4 4 pc_bu))
1975           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1976           generalize in match (refl … (split bool 3 8 rest_addr))
1977           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1978           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1979           generalize in match
1980            (refl …
1981             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
1982             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1983           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
1984           @split_eq_status try %
1985            [ change with (? = sigma ? (address_of_word_labels ps label))
1986              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1987            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1988              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
1989  |4: (* Jmp *) #label #MAP
1990      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
1991      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1992       [3: (* long *) #H1 #H2 #EQ %[@1]
1993           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1994           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1995           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1996           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1997           >H2b >(eq_instruction_to_eq … H2a)
1998           generalize in match EQ; -EQ;
1999           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2000           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2001       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2002           generalize in match
2003            (refl ?
2004             (sub_16_with_carry
2005              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
2006              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
2007              false))
2008           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2009           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2010           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2011           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2012           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2013           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2014           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2015           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2016           >H2b >(eq_instruction_to_eq … H2a)
2017           generalize in match EQ; -EQ;
2018           whd in ⊢ (???% → ?);
2019           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
2020           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
2021           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
2022           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2023           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
2024           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2025       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2026         generalize in match
2027          (refl …
2028            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
2029         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2030         generalize in match
2031          (refl …
2032            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
2033         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2034         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2035         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2036         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2037         change in ⊢ (? →??%?) with (execute_1_0 ??)
2038           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2039           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2040           >H2b >(eq_instruction_to_eq … H2a)
2041           generalize in match EQ; -EQ;
2042           whd in ⊢ (???% → ?);
2043           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
2044           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
2045           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
2046           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2047           generalize in match (refl … (split bool 4 4 pc_bu))
2048           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2049           generalize in match (refl … (split bool 3 8 rest_addr))
2050           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2051           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2052           generalize in match
2053            (refl …
2054             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
2055             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2056           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
2057           @split_eq_status try %
2058            [ change with (? = sigma ?? (address_of_word_labels ps label))
2059              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2060            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2061              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2062  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
2063    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2064       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2065       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2066       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2067       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2068       >H2b >(eq_instruction_to_eq … H2a)
2069       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2070       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2071       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2072       normalize nodelta; #MAP;
2073       [1: change in ⊢ (? → %) with
2074        ((let 〈result,flags〉 ≝
2075          add_8_with_carry
2076           (get_arg_8 ? ps false ACC_A)
2077           (get_arg_8 ?
2078             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2079             false (DIRECT ARG2))
2080           ? in ?) = ?) //
2081       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
2082        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
2083       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2084       #result #flags
2085       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
2086    (*| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2087       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2088       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2089       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2090       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2091       >H2b >(eq_instruction_to_eq … H2a)
2092       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2093       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2094       [1,2,3,4: cases (half_add ???) #carry #result
2095       | cases (half_add ???) #carry #bl normalize nodelta;
2096         cases (full_add ????) #carry' #bu normalize nodelta ]
2097        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
2098        [5: %
2099        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2100      (set_program_counter pseudo_assembly_program ps newppc)
2101      (\fst  (ticks_of0 〈preamble,instr_list〉
2102                   (program_counter pseudo_assembly_program ps)
2103                   (Instruction (INC Identifier (DIRECT ARG))))
2104       +clock pseudo_assembly_program
2105        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2106        [2,3: // ]
2107            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2108            whd in ⊢ (??%%)
2109            cases (split bool 4 4 ARG)
2110            #nu' #nl'
2111            normalize nodelta
2112            cases (split bool 1 3 nu')
2113            #bit_1' #ignore'
2114            normalize nodelta
2115            cases (get_index_v bool 4 nu' ? ?)
2116            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2117            |
2118            ] *)
Note: See TracBrowser for help on using the repository browser.