source: src/ASM/AssemblyProof.ma @ 2115

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

Old commented out code removed

File size: 63.0 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
618definition load_code_memory_aux ≝
619 fold_left_i_aux … (
620   λi, mem, v.
621     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
622
623lemma vsplit_zero:
624  ∀A,m.
625  ∀v: Vector A m.
626    〈[[]], v〉 = vsplit A 0 m v.
627  #A #m #v
628  cases v try %
629  #n #hd #tl %
630qed.
631
632lemma Vector_O:
633  ∀A: Type[0].
634  ∀v: Vector A 0.
635    v ≃ VEmpty A.
636 #A #v
637 generalize in match (refl … 0);
638 cases v in ⊢ (??%? → ?%%??); //
639 #n #hd #tl #absurd
640 destruct(absurd)
641qed.
642
643lemma Vector_Sn:
644  ∀A: Type[0].
645  ∀n: nat.
646  ∀v: Vector A (S n).
647    ∃hd: A. ∃tl: Vector A n.
648      v ≃ VCons A n hd tl.
649  #A #n #v
650  generalize in match (refl … (S n));
651  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
652  [1:
653    #absurd destruct(absurd)
654  |2:
655    #m #hd #tl #eq
656    <(injective_S … eq)
657    %{hd} %{tl} %
658  ]
659qed.
660
661lemma vector_append_zero:
662  ∀A,m.
663  ∀v: Vector A m.
664  ∀q: Vector A 0.
665    v = q@@v.
666  #A #m #v #q
667  >(Vector_O A q) %
668qed.
669
670lemma prod_eq_left:
671  ∀A: Type[0].
672  ∀p, q, r: A.
673    p = q → 〈p, r〉 = 〈q, r〉.
674  #A #p #q #r #hyp
675  destruct %
676qed.
677
678lemma prod_eq_right:
679  ∀A: Type[0].
680  ∀p, q, r: A.
681    p = q → 〈r, p〉 = 〈r, q〉.
682  #A #p #q #r #hyp
683  destruct %
684qed.
685
686corollary prod_vector_zero_eq_left:
687  ∀A, n.
688  ∀q: Vector A O.
689  ∀r: Vector A n.
690    〈q, r〉 = 〈[[ ]], r〉.
691  #A #n #q #r
692  generalize in match (Vector_O A q …);
693  #hyp destruct %
694qed.
695
696lemma tail_head:
697  ∀a: Type[0].
698  ∀m, n: nat.
699  ∀hd: a.
700  ∀l: Vector a m.
701  ∀r: Vector a n.
702    tail a ? (hd:::(l@@r)) = l@@r.
703  #a #m #n #hd #l #r
704  cases l try %
705  #m' #hd' #tl' %
706qed.
707
708lemma head_head':
709  ∀a: Type[0].
710  ∀m: nat.
711  ∀hd: a.
712  ∀l: Vector a m.
713    hd = head' … (hd:::l).
714  #a #m #hd #l cases l try %
715  #m' #hd' #tl %
716qed.
717
718lemma vsplit_succ:
719  ∀A: Type[0].
720  ∀m, n: nat.
721  ∀l: Vector A m.
722  ∀r: Vector A n.
723  ∀v: Vector A (m + n).
724  ∀hd: A.
725    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
726  #A #m
727  elim m
728  [1:
729    #n #l #r #v #hd #eq #hyp
730    destruct >(Vector_O … l) %
731  |2:
732    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
733    destruct
734    cases (Vector_Sn … l) #hd' #tl'
735    whd in ⊢ (???%);
736    >tail_head
737    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
738    try (<hyp <head_head' %)
739    elim l normalize //
740  ]
741qed.
742
743lemma vsplit_prod:
744  ∀A: Type[0].
745  ∀m, n: nat.
746  ∀p: Vector A (m + n).
747  ∀v: Vector A m.
748  ∀q: Vector A n.
749    p = v@@q → 〈v, q〉 = vsplit A m n p.
750  #A #m elim m
751  [1:
752    #n #p #v #q #hyp
753    >hyp <(vector_append_zero A n q v)
754    >(prod_vector_zero_eq_left A …)
755    @vsplit_zero
756  |2:
757    #r #ih #n #p #v #q #hyp
758    >hyp
759    cases (Vector_Sn A r v) #hd #exists
760    cases exists #tl #jmeq
761    >jmeq @vsplit_succ try %
762    @ih %
763  ]
764qed.
765
766definition vsplit_elim:
767  ∀A: Type[0].
768  ∀l, m: nat.
769  ∀v: Vector A (l + m).
770  ∀P: (Vector A l) × (Vector A m) → Prop.
771    (∀vl: Vector A l.
772     ∀vm: Vector A m.
773      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
774  λa: Type[0].
775  λl, m: nat.
776  λv: Vector a (l + m).
777  λP. ?.
778  cases daemon
779qed.
780
781let rec encoding_check
782  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
783    (encoding: list Byte)
784      on encoding: Prop ≝
785  match encoding with
786  [ nil ⇒ final_pc = pc
787  | cons hd tl ⇒
788    let 〈new_pc, byte〉 ≝ next code_memory pc in
789      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
790  ].
791
792lemma add_bitvector_of_nat_Sm:
793  ∀n, m: nat.
794    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
795      bitvector_of_nat n (S m).
796 #n #m @add_bitvector_of_nat_plus
797qed.
798
799lemma encoding_check_append:
800  ∀code_memory: BitVectorTrie Byte 16.
801  ∀final_pc: Word.
802  ∀l1: list Byte.
803  ∀pc: Word.
804  ∀l2: list Byte.
805    encoding_check code_memory pc final_pc (l1@l2) →
806      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
807        encoding_check code_memory pc pc_plus_len l1 ∧
808          encoding_check code_memory pc_plus_len final_pc l2.
809  #code_memory #final_pc #l1 elim l1
810  [1:
811    #pc #l2
812    whd in ⊢ (????% → ?); #H
813    <add_zero
814    whd whd in ⊢ (?%?); /2/
815  |2:
816    #hd #tl #IH #pc #l2 * #H1 #H2
817(*    >add_SO in H2; #H2 *)
818    cases (IH … H2) #E1 #E2 %
819    [1:
820      % try @H1
821      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
822      <add_associative #assm assumption
823    |2:
824      <add_associative in E2;
825      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
826      assumption
827    ]
828  ]
829qed.
830
831lemma destruct_bug_fix_1:
832  ∀n: nat.
833    S n = 0 → False.
834  #n #absurd destruct(absurd)
835qed.
836
837lemma destruct_bug_fix_2:
838  ∀m, n: nat.
839    S m = S n → m = n.
840  #m #n #refl destruct %
841qed.
842
843definition bitvector_3_cases:
844  ∀b: BitVector 3.
845    ∃l, c, r: bool.
846      b ≃ [[l; c; r]].
847  #b
848  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
849  [1:
850    #absurd @⊥ -b @(destruct_bug_fix_1 2)
851    >absurd %
852  |2:
853    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
854    cut (n = 2)
855    [1:
856      @destruct_bug_fix_2
857      >size_refl %
858    |2:
859      #n_refl >n_refl in tl; #V
860      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
861      [1:
862        #absurd @⊥ -V @(destruct_bug_fix_1 1)
863        >absurd %
864      |2:
865        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
866        cut (n' = 1)
867        [1:
868          @destruct_bug_fix_2 >size_refl' %
869        |2:
870          #n_refl' >n_refl' in tl'; #V'
871          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
872          [1:
873            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
874            >absurd %
875          |2:
876            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
877            cut (n'' = 0)
878            [1:
879              @destruct_bug_fix_2 >size_refl'' %
880            |2:
881              #n_refl'' >n_refl'' in tl''; #tl'''
882              >(Vector_O … tl''') %
883            ]
884          ]
885        ]
886      ]
887    ]
888  ]
889qed.
890
891lemma bitvector_3_elim_prop:
892  ∀P: BitVector 3 → Prop.
893    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
894    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
895    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
896  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
897  cases (bitvector_3_cases … H9) #l #assm cases assm
898  -assm #c #assm cases assm
899  -assm #r #assm cases assm destruct
900  cases l cases c cases r assumption
901qed.
902
903definition ticks_of_instruction ≝
904  λi.
905    let trivial_code_memory ≝ assembly1 i in
906    let trivial_status ≝ load_code_memory trivial_code_memory in
907      \snd (fetch trivial_status (zero ?)).
908
909lemma fetch_assembly:
910  ∀pc: Word.
911  ∀i: instruction.
912  ∀code_memory: BitVectorTrie Byte 16.
913  ∀assembled: list Byte.
914    assembled = assembly1 i →
915      let len ≝ length … assembled in
916      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
917        encoding_check code_memory pc pc_plus_len assembled →
918          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
919           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
920  #pc #i #code_memory #assembled cases i [8: *]
921 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
922 [47,48,49:
923 |*: #arg @(subaddressing_mode_elim … arg)
924  [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,
925   59,60,63,64,65,66,67: #ARG]]
926 [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,
927  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
928  [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,
929   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,
930   68,69,70,71: #ARG2]]
931 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
932 normalize in ⊢ (???% → ?);
933 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
934  normalize in ⊢ (???% → ?);]
935 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
936 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
937 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
938 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
939 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl
940qed.
941
942let rec fetch_many
943  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
944    (expected: list instruction)
945      on expected: Prop ≝
946  match expected with
947  [ nil ⇒ eq_bv … pc final_pc = true
948  | cons i tl ⇒
949    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
950      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
951        fetch_many code_memory final_pc pc' tl)
952  ].
953
954lemma option_destruct_Some:
955  ∀A: Type[0].
956  ∀a, b: A.
957    Some A a = Some A b → a = b.
958  #A #a #b #EQ
959  destruct %
960qed.
961
962lemma eq_instruction_to_eq:
963  ∀i1, i2: instruction.
964    eq_instruction i1 i2 = true → i1 ≃ i2.
965  #i1 #i2
966  cases i1 cases i2 cases daemon (*
967  [1,10,19,28,37,46:
968    #arg1 #arg2
969    whd in match (eq_instruction ??);
970    cases arg1 #subaddressing_mode
971    cases subaddressing_mode
972    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
973    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
974    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
975    #word11 #irrelevant
976    cases arg2 #subaddressing_mode
977    cases subaddressing_mode
978    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
979    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
980    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
981    #word11' #irrelevant normalize nodelta
982    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
983qed.
984         
985lemma fetch_assembly_pseudo':
986  ∀lookup_labels.
987  ∀sigma: Word → Word.
988  ∀policy: Word → bool.
989  ∀ppc.
990  ∀lookup_datalabels.
991  ∀pi.
992  ∀code_memory.
993  ∀len.
994  ∀assembled.
995  ∀instructions.
996    let pc ≝ sigma ppc in
997      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
998        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
999          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1000            encoding_check code_memory pc pc_plus_len assembled →
1001              fetch_many code_memory pc_plus_len pc instructions.
1002  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
1003  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
1004  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
1005  >len_refl >assembled_refl -len_refl
1006  generalize in match (add 16 (sigma ppc)
1007    (bitvector_of_nat 16
1008     (|flatten (Vector bool 8)
1009       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
1010  #final_pc
1011  generalize in match (sigma ppc); elim instructions
1012  [1:
1013    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
1014  |2:
1015    #i #tl #IH #pc #H whd
1016    cases (encoding_check_append ????? H) -H #H1 #H2
1017    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
1018    cases (fetch ??) * #instr #pc' #ticks
1019    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
1020    lapply (conjunction_true ?? H3) * #H4 #H5
1021    lapply (conjunction_true … H4) * #B1 #B2
1022    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
1023    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
1024  ]
1025qed.
1026
1027lemma fetch_assembly_pseudo:
1028  ∀program: pseudo_assembly_program.
1029  ∀sigma: Word → Word.
1030  ∀policy: Word → bool.
1031  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
1032  ∀ppc.∀ppc_ok.
1033  ∀code_memory.
1034  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
1035  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
1036  let pc ≝ sigma ppc in
1037  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1038  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1039  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1040    encoding_check code_memory pc pc_plus_len assembled →
1041      fetch_many code_memory pc_plus_len pc instructions.
1042  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
1043  letin lookup_datalabels ≝ (λx.?)
1044  letin pi ≝ (fst ???)
1045  letin pc ≝ (sigma ?)
1046  letin instructions ≝ (expand_pseudo_instruction ??????)
1047  @pair_elim #len #assembled #assembled_refl normalize nodelta
1048  #H
1049  generalize in match
1050   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
1051  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
1052qed.
1053
1054definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
1055  λpseudo_instruction.
1056    match pseudo_instruction with
1057    [ Comment c ⇒ False
1058    | Cost c ⇒ False
1059    | _ ⇒ True
1060    ].
1061
1062(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
1063   function that load the code in memory is correct. The latter is based
1064   on missing properties from the standard library on the BitVectorTrie
1065   data structrure.
1066   
1067   Wrong at the moment, requires Jaap's precondition to ensure that the program
1068   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1069*)
1070
1071lemma load_code_memory_ok:
1072 ∀program.
1073 let program_size ≝ |program| in
1074  program_size ≤ 2^16 →
1075   ∀pc. ∀pc_ok: pc < program_size.
1076    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1077 #program elim program
1078 [ #_ #pc #abs normalize in abs; @⊥ /2/
1079 | #hd #tl #IH #size_ok *
1080   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
1081     whd in match next; normalize nodelta
1082   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
1083     whd in match next; normalize nodelta
1084   ]
1085 cases daemon (*CSC: complete! *)
1086qed.
1087(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
1088Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
1089e' come fetchare l'i-esimo bit dalla memoria.
1090Concludere assembly_ok come semplice corollario.
1091*)
1092lemma assembly_ok:
1093  ∀program.
1094  ∀length_proof: |\snd program| ≤ 2^16.
1095  ∀sigma: Word → Word.
1096  ∀policy: Word → bool.
1097  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
1098  ∀assembled.
1099  ∀costs': BitVectorTrie costlabel 16.
1100  let 〈preamble, instr_list〉 ≝ program in
1101  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
1102  let datalabels ≝ construct_datalabels preamble in
1103  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1104    〈assembled,costs'〉 = assembly program sigma policy →
1105      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
1106        let code_memory ≝ load_code_memory assembled in
1107        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
1108          ∀ppc.∀ppc_ok.
1109            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
1110            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1111            let pc ≝ sigma ppc in
1112            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1113              encoding_check code_memory pc pc_plus_len assembled ∧
1114                  sigma newppc = add … pc (bitvector_of_nat … len).
1115  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
1116  cases (assembly program sigma policy) * #assembled' #costs''
1117  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
1118  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
1119  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
1120  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
1121  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
1122  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
1123  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
1124  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
1125  >eq_fetch_pseudo_instruction
1126  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
1127  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
1128       (λx.address_of_word_labels_code_mem instr_list x)))
1129  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
1130      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
1131  >eq_assembly_1_pseudoinstruction
1132  whd in ⊢ (% → ?); #assembly_ok
1133  %
1134  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
1135      >snd_fetch_pseudo_instruction
1136      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
1137      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
1138      >eq_fetch_pseudo_instruction whd in match instruction_size;
1139      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
1140      cases daemon
1141  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
1142    #load_code_memory_ok
1143    cut (len=|assembled|)
1144    [1: (*CSC: provable before cleaning *)
1145        cases daemon
1146    ]
1147    #EQlen
1148    (* Nice statement here *)
1149    cut (∀j. ∀H: j < |assembled|.
1150          nth_safe Byte j assembled H =
1151          \snd (next (load_code_memory assembled')
1152          (bitvector_of_nat 16
1153           (nat_of_bitvector …
1154            (add … (sigma ppc) (bitvector_of_nat … j))))))
1155    [1:
1156      cases daemon
1157    |2:
1158      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
1159      elim assembled
1160      [1:
1161        #pc #_ whd <add_zero %
1162      | #hd #tl #IH #pc #H %
1163         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
1164           >H -H whd in ⊢ (??%?); <add_zero //
1165         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
1166           [2: <add_bitvector_of_nat_Sm @add_associative ]
1167           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
1168           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
1169           >add_associative % ]]
1170  ]]
1171qed.
1172
1173(* XXX: should we add that costs = costs'? *)
1174lemma fetch_assembly_pseudo2:
1175  ∀program.
1176  ∀length_proof: |\snd program| ≤ 2^16.
1177  ∀sigma.
1178  ∀policy.
1179  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1180  ∀ppc.∀ppc_ok.
1181  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1182  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
1183  let code_memory ≝ load_code_memory assembled in
1184  let data_labels ≝ construct_datalabels (\fst program) in
1185  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
1186  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
1187  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1188  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1189    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
1190  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
1191  @pair_elim #labels #costs #create_label_map_refl
1192  @pair_elim #assembled #costs' #assembled_refl
1193  letin code_memory ≝ (load_code_memory ?)
1194  letin data_labels ≝ (construct_datalabels ?)
1195  letin lookup_labels ≝ (λx. ?)
1196  letin lookup_datalabels ≝ (λx. ?)
1197  @pair_elim #pi #newppc #fetch_pseudo_refl
1198  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
1199  normalize nodelta try assumption
1200  @pair_elim #labels' #costs' #create_label_map_refl' #H
1201  lapply (H (sym_eq … assembled_refl)) -H
1202  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1203  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
1204  #len #assembledi #EQ4 #H
1205  lapply (H ppc) >fetch_pseudo_refl #H
1206  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
1207  >EQ4 #H1 cases (H ppc_ok)
1208  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
1209  >fetch_pseudo_refl in H1; #assm @assm assumption
1210qed.
1211
1212(* XXX: changed this type.  Bool specifies whether byte is first or second
1213        component of an address, and the Word is the pseudoaddress that it
1214        corresponds to.  Second component is the same principle for the accumulator
1215        A.
1216*)
1217definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
1218
1219include alias "ASM/BitVectorTrie.ma".
1220 
1221include "common/AssocList.ma".
1222
1223axiom low_internal_ram_of_pseudo_low_internal_ram:
1224 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1225
1226axiom high_internal_ram_of_pseudo_high_internal_ram:
1227 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1228
1229axiom low_internal_ram_of_pseudo_internal_ram_hit:
1230 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
1231  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
1232   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1233   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1234   let bl ≝ lookup ? 7 addr ram (zero 8) in
1235   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
1236   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
1237     if high then
1238       (pbl = higher) ∧ (bl = phigher)
1239     else
1240       (pbl = lower) ∧ (bl = plower).
1241
1242(* changed from add to sub *)
1243axiom low_internal_ram_of_pseudo_internal_ram_miss:
1244 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
1245  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1246    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
1247      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1248
1249definition addressing_mode_ok ≝
1250 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
1251  λaddr:addressing_mode.
1252   match addr with
1253    [ DIRECT d ⇒
1254       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1255       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1256    | INDIRECT i ⇒
1257       let d ≝ get_register … s [[false;false;i]] in
1258       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1259       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1260    | EXT_INDIRECT _ ⇒ true
1261    | REGISTER _ ⇒ true
1262    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
1263    | ACC_B ⇒ true
1264    | DPTR ⇒ true
1265    | DATA _ ⇒ true
1266    | DATA16 _ ⇒ true
1267    | ACC_DPTR ⇒ true
1268    | ACC_PC ⇒ true
1269    | EXT_INDIRECT_DPTR ⇒ true
1270    | INDIRECT_DPTR ⇒ true
1271    | CARRY ⇒ true
1272    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1273    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1274    | RELATIVE _ ⇒ true
1275    | ADDR11 _ ⇒ true
1276    | ADDR16 _ ⇒ true ].
1277   
1278definition next_internal_pseudo_address_map0 ≝
1279  λT.
1280  λcm:T.
1281  λaddr_of: Identifier → PreStatus T cm → Word.
1282  λfetched.
1283  λM: internal_pseudo_address_map.
1284  λs: PreStatus T cm.
1285   match fetched with
1286    [ Comment _ ⇒ Some ? M
1287    | Cost _ ⇒ Some … M
1288    | Jmp _ ⇒ Some … M
1289    | Call a ⇒
1290      let a' ≝ addr_of a s in
1291      let 〈callM, accM〉 ≝ M in
1292         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
1293                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
1294    | Mov _ _ ⇒ Some … M
1295    | Instruction instr ⇒
1296       match instr with
1297        [ ADD addr1 addr2 ⇒
1298           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1299            Some ? M
1300           else
1301            None ?
1302        | ADDC addr1 addr2 ⇒
1303           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1304            Some ? M
1305           else
1306            None ?
1307        | SUBB addr1 addr2 ⇒
1308           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1309            Some ? M
1310           else
1311            None ?       
1312        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1313
1314definition next_internal_pseudo_address_map ≝
1315 λM:internal_pseudo_address_map.
1316 λcm.
1317 λaddr_of.
1318 λs:PseudoStatus cm.
1319 λppc_ok.
1320    next_internal_pseudo_address_map0 ? cm addr_of
1321     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1322
1323definition code_memory_of_pseudo_assembly_program:
1324    ∀pap:pseudo_assembly_program.
1325      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1326  λpap.
1327  λsigma.
1328  λpolicy.
1329    let p ≝ pi1 … (assembly pap sigma policy) in
1330      load_code_memory (\fst p).
1331
1332definition sfr_8051_of_pseudo_sfr_8051 ≝
1333  λM: internal_pseudo_address_map.
1334  λsfrs: Vector Byte 19.
1335  λsigma: Word → Word.
1336    match \snd M with
1337    [ None ⇒ sfrs
1338    | Some s ⇒
1339      let 〈high, address〉 ≝ s in
1340      let index ≝ sfr_8051_index SFR_ACC_A in
1341      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
1342        if high then
1343          set_index Byte 19 sfrs index upper ?
1344        else
1345          set_index Byte 19 sfrs index lower ?
1346    ].
1347  //
1348qed.
1349
1350definition status_of_pseudo_status:
1351    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1352      ∀sigma: Word → Word. ∀policy: Word → bool.
1353        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1354  λM.
1355  λpap.
1356  λps.
1357  λsigma.
1358  λpolicy.
1359  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1360  let pc ≝ sigma (program_counter … ps) in
1361  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1362  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1363     mk_PreStatus (BitVectorTrie Byte 16)
1364      cm
1365      lir
1366      hir
1367      (external_ram … ps)
1368      pc
1369      (special_function_registers_8051 … ps)
1370      (special_function_registers_8052 … ps)
1371      (p1_latch … ps)
1372      (p3_latch … ps)
1373      (clock … ps).
1374
1375(*
1376definition write_at_stack_pointer':
1377 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1378  λM: Type[0].
1379  λs: PreStatus M.
1380  λv: Byte.
1381    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1382    let bit_zero ≝ get_index_v… nu O ? in
1383    let bit_1 ≝ get_index_v… nu 1 ? in
1384    let bit_2 ≝ get_index_v… nu 2 ? in
1385    let bit_3 ≝ get_index_v… nu 3 ? in
1386      if bit_zero then
1387        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1388                              v (low_internal_ram ? s) in
1389          set_low_internal_ram ? s memory
1390      else
1391        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1392                              v (high_internal_ram ? s) in
1393          set_high_internal_ram ? s memory.
1394  [ cases l0 %
1395  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1396qed.
1397
1398definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1399 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1400
1401  λticks_of.
1402  λs.
1403  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1404  let ticks ≝ ticks_of (program_counter ? s) in
1405  let s ≝ set_clock ? s (clock ? s + ticks) in
1406  let s ≝ set_program_counter ? s pc in
1407    match instr with
1408    [ Instruction instr ⇒
1409       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1410    | Comment cmt ⇒ s
1411    | Cost cst ⇒ s
1412    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1413    | Call call ⇒
1414      let a ≝ address_of_word_labels s call in
1415      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1416      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1417      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1418      let s ≝ write_at_stack_pointer' ? s pc_bl in
1419      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1420      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1421      let s ≝ write_at_stack_pointer' ? s pc_bu in
1422        set_program_counter ? s a
1423    | Mov dptr ident ⇒
1424       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1425    ].
1426 [
1427 |2,3,4: %
1428 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1429 |
1430 | %
1431 ]
1432 cases not_implemented
1433qed.
1434*)
1435
1436(*
1437lemma execute_code_memory_unchanged:
1438 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1439 #ticks #ps whd in ⊢ (??? (??%))
1440 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1441  (program_counter pseudo_assembly_program ps)) #instr #pc
1442 whd in ⊢ (??? (??%)) cases instr
1443  [ #pre cases pre
1444     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1445       cases (vsplit ????) #z1 #z2 %
1446     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1447       cases (vsplit ????) #z1 #z2 %
1448     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1449       cases (vsplit ????) #z1 #z2 %
1450     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1451       [ #x1 whd in ⊢ (??? (??%))
1452     | *: cases not_implemented
1453     ]
1454  | #comment %
1455  | #cost %
1456  | #label %
1457  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1458    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1459    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1460    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1461    (* CSC: ??? *)
1462  | #dptr #label (* CSC: ??? *)
1463  ]
1464  cases not_implemented
1465qed.
1466*)
1467
1468(* DEAD CODE?
1469lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1470 ∀M:internal_pseudo_address_map.
1471 ∀ps,ps': PseudoStatus.
1472 ∀pol.
1473  ∀prf:code_memory … ps = code_memory … ps'.
1474   let pol' ≝ ? in
1475   match status_of_pseudo_status M ps pol with
1476    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1477    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1478    ].
1479 [2: <prf @pol]
1480 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1481 generalize in match (refl … (assembly (code_memory … ps) pol))
1482 cases (assembly ??) in ⊢ (???% → %)
1483  [ #K whd whd in ⊢ (??%?) <H >K %
1484  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1485qed.
1486*)
1487
1488definition ticks_of0:
1489    ∀p:pseudo_assembly_program.
1490      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1491  λprogram: pseudo_assembly_program.
1492  λsigma.
1493  λpolicy.
1494  λppc: Word.
1495  λfetched.
1496    match fetched with
1497    [ Instruction instr ⇒
1498      match instr with
1499      [ JC lbl ⇒ ? (*
1500        match pol lookup_labels ppc with
1501        [ short_jump ⇒ 〈2, 2〉
1502        | absolute_jump ⇒ ?
1503        | long_jump ⇒ 〈4, 4〉
1504        ] *)
1505      | JNC lbl ⇒ ? (*
1506        match pol lookup_labels ppc with
1507        [ short_jump ⇒ 〈2, 2〉
1508        | absolute_jump ⇒ ?
1509        | long_jump ⇒ 〈4, 4〉
1510        ] *)
1511      | JB bit lbl ⇒ ? (*
1512        match pol lookup_labels ppc with
1513        [ short_jump ⇒ 〈2, 2〉
1514        | absolute_jump ⇒ ?
1515        | long_jump ⇒ 〈4, 4〉
1516        ] *)
1517      | JNB bit lbl ⇒ ? (*
1518        match pol lookup_labels ppc with
1519        [ short_jump ⇒ 〈2, 2〉
1520        | absolute_jump ⇒ ?
1521        | long_jump ⇒ 〈4, 4〉
1522        ] *)
1523      | JBC bit lbl ⇒ ? (*
1524        match pol lookup_labels ppc with
1525        [ short_jump ⇒ 〈2, 2〉
1526        | absolute_jump ⇒ ?
1527        | long_jump ⇒ 〈4, 4〉
1528        ] *)
1529      | JZ lbl ⇒ ? (*
1530        match pol lookup_labels ppc with
1531        [ short_jump ⇒ 〈2, 2〉
1532        | absolute_jump ⇒ ?
1533        | long_jump ⇒ 〈4, 4〉
1534        ] *)
1535      | JNZ lbl ⇒ ? (*
1536        match pol lookup_labels  ppc with
1537        [ short_jump ⇒ 〈2, 2〉
1538        | absolute_jump ⇒ ?
1539        | long_jump ⇒ 〈4, 4〉
1540        ] *)
1541      | CJNE arg lbl ⇒ ? (*
1542        match pol lookup_labels ppc with
1543        [ short_jump ⇒ 〈2, 2〉
1544        | absolute_jump ⇒ ?
1545        | long_jump ⇒ 〈4, 4〉
1546        ] *)
1547      | DJNZ arg lbl ⇒ ? (*
1548        match pol lookup_labels ppc with
1549        [ short_jump ⇒ 〈2, 2〉
1550        | absolute_jump ⇒ ?
1551        | long_jump ⇒ 〈4, 4〉
1552        ] *)
1553      | ADD arg1 arg2 ⇒
1554        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1555         〈ticks, ticks〉
1556      | ADDC arg1 arg2 ⇒
1557        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1558         〈ticks, ticks〉
1559      | SUBB arg1 arg2 ⇒
1560        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1561         〈ticks, ticks〉
1562      | INC arg ⇒
1563        let ticks ≝ ticks_of_instruction (INC ? arg) in
1564         〈ticks, ticks〉
1565      | DEC arg ⇒
1566        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1567         〈ticks, ticks〉
1568      | MUL arg1 arg2 ⇒
1569        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1570         〈ticks, ticks〉
1571      | DIV arg1 arg2 ⇒
1572        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1573         〈ticks, ticks〉
1574      | DA arg ⇒
1575        let ticks ≝ ticks_of_instruction (DA ? arg) in
1576         〈ticks, ticks〉
1577      | ANL arg ⇒
1578        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1579         〈ticks, ticks〉
1580      | ORL arg ⇒
1581        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1582         〈ticks, ticks〉
1583      | XRL arg ⇒
1584        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1585         〈ticks, ticks〉
1586      | CLR arg ⇒
1587        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1588         〈ticks, ticks〉
1589      | CPL arg ⇒
1590        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1591         〈ticks, ticks〉
1592      | RL arg ⇒
1593        let ticks ≝ ticks_of_instruction (RL ? arg) in
1594         〈ticks, ticks〉
1595      | RLC arg ⇒
1596        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1597         〈ticks, ticks〉
1598      | RR arg ⇒
1599        let ticks ≝ ticks_of_instruction (RR ? arg) in
1600         〈ticks, ticks〉
1601      | RRC arg ⇒
1602        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1603         〈ticks, ticks〉
1604      | SWAP arg ⇒
1605        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1606         〈ticks, ticks〉
1607      | MOV arg ⇒
1608        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1609         〈ticks, ticks〉
1610      | MOVX arg ⇒
1611        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1612         〈ticks, ticks〉
1613      | SETB arg ⇒
1614        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1615         〈ticks, ticks〉
1616      | PUSH arg ⇒
1617        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1618         〈ticks, ticks〉
1619      | POP arg ⇒
1620        let ticks ≝ ticks_of_instruction (POP ? arg) in
1621         〈ticks, ticks〉
1622      | XCH arg1 arg2 ⇒
1623        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1624         〈ticks, ticks〉
1625      | XCHD arg1 arg2 ⇒
1626        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1627         〈ticks, ticks〉
1628      | RET ⇒
1629        let ticks ≝ ticks_of_instruction (RET ?) in
1630         〈ticks, ticks〉
1631      | RETI ⇒
1632        let ticks ≝ ticks_of_instruction (RETI ?) in
1633         〈ticks, ticks〉
1634      | NOP ⇒
1635        let ticks ≝ ticks_of_instruction (NOP ?) in
1636         〈ticks, ticks〉
1637      ]
1638    | Comment comment ⇒ 〈0, 0〉
1639    | Cost cost ⇒ 〈0, 0〉
1640    | Jmp jmp ⇒ 〈2, 2〉
1641    | Call call ⇒ 〈2, 2〉
1642    | Mov dptr tgt ⇒ 〈2, 2〉
1643    ].
1644    cases daemon
1645qed.
1646
1647definition ticks_of:
1648    ∀p:pseudo_assembly_program.
1649      (Word → Word) → (Word → bool) → ∀ppc:Word.
1650       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1651  λprogram: pseudo_assembly_program.
1652  λsigma.
1653  λpolicy.
1654  λppc: Word. λppc_ok.
1655    let pseudo ≝ \snd program in
1656    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1657     ticks_of0 program sigma policy ppc fetched.
1658
1659lemma eq_rect_Type1_r:
1660  ∀A: Type[1].
1661  ∀a: A.
1662  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1663  #A #a #P #H #x #p
1664  generalize in match H;
1665  generalize in match P;
1666  cases p //
1667qed.
1668
1669axiom vsplit_append:
1670  ∀A: Type[0].
1671  ∀m, n: nat.
1672  ∀v, v': Vector A m.
1673  ∀q, q': Vector A n.
1674    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
1675      v = v' ∧ q = q'.
1676
1677lemma vsplit_vector_singleton:
1678  ∀A: Type[0].
1679  ∀n: nat.
1680  ∀v: Vector A (S n).
1681  ∀rest: Vector A n.
1682  ∀s: Vector A 1.
1683    v = s @@ rest →
1684    ((get_index_v A ? v 0 ?) ::: rest) = v.
1685  [1:
1686    #A #n #v cases daemon (* XXX: !!! *)
1687  |2:
1688    @le_S_S @le_O_n
1689  ]
1690qed.
1691
1692example sub_minus_one_seven_eight:
1693  ∀v: BitVector 7.
1694  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1695  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1696 cases daemon.
1697qed.
1698
1699(*
1700lemma blah:
1701  ∀m: internal_pseudo_address_map.
1702  ∀s: PseudoStatus.
1703  ∀arg: Byte.
1704  ∀b: bool.
1705    addressing_mode_ok m s (DIRECT arg) = true →
1706      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1707      get_arg_8 ? s b (DIRECT arg).
1708  [2, 3: normalize % ]
1709  #m #s #arg #b #hyp
1710  whd in ⊢ (??%%)
1711  @vsplit_elim''
1712  #nu' #nl' #arg_nu_nl_eq
1713  normalize nodelta
1714  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1715  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1716  #get_index_v_eq
1717  normalize nodelta
1718  [2:
1719    normalize nodelta
1720    @vsplit_elim''
1721    #bit_one' #three_bits' #bit_one_three_bit_eq
1722    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1723    normalize nodelta
1724    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1725    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1726    #Saddr #carr' #Saddr_carr_eq
1727    normalize nodelta
1728    #carr_hyp'
1729    @carr_hyp'
1730    [1:
1731    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1732        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1733        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1734        #member_eq
1735        normalize nodelta
1736        [2: #destr destruct(destr)
1737        |1: -carr_hyp';
1738            >arg_nu_nl_eq
1739            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1740            [1: >get_index_v_eq in ⊢ (??%? → ?)
1741            |2: @le_S @le_S @le_S @le_n
1742            ]
1743            cases (member (BitVector 8) ? (\fst ?) ?)
1744            [1: #destr normalize in destr; destruct(destr)
1745            |2:
1746            ]
1747        ]
1748    |3: >get_index_v_eq in ⊢ (??%?)
1749        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1750        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1751        <arg_nu_nl_eq
1752        whd in hyp:(??%?)
1753        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1754        normalize nodelta [*: #ignore @sym_eq ]
1755    ]
1756  |
1757  ].
1758*)
1759(*
1760map_address0 ... (DIRECT arg) = Some .. →
1761  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1762  get_arg_8 (internal_ram ...) (DIRECT arg)
1763
1764((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1765                     then Some internal_pseudo_address_map M 
1766                     else None internal_pseudo_address_map )
1767                    =Some internal_pseudo_address_map M')
1768
1769axiom low_internal_ram_write_at_stack_pointer:
1770 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1771 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1772  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1773  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1774  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1775  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1776  bu@@bl = sigma (pbu@@pbl) →
1777   low_internal_ram T1 cm1
1778     (write_at_stack_pointer …
1779       (set_8051_sfr …
1780         (write_at_stack_pointer …
1781           (set_8051_sfr …
1782             (set_low_internal_ram … s1
1783               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1784             SFR_SP sp1)
1785          bl)
1786        SFR_SP sp2)
1787      bu)
1788   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1789      (low_internal_ram …
1790       (write_at_stack_pointer …
1791         (set_8051_sfr …
1792           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1793          SFR_SP sp2)
1794        pbu)).
1795
1796lemma high_internal_ram_write_at_stack_pointer:
1797 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1798 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1799  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1800  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1801  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1802  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1803  bu@@bl = sigma (pbu@@pbl) →
1804   high_internal_ram T1 cm1
1805     (write_at_stack_pointer …
1806       (set_8051_sfr …
1807         (write_at_stack_pointer …
1808           (set_8051_sfr …
1809             (set_high_internal_ram … s1
1810               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1811             SFR_SP sp1)
1812          bl)
1813        SFR_SP sp2)
1814      bu)
1815   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1816      (high_internal_ram …
1817       (write_at_stack_pointer …
1818         (set_8051_sfr …
1819           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1820          SFR_SP sp2)
1821        pbu)).
1822  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1823  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1824  cases daemon (* XXX: !!! *)
1825qed.
1826*)
1827
1828lemma Some_Some_elim:
1829 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
1830 #T #x #y #P #H #K @H @option_destruct_Some //
1831qed.
1832
1833lemma pair_destruct_right:
1834  ∀A: Type[0].
1835  ∀B: Type[0].
1836  ∀a, c: A.
1837  ∀b, d: B.
1838    〈a, b〉 = 〈c, d〉 → b = d.
1839  #A #B #a #b #c #d //
1840qed.
1841   
1842(*CSC: ???*)
1843(* XXX: we need a precondition here stating that the PPC is within the
1844        bounds of the instruction list in order for Jaap's specification to
1845        apply.
1846*)
1847lemma snd_assembly_1_pseudoinstruction_ok:
1848  ∀program: pseudo_assembly_program.
1849  ∀program_length_proof: |\snd program| ≤ 2^16.
1850  ∀sigma: Word → Word.
1851  ∀policy: Word → bool.
1852  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1853  ∀ppc: Word.
1854  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1855  ∀pi.
1856  ∀lookup_labels.
1857  ∀lookup_datalabels.
1858    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
1859    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1860    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1861    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1862      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1863  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1864  #lookup_labels #lookup_datalabels
1865  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1866  normalize nodelta
1867  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1868  #fetch_pseudo_refl
1869  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1870  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1871  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1872  @pair_elim #preamble #instr_list #program_refl
1873  @pair_elim #labels #costs' #create_label_cost_map_refl
1874  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1875  lapply (H ppc ppc_in_bounds) -H
1876  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1877  @pair_elim #len #assembled #assembly1_refl #H
1878  cases H
1879  #encoding_check_assm #sigma_newppc_refl
1880  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1881  >pi_refl' in assembly1_refl; #assembly1_refl
1882  >lookup_labels_refl >lookup_datalabels_refl
1883  >program_refl normalize nodelta
1884  >assembly1_refl
1885  <sigma_newppc_refl
1886  generalize in match fetch_pseudo_refl';
1887  whd in match (fetch_pseudo_instruction ???);
1888  @pair_elim #lbl #instr #nth_refl normalize nodelta
1889  #G cases (pair_destruct_right ?????? G) %
1890qed.
1891
1892lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
1893  /2/
1894qed.
1895
1896(* To be moved in ProofStatus *)
1897lemma program_counter_set_program_counter:
1898  ∀T.
1899  ∀cm.
1900  ∀s.
1901  ∀x.
1902    program_counter T cm (set_program_counter T cm s x) = x.
1903  //
1904qed.
1905
1906(* XXX: easy but tedious *)
1907lemma assembly1_lt_128:
1908  ∀i: instruction.
1909    |(assembly1 i)| < 128.
1910  #i cases i
1911  try (#assm1 #assm2) try #assm1
1912  [8:
1913    cases assm1
1914    try (#assm1 #assm2) try #assm1
1915    whd in match assembly1; normalize nodelta
1916    whd in match assembly_preinstruction; normalize nodelta
1917    try @(subaddressing_mode_elim … assm2)
1918    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
1919    [32:
1920      cases assm1 -assm1 #assm1 normalize nodelta
1921      cases assm1 #addr1 #addr2 normalize nodelta
1922      [1:
1923        @(subaddressing_mode_elim … addr2)
1924      |2:
1925        @(subaddressing_mode_elim … addr1)
1926      ]
1927      #w
1928    |35,36,37:
1929      cases assm1 -assm1 #assm1 normalize nodelta
1930      [1,3:
1931        cases assm1 -assm1 #assm1 normalize nodelta
1932      ]
1933      cases assm1 #addr1 #addr2 normalize nodelta
1934      @(subaddressing_mode_elim … addr2) try #w
1935    |49:
1936      cases assm1 -assm1 #assm1 normalize nodelta
1937      [1:
1938        cases assm1 -assm1 #assm1 normalize nodelta
1939        [1:
1940          cases assm1 -assm1 #assm1 normalize nodelta
1941          [1:
1942            cases assm1 -assm1 #assm1 normalize nodelta
1943            [1:
1944              cases assm1 -assm1 #assm1 normalize nodelta
1945            ]
1946          ]
1947        ]
1948      ]
1949      cases assm1 #addr1 #addr2 normalize nodelta
1950      [1,3,4,5:
1951        @(subaddressing_mode_elim … addr2) try #w
1952      |*:
1953        @(subaddressing_mode_elim … addr1) try #w
1954        normalize nodelta
1955        [1,2:
1956          @(subaddressing_mode_elim … addr2) try #w
1957        ]
1958      ]
1959    |50:
1960      cases assm1 -assm1 #assm1 normalize nodelta
1961      cases assm1 #addr1 #addr2 normalize nodelta
1962      [1:
1963        @(subaddressing_mode_elim … addr2) try #w
1964      |2:
1965        @(subaddressing_mode_elim … addr1) try #w
1966      ]
1967    ]
1968    normalize repeat @le_S_S @le_O_n
1969  ]
1970  whd in match assembly1; normalize nodelta
1971  [6:
1972    normalize repeat @le_S_S @le_O_n
1973  |7:
1974    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
1975  |*:
1976    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
1977  ]
1978qed.
Note: See TracBrowser for help on using the repository browser.