source: src/ASM/AssemblyProof.ma @ 2119

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

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

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