source: src/ASM/AssemblyProof.ma @ 2057

Last change on this file since 2057 was 2057, checked in by sacerdot, 7 years ago

Repaired (was broken by fetch_pseudo_instruction now taking a proof obligation)

File size: 78.0 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
1481definition sigma_policy_specification ≝
1482  λprogram: pseudo_assembly_program.
1483  λsigma: Word → Word.
1484  λpolicy: Word → bool.
1485  ∀ppc: Word. ∀ppc_ok.
1486    let instr_list ≝ \snd program in
1487    let pc ≝ sigma ppc in
1488    let labels ≝ \fst (create_label_cost_map instr_list) in
1489    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
1490    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
1491    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
1492      And (nat_of_bitvector … ppc ≤ |instr_list| →
1493        next_pc = add 16 pc (bitvector_of_nat …
1494          (instruction_size lookup_labels sigma policy ppc instruction)))
1495       (Or (nat_of_bitvector … ppc < |instr_list| →
1496         nat_of_bitvector … pc < nat_of_bitvector … next_pc)
1497        (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
1498
1499(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
1500   function that load the code in memory is correct. The latter is based
1501   on missing properties from the standard library on the BitVectorTrie
1502   data structrure.
1503   
1504   Wrong at the moment, requires Jaap's precondition to ensure that the program
1505   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1506*)
1507
1508lemma load_code_memory_ok:
1509 ∀program.
1510 let program_size ≝ |program| in
1511  program_size ≤ 2^16 →
1512   ∀pc. ∀pc_ok: pc < program_size.
1513    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1514 #program elim program
1515 [ #_ #pc #abs normalize in abs; @⊥ /2/
1516 | #hd #tl #IH #size_ok *
1517   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
1518     whd in match next; normalize nodelta
1519   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
1520     whd in match next; normalize nodelta
1521   ]
1522 cases daemon (*CSC: complete! *)
1523qed.
1524(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
1525Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
1526e' come fetchare l'i-esimo bit dalla memoria.
1527Concludere assembly_ok come semplice corollario.
1528*)
1529lemma assembly_ok:
1530  ∀program.
1531  ∀sigma: Word → Word.
1532  ∀policy: Word → bool.
1533  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
1534  ∀assembled.
1535  ∀costs': BitVectorTrie costlabel 16.
1536  let 〈preamble, instr_list〉 ≝ program in
1537  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
1538  let datalabels ≝ construct_datalabels preamble in
1539  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1540    〈assembled,costs'〉 = assembly program sigma policy →
1541      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
1542        let code_memory ≝ load_code_memory assembled in
1543        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
1544          ∀ppc.∀ppc_ok.
1545            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
1546            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1547            let pc ≝ sigma ppc in
1548            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1549              encoding_check code_memory pc pc_plus_len assembled ∧
1550                  sigma newppc = add … pc (bitvector_of_nat … len).
1551  #program #sigma #policy #sigma_policy_witness #assembled #costs'
1552  cases (assembly program sigma policy) * #assembled' #costs''
1553  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
1554  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
1555  #assembly_ok #Pair_eq destruct(Pair_eq) whd
1556  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
1557  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
1558  lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok
1559  >eq_fetch_pseudo_instruction
1560  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
1561  >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉)
1562   [2: (*CSC: Provable, isn't it?*) cases daemon
1563   | whd in ⊢ (% → ?); #assembly_ok
1564  %
1565  [2: (*CSC: Use Jaap's invariant here *) cases daemon
1566  | lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon]
1567    #load_code_memory_ok
1568    -eq_assembly_1_pseudoinstruction -program -policy -costs'' -labels -preamble -instr_list -costs -pi -newppc
1569    cut (len=|assembled|) [(*CSC: provable before cleaning*) cases daemon] #EQlen
1570    (* Nice statement here *)
1571    cut (∀j. ∀H: j < |assembled|.
1572          nth_safe Byte j assembled H =
1573          \snd (next (load_code_memory assembled')
1574          (bitvector_of_nat 16
1575           (nat_of_bitvector …
1576            (add … (sigma ppc) (bitvector_of_nat … j))))))
1577    [(*CSC: is it provable?*) cases daemon
1578    | -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
1579      elim assembled
1580       [ #pc #_ whd <add_zero %
1581       | #hd #tl #IH #pc #H %
1582         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
1583           >H -H whd in ⊢ (??%?); <add_zero //
1584         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
1585           [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]
1586           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
1587           <(nth_safe_prepend … [hd] … LTj) #IH >IH
1588           (*CSC: TRUE, ARITHMETICS*)
1589           cases daemon
1590         ]
1591    ]
1592qed.
1593
1594(* XXX: should we add that costs = costs'? *)
1595lemma fetch_assembly_pseudo2:
1596  ∀program.
1597  ∀sigma.
1598  ∀policy.
1599  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1600  ∀ppc.∀ppc_ok.
1601  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1602  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
1603  let code_memory ≝ load_code_memory assembled in
1604  let data_labels ≝ construct_datalabels (\fst program) in
1605  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
1606  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
1607  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1608  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1609    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
1610  * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
1611  @pair_elim #labels #costs #create_label_map_refl
1612  @pair_elim #assembled #costs' #assembled_refl
1613  letin code_memory ≝ (load_code_memory ?)
1614  letin data_labels ≝ (construct_datalabels ?)
1615  letin lookup_labels ≝ (λx. ?)
1616  letin lookup_datalabels ≝ (λx. ?)
1617  @pair_elim #pi #newppc #fetch_pseudo_refl
1618  lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs')
1619  normalize nodelta
1620  @pair_elim #labels' #costs' #create_label_map_refl' #H
1621  lapply (H (sym_eq … assembled_refl)) -H
1622  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1623  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
1624  #len #assembledi #EQ4 #H
1625  lapply (H ppc) >fetch_pseudo_refl #H
1626  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
1627  >EQ4 #H1 cases (H ppc_ok)
1628  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
1629  >fetch_pseudo_refl in H1; #assm @assm assumption
1630qed.
1631
1632(* OLD?
1633definition assembly_specification:
1634  ∀assembly_program: pseudo_assembly_program.
1635  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1636  λpseudo_assembly_program.
1637  λcode_mem.
1638    ∀pc: Word.
1639      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1640      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1641      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1642      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1643      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1644       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1645      match pre_assembled with
1646       [ None ⇒ True
1647       | Some pc_code ⇒
1648          let 〈new_pc,code〉 ≝ pc_code in
1649           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1650
1651axiom assembly_meets_specification:
1652  ∀pseudo_assembly_program.
1653    match assembly pseudo_assembly_program with
1654    [ None ⇒ True
1655    | Some code_mem_cost ⇒
1656      let 〈code_mem, cost〉 ≝ code_mem_cost in
1657        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1658    ].
1659(*
1660  # PROGRAM
1661  [ cases PROGRAM
1662    # PREAMBLE
1663    # INSTR_LIST
1664    elim INSTR_LIST
1665    [ whd
1666      whd in ⊢ (∀_. %)
1667      # PC
1668      whd
1669    | # INSTR
1670      # INSTR_LIST_TL
1671      # H
1672      whd
1673      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1674    ]
1675  | cases not_implemented
1676  ] *)
1677*)
1678
1679definition internal_pseudo_address_map ≝ list (BitVector 8).
1680
1681axiom low_internal_ram_of_pseudo_low_internal_ram:
1682 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1683
1684axiom high_internal_ram_of_pseudo_high_internal_ram:
1685 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1686
1687axiom low_internal_ram_of_pseudo_internal_ram_hit:
1688 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀addr:BitVector 7.
1689  member ? (eq_bv 8) (false:::addr) M = true →
1690   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1691   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1692   let pbu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) (low_internal_ram … s) (zero 8) in
1693   let bl ≝ lookup ? 7 addr ram (zero 8) in
1694   let bu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) ram (zero 8) in
1695    bu@@bl = \fst (sigma (pbu@@pbl)).
1696
1697(* changed from add to sub *)
1698axiom low_internal_ram_of_pseudo_internal_ram_miss:
1699 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
1700  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1701  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1702  let carr ≝ get_index_v ? ? flags 1 ? in
1703  carr = false →
1704  member ? (eq_bv 8) (false:::Saddr) M = false →
1705   member ? (eq_bv 8) (false:::addr) M = false →
1706    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1707  //
1708qed.
1709
1710definition addressing_mode_ok ≝
1711 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
1712  λaddr:addressing_mode.
1713   match addr with
1714    [ DIRECT d ⇒
1715       ¬(member ? (eq_bv 8) d M) ∧
1716       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1717    | INDIRECT i ⇒
1718       let d ≝ get_register … s [[false;false;i]] in
1719       ¬(member ? (eq_bv 8) d M) ∧
1720       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1721    | EXT_INDIRECT _ ⇒ true
1722    | REGISTER _ ⇒ true
1723    | ACC_A ⇒ true
1724    | ACC_B ⇒ true
1725    | DPTR ⇒ true
1726    | DATA _ ⇒ true
1727    | DATA16 _ ⇒ true
1728    | ACC_DPTR ⇒ true
1729    | ACC_PC ⇒ true
1730    | EXT_INDIRECT_DPTR ⇒ true
1731    | INDIRECT_DPTR ⇒ true
1732    | CARRY ⇒ true
1733    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1734    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1735    | RELATIVE _ ⇒ true
1736    | ADDR11 _ ⇒ true
1737    | ADDR16 _ ⇒ true ].
1738   
1739definition next_internal_pseudo_address_map0 ≝
1740  λT.
1741  λfetched.
1742  λM: internal_pseudo_address_map.
1743  λcm:T.
1744  λs: PreStatus T cm.
1745   match fetched with
1746    [ Comment _ ⇒ Some ? M
1747    | Cost _ ⇒ Some … M
1748    | Jmp _ ⇒ Some … M
1749    | Call _ ⇒
1750       Some … (add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1)::M)
1751    | Mov _ _ ⇒ Some … M
1752    | Instruction instr ⇒
1753       match instr with
1754        [ ADD addr1 addr2 ⇒
1755           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1756            Some ? M
1757           else
1758            None ?
1759        | ADDC addr1 addr2 ⇒
1760           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1761            Some ? M
1762           else
1763            None ?
1764        | SUBB addr1 addr2 ⇒
1765           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1766            Some ? M
1767           else
1768            None ?       
1769        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1770 
1771
1772definition next_internal_pseudo_address_map ≝
1773 λM:internal_pseudo_address_map.
1774 λcm.
1775  λs:PseudoStatus cm. λppc_ok.
1776    next_internal_pseudo_address_map0 ?
1777     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M cm s.
1778
1779definition code_memory_of_pseudo_assembly_program:
1780    ∀pap:pseudo_assembly_program.
1781      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1782  λpap.
1783  λsigma.
1784  λpolicy.
1785    let p ≝ pi1 … (assembly pap sigma policy) in
1786      load_code_memory (\fst p).
1787
1788definition status_of_pseudo_status:
1789    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1790      ∀sigma: Word → Word. ∀policy: Word → bool.
1791        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1792  λM.
1793  λpap.
1794  λps.
1795  λsigma.
1796  λpolicy.
1797  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1798  let pc ≝ sigma (program_counter … ps) in
1799  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1800  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1801     mk_PreStatus (BitVectorTrie Byte 16)
1802      cm
1803      lir
1804      hir
1805      (external_ram … ps)
1806      pc
1807      (special_function_registers_8051 … ps)
1808      (special_function_registers_8052 … ps)
1809      (p1_latch … ps)
1810      (p3_latch … ps)
1811      (clock … ps).
1812
1813(*
1814definition write_at_stack_pointer':
1815 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1816  λM: Type[0].
1817  λs: PreStatus M.
1818  λv: Byte.
1819    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1820    let bit_zero ≝ get_index_v… nu O ? in
1821    let bit_1 ≝ get_index_v… nu 1 ? in
1822    let bit_2 ≝ get_index_v… nu 2 ? in
1823    let bit_3 ≝ get_index_v… nu 3 ? in
1824      if bit_zero then
1825        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1826                              v (low_internal_ram ? s) in
1827          set_low_internal_ram ? s memory
1828      else
1829        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1830                              v (high_internal_ram ? s) in
1831          set_high_internal_ram ? s memory.
1832  [ cases l0 %
1833  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1834qed.
1835
1836definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1837 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1838
1839  λticks_of.
1840  λs.
1841  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1842  let ticks ≝ ticks_of (program_counter ? s) in
1843  let s ≝ set_clock ? s (clock ? s + ticks) in
1844  let s ≝ set_program_counter ? s pc in
1845    match instr with
1846    [ Instruction instr ⇒
1847       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1848    | Comment cmt ⇒ s
1849    | Cost cst ⇒ s
1850    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1851    | Call call ⇒
1852      let a ≝ address_of_word_labels s call in
1853      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1854      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1855      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1856      let s ≝ write_at_stack_pointer' ? s pc_bl in
1857      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1858      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1859      let s ≝ write_at_stack_pointer' ? s pc_bu in
1860        set_program_counter ? s a
1861    | Mov dptr ident ⇒
1862       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1863    ].
1864 [
1865 |2,3,4: %
1866 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1867 |
1868 | %
1869 ]
1870 cases not_implemented
1871qed.
1872*)
1873
1874(*
1875lemma execute_code_memory_unchanged:
1876 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1877 #ticks #ps whd in ⊢ (??? (??%))
1878 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1879  (program_counter pseudo_assembly_program ps)) #instr #pc
1880 whd in ⊢ (??? (??%)) cases instr
1881  [ #pre cases pre
1882     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1883       cases (vsplit ????) #z1 #z2 %
1884     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1885       cases (vsplit ????) #z1 #z2 %
1886     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1887       cases (vsplit ????) #z1 #z2 %
1888     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1889       [ #x1 whd in ⊢ (??? (??%))
1890     | *: cases not_implemented
1891     ]
1892  | #comment %
1893  | #cost %
1894  | #label %
1895  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1896    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1897    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1898    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1899    (* CSC: ??? *)
1900  | #dptr #label (* CSC: ??? *)
1901  ]
1902  cases not_implemented
1903qed.
1904*)
1905
1906(* DEAD CODE?
1907lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1908 ∀M:internal_pseudo_address_map.
1909 ∀ps,ps': PseudoStatus.
1910 ∀pol.
1911  ∀prf:code_memory … ps = code_memory … ps'.
1912   let pol' ≝ ? in
1913   match status_of_pseudo_status M ps pol with
1914    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1915    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1916    ].
1917 [2: <prf @pol]
1918 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1919 generalize in match (refl … (assembly (code_memory … ps) pol))
1920 cases (assembly ??) in ⊢ (???% → %)
1921  [ #K whd whd in ⊢ (??%?) <H >K %
1922  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1923qed.
1924*)
1925
1926definition ticks_of0:
1927    ∀p:pseudo_assembly_program.
1928      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1929  λprogram: pseudo_assembly_program.
1930  λsigma.
1931  λpolicy.
1932  λppc: Word.
1933  λfetched.
1934    match fetched with
1935    [ Instruction instr ⇒
1936      match instr with
1937      [ JC lbl ⇒ ? (*
1938        match pol lookup_labels ppc with
1939        [ short_jump ⇒ 〈2, 2〉
1940        | medium_jump ⇒ ?
1941        | long_jump ⇒ 〈4, 4〉
1942        ] *)
1943      | JNC lbl ⇒ ? (*
1944        match pol lookup_labels ppc with
1945        [ short_jump ⇒ 〈2, 2〉
1946        | medium_jump ⇒ ?
1947        | long_jump ⇒ 〈4, 4〉
1948        ] *)
1949      | JB bit lbl ⇒ ? (*
1950        match pol lookup_labels ppc with
1951        [ short_jump ⇒ 〈2, 2〉
1952        | medium_jump ⇒ ?
1953        | long_jump ⇒ 〈4, 4〉
1954        ] *)
1955      | JNB bit lbl ⇒ ? (*
1956        match pol lookup_labels ppc with
1957        [ short_jump ⇒ 〈2, 2〉
1958        | medium_jump ⇒ ?
1959        | long_jump ⇒ 〈4, 4〉
1960        ] *)
1961      | JBC bit lbl ⇒ ? (*
1962        match pol lookup_labels ppc with
1963        [ short_jump ⇒ 〈2, 2〉
1964        | medium_jump ⇒ ?
1965        | long_jump ⇒ 〈4, 4〉
1966        ] *)
1967      | JZ lbl ⇒ ? (*
1968        match pol lookup_labels ppc with
1969        [ short_jump ⇒ 〈2, 2〉
1970        | medium_jump ⇒ ?
1971        | long_jump ⇒ 〈4, 4〉
1972        ] *)
1973      | JNZ lbl ⇒ ? (*
1974        match pol lookup_labels  ppc with
1975        [ short_jump ⇒ 〈2, 2〉
1976        | medium_jump ⇒ ?
1977        | long_jump ⇒ 〈4, 4〉
1978        ] *)
1979      | CJNE arg lbl ⇒ ? (*
1980        match pol lookup_labels ppc with
1981        [ short_jump ⇒ 〈2, 2〉
1982        | medium_jump ⇒ ?
1983        | long_jump ⇒ 〈4, 4〉
1984        ] *)
1985      | DJNZ arg lbl ⇒ ? (*
1986        match pol lookup_labels ppc with
1987        [ short_jump ⇒ 〈2, 2〉
1988        | medium_jump ⇒ ?
1989        | long_jump ⇒ 〈4, 4〉
1990        ] *)
1991      | ADD arg1 arg2 ⇒
1992        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1993         〈ticks, ticks〉
1994      | ADDC arg1 arg2 ⇒
1995        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1996         〈ticks, ticks〉
1997      | SUBB arg1 arg2 ⇒
1998        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1999         〈ticks, ticks〉
2000      | INC arg ⇒
2001        let ticks ≝ ticks_of_instruction (INC ? arg) in
2002         〈ticks, ticks〉
2003      | DEC arg ⇒
2004        let ticks ≝ ticks_of_instruction (DEC ? arg) in
2005         〈ticks, ticks〉
2006      | MUL arg1 arg2 ⇒
2007        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
2008         〈ticks, ticks〉
2009      | DIV arg1 arg2 ⇒
2010        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
2011         〈ticks, ticks〉
2012      | DA arg ⇒
2013        let ticks ≝ ticks_of_instruction (DA ? arg) in
2014         〈ticks, ticks〉
2015      | ANL arg ⇒
2016        let ticks ≝ ticks_of_instruction (ANL ? arg) in
2017         〈ticks, ticks〉
2018      | ORL arg ⇒
2019        let ticks ≝ ticks_of_instruction (ORL ? arg) in
2020         〈ticks, ticks〉
2021      | XRL arg ⇒
2022        let ticks ≝ ticks_of_instruction (XRL ? arg) in
2023         〈ticks, ticks〉
2024      | CLR arg ⇒
2025        let ticks ≝ ticks_of_instruction (CLR ? arg) in
2026         〈ticks, ticks〉
2027      | CPL arg ⇒
2028        let ticks ≝ ticks_of_instruction (CPL ? arg) in
2029         〈ticks, ticks〉
2030      | RL arg ⇒
2031        let ticks ≝ ticks_of_instruction (RL ? arg) in
2032         〈ticks, ticks〉
2033      | RLC arg ⇒
2034        let ticks ≝ ticks_of_instruction (RLC ? arg) in
2035         〈ticks, ticks〉
2036      | RR arg ⇒
2037        let ticks ≝ ticks_of_instruction (RR ? arg) in
2038         〈ticks, ticks〉
2039      | RRC arg ⇒
2040        let ticks ≝ ticks_of_instruction (RRC ? arg) in
2041         〈ticks, ticks〉
2042      | SWAP arg ⇒
2043        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
2044         〈ticks, ticks〉
2045      | MOV arg ⇒
2046        let ticks ≝ ticks_of_instruction (MOV ? arg) in
2047         〈ticks, ticks〉
2048      | MOVX arg ⇒
2049        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
2050         〈ticks, ticks〉
2051      | SETB arg ⇒
2052        let ticks ≝ ticks_of_instruction (SETB ? arg) in
2053         〈ticks, ticks〉
2054      | PUSH arg ⇒
2055        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
2056         〈ticks, ticks〉
2057      | POP arg ⇒
2058        let ticks ≝ ticks_of_instruction (POP ? arg) in
2059         〈ticks, ticks〉
2060      | XCH arg1 arg2 ⇒
2061        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
2062         〈ticks, ticks〉
2063      | XCHD arg1 arg2 ⇒
2064        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
2065         〈ticks, ticks〉
2066      | RET ⇒
2067        let ticks ≝ ticks_of_instruction (RET ?) in
2068         〈ticks, ticks〉
2069      | RETI ⇒
2070        let ticks ≝ ticks_of_instruction (RETI ?) in
2071         〈ticks, ticks〉
2072      | NOP ⇒
2073        let ticks ≝ ticks_of_instruction (NOP ?) in
2074         〈ticks, ticks〉
2075      ]
2076    | Comment comment ⇒ 〈0, 0〉
2077    | Cost cost ⇒ 〈0, 0〉
2078    | Jmp jmp ⇒ 〈2, 2〉
2079    | Call call ⇒ 〈2, 2〉
2080    | Mov dptr tgt ⇒ 〈2, 2〉
2081    ].
2082    cases daemon
2083qed.
2084
2085definition ticks_of:
2086    ∀p:pseudo_assembly_program.
2087      (Word → Word) → (Word → bool) → ∀ppc:Word.
2088       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
2089  λprogram: pseudo_assembly_program.
2090  λsigma.
2091  λpolicy.
2092  λppc: Word. λppc_ok.
2093    let pseudo ≝ \snd program in
2094    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
2095     ticks_of0 program sigma policy ppc fetched.
2096
2097lemma eq_rect_Type1_r:
2098  ∀A: Type[1].
2099  ∀a: A.
2100  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2101  #A #a #P #H #x #p
2102  generalize in match H;
2103  generalize in match P;
2104  cases p //
2105qed.
2106
2107axiom vsplit_append:
2108  ∀A: Type[0].
2109  ∀m, n: nat.
2110  ∀v, v': Vector A m.
2111  ∀q, q': Vector A n.
2112    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
2113      v = v' ∧ q = q'.
2114
2115lemma vsplit_vector_singleton:
2116  ∀A: Type[0].
2117  ∀n: nat.
2118  ∀v: Vector A (S n).
2119  ∀rest: Vector A n.
2120  ∀s: Vector A 1.
2121    v = s @@ rest →
2122    ((get_index_v A ? v 0 ?) ::: rest) = v.
2123  [1:
2124    #A #n #v cases daemon (* XXX: !!! *)
2125  |2:
2126    @le_S_S @le_O_n
2127  ]
2128qed.
2129
2130example sub_minus_one_seven_eight:
2131  ∀v: BitVector 7.
2132  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
2133  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
2134 cases daemon.
2135qed.
2136
2137(*
2138lemma blah:
2139  ∀m: internal_pseudo_address_map.
2140  ∀s: PseudoStatus.
2141  ∀arg: Byte.
2142  ∀b: bool.
2143    addressing_mode_ok m s (DIRECT arg) = true →
2144      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2145      get_arg_8 ? s b (DIRECT arg).
2146  [2, 3: normalize % ]
2147  #m #s #arg #b #hyp
2148  whd in ⊢ (??%%)
2149  @vsplit_elim''
2150  #nu' #nl' #arg_nu_nl_eq
2151  normalize nodelta
2152  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2153  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2154  #get_index_v_eq
2155  normalize nodelta
2156  [2:
2157    normalize nodelta
2158    @vsplit_elim''
2159    #bit_one' #three_bits' #bit_one_three_bit_eq
2160    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2161    normalize nodelta
2162    generalize in match (refl ? (sub_7_with_carry ? ? ?))
2163    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2164    #Saddr #carr' #Saddr_carr_eq
2165    normalize nodelta
2166    #carr_hyp'
2167    @carr_hyp'
2168    [1:
2169    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2170        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2171        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2172        #member_eq
2173        normalize nodelta
2174        [2: #destr destruct(destr)
2175        |1: -carr_hyp';
2176            >arg_nu_nl_eq
2177            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2178            [1: >get_index_v_eq in ⊢ (??%? → ?)
2179            |2: @le_S @le_S @le_S @le_n
2180            ]
2181            cases (member (BitVector 8) ? (\fst ?) ?)
2182            [1: #destr normalize in destr; destruct(destr)
2183            |2:
2184            ]
2185        ]
2186    |3: >get_index_v_eq in ⊢ (??%?)
2187        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2188        >(vsplit_vector_singleton … bit_one_three_bit_eq)
2189        <arg_nu_nl_eq
2190        whd in hyp:(??%?)
2191        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2192        normalize nodelta [*: #ignore @sym_eq ]
2193    ]
2194  |
2195  ].
2196*)
2197(*
2198map_address0 ... (DIRECT arg) = Some .. →
2199  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2200  get_arg_8 (internal_ram ...) (DIRECT arg)
2201
2202((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
2203                     then Some internal_pseudo_address_map M 
2204                     else None internal_pseudo_address_map )
2205                    =Some internal_pseudo_address_map M')
2206*)
2207
2208axiom low_internal_ram_write_at_stack_pointer:
2209 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
2210 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2211  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
2212  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
2213  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2214  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
2215  bu@@bl = sigma (pbu@@pbl) →
2216   low_internal_ram T1 cm1
2217     (write_at_stack_pointer …
2218       (set_8051_sfr …
2219         (write_at_stack_pointer …
2220           (set_8051_sfr …
2221             (set_low_internal_ram … s1
2222               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
2223             SFR_SP sp1)
2224          bl)
2225        SFR_SP sp2)
2226      bu)
2227   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
2228      (low_internal_ram …
2229       (write_at_stack_pointer …
2230         (set_8051_sfr …
2231           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
2232          SFR_SP sp2)
2233        pbu)).
2234
2235lemma high_internal_ram_write_at_stack_pointer:
2236 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
2237 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2238  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
2239  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
2240  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
2241  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
2242  bu@@bl = sigma (pbu@@pbl) →
2243   high_internal_ram T1 cm1
2244     (write_at_stack_pointer …
2245       (set_8051_sfr …
2246         (write_at_stack_pointer …
2247           (set_8051_sfr …
2248             (set_high_internal_ram … s1
2249               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
2250             SFR_SP sp1)
2251          bl)
2252        SFR_SP sp2)
2253      bu)
2254   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2255      (high_internal_ram …
2256       (write_at_stack_pointer …
2257         (set_8051_sfr …
2258           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
2259          SFR_SP sp2)
2260        pbu)).
2261  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
2262  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
2263  cases daemon (* XXX: !!! *)
2264qed.
2265
2266lemma Some_Some_elim:
2267 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
2268 #T #x #y #P #H #K @H @option_destruct_Some //
2269qed.
2270
2271lemma pair_destruct_right:
2272  ∀A: Type[0].
2273  ∀B: Type[0].
2274  ∀a, c: A.
2275  ∀b, d: B.
2276    〈a, b〉 = 〈c, d〉 → b = d.
2277  #A #B #a #b #c #d //
2278qed.
2279   
2280(*CSC: ???*)
2281(* XXX: we need a precondition here stating that the PPC is within the
2282        bounds of the instruction list in order for Jaap's specification to
2283        apply.
2284*)
2285lemma snd_assembly_1_pseudoinstruction_ok:
2286  ∀program: pseudo_assembly_program.
2287  ∀sigma: Word → Word.
2288  ∀policy: Word → bool.
2289  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
2290  ∀ppc: Word.
2291  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
2292  ∀pi.
2293  ∀lookup_labels.
2294  ∀lookup_datalabels.
2295    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
2296    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
2297    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
2298    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
2299      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
2300  #program #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
2301  #lookup_labels #lookup_datalabels
2302  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
2303  normalize nodelta
2304  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
2305  #fetch_pseudo_refl
2306  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
2307  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
2308  lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)
2309  @pair_elim #preamble #instr_list #program_refl
2310  @pair_elim #labels #costs' #create_label_cost_map_refl
2311  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
2312  lapply (H ppc ppc_in_bounds) -H
2313  @pair_elim #pi' #newppc #fetch_pseudo_refl'
2314  @pair_elim #len #assembled #assembly1_refl #H
2315  cases H
2316  #encoding_check_assm #sigma_newppc_refl
2317  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
2318  >pi_refl' in assembly1_refl; #assembly1_refl
2319  >lookup_labels_refl >lookup_datalabels_refl
2320  >program_refl normalize nodelta
2321  >assembly1_refl
2322  <sigma_newppc_refl
2323  generalize in match fetch_pseudo_refl';
2324  whd in match (fetch_pseudo_instruction ???);
2325  @pair_elim #lbl #instr #nth_refl normalize nodelta
2326  #G cases (pair_destruct_right ?????? G) %
2327qed.
2328
2329lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
2330  /2/
2331qed.
2332
2333(* To be moved in ProofStatus *)
2334lemma program_counter_set_program_counter:
2335  ∀T.
2336  ∀cm.
2337  ∀s.
2338  ∀x.
2339    program_counter T cm (set_program_counter T cm s x) = x.
2340  //
2341qed.
2342
2343(* XXX: easy but tedious *)
2344axiom assembly1_lt_128:
2345  ∀i: instruction.
2346    |(assembly1 i)| < 128.
2347
2348axiom most_significant_bit_zero:
2349  ∀size, m: nat.
2350  ∀size_proof: 0 < size.
2351    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
2352  normalize in size_proof; /2/
2353qed.
2354
2355lemma bitvector_of_nat_sign_extension_equivalence:
2356  ∀m: nat.
2357  ∀size_proof: m < 128.
2358    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
2359  #m #size_proof whd in ⊢ (??%?);
2360  >most_significant_bit_zero
2361  [1:
2362    cases daemon
2363  |2:
2364    assumption
2365  |3:
2366    //
2367  ]
2368qed.
Note: See TracBrowser for help on using the repository browser.