source: src/ASM/AssemblyProof.ma @ 2121

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

More functions moved to the places they belong to

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