source: src/ASM/AssemblyProof.ma @ 942

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

New invariant for the main theorem.
The new invariant is much more complex since it needs to take care of
memory locations that hold pseudo addresses.

ATM, only the Comment and Cost cases are accepted, but the proof for
ADD/ADDC/SUBB is almost there and the one for Jump should pass almost untouched.
The Call proof should pass for the first time. All the others are still to
be done.
File size: 84.4 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)
116    #eq_heads #eq_tails
117    whd in eq_heads:(??(??(%))?);
118    cases(eq_b_eq … eq_heads)
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.
373  ∀p: Vector addressing_mode_tag m.
374  ∀q: Vector addressing_mode_tag n.
375  ∀to_search: addressing_mode.
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:
395  ∀to_search: addressing_mode.
396  ∀hd: addressing_mode_tag.
397  ∀n: nat.
398  ∀v: Vector addressing_mode_tag n.
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 
413let rec list_addressing_mode_tags_elim
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
435      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
436      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
437      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
438      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
439      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 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.
476    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
477    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
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)) ∧
481    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
482    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
483    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
484    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
485    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
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))) ∧
504    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
505    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
506    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
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)))) ∧
510    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
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 ]]))
516                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
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 ]]))
520                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
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
571let rec list_addressing_mode_tags_elim_prop
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.
578  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
579  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_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.
600               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
601               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
602               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
603               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
604               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 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. ?
638      | bit_addr ⇒ λbit_addr_prf. ?
639      | n_bit_addr ⇒ λn_bit_addr_prf. ?
640      | relative ⇒ λrelative_prf. ?
641      | addr11 ⇒ λaddr11_prf. ?
642      | addr16 ⇒ λaddr16_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
674      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
675      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
676      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
677      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
678      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 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
768definition load_code_memory_aux ≝
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
777axiom half_add_SO:
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
1024lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1025 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1026  address_of_word_labels_code_mem instr_list id =
1027  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
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
1091     [ >(address_of_word_labels_code_mem_None … Hid)
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
1423  (load_code_memory assembled));
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
1461        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
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 internal_pseudo_address_map ≝ list (BitVector 8).
1484
1485axiom low_internal_ram_of_pseudo_low_internal_ram:
1486 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1487
1488axiom high_internal_ram_of_pseudo_high_internal_ram:
1489 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1490
1491axiom low_internal_ram_of_pseudo_internal_ram_hit:
1492 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
1493  member ? (eq_bv 8) (false:::addr) M = true →
1494   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1495   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1496   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1497   let bl ≝ lookup ? 7 addr ram (zero 8) in
1498   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1499    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
1500
1501axiom low_internal_ram_of_pseudo_internal_ram_miss:
1502 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
1503  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1504  let 〈carr,Saddr〉 ≝ half_add ? addr (bitvector_of_nat 7 1) in
1505  carr = false →
1506  member ? (eq_bv 8) (false:::addr) M = false →
1507   member ? (eq_bv 8) (false:::Saddr) M = false →
1508    lookup ? 7 Saddr ram = lookup ? 7 Saddr (low_internal_ram … s).
1509
1510definition addressing_mode_ok ≝
1511 λM:internal_pseudo_address_map.λs:PseudoStatus.
1512  λaddr:addressing_mode.
1513   match addr with
1514    [ DIRECT d ⇒
1515       ¬(member ? (eq_bv 8) d M) ∧
1516       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1517    | INDIRECT i ⇒
1518       let d ≝ get_register ? s [[false;false;i]] in
1519       ¬(member ? (eq_bv 8) d M) ∧
1520       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1521    | EXT_INDIRECT _ ⇒ true
1522    | REGISTER _ ⇒ true
1523    | ACC_A ⇒ true
1524    | ACC_B ⇒ true
1525    | DPTR ⇒ true
1526    | DATA _ ⇒ true
1527    | DATA16 _ ⇒ true
1528    | ACC_DPTR ⇒ true
1529    | ACC_PC ⇒ true
1530    | EXT_INDIRECT_DPTR ⇒ true
1531    | INDIRECT_DPTR ⇒ true
1532    | CARRY ⇒ true
1533    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1534    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1535    | RELATIVE _ ⇒ true
1536    | ADDR11 _ ⇒ true
1537    | ADDR16 _ ⇒ true ].
1538
1539definition next_internal_pseudo_address_map ≝
1540 λM:internal_pseudo_address_map.
1541  λs:PseudoStatus.
1542   match \fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s)) with
1543    [ Comment _ ⇒ Some ? M
1544    | Cost _ ⇒ Some … M
1545    | Jmp _ ⇒ Some … M
1546    | Call _ ⇒
1547       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1548    | Mov _ _ ⇒ Some … M
1549    | Instruction instr ⇒
1550       match instr with
1551        [ ADD addr1 addr2 ⇒
1552           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
1553            Some ? M
1554           else
1555            None ?
1556        | ADDC addr1 addr2 ⇒
1557           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
1558            Some ? M
1559           else
1560            None ?
1561        | SUBB addr1 addr2 ⇒
1562           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
1563            Some ? M
1564           else
1565            None ?       
1566        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1567   
1568definition status_of_pseudo_status:
1569 internal_pseudo_address_map → PseudoStatus → option Status ≝
1570 λM,ps.
1571  let pap ≝ code_memory … ps in
1572   match assembly pap with
1573    [ None ⇒ None …
1574    | Some p ⇒
1575       let cm ≝ load_code_memory (\fst p) in
1576       let pc ≝ sigma pap (program_counter ? ps) in
1577       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1578       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (low_internal_ram … ps) in
1579        Some …
1580         (mk_PreStatus (BitVectorTrie Byte 16)
1581           cm
1582           lir
1583           hir
1584           (external_ram … ps)
1585           pc
1586           (special_function_registers_8051 … ps)
1587           (special_function_registers_8052 … ps)
1588           (p1_latch … ps)
1589           (p3_latch … ps)
1590           (clock … ps)) ].
1591
1592(*
1593definition write_at_stack_pointer':
1594 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1595  λM: Type[0].
1596  λs: PreStatus M.
1597  λv: Byte.
1598    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1599    let bit_zero ≝ get_index_v… nu O ? in
1600    let bit_1 ≝ get_index_v… nu 1 ? in
1601    let bit_2 ≝ get_index_v… nu 2 ? in
1602    let bit_3 ≝ get_index_v… nu 3 ? in
1603      if bit_zero then
1604        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1605                              v (low_internal_ram ? s) in
1606          set_low_internal_ram ? s memory
1607      else
1608        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1609                              v (high_internal_ram ? s) in
1610          set_high_internal_ram ? s memory.
1611  [ cases l0 %
1612  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1613qed.
1614
1615definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1616 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1617≝
1618  λticks_of.
1619  λs.
1620  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1621  let ticks ≝ ticks_of (program_counter ? s) in
1622  let s ≝ set_clock ? s (clock ? s + ticks) in
1623  let s ≝ set_program_counter ? s pc in
1624    match instr with
1625    [ Instruction instr ⇒
1626       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1627    | Comment cmt ⇒ s
1628    | Cost cst ⇒ s
1629    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1630    | Call call ⇒
1631      let a ≝ address_of_word_labels s call in
1632      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1633      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1634      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1635      let s ≝ write_at_stack_pointer' ? s pc_bl in
1636      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1637      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1638      let s ≝ write_at_stack_pointer' ? s pc_bu in
1639        set_program_counter ? s a
1640    | Mov dptr ident ⇒
1641       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1642    ].
1643 [
1644 |2,3,4: %
1645 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1646 |
1647 | %
1648 ]
1649 cases not_implemented
1650qed.
1651*)
1652
1653axiom execute_1_pseudo_instruction_preserves_code_memory:
1654 ∀ticks_of,ps.
1655  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1656
1657(*
1658lemma execute_code_memory_unchanged:
1659 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1660 #ticks #ps whd in ⊢ (??? (??%))
1661 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1662  (program_counter pseudo_assembly_program ps)) #instr #pc
1663 whd in ⊢ (??? (??%)) cases instr
1664  [ #pre cases pre
1665     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1666       cases (split ????) #z1 #z2 %
1667     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1668       cases (split ????) #z1 #z2 %
1669     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1670       cases (split ????) #z1 #z2 %
1671     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1672       [ #x1 whd in ⊢ (??? (??%))
1673     | *: cases not_implemented
1674     ]
1675  | #comment %
1676  | #cost %
1677  | #label %
1678  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1679    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1680    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1681    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1682    (* CSC: ??? *)
1683  | #dptr #label (* CSC: ??? *)
1684  ]
1685  cases not_implemented
1686qed.
1687*)
1688
1689lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1690 ∀M:internal_pseudo_address_map.
1691 ∀ps,ps': PseudoStatus.
1692  code_memory … ps = code_memory … ps' →
1693   match status_of_pseudo_status M ps with
1694    [ None ⇒ status_of_pseudo_status M ps' = None …
1695    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
1696    ].
1697 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1698 generalize in match (refl … (assembly (code_memory … ps)))
1699 cases (assembly ?) in ⊢ (???% → %)
1700  [ #K whd whd in ⊢ (??%?) <H >K %
1701  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1702qed.
1703
1704definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
1705  λprogram: pseudo_assembly_program.
1706  λppc: Word.
1707  λfetched.
1708    match fetched with
1709    [ Instruction instr ⇒
1710      match instr with
1711      [ JC lbl ⇒
1712        match jump_expansion ppc program with
1713        [ short_jump ⇒ 〈2, 2〉
1714        | medium_jump ⇒ ?
1715        | long_jump ⇒ 〈4, 4〉
1716        ]
1717      | JNC lbl ⇒
1718        match jump_expansion ppc program with
1719        [ short_jump ⇒ 〈2, 2〉
1720        | medium_jump ⇒ ?
1721        | long_jump ⇒ 〈4, 4〉
1722        ]
1723      | JB bit lbl ⇒
1724        match jump_expansion ppc program with
1725        [ short_jump ⇒ 〈2, 2〉
1726        | medium_jump ⇒ ?
1727        | long_jump ⇒ 〈4, 4〉
1728        ]
1729      | JNB bit lbl ⇒
1730        match jump_expansion ppc program with
1731        [ short_jump ⇒ 〈2, 2〉
1732        | medium_jump ⇒ ?
1733        | long_jump ⇒ 〈4, 4〉
1734        ]
1735      | JBC bit lbl ⇒
1736        match jump_expansion ppc program with
1737        [ short_jump ⇒ 〈2, 2〉
1738        | medium_jump ⇒ ?
1739        | long_jump ⇒ 〈4, 4〉
1740        ]
1741      | JZ lbl ⇒
1742        match jump_expansion ppc program with
1743        [ short_jump ⇒ 〈2, 2〉
1744        | medium_jump ⇒ ?
1745        | long_jump ⇒ 〈4, 4〉
1746        ]
1747      | JNZ lbl ⇒
1748        match jump_expansion ppc program with
1749        [ short_jump ⇒ 〈2, 2〉
1750        | medium_jump ⇒ ?
1751        | long_jump ⇒ 〈4, 4〉
1752        ]
1753      | CJNE arg lbl ⇒
1754        match jump_expansion ppc program with
1755        [ short_jump ⇒ 〈2, 2〉
1756        | medium_jump ⇒ ?
1757        | long_jump ⇒ 〈4, 4〉
1758        ]
1759      | DJNZ arg lbl ⇒
1760        match jump_expansion ppc program with
1761        [ short_jump ⇒ 〈2, 2〉
1762        | medium_jump ⇒ ?
1763        | long_jump ⇒ 〈4, 4〉
1764        ]
1765      | ADD arg1 arg2 ⇒
1766        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1767         〈ticks, ticks〉
1768      | ADDC arg1 arg2 ⇒
1769        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1770         〈ticks, ticks〉
1771      | SUBB arg1 arg2 ⇒
1772        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1773         〈ticks, ticks〉
1774      | INC arg ⇒
1775        let ticks ≝ ticks_of_instruction (INC ? arg) in
1776         〈ticks, ticks〉
1777      | DEC arg ⇒
1778        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1779         〈ticks, ticks〉
1780      | MUL arg1 arg2 ⇒
1781        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1782         〈ticks, ticks〉
1783      | DIV arg1 arg2 ⇒
1784        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1785         〈ticks, ticks〉
1786      | DA arg ⇒
1787        let ticks ≝ ticks_of_instruction (DA ? arg) in
1788         〈ticks, ticks〉
1789      | ANL arg ⇒
1790        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1791         〈ticks, ticks〉
1792      | ORL arg ⇒
1793        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1794         〈ticks, ticks〉
1795      | XRL arg ⇒
1796        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1797         〈ticks, ticks〉
1798      | CLR arg ⇒
1799        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1800         〈ticks, ticks〉
1801      | CPL arg ⇒
1802        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1803         〈ticks, ticks〉
1804      | RL arg ⇒
1805        let ticks ≝ ticks_of_instruction (RL ? arg) in
1806         〈ticks, ticks〉
1807      | RLC arg ⇒
1808        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1809         〈ticks, ticks〉
1810      | RR arg ⇒
1811        let ticks ≝ ticks_of_instruction (RR ? arg) in
1812         〈ticks, ticks〉
1813      | RRC arg ⇒
1814        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1815         〈ticks, ticks〉
1816      | SWAP arg ⇒
1817        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1818         〈ticks, ticks〉
1819      | MOV arg ⇒
1820        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1821         〈ticks, ticks〉
1822      | MOVX arg ⇒
1823        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1824         〈ticks, ticks〉
1825      | SETB arg ⇒
1826        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1827         〈ticks, ticks〉
1828      | PUSH arg ⇒
1829        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1830         〈ticks, ticks〉
1831      | POP arg ⇒
1832        let ticks ≝ ticks_of_instruction (POP ? arg) in
1833         〈ticks, ticks〉
1834      | XCH arg1 arg2 ⇒
1835        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1836         〈ticks, ticks〉
1837      | XCHD arg1 arg2 ⇒
1838        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1839         〈ticks, ticks〉
1840      | RET ⇒
1841        let ticks ≝ ticks_of_instruction (RET ?) in
1842         〈ticks, ticks〉
1843      | RETI ⇒
1844        let ticks ≝ ticks_of_instruction (RETI ?) in
1845         〈ticks, ticks〉
1846      | NOP ⇒
1847        let ticks ≝ ticks_of_instruction (NOP ?) in
1848         〈ticks, ticks〉
1849      ]
1850    | Comment comment ⇒ 〈0, 0〉
1851    | Cost cost ⇒ 〈0, 0〉
1852    | Jmp jmp ⇒ 〈2, 2〉
1853    | Call call ⇒ 〈2, 2〉
1854    | Mov dptr tgt ⇒ 〈2, 2〉
1855    ].
1856  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1857qed.
1858
1859definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
1860  λprogram: pseudo_assembly_program.
1861  λppc: Word.
1862    let 〈preamble, pseudo〉 ≝ program in
1863    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1864     ticks_of0 program ppc fetched.
1865
1866lemma get_register_set_program_counter:
1867 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1868 #T #s #pc %
1869qed.
1870
1871lemma get_8051_sfr_set_program_counter:
1872 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1873 #T #s #pc %
1874qed.
1875
1876lemma get_bit_addressable_sfr_set_program_counter:
1877 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1878 #T #s #pc %
1879qed.
1880
1881lemma low_internal_ram_set_program_counter:
1882 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1883 #T #s #pc %
1884qed.
1885
1886lemma get_arg_8_set_program_counter:
1887 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
1888  ∀T,s,pc,b.∀arg:l.
1889   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
1890 [2,3: cases arg; *; normalize //]
1891 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
1892qed.
1893
1894lemma set_bit_addressable_sfr_set_code_memory:
1895  ∀T, U: Type[0].
1896  ∀ps: PreStatus ?.
1897  ∀code_mem.
1898  ∀x.
1899  ∀val.
1900  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
1901  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
1902  #T #U #ps #code_mem #x #val
1903  whd in ⊢ (??%?)
1904  whd in ⊢ (???(???%?))
1905  cases (eqb ? 128) [ normalize nodelta cases not_implemented
1906  | normalize nodelta
1907  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1908  | normalize nodelta
1909  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1910  | normalize nodelta
1911  cases (eqb ? 176) [ normalize nodelta %
1912  | normalize nodelta
1913  cases (eqb ? 153) [ normalize nodelta %
1914  | normalize nodelta
1915  cases (eqb ? 138) [ normalize nodelta %
1916  | normalize nodelta
1917  cases (eqb ? 139) [ normalize nodelta %
1918  | normalize nodelta
1919  cases (eqb ? 140) [ normalize nodelta %
1920  | normalize nodelta
1921  cases (eqb ? 141) [ normalize nodelta %
1922  | normalize nodelta
1923  cases (eqb ? 200) [ normalize nodelta %
1924  | normalize nodelta
1925  cases (eqb ? 202) [ normalize nodelta %
1926  | normalize nodelta
1927  cases (eqb ? 203) [ normalize nodelta %
1928  | normalize nodelta
1929  cases (eqb ? 204) [ normalize nodelta %
1930  | normalize nodelta
1931  cases (eqb ? 205) [ normalize nodelta %
1932  | normalize nodelta
1933  cases (eqb ? 135) [ normalize nodelta %
1934  | normalize nodelta
1935  cases (eqb ? 136) [ normalize nodelta %
1936  | normalize nodelta
1937  cases (eqb ? 137) [ normalize nodelta %
1938  | normalize nodelta
1939  cases (eqb ? 152) [ normalize nodelta %
1940  | normalize nodelta
1941  cases (eqb ? 168) [ normalize nodelta %
1942  | normalize nodelta
1943  cases (eqb ? 184) [ normalize nodelta %
1944  | normalize nodelta
1945  cases (eqb ? 129) [ normalize nodelta %
1946  | normalize nodelta
1947  cases (eqb ? 130) [ normalize nodelta %
1948  | normalize nodelta
1949  cases (eqb ? 131) [ normalize nodelta %
1950  | normalize nodelta
1951  cases (eqb ? 208) [ normalize nodelta %
1952  | normalize nodelta
1953  cases (eqb ? 224) [ normalize nodelta %
1954  | normalize nodelta
1955  cases (eqb ? 240) [ normalize nodelta %
1956  | normalize nodelta
1957    cases not_implemented
1958  ]]]]]]]]]]]]]]]]]]]]]]]]]]
1959qed.
1960
1961lemma set_arg_8_set_code_memory:
1962  ∀n:nat.
1963  ∀l:Vector addressing_mode_tag (S n).
1964    ¬(is_in ? l ACC_PC) →
1965    ∀T: Type[0].
1966    ∀U: Type[0].
1967    ∀ps: PreStatus ?.
1968    ∀code_mem.
1969    ∀val.
1970    ∀b: l.
1971  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
1972  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
1973  [2,3: cases b; *; normalize //]
1974  #n #l #prf #T #U #ps #code_mem #val * *;
1975  [*:
1976    [1,2,3,4,8,9,15,16,17,18,19: #x]
1977    try #y whd in ⊢ (??(%)?)
1978    whd in ⊢ (???(???(%)?))
1979    [1,2:
1980      cases (split bool 4 4 ?)
1981      #nu' #nl'
1982      normalize nodelta
1983      cases (split bool 1 3 nu')
1984      #bit1' #ignore'
1985      normalize nodelta
1986      cases (get_index_v bool 4 nu' 1 ?)
1987      [1,2,3,4:
1988        normalize nodelta
1989        try %
1990        try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
1991        try (normalize in ⊢ (???(???%?)))
1992      ]
1993    |3,4: %
1994    |*:
1995       try normalize nodelta
1996       normalize cases (not_implemented)
1997    ]
1998 ]
1999qed.
2000
2001axiom set_arg_8_set_program_counter:
2002  ∀n:nat.
2003  ∀l:Vector addressing_mode_tag (S n).
2004    ¬(is_in ? l ACC_PC) →
2005    ∀T: Type[0].
2006    ∀ps: PreStatus ?.
2007    ∀pc.
2008    ∀val.
2009    ∀b: l.
2010  set_arg_8 ? (set_program_counter T ps pc) b val =
2011  set_program_counter T (set_arg_8 ? ps b val) pc.
2012  [1,2: cases b; *; normalize //]
2013qed.
2014 
2015
2016lemma get_arg_8_set_code_memory:
2017 ∀T1,T2,s,code_mem,b,arg.
2018   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
2019 #T1 #T2 #s #code_mem #b #arg %
2020qed.
2021
2022lemma set_code_memory_set_flags:
2023 ∀T1,T2,s,f1,f2,f3,code_mem.
2024  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
2025   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
2026 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
2027qed.
2028
2029lemma set_program_counter_set_flags:
2030 ∀T1,s,f1,f2,f3,pc.
2031  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
2032   set_flags … (set_program_counter … s pc) f1 f2 f3.
2033 #T1 #s #f1 #f2 #f3 #pc  %
2034qed.
2035
2036lemma program_counter_set_flags:
2037 ∀T1,s,f1,f2,f3.
2038  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
2039 #T1 #s #f1 #f2 #f3 %
2040qed.
2041
2042lemma eq_rect_Type1_r:
2043  ∀A: Type[1].
2044  ∀a:A.
2045  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2046  #A #a #P #H #x #p
2047  generalize in match H
2048  generalize in match P
2049  cases p
2050  //
2051qed.
2052
2053lemma split_eq_status:
2054 ∀T.
2055 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
2056 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
2057  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
2058   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
2059   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
2060 //
2061qed.
2062
2063lemma main_thm:
2064 ∀M,M',ps,s,s''.
2065  next_internal_pseudo_address_map M ps = Some … M' →
2066  status_of_pseudo_status M ps = Some … s →
2067  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
2068   ∃n. execute n s = s''.
2069 #M #M' #ps #s #s''
2070 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
2071 whd in ⊢ (? → ? → ??%? → ??%? → ?)
2072 >execute_1_pseudo_instruction_preserves_code_memory
2073 generalize in match (refl … (assembly (code_memory … ps)))
2074 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
2075 cases (build_maps (code_memory … ps))
2076  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
2077    #abs @⊥ normalize in abs; destruct (abs) ]
2078 * #labels #costs whd in ⊢ (? → ? → ??%? → ?) generalize in match (refl … (code_memory … ps))
2079 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
2080 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
2081  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
2082 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
2083 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
2084 #MAP
2085 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
2086 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
2087 change with
2088  (∃n.
2089    execute n
2090     (set_low_internal_ram ?
2091       (set_high_internal_ram ?
2092         (set_program_counter ?
2093           (set_code_memory ?? ps (load_code_memory assembled))
2094          (sigma 〈preamble,instr_list〉 (program_counter ? ps)))
2095        (high_internal_ram_of_pseudo_high_internal_ram M ?))
2096      (low_internal_ram_of_pseudo_low_internal_ram M ?))
2097   = set_low_internal_ram ?
2098      (set_high_internal_ram ?
2099        (set_program_counter ?
2100          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
2101         (sigma ??))
2102       ?)
2103     ?)
2104 whd in match (\snd 〈preamble,instr_list〉) in H;
2105 whd in match (\fst 〈preamble,instr_list〉) in H;
2106 whd in match (\snd 〈final_pc,assembled〉) in H;
2107 whd in match (\snd 〈preamble,instr_list〉) in MAP;
2108 -s s'' labels costs final_ppc final_pc;
2109 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
2110 (* NICE STATEMENT HERE *)
2111 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
2112 #K <K generalize in match K; -K;
2113 (* STATEMENT WITH EQUALITY HERE *)
2114 whd in ⊢ (???(?%?) → ?)
2115 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
2116 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
2117 #pi #newppc normalize nodelta; #MAP * #instructions *;
2118 cases pi in MAP; normalize nodelta;
2119  [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
2120    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
2121    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2122    #H2 >(eq_bv_to_eq … H2) >EQ %
2123(*  |6: (* Mov *) #arg1 #arg2
2124       #H1 #H2 #EQ %[@1]
2125       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2126       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2127       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2128       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2129       >H2b >(eq_instruction_to_eq … H2a)
2130       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2131       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2132       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2133       normalize nodelta;
2134       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2135       #result #flags
2136       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
2137(*  |4,5: (* Jmp, Call *) #label
2138      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
2139       [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
2140           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2141           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2142           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2143           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2144           >H2b >(eq_instruction_to_eq … H2a)
2145           generalize in match EQ; -EQ;
2146           [2: whd in ⊢ (???% → ??%?);
2147               cases (half_add ???) #carry #new_sp normalize nodelta;
2148               >(eq_bv_to_eq … H2c)
2149               change with
2150                ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) →
2151                    (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2152               (* MISMATCH ON WHAT IS ON THE STACK!!!! *)
2153               (* HOW TO PROVE THIS?? *)
2154           ]
2155           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2156           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
2157            [2: % | ]
2158       |4: (* short Call *) #abs @⊥ destruct (abs)
2159       |1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2160           generalize in match
2161            (refl ?
2162             (sub_16_with_carry
2163              (sigma 〈preamble,instr_list〉 (program_counter … ps))
2164              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
2165              false))
2166           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2167           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2168           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2169           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2170           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2171           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2172           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2173           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2174           >H2b >(eq_instruction_to_eq … H2a)
2175           generalize in match EQ; -EQ;
2176           whd in ⊢ (???% → ?);
2177           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2178           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
2179           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
2180           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2181           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
2182           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2183       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2184         generalize in match
2185          (refl …
2186            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
2187         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2188         generalize in match
2189          (refl …
2190            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
2191         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2192         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2193         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2194         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2195         change in ⊢ (? →??%?) with (execute_1_0 ??)
2196           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2197           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2198           >H2b >(eq_instruction_to_eq … H2a)
2199           generalize in match EQ; -EQ;
2200           whd in ⊢ (???% → ?);
2201           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
2202           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2203           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2204           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2205           generalize in match (refl … (split bool 4 4 pc_bu))
2206           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2207           generalize in match (refl … (split bool 3 8 rest_addr))
2208           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2209           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2210           generalize in match
2211            (refl …
2212             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2213             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2214           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2215           @split_eq_status try %
2216            [ change with (? = sigma ? (address_of_word_labels ps label))
2217              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2218            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2219              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2220  (*|5: (* Call *)*) *)
2221  | (* Instruction *) -pi; *; normalize nodelta;
2222    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2223       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2224       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2225       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2226       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2227       >H2b >(eq_instruction_to_eq … H2a)
2228       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2229       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2230       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2231       normalize nodelta; #MAP;(* [1,2:whd in MAP:(??(match % with [ _ ⇒ ?])?)]*)
2232       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2233       #result #flags
2234       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
2235    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2236       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2237       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2238       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2239       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2240       >H2b >(eq_instruction_to_eq … H2a)
2241       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2242       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2243       [1,2,3,4: cases (half_add ???) #carry #result
2244       | cases (half_add ???) #carry #bl normalize nodelta;
2245         cases (full_add ????) #carry' #bu normalize nodelta ]
2246        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
2247        [5: %
2248        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2249      (set_program_counter pseudo_assembly_program ps newppc)
2250      (\fst  (ticks_of0 〈preamble,instr_list〉
2251                   (program_counter pseudo_assembly_program ps)
2252                   (Instruction (INC Identifier (DIRECT ARG))))
2253       +clock pseudo_assembly_program
2254        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2255        [2,3: // ]
2256            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2257            whd in ⊢ (??%%)
2258            cases (split bool 4 4 ARG)
2259            #nu' #nl'
2260            normalize nodelta
2261            cases (split bool 1 3 nu')
2262            #bit_1' #ignore'
2263            normalize nodelta
2264            cases (get_index_v bool 4 nu' ? ?)
2265            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2266            |
2267            ]
Note: See TracBrowser for help on using the repository browser.