source: src/ASM/AssemblyProof.ma @ 1009

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

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

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