source: src/ASM/AssemblyProof.ma @ 2112

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

WARNING: this commit may break some code.

  • dead/useless code removed
File size: 64.9 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 XXX
938 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
939(*
940 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
941 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
942 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
943  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
944  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
945 whd >eq_instruction_refl >H4 @eq_bv_refl
946*) (* XXX: not working! *)
947qed.
948
949let rec fetch_many
950  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
951    (expected: list instruction)
952      on expected: Prop ≝
953  match expected with
954  [ nil ⇒ eq_bv … pc final_pc = true
955  | cons i tl ⇒
956    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
957      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
958        fetch_many code_memory final_pc pc' tl)
959  ].
960
961lemma option_destruct_Some:
962  ∀A: Type[0].
963  ∀a, b: A.
964    Some A a = Some A b → a = b.
965  #A #a #b #EQ
966  destruct %
967qed.
968
969lemma eq_instruction_to_eq:
970  ∀i1, i2: instruction.
971    eq_instruction i1 i2 = true → i1 ≃ i2.
972  #i1 #i2
973  cases i1 cases i2 cases daemon (*
974  [1,10,19,28,37,46:
975    #arg1 #arg2
976    whd in match (eq_instruction ??);
977    cases arg1 #subaddressing_mode
978    cases subaddressing_mode
979    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
980    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
981    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
982    #word11 #irrelevant
983    cases arg2 #subaddressing_mode
984    cases subaddressing_mode
985    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
986    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
987    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
988    #word11' #irrelevant normalize nodelta
989    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
990qed.
991         
992lemma fetch_assembly_pseudo':
993  ∀lookup_labels.
994  ∀sigma: Word → Word.
995  ∀policy: Word → bool.
996  ∀ppc.
997  ∀lookup_datalabels.
998  ∀pi.
999  ∀code_memory.
1000  ∀len.
1001  ∀assembled.
1002  ∀instructions.
1003    let pc ≝ sigma ppc in
1004      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
1005        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
1006          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1007            encoding_check code_memory pc pc_plus_len assembled →
1008              fetch_many code_memory pc_plus_len pc instructions.
1009  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
1010  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
1011  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
1012  >len_refl >assembled_refl -len_refl
1013  generalize in match (add 16 (sigma ppc)
1014    (bitvector_of_nat 16
1015     (|flatten (Vector bool 8)
1016       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
1017  #final_pc
1018  generalize in match (sigma ppc); elim instructions
1019  [1:
1020    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
1021  |2:
1022    #i #tl #IH #pc #H whd
1023    cases (encoding_check_append ????? H) -H #H1 #H2
1024    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
1025    cases (fetch ??) * #instr #pc' #ticks
1026    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
1027    lapply (conjunction_true ?? H3) * #H4 #H5
1028    lapply (conjunction_true … H4) * #B1 #B2
1029    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
1030    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
1031  ]
1032qed.
1033
1034lemma fetch_assembly_pseudo:
1035  ∀program: pseudo_assembly_program.
1036  ∀sigma: Word → Word.
1037  ∀policy: Word → bool.
1038  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
1039  ∀ppc.∀ppc_ok.
1040  ∀code_memory.
1041  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
1042  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
1043  let pc ≝ sigma ppc in
1044  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1045  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1046  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1047    encoding_check code_memory pc pc_plus_len assembled →
1048      fetch_many code_memory pc_plus_len pc instructions.
1049  #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
1050  letin lookup_datalabels ≝ (λx.?)
1051  letin pi ≝ (fst ???)
1052  letin pc ≝ (sigma ?)
1053  letin instructions ≝ (expand_pseudo_instruction ??????)
1054  @pair_elim #len #assembled #assembled_refl normalize nodelta
1055  #H
1056  generalize in match
1057   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
1058  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
1059qed.
1060
1061definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
1062  λpseudo_instruction.
1063    match pseudo_instruction with
1064    [ Comment c ⇒ False
1065    | Cost c ⇒ False
1066    | _ ⇒ True
1067    ].
1068
1069(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
1070   function that load the code in memory is correct. The latter is based
1071   on missing properties from the standard library on the BitVectorTrie
1072   data structrure.
1073   
1074   Wrong at the moment, requires Jaap's precondition to ensure that the program
1075   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
1076*)
1077
1078lemma load_code_memory_ok:
1079 ∀program.
1080 let program_size ≝ |program| in
1081  program_size ≤ 2^16 →
1082   ∀pc. ∀pc_ok: pc < program_size.
1083    nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
1084 #program elim program
1085 [ #_ #pc #abs normalize in abs; @⊥ /2/
1086 | #hd #tl #IH #size_ok *
1087   [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
1088     whd in match next; normalize nodelta
1089   | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
1090     whd in match next; normalize nodelta
1091   ]
1092 cases daemon (*CSC: complete! *)
1093qed.
1094(*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
1095Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
1096e' come fetchare l'i-esimo bit dalla memoria.
1097Concludere assembly_ok come semplice corollario.
1098*)
1099lemma assembly_ok:
1100  ∀program.
1101  ∀length_proof: |\snd program| ≤ 2^16.
1102  ∀sigma: Word → Word.
1103  ∀policy: Word → bool.
1104  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
1105  ∀assembled.
1106  ∀costs': BitVectorTrie costlabel 16.
1107  let 〈preamble, instr_list〉 ≝ program in
1108  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
1109  let datalabels ≝ construct_datalabels preamble in
1110  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
1111    〈assembled,costs'〉 = assembly program sigma policy →
1112      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
1113        let code_memory ≝ load_code_memory assembled in
1114        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
1115          ∀ppc.∀ppc_ok.
1116            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
1117            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
1118            let pc ≝ sigma ppc in
1119            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
1120              encoding_check code_memory pc pc_plus_len assembled ∧
1121                  sigma newppc = add … pc (bitvector_of_nat … len).
1122  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
1123  cases (assembly program sigma policy) * #assembled' #costs''
1124  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
1125  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
1126  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
1127  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
1128  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
1129  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
1130  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
1131  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
1132  >eq_fetch_pseudo_instruction
1133  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
1134  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
1135       (λx.address_of_word_labels_code_mem instr_list x)))
1136  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
1137      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
1138  >eq_assembly_1_pseudoinstruction
1139  whd in ⊢ (% → ?); #assembly_ok
1140  %
1141  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
1142      >snd_fetch_pseudo_instruction
1143      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
1144      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
1145      >eq_fetch_pseudo_instruction whd in match instruction_size;
1146      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
1147      cases daemon
1148  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
1149    #load_code_memory_ok
1150    cut (len=|assembled|)
1151    [1: (*CSC: provable before cleaning *)
1152        cases daemon
1153    ]
1154    #EQlen
1155    (* Nice statement here *)
1156    cut (∀j. ∀H: j < |assembled|.
1157          nth_safe Byte j assembled H =
1158          \snd (next (load_code_memory assembled')
1159          (bitvector_of_nat 16
1160           (nat_of_bitvector …
1161            (add … (sigma ppc) (bitvector_of_nat … j))))))
1162    [1:
1163      cases daemon
1164    |2:
1165      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
1166      elim assembled
1167      [1:
1168        #pc #_ whd <add_zero %
1169      | #hd #tl #IH #pc #H %
1170         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
1171           >H -H whd in ⊢ (??%?); <add_zero //
1172         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
1173           [2: <add_bitvector_of_nat_Sm @add_associative ]
1174           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
1175           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
1176           >add_associative % ]]
1177  ]]
1178qed.
1179
1180(* XXX: should we add that costs = costs'? *)
1181lemma fetch_assembly_pseudo2:
1182  ∀program.
1183  ∀length_proof: |\snd program| ≤ 2^16.
1184  ∀sigma.
1185  ∀policy.
1186  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1187  ∀ppc.∀ppc_ok.
1188  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
1189  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
1190  let code_memory ≝ load_code_memory assembled in
1191  let data_labels ≝ construct_datalabels (\fst program) in
1192  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
1193  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
1194  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
1195  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
1196    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
1197  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
1198  @pair_elim #labels #costs #create_label_map_refl
1199  @pair_elim #assembled #costs' #assembled_refl
1200  letin code_memory ≝ (load_code_memory ?)
1201  letin data_labels ≝ (construct_datalabels ?)
1202  letin lookup_labels ≝ (λx. ?)
1203  letin lookup_datalabels ≝ (λx. ?)
1204  @pair_elim #pi #newppc #fetch_pseudo_refl
1205  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
1206  normalize nodelta try assumption
1207  @pair_elim #labels' #costs' #create_label_map_refl' #H
1208  lapply (H (sym_eq … assembled_refl)) -H
1209  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
1210  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
1211  #len #assembledi #EQ4 #H
1212  lapply (H ppc) >fetch_pseudo_refl #H
1213  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
1214  >EQ4 #H1 cases (H ppc_ok)
1215  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
1216  >fetch_pseudo_refl in H1; #assm @assm assumption
1217qed.
1218
1219(* OLD?
1220definition assembly_specification:
1221  ∀assembly_program: pseudo_assembly_program.
1222  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1223  λpseudo_assembly_program.
1224  λcode_mem.
1225    ∀pc: Word.
1226      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1227      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1228      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1229      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1230      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1231       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1232      match pre_assembled with
1233       [ None ⇒ True
1234       | Some pc_code ⇒
1235          let 〈new_pc,code〉 ≝ pc_code in
1236           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1237
1238axiom assembly_meets_specification:
1239  ∀pseudo_assembly_program.
1240    match assembly pseudo_assembly_program with
1241    [ None ⇒ True
1242    | Some code_mem_cost ⇒
1243      let 〈code_mem, cost〉 ≝ code_mem_cost in
1244        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1245    ].
1246(*
1247  # PROGRAM
1248  [ cases PROGRAM
1249    # PREAMBLE
1250    # INSTR_LIST
1251    elim INSTR_LIST
1252    [ whd
1253      whd in ⊢ (∀_. %)
1254      # PC
1255      whd
1256    | # INSTR
1257      # INSTR_LIST_TL
1258      # H
1259      whd
1260      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1261    ]
1262  | cases not_implemented
1263  ] *)
1264*)
1265
1266(* XXX: changed this type.  Bool specifies whether byte is first or second
1267        component of an address, and the Word is the pseudoaddress that it
1268        corresponds to.  Second component is the same principle for the accumulator
1269        A.
1270*)
1271definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
1272
1273include alias "ASM/BitVectorTrie.ma".
1274 
1275include "common/AssocList.ma".
1276
1277axiom low_internal_ram_of_pseudo_low_internal_ram:
1278 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1279
1280axiom high_internal_ram_of_pseudo_high_internal_ram:
1281 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1282
1283axiom low_internal_ram_of_pseudo_internal_ram_hit:
1284 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
1285  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
1286   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1287   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1288   let bl ≝ lookup ? 7 addr ram (zero 8) in
1289   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
1290   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
1291     if high then
1292       (pbl = higher) ∧ (bl = phigher)
1293     else
1294       (pbl = lower) ∧ (bl = plower).
1295
1296(* changed from add to sub *)
1297axiom low_internal_ram_of_pseudo_internal_ram_miss:
1298 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
1299  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1300    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
1301      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1302
1303definition addressing_mode_ok ≝
1304 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
1305  λaddr:addressing_mode.
1306   match addr with
1307    [ DIRECT d ⇒
1308       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1309       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1310    | INDIRECT i ⇒
1311       let d ≝ get_register … s [[false;false;i]] in
1312       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1313       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1314    | EXT_INDIRECT _ ⇒ true
1315    | REGISTER _ ⇒ true
1316    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
1317    | ACC_B ⇒ true
1318    | DPTR ⇒ true
1319    | DATA _ ⇒ true
1320    | DATA16 _ ⇒ true
1321    | ACC_DPTR ⇒ true
1322    | ACC_PC ⇒ true
1323    | EXT_INDIRECT_DPTR ⇒ true
1324    | INDIRECT_DPTR ⇒ true
1325    | CARRY ⇒ true
1326    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1327    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1328    | RELATIVE _ ⇒ true
1329    | ADDR11 _ ⇒ true
1330    | ADDR16 _ ⇒ true ].
1331   
1332definition next_internal_pseudo_address_map0 ≝
1333  λT.
1334  λcm:T.
1335  λaddr_of: Identifier → PreStatus T cm → Word.
1336  λfetched.
1337  λM: internal_pseudo_address_map.
1338  λs: PreStatus T cm.
1339   match fetched with
1340    [ Comment _ ⇒ Some ? M
1341    | Cost _ ⇒ Some … M
1342    | Jmp _ ⇒ Some … M
1343    | Call a ⇒
1344      let a' ≝ addr_of a s in
1345      let 〈callM, accM〉 ≝ M in
1346         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
1347                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
1348    | Mov _ _ ⇒ Some … M
1349    | Instruction instr ⇒
1350       match instr with
1351        [ ADD addr1 addr2 ⇒
1352           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1353            Some ? M
1354           else
1355            None ?
1356        | ADDC addr1 addr2 ⇒
1357           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1358            Some ? M
1359           else
1360            None ?
1361        | SUBB addr1 addr2 ⇒
1362           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1363            Some ? M
1364           else
1365            None ?       
1366        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1367
1368definition next_internal_pseudo_address_map ≝
1369 λM:internal_pseudo_address_map.
1370 λcm.
1371 λaddr_of.
1372 λs:PseudoStatus cm.
1373 λppc_ok.
1374    next_internal_pseudo_address_map0 ? cm addr_of
1375     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1376
1377definition code_memory_of_pseudo_assembly_program:
1378    ∀pap:pseudo_assembly_program.
1379      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1380  λpap.
1381  λsigma.
1382  λpolicy.
1383    let p ≝ pi1 … (assembly pap sigma policy) in
1384      load_code_memory (\fst p).
1385
1386definition sfr_8051_of_pseudo_sfr_8051 ≝
1387  λM: internal_pseudo_address_map.
1388  λsfrs: Vector Byte 19.
1389  λsigma: Word → Word.
1390    match \snd M with
1391    [ None ⇒ sfrs
1392    | Some s ⇒
1393      let 〈high, address〉 ≝ s in
1394      let index ≝ sfr_8051_index SFR_ACC_A in
1395      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
1396        if high then
1397          set_index Byte 19 sfrs index upper ?
1398        else
1399          set_index Byte 19 sfrs index lower ?
1400    ].
1401  //
1402qed.
1403
1404definition status_of_pseudo_status:
1405    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1406      ∀sigma: Word → Word. ∀policy: Word → bool.
1407        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1408  λM.
1409  λpap.
1410  λps.
1411  λsigma.
1412  λpolicy.
1413  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1414  let pc ≝ sigma (program_counter … ps) in
1415  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1416  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1417     mk_PreStatus (BitVectorTrie Byte 16)
1418      cm
1419      lir
1420      hir
1421      (external_ram … ps)
1422      pc
1423      (special_function_registers_8051 … ps)
1424      (special_function_registers_8052 … ps)
1425      (p1_latch … ps)
1426      (p3_latch … ps)
1427      (clock … ps).
1428
1429(*
1430definition write_at_stack_pointer':
1431 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1432  λM: Type[0].
1433  λs: PreStatus M.
1434  λv: Byte.
1435    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1436    let bit_zero ≝ get_index_v… nu O ? in
1437    let bit_1 ≝ get_index_v… nu 1 ? in
1438    let bit_2 ≝ get_index_v… nu 2 ? in
1439    let bit_3 ≝ get_index_v… nu 3 ? in
1440      if bit_zero then
1441        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1442                              v (low_internal_ram ? s) in
1443          set_low_internal_ram ? s memory
1444      else
1445        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1446                              v (high_internal_ram ? s) in
1447          set_high_internal_ram ? s memory.
1448  [ cases l0 %
1449  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1450qed.
1451
1452definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1453 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1454
1455  λticks_of.
1456  λs.
1457  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1458  let ticks ≝ ticks_of (program_counter ? s) in
1459  let s ≝ set_clock ? s (clock ? s + ticks) in
1460  let s ≝ set_program_counter ? s pc in
1461    match instr with
1462    [ Instruction instr ⇒
1463       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1464    | Comment cmt ⇒ s
1465    | Cost cst ⇒ s
1466    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1467    | Call call ⇒
1468      let a ≝ address_of_word_labels s call in
1469      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1470      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1471      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1472      let s ≝ write_at_stack_pointer' ? s pc_bl in
1473      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1474      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1475      let s ≝ write_at_stack_pointer' ? s pc_bu in
1476        set_program_counter ? s a
1477    | Mov dptr ident ⇒
1478       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1479    ].
1480 [
1481 |2,3,4: %
1482 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1483 |
1484 | %
1485 ]
1486 cases not_implemented
1487qed.
1488*)
1489
1490(*
1491lemma execute_code_memory_unchanged:
1492 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1493 #ticks #ps whd in ⊢ (??? (??%))
1494 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1495  (program_counter pseudo_assembly_program ps)) #instr #pc
1496 whd in ⊢ (??? (??%)) cases instr
1497  [ #pre cases pre
1498     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1499       cases (vsplit ????) #z1 #z2 %
1500     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1501       cases (vsplit ????) #z1 #z2 %
1502     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1503       cases (vsplit ????) #z1 #z2 %
1504     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1505       [ #x1 whd in ⊢ (??? (??%))
1506     | *: cases not_implemented
1507     ]
1508  | #comment %
1509  | #cost %
1510  | #label %
1511  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1512    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1513    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1514    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1515    (* CSC: ??? *)
1516  | #dptr #label (* CSC: ??? *)
1517  ]
1518  cases not_implemented
1519qed.
1520*)
1521
1522(* DEAD CODE?
1523lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1524 ∀M:internal_pseudo_address_map.
1525 ∀ps,ps': PseudoStatus.
1526 ∀pol.
1527  ∀prf:code_memory … ps = code_memory … ps'.
1528   let pol' ≝ ? in
1529   match status_of_pseudo_status M ps pol with
1530    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1531    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1532    ].
1533 [2: <prf @pol]
1534 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1535 generalize in match (refl … (assembly (code_memory … ps) pol))
1536 cases (assembly ??) in ⊢ (???% → %)
1537  [ #K whd whd in ⊢ (??%?) <H >K %
1538  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1539qed.
1540*)
1541
1542definition ticks_of0:
1543    ∀p:pseudo_assembly_program.
1544      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1545  λprogram: pseudo_assembly_program.
1546  λsigma.
1547  λpolicy.
1548  λppc: Word.
1549  λfetched.
1550    match fetched with
1551    [ Instruction instr ⇒
1552      match instr with
1553      [ JC lbl ⇒ ? (*
1554        match pol lookup_labels ppc with
1555        [ short_jump ⇒ 〈2, 2〉
1556        | absolute_jump ⇒ ?
1557        | long_jump ⇒ 〈4, 4〉
1558        ] *)
1559      | JNC lbl ⇒ ? (*
1560        match pol lookup_labels ppc with
1561        [ short_jump ⇒ 〈2, 2〉
1562        | absolute_jump ⇒ ?
1563        | long_jump ⇒ 〈4, 4〉
1564        ] *)
1565      | JB bit lbl ⇒ ? (*
1566        match pol lookup_labels ppc with
1567        [ short_jump ⇒ 〈2, 2〉
1568        | absolute_jump ⇒ ?
1569        | long_jump ⇒ 〈4, 4〉
1570        ] *)
1571      | JNB bit lbl ⇒ ? (*
1572        match pol lookup_labels ppc with
1573        [ short_jump ⇒ 〈2, 2〉
1574        | absolute_jump ⇒ ?
1575        | long_jump ⇒ 〈4, 4〉
1576        ] *)
1577      | JBC bit lbl ⇒ ? (*
1578        match pol lookup_labels ppc with
1579        [ short_jump ⇒ 〈2, 2〉
1580        | absolute_jump ⇒ ?
1581        | long_jump ⇒ 〈4, 4〉
1582        ] *)
1583      | JZ lbl ⇒ ? (*
1584        match pol lookup_labels ppc with
1585        [ short_jump ⇒ 〈2, 2〉
1586        | absolute_jump ⇒ ?
1587        | long_jump ⇒ 〈4, 4〉
1588        ] *)
1589      | JNZ lbl ⇒ ? (*
1590        match pol lookup_labels  ppc with
1591        [ short_jump ⇒ 〈2, 2〉
1592        | absolute_jump ⇒ ?
1593        | long_jump ⇒ 〈4, 4〉
1594        ] *)
1595      | CJNE arg lbl ⇒ ? (*
1596        match pol lookup_labels ppc with
1597        [ short_jump ⇒ 〈2, 2〉
1598        | absolute_jump ⇒ ?
1599        | long_jump ⇒ 〈4, 4〉
1600        ] *)
1601      | DJNZ arg lbl ⇒ ? (*
1602        match pol lookup_labels ppc with
1603        [ short_jump ⇒ 〈2, 2〉
1604        | absolute_jump ⇒ ?
1605        | long_jump ⇒ 〈4, 4〉
1606        ] *)
1607      | ADD arg1 arg2 ⇒
1608        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1609         〈ticks, ticks〉
1610      | ADDC arg1 arg2 ⇒
1611        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1612         〈ticks, ticks〉
1613      | SUBB arg1 arg2 ⇒
1614        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1615         〈ticks, ticks〉
1616      | INC arg ⇒
1617        let ticks ≝ ticks_of_instruction (INC ? arg) in
1618         〈ticks, ticks〉
1619      | DEC arg ⇒
1620        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1621         〈ticks, ticks〉
1622      | MUL arg1 arg2 ⇒
1623        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1624         〈ticks, ticks〉
1625      | DIV arg1 arg2 ⇒
1626        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1627         〈ticks, ticks〉
1628      | DA arg ⇒
1629        let ticks ≝ ticks_of_instruction (DA ? arg) in
1630         〈ticks, ticks〉
1631      | ANL arg ⇒
1632        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1633         〈ticks, ticks〉
1634      | ORL arg ⇒
1635        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1636         〈ticks, ticks〉
1637      | XRL arg ⇒
1638        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1639         〈ticks, ticks〉
1640      | CLR arg ⇒
1641        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1642         〈ticks, ticks〉
1643      | CPL arg ⇒
1644        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1645         〈ticks, ticks〉
1646      | RL arg ⇒
1647        let ticks ≝ ticks_of_instruction (RL ? arg) in
1648         〈ticks, ticks〉
1649      | RLC arg ⇒
1650        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1651         〈ticks, ticks〉
1652      | RR arg ⇒
1653        let ticks ≝ ticks_of_instruction (RR ? arg) in
1654         〈ticks, ticks〉
1655      | RRC arg ⇒
1656        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1657         〈ticks, ticks〉
1658      | SWAP arg ⇒
1659        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1660         〈ticks, ticks〉
1661      | MOV arg ⇒
1662        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1663         〈ticks, ticks〉
1664      | MOVX arg ⇒
1665        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1666         〈ticks, ticks〉
1667      | SETB arg ⇒
1668        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1669         〈ticks, ticks〉
1670      | PUSH arg ⇒
1671        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1672         〈ticks, ticks〉
1673      | POP arg ⇒
1674        let ticks ≝ ticks_of_instruction (POP ? arg) in
1675         〈ticks, ticks〉
1676      | XCH arg1 arg2 ⇒
1677        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1678         〈ticks, ticks〉
1679      | XCHD arg1 arg2 ⇒
1680        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1681         〈ticks, ticks〉
1682      | RET ⇒
1683        let ticks ≝ ticks_of_instruction (RET ?) in
1684         〈ticks, ticks〉
1685      | RETI ⇒
1686        let ticks ≝ ticks_of_instruction (RETI ?) in
1687         〈ticks, ticks〉
1688      | NOP ⇒
1689        let ticks ≝ ticks_of_instruction (NOP ?) in
1690         〈ticks, ticks〉
1691      ]
1692    | Comment comment ⇒ 〈0, 0〉
1693    | Cost cost ⇒ 〈0, 0〉
1694    | Jmp jmp ⇒ 〈2, 2〉
1695    | Call call ⇒ 〈2, 2〉
1696    | Mov dptr tgt ⇒ 〈2, 2〉
1697    ].
1698    cases daemon
1699qed.
1700
1701definition ticks_of:
1702    ∀p:pseudo_assembly_program.
1703      (Word → Word) → (Word → bool) → ∀ppc:Word.
1704       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1705  λprogram: pseudo_assembly_program.
1706  λsigma.
1707  λpolicy.
1708  λppc: Word. λppc_ok.
1709    let pseudo ≝ \snd program in
1710    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1711     ticks_of0 program sigma policy ppc fetched.
1712
1713lemma eq_rect_Type1_r:
1714  ∀A: Type[1].
1715  ∀a: A.
1716  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1717  #A #a #P #H #x #p
1718  generalize in match H;
1719  generalize in match P;
1720  cases p //
1721qed.
1722
1723axiom vsplit_append:
1724  ∀A: Type[0].
1725  ∀m, n: nat.
1726  ∀v, v': Vector A m.
1727  ∀q, q': Vector A n.
1728    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
1729      v = v' ∧ q = q'.
1730
1731lemma vsplit_vector_singleton:
1732  ∀A: Type[0].
1733  ∀n: nat.
1734  ∀v: Vector A (S n).
1735  ∀rest: Vector A n.
1736  ∀s: Vector A 1.
1737    v = s @@ rest →
1738    ((get_index_v A ? v 0 ?) ::: rest) = v.
1739  [1:
1740    #A #n #v cases daemon (* XXX: !!! *)
1741  |2:
1742    @le_S_S @le_O_n
1743  ]
1744qed.
1745
1746example sub_minus_one_seven_eight:
1747  ∀v: BitVector 7.
1748  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1749  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1750 cases daemon.
1751qed.
1752
1753(*
1754lemma blah:
1755  ∀m: internal_pseudo_address_map.
1756  ∀s: PseudoStatus.
1757  ∀arg: Byte.
1758  ∀b: bool.
1759    addressing_mode_ok m s (DIRECT arg) = true →
1760      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1761      get_arg_8 ? s b (DIRECT arg).
1762  [2, 3: normalize % ]
1763  #m #s #arg #b #hyp
1764  whd in ⊢ (??%%)
1765  @vsplit_elim''
1766  #nu' #nl' #arg_nu_nl_eq
1767  normalize nodelta
1768  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1769  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1770  #get_index_v_eq
1771  normalize nodelta
1772  [2:
1773    normalize nodelta
1774    @vsplit_elim''
1775    #bit_one' #three_bits' #bit_one_three_bit_eq
1776    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1777    normalize nodelta
1778    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1779    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1780    #Saddr #carr' #Saddr_carr_eq
1781    normalize nodelta
1782    #carr_hyp'
1783    @carr_hyp'
1784    [1:
1785    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1786        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1787        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1788        #member_eq
1789        normalize nodelta
1790        [2: #destr destruct(destr)
1791        |1: -carr_hyp';
1792            >arg_nu_nl_eq
1793            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1794            [1: >get_index_v_eq in ⊢ (??%? → ?)
1795            |2: @le_S @le_S @le_S @le_n
1796            ]
1797            cases (member (BitVector 8) ? (\fst ?) ?)
1798            [1: #destr normalize in destr; destruct(destr)
1799            |2:
1800            ]
1801        ]
1802    |3: >get_index_v_eq in ⊢ (??%?)
1803        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1804        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1805        <arg_nu_nl_eq
1806        whd in hyp:(??%?)
1807        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1808        normalize nodelta [*: #ignore @sym_eq ]
1809    ]
1810  |
1811  ].
1812*)
1813(*
1814map_address0 ... (DIRECT arg) = Some .. →
1815  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1816  get_arg_8 (internal_ram ...) (DIRECT arg)
1817
1818((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1819                     then Some internal_pseudo_address_map M 
1820                     else None internal_pseudo_address_map )
1821                    =Some internal_pseudo_address_map M')
1822
1823axiom low_internal_ram_write_at_stack_pointer:
1824 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1825 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1826  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1827  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1828  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1829  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1830  bu@@bl = sigma (pbu@@pbl) →
1831   low_internal_ram T1 cm1
1832     (write_at_stack_pointer …
1833       (set_8051_sfr …
1834         (write_at_stack_pointer …
1835           (set_8051_sfr …
1836             (set_low_internal_ram … s1
1837               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1838             SFR_SP sp1)
1839          bl)
1840        SFR_SP sp2)
1841      bu)
1842   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1843      (low_internal_ram …
1844       (write_at_stack_pointer …
1845         (set_8051_sfr …
1846           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1847          SFR_SP sp2)
1848        pbu)).
1849
1850lemma high_internal_ram_write_at_stack_pointer:
1851 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1852 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1853  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1854  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1855  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1856  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1857  bu@@bl = sigma (pbu@@pbl) →
1858   high_internal_ram T1 cm1
1859     (write_at_stack_pointer …
1860       (set_8051_sfr …
1861         (write_at_stack_pointer …
1862           (set_8051_sfr …
1863             (set_high_internal_ram … s1
1864               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1865             SFR_SP sp1)
1866          bl)
1867        SFR_SP sp2)
1868      bu)
1869   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1870      (high_internal_ram …
1871       (write_at_stack_pointer …
1872         (set_8051_sfr …
1873           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1874          SFR_SP sp2)
1875        pbu)).
1876  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1877  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1878  cases daemon (* XXX: !!! *)
1879qed.
1880*)
1881
1882lemma Some_Some_elim:
1883 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
1884 #T #x #y #P #H #K @H @option_destruct_Some //
1885qed.
1886
1887lemma pair_destruct_right:
1888  ∀A: Type[0].
1889  ∀B: Type[0].
1890  ∀a, c: A.
1891  ∀b, d: B.
1892    〈a, b〉 = 〈c, d〉 → b = d.
1893  #A #B #a #b #c #d //
1894qed.
1895   
1896(*CSC: ???*)
1897(* XXX: we need a precondition here stating that the PPC is within the
1898        bounds of the instruction list in order for Jaap's specification to
1899        apply.
1900*)
1901lemma snd_assembly_1_pseudoinstruction_ok:
1902  ∀program: pseudo_assembly_program.
1903  ∀program_length_proof: |\snd program| ≤ 2^16.
1904  ∀sigma: Word → Word.
1905  ∀policy: Word → bool.
1906  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1907  ∀ppc: Word.
1908  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1909  ∀pi.
1910  ∀lookup_labels.
1911  ∀lookup_datalabels.
1912    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
1913    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1914    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1915    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1916      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1917  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1918  #lookup_labels #lookup_datalabels
1919  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1920  normalize nodelta
1921  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1922  #fetch_pseudo_refl
1923  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1924  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1925  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1926  @pair_elim #preamble #instr_list #program_refl
1927  @pair_elim #labels #costs' #create_label_cost_map_refl
1928  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1929  lapply (H ppc ppc_in_bounds) -H
1930  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1931  @pair_elim #len #assembled #assembly1_refl #H
1932  cases H
1933  #encoding_check_assm #sigma_newppc_refl
1934  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1935  >pi_refl' in assembly1_refl; #assembly1_refl
1936  >lookup_labels_refl >lookup_datalabels_refl
1937  >program_refl normalize nodelta
1938  >assembly1_refl
1939  <sigma_newppc_refl
1940  generalize in match fetch_pseudo_refl';
1941  whd in match (fetch_pseudo_instruction ???);
1942  @pair_elim #lbl #instr #nth_refl normalize nodelta
1943  #G cases (pair_destruct_right ?????? G) %
1944qed.
1945
1946lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
1947  /2/
1948qed.
1949
1950(* To be moved in ProofStatus *)
1951lemma program_counter_set_program_counter:
1952  ∀T.
1953  ∀cm.
1954  ∀s.
1955  ∀x.
1956    program_counter T cm (set_program_counter T cm s x) = x.
1957  //
1958qed.
1959
1960(* XXX: easy but tedious *)
1961lemma assembly1_lt_128:
1962  ∀i: instruction.
1963    |(assembly1 i)| < 128.
1964  #i cases i
1965  try (#assm1 #assm2) try #assm1
1966  [8:
1967    cases assm1
1968    try (#assm1 #assm2) try #assm1
1969    whd in match assembly1; normalize nodelta
1970    whd in match assembly_preinstruction; normalize nodelta
1971    try @(subaddressing_mode_elim … assm2)
1972    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
1973    [32:
1974      cases assm1 -assm1 #assm1 normalize nodelta
1975      cases assm1 #addr1 #addr2 normalize nodelta
1976      [1:
1977        @(subaddressing_mode_elim … addr2)
1978      |2:
1979        @(subaddressing_mode_elim … addr1)
1980      ]
1981      #w
1982    |35,36,37:
1983      cases assm1 -assm1 #assm1 normalize nodelta
1984      [1,3:
1985        cases assm1 -assm1 #assm1 normalize nodelta
1986      ]
1987      cases assm1 #addr1 #addr2 normalize nodelta
1988      @(subaddressing_mode_elim … addr2) try #w
1989    |49:
1990      cases assm1 -assm1 #assm1 normalize nodelta
1991      [1:
1992        cases assm1 -assm1 #assm1 normalize nodelta
1993        [1:
1994          cases assm1 -assm1 #assm1 normalize nodelta
1995          [1:
1996            cases assm1 -assm1 #assm1 normalize nodelta
1997            [1:
1998              cases assm1 -assm1 #assm1 normalize nodelta
1999            ]
2000          ]
2001        ]
2002      ]
2003      cases assm1 #addr1 #addr2 normalize nodelta
2004      [1,3,4,5:
2005        @(subaddressing_mode_elim … addr2) try #w
2006      |*:
2007        @(subaddressing_mode_elim … addr1) try #w
2008        normalize nodelta
2009        [1,2:
2010          @(subaddressing_mode_elim … addr2) try #w
2011        ]
2012      ]
2013    |50:
2014      cases assm1 -assm1 #assm1 normalize nodelta
2015      cases assm1 #addr1 #addr2 normalize nodelta
2016      [1:
2017        @(subaddressing_mode_elim … addr2) try #w
2018      |2:
2019        @(subaddressing_mode_elim … addr1) try #w
2020      ]
2021    ]
2022    normalize repeat @le_S_S @le_O_n
2023  ]
2024  whd in match assembly1; normalize nodelta
2025  [6:
2026    normalize repeat @le_S_S @le_O_n
2027  |7:
2028    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
2029  |*:
2030    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
2031  ]
2032qed.
Note: See TracBrowser for help on using the repository browser.