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

Last change on this file since 2109 was 2108, checked in by mulligan, 8 years ago

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

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