source: src/ASM/AssemblyProof.ma @ 2113

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

Proof by cases repaired; dead code removed.

File size: 64.6 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(* OLD?
1213definition assembly_specification:
1214  ∀assembly_program: pseudo_assembly_program.
1215  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1216  λpseudo_assembly_program.
1217  λcode_mem.
1218    ∀pc: Word.
1219      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1220      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1221      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1222      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1223      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1224       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1225      match pre_assembled with
1226       [ None ⇒ True
1227       | Some pc_code ⇒
1228          let 〈new_pc,code〉 ≝ pc_code in
1229           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1230
1231axiom assembly_meets_specification:
1232  ∀pseudo_assembly_program.
1233    match assembly pseudo_assembly_program with
1234    [ None ⇒ True
1235    | Some code_mem_cost ⇒
1236      let 〈code_mem, cost〉 ≝ code_mem_cost in
1237        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1238    ].
1239(*
1240  # PROGRAM
1241  [ cases PROGRAM
1242    # PREAMBLE
1243    # INSTR_LIST
1244    elim INSTR_LIST
1245    [ whd
1246      whd in ⊢ (∀_. %)
1247      # PC
1248      whd
1249    | # INSTR
1250      # INSTR_LIST_TL
1251      # H
1252      whd
1253      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1254    ]
1255  | cases not_implemented
1256  ] *)
1257*)
1258
1259(* XXX: changed this type.  Bool specifies whether byte is first or second
1260        component of an address, and the Word is the pseudoaddress that it
1261        corresponds to.  Second component is the same principle for the accumulator
1262        A.
1263*)
1264definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
1265
1266include alias "ASM/BitVectorTrie.ma".
1267 
1268include "common/AssocList.ma".
1269
1270axiom low_internal_ram_of_pseudo_low_internal_ram:
1271 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1272
1273axiom high_internal_ram_of_pseudo_high_internal_ram:
1274 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1275
1276axiom low_internal_ram_of_pseudo_internal_ram_hit:
1277 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
1278  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
1279   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1280   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
1281   let bl ≝ lookup ? 7 addr ram (zero 8) in
1282   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
1283   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
1284     if high then
1285       (pbl = higher) ∧ (bl = phigher)
1286     else
1287       (pbl = lower) ∧ (bl = plower).
1288
1289(* changed from add to sub *)
1290axiom low_internal_ram_of_pseudo_internal_ram_miss:
1291 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
1292  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1293    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
1294      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1295
1296definition addressing_mode_ok ≝
1297 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
1298  λaddr:addressing_mode.
1299   match addr with
1300    [ DIRECT d ⇒
1301       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1302       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1303    | INDIRECT i ⇒
1304       let d ≝ get_register … s [[false;false;i]] in
1305       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
1306       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
1307    | EXT_INDIRECT _ ⇒ true
1308    | REGISTER _ ⇒ true
1309    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
1310    | ACC_B ⇒ true
1311    | DPTR ⇒ true
1312    | DATA _ ⇒ true
1313    | DATA16 _ ⇒ true
1314    | ACC_DPTR ⇒ true
1315    | ACC_PC ⇒ true
1316    | EXT_INDIRECT_DPTR ⇒ true
1317    | INDIRECT_DPTR ⇒ true
1318    | CARRY ⇒ true
1319    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1320    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1321    | RELATIVE _ ⇒ true
1322    | ADDR11 _ ⇒ true
1323    | ADDR16 _ ⇒ true ].
1324   
1325definition next_internal_pseudo_address_map0 ≝
1326  λT.
1327  λcm:T.
1328  λaddr_of: Identifier → PreStatus T cm → Word.
1329  λfetched.
1330  λM: internal_pseudo_address_map.
1331  λs: PreStatus T cm.
1332   match fetched with
1333    [ Comment _ ⇒ Some ? M
1334    | Cost _ ⇒ Some … M
1335    | Jmp _ ⇒ Some … M
1336    | Call a ⇒
1337      let a' ≝ addr_of a s in
1338      let 〈callM, accM〉 ≝ M in
1339         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
1340                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
1341    | Mov _ _ ⇒ Some … M
1342    | Instruction instr ⇒
1343       match instr with
1344        [ ADD addr1 addr2 ⇒
1345           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1346            Some ? M
1347           else
1348            None ?
1349        | ADDC addr1 addr2 ⇒
1350           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1351            Some ? M
1352           else
1353            None ?
1354        | SUBB addr1 addr2 ⇒
1355           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
1356            Some ? M
1357           else
1358            None ?       
1359        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1360
1361definition next_internal_pseudo_address_map ≝
1362 λM:internal_pseudo_address_map.
1363 λcm.
1364 λaddr_of.
1365 λs:PseudoStatus cm.
1366 λppc_ok.
1367    next_internal_pseudo_address_map0 ? cm addr_of
1368     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
1369
1370definition code_memory_of_pseudo_assembly_program:
1371    ∀pap:pseudo_assembly_program.
1372      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
1373  λpap.
1374  λsigma.
1375  λpolicy.
1376    let p ≝ pi1 … (assembly pap sigma policy) in
1377      load_code_memory (\fst p).
1378
1379definition sfr_8051_of_pseudo_sfr_8051 ≝
1380  λM: internal_pseudo_address_map.
1381  λsfrs: Vector Byte 19.
1382  λsigma: Word → Word.
1383    match \snd M with
1384    [ None ⇒ sfrs
1385    | Some s ⇒
1386      let 〈high, address〉 ≝ s in
1387      let index ≝ sfr_8051_index SFR_ACC_A in
1388      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
1389        if high then
1390          set_index Byte 19 sfrs index upper ?
1391        else
1392          set_index Byte 19 sfrs index lower ?
1393    ].
1394  //
1395qed.
1396
1397definition status_of_pseudo_status:
1398    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
1399      ∀sigma: Word → Word. ∀policy: Word → bool.
1400        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
1401  λM.
1402  λpap.
1403  λps.
1404  λsigma.
1405  λpolicy.
1406  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
1407  let pc ≝ sigma (program_counter … ps) in
1408  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1409  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1410     mk_PreStatus (BitVectorTrie Byte 16)
1411      cm
1412      lir
1413      hir
1414      (external_ram … ps)
1415      pc
1416      (special_function_registers_8051 … ps)
1417      (special_function_registers_8052 … ps)
1418      (p1_latch … ps)
1419      (p3_latch … ps)
1420      (clock … ps).
1421
1422(*
1423definition write_at_stack_pointer':
1424 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1425  λM: Type[0].
1426  λs: PreStatus M.
1427  λv: Byte.
1428    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
1429    let bit_zero ≝ get_index_v… nu O ? in
1430    let bit_1 ≝ get_index_v… nu 1 ? in
1431    let bit_2 ≝ get_index_v… nu 2 ? in
1432    let bit_3 ≝ get_index_v… nu 3 ? in
1433      if bit_zero then
1434        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1435                              v (low_internal_ram ? s) in
1436          set_low_internal_ram ? s memory
1437      else
1438        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1439                              v (high_internal_ram ? s) in
1440          set_high_internal_ram ? s memory.
1441  [ cases l0 %
1442  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1443qed.
1444
1445definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1446 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1447
1448  λticks_of.
1449  λs.
1450  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1451  let ticks ≝ ticks_of (program_counter ? s) in
1452  let s ≝ set_clock ? s (clock ? s + ticks) in
1453  let s ≝ set_program_counter ? s pc in
1454    match instr with
1455    [ Instruction instr ⇒
1456       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1457    | Comment cmt ⇒ s
1458    | Cost cst ⇒ s
1459    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1460    | Call call ⇒
1461      let a ≝ address_of_word_labels s call in
1462      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1463      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1464      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
1465      let s ≝ write_at_stack_pointer' ? s pc_bl in
1466      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1467      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1468      let s ≝ write_at_stack_pointer' ? s pc_bu in
1469        set_program_counter ? s a
1470    | Mov dptr ident ⇒
1471       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1472    ].
1473 [
1474 |2,3,4: %
1475 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1476 |
1477 | %
1478 ]
1479 cases not_implemented
1480qed.
1481*)
1482
1483(*
1484lemma execute_code_memory_unchanged:
1485 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1486 #ticks #ps whd in ⊢ (??? (??%))
1487 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1488  (program_counter pseudo_assembly_program ps)) #instr #pc
1489 whd in ⊢ (??? (??%)) cases instr
1490  [ #pre cases pre
1491     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1492       cases (vsplit ????) #z1 #z2 %
1493     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1494       cases (vsplit ????) #z1 #z2 %
1495     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1496       cases (vsplit ????) #z1 #z2 %
1497     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1498       [ #x1 whd in ⊢ (??? (??%))
1499     | *: cases not_implemented
1500     ]
1501  | #comment %
1502  | #cost %
1503  | #label %
1504  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1505    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1506    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
1507    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1508    (* CSC: ??? *)
1509  | #dptr #label (* CSC: ??? *)
1510  ]
1511  cases not_implemented
1512qed.
1513*)
1514
1515(* DEAD CODE?
1516lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1517 ∀M:internal_pseudo_address_map.
1518 ∀ps,ps': PseudoStatus.
1519 ∀pol.
1520  ∀prf:code_memory … ps = code_memory … ps'.
1521   let pol' ≝ ? in
1522   match status_of_pseudo_status M ps pol with
1523    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
1524    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
1525    ].
1526 [2: <prf @pol]
1527 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1528 generalize in match (refl … (assembly (code_memory … ps) pol))
1529 cases (assembly ??) in ⊢ (???% → %)
1530  [ #K whd whd in ⊢ (??%?) <H >K %
1531  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1532qed.
1533*)
1534
1535definition ticks_of0:
1536    ∀p:pseudo_assembly_program.
1537      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
1538  λprogram: pseudo_assembly_program.
1539  λsigma.
1540  λpolicy.
1541  λppc: Word.
1542  λfetched.
1543    match fetched with
1544    [ Instruction instr ⇒
1545      match instr with
1546      [ JC lbl ⇒ ? (*
1547        match pol lookup_labels ppc with
1548        [ short_jump ⇒ 〈2, 2〉
1549        | absolute_jump ⇒ ?
1550        | long_jump ⇒ 〈4, 4〉
1551        ] *)
1552      | JNC lbl ⇒ ? (*
1553        match pol lookup_labels ppc with
1554        [ short_jump ⇒ 〈2, 2〉
1555        | absolute_jump ⇒ ?
1556        | long_jump ⇒ 〈4, 4〉
1557        ] *)
1558      | JB bit lbl ⇒ ? (*
1559        match pol lookup_labels ppc with
1560        [ short_jump ⇒ 〈2, 2〉
1561        | absolute_jump ⇒ ?
1562        | long_jump ⇒ 〈4, 4〉
1563        ] *)
1564      | JNB bit lbl ⇒ ? (*
1565        match pol lookup_labels ppc with
1566        [ short_jump ⇒ 〈2, 2〉
1567        | absolute_jump ⇒ ?
1568        | long_jump ⇒ 〈4, 4〉
1569        ] *)
1570      | JBC bit lbl ⇒ ? (*
1571        match pol lookup_labels ppc with
1572        [ short_jump ⇒ 〈2, 2〉
1573        | absolute_jump ⇒ ?
1574        | long_jump ⇒ 〈4, 4〉
1575        ] *)
1576      | JZ lbl ⇒ ? (*
1577        match pol lookup_labels ppc with
1578        [ short_jump ⇒ 〈2, 2〉
1579        | absolute_jump ⇒ ?
1580        | long_jump ⇒ 〈4, 4〉
1581        ] *)
1582      | JNZ lbl ⇒ ? (*
1583        match pol lookup_labels  ppc with
1584        [ short_jump ⇒ 〈2, 2〉
1585        | absolute_jump ⇒ ?
1586        | long_jump ⇒ 〈4, 4〉
1587        ] *)
1588      | CJNE arg lbl ⇒ ? (*
1589        match pol lookup_labels ppc with
1590        [ short_jump ⇒ 〈2, 2〉
1591        | absolute_jump ⇒ ?
1592        | long_jump ⇒ 〈4, 4〉
1593        ] *)
1594      | DJNZ arg lbl ⇒ ? (*
1595        match pol lookup_labels ppc with
1596        [ short_jump ⇒ 〈2, 2〉
1597        | absolute_jump ⇒ ?
1598        | long_jump ⇒ 〈4, 4〉
1599        ] *)
1600      | ADD arg1 arg2 ⇒
1601        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1602         〈ticks, ticks〉
1603      | ADDC arg1 arg2 ⇒
1604        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1605         〈ticks, ticks〉
1606      | SUBB arg1 arg2 ⇒
1607        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1608         〈ticks, ticks〉
1609      | INC arg ⇒
1610        let ticks ≝ ticks_of_instruction (INC ? arg) in
1611         〈ticks, ticks〉
1612      | DEC arg ⇒
1613        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1614         〈ticks, ticks〉
1615      | MUL arg1 arg2 ⇒
1616        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1617         〈ticks, ticks〉
1618      | DIV arg1 arg2 ⇒
1619        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1620         〈ticks, ticks〉
1621      | DA arg ⇒
1622        let ticks ≝ ticks_of_instruction (DA ? arg) in
1623         〈ticks, ticks〉
1624      | ANL arg ⇒
1625        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1626         〈ticks, ticks〉
1627      | ORL arg ⇒
1628        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1629         〈ticks, ticks〉
1630      | XRL arg ⇒
1631        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1632         〈ticks, ticks〉
1633      | CLR arg ⇒
1634        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1635         〈ticks, ticks〉
1636      | CPL arg ⇒
1637        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1638         〈ticks, ticks〉
1639      | RL arg ⇒
1640        let ticks ≝ ticks_of_instruction (RL ? arg) in
1641         〈ticks, ticks〉
1642      | RLC arg ⇒
1643        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1644         〈ticks, ticks〉
1645      | RR arg ⇒
1646        let ticks ≝ ticks_of_instruction (RR ? arg) in
1647         〈ticks, ticks〉
1648      | RRC arg ⇒
1649        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1650         〈ticks, ticks〉
1651      | SWAP arg ⇒
1652        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1653         〈ticks, ticks〉
1654      | MOV arg ⇒
1655        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1656         〈ticks, ticks〉
1657      | MOVX arg ⇒
1658        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1659         〈ticks, ticks〉
1660      | SETB arg ⇒
1661        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1662         〈ticks, ticks〉
1663      | PUSH arg ⇒
1664        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1665         〈ticks, ticks〉
1666      | POP arg ⇒
1667        let ticks ≝ ticks_of_instruction (POP ? arg) in
1668         〈ticks, ticks〉
1669      | XCH arg1 arg2 ⇒
1670        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1671         〈ticks, ticks〉
1672      | XCHD arg1 arg2 ⇒
1673        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1674         〈ticks, ticks〉
1675      | RET ⇒
1676        let ticks ≝ ticks_of_instruction (RET ?) in
1677         〈ticks, ticks〉
1678      | RETI ⇒
1679        let ticks ≝ ticks_of_instruction (RETI ?) in
1680         〈ticks, ticks〉
1681      | NOP ⇒
1682        let ticks ≝ ticks_of_instruction (NOP ?) in
1683         〈ticks, ticks〉
1684      ]
1685    | Comment comment ⇒ 〈0, 0〉
1686    | Cost cost ⇒ 〈0, 0〉
1687    | Jmp jmp ⇒ 〈2, 2〉
1688    | Call call ⇒ 〈2, 2〉
1689    | Mov dptr tgt ⇒ 〈2, 2〉
1690    ].
1691    cases daemon
1692qed.
1693
1694definition ticks_of:
1695    ∀p:pseudo_assembly_program.
1696      (Word → Word) → (Word → bool) → ∀ppc:Word.
1697       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
1698  λprogram: pseudo_assembly_program.
1699  λsigma.
1700  λpolicy.
1701  λppc: Word. λppc_ok.
1702    let pseudo ≝ \snd program in
1703    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
1704     ticks_of0 program sigma policy ppc fetched.
1705
1706lemma eq_rect_Type1_r:
1707  ∀A: Type[1].
1708  ∀a: A.
1709  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1710  #A #a #P #H #x #p
1711  generalize in match H;
1712  generalize in match P;
1713  cases p //
1714qed.
1715
1716axiom vsplit_append:
1717  ∀A: Type[0].
1718  ∀m, n: nat.
1719  ∀v, v': Vector A m.
1720  ∀q, q': Vector A n.
1721    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
1722      v = v' ∧ q = q'.
1723
1724lemma vsplit_vector_singleton:
1725  ∀A: Type[0].
1726  ∀n: nat.
1727  ∀v: Vector A (S n).
1728  ∀rest: Vector A n.
1729  ∀s: Vector A 1.
1730    v = s @@ rest →
1731    ((get_index_v A ? v 0 ?) ::: rest) = v.
1732  [1:
1733    #A #n #v cases daemon (* XXX: !!! *)
1734  |2:
1735    @le_S_S @le_O_n
1736  ]
1737qed.
1738
1739example sub_minus_one_seven_eight:
1740  ∀v: BitVector 7.
1741  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1742  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1743 cases daemon.
1744qed.
1745
1746(*
1747lemma blah:
1748  ∀m: internal_pseudo_address_map.
1749  ∀s: PseudoStatus.
1750  ∀arg: Byte.
1751  ∀b: bool.
1752    addressing_mode_ok m s (DIRECT arg) = true →
1753      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
1754      get_arg_8 ? s b (DIRECT arg).
1755  [2, 3: normalize % ]
1756  #m #s #arg #b #hyp
1757  whd in ⊢ (??%%)
1758  @vsplit_elim''
1759  #nu' #nl' #arg_nu_nl_eq
1760  normalize nodelta
1761  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
1762  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
1763  #get_index_v_eq
1764  normalize nodelta
1765  [2:
1766    normalize nodelta
1767    @vsplit_elim''
1768    #bit_one' #three_bits' #bit_one_three_bit_eq
1769    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
1770    normalize nodelta
1771    generalize in match (refl ? (sub_7_with_carry ? ? ?))
1772    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
1773    #Saddr #carr' #Saddr_carr_eq
1774    normalize nodelta
1775    #carr_hyp'
1776    @carr_hyp'
1777    [1:
1778    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
1779        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
1780        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
1781        #member_eq
1782        normalize nodelta
1783        [2: #destr destruct(destr)
1784        |1: -carr_hyp';
1785            >arg_nu_nl_eq
1786            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
1787            [1: >get_index_v_eq in ⊢ (??%? → ?)
1788            |2: @le_S @le_S @le_S @le_n
1789            ]
1790            cases (member (BitVector 8) ? (\fst ?) ?)
1791            [1: #destr normalize in destr; destruct(destr)
1792            |2:
1793            ]
1794        ]
1795    |3: >get_index_v_eq in ⊢ (??%?)
1796        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
1797        >(vsplit_vector_singleton … bit_one_three_bit_eq)
1798        <arg_nu_nl_eq
1799        whd in hyp:(??%?)
1800        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
1801        normalize nodelta [*: #ignore @sym_eq ]
1802    ]
1803  |
1804  ].
1805*)
1806(*
1807map_address0 ... (DIRECT arg) = Some .. →
1808  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
1809  get_arg_8 (internal_ram ...) (DIRECT arg)
1810
1811((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
1812                     then Some internal_pseudo_address_map M 
1813                     else None internal_pseudo_address_map )
1814                    =Some internal_pseudo_address_map M')
1815
1816axiom low_internal_ram_write_at_stack_pointer:
1817 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
1818 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1819  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1820  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
1821  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1822  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1823  bu@@bl = sigma (pbu@@pbl) →
1824   low_internal_ram T1 cm1
1825     (write_at_stack_pointer …
1826       (set_8051_sfr …
1827         (write_at_stack_pointer …
1828           (set_8051_sfr …
1829             (set_low_internal_ram … s1
1830               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
1831             SFR_SP sp1)
1832          bl)
1833        SFR_SP sp2)
1834      bu)
1835   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
1836      (low_internal_ram …
1837       (write_at_stack_pointer …
1838         (set_8051_sfr …
1839           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1840          SFR_SP sp2)
1841        pbu)).
1842
1843lemma high_internal_ram_write_at_stack_pointer:
1844 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
1845 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
1846  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
1847  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
1848  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
1849  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
1850  bu@@bl = sigma (pbu@@pbl) →
1851   high_internal_ram T1 cm1
1852     (write_at_stack_pointer …
1853       (set_8051_sfr …
1854         (write_at_stack_pointer …
1855           (set_8051_sfr …
1856             (set_high_internal_ram … s1
1857               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
1858             SFR_SP sp1)
1859          bl)
1860        SFR_SP sp2)
1861      bu)
1862   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
1863      (high_internal_ram …
1864       (write_at_stack_pointer …
1865         (set_8051_sfr …
1866           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
1867          SFR_SP sp2)
1868        pbu)).
1869  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
1870  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
1871  cases daemon (* XXX: !!! *)
1872qed.
1873*)
1874
1875lemma Some_Some_elim:
1876 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
1877 #T #x #y #P #H #K @H @option_destruct_Some //
1878qed.
1879
1880lemma pair_destruct_right:
1881  ∀A: Type[0].
1882  ∀B: Type[0].
1883  ∀a, c: A.
1884  ∀b, d: B.
1885    〈a, b〉 = 〈c, d〉 → b = d.
1886  #A #B #a #b #c #d //
1887qed.
1888   
1889(*CSC: ???*)
1890(* XXX: we need a precondition here stating that the PPC is within the
1891        bounds of the instruction list in order for Jaap's specification to
1892        apply.
1893*)
1894lemma snd_assembly_1_pseudoinstruction_ok:
1895  ∀program: pseudo_assembly_program.
1896  ∀program_length_proof: |\snd program| ≤ 2^16.
1897  ∀sigma: Word → Word.
1898  ∀policy: Word → bool.
1899  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
1900  ∀ppc: Word.
1901  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
1902  ∀pi.
1903  ∀lookup_labels.
1904  ∀lookup_datalabels.
1905    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
1906    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
1907    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
1908    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
1909      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
1910  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
1911  #lookup_labels #lookup_datalabels
1912  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
1913  normalize nodelta
1914  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
1915  #fetch_pseudo_refl
1916  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
1917  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
1918  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
1919  @pair_elim #preamble #instr_list #program_refl
1920  @pair_elim #labels #costs' #create_label_cost_map_refl
1921  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
1922  lapply (H ppc ppc_in_bounds) -H
1923  @pair_elim #pi' #newppc #fetch_pseudo_refl'
1924  @pair_elim #len #assembled #assembly1_refl #H
1925  cases H
1926  #encoding_check_assm #sigma_newppc_refl
1927  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
1928  >pi_refl' in assembly1_refl; #assembly1_refl
1929  >lookup_labels_refl >lookup_datalabels_refl
1930  >program_refl normalize nodelta
1931  >assembly1_refl
1932  <sigma_newppc_refl
1933  generalize in match fetch_pseudo_refl';
1934  whd in match (fetch_pseudo_instruction ???);
1935  @pair_elim #lbl #instr #nth_refl normalize nodelta
1936  #G cases (pair_destruct_right ?????? G) %
1937qed.
1938
1939lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
1940  /2/
1941qed.
1942
1943(* To be moved in ProofStatus *)
1944lemma program_counter_set_program_counter:
1945  ∀T.
1946  ∀cm.
1947  ∀s.
1948  ∀x.
1949    program_counter T cm (set_program_counter T cm s x) = x.
1950  //
1951qed.
1952
1953(* XXX: easy but tedious *)
1954lemma assembly1_lt_128:
1955  ∀i: instruction.
1956    |(assembly1 i)| < 128.
1957  #i cases i
1958  try (#assm1 #assm2) try #assm1
1959  [8:
1960    cases assm1
1961    try (#assm1 #assm2) try #assm1
1962    whd in match assembly1; normalize nodelta
1963    whd in match assembly_preinstruction; normalize nodelta
1964    try @(subaddressing_mode_elim … assm2)
1965    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
1966    [32:
1967      cases assm1 -assm1 #assm1 normalize nodelta
1968      cases assm1 #addr1 #addr2 normalize nodelta
1969      [1:
1970        @(subaddressing_mode_elim … addr2)
1971      |2:
1972        @(subaddressing_mode_elim … addr1)
1973      ]
1974      #w
1975    |35,36,37:
1976      cases assm1 -assm1 #assm1 normalize nodelta
1977      [1,3:
1978        cases assm1 -assm1 #assm1 normalize nodelta
1979      ]
1980      cases assm1 #addr1 #addr2 normalize nodelta
1981      @(subaddressing_mode_elim … addr2) try #w
1982    |49:
1983      cases assm1 -assm1 #assm1 normalize nodelta
1984      [1:
1985        cases assm1 -assm1 #assm1 normalize nodelta
1986        [1:
1987          cases assm1 -assm1 #assm1 normalize nodelta
1988          [1:
1989            cases assm1 -assm1 #assm1 normalize nodelta
1990            [1:
1991              cases assm1 -assm1 #assm1 normalize nodelta
1992            ]
1993          ]
1994        ]
1995      ]
1996      cases assm1 #addr1 #addr2 normalize nodelta
1997      [1,3,4,5:
1998        @(subaddressing_mode_elim … addr2) try #w
1999      |*:
2000        @(subaddressing_mode_elim … addr1) try #w
2001        normalize nodelta
2002        [1,2:
2003          @(subaddressing_mode_elim … addr2) try #w
2004        ]
2005      ]
2006    |50:
2007      cases assm1 -assm1 #assm1 normalize nodelta
2008      cases assm1 #addr1 #addr2 normalize nodelta
2009      [1:
2010        @(subaddressing_mode_elim … addr2) try #w
2011      |2:
2012        @(subaddressing_mode_elim … addr1) try #w
2013      ]
2014    ]
2015    normalize repeat @le_S_S @le_O_n
2016  ]
2017  whd in match assembly1; normalize nodelta
2018  [6:
2019    normalize repeat @le_S_S @le_O_n
2020  |7:
2021    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
2022  |*:
2023    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
2024  ]
2025qed.
Note: See TracBrowser for help on using the repository browser.