source:src/ASM/AssemblyProof.ma@936

Last change on this file since 936 was 936, checked in by sacerdot, 10 years ago

Ticks are now handled correctly everywhere and the main proof takes care of
them.

File size: 68.9 KB
Line
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4(* RUSSEL **)
5
6include "basics/jmeq.ma".
7
8notation > "hvbox(a break ≃ b)"
9  non associative with precedence 45
10for @{ 'jmeq ? \$a ? \$b }.
11
12notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
13  non associative with precedence 45
14for @{ 'jmeq \$t \$a \$u \$b }.
15
16interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
17
18lemma eq_to_jmeq:
19  ∀A: Type[0].
20  ∀x, y: A.
21    x = y → x ≃ y.
22  //
23qed.
24
25definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
26definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
27
28coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
29coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
30
31axiom VOID: Type[0].
32axiom assert_false: VOID.
33definition bigbang: ∀A:Type[0].False → VOID → A.
34 #A #abs cases abs
35qed.
36
37coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
38
39lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
40 #A #P #p cases p #w #q @q
41qed.
42
43lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
44 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
45qed.
46
47coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
48
49(* END RUSSELL **)
50
51
52definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
53  λP.
54    P true ∧ P false.
55
56let rec bitvector_elim_prop_internal
57  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
58  match m return λm. m ≤ n → BitVector (n - m) → Prop with
59  [ O    ⇒ λprf1. λprefix. P ?
60  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
61  ].
62  [ applyS prefix
63  | letin res ≝ (bit ::: prefix)
64    < (minus_S_S ? ?)
65    > (minus_Sn_m ? ?)
66  [ @ res
67  | @ prf2
68  ]
69  | /2/
70  ].
71qed.
72
73definition bitvector_elim_prop ≝
74  λn: nat.
75  λP: BitVector n → Prop.
76    bitvector_elim_prop_internal n P n ? ?.
77  [ @ (le_n ?)
78  | < (minus_n_n ?)
79    @ [[ ]]
80  ]
81qed.
82
83lemma eq_b_eq:
84  ∀b, c.
85    eq_b b c = true → b = c.
86  #b #c
87  cases b
88  cases c
89  normalize //
90qed.
91
92lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
93 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
94 #n #hd #tl #abs @⊥ //
95qed.
96
97lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
98 ∃hd.∃tl.v ≃ VCons bool n hd tl.
99 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
100 [ #abs @⊥ //
101 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
102qed.
103
104lemma eq_bv_eq:
105  ∀n, v, q.
106    eq_bv n v q = true → v = q.
107  #n #v #q generalize in match v
108  elim q
109  [ #v #h @BitVector_O
110  | #n #hd #tl #ih #v' #h
111    cases (BitVector_Sn ? v')
112    #hd' * #tl' #jmeq >jmeq in h;
113    #new_h
114    change in new_h with ((andb ? ?) = ?);
115    cases(conjunction_true … new_h)
119    whd in eq_tails:(??(?????(%))?);
120    change in eq_tails with (eq_bv ??? = ?);
121    <(ih tl') //
122  ]
123qed.
124
125lemma bool_eq_internal_eq:
126  ∀b, c.
127    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
128  #b #c
129  cases b
130  [ normalize //
131  | normalize
132    cases c
133    [ normalize //
134    | normalize //
135    ]
136  ]
137qed.
138
139lemma eq_bv_refl:
140  ∀n,v. eq_bv n v v = true.
141  #n #v
142  elim v
143  [ //
144  | #n #hd #tl #ih
145    normalize
146    cases hd
147    [ normalize
148      @ ih
149    | normalize
150      @ ih
151    ]
152  ]
153qed.
154
155lemma eq_eq_bv:
156  ∀n, v, q.
157    v = q → eq_bv n v q = true.
158  #n #v
159  elim v
160  [ #q #h <h normalize %
161  | #n #hd #tl #ih #q #h >h //
162  ]
163qed.
164
165let rec foldl_strong_internal
166  (A: Type[0]) (P: list A → Type[0]) (l: list A)
167  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
168  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
169    l = prefix @ suffix → P(prefix @ suffix) ≝
170  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
171  [ nil ⇒ λprf. ?
172  | cons hd tl ⇒ λprf. ?
173  ].
174  [ > (append_nil ?)
175    @ acc
176  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
177    [ @ (H prefix hd tl prf acc)
178    | applyS prf
179    ]
180  ]
181qed.
182
183definition foldl_strong ≝
184  λA: Type[0].
185  λP: list A → Type[0].
186  λl: list A.
187  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
188  λacc: P [ ].
189    foldl_strong_internal A P l H [ ] l acc (refl …).
190
191definition bit_elim: ∀P: bool → bool. bool ≝
192  λP.
193    P true ∧ P false.
194
195let rec bitvector_elim_internal
196  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
197  match m return λm. m ≤ n → BitVector (n - m) → bool with
198  [ O    ⇒ λprf1. λprefix. P ?
199  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
200  ].
201  [ applyS prefix
202  | letin res ≝ (bit ::: prefix)
203    < (minus_S_S ? ?)
204    > (minus_Sn_m ? ?)
205    [ @ res
206    | @ prf2
207    ]
208  | /2/
209  ].
210qed.
211
212definition bitvector_elim ≝
213  λn: nat.
214  λP: BitVector n → bool.
215    bitvector_elim_internal n P n ? ?.
216  [ @ (le_n ?)
217  | < (minus_n_n ?)
218    @ [[ ]]
219  ]
220qed.
221
222axiom vector_associative_append:
223  ∀A: Type[0].
224  ∀n, m, o:  nat.
225  ∀v: Vector A n.
226  ∀q: Vector A m.
227  ∀r: Vector A o.
228    ((v @@ q) @@ r)
229    ≃
230    (v @@ (q @@ r)).
231
232lemma vector_cons_append:
233  ∀A: Type[0].
234  ∀n: nat.
235  ∀e: A.
236  ∀v: Vector A n.
237    e ::: v = [[ e ]] @@ v.
238  # A # N # E # V
239  elim V
240  [ normalize %
241  | # NN # AA # VV # IH
242    normalize
243    %
244  ]
245qed.
246
247lemma super_rewrite2:
248 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
249  ∀P: ∀m. Vector A m → Prop.
250   n=m → v1 ≃ v2 → P n v1 → P m v2.
251 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
252qed.
253
254lemma mem_middle_vector:
255  ∀A: Type[0].
256  ∀m, o: nat.
257  ∀eq: A → A → bool.
258  ∀reflex: ∀a. eq a a = true.
259  ∀p: Vector A m.
260  ∀a: A.
261  ∀r: Vector A o.
262    mem A eq ? (p@@(a:::r)) a = true.
263  # A # M # O # EQ # REFLEX # P # A
264  elim P
265  [ normalize
266    > (REFLEX A)
267    normalize
268    # H
269    %
270  | # NN # AA # PP # IH
271    normalize
272    cases (EQ A AA) //
273     @ IH
274  ]
275qed.
276
277lemma mem_monotonic_wrt_append:
278  ∀A: Type[0].
279  ∀m, o: nat.
280  ∀eq: A → A → bool.
281  ∀reflex: ∀a. eq a a = true.
282  ∀p: Vector A m.
283  ∀a: A.
284  ∀r: Vector A o.
285    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
286  # A # M # O # EQ # REFLEX # P # A
287  elim P
288  [ #R #H @H
289  | #NN #AA # PP # IH #R #H
290    normalize
291    cases (EQ A AA)
292    [ normalize %
293    | @ IH @ H
294    ]
295  ]
296qed.
297
298lemma subvector_multiple_append:
299  ∀A: Type[0].
300  ∀o, n: nat.
301  ∀eq: A → A → bool.
302  ∀refl: ∀a. eq a a = true.
303  ∀h: Vector A o.
304  ∀v: Vector A n.
305  ∀m: nat.
306  ∀q: Vector A m.
307    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
308  # A # O # N # EQ # REFLEX # H # V
309  elim V
310  [ normalize
311    # M # V %
312  | # NN # AA # VV # IH # MM # QQ
313    change with (bool_to_Prop (andb ??))
314    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
315    [
316    | # HH > HH
317      > (vector_cons_append ? ? AA VV)
318      change with (bool_to_Prop (subvector_with ??????))
319      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
320        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
321        ?
322        (vector_associative_append A ? ? ? QQ [[AA]] VV))
323      [ >associative_plus //
324      | @IH ]
325    ]
326    @(mem_monotonic_wrt_append)
327    [ @ REFLEX
328    | @(mem_monotonic_wrt_append)
329      [ @ REFLEX
330      | normalize
331        > REFLEX
332        normalize
333        %
334      ]
335    ]
336qed.
337
338lemma vector_cons_empty:
339  ∀A: Type[0].
340  ∀n: nat.
341  ∀v: Vector A n.
342    [[ ]] @@ v = v.
343  # A # N # V
344  elim V
345  [ normalize %
346  | # NN # HH # VV #H %
347  ]
348qed.
349
350corollary subvector_hd_tl:
351  ∀A: Type[0].
352  ∀o: nat.
353  ∀eq: A → A → bool.
354  ∀refl: ∀a. eq a a = true.
355  ∀h: A.
356  ∀v: Vector A o.
357    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
358  # A # O # EQ # REFLEX # H # V
359  > (vector_cons_append A ? H V)
360  < (vector_cons_empty A ? ([[H]] @@ V))
361  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
362qed.
363
364lemma eq_a_reflexive:
365  ∀a. eq_a a a = true.
366  # A
367  cases A
368  %
369qed.
370
371lemma is_in_monotonic_wrt_append:
372  ∀m, n: nat.
376    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
377  # M # N # P # Q # TO_SEARCH
378  # H
379  elim Q
380  [ normalize
381    @ H
382  | # NN # PP # QQ # IH
383    normalize
384    cases (is_a PP TO_SEARCH)
385    [ normalize
386      %
387    | normalize
388      normalize in IH
389      @ IH
390    ]
391  ]
392qed.
393
394corollary is_in_hd_tl:
397  ∀n: nat.
399    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
400  # TO_SEARCH # HD # N # V
401  elim V
402  [ # H
403    normalize in H;
404    cases H
405  | # NN # HHD # VV # IH # HH
406    > vector_cons_append
407    > (vector_cons_append ? ? HHD VV)
408    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
409    @ HH
410  ]
411qed.
412
414  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
415  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
416   (l → bool) → bool ] with
417  [ VEmpty      ⇒  true
418  | VCons len hd tl ⇒ λP.
419    let process_hd ≝
420      match hd return λhd. ∀P: hd:::tl → bool. bool with
421      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
422      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
423      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
424      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
425      | acc_a ⇒ λP.P ACC_A
426      | acc_b ⇒ λP.P ACC_B
427      | dptr ⇒ λP.P DPTR
428      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
429      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
430      | acc_dptr ⇒ λP.P ACC_DPTR
431      | acc_pc ⇒ λP.P ACC_PC
432      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
433      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
434      | carry ⇒ λP.P CARRY
437      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
440      ]
441    in
442      andb (process_hd P)
443       (match len return λx. x = len → bool with
444         [ O ⇒ λprf. true
445         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
446  ].
447  try %
448  [ 2: cases (sym_eq ??? prf); @tl
449  | generalize in match H; generalize in match tl; cases prf;
450    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
451    #tl
452    normalize in ⊢ (∀_: %. ?)
453    # H
454    whd
455    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
456    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
457qed.
458
459definition product_elim ≝
460  λm, n: nat.
461  λv: Vector addressing_mode_tag (S m).
462  λq: Vector addressing_mode_tag (S n).
463  λP: (v × q) → bool.
464    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
465
466definition union_elim ≝
467  λA, B: Type[0].
468  λelimA: (A → bool) → bool.
469  λelimB: (B → bool) → bool.
470  λelimU: A ⊎ B → bool.
471    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
472
473(*
474definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
475  λP.
478    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
479    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
480    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
483    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
486    P (DA ? ACC_A) ∧
487    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
488    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
489    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
490    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
491    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
492    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
493    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
494    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
495    P (RL ? ACC_A) ∧
496    P (RLC ? ACC_A) ∧
497    P (RR ? ACC_A) ∧
498    P (RRC ? ACC_A) ∧
499    P (SWAP ? ACC_A) ∧
500    P (RET ?) ∧
501    P (RETI ?) ∧
502    P (NOP ?) ∧
503    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
507    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
508                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
509                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
511    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
512                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
513                   (λd. P (XRL ? d)) ∧
514    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
515                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
517                   (λd. P (ANL ? d)) ∧
518    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
519                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
521                   (λd. P (ORL ? d)) ∧
522    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
523                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
524                   (λd. P (MOVX ? d)) ∧
525    union_elim ? ? (
526      union_elim ? ? (
527        union_elim ? ? (
528          union_elim ? ? (
529            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
530                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
531                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
532                            (product_elim ? ? [[dptr]] [[data16]]))
533                            (product_elim ? ? [[carry]] [[bit_addr]]))
534                            (product_elim ? ? [[bit_addr]] [[carry]])
535                            (λd. P (MOV ? d)).
536  %
537qed.
538
539definition instruction_elim: ∀P: instruction → bool. bool ≝
540  λP. (*
541    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
542    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
543    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
544    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
545    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
546    P (JMP INDIRECT_DPTR) ∧
547    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
548    preinstruction_elim (λp. P (RealInstruction p)). *)
549  %
550qed.
551
552
553axiom instruction_elim_complete:
554 ∀P. instruction_elim P = true → ∀i. P i = true.
555*)
556(*definition eq_instruction ≝
557  λi, j: instruction.
558    true.*)
559axiom eq_instruction: instruction → instruction → bool.
560axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
561
562let rec vect_member
563  (A: Type[0]) (n: nat) (eq: A → A → bool)
564  (v: Vector A n) (a: A) on v: bool ≝
565  match v with
566  [ VEmpty          ⇒ false
567  | VCons len hd tl ⇒
568    eq hd a ∨ (vect_member A ? eq tl a)
569  ].
570
572  (n: nat)
573  (l: Vector addressing_mode_tag (S n))
574  on l:
575  ∀P: l → Prop.
576  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
577  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
580  ∀x: l. P x ≝
581  match l return
582    λy.
583      match y with
584      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
585      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
586               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
587               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
588               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
589               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
590               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
591               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
592               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
593               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
594               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
595               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
596               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
597               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
598               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
599               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
602               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
605               ∀x:l. P x
606      ] with
607  [ VEmpty          ⇒ λAbsurd. ⊥
608  | VCons len hd tl ⇒ λProof. ?
609  ] (refl ? (S n)). cases daemon. qed. (*
610  [ destruct(Absurd)
611  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
612    # A8 # A9 # A10 # A11 # A12 # A13 # A14
613    # A15 # A16 # A17 # A18 # A19 # X
614    cases X
615    # SUB cases daemon ] qed.
616    cases SUB
617    [ # BYTE
618    normalize
619  ].
620
621
622(*    let prepare_hd ≝
623      match hd with
624      [ direct ⇒ λdirect_prf. ?
625      | indirect ⇒ λindirect_prf. ?
626      | ext_indirect ⇒ λext_indirect_prf. ?
627      | registr ⇒ λregistr_prf. ?
628      | acc_a ⇒ λacc_a_prf. ?
629      | acc_b ⇒ λacc_b_prf. ?
630      | dptr ⇒ λdptr_prf. ?
631      | data ⇒ λdata_prf. ?
632      | data16 ⇒ λdata16_prf. ?
633      | acc_dptr ⇒ λacc_dptr_prf. ?
634      | acc_pc ⇒ λacc_pc_prf. ?
635      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
636      | indirect_dptr ⇒ λindirect_prf. ?
637      | carry ⇒ λcarry_prf. ?
640      | relative ⇒ λrelative_prf. ?
643      ]
644    in ? *)
645  ].
646  [ 1: destruct(absd)
647  | 2: # A1 # A2 # A3 # A4 # A5 # A6
648       # A7 # A8 # A9 # A10 # A11 # A12
649       # A13 # A14 # A15 # A16 # A17 # A18
650       # A19 *
651  ].
652
653
654  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
655   (l → bool) → bool ] with
656  [ VEmpty      ⇒  true
657  | VCons len hd tl ⇒ λP.
658    let process_hd ≝
659      match hd return λhd. ∀P: hd:::tl → bool. bool with
660      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
661      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
662      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
663      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
664      | acc_a ⇒ λP.P ACC_A
665      | acc_b ⇒ λP.P ACC_B
666      | dptr ⇒ λP.P DPTR
667      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
668      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
669      | acc_dptr ⇒ λP.P ACC_DPTR
670      | acc_pc ⇒ λP.P ACC_PC
671      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
672      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
673      | carry ⇒ λP.P CARRY
676      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
679      ]
680    in
681      andb (process_hd P)
682       (match len return λx. x = len → bool with
683         [ O ⇒ λprf. true
684         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
685  ].
686  try %
687  [ 2: cases (sym_eq ??? prf); @tl
688  | generalize in match H; generalize in match tl; cases prf;
689    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
690    #tl
691    normalize in ⊢ (∀_: %. ?)
692    # H
693    whd
694    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
695    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
696qed.
697*)
698(*
699lemma test:
700  let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
701      (let assembled ≝ assembly1 i in
702      let code_memory ≝ load_code_memory assembled in
703      let fetched ≝ fetch code_memory ? in
704      let 〈instr_pc, ticks〉 ≝ fetched in
705        eq_instruction (\fst instr_pc)) i = true.
706 [2: @ zero
707 | normalize
708 ]*)
709
710lemma BitVectorTrie_O:
711 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
712 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
713  [ #w #_ %1 %[@w] %
714  | #n #l #r #abs @⊥ //
715  | #n #EQ %2 >EQ %]
716qed.
717
718lemma BitVectorTrie_Sn:
719 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
720 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
721  [ #m #abs @⊥ //
722  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
723  | #m #EQ %2 // ]
724qed.
725
726lemma lookup_prepare_trie_for_insertion_hit:
727 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
728  lookup … b (prepare_trie_for_insertion … b v) a = v.
729 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
730qed.
731
732lemma lookup_insert_hit:
733 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
734  lookup … b (insert … b v t) a = v.
735 #A #a #v #n #b elim b -b -n //
736 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
737  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
738  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
739qed.
740
741coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
742
743lemma lookup_prepare_trie_for_insertion_miss:
744 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
745  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
746 #A #a #v #n #c elim c
747  [ #b >(BitVector_O … b) normalize #abs @⊥ //
748  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
749    cases hd cases hd' normalize
750    [2,3: #_ cases tl' //
751    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
752qed.
753
754lemma lookup_insert_miss:
755 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
756  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
757 #A #a #v #n #c elim c -c -n
758  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
759  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
760    #t cases(BitVectorTrie_Sn … t)
761    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
762     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
763    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
764     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
765     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
766qed.
767
769 fold_left_i_aux … (
770   λi, mem, v.
771     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
772
773axiom split_elim:
774 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
775  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
776
778 ∀pc.
779 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
780
781(*
782axiom not_eqvb_S:
783 ∀pc.
784 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
785
786axiom not_eqvb_SS:
787 ∀pc.
788 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
789
790axiom bitvector_elim_complete:
791 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
792
793lemma bitvector_elim_complete':
794 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
795 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
796 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
797qed.
798*)
799
800
801
802
803(*
804lemma andb_elim':
805 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
806 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
807qed.
808*)
809
810let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
811                       (encoding: list Byte) on encoding: Prop ≝
812  match encoding with
813  [ nil ⇒ final_pc = pc
814  | cons hd tl ⇒
815    let 〈new_pc, byte〉 ≝ next code_memory pc in
816      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
817  ].
818
819lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
820 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
821  let intermediate_pc ≝ pc + length … l1 in
822   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
823    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
824 #code_memory #final_pc #l1 elim l1
825  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
826  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
827    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
828qed.
829
830axiom bitvector_3_elim_prop:
831 ∀P: BitVector 3 → Prop.
832  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
833  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
834  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
835
836definition ticks_of_instruction ≝
837 λi.
838  let trivial_code_memory ≝ assembly1 i in
839  let trivial_status ≝ load_code_memory trivial_code_memory in
840   \snd (fetch trivial_status (zero ?)).
841
842axiom fetch_assembly:
843  ∀pc,i,code_memory,assembled.
844    assembled = assembly1 i →
845      let len ≝ length … assembled in
846      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
847      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
848      let 〈instr_pc, ticks〉 ≝ fetched in
849      let 〈instr,pc'〉 ≝ instr_pc in
850       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
851(* #pc #i #code_memory #assembled cases i [8: *]
852 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
853 [47,48,49:
854 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
855  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
856   59,60,63,64,65,66,67: #ARG]]
857 [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,
858  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
859  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
860   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,
861   68,69,70,71: #ARG2]]
862 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
863 normalize in ⊢ (???% → ?)
864 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
865  normalize in ⊢ (???% → ?)]
866 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
867 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
868 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
869 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
870 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
871 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
872  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
873  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
874 whd >eq_instruction_refl >H4 @eq_bv_refl
875qed. *)
876
877let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
878 match expected with
879  [ nil ⇒ eq_bv … pc final_pc = true
880  | cons i tl ⇒
881     let fetched ≝ fetch code_memory pc in
882     let 〈instr_pc, ticks〉 ≝ fetched in
883     let 〈instr,pc'〉 ≝ instr_pc in
884      eq_instruction instr i = true ∧
885      ticks = (ticks_of_instruction i) ∧
886      fetch_many code_memory final_pc pc' tl].
887
888lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
889 #A #a #b #EQ destruct //
890qed.
891
892lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
893 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
894qed.
895
896axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
897
898axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
899
900lemma fetch_assembly_pseudo:
901 ∀program,ppc,lookup_labels,lookup_datalabels.
902  ∀pi,code_memory,len,assembled,instructions,pc.
903   let expansion ≝ jump_expansion ppc program in
904   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
905    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
906     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
907      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
908 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
909 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
910 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
911 >EQ2a >EQ2b -EQ2a EQ2b;
912  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
913  generalize in match pc elim instructions
914  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
915  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
916    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
917    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
918    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
919    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % //
920    [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ]
921qed.
922
923(* This establishes the correspondence between pseudo program counters and
924   program counters. It is at the heart of the proof. *)
925(*CSC: code taken from build_maps *)
926definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
927 λinstr_list.
928  foldl ??
929    (λt. λi.
930       match t with
931       [ None ⇒ None ?
932       | Some ppc_pc_map ⇒
933         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
934         let 〈program_counter, sigma_map〉 ≝ pc_map in
935         let 〈label, i〉 ≝ i in
936          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
937           [ None ⇒ None ?
938           | Some pc_ignore ⇒
939              let 〈pc,ignore〉 ≝ pc_ignore in
940              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
941       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
942
943definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
944 λinstr_list.
945  match sigma0 instr_list with
946   [ None ⇒ None …
947   | Some result ⇒
948      let 〈ppc,pc_sigma_map〉 ≝ result in
949       Some … pc_sigma_map ].
950
951definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
952 λinstr_list.
953  match sigma0 instr_list with
954  [ None ⇒ None ?
955  | Some result ⇒
956    let 〈ppc,pc_sigma_map〉 ≝ result in
957    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
958      if gtb pc (2^16) then
959        None ?
960      else
961        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
962
963axiom policy_ok: ∀p. sigma_safe p ≠ None ….
964
965definition sigma: pseudo_assembly_program → Word → Word ≝
966 λp.
967  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
968   [ None ⇒ λabs. ⊥
969   | Some r ⇒ λ_.r] (policy_ok p).
970 cases abs //
971qed.
972
973lemma length_append:
974 ∀A.∀l1,l2:list A.
975  |l1 @ l2| = |l1| + |l2|.
976 #A #l1 elim l1
977  [ //
978  | #hd #tl #IH #l2 normalize <IH //]
979qed.
980
981let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
982 match l with
983  [ nil ⇒ true
984  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
985
986lemma does_not_occur_None:
987 ∀id,i,list_instr.
988  does_not_occur id (list_instr@[〈None …,i〉]) =
989  does_not_occur id list_instr.
990 #id #i #list_instr elim list_instr
991  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
992qed.
993
994let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
995 match l with
996  [ nil ⇒ false
997  | cons hd tl ⇒
998     if instruction_matches_identifier id hd then
999      does_not_occur id tl
1000     else
1001      occurs_exactly_once id tl ].
1002
1003lemma occurs_exactly_once_None:
1004 ∀id,i,list_instr.
1005  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
1006  occurs_exactly_once id list_instr.
1007 #id #i #list_instr elim list_instr
1008  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
1009qed.
1010
1011lemma index_of_internal_None: ∀i,id,instr_list,n.
1012 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1013  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1014   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
1015 #i #id #instr_list elim instr_list
1016  [ #n #abs whd in abs; cases abs
1017  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
1018    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
1019    [ #H %
1020    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
1021      [ #_ % | #abs cases abs ]]]
1022qed.
1023
1025 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1028 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1029 >(index_of_internal_None … H) %
1030qed.
1031
1032axiom tech_pc_sigma0_append:
1033 ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'.
1034  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
1035   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
1036    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
1037
1038axiom tech_pc_sigma0_append_None:
1039 ∀preamble,instr_list,prefix,i,ppc,pc,costs.
1040  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
1041   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
1042    → False.
1043
1044(*
1045definition build_maps' ≝
1046  λpseudo_program.
1047  let 〈preamble,instr_list〉 ≝ pseudo_program in
1048  let result ≝
1049   foldl_strong
1050    (option Identifier × pseudo_instruction)
1051    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1052      let pre' ≝ 〈preamble,pre〉 in
1053      let 〈labels,pc_costs〉 ≝ res in
1054       tech_pc_sigma0 pre' = Some … pc_costs ∧
1055       ∀id. occurs_exactly_once id pre →
1056        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
1057    instr_list
1058    (λprefix,i,tl,prf,t.
1059      let 〈labels, pc_costs〉 ≝ t in
1060      let 〈program_counter, costs〉 ≝ pc_costs in
1061       let 〈label, i'〉 ≝ i in
1062       let labels ≝
1063         match label with
1064         [ None ⇒ labels
1065         | Some label ⇒
1066           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1067             insert ? ? label program_counter_bv labels
1068         ]
1069       in
1070         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
1071         [ None ⇒
1072            let dummy ≝ 〈labels,pc_costs〉 in
1073             dummy
1074         | Some construct ⇒ 〈labels, construct〉
1075         ]
1076    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
1077  in
1078   let 〈labels, pc_costs〉 ≝ result in
1079   let 〈pc, costs〉 ≝ pc_costs in
1080    〈labels, costs〉.
1081 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
1082 | whd cases construct in p3 #PC #CODE #JMEQ %
1083    [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
1084 | (* dummy case *) @⊥
1085   @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
1086 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
1087     >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
1088 whd in ⊢ (??(????%?)?) -labels1;
1089 cases label in Hid
1090  [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
1092       (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
1093     | whd in Hid >occurs_exactly_once_None in Hid // ]
1094  | -label #label #Hid whd in ⊢ (??(????%?)?)
1095
1096  ]
1097qed.
1098
1099lemma build_maps_ok:
1100 ∀p:pseudo_assembly_program.
1101  let 〈labels,costs〉 ≝ build_maps' p in
1102   ∀pc.
1103    (nat_of_bitvector … pc) < length … (\snd p) →
1104     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
1105 #p cases p #preamble #instr_list
1106  elim instr_list
1107   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
1108   | #hd #tl #IH
1109    whd in ⊢ (match % with [ _ ⇒ ?])
1110   ]
1111qed.
1112*)
1113
1114(*
1115lemma rev_preserves_length:
1116 ∀A.∀l. length … (rev A l) = length … l.
1117  #A #l elim l
1118   [ %
1119   | #hd #tl #IH normalize >length_append normalize /2/ ]
1120qed.
1121
1122lemma rev_append:
1123 ∀A.∀l1,l2.
1124  rev A (l1@l2) = rev A l2 @ rev A l1.
1125 #A #l1 elim l1 normalize //
1126qed.
1127
1128lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
1129 #A #l elim l
1130  [ //
1131  | #hd #tl #IH normalize >rev_append normalize // ]
1132qed.
1133
1134lemma split_len_Sn:
1135 ∀A:Type[0].∀l:list A.∀len.
1136  length … l = S len →
1137   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
1138 #A #l elim l
1139  [ normalize #len #abs destruct
1140  | #hd #tl #IH #len
1141    generalize in match (rev_rev … tl)
1142    cases (rev A tl) in ⊢ (??%? → ?)
1143     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/
1144     | #a #l' #H <H normalize #EQ
1145      %[@(hd::rev … l')] %[@a] % //
1146      >length_append in EQ #EQ normalize in EQ; normalize;
1147      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
1148qed.
1149
1150lemma list_elim_rev:
1151 ∀A:Type[0].∀P:list A → Type[0].
1152  P [ ] → (∀l,a. P l → P (l@[a])) →
1153   ∀l. P l.
1154 #A #P #H1 #H2 #l
1155 generalize in match (refl … (length … l))
1156 generalize in ⊢ (???% → ?) #n generalize in match l
1157 elim n
1158  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
1159  | #m #IH #L #EQ
1160    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
1161qed.
1162
1163axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
1164axiom prefix_of_append:
1165 ∀A:Type[0].∀l,l1,l2:list A.
1166  is_prefix … l l1 → is_prefix … l (l1@l2).
1167axiom prefix_reflexive: ∀A,l. is_prefix A l l.
1168axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
1169
1170record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
1171
1172definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
1173 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
1174
1175definition app ≝
1176 λA:Type[0].λl1:Propify (list A).λl2:list A.
1177  match l1 with
1178   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
1179
1180lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
1181 #A * /3/
1182qed.
1183
1184lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
1185 #A * #l1 normalize //
1186qed.
1187
1188let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
1189 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
1190 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
1191 B (app … prefix l) ≝
1192  match l with
1193  [ nil ⇒ ? (* b *)
1194  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1195  ].
1196 [ applyS b
1197 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
1198qed.
1199
1200(*
1201let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
1202 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
1203  match l with
1204  [ nil ⇒ ? (* b *)
1205  | cons hd tl ⇒
1206     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1207  ].
1208 [ applyS b
1209 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
1210qed.
1211*)
1212
1213definition foldll:
1214 ∀A:Type[0].∀B: Propify (list A) → Type[0].
1215  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
1216   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
1217 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1218
1219axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
1220axiom pprefix_of_append:
1221 ∀A:Type[0].∀l,l1,l2.
1222  is_pprefix A l l1 → is_pprefix A l (l1@l2).
1223axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
1224axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
1225
1226
1227axiom foldll':
1228 ∀A:Type[0].∀l: list A.
1229  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
1230  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
1231   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
1232 #A #l #B
1233 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
1234
1235
1236  #H #acc
1237 @foldll
1238  [
1239  |
1240  ]
1241
1242 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1243
1244
1245(*
1246record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
1247 { subset_wit:> A;
1248   subset_proof: P subset_wit
1249 }.
1250*)
1251
1252definition build_maps' ≝
1253  λpseudo_program.
1254  let 〈preamble,instr_list〉 ≝ pseudo_program in
1255  let result ≝
1256   foldll
1257    (option Identifier × pseudo_instruction)
1258    (λprefix.
1259      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1260       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
1261    (λprefix,t,i.
1262      let 〈labels, pc_costs〉 ≝ t in
1263      let 〈program_counter, costs〉 ≝ pc_costs in
1264       let 〈label, i'〉 ≝ i in
1265       let labels ≝
1266         match label with
1267         [ None ⇒ labels
1268         | Some label ⇒
1269           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1270             insert ? ? label program_counter_bv labels
1271         ]
1272       in
1273         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1274         [ None ⇒
1275            let dummy ≝ 〈labels,pc_costs〉 in
1276              dummy
1277         | Some construct ⇒ 〈labels, construct〉
1278         ]
1279    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
1280  in
1281   let 〈labels, pc_costs〉 ≝ result in
1282   let 〈pc, costs〉 ≝ pc_costs in
1283    〈labels, costs〉.
1284 [
1285 | @⊥
1286 | normalize % //
1287 ]
1288qed.
1289
1290definition build_maps' ≝
1291  λpseudo_program.
1292  let 〈preamble,instr_list〉 ≝ pseudo_program in
1293  let result ≝
1294   foldl
1295    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1296          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1297           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
1298    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1299          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1300           is_prefix ? instr_list_prefix' instr_list →
1301           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
1302    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1303          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1304           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
1305     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1306          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1307           is_prefix ? instr_list_prefix' instr_list →
1308           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
1309      let 〈labels, pc_costs〉 ≝ t in
1310      let 〈program_counter, costs〉 ≝ pc_costs in
1311       let 〈label, i'〉 ≝ i in
1312       let labels ≝
1313         match label with
1314         [ None ⇒ labels
1315         | Some label ⇒
1316           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1317             insert ? ? label program_counter_bv labels
1318         ]
1319       in
1320         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1321         [ None ⇒
1322            let dummy ≝ 〈labels,pc_costs〉 in
1323              dummy
1324         | Some construct ⇒ 〈labels, construct〉
1325         ]
1326    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
1327  in
1328   let 〈labels, pc_costs〉 ≝ result in
1329   let 〈pc, costs〉 ≝ pc_costs in
1330    〈labels, costs〉.
1331 [4: @(list_elim_rev ?
1332       (λinstr_list. list (
1333        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1334          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1335           is_prefix ? instr_list_prefix' instr_list →
1336           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
1337       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
1338      [ @[ ]
1339      | #l' #a #limage %2
1340        [ %[@a] #PREFIX #PREFIX_OK
1341        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
1342             THE INDUCTION HYPOTHESIS INSTEAD *)
1343          elim limage
1344           [ %1
1345           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
1346             @K1 @(prefix_of_append ???? K3)
1347           ]
1348        ]
1349
1350
1351
1352
1353  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
1354     % [@ (LIST_PREFIX @ [i])] %
1355      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
1356      | (* DOABLE IN PRINCIPLE *)
1357      ]
1358 | (* assert false case *)
1359 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
1360 |
1361*)
1362
1363axiom assembly_ok:
1364 ∀program,assembled,costs,labels.
1365  Some … 〈labels,costs〉 = build_maps program →
1366  Some … 〈assembled,costs〉 = assembly program →
1367  let code_memory ≝ load_code_memory assembled in
1368  let preamble ≝ \fst program in
1369  let datalabels ≝ construct_datalabels preamble in
1370  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1371  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1372   ∀ppc,len,assembledi.
1373    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1374     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
1375      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
1376       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
1377
1378axiom bitvector_of_nat_nat_of_bitvector:
1379  ∀n,v.
1380    bitvector_of_nat n (nat_of_bitvector n v) = v.
1381
1382axiom assembly_ok_to_expand_pseudo_instruction_ok:
1383 ∀program,assembled,costs.
1384  Some … 〈assembled,costs〉 = assembly program →
1385   ∀ppc.
1386    let code_memory ≝ load_code_memory assembled in
1387    let preamble ≝ \fst program in
1388    let data_labels ≝ construct_datalabels preamble in
1389    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1390    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1391    let expansion ≝ jump_expansion ppc program in
1392    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1393     ∃instructions.
1394      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
1395
1396lemma fetch_assembly_pseudo2:
1397 ∀program,assembled,costs,labels.
1398  Some … 〈labels,costs〉 = build_maps program →
1399  Some … 〈assembled,costs〉 = assembly program →
1400   ∀ppc.
1401    let code_memory ≝ load_code_memory assembled in
1402    let preamble ≝ \fst program in
1403    let data_labels ≝ construct_datalabels preamble in
1404    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1405    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1406    let expansion ≝ jump_expansion ppc program in
1407    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1408     ∃instructions.
1409      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
1410       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
1411 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
1412 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
1413 letin code_memory ≝ (load_code_memory assembled)
1414 letin preamble ≝ (\fst program)
1415 letin data_labels ≝ (construct_datalabels preamble)
1416 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
1417 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1418 whd in ⊢ (% → %)
1419 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
1420 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
1421 generalize in match (fetch_assembly_pseudo program ppc
1422  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
1424 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
1425 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
1426 normalize nodelta in EXPAND; (* HERE *)
1427 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
1428 >bitvector_of_nat_nat_of_bitvector in H1; #H1
1429 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
1430 #H1 #H2
1431 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
1432 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
1433  [ #K3 % [2: % [% | @K3]] | @K1 ]
1434qed.
1435
1436(* OLD?
1437definition assembly_specification:
1438  ∀assembly_program: pseudo_assembly_program.
1439  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1440  λpseudo_assembly_program.
1441  λcode_mem.
1442    ∀pc: Word.
1443      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1444      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1445      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1446      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1447      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1448       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1449      match pre_assembled with
1450       [ None ⇒ True
1451       | Some pc_code ⇒
1452          let 〈new_pc,code〉 ≝ pc_code in
1453           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1454
1455axiom assembly_meets_specification:
1456  ∀pseudo_assembly_program.
1457    match assembly pseudo_assembly_program with
1458    [ None ⇒ True
1459    | Some code_mem_cost ⇒
1460      let 〈code_mem, cost〉 ≝ code_mem_cost in
1462    ].
1463(*
1464  # PROGRAM
1465  [ cases PROGRAM
1466    # PREAMBLE
1467    # INSTR_LIST
1468    elim INSTR_LIST
1469    [ whd
1470      whd in ⊢ (∀_. %)
1471      # PC
1472      whd
1473    | # INSTR
1474      # INSTR_LIST_TL
1475      # H
1476      whd
1477      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1478    ]
1479  | cases not_implemented
1480  ] *)
1481*)
1482
1483definition status_of_pseudo_status: PseudoStatus → option Status ≝
1484 λps.
1485  let pap ≝ code_memory … ps in
1486   match assembly pap with
1487    [ None ⇒ None …
1488    | Some p ⇒
1489       let cm ≝ load_code_memory (\fst p) in
1490       let pc ≝ sigma pap (program_counter ? ps) in
1491        Some …
1492         (mk_PreStatus (BitVectorTrie Byte 16)
1493           cm
1494           (low_internal_ram … ps)
1495           (high_internal_ram … ps)
1496           (external_ram … ps)
1497           pc
1498           (special_function_registers_8051 … ps)
1499           (special_function_registers_8052 … ps)
1500           (p1_latch … ps)
1501           (p3_latch … ps)
1502           (clock … ps)) ].
1503
1504(*
1505definition write_at_stack_pointer':
1506 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1507  λM: Type[0].
1508  λs: PreStatus M.
1509  λv: Byte.
1510    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1511    let bit_zero ≝ get_index_v… nu O ? in
1512    let bit_1 ≝ get_index_v… nu 1 ? in
1513    let bit_2 ≝ get_index_v… nu 2 ? in
1514    let bit_3 ≝ get_index_v… nu 3 ? in
1515      if bit_zero then
1516        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1517                              v (low_internal_ram ? s) in
1518          set_low_internal_ram ? s memory
1519      else
1520        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1521                              v (high_internal_ram ? s) in
1522          set_high_internal_ram ? s memory.
1523  [ cases l0 %
1524  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1525qed.
1526
1527definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1528 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1529
1530  λticks_of.
1531  λs.
1532  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1533  let ticks ≝ ticks_of (program_counter ? s) in
1534  let s ≝ set_clock ? s (clock ? s + ticks) in
1535  let s ≝ set_program_counter ? s pc in
1536    match instr with
1537    [ Instruction instr ⇒
1538       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1539    | Comment cmt ⇒ s
1540    | Cost cst ⇒ s
1541    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1542    | Call call ⇒
1543      let a ≝ address_of_word_labels s call in
1544      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1545      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1546      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1547      let s ≝ write_at_stack_pointer' ? s pc_bl in
1548      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1549      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1550      let s ≝ write_at_stack_pointer' ? s pc_bu in
1551        set_program_counter ? s a
1552    | Mov dptr ident ⇒
1553       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1554    ].
1555 [
1556 |2,3,4: %
1557 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1558 |
1559 | %
1560 ]
1561 cases not_implemented
1562qed.
1563*)
1564
1565axiom execute_1_pseudo_instruction_preserves_code_memory:
1566 ∀ticks_of,ps.
1567  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1568
1569(*
1570lemma execute_code_memory_unchanged:
1571 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1572 #ticks #ps whd in ⊢ (??? (??%))
1573 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1574  (program_counter pseudo_assembly_program ps)) #instr #pc
1575 whd in ⊢ (??? (??%)) cases instr
1576  [ #pre cases pre
1577     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1578       cases (split ????) #z1 #z2 %
1579     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1580       cases (split ????) #z1 #z2 %
1581     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1582       cases (split ????) #z1 #z2 %
1583     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1584       [ #x1 whd in ⊢ (??? (??%))
1585     | *: cases not_implemented
1586     ]
1587  | #comment %
1588  | #cost %
1589  | #label %
1590  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1591    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1592    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1593    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1594    (* CSC: ??? *)
1595  | #dptr #label (* CSC: ??? *)
1596  ]
1597  cases not_implemented
1598qed.
1599*)
1600
1601lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1602 ∀ps,ps': PseudoStatus.
1603  code_memory … ps = code_memory … ps' →
1604   match status_of_pseudo_status ps with
1605    [ None ⇒ status_of_pseudo_status ps' = None …
1606    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
1607    ].
1608 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1609 generalize in match (refl … (assembly (code_memory … ps)))
1610 cases (assembly ?) in ⊢ (???% → %)
1611  [ #K whd whd in ⊢ (??%?) <H >K %
1612  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1613qed.
1614
1615definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
1616  λprogram: pseudo_assembly_program.
1617  λppc: Word.
1618  λfetched.
1619    match fetched with
1620    [ Instruction instr ⇒
1621      match instr with
1622      [ JC lbl ⇒
1623        match jump_expansion ppc program with
1624        [ short_jump ⇒ 〈2, 2〉
1625        | medium_jump ⇒ ?
1626        | long_jump ⇒ 〈4, 4〉
1627        ]
1628      | JNC lbl ⇒
1629        match jump_expansion ppc program with
1630        [ short_jump ⇒ 〈2, 2〉
1631        | medium_jump ⇒ ?
1632        | long_jump ⇒ 〈4, 4〉
1633        ]
1634      | JB bit lbl ⇒
1635        match jump_expansion ppc program with
1636        [ short_jump ⇒ 〈2, 2〉
1637        | medium_jump ⇒ ?
1638        | long_jump ⇒ 〈4, 4〉
1639        ]
1640      | JNB bit lbl ⇒
1641        match jump_expansion ppc program with
1642        [ short_jump ⇒ 〈2, 2〉
1643        | medium_jump ⇒ ?
1644        | long_jump ⇒ 〈4, 4〉
1645        ]
1646      | JBC bit lbl ⇒
1647        match jump_expansion ppc program with
1648        [ short_jump ⇒ 〈2, 2〉
1649        | medium_jump ⇒ ?
1650        | long_jump ⇒ 〈4, 4〉
1651        ]
1652      | JZ lbl ⇒
1653        match jump_expansion ppc program with
1654        [ short_jump ⇒ 〈2, 2〉
1655        | medium_jump ⇒ ?
1656        | long_jump ⇒ 〈4, 4〉
1657        ]
1658      | JNZ lbl ⇒
1659        match jump_expansion ppc program with
1660        [ short_jump ⇒ 〈2, 2〉
1661        | medium_jump ⇒ ?
1662        | long_jump ⇒ 〈4, 4〉
1663        ]
1664      | CJNE arg lbl ⇒
1665        match jump_expansion ppc program with
1666        [ short_jump ⇒ 〈2, 2〉
1667        | medium_jump ⇒ ?
1668        | long_jump ⇒ 〈4, 4〉
1669        ]
1670      | DJNZ arg lbl ⇒
1671        match jump_expansion ppc program with
1672        [ short_jump ⇒ 〈2, 2〉
1673        | medium_jump ⇒ ?
1674        | long_jump ⇒ 〈4, 4〉
1675        ]
1676      | ADD arg1 arg2 ⇒
1677        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1678         〈ticks, ticks〉
1679      | ADDC arg1 arg2 ⇒
1680        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1681         〈ticks, ticks〉
1682      | SUBB arg1 arg2 ⇒
1683        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1684         〈ticks, ticks〉
1685      | INC arg ⇒
1686        let ticks ≝ ticks_of_instruction (INC ? arg) in
1687         〈ticks, ticks〉
1688      | DEC arg ⇒
1689        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1690         〈ticks, ticks〉
1691      | MUL arg1 arg2 ⇒
1692        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1693         〈ticks, ticks〉
1694      | DIV arg1 arg2 ⇒
1695        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1696         〈ticks, ticks〉
1697      | DA arg ⇒
1698        let ticks ≝ ticks_of_instruction (DA ? arg) in
1699         〈ticks, ticks〉
1700      | ANL arg ⇒
1701        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1702         〈ticks, ticks〉
1703      | ORL arg ⇒
1704        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1705         〈ticks, ticks〉
1706      | XRL arg ⇒
1707        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1708         〈ticks, ticks〉
1709      | CLR arg ⇒
1710        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1711         〈ticks, ticks〉
1712      | CPL arg ⇒
1713        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1714         〈ticks, ticks〉
1715      | RL arg ⇒
1716        let ticks ≝ ticks_of_instruction (RL ? arg) in
1717         〈ticks, ticks〉
1718      | RLC arg ⇒
1719        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1720         〈ticks, ticks〉
1721      | RR arg ⇒
1722        let ticks ≝ ticks_of_instruction (RR ? arg) in
1723         〈ticks, ticks〉
1724      | RRC arg ⇒
1725        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1726         〈ticks, ticks〉
1727      | SWAP arg ⇒
1728        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1729         〈ticks, ticks〉
1730      | MOV arg ⇒
1731        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1732         〈ticks, ticks〉
1733      | MOVX arg ⇒
1734        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1735         〈ticks, ticks〉
1736      | SETB arg ⇒
1737        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1738         〈ticks, ticks〉
1739      | PUSH arg ⇒
1740        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1741         〈ticks, ticks〉
1742      | POP arg ⇒
1743        let ticks ≝ ticks_of_instruction (POP ? arg) in
1744         〈ticks, ticks〉
1745      | XCH arg1 arg2 ⇒
1746        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1747         〈ticks, ticks〉
1748      | XCHD arg1 arg2 ⇒
1749        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1750         〈ticks, ticks〉
1751      | RET ⇒
1752        let ticks ≝ ticks_of_instruction (RET ?) in
1753         〈ticks, ticks〉
1754      | RETI ⇒
1755        let ticks ≝ ticks_of_instruction (RETI ?) in
1756         〈ticks, ticks〉
1757      | NOP ⇒
1758        let ticks ≝ ticks_of_instruction (NOP ?) in
1759         〈ticks, ticks〉
1760      ]
1761    | Comment comment ⇒ 〈0, 0〉
1762    | Cost cost ⇒ 〈0, 0〉
1763    | Jmp jmp ⇒ 〈0, 2〉
1764    | Call call ⇒ 〈0, 2〉
1765    | Mov dptr tgt ⇒ 〈0, 2〉
1766    ].
1767  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1768qed.
1769
1770definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
1771  λprogram: pseudo_assembly_program.
1772  λppc: Word.
1773    let 〈preamble, pseudo〉 ≝ program in
1774    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1775     ticks_of0 program ppc fetched.
1776
1777lemma get_register_set_program_counter:
1778 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1779 #T #s #pc %
1780qed.
1781
1782lemma get_8051_sfr_set_program_counter:
1783 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1784 #T #s #pc %
1785qed.
1786
1788 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1789 #T #s #pc %
1790qed.
1791
1792lemma low_internal_ram_set_program_counter:
1793 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1794 #T #s #pc %
1795qed.
1796
1797lemma get_arg_8_set_program_counter:
1798 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
1799  ∀T,s,pc,b.∀arg:l.
1800   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
1801 [2,3: cases arg; *; normalize //]
1802 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
1803qed.
1804
1805lemma get_arg_8_set_code_memory:
1806 ∀T1,T2,s,code_mem,b,arg.
1807   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
1808 #T1 #T2 #s #code_mem #b #arg %
1809qed.
1810
1811lemma set_code_memory_set_flags:
1812 ∀T1,T2,s,f1,f2,f3,code_mem.
1813  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
1814   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
1815 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
1816qed.
1817
1818lemma set_program_counter_set_flags:
1819 ∀T1,s,f1,f2,f3,pc.
1820  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
1821   set_flags … (set_program_counter … s pc) f1 f2 f3.
1822 #T1 #s #f1 #f2 #f3 #pc  %
1823qed.
1824
1825lemma program_counter_set_flags:
1826 ∀T1,s,f1,f2,f3.
1827  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
1828 #T1 #s #f1 #f2 #f3 %
1829qed.
1830
1831lemma eq_rect_Type1_r:
1832  ∀A: Type[1].
1833  ∀a:A.
1834  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
1835  #A #a #P #H #x #p
1836  generalize in match H
1837  generalize in match P
1838  cases p
1839  //
1840qed.
1841
1842lemma main_thm:
1843 ∀ps,s,s''.
1844  status_of_pseudo_status ps = Some … s →
1845  status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
1846   ∃n. execute n s = s''.
1847 #ps #s #s''
1848 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
1849 whd in ⊢ (? → ??%? → ??%? → ?)
1850 >execute_1_pseudo_instruction_preserves_code_memory
1851 generalize in match (refl … (assembly (code_memory … ps)))
1852 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
1853 cases (build_maps (code_memory … ps))
1854  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H
1855    #abs @⊥ normalize in abs; destruct (abs) ]
1856 * #labels #costs generalize in match (refl … (code_memory … ps))
1857 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
1858 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
1859  [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
1860 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
1861 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
1862 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
1863 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
1864 change with
1865  (∃n.
1866    execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
1867   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?)
1868 whd in match (\snd 〈preamble,instr_list〉) in H;
1869 whd in match (\fst 〈preamble,instr_list〉) in H;
1870 whd in match (\snd 〈final_pc,assembled〉) in H;
1871 -s s'' labels costs final_ppc final_pc;
1872 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
1873 (* NICE STATEMENT HERE *)
1874 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
1875 #K <K generalize in match K; -K;
1876 (* STATEMENT WITH EQUALITY HERE *)
1877 whd in ⊢ (???(?%?) → ?)
1878 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
1879 cases (fetch_pseudo_instruction instr_list (program_counter … ps))
1880 #pi #newppc normalize nodelta; * #instructions *;
1881 cases pi normalize nodelta;
1882  [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0]
1883    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1884    #H2 >(eq_bv_to_eq … H2) >EQ %
1885  |4: (* Jmp *)
1886  |5: (* Call *)
1887  |6: (* Mov *)
1888  | (* Instruction *) -pi; *
1889    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #H1 #H2 #EQ %[1,3,5:@1]
1890       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1891       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1892       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1893       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1894       >H2b >(eq_instruction_to_eq … H2a)
1895       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1896       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1897       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1898       normalize nodelta;
1899       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1900       #result #flags
1901       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
1902    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
1903       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1904       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1905       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1906       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1907       >H2b >(eq_instruction_to_eq … H2a)
1908       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1909       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
1910       [1,2,3,4: cases (half_add ???) #carry #result
1911       | cases (half_add ???) #carry #bl normalize nodelta;
1912         cases (full_add ????) #carry' #bu normalize nodelta ]
1913        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
1914        [5: %
1915        |1:
Note: See TracBrowser for help on using the repository browser.