# source:src/ASM/AssemblyProof.ma@2110

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

...

File size: 80.6 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.
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:
171  ∀n: nat.
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
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
215      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE 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.
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)) ∧
263    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
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))) ∧
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)))) ∧
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 ]]))
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 ]]))
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
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 ]
382    match b with
383    [ BIT_ADDR e ⇒ eq_bv ? b' e
384    | _ ⇒ false
385    ]
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    ]
397    match b with
398    [ ADDR11 e ⇒ eq_bv ? w e
399    | _ ⇒ false
400    ]
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
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
456    | _ ⇒ false
457    ]
458  | ADDC arg1 arg2 ⇒
459    match j with
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' ⇒
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' ⇒
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
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
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
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
694  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
695    whd in ⊢ (??%?); try %
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 ]
713    |2:
714      #arg1_left normalize nodelta
716    |3:
717      #arg1_left normalize nodelta
718      >(eq_sum_refl …)
719      [1:
720        %
721      |2,3:
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              [*:
744              ]
745            |2:
746              #arg @eq_prod_refl
747              [*:
749              ]
750            ]
751          |2:
752            #arg @eq_prod_refl
753            [*:
755            ]
756          ]
757        |2:
758          #arg @eq_prod_refl
759          [*:
761          ]
762        ]
763      |2:
764        #arg @eq_prod_refl
765        [*:
767        ]
768      ]
769    |2:
770      #arg1_right normalize nodelta
771      @eq_prod_refl
772      [*:
774      ]
775    ]
776  |*:
777    whd in ⊢ (??%?);
778    cases arg1
779    [*:
780      #arg1 >eq_sum_refl
781      [1,4:
783      |2,3,5,6:
784        #arg @eq_prod_refl
785        [*:
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 ]
842  try @eq_preinstruction_refl
843  #arg2 whd in ⊢ (??%?);
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
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.
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.
887               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE 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. ?
925      | relative ⇒ λrelative_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
961      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE 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
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
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
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 ⊢ (???%);
1103    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
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
1203  ∀n: nat.
1204  ∀l, r: BitVector n.
1206
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
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;
1236    |2:
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 ??);
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
1397    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1398    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
1399    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
1400    #word11' #irrelevant normalize nodelta
1401    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
1402qed.
1403
1404lemma fetch_assembly_pseudo':
1405  ∀lookup_labels.
1406  ∀sigma: Word → Word.
1407  ∀policy: Word → bool.
1408  ∀ppc.
1409  ∀lookup_datalabels.
1410  ∀pi.
1411  ∀code_memory.
1412  ∀len.
1413  ∀assembled.
1414  ∀instructions.
1415    let pc ≝ sigma ppc in
1416      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
1417        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
1418          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1419            encoding_check code_memory pc pc_plus_len assembled →
1420              fetch_many code_memory pc_plus_len pc instructions.
1421  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
1422  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
1423  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
1424  >len_refl >assembled_refl -len_refl
1425  generalize in match (add 16 (sigma ppc)
1426    (bitvector_of_nat 16
1427     (|flatten (Vector bool 8)
1428       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
1429  #final_pc
1430  generalize in match (sigma ppc); elim instructions
1431  [1:
1432    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
1433  |2:
1434    #i #tl #IH #pc #H whd
1435    cases (encoding_check_append ????? H) -H #H1 #H2
1436    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
1437    cases (fetch ??) * #instr #pc' #ticks
1438    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
1439    lapply (conjunction_true ?? H3) * #H4 #H5
1440    lapply (conjunction_true … H4) * #B1 #B2
1441    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
1442    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
1443  ]
1444qed.
1445
1446lemma fetch_assembly_pseudo:
1447  ∀program: pseudo_assembly_program.
1448  ∀sigma: Word → Word.
1449  ∀policy: Word → bool.
1450  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
1451  ∀ppc.∀ppc_ok.
1452  ∀code_memory.
1453  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
1454  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
1455  let pc ≝ sigma ppc in
1456  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1457  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1458  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1459    encoding_check code_memory pc pc_plus_len assembled →
1460      fetch_many code_memory pc_plus_len pc instructions.
1461  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
1462  letin lookup_datalabels ≝ (λx.?)
1463  letin pi ≝ (fst ???)
1464  letin pc ≝ (sigma ?)
1465  letin instructions ≝ (expand_pseudo_instruction ??????)
1466  @pair_elim #len #assembled #assembled_refl normalize nodelta
1467  #H
1468  generalize in match
1469   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
1470  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
1471qed.
1472
1473definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
1474  λpseudo_instruction.
1475    match pseudo_instruction with
1476    [ Comment c ⇒ False
1477    | Cost c ⇒ False
1478    | _ ⇒ True
1479    ].
1480
1481(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
1482   function that load the code in memory is correct. The latter is based
1483   on missing properties from the standard library on the BitVectorTrie
1484   data structrure.
1485
1486   Wrong at the moment, requires Jaap's precondition to ensure that the program
1487   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1488*)
1489
1491 ∀program.
1492 let program_size ≝ |program| in
1493  program_size ≤ 2^16 →
1494   ∀pc. ∀pc_ok: pc < program_size.
1495    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1496 #program elim program
1497 [ #_ #pc #abs normalize in abs; @⊥ /2/
1498 | #hd #tl #IH #size_ok *
1499   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
1500     whd in match next; normalize nodelta
1501   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
1502     whd in match next; normalize nodelta
1503   ]
1504 cases daemon (*CSC: complete! *)
1505qed.
1506(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
1507Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
1508e' come fetchare l'i-esimo bit dalla memoria.
1509Concludere assembly_ok come semplice corollario.
1510*)
1511lemma assembly_ok:
1512  ∀program.
1513  ∀length_proof: |\snd program| ≤ 2^16.
1514  ∀sigma: Word → Word.
1515  ∀policy: Word → bool.
1516  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
1517  ∀assembled.
1518  ∀costs': BitVectorTrie costlabel 16.
1519  let 〈preamble, instr_list〉 ≝ program in
1520  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
1521  let datalabels ≝ construct_datalabels preamble in
1522  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1523    〈assembled,costs'〉 = assembly program sigma policy →
1524      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
1525        let code_memory ≝ load_code_memory assembled in
1526        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in
1527          ∀ppc.∀ppc_ok.
1528            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1529            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1530            let pc ≝ sigma ppc in
1531            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1532              encoding_check code_memory pc pc_plus_len assembled ∧
1533                  sigma newppc = add … pc (bitvector_of_nat … len).
1534  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
1535  cases (assembly program sigma policy) * #assembled' #costs''
1536  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
1537  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
1538  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
1539  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
1540  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
1541  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
1542  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
1543  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
1544  >eq_fetch_pseudo_instruction
1545  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
1546  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
1548  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
1549      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
1550  >eq_assembly_1_pseudoinstruction
1551  whd in ⊢ (% → ?); #assembly_ok
1552  %
1553  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
1554      >snd_fetch_pseudo_instruction
1555      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
1556      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
1557      >eq_fetch_pseudo_instruction whd in match instruction_size;
1558      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
1559      cases daemon
1560  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
1562    cut (len=|assembled|)
1563    [1: (*CSC: provable before cleaning *)
1564        cases daemon
1565    ]
1566    #EQlen
1567    (* Nice statement here *)
1568    cut (∀j. ∀H: j < |assembled|.
1569          nth_safe Byte j assembled H =
1571          (bitvector_of_nat 16
1572           (nat_of_bitvector …
1573            (add … (sigma ppc) (bitvector_of_nat … j))))))
1574    [1:
1575      cases daemon
1576    |2:
1577      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
1578      elim assembled
1579      [1:
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|)))
1586           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
1587           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
1589  ]]
1590qed.
1591
1592(* XXX: should we add that costs = costs'? *)
1593lemma fetch_assembly_pseudo2:
1594  ∀program.
1595  ∀length_proof: |\snd program| ≤ 2^16.
1596  ∀sigma.
1597  ∀policy.
1598  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1599  ∀ppc.∀ppc_ok.
1600  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1601  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
1602  let code_memory ≝ load_code_memory assembled in
1603  let data_labels ≝ construct_datalabels (\fst program) in
1604  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in
1605  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
1606  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1607  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1608    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
1609  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
1610  @pair_elim #labels #costs #create_label_map_refl
1611  @pair_elim #assembled #costs' #assembled_refl
1612  letin code_memory ≝ (load_code_memory ?)
1613  letin data_labels ≝ (construct_datalabels ?)
1614  letin lookup_labels ≝ (λx. ?)
1615  letin lookup_datalabels ≝ (λx. ?)
1616  @pair_elim #pi #newppc #fetch_pseudo_refl
1617  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
1618  normalize nodelta try assumption
1619  @pair_elim #labels' #costs' #create_label_map_refl' #H
1620  lapply (H (sym_eq … assembled_refl)) -H
1621  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1622  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
1623  #len #assembledi #EQ4 #H
1624  lapply (H ppc) >fetch_pseudo_refl #H
1625  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
1626  >EQ4 #H1 cases (H ppc_ok)
1627  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
1628  >fetch_pseudo_refl in H1; #assm @assm assumption
1629qed.
1630
1631(* OLD?
1632definition assembly_specification:
1633  ∀assembly_program: pseudo_assembly_program.
1634  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1635  λpseudo_assembly_program.
1636  λcode_mem.
1637    ∀pc: Word.
1638      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1639      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1640      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1641      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1642      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1643       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1644      match pre_assembled with
1645       [ None ⇒ True
1646       | Some pc_code ⇒
1647          let 〈new_pc,code〉 ≝ pc_code in
1648           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1649
1650axiom assembly_meets_specification:
1651  ∀pseudo_assembly_program.
1652    match assembly pseudo_assembly_program with
1653    [ None ⇒ True
1654    | Some code_mem_cost ⇒
1655      let 〈code_mem, cost〉 ≝ code_mem_cost in
1657    ].
1658(*
1659  # PROGRAM
1660  [ cases PROGRAM
1661    # PREAMBLE
1662    # INSTR_LIST
1663    elim INSTR_LIST
1664    [ whd
1665      whd in ⊢ (∀_. %)
1666      # PC
1667      whd
1668    | # INSTR
1669      # INSTR_LIST_TL
1670      # H
1671      whd
1672      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1673    ]
1674  | cases not_implemented
1675  ] *)
1676*)
1677
1678(* XXX: changed this type.  Bool specifies whether byte is first or second
1679        component of an address, and the Word is the pseudoaddress that it
1680        corresponds to.  Second component is the same principle for the accumulator
1681        A.
1682*)
1683definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
1684
1685include alias "ASM/BitVectorTrie.ma".
1686
1687include "common/AssocList.ma".
1688
1689axiom low_internal_ram_of_pseudo_low_internal_ram:
1690 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1691
1692axiom high_internal_ram_of_pseudo_high_internal_ram:
1693 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1694
1695axiom low_internal_ram_of_pseudo_internal_ram_hit:
1696 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
1697  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
1698   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1699   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1700   let bl ≝ lookup ? 7 addr ram (zero 8) in
1701   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
1702   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
1703     if high then
1704       (pbl = higher) ∧ (bl = phigher)
1705     else
1706       (pbl = lower) ∧ (bl = plower).
1707
1708(* changed from add to sub *)
1709axiom low_internal_ram_of_pseudo_internal_ram_miss:
1711  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1712    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
1713      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1714
1719    [ DIRECT d ⇒
1720       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1721       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1722    | INDIRECT i ⇒
1723       let d ≝ get_register … s [[false;false;i]] in
1724       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1725       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1726    | EXT_INDIRECT _ ⇒ true
1727    | REGISTER _ ⇒ true
1728    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
1729    | ACC_B ⇒ true
1730    | DPTR ⇒ true
1731    | DATA _ ⇒ true
1732    | DATA16 _ ⇒ true
1733    | ACC_DPTR ⇒ true
1734    | ACC_PC ⇒ true
1735    | EXT_INDIRECT_DPTR ⇒ true
1736    | INDIRECT_DPTR ⇒ true
1737    | CARRY ⇒ true
1738    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1739    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1740    | RELATIVE _ ⇒ true
1741    | ADDR11 _ ⇒ true
1742    | ADDR16 _ ⇒ true ].
1743
1745  λT.
1746  λcm:T.
1747  λaddr_of: Identifier → PreStatus T cm → Word.
1748  λfetched.
1750  λs: PreStatus T cm.
1751   match fetched with
1752    [ Comment _ ⇒ Some ? M
1753    | Cost _ ⇒ Some … M
1754    | Jmp _ ⇒ Some … M
1755    | Call a ⇒
1756      let a' ≝ addr_of a s in
1757      let 〈callM, accM〉 ≝ M in
1758         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
1759                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
1760    | Mov _ _ ⇒ Some … M
1761    | Instruction instr ⇒
1762       match instr with
1765            Some ? M
1766           else
1767            None ?
1770            Some ? M
1771           else
1772            None ?
1775            Some ? M
1776           else
1777            None ?
1778        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1779
1782 λcm.
1784 λs:PseudoStatus cm.
1785 λppc_ok.
1787     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M 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
1797
1798definition sfr_8051_of_pseudo_sfr_8051 ≝
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
1935lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
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        | absolute_jump ⇒ ?
1969        | long_jump ⇒ 〈4, 4〉
1970        ] *)
1971      | JNC lbl ⇒ ? (*
1972        match pol lookup_labels ppc with
1973        [ short_jump ⇒ 〈2, 2〉
1974        | absolute_jump ⇒ ?
1975        | long_jump ⇒ 〈4, 4〉
1976        ] *)
1977      | JB bit lbl ⇒ ? (*
1978        match pol lookup_labels ppc with
1979        [ short_jump ⇒ 〈2, 2〉
1980        | absolute_jump ⇒ ?
1981        | long_jump ⇒ 〈4, 4〉
1982        ] *)
1983      | JNB bit lbl ⇒ ? (*
1984        match pol lookup_labels ppc with
1985        [ short_jump ⇒ 〈2, 2〉
1986        | absolute_jump ⇒ ?
1987        | long_jump ⇒ 〈4, 4〉
1988        ] *)
1989      | JBC bit lbl ⇒ ? (*
1990        match pol lookup_labels ppc with
1991        [ short_jump ⇒ 〈2, 2〉
1992        | absolute_jump ⇒ ?
1993        | long_jump ⇒ 〈4, 4〉
1994        ] *)
1995      | JZ lbl ⇒ ? (*
1996        match pol lookup_labels ppc with
1997        [ short_jump ⇒ 〈2, 2〉
1998        | absolute_jump ⇒ ?
1999        | long_jump ⇒ 〈4, 4〉
2000        ] *)
2001      | JNZ lbl ⇒ ? (*
2002        match pol lookup_labels  ppc with
2003        [ short_jump ⇒ 〈2, 2〉
2004        | absolute_jump ⇒ ?
2005        | long_jump ⇒ 〈4, 4〉
2006        ] *)
2007      | CJNE arg lbl ⇒ ? (*
2008        match pol lookup_labels ppc with
2009        [ short_jump ⇒ 〈2, 2〉
2010        | absolute_jump ⇒ ?
2011        | long_jump ⇒ 〈4, 4〉
2012        ] *)
2013      | DJNZ arg lbl ⇒ ? (*
2014        match pol lookup_labels ppc with
2015        [ short_jump ⇒ 〈2, 2〉
2016        | absolute_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:
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 ⊢ (??%? → %)
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
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  ∀program_length_proof: |\snd program| ≤ 2^16.
2316  ∀sigma: Word → Word.
2317  ∀policy: Word → bool.
2318  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
2319  ∀ppc: Word.
2320  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
2321  ∀pi.
2322  ∀lookup_labels.
2323  ∀lookup_datalabels.
2324    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
2325    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
2326    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
2327    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
2328      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
2329  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
2330  #lookup_labels #lookup_datalabels
2331  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
2332  normalize nodelta
2333  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
2334  #fetch_pseudo_refl
2335  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
2336  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
2337  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
2338  @pair_elim #preamble #instr_list #program_refl
2339  @pair_elim #labels #costs' #create_label_cost_map_refl
2340  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
2341  lapply (H ppc ppc_in_bounds) -H
2342  @pair_elim #pi' #newppc #fetch_pseudo_refl'
2343  @pair_elim #len #assembled #assembly1_refl #H
2344  cases H
2345  #encoding_check_assm #sigma_newppc_refl
2346  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
2347  >pi_refl' in assembly1_refl; #assembly1_refl
2348  >lookup_labels_refl >lookup_datalabels_refl
2349  >program_refl normalize nodelta
2350  >assembly1_refl
2351  <sigma_newppc_refl
2352  generalize in match fetch_pseudo_refl';
2353  whd in match (fetch_pseudo_instruction ???);
2354  @pair_elim #lbl #instr #nth_refl normalize nodelta
2355  #G cases (pair_destruct_right ?????? G) %
2356qed.
2357
2358lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
2359  /2/
2360qed.
2361
2362(* To be moved in ProofStatus *)
2363lemma program_counter_set_program_counter:
2364  ∀T.
2365  ∀cm.
2366  ∀s.
2367  ∀x.
2368    program_counter T cm (set_program_counter T cm s x) = x.
2369  //
2370qed.
2371
2372(* XXX: easy but tedious *)
2373lemma assembly1_lt_128:
2374  ∀i: instruction.
2375    |(assembly1 i)| < 128.
2376  #i cases i
2377  try (#assm1 #assm2) try #assm1
2378  [8:
2379    cases assm1
2380    try (#assm1 #assm2) try #assm1
2381    whd in match assembly1; normalize nodelta
2382    whd in match assembly_preinstruction; normalize nodelta
2384    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
2385    [32:
2386      cases assm1 -assm1 #assm1 normalize nodelta
2388      [1:
2390      |2:
2392      ]
2393      #w
2394    |35,36,37:
2395      cases assm1 -assm1 #assm1 normalize nodelta
2396      [1,3:
2397        cases assm1 -assm1 #assm1 normalize nodelta
2398      ]
2401    |49:
2402      cases assm1 -assm1 #assm1 normalize nodelta
2403      [1:
2404        cases assm1 -assm1 #assm1 normalize nodelta
2405        [1:
2406          cases assm1 -assm1 #assm1 normalize nodelta
2407          [1:
2408            cases assm1 -assm1 #assm1 normalize nodelta
2409            [1:
2410              cases assm1 -assm1 #assm1 normalize nodelta
2411            ]
2412          ]
2413        ]
2414      ]
2416      [1,3,4,5:
2418      |*:
2420        normalize nodelta
2421        [1,2:
2423        ]
2424      ]
2425    |50:
2426      cases assm1 -assm1 #assm1 normalize nodelta
2428      [1:
2430      |2:
2432      ]
2433    ]
2434    normalize repeat @le_S_S @le_O_n
2435  ]
2436  whd in match assembly1; normalize nodelta
2437  [6:
2438    normalize repeat @le_S_S @le_O_n
2439  |7:
2440    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
2441  |*:
2442    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
2443  ]
2444qed.
Note: See TracBrowser for help on using the repository browser.