source: src/ASM/AssemblyProof.ma @ 979

Last change on this file since 979 was 979, checked in by sacerdot, 9 years ago

...

File size: 106.7 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 sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
927 λinstr_list.λl:list labelled_instruction.
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 ? ?)〉〉) l.
942
943definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
944 ≝ λprog.sigma00 prog (\snd prog).
945
946definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
947 λprogram,instr_list.
948  match sigma00 program instr_list with
949   [ None ⇒ None …
950   | Some result ⇒
951      let 〈ppc,pc_sigma_map〉 ≝ result in
952      let 〈pc,map〉 ≝ pc_sigma_map in
953       Some … 〈ppc,pc〉 ].
954
955definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
956 λinstr_list.
957  match sigma0 instr_list with
958  [ None ⇒ None ?
959  | Some result ⇒
960    let 〈ppc,pc_sigma_map〉 ≝ result in
961    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
962      if gtb pc (2^16) then
963        None ?
964      else
965        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
966
967axiom policy_ok: ∀p. sigma_safe p ≠ None ….
968
969definition sigma: pseudo_assembly_program → Word → Word ≝
970 λp.
971  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
972   [ None ⇒ λabs. ⊥
973   | Some r ⇒ λ_.r] (policy_ok p).
974 cases abs //
975qed.
976
977lemma length_append:
978 ∀A.∀l1,l2:list A.
979  |l1 @ l2| = |l1| + |l2|.
980 #A #l1 elim l1
981  [ //
982  | #hd #tl #IH #l2 normalize <IH //]
983qed.
984
985let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
986 match l with
987  [ nil ⇒ true
988  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
989
990lemma does_not_occur_None:
991 ∀id,i,list_instr.
992  does_not_occur id (list_instr@[〈None …,i〉]) =
993  does_not_occur id list_instr.
994 #id #i #list_instr elim list_instr
995  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
996qed.
997
998lemma does_not_occur_Some:
999 ∀id,id',i,list_instr.
1000  eq_bv ? id' id = false →
1001   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
1002    does_not_occur id list_instr.
1003 #id #id' #i #list_instr elim list_instr
1004  [ #H normalize in H ⊢ %; >H %
1005  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
1006qed.
1007
1008lemma does_not_occur_absurd:
1009 ∀id,i,list_instr.
1010  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
1011 #id #i #list_instr elim list_instr
1012  [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
1013    >eq_bv_refl %
1014  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
1015qed.
1016
1017let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
1018 match l with
1019  [ nil ⇒ false
1020  | cons hd tl ⇒
1021     if instruction_matches_identifier id hd then
1022      does_not_occur id tl
1023     else
1024      occurs_exactly_once id tl ].
1025
1026lemma occurs_exactly_once_None:
1027 ∀id,i,list_instr.
1028  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
1029  occurs_exactly_once id list_instr.
1030 #id #i #list_instr elim list_instr
1031  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
1032qed.
1033
1034lemma occurs_exactly_once_Some:
1035 ∀id,id',i,prefix.
1036  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
1037 #id #id' #i #prefix elim prefix
1038  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
1039    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
1040  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
1041    cases he; normalize nodelta
1042     [ #H @ (IH H)
1043     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
1044       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
1045       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
1046        /2/ #H >does_not_occur_Some //
1047       | #H @IH @H]]]
1048qed.
1049
1050lemma index_of_internal_None: ∀i,id,instr_list,n.
1051 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1052  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1053   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
1054 #i #id #instr_list elim instr_list
1055  [ #n #abs whd in abs; cases abs
1056  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
1057    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
1058    [ #H %
1059    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
1060      [ #_ % | #abs cases abs ]]]
1061qed.
1062
1063lemma index_of_internal_Some_miss: ∀i,id,id'.
1064 eq_bv ? id' id = false →
1065 ∀instr_list,n.
1066 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
1067  index_of_internal ? (instruction_matches_identifier id) instr_list n =
1068   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
1069 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
1070 change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
1071  [ #n #abs cases abs
1072  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
1073    [ // | #K @IH //]]
1074qed.
1075
1076lemma index_of_internal_Some_hit: ∀i,id.
1077 ∀instr_list,n.
1078  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1079   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
1080  = |instr_list| + n.
1081 #i #id #instr_list elim instr_list
1082  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
1083  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
1084    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
1085qed.
1086
1087lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1088 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1089  address_of_word_labels_code_mem instr_list id =
1090  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1091 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1092 >(index_of_internal_None … H) %
1093qed.
1094
1095lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1096 eq_bv ? id' id = false →
1097  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
1098   address_of_word_labels_code_mem instr_list id =
1099   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1100 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1101 >(index_of_internal_Some_miss … H) //
1102qed.
1103
1104lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1105  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1106   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1107   = bitvector_of_nat … (|instr_list|).
1108 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
1109 >(index_of_internal_Some_hit … H) //
1110qed.
1111
1112axiom tech_pc_sigma00_append_Some:
1113 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
1114  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
1115   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
1116    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
1117
1118axiom tech_pc_sigma00_append_None:
1119 ∀program,prefix,i,ppc,pc,costs.
1120  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
1121   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
1122    → False.
1123
1124lemma eq_false_to_notb: ∀b. b = false → ¬ b.
1125 *; //
1126qed.
1127
1128lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
1129 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
1130qed.
1131
1132example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1133 cases daemon.
1134qed.
1135
1136axiom construct_costs_sigma:
1137 ∀p,ppc,pc,pc',costs,costs',i.
1138  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
1139   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
1140    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
1141
1142definition build_maps' ≝
1143  λpseudo_program.
1144  let result ≝
1145   foldl_strong
1146    (option Identifier × pseudo_instruction)
1147    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1148      let 〈labels,ppc_pc_costs〉 ≝ res in
1149      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1150      let 〈pc',costs〉 ≝ pc_costs in
1151       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
1152       ppc' = length … pre ∧
1153       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
1154       ∀id. occurs_exactly_once id pre →
1155        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
1156    (\snd pseudo_program)
1157    (λprefix,i,tl,prf,t.
1158      let 〈labels, ppc_pc_costs〉 ≝ t in
1159      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1160      let 〈pc,costs〉 ≝ pc_costs in
1161       let 〈label, i'〉 ≝ i in
1162       let labels ≝
1163         match label with
1164         [ None ⇒ labels
1165         | Some label ⇒
1166           let program_counter_bv ≝ bitvector_of_nat ? pc in
1167             insert ? ? label program_counter_bv labels
1168         ]
1169       in
1170         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
1171         [ None ⇒
1172            let dummy ≝ 〈labels,ppc_pc_costs〉 in
1173             dummy
1174         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
1175         ]
1176    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1177  in
1178   let 〈labels, ppc_pc_costs〉 ≝ result in
1179   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1180   let 〈pc, costs〉 ≝ pc_costs in
1181    〈labels, costs〉.
1182 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1183 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1184   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
1185   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
1186   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1187   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
1188   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1189     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1190     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1191       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1192        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1193          <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H]
1194        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
1195          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1196 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
1197   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
1198qed.
1199
1200lemma build_maps_ok:
1201 ∀p:pseudo_assembly_program.
1202  let 〈labels,costs〉 ≝ build_maps' p in
1203   ∀pc.
1204    (nat_of_bitvector … pc) < length … (\snd p) →
1205     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
1206 #p cases p #preamble #instr_list
1207  elim instr_list
1208   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
1209   | #hd #tl #IH
1210    whd in ⊢ (match % with [ _ ⇒ ?])
1211   ]
1212qed.
1213*)
1214
1215(*
1216lemma rev_preserves_length:
1217 ∀A.∀l. length … (rev A l) = length … l.
1218  #A #l elim l
1219   [ %
1220   | #hd #tl #IH normalize >length_append normalize /2/ ]
1221qed.
1222
1223lemma rev_append:
1224 ∀A.∀l1,l2.
1225  rev A (l1@l2) = rev A l2 @ rev A l1.
1226 #A #l1 elim l1 normalize //
1227qed.
1228 
1229lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
1230 #A #l elim l
1231  [ //
1232  | #hd #tl #IH normalize >rev_append normalize // ]
1233qed.
1234
1235lemma split_len_Sn:
1236 ∀A:Type[0].∀l:list A.∀len.
1237  length … l = S len →
1238   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
1239 #A #l elim l
1240  [ normalize #len #abs destruct
1241  | #hd #tl #IH #len
1242    generalize in match (rev_rev … tl)
1243    cases (rev A tl) in ⊢ (??%? → ?)
1244     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
1245     | #a #l' #H <H normalize #EQ
1246      %[@(hd::rev … l')] %[@a] % //
1247      >length_append in EQ #EQ normalize in EQ; normalize;
1248      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
1249qed.
1250
1251lemma list_elim_rev:
1252 ∀A:Type[0].∀P:list A → Type[0].
1253  P [ ] → (∀l,a. P l → P (l@[a])) →
1254   ∀l. P l.
1255 #A #P #H1 #H2 #l
1256 generalize in match (refl … (length … l))
1257 generalize in ⊢ (???% → ?) #n generalize in match l
1258 elim n
1259  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
1260  | #m #IH #L #EQ
1261    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
1262qed.
1263
1264axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
1265axiom prefix_of_append:
1266 ∀A:Type[0].∀l,l1,l2:list A.
1267  is_prefix … l l1 → is_prefix … l (l1@l2).
1268axiom prefix_reflexive: ∀A,l. is_prefix A l l.
1269axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
1270
1271record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
1272
1273definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
1274 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
1275
1276definition app ≝
1277 λA:Type[0].λl1:Propify (list A).λl2:list A.
1278  match l1 with
1279   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
1280
1281lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
1282 #A * /3/
1283qed.
1284
1285lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
1286 #A * #l1 normalize //
1287qed.
1288
1289let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
1290 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
1291 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
1292 B (app … prefix l) ≝
1293  match l with
1294  [ nil ⇒ ? (* b *)
1295  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1296  ].
1297 [ applyS b
1298 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
1299qed.
1300
1301(*
1302let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
1303 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
1304  match l with
1305  [ nil ⇒ ? (* b *)
1306  | cons hd tl ⇒
1307     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1308  ].
1309 [ applyS b
1310 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
1311qed.
1312*)
1313
1314definition foldll:
1315 ∀A:Type[0].∀B: Propify (list A) → Type[0].
1316  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
1317   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
1318 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1319
1320axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
1321axiom pprefix_of_append:
1322 ∀A:Type[0].∀l,l1,l2.
1323  is_pprefix A l l1 → is_pprefix A l (l1@l2).
1324axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
1325axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
1326
1327
1328axiom foldll':
1329 ∀A:Type[0].∀l: list A.
1330  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
1331  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
1332   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
1333 #A #l #B
1334 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
1335 
1336 
1337  #H #acc
1338 @foldll
1339  [
1340  |
1341  ]
1342 
1343 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1344
1345
1346(*
1347record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
1348 { subset_wit:> A;
1349   subset_proof: P subset_wit
1350 }.
1351*)
1352
1353definition build_maps' ≝
1354  λpseudo_program.
1355  let 〈preamble,instr_list〉 ≝ pseudo_program in
1356  let result ≝
1357   foldll
1358    (option Identifier × pseudo_instruction)
1359    (λprefix.
1360      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1361       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
1362    (λprefix,t,i.
1363      let 〈labels, pc_costs〉 ≝ t in
1364      let 〈program_counter, costs〉 ≝ pc_costs in
1365       let 〈label, i'〉 ≝ i in
1366       let labels ≝
1367         match label with
1368         [ None ⇒ labels
1369         | Some label ⇒
1370           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1371             insert ? ? label program_counter_bv labels
1372         ]
1373       in
1374         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1375         [ None ⇒
1376            let dummy ≝ 〈labels,pc_costs〉 in
1377              dummy
1378         | Some construct ⇒ 〈labels, construct〉
1379         ]
1380    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
1381  in
1382   let 〈labels, pc_costs〉 ≝ result in
1383   let 〈pc, costs〉 ≝ pc_costs in
1384    〈labels, costs〉.
1385 [
1386 | @⊥
1387 | normalize % //
1388 ]
1389qed.
1390
1391definition build_maps' ≝
1392  λpseudo_program.
1393  let 〈preamble,instr_list〉 ≝ pseudo_program in
1394  let result ≝
1395   foldl
1396    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1397          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1398           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
1399    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1400          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1401           is_prefix ? instr_list_prefix' instr_list →
1402           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
1403    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1404          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1405           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
1406     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1407          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1408           is_prefix ? instr_list_prefix' instr_list →
1409           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
1410      let 〈labels, pc_costs〉 ≝ t in
1411      let 〈program_counter, costs〉 ≝ pc_costs in
1412       let 〈label, i'〉 ≝ i in
1413       let labels ≝
1414         match label with
1415         [ None ⇒ labels
1416         | Some label ⇒
1417           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1418             insert ? ? label program_counter_bv labels
1419         ]
1420       in
1421         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1422         [ None ⇒
1423            let dummy ≝ 〈labels,pc_costs〉 in
1424              dummy
1425         | Some construct ⇒ 〈labels, construct〉
1426         ]
1427    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
1428  in
1429   let 〈labels, pc_costs〉 ≝ result in
1430   let 〈pc, costs〉 ≝ pc_costs in
1431    〈labels, costs〉.
1432 [4: @(list_elim_rev ?
1433       (λinstr_list. list (
1434        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1435          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1436           is_prefix ? instr_list_prefix' instr_list →
1437           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
1438       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
1439      [ @[ ]
1440      | #l' #a #limage %2
1441        [ %[@a] #PREFIX #PREFIX_OK
1442        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
1443             THE INDUCTION HYPOTHESIS INSTEAD *)
1444          elim limage
1445           [ %1
1446           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
1447             @K1 @(prefix_of_append ???? K3)
1448           ] 
1449        ]
1450       
1451       
1452     
1453 
1454  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
1455     % [@ (LIST_PREFIX @ [i])] %
1456      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
1457      | (* DOABLE IN PRINCIPLE *)
1458      ]
1459 | (* assert false case *)
1460 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
1461 |   
1462*)
1463
1464axiom assembly_ok:
1465 ∀program,assembled,costs,labels.
1466  Some … 〈labels,costs〉 = build_maps program →
1467  Some … 〈assembled,costs〉 = assembly program →
1468  let code_memory ≝ load_code_memory assembled in
1469  let preamble ≝ \fst program in
1470  let datalabels ≝ construct_datalabels preamble in
1471  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1472  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1473   ∀ppc,len,assembledi.
1474    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1475     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
1476      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
1477       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
1478
1479axiom bitvector_of_nat_nat_of_bitvector:
1480  ∀n,v.
1481    bitvector_of_nat n (nat_of_bitvector n v) = v.
1482
1483axiom assembly_ok_to_expand_pseudo_instruction_ok:
1484 ∀program,assembled,costs.
1485  Some … 〈assembled,costs〉 = assembly program →
1486   ∀ppc.
1487    let code_memory ≝ load_code_memory assembled in
1488    let preamble ≝ \fst program in   
1489    let data_labels ≝ construct_datalabels preamble in
1490    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1491    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1492    let expansion ≝ jump_expansion ppc program in
1493    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1494     ∃instructions.
1495      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
1496
1497lemma fetch_assembly_pseudo2:
1498 ∀program,assembled,costs,labels.
1499  Some … 〈labels,costs〉 = build_maps program →
1500  Some … 〈assembled,costs〉 = assembly program →
1501   ∀ppc.
1502    let code_memory ≝ load_code_memory assembled in
1503    let preamble ≝ \fst program in
1504    let data_labels ≝ construct_datalabels preamble in
1505    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1506    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1507    let expansion ≝ jump_expansion ppc program in
1508    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1509     ∃instructions.
1510      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
1511       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
1512 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
1513 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
1514 letin code_memory ≝ (load_code_memory assembled)
1515 letin preamble ≝ (\fst program)
1516 letin data_labels ≝ (construct_datalabels preamble)
1517 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
1518 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1519 whd in ⊢ (% → %)
1520 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
1521 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
1522 generalize in match (fetch_assembly_pseudo program ppc
1523  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
1524  (load_code_memory assembled));
1525 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
1526 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
1527 normalize nodelta in EXPAND; (* HERE *)
1528 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
1529 >bitvector_of_nat_nat_of_bitvector in H1; #H1
1530 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
1531 #H1 #H2
1532 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
1533 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
1534  [ #K3 % [2: % [% | @K3]] | @K1 ]
1535qed.
1536
1537(* OLD?
1538definition assembly_specification:
1539  ∀assembly_program: pseudo_assembly_program.
1540  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1541  λpseudo_assembly_program.
1542  λcode_mem.
1543    ∀pc: Word.
1544      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1545      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1546      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1547      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1548      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1549       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1550      match pre_assembled with
1551       [ None ⇒ True
1552       | Some pc_code ⇒
1553          let 〈new_pc,code〉 ≝ pc_code in
1554           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1555
1556axiom assembly_meets_specification:
1557  ∀pseudo_assembly_program.
1558    match assembly pseudo_assembly_program with
1559    [ None ⇒ True
1560    | Some code_mem_cost ⇒
1561      let 〈code_mem, cost〉 ≝ code_mem_cost in
1562        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1563    ].
1564(*
1565  # PROGRAM
1566  [ cases PROGRAM
1567    # PREAMBLE
1568    # INSTR_LIST
1569    elim INSTR_LIST
1570    [ whd
1571      whd in ⊢ (∀_. %)
1572      # PC
1573      whd
1574    | # INSTR
1575      # INSTR_LIST_TL
1576      # H
1577      whd
1578      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1579    ]
1580  | cases not_implemented
1581  ] *)
1582*)
1583
1584definition internal_pseudo_address_map ≝ list (BitVector 8).
1585
1586axiom low_internal_ram_of_pseudo_low_internal_ram:
1587 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1588
1589axiom high_internal_ram_of_pseudo_high_internal_ram:
1590 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1591
1592axiom low_internal_ram_of_pseudo_internal_ram_hit:
1593 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
1594  member ? (eq_bv 8) (false:::addr) M = true →
1595   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1596   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1597   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1598   let bl ≝ lookup ? 7 addr ram (zero 8) in
1599   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1600    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
1601
1602(* changed from add to sub *)
1603axiom low_internal_ram_of_pseudo_internal_ram_miss:
1604 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
1605  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1606  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1607  let carr ≝ get_index_v ? ? flags 1 ? in
1608  carr = false →
1609  member ? (eq_bv 8) (false:::Saddr) M = false →
1610   member ? (eq_bv 8) (false:::addr) M = false →
1611    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1612  //
1613qed.
1614
1615definition addressing_mode_ok ≝
1616 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
1617  λaddr:addressing_mode.
1618   match addr with
1619    [ DIRECT d ⇒
1620       ¬(member ? (eq_bv 8) d M) ∧
1621       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1622    | INDIRECT i ⇒
1623       let d ≝ get_register ? s [[false;false;i]] in
1624       ¬(member ? (eq_bv 8) d M) ∧
1625       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1626    | EXT_INDIRECT _ ⇒ true
1627    | REGISTER _ ⇒ true
1628    | ACC_A ⇒ true
1629    | ACC_B ⇒ true
1630    | DPTR ⇒ true
1631    | DATA _ ⇒ true
1632    | DATA16 _ ⇒ true
1633    | ACC_DPTR ⇒ true
1634    | ACC_PC ⇒ true
1635    | EXT_INDIRECT_DPTR ⇒ true
1636    | INDIRECT_DPTR ⇒ true
1637    | CARRY ⇒ true
1638    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1639    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1640    | RELATIVE _ ⇒ true
1641    | ADDR11 _ ⇒ true
1642    | ADDR16 _ ⇒ true ].
1643   
1644definition next_internal_pseudo_address_map0 ≝
1645  λT.
1646  λfetched.
1647  λM: internal_pseudo_address_map.
1648  λs: PreStatus T.
1649   match fetched with
1650    [ Comment _ ⇒ Some ? M
1651    | Cost _ ⇒ Some … M
1652    | Jmp _ ⇒ Some … M
1653    | Call _ ⇒
1654       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1655    | Mov _ _ ⇒ Some … M
1656    | Instruction instr ⇒
1657       match instr with
1658        [ ADD addr1 addr2 ⇒
1659           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1660            Some ? M
1661           else
1662            None ?
1663        | ADDC addr1 addr2 ⇒
1664           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1665            Some ? M
1666           else
1667            None ?
1668        | SUBB addr1 addr2 ⇒
1669           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1670            Some ? M
1671           else
1672            None ?       
1673        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1674 
1675
1676definition next_internal_pseudo_address_map ≝
1677 λM:internal_pseudo_address_map.
1678  λs:PseudoStatus.
1679    next_internal_pseudo_address_map0 ?
1680     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1681   
1682definition status_of_pseudo_status:
1683 internal_pseudo_address_map → PseudoStatus → option Status ≝
1684 λM,ps.
1685  let pap ≝ code_memory … ps in
1686   match assembly pap with
1687    [ None ⇒ None …
1688    | Some p ⇒
1689       let cm ≝ load_code_memory (\fst p) in
1690       let pc ≝ sigma pap (program_counter ? ps) in
1691       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1692       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1693        Some …
1694         (mk_PreStatus (BitVectorTrie Byte 16)
1695           cm
1696           lir
1697           hir
1698           (external_ram … ps)
1699           pc
1700           (special_function_registers_8051 … ps)
1701           (special_function_registers_8052 … ps)
1702           (p1_latch … ps)
1703           (p3_latch … ps)
1704           (clock … ps)) ].
1705
1706(*
1707definition write_at_stack_pointer':
1708 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1709  λM: Type[0].
1710  λs: PreStatus M.
1711  λv: Byte.
1712    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1713    let bit_zero ≝ get_index_v… nu O ? in
1714    let bit_1 ≝ get_index_v… nu 1 ? in
1715    let bit_2 ≝ get_index_v… nu 2 ? in
1716    let bit_3 ≝ get_index_v… nu 3 ? in
1717      if bit_zero then
1718        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1719                              v (low_internal_ram ? s) in
1720          set_low_internal_ram ? s memory
1721      else
1722        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1723                              v (high_internal_ram ? s) in
1724          set_high_internal_ram ? s memory.
1725  [ cases l0 %
1726  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1727qed.
1728
1729definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1730 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1731
1732  λticks_of.
1733  λs.
1734  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1735  let ticks ≝ ticks_of (program_counter ? s) in
1736  let s ≝ set_clock ? s (clock ? s + ticks) in
1737  let s ≝ set_program_counter ? s pc in
1738    match instr with
1739    [ Instruction instr ⇒
1740       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1741    | Comment cmt ⇒ s
1742    | Cost cst ⇒ s
1743    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1744    | Call call ⇒
1745      let a ≝ address_of_word_labels s call in
1746      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1747      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1748      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1749      let s ≝ write_at_stack_pointer' ? s pc_bl in
1750      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1751      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1752      let s ≝ write_at_stack_pointer' ? s pc_bu in
1753        set_program_counter ? s a
1754    | Mov dptr ident ⇒
1755       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1756    ].
1757 [
1758 |2,3,4: %
1759 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1760 |
1761 | %
1762 ]
1763 cases not_implemented
1764qed.
1765*)
1766
1767axiom execute_1_pseudo_instruction_preserves_code_memory:
1768 ∀ticks_of,ps.
1769  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1770
1771(*
1772lemma execute_code_memory_unchanged:
1773 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1774 #ticks #ps whd in ⊢ (??? (??%))
1775 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1776  (program_counter pseudo_assembly_program ps)) #instr #pc
1777 whd in ⊢ (??? (??%)) cases instr
1778  [ #pre cases pre
1779     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1780       cases (split ????) #z1 #z2 %
1781     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1782       cases (split ????) #z1 #z2 %
1783     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1784       cases (split ????) #z1 #z2 %
1785     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1786       [ #x1 whd in ⊢ (??? (??%))
1787     | *: cases not_implemented
1788     ]
1789  | #comment %
1790  | #cost %
1791  | #label %
1792  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1793    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1794    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1795    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1796    (* CSC: ??? *)
1797  | #dptr #label (* CSC: ??? *)
1798  ]
1799  cases not_implemented
1800qed.
1801*)
1802
1803lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1804 ∀M:internal_pseudo_address_map.
1805 ∀ps,ps': PseudoStatus.
1806  code_memory … ps = code_memory … ps' →
1807   match status_of_pseudo_status M ps with
1808    [ None ⇒ status_of_pseudo_status M ps' = None …
1809    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
1810    ].
1811 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1812 generalize in match (refl … (assembly (code_memory … ps)))
1813 cases (assembly ?) in ⊢ (???% → %)
1814  [ #K whd whd in ⊢ (??%?) <H >K %
1815  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1816qed.
1817
1818definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
1819  λprogram: pseudo_assembly_program.
1820  λppc: Word.
1821  λfetched.
1822    match fetched with
1823    [ Instruction instr ⇒
1824      match instr with
1825      [ JC lbl ⇒
1826        match jump_expansion ppc program with
1827        [ short_jump ⇒ 〈2, 2〉
1828        | medium_jump ⇒ ?
1829        | long_jump ⇒ 〈4, 4〉
1830        ]
1831      | JNC lbl ⇒
1832        match jump_expansion ppc program with
1833        [ short_jump ⇒ 〈2, 2〉
1834        | medium_jump ⇒ ?
1835        | long_jump ⇒ 〈4, 4〉
1836        ]
1837      | JB bit lbl ⇒
1838        match jump_expansion ppc program with
1839        [ short_jump ⇒ 〈2, 2〉
1840        | medium_jump ⇒ ?
1841        | long_jump ⇒ 〈4, 4〉
1842        ]
1843      | JNB bit lbl ⇒
1844        match jump_expansion ppc program with
1845        [ short_jump ⇒ 〈2, 2〉
1846        | medium_jump ⇒ ?
1847        | long_jump ⇒ 〈4, 4〉
1848        ]
1849      | JBC bit lbl ⇒
1850        match jump_expansion ppc program with
1851        [ short_jump ⇒ 〈2, 2〉
1852        | medium_jump ⇒ ?
1853        | long_jump ⇒ 〈4, 4〉
1854        ]
1855      | JZ lbl ⇒
1856        match jump_expansion ppc program with
1857        [ short_jump ⇒ 〈2, 2〉
1858        | medium_jump ⇒ ?
1859        | long_jump ⇒ 〈4, 4〉
1860        ]
1861      | JNZ lbl ⇒
1862        match jump_expansion ppc program with
1863        [ short_jump ⇒ 〈2, 2〉
1864        | medium_jump ⇒ ?
1865        | long_jump ⇒ 〈4, 4〉
1866        ]
1867      | CJNE arg lbl ⇒
1868        match jump_expansion ppc program with
1869        [ short_jump ⇒ 〈2, 2〉
1870        | medium_jump ⇒ ?
1871        | long_jump ⇒ 〈4, 4〉
1872        ]
1873      | DJNZ arg lbl ⇒
1874        match jump_expansion ppc program with
1875        [ short_jump ⇒ 〈2, 2〉
1876        | medium_jump ⇒ ?
1877        | long_jump ⇒ 〈4, 4〉
1878        ]
1879      | ADD arg1 arg2 ⇒
1880        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1881         〈ticks, ticks〉
1882      | ADDC arg1 arg2 ⇒
1883        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1884         〈ticks, ticks〉
1885      | SUBB arg1 arg2 ⇒
1886        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1887         〈ticks, ticks〉
1888      | INC arg ⇒
1889        let ticks ≝ ticks_of_instruction (INC ? arg) in
1890         〈ticks, ticks〉
1891      | DEC arg ⇒
1892        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1893         〈ticks, ticks〉
1894      | MUL arg1 arg2 ⇒
1895        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1896         〈ticks, ticks〉
1897      | DIV arg1 arg2 ⇒
1898        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1899         〈ticks, ticks〉
1900      | DA arg ⇒
1901        let ticks ≝ ticks_of_instruction (DA ? arg) in
1902         〈ticks, ticks〉
1903      | ANL arg ⇒
1904        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1905         〈ticks, ticks〉
1906      | ORL arg ⇒
1907        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1908         〈ticks, ticks〉
1909      | XRL arg ⇒
1910        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1911         〈ticks, ticks〉
1912      | CLR arg ⇒
1913        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1914         〈ticks, ticks〉
1915      | CPL arg ⇒
1916        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1917         〈ticks, ticks〉
1918      | RL arg ⇒
1919        let ticks ≝ ticks_of_instruction (RL ? arg) in
1920         〈ticks, ticks〉
1921      | RLC arg ⇒
1922        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1923         〈ticks, ticks〉
1924      | RR arg ⇒
1925        let ticks ≝ ticks_of_instruction (RR ? arg) in
1926         〈ticks, ticks〉
1927      | RRC arg ⇒
1928        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1929         〈ticks, ticks〉
1930      | SWAP arg ⇒
1931        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1932         〈ticks, ticks〉
1933      | MOV arg ⇒
1934        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1935         〈ticks, ticks〉
1936      | MOVX arg ⇒
1937        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1938         〈ticks, ticks〉
1939      | SETB arg ⇒
1940        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1941         〈ticks, ticks〉
1942      | PUSH arg ⇒
1943        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1944         〈ticks, ticks〉
1945      | POP arg ⇒
1946        let ticks ≝ ticks_of_instruction (POP ? arg) in
1947         〈ticks, ticks〉
1948      | XCH arg1 arg2 ⇒
1949        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1950         〈ticks, ticks〉
1951      | XCHD arg1 arg2 ⇒
1952        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1953         〈ticks, ticks〉
1954      | RET ⇒
1955        let ticks ≝ ticks_of_instruction (RET ?) in
1956         〈ticks, ticks〉
1957      | RETI ⇒
1958        let ticks ≝ ticks_of_instruction (RETI ?) in
1959         〈ticks, ticks〉
1960      | NOP ⇒
1961        let ticks ≝ ticks_of_instruction (NOP ?) in
1962         〈ticks, ticks〉
1963      ]
1964    | Comment comment ⇒ 〈0, 0〉
1965    | Cost cost ⇒ 〈0, 0〉
1966    | Jmp jmp ⇒ 〈2, 2〉
1967    | Call call ⇒ 〈2, 2〉
1968    | Mov dptr tgt ⇒ 〈2, 2〉
1969    ].
1970  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1971qed.
1972
1973definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
1974  λprogram: pseudo_assembly_program.
1975  λppc: Word.
1976    let 〈preamble, pseudo〉 ≝ program in
1977    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1978     ticks_of0 program ppc fetched.
1979
1980lemma get_register_set_program_counter:
1981 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1982 #T #s #pc %
1983qed.
1984
1985lemma get_8051_sfr_set_program_counter:
1986 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1987 #T #s #pc %
1988qed.
1989
1990lemma get_bit_addressable_sfr_set_program_counter:
1991 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1992 #T #s #pc %
1993qed.
1994
1995lemma low_internal_ram_set_program_counter:
1996 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1997 #T #s #pc %
1998qed.
1999
2000lemma get_arg_8_set_program_counter:
2001 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
2002  ∀T,s,pc,b.∀arg:l.
2003   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
2004 [2,3: cases arg; *; normalize //]
2005 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
2006qed.
2007
2008lemma set_bit_addressable_sfr_set_code_memory:
2009  ∀T, U: Type[0].
2010  ∀ps: PreStatus ?.
2011  ∀code_mem.
2012  ∀x.
2013  ∀val.
2014  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
2015  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
2016  #T #U #ps #code_mem #x #val
2017  whd in ⊢ (??%?)
2018  whd in ⊢ (???(???%?))
2019  cases (eqb ? 128) [ normalize nodelta cases not_implemented
2020  | normalize nodelta
2021  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
2022  | normalize nodelta
2023  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
2024  | normalize nodelta
2025  cases (eqb ? 176) [ normalize nodelta %
2026  | normalize nodelta
2027  cases (eqb ? 153) [ normalize nodelta %
2028  | normalize nodelta
2029  cases (eqb ? 138) [ normalize nodelta %
2030  | normalize nodelta
2031  cases (eqb ? 139) [ normalize nodelta %
2032  | normalize nodelta
2033  cases (eqb ? 140) [ normalize nodelta %
2034  | normalize nodelta
2035  cases (eqb ? 141) [ normalize nodelta %
2036  | normalize nodelta
2037  cases (eqb ? 200) [ normalize nodelta %
2038  | normalize nodelta
2039  cases (eqb ? 202) [ normalize nodelta %
2040  | normalize nodelta
2041  cases (eqb ? 203) [ normalize nodelta %
2042  | normalize nodelta
2043  cases (eqb ? 204) [ normalize nodelta %
2044  | normalize nodelta
2045  cases (eqb ? 205) [ normalize nodelta %
2046  | normalize nodelta
2047  cases (eqb ? 135) [ normalize nodelta %
2048  | normalize nodelta
2049  cases (eqb ? 136) [ normalize nodelta %
2050  | normalize nodelta
2051  cases (eqb ? 137) [ normalize nodelta %
2052  | normalize nodelta
2053  cases (eqb ? 152) [ normalize nodelta %
2054  | normalize nodelta
2055  cases (eqb ? 168) [ normalize nodelta %
2056  | normalize nodelta
2057  cases (eqb ? 184) [ normalize nodelta %
2058  | normalize nodelta
2059  cases (eqb ? 129) [ normalize nodelta %
2060  | normalize nodelta
2061  cases (eqb ? 130) [ normalize nodelta %
2062  | normalize nodelta
2063  cases (eqb ? 131) [ normalize nodelta %
2064  | normalize nodelta
2065  cases (eqb ? 208) [ normalize nodelta %
2066  | normalize nodelta
2067  cases (eqb ? 224) [ normalize nodelta %
2068  | normalize nodelta
2069  cases (eqb ? 240) [ normalize nodelta %
2070  | normalize nodelta
2071    cases not_implemented
2072  ]]]]]]]]]]]]]]]]]]]]]]]]]]
2073qed.
2074
2075lemma set_arg_8_set_code_memory:
2076  ∀n:nat.
2077  ∀l:Vector addressing_mode_tag (S n).
2078    ¬(is_in ? l ACC_PC) →
2079    ∀T: Type[0].
2080    ∀U: Type[0].
2081    ∀ps: PreStatus ?.
2082    ∀code_mem.
2083    ∀val.
2084    ∀b: l.
2085  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
2086  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
2087  [2,3: cases b; *; normalize //]
2088  #n #l #prf #T #U #ps #code_mem #val * *;
2089  [*:
2090    [1,2,3,4,8,9,15,16,17,18,19: #x]
2091    try #y whd in ⊢ (??(%)?)
2092    whd in ⊢ (???(???(%)?))
2093    [1,2:
2094      cases (split bool 4 4 ?)
2095      #nu' #nl'
2096      normalize nodelta
2097      cases (split bool 1 3 nu')
2098      #bit1' #ignore'
2099      normalize nodelta
2100      cases (get_index_v bool 4 nu' 0 ?)
2101      [1,2,3,4:
2102        normalize nodelta
2103        try %
2104        try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
2105        try (normalize in ⊢ (???(???%?)))
2106      ]
2107    |3,4: %
2108    |*:
2109       try normalize nodelta
2110       normalize cases (not_implemented)
2111    ]
2112 ]
2113 
2114
2115qed.
2116
2117axiom set_arg_8_set_program_counter:
2118  ∀n:nat.
2119  ∀l:Vector addressing_mode_tag (S n).
2120    ¬(is_in ? l ACC_PC) →
2121    ∀T: Type[0].
2122    ∀ps: PreStatus ?.
2123    ∀pc.
2124    ∀val.
2125    ∀b: l.
2126  set_arg_8 ? (set_program_counter T ps pc) b val =
2127  set_program_counter T (set_arg_8 ? ps b val) pc.
2128  [1,2: cases b; *; normalize //]
2129qed.
2130 
2131
2132lemma get_arg_8_set_code_memory:
2133 ∀T1,T2,s,code_mem,b,arg.
2134   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
2135 #T1 #T2 #s #code_mem #b #arg %
2136qed.
2137
2138lemma set_code_memory_set_flags:
2139 ∀T1,T2,s,f1,f2,f3,code_mem.
2140  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
2141   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
2142 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
2143qed.
2144
2145lemma set_program_counter_set_flags:
2146 ∀T1,s,f1,f2,f3,pc.
2147  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
2148   set_flags … (set_program_counter … s pc) f1 f2 f3.
2149 #T1 #s #f1 #f2 #f3 #pc  %
2150qed.
2151
2152lemma program_counter_set_flags:
2153 ∀T1,s,f1,f2,f3.
2154  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
2155 #T1 #s #f1 #f2 #f3 %
2156qed.
2157
2158lemma special_function_registers_8051_write_at_stack_pointer:
2159 ∀T,s,x.
2160    special_function_registers_8051 T (write_at_stack_pointer T s x)
2161  = special_function_registers_8051 T s.
2162 #T #s #x whd in ⊢ (??(??%)?)
2163 cases (split ????) #nu #nl normalize nodelta;
2164 cases (get_index_v bool ????) %
2165qed.
2166
2167lemma get_8051_sfr_write_at_stack_pointer:
2168 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
2169 #T #s #x #y whd in ⊢ (??%%) //
2170qed.
2171
2172lemma code_memory_write_at_stack_pointer:
2173 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
2174 #T #s #x whd in ⊢ (??(??%)?)
2175 cases (split ????) #nu #nl normalize nodelta;
2176 cases (get_index_v bool ????) %
2177qed.
2178
2179axiom low_internal_ram_write_at_stack_pointer:
2180 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2181  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2182  low_internal_ram ? s2 = low_internal_ram T2 s3 →
2183  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2184  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2185  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
2186   low_internal_ram T1
2187     (write_at_stack_pointer ?
2188       (set_8051_sfr ?
2189         (write_at_stack_pointer ?
2190           (set_8051_sfr ?
2191             (set_low_internal_ram ? s1
2192               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
2193             SFR_SP sp1)
2194          bl)
2195        SFR_SP sp2)
2196      bu)
2197   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
2198      (low_internal_ram ?
2199       (write_at_stack_pointer ?
2200         (set_8051_sfr ?
2201           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2202          SFR_SP sp2)
2203        pbu)).
2204       
2205axiom high_internal_ram_write_at_stack_pointer:
2206 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2207  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2208  high_internal_ram ? s2 = high_internal_ram T2 s3 →
2209  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2210  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2211  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
2212   high_internal_ram T1
2213     (write_at_stack_pointer ?
2214       (set_8051_sfr ?
2215         (write_at_stack_pointer ?
2216           (set_8051_sfr ?
2217             (set_high_internal_ram ? s1
2218               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
2219             SFR_SP sp1)
2220          bl)
2221        SFR_SP sp2)
2222      bu)
2223   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2224      (high_internal_ram ?
2225       (write_at_stack_pointer ?
2226         (set_8051_sfr ?
2227           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2228          SFR_SP sp2)
2229        pbu)).
2230
2231lemma set_program_counter_set_low_internal_ram:
2232 ∀T,s,x,y.
2233  set_program_counter T (set_low_internal_ram … s x) y =
2234   set_low_internal_ram … (set_program_counter … s y) x.
2235 //
2236qed.
2237
2238lemma set_clock_set_low_internal_ram:
2239 ∀T,s,x,y.
2240  set_clock T (set_low_internal_ram … s x) y =
2241   set_low_internal_ram … (set_clock … s y) x.
2242 //
2243qed.
2244
2245lemma set_program_counter_set_high_internal_ram:
2246 ∀T,s,x,y.
2247  set_program_counter T (set_high_internal_ram … s x) y =
2248   set_high_internal_ram … (set_program_counter … s y) x.
2249 //
2250qed.
2251
2252lemma set_clock_set_high_internal_ram:
2253 ∀T,s,x,y.
2254  set_clock T (set_high_internal_ram … s x) y =
2255   set_high_internal_ram … (set_clock … s y) x.
2256 //
2257qed.
2258
2259lemma set_low_internal_ram_set_high_internal_ram:
2260 ∀T,s,x,y.
2261  set_low_internal_ram T (set_high_internal_ram … s x) y =
2262   set_high_internal_ram … (set_low_internal_ram … s y) x.
2263 //
2264qed.
2265
2266lemma external_ram_write_at_stack_pointer:
2267 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
2268 #T #s #x whd in ⊢ (??(??%)?)
2269 cases (split ????) #nu #nl normalize nodelta;
2270 cases (get_index_v bool ????) %
2271qed.
2272
2273lemma special_function_registers_8052_write_at_stack_pointer:
2274 ∀T,s,x.
2275    special_function_registers_8052 T (write_at_stack_pointer T s x)
2276  = special_function_registers_8052 T s.
2277 #T #s #x whd in ⊢ (??(??%)?)
2278 cases (split ????) #nu #nl normalize nodelta;
2279 cases (get_index_v bool ????) %
2280qed.
2281
2282lemma p1_latch_write_at_stack_pointer:
2283 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
2284 #T #s #x whd in ⊢ (??(??%)?)
2285 cases (split ????) #nu #nl normalize nodelta;
2286 cases (get_index_v bool ????) %
2287qed.
2288
2289lemma p3_latch_write_at_stack_pointer:
2290 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
2291 #T #s #x whd in ⊢ (??(??%)?)
2292 cases (split ????) #nu #nl normalize nodelta;
2293 cases (get_index_v bool ????) %
2294qed.
2295
2296lemma clock_write_at_stack_pointer:
2297 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
2298 #T #s #x whd in ⊢ (??(??%)?)
2299 cases (split ????) #nu #nl normalize nodelta;
2300 cases (get_index_v bool ????) %
2301qed.
2302
2303axiom get_index_v_set_index:
2304 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
2305
2306lemma get_8051_sfr_set_8051_sfr:
2307 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
2308 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
2309 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
2310qed.
2311
2312lemma program_counter_set_8051_sfr:
2313 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
2314 //
2315qed.
2316
2317lemma eq_rect_Type1_r:
2318  ∀A: Type[1].
2319  ∀a:A.
2320  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2321  #A #a #P #H #x #p
2322  generalize in match H
2323  generalize in match P
2324  cases p
2325  //
2326qed.
2327
2328lemma split_eq_status:
2329 ∀T.
2330 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
2331 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
2332  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
2333   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
2334   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
2335 //
2336qed.
2337
2338axiom pair_elim':
2339  ∀A,B,C: Type[0].
2340  ∀T: A → B → C.
2341  ∀p.
2342  ∀P: A×B → C → Prop.
2343    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
2344      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
2345
2346axiom pair_elim'':
2347  ∀A,B,C,C': Type[0].
2348  ∀T: A → B → C.
2349  ∀T': A → B → C'.
2350  ∀p.
2351  ∀P: A×B → C → C' → Prop.
2352    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
2353      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
2354
2355axiom split_elim':
2356  ∀A: Type[0].
2357  ∀B: Type[1].
2358  ∀l, m, v.
2359  ∀T: Vector A l → Vector A m → B.
2360  ∀P: B → Prop.
2361    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
2362      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
2363
2364axiom split_elim'':
2365  ∀A: Type[0].
2366  ∀B,B': Type[1].
2367  ∀l, m, v.
2368  ∀T: Vector A l → Vector A m → B.
2369  ∀T': Vector A l → Vector A m → B'.
2370  ∀P: B → B' → Prop.
2371    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
2372      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
2373        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
2374
2375axiom split_append:
2376  ∀A: Type[0].
2377  ∀m, n: nat.
2378  ∀v, v': Vector A m.
2379  ∀q, q': Vector A n.
2380    let 〈v', q'〉 ≝ split A m n (v@@q) in
2381      v = v' ∧ q = q'.
2382
2383axiom split_vector_singleton:
2384  ∀A: Type[0].
2385  ∀n: nat.
2386  ∀v: Vector A (S n).
2387  ∀rest: Vector A n.
2388  ∀s: Vector A 1.
2389  ∀prf.
2390    v = s @@ rest →
2391    ((get_index_v A ? v 0 prf) ::: rest) = v.
2392
2393axiom sub_minus_one_seven_eight:
2394  ∀v: BitVector 7.
2395  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
2396  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
2397
2398lemma pair_destruct_1:
2399 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
2400 #A #B #a #b *; /2/
2401qed.
2402
2403lemma pair_destruct_2:
2404 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
2405 #A #B #a #b *; /2/
2406qed.
2407
2408(*
2409lemma blah:
2410  ∀m: internal_pseudo_address_map.
2411  ∀s: PseudoStatus.
2412  ∀arg: Byte.
2413  ∀b: bool.
2414    addressing_mode_ok m s (DIRECT arg) = true →
2415      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2416      get_arg_8 ? s b (DIRECT arg).
2417  [2, 3: normalize % ]
2418  #m #s #arg #b #hyp
2419  whd in ⊢ (??%%)
2420  @split_elim''
2421  #nu' #nl' #arg_nu_nl_eq
2422  normalize nodelta
2423  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2424  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2425  #get_index_v_eq
2426  normalize nodelta
2427  [2:
2428    normalize nodelta
2429    @split_elim''
2430    #bit_one' #three_bits' #bit_one_three_bit_eq
2431    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2432    normalize nodelta
2433    generalize in match (refl ? (sub_7_with_carry ? ? ?))
2434    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2435    #Saddr #carr' #Saddr_carr_eq
2436    normalize nodelta
2437    #carr_hyp'
2438    @carr_hyp'
2439    [1:
2440    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2441        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2442        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2443        #member_eq
2444        normalize nodelta
2445        [2: #destr destruct(destr)
2446        |1: -carr_hyp';
2447            >arg_nu_nl_eq
2448            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2449            [1: >get_index_v_eq in ⊢ (??%? → ?)
2450            |2: @le_S @le_S @le_S @le_n
2451            ]
2452            cases (member (BitVector 8) ? (\fst ?) ?)
2453            [1: #destr normalize in destr; destruct(destr)
2454            |2:
2455            ]
2456        ]
2457    |3: >get_index_v_eq in ⊢ (??%?)
2458        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2459        >(split_vector_singleton … bit_one_three_bit_eq)
2460        <arg_nu_nl_eq
2461        whd in hyp:(??%?)
2462        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2463        normalize nodelta [*: #ignore @sym_eq ]
2464    ]
2465  |
2466  ].
2467*)
2468(*
2469map_address0 ... (DIRECT arg) = Some .. →
2470  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2471  get_arg_8 (internal_ram ...) (DIRECT arg)
2472
2473((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
2474                     then Some internal_pseudo_address_map M 
2475                     else None internal_pseudo_address_map )
2476                    =Some internal_pseudo_address_map M')
2477*)
2478
2479lemma main_thm:
2480 ∀M,M',ps,s,s''.
2481  next_internal_pseudo_address_map M ps = Some … M' →
2482  status_of_pseudo_status M ps = Some … s →
2483  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
2484   ∃n. execute n s = s''.
2485 #M #M' #ps #s #s''
2486 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
2487 whd in ⊢ (? → ? → ??%? → ??%? → ?)
2488 >execute_1_pseudo_instruction_preserves_code_memory
2489 generalize in match (refl … (assembly (code_memory … ps)))
2490 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
2491 cases (build_maps (code_memory … ps))
2492  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
2493    #abs @⊥ normalize in abs; destruct (abs) ]
2494 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
2495 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
2496 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
2497  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
2498 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
2499 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
2500 #MAP
2501 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
2502 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
2503 change with
2504  (∃n.
2505    execute n
2506     (set_low_internal_ram ?
2507       (set_high_internal_ram ?
2508         (set_program_counter ?
2509           (set_code_memory ?? ps (load_code_memory assembled))
2510          (sigma 〈preamble,instr_list〉 (program_counter ? ps)))
2511        (high_internal_ram_of_pseudo_high_internal_ram M ?))
2512      (low_internal_ram_of_pseudo_low_internal_ram M ?))
2513   = set_low_internal_ram ?
2514      (set_high_internal_ram ?
2515        (set_program_counter ?
2516          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
2517         (sigma ??))
2518       ?)
2519     ?)
2520 whd in match (\snd 〈preamble,instr_list〉) in H;
2521 whd in match (\fst 〈preamble,instr_list〉) in H;
2522 whd in match (\snd 〈final_pc,assembled〉) in H;
2523 whd in match (\snd 〈preamble,instr_list〉) in MAP;
2524 -s s'' labels costs final_ppc final_pc;
2525 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
2526 (* NICE STATEMENT HERE *)
2527 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
2528 #K <K generalize in match K; -K;
2529 (* STATEMENT WITH EQUALITY HERE *)
2530 whd in ⊢ (???(?%?) → ?)
2531 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
2532 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
2533 #pi #newppc normalize nodelta; #MAP * #instructions *;
2534 cases pi in MAP; normalize nodelta;
2535  [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
2536    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
2537    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2538    #H2 >(eq_bv_to_eq … H2) >EQ %
2539(*  |6: (* Mov *) #arg1 #arg2
2540       #H1 #H2 #EQ %[@1]
2541       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2542       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2543       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2544       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2545       >H2b >(eq_instruction_to_eq … H2a)
2546       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2547       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2548       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2549       normalize nodelta;
2550       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2551       #result #flags
2552       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
2553  |5: (* Call *) #label #MAP
2554      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
2555      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
2556       [ (* short *) #abs @⊥ destruct (abs)
2557       |3: (* long *) #H1 #H2 #EQ %[@1]
2558           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2559           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2560           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2561           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2562           >H2b >(eq_instruction_to_eq … H2a)
2563           generalize in match EQ; -EQ;
2564           whd in ⊢ (???% → ??%?);
2565           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
2566           >(eq_bv_to_eq … H2c)
2567           change with
2568            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
2569                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2570           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
2571           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
2572           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
2573           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
2574           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
2575           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2576           @split_eq_status;
2577            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
2578              >code_memory_write_at_stack_pointer %
2579            | >set_program_counter_set_low_internal_ram
2580              >set_clock_set_low_internal_ram
2581              @low_internal_ram_write_at_stack_pointer
2582               [ % | %
2583               | @(pair_destruct_2 … EQ1)
2584               | @(pair_destruct_2 … EQ2)
2585               | >(pair_destruct_1 ????? EQpc)
2586                 >(pair_destruct_2 ????? EQpc)
2587                 @split_elim #x #y #H <H -x y H;
2588                 >(pair_destruct_1 ????? EQppc)
2589                 >(pair_destruct_2 ????? EQppc)
2590                 @split_elim #x #y #H <H -x y H;
2591                 >EQ0 % ]
2592            | >set_low_internal_ram_set_high_internal_ram
2593              >set_program_counter_set_high_internal_ram
2594              >set_clock_set_high_internal_ram
2595              @high_internal_ram_write_at_stack_pointer
2596               [ % | %
2597               | @(pair_destruct_2 … EQ1)
2598               | @(pair_destruct_2 … EQ2)
2599               | >(pair_destruct_1 ????? EQpc)
2600                 >(pair_destruct_2 ????? EQpc)
2601                 @split_elim #x #y #H <H -x y H;
2602                 >(pair_destruct_1 ????? EQppc)
2603                 >(pair_destruct_2 ????? EQppc)
2604                 @split_elim #x #y #H <H -x y H;
2605                 >EQ0 % ]           
2606            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
2607              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2608              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2609              >external_ram_write_at_stack_pointer %
2610            | change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
2611              >EQ0 %
2612            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
2613              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2614              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2615              >special_function_registers_8051_write_at_stack_pointer %
2616            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
2617              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2618              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2619              >special_function_registers_8052_write_at_stack_pointer %
2620            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
2621              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2622              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2623              >p1_latch_write_at_stack_pointer %
2624            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
2625              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2626              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2627              >p3_latch_write_at_stack_pointer %
2628            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
2629              >clock_write_at_stack_pointer whd in ⊢ (???%)
2630              >clock_write_at_stack_pointer whd in ⊢ (???%)
2631              >clock_write_at_stack_pointer %]
2632       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2633         @pair_elim' #fst_5_addr #rest_addr #EQ1
2634         @pair_elim' #fst_5_pc #rest_pc #EQ2
2635         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2636         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2637         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2638         change in ⊢ (? →??%?) with (execute_1_0 ??)
2639         @pair_elim' * #instr #newppc' #ticks #EQn
2640          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
2641          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2642          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
2643          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
2644          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
2645          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
2646          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
2647          >get_8051_sfr_set_8051_sfr
2648         
2649          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
2650           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2651           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2652           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2653           generalize in match (refl … (split bool 4 4 pc_bu))
2654           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2655           generalize in match (refl … (split bool 3 8 rest_addr))
2656           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2657           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2658           generalize in match
2659            (refl …
2660             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2661             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2662           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2663           @split_eq_status try %
2664            [ change with (? = sigma ? (address_of_word_labels ps label))
2665              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2666            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2667              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
2668  |4: (* Jmp *) #label #MAP
2669      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
2670      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
2671       [3: (* long *) #H1 #H2 #EQ %[@1]
2672           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2673           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2674           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2675           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2676           >H2b >(eq_instruction_to_eq … H2a)
2677           generalize in match EQ; -EQ;
2678           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2679           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2680       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2681           generalize in match
2682            (refl ?
2683             (sub_16_with_carry
2684              (sigma 〈preamble,instr_list〉 (program_counter … ps))
2685              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
2686              false))
2687           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2688           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2689           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2690           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2691           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2692           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2693           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2694           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2695           >H2b >(eq_instruction_to_eq … H2a)
2696           generalize in match EQ; -EQ;
2697           whd in ⊢ (???% → ?);
2698           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2699           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
2700           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
2701           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2702           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
2703           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2704       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2705         generalize in match
2706          (refl …
2707            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
2708         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2709         generalize in match
2710          (refl …
2711            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
2712         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2713         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2714         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2715         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2716         change in ⊢ (? →??%?) with (execute_1_0 ??)
2717           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2718           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2719           >H2b >(eq_instruction_to_eq … H2a)
2720           generalize in match EQ; -EQ;
2721           whd in ⊢ (???% → ?);
2722           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
2723           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2724           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2725           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2726           generalize in match (refl … (split bool 4 4 pc_bu))
2727           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2728           generalize in match (refl … (split bool 3 8 rest_addr))
2729           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2730           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2731           generalize in match
2732            (refl …
2733             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2734             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2735           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
2736           @split_eq_status try %
2737            [ change with (? = sigma ? (address_of_word_labels ps label))
2738              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2739            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2740              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2741  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
2742    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2743       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2744       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2745       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2746       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2747       >H2b >(eq_instruction_to_eq … H2a)
2748       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2749       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2750       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2751       normalize nodelta; #MAP;
2752       [1: change in ⊢ (? → %) with
2753        ((let 〈result,flags〉 ≝
2754          add_8_with_carry
2755           (get_arg_8 ? ps false ACC_A)
2756           (get_arg_8 ?
2757             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2758             false (DIRECT ARG2))
2759           ? in ?) = ?)
2760       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
2761        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
2762       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2763       #result #flags
2764       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
2765    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2766       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2767       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2768       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2769       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2770       >H2b >(eq_instruction_to_eq … H2a)
2771       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2772       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2773       [1,2,3,4: cases (half_add ???) #carry #result
2774       | cases (half_add ???) #carry #bl normalize nodelta;
2775         cases (full_add ????) #carry' #bu normalize nodelta ]
2776        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
2777        [5: %
2778        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2779      (set_program_counter pseudo_assembly_program ps newppc)
2780      (\fst  (ticks_of0 〈preamble,instr_list〉
2781                   (program_counter pseudo_assembly_program ps)
2782                   (Instruction (INC Identifier (DIRECT ARG))))
2783       +clock pseudo_assembly_program
2784        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2785        [2,3: // ]
2786            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2787            whd in ⊢ (??%%)
2788            cases (split bool 4 4 ARG)
2789            #nu' #nl'
2790            normalize nodelta
2791            cases (split bool 1 3 nu')
2792            #bit_1' #ignore'
2793            normalize nodelta
2794            cases (get_index_v bool 4 nu' ? ?)
2795            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2796            |
2797            ]
Note: See TracBrowser for help on using the repository browser.