source: src/ASM/AssemblyProof.ma @ 992

Last change on this file since 992 was 992, checked in by mulligan, 9 years ago

a few more axioms closed

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