source: src/ASM/AssemblyProof.ma @ 2075

Last change on this file since 2075 was 2075, checked in by mulligan, 7 years ago

Solved conflict in AssemblyProof?

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