source: src/ASM/AssemblyProof.ma @ 982

Last change on this file since 982 was 982, checked in by boender, 8 years ago
  • this should work (see previous commit)
File size: 104.5 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4
5definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
6  λP.
7    P true ∧ P false.
8 
9let rec bitvector_elim_prop_internal
10  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
11  match m return λm. m ≤ n → BitVector (n - m) → Prop with
12  [ O    ⇒ λprf1. λprefix. P ?
13  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
14  ].
15  [ applyS prefix
16  | letin res ≝ (bit ::: prefix)
17    < (minus_S_S ? ?)
18    > (minus_Sn_m ? ?)
19  [ @ res
20  | @ prf2
21  ]
22  | /2/
23  ].
24qed.
25
26definition bitvector_elim_prop ≝
27  λn: nat.
28  λP: BitVector n → Prop.
29    bitvector_elim_prop_internal n P n ? ?.
30  [ @ (le_n ?)
31  | < (minus_n_n ?)
32    @ [[ ]]
33  ]
34qed.
35
36lemma eq_b_eq:
37  ∀b, c.
38    eq_b b c = true → b = c.
39  #b #c
40  cases b
41  cases c
42  normalize //
43qed.
44
45lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
46 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
47 #n #hd #tl #abs @⊥ //
48qed.
49
50lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
51 ∃hd.∃tl.v ≃ VCons bool n hd tl.
52 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
53 [ #abs @⊥ //
54 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
55qed.
56
57lemma eq_bv_eq:
58  ∀n, v, q.
59    eq_bv n v q = true → v = q.
60  #n #v #q generalize in match v
61  elim q
62  [ #v #h @BitVector_O
63  | #n #hd #tl #ih #v' #h
64    cases (BitVector_Sn ? v')
65    #hd' * #tl' #jmeq >jmeq in h;
66    #new_h
67    change in new_h with ((andb ? ?) = ?);
68    cases(conjunction_true … new_h)
69    #eq_heads #eq_tails
70    whd in eq_heads:(??(??(%))?);
71    cases(eq_b_eq … eq_heads)
72    whd in eq_tails:(??(?????(%))?);
73    change in eq_tails with (eq_bv ??? = ?);
74    <(ih tl') //
75  ]
76qed.
77
78lemma bool_eq_internal_eq:
79  ∀b, c.
80    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
81  #b #c
82  cases b
83  [ normalize //
84  | normalize
85    cases c
86    [ normalize //
87    | normalize //
88    ]
89  ]
90qed.
91
92lemma eq_bv_refl:
93  ∀n,v. eq_bv n v v = true.
94  #n #v
95  elim v
96  [ //
97  | #n #hd #tl #ih
98    normalize
99    cases hd
100    [ normalize
101      @ ih
102    | normalize
103      @ ih
104    ]
105  ]
106qed.
107
108lemma eq_eq_bv:
109  ∀n, v, q.
110    v = q → eq_bv n v q = true.
111  #n #v
112  elim v
113  [ #q #h <h normalize %
114  | #n #hd #tl #ih #q #h >h //
115  ]
116qed.
117
118definition bit_elim: ∀P: bool → bool. bool ≝
119  λP.
120    P true ∧ P false.
121
122let rec bitvector_elim_internal
123  (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
124  match m return λm. m ≤ n → BitVector (n - m) → bool with
125  [ O    ⇒ λprf1. λprefix. P ?
126  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
127  ].
128  [ applyS prefix
129  | letin res ≝ (bit ::: prefix)
130    < (minus_S_S ? ?)
131    > (minus_Sn_m ? ?)
132    [ @ res
133    | @ prf2
134    ]
135  | /2/
136  ].
137qed.
138
139definition bitvector_elim ≝
140  λn: nat.
141  λP: BitVector n → bool.
142    bitvector_elim_internal n P n ? ?.
143  [ @ (le_n ?)
144  | < (minus_n_n ?)
145    @ [[ ]]
146  ]
147qed.
148
149axiom vector_associative_append:
150  ∀A: Type[0].
151  ∀n, m, o:  nat.
152  ∀v: Vector A n.
153  ∀q: Vector A m.
154  ∀r: Vector A o.
155    ((v @@ q) @@ r)
156    ≃
157    (v @@ (q @@ r)).
158       
159lemma vector_cons_append:
160  ∀A: Type[0].
161  ∀n: nat.
162  ∀e: A.
163  ∀v: Vector A n.
164    e ::: v = [[ e ]] @@ v.
165  # A # N # E # V
166  elim V
167  [ normalize %
168  | # NN # AA # VV # IH
169    normalize
170    %
171  ]
172qed.
173
174lemma super_rewrite2:
175 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
176  ∀P: ∀m. Vector A m → Prop.
177   n=m → v1 ≃ v2 → P n v1 → P m v2.
178 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
179qed.
180
181lemma mem_middle_vector:
182  ∀A: Type[0].
183  ∀m, o: nat.
184  ∀eq: A → A → bool.
185  ∀reflex: ∀a. eq a a = true.
186  ∀p: Vector A m.
187  ∀a: A.
188  ∀r: Vector A o.
189    mem A eq ? (p@@(a:::r)) a = true.
190  # A # M # O # EQ # REFLEX # P # A
191  elim P
192  [ normalize
193    > (REFLEX A)
194    normalize
195    # H
196    %
197  | # NN # AA # PP # IH
198    normalize
199    cases (EQ A AA) //
200     @ IH
201  ]
202qed.
203
204lemma mem_monotonic_wrt_append:
205  ∀A: Type[0].
206  ∀m, o: nat.
207  ∀eq: A → A → bool.
208  ∀reflex: ∀a. eq a a = true.
209  ∀p: Vector A m.
210  ∀a: A.
211  ∀r: Vector A o.
212    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
213  # A # M # O # EQ # REFLEX # P # A
214  elim P
215  [ #R #H @H
216  | #NN #AA # PP # IH #R #H
217    normalize
218    cases (EQ A AA)
219    [ normalize %
220    | @ IH @ H
221    ]
222  ]
223qed.
224
225lemma subvector_multiple_append:
226  ∀A: Type[0].
227  ∀o, n: nat.
228  ∀eq: A → A → bool.
229  ∀refl: ∀a. eq a a = true.
230  ∀h: Vector A o.
231  ∀v: Vector A n.
232  ∀m: nat.
233  ∀q: Vector A m.
234    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
235  # A # O # N # EQ # REFLEX # H # V
236  elim V
237  [ normalize
238    # M # V %
239  | # NN # AA # VV # IH # MM # QQ
240    change with (bool_to_Prop (andb ??))
241    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
242    [
243    | # HH > HH
244      > (vector_cons_append ? ? AA VV)
245      change with (bool_to_Prop (subvector_with ??????))
246      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
247        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
248        ?
249        (vector_associative_append A ? ? ? QQ [[AA]] VV))
250      [ >associative_plus //
251      | @IH ]
252    ]
253    @(mem_monotonic_wrt_append)
254    [ @ REFLEX
255    | @(mem_monotonic_wrt_append)
256      [ @ REFLEX
257      | normalize
258        > REFLEX
259        normalize
260        %
261      ]
262    ]
263qed.
264
265lemma vector_cons_empty:
266  ∀A: Type[0].
267  ∀n: nat.
268  ∀v: Vector A n.
269    [[ ]] @@ v = v.
270  # A # N # V
271  elim V
272  [ normalize %
273  | # NN # HH # VV #H %
274  ]
275qed.
276
277corollary subvector_hd_tl:
278  ∀A: Type[0].
279  ∀o: nat.
280  ∀eq: A → A → bool.
281  ∀refl: ∀a. eq a a = true.
282  ∀h: A.
283  ∀v: Vector A o.
284    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
285  # A # O # EQ # REFLEX # H # V
286  > (vector_cons_append A ? H V)
287  < (vector_cons_empty A ? ([[H]] @@ V))
288  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
289qed.
290
291lemma eq_a_reflexive:
292  ∀a. eq_a a a = true.
293  # A
294  cases A
295  %
296qed.
297
298lemma is_in_monotonic_wrt_append:
299  ∀m, n: nat.
300  ∀p: Vector addressing_mode_tag m.
301  ∀q: Vector addressing_mode_tag n.
302  ∀to_search: addressing_mode.
303    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
304  # M # N # P # Q # TO_SEARCH
305  # H
306  elim Q
307  [ normalize
308    @ H
309  | # NN # PP # QQ # IH
310    normalize
311    cases (is_a PP TO_SEARCH)
312    [ normalize
313      %
314    | normalize
315      normalize in IH
316      @ IH
317    ]
318  ]
319qed.
320
321corollary is_in_hd_tl:
322  ∀to_search: addressing_mode.
323  ∀hd: addressing_mode_tag.
324  ∀n: nat.
325  ∀v: Vector addressing_mode_tag n.
326    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
327  # TO_SEARCH # HD # N # V
328  elim V
329  [ # H
330    normalize in H;
331    cases H
332  | # NN # HHD # VV # IH # HH
333    > vector_cons_append
334    > (vector_cons_append ? ? HHD VV)
335    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
336    @ HH
337  ]
338qed.
339 
340let rec list_addressing_mode_tags_elim
341  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
342  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
343   (l → bool) → bool ] with
344  [ VEmpty      ⇒  true 
345  | VCons len hd tl ⇒ λP.
346    let process_hd ≝
347      match hd return λhd. ∀P: hd:::tl → bool. bool with
348      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
349      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
350      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
351      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
352      | acc_a ⇒ λP.P ACC_A
353      | acc_b ⇒ λP.P ACC_B
354      | dptr ⇒ λP.P DPTR
355      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
356      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
357      | acc_dptr ⇒ λP.P ACC_DPTR
358      | acc_pc ⇒ λP.P ACC_PC
359      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
360      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
361      | carry ⇒ λP.P CARRY
362      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
363      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
364      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
365      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
366      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
367      ]
368    in
369      andb (process_hd P)
370       (match len return λx. x = len → bool with
371         [ O ⇒ λprf. true
372         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
373  ].
374  try %
375  [ 2: cases (sym_eq ??? prf); @tl
376  | generalize in match H; generalize in match tl; cases prf;
377    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
378    #tl
379    normalize in ⊢ (∀_: %. ?)
380    # H
381    whd
382    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
383    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
384qed.
385
386definition product_elim ≝
387  λm, n: nat.
388  λv: Vector addressing_mode_tag (S m).
389  λq: Vector addressing_mode_tag (S n).
390  λP: (v × q) → bool.
391    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
392
393definition union_elim ≝
394  λA, B: Type[0].
395  λelimA: (A → bool) → bool.
396  λelimB: (B → bool) → bool.
397  λelimU: A ⊎ B → bool.
398    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
399
400(*                           
401definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
402  λP.
403    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
404    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
405    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
406    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
407    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
408    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
409    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
410    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
411    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
412    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
413    P (DA ? ACC_A) ∧
414    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
415    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
416    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
417    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
418    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
419    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
420    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
421    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
422    P (RL ? ACC_A) ∧
423    P (RLC ? ACC_A) ∧
424    P (RR ? ACC_A) ∧
425    P (RRC ? ACC_A) ∧
426    P (SWAP ? ACC_A) ∧
427    P (RET ?) ∧
428    P (RETI ?) ∧
429    P (NOP ?) ∧
430    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
431    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
432    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
433    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
434    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
435                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
436                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
437    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
438    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
439                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
440                   (λd. P (XRL ? d)) ∧
441    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
442                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
443                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
444                   (λd. P (ANL ? d)) ∧
445    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
446                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
447                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
448                   (λd. P (ORL ? d)) ∧
449    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
450                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
451                   (λd. P (MOVX ? d)) ∧
452    union_elim ? ? (
453      union_elim ? ? (
454        union_elim ? ? (
455          union_elim ? ? (
456            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
457                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
458                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
459                            (product_elim ? ? [[dptr]] [[data16]]))
460                            (product_elim ? ? [[carry]] [[bit_addr]]))
461                            (product_elim ? ? [[bit_addr]] [[carry]])
462                            (λd. P (MOV ? d)).
463  %
464qed.
465 
466definition instruction_elim: ∀P: instruction → bool. bool ≝
467  λP. (*
468    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
469    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
470    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
471    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
472    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
473    P (JMP INDIRECT_DPTR) ∧
474    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
475    preinstruction_elim (λp. P (RealInstruction p)). *)
476  %
477qed.
478
479
480axiom instruction_elim_complete:
481 ∀P. instruction_elim P = true → ∀i. P i = true.
482*)
483(*definition eq_instruction ≝
484  λi, j: instruction.
485    true.*)
486axiom eq_instruction: instruction → instruction → bool.
487axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
488
489let rec vect_member
490  (A: Type[0]) (n: nat) (eq: A → A → bool)
491  (v: Vector A n) (a: A) on v: bool ≝
492  match v with
493  [ VEmpty          ⇒ false
494  | VCons len hd tl ⇒
495    eq hd a ∨ (vect_member A ? eq tl a)
496  ].
497
498let rec list_addressing_mode_tags_elim_prop
499  (n: nat)
500  (l: Vector addressing_mode_tag (S n))
501  on l:
502  ∀P: l → Prop.
503  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
504  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
505  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
506  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
507  ∀x: l. P x ≝
508  match l return
509    λy.
510      match y with
511      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
512      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
513               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
514               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
515               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
516               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
517               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
518               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
519               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
520               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
521               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
522               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
523               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
524               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
525               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
526               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
527               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
528               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
529               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
530               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
531               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
532               ∀x:l. P x
533      ] with
534  [ VEmpty          ⇒ λAbsurd. ⊥
535  | VCons len hd tl ⇒ λProof. ?
536  ] (refl ? (S n)). cases daemon. qed. (*
537  [ destruct(Absurd)
538  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
539    # A8 # A9 # A10 # A11 # A12 # A13 # A14
540    # A15 # A16 # A17 # A18 # A19 # X
541    cases X
542    # SUB cases daemon ] qed.
543    cases SUB
544    [ # BYTE
545    normalize
546  ].
547 
548 
549(*    let prepare_hd ≝
550      match hd with
551      [ direct ⇒ λdirect_prf. ?
552      | indirect ⇒ λindirect_prf. ?
553      | ext_indirect ⇒ λext_indirect_prf. ?
554      | registr ⇒ λregistr_prf. ?
555      | acc_a ⇒ λacc_a_prf. ?
556      | acc_b ⇒ λacc_b_prf. ?
557      | dptr ⇒ λdptr_prf. ?
558      | data ⇒ λdata_prf. ?
559      | data16 ⇒ λdata16_prf. ?
560      | acc_dptr ⇒ λacc_dptr_prf. ?
561      | acc_pc ⇒ λacc_pc_prf. ?
562      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
563      | indirect_dptr ⇒ λindirect_prf. ?
564      | carry ⇒ λcarry_prf. ?
565      | bit_addr ⇒ λbit_addr_prf. ?
566      | n_bit_addr ⇒ λn_bit_addr_prf. ?
567      | relative ⇒ λrelative_prf. ?
568      | addr11 ⇒ λaddr11_prf. ?
569      | addr16 ⇒ λaddr16_prf. ?
570      ]
571    in ? *)
572  ].
573  [ 1: destruct(absd)
574  | 2: # A1 # A2 # A3 # A4 # A5 # A6
575       # A7 # A8 # A9 # A10 # A11 # A12
576       # A13 # A14 # A15 # A16 # A17 # A18
577       # A19 *
578  ].
579
580
581  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
582   (l → bool) → bool ] with
583  [ VEmpty      ⇒  true 
584  | VCons len hd tl ⇒ λP.
585    let process_hd ≝
586      match hd return λhd. ∀P: hd:::tl → bool. bool with
587      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
588      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
589      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
590      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
591      | acc_a ⇒ λP.P ACC_A
592      | acc_b ⇒ λP.P ACC_B
593      | dptr ⇒ λP.P DPTR
594      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
595      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
596      | acc_dptr ⇒ λP.P ACC_DPTR
597      | acc_pc ⇒ λP.P ACC_PC
598      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
599      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
600      | carry ⇒ λP.P CARRY
601      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
602      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
603      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
604      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
605      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
606      ]
607    in
608      andb (process_hd P)
609       (match len return λx. x = len → bool with
610         [ O ⇒ λprf. true
611         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
612  ].
613  try %
614  [ 2: cases (sym_eq ??? prf); @tl
615  | generalize in match H; generalize in match tl; cases prf;
616    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
617    #tl
618    normalize in ⊢ (∀_: %. ?)
619    # H
620    whd
621    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
622    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
623qed.
624*)
625(*
626lemma test:
627  let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
628      (let assembled ≝ assembly1 i in
629      let code_memory ≝ load_code_memory assembled in
630      let fetched ≝ fetch code_memory ? in
631      let 〈instr_pc, ticks〉 ≝ fetched in
632        eq_instruction (\fst instr_pc)) i = true.
633 [2: @ zero
634 | normalize
635 ]*)
636
637lemma BitVectorTrie_O:
638 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
639 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
640  [ #w #_ %1 %[@w] %
641  | #n #l #r #abs @⊥ //
642  | #n #EQ %2 >EQ %]
643qed.
644
645lemma BitVectorTrie_Sn:
646 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
647 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
648  [ #m #abs @⊥ //
649  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
650  | #m #EQ %2 // ]
651qed.
652
653lemma lookup_prepare_trie_for_insertion_hit:
654 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
655  lookup … b (prepare_trie_for_insertion … b v) a = v.
656 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
657qed.
658 
659lemma lookup_insert_hit:
660 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
661  lookup … b (insert … b v t) a = v.
662 #A #a #v #n #b elim b -b -n //
663 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
664  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
665  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
666qed.
667
668coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
669
670lemma lookup_prepare_trie_for_insertion_miss:
671 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
672  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
673 #A #a #v #n #c elim c
674  [ #b >(BitVector_O … b) normalize #abs @⊥ //
675  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
676    cases hd cases hd' normalize
677    [2,3: #_ cases tl' //
678    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
679qed.
680 
681lemma lookup_insert_miss:
682 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
683  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
684 #A #a #v #n #c elim c -c -n
685  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
686  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
687    #t cases(BitVectorTrie_Sn … t)
688    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
689     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
690    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
691     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
692     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
693qed.
694
695definition load_code_memory_aux ≝
696 fold_left_i_aux … (
697   λi, mem, v.
698     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
699
700axiom split_elim:
701 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
702  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
703
704axiom half_add_SO:
705 ∀pc.
706 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
707
708(*
709axiom not_eqvb_S:
710 ∀pc.
711 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
712
713axiom not_eqvb_SS:
714 ∀pc.
715 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
716 
717axiom bitvector_elim_complete:
718 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
719
720lemma bitvector_elim_complete':
721 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
722 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
723 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
724qed.
725*)
726
727
728
729
730(*
731lemma andb_elim':
732 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
733 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
734qed.
735*)
736
737let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
738                       (encoding: list Byte) on encoding: Prop ≝
739  match encoding with
740  [ nil ⇒ final_pc = pc
741  | cons hd tl ⇒
742    let 〈new_pc, byte〉 ≝ next code_memory pc in
743      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
744  ].
745
746lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
747 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
748  let intermediate_pc ≝ pc + length … l1 in
749   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
750    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
751 #code_memory #final_pc #l1 elim l1
752  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
753  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
754    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
755qed.
756
757axiom bitvector_3_elim_prop:
758 ∀P: BitVector 3 → Prop.
759  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
760  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
761  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
762
763definition ticks_of_instruction ≝
764 λi.
765  let trivial_code_memory ≝ assembly1 i in
766  let trivial_status ≝ load_code_memory trivial_code_memory in
767   \snd (fetch trivial_status (zero ?)).
768
769axiom fetch_assembly:
770  ∀pc,i,code_memory,assembled.
771    assembled = assembly1 i →
772      let len ≝ length … assembled in
773      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
774      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
775      let 〈instr_pc, ticks〉 ≝ fetched in
776      let 〈instr,pc'〉 ≝ instr_pc in
777       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
778(* #pc #i #code_memory #assembled cases i [8: *]
779 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
780 [47,48,49:
781 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
782  [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,
783   59,60,63,64,65,66,67: #ARG]]
784 [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,
785  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
786  [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,
787   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,
788   68,69,70,71: #ARG2]]
789 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
790 normalize in ⊢ (???% → ?)
791 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
792  normalize in ⊢ (???% → ?)]
793 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
794 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
795 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
796 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
797 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
798 [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,
799  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,
800  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
801 whd >eq_instruction_refl >H4 @eq_bv_refl
802qed. *)
803
804let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
805 match expected with
806  [ nil ⇒ eq_bv … pc final_pc = true
807  | cons i tl ⇒
808     let fetched ≝ fetch code_memory pc in
809     let 〈instr_pc, ticks〉 ≝ fetched in
810     let 〈instr,pc'〉 ≝ instr_pc in
811      eq_instruction instr i = true ∧
812      ticks = (ticks_of_instruction i) ∧
813      fetch_many code_memory final_pc pc' tl].
814
815lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
816 #A #a #b #EQ destruct //
817qed.
818
819axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
820
821axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
822
823lemma fetch_assembly_pseudo:
824 ∀program,ppc,lookup_labels,lookup_datalabels.
825  ∀pi,code_memory,len,assembled,instructions,pc.
826   let expansion ≝ jump_expansion ppc program in
827   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
828    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
829     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
830      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
831 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
832 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
833 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
834 >EQ2a >EQ2b -EQ2a EQ2b;
835  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
836  generalize in match pc elim instructions
837  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
838  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
839    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
840    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
841    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
842    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % //
843    [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ]
844qed.
845
846(* This establishes the correspondence between pseudo program counters and
847   program counters. It is at the heart of the proof. *)
848(*CSC: code taken from build_maps *)
849definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
850 λinstr_list.λl:list labelled_instruction.
851  foldl ??
852   (λt,i.
853       match t with
854       [ None ⇒ None ?
855       | Some ppc_pc_map ⇒
856         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
857         let 〈program_counter, sigma_map〉 ≝ pc_map in
858         let 〈label, i〉 ≝ i in
859          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
860           [ None ⇒ None ?
861           | Some pc_ignore ⇒
862              let 〈pc,ignore〉 ≝ pc_ignore in
863              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
864       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
865
866definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
867 ≝ λprog.sigma00 prog (\snd prog).
868
869definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
870 λprogram,instr_list.
871  match sigma00 program instr_list with
872   [ None ⇒ None …
873   | Some result ⇒
874      let 〈ppc,pc_sigma_map〉 ≝ result in
875      let 〈pc,map〉 ≝ pc_sigma_map in
876       Some … 〈ppc,pc〉 ].
877
878definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
879 λinstr_list.
880  match sigma0 instr_list with
881  [ None ⇒ None ?
882  | Some result ⇒
883    let 〈ppc,pc_sigma_map〉 ≝ result in
884    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
885      if gtb pc (2^16) then
886        None ?
887      else
888        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
889
890(* stuff about policy *)
891
892lemma policy_ok: ∀p. sigma_safe p ≠ None ….
893 #instr_list whd in match (sigma_safe ?) whd in match (sigma0 ?)
894 
895definition sigma: pseudo_assembly_program → Word → Word ≝
896 λp.
897  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
898   [ None ⇒ λabs. ⊥
899   | Some r ⇒ λ_.r] (policy_ok p).
900 cases abs //
901qed.
902
903lemma length_append:
904 ∀A.∀l1,l2:list A.
905  |l1 @ l2| = |l1| + |l2|.
906 #A #l1 elim l1
907  [ //
908  | #hd #tl #IH #l2 normalize <IH //]
909qed.
910
911let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
912 match l with
913  [ nil ⇒ true
914  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
915
916lemma does_not_occur_None:
917 ∀id,i,list_instr.
918  does_not_occur id (list_instr@[〈None …,i〉]) =
919  does_not_occur id list_instr.
920 #id #i #list_instr elim list_instr
921  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
922qed.
923
924lemma does_not_occur_Some:
925 ∀id,id',i,list_instr.
926  eq_bv ? id' id = false →
927   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
928    does_not_occur id list_instr.
929 #id #id' #i #list_instr elim list_instr
930  [ #H normalize in H ⊢ %; >H %
931  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
932qed.
933
934lemma does_not_occur_absurd:
935 ∀id,i,list_instr.
936  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
937 #id #i #list_instr elim list_instr
938  [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
939    >eq_bv_refl %
940  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
941qed.
942
943let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
944 match l with
945  [ nil ⇒ false
946  | cons hd tl ⇒
947     if instruction_matches_identifier id hd then
948      does_not_occur id tl
949     else
950      occurs_exactly_once id tl ].
951
952lemma occurs_exactly_once_None:
953 ∀id,i,list_instr.
954  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
955  occurs_exactly_once id list_instr.
956 #id #i #list_instr elim list_instr
957  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
958qed.
959
960lemma occurs_exactly_once_Some:
961 ∀id,id',i,prefix.
962  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
963 #id #id' #i #prefix elim prefix
964  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
965    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
966  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
967    cases he; normalize nodelta
968     [ #H @ (IH H)
969     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
970       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
971       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
972        /2/ #H >does_not_occur_Some //
973       | #H @IH @H]]]
974qed.
975
976lemma index_of_internal_None: ∀i,id,instr_list,n.
977 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
978  index_of_internal ? (instruction_matches_identifier id) instr_list n =
979   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
980 #i #id #instr_list elim instr_list
981  [ #n #abs whd in abs; cases abs
982  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
983    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
984    [ #H %
985    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
986      [ #_ % | #abs cases abs ]]]
987qed.
988
989lemma index_of_internal_Some_miss: ∀i,id,id'.
990 eq_bv ? id' id = false →
991 ∀instr_list,n.
992 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
993  index_of_internal ? (instruction_matches_identifier id) instr_list n =
994   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
995 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
996 change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
997  [ #n #abs cases abs
998  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
999    [ // | #K @IH //]]
1000qed.
1001
1002lemma index_of_internal_Some_hit: ∀i,id.
1003 ∀instr_list,n.
1004  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1005   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
1006  = |instr_list| + n.
1007 #i #id #instr_list elim instr_list
1008  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
1009  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
1010    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
1011qed.
1012
1013lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
1014 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
1015  address_of_word_labels_code_mem instr_list id =
1016  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
1017 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1018 >(index_of_internal_None … H) %
1019qed.
1020
1021lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
1022 eq_bv ? id' id = false →
1023  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
1024   address_of_word_labels_code_mem instr_list id =
1025   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
1026 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
1027 >(index_of_internal_Some_miss … H) //
1028qed.
1029
1030lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
1031  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
1032   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
1033   = bitvector_of_nat … (|instr_list|).
1034 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
1035 >(index_of_internal_Some_hit … H) //
1036qed.
1037
1038axiom tech_pc_sigma00_append_Some:
1039 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
1040  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
1041   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
1042    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
1043
1044axiom tech_pc_sigma00_append_None:
1045 ∀program,prefix,i,ppc,pc,costs.
1046  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
1047   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
1048    → False.
1049
1050lemma eq_false_to_notb: ∀b. b = false → ¬ b.
1051 *; //
1052qed.
1053
1054lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
1055 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
1056qed.
1057
1058example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
1059 cases daemon.
1060qed.
1061
1062axiom construct_costs_sigma:
1063 ∀p,ppc,pc,pc',costs,costs',i.
1064  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
1065   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
1066    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
1067
1068definition build_maps' ≝
1069  λpseudo_program.
1070  let result ≝
1071   foldl_strong
1072    (option Identifier × pseudo_instruction)
1073    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
1074      let 〈labels,ppc_pc_costs〉 ≝ res in
1075      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
1076      let 〈pc',costs〉 ≝ pc_costs in
1077       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
1078       ppc' = length … pre ∧
1079       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
1080       ∀id. occurs_exactly_once id pre →
1081        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
1082    (\snd pseudo_program)
1083    (λprefix,i,tl,prf,t.
1084      let 〈labels, ppc_pc_costs〉 ≝ t in
1085      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
1086      let 〈pc,costs〉 ≝ pc_costs in
1087       let 〈label, i'〉 ≝ i in
1088       let labels ≝
1089         match label with
1090         [ None ⇒ labels
1091         | Some label ⇒
1092           let program_counter_bv ≝ bitvector_of_nat ? pc in
1093             insert ? ? label program_counter_bv labels
1094         ]
1095       in
1096         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
1097         [ None ⇒
1098            let dummy ≝ 〈labels,ppc_pc_costs〉 in
1099             dummy
1100         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
1101         ]
1102    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
1103  in
1104   let 〈labels, ppc_pc_costs〉 ≝ result in
1105   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
1106   let 〈pc, costs〉 ≝ pc_costs in
1107    〈labels, costs〉.
1108 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
1109 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
1110   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
1111   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
1112   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
1113   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
1114   | #id normalize nodelta; -labels1; cases label; normalize nodelta
1115     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
1116     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
1117       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
1118        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
1119          <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H]
1120        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
1121          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
1122 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
1123   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
1124qed.
1125
1126lemma build_maps_ok:
1127 ∀p:pseudo_assembly_program.
1128  let 〈labels,costs〉 ≝ build_maps' p in
1129   ∀pc.
1130    (nat_of_bitvector … pc) < length … (\snd p) →
1131     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
1132 #p cases p #preamble #instr_list
1133  elim instr_list
1134   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
1135   | #hd #tl #IH
1136    whd in ⊢ (match % with [ _ ⇒ ?])
1137   ]
1138qed.
1139*)
1140
1141(*
1142lemma rev_preserves_length:
1143 ∀A.∀l. length … (rev A l) = length … l.
1144  #A #l elim l
1145   [ %
1146   | #hd #tl #IH normalize >length_append normalize /2/ ]
1147qed.
1148
1149lemma rev_append:
1150 ∀A.∀l1,l2.
1151  rev A (l1@l2) = rev A l2 @ rev A l1.
1152 #A #l1 elim l1 normalize //
1153qed.
1154 
1155lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
1156 #A #l elim l
1157  [ //
1158  | #hd #tl #IH normalize >rev_append normalize // ]
1159qed.
1160
1161lemma split_len_Sn:
1162 ∀A:Type[0].∀l:list A.∀len.
1163  length … l = S len →
1164   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
1165 #A #l elim l
1166  [ normalize #len #abs destruct
1167  | #hd #tl #IH #len
1168    generalize in match (rev_rev … tl)
1169    cases (rev A tl) in ⊢ (??%? → ?)
1170     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
1171     | #a #l' #H <H normalize #EQ
1172      %[@(hd::rev … l')] %[@a] % //
1173      >length_append in EQ #EQ normalize in EQ; normalize;
1174      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
1175qed.
1176
1177lemma list_elim_rev:
1178 ∀A:Type[0].∀P:list A → Type[0].
1179  P [ ] → (∀l,a. P l → P (l@[a])) →
1180   ∀l. P l.
1181 #A #P #H1 #H2 #l
1182 generalize in match (refl … (length … l))
1183 generalize in ⊢ (???% → ?) #n generalize in match l
1184 elim n
1185  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
1186  | #m #IH #L #EQ
1187    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
1188qed.
1189
1190axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
1191axiom prefix_of_append:
1192 ∀A:Type[0].∀l,l1,l2:list A.
1193  is_prefix … l l1 → is_prefix … l (l1@l2).
1194axiom prefix_reflexive: ∀A,l. is_prefix A l l.
1195axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
1196
1197record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
1198
1199definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
1200 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
1201
1202definition app ≝
1203 λA:Type[0].λl1:Propify (list A).λl2:list A.
1204  match l1 with
1205   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
1206
1207lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
1208 #A * /3/
1209qed.
1210
1211lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
1212 #A * #l1 normalize //
1213qed.
1214
1215let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
1216 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
1217 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
1218 B (app … prefix l) ≝
1219  match l with
1220  [ nil ⇒ ? (* b *)
1221  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1222  ].
1223 [ applyS b
1224 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
1225qed.
1226
1227(*
1228let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
1229 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
1230  match l with
1231  [ nil ⇒ ? (* b *)
1232  | cons hd tl ⇒
1233     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
1234  ].
1235 [ applyS b
1236 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
1237qed.
1238*)
1239
1240definition foldll:
1241 ∀A:Type[0].∀B: Propify (list A) → Type[0].
1242  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
1243   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
1244 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1245
1246axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
1247axiom pprefix_of_append:
1248 ∀A:Type[0].∀l,l1,l2.
1249  is_pprefix A l l1 → is_pprefix A l (l1@l2).
1250axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
1251axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
1252
1253
1254axiom foldll':
1255 ∀A:Type[0].∀l: list A.
1256  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
1257  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
1258   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
1259 #A #l #B
1260 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
1261 
1262 
1263  #H #acc
1264 @foldll
1265  [
1266  |
1267  ]
1268 
1269 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
1270
1271
1272(*
1273record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
1274 { subset_wit:> A;
1275   subset_proof: P subset_wit
1276 }.
1277*)
1278
1279definition build_maps' ≝
1280  λpseudo_program.
1281  let 〈preamble,instr_list〉 ≝ pseudo_program in
1282  let result ≝
1283   foldll
1284    (option Identifier × pseudo_instruction)
1285    (λprefix.
1286      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1287       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
1288    (λprefix,t,i.
1289      let 〈labels, pc_costs〉 ≝ t in
1290      let 〈program_counter, costs〉 ≝ pc_costs in
1291       let 〈label, i'〉 ≝ i in
1292       let labels ≝
1293         match label with
1294         [ None ⇒ labels
1295         | Some label ⇒
1296           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1297             insert ? ? label program_counter_bv labels
1298         ]
1299       in
1300         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1301         [ None ⇒
1302            let dummy ≝ 〈labels,pc_costs〉 in
1303              dummy
1304         | Some construct ⇒ 〈labels, construct〉
1305         ]
1306    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
1307  in
1308   let 〈labels, pc_costs〉 ≝ result in
1309   let 〈pc, costs〉 ≝ pc_costs in
1310    〈labels, costs〉.
1311 [
1312 | @⊥
1313 | normalize % //
1314 ]
1315qed.
1316
1317definition build_maps' ≝
1318  λpseudo_program.
1319  let 〈preamble,instr_list〉 ≝ pseudo_program in
1320  let result ≝
1321   foldl
1322    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1323          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1324           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
1325    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1326          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1327           is_prefix ? instr_list_prefix' instr_list →
1328           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
1329    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
1330          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
1331           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
1332     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1333          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1334           is_prefix ? instr_list_prefix' instr_list →
1335           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
1336      let 〈labels, pc_costs〉 ≝ t in
1337      let 〈program_counter, costs〉 ≝ pc_costs in
1338       let 〈label, i'〉 ≝ i in
1339       let labels ≝
1340         match label with
1341         [ None ⇒ labels
1342         | Some label ⇒
1343           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
1344             insert ? ? label program_counter_bv labels
1345         ]
1346       in
1347         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
1348         [ None ⇒
1349            let dummy ≝ 〈labels,pc_costs〉 in
1350              dummy
1351         | Some construct ⇒ 〈labels, construct〉
1352         ]
1353    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
1354  in
1355   let 〈labels, pc_costs〉 ≝ result in
1356   let 〈pc, costs〉 ≝ pc_costs in
1357    〈labels, costs〉.
1358 [4: @(list_elim_rev ?
1359       (λinstr_list. list (
1360        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
1361          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
1362           is_prefix ? instr_list_prefix' instr_list →
1363           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
1364       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
1365      [ @[ ]
1366      | #l' #a #limage %2
1367        [ %[@a] #PREFIX #PREFIX_OK
1368        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
1369             THE INDUCTION HYPOTHESIS INSTEAD *)
1370          elim limage
1371           [ %1
1372           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
1373             @K1 @(prefix_of_append ???? K3)
1374           ] 
1375        ]
1376       
1377       
1378     
1379 
1380  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
1381     % [@ (LIST_PREFIX @ [i])] %
1382      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
1383      | (* DOABLE IN PRINCIPLE *)
1384      ]
1385 | (* assert false case *)
1386 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
1387 |   
1388*)
1389
1390axiom assembly_ok:
1391 ∀program,assembled,costs,labels.
1392  Some … 〈labels,costs〉 = build_maps program →
1393  Some … 〈assembled,costs〉 = assembly program →
1394  let code_memory ≝ load_code_memory assembled in
1395  let preamble ≝ \fst program in
1396  let datalabels ≝ construct_datalabels preamble in
1397  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1398  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
1399   ∀ppc,len,assembledi.
1400    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1401     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
1402      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
1403       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
1404
1405axiom bitvector_of_nat_nat_of_bitvector:
1406  ∀n,v.
1407    bitvector_of_nat n (nat_of_bitvector n v) = v.
1408
1409axiom assembly_ok_to_expand_pseudo_instruction_ok:
1410 ∀program,assembled,costs.
1411  Some … 〈assembled,costs〉 = assembly program →
1412   ∀ppc.
1413    let code_memory ≝ load_code_memory assembled in
1414    let preamble ≝ \fst program in   
1415    let data_labels ≝ construct_datalabels preamble in
1416    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1417    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1418    let expansion ≝ jump_expansion ppc program in
1419    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1420     ∃instructions.
1421      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
1422
1423lemma fetch_assembly_pseudo2:
1424 ∀program,assembled,costs,labels.
1425  Some … 〈labels,costs〉 = build_maps program →
1426  Some … 〈assembled,costs〉 = assembly program →
1427   ∀ppc.
1428    let code_memory ≝ load_code_memory assembled in
1429    let preamble ≝ \fst program in
1430    let data_labels ≝ construct_datalabels preamble in
1431    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
1432    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
1433    let expansion ≝ jump_expansion ppc program in
1434    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
1435     ∃instructions.
1436      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
1437       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
1438 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
1439 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
1440 letin code_memory ≝ (load_code_memory assembled)
1441 letin preamble ≝ (\fst program)
1442 letin data_labels ≝ (construct_datalabels preamble)
1443 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
1444 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
1445 whd in ⊢ (% → %)
1446 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
1447 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
1448 generalize in match (fetch_assembly_pseudo program ppc
1449  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
1450  (load_code_memory assembled));
1451 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
1452 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
1453 normalize nodelta in EXPAND; (* HERE *)
1454 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
1455 >bitvector_of_nat_nat_of_bitvector in H1; #H1
1456 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
1457 #H1 #H2
1458 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
1459 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
1460  [ #K3 % [2: % [% | @K3]] | @K1 ]
1461qed.
1462
1463(* OLD?
1464definition assembly_specification:
1465  ∀assembly_program: pseudo_assembly_program.
1466  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
1467  λpseudo_assembly_program.
1468  λcode_mem.
1469    ∀pc: Word.
1470      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
1471      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
1472      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
1473      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
1474      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
1475       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
1476      match pre_assembled with
1477       [ None ⇒ True
1478       | Some pc_code ⇒
1479          let 〈new_pc,code〉 ≝ pc_code in
1480           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
1481
1482axiom assembly_meets_specification:
1483  ∀pseudo_assembly_program.
1484    match assembly pseudo_assembly_program with
1485    [ None ⇒ True
1486    | Some code_mem_cost ⇒
1487      let 〈code_mem, cost〉 ≝ code_mem_cost in
1488        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
1489    ].
1490(*
1491  # PROGRAM
1492  [ cases PROGRAM
1493    # PREAMBLE
1494    # INSTR_LIST
1495    elim INSTR_LIST
1496    [ whd
1497      whd in ⊢ (∀_. %)
1498      # PC
1499      whd
1500    | # INSTR
1501      # INSTR_LIST_TL
1502      # H
1503      whd
1504      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
1505    ]
1506  | cases not_implemented
1507  ] *)
1508*)
1509
1510definition internal_pseudo_address_map ≝ list (BitVector 8).
1511
1512axiom low_internal_ram_of_pseudo_low_internal_ram:
1513 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1514
1515axiom high_internal_ram_of_pseudo_high_internal_ram:
1516 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
1517
1518axiom low_internal_ram_of_pseudo_internal_ram_hit:
1519 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
1520  member ? (eq_bv 8) (false:::addr) M = true →
1521   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1522   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
1523   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
1524   let bl ≝ lookup ? 7 addr ram (zero 8) in
1525   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
1526    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
1527
1528(* changed from add to sub *)
1529axiom low_internal_ram_of_pseudo_internal_ram_miss:
1530 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
1531  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
1532  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
1533  let carr ≝ get_index_v ? ? flags 1 ? in
1534  carr = false →
1535  member ? (eq_bv 8) (false:::Saddr) M = false →
1536   member ? (eq_bv 8) (false:::addr) M = false →
1537    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
1538  //
1539qed.
1540
1541definition addressing_mode_ok ≝
1542 λT.λM:internal_pseudo_address_map.λs:PreStatus T.
1543  λaddr:addressing_mode.
1544   match addr with
1545    [ DIRECT d ⇒
1546       ¬(member ? (eq_bv 8) d M) ∧
1547       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1548    | INDIRECT i ⇒
1549       let d ≝ get_register ? s [[false;false;i]] in
1550       ¬(member ? (eq_bv 8) d M) ∧
1551       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
1552    | EXT_INDIRECT _ ⇒ true
1553    | REGISTER _ ⇒ true
1554    | ACC_A ⇒ true
1555    | ACC_B ⇒ true
1556    | DPTR ⇒ true
1557    | DATA _ ⇒ true
1558    | DATA16 _ ⇒ true
1559    | ACC_DPTR ⇒ true
1560    | ACC_PC ⇒ true
1561    | EXT_INDIRECT_DPTR ⇒ true
1562    | INDIRECT_DPTR ⇒ true
1563    | CARRY ⇒ true
1564    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1565    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
1566    | RELATIVE _ ⇒ true
1567    | ADDR11 _ ⇒ true
1568    | ADDR16 _ ⇒ true ].
1569   
1570definition next_internal_pseudo_address_map0 ≝
1571  λT.
1572  λfetched.
1573  λM: internal_pseudo_address_map.
1574  λs: PreStatus T.
1575   match fetched with
1576    [ Comment _ ⇒ Some ? M
1577    | Cost _ ⇒ Some … M
1578    | Jmp _ ⇒ Some … M
1579    | Call _ ⇒
1580       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
1581    | Mov _ _ ⇒ Some … M
1582    | Instruction instr ⇒
1583       match instr with
1584        [ ADD addr1 addr2 ⇒
1585           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1586            Some ? M
1587           else
1588            None ?
1589        | ADDC addr1 addr2 ⇒
1590           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1591            Some ? M
1592           else
1593            None ?
1594        | SUBB addr1 addr2 ⇒
1595           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
1596            Some ? M
1597           else
1598            None ?       
1599        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
1600 
1601
1602definition next_internal_pseudo_address_map ≝
1603 λM:internal_pseudo_address_map.
1604  λs:PseudoStatus.
1605    next_internal_pseudo_address_map0 ?
1606     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
1607   
1608definition status_of_pseudo_status:
1609 internal_pseudo_address_map → PseudoStatus → option Status ≝
1610 λM,ps.
1611  let pap ≝ code_memory … ps in
1612   match assembly pap with
1613    [ None ⇒ None …
1614    | Some p ⇒
1615       let cm ≝ load_code_memory (\fst p) in
1616       let pc ≝ sigma pap (program_counter ? ps) in
1617       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
1618       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
1619        Some …
1620         (mk_PreStatus (BitVectorTrie Byte 16)
1621           cm
1622           lir
1623           hir
1624           (external_ram … ps)
1625           pc
1626           (special_function_registers_8051 … ps)
1627           (special_function_registers_8052 … ps)
1628           (p1_latch … ps)
1629           (p3_latch … ps)
1630           (clock … ps)) ].
1631
1632(*
1633definition write_at_stack_pointer':
1634 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
1635  λM: Type[0].
1636  λs: PreStatus M.
1637  λv: Byte.
1638    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
1639    let bit_zero ≝ get_index_v… nu O ? in
1640    let bit_1 ≝ get_index_v… nu 1 ? in
1641    let bit_2 ≝ get_index_v… nu 2 ? in
1642    let bit_3 ≝ get_index_v… nu 3 ? in
1643      if bit_zero then
1644        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1645                              v (low_internal_ram ? s) in
1646          set_low_internal_ram ? s memory
1647      else
1648        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
1649                              v (high_internal_ram ? s) in
1650          set_high_internal_ram ? s memory.
1651  [ cases l0 %
1652  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
1653qed.
1654
1655definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
1656 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
1657
1658  λticks_of.
1659  λs.
1660  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
1661  let ticks ≝ ticks_of (program_counter ? s) in
1662  let s ≝ set_clock ? s (clock ? s + ticks) in
1663  let s ≝ set_program_counter ? s pc in
1664    match instr with
1665    [ Instruction instr ⇒
1666       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
1667    | Comment cmt ⇒ s
1668    | Cost cst ⇒ s
1669    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
1670    | Call call ⇒
1671      let a ≝ address_of_word_labels s call in
1672      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1673      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1674      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
1675      let s ≝ write_at_stack_pointer' ? s pc_bl in
1676      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
1677      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
1678      let s ≝ write_at_stack_pointer' ? s pc_bu in
1679        set_program_counter ? s a
1680    | Mov dptr ident ⇒
1681       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
1682    ].
1683 [
1684 |2,3,4: %
1685 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
1686 |
1687 | %
1688 ]
1689 cases not_implemented
1690qed.
1691*)
1692
1693axiom execute_1_pseudo_instruction_preserves_code_memory:
1694 ∀ticks_of,ps.
1695  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
1696
1697(*
1698lemma execute_code_memory_unchanged:
1699 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
1700 #ticks #ps whd in ⊢ (??? (??%))
1701 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
1702  (program_counter pseudo_assembly_program ps)) #instr #pc
1703 whd in ⊢ (??? (??%)) cases instr
1704  [ #pre cases pre
1705     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1706       cases (split ????) #z1 #z2 %
1707     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1708       cases (split ????) #z1 #z2 %
1709     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
1710       cases (split ????) #z1 #z2 %
1711     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
1712       [ #x1 whd in ⊢ (??? (??%))
1713     | *: cases not_implemented
1714     ]
1715  | #comment %
1716  | #cost %
1717  | #label %
1718  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
1719    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
1720    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
1721    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
1722    (* CSC: ??? *)
1723  | #dptr #label (* CSC: ??? *)
1724  ]
1725  cases not_implemented
1726qed.
1727*)
1728
1729lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
1730 ∀M:internal_pseudo_address_map.
1731 ∀ps,ps': PseudoStatus.
1732  code_memory … ps = code_memory … ps' →
1733   match status_of_pseudo_status M ps with
1734    [ None ⇒ status_of_pseudo_status M ps' = None …
1735    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
1736    ].
1737 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
1738 generalize in match (refl … (assembly (code_memory … ps)))
1739 cases (assembly ?) in ⊢ (???% → %)
1740  [ #K whd whd in ⊢ (??%?) <H >K %
1741  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
1742qed.
1743
1744definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
1745  λprogram: pseudo_assembly_program.
1746  λppc: Word.
1747  λfetched.
1748    match fetched with
1749    [ Instruction instr ⇒
1750      match instr with
1751      [ JC lbl ⇒
1752        match jump_expansion ppc program with
1753        [ short_jump ⇒ 〈2, 2〉
1754        | medium_jump ⇒ ?
1755        | long_jump ⇒ 〈4, 4〉
1756        ]
1757      | JNC lbl ⇒
1758        match jump_expansion ppc program with
1759        [ short_jump ⇒ 〈2, 2〉
1760        | medium_jump ⇒ ?
1761        | long_jump ⇒ 〈4, 4〉
1762        ]
1763      | JB bit lbl ⇒
1764        match jump_expansion ppc program with
1765        [ short_jump ⇒ 〈2, 2〉
1766        | medium_jump ⇒ ?
1767        | long_jump ⇒ 〈4, 4〉
1768        ]
1769      | JNB bit lbl ⇒
1770        match jump_expansion ppc program with
1771        [ short_jump ⇒ 〈2, 2〉
1772        | medium_jump ⇒ ?
1773        | long_jump ⇒ 〈4, 4〉
1774        ]
1775      | JBC bit lbl ⇒
1776        match jump_expansion ppc program with
1777        [ short_jump ⇒ 〈2, 2〉
1778        | medium_jump ⇒ ?
1779        | long_jump ⇒ 〈4, 4〉
1780        ]
1781      | JZ lbl ⇒
1782        match jump_expansion ppc program with
1783        [ short_jump ⇒ 〈2, 2〉
1784        | medium_jump ⇒ ?
1785        | long_jump ⇒ 〈4, 4〉
1786        ]
1787      | JNZ lbl ⇒
1788        match jump_expansion ppc program with
1789        [ short_jump ⇒ 〈2, 2〉
1790        | medium_jump ⇒ ?
1791        | long_jump ⇒ 〈4, 4〉
1792        ]
1793      | CJNE arg lbl ⇒
1794        match jump_expansion ppc program with
1795        [ short_jump ⇒ 〈2, 2〉
1796        | medium_jump ⇒ ?
1797        | long_jump ⇒ 〈4, 4〉
1798        ]
1799      | DJNZ arg lbl ⇒
1800        match jump_expansion ppc program with
1801        [ short_jump ⇒ 〈2, 2〉
1802        | medium_jump ⇒ ?
1803        | long_jump ⇒ 〈4, 4〉
1804        ]
1805      | ADD arg1 arg2 ⇒
1806        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
1807         〈ticks, ticks〉
1808      | ADDC arg1 arg2 ⇒
1809        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
1810         〈ticks, ticks〉
1811      | SUBB arg1 arg2 ⇒
1812        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
1813         〈ticks, ticks〉
1814      | INC arg ⇒
1815        let ticks ≝ ticks_of_instruction (INC ? arg) in
1816         〈ticks, ticks〉
1817      | DEC arg ⇒
1818        let ticks ≝ ticks_of_instruction (DEC ? arg) in
1819         〈ticks, ticks〉
1820      | MUL arg1 arg2 ⇒
1821        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
1822         〈ticks, ticks〉
1823      | DIV arg1 arg2 ⇒
1824        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
1825         〈ticks, ticks〉
1826      | DA arg ⇒
1827        let ticks ≝ ticks_of_instruction (DA ? arg) in
1828         〈ticks, ticks〉
1829      | ANL arg ⇒
1830        let ticks ≝ ticks_of_instruction (ANL ? arg) in
1831         〈ticks, ticks〉
1832      | ORL arg ⇒
1833        let ticks ≝ ticks_of_instruction (ORL ? arg) in
1834         〈ticks, ticks〉
1835      | XRL arg ⇒
1836        let ticks ≝ ticks_of_instruction (XRL ? arg) in
1837         〈ticks, ticks〉
1838      | CLR arg ⇒
1839        let ticks ≝ ticks_of_instruction (CLR ? arg) in
1840         〈ticks, ticks〉
1841      | CPL arg ⇒
1842        let ticks ≝ ticks_of_instruction (CPL ? arg) in
1843         〈ticks, ticks〉
1844      | RL arg ⇒
1845        let ticks ≝ ticks_of_instruction (RL ? arg) in
1846         〈ticks, ticks〉
1847      | RLC arg ⇒
1848        let ticks ≝ ticks_of_instruction (RLC ? arg) in
1849         〈ticks, ticks〉
1850      | RR arg ⇒
1851        let ticks ≝ ticks_of_instruction (RR ? arg) in
1852         〈ticks, ticks〉
1853      | RRC arg ⇒
1854        let ticks ≝ ticks_of_instruction (RRC ? arg) in
1855         〈ticks, ticks〉
1856      | SWAP arg ⇒
1857        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
1858         〈ticks, ticks〉
1859      | MOV arg ⇒
1860        let ticks ≝ ticks_of_instruction (MOV ? arg) in
1861         〈ticks, ticks〉
1862      | MOVX arg ⇒
1863        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
1864         〈ticks, ticks〉
1865      | SETB arg ⇒
1866        let ticks ≝ ticks_of_instruction (SETB ? arg) in
1867         〈ticks, ticks〉
1868      | PUSH arg ⇒
1869        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
1870         〈ticks, ticks〉
1871      | POP arg ⇒
1872        let ticks ≝ ticks_of_instruction (POP ? arg) in
1873         〈ticks, ticks〉
1874      | XCH arg1 arg2 ⇒
1875        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
1876         〈ticks, ticks〉
1877      | XCHD arg1 arg2 ⇒
1878        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
1879         〈ticks, ticks〉
1880      | RET ⇒
1881        let ticks ≝ ticks_of_instruction (RET ?) in
1882         〈ticks, ticks〉
1883      | RETI ⇒
1884        let ticks ≝ ticks_of_instruction (RETI ?) in
1885         〈ticks, ticks〉
1886      | NOP ⇒
1887        let ticks ≝ ticks_of_instruction (NOP ?) in
1888         〈ticks, ticks〉
1889      ]
1890    | Comment comment ⇒ 〈0, 0〉
1891    | Cost cost ⇒ 〈0, 0〉
1892    | Jmp jmp ⇒ 〈2, 2〉
1893    | Call call ⇒ 〈2, 2〉
1894    | Mov dptr tgt ⇒ 〈2, 2〉
1895    ].
1896  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
1897qed.
1898
1899definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
1900  λprogram: pseudo_assembly_program.
1901  λppc: Word.
1902    let 〈preamble, pseudo〉 ≝ program in
1903    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
1904     ticks_of0 program ppc fetched.
1905
1906lemma get_register_set_program_counter:
1907 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
1908 #T #s #pc %
1909qed.
1910
1911lemma get_8051_sfr_set_program_counter:
1912 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
1913 #T #s #pc %
1914qed.
1915
1916lemma get_bit_addressable_sfr_set_program_counter:
1917 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
1918 #T #s #pc %
1919qed.
1920
1921lemma low_internal_ram_set_program_counter:
1922 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
1923 #T #s #pc %
1924qed.
1925
1926lemma get_arg_8_set_program_counter:
1927 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
1928  ∀T,s,pc,b.∀arg:l.
1929   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
1930 [2,3: cases arg; *; normalize //]
1931 #n #l #H #T #s #pc #b * *; [11: #NH @⊥ //] #X try #Y %
1932qed.
1933
1934lemma set_bit_addressable_sfr_set_code_memory:
1935  ∀T, U: Type[0].
1936  ∀ps: PreStatus ?.
1937  ∀code_mem.
1938  ∀x.
1939  ∀val.
1940  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
1941  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
1942  #T #U #ps #code_mem #x #val
1943  whd in ⊢ (??%?)
1944  whd in ⊢ (???(???%?))
1945  cases (eqb ? 128) [ normalize nodelta cases not_implemented
1946  | normalize nodelta
1947  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1948  | normalize nodelta
1949  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
1950  | normalize nodelta
1951  cases (eqb ? 176) [ normalize nodelta %
1952  | normalize nodelta
1953  cases (eqb ? 153) [ normalize nodelta %
1954  | normalize nodelta
1955  cases (eqb ? 138) [ normalize nodelta %
1956  | normalize nodelta
1957  cases (eqb ? 139) [ normalize nodelta %
1958  | normalize nodelta
1959  cases (eqb ? 140) [ normalize nodelta %
1960  | normalize nodelta
1961  cases (eqb ? 141) [ normalize nodelta %
1962  | normalize nodelta
1963  cases (eqb ? 200) [ normalize nodelta %
1964  | normalize nodelta
1965  cases (eqb ? 202) [ normalize nodelta %
1966  | normalize nodelta
1967  cases (eqb ? 203) [ normalize nodelta %
1968  | normalize nodelta
1969  cases (eqb ? 204) [ normalize nodelta %
1970  | normalize nodelta
1971  cases (eqb ? 205) [ normalize nodelta %
1972  | normalize nodelta
1973  cases (eqb ? 135) [ normalize nodelta %
1974  | normalize nodelta
1975  cases (eqb ? 136) [ normalize nodelta %
1976  | normalize nodelta
1977  cases (eqb ? 137) [ normalize nodelta %
1978  | normalize nodelta
1979  cases (eqb ? 152) [ normalize nodelta %
1980  | normalize nodelta
1981  cases (eqb ? 168) [ normalize nodelta %
1982  | normalize nodelta
1983  cases (eqb ? 184) [ normalize nodelta %
1984  | normalize nodelta
1985  cases (eqb ? 129) [ normalize nodelta %
1986  | normalize nodelta
1987  cases (eqb ? 130) [ normalize nodelta %
1988  | normalize nodelta
1989  cases (eqb ? 131) [ normalize nodelta %
1990  | normalize nodelta
1991  cases (eqb ? 208) [ normalize nodelta %
1992  | normalize nodelta
1993  cases (eqb ? 224) [ normalize nodelta %
1994  | normalize nodelta
1995  cases (eqb ? 240) [ normalize nodelta %
1996  | normalize nodelta
1997    cases not_implemented
1998  ]]]]]]]]]]]]]]]]]]]]]]]]]]
1999qed.
2000
2001lemma set_arg_8_set_code_memory:
2002  ∀n:nat.
2003  ∀l:Vector addressing_mode_tag (S n).
2004    ¬(is_in ? l ACC_PC) →
2005    ∀T: Type[0].
2006    ∀U: Type[0].
2007    ∀ps: PreStatus ?.
2008    ∀code_mem.
2009    ∀val.
2010    ∀b: l.
2011  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
2012  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
2013  [2,3: cases b; *; normalize //]
2014  #n #l #prf #T #U #ps #code_mem #val * *;
2015  [*:
2016    [1,2,3,4,8,9,15,16,17,18,19: #x]
2017    try #y whd in ⊢ (??(%)?)
2018    whd in ⊢ (???(???(%)?))
2019    [1,2:
2020      cases (split bool 4 4 ?)
2021      #nu' #nl'
2022      normalize nodelta
2023      cases (split bool 1 3 nu')
2024      #bit1' #ignore'
2025      normalize nodelta
2026      cases (get_index_v bool 4 nu' 0 ?)
2027      [1,2,3,4:
2028        normalize nodelta
2029        try %
2030        try (@(set_bit_addressable_sfr_set_code_memory T U ps code_mem x val))
2031        try (normalize in ⊢ (???(???%?)))
2032      ]
2033    |3,4: %
2034    |*:
2035       try normalize nodelta
2036       normalize cases (not_implemented)
2037    ]
2038 ]
2039 
2040
2041qed.
2042
2043axiom set_arg_8_set_program_counter:
2044  ∀n:nat.
2045  ∀l:Vector addressing_mode_tag (S n).
2046    ¬(is_in ? l ACC_PC) →
2047    ∀T: Type[0].
2048    ∀ps: PreStatus ?.
2049    ∀pc.
2050    ∀val.
2051    ∀b: l.
2052  set_arg_8 ? (set_program_counter T ps pc) b val =
2053  set_program_counter T (set_arg_8 ? ps b val) pc.
2054  [1,2: cases b; *; normalize //]
2055qed.
2056 
2057
2058lemma get_arg_8_set_code_memory:
2059 ∀T1,T2,s,code_mem,b,arg.
2060   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
2061 #T1 #T2 #s #code_mem #b #arg %
2062qed.
2063
2064lemma set_code_memory_set_flags:
2065 ∀T1,T2,s,f1,f2,f3,code_mem.
2066  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
2067   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
2068 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
2069qed.
2070
2071lemma set_program_counter_set_flags:
2072 ∀T1,s,f1,f2,f3,pc.
2073  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
2074   set_flags … (set_program_counter … s pc) f1 f2 f3.
2075 #T1 #s #f1 #f2 #f3 #pc  %
2076qed.
2077
2078lemma program_counter_set_flags:
2079 ∀T1,s,f1,f2,f3.
2080  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
2081 #T1 #s #f1 #f2 #f3 %
2082qed.
2083
2084lemma special_function_registers_8051_write_at_stack_pointer:
2085 ∀T,s,x.
2086    special_function_registers_8051 T (write_at_stack_pointer T s x)
2087  = special_function_registers_8051 T s.
2088 #T #s #x whd in ⊢ (??(??%)?)
2089 cases (split ????) #nu #nl normalize nodelta;
2090 cases (get_index_v bool ????) %
2091qed.
2092
2093lemma get_8051_sfr_write_at_stack_pointer:
2094 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
2095 #T #s #x #y whd in ⊢ (??%%) //
2096qed.
2097
2098lemma code_memory_write_at_stack_pointer:
2099 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
2100 #T #s #x whd in ⊢ (??(??%)?)
2101 cases (split ????) #nu #nl normalize nodelta;
2102 cases (get_index_v bool ????) %
2103qed.
2104
2105axiom low_internal_ram_write_at_stack_pointer:
2106 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2107  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2108  low_internal_ram ? s2 = low_internal_ram T2 s3 →
2109  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2110  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2111  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
2112   low_internal_ram T1
2113     (write_at_stack_pointer ?
2114       (set_8051_sfr ?
2115         (write_at_stack_pointer ?
2116           (set_8051_sfr ?
2117             (set_low_internal_ram ? s1
2118               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
2119             SFR_SP sp1)
2120          bl)
2121        SFR_SP sp2)
2122      bu)
2123   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
2124      (low_internal_ram ?
2125       (write_at_stack_pointer ?
2126         (set_8051_sfr ?
2127           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2128          SFR_SP sp2)
2129        pbu)).
2130       
2131axiom high_internal_ram_write_at_stack_pointer:
2132 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
2133  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
2134  high_internal_ram ? s2 = high_internal_ram T2 s3 →
2135  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
2136  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
2137  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
2138   high_internal_ram T1
2139     (write_at_stack_pointer ?
2140       (set_8051_sfr ?
2141         (write_at_stack_pointer ?
2142           (set_8051_sfr ?
2143             (set_high_internal_ram ? s1
2144               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2)))
2145             SFR_SP sp1)
2146          bl)
2147        SFR_SP sp2)
2148      bu)
2149   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
2150      (high_internal_ram ?
2151       (write_at_stack_pointer ?
2152         (set_8051_sfr ?
2153           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
2154          SFR_SP sp2)
2155        pbu)).
2156
2157lemma set_program_counter_set_low_internal_ram:
2158 ∀T,s,x,y.
2159  set_program_counter T (set_low_internal_ram … s x) y =
2160   set_low_internal_ram … (set_program_counter … s y) x.
2161 //
2162qed.
2163
2164lemma set_clock_set_low_internal_ram:
2165 ∀T,s,x,y.
2166  set_clock T (set_low_internal_ram … s x) y =
2167   set_low_internal_ram … (set_clock … s y) x.
2168 //
2169qed.
2170
2171lemma set_program_counter_set_high_internal_ram:
2172 ∀T,s,x,y.
2173  set_program_counter T (set_high_internal_ram … s x) y =
2174   set_high_internal_ram … (set_program_counter … s y) x.
2175 //
2176qed.
2177
2178lemma set_clock_set_high_internal_ram:
2179 ∀T,s,x,y.
2180  set_clock T (set_high_internal_ram … s x) y =
2181   set_high_internal_ram … (set_clock … s y) x.
2182 //
2183qed.
2184
2185lemma set_low_internal_ram_set_high_internal_ram:
2186 ∀T,s,x,y.
2187  set_low_internal_ram T (set_high_internal_ram … s x) y =
2188   set_high_internal_ram … (set_low_internal_ram … s y) x.
2189 //
2190qed.
2191
2192lemma external_ram_write_at_stack_pointer:
2193 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
2194 #T #s #x whd in ⊢ (??(??%)?)
2195 cases (split ????) #nu #nl normalize nodelta;
2196 cases (get_index_v bool ????) %
2197qed.
2198
2199lemma special_function_registers_8052_write_at_stack_pointer:
2200 ∀T,s,x.
2201    special_function_registers_8052 T (write_at_stack_pointer T s x)
2202  = special_function_registers_8052 T s.
2203 #T #s #x whd in ⊢ (??(??%)?)
2204 cases (split ????) #nu #nl normalize nodelta;
2205 cases (get_index_v bool ????) %
2206qed.
2207
2208lemma p1_latch_write_at_stack_pointer:
2209 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
2210 #T #s #x whd in ⊢ (??(??%)?)
2211 cases (split ????) #nu #nl normalize nodelta;
2212 cases (get_index_v bool ????) %
2213qed.
2214
2215lemma p3_latch_write_at_stack_pointer:
2216 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
2217 #T #s #x whd in ⊢ (??(??%)?)
2218 cases (split ????) #nu #nl normalize nodelta;
2219 cases (get_index_v bool ????) %
2220qed.
2221
2222lemma clock_write_at_stack_pointer:
2223 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
2224 #T #s #x whd in ⊢ (??(??%)?)
2225 cases (split ????) #nu #nl normalize nodelta;
2226 cases (get_index_v bool ????) %
2227qed.
2228
2229axiom get_index_v_set_index:
2230 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
2231
2232lemma get_8051_sfr_set_8051_sfr:
2233 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
2234 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
2235 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
2236qed.
2237
2238lemma program_counter_set_8051_sfr:
2239 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
2240 //
2241qed.
2242
2243lemma eq_rect_Type1_r:
2244  ∀A: Type[1].
2245  ∀a:A.
2246  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
2247  #A #a #P #H #x #p
2248  generalize in match H
2249  generalize in match P
2250  cases p
2251  //
2252qed.
2253
2254lemma split_eq_status:
2255 ∀T.
2256 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
2257 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
2258  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
2259   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
2260   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
2261 //
2262qed.
2263
2264axiom pair_elim':
2265  ∀A,B,C: Type[0].
2266  ∀T: A → B → C.
2267  ∀p.
2268  ∀P: A×B → C → Prop.
2269    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
2270      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
2271
2272axiom pair_elim'':
2273  ∀A,B,C,C': Type[0].
2274  ∀T: A → B → C.
2275  ∀T': A → B → C'.
2276  ∀p.
2277  ∀P: A×B → C → C' → Prop.
2278    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
2279      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
2280
2281axiom split_elim':
2282  ∀A: Type[0].
2283  ∀B: Type[1].
2284  ∀l, m, v.
2285  ∀T: Vector A l → Vector A m → B.
2286  ∀P: B → Prop.
2287    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
2288      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
2289
2290axiom split_elim'':
2291  ∀A: Type[0].
2292  ∀B,B': Type[1].
2293  ∀l, m, v.
2294  ∀T: Vector A l → Vector A m → B.
2295  ∀T': Vector A l → Vector A m → B'.
2296  ∀P: B → B' → Prop.
2297    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
2298      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
2299        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
2300
2301axiom split_append:
2302  ∀A: Type[0].
2303  ∀m, n: nat.
2304  ∀v, v': Vector A m.
2305  ∀q, q': Vector A n.
2306    let 〈v', q'〉 ≝ split A m n (v@@q) in
2307      v = v' ∧ q = q'.
2308
2309axiom split_vector_singleton:
2310  ∀A: Type[0].
2311  ∀n: nat.
2312  ∀v: Vector A (S n).
2313  ∀rest: Vector A n.
2314  ∀s: Vector A 1.
2315  ∀prf.
2316    v = s @@ rest →
2317    ((get_index_v A ? v 0 prf) ::: rest) = v.
2318
2319axiom sub_minus_one_seven_eight:
2320  ∀v: BitVector 7.
2321  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
2322  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
2323
2324lemma pair_destruct_1:
2325 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
2326 #A #B #a #b *; /2/
2327qed.
2328
2329lemma pair_destruct_2:
2330 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
2331 #A #B #a #b *; /2/
2332qed.
2333
2334(*
2335lemma blah:
2336  ∀m: internal_pseudo_address_map.
2337  ∀s: PseudoStatus.
2338  ∀arg: Byte.
2339  ∀b: bool.
2340    addressing_mode_ok m s (DIRECT arg) = true →
2341      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
2342      get_arg_8 ? s b (DIRECT arg).
2343  [2, 3: normalize % ]
2344  #m #s #arg #b #hyp
2345  whd in ⊢ (??%%)
2346  @split_elim''
2347  #nu' #nl' #arg_nu_nl_eq
2348  normalize nodelta
2349  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
2350  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
2351  #get_index_v_eq
2352  normalize nodelta
2353  [2:
2354    normalize nodelta
2355    @split_elim''
2356    #bit_one' #three_bits' #bit_one_three_bit_eq
2357    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
2358    normalize nodelta
2359    generalize in match (refl ? (sub_7_with_carry ? ? ?))
2360    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
2361    #Saddr #carr' #Saddr_carr_eq
2362    normalize nodelta
2363    #carr_hyp'
2364    @carr_hyp'
2365    [1:
2366    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
2367        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
2368        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
2369        #member_eq
2370        normalize nodelta
2371        [2: #destr destruct(destr)
2372        |1: -carr_hyp';
2373            >arg_nu_nl_eq
2374            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
2375            [1: >get_index_v_eq in ⊢ (??%? → ?)
2376            |2: @le_S @le_S @le_S @le_n
2377            ]
2378            cases (member (BitVector 8) ? (\fst ?) ?)
2379            [1: #destr normalize in destr; destruct(destr)
2380            |2:
2381            ]
2382        ]
2383    |3: >get_index_v_eq in ⊢ (??%?)
2384        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
2385        >(split_vector_singleton … bit_one_three_bit_eq)
2386        <arg_nu_nl_eq
2387        whd in hyp:(??%?)
2388        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
2389        normalize nodelta [*: #ignore @sym_eq ]
2390    ]
2391  |
2392  ].
2393*)
2394(*
2395map_address0 ... (DIRECT arg) = Some .. →
2396  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
2397  get_arg_8 (internal_ram ...) (DIRECT arg)
2398
2399((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
2400                     then Some internal_pseudo_address_map M 
2401                     else None internal_pseudo_address_map )
2402                    =Some internal_pseudo_address_map M')
2403*)
2404
2405lemma main_thm:
2406 ∀M,M',ps,s,s''.
2407  next_internal_pseudo_address_map M ps = Some … M' →
2408  status_of_pseudo_status M ps = Some … s →
2409  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
2410   ∃n. execute n s = s''.
2411 #M #M' #ps #s #s''
2412 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
2413 whd in ⊢ (? → ? → ??%? → ??%? → ?)
2414 >execute_1_pseudo_instruction_preserves_code_memory
2415 generalize in match (refl … (assembly (code_memory … ps)))
2416 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
2417 cases (build_maps (code_memory … ps))
2418  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
2419    #abs @⊥ normalize in abs; destruct (abs) ]
2420 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
2421 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
2422 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
2423  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
2424 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
2425 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
2426 #MAP
2427 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
2428 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
2429 change with
2430  (∃n.
2431    execute n
2432     (set_low_internal_ram ?
2433       (set_high_internal_ram ?
2434         (set_program_counter ?
2435           (set_code_memory ?? ps (load_code_memory assembled))
2436          (sigma 〈preamble,instr_list〉 (program_counter ? ps)))
2437        (high_internal_ram_of_pseudo_high_internal_ram M ?))
2438      (low_internal_ram_of_pseudo_low_internal_ram M ?))
2439   = set_low_internal_ram ?
2440      (set_high_internal_ram ?
2441        (set_program_counter ?
2442          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
2443         (sigma ??))
2444       ?)
2445     ?)
2446 whd in match (\snd 〈preamble,instr_list〉) in H;
2447 whd in match (\fst 〈preamble,instr_list〉) in H;
2448 whd in match (\snd 〈final_pc,assembled〉) in H;
2449 whd in match (\snd 〈preamble,instr_list〉) in MAP;
2450 -s s'' labels costs final_ppc final_pc;
2451 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
2452 (* NICE STATEMENT HERE *)
2453 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
2454 #K <K generalize in match K; -K;
2455 (* STATEMENT WITH EQUALITY HERE *)
2456 whd in ⊢ (???(?%?) → ?)
2457 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
2458 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
2459 #pi #newppc normalize nodelta; #MAP * #instructions *;
2460 cases pi in MAP; normalize nodelta;
2461  [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
2462    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
2463    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2464    #H2 >(eq_bv_to_eq … H2) >EQ %
2465(*  |6: (* Mov *) #arg1 #arg2
2466       #H1 #H2 #EQ %[@1]
2467       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2468       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2469       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2470       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2471       >H2b >(eq_instruction_to_eq … H2a)
2472       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2473       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
2474       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2475       normalize nodelta;
2476       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2477       #result #flags
2478       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
2479  |5: (* Call *) #label #MAP
2480      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
2481      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
2482       [ (* short *) #abs @⊥ destruct (abs)
2483       |3: (* long *) #H1 #H2 #EQ %[@1]
2484           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2485           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2486           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2487           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2488           >H2b >(eq_instruction_to_eq … H2a)
2489           generalize in match EQ; -EQ;
2490           whd in ⊢ (???% → ??%?);
2491           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;
2492           >(eq_bv_to_eq … H2c)
2493           change with
2494            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
2495                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2496           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
2497           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;
2498           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
2499           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
2500           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
2501           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2502           @split_eq_status;
2503            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
2504              >code_memory_write_at_stack_pointer %
2505            | >set_program_counter_set_low_internal_ram
2506              >set_clock_set_low_internal_ram
2507              @low_internal_ram_write_at_stack_pointer
2508               [ % | %
2509               | @(pair_destruct_2 … EQ1)
2510               | @(pair_destruct_2 … EQ2)
2511               | >(pair_destruct_1 ????? EQpc)
2512                 >(pair_destruct_2 ????? EQpc)
2513                 @split_elim #x #y #H <H -x y H;
2514                 >(pair_destruct_1 ????? EQppc)
2515                 >(pair_destruct_2 ????? EQppc)
2516                 @split_elim #x #y #H <H -x y H;
2517                 >EQ0 % ]
2518            | >set_low_internal_ram_set_high_internal_ram
2519              >set_program_counter_set_high_internal_ram
2520              >set_clock_set_high_internal_ram
2521              @high_internal_ram_write_at_stack_pointer
2522               [ % | %
2523               | @(pair_destruct_2 … EQ1)
2524               | @(pair_destruct_2 … EQ2)
2525               | >(pair_destruct_1 ????? EQpc)
2526                 >(pair_destruct_2 ????? EQpc)
2527                 @split_elim #x #y #H <H -x y H;
2528                 >(pair_destruct_1 ????? EQppc)
2529                 >(pair_destruct_2 ????? EQppc)
2530                 @split_elim #x #y #H <H -x y H;
2531                 >EQ0 % ]           
2532            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
2533              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2534              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
2535              >external_ram_write_at_stack_pointer %
2536            | change with (? = sigma ?(address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
2537              >EQ0 %
2538            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
2539              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2540              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
2541              >special_function_registers_8051_write_at_stack_pointer %
2542            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
2543              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2544              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
2545              >special_function_registers_8052_write_at_stack_pointer %
2546            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
2547              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2548              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
2549              >p1_latch_write_at_stack_pointer %
2550            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
2551              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2552              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
2553              >p3_latch_write_at_stack_pointer %
2554            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
2555              >clock_write_at_stack_pointer whd in ⊢ (???%)
2556              >clock_write_at_stack_pointer whd in ⊢ (???%)
2557              >clock_write_at_stack_pointer %]
2558       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2559         @pair_elim' #fst_5_addr #rest_addr #EQ1
2560         @pair_elim' #fst_5_pc #rest_pc #EQ2
2561         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2562         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2563         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2564         change in ⊢ (? →??%?) with (execute_1_0 ??)
2565         @pair_elim' * #instr #newppc' #ticks #EQn
2566          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
2567          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2568          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
2569          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
2570          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
2571          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
2572          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
2573          >get_8051_sfr_set_8051_sfr
2574         
2575          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
2576           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2577           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2578           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2579           generalize in match (refl … (split bool 4 4 pc_bu))
2580           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2581           generalize in match (refl … (split bool 3 8 rest_addr))
2582           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2583           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2584           generalize in match
2585            (refl …
2586             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2587             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2588           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
2589           @split_eq_status try %
2590            [ change with (? = sigma ? (address_of_word_labels ps label))
2591              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2592            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2593              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
2594  |4: (* Jmp *) #label #MAP
2595      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
2596      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
2597       [3: (* long *) #H1 #H2 #EQ %[@1]
2598           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2599           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2600           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2601           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2602           >H2b >(eq_instruction_to_eq … H2a)
2603           generalize in match EQ; -EQ;
2604           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2605           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
2606       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2607           generalize in match
2608            (refl ?
2609             (sub_16_with_carry
2610              (sigma 〈preamble,instr_list〉 (program_counter … ps))
2611              (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))
2612              false))
2613           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
2614           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
2615           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
2616           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
2617           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2618           change in ⊢ (? → ??%?) with (execute_1_0 ??)
2619           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2620           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2621           >H2b >(eq_instruction_to_eq … H2a)
2622           generalize in match EQ; -EQ;
2623           whd in ⊢ (???% → ?);
2624           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
2625           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
2626           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
2627           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
2628           @split_eq_status try % change with (newpc = sigma ? (address_of_word_labels ps label))
2629           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2630       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
2631         generalize in match
2632          (refl …
2633            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
2634         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
2635         generalize in match
2636          (refl …
2637            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
2638         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
2639         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
2640         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
2641         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
2642         change in ⊢ (? →??%?) with (execute_1_0 ??)
2643           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2644           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2645           >H2b >(eq_instruction_to_eq … H2a)
2646           generalize in match EQ; -EQ;
2647           whd in ⊢ (???% → ?);
2648           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
2649           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
2650           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
2651           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
2652           generalize in match (refl … (split bool 4 4 pc_bu))
2653           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
2654           generalize in match (refl … (split bool 3 8 rest_addr))
2655           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
2656           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
2657           generalize in match
2658            (refl …
2659             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
2660             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
2661           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
2662           @split_eq_status try %
2663            [ change with (? = sigma ? (address_of_word_labels ps label))
2664              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
2665            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
2666              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
2667  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
2668    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
2669       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2670       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2671       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2672       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2673       >H2b >(eq_instruction_to_eq … H2a)
2674       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
2675       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
2676       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
2677       normalize nodelta; #MAP;
2678       [1: change in ⊢ (? → %) with
2679        ((let 〈result,flags〉 ≝
2680          add_8_with_carry
2681           (get_arg_8 ? ps false ACC_A)
2682           (get_arg_8 ?
2683             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
2684             false (DIRECT ARG2))
2685           ? in ?) = ?)
2686       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
2687        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
2688       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
2689       #result #flags
2690       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
2691    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
2692       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
2693       change in ⊢ (? → ??%?) with (execute_1_0 ??)
2694       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
2695       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
2696       >H2b >(eq_instruction_to_eq … H2a)
2697       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
2698       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
2699       [1,2,3,4: cases (half_add ???) #carry #result
2700       | cases (half_add ???) #carry #bl normalize nodelta;
2701         cases (full_add ????) #carry' #bu normalize nodelta ]
2702        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
2703        [5: %
2704        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
2705      (set_program_counter pseudo_assembly_program ps newppc)
2706      (\fst  (ticks_of0 〈preamble,instr_list〉
2707                   (program_counter pseudo_assembly_program ps)
2708                   (Instruction (INC Identifier (DIRECT ARG))))
2709       +clock pseudo_assembly_program
2710        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
2711        [2,3: // ]
2712            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
2713            whd in ⊢ (??%%)
2714            cases (split bool 4 4 ARG)
2715            #nu' #nl'
2716            normalize nodelta
2717            cases (split bool 1 3 nu')
2718            #bit_1' #ignore'
2719            normalize nodelta
2720            cases (get_index_v bool 4 nu' ? ?)
2721            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
2722            |
2723            ]
Note: See TracBrowser for help on using the repository browser.