source: src/ASM/AssemblyProof.ma @ 2093

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

sigma_policy_specification has been
1) strengthened
2) made nicer to see
3) moved to Assembly.ma
4) used into Policy

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